diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 83 |
1 files changed, 57 insertions, 26 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<Node, Node> sol_map; + std::map<Node, std::map<Node, Node>> 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<Node> function_vars, function_sols; - for (const auto& pair : sol_map) + // the set of synthesis conjectures in our assertions + std::unordered_set<Node, NodeHashFunction> conjs; + // For each of the above conjectures, the functions-to-synthesis and their + // solutions. This is used as a substitution below. + std::map<Node, std::vector<Node>> fvarMap; + std::map<Node, std::vector<Node>> fsolMap; + for (const std::pair<const Node, std::map<Node, Node>>& 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<Node>& fvars = fvarMap[cmap.first]; + std::vector<Node>& fsols = fsolMap[cmap.first]; + for (const std::pair<const Node, Node>& 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<Node> auxAssertions; + // expand definitions cache + std::unordered_map<Node, Node, NodeHashFunction> 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<Node, Node, NodeHashFunction> 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<Node>& fvars = fvarMap[conj]; + std::vector<Node>& 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<Node> 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<Expr, Expr>& sol_map) { SmtScope smts(this); finalOptionsAreSet(); - map<Node, Node> sol_mapn; + std::map<Node, std::map<Node, Node>> 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<const Node, Node>& s : sol_mapn) + for (std::pair<const Node, std::map<Node, Node>>& cs : sol_mapn) { - sol_map[s.first.toExpr()] = s.second.toExpr(); + for (std::pair<const Node, Node>& s : cs.second) + { + sol_map[s.first.toExpr()] = s.second.toExpr(); + } } return true; } |