Merge branch 'master' into docsLinkdocsLink

18 files changed, 367 insertions, 83 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 28788a5ea..544bdcc5c 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -19,6 +19,7 @@
 #include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -205,8 +206,8 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
             if (curr_val < prev_val)
             {
               // must have the same size
-              unsigned prev_size = d_tds->getSygusTermSize(prev_val);
-              unsigned curr_size = d_tds->getSygusTermSize(curr_val);
+              unsigned prev_size = datatypes::utils::getSygusTermSize(prev_val);
+              unsigned curr_size = datatypes::utils::getSygusTermSize(curr_val);
               Assert(prev_size <= curr_size);
               if (curr_size == prev_size)
               {
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 3ae34d82c..f853ac8e8 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 #include <numeric>  // for std::iota
+#include <sstream>
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h
index ea028991b..05c693ace 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.h
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h
@@ -19,12 +19,14 @@
 #define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
 
 #include "expr/node.h"
-#include "theory/quantifiers/sygus/synth_conjecture.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
 
 namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
+class TermDbSygus;
+
 /** Streamer of different values according to variable permutations
  *
  * Generates a new value (modulo rewriting) when queried in which its variables
@@ -33,7 +35,7 @@ namespace quantifiers {
 class EnumStreamPermutation
 {
  public:
-  EnumStreamPermutation(quantifiers::TermDbSygus* tds);
+  EnumStreamPermutation(TermDbSygus* tds);
   ~EnumStreamPermutation() {}
   /** resets utility
    *
@@ -70,7 +72,7 @@ class EnumStreamPermutation
 
  private:
   /** sygus term database of current quantifiers engine */
-  quantifiers::TermDbSygus* d_tds;
+  TermDbSygus* d_tds;
   /** maps subclass ids to subset of d_vars with that subclass id */
   std::map<unsigned, std::vector<Node>> d_var_classes;
   /** maps variables to subfield types with constructors for
@@ -165,7 +167,7 @@ class EnumStreamPermutation
 class EnumStreamSubstitution
 {
  public:
-  EnumStreamSubstitution(quantifiers::TermDbSygus* tds);
+  EnumStreamSubstitution(TermDbSygus* tds);
   ~EnumStreamSubstitution() {}
   /** initializes utility
    *
@@ -211,7 +213,7 @@ class EnumStreamSubstitution
 
  private:
   /** sygus term database of current quantifiers engine */
-  quantifiers::TermDbSygus* d_tds;
+  TermDbSygus* d_tds;
   /** type this utility has been initialized for */
   TypeNode d_tn;
   /** current value */
@@ -281,7 +283,7 @@ class EnumStreamSubstitution
 class EnumStreamConcrete : public EnumValGenerator
 {
  public:
-  EnumStreamConcrete(quantifiers::TermDbSygus* tds) : d_ess(tds) {}
+  EnumStreamConcrete(TermDbSygus* tds) : d_ess(tds) {}
   /** initialize this class with enumerator e */
   void initialize(Node e) override;
   /** get that value v was enumerated */
diff --git a/src/theory/quantifiers/sygus/enum_val_generator.h b/src/theory/quantifiers/sygus/enum_val_generator.h
new file mode 100644
index 000000000..64c069087
--- /dev/null
+++ b/src/theory/quantifiers/sygus/enum_val_generator.h
@@ -0,0 +1,62 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Base class for sygus enumerators
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VAL_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VAL_GENERATOR_H
+
+#include "expr/node.h"
+
+namespace cvc5 {
+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;
+  /**
+   * Increment this value generator. If this returns false, then we are out of
+   * values. If this returns true, getCurrent(), if non-null, returns the
+   * current term.
+   *
+   * Notice that increment() may return true and afterwards it may be the case
+   * getCurrent() is null. We do this so that increment() does not take too
+   * much time per call, which can be the case for grammars where it is
+   * difficult to find the next (non-redundant) term. Returning true with
+   * a null current term gives the caller the chance to interleave other
+   * reasoning.
+   */
+  virtual bool increment() = 0;
+  /** Get the current concrete value generated by this class. */
+  virtual Node getCurrent() = 0;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp
index 1c62f030d..a1ae53ad1 100644
--- a/src/theory/quantifiers/sygus/rcons_type_info.cpp
+++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp
@@ -31,7 +31,7 @@ void RConsTypeInfo::initialize(TermDbSygus* tds,
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
 
-  d_enumerator.reset(new SygusEnumerator(tds, nullptr, s, true));
+  d_enumerator.reset(new SygusEnumerator(tds, nullptr, &s, true));
   d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn));
   d_crd.reset(new CandidateRewriteDatabase(true, false, true, false));
   // since initial samples are not always useful for equivalence checks, set
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 0cf92b373..2dfd41fb4 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -20,6 +20,7 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "smt/logic_exception.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/type_node_id_trie.h"
@@ -33,12 +34,14 @@ namespace quantifiers {
 
 SygusEnumerator::SygusEnumerator(TermDbSygus* tds,
                                  SynthConjecture* p,
-                                 SygusStatistics& s,
-                                 bool enumShapes)
+                                 SygusStatistics* s,
+                                 bool enumShapes,
+                                 bool enumAnyConstHoles)
     : d_tds(tds),
       d_parent(p),
       d_stats(s),
       d_enumShapes(enumShapes),
+      d_enumAnyConstHoles(enumAnyConstHoles),
       d_tlEnum(nullptr),
       d_abortSize(-1)
 {
@@ -54,6 +57,12 @@ void SygusEnumerator::initialize(Node e)
   d_tlEnum = getMasterEnumForType(d_etype);
   d_abortSize = options::sygusAbortSize();
 
+  // if we don't have a term database, we don't register symmetry breaking
+  // lemmas
+  if (!d_tds)
+  {
+    return;
+  }
   // Get the statically registered symmetry breaking clauses for e, see if they
   // can be used for speeding up the enumeration.
   NodeManager* nm = NodeManager::currentNM();
@@ -141,7 +150,8 @@ Node SygusEnumerator::getCurrent()
     if (d_sbExcTlCons.find(ret.getOperator()) != d_sbExcTlCons.end())
     {
       Trace("sygus-enum-exc")
-          << "Exclude (external) : " << d_tds->sygusToBuiltin(ret) << std::endl;
+          << "Exclude (external) : " << datatypes::utils::sygusToBuiltin(ret)
+          << std::endl;
       ret = Node::null();
     }
   }
@@ -330,9 +340,12 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
   Assert(!n.isNull());
   if (options::sygusSymBreakDynamic())
   {
-    Node bn = d_tds->sygusToBuiltin(n);
-    Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
-    ++(d_stats->d_enumTermsRewrite);
+    Node bn = datatypes::utils::sygusToBuiltin(n);
+    Node bnr = d_extr.extendedRewrite(bn);
+    if (d_stats != nullptr)
+    {
+      ++(d_stats->d_enumTermsRewrite);
+    }
     if (options::sygusRewVerify())
     {
       if (bn != bnr)
@@ -358,7 +371,10 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
     // if we are doing PBE symmetry breaking
     if (d_eec != nullptr)
     {
-      ++(d_stats->d_enumTermsExampleEval);
+      if (d_stats != nullptr)
+      {
+        ++(d_stats->d_enumTermsExampleEval);
+      }
       // Is it equivalent under examples?
       Node bne = d_eec->addSearchVal(d_tn, bnr);
       if (!bne.isNull())
@@ -374,7 +390,10 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
     }
     Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
   }
-  ++(d_stats->d_enumTerms);
+  if (d_stats != nullptr)
+  {
+    ++(d_stats->d_enumTerms);
+  }
   d_terms.push_back(n);
   return true;
 }
@@ -474,8 +493,8 @@ Node SygusEnumerator::TermEnumSlave::getCurrent()
   Node curr = tc.getTerm(d_index);
   Trace("sygus-enum-debug2")
       << "slave(" << d_tn
-      << "): current : " << d_se->d_tds->sygusToBuiltin(curr)
-      << ", sizes = " << d_se->d_tds->getSygusTermSize(curr) << " "
+      << "): current : " << datatypes::utils::sygusToBuiltin(curr)
+      << ", sizes = " << datatypes::utils::getSygusTermSize(curr) << " "
       << getCurrentSize() << std::endl;
   Trace("sygus-enum-debug2") << "slave(" << d_tn
                              << "): indices : " << d_hasIndexNextEnd << " "
@@ -560,7 +579,7 @@ void SygusEnumerator::initializeTermCache(TypeNode tn)
   {
     eec = d_parent->getExampleEvalCache(d_enum);
   }
-  d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, eec);
+  d_tcache[tn].initialize(d_stats, d_enum, tn, d_tds, eec);
 }
 
 SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
@@ -578,7 +597,7 @@ SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
     AlwaysAssert(ret);
     return &d_masterEnum[tn];
   }
-  if (options::sygusRepairConst())
+  if (d_enumAnyConstHoles)
   {
     std::map<TypeNode, TermEnumMasterFv>::iterator it = d_masterEnumFv.find(tn);
     if (it != d_masterEnumFv.end())
@@ -720,6 +739,7 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal()
   // If we are enumerating shapes, the first enumerated term is a free variable.
   if (d_enumShapes && !d_enumShapesInit)
   {
+    Assert(d_tds != nullptr);
     Node fv = d_tds->getFreeVar(d_tn, 0);
     d_enumShapesInit = true;
     d_currTermSet = true;
@@ -1083,6 +1103,7 @@ void SygusEnumerator::TermEnumMaster::childrenToShape(
 Node SygusEnumerator::TermEnumMaster::convertShape(
     Node n, std::map<TypeNode, int>& vcounter)
 {
+  Assert(d_tds != nullptr);
   NodeManager* nm = NodeManager::currentNM();
   std::unordered_map<TNode, Node> visited;
   std::unordered_map<TNode, Node>::iterator it;
@@ -1195,6 +1216,7 @@ bool SygusEnumerator::TermEnumMasterFv::initialize(SygusEnumerator* se,
 
 Node SygusEnumerator::TermEnumMasterFv::getCurrent()
 {
+  Assert(d_se->d_tds != nullptr);
   Node ret = d_se->d_tds->getFreeVar(d_tn, d_currSize);
   Trace("sygus-enum-debug2") << "master_fv(" << d_tn << "): mk " << ret
                              << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index 355108957..39e58d5f3 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -22,6 +22,7 @@
 #include <unordered_set>
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
@@ -56,10 +57,23 @@ class SygusPbe;
 class SygusEnumerator : public EnumValGenerator
 {
  public:
-  SygusEnumerator(TermDbSygus* tds,
-                  SynthConjecture* p,
-                  SygusStatistics& s,
-                  bool enumShapes = false);
+  /**
+   * @param tds Pointer to the term database, required if enumShapes or
+   * enumAnyConstHoles is true, or if we want to include symmetry breaking from
+   * lemmas stored in the sygus term database,
+   * @param p Pointer to the conjecture, required if we wish to do
+   * conjecture-specific symmetry breaking
+   * @param s Pointer to the statistics
+   * @param enumShapes If true, this enumerator will generate terms having any
+   * number of free variables
+   * @param enumAnyConstHoles If true, this enumerator will generate terms where
+   * free variables are the arguments to any-constant constructors.
+   */
+  SygusEnumerator(TermDbSygus* tds = nullptr,
+                  SynthConjecture* p = nullptr,
+                  SygusStatistics* s = nullptr,
+                  bool enumShapes = false,
+                  bool enumAnyConstHoles = false);
   ~SygusEnumerator() {}
   /** initialize this class with enumerator e */
   void initialize(Node e) override;
@@ -77,10 +91,13 @@ class SygusEnumerator : public EnumValGenerator
   TermDbSygus* d_tds;
   /** pointer to the synth conjecture that owns this enumerator */
   SynthConjecture* d_parent;
-  /** reference to the statistics of parent */
-  SygusStatistics& d_stats;
+  /** pointer to the statistics */
+  SygusStatistics* d_stats;
   /** Whether we are enumerating shapes */
   bool d_enumShapes;
+  /** Whether we are enumerating free variables as arguments to any-constant
+   * constructors */
+  bool d_enumAnyConstHoles;
   /** Term cache
    *
    * This stores a list of terms for a given sygus type. The key features of
@@ -171,6 +188,8 @@ class SygusEnumerator : public EnumValGenerator
     TypeNode d_tn;
     /** pointer to term database sygus */
     TermDbSygus* d_tds;
+    /** extended rewriter */
+    ExtendedRewriter d_extr;
     /**
      * Pointer to the example evaluation cache utility (used for symmetry
      * breaking).
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
index bae6f6327..42bce471d 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
@@ -22,7 +22,7 @@
 #include <unordered_set>
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "theory/quantifiers/sygus/synth_conjecture.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/type_enumerator.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
new file mode 100644
index 000000000..7b3236832
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
@@ -0,0 +1,107 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * sygus_enumerator
+ */
+
+#include "theory/quantifiers/sygus/sygus_enumerator_callback.h"
+
+#include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/sygus/example_eval_cache.h"
+#include "theory/quantifiers/sygus/sygus_stats.h"
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+SygusEnumeratorCallback::SygusEnumeratorCallback(Node e, SygusStatistics* s)
+    : d_enum(e), d_stats(s)
+{
+  d_tn = e.getType();
+}
+
+bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
+{
+  Node bn = datatypes::utils::sygusToBuiltin(n);
+  Node bnr = d_extr.extendedRewrite(bn);
+  if (d_stats != nullptr)
+  {
+    ++(d_stats->d_enumTermsRewrite);
+  }
+  // call the solver-specific notify term
+  notifyTermInternal(n, bn, bnr);
+  // check whether we should keep the term, which is based on the callback,
+  // and the builtin terms
+  // First, must be unique up to rewriting
+  if (bterms.find(bnr) != bterms.end())
+  {
+    Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
+    return false;
+  }
+  // insert to builtin term cache, regardless of whether it is redundant
+  // based on the callback
+  bterms.insert(bnr);
+  // callback-specific add term
+  if (!addTermInternal(n, bn, bnr))
+  {
+    Trace("sygus-enum-exc")
+        << "Exclude: " << bn << " due to callback" << std::endl;
+    return false;
+  }
+  Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
+  return true;
+}
+
+SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault(
+    Node e, SygusStatistics* s, ExampleEvalCache* eec, SygusSampler* ssrv)
+    : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv)
+{
+}
+void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n,
+                                                        Node bn,
+                                                        Node bnr)
+{
+  if (d_samplerRrV != nullptr)
+  {
+    d_samplerRrV->checkEquivalent(bn, bnr);
+  }
+}
+
+bool SygusEnumeratorCallbackDefault::addTermInternal(Node n, Node bn, Node bnr)
+{
+  // if we are doing PBE symmetry breaking
+  if (d_eec != nullptr)
+  {
+    if (d_stats != nullptr)
+    {
+      ++(d_stats->d_enumTermsExampleEval);
+    }
+    // Is it equivalent under examples?
+    Node bne = d_eec->addSearchVal(d_tn, bnr);
+    if (!bne.isNull())
+    {
+      if (bnr != bne)
+      {
+        Trace("sygus-enum-exc")
+            << "Exclude (by examples): " << bn << ", since we already have "
+            << bne << std::endl;
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
new file mode 100644
index 000000000..545440eef
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
@@ -0,0 +1,110 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * sygus_enumerator
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
+
+#include <unordered_set>
+
+#include "expr/node.h"
+#include "theory/quantifiers/extended_rewrite.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+class ExampleEvalCache;
+class SygusStatistics;
+class SygusSampler;
+
+/**
+ * Base class for callbacks in the fast enumerator. This allows a user to
+ * provide custom criteria for whether or not enumerated values should be
+ * considered.
+ */
+class SygusEnumeratorCallback
+{
+ public:
+  SygusEnumeratorCallback(Node e, SygusStatistics* s = nullptr);
+  virtual ~SygusEnumeratorCallback() {}
+  /**
+   * Add term, return true if the term should be considered in the enumeration.
+   * Notice that returning false indicates that n should not be considered as a
+   * subterm of any other term in the enumeration.
+   *
+   * @param n The SyGuS term
+   * @param bterms The (rewritten, builtin) terms we have already enumerated
+   * @return true if n should be considered in the enumeration.
+   */
+  virtual bool addTerm(Node n, std::unordered_set<Node>& bterms) = 0;
+
+ protected:
+  /**
+   * Callback-specific notification of the above
+   *
+   * @param n The SyGuS term
+   * @param bn The builtin version of the enumerated term
+   * @param bnr The (extended) rewritten form of bn
+   */
+  virtual void notifyTermInternal(Node n, Node bn, Node bnr) = 0;
+  /**
+   * Callback-specific add term
+   *
+   * @param n The SyGuS term
+   * @param bn The builtin version of the enumerated term
+   * @param bnr The (extended) rewritten form of bn
+   * @return true if the term should be considered in the enumeration.
+   */
+  virtual bool addTermInternal(Node n, Node bn, Node bnr) = 0;
+  /** The enumerator */
+  Node d_enum;
+  /** The type of enum */
+  TypeNode d_tn;
+  /** extended rewriter */
+  ExtendedRewriter d_extr;
+  /** pointer to the statistics */
+  SygusStatistics* d_stats;
+};
+
+class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
+{
+ public:
+  SygusEnumeratorCallbackDefault(Node e,
+                                 SygusStatistics* s = nullptr,
+                                 ExampleEvalCache* eec = nullptr,
+                                 SygusSampler* ssrv = nullptr);
+  virtual ~SygusEnumeratorCallbackDefault() {}
+
+ protected:
+  /** Notify that bn / bnr is an enumerated builtin, rewritten form of a term */
+  void notifyTermInternal(Node n, Node bn, Node bnr) override;
+  /** Add term, return true if n should be considered in the enumeration */
+  bool addTermInternal(Node n, Node bn, Node bnr) override;
+  /**
+   * Pointer to the example evaluation cache utility (used for symmetry
+   * breaking).
+   */
+  ExampleEvalCache* d_eec;
+  /** sampler (for --sygus-rr-verify) */
+  SygusSampler* d_samplerRrV;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H */
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 395f16beb..23c315f42 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -18,6 +18,7 @@
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "smt/logic_exception.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/sygus_invariance.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -220,7 +221,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
       // we are tracking term size if positive
       if (sz >= 0)
       {
-        int s = d_tdb->getSygusTermSize(vn[i]);
+        int s = datatypes::utils::getSygusTermSize(vn[i]);
         sz = sz - s;
       }
     }
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 86d0bbc8e..892ee6dd4 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_pbe.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/example_infer.h"
 #include "theory/quantifiers/sygus/sygus_unif_io.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
@@ -180,7 +181,7 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
       Trace("sygus-pbe-enum") << std::endl;
       if (!enum_values[i].isNull())
       {
-        unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
+        unsigned sz = datatypes::utils::getSygusTermSize(enum_values[i]);
         szs.push_back(sz);
         if (i == 0 || sz < min_term_size)
         {
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index 16ca1f4e6..00370ffa2 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/sygus/sygus_unif.h"
 
+#include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "util/random.h"
@@ -52,7 +53,7 @@ Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
     unsigned ssize = 0;
     if (it == d_termToSize.end())
     {
-      ssize = d_tds->getSygusTermSize(n);
+      ssize = datatypes::utils::getSygusTermSize(n);
       d_termToSize[n] = ssize;
     }
     else
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 8c8f5ccd4..8207a07f2 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/sygus/sygus_unif_io.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/evaluator.h"
 #include "theory/quantifiers/sygus/example_infer.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
@@ -835,7 +836,8 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
       if (!vcc.isNull()
           && (d_solution.isNull()
               || (!d_solution.isNull()
-                  && d_tds->getSygusTermSize(vcc) < d_sol_term_size)))
+                  && datatypes::utils::getSygusTermSize(vcc)
+                         < d_sol_term_size)))
       {
         if (Trace.isOn("sygus-pbe"))
         {
@@ -846,7 +848,7 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
         }
         d_solution = vcc;
         newSolution = vcc;
-        d_sol_term_size = d_tds->getSygusTermSize(vcc);
+        d_sol_term_size = datatypes::utils::getSygusTermSize(vcc);
         Trace("sygus-pbe-sol")
             << "PBE solution size: " << d_sol_term_size << std::endl;
         // We've determined its feasible, now, enable information gain and
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 1ddc2fa22..73bd6b8a4 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -827,7 +827,10 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
                    == options::SygusActiveGenMode::ENUM
                || options::sygusActiveGenMode()
                       == options::SygusActiveGenMode::AUTO);
-        d_evg[e].reset(new SygusEnumerator(d_tds, this, d_stats));
+        // if sygus repair const is enabled, we enumerate terms with free
+        // variables as arguments to any-constant constructors
+        d_evg[e].reset(new SygusEnumerator(
+            d_tds, this, &d_stats, false, options::sygusRepairConst()));
       }
     }
     Trace("sygus-active-gen")
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index e6645ddf2..04999da0d 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/cegis_core_connective.h"
 #include "theory/quantifiers/sygus/cegis_unif.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
 #include "theory/quantifiers/sygus/example_eval_cache.h"
 #include "theory/quantifiers/sygus/example_infer.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
@@ -42,37 +43,6 @@ class CegGrammarConstructor;
 class SygusPbe;
 class SygusStatistics;
 
-/**
- * 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;
-  /**
-   * Increment this value generator. If this returns false, then we are out of
-   * values. If this returns true, getCurrent(), if non-null, returns the
-   * current term.
-   *
-   * Notice that increment() may return true and afterwards it may be the case
-   * getCurrent() is null. We do this so that increment() does not take too
-   * much time per call, which can be the case for grammars where it is
-   * difficult to find the next (non-redundant) term. Returning true with
-   * a null current term gives the caller the chance to interleave other
-   * reasoning.
-   */
-  virtual bool increment() = 0;
-  /** Get the current concrete value generated by this class. */
-  virtual Node getCurrent() = 0;
-};
-
 /** a synthesis conjecture
  * This class implements approaches for a synthesis conjecture, given by data
  * member d_quant.
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 826563401..3b0ea3312 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -359,23 +359,6 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
   return ret;
 }
 
-unsigned TermDbSygus::getSygusTermSize( Node n ){
-  if (n.getKind() != APPLY_CONSTRUCTOR)
-  {
-    return 0;
-  }
-  unsigned sum = 0;
-  for (unsigned i = 0; i < n.getNumChildren(); i++)
-  {
-    sum += getSygusTermSize(n[i]);
-  }
-  const DType& dt = datatypes::utils::datatypeOf(n.getOperator());
-  int cindex = datatypes::utils::indexOf(n.getOperator());
-  Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
-  unsigned weight = dt[cindex].getWeight();
-  return weight + sum;
-}
-
 bool TermDbSygus::registerSygusType(TypeNode tn)
 {
   std::map<TypeNode, bool>::iterator it = d_registerStatus.find(tn);
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index e0a812069..80411b258 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -456,7 +456,6 @@ class TermDbSygus {
 
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized(TypeNode t, Node prog);
-  unsigned getSygusTermSize( Node n );
   /** involves div-by-zero */
   bool involvesDivByZero( Node n );
   /** get anchor */