Move methods from term util to quantifiers registry (#5916)

Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.

Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.

51 files changed, 613 insertions, 454 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 12e3f24b3..654ccb40c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -726,6 +726,8 @@ libcvc4_add_sources(
   theory/quantifiers/quant_split.h
   theory/quantifiers/quant_util.cpp
   theory/quantifiers/quant_util.h
+  theory/quantifiers/quant_module.cpp
+  theory/quantifiers/quant_module.h
   theory/quantifiers/quantifiers_attributes.cpp
   theory/quantifiers/quantifiers_attributes.h
   theory/quantifiers/quantifiers_inference_manager.cpp
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 69b665854..eef0326b6 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -24,8 +24,8 @@
 #include "smt/smt_engine_scope.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 
@@ -196,8 +196,8 @@ bool QuantifierMacros::isGroundUfTerm(Node q, Node n)
 {
   Node icn = d_preprocContext->getTheoryEngine()
                  ->getQuantifiersEngine()
-                 ->getTermUtil()
-                 ->substituteBoundVariablesToInstConstants(n, q);
+                 ->getQuantifiersRegistry()
+                 .substituteBoundVariablesToInstConstants(n, q);
   Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
   std::vector< Node > var;
   quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var);
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index c37054fdd..e4881b112 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -103,7 +103,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
     //add cbqi lemma
     //get the counterexample literal
     Node ceLit = getCounterexampleLiteral(q);
-    Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q );
+    Node ceBody = d_qreg.getInstConstantBody(q);
     if( !ceBody.isNull() ){
       //add counterexample lemma
       Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
@@ -369,19 +369,18 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
   // must register with the instantiator
   // must explicitly remove ITEs so that we record dependencies
   std::vector<Node> ce_vars;
-  TermUtil* tutil = d_quantEngine->getTermUtil();
-  for (unsigned i = 0, nics = tutil->getNumInstantiationConstants(q); i < nics;
+  for (size_t i = 0, nics = d_qreg.getNumInstantiationConstants(q); i < nics;
        i++)
   {
-    ce_vars.push_back(tutil->getInstantiationConstant(q, i));
+    ce_vars.push_back(d_qreg.getInstantiationConstant(q, i));
   }
   // send the lemma
-  d_quantEngine->getOutputChannel().lemma(lem);
+  d_qim.lemma(lem, InferenceId::UNKNOWN);
   // get the preprocessed form of the lemma we just sent
   std::vector<Node> skolems;
   std::vector<Node> skAsserts;
-  Node ppLem = d_quantEngine->getValuation().getPreprocessedTerm(
-      lem, skAsserts, skolems);
+  Node ppLem =
+      d_qstate.getValuation().getPreprocessedTerm(lem, skAsserts, skolems);
   std::vector<Node> lemp{ppLem};
   lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end());
   ppLem = NodeManager::currentNM()->mkAnd(lemp);
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 7d39efc6b..18c71e77e 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -24,7 +24,7 @@
 #include "theory/quantifiers/cegqi/nested_qe.h"
 #include "theory/quantifiers/cegqi/vts_term_cache.h"
 #include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 644461da2..9a9492d00 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -20,7 +20,7 @@
 #include "context/cdhashmap.h"
 #include "expr/node_trie.h"
 #include "expr/term_canonize.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
 #include "theory/type_enumerator.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 0ab2988d2..4c606a273 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -17,7 +17,6 @@
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/theory_uf_rewriter.h"
 #include "util/hash.h"
@@ -31,10 +30,11 @@ namespace inst {
 HigherOrderTrigger::HigherOrderTrigger(
     QuantifiersEngine* qe,
     quantifiers::QuantifiersInferenceManager& qim,
+    quantifiers::QuantifiersRegistry& qr,
     Node q,
     std::vector<Node>& nodes,
     std::map<Node, std::vector<Node> >& ho_apps)
-    : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps)
+    : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
 {
   NodeManager* nm = NodeManager::currentNM();
   // process the higher-order variable applications
@@ -201,11 +201,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
     // get substitution corresponding to m
     std::vector<TNode> vars;
     std::vector<TNode> subs;
-    quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil();
     for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
     {
       subs.push_back(m.d_vals[i]);
-      vars.push_back(tutil->getInstantiationConstant(d_quant, i));
+      vars.push_back(d_qreg.getInstantiationConstant(d_quant, i));
     }
 
     Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl;
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index e424f69d1..af7020bfc 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -94,6 +94,7 @@ class HigherOrderTrigger : public Trigger
  private:
   HigherOrderTrigger(QuantifiersEngine* qe,
                      quantifiers::QuantifiersInferenceManager& qim,
+                     quantifiers::QuantifiersRegistry& qr,
                      Node q,
                      std::vector<Node>& nodes,
                      std::map<Node, std::vector<Node> >& ho_apps);
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index a0114ba80..4f393bc4f 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -238,8 +238,6 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
   if (trieIndex < iio->d_order.size())
   {
     size_t curr_index = iio->d_order[trieIndex];
-    // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
-    // curr_index );
     Node n = m.get(curr_index);
     if (n.isNull())
     {
diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp
index fc85703c0..fe771b4e7 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy.cpp
@@ -22,8 +22,9 @@ namespace quantifiers {
 
 InstStrategy::InstStrategy(QuantifiersEngine* qe,
                            QuantifiersState& qs,
-                           QuantifiersInferenceManager& qim)
-    : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
+                           QuantifiersInferenceManager& qim,
+                           QuantifiersRegistry& qr)
+    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
 {
 }
 InstStrategy::~InstStrategy() {}
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index b9d0aa745..1455ce0c5 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -31,6 +31,7 @@ namespace quantifiers {
 
 class QuantifiersState;
 class QuantifiersInferenceManager;
+class QuantifiersRegistry;
 
 /** A status response to process */
 enum class InstStrategyStatus
@@ -49,7 +50,8 @@ class InstStrategy
  public:
   InstStrategy(QuantifiersEngine* qe,
                QuantifiersState& qs,
-               QuantifiersInferenceManager& qim);
+               QuantifiersInferenceManager& qim,
+               QuantifiersRegistry& qr);
   virtual ~InstStrategy();
   /** presolve */
   virtual void presolve();
@@ -72,6 +74,8 @@ class InstStrategy
   QuantifiersState& d_qstate;
   /** The quantifiers inference manager object */
   QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  QuantifiersRegistry& d_qreg;
 }; /* class InstStrategy */
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 90d8de128..2a1e38c3c 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -62,8 +62,9 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(
     QuantifiersEngine* qe,
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
-    QuantRelevance* qr)
-    : InstStrategy(qe, qs, qim), d_quant_rel(qr)
+    QuantifiersRegistry& qr,
+    QuantRelevance* qrlv)
+    : InstStrategy(qe, qs, qim, qr), d_quant_rel(qrlv)
 {
   //how to select trigger terms
   d_tr_strategy = options::triggerSelMode();
@@ -283,6 +284,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     {
       tr = Trigger::mkTrigger(d_quantEngine,
                               d_qim,
+                              d_qreg,
                               f,
                               patTerms[0],
                               false,
@@ -320,6 +322,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       // will possibly want to get an old trigger
       tr = Trigger::mkTrigger(d_quantEngine,
                               d_qim,
+                              d_qreg,
                               f,
                               patTerms,
                               false,
@@ -362,6 +365,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
           d_single_trigger_gen[patTerms[index]] = true;
           Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
                                             d_qim,
+                                            d_qreg,
                                             f,
                                             patTerms[index],
                                             false,
@@ -390,7 +394,6 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
   bool ntrivTriggers = options::relationalTriggers();
   std::vector<Node> patTermsF;
   std::map<Node, inst::TriggerTermInfo> tinfo;
-  TermUtil* tu = d_quantEngine->getTermUtil();
   NodeManager* nm = NodeManager::currentNM();
   // well-defined function: can assume LHS is only pattern
   if (options::quantFunWellDefined())
@@ -398,7 +401,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
     Node hd = QuantAttributes::getFunDefHead(f);
     if (!hd.isNull())
     {
-      hd = tu->substituteBoundVariablesToInstConstants(hd, f);
+      hd = d_qreg.substituteBoundVariablesToInstConstants(hd, f);
       patTermsF.push_back(hd);
       tinfo[hd].init(f, hd);
     }
@@ -406,7 +409,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
   // otherwise, use algorithm for collecting pattern terms
   if (patTermsF.empty())
   {
-    Node bd = tu->getInstConstantBody(f);
+    Node bd = d_qreg.getInstConstantBody(f);
     PatternTermSelector pts(f, d_tr_strategy, d_user_no_gen[f], true);
     pts.collect(bd, patTermsF, tinfo);
     if (ntrivTriggers)
@@ -486,7 +489,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
       std::vector<Node> vcs[2];
       for (size_t i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
       {
-        Node ic = tu->getInstantiationConstant(f, i);
+        Node ic = d_qreg.getInstantiationConstant(f, i);
         vcs[vcMap.find(ic) == vcMap.end() ? 0 : 1].push_back(f[0][i]);
       }
       for (size_t i = 0; i < 2; i++)
@@ -621,8 +624,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
     NodeManager* nm = NodeManager::currentNM();
     // partial trigger : generate implication to mark user pattern
     Node pat =
-        d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables(
-            tr->getInstPattern(), q);
+        d_qreg.substituteInstConstantsToBoundVariables(tr->getInstPattern(), q);
     Node ipl = nm->mkNode(INST_PATTERN_LIST, pat);
     Node qq = nm->mkNode(FORALL,
                          d_vc_partition[1][q],
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index 81b40f067..6170d3067 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -88,7 +88,8 @@ class InstStrategyAutoGenTriggers : public InstStrategy
   InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
                               QuantifiersState& qs,
                               QuantifiersInferenceManager& qim,
-                              QuantRelevance* qr);
+                              QuantifiersRegistry& qr,
+                              QuantRelevance* qrlv);
   ~InstStrategyAutoGenTriggers() {}
 
   /** get auto-generated trigger */
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index cf6405b38..ca2f1bdc5 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -27,8 +27,9 @@ namespace quantifiers {
 InstStrategyUserPatterns::InstStrategyUserPatterns(
     QuantifiersEngine* ie,
     QuantifiersState& qs,
-    QuantifiersInferenceManager& qim)
-    : InstStrategy(ie, qs, qim)
+    QuantifiersInferenceManager& qim,
+    QuantifiersRegistry& qr)
+    : InstStrategy(ie, qs, qim, qr)
 {
 }
 InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
@@ -105,8 +106,13 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q,
     std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q];
     for (size_t i = 0, usize = ugw.size(); i < usize; i++)
     {
-      Trigger* t = Trigger::mkTrigger(
-          d_quantEngine, d_qim, q, ugw[i], true, Trigger::TR_RETURN_NULL);
+      Trigger* t = Trigger::mkTrigger(d_quantEngine,
+                                      d_qim,
+                                      d_qreg,
+                                      q,
+                                      ugw[i],
+                                      true,
+                                      Trigger::TR_RETURN_NULL);
       if (t)
       {
         d_user_gen[q].push_back(t);
@@ -165,7 +171,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
     return;
   }
   Trigger* t = Trigger::mkTrigger(
-      d_quantEngine, d_qim, q, nodes, true, Trigger::TR_MAKE_NEW);
+      d_quantEngine, d_qim, d_qreg, q, nodes, true, Trigger::TR_MAKE_NEW);
   if (t)
   {
     d_user_gen[q].push_back(t);
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
index 996adc444..1cad77fef 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -36,7 +36,8 @@ class InstStrategyUserPatterns : public InstStrategy
  public:
   InstStrategyUserPatterns(QuantifiersEngine* qe,
                            QuantifiersState& qs,
-                           QuantifiersInferenceManager& qim);
+                           QuantifiersInferenceManager& qim,
+                           QuantifiersRegistry& qr);
   ~InstStrategyUserPatterns();
   /** add pattern */
   void addUserPattern(Node q, Node pat);
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 50d91a1e1..3e344f7fb 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -53,13 +53,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
     // user-provided patterns
     if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
     {
-      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim));
+      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr));
       d_instStrategies.push_back(d_isup.get());
     }
 
     // auto-generated patterns
     d_i_ag.reset(new InstStrategyAutoGenTriggers(
-        d_quantEngine, qs, qim, d_quant_rel.get()));
+        d_quantEngine, qs, qim, qr, d_quant_rel.get()));
     d_instStrategies.push_back(d_i_ag.get());
   }
 }
@@ -228,9 +228,7 @@ void InstantiationEngine::registerQuantifier(Node q)
   // take into account user patterns
   if (q.getNumChildren() == 3)
   {
-    Node subsPat =
-        d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
-            q[2], q);
+    Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
     // add patterns
     for (const Node& p : subsPat)
     {
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 016784152..e27277933 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -20,8 +20,8 @@
 #include <vector>
 
 #include "theory/quantifiers/ematching/inst_strategy.h"
+#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quant_relevance.h"
-#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 3bc5ded16..ac43d3bc9 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -36,9 +36,10 @@ namespace inst {
 /** trigger class constructor */
 Trigger::Trigger(QuantifiersEngine* qe,
                  quantifiers::QuantifiersInferenceManager& qim,
+                 quantifiers::QuantifiersRegistry& qr,
                  Node q,
                  std::vector<Node>& nodes)
-    : d_quantEngine(qe), d_qim(qim), d_quant(q)
+    : d_quantEngine(qe), d_qim(qim), d_qreg(qr), d_quant(q)
 {
   // We must ensure that the ground subterms of the trigger have been
   // preprocessed.
@@ -233,6 +234,7 @@ bool Trigger::mkTriggerTerms(Node q,
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
                             quantifiers::QuantifiersInferenceManager& qim,
+                            quantifiers::QuantifiersRegistry& qr,
                             Node f,
                             std::vector<Node>& nodes,
                             bool keepAll,
@@ -273,11 +275,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
   Trigger* t;
   if (!ho_apps.empty())
   {
-    t = new HigherOrderTrigger(qe, qim, f, trNodes, ho_apps);
+    t = new HigherOrderTrigger(qe, qim, qr, f, trNodes, ho_apps);
   }
   else
   {
-    t = new Trigger(qe, qim, f, trNodes);
+    t = new Trigger(qe, qim, qr, f, trNodes);
   }
 
   qe->getTriggerDatabase()->addTrigger( trNodes, t );
@@ -286,6 +288,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
                             quantifiers::QuantifiersInferenceManager& qim,
+                            quantifiers::QuantifiersRegistry& qr,
                             Node f,
                             Node n,
                             bool keepAll,
@@ -294,7 +297,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 {
   std::vector< Node > nodes;
   nodes.push_back( n );
-  return mkTrigger(qe, qim, f, nodes, keepAll, trOption, useNVars);
+  return mkTrigger(qe, qim, qr, f, nodes, keepAll, trOption, useNVars);
 }
 
 int Trigger::getActiveScore() {
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index e2ce61bd1..21888ff8f 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -31,6 +31,7 @@ class QuantifiersEngine;
 
 namespace quantifiers {
 class QuantifiersInferenceManager;
+class QuantifiersRegistry;
 }
 
 namespace inst {
@@ -163,6 +164,7 @@ class Trigger {
   };
   static Trigger* mkTrigger(QuantifiersEngine* qe,
                             quantifiers::QuantifiersInferenceManager& qim,
+                            quantifiers::QuantifiersRegistry& qr,
                             Node q,
                             std::vector<Node>& nodes,
                             bool keepAll = true,
@@ -171,6 +173,7 @@ class Trigger {
   /** single trigger version that calls the above function */
   static Trigger* mkTrigger(QuantifiersEngine* qe,
                             quantifiers::QuantifiersInferenceManager& qim,
+                            quantifiers::QuantifiersRegistry& qr,
                             Node q,
                             Node n,
                             bool keepAll = true,
@@ -194,6 +197,7 @@ class Trigger {
   /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
   Trigger(QuantifiersEngine* ie,
           quantifiers::QuantifiersInferenceManager& qim,
+          quantifiers::QuantifiersRegistry& qr,
           Node q,
           std::vector<Node>& nodes);
   /** add an instantiation (called by InstMatchGenerator)
@@ -243,6 +247,8 @@ class Trigger {
   QuantifiersEngine* d_quantEngine;
   /** Reference to the quantifiers inference manager */
   quantifiers::QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  quantifiers::QuantifiersRegistry& d_qreg;
   /** The quantified formula this trigger is for. */
   Node d_quant;
   /** match generator
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 37a3396e2..7b5bd92b8 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 #include "theory/strings/sequences_rewriter.h"
+#include "theory/theory.h"
 
 using namespace CVC4::kind;
 using namespace std;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index db977c53d..593ec98f9 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -35,9 +35,11 @@ namespace quantifiers {
 
 FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe,
                                  QuantifiersState& qs,
+                                 QuantifiersRegistry& qr,
                                  std::string name)
     : TheoryModel(qs.getSatContext(), name, true),
       d_qe(qe),
+      d_qreg(qr),
       d_forall_asserts(qs.getSatContext()),
       d_forallRlvComputed(false)
 {
@@ -301,8 +303,7 @@ Node FirstOrderModel::getModelBasis(Node q, Node n)
       d_model_basis_terms[q].push_back(getModelBasisTerm(q[0][j].getType()));
     }
   }
-  Node gn = d_qe->getTermUtil()->substituteInstConstants(
-      n, q, d_model_basis_terms[q]);
+  Node gn = d_qreg.substituteInstConstants(n, q, d_model_basis_terms[q]);
   return gn;
 }
 
@@ -337,8 +338,9 @@ unsigned FirstOrderModel::getModelBasisArg(Node n)
 
 FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe,
                                        QuantifiersState& qs,
+                                       QuantifiersRegistry& qr,
                                        std::string name)
-    : FirstOrderModel(qe, qs, name)
+    : FirstOrderModel(qe, qs, qr, name)
 {
 }
 
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index e4236a95d..ebc68ca53 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -19,7 +19,6 @@
 
 #include "context/cdlist.h"
 #include "expr/attribute.h"
-#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
 
@@ -43,6 +42,8 @@ typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t>
 namespace quantifiers {
 
 class TermDb;
+class QuantifiersState;
+class QuantifiersRegistry;
 
 namespace fmcheck {
   class FirstOrderModelFmc;
@@ -57,6 +58,7 @@ class FirstOrderModel : public TheoryModel
  public:
   FirstOrderModel(QuantifiersEngine* qe,
                   QuantifiersState& qs,
+                  QuantifiersRegistry& qr,
                   std::string name);
 
   virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
@@ -134,6 +136,8 @@ class FirstOrderModel : public TheoryModel
  protected:
   /** quant engine */
   QuantifiersEngine* d_qe;
+  /** The quantifiers registry */
+  QuantifiersRegistry& d_qreg;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
   /** 
@@ -203,6 +207,7 @@ class FirstOrderModelFmc : public FirstOrderModel
  public:
   FirstOrderModelFmc(QuantifiersEngine* qe,
                      QuantifiersState& qs,
+                     QuantifiersRegistry& qr,
                      std::string name);
   ~FirstOrderModelFmc() override;
   FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 5a0407f1f..3ade304e8 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -546,7 +546,7 @@ void BoundedIntegers::getBoundVarIndices(Node q,
   {
     for (const Node& v : it->second)
     {
-      indices.push_back(d_quantEngine->getTermUtil()->getVariableNum(q, v));
+      indices.push_back(TermUtil::getVariableNum(q, v));
     }
   }
 }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 74ff8a19b..dce515d0d 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -18,7 +18,7 @@
 #ifndef CVC4__BOUNDED_INTEGERS_H
 #define CVC4__BOUNDED_INTEGERS_H
 
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
 
 #include "context/cdhashmap.h"
 #include "context/context.h"
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 428c435df..1c0a74013 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -21,7 +21,6 @@
 #include "theory/quantifiers/quant_rep_bound_ext.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace std;
@@ -268,7 +267,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     if( Trace.isOn("fmf-exh-inst-debug") ){
       Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
       for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-        Trace("fmf-exh-inst-debug") << d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ) << " ";
+        Trace("fmf-exh-inst-debug")
+            << d_qreg.getInstantiationConstant(f, i) << " ";
       }
       Trace("fmf-exh-inst-debug") << std::endl;
     }
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 1cb780dd0..b3006cad1 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -18,7 +18,7 @@
 #define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 
 #include "theory/quantifiers/fmf/model_builder.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 5d6779406..96e8a40be 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/inst_match.h"
 
 #include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index 35c43d740..1c606998a 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -19,7 +19,7 @@
 
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index b4fed5b13..729dd6100 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -39,13 +39,14 @@ namespace quantifiers {
 Instantiate::Instantiate(QuantifiersEngine* qe,
                          QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
+                         QuantifiersRegistry& qr,
                          ProofNodeManager* pnm)
     : d_qe(qe),
       d_qstate(qs),
       d_qim(qim),
+      d_qreg(qr),
       d_pnm(pnm),
       d_term_db(nullptr),
-      d_term_util(nullptr),
       d_total_inst_debug(qs.getUserContext()),
       d_c_inst_match_trie_dom(qs.getUserContext()),
       d_pfInst(pnm ? new CDProof(pnm) : nullptr)
@@ -75,7 +76,6 @@ bool Instantiate::reset(Theory::Effort e)
     d_recorded_inst.clear();
   }
   d_term_db = d_qe->getTermDatabase();
-  d_term_util = d_qe->getTermUtil();
   return true;
 }
 
@@ -111,7 +111,6 @@ bool Instantiate::addInstantiation(
   Assert(!d_qstate.isInConflict());
   Assert(terms.size() == q[0].getNumChildren());
   Assert(d_term_db != nullptr);
-  Assert(d_term_util != nullptr);
   Trace("inst-add-debug") << "For quantified formula " << q
                           << ", add instantiation: " << std::endl;
   for (unsigned i = 0, size = terms.size(); i < size; i++)
@@ -167,7 +166,7 @@ bool Instantiate::addInstantiation(
                         << terms[i] << std::endl;
           bad_inst = true;
         }
-        else if (expr::hasSubterm(terms[i], d_term_util->d_inst_constants[q]))
+        else if (expr::hasSubterm(terms[i], d_qreg.d_inst_constants[q]))
         {
           Trace("inst") << "***& inst contains inst constants : " << terms[i]
                         << std::endl;
@@ -250,10 +249,9 @@ bool Instantiate::addInstantiation(
 
   // construct the instantiation
   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
-  Assert(d_term_util->d_vars[q].size() == terms.size());
+  Assert(d_qreg.d_vars[q].size() == terms.size());
   // get the instantiation
-  Node body =
-      getInstantiation(q, d_term_util->d_vars[q], terms, doVts, pfTmp.get());
+  Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get());
   Node orig_body = body;
   // now preprocess, storing the trust node for the rewrite
   TrustNode tpBody = quantifiers::QuantifiersRewriter::preprocess(body, true);
@@ -466,15 +464,15 @@ Node Instantiate::getInstantiation(Node q,
 
 Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts)
 {
-  Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end());
+  Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
   Assert(m.d_vals.size() == q[0].getNumChildren());
-  return getInstantiation(q, d_term_util->d_vars[q], m.d_vals, doVts);
+  return getInstantiation(q, d_qreg.d_vars[q], m.d_vals, doVts);
 }
 
 Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
 {
-  Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end());
-  return getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
+  Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
+  return getInstantiation(q, d_qreg.d_vars[q], terms, doVts);
 }
 
 bool Instantiate::recordInstantiationInternal(Node q,
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index aad1762c5..4188311ec 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -33,7 +33,9 @@ class QuantifiersEngine;
 namespace quantifiers {
 
 class TermDb;
-class TermUtil;
+class QuantifiersState;
+class QuantifiersInferenceManager;
+class QuantifiersRegistry;
 
 /** Instantiation rewriter
  *
@@ -91,6 +93,7 @@ class Instantiate : public QuantifiersUtil
   Instantiate(QuantifiersEngine* qe,
               QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
+              QuantifiersRegistry& qr,
               ProofNodeManager* pnm = nullptr);
   ~Instantiate();
 
@@ -293,12 +296,12 @@ class Instantiate : public QuantifiersUtil
   QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  QuantifiersRegistry& d_qreg;
   /** pointer to the proof node manager */
   ProofNodeManager* d_pnm;
   /** cache of term database for quantifiers engine */
   TermDb* d_term_db;
-  /** cache of term util for quantifiers engine */
-  TermUtil* d_term_util;
   /** instantiation rewriter classes */
   std::vector<InstantiationRewriter*> d_instRewrite;
 
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 0829ccd9c..f89f9f0ea 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -628,8 +628,8 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
     //check constraints
     for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
       //apply substitution to the tconstraint
-      Node cons =
-          p->getTermUtil()->substituteBoundVariables(it->first, d_q, terms);
+      Node cons = p->getQuantifiersRegistry().substituteBoundVariables(
+          it->first, d_q, terms);
       cons = it->second ? cons : cons.negate();
       if (!entailmentTest(p, cons, p->atConflictEffort())) {
         return true;
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 086d492f4..aea03984c 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -23,7 +23,7 @@
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node_trie.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp
new file mode 100644
index 000000000..1d2da7e79
--- /dev/null
+++ b/src/theory/quantifiers/quant_module.cpp
@@ -0,0 +1,92 @@
+/*********************                                                        */
+/*! \file quant_module.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Implementation of quantifier module
+ **/
+
+#include "theory/quantifiers/quant_module.h"
+#include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+QuantifiersModule::QuantifiersModule(
+    quantifiers::QuantifiersState& qs,
+    quantifiers::QuantifiersInferenceManager& qim,
+    quantifiers::QuantifiersRegistry& qr,
+    QuantifiersEngine* qe)
+    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
+{
+}
+
+QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
+{
+  return QEFFORT_NONE;
+}
+
+eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
+{
+  return d_qstate.getEqualityEngine();
+}
+
+bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
+{
+  return d_qstate.areEqual(n1, n2);
+}
+
+bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const
+{
+  return d_qstate.areDisequal(n1, n2);
+}
+
+TNode QuantifiersModule::getRepresentative(TNode n) const
+{
+  return d_qstate.getRepresentative(n);
+}
+
+QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const
+{
+  return d_quantEngine;
+}
+
+quantifiers::TermDb* QuantifiersModule::getTermDatabase() const
+{
+  return d_quantEngine->getTermDatabase();
+}
+
+quantifiers::TermUtil* QuantifiersModule::getTermUtil() const
+{
+  return d_quantEngine->getTermUtil();
+}
+
+quantifiers::QuantifiersState& QuantifiersModule::getState()
+{
+  return d_qstate;
+}
+
+quantifiers::QuantifiersInferenceManager&
+QuantifiersModule::getInferenceManager()
+{
+  return d_qim;
+}
+
+quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry()
+{
+  return d_qreg;
+}
+
+}  // namespace theory
+} /* namespace CVC4 */
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
new file mode 100644
index 000000000..4d0481484
--- /dev/null
+++ b/src/theory/quantifiers/quant_module.h
@@ -0,0 +1,186 @@
+/*********************                                                        */
+/*! \file quant_module.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief quantifier module
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANT_MODULE_H
+#define CVC4__THEORY__QUANT_MODULE_H
+
+#include <iostream>
+#include <map>
+#include <vector>
+
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_registry.h"
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers {
+class TermDb;
+class TermUtil;
+}  // namespace quantifiers
+
+/** QuantifiersModule class
+ *
+ * This is the virtual class for defining subsolvers of the quantifiers theory.
+ * It has a similar interface to a Theory object.
+ */
+class QuantifiersModule
+{
+ public:
+  /** effort levels for quantifiers modules check */
+  enum QEffort
+  {
+    // conflict effort, for conflict-based instantiation
+    QEFFORT_CONFLICT,
+    // standard effort, for heuristic instantiation
+    QEFFORT_STANDARD,
+    // model effort, for model-based instantiation
+    QEFFORT_MODEL,
+    // last call effort, for last resort techniques
+    QEFFORT_LAST_CALL,
+    // none
+    QEFFORT_NONE,
+  };
+
+ public:
+  QuantifiersModule(quantifiers::QuantifiersState& qs,
+                    quantifiers::QuantifiersInferenceManager& qim,
+                    quantifiers::QuantifiersRegistry& qr,
+                    QuantifiersEngine* qe);
+  virtual ~QuantifiersModule() {}
+  /** Presolve.
+   *
+   * Called at the beginning of check-sat call.
+   */
+  virtual void presolve() {}
+  /** Needs check.
+   *
+   * Returns true if this module wishes a call to be made
+   * to check(e) during QuantifiersEngine::check(e).
+   */
+  virtual bool needsCheck(Theory::Effort e)
+  {
+    return e >= Theory::EFFORT_LAST_CALL;
+  }
+  /** Needs model.
+   *
+   * Whether this module needs a model built during a
+   * call to QuantifiersEngine::check(e)
+   * It returns one of QEFFORT_* from quantifiers_engine.h,
+   * which specifies the quantifiers effort in which it requires the model to
+   * be built.
+   */
+  virtual QEffort needsModel(Theory::Effort e);
+  /** Reset.
+   *
+   * Called at the beginning of QuantifiersEngine::check(e).
+   */
+  virtual void reset_round(Theory::Effort e) {}
+  /** Check.
+   *
+   *   Called during QuantifiersEngine::check(e) depending
+   *   if needsCheck(e) returns true.
+   */
+  virtual void check(Theory::Effort e, QEffort quant_e) = 0;
+  /** Check complete?
+   *
+   * Returns false if the module's reasoning was globally incomplete
+   * (e.g. "sat" must be replaced with "incomplete").
+   *
+   * This is called just before the quantifiers engine will return
+   * with no lemmas added during a LAST_CALL effort check.
+   */
+  virtual bool checkComplete() { return true; }
+  /** Check was complete for quantified formula q
+   *
+   * If for each quantified formula q, some module returns true for
+   * checkCompleteFor( q ),
+   * and no lemmas are added by the quantifiers theory, then we may answer
+   * "sat", unless
+   * we are incomplete for other reasons.
+   */
+  virtual bool checkCompleteFor(Node q) { return false; }
+  /** Check ownership
+   *
+   * Called once for new quantified formulas that are registered by the
+   * quantifiers theory. The primary purpose of this function is to establish
+   * if this module is the owner of quantified formula q.
+   */
+  virtual void checkOwnership(Node q) {}
+  /** Register quantifier
+   *
+   * Called once for new quantified formulas q that are pre-registered by the
+   * quantifiers theory, after internal ownership of quantified formulas is
+   * finalized. This does context-independent initialization of this module
+   * for quantified formula q.
+   */
+  virtual void registerQuantifier(Node q) {}
+  /** Pre-register quantifier
+   *
+   * Called once for new quantified formulas that are
+   * pre-registered by the quantifiers theory, after
+   * internal ownership of quantified formulas is finalized.
+   */
+  virtual void preRegisterQuantifier(Node q) {}
+  /** Assert node.
+   *
+   * Called when a quantified formula q is asserted to the quantifiers theory
+   */
+  virtual void assertNode(Node q) {}
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  virtual std::string identify() const = 0;
+  //----------------------------general queries
+  /** get currently used the equality engine */
+  eq::EqualityEngine* getEqualityEngine() const;
+  /** are n1 and n2 equal in the current used equality engine? */
+  bool areEqual(TNode n1, TNode n2) const;
+  /** are n1 and n2 disequal in the current used equality engine? */
+  bool areDisequal(TNode n1, TNode n2) const;
+  /** get the representative of n in the current used equality engine */
+  TNode getRepresentative(TNode n) const;
+  /** get quantifiers engine that owns this module */
+  QuantifiersEngine* getQuantifiersEngine() const;
+  /** get currently used term database */
+  quantifiers::TermDb* getTermDatabase() const;
+  /** get currently used term utility object */
+  quantifiers::TermUtil* getTermUtil() const;
+  /** get the quantifiers state */
+  quantifiers::QuantifiersState& getState();
+  /** get the quantifiers inference manager */
+  quantifiers::QuantifiersInferenceManager& getInferenceManager();
+  /** get the quantifiers registry */
+  quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
+  //----------------------------end general queries
+ protected:
+  /** pointer to the quantifiers engine that owns this module */
+  QuantifiersEngine* d_quantEngine;
+  /** The state of the quantifiers engine */
+  quantifiers::QuantifiersState& d_qstate;
+  /** The quantifiers inference manager */
+  quantifiers::QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  quantifiers::QuantifiersRegistry& d_qreg;
+}; /* class QuantifiersModule */
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANT_UTIL_H */
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 8fb9b4eb6..a51575f93 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -18,7 +18,7 @@
 #define CVC4__THEORY__QUANT_SPLIT_H
 
 #include "context/cdo.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index db643d96b..7516ea529 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -13,76 +13,14 @@
  **/
 
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/term_database.h"
+
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
 
-QuantifiersModule::QuantifiersModule(
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim,
-    quantifiers::QuantifiersRegistry& qr,
-    QuantifiersEngine* qe)
-    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
-{
-}
-
-QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
-{
-  return QEFFORT_NONE;
-}
-
-eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
-{
-  return d_qstate.getEqualityEngine();
-}
-
-bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
-{
-  return d_qstate.areEqual(n1, n2);
-}
-
-bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const
-{
-  return d_qstate.areDisequal(n1, n2);
-}
-
-TNode QuantifiersModule::getRepresentative(TNode n) const
-{
-  return d_qstate.getRepresentative(n);
-}
-
-QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const
-{
-  return d_quantEngine;
-}
-
-quantifiers::TermDb* QuantifiersModule::getTermDatabase() const
-{
-  return d_quantEngine->getTermDatabase();
-}
-
-quantifiers::TermUtil* QuantifiersModule::getTermUtil() const
-{
-  return d_quantEngine->getTermUtil();
-}
-
-quantifiers::QuantifiersState& QuantifiersModule::getState()
-{
-  return d_qstate;
-}
-
-quantifiers::QuantifiersInferenceManager&
-QuantifiersModule::getInferenceManager()
-{
-  return d_qim;
-}
-
 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
   initialize( n, computeEq );
 }
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 551143e40..e0cb11712 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -21,165 +21,17 @@
 #include <map>
 #include <vector>
 
-#include "theory/quantifiers/quantifiers_inference_manager.h"
-#include "theory/quantifiers/quantifiers_registry.h"
-#include "theory/quantifiers/quantifiers_state.h"
+#include "expr/node.h"
 #include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
 
-class QuantifiersEngine;
-
-namespace quantifiers {
-  class TermDb;
-  class TermUtil;
-}
-
-/** QuantifiersModule class
-*
-* This is the virtual class for defining subsolvers of the quantifiers theory.
-* It has a similar interface to a Theory object.
-*/
-class QuantifiersModule {
- public:
-  /** effort levels for quantifiers modules check */
-  enum QEffort
-  {
-    // conflict effort, for conflict-based instantiation
-    QEFFORT_CONFLICT,
-    // standard effort, for heuristic instantiation
-    QEFFORT_STANDARD,
-    // model effort, for model-based instantiation
-    QEFFORT_MODEL,
-    // last call effort, for last resort techniques
-    QEFFORT_LAST_CALL,
-    // none
-    QEFFORT_NONE,
-  };
-
- public:
-  QuantifiersModule(quantifiers::QuantifiersState& qs,
-                    quantifiers::QuantifiersInferenceManager& qim,
-                    quantifiers::QuantifiersRegistry& qr,
-                    QuantifiersEngine* qe);
-  virtual ~QuantifiersModule(){}
-  /** Presolve.
-   *
-   * Called at the beginning of check-sat call.
-   */
-  virtual void presolve() {}
-  /** Needs check.
-   *
-   * Returns true if this module wishes a call to be made
-   * to check(e) during QuantifiersEngine::check(e).
-   */
-  virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
-  /** Needs model.
-   *
-   * Whether this module needs a model built during a
-   * call to QuantifiersEngine::check(e)
-   * It returns one of QEFFORT_* from quantifiers_engine.h,
-   * which specifies the quantifiers effort in which it requires the model to
-   * be built.
-   */
-  virtual QEffort needsModel(Theory::Effort e);
-  /** Reset.
-   *
-   * Called at the beginning of QuantifiersEngine::check(e).
-   */
-  virtual void reset_round( Theory::Effort e ){}
-  /** Check.
-   *
-   *   Called during QuantifiersEngine::check(e) depending
-   *   if needsCheck(e) returns true.
-   */
-  virtual void check(Theory::Effort e, QEffort quant_e) = 0;
-  /** Check complete?
-   *
-   * Returns false if the module's reasoning was globally incomplete
-   * (e.g. "sat" must be replaced with "incomplete").
-   *
-   * This is called just before the quantifiers engine will return
-   * with no lemmas added during a LAST_CALL effort check.
-   */
-  virtual bool checkComplete() { return true; }
-  /** Check was complete for quantified formula q
-   *
-   * If for each quantified formula q, some module returns true for
-   * checkCompleteFor( q ),
-   * and no lemmas are added by the quantifiers theory, then we may answer
-   * "sat", unless
-   * we are incomplete for other reasons.
-   */
-  virtual bool checkCompleteFor( Node q ) { return false; }
-  /** Check ownership
-   *
-   * Called once for new quantified formulas that are registered by the
-   * quantifiers theory. The primary purpose of this function is to establish
-   * if this module is the owner of quantified formula q.
-   */
-  virtual void checkOwnership(Node q) {}
-  /** Register quantifier
-   *
-   * Called once for new quantified formulas q that are pre-registered by the
-   * quantifiers theory, after internal ownership of quantified formulas is
-   * finalized. This does context-independent initialization of this module
-   * for quantified formula q.
-   */
-  virtual void registerQuantifier(Node q) {}
-  /** Pre-register quantifier
-   *
-   * Called once for new quantified formulas that are
-   * pre-registered by the quantifiers theory, after
-   * internal ownership of quantified formulas is finalized.
-   */
-  virtual void preRegisterQuantifier(Node q) {}
-  /** Assert node.
-   *
-   * Called when a quantified formula q is asserted to the quantifiers theory
-   */
-  virtual void assertNode(Node q) {}
-  /** Identify this module (for debugging, dynamic configuration, etc..) */
-  virtual std::string identify() const = 0;
-  //----------------------------general queries
-  /** get currently used the equality engine */
-  eq::EqualityEngine* getEqualityEngine() const;
-  /** are n1 and n2 equal in the current used equality engine? */
-  bool areEqual(TNode n1, TNode n2) const;
-  /** are n1 and n2 disequal in the current used equality engine? */
-  bool areDisequal(TNode n1, TNode n2) const;
-  /** get the representative of n in the current used equality engine */
-  TNode getRepresentative(TNode n) const;
-  /** get quantifiers engine that owns this module */
-  QuantifiersEngine* getQuantifiersEngine() const;
-  /** get currently used term database */
-  quantifiers::TermDb* getTermDatabase() const;
-  /** get currently used term utility object */
-  quantifiers::TermUtil* getTermUtil() const;
-  /** get the quantifiers state */
-  quantifiers::QuantifiersState& getState();
-  /** get the quantifiers inference manager */
-  quantifiers::QuantifiersInferenceManager& getInferenceManager();
-  //----------------------------end general queries
- protected:
-  /** pointer to the quantifiers engine that owns this module */
-  QuantifiersEngine* d_quantEngine;
-  /** The state of the quantifiers engine */
-  quantifiers::QuantifiersState& d_qstate;
-  /** The quantifiers inference manager */
-  quantifiers::QuantifiersInferenceManager& d_qim;
-  /** The quantifiers registry */
-  quantifiers::QuantifiersRegistry& d_qreg;
-};/* class QuantifiersModule */
-
 /** Quantifiers utility
-*
-* This is a lightweight version of a quantifiers module that does not implement
-* methods
-* for checking satisfiability.
-*/
+ *
+ * This is a lightweight version of a quantifiers module that does not implement
+ * methods for checking satisfiability.
+ */
 class QuantifiersUtil {
 public:
   QuantifiersUtil(){}
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index f1a05f401..74f553800 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -93,7 +93,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   // full saturation : instantiate from relevant domain, then arbitrary terms
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
-    d_rel_dom.reset(new RelevantDomain(qe));
+    d_rel_dom.reset(new RelevantDomain(qe, qr));
     d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp
index 1633382c8..e6d4c75fe 100644
--- a/src/theory/quantifiers/quantifiers_registry.cpp
+++ b/src/theory/quantifiers/quantifiers_registry.cpp
@@ -14,12 +14,45 @@
 
 #include "theory/quantifiers/quantifiers_registry.h"
 
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
+#include "theory/quantifiers/term_util.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+void QuantifiersRegistry::registerQuantifier(Node q)
+{
+  if (d_inst_constants.find(q) != d_inst_constants.end())
+  {
+    return;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Debug("quantifiers-engine")
+      << "Instantiation constants for " << q << " : " << std::endl;
+  for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+  {
+    d_vars[q].push_back(q[0][i]);
+    // make instantiation constants
+    Node ic = nm->mkInstConstant(q[0][i].getType());
+    d_inst_constants_map[ic] = q;
+    d_inst_constants[q].push_back(ic);
+    Debug("quantifiers-engine") << "  " << ic << std::endl;
+    // set the var number attribute
+    InstVarNumAttribute ivna;
+    ic.setAttribute(ivna, i);
+    InstConstantAttribute ica;
+    ic.setAttribute(ica, q);
+  }
+}
+
+bool QuantifiersRegistry::reset(Theory::Effort e) { return true; }
+
+std::string QuantifiersRegistry::identify() const
+{
+  return "QuantifiersRegistry";
+}
+
 QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
 {
   std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
@@ -60,6 +93,82 @@ bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
   return mo == m || mo == nullptr;
 }
 
+Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator it =
+      d_inst_constants.find(q);
+  if (it != d_inst_constants.end())
+  {
+    return it->second[i];
+  }
+  return Node::null();
+}
+
+size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator it =
+      d_inst_constants.find(q);
+  if (it != d_inst_constants.end())
+  {
+    return it->second.size();
+  }
+  return 0;
+}
+
+Node QuantifiersRegistry::getInstConstantBody(Node q)
+{
+  std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q);
+  if (it == d_inst_const_body.end())
+  {
+    Node n = substituteBoundVariablesToInstConstants(q[1], q);
+    d_inst_const_body[q] = n;
+    return n;
+  }
+  return it->second;
+}
+
+Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
+                                                                  Node q)
+{
+  registerQuantifier(q);
+  return n.substitute(d_vars[q].begin(),
+                      d_vars[q].end(),
+                      d_inst_constants[q].begin(),
+                      d_inst_constants[q].end());
+}
+
+Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
+                                                                  Node q)
+{
+  registerQuantifier(q);
+  return n.substitute(d_inst_constants[q].begin(),
+                      d_inst_constants[q].end(),
+                      d_vars[q].begin(),
+                      d_vars[q].end());
+}
+
+Node QuantifiersRegistry::substituteBoundVariables(Node n,
+                                                   Node q,
+                                                   std::vector<Node>& terms)
+{
+  registerQuantifier(q);
+  Assert(d_vars[q].size() == terms.size());
+  return n.substitute(
+      d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end());
+}
+
+Node QuantifiersRegistry::substituteInstConstants(Node n,
+                                                  Node q,
+                                                  std::vector<Node>& terms)
+{
+  registerQuantifier(q);
+  Assert(d_inst_constants[q].size() == terms.size());
+  return n.substitute(d_inst_constants[q].begin(),
+                      d_inst_constants[q].end(),
+                      terms.begin(),
+                      terms.end());
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h
index 59db1dfe2..b89a2c01b 100644
--- a/src/theory/quantifiers/quantifiers_registry.h
+++ b/src/theory/quantifiers/quantifiers_registry.h
@@ -18,6 +18,7 @@
 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
 
 #include "expr/node.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {
@@ -26,15 +27,29 @@ class QuantifiersModule;
 
 namespace quantifiers {
 
+class Instantiate;
+
 /**
  * The quantifiers registry, which manages basic information about which
- * quantifiers modules have ownership of quantified formulas.
+ * quantifiers modules have ownership of quantified formulas, and manages
+ * the allocation of instantiation constants per quantified formula.
  */
-class QuantifiersRegistry
+class QuantifiersRegistry : public QuantifiersUtil
 {
+  friend class Instantiate;
+
  public:
   QuantifiersRegistry() {}
   ~QuantifiersRegistry() {}
+  /**
+   * Register quantifier, which allocates the instantiation constants for q.
+   */
+  void registerQuantifier(Node q) override;
+  /** reset */
+  bool reset(Theory::Effort e) override;
+  /** identify */
+  std::string identify() const override;
+  //----------------------------- ownership
   /** get the owner of quantified formula q */
   QuantifiersModule* getOwner(Node q) const;
   /**
@@ -47,7 +62,28 @@ class QuantifiersRegistry
    * Return true if module q has no owner registered or if its registered owner is m.
    */
   bool hasOwnership(Node q, QuantifiersModule* m) const;
-
+  //----------------------------- end ownership
+  //----------------------------- instantiation constants
+  /** get the i^th instantiation constant of q */
+  Node getInstantiationConstant(Node q, size_t i) const;
+  /** get number of instantiation constants for q */
+  size_t getNumInstantiationConstants(Node q) const;
+  /** get the ce body q[e/x] */
+  Node getInstConstantBody(Node q);
+  /** returns node n with bound vars of q replaced by instantiation constants of
+     q node n : is the future pattern node q : is the quantifier containing
+     which bind the variable return a pattern where the variable are replaced by
+     variable for instantiation.
+   */
+  Node substituteBoundVariablesToInstConstants(Node n, Node q);
+  /** substitute { instantiation constants of q -> bound variables of q } in n
+   */
+  Node substituteInstConstantsToBoundVariables(Node n, Node q);
+  /** substitute { variables of q -> terms } in n */
+  Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms);
+  /** substitute { instantiation constants of q -> terms } in n */
+  Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms);
+  //----------------------------- end instantiation constants
  private:
   /**
    * Maps quantified formulas to the module that owns them, if any module has
@@ -60,6 +96,14 @@ class QuantifiersRegistry
    * precendence.
    */
   std::map<Node, int32_t> d_owner_priority;
+  /** map from universal quantifiers to the list of variables */
+  std::map<Node, std::vector<Node> > d_vars;
+  /** map from universal quantifiers to their inst constant body */
+  std::map<Node, Node> d_inst_const_body;
+  /** instantiation constants to universal quantifiers */
+  std::map<Node, Node> d_inst_constants_map;
+  /** map from universal quantifiers to the list of instantiation constants */
+  std::map<Node, std::vector<Node> > d_inst_constants;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 1743cafe5..3cef2884f 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -69,10 +69,10 @@ void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
   }
 }
 
-
-
-RelevantDomain::RelevantDomain( QuantifiersEngine* qe ) : d_qe( qe ){
-   d_is_computed = false;
+RelevantDomain::RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr)
+    : d_qe(qe), d_qreg(qr)
+{
+  d_is_computed = false;
 }
 
 RelevantDomain::~RelevantDomain() {
@@ -111,7 +111,7 @@ void RelevantDomain::compute(){
     FirstOrderModel* fm = d_qe->getModel();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node q = fm->getAssertedQuantifier( i );
-      Node icf = d_qe->getTermUtil()->getInstConstantBody( q );
+      Node icf = d_qreg.getInstConstantBody(q);
       Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
       computeRelevantDomain( q, icf, true, true );
     }
@@ -204,12 +204,13 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po
 
 void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
   if( n.getKind()==INST_CONSTANT ){
-    Node q = d_qe->getTermUtil()->getInstConstAttr( n );
+    Node q = TermUtil::getInstConstAttr(n);
     //merge the RDomains
     unsigned id = n.getAttribute(InstVarNumAttribute());
     Assert(q[0][id].getType() == n.getType());
     Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
-    Trace("rel-dom-debug") << " with body : " << d_qe->getTermUtil()->getInstConstantBody( q ) << std::endl;
+    Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q)
+                           << std::endl;
     RDomain * rq = getRDomain( q, id );
     if( rf!=rq ){
       rq->merge( rf );
@@ -226,12 +227,11 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No
     d_rel_dom_lit[hasPol][pol][n].d_merge = false;
     int varCount = 0;
     int varCh = -1;
-    TermUtil* tu = d_qe->getTermUtil();
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( n[i].getKind()==INST_CONSTANT ){
         // must get the quantified formula this belongs to, which may be
         // different from q
-        Node qi = tu->getInstConstAttr(n[i]);
+        Node qi = TermUtil::getInstConstAttr(n[i]);
         unsigned id = n[i].getAttribute(InstVarNumAttribute());
         d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false);
         varCount++;
@@ -262,7 +262,7 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No
             bool hasNonVar = false;
             for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
               if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
-                  && tu->getInstConstAttr(it->first) == q)
+                  && TermUtil::getInstConstAttr(it->first) == q)
               {
                 if( var.isNull() ){
                   var = it->first;
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 36364191c..68ffbefe5 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -24,6 +24,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class QuantifiersRegistry;
+
 /** Relevant Domain
  *
  * This class computes the relevant domain of
@@ -40,7 +42,7 @@ namespace quantifiers {
 class RelevantDomain : public QuantifiersUtil
 {
  public:
-  RelevantDomain(QuantifiersEngine* qe);
+  RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr);
   virtual ~RelevantDomain();
   /** Reset. */
   bool reset(Theory::Effort e) override;
@@ -117,6 +119,8 @@ class RelevantDomain : public QuantifiersUtil
   std::map< RDomain *, int > d_ri_map;
   /** Quantifiers engine associated with this utility. */
   QuantifiersEngine* d_qe;
+  /** The quantifiers registry */
+  QuantifiersRegistry& d_qreg;
   /** have we computed the relevant domain on this full effort check? */
   bool d_is_computed;
   /** relevant domain literal
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index c329d924b..f1307f142 100644
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index b28854baf..c959758a0 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -23,7 +23,7 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
@@ -31,8 +31,13 @@ namespace CVC4 {
 class DTypeConstructor;
 
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
+class QuantifiersState;
+
 /** Skolemization utility
  *
  * This class constructs Skolemization lemmas.
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 4cb73d450..0e0068c7b 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -19,7 +19,7 @@
 #define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
 
 #include "context/cdhashmap.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/sygus/sygus_qe_preproc.h"
 #include "theory/quantifiers/sygus/sygus_stats.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 123ec1f5e..3116f35e6 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -21,7 +21,7 @@
 #include <unordered_set>
 
 #include "context/cdhashset.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 61a62a820..28eb715a3 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -36,10 +36,12 @@ namespace quantifiers {
 
 TermDb::TermDb(QuantifiersState& qs,
                QuantifiersInferenceManager& qim,
+               QuantifiersRegistry& qr,
                QuantifiersEngine* qe)
     : d_quantEngine(qe),
       d_qstate(qs),
       d_qim(qim),
+      d_qreg(qr),
       d_termsContext(),
       d_termsContextUse(options::termDbCd() ? qs.getSatContext()
                                             : &d_termsContext),
@@ -65,10 +67,10 @@ TermDb::~TermDb(){
 }
 
 void TermDb::registerQuantifier( Node q ) {
-  Assert(q[0].getNumChildren()
-         == d_quantEngine->getTermUtil()->getNumInstantiationConstants(q));
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
+  Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q));
+  for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+  {
+    Node ic = d_qreg.getInstantiationConstant(q, i);
     setTermInactive( ic );
   }
 }
@@ -688,10 +690,10 @@ Node TermDb::evaluateTerm2(TNode n,
         {
           if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
           {
-            TheoryEngine* te = d_quantEngine->getTheoryEngine();
+            Valuation& val = d_qstate.getValuation();
             for (unsigned j = 0; j < 2; j++)
             {
-              std::pair<bool, Node> et = te->entailmentCheck(
+              std::pair<bool, Node> et = val.entailmentCheck(
                   options::TheoryOfMode::THEORY_OF_TYPE_BASED,
                   j == 0 ? ret : ret.negate());
               if (et.first)
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index b2f964a3a..89d77e169 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -33,8 +33,9 @@ class QuantifiersEngine;
 
 namespace quantifiers {
 
-class ConjectureGenerator;
-class TermGenEnv;
+class QuantifiersState;
+class QuantifiersInferenceManager;
+class QuantifiersRegistry;
 
 /** Context-dependent list of nodes */
 class DbList
@@ -76,6 +77,7 @@ class TermDb : public QuantifiersUtil {
  public:
   TermDb(QuantifiersState& qs,
          QuantifiersInferenceManager& qim,
+         QuantifiersRegistry& qr,
          QuantifiersEngine* qe);
   ~TermDb();
   /** presolve (called once per user check-sat) */
@@ -295,6 +297,8 @@ class TermDb : public QuantifiersUtil {
   QuantifiersState& d_qstate;
   /** The quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  QuantifiersRegistry& d_qreg;
   /** A context for the data structures below, when not context-dependent */
   context::Context d_termsContext;
   /** The context we are using for the data structures below */
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index b0a067630..97a731fb9 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -47,24 +47,11 @@ TermUtil::~TermUtil(){
 
 }
 
-void TermUtil::registerQuantifier( Node q ){
-  if( d_inst_constants.find( q )==d_inst_constants.end() ){
-    Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      d_vars[q].push_back( q[0][i] );
-      d_var_num[q][q[0][i]] = i;
-      //make instantiation constants
-      Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() );
-      d_inst_constants_map[ic] = q;
-      d_inst_constants[ q ].push_back( ic );
-      Debug("quantifiers-engine") << "  " << ic << std::endl;
-      //set the var number attribute
-      InstVarNumAttribute ivna;
-      ic.setAttribute( ivna, i );
-      InstConstantAttribute ica;
-      ic.setAttribute( ica, q );
-    }
-  }
+size_t TermUtil::getVariableNum(Node q, Node v)
+{
+  Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
+  Assert(it != q[0].end());
+  return it - q[0].begin();
 }
 
 Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
@@ -168,68 +155,6 @@ Node TermUtil::getQuantSimplify( Node n ) {
   return getRemoveQuantifiers(q);
 }
 
-/** get the i^th instantiation constant of q */
-Node TermUtil::getInstantiationConstant( Node q, int i ) const {
-  std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
-  if( it!=d_inst_constants.end() ){
-    return it->second[i];
-  }else{
-    return Node::null();
-  }
-}
-
-/** get number of instantiation constants for q */
-unsigned TermUtil::getNumInstantiationConstants( Node q ) const {
-  std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
-  if( it!=d_inst_constants.end() ){
-    return it->second.size();
-  }else{
-    return 0;
-  }
-}
-
-Node TermUtil::getInstConstantBody( Node q ){
-  std::map< Node, Node >::iterator it = d_inst_const_body.find( q );
-  if( it==d_inst_const_body.end() ){
-    Node n = substituteBoundVariablesToInstConstants(q[1], q);
-    d_inst_const_body[ q ] = n;
-    return n;
-  }else{
-    return it->second;
-  }
-}
-
-Node TermUtil::substituteBoundVariablesToInstConstants(Node n, Node q)
-{
-  registerQuantifier( q );
-  return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() );
-}
-
-Node TermUtil::substituteInstConstantsToBoundVariables(Node n, Node q)
-{
-  registerQuantifier( q );
-  return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() );
-}
-
-Node TermUtil::substituteBoundVariables(Node n,
-                                        Node q,
-                                        std::vector<Node>& terms)
-{
-  registerQuantifier(q);
-  Assert(d_vars[q].size() == terms.size());
-  return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() );
-}
-
-Node TermUtil::substituteInstConstants(Node n, Node q, std::vector<Node>& terms)
-{
-  registerQuantifier(q);
-  Assert(d_inst_constants[q].size() == terms.size());
-  return n.substitute(d_inst_constants[q].begin(),
-                      d_inst_constants[q].end(),
-                      terms.begin(),
-                      terms.end());
-}
-
 void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
 {
   computeVarContainsInternal(n, INST_CONSTANT, ics);
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 4033c888f..e9e3c7e98 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -21,7 +21,6 @@
 #include <unordered_set>
 
 #include "expr/attribute.h"
-#include "theory/quantifiers/quant_util.h"
 #include "theory/type_enumerator.h"
 
 namespace CVC4 {
@@ -61,15 +60,10 @@ namespace inst{
 namespace quantifiers {
 
 class TermDatabase;
-class Instantiate;
 
 // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
-class TermUtil : public QuantifiersUtil
+class TermUtil
 {
-  // TODO : remove these
-  friend class ::CVC4::theory::QuantifiersEngine;
-  friend class Instantiate;
-
  public:
   TermUtil();
   ~TermUtil();
@@ -80,46 +74,10 @@ class TermUtil : public QuantifiersUtil
   Node d_zero;
   Node d_one;
 
-  /** reset */
-  bool reset(Theory::Effort e) override { return true; }
-  /** register quantifier */
-  void registerQuantifier(Node q) override;
-  /** identify */
-  std::string identify() const override { return "TermUtil"; }
   // for inst constant
- private:
-  /** map from universal quantifiers to the list of variables */
-  std::map< Node, std::vector< Node > > d_vars;
-  std::map< Node, std::map< Node, unsigned > > d_var_num;
-  /** map from universal quantifiers to their inst constant body */
-  std::map< Node, Node > d_inst_const_body;
-  /** instantiation constants to universal quantifiers */
-  std::map< Node, Node > d_inst_constants_map;
-public:
-  /** map from universal quantifiers to the list of instantiation constants */
-  std::map< Node, std::vector< Node > > d_inst_constants;
-  /** get variable number */
-  unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; }
-  /** get the i^th instantiation constant of q */
-  Node getInstantiationConstant( Node q, int i ) const;
-  /** get number of instantiation constants for q */
-  unsigned getNumInstantiationConstants( Node q ) const;
-  /** get the ce body q[e/x] */
-  Node getInstConstantBody( Node q );
-  /** returns node n with bound vars of q replaced by instantiation constants of q
-      node n : is the future pattern
-      node q : is the quantifier containing which bind the variable
-      return a pattern where the variable are replaced by variable for
-      instantiation.
-   */
-  Node substituteBoundVariablesToInstConstants(Node n, Node q);
-  /** substitute { instantiation constants of q -> bound variables of q } in n
-   */
-  Node substituteInstConstantsToBoundVariables(Node n, Node q);
-  /** substitute { variables of q -> terms } in n */
-  Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms);
-  /** substitute { instantiation constants of q -> terms } in n */
-  Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms);
+ public:
+  /** Get the index of BOUND_VARIABLE v in quantifier q */
+  static size_t getVariableNum(Node q, Node v);
 
   static Node getInstConstAttr( Node n );
   static bool hasInstConstAttr( Node n );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e85d6f2ff..9c56c1ba5 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -45,11 +45,12 @@ QuantifiersEngine::QuantifiersEngine(
       d_model(nullptr),
       d_builder(nullptr),
       d_term_util(new quantifiers::TermUtil),
-      d_term_db(new quantifiers::TermDb(qstate, qim, this)),
+      d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)),
       d_eq_query(nullptr),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes),
-      d_instantiate(new quantifiers::Instantiate(this, qstate, qim, pnm)),
+      d_instantiate(
+          new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
       d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
       d_term_enum(new quantifiers::TermEnumeration),
       d_quants_prereg(qstate.getUserContext()),
@@ -59,8 +60,8 @@ QuantifiersEngine::QuantifiersEngine(
       d_presolve_cache(qstate.getUserContext())
 {
   //---- utilities
-  // term util must come before the other utilities
-  d_util.push_back(d_term_util.get());
+  // quantifiers registry must come before the other utilities
+  d_util.push_back(&d_qreg);
   d_util.push_back(d_term_db.get());
 
   if (options::sygus() || options::sygusInst())
@@ -88,17 +89,17 @@ QuantifiersEngine::QuantifiersEngine(
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-          this, qstate, "FirstOrderModelFmc"));
+          this, qstate, d_qreg, "FirstOrderModelFmc"));
       d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
-      d_model.reset(
-          new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
+      d_model.reset(new quantifiers::FirstOrderModel(
+          this, qstate, d_qreg, "FirstOrderModel"));
       d_builder.reset(new quantifiers::QModelBuilder(this, qstate));
     }
   }else{
-    d_model.reset(
-        new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
+    d_model.reset(new quantifiers::FirstOrderModel(
+        this, qstate, d_qreg, "FirstOrderModel"));
   }
   d_eq_query.reset(new quantifiers::EqualityQueryQuantifiersEngine(
       qstate, d_term_db.get(), d_model.get()));
@@ -142,6 +143,12 @@ QuantifiersEngine::getInferenceManager()
 {
   return d_qim;
 }
+
+quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
+{
+  return d_qreg;
+}
+
 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 {
   return d_builder.get();
@@ -737,7 +744,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   {
     mdl->assertNode(f);
   }
-  addTermToDatabase(d_term_util->getInstConstantBody(f), true);
+  addTermToDatabase(d_qreg.getInstConstantBody(f), true);
 }
 
 void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant)
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 99e4ad5cc..2fbf6b70f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -28,6 +28,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
@@ -77,6 +78,8 @@ class QuantifiersEngine {
   quantifiers::QuantifiersState& getState();
   /** The quantifiers inference manager */
   quantifiers::QuantifiersInferenceManager& getInferenceManager();
+  /** The quantifiers registry */
+  quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
   //---------------------- end external interface
   //---------------------- utilities
   /** get the model builder */