From: Andrew Reynolds Date: Mon, 4 Nov 2019 18:23:34 +0000 (-0600) Subject: Make getSynthSolution return a Bool (#3306) X-Git-Tag: cvc5-1.0.0~3861 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9a2913c2f1a22ed43ed772467ec42ba2262bee17;p=cvc5.git Make getSynthSolution return a Bool (#3306) --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b934617de..6a60c45da 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3839,12 +3839,6 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, checkUnsatCore(); } } - // Check that synthesis solutions satisfy the conjecture - if (options::checkSynthSol() - && r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - checkSynthSolution(); - } return r; } catch (UnsafeInterruptException& e) { @@ -4062,62 +4056,70 @@ Result SmtEngine::checkSynth() throw ModalException( "Cannot make check-synth commands when incremental solving is enabled"); } - - if (!d_private->d_sygusConjectureStale) + Expr query; + if (d_private->d_sygusConjectureStale) { - // do not need to reconstruct, we're done - return checkSatisfiability(Expr(), true, false); - } - - // build synthesis conjecture from asserted constraints and declared - // variables/functions - Node sygusVar = - d_nodeManager->mkSkolem("sygus", d_nodeManager->booleanType()); - Node inst_attr = d_nodeManager->mkNode(kind::INST_ATTRIBUTE, sygusVar); - Node sygusAttr = d_nodeManager->mkNode(kind::INST_PATTERN_LIST, inst_attr); - std::vector bodyv; - Trace("smt") << "Sygus : Constructing sygus constraint...\n"; - unsigned n_constraints = d_private->d_sygusConstraints.size(); - Node body = n_constraints == 0 - ? d_nodeManager->mkConst(true) - : (n_constraints == 1 - ? d_private->d_sygusConstraints[0] - : d_nodeManager->mkNode( + // build synthesis conjecture from asserted constraints and declared + // variables/functions + Node sygusVar = + d_nodeManager->mkSkolem("sygus", d_nodeManager->booleanType()); + Node inst_attr = d_nodeManager->mkNode(kind::INST_ATTRIBUTE, sygusVar); + Node sygusAttr = d_nodeManager->mkNode(kind::INST_PATTERN_LIST, inst_attr); + std::vector bodyv; + Trace("smt") << "Sygus : Constructing sygus constraint...\n"; + unsigned n_constraints = d_private->d_sygusConstraints.size(); + Node body = n_constraints == 0 + ? d_nodeManager->mkConst(true) + : (n_constraints == 1 + ? d_private->d_sygusConstraints[0] + : d_nodeManager->mkNode( kind::AND, d_private->d_sygusConstraints)); - body = body.notNode(); - Trace("smt") << "...constructed sygus constraint " << body << std::endl; - if (!d_private->d_sygusVars.empty()) - { - Node boundVars = - d_nodeManager->mkNode(kind::BOUND_VAR_LIST, d_private->d_sygusVars); - body = d_nodeManager->mkNode(kind::EXISTS, boundVars, body); - Trace("smt") << "...constructed exists " << body << std::endl; - } - if (!d_private->d_sygusFunSymbols.empty()) - { - Node boundVars = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, - d_private->d_sygusFunSymbols); - body = d_nodeManager->mkNode(kind::FORALL, boundVars, body, sygusAttr); - } - Trace("smt") << "...constructed forall " << body << std::endl; + body = body.notNode(); + Trace("smt") << "...constructed sygus constraint " << body << std::endl; + if (!d_private->d_sygusVars.empty()) + { + Node boundVars = + d_nodeManager->mkNode(kind::BOUND_VAR_LIST, d_private->d_sygusVars); + body = d_nodeManager->mkNode(kind::EXISTS, boundVars, body); + Trace("smt") << "...constructed exists " << body << std::endl; + } + if (!d_private->d_sygusFunSymbols.empty()) + { + Node boundVars = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, + d_private->d_sygusFunSymbols); + body = d_nodeManager->mkNode(kind::FORALL, boundVars, body, sygusAttr); + } + Trace("smt") << "...constructed forall " << body << std::endl; - // set attribute for synthesis conjecture - setUserAttribute("sygus", sygusVar.toExpr(), {}, ""); + // set attribute for synthesis conjecture + setUserAttribute("sygus", sygusVar.toExpr(), {}, ""); - Trace("smt") << "Check synthesis conjecture: " << body << std::endl; + Trace("smt") << "Check synthesis conjecture: " << body << std::endl; - d_private->d_sygusConjectureStale = false; + d_private->d_sygusConjectureStale = false; - if (options::incrementalSolving()) - { - // we push a context so that this conjecture is removed if we modify it - // later - internalPush(); - assertFormula(body.toExpr(), true); - return checkSatisfiability(body.toExpr(), true, false); + if (options::incrementalSolving()) + { + // we push a context so that this conjecture is removed if we modify it + // later + internalPush(); + assertFormula(body.toExpr(), true); + } + else + { + query = body.toExpr(); + } } - return checkSatisfiability(body.toExpr(), true, false); + Result r = checkSatisfiability(query, true, false); + + // Check that synthesis solutions satisfy the conjecture + if (options::checkSynthSol() + && r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + checkSynthSolution(); + } + return r; } /* @@ -4820,10 +4822,14 @@ void SmtEngine::checkSynthSolution() Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl; map sol_map; /* Get solutions and build auxiliary vectors for substituting */ - d_theoryEngine->getSynthSolutions(sol_map); + if (!d_theoryEngine->getSynthSolutions(sol_map)) + { + InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!"; + return; + } if (sol_map.empty()) { - Trace("check-synth-sol") << "No solution to check!\n"; + InternalError() << "SmtEngine::checkSynthSolution(): Got empty solution!"; return; } Trace("check-synth-sol") << "Got solution map:\n"; @@ -5049,17 +5055,21 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { } } -void SmtEngine::getSynthSolutions(std::map& sol_map) +bool SmtEngine::getSynthSolutions(std::map& sol_map) { SmtScope smts(this); finalOptionsAreSet(); map sol_mapn; Assert(d_theoryEngine != nullptr); - d_theoryEngine->getSynthSolutions(sol_mapn); + if (!d_theoryEngine->getSynthSolutions(sol_mapn)) + { + return false; + } for (std::pair& s : sol_mapn) { sol_map[s.first.toExpr()] = s.second.toExpr(); } + return true; } Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 4f18546ad..d99606126 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -510,7 +510,10 @@ class CVC4_PUBLIC SmtEngine /** * Get synth solution. * - * This function adds entries to sol_map that map functions-to-synthesize with + * This method returns true if we are in a state immediately preceeded by + * a successful call to checkSynth. + * + * This method adds entries to sol_map that map functions-to-synthesize with * their solutions, for all active conjectures. This should be called * immediately after the solver answers unsat for sygus input. * @@ -521,7 +524,7 @@ class CVC4_PUBLIC SmtEngine * forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn ) * is a valid formula. */ - void getSynthSolutions(std::map& sol_map); + bool getSynthSolutions(std::map& sol_map); /** * Do quantifier elimination. diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 7f48d30d8..d8c69edac 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -47,7 +47,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p) : d_qe(qe), d_parent(p), d_tds(qe->getTermDatabaseSygus()), - d_hasSolution(false, qe->getUserContext()), + d_hasSolution(false), d_ceg_si(new CegSingleInv(qe, this)), d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), @@ -300,6 +300,7 @@ bool SynthConjecture::doCheck(std::vector& lems) return true; } Assert(d_master != nullptr); + Assert(!d_hasSolution); // get the list of terms that the master strategy is interested in std::vector terms; @@ -486,6 +487,7 @@ bool SynthConjecture::doCheck(std::vector& lems) lem = getStreamGuardedLemma(lem); lems.push_back(lem); recordInstantiation(candidate_values); + d_hasSolution = true; return true; } Assert(!d_set_ce_sk_vars); @@ -607,14 +609,16 @@ bool SynthConjecture::doCheck(std::vector& lems) } if (success) { + d_hasSolution = true; if (options::sygusStream()) { // if we were successful, we immediately print the current solution. // this saves us from introducing a verification lemma and a new guard. printAndContinueStream(terms, candidate_values); + // streaming means now we immediately are looking for a new solution + d_hasSolution = false; return false; } - d_hasSolution = true; } lem = getStreamGuardedLemma(lem); lems.push_back(lem); @@ -1140,14 +1144,14 @@ void SynthConjecture::printSynthSolution(std::ostream& out) } } -void SynthConjecture::getSynthSolutions(std::map& sol_map) +bool SynthConjecture::getSynthSolutions(std::map& sol_map) { NodeManager* nm = NodeManager::currentNM(); std::vector sols; std::vector statuses; if (!getSynthSolutionsInternal(sols, statuses)) { - return; + return false; } for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { @@ -1180,11 +1184,16 @@ void SynthConjecture::getSynthSolutions(std::map& sol_map) // store in map sol_map[fvar] = bsol; } + return true; } bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, std::vector& statuses) { + if (!d_hasSolution) + { + return false; + } for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { Node prog = d_embed_quant[0][i]; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 8ae30f636..a86ff6f75 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -113,13 +113,16 @@ class SynthConjecture void printSynthSolution(std::ostream& out); /** get synth solutions * - * This returns a map from function-to-synthesize variables to their - * builtin solution, which has the same type. For example, for synthesis + * This method returns true if this class has a solution available to the + * conjecture that it was assigned. + * + * This method adds entries to sol_map that map functions-to-synthesize to + * their builtin solution, which has the same type. For example, for synthesis * conjecture exists f. forall x. f( x )>x, this function may return the map * containing the entry: * f -> (lambda x. x+1) */ - void getSynthSolutions(std::map& sol_map); + bool getSynthSolutions(std::map& sol_map); /** * The feasible guard whose semantics are "this conjecture is feasiable". * This is "G" in Figure 3 of Reynolds et al CAV 2015. @@ -174,10 +177,10 @@ class SynthConjecture /** The feasible guard. */ Node d_feasible_guard; /** - * Do we have a solution in this user context? This is user-context dependent - * to enable use cases of sygus in incremental mode. + * Do we have a solution in this solve context? This flag is reset to false + * on every call to presolve. */ - context::CDO d_hasSolution; + bool d_hasSolution; /** the decision strategy for the feasible guard */ std::unique_ptr d_feasible_strategy; /** single invocation utility */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index d13bd2dcf..73105af6f 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -41,6 +41,17 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) } SynthEngine::~SynthEngine() {} + +void SynthEngine::presolve() +{ + Trace("cegqi-engine") << "SynthEngine::presolve" << std::endl; + for (unsigned i = 0, size = d_conjs.size(); i < size; i++) + { + d_conjs[i]->presolve(); + } + Trace("cegqi-engine") << "SynthEngine::presolve finished" << std::endl; +} + bool SynthEngine::needsCheck(Theory::Effort e) { return e >= Theory::EFFORT_LAST_CALL; @@ -130,7 +141,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) void SynthEngine::assignConjecture(Node q) { - Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl; + Trace("cegqi-engine") << "SynthEngine::assignConjecture " << q << std::endl; if (options::sygusQePreproc()) { // the following does quantifier elimination as a preprocess step @@ -376,15 +387,22 @@ void SynthEngine::printSynthSolution(std::ostream& out) } } -void SynthEngine::getSynthSolutions(std::map& sol_map) +bool SynthEngine::getSynthSolutions(std::map& sol_map) { + bool ret = true; for (unsigned i = 0, size = d_conjs.size(); i < size; i++) { if (d_conjs[i]->isAssigned()) { - d_conjs[i]->getSynthSolutions(sol_map); + if (!d_conjs[i]->getSynthSolutions(sol_map)) + { + // if one conjecture fails, we fail overall + ret = false; + break; + } } } + return ret; } void SynthEngine::preregisterAssertion(Node n) diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index e099657ad..b5880b0c1 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -60,8 +60,15 @@ class SynthEngine : public QuantifiersModule public: SynthEngine(QuantifiersEngine* qe, context::Context* c); ~SynthEngine(); - + /** presolve + * + * Called at the beginning of each call to solve a synthesis problem, which + * may be e.g. a check-synth or get-abduct call. + */ + void presolve() override; + /** needs check, return true if e is last call */ bool needsCheck(Theory::Effort e) override; + /** always needs model at effort QEFFORT_MODEL */ QEffort needsModel(Theory::Effort e) override; /* Call during quantifier engine's check */ void check(Theory::Effort e, QEffort quant_e) override; @@ -81,7 +88,7 @@ class SynthEngine : public QuantifiersModule * For details on what is added to sol_map, see * SynthConjecture::getSynthSolutions. */ - void getSynthSolutions(std::map& sol_map); + bool getSynthSolutions(std::map& sol_map); /** preregister assertion (before rewrite) * * The purpose of this method is to inform the solution reconstruction diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 686843189..dfda79aec 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1294,9 +1294,9 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ return ret; } -void QuantifiersEngine::getSynthSolutions(std::map& sol_map) +bool QuantifiersEngine::getSynthSolutions(std::map& sol_map) { - d_private->d_synth_e->getSynthSolutions(sol_map); + return d_private->d_synth_e->getSynthSolutions(sol_map); } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 323158404..f84b59761 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -256,14 +256,19 @@ public: /** get synth solutions * - * This function adds entries to sol_map that map functions-to-synthesize with + * This method returns true if there is a synthesis solution available. This + * is the case if the last call to check satisfiability originated in a + * check-synth call, and the synthesis engine module of this class + * successfully found a solution for all active synthesis conjectures. + * + * This method adds entries to sol_map that map functions-to-synthesize with * their solutions, for all active conjectures. This should be called * immediately after the solver answers unsat for sygus input. * * For details on what is added to sol_map, see - * CegConjecture::getSynthSolutions. + * SynthConjecture::getSynthSolutions. */ - void getSynthSolutions(std::map& sol_map); + bool getSynthSolutions(std::map& sol_map); //----------end user interface for instantiations diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0adb592f2..d73babdc0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -944,16 +944,14 @@ TheoryModel* TheoryEngine::getBuiltModel() return d_curr_model; } -void TheoryEngine::getSynthSolutions(std::map& sol_map) +bool TheoryEngine::getSynthSolutions(std::map& sol_map) { if (d_quantEngine) { - d_quantEngine->getSynthSolutions(sol_map); - } - else - { - Assert(false); + return d_quantEngine->getSynthSolutions(sol_map); } + // we are not in a quantified logic, there is no synthesis solution + return false; } bool TheoryEngine::presolve() { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index bf3e394f1..fc31572ec 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -767,14 +767,19 @@ public: /** get synth solutions * - * This function adds entries to sol_map that map functions-to-synthesize with + * This method returns true if there is a synthesis solution available. This + * is the case if the last call to check satisfiability originated in a + * check-synth call, and the synthesis solver successfully found a solution + * for all active synthesis conjectures. + * + * This method adds entries to sol_map that map functions-to-synthesize with * their solutions, for all active conjectures. This should be called * immediately after the solver answers unsat for sygus input. * * For details on what is added to sol_map, see - * CegConjecture::getSynthSolutions. + * SynthConjecture::getSynthSolutions. */ - void getSynthSolutions(std::map& sol_map); + bool getSynthSolutions(std::map& sol_map); /** * Get the model builder diff --git a/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy index e994c2a5b..efec0e0e7 100644 --- a/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy +++ b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status -; COMMAND-LINE: --sygus-out=status --cegis-sample=trust +; COMMAND-LINE: --sygus-out=status --cegis-sample=trust --no-check-synth-sol (set-logic BV) ; we test --cegis-sample=trust since we can exhaustively sample BV4