Quantifiers subdirectories (#1608)

6 files changed, 5435 insertions, 0 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
new file mode 100644
index 000000000..d7d46bb4b
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -0,0 +1,1337 @@
+/*********************                                                        */
+/*! \file ceg_instantiator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, 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 counterexample-guided quantifier instantiation
+ **/
+
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/cegqi/ceg_t_instantiator.h"
+
+#include "options/quantifiers_options.h"
+#include "smt/term_formula_removal.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/first_order_model.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"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/theory_engine.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+std::ostream& operator<<(std::ostream& os, CegInstEffort e)
+{
+  switch (e)
+  {
+    case CEG_INST_EFFORT_NONE: os << "?"; break;
+    case CEG_INST_EFFORT_STANDARD: os << "STANDARD"; break;
+    case CEG_INST_EFFORT_STANDARD_MV: os << "STANDARD_MV"; break;
+    case CEG_INST_EFFORT_FULL: os << "FULL"; break;
+    default: Unreachable();
+  }
+  return os;
+}
+
+std::ostream& operator<<(std::ostream& os, CegInstPhase phase)
+{
+  switch (phase)
+  {
+    case CEG_INST_PHASE_NONE: os << "?"; break;
+    case CEG_INST_PHASE_EQC: os << "eqc"; break;
+    case CEG_INST_PHASE_EQUAL: os << "eq"; break;
+    case CEG_INST_PHASE_ASSERTION: os << "as"; break;
+    case CEG_INST_PHASE_MVALUE: os << "mv"; break;
+    default: Unreachable();
+  }
+  return os;
+}
+
+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),
+      d_effort(CEG_INST_EFFORT_NONE)
+{
+}
+
+CegInstantiator::~CegInstantiator() {
+  for (std::pair<Node, Instantiator*> inst : d_instantiator)
+  {
+    delete inst.second;
+  }
+  for (std::pair<TheoryId, InstantiatorPreprocess*> instp : d_tipp)
+  {
+    delete instp.second;
+  }
+}
+
+void CegInstantiator::computeProgVars( Node n ){
+  if( d_prog_var.find( n )==d_prog_var.end() ){
+    d_prog_var[n].clear();
+    if (n.getKind() == kind::CHOICE)
+    {
+      Assert(d_prog_var.find(n[0][0]) == d_prog_var.end());
+      d_prog_var[n[0][0]].clear();
+    }
+    if (d_vars_set.find(n) != d_vars_set.end())
+    {
+      d_prog_var[n].insert(n);
+    }else if( !d_out->isEligibleForInstantiation( n ) ){
+      d_inelig.insert(n);
+      return;
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      computeProgVars( n[i] );
+      if( d_inelig.find( n[i] )!=d_inelig.end() ){
+        d_inelig.insert(n);
+      }
+      // all variables in child are contained in this
+      d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end());
+    }
+    // selectors applied to program variables are also variables
+    if (n.getKind() == APPLY_SELECTOR_TOTAL
+        && d_prog_var[n].find(n[0]) != d_prog_var[n].end())
+    {
+      d_prog_var[n].insert(n);
+    }
+    if (n.getKind() == kind::CHOICE)
+    {
+      d_prog_var.erase(n[0][0]);
+    }
+  }
+}
+
+bool CegInstantiator::isEligible( Node n ) {
+  //compute d_subs_fv, which program variables are contained in n, and determines if eligible
+  computeProgVars( n );
+  return d_inelig.find( n )==d_inelig.end();
+}
+
+bool CegInstantiator::hasVariable( Node n, Node pv ) {
+  computeProgVars( n );
+  return d_prog_var[n].find( pv )!=d_prog_var[n].end();
+}
+
+void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
+{
+  if( d_instantiator.find( v )==d_instantiator.end() ){
+    TypeNode tn = v.getType();
+    Instantiator * vinst;
+    if( tn.isReal() ){
+      vinst = new ArithInstantiator( d_qe, tn );
+    }else if( tn.isSort() ){
+      Assert( options::quantEpr() );
+      vinst = new EprInstantiator( d_qe, tn );
+    }else if( tn.isDatatype() ){
+      vinst = new DtInstantiator( d_qe, tn );
+    }else if( tn.isBitVector() ){
+      vinst = new BvInstantiator( d_qe, tn );
+    }else if( tn.isBoolean() ){
+      vinst = new ModelValueInstantiator( d_qe, tn );
+    }else{
+      //default
+      vinst = new Instantiator( d_qe, tn );
+    }
+    d_instantiator[v] = vinst;
+  }
+  d_curr_subs_proc[v].clear();
+  d_curr_index[v] = index;
+  d_curr_iphase[v] = CEG_INST_PHASE_NONE;
+}
+
+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
+    if (tid == THEORY_BV)
+    {
+      d_tipp[tid] = new BvInstantiatorPreprocess;
+    }
+    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 );
+  d_curr_iphase.erase(v);
+}
+
+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_input_vars.size() || !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, d_effort))
+      {
+        needsPostprocess = true;
+        pp_inst_to_var[ ita->second ] = ita->first;
+      }
+    }
+    if( needsPostprocess ){
+      //must make copy so that backtracking reverts sf
+      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, d_effort, lemmas))
+        {
+          postProcessSuccess = false;
+          break;
+        }
+      }
+      if( postProcessSuccess ){
+        return doAddInstantiation( sf_tmp.d_vars, sf_tmp.d_subs, lemmas );
+      }else{
+        return false;
+      }
+    }else{
+      return doAddInstantiation( sf.d_vars, sf.d_subs, lemmas );
+    }
+  }else{
+    //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
+    bool is_cv = false;
+    Node pv;
+    if( d_stack_vars.empty() ){
+      pv = d_vars[i];
+    }else{
+      pv = d_stack_vars.back();
+      is_cv = true;
+      d_stack_vars.pop_back();
+    }
+    activateInstantiationVariable(pv, i);
+
+    //get the instantiator object
+    Instantiator * vinst = NULL;
+    std::map< Node, Instantiator * >::iterator itin = d_instantiator.find( pv );
+    if( itin!=d_instantiator.end() ){
+      vinst = itin->second;
+    }
+    Assert( vinst!=NULL );
+    d_active_instantiators[pv] = vinst;
+    vinst->reset(this, sf, pv, d_effort);
+
+    TypeNode pvtn = pv.getType();
+    TypeNode pvtnb = pvtn.getBaseType();
+    Node pvr = pv;
+    if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){
+      pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv );
+    }
+    Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "], rep=" << pvr << ", instantiator is " << vinst->identify() << std::endl;
+    Node pv_value;
+    if( options::cbqiModel() ){
+      pv_value = getModelValue( pv );
+      Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+    }
+
+    // if d_effort is full, we must choose at least one model value
+    if ((i + 1) < d_vars.size() || d_effort != CEG_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;
+      d_curr_iphase[pv] = CEG_INST_PHASE_EQC;
+      std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
+      if( it_eqc!=d_curr_eqc.end() ){
+        //std::vector< Node > eq_candidates;
+        Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl;
+        for( unsigned k=0; k<it_eqc->second.size(); k++ ){
+          Node n = it_eqc->second[k];
+          if( n!=pv ){
+            Trace("cbqi-inst-debug") << "...try based on equal term " << n << std::endl;
+            //must be an eligible term
+            if( isEligible( n ) ){
+              Node ns;
+              TermProperties pv_prop;  //coefficient of pv in the equality we solve (null is 1)
+              bool proc = false;
+              if( !d_prog_var[n].empty() ){
+                ns = applySubstitution( pvtn, n, sf, pv_prop, false );
+                if( !ns.isNull() ){
+                  computeProgVars( ns );
+                  //substituted version must be new and cannot contain pv
+                  proc = d_prog_var[ns].find( pv )==d_prog_var[ns].end();
+                }
+              }else{
+                ns = n;
+                proc = true;
+              }
+              if( proc ){
+                if (vinst->processEqualTerm(
+                        this, sf, pv, pv_prop, ns, d_effort))
+                {
+                  return true;
+                }
+                // Do not consider more than one equal term,
+                // this helps non-monotonic strategies that may encounter
+                // duplicate instantiations.
+                break;
+              }
+            }
+          }
+        }
+        if (vinst->processEqualTerms(this, sf, pv, it_eqc->second, d_effort))
+        {
+          return true;
+        }
+      }else{
+        Trace("cbqi-inst-debug2") << "...eqc not found." << 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;
+        d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL;
+        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 );
+          std::vector< Node > lhs;
+          std::vector< bool > lhs_v;
+          std::vector< TermProperties > lhs_prop;
+          Assert( it_reqc!=d_curr_eqc.end() );
+          for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
+            Node n = it_reqc->second[kk];
+            Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
+            //must be an eligible term
+            if( isEligible( n ) ){
+              Node ns;
+              TermProperties pv_prop;
+              if( !d_prog_var[n].empty() ){
+                ns = applySubstitution( pvtn, n, sf, pv_prop );
+                if( !ns.isNull() ){
+                  computeProgVars( ns );
+                }
+              }else{
+                ns = n;
+              }
+              if( !ns.isNull() ){
+                bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end();
+                Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl;
+                std::vector< TermProperties > term_props;
+                std::vector< Node > terms;
+                term_props.push_back( pv_prop );
+                terms.push_back( ns );
+                for( unsigned j=0; j<lhs.size(); j++ ){
+                  //if this term or the another has pv in it, try to solve for it
+                  if( hasVar || lhs_v[j] ){
+                    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, d_effort))
+                    {
+                      return true;
+                    }
+                    term_props.pop_back();
+                    terms.pop_back();
+                  }
+                }
+                lhs.push_back( ns );
+                lhs_v.push_back( hasVar );
+                lhs_prop.push_back( pv_prop );
+              }else{
+                Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl;
+              }
+            }else{
+              Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << 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;
+        d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION;
+        std::unordered_set< Node, NodeHashFunction > lits;
+        //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
+        for( unsigned r=0; r<2; r++ ){
+          TheoryId tid = r==0 ? Theory::theoryOf( pvtn ) : THEORY_UF;
+          Trace("cbqi-inst-debug2") << "  look at assertions of " << tid << std::endl;
+          std::map< TheoryId, std::vector< Node > >::iterator ita = d_curr_asserts.find( tid );
+          if( ita!=d_curr_asserts.end() ){
+            for (unsigned j = 0; j<ita->second.size(); j++) {
+              Node lit = ita->second[j];
+              if( lits.find(lit)==lits.end() ){
+                lits.insert(lit);
+                Node plit;
+                if (options::cbqiRepeatLit() || !isSolvedAssertion(lit))
+                {
+                  plit =
+                      vinst->hasProcessAssertion(this, sf, pv, lit, d_effort);
+                }
+                if (!plit.isNull()) {
+                  Trace("cbqi-inst-debug2") << "  look at " << lit;
+                  if (plit != lit) {
+                    Trace("cbqi-inst-debug2") << "...processed to : " << plit;
+                  }
+                  Trace("cbqi-inst-debug2") << std::endl;
+                  // apply substitutions
+                  Node slit = applySubstitutionToLiteral(plit, sf);
+                  if( !slit.isNull() ){
+                    // check if contains pv
+                    if( hasVariable( slit, pv ) ){
+                      Trace("cbqi-inst-debug") << "...try based on literal "
+                                               << slit << "," << std::endl;
+                      Trace("cbqi-inst-debug") << "...from " << lit
+                                               << std::endl;
+                      if (vinst->processAssertion(
+                              this, sf, pv, slit, lit, d_effort))
+                      {
+                        return true;
+                      }
+                    }
+                  }
+                }
+              }
+            }
+          }
+        }
+        if (vinst->processAssertions(this, sf, pv, d_effort))
+        {
+          return true;
+        }
+      }
+    }
+
+    //[4] resort to using value in model. We do so if:
+    // - if the instantiator uses model values at this effort, or
+    // - if we are solving for a subfield of a datatype (is_cv).
+    if ((vinst->useModelValue(this, sf, pv, d_effort) || 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;
+        Assert( false );
+      }
+#endif
+      Node mv = getModelValue( pv );
+      TermProperties pv_prop_m;
+      Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
+      d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE;
+      CegInstEffort prev = d_effort;
+      if (d_effort < CEG_INST_EFFORT_STANDARD_MV)
+      {
+        // update the effort level to indicate we have used a model value
+        d_effort = CEG_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 );
+    deactivateInstantiationVariable(pv);
+    return false;
+  }
+}
+
+void CegInstantiator::pushStackVariable( Node v ) {
+  d_stack_vars.push_back( v );
+}
+
+void CegInstantiator::popStackVariable() {
+  Assert( !d_stack_vars.empty() );
+  d_stack_vars.pop_back();
+}
+
+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() ){
+    d_curr_subs_proc[pv][n][cnode] = true;
+    if( Trace.isOn("cbqi-inst-debug") ){
+      for( unsigned j=0; j<sf.d_subs.size(); j++ ){
+        Trace("cbqi-inst-debug") << " ";
+      }
+      Trace("cbqi-inst-debug") << sf.d_subs.size() << ": (" << d_curr_iphase[pv]
+                         << ") ";
+      Node mod_pv = pv_prop.getModifiedTerm( pv );
+      Trace("cbqi-inst-debug") << mod_pv << " -> " << n << std::endl;
+      Assert( n.getType().isSubtypeOf( pv.getType() ) );
+    }
+    //must ensure variables have been computed for n
+    computeProgVars( n );
+    Assert( d_inelig.find( n )==d_inelig.end() );
+
+    //substitute into previous substitutions, when applicable
+    std::vector< Node > a_var;
+    a_var.push_back( pv );
+    std::vector< Node > a_subs;
+    a_subs.push_back( n );
+    std::vector< TermProperties > a_prop;
+    a_prop.push_back( pv_prop );
+    std::vector< Node > a_non_basic;
+    if( !pv_prop.isBasic() ){
+      a_non_basic.push_back( pv );
+    }
+    bool success = true;
+    std::map< int, Node > prev_subs;
+    std::map< int, TermProperties > prev_prop;
+    std::map< int, Node > prev_sym_subs;
+    std::vector< Node > new_non_basic;
+    Trace("cbqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl;
+    for( unsigned j=0; j<sf.d_subs.size(); j++ ){
+      Trace("cbqi-inst-debug2") << "  Apply for " << sf.d_subs[j]  << std::endl;
+      Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() );
+      if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
+        prev_subs[j] = sf.d_subs[j];
+        TNode tv = pv;
+        TNode ts = n;
+        TermProperties a_pv_prop;
+        Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_var, a_subs, a_prop, a_non_basic, a_pv_prop, true );
+        if( !new_subs.isNull() ){
+          sf.d_subs[j] = new_subs;
+          // the substitution apply to this term resulted in a non-basic substitution relationship
+          if( !a_pv_prop.isBasic() ){
+            // we are processing:
+            //    sf.d_props[j].getModifiedTerm( sf.d_vars[j] ) = sf.d_subs[j] { pv_prop.getModifiedTerm( pv ) -> n } 
+          
+            // based on the above substitution, we have:
+            //   x = sf.d_subs[j] { pv_prop.getModifiedTerm( pv ) -> n } 
+            // is equivalent to
+            //   a_pv_prop.getModifiedTerm( x ) = new_subs
+            
+            // thus we must compose substitutions:
+            //   a_pv_prop.getModifiedTerm( sf.d_props[j].getModifiedTerm( sf.d_vars[j] ) ) = new_subs
+            
+            prev_prop[j] = sf.d_props[j];
+            bool prev_basic = sf.d_props[j].isBasic();
+            
+            // now compose the property
+            sf.d_props[j].composeProperty( a_pv_prop );
+            
+            // if previously was basic, becomes non-basic
+            if( prev_basic && !sf.d_props[j].isBasic() ){
+              Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), sf.d_vars[j] )==sf.d_non_basic.end() );
+              new_non_basic.push_back( sf.d_vars[j] );
+              sf.d_non_basic.push_back( sf.d_vars[j] );
+            }
+          }
+          if( sf.d_subs[j]!=prev_subs[j] ){
+            computeProgVars( sf.d_subs[j] );
+            Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() );
+          }
+          Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
+        }else{
+          Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
+          success = false;
+          break;
+        }
+      }else{
+        Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
+      }
+    }
+    if( success ){
+      Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
+      sf.push_back( pv, n, pv_prop );
+      Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
+      unsigned i = d_curr_index[pv];
+      success = constructInstantiation(sf, d_stack_vars.empty() ? i + 1 : i);
+      if (!success || revertOnSuccess)
+      {
+        Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
+        sf.pop_back( pv, n, pv_prop );
+      }
+    }
+    if (success && !revertOnSuccess)
+    {
+      return true;
+    }else{
+      Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl;
+      //revert substitution information
+      for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){
+        sf.d_subs[it->first] = it->second;
+      }
+      for( std::map< int, TermProperties >::iterator it = prev_prop.begin(); it != prev_prop.end(); it++ ){
+        sf.d_props[it->first] = it->second;
+      }
+      for( unsigned i=0; i<new_non_basic.size(); i++ ){
+        sf.d_non_basic.pop_back();
+      }
+      return success;
+    }
+  }else{
+    //already tried this substitution
+    return false;
+  }
+}
+
+bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) {
+  if (vars.size() > d_input_vars.size() || !d_var_order_index.empty())
+  {
+    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, size = d_input_vars.size(); i < size; ++i)
+    {
+      std::map<Node, Node>::iterator it = subs_map.find(d_input_vars[i]);
+      Assert( it!=subs_map.end() );
+      Node n = it->second;
+      Trace("cbqi-inst-debug") << "  " << d_input_vars[i] << " -> " << n
+                               << std::endl;
+      Assert(n.getType().isSubtypeOf(d_input_vars[i].getType()));
+      subs.push_back( n );
+    }
+  }
+  if (Trace.isOn("cbqi-inst"))
+  {
+    Trace("cbqi-inst") << "Ceg Instantiator produced : " << std::endl;
+    for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
+    {
+      Node v = d_input_vars[i];
+      Trace("cbqi-inst") << i << " (" << d_curr_iphase[v] << ") : " 
+                         << v << " -> " << subs[i] << std::endl;
+      Assert(subs[i].getType().isSubtypeOf(v.getType()));
+    }
+  }
+  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] );
+  }
+  return ret;
+}
+
+bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){
+  Assert( d_prog_var.find( n )!=d_prog_var.end() );
+  if( !non_basic.empty() ){
+    for (std::unordered_set<Node, NodeHashFunction>::iterator it =
+             d_prog_var[n].begin();
+         it != d_prog_var[n].end();
+         ++it)
+    {
+      if (std::find(non_basic.begin(), non_basic.end(), *it) != non_basic.end())
+      {
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, 
+                                         std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) {
+  computeProgVars( n );
+  Assert( n==Rewriter::rewrite( n ) );
+  bool is_basic = canApplyBasicSubstitution( n, non_basic );
+  if( Trace.isOn("cegqi-si-apply-subs-debug") ){
+    Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << "  " << tn << std::endl;
+    for( unsigned i=0; i<subs.size(); i++ ){
+      Trace("cegqi-si-apply-subs-debug") << "  " << vars[i] << " -> " << subs[i] << "   types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
+      Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) );
+    }
+  }
+  Node nret;
+  if( is_basic ){
+    nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+  }else{
+    if( !tn.isInteger() ){
+      //can do basic substitution instead with divisions
+      std::vector< Node > nvars;
+      std::vector< Node > nsubs;
+      for( unsigned i=0; i<vars.size(); i++ ){
+        if( !prop[i].d_coeff.isNull() ){
+          Assert( vars[i].getType().isInteger() );
+          Assert( prop[i].d_coeff.isConst() );
+          Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) );
+          nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
+          nn =  Rewriter::rewrite( nn );
+          nsubs.push_back( nn );
+        }else{
+          nsubs.push_back( subs[i] );
+        }
+      }
+      nret = n.substitute( vars.begin(), vars.end(), nsubs.begin(), nsubs.end() );
+    }else if( try_coeff ){
+      //must convert to monomial representation
+      std::map< Node, Node > msum;
+      if (ArithMSum::getMonomialSum(n, msum))
+      {
+        std::map< Node, Node > msum_coeff;
+        std::map< Node, Node > msum_term;
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          //check if in substitution
+          std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first );
+          if( its!=vars.end() ){
+            int index = its-vars.begin();
+            if( prop[index].d_coeff.isNull() ){
+              //apply substitution
+              msum_term[it->first] = subs[index];
+            }else{
+              //apply substitution, multiply to ensure no divisibility conflict
+              msum_term[it->first] = subs[index];
+              //relative coefficient
+              msum_coeff[it->first] = prop[index].d_coeff;
+              if( pv_prop.d_coeff.isNull() ){
+                pv_prop.d_coeff = prop[index].d_coeff;
+              }else{
+                pv_prop.d_coeff = NodeManager::currentNM()->mkNode( MULT, pv_prop.d_coeff, prop[index].d_coeff );
+              }
+            }
+          }else{
+            msum_term[it->first] = it->first;
+          }
+        }
+        //make sum with normalized coefficient
+        if( !pv_prop.d_coeff.isNull() ){
+          pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff );
+          Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl;
+          std::vector< Node > children;
+          for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+            Node c_coeff;
+            if( !msum_coeff[it->first].isNull() ){
+              c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_prop.d_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) );
+            }else{
+              c_coeff = pv_prop.d_coeff;
+            }
+            if( !it->second.isNull() ){
+              c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second );
+            }
+            Assert( !c_coeff.isNull() );
+            Node c;
+            if( msum_term[it->first].isNull() ){
+              c = c_coeff;
+            }else{
+              c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] );
+            }
+            children.push_back( c );
+            Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl;
+          }
+          Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
+          nretc = Rewriter::rewrite( nretc );
+          //ensure that nret does not contain vars
+          if( !TermUtil::containsTerms( nretc, vars ) ){
+            //result is ( nret / pv_prop.d_coeff )
+            nret = nretc;
+          }else{
+            Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl;
+          }
+        }else{
+          //implies that we have a monomial that has a free variable
+          Trace("cegqi-si-apply-subs-debug") << "Failed to find coefficient during substitution, implies monomial with free variable." << std::endl;
+        }
+      }else{
+        Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
+      }
+    }
+  }
+  if( n!=nret && !nret.isNull() ){
+    nret = Rewriter::rewrite( nret );
+  }
+  return nret;
+}
+
+Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, 
+                                                  std::vector< TermProperties >& prop, std::vector< Node >& non_basic ) {
+  computeProgVars( lit );
+  bool is_basic = canApplyBasicSubstitution( lit, non_basic );
+  Node lret;
+  if( is_basic ){
+   lret = lit.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+  }else{
+    Node atom = lit.getKind()==NOT ? lit[0] : lit;
+    bool pol = lit.getKind()!=NOT;
+    //arithmetic inequalities and disequalities
+    if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){
+      Assert( atom.getKind()!=GEQ || atom[1].isConst() );
+      Node atom_lhs;
+      Node atom_rhs;
+      if( atom.getKind()==GEQ ){
+        atom_lhs = atom[0];
+        atom_rhs = atom[1];
+      }else{
+        atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
+        atom_lhs = Rewriter::rewrite( atom_lhs );
+        atom_rhs = getQuantifiersEngine()->getTermUtil()->d_zero;
+      }
+      //must be an eligible term
+      if( isEligible( atom_lhs ) ){
+        //apply substitution to LHS of atom
+        TermProperties atom_lhs_prop;
+        atom_lhs = applySubstitution( NodeManager::currentNM()->realType(), atom_lhs, vars, subs, prop, non_basic, atom_lhs_prop );
+        if( !atom_lhs.isNull() ){
+          if( !atom_lhs_prop.d_coeff.isNull() ){
+            atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) );
+          }
+          lret = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
+          if( !pol ){
+            lret = lret.negate();
+          }
+        }
+      }
+    }else{
+      // don't know how to apply substitution to literal
+    }
+  }
+  if( lit!=lret && !lret.isNull() ){
+    lret = Rewriter::rewrite( lret );
+  }
+  return lret;
+}
+  
+bool CegInstantiator::check() {
+  if( d_qe->getTheoryEngine()->needCheck() ){
+    Trace("cbqi-engine") << "  CEGQI instantiator : wait until all ground theories are finished." << std::endl;
+    return false;
+  }
+  processAssertions();
+  for( unsigned r=0; r<2; r++ ){
+    d_effort = r == 0 ? CEG_INST_EFFORT_STANDARD : CEG_INST_EFFORT_FULL;
+    SolvedForm sf;
+    d_stack_vars.clear();
+    d_bound_var_index.clear();
+    d_solved_asserts.clear();
+    //try to add an instantiation
+    if (constructInstantiation(sf, 0))
+    {
+      return true;
+    }
+  }
+  Trace("cbqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+  return false;
+}
+
+void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) {
+  if( n.getKind()==FORALL || n.getKind()==EXISTS ){
+    //do nothing
+  }else{
+    if( n.getKind()==EQUAL ){
+      for( unsigned i=0; i<2; i++ ){
+        std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] );
+        if( it!=teq.end() ){
+          Node nn = n[ i==0 ? 1 : 0 ];
+          if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){
+            it->second.push_back( nn );
+            Trace("cbqi-presolve") << "  - " << n[i] << " = " << nn << std::endl;
+          }
+        }
+      }
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectPresolveEqTerms( n[i], teq );
+    }
+  }
+}
+
+void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms,
+                             std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) {
+  if( conj.size()<1000 ){
+    if( terms.size()==f[0].getNumChildren() ){
+      Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+      conj.push_back( c );
+    }else{
+      unsigned i = terms.size();
+      Node v = f[0][i];
+      terms.push_back( Node::null() );
+      for( unsigned j=0; j<teq[v].size(); j++ ){
+        terms[i] = teq[v][j];
+        getPresolveEqConjuncts( vars, terms, teq, f, conj );
+      }
+      terms.pop_back();
+    }
+  }
+}
+
+void CegInstantiator::presolve( Node q ) {
+  //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
+  //only if no nested quantifiers
+  if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){
+    std::vector< Node > ps_vars;
+    std::map< Node, std::vector< Node > > teq;
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      ps_vars.push_back( q[0][i] );
+      teq[q[0][i]].clear();
+    }
+    collectPresolveEqTerms( q[1], teq );
+    std::vector< Node > terms;
+    std::vector< Node > conj;
+    getPresolveEqConjuncts( ps_vars, terms, teq, q, conj );
+
+    if( !conj.empty() ){
+      Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
+      Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
+      lem = NodeManager::currentNM()->mkNode( OR, g, lem );
+      Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
+      d_qe->getOutputChannel().lemma( lem, false, true );
+    }
+  }
+}
+
+void CegInstantiator::processAssertions() {
+  Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl;
+  d_curr_asserts.clear();
+  d_curr_eqc.clear();
+  d_curr_type_eqc.clear();
+
+  // must use master equality engine to avoid value instantiations
+  eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
+  //to eliminate identified illegal terms
+  std::map< Node, Node > aux_subs;
+
+  //for each variable
+  for( unsigned i=0; i<d_vars.size(); i++ ){
+    Node pv = d_vars[i];
+    TypeNode pvtn = pv.getType();
+    Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
+    //collect information about eqc
+    if( ee->hasTerm( pv ) ){
+      Node pvr = ee->getRepresentative( pv );
+      if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){
+        Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl;
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee );
+        while( !eqc_i.isFinished() ){
+          d_curr_eqc[pvr].push_back( *eqc_i );
+          ++eqc_i;
+        }
+      }
+    }
+  }
+  //collect assertions for relevant theories
+  for( unsigned i=0; i<d_tids.size(); i++ ){
+    TheoryId tid = d_tids[i];
+    Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
+    if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){
+      Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl;
+      d_curr_asserts[tid].clear();
+      //collect all assertions from theory
+      for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) {
+        Node lit = (*it).assertion;
+        Node atom = lit.getKind()==NOT ? lit[0] : lit;
+        if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
+          d_curr_asserts[tid].push_back( lit );
+          Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+        }else{
+          Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
+        }
+        if( lit.getKind()==EQUAL ){
+          std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit );
+          if( itae!=d_aux_eq.end() ){
+            for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){
+              aux_subs[ itae2->first ] = itae2->second;
+              Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl;
+            }
+          }
+        }else if( atom.getKind()==BOOLEAN_TERM_VARIABLE ){
+          if( std::find( d_aux_vars.begin(), d_aux_vars.end(), atom )!=d_aux_vars.end() ){
+            Node val = NodeManager::currentNM()->mkConst( lit.getKind()!=NOT );
+            aux_subs[ atom ] = val;
+            Trace("cbqi-proc") << "......add substitution : " << atom << " -> " << val << std::endl;
+          }
+        }
+      }
+    }
+  }
+  //collect equivalence classes that correspond to relevant theories
+  Trace("cbqi-proc-debug") << "...collect typed equivalence classes" << std::endl;
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+  while( !eqcs_i.isFinished() ){
+    Node r = *eqcs_i;
+    TypeNode rtn = r.getType();
+    TheoryId tid = Theory::theoryOf( rtn );
+    //if we care about the theory of this eqc
+    if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){
+      if( rtn.isInteger() || rtn.isReal() ){
+        rtn = rtn.getBaseType();
+      }
+      Trace("cbqi-proc-debug") << "...type eqc: " << r << std::endl;
+      d_curr_type_eqc[rtn].push_back( r );
+      if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
+        Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl;
+        Trace("cbqi-proc-debug") << "  ";
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+        while( !eqc_i.isFinished() ){
+          Trace("cbqi-proc-debug") << *eqc_i << " ";
+          d_curr_eqc[r].push_back( *eqc_i );
+          ++eqc_i;
+        }
+        Trace("cbqi-proc-debug") << std::endl;
+      }
+    }
+    ++eqcs_i;
+  }
+  //construct substitution from auxiliary variable equalities (if e.g. ITE removal was applied to CE body of quantified formula)
+  std::vector< Node > subs_lhs;
+  std::vector< Node > subs_rhs;
+  for( unsigned i=0; i<d_aux_vars.size(); i++ ){
+    Node r = d_aux_vars[i];
+    std::map< Node, Node >::iterator it = aux_subs.find( r );
+    if( it!=aux_subs.end() ){
+      addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second );
+    }else{
+      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!! type is " << r.getType() << std::endl;
+      Assert( false );
+    }
+  }
+
+  //apply substitutions to everything, if necessary
+  if( !subs_lhs.empty() ){
+    Trace("cbqi-proc") << "Applying substitution : " << std::endl;
+    for( unsigned i=0; i<subs_lhs.size(); i++ ){
+      Trace("cbqi-proc") << "  " << subs_lhs[i] << " -> " << subs_rhs[i] << std::endl;
+    }
+    for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node lit = it->second[i];
+        lit = lit.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+        lit = Rewriter::rewrite( lit );
+        it->second[i] = lit;
+      }
+    }
+    for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node n = it->second[i];
+        n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+        n = Rewriter::rewrite( n  );
+        it->second[i] = n;
+      }
+    }
+  }
+
+  //remove unecessary assertions
+  for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
+    std::vector< Node > akeep;
+    for( unsigned i=0; i<it->second.size(); i++ ){
+      Node n = it->second[i];
+      //must be an eligible term
+      if( isEligible( n ) ){
+        //must contain at least one variable
+        if( !d_prog_var[n].empty() ){
+          Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
+          akeep.push_back( n );
+        }else{
+          Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
+        }
+      }else{
+        Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl;
+      }
+    }
+    it->second.clear();
+    it->second.insert( it->second.end(), akeep.begin(), akeep.end() );
+  }
+
+  //remove duplicate terms from eqc
+  for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){
+    std::vector< Node > new_eqc;
+    for( unsigned i=0; i<it->second.size(); i++ ){
+      if( std::find( new_eqc.begin(), new_eqc.end(), it->second[i] )==new_eqc.end() ){
+        new_eqc.push_back( it->second[i] );
+      }
+    }
+    it->second.clear();
+    it->second.insert( it->second.end(), new_eqc.begin(), new_eqc.end() );
+  }
+}
+
+void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) {
+  r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+
+  std::vector< Node > cl;
+  cl.push_back( l );
+  std::vector< Node > cr;
+  cr.push_back( r );
+  for( unsigned i=0; i<subs_lhs.size(); i++ ){
+    Node nr = subs_rhs[i].substitute( cl.begin(), cl.end(), cr.begin(), cr.end() );
+    nr = Rewriter::rewrite( nr );
+    subs_rhs[i] = nr;
+  }
+
+  subs_lhs.push_back( l );
+  subs_rhs.push_back( r );
+}
+
+Node CegInstantiator::getModelValue( Node n ) {
+  return d_qe->getModel()->getValue( n );
+}
+
+Node CegInstantiator::getBoundVariable(TypeNode tn)
+{
+  unsigned index = 0;
+  std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>::iterator itb =
+      d_bound_var_index.find(tn);
+  if (itb != d_bound_var_index.end())
+  {
+    index = itb->second;
+  }
+  d_bound_var_index[tn] = index + 1;
+  while (index >= d_bound_var[tn].size())
+  {
+    std::stringstream ss;
+    ss << "x" << index;
+    Node x = NodeManager::currentNM()->mkBoundVar(ss.str(), tn);
+    d_bound_var[tn].push_back(x);
+  }
+  return d_bound_var[tn][index];
+}
+
+bool CegInstantiator::isSolvedAssertion(Node n) const
+{
+  return d_solved_asserts.find(n) != d_solved_asserts.end();
+}
+
+void CegInstantiator::markSolved(Node n, bool solved)
+{
+  if (solved)
+  {
+    d_solved_asserts.insert(n);
+  }
+  else if (isSolvedAssertion(n))
+  {
+    d_solved_asserts.erase(n);
+  }
+}
+
+void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) {
+  if( n.getKind()==FORALL ){
+    d_is_nested_quant = true;
+  }else if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( TermUtil::isBoolConnectiveTerm( n ) ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        collectCeAtoms( n[i], visited );
+      }
+    }else{
+      if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){
+        Trace("cbqi-ce-atoms") << "CE atoms : " << n << std::endl;
+        d_ce_atoms.push_back( n );
+      }
+    }
+  }
+}
+
+void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
+  Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl;
+  d_input_vars.clear();
+  d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end());
+
+  //Assert( d_vars.empty() );
+  d_vars.clear();
+  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]);
+  }
+
+  // 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::pair<const TheoryId, InstantiatorPreprocess*>& p : d_tipp)
+  {
+    p.second->registerCounterexampleLemma(lems, pvars);
+  }
+  // must register variables generated by preprocessors
+  Trace("cbqi-debug") << "Register variables from theory-specific methods "
+                      << d_input_vars.size() << " " << pvars.size() << " ..."
+                      << std::endl;
+  for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i)
+  {
+    Trace("cbqi-reg") << "  register theory preprocess variable : " << pvars[i]
+                      << std::endl;
+    registerVariable(pvars[i]);
+  }
+
+  //remove ITEs
+  IteSkolemMap iteSkolemMap;
+  d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
+  //Assert( d_aux_vars.empty() );
+  d_aux_vars.clear();
+  d_aux_eq.clear();
+  for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
+    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;
+    Node rlem = lems[i];
+    rlem = Rewriter::rewrite( rlem );
+    Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
+    //record the literals that imply auxiliary variables to be equal to terms
+    if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
+      if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
+        if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){
+          Node v = lems[i][1][0];
+          for( unsigned r=1; r<=2; r++ ){
+            d_aux_eq[rlem[r]][v] = lems[i][r][1];
+            Trace("cbqi-debug") << "  " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
+          }
+        }
+      }
+    }
+    /*else if( lems[i].getKind()==EQUAL && lems[i][0].getType().isBoolean() ){
+      //Boolean terms
+      if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][0] )!=d_aux_vars.end() ){
+        Node v = lems[i][0];
+        d_aux_eq[rlem][v] = lems[i][1];
+         Trace("cbqi-debug") << "  " << rlem << " implies " << v << " = " << lems[i][1] << std::endl;
+      }
+    }*/
+    lems[i] = rlem;
+  }
+
+  // determine variable order: must do Reals before Ints
+  Trace("cbqi-debug") << "Determine variable order..." << std::endl;
+  if (!d_vars.empty())
+  {
+    std::map<Node, unsigned> voo;
+    bool doSort = false;
+    std::vector<Node> vars;
+    std::map<TypeNode, std::vector<Node> > tvars;
+    for (unsigned i = 0, size = d_vars.size(); i < size; i++)
+    {
+      voo[d_vars[i]] = i;
+      d_var_order_index.push_back(0);
+      TypeNode tn = d_vars[i].getType();
+      if (tn.isInteger())
+      {
+        doSort = true;
+        tvars[tn].push_back(d_vars[i]);
+      }
+      else
+      {
+        vars.push_back(d_vars[i]);
+      }
+    }
+    if (doSort)
+    {
+      Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl;
+      for (std::pair<const TypeNode, std::vector<Node> >& vs : tvars)
+      {
+        vars.insert(vars.end(), vs.second.begin(), vs.second.end());
+      }
+
+      Trace("cbqi-debug") << "Consider variables in this order : " << std::endl;
+      for (unsigned i = 0; i < vars.size(); i++)
+      {
+        d_var_order_index[voo[vars[i]]] = i;
+        Trace("cbqi-debug") << "  " << vars[i] << " : " << vars[i].getType()
+                            << ", index was : " << voo[vars[i]] << std::endl;
+        d_vars[i] = vars[i];
+      }
+      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 );
+  }
+}
+
+
+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,
+                                    CegInstEffort effort)
+{
+  pv_prop.d_type = 0;
+  return ci->constructInstantiationInc(pv, n, pv_prop, sf);
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
new file mode 100644
index 000000000..03983fe1a
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -0,0 +1,783 @@
+/*********************                                                        */
+/*! \file ceg_instantiator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, 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 counterexample-guided quantifier instantiation
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+
+#include "theory/quantifiers_engine.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace arith {
+  class TheoryArith;
+}
+
+namespace quantifiers {
+
+class CegqiOutput {
+public:
+  virtual ~CegqiOutput() {}
+  virtual bool doAddInstantiation( std::vector< Node >& subs ) = 0;
+  virtual bool isEligibleForInstantiation( Node n ) = 0;
+  virtual bool addLemma( Node lem ) = 0;
+};
+
+class Instantiator;
+class InstantiatorPreprocess;
+
+/** Term Properties
+ *
+ * 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 {
+public:
+  TermProperties() : d_type(0) {}
+  virtual ~TermProperties() {}
+
+  // type of property for a term
+  //  for arithmetic this corresponds to bound type (0:equal, 1:upper bound, -1:lower bound)
+  int d_type;
+  // for arithmetic
+  Node d_coeff;
+  // 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(); }
+  // get modified term 
+  virtual Node getModifiedTerm( Node pv ) const {
+    if( !d_coeff.isNull() ){
+      return NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, pv );
+    }else{
+      return pv;
+    }
+  }
+  // compose property, should be such that: 
+  //   p.getModifiedTerm( this.getModifiedTerm( x ) ) = this_updated.getModifiedTerm( x )
+  virtual void composeProperty( TermProperties& p ){
+    if( !p.d_coeff.isNull() ){
+      if( d_coeff.isNull() ){
+        d_coeff = p.d_coeff;
+      }else{
+        d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, p.d_coeff ) );
+      }
+    }
+  }
+};
+
+/** Solved form
+ *  This specifies a substitution:
+ *  { d_props[i].getModifiedTerm(d_vars[i]) -> d_subs[i] | i = 0...|d_vars| }
+ */
+class SolvedForm {
+public:
+  // list of variables
+  std::vector< Node > d_vars;
+  // list of terms that they are substituted to
+  std::vector< Node > d_subs;
+  // properties for each variable
+  std::vector< TermProperties > d_props;
+  // the variables that have non-basic information regarding how they are substituted
+  //   an example is for linear arithmetic, we store "substitution with coefficients".
+  std::vector<Node> d_non_basic;
+  // push the substitution pv_prop.getModifiedTerm(pv) -> n
+  void push_back( Node pv, Node n, TermProperties& pv_prop ){
+    d_vars.push_back( pv );
+    d_subs.push_back( n );
+    d_props.push_back( pv_prop );
+    if( !pv_prop.isBasic() ){
+      d_non_basic.push_back( pv );
+      // update theta value
+      Node new_theta = getTheta();
+      if( new_theta.isNull() ){
+        new_theta = pv_prop.d_coeff;
+      }else{
+        new_theta = NodeManager::currentNM()->mkNode( kind::MULT, new_theta, pv_prop.d_coeff );
+        new_theta = Rewriter::rewrite( new_theta );
+      }
+      d_theta.push_back( new_theta );
+    }
+  }
+  // pop the substitution pv_prop.getModifiedTerm(pv) -> n
+  void pop_back( Node pv, Node n, TermProperties& pv_prop ){
+    d_vars.pop_back();
+    d_subs.pop_back();
+    d_props.pop_back();
+    if( !pv_prop.isBasic() ){
+      d_non_basic.pop_back();
+      // update theta value
+      d_theta.pop_back();
+    }
+  }
+  // is this solved form empty?
+  bool empty() { return d_vars.empty(); }
+public:
+  // theta values (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017)
+  std::vector< Node > d_theta;
+  // get the current value for theta (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017)
+  Node getTheta() {
+    if( d_theta.empty() ){
+      return Node::null();
+    }else{
+      return d_theta[d_theta.size()-1];
+    }
+  }
+};
+
+/** instantiation effort levels
+ *
+ * This effort is used to stratify the construction of
+ * instantiations for some theories that may result to
+ * using model value instantiations.
+ */
+enum CegInstEffort
+{
+  // uninitialized
+  CEG_INST_EFFORT_NONE,
+  // standard effort level
+  CEG_INST_EFFORT_STANDARD,
+  // standard effort level, but we have used model values
+  CEG_INST_EFFORT_STANDARD_MV,
+  // full effort level
+  CEG_INST_EFFORT_FULL
+};
+
+std::ostream& operator<<(std::ostream& os, CegInstEffort e);
+
+/** instantiation phase for variables
+ *
+ * This indicates the phase in which we constructed
+ * a substitution for individual variables.
+ */
+enum CegInstPhase
+{
+  // uninitialized
+  CEG_INST_PHASE_NONE,
+  // instantiation constructed during traversal of equivalence classes
+  CEG_INST_PHASE_EQC,
+  // instantiation constructed during solving equalities
+  CEG_INST_PHASE_EQUAL,
+  // instantiation constructed by looking at theory assertions
+  CEG_INST_PHASE_ASSERTION,
+  // instantiation constructed by querying model value
+  CEG_INST_PHASE_MVALUE,
+};
+
+std::ostream& operator<<(std::ostream& os, CegInstPhase phase);
+
+/** 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);
+  /** has this assertion been marked as solved? */
+  bool isSolvedAssertion(Node n) const;
+  /** marked solved */
+  void markSolved(Node n, bool solved = true);
+  //------------------------------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;
+  /** output channel of this instantiator */
+  CegqiOutput* d_out;
+  /** whether we are using delta for virtual term substitution
+    * (for quantified LRA).
+    */
+  bool d_use_vts_delta;
+  /** whether we are using infinity for virtual term substitution
+    * (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).
+    */
+  std::unordered_map<Node,
+                     std::unordered_set<Node, NodeHashFunction>,
+                     NodeHashFunction>
+      d_prog_var;
+  /** cache of the set of terms that we have established are
+   * 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;
+  /** solved asserts */
+  std::unordered_set<Node, NodeHashFunction> d_solved_asserts;
+  /** 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.
+   */
+  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
+   *
+   * This is a superset of the variables for the instantiations we are
+   * generating and sending on the output channel of this class.
+   */
+  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
+   *
+   * These are the variables, in order, for the instantiations we are generating
+   * and sending on the output channel of this class.
+   */
+  std::vector<Node> d_input_vars;
+  /** literals to equalities for aux vars
+   * This stores entries of the form
+   *   L -> ( k -> t )
+   * where
+   *   k is a variable in d_aux_vars,
+   *   L is a literal that if asserted implies that our
+   *    instantiation should map { k -> t }.
+   * For example, if a term of the form
+   *   ite( C, t1, t2 )
+   * was replaced by k, we get this (top-level) assertion:
+   *   ite( C, k=t1, k=t2 )
+   * The vector d_aux_eq contains the exact form of
+   * the literals in the above constraint that they would
+   * appear in assertions, meaning d_aux_eq may contain:
+   *   t1=k -> ( k -> t1 )
+   *   t2=k -> ( k -> t2 )
+   * where t1=k and t2=k are the rewritten form of
+   * k=t1 and k=t2 respectively.
+   */
+  std::map<Node, std::map<Node, Node> > d_aux_eq;
+  /** 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_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;
+  /** collect atoms */
+  void collectCeAtoms(Node n, std::map<Node, bool>& visited);
+  //-------------------------------end quantified formula info
+
+  //-------------------------------current state
+  /** the current effort level of the instantiator
+   * This indicates the effort Instantiator objects
+   * will put into the terms they return.
+   */
+  CegInstEffort d_effort;
+  /** for each variable, the instantiator used for that variable */
+  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;
+  /** map from variables to the phase in which we instantiated them */
+  std::map<Node, CegInstPhase> d_curr_iphase;
+  /** 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
+  * We wish to process the substitution: 
+  *   ( pv = n * sf )
+  * where pv is a variable with type tn, and * denotes application of substitution.
+  * The return value "ret" and pv_prop is such that the above equality is equivalent to
+  *   ( pv_prop.getModifiedTerm(pv) = ret )
+  */
+  Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, TermProperties& pv_prop, bool try_coeff = true ) {
+    return applySubstitution( tn, n, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic, pv_prop, try_coeff );
+  }
+  /** apply substitution, with solved form expanded to subs/prop/non_basic/vars */
+  Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, 
+                          std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff = true );
+  /** apply substitution to literal lit 
+  * The return value is equivalent to ( lit * sf )
+  * where * denotes application of substitution.
+  */
+  Node applySubstitutionToLiteral( Node lit, SolvedForm& sf ) {
+    return applySubstitutionToLiteral( lit, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic );
+  }
+  /** 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:
+  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.
+   */
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     CegInstEffort effort)
+  {
+  }
+
+  /** process equal term
+   *
+   * 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.
+   *
+   * Returns true if an instantiation was successfully added via a call to
+   * CegInstantiator::constructInstantiationInc.
+   */
+  virtual bool processEqualTerm(CegInstantiator* ci,
+                                SolvedForm& sf,
+                                Node pv,
+                                TermProperties& pv_prop,
+                                Node n,
+                                CegInstEffort effort);
+  /** process equal terms
+   *
+   * 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.
+   */
+  virtual bool processEqualTerms(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 std::vector<Node>& eqc,
+                                 CegInstEffort effort)
+  {
+    return false;
+  }
+
+  /** whether the instantiator implements processEquality */
+  virtual bool hasProcessEquality(CegInstantiator* ci,
+                                  SolvedForm& sf,
+                                  Node pv,
+                                  CegInstEffort 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,
+                               CegInstEffort effort)
+  {
+    return false;
+  }
+
+  /** whether the instantiator implements processAssertion for any literal */
+  virtual bool hasProcessAssertion(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   CegInstEffort effort)
+  {
+    return false;
+  }
+  /** has process assertion
+  *
+  * This method is called when the entailment:
+  *   E |= lit
+  * holds in current context E. Typically, lit belongs to the list of current
+  * assertions.
+  *
+  * This method is used to determine whether the instantiator implements
+  * processAssertion for literal lit.
+  *   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,
+                                   CegInstEffort effort)
+  {
+    return Node::null();
+  }
+  /** process assertion
+   * 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,
+                                CegInstEffort effort)
+  {
+    return false;
+  }
+  /** process assertions
+   *
+   * 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,
+                                 CegInstEffort effort)
+  {
+    return false;
+  }
+
+  /** 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,
+                             CegInstEffort effort)
+  {
+    return effort > CEG_INST_EFFORT_STANDARD;
+  }
+  /** do we allow the model value as instantiation for pv? */
+  virtual bool allowModelValue(CegInstantiator* ci,
+                               SolvedForm& sf,
+                               Node pv,
+                               CegInstEffort 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,
+                                                        CegInstEffort 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,
+                                                   CegInstEffort 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,
+                     CegInstEffort 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/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
new file mode 100644
index 000000000..e6e64201e
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -0,0 +1,1990 @@
+/*********************                                                        */
+/*! \file ceg_t_instantiator.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 theory-specific counterexample-guided quantifier instantiation
+ **/
+
+#include "theory/quantifiers/cegqi/ceg_t_instantiator.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/ematching/trigger.h"
+
+#include "theory/arith/arith_msum.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arith/theory_arith_private.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
+#include "util/random.h"
+
+#include <algorithm>
+#include <stack>
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+struct BvLinearAttributeId {};
+using BvLinearAttribute = expr::Attribute<BvLinearAttributeId, bool>;
+
+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;
+  Trace("cegqi-arith-bound2") << "Value : " << val << std::endl;
+  Assert( !e.getType().isInteger() || t.getType().isInteger() );
+  Assert( !e.getType().isInteger() || mt.getType().isInteger() );
+  //add rho value
+  //get the value of c*e
+  Node ceValue = me;
+  Node new_theta = theta;
+  if( !c.isNull() ){
+    Assert( c.getType().isInteger() );
+    ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c );
+    ceValue = Rewriter::rewrite( ceValue );
+    if( new_theta.isNull() ){
+      new_theta = c;
+    }else{
+      new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c );
+      new_theta = Rewriter::rewrite( new_theta );
+    }
+    Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl;
+    Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl;
+  }
+  if( !new_theta.isNull() && e.getType().isInteger() ){
+    Node rho;
+    //if( !mt.getType().isInteger() ){
+      //round up/down
+      //mt = NodeManager::currentNM()->mkNode(
+    //}
+    if( isLower ){
+      rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
+    }else{
+      rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue );
+    }
+    rho = Rewriter::rewrite( rho );
+    Trace("cegqi-arith-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl;
+    Trace("cegqi-arith-bound2") << "..." << rho << " mod " << new_theta << " = ";
+    rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta );
+    rho = Rewriter::rewrite( rho );
+    Trace("cegqi-arith-bound2") << rho << std::endl;
+    Kind rk = isLower ? PLUS : MINUS;
+    val = NodeManager::currentNM()->mkNode( rk, val, rho );
+    val = Rewriter::rewrite( val );
+    Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl;
+  }
+  if( !inf_coeff.isNull() ){
+    Assert( !d_vts_sym[0].isNull() );
+    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) );
+    val = Rewriter::rewrite( val );
+  }
+  if( !delta_coeff.isNull() ){
+    //create delta here if necessary
+    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta() ) );
+    val = Rewriter::rewrite( val );
+  }
+  return val;
+}
+
+//this isolates the atom into solved form
+//     veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf
+//  ensures val is Int if pv is Int, and val does not contain vts symbols
+int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
+  int ires = 0;
+  Trace("cegqi-arith-debug") << "isolate for " << pv << " in " << atom << std::endl;
+  std::map< Node, Node > msum;
+  if (ArithMSum::getMonomialSumLit(atom, msum))
+  {
+    Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl;
+    if( Trace.isOn("cegqi-arith-debug") ){
+      ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug");
+    }
+    TypeNode pvtn = pv.getType();
+    //remove vts symbols from polynomial
+    Node vts_coeff[2];
+    for( unsigned t=0; t<2; t++ ){
+      if( !d_vts_sym[t].isNull() ){
+        std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] );
+        if( itminf!=msum.end() ){
+          vts_coeff[t] = itminf->second;
+          if( vts_coeff[t].isNull() ){
+            vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+          }
+          //negate if coefficient on variable is positive
+          std::map< Node, Node >::iterator itv = msum.find( pv );
+          if( itv!=msum.end() ){
+            //multiply by the coefficient we will isolate for
+            if( itv->second.isNull() ){
+              vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
+            }else{
+              if( !pvtn.isInteger() ){
+                vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] );
+                vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] );
+              }else if( itv->second.getConst<Rational>().sgn()==1 ){
+                vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
+              }
+            }
+          }
+          Trace("cegqi-arith-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
+          msum.erase( d_vts_sym[t] );
+        }
+      }
+    }
+
+    ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
+    if( ires!=0 ){
+      Node realPart;
+      if( Trace.isOn("cegqi-arith-debug") ){
+        Trace("cegqi-arith-debug") << "Isolate : ";
+        if( !veq_c.isNull() ){
+          Trace("cegqi-arith-debug") << veq_c << " * ";
+        }
+        Trace("cegqi-arith-debug") << pv << " " << atom.getKind() << " " << val << std::endl;
+      }
+      if( options::cbqiAll() ){
+        // when not pure LIA/LRA, we must check whether the lhs contains pv
+        if( TermUtil::containsTerm( val, pv ) ){
+          Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
+          return 0;
+        }
+      }
+      if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
+        //redo, split integer/non-integer parts
+        bool useCoeff = false;
+        Integer coeff = ci->getQuantifiersEngine()->getTermUtil()->d_one.getConst<Rational>().getNumerator();
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          if( it->first.isNull() || it->first.getType().isInteger() ){
+            if( !it->second.isNull() ){
+              coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() );
+              useCoeff = true;
+            }
+          }
+        }
+        //multiply everything by this coefficient
+        Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) );
+        std::vector< Node > real_part;
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          if( useCoeff ){
+            if( it->second.isNull() ){
+              msum[it->first] = rcoeff;
+            }else{
+              msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) );
+            }
+          }
+          if( !it->first.isNull() && !it->first.getType().isInteger() ){
+            real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) );
+          }
+        }
+        //remove delta  TODO: check this
+        vts_coeff[1] = Node::null();
+        //multiply inf
+        if( !vts_coeff[0].isNull() ){
+          vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) );
+        }
+        realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermUtil()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) );
+        Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) );
+        //re-isolate
+        Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
+        ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
+        Trace("cegqi-arith-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
+        Trace("cegqi-arith-debug") << "                 real part : " << realPart << std::endl;
+        if( ires!=0 ){
+          int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1;
+          val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS,
+                                    NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ),
+                                    NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );  //TODO: round up for upper bounds?
+          Trace("cegqi-arith-debug") << "result : " << val << std::endl;
+          Assert( val.getType().isInteger() );
+        }
+      }
+    }
+    vts_coeff_inf = vts_coeff[0];
+    vts_coeff_delta = vts_coeff[1];
+    Trace("cegqi-arith-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl;
+  }else{
+    Trace("cegqi-arith-debug") << "fail : could not get monomial sum" << std::endl;
+  }
+  return ires;
+}
+
+void ArithInstantiator::reset(CegInstantiator* ci,
+                              SolvedForm& sf,
+                              Node pv,
+                              CegInstEffort 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++ ){
+    d_mbp_bounds[i].clear();
+    d_mbp_coeff[i].clear();
+    for( unsigned j=0; j<2; j++ ){
+      d_mbp_vts_coeff[i][j].clear();
+    }
+    d_mbp_lit[i].clear();
+  }
+}
+
+bool ArithInstantiator::processEquality(CegInstantiator* ci,
+                                        SolvedForm& sf,
+                                        Node pv,
+                                        std::vector<TermProperties>& term_props,
+                                        std::vector<Node>& terms,
+                                        CegInstEffort effort)
+{
+  Node eq_lhs = terms[0];
+  Node eq_rhs = terms[1];
+  Node lhs_coeff = term_props[0].d_coeff;
+  Node rhs_coeff = term_props[1].d_coeff;
+  //make the same coefficient
+  if( rhs_coeff!=lhs_coeff ){
+    if( !rhs_coeff.isNull() ){
+      Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl;
+      eq_lhs = NodeManager::currentNM()->mkNode( MULT, rhs_coeff, eq_lhs );
+      eq_lhs = Rewriter::rewrite( eq_lhs );
+    }
+    if( !lhs_coeff.isNull() ){
+      Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl;
+      eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff, eq_rhs );
+      eq_rhs = Rewriter::rewrite( eq_rhs );
+    }
+  }
+  Node eq = eq_lhs.eqNode( eq_rhs );
+  eq = Rewriter::rewrite( eq );
+  Node val;
+  TermProperties pv_prop;
+  Node vts_coeff_inf;
+  Node vts_coeff_delta;
+  //isolate pv in the equality
+  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->constructInstantiationInc(pv, val, pv_prop, sf))
+    {
+      return true;
+    }
+  }
+
+  return false;
+}
+
+Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
+                                            SolvedForm& sf,
+                                            Node pv,
+                                            Node lit,
+                                            CegInstEffort effort)
+{
+  Node atom = lit.getKind()==NOT ? lit[0] : lit;
+  bool pol = lit.getKind()!=NOT;
+  //arithmetic inequalities and disequalities
+  if (atom.getKind() == GEQ ||
+      (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())) {
+    return lit;
+  } else {
+    return Node::null();
+  }
+}
+
+bool ArithInstantiator::processAssertion(CegInstantiator* ci,
+                                         SolvedForm& sf,
+                                         Node pv,
+                                         Node lit,
+                                         Node alit,
+                                         CegInstEffort effort)
+{
+  Node atom = lit.getKind()==NOT ? lit[0] : lit;
+  bool pol = lit.getKind()!=NOT;
+  //arithmetic inequalities and disequalities
+  Assert( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) );
+  // get model value for pv
+  Node pv_value = ci->getModelValue( pv );
+  //cannot contain infinity?
+  Node vts_coeff_inf;
+  Node vts_coeff_delta;
+  Node val;
+  TermProperties pv_prop;
+  //isolate pv in the inequality
+  int ires = solve_arith( ci, pv, atom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta );
+  if( ires!=0 ){
+    //disequalities are either strict upper or lower bounds
+    unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2;
+    for( unsigned r=0; r<rmax; r++ ){
+      int uires = ires;
+      Node uval = val;
+      if( atom.getKind()==GEQ ){
+        //push negation downwards
+        if( !pol ){
+          uires = -ires;
+          if( d_type.isInteger() ){
+            uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+            uval = Rewriter::rewrite( uval );
+          }else{
+            Assert( d_type.isReal() );
+            //now is strict inequality
+            uires = uires*2;
+          }
+        }
+      }else{
+        bool is_upper;
+        if( options::cbqiModel() ){
+          // disequality is a disjunction : only consider the bound in the direction of the model
+          //first check if there is an infinity...
+          if( !vts_coeff_inf.isNull() ){
+            //coefficient or val won't make a difference, just compare with zero
+            Trace("cegqi-arith-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl;
+            Assert( vts_coeff_inf.isConst() );
+            is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 );
+          }else{
+            Node rhs_value = ci->getModelValue( val );
+            Node lhs_value = pv_prop.getModifiedTerm( pv_value );
+            if( !pv_prop.isBasic() ){
+              lhs_value = pv_prop.getModifiedTerm( pv_value );
+              lhs_value = Rewriter::rewrite( lhs_value );
+            }
+            Trace("cegqi-arith-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
+            Assert( lhs_value!=rhs_value );
+            Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
+            cmp = Rewriter::rewrite( cmp );
+            Assert( cmp.isConst() );
+            is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermUtil()->d_true );
+          }
+        }else{
+          is_upper = (r==0);
+        }
+        Assert( atom.getKind()==EQUAL && !pol );
+        if( d_type.isInteger() ){
+          uires = is_upper ? -1 : 1;
+          uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+          uval = Rewriter::rewrite( uval );
+        }else{
+          Assert( d_type.isReal() );
+          uires = is_upper ? -2 : 2;
+        }
+      }
+      if( Trace.isOn("cegqi-arith-bound-inf") ){
+        Node pvmod = pv_prop.getModifiedTerm( pv );
+        Trace("cegqi-arith-bound-inf") << "From " << lit << ", got : ";
+        Trace("cegqi-arith-bound-inf") << pvmod << " -> " << uval << ", styp = " << uires << std::endl;
+      }
+      //take into account delta
+      if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){
+        if( options::cbqiModel() ){
+          Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) );
+          if( vts_coeff_delta.isNull() ){
+            vts_coeff_delta = delta_coeff;
+          }else{
+            vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff );
+            vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta );
+          }
+        }else{
+          Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta();
+          uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
+          uval = Rewriter::rewrite( uval );
+        }
+      }
+      if( options::cbqiModel() ){
+        //just store bounds, will choose based on tighest bound
+        unsigned index = uires>0 ? 0 : 1;
+        d_mbp_bounds[index].push_back( uval );
+        d_mbp_coeff[index].push_back( pv_prop.d_coeff );
+        Trace("cegqi-arith-debug") << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl;
+        for( unsigned t=0; t<2; t++ ){
+          d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta );
+        }
+        d_mbp_lit[index].push_back( lit );
+      }else{
+        //try this bound
+        pv_prop.d_type = uires>0 ? 1 : -1;
+        if (ci->constructInstantiationInc(pv, uval, pv_prop, sf))
+        {
+          return true;
+        }
+      }
+    }
+  }
+
+
+  return false;
+}
+
+bool ArithInstantiator::processAssertions(CegInstantiator* ci,
+                                          SolvedForm& sf,
+                                          Node pv,
+                                          CegInstEffort effort)
+{
+  if (options::cbqiModel()) {
+    bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() );
+    bool upper_first = false;
+    if( options::cbqiMinBounds() ){
+      upper_first = d_mbp_bounds[1].size()<d_mbp_bounds[0].size();
+    }
+    int best_used[2];
+    std::vector< Node > t_values[3];
+    Node zero = ci->getQuantifiersEngine()->getTermUtil()->d_zero;
+    Node one = ci->getQuantifiersEngine()->getTermUtil()->d_one;
+    Node pv_value = ci->getModelValue( pv );
+    //try optimal bounds
+    for( unsigned r=0; r<2; r++ ){
+      int rr = upper_first ? (1-r) : r;
+      best_used[rr] = -1;
+      if( d_mbp_bounds[rr].empty() ){
+        if( use_inf ){
+          Trace("cegqi-arith-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl;
+          //no bounds, we do +- infinity
+          Node val = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type );
+          //TODO : rho value for infinity?
+          if( rr==0 ){
+            val = NodeManager::currentNM()->mkNode( UMINUS, val );
+            val = Rewriter::rewrite( val );
+          }
+          TermProperties pv_prop_no_bound;
+          if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf))
+          {
+            return true;
+          }
+        }
+      }else{
+        Trace("cegqi-arith-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl;
+        int best = -1;
+        Node best_bound_value[3];
+        for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){
+          Node value[3];
+          if( Trace.isOn("cegqi-arith-bound") ){
+            Assert( !d_mbp_bounds[rr][j].isNull() );
+            Trace("cegqi-arith-bound") << "  " << j << ": " << d_mbp_bounds[rr][j];
+            if( !d_mbp_vts_coeff[rr][0][j].isNull() ){
+              Trace("cegqi-arith-bound") << " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)";
+            }
+            if( !d_mbp_vts_coeff[rr][1][j].isNull() ){
+              Trace("cegqi-arith-bound") << " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)";
+            }
+            if( !d_mbp_coeff[rr][j].isNull() ){
+              Trace("cegqi-arith-bound") << " (div " << d_mbp_coeff[rr][j] << ")";
+            }
+            Trace("cegqi-arith-bound") << ", value = ";
+          }
+          t_values[rr].push_back( Node::null() );
+          //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts
+          bool new_best = true;
+          for( unsigned t=0; t<3; t++ ){
+            //get the value
+            if( t==0 ){
+              value[0] = d_mbp_vts_coeff[rr][0][j];
+              if( !value[0].isNull() ){
+                Trace("cegqi-arith-bound") << "( " << value[0] << " * INF ) + ";
+              }else{
+                value[0] = zero;
+              }
+            }else if( t==1 ){
+              Node t_value = ci->getModelValue( d_mbp_bounds[rr][j] );
+              t_values[rr][j] = t_value;
+              value[1] = t_value;
+              Trace("cegqi-arith-bound") << value[1];
+            }else{
+              value[2] = d_mbp_vts_coeff[rr][1][j];
+              if( !value[2].isNull() ){
+                Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )";
+              }else{
+                value[2] = zero;
+              }
+            }
+            //multiply by coefficient
+            if( value[t]!=zero && !d_mbp_coeff[rr][j].isNull() ){
+              Assert( d_mbp_coeff[rr][j].isConst() );
+              value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / d_mbp_coeff[rr][j].getConst<Rational>() ), value[t] );
+              value[t] = Rewriter::rewrite( value[t] );
+            }
+            //check if new best
+            if( best!=-1 ){
+              Assert( !value[t].isNull() && !best_bound_value[t].isNull() );
+              if( value[t]!=best_bound_value[t] ){
+                Kind k = rr==0 ? GEQ : LEQ;
+                Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] );
+                cmp_bound = Rewriter::rewrite( cmp_bound );
+                if( cmp_bound!=ci->getQuantifiersEngine()->getTermUtil()->d_true ){
+                  new_best = false;
+                  break;
+                }
+              }
+            }
+          }
+          Trace("cegqi-arith-bound") << std::endl;
+          if( new_best ){
+            for( unsigned t=0; t<3; t++ ){
+              best_bound_value[t] = value[t];
+            }
+            best = j;
+          }
+        }
+        if( best!=-1 ){
+          Trace("cegqi-arith-bound") << "...best bound is " << best << " : ";
+          if( best_bound_value[0]!=zero ){
+            Trace("cegqi-arith-bound") << "( " << best_bound_value[0] << " * INF ) + ";
+          }
+          Trace("cegqi-arith-bound") << best_bound_value[1];
+          if( best_bound_value[2]!=zero ){
+            Trace("cegqi-arith-bound") << " + ( " << best_bound_value[2] << " * DELTA )";
+          }
+          Trace("cegqi-arith-bound") << std::endl;
+          best_used[rr] = best;
+          //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict
+          if (!options::cbqiMidpoint() || d_type.isInteger()
+              || (ci->useVtsDelta() && d_mbp_vts_coeff[rr][1][best].isNull()))
+          {
+            Node val = d_mbp_bounds[rr][best];
+            val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.getTheta(),
+                                                d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] );
+            if( !val.isNull() ){
+              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->constructInstantiationInc(pv, val, pv_prop_bound, sf))
+              {
+                return true;
+              }
+            }
+          }
+        }
+      }
+    }
+    //if not using infinity, use model value of zero
+    if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){
+      Node val = zero;
+      TermProperties pv_prop_zero;
+      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->constructInstantiationInc(pv, val, pv_prop_zero, sf))
+        {
+          return true;
+        }
+      }
+    }
+    if( options::cbqiMidpoint() && !d_type.isInteger() ){
+      Node vals[2];
+      bool bothBounds = true;
+      Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl;
+      for( unsigned rr=0; rr<2; rr++ ){
+        int best = best_used[rr];
+        if( best==-1 ){
+          bothBounds = false;
+        }else{
+          vals[rr] = d_mbp_bounds[rr][best];
+          vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.getTheta(),
+                                                   d_mbp_vts_coeff[rr][0][best], Node::null() );
+        }
+        Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl;
+      }
+      Node val;
+      if( bothBounds ){
+        Assert( !vals[0].isNull() && !vals[1].isNull() );
+        if( vals[0]==vals[1] ){
+          val = vals[0];
+        }else{
+          val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ),
+                                                        NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) );
+          val = Rewriter::rewrite( val );
+        }
+      }else{
+        if( !vals[0].isNull() ){
+          val = NodeManager::currentNM()->mkNode( PLUS, vals[0], one );
+          val = Rewriter::rewrite( val );
+        }else if( !vals[1].isNull() ){
+          val = NodeManager::currentNM()->mkNode( MINUS, vals[1], one );
+          val = Rewriter::rewrite( val );
+        }
+      }
+      Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl;
+      if( !val.isNull() ){
+        TermProperties pv_prop_midpoint;
+        if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf))
+        {
+          return true;
+        }
+      }
+    }
+    //generally should not make it to this point FIXME: write proper assertion
+    //Assert( ( ci->hasNestedQuantification() && !options::cbqiNestedQE() ) || options::cbqiAll() );
+
+    if( options::cbqiNopt() ){
+      //try non-optimal bounds (heuristic, may help when nested quantification) ?
+      Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl;
+      for( unsigned r=0; r<2; r++ ){
+        int rr = upper_first ? (1-r) : r;
+        for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){
+          if( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull() ) ){
+            Node val = getModelBasedProjectionValue( ci, pv, d_mbp_bounds[rr][j], rr==0, d_mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.getTheta(),
+                                                     d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] );
+            if( !val.isNull() ){
+              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->constructInstantiationInc(
+                      pv, val, pv_prop_nopt_bound, sf))
+              {
+                return true;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  return false;
+}
+
+bool ArithInstantiator::needsPostProcessInstantiationForVariable(
+    CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort 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,
+    CegInstEffort 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();
+  Assert( !sf.d_props[index].isBasic() );
+  Node eq_lhs = sf.d_props[index].getModifiedTerm( sf.d_vars[index] );
+  if( Trace.isOn("cegqi-arith-debug") ){
+    Trace("cegqi-arith-debug") << "Normalize substitution for ";
+    Trace("cegqi-arith-debug") << eq_lhs << " = " << sf.d_subs[index] << std::endl;
+  }
+  Assert( sf.d_vars[index].getType().isInteger() );
+  //must ensure that divisibility constraints are met
+  //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful
+  Node eq_rhs = sf.d_subs[index];
+  Node eq = eq_lhs.eqNode( eq_rhs );
+  eq = Rewriter::rewrite( eq );
+  Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl;
+  std::map< Node, Node > msum;
+  if (ArithMSum::getMonomialSumLit(eq, msum))
+  {
+    Node veq;
+    if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) != 0)
+    {
+      Node veq_c;
+      if( veq[0]!=sf.d_vars[index] ){
+        Node veq_v;
+        if (ArithMSum::getMonomial(veq[0], veq_c, veq_v))
+        {
+          Assert( veq_v==sf.d_vars[index] );
+        }
+      }
+      sf.d_subs[index] = veq[1];
+      if( !veq_c.isNull() ){
+        sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c );
+        Trace("cegqi-arith-debug") << "...bound type is : " << sf.d_props[index].d_type << std::endl;
+        //intger division rounding up if from a lower bound
+        if( sf.d_props[index].d_type==1 && options::cbqiRoundUpLowerLia() ){
+          sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
+            NodeManager::currentNM()->mkNode( ITE,
+              NodeManager::currentNM()->mkNode( EQUAL,
+                NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ),
+                ci->getQuantifiersEngine()->getTermUtil()->d_zero ),
+              ci->getQuantifiersEngine()->getTermUtil()->d_zero, ci->getQuantifiersEngine()->getTermUtil()->d_one )
+          );
+        }
+      }
+      Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl;
+    }else{
+      Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl;
+      return false;
+    }
+  }else{
+    Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl;
+    return false;
+  }
+  return true;
+}
+
+void DtInstantiator::reset(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort)
+{
+}
+
+Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) {
+  Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl;
+  Node ret;
+  if( !a.isNull() && a==v ){
+    ret = sb;
+  }else if( !b.isNull() && b==v ){
+    ret = sa;
+  }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){
+    if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){
+      if( a.getOperator()==b.getOperator() ){
+        for( unsigned i=0; i<a.getNumChildren(); i++ ){
+          Node s = solve_dt( v, a[i], b[i], sa[i], sb[i] );
+          if( !s.isNull() ){
+            return s;
+          }
+        }
+      }
+    }else{
+      unsigned cindex = Datatype::indexOf( a.getOperator().toExpr() );
+      TypeNode tn = a.getType();
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      for( unsigned i=0; i<a.getNumChildren(); i++ ){
+        Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), sb );
+        Node s = solve_dt( v, a[i], Node::null(), sa[i], nn );
+        if( !s.isNull() ){
+          return s;
+        }
+      }
+    }
+  }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){
+    return solve_dt( v, b, a, sb, sa );
+  }
+  if( !ret.isNull() ){
+    //ensure does not contain
+    if( TermUtil::containsTerm( ret, v ) ){
+      ret = Node::null();
+    }
+  }
+  return ret;
+}
+
+bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
+                                       SolvedForm& sf,
+                                       Node pv,
+                                       std::vector<Node>& eqc,
+                                       CegInstEffort effort)
+{
+  Trace("cegqi-dt-debug") << "try based on constructors in equivalence class."
+                          << std::endl;
+  // look in equivalence class for a constructor
+  for( unsigned k=0; k<eqc.size(); k++ ){
+    Node n = eqc[k];
+    if( n.getKind()==APPLY_CONSTRUCTOR ){
+      Trace("cegqi-dt-debug") << "...try based on constructor term " << n << std::endl;
+      std::vector< Node > children;
+      children.push_back( n.getOperator() );
+      const Datatype& dt = ((DatatypeType)(d_type).toType()).getDatatype();
+      unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() );
+      //now must solve for selectors applied to pv
+      for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
+        Node c = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( d_type.toType(), j ) ), pv );
+        ci->pushStackVariable( c );
+        children.push_back( c );
+      }
+      Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
+      TermProperties pv_prop_dt;
+      if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf))
+      {
+        return true;
+      }else{
+        //cleanup
+        for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
+          ci->popStackVariable();
+        }
+        break;
+      }
+    }
+  }
+  return false;
+}
+
+bool DtInstantiator::processEquality(CegInstantiator* ci,
+                                     SolvedForm& sf,
+                                     Node pv,
+                                     std::vector<TermProperties>& term_props,
+                                     std::vector<Node>& terms,
+                                     CegInstEffort effort)
+{
+  Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] );
+  if( !val.isNull() ){
+    TermProperties pv_prop;
+    if (ci->constructInstantiationInc(pv, val, pv_prop, sf))
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
+void EprInstantiator::reset(CegInstantiator* ci,
+                            SolvedForm& sf,
+                            Node pv,
+                            CegInstEffort effort)
+{
+  d_equal_terms.clear();
+}
+
+bool EprInstantiator::processEqualTerm(CegInstantiator* ci,
+                                       SolvedForm& sf,
+                                       Node pv,
+                                       TermProperties& pv_prop,
+                                       Node n,
+                                       CegInstEffort effort)
+{
+  if( options::quantEprMatching() ){
+    Assert( pv_prop.isBasic() );
+    d_equal_terms.push_back( n );
+    return false;
+  }else{
+    pv_prop.d_type = 0;
+    return ci->constructInstantiationInc(pv, n, pv_prop, sf);
+  }
+}
+
+void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ) {
+  if( index==catom.getNumChildren() ){
+    Assert( tat->hasNodeData() );
+    Node gcatom = tat->getNodeData();
+    Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom << std::endl;
+    for( unsigned i=0; i<catom.getNumChildren(); i++ ){
+      if( catom[i]==pv ){
+        Trace("cegqi-epr") << "...increment " << gcatom[i] << std::endl;
+        match_score[gcatom[i]]++;
+      }else{
+        //recursive matching
+        computeMatchScore( ci, pv, catom[i], gcatom[i], match_score );
+      }
+    }
+  }else{
+    std::map< TNode, TermArgTrie >::iterator it = tat->d_data.find( arg_reps[index] );
+    if( it!=tat->d_data.end() ){
+      computeMatchScore( ci, pv, catom, arg_reps, &it->second, index+1, match_score );
+    }
+  }
+}
+
+void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) {
+  if( inst::Trigger::isAtomicTrigger( catom ) && TermUtil::containsTerm( catom, pv ) ){
+    Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl;
+    std::vector< Node > arg_reps;
+    for( unsigned j=0; j<catom.getNumChildren(); j++ ){
+      arg_reps.push_back( ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) );
+    }
+    if( ci->getQuantifiersEngine()->getMasterEqualityEngine()->hasTerm( eqc ) ){
+      Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc );
+      Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom );
+      TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op );
+      Trace("cegqi-epr") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl;
+      if( tat ){
+        computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score );
+      }
+    }
+  }
+}
+
+struct sortEqTermsMatch {
+  std::map< Node, int > d_match_score;
+  bool operator() (Node i, Node j) {
+    int match_score_i = d_match_score[i];
+    int match_score_j = d_match_score[j];
+    return match_score_i>match_score_j || ( match_score_i==match_score_j && i<j );
+  }
+};
+
+bool EprInstantiator::processEqualTerms(CegInstantiator* ci,
+                                        SolvedForm& sf,
+                                        Node pv,
+                                        std::vector<Node>& eqc,
+                                        CegInstEffort effort)
+{
+  if( options::quantEprMatching() ){
+    //heuristic for best matching constant
+    sortEqTermsMatch setm;
+    for( unsigned i=0; i<ci->getNumCEAtoms(); i++ ){
+      Node catom = ci->getCEAtom( i );
+      computeMatchScore( ci, pv, catom, catom, setm.d_match_score );
+    }
+    //sort by match score
+    std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm );
+    TermProperties pv_prop;
+    pv_prop.d_type = 0;
+    for( unsigned i=0; i<d_equal_terms.size(); i++ ){
+      if (ci->constructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+// this class can be used to query the model value through the CegInstaniator class
+class CegInstantiatorBvInverterQuery : public BvInverterQuery
+{
+ public:
+  CegInstantiatorBvInverterQuery(CegInstantiator* ci)
+      : BvInverterQuery(), d_ci(ci)
+  {
+  }
+  ~CegInstantiatorBvInverterQuery() {}
+  /** return the model value of n */
+  Node getModelValue( Node n ) {
+    return d_ci->getModelValue( n );
+  }
+  /** get bound variable of type tn */
+  Node getBoundVariable(TypeNode tn) { return d_ci->getBoundVariable(tn); }
+ protected:
+  // pointer to class that is able to query model values
+  CegInstantiator * d_ci;
+};
+
+BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
+    : Instantiator(qe, tn), d_tried_assertion_inst(false)
+{
+  // get the global inverter utility
+  // this must be global since we need to:
+  // * process Skolem functions properly across multiple variables within the same quantifier
+  // * cache Skolem variables uniformly across multiple quantified formulas
+  d_inverter = qe->getBvInverter();
+}
+
+BvInstantiator::~BvInstantiator(){
+
+}
+void BvInstantiator::reset(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort)
+{
+  d_inst_id_counter = 0;
+  d_var_to_inst_id.clear();
+  d_inst_id_to_term.clear();
+  d_inst_id_to_alit.clear();
+  d_var_to_curr_inst_id.clear();
+  d_alit_to_model_slack.clear();
+  d_tried_assertion_inst = false;
+}
+
+void BvInstantiator::processLiteral(CegInstantiator* ci,
+                                    SolvedForm& sf,
+                                    Node pv,
+                                    Node lit,
+                                    Node alit,
+                                    CegInstEffort effort)
+{
+  Assert(d_inverter != NULL);
+  // find path to pv
+  std::vector<unsigned> path;
+  Node sv = d_inverter->getSolveVariable(pv.getType());
+  Node pvs = ci->getModelValue(pv);
+  Trace("cegqi-bv") << "Get path to pv : " << lit << std::endl;
+  Node slit = d_inverter->getPathToPv(lit, pv, sv, pvs, path);
+  if (!slit.isNull())
+  {
+    CegInstantiatorBvInverterQuery m(ci);
+    unsigned iid = d_inst_id_counter;
+    Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl;
+    Node inst = d_inverter->solveBvLit(sv, slit, path, &m);
+    if (!inst.isNull())
+    {
+      inst = Rewriter::rewrite(inst);
+      if (inst.isConst() || !ci->hasNestedQuantification())
+      {
+        Trace("cegqi-bv") << "...solved form is " << inst << std::endl;
+        // store information for id and increment
+        d_var_to_inst_id[pv].push_back(iid);
+        d_inst_id_to_term[iid] = inst;
+        d_inst_id_to_alit[iid] = alit;
+        d_inst_id_counter++;
+      }
+    }
+    else
+    {
+      Trace("cegqi-bv") << "...failed to solve." << std::endl;
+    }
+  }
+}
+
+Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
+                                         SolvedForm& sf,
+                                         Node pv,
+                                         Node lit,
+                                         CegInstEffort effort)
+{
+  if (effort == CEG_INST_EFFORT_FULL)
+  {
+    // always use model values at full effort
+    return Node::null();
+  }
+  Node atom = lit.getKind() == NOT ? lit[0] : lit;
+  bool pol = lit.getKind() != NOT;
+  Kind k = atom.getKind();
+  if (k != EQUAL && k != BITVECTOR_ULT && k != BITVECTOR_SLT)
+  {
+    // others are unhandled
+    return Node::null();
+  }
+  else if (!atom[0].getType().isBitVector())
+  {
+    return Node::null();
+  }
+  else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP
+           || (pol && k == EQUAL))
+  {
+    return lit;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node s = atom[0];
+  Node t = atom[1];
+
+  Node sm = ci->getModelValue(s);
+  Node tm = ci->getModelValue(t);
+  Assert(!sm.isNull() && sm.isConst());
+  Assert(!tm.isNull() && tm.isConst());
+  Trace("cegqi-bv") << "Model value: " << std::endl;
+  Trace("cegqi-bv") << "   " << s << " " << k << " " << t << " is "
+                    << std::endl;
+  Trace("cegqi-bv") << "   " << sm << " <> " << tm << std::endl;
+
+  Node ret;
+  if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK)
+  {
+    // if using slack, we convert constraints to a positive equality based on
+    // the current model M, e.g.:
+    //   (not) s ~ t  --->  s = t + ( s^M - t^M )
+    if (sm != tm)
+    {
+      Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm));
+      Assert(slack.isConst());
+      // remember the slack value for the asserted literal
+      d_alit_to_model_slack[lit] = slack;
+      ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack));
+      Trace("cegqi-bv") << "Slack is " << slack << std::endl;
+    }
+    else
+    {
+      ret = s.eqNode(t);
+    }
+  } else {
+    // turn disequality into an inequality
+    // e.g. s != t becomes s < t or t < s
+    if (k == EQUAL)
+    {
+      if (Random::getRandom().pickWithProb(0.5))
+      {
+        std::swap(s, t);
+      }
+      pol = true;
+    }
+    // otherwise, we optimistically solve for the boundary point of an
+    // inequality, for example:
+    //   for s < t, we solve s+1 = t
+    //   for ~( s < t ), we solve s = t
+    // notice that this equality does not necessarily hold in the model, and
+    // hence the corresponding instantiation strategy is not guaranteed to be
+    // monotonic.
+    if (!pol)
+    {
+      ret = s.eqNode(t);
+    } else {
+      Node bv_one = bv::utils::mkOne(bv::utils::getSize(s));
+      ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t);
+    }
+  }
+  Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
+  return ret;
+}
+
+bool BvInstantiator::processAssertion(CegInstantiator* ci,
+                                      SolvedForm& sf,
+                                      Node pv,
+                                      Node lit,
+                                      Node alit,
+                                      CegInstEffort 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 
+    //   this should remove instances of non-invertible operators, and "linearize" lit with respect to pv as much as possible
+    Node rlit = rewriteAssertionForSolvePv(ci, pv, lit);
+    if( Trace.isOn("cegqi-bv") ){
+      Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv << " in " << lit << std::endl;
+      if( lit!=rlit ){
+        Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl;
+      }
+    }
+    if (!rlit.isNull())
+    {
+      processLiteral(ci, sf, pv, rlit, alit, effort);
+    }
+  }
+  return false;
+}
+
+bool BvInstantiator::useModelValue(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   CegInstEffort effort)
+{
+  return !d_tried_assertion_inst
+         && (effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort());
+}
+
+bool BvInstantiator::processAssertions(CegInstantiator* ci,
+                                       SolvedForm& sf,
+                                       Node pv,
+                                       CegInstEffort 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;
+    // if interleaving, do not do inversion half the time
+    if (!options::cbqiBvInterleaveValue() || Random::getRandom().pickWithProb(0.5))
+    {
+      bool firstVar = sf.empty();
+      // get inst id list
+      if (Trace.isOn("cegqi-bv"))
+      {
+        Trace("cegqi-bv") << "  " << iti->second.size()
+                          << " candidate instantiations for " << pv << " : "
+                          << std::endl;
+        if (firstVar)
+        {
+          Trace("cegqi-bv") << "  ...this is the first variable" << std::endl;
+        }
+      }
+      // until we have a model-preserving selection function for BV, this must
+      // be heuristic (we only pick one literal)
+      // hence we randomize the list
+      // this helps robustness, since picking the same literal every time may
+      // lead to a stream of value instantiations, whereas with randomization
+      // we may find an invertible literal that leads to a useful instantiation.
+      std::random_shuffle(iti->second.begin(), iti->second.end());
+
+      if (Trace.isOn("cegqi-bv"))
+      {
+        for (unsigned j = 0, size = iti->second.size(); j < size; j++)
+        {
+          unsigned inst_id = iti->second[j];
+          Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
+          Node inst_term = d_inst_id_to_term[inst_id];
+          Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end());
+          Node alit = d_inst_id_to_alit[inst_id];
+
+          // get the slack value introduced for the asserted literal
+          Node curr_slack_val;
+          std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
+              d_alit_to_model_slack.find(alit);
+          if (itms != d_alit_to_model_slack.end())
+          {
+            curr_slack_val = itms->second;
+          }
+
+          // debug printing
+          Trace("cegqi-bv") << "   [" << j << "] : ";
+          Trace("cegqi-bv") << inst_term << std::endl;
+          if (!curr_slack_val.isNull()) {
+            Trace("cegqi-bv") << "   ...with slack value : " << curr_slack_val
+                              << std::endl;
+          }
+          Trace("cegqi-bv-debug") << "   ...from : " << alit << std::endl;
+          Trace("cegqi-bv") << std::endl;
+        }
+      }
+
+      // Now, try all instantiation ids we want to try
+      // Typically we try only one, otherwise worst-case performance
+      // for constructing instantiations is exponential on the number of
+      // variables in this quantifier prefix.
+      bool ret = false;
+      bool tryMultipleInst = firstVar && options::cbqiMultiInst();
+      bool revertOnSuccess = tryMultipleInst;
+      for (unsigned j = 0, size = iti->second.size(); j < size; j++)
+      {
+        unsigned inst_id = iti->second[j];
+        Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
+        Node inst_term = d_inst_id_to_term[inst_id];
+        Node alit = d_inst_id_to_alit[inst_id];
+        // try instantiation pv -> inst_term
+        TermProperties pv_prop_bv;
+        Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term
+                          << std::endl;
+        d_var_to_curr_inst_id[pv] = inst_id;
+        d_tried_assertion_inst = true;
+        ci->markSolved(alit);
+        if (ci->constructInstantiationInc(
+                pv, inst_term, pv_prop_bv, sf, revertOnSuccess))
+        {
+          ret = true;
+        }
+        ci->markSolved(alit, false);
+        // we are done unless we try multiple instances
+        if (!tryMultipleInst)
+        {
+          break;
+        }
+      }
+      if (ret)
+      {
+        return true;
+      }
+      Trace("cegqi-bv") << "...failed to add instantiation for " << pv
+                        << std::endl;
+      d_var_to_curr_inst_id.erase(pv);
+    } else {
+      Trace("cegqi-bv") << "...do not do instantiation for " << pv
+                        << " (skip, based on heuristic)" << std::endl;
+    }
+  }
+
+  return false;
+}
+
+Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
+                                                Node pv,
+                                                Node lit)
+{
+  // result of rewriting the visited term
+  std::stack<std::unordered_map<TNode, Node, TNodeHashFunction> > visited;
+  visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
+  // whether the visited term contains pv
+  std::unordered_map<TNode, bool, TNodeHashFunction> visited_contains_pv;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::unordered_map<TNode, Node, TNodeHashFunction> curr_subs;
+  std::stack<std::stack<TNode> > visit;
+  TNode cur;
+  visit.push(std::stack<TNode>());
+  visit.top().push(lit);
+  do {
+    cur = visit.top().top();
+    visit.top().pop();
+    it = visited.top().find(cur);
+
+    if (it == visited.top().end())
+    {
+      std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itc =
+          curr_subs.find(cur);
+      if (itc != curr_subs.end())
+      {
+        visited.top()[cur] = itc->second;
+      }
+      else
+      {
+        if (cur.getKind() == CHOICE)
+        {
+          // must replace variables of choice functions
+          // with new variables to avoid variable
+          // capture when considering substitutions
+          // with multiple literals.
+          Node bv = ci->getBoundVariable(cur[0][0].getType());
+          // should not have captured variables
+          Assert(curr_subs.find(cur[0][0]) == curr_subs.end());
+          curr_subs[cur[0][0]] = bv;
+          // we cannot cache the results of subterms
+          // of this choice expression since we are
+          // now in the context { cur[0][0] -> bv },
+          // hence we push a context here
+          visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
+          visit.push(std::stack<TNode>());
+        }
+        visited.top()[cur] = Node::null();
+        visit.top().push(cur);
+        for (unsigned i = 0; i < cur.getNumChildren(); i++)
+        {
+          visit.top().push(cur[i]);
+        }
+      }
+    } else if (it->second.isNull()) {
+      Node ret;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        children.push_back(cur.getOperator());
+      }
+      bool contains_pv = ( cur==pv );
+      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
+        it = visited.top().find(cur[i]);
+        Assert(it != visited.top().end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cur[i] != it->second;
+        children.push_back(it->second);
+        contains_pv = contains_pv || visited_contains_pv[cur[i]];
+      }
+      // careful that rewrites above do not affect whether this term contains pv
+      visited_contains_pv[cur] = contains_pv;
+
+      // rewrite the term
+      ret = rewriteTermForSolvePv(pv, cur, children, visited_contains_pv);
+
+      // return original if the above function does not produce a result
+      if (ret.isNull()) {
+        if (childChanged) {
+          ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
+        }else{
+          ret = cur;
+        }
+      }
+
+      /* We need to update contains_pv also for rewritten nodes, since
+       * the normalizePv* functions rely on the information if pv occurs in a
+       * rewritten node or not. */
+      if (ret != cur)
+      {
+        contains_pv = (ret == pv);
+        for (unsigned i = 0, size = ret.getNumChildren(); i < size; ++i)
+        {
+          contains_pv = contains_pv || visited_contains_pv[ret[i]];
+        }
+        visited_contains_pv[ret] = contains_pv;
+      }
+
+      // if was choice, pop context
+      if (cur.getKind() == CHOICE)
+      {
+        Assert(curr_subs.find(cur[0][0]) != curr_subs.end());
+        curr_subs.erase(cur[0][0]);
+        visited.pop();
+        visit.pop();
+        Assert(visited.size() == visit.size());
+        Assert(!visit.empty());
+      }
+
+      visited.top()[cur] = ret;
+    }
+  } while (!visit.top().empty());
+  Assert(visited.size() == 1);
+  Assert(visited.top().find(lit) != visited.top().end());
+  Assert(!visited.top().find(lit)->second.isNull());
+
+  Node result = visited.top()[lit];
+
+  if (Trace.isOn("cegqi-bv-nl"))
+  {
+    std::vector<TNode> trace_visit;
+    std::unordered_set<TNode, TNodeHashFunction> trace_visited;
+
+    trace_visit.push_back(result);
+    do
+    {
+      cur = trace_visit.back();
+      trace_visit.pop_back();
+
+      if (trace_visited.find(cur) == trace_visited.end())
+      {
+        trace_visited.insert(cur);
+        trace_visit.insert(trace_visit.end(), cur.begin(), cur.end());
+      }
+      else if (cur == pv)
+      {
+        Trace("cegqi-bv-nl")
+            << "NONLINEAR LITERAL for " << pv << " : " << lit << std::endl;
+      }
+    } while (!trace_visit.empty());
+  }
+
+  return result;
+}
+
+/**
+ * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t,
+ * or -pv * t. Extracting the coefficient of multiplications only succeeds if
+ * the multiplication are normalized with normalizePvMult.
+ *
+ * If sucessful it returns
+ *   1    if n ==  pv,
+ *  -1    if n == -pv,
+ *   t    if n ==  pv * t,
+ *  -t    if n == -pv * t.
+ * If n is not a linear term, a null node is returned.
+ */
+static Node getPvCoeff(TNode pv, TNode n)
+{
+  bool neg = false;
+  Node coeff;
+
+  if (n.getKind() == BITVECTOR_NEG)
+  {
+    neg = true;
+    n = n[0];
+  }
+
+  if (n == pv)
+  {
+    coeff = bv::utils::mkOne(bv::utils::getSize(pv));
+  }
+  /* All multiplications are normalized to pv * (t1 * t2). */
+  else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute()))
+  {
+    Assert(n.getNumChildren() == 2);
+    Assert(n[0] == pv);
+    coeff = n[1];
+  }
+  else /* n is in no form to extract the coefficient for pv */
+  {
+    Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in "
+                         << n << std::endl;
+    return Node::null();
+  }
+  Assert(!coeff.isNull());
+
+  if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff);
+  return coeff;
+}
+
+/**
+ * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks
+ * terms in which pv occurs.
+ * For example,
+ *
+ *  a * -pv * b * c
+ *
+ * is rewritten to
+ *
+ *  pv * -(a * b * c)
+ *
+ * Returns the normalized node if the resulting term is linear w.r.t. pv and
+ * a null node otherwise. If pv does not occur in children it returns a
+ * multiplication over children.
+ */
+static Node normalizePvMult(
+    TNode pv,
+    const std::vector<Node>& children,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  bool neg, neg_coeff = false;
+  bool found_pv = false;
+  NodeManager* nm;
+  NodeBuilder<> nb(BITVECTOR_MULT);
+  BvLinearAttribute is_linear;
+
+  nm = NodeManager::currentNM();
+  for (TNode nc : children)
+  {
+    if (!contains_pv[nc])
+    {
+      nb << nc;
+      continue;
+    }
+
+    neg = false;
+    if (nc.getKind() == BITVECTOR_NEG)
+    {
+      neg = true;
+      nc = nc[0];
+    }
+
+    if (!found_pv && nc == pv)
+    {
+      found_pv = true;
+      neg_coeff = neg;
+      continue;
+    }
+    else if (!found_pv && nc.getKind() == BITVECTOR_MULT
+             && nc.getAttribute(is_linear))
+    {
+      Assert(nc.getNumChildren() == 2);
+      Assert(nc[0] == pv);
+      Assert(!contains_pv[nc[1]]);
+      found_pv = true;
+      neg_coeff = neg;
+      nb << nc[1];
+      continue;
+    }
+    return Node::null(); /* non-linear */
+  }
+  Assert(nb.getNumChildren() > 0);
+
+  Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode();
+  if (neg_coeff)
+  {
+    coeff = nm->mkNode(BITVECTOR_NEG, coeff);
+  }
+  coeff = Rewriter::rewrite(coeff);
+  unsigned size_coeff = bv::utils::getSize(coeff);
+  Node zero = bv::utils::mkZero(size_coeff);
+  if (coeff == zero)
+  {
+    return zero;
+  }
+  Node result;
+  if (found_pv)
+  {
+    if (coeff == bv::utils::mkOne(size_coeff))
+    {
+      return pv;
+    }
+    result = nm->mkNode(BITVECTOR_MULT, pv, coeff);
+    contains_pv[result] = true;
+    result.setAttribute(is_linear, true);
+  }
+  else
+  {
+    result = coeff;
+  }
+  return result;
+}
+
+#ifdef CVC4_ASSERTIONS
+static bool isLinearPlus(
+    TNode n,
+    TNode pv,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  Node coeff;
+  Assert(n.getAttribute(BvLinearAttribute()));
+  Assert(n.getNumChildren() == 2);
+  if (n[0] != pv)
+  {
+    Assert(n[0].getKind() == BITVECTOR_MULT);
+    Assert(n[0].getNumChildren() == 2);
+    Assert(n[0][0] == pv);
+    Assert(!contains_pv[n[0][1]]);
+  }
+  Assert(!contains_pv[n[1]]);
+  coeff = getPvCoeff(pv, n[0]);
+  Assert(!coeff.isNull());
+  Assert(!contains_pv[coeff]);
+  return true;
+}
+#endif
+
+/**
+ * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks
+ * terms in which pv occurs.
+ * For example,
+ *
+ *  a * pv + b + c * -pv
+ *
+ * is rewritten to
+ *
+ *  pv * (a - c) + b
+ *
+ * Returns the normalized node if the resulting term is linear w.r.t. pv and
+ * a null node otherwise. If pv does not occur in children it returns an
+ * addition over children.
+ */
+static Node normalizePvPlus(
+    Node pv,
+    const std::vector<Node>& children,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  NodeManager* nm;
+  NodeBuilder<> nb_c(BITVECTOR_PLUS);
+  NodeBuilder<> nb_l(BITVECTOR_PLUS);
+  BvLinearAttribute is_linear;
+  bool neg;
+
+  nm = NodeManager::currentNM();
+  for (TNode nc : children)
+  {
+    if (!contains_pv[nc])
+    {
+      nb_l << nc;
+      continue;
+    }
+
+    neg = false;
+    if (nc.getKind() == BITVECTOR_NEG)
+    {
+      neg = true;
+      nc = nc[0];
+    }
+
+    if (nc == pv
+        || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear)))
+    {
+      Node coeff = getPvCoeff(pv, nc);
+      Assert(!coeff.isNull());
+      if (neg)
+      {
+        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
+      }
+      nb_c << coeff;
+      continue;
+    }
+    else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear))
+    {
+      Assert(isLinearPlus(nc, pv, contains_pv));
+      Node coeff = getPvCoeff(pv, nc[0]);
+      Assert(!coeff.isNull());
+      Node leaf = nc[1];
+      if (neg)
+      {
+        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
+        leaf = nm->mkNode(BITVECTOR_NEG, leaf);
+      }
+      nb_c << coeff;
+      nb_l << leaf;
+      continue;
+    }
+    /* can't collect coefficients of 'pv' in 'cur' -> non-linear */
+    return Node::null();
+  }
+  Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0);
+
+  Node pv_mult_coeffs, result;
+  if (nb_c.getNumChildren() > 0)
+  {
+    Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode();
+    coeffs = Rewriter::rewrite(coeffs);
+    result = pv_mult_coeffs = normalizePvMult(pv, {pv, coeffs}, contains_pv);
+  }
+
+  if (nb_l.getNumChildren() > 0)
+  {
+    Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode();
+    leafs = Rewriter::rewrite(leafs);
+    Node zero = bv::utils::mkZero(bv::utils::getSize(pv));
+    /* pv * 0 + t --> t */
+    if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero)
+    {
+      result = leafs;
+    }
+    else
+    {
+      result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs);
+      contains_pv[result] = true;
+      result.setAttribute(is_linear, true);
+    }
+  }
+  Assert(!result.isNull());
+  return result;
+}
+
+/**
+ * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv
+ * marks terms in which pv occurs.
+ * For example, equality
+ *
+ *   -pv * a + b = c + pv
+ *
+ * rewrites to
+ *
+ *   pv * (-a - 1) = c - b.
+ */
+static Node normalizePvEqual(
+    Node pv,
+    const std::vector<Node>& children,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  Assert(children.size() == 2);
+
+  NodeManager* nm = NodeManager::currentNM();
+  BvLinearAttribute is_linear;
+  Node coeffs[2], leafs[2];
+  bool neg;
+  TNode child;
+
+  for (unsigned i = 0; i < 2; ++i)
+  {
+    child = children[i];
+    neg = false;
+    if (child.getKind() == BITVECTOR_NEG)
+    {
+      neg = true;
+      child = child[0];
+    }
+    if (child.getAttribute(is_linear) || child == pv)
+    {
+      if (child.getKind() == BITVECTOR_PLUS)
+      {
+        Assert(isLinearPlus(child, pv, contains_pv));
+        coeffs[i] = getPvCoeff(pv, child[0]);
+        leafs[i] = child[1];
+      }
+      else
+      {
+        Assert(child.getKind() == BITVECTOR_MULT || child == pv);
+        coeffs[i] = getPvCoeff(pv, child);
+      }
+    }
+    if (neg)
+    {
+      if (!coeffs[i].isNull())
+      {
+        coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]);
+      }
+      if (!leafs[i].isNull())
+      {
+        leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]);
+      }
+    }
+  }
+
+  if (coeffs[0].isNull() || coeffs[1].isNull())
+  {
+    return Node::null();
+  }
+
+  Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]);
+  coeff = Rewriter::rewrite(coeff);
+  std::vector<Node> mult_children = {pv, coeff};
+  Node lhs = normalizePvMult(pv, mult_children, contains_pv);
+
+  Node rhs;
+  if (!leafs[0].isNull() && !leafs[1].isNull())
+  {
+    rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]);
+  }
+  else if (!leafs[0].isNull())
+  {
+    rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]);
+  }
+  else if (!leafs[1].isNull())
+  {
+    rhs = leafs[1];
+  }
+  else
+  {
+    rhs = bv::utils::mkZero(bv::utils::getSize(pv));
+  }
+  rhs = Rewriter::rewrite(rhs);
+
+  if (lhs == rhs)
+  {
+    return bv::utils::mkTrue();
+  }
+
+  Node result = lhs.eqNode(rhs);
+  contains_pv[result] = true;
+  return result;
+}
+
+Node BvInstantiator::rewriteTermForSolvePv(
+    Node pv,
+    Node n,
+    std::vector<Node>& children,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  NodeManager* nm = NodeManager::currentNM();
+
+  // [1] rewrite cases of non-invertible operators
+
+  if (n.getKind() == EQUAL)
+  {
+    TNode lhs = children[0];
+    TNode rhs = children[1];
+
+    /* rewrite: x * x = x -> x < 2 */
+    if ((lhs == pv && rhs.getKind() == BITVECTOR_MULT && rhs[0] == pv
+         && rhs[1] == pv)
+        || (rhs == pv && lhs.getKind() == BITVECTOR_MULT && lhs[0] == pv
+            && lhs[1] == pv))
+    {
+      return nm->mkNode(
+          BITVECTOR_ULT,
+          pv,
+          bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2))));
+    }
+
+    if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs])
+    {
+      Node result = normalizePvEqual(pv, children, contains_pv);
+      if (!result.isNull())
+      {
+        Trace("cegqi-bv-nl")
+            << "Normalize " << n << " to " << result << std::endl;
+      }
+      else
+      {
+        Trace("cegqi-bv-nl")
+            << "Nonlinear " << n.getKind() << " " << n << std::endl;
+      }
+      return result;
+    }
+  }
+  else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS)
+  {
+    if (options::cbqiBvLinearize() && contains_pv[n])
+    {
+      Node result;
+      if (n.getKind() == BITVECTOR_MULT)
+      {
+        result = normalizePvMult(pv, children, contains_pv);
+      }
+      else
+      {
+        result = normalizePvPlus(pv, children, contains_pv);
+      }
+      if (!result.isNull())
+      {
+        Trace("cegqi-bv-nl")
+            << "Normalize " << n << " to " << result << std::endl;
+        return result;
+      }
+      else
+      {
+        Trace("cegqi-bv-nl")
+            << "Nonlinear " << n.getKind() << " " << n << std::endl;
+      }
+    }
+  }
+
+  // [2] try to rewrite non-linear literals -> linear literals
+
+  return Node::null();
+}
+
+/** sort bv extract interval
+ *
+ * This sorts lists of bitvector extract terms where
+ * ((_ extract i1 i2) t) < ((_ extract j1 j2) t)
+ * if i1>j1 or i1=j1 and i2>j2.
+ */
+struct SortBvExtractInterval
+{
+  bool operator()(Node i, Node j)
+  {
+    Assert(i.getKind() == BITVECTOR_EXTRACT);
+    Assert(j.getKind() == BITVECTOR_EXTRACT);
+    BitVectorExtract ie = i.getOperator().getConst<BitVectorExtract>();
+    BitVectorExtract je = j.getOperator().getConst<BitVectorExtract>();
+    if (ie.high > je.high)
+    {
+      return true;
+    }
+    else if (ie.high == je.high)
+    {
+      Assert(ie.low != je.low);
+      return ie.low > je.low;
+    }
+    return false;
+  }
+};
+
+void BvInstantiatorPreprocess::registerCounterexampleLemma(
+    std::vector<Node>& lems, std::vector<Node>& ce_vars)
+{
+  // new variables
+  std::vector<Node> vars;
+  // new lemmas
+  std::vector<Node> new_lems;
+
+  if (options::cbqiBvRmExtract())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
+    // map from terms to bitvector extracts applied to that term
+    std::map<Node, std::vector<Node> > extract_map;
+    std::unordered_set<TNode, TNodeHashFunction> visited;
+    for (unsigned i = 0, size = lems.size(); i < size; i++)
+    {
+      Trace("cegqi-bv-pp-debug2") << "Register ce lemma # " << i << " : "
+                                  << lems[i] << std::endl;
+      collectExtracts(lems[i], extract_map, visited);
+    }
+    for (std::pair<const Node, std::vector<Node> >& es : extract_map)
+    {
+      // sort based on the extract start position
+      std::vector<Node>& curr_vec = es.second;
+
+      SortBvExtractInterval sbei;
+      std::sort(curr_vec.begin(), curr_vec.end(), sbei);
+
+      unsigned width = es.first.getType().getBitVectorSize();
+
+      // list of points b such that:
+      //   b>0 and we must start a segment at (b-1)  or  b==0
+      std::vector<unsigned> boundaries;
+      boundaries.push_back(width);
+      boundaries.push_back(0);
+
+      Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl;
+      for (unsigned i = 0, size = curr_vec.size(); i < size; i++)
+      {
+        Trace("cegqi-bv-pp") << "  " << i << " : " << curr_vec[i] << std::endl;
+        BitVectorExtract e =
+            curr_vec[i].getOperator().getConst<BitVectorExtract>();
+        if (std::find(boundaries.begin(), boundaries.end(), e.high + 1)
+            == boundaries.end())
+        {
+          boundaries.push_back(e.high + 1);
+        }
+        if (std::find(boundaries.begin(), boundaries.end(), e.low)
+            == boundaries.end())
+        {
+          boundaries.push_back(e.low);
+        }
+      }
+      std::sort(boundaries.rbegin(), boundaries.rend());
+
+      // make the extract variables
+      std::vector<Node> children;
+      for (unsigned i = 1; i < boundaries.size(); i++)
+      {
+        Assert(boundaries[i - 1] > 0);
+        Node ex = bv::utils::mkExtract(
+            es.first, boundaries[i - 1] - 1, boundaries[i]);
+        Node var =
+            nm->mkSkolem("ek",
+                         ex.getType(),
+                         "variable to represent disjoint extract region");
+        children.push_back(var);
+        vars.push_back(var);
+      }
+
+      Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children);
+      Assert(conc.getType() == es.first.getType());
+      Node eq_lem = conc.eqNode(es.first);
+      Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl;
+      new_lems.push_back(eq_lem);
+      Trace("cegqi-bv-pp") << "...finished processing extracts for term "
+                            << es.first << std::endl;
+    }
+    Trace("cegqi-bv-pp") << "-----done remove extracts" << std::endl;
+  }
+
+  if (!vars.empty())
+  {
+    // could try applying subs -> vars here
+    // in practice, this led to worse performance
+
+    Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..."
+                         << std::endl;
+    lems.insert(lems.end(), new_lems.begin(), new_lems.end());
+    Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..."
+                         << std::endl;
+    ce_vars.insert(ce_vars.end(), vars.begin(), vars.end());
+  }
+}
+
+void BvInstantiatorPreprocess::collectExtracts(
+    Node lem,
+    std::map<Node, std::vector<Node> >& extract_map,
+    std::unordered_set<TNode, TNodeHashFunction>& visited)
+{
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(lem);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.getKind() != FORALL)
+      {
+        if (cur.getKind() == BITVECTOR_EXTRACT)
+        {
+          extract_map[cur[0]].push_back(cur);
+        }
+
+        for (const Node& nc : cur)
+        {
+          visit.push_back(nc);
+        }
+      }
+    }
+  } while (!visit.empty());
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h
new file mode 100644
index 000000000..b9c7e2024
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h
@@ -0,0 +1,331 @@
+/*********************                                                        */
+/*! \file ceg_t_instantiator.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 theory-specific counterexample-guided quantifier instantiation
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CEG_T_INSTANTIATOR_H
+#define __CVC4__CEG_T_INSTANTIATOR_H
+
+#include "theory/quantifiers/bv_inverter.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+
+#include <unordered_set>
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** TODO (#1367) : document these classes, also move to separate files. */
+
+class ArithInstantiator : public Instantiator {
+ public:
+  ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
+  virtual ~ArithInstantiator(){}
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     CegInstEffort effort) override;
+  virtual bool hasProcessEquality(CegInstantiator* ci,
+                                  SolvedForm& sf,
+                                  Node pv,
+                                  CegInstEffort effort) override
+  {
+    return true;
+  }
+  virtual bool processEquality(CegInstantiator* ci,
+                               SolvedForm& sf,
+                               Node pv,
+                               std::vector<TermProperties>& term_props,
+                               std::vector<Node>& terms,
+                               CegInstEffort effort) override;
+  virtual bool hasProcessAssertion(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   CegInstEffort effort) override
+  {
+    return true;
+  }
+  virtual Node hasProcessAssertion(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   Node lit,
+                                   CegInstEffort effort) override;
+  virtual bool processAssertion(CegInstantiator* ci,
+                                SolvedForm& sf,
+                                Node pv,
+                                Node lit,
+                                Node alit,
+                                CegInstEffort effort) override;
+  virtual bool processAssertions(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 CegInstEffort effort) override;
+  virtual bool needsPostProcessInstantiationForVariable(
+      CegInstantiator* ci,
+      SolvedForm& sf,
+      Node pv,
+      CegInstEffort effort) override;
+  virtual bool postProcessInstantiationForVariable(
+      CegInstantiator* ci,
+      SolvedForm& sf,
+      Node pv,
+      CegInstEffort 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 {
+public:
+  DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
+  virtual ~DtInstantiator(){}
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     CegInstEffort effort) override;
+  virtual bool processEqualTerms(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 std::vector<Node>& eqc,
+                                 CegInstEffort effort) override;
+  virtual bool hasProcessEquality(CegInstantiator* ci,
+                                  SolvedForm& sf,
+                                  Node pv,
+                                  CegInstEffort effort) override
+  {
+    return true;
+  }
+  virtual bool processEquality(CegInstantiator* ci,
+                               SolvedForm& sf,
+                               Node pv,
+                               std::vector<TermProperties>& term_props,
+                               std::vector<Node>& terms,
+                               CegInstEffort 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 {
+ public:
+  EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
+  virtual ~EprInstantiator(){}
+  virtual void reset(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     CegInstEffort effort) override;
+  virtual bool processEqualTerm(CegInstantiator* ci,
+                                SolvedForm& sf,
+                                Node pv,
+                                TermProperties& pv_prop,
+                                Node n,
+                                CegInstEffort effort) override;
+  virtual bool processEqualTerms(CegInstantiator* ci,
+                                 SolvedForm& sf,
+                                 Node pv,
+                                 std::vector<Node>& eqc,
+                                 CegInstEffort 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 {
+ public:
+  BvInstantiator(QuantifiersEngine* qe, TypeNode tn);
+  ~BvInstantiator() override;
+  void reset(CegInstantiator* ci,
+             SolvedForm& sf,
+             Node pv,
+             CegInstEffort effort) override;
+  bool hasProcessAssertion(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort) override
+  {
+    return true;
+  }
+  Node hasProcessAssertion(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           Node lit,
+                           CegInstEffort effort) override;
+  bool processAssertion(CegInstantiator* ci,
+                        SolvedForm& sf,
+                        Node pv,
+                        Node lit,
+                        Node alit,
+                        CegInstEffort effort) override;
+  bool processAssertions(CegInstantiator* ci,
+                         SolvedForm& sf,
+                         Node pv,
+                         CegInstEffort effort) override;
+  /** use model value
+   *
+   * We allow model values if we have not already tried an assertion,
+   * and only at levels below full if cbqiFullEffort is false.
+   */
+  bool useModelValue(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     CegInstEffort effort) override;
+  std::string identify() const override { return "Bv"; }
+
+ private:
+  // point to the bv inverter class
+  BvInverter * d_inverter;
+  unsigned d_inst_id_counter;
+  /** information about solved forms */
+  std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction > d_var_to_inst_id;
+  std::unordered_map< unsigned, Node > d_inst_id_to_term;
+  std::unordered_map<unsigned, Node> d_inst_id_to_alit;
+  // variable to current id we are processing
+  std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id;
+  /** the amount of slack we added for asserted literals */
+  std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack;
+  /** whether we have tried an instantiation based on assertion in this round */
+  bool d_tried_assertion_inst;
+  /** rewrite assertion for solve pv
+  * returns a literal that is equivalent to lit that leads to best solved form for pv
+  */
+  Node rewriteAssertionForSolvePv(CegInstantiator* ci, Node pv, Node lit);
+  /** rewrite term for solve pv
+   * This is a helper function for rewriteAssertionForSolvePv.
+   * If this returns non-null value ret, then this indicates
+   * that n should be rewritten to ret. It is called as
+   * a "post-rewrite", that is, after the children of n
+   * have been rewritten and stored in the vector children.
+   *
+   * contains_pv stores whether certain nodes contain pv.
+   * where we guarantee that all subterms of terms in children
+   * appear in the domain of contains_pv.
+   */
+  Node rewriteTermForSolvePv(
+      Node pv,
+      Node n,
+      std::vector<Node>& children,
+      std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+  /** process literal, called from processAssertion
+  * lit is the literal to solve for pv that has been rewritten according to
+  * 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,
+                      CegInstEffort effort);
+};
+
+/** Bitvector instantiator preprocess
+ *
+ * This class implements preprocess techniques that are helpful for
+ * counterexample-guided instantiation, such as introducing variables
+ * that refer to disjoint bit-vector extracts.
+ */
+class BvInstantiatorPreprocess : public InstantiatorPreprocess
+{
+ public:
+  BvInstantiatorPreprocess() {}
+  ~BvInstantiatorPreprocess() override {}
+  /** register counterexample lemma
+   *
+   * This method modifies the contents of lems based on the extract terms
+   * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces
+   * a dummy equality so that segments of terms t under extracts can be solved
+   * independently.
+   *
+   * For example:
+   *   P[ ((extract 7 4) t), ((extract 3 0) t)]
+   *     becomes:
+   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
+   *   t = concat( x74, x30 )
+   * where x74 and x30 are fresh variables of type BV_4.
+   *
+   * Another example:
+   *   P[ ((extract 7 3) t), ((extract 4 0) t)]
+   *     becomes:
+   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
+   *   t = concat( x75, x44, x30 )
+   * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4
+   * respectively.
+   *
+   * Notice we leave the original conjecture alone. This is done for performance
+   * since the added equalities ensure we are able to construct the proper
+   * solved forms for variables in t and for the intermediate variables above.
+   */
+  void registerCounterexampleLemma(std::vector<Node>& lems,
+                                   std::vector<Node>& ce_vars) override;
+
+ private:
+  /** collect extracts
+   *
+   * This method collects all extract terms in lem
+   * and stores them in d_extract_map.
+   * visited is the terms we've already visited.
+   */
+  void collectExtracts(Node lem,
+                       std::map<Node, std::vector<Node> >& extract_map,
+                       std::unordered_set<TNode, TNodeHashFunction>& visited);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
new file mode 100644
index 000000000..8de3dbfcb
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -0,0 +1,828 @@
+/*********************                                                        */
+/*! \file inst_strategy_cbqi.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King, Morgan Deters
+ ** 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 counterexample-guided quantifier instantiation strategies
+ **/
+#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
+
+#include "options/quantifiers_options.h"
+#include "smt/term_formula_removal.h"
+#include "theory/arith/partial_model.h"
+#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"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#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;
+using namespace CVC4::theory::arith;
+
+#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
+
+InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
+  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), 
+d_elim_quants( qe->getSatContext() ),
+d_nested_qe_waitlist_size( qe->getUserContext() ),
+d_nested_qe_waitlist_proc( qe->getUserContext() )
+//, d_added_inst( qe->getUserContext() )
+{
+  d_qid_count = 0;
+}
+
+bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
+  return e>=Theory::EFFORT_LAST_CALL;
+}
+
+QuantifiersModule::QEffort InstStrategyCbqi::needsModel(Theory::Effort e)
+{
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+      return QEFFORT_STANDARD;
+    }
+  }
+  return QEFFORT_NONE;
+}
+
+bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
+  if( !hasAddedCbqiLemma( q ) ){
+    d_added_cbqi_lemma.insert( q );
+    Trace("cbqi-debug") << "Do cbqi for " << q << std::endl;
+    //add cbqi lemma
+    //get the counterexample literal
+    Node ceLit = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q );
+    Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q );
+    if( !ceBody.isNull() ){
+      //add counterexample lemma
+      Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
+      //require any decision on cel to be phase=true
+      d_quantEngine->addRequirePhase( ceLit, true );
+      Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
+      //add counterexample lemma
+      lem = Rewriter::rewrite( lem );
+      Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl;
+      registerCounterexampleLemma( q, lem );
+      
+      //totality lemmas for EPR
+      QuantEPR * qepr = d_quantEngine->getQuantEPR();
+      if( qepr!=NULL ){   
+        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+          TypeNode tn = q[0][i].getType();
+          if( tn.isSort() ){
+            if( qepr->isEPR( tn ) ){
+              //add totality lemma
+              std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
+              if( itc!=qepr->d_consts.end() ){
+                Assert( !itc->second.empty() );
+                Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
+                std::vector< Node > disj;
+                for( unsigned j=0; j<itc->second.size(); j++ ){
+                  disj.push_back( ic.eqNode( itc->second[j] ) );
+                }
+                Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
+                Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
+                d_quantEngine->getOutputChannel().lemma( tlem );
+              }else{
+                Assert( false );
+              }                  
+            }else{
+              Assert( !options::cbqiAll() );
+            }
+          }
+        }
+      }      
+      
+      //compute dependencies between quantified formulas
+      if( options::cbqiLitDepend() || options::cbqiInnermost() ){
+        std::vector< Node > ics;
+        TermUtil::computeVarContains( q, ics );
+        d_parent_quant[q].clear();
+        d_children_quant[q].clear();
+        std::vector< Node > dep;
+        for( unsigned i=0; i<ics.size(); i++ ){
+          Node qi = ics[i].getAttribute(InstConstantAttribute());
+          if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
+            d_parent_quant[q].push_back( qi );
+            d_children_quant[qi].push_back( q );
+            Assert( hasAddedCbqiLemma( qi ) );
+            Node qicel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( qi );
+            dep.push_back( qi );
+            dep.push_back( qicel );
+          }
+        }
+        if( !dep.empty() ){
+          Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) );
+          Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl;
+          d_quantEngine->getOutputChannel().lemma( dep_lemma );
+        }
+      }
+      
+      //must register all sub-quantifiers of counterexample lemma, register their lemmas
+      std::vector< Node > quants;
+      TermUtil::computeQuantContains( lem, quants );
+      for( unsigned i=0; i<quants.size(); i++ ){
+        if( doCbqi( quants[i] ) ){
+          registerCbqiLemma( quants[i] );
+        }
+        if( options::cbqiNestedQE() ){
+          //record these as counterexample quantifiers
+          QAttributes qa;
+          QuantAttributes::computeQuantAttributes( quants[i], qa );
+          if( !qa.d_qid_num.isNull() ){
+            d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
+            d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
+            Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
+          }
+        }
+      }
+    }
+    return true;
+  }else{
+    return false;
+  }
+}
+
+void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
+  d_cbqi_set_quant_inactive = false;
+  d_incomplete_check = false;
+  d_active_quant.clear();
+  //check if any cbqi lemma has not been added yet
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
+    if( doCbqi( q ) ){
+      Assert( hasAddedCbqiLemma( q ) );
+      if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
+        d_active_quant[q] = true;
+        Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
+        Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q );
+        bool value;
+        if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
+          Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
+          if( !value ){
+            if( d_quantEngine->getValuation().isDecision( cel ) ){
+              Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
+            }else{
+              Trace("cbqi") << "Inactive : " << q << std::endl;
+              d_quantEngine->getModel()->setQuantifierActive( q, false );
+              d_cbqi_set_quant_inactive = true;
+              d_active_quant.erase( q );
+              d_elim_quants.insert( q );
+              Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
+              //process from waitlist
+              while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
+                int index = d_nested_qe_waitlist_proc[q];
+                Assert( index>=0 );
+                Assert( index<(int)d_nested_qe_waitlist[q].size() );
+                Node nq = d_nested_qe_waitlist[q][index];
+                Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
+                Node dqelem = nq.eqNode( nqeqn ); 
+                Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
+                d_quantEngine->getOutputChannel().lemma( dqelem );
+                d_nested_qe_waitlist_proc[q] = index + 1;
+              }
+            }
+          }
+        }else{
+          Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
+        }
+      }
+    }
+  }
+
+  //refinement: only consider innermost active quantified formulas
+  if( options::cbqiInnermost() ){
+    if( !d_children_quant.empty() && !d_active_quant.empty() ){
+      Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl;
+      std::vector< Node > ninner;
+      for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
+        std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
+        if( itc!=d_children_quant.end() ){
+          for( unsigned j=0; j<itc->second.size(); j++ ){
+            if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
+              Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
+              ninner.push_back( it->first );
+              break;
+            }
+          }
+        }
+      } 
+      Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
+      for( unsigned i=0; i<ninner.size(); i++ ){
+        Assert( d_active_quant.find( ninner[i] )!=d_active_quant.end() );
+        d_active_quant.erase( ninner[i] );
+      }
+      Assert( !d_active_quant.empty() );
+      Trace("cbqi-debug") << "...done removing." << std::endl;
+    }
+  }
+  
+  processResetInstantiationRound( effort );
+}
+
+void InstStrategyCbqi::check(Theory::Effort e, QEffort quant_e)
+{
+  if (quant_e == QEFFORT_STANDARD)
+  {
+    Assert( !d_quantEngine->inConflict() );
+    double clSet = 0;
+    if( Trace.isOn("cbqi-engine") ){
+      clSet = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
+    }
+    unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+    for( int ee=0; ee<=1; ee++ ){
+      //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      //  Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+      //  if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+      for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
+        Node q = it->first;
+        Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
+        if( d_nested_qe.find( q )==d_nested_qe.end() ){
+          process( q, e, ee );
+          if( d_quantEngine->inConflict() ){
+            break;
+          }
+        }else{
+          Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
+          Assert( false );
+        }
+      }
+      if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+        break;
+      }
+    }
+    if( Trace.isOn("cbqi-engine") ){
+      if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+        Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+      }
+      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
+    }
+  }
+}
+
+bool InstStrategyCbqi::checkComplete() {
+  if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
+    return false;
+  }else{
+    return true;
+  }
+}
+
+bool InstStrategyCbqi::checkCompleteFor( Node q ) {
+  std::map< Node, int >::iterator it = d_do_cbqi.find( q );
+  if( it!=d_do_cbqi.end() ){
+    return it->second>0;
+  }else{
+    return false;
+  }
+}
+
+Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){
+  std::map< Node, Node >::iterator it = visited.find( n );
+  if( it==visited.end() ){
+    Node ret = n;
+    if( n.getKind()==FORALL ){
+      QAttributes qa;
+      QuantAttributes::computeQuantAttributes( n, qa );
+      if( qa.d_qid_num.isNull() ){
+        std::vector< Node > rc;
+        rc.push_back( n[0] );
+        rc.push_back( getIdMarkedQuantNode( n[1], visited ) );
+        Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
+        QuantIdNumAttribute ida;
+        avar.setAttribute(ida,d_qid_count);
+        d_qid_count++;
+        std::vector< Node > iplc;
+        iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
+        if( n.getNumChildren()==3 ){
+          for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
+            iplc.push_back( n[2][i] );
+          }
+        }
+        rc.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
+        ret = NodeManager::currentNM()->mkNode( FORALL, rc );
+      }
+    }else if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = getIdMarkedQuantNode( n[i], visited );
+        childChanged = childChanged || nc!=n[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return it->second;
+  }
+}
+
+void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
+  if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
+    if( d_do_cbqi[q]==2 ){
+      //take full ownership of the quantified formula
+      d_quantEngine->setOwner( q, this );
+      
+      //mark all nested quantifiers with id
+      if( options::cbqiNestedQE() ){
+        std::map< Node, Node > visited;
+        Node mq = getIdMarkedQuantNode( q[1], visited );
+        if( mq!=q[1] ){
+          //do not do cbqi
+          d_do_cbqi[q] = false;
+          //instead do reduction
+          std::vector< Node > qqc;
+          qqc.push_back( q[0] );
+          qqc.push_back( mq );
+          if( q.getNumChildren()==3 ){
+            qqc.push_back( q[2] );
+          }
+          Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc );
+          Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq );
+          Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
+          d_quantEngine->getOutputChannel().lemma( mlem );
+        }
+      }
+    }
+  }
+}
+
+void InstStrategyCbqi::registerQuantifier( Node q ) {
+  if( doCbqi( q ) ){
+    if( registerCbqiLemma( q ) ){
+      Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
+    }
+  }
+}
+
+Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) {
+  // there is a nested quantified formula (forall y. nq[y,x]) such that 
+  //    q is (forall y. nq[y,t]) for ground terms t,
+  //    ceq is (forall y. nq[y,e]) for CE variables e.
+  // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e].
+  // in this case, q is equivalent to the quantifier-free formula C[t].
+  if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
+    d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
+    Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl;
+    Trace("cbqi-nqe") << "  " << ceq << std::endl; 
+    Trace("cbqi-nqe") << "  " << d_nested_qe[ceq] << std::endl;
+    //should not contain quantifiers
+    Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) );
+  }
+  Assert( d_quantEngine->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() );
+  //replace inst constants with instantiation
+  Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(),
+                                          d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
+                                          inst_terms.begin(), inst_terms.end() );
+  if( doVts ){
+    //do virtual term substitution
+    ret = Rewriter::rewrite( ret );
+    ret = d_quantEngine->getTermUtil()->rewriteVtsSymbols( ret );
+  }
+  Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl;
+  Trace("cbqi-nqe") << "  " << n << std::endl; 
+  Trace("cbqi-nqe") << "  " << ret << std::endl;
+  return ret;
+}
+
+Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) {
+  if( visited.find( n )==visited.end() ){
+    Node ret = n;
+    if( n.getKind()==FORALL ){
+      QAttributes qa;
+      QuantAttributes::computeQuantAttributes( n, qa );
+      if( !qa.d_qid_num.isNull() ){
+        //if it has an id, check whether we have done quantifier elimination for this id
+        std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
+        if( it!=d_id_to_ce_quant.end() ){
+          Node ceq = it->second;
+          bool doNestedQe = d_elim_quants.contains( ceq );
+          if( doNestedQe ){
+            ret = doNestedQENode( q, ceq, n, inst_terms, doVts );
+          }else{
+            Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl;
+            Node nr = Rewriter::rewrite( n );
+            Trace("cbqi-nqe") << "  " << ceq << std::endl;
+            Trace("cbqi-nqe") << "  " << nr << std::endl;
+            int wlsize = d_nested_qe_waitlist_size[ceq] + 1;
+            d_nested_qe_waitlist_size[ceq] = wlsize;
+            if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){
+              d_nested_qe_waitlist[ceq][wlsize] = nr;
+            }else{
+              d_nested_qe_waitlist[ceq].push_back( nr );
+            }
+            d_nested_qe_info[nr].d_q = q;
+            d_nested_qe_info[nr].d_inst_terms.clear();
+            d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
+            d_nested_qe_info[nr].d_doVts = doVts;
+            //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
+            Assert( !options::cbqiInnermost() );
+          }
+        } 
+      } 
+    }else if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = doNestedQERec( q, n[i], visited, inst_terms, doVts );
+        childChanged = childChanged || nc!=n[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return n;
+  }  
+}
+
+Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) {
+  std::map< Node, Node > visited;
+  return doNestedQERec( q, lem, visited, inst_terms, doVts );
+}
+
+void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
+  Trace("cbqi-debug") << "Counterexample lemma  : " << lem << std::endl;
+  d_quantEngine->addLemma( lem, false );
+}
+
+bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()!=BOUND_VARIABLE && TermUtil::hasBoundVarAttr( n ) ){
+      if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
+        Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n  << std::endl;
+        return true;
+      }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){
+        Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl;
+        return true;
+      }else if( n.getKind()==FORALL ){
+        return hasNonCbqiOperator( n[1], visited );
+      }else{
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          if( hasNonCbqiOperator( n[i], visited ) ){
+            return true;
+          }
+        }
+      }
+    }
+  }
+  return false;
+}
+
+// -1 : not cbqi sort, 0 : cbqi sort, 1 : cbqi sort regardless of quantifier body
+int InstStrategyCbqi::isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited ) {
+  std::map< TypeNode, int >::iterator itv = visited.find( tn );
+  if( itv==visited.end() ){
+    visited[tn] = 0;
+    int ret = -1;
+    if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){
+      ret = 0;
+    }else if( tn.isDatatype() ){
+      ret = 1;
+      const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+          TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() );
+          int cret = isCbqiSort( crange, visited );
+          if( cret==-1 ){
+            visited[tn] = -1;
+            return -1;
+          }else if( cret<ret ){
+            ret = cret;
+          }
+        }
+      }
+    }else if( tn.isSort() ){
+      QuantEPR * qepr = d_quantEngine->getQuantEPR();
+      if( qepr!=NULL ){
+        ret = qepr->isEPR( tn ) ? 1 : -1;
+      }
+    }
+    visited[tn] = ret;
+    return ret;
+  }else{
+    return itv->second;
+  }
+}
+
+int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
+  int hmin = 1;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    TypeNode tn = q[0][i].getType();
+    std::map< TypeNode, int > visited;
+    int handled = isCbqiSort( tn, visited );
+    if( handled==-1 ){
+      return -1;
+    }else if( handled<hmin ){
+      hmin = handled;
+    }
+  }
+  return hmin;
+}
+
+bool InstStrategyCbqi::doCbqi( Node q ){
+  std::map< Node, int >::iterator it = d_do_cbqi.find( q );
+  if( it==d_do_cbqi.end() ){
+    int ret = 2;
+    if( !d_quantEngine->getQuantAttributes()->isQuantElim( q ) ){
+      Assert( !d_quantEngine->getQuantAttributes()->isQuantElimPartial( q ) );
+      //if has an instantiation pattern, don't do it
+      if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
+        for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+          if( q[2][i].getKind()==INST_PATTERN ){
+            ret = 0;
+          }
+        }
+      }
+      if( d_quantEngine->getQuantAttributes()->isSygus( q ) ){
+        ret = 0;
+      }
+      if( ret!=0 ){
+        //if quantifier has a non-handled variable, then do not use cbqi
+        //if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
+        int ncbqiv = hasNonCbqiVariable( q );
+        if( ncbqiv==0 || ncbqiv==1 ){
+          std::map< Node, bool > visited;
+          if( hasNonCbqiOperator( q[1], visited ) ){
+            if( ncbqiv==1 ){
+              //all variables are fully handled, this implies this will be handlable regardless of body (e.g. for EPR)
+              //  so, try but not exclusively
+              ret = 1;
+            }else{
+              //cannot be handled
+              ret = 0;
+            }
+          }
+        }else{
+          // unhandled variable type
+          ret = 0;
+        }
+        if( ret==0 && options::cbqiAll() ){
+          //try but not exclusively
+          ret = 1;
+        }
+      }
+    }
+    Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
+    d_do_cbqi[q] = ret;
+    return ret!=0;
+  }else{
+    return it->second!=0;
+  }
+}
+
+Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) {
+  if( proc.find( q )==proc.end() ){
+    proc[q] = true;
+    //first check children
+    std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q );
+    if( itc!=d_children_quant.end() ){
+      for( unsigned j=0; j<itc->second.size(); j++ ){
+        Node d = getNextDecisionRequestProc( itc->second[j], proc );
+        if( !d.isNull() ){
+          return d;
+        }
+      }
+    }
+    //then check self
+    if( hasAddedCbqiLemma( q ) ){
+      Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q );
+      bool value;
+      if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
+        Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
+        return cel;
+      }
+    }    
+  }
+  return Node::null(); 
+}
+
+Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){
+  std::map< Node, bool > proc;
+  //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  //  Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+  for( NodeSet::const_iterator it = d_added_cbqi_lemma.begin(); it != d_added_cbqi_lemma.end(); ++it ){
+    Node q = *it;
+    Node d = getNextDecisionRequestProc( q, proc );
+    if( !d.isNull() ){
+      priority = 0;
+      return d;
+    }
+  }
+  return Node::null();
+}
+
+
+
+//new implementation
+
+bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) {
+  return d_out->doAddInstantiation( subs );
+}
+
+bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) {
+  return d_out->isEligibleForInstantiation( n );
+}
+
+bool CegqiOutputInstStrategy::addLemma( Node lem ) {
+  return d_out->addLemma( lem );
+}
+
+
+InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe )
+  : InstStrategyCbqi( qe ) {
+  d_out = new CegqiOutputInstStrategy( this );
+  d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
+  d_check_vts_lemma_lc = false;
+}
+
+InstStrategyCegqi::~InstStrategyCegqi()
+{
+  delete d_out;
+
+  for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(),
+          iend = d_cinst.end(); i != iend; ++i) {
+    CegInstantiator * instantiator = (*i).second;
+    delete instantiator;
+  }
+  d_cinst.clear();
+}
+
+void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
+  d_check_vts_lemma_lc = false;
+}
+
+void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
+  if( e==0 ){
+    CegInstantiator * cinst = getInstantiator( q );
+    Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
+    d_curr_quant = q;
+    if( !cinst->check() ){
+      d_incomplete_check = true;
+      d_check_vts_lemma_lc = true;
+    }
+    d_curr_quant = Node::null();
+  }else if( e==1 ){
+    //minimize the free delta heuristically on demand
+    if( d_check_vts_lemma_lc ){
+      Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
+      d_check_vts_lemma_lc = false;
+      d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
+      d_small_const = Rewriter::rewrite( d_small_const );
+      //heuristic for now, until we know how to do nested quantification
+      Node delta = d_quantEngine->getTermUtil()->getVtsDelta( true, false );
+      if( !delta.isNull() ){
+        Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
+        Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
+        d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+      }
+      std::vector< Node > inf;
+      d_quantEngine->getTermUtil()->getVtsTerms( inf, true, false, false );
+      for( unsigned i=0; i<inf.size(); i++ ){
+        Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
+        Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
+        d_quantEngine->getOutputChannel().lemma( inf_lem_lb );
+      }
+    }
+  }
+}
+
+bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
+  Assert( !d_curr_quant.isNull() );
+  //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
+  if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){
+    d_cbqi_set_quant_inactive = true;
+    d_incomplete_check = true;
+    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->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;
+    }else{
+      //this should never happen for monotonic selection strategies
+      Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
+      return false;
+    }
+  }
+}
+
+bool InstStrategyCegqi::addLemma( Node lem ) {
+  return d_quantEngine->addLemma( lem );
+}
+
+bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
+  if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
+    if( n.getAttribute(VirtualTermSkolemAttribute()) ){
+      // virtual terms are allowed
+      return true;
+    }else{
+      TypeNode tn = n.getType();
+      if( tn.isSort() ){
+        QuantEPR * qepr = d_quantEngine->getQuantEPR();
+        if( qepr!=NULL ){
+          //legal if in the finite set of constants of type tn
+          if( qepr->isEPRConstant( tn, n ) ){
+            return true;
+          }
+        }
+      }
+      //only legal if current quantified formula contains n
+      return TermUtil::containsTerm( d_curr_quant, n );
+    }
+  }else{
+    return true;
+  }
+}
+
+CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
+  std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
+  if( it==d_cinst.end() ){
+    CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true );
+    d_cinst[q] = cinst;
+    return cinst;
+  }else{
+   return it->second;
+  }
+}
+
+void InstStrategyCegqi::registerQuantifier( Node q ) {
+  if( doCbqi( q ) ){
+    // get the instantiator  
+    if( options::cbqiPreRegInst() ){
+      getInstantiator( q );
+    }
+    // register the cbqi lemma
+    if( registerCbqiLemma( q ) ){
+      Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
+    }
+  }
+}
+
+void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) {
+  //must register with the instantiator
+  //must explicitly remove ITEs so that we record dependencies
+  std::vector< Node > ce_vars;
+  for( unsigned i=0; i<d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ); i++ ){
+    ce_vars.push_back( d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ) );
+  }
+  std::vector< Node > lems;
+  lems.push_back( lem );
+  CegInstantiator * cinst = getInstantiator( q );
+  cinst->registerCounterexampleLemma( lems, ce_vars );
+  for( unsigned i=0; i<lems.size(); i++ ){
+    Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl;
+    d_quantEngine->addLemma( lems[i], false );
+  }
+}
+
+void InstStrategyCegqi::presolve() {
+  if( options::cbqiPreRegInst() ){
+    for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
+      Trace("cbqi-presolve") << "Presolve " << it->first << std::endl;
+      it->second->presolve( it->first );
+    }
+  }
+}
+
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
new file mode 100644
index 000000000..3443d2c4d
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
@@ -0,0 +1,166 @@
+/*********************                                                        */
+/*! \file inst_strategy_cbqi.h
+ ** \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 counterexample-guided quantifier instantiation
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INST_STRATEGY_CBQI_H
+#define __CVC4__INST_STRATEGY_CBQI_H
+
+#include "theory/arith/arithvar.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace arith {
+  class TheoryArith;
+}
+
+namespace quantifiers {
+
+class InstStrategyCbqi : public QuantifiersModule {
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
+
+ protected:
+  bool d_cbqi_set_quant_inactive;
+  bool d_incomplete_check;
+  /** whether we have added cbqi lemma */
+  NodeSet d_added_cbqi_lemma;
+  /** whether we have added cbqi lemma */
+  NodeSet d_elim_quants;
+  /** parent guards */
+  std::map< Node, std::vector< Node > > d_parent_quant;
+  std::map< Node, std::vector< Node > > d_children_quant;
+  std::map< Node, bool > d_active_quant;
+  /** whether we have instantiated quantified formulas */
+  //NodeSet d_added_inst;
+  /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */
+  std::map< Node, int > d_do_cbqi;
+  /** register ce lemma */
+  bool registerCbqiLemma( Node q );
+  virtual void registerCounterexampleLemma( Node q, Node lem );
+  /** has added cbqi lemma */
+  bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
+  /** helper functions */
+  int hasNonCbqiVariable( Node q );
+  bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
+  int isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited );
+  /** get next decision request with dependency checking */
+  Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc );  
+  /** process functions */
+  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+  virtual void process( Node q, Theory::Effort effort, int e ) = 0;
+
+ protected:
+  //for identification
+  uint64_t d_qid_count;
+  //nested qe map
+  std::map< Node, Node > d_nested_qe;
+  //mark ids on quantifiers 
+  Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited );
+  // id to ce quant
+  std::map< Node, Node > d_id_to_ce_quant;
+  std::map< Node, Node > d_ce_quant_to_id;
+  //do nested quantifier elimination recursive
+  Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts );
+  Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts );
+  //elimination information (for delayed elimination)
+  class NestedQEInfo {
+  public:
+    NestedQEInfo() : d_doVts(false){}
+    ~NestedQEInfo(){}
+    Node d_q;
+    std::vector< Node > d_inst_terms;
+    bool d_doVts;
+  };
+  std::map< Node, NestedQEInfo > d_nested_qe_info;
+  NodeIntMap d_nested_qe_waitlist_size;
+  NodeIntMap d_nested_qe_waitlist_proc;
+  std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
+
+ public:
+  //do nested quantifier elimination
+  Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts );
+
+ public:
+  InstStrategyCbqi( QuantifiersEngine * qe );
+
+  /** whether to do CBQI for quantifier q */
+  bool doCbqi( Node q );
+  /** process functions */
+  bool needsCheck( Theory::Effort e );
+  QEffort needsModel(Theory::Effort e);
+  void reset_round( Theory::Effort e );
+  void check(Theory::Effort e, QEffort quant_e);
+  bool checkComplete();
+  bool checkCompleteFor( Node q );
+  void preRegisterQuantifier( Node q );
+  void registerQuantifier( Node q );
+  /** get next decision request */
+  Node getNextDecisionRequest( unsigned& priority );
+};
+
+//generalized counterexample guided quantifier instantiation
+
+class InstStrategyCegqi;
+
+class CegqiOutputInstStrategy : public CegqiOutput {
+public:
+  CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
+  InstStrategyCegqi * d_out;
+  bool doAddInstantiation( std::vector< Node >& subs );
+  bool isEligibleForInstantiation( Node n );
+  bool addLemma( Node lem );
+};
+
+class InstStrategyCegqi : public InstStrategyCbqi {
+ protected:
+  CegqiOutputInstStrategy * d_out;
+  std::map< Node, CegInstantiator * > d_cinst;
+  Node d_small_const;
+  Node d_curr_quant;
+  bool d_check_vts_lemma_lc;
+  /** process functions */
+  void processResetInstantiationRound(Theory::Effort effort) override;
+  void process(Node f, Theory::Effort effort, int e) override;
+  /** register ce lemma */
+  void registerCounterexampleLemma(Node q, Node lem) override;
+
+ public:
+  InstStrategyCegqi( QuantifiersEngine * qe );
+  ~InstStrategyCegqi() override;
+
+  bool doAddInstantiation( std::vector< Node >& subs );
+  bool isEligibleForInstantiation( Node n );
+  bool addLemma( Node lem );
+  /** identify */
+  std::string identify() const override { return std::string("Cegqi"); }
+
+  //get instantiator for quantifier
+  CegInstantiator * getInstantiator( Node q );
+  //register quantifier
+  void registerQuantifier(Node q) override;
+  //presolve
+  void presolve() override;
+};
+
+}
+}
+}
+
+#endif