From af86e5a8dc7a64fb5f7b4ca7bd3b2bedf5e8fe32 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 26 Oct 2015 16:11:00 +0100
Subject: [PATCH] Promote InstStrategyCbqi to quantifier module. Cleanup unused
 code.

---
 src/theory/quantifiers/inst_strategy_cbqi.cpp | 299 ++++++++++--------
 src/theory/quantifiers/inst_strategy_cbqi.h   |  26 +-
 .../quantifiers/inst_strategy_e_matching.cpp  |  11 +-
 .../quantifiers/inst_strategy_e_matching.h    |   1 -
 .../quantifiers/instantiation_engine.cpp      | 127 +-------
 src/theory/quantifiers/instantiation_engine.h |  33 +-
 src/theory/quantifiers/model_builder.cpp      |   6 +-
 src/theory/quantifiers/model_builder.h        |   2 +
 src/theory/quantifiers/quant_util.cpp         |   4 +
 src/theory/quantifiers/quant_util.h           |   2 +
 .../quantifiers/quantifiers_rewriter.cpp      |   8 +-
 src/theory/quantifiers_engine.cpp             |  71 +++--
 src/theory/quantifiers_engine.h               |  22 +-
 src/theory/uf/theory_uf.cpp                   |  27 --
 src/theory/uf/theory_uf.h                     |  23 --
 15 files changed, 273 insertions(+), 389 deletions(-)

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 39e7abd3b..07de0a3d1 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -33,19 +33,33 @@ using namespace CVC4::theory::arith;
 
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
-InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : InstStrategy( qe ){
+InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ){
   
 }
 
-void InstStrategyCbqi::processResetInstantiationRound( Theory::Effort effort ) {
+bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
+  return e>=Theory::EFFORT_LAST_CALL;
+}
+
+unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
+  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    if( d_quantEngine->getOwner( q )==this && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+      return QuantifiersEngine::QEFFORT_STANDARD;
+    }
+  }
+  return QuantifiersEngine::QEFFORT_NONE;
+}
+
+void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
   d_cbqi_set_quant_inactive = false;
   //check if any cbqi lemma has not been added yet
   for( int 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( d_quantEngine->hasOwnership( q, d_quantEngine->getInstantiationEngine() ) && doCbqi( q ) ){
+    if( d_quantEngine->getOwner( q )==this ){
       if( !hasAddedCbqiLemma( q ) ){
-        d_added_cbqi_lemma[q] = true;
+        d_added_cbqi_lemma.insert( q );
         Trace("cbqi") << "Do cbqi for " << q << std::endl;
         //add cbqi lemma
         //get the counterexample literal
@@ -83,6 +97,43 @@ void InstStrategyCbqi::processResetInstantiationRound( Theory::Effort effort ) {
       }
     }
   }
+  processResetInstantiationRound( effort );
+}
+
+void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
+  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+    for( int ee=0; ee<=1; ee++ ){
+      unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+      for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+        Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+        if( d_quantEngine->getOwner( q )==this && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+          process( q, e, ee );
+        }
+      }
+      if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+        break;
+      }
+    }
+  }
+}
+
+bool InstStrategyCbqi::checkComplete() {
+  if( !options::cbqiSat() && d_cbqi_set_quant_inactive ){
+    return false;
+  }else{
+    return true;
+  }
+}
+
+void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
+  if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
+    //take ownership of the quantified formula
+    d_quantEngine->setOwner( q, this );
+  }
+}
+
+void InstStrategyCbqi::registerQuantifier( Node q ) {
+  
 }
 
 void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
@@ -132,15 +183,19 @@ bool InstStrategyCbqi::doCbqi( Node q ){
   std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
   if( it==d_do_cbqi.end() ){
     bool ret = false;
-    Assert( options::cbqi() );
-    if( options::cbqiAll() ){
-      ret = true;
+    //if has an instantiation pattern, don't do it
+    if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
+      ret = false;
     }else{
-      //if quantifier has a non-arithmetic variable, then do not use cbqi
-      //if quantifier has an APPLY_UF term, then do not use cbqi
-      Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
-      std::map< Node, bool > visited;
-      ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+      if( options::cbqiAll() ){
+        ret = true;
+      }else{
+        //if quantifier has a non-arithmetic variable, then do not use cbqi
+        //if quantifier has an APPLY_UF term, then do not use cbqi
+        Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+        std::map< Node, bool > visited;
+        ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+      }
     }
     d_do_cbqi[q] = ret;
     return ret;
@@ -234,7 +289,6 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
   Debug("quant-arith-debug") << std::endl;
   debugPrint( "quant-arith-debug" );
   d_counter++;
-  InstStrategyCbqi::processResetInstantiationRound( effort );
 }
 
 void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){
@@ -263,97 +317,92 @@ void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<
   }
 }
 
-int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
-  if( doCbqi( f ) ){
-    if( e<1 ){
-      return STATUS_UNFINISHED;
-    }else if( e==1 ){
-      if( d_quantActive.find( f )!=d_quantActive.end() ){
-        //the point instantiation
-        InstMatch m_point( f );
-        bool m_point_valid = true;
-        int lem = 0;
-        //scan over all instantiation rows
-        for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-          Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
-          Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
-          for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
-            ArithVar x = d_instRows[ic][j];
-            if( !d_ceTableaux[ic][x].empty() ){
-              if( Debug.isOn("quant-arith-simplex") ){
-                Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
-                Debug("quant-arith-simplex") << "  ";
-                for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
-                  if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
-                  Debug("quant-arith-simplex") << it->first << " * " << it->second;
-                }
-                Debug("quant-arith-simplex") << " = ";
-                Node v = getTableauxValue( x, false );
-                Debug("quant-arith-simplex") << v << std::endl;
-                Debug("quant-arith-simplex") << "  term : " << d_tableaux_term[ic][x] << std::endl;
-                Debug("quant-arith-simplex") << "  ce-term : ";
-                for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
-                  if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
-                  Debug("quant-arith-simplex") << it->first << " * " << it->second;
-                }
-                Debug("quant-arith-simplex") << std::endl;
+void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
+  if( e==0 ){
+    if( d_quantActive.find( f )!=d_quantActive.end() ){
+      //the point instantiation
+      InstMatch m_point( f );
+      bool m_point_valid = true;
+      int lem = 0;
+      //scan over all instantiation rows
+      for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+        Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+        Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
+        for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
+          ArithVar x = d_instRows[ic][j];
+          if( !d_ceTableaux[ic][x].empty() ){
+            if( Debug.isOn("quant-arith-simplex") ){
+              Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
+              Debug("quant-arith-simplex") << "  ";
+              for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
+                if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+                Debug("quant-arith-simplex") << it->first << " * " << it->second;
               }
-              //instantiation row will be A*e + B*t = beta,
-              // where e is a vector of terms , and t is vector of ground terms.
-              // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
-              // We will construct the term ( beta - B*t)/coeff to use for e_i.
-              InstMatch m( f );
-              for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
-                if( f[0][k].getType().isInteger() ){
-                  m.setValue( k, d_zero );
-                }
+              Debug("quant-arith-simplex") << " = ";
+              Node v = getTableauxValue( x, false );
+              Debug("quant-arith-simplex") << v << std::endl;
+              Debug("quant-arith-simplex") << "  term : " << d_tableaux_term[ic][x] << std::endl;
+              Debug("quant-arith-simplex") << "  ce-term : ";
+              for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
+                if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+                Debug("quant-arith-simplex") << it->first << " * " << it->second;
               }
-              //By default, choose the first instantiation constant to be e_i.
-              Node var = d_ceTableaux[ic][x].begin()->first;
-              //if it is integer, we need to find variable with coefficent +/- 1
-              if( var.getType().isInteger() ){
-                std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
-                while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
-                  ++it;
-                  if( it==d_ceTableaux[ic][x].end() ){
-                    var = Node::null();
-                  }else{
-                    var = it->first;
-                  }
-                }
-                //Otherwise, try one that divides all ground term coefficients?
-                //  Might be futile, if rewrite ensures gcd of coeffs is 1.
+              Debug("quant-arith-simplex") << std::endl;
+            }
+            //instantiation row will be A*e + B*t = beta,
+            // where e is a vector of terms , and t is vector of ground terms.
+            // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
+            // We will construct the term ( beta - B*t)/coeff to use for e_i.
+            InstMatch m( f );
+            for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
+              if( f[0][k].getType().isInteger() ){
+                m.setValue( k, d_zero );
               }
-              if( !var.isNull() ){
-                //add to point instantiation if applicable
-                if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
-                  Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
-                  Node v = getTableauxValue( x, false );
-                  if( !var.getType().isInteger() || v.getType().isInteger() ){
-                    m_point.setValue( i, v );
-                  }else{
-                    m_point_valid = false;
-                  }
+            }
+            //By default, choose the first instantiation constant to be e_i.
+            Node var = d_ceTableaux[ic][x].begin()->first;
+            //if it is integer, we need to find variable with coefficent +/- 1
+            if( var.getType().isInteger() ){
+              std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
+              while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
+                ++it;
+                if( it==d_ceTableaux[ic][x].end() ){
+                  var = Node::null();
+                }else{
+                  var = it->first;
                 }
-                Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
-                if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
-                  lem++;
+              }
+              //Otherwise, try one that divides all ground term coefficients?
+              //  Might be futile, if rewrite ensures gcd of coeffs is 1.
+            }
+            if( !var.isNull() ){
+              //add to point instantiation if applicable
+              if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
+                Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
+                Node v = getTableauxValue( x, false );
+                if( !var.getType().isInteger() || v.getType().isInteger() ){
+                  m_point.setValue( i, v );
+                }else{
+                  m_point_valid = false;
                 }
-              }else{
-                Debug("quant-arith-simplex") << "Could not find var." << std::endl;
               }
+              Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
+              if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
+                lem++;
+              }
+            }else{
+              Debug("quant-arith-simplex") << "Could not find var." << std::endl;
             }
           }
         }
-        if( lem==0 && m_point_valid ){
-          if( d_quantEngine->addInstantiation( f, m_point ) ){
-            Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
-          }
+      }
+      if( lem==0 && m_point_valid ){
+        if( d_quantEngine->addInstantiation( f, m_point ) ){
+          Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
         }
       }
     }
   }
-  return STATUS_UNKNOWN;
 }
 
 
@@ -428,13 +477,13 @@ void InstStrategySimplex::debugPrint( const char* c ){
 bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){
   //first try +delta
   if( doInstantiation2( f, ic, term, x, m, var ) ){
-    ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);
+    ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
     return true;
   }else{
 #ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
     //otherwise try -delta
     if( doInstantiation2( f, ic, term, x, m, var, true ) ){
-      ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);
+      ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
       return true;
     }else{
       return false;
@@ -512,45 +561,37 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategyCbq
 
 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
   d_check_vts_lemma_lc = true;
-  InstStrategyCbqi::processResetInstantiationRound( effort );
-}
-
-int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
-  //can only be called at last call, since it is model-based
-  if( doCbqi( f ) && effort==Theory::EFFORT_LAST_CALL ){
-    if( e<1 ){
-      return STATUS_UNFINISHED;
-    }else if( e==1 ){
-      CegInstantiator * cinst = getInstantiator( f );
-      Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
-      d_curr_quant = f;
-      bool addedLemma = cinst->check();
-      d_curr_quant = Node::null();
-      return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED;
-    }else if( e==2 ){
-      //minimize the free delta heuristically on demand
-      if( d_check_vts_lemma_lc ){
-        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->getTermDatabase()->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->getTermDatabase()->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 );
-        }
+}
+
+void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
+  if( e==0 ){
+    CegInstantiator * cinst = getInstantiator( f );
+    Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
+    d_curr_quant = f;
+    cinst->check();
+    d_curr_quant = Node::null();
+  }else if( e==1 ){
+    //minimize the free delta heuristically on demand
+    if( d_check_vts_lemma_lc ){
+      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->getTermDatabase()->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->getTermDatabase()->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 );
       }
     }
   }
-  return STATUS_UNKNOWN;
 }
 
 bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) {
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index adbb2a5e4..6619860e0 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -33,11 +33,12 @@ namespace arith {
 
 namespace quantifiers {
 
-class InstStrategyCbqi : public InstStrategy {
+class InstStrategyCbqi : public QuantifiersModule {
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 protected:
   bool d_cbqi_set_quant_inactive;
   /** whether we have added cbqi lemma */
-  std::map< Node, bool > d_added_cbqi_lemma;
+  NodeSet d_added_cbqi_lemma;
   /** whether to do cbqi for this quantified formula */
   std::map< Node, bool > d_do_cbqi;  
   /** register ce lemma */
@@ -47,17 +48,24 @@ protected:
   /** helper functions */
   bool hasNonCbqiVariable( Node q );
   bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
+  /** process functions */
+  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+  virtual void process( Node q, Theory::Effort effort, int e ) = 0;
 public:
   InstStrategyCbqi( QuantifiersEngine * qe );
   ~InstStrategyCbqi() throw() {}
+  /** whether to do CBQI for quantifier q */
+  bool doCbqi( Node q );
   /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
+  bool needsCheck( Theory::Effort e );
+  unsigned needsModel( Theory::Effort e );
+  void reset_round( Theory::Effort e );
+  void check( Theory::Effort e, unsigned quant_e );
+  bool checkComplete();
+  void preRegisterQuantifier( Node q );
+  void registerQuantifier( Node q );
   /** get next decision request */
   Node getNextDecisionRequest();
-  //set quant inactive
-  bool setQuantifierInactive() { return d_cbqi_set_quant_inactive; }
-  /** whether to do CBQI for quantifier q */
-  bool doCbqi( Node q );
 };
 
 
@@ -95,7 +103,7 @@ private:
   Node d_negOne;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
+  void process( Node f, Theory::Effort effort, int e );
 public:
   InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
   ~InstStrategySimplex() throw() {}
@@ -126,7 +134,7 @@ protected:
   bool d_check_vts_lemma_lc;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
+  void process( Node f, Theory::Effort effort, int e );
   /** register ce lemma */
   void registerCounterexampleLemma( Node q, Node lem );
 public:
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 9330bac7e..928c15593 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -95,7 +95,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
           InstMatch baseMatch( f );
           int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
           Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
-          d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
+          d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
           if( d_user_gen[f][i]->isMultiTrigger() ){
             d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
           }
@@ -212,7 +212,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
               int numInst = tr->addInstantiations( baseMatch );
               hasInst = numInst>0 || hasInst;
               Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
-              d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;
+              d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
               if( r==1 ){
                 d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
               }
@@ -583,7 +583,7 @@ bool FullSaturation::process( Node f, Theory::Effort effort ){
             }
             if( d_quantEngine->addInstantiation( f, terms, false ) ){
               Trace("inst-alg-rd") << "Success!" << std::endl;
-              ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+              ++(d_quantEngine->d_statistics.d_instantiations_guess);
               return true;
             }else{
               index--;
@@ -600,7 +600,7 @@ bool FullSaturation::process( Node f, Theory::Effort effort ){
         d_guessed[f] = true;
         InstMatch m( f );
         if( d_quantEngine->addInstantiation( f, m ) ){
-          ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+          ++(d_quantEngine->d_statistics.d_instantiations_guess);
           return true;
         }
       }
@@ -614,6 +614,3 @@ void FullSaturation::registerQuantifier( Node q ) {
 
 }
 
-void FullSaturation::assertNode( Node n ) {
-
-}
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index c6a0be03b..f02339e2e 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -118,7 +118,6 @@ public:
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node q );
-  void assertNode( Node n );
   /** identify */
   std::string identify() const { return std::string("FullSaturation"); }
 };/* class FullSaturation */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index f5333dbe1..2785ad128 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -19,7 +19,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_strategy_e_matching.h"
-#include "theory/quantifiers/inst_strategy_cbqi.h"
 #include "theory/quantifiers/trigger.h"
 
 using namespace std;
@@ -31,21 +30,18 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL){
 
 }
 
 InstantiationEngine::~InstantiationEngine() {
   delete d_i_ag;
   delete d_isup;
-  delete d_i_splx;
-  delete d_i_cegqi;
 }
 
 void InstantiationEngine::finishInit(){
   if( options::eMatching() ){
     //these are the instantiation strategies for E-matching
-
     //user-provided patterns
     if( options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
       d_isup = new InstStrategyUserPatterns( d_quantEngine );
@@ -56,21 +52,6 @@ void InstantiationEngine::finishInit(){
     d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine );
     d_instStrategies.push_back( d_i_ag );
   }
-
-  //counterexample-based quantifier instantiation
-  if( options::cbqi() ){
-    if( options::cbqiSplx() ){
-      d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
-      d_instStrategies.push_back( d_i_splx );
-      d_i_cbqi = d_i_splx;
-    }else{
-      d_i_cegqi = new InstStrategyCegqi( d_quantEngine );
-      d_instStrategies.push_back( d_i_cegqi );
-      d_i_cbqi = d_i_cegqi;
-    }
-  }else{
-    d_i_cbqi = NULL;
-  }
 }
 
 void InstantiationEngine::presolve() {
@@ -80,7 +61,7 @@ void InstantiationEngine::presolve() {
 }
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
-  unsigned lastWaiting = d_quantEngine->d_lemmas_waiting.size();
+  unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
   //iterate over an internal effort level e
   int e = 0;
   int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
@@ -110,7 +91,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
       }
     }
     //do not consider another level if already added lemma at this level
-    if( d_quantEngine->d_lemmas_waiting.size()>lastWaiting ){
+    if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
       finished = true;
     }
     e++;
@@ -128,20 +109,6 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
   return d_quantEngine->getInstWhenNeedsCheck( e );
 }
 
-unsigned InstantiationEngine::needsModel( Theory::Effort e ){
-  if( options::cbqiModel() && options::cbqi() ){
-    Assert( d_i_cbqi!=NULL );
-    //needs model if there is at least one cbqi quantified formula that is active
-    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      if( d_quantEngine->hasOwnership( q, this ) && d_i_cbqi->doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
-        return QuantifiersEngine::QEFFORT_STANDARD;
-      }
-    }
-  }
-  return QuantifiersEngine::QEFFORT_NONE;
-}
-
 void InstantiationEngine::reset_round( Theory::Effort e ){
   //if not, proceed to instantiation round
   //reset the instantiation strategies
@@ -158,15 +125,13 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
       Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
     }
-    ++(d_statistics.d_instantiation_rounds);
+    //collect all active quantified formulas belonging to this
     bool quantActive = false;
     d_quants.clear();
     for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
       if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
-        if( !options::cbqi() || !TermDb::hasInstConstAttr( q ) ){
-          quantActive = true;
-        }
+        quantActive = true;
         d_quants.push_back( q );
       }
     }
@@ -186,42 +151,25 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
 }
 
 bool InstantiationEngine::checkComplete() {
-  if( !options::cbqiSat() && ( d_i_cbqi && d_i_cbqi->setQuantifierInactive() ) ){
-    return false;
-  }else{
+  if( !options::finiteModelFind() ){
     for( unsigned i=0; i<d_quants.size(); i++ ){
       if( isIncomplete( d_quants[i] ) ){
         return false;
       }
     }
-    return true;
   }
+  return true;
 }
 
-
-void InstantiationEngine::preRegisterQuantifier( Node q ) {
-  if( options::cbqi() ){
-    if( d_i_cbqi->doCbqi( q ) ){
-      d_quantEngine->setOwner( q, this );
-    }
-  }
+bool InstantiationEngine::isIncomplete( Node q ) {
+  return true;
 }
 
 void InstantiationEngine::registerQuantifier( Node f ){
   if( d_quantEngine->hasOwnership( f, this ) ){
-    for( unsigned i=0; i<d_instStrategies.size(); ++i ){
-      d_instStrategies[i]->registerQuantifier( f );
-    }
-    //Notice() << "do cbqi " << f << " ? " << std::endl;
-    /*
-    if( options::cbqi() ){
-      Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
-      if( !doCbqi( f ) ){
-        d_quantEngine->addTermToDatabase( ceBody, true );
-      }
-    }
-    */
-
+    //for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+    //  d_instStrategies[i]->registerQuantifier( f );
+    //}
     //take into account user patterns
     if( f.getNumChildren()==3 ){
       Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f );
@@ -238,26 +186,6 @@ void InstantiationEngine::registerQuantifier( Node f ){
   }
 }
 
-void InstantiationEngine::assertNode( Node f ){
-}
-
-bool InstantiationEngine::isIncomplete( Node q ) {
-  return true;
-}
-
-Node InstantiationEngine::getNextDecisionRequest(){
-  if( options::cbqi() ){
-    for( unsigned i=0; i<d_instStrategies.size(); ++i ){
-      InstStrategy* is = d_instStrategies[i];
-      Node lit = is->getNextDecisionRequest();
-      if( !lit.isNull() ){
-        return lit;
-      }
-    }
-  }
-  return Node::null();
-}
-
 void InstantiationEngine::addUserPattern( Node f, Node pat ){
   if( d_isup ){
     d_isup->addUserPattern( f, pat );
@@ -269,34 +197,3 @@ void InstantiationEngine::addUserNoPattern( Node f, Node pat ){
     d_i_ag->addUserNoPattern( f, pat );
   }
 }
-
-InstantiationEngine::Statistics::Statistics():
-  d_instantiations_user_patterns("InstantiationEngine::Instantiations_User_Patterns", 0),
-  d_instantiations_auto_gen("InstantiationEngine::Instantiations_Auto_Gen", 0),
-  d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
-  d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
-  d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
-  d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0),
-  d_instantiations_lte("InstantiationEngine::Instantiations_Local_T_Ext", 0),
-  d_instantiation_rounds("InstantiationEngine::Rounds", 0 )
-{
-  StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
-  StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
-  StatisticsRegistry::registerStat(&d_instantiations_guess);
-  StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
-  StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
-  StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes);
-  StatisticsRegistry::registerStat(&d_instantiations_lte);
-  StatisticsRegistry::registerStat(&d_instantiation_rounds);
-}
-
-InstantiationEngine::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
-  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
-  StatisticsRegistry::unregisterStat(&d_instantiations_guess);
-  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
-  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
-  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
-  StatisticsRegistry::unregisterStat(&d_instantiations_lte);
-  StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
-}
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 51daef9dc..bc1199588 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -27,9 +27,6 @@ namespace quantifiers {
 class InstStrategyUserPatterns;
 class InstStrategyAutoGenTriggers;
 class InstStrategyFreeVariable;
-class InstStrategyCbqi;
-class InstStrategySimplex;
-class InstStrategyCegqi;
 
 /** instantiation strategy class */
 class InstStrategy {
@@ -53,9 +50,7 @@ public:
   /** identify */
   virtual std::string identify() const { return std::string("Unknown"); }
   /** register quantifier */
-  virtual void registerQuantifier( Node q ) {}
-  /** get next decision request */
-  virtual Node getNextDecisionRequest() { return Node::null(); }
+  //virtual void registerQuantifier( Node q ) {}
 };/* class InstStrategy */
 
 class InstantiationEngine : public QuantifiersModule
@@ -63,17 +58,10 @@ class InstantiationEngine : public QuantifiersModule
 private:
   /** instantiation strategies */
   std::vector< InstStrategy* > d_instStrategies;
-  /** instantiation strategies active */
-  //std::map< InstStrategy*, bool > d_instStrategyActive;
   /** user-pattern instantiation strategy */
   InstStrategyUserPatterns* d_isup;
   /** auto gen triggers; only kept for destructor cleanup */
   InstStrategyAutoGenTriggers* d_i_ag;
-  InstStrategyCbqi * d_i_cbqi;
-  /** simplex (cbqi) */
-  InstStrategySimplex * d_i_splx;
-  /** generic cegqi */
-  InstStrategyCegqi * d_i_cegqi;
 private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   /** current processing quantified formulas */
@@ -90,34 +78,15 @@ public:
   void finishInit();
   void presolve();
   bool needsCheck( Theory::Effort e );
-  unsigned needsModel( Theory::Effort e );
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
-  void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
-  void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
-  Node getNextDecisionRequest();
   /** add user pattern */
   void addUserPattern( Node f, Node pat );
   void addUserNoPattern( Node f, Node pat );
 public:
-  /** statistics class */
-  class Statistics {
-  public:
-    IntStat d_instantiations_user_patterns;
-    IntStat d_instantiations_auto_gen;
-    IntStat d_instantiations_guess;
-    IntStat d_instantiations_cbqi_arith;
-    IntStat d_instantiations_cbqi_arith_minus;
-    IntStat d_instantiations_cbqi_datatypes;
-    IntStat d_instantiations_lte;
-    IntStat d_instantiation_rounds;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
   /** Identify this module */
   std::string identify() const { return "InstEngine"; }
 };/* class InstantiationEngine */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index e297e138c..79b995ef0 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -500,9 +500,11 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
   //for each asserted quantifier f,
   // - determine selection literals
   // - check which function/predicates have good and bad definitions for satisfying f
+  if( d_phase_reqs.find( f )==d_phase_reqs.end() ){
+    d_phase_reqs[f].initialize( d_qe->getTermDatabase()->getInstConstantBody( f ), true );
+  }
   int selectLitScore = -1;
-  QuantPhaseReq* qpr = d_qe->getPhaseRequirements( f );
-  for( std::map< Node, bool >::iterator it = qpr->d_phase_reqs.begin(); it != qpr->d_phase_reqs.end(); ++it ){
+  for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
     //the literal n is phase-required for quantifier f
     Node n = it->first;
     Node gn = d_qe->getTermDatabase()->getModelBasis( f, n );
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 8e84f15e2..b45aa0ff0 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -184,6 +184,8 @@ protected:
   int doInstGen( FirstOrderModel* fm, Node f );
   //theory-specific build models
   void constructModelUf( FirstOrderModel* fm, Node op );
+protected:
+  std::map< Node, QuantPhaseReq > d_phase_reqs;
 public:
   QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
   ~QModelBuilderDefault() throw() {}
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index ebeb4b871..026293e02 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -250,6 +250,10 @@ void QuantRelevance::setRelevance( Node s, int r ){
 
 
 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
+  initialize( n, computeEq );
+}
+
+void QuantPhaseReq::initialize( Node n, bool computeEq ){
   std::map< Node, int > phaseReqs2;
   computePhaseReqs( n, false, phaseReqs2 );
   for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 5e0f511e0..2186e03fd 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -77,8 +77,10 @@ private:
   /** helper functions compute phase requirements */
   void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );
 public:
+  QuantPhaseReq(){}
   QuantPhaseReq( Node n, bool computeEq = false );
   ~QuantPhaseReq(){}
+  void initialize( Node n, bool computeEq );
   /** is phase required */
   bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }
   /** get phase requirement */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index f2a47e8d8..e911b0dc4 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -550,10 +550,12 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, bool hasPol, bool pol,
             break;
           }
         }else{
-          for( unsigned j=0; j<new_cond.size(); j++ ){
-            currCond.erase( new_cond[j] );
+          if( !new_cond.empty() ){
+            for( unsigned j=0; j<new_cond.size(); j++ ){
+              currCond.erase( new_cond[j] );
+            }
+            cache.clear();
           }
-          cache.clear();
         }
       }
       children.push_back( nn );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 913d9b0c6..9ae3b1d40 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -40,6 +40,7 @@
 #include "theory/quantifiers/fun_def_engine.h"
 #include "theory/quantifiers/quant_equality_engine.h"
 #include "theory/quantifiers/inst_strategy_e_matching.h"
+#include "theory/quantifiers/inst_strategy_cbqi.h"
 
 using namespace std;
 using namespace CVC4;
@@ -128,15 +129,18 @@ d_presolve_cache_wic(u){
     d_sg_gen = NULL;
   }
   //maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules
-  if( !options::finiteModelFind() || options::fmfInstEngine() || options::cbqi() ){
+  if( !options::finiteModelFind() || options::fmfInstEngine() ){
     d_inst_engine = new quantifiers::InstantiationEngine( this );
     d_modules.push_back(  d_inst_engine );
-    if( options::cbqi() && options::cbqiModel() ){
-      needsBuilder = true;
-    }
   }else{
     d_inst_engine = NULL;
   }
+  //counterexample-based instantiation (initialized during finishInit)
+  d_i_cbqi = NULL;
+  if( options::cbqi() && options::cbqiModel() ){
+    needsBuilder = true;
+  }
+  //finite model finding
   if( options::finiteModelFind() ){
     if( options::fmfBoundInt() ){
       d_bint = new quantifiers::BoundedIntegers( c, this );
@@ -243,9 +247,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_fun_def_engine;
   delete d_uee;
   delete d_fs;
-  for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
-    delete (*i).second;
-  }
+  delete d_i_cbqi;
 }
 
 EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
@@ -270,6 +272,18 @@ Valuation& QuantifiersEngine::getValuation(){
 
 void QuantifiersEngine::finishInit(){
   Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
+  //counterexample-based quantifier instantiation
+  if( options::cbqi() ){
+    if( options::cbqiSplx() ){
+      d_i_cbqi = new quantifiers::InstStrategySimplex( (arith::TheoryArith*)getTheoryEngine()->theoryOf( THEORY_ARITH ), this );
+      d_modules.push_back( d_i_cbqi );
+    }else{
+      d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
+      d_modules.push_back( d_i_cbqi );
+    }
+  }else{
+    d_i_cbqi = NULL;
+  }
   for( int i=0; i<(int)d_modules.size(); i++ ){
     d_modules[i]->finishInit();
   }
@@ -449,12 +463,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }else if( e==Theory::EFFORT_LAST_CALL && quant_e==QEFFORT_MODEL ){
         //if we have a chance not to set incomplete
         if( !setIncomplete ){
-          setIncomplete = true;
+          setIncomplete = false;
           //check if we should set the incomplete flag
           for( unsigned i=0; i<qm.size(); i++ ){
-            if( qm[i]->checkComplete() ){
-              Trace("quant-engine-debug") << "Do not set incomplete because " << qm[i]->identify().c_str() << " was complete." << std::endl;
-              setIncomplete = false;
+            if( !qm[i]->checkComplete() ){
+              Trace("quant-engine-debug") << "Set incomplete because " << qm[i]->identify().c_str() << " was incomplete." << std::endl;
+              setIncomplete = true;
               break;
             }
           }
@@ -571,7 +585,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
       }
       Node ceBody = d_term_db->getInstConstantBody( f );
       //generate the phase requirements
-      d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
+      //d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
       //also register it with the strong solver
       //if( options::finiteModelFind() ){
       //  ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
@@ -1043,23 +1057,6 @@ void QuantifiersEngine::flushLemmas(){
   }
 }
 
-void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
-  if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE && d_phase_reqs.find( f )!=d_phase_reqs.end() ){
-    // doing literal-based matching (consider polarity of literals)
-    for( int i=0; i<(int)nodes.size(); i++ ){
-      Node prev = nodes[i];
-      if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
-        bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
-        nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
-      }
-      //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
-      //  Node req = qe->getPhaseReqEquality( f, trNodes[i] );
-      //  trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req );
-      //}
-    }
-  }
-}
-
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
   bool printed = false;
   for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
@@ -1113,7 +1110,11 @@ QuantifiersEngine::Statistics::Statistics():
   d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
   d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
   d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
-  d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0)
+  d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0),
+  d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
+  d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
+  d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
+  d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0)
 {
   StatisticsRegistry::registerStat(&d_num_quant);
   StatisticsRegistry::registerStat(&d_instantiation_rounds);
@@ -1126,7 +1127,11 @@ QuantifiersEngine::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_multi_triggers);
   StatisticsRegistry::registerStat(&d_multi_trigger_instantiations);
   StatisticsRegistry::registerStat(&d_red_alpha_equiv);
-  StatisticsRegistry::registerStat(&d_red_lte_partial_inst);
+  StatisticsRegistry::registerStat(&d_red_lte_partial_inst);  
+  StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
+  StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
+  StatisticsRegistry::registerStat(&d_instantiations_guess);
+  StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
 }
 
 QuantifiersEngine::Statistics::~Statistics(){
@@ -1142,6 +1147,10 @@ QuantifiersEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations);
   StatisticsRegistry::unregisterStat(&d_red_alpha_equiv);
   StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst);
+  StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
+  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
+  StatisticsRegistry::unregisterStat(&d_instantiations_guess);
+  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
 }
 
 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 76fb920bb..3aea9356d 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -66,15 +66,14 @@ public:
   /* Call during quantifier engine's check */
   virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
   /* check was complete (e.g. no lemmas implies a model) */
-  virtual bool checkComplete() { return false; }
+  virtual bool checkComplete() { return true; }
   /* Called for new quantifiers */
   virtual void preRegisterQuantifier( Node q ) {}
   /* Called for new quantifiers after owners are finalized */
   virtual void registerQuantifier( Node q ) = 0;
-  virtual void assertNode( Node n ) = 0;
+  virtual void assertNode( Node n ) {}
   virtual void propagate( Theory::Effort level ){}
   virtual Node getNextDecisionRequest() { return TNode::null(); }
-  virtual Node explain(TNode n) { return TNode::null(); }
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   virtual std::string identify() const = 0;
 public:
@@ -102,6 +101,7 @@ namespace quantifiers {
   class FunDefEngine;
   class QuantEqualityEngine;
   class FullSaturation;
+  class InstStrategyCbqi;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -136,8 +136,6 @@ private:
   quantifiers::AlphaEquivalence * d_alpha_equiv;
   /** model builder */
   quantifiers::QModelBuilder* d_builder;
-  /** phase requirements for each quantifier for each instantiation literal */
-  std::map< Node, QuantPhaseReq* > d_phase_reqs;
   /** instantiation engine */
   quantifiers::InstantiationEngine* d_inst_engine;
   /** model engine */
@@ -160,6 +158,8 @@ private:
   quantifiers::QuantEqualityEngine * d_uee;
   /** full saturation */
   quantifiers::FullSaturation * d_fs;
+  /** counterexample-based quantifier instantiation */
+  quantifiers::InstStrategyCbqi * d_i_cbqi;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -231,10 +231,6 @@ public:
   QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
   /** get the model builder */
   quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
-  /** get phase requirement information */
-  QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
-  /** get phase requirement terms */
-  void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
 public:  //modules
   /** get instantiation engine */
   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
@@ -258,6 +254,8 @@ public:  //modules
   quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
   /** get full saturation */
   quantifiers::FullSaturation * getFullSaturation() { return d_fs; }
+  /** get inst strategy cbqi */
+  quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
@@ -320,7 +318,7 @@ public:
   /** has added lemma */
   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
   /** get number of waiting lemmas */
-  int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
+  unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
   /** get needs check */
   bool getInstWhenNeedsCheck( Theory::Effort e );
   /** get user pat mode */
@@ -362,6 +360,10 @@ public:
     IntStat d_multi_trigger_instantiations;
     IntStat d_red_alpha_equiv;
     IntStat d_red_lte_partial_inst;
+    IntStat d_instantiations_user_patterns;
+    IntStat d_instantiations_auto_gen;
+    IntStat d_instantiations_guess;
+    IntStat d_instantiations_cbqi_arith;
     Statistics();
     ~Statistics();
   };/* class QuantifiersEngine::Statistics */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 95671d6ec..6679b5dc2 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -47,12 +47,6 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
 }
 
 TheoryUF::~TheoryUF() {
-  // destruct all ppRewrite() callbacks
-  for(RegisterPpRewrites::iterator i = d_registeredPpRewrites.begin();
-      i != d_registeredPpRewrites.end();
-      ++i) {
-    delete i->second;
-  }
   delete d_thss;
 }
 
@@ -544,24 +538,3 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
     d_thss->assertDisequal(t1, t2, reason);
   }
 }
-
-Node TheoryUF::ppRewrite(TNode node) {
-
-  if (node.getKind() != kind::APPLY_UF) {
-    return node;
-  }
-
-  // perform the callbacks requested by TheoryUF::registerPpRewrite()
-  RegisterPpRewrites::iterator c = d_registeredPpRewrites.find(node.getOperator());
-  if (c == d_registeredPpRewrites.end()) {
-    return node;
-  } else {
-    Node res = c->second->ppRewrite(node);
-    if (res != node) {
-      return ppRewrite(res);
-    } else {
-      return res;
-    }
-  }
-}
-
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 11830f0e2..82597e286 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -103,13 +103,6 @@ public:
 
   };/* class TheoryUF::NotifyClass */
 
-  /** A callback class for ppRewrite().  See registerPpRewrite(), below. */
-  class PpRewrite {
-  public:
-    virtual Node ppRewrite(TNode node) = 0;
-    virtual ~PpRewrite() {}
-  };/* class TheoryUF::PpRewrite */
-
 private:
 
   /** The notify class */
@@ -165,12 +158,6 @@ private:
   /** called when two equivalence classes are made disequal */
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 
-  /** a registry type for keeping Node-specific callbacks for ppRewrite() */
-  typedef std::hash_map<Node, PpRewrite*, NodeHashFunction> RegisterPpRewrites;
-
-  /** a collection of callbacks to issue while doing a ppRewrite() */
-  RegisterPpRewrites d_registeredPpRewrites;
-
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
@@ -209,16 +196,6 @@ public:
   StrongSolverTheoryUF* getStrongSolver() {
     return d_thss;
   }
-
-  Node ppRewrite(TNode node);
-
-  /**
-   * Register a ppRewrite() callback on "op."  TheoryUF owns
-   * the callback, and will delete it when it is destructed.
-   */
-  void registerPpRewrite(TNode op, PpRewrite* callback) {
-    d_registeredPpRewrites.insert(std::make_pair(op, callback));
-  }
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */
-- 
2.30.2