From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 17 Feb 2021 19:34:54 +0000 (-0600)
Subject: Move methods from term util to quantifiers registry (#5916)
X-Git-Tag: cvc5-1.0.0~2269
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f03dbb1378354adcfef635a93f8b13987c2d983;p=cvc5.git

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.
---

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 */