From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 29 Mar 2021 19:40:53 +0000 (-0500)
Subject: Eliminate the use of quantifiers engine in sygus solver (#6232)
X-Git-Tag: cvc5-1.0.0~2016
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=96ac1d2a5d1f25eaa1b0b265bb21d1a8b3c3d872;p=cvc5.git

Eliminate the use of quantifiers engine in sygus solver (#6232)
---

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 103b32be0..a0b9b20f4 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -21,7 +21,6 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -36,8 +35,7 @@ CandidateRewriteDatabase::CandidateRewriteDatabase(bool doCheck,
                                                    bool rewAccel,
                                                    bool silent,
                                                    bool filterPairs)
-    : d_qe(nullptr),
-      d_tds(nullptr),
+    : d_tds(nullptr),
       d_ext_rewrite(nullptr),
       d_doCheck(doCheck),
       d_rewAccel(rewAccel),
@@ -52,7 +50,6 @@ void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars,
   Assert(ss != nullptr);
   d_candidate = Node::null();
   d_using_sygus = false;
-  d_qe = nullptr;
   d_tds = nullptr;
   d_ext_rewrite = nullptr;
   if (d_filterPairs)
@@ -63,15 +60,14 @@ void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars,
 }
 
 void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars,
-                                               QuantifiersEngine* qe,
+                                               TermDbSygus* tds,
                                                Node f,
                                                SygusSampler* ss)
 {
   Assert(ss != nullptr);
   d_candidate = f;
   d_using_sygus = true;
-  d_qe = qe;
-  d_tds = d_qe->getTermDatabaseSygus();
+  d_tds = tds;
   d_ext_rewrite = nullptr;
   if (d_filterPairs)
   {
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index 3313b507b..321880dc0 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -64,15 +64,14 @@ class CandidateRewriteDatabase : public ExprMiner
    * Serves the same purpose as the above function, but we will be using
    * sygus to enumerate terms and generate samples.
    *
-   * qe : pointer to quantifiers engine. We use the sygus term database of this
-   * quantifiers engine, and the extended rewriter of the corresponding term
+   * tds : pointer to sygus term database. We use the extended rewriter of this
    * database when computing candidate rewrites,
    * f : a term of some SyGuS datatype type whose values we will be
    * testing under the free variables in the grammar of f. This is the
    * "candidate variable" CegConjecture::d_candidates.
    */
   void initializeSygus(const std::vector<Node>& vars,
-                       QuantifiersEngine* qe,
+                       TermDbSygus* tds,
                        Node f,
                        SygusSampler* ss);
   /** add term
@@ -102,8 +101,6 @@ class CandidateRewriteDatabase : public ExprMiner
   void setExtendedRewriter(ExtendedRewriter* er);
 
  private:
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
   /** (required) pointer to the sygus term database of d_qe */
   TermDbSygus* d_tds;
   /** an extended rewriter object */
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index ca9599ba3..fd6a087ca 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -315,16 +315,14 @@ CegHandledStatus CegInstantiator::isCbqiTerm(Node n)
   return ret;
 }
 
-CegHandledStatus CegInstantiator::isCbqiSort(TypeNode tn, QuantifiersEngine* qe)
+CegHandledStatus CegInstantiator::isCbqiSort(TypeNode tn)
 {
   std::map<TypeNode, CegHandledStatus> visited;
-  return isCbqiSort(tn, visited, qe);
+  return isCbqiSort(tn, visited);
 }
 
 CegHandledStatus CegInstantiator::isCbqiSort(
-    TypeNode tn,
-    std::map<TypeNode, CegHandledStatus>& visited,
-    QuantifiersEngine* qe)
+    TypeNode tn, std::map<TypeNode, CegHandledStatus>& visited)
 {
   std::map<TypeNode, CegHandledStatus>::iterator itv = visited.find(tn);
   if (itv != visited.end())
@@ -360,7 +358,7 @@ CegHandledStatus CegInstantiator::isCbqiSort(
       }
       for (const TypeNode& crange : consType)
       {
-        CegHandledStatus cret = isCbqiSort(crange, visited, qe);
+        CegHandledStatus cret = isCbqiSort(crange, visited);
         if (cret == CEG_UNHANDLED)
         {
           Trace("cegqi-debug2")
@@ -380,14 +378,13 @@ CegHandledStatus CegInstantiator::isCbqiSort(
   return ret;
 }
 
-CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q,
-                                                    QuantifiersEngine* qe)
+CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q)
 {
   CegHandledStatus hmin = CEG_HANDLED_UNCONDITIONAL;
   for (const Node& v : q[0])
   {
     TypeNode tn = v.getType();
-    CegHandledStatus handled = isCbqiSort(tn, qe);
+    CegHandledStatus handled = isCbqiSort(tn);
     if (handled == CEG_UNHANDLED)
     {
       return CEG_UNHANDLED;
@@ -400,7 +397,7 @@ CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q,
   return hmin;
 }
 
-CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe)
+CegHandledStatus CegInstantiator::isCbqiQuant(Node q)
 {
   Assert(q.getKind() == FORALL);
   // compute attributes
@@ -428,8 +425,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe)
   }
   CegHandledStatus ret = CEG_HANDLED;
   // if quantifier has a non-handled variable, then do not use cbqi
-  // if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
-  CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q, qe);
+  CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q);
   Trace("cegqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv
                             << std::endl;
   if (ncbqiv == CEG_UNHANDLED)
@@ -668,7 +664,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
   TypeNode pvtn = pv.getType();
   TypeNode pvtnb = pvtn.getBaseType();
   Node pvr = pv;
-  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
   if (ee->hasTerm(pv))
   {
     pvr = ee->getRepresentative(pv);
@@ -1321,7 +1317,7 @@ void CegInstantiator::processAssertions() {
   d_curr_type_eqc.clear();
 
   // must use master equality engine to avoid value instantiations
-  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
 
   //for each variable
   for( unsigned i=0; i<d_vars.size(); i++ ){
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 601650de2..217584de8 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -323,20 +323,14 @@ class CegInstantiator {
    * This method returns whether the type tn is handled by cegqi techniques.
    * If the result is CEG_HANDLED_UNCONDITIONAL, then this indicates that a
    * variable of this type is handled regardless of the formula it appears in.
-   *
-   * The argument qe is used if handling sort tn is conditional on the
-   * strategies initialized in qe. For example, uninterpreted sorts are
-   * handled if dedicated support for EPR is enabled.
    */
-  static CegHandledStatus isCbqiSort(TypeNode tn,
-                                     QuantifiersEngine* qe = nullptr);
+  static CegHandledStatus isCbqiSort(TypeNode tn);
   /** is cbqi quantifier prefix
    *
    * This returns the minimum value of the above method for a bound variable
    * in the prefix of quantified formula q.
    */
-  static CegHandledStatus isCbqiQuantPrefix(Node q,
-                                            QuantifiersEngine* qe = nullptr);
+  static CegHandledStatus isCbqiQuantPrefix(Node q);
   /** is cbqi quantified formula
    *
    * This returns whether quantified formula q can and should be handled by
@@ -348,7 +342,7 @@ class CegInstantiator {
    * quantified formula using cegqi, however other strategies should also be
    * tried.
    */
-  static CegHandledStatus isCbqiQuant(Node q, QuantifiersEngine* qe = nullptr);
+  static CegHandledStatus isCbqiQuant(Node q);
   //------------------------------------ end static queries
  private:
   /** The quantified formula of this instantiator */
@@ -572,9 +566,7 @@ class CegInstantiator {
    * of the type tn, where visited stores the types we have visited.
    */
   static CegHandledStatus isCbqiSort(
-      TypeNode tn,
-      std::map<TypeNode, CegHandledStatus>& visited,
-      QuantifiersEngine* qe);
+      TypeNode tn, std::map<TypeNode, CegHandledStatus>& visited);
   //------------------------------------ end  static queries
 };
 
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 4f66e1034..8318c5f4c 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -410,7 +410,7 @@ bool InstStrategyCegqi::doCbqi(Node q)
 {
   std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
   if( it==d_do_cbqi.end() ){
-    CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine);
+    CegHandledStatus ret = CegInstantiator::isCbqiQuant(q);
     Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
     d_do_cbqi[q] = ret;
     return ret != CEG_UNHANDLED;
diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp
index e482cb05e..6a77d8e45 100644
--- a/src/theory/quantifiers/expr_miner_manager.cpp
+++ b/src/theory/quantifiers/expr_miner_manager.cpp
@@ -13,7 +13,6 @@
  **/
 
 #include "theory/quantifiers/expr_miner_manager.h"
-#include "theory/quantifiers_engine.h"
 
 #include "options/quantifiers_options.h"
 
@@ -26,7 +25,6 @@ ExpressionMinerManager::ExpressionMinerManager()
       d_doQueryGen(false),
       d_doFilterLogicalStrength(false),
       d_use_sygus_type(false),
-      d_qe(nullptr),
       d_tds(nullptr),
       d_crd(options::sygusRewSynthCheck(), options::sygusRewSynthAccel(), false)
 {
@@ -42,13 +40,12 @@ void ExpressionMinerManager::initialize(const std::vector<Node>& vars,
   d_doFilterLogicalStrength = false;
   d_sygus_fun = Node::null();
   d_use_sygus_type = false;
-  d_qe = nullptr;
   d_tds = nullptr;
   // initialize the sampler
   d_sampler.initialize(tn, vars, nsamples, unique_type_ids);
 }
 
-void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe,
+void ExpressionMinerManager::initializeSygus(TermDbSygus* tds,
                                              Node f,
                                              unsigned nsamples,
                                              bool useSygusType)
@@ -58,8 +55,7 @@ void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe,
   d_doFilterLogicalStrength = false;
   d_sygus_fun = f;
   d_use_sygus_type = useSygusType;
-  d_qe = qe;
-  d_tds = qe->getTermDatabaseSygus();
+  d_tds = tds;
   // initialize the sampler
   d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType);
 }
@@ -77,8 +73,8 @@ void ExpressionMinerManager::enableRewriteRuleSynth()
   // initialize the candidate rewrite database
   if (!d_sygus_fun.isNull())
   {
-    Assert(d_qe != nullptr);
-    d_crd.initializeSygus(vars, d_qe, d_sygus_fun, &d_sampler);
+    Assert(d_tds != nullptr);
+    d_crd.initializeSygus(vars, d_tds, d_sygus_fun, &d_sampler);
   }
   else
   {
diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index aa6f3cb31..eb2a01fac 100644
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -65,7 +65,7 @@ class ExpressionMinerManager
    * If useSygusType is false, the terms are the builtin equivalent of these
    * terms. The argument nsamples is used to initialize the sampler.
    */
-  void initializeSygus(QuantifiersEngine* qe,
+  void initializeSygus(TermDbSygus* tds,
                        Node f,
                        unsigned nsamples,
                        bool useSygusType);
@@ -102,9 +102,7 @@ class ExpressionMinerManager
   Node d_sygus_fun;
   /** whether we are using sygus types */
   bool d_use_sygus_type;
-  /** pointer to the quantifiers engine, used if d_use_sygus is true */
-  QuantifiersEngine* d_qe;
-  /** the sygus term database of d_qe */
+  /** the sygus term database of the quantifiers engine */
   TermDbSygus* d_tds;
   /** candidate rewrite database */
   CandidateRewriteDatabase d_crd;
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 066bcd769..c9b2559c1 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -29,7 +29,6 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
@@ -39,12 +38,12 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s)
-    : d_qe(qe),
-      d_sip(new SingleInvocationPartition),
-      d_srcons(new SygusReconstruct(qe->getTermDatabaseSygus(), s)),
+CegSingleInv::CegSingleInv(TermRegistry& tr, SygusStatistics& s)
+    : d_sip(new SingleInvocationPartition),
+      d_srcons(new SygusReconstruct(tr.getTermDatabaseSygus(), s)),
       d_isSolved(false),
-      d_single_invocation(false)
+      d_single_invocation(false),
+      d_treg(tr)
 {
 }
 
@@ -349,7 +348,7 @@ Node CegSingleInv::getSolutionFromInst(size_t index)
       ptn = ptn.getRangeType();
     }
     Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
-    s = d_qe->getTermRegistry().getTermEnumeration()->getEnumerateTerm(ptn, 0);
+    s = d_treg.getTermEnumeration()->getEnumerateTerm(ptn, 0);
   }
   else
   {
@@ -395,7 +394,7 @@ Node CegSingleInv::getSolutionFromInst(size_t index)
   }
   //simplify the solution using the extended rewriter
   Trace("csi-sol") << "Solution (pre-simplification): " << s << std::endl;
-  s = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s);
+  s = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s);
   Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
   // wrap into lambda, as needed
   return SygusUtils::wrapSolutionForSynthFun(prog, s);
@@ -462,7 +461,7 @@ Node CegSingleInv::reconstructToSyntax(Node s,
   {
     Trace("csi-sol") << "Post-process solution..." << std::endl;
     Node prev = sol;
-    sol = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol);
+    sol = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol);
     if (prev != sol)
     {
       Trace("csi-sol") << "Solution (after post process) : " << sol
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index c73954195..8a2ed3a71 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -50,8 +50,6 @@ class CegSingleInv
                                std::map< Node, std::vector< Node > >& teq,
                                Node n, std::vector< Node >& conj );
  private:
-  /** pointer to the quantifiers engine */
-  QuantifiersEngine* d_qe;
   // single invocation inference utility
   SingleInvocationPartition* d_sip;
   /** solution reconstruction */
@@ -92,7 +90,7 @@ class CegSingleInv
   Node d_single_inv;
   
  public:
-  CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s);
+  CegSingleInv(TermRegistry& tr, SygusStatistics& s);
   ~CegSingleInv();
 
   // get simplified conjecture
@@ -164,6 +162,8 @@ class CegSingleInv
    * calls to the above method getSolutionFromInst.
    */
   void setSolution();
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
   /** The conjecture */
   Node d_quant;
   //-------------- decomposed conjecture
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 56743e264..678ce4ce1 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -31,12 +31,13 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-Cegis::Cegis(QuantifiersEngine* qe,
-             QuantifiersInferenceManager& qim,
+Cegis::Cegis(QuantifiersInferenceManager& qim,
+             TermDbSygus* tds,
              SynthConjecture* p)
-    : SygusModule(qe, qim, p), d_eval_unfold(nullptr), d_usingSymCons(false)
+    : SygusModule(qim, tds, p),
+      d_eval_unfold(tds->getEvalUnfold()),
+      d_usingSymCons(false)
 {
-  d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
 }
 
 bool Cegis::initialize(Node conj,
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 0a777a118..9d91a3d66 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -41,9 +41,7 @@ namespace quantifiers {
 class Cegis : public SygusModule
 {
  public:
-  Cegis(QuantifiersEngine* qe,
-        QuantifiersInferenceManager& qim,
-        SynthConjecture* p);
+  Cegis(QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p);
   ~Cegis() override {}
   /** initialize */
   virtual bool initialize(Node conj,
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 3c6ab6bc1..5211251fa 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -70,10 +70,10 @@ bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
   return false;
 }
 
-CegisCoreConnective::CegisCoreConnective(QuantifiersEngine* qe,
-                                         QuantifiersInferenceManager& qim,
+CegisCoreConnective::CegisCoreConnective(QuantifiersInferenceManager& qim,
+                                         TermDbSygus* tds,
                                          SynthConjecture* p)
-    : Cegis(qe, qim, p)
+    : Cegis(qim, tds, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index d20755e47..5b8be444e 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -159,8 +159,8 @@ class VariadicTrie
 class CegisCoreConnective : public Cegis
 {
  public:
-  CegisCoreConnective(QuantifiersEngine* qe,
-                      QuantifiersInferenceManager& qim,
+  CegisCoreConnective(QuantifiersInferenceManager& qim,
+                      TermDbSygus* tds,
                       SynthConjecture* p);
   ~CegisCoreConnective() {}
   /**
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index ce7d058c3..0d4907a58 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -29,11 +29,11 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegisUnif::CegisUnif(QuantifiersEngine* qe,
-                     QuantifiersState& qs,
+CegisUnif::CegisUnif(QuantifiersState& qs,
                      QuantifiersInferenceManager& qim,
+                     TermDbSygus* tds,
                      SynthConjecture* p)
-    : Cegis(qe, qim, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, qim, p)
+    : Cegis(qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p)
 {
 }
 
@@ -59,7 +59,7 @@ bool CegisUnif::processInitialize(Node conj,
   {
     // Init UNIF util for this candidate
     d_sygus_unif.initializeCandidate(
-        d_qe, f, d_cand_to_strat_pt[f], strategy_lemmas);
+        d_tds, f, d_cand_to_strat_pt[f], strategy_lemmas);
     if (!d_sygus_unif.usingUnif(f))
     {
       Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
@@ -401,17 +401,16 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
 }
 
 CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
-    QuantifiersEngine* qe,
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
+    TermDbSygus* tds,
     SynthConjecture* parent)
     : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()),
-      d_qe(qe),
       d_qim(qim),
+      d_tds(tds),
       d_parent(parent)
 {
   d_initialized = false;
-  d_tds = d_qe->getTermDatabaseSygus();
   options::SygusUnifPiMode mode = options::sygusUnifPi();
   d_useCondPool = mode == options::SygusUnifPiMode::CENUM
                   || mode == options::SygusUnifPiMode::CENUM_IGAIN;
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 7bcd3788b..e450c3fa7 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -48,9 +48,9 @@ namespace quantifiers {
 class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 {
  public:
-  CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
-                                QuantifiersState& qs,
+  CegisUnifEnumDecisionStrategy(QuantifiersState& qs,
                                 QuantifiersInferenceManager& qim,
+                                TermDbSygus* tds,
                                 SynthConjecture* parent);
   /** Make the n^th literal of this strategy (G_uq_n).
    *
@@ -101,8 +101,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
   void registerEvalPts(const std::vector<Node>& eis, Node e);
 
  private:
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
   /** sygus term database of d_qe */
@@ -208,9 +206,9 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 class CegisUnif : public Cegis
 {
  public:
-  CegisUnif(QuantifiersEngine* qe,
-            QuantifiersState& qs,
+  CegisUnif(QuantifiersState& qs,
             QuantifiersInferenceManager& qim,
+            TermDbSygus* tds,
             SynthConjecture* p);
   ~CegisUnif() override;
   /** Retrieves enumerators for constructing solutions
diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index d8186e592..e79841c81 100644
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -20,10 +20,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusModule::SygusModule(QuantifiersEngine* qe,
-                         QuantifiersInferenceManager& qim,
+SygusModule::SygusModule(QuantifiersInferenceManager& qim,
+                         TermDbSygus* tds,
                          SynthConjecture* p)
-    : d_qe(qe), d_qim(qim), d_tds(qe->getTermDatabaseSygus()), d_parent(p)
+    : d_qim(qim), d_tds(tds), d_parent(p)
 {
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 86d113edc..9c543c6b6 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -23,9 +23,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
 class SynthConjecture;
@@ -53,8 +50,8 @@ class QuantifiersInferenceManager;
 class SygusModule
 {
  public:
-  SygusModule(QuantifiersEngine* qe,
-              QuantifiersInferenceManager& qim,
+  SygusModule(QuantifiersInferenceManager& qim,
+              TermDbSygus* tds,
               SynthConjecture* p);
   virtual ~SygusModule() {}
   /** initialize
@@ -150,8 +147,6 @@ class SygusModule
   virtual bool usingRepairConst() { return false; }
 
  protected:
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
   /** sygus term database of d_qe */
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index bc9da0c4d..170cf6fd7 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -29,10 +29,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusPbe::SygusPbe(QuantifiersEngine* qe,
-                   QuantifiersInferenceManager& qim,
+SygusPbe::SygusPbe(QuantifiersInferenceManager& qim,
+                   TermDbSygus* tds,
                    SynthConjecture* p)
-    : SygusModule(qe, qim, p)
+    : SygusModule(qim, tds, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -75,7 +75,7 @@ bool SygusPbe::initialize(Node conj,
                        << std::endl;
     std::map<Node, std::vector<Node>> strategy_lemmas;
     d_sygus_unif[c]->initializeCandidate(
-        d_qe, c, d_candidate_to_enum[c], strategy_lemmas);
+        d_tds, c, d_candidate_to_enum[c], strategy_lemmas);
     Assert(!d_candidate_to_enum[c].empty());
     Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
                        << " enumerators for " << c << "..." << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 7b20df8de..cbd307cab 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -85,8 +85,8 @@ class SynthConjecture;
 class SygusPbe : public SygusModule
 {
  public:
-  SygusPbe(QuantifiersEngine* qe,
-           QuantifiersInferenceManager& qim,
+  SygusPbe(QuantifiersInferenceManager& qim,
+           TermDbSygus* tds,
            SynthConjecture* p);
   ~SygusPbe();
 
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index 93474b4ae..e58c209d4 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -520,7 +520,7 @@ void SynthConjectureProcessFun::getIrrelevantArgs(
   }
 }
 
-SynthConjectureProcess::SynthConjectureProcess(QuantifiersEngine* qe) {}
+SynthConjectureProcess::SynthConjectureProcess() {}
 SynthConjectureProcess::~SynthConjectureProcess() {}
 Node SynthConjectureProcess::preSimplify(Node q)
 {
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h
index d4ae48952..5185e549f 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.h
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.h
@@ -276,7 +276,7 @@ struct SynthConjectureProcessFun
 class SynthConjectureProcess
 {
  public:
-  SynthConjectureProcess(QuantifiersEngine* qe);
+  SynthConjectureProcess();
   ~SynthConjectureProcess();
   /** simplify the synthesis conjecture q
    * Returns a formula that is equivalent to q.
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index a96974908..a7d352740 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -27,7 +27,6 @@
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace CVC4::kind;
@@ -36,10 +35,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusRepairConst::SygusRepairConst(QuantifiersEngine* qe)
-    : d_qe(qe), d_allow_constant_grammar(false)
+SygusRepairConst::SygusRepairConst(TermDbSygus* tds)
+    : d_tds(tds), d_allow_constant_grammar(false)
 {
-  d_tds = d_qe->getTermDatabaseSygus();
 }
 
 void SygusRepairConst::initialize(Node base_inst,
@@ -218,7 +216,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   if (fo_body.getKind() == FORALL)
   {
     // must be a CBQI quantifier
-    CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body, d_qe);
+    CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body);
     if (hstatus < CEG_HANDLED)
     {
       // abort if less than fully handled
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index 319497f77..78c17280c 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -25,9 +25,6 @@ namespace CVC4 {
 class LogicInfo;
 
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
 class TermDbSygus;
@@ -50,7 +47,7 @@ class TermDbSygus;
 class SygusRepairConst
 {
  public:
-  SygusRepairConst(QuantifiersEngine* qe);
+  SygusRepairConst(TermDbSygus* tds);
   ~SygusRepairConst() {}
   /** initialize
    *
@@ -107,8 +104,6 @@ class SygusRepairConst
   static bool mustRepair(Node n);
 
  private:
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
   /** pointer to the sygus term database of d_qe */
   TermDbSygus* d_tds;
   /**
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index 4867fc402..621b5153f 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -26,23 +26,19 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusUnif::SygusUnif()
-    : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false)
-{
-}
+SygusUnif::SygusUnif() : d_tds(nullptr), d_enableMinimality(false) {}
 SygusUnif::~SygusUnif() {}
 
 void SygusUnif::initializeCandidate(
-    QuantifiersEngine* qe,
+    TermDbSygus* tds,
     Node f,
     std::vector<Node>& enums,
     std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
-  d_qe = qe;
-  d_tds = qe->getTermDatabaseSygus();
+  d_tds = tds;
   d_candidates.push_back(f);
   // initialize the strategy
-  d_strategy[f].initialize(qe, f, enums);
+  d_strategy[f].initialize(tds, f, enums);
 }
 
 Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index a8a82b2cf..ca5eb0a73 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -23,9 +23,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
 class TermDbSygus;
@@ -67,7 +64,7 @@ class SygusUnif
    * the respective function-to-synthesize.
    */
   virtual void initializeCandidate(
-      QuantifiersEngine* qe,
+      TermDbSygus* tds,
       Node f,
       std::vector<Node>& enums,
       std::map<Node, std::vector<Node>>& strategy_lemmas);
@@ -92,10 +89,8 @@ class SygusUnif
                                  std::vector<Node>& lemmas) = 0;
 
  protected:
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
-  /** sygus term database of d_qe */
-  quantifiers::TermDbSygus* d_tds;
+  /** Pointer to the term database sygus */
+  TermDbSygus* d_tds;
 
   //-----------------------debug printing
   /** print ind indentations on trace c */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index a9891aa72..813aaa2b5 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -20,7 +20,6 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/strings/word.h"
 #include "util/random.h"
@@ -523,7 +522,7 @@ SygusUnifIo::SygusUnifIo(SynthConjecture* p)
 SygusUnifIo::~SygusUnifIo() {}
 
 void SygusUnifIo::initializeCandidate(
-    QuantifiersEngine* qe,
+    TermDbSygus* tds,
     Node f,
     std::vector<Node>& enums,
     std::map<Node, std::vector<Node>>& strategy_lemmas)
@@ -546,7 +545,7 @@ void SygusUnifIo::initializeCandidate(
     }
   }
   d_ecache.clear();
-  SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas);
+  SygusUnif::initializeCandidate(tds, f, enums, strategy_lemmas);
   // learn redundant operators based on the strategy
   d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
 }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index 6bb7ab7c5..d7b0e231c 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -276,7 +276,7 @@ class SygusUnifIo : public SygusUnif
    * multiple functions can be separated.
    */
   void initializeCandidate(
-      QuantifiersEngine* qe,
+      TermDbSygus* tds,
       Node f,
       std::vector<Node>& enums,
       std::map<Node, std::vector<Node>>& strategy_lemmas) override;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index a3cf5ed19..8859ba72b 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -36,14 +36,14 @@ SygusUnifRl::SygusUnifRl(SynthConjecture* p)
 }
 SygusUnifRl::~SygusUnifRl() {}
 void SygusUnifRl::initializeCandidate(
-    QuantifiersEngine* qe,
+    TermDbSygus* tds,
     Node f,
     std::vector<Node>& enums,
     std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
   // initialize
   std::vector<Node> all_enums;
-  SygusUnif::initializeCandidate(qe, f, all_enums, strategy_lemmas);
+  SygusUnif::initializeCandidate(tds, f, all_enums, strategy_lemmas);
   // based on the strategy inferred for each function, determine if we are
   // using a unification strategy that is compatible our approach.
   StrategyRestrictions restrictions;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index dc012c8e4..4c40e39db 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -51,7 +51,7 @@ class SygusUnifRl : public SygusUnif
 
   /** initialize */
   void initializeCandidate(
-      QuantifiersEngine* qe,
+      TermDbSygus* tds,
       Node f,
       std::vector<Node>& enums,
       std::map<Node, std::vector<Node>>& strategy_lemmas) override;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index d9b75fc9d..3a61c5635 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -21,7 +21,6 @@
 #include "theory/quantifiers/sygus/sygus_unif.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -83,14 +82,14 @@ std::ostream& operator<<(std::ostream& os, StrategyType st)
   return os;
 }
 
-void SygusUnifStrategy::initialize(QuantifiersEngine* qe,
+void SygusUnifStrategy::initialize(TermDbSygus* tds,
                                    Node f,
                                    std::vector<Node>& enums)
 {
   Assert(d_candidate.isNull());
   d_candidate = f;
   d_root = f.getType();
-  d_qe = qe;
+  d_tds = tds;
 
   // collect the enumerator types and form the strategy
   buildStrategyGraph(d_root, role_equal);
@@ -263,7 +262,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
     Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren);
     Trace("sygus-unif-debug2") << "  Test evaluation of " << eut << "..."
                                << std::endl;
-    eut = d_qe->getTermDatabaseSygus()->getEvalUnfold()->unfold(eut);
+    eut = d_tds->getEvalUnfold()->unfold(eut);
     Trace("sygus-unif-debug2") << "  ...got " << eut;
     Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index de498dc38..a1d34ad4e 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -22,11 +22,10 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
+class TermDbSygus;
+
 /** roles for enumerators
  *
  * This indicates the role of an enumerator that is allocated by approaches
@@ -279,7 +278,7 @@ struct StrategyRestrictions
 class SygusUnifStrategy
 {
  public:
-  SygusUnifStrategy() : d_qe(nullptr) {}
+  SygusUnifStrategy() : d_tds(nullptr) {}
   /** initialize
    *
    * This initializes this class with function-to-synthesize f. We also call
@@ -288,7 +287,7 @@ class SygusUnifStrategy
    * This call constructs a set of enumerators for the relevant subfields of
    * the grammar of f and adds them to enums.
    */
-  void initialize(QuantifiersEngine* qe, Node f, std::vector<Node>& enums);
+  void initialize(TermDbSygus* tds, Node f, std::vector<Node>& enums);
   /** Get the root enumerator for this class */
   Node getRootEnumerator() const;
   /**
@@ -329,8 +328,8 @@ class SygusUnifStrategy
   void debugPrint(const char* c);
 
  private:
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
+  /** pointer to the term database sygus */
+  TermDbSygus* d_tds;
   /** The candidate variable this strategy is for */
   Node d_candidate;
   /** maps enumerators to relevant information */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index d6afd2f66..72e69afae 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -34,7 +34,6 @@
 #include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
@@ -45,28 +44,28 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
-                                 QuantifiersState& qs,
+SynthConjecture::SynthConjecture(QuantifiersState& qs,
                                  QuantifiersInferenceManager& qim,
                                  QuantifiersRegistry& qr,
+                                 TermRegistry& tr,
                                  SygusStatistics& s)
-    : d_qe(qe),
-      d_qstate(qs),
+    : d_qstate(qs),
       d_qim(qim),
       d_qreg(qr),
+      d_treg(tr),
       d_stats(s),
-      d_tds(qe->getTermDatabaseSygus()),
+      d_tds(tr.getTermDatabaseSygus()),
       d_hasSolution(false),
-      d_ceg_si(new CegSingleInv(qe, s)),
+      d_ceg_si(new CegSingleInv(tr, s)),
       d_templInfer(new SygusTemplateInfer),
-      d_ceg_proc(new SynthConjectureProcess(qe)),
+      d_ceg_proc(new SynthConjectureProcess),
       d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
-      d_sygus_rconst(new SygusRepairConst(qe)),
+      d_sygus_rconst(new SygusRepairConst(d_tds)),
       d_exampleInfer(new ExampleInfer(d_tds)),
-      d_ceg_pbe(new SygusPbe(qe, qim, this)),
-      d_ceg_cegis(new Cegis(qe, qim, this)),
-      d_ceg_cegisUnif(new CegisUnif(qe, qs, qim, this)),
-      d_sygus_ccore(new CegisCoreConnective(qe, qim, this)),
+      d_ceg_pbe(new SygusPbe(qim, d_tds, this)),
+      d_ceg_cegis(new Cegis(qim, d_tds, this)),
+      d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)),
+      d_sygus_ccore(new CegisCoreConnective(qim, d_tds, this)),
       d_master(nullptr),
       d_set_ce_sk_vars(false),
       d_repair_index(0),
@@ -409,10 +408,11 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     {
       Trace("sygus-engine") << "  * Value is : ";
       std::stringstream sygusEnumOut;
+      FirstOrderModel* m = d_treg.getModel();
       for (unsigned i = 0, size = terms.size(); i < size; i++)
       {
         Node nv = enum_values[i];
-        Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv;
+        Node onv = nv.isNull() ? m->getValue(terms[i]) : nv;
         TypeNode tn = onv.getType();
         std::stringstream ss;
         TermDbSygus::toStreamSygus(ss, onv);
@@ -969,7 +969,7 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
 Node SynthConjecture::getModelValue(Node n)
 {
   Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
-  return d_qe->getModel()->getValue(n);
+  return d_treg.getModel()->getValue(n);
 }
 
 void SynthConjecture::debugPrint(const char* c)
@@ -1071,7 +1071,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
         if (its == d_exprm.end())
         {
           d_exprm[prog].initializeSygus(
-              d_qe, d_candidates[i], options::sygusSamples(), true);
+              d_tds, d_candidates[i], options::sygusSamples(), true);
           if (options::sygusRewSynth())
           {
             d_exprm[prog].enableRewriteRuleSynth();
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 1b9f656bd..efb559889 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -81,10 +81,10 @@ class EnumValGenerator
 class SynthConjecture
 {
  public:
-  SynthConjecture(QuantifiersEngine* qe,
-                  QuantifiersState& qs,
+  SynthConjecture(QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
+                  TermRegistry& tr,
                   SygusStatistics& s);
   ~SynthConjecture();
   /** presolve */
@@ -203,14 +203,14 @@ class SynthConjecture
   SygusStatistics& getSygusStatistics() { return d_stats; };
 
  private:
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
   /** The quantifiers registry */
   QuantifiersRegistry& d_qreg;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
   /** reference to the statistics of parent */
   SygusStatistics& d_stats;
   /** term database sygus of d_qe */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index d77a42a14..f4d50118e 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -15,11 +15,10 @@
  **/
 #include "theory/quantifiers/sygus/synth_engine.h"
 
-#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/term_registry.h"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -34,12 +33,11 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr)
     : QuantifiersModule(qs, qim, qr, tr, qe),
-      d_tds(tr.getTermDatabaseSygus()),
       d_conj(nullptr),
       d_sqp(qe)
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-      new SynthConjecture(d_quantEngine, qs, qim, qr, d_statistics)));
+      new SynthConjecture(qs, qim, qr, tr, d_statistics)));
   d_conj = d_conjs.back().get();
 }
 
@@ -159,8 +157,8 @@ void SynthEngine::assignConjecture(Node q)
   // allocate a new synthesis conjecture if not assigned
   if (d_conjs.back()->isAssigned())
   {
-    d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture(
-        d_quantEngine, d_qstate, d_qim, d_qreg, d_statistics)));
+    d_conjs.push_back(std::unique_ptr<SynthConjecture>(
+        new SynthConjecture(d_qstate, d_qim, d_qreg, d_treg, d_statistics)));
   }
   d_conjs.back()->assign(q);
 }
@@ -190,7 +188,7 @@ void SynthEngine::registerQuantifier(Node q)
     // If it is a recursive function definition, add it to the function
     // definition evaluator class.
     Trace("cegqi") << "Registering function definition : " << q << "\n";
-    FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
+    FunDefEvaluator* fde = d_treg.getTermDatabaseSygus()->getFunDefEvaluator();
     fde->assertDefinition(q);
     return;
   }
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index a4bed1737..4644c5877 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -81,8 +81,6 @@ class SynthEngine : public QuantifiersModule
   void preregisterAssertion(Node n);
 
  private:
-  /** term database sygus of d_qe */
-  TermDbSygus* d_tds;
   /** the conjecture formula(s) we are waiting to assign */
   std::vector<Node> d_waiting_conj;
   /** The synthesis conjectures that this class is managing. */