Support for basic actively-generated enumerators (#2606)

13 files changed, 200 insertions, 122 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index b698422a7..d4735b3d8 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -661,8 +661,6 @@ Node CegSingleInv::reconstructToSyntax(Node s,
   }
 }
 
-bool CegSingleInv::needsCheck() { return true; }
-
 void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; }
 
 bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index cfd7cd23b..0de7b4290 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -275,8 +275,6 @@ class CegSingleInv
                             bool rconsSygus = true );
   // is single invocation
   bool isSingleInvocation() const { return !d_single_inv.isNull(); }
-  //needs check
-  bool needsCheck();
   /** preregister conjecture */
   void preregisterConjecture( Node q );
 
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index ad45fb9b7..2e7f0cc02 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -78,7 +78,8 @@ bool Cegis::processInitialize(Node n,
   // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj)
   // for each i,j. We do not do this and revert to the default behavior of
   // this module instead.
-  bool isVarAgnostic = options::sygusEnumVarAgnostic() && csize == 1;
+  bool isActiveGen =
+      options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1;
   // initialize an enumerator for each candidate
   for (unsigned i = 0; i < csize; i++)
   {
@@ -101,9 +102,9 @@ bool Cegis::processInitialize(Node n,
     d_tds->registerEnumerator(candidates[i],
                               candidates[i],
                               d_parent,
-                              isVarAgnostic,
+                              isActiveGen,
                               do_repair_const,
-                              isVarAgnostic);
+                              isActiveGen);
   }
   return true;
 }
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 9367444ac..dbde79aae 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -86,7 +86,6 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates,
   // Non-unif candidate are themselves the enumerators
   enums.insert(
       enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end());
-  Valuation& valuation = d_qe->getValuation();
   for (const Node& c : d_unif_candidates)
   {
     // Collect heads of candidates
@@ -104,19 +103,6 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates,
         std::vector<Node> uenums;
         // get the current unification enumerators
         d_u_enum_manager.getEnumeratorsForStrategyPt(e, uenums, index);
-        if (index == 1 && options::sygusUnifCondIndependent())
-        {
-          Assert(uenums.size() == 1);
-          Node eu = uenums[0];
-          Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu);
-          // If active guard for this enumerator is not true, there are no more
-          // values for it, and hence we ignore it
-          Node gstatus = valuation.getSatValue(g);
-          if (gstatus.isNull() || !gstatus.getConst<bool>())
-          {
-            continue;
-          }
-        }
         // get the model value of each enumerator
         enums.insert(enums.end(), uenums.begin(), uenums.end());
       }
@@ -264,7 +250,7 @@ void CegisUnif::setConditions(
         Assert(!itv->second.empty());
         if (d_tds->isPassiveEnumerator(eu))
         {
-          Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu);
+          Node g = d_tds->getActiveGuardForEnumerator(eu);
           Node exp_exc = d_tds->getExplain()
                              ->getExplanationForEquality(eu, itv->second[0])
                              .negate();
@@ -563,7 +549,6 @@ void CegisUnifEnumDecisionStrategy::initialize(
     {
       Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
       setUpEnumerator(ceu, ci.second, 1);
-      d_enum_to_active_guard[ceu] = d_tds->getActiveGuardForEnumerator(ceu);
     }
   }
 }
@@ -592,12 +577,6 @@ void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt(
   }
 }
 
-Node CegisUnifEnumDecisionStrategy::getActiveGuardForEnumerator(Node e)
-{
-  Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
-  return d_enum_to_active_guard[e];
-}
-
 void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
                                                     StrategyPtInfo& si,
                                                     unsigned index)
@@ -628,19 +607,19 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
   // register the enumerator
   si.d_enums[index].push_back(e);
   bool mkActiveGuard = false;
-  bool isVarAgnostic = false;
+  bool isActiveGen = false;
   // if we are using a single independent enumerator for conditions, then we
   // allocate an active guard, and are eligible to use variable-agnostic
   // enumeration.
   if (options::sygusUnifCondIndependent() && index == 1)
   {
     mkActiveGuard = true;
-    isVarAgnostic = options::sygusEnumVarAgnostic();
+    isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE;
   }
   Trace("cegis-unif-enum") << "* Registering new enumerator " << e
                            << " to strategy point " << si.d_pt << "\n";
   d_tds->registerEnumerator(
-      e, si.d_pt, d_parent, mkActiveGuard, false, isVarAgnostic);
+      e, si.d_pt, d_parent, mkActiveGuard, false, isActiveGen);
 }
 
 void CegisUnifEnumDecisionStrategy::registerEvalPts(
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 02cf1cdf2..fef24e9bb 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -84,10 +84,14 @@ class SygusModule
   /** construct candidate
    *
    * This function takes as input:
-   *   terms : the terms returned by a call to getTermList,
+   *   terms : (a subset of) the terms returned by a call to getTermList,
    *   term_values : the current model values of terms,
    *   candidates : the list of candidates.
    *
+   * In particular, notice that terms do not include inactive enumerators,
+   * thus if inactive enumerators were added to getTermList, then the terms
+   * list passed to this call will be a (strict) subset of that list.
+   *
    * If this function returns true, it adds to candidate_values a list of terms
    * of the same length and type as candidates that are candidate solutions
    * to the synthesis conjecture in question. This candidate { v } will then be
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 8050e97f8..ac8b56ee4 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -179,7 +179,7 @@ bool SygusPbe::initialize(Node n,
       return false;
     }
   }
-  bool isVarAgnostic = options::sygusEnumVarAgnostic();
+  bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE;
   for (const Node& c : candidates)
   {
     Assert(d_examples.find(c) != d_examples.end());
@@ -203,9 +203,7 @@ bool SygusPbe::initialize(Node n,
     for (const Node& e : d_candidate_to_enum[c])
     {
       TypeNode etn = e.getType();
-      d_tds->registerEnumerator(e, c, d_parent, true, false, isVarAgnostic);
-      Node g = d_tds->getActiveGuardForEnumerator(e);
-      d_enum_to_active_guard[e] = g;
+      d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen);
       d_enum_to_candidate[e] = c;
       TNode te = e;
       // initialize static symmetry breaking lemmas for it
@@ -397,27 +395,13 @@ Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i)
 void SygusPbe::getTermList(const std::vector<Node>& candidates,
                            std::vector<Node>& terms)
 {
-  Valuation& valuation = d_qe->getValuation();
   for( unsigned i=0; i<candidates.size(); i++ ){
     Node v = candidates[i];
     std::map<Node, std::vector<Node> >::iterator it =
         d_candidate_to_enum.find(v);
     if (it != d_candidate_to_enum.end())
     {
-      for (unsigned j = 0; j < it->second.size(); j++)
-      {
-        Node e = it->second[j];
-        Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
-        Node g = d_enum_to_active_guard[e];
-        // Get whether the active guard for this enumerator is true,
-        // if so, then there may exist more values for it, and hence we add it
-        // to terms.
-        Node gstatus = valuation.getSatValue(g);
-        if (!gstatus.isNull() && gstatus.getConst<bool>())
-        {
-          terms.push_back(e);
-        }
-      }
+      terms.insert(terms.end(), it->second.begin(), it->second.end());
     }
   }
 }
@@ -491,8 +475,8 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
       if (!enum_lems.empty())
       {
         // the lemmas must be guarded by the active guard of the enumerator
-        Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
-        Node g = d_enum_to_active_guard[e];
+        Node g = d_tds->getActiveGuardForEnumerator(e);
+        Assert(!g.isNull());
         for (unsigned j = 0, size = enum_lems.size(); j < size; j++)
         {
           enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]);
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index b2ad5f63a..e21c9263f 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -230,8 +230,6 @@ class SygusPbe : public SygusModule
   std::map<Node, std::vector<Node> > d_candidate_to_enum;
   /** reverse map of above */
   std::map<Node, Node> d_enum_to_candidate;
-  /** map from enumerators to active guards */
-  std::map<Node, Node> d_enum_to_active_guard;
   /** for each candidate variable (function-to-synthesize), input of I/O
    * examples */
   std::map<Node, std::vector<std::vector<Node> > > d_examples;
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 469775a46..7955d59a8 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -53,7 +53,8 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe)
       d_master(nullptr),
       d_set_ce_sk_vars(false),
       d_repair_index(0),
-      d_refine_count(0)
+      d_refine_count(0),
+      d_guarded_stream_exc(false)
 {
   if (options::sygusSymBreakPbe() || options::sygusUnifPbe())
   {
@@ -240,10 +241,6 @@ bool SynthConjecture::isSingleInvocation() const
 
 bool SynthConjecture::needsCheck()
 {
-  if (isSingleInvocation() && !d_ceg_si->needsCheck())
-  {
-    return false;
-  }
   bool value;
   Assert(!d_feasible_guard.isNull());
   // non or fully single invocation : look at guard only
@@ -254,6 +251,11 @@ bool SynthConjecture::needsCheck()
       Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
       return false;
     }
+    else
+    {
+      Trace("cegqi-engine-debug") << "Feasible guard " << d_feasible_guard
+                                  << " assigned true." << std::endl;
+    }
   }
   else
   {
@@ -273,7 +275,7 @@ void SynthConjecture::doSingleInvCheck(std::vector<Node>& lems)
 }
 
 bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
-void SynthConjecture::doCheck(std::vector<Node>& lems)
+bool SynthConjecture::doCheck(std::vector<Node>& lems)
 {
   Assert(d_master != nullptr);
 
@@ -288,24 +290,10 @@ void SynthConjecture::doCheck(std::vector<Node>& lems)
       // we have a new guard, print and continue the stream
       printAndContinueStream();
       d_current_stream_guard = currGuard;
-      return;
+      return true;
     }
   }
-  bool checkSuccess = false;
-  do
-  {
-    Trace("cegqi-check-debug") << "doCheckNext..." << std::endl;
-    checkSuccess = doCheckNext(lems);
-    Trace("cegqi-check-debug")
-        << "...finished " << lems.empty() << " " << !needsRefinement() << " "
-        << !d_qe->getTheoryEngine()->needCheck() << " " << checkSuccess
-        << std::endl;
-  } while (lems.empty() && !needsRefinement()
-           && !d_qe->getTheoryEngine()->needCheck() && checkSuccess);
-}
 
-bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
-{
   // get the list of terms that the master strategy is interested in
   std::vector<Node> terms;
   d_master->getTermList(d_candidates, terms);
@@ -364,7 +352,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
     {
       // we retain the values in d_ev_active_gen_waiting
       Trace("cegqi-engine") << "...partial model, fail." << std::endl;
-      return false;
+      return true;
     }
     // the waiting values are passed to the module below, clear
     d_ev_active_gen_waiting.clear();
@@ -407,7 +395,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
     if (emptyModel)
     {
       Trace("cegqi-engine") << "...empty model, fail." << std::endl;
-      return false;
+      return true;
     }
     Assert(candidate_values.empty());
     constructed_cand = d_master->constructCandidates(
@@ -462,7 +450,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
   {
     if (!constructed_cand)
     {
-      return true;
+      return false;
     }
   }
 
@@ -502,7 +490,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
   if (lem.isNull())
   {
     // no lemma to check
-    return true;
+    return false;
   }
 
   lem = Rewriter::rewrite(lem);
@@ -557,7 +545,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
         Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
         Assert(squery.isConst() && squery.getConst<bool>());
 #endif
-        return true;
+        return false;
       }
       else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
@@ -577,7 +565,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
     // if we were successful, we immediately print the current solution.
     // this saves us from introducing a verification lemma and a new guard.
     printAndContinueStream();
-    return true;
+    return false;
   }
   lem = getStreamGuardedLemma(lem);
   lems.push_back(lem);
@@ -662,30 +650,101 @@ void SynthConjecture::preregisterConjecture(Node q)
 bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
                                           std::vector<Node>& v)
 {
+  std::vector<Node> ncheck = n;
+  n.clear();
   bool ret = true;
-  for (unsigned i = 0; i < n.size(); i++)
+  for (unsigned i = 0, size = ncheck.size(); i < size; i++)
   {
-    Node nv = getEnumeratedValue(n[i]);
+    Node e = ncheck[i];
+    // if it is not active, we return null
+    Node g = d_tds->getActiveGuardForEnumerator(e);
+    if (!g.isNull())
+    {
+      Node gstatus = d_qe->getValuation().getSatValue(g);
+      if (gstatus.isNull() || !gstatus.getConst<bool>())
+      {
+        Trace("cegqi-engine-debug")
+            << "Enumerator " << e << " is inactive." << std::endl;
+        continue;
+      }
+    }
+    Node nv = getEnumeratedValue(e);
+    n.push_back(e);
     v.push_back(nv);
     ret = ret && !nv.isNull();
   }
   return ret;
 }
 
+/** A basic sygus value generator
+ *
+ * This class is a "naive" term generator for sygus conjectures, which invokes
+ * the type enumerator to generate a stream of (all) sygus terms of a given
+ * type.
+ */
+class EnumValGeneratorBasic : public EnumValGenerator
+{
+ public:
+  EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn) : d_tds(tds), d_te(tn) {}
+  ~EnumValGeneratorBasic() {}
+  /** initialize (do nothing) */
+  void initialize(Node e) override {}
+  /** initialize (do nothing) */
+  void addValue(Node v) override {}
+  /**
+   * Get next returns the next (T-rewriter-unique) value based on the type
+   * enumerator.
+   */
+  Node getNext() override
+  {
+    if (d_te.isFinished())
+    {
+      return Node::null();
+    }
+    Node next = *d_te;
+    ++d_te;
+    Node nextb = d_tds->sygusToBuiltin(next);
+    if (options::sygusSymBreakDynamic())
+    {
+      nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
+    }
+    if (d_cache.find(nextb) == d_cache.end())
+    {
+      d_cache.insert(nextb);
+      return next;
+    }
+    return getNext();
+  }
+
+ private:
+  /** pointer to term database sygus */
+  TermDbSygus* d_tds;
+  /** the type enumerator */
+  TypeEnumerator d_te;
+  /** cache of (enumerated) builtin values we have enumerated so far */
+  std::unordered_set<Node, NodeHashFunction> d_cache;
+};
+
 Node SynthConjecture::getEnumeratedValue(Node e)
 {
-  if (e.getAttribute(SygusSymBreakExcAttribute()))
+  bool isEnum = d_tds->isEnumerator(e);
+
+  if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
   {
-    // if the current model value of e was excluded by symmetry breaking, then
-    // it does not have a proper model value that we should consider, thus we
-    // return null.
+    // if the current model value of e was not registered by the datatypes
+    // sygus solver, or was excluded by symmetry breaking, then it does not
+    // have a proper model value that we should consider, thus we return null.
+    Trace("cegqi-engine-debug")
+        << "Enumerator " << e << " does not have proper model value."
+        << std::endl;
     return Node::null();
   }
 
-  if (!d_tds->isEnumerator(e) || d_tds->isPassiveEnumerator(e))
+  if (!isEnum || d_tds->isPassiveEnumerator(e))
   {
     return getModelValue(e);
   }
+
   // management of actively generated enumerators goes here
 
   // initialize the enumerated value generator for e
@@ -693,7 +752,14 @@ Node SynthConjecture::getEnumeratedValue(Node e)
       d_evg.find(e);
   if (iteg == d_evg.end())
   {
-    d_evg[e].reset(new EnumStreamConcrete(d_tds));
+    if (d_tds->isVariableAgnosticEnumerator(e))
+    {
+      d_evg[e].reset(new EnumStreamConcrete(d_tds));
+    }
+    else
+    {
+      d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
+    }
     Trace("sygus-active-gen")
         << "Active-gen: initialize for " << e << std::endl;
     d_evg[e]->initialize(e);
@@ -872,6 +938,11 @@ void SynthConjecture::printAndContinueStream()
   }
   if (!exp.empty())
   {
+    if (!d_guarded_stream_exc)
+    {
+      d_guarded_stream_exc = true;
+      exp.push_back(d_feasible_guard);
+    }
     Node exc_lem = exp.size() == 1
                        ? exp[0]
                        : NodeManager::currentNM()->mkNode(kind::AND, exp);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index d5ace4dfe..ef1b4459f 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -83,9 +83,19 @@ class SynthConjecture
    */
   void doSingleInvCheck(std::vector<Node>& lems);
   /** do syntax-guided enumerative check
+   *
    * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
+   *
+   * The method returns true if this conjecture is finished trying solutions
+   * for the given call to SynthEngine::check.
+   *
+   * Notice that we make multiple calls to doCheck on one call to
+   * SynthEngine::check. For example, if we are using an actively-generated
+   * enumerator, one enumerated (abstract) term may correspond to multiple
+   * concrete terms t1, ..., tn to check, where we make up to n calls to doCheck
+   * when each of t1, ..., tn fails to satisfy the current refinement lemmas.
    */
-  void doCheck(std::vector<Node>& lems);
+  bool doCheck(std::vector<Node>& lems);
   /** do refinement
    * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
    */
@@ -94,7 +104,7 @@ class SynthConjecture
   /**
    * Prints the synthesis solution to output stream out. This invokes solution
    * reconstruction if the conjecture is single invocation. Otherwise, it
-   * returns the enumer
+   * returns the solution found by sygus enumeration.
    */
   void printSynthSolution(std::ostream& out);
   /** get synth solutions
@@ -182,6 +192,9 @@ class SynthConjecture
   /**
    * Get model values for terms n, store in vector v. This method returns true
    * if and only if all values added to v are non-null.
+   *
+   * It removes terms from n that correspond to "inactive" enumerators, that
+   * is, enumerators whose values have been exhausted.
    */
   bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v);
   /**
@@ -282,18 +295,6 @@ class SynthConjecture
       d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
     }
   }
-  /**
-   * This performs the next check of the syntax-guided enumerative check
-   * (see doCheck above). The method returns true if a new solution was
-   * considered.
-   *
-   * Notice that one call to doCheck may correspond to multiple calls to
-   * doCheckNext. For example, if we are using an actively-generated enumerator,
-   * one enumerated (abstract) term may correspond to multiple concrete
-   * terms t1, ..., tn to check, where we make up to n calls to doCheckNext when
-   * each of t1, ..., tn fail to satisfy the current refinement lemmas.
-   */
-  bool doCheckNext(std::vector<Node>& lems);
   /** get synth solutions internal
    *
    * This function constructs the body of solutions for all
@@ -343,9 +344,15 @@ class SynthConjecture
   /**
    * Prints the current synthesis solution to the output stream indicated by
    * the Options object, send a lemma blocking the current solution to the
-   * output channel.
+   * output channel, which we refer to as a "stream exclusion lemma".
    */
   void printAndContinueStream();
+  /**
+   * Whether we have guarded a stream exclusion lemma when using sygusStream.
+   * This is an optimization that allows us to guard only the first stream
+   * exclusion lemma.
+   */
+  bool d_guarded_stream_exc;
   //-------------------------------- end sygus stream
   /** expression miner managers for each function-to-synthesize
    *
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 7ff16d82b..ba227bc8f 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -80,6 +80,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
                         << std::endl;
   Trace("cegqi-engine-debug") << std::endl;
   Valuation& valuation = d_quantEngine->getValuation();
+  std::vector<SynthConjecture*> activeCheckConj;
   for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
   {
     SynthConjecture* sc = d_conjs[i].get();
@@ -98,9 +99,30 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
         << "Current conjecture status : active : " << active << std::endl;
     if (active && sc->needsCheck())
     {
-      checkConjecture(sc);
+      activeCheckConj.push_back(sc);
     }
   }
+  std::vector<SynthConjecture*> acnext;
+  do
+  {
+    Trace("cegqi-engine-debug") << "Checking " << activeCheckConj.size()
+                                << " active conjectures..." << std::endl;
+    for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
+    {
+      SynthConjecture* sc = activeCheckConj[i];
+      if (!checkConjecture(sc))
+      {
+        if (!sc->needsRefinement())
+        {
+          acnext.push_back(sc);
+        }
+      }
+    }
+    activeCheckConj.clear();
+    activeCheckConj = acnext;
+    acnext.clear();
+  } while (!activeCheckConj.empty()
+           && !d_quantEngine->getTheoryEngine()->needCheck());
   Trace("cegqi-engine")
       << "Finished Counterexample Guided Instantiation engine." << std::endl;
 }
@@ -258,7 +280,7 @@ void SynthEngine::registerQuantifier(Node q)
   }
 }
 
-void SynthEngine::checkConjecture(SynthConjecture* conj)
+bool SynthEngine::checkConjecture(SynthConjecture* conj)
 {
   Node q = conj->getEmbeddedConjecture();
   Node aq = conj->getConjecture();
@@ -296,12 +318,12 @@ void SynthEngine::checkConjecture(SynthConjecture* conj)
             << "  ...FAILED to add cbqi instantiation for single invocation!"
             << std::endl;
       }
-      return;
+      return true;
     }
 
     Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
     std::vector<Node> cclems;
-    conj->doCheck(cclems);
+    bool ret = conj->doCheck(cclems);
     bool addedLemma = false;
     for (const Node& lem : cclems)
     {
@@ -322,16 +344,17 @@ void SynthEngine::checkConjecture(SynthConjecture* conj)
     if (addedLemma)
     {
       Trace("cegqi-engine") << "  ...check for counterexample." << std::endl;
+      return true;
     }
     else
     {
       if (conj->needsRefinement())
       {
         // immediately go to refine candidate
-        checkConjecture(conj);
-        return;
+        return checkConjecture(conj);
       }
     }
+    return ret;
   }
   else
   {
@@ -361,6 +384,7 @@ void SynthEngine::checkConjecture(SynthConjecture* conj)
       Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
     }
   }
+  return true;
 }
 
 void SynthEngine::printSynthSolution(std::ostream& out)
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 2a8994c25..8f0eea58f 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -50,8 +50,12 @@ class SynthEngine : public QuantifiersModule
    * this is the quantifier elimination step option::sygusQePreproc().
    */
   void assignConjecture(Node q);
-  /** check conjecture */
-  void checkConjecture(SynthConjecture* conj);
+  /** check conjecture
+   *
+   * This method returns true if the conjecture is finished processing solutions
+   * for this call to SynthEngine::check().
+   */
+  bool checkConjecture(SynthConjecture* conj);
 
  public:
   SynthEngine(QuantifiersEngine* qe, context::Context* c);
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 1a8c81bcc..d5b7bc51c 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -371,7 +371,9 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
             Trace("sygus-db") << ", kind = " << sk;
             d_kinds[tn][sk] = i;
             d_arg_kind[tn][i] = sk;
-          }else if( sop.isConst() ){
+          }
+          else if (sop.isConst() && dt[i].getNumArgs() == 0)
+          {
             Trace("sygus-db") << ", constant";
             d_consts[tn][n] = i;
             d_arg_const[tn][i] = n;
@@ -466,7 +468,7 @@ void TermDbSygus::registerEnumerator(Node e,
                                      SynthConjecture* conj,
                                      bool mkActiveGuard,
                                      bool useSymbolicCons,
-                                     bool isVarAgnostic)
+                                     bool isActiveGen)
 {
   if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
   {
@@ -564,6 +566,10 @@ void TermDbSygus::registerEnumerator(Node e,
   }
   Trace("sygus-db") << "  ...finished" << std::endl;
 
+  d_enum_active_gen[e] = isActiveGen;
+  bool isVarAgnostic =
+      isActiveGen
+      && options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
   d_enum_var_agnostic[e] = isVarAgnostic;
   if (isVarAgnostic)
   {
@@ -667,11 +673,11 @@ bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const
 
 bool TermDbSygus::isPassiveEnumerator(Node e) const
 {
-  if (isVariableAgnosticEnumerator(e))
+  std::map<Node, bool>::const_iterator itus = d_enum_active_gen.find(e);
+  if (itus != d_enum_active_gen.end())
   {
-    return false;
+    return !itus->second;
   }
-  // other criteria go here
   return true;
 }
 
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 785e8731c..56ed68e76 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -69,8 +69,10 @@ class TermDbSygus {
    * (see d_enum_to_active_guard),
    * useSymbolicCons : whether we want model values for e to include symbolic
    * constructors like the "any constant" variable.
-   * isVarAgnostic : if this flag is true, the enumerator will only generate
-   * values whose variables are in canonical order (for example, only x1-x2
+   * isActiveGen : if this flag is true, the enumerator will be
+   * actively-generated based on the mode specified by --sygus-active-gen.
+   * For example, if --sygus-active-gen=var-agnostic, then the enumerator will
+   * only generate values whose variables are in canonical order (only x1-x2
    * and not x2-x1 will be generated, assuming x1 and x2 are in the same
    * "subclass", see getSubclassForVar).
    *
@@ -83,7 +85,7 @@ class TermDbSygus {
                           SynthConjecture* conj,
                           bool mkActiveGuard = false,
                           bool useSymbolicCons = false,
-                          bool isVarAgnostic = false);
+                          bool isActiveGen = false);
   /** is e an enumerator registered with this class? */
   bool isEnumerator(Node e) const;
   /** return the conjecture e is associated with */
@@ -298,6 +300,8 @@ class TermDbSygus {
   std::map<Node, TypeNode> d_sb_lemma_to_type;
   /** mapping from symmetry breaking lemmas to size */
   std::map<Node, unsigned> d_sb_lemma_to_size;
+  /** enumerators to whether they are actively-generated */
+  std::map<Node, bool> d_enum_active_gen;
   /** enumerators to whether they are variable agnostic */
   std::map<Node, bool> d_enum_var_agnostic;
   //------------------------------end enumerators