summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp83
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp7
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.h9
-rw-r--r--src/theory/quantifiers/sygus/synth_engine.cpp3
-rw-r--r--src/theory/quantifiers/sygus/synth_engine.h2
-rw-r--r--src/theory/quantifiers_engine.cpp3
-rw-r--r--src/theory/quantifiers_engine.h2
-rw-r--r--src/theory/theory_engine.cpp3
-rw-r--r--src/theory/theory_engine.h2
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<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;
}
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<Node, Node>& sol_map)
+bool SynthConjecture::getSynthSolutions(
+ std::map<Node, std::map<Node, Node> >& sol_map)
{
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> sols;
@@ -1153,6 +1154,8 @@ bool SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
{
return false;
}
+ // we add it to the solution map, indexed by this conjecture
+ std::map<Node, Node>& 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<Node, Node>& 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<Node, Node>& sol_map);
+ bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& 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<Node, Node>& sol_map)
+bool SynthEngine::getSynthSolutions(
+ std::map<Node, std::map<Node, Node> >& 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<Node, Node>& sol_map);
+ bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& 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<Node, Node>& sol_map)
+bool QuantifiersEngine::getSynthSolutions(
+ std::map<Node, std::map<Node, Node> >& 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<Node, Node>& sol_map);
+ bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& 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<Node, Node>& sol_map)
+bool TheoryEngine::getSynthSolutions(
+ std::map<Node, std::map<Node, Node>>& 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<Node, Node>& sol_map);
+ bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
/**
* Get the model builder
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback