Add actively generated sygus enumerators (#2552)

13 files changed, 538 insertions, 161 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 7b58f955a..e8d8fbe3d 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1032,6 +1032,14 @@ header = "options/quantifiers_options.h"
   help       = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
 
 [[option]]
+  name       = "sygusEnumVarAgnostic"
+  category   = "regular"
+  long       = "sygus-var-agnostic"
+  type       = "bool"
+  default    = "false"
+  help       = "when possible, use variable-agnostic enumerators"
+
+[[option]]
   name       = "sygusMinGrammar"
   category   = "regular"
   long       = "sygus-min-grammar"
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 227bd6170..0db05d93c 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -556,22 +556,40 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
       << "Simple symmetry breaking for " << dt.getName() << ", constructor "
       << dt[tindex].getName() << ", at depth " << depth << std::endl;
 
-  // if we are the "any constant" constructor, we do no symmetry breaking
-  // only do simple symmetry breaking up to depth 2
+  // get the sygus operator
   Node sop = Node::fromExpr(dt[tindex].getSygusOp());
-  if (sop.getAttribute(SygusAnyConstAttribute()) || depth > 2)
-  {
-    d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = Node::null();
-    return Node::null();
-  }
+  // get the kind of the constructor operator
+  Kind nk = d_tds->getConsNumKind(tn, tindex);
+  // is this the any-constant constructor?
+  bool isAnyConstant = sop.getAttribute(SygusAnyConstAttribute());
+
   // conjunctive conclusion of lemma
   std::vector<Node> sbp_conj;
 
+  // the number of (sygus) arguments
+  // Notice if this is an any-constant constructor, its child is not a
+  // sygus child, hence we set to 0 here.
+  unsigned dt_index_nargs = isAnyConstant ? 0 : dt[tindex].getNumArgs();
+
+  // builtin type
+  TypeNode tnb = TypeNode::fromType(dt.getSygusType());
+  // get children
+  std::vector<Node> children;
+  for (unsigned j = 0; j < dt_index_nargs; j++)
+  {
+    Node sel = nm->mkNode(
+        APPLY_SELECTOR_TOTAL,
+        Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)),
+        n);
+    Assert(sel.getType().isDatatype());
+    children.push_back(sel);
+  }
+
   if (depth == 0)
   {
     Trace("sygus-sb-simple-debug") << "  Size..." << std::endl;
     // fairness
-    if (options::sygusFair() == SYGUS_FAIR_DT_SIZE)
+    if (options::sygusFair() == SYGUS_FAIR_DT_SIZE && !isAnyConstant)
     {
       Node szl = nm->mkNode(DT_SIZE, n);
       Node szr =
@@ -579,48 +597,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
       szr = Rewriter::rewrite(szr);
       sbp_conj.push_back(szl.eqNode(szr));
     }
-  }
-
-  // symmetry breaking
-  Kind nk = d_tds->getConsNumKind(tn, tindex);
-  if (options::sygusSymBreak())
-  {
-    // the number of (sygus) arguments
-    unsigned dt_index_nargs = dt[tindex].getNumArgs();
-
-    // builtin type
-    TypeNode tnb = TypeNode::fromType(dt.getSygusType());
-    // get children
-    std::vector<Node> children;
-    for (unsigned j = 0; j < dt_index_nargs; j++)
-    {
-      Node sel = nm->mkNode(
-          APPLY_SELECTOR_TOTAL,
-          Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)),
-          n);
-      Assert(sel.getType().isDatatype());
-      children.push_back(sel);
-    }
-
-    // direct solving for children
-    //   for instance, we may want to insist that the LHS of MINUS is 0
-    Trace("sygus-sb-simple-debug") << "  Solve children..." << std::endl;
-    std::map<unsigned, unsigned> children_solved;
-    for (unsigned j = 0; j < dt_index_nargs; j++)
-    {
-      int i = d_ssb.solveForArgument(tn, tindex, j);
-      if (i >= 0)
-      {
-        children_solved[j] = i;
-        TypeNode ctn = children[j].getType();
-        const Datatype& cdt =
-            static_cast<DatatypeType>(ctn.toType()).getDatatype();
-        Assert(i < static_cast<int>(cdt.getNumConstructors()));
-        sbp_conj.push_back(DatatypesRewriter::mkTester(children[j], i, cdt));
-      }
-    }
-
-    if (isVarAgnostic && depth == 0)
+    if (isVarAgnostic)
     {
       // Enforce symmetry breaking lemma template for each x_i:
       // template z.
@@ -695,6 +672,36 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
         sbp_conj.push_back(finish.eqNode(prev));
       }
     }
+  }
+
+  // if we are the "any constant" constructor, we do no symmetry breaking
+  // only do simple symmetry breaking up to depth 2
+  bool doSymBreak = options::sygusSymBreak();
+  if (isAnyConstant || depth > 2)
+  {
+    doSymBreak = false;
+  }
+  // symmetry breaking
+  if (doSymBreak)
+  {
+    // direct solving for children
+    //   for instance, we may want to insist that the LHS of MINUS is 0
+    Trace("sygus-sb-simple-debug") << "  Solve children..." << std::endl;
+    std::map<unsigned, unsigned> children_solved;
+    for (unsigned j = 0; j < dt_index_nargs; j++)
+    {
+      int i = d_ssb.solveForArgument(tn, tindex, j);
+      if (i >= 0)
+      {
+        children_solved[j] = i;
+        TypeNode ctn = children[j].getType();
+        const Datatype& cdt =
+            static_cast<DatatypeType>(ctn.toType()).getDatatype();
+        Assert(i < static_cast<int>(cdt.getNumConstructors()));
+        sbp_conj.push_back(DatatypesRewriter::mkTester(children[j], i, cdt));
+      }
+    }
+
     // depth 1 symmetry breaking : talks about direct children
     if (depth == 1)
     {
@@ -947,8 +954,13 @@ void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool
   }
 }
 
-Node SygusSymBreakNew::registerSearchValue(
-    Node a, Node n, Node nv, unsigned d, std::vector<Node>& lemmas)
+Node SygusSymBreakNew::registerSearchValue(Node a,
+                                           Node n,
+                                           Node nv,
+                                           unsigned d,
+                                           std::vector<Node>& lemmas,
+                                           bool isVarAgnostic,
+                                           bool doSym)
 {
   Assert(n.getType().isComparableTo(nv.getType()));
   TypeNode tn = n.getType();
@@ -979,7 +991,13 @@ Node SygusSymBreakNew::registerSearchValue(
           APPLY_SELECTOR_TOTAL,
           Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
           n);
-      Node nvc = registerSearchValue(a, sel, nv[i], d + 1, lemmas);
+      Node nvc = registerSearchValue(a,
+                                     sel,
+                                     nv[i],
+                                     d + 1,
+                                     lemmas,
+                                     isVarAgnostic,
+                                     doSym && (!isVarAgnostic || i == 0));
       if (nvc.isNull())
       {
         return Node::null();
@@ -993,6 +1011,10 @@ Node SygusSymBreakNew::registerSearchValue(
       nv = nm->mkNode(APPLY_CONSTRUCTOR, rcons_children);
     }
   }
+  if (!doSym)
+  {
+    return nv;
+  }
   Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl;
   std::map<TypeNode, int> var_count;
   Node cnv = d_tds->canonizeBuiltin(nv, var_count);
@@ -1127,11 +1149,22 @@ Node SygusSymBreakNew::registerSearchValue(
         Node bad_val_o = d_cache[a].d_search_val[tn][bad_val_bvr];
         Assert( d_cache[a].d_search_val_sz[tn].find( bad_val_bvr )!=d_cache[a].d_search_val_sz[tn].end() );
         unsigned prev_sz = d_cache[a].d_search_val_sz[tn][bad_val_bvr];
-        if( prev_sz>sz ){
+        bool doFlip = (prev_sz > sz);
+        if (doFlip)
+        {
           //swap : the excluded value is the previous
           d_cache[a].d_search_val_sz[tn][bad_val_bvr] = sz;
           bad_val = d_cache[a].d_search_val[tn][bad_val_bvr];
           bad_val_o = nv;
+          if (Trace.isOn("sygus-sb-exc"))
+          {
+            Trace("sygus-sb-exc") << "Flip : exclude ";
+            quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val);
+            Trace("sygus-sb-exc") << " instead of ";
+            quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val_o);
+            Trace("sygus-sb-exc") << ", since its size is " << sz << " < "
+                                  << prev_sz << std::endl;
+          }
           sz = prev_sz;
         }
         if( Trace.isOn("sygus-sb-exc") ){
@@ -1154,7 +1187,14 @@ Node SygusSymBreakNew::registerSearchValue(
             a, bad_val, eset, bad_val_o, var_count, lemmas);
 
         // other generalization criteria go here
-        return Node::null();
+
+        // If the exclusion was flipped, we are excluding a previous value
+        // instead of the current one. Hence, the current value is a legal
+        // value that we will consider.
+        if (!doFlip)
+        {
+          return Node::null();
+        }
       }
     }
   }
@@ -1538,8 +1578,10 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
         Trace("dt-sygus") << ss.str() << std::endl;
       }
       // first check that the value progv for prog is what we expected
+      bool isExc = true;
       if (checkValue(prog, progv, 0, lemmas))
       {
+        isExc = false;
         //debugging : ensure fairness was properly handled
         if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){  
           Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog );
@@ -1552,20 +1594,23 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
             Node szlem = NodeManager::currentNM()->mkNode( kind::OR, prog.eqNode( progv ).negate(),
                                                                      prog_sz.eqNode( progv_sz ) );
             Trace("sygus-sb-warn") << "SygusSymBreak : WARNING : adding size correction : " << szlem << std::endl;
-            lemmas.push_back( szlem );                                                     
-            return;
+            lemmas.push_back(szlem);
+            isExc = true;
           }
         }
-        
-        // register the search value ( prog -> progv ), this may invoke symmetry breaking 
-        if( options::sygusSymBreakDynamic() ){
+
+        // register the search value ( prog -> progv ), this may invoke symmetry
+        // breaking
+        if (!isExc && options::sygusSymBreakDynamic())
+        {
+          bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog);
           // check that it is unique up to theory-specific rewriting and
           // conjecture-specific symmetry breaking.
-          Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas);
-          SygusSymBreakExcAttribute ssbea;
-          prog.setAttribute(ssbea, rsv.isNull());
+          Node rsv = registerSearchValue(
+              prog, prog, progv, 0, lemmas, isVarAgnostic, true);
           if (rsv.isNull())
           {
+            isExc = true;
             Trace("sygus-sb") << "  SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
           }
           else
@@ -1574,6 +1619,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
           }
         }
       }
+      SygusSymBreakExcAttribute ssbea;
+      prog.setAttribute(ssbea, isExc);
     }
   }
   //register any measured terms that we haven't encountered yet (should only be invoked on first call to check
@@ -1584,9 +1631,10 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
     registerSizeTerm( mts[i], lemmas );
   }
   Trace("sygus-sb") << " SygusSymBreakNew::check: finished." << std::endl;
-  
-  if( Trace.isOn("cegqi-engine") ){
-    if (lemmas.empty() && !d_szinfo.empty())
+
+  if (Trace.isOn("cegqi-engine") && !d_szinfo.empty())
+  {
+    if (lemmas.empty())
     {
       Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
       for (std::pair<const Node, std::unique_ptr<SygusSizeDecisionStrategy>>&
@@ -1597,6 +1645,15 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
       }
       Trace("cegqi-engine") << std::endl;
     }
+    else
+    {
+      Trace("cegqi-engine")
+          << "*** Sygus : produced symmetry breaking lemmas" << std::endl;
+      for (const Node& lem : lemmas)
+      {
+        Trace("cegqi-engine-debug") << "  " << lem << std::endl;
+      }
+    }
   }
 }
 
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index a38e7c5b8..6cf1d7d37 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -370,9 +370,29 @@ private:
    * not "some constant". Thus, we should consider the subterm
    * C_{any_constant}( 5 ) above to be an unconstrained variable (as represented
    * by a selector chain), instead of the concrete value 5.
-   */
-  Node registerSearchValue(
-      Node a, Node n, Node nv, unsigned d, std::vector<Node>& lemmas);
+   *
+   * The flag isVarAgnostic is whether "a" is a variable agnostic enumerator. If
+   * this is the case, we restrict symmetry breaking to subterms of n on its
+   * leftmost subchain. For example, consider the grammar:
+   *   A -> B=B
+   *   B -> B+B | x | y | 0
+   * Say we are registering the search value x = y+x. Notice that this value is
+   * ordered. If a were a variable-agnostic enumerator of type A in this
+   * case, we would only register x = y+x and x, and not y+x or y, since the
+   * latter two terms are not leftmost subterms in this value. If we did on the
+   * other hand register y+x, we would be prevented from solutions like x+y = 0
+   * later, since x+y is equivalent to (the already registered value) y+x.
+   *
+   * If doSym is false, we are not performing symmetry breaking on n. This flag
+   * is set to false on branches of n that are not leftmost.
+   */
+  Node registerSearchValue(Node a,
+                           Node n,
+                           Node nv,
+                           unsigned d,
+                           std::vector<Node>& lemmas,
+                           bool isVarAgnostic,
+                           bool doSym);
   /** Register symmetry breaking lemma
    *
    * This function adds the symmetry breaking lemma template lem for terms of
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 10328c653..6aed1514c 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -453,6 +453,8 @@ bool TheoryDatatypes::doSendLemma( Node lem ) {
     d_addedLemma = true;
     return true;
   }else{
+    Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : duplicate : "
+                           << lem << std::endl;
     return false;
   }
 }
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index db9af10b4..9706e3732 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -68,8 +68,19 @@ bool Cegis::processInitialize(Node n,
                               std::vector<Node>& lemmas)
 {
   Trace("cegis") << "Initialize cegis..." << std::endl;
+  unsigned csize = candidates.size();
+  // We only can use actively-generated enumerators if there is only one
+  // function-to-synthesize. Otherwise, we would have to generate a "product" of
+  // two actively-generated enumerators. That is, given a conjecture with two
+  // functions-to-synthesize with enumerators e_f and e_g, if:
+  // e_f -> t1, ..., tn
+  // e_g -> s1, ..., sm
+  // 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;
   // initialize an enumerator for each candidate
-  for (unsigned i = 0; i < candidates.size(); i++)
+  for (unsigned i = 0; i < csize; i++)
   {
     Trace("cegis") << "...register enumerator " << candidates[i];
     bool do_repair_const = false;
@@ -86,8 +97,13 @@ bool Cegis::processInitialize(Node n,
       }
     }
     Trace("cegis") << std::endl;
-    d_tds->registerEnumerator(
-        candidates[i], candidates[i], d_parent, false, do_repair_const);
+    // variable agnostic enumerators require an active guard
+    d_tds->registerEnumerator(candidates[i],
+                              candidates[i],
+                              d_parent,
+                              isVarAgnostic,
+                              do_repair_const,
+                              isVarAgnostic);
   }
   return true;
 }
@@ -99,7 +115,8 @@ void Cegis::getTermList(const std::vector<Node>& candidates,
 }
 
 bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
-                          const std::vector<Node>& candidate_values)
+                          const std::vector<Node>& candidate_values,
+                          std::vector<Node>& lems)
 {
   // First, decide if this call will apply "conjecture-specific refinement".
   // In other words, in some settings, the following method will identify and
@@ -144,13 +161,14 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
     }
     if (!cre_lems.empty())
     {
-      for (const Node& lem : cre_lems)
+      lems.insert(lems.end(), cre_lems.begin(), cre_lems.end());
+      addedEvalLemmas = true;
+      if (Trace.isOn("cegqi-lemma"))
       {
-        if (d_qe->addLemma(lem))
+        for (const Node& lem : cre_lems)
         {
           Trace("cegqi-lemma")
               << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
-          addedEvalLemmas = true;
         }
       }
       /* we could, but do not return here. experimentally, it is better to
@@ -178,12 +196,9 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
     {
       Node lem = nm->mkNode(
           OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
-      if (d_qe->addLemma(lem))
-      {
-        Trace("cegqi-lemma")
-            << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl;
-        addedEvalLemmas = true;
-      }
+      lems.push_back(lem);
+      Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
+                           << std::endl;
     }
   }
   return addedEvalLemmas;
@@ -258,7 +273,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
   }
 
   // evaluate on refinement lemmas
-  bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
+  bool addedEvalLemmas = addEvalLemmas(enums, enum_values, lems);
 
   // try to construct candidates
   if (!processConstructCandidates(enums,
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 7387bd468..849a39639 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -137,18 +137,39 @@ class Cegis : public SygusModule
 
   /** evaluates candidate values on current refinement lemmas
    *
-   * Returns true if refinement lemmas are added after evaluation, false
-   * otherwise.
+   * This method performs techniques that ensure that
+   * { candidates -> candidate_values } is a candidate solution that should
+   * be checked by the solution verifier of the CEGIS loop. This method
+   * invokes two sub-methods which may reject the current solution.
+   * The first is "refinement evaluation", described above the method
+   * getRefinementEvalLemmas below. The second is "evaluation unfolding",
+   * which eagerly unfolds applications of evaluation functions (see
+   * sygus_eval_unfold.h for details).
    *
-   * Also eagerly unfolds evaluation functions in a heuristic manner, which is
-   * useful e.g. for boolean connectives
+   * If this method returns true, then { candidates -> candidate_values }
+   * is not ready to be tried as a candidate solution. In this case, it may add
+   * lemmas to lems.
+   *
+   * Notice that this method may return true without adding any lemmas to
+   * lems, in the case that terms from candidates are "actively-generated
+   * enumerators", since the model values of such terms are managed
+   * explicitly within getEnumeratedValue. In this case, the owner of the
+   * actively-generated enumerators (e.g. SynthConjecture) is responsible for
+   * blocking the current value of candidates.
    */
   bool addEvalLemmas(const std::vector<Node>& candidates,
-                     const std::vector<Node>& candidate_values);
+                     const std::vector<Node>& candidate_values,
+                     std::vector<Node>& lems);
   //-----------------------------------end refinement lemmas
 
   /** Get refinement evaluation lemmas
    *
+   * This method performs "refinement evaluation", that is, it tests
+   * whether the current solution, given by { candidates -> candidate_values },
+   * satisfies all current refinement lemmas. If it does not, it may add
+   * blocking lemmas L to lems which exclude (a generalization of) the current
+   * solution.
+   *
    * Given a candidate solution ms for candidates vs, this function adds lemmas
    * to lems based on evaluating the conjecture, instantiated for ms, on lemmas
    * for previous refinements (d_refinement_lemmas).
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index d71139eef..fc26d72f6 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -600,10 +600,20 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
   }
   // register the enumerator
   si.d_enums[index].push_back(e);
+  bool mkActiveGuard = false;
+  bool isVarAgnostic = 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();
+  }
   Trace("cegis-unif-enum") << "* Registering new enumerator " << e
                            << " to strategy point " << si.d_pt << "\n";
   d_tds->registerEnumerator(
-      e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1);
+      e, si.d_pt, d_parent, mkActiveGuard, false, isVarAgnostic);
 }
 
 void CegisUnifEnumDecisionStrategy::registerEvalPts(
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index b307876ed..bf939e0fe 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -597,6 +597,9 @@ bool EnumStreamSubstitution::CombinationState::getNextCombination()
   return new_comb;
 }
 
+void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); }
+void EnumStreamConcrete::addValue(Node v) { d_ess.resetValue(v); }
+Node EnumStreamConcrete::getNext() { return d_ess.getNext(); }
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h
index 5d3daa538..38fa0627b 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.h
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h
@@ -274,6 +274,26 @@ class EnumStreamSubstitution
   unsigned d_curr_ind;
 };
 
+/**
+ * An enumerated value generator based on the above class. This is
+ * SynthConjecture's interface to using the above utility.
+ */
+class EnumStreamConcrete : public EnumValGenerator
+{
+ public:
+  EnumStreamConcrete(quantifiers::TermDbSygus* tds) : d_ess(tds) {}
+  /** initialize this class with enumerator e */
+  void initialize(Node e) override;
+  /** get that value v was enumerated */
+  void addValue(Node v) override;
+  /** get the next value enumerated by this class */
+  Node getNext() override;
+
+ private:
+  /** stream substitution utility */
+  EnumStreamSubstitution d_ess;
+};
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index b7e6e0c65..889f4d9c9 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -179,6 +179,7 @@ bool SygusPbe::initialize(Node n,
       return false;
     }
   }
+  bool isVarAgnostic = options::sygusEnumVarAgnostic();
   for (const Node& c : candidates)
   {
     Assert(d_examples.find(c) != d_examples.end());
@@ -202,7 +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);
+      d_tds->registerEnumerator(e, c, d_parent, true, false, isVarAgnostic);
       Node g = d_tds->getActiveGuardForEnumerator(e);
       d_enum_to_active_guard[e] = g;
       d_enum_to_candidate[e] = c;
@@ -357,6 +358,12 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
 {
   Assert(isPbe());
   Assert(!e.isNull());
+  if (!d_tds->isPassiveEnumerator(e))
+  {
+    // we cannot apply conjecture-specific symmetry breaking on enumerators that
+    // are not passive
+    return Node::null();
+  }
   e = d_tds->getSynthFunForEnumerator(e);
   Assert(!e.isNull());
   std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 99f1131fe..4dfe33b58 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -27,6 +27,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/enum_stream_substitution.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -290,7 +291,21 @@ void SynthConjecture::doCheck(std::vector<Node>& lems)
       return;
     }
   }
+  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);
@@ -318,16 +333,16 @@ void SynthConjecture::doCheck(std::vector<Node>& lems)
         Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
         fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
       }
-      if (Trace.isOn("cegqi-check"))
+      if (Trace.isOn("cegqi-engine"))
       {
-        Trace("cegqi-check") << "CegConjuncture : repair previous solution ";
+        Trace("cegqi-engine") << "CegConjuncture : repair previous solution ";
         for (const Node& fc : fail_cvs)
         {
           std::stringstream ss;
           Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc);
-          Trace("cegqi-check") << ss.str() << " ";
+          Trace("cegqi-engine") << ss.str() << " ";
         }
-        Trace("cegqi-check") << std::endl;
+        Trace("cegqi-engine") << std::endl;
       }
       d_repair_index++;
       if (d_sygus_rconst->repairSolution(
@@ -338,19 +353,62 @@ void 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);
-
-  // if the master requires a full model and the model is partial, we fail
-  if (!d_master->allowPartialModel() && !fullModel)
-  {
-    Trace("cegqi-check") << "...partial model, fail." << std::endl;
-    return;
-  }
-
   if (!constructed_cand)
   {
+    // get the model value of the relevant terms from the master module
+    std::vector<Node> enum_values;
+    bool fullModel = getEnumeratedValues(terms, enum_values);
+
+    // 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 false;
+    }
+    // the waiting values are passed to the module below, clear
+    d_ev_active_gen_waiting.clear();
+
+    // debug print
+    Assert(terms.size() == enum_values.size());
+    bool emptyModel = true;
+    Trace("cegqi-engine") << "  * Value is : ";
+    for (unsigned i = 0, size = terms.size(); i < size; i++)
+    {
+      Node nv = enum_values[i];
+      if (!nv.isNull())
+      {
+        emptyModel = false;
+      }
+      if (Trace.isOn("cegqi-engine"))
+      {
+        Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv;
+        TypeNode tn = onv.getType();
+        std::stringstream ss;
+        Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
+        Trace("cegqi-engine") << terms[i] << " -> ";
+        if (nv.isNull())
+        {
+          Trace("cegqi-engine") << "[EXC: " << ss.str() << "] ";
+        }
+        else
+        {
+          Trace("cegqi-engine") << ss.str() << " ";
+          if (Trace.isOn("cegqi-engine-rr"))
+          {
+            Node bv = d_tds->sygusToBuiltin(nv, tn);
+            bv = Rewriter::rewrite(bv);
+            Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+          }
+        }
+      }
+    }
+    Trace("cegqi-engine") << std::endl;
+    if (emptyModel)
+    {
+      Trace("cegqi-engine") << "...empty model, fail." << std::endl;
+      return false;
+    }
     Assert(candidate_values.empty());
     constructed_cand = d_master->constructCandidates(
         terms, enum_values, d_candidates, candidate_values, lems);
@@ -396,7 +454,7 @@ void SynthConjecture::doCheck(std::vector<Node>& lems)
       lem = getStreamGuardedLemma(lem);
       lems.push_back(lem);
       recordInstantiation(candidate_values);
-      return;
+      return true;
     }
     Assert(!d_set_ce_sk_vars);
   }
@@ -404,7 +462,7 @@ void SynthConjecture::doCheck(std::vector<Node>& lems)
   {
     if (!constructed_cand)
     {
-      return;
+      return true;
     }
   }
 
@@ -444,7 +502,7 @@ void SynthConjecture::doCheck(std::vector<Node>& lems)
   if (lem.isNull())
   {
     // no lemma to check
-    return;
+    return true;
   }
 
   lem = Rewriter::rewrite(lem);
@@ -499,7 +557,7 @@ void SynthConjecture::doCheck(std::vector<Node>& lems)
         Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
         Assert(squery.isConst() && squery.getConst<bool>());
 #endif
-        return;
+        return true;
       }
       else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
@@ -519,10 +577,11 @@ void SynthConjecture::doCheck(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;
+    return true;
   }
   lem = getStreamGuardedLemma(lem);
   lems.push_back(lem);
+  return true;
 }
 
 void SynthConjecture::doRefine(std::vector<Node>& lems)
@@ -604,36 +663,12 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
                                           std::vector<Node>& v)
 {
   bool ret = true;
-  Trace("cegqi-engine") << "  * Value is : ";
   for (unsigned i = 0; i < n.size(); i++)
   {
     Node nv = getEnumeratedValue(n[i]);
     v.push_back(nv);
     ret = ret && !nv.isNull();
-    if (Trace.isOn("cegqi-engine"))
-    {
-      Node onv = nv.isNull() ? d_qe->getModel()->getValue(n[i]) : nv;
-      TypeNode tn = onv.getType();
-      std::stringstream ss;
-      Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
-      Trace("cegqi-engine") << n[i] << " -> ";
-      if (nv.isNull())
-      {
-        Trace("cegqi-engine") << "[EXC: " << ss.str() << "] ";
-      }
-      else
-      {
-        Trace("cegqi-engine") << ss.str() << " ";
-        if (Trace.isOn("cegqi-engine-rr"))
-        {
-          Node bv = d_tds->sygusToBuiltin(nv, tn);
-          bv = Rewriter::rewrite(bv);
-          Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
-        }
-      }
-    }
   }
-  Trace("cegqi-engine") << std::endl;
   return ret;
 }
 
@@ -646,13 +681,105 @@ Node SynthConjecture::getEnumeratedValue(Node e)
     // return null.
     return Node::null();
   }
-  if (d_tds->isPassiveEnumerator(e))
+
+  if (!d_tds->isEnumerator(e) || d_tds->isPassiveEnumerator(e))
   {
     return getModelValue(e);
   }
-  Assert(false);
   // management of actively generated enumerators goes here
-  return getModelValue(e);
+
+  // initialize the enumerated value generator for e
+  std::map<Node, std::unique_ptr<EnumValGenerator> >::iterator iteg =
+      d_evg.find(e);
+  if (iteg == d_evg.end())
+  {
+    d_evg[e].reset(new EnumStreamConcrete(d_tds));
+    Trace("sygus-active-gen")
+        << "Active-gen: initialize for " << e << std::endl;
+    d_evg[e]->initialize(e);
+    d_ev_curr_active_gen[e] = Node::null();
+    iteg = d_evg.find(e);
+    Trace("sygus-active-gen-debug") << "...finish" << std::endl;
+  }
+  // if we have a waiting value, return it
+  std::map<Node, Node>::iterator itw = d_ev_active_gen_waiting.find(e);
+  if (itw != d_ev_active_gen_waiting.end())
+  {
+    Trace("sygus-active-gen-debug")
+        << "Active-gen: return waiting " << itw->second << std::endl;
+    return itw->second;
+  }
+  // Check if there is an (abstract) value absE we were actively generating
+  // values based on.
+  Node absE = d_ev_curr_active_gen[e];
+  if (absE.isNull())
+  {
+    // None currently exist. The next abstract value is the model value for e.
+    absE = getModelValue(e);
+    if (Trace.isOn("sygus-active-gen"))
+    {
+      Trace("sygus-active-gen") << "Active-gen: new abstract value : ";
+      TermDbSygus::toStreamSygus("sygus-active-gen", e);
+      Trace("sygus-active-gen") << " -> ";
+      TermDbSygus::toStreamSygus("sygus-active-gen", absE);
+      Trace("sygus-active-gen") << std::endl;
+    }
+    d_ev_curr_active_gen[e] = absE;
+    iteg->second->addValue(absE);
+  }
+  Node v = iteg->second->getNext();
+  if (v.isNull())
+  {
+    // No more concrete values generated from absE.
+    NodeManager* nm = NodeManager::currentNM();
+    d_ev_curr_active_gen[e] = Node::null();
+    // We must block e = absE.
+    std::vector<Node> exp;
+    d_tds->getExplain()->getExplanationForEquality(e, absE, exp);
+    for (unsigned i = 0, size = exp.size(); i < size; i++)
+    {
+      exp[i] = exp[i].negate();
+    }
+    Node g = d_tds->getActiveGuardForEnumerator(e);
+    if (!g.isNull())
+    {
+      if (d_ev_active_gen_first_val.find(e) == d_ev_active_gen_first_val.end())
+      {
+        exp.push_back(g.negate());
+        d_ev_active_gen_first_val[e] = absE;
+      }
+    }
+    else
+    {
+      Assert(false);
+    }
+    Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp);
+    Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator "
+                            "exclude current solution : "
+                         << lem << std::endl;
+    if (Trace.isOn("sygus-active-gen-debug"))
+    {
+      Trace("sygus-active-gen-debug") << "Active-gen: block ";
+      TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
+      Trace("sygus-active-gen-debug") << std::endl;
+    }
+    d_qe->getOutputChannel().lemma(lem);
+  }
+  else
+  {
+    // We are waiting to send e -> v to the module that requested it.
+    d_ev_active_gen_waiting[e] = v;
+    if (Trace.isOn("sygus-active-gen"))
+    {
+      Trace("sygus-active-gen") << "Active-gen : " << e << " : ";
+      TermDbSygus::toStreamSygus("sygus-active-gen", absE);
+      Trace("sygus-active-gen") << " -> ";
+      TermDbSygus::toStreamSygus("sygus-active-gen", v);
+      Trace("sygus-active-gen") << std::endl;
+    }
+  }
+
+  return v;
 }
 
 Node SynthConjecture::getModelValue(Node n)
@@ -724,28 +851,35 @@ void SynthConjecture::printAndContinueStream()
   d_ce_sk_vars.clear();
   d_ce_sk_var_mvs.clear();
   // However, we need to exclude the current solution using an explicit
-  // blocking clause, so that we proceed to the next solution.
+  // blocking clause, so that we proceed to the next solution. We do this only
+  // for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
   std::vector<Node> terms;
   d_master->getTermList(d_candidates, terms);
   std::vector<Node> exp;
   for (const Node& cprog : terms)
   {
-    Node sol = cprog;
-    if (!d_cinfo[cprog].d_inst.empty())
+    Assert(d_tds->isEnumerator(cprog));
+    if (d_tds->isPassiveEnumerator(cprog))
     {
-      sol = d_cinfo[cprog].d_inst.back();
-      // add to explanation of exclusion
-      d_tds->getExplain()->getExplanationForEquality(cprog, sol, exp);
+      Node sol = cprog;
+      if (!d_cinfo[cprog].d_inst.empty())
+      {
+        sol = d_cinfo[cprog].d_inst.back();
+        // add to explanation of exclusion
+        d_tds->getExplain()->getExplanationForEquality(cprog, sol, exp);
+      }
     }
   }
-  Assert(!exp.empty());
-  Node exc_lem = exp.size() == 1
-                     ? exp[0]
-                     : NodeManager::currentNM()->mkNode(kind::AND, exp);
-  exc_lem = exc_lem.negate();
-  Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : "
-                       << exc_lem << std::endl;
-  d_qe->getOutputChannel().lemma(exc_lem);
+  if (!exp.empty())
+  {
+    Node exc_lem = exp.size() == 1
+                       ? exp[0]
+                       : NodeManager::currentNM()->mkNode(kind::AND, exp);
+    exc_lem = exc_lem.negate();
+    Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : "
+                         << exc_lem << std::endl;
+    d_qe->getOutputChannel().lemma(exc_lem);
+  }
 }
 
 void SynthConjecture::printSynthSolution(std::ostream& out,
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 694e4a0cb..4c18205af 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -35,6 +35,24 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+/**
+ * A base class for generating values for actively-generated enumerators.
+ * At a high level, the job of this class is to accept a stream of "abstract
+ * values" a1, ..., an, ..., and generate a (possibly larger) stream of
+ * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, ....
+ */
+class EnumValGenerator
+{
+ public:
+  virtual ~EnumValGenerator() {}
+  /** initialize this class with enumerator e */
+  virtual void initialize(Node e) = 0;
+  /** Inform this generator that abstract value v was enumerated. */
+  virtual void addValue(Node v) = 0;
+  /** Get the next concrete value generated by this class. */
+  virtual Node getNext() = 0;
+};
+
 /** a synthesis conjecture
  * This class implements approaches for a synthesis conecjture, given by data
  * member d_quant.
@@ -113,16 +131,6 @@ class SynthConjecture
   /** has a conjecture been assigned to this class */
   bool isAssigned() { return !d_embed_quant.isNull(); }
   /**
-   * 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.
-   */
-  bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v);
-  /**
-   * Get model value for term n. If n has a value that was excluded by
-   * datatypes sygus symmetry breaking, this method returns null.
-   */
-  Node getEnumeratedValue(Node n);
-  /**
    * Get model value for term n.
    */
   Node getModelValue(Node n);
@@ -174,6 +182,47 @@ class SynthConjecture
   SygusModule* d_master;
   //------------------------end modules
 
+  //------------------------enumerators
+  /**
+   * 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.
+   */
+  bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v);
+  /**
+   * Get model value for term n. If n has a value that was excluded by
+   * datatypes sygus symmetry breaking, this method returns null.
+   */
+  Node getEnumeratedValue(Node n);
+  /** enumerator generators for each actively-generated enumerator */
+  std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg;
+  /**
+   * Map from enumerators to whether they are currently being
+   * "actively-generated". That is, we are in a state where we have called
+   * d_evg[e].addValue(v) for some v, and d_evg[e].getNext() has not yet
+   * returned null. The range of this map stores the abstract value that
+   * we are currently generating values from.
+   */
+  std::map<Node, Node> d_ev_curr_active_gen;
+  /** the current waiting value of each actively-generated enumerator, if any
+   *
+   * This caches values that are actively generated and that we have not yet
+   * passed to a call to SygusModule::constructCandidates. An example of when
+   * this may occur is when there are two actively-generated enumerators e1 and
+   * e2. Say on some iteration we actively-generate v1 for e1, the value
+   * of e2 was excluded by symmetry breaking, and say the current master sygus
+   * module does not handle partial models. Hence, we abort the current check.
+   * We remember that the value of e1 was v1 by storing it here, so that on
+   * a future check when v2 has a proper value, it is returned.
+   */
+  std::map<Node, Node> d_ev_active_gen_waiting;
+  /** the first value enumerated for each actively-generated enumerator
+   *
+   * This is to implement an optimization that only guards the blocking lemma
+   * for the first value of an actively-generated enumerator.
+   */
+  std::map<Node, Node> d_ev_active_gen_first_val;
+  //------------------------end enumerators
+
   /** list of constants for quantified formula
    * The outer Skolems for the negation of d_embed_quant.
    */
@@ -237,6 +286,18 @@ 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
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 23b35cfed..1a8c81bcc 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -589,6 +589,25 @@ void TermDbSygus::registerEnumerator(Node e,
         d_var_subclass_list[et][sc].push_back(v);
       }
     }
+    // If no subclass has more than one variable, do not use variable agnostic
+    // enumeration
+    bool useVarAgnostic = false;
+    for (std::pair<const unsigned, std::vector<Node> >& p :
+         d_var_subclass_list[et])
+    {
+      if (p.second.size() > 1)
+      {
+        useVarAgnostic = true;
+      }
+    }
+    if (!useVarAgnostic)
+    {
+      Trace("sygus-db")
+          << "...disabling variable agnostic for " << e
+          << " since it has no subclass with more than one variable."
+          << std::endl;
+      d_enum_var_agnostic[e] = false;
+    }
   }
 }