Passing term registry to ematching utilities (#6190)

Model is now nested into term registry.

This PR also resolves some complications due to namespaces within quantifiers.

53 files changed, 376 insertions, 297 deletions

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 4cc912e45..60350f882 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -19,30 +19,37 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
+CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr)
+    : d_qs(qs), d_treg(tr)
+{
+}
+
 bool CandidateGenerator::isLegalCandidate( Node n ){
-  return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
+  return d_treg.getTermDatabase()->isTermActive(n)
+         && (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n));
 }
 
-CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
-    : CandidateGenerator(qe),
+CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs,
+                                           TermRegistry& tr,
+                                           Node pat)
+    : CandidateGenerator(qs, tr),
       d_term_iter(-1),
       d_term_iter_limit(0),
       d_mode(cand_term_none)
 {
-  d_op = qe->getTermDatabase()->getMatchOperator( pat );
+  d_op = d_treg.getTermDatabase()->getMatchOperator(pat);
   Assert(!d_op.isNull());
 }
 
@@ -53,16 +60,16 @@ void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
   d_term_iter = 0;
   d_eqc = eqc;
   d_op = op;
-  d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms(d_op);
+  d_term_iter_limit = d_treg.getTermDatabase()->getNumGroundTerms(d_op);
   if( eqc.isNull() ){
     d_mode = cand_term_db;
   }else{
     if( isExcludedEqc( eqc ) ){
       d_mode = cand_term_none;
     }else{
-      eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+      eq::EqualityEngine* ee = d_qs.getEqualityEngine();
       if( ee->hasTerm( eqc ) ){
-        TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op);
+        TNodeTrie* tat = d_treg.getTermDatabase()->getTermArgTrie(eqc, op);
         if( tat ){
           //create an equivalence class iterator in eq class eqc
           Node rep = ee->getRepresentative( eqc );
@@ -81,7 +88,7 @@ void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
 bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
   if( n.hasOperator() ){
     if( isLegalCandidate( n ) ){
-      return d_qe->getTermDatabase()->getMatchOperator( n )==d_op;
+      return d_treg.getTermDatabase()->getMatchOperator(n) == d_op;
     }
   }
   return false;
@@ -94,18 +101,18 @@ Node CandidateGeneratorQE::getNextCandidate(){
 Node CandidateGeneratorQE::getNextCandidateInternal()
 {
   if( d_mode==cand_term_db ){
-    quantifiers::QuantifiersState& qs = d_qe->getState();
     Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
     //get next candidate term in the uf term database
     while( d_term_iter<d_term_iter_limit ){
-      Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter );
+      Node n = d_treg.getTermDatabase()->getGroundTerm(d_op, d_term_iter);
       d_term_iter++;
       if( isLegalCandidate( n ) ){
-        if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
+        if (d_treg.getTermDatabase()->hasTermCurrent(n))
+        {
           if( d_exclude_eqc.empty() ){
             return n;
           }else{
-            Node r = qs.getRepresentative(n);
+            Node r = d_qs.getRepresentative(n);
             if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
               Debug("cand-gen-qe") << "...returning " << n << std::endl;
               return n;
@@ -138,14 +145,17 @@ Node CandidateGeneratorQE::getNextCandidateInternal()
   return Node::null();
 }
 
-CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
-CandidateGenerator( qe ), d_match_pattern( mpat ){
+CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq(QuantifiersState& qs,
+                                                       TermRegistry& tr,
+                                                       Node mpat)
+    : CandidateGenerator(qs, tr), d_match_pattern(mpat)
+{
   Assert(d_match_pattern.getKind() == EQUAL);
   d_match_pattern_type = d_match_pattern[0].getType();
 }
 
 void CandidateGeneratorQELitDeq::reset( Node eqc ){
-  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+  eq::EqualityEngine* ee = d_qs.getEqualityEngine();
   Node falset = NodeManager::currentNM()->mkConst(false);
   d_eqc_false = eq::EqClassIterator(falset, ee);
 }
@@ -169,9 +179,11 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){
   return Node::null();
 }
 
-
-CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) :
-  CandidateGenerator( qe ), d_match_pattern( mpat ){
+CandidateGeneratorQEAll::CandidateGeneratorQEAll(QuantifiersState& qs,
+                                                 TermRegistry& tr,
+                                                 Node mpat)
+    : CandidateGenerator(qs, tr), d_match_pattern(mpat)
+{
   d_match_pattern_type = mpat.getType();
   Assert(mpat.getKind() == INST_CONSTANT);
   d_f = quantifiers::TermUtil::getInstConstAttr( mpat );
@@ -180,12 +192,12 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp
 }
 
 void CandidateGeneratorQEAll::reset( Node eqc ) {
-  d_eq = eq::EqClassesIterator(d_qe->getState().getEqualityEngine());
+  d_eq = eq::EqClassesIterator(d_qs.getEqualityEngine());
   d_firstTime = true;
 }
 
 Node CandidateGeneratorQEAll::getNextCandidate() {
-  quantifiers::TermDb* tdb = d_qe->getTermDatabase();
+  quantifiers::TermDb* tdb = d_treg.getTermDatabase();
   while( !d_eq.isFinished() ){
     TNode n = (*d_eq);
     ++d_eq;
@@ -194,7 +206,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
       if( !nh.isNull() ){
         if (options::instMaxLevel() != -1)
         {
-          nh = d_qe->getModel()->getInternalRepresentative(nh, d_f, d_index);
+          nh = d_treg.getModel()->getInternalRepresentative(nh, d_f, d_index);
           //don't consider this if already the instantiation is ineligible
           if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f))
           {
@@ -212,14 +224,15 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
   if( d_firstTime ){
     //must return something
     d_firstTime = false;
-    return d_qe->getInstantiate()->getTermForType(d_match_pattern_type);
+    return d_treg.getTermForType(d_match_pattern_type);
   }
   return Node::null();
 }
 
-CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(
-    QuantifiersEngine* qe, Node mpat)
-    : CandidateGeneratorQE(qe, mpat)
+CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(QuantifiersState& qs,
+                                                           TermRegistry& tr,
+                                                           Node mpat)
+    : CandidateGeneratorQE(qs, tr, mpat)
 {
   Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
   d_mpat_type = mpat.getType();
@@ -268,9 +281,10 @@ bool CandidateGeneratorConsExpand::isLegalOpCandidate(Node n)
   return isLegalCandidate(n);
 }
 
-CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersEngine* qe,
+CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
+                                                       TermRegistry& tr,
                                                        Node mpat)
-    : CandidateGeneratorQE(qe, mpat)
+    : CandidateGeneratorQE(qs, tr, mpat)
 {
   Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
   Assert(mpat.getKind() == APPLY_SELECTOR);
@@ -280,19 +294,19 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersEngine* qe,
   {
     Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
     Assert(mpatExp[2].getKind() == APPLY_UF);
-    d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp[1]);
-    d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp[2]);
+    d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]);
+    d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]);
   }
   else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL)
   {
     // corner case of datatype with one constructor
-    d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp);
+    d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
   }
   else
   {
     // corner case of a wrongly applied selector as a trigger
     Assert(mpatExp.getKind() == APPLY_UF);
-    d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp);
+    d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
   }
   Assert(d_selOp != d_ufOp);
 }
@@ -332,5 +346,6 @@ Node CandidateGeneratorSelector::getNextCandidate()
 }
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index e0d25eb64..45eec1d4c 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.h
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
@@ -22,8 +22,10 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 
-class QuantifiersEngine;
+class QuantifiersState;
+class TermRegistry;
 
 namespace inst {
 
@@ -51,10 +53,8 @@ namespace inst {
  *
  */
 class CandidateGenerator {
-protected:
-  QuantifiersEngine* d_qe;
-public:
-  CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){}
+ public:
+  CandidateGenerator(QuantifiersState& qs, TermRegistry& tr);
   virtual ~CandidateGenerator(){}
   /** reset instantiation round
    *
@@ -70,10 +70,15 @@ public:
   virtual void reset( Node eqc ) = 0;
   /** get the next candidate */
   virtual Node getNextCandidate() = 0;
-public:
- /** is n a legal candidate? */
- bool isLegalCandidate(Node n);
-};/* class CandidateGenerator */
+  /** is n a legal candidate? */
+  bool isLegalCandidate(Node n);
+
+ protected:
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qs;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
+};
 
 /* the default candidate generator class
  *
@@ -88,7 +93,7 @@ class CandidateGeneratorQE : public CandidateGenerator
   friend class CandidateGeneratorQEDisequal;
 
  public:
-  CandidateGeneratorQE(QuantifiersEngine* qe, Node pat);
+  CandidateGeneratorQE(QuantifiersState& qs, TermRegistry& tr, Node pat);
   /** reset */
   void reset(Node eqc) override;
   /** get next candidate */
@@ -142,7 +147,7 @@ class CandidateGeneratorQELitDeq : public CandidateGenerator
    * mpat is an equality that we are matching to equalities in the equivalence
    * class of false
    */
-  CandidateGeneratorQELitDeq(QuantifiersEngine* qe, Node mpat);
+  CandidateGeneratorQELitDeq(QuantifiersState& qs, TermRegistry& tr, Node mpat);
   /** reset */
   void reset(Node eqc) override;
   /** get next candidate */
@@ -178,7 +183,7 @@ class CandidateGeneratorQEAll : public CandidateGenerator
   bool d_firstTime;
 
  public:
-  CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
+  CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat);
   /** reset */
   void reset(Node eqc) override;
   /** get next candidate */
@@ -196,7 +201,9 @@ class CandidateGeneratorQEAll : public CandidateGenerator
 class CandidateGeneratorConsExpand : public CandidateGeneratorQE
 {
  public:
-  CandidateGeneratorConsExpand(QuantifiersEngine* qe, Node mpat);
+  CandidateGeneratorConsExpand(QuantifiersState& qs,
+                               TermRegistry& tr,
+                               Node mpat);
   /** reset */
   void reset(Node eqc) override;
   /** get next candidate */
@@ -216,7 +223,7 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE
 class CandidateGeneratorSelector : public CandidateGeneratorQE
 {
  public:
-  CandidateGeneratorSelector(QuantifiersEngine* qe, Node mpat);
+  CandidateGeneratorSelector(QuantifiersState& qs, TermRegistry& tr, Node mpat);
   /** reset */
   void reset(Node eqc) override;
   /**
@@ -234,6 +241,7 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE
 };
 
 }/* CVC4::theory::inst namespace */
+}  // namespace quantifiers
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 17cbba7ea..6206b24a7 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -29,17 +29,19 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 HigherOrderTrigger::HigherOrderTrigger(
     QuantifiersEngine* qe,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim,
-    quantifiers::QuantifiersRegistry& qr,
+    QuantifiersState& qs,
+    QuantifiersInferenceManager& qim,
+    QuantifiersRegistry& qr,
+    TermRegistry& tr,
     Node q,
     std::vector<Node>& nodes,
     std::map<Node, std::vector<Node> >& ho_apps)
-    : Trigger(qe, qs, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
+    : Trigger(qe, qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps)
 {
   NodeManager* nm = NodeManager::currentNM();
   // process the higher-order variable applications
@@ -166,7 +168,7 @@ void HigherOrderTrigger::collectHoVarApplyTerms(
           {
             if (op.getKind() == kind::INST_CONSTANT)
             {
-              Assert(quantifiers::TermUtil::getInstConstAttr(ret) == q);
+              Assert(TermUtil::getInstConstAttr(ret) == q);
               Trace("ho-quant-trigger-debug")
                   << "Ho variable apply term : " << ret << " with head " << op
                   << std::endl;
@@ -234,7 +236,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
     d_lchildren.clear();
     d_arg_to_arg_rep.clear();
     d_arg_vector.clear();
-    quantifiers::QuantifiersState& qs = d_quantEngine->getState();
+    QuantifiersState& qs = d_quantEngine->getState();
     for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
     {
       TNode var = ha.first;
@@ -474,7 +476,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
   Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
   uint64_t numLemmas = 0;
   // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
-  quantifiers::TermDb* tdb = d_quantEngine->getTermDatabase();
+  TermDb* tdb = d_quantEngine->getTermDatabase();
   unsigned size = tdb->getNumOperators();
   NodeManager* nm = NodeManager::currentNM();
   for (unsigned j = 0; j < size; j++)
@@ -522,6 +524,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
   return numLemmas;
 }
 
-} /* CVC4::theory::inst namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index fcb3cbfee..87c7adeec 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -27,6 +27,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 class Trigger;
@@ -93,9 +94,10 @@ class HigherOrderTrigger : public Trigger
 
  private:
   HigherOrderTrigger(QuantifiersEngine* qe,
-                     quantifiers::QuantifiersState& qs,
-                     quantifiers::QuantifiersInferenceManager& qim,
-                     quantifiers::QuantifiersRegistry& qr,
+                     QuantifiersState& qs,
+                     QuantifiersInferenceManager& qim,
+                     QuantifiersRegistry& qr,
+                     TermRegistry& tr,
                      Node q,
                      std::vector<Node>& nodes,
                      std::map<Node, std::vector<Node> >& ho_apps);
@@ -274,8 +276,9 @@ class HigherOrderTrigger : public Trigger
                             bool arg_changed);
 };
 
-} /* CVC4::theory::inst namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp
index 829ccc8b1..48c07ba4d 100644
--- a/src/theory/quantifiers/ematching/im_generator.cpp
+++ b/src/theory/quantifiers/ematching/im_generator.cpp
@@ -20,10 +20,11 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 IMGenerator::IMGenerator(Trigger* tparent)
-    : d_tparent(tparent), d_qstate(tparent->d_qstate)
+    : d_tparent(tparent), d_qstate(tparent->d_qstate), d_treg(tparent->d_treg)
 {
 }
 
@@ -37,7 +38,7 @@ QuantifiersEngine* IMGenerator::getQuantifiersEngine()
   return d_tparent->d_quantEngine;
 }
 
-
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h
index 6bf472cb5..0d0f9498d 100644
--- a/src/theory/quantifiers/ematching/im_generator.h
+++ b/src/theory/quantifiers/ematching/im_generator.h
@@ -29,7 +29,7 @@ class QuantifiersEngine;
 
 namespace quantifiers {
 class QuantifiersState;
-}  // namespace quantifiers
+class TermRegistry;
 
 namespace inst {
 
@@ -110,12 +110,15 @@ protected:
  bool sendInstantiation(InstMatch& m, InferenceId id);
  /** The parent trigger that owns this */
  Trigger* d_tparent;
- /** The state of the quantifiers engine */
- quantifiers::QuantifiersState& d_qstate;
+ /** Reference to the state of the quantifiers engine */
+ QuantifiersState& d_qstate;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
  // !!!!!!!!! temporarily available (project #15)
  QuantifiersEngine* getQuantifiersEngine();
 };/* class IMGenerator */
 
+}  // namespace inst
 }
 }
 }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 5f47f70c3..ac3e1b9be 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -33,6 +33,7 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat)
@@ -200,13 +201,13 @@ void InstMatchGenerator::initialize(Node q,
     }
   }
 
-  QuantifiersEngine* qe = getQuantifiersEngine();
   // create candidate generator
   if (mpk == APPLY_SELECTOR)
   {
     // candidates for apply selector are a union of correctly and incorrectly
     // applied selectors
-    d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern);
+    d_cg =
+        new inst::CandidateGeneratorSelector(d_qstate, d_treg, d_match_pattern);
   }
   else if (TriggerTermInfo::isAtomicTriggerKind(mpk))
   {
@@ -217,12 +218,14 @@ void InstMatchGenerator::initialize(Node q,
       const DType& dt = d_match_pattern.getType().getDType();
       if (dt.getNumConstructors() == 1)
       {
-        d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
+        d_cg = new inst::CandidateGeneratorConsExpand(
+            d_qstate, d_treg, d_match_pattern);
       }
     }
     if (d_cg == nullptr)
     {
-      CandidateGeneratorQE* cg = new CandidateGeneratorQE(qe, d_match_pattern);
+      CandidateGeneratorQE* cg =
+          new CandidateGeneratorQE(d_qstate, d_treg, d_match_pattern);
       // we will be scanning lists trying to find ground terms whose operator
       // is the same as d_match_operator's.
       d_cg = cg;
@@ -247,9 +250,9 @@ void InstMatchGenerator::initialize(Node q,
       Trace("inst-match-gen")
           << "Purify dt trigger " << d_pattern << ", will match terms of op "
           << cOp << std::endl;
-      d_cg = new inst::CandidateGeneratorQE(qe, cOp);
+      d_cg = new inst::CandidateGeneratorQE(d_qstate, d_treg, cOp);
     }else{
-      d_cg = new CandidateGeneratorQEAll(qe, d_match_pattern);
+      d_cg = new CandidateGeneratorQEAll(d_qstate, d_treg, d_match_pattern);
     }
   }
   else if (mpk == EQUAL)
@@ -258,7 +261,8 @@ void InstMatchGenerator::initialize(Node q,
     if (d_pattern.getKind() == NOT)
     {
       // candidates will be all disequalities
-      d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
+      d_cg = new inst::CandidateGeneratorQELitDeq(
+          d_qstate, d_treg, d_match_pattern);
     }
   }
   else
@@ -666,6 +670,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
   return new InstMatchGenerator(tparent, n);
 }
 
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 3f6976ca7..375fe73e1 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -24,6 +24,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 class CandidateGenerator;
@@ -321,6 +322,7 @@ class InstMatchGenerator : public IMGenerator {
                                                    Node n);
 };/* class InstMatchGenerator */
 
+}  // namespace inst
 }
 }
 }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index 2920be1a2..c4d5272a4 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -23,6 +23,7 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent,
@@ -35,8 +36,7 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent,
   std::map<Node, std::vector<Node> > var_contains;
   for (const Node& pat : pats)
   {
-    quantifiers::TermUtil::computeInstConstContainsForQuant(
-        q, pat, var_contains[pat]);
+    TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]);
   }
   // convert to indicies
   for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
@@ -269,7 +269,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
     {
       return;
     }
-    quantifiers::QuantifiersState& qs = d_qstate;
+    QuantifiersState& qs = d_qstate;
     // check modulo equality for other possible instantiations
     if (!qs.hasTerm(n))
     {
@@ -314,5 +314,6 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
 }
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
index 85cbff7f0..1e25baea4 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
@@ -25,6 +25,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 /** InstMatchGeneratorMulti
@@ -100,6 +101,7 @@ class InstMatchGeneratorMulti : public IMGenerator
 };
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
 
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
index ac7bb5f3c..e8c08ef1e 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -22,6 +22,7 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
@@ -32,8 +33,7 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
   std::map<Node, std::vector<Node> > var_contains;
   for (const Node& pat : pats)
   {
-    quantifiers::TermUtil::computeInstConstContainsForQuant(
-        q, pat, var_contains[pat]);
+    TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]);
   }
   std::map<Node, std::vector<Node> > var_to_node;
   for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
@@ -174,5 +174,6 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
 }
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
index ce1e79229..b46960400 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
@@ -24,6 +24,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 /** InstMatchGeneratorMultiLinear class
@@ -82,6 +83,7 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator
 };
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
 
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index eaf917545..c7360d02f 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -26,6 +26,7 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
@@ -46,7 +47,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
   {
     d_eqc = d_match_pattern[1];
     d_match_pattern = d_match_pattern[0];
-    Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc));
+    Assert(!TermUtil::hasInstConstAttr(d_eqc));
   }
   Assert(TriggerTermInfo::isSimpleTrigger(d_match_pattern));
   for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
@@ -54,7 +55,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
     if (d_match_pattern[i].getKind() == INST_CONSTANT)
     {
       if (!options::cegqi()
-          || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]) == q)
+          || TermUtil::getInstConstAttr(d_match_pattern[i]) == q)
       {
         d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
       }
@@ -65,7 +66,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
     }
     d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
   }
-  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
   d_op = tdb->getMatchOperator(d_match_pattern);
 }
 
@@ -74,7 +75,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
 {
   uint64_t addedLemmas = 0;
   TNodeTrie* tat;
-  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
   if (d_eqc.isNull())
   {
     tat = tdb->getTermArgTrie(d_op);
@@ -187,7 +188,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
 
 int InstMatchGeneratorSimple::getActiveScore()
 {
-  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
   Node f = tdb->getMatchOperator(d_match_pattern);
   size_t ngt = tdb->getNumGroundTerms(f);
   Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) "
@@ -196,5 +197,6 @@ int InstMatchGeneratorSimple::getActiveScore()
 }
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
index bfb4b6840..ad48d9c91 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
@@ -25,6 +25,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 /** InstMatchGeneratorSimple class
@@ -101,6 +102,7 @@ class InstMatchGeneratorSimple : public IMGenerator
 };
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
 
diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp
index 2ca7f7af0..083331948 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy.cpp
@@ -23,8 +23,9 @@ namespace quantifiers {
 InstStrategy::InstStrategy(QuantifiersEngine* qe,
                            QuantifiersState& qs,
                            QuantifiersInferenceManager& qim,
-                           QuantifiersRegistry& qr)
-    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
+                           QuantifiersRegistry& qr,
+                           TermRegistry& tr)
+    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
 {
 }
 InstStrategy::~InstStrategy() {}
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index 84b9c4b77..cbe6e341b 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -32,6 +32,7 @@ namespace quantifiers {
 class QuantifiersState;
 class QuantifiersInferenceManager;
 class QuantifiersRegistry;
+class TermRegistry;
 
 /** A status response to process */
 enum class InstStrategyStatus
@@ -51,7 +52,8 @@ class InstStrategy
   InstStrategy(QuantifiersEngine* qe,
                QuantifiersState& qs,
                QuantifiersInferenceManager& qim,
-               QuantifiersRegistry& qr);
+               QuantifiersRegistry& qr,
+               TermRegistry& tr);
   virtual ~InstStrategy();
   /** presolve */
   virtual void presolve();
@@ -74,8 +76,10 @@ class InstStrategy
   QuantifiersState& d_qstate;
   /** The quantifiers inference manager object */
   QuantifiersInferenceManager& d_qim;
-  /** The quantifiers registry */
+  /** Reference to the quantifiers registry */
   QuantifiersRegistry& d_qreg;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
 }; /* 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 4470e5bf4..ba068230d 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -23,7 +23,7 @@
 #include "util/random.h"
 
 using namespace CVC4::kind;
-using namespace CVC4::theory::inst;
+using namespace CVC4::theory::quantifiers::inst;
 
 namespace CVC4 {
 namespace theory {
@@ -66,8 +66,9 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
     QuantifiersRegistry& qr,
+    TermRegistry& tr,
     QuantRelevance* qrlv)
-    : InstStrategy(qe, qs, qim, qr), d_quant_rel(qrlv)
+    : InstStrategy(qe, qs, qim, qr, tr), d_quant_rel(qrlv)
 {
   //how to select trigger terms
   d_tr_strategy = options::triggerSelMode();
@@ -284,6 +285,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
                               d_qstate,
                               d_qim,
                               d_qreg,
+                              d_treg,
                               f,
                               patTerms[0],
                               false,
@@ -323,6 +325,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
                               d_qstate,
                               d_qim,
                               d_qreg,
+                              d_treg,
                               f,
                               patTerms,
                               false,
@@ -367,6 +370,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
                                             d_qstate,
                                             d_qim,
                                             d_qreg,
+                                            d_treg,
                                             f,
                                             patTerms[index],
                                             false,
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index e0999e984..f4c74c43a 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -89,6 +89,7 @@ class InstStrategyAutoGenTriggers : public InstStrategy
                               QuantifiersState& qs,
                               QuantifiersInferenceManager& qim,
                               QuantifiersRegistry& qr,
+                              TermRegistry& tr,
                               QuantRelevance* qrlv);
   ~InstStrategyAutoGenTriggers() {}
 
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 c9e566b77..412676ad4 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -19,7 +19,7 @@
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
-using namespace CVC4::theory::inst;
+using namespace CVC4::theory::quantifiers::inst;
 
 namespace CVC4 {
 namespace theory {
@@ -29,15 +29,16 @@ InstStrategyUserPatterns::InstStrategyUserPatterns(
     QuantifiersEngine* ie,
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
-    QuantifiersRegistry& qr)
-    : InstStrategy(ie, qs, qim, qr)
+    QuantifiersRegistry& qr,
+    TermRegistry& tr)
+    : InstStrategy(ie, qs, qim, qr, tr)
 {
 }
 InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
 
 size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const
 {
-  std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
+  std::map<Node, std::vector<Trigger*> >::const_iterator it =
       d_user_gen.find(q);
   if (it == d_user_gen.end())
   {
@@ -46,10 +47,9 @@ size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const
   return it->second.size();
 }
 
-inst::Trigger* InstStrategyUserPatterns::getUserGenerator(Node q,
-                                                          size_t i) const
+Trigger* InstStrategyUserPatterns::getUserGenerator(Node q, size_t i) const
 {
-  std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
+  std::map<Node, std::vector<Trigger*> >::const_iterator it =
       d_user_gen.find(q);
   if (it == d_user_gen.end())
   {
@@ -111,6 +111,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q,
                                       d_qstate,
                                       d_qim,
                                       d_qreg,
+                                      d_treg,
                                       q,
                                       ugw[i],
                                       true,
@@ -123,7 +124,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q,
     ugw.clear();
   }
 
-  std::vector<inst::Trigger*>& ug = d_user_gen[q];
+  std::vector<Trigger*>& ug = d_user_gen[q];
   for (Trigger* t : ug)
   {
     if (Trace.isOn("process-trigger"))
@@ -171,6 +172,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
                                   d_qstate,
                                   d_qim,
                                   d_qreg,
+                                  d_treg,
                                   q,
                                   nodes,
                                   true,
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 4da092f70..e63154a60 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -37,7 +37,8 @@ class InstStrategyUserPatterns : public InstStrategy
   InstStrategyUserPatterns(QuantifiersEngine* qe,
                            QuantifiersState& qs,
                            QuantifiersInferenceManager& qim,
-                           QuantifiersRegistry& qr);
+                           QuantifiersRegistry& qr,
+                           TermRegistry& tr);
   ~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 619c8b9bb..1c301141c 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -24,10 +24,9 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
-using namespace std;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory::inst;
+using namespace CVC4::theory::quantifiers::inst;
 
 namespace CVC4 {
 namespace theory {
@@ -36,7 +35,8 @@ namespace quantifiers {
 InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
                                          QuantifiersState& qs,
                                          QuantifiersInferenceManager& qim,
-                                         QuantifiersRegistry& qr)
+                                         QuantifiersRegistry& qr,
+                                         TermRegistry& tr)
     : QuantifiersModule(qs, qim, qr, qe),
       d_instStrategies(),
       d_isup(),
@@ -53,13 +53,14 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
     // user-provided patterns
     if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
     {
-      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr));
+      d_isup.reset(
+          new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr, tr));
       d_instStrategies.push_back(d_isup.get());
     }
 
     // auto-generated patterns
     d_i_ag.reset(new InstStrategyAutoGenTriggers(
-        d_quantEngine, qs, qim, qr, d_quant_rel.get()));
+        d_quantEngine, qs, qim, qr, tr, d_quant_rel.get()));
     d_instStrategies.push_back(d_i_ag.get());
   }
 }
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index b327fb4a6..4042e3424 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -51,7 +51,8 @@ class InstantiationEngine : public QuantifiersModule {
   InstantiationEngine(QuantifiersEngine* qe,
                       QuantifiersState& qs,
                       QuantifiersInferenceManager& qim,
-                      QuantifiersRegistry& qr);
+                      QuantifiersRegistry& qr,
+                      TermRegistry& tr);
   ~InstantiationEngine();
   void presolve() override;
   bool needsCheck(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
index bdf5499fa..7ab54fcfe 100644
--- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
@@ -24,6 +24,7 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 PatternTermSelector::PatternTermSelector(Node q,
@@ -726,5 +727,6 @@ void PatternTermSelector::getTriggerVariables(Node n,
 }
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h
index a05600095..9cbf4cf5e 100644
--- a/src/theory/quantifiers/ematching/pattern_term_selector.h
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.h
@@ -25,6 +25,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 /**
@@ -189,6 +190,7 @@ class PatternTermSelector
 };
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
 
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 3940370cf..af0a0bfbc 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -38,16 +38,23 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 /** trigger class constructor */
 Trigger::Trigger(QuantifiersEngine* qe,
-                 quantifiers::QuantifiersState& qs,
-                 quantifiers::QuantifiersInferenceManager& qim,
-                 quantifiers::QuantifiersRegistry& qr,
+                 QuantifiersState& qs,
+                 QuantifiersInferenceManager& qim,
+                 QuantifiersRegistry& qr,
+                 TermRegistry& tr,
                  Node q,
                  std::vector<Node>& nodes)
-    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_quant(q)
+    : d_quantEngine(qe),
+      d_qstate(qs),
+      d_qim(qim),
+      d_qreg(qr),
+      d_treg(tr),
+      d_quant(q)
 {
   // We must ensure that the ground subterms of the trigger have been
   // preprocessed.
@@ -59,7 +66,7 @@ Trigger::Trigger(QuantifiersEngine* qe,
   }
   if (Trace.isOn("trigger"))
   {
-    quantifiers::QuantAttributes& qa = d_qreg.getQuantAttributes();
+    QuantAttributes& qa = d_qreg.getQuantAttributes();
     Trace("trigger") << "Trigger for " << qa.quantToString(q) << ": "
                      << std::endl;
     for (const Node& n : d_nodes)
@@ -169,8 +176,7 @@ bool Trigger::mkTriggerTerms(Node q,
   std::map< Node, std::vector< Node > > varContains;
   for (const Node& pat : temp)
   {
-    quantifiers::TermUtil::computeInstConstContainsForQuant(
-        q, pat, varContains[pat]);
+    TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
   }
   for (const Node& t : temp)
   {
@@ -178,7 +184,7 @@ bool Trigger::mkTriggerTerms(Node q,
     bool foundVar = false;
     for (const Node& v : vct)
     {
-      Assert(quantifiers::TermUtil::getInstConstAttr(v) == q);
+      Assert(TermUtil::getInstConstAttr(v) == q);
       if( vars.find( v )==vars.end() ){
         varCount++;
         vars[ v ] = true;
@@ -242,9 +248,10 @@ bool Trigger::mkTriggerTerms(Node q,
 }
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
-                            quantifiers::QuantifiersState& qs,
-                            quantifiers::QuantifiersInferenceManager& qim,
-                            quantifiers::QuantifiersRegistry& qr,
+                            QuantifiersState& qs,
+                            QuantifiersInferenceManager& qim,
+                            QuantifiersRegistry& qr,
+                            TermRegistry& tr,
                             Node f,
                             std::vector<Node>& nodes,
                             bool keepAll,
@@ -285,11 +292,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
   Trigger* t;
   if (!ho_apps.empty())
   {
-    t = new HigherOrderTrigger(qe, qs, qim, qr, f, trNodes, ho_apps);
+    t = new HigherOrderTrigger(qe, qs, qim, qr, tr, f, trNodes, ho_apps);
   }
   else
   {
-    t = new Trigger(qe, qs, qim, qr, f, trNodes);
+    t = new Trigger(qe, qs, qim, qr, tr, f, trNodes);
   }
 
   qe->getTriggerDatabase()->addTrigger( trNodes, t );
@@ -297,9 +304,10 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 }
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
-                            quantifiers::QuantifiersState& qs,
-                            quantifiers::QuantifiersInferenceManager& qim,
-                            quantifiers::QuantifiersRegistry& qr,
+                            QuantifiersState& qs,
+                            QuantifiersInferenceManager& qim,
+                            QuantifiersRegistry& qr,
+                            TermRegistry& tr,
                             Node f,
                             Node n,
                             bool keepAll,
@@ -308,7 +316,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 {
   std::vector< Node > nodes;
   nodes.push_back( n );
-  return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars);
+  return mkTrigger(qe, qs, qim, qr, tr, f, nodes, keepAll, trOption, useNVars);
 }
 
 int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
@@ -334,7 +342,7 @@ Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
       {
         visited[cur] = cur;
       }
-      else if (!quantifiers::TermUtil::hasInstConstAttr(cur))
+      else if (!TermUtil::hasInstConstAttr(cur))
       {
         // cur has no INST_CONSTANT, thus is ground.
         Node vcur = val.getPreprocessedTerm(cur);
@@ -382,6 +390,7 @@ void Trigger::debugPrint(const char* c) const
   Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl;
 }
 
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index b5a271fae..3c218ca7b 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -30,12 +30,12 @@ namespace quantifiers {
 class QuantifiersState;
 class QuantifiersInferenceManager;
 class QuantifiersRegistry;
-}
+class TermRegistry;
+class InstMatch;
 
 namespace inst {
 
 class IMGenerator;
-class InstMatch;
 class InstMatchGenerator;
 /** A collection of nodes representing a trigger.
 *
@@ -162,9 +162,10 @@ class Trigger {
     TR_RETURN_NULL  //return null if a duplicate is found
   };
   static Trigger* mkTrigger(QuantifiersEngine* qe,
-                            quantifiers::QuantifiersState& qs,
-                            quantifiers::QuantifiersInferenceManager& qim,
-                            quantifiers::QuantifiersRegistry& qr,
+                            QuantifiersState& qs,
+                            QuantifiersInferenceManager& qim,
+                            QuantifiersRegistry& qr,
+                            TermRegistry& tr,
                             Node q,
                             std::vector<Node>& nodes,
                             bool keepAll = true,
@@ -172,9 +173,10 @@ class Trigger {
                             size_t useNVars = 0);
   /** single trigger version that calls the above function */
   static Trigger* mkTrigger(QuantifiersEngine* qe,
-                            quantifiers::QuantifiersState& qs,
-                            quantifiers::QuantifiersInferenceManager& qim,
-                            quantifiers::QuantifiersRegistry& qr,
+                            QuantifiersState& qs,
+                            QuantifiersInferenceManager& qim,
+                            QuantifiersRegistry& qr,
+                            TermRegistry& tr,
                             Node q,
                             Node n,
                             bool keepAll = true,
@@ -197,9 +199,10 @@ class Trigger {
  protected:
   /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
   Trigger(QuantifiersEngine* ie,
-          quantifiers::QuantifiersState& qs,
-          quantifiers::QuantifiersInferenceManager& qim,
-          quantifiers::QuantifiersRegistry& qr,
+          QuantifiersState& qs,
+          QuantifiersInferenceManager& qim,
+          QuantifiersRegistry& qr,
+          TermRegistry& tr,
           Node q,
           std::vector<Node>& nodes);
   /** add an instantiation (called by InstMatchGenerator)
@@ -250,11 +253,13 @@ class Trigger {
   // !!!!!!!!!!!!!!!!!! temporarily available (project #15)
   QuantifiersEngine* d_quantEngine;
   /** Reference to the quantifiers state */
-  quantifiers::QuantifiersState& d_qstate;
+  QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
-  quantifiers::QuantifiersInferenceManager& d_qim;
+  QuantifiersInferenceManager& d_qim;
   /** The quantifiers registry */
-  quantifiers::QuantifiersRegistry& d_qreg;
+  QuantifiersRegistry& d_qreg;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
   /** The quantified formula this trigger is for. */
   Node d_quant;
   /** match generator
@@ -265,8 +270,9 @@ class Trigger {
   IMGenerator* d_mg;
 }; /* class Trigger */
 
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp
index c0aa6bcac..4bc74dd96 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.cpp
+++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp
@@ -20,6 +20,7 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 void TriggerTermInfo::init(Node q, Node n, int reqPol, Node reqPolEq)
@@ -111,5 +112,6 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n)
 }
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h
index bb829b432..5bf7e8099 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.h
+++ b/src/theory/quantifiers/ematching/trigger_term_info.h
@@ -23,6 +23,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 /** Information about a node used in a trigger.
@@ -121,6 +122,7 @@ class TriggerTermInfo
 };
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
 
diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp
index 2ed2f4fb6..04e9dabb0 100644
--- a/src/theory/quantifiers/ematching/trigger_trie.cpp
+++ b/src/theory/quantifiers/ematching/trigger_trie.cpp
@@ -16,6 +16,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 TriggerTrie::TriggerTrie() {}
@@ -71,5 +72,6 @@ void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
 }
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h
index c016031ed..ad221ee21 100644
--- a/src/theory/quantifiers/ematching/trigger_trie.h
+++ b/src/theory/quantifiers/ematching/trigger_trie.h
@@ -24,7 +24,7 @@
 
 namespace CVC4 {
 namespace theory {
-
+namespace quantifiers {
 namespace inst {
 
 /** A trie of triggers.
@@ -56,6 +56,7 @@ class TriggerTrie
 }; /* class inst::Trigger::TriggerTrie */
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
 
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index c8d907bcf..1f87c88b4 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -21,6 +21,7 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Trigger* tparent,
@@ -79,5 +80,6 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m)
 }
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h
index 591c47958..d85a20189 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.h
+++ b/src/theory/quantifiers/ematching/var_match_generator.h
@@ -22,6 +22,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 namespace inst {
 
 /** match generator for purified terms
@@ -50,6 +51,7 @@ class VarMatchGeneratorTermSubs : public InstMatchGenerator
 };
 
 }  // namespace inst
+}  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
 
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index be83f3b10..2245e16dd 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -28,14 +28,13 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 
-using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::theory::inst;
-using namespace CVC4::theory::quantifiers::fmcheck;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+namespace fmcheck {
 
 struct ModelBasisArgSort
 {
@@ -1370,3 +1369,8 @@ bool FullModelChecker::isHandled(Node q) const
 {
   return d_unhandledQuant.find(q) == d_unhandledQuant.end();
 }
+
+}  // namespace fmcheck
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 789a7bd7c..eb7398f92 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -23,13 +23,12 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 
-using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 //Model Engine constructor
 ModelEngine::ModelEngine(QuantifiersEngine* qe,
@@ -335,3 +334,6 @@ void ModelEngine::debugPrint( const char* c ){
   //d_quantEngine->getModel()->debugPrint( c );
 }
 
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index bb92b905e..a51d66278 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -21,7 +21,7 @@
 
 namespace CVC4 {
 namespace theory {
-namespace inst {
+namespace quantifiers {
 
 InstMatch::InstMatch(TNode q)
 {
@@ -103,6 +103,6 @@ bool InstMatch::set(quantifiers::QuantifiersState& qs, size_t i, TNode n)
   return true;
 }
 
-}/* CVC4::theory::inst namespace */
+}  // namespace quantifiers
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 7bab2083e..0c6ddcf77 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -23,12 +23,9 @@
 
 namespace CVC4 {
 namespace theory {
-
 namespace quantifiers {
-class QuantifiersState;
-}
 
-namespace inst {
+class QuantifiersState;
 
 /** Inst match
  *
@@ -90,10 +87,7 @@ inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
   return out;
 }
 
-}/* CVC4::theory::inst namespace */
-
-typedef CVC4::theory::inst::InstMatch InstMatch;
-
+}  // namespace quantifiers
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index 9c3b9af93..96f668c82 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -25,7 +25,7 @@ using namespace CVC4::context;
 
 namespace CVC4 {
 namespace theory {
-namespace inst {
+namespace quantifiers {
 
 bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
                                     Node q,
@@ -368,6 +368,6 @@ bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs,
   return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
 }
 
-} /* CVC4::theory::inst namespace */
+}  // namespace quantifiers
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index 6e6dd92bf..5164f1820 100644
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -25,14 +25,9 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
-class QuantifiersState;
-}
 
-namespace inst {
+class QuantifiersState;
 
 /** trie for InstMatch objects
  *
@@ -62,7 +57,7 @@ class InstMatchTrie
    * If modEq is true, we check for duplication modulo equality the current
    * equalities in the equality engine of qs.
    */
-  bool existsInstMatch(quantifiers::QuantifiersState& qs,
+  bool existsInstMatch(QuantifiersState& qs,
                        Node q,
                        const std::vector<Node>& m,
                        bool modEq = false,
@@ -76,7 +71,7 @@ class InstMatchTrie
    * If modEq is true, we check for duplication modulo equality the current
    * equalities in the equality engine of qs.
    */
-  bool addInstMatch(quantifiers::QuantifiersState& qs,
+  bool addInstMatch(QuantifiersState& qs,
                     Node f,
                     const std::vector<Node>& m,
                     bool modEq = false,
@@ -135,7 +130,7 @@ class CDInstMatchTrie
    * equalities in the equality engine of qs.
    * It additionally takes a context c, for which the entry is valid in.
    */
-  bool existsInstMatch(quantifiers::QuantifiersState& qs,
+  bool existsInstMatch(QuantifiersState& qs,
                        Node q,
                        const std::vector<Node>& m,
                        bool modEq = false,
@@ -149,7 +144,7 @@ class CDInstMatchTrie
    * equalities in the equality engine of qs.
    * It additionally takes a context c, for which the entry is valid in.
    */
-  bool addInstMatch(quantifiers::QuantifiersState& qs,
+  bool addInstMatch(QuantifiersState& qs,
                     Node q,
                     const std::vector<Node>& m,
                     bool modEq = false,
@@ -205,7 +200,7 @@ class InstMatchTrieOrdered
    * class. If modEq is true, we consider duplicates modulo the current
    * equalities stored in the equality engine of qs.
    */
-  bool addInstMatch(quantifiers::QuantifiersState& qs,
+  bool addInstMatch(QuantifiersState& qs,
                     Node q,
                     const std::vector<Node>& m,
                     bool modEq = false);
@@ -215,7 +210,7 @@ class InstMatchTrieOrdered
    * class. If modEq is true, we consider duplicates modulo the current
    * equalities stored in the equality engine of qs.
    */
-  bool existsInstMatch(quantifiers::QuantifiersState& qs,
+  bool existsInstMatch(QuantifiersState& qs,
                        Node q,
                        const std::vector<Node>& m,
                        bool modEq = false);
@@ -227,8 +222,8 @@ class InstMatchTrieOrdered
   InstMatchTrie d_imt;
 };
 
-} /* CVC4::theory::inst namespace */
+}  // namespace quantifiers
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
 
-#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 6efcd2adf..c14ce4ad3 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -28,11 +28,10 @@ using namespace kind;
 using namespace context;
 
 namespace theory {
+namespace quantifiers {
 
 using namespace inst;
 
-namespace quantifiers {
-
 InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
                                    QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index fd74e17e8..61c7703ed 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -45,13 +45,11 @@ Instantiate::Instantiate(QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr,
-                         FirstOrderModel* m,
                          ProofNodeManager* pnm)
     : d_qstate(qs),
       d_qim(qim),
       d_qreg(qr),
       d_treg(tr),
-      d_model(m),
       d_pnm(pnm),
       d_total_inst_debug(qs.getUserContext()),
       d_c_inst_match_trie_dom(qs.getUserContext()),
@@ -61,7 +59,7 @@ Instantiate::Instantiate(QuantifiersState& qs,
 
 Instantiate::~Instantiate()
 {
-  for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+  for (std::pair<const Node, CDInstMatchTrie*>& t : d_c_inst_match_trie)
   {
     delete t.second;
   }
@@ -121,7 +119,7 @@ bool Instantiate::addInstantiation(Node q,
     TypeNode tn = q[0][i].getType();
     if (terms[i].isNull())
     {
-      terms[i] = getTermForType(tn);
+      terms[i] = d_treg.getTermForType(tn);
     }
     // Ensure the type is correct, this for instance ensures that real terms
     // are cast to integers for { x -> t } where x has type Int and t has
@@ -131,7 +129,7 @@ bool Instantiate::addInstantiation(Node q,
     {
       // pick the best possible representative for instantiation, based on past
       // use and simplicity of term
-      terms[i] = d_model->getInternalRepresentative(terms[i], q, i);
+      terms[i] = d_treg.getModel()->getInternalRepresentative(terms[i], q, i);
     }
     Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
     if (terms[i].isNull())
@@ -496,8 +494,7 @@ bool Instantiate::existsInstantiation(Node q,
 {
   if (options::incrementalSolving())
   {
-    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
-        d_c_inst_match_trie.find(q);
+    std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
     {
       return it->second->existsInstMatch(d_qstate, q, terms, modEq);
@@ -505,8 +502,7 @@ bool Instantiate::existsInstantiation(Node q,
   }
   else
   {
-    std::map<Node, inst::InstMatchTrie>::iterator it =
-        d_inst_match_trie.find(q);
+    std::map<Node, InstMatchTrie>::iterator it = d_inst_match_trie.find(q);
     if (it != d_inst_match_trie.end())
     {
       return it->second.existsInstMatch(d_qstate, q, terms, modEq);
@@ -579,16 +575,15 @@ bool Instantiate::recordInstantiationInternal(Node q,
     Trace("inst-add-debug")
         << "Adding into context-dependent inst trie, modEq = " << modEq
         << std::endl;
-    inst::CDInstMatchTrie* imt;
-    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
-        d_c_inst_match_trie.find(q);
+    CDInstMatchTrie* imt;
+    std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
     {
       imt = it->second;
     }
     else
     {
-      imt = new inst::CDInstMatchTrie(d_qstate.getUserContext());
+      imt = new CDInstMatchTrie(d_qstate.getUserContext());
       d_c_inst_match_trie[q] = imt;
     }
     d_c_inst_match_trie_dom.insert(q);
@@ -602,8 +597,7 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
 {
   if (options::incrementalSolving())
   {
-    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
-        d_c_inst_match_trie.find(q);
+    std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
     {
       return it->second->removeInstMatch(q, terms);
@@ -613,15 +607,6 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
   return d_inst_match_trie[q].removeInstMatch(q, terms);
 }
 
-Node Instantiate::getTermForType(TypeNode tn)
-{
-  if (tn.isClosedEnumerable())
-  {
-    return d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0);
-  }
-  return d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn);
-}
-
 void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 {
   if (options::incrementalSolving())
@@ -636,7 +621,7 @@ void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
   }
   else
   {
-    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    for (std::pair<const Node, InstMatchTrie>& t : d_inst_match_trie)
     {
       qs.push_back(t.first);
     }
@@ -649,7 +634,7 @@ void Instantiate::getInstantiationTermVectors(
 
   if (options::incrementalSolving())
   {
-    std::map<Node, inst::CDInstMatchTrie*>::const_iterator it =
+    std::map<Node, CDInstMatchTrie*>::const_iterator it =
         d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
     {
@@ -658,7 +643,7 @@ void Instantiate::getInstantiationTermVectors(
   }
   else
   {
-    std::map<Node, inst::InstMatchTrie>::const_iterator it =
+    std::map<Node, InstMatchTrie>::const_iterator it =
         d_inst_match_trie.find(q);
     if (it != d_inst_match_trie.end())
     {
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 8e556b648..be410c2c8 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -97,7 +97,6 @@ class Instantiate : public QuantifiersUtil
               QuantifiersInferenceManager& qim,
               QuantifiersRegistry& qr,
               TermRegistry& tr,
-              FirstOrderModel* m,
               ProofNodeManager* pnm = nullptr);
   ~Instantiate();
 
@@ -224,17 +223,6 @@ class Instantiate : public QuantifiersUtil
    * Same as above but with vars equal to the bound variables of q.
    */
   Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false);
-  /** get term for type
-   *
-   * This returns an arbitrary term for type tn.
-   * This term is chosen heuristically to be the best
-   * term for instantiation. Currently, this
-   * heuristic enumerates the first term of the
-   * type if the type is closed enumerable, otherwise
-   * an existing ground term from the term database if
-   * one exists, or otherwise a fresh variable.
-   */
-  Node getTermForType(TypeNode tn);
   //--------------------------------------end general utilities
 
   /**
@@ -318,8 +306,6 @@ class Instantiate : public QuantifiersUtil
   QuantifiersRegistry& d_qreg;
   /** Reference to the term registry */
   TermRegistry& d_treg;
-  /** Pointer to the model */
-  FirstOrderModel* d_model;
   /** pointer to the proof node manager */
   ProofNodeManager* d_pnm;
   /** instantiation rewriter classes */
@@ -335,8 +321,8 @@ class Instantiate : public QuantifiersUtil
    * We store context (dependent, independent) versions. If incremental solving
    * is disabled, we use d_inst_match_trie for performance reasons.
    */
-  std::map<Node, inst::InstMatchTrie> d_inst_match_trie;
-  std::map<Node, inst::CDInstMatchTrie*> d_c_inst_match_trie;
+  std::map<Node, InstMatchTrie> d_inst_match_trie;
+  std::map<Node, CDInstMatchTrie*> d_c_inst_match_trie;
   /**
    * The list of quantified formulas for which the domain of d_c_inst_match_trie
    * is valid.
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index 9a82265f9..b25c1aed3 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -26,10 +26,9 @@ QuantifiersInferenceManager::QuantifiersInferenceManager(
     QuantifiersState& state,
     QuantifiersRegistry& qr,
     TermRegistry& tr,
-    FirstOrderModel* m,
     ProofNodeManager* pnm)
     : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"),
-      d_instantiate(new Instantiate(state, *this, qr, tr, m, pnm)),
+      d_instantiate(new Instantiate(state, *this, qr, tr, pnm)),
       d_skolemize(new Skolemize(state, pnm))
 {
 }
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h
index aa7fc1b6a..f16f91f04 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.h
+++ b/src/theory/quantifiers/quantifiers_inference_manager.h
@@ -39,7 +39,6 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered
                               QuantifiersState& state,
                               QuantifiersRegistry& qr,
                               TermRegistry& tr,
-                              FirstOrderModel* m,
                               ProofNodeManager* pnm);
   ~QuantifiersInferenceManager();
   /** get instantiate utility */
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 11d9a116c..bb35d6d26 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -15,8 +15,9 @@
 #include "theory/quantifiers/quantifiers_modules.h"
 
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_registry.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -43,6 +44,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
                                     QuantifiersState& qs,
                                     QuantifiersInferenceManager& qim,
                                     QuantifiersRegistry& qr,
+                                    TermRegistry& tr,
                                     DecisionManager* dm,
                                     std::vector<QuantifiersModule*>& modules)
 {
@@ -59,7 +61,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   }
   if (!options::finiteModelFind() || options::fmfInstEngine())
   {
-    d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr));
+    d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr, tr));
     modules.push_back(d_inst_engine.get());
   }
   if (options::cegqi())
@@ -86,7 +88,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
     Trace("quant-init-debug")
         << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
         << options::fmfBound() << std::endl;
-    if (useFmcModel())
+    if (tr.useFmcModel())
     {
       Trace("quant-init-debug") << "...make fmc builder." << std::endl;
       d_builder.reset(new fmcheck::FullModelChecker(qs, qr));
@@ -123,13 +125,6 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   }
 }
 
-bool QuantifiersModules::useFmcModel()
-{
-  return options::mbqiMode() == options::MbqiMode::FMC
-         || options::mbqiMode() == options::MbqiMode::TRUST
-         || options::fmfBound();
-}
-
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index c111eba25..4ecbf7af4 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -58,12 +58,10 @@ class QuantifiersModules
                   QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
+                  TermRegistry& tr,
                   DecisionManager* dm,
                   std::vector<QuantifiersModule*>& modules);
 
-  /** Whether we use the full model check builder and corresponding model */
-  static bool useFmcModel();
-
  private:
   //------------------------------ quantifier utilities
   /** relevant domain */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ca11d491d..a6d138806 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -28,10 +28,8 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
-using namespace std;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory::inst;
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index d23ff060a..74dad6cc7 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -16,6 +16,8 @@
 
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/quantifiers_state.h"
 
 namespace CVC4 {
@@ -24,6 +26,7 @@ namespace quantifiers {
 
 TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
     : d_presolve(qs.getUserContext(), true),
+      d_useFmcModel(false),
       d_presolveCache(qs.getUserContext()),
       d_termEnum(new TermEnumeration),
       d_termDb(new TermDb(qs, qr)),
@@ -34,6 +37,26 @@ TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
     // must be constructed here since it is required for datatypes finistInit
     d_sygusTdb.reset(new TermDbSygus(qs));
   }
+  Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
+  Trace("quant-engine-debug")
+      << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
+  // Finite model finding requires specialized ways of building the model.
+  // We require constructing the model here, since it is required for
+  // initializing the CombinationEngine and the rest of quantifiers engine.
+  if ((options::finiteModelFind() || options::fmfBound())
+      && (options::mbqiMode() == options::MbqiMode::FMC
+          || options::mbqiMode() == options::MbqiMode::TRUST
+          || options::fmfBound()))
+  {
+    d_useFmcModel = true;
+    d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
+        qs, qr, *this, "FirstOrderModelFmc"));
+  }
+  else
+  {
+    d_qmodel.reset(
+        new quantifiers::FirstOrderModel(qs, qr, *this, "FirstOrderModel"));
+  }
 }
 
 void TermRegistry::finishInit(QuantifiersInferenceManager* qim)
@@ -84,6 +107,15 @@ void TermRegistry::addTerm(Node n, bool withinQuant)
   }
 }
 
+Node TermRegistry::getTermForType(TypeNode tn)
+{
+  if (tn.isClosedEnumerable())
+  {
+    return d_termEnum->getEnumerateTerm(tn, 0);
+  }
+  return d_termDb->getOrMakeTypeGroundTerm(tn);
+}
+
 TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); }
 
 TermDbSygus* TermRegistry::getTermDatabaseSygus() const
@@ -95,6 +127,11 @@ TermEnumeration* TermRegistry::getTermEnumeration() const
 {
   return d_termEnum.get();
 }
+
+FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); }
+
+bool TermRegistry::useFmcModel() const { return d_useFmcModel; }
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index 1d9058603..d70b7acf8 100644
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -29,6 +29,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class FirstOrderModel;
+
 /**
  * Term Registry, which manages notifying modules within quantifiers about
  * (ground) terms that exist in the current context.
@@ -54,16 +56,35 @@ class TermRegistry
    */
   void addTerm(Node n, bool withinQuant = false);
 
+  /** get term for type
+   *
+   * This returns an arbitrary term for type tn.
+   * This term is chosen heuristically to be the best
+   * term for instantiation. Currently, this
+   * heuristic enumerates the first term of the
+   * type if the type is closed enumerable, otherwise
+   * an existing ground term from the term database if
+   * one exists, or otherwise a fresh variable.
+   */
+  Node getTermForType(TypeNode tn);
+
+  /** Whether we use the full model check builder and corresponding model */
+  bool useFmcModel() const;
+
   /** get term database */
   TermDb* getTermDatabase() const;
   /** get term database sygus */
   TermDbSygus* getTermDatabaseSygus() const;
   /** get term enumeration utility */
   TermEnumeration* getTermEnumeration() const;
+  /** get the model utility */
+  FirstOrderModel* getModel() const;
 
  private:
   /** has presolve been called */
   context::CDO<bool> d_presolve;
+  /** Whether we are using the fmc model */
+  bool d_useFmcModel;
   /** the set of terms we have seen before presolve */
   NodeSet d_presolveCache;
   /** term enumeration utility */
@@ -72,6 +93,8 @@ class TermRegistry
   std::unique_ptr<TermDb> d_termDb;
   /** sygus term database */
   std::unique_ptr<TermDbSygus> d_sygusTdb;
+  /** extended model object */
+  std::unique_ptr<FirstOrderModel> d_qmodel;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 069b9b935..d555a85da 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -27,10 +27,7 @@
 #include "theory/strings/word.h"
 #include "theory/rewriter.h"
 
-using namespace std;
 using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory::inst;
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 092689b5f..ace7b79ff 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -18,8 +18,6 @@
 
 #include "expr/proof_node_manager.h"
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/quantifiers_modules.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/valuation.h"
@@ -41,7 +39,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
       d_qstate(c, u, valuation, logicInfo),
       d_qreg(),
       d_treg(d_qstate, d_qreg),
-      d_qim(nullptr),
+      d_qim(*this, d_qstate, d_qreg, d_treg, pnm),
       d_qengine(nullptr)
 {
   out.handleUserAttribute( "fun-def", this );
@@ -57,45 +55,23 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
     d_qChecker.registerTo(pc);
   }
 
-  Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
-  Trace("quant-engine-debug")
-      << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
-  // Finite model finding requires specialized ways of building the model.
-  // We require constructing the model here, since it is required for
-  // initializing the CombinationEngine and the rest of quantifiers engine.
-  if ((options::finiteModelFind() || options::fmfBound())
-      && QuantifiersModules::useFmcModel())
-  {
-    d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-        d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
-  }
-  else
-  {
-    d_qmodel.reset(new quantifiers::FirstOrderModel(
-        d_qstate, d_qreg, d_treg, "FirstOrderModel"));
-  }
-
-  d_qim.reset(new QuantifiersInferenceManager(
-      *this, d_qstate, d_qreg, d_treg, d_qmodel.get(), pnm));
-
   // Finish initializing the term registry by hooking it up to the inference
   // manager. This is required due to a cyclic dependency between the term
   // database and the instantiate module. Term database needs inference manager
   // since it sends out lemmas when term indexing is inconsistent, instantiate
   // needs term database for entailment checks.
-  d_treg.finishInit(d_qim.get());
+  d_treg.finishInit(&d_qim);
 
   // construct the quantifiers engine
-  d_qengine.reset(new QuantifiersEngine(
-      d_qstate, d_qreg, d_treg, *d_qim.get(), d_qmodel.get(), pnm));
+  d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm));
 
   //!!!!!!!!!!!!!! temporary (project #15)
-  d_qmodel->finishInit(d_qengine.get());
+  d_treg.getModel()->finishInit(d_qengine.get());
 
   // indicate we are using the quantifiers theory state object
   d_theoryState = &d_qstate;
   // use the inference manager as the official inference manager
-  d_inferManager = d_qim.get();
+  d_inferManager = &d_qim;
   // Set the pointer to the quantifiers engine, which this theory owns. This
   // pointer will be retreived by TheoryEngine and set to all theories
   // post-construction.
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 2371b00ce..91f12c0ed 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -20,7 +20,6 @@
 #define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
 #include "expr/node.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/proof_checker.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_registry.h"
@@ -89,12 +88,10 @@ class TheoryQuantifiers : public Theory {
   QuantifiersState d_qstate;
   /** The quantifiers registry */
   QuantifiersRegistry d_qreg;
-  /** extended model object */
-  std::unique_ptr<FirstOrderModel> d_qmodel;
   /** The term registry */
   TermRegistry d_treg;
   /** The quantifiers inference manager */
-  std::unique_ptr<QuantifiersInferenceManager> d_qim;
+  QuantifiersInferenceManager d_qim;
   /** The quantifiers engine, which lives here */
   std::unique_ptr<QuantifiersEngine> d_qengine;
 };/* class TheoryQuantifiers */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9ca8226bc..2cface166 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -51,7 +51,6 @@ QuantifiersEngine::QuantifiersEngine(
     quantifiers::QuantifiersRegistry& qr,
     quantifiers::TermRegistry& tr,
     quantifiers::QuantifiersInferenceManager& qim,
-    quantifiers::FirstOrderModel* qm,
     ProofNodeManager* pnm)
     : d_qstate(qstate),
       d_qim(qim),
@@ -60,8 +59,8 @@ QuantifiersEngine::QuantifiersEngine(
       d_pnm(pnm),
       d_qreg(qr),
       d_treg(tr),
-      d_tr_trie(new inst::TriggerTrie),
-      d_model(qm),
+      d_tr_trie(new quantifiers::inst::TriggerTrie),
+      d_model(d_treg.getModel()),
       d_quants_prereg(qstate.getUserContext()),
       d_quants_red(qstate.getUserContext())
 {
@@ -81,7 +80,7 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
   d_decManager = dm;
   // Initialize the modules and the utilities here.
   d_qmodules.reset(new quantifiers::QuantifiersModules);
-  d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, dm, d_modules);
+  d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_treg, dm, d_modules);
   if (d_qmodules->d_rel_dom.get())
   {
     d_util.push_back(d_qmodules->d_rel_dom.get());
@@ -145,7 +144,7 @@ quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
 {
   return d_qim.getSkolemize();
 }
-inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
+quantifiers::inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
 {
   return d_tr_trie.get();
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b6562caa7..1f1dcc950 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -36,10 +36,12 @@ class DecisionManager;
 class QuantifiersModule;
 class RepSetIterator;
 
+namespace quantifiers {
+
 namespace inst {
 class TriggerTrie;
 }
-namespace quantifiers {
+
 class FirstOrderModel;
 class Instantiate;
 class QModelBuilder;
@@ -67,7 +69,6 @@ class QuantifiersEngine {
                     quantifiers::QuantifiersRegistry& qr,
                     quantifiers::TermRegistry& tr,
                     quantifiers::QuantifiersInferenceManager& qim,
-                    quantifiers::FirstOrderModel* qm,
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
   //---------------------- external interface
@@ -96,7 +97,7 @@ class QuantifiersEngine {
   /** get skolemize utility */
   quantifiers::Skolemize* getSkolemize() const;
   /** get trigger database */
-  inst::TriggerTrie* getTriggerDatabase() const;
+  quantifiers::inst::TriggerTrie* getTriggerDatabase() const;
   //---------------------- end utilities
  private:
   //---------------------- private initialization
@@ -234,7 +235,7 @@ public:
   /** The term registry */
   quantifiers::TermRegistry& d_treg;
   /** all triggers will be stored in this trie */
-  std::unique_ptr<inst::TriggerTrie> d_tr_trie;
+  std::unique_ptr<quantifiers::inst::TriggerTrie> d_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
   //------------- end quantifiers utilities