Make check synth solution robust to auxiliary assertions (#3432)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6a60c45dac471949f0ca3eb5165b5837e75e7240..7d28d8b85016cf0d8bcdfd3e8a23ad746a39bafc 100644 (file)
--- 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 d8c69edac354593fdcf363d6e88e00b49a3504f5..5edd18464d935d5771d34707939fc78e20ab9bd6 100644 (file)
--- 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 a86ff6f75dce7bc865568f8457db77e332df5c3e..344f8b4601c98f1c77519f5418b07de722ae06ff 100644 (file)
--- 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 73105af6f959059728643c10a644126ef558b485..88d00ce3a175b3daea31fd80f073c90e45ecbfbe 100644 (file)
--- 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 b5880b0c1772c3940f650ee784a3cd2454e9ce72..20e4deec6bd085f185dba31f9895ca16b5578c4e 100644 (file)
--- 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 dfda79aec0ccd58be5a1c3781f2bcd3b30a7a71b..8337ba0b072d09747e186261fa423efad97bb494 100644 (file)
--- 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 f84b59761a2452f9beaf5a2fe7dccb4e789e7810..d1d7f16330ff7c72615d19b067d450c6c305796f 100644 (file)
--- 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 d73babdc03204b0818d9853a8476c331341fbddc..7a72367de608d213d9dd1ca5c17a990b02935c13 100644 (file)
--- 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 fc31572ec102f6f3b8e8e02df20de4a37d55797b..dd34ae16b20c432a4ab5332befdc1d01e3c280a4 100644 (file)
--- 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