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

8 files changed, 19 insertions, 12 deletions

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