From 24a40040a4a5f88f96eada87e46323ace729f06a Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 4 Aug 2020 15:23:54 -0500 Subject: [PATCH] Modify the smt2 parser to use the Sygus grammar. (#4829) --- src/api/cvc4cpp.cpp | 144 +++++++++++++++++++++++++----- src/api/cvc4cpp.h | 56 ++++++++++-- src/parser/smt2/Smt2.g | 79 +++------------- src/parser/smt2/smt2.cpp | 134 +++++---------------------- src/parser/smt2/smt2.h | 84 +++++++---------- src/printer/smt2/smt2_printer.cpp | 28 +++--- src/smt/command.cpp | 140 ++++++++++++++++------------- src/smt/command.h | 105 +++++++++++----------- src/smt/smt_engine.cpp | 4 +- 9 files changed, 388 insertions(+), 386 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index a1effec91..64f9dbd35 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1413,16 +1413,14 @@ size_t OpHashFunction::operator()(const Op& t) const Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {} -Term::Term(const Solver* slv, const CVC4::Expr& e) - : d_solver(slv) +Term::Term(const Solver* slv, const CVC4::Expr& e) : d_solver(slv) { // Ensure that we create the node in the correct node manager. NodeManagerScope scope(d_solver->getNodeManager()); d_node.reset(new CVC4::Node(e)); } -Term::Term(const Solver* slv, const CVC4::Node& n) - : d_solver(slv) +Term::Term(const Solver* slv, const CVC4::Node& n) : d_solver(slv) { // Ensure that we create the node in the correct node manager. NodeManagerScope scope(d_solver->getNodeManager()); @@ -2568,6 +2566,78 @@ void Grammar::addAnyVariable(Term ntSymbol) d_allowVars.insert(ntSymbol); } +/** + * this function concatinates the outputs of calling f on each element between + * first and last, seperated by sep. + * @param first the beginning of the range + * @param last the end of the range + * @param f the function to call on each element in the range, its output must + * be overloaded for operator<< + * @param sep the string to add between successive calls to f + */ +template +std::string join(Iterator first, Iterator last, Function f, std::string sep) +{ + std::stringstream ss; + Iterator i = first; + + if (i != last) + { + ss << f(*i); + ++i; + } + + while (i != last) + { + ss << sep << f(*i); + ++i; + } + + return ss.str(); +} + +std::string Grammar::toString() const +{ + std::stringstream ss; + ss << " (" // pre-declaration + << join( + d_ntSyms.cbegin(), + d_ntSyms.cend(), + [](const Term& t) { + std::stringstream s; + s << '(' << t << ' ' << t.getSort() << ')'; + return s.str(); + }, + " ") + << ")\n (" // grouped rule listing + << join( + d_ntSyms.cbegin(), + d_ntSyms.cend(), + [this](const Term& t) { + bool allowConst = d_allowConst.find(t) != d_allowConst.cend(), + allowVars = d_allowVars.find(t) != d_allowVars.cend(); + const std::vector& rules = d_ntsToTerms.at(t); + std::stringstream s; + s << '(' << t << ' ' << t.getSort() << " (" + << (allowConst ? "(Constant " + t.getSort().toString() + ")" + : "") + << (allowConst && allowVars ? " " : "") + << (allowVars ? "(Var " + t.getSort().toString() + ")" : "") + << ((allowConst || allowVars) && !rules.empty() ? " " : "") + << join( + rules.cbegin(), + rules.cend(), + [](const Term& rule) { return rule.toString(); }, + " ") + << "))"; + return s.str(); + }, + "\n ") + << ')'; + + return ss.str(); +} + Sort Grammar::resolve() { d_isResolved = true; @@ -2737,6 +2807,11 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const } } +std::ostream& operator<<(std::ostream& out, const Grammar& g) +{ + return out << g.toString(); +} + /* -------------------------------------------------------------------------- */ /* Rounding Mode for Floating Points */ /* -------------------------------------------------------------------------- */ @@ -4982,18 +5057,47 @@ bool Solver::getInterpolant(Term conj, Term& output) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; Expr result; bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), result); - if (success) { + if (success) + { output = Term(output.d_solver, result); } return success; CVC4_API_SOLVER_TRY_CATCH_END; } -bool Solver::getInterpolant(Term conj, const Type& gtype, Term& output) const +bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; Expr result; - bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), gtype, result); + bool success = d_smtEngine->getInterpol( + conj.d_node->toExpr(), *g.resolve().d_type, result); + if (success) + { + output = Term(output.d_solver, result); + } + return success; + CVC4_API_SOLVER_TRY_CATCH_END; +} + +bool Solver::getAbduct(Term conj, Term& output) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + Node result; + bool success = d_smtEngine->getAbduct(*conj.d_node, result); + if (success) + { + output = Term(output.d_solver, result); + } + return success; + CVC4_API_SOLVER_TRY_CATCH_END; +} + +bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + Node result; + bool success = d_smtEngine->getAbduct( + *conj.d_node, TypeNode::fromType(*g.resolve().d_type), result); if (success) { output = Term(output.d_solver, result); @@ -5149,38 +5253,38 @@ Grammar Solver::mkSygusGrammar(const std::vector& boundVars, { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols) - << "non-empty vector"; + << "a non-empty vector"; for (size_t i = 0, n = boundVars.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == boundVars[i].d_solver, "bound variable", boundVars[i], i) << "bound variable associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !boundVars[i].isNull(), "bound variable", boundVars[i], i) + << "a non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", boundVars[i], i) << "a bound variable"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !boundVars[i].isNull(), "parameter term", boundVars[i], i) - << "non-null term"; } for (size_t i = 0, n = ntSymbols.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == ntSymbols[i].d_solver, "term", ntSymbols[i], i) + this == ntSymbols[i].d_solver, "non-terminal", ntSymbols[i], i) << "term associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !ntSymbols[i].isNull(), "non-terminal", ntSymbols[i], i) + << "a non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, - "bound variable", + "non-terminal", ntSymbols[i], i) << "a bound variable"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !ntSymbols[i].isNull(), "parameter term", ntSymbols[i], i) - << "non-null term"; } return Grammar(this, boundVars, ntSymbols); @@ -5227,7 +5331,7 @@ Term Solver::synthFunHelper(const std::string& symbol, CVC4_API_ARG_CHECK_NOT_NULL(sort); CVC4_API_ARG_CHECK_EXPECTED(sort.d_type->isFirstClass(), sort) - << "first-class sort as codomain sort for function sort"; + << "first-class codomain sort for function"; std::vector varTypes; for (size_t i = 0, n = boundVars.size(); i < n; ++i) @@ -5235,15 +5339,15 @@ Term Solver::synthFunHelper(const std::string& symbol, CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == boundVars[i].d_solver, "bound variable", boundVars[i], i) << "bound variable associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !boundVars[i].isNull(), "bound variable", boundVars[i], i) + << "a non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", boundVars[i], i) << "a bound variable"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !boundVars[i].isNull(), "parameter term", boundVars[i], i) - << "non-null term"; varTypes.push_back(boundVars[i].d_node->getType().toType()); } CVC4_API_SOLVER_CHECK_SORT(sort); diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 30a0ad0a7..5d14e76a1 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -46,6 +46,7 @@ class DatatypeConstructorArg; class ExprManager; class NodeManager; class SmtEngine; +class SynthFunCommand; class Type; class Options; class Random; @@ -1950,6 +1951,7 @@ std::ostream& operator<<(std::ostream& out, class CVC4_PUBLIC Grammar { friend class Solver; + friend class CVC4::SynthFunCommand; public: /** @@ -1959,6 +1961,13 @@ class CVC4_PUBLIC Grammar */ void addRule(Term ntSymbol, Term rule); + /** + * Add to the set of rules corresponding to . + * @param ntSymbol the non-terminal to which the rules are added + * @param rule the rules to add + */ + void addRules(Term ntSymbol, std::vector rules); + /** * Allow to be an arbitrary constant. * @param ntSymbol the non-terminal allowed to be any constant @@ -1973,11 +1982,9 @@ class CVC4_PUBLIC Grammar void addAnyVariable(Term ntSymbol); /** - * Add to the set of rules corresponding to . - * @param ntSymbol the non-terminal to which the rules are added - * @param rule the rules to add + * @return a string representation of this grammar. */ - void addRules(Term ntSymbol, std::vector rules); + std::string toString() const; /** * Nullary constructor. Needed for the Cython API. @@ -2072,6 +2079,14 @@ class CVC4_PUBLIC Grammar bool d_isResolved; }; +/** + * Serialize a grammar to given stream. + * @param out the output stream + * @param g the grammar to be serialized to the given output stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_PUBLIC; + /* -------------------------------------------------------------------------- */ /* Rounding Mode for Floating Points */ /* -------------------------------------------------------------------------- */ @@ -3125,7 +3140,7 @@ class CVC4_PUBLIC Solver /** * Get an interpolant - * SMT-LIB: ( get-interpol ) + * SMT-LIB: ( get-interpol ) * Requires to enable option 'produce-interpols'. * @param conj the conjecture term * @param output a Term I such that A->I and I->B are valid, where A is the @@ -3136,15 +3151,40 @@ class CVC4_PUBLIC Solver /** * Get an interpolant - * SMT-LIB: ( get-interpol ) + * SMT-LIB: ( get-interpol ) * Requires to enable option 'produce-interpols'. * @param conj the conjecture term - * @param gtype the grammar for the interpolant I + * @param g the grammar for the interpolant I * @param output a Term I such that A->I and I->B are valid, where A is the * current set of assertions and B is given in the input by conj. * @return true if it gets I successfully, false otherwise. */ - bool getInterpolant(Term conj, const Type& gtype, Term& output) const; + bool getInterpolant(Term conj, Grammar& g, Term& output) const; + + /** + * Get an abduct. + * SMT-LIB: ( get-abduct ) + * Requires enabling option 'produce-abducts' + * @param conj the conjecture term + * @param output a term C such that A^C is satisfiable, and A^~B^C is + * unsatisfiable, where A is the current set of assertions and B is + * given in the input by conj + * @return true if it gets C successfully, false otherwise + */ + bool getAbduct(Term conj, Term& output) const; + + /** + * Get an abduct. + * SMT-LIB: ( get-abduct ) + * Requires enabling option 'produce-abducts' + * @param conj the conjecture term + * @param g the grammar for the abduct C + * @param output a term C such that A^C is satisfiable, and A^~B^C is + * unsatisfiable, where A is the current set of assertions and B is + * given in the input by conj + * @return true if it gets C successfully, false otherwise + */ + bool getAbduct(Term conj, Grammar& g, Term& output) const; /** * Print the model of a satisfiable query to the given output stream. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b88dc70b6..354f2d472 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -549,7 +549,7 @@ sygusCommand returns [std::unique_ptr cmd] std::unique_ptr synthFunFactory; std::string name, fun; bool isInv; - CVC4::api::Sort grammar; + CVC4::api::Grammar* grammar = nullptr; } : /* declare-var */ DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -560,7 +560,6 @@ sygusCommand returns [std::unique_ptr cmd] api::Term var = PARSER_STATE->bindBoundVar(name, t); cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType())); } - | /* synth-fun */ ( SYNTH_FUN_TOK { isInv = false; } | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); } @@ -618,23 +617,19 @@ sygusCommand returns [std::unique_ptr cmd] * The argument fun is a unique identifier to avoid naming clashes for the * datatypes constructed by this call. */ -sygusGrammar[CVC4::api::Sort & ret, +sygusGrammar[CVC4::api::Grammar*& ret, const std::vector& sygusVars, const std::string& fun] @declarations { // the pre-declaration - std::vector > sortedVarNames; + std::vector> sortedVarNames; // non-terminal symbols of the grammar std::vector ntSyms; CVC4::api::Sort t; std::string name; CVC4::api::Term e, e2; - std::vector datatypes; - std::set unresTypes; - std::map ntsToUnres; unsigned dtProcessed = 0; - std::unordered_set allowConst; } : // predeclaration @@ -675,21 +670,13 @@ sygusGrammar[CVC4::api::Sort & ret, PARSER_STATE->pushScope(true); for (std::pair& i : sortedVarNames) { - Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl; - // make the datatype, which encodes terms generated by this non-terminal - std::string dname = i.first; - datatypes.push_back(SOLVER->mkDatatypeDecl(dname)); - // make its unresolved type, used for referencing the final version of - // the datatype - PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); - api::Sort urt = PARSER_STATE->mkUnresolvedType(dname); - unresTypes.insert(urt); + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT); // make the non-terminal symbol, which will be parsed as an ordinary // free variable. api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second); ntSyms.push_back(nts); - ntsToUnres[nts] = urt; } + ret = PARSER_STATE->mkGrammar(sygusVars, ntSyms); } // the grouped rule listing LPAREN_TOK @@ -719,17 +706,15 @@ sygusGrammar[CVC4::api::Sort & ret, ( term[e,e2] { // add term as constructor to datatype - PARSER_STATE->addSygusConstructorTerm( - datatypes[dtProcessed], e, ntsToUnres); + ret->addRule(ntSyms[dtProcessed], e); } | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK { - // allow constants in datatypes[dtProcessed] - allowConst.insert(dtProcessed); + // allow constants in datatype for ntSyms[dtProcessed] + ret->addAnyConstant(ntSyms[dtProcessed]); } | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK { // add variable constructors to datatype - PARSER_STATE->addSygusConstructorVariables( - datatypes[dtProcessed], sygusVars, t); + ret->addAnyVariable(ntSyms[dtProcessed]); } )+ RPAREN_TOK @@ -740,45 +725,8 @@ sygusGrammar[CVC4::api::Sort & ret, )+ RPAREN_TOK { - if (dtProcessed != sortedVarNames.size()) - { - PARSER_STATE->parseError( - "Number of grouped rule listings does not match " - "number of symbols in predeclaration."); - } - api::Term bvl; - if (!sygusVars.empty()) - { - bvl = MK_TERM(api::BOUND_VAR_LIST, sygusVars); - } - Trace("parser-sygus2") << "Process " << dtProcessed << " sygus datatypes..." << std::endl; - for (unsigned i = 0; i < dtProcessed; i++) - { - bool aci = allowConst.find(i)!=allowConst.end(); - api::Sort btt = sortedVarNames[i].second; - datatypes[i].getDatatype().setSygus(btt.getType(), bvl.getExpr(), aci, false); - Trace("parser-sygus2") << "- " << datatypes[i].getName() - << ", #cons= " << datatypes[i].getNumConstructors() - << ", aci= " << aci << std::endl; - // We can be in a case where the only rule specified was (Variable T) - // and there are no variables of type T, in which case this is a bogus - // grammar. This results in the error below. - if (datatypes[i].getNumConstructors() == 0) - { - std::stringstream se; - se << "Grouped rule listing for " << datatypes[i].getName() - << " produced an empty rule list."; - PARSER_STATE->parseError(se.str()); - } - } // pop scope from the pre-declaration PARSER_STATE->popScope(); - // now, make the sygus datatype - Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl; - std::vector datatypeTypes = - SOLVER->mkDatatypeSorts(datatypes, unresTypes); - // return is the first datatype - ret = api::Sort(datatypeTypes[0]); } ; @@ -966,6 +914,7 @@ extendedCommand[std::unique_ptr* cmd] std::vector sorts; std::vector > sortedVarNames; std::unique_ptr seq; + api::Grammar* g = nullptr; } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ @@ -1131,10 +1080,10 @@ extendedCommand[std::unique_ptr* cmd] symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[e,e2] ( - sygusGrammar[t, terms, name] + sygusGrammar[g, terms, name] )? { - cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType())); + cmd->reset(new GetAbductCommand(SOLVER, name, e, g)); } | GET_INTERPOL_TOK { PARSER_STATE->checkThatLogicIsSet(); @@ -1142,10 +1091,10 @@ extendedCommand[std::unique_ptr* cmd] symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[e,e2] ( - sygusGrammar[t, terms, name] + sygusGrammar[g, terms, name] )? { - cmd->reset(new GetInterpolCommand(SOLVER, name, e, t.getType())); + cmd->reset(new GetInterpolCommand(SOLVER, name, e, g)); } | DECLARE_HEAP LPAREN_TOK sortSymbol[t, CHECK_DECLARED] diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index eef23edfd..fa0f8af43 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -487,11 +487,11 @@ void Smt2::resetAssertions() { Smt2::SynthFunFactory::SynthFunFactory( Smt2* smt2, - const std::string& fun, + const std::string& id, bool isInv, api::Sort range, std::vector>& sortedVarNames) - : d_smt2(smt2), d_fun(fun), d_isInv(isInv) + : d_smt2(smt2), d_id(id), d_sort(range), d_isInv(isInv) { if (range.isNull()) { @@ -501,37 +501,32 @@ Smt2::SynthFunFactory::SynthFunFactory( { smt2->parseError("Cannot use synth-fun with function return type."); } + std::vector varSorts; for (const std::pair& p : sortedVarNames) { varSorts.push_back(p.second); } - Debug("parser-sygus") << "Define synth fun : " << fun << std::endl; - api::Sort synthFunType = - varSorts.size() > 0 ? d_smt2->getSolver()->mkFunctionSort(varSorts, range) - : range; + + api::Sort funSort = varSorts.empty() + ? range + : d_smt2->d_solver->mkFunctionSort(varSorts, range); // we do not allow overloading for synth fun - d_synthFun = d_smt2->bindBoundVar(fun, synthFunType); - // set the sygus type to be range by default, which is overwritten below - // if a grammar is provided - d_sygusType = range; + d_fun = d_smt2->bindBoundVar(id, funSort); + + Debug("parser-sygus") << "Define synth fun : " << id << std::endl; d_smt2->pushScope(true); d_sygusVars = d_smt2->bindBoundVars(sortedVarNames); } -Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); } - -std::unique_ptr Smt2::SynthFunFactory::mkCommand(api::Sort grammar) +std::unique_ptr Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar) { - Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl; + Debug("parser-sygus") << "...read synth fun " << d_id << std::endl; + d_smt2->popScope(); return std::unique_ptr(new SynthFunCommand( - d_fun, - d_synthFun.getExpr(), - grammar.isNull() ? d_sygusType.getType() : grammar.getType(), - d_isInv, - api::termVectorToExprs(d_sygusVars))); + d_smt2->d_solver, d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar)); } std::unique_ptr Smt2::invConstraint( @@ -762,6 +757,14 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) return cmd; } /* Smt2::setLogic() */ +api::Grammar* Smt2::mkGrammar(const std::vector& boundVars, + const std::vector& ntSymbols) +{ + d_allocGrammars.emplace_back(new api::Grammar( + std::move(d_solver->mkSygusGrammar(boundVars, ntSymbols)))); + return d_allocGrammars.back().get(); +} + bool Smt2::sygus() const { InputLanguage ilang = getLanguage(); @@ -906,99 +909,6 @@ api::Term Smt2::mkAbstractValue(const std::string& name) return d_solver->mkAbstractValue(name.substr(1)); } - -void Smt2::addSygusConstructorTerm( - api::DatatypeDecl& dt, - api::Term term, - std::map& ntsToUnres) const -{ - Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl; - // At this point, we should know that dt is well founded, and that its - // builtin sygus operators are well-typed. - // Now, purify each occurrence of a non-terminal symbol in term, replace by - // free variables. These become arguments to constructors. Notice we must do - // a tree traversal in this function, since unique paths to the same term - // should be treated as distinct terms. - // Notice that let expressions are forbidden in the input syntax of term, so - // this does not lead to exponential behavior with respect to input size. - std::vector args; - std::vector cargs; - api::Term op = purifySygusGTerm(term, ntsToUnres, args, cargs); - std::stringstream ssCName; - ssCName << op.getKind(); - Trace("parser-sygus2") << "Purified operator " << op - << ", #args/cargs=" << args.size() << "/" - << cargs.size() << std::endl; - if (!args.empty()) - { - api::Term lbvl = d_solver->mkTerm(api::BOUND_VAR_LIST, args); - // its operator is a lambda - op = d_solver->mkTerm(api::LAMBDA, lbvl, op); - } - Trace("parser-sygus2") << "addSygusConstructor: operator " << op - << std::endl; - dt.getDatatype().addSygusConstructor( - op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs)); -} - -api::Term Smt2::purifySygusGTerm(api::Term term, - std::map& ntsToUnres, - std::vector& args, - std::vector& cargs) const -{ - Trace("parser-sygus2-debug") - << "purifySygusGTerm: " << term - << " #nchild=" << term.getExpr().getNumChildren() << std::endl; - std::map::iterator itn = ntsToUnres.find(term); - if (itn != ntsToUnres.end()) - { - api::Term ret = d_solver->mkVar(term.getSort()); - Trace("parser-sygus2-debug") - << "...unresolved non-terminal, intro " << ret << std::endl; - args.push_back(api::Term(d_solver, ret.getExpr())); - cargs.push_back(itn->second); - return ret; - } - std::vector pchildren; - bool childChanged = false; - for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++) - { - Trace("parser-sygus2-debug") - << "......purify child " << i << " : " << term[i] << std::endl; - api::Term ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs); - pchildren.push_back(ptermc); - childChanged = childChanged || ptermc != term[i]; - } - if (!childChanged) - { - Trace("parser-sygus2-debug") << "...no child changed" << std::endl; - return term; - } - api::Term nret = d_solver->mkTerm(term.getOp(), pchildren); - Trace("parser-sygus2-debug") - << "...child changed, return " << nret << std::endl; - return nret; -} - -void Smt2::addSygusConstructorVariables(api::DatatypeDecl& dt, - const std::vector& sygusVars, - api::Sort type) const -{ - // each variable of appropriate type becomes a sygus constructor in dt. - for (unsigned i = 0, size = sygusVars.size(); i < size; i++) - { - api::Term v = sygusVars[i]; - if (v.getSort() == type) - { - std::stringstream ss; - ss << v; - std::vector cargs; - dt.getDatatype().addSygusConstructor( - v.getExpr(), ss.str(), api::sortVectorToTypes(cargs)); - } - } -} - InputLanguage Smt2::getLanguage() const { return d_solver->getOptions().getInputLanguage(); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 579fa90ce..2e725f9bf 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -60,6 +60,11 @@ class Smt2 : public Parser */ std::unordered_map d_indexedOpKindMap; std::pair d_lastNamedTerm; + /** + * A list of sygus grammar objects. We keep track of them here to ensure that + * they don't get deleted before the commands using them get invoked. + */ + std::vector> d_allocGrammars; protected: Smt2(api::Solver* solver, @@ -198,7 +203,7 @@ class Smt2 : public Parser * Creates an instance of `SynthFunFactory`. * * @param smt2 Pointer to the parser state - * @param fun Name of the function to synthesize + * @param id Name of the function to synthesize * @param isInv True if the goal is to synthesize an invariant, false * otherwise * @param range The return type of the function-to-synthesize @@ -206,11 +211,10 @@ class Smt2 : public Parser */ SynthFunFactory( Smt2* smt2, - const std::string& fun, + const std::string& id, bool isInv, api::Sort range, std::vector>& sortedVarNames); - ~SynthFunFactory(); const std::vector& getSygusVars() const { return d_sygusVars; } @@ -220,13 +224,13 @@ class Smt2 : public Parser * @param grammar Optional grammar associated with the synth-fun command * @return The instance of `SynthFunCommand` */ - std::unique_ptr mkCommand(api::Sort grammar); + std::unique_ptr mkCommand(api::Grammar* grammar); private: Smt2* d_smt2; - std::string d_fun; - api::Term d_synthFun; - api::Sort d_sygusType; + std::string d_id; + api::Term d_fun; + api::Sort d_sort; bool d_isInv; std::vector d_sygusVars; }; @@ -257,6 +261,15 @@ class Smt2 : public Parser */ const LogicInfo& getLogic() const { return d_logic; } + /** + * Create a Sygus grammar. + * @param boundVars the parameters to corresponding synth-fun/synth-inv + * @param ntSymbols the pre-declaration of the non-terminal symbols + * @return a pointer to the grammar + */ + api::Grammar* mkGrammar(const std::vector& boundVars, + const std::vector& ntSymbols); + bool v2_0() const { return getLanguage() == language::input::LANG_SMTLIB_V2_0; @@ -308,10 +321,13 @@ class Smt2 : public Parser */ void checkLogicAllowsFunctions(); - void checkUserSymbol(const std::string& name) { - if(name.length() > 0 && (name[0] == '.' || name[0] == '@')) { + void checkUserSymbol(const std::string& name) + { + if (name.length() > 0 && (name[0] == '.' || name[0] == '@')) + { std::stringstream ss; - ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIB"; + ss << "cannot declare or define symbol `" << name + << "'; symbols starting with . and @ are reserved in SMT-LIB"; parseError(ss.str()); } else if (isOperatorEnabled(name)) @@ -329,7 +345,8 @@ class Smt2 : public Parser d_lastNamedTerm = std::make_pair(e, name); } - void clearLastNamedTerm() { + void clearLastNamedTerm() + { d_lastNamedTerm = std::make_pair(api::Term(), ""); } @@ -345,31 +362,6 @@ class Smt2 : public Parser */ api::Term mkAbstractValue(const std::string& name); - /** - * Adds a constructor to sygus datatype dt whose sygus operator is term. - * - * ntsToUnres contains a mapping from non-terminal symbols to the unresolved - * types they correspond to. This map indicates how the argument term should - * be interpreted (instances of symbols from the domain of ntsToUnres - * correspond to constructor arguments). - * - * The sygus operator that is actually added to dt corresponds to replacing - * each occurrence of non-terminal symbols from the domain of ntsToUnres - * with bound variables via purifySygusGTerm, and binding these variables - * via a lambda. - */ - void addSygusConstructorTerm( - api::DatatypeDecl& dt, - api::Term term, - std::map& ntsToUnres) const; - /** - * This adds constructors to dt for sygus variables in sygusVars whose - * type is argument type. This method should be called when the sygus grammar - * term (Variable type) is encountered. - */ - void addSygusConstructorVariables(api::DatatypeDecl& dt, - const std::vector& sygusVars, - api::Sort type) const; /** * Smt2 parser provides its own checkDeclaration, which does the * same as the base, but with some more helpful errors. @@ -475,22 +467,6 @@ class Smt2 : public Parser //------------------------- end processing parse operators private: - /** Purify sygus grammar term - * - * This returns a term where all occurrences of non-terminal symbols (those - * in the domain of ntsToUnres) are replaced by fresh variables. For each - * variable replaced in this way, we add the fresh variable it is replaced - * with to args, and the unresolved type corresponding to the non-terminal - * symbol to cargs (constructor args). In other words, args contains the - * free variables in the term returned by this method (which should be bound - * by a lambda), and cargs contains the types of the arguments of the - * sygus constructor. - */ - api::Term purifySygusGTerm(api::Term term, - std::map& ntsToUnres, - std::vector& args, - std::vector& cargs) const; - void addArithmeticOperators(); void addTranscendentalOperators(); @@ -519,7 +495,7 @@ class Smt2 : public Parser api::Term mkAnd(const std::vector& es); }; /* class Smt2 */ -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ +} // namespace parser +} // namespace CVC4 #endif /* CVC4__PARSER__SMT2_H */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d6b304a78..45cc2426c 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -2071,33 +2071,32 @@ static void toStream(std::ostream& out, const SynthFunCommand* c) { out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol()) << ' '; - Type type = c->getFunction().getType(); - const std::vector& vars = c->getVars(); - Assert(!type.isFunction() || !vars.empty()); + const std::vector& vars = c->getVars(); out << '('; - if (type.isFunction()) + if (!vars.empty()) { // print variable list - std::vector::const_iterator i = vars.begin(), i_end = vars.end(); - Assert(i != i_end); - out << '(' << *i << ' ' << i->getType() << ')'; + std::vector::const_iterator i = vars.begin(), i_end = vars.end(); + out << '(' << *i << ' ' << i->getSort() << ')'; ++i; while (i != i_end) { - out << " (" << *i << ' ' << i->getType() << ')'; + out << " (" << *i << ' ' << i->getSort() << ')'; ++i; } - FunctionType ft = type; - type = ft.getRangeType(); } out << ')'; // if not invariant-to-synthesize, print return type if (!c->isInv()) { - out << ' ' << type; + out << ' ' << c->getSort(); } + out << '\n'; // print grammar, if any - toStreamSygusGrammar(out, c->getSygusType()); + if (c->getGrammar() != nullptr) + { + out << *c->getGrammar(); + } out << ')'; } @@ -2152,7 +2151,10 @@ static void toStream(std::ostream& out, const GetAbductCommand* c) out << c->getConjecture(); // print grammar, if any - toStreamSygusGrammar(out, c->getGrammarType()); + if (c->getGrammar() != nullptr) + { + out << *c->getGrammar(); + } out << ')'; } diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 2e36190b4..97a51277b 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -90,7 +90,6 @@ ostream& operator<<(ostream& out, const CommandStatus* s) return out; } - /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) { @@ -137,7 +136,7 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) Command::Command() : d_commandStatus(nullptr), d_muted(false) {} -Command::Command(api::Solver* solver) +Command::Command(const api::Solver* solver) : d_solver(solver), d_commandStatus(nullptr), d_muted(false) { } @@ -652,40 +651,49 @@ std::string DeclareSygusFunctionCommand::getCommandName() const } /* -------------------------------------------------------------------------- */ -/* class SynthFunCommand */ +/* class SynthFunCommand */ /* -------------------------------------------------------------------------- */ -SynthFunCommand::SynthFunCommand(const std::string& id, - Expr func, - Type sygusType, +SynthFunCommand::SynthFunCommand(const api::Solver* solver, + const std::string& id, + api::Term fun, + const std::vector& vars, + api::Sort sort, bool isInv, - const std::vector& vars) + api::Grammar* g) : DeclarationDefinitionCommand(id), - d_func(func), - d_sygusType(sygusType), + d_fun(fun), + d_vars(vars), + d_sort(sort), d_isInv(isInv), - d_vars(vars) + d_grammar(g) { + d_solver = solver; } -SynthFunCommand::SynthFunCommand(const std::string& id, - Expr func, - Type sygusType, - bool isInv) - : SynthFunCommand(id, func, sygusType, isInv, {}) +api::Term SynthFunCommand::getFunction() const { return d_fun; } + +const std::vector& SynthFunCommand::getVars() const { + return d_vars; } -Expr SynthFunCommand::getFunction() const { return d_func; } -const std::vector& SynthFunCommand::getVars() const { return d_vars; } -Type SynthFunCommand::getSygusType() const { return d_sygusType; } +api::Sort SynthFunCommand::getSort() const { return d_sort; } bool SynthFunCommand::isInv() const { return d_isInv; } +const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; } + void SynthFunCommand::invoke(SmtEngine* smtEngine) { try { - smtEngine->declareSynthFun(d_symbol, d_func, d_sygusType, d_isInv, d_vars); + smtEngine->declareSynthFun(d_symbol, + d_fun.getExpr(), + d_grammar == nullptr + ? d_sort.getType() + : d_grammar->resolve().getType(), + d_isInv, + api::termVectorToExprs(d_vars)); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -697,15 +705,13 @@ void SynthFunCommand::invoke(SmtEngine* smtEngine) Command* SynthFunCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SynthFunCommand(d_symbol, - d_func.exportTo(exprManager, variableMap), - d_sygusType.exportTo(exprManager, variableMap), - d_isInv); + Unimplemented(); } Command* SynthFunCommand::clone() const { - return new SynthFunCommand(d_symbol, d_func, d_sygusType, d_isInv, d_vars); + return new SynthFunCommand( + d_solver, d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar); } std::string SynthFunCommand::getCommandName() const @@ -1352,7 +1358,7 @@ Command* DefineNamedFunctionCommand::clone() const /* -------------------------------------------------------------------------- */ DefineFunctionRecCommand::DefineFunctionRecCommand( - api::Solver* solver, + const api::Solver* solver, api::Term func, const std::vector& formals, api::Term formula, @@ -1365,7 +1371,7 @@ DefineFunctionRecCommand::DefineFunctionRecCommand( } DefineFunctionRecCommand::DefineFunctionRecCommand( - api::Solver* solver, + const api::Solver* solver, const std::vector& funcs, const std::vector>& formals, const std::vector& formulas, @@ -2094,40 +2100,49 @@ std::string GetSynthSolutionCommand::getCommandName() const return "get-instantiations"; } -GetInterpolCommand::GetInterpolCommand(api::Solver* solver, +/* -------------------------------------------------------------------------- */ +/* class GetInterpolCommand */ +/* -------------------------------------------------------------------------- */ + +GetInterpolCommand::GetInterpolCommand(const api::Solver* solver, const std::string& name, api::Term conj) : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false) { } -GetInterpolCommand::GetInterpolCommand(api::Solver* solver, +GetInterpolCommand::GetInterpolCommand(const api::Solver* solver, const std::string& name, api::Term conj, - const Type& gtype) + api::Grammar* g) : Command(solver), d_name(name), d_conj(conj), - d_sygus_grammar_type(gtype), + d_sygus_grammar(g), d_resultStatus(false) { } api::Term GetInterpolCommand::getConjecture() const { return d_conj; } -Type GetInterpolCommand::getGrammarType() const { return d_sygus_grammar_type; } + +const api::Grammar* GetInterpolCommand::getGrammar() const +{ + return d_sygus_grammar; +} + api::Term GetInterpolCommand::getResult() const { return d_result; } void GetInterpolCommand::invoke(SmtEngine* smtEngine) { try { - if (d_sygus_grammar_type.isNull()) + if (!d_sygus_grammar) { d_resultStatus = d_solver->getInterpolant(d_conj, d_result); } else { d_resultStatus = - d_solver->getInterpolant(d_conj, d_sygus_grammar_type, d_result); + d_solver->getInterpolant(d_conj, *d_sygus_grammar, d_result); } d_commandStatus = CommandSuccess::instance(); } @@ -2167,7 +2182,8 @@ Command* GetInterpolCommand::exportTo(ExprManager* exprManager, Command* GetInterpolCommand::clone() const { - GetInterpolCommand* c = new GetInterpolCommand(d_solver, d_name, d_conj); + GetInterpolCommand* c = + new GetInterpolCommand(d_solver, d_name, d_conj, d_sygus_grammar); c->d_result = d_result; c->d_resultStatus = d_resultStatus; return c; @@ -2178,42 +2194,50 @@ std::string GetInterpolCommand::getCommandName() const return "get-interpol"; } -GetAbductCommand::GetAbductCommand() {} -GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj) - : d_name(name), d_conj(conj), d_resultStatus(false) +/* -------------------------------------------------------------------------- */ +/* class GetAbductCommand */ +/* -------------------------------------------------------------------------- */ + +GetAbductCommand::GetAbductCommand(const api::Solver* solver, + const std::string& name, + api::Term conj) + : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false) { } -GetAbductCommand::GetAbductCommand(const std::string& name, - Expr conj, - const Type& gtype) - : d_name(name), +GetAbductCommand::GetAbductCommand(const api::Solver* solver, + const std::string& name, + api::Term conj, + api::Grammar* g) + : Command(solver), + d_name(name), d_conj(conj), - d_sygus_grammar_type(gtype), + d_sygus_grammar(g), d_resultStatus(false) { } -Expr GetAbductCommand::getConjecture() const { return d_conj; } -Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; } +api::Term GetAbductCommand::getConjecture() const { return d_conj; } + +const api::Grammar* GetAbductCommand::getGrammar() const +{ + return d_sygus_grammar; +} + std::string GetAbductCommand::getAbductName() const { return d_name; } -Expr GetAbductCommand::getResult() const { return d_result; } +api::Term GetAbductCommand::getResult() const { return d_result; } void GetAbductCommand::invoke(SmtEngine* smtEngine) { try { - Node conjNode = Node::fromExpr(d_conj); - Node resn; - if (d_sygus_grammar_type.isNull()) + if (!d_sygus_grammar) { - d_resultStatus = smtEngine->getAbduct(conjNode, resn); + d_resultStatus = d_solver->getAbduct(d_conj, d_result); } else { - TypeNode gtype = TypeNode::fromType(d_sygus_grammar_type); - d_resultStatus = smtEngine->getAbduct(conjNode, gtype, resn); + d_resultStatus = d_solver->getAbduct(d_conj, *d_sygus_grammar, d_result); } - d_result = resn.toExpr(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2246,19 +2270,13 @@ void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const Command* GetAbductCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAbductCommand* c = - new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap)); - c->d_sygus_grammar_type = - d_sygus_grammar_type.exportTo(exprManager, variableMap); - c->d_result = d_result.exportTo(exprManager, variableMap); - c->d_resultStatus = d_resultStatus; - return c; + Unimplemented(); } Command* GetAbductCommand::clone() const { - GetAbductCommand* c = new GetAbductCommand(d_name, d_conj); - c->d_sygus_grammar_type = d_sygus_grammar_type; + GetAbductCommand* c = + new GetAbductCommand(d_solver, d_name, d_conj, d_sygus_grammar); c->d_result = d_result; c->d_resultStatus = d_resultStatus; return c; diff --git a/src/smt/command.h b/src/smt/command.h index 552847fee..1674e0a62 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -121,6 +121,7 @@ class CVC4_PUBLIC CommandStatus protected: // shouldn't construct a CommandStatus (use a derived class) CommandStatus() {} + public: virtual ~CommandStatus() {} void toStream(std::ostream& out, @@ -196,7 +197,7 @@ class CVC4_PUBLIC Command typedef CommandPrintSuccess printsuccess; Command(); - Command(api::Solver* solver); + Command(const api::Solver* solver); Command(const Command& cmd); virtual ~Command(); @@ -273,7 +274,7 @@ class CVC4_PUBLIC Command }; /* class Command::ExportTransformer */ /** The solver instance that this command is associated with. */ - api::Solver* d_solver; + const api::Solver* d_solver; /** * This field contains a command status if the command has been @@ -290,7 +291,7 @@ class CVC4_PUBLIC Command * successful execution. */ bool d_muted; -}; /* class Command */ +}; /* class Command */ /** * EmptyCommands are the residue of a command after the parser handles @@ -507,12 +508,12 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand class CVC4_PUBLIC DefineFunctionRecCommand : public Command { public: - DefineFunctionRecCommand(api::Solver* solver, + DefineFunctionRecCommand(const api::Solver* solver, api::Term func, const std::vector& formals, api::Term formula, bool global); - DefineFunctionRecCommand(api::Solver* solver, + DefineFunctionRecCommand(const api::Solver* solver, const std::vector& funcs, const std::vector >& formals, const std::vector& formula, @@ -715,20 +716,23 @@ class CVC4_PUBLIC DeclareSygusFunctionCommand class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand { public: - SynthFunCommand(const std::string& id, - Expr func, - Type sygusType, + SynthFunCommand(const api::Solver* solver, + const std::string& id, + api::Term fun, + const std::vector& vars, + api::Sort sort, bool isInv, - const std::vector& vars); - SynthFunCommand(const std::string& id, Expr func, Type sygusType, bool isInv); + api::Grammar* g); /** returns the function-to-synthesize */ - Expr getFunction() const; + api::Term getFunction() const; /** returns the input variables of the function-to-synthesize */ - const std::vector& getVars() const; - /** returns the sygus type of the function-to-synthesize */ - Type getSygusType() const; + const std::vector& getVars() const; + /** returns the sygus sort of the function-to-synthesize */ + api::Sort getSort() const; /** returns whether the function-to-synthesize should be an invariant */ bool isInv() const; + /** Get the sygus grammar given for the synth fun command */ + const api::Grammar* getGrammar() const; /** invokes this command * @@ -746,17 +750,15 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand protected: /** the function-to-synthesize */ - Expr d_func; - /** sygus type of the function-to-synthesize - * - * If this type is a "sygus datatype" then it encodes a grammar for the - * possible varlues of the function-to-sytnhesize - */ - Type d_sygusType; + api::Term d_fun; + /** the input variables of the function-to-synthesize */ + std::vector d_vars; + /** sort of the function-to-synthesize */ + api::Sort d_sort; /** whether the function-to-synthesize should be an invariant */ bool d_isInv; - /** the input variables of the function-to-synthesize */ - std::vector d_vars; + /** optional grammar for the possible values of the function-to-sytnhesize */ + api::Grammar* d_grammar; }; /** Declares a sygus constraint */ @@ -1039,7 +1041,7 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command SmtEngine* d_smtEngine; }; /* class GetSynthSolutionCommand */ -/** The command (get-interpol s B) +/** The command (get-interpol s B (G)?) * * This command asks for an interpolant from the current set of assertions and * conjecture (goal) B. @@ -1051,19 +1053,19 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command class CVC4_PUBLIC GetInterpolCommand : public Command { public: - GetInterpolCommand(api::Solver* solver, + GetInterpolCommand(const api::Solver* solver, const std::string& name, api::Term conj); - /** The argument gtype is the grammar of the interpolation query */ - GetInterpolCommand(api::Solver* solver, + /** The argument g is the grammar of the interpolation query */ + GetInterpolCommand(const api::Solver* solver, const std::string& name, api::Term conj, - const Type& gtype); + api::Grammar* g); /** Get the conjecture of the interpolation query */ api::Term getConjecture() const; - /** Get the grammar sygus datatype type given for the interpolation query */ - Type getGrammarType() const; + /** Get the sygus grammar given for the interpolation query */ + const api::Grammar* getGrammar() const; /** Get the result of the query, which is the solution to the interpolation * query. */ api::Term getResult() const; @@ -1080,11 +1082,8 @@ class CVC4_PUBLIC GetInterpolCommand : public Command std::string d_name; /** The conjecture of the interpolation query */ api::Term d_conj; - /** - * The (optional) grammar of the interpolation query, expressed as a sygus - * datatype type. - */ - Type d_sygus_grammar_type; + /** The (optional) grammar of the interpolation query */ + api::Grammar* d_sygus_grammar; /** the return status of the command */ bool d_resultStatus; /** the return expression of the command */ @@ -1100,25 +1099,29 @@ class CVC4_PUBLIC GetInterpolCommand : public Command * find a predicate P, then the output response of this command is: * (define-fun s () Bool P) * - * A grammar type G can be optionally provided to indicate the syntactic - * restrictions on the possible solutions returned. + * A grammar G can be optionally provided to indicate the syntactic restrictions + * on the possible solutions returned. */ class CVC4_PUBLIC GetAbductCommand : public Command { public: - GetAbductCommand(); - GetAbductCommand(const std::string& name, Expr conj); - GetAbductCommand(const std::string& name, Expr conj, const Type& gtype); + GetAbductCommand(const api::Solver* solver, + const std::string& name, + api::Term conj); + GetAbductCommand(const api::Solver* solver, + const std::string& name, + api::Term conj, + api::Grammar* g); /** Get the conjecture of the abduction query */ - Expr getConjecture() const; - /** Get the grammar type given for the abduction query */ - Type getGrammarType() const; + api::Term getConjecture() const; + /** Get the grammar given for the abduction query */ + const api::Grammar* getGrammar() const; /** Get the name of the abduction predicate for the abduction query */ std::string getAbductName() const; /** Get the result of the query, which is the solution to the abduction query. */ - Expr getResult() const; + api::Term getResult() const; void invoke(SmtEngine* smtEngine) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; @@ -1131,16 +1134,13 @@ class CVC4_PUBLIC GetAbductCommand : public Command /** The name of the abduction predicate */ std::string d_name; /** The conjecture of the abduction query */ - Expr d_conj; - /** - * The (optional) grammar of the abduction query, expressed as a sygus - * datatype type. - */ - Type d_sygus_grammar_type; + api::Term d_conj; + /** The (optional) grammar of the abduction query */ + api::Grammar* d_sygus_grammar; /** the return status of the command */ bool d_resultStatus; /** the return expression of the command */ - Expr d_result; + api::Term d_result; }; /* class GetAbductCommand */ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command @@ -1177,6 +1177,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; + protected: std::vector d_result; }; /* class GetUnsatAssumptionsCommand */ @@ -1454,6 +1455,6 @@ class CVC4_PUBLIC DeclarationSequence : public CommandSequence { }; -} /* CVC4 namespace */ +} // namespace CVC4 #endif /* CVC4__COMMAND_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6d1e7ffbc..91ff522b5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1604,7 +1604,9 @@ void SmtEngine::declareSynthFun(const std::string& id, setUserAttribute("sygus-synth-grammar", func, attr_value, ""); } Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n"; - Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars); + // dumping SynthFunCommand from smt-engine is currently broken (please take at + // CVC4/cvc4-projects#211) + // Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars); // sygus conjecture is now stale setSygusConjectureStale(); } -- 2.30.2