From 2a888bdb47b18ea29f67659b5d64aad6d8da389b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Nov 2019 17:48:30 -0600 Subject: [PATCH] Make check synth solution robust to auxiliary assertions (#3432) --- src/smt/smt_engine.cpp | 83 +++++++++++++------ .../quantifiers/sygus/synth_conjecture.cpp | 7 +- .../quantifiers/sygus/synth_conjecture.h | 9 +- src/theory/quantifiers/sygus/synth_engine.cpp | 3 +- src/theory/quantifiers/sygus/synth_engine.h | 2 +- src/theory/quantifiers_engine.cpp | 3 +- src/theory/quantifiers_engine.h | 2 +- src/theory/theory_engine.cpp | 3 +- src/theory/theory_engine.h | 2 +- 9 files changed, 76 insertions(+), 38 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6a60c45da..7d28d8b85 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4820,7 +4820,7 @@ void SmtEngine::checkSynthSolution() { NodeManager* nm = NodeManager::currentNM(); Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl; - map sol_map; + std::map> sol_map; /* Get solutions and build auxiliary vectors for substituting */ if (!d_theoryEngine->getSynthSolutions(sol_map)) { @@ -4833,12 +4833,25 @@ void SmtEngine::checkSynthSolution() return; } Trace("check-synth-sol") << "Got solution map:\n"; - std::vector function_vars, function_sols; - for (const auto& pair : sol_map) + // the set of synthesis conjectures in our assertions + std::unordered_set conjs; + // 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) { - Trace("check-synth-sol") << pair.first << " --> " << pair.second << "\n"; - function_vars.push_back(pair.first); - function_sols.push_back(pair.second); + 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") << "Starting new SMT Engine\n"; /* Start new SMT engine to check solutions */ @@ -4853,42 +4866,50 @@ void SmtEngine::checkSynthSolution() Trace("check-synth-sol") << "No assertions to check\n"; return; } + // auxiliary assertions + std::vector auxAssertions; + // expand definitions cache + std::unordered_map cache; for (AssertionList::const_iterator i = d_assertionList->begin(); i != d_assertionList->end(); ++i) { Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i << endl; Trace("check-synth-sol") << "Retrieving assertion " << *i << "\n"; - Node conj = Node::fromExpr(*i); + Node assertion = Node::fromExpr(*i); // Apply any define-funs from the problem. + assertion = d_private->expandDefinitions(assertion, cache); + Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << assertion + << endl; + Trace("check-synth-sol") << "Expanded assertion " << assertion << "\n"; + if (conjs.find(assertion) == conjs.end()) { - unordered_map cache; - conj = d_private->expandDefinitions(conj, cache); + Trace("check-synth-sol") << "It is an auxiliary assertion\n"; + auxAssertions.push_back(assertion); } - Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << conj << endl; - Trace("check-synth-sol") << "Expanded assertion " << conj << "\n"; - if (conj.getKind() != kind::FORALL) + else { - Trace("check-synth-sol") << "Not a checkable assertion.\n"; - continue; + Trace("check-synth-sol") << "It is a synthesis conjecture\n"; } - + } + // check all conjectures + for (const Node& conj : conjs) + { + // get the solution for this conjecture + std::vector& fvars = fvarMap[conj]; + std::vector& fsols = fsolMap[conj]; // Apply solution map to conjecture body Node conjBody; /* Whether property is quantifier free */ if (conj[1].getKind() != kind::EXISTS) { - conjBody = conj[1].substitute(function_vars.begin(), - function_vars.end(), - function_sols.begin(), - function_sols.end()); + conjBody = conj[1].substitute( + fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); } else { - conjBody = conj[1][1].substitute(function_vars.begin(), - function_vars.end(), - function_sols.begin(), - function_sols.end()); + conjBody = conj[1][1].substitute( + fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); /* Skolemize property */ std::vector vars, skos; @@ -4909,6 +4930,12 @@ void SmtEngine::checkSynthSolution() Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody << "\n"; solChecker.assertFormula(conjBody.toExpr()); + // Assert all auxiliary assertions. This may include recursive function + // definitions that were added as assertions to the sygus problem. + for (const Node& a : auxAssertions) + { + solChecker.assertFormula(a.toExpr()); + } Result r = solChecker.checkSat(); Notice() << "SmtEngine::checkSynthSolution(): result is " << r << endl; Trace("check-synth-sol") << "Satsifiability check: " << r << "\n"; @@ -5059,15 +5086,19 @@ bool SmtEngine::getSynthSolutions(std::map& sol_map) { SmtScope smts(this); finalOptionsAreSet(); - map sol_mapn; + std::map> sol_mapn; Assert(d_theoryEngine != nullptr); + // fail if the theory engine does not have synthesis solutions if (!d_theoryEngine->getSynthSolutions(sol_mapn)) { return false; } - for (std::pair& s : sol_mapn) + for (std::pair>& cs : sol_mapn) { - sol_map[s.first.toExpr()] = s.second.toExpr(); + for (std::pair& s : cs.second) + { + sol_map[s.first.toExpr()] = s.second.toExpr(); + } } return true; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index d8c69edac..5edd18464 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1144,7 +1144,8 @@ void SynthConjecture::printSynthSolution(std::ostream& out) } } -bool SynthConjecture::getSynthSolutions(std::map& sol_map) +bool SynthConjecture::getSynthSolutions( + std::map >& sol_map) { NodeManager* nm = NodeManager::currentNM(); std::vector sols; @@ -1153,6 +1154,8 @@ bool SynthConjecture::getSynthSolutions(std::map& sol_map) { return false; } + // we add it to the solution map, indexed by this conjecture + std::map& smc = sol_map[d_quant]; for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { Node sol = sols[i]; @@ -1182,7 +1185,7 @@ bool SynthConjecture::getSynthSolutions(std::map& sol_map) Assert(fvar.getType().isComparableTo(bsol.getType())); } // store in map - sol_map[fvar] = bsol; + smc[fvar] = bsol; } return true; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index a86ff6f75..344f8b460 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -116,13 +116,14 @@ class SynthConjecture * 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 + * Let q be the synthesis conjecture assigned to this class. + * This method adds entries to sol_map[q] 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: + * conjecture exists f. forall x. f( x )>x, this function will update + * sol_map[q] to contain the entry: * f -> (lambda x. x+1) */ - bool 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. diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 73105af6f..88d00ce3a 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -387,7 +387,8 @@ void SynthEngine::printSynthSolution(std::ostream& out) } } -bool 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++) diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index b5880b0c1..20e4deec6 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -88,7 +88,7 @@ class SynthEngine : public QuantifiersModule * For details on what is added to sol_map, see * SynthConjecture::getSynthSolutions. */ - bool 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 dfda79aec..8337ba0b0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1294,7 +1294,8 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ return ret; } -bool QuantifiersEngine::getSynthSolutions(std::map& sol_map) +bool QuantifiersEngine::getSynthSolutions( + std::map >& sol_map) { return d_private->d_synth_e->getSynthSolutions(sol_map); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f84b59761..d1d7f1633 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -268,7 +268,7 @@ public: * For details on what is added to sol_map, see * SynthConjecture::getSynthSolutions. */ - bool 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 d73babdc0..7a72367de 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -944,7 +944,8 @@ TheoryModel* TheoryEngine::getBuiltModel() return d_curr_model; } -bool TheoryEngine::getSynthSolutions(std::map& sol_map) +bool TheoryEngine::getSynthSolutions( + std::map>& sol_map) { if (d_quantEngine) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index fc31572ec..dd34ae16b 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -779,7 +779,7 @@ public: * For details on what is added to sol_map, see * SynthConjecture::getSynthSolutions. */ - bool getSynthSolutions(std::map& sol_map); + bool getSynthSolutions(std::map >& sol_map); /** * Get the model builder -- 2.30.2