Clean Ceg Instantiators (#1365)

* Initial setup for preprocessing counterexample lemmas.

* Improve documentation.

* Improving documentation, infrastructure.

* Extraction -> concatentation as a preprocess step.

* Clang format

* Minor

* Make option, refactor effort levels.

* Format

* Clean

* Format

* Rename

* Format

* More

* Format

* Splitting changes.

* Format

* Revert option.

* Minor

* Format

4 files changed, 1017 insertions, 407 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 36fac5e80..b41a3cfca 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -26,20 +26,35 @@
 #include "theory/theory_engine.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
 
-CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta, bool use_vts_inf ) :
-d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_vts_inf ){
-  d_is_nested_quant = false;
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+CegInstantiator::CegInstantiator(QuantifiersEngine* qe,
+                                 CegqiOutput* out,
+                                 bool use_vts_delta,
+                                 bool use_vts_inf)
+    : d_qe(qe),
+      d_out(out),
+      d_use_vts_delta(use_vts_delta),
+      d_use_vts_inf(use_vts_inf),
+      d_num_input_variables(0),
+      d_is_nested_quant(false),
+      d_effort(INST_EFFORT_NONE)
+{
 }
 
 CegInstantiator::~CegInstantiator() {
-  for( std::map< Node, Instantiator * >::iterator it = d_instantiator.begin(); it != d_instantiator.end(); ++it ){
-    delete it->second;
+  for (std::pair<Node, Instantiator*> inst : d_instantiator)
+  {
+    delete inst.second;
+  }
+  for (std::pair<TheoryId, InstantiatorPreprocess*> instp : d_tipp)
+  {
+    delete instp.second;
   }
 }
 
@@ -90,8 +105,8 @@ bool CegInstantiator::hasVariable( Node n, Node pv ) {
   return d_prog_var[n].find( pv )!=d_prog_var[n].end();
 }
 
-
-void CegInstantiator::registerInstantiationVariable( Node v, unsigned index ) {
+void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
+{
   if( d_instantiator.find( v )==d_instantiator.end() ){
     TypeNode tn = v.getType();
     Instantiator * vinst;
@@ -116,21 +131,82 @@ void CegInstantiator::registerInstantiationVariable( Node v, unsigned index ) {
   d_curr_index[v] = index;
 }
 
-void CegInstantiator::unregisterInstantiationVariable( Node v ) {
+void CegInstantiator::registerTheoryIds(TypeNode tn,
+                                        std::map<TypeNode, bool>& visited)
+{
+  if (visited.find(tn) == visited.end())
+  {
+    visited[tn] = true;
+    TheoryId tid = Theory::theoryOf(tn);
+    registerTheoryId(tid);
+    if (tn.isDatatype())
+    {
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+      {
+        for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
+        {
+          registerTheoryIds(
+              TypeNode::fromType(
+                  ((SelectorType)dt[i][j].getType()).getRangeType()),
+              visited);
+        }
+      }
+    }
+  }
+}
+
+void CegInstantiator::registerTheoryId(TheoryId tid)
+{
+  if (std::find(d_tids.begin(), d_tids.end(), tid) == d_tids.end())
+  {
+    // setup any theory-specific preprocessors here
+
+    d_tids.push_back(tid);
+  }
+}
+
+void CegInstantiator::registerVariable(Node v, bool is_aux)
+{
+  Assert(std::find(d_vars.begin(), d_vars.end(), v) == d_vars.end());
+  Assert(std::find(d_aux_vars.begin(), d_aux_vars.end(), v)
+         == d_aux_vars.end());
+  if (!is_aux)
+  {
+    d_vars.push_back(v);
+    d_vars_set.insert(v);
+  }
+  else
+  {
+    d_aux_vars.push_back(v);
+  }
+  TypeNode vtn = v.getType();
+  Trace("cbqi-proc-debug") << "Collect theory ids from type " << vtn << " of "
+                           << v << std::endl;
+  // collect relevant theories for this variable
+  std::map<TypeNode, bool> visited;
+  registerTheoryIds(vtn, visited);
+}
+
+void CegInstantiator::deactivateInstantiationVariable(Node v)
+{
   d_curr_subs_proc.erase( v );
   d_curr_index.erase( v );
 }
 
-bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){
+bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
+{
   if( i==d_vars.size() ){
     //solved for all variables, now construct instantiation
     bool needsPostprocess =
-        sf.d_vars.size() > d_vars.size() || !d_var_order_index.empty();
+        sf.d_vars.size() > d_num_input_variables || !d_var_order_index.empty();
     std::vector< Instantiator * > pp_inst;
     std::map< Instantiator *, Node > pp_inst_to_var;
     std::vector< Node > lemmas;
     for( std::map< Node, Instantiator * >::iterator ita = d_active_instantiators.begin(); ita != d_active_instantiators.end(); ++ita ){
-      if( ita->second->needsPostProcessInstantiationForVariable( this, sf, ita->first, effort ) ){
+      if (ita->second->needsPostProcessInstantiationForVariable(
+              this, sf, ita->first, d_effort))
+      {
         needsPostprocess = true;
         pp_inst_to_var[ ita->second ] = ita->first;
       }
@@ -140,7 +216,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
       SolvedForm sf_tmp = sf;
       bool postProcessSuccess = true;
       for( std::map< Instantiator *, Node >::iterator itp = pp_inst_to_var.begin(); itp != pp_inst_to_var.end(); ++itp ){
-        if( !itp->first->postProcessInstantiationForVariable( this, sf_tmp, itp->second, effort, lemmas ) ){
+        if (!itp->first->postProcessInstantiationForVariable(
+                this, sf_tmp, itp->second, d_effort, lemmas))
+        {
           postProcessSuccess = false;
           break;
         }
@@ -164,7 +242,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
       is_cv = true;
       d_stack_vars.pop_back();
     }
-    registerInstantiationVariable( pv, i );
+    activateInstantiationVariable(pv, i);
 
     //get the instantiator object
     Instantiator * vinst = NULL;
@@ -174,7 +252,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
     }
     Assert( vinst!=NULL );
     d_active_instantiators[pv] = vinst;
-    vinst->reset( this, sf, pv, effort );
+    vinst->reset(this, sf, pv, d_effort);
 
     TypeNode pvtn = pv.getType();
     TypeNode pvtnb = pvtn.getBaseType();
@@ -189,9 +267,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
       Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
     }
 
-    //if in effort=2, we must choose at least one model value
-    if( (i+1)<d_vars.size() || effort!=2 ){
-
+    // if d_effort is full, we must choose at least one model value
+    if ((i + 1) < d_vars.size() || d_effort != INST_EFFORT_FULL)
+    {
       //[1] easy case : pv is in the equivalence class as another term not containing pv
       Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
       std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
@@ -219,24 +297,29 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
                 proc = true;
               }
               if( proc ){
-                if( vinst->processEqualTerm( this, sf, pv, pv_prop, ns, effort ) ){
+                if (vinst->processEqualTerm(
+                        this, sf, pv, pv_prop, ns, d_effort))
+                {
                   return true;
                 }
               }
             }
           }
         }
-        if( vinst->processEqualTerms( this, sf, pv, it_eqc->second, effort ) ){
+        if (vinst->processEqualTerms(this, sf, pv, it_eqc->second, d_effort))
+        {
           return true;
         }
       }else{
         Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
       }
 
-      //[3] : we can solve an equality for pv
-      ///iterate over equivalence classes to find cases where we can solve for the variable
-      if( vinst->hasProcessEquality( this, sf, pv, effort ) ){
-        Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << std::endl;
+      //[2] : we can solve an equality for pv
+      /// iterate over equivalence classes to find cases where we can solve for
+      /// the variable
+      if (vinst->hasProcessEquality(this, sf, pv, d_effort))
+      {
+        Trace("cbqi-inst-debug") << "[2] try based on solving equalities." << std::endl;
         for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){
           Node r = d_curr_type_eqc[pvtnb][k];
           std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
@@ -272,7 +355,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
                     Trace("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl;
                     term_props.push_back( lhs_prop[j] );
                     terms.push_back( lhs[j] );
-                    if( vinst->processEquality( this, sf, pv, term_props, terms, effort ) ){
+                    if (vinst->processEquality(
+                            this, sf, pv, term_props, terms, d_effort))
+                    {
                       return true;
                     }
                     term_props.pop_back();
@@ -292,9 +377,10 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
         }
       }
 
-      //[4] directly look at assertions
-      if( vinst->hasProcessAssertion( this, sf, pv, effort ) ){
-        Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl;
+      //[3] directly look at assertions
+      if (vinst->hasProcessAssertion(this, sf, pv, d_effort))
+      {
+        Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
         std::unordered_set< Node, NodeHashFunction > lits;
         //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
         for( unsigned r=0; r<2; r++ ){
@@ -307,7 +393,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
               if( lits.find(lit)==lits.end() ){
                 lits.insert(lit);
                 Node plit =
-                    vinst->hasProcessAssertion(this, sf, pv, lit, effort);
+                    vinst->hasProcessAssertion(this, sf, pv, lit, d_effort);
                 if (!plit.isNull()) {
                   Trace("cbqi-inst-debug2") << "  look at " << lit;
                   if (plit != lit) {
@@ -320,8 +406,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
                     Trace("cbqi-inst-debug") << "...try based on literal " << slit << std::endl;
                     // check if contains pv
                     if( hasVariable( slit, pv ) ){
-                      if (vinst->processAssertion(this, sf, pv, slit, lit,
-                                                  effort)) {
+                      if (vinst->processAssertion(
+                              this, sf, pv, slit, lit, d_effort))
+                      {
                         return true;
                       }
                     }
@@ -331,16 +418,21 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
             }
           }
         }
-        if (vinst->processAssertions(this, sf, pv, effort)) {
+        if (vinst->processAssertions(this, sf, pv, d_effort))
+        {
           return true;
         }
       }
     }
 
-    //[5] resort to using value in model
-    // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype
-    bool use_model_value = vinst->useModelValue( this, sf, pv, effort );
-    if( ( effort>0 || use_model_value || is_cv ) && vinst->allowModelValue( this, sf, pv, effort ) ){
+    //[4] resort to using value in model. We do so if:
+    // - we are in a higher effort than INST_EFFORT_STANDARD,
+    // - if the variable is Boolean, or
+    // - if we are solving for a subfield of a datatype.
+    bool use_model_value = vinst->useModelValue(this, sf, pv, d_effort);
+    if ((d_effort > INST_EFFORT_STANDARD || use_model_value || is_cv)
+        && vinst->allowModelValue(this, sf, pv, d_effort))
+    {
 #ifdef CVC4_ASSERTIONS
       if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){
         Trace("cbqi-warn") << "Had to resort to model value." << std::endl;
@@ -349,18 +441,25 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
 #endif
       Node mv = getModelValue( pv );
       TermProperties pv_prop_m;
-      Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl;
-      int new_effort = use_model_value ? effort : 1;
-      if( doAddInstantiationInc( pv, mv, pv_prop_m, sf, new_effort ) ){
+      Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
+      InstEffort prev = d_effort;
+      if (!use_model_value)
+      {
+        // update the effort level to indicate we have used a model value
+        d_effort = INST_EFFORT_STANDARD_MV;
+      }
+      if (constructInstantiationInc(pv, mv, pv_prop_m, sf))
+      {
         return true;
       }
+      d_effort = prev;
     }
     Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
     if( is_cv ){
       d_stack_vars.push_back( pv );
     }
     d_active_instantiators.erase( pv );
-    unregisterInstantiationVariable( pv );
+    deactivateInstantiationVariable(pv);
     return false;
   }
 }
@@ -374,12 +473,11 @@ void CegInstantiator::popStackVariable() {
   d_stack_vars.pop_back();
 }
 
-bool CegInstantiator::doAddInstantiationInc(Node pv,
-                                            Node n,
-                                            TermProperties& pv_prop,
-                                            SolvedForm& sf,
-                                            unsigned effort,
-                                            bool revertOnSuccess)
+bool CegInstantiator::constructInstantiationInc(Node pv,
+                                                Node n,
+                                                TermProperties& pv_prop,
+                                                SolvedForm& sf,
+                                                bool revertOnSuccess)
 {
   Node cnode = pv_prop.getCacheNode();
   if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
@@ -470,7 +568,7 @@ bool CegInstantiator::doAddInstantiationInc(Node pv,
       sf.push_back( pv, n, pv_prop );
       Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
       unsigned i = d_curr_index[pv];
-      success = doAddInstantiation( sf, d_stack_vars.empty() ? i+1 : i, effort );
+      success = constructInstantiation(sf, d_stack_vars.empty() ? i + 1 : i);
       if (!success || revertOnSuccess)
       {
         Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
@@ -501,14 +599,16 @@ bool CegInstantiator::doAddInstantiationInc(Node pv,
 }
 
 bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) {
-  if( vars.size()>d_vars.size() ){
+  if (vars.size() > d_num_input_variables)
+  {
     Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
     std::map< Node, Node > subs_map;
     for( unsigned i=0; i<subs.size(); i++ ){
       subs_map[vars[i]] = subs[i];
     }
     subs.clear();
-    for( unsigned i=0; i<d_vars.size(); i++ ){
+    for (unsigned i = 0; i < d_vars.size(); i++)
+    {
       std::map< Node, Node >::iterator it = subs_map.find( d_vars[i] );
       Assert( it!=subs_map.end() );
       Node n = it->second;
@@ -516,14 +616,18 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector
       subs.push_back( n );
     }
   }
+  Trace("cbqi-inst-debug") << "Sort based on order...." << std::endl;
   if( !d_var_order_index.empty() ){
     std::vector< Node > subs_orig;
     subs_orig.insert( subs_orig.end(), subs.begin(), subs.end() );
     subs.clear();
     for( unsigned i=0; i<subs_orig.size(); i++ ){
+      Assert(d_var_order_index[i]<subs_orig.size());
       subs.push_back( subs_orig[d_var_order_index[i]] );
     }
   }
+  subs.resize(d_num_input_variables);
+  Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl;
   bool ret = d_out->doAddInstantiation( subs );
   for( unsigned i=0; i<lemmas.size(); i++ ){
     d_out->addLemma( lemmas[i] );
@@ -714,11 +818,13 @@ bool CegInstantiator::check() {
   }
   processAssertions();
   for( unsigned r=0; r<2; r++ ){
+    d_effort = r == 0 ? INST_EFFORT_STANDARD : INST_EFFORT_FULL;
     SolvedForm sf;
     d_stack_vars.clear();
     d_bound_var_index.clear();
     //try to add an instantiation
-    if( doAddInstantiation( sf, 0, r==0 ? 0 : 2 ) ){
+    if (constructInstantiation(sf, 0))
+    {
       return true;
     }
   }
@@ -792,25 +898,6 @@ void CegInstantiator::presolve( Node q ) {
   }
 }
 
-void collectTheoryIds( TypeNode tn, std::map< TypeNode, bool >& visited, std::vector< TheoryId >& tids ){
-  std::map< TypeNode, bool >::iterator itt = visited.find( tn );
-  if( itt==visited.end() ){
-    visited[tn] = true;
-    TheoryId tid = Theory::theoryOf( tn );
-    if( std::find( tids.begin(), tids.end(), tid )==tids.end() ){
-      tids.push_back( tid );
-    }
-    if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-        for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-          collectTheoryIds( TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ), visited, tids );
-        }
-      }
-    }
-  }
-}
-
 void CegInstantiator::processAssertions() {
   Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl;
   d_curr_asserts.clear();
@@ -1045,36 +1132,15 @@ struct sortCegVarOrder {
 
 
 void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
+  Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl;
   //Assert( d_vars.empty() );
   d_vars.clear();
-  d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
-  d_vars_set.insert(ce_vars.begin(), ce_vars.end());
-
-  //determine variable order: must do Reals before Ints
-  if( !d_vars.empty() ){
-    TypeNode tn0 = d_vars[0].getType();
-    bool doSort = false;
-    std::map< Node, unsigned > voo;
-    for( unsigned i=0; i<d_vars.size(); i++ ){
-      voo[d_vars[i]] = i;
-      d_var_order_index.push_back( 0 );
-      if( d_vars[i].getType()!=tn0 ){
-        doSort = true;
-      }
-    }
-    if( doSort ){
-      Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl;
-      sortCegVarOrder scvo;
-      std::sort( d_vars.begin(), d_vars.end(), scvo );
-      Trace("cbqi-debug") << "Consider variables in this order : " << std::endl;
-      for( unsigned i=0; i<d_vars.size(); i++ ){
-        d_var_order_index[voo[d_vars[i]]] = i;
-        Trace("cbqi-debug") << "  " << d_vars[i] << " : " << d_vars[i].getType() << ", index was : " << voo[d_vars[i]] << std::endl;
-      }
-      Trace("cbqi-debug") << std::endl;
-    }else{
-      d_var_order_index.clear();
-    }
+  d_num_input_variables = ce_vars.size();
+  registerTheoryId(THEORY_UF);
+  for (unsigned i = 0; i < ce_vars.size(); i++)
+  {
+    Trace("cbqi-reg") << "  register input variable : " << ce_vars[i] << std::endl;
+    registerVariable(ce_vars[i]);
   }
 
   //remove ITEs
@@ -1084,8 +1150,8 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   d_aux_vars.clear();
   d_aux_eq.clear();
   for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
-    Trace("cbqi-debug") << "  Auxiliary var (from ITE) : " << i->first << std::endl;
-    d_aux_vars.push_back( i->first );
+    Trace("cbqi-reg") << "  register aux variable : " << i->first << std::endl;
+    registerVariable(i->first, true);
   }
   for( unsigned i=0; i<lems.size(); i++ ){
     Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
@@ -1114,27 +1180,71 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     }*/
     lems[i] = rlem;
   }
+
+  // preprocess with all relevant instantiator preprocessors
+  Trace("cbqi-debug") << "Preprocess based on theory-specific methods..."
+                      << std::endl;
+  std::vector<Node> pvars;
+  pvars.insert(pvars.end(), d_vars.begin(), d_vars.end());
+  for (std::map<TheoryId, InstantiatorPreprocess*>::iterator it =
+           d_tipp.begin();
+       it != d_tipp.end();
+       ++it)
+  {
+    it->second->registerCounterexampleLemma(lems, pvars);
+  }
+  // must register variables generated by preprocessors
+  Trace("cbqi-debug") << "Register variables from theory-specific methods "
+                      << d_num_input_variables << " " << d_vars.size() << " ..."
+                      << std::endl;
+  for (unsigned i = d_num_input_variables; i < pvars.size(); i++)
+  {
+    Trace("cbqi-reg") << "  register theory preprocess variable : " << pvars[i] << std::endl;
+    registerVariable(pvars[i]);
+  }
+
+  // determine variable order: must do Reals before Ints
+  Trace("cbqi-debug") << "Determine variable order..." << std::endl;
+  if (!d_vars.empty())
+  {
+    TypeNode tn0 = d_vars[0].getType();
+    bool doSort = false;
+    std::map<Node, unsigned> voo;
+    for (unsigned i = 0; i < d_vars.size(); i++)
+    {
+      voo[d_vars[i]] = i;
+      d_var_order_index.push_back(0);
+      if (d_vars[i].getType() != tn0)
+      {
+        doSort = true;
+      }
+    }
+    if (doSort)
+    {
+      Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl;
+      sortCegVarOrder scvo;
+      std::sort(d_vars.begin(), d_vars.end(), scvo);
+      Trace("cbqi-debug") << "Consider variables in this order : " << std::endl;
+      for (unsigned i = 0; i < d_vars.size(); i++)
+      {
+        d_var_order_index[voo[d_vars[i]]] = i;
+        Trace("cbqi-debug") << "  " << d_vars[i] << " : " << d_vars[i].getType()
+                            << ", index was : " << voo[d_vars[i]] << std::endl;
+      }
+      Trace("cbqi-debug") << std::endl;
+    }
+    else
+    {
+      d_var_order_index.clear();
+    }
+  }
+
   //collect atoms from all lemmas: we will only do bounds coming from original body
   d_is_nested_quant = false;
   std::map< Node, bool > visited;
   for( unsigned i=0; i<lems.size(); i++ ){
     collectCeAtoms( lems[i], visited );
   }
-
-  //compute the theory ids
-  d_tids.clear();
-  d_tids.push_back(THEORY_UF);
-  for( unsigned r=0; r<2; r++ ){
-    unsigned sz = r==0 ? d_vars.size() : d_aux_vars.size();
-    for( unsigned i=0; i<sz; i++ ){
-      Node pv = r==0 ? d_vars[i] : d_aux_vars[i];
-      TypeNode pvtn = pv.getType();
-      Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
-      //collect relevant theories
-      std::map< TypeNode, bool > visited;
-      collectTheoryIds( pvtn, visited, d_tids );
-    }
-  }
 }
 
 
@@ -1142,10 +1252,17 @@ Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn )
   d_closed_enum_type = qe->getTermEnumeration()->isClosedEnumerableType(tn);
 }
 
-
-bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) {
+bool Instantiator::processEqualTerm(CegInstantiator* ci,
+                                    SolvedForm& sf,
+                                    Node pv,
+                                    TermProperties& pv_prop,
+                                    Node n,
+                                    InstEffort effort)
+{
   pv_prop.d_type = 0;
-  return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort );
+  return ci->constructInstantiationInc(pv, n, pv_prop, sf);
 }
 
-
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 1e59bfb43..bf5a37026 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -39,10 +39,14 @@ public:
 };
 
 class Instantiator;
+class InstantiatorPreprocess;
 
 /** Term Properties
- * stores properties for a variable to solve for in CEGQI
- *  For LIA, this includes the coefficient of the variable, and the bound type
+ *
+ * Stores properties for a variable to solve for in counterexample-guided
+ * instantiation.
+ *
+ * For LIA, this includes the coefficient of the variable, and the bound type
  * for the variable.
  */
 class TermProperties {
@@ -53,8 +57,9 @@ public:
   int d_type;
   // for arithmetic
   Node d_coeff;
-  // get cache node 
-  // we consider terms + TermProperties that are unique up to their cache node (see doAddInstantiationInc)
+  // get cache node
+  // we consider terms + TermProperties that are unique up to their cache node
+  // (see constructInstantiationInc)
   virtual Node getCacheNode() const { return d_coeff; }
   // is non-basic 
   virtual bool isBasic() const { return d_coeff.isNull(); }
@@ -138,12 +143,126 @@ public:
   }
 };
 
+/** instantiation effort levels */
+enum InstEffort
+{
+  // uninitialized
+  INST_EFFORT_NONE,
+  // standard effort level
+  INST_EFFORT_STANDARD,
+  // standard effort level, but we have used model values
+  INST_EFFORT_STANDARD_MV,
+  // full effort level
+  INST_EFFORT_FULL
+};
+
 /** Ceg instantiator
  *
  * This class manages counterexample-guided quantifier instantiation
  * for a single quantified formula.
+ *
+ * For details on counterexample-guided quantifier instantiation
+ * (for linear arithmetic), see Reynolds/King/Kuncak FMSD 2017.
  */
 class CegInstantiator {
+ public:
+  CegInstantiator(QuantifiersEngine* qe,
+                  CegqiOutput* out,
+                  bool use_vts_delta = true,
+                  bool use_vts_inf = true);
+  virtual ~CegInstantiator();
+  /** check
+   * This adds instantiations based on the state of d_vars in current context
+   * on the output channel d_out of this class.
+   */
+  bool check();
+  /** presolve for quantified formula
+   *
+   * This initializes formulas that help static learning of the quantifier-free
+   * solver. It is only called if the option --cbqi-prereg-inst is used.
+   */
+  void presolve(Node q);
+  /** Register the counterexample lemma
+   *
+   * lems : contains the conjuncts of the counterexample lemma of the
+   *        quantified formula we are processing. The counterexample
+   *        lemma is the formula { ~phi[e/x] } in Figure 1 of Reynolds
+   *        et al. FMSD 2017.
+   * ce_vars : contains the variables e. Notice these are variables of
+   *           INST_CONSTANT kind, since we do not permit bound
+   *           variables in assertions.
+   *
+   * This method may modify the set of lemmas lems based on:
+   * - ITE removal,
+   * - Theory-specific preprocessing of instantiation lemmas.
+   * It may also introduce new variables to ce_vars if necessary.
+   */
+  void registerCounterexampleLemma(std::vector<Node>& lems,
+                                   std::vector<Node>& ce_vars);
+  /** get the output channel of this class */
+  CegqiOutput* getOutput() { return d_out; }
+  //------------------------------interface for instantiators
+  /** get quantifiers engine */
+  QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
+  /** push stack variable
+   * This adds a new variable to solve for in the stack
+   * of variables we are processing. This stack is only
+   * used for datatypes, where e.g. the DtInstantiator
+   * solving for a list x may push the stack "variables"
+   * head(x) and tail(x).
+   */
+  void pushStackVariable(Node v);
+  /** pop stack variable */
+  void popStackVariable();
+  /** construct instantiation increment
+   *
+   * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current
+   * instantiation, specified by sf.
+   *
+   * This function returns true if a call to
+   * QuantifiersEngine::addInstantiation(...)
+   * was successfully made in a recursive call.
+   *
+   * The solved form sf is reverted to its original state if
+   *   this function returns false, or
+   *   revertOnSuccess is true and this function returns true.
+   */
+  bool constructInstantiationInc(Node pv,
+                                 Node n,
+                                 TermProperties& pv_prop,
+                                 SolvedForm& sf,
+                                 bool revertOnSuccess = false);
+  /** get the current model value of term n */
+  Node getModelValue(Node n);
+  /** get bound variable for type
+   *
+   * This gets the next (canonical) bound variable of
+   * type tn. This can be used for instance when
+   * constructing instantiations that involve choice expressions.
+   */
+  Node getBoundVariable(TypeNode tn);
+  //------------------------------end interface for instantiators
+
+  /**
+   * Get the number of atoms in the counterexample lemma of the quantified
+   * formula we are processing with this class.
+   */
+  unsigned getNumCEAtoms() { return d_ce_atoms.size(); }
+  /**
+   * Get the i^th atom of the counterexample lemma of the quantified
+   * formula we are processing with this class.
+   */
+  Node getCEAtom(unsigned i) { return d_ce_atoms[i]; }
+  /** is n a term that is eligible for instantiation? */
+  bool isEligible(Node n);
+  /** does n have variable pv? */
+  bool hasVariable(Node n, Node pv);
+  /** are we using delta for LRA virtual term substitution? */
+  bool useVtsDelta() { return d_use_vts_delta; }
+  /** are we using infinity for LRA virtual term substitution? */
+  bool useVtsInfinity() { return d_use_vts_inf; }
+  /** are we processing a nested quantified formula? */
+  bool hasNestedQuantification() { return d_is_nested_quant; }
  private:
   /** quantified formula associated with this instantiator */
   QuantifiersEngine* d_qe;
@@ -157,6 +276,8 @@ class CegInstantiator {
     * (for quantified LRA).
     */
   bool d_use_vts_inf;
+
+  //-------------------------------globally cached
   /** cache from nodes to the set of variables it contains
     * (from the quantified formula we are instantiating).
     */
@@ -168,25 +289,88 @@ class CegInstantiator {
    * ineligible for instantiation.
     */
   std::unordered_set<Node, NodeHashFunction> d_inelig;
+  /** ensures n is in d_prog_var and d_inelig. */
+  void computeProgVars(Node n);
+  //-------------------------------end globally cached
+
+  //-------------------------------cached per round
   /** current assertions per theory */
   std::map<TheoryId, std::vector<Node> > d_curr_asserts;
   /** map from representatives to the terms in their equivalence class */
   std::map<Node, std::vector<Node> > d_curr_eqc;
   /** map from types to representatives of that type */
   std::map<TypeNode, std::vector<Node> > d_curr_type_eqc;
-  /** auxiliary variables
-   * These variables include the result of removing ITE
-   * terms from the quantified formula we are processing.
-   * These variables must be eliminated from constraints
-   * as a preprocess step to check().
+  /** process assertions
+   * This is called once at the beginning of check to
+   * set up all necessary information for constructing instantiations,
+   * such as the above data structures.
    */
-  std::vector<Node> d_aux_vars;
+  void processAssertions();
+  /** add to auxiliary variable substitution
+   * This adds the substitution l -> r to the auxiliary
+   * variable substitution subs_lhs -> subs_rhs, and serializes
+   * it (applies it to existing substitutions).
+   */
+  void addToAuxVarSubstitution(std::vector<Node>& subs_lhs,
+                               std::vector<Node>& subs_rhs,
+                               Node l,
+                               Node r);
+  /** cache bound variables for type returned
+   * by getBoundVariable(...).
+   */
+  std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
+      d_bound_var;
+  /** current index of bound variables for type.
+   * The next call to getBoundVariable(...) for
+   * type tn returns the d_bound_var_index[tn]^th
+   * element of d_bound_var[tn], or a fresh variable
+   * if not in bounds.
+   */
+  std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>
+      d_bound_var_index;
+  //-------------------------------end cached per round
+
+  //-------------------------------data per theory
   /** relevant theory ids
    * A list of theory ids that contain at least one
    * constraint in the body of the quantified formula we
    * are processing.
    */
   std::vector<TheoryId> d_tids;
+  /** map from theory ids to instantiator preprocessors */
+  std::map<TheoryId, InstantiatorPreprocess*> d_tipp;
+  /** registers all theory ids associated with type tn
+   *
+   * This recursively calls registerTheoryId for typeOf(tn') for
+   * all parameters and datatype subfields of type tn.
+   * visited stores the types we have already visited.
+   */
+  void registerTheoryIds(TypeNode tn, std::map<TypeNode, bool>& visited);
+  /** register theory id tid
+   *
+   * This is called when the quantified formula we are processing
+   * with this class involves theory tid. In this case, we will
+   * construct instantiations based on the assertion list of this theory.
+   */
+  void registerTheoryId(TheoryId tid);
+  //-------------------------------end data per theory
+
+  //-------------------------------the variables
+  /** the variables we are instantiating
+   * For a quantified formula with n variables,
+   * the first n terms in d_vars are the instantiation
+   * constants corresponding to these variables.
+   */
+  std::vector<Node> d_vars;
+  /** set form of d_vars */
+  std::unordered_set<Node, NodeHashFunction> d_vars_set;
+  /** index of variables reported in instantiation */
+  std::vector<unsigned> d_var_order_index;
+  /** number of input variables
+   * This is n for quantified formulas with n variables,
+   * and is at most the size of d_vars.
+   */
+  unsigned d_num_input_variables;
   /** literals to equalities for aux vars
    * This stores entries of the form
    *   L -> ( k -> t )
@@ -207,59 +391,64 @@ class CegInstantiator {
    * k=t1 and k=t2 respectively.
    */
   std::map<Node, std::map<Node, Node> > d_aux_eq;
-  /** the variables we are instantiating
-   * These are the inst constants of the quantified formula
-   * we are processing.
+  /** auxiliary variables
+   * These variables include the result of removing ITE
+   * terms from the quantified formula we are processing.
+   * These variables must be eliminated from constraints
+   * as a preprocess step to check().
    */
-  std::vector<Node> d_vars;
-  /** set form of d_vars */
-  std::unordered_set<Node, NodeHashFunction> d_vars_set;
-  /** index of variables reported in instantiation */
-  std::vector<unsigned> d_var_order_index;
-  /** are we handled a nested quantified formula? */
+  std::vector<Node> d_aux_vars;
+  /** register variable */
+  void registerVariable(Node v, bool is_aux = false);
+  //-------------------------------the variables
+
+  //-------------------------------quantified formula info
+  /** are we processing a nested quantified formula? */
   bool d_is_nested_quant;
   /** the atoms of the CE lemma */
   std::vector<Node> d_ce_atoms;
-  /** cache bound variables for type returned
-   * by getBoundVariable(...).
-   */
-  std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
-      d_bound_var;
-  /** current index of bound variables for type.
-   * The next call to getBoundVariable(...) for
-   * type tn returns the d_bound_var_index[tn]^th
-   * element of d_bound_var[tn], or a fresh variable
-   * if not in bounds.
-   */
-  std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>
-      d_bound_var_index;
   /** collect atoms */
   void collectCeAtoms(Node n, std::map<Node, bool>& visited);
+  //-------------------------------end quantified formula info
 
- private:
-  //map from variables to their instantiators
-  std::map< Node, Instantiator * > d_instantiator;
-  //cache of current substitutions tried between register/unregister
-  std::map< Node, std::map< Node, std::map< Node, bool > > > d_curr_subs_proc;
-  std::map< Node, unsigned > d_curr_index;
-  //stack of temporary variables we are solving (e.g. subfields of datatypes)
-  std::vector< Node > d_stack_vars;
+  //-------------------------------current state
+  /** the current effort level of the instantiator
+   * This indicates the effort Instantiator objects
+   * will put into the terms they return.
+   */
+  InstEffort d_effort;
   /** for each variable, the instantiator used for that variable */
-  std::map< Node, Instantiator * > d_active_instantiators;
-  //register variable
-  void registerInstantiationVariable( Node v, unsigned index );
-  void unregisterInstantiationVariable( Node v );
-private:
-  //for adding instantiations during check
-  void computeProgVars( Node n );
-  // effort=0 : do not use model value, 1: use model value, 2: one must use model value
-  bool doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort );
-  // called by the above function after we finalize the variables/substitution and auxiliary lemmas
-  bool doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas );
-  //process
-  void processAssertions();
-  void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r );
-private:
+  std::map<Node, Instantiator*> d_active_instantiators;
+  /** map from variables to the index in the prefix of the quantified
+   * formula we are processing.
+   */
+  std::map<Node, unsigned> d_curr_index;
+  /** cache of current substitutions tried between activate/deactivate */
+  std::map<Node, std::map<Node, std::map<Node, bool> > > d_curr_subs_proc;
+  /** stack of temporary variables we are solving for,
+   * e.g. subfields of datatypes.
+   */
+  std::vector<Node> d_stack_vars;
+  /** activate instantiation variable v at index
+   *
+   * This is called when variable (inst constant) v is activated
+   * for the quantified formula we are processing.
+   * This method initializes the instantiator class for
+   * that variable if necessary, where this class is
+   * determined by the type of v. It also initializes
+   * the cache of values we have tried substituting for v
+   * (in d_curr_subs_proc), and stores its index.
+   */
+  void activateInstantiationVariable(Node v, unsigned index);
+  /** deactivate instantiation variable
+   *
+   * This is called when variable (inst constant) v is deactivated
+   * for the quantified formula we are processing.
+   */
+  void deactivateInstantiationVariable(Node v);
+  //-------------------------------end current state
+
+  //---------------------------------for applying substitutions
   /** can use basic substitution */
   bool canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic );
   /** apply substitution
@@ -285,170 +474,268 @@ private:
   /** apply substitution to literal lit, with solved form expanded to subs/prop/non_basic/vars */
   Node applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, 
                                    std::vector< Node >& non_basic );
+  //---------------------------------end for applying substitutions
+
+  /** map from variables to their instantiators */
+  std::map<Node, Instantiator*> d_instantiator;
+
+  /** construct instantiation
+   * This method constructs the current instantiation, where we
+   * are currently processing the i^th variable in d_vars.
+   * It returns true if a successful call to the output channel's
+   * doAddInstantiation was made.
+   */
+  bool constructInstantiation(SolvedForm& sf, unsigned i);
+  /** do add instantiation
+   * This method is called by the above function after we finalize the
+   * variables/substitution and auxiliary lemmas.
+   * It returns true if a successful call to the output channel's
+   * doAddInstantiation was made.
+   */
+  bool doAddInstantiation(std::vector<Node>& vars,
+                          std::vector<Node>& subs,
+                          std::vector<Node>& lemmas);
+};
+
+/** Instantiator class
+ *
+ * This is a virtual class that is used for methods for constructing
+ * substitutions for individual variables in counterexample-guided
+ * instantiation techniques.
+ *
+ * This class contains a set of interface functions below, which are called
+ * based on a fixed instantiation method implemented by CegInstantiator.
+ * In these calls, the Instantiator in turn makes calls to methods in
+ * CegInstanatior (primarily constructInstantiationInc).
+ */
+class Instantiator {
 public:
-  CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true );
-  virtual ~CegInstantiator();
-  //check : add instantiations based on valuation of d_vars
-  bool check();
-  //presolve for quantified formula
-  void presolve( Node q );
-  //register the counterexample lemma (stored in lems), modify vector
-  void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars );
-  //output
-  CegqiOutput * getOutput() { return d_out; }
-  //get quantifiers engine
-  QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
-  //------------------------------interface for instantiators
-  /** push stack variable
-   * This adds a new variable to solve for in the stack
-   * of variables we are processing. This stack is only
-   * used for datatypes, where e.g. the DtInstantiator
-   * solving for a list x may push the stack "variables"
-   * head(x) and tail(x).
+  Instantiator( QuantifiersEngine * qe, TypeNode tn );
+  virtual ~Instantiator(){}
+  /** reset
+   * This is called once, prior to any of the below methods are called.
+   * This function sets up any initial information necessary for constructing
+   * instantiations for pv based on the current context.
    */
-  void pushStackVariable( Node v );
-  /** pop stack variable */
-  void popStackVariable();
-  /** do add instantiation increment
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     InstEffort effort)
+  {
+  }
+
+  /** process equal term
    *
-   * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current
-   * instantiation, specified by sf.
+   * This method is called when the entailment:
+   *   E |= pv_prop.getModifiedTerm(pv) = n
+   * holds in the current context E, and n is eligible for instantiation.
    *
-   * This function returns true if a call to
-   * QuantifiersEngine::addInstantiation(...)
-   * was successfully made in a recursive call.
-   *
-   * The solved form sf is reverted to its original state if
-   *   this function returns false, or
-   *   revertOnSuccess is true and this function returns true.
+   * Returns true if an instantiation was successfully added via a call to
+   * CegInstantiator::constructInstantiationInc.
    */
-  bool doAddInstantiationInc(Node pv,
-                             Node n,
-                             TermProperties& pv_prop,
-                             SolvedForm& sf,
-                             unsigned effort,
-                             bool revertOnSuccess = false);
-  /** get the current model value of term n */
-  Node getModelValue( Node n );
-  /** get bound variable for type
+  virtual bool processEqualTerm(CegInstantiator* ci,
+                                SolvedForm& sf,
+                                Node pv,
+                                TermProperties& pv_prop,
+                                Node n,
+                                InstEffort effort);
+  /** process equal terms
    *
-   * This gets the next (canonical) bound variable of
-   * type tn. This can be used for instance when
-   * constructing instantiations that involve choice expressions.
+   * This method is called after process equal term, where eqc is the list of
+   * eligible terms in the equivalence class of pv.
+   *
+   * Returns true if an instantiation was successfully added via a call to
+   * CegInstantiator::constructInstantiationInc.
    */
-  Node getBoundVariable(TypeNode tn);
-  //------------------------------end interface for instantiators
-  unsigned getNumCEAtoms() { return d_ce_atoms.size(); }
-  Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; }
-  /** is n a term that is eligible for instantiation? */
-  bool isEligible( Node n );
-  /** does n have variable pv? */
-  bool hasVariable( Node n, Node pv );
-  /** are we using delta for LRA virtual term substitution? */
-  bool useVtsDelta() { return d_use_vts_delta; }
-  /** are we using infinity for LRA virtual term substitution? */
-  bool useVtsInfinity() { return d_use_vts_inf; }
-  /** are we processing a nested quantified formula? */
-  bool hasNestedQuantification() { return d_is_nested_quant; }
-};
+  virtual bool processEqualTerms(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 std::vector<Node>& eqc,
+                                 InstEffort effort)
+  {
+    return false;
+  }
 
+  /** whether the instantiator implements processEquality */
+  virtual bool hasProcessEquality(CegInstantiator* ci,
+                                  SolvedForm& sf,
+                                  Node pv,
+                                  InstEffort effort)
+  {
+    return false;
+  }
+  /** process equality
+   *  The input is such that term_props.size() = terms.size() = 2
+   *  This method is called when the entailment:
+   *    E ^ term_props[0].getModifiedTerm(x0) =
+   *    terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1
+   *  holds in current context E for fresh variables xi, terms[i] are eligible,
+   *  and at least one terms[i] contains pv for i = 0,1.
+   *  Notice in the basic case, E |= terms[0] = terms[1].
+   *
+   *  Returns true if an instantiation was successfully added via a call to
+   *  CegInstantiator::constructInstantiationInc.
+   */
+  virtual bool processEquality(CegInstantiator* ci,
+                               SolvedForm& sf,
+                               Node pv,
+                               std::vector<TermProperties>& term_props,
+                               std::vector<Node>& terms,
+                               InstEffort effort)
+  {
+    return false;
+  }
 
-// an instantiator for individual variables
-//   will make calls into CegInstantiator::doAddInstantiationInc
-class Instantiator {
-protected:
-  TypeNode d_type;
-  bool d_closed_enum_type;
-public:
-  Instantiator( QuantifiersEngine * qe, TypeNode tn );
-  virtual ~Instantiator(){}
-  virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {}
-
-  //  Called when the entailment:
-  //    E |= pv_prop.getModifiedTerm(pv) = n
-  //  holds in the current context E, and n is eligible for instantiation.
-  virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort );
-  //  Called about process equal term, where eqc is the list of eligible terms in the equivalence class of pv
-  virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; }
-
-  // whether the instantiator implements processEquality
-  virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
-  //  term_props.size() = terms.size() = 2
-  //  Called when the entailment:
-  //    E ^ term_props[0].getModifiedTerm(x0) = terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1
-  //  holds in current context E for fresh variables xi, terms[i] are eligible, and at least one terms[i] contains pv for i = 0,1.
-  //  Notice in the basic case, E |= terms[0] = terms[1].
-  //  Returns true if an instantiation was successfully added via a recursive call
-  virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { return false; }
-
-  // whether the instantiator implements processAssertion for any literal
-  virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  /** whether the instantiator implements processAssertion for any literal */
+  virtual bool hasProcessAssertion(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   InstEffort effort)
+  {
+    return false;
+  }
   /** has process assertion
   *
-  * Called when the entailment:
+  * This method is called when the entailment:
   *   E |= lit
   * holds in current context E. Typically, lit belongs to the list of current
   * assertions.
   *
-  * This function is used to determine whether the instantiator implements
+  * This method is used to determine whether the instantiator implements
   * processAssertion for literal lit.
-  *   If this function returns null, then this intantiator does not handle the
-  * literal lit
-  *   Otherwise, this function returns a literal lit' with the properties:
+  *   If this method returns null, then this intantiator does not handle the
+  *   literal lit. Otherwise, this method returns a literal lit' such that:
   *   (1) lit' is true in the current model,
   *   (2) lit' implies lit.
   *   where typically lit' = lit.
   */
-  virtual Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv,
-                                   Node lit, unsigned effort) {
+  virtual Node hasProcessAssertion(
+      CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort)
+  {
     return Node::null();
   }
   /** process assertion
-  * Processes the assertion slit for variable pv
-  *
-  * lit is the substituted form (under sf) of a literal returned by
-  * hasProcessAssertion
-  * alit is the asserted literal, given as input to hasProcessAssertion
-  *
-  * Returns true if an instantiation was successfully added via a recursive call
-  */
-  virtual bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv,
-                                Node lit, Node alit, unsigned effort) {
+   * This method processes the assertion slit for variable pv.
+   * lit : the substituted form (under sf) of a literal returned by
+   *       hasProcessAssertion
+   * alit : the asserted literal, given as input to hasProcessAssertion
+   *
+   *  Returns true if an instantiation was successfully added via a call to
+   *  CegInstantiator::constructInstantiationInc.
+   */
+  virtual bool processAssertion(CegInstantiator* ci,
+                                SolvedForm& sf,
+                                Node pv,
+                                Node lit,
+                                Node alit,
+                                InstEffort effort)
+  {
     return false;
   }
   /** process assertions
-  * Called after processAssertion is called for each literal asserted to the
-  * instantiator.
-  */
-  virtual bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv,
-                                 unsigned effort) {
+   *
+   * Called after processAssertion is called for each literal asserted to the
+   * instantiator.
+   *
+   * Returns true if an instantiation was successfully added via a call to
+   * CegInstantiator::constructInstantiationInc.
+   */
+  virtual bool processAssertions(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 InstEffort effort)
+  {
     return false;
   }
 
-  //do we use the model value as instantiation for pv
-  virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
-  //do we allow the model value as instantiation for pv
-  virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; }
+  /** do we use the model value as instantiation for pv?
+   * This method returns true if we use model value instantiations
+   * at the same effort level as those determined by this instantiator.
+   */
+  virtual bool useModelValue(CegInstantiator* ci,
+                             SolvedForm& sf,
+                             Node pv,
+                             InstEffort effort)
+  {
+    return false;
+  }
+  /** do we allow the model value as instantiation for pv? */
+  virtual bool allowModelValue(CegInstantiator* ci,
+                               SolvedForm& sf,
+                               Node pv,
+                               InstEffort effort)
+  {
+    return d_closed_enum_type;
+  }
 
-  //do we need to postprocess the solved form for pv?
-  virtual bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
-  //postprocess the solved form for pv, returns true if we successfully postprocessed, lemmas is a set of lemmas we wish to return along with the instantiation
-  virtual bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ) { return true; }
+  /** do we need to postprocess the solved form for pv? */
+  virtual bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
+                                                        SolvedForm& sf,
+                                                        Node pv,
+                                                        InstEffort effort)
+  {
+    return false;
+  }
+  /** postprocess the solved form for pv
+   *
+   * This method returns true if we successfully postprocessed the solved form.
+   * lemmas is a set of lemmas we wish to return along with the instantiation.
+   */
+  virtual bool postProcessInstantiationForVariable(CegInstantiator* ci,
+                                                   SolvedForm& sf,
+                                                   Node pv,
+                                                   InstEffort effort,
+                                                   std::vector<Node>& lemmas)
+  {
+    return true;
+  }
 
   /** Identify this module (for debugging) */
   virtual std::string identify() const { return "Default"; }
+ protected:
+  /** the type of the variable we are instantiating */
+  TypeNode d_type;
+  /** whether d_type is a closed enumerable type */
+  bool d_closed_enum_type;
 };
 
 class ModelValueInstantiator : public Instantiator {
 public:
   ModelValueInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
   virtual ~ModelValueInstantiator(){}
-  bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  bool useModelValue(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     InstEffort effort)
+  {
+    return true;
+  }
   std::string identify() const { return "ModelValue"; }
 };
 
-}
-}
-}
+/** instantiator preprocess
+ *
+ * This class implements techniques for preprocessing the counterexample lemma
+ * generated for counterexample-guided quantifier instantiation.
+ */
+class InstantiatorPreprocess
+{
+ public:
+  InstantiatorPreprocess() {}
+  virtual ~InstantiatorPreprocess() {}
+  /** register counterexample lemma
+   * This implements theory-specific preprocessing and registration
+   * of counterexample lemmas, with the same contract as
+   * CegInstantiation::registerCounterexampleLemma.
+   */
+  virtual void registerCounterexampleLemma(std::vector<Node>& lems,
+                                           std::vector<Node>& ce_vars)
+  {
+  }
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
 
 #endif
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index e16286fa9..7502d42f1 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -31,11 +31,12 @@
 #include <stack>
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) {
   Node val = t;
@@ -214,7 +215,11 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
   return ires;
 }
 
-void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+void ArithInstantiator::reset(CegInstantiator* ci,
+                              SolvedForm& sf,
+                              Node pv,
+                              InstEffort effort)
+{
   d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type, false, false );
   d_vts_sym[1] = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta( false, false );
   for( unsigned i=0; i<2; i++ ){
@@ -227,7 +232,13 @@ void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, un
   }
 }
 
-bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
+bool ArithInstantiator::processEquality(CegInstantiator* ci,
+                                        SolvedForm& sf,
+                                        Node pv,
+                                        std::vector<TermProperties>& term_props,
+                                        std::vector<Node>& terms,
+                                        InstEffort effort)
+{
   Node eq_lhs = terms[0];
   Node eq_rhs = terms[1];
   Node lhs_coeff = term_props[0].d_coeff;
@@ -255,7 +266,8 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N
   int ires = solve_arith( ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta );
   if( ires!=0 ){
     pv_prop.d_type = 0;
-    if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){
+    if (ci->constructInstantiationInc(pv, val, pv_prop, sf))
+    {
       return true;
     }
   }
@@ -263,9 +275,9 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N
   return false;
 }
 
-Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
-                                            Node pv, Node lit,
-                                            unsigned effort) {
+Node ArithInstantiator::hasProcessAssertion(
+    CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort)
+{
   Node atom = lit.getKind()==NOT ? lit[0] : lit;
   bool pol = lit.getKind()!=NOT;
   //arithmetic inequalities and disequalities
@@ -277,9 +289,13 @@ Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
   }
 }
 
-bool ArithInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf,
-                                         Node pv, Node lit, Node alit,
-                                         unsigned effort) {
+bool ArithInstantiator::processAssertion(CegInstantiator* ci,
+                                         SolvedForm& sf,
+                                         Node pv,
+                                         Node lit,
+                                         Node alit,
+                                         InstEffort effort)
+{
   Node atom = lit.getKind()==NOT ? lit[0] : lit;
   bool pol = lit.getKind()!=NOT;
   //arithmetic inequalities and disequalities
@@ -383,7 +399,8 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf,
       }else{
         //try this bound
         pv_prop.d_type = uires>0 ? 1 : -1;
-        if( ci->doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){
+        if (ci->constructInstantiationInc(pv, uval, pv_prop, sf))
+        {
           return true;
         }
       }
@@ -394,8 +411,11 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf,
   return false;
 }
 
-bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
-                                          Node pv, unsigned effort) {
+bool ArithInstantiator::processAssertions(CegInstantiator* ci,
+                                          SolvedForm& sf,
+                                          Node pv,
+                                          InstEffort effort)
+{
   if (options::cbqiModel()) {
     bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() );
     bool upper_first = false;
@@ -422,7 +442,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
             val = Rewriter::rewrite( val );
           }
           TermProperties pv_prop_no_bound;
-          if( ci->doAddInstantiationInc( pv, val, pv_prop_no_bound, sf, effort ) ){
+          if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf))
+          {
             return true;
           }
         }
@@ -519,7 +540,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
               TermProperties pv_prop_bound;
               pv_prop_bound.d_coeff = d_mbp_coeff[rr][best];
               pv_prop_bound.d_type = rr==0 ? 1 : -1;
-              if( ci->doAddInstantiationInc( pv, val, pv_prop_bound, sf, effort ) ){
+              if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf))
+              {
                 return true;
               }
             }
@@ -534,7 +556,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
       Node theta = sf.getTheta();
       val = getModelBasedProjectionValue( ci, pv, val, true, pv_prop_zero.d_coeff, pv_value, zero, sf.getTheta(), Node::null(), Node::null() );
       if( !val.isNull() ){
-        if( ci->doAddInstantiationInc( pv, val, pv_prop_zero, sf, effort ) ){
+        if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf))
+        {
           return true;
         }
       }
@@ -576,7 +599,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
       Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl;
       if( !val.isNull() ){
         TermProperties pv_prop_midpoint;
-        if( ci->doAddInstantiationInc( pv, val, pv_prop_midpoint, sf, effort ) ){
+        if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf))
+        {
           return true;
         }
       }
@@ -597,7 +621,9 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
               TermProperties pv_prop_nopt_bound;
               pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j];
               pv_prop_nopt_bound.d_type = rr==0 ? 1 : -1;
-              if( ci->doAddInstantiationInc( pv, val, pv_prop_nopt_bound, sf, effort ) ){
+              if (ci->constructInstantiationInc(
+                      pv, val, pv_prop_nopt_bound, sf))
+              {
                 return true;
               }
             }
@@ -609,12 +635,19 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
   return false;
 }
 
-bool ArithInstantiator::needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+bool ArithInstantiator::needsPostProcessInstantiationForVariable(
+    CegInstantiator* ci, SolvedForm& sf, Node pv, InstEffort effort)
+{
   return std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end();
 }
 
-bool ArithInstantiator::postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, 
-                                                             std::vector< Node >& lemmas ) {
+bool ArithInstantiator::postProcessInstantiationForVariable(
+    CegInstantiator* ci,
+    SolvedForm& sf,
+    Node pv,
+    InstEffort effort,
+    std::vector<Node>& lemmas)
+{
   Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end() );
   Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() );
   unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin();
@@ -669,8 +702,11 @@ bool ArithInstantiator::postProcessInstantiationForVariable( CegInstantiator * c
   return true;
 }
 
-void DtInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
-
+void DtInstantiator::reset(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           InstEffort effort)
+{
 }
 
 Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) {
@@ -714,7 +750,12 @@ Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) {
   return ret;
 }
 
-bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) {
+bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
+                                       SolvedForm& sf,
+                                       Node pv,
+                                       std::vector<Node>& eqc,
+                                       InstEffort effort)
+{
   Trace("cegqi-dt-debug") << "[2] try based on constructors in equivalence class." << std::endl;
   //[2] look in equivalence class for a constructor
   for( unsigned k=0; k<eqc.size(); k++ ){
@@ -733,7 +774,8 @@ bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, No
       }
       Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
       TermProperties pv_prop_dt;
-      if( ci->doAddInstantiationInc( pv, val, pv_prop_dt, sf, effort ) ){
+      if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf))
+      {
         return true;
       }else{
         //cleanup
@@ -747,29 +789,46 @@ bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, No
   return false;
 }
 
-bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
+bool DtInstantiator::processEquality(CegInstantiator* ci,
+                                     SolvedForm& sf,
+                                     Node pv,
+                                     std::vector<TermProperties>& term_props,
+                                     std::vector<Node>& terms,
+                                     InstEffort effort)
+{
   Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] );
   if( !val.isNull() ){
     TermProperties pv_prop;
-    if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){
+    if (ci->constructInstantiationInc(pv, val, pv_prop, sf))
+    {
       return true;
     }
   }
   return false;
 }
 
-void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+void EprInstantiator::reset(CegInstantiator* ci,
+                            SolvedForm& sf,
+                            Node pv,
+                            InstEffort effort)
+{
   d_equal_terms.clear();
 }
 
-bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) {
+bool EprInstantiator::processEqualTerm(CegInstantiator* ci,
+                                       SolvedForm& sf,
+                                       Node pv,
+                                       TermProperties& pv_prop,
+                                       Node n,
+                                       InstEffort effort)
+{
   if( options::quantEprMatching() ){
     Assert( pv_prop.isBasic() );
     d_equal_terms.push_back( n );
     return false;
   }else{
     pv_prop.d_type = 0;
-    return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort );
+    return ci->constructInstantiationInc(pv, n, pv_prop, sf);
   }
 }
 
@@ -823,8 +882,12 @@ struct sortEqTermsMatch {
   }
 };
 
-
-bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) {
+bool EprInstantiator::processEqualTerms(CegInstantiator* ci,
+                                        SolvedForm& sf,
+                                        Node pv,
+                                        std::vector<Node>& eqc,
+                                        InstEffort effort)
+{
   if( options::quantEprMatching() ){
     //heuristic for best matching constant
     sortEqTermsMatch setm;
@@ -837,7 +900,8 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N
     TermProperties pv_prop;
     pv_prop.d_type = 0;
     for( unsigned i=0; i<d_equal_terms.size(); i++ ){
-      if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_prop, sf, effort ) ){
+      if (ci->constructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf))
+      {
         return true;
       }
     }
@@ -877,8 +941,11 @@ BvInstantiator::BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instanti
 BvInstantiator::~BvInstantiator(){
 
 }
-
-void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+void BvInstantiator::reset(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           InstEffort effort)
+{
   d_inst_id_counter = 0;
   d_var_to_inst_id.clear();
   d_inst_id_to_term.clear();
@@ -888,9 +955,13 @@ void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsig
   d_alit_to_model_slack.clear();
 }
 
-void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf,
-                                    Node pv, Node lit, Node alit,
-                                    unsigned effort) {
+void BvInstantiator::processLiteral(CegInstantiator* ci,
+                                    SolvedForm& sf,
+                                    Node pv,
+                                    Node lit,
+                                    Node alit,
+                                    InstEffort effort)
+{
   Assert( d_inverter!=NULL );
   // find path to pv
   std::vector< unsigned > path;
@@ -919,8 +990,9 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf,
   }
 }
 
-Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
-                                         Node pv, Node lit, unsigned effort) {
+Node BvInstantiator::hasProcessAssertion(
+    CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort)
+{
   Node atom = lit.getKind() == NOT ? lit[0] : lit;
   bool pol = lit.getKind() != NOT;
   Kind k = atom.getKind();
@@ -1010,9 +1082,13 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
   return Node::null();
 }
 
-bool BvInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf,
-                                      Node pv, Node lit, Node alit,
-                                      unsigned effort) {
+bool BvInstantiator::processAssertion(CegInstantiator* ci,
+                                      SolvedForm& sf,
+                                      Node pv,
+                                      Node lit,
+                                      Node alit,
+                                      InstEffort effort)
+{
   // if option enabled, use approach for word-level inversion for BV instantiation
   if( options::cbqiBv() ){
     // get the best rewritten form of lit for solving for pv 
@@ -1029,8 +1105,11 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf,
   return false;
 }
 
-bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
-                                       Node pv, unsigned effort) {
+bool BvInstantiator::processAssertions(CegInstantiator* ci,
+                                       SolvedForm& sf,
+                                       Node pv,
+                                       InstEffort effort)
+{
   std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv );
   if( iti!=d_var_to_inst_id.end() ){
     Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl;
@@ -1124,8 +1203,8 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
         Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term
                           << std::endl;
         d_var_to_curr_inst_id[pv] = inst_id;
-        if (ci->doAddInstantiationInc(
-                pv, inst_term, pv_prop_bv, sf, effort, revertOnSuccess))
+        if (ci->constructInstantiationInc(
+                pv, inst_term, pv_prop_bv, sf, revertOnSuccess))
         {
           ret = true;
         }
@@ -1280,3 +1359,7 @@ Node BvInstantiator::rewriteTermForSolvePv(
 
   return Node::null();
 }
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index 30dd1bffa..0242a2994 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -27,65 +27,199 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+/** TODO (#1367) : document these classes, also move to separate files. */
+
 class ArithInstantiator : public Instantiator {
-private:
-  Node d_vts_sym[2];
-  std::vector< Node > d_mbp_bounds[2];
-  std::vector< Node > d_mbp_coeff[2];
-  std::vector< Node > d_mbp_vts_coeff[2][2];
-  std::vector< Node > d_mbp_lit[2];
-  int solve_arith( CegInstantiator * ci, Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta );
-  Node getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff );
-public:
+ public:
   ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
   virtual ~ArithInstantiator(){}
-  void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
-  bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
-  bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort );
-  bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
-  Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv,
-                           Node lit, unsigned effort);
-  bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit,
-                        Node alit, unsigned effort);
-  bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv,
-                         unsigned effort);
-  bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
-  bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas );
-  std::string identify() const { return "Arith"; }
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     InstEffort effort) override;
+  virtual bool hasProcessEquality(CegInstantiator* ci,
+                                  SolvedForm& sf,
+                                  Node pv,
+                                  InstEffort effort) override
+  {
+    return true;
+  }
+  virtual bool processEquality(CegInstantiator* ci,
+                               SolvedForm& sf,
+                               Node pv,
+                               std::vector<TermProperties>& term_props,
+                               std::vector<Node>& terms,
+                               InstEffort effort) override;
+  virtual bool hasProcessAssertion(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   InstEffort effort) override
+  {
+    return true;
+  }
+  virtual Node hasProcessAssertion(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   Node lit,
+                                   InstEffort effort) override;
+  virtual bool processAssertion(CegInstantiator* ci,
+                                SolvedForm& sf,
+                                Node pv,
+                                Node lit,
+                                Node alit,
+                                InstEffort effort) override;
+  virtual bool processAssertions(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 InstEffort effort) override;
+  virtual bool needsPostProcessInstantiationForVariable(
+      CegInstantiator* ci, SolvedForm& sf, Node pv, InstEffort effort) override;
+  virtual bool postProcessInstantiationForVariable(
+      CegInstantiator* ci,
+      SolvedForm& sf,
+      Node pv,
+      InstEffort effort,
+      std::vector<Node>& lemmas) override;
+  virtual std::string identify() const override { return "Arith"; }
+ private:
+  Node d_vts_sym[2];
+  std::vector<Node> d_mbp_bounds[2];
+  std::vector<Node> d_mbp_coeff[2];
+  std::vector<Node> d_mbp_vts_coeff[2][2];
+  std::vector<Node> d_mbp_lit[2];
+  int solve_arith(CegInstantiator* ci,
+                  Node v,
+                  Node atom,
+                  Node& veq_c,
+                  Node& val,
+                  Node& vts_coeff_inf,
+                  Node& vts_coeff_delta);
+  Node getModelBasedProjectionValue(CegInstantiator* ci,
+                                    Node e,
+                                    Node t,
+                                    bool isLower,
+                                    Node c,
+                                    Node me,
+                                    Node mt,
+                                    Node theta,
+                                    Node inf_coeff,
+                                    Node delta_coeff);
 };
 
 class DtInstantiator : public Instantiator {
-private:
-  Node solve_dt( Node v, Node a, Node b, Node sa, Node sb );
 public:
   DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
   virtual ~DtInstantiator(){}
-  void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
-  bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort );
-  bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
-  bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort );
-  std::string identify() const { return "Dt"; }
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     InstEffort effort) override;
+  virtual bool processEqualTerms(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 std::vector<Node>& eqc,
+                                 InstEffort effort) override;
+  virtual bool hasProcessEquality(CegInstantiator* ci,
+                                  SolvedForm& sf,
+                                  Node pv,
+                                  InstEffort effort) override
+  {
+    return true;
+  }
+  virtual bool processEquality(CegInstantiator* ci,
+                               SolvedForm& sf,
+                               Node pv,
+                               std::vector<TermProperties>& term_props,
+                               std::vector<Node>& terms,
+                               InstEffort effort) override;
+  virtual std::string identify() const override { return "Dt"; }
+ private:
+  Node solve_dt(Node v, Node a, Node b, Node sa, Node sb);
 };
 
 class TermArgTrie;
 
 class EprInstantiator : public Instantiator {
-private:
-  std::vector< Node > d_equal_terms;
-  void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score );
-  void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score );
-public:
+ public:
   EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
   virtual ~EprInstantiator(){}
-  void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
-  bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort );
-  bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort );
-  std::string identify() const { return "Epr"; }
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     InstEffort effort) override;
+  virtual bool processEqualTerm(CegInstantiator* ci,
+                                SolvedForm& sf,
+                                Node pv,
+                                TermProperties& pv_prop,
+                                Node n,
+                                InstEffort effort) override;
+  virtual bool processEqualTerms(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 std::vector<Node>& eqc,
+                                 InstEffort effort) override;
+  virtual std::string identify() const override { return "Epr"; }
+ private:
+  std::vector<Node> d_equal_terms;
+  void computeMatchScore(CegInstantiator* ci,
+                         Node pv,
+                         Node catom,
+                         std::vector<Node>& arg_reps,
+                         TermArgTrie* tat,
+                         unsigned index,
+                         std::map<Node, int>& match_score);
+  void computeMatchScore(CegInstantiator* ci,
+                         Node pv,
+                         Node catom,
+                         Node eqc,
+                         std::map<Node, int>& match_score);
 };
 
-
+/** Bitvector instantiator
+ *
+ * This implements an approach for counterexample-guided instantiation
+ * for bit-vector variables based on word-level inversions.
+ * It is enabled by --cbqi-bv.
+ */
 class BvInstantiator : public Instantiator {
-private:
+ public:
+  BvInstantiator(QuantifiersEngine* qe, TypeNode tn);
+  virtual ~BvInstantiator();
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     InstEffort effort) override;
+  virtual bool hasProcessAssertion(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   InstEffort effort) override
+  {
+    return true;
+  }
+  virtual Node hasProcessAssertion(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   Node lit,
+                                   InstEffort effort) override;
+  virtual bool processAssertion(CegInstantiator* ci,
+                                SolvedForm& sf,
+                                Node pv,
+                                Node lit,
+                                Node alit,
+                                InstEffort effort) override;
+  virtual bool processAssertions(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 InstEffort effort) override;
+  virtual bool useModelValue(CegInstantiator* ci,
+                             SolvedForm& sf,
+                             Node pv,
+                             InstEffort effort) override
+  {
+    return true;
+  }
+  virtual std::string identify() const { return "Bv"; }
+ private:
   // point to the bv inverter class
   BvInverter * d_inverter;
   unsigned d_inst_id_counter;
@@ -123,27 +257,16 @@ private:
   * internal rules here.
   * alit is the asserted literal that lit is derived from.
   */
-  void processLiteral(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit,
-                      Node alit, unsigned effort);
-
- public:
-  BvInstantiator( QuantifiersEngine * qe, TypeNode tn );
-  virtual ~BvInstantiator();
-  void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
-  bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
-  Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv,
-                           Node lit, unsigned effort);
-  bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit,
-                        Node alit, unsigned effort);
-  bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv,
-                         unsigned effort);
-  bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
-  std::string identify() const { return "Bv"; }
+  void processLiteral(CegInstantiator* ci,
+                      SolvedForm& sf,
+                      Node pv,
+                      Node lit,
+                      Node alit,
+                      InstEffort effort);
 };
 
-
-}
-}
-}
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
 
 #endif