From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 27 Oct 2020 18:19:11 +0000 (-0500) Subject: Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334) X-Git-Tag: cvc5-1.0.0~2656 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=70d6e3c33571807b7bb94bf4f462de4fdf7a369c;p=cvc5.git Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334) This PR is part of migrating commands. DeclareSygusVarCommand and SynthFunCommand now call public API function instead of their corresponding SmtEngine functions. Those two commands don't fully initialize the solver anymore. Some operations in SygusInterpol::solveInterpolation, which creates an interpolation sub-solver, depend on the solver being fully initialized and were affected by this change. Those operations are now executed by the main solver instead of the sub-solver, which is not fully initialized by the time they are needed. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index bda88c539..3cfeaf6cd 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -5591,9 +5591,6 @@ Term Solver::synthFunHelper(const std::string& symbol, CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(sort); - CVC4_API_ARG_CHECK_EXPECTED(sort.d_type->isFirstClass(), sort) - << "first-class codomain sort for function"; - std::vector varTypes; for (size_t i = 0, n = boundVars.size(); i < n; ++i) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 232723fc0..7c1c5dc3e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -537,12 +537,12 @@ command [std::unique_ptr* cmd] sygusCommand returns [std::unique_ptr cmd] @declarations { - CVC4::api::Term expr, expr2; + CVC4::api::Term expr, expr2, fun; CVC4::api::Sort t, range; std::vector names; std::vector > sortedVarNames; - std::unique_ptr synthFunFactory; - std::string name, fun; + std::vector sygusVars; + std::string name; bool isInv; CVC4::api::Grammar* grammar = nullptr; } @@ -552,7 +552,8 @@ sygusCommand returns [std::unique_ptr cmd] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] { - api::Term var = PARSER_STATE->bindBoundVar(name, t); + api::Term var = SOLVER->mkSygusVar(t, name); + PARSER_STATE->defineVar(name, var); cmd.reset(new DeclareSygusVarCommand(name, var, t)); } | /* synth-fun */ @@ -560,22 +561,36 @@ sygusCommand returns [std::unique_ptr cmd] | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); } ) { PARSER_STATE->checkThatLogicIsSet(); } - symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK ( sortSymbol[range,CHECK_DECLARED] )? { - synthFunFactory.reset(new Smt2::SynthFunFactory( - PARSER_STATE, fun, isInv, range, sortedVarNames)); + PARSER_STATE->pushScope(true); + sygusVars = PARSER_STATE->bindBoundVars(sortedVarNames); } ( // optionally, read the sygus grammar // // `grammar` specifies the required grammar for the function to // synthesize, expressed as a type - sygusGrammar[grammar, synthFunFactory->getSygusVars(), fun] + sygusGrammar[grammar, sygusVars, name] )? { - cmd = synthFunFactory->mkCommand(grammar); + Debug("parser-sygus") << "Define synth fun : " << name << std::endl; + + fun = isInv ? (grammar == nullptr + ? SOLVER->synthInv(name, sygusVars) + : SOLVER->synthInv(name, sygusVars, *grammar)) + : (grammar == nullptr + ? SOLVER->synthFun(name, sygusVars, range) + : SOLVER->synthFun(name, sygusVars, range, *grammar)); + + Debug("parser-sygus") << "...read synth fun " << name << std::endl; + PARSER_STATE->popScope(); + // we do not allow overloading for synth fun + PARSER_STATE->defineVar(name, fun); + cmd = std::unique_ptr( + new SynthFunCommand(name, fun, sygusVars, range, isInv, grammar)); } | /* constraint */ CONSTRAINT_TOK { diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 81a4bd4a6..629164593 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -482,50 +482,6 @@ void Smt2::resetAssertions() { pushScope(true); } -Smt2::SynthFunFactory::SynthFunFactory( - Smt2* smt2, - const std::string& id, - bool isInv, - api::Sort range, - std::vector>& sortedVarNames) - : d_smt2(smt2), d_id(id), d_sort(range), d_isInv(isInv) -{ - if (range.isNull()) - { - smt2->parseError("Must supply return type for synth-fun."); - } - if (range.isFunction()) - { - smt2->parseError("Cannot use synth-fun with function return type."); - } - - std::vector varSorts; - for (const std::pair& p : sortedVarNames) - { - varSorts.push_back(p.second); - } - - api::Sort funSort = varSorts.empty() - ? range - : d_smt2->d_solver->mkFunctionSort(varSorts, range); - - // we do not allow overloading for synth fun - 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); -} - -std::unique_ptr Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar) -{ - Debug("parser-sygus") << "...read synth fun " << d_id << std::endl; - d_smt2->popScope(); - return std::unique_ptr( - new SynthFunCommand(d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar)); -} - std::unique_ptr Smt2::invConstraint( const std::vector& names) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 5fcf49637..1aa0ebac7 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -194,49 +194,6 @@ class Smt2 : public Parser void resetAssertions(); - /** - * Class for creating instances of `SynthFunCommand`s. Creating an instance - * of this class pushes the scope, destroying it pops the scope. - */ - class SynthFunFactory - { - public: - /** - * Creates an instance of `SynthFunFactory`. - * - * @param smt2 Pointer to the parser state - * @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 - * @param sortedVarNames The parameters of the function-to-synthesize - */ - SynthFunFactory( - Smt2* smt2, - const std::string& id, - bool isInv, - api::Sort range, - std::vector>& sortedVarNames); - - const std::vector& getSygusVars() const { return d_sygusVars; } - - /** - * Create an instance of `SynthFunCommand`. - * - * @param grammar Optional grammar associated with the synth-fun command - * @return The instance of `SynthFunCommand` - */ - std::unique_ptr mkCommand(api::Grammar* grammar); - - private: - Smt2* d_smt2; - std::string d_id; - api::Term d_fun; - api::Sort d_sort; - bool d_isInv; - std::vector d_sygusVars; - }; - /** * Creates a command that adds an invariant constraint. * diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 9c45c0b19..eb03edf4f 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -581,16 +581,7 @@ api::Sort DeclareSygusVarCommand::getSort() const { return d_sort; } void DeclareSygusVarCommand::invoke(api::Solver* solver) { - try - { - solver->getSmtEngine()->declareSygusVar( - d_symbol, d_var.getNode(), TypeNode::fromType(d_sort.getType())); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } + d_commandStatus = CommandSuccess::instance(); } Command* DeclareSygusVarCommand::clone() const @@ -646,27 +637,7 @@ const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; } void SynthFunCommand::invoke(api::Solver* solver) { - try - { - std::vector vns; - for (const api::Term& t : d_vars) - { - vns.push_back(Node::fromExpr(t.getExpr())); - } - solver->getSmtEngine()->declareSynthFun( - d_symbol, - Node::fromExpr(d_fun.getExpr()), - TypeNode::fromType(d_grammar == nullptr - ? d_sort.getType() - : d_grammar->resolve().getType()), - d_isInv, - vns); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } + d_commandStatus = CommandSuccess::instance(); } Command* SynthFunCommand::clone() const diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f345bee2e..d0906ce98 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1065,7 +1065,6 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type) { SmtScope smts(this); - finishInit(); d_sygusSolver->declareSygusVar(id, var, type); if (Dump.isOn("raw-benchmark")) { @@ -1082,7 +1081,6 @@ void SmtEngine::declareSynthFun(const std::string& id, const std::vector& vars) { SmtScope smts(this); - finishInit(); d_state->doPendingPops(); d_sygusSolver->declareSynthFun(id, func, sygusType, isInv, vars); diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index e4e7a02c7..d5ab0e51f 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -319,6 +319,18 @@ bool SygusInterpol::solveInterpolation(const std::string& name, const TypeNode& itpGType, Node& interpol) { + // Some instructions in setSynthGrammar and mkSygusConjecture need a fully + // initialized solver to work properly. Notice, however, that the sub-solver + // created below is not fully initialized by the time those two methods are + // needed. Therefore, we call them while the current parent solver is in scope + // (i.e., before creating the sub-solver). + collectSymbols(axioms, conj); + createVariables(itpGType.isNull()); + TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj); + + Node itp = mkPredicate(name); + mkSygusConjecture(itp, axioms, conj); + std::unique_ptr subSolver; initializeSubsolver(subSolver); // get the logic @@ -327,17 +339,12 @@ bool SygusInterpol::solveInterpolation(const std::string& name, l.enableSygus(); subSolver->setLogic(l); - collectSymbols(axioms, conj); - createVariables(itpGType.isNull()); for (Node var : d_vars) { subSolver->declareSygusVar(name, var, var.getType()); } std::vector vars_empty; - TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj); - Node itp = mkPredicate(name); subSolver->declareSynthFun(name, itp, grammarType, false, vars_empty); - mkSygusConjecture(itp, axioms, conj); Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : " << d_sygusConj << ", solving for " << d_sygusConj[0][0] << std::endl; diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index aa4289ef3..8b8c6dd58 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -2268,7 +2268,6 @@ void SolverBlack::testSynthFun() Sort null = d_solver->getNullSort(); Sort boolean = d_solver->getBooleanSort(); Sort integer = d_solver->getIntegerSort(); - Sort boolToBool = d_solver->mkFunctionSort(boolean, boolean); Term nullTerm; Term x = d_solver->mkVar(boolean); @@ -2289,7 +2288,6 @@ void SolverBlack::testSynthFun() TS_ASSERT_THROWS(d_solver->synthFun("f3", {nullTerm}, boolean), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->synthFun("f4", {}, null), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->synthFun("f5", {}, boolToBool), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->synthFun("f6", {x}, boolean, g2), CVC4ApiException&); Solver slv;