Allow multiple synthesis conjectures. (#2593)

1 files changed, 63 insertions, 63 deletions

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);
+    }
   }
 }