1 files changed, 52 insertions, 19 deletions

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e668b2206..03344d2e7 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -346,14 +346,17 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   {
     // get the model value of the relevant terms from the master module
     std::vector<Node> enum_values;
-    bool fullModel = getEnumeratedValues(terms, enum_values);
+    bool activeIncomplete = false;
+    bool fullModel = getEnumeratedValues(terms, enum_values, activeIncomplete);
 
     // if the master requires a full model and the model is partial, we fail
     if (!d_master->allowPartialModel() && !fullModel)
     {
       // we retain the values in d_ev_active_gen_waiting
       Trace("cegqi-engine") << "...partial model, fail." << std::endl;
-      return true;
+      // if we are partial due to an active enumerator, we may still succeed
+      // on the next call
+      return !activeIncomplete;
     }
     // the waiting values are passed to the module below, clear
     d_ev_active_gen_waiting.clear();
@@ -396,7 +399,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     if (emptyModel)
     {
       Trace("cegqi-engine") << "...empty model, fail." << std::endl;
-      return true;
+      return !activeIncomplete;
     }
     Assert(candidate_values.empty());
     constructed_cand = d_master->constructCandidates(
@@ -650,7 +653,8 @@ void SynthConjecture::preregisterConjecture(Node q)
 }
 
 bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
-                                          std::vector<Node>& v)
+                                          std::vector<Node>& v,
+                                          bool& activeIncomplete)
 {
   std::vector<Node> ncheck = n;
   n.clear();
@@ -670,7 +674,7 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
         continue;
       }
     }
-    Node nv = getEnumeratedValue(e);
+    Node nv = getEnumeratedValue(e, activeIncomplete);
     n.push_back(e);
     v.push_back(nv);
     ret = ret && !nv.isNull();
@@ -692,42 +696,50 @@ class EnumValGeneratorBasic : public EnumValGenerator
   /** initialize (do nothing) */
   void initialize(Node e) override {}
   /** initialize (do nothing) */
-  void addValue(Node v) override {}
+  void addValue(Node v) override { d_currTerm = *d_te; }
   /**
    * Get next returns the next (T-rewriter-unique) value based on the type
    * enumerator.
    */
-  Node getNext() override
+  bool increment() override
   {
     if (d_te.isFinished())
     {
-      return Node::null();
+      d_currTerm = Node::null();
+      return false;
     }
-    Node next = *d_te;
+    d_currTerm = *d_te;
     ++d_te;
     if (options::sygusSymBreakDynamic())
     {
-      Node nextb = d_tds->sygusToBuiltin(next);
+      Node nextb = d_tds->sygusToBuiltin(d_currTerm);
       nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
-      if (d_cache.find(nextb) != d_cache.end())
+      if (d_cache.find(nextb) == d_cache.end())
+      {
+        d_cache.insert(nextb);
+        // only return the current term if not unique
+      }
+      else
       {
-        return getNext();
+        d_currTerm = Node::null();
       }
-      d_cache.insert(nextb);
     }
-    return next;
+    return true;
   }
-
+  /** get the current term */
+  Node getCurrent() override { return d_currTerm; }
  private:
   /** pointer to term database sygus */
   TermDbSygus* d_tds;
   /** the type enumerator */
   TypeEnumerator d_te;
+  /** the current term */
+  Node d_currTerm;
   /** cache of (enumerated) builtin values we have enumerated so far */
   std::unordered_set<Node, NodeHashFunction> d_cache;
 };
 
-Node SynthConjecture::getEnumeratedValue(Node e)
+Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
 {
   bool isEnum = d_tds->isEnumerator(e);
 
@@ -790,6 +802,7 @@ Node SynthConjecture::getEnumeratedValue(Node e)
   // Check if there is an (abstract) value absE we were actively generating
   // values based on.
   Node absE = d_ev_curr_active_gen[e];
+  bool firstTime = false;
   if (absE.isNull())
   {
     // None currently exist. The next abstract value is the model value for e.
@@ -804,9 +817,22 @@ Node SynthConjecture::getEnumeratedValue(Node e)
     }
     d_ev_curr_active_gen[e] = absE;
     iteg->second->addValue(absE);
+    firstTime = true;
+  }
+  bool inc = true;
+  if (!firstTime)
+  {
+    inc = iteg->second->increment();
+  }
+  Node v;
+  if (inc)
+  {
+    v = iteg->second->getCurrent();
   }
-  Node v = iteg->second->getNext();
-  if (v.isNull())
+  Trace("sygus-active-gen-debug") << "...generated " << v
+                                  << ", with increment success : " << inc
+                                  << std::endl;
+  if (!inc)
   {
     // No more concrete values generated from absE.
     NodeManager* nm = NodeManager::currentNM();
@@ -852,7 +878,14 @@ Node SynthConjecture::getEnumeratedValue(Node e)
   else
   {
     // We are waiting to send e -> v to the module that requested it.
-    d_ev_active_gen_waiting[e] = v;
+    if (v.isNull())
+    {
+      activeIncomplete = true;
+    }
+    else
+    {
+      d_ev_active_gen_waiting[e] = v;
+    }
     if (Trace.isOn("sygus-active-gen"))
     {
       Trace("sygus-active-gen") << "Active-gen : " << e << " : ";