From: Andrew Reynolds Date: Fri, 20 Aug 2021 21:08:52 +0000 (-0500) Subject: Simplify how user-provided quantifier attributes are handled (#6963) X-Git-Tag: cvc5-1.0.0~1356 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4b184f5382921b35be5972de77ef5700fdbf505d;p=cvc5.git Simplify how user-provided quantifier attributes are handled (#6963) This makes INST_ATTRIBUTE (optionally) take multiple children, giving a way for the user to set attributes on quantified formulas, which does not require a new API command. This is a special case of term annotations that occur as the body of a quantified formula. If we need to extend our API to support further user-provided attributes, we should use a similar approach, e.g. a new kind ANNOTATE. --- diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 2c5d2873e..e8b876b55 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -3348,11 +3348,14 @@ enum CVC5_EXPORT Kind : int32_t * Specifies a custom property for a quantified formula given by a * term that is ascribed a user attribute. * - * Parameters: - * - 1: Term with a user attribute. + * Parameters: n >= 1 + * - 1: The keyword of the attribute (a term with kind CONST_STRING). + * - 2...n: The values of the attribute. * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child) const` + * - `mkTerm(Kind kind, Term child1, Term child2) + * - `mkTerm(Kind kind, Term child1, Term child2, Term child3) + * - `mkTerm(Kind kind, const std::vector& children) */ INST_ATTRIBUTE, /** diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 577aeb0a9..c3cf3ea66 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1815,26 +1815,15 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr] { std::stringstream sIntLit; sIntLit << $INTEGER_LITERAL; + api::Term keyword = SOLVER->mkString("quant-inst-max-level"); api::Term n = SOLVER->mkInteger(sIntLit.str()); - std::vector values; - values.push_back( n ); - std::string attr_name(AntlrInput::tokenText($tok)); - attr_name.erase( attr_name.begin() ); - api::Sort boolType = SOLVER->getBooleanSort(); - api::Term avar = PARSER_STATE->bindVar(attr_name, boolType); - retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); - Command* c = new SetUserAttributeCommand(attr_name, avar, values); - c->setMuted(true); - PARSER_STATE->preemptCommand(c); + retExpr = MK_TERM(api::INST_ATTRIBUTE, keyword, n); } | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr] { - api::Sort boolType = SOLVER->getBooleanSort(); - api::Term avar = SOLVER->mkConst(boolType, sexprToString(sexpr)); - retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); - Command* c = new SetUserAttributeCommand("qid", avar); - c->setMuted(true); - PARSER_STATE->preemptCommand(c); + api::Term keyword = SOLVER->mkString("qid"); + api::Term name = SOLVER->mkString(sexprToString(sexpr)); + retExpr = MK_TERM(api::INST_ATTRIBUTE, keyword, name); } | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] { diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 7aa05dde1..1981f1063 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1530,78 +1530,6 @@ void DeclareHeapCommand::toStream(std::ostream& out, out, sortToTypeNode(d_locSort), sortToTypeNode(d_dataSort)); } -/* -------------------------------------------------------------------------- */ -/* class SetUserAttributeCommand */ -/* -------------------------------------------------------------------------- */ - -SetUserAttributeCommand::SetUserAttributeCommand( - const std::string& attr, - api::Term term, - const std::vector& termValues, - const std::string& strValue) - : d_attr(attr), d_term(term), d_termValues(termValues), d_strValue(strValue) -{ -} - -SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr, - api::Term term) - : SetUserAttributeCommand(attr, term, {}, "") -{ -} - -SetUserAttributeCommand::SetUserAttributeCommand( - const std::string& attr, - api::Term term, - const std::vector& values) - : SetUserAttributeCommand(attr, term, values, "") -{ -} - -SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr, - api::Term term, - const std::string& value) - : SetUserAttributeCommand(attr, term, {}, value) -{ -} - -void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm) -{ - try - { - if (!d_term.isNull()) - { - solver->getSmtEngine()->setUserAttribute(d_attr, - termToNode(d_term), - termVectorToNodes(d_termValues), - d_strValue); - } - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetUserAttributeCommand::clone() const -{ - return new SetUserAttributeCommand(d_attr, d_term, d_termValues, d_strValue); -} - -std::string SetUserAttributeCommand::getCommandName() const -{ - return "set-user-attribute"; -} - -void SetUserAttributeCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - OutputLanguage language) const -{ - Printer::getPrinter(language)->toStreamCmdSetUserAttribute( - out, d_attr, termToNode(d_term)); -} - /* -------------------------------------------------------------------------- */ /* class SimplifyCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 5a67e6685..b83da5825 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -615,42 +615,6 @@ class CVC5_EXPORT DeclareHeapCommand : public Command api::Sort d_dataSort; }; -/** - * The command when an attribute is set by a user. In SMT-LIBv2 this is done - * via the syntax (! expr :attr) - */ -class CVC5_EXPORT SetUserAttributeCommand : public Command -{ - public: - SetUserAttributeCommand(const std::string& attr, api::Term term); - SetUserAttributeCommand(const std::string& attr, - api::Term term, - const std::vector& values); - SetUserAttributeCommand(const std::string& attr, - api::Term term, - const std::string& value); - - void invoke(api::Solver* solver, SymbolManager* sm) override; - Command* clone() const override; - std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; - - private: - SetUserAttributeCommand(const std::string& attr, - api::Term term, - const std::vector& termValues, - const std::string& strValue); - - const std::string d_attr; - const api::Term d_term; - const std::vector d_termValues; - const std::string d_strValue; -}; /* class SetUserAttributeCommand */ - /** * The command when parsing check-sat. * This command will check satisfiability of the input formula. @@ -1000,9 +964,6 @@ class CVC5_EXPORT GetModelCommand : public Command { public: GetModelCommand(); - - // Model is private to the library -- for now - // Model* getResult() const ; void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 185a60e46..e675feaa0 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" +#include "util/string.h" using namespace cvc5::theory; using namespace cvc5::kind; @@ -47,7 +48,6 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, "Expecting a quantified formula as argument to get-qe."); } NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); // ensure the body is rewritten q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1])); // do nested quantifier elimination if necessary @@ -56,14 +56,11 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, << q << std::endl; // tag the quantified formula with the quant-elim attribute TypeNode t = nm->booleanType(); - Node n_attr = sm->mkDummySkolem("qe", t, "Auxiliary variable for qe attr."); - std::vector node_values; TheoryEngine* te = d_smtSolver.getTheoryEngine(); Assert(te != nullptr); - te->setUserAttribute( - doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, ""); - QuantifiersEngine* qe = te->getQuantifiersEngine(); - n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr); + Node keyword = + nm->mkConst(String(doFull ? "quant-elim" : "quant-elim-partial")); + Node n_attr = nm->mkNode(INST_ATTRIBUTE, keyword); n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); std::vector children; children.push_back(q[0]); @@ -87,6 +84,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // failed, return original return q; } + QuantifiersEngine* qe = te->getQuantifiersEngine(); // must use original quantified formula to compute QE, which ensures that // e.g. term formula removal is not run on the body. Notice that we assume // that the (single) quantified formula is preprocessed, rewritten diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 61aed2009..f55bfa88b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1921,18 +1921,6 @@ void SmtEngine::printStatisticsDiff() const d_env->getStatisticsRegistry().storeSnapshot(); } -void SmtEngine::setUserAttribute(const std::string& attr, - Node expr, - const std::vector& expr_values, - const std::string& str_value) -{ - SmtScope smts(this); - finishInit(); - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - te->setUserAttribute(attr, expr, expr_values, str_value); -} - void SmtEngine::setOption(const std::string& key, const std::string& value) { NodeManagerScope nms(getNodeManager()); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index df8346de7..208c83db8 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -824,16 +824,6 @@ class CVC5_EXPORT SmtEngine */ void printStatisticsDiff() const; - /** - * Set user attribute. - * This function is called when an attribute is set by a user. - * In SMT-LIBv2 this is done via the syntax (! expr :attr) - */ - void setUserAttribute(const std::string& attr, - Node expr, - const std::vector& expr_values, - const std::string& str_value); - /** Get the options object (const and non-const versions) */ Options& getOptions(); const Options& getOptions() const; diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index ee07dcd57..218175ee9 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -116,12 +116,6 @@ void EngineOutputChannel::spendResource(Resource r) d_engine->spendResource(r); } -void EngineOutputChannel::handleUserAttribute(const char* attr, - theory::Theory* t) -{ - d_engine->handleUserAttribute(attr, t); -} - void EngineOutputChannel::trustedConflict(TrustNode pconf) { Assert(pconf.getKind() == TrustNodeKind::CONFLICT); diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index cc1d8ece7..468825a7e 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -61,8 +61,6 @@ class EngineOutputChannel : public theory::OutputChannel void spendResource(Resource r) override; - void handleUserAttribute(const char* attr, theory::Theory* t) override; - /** * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method * sends conf on the output channel of this class whose proof can be generated diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index 4561226e1..250082952 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -34,7 +34,7 @@ sort INST_PATTERN_TYPE \ # An instantiation pattern may have more than 1 child, in which case it specifies a multi-trigger. operator INST_PATTERN 1: "instantiation pattern" operator INST_NO_PATTERN 1 "instantiation no-pattern" -operator INST_ATTRIBUTE 1 "instantiation attribute" +operator INST_ATTRIBUTE 1: "instantiation attribute" operator INST_POOL 1: "instantiation pool" operator INST_ADD_TO_POOL 2 "instantiation add to pool" operator SKOLEM_ADD_TO_POOL 2 "skolemization add to pool" diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 33ed6f536..7204a60e1 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -35,7 +35,10 @@ bool QAttributes::isStandard() const QuantAttributes::QuantAttributes() {} -void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){ +void QuantAttributes::setUserAttribute(const std::string& attr, + TNode n, + const std::vector& nodeValues) +{ Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl; if (attr == "fun-def") { @@ -50,8 +53,8 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve QuantNameAttribute qna; n.setAttribute(qna, true); }else if( attr=="quant-inst-max-level" ){ - Assert(node_values.size() == 1); - uint64_t lvl = node_values[0].getConst().getNumerator().getLong(); + Assert(nodeValues.size() == 1); + uint64_t lvl = nodeValues[0].getConst().getNumerator().getLong(); Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl; QuantInstLevelAttribute qila; n.setAttribute( qila, lvl ); @@ -183,6 +186,7 @@ void QuantAttributes::computeAttributes( Node q ) { void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl; if( q.getNumChildren()==3 ){ + NodeManager* nm = NodeManager::currentNM(); qa.d_ipl = q[2]; for( unsigned i=0; imkBoundVar(nm->booleanType()); + std::vector nodeValues(q[2][i].begin() + 1, q[2][i].end()); + // set user attribute on the dummy variable + setUserAttribute( + q[2][i][0].getConst().toString(), avar, nodeValues); + } + else + { + // assume the dummy variable has already had its attributes set + avar = q[2][i][0]; + } if( avar.getAttribute(FunDefAttribute()) ){ Trace("quant-attr") << "Attribute : function definition : " << q << std::endl; //get operator directly from pattern @@ -222,9 +247,21 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ } if (avar.getAttribute(QuantNameAttribute())) { - Trace("quant-attr") << "Attribute : quantifier name : " << avar - << " for " << q << std::endl; - qa.d_name = avar; + // only set the name if there is a value + if (q[2][i].getNumChildren() > 1) + { + Trace("quant-attr") << "Attribute : quantifier name : " + << q[2][i][1].getConst().toString() + << " for " << q << std::endl; + // assign the name to a variable with the given name (to avoid + // enclosing the name in quotes) + qa.d_name = nm->mkBoundVar(q[2][i][1].getConst().toString(), + nm->booleanType()); + } + else + { + Warning() << "Missing name for qid attribute"; + } } if( avar.hasAttribute(QuantInstLevelAttribute()) ){ qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute()); diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 910dbab5b..48fb4f159 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -179,16 +179,15 @@ class QuantAttributes QuantAttributes(); ~QuantAttributes(){} /** set user attribute - * This function applies an attribute - * This can be called when we mark expressions with attributes, e.g. (! q - * :attribute attr [node_values, str_value...]), - * It can also be called internally in various ways (for SyGus, quantifier - * elimination, etc.) - */ + * This function applies an attribute + * This can be called when we mark expressions with attributes, e.g. (! q + * :attribute attr [nodeValues]), + * It can also be called internally in various ways (for SyGus, quantifier + * elimination, etc.) + */ static void setUserAttribute(const std::string& attr, - Node q, - std::vector& node_values, - std::string str_value); + TNode q, + const std::vector& nodeValues); /** compute quantifier attributes */ static void computeQuantAttributes(Node q, QAttributes& qa); diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index a108d4614..2ad475f01 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -40,12 +40,6 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm), d_qengine(nullptr) { - out.handleUserAttribute( "fun-def", this ); - out.handleUserAttribute("qid", this); - out.handleUserAttribute( "quant-inst-max-level", this ); - out.handleUserAttribute( "quant-elim", this ); - out.handleUserAttribute( "quant-elim-partial", this ); - // construct the quantifiers engine d_qengine.reset( new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, d_pnm)); @@ -188,10 +182,6 @@ bool TheoryQuantifiers::preNotifyFact( return true; } -void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value){ - QuantAttributes::setUserAttribute( attr, n, node_values, str_value ); -} - } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 0ef5cfcbb..1d721a0ae 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -77,10 +77,6 @@ class TheoryQuantifiers : public Theory { { return std::string("TheoryQuantifiers"); } - void setUserAttribute(const std::string& attr, - Node n, - std::vector node_values, - std::string str_value) override; private: /** The theory rewriter for this theory. */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.cpp b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp index 6fb377a56..14f066ce1 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.cpp +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp @@ -106,6 +106,18 @@ TypeNode QuantifierAnnotationTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { + if (n.getKind() == kind::INST_ATTRIBUTE) + { + if (n.getNumChildren() > 1) + { + // first must be a keyword + if (n[0].getKind() != kind::CONST_STRING) + { + throw TypeCheckingExceptionPrivate( + n[0], "Expecting a keyword at the head of INST_ATTRIBUTE."); + } + } + } return nodeManager->instPatternType(); } diff --git a/src/theory/theory.h b/src/theory/theory.h index bde00b908..44a0e597b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -775,15 +775,6 @@ class Theory { */ virtual std::string identify() const = 0; - /** Set user attribute - * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done - * via the syntax (! n :attr) - */ - virtual void setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value) { - Unimplemented() << "Theory " << identify() - << " doesn't support Theory::setUserAttribute interface"; - } - typedef context::CDList::const_iterator assertions_iterator; /** diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bd621126c..6bec3dc8f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -253,8 +253,7 @@ TheoryEngine::TheoryEngine(Env& env) d_false(), d_interrupted(false), d_inPreregister(false), - d_factsAsserted(d_env.getContext(), false), - d_attr_handle() + d_factsAsserted(d_env.getContext(), false) { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) @@ -1833,27 +1832,6 @@ TrustNode TheoryEngine::getExplanation( bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; } -void TheoryEngine::setUserAttribute(const std::string& attr, - Node n, - const std::vector& node_values, - const std::string& str_value) -{ - Trace("te-attr") << "set user attribute " << attr << " " << n << endl; - if( d_attr_handle.find( attr )!=d_attr_handle.end() ){ - for( size_t i=0; isetUserAttribute(attr, n, node_values, str_value); - } - } else { - //unhandled exception? - } -} - -void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) { - Trace("te-attr") << "Handle user attribute " << attr << " " << t << endl; - std::string str( attr ); - d_attr_handle[ str ].push_back( t ); -} - void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { Theory* theory = d_theoryTable[theoryId]; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3f2e589b3..e610adcf7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -660,27 +660,7 @@ public: /** Prints the assertions to the debug stream */ void printAssertions(const char* tag); -private: - - std::map< std::string, std::vector< theory::Theory* > > d_attr_handle; - public: - /** Set user attribute. - * - * This function is called when an attribute is set by a user. In SMT-LIBv2 - * this is done via the syntax (! n :attr) - */ - void setUserAttribute(const std::string& attr, - Node n, - const std::vector& node_values, - const std::string& str_value); - - /** Handle user attribute. - * - * Associates theory t with the attribute attr. Theory t will be - * notified whenever an attribute of name attr is set. - */ - void handleUserAttribute(const char* attr, theory::Theory* t); /** * Check that the theory assertions are satisfied in the model. diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index f1644dfcd..1cc6b0507 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -136,7 +136,6 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel void requirePhase(TNode, bool) override {} void setIncomplete(theory::IncompleteId id) override {} - void handleUserAttribute(const char* attr, theory::Theory* t) override {} void clear() { d_callHistory.clear(); }