Better combination of UF with cbqi, refactor quantifiers intialization.

10 files changed, 178 insertions, 101 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 5ae8905d1..3e69a616a 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -292,9 +292,9 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
       std::vector< Node > mbp_vts_coeff[2][2];
       std::vector< Node > mbp_lit[2];
       //std::vector< MbpBounds > mbp_bounds[2];
-      unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
-      for( unsigned r=0; r<rmax; r++ ){
-        TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() );
+      //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
+      for( unsigned r=0; r<2; r++ ){
+        TheoryId tid = r==0 ? Theory::theoryOf( pvtn ) : THEORY_UF;
         Trace("cbqi-inst-debug2") << "  look at assertions of " << tid << std::endl;
         std::map< TheoryId, std::vector< Node > >::iterator ita = d_curr_asserts.find( tid );
         if( ita!=d_curr_asserts.end() ){
@@ -303,7 +303,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
             Trace("cbqi-inst-debug2") << "  look at " << lit << std::endl;
             Node atom = lit.getKind()==NOT ? lit[0] : lit;
             bool pol = lit.getKind()!=NOT;
-            if( tid==THEORY_ARITH ){
+            if( pvtn.isReal() ){
               //arithmetic inequalities and disequalities
               if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){
                 Assert( atom[0].getType().isInteger() || atom[0].getType().isReal() );
@@ -614,7 +614,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
 
     //[4] resort to using value in model
     // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype
-    if( effort>0 || pvtn.isBoolean() || !curr_var.empty() ){
+    if( ( effort>0 || pvtn.isBoolean() || !curr_var.empty() ) && !pvtn.isSort() ){
       Node mv = getModelValue( pv );
       Node pv_coeff_m;
       Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
@@ -976,14 +976,10 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
 }
 
 Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) {
-  /*
-  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;
+  Assert( !e.getType().isInteger() || t.getType().isInteger() );
+  Assert( !e.getType().isInteger() || mt.getType().isInteger() );
   //add rho value
   //get the value of c*e
   Node ceValue = me;
@@ -1005,7 +1001,7 @@ Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower
     Node rho;
     //if( !mt.getType().isInteger() ){
       //round up/down
-      //mt = NodeManager::currentNM()->mkNode( 
+      //mt = NodeManager::currentNM()->mkNode(
     //}
     if( isLower ){
       rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
@@ -1157,6 +1153,7 @@ void CegInstantiator::processAssertions() {
 
   //for each variable
   std::vector< TheoryId > tids;
+  tids.push_back(THEORY_UF);
   for( unsigned i=0; i<d_vars.size(); i++ ){
     Node pv = d_vars[i];
     TypeNode pvtn = pv.getType();
@@ -1389,8 +1386,8 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
       d_var_order_index.clear();
     }
   }
-  
-  //remove ITEs 
+
+  //remove ITEs
   IteSkolemMap iteSkolemMap;
   d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
   Assert( d_aux_vars.empty() );
@@ -1466,7 +1463,7 @@ int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node
         }
       }
     }
-    
+
     ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
     if( ires!=0 ){
       Node realPart;
@@ -1510,7 +1507,7 @@ int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node
         Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
         Trace("cbqi-inst-debug") << "                 real part : " << realPart << std::endl;
         if( ires!=0 ){
-          val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS, 
+          val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS,
                                     NodeManager::currentNM()->mkNode( ires==-1 ? MINUS : PLUS, val, realPart ),
                                     NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );
           Trace("cbqi-inst-debug") << "result : " << val << std::endl;
@@ -1521,6 +1518,6 @@ int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node
     vts_coeff_inf = vts_coeff[0];
     vts_coeff_delta = vts_coeff[1];
   }
-    
+
   return ires;
 }
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 07de0a3d1..56d5022c4 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -34,7 +34,7 @@ using namespace CVC4::theory::arith;
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
 InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ){
-  
+
 }
 
 bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
@@ -44,7 +44,7 @@ bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
 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 ) ){
+    if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
       return QuantifiersEngine::QEFFORT_STANDARD;
     }
   }
@@ -57,7 +57,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
   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->getOwner( q )==this ){
+    if( doCbqi( q ) ){
       if( !hasAddedCbqiLemma( q ) ){
         d_added_cbqi_lemma.insert( q );
         Trace("cbqi") << "Do cbqi for " << q << std::endl;
@@ -76,7 +76,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
           Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
           registerCounterexampleLemma( q, lem );
         }
-      //set inactive the quantified formulas whose CE literals are asserted false  
+      //set inactive the quantified formulas whose CE literals are asserted false
       }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
         Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
@@ -106,7 +106,7 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
       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 ) ){
+        if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
           process( q, e, ee );
         }
       }
@@ -127,13 +127,15 @@ bool InstStrategyCbqi::checkComplete() {
 
 void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
-    //take ownership of the quantified formula
-    d_quantEngine->setOwner( q, this );
+    if( !options::cbqiAll() && !options::cbqiSplx() ){
+      //take full ownership of the quantified formula
+      d_quantEngine->setOwner( q, this );
+    }
   }
 }
 
 void InstStrategyCbqi::registerQuantifier( Node q ) {
-  
+
 }
 
 void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 2785ad128..49f561234 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -30,16 +30,7 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL){
-
-}
-
-InstantiationEngine::~InstantiationEngine() {
-  delete d_i_ag;
-  delete d_isup;
-}
-
-void InstantiationEngine::finishInit(){
+QuantifiersModule( qe ){
   if( options::eMatching() ){
     //these are the instantiation strategies for E-matching
     //user-provided patterns
@@ -51,9 +42,18 @@ void InstantiationEngine::finishInit(){
     //auto-generated patterns
     d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine );
     d_instStrategies.push_back( d_i_ag );
+  }else{
+    d_isup = NULL;
+    d_i_ag = NULL;
   }
 }
 
+InstantiationEngine::~InstantiationEngine() {
+  delete d_i_ag;
+  delete d_isup;
+}
+
+
 void InstantiationEngine::presolve() {
   for( unsigned i=0; i<d_instStrategies.size(); ++i ){
     d_instStrategies[i]->presolve();
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index bc1199588..4a990ff6b 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -74,8 +74,6 @@ private:
 public:
   InstantiationEngine( QuantifiersEngine* qe );
   ~InstantiationEngine();
-  /** initialize */
-  void finishInit();
   void presolve();
   bool needsCheck( Theory::Effort e );
   void reset_round( Theory::Effort e );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index a60f5af78..2578d0b7f 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -31,8 +31,10 @@ option dtVarExpandQuant --dt-var-exp-quant bool :default true
 #ite lift mode for quantified formulas
 option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h"
  ite lifting mode for quantified formulas
-option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
- split variables occurring as conditions of ITE in quantifiers
+option condVarSplitQuant --cond-var-split-quant bool :default true
+ split quantified formulas that lead to variable eliminations
+option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false
+ aggressive split quantified formulas that lead to variable eliminations
 option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false
  split ites with dt testers as conditions
 # Whether to CNF quantifier bodies
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index a1af1313d..26b598413 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -624,7 +624,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
   }
 
   if( !d_unassigned.empty() && ( success || doContinue ) ){
-    Trace("qcf-check") << "Assign to unassigned..." << std::endl;
+    Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size() << ")..." << std::endl;
     do {
       if( doFail ){
         Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
@@ -702,6 +702,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
         }
       }
     }while( success && isMatchSpurious( p ) );
+    Trace("qcf-check") << "done assigning." << std::endl;
   }
   if( success ){
     for( unsigned i=0; i<d_unassigned.size(); i++ ){
@@ -2113,7 +2114,9 @@ void QuantConflictFind::computeRelevantEqr() {
             itt->second.push_back( r );
           }
         }else{
-          d_eqcs[rtn].push_back( r );
+          if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
+            d_eqcs[rtn].push_back( r );
+          }
         }
       }
       ++eqcs_i;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index e911b0dc4..895408269 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -648,62 +648,111 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, bool hasPol, bool pol,
   }
 }
 
-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;
+
+bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){
+  if( n.getKind()==NOT ){
+    return isConditionalVariableElim( n[0], -pol );
+  }else if( ( n.getKind()==AND && pol>=0 ) || ( n.getKind()==OR && pol<=0 ) ){
+    pol = n.getKind()==AND ? 1 : -1;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( isConditionalVariableElim( n[i], pol ) ){
+        return true;
+      }
+    }
+  }else if( n.getKind()==EQUAL ){
+    for( unsigned i=0; i<2; i++ ){
+      if( n[i].getKind()==BOUND_VARIABLE ){
+        if( !TermDb::containsTerm( n[1-i], n[i] ) ){
+          return true;
         }
-        return NodeManager::currentNM()->mkNode( AND, conj );
       }
     }
-    if( options::iteCondVarSplitQuant() ){
-      Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+  }else if( n.getKind()==BOUND_VARIABLE ){
+    return true;
+  }
+  return false;
+}
+
+Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){
+  if( options::iteDtTesterSplitQuant() && body.getKind()==ITE ){
+    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 );
+    }
+  }
+  if( options::condVarSplitQuant() ){
+    if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() && !TermDb::isFunDefAnnotation( ipl ) ) ){
+      Trace("quantifiers-rewrite-debug") << "Conditional var elim 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 );
-        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( !TermDb::containsTerm( it->first[j], it->first[i] ) ){
-                    do_split = true;
-                    break;
-                  }
-                }
+      unsigned index_max = body.getKind()==ITE ? 0 : 1;
+      for( unsigned index=0; index<=index_max; index++ ){
+        if( isConditionalVariableElim( body[index] ) ){
+          do_split = true;
+          break;
+        }
+      }
+      if( do_split ){
+        Node pos;
+        Node neg;
+        if( body.getKind()==ITE ){
+          pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+          neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
+        }else{
+          pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+          neg = NodeManager::currentNM()->mkNode( OR, body[0], body[1].negate() );
+        }
+        Trace("quantifiers-rewrite-debug") << "*** Split (conditional variable eq) " << body << " into : " << std::endl;
+        Trace("quantifiers-rewrite-debug") << "   " << pos << std::endl;
+        Trace("quantifiers-rewrite-debug") << "   " << neg << std::endl;
+        return NodeManager::currentNM()->mkNode( AND, pos, neg );
+      }
+    }else if( body.getKind()==OR && options::condVarSplitQuantAgg() ){
+      std::vector< Node > bchildren;
+      std::vector< Node > nchildren;
+      for( unsigned i=0; i<body.getNumChildren(); i++ ){
+        bool split = false;
+        if( nchildren.empty() ){
+          if( body[i].getKind()==AND ){
+            std::vector< Node > children;
+            for( unsigned j=0; j<body[i].getNumChildren(); j++ ){
+              if( ( body[i][j].getKind()==NOT && body[i][j][0].getKind()==EQUAL && isConditionalVariableElim( body[i][j][0] ) ) ||
+                  body[i][j].getKind()==BOUND_VARIABLE ){
+                nchildren.push_back( body[i][j] );
+              }else{
+                children.push_back( body[i][j] );
               }
             }
-          }
-          if( do_split ){
-            break;
+            if( !nchildren.empty() ){
+              if( !children.empty() ){
+                nchildren.push_back( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ) );
+              }
+              split = true;
+            }
           }
         }
-        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() );
-          //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( !split ){
+          bchildren.push_back( body[i] );
         }
       }
+      if( !nchildren.empty() ){
+        Trace("quantifiers-rewrite-debug") << "*** Split (conditional variable eq) " << body << " into : " << std::endl;
+        for( unsigned i=0; i<nchildren.size(); i++ ){
+          bchildren.push_back( nchildren[i] );
+          nchildren[i] = NodeManager::currentNM()->mkNode( OR, bchildren );
+          Trace("quantifiers-rewrite-debug") << "   " << nchildren[i] << std::endl;
+          bchildren.pop_back();
+        }
+        return NodeManager::currentNM()->mkNode( AND, nchildren );
+      }
     }
   }
   return body;
@@ -738,10 +787,9 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
           break;
         }
       }
-    }
-    else if( it->first.getKind()==APPLY_TESTER ){
+    }else if( it->first.getKind()==APPLY_TESTER ){
       if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){
-        Trace("dt-var-expand") << "Expand datatype variable based on : " << it->first << std::endl;
+        Trace("var-elim-dt") << "Expand datatype variable based on : " << it->first << std::endl;
         std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] );
         if( ita!=args.end() ){
           vars.push_back( it->first[0] );
@@ -760,11 +808,21 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
             newVars.push_back( v );
           }
           subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
-          Trace("dt-var-expand") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
+          Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
           args.erase( ita );
           args.insert( args.end(), newVars.begin(), newVars.end() );
         }
       }
+    }else if( it->first.getKind()==BOUND_VARIABLE ){
+      if( options::varElimQuant() ){
+        std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first );
+        if( ita!=args.end() ){
+          Trace("var-elim-bool") << "Variable eliminate : " << it->first << " in " << body << std::endl;
+          vars.push_back( it->first );
+          subs.push_back( NodeManager::currentNM()->mkConst( it->second ) );
+          args.erase( ita );
+        }
+      }
     }
   }
   if( !vars.empty() ){
@@ -1286,7 +1344,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
     return true;
     //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
   }else if( computeOption==COMPUTE_PROCESS_ITE ){
-    return options::iteDtTesterSplitQuant() || options::iteCondVarSplitQuant();
+    return options::iteDtTesterSplitQuant() || options::condVarSplitQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
@@ -1332,7 +1390,7 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
         n = NodeManager::currentNM()->mkNode( OR, new_conds );
       }
     }else if( computeOption==COMPUTE_PROCESS_ITE ){
-      n = computeProcessIte( n );
+      n = computeProcessIte( n, ipl );
     }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 98a83b7de..0ad79587a 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -39,6 +39,7 @@ private:
   static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
   static Node computeClause( Node n );
   static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
+  static bool isConditionalVariableElim( Node n, int pol=0 );
 private:
   static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
@@ -48,7 +49,7 @@ private:
   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 computeProcessIte( Node body, Node ipl );
   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 );
@@ -60,9 +61,9 @@ private:
     COMPUTE_AGGRESSIVE_MINISCOPING,
     COMPUTE_NNF,
     COMPUTE_PROCESS_TERMS,
-    COMPUTE_PROCESS_ITE,
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
+    COMPUTE_PROCESS_ITE,
     //COMPUTE_FLATTEN_ARGS_UF,
     //COMPUTE_CNF,
     COMPUTE_LAST
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index bfeacf044..e513666a4 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1599,9 +1599,23 @@ bool TermDb::isFunDef( Node q ) {
   return !getFunDefHead( q ).isNull();
 }
 
+bool TermDb::isFunDefAnnotation( Node ipl ) {
+  if( !ipl.isNull() ){
+    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+      if( ipl[i].getKind()==INST_ATTRIBUTE ){
+        if( ipl[i][0].getAttribute(FunDefAttribute()) ){
+          return true;
+        }
+      }
+    }
+  }
+  return false;
+}
+
 Node TermDb::getFunDefHead( Node q ) {
   //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF &&
   if( q.getKind()==FORALL && q.getNumChildren()==3 ){
+
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
       if( q[2][i].getKind()==INST_ATTRIBUTE ){
         if( q[2][i][0].getAttribute(FunDefAttribute()) ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 3e38897d1..bc8851195 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -147,13 +147,13 @@ public:
   /** constants */
   Node d_zero;
   Node d_one;
-  
+
   /** map from operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
   /** map from type nodes to terms of that type */
   std::map< TypeNode, std::vector< Node > > d_type_map;
-  
-  
+
+
   /** count number of non-redundant ground terms per operator */
   std::map< Node, int > d_op_nonred_count;
   /**mapping from UF terms to representatives of their arguments */
@@ -165,7 +165,7 @@ public:
   std::map< Node, bool > d_has_map;
   /** map from reps to a term in eqc in d_has_map */
   std::map< Node, Node > d_term_elig_eqc;
-  
+
 public:
   /** ground terms for operator */
   unsigned getNumGroundTerms( Node f );
@@ -204,7 +204,7 @@ public:
   Node getEligibleTermInEqc( TNode r );
   /** is inst closure */
   bool isInstClosure( Node r );
-  
+
 //for model basis
 private:
   //map from types to model basis terms
@@ -301,7 +301,7 @@ public:
   bool isClosedEnumerableType( TypeNode tn );
   // may complete
   bool mayComplete( TypeNode tn );
-  
+
 //for triggers
 private:
   /** helper function for compute var contains */
@@ -414,6 +414,8 @@ public: //general queries concerning quantified formulas wrt modules
   static Node getRewriteRule( Node q );
   /** is fun def */
   static bool isFunDef( Node q );
+  /** is fun def */
+  static bool isFunDefAnnotation( Node ipl );
   /** is sygus conjecture */
   static bool isSygusConjecture( Node q );
   /** is sygus conjecture */