Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Enable redundant ITE branch elimination in quantifiers rewriter.

10 files changed, 317 insertions, 258 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 9d49f3d72..bf0168c64 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -74,10 +74,15 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
     Node pv = d_vars[i];
     TypeNode pvtn = pv.getType();
     Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl;
+    Node pv_value;
+    if( options::cbqiModel() ){
+      pv_value = d_qe->getModel()->getValue( pv );
+      Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+    }
 
     //if in effort=2, we must choose at least one model value
     if( (i+1)<d_vars.size() || effort!=2 ){
-      
+
       //[1] easy case : pv is in the equivalence class as another term not containing pv
       Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
       std::map< Node, Node >::iterator itr = d_curr_rep.find( pv );
@@ -169,38 +174,37 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                     }
                     Node eq = eq_lhs.eqNode( eq_rhs );
                     eq = Rewriter::rewrite( eq );
-                    //cannot contain infinity
-                    if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){
-                      Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
-                      std::map< Node, Node > msum;
-                      if( QuantArith::getMonomialSumLit( eq, msum ) ){
-                        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;
-                        }
-                        Node veq;
-                        if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
-                          Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl;
-                          Node veq_c;
-                          if( veq[0]!=pv ){
-                            Node veq_v;
-                            if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
-                              Assert( veq_v==pv );
-                            }
-                          }
-                          Node val = veq[1];
-                          //eliminate coefficient if real
-                          if( !pvtn.isInteger() && !veq_c.isNull() ){
-                            val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
-                            val = Rewriter::rewrite( val );
-                            veq_c = Node::null();
+                    //cannot contain infinity?
+                    //if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){
+                    Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
+                    std::map< Node, Node > msum;
+                    if( QuantArith::getMonomialSumLit( eq, msum ) ){
+                      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;
+                      }
+                      Node veq;
+                      if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
+                        Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl;
+                        Node veq_c;
+                        if( veq[0]!=pv ){
+                          Node veq_v;
+                          if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+                            Assert( veq_v==pv );
                           }
-                          if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
-                            subs_proc[val][veq_c] = true;
-                            if( addInstantiationInc( val, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
-                              return true;
-                            }
+                        }
+                        Node val = veq[1];
+                        //eliminate coefficient if real
+                        if( !pvtn.isInteger() && !veq_c.isNull() ){
+                          val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
+                          val = Rewriter::rewrite( val );
+                          veq_c = Node::null();
+                        }
+                        if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
+                          subs_proc[val][veq_c] = true;
+                          if( addInstantiationInc( val, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
+                            return true;
                           }
                         }
                       }
@@ -264,97 +268,111 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                 //if it contains pv, not infinity
                 if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){
                   Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
-                  //cannot contain infinity
-                  if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){
-                    Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl;
-                    Trace("cbqi-inst-debug") << "         substituted : " << satom << ", pol = " << pol << std::endl;
-                    std::map< Node, Node > msum;
-                    if( QuantArith::getMonomialSumLit( satom, msum ) ){
-                      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;
-                      }
-                      Node vatom;
-                      //isolate pv in the inequality
-                      int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true );
-                      if( ires!=0 ){
-                        Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl;
-                        Node val = vatom[ ires==1 ? 1 : 0 ];
-                        Node pvm = vatom[ ires==1 ? 0 : 1 ];
-                        //get monomial
-                        Node veq_c;
-                        if( pvm!=pv ){
-                          Node veq_v;
-                          if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
-                            Assert( veq_v==pv );
-                          }
-                        }
-                        //eliminate coefficient if real
-                        if( !pvtn.isInteger() && !veq_c.isNull() ){
-                          val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
-                          val = Rewriter::rewrite( val );
-                          veq_c = Node::null();
+                  //cannot contain infinity?
+                  //if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){
+                  Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl;
+                  Trace("cbqi-inst-debug") << "         substituted : " << satom << ", pol = " << pol << std::endl;
+                  std::map< Node, Node > msum;
+                  if( QuantArith::getMonomialSumLit( satom, msum ) ){
+                    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;
+                    }
+                    Node vatom;
+                    //isolate pv in the inequality
+                    int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true );
+                    if( ires!=0 ){
+                      Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl;
+                      Node val = vatom[ ires==1 ? 1 : 0 ];
+                      Node pvm = vatom[ ires==1 ? 0 : 1 ];
+                      //get monomial
+                      Node veq_c;
+                      if( pvm!=pv ){
+                        Node veq_v;
+                        if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+                          Assert( veq_v==pv );
                         }
+                      }
+                      //eliminate coefficient if real
+                      if( !pvtn.isInteger() && !veq_c.isNull() ){
+                        val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
+                        val = Rewriter::rewrite( val );
+                        veq_c = Node::null();
+                      }
 
-                        //disequalities are both strict upper and lower bounds
-                        unsigned rmax = atom.getKind()==GEQ ? 1 : 2;
-                        for( unsigned r=0; r<rmax; r++ ){
-                          int uires = ires;
-                          Node uval = val;
-                          if( atom.getKind()==GEQ ){
-                            //push negation downwards
-                            if( !pol ){
-                              uires = -ires;
-                              if( pvtn.isInteger() ){
-                                uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
-                                uval = Rewriter::rewrite( uval );
-                              }else{
-                                Assert( pvtn.isReal() );
-                                //now is strict inequality
-                                uires = uires*2;
-                              }
-                            }
-                          }else{
-                            Assert( atom.getKind()==EQUAL && !pol );
+                      //disequalities are either strict upper or lower bounds
+                      unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2;
+                      for( unsigned r=0; r<rmax; r++ ){
+                        int uires = ires;
+                        Node uval = val;
+                        if( atom.getKind()==GEQ ){
+                          //push negation downwards
+                          if( !pol ){
+                            uires = -ires;
                             if( pvtn.isInteger() ){
-                              uires = r==0 ? -1 : 1;
                               uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
                               uval = Rewriter::rewrite( uval );
                             }else{
                               Assert( pvtn.isReal() );
-                              uires = r==0 ? -2 : 2;
+                              //now is strict inequality
+                              uires = uires*2;
                             }
                           }
-                          Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
-                          if( !veq_c.isNull() ){
-                            Trace("cbqi-bound-inf") << veq_c << " * ";
-                          }
-                          Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl;
+                        }else{
+                          unsigned use_r = r;
                           if( options::cbqiModel() ){
-                            //just store bounds, will choose based on tighest bound
-                            unsigned index = uires>0 ? 0 : 1;
-                            mbp_bounds[index].push_back( uval );
-                            mbp_coeff[index].push_back( veq_c );
-                            mbp_strict[index].push_back( uires==2 || uires==-2 );
-                            mbp_lit[index].push_back( lit );
+                            // disequality is a disjunction : only consider the bound in the direction of the model
+                            Node rhs_value = d_qe->getModel()->getValue( val );
+                            Node lhs_value = pv_value;
+                            if( !veq_c.isNull() ){
+                              lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c );
+                              lhs_value = Rewriter::rewrite( lhs_value );
+                            }
+                            Assert( lhs_value!=rhs_value );
+                            Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
+                            cmp = Rewriter::rewrite( cmp );
+                            Assert( cmp.isConst() );
+                            use_r = cmp==d_true ? 1 : 0;
+                          }
+                          Assert( atom.getKind()==EQUAL && !pol );
+                          if( pvtn.isInteger() ){
+                            uires = use_r==0 ? -1 : 1;
+                            uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+                            uval = Rewriter::rewrite( uval );
                           }else{
-                            //take into account delta
-                            if( uires==2 || uires==-2 ){
-                              if( d_use_vts_delta ){
-                                Node delta = d_qe->getTermDatabase()->getVtsDelta();
-                                uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
-                                uval = Rewriter::rewrite( uval );
-                              }
+                            Assert( pvtn.isReal() );
+                            uires = use_r==0 ? -2 : 2;
+                          }
+                        }
+                        Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
+                        if( !veq_c.isNull() ){
+                          Trace("cbqi-bound-inf") << veq_c << " * ";
+                        }
+                        Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl;
+                        if( options::cbqiModel() ){
+                          //just store bounds, will choose based on tighest bound
+                          unsigned index = uires>0 ? 0 : 1;
+                          mbp_bounds[index].push_back( uval );
+                          mbp_coeff[index].push_back( veq_c );
+                          mbp_strict[index].push_back( uires==2 || uires==-2 );
+                          mbp_lit[index].push_back( lit );
+                        }else{
+                          //take into account delta
+                          if( uires==2 || uires==-2 ){
+                            if( d_use_vts_delta ){
+                              Node delta = d_qe->getTermDatabase()->getVtsDelta();
+                              uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
+                              uval = Rewriter::rewrite( uval );
                             }
-                            if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
-                              subs_proc[uval][veq_c] = true;
-                              if( addInstantiationInc( uval, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
-                                return true;
-                              }
-                            }else{
-                              Trace("cbqi-inst-debug") << "...already processed." << std::endl;
+                          }
+                          if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
+                            subs_proc[uval][veq_c] = true;
+                            if( addInstantiationInc( uval, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
+                              return true;
                             }
+                          }else{
+                            Trace("cbqi-inst-debug") << "...already processed." << std::endl;
                           }
                         }
                       }
@@ -371,13 +389,11 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
           bool upper_first = false;
           unsigned best_used[2];
           std::vector< Node > t_values[2];
-          Node pv_value = d_qe->getModel()->getValue( pv );
-          Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
           //try optimal bounds
           for( unsigned r=0; r<2; r++ ){
             int rr = upper_first ? (1-r) : r;
             if( mbp_bounds[rr].empty() ){
-              if( d_use_vts_inf ){
+              if( d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ) ){
                 Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl;
                 //no bounds, we do +- infinity
                 Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn );
@@ -459,7 +475,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       int new_effort = pvtn.isBoolean() ? effort : 1;
 #ifdef MBP_STRICT_ASSERTIONS
       //we only resort to values in the case of booleans
-      Assert( !options::cbqiUseInf() || pvtn.isBoolean() );
+      Assert( !options::cbqiUseInfInt() || !options::cbqiUseInfReal() || pvtn.isBoolean() );
 #endif
       if( addInstantiationInc( mv, pv, pv_coeff_m, subs, vars, coeff, has_coeff, theta, i, new_effort ) ){
         return true;
@@ -474,10 +490,10 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
 bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars,
                                            std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ) {
   if( Trace.isOn("cbqi-inst") ){
-    for( unsigned i=0; i<subs.size(); i++ ){
+    for( unsigned j=0; j<subs.size(); j++ ){
       Trace("cbqi-inst") << " ";
     }
-    Trace("cbqi-inst") << "i: ";
+    Trace("cbqi-inst") << subs.size() << ": ";
     if( !pv_coeff.isNull() ){
       Trace("cbqi-inst") << pv_coeff << " * ";
     }
@@ -540,11 +556,6 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::
     if( !pv_coeff.isNull() ){
       has_coeff.push_back( pv );
     }
-    Trace("cbqi-inst-debug") << i << ": ";
-    if( !pv_coeff.isNull() ){
-      Trace("cbqi-inst-debug") << pv_coeff << "*";
-    }
-    Trace("cbqi-inst-debug") << pv << " -> " << n << std::endl;
     Node new_theta = theta;
     if( !pv_coeff.isNull() ){
       if( new_theta.isNull() ){
@@ -829,13 +840,13 @@ void CegInstantiator::processAssertions() {
   d_curr_eqc.clear();
   d_curr_rep.clear();
   d_curr_arith_eqc.clear();
-  
+
   eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
   //to eliminate identified illegal terms
   std::map< Node, Node > aux_uf;
   std::map< Node, Node > aux_subs;
   std::map< Node, bool > aux_subs_inelig;
-  
+
   //for each variable
   bool has_arith_var = false;
   for( unsigned i=0; i<d_vars.size(); i++ ){
@@ -857,6 +868,16 @@ void CegInstantiator::processAssertions() {
             d_curr_asserts[tid].push_back( lit );
             Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
             if( lit.getKind()==EQUAL ){
+              std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit );
+              if( itae!=d_aux_eq.end() ){
+                for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){
+                  aux_subs[ itae2->first ] = itae2->second;
+                  Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl;
+                }
+              }
+            } 
+            /*
+            if( lit.getKind()==EQUAL ){
               //check if it is an auxiliary variable (for instance, from ITE removal).  If so, solve for it.
               for( unsigned k=0; k<2; k++ ){
                 Node s = lit[k];
@@ -881,6 +902,7 @@ void CegInstantiator::processAssertions() {
                 }
               }
             }
+            */
           }
         }
       }
@@ -910,7 +932,7 @@ void CegInstantiator::processAssertions() {
     while( !eqcs_i.isFinished() ){
       Node r = *eqcs_i;
       TypeNode rtn = r.getType();
-      if( rtn.isInteger() || rtn.isReal() ){  
+      if( rtn.isInteger() || rtn.isReal() ){
         Trace("cbqi-proc-debug") << "...arith eqc: " << r << std::endl;
         d_curr_arith_eqc.push_back( r );
         if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
@@ -935,21 +957,21 @@ void CegInstantiator::processAssertions() {
     if( it!=aux_subs.end() ){
       addToAuxVarSubstitution( subs_lhs, subs_rhs, l, it->second );
     }else{
+      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << l << "!!!" << std::endl;
 #ifdef MBP_STRICT_ASSERTIONS
       Assert( false );
 #endif
-      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << l << "!!!" << std::endl;
     }
-  }  
+  }
+
 
-  
   //apply substitutions to everything, if necessary
   if( !subs_lhs.empty() ){
     Trace("cbqi-proc") << "Applying substitution : " << std::endl;
     for( unsigned i=0; i<subs_lhs.size(); i++ ){
       Trace("cbqi-proc") << "  " << subs_lhs[i] << " -> " << subs_rhs[i] << std::endl;
     }
-    
+
     for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
       for( unsigned i=0; i<it->second.size(); i++ ){
         Node lit = it->second[i];
@@ -979,6 +1001,7 @@ void CegInstantiator::processAssertions() {
       if( d_inelig.find( n )==d_inelig.end() ){
         //must contain at least one variable
         if( !d_prog_var[n].empty() ){
+          Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
           akeep.push_back( n );
         }else{
           Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
@@ -990,7 +1013,7 @@ void CegInstantiator::processAssertions() {
     it->second.clear();
     it->second.insert( it->second.end(), akeep.begin(), akeep.end() );
   }
-  
+
   //remove duplicate terms from eqc
   for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){
     std::vector< Node > new_eqc;
@@ -1006,7 +1029,7 @@ void CegInstantiator::processAssertions() {
 
 void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) {
   r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
-  
+
   std::vector< Node > cl;
   cl.push_back( l );
   std::vector< Node > cr;
@@ -1016,7 +1039,7 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st
     nr = Rewriter::rewrite( nr );
     subs_rhs[i] = nr;
   }
-  
+
   subs_lhs.push_back( l );
   subs_rhs.push_back( r );
 }
@@ -1369,21 +1392,7 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
   if( e<1 ){
     return STATUS_UNFINISHED;
   }else if( e==1 ){
-    CegInstantiator * cinst;
-    std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
-    if( it==d_cinst.end() ){
-      cinst = new CegInstantiator( d_quantEngine, d_out, true, options::cbqiUseInf() );
-      for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-        cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
-      }
-      std::map< Node, std::vector< Node > >::iterator itav = d_aux_variables.find( f );
-      if( itav!=d_aux_variables.end() ){
-        cinst->d_aux_vars.insert( cinst->d_aux_vars.begin(), itav->second.begin(), itav->second.end() );
-      }
-      d_cinst[f] = cinst;
-    }else{
-      cinst = it->second;
-    }
+    CegInstantiator * cinst = getInstantiator( f );
     Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
     d_curr_quant = f;
     bool addedLemma = cinst->check();
@@ -1434,14 +1443,17 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
   }
 }
 
-void InstStrategyCegqi::setAuxiliaryVariables( Node q, std::vector< Node >& vars ) {
+CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
-  if( it!=d_cinst.end() ){
-    Assert( it->second->d_aux_vars.empty() );
-    it->second->d_aux_vars.insert( it->second->d_aux_vars.end(), vars.begin(), vars.end() );
+  if( it==d_cinst.end() ){
+    CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true );
+    for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
+      cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
+    }
+    d_cinst[q] = cinst;
+    return cinst;
   }else{
-    Assert( d_aux_variables.find( q )==d_aux_variables.end() );
-    d_aux_variables[q].insert( d_aux_variables[q].end(), vars.begin(), vars.end() );
+   return it->second;
   }
 }
 
@@ -1453,5 +1465,3 @@ void InstStrategyCegqi::setAuxiliaryVariables( Node q, std::vector< Node >& vars
 
 
 
-
-
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 64303e1f3..f7cb290b2 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -88,6 +88,8 @@ public:
   std::vector< Node > d_vars;
   //auxiliary variables
   std::vector< Node > d_aux_vars;
+  //literals to equalities for aux vars
+  std::map< Node, std::map< Node, Node > > d_aux_eq;
   //check : add instantiations based on valuation of d_vars
   bool check();
 };
@@ -153,7 +155,6 @@ class InstStrategyCegqi : public InstStrategy {
 private:
   CegqiOutputInstStrategy * d_out;
   std::map< Node, CegInstantiator * > d_cinst;
-  std::map< Node, std::vector< Node > > d_aux_variables;
   Node d_small_const;
   Node d_curr_quant;
   bool d_check_vts_lemma_lc;
@@ -170,8 +171,8 @@ public:
   /** identify */
   std::string identify() const { return std::string("Cegqi"); }
   
-  //set auxiliary variables
-  void setAuxiliaryVariables( Node q, std::vector< Node >& vars );
+  //get instantiator for quantifier
+  CegInstantiator * getInstantiator( Node q );
 };
 
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index b12c822ef..3dad74044 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -108,18 +108,37 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           std::vector< Node > lems;
           lems.push_back( lem );
           d_quantEngine->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
-          std::vector< Node > aux_vars;
-          for( unsigned i=0; i<lems.size(); i++ ){
-            Trace("cbqi-debug") << "Counterexample lemma (processed) " << i << " : " << lems[i] << std::endl;
-            d_quantEngine->addLemma( lems[i], false );
-          }
-          for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
-            Trace("cbqi-debug") << "  Auxiliary var (from ITE) : " << i->first << std::endl;
-            aux_vars.push_back( i->first );
-          }
-          //record the auxiliary variables in the inst strategy
+          CegInstantiator * cinst = NULL;
           if( d_i_cegqi ){
-            d_i_cegqi->setAuxiliaryVariables( f, aux_vars );
+            cinst = d_i_cegqi->getInstantiator( f );
+            Assert( cinst->d_aux_vars.empty() );
+            for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
+              Trace("cbqi-debug") << "  Auxiliary var (from ITE) : " << i->first << std::endl;
+              cinst->d_aux_vars.push_back( i->first );
+            }
+          }
+          for( unsigned i=0; i<lems.size(); i++ ){
+            Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
+            if( !cinst ){
+              d_quantEngine->addLemma( lems[i], false );
+            }else{
+              Node rlem = lems[i];
+              rlem = Rewriter::rewrite( rlem );
+              Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
+              d_quantEngine->addLemma( rlem, false );
+              //record the literals that imply auxiliary variables to be equal to terms
+              if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
+                if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
+                  if( std::find( cinst->d_aux_vars.begin(), cinst->d_aux_vars.end(), lems[i][1][0] )!=cinst->d_aux_vars.end() ){
+                    Node v = lems[i][1][0];
+                    for( unsigned r=1; r<=2; r++ ){
+                      cinst->d_aux_eq[rlem[r]][v] = lems[i][r][1];
+                      Trace("cbqi-debug") << "  " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
+                    }
+                  }
+                }
+              }
+            }
           }
           
           addedLemma = true;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index b573ebd67..66de51f39 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -17,7 +17,8 @@ option miniscopeQuant --miniscope-quant bool :default true :read-write
 # ( forall x. P( x ) ) V Q
 option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  disable miniscope quantifiers for ground subformulas
-# Whether to prenex (nested universal) quantifiers
+option clauseSplit --clause-split bool :default true
+ apply clause splitting to quantified formulas
 option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
  prenex mode for quantified formulas
 # Whether to variable-eliminate quantifiers.
@@ -37,11 +38,8 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal
 # Whether to CNF quantifier bodies
 # option cnfQuant --cnf-quant bool :default false
 #  apply CNF conversion to quantified formulas
-# Whether to NNF quantifier bodies
 option nnfQuant --nnf-quant bool :default true
  apply NNF conversion to quantified formulas
-option clauseSplit --clause-split bool :default true
- apply clause splitting to quantified formulas
 # Whether to pre-skolemize quantifier bodies.
 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
 #   forall x. P( x ) => f( S( x ) ) = x
@@ -51,10 +49,8 @@ option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default
  apply skolemization to nested quantified formulass
 option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
  apply skolemization to quantified formulas aggressively
-# Whether to perform agressive miniscoping
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
-# Whether to CNF quantifier bodies
 option elimTautQuant --elim-taut-quant bool :default true
  eliminate tautological disjuncts of quantified formulas
  
@@ -246,8 +242,11 @@ option cbqiSat --cbqi-sat bool :read-write :default true
  answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
 option cbqiModel --cbqi-model bool :read-write :default true
  guide instantiations by model values for counterexample-based quantifier instantiation
-option cbqiUseInf --cbqi-use-inf bool :read-write :default false
- use infinity for vts in counterexample-based quantifier instantiation
+option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
+ use integer infinity for vts in counterexample-based quantifier instantiation
+option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false
+ use real infinity for vts in counterexample-based quantifier instantiation
+ 
  
 ### local theory extensions options 
 
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 2c65b62b3..938245871 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -313,15 +313,20 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int
 }
 
 void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
-  newHasPol = hasPol;
-  newPol = pol;
-  if( n.getKind()==NOT || ( n.getKind()==IMPLIES && child==0 ) ){
+  if( n.getKind()==AND || n.getKind()==OR ){
+    newHasPol = hasPol;
+    newPol = pol;
+  }else if( n.getKind()==IMPLIES ){
+    newHasPol = hasPol;
+    newPol = child==0 ? !pol : pol;
+  }else if( n.getKind()==NOT ){
+    newHasPol = hasPol;
     newPol = !pol;
-  }else if( n.getKind()==IFF || n.getKind()==XOR ){
-    newHasPol = false;
   }else if( n.getKind()==ITE ){
-    if( child==0 ){
-      newHasPol = false;
-    }
+    newHasPol = (child!=0) && hasPol;
+    newPol = pol;
+  }else{
+    newHasPol = false;
+    newPol = pol;
   }
 }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index d6cbe386c..c32aeeb78 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -415,89 +415,105 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node
   }
 }
 
-Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) {
-  if( body.getType().isBoolean() ){
-    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;
-              }
-            }
-            if( doRewrite ){
-              return NodeManager::currentNM()->mkNode( ITE, children );
+Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond ) {
+  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;
             }
           }
+          if( doRewrite ){
+            return NodeManager::currentNM()->mkNode( ITE, children );
+          }
         }
       }
-    }else if( body.getKind()==ITE && hasPol ){
-      if( options::iteCondVarSplitQuant() ){
-        Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
-        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;
-            if( it->second ){
-              if( it->first.getKind()==EQUAL ){
-                for( unsigned i=0; i<2; i++ ){
-                  if( it->first[i].getKind()==BOUND_VARIABLE ){
-                    unsigned j = i==0 ? 1 : 0;
-                    if( !hasArg1( it->first[i], it->first[j] ) ){
-                      vars.push_back( it->first[i] );
-                      subs.push_back( it->first[j] );
-                      break;
-                    }
+    }
+  }else if( body.getKind()==ITE ){
+    if( body.getType().isBoolean() && hasPol && options::iteCondVarSplitQuant() ){
+      Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+      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;
+          if( it->second ){
+            if( it->first.getKind()==EQUAL ){
+              for( unsigned i=0; i<2; i++ ){
+                if( it->first[i].getKind()==BOUND_VARIABLE ){
+                  unsigned j = i==0 ? 1 : 0;
+                  if( !hasArg1( it->first[i], it->first[j] ) ){
+                    vars.push_back( it->first[i] );
+                    subs.push_back( it->first[j] );
+                    break;
                   }
                 }
               }
             }
           }
-          if( !vars.empty() ){
-            //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() );
-            //pos = Rewriter::rewrite( pos );
-            Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
-            Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
-            Trace("quantifiers-rewrite-ite") << "   " << pos << std::endl;
-            Trace("quantifiers-rewrite-ite") << "   " << neg << std::endl;
-            return NodeManager::currentNM()->mkNode( AND, pos, neg );
-          }
+        }
+        if( !vars.empty() ){
+          //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() );
+          //pos = Rewriter::rewrite( pos );
+          Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
+          Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
+          Trace("quantifiers-rewrite-ite") << "   " << pos << std::endl;
+          Trace("quantifiers-rewrite-ite") << "   " << neg << std::endl;
+          return NodeManager::currentNM()->mkNode( AND, pos, neg );
         }
       }
     }
-    if( body.getKind()!=EQUAL && body.getKind()!=APPLY_UF ){
-      bool changed = false;
-      std::vector< Node > children;
-      for( size_t i=0; i<body.getNumChildren(); i++ ){
-        bool newHasPol;
-        bool newPol;
-        QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
-        Node nn = computeProcessIte( body[i], newHasPol, newPol );
-        children.push_back( nn );
-        changed = changed || nn!=body[i];
-      }
-      if( changed ){
-        return NodeManager::currentNM()->mkNode( body.getKind(), children );
+  }
+  bool changed = false;
+  std::vector< Node > children;
+  for( size_t i=0; i<body.getNumChildren(); i++ ){
+    bool newHasPol;
+    bool newPol;
+    QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+    if( body.getKind()==ITE && i>0 ){
+      currCond[children[0]] = (i==1);
+    }
+    Node nn = computeProcessIte( body[i], newHasPol, newPol, currCond );
+    if( body.getKind()==ITE && i==0 ){
+      std::map< Node, bool >::iterator itc = currCond.find( nn );
+      if( itc!=currCond.end() ){
+        if( itc->second ){
+          return computeProcessIte( body[1], hasPol, pol, currCond );
+        }else{
+          return computeProcessIte( body[2], hasPol, pol, currCond );
+        }
       }
     }
+    children.push_back( nn );
+    changed = changed || nn!=body[i];
+  }
+  if( body.getKind()==ITE ){
+    currCond.erase( children[0] );
+  }
+  if( changed ){
+    if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.insert( children.begin(), body.getOperator() );
+    }
+    return NodeManager::currentNM()->mkNode( body.getKind(), children );
+  }else{
+    return body;
   }
-  return body;
 }
 
 Node QuantifiersRewriter::computeProcessIte2( Node body ){
@@ -1140,7 +1156,9 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_NNF ){
     return options::nnfQuant();
   }else if( computeOption==COMPUTE_PROCESS_ITE ){
-    return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
+    //always eliminate redundant conditions in ITE
+    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_PRENEX ){
@@ -1182,7 +1200,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
     }else if( computeOption==COMPUTE_NNF ){
       n = computeNNF( n );
     }else if( computeOption==COMPUTE_PROCESS_ITE ){
-      n = computeProcessIte( n, true, true );
+      std::map< Node, bool > curr_cond;
+      n = computeProcessIte( n, true, true, curr_cond );
     }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
       n = computeProcessIte2( n );
     }else if( computeOption==COMPUTE_PRENEX ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index d01677171..7db80c84b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -46,7 +46,7 @@ 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 );
+  static Node computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond );
   static Node computeProcessIte2( 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 );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 13c408d85..d1a268950 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -329,6 +329,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
       debugPrintEqualityEngine( "quant-engine-ee" );
     }
+    if( Trace.isOn("quant-engine-assert") ){
+      Trace("quant-engine-assert") << "Assertions : " << std::endl;
+      getTheoryEngine()->printAssertions("quant-engine-assert");
+    }
 
     //reset relevant information
     d_conflict = false;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 96a99763d..b28a73b9d 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -798,9 +798,6 @@ private:
   /** Visitor for collecting shared terms */
   SharedTermsVisitor d_sharedTermsVisitor;
 
-  /** Prints the assertions to the debug stream */
-  void printAssertions(const char* tag);
-
   /** Dump the assertions to the dump */
   void dumpAssertions(const char* tag);
 
@@ -834,6 +831,10 @@ public:
   RemoveITE* getIteRemover() { return &d_iteRemover; }
 
   SortInference* getSortInference() { return &d_sortInfer; }
+  
+  /** Prints the assertions to the debug stream */
+  void printAssertions(const char* tag);
+
 private:
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
 public:
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index c15074d8c..d913cb76a 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1047,6 +1047,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
     //add splitting lemma for cardinality constraint
     Assert( !d_cardinality_term.isNull() );
     Node lem = getCardinalityLiteral( d_aloc_cardinality );
+    Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl;
     lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
     d_cardinality_lemma[ d_aloc_cardinality ] = lem;
     //add as lemma to output channel