(Refactor) Instantiate utility (#1387)

33 files changed, 2493 insertions, 1311 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index b3c4ec98c..f50893497 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -395,8 +395,12 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/fun_def_process.h \
 	theory/quantifiers/ho_trigger.cpp \
 	theory/quantifiers/ho_trigger.h \
+	theory/quantifiers/instantiate.cpp \
+	theory/quantifiers/instantiate.h \
 	theory/quantifiers/inst_match.cpp \
 	theory/quantifiers/inst_match.h \
+	theory/quantifiers/inst_match_trie.cpp \
+	theory/quantifiers/inst_match_trie.h \
 	theory/quantifiers/inst_match_generator.cpp \
 	theory/quantifiers/inst_match_generator.h \
 	theory/quantifiers/inst_propagator.cpp \
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index c418d0fb1..0a6df7df5 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/ambqi_builder.h"
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 
@@ -165,7 +166,8 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe,
       return true;
     }else{
       if( depth==q[0].getNumChildren() ){
-        if( qe->addInstantiation( q, terms, true ) ){
+        if (qe->getInstantiate()->addInstantiation(q, terms, true))
+        {
           Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;
           inst++;
           return true;
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 712112615..699a93286 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -12,9 +12,10 @@
  ** \brief Implementation of theory uf candidate generator class
  **/
 
-#include "options/quantifiers_options.h"
 #include "theory/quantifiers/candidate_generator.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -302,7 +303,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
   if( d_firstTime ){
     //must return something
     d_firstTime = false;
-    return d_qe->getTermForType(d_match_pattern_type);
+    return d_qe->getInstantiate()->getTermForType(d_match_pattern_type);
   }
   return Node::null();
 }
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index bc6817560..378b26eef 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -21,6 +21,7 @@
 #include "prop/prop_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database_sygus.h"
@@ -108,7 +109,8 @@ void CegConjecture::assign( Node q ) {
   }
   Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl;
   //construct base instantiation
-  d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( d_embed_quant, vars, d_candidates ) );
+  d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation(
+      d_embed_quant, vars, d_candidates));
   Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
 
   // register this term with sygus database and other utilities that impact
@@ -224,7 +226,8 @@ void CegConjecture::doBasicCheck(std::vector< Node >& lems) {
   getCandidateList( clist, true );
   Assert( clist.size()==d_quant[0].getNumChildren() );
   getModelValues( clist, model_terms );
-  if( d_qe->addInstantiation( d_quant, model_terms ) ){
+  if (d_qe->getInstantiate()->addInstantiation(d_quant, model_terms))
+  {
     //record the instantiation
     recordInstantiation( model_terms );
   }else{
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 8e63e8909..33fc7303f 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -20,6 +20,7 @@
 #include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 #include "theory/quantifiers/ce_guided_single_inv_sol.h"
+#include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/inst_strategy_cbqi.h"
 #include "theory/quantifiers/single_inv_partition.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index e79f3456b..86878b9ca 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -15,8 +15,9 @@
 #include "theory/quantifiers/equality_query.h"
 
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/equality_infer.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 4277ab366..15b96d2a0 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -12,9 +12,10 @@
  ** \brief Implementation of full model check class
  **/
 
+#include "theory/quantifiers/full_model_check.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 
@@ -694,7 +695,8 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
               }else{
                 //just add the instance
                 d_triedLemmas++;
-                if( d_qe->addInstantiation( f, inst, true ) ){
+                if (d_qe->getInstantiate()->addInstantiation(f, inst, true))
+                {
                   Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
                   d_addedLemmas++;
                   if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
@@ -845,7 +847,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       if (ev!=d_true) {
         Trace("fmc-exh-debug") << ", add!";
         //add as instantiation
-        if( d_qe->addInstantiation( f, inst, true ) ){
+        if (d_qe->getInstantiate()->addInstantiation(f, inst, true))
+        {
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
           if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
diff --git a/src/theory/quantifiers/ho_trigger.cpp b/src/theory/quantifiers/ho_trigger.cpp
index b0ac02a25..0386c0cf0 100644
--- a/src/theory/quantifiers/ho_trigger.cpp
+++ b/src/theory/quantifiers/ho_trigger.cpp
@@ -15,6 +15,7 @@
 #include <stack>
 
 #include "theory/quantifiers/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"
@@ -325,7 +326,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
   else
   {
     // do not run higher-order matching
-    return d_quantEngine->addInstantiation(d_f, m);
+    return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
   }
 }
 
@@ -336,7 +337,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
   if (var_index == d_ho_var_list.size())
   {
     // we now have an instantiation to try
-    return d_quantEngine->addInstantiation(d_f, m);
+    return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
   }
   else
   {
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index e24b8f96a..da16010cd 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -13,41 +13,42 @@
  **/
 
 #include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/term_database.h"
+
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_util.h"
+#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;
-
 namespace CVC4 {
 namespace theory {
 namespace inst {
 
-InstMatch::InstMatch( TNode f ) {
-  for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-    d_vals.push_back( Node::null() );
-  }
+InstMatch::InstMatch(TNode q)
+{
+  d_vals.resize(q[0].getNumChildren());
+  Assert(!d_vals.empty());
+  // resize must initialize with null nodes
+  Assert(d_vals[0].isNull());
 }
 
 InstMatch::InstMatch( InstMatch* m ) {
   d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() );
 }
 
-bool InstMatch::add( InstMatch& m ){
-  for( unsigned i=0; i<d_vals.size(); i++ ){
+void InstMatch::add(InstMatch& m)
+{
+  for (unsigned i = 0, size = d_vals.size(); i < size; i++)
+  {
     if( d_vals[i].isNull() ){
       d_vals[i] = m.d_vals[i];
     }
   }
-  return true;
 }
 
 bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
-  for( unsigned i=0; i<m.d_vals.size(); i++ ){
+  Assert(d_vals.size() == m.d_vals.size());
+  for (unsigned i = 0, size = d_vals.size(); i < size; i++)
+  {
     if( !m.d_vals[i].isNull() ){
       if( d_vals[i].isNull() ){
         d_vals[i] = m.d_vals[i];
@@ -63,7 +64,8 @@ bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
 }
 
 void InstMatch::debugPrint( const char* c ){
-  for( unsigned i=0; i<d_vals.size(); i++ ){
+  for (unsigned i = 0, size = d_vals.size(); i < size; i++)
+  {
     if( !d_vals[i].isNull() ){
       Debug( c ) << "   " << i << " -> " << d_vals[i] << std::endl;
     }
@@ -71,8 +73,10 @@ void InstMatch::debugPrint( const char* c ){
 }
 
 bool InstMatch::isComplete() {
-  for( unsigned i=0; i<d_vals.size(); i++ ){
-    if( d_vals[i].isNull() ){
+  for (Node& v : d_vals)
+  {
+    if (v.isNull())
+    {
       return false;
     }
   }
@@ -80,58 +84,37 @@ bool InstMatch::isComplete() {
 }
 
 bool InstMatch::empty() {
-  for( unsigned i=0; i<d_vals.size(); i++ ){
-    if( !d_vals[i].isNull() ){
+  for (Node& v : d_vals)
+  {
+    if (!v.isNull())
+    {
       return false;
     }
   }
   return true;
 }
 
-void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
-  for( unsigned i=0; i<d_vals.size(); i++ ){
-    if( !d_vals[i].isNull() ){
-      if( qe->getEqualityQuery()->getEngine()->hasTerm( d_vals[i] ) ){
-        d_vals[i] = qe->getEqualityQuery()->getEngine()->getRepresentative( d_vals[i] );
-      }
-    }
-  }
-}
-
-void InstMatch::applyRewrite(){
-  for( unsigned i=0; i<d_vals.size(); i++ ){
-    if( !d_vals[i].isNull() ){
-      d_vals[i] = Rewriter::rewrite( d_vals[i] );
-    }
-  }
-}
-
 void InstMatch::clear() {
   for( unsigned i=0; i<d_vals.size(); i++ ){
     d_vals[i] = Node::null();
   }
 }
 
-/** get value */
-
-Node InstMatch::get( int i ) {
-  return d_vals[i];
-}
-
-void InstMatch::getTerms( Node f, std::vector< Node >& inst ){
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    inst.push_back( d_vals[i] );
-  }
+Node InstMatch::get(int i) const { return d_vals[i]; }
+void InstMatch::getInst(std::vector<Node>& inst) const
+{
+  inst.insert(inst.end(), d_vals.begin(), d_vals.end());
 }
 
 void InstMatch::setValue( int i, TNode n ) {
   d_vals[i] = n;
 }
-
-bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
+bool InstMatch::set(EqualityQuery* q, int i, TNode n)
+{
   Assert( i>=0 );
   if( !d_vals[i].isNull() ){
-    if( qe->getEqualityQuery()->areEqual( d_vals[i], n ) ){
+    if (q->areEqual(d_vals[i], n))
+    {
       return true;
     }else{
       return false;
@@ -142,341 +125,6 @@ bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
   }
 }
 
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq,
-                                  ImtIndexOrder* imtio, bool onlyExist, int index ) {
-  if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
-    return false;
-  }else{
-    int i_index = imtio ? imtio->d_order[index] : index;
-    Node n = m[i_index];
-    std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
-    if( it!=d_data.end() ){
-      bool ret = it->second.addInstMatch( qe, f, m, modEq, imtio, onlyExist, index+1 );
-      if( !onlyExist || !ret ){
-        return ret;
-      }
-    }
-    if( modEq ){
-      //check modulo equality if any other instantiation match exists
-      if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
-        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
-                                 qe->getEqualityQuery()->getEngine() );
-        while( !eqc.isFinished() ){
-          Node en = (*eqc);
-          if( en!=n ){
-            std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
-            if( itc!=d_data.end() ){
-              if( itc->second.addInstMatch( qe, f, m, modEq, imtio, true, index+1 ) ){
-                return false;
-              }
-            }
-          }
-          ++eqc;
-        }
-      }
-    }
-    if( !onlyExist ){
-      d_data[n].addInstMatch( qe, f, m, modEq, imtio, false, index+1 );
-    }
-    return true;
-  }
-}
-
-bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, ImtIndexOrder* imtio, int index ) {
-  Assert( index<(int)q[0].getNumChildren() );
-  Assert( !imtio || index<(int)imtio->d_order.size() );
-  int i_index = imtio ? imtio->d_order[index] : index;
-  Node n = m[i_index];
-  std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
-  if( it!=d_data.end() ){
-    if( (index+1)==(int)q[0].getNumChildren() || ( imtio && (index+1)==(int)imtio->d_order.size() ) ){
-      d_data.erase( n );
-      return true;
-    }else{
-      return it->second.removeInstMatch( qe, q, m, imtio, index+1 );
-    }
-  }else{
-    return false;
-  }
-}
-
-bool InstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio, int index ){
-  if( index==(int)q[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
-    setInstLemma( lem );
-    return true;
-  }else{
-    int i_index = imtio ? imtio->d_order[index] : index;
-    std::map< Node, InstMatchTrie >::iterator it = d_data.find( m[i_index] );
-    if( it!=d_data.end() ){
-      return it->second.recordInstLemma( q, m, lem, imtio, index+1 );
-    }else{
-      return false;
-    }
-  }
-}
-
-void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const {
-  if( terms.size()==q[0].getNumChildren() ){
-    bool print;
-    if( useActive ){
-      if( hasInstLemma() ){
-        Node lem = getInstLemma();
-        print = std::find( active.begin(), active.end(), lem )!=active.end();
-      }else{
-        print = false;
-      }
-    }else{
-      print = true;
-    }  
-    if( print ){ 
-      if( firstTime ){
-        out << "(instantiation " << q << std::endl;
-        firstTime = false;
-      }
-      out << "  ( ";
-      for( unsigned i=0; i<terms.size(); i++ ){
-        if( i>0 ){ out << ", ";}
-        out << terms[i];
-      }
-      out << " )" << std::endl;
-    }
-  }else{
-    for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
-      terms.push_back( it->first );
-      it->second.print( out, q, terms, firstTime, useActive, active );
-      terms.pop_back();
-    }
-  }
-}
-
-void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const {
-  if( terms.size()==q[0].getNumChildren() ){
-    if( useActive ){
-      if( hasInstLemma() ){
-        Node lem = getInstLemma();
-        if( std::find( active.begin(), active.end(), lem )!=active.end() ){
-          insts.push_back( lem );
-        }
-      }
-    }else{
-      if( hasInstLemma() ){
-        insts.push_back( getInstLemma() );
-      }else{
-        insts.push_back( qe->getInstantiation( q, terms, true ) );
-      }
-    }
-  }else{
-    for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
-      terms.push_back( it->first );
-      it->second.getInstantiations( insts, q, terms, qe, useActive, active );
-      terms.pop_back();
-    }
-  }
-}
-
-void InstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
-  if( terms.size()==q[0].getNumChildren() ){
-    if( hasInstLemma() ){
-      Node lem = getInstLemma();
-      if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){
-        quant[lem] = q;
-        tvec[lem].clear();
-        tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() );
-      }
-    }
-  }else{
-    for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
-      terms.push_back( it->first );
-      it->second.getExplanationForInstLemmas( q, terms, lems, quant, tvec );
-      terms.pop_back();
-    }
-  }
-}
-
-CDInstMatchTrie::~CDInstMatchTrie() {
-  for(std::map< Node, CDInstMatchTrie* >::iterator i = d_data.begin(),
-          iend = d_data.end(); i != iend; ++i) {
-    CDInstMatchTrie* current = (*i).second;
-    delete current;
-  }
-  d_data.clear();
-}
-
-
-bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
-                                    context::Context* c, bool modEq, int index, bool onlyExist ){
-  bool reset = false;
-  if( !d_valid.get() ){
-    if( onlyExist ){
-      return true;
-    }else{
-      d_valid.set( true );
-      reset = true;
-    }
-  }
-  if( index==(int)f[0].getNumChildren() ){
-    return reset;
-  }else{
-    Node n = m[ index ];
-    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
-    if( it!=d_data.end() ){
-      bool ret = it->second->addInstMatch( qe, f, m, c, modEq, index+1, onlyExist );
-      if( !onlyExist || !ret ){
-        return reset || ret;
-      }
-    }
-    if( modEq ){
-      //check modulo equality if any other instantiation match exists
-      if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
-        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
-                                 qe->getEqualityQuery()->getEngine() );
-        while( !eqc.isFinished() ){
-          Node en = (*eqc);
-          if( en!=n ){
-            std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
-            if( itc!=d_data.end() ){
-              if( itc->second->addInstMatch( qe, f, m, c, modEq, index+1, true ) ){
-                return false;
-              }
-            }
-          }
-          ++eqc;
-        }
-      }
-    }
-
-    if( !onlyExist ){
-      // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
-      CDInstMatchTrie* imt = new CDInstMatchTrie( c );
-      Assert(d_data.find(n) == d_data.end());
-      d_data[n] = imt;
-      imt->addInstMatch( qe, f, m, c, modEq, index+1, false );
-    }
-    return true;
-  }
-}
-
-bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index ) {
-  if( index==(int)q[0].getNumChildren() ){
-    if( d_valid.get() ){
-      d_valid.set( false );
-      return true;
-    }else{
-      return false;
-    }
-  }else{
-    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] );
-    if( it!=d_data.end() ){
-      return it->second->removeInstMatch( qe, q, m, index+1 );
-    }else{
-      return false;
-    }
-  }
-}
-
-bool CDInstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index ) {
-  if( index==(int)q[0].getNumChildren() ){
-    if( d_valid.get() ){
-      setInstLemma( lem );
-      return true;
-    }else{
-      return false;
-    }
-  }else{
-    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] );
-    if( it!=d_data.end() ){
-      return it->second->recordInstLemma( q, m, lem, index+1 );
-    }else{
-      return false;
-    }
-  }
-}
-
-void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
-  if( d_valid.get() ){
-    if( terms.size()==q[0].getNumChildren() ){
-      bool print;    
-      if( useActive ){
-        if( hasInstLemma() ){
-          Node lem = getInstLemma();
-          print = std::find( active.begin(), active.end(), lem )!=active.end();
-        }else{
-          print = false;
-        }
-      }else{
-        print = true;
-      }  
-      if( print ){ 
-        if( firstTime ){
-          out << "(instantiation " << q << std::endl;
-          firstTime = false;
-        }
-        out << "  ( ";
-        for( unsigned i=0; i<terms.size(); i++ ){
-          if( i>0 ) out << " ";
-          out << terms[i];
-        }
-        out << " )" << std::endl;
-      }
-    }else{
-      for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
-        terms.push_back( it->first );
-        it->second->print( out, q, terms, firstTime, useActive, active );
-        terms.pop_back();
-      }
-    }
-  }
-}
-
-void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const{
-  if( d_valid.get() ){
-    if( terms.size()==q[0].getNumChildren() ){
-      if( useActive ){
-        if( hasInstLemma() ){
-          Node lem = getInstLemma();
-          if( std::find( active.begin(), active.end(), lem )!=active.end() ){
-            insts.push_back( lem );
-          }
-        }
-      }else{
-        if( hasInstLemma() ){
-          insts.push_back( getInstLemma() );
-        }else{
-          insts.push_back( qe->getInstantiation( q, terms, true ) );
-        }
-      }
-    }else{
-      for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
-        terms.push_back( it->first );
-        it->second->getInstantiations( insts, q, terms, qe, useActive, active );
-        terms.pop_back();
-      }
-    }
-  }
-}
-
-
-void CDInstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
-  if( d_valid.get() ){
-    if( terms.size()==q[0].getNumChildren() ){
-      if( hasInstLemma() ){
-        Node lem;
-        if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){
-          quant[lem] = q;
-          tvec[lem].clear();
-          tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() );
-        }
-      }
-    }else{
-      for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
-        terms.push_back( it->first );
-        it->second->getExplanationForInstLemmas( q, terms, lems, quant, tvec );
-        terms.pop_back();
-      }
-    }
-  }
-}
-
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 8597755c9..ce438861c 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -17,45 +17,54 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
 
-#include <map>
+#include <vector>
 
-#include "context/cdlist.h"
-#include "context/cdo.h"
 #include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
 
-class QuantifiersEngine;
 class EqualityQuery;
 
 namespace inst {
 
-/** basic class defining an instantiation */
+/** Inst match
+ *
+ * This is the basic class specifying an instantiation. Its domain size (the
+ * size of d_vals) is the number of bound variables of the quantified formula
+ * that is passed to its constructor.
+ *
+ * The values of d_vals may be null, which indicate that the field has
+ * yet to be initialized.
+ */
 class InstMatch {
 public:
-  /* map from variable to ground terms */
-  std::vector< Node > d_vals;
-public:
   InstMatch(){}
-  explicit InstMatch( TNode f );
+  explicit InstMatch(TNode q);
   InstMatch( InstMatch* m );
-
-  /** fill all unfilled values with m */
-  bool add( InstMatch& m );
-  /** if compatible, fill all unfilled values with m and return true
-      return false otherwise */
+  /* map from variable to ground terms */
+  std::vector<Node> d_vals;
+  /** add match m
+   *
+   * This adds the initialized fields of m to this match for each field that is
+   * not already initialized in this match.
+   */
+  void add(InstMatch& m);
+  /** merge with match m
+   *
+   * This method returns true if the merge was successful, that is, all jointly
+   * initialized fields of this class and m are equivalent modulo the equalities
+   * given by q.
+   */
   bool merge( EqualityQuery* q, InstMatch& m );
-  /** debug print method */
-  void debugPrint( const char* c );
-  /** is complete? */
+  /** is this complete, i.e. are all fields non-null? */
   bool isComplete();
-  /** make representative */
-  void makeRepresentative( QuantifiersEngine* qe );
-  /** empty */
+  /** is this empty, i.e. are all fields the null node? */
   bool empty();
-  /** clear */
+  /** clear the instantiation, i.e. set all fields to the null node */
   void clear();
+  /** debug print method */
+  void debugPrint(const char* c);
   /** to stream */
   inline void toStream(std::ostream& out) const {
     out << "INST_MATCH( ";
@@ -69,166 +78,25 @@ public:
     }
     out << " )";
   }
-  /** apply rewrite */
-  void applyRewrite();
-  /** get */
-  Node get( int i );
-  void getTerms( Node f, std::vector< Node >& inst );
-  /** set */
+  /** get the i^th term in the instantiation */
+  Node get(int i) const;
+  /** append the terms of this instantiation to inst */
+  void getInst(std::vector<Node>& inst) const;
+  /** set/overwrites the i^th field in the instantiation with n */
   void setValue( int i, TNode n );
-  bool set( QuantifiersEngine* qe, int i, TNode n );
-};/* class InstMatch */
+  /** set the i^th term in the instantiation to n
+   *
+   * This method returns true if the i^th field was previously uninitialized,
+   * or is equivalent to n modulo the equalities given by q.
+   */
+  bool set(EqualityQuery* q, int i, TNode n);
+};
 
 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
   m.toStream(out);
   return out;
 }
 
-/** trie for InstMatch objects */
-class InstMatchTrie {
-public:
-  class ImtIndexOrder {
-  public:
-    std::vector< int > d_order;
-  };/* class InstMatchTrie ImtIndexOrder */
-  /** the data */
-  std::map< Node, InstMatchTrie > d_data;
-private:
-  void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
-  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
-  void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const;
-private:
-  void setInstLemma( Node n ){ 
-    d_data.clear();
-    d_data[n].clear(); 
-  }
-  bool hasInstLemma() const { return !d_data.empty(); }
-  Node getInstLemma() const { return d_data.begin()->first; }
-public:
-  InstMatchTrie(){}
-  ~InstMatchTrie(){}
-public:
-  /** return true if m exists in this trie
-        modEq is if we check modulo equality
-        modInst is if we return true if m is an instance of a match that exists
-   */
-  bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                        ImtIndexOrder* imtio = NULL, int index = 0 ) {
-    return !addInstMatch( qe, f, m, modEq, imtio, true, index );
-  }
-  bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
-                        ImtIndexOrder* imtio = NULL, int index = 0 ) {
-    return !addInstMatch( qe, f, m, modEq, imtio, true, index );
-  }
-  /** add match m for quantifier f, take into account equalities if modEq = true,
-      if imtio is non-null, this is the order to add to trie
-      return true if successful
-  */
-  bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                     ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
-    return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index );
-  }
-  bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
-                     ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
-  bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
-  bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio = NULL, int index = 0 );
-  void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
-    std::vector< TNode > terms;
-    print( out, q, terms, firstTime, useActive, active );
-  }
-  void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
-    std::vector< Node > terms;
-    getInstantiations( insts, q, terms, qe, useActive, active );
-  }
-  void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
-    std::vector< Node > terms;
-    getExplanationForInstLemmas( q, terms, lems, quant, tvec );
-  }  
-  void clear() { d_data.clear(); }
-};/* class InstMatchTrie */
-
-/** trie for InstMatch objects */
-class CDInstMatchTrie {
-private:
-  /** the data */
-  std::map< Node, CDInstMatchTrie* > d_data;
-  /** is valid */
-  context::CDO< bool > d_valid;
-private:
-  void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
-  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
-  void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const;
-private:
-  void setInstLemma( Node n ){ 
-    d_data.clear();
-    d_data[n] = NULL; 
-  }
-  bool hasInstLemma() const { return !d_data.empty(); }
-  Node getInstLemma() const { return d_data.begin()->first; }
-public:
-  CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
-  ~CDInstMatchTrie();
-
-  /** return true if m exists in this trie
-        modEq is if we check modulo equality
-        modInst is if we return true if m is an instance of a match that exists
-   */
-  bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
-                        int index = 0 ) {
-    return !addInstMatch( qe, q, m, c, modEq, index, true );
-  }
-  bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
-                        int index = 0 ) {
-    return !addInstMatch( qe, q, m, c, modEq, index, true );
-  }
-  /** add match m for quantifier f, take into account equalities if modEq = true,
-      if imtio is non-null, this is the order to add to trie
-      return true if successful
-  */
-  bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
-                     int index = 0, bool onlyExist = false ) {
-    return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist );
-  }
-  bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
-                     int index = 0, bool onlyExist = false );
-  bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
-  bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index = 0 );
-  void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
-    std::vector< TNode > terms;
-    print( out, q, terms, firstTime, useActive, active );
-  }
-  void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
-    std::vector< Node > terms;
-    getInstantiations( insts, q, terms, qe, useActive, active );
-  }
-  void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
-    std::vector< Node > terms;
-    getExplanationForInstLemmas( q, terms, lems, quant, tvec );
-  }  
-};/* class CDInstMatchTrie */
-
-
-class InstMatchTrieOrdered{
-private:
-  InstMatchTrie::ImtIndexOrder* d_imtio;
-  InstMatchTrie d_imt;
-public:
-  InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
-  ~InstMatchTrieOrdered(){}
-  /** get ordering */
-  InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
-  /** get trie */
-  InstMatchTrie* getTrie() { return &d_imt; }
-public:
-  /** add match m, return true if successful */
-  bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
-    return d_imt.addInstMatch( qe, f, m, modEq, d_imtio );
-  }
-  bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
-    return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio );
-  }
-};/* class InstMatchTrieOrdered */
-
 }/* CVC4::theory::inst namespace */
 
 typedef CVC4::theory::inst::InstMatch InstMatch;
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index a8942326c..5cdb2a64b 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -15,9 +15,10 @@
 #include "theory/quantifiers/inst_match_generator.h"
 
 #include "expr/datatype.h"
-#include "options/quantifiers_options.h"
 #include "options/datatypes_options.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/trigger.h"
@@ -238,7 +239,8 @@ int InstMatchGenerator::getMatch(
       if( d_children_types[i]==0 ){
         Trace("matching-debug2") << "Setting " << d_var_num[i] << " to " << t[i] << "..." << std::endl;
         bool addToPrev = m.get( d_var_num[i] ).isNull();
-        if( !m.set( qe, d_var_num[i], t[i] ) ){
+        if (!m.set(q, d_var_num[i], t[i]))
+        {
           //match is in conflict
           Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << t[i] << std::endl;
           success = false;
@@ -260,7 +262,8 @@ int InstMatchGenerator::getMatch(
     //for variable matching
     if( d_match_pattern.getKind()==INST_CONSTANT ){
       bool addToPrev = m.get( d_var_num[0] ).isNull();
-      if( !m.set( qe, d_var_num[0], t ) ){
+      if (!m.set(q, d_var_num[0], t))
+      {
         success = false;
       }else{
         if( addToPrev ){
@@ -296,7 +299,8 @@ int InstMatchGenerator::getMatch(
       }
       if( !t_match.isNull() ){
         bool addToPrev = m.get( v ).isNull();
-        if( !m.set( qe, v, t_match ) ){
+        if (!m.set(q, v, t_match))
+        {
           success = false;
         }else if( addToPrev ){
           prev.push_back( v );
@@ -572,7 +576,8 @@ int VarMatchGeneratorBooleanTerm::getNextMatch(Node q,
     Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern ));
     d_eq_class = Node::null();
     d_rm_prev = m.get( d_var_num[0] ).isNull();
-    if( !m.set( qe, d_var_num[0], s ) ){
+    if (!m.set(qe->getEqualityQuery(), d_var_num[0], s))
+    {
       return -1;
     }else{
       ret_val = continueNextMatch(q, m, qe, tparent);
@@ -608,7 +613,8 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q,
     d_eq_class = Node::null();
     //if( s.getType().isSubtypeOf( d_var_type ) ){
     d_rm_prev = m.get( d_var_num[0] ).isNull();
-    if( !m.set( qe, d_var_num[0], s ) ){
+    if (!m.set(qe->getEqualityQuery(), d_var_num[0], s))
+    {
       return -1;
     }else{
       ret_val = continueNextMatch(q, m, qe, tparent);
@@ -1087,7 +1093,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     // we do not need the trigger parent for simple triggers (no post-processing
     // required)
-    if (qe->addInstantiation(d_quant, m))
+    if (qe->getInstantiate()->addInstantiation(d_quant, m))
     {
       addedLemmas++;
       Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index a74035076..e36ee2b58 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -17,8 +17,8 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
 
-#include "theory/quantifiers/inst_match.h"
 #include <map>
+#include "theory/quantifiers/inst_match_trie.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
new file mode 100644
index 000000000..12844eacb
--- /dev/null
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -0,0 +1,527 @@
+/*********************                                                        */
+/*! \file inst_match.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 inst match class
+ **/
+
+#include "theory/quantifiers/inst_match_trie.h"
+
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe,
+                                 Node f,
+                                 std::vector<Node>& m,
+                                 bool modEq,
+                                 ImtIndexOrder* imtio,
+                                 bool onlyExist,
+                                 unsigned index)
+{
+  if (index == f[0].getNumChildren()
+      || (imtio && index == imtio->d_order.size()))
+  {
+    return false;
+  }
+  unsigned i_index = imtio ? imtio->d_order[index] : index;
+  Node n = m[i_index];
+  std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
+  if (it != d_data.end())
+  {
+    bool ret =
+        it->second.addInstMatch(qe, f, m, modEq, imtio, onlyExist, index + 1);
+    if (!onlyExist || !ret)
+    {
+      return ret;
+    }
+  }
+  if (modEq)
+  {
+    // check modulo equality if any other instantiation match exists
+    if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n))
+    {
+      eq::EqClassIterator eqc(
+          qe->getEqualityQuery()->getEngine()->getRepresentative(n),
+          qe->getEqualityQuery()->getEngine());
+      while (!eqc.isFinished())
+      {
+        Node en = (*eqc);
+        if (en != n)
+        {
+          std::map<Node, InstMatchTrie>::iterator itc = d_data.find(en);
+          if (itc != d_data.end())
+          {
+            if (itc->second.addInstMatch(
+                    qe, f, m, modEq, imtio, true, index + 1))
+            {
+              return false;
+            }
+          }
+        }
+        ++eqc;
+      }
+    }
+  }
+  if (!onlyExist)
+  {
+    d_data[n].addInstMatch(qe, f, m, modEq, imtio, false, index + 1);
+  }
+  return true;
+}
+
+bool InstMatchTrie::removeInstMatch(Node q,
+                                    std::vector<Node>& m,
+                                    ImtIndexOrder* imtio,
+                                    unsigned index)
+{
+  Assert(index < q[0].getNumChildren());
+  Assert(!imtio || index < imtio->d_order.size());
+  unsigned i_index = imtio ? imtio->d_order[index] : index;
+  Node n = m[i_index];
+  std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
+  if (it != d_data.end())
+  {
+    if ((index + 1) == q[0].getNumChildren()
+        || (imtio && (index + 1) == imtio->d_order.size()))
+    {
+      d_data.erase(n);
+      return true;
+    }
+    return it->second.removeInstMatch(q, m, imtio, index + 1);
+  }
+  return false;
+}
+
+bool InstMatchTrie::recordInstLemma(Node q,
+                                    std::vector<Node>& m,
+                                    Node lem,
+                                    ImtIndexOrder* imtio,
+                                    unsigned index)
+{
+  if (index == q[0].getNumChildren()
+      || (imtio && index == imtio->d_order.size()))
+  {
+    setInstLemma(lem);
+    return true;
+  }
+  unsigned i_index = imtio ? imtio->d_order[index] : index;
+  std::map<Node, InstMatchTrie>::iterator it = d_data.find(m[i_index]);
+  if (it != d_data.end())
+  {
+    return it->second.recordInstLemma(q, m, lem, imtio, index + 1);
+  }
+  return false;
+}
+
+void InstMatchTrie::print(std::ostream& out,
+                          Node q,
+                          std::vector<TNode>& terms,
+                          bool& firstTime,
+                          bool useActive,
+                          std::vector<Node>& active) const
+{
+  if (terms.size() == q[0].getNumChildren())
+  {
+    bool print;
+    if (useActive)
+    {
+      if (hasInstLemma())
+      {
+        Node lem = getInstLemma();
+        print = std::find(active.begin(), active.end(), lem) != active.end();
+      }
+      else
+      {
+        print = false;
+      }
+    }
+    else
+    {
+      print = true;
+    }
+    if (print)
+    {
+      if (firstTime)
+      {
+        out << "(instantiation " << q << std::endl;
+        firstTime = false;
+      }
+      out << "  ( ";
+      for (unsigned i = 0, size = terms.size(); i < size; i++)
+      {
+        if (i > 0)
+        {
+          out << ", ";
+        }
+        out << terms[i];
+      }
+      out << " )" << std::endl;
+    }
+  }
+  else
+  {
+    for (const std::pair<const Node, InstMatchTrie>& d : d_data)
+    {
+      terms.push_back(d.first);
+      d.second.print(out, q, terms, firstTime, useActive, active);
+      terms.pop_back();
+    }
+  }
+}
+
+void InstMatchTrie::getInstantiations(std::vector<Node>& insts,
+                                      Node q,
+                                      std::vector<Node>& terms,
+                                      QuantifiersEngine* qe,
+                                      bool useActive,
+                                      std::vector<Node>& active) const
+{
+  if (terms.size() == q[0].getNumChildren())
+  {
+    if (useActive)
+    {
+      if (hasInstLemma())
+      {
+        Node lem = getInstLemma();
+        if (std::find(active.begin(), active.end(), lem) != active.end())
+        {
+          insts.push_back(lem);
+        }
+      }
+    }
+    else
+    {
+      if (hasInstLemma())
+      {
+        insts.push_back(getInstLemma());
+      }
+      else
+      {
+        insts.push_back(qe->getInstantiate()->getInstantiation(q, terms, true));
+      }
+    }
+  }
+  else
+  {
+    for (const std::pair<const Node, InstMatchTrie>& d : d_data)
+    {
+      terms.push_back(d.first);
+      d.second.getInstantiations(insts, q, terms, qe, useActive, active);
+      terms.pop_back();
+    }
+  }
+}
+
+void InstMatchTrie::getExplanationForInstLemmas(
+    Node q,
+    std::vector<Node>& terms,
+    const std::vector<Node>& lems,
+    std::map<Node, Node>& quant,
+    std::map<Node, std::vector<Node> >& tvec) const
+{
+  if (terms.size() == q[0].getNumChildren())
+  {
+    if (hasInstLemma())
+    {
+      Node lem = getInstLemma();
+      if (std::find(lems.begin(), lems.end(), lem) != lems.end())
+      {
+        quant[lem] = q;
+        tvec[lem].clear();
+        tvec[lem].insert(tvec[lem].end(), terms.begin(), terms.end());
+      }
+    }
+  }
+  else
+  {
+    for (const std::pair<const Node, InstMatchTrie>& d : d_data)
+    {
+      terms.push_back(d.first);
+      d.second.getExplanationForInstLemmas(q, terms, lems, quant, tvec);
+      terms.pop_back();
+    }
+  }
+}
+
+CDInstMatchTrie::~CDInstMatchTrie()
+{
+  for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+  {
+    CDInstMatchTrie* current = d.second;
+    delete current;
+  }
+  d_data.clear();
+}
+
+bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe,
+                                   Node f,
+                                   std::vector<Node>& m,
+                                   context::Context* c,
+                                   bool modEq,
+                                   unsigned index,
+                                   bool onlyExist)
+{
+  bool reset = false;
+  if (!d_valid.get())
+  {
+    if (onlyExist)
+    {
+      return true;
+    }
+    else
+    {
+      d_valid.set(true);
+      reset = true;
+    }
+  }
+  if (index == f[0].getNumChildren())
+  {
+    return reset;
+  }
+  Node n = m[index];
+  std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
+  if (it != d_data.end())
+  {
+    bool ret =
+        it->second->addInstMatch(qe, f, m, c, modEq, index + 1, onlyExist);
+    if (!onlyExist || !ret)
+    {
+      return reset || ret;
+    }
+  }
+  if (modEq)
+  {
+    // check modulo equality if any other instantiation match exists
+    if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n))
+    {
+      eq::EqClassIterator eqc(
+          qe->getEqualityQuery()->getEngine()->getRepresentative(n),
+          qe->getEqualityQuery()->getEngine());
+      while (!eqc.isFinished())
+      {
+        Node en = (*eqc);
+        if (en != n)
+        {
+          std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
+          if (itc != d_data.end())
+          {
+            if (itc->second->addInstMatch(qe, f, m, c, modEq, index + 1, true))
+            {
+              return false;
+            }
+          }
+        }
+        ++eqc;
+      }
+    }
+  }
+
+  if (!onlyExist)
+  {
+    // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    CDInstMatchTrie* imt = new CDInstMatchTrie(c);
+    Assert(d_data.find(n) == d_data.end());
+    d_data[n] = imt;
+    imt->addInstMatch(qe, f, m, c, modEq, index + 1, false);
+  }
+  return true;
+}
+
+bool CDInstMatchTrie::removeInstMatch(Node q,
+                                      std::vector<Node>& m,
+                                      unsigned index)
+{
+  if (index == q[0].getNumChildren())
+  {
+    if (d_valid.get())
+    {
+      d_valid.set(false);
+      return true;
+    }
+    return false;
+  }
+  std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
+  if (it != d_data.end())
+  {
+    return it->second->removeInstMatch(q, m, index + 1);
+  }
+  return false;
+}
+
+bool CDInstMatchTrie::recordInstLemma(Node q,
+                                      std::vector<Node>& m,
+                                      Node lem,
+                                      unsigned index)
+{
+  if (index == q[0].getNumChildren())
+  {
+    if (d_valid.get())
+    {
+      setInstLemma(lem);
+      return true;
+    }
+    return false;
+  }
+  std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
+  if (it != d_data.end())
+  {
+    return it->second->recordInstLemma(q, m, lem, index + 1);
+  }
+  return false;
+}
+
+void CDInstMatchTrie::print(std::ostream& out,
+                            Node q,
+                            std::vector<TNode>& terms,
+                            bool& firstTime,
+                            bool useActive,
+                            std::vector<Node>& active) const
+{
+  if (d_valid.get())
+  {
+    if (terms.size() == q[0].getNumChildren())
+    {
+      bool print;
+      if (useActive)
+      {
+        if (hasInstLemma())
+        {
+          Node lem = getInstLemma();
+          print = std::find(active.begin(), active.end(), lem) != active.end();
+        }
+        else
+        {
+          print = false;
+        }
+      }
+      else
+      {
+        print = true;
+      }
+      if (print)
+      {
+        if (firstTime)
+        {
+          out << "(instantiation " << q << std::endl;
+          firstTime = false;
+        }
+        out << "  ( ";
+        for (unsigned i = 0; i < terms.size(); i++)
+        {
+          if (i > 0) out << " ";
+          out << terms[i];
+        }
+        out << " )" << std::endl;
+      }
+    }
+    else
+    {
+      for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+      {
+        terms.push_back(d.first);
+        d.second->print(out, q, terms, firstTime, useActive, active);
+        terms.pop_back();
+      }
+    }
+  }
+}
+
+void CDInstMatchTrie::getInstantiations(std::vector<Node>& insts,
+                                        Node q,
+                                        std::vector<Node>& terms,
+                                        QuantifiersEngine* qe,
+                                        bool useActive,
+                                        std::vector<Node>& active) const
+{
+  if (d_valid.get())
+  {
+    if (terms.size() == q[0].getNumChildren())
+    {
+      if (useActive)
+      {
+        if (hasInstLemma())
+        {
+          Node lem = getInstLemma();
+          if (std::find(active.begin(), active.end(), lem) != active.end())
+          {
+            insts.push_back(lem);
+          }
+        }
+      }
+      else
+      {
+        if (hasInstLemma())
+        {
+          insts.push_back(getInstLemma());
+        }
+        else
+        {
+          insts.push_back(
+              qe->getInstantiate()->getInstantiation(q, terms, true));
+        }
+      }
+    }
+    else
+    {
+      for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+      {
+        terms.push_back(d.first);
+        d.second->getInstantiations(insts, q, terms, qe, useActive, active);
+        terms.pop_back();
+      }
+    }
+  }
+}
+
+void CDInstMatchTrie::getExplanationForInstLemmas(
+    Node q,
+    std::vector<Node>& terms,
+    const std::vector<Node>& lems,
+    std::map<Node, Node>& quant,
+    std::map<Node, std::vector<Node> >& tvec) const
+{
+  if (d_valid.get())
+  {
+    if (terms.size() == q[0].getNumChildren())
+    {
+      if (hasInstLemma())
+      {
+        Node lem;
+        if (std::find(lems.begin(), lems.end(), lem) != lems.end())
+        {
+          quant[lem] = q;
+          tvec[lem].clear();
+          tvec[lem].insert(tvec[lem].end(), terms.begin(), terms.end());
+        }
+      }
+    }
+    else
+    {
+      for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+      {
+        terms.push_back(d.first);
+        d.second->getExplanationForInstLemmas(q, terms, lems, quant, tvec);
+        terms.pop_back();
+      }
+    }
+  }
+}
+
+} /* CVC4::theory::inst namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
new file mode 100644
index 000000000..e33bf5997
--- /dev/null
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -0,0 +1,439 @@
+/*********************                                                        */
+/*! \file inst_match.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Francois Bobot
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 inst match class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+
+#include <map>
+
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "expr/node.h"
+#include "theory/quantifiers/inst_match.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+class EqualityQuery;
+
+namespace inst {
+
+/** trie for InstMatch objects
+ *
+ * This class is used for storing instantiations of a quantified formula q.
+ * It is a trie data structure for which entries can be added and removed.
+ * This class has interfaces for adding instantiations that are either
+ * represented by std::vectors or InstMatch objects (see inst_match.h).
+ */
+class InstMatchTrie
+{
+ public:
+  /** index ordering */
+  class ImtIndexOrder
+  {
+   public:
+    std::vector<unsigned> d_order;
+  };
+
+ public:
+  InstMatchTrie() {}
+  ~InstMatchTrie() {}
+  /** exists inst match
+   *
+   * This method considers the entry given by m, starting at the given index.
+   * The domain of m is the bound variables of quantified formula q.
+   * It returns true if (the suffix) of m exists in this trie.
+   * If modEq is true, we check for duplication modulo equality the current
+   * equalities in the active equality engine of qe.
+   */
+  bool existsInstMatch(QuantifiersEngine* qe,
+                       Node q,
+                       InstMatch& m,
+                       bool modEq = false,
+                       ImtIndexOrder* imtio = NULL,
+                       unsigned index = 0)
+  {
+    return !addInstMatch(qe, q, m, modEq, imtio, true, index);
+  }
+  /** exists inst match, vector version */
+  bool existsInstMatch(QuantifiersEngine* qe,
+                       Node q,
+                       std::vector<Node>& m,
+                       bool modEq = false,
+                       ImtIndexOrder* imtio = NULL,
+                       unsigned index = 0)
+  {
+    return !addInstMatch(qe, q, m, modEq, imtio, true, index);
+  }
+  /** add inst match
+   *
+   * This method adds (the suffix of) m starting at the given index to this
+   * trie, and returns true if and only if m did not already occur in this trie.
+   * The domain of m is the bound variables of quantified formula q.
+   * If modEq is true, we check for duplication modulo equality the current
+   * equalities in the active equality engine of qe.
+   */
+  bool addInstMatch(QuantifiersEngine* qe,
+                    Node q,
+                    InstMatch& m,
+                    bool modEq = false,
+                    ImtIndexOrder* imtio = NULL,
+                    bool onlyExist = false,
+                    unsigned index = 0)
+  {
+    return addInstMatch(qe, q, m.d_vals, modEq, imtio, onlyExist, index);
+  }
+  /** add inst match, vector version */
+  bool addInstMatch(QuantifiersEngine* qe,
+                    Node f,
+                    std::vector<Node>& m,
+                    bool modEq = false,
+                    ImtIndexOrder* imtio = NULL,
+                    bool onlyExist = false,
+                    unsigned index = 0);
+  /** remove inst match
+   *
+   * This removes (the suffix of) m starting at the given index from this trie.
+   * It returns true if and only if this entry existed in this trie.
+   * The domain of m is the bound variables of quantified formula q.
+   */
+  bool removeInstMatch(Node f,
+                       std::vector<Node>& m,
+                       ImtIndexOrder* imtio = NULL,
+                       unsigned index = 0);
+  /** record instantiation lemma
+   *
+   * This records that the instantiation lemma lem corresponds to the entry
+   * given by (the suffix of) m starting at the given index.
+   */
+  bool recordInstLemma(Node q,
+                       std::vector<Node>& m,
+                       Node lem,
+                       ImtIndexOrder* imtio = NULL,
+                       unsigned index = 0);
+
+  /** get instantiations
+   *
+   * This gets the set of instantiation lemmas that were recorded in this trie
+   * via calls to recordInstLemma. If useActive is true, we only add
+   * instantiations that occur in active.
+   */
+  void getInstantiations(std::vector<Node>& insts,
+                         Node q,
+                         QuantifiersEngine* qe,
+                         bool useActive,
+                         std::vector<Node>& active)
+  {
+    std::vector<Node> terms;
+    getInstantiations(insts, q, terms, qe, useActive, active);
+  }
+  /** get explanation for inst lemmas
+   *
+   * This gets the explanation for the instantiation lemmas in lems for
+   * quantified formula q, for which this trie stores instantiation matches for.
+   * For each instantiation lemma lem recording in this trie via calls to
+   * recordInstLemma, we map lem to q in map quant, and lem to its corresponding
+   * vector of terms in tvec.
+   */
+  void getExplanationForInstLemmas(
+      Node q,
+      const std::vector<Node>& lems,
+      std::map<Node, Node>& quant,
+      std::map<Node, std::vector<Node> >& tvec) const
+  {
+    std::vector<Node> terms;
+    getExplanationForInstLemmas(q, terms, lems, quant, tvec);
+  }
+
+  /** clear the data of this class */
+  void clear() { d_data.clear(); }
+  /** print this class */
+  void print(std::ostream& out,
+             Node q,
+             bool& firstTime,
+             bool useActive,
+             std::vector<Node>& active) const
+  {
+    std::vector<TNode> terms;
+    print(out, q, terms, firstTime, useActive, active);
+  }
+  /** the data */
+  std::map<Node, InstMatchTrie> d_data;
+
+ private:
+  /** helper for print
+   * terms accumulates the path we are on in the trie.
+   */
+  void print(std::ostream& out,
+             Node q,
+             std::vector<TNode>& terms,
+             bool& firstTime,
+             bool useActive,
+             std::vector<Node>& active) const;
+  /** helper for get instantiations
+   * terms accumulates the path we are on in the trie.
+   */
+  void getInstantiations(std::vector<Node>& insts,
+                         Node q,
+                         std::vector<Node>& terms,
+                         QuantifiersEngine* qe,
+                         bool useActive,
+                         std::vector<Node>& active) const;
+  /** helper for get explantaion for inst lemmas
+   * terms accumulates the path we are on in the trie.
+   */
+  void getExplanationForInstLemmas(
+      Node q,
+      std::vector<Node>& terms,
+      const std::vector<Node>& lems,
+      std::map<Node, Node>& quant,
+      std::map<Node, std::vector<Node> >& tvec) const;
+  /** set instantiation lemma at this node in the trie */
+  void setInstLemma(Node n)
+  {
+    d_data.clear();
+    d_data[n].clear();
+  }
+  /** does this node of the trie store an instantiation lemma? */
+  bool hasInstLemma() const { return !d_data.empty(); }
+  /** get the instantiation lemma stored in this node of the trie */
+  Node getInstLemma() const { return d_data.begin()->first; }
+};
+
+/** trie for InstMatch objects
+ *
+ * This is a context-dependent version of the above class.
+ */
+class CDInstMatchTrie
+{
+ public:
+  CDInstMatchTrie(context::Context* c) : d_valid(c, false) {}
+  ~CDInstMatchTrie();
+
+  /** exists inst match
+   *
+   * This method considers the entry given by m, starting at the given index.
+   * The domain of m is the bound variables of quantified formula q.
+   * It returns true if (the suffix) of m exists in this trie.
+   * If modEq is true, we check for duplication modulo equality the current
+   * equalities in the active equality engine of qe.
+   * It additionally takes a context c, for which the entry is valid in.
+   */
+  bool existsInstMatch(QuantifiersEngine* qe,
+                       Node q,
+                       InstMatch& m,
+                       context::Context* c,
+                       bool modEq = false,
+                       unsigned index = 0)
+  {
+    return !addInstMatch(qe, q, m, c, modEq, index, true);
+  }
+  /** exists inst match, vector version */
+  bool existsInstMatch(QuantifiersEngine* qe,
+                       Node q,
+                       std::vector<Node>& m,
+                       context::Context* c,
+                       bool modEq = false,
+                       unsigned index = 0)
+  {
+    return !addInstMatch(qe, q, m, c, modEq, index, true);
+  }
+  /** add inst match
+   *
+   * This method adds (the suffix of) m starting at the given index to this
+   * trie, and returns true if and only if m did not already occur in this trie.
+   * The domain of m is the bound variables of quantified formula q.
+   * If modEq is true, we check for duplication modulo equality the current
+   * equalities in the active equality engine of qe.
+   * It additionally takes a context c, for which the entry is valid in.
+   */
+  bool addInstMatch(QuantifiersEngine* qe,
+                    Node q,
+                    InstMatch& m,
+                    context::Context* c,
+                    bool modEq = false,
+                    unsigned index = 0,
+                    bool onlyExist = false)
+  {
+    return addInstMatch(qe, q, m.d_vals, c, modEq, index, onlyExist);
+  }
+  /** add inst match, vector version */
+  bool addInstMatch(QuantifiersEngine* qe,
+                    Node q,
+                    std::vector<Node>& m,
+                    context::Context* c,
+                    bool modEq = false,
+                    unsigned index = 0,
+                    bool onlyExist = false);
+  /** remove inst match
+   *
+   * This removes (the suffix of) m starting at the given index from this trie.
+   * It returns true if and only if this entry existed in this trie.
+   * The domain of m is the bound variables of quantified formula q.
+   */
+  bool removeInstMatch(Node q, std::vector<Node>& m, unsigned index = 0);
+  /** record instantiation lemma
+   *
+   * This records that the instantiation lemma lem corresponds to the entry
+   * given by (the suffix of) m starting at the given index.
+   */
+  bool recordInstLemma(Node q,
+                       std::vector<Node>& m,
+                       Node lem,
+                       unsigned index = 0);
+
+  /** get instantiations
+   *
+   * This gets the set of instantiation lemmas that were recorded in this class
+   * via calls to recordInstLemma. If useActive is true, we only add
+   * instantiations that occur in active.
+   */
+  void getInstantiations(std::vector<Node>& insts,
+                         Node q,
+                         QuantifiersEngine* qe,
+                         bool useActive,
+                         std::vector<Node>& active)
+  {
+    std::vector<Node> terms;
+    getInstantiations(insts, q, terms, qe, useActive, active);
+  }
+  /** get explanation for inst lemmas
+   *
+   * This gets the explanation for the instantiation lemmas in lems for
+   * quantified formula q, for which this trie stores instantiation matches for.
+   * For each instantiation lemma lem recording in this trie via calls to
+   * recordInstLemma, we map lem to q in map quant, and lem to its corresponding
+   * vector of terms in tvec.
+   */
+  void getExplanationForInstLemmas(
+      Node q,
+      const std::vector<Node>& lems,
+      std::map<Node, Node>& quant,
+      std::map<Node, std::vector<Node> >& tvec) const
+  {
+    std::vector<Node> terms;
+    getExplanationForInstLemmas(q, terms, lems, quant, tvec);
+  }
+
+  /** print this class */
+  void print(std::ostream& out,
+             Node q,
+             bool& firstTime,
+             bool useActive,
+             std::vector<Node>& active) const
+  {
+    std::vector<TNode> terms;
+    print(out, q, terms, firstTime, useActive, active);
+  }
+
+ private:
+  /** the data */
+  std::map<Node, CDInstMatchTrie*> d_data;
+  /** is valid */
+  context::CDO<bool> d_valid;
+  /** helper for print
+   * terms accumulates the path we are on in the trie.
+   */
+  void print(std::ostream& out,
+             Node q,
+             std::vector<TNode>& terms,
+             bool& firstTime,
+             bool useActive,
+             std::vector<Node>& active) const;
+  /** helper for get instantiations
+   * terms accumulates the path we are on in the trie.
+   */
+  void getInstantiations(std::vector<Node>& insts,
+                         Node q,
+                         std::vector<Node>& terms,
+                         QuantifiersEngine* qe,
+                         bool useActive,
+                         std::vector<Node>& active) const;
+  /** helper for get explanation for inst lemma
+   * terms accumulates the path we are on in the trie.
+   */
+  void getExplanationForInstLemmas(
+      Node q,
+      std::vector<Node>& terms,
+      const std::vector<Node>& lems,
+      std::map<Node, Node>& quant,
+      std::map<Node, std::vector<Node> >& tvec) const;
+  /** set instantiation lemma at this node in the trie */
+  void setInstLemma(Node n)
+  {
+    d_data.clear();
+    d_data[n] = NULL;
+  }
+  /** does this node of the trie store an instantiation lemma? */
+  bool hasInstLemma() const { return !d_data.empty(); }
+  /** get the instantiation lemma stored in this node of the trie */
+  Node getInstLemma() const { return d_data.begin()->first; }
+};
+
+/** inst match trie ordered
+ *
+ * This is an ordered version of the context-independent instantiation match
+ * trie. It stores a variable order and a base InstMatchTrie.
+ */
+class InstMatchTrieOrdered
+{
+ public:
+  InstMatchTrieOrdered(InstMatchTrie::ImtIndexOrder* imtio) : d_imtio(imtio) {}
+  ~InstMatchTrieOrdered() {}
+  /** get the ordering */
+  InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
+  /** get the trie data */
+  InstMatchTrie* getTrie() { return &d_imt; }
+  /** add match m for quantified formula q
+   *
+   * This method returns true if the match m was not previously added to this
+   * class. If modEq is true, we consider duplicates modulo the current
+   * equalities stored in the active equality engine of quantifiers engine.
+   */
+  bool addInstMatch(QuantifiersEngine* qe,
+                    Node q,
+                    InstMatch& m,
+                    bool modEq = false)
+  {
+    return d_imt.addInstMatch(qe, q, m, modEq, d_imtio);
+  }
+  /** returns true if this trie contains m
+   *
+   * This method returns true if the match m exists in this
+   * class. If modEq is true, we consider duplicates modulo the current
+   * equalities stored in the active equality engine of quantifiers engine.
+   */
+  bool existsInstMatch(QuantifiersEngine* qe,
+                       Node q,
+                       InstMatch& m,
+                       bool modEq = false)
+  {
+    return d_imt.existsInstMatch(qe, q, m, modEq, d_imtio);
+  }
+
+ private:
+  /** the ordering */
+  InstMatchTrie::ImtIndexOrder* d_imtio;
+  /** the data of this class */
+  InstMatchTrie d_imt;
+};
+
+} /* CVC4::theory::inst namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 3c351cad5..f97413026 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -15,8 +15,9 @@
 #include <vector>
 
 #include "theory/quantifiers/inst_propagator.h"
-#include "theory/rewriter.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4;
 using namespace std;
@@ -670,7 +671,9 @@ void InstPropagator::filterInstantiations() {
     for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
       if( !it->second.d_q.isNull() ){
         if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
-          if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
+          if (!d_qe->getInstantiate()->removeInstantiation(
+                  it->second.d_q, it->second.d_lem, it->second.d_terms))
+          {
             Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
             Assert( false );
           }else{
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index b8ea2c49e..7f485750a 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -18,13 +18,14 @@
 #define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
 
 #include <iostream>
+#include <map>
 #include <string>
 #include <vector>
-#include <map>
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 24a9f1bdf..668593842 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_epr.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
@@ -728,12 +729,15 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){
     d_cbqi_set_quant_inactive = true;
     d_incomplete_check = true;
-    d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
+    d_quantEngine->getInstantiate()->recordInstantiation(
+        d_curr_quant, subs, false, false);
     return true;
   }else{
     //check if we need virtual term substitution (if used delta or infinity)
     bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false );
-    if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
+    if (d_quantEngine->getInstantiate()->addInstantiation(
+            d_curr_quant, subs, false, false, used_vts))
+    {
       ++(d_quantEngine->d_statistics.d_instantiations_cbqi);
       //d_added_inst.insert( d_curr_quant );
       return true;
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index edd15fa2c..54689b32a 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/inst_strategy_enumerative.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
@@ -273,7 +274,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort)
                                        << std::endl;
                 }
               }
-              if (d_quantEngine->addInstantiation(f, terms))
+              if (d_quantEngine->getInstantiate()->addInstantiation(f, terms))
               {
                 Trace("inst-alg-rd") << "Success!" << std::endl;
                 ++(d_quantEngine->d_statistics.d_instantiations_guess);
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
new file mode 100644
index 000000000..e04217b16
--- /dev/null
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -0,0 +1,821 @@
+/*********************                                                        */
+/*! \file instantiate.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 instantiate
+ **/
+
+#include "theory/quantifiers/instantiate.h"
+
+#include "options/quantifiers_options.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Instantiate::Instantiate(QuantifiersEngine* qe, context::UserContext* u)
+    : d_qe(qe),
+      d_term_db(nullptr),
+      d_term_util(nullptr),
+      d_total_inst_count_debug(0),
+      d_c_inst_match_trie_dom(u)
+{
+}
+
+Instantiate::~Instantiate()
+{
+  for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+  {
+    delete t.second;
+  }
+  d_c_inst_match_trie.clear();
+}
+
+bool Instantiate::reset(Theory::Effort e)
+{
+  if (!d_recorded_inst.empty())
+  {
+    Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size()
+                                << " instantiations..." << std::endl;
+    // remove explicitly recorded instantiations
+    for (std::pair<Node, std::vector<Node> >& r : d_recorded_inst)
+    {
+      removeInstantiationInternal(r.first, r.second);
+    }
+    d_recorded_inst.clear();
+  }
+  d_term_db = d_qe->getTermDatabase();
+  d_term_util = d_qe->getTermUtil();
+  return true;
+}
+
+void Instantiate::registerQuantifier(Node q) {}
+bool Instantiate::checkComplete()
+{
+  if (!d_recorded_inst.empty())
+  {
+    Trace("quant-engine-debug")
+        << "Set incomplete due to recorded instantiations." << std::endl;
+    return false;
+  }
+  return true;
+}
+
+void Instantiate::addNotify(InstantiationNotify* in)
+{
+  d_inst_notify.push_back(in);
+}
+
+void Instantiate::notifyFlushLemmas()
+{
+  for (InstantiationNotify*& in : d_inst_notify)
+  {
+    in->filterInstantiations();
+  }
+}
+
+bool Instantiate::addInstantiation(
+    Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts)
+{
+  Assert(q[0].getNumChildren() == m.d_vals.size());
+  return addInstantiation(q, m.d_vals, mkRep, modEq, doVts);
+}
+
+bool Instantiate::addInstantiation(
+    Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
+{
+  // For resource-limiting (also does a time check).
+  d_qe->getOutputChannel().safePoint(options::quantifierStep());
+  Assert(!d_qe->inConflict());
+  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++)
+  {
+    Trace("inst-add-debug") << "  " << q[0][i];
+    Trace("inst-add-debug2") << " -> " << terms[i];
+    TypeNode tn = q[0][i].getType();
+    if (terms[i].isNull())
+    {
+      terms[i] = getTermForType(tn);
+    }
+    if (mkRep)
+    {
+      // pick the best possible representative for instantiation, based on past
+      // use and simplicity of term
+      terms[i] = d_qe->getInternalRepresentative(terms[i], q, i);
+    }
+    else
+    {
+      // ensure the type is correct
+      terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn);
+    }
+    Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
+    if (terms[i].isNull())
+    {
+      Trace("inst-add-debug")
+          << " --> Failed to make term vector, due to term/type restrictions."
+          << std::endl;
+      return false;
+    }
+#ifdef CVC4_ASSERTIONS
+    bool bad_inst = false;
+    if (quantifiers::TermUtil::containsUninterpretedConstant(terms[i]))
+    {
+      Trace("inst") << "***& inst contains uninterpreted constant : "
+                    << terms[i] << std::endl;
+      bad_inst = true;
+    }
+    else if (!terms[i].getType().isSubtypeOf(q[0][i].getType()))
+    {
+      Trace("inst") << "***& inst bad type : " << terms[i] << " "
+                    << terms[i].getType() << "/" << q[0][i].getType()
+                    << std::endl;
+      bad_inst = true;
+    }
+    else if (options::cbqi())
+    {
+      Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
+      if (!icf.isNull())
+      {
+        if (icf == q)
+        {
+          Trace("inst") << "***& inst contains inst constant attr : "
+                        << terms[i] << std::endl;
+          bad_inst = true;
+        }
+        else if (quantifiers::TermUtil::containsTerms(
+                     terms[i], d_term_util->d_inst_constants[q]))
+        {
+          Trace("inst") << "***& inst contains inst constants : " << terms[i]
+                        << std::endl;
+          bad_inst = true;
+        }
+      }
+    }
+    // this assertion is critical to soundness
+    if (bad_inst)
+    {
+      Trace("inst") << "***& Bad Instantiate " << q << " with " << std::endl;
+      for (unsigned j = 0; j < terms.size(); j++)
+      {
+        Trace("inst") << "   " << terms[j] << std::endl;
+      }
+      Assert(false);
+    }
+#endif
+  }
+
+  // Note we check for entailment before checking for term vector duplication.
+  // Although checking for term vector duplication is a faster check, it is
+  // included automatically with recordInstantiationInternal, hence we prefer
+  // two checks instead of three. In experiments, it is 1% slower or so to call
+  // existsInstantiation here.
+  // Alternatively, we could return an (index, trie node) in the call to
+  // existsInstantiation here, where this would return the node in the trie
+  // where we determined that there is definitely no duplication, and then
+  // continue from that point in recordInstantiation below. However, for
+  // simplicity, we do not pursue this option (as it would likely only
+  // lead to very small gains).
+
+  // check for positive entailment
+  if (options::instNoEntail())
+  {
+    // should check consistency of equality engine
+    // (if not aborting on utility's reset)
+    std::map<TNode, TNode> subs;
+    for (unsigned i = 0, size = terms.size(); i < size; i++)
+    {
+      subs[q[0][i]] = terms[i];
+    }
+    if (d_term_db->isEntailed(q[1], subs, false, true))
+    {
+      Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
+      ++(d_statistics.d_inst_duplicate_ent);
+      return false;
+    }
+  }
+
+  // check based on instantiation level
+  if (options::instMaxLevel() != -1 || options::lteRestrictInstClosure())
+  {
+    for (Node& t : terms)
+    {
+      if (!d_term_db->isTermEligibleForInstantiation(t, q, true))
+      {
+        return false;
+      }
+    }
+  }
+
+  // record the instantiation
+  bool recorded = recordInstantiationInternal(q, terms, modEq);
+  if (!recorded)
+  {
+    Trace("inst-add-debug") << " --> Already exists (no record)." << std::endl;
+    ++(d_statistics.d_inst_duplicate_eq);
+    return false;
+  }
+
+  // construct the instantiation
+  Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
+  Assert(d_term_util->d_vars[q].size() == terms.size());
+  // get the instantiation
+  Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
+  Node orig_body = body;
+  if (options::cbqiNestedQE())
+  {
+    InstStrategyCbqi* icbqi = d_qe->getInstStrategyCbqi();
+    if (icbqi)
+    {
+      body = icbqi->doNestedQE(q, terms, body, doVts);
+    }
+  }
+  body = quantifiers::QuantifiersRewriter::preprocess(body, true);
+  Trace("inst-debug") << "...preprocess to " << body << std::endl;
+
+  // construct the lemma
+  Trace("inst-assert") << "(assert " << body << ")" << std::endl;
+
+  if (d_qe->usingModelEqualityEngine() && options::instNoModelTrue())
+  {
+    Node val_body = d_qe->getModel()->getValue(body);
+    if (val_body.isConst() && val_body.getConst<bool>())
+    {
+      Trace("inst-add-debug") << " --> True in model." << std::endl;
+      ++(d_statistics.d_inst_duplicate_model_true);
+      return false;
+    }
+  }
+
+  Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body);
+
+  // get relevancy conditions
+  if (options::instRelevantCond())
+  {
+    std::vector<Node> rlv_cond;
+    for (Node& t : terms)
+    {
+      quantifiers::TermUtil::getRelevancyCondition(t, rlv_cond);
+    }
+    if (!rlv_cond.empty())
+    {
+      rlv_cond.push_back(lem);
+      lem = NodeManager::currentNM()->mkNode(kind::OR, rlv_cond);
+    }
+  }
+
+  lem = Rewriter::rewrite(lem);
+
+  // check for lemma duplication
+  if (!d_qe->addLemma(lem, true, false))
+  {
+    Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
+    ++(d_statistics.d_inst_duplicate);
+    return false;
+  }
+
+  d_total_inst_debug[q]++;
+  d_temp_inst_debug[q]++;
+  d_total_inst_count_debug++;
+  if (Trace.isOn("inst"))
+  {
+    Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
+    for (unsigned i = 0, size = terms.size(); i < size; i++)
+    {
+      if (Trace.isOn("inst"))
+      {
+        Trace("inst") << "   " << terms[i];
+        if (Trace.isOn("inst-debug"))
+        {
+          Trace("inst-debug") << ", type=" << terms[i].getType()
+                              << ", var_type=" << q[0][i].getType();
+        }
+        Trace("inst") << std::endl;
+      }
+    }
+  }
+  if (options::instMaxLevel() != -1)
+  {
+    if (doVts)
+    {
+      // virtual term substitution/instantiation level features are
+      // incompatible
+      Assert(false);
+    }
+    else
+    {
+      uint64_t maxInstLevel = 0;
+      for (const Node& tc : terms)
+      {
+        if (tc.hasAttribute(InstLevelAttribute())
+            && tc.getAttribute(InstLevelAttribute()) > maxInstLevel)
+        {
+          maxInstLevel = tc.getAttribute(InstLevelAttribute());
+        }
+      }
+      QuantAttributes::setInstantiationLevelAttr(
+          orig_body, q[1], maxInstLevel + 1);
+    }
+  }
+  QuantifiersModule::QEffort elevel = d_qe->getCurrentQEffort();
+  if (elevel > QuantifiersModule::QEFFORT_CONFLICT
+      && elevel < QuantifiersModule::QEFFORT_NONE
+      && !d_inst_notify.empty())
+  {
+    // notify listeners
+    for (InstantiationNotify*& in : d_inst_notify)
+    {
+      if (!in->notifyInstantiation(elevel, q, lem, terms, body))
+      {
+        Trace("inst-add-debug") << "...we are in conflict." << std::endl;
+        d_qe->setConflict();
+        Assert(d_qe->getNumLemmasWaiting() > 0);
+        break;
+      }
+    }
+  }
+  if (options::trackInstLemmas())
+  {
+    bool recorded;
+    if (options::incrementalSolving())
+    {
+      recorded = d_c_inst_match_trie[q]->recordInstLemma(q, terms, lem);
+    }
+    else
+    {
+      recorded = d_inst_match_trie[q].recordInstLemma(q, terms, lem);
+    }
+    Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl;
+    Assert(recorded);
+  }
+  Trace("inst-add-debug") << " --> Success." << std::endl;
+  ++(d_statistics.d_instantiations);
+  return true;
+}
+
+bool Instantiate::removeInstantiation(Node q,
+                                      Node lem,
+                                      std::vector<Node>& terms)
+{
+  // lem must occur in d_waiting_lemmas
+  if (d_qe->removeLemma(lem))
+  {
+    return removeInstantiationInternal(q, terms);
+  }
+  return false;
+}
+
+bool Instantiate::recordInstantiation(Node q,
+                                      std::vector<Node>& terms,
+                                      bool modEq,
+                                      bool addedLem)
+{
+  return recordInstantiationInternal(q, terms, modEq, addedLem);
+}
+
+bool Instantiate::existsInstantiation(Node q,
+                                      std::vector<Node>& terms,
+                                      bool modEq)
+{
+  if (options::incrementalSolving())
+  {
+    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+        d_c_inst_match_trie.find(q);
+    if (it != d_c_inst_match_trie.end())
+    {
+      return it->second->existsInstMatch(
+          d_qe, q, terms, d_qe->getUserContext(), modEq);
+    }
+  }
+  else
+  {
+    std::map<Node, inst::InstMatchTrie>::iterator it =
+        d_inst_match_trie.find(q);
+    if (it != d_inst_match_trie.end())
+    {
+      return it->second.existsInstMatch(d_qe, q, terms, modEq);
+    }
+  }
+  return false;
+}
+
+Node Instantiate::getInstantiation(Node q,
+                                   std::vector<Node>& vars,
+                                   std::vector<Node>& terms,
+                                   bool doVts)
+{
+  Node body;
+  Assert(vars.size() == terms.size());
+  Assert(q[0].getNumChildren() == vars.size());
+  // TODO (#1386) : optimize this
+  body = q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
+  if (doVts)
+  {
+    // do virtual term substitution
+    body = Rewriter::rewrite(body);
+    Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
+    Node body_r = d_term_util->rewriteVtsSymbols(body);
+    Trace("quant-vts-debug") << "            ...result: " << body_r
+                             << std::endl;
+    body = body_r;
+  }
+  return body;
+}
+
+Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts)
+{
+  Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end());
+  Assert(m.d_vals.size() == q[0].getNumChildren());
+  return getInstantiation(q, d_term_util->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);
+}
+
+bool Instantiate::recordInstantiationInternal(Node q,
+                                              std::vector<Node>& terms,
+                                              bool modEq,
+                                              bool addedLem)
+{
+  if (!addedLem)
+  {
+    // record the instantiation for deletion later
+    d_recorded_inst.push_back(std::pair<Node, std::vector<Node> >(q, terms));
+  }
+  if (options::incrementalSolving())
+  {
+    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);
+    if (it != d_c_inst_match_trie.end())
+    {
+      imt = it->second;
+    }
+    else
+    {
+      imt = new inst::CDInstMatchTrie(d_qe->getUserContext());
+      d_c_inst_match_trie[q] = imt;
+    }
+    d_c_inst_match_trie_dom.insert(q);
+    return imt->addInstMatch(d_qe, q, terms, d_qe->getUserContext(), modEq);
+  }
+  Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+  return d_inst_match_trie[q].addInstMatch(d_qe, q, terms, modEq);
+}
+
+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);
+    if (it != d_c_inst_match_trie.end())
+    {
+      return it->second->removeInstMatch(q, terms);
+    }
+    return false;
+  }
+  return d_inst_match_trie[q].removeInstMatch(q, terms);
+}
+
+Node Instantiate::getTermForType(TypeNode tn)
+{
+  if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+  {
+    return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
+  }
+  return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
+}
+
+bool Instantiate::printInstantiations(std::ostream& out)
+{
+  bool useUnsatCore = false;
+  std::vector<Node> active_lemmas;
+  if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas))
+  {
+    useUnsatCore = true;
+  }
+  bool printed = false;
+  if (options::incrementalSolving())
+  {
+    for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+    {
+      bool firstTime = true;
+      t.second->print(out, t.first, firstTime, useUnsatCore, active_lemmas);
+      if (!firstTime)
+      {
+        out << ")" << std::endl;
+      }
+      printed = printed || !firstTime;
+    }
+  }
+  else
+  {
+    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    {
+      bool firstTime = true;
+      t.second.print(out, t.first, firstTime, useUnsatCore, active_lemmas);
+      if (!firstTime)
+      {
+        out << ")" << std::endl;
+      }
+      printed = printed || !firstTime;
+    }
+  }
+  return printed;
+}
+
+void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+{
+  if (options::incrementalSolving())
+  {
+    for (context::CDHashSet<Node, NodeHashFunction>::const_iterator it =
+             d_c_inst_match_trie_dom.begin();
+         it != d_c_inst_match_trie_dom.end();
+         ++it)
+    {
+      qs.push_back(*it);
+    }
+  }
+  else
+  {
+    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    {
+      qs.push_back(t.first);
+    }
+  }
+}
+
+bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
+{
+  // only if unsat core available
+  if (options::proof())
+  {
+    if (!ProofManager::currentPM()->unsatCoreAvailable())
+    {
+      return false;
+    }
+  }
+
+  Trace("inst-unsat-core") << "Get instantiations in unsat core..."
+                           << std::endl;
+  ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS,
+                                                  active_lemmas);
+  if (Trace.isOn("inst-unsat-core"))
+  {
+    Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: "
+                             << std::endl;
+    for (const Node& lem : active_lemmas)
+    {
+      Trace("inst-unsat-core") << "  " << lem << std::endl;
+    }
+    Trace("inst-unsat-core") << std::endl;
+  }
+  return true;
+}
+
+bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
+                                     std::map<Node, Node>& weak_imp)
+{
+  if (getUnsatCoreLemmas(active_lemmas))
+  {
+    for (unsigned i = 0, size = active_lemmas.size(); i < size; ++i)
+    {
+      Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(
+          active_lemmas[i]);
+      if (n != active_lemmas[i])
+      {
+        Trace("inst-unsat-core") << "  weaken : " << active_lemmas[i] << " -> "
+                                 << n << std::endl;
+      }
+      weak_imp[active_lemmas[i]] = n;
+    }
+    return true;
+  }
+  return false;
+}
+
+void Instantiate::getInstantiationTermVectors(
+    Node q, std::vector<std::vector<Node> >& tvecs)
+{
+  std::vector<Node> lemmas;
+  getInstantiations(q, lemmas);
+  std::map<Node, Node> quant;
+  std::map<Node, std::vector<Node> > tvec;
+  getExplanationForInstLemmas(lemmas, quant, tvec);
+  for (std::pair<const Node, std::vector<Node> >& t : tvec)
+  {
+    tvecs.push_back(t.second);
+  }
+}
+
+void Instantiate::getInstantiationTermVectors(
+    std::map<Node, std::vector<std::vector<Node> > >& insts)
+{
+  if (options::incrementalSolving())
+  {
+    for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+    {
+      getInstantiationTermVectors(t.first, insts[t.first]);
+    }
+  }
+  else
+  {
+    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    {
+      getInstantiationTermVectors(t.first, insts[t.first]);
+    }
+  }
+}
+
+void Instantiate::getExplanationForInstLemmas(
+    const std::vector<Node>& lems,
+    std::map<Node, Node>& quant,
+    std::map<Node, std::vector<Node> >& tvec)
+{
+  if (options::trackInstLemmas())
+  {
+    if (options::incrementalSolving())
+    {
+      for (std::pair<const Node, inst::CDInstMatchTrie*>& t :
+           d_c_inst_match_trie)
+      {
+        t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec);
+      }
+    }
+    else
+    {
+      for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+      {
+        t.second.getExplanationForInstLemmas(t.first, lems, quant, tvec);
+      }
+    }
+#ifdef CVC4_ASSERTIONS
+    for (unsigned j = 0; j < lems.size(); j++)
+    {
+      Assert(quant.find(lems[j]) != quant.end());
+      Assert(tvec.find(lems[j]) != tvec.end());
+    }
+#endif
+  }
+  Assert(false);
+}
+
+void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts)
+{
+  bool useUnsatCore = false;
+  std::vector<Node> active_lemmas;
+  if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas))
+  {
+    useUnsatCore = true;
+  }
+
+  if (options::incrementalSolving())
+  {
+    for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+    {
+      t.second->getInstantiations(
+          insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas);
+    }
+  }
+  else
+  {
+    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    {
+      t.second.getInstantiations(
+          insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas);
+    }
+  }
+}
+
+void Instantiate::getInstantiations(Node q, std::vector<Node>& insts)
+{
+  if (options::incrementalSolving())
+  {
+    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+        d_c_inst_match_trie.find(q);
+    if (it != d_c_inst_match_trie.end())
+    {
+      std::vector<Node> active_lemmas;
+      it->second->getInstantiations(
+          insts, it->first, d_qe, false, active_lemmas);
+    }
+  }
+  else
+  {
+    std::map<Node, inst::InstMatchTrie>::iterator it =
+        d_inst_match_trie.find(q);
+    if (it != d_inst_match_trie.end())
+    {
+      std::vector<Node> active_lemmas;
+      it->second.getInstantiations(
+          insts, it->first, d_qe, false, active_lemmas);
+    }
+  }
+}
+
+Node Instantiate::getInstantiatedConjunction(Node q)
+{
+  Assert(q.getKind() == FORALL);
+  std::vector<Node> insts;
+  getInstantiations(q, insts);
+  if (insts.empty())
+  {
+    return NodeManager::currentNM()->mkConst(true);
+  }
+  Node ret;
+  if (insts.size() == 1)
+  {
+    ret = insts[0];
+  }
+  else
+  {
+    ret = NodeManager::currentNM()->mkNode(kind::AND, insts);
+  }
+  // have to remove q
+  // may want to do this in a better way
+  TNode tq = q;
+  TNode tt = NodeManager::currentNM()->mkConst(true);
+  ret = ret.substitute(tq, tt);
+  return ret;
+}
+
+void Instantiate::debugPrint()
+{
+  // debug information
+  if (Trace.isOn("inst-per-quant-round"))
+  {
+    for (std::pair<const Node, int>& i : d_temp_inst_debug)
+    {
+      Trace("inst-per-quant-round") << " * " << i.second << " for " << i.first
+                                    << std::endl;
+      d_temp_inst_debug[i.first] = 0;
+    }
+  }
+}
+
+void Instantiate::debugPrintModel()
+{
+  if (Trace.isOn("inst-per-quant"))
+  {
+    for (std::pair<const Node, int>& i : d_total_inst_debug)
+    {
+      Trace("inst-per-quant") << " * " << i.second << " for " << i.first
+                              << std::endl;
+    }
+  }
+}
+
+Instantiate::Statistics::Statistics()
+    : d_instantiations("Instantiate::Instantiations_Total", 0),
+      d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
+      d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0),
+      d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0),
+      d_inst_duplicate_model_true("Instantiate::Duplicate_Inst_Model_True", 0)
+{
+  smtStatisticsRegistry()->registerStat(&d_instantiations);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true);
+}
+
+Instantiate::Statistics::~Statistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_instantiations);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true);
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
new file mode 100644
index 000000000..d1973eadb
--- /dev/null
+++ b/src/theory/quantifiers/instantiate.h
@@ -0,0 +1,377 @@
+/*********************                                                        */
+/*! \file instantiate.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 instantiate
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "theory/quantifiers/inst_match_trie.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers_engine.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermDb;
+class TermUtil;
+
+/** instantiation notify
+ *
+ * This class is a listener for all instantiations generated with quantifiers.
+ * By default, no notify classes are used. For an example of an instantiation
+ * notify class, see quantifiers/inst_propagate.h, which has a notify class
+ * that recognizes when the set of enqueued instantiations form a conflict.
+ */
+class InstantiationNotify
+{
+ public:
+  InstantiationNotify() {}
+  virtual ~InstantiationNotify() {}
+  /** notify instantiation
+   *
+   * This is called when an instantiation of quantified formula q is
+   * instantiated by a substitution whose range is terms at quantifier effort
+   * quant_e. Furthermore:
+   *   body is the substituted, preprocessed body of the quantified formula,
+   *   lem is the instantiation lemma ( ~q V body ) after rewriting.
+   */
+  virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+                                   Node q,
+                                   Node lem,
+                                   std::vector<Node>& terms,
+                                   Node body) = 0;
+  /** filter instantiations
+   *
+   * This is called just before the quantifiers engine flushes its lemmas to the
+   * output channel. During this call, the instantiation notify object may
+   * call, e.g. QuantifiersEngine::getInstantiate()->removeInstantiation
+   * to remove instantiations that should not be sent on the output channel.
+   */
+  virtual void filterInstantiations() = 0;
+};
+
+/** Instantiate
+ *
+ * This class is used for generating instantiation lemmas.  It maintains an
+ * instantiation trie, which is represented by a different data structure
+ * depending on whether incremental solving is enabled (see d_inst_match_trie
+ * and d_c_inst_match_trie).
+ *
+ * Below, we say an instantiation lemma for q = forall x. F under substitution
+ * { x -> t } is the formula:
+ *   ( ~forall x. F V F * { x -> t } )
+ * where * is application of substitution.
+ *
+ * Its main interface is ::addInstantiation(...), which is called by many of
+ * the quantifiers modules, which enqueues instantiation lemmas in quantifiers
+ * engine via calls to QuantifiersEngine::addLemma.
+ *
+ * It also has utilities for constructing instantiations, and interfaces for
+ * getting the results of the instantiations produced during check-sat calls.
+ */
+class Instantiate : public QuantifiersUtil
+{
+ public:
+  Instantiate(QuantifiersEngine* qe, context::UserContext* u);
+  ~Instantiate();
+
+  /** reset */
+  virtual bool reset(Theory::Effort e) override;
+  /** register quantifier */
+  virtual void registerQuantifier(Node q) override;
+  /** identify */
+  virtual std::string identify() const override { return "Instantiate"; }
+  /** check incomplete */
+  virtual bool checkComplete() override;
+
+  //--------------------------------------notify objects
+  /** add instantiation notify
+   *
+   * Adds an instantiation notify class to listen to the instantiations reported
+   * to this class.
+   */
+  void addNotify(InstantiationNotify* in);
+  /** get number of instantiation notify added to this class */
+  bool hasNotify() const { return !d_inst_notify.empty(); }
+  /** notify flush lemmas
+   *
+   * This is called just before the quantifiers engine flushes its lemmas to
+   * the output channel.
+   */
+  void notifyFlushLemmas();
+  //--------------------------------------end notify objects
+
+  /** do instantiation specified by m
+   *
+   * This function returns true if the instantiation lemma for quantified
+   * formula q for the substitution specified by m is successfully enqueued
+   * via a call to QuantifiersEngine::addLemma.
+   *   mkRep : whether to take the representatives of the terms in the range of
+   *           the substitution m,
+   *   modEq : whether to check for duplication modulo equality in instantiation
+   *           tries (for performance),
+   *   doVts : whether we must apply virtual term substitution to the
+   *           instantiation lemma.
+   *
+   * This call may fail if it can be determined that the instantiation is not
+   * relevant or legal in the current context. This happens if:
+   * (1) The substitution is not well-typed,
+   * (2) The substitution involves terms whose instantiation level is above the
+   *     allowed limit,
+   * (3) The resulting instantiation is entailed in the current context using a
+   *     fast entailment check (see TermDb::isEntailed),
+   * (4) The range of the substitution is a duplicate of that of a previously
+   *     added instantiation,
+   * (5) The instantiation lemma is a duplicate of previously added lemma.
+   *
+   */
+  bool addInstantiation(Node q,
+                        InstMatch& m,
+                        bool mkRep = false,
+                        bool modEq = false,
+                        bool doVts = false);
+  /** add instantiation
+   *
+   * Same as above, but the substitution we are considering maps the variables
+   * of q to the vector terms, in order.
+   */
+  bool addInstantiation(Node q,
+                        std::vector<Node>& terms,
+                        bool mkRep = false,
+                        bool modEq = false,
+                        bool doVts = false);
+  /** remove pending instantiation
+   *
+   * Removes the instantiation lemma lem from the instantiation trie.
+   */
+  bool removeInstantiation(Node q, Node lem, std::vector<Node>& terms);
+  /** record instantiation
+   *
+   * Explicitly record that q has been instantiated with terms. This is the
+   * same as addInstantiation, but does not enqueue an instantiation lemma.
+   */
+  bool recordInstantiation(Node q,
+                           std::vector<Node>& terms,
+                           bool modEq = false,
+                           bool addedLem = true);
+  /** exists instantiation
+   *
+   * Returns true if and only if the instantiation already was added or
+   * recorded by this class.
+   *   modEq : whether to check for duplication modulo equality
+   */
+  bool existsInstantiation(Node q,
+                           std::vector<Node>& terms,
+                           bool modEq = false);
+  //--------------------------------------general utilities
+  /** get instantiation
+   *
+   * Returns the instantiation lemma for q under substitution { vars -> terms }.
+   * doVts is whether to apply virtual term substitution to its body.
+   */
+  Node getInstantiation(Node q,
+                        std::vector<Node>& vars,
+                        std::vector<Node>& terms,
+                        bool doVts = false);
+  /** get instantiation
+   *
+   * Same as above, but with vars/terms specified by InstMatch m.
+   */
+  Node getInstantiation(Node q, InstMatch& m, bool doVts = false);
+  /** get instantiation
+   *
+   * 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
+
+  /** debug print, called once per instantiation round. */
+  void debugPrint();
+  /** debug print model, called once, before we terminate with sat/unknown. */
+  void debugPrintModel();
+
+  //--------------------------------------user-level interface utilities
+  /** print instantiations
+   *
+   * Print all instantiations for all quantified formulas on out,
+   * returns true if at least one instantiation was printed.
+   */
+  bool printInstantiations(std::ostream& out);
+  /** get instantiated quantified formulas
+   *
+   * Get the list of quantified formulas that were instantiated in the current
+   * user context, store them in qs.
+   */
+  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
+  /** get instantiations
+   *
+   * Get the body of all instantiation lemmas added in the current user context
+   * for quantified formula q, store them in insts.
+   */
+  void getInstantiations(Node q, std::vector<Node>& insts);
+  /** get instantiations
+   *
+   * Get the body of all instantiation lemmas added in the current user context
+   * for all quantified formulas stored in the domain of insts, store them in
+   * the range of insts.
+   */
+  void getInstantiations(std::map<Node, std::vector<Node> >& insts);
+  /** get instantiation term vectors
+   *
+   * Get term vectors corresponding to for all instantiations lemmas added in
+   * the current user context for quantified formula q, store them in tvecs.
+   */
+  void getInstantiationTermVectors(Node q,
+                                   std::vector<std::vector<Node> >& tvecs);
+  /** get instantiation term vectors
+   *
+   * Get term vectors for all instantiations lemmas added in the current user
+   * context for quantified formula q, store them in tvecs.
+   */
+  void getInstantiationTermVectors(
+      std::map<Node, std::vector<std::vector<Node> > >& insts);
+  /** get instantiated conjunction
+   *
+   * This gets a conjunction of the bodies of instantiation lemmas added in the
+   * current user context for quantified formula q.  For example, if we added:
+   *   ~forall x. P( x ) V P( a )
+   *   ~forall x. P( x ) V P( b )
+   * Then, this method returns P( a ) ^ P( b ).
+   */
+  Node getInstantiatedConjunction(Node q);
+  /** get unsat core lemmas
+   *
+   * If this method returns true, then it appends to active_lemmas all lemmas
+   * that are in the unsat core that originated from the theory of quantifiers.
+   * This method returns false if the unsat core is not available.
+   */
+  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+  /** get unsat core lemmas
+   *
+   * If this method returns true, then it appends to active_lemmas all lemmas
+   * that are in the unsat core that originated from the theory of quantifiers.
+   * This method returns false if the unsat core is not available.
+   *
+   * It also computes a weak implicant for each of these lemmas. For each lemma
+   * L in active_lemmas, this is a formula L' such that:
+   *   L => L'
+   * and replacing L by L' in the unsat core results in a set that is still
+   * unsatisfiable. The map weak_imp stores this formula for each formula in
+   * active_lemmas.
+   */
+  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
+                          std::map<Node, Node>& weak_imp);
+  /** get explanation for instantiation lemmas
+   *
+   *
+   */
+  void getExplanationForInstLemmas(const std::vector<Node>& lems,
+                                   std::map<Node, Node>& quant,
+                                   std::map<Node, std::vector<Node> >& tvec);
+  //--------------------------------------end user-level interface utilities
+
+  /** statistics class
+   *
+   * This tracks statistics on the number of instantiations successfully
+   * enqueued on the quantifiers output channel, and the number of redundant
+   * instantiations encountered by various criteria.
+   */
+  class Statistics
+  {
+   public:
+    IntStat d_instantiations;
+    IntStat d_inst_duplicate;
+    IntStat d_inst_duplicate_eq;
+    IntStat d_inst_duplicate_ent;
+    IntStat d_inst_duplicate_model_true;
+    Statistics();
+    ~Statistics();
+  }; /* class Instantiate::Statistics */
+  Statistics d_statistics;
+
+ private:
+  /** record instantiation, return true if it was not a duplicate
+   *
+   * addedLem : whether an instantiation lemma was added for the vector we are
+   *            recording. If this is false, we bookkeep the vector.
+   * modEq : whether to check for duplication modulo equality in instantiation
+   *         tries (for performance),
+   */
+  bool recordInstantiationInternal(Node q,
+                                   std::vector<Node>& terms,
+                                   bool modEq = false,
+                                   bool addedLem = true);
+  /** remove instantiation from the cache */
+  bool removeInstantiationInternal(Node q, std::vector<Node>& terms);
+
+  /** pointer to the quantifiers engine */
+  QuantifiersEngine* d_qe;
+  /** cache of term database for quantifiers engine */
+  TermDb* d_term_db;
+  /** cache of term util for quantifiers engine */
+  TermUtil* d_term_util;
+  /** instantiation notify classes */
+  std::vector<InstantiationNotify*> d_inst_notify;
+
+  /** statistics for debugging total instantiation */
+  int d_total_inst_count_debug;
+  /** statistics for debugging total instantiations per quantifier */
+  std::map<Node, int> d_total_inst_debug;
+  /** statistics for debugging total instantiations per quantifier per round */
+  std::map<Node, int> d_temp_inst_debug;
+
+  /** list of all instantiations produced for each quantifier
+   *
+   * 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;
+  /**
+   * The list of quantified formulas for which the domain of d_c_inst_match_trie
+   * is valid.
+   */
+  context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom;
+
+  /** explicitly recorded instantiations
+   *
+   * Sometimes an instantiation is recorded internally but not sent out as a
+   * lemma, for instance, for partial quantifier elimination. This is a map
+   * of these instantiations, for each quantified formula.
+   */
+  std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 358838b11..dba04ce51 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
@@ -118,7 +119,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){
           {
             terms.push_back( riter.getCurrentTerm( k ) );
           }
-          Node n = d_qe->getInstantiation( f, vars, terms );
+          Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms);
           Node val = fm->getValue( n );
           if (val != d_qe->getTermUtil()->d_true)
           {
@@ -322,7 +323,8 @@ int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm)
     //try to add it
     Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
     //add model basis instantiation
-    if( d_qe->addInstantiation( fp, d_quant_basis_match[f] ) ){
+    if (d_qe->getInstantiate()->addInstantiation(fp, d_quant_basis_match[f]))
+    {
       d_quant_basis_match_added[f] = true;
       return 1;
     }else{
@@ -428,6 +430,9 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in
       Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
       fmig->resetEvaluate();
       Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
+      EqualityQuery* qy = d_qe->getEqualityQuery();
+      Instantiate* inst = d_qe->getInstantiate();
+      TermUtil* util = d_qe->getTermUtil();
       while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
         d_triedLemmas++;
         if( Debug.isOn("inst-fmf-ei-debug") ){
@@ -446,8 +451,9 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in
         //if evaluate(...)==1, then the instantiation is already true in the model
         //  depIndex is the index of the least significant variable that this evaluation relies upon
         depIndex = riter.getNumTerms()-1;
-        Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermUtil()->getInstConstantBody( f ) << std::endl;
-        eval = fmig->evaluate( d_qe->getTermUtil()->getInstConstantBody( f ), depIndex, &riter );
+        Debug("fmf-model-eval") << "We will evaluate "
+                                << util->getInstConstantBody(f) << std::endl;
+        eval = fmig->evaluate(util->getInstConstantBody(f), depIndex, &riter);
         if( eval==1 ){
           Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
         }else{
@@ -461,11 +467,12 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in
           InstMatch m( f );
           for (unsigned i = 0; i < riter.getNumTerms(); i++)
           {
-            m.set( d_qe, i, riter.getCurrentTerm( i ) );
+            m.set(qy, i, riter.getCurrentTerm(i));
           }
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           //add as instantiation
-          if( d_qe->addInstantiation( f, m, true ) ){
+          if (inst->addInstantiation(f, m, true))
+          {
             d_addedLemmas++;
             if( d_qe->inConflict() ){
               break;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 5d01e04e6..fe6e3945b 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/ambqi_builder.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
@@ -285,17 +286,20 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
       if( !riter.isIncomplete() ){
         int triedLemmas = 0;
         int addedLemmas = 0;
+        EqualityQuery* qy = d_quantEngine->getEqualityQuery();
+        Instantiate* inst = d_quantEngine->getInstantiate();
         while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
           //instantiation was not shown to be true, construct the match
           InstMatch m( f );
           for (unsigned i = 0; i < riter.getNumTerms(); i++)
           {
-            m.set( d_quantEngine, i, riter.getCurrentTerm( i ) );
+            m.set(qy, i, riter.getCurrentTerm(i));
           }
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           triedLemmas++;
           //add as instantiation
-          if( d_quantEngine->addInstantiation( f, m, true ) ){
+          if (inst->addInstantiation(f, m, true))
+          {
             addedLemmas++;
             if( d_quantEngine->inConflict() ){
               break;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 9ed4e5996..6c2b95a52 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -19,11 +19,12 @@
 
 #include "options/quantifiers_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
@@ -586,7 +587,8 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node
         return true;
       }
     }else{
-      Node inst = p->d_quantEngine->getInstantiation( d_q, terms );
+      Node inst =
+          p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms);
       Node inst_eval = p->getTermDatabase()->evaluateTerm( inst, NULL, options::qcfTConstraint() );
       if( Trace.isOn("qcf-instance-check") ){
         Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
@@ -2111,13 +2113,16 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
                         if( !tcs ){
                           //for debugging
                           if( Debug.isOn("qcf-check-inst") ){
-                            Node inst = d_quantEngine->getInstantiation( q, terms );
+                            Node inst = d_quantEngine->getInstantiate()
+                                            ->getInstantiation(q, terms);
                             Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
                             Assert( !getTermDatabase()->isEntailed( inst, true ) );
                             Assert(getTermDatabase()->isEntailed(inst, false) ||
                                    e > EFFORT_CONFLICT);
                           }
-                          if( d_quantEngine->addInstantiation( q, terms ) ){
+                          if (d_quantEngine->getInstantiate()->addInstantiation(
+                                  q, terms))
+                          {
                             Trace("qcf-check") << "   ... Added instantiation" << std::endl;
                             Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
                             qi->debugPrintMatch("qcf-inst");
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index f958605b1..b1bba1842 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -167,14 +167,19 @@ public:
   /* reset
   * Called at the beginning of an instantiation round
   * Returns false if the reset failed. When reset fails, the utility should have
-  * added a lemma
-  * via a call to qe->addLemma. TODO: improve this contract #1163
+  * added a lemma via a call to qe->addLemma. TODO: improve this contract #1163
   */
   virtual bool reset( Theory::Effort e ) = 0;
   /* Called for new quantifiers */
   virtual void registerQuantifier(Node q) = 0;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   virtual std::string identify() const = 0;
+  /** Check complete?
+   *
+   * Returns false if the utility's reasoning was globally incomplete
+   * (e.g. "sat" must be replaced with "incomplete").
+   */
+  virtual bool checkComplete() { return true; }
 };
 
 /** Arithmetic utilities regarding monomial sums.
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index d02ad667e..92d42d578 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -388,6 +388,44 @@ Node QuantAttributes::getQuantIdNumNode( Node q ) {
   }
 }
 
+void QuantAttributes::setInstantiationLevelAttr(Node n, Node qn, uint64_t level)
+{
+  Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level
+                             << std::endl;
+  // if not from the vector of terms we instantiatied
+  if (qn.getKind() != BOUND_VARIABLE && n != qn)
+  {
+    // if this is a new term, without an instantiation level
+    if (!n.hasAttribute(InstLevelAttribute()))
+    {
+      InstLevelAttribute ila;
+      n.setAttribute(ila, level);
+      Trace("inst-level-debug") << "Set instantiation level " << n << " to "
+                                << level << std::endl;
+      Assert(n.getNumChildren() == qn.getNumChildren());
+      for (unsigned i = 0; i < n.getNumChildren(); i++)
+      {
+        setInstantiationLevelAttr(n[i], qn[i], level);
+      }
+    }
+  }
+}
+
+void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level)
+{
+  if (!n.hasAttribute(InstLevelAttribute()))
+  {
+    InstLevelAttribute ila;
+    n.setAttribute(ila, level);
+    Trace("inst-level-debug") << "Set instantiation level " << n << " to "
+                              << level << std::endl;
+    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    {
+      setInstantiationLevelAttr(n[i], level);
+    }
+  }
+}
+
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 9a18d13fb..87315de7c 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -55,6 +55,11 @@ typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
 struct SynthesisAttributeId {};
 typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
 
+struct InstLevelAttributeId
+{
+};
+typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
+
 /** Attribute for setting printing information for sygus variables
  *
  * For variable d of sygus datatype type, if
@@ -185,7 +190,12 @@ public:
   /** get quant id num */
   Node getQuantIdNumNode( Node q );
 
-private:
+  /** set instantiation level attr */
+  static void setInstantiationLevelAttr(Node n, uint64_t level);
+  /** set instantiation level attr */
+  static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level);
+
+ private:
   /** pointer to quantifiers engine */
   QuantifiersEngine * d_quantEngine;
   /** cache of attributes */
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 337d61976..922a8cce6 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -19,10 +19,11 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_match_generator.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
@@ -159,7 +160,8 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
                 if( inst.size()>f[0].getNumChildren() ){
                   inst.resize( f[0].getNumChildren() );
                 }
-                if( d_quantEngine->addInstantiation( f, inst ) ){
+                if (d_quantEngine->getInstantiate()->addInstantiation(f, inst))
+                {
                   addedLemmas++;
                   tempAddedLemmas++;
                   /*
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 2f210cc20..555058d98 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/skolemize.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/sort_inference.h"
@@ -286,7 +287,7 @@ Node Skolemize::mkSkolemizedBody(Node f,
   // if it has an instantiation level, set the skolemized body to that level
   if (f.hasAttribute(InstLevelAttribute()))
   {
-    theory::QuantifiersEngine::setInstantiationLevelAttr(
+    QuantAttributes::setInstantiationLevelAttr(
         ret, f.getAttribute(InstLevelAttribute()));
   }
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5db58067f..19cdc68e5 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -186,7 +186,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
                    << std::endl;
     if (options::instMaxLevel() != -1)
     {
-      QuantifiersEngine::setInstantiationLevelAttr(k, 0);
+      QuantAttributes::setInstantiationLevelAttr(k, 0);
     }
     d_type_fv[tn] = k;
     return k;
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 5ac21dafb..ed6cd018f 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -34,9 +34,6 @@ typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
 struct BoundVarAttributeId {};
 typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute;
 
-struct InstLevelAttributeId {};
-typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
-
 struct InstVarNumAttributeId {};
 typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
 
@@ -97,13 +94,16 @@ 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
 {
   // TODO : remove these
   friend class ::CVC4::theory::QuantifiersEngine;
-private:
+  friend class Instantiate;
+
+ private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
 public:
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index b72f6c8cb..61920250e 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/candidate_generator.h"
 #include "theory/quantifiers/ho_trigger.h"
 #include "theory/quantifiers/inst_match_generator.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -119,7 +120,7 @@ int Trigger::addInstantiations(InstMatch& baseMatch)
 
 bool Trigger::sendInstantiation(InstMatch& m)
 {
-  return d_quantEngine->addInstantiation(d_f, m);
+  return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
 }
 
 bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index bc2b533be..59a85de1f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -35,6 +35,7 @@
 #include "theory/quantifiers/inst_strategy_cbqi.h"
 #include "theory/quantifiers/inst_strategy_e_matching.h"
 #include "theory/quantifiers/inst_strategy_enumerative.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/instantiation_engine.h"
 #include "theory/quantifiers/local_theory_ext.h"
 #include "theory/quantifiers/model_engine.h"
@@ -71,6 +72,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
                                      TheoryEngine* te)
     : d_te(te),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
+      d_instantiate(new quantifiers::Instantiate(this, u)),
       d_skolemize(new quantifiers::Skolemize(this, u)),
       d_term_enum(new quantifiers::TermEnumeration),
       d_conflict_c(c, false),
@@ -108,7 +110,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
     // notice that this option is incompatible with options::qcfAllConflict()
     d_inst_prop = new quantifiers::InstPropagator( this );
     d_util.push_back( d_inst_prop );
-    d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() );
+    d_instantiate->addNotify(d_inst_prop->getInstantiationNotify());
   }else{
     d_inst_prop = NULL;
   }
@@ -119,6 +121,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
     d_eq_inference = NULL;
   }
 
+  d_util.push_back(d_instantiate.get());
+
   d_tr_trie = new inst::TriggerTrie;
   d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
   d_conflict = false;
@@ -165,7 +169,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   d_bv_invert = NULL;
   d_builder = NULL;
 
-  d_total_inst_count_debug = 0;
   //allow theory combination to go first, once initially
   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
   d_ierCounter_c = d_ierCounter;
@@ -175,14 +178,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
 }
 
 QuantifiersEngine::~QuantifiersEngine(){
-  for(std::map< Node, inst::CDInstMatchTrie* >::iterator
-      i = d_c_inst_match_trie.begin(), iend = d_c_inst_match_trie.end();
-      i != iend; ++i)
-  {
-    delete (*i).second;
-  }
-  d_c_inst_match_trie.clear();
-
   delete d_alpha_equiv;
   delete d_builder;
   delete d_qepr;
@@ -406,7 +401,8 @@ void QuantifiersEngine::ppNotifyAssertions(
       d_qepr != NULL) {
     for (unsigned i = 0; i < assertions.size(); i++) {
       if (options::instLevelInputOnly() && options::instMaxLevel() != -1) {
-        setInstantiationLevelAttr(assertions[i], 0);
+        quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions[i],
+                                                                0);
       }
       if (d_qepr != NULL) {
         d_qepr->registerAssertion(assertions[i]);
@@ -448,13 +444,15 @@ void QuantifiersEngine::check( Theory::Effort e ){
   std::vector< QuantifiersModule* > qm;
   if( d_model->checkNeeded() ){
     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
-    for( unsigned i=0; i<d_modules.size(); i++ ){
-      if( d_modules[i]->needsCheck( e ) ){
-        qm.push_back( d_modules[i] );
+    for (QuantifiersModule*& mdl : d_modules)
+    {
+      if (mdl->needsCheck(e))
+      {
+        qm.push_back(mdl);
         needsCheck = true;
         //can only request model at last call since theory combination can find inconsistencies
         if( e>=Theory::EFFORT_LAST_CALL ){
-          QuantifiersModule::QEffort me = d_modules[i]->needsModel(e);
+          QuantifiersModule::QEffort me = mdl->needsModel(e);
           needsModelE = me<needsModelE ? me : needsModelE;
         }
       }
@@ -474,14 +472,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     if( d_hasAddedLemma ){
       return;
     }
-    if( !d_recorded_inst.empty() ){
-      Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size() << " instantiations..." << std::endl;
-      //remove explicitly recorded instantiations
-      for( unsigned i=0; i<d_recorded_inst.size(); i++ ){
-        removeInstantiationInternal( d_recorded_inst[i].first, d_recorded_inst[i].second );
-      } 
-      d_recorded_inst.clear();
-    }
     
     double clSet = 0;
     if( Trace.isOn("quant-engine") ){
@@ -515,9 +505,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
     //reset utilities
     Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
-    for( unsigned i=0; i<d_util.size(); i++ ){
-      Trace("quant-engine-debug2") << "Reset " << d_util[i]->identify().c_str() << "..." << std::endl;
-      if( !d_util[i]->reset( e ) ){
+    for (QuantifiersUtil*& util : d_util)
+    {
+      Trace("quant-engine-debug2") << "Reset " << util->identify().c_str()
+                                   << "..." << std::endl;
+      if (!util->reset(e))
+      {
         flushLemmas();
         if( d_hasAddedLemma ){
           return;
@@ -539,9 +532,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
     //reset the modules
     Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
-    for( unsigned i=0; i<d_modules.size(); i++ ){
-      Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
-      d_modules[i]->reset_round( e );
+    for (QuantifiersModule*& mdl : d_modules)
+    {
+      Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str()
+                                   << std::endl;
+      mdl->reset_round(e);
     }
     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
     //reset may have added lemmas
@@ -579,9 +574,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
       if( !d_hasAddedLemma ){
         //check each module
-        for( unsigned i=0; i<qm.size(); i++ ){
-          Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
-          qm[i]->check( e, quant_e );
+        for (QuantifiersModule*& mdl : qm)
+        {
+          Trace("quant-engine-debug") << "Check " << mdl->identify().c_str()
+                                      << " at effort " << quant_e << "..."
+                                      << std::endl;
+          mdl->check(e, quant_e);
           if( d_conflict ){
             Trace("quant-engine-debug") << "...conflict!" << std::endl;
             break;
@@ -612,17 +610,27 @@ void QuantifiersEngine::check( Theory::Effort e ){
         {
           if( e==Theory::EFFORT_LAST_CALL ){
             //sources of incompleteness
-            if( !d_recorded_inst.empty() ){
-              Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl;
-              setIncomplete = true;
+            for (QuantifiersUtil*& util : d_util)
+            {
+              if (!util->checkComplete())
+              {
+                Trace("quant-engine-debug") << "Set incomplete because utility "
+                                            << util->identify().c_str()
+                                            << " was incomplete." << std::endl;
+                setIncomplete = true;
+              }
             }
             //if we have a chance not to set incomplete
             if( !setIncomplete ){
-              setIncomplete = false;
               //check if we should set the incomplete flag
-              for( unsigned i=0; i<d_modules.size(); i++ ){
-                if( !d_modules[i]->checkComplete() ){
-                  Trace("quant-engine-debug") << "Set incomplete because " << d_modules[i]->identify().c_str() << " was incomplete." << std::endl;
+              for (QuantifiersModule*& mdl : d_modules)
+              {
+                if (!mdl->checkComplete())
+                {
+                  Trace("quant-engine-debug")
+                      << "Set incomplete because module "
+                      << mdl->identify().c_str() << " was incomplete."
+                      << std::endl;
                   setIncomplete = true;
                   break;
                 }
@@ -666,13 +674,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
     if( d_hasAddedLemma ){
-      //debug information
-      if( Trace.isOn("inst-per-quant-round") ){
-        for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){
-          Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl;
-          d_temp_inst_debug[it->first] = 0;
-        }
-      }
+      d_instantiate->debugPrint();
     }
     if( Trace.isOn("quant-engine") ){
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
@@ -703,11 +705,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       getOutputChannel().setIncomplete();
     }
     //output debug stats
-    if( Trace.isOn("inst-per-quant") ){
-      for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
-        Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
-      }
-    }
+    d_instantiate->debugPrintModel();
   }
 }
 
@@ -907,192 +905,6 @@ void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
   //}
 }
 
-void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    Node n = m.get( i );
-    if( !n.isNull() ){
-      vars.push_back( f[0][i] );
-      terms.push_back( n );
-    }
-  }
-}
-
-
-bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool addedLem ) {
-  if( !addedLem ){
-    //record the instantiation for deletion later
-    d_recorded_inst.push_back( std::pair< Node, std::vector< Node > >( q, terms ) );
-  }
-  if( options::incrementalSolving() ){
-    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 );
-    if( it!=d_c_inst_match_trie.end() ){
-      imt = it->second;
-    }else{
-      imt = new CDInstMatchTrie( getUserContext() );
-      d_c_inst_match_trie[q] = imt;
-    }
-    return imt->addInstMatch( this, q, terms, getUserContext(), modEq );
-  }else{
-    Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
-    return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq );
-  }
-}
-
-bool QuantifiersEngine::removeInstantiationInternal( Node q, std::vector< Node >& terms ) {
-  if( options::incrementalSolving() ){
-    std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
-    if( it!=d_c_inst_match_trie.end() ){
-      return it->second->removeInstMatch( this, q, terms );
-    }else{
-      return false;
-    }
-  }else{
-    return d_inst_match_trie[q].removeInstMatch( this, q, terms );
-  }
-}
-
-void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
-  Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl;
-  //if not from the vector of terms we instantiatied
-  if( qn.getKind()!=BOUND_VARIABLE && n!=qn ){
-    //if this is a new term, without an instantiation level
-    if( !n.hasAttribute(InstLevelAttribute()) ){
-      InstLevelAttribute ila;
-      n.setAttribute(ila,level);
-      Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
-      Assert( n.getNumChildren()==qn.getNumChildren() );
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        setInstantiationLevelAttr( n[i], qn[i], level );
-      }
-    }
-  }
-}
-
-void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
-  if( !n.hasAttribute(InstLevelAttribute()) ){
-    InstLevelAttribute ila;
-    n.setAttribute(ila,level);
-    Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      setInstantiationLevelAttr( n[i], level );
-    }
-  }
-}
-
-Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited ){
-  std::map< Node, Node >::iterator itv = visited.find( n );
-  if( itv==visited.end() ){
-    Node ret = n;
-    if( n.getKind()==INST_CONSTANT ){
-      Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
-      ret = terms[n.getAttribute(InstVarNumAttribute())];
-    }else{
-      //if( !quantifiers::TermUtil::hasInstConstAttr( n ) ){
-        //Debug("check-inst") << "No inst const attr : " << n << std::endl;
-        //return n;
-      //}else{
-        //Debug("check-inst") << "Recurse on : " << n << std::endl;
-      std::vector< Node > cc;
-      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        cc.push_back( n.getOperator() );
-      }
-      bool changed = false;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node c = getSubstitute( n[i], terms, visited );
-        cc.push_back( c );
-        changed = changed || c!=n[i];
-      }
-      if( changed ){
-        ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
-      }
-    }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return itv->second;
-  }
-}
-
-
-Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
-  Node body;
-  Assert( vars.size()==terms.size() );
-  //process partial instantiation if necessary
-  if( q[0].getNumChildren()!=vars.size() ){
-    body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-    std::vector< Node > uninst_vars;
-    //doing a partial instantiation, must add quantifier for all uninstantiated variables
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      if( std::find( vars.begin(), vars.end(), q[0][i] )==vars.end() ){
-        uninst_vars.push_back( q[0][i] );
-      }
-    }
-    Trace("partial-inst") << "Partially instantiating with " << vars.size() << " / " << q[0].getNumChildren() << " for " << q << std::endl;
-    Assert( !uninst_vars.empty() );
-    Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
-    body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
-    Trace("partial-inst") << "Partial instantiation : " << q << std::endl;
-    Trace("partial-inst") << "                      : " << body << std::endl;
-  }else{
-    if( options::cbqi() ){
-      body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-    }else{
-      //do optimized version
-      Node icb = d_term_util->getInstConstantBody( q );
-      std::map< Node, Node > visited;
-      body = getSubstitute( icb, terms, visited );
-      if( Debug.isOn("check-inst") ){
-        Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-        if( body!=body2 ){
-          Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
-        }
-      }
-    }
-  }
-  if( doVts ){
-    //do virtual term substitution
-    body = Rewriter::rewrite( body );
-    Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
-    Node body_r = d_term_util->rewriteVtsSymbols( body );
-    Trace("quant-vts-debug") << "            ...result: " << body_r << std::endl;
-    body = body_r;
-  }
-  return body;
-}
-
-Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){
-  std::vector< Node > vars;
-  std::vector< Node > terms;
-  computeTermVector( q, m, vars, terms );
-  return getInstantiation( q, vars, terms, doVts );
-}
-
-Node QuantifiersEngine::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 );
-}
-
-/*
-bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){
-  if( options::incrementalSolving() ){
-    if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
-      if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){
-        return true;
-      }
-    }
-  }else{
-    if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
-      if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-*/
-
 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
   if( doCache ){
     if( doRewrite ){
@@ -1132,217 +944,6 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
   d_phase_req_waiting[lit] = req;
 }
 
-bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts ){
-  std::vector< Node > terms;
-  m.getTerms( q, terms );
-  return addInstantiation( q, terms, mkRep, modEq, doVts );
-}
-
-bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool doVts ) {
-  // For resource-limiting (also does a time check).
-  getOutputChannel().safePoint(options::quantifierStep());
-  Assert( !d_conflict );
-  Assert( terms.size()==q[0].getNumChildren() );
-  Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
-  std::vector< Node > rlv_cond;
-  for( unsigned i=0; i<terms.size(); i++ ){
-    Trace("inst-add-debug") << "  " << q[0][i];
-    Trace("inst-add-debug2") << " -> " << terms[i];
-    TypeNode tn = q[0][i].getType();
-    if( terms[i].isNull() ){
-      terms[i] = getTermForType(tn);
-    }
-    if( mkRep ){
-      //pick the best possible representative for instantiation, based on past use and simplicity of term
-      terms[i] = getInternalRepresentative( terms[i], q, i );
-    }else{
-      //ensure the type is correct
-      terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn);
-    }
-    Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
-    if( terms[i].isNull() ){
-      Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl;
-      return false;
-    }else{
-      //get relevancy conditions
-      if( options::instRelevantCond() ){
-        quantifiers::TermUtil::getRelevancyCondition( terms[i], rlv_cond );
-      }
-    }
-#ifdef CVC4_ASSERTIONS
-    bool bad_inst = false;
-    if( quantifiers::TermUtil::containsUninterpretedConstant( terms[i] ) ){
-      Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl;
-      bad_inst = true;
-    }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
-      Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl;
-      bad_inst = true;
-    }else if( options::cbqi() ){
-      Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
-      if( !icf.isNull() ){
-        if( icf==q ){
-          Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl;
-          bad_inst = true;
-        }else if( quantifiers::TermUtil::containsTerms( terms[i], d_term_util->d_inst_constants[q] ) ){
-          Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl;
-          bad_inst = true;
-        }
-      }
-    }
-    //this assertion is critical to soundness
-    if( bad_inst ){
-      Trace("inst")<< "***& Bad Instantiate " << q << " with " << std::endl;
-      for( unsigned j=0; j<terms.size(); j++ ){
-        Trace("inst") << "   " << terms[j] << std::endl;
-      }
-      Assert( false );
-    }
-#endif
-  }
-
-  //check based on instantiation level
-  if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
-    for( unsigned i=0; i<terms.size(); i++ ){
-      if( !d_term_db->isTermEligibleForInstantiation( terms[i], q, true ) ){
-        return false;
-      }
-    }
-  }
-
-  //check for positive entailment
-  if( options::instNoEntail() ){
-    //TODO: check consistency of equality engine (if not aborting on utility's reset)
-    std::map< TNode, TNode > subs;
-    for( unsigned i=0; i<terms.size(); i++ ){
-      subs[q[0][i]] = terms[i];
-    }
-    if( d_term_db->isEntailed( q[1], subs, false, true ) ){
-      Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
-      ++(d_statistics.d_inst_duplicate_ent);
-      return false;
-    }
-    //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
-    //Trace("inst-add-debug2") << "Instantiation evaluates to : " << std::endl;
-    //Trace("inst-add-debug2") << "   " << eval << std::endl;
-  }
-
-  //check for term vector duplication
-  bool alreadyExists = !recordInstantiationInternal( q, terms, modEq );
-  if( alreadyExists ){
-    Trace("inst-add-debug") << " --> Already exists." << std::endl;
-    ++(d_statistics.d_inst_duplicate_eq);
-    return false;
-  }
-
-  //construct the instantiation
-  Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
-  Assert( d_term_util->d_vars[q].size()==terms.size() );
-  Node body = getInstantiation( q, d_term_util->d_vars[q], terms, doVts );  //do virtual term substitution
-  Node orig_body = body;
-  if( options::cbqiNestedQE() && d_i_cbqi ){
-    body = d_i_cbqi->doNestedQE( q, terms, body, doVts );
-  }  
-  body = quantifiers::QuantifiersRewriter::preprocess( body, true );
-  Trace("inst-debug") << "...preprocess to " << body << std::endl;
-
-  //construct the lemma
-  Trace("inst-assert") << "(assert " << body << ")" << std::endl;
-  body = Rewriter::rewrite(body);
-  
-  if( d_useModelEe && options::instNoModelTrue() ){
-    Node val_body = d_model->getValue( body );
-    if( val_body==d_term_util->d_true ){
-      Trace("inst-add-debug") << " --> True in model." << std::endl;
-      ++(d_statistics.d_inst_duplicate_model_true);
-      return false;
-    }
-  }
-  
-  Node lem;
-  if( rlv_cond.empty() ){
-    lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
-  }else{
-    rlv_cond.push_back( q.negate() );
-    rlv_cond.push_back( body );
-    lem = NodeManager::currentNM()->mkNode( kind::OR, rlv_cond );
-  }
-  lem = Rewriter::rewrite(lem);
-
-  //check for lemma duplication
-  if( addLemma( lem, true, false ) ){
-    d_total_inst_debug[q]++;
-    d_temp_inst_debug[q]++;
-    d_total_inst_count_debug++;
-    if( Trace.isOn("inst") ){
-      Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
-      for( unsigned i=0; i<terms.size(); i++ ){
-        if( Trace.isOn("inst") ){
-          Trace("inst") << "   " << terms[i];
-          if( Trace.isOn("inst-debug") ){
-            Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << q[0][i].getType();
-          }
-          Trace("inst") << std::endl;
-        }
-      }
-    }
-    if( options::instMaxLevel()!=-1 ){
-      if( doVts ){
-        //virtual term substitution/instantiation level features are incompatible
-        Assert( false );
-      }else{
-        uint64_t maxInstLevel = 0;
-        for( unsigned i=0; i<terms.size(); i++ ){
-          if( terms[i].hasAttribute(InstLevelAttribute()) ){
-            if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
-              maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
-            }
-          }
-        }
-        setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 );
-      }
-    }
-    if (d_curr_effort_level > QuantifiersModule::QEFFORT_CONFLICT
-        && d_curr_effort_level < QuantifiersModule::QEFFORT_NONE)
-    {
-      //notify listeners
-      for( unsigned j=0; j<d_inst_notify.size(); j++ ){
-        if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){
-          Trace("inst-add-debug") << "...we are in conflict." << std::endl;
-          setConflict();
-          Assert( !d_lemmas_waiting.empty() );
-          break;
-        }
-      }
-    }
-    if( options::trackInstLemmas() ){
-      bool recorded;
-      if( options::incrementalSolving() ){
-        recorded = d_c_inst_match_trie[q]->recordInstLemma( q, terms, lem );
-      }else{
-        recorded = d_inst_match_trie[q].recordInstLemma( q, terms, lem );
-      }
-      Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl;
-      Assert( recorded );
-    }
-    Trace("inst-add-debug") << " --> Success." << std::endl;
-    ++(d_statistics.d_instantiations);
-    return true;
-  }else{
-    Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
-    ++(d_statistics.d_inst_duplicate);
-    return false;
-  }
-}
-
-bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) {
-  //lem must occur in d_waiting_lemmas
-  if( removeLemma( lem ) ){
-    return removeInstantiationInternal( q, terms );
-  }else{
-    return false;
-  }
-}
-
 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
   n = Rewriter::rewrite( n );
   Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
@@ -1419,11 +1020,10 @@ quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
 void QuantifiersEngine::flushLemmas(){
   if( !d_lemmas_waiting.empty() ){
     //filter based on notify classes
-    if( !d_inst_notify.empty() ){
+    if (d_instantiate->hasNotify())
+    {
       unsigned prev_lem_sz = d_lemmas_waiting.size();
-      for( unsigned j=0; j<d_inst_notify.size(); j++ ){
-        d_inst_notify[j]->filterInstantiations();
-      }  
+      d_instantiate->notifyFlushLemmas();
       if( prev_lem_sz!=d_lemmas_waiting.size() ){
         Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
       }
@@ -1446,94 +1046,30 @@ void QuantifiersEngine::flushLemmas(){
 }
 
 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
-  //only if unsat core available
-  bool isUnsatCoreAvailable = false;
-  if( options::proof() ){
-    isUnsatCoreAvailable = ProofManager::currentPM()->unsatCoreAvailable();
-  }
-  if( isUnsatCoreAvailable ){
-    Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl;
-    ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, active_lemmas);
-    if( Trace.isOn("inst-unsat-core") ){
-      Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " << std::endl;
-      for (unsigned i = 0; i < active_lemmas.size(); ++i) {
-        Trace("inst-unsat-core") << "  " << active_lemmas[i] << std::endl;
-      }
-      Trace("inst-unsat-core") << std::endl;
-    }
-    return true;
-  }else{
-    return false;
-  }
+  return d_instantiate->getUnsatCoreLemmas(active_lemmas);
 }
 
 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) {
-  if( getUnsatCoreLemmas( active_lemmas ) ){
-    for (unsigned i = 0; i < active_lemmas.size(); ++i) {
-      Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(active_lemmas[i]);
-      if( n!=active_lemmas[i] ){
-        Trace("inst-unsat-core") << "  weaken : " << active_lemmas[i] << " -> " << n << std::endl;
-      }
-      weak_imp[active_lemmas[i]] = n;
-    }
-    return true;
-  }else{
-    return false;
-  }
+  return d_instantiate->getUnsatCoreLemmas(active_lemmas, weak_imp);
 }
 
 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
-  std::vector< Node > lemmas;
-  getInstantiations( q, lemmas );
-  std::map< Node, Node > quant;
-  std::map< Node, std::vector< Node > > tvec;
-  getExplanationForInstLemmas( lemmas, quant, tvec );
-  for( std::map< Node, std::vector< Node > >::iterator it = tvec.begin(); it != tvec.end(); ++it ){
-    tvecs.push_back( it->second );
-  }
+  d_instantiate->getInstantiationTermVectors(q, tvecs);
 }
 
 void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
-  if( options::incrementalSolving() ){
-    for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
-      getInstantiationTermVectors( it->first, insts[it->first] );
-    }
-  }else{
-    for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
-      getInstantiationTermVectors( it->first, insts[it->first] );
-    }
-  }
+  d_instantiate->getInstantiationTermVectors(insts);
 }
 
-void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) {
-  if( options::trackInstLemmas() ){
-    if( options::incrementalSolving() ){
-      for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
-        it->second->getExplanationForInstLemmas( it->first, lems, quant, tvec );
-      }
-    }else{
-      for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
-        it->second.getExplanationForInstLemmas( it->first, lems, quant, tvec );
-      }
-    }
-#ifdef CVC4_ASSERTIONS
-    for( unsigned j=0; j<lems.size(); j++ ){
-      Assert( quant.find( lems[j] )!=quant.end() );
-      Assert( tvec.find( lems[j] )!=tvec.end() );
-    }
-#endif
-  }else{
-    Assert( false );
-  }
+void QuantifiersEngine::getExplanationForInstLemmas(
+    const std::vector<Node>& lems,
+    std::map<Node, Node>& quant,
+    std::map<Node, std::vector<Node> >& tvec)
+{
+  d_instantiate->getExplanationForInstLemmas(lems, quant, tvec);
 }
 
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
-  bool useUnsatCore = false;
-  std::vector< Node > active_lemmas;
-  if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
-    useUnsatCore = true;
-  }
-
   bool printed = false;
   // print the skolemizations
   if (d_skolemize->printSkolemization(out))
@@ -1541,24 +1077,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) {
     printed = true;
   }
   // print the instantiations
-  if( options::incrementalSolving() ){
-    for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
-      bool firstTime = true;
-      it->second->print( out, it->first, firstTime, useUnsatCore, active_lemmas );
-      if( !firstTime ){
-        out << ")" << std::endl;
-      }      
-      printed = printed || !firstTime;
-    }
-  }else{
-    for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
-      bool firstTime = true;
-      it->second.print( out, it->first, firstTime, useUnsatCore, active_lemmas );
-      if( !firstTime ){
-        out << ")" << std::endl;
-      }
-      printed = printed || !firstTime;
-    }
+  if (d_instantiate->printInstantiations(out))
+  {
+    printed = true;
   }
   if( !printed ){
     out << "No instantiations" << std::endl;
@@ -1574,70 +1095,19 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
 }
 
 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
-  if( options::incrementalSolving() ){
-    for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
-      qs.push_back( it->first );
-    }
-  }else{
-    for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
-      qs.push_back( it->first );
-    }
-  }
+  d_instantiate->getInstantiatedQuantifiedFormulas(qs);
 }
 
 void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
-  bool useUnsatCore = false;
-  std::vector< Node > active_lemmas;
-  if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
-    useUnsatCore = true;
-  }
-
-  if( options::incrementalSolving() ){
-    for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
-      it->second->getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas );
-    }
-  }else{
-    for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
-      it->second.getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas );
-    }
-  }
+  d_instantiate->getInstantiations(insts);
 }
 
 void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts  ) {
-  if( options::incrementalSolving() ){
-    std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
-    if( it!=d_c_inst_match_trie.end() ){
-      std::vector< Node > active_lemmas;
-      it->second->getInstantiations( insts, it->first, this, false, active_lemmas );
-    }
-  }else{
-    std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.find( q );
-    if( it!=d_inst_match_trie.end() ){
-      std::vector< Node > active_lemmas;
-      it->second.getInstantiations( insts, it->first, this, false, active_lemmas );
-    }
-  }
+  d_instantiate->getInstantiations(q, insts);
 }
 
 Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
-  Assert( q.getKind()==FORALL );
-  std::vector< Node > insts;
-  getInstantiations( q, insts );
-  if( insts.empty() ){
-    return NodeManager::currentNM()->mkConst(true);
-  }else{
-    Node ret;
-    if( insts.size()==1 ){
-      ret = insts[0];
-    }else{
-      ret = NodeManager::currentNM()->mkNode( kind::AND, insts );
-    }
-    //have to remove q, TODO: avoid this in a better way
-    TNode tq = q;
-    TNode tt = d_term_util->d_true;
-    ret = ret.substitute( tq, tt );
-    return ret;
-  }
+  return d_instantiate->getInstantiatedConjunction(q);
 }
 
 QuantifiersEngine::Statistics::Statistics()
@@ -1647,11 +1117,6 @@ QuantifiersEngine::Statistics::Statistics()
       d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
       d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
       d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
-      d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
-      d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
-      d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
-      d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0),
-      d_inst_duplicate_model_true("QuantifiersEngine::Duplicate_Inst_Model_True", 0),
       d_triggers("QuantifiersEngine::Triggers", 0),
       d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
@@ -1673,11 +1138,6 @@ QuantifiersEngine::Statistics::Statistics()
   smtStatisticsRegistry()->registerStat(&d_num_quant);
   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
-  smtStatisticsRegistry()->registerStat(&d_instantiations);
-  smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
-  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
-  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
-  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true);
   smtStatisticsRegistry()->registerStat(&d_triggers);
   smtStatisticsRegistry()->registerStat(&d_simple_triggers);
   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
@@ -1701,11 +1161,6 @@ QuantifiersEngine::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_num_quant);
   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations);
-  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
-  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
-  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
-  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true);
   smtStatisticsRegistry()->unregisterStat(&d_triggers);
   smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
@@ -1742,18 +1197,6 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
   return ret;
 }
 
-Node QuantifiersEngine::getTermForType(TypeNode tn)
-{
-  if (d_term_enum->isClosedEnumerableType(tn))
-  {
-    return d_term_enum->getEnumerateTerm(tn, 0);
-  }
-  else
-  {
-    return d_term_db->getOrMakeTypeGroundTerm(tn);
-  }
-}
-
 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
   eq::EqualityEngine* ee = getActiveEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 37691488e..6c7820cef 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -40,18 +40,6 @@ namespace theory {
 
 class QuantifiersEngine;
 
-class InstantiationNotify {
-public:
-  InstantiationNotify(){}
-  virtual ~InstantiationNotify() {}
-  virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
-                                   Node q,
-                                   Node lem,
-                                   std::vector<Node>& terms,
-                                   Node body) = 0;
-  virtual void filterInstantiations() = 0;
-};
-
 namespace quantifiers {
   //TODO: organize this more/review this, github issue #1163
   //TODO: include these instead of doing forward declarations? #1307
@@ -59,6 +47,7 @@ namespace quantifiers {
   class TermDb;
   class TermDbSygus;
   class TermUtil;
+  class Instantiate;
   class Skolemize;
   class TermEnumeration;
   class FirstOrderModel;
@@ -97,6 +86,7 @@ namespace inst {
 
 
 class QuantifiersEngine {
+  // TODO: remove these github issue #1163
   friend class quantifiers::InstantiationEngine;
   friend class quantifiers::InstStrategyCbqi;
   friend class quantifiers::InstStrategyCegqi;
@@ -115,8 +105,6 @@ private:
   std::vector< QuantifiersUtil* > d_util;
   /** vector of modules for quantifiers */
   std::vector< QuantifiersModule* > d_modules;
-  /** instantiation notify */
-  std::vector< InstantiationNotify* > d_inst_notify;
   /** equality query class */
   quantifiers::EqualityQueryQuantifiersEngine* d_eq_query;
   /** equality inference class */
@@ -141,6 +129,8 @@ private:
   quantifiers::TermUtil* d_term_util;
   /** quantifiers attributes */
   std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+  /** instantiate utility */
+  std::unique_ptr<quantifiers::Instantiate> d_instantiate;
   /** skolemize utility */
   std::unique_ptr<quantifiers::Skolemize> d_skolemize;
   /** term enumeration utility */
@@ -199,19 +189,10 @@ private:
   std::vector< Node > d_lemmas_waiting;
   /** phase requirements waiting */
   std::map< Node, bool > d_phase_req_waiting;
-  /** list of all instantiations produced for each quantifier */
-  std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
-  std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
-  /** recorded instantiations */
-  std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
   /** all triggers will be stored in this trie */
   inst::TriggerTrie* d_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
-  /** statistics for debugging */
-  std::map< Node, int > d_total_inst_debug;
-  std::map< Node, int > d_temp_inst_debug;
-  int d_total_inst_count_debug;
   /** inst round counters TODO: make context-dependent? */
   context::CDO< int > d_ierCounter_c;
   int d_ierCounter;
@@ -319,37 +300,15 @@ public:
 private:
   /** reduceQuantifier, return true if reduced */
   bool reduceQuantifier( Node q );
-  /** compute term vector */
-  void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
-  /** record instantiation, return true if it was non-duplicate */
-  bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true );
-  /** remove instantiation */
-  bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
-  /** set instantiation level attr */
-  static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
   /** flush lemmas */
   void flushLemmas();
 public:
-  /** get instantiation */
-  Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
-  /** get instantiation */
-  Node getInstantiation( Node q, InstMatch& m, bool doVts = false );
-  /** get instantiation */
-  Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false );
-  /** do substitution */
-  Node getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited );
   /** add lemma lem */
   bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
   /** remove pending lemma */
   bool removeLemma( Node lem );
   /** add require phase */
   void addRequirePhase( Node lit, bool req );
-  /** do instantiation specified by m */
-  bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false );
-  /** add instantiation */
-  bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false );
-  /** remove pending instantiation */
-  bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms );
   /** split on node n */
   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
   /** add split equality */
@@ -364,14 +323,14 @@ public:
   bool inConflict() { return d_conflict; }
   /** set conflict */
   void setConflict();
+  /** get current q effort */
+  QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
   /** get number of waiting lemmas */
   unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
   /** get needs check */
   bool getInstWhenNeedsCheck( Theory::Effort e );
   /** get user pat mode */
   quantifiers::UserPatMode getInstUserPatMode();
-  /** set instantiation level attr */
-  static void setInstantiationLevelAttr( Node n, uint64_t level );
 public:
   /** get model */
   quantifiers::FirstOrderModel* getModel() { return d_model; }
@@ -385,6 +344,8 @@ public:
   quantifiers::QuantAttributes* getQuantAttributes() {
     return d_quant_attr.get();
   }
+  /** get instantiate utility */
+  quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); }
   /** get skolemize utility */
   quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); }
   /** get term enumeration utility */
@@ -405,42 +366,41 @@ public:
   eq::EqualityEngine* getMasterEqualityEngine();
   /** get the active equality engine */
   eq::EqualityEngine* getActiveEqualityEngine();
+  /** use model equality engine */
+  bool usingModelEqualityEngine() const { return d_useModelEe; }
   /** debug print equality engine */
   void debugPrintEqualityEngine( const char * c );
   /** get internal representative */
   Node getInternalRepresentative( Node a, Node q, int index );
-  /** 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);
 
  public:
+  //----------user interface for instantiations (see quantifiers/instantiate.h)
   /** print instantiations */
-  void printInstantiations( std::ostream& out );
+  void printInstantiations(std::ostream& out);
   /** print solution for synthesis conjectures */
-  void printSynthSolution( std::ostream& out );
+  void printSynthSolution(std::ostream& out);
   /** get list of quantified formulas that were instantiated */
-  void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
+  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
   /** get instantiations */
-  void getInstantiations( Node q, std::vector< Node >& insts );
-  void getInstantiations( std::map< Node, std::vector< Node > >& insts );
+  void getInstantiations(Node q, std::vector<Node>& insts);
+  void getInstantiations(std::map<Node, std::vector<Node> >& insts);
   /** get instantiation term vectors */
-  void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
-  void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
+  void getInstantiationTermVectors(Node q,
+                                   std::vector<std::vector<Node> >& tvecs);
+  void getInstantiationTermVectors(
+      std::map<Node, std::vector<std::vector<Node> > >& insts);
   /** get instantiated conjunction */
-  Node getInstantiatedConjunction( Node q );
+  Node getInstantiatedConjunction(Node q);
   /** get unsat core lemmas */
-  bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas );
-  bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp );
-  /** get inst for lemmas */
-  void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ); 
+  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
+                          std::map<Node, Node>& weak_imp);
+  /** get explanation for instantiation lemmas */
+  void getExplanationForInstLemmas(const std::vector<Node>& lems,
+                                   std::map<Node, Node>& quant,
+                                   std::map<Node, std::vector<Node> >& tvec);
+  //----------end user interface for instantiations
+
   /** statistics class */
   class Statistics {
   public:
@@ -450,11 +410,6 @@ public:
     IntStat d_num_quant;
     IntStat d_instantiation_rounds;
     IntStat d_instantiation_rounds_lc;
-    IntStat d_instantiations;
-    IntStat d_inst_duplicate;
-    IntStat d_inst_duplicate_eq;
-    IntStat d_inst_duplicate_ent;
-    IntStat d_inst_duplicate_model_true;
     IntStat d_triggers;
     IntStat d_simple_triggers;
     IntStat d_multi_triggers;