Make getSynthSolution return a Bool (#3306)

4 files changed, 52 insertions, 15 deletions

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 7f48d30d8..d8c69edac 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -47,7 +47,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p)
     : d_qe(qe),
       d_parent(p),
       d_tds(qe->getTermDatabaseSygus()),
-      d_hasSolution(false, qe->getUserContext()),
+      d_hasSolution(false),
       d_ceg_si(new CegSingleInv(qe, this)),
       d_ceg_proc(new SynthConjectureProcess(qe)),
       d_ceg_gc(new CegGrammarConstructor(qe, this)),
@@ -300,6 +300,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     return true;
   }
   Assert(d_master != nullptr);
+  Assert(!d_hasSolution);
 
   // get the list of terms that the master strategy is interested in
   std::vector<Node> terms;
@@ -486,6 +487,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       lem = getStreamGuardedLemma(lem);
       lems.push_back(lem);
       recordInstantiation(candidate_values);
+      d_hasSolution = true;
       return true;
     }
     Assert(!d_set_ce_sk_vars);
@@ -607,14 +609,16 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   }
   if (success)
   {
+    d_hasSolution = true;
     if (options::sygusStream())
     {
       // if we were successful, we immediately print the current solution.
       // this saves us from introducing a verification lemma and a new guard.
       printAndContinueStream(terms, candidate_values);
+      // streaming means now we immediately are looking for a new solution
+      d_hasSolution = false;
       return false;
     }
-    d_hasSolution = true;
   }
   lem = getStreamGuardedLemma(lem);
   lems.push_back(lem);
@@ -1140,14 +1144,14 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
   }
 }
 
-void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
+bool SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> sols;
   std::vector<int> statuses;
   if (!getSynthSolutionsInternal(sols, statuses))
   {
-    return;
+    return false;
   }
   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
   {
@@ -1180,11 +1184,16 @@ void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
     // store in map
     sol_map[fvar] = bsol;
   }
+  return true;
 }
 
 bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
                                                 std::vector<int>& statuses)
 {
+  if (!d_hasSolution)
+  {
+    return false;
+  }
   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
   {
     Node prog = d_embed_quant[0][i];
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 8ae30f636..a86ff6f75 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -113,13 +113,16 @@ class SynthConjecture
   void printSynthSolution(std::ostream& out);
   /** get synth solutions
    *
-   * This returns a map from function-to-synthesize variables to their
-   * builtin solution, which has the same type. For example, for synthesis
+   * 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
+   * 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:
    *   f -> (lambda x. x+1)
    */
-  void getSynthSolutions(std::map<Node, Node>& sol_map);
+  bool getSynthSolutions(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.
@@ -174,10 +177,10 @@ class SynthConjecture
   /** The feasible guard. */
   Node d_feasible_guard;
   /**
-   * Do we have a solution in this user context? This is user-context dependent
-   * to enable use cases of sygus in incremental mode.
+   * Do we have a solution in this solve context? This flag is reset to false
+   * on every call to presolve.
    */
-  context::CDO<bool> d_hasSolution;
+  bool d_hasSolution;
   /** the decision strategy for the feasible guard */
   std::unique_ptr<DecisionStrategy> d_feasible_strategy;
   /** single invocation utility */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index d13bd2dcf..73105af6f 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -41,6 +41,17 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
 }
 
 SynthEngine::~SynthEngine() {}
+
+void SynthEngine::presolve()
+{
+  Trace("cegqi-engine") << "SynthEngine::presolve" << std::endl;
+  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
+  {
+    d_conjs[i]->presolve();
+  }
+  Trace("cegqi-engine") << "SynthEngine::presolve finished" << std::endl;
+}
+
 bool SynthEngine::needsCheck(Theory::Effort e)
 {
   return e >= Theory::EFFORT_LAST_CALL;
@@ -130,7 +141,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
 
 void SynthEngine::assignConjecture(Node q)
 {
-  Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl;
+  Trace("cegqi-engine") << "SynthEngine::assignConjecture " << q << std::endl;
   if (options::sygusQePreproc())
   {
     // the following does quantifier elimination as a preprocess step
@@ -376,15 +387,22 @@ void SynthEngine::printSynthSolution(std::ostream& out)
   }
 }
 
-void SynthEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
+bool SynthEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
 {
+  bool ret = true;
   for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
   {
     if (d_conjs[i]->isAssigned())
     {
-      d_conjs[i]->getSynthSolutions(sol_map);
+      if (!d_conjs[i]->getSynthSolutions(sol_map))
+      {
+        // if one conjecture fails, we fail overall
+        ret = false;
+        break;
+      }
     }
   }
+  return ret;
 }
 
 void SynthEngine::preregisterAssertion(Node n)
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index e099657ad..b5880b0c1 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -60,8 +60,15 @@ class SynthEngine : public QuantifiersModule
  public:
   SynthEngine(QuantifiersEngine* qe, context::Context* c);
   ~SynthEngine();
-
+  /** presolve
+   *
+   * Called at the beginning of each call to solve a synthesis problem, which
+   * may be e.g. a check-synth or get-abduct call.
+   */
+  void presolve() override;
+  /** needs check, return true if e is last call */
   bool needsCheck(Theory::Effort e) override;
+  /** always needs model at effort QEFFORT_MODEL */
   QEffort needsModel(Theory::Effort e) override;
   /* Call during quantifier engine's check */
   void check(Theory::Effort e, QEffort quant_e) override;
@@ -81,7 +88,7 @@ class SynthEngine : public QuantifiersModule
    * For details on what is added to sol_map, see
    * SynthConjecture::getSynthSolutions.
    */
-  void getSynthSolutions(std::map<Node, Node>& sol_map);
+  bool getSynthSolutions(std::map<Node, Node>& sol_map);
   /** preregister assertion (before rewrite)
    *
    * The purpose of this method is to inform the solution reconstruction