Allow multiple synthesis conjectures. (#2593)

4 files changed, 102 insertions, 103 deletions

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 4dfe33b58..469775a46 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -843,7 +843,7 @@ void SynthConjecture::printAndContinueStream()
   // get the current output stream
   // this output stream should coincide with wherever --dump-synth is output on
   Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
-  printSynthSolution(*nodeManagerOptions.getOut(), false);
+  printSynthSolution(*nodeManagerOptions.getOut());
 
   // We will not refine the current candidate solution since it is a solution
   // thus, we clear information regarding the current refinement
@@ -882,14 +882,13 @@ void SynthConjecture::printAndContinueStream()
   }
 }
 
-void SynthConjecture::printSynthSolution(std::ostream& out,
-                                         bool singleInvocation)
+void SynthConjecture::printSynthSolution(std::ostream& out)
 {
   Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
   Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
   std::vector<Node> sols;
   std::vector<int> statuses;
-  if (!getSynthSolutionsInternal(sols, statuses, singleInvocation))
+  if (!getSynthSolutionsInternal(sols, statuses))
   {
     return;
   }
@@ -963,13 +962,12 @@ void SynthConjecture::printSynthSolution(std::ostream& out,
   }
 }
 
-void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map,
-                                        bool singleInvocation)
+void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> sols;
   std::vector<int> statuses;
-  if (!getSynthSolutionsInternal(sols, statuses, singleInvocation))
+  if (!getSynthSolutionsInternal(sols, statuses))
   {
     return;
   }
@@ -1000,8 +998,7 @@ void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map,
 }
 
 bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
-                                                std::vector<int>& statuses,
-                                                bool singleInvocation)
+                                                std::vector<int>& statuses)
 {
   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
   {
@@ -1012,7 +1009,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
     // get the solution
     Node sol;
     int status = -1;
-    if (singleInvocation)
+    if (isSingleInvocation())
     {
       Assert(d_ceg_si != NULL);
       sol = d_ceg_si->getSolution(i, tn, status, true);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 4c18205af..d5ace4dfe 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -92,12 +92,11 @@ class SynthConjecture
   void doRefine(std::vector<Node>& lems);
   //-------------------------------end for counterexample-guided check/refine
   /**
-   * prints the synthesis solution to output stream out.
-   *
-   * singleInvocation : set to true if we should consult the single invocation
-   * module to get synthesis solutions.
+   * Prints the synthesis solution to output stream out. This invokes solution
+   * reconstruction if the conjecture is single invocation. Otherwise, it
+   * returns the enumer
    */
-  void printSynthSolution(std::ostream& out, bool singleInvocation);
+  void printSynthSolution(std::ostream& out);
   /** get synth solutions
    *
    * This returns a map from function-to-synthesize variables to their
@@ -105,11 +104,8 @@ class SynthConjecture
    * conjecture exists f. forall x. f( x )>x, this function may return the map
    * containing the entry:
    *   f -> (lambda x. x+1)
-   *
-   * singleInvocation : set to true if we should consult the single invocation
-   * module to get synthesis solutions.
    */
-  void getSynthSolutions(std::map<Node, Node>& sol_map, bool singleInvocation);
+  void 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.
@@ -309,16 +305,15 @@ class SynthConjecture
    * We store builtin versions under some conditions (such as when the sygus
    * grammar is being ignored).
    *
-   * singleInvocation : set to true if we should consult the single invocation
-   * module to get synthesis solutions.
+   * This consults the single invocation module to get synthesis solutions if
+   * isSingleInvocation() returns true.
    *
    * For example, for conjecture exists fg. forall x. f(x)>g(x), this function
    * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is
    * the sygus datatype constructor corresponding to variable x.
    */
   bool getSynthSolutionsInternal(std::vector<Node>& sols,
-                                 std::vector<int>& status,
-                                 bool singleInvocation);
+                                 std::vector<int>& status);
   //-------------------------------- sygus stream
   /** current stream guard */
   Node d_current_stream_guard;
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 296c10ff6..7ff16d82b 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -34,12 +34,12 @@ namespace quantifiers {
 SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
     : QuantifiersModule(qe)
 {
-  d_conj = new SynthConjecture(qe);
-  d_last_inst_si = false;
+  d_conjs.push_back(
+      std::unique_ptr<SynthConjecture>(new SynthConjecture(d_quantEngine)));
+  d_conj = d_conjs.back().get();
 }
 
-SynthEngine::~SynthEngine() { delete d_conj; }
-
+SynthEngine::~SynthEngine() {}
 bool SynthEngine::needsCheck(Theory::Effort e)
 {
   return e >= Theory::EFFORT_LAST_CALL;
@@ -47,65 +47,66 @@ bool SynthEngine::needsCheck(Theory::Effort e)
 
 QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
 {
-  return d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
+  return QEFFORT_MODEL;
 }
 
 void SynthEngine::check(Theory::Effort e, QEffort quant_e)
 {
   // are we at the proper effort level?
-  unsigned echeck =
-      d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
-  if (quant_e != echeck)
+  if (quant_e != QEFFORT_MODEL)
   {
     return;
   }
 
   // if we are waiting to assign the conjecture, do it now
-  if (!d_waiting_conj.isNull())
+  bool assigned = !d_waiting_conj.empty();
+  while (!d_waiting_conj.empty())
   {
-    Node q = d_waiting_conj;
+    Node q = d_waiting_conj.back();
+    d_waiting_conj.pop_back();
     Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q
                           << std::endl;
-    d_waiting_conj = Node::null();
-    if (!d_conj->isAssigned())
-    {
-      assignConjecture(q);
-      // assign conjecture always uses the output channel, we return and
-      // re-check here.
-      return;
-    }
+    assignConjecture(q);
+  }
+  if (assigned)
+  {
+    // assign conjecture always uses the output channel, either by reducing a
+    // quantified formula to another, or adding initial lemmas during
+    // SynthConjecture::assign. Thus, we return here and re-check.
+    return;
   }
 
   Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---"
                         << std::endl;
   Trace("cegqi-engine-debug") << std::endl;
-  bool active = false;
-  bool value;
-  if (d_quantEngine->getValuation().hasSatValue(d_conj->getConjecture(), value))
-  {
-    active = value;
-  }
-  else
+  Valuation& valuation = d_quantEngine->getValuation();
+  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
   {
+    SynthConjecture* sc = d_conjs[i].get();
+    bool active = false;
+    bool value;
+    if (valuation.hasSatValue(sc->getConjecture(), value))
+    {
+      active = value;
+    }
+    else
+    {
+      Trace("cegqi-engine-debug") << "...no value for quantified formula."
+                                  << std::endl;
+    }
     Trace("cegqi-engine-debug")
-        << "...no value for quantified formula." << std::endl;
-  }
-  Trace("cegqi-engine-debug")
-      << "Current conjecture status : active : " << active << std::endl;
-  if (active && d_conj->needsCheck())
-  {
-    checkConjecture(d_conj);
+        << "Current conjecture status : active : " << active << std::endl;
+    if (active && sc->needsCheck())
+    {
+      checkConjecture(sc);
+    }
   }
   Trace("cegqi-engine")
       << "Finished Counterexample Guided Instantiation engine." << std::endl;
 }
 
-bool SynthEngine::assignConjecture(Node q)
+void SynthEngine::assignConjecture(Node q)
 {
-  if (d_conj->isAssigned())
-  {
-    return false;
-  }
   Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl;
   if (options::sygusQePreproc())
   {
@@ -224,33 +225,31 @@ bool SynthEngine::assignConjecture(Node q)
                            << std::endl;
       d_quantEngine->getOutputChannel().lemma(lem);
       // we've reduced the original to a preprocessed version, return
-      return false;
+      return;
     }
   }
-  d_conj->assign(q);
-  return true;
+  // allocate a new synthesis conjecture if not assigned
+  if (d_conjs.back()->isAssigned())
+  {
+    d_conjs.push_back(
+        std::unique_ptr<SynthConjecture>(new SynthConjecture(d_quantEngine)));
+  }
+  d_conjs.back()->assign(q);
 }
 
 void SynthEngine::registerQuantifier(Node q)
 {
   if (d_quantEngine->getOwner(q) == this)
-  {  // && d_eval_axioms.find( q )==d_eval_axioms.end() ){
-    if (!d_conj->isAssigned())
+  {
+    Trace("cegqi") << "Register conjecture : " << q << std::endl;
+    if (options::sygusQePreproc())
     {
-      Trace("cegqi") << "Register conjecture : " << q << std::endl;
-      if (options::sygusQePreproc())
-      {
-        d_waiting_conj = q;
-      }
-      else
-      {
-        // assign it now
-        assignConjecture(q);
-      }
+      d_waiting_conj.push_back(q);
     }
     else
     {
-      Assert(d_conj->getEmbeddedConjecture() == q);
+      // assign it now
+      assignConjecture(q);
     }
   }
   else
@@ -278,7 +277,6 @@ void SynthEngine::checkConjecture(SynthConjecture* conj)
       conj->doSingleInvCheck(clems);
       if (!clems.empty())
       {
-        d_last_inst_si = true;
         for (const Node& lem : clems)
         {
           Trace("cegqi-lemma")
@@ -307,7 +305,6 @@ void SynthEngine::checkConjecture(SynthConjecture* conj)
     bool addedLemma = false;
     for (const Node& lem : cclems)
     {
-      d_last_inst_si = false;
       Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem
                            << std::endl;
       if (d_quantEngine->addLemma(lem))
@@ -368,21 +365,24 @@ void SynthEngine::checkConjecture(SynthConjecture* conj)
 
 void SynthEngine::printSynthSolution(std::ostream& out)
 {
-  if (d_conj->isAssigned())
-  {
-    d_conj->printSynthSolution(out, d_last_inst_si);
-  }
-  else
+  Assert(!d_conjs.empty());
+  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
   {
-    Assert(false);
+    if (d_conjs[i]->isAssigned())
+    {
+      d_conjs[i]->printSynthSolution(out);
+    }
   }
 }
 
 void SynthEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
 {
-  if (d_conj->isAssigned())
+  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
   {
-    d_conj->getSynthSolutions(sol_map, d_last_inst_si);
+    if (d_conjs[i]->isAssigned())
+    {
+      d_conjs[i]->getSynthSolutions(sol_map);
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index a7004c5c7..2a8994c25 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -31,24 +31,25 @@ class SynthEngine : public QuantifiersModule
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 
  private:
-  /** the quantified formula stating the synthesis conjecture */
+  /** the conjecture formula(s) we are waiting to assign */
+  std::vector<Node> d_waiting_conj;
+  /** The synthesis conjectures that this class is managing. */
+  std::vector<std::unique_ptr<SynthConjecture> > d_conjs;
+  /**
+   * The first conjecture in the above vector. We track this conjecture
+   * so that a synthesis conjecture can be preregistered during a call to
+   * preregisterAssertion.
+   */
   SynthConjecture* d_conj;
-  /** last instantiation by single invocation module? */
-  bool d_last_inst_si;
-  /** the conjecture we are waiting to assign */
-  Node d_waiting_conj;
-
- private:
-  /** assign quantified formula q as the conjecture
+  /** assign quantified formula q as a conjecture
    *
-   * This method returns true if q was successfully assigned as the synthesis
-   * conjecture considered by this class. This method may return false, for
-   * instance, if this class determines that it would rather rewrite q to
-   * an equivalent form r (in which case this method returns the lemma
-   * q <=> r). An example of this is the quantifier elimination step
-   * option::sygusQePreproc().
+   * This method either assigns q to a synthesis conjecture object in d_conjs,
+   * or otherwise reduces q to an equivalent form. This method does the latter
+   * if this class determines that it would rather rewrite q to an equivalent
+   * form r (in which case this method returns the lemma q <=> r). An example of
+   * this is the quantifier elimination step option::sygusQePreproc().
    */
-  bool assignConjecture(Node q);
+  void assignConjecture(Node q);
   /** check conjecture */
   void checkConjecture(SynthConjecture* conj);
 
@@ -56,7 +57,6 @@ class SynthEngine : public QuantifiersModule
   SynthEngine(QuantifiersEngine* qe, context::Context* c);
   ~SynthEngine();
 
- public:
   bool needsCheck(Theory::Effort e) override;
   QEffort needsModel(Theory::Effort e) override;
   /* Call during quantifier engine's check */
@@ -78,7 +78,14 @@ class SynthEngine : public QuantifiersModule
    * SynthConjecture::getSynthSolutions.
    */
   void getSynthSolutions(std::map<Node, Node>& sol_map);
-  /** preregister assertion (before rewrite) */
+  /** preregister assertion (before rewrite)
+   *
+   * The purpose of this method is to inform the solution reconstruction
+   * techniques within the single invocation module that n is an original
+   * assertion, prior to rewriting. This is used as a heuristic to remember
+   * terms that are likely to help when trying to reconstruct a solution
+   * that fits a given input syntax.
+   */
   void preregisterAssertion(Node n);
 
  public: