Extend counterexample-guided instantiation to extended theory of Int/Real, mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.

9 files changed, 294 insertions, 161 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 90639d68c..c7bf61eab 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -125,7 +125,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
               Node pv_coeff;  //coefficient of pv in the equality we solve (null is 1)
               bool proc = false;
               if( !d_prog_var[n].empty() ){
-                ns = applySubstitution( n, sf, vars, pv_coeff, false );
+                ns = applySubstitution( pvtn, n, sf, vars, pv_coeff, false );
                 if( !ns.isNull() ){
                   computeProgVars( ns );
                   //substituted version must be new and cannot contain pv
@@ -171,7 +171,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
               Node ns;
               Node pv_coeff;
               if( !d_prog_var[n].empty() ){
-                ns = applySubstitution( n, sf, vars, pv_coeff );
+                ns = applySubstitution( pvtn, n, sf, vars, pv_coeff );
                 if( !ns.isNull() ){
                   computeProgVars( ns );
                 }
@@ -210,7 +210,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                       if( Trace.isOn("cbqi-inst-debug") ){
                         Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
                         QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
-                        Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
+                        Trace("cbqi-inst-debug") << "isolate for " << pv << " : " << pv.getType() << "..." << std::endl;
                       }
                       Node veq;
                       if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
@@ -325,7 +325,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                   //apply substitution to LHS of atom
                   if( !d_prog_var[atom_lhs].empty() ){
                     Node atom_lhs_coeff;
-                    atom_lhs = applySubstitution( atom_lhs, sf, vars, atom_lhs_coeff );
+                    atom_lhs = applySubstitution( pvtn, atom_lhs, sf, vars, atom_lhs_coeff );
                     if( !atom_lhs.isNull() ){
                       computeProgVars( atom_lhs );
                       if( !atom_lhs_coeff.isNull() ){
@@ -470,6 +470,20 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                           }
                           if( options::cbqiModel() ){
                             //just store bounds, will choose based on tighest bound
+                            if( pvtn.isInteger() && !veq_c.isNull() && !veq_c.getType().isInteger() ){
+                              Trace("cbqi-bound2") << "Non-integer coefficient : " << veq_c << " for " << pv << std::endl;
+                              Assert( veq_c.isConst() );
+                              //multiply everything by denominator of coefficient
+                              Rational r = veq_c.getConst<Rational>();
+                              Node den = NodeManager::currentNM()->mkConst( Rational(r.getDenominator()) );
+                              uval = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, den, uval ) );
+                              veq_c = NodeManager::currentNM()->mkConst( Rational(r.getNumerator()) );
+                              for( unsigned t=0; t<2; t++ ){
+                                if( !vts_coeff[t].isNull() ){
+                                  vts_coeff[t] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, den, vts_coeff[t] ) );
+                                }
+                              }
+                            }
                             unsigned index = uires>0 ? 0 : 1;
                             mbp_bounds[index].push_back( uval );
                             mbp_coeff[index].push_back( veq_c );
@@ -607,7 +621,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                 Trace("cbqi-bound") << std::endl;
                 best_used[rr] = (unsigned)best;
                 Node val = mbp_bounds[rr][best];
-                val = getModelBasedProjectionValue( val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta,
+                val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta,
                                                     mbp_vts_coeff[rr][0][best], vts_sym[0], mbp_vts_coeff[rr][1][best], vts_sym[1] );
                 if( !val.isNull() ){
                   if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
@@ -624,7 +638,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
           if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){
             Node val = d_zero;
             Node c; //null (one) coefficient
-            val = getModelBasedProjectionValue( val, true, c, pv_value, d_zero, theta, Node::null(), vts_sym[0], Node::null(), vts_sym[1] );
+            val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), vts_sym[0], Node::null(), vts_sym[1] );
             if( !val.isNull() ){
               if( subs_proc[val].find( c )==subs_proc[val].end() ){
                 subs_proc[val][c] = true;
@@ -643,7 +657,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
             int rr = upper_first ? (1-r) : r;
             for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){
               if( j!=best_used[rr] ){
-                Node val = getModelBasedProjectionValue( mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta,
+                Node val = getModelBasedProjectionValue( pv, mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta,
                                                          mbp_vts_coeff[rr][0][j], vts_sym[0], mbp_vts_coeff[rr][1][j], vts_sym[1] );
                 if( !val.isNull() ){
                   if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
@@ -720,7 +734,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
       TNode tv = pv;
       TNode ts = n;
       Node a_pv_coeff;
-      Node new_subs = applySubstitution( sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
+      Node new_subs = applySubstitution( vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
       if( !new_subs.isNull() ){
         sf.d_subs[j] = new_subs;
         if( !a_pv_coeff.isNull() ){
@@ -917,7 +931,7 @@ Node CegInstantiator::constructInstantiation( Node n, std::map< Node, Node >& su
   }
 }
 
-Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
+Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
                                          std::vector< Node >& vars, Node& pv_coeff, bool try_coeff ) {
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
   Assert( n==Rewriter::rewrite( n ) );
@@ -935,10 +949,26 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std:
     if( n!=nret ){
       nret = Rewriter::rewrite( nret );
     }
-    //result is nret
     return nret;
   }else{
-    if( try_coeff ){
+    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( !coeff[i].isNull() ){
+          Assert( coeff[i].isConst() );
+          nsubs.push_back( Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) ) ));
+        }else{
+          nsubs.push_back( subs[i] );
+        }
+      }
+      Node nret = n.substitute( vars.begin(), vars.end(), nsubs.begin(), nsubs.end() );
+      if( n!=nret ){
+        nret = Rewriter::rewrite( nret );
+      }
+      return nret;
+    }else if( try_coeff ){
       //must convert to monomial representation
       std::map< Node, Node > msum;
       if( QuantArith::getMonomialSum( n, msum ) ){
@@ -999,8 +1029,12 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std:
   }
 }
 
-Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta,
+Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta,
                                                     Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ) {
+  if( e.getType().isInteger() && !t.getType().isInteger() ){
+    //TODO : round up/down this bound?
+    return Node::null();
+  }
   Node val = t;
   Trace("cbqi-bound2") << "Value : " << val << std::endl;
   //add rho value
@@ -1008,6 +1042,7 @@ Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c
   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() ){
@@ -1019,7 +1054,7 @@ Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c
     Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl;
     Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl;
   }
-  if( !new_theta.isNull() ){
+  if( !new_theta.isNull() && e.getType().isInteger() ){
     Node rho;
     if( isLower ){
       rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 7dd6ef12b..38bb12e5b 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -107,12 +107,12 @@ private:
                               unsigned j, std::map< Node, Node >& cons );
   bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons );
   Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons );
-  Node applySubstitution( Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) {
-    return applySubstitution( n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff );
+  Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) {
+    return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff );
   }
-  Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
+  Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
                           std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true );
-  Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta,
+  Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta,
                                      Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta );
   void processAssertions();
   void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index eb1ce56ef..9330bac7e 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -122,8 +122,6 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
   }
   if( usable ){
     Trace("user-pat") << "Add user pattern: " << pat << " for " << f << std::endl;
-    //extend to literal matching
-    d_quantEngine->getPhaseReqTerms( f, nodes );
     //check match option
     int matchOption = 0;
     if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
@@ -260,8 +258,6 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
       }
       Trace("auto-gen-trigger") << std::endl;
     }
-    //extend to literal matching (if applicable)
-    d_quantEngine->getPhaseReqTerms( f, patTermsF );
     //sort into single/multi triggers
     std::map< Node, std::vector< Node > > varContains;
     d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index b32f27d8f..f5333dbe1 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -56,7 +56,7 @@ 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() ){
@@ -164,7 +164,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     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) ){
+        if( !options::cbqi() || !TermDb::hasInstConstAttr( q ) ){
           quantActive = true;
         }
         d_quants.push_back( q );
@@ -198,6 +198,15 @@ bool InstantiationEngine::checkComplete() {
   }
 }
 
+
+void InstantiationEngine::preRegisterQuantifier( Node q ) {
+  if( options::cbqi() ){
+    if( d_i_cbqi->doCbqi( q ) ){
+      d_quantEngine->setOwner( q, this );
+    }
+  }
+}
+
 void InstantiationEngine::registerQuantifier( Node f ){
   if( d_quantEngine->hasOwnership( f, this ) ){
     for( unsigned i=0; i<d_instStrategies.size(); ++i ){
@@ -230,7 +239,6 @@ void InstantiationEngine::registerQuantifier( Node f ){
 }
 
 void InstantiationEngine::assertNode( Node f ){
-
 }
 
 bool InstantiationEngine::isIncomplete( Node q ) {
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index e545ff43d..51daef9dc 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -94,7 +94,8 @@ public:
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
-  void registerQuantifier( Node f );
+  void preRegisterQuantifier( Node q );
+  void registerQuantifier( Node q );
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
   Node getNextDecisionRequest();
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index bf17867bf..f2a47e8d8 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -416,50 +416,6 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node
   }
 }
 
-bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
-  std::map< Node, bool >::iterator it = currCond.find( n );
-  if( it==currCond.end() ){
-    Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl;
-    new_cond.push_back( n );
-    currCond[n] = pol;
-    return true;
-  }else{
-    Assert( it->second==pol );
-    return false;
-  }
-}
-
-void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
-  if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      setEntailedCond( n[i], pol, currCond, new_cond );
-    }
-  }else if( n.getKind()==NOT ){
-    setEntailedCond( n[0], !pol, currCond, new_cond );
-  }
-  if( addEntailedCond( n, pol, currCond, new_cond ) ){
-    if( n.getKind()==APPLY_TESTER ){
-      const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
-      unsigned index = Datatype::indexOf(n.getOperator().toExpr());
-      Assert( dt.getNumConstructors()>1 );
-      if( pol ){
-        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          if( i!=index ){
-            Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
-            addEntailedCond( t, false, currCond, new_cond );
-          }
-        }
-      }else{
-        if( dt.getNumConstructors()==2 ){
-          int oindex = 1-index;
-          Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
-          addEntailedCond( t, true, currCond, new_cond );
-        }
-      }
-    }
-  }
-}
-
 int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
   std::map< Node, bool >::iterator it = currCond.find( n );
   if( it!=currCond.end() ){
@@ -507,74 +463,213 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
   return 0;
 }
 
-Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond ) {
-  bool changed = false;
-  std::vector< Node > children;
-  for( size_t i=0; i<body.getNumChildren(); i++ ){
-    std::vector< Node > new_cond;
-    if( body.getKind()==ITE && i>0 ){
-      setEntailedCond( children[0], i==1, currCond, new_cond );
-    }
-    bool newHasPol;
-    bool newPol;
-    QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
-    Node nn = computeProcessIte( body[i], newHasPol, newPol, currCond );
-    if( body.getKind()==ITE ){
-      if( i==0 ){
-        int res = getEntailedCond( nn, currCond );
-        if( res==1 ){
-          return computeProcessIte( body[1], hasPol, pol, currCond );
-        }else if( res==-1 ){
-          return computeProcessIte( body[2], hasPol, pol, currCond );
+bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+  std::map< Node, bool >::iterator it = currCond.find( n );
+  if( it==currCond.end() ){
+    Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl;
+    new_cond.push_back( n );
+    currCond[n] = pol;
+    return true;
+  }else{
+    Assert( it->second==pol );
+    return false;
+  }
+}
+
+void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+  if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      setEntailedCond( n[i], pol, currCond, new_cond );
+    }
+  }else if( n.getKind()==NOT ){
+    setEntailedCond( n[0], !pol, currCond, new_cond );
+  }else if( n.getKind()==ITE ){
+    int pol = getEntailedCond( n, currCond );
+    if( pol==1 ){
+      setEntailedCond( n[1], pol, currCond, new_cond );
+    }else if( pol==-1 ){
+      setEntailedCond( n[2], pol, currCond, new_cond );
+    }
+  }
+  if( addEntailedCond( n, pol, currCond, new_cond ) ){
+    if( n.getKind()==APPLY_TESTER ){
+      const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+      unsigned index = Datatype::indexOf(n.getOperator().toExpr());
+      Assert( dt.getNumConstructors()>1 );
+      if( pol ){
+        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+          if( i!=index ){
+            Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
+            addEntailedCond( t, false, currCond, new_cond );
+          }
         }
       }else{
-        for( unsigned j=0; j<new_cond.size(); j++ ){
-          currCond.erase( new_cond[j] );
+        if( dt.getNumConstructors()==2 ){
+          int oindex = 1-index;
+          Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
+          addEntailedCond( t, true, currCond, new_cond );
         }
       }
     }
-    children.push_back( nn );
-    changed = changed || nn!=body[i];
   }
-  if( changed ){
-    if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      children.insert( children.begin(), body.getOperator() );
+}
+
+Node QuantifiersRewriter::computeProcessTerms( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
+                                               std::map< Node, Node >& cache, std::map< Node, Node >& icache,
+                                               std::vector< Node >& new_vars, std::vector< Node >& new_conds ) {
+  Node ret;
+  std::map< Node, Node >::iterator iti = cache.find( body );
+  if( iti!=cache.end() ){
+    ret = iti->second;
+  }else{
+    bool do_ite = false;
+    if( body.getKind()==ITE && nCurrCond<8 ){
+      do_ite = true;
+      nCurrCond = nCurrCond + 1;
+    }
+    bool changed = false;
+    std::vector< Node > children;
+    for( size_t i=0; i<body.getNumChildren(); i++ ){
+      std::vector< Node > new_cond;
+      if( do_ite && i>0 ){
+        setEntailedCond( children[0], i==1, currCond, new_cond );
+        cache.clear();
+      }
+      bool newHasPol;
+      bool newPol;
+      QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+      Node nn = computeProcessTerms( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+      if( body.getKind()==ITE ){
+        if( i==0 ){
+          int res = getEntailedCond( nn, currCond );
+          if( res==1 ){
+            ret = computeProcessTerms( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+            break;
+          }else if( res==-1 ){
+            ret = computeProcessTerms( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+            break;
+          }
+        }else{
+          for( unsigned j=0; j<new_cond.size(); j++ ){
+            currCond.erase( new_cond[j] );
+          }
+          cache.clear();
+        }
+      }
+      children.push_back( nn );
+      changed = changed || nn!=body[i];
+    }
+    if( ret.isNull() && changed ){
+      if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.insert( children.begin(), body.getOperator() );
+      }
+      ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
+    }else{
+      ret = body;
     }
-    body = NodeManager::currentNM()->mkNode( body.getKind(), children );
+    cache[body] = ret;
   }
 
-  if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
-    for( size_t i=0; i<2; i++ ){
-      if( body[i].getKind()==ITE ){
-        Node no = i==0 ? body[1] : body[0];
-        if( no.getKind()!=ITE ){
-          bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
-          std::vector< Node > children;
-          children.push_back( body[i][0] );
-          for( size_t j=1; j<=2; j++ ){
-            //check if it rewrites to a constant
-            Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
-            nn = Rewriter::rewrite( nn );
-            children.push_back( nn );
-            if( nn.isConst() ){
-              doRewrite = true;
+  iti = icache.find( ret );
+  if( iti!=icache.end() ){
+    return iti->second;
+  }else{
+    Node prev = ret;
+    if( ret.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
+      for( size_t i=0; i<2; i++ ){
+        if( ret[i].getKind()==ITE ){
+          Node no = i==0 ? ret[1] : ret[0];
+          if( no.getKind()!=ITE ){
+            bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
+            std::vector< Node > children;
+            children.push_back( ret[i][0] );
+            for( size_t j=1; j<=2; j++ ){
+              //check if it rewrites to a constant
+              Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, ret[i][j] );
+              nn = Rewriter::rewrite( nn );
+              children.push_back( nn );
+              if( nn.isConst() ){
+                doRewrite = true;
+              }
+            }
+            if( doRewrite ){
+              ret = NodeManager::currentNM()->mkNode( ITE, children );
+              break;
             }
           }
-          if( doRewrite ){
-            return NodeManager::currentNM()->mkNode( ITE, children );
+        }
+      }
+    }else if( ret.getKind()==INTS_DIVISION_TOTAL || ret.getKind()==INTS_MODULUS_TOTAL ){
+      Node num = ret[0];
+      Node den = ret[1];
+      if(den.isConst()) {
+        const Rational& rat = den.getConst<Rational>();
+        Assert(!num.isConst());
+        if(rat != 0) {
+          Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+          new_vars.push_back( intVar );
+          Node cond;
+          if(rat > 0) {
+            cond = NodeManager::currentNM()->mkNode(kind::AND,
+                     NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num),
+                     NodeManager::currentNM()->mkNode(kind::LT, num,
+                       NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(1))))));
+          } else {
+            cond = NodeManager::currentNM()->mkNode(kind::AND,
+                     NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num),
+                     NodeManager::currentNM()->mkNode(kind::LT, num,
+                       NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(-1))))));
           }
+          new_conds.push_back( cond.negate() );
+          if( ret.getKind()==INTS_DIVISION_TOTAL ){
+            ret = intVar;
+          }else{
+            ret = NodeManager::currentNM()->mkNode(kind::MINUS, num, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar));
+          }
+        }
+      }
+    }else if( ret.getKind()==TO_INTEGER || ret.getKind()==IS_INTEGER ){
+      Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+      new_vars.push_back( intVar );
+      new_conds.push_back(NodeManager::currentNM()->mkNode(kind::AND,
+                            NodeManager::currentNM()->mkNode(kind::LT,
+                              NodeManager::currentNM()->mkNode(kind::MINUS, ret[0], NodeManager::currentNM()->mkConst(Rational(1))), intVar),
+                            NodeManager::currentNM()->mkNode(kind::LEQ, intVar, ret[0])).negate());
+      if( ret.getKind()==TO_INTEGER ){
+        ret = intVar;
+      }else{
+        ret = ret[0].eqNode( intVar );
+      }
+    }
+    icache[prev] = ret;
+    return ret;
+  }
+}
+
+Node QuantifiersRewriter::computeProcessIte( Node body ){
+  if( body.getKind()==ITE ){
+    if( options::iteDtTesterSplitQuant() ){
+      Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
+      std::map< Node, Node > pcons;
+      std::map< Node, std::map< int, Node > > ncons;
+      std::vector< Node > conj;
+      computeDtTesterIteSplit( body, pcons, ncons, conj );
+      Assert( !conj.empty() );
+      if( conj.size()>1 ){
+        Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
+        for( unsigned i=0; i<conj.size(); i++ ){
+          Trace("quantifiers-rewrite-ite") << "   " << conj[i] << std::endl;
         }
+        return NodeManager::currentNM()->mkNode( AND, conj );
       }
     }
-  }else if( body.getKind()==ITE ){
-    if( body.getType().isBoolean() && hasPol && options::iteCondVarSplitQuant() ){
+    if( options::iteCondVarSplitQuant() ){
       Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+      bool do_split = false;
       for( unsigned r=0; r<2; r++ ){
         //check if there is a variable elimination
         Node b = r==0 ? body[0] : body[0].negate();
         QuantPhaseReq qpr( b );
-        std::vector< Node > vars;
-        std::vector< Node > subs;
         Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
         for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
           Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
@@ -584,16 +679,18 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, s
                 if( it->first[i].getKind()==BOUND_VARIABLE ){
                   unsigned j = i==0 ? 1 : 0;
                   if( !TermDb::containsTerm( it->first[j], it->first[i] ) ){
-                    vars.push_back( it->first[i] );
-                    subs.push_back( it->first[j] );
+                    do_split = true;
                     break;
                   }
                 }
               }
             }
           }
+          if( do_split ){
+            break;
+          }
         }
-        if( !vars.empty() ){
+        if( do_split ){
           //bool cpol = (r==1);
           Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
           //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
@@ -610,27 +707,6 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, s
   return body;
 }
 
-Node QuantifiersRewriter::computeProcessIte2( Node body ){
-  if( body.getKind()==ITE ){
-    if( options::iteDtTesterSplitQuant() ){
-      Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
-      std::map< Node, Node > pcons;
-      std::map< Node, std::map< int, Node > > ncons;
-      std::vector< Node > conj;
-      computeDtTesterIteSplit( body, pcons, ncons, conj );
-      Assert( !conj.empty() );
-      if( conj.size()>1 ){
-        Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
-        for( unsigned i=0; i<conj.size(); i++ ){
-          Trace("quantifiers-rewrite-ite") << "   " << conj[i] << std::endl;
-        }
-        return NodeManager::currentNM()->mkNode( AND, conj );
-      }
-    }
-  }
-  return body;
-}
-
 
 Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
   Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
@@ -641,13 +717,16 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
     //Notice() << "   " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
     if( it->first.getKind()==EQUAL ){
       if( it->second && options::varElimQuant() ){
+        TypeNode types[2];
+        for( int i=0; i<2; i++ ){
+          types[i] = it->first[i].getType();
+        }
         for( int i=0; i<2; i++ ){
-          int j = i==0 ? 1 : 0;
           std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
           if( ita!=args.end() ){
-            if( !TermDb::containsTerm( it->first[j], it->first[i] ) ){
+            if( !TermDb::containsTerm( it->first[1-i], it->first[i] ) && types[1-i].isSubtypeOf( types[i] ) ){
               vars.push_back( it->first[i] );
-              subs.push_back( it->first[j] );
+              subs.push_back( it->first[1-i] );
               args.erase( ita );
               break;
             }
@@ -1201,12 +1280,11 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
     return options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_NNF ){
     return options::nnfQuant();
-  }else if( computeOption==COMPUTE_PROCESS_ITE ){
-    //always eliminate redundant conditions in ITE
+  }else if( computeOption==COMPUTE_PROCESS_TERMS ){
     return true;
     //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
-  }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
-    return options::iteDtTesterSplitQuant();
+  }else if( computeOption==COMPUTE_PROCESS_ITE ){
+    return options::iteDtTesterSplitQuant() || options::iteCondVarSplitQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
@@ -1241,11 +1319,18 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
       return computeAggressiveMiniscoping( args, n );
     }else if( computeOption==COMPUTE_NNF ){
       n = computeNNF( n );
-    }else if( computeOption==COMPUTE_PROCESS_ITE ){
+    }else if( computeOption==COMPUTE_PROCESS_TERMS ){
       std::map< Node, bool > curr_cond;
-      n = computeProcessIte( n, true, true, curr_cond );
-    }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
-      n = computeProcessIte2( n );
+      std::map< Node, Node > cache;
+      std::map< Node, Node > icache;
+      std::vector< Node > new_conds;
+      n = computeProcessTerms( n, true, true, curr_cond, 0, cache, icache, args, new_conds );
+      if( !new_conds.empty() ){
+        new_conds.push_back( n );
+        n = NodeManager::currentNM()->mkNode( OR, new_conds );
+      }
+    }else if( computeOption==COMPUTE_PROCESS_ITE ){
+      n = computeProcessIte( n );
     }else if( computeOption==COMPUTE_PRENEX ){
       n = computePrenex( n, args, true );
     }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 828099984..98a83b7de 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -44,8 +44,11 @@ private:
   static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   static Node computeNNF( Node body );
-  static Node computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond );
-  static Node computeProcessIte2( Node body );
+  //cache is dependent upon currCond, icache is not, new_conds are negated conditions
+  static Node computeProcessTerms( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
+                                   std::map< Node, Node >& cache, std::map< Node, Node >& icache,
+                                   std::vector< Node >& new_vars, std::vector< Node >& new_conds );
+  static Node computeProcessIte( Node body );
   static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
@@ -56,8 +59,8 @@ private:
     COMPUTE_MINISCOPING,
     COMPUTE_AGGRESSIVE_MINISCOPING,
     COMPUTE_NNF,
+    COMPUTE_PROCESS_TERMS,
     COMPUTE_PROCESS_ITE,
-    COMPUTE_PROCESS_ITE_2,
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
     //COMPUTE_FLATTEN_ARGS_UF,
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 28a4d4c6b..913d9b0c6 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -128,7 +128,7 @@ 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() ){
+  if( !options::finiteModelFind() || options::fmfInstEngine() || options::cbqi() ){
     d_inst_engine = new quantifiers::InstantiationEngine( this );
     d_modules.push_back(  d_inst_engine );
     if( options::cbqi() && options::cbqiModel() ){
@@ -201,7 +201,7 @@ d_presolve_cache_wic(u){
   }else{
     d_rel_dom = NULL;
   }
-  
+
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
     if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
@@ -344,7 +344,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
     }
   }
-  
+
   d_hasAddedLemma = false;
   bool setIncomplete = false;
   if( e==Theory::EFFORT_LAST_CALL ){
@@ -355,7 +355,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
   }
   bool usedModelBuilder = false;
-    
+
   Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl;
   if( needsCheck ){
     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
@@ -479,7 +479,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }else{
     Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl;
   }
-  
+
   //SAT case
   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
     if( options::produceModels() ){
@@ -554,6 +554,9 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
       //make instantiation constants for f
       d_term_db->makeInstantiationConstantsFor( f );
       d_term_db->computeAttributes( f );
+      for( unsigned i=0; i<d_modules.size(); i++ ){
+        d_modules[i]->preRegisterQuantifier( f );
+      }
       QuantifiersModule * qm = getOwner( f );
       if( qm!=NULL ){
         Trace("quant") << "   Owner : " << qm->identify() << std::endl;
@@ -563,7 +566,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
         d_quant_rel->registerQuantifier( f );
       }
       //register with each module
-      for( int i=0; i<(int)d_modules.size(); i++ ){
+      for( unsigned i=0; i<d_modules.size(); i++ ){
         d_modules[i]->registerQuantifier( f );
       }
       Node ceBody = d_term_db->getInstConstantBody( f );
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 30c4dabdf..76fb920bb 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -68,6 +68,8 @@ public:
   /* check was complete (e.g. no lemmas implies a model) */
   virtual bool checkComplete() { return false; }
   /* 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 propagate( Theory::Effort level ){}