From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 24 Aug 2021 17:26:35 +0000 (-0500)
Subject: Refactor enumerator management in synth conjecture (#6942)
X-Git-Tag: cvc5-1.0.0~1340
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba34ba8fc1edc62702f6b6ffcd247d13ba7f8271;p=cvc5.git

Refactor enumerator management in synth conjecture (#6942)

This moves the method SynthConjecture::getEnumeratedValue to its own class, EnumManager.

It also integrates the sygus enumerator callback into the fast enumerator.
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9d887cc63..f5af58aeb 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -884,6 +884,8 @@ libcvc5_add_sources(
   theory/quantifiers/sygus/example_min_eval.h
   theory/quantifiers/sygus/enum_stream_substitution.cpp
   theory/quantifiers/sygus/enum_stream_substitution.h
+  theory/quantifiers/sygus/enum_value_manager.cpp
+  theory/quantifiers/sygus/enum_value_manager.h
   theory/quantifiers/sygus/example_infer.cpp
   theory/quantifiers/sygus/example_infer.h
   theory/quantifiers/sygus/example_min_eval.cpp
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
new file mode 100644
index 000000000..fd92e4d23
--- /dev/null
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -0,0 +1,251 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner, Haniel Barbosa
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Management of current value for an enumerator
+ */
+#include "theory/quantifiers/sygus/enum_value_manager.h"
+
+#include "options/datatypes_options.h"
+#include "options/quantifiers_options.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/sygus/enum_stream_substitution.h"
+#include "theory/quantifiers/sygus/sygus_enumerator.h"
+#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_registry.h"
+
+using namespace cvc5::kind;
+using namespace std;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+EnumValueManager::EnumValueManager(Node e,
+                                   QuantifiersInferenceManager& qim,
+                                   TermRegistry& tr,
+                                   SygusStatistics& s,
+                                   bool hasExamples)
+    : d_enum(e),
+      d_qim(qim),
+      d_treg(tr),
+      d_stats(s),
+      d_tds(tr.getTermDatabaseSygus()),
+      d_eec(hasExamples ? new ExampleEvalCache(d_tds, e) : nullptr)
+{
+}
+
+EnumValueManager::~EnumValueManager() {}
+
+Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
+{
+  Node e = d_enum;
+  bool isEnum = d_tds->isEnumerator(e);
+
+  if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
+  {
+    // 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("sygus-engine-debug")
+        << "Enumerator " << e << " does not have proper model value."
+        << std::endl;
+    return Node::null();
+  }
+
+  if (!isEnum || d_tds->isPassiveEnumerator(e))
+  {
+    return getModelValue(e);
+  }
+
+  // management of actively generated enumerators goes here
+
+  // initialize the enumerated value generator for e
+  if (d_evg == nullptr)
+  {
+    if (d_tds->isVariableAgnosticEnumerator(e))
+    {
+      d_evg.reset(new EnumStreamConcrete(d_tds));
+    }
+    else
+    {
+      // Actively-generated enumerators are currently either variable agnostic
+      // or basic. The auto mode always prefers the optimized enumerator over
+      // the basic one.
+      Assert(d_tds->isBasicEnumerator(e));
+      if (options::sygusActiveGenMode()
+          == options::SygusActiveGenMode::ENUM_BASIC)
+      {
+        d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType()));
+      }
+      else
+      {
+        Assert(options::sygusActiveGenMode()
+                   == options::SygusActiveGenMode::ENUM
+               || options::sygusActiveGenMode()
+                      == options::SygusActiveGenMode::AUTO);
+        // create the enumerator callback
+        if (options::sygusSymBreakDynamic())
+        {
+          if (options::sygusRewVerify())
+          {
+            d_samplerRrV.reset(new SygusSampler);
+            d_samplerRrV->initializeSygus(
+                d_tds, e, options::sygusSamples(), false);
+          }
+          d_secd.reset(new SygusEnumeratorCallbackDefault(
+              e, &d_stats, d_eec.get(), d_samplerRrV.get()));
+        }
+        // if sygus repair const is enabled, we enumerate terms with free
+        // variables as arguments to any-constant constructors
+        d_evg.reset(new SygusEnumerator(
+            d_tds, d_secd.get(), &d_stats, false, options::sygusRepairConst()));
+      }
+    }
+    Trace("sygus-active-gen")
+        << "Active-gen: initialize for " << e << std::endl;
+    d_evg->initialize(e);
+    d_ev_curr_active_gen = Node::null();
+    Trace("sygus-active-gen-debug") << "...finish" << std::endl;
+  }
+  // if we have a waiting value, return it
+  if (!d_evActiveGenWaiting.isNull())
+  {
+    Trace("sygus-active-gen-debug")
+        << "Active-gen: return waiting " << d_evActiveGenWaiting << std::endl;
+    return d_evActiveGenWaiting;
+  }
+  // Check if there is an (abstract) value absE we were actively generating
+  // values based on.
+  Node absE = d_ev_curr_active_gen;
+  bool firstTime = false;
+  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 = absE;
+    d_evg->addValue(absE);
+    firstTime = true;
+  }
+  bool inc = true;
+  if (!firstTime)
+  {
+    inc = d_evg->increment();
+  }
+  Node v;
+  if (inc)
+  {
+    v = d_evg->getCurrent();
+  }
+  Trace("sygus-active-gen-debug")
+      << "...generated " << v << ", with increment success : " << inc
+      << std::endl;
+  if (!inc)
+  {
+    // No more concrete values generated from absE.
+    NodeManager* nm = NodeManager::currentNM();
+    d_ev_curr_active_gen = Node::null();
+    std::vector<Node> exp;
+    // If we are a basic enumerator, a single abstract value maps to *all*
+    // concrete values of its type, thus we don't depend on the current
+    // solution.
+    if (!d_tds->isBasicEnumerator(e))
+    {
+      // We must block e = absE
+      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_evActiveGenFirstVal.isNull())
+      {
+        exp.push_back(g.negate());
+        d_evActiveGenFirstVal = 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_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT);
+  }
+  else
+  {
+    // We are waiting to send e -> v to the module that requested it.
+    if (v.isNull())
+    {
+      activeIncomplete = true;
+    }
+    else
+    {
+      d_evActiveGenWaiting = 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;
+}
+
+void EnumValueManager::notifyCandidate(bool modelSuccess)
+{
+  d_evActiveGenWaiting = Node::null();
+  // clear evaluation
+  if (modelSuccess && d_eec != nullptr)
+  {
+    d_eec->clearEvaluationAll();
+  }
+}
+
+ExampleEvalCache* EnumValueManager::getExampleEvalCache()
+{
+  return d_eec.get();
+}
+
+Node EnumValueManager::getModelValue(Node n)
+{
+  return d_treg.getModel()->getValue(n);
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.h b/src/theory/quantifiers/sygus/enum_value_manager.h
new file mode 100644
index 000000000..e610764e0
--- /dev/null
+++ b/src/theory/quantifiers/sygus/enum_value_manager.h
@@ -0,0 +1,122 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Management of current value for an enumerator
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VALUE_MANAGER_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VALUE_MANAGER_H
+
+#include "expr/node.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
+#include "theory/quantifiers/sygus/example_eval_cache.h"
+#include "theory/quantifiers/sygus/sygus_enumerator_callback.h"
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifiersInferenceManager;
+class TermRegistry;
+class SygusStatistics;
+
+/**
+ * Management of current value for an enumerator. This class determines the
+ * current value of an enumerator, which may be its model value if it is
+ * not actively generated, or may be determined by the (fast) enumerator
+ * when it is actively generated.
+ */
+class EnumValueManager
+{
+ public:
+  EnumValueManager(Node e,
+                   QuantifiersInferenceManager& qim,
+                   TermRegistry& tr,
+                   SygusStatistics& s,
+                   bool hasExamples);
+  ~EnumValueManager();
+  /**
+   * Get model value for term n. If n has a value that was excluded by
+   * datatypes sygus symmetry breaking, this method returns null. It sets
+   * activeIncomplete to true if the enumerator we are managing is
+   * actively-generated, and its current value is null but it has not finished
+   * generating values.
+   */
+  Node getEnumeratedValue(bool& activeIncomplete);
+  /**
+   * Notify that a synthesis candidate was tried, which clears the value
+   * of d_evActiveGenWaiting, as well as the evaluation cache if modelSuccess
+   * is true
+   */
+  void notifyCandidate(bool modelSuccess);
+  /** Get the example evaluation cache */
+  ExampleEvalCache* getExampleEvalCache();
+
+ private:
+  /**
+   * Get model value for term n.
+   */
+  Node getModelValue(Node n);
+  /** The enumerator */
+  Node d_enum;
+  /** Reference to the quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
+  /** reference to the statistics of parent */
+  SygusStatistics& d_stats;
+  /** term database sygus of d_qe */
+  TermDbSygus* d_tds;
+  /** Sygus sampler (for --sygus-rr-verify) */
+  std::unique_ptr<SygusSampler> d_samplerRrV;
+  /** if we allocated a default sygus enumerator callback */
+  std::unique_ptr<SygusEnumeratorCallbackDefault> d_secd;
+  /** enumerator generators for each actively-generated enumerator */
+  std::unique_ptr<EnumValGenerator> d_evg;
+  /** example evaluation cache utility for each enumerator */
+  std::unique_ptr<ExampleEvalCache> d_eec;
+  /**
+   * Map from enumerators to whether they are currently being
+   * "actively-generated". That is, we are in a state where we have called
+   * d_evg.addValue(v) for some v, and d_evg.getNext() has not yet
+   * returned null. The range of this map stores the abstract value that
+   * we are currently generating values from.
+   */
+  Node d_ev_curr_active_gen;
+  /** the current waiting value of the 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.
+   */
+  Node d_evActiveGenWaiting;
+  /** the first value enumerated for the actively-generated enumerator
+   *
+   * This is to implement an optimization that only guards the blocking lemma
+   * for the first value of an actively-generated enumerator.
+   */
+  Node d_evActiveGenFirstVal;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp
index bd9e24eaa..67fbf65bf 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.cpp
+++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/sygus/example_eval_cache.h"
 
 #include "theory/quantifiers/sygus/example_min_eval.h"
-#include "theory/quantifiers/sygus/synth_conjecture.h"
 
 using namespace cvc5;
 using namespace cvc5::kind;
@@ -25,24 +24,19 @@ namespace theory {
 namespace quantifiers {
 
 ExampleEvalCache::ExampleEvalCache(TermDbSygus* tds,
-                                   SynthConjecture* p,
-                                   Node f,
                                    Node e)
     : d_tds(tds), d_stn(e.getType())
 {
-  ExampleInfer* ei = p->getExampleInfer();
-  Assert(ei->hasExamples(f));
-  for (unsigned i = 0, nex = ei->getNumExamples(f); i < nex; i++)
-  {
-    std::vector<Node> input;
-    ei->getExample(f, i, input);
-    d_examples.push_back(input);
-  }
   d_indexSearchVals = !d_tds->isVariableAgnosticEnumerator(e);
 }
 
 ExampleEvalCache::~ExampleEvalCache() {}
 
+void ExampleEvalCache::addExample(const std::vector<Node>& ex)
+{
+  d_examples.push_back(ex);
+}
+
 Node ExampleEvalCache::addSearchVal(TypeNode tn, Node bv)
 {
   if (!d_indexSearchVals)
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h
index 2bc783c0f..fe544d11d 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.h
+++ b/src/theory/quantifiers/sygus/example_eval_cache.h
@@ -73,8 +73,12 @@ class ExampleEvalCache
    * are builtin terms that the analog of values taken by enumerator e that
    * is associated with f.
    */
-  ExampleEvalCache(TermDbSygus* tds, SynthConjecture* p, Node f, Node e);
+  ExampleEvalCache(TermDbSygus* tds, Node e);
   ~ExampleEvalCache();
+  /**
+   * Add example to the list of examples maintained by this class.
+   */
+  void addExample(const std::vector<Node>& ex);
 
   /** Add search value
    *
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h
index dac89c7c6..4c9ae48e0 100644
--- a/src/theory/quantifiers/sygus/rcons_type_info.h
+++ b/src/theory/quantifiers/sygus/rcons_type_info.h
@@ -18,13 +18,16 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
 #define CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
 
+#include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
+#include "theory/quantifiers/sygus_sampler.h"
 
 namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
 class RConsObligation;
+class CandidateRewriteDatabase;
 
 /**
  * A utility class for Sygus Reconstruct datatype types (grammar non-terminals).
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 2dfd41fb4..fca09c43d 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -33,12 +33,12 @@ namespace theory {
 namespace quantifiers {
 
 SygusEnumerator::SygusEnumerator(TermDbSygus* tds,
-                                 SynthConjecture* p,
+                                 SygusEnumeratorCallback* sec,
                                  SygusStatistics* s,
                                  bool enumShapes,
                                  bool enumAnyConstHoles)
     : d_tds(tds),
-      d_parent(p),
+      d_sec(sec),
       d_stats(s),
       d_enumShapes(enumShapes),
       d_enumAnyConstHoles(enumAnyConstHoles),
@@ -51,6 +51,12 @@ void SygusEnumerator::initialize(Node e)
 {
   Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl;
   d_enum = e;
+  // allocate the default callback
+  if (d_sec == nullptr && options::sygusSymBreakDynamic())
+  {
+    d_secd.reset(new SygusEnumeratorCallbackDefault(e, d_stats));
+    d_sec = d_secd.get();
+  }
   d_etype = d_enum.getType();
   Assert(d_etype.isDatatype());
   Assert(d_etype.getDType().isSygus());
@@ -59,7 +65,7 @@ void SygusEnumerator::initialize(Node e)
 
   // if we don't have a term database, we don't register symmetry breaking
   // lemmas
-  if (!d_tds)
+  if (d_tds == nullptr)
   {
     return;
   }
@@ -167,28 +173,24 @@ Node SygusEnumerator::getCurrent()
 bool SygusEnumerator::isEnumShapes() const { return d_enumShapes; }
 
 SygusEnumerator::TermCache::TermCache()
-    : d_tds(nullptr),
-      d_eec(nullptr),
+    : d_sec(nullptr),
       d_isSygusType(false),
       d_numConClasses(0),
       d_sizeEnum(0),
-      d_isComplete(false),
-      d_sampleRrVInit(false)
+      d_isComplete(false)
 {
 }
 
 void SygusEnumerator::TermCache::initialize(SygusStatistics* s,
                                             Node e,
                                             TypeNode tn,
-                                            TermDbSygus* tds,
-                                            ExampleEvalCache* eec)
+                                            SygusEnumeratorCallback* sec)
 {
   Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl;
   d_stats = s;
   d_enum = e;
   d_tn = tn;
-  d_tds = tds;
-  d_eec = eec;
+  d_sec = sec;
   d_sizeStartIndex[0] = 0;
   d_isSygusType = false;
 
@@ -338,57 +340,15 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
     return true;
   }
   Assert(!n.isNull());
-  if (options::sygusSymBreakDynamic())
+  if (d_sec != nullptr)
   {
-    Node bn = datatypes::utils::sygusToBuiltin(n);
-    Node bnr = d_extr.extendedRewrite(bn);
-    if (d_stats != nullptr)
-    {
-      ++(d_stats->d_enumTermsRewrite);
-    }
-    if (options::sygusRewVerify())
+    if (!d_sec->addTerm(n, d_bterms))
     {
-      if (bn != bnr)
-      {
-        if (!d_sampleRrVInit)
-        {
-          d_sampleRrVInit = true;
-          d_samplerRrV.initializeSygus(
-              d_tds, d_enum, options::sygusSamples(), false);
-        }
-        d_samplerRrV.checkEquivalent(bn, bnr);
-      }
-    }
-    // must be unique up to rewriting
-    if (d_bterms.find(bnr) != d_bterms.end())
-    {
-      Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
+      Trace("sygus-enum-exc")
+          << "Exclude: " << datatypes::utils::sygusToBuiltin(n)
+          << " due to callback" << std::endl;
       return false;
     }
-    // insert to builtin term cache, regardless of whether it is redundant
-    // based on examples.
-    d_bterms.insert(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;
-        }
-      }
-    }
-    Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
   }
   if (d_stats != nullptr)
   {
@@ -573,13 +533,7 @@ void SygusEnumerator::TermEnumSlave::validateIndexNextEnd()
 void SygusEnumerator::initializeTermCache(TypeNode tn)
 {
   // initialize the term cache
-  // see if we use an example evaluation cache for symmetry breaking
-  ExampleEvalCache* eec = nullptr;
-  if (d_parent != nullptr && options::sygusSymBreakPbe())
-  {
-    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_sec);
 }
 
 SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index 39e58d5f3..612a753af 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -20,10 +20,11 @@
 
 #include <map>
 #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/sygus_enumerator_callback.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 namespace cvc5 {
@@ -61,7 +62,7 @@ class SygusEnumerator : public EnumValGenerator
    * @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
+   * @param sec Pointer to the callback, required e.g. 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
@@ -70,7 +71,7 @@ class SygusEnumerator : public EnumValGenerator
    * free variables are the arguments to any-constant constructors.
    */
   SygusEnumerator(TermDbSygus* tds = nullptr,
-                  SynthConjecture* p = nullptr,
+                  SygusEnumeratorCallback* sec = nullptr,
                   SygusStatistics* s = nullptr,
                   bool enumShapes = false,
                   bool enumAnyConstHoles = false);
@@ -89,8 +90,10 @@ class SygusEnumerator : public EnumValGenerator
  private:
   /** pointer to term database sygus */
   TermDbSygus* d_tds;
-  /** pointer to the synth conjecture that owns this enumerator */
-  SynthConjecture* d_parent;
+  /** pointer to the enumerator callback we are using (if any) */
+  SygusEnumeratorCallback* d_sec;
+  /** if we allocated a default sygus enumerator callback */
+  std::unique_ptr<SygusEnumeratorCallbackDefault> d_secd;
   /** pointer to the statistics */
   SygusStatistics* d_stats;
   /** Whether we are enumerating shapes */
@@ -138,8 +141,7 @@ class SygusEnumerator : public EnumValGenerator
     void initialize(SygusStatistics* s,
                     Node e,
                     TypeNode tn,
-                    TermDbSygus* tds,
-                    ExampleEvalCache* ece = nullptr);
+                    SygusEnumeratorCallback* sec = nullptr);
     /** get last constructor class index for weight
      *
      * This returns a minimal index n such that all constructor classes at
@@ -186,15 +188,8 @@ class SygusEnumerator : public EnumValGenerator
     Node d_enum;
     /** the sygus type of terms in this cache */
     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).
-     */
-    ExampleEvalCache* d_eec;
+    /** Pointer to the callback (used for symmetry breaking). */
+    SygusEnumeratorCallback* d_sec;
     //-------------------------static information about type
     /** is d_tn a sygus type? */
     bool d_isSygusType;
@@ -233,10 +228,6 @@ class SygusEnumerator : public EnumValGenerator
     unsigned d_sizeEnum;
     /** whether this term cache is complete */
     bool d_isComplete;
-    /** sampler (for --sygus-rr-verify) */
-    quantifiers::SygusSampler d_samplerRrV;
-    /** is the above sampler initialized? */
-    bool d_sampleRrVInit;
   };
   /** above cache for each sygus type */
   std::map<TypeNode, TermCache> d_tcache;
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
index 545440eef..46ca68c51 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
@@ -50,7 +50,7 @@ class SygusEnumeratorCallback
    * @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;
+  virtual bool addTerm(Node n, std::unordered_set<Node>& bterms);
 
  protected:
   /**
@@ -60,7 +60,7 @@ class SygusEnumeratorCallback
    * @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;
+  virtual void notifyTermInternal(Node n, Node bn, Node bnr) {}
   /**
    * Callback-specific add term
    *
@@ -69,7 +69,7 @@ class SygusEnumeratorCallback
    * @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;
+  virtual bool addTermInternal(Node n, Node bn, Node bnr) { return true; }
   /** The enumerator */
   Node d_enum;
   /** The type of enum */
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h
index 221d3bb7b..e86b1688c 100644
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.h
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h
@@ -21,6 +21,7 @@
 #include <map>
 #include <vector>
 
+#include "expr/match_trie.h"
 #include "theory/quantifiers/sygus/rcons_obligation.h"
 #include "theory/quantifiers/sygus/rcons_type_info.h"
 
@@ -30,6 +31,7 @@ namespace quantifiers {
 
 using BuiltinSet = std::unordered_set<Node>;
 using TypeBuiltinSetMap = std::unordered_map<TypeNode, BuiltinSet>;
+using NodePairMap = std::unordered_map<Node, Node>;
 
 /** SygusReconstruct
  *
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index ad9aceb8f..3f7ce158c 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -30,9 +30,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/sygus_enumerator.h"
-#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
+#include "theory/quantifiers/sygus/enum_value_manager.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
@@ -380,74 +378,72 @@ bool SynthConjecture::doCheck()
       // on the next call
       return !activeIncomplete;
     }
-    // the waiting values are passed to the module below, clear
-    d_ev_active_gen_waiting.clear();
-
+    // determine if we had at least one value for an enumerator
     Assert(terms.size() == enum_values.size());
-    bool emptyModel = true;
+    bool modelSuccess = false;
     for (unsigned i = 0, size = terms.size(); i < size; i++)
     {
       if (!enum_values[i].isNull())
       {
-        emptyModel = false;
+        modelSuccess = true;
       }
     }
-    if (emptyModel)
-    {
-      Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
-      return !activeIncomplete;
-    }
-    // Must separately compute whether trace is on due to compilation of
-    // Trace.isOn.
-    bool traceIsOn = Trace.isOn("sygus-engine");
-    if (printDebug || traceIsOn)
+    if (modelSuccess)
     {
-      Trace("sygus-engine") << "  * Value is : ";
-      std::stringstream sygusEnumOut;
-      FirstOrderModel* m = d_treg.getModel();
-      for (unsigned i = 0, size = terms.size(); i < size; i++)
+      // Must separately compute whether trace is on due to compilation of
+      // Trace.isOn.
+      bool traceIsOn = Trace.isOn("sygus-engine");
+      if (printDebug || traceIsOn)
       {
-        Node nv = enum_values[i];
-        Node onv = nv.isNull() ? m->getValue(terms[i]) : nv;
-        TypeNode tn = onv.getType();
-        std::stringstream ss;
-        TermDbSygus::toStreamSygus(ss, onv);
-        if (printDebug)
-        {
-          sygusEnumOut << " " << ss.str();
-        }
-        Trace("sygus-engine") << terms[i] << " -> ";
-        if (nv.isNull())
-        {
-          Trace("sygus-engine") << "[EXC: " << ss.str() << "] ";
-        }
-        else
+        Trace("sygus-engine") << "  * Value is : ";
+        std::stringstream sygusEnumOut;
+        FirstOrderModel* m = d_treg.getModel();
+        for (unsigned i = 0, size = terms.size(); i < size; i++)
         {
-          Trace("sygus-engine") << ss.str() << " ";
-          if (Trace.isOn("sygus-engine-rr"))
+          Node nv = enum_values[i];
+          Node onv = nv.isNull() ? m->getValue(terms[i]) : nv;
+          TypeNode tn = onv.getType();
+          std::stringstream ss;
+          TermDbSygus::toStreamSygus(ss, onv);
+          if (printDebug)
+          {
+            sygusEnumOut << " " << ss.str();
+          }
+          Trace("sygus-engine") << terms[i] << " -> ";
+          if (nv.isNull())
           {
-            Node bv = d_tds->sygusToBuiltin(nv, tn);
-            bv = Rewriter::rewrite(bv);
-            Trace("sygus-engine-rr") << " -> " << bv << std::endl;
+            Trace("sygus-engine") << "[EXC: " << ss.str() << "] ";
+          }
+          else
+          {
+            Trace("sygus-engine") << ss.str() << " ";
+            if (Trace.isOn("sygus-engine-rr"))
+            {
+              Node bv = d_tds->sygusToBuiltin(nv, tn);
+              bv = Rewriter::rewrite(bv);
+              Trace("sygus-engine-rr") << " -> " << bv << std::endl;
+            }
           }
         }
+        Trace("sygus-engine") << std::endl;
+        Output(options::OutputTag::SYGUS)
+            << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
       }
-      Trace("sygus-engine") << std::endl;
-      Output(options::OutputTag::SYGUS)
-          << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
+      Assert(candidate_values.empty());
+      constructed_cand = d_master->constructCandidates(
+          terms, enum_values, d_candidates, candidate_values);
     }
-    Assert(candidate_values.empty());
-    constructed_cand = d_master->constructCandidates(
-        terms, enum_values, d_candidates, candidate_values);
-    // now clear the evaluation caches
-    for (std::pair<const Node, std::unique_ptr<ExampleEvalCache> >& ecp :
-         d_exampleEvalCache)
+    // notify the enumerator managers of the status of the candidate
+    for (std::pair<const Node, std::unique_ptr<EnumValueManager>>& ecp :
+         d_enumManager)
     {
-      ExampleEvalCache* eec = ecp.second.get();
-      if (eec != nullptr)
-      {
-        eec->clearEvaluationAll();
-      }
+      ecp.second->notifyCandidate(modelSuccess);
+    }
+    // if we did not generate a candidate, return now
+    if (!modelSuccess)
+    {
+      Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
+      return !activeIncomplete;
     }
   }
 
@@ -746,7 +742,8 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
         continue;
       }
     }
-    Node nv = getEnumeratedValue(e, activeIncomplete);
+    EnumValueManager* eman = getEnumValueManagerFor(e);
+    Node nv = eman->getEnumeratedValue(activeIncomplete);
     n.push_back(e);
     v.push_back(nv);
     ret = ret && !nv.isNull();
@@ -754,173 +751,34 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
   return ret;
 }
 
-Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
+EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e)
 {
-  bool isEnum = d_tds->isEnumerator(e);
-
-  if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
-  {
-    // 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("sygus-engine-debug")
-        << "Enumerator " << e << " does not have proper model value."
-        << std::endl;
-    return Node::null();
-  }
-
-  if (!isEnum || d_tds->isPassiveEnumerator(e))
-  {
-    return getModelValue(e);
-  }
-
-  // management of actively generated enumerators goes here
-
-  // 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())
-  {
-    if (d_tds->isVariableAgnosticEnumerator(e))
-    {
-      d_evg[e].reset(new EnumStreamConcrete(d_tds));
-    }
-    else
-    {
-      // Actively-generated enumerators are currently either variable agnostic
-      // or basic. The auto mode always prefers the optimized enumerator over
-      // the basic one.
-      Assert(d_tds->isBasicEnumerator(e));
-      if (options::sygusActiveGenMode()
-          == options::SygusActiveGenMode::ENUM_BASIC)
-      {
-        d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
-      }
-      else
-      {
-        Assert(options::sygusActiveGenMode()
-                   == options::SygusActiveGenMode::ENUM
-               || options::sygusActiveGenMode()
-                      == options::SygusActiveGenMode::AUTO);
-        // 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")
-        << "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];
-  bool firstTime = false;
-  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);
-    firstTime = true;
-  }
-  bool inc = true;
-  if (!firstTime)
-  {
-    inc = iteg->second->increment();
-  }
-  Node v;
-  if (inc)
-  {
-    v = iteg->second->getCurrent();
-  }
-  Trace("sygus-active-gen-debug") << "...generated " << v
-                                  << ", with increment success : " << inc
-                                  << std::endl;
-  if (!inc)
+  std::map<Node, std::unique_ptr<EnumValueManager>>::iterator it =
+      d_enumManager.find(e);
+  if (it != d_enumManager.end())
   {
-    // No more concrete values generated from absE.
-    NodeManager* nm = NodeManager::currentNM();
-    d_ev_curr_active_gen[e] = Node::null();
-    std::vector<Node> exp;
-    // If we are a basic enumerator, a single abstract value maps to *all*
-    // concrete values of its type, thus we don't depend on the current
-    // solution.
-    if (!d_tds->isBasicEnumerator(e))
-    {
-      // We must block e = absE
-      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_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT);
+    return it->second.get();
   }
-  else
+  // otherwise, allocate it
+  Node f = d_tds->getSynthFunForEnumerator(e);
+  bool hasExamples = (d_exampleInfer->hasExamples(f)
+                      && d_exampleInfer->getNumExamples(f) != 0);
+  d_enumManager[e].reset(
+      new EnumValueManager(e, d_qim, d_treg, d_stats, hasExamples));
+  EnumValueManager* eman = d_enumManager[e].get();
+  // set up the examples
+  if (hasExamples)
   {
-    // We are waiting to send e -> v to the module that requested it.
-    if (v.isNull())
-    {
-      activeIncomplete = true;
-    }
-    else
-    {
-      d_ev_active_gen_waiting[e] = v;
-    }
-    if (Trace.isOn("sygus-active-gen"))
+    ExampleEvalCache* eec = eman->getExampleEvalCache();
+    Assert(eec != nullptr);
+    for (unsigned i = 0, nex = d_exampleInfer->getNumExamples(f); i < nex; i++)
     {
-      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;
+      std::vector<Node> input;
+      d_exampleInfer->getExample(f, i, input);
+      eec->addExample(input);
     }
   }
-
-  return v;
+  return eman;
 }
 
 Node SynthConjecture::getModelValue(Node n)
@@ -1291,21 +1149,8 @@ Node SynthConjecture::getSymmetryBreakingPredicate(
 
 ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e)
 {
-  std::map<Node, std::unique_ptr<ExampleEvalCache> >::iterator it =
-      d_exampleEvalCache.find(e);
-  if (it != d_exampleEvalCache.end())
-  {
-    return it->second.get();
-  }
-  Node f = d_tds->getSynthFunForEnumerator(e);
-  // if f does not have examples, we don't construct the utility
-  if (!d_exampleInfer->hasExamples(f) || d_exampleInfer->getNumExamples(f) == 0)
-  {
-    d_exampleEvalCache[e].reset(nullptr);
-    return nullptr;
-  }
-  d_exampleEvalCache[e].reset(new ExampleEvalCache(d_tds, this, f, e));
-  return d_exampleEvalCache[e].get();
+  EnumValueManager* eman = getEnumValueManagerFor(e);
+  return eman->getExampleEvalCache();
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 748ab8b3b..c1635c05c 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -42,6 +42,7 @@ namespace quantifiers {
 class CegGrammarConstructor;
 class SygusPbe;
 class SygusStatistics;
+class EnumValueManager;
 
 /** a synthesis conjecture
  * This class implements approaches for a synthesis conjecture, given by data
@@ -210,8 +211,8 @@ class SynthConjecture
   std::unique_ptr<SygusRepairConst> d_sygus_rconst;
   /** example inference utility */
   std::unique_ptr<ExampleInfer> d_exampleInfer;
-  /** example evaluation cache utility for each enumerator */
-  std::map<Node, std::unique_ptr<ExampleEvalCache> > d_exampleEvalCache;
+  /** map from enumerators to their enumerator manager */
+  std::map<Node, std::unique_ptr<EnumValueManager>> d_enumManager;
 
   //------------------------modules
   /** program by examples module */
@@ -250,40 +251,9 @@ class SynthConjecture
                            std::vector<Node>& v,
                            bool& activeIncomplete);
   /**
-   * Get model value for term n. If n has a value that was excluded by
-   * datatypes sygus symmetry breaking, this method returns null. It sets
-   * activeIncomplete to true if there is an actively-generated enumerator whose
-   * current value is null but it has not finished generating values.
+   * Get or make enumerator manager for the enumerator e.
    */
-  Node getEnumeratedValue(Node n, bool& activeIncomplete);
-  /** 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;
+  EnumValueManager* getEnumValueManagerFor(Node e);
   //------------------------end enumerators
 
   /** list of constants for quantified formula
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 48dce7cf3..c072fd7b4 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -782,6 +782,10 @@ void SygusSampler::registerSygusType(TypeNode tn)
 
 void SygusSampler::checkEquivalent(Node bv, Node bvr)
 {
+  if (bv == bvr)
+  {
+    return;
+  }
   Trace("sygus-rr-verify") << "Testing rewrite rule " << bv << " ---> " << bvr
                            << std::endl;