From 4f61c76d8170e97c431ea9529f493cb42a9a3e5f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Dec 2021 09:46:49 -0600 Subject: [PATCH] Towards support for incremental sygus (#7736) This makes several key changes to smt::SygusSolver in preparation for incremental mode. The key idea is to use a subsolver that: may take multiple check-sat commands for an encoded synthesis conjecture does not push/pop is reconstructed when the SyGuS conjecture becomes stale. This is motivated by 2 use cases of incremental SyGuS: Where constraints are push/pop, in which case we should start from scratch, since the SyGuS solver uses symmetry breaking techniques that become unsound when new constraints are added. Where multiple solutions are needed for the same set of constraints, in which the state of the subsolver should be preserved. This functionality is still guarded by an exception. A follow up PR will make several further changes to allow for the above use cases. --- src/preprocessing/passes/sygus_inference.cpp | 3 +- src/smt/abduction_solver.cpp | 4 +- src/smt/set_defaults.cpp | 2 +- src/smt/solver_engine.cpp | 7 + src/smt/solver_engine.h | 10 + src/smt/sygus_solver.cpp | 256 ++++++++++--------- src/smt/sygus_solver.h | 93 +++++-- 7 files changed, 230 insertions(+), 145 deletions(-) diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 3da75beb2..7ebb3ab80 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -308,7 +308,8 @@ bool SygusInference::solveSygus(const std::vector& assertions, } // get the synthesis solutions std::map synth_sols; - rrSygus->getSynthSolutions(synth_sols); + bool sinferSol = rrSygus->getSubsolverSynthSolutions(synth_sols); + AlwaysAssert(sinferSol) << "Failed to get solutions for sygus-inference"; std::vector final_ff; std::vector final_ff_sol; diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 063ffe09b..a5a180ffb 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -98,7 +98,9 @@ bool AbductionSolver::getAbductInternal(const std::vector& axioms, { // get the synthesis solution std::map sols; - d_subsolver->getSynthSolutions(sols); + // use the "getSubsolverSynthSolutions" interface, since we asserted the + // internal form of the SyGuS conjecture and used check-sat. + d_subsolver->getSubsolverSynthSolutions(sols); Assert(sols.size() == 1); std::map::iterator its = sols.find(d_sssf); if (its != sols.end()) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index b2fe2b5d6..aeb732dd5 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -373,7 +373,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const || opts.smt.produceInterpols != options::ProduceInterpols::NONE || opts.smt.modelCoresMode != options::ModelCoresMode::NONE || opts.smt.blockModelsMode != options::BlockModelsMode::NONE - || opts.smt.produceProofs) + || opts.smt.produceProofs || isSygus(opts)) && !opts.smt.produceAssertions) { verbose(1) << "SolverEngine: turning on produce-assertions to support " diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 52fdaf74b..be53bad80 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1601,6 +1601,13 @@ bool SolverEngine::getSynthSolutions(std::map& solMap) return d_sygusSolver->getSynthSolutions(solMap); } +bool SolverEngine::getSubsolverSynthSolutions(std::map& solMap) +{ + SolverEngineScope smts(this); + finishInit(); + return d_sygusSolver->getSubsolverSynthSolutions(solMap); +} + Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict) { SolverEngineScope smts(this); diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index d7df78f08..1e710f213 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -563,6 +563,16 @@ class CVC5_EXPORT SolverEngine * is a valid formula. */ bool getSynthSolutions(std::map& solMap); + /** + * Same as above, but used for getting synthesis solutions from a "subsolver" + * that has been initialized to assert the synthesis conjecture as a + * normal assertion. + * + * This method returns true if we are in a state immediately preceded by + * a successful call to checkSat, where this SolverEngine has an asserted + * synthesis conjecture. + */ + bool getSubsolverSynthSolutions(std::map& solMap); /** * Do quantifier elimination. diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 4c8d3e5bd..2e4461c1c 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -42,7 +42,14 @@ namespace cvc5 { namespace smt { SygusSolver::SygusSolver(Env& env, SmtSolver& sms) - : EnvObj(env), d_smtSolver(sms), d_sygusConjectureStale(userContext(), true) + : EnvObj(env), + d_smtSolver(sms), + d_sygusVars(userContext()), + d_sygusConstraints(userContext()), + d_sygusAssumps(userContext()), + d_sygusFunSymbols(userContext()), + d_sygusConjectureStale(userContext(), true), + d_subsolverCd(userContext(), nullptr) { } @@ -84,7 +91,7 @@ void SygusSolver::declareSynthFun(Node fn, } // sygus conjecture is now stale - setSygusConjectureStale(); + d_sygusConjectureStale = true; } void SygusSolver::assertSygusConstraint(Node n, bool isAssume) @@ -101,7 +108,7 @@ void SygusSolver::assertSygusConstraint(Node n, bool isAssume) } // sygus conjecture is now stale - setSygusConjectureStale(); + d_sygusConjectureStale = true; } void SygusSolver::assertSygusInvConstraint(Node inv, @@ -173,7 +180,7 @@ void SygusSolver::assertSygusInvConstraint(Node inv, d_sygusConstraints.push_back(constraint); // sygus conjecture is now stale - setSygusConjectureStale(); + d_sygusConjectureStale = true; } Result SygusSolver::checkSynth(Assertions& as) @@ -185,32 +192,39 @@ Result SygusSolver::checkSynth(Assertions& as) "Cannot make check-synth commands when incremental solving is enabled"); } Trace("smt") << "SygusSolver::checkSynth" << std::endl; - std::vector query; + // if applicable, check if the subsolver is the correct one + if (usingSygusSubsolver() && d_subsolverCd.get() != d_subsolver.get()) + { + // this can occur if we backtrack to a place where we were using a different + // subsolver than the current one. In this case, we should reconstruct + // the subsolver. + d_sygusConjectureStale = true; + } if (d_sygusConjectureStale) { NodeManager* nm = NodeManager::currentNM(); // build synthesis conjecture from asserted constraints and declared // variables/functions Trace("smt") << "Sygus : Constructing sygus constraint...\n"; - Node body = nm->mkAnd(d_sygusConstraints); + Node body = nm->mkAnd(listToVector(d_sygusConstraints)); // note that if there are no constraints, then assumptions are irrelevant if (!d_sygusConstraints.empty() && !d_sygusAssumps.empty()) { - Node bodyAssump = nm->mkAnd(d_sygusAssumps); + Node bodyAssump = nm->mkAnd(listToVector(d_sygusAssumps)); body = nm->mkNode(IMPLIES, bodyAssump, body); } body = body.notNode(); Trace("smt") << "...constructed sygus constraint " << body << std::endl; if (!d_sygusVars.empty()) { - Node boundVars = nm->mkNode(BOUND_VAR_LIST, d_sygusVars); + Node boundVars = nm->mkNode(BOUND_VAR_LIST, listToVector(d_sygusVars)); body = nm->mkNode(EXISTS, boundVars, body); Trace("smt") << "...constructed exists " << body << std::endl; } if (!d_sygusFunSymbols.empty()) { - body = - quantifiers::SygusUtils::mkSygusConjecture(d_sygusFunSymbols, body); + body = quantifiers::SygusUtils::mkSygusConjecture( + listToVector(d_sygusFunSymbols), body); } Trace("smt") << "...constructed forall " << body << std::endl; @@ -218,12 +232,36 @@ Result SygusSolver::checkSynth(Assertions& as) d_sygusConjectureStale = false; - // TODO (project #7): if incremental, we should push a context and assert - query.push_back(body); - } + d_conj = body; + + // if we are using a subsolver, initialize it now + if (usingSygusSubsolver()) + { + // we generate a new solver engine to do the SyGuS query + initializeSygusSubsolver(d_subsolver, as); - Result r = d_smtSolver.checkSatisfiability(as, query, false); + // store the pointer (context-dependent) + d_subsolverCd = d_subsolver.get(); + // also assert the internal SyGuS conjecture + d_subsolver->assertFormula(d_conj); + } + } + else + { + Assert(d_subsolver != nullptr); + } + Result r; + if (usingSygusSubsolver()) + { + r = d_subsolver->checkSat(); + } + else + { + std::vector query; + query.push_back(d_conj); + r = d_smtSolver.checkSatisfiability(as, query, false); + } // Check that synthesis solutions satisfy the conjecture if (options().smt.checkSynthSol && r.asSatisfiabilityResult().isSat() == Result::UNSAT) @@ -233,21 +271,32 @@ Result SygusSolver::checkSynth(Assertions& as) return r; } -bool SygusSolver::getSynthSolutions(std::map& sol_map) +bool SygusSolver::getSynthSolutions(std::map& solMap) { Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl; - std::map> sol_mapn; + if (usingSygusSubsolver()) + { + // use the call to get the synth solutions from the subsolver + return d_subsolver->getSubsolverSynthSolutions(solMap); + } + return getSubsolverSynthSolutions(solMap); +} + +bool SygusSolver::getSubsolverSynthSolutions(std::map& solMap) +{ + Trace("smt") << "SygusSolver::getSubsolverSynthSolutions" << std::endl; + std::map> solMapn; // fail if the theory engine does not have synthesis solutions QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine(); - if (qe == nullptr || !qe->getSynthSolutions(sol_mapn)) + if (qe == nullptr || !qe->getSynthSolutions(solMapn)) { return false; } - for (std::pair>& cs : sol_mapn) + for (std::pair>& cs : solMapn) { for (std::pair& s : cs.second) { - sol_map[s.first] = s.second; + solMap[s.first] = s.second; } } return true; @@ -255,17 +304,14 @@ bool SygusSolver::getSynthSolutions(std::map& sol_map) void SygusSolver::checkSynthSolution(Assertions& as) { - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); if (isVerboseOn(1)) { verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution" << std::endl; } - std::map> sol_map; + std::map sol_map; // Get solutions and build auxiliary vectors for substituting - QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine(); - if (qe == nullptr || !qe->getSynthSolutions(sol_map)) + if (!getSynthSolutions(sol_map)) { InternalError() << "SygusSolver::checkSynthSolution(): No solution to check!"; @@ -279,100 +325,39 @@ void SygusSolver::checkSynthSolution(Assertions& as) Trace("check-synth-sol") << "Got solution map:\n"; // the set of synthesis conjectures in our assertions std::unordered_set conjs; + conjs.insert(d_conj); // For each of the above conjectures, the functions-to-synthesis and their // solutions. This is used as a substitution below. - std::map> fvarMap; - std::map> fsolMap; - for (const std::pair>& cmap : sol_map) + std::vector fvars; + std::vector fsols; + for (const std::pair& pair : sol_map) { - Trace("check-synth-sol") << "For conjecture " << cmap.first << ":\n"; - conjs.insert(cmap.first); - std::vector& fvars = fvarMap[cmap.first]; - std::vector& fsols = fsolMap[cmap.first]; - for (const std::pair& pair : cmap.second) - { - Trace("check-synth-sol") - << " " << pair.first << " --> " << pair.second << "\n"; - fvars.push_back(pair.first); - fsols.push_back(pair.second); - } + Trace("check-synth-sol") + << " " << pair.first << " --> " << pair.second << "\n"; + fvars.push_back(pair.first); + fsols.push_back(pair.second); } + Trace("check-synth-sol") << "Starting new SMT Engine\n"; Trace("check-synth-sol") << "Retrieving assertions\n"; // Build conjecture from original assertions - const context::CDList& alist = as.getAssertionList(); - Assert(options().smt.produceAssertions) - << "Expected produce assertions to be true when checking synthesis " - "solution"; - // auxiliary assertions - std::vector auxAssertions; - // expand definitions cache - std::unordered_map cache; - for (const Node& assertion : alist) - { - if (isVerboseOn(1)) - { - verbose(1) << "SyGuS::checkSynthSolution: checking assertion " - << assertion << std::endl; - } - Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n"; - // Apply any define-funs from the problem. - Node n = d_smtSolver.getPreprocessor()->expandDefinitions(assertion, cache); - if (isVerboseOn(1)) - { - verbose(1) << "SyGuS::checkSynthSolution: -- expands to " << n - << std::endl; - } - Trace("check-synth-sol") << "Expanded assertion " << n << "\n"; - if (conjs.find(n) == conjs.end()) - { - Trace("check-synth-sol") << "It is an auxiliary assertion\n"; - auxAssertions.push_back(n); - } - else - { - Trace("check-synth-sol") << "It is a synthesis conjecture\n"; - } - } // check all conjectures - for (Node conj : conjs) + for (const Node& conj : conjs) { // Start new SMT engine to check solutions std::unique_ptr solChecker; - initializeSubsolver(solChecker, d_env); + initializeSygusSubsolver(solChecker, as); solChecker->getOptions().smt.checkSynthSol = false; solChecker->getOptions().quantifiers.sygusRecFun = false; - // get the solution for this conjecture - std::vector& fvars = fvarMap[conj]; - std::vector& fsols = fsolMap[conj]; + Assert(conj.getKind() == FORALL); + Node conjBody = conj[1]; + // we must expand definitions here, since define-fun may contain the + // function-to-synthesize, which needs to be substituted. + conjBody = d_smtSolver.getPreprocessor()->expandDefinitions(conjBody); // Apply solution map to conjecture body - Node conjBody; - /* Whether property is quantifier free */ - if (conj[1].getKind() != EXISTS) - { - conjBody = conj[1].substitute( - fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); - } - else - { - conjBody = conj[1][1].substitute( - fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); - - /* Skolemize property */ - std::vector vars, skos; - for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j) - { - vars.push_back(conj[1][0][j]); - std::stringstream ss; - ss << "sk_" << j; - skos.push_back(sm->mkDummySkolem(ss.str(), conj[1][0][j].getType())); - Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to " - << skos.back() << "\n"; - } - conjBody = conjBody.substitute( - vars.begin(), vars.end(), skos.begin(), skos.end()); - } + conjBody = conjBody.substitute( + fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); if (isVerboseOn(1)) { @@ -382,17 +367,6 @@ void SygusSolver::checkSynthSolution(Assertions& as) Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody << "\n"; solChecker->assertFormula(conjBody); - // Assert all auxiliary assertions. This may include recursive function - // definitions that were added as assertions to the sygus problem. - for (Node a : auxAssertions) - { - // We require rewriting here, e.g. so that define-fun from the original - // problem are rewritten to true. If this is not the case, then the - // assertions module of the subsolver will complain about assertions - // with free variables. - Node ar = rewrite(a); - solChecker->assertFormula(ar); - } Result r = solChecker->checkSat(); if (isVerboseOn(1)) { @@ -414,15 +388,47 @@ void SygusSolver::checkSynthSolution(Assertions& as) } } -void SygusSolver::setSygusConjectureStale() +void SygusSolver::initializeSygusSubsolver(std::unique_ptr& se, + Assertions& as) { - if (d_sygusConjectureStale) + initializeSubsolver(se, d_env); + // carry the ordinary define-fun definitions + const context::CDList& alistDefs = as.getAssertionListDefinitions(); + std::unordered_set processed; + for (const Node& def : alistDefs) { - // already stale - return; + // only consider define-fun, represented as (= f (lambda ...)). + if (def.getKind() == EQUAL) + { + Assert(def[0].isVar()); + std::vector formals; + Node dbody = def[1]; + if (def[1].getKind() == LAMBDA) + { + formals.insert(formals.end(), def[1][0].begin(), def[1][0].end()); + dbody = dbody[1]; + } + se->defineFunction(def[0], formals, dbody); + processed.insert(def); + } + } + // Also assert auxiliary assertions + const context::CDList& alist = as.getAssertionList(); + for (size_t i = 0, asize = alist.size(); i < asize; ++i) + { + Node a = alist[i]; + // ignore definitions here + if (processed.find(a) == processed.end()) + { + se->assertFormula(a); + } } - d_sygusConjectureStale = true; - // TODO (project #7): if incremental, we should pop a context +} + +bool SygusSolver::usingSygusSubsolver() const +{ + // use SyGuS subsolver if in incremental mode + return options().base.incrementalSolving; } void SygusSolver::expandDefinitionsSygusDt(TypeNode tn) const @@ -467,5 +473,15 @@ void SygusSolver::expandDefinitionsSygusDt(TypeNode tn) const } } +std::vector SygusSolver::listToVector(const NodeList& list) +{ + std::vector vec; + for (const Node& n : list) + { + vec.push_back(n); + } + return vec; +} + } // namespace smt } // namespace cvc5 diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 0c742fbd4..9fe9f7a36 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -18,6 +18,7 @@ #ifndef CVC5__SMT__SYGUS_SOLVER_H #define CVC5__SMT__SYGUS_SOLVER_H +#include "context/cdlist.h" #include "context/cdo.h" #include "expr/node.h" #include "expr/type_node.h" @@ -27,7 +28,7 @@ namespace cvc5 { -class OutputManager; +class SolverEngine; namespace smt { @@ -37,13 +38,28 @@ class SmtSolver; * A solver for sygus queries. * * This class is responsible for responding to check-synth commands. It calls - * check satisfiability using an underlying SmtSolver object. + * check satisfiability using a separate SolverEngine "subsolver". * - * It also maintains a reference to a preprocessor for implementing - * checkSynthSolution. + * This solver operates in two modes. + * + * If in incremental mode, then the "main" SolverEngine for SyGuS inputs only + * maintains a (user-context) dependent state of SyGuS assertions, as well as + * assertions corresponding to (recursive) function definitions. The subsolver + * that solves SyGuS conjectures may be called to checkSat multiple times, + * however, push/pop (which impact SyGuS constraints) impacts only the main + * solver. This means that the conjecture being handled by the subsolver is + * reconstructed when the SyGuS conjecture is updated. The key property that + * this enables is that the subsolver does *not* get calls to push/pop, + * although it may receive multiple check-sat if the sygus functions and + * constraints are not updated between check-sat calls. + * + * If not in incremental mode, then the internal SyGuS conjecture is asserted + * to the "main" SolverEngine. */ class SygusSolver : protected EnvObj { + using NodeList = context::CDList; + public: SygusSolver(Env& env, SmtSolver& sms); ~SygusSolver(); @@ -134,6 +150,16 @@ class SygusSolver : protected EnvObj * is a valid formula. */ bool getSynthSolutions(std::map& sol_map); + /** + * Same as above, but used for getting synthesis solutions from a "subsolver" + * that has been initialized to assert the synthesis conjecture as a + * normal assertion. + * + * This method returns true if we are in a state immediately preceded by + * a successful call to checkSat, where this SolverEngine has an asserted + * synthesis conjecture. + */ + bool getSubsolverSynthSolutions(std::map& solMap); private: /** @@ -145,19 +171,6 @@ class SygusSolver : protected EnvObj * unsatisfiable. If not, then the found solutions are wrong. */ void checkSynthSolution(Assertions& as); - /** - * Set sygus conjecture is stale. The sygus conjecture is stale if either: - * (1) no sygus conjecture has been added as an assertion to this SMT engine, - * (2) there is a sygus conjecture that has been added as an assertion - * internally to this SMT engine, and there have been further calls such that - * the asserted conjecture is no longer up-to-date. - * - * This method should be called when new sygus constraints are asserted and - * when functions-to-synthesize are declared. This function pops a user - * context if we are in incremental mode and the sygus conjecture was - * previously not stale. - */ - void setSygusConjectureStale(); /** * Expand definitions in sygus datatype tn, which ensures that all * sygus constructors that are used to build values of sygus datatype @@ -170,7 +183,19 @@ class SygusSolver : protected EnvObj * expansion. */ void expandDefinitionsSygusDt(TypeNode tn) const; - /** The SMT solver, which is used during checkSynth. */ + /** List to vector helper */ + static std::vector listToVector(const NodeList& list); + /** + * Initialize SyGuS subsolver based on the assertions from the "main" solver. + * This is used for check-synth using a subsolver, and for check-synth-sol. + * This constructs a subsolver se, and makes calls to add all define-fun + * and auxilary assertions. + */ + void initializeSygusSubsolver(std::unique_ptr& se, + Assertions& as); + /** Are we using a subsolver for the SyGuS query? */ + bool usingSygusSubsolver() const; + /** The SMT solver. */ SmtSolver& d_smtSolver; /** * sygus variables declared (from "declare-var" and "declare-fun" commands) @@ -178,17 +203,41 @@ class SygusSolver : protected EnvObj * The SyGuS semantics for declared variables is that they are implicitly * universally quantified in the constraints. */ - std::vector d_sygusVars; + NodeList d_sygusVars; /** sygus constraints */ - std::vector d_sygusConstraints; + NodeList d_sygusConstraints; /** sygus assumptions */ - std::vector d_sygusAssumps; + NodeList d_sygusAssumps; /** functions-to-synthesize */ - std::vector d_sygusFunSymbols; + NodeList d_sygusFunSymbols; + /** The current sygus conjecture */ + Node d_conj; /** * Whether we need to reconstruct the sygus conjecture. + * + * The sygus conjecture is stale if either: + * (1) no sygus conjecture has been added as an assertion to this SMT engine, + * (2) there is a sygus conjecture that has been added as an assertion + * internally to this SMT engine, and there have been further calls such that + * the asserted conjecture is no longer up-to-date. + * + * This flag should be set to true when new sygus constraints are asserted and + * when functions-to-synthesize are declared. */ context::CDO d_sygusConjectureStale; + /** + * The (context-dependent) pointer to the subsolver we have constructed. + * This is used to verify if the current subsolver is current, in case + * user-context dependent pop has a occurred. If this pointer does not match + * d_subsolver, then d_subsolver must be reconstructed in this context. + */ + context::CDO d_subsolverCd; + /** + * The subsolver we are using. This is a separate copy of the SolverEngine + * which has the asserted synthesis conjecture, i.e. a formula returned by + * quantifiers::SygusUtils::mkSygusConjecture. + */ + std::unique_ptr d_subsolver; }; } // namespace smt -- 2.30.2