More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established.

19 files changed, 1087 insertions, 981 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 18496b173..dd6db951d 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -190,7 +190,7 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe,
                 success = true;
               }
             }
-          }while( !success && index<32 );
+          }while( !qe->inConflict() && !success && index<32 );
           //mark if we are incomplete
           osuccess = osuccess && success;
         }
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index b17286dba..33856d226 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -33,8 +33,8 @@ using namespace std;
 
 namespace CVC4 {
 
-bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs ) {
-  return d_out->addInstantiation( subs );
+bool CegqiOutputSingleInv::doAddInstantiation( std::vector< Node >& subs ) {
+  return d_out->doAddInstantiation( subs );
 }
 
 bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) {
@@ -55,12 +55,12 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje
   }
   d_cosi = new CegqiOutputSingleInv( this );
   //  third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity
-  d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );   
+  d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
 
   d_sol = new CegConjectureSingleInvSol( qe );
 
   d_sip = new SingleInvocationPartition;
-  
+
   if( options::cegqiSingleInvPartial() ){
     d_ei = new CegEntailmentInfer( qe, d_sip );
   }else{
@@ -104,7 +104,7 @@ void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems
     if( d_cinst ){
       delete d_cinst;
     }
-    d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );   
+    d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
     d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
   }
 }
@@ -480,7 +480,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() {
   if( d_single_inv.isNull() ){
     if( d_ei->getEntailedConjecture( d_single_inv, d_single_inv_exp ) ){
       Trace("cegqi-nsi") << "NSI : got : " << d_single_inv << std::endl;
-      Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl; 
+      Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl;
     }else{
       Trace("cegqi-nsi") << "NSI : failed to construct next conjecture." << std::endl;
       Notice() << "Incomplete due to --cegqi-si-partial." << std::endl;
@@ -491,7 +491,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() {
     Trace("cegqi-nsi") << "NSI : have : " << d_single_inv << std::endl;
     Assert( d_single_inv_exp.isNull() );
   }
-  
+
   d_si_guard = Node::null();
   d_ns_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GS", NodeManager::currentNM()->booleanType() ) );
   d_ns_guard = d_qe->getValuation().ensureLiteral( d_ns_guard );
@@ -508,7 +508,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() {
   Trace("cegqi-nsi") << "NSI : conjecture is " << d_single_inv << std::endl;
 }
 
-bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){
+bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){
   std::stringstream siss;
   if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){
     siss << "  * single invocation: " << std::endl;
@@ -843,7 +843,7 @@ bool SingleInvocationPartition::init( Node n ) {
   std::vector< TypeNode > typs;
   std::map< Node, bool > visited;
   if( inferArgTypes( n, typs, visited ) ){
-    return init( typs, n );  
+    return init( typs, n );
   }else{
     Trace("si-prt") << "Could not infer argument types." << std::endl;
     return false;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 6d47b8d9a..4d2f9a0e5 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -37,7 +37,7 @@ public:
   CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
   ~CegqiOutputSingleInv() {}
   CegConjectureSingleInv * d_out;
-  bool addInstantiation( std::vector< Node >& subs );
+  bool doAddInstantiation( std::vector< Node >& subs );
   bool isEligibleForInstantiation( Node n );
   bool addLemma( Node lem );
 };
@@ -102,7 +102,7 @@ public:
 private:
   std::vector< Node > d_curr_lemmas;
   //add instantiation
-  bool addInstantiation( std::vector< Node >& subs );
+  bool doAddInstantiation( std::vector< Node >& subs );
   //is eligible for instantiation
   bool isEligibleForInstantiation( Node n );
   // add lemma
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 6a56977b8..da488ea98 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -65,9 +65,9 @@ void CegInstantiator::computeProgVars( Node n ){
   }
 }
 
-bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                                        std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
-                                        std::map< Node, Node >& cons, std::vector< Node >& curr_var ){
+bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                                          std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+                                          std::map< Node, Node >& cons, std::vector< Node >& curr_var ){
   if( i==d_vars.size() ){
     //solved for all variables, now construct instantiation
     if( !sf.d_has_coeff.empty() ){
@@ -75,12 +75,12 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
         //use symbolic solved forms
         SolvedForm csf;
         csf.copy( ssf );
-        return addInstantiationCoeff( csf, vars, btyp, 0, cons );
+        return doAddInstantiationCoeff( csf, vars, btyp, 0, cons );
       }else{
-        return addInstantiationCoeff( sf, vars, btyp, 0, cons );
+        return doAddInstantiationCoeff( sf, vars, btyp, 0, cons );
       }
     }else{
-      return addInstantiation( sf.d_subs, vars, cons );
+      return doAddInstantiation( sf.d_subs, vars, cons );
     }
   }else{
     std::map< Node, std::map< Node, bool > > subs_proc;
@@ -139,7 +139,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
               if( proc ){
                 //try the substitution
                 subs_proc[ns][pv_coeff] = true;
-                if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars,  btyp, theta, i, effort, cons, curr_var ) ){
+                if( doAddInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars,  btyp, theta, i, effort, cons, curr_var ) ){
                   return true;
                 }
               }
@@ -163,7 +163,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
               for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
                 curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) );
               }
-              if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+              if( doAddInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                 return true;
               }else{
                 //cleanup
@@ -270,7 +270,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                         Node val = veq[1];
                         if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
                           subs_proc[val][veq_c] = true;
-                          if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                          if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                             return true;
                           }
                         }
@@ -286,7 +286,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                   if( success ){
                     if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
                       subs_proc[val][veq_c] = true;
-                      if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                      if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                         return true;
                       }
                     }
@@ -455,7 +455,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                           //try this bound
                           if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
                             subs_proc[uval][veq_c] = true;
-                            if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                            if( doAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                               return true;
                             }
                           }
@@ -492,7 +492,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                   val = NodeManager::currentNM()->mkNode( UMINUS, val );
                   val = Rewriter::rewrite( val );
                 }
-                if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                   return true;
                 }
               }
@@ -588,7 +588,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                   if( !val.isNull() ){
                     if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
                       subs_proc[val][mbp_coeff[rr][best]] = true;
-                      if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                      if( doAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                         return true;
                       }
                     }
@@ -605,7 +605,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
             if( !val.isNull() ){
               if( subs_proc[val].find( c )==subs_proc[val].end() ){
                 subs_proc[val][c] = true;
-                if( addInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                if( doAddInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                   return true;
                 }
               }
@@ -649,7 +649,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
             if( !val.isNull() ){
               if( subs_proc[val].find( Node::null() )==subs_proc[val].end() ){
                 subs_proc[val][Node::null()] = true;
-                if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                   return true;
                 }
               }
@@ -670,7 +670,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                   if( !val.isNull() ){
                     if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
                       subs_proc[val][mbp_coeff[rr][j]] = true;
-                      if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                      if( doAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                         return true;
                       }
                     }
@@ -694,7 +694,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
       //we only resort to values in the case of booleans
       Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() );
 #endif
-      if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
+      if( doAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
         return true;
       }
     }
@@ -704,9 +704,9 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
 }
 
 
-bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                                           std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
-                                           std::map< Node, Node >& cons, std::vector< Node >& curr_var ) {
+bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                                             std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+                                             std::map< Node, Node >& cons, std::vector< Node >& curr_var ) {
   if( Trace.isOn("cbqi-inst") ){
     for( unsigned j=0; j<sf.d_subs.size(); j++ ){
       Trace("cbqi-inst") << " ";
@@ -800,7 +800,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
       curr_var.pop_back();
       is_cv = true;
     }
-    success = addInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
+    success = doAddInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
     if( !success ){
       if( is_cv ){
         curr_var.push_back( pv );
@@ -831,12 +831,12 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
   }
 }
 
-bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp,
+bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp,
                                              unsigned j, std::map< Node, Node >& cons ) {
 
 
   if( j==sf.d_has_coeff.size() ){
-    return addInstantiation( sf.d_subs, vars, cons );
+    return doAddInstantiation( sf.d_subs, vars, cons );
   }else{
     Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() );
     unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin();
@@ -894,7 +894,7 @@ bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >
             }
           }
         }
-        if( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
+        if( doAddInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
           return true;
         }
       }
@@ -905,7 +905,7 @@ bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >
   }
 }
 
-bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) {
+bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) {
   if( vars.size()>d_vars.size() ){
     Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
     std::map< Node, Node > subs_map;
@@ -927,7 +927,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       subs.push_back( subs_orig[d_var_order_index[i]] );
     }
   }
-  bool ret = d_out->addInstantiation( subs );
+  bool ret = d_out->doAddInstantiation( subs );
 #ifdef MBP_STRICT_ASSERTIONS
   Assert( ret );
 #endif
@@ -1127,7 +1127,7 @@ bool CegInstantiator::check() {
     std::map< Node, Node > cons;
     std::vector< Node > curr_var;
     //try to add an instantiation
-    if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
+    if( doAddInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
       return true;
     }
   }
@@ -1499,7 +1499,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   }
 }
 
-//this isolates the atom into solved form 
+//this isolates the atom into solved form
 //     veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf
 //  ensures val is Int if pv is Int, and val does not contain vts symbols
 int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 36c6f1bce..3d7bbcb55 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -33,7 +33,7 @@ namespace quantifiers {
 class CegqiOutput {
 public:
   virtual ~CegqiOutput() {}
-  virtual bool addInstantiation( std::vector< Node >& subs ) = 0;
+  virtual bool doAddInstantiation( std::vector< Node >& subs ) = 0;
   virtual bool isEligibleForInstantiation( Node n ) = 0;
   virtual bool addLemma( Node lem ) = 0;
 };
@@ -108,16 +108,16 @@ private:
   };
   */
   // effort=0 : do not use model value, 1: use model value, 2: one must use model value
-  bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+  bool doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
                          std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
                          std::map< Node, Node >& cons, std::vector< Node >& curr_var );
-  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+  bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
                             std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
                             std::map< Node, Node >& cons, std::vector< Node >& curr_var );
-  bool addInstantiationCoeff( SolvedForm& sf,
+  bool doAddInstantiationCoeff( SolvedForm& sf,
                               std::vector< Node >& vars, std::vector< int >& btyp,
                               unsigned j, std::map< Node, Node >& cons );
-  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons );
+  bool doAddInstantiation( 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( 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 );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index d06e9f7f7..0276cf7ab 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -591,6 +591,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
 
 bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
+  Assert( !d_qe->inConflict() );
   if( optUseModel() ){
     FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();
     if (effort==0) {
@@ -684,7 +685,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
                 if( d_qe->addInstantiation( f, inst ) ){
                   Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
                   d_addedLemmas++;
-                  if( options::fmfOneInstPerRound() ){
+                  if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
                     break;
                   }
                 }else{
@@ -812,7 +813,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
         if( d_qe->addInstantiation( f, inst ) ){
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
-          if( options::fmfOneInstPerRound() ){
+          if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
             break;
           }
         }else{
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 1751f3a87..55a4e8f8c 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -155,20 +155,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
         return ret;
       }
     }
-    /*
-    //check if m is an instance of another instantiation if modInst is true
-    if( modInst ){
-      if( !n.isNull() ){
-        Node nl;
-        std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
-        if( itm!=d_data.end() ){
-          if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
-            return false;
-          }
-        }
-      }
-    }
-    */
     if( modEq ){
       //check modulo equality if any other instantiation match exists
       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
@@ -195,6 +181,24 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
   }
 }
 
+bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, ImtIndexOrder* imtio, int index ) {
+  Assert( index<(int)q[0].getNumChildren() );
+  Assert( !imtio || index<(int)imtio->d_order.size() );
+  int i_index = imtio ? imtio->d_order[index] : index;
+  Node n = m[i_index];
+  std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
+  if( it!=d_data.end() ){
+    if( (index+1)==(int)q[0].getNumChildren() || ( imtio && (index+1)==(int)imtio->d_order.size() ) ){
+      d_data.erase( n );
+      return true;
+    }else{
+      return it->second.removeInstMatch( qe, q, m, imtio, index+1 );
+    }
+  }else{
+    return false;
+  }
+}
+
 void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const {
   if( terms.size()==q[0].getNumChildren() ){
     out << "  ( ";
@@ -257,20 +261,6 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
         return reset || ret;
       }
     }
-    //check if m is an instance of another instantiation if modInst is true
-    /*
-    if( modInst ){
-      if( !n.isNull() ){
-        Node nl;
-        std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl );
-        if( itm!=d_data.end() ){
-          if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
-            return false;
-          }
-        }
-      }
-    }
-    */
     if( modEq ){
       //check modulo equality if any other instantiation match exists
       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
@@ -302,6 +292,25 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
   }
 }
 
+bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index ) {
+  if( index==(int)q[0].getNumChildren() ){
+    if( d_valid.get() ){
+      d_valid.set( false );
+      return true;
+    }else{
+      return false;
+    }
+  }else{
+    Node n = m[index];
+    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    if( it!=d_data.end() ){
+      return it->second->removeInstMatch( qe, q, m, index+1 );
+    }else{
+      return false;
+    }
+  }
+}
+
 void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{
   if( d_valid.get() ){
     if( terms.size()==q[0].getNumChildren() ){
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index fbdef61c2..a87d2704e 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -128,6 +128,7 @@ public:
   }
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
+  bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
   void print( std::ostream& out, Node q ) const{
     std::vector< TNode > terms;
     print( out, q, terms );
@@ -157,24 +158,25 @@ public:
         modEq is if we check modulo equality
         modInst is if we return true if m is an instance of a match that exists
    */
-  bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
+  bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
                         bool modInst = false, int index = 0 ) {
-    return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
+    return !addInstMatch( qe, q, m, c, modEq, modInst, index, true );
   }
-  bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
+  bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
                         bool modInst = false, int index = 0 ) {
-    return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
+    return !addInstMatch( qe, q, m, c, modEq, modInst, index, true );
   }
   /** add match m for quantifier f, take into account equalities if modEq = true,
       if imtio is non-null, this is the order to add to trie
       return true if successful
   */
-  bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
+  bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
                      bool modInst = false, int index = 0, bool onlyExist = false ) {
-    return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist );
+    return addInstMatch( qe, q, m.d_vals, c, modEq, modInst, index, onlyExist );
   }
-  bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
+  bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
                      bool modInst = false, int index = 0, bool onlyExist = false );
+  bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
   void print( std::ostream& out, Node q ) const{
     std::vector< TNode > terms;
     print( out, q, terms );
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index cfa4190e4..29754d3e6 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -126,7 +126,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){
         ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
         d_eq_class_rel = Node::null();
-      } 
+      }
     }else if( d_match_pattern.getKind()==INST_CONSTANT ){
       if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
         Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr();
@@ -139,7 +139,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       }else{
         d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
       }
-    }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) && 
+    }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) &&
               d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){
       //we will be producing candidates via literal matching heuristics
       if( d_pattern.getKind()!=NOT ){
@@ -307,6 +307,9 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
 }
 
 bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
+  if( qe->inConflict() ){
+    return false;
+  }
   if( d_needsReset ){
     Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
     reset( d_eq_class, qe );
@@ -767,15 +770,20 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
             m.setValue( v, t);
             addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
             m.setValue( v, prev);
+            if( qe->inConflict() ){
+              break;
+            }
           }
         }
         return;
       }
     }
-    Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
-    std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
-    if( it!=tat->d_data.end() ){
-      addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+    if( !qe->inConflict() ){
+      Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
+      std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
+      if( it!=tat->d_data.end() ){
+        addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+      }
     }
   }
 }
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index d20f3fd4a..863914567 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -1,674 +1,728 @@
-/*********************                                                        */

-/*! \file inst_propagator.cpp

- ** \verbatim

- ** Top contributors (to current version):

- **   Andrew Reynolds

- ** This file is part of the CVC4 project.

- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS

- ** in the top-level source directory) and their institutional affiliations.

- ** All rights reserved.  See the file COPYING in the top-level source

- ** directory for licensing information.\endverbatim

- **

- ** Propagate mechanism for instantiations

- **/

-

-#include <vector>

-

-#include "theory/quantifiers/inst_propagator.h"

-#include "theory/rewriter.h"

-#include "theory/quantifiers/term_database.h"

-

-using namespace CVC4;

-using namespace std;

-using namespace CVC4::theory;

-using namespace CVC4::theory::quantifiers;

-using namespace CVC4::kind;

-

-

-EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){

-  d_true = NodeManager::currentNM()->mkConst( true );

-  d_false = NodeManager::currentNM()->mkConst( false );

-}

-

-bool EqualityQueryInstProp::reset( Theory::Effort e ) {

-  d_uf.clear();

-  d_uf_exp.clear();

-  d_diseq_list.clear();

-  return true;

-}

-

-/** contains term */

-bool EqualityQueryInstProp::hasTerm( Node a ) {

-  if( getEngine()->hasTerm( a ) ){

-    return true;

-  }else{

-    std::vector< Node > exp;

-    Node ar = getUfRepresentative( a, exp );

-    return !ar.isNull() && getEngine()->hasTerm( ar );

-  }

-}

-

-/** get the representative of the equivalence class of a */

-Node EqualityQueryInstProp::getRepresentative( Node a ) {

-  if( getEngine()->hasTerm( a ) ){

-    a = getEngine()->getRepresentative( a );

-  }

-  std::vector< Node > exp;

-  Node ar = getUfRepresentative( a, exp );

-  return ar.isNull() ? a : ar;

-}

-

-/** returns true if a and b are equal in the current context */

-bool EqualityQueryInstProp::areEqual( Node a, Node b ) {

-  if( a==b ){

-    return true;

-  }else{

-    eq::EqualityEngine* ee = getEngine();

-    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){

-      if( ee->areEqual( a, b ) ){

-        return true;

-      }

-    }

-    return false;

-  }

-}

-

-/** returns true is a and b are disequal in the current context */

-bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {

-  if( a==b ){

-    return true;

-  }else{

-    eq::EqualityEngine* ee = getEngine();

-    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){

-      if( ee->areDisequal( a, b, false ) ){

-        return true;

-      }

-    }

-    return false;

-  }

-}

-

-/** get the equality engine associated with this query */

-eq::EqualityEngine* EqualityQueryInstProp::getEngine() {

-  return d_qe->getMasterEqualityEngine();

-}

-

-/** get the equivalence class of a */

-void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {

-  //TODO?

-}

-

-TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {

-  TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );

-  if( !t.isNull() ){

-    return t;

-  }else{

-    //TODO?

-    return TNode::null();

-  }

-}

-

-Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {

-  bool engine_has_a = getEngine()->hasTerm( a );

-  if( engine_has_a ){

-    a = getEngine()->getRepresentative( a );

-  }

-  //get union find representative, if this occurs in the equality engine, return it

-  unsigned prev_size = exp.size();

-  Node ar = getUfRepresentative( a, exp );

-  if( !ar.isNull() ){

-    if( engine_has_a || getEngine()->hasTerm( ar ) ){

-      Assert( getEngine()->hasTerm( ar ) );

-      Assert( getEngine()->getRepresentative( ar )==ar );

-      return ar;

-    }

-  }else{

-    if( engine_has_a ){

-      return a;

-    }

-  }

-  //retract explanation

-  while( exp.size()>prev_size ){

-    exp.pop_back();

-  }

-  return Node::null();

-}

-

-bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {

-  if( areEqual( a, b ) ){

-    return true;

-  }else{

-    std::vector< Node > exp_a;

-    Node ar = getUfRepresentative( a, exp_a );

-    if( !ar.isNull() ){

-      std::vector< Node > exp_b;

-      if( ar==getUfRepresentative( b, exp_b ) ){

-        merge_exp( exp, exp_a );

-        merge_exp( exp, exp_b );

-        return true;

-      }

-    }

-    return false;

-  }

-}

-

-bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {

-  if( areDisequal( a, b ) ){

-    return true;

-  }else{

-    //TODO?

-    return false;

-  }

-}

-

-Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {

-  Assert( exp.empty() );

-  std::map< Node, Node >::iterator it = d_uf.find( a );

-  if( it!=d_uf.end() ){

-    if( it->second==a ){

-      Assert( d_uf_exp[ a ].empty() );

-      return it->second;

-    }else{

-      Node m = getUfRepresentative( it->second, exp );

-      Assert( !m.isNull() );

-      if( m!=it->second ){

-        //update union find

-        d_uf[ a ] = m;

-        //update explanation : merge the explanation of the parent

-        merge_exp( d_uf_exp[ a ], exp );

-        Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;

-      }

-      //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset

-      exp.clear();

-      exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );

-      return m;

-    }

-  }else{

-    return Node::null();

-  }

-}

-

-// set a == b with reason, return status, modify a and b to representatives pre-merge

-int EqualityQueryInstProp::setEqual( Node& a, Node& b, std::vector< Node >& reason ) {

-  int status = STATUS_MERGED_UNKNOWN;

-  Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", reason size = " << reason.size() << std::endl;

-  //get the representative for a

-  std::vector< Node > exp_a;

-  Node ar = getUfRepresentative( a, exp_a );

-  if( ar.isNull() ){

-    Assert( exp_a.empty() );

-    ar = a;

-  }

-  if( ar==b ){

-    Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;

-    return STATUS_NONE;

-  }

-  bool swap = false;

-  //get the representative for b

-  std::vector< Node > exp_b;

-  Node br = getUfRepresentative( b, exp_b );

-  if( br.isNull() ){

-    Assert( exp_b.empty() );

-    br = b;

-    if( !getEngine()->hasTerm( br ) ){

-      if( ar!=a ){

-        swap = true;

-      }

-    }else{

-      if( getEngine()->hasTerm( ar ) ){

-        status = STATUS_MERGED_KNOWN;

-      }

-    }

-  }else{

-    if( ar==br ){

-      Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;

-      return STATUS_NONE;

-    }else if( getEngine()->hasTerm( ar ) ){

-      if( getEngine()->hasTerm( br ) ){

-        status = STATUS_MERGED_KNOWN;

-      }else{

-        swap = true;

-      }

-    }

-  }

-  if( swap ){

-    //swap

-    Node temp_r = ar;

-    ar = br;

-    br = temp_r;

-  }

-

-  Assert( ar!=br );

-  Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );

-

-  //update the union find

-  Assert( d_uf_exp[ar].empty() );

-  Assert( d_uf_exp[br].empty() );

-

-  d_uf[ar] = br;

-  merge_exp( d_uf_exp[ar], exp_a );

-  merge_exp( d_uf_exp[ar], exp_b );

-  merge_exp( d_uf_exp[ar], reason );

-

-  d_uf[br] = br;

-  d_uf_exp[br].clear();

-

-  Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;

-  a = ar;

-  b = br;

-  return status;

-}

-

-

-void EqualityQueryInstProp::addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol ) {

-  if( is_prop ){

-    if( isLiteral( n ) ){

-      props.push_back( pol ? n : n.negate() );

-      return;

-    }

-  }

-  args.push_back( n );

-}

-

-bool EqualityQueryInstProp::isLiteral( Node n ) {

-  Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();

-  Assert( ak!=NOT );

-  return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;

-}

-

-//this is identical to TermDb::evaluateTerm2, but tracks more information

-Node EqualityQueryInstProp::evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,

-                                             std::map< Node, bool >& watch_list_out, std::vector< TNode >& props ) {

-  std::map< TNode, Node >::iterator itv = visited.find( n );

-  if( itv != visited.end() ){

-    return itv->second;

-  }else{

-    Trace("term-db-eval") << "evaluate term : " << n << std::endl;

-    std::vector< Node > exp_n;

-    Node ret = getRepresentativeExp( n, exp_n );

-    if( ret.isNull() ){

-      //term is not known to be equal to a representative in equality engine, evaluate it

-      Kind k = n.getKind();

-      if( k==FORALL ){

-        ret = Node::null();

-      }else{

-        std::map< Node, bool > watch_list_out_curr;

-        TNode f = d_qe->getTermDatabase()->getMatchOperator( n );

-        std::vector< TNode > args;

-        bool ret_set = false;

-        bool childChanged = false;

-        int abort_i = -1;

-        //get the child entailed polarity

-        Assert( n.getKind()!=IMPLIES );

-        bool newHasPol, newPol;

-        QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );

-        //for each child

-        for( unsigned i=0; i<n.getNumChildren(); i++ ){

-          TNode c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props );

-          if( c.isNull() ){

-            ret = Node::null();

-            ret_set = true;

-            break;

-          }else if( c==d_true || c==d_false ){

-            //short-circuiting

-            if( k==kind::AND || k==kind::OR ){

-              if( (k==kind::AND)==(c==d_false) ){

-                ret = c;

-                ret_set = true;

-                break;

-              }else{

-                //redundant

-                c = Node::null();

-                childChanged = true;

-              }

-            }else if( k==kind::ITE && i==0 ){

-              Assert( watch_list_out_curr.empty() );

-              ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props );

-              ret_set = true;

-              break;

-            }else if( k==kind::NOT ){

-              ret = c==d_true ? d_false : d_true;

-              ret_set = true;

-              break;

-            }

-          }

-          if( !c.isNull() ){

-            childChanged = childChanged || n[i]!=c;

-            if( !f.isNull() && !watch_list_out_curr.empty() ){

-              // we are done if this is an UF application and an argument is unevaluated

-              args.push_back( c );

-              abort_i = i;

-              break;

-            }else if( ( k==kind::AND || k==kind::OR ) ){

-              if( c.getKind()==k ){

-                //flatten

-                for( unsigned j=0; j<c.getNumChildren(); j++ ){

-                  addArgument( args, props, c[j], newHasPol, newPol );

-                }

-              }else{

-                addArgument( args, props, c, newHasPol, newPol );

-              }

-              //if we are in a branching position

-              if( hasPol && !newHasPol && args.size()>=2 ){

-                //we are done if at least two args are unevaluated

-                abort_i = i;

-                break;

-              }

-            }else if( k==kind::ITE ){

-              //we are done if we are ITE and condition is unevaluated

-              Assert( i==0 );

-              args.push_back( c );

-              abort_i = i;

-              break;

-            }else{

-              args.push_back( c );

-            }

-          }

-        }

-        //add remaining children if we aborted

-        if( abort_i!=-1 ){

-          for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){

-            args.push_back( n[i] );

-          }

-        }

-        //copy over the watch list

-        for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){

-          watch_list_out[itc->first] = itc->second;

-        }

-

-        //if we have not short-circuited evaluation

-        if( !ret_set ){

-          //if it is an indexed term, return the congruent term

-          if( !f.isNull() && watch_list_out.empty() ){

-            Assert( args.size()==n.getNumChildren() );

-            //args contains terms known by the equality engine

-            TNode nn = getCongruentTerm( f, args );

-            Trace("term-db-eval") << "  got congruent term " << nn << " from DB for " << n << std::endl;

-            if( !nn.isNull() ){

-              //successfully constructed representative in EE

-              Assert( exp_n.empty() );

-              ret = getRepresentativeExp( nn, exp_n );

-              Trace("term-db-eval") << "return rep, exp size = " << exp_n.size() << std::endl;

-              merge_exp( exp, exp_n );

-              ret_set = true;

-              Assert( !ret.isNull() );

-            }

-          }

-          if( !ret_set ){

-            if( childChanged ){

-              Trace("term-db-eval") << "return rewrite" << std::endl;

-              if( ( k==kind::AND || k==kind::OR ) ){

-                if( args.empty() ){

-                  ret = k==kind::AND ? d_true : d_false;

-                  ret_set = true;

-                }else if( args.size()==1 ){

-                  ret = args[0];

-                  ret_set = true;

-                }

-              }

-              if( !ret_set ){

-                Assert( args.size()==n.getNumChildren() );

-                if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){

-                  args.insert( args.begin(), n.getOperator() );

-                }

-                ret = NodeManager::currentNM()->mkNode( k, args );

-                ret = Rewriter::rewrite( ret );

-                watch_list_out[ret] = true;

-              }

-            }else{

-              ret = n;

-              watch_list_out[ret] = true;

-            }

-          }

-        }

-      }

-    }else{

-      Trace("term-db-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;

-      merge_exp( exp, exp_n );

-    }

-    Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl;

-    visited[n] = ret;

-    return ret;

-  }

-}

-

-void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {

-  //TODO : optimize

-  if( v.empty() ){

-    Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() );

-    v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );

-  }else{

-    //std::vector< Node >::iterator v_end = v.end();

-    up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;

-    for( int j=0; j<up_to_size; j++ ){

-      if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){

-        v.push_back( v_to_merge[j] );

-      }

-    }

-  }

-}

-

-

-void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {

-  d_active = true;

-  //information about the instance

-  d_q = q;

-  d_lem = lem;

-  Assert( d_terms.empty() );

-  d_terms.insert( d_terms.end(), terms.begin(), terms.end() );

-  //the current lemma

-  d_curr = body;

-  d_curr_exp.push_back( body );

-}

-

-InstPropagator::InstPropagator( QuantifiersEngine* qe ) :

-d_qe( qe ), d_notify(*this), d_qy( qe ){

-}

-

-bool InstPropagator::reset( Theory::Effort e ) {

-  d_icount = 0;

-  d_ii.clear();

-  for( unsigned i=0; i<2; i++ ){

-    d_conc_to_id[i].clear();

-  }

-  d_conflict = false;

-  d_watch_list.clear();

-  d_relevant_inst.clear();

-  return d_qy.reset( e );

-}

-

-void InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {

-  if( !d_conflict ){

-    if( Trace.isOn("qip-prop") ){

-      Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;

-      for( unsigned i=0; i<terms.size(); i++ ){

-        Trace("qip-prop") << "  " << terms[i] << std::endl;

-      }

-    }

-    unsigned id = d_icount;

-    d_icount++;

-    Trace("qip-prop") << "...assign id=" << id << std::endl;

-    d_ii[id].init( q, lem, terms, body );

-    //initialize the information

-    if( cacheConclusion( id, body ) ){

-      Assert( d_update_list.empty() );

-      d_update_list.push_back( id );

-      bool firstTime = true;

-      //update infos in the update list until empty 

-      do {

-        unsigned uid = d_update_list.back();

-        d_update_list.pop_back();

-        if( d_ii[uid].d_active ){

-          update( uid, d_ii[uid], firstTime );

-        }

-        firstTime = false;

-      }while( !d_update_list.empty() );

-    }else{

-      d_ii[id].d_active = false;

-      Trace("qip-prop") << "...duplicate." << std::endl;

-    }

-  }

-}

-

-bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {

-  Assert( !d_conflict );

-  Assert( ii.d_active );

-  Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;

-  //update the evaluation of the current lemma

-  std::map< TNode, Node > visited;

-  std::map< Node, bool > watch_list;

-  std::vector< TNode > props;

-  Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props );

-  if( eval.isNull() ){

-    ii.d_active = false;

-  }else if( firstTime || eval!=ii.d_curr ){

-    if( EqualityQueryInstProp::isLiteral( eval ) ){

-      props.push_back( eval );

-      eval = d_qy.d_true;

-      watch_list.clear();

-    }

-    if( Trace.isOn("qip-prop") ){

-      Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;

-      Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = ";

-      debugPrintExplanation( ii.d_curr_exp, "qip-prop" );

-      Trace("qip-prop") << std::endl;

-      Trace("qip-prop") << "...watch list: " << std::endl;

-      for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){

-        Trace("qip-prop") << "  " << itw->first << std::endl;

-      }

-      Trace("qip-prop") << "...new propagations: " << std::endl;

-      for( unsigned i=0; i<props.size(); i++ ){

-        Trace("qip-prop") << "  " << props[i] << std::endl;

-      }

-      Trace("qip-prop") << std::endl;

-    }

-    //determine the status of eval

-    if( eval==d_qy.d_false ){

-      Assert( props.empty() );

-      //we have inferred a conflict

-      conflict( ii.d_curr_exp );

-      return false;

-    }else{

-      for( unsigned i=0; i<props.size(); i++ ){

-        //if we haven't propagated this literal yet

-        if( cacheConclusion( id, props[i], 1 ) ){

-          Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];

-          bool pol = props[i].getKind()!=NOT;

-          if( lit.getKind()==EQUAL ){

-            propagate( lit[0], lit[1], pol, ii.d_curr_exp );

-          }else{

-            propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );

-          }

-          if( d_conflict ){

-            return false;

-          }

-        }

-      }

-      //if we have not inferred this conclusion yet

-      if( cacheConclusion( id, eval ) ){

-        ii.d_curr = eval;

-        //update the watch list

-        Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;

-        //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations.

-        //  Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms.

-        for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){

-          d_watch_list[ itw->first ][ id ] = true;

-        }

-      }else{

-        Trace("qip-prop-debug") << "...conclusion is duplicate." << std::endl;

-        ii.d_active = false;

-      }

-    }

-  }else{

-    Trace("qip-prop-debug") << "...did not update." << std::endl;

-  }

-  Assert( !d_conflict );

-  return true;

-}

-

-void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {

-  if( Trace.isOn("qip-propagate") ){

-    Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";

-    debugPrintExplanation( exp, "qip-propagate" );

-    Trace("qip-propagate") << "..." << std::endl;

-  }

-  if( pol ){

-    std::vector< Node > exp_d;

-    if( d_qy.areDisequalExp( a, b, exp_d ) ){

-      Trace("qip-prop-debug") << "...conflict." << std::endl;

-      EqualityQueryInstProp::merge_exp( exp, exp_d );

-      conflict( exp );

-    }else{

-      //set equal

-      int status = d_qy.setEqual( a, b, exp );

-      if( status==EqualityQueryInstProp::STATUS_NONE ){

-        Trace("qip-prop-debug") << "...already equal." << std::endl;

-        return;

-      }else if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){

-        Assert( d_qy.getEngine()->hasTerm( a ) );

-        Assert( d_qy.getEngine()->hasTerm( b ) );

-        Trace("qip-prop-debug") << "...equality between known terms." << std::endl;

-        addRelevantInstances( exp, "qip-propagate" );

-      }

-      Trace("qip-prop-debug") << "...merging " << a << " and " << b << std::endl;

-      for( unsigned i=0; i<2; i++ ){

-        //update terms from watched lists

-        Node c = i==0 ? a : b;

-        std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );

-        if( it!=d_watch_list.end() ){

-          Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;

-          for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){

-            unsigned idw = itw->first;

-            if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){

-              Trace("qip-prop-debug") << "...will update " << idw << std::endl;

-              d_update_list.push_back( idw );

-            }

-          }

-          d_watch_list.erase( c );

-        }

-      }

-    }

-  }else{

-    std::vector< Node > exp_e;

-    if( d_qy.areEqualExp( a, b, exp_e ) ){

-      EqualityQueryInstProp::merge_exp( exp, exp_e );

-      conflict( exp );

-    }else{

-      //TODO?

-    }

-  }

-}

-

-void InstPropagator::conflict( std::vector< Node >& exp ) {

-  Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;

-  d_conflict = true;

-  d_relevant_inst.clear();

-  addRelevantInstances( exp, "qip-propagate" );

-}

-

-bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {

-  Assert( prop_index==0 || prop_index==1 );

-  //check if the conclusion is non-redundant

-  if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){

-    d_conc_to_id[prop_index][body] = id;

-    return true;

-  }else{

-    return false;

-  }

-}

-

-void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {

-  for( unsigned i=0; i<exp.size(); i++ ){

-    Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );

-    Trace(c) << "  relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;

-    d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;

-  }

-}

-

-void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {

-  for( unsigned i=0; i<exp.size(); i++ ){

-    Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );

-    Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";

-  }

-}

-

+/*********************                                                        */
+/*! \file inst_propagator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** Propagate mechanism for instantiations
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/inst_propagator.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+
+EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){
+  d_true = NodeManager::currentNM()->mkConst( true );
+  d_false = NodeManager::currentNM()->mkConst( false );
+}
+
+bool EqualityQueryInstProp::reset( Theory::Effort e ) {
+  d_uf.clear();
+  d_uf_exp.clear();
+  d_diseq_list.clear();
+  return true;
+}
+
+/** contains term */
+bool EqualityQueryInstProp::hasTerm( Node a ) {
+  if( getEngine()->hasTerm( a ) ){
+    return true;
+  }else{
+    std::vector< Node > exp;
+    Node ar = getUfRepresentative( a, exp );
+    return !ar.isNull() && getEngine()->hasTerm( ar );
+  }
+}
+
+/** get the representative of the equivalence class of a */
+Node EqualityQueryInstProp::getRepresentative( Node a ) {
+  if( getEngine()->hasTerm( a ) ){
+    a = getEngine()->getRepresentative( a );
+  }
+  std::vector< Node > exp;
+  Node ar = getUfRepresentative( a, exp );
+  return ar.isNull() ? a : ar;
+}
+
+/** returns true if a and b are equal in the current context */
+bool EqualityQueryInstProp::areEqual( Node a, Node b ) {
+  if( a==b ){
+    return true;
+  }else{
+    eq::EqualityEngine* ee = getEngine();
+    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+      if( ee->areEqual( a, b ) ){
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
+/** returns true is a and b are disequal in the current context */
+bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {
+  if( a==b ){
+    return false;
+  }else{
+    eq::EqualityEngine* ee = getEngine();
+    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+      if( ee->areDisequal( a, b, false ) ){
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
+/** get the equality engine associated with this query */
+eq::EqualityEngine* EqualityQueryInstProp::getEngine() {
+  return d_qe->getMasterEqualityEngine();
+}
+
+/** get the equivalence class of a */
+void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {
+  //TODO?
+}
+
+TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+  TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );
+  if( !t.isNull() ){
+    return t;
+  }else{
+    //TODO?
+    return TNode::null();
+  }
+}
+
+Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {
+  bool engine_has_a = getEngine()->hasTerm( a );
+  if( engine_has_a ){
+    a = getEngine()->getRepresentative( a );
+  }
+  //get union find representative, if this occurs in the equality engine, return it
+  unsigned prev_size = exp.size();
+  Node ar = getUfRepresentative( a, exp );
+  if( !ar.isNull() ){
+    if( engine_has_a || getEngine()->hasTerm( ar ) ){
+      Assert( getEngine()->hasTerm( ar ) );
+      Assert( getEngine()->getRepresentative( ar )==ar );
+      return ar;
+    }
+  }else{
+    if( engine_has_a ){
+      return a;
+    }
+  }
+  //retract explanation
+  while( exp.size()>prev_size ){
+    exp.pop_back();
+  }
+  return Node::null();
+}
+
+bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {
+  if( areEqual( a, b ) ){
+    return true;
+  }else{
+    std::vector< Node > exp_a;
+    Node ar = getUfRepresentative( a, exp_a );
+    if( !ar.isNull() ){
+      std::vector< Node > exp_b;
+      if( ar==getUfRepresentative( b, exp_b ) ){
+        merge_exp( exp, exp_a );
+        merge_exp( exp, exp_b );
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
+bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {
+  if( areDisequal( a, b ) ){
+    return true;
+  }else{
+    //TODO?
+    return false;
+  }
+}
+
+Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {
+  Assert( exp.empty() );
+  std::map< Node, Node >::iterator it = d_uf.find( a );
+  if( it!=d_uf.end() ){
+    if( it->second==a ){
+      Assert( d_uf_exp[ a ].empty() );
+      return it->second;
+    }else{
+      Node m = getUfRepresentative( it->second, exp );
+      Assert( !m.isNull() );
+      if( m!=it->second ){
+        //update union find
+        d_uf[ a ] = m;
+        //update explanation : merge the explanation of the parent
+        merge_exp( d_uf_exp[ a ], exp );
+        Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;
+      }
+      //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset
+      exp.clear();
+      exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );
+      return m;
+    }
+  }else{
+    return Node::null();
+  }
+}
+
+// set a == b with reason, return status, modify a and b to representatives pre-merge
+int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason ) {
+  if( a==b ){
+    return pol ? STATUS_NONE : STATUS_CONFLICT;
+  }
+  int status = pol ? STATUS_MERGED_UNKNOWN : STATUS_NONE;
+  Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", pol = " << pol << ", reason size = " << reason.size() << std::endl;
+  //get the representative for a
+  std::vector< Node > exp_a;
+  Node ar = getUfRepresentative( a, exp_a );
+  if( ar.isNull() ){
+    Assert( exp_a.empty() );
+    ar = a;
+  }
+  if( ar==b ){
+    Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
+    if( pol ){
+      return STATUS_NONE;
+    }else{
+      merge_exp( reason, exp_a );
+      return STATUS_CONFLICT;
+    }
+  }
+  bool swap = false;
+  //get the representative for b
+  std::vector< Node > exp_b;
+  Node br = getUfRepresentative( b, exp_b );
+  if( br.isNull() ){
+    Assert( exp_b.empty() );
+    br = b;
+    if( !getEngine()->hasTerm( br ) ){
+      if( ar!=a || getEngine()->hasTerm( ar ) ){
+        swap = true;
+      }
+    }else{
+      if( getEngine()->hasTerm( ar ) ){
+        status = STATUS_MERGED_KNOWN;
+      }
+    }
+  }else{
+    if( ar==br ){
+      Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
+      if( pol ){
+        return STATUS_NONE;
+      }else{
+        merge_exp( reason, exp_a );
+        merge_exp( reason, exp_b );
+        return STATUS_CONFLICT;
+      }
+    }else if( getEngine()->hasTerm( ar ) ){
+      if( getEngine()->hasTerm( br ) ){
+        status = STATUS_MERGED_KNOWN;
+      }else{
+        swap = true;
+      }
+    }
+  }
+  
+  if( swap ){
+    //swap
+    Node temp_r = ar;
+    ar = br;
+    br = temp_r;
+  }
+
+  Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );
+  Assert( ar!=br );
+  
+  std::vector< Node > exp_d;
+  if( areDisequalExp( ar, br, exp_d ) ){
+    if( pol ){
+      merge_exp( reason, exp_b );
+      merge_exp( reason, exp_b );
+      merge_exp( reason, exp_d );
+      return STATUS_CONFLICT;
+    }else{
+      return STATUS_NONE;
+    }
+  }else{
+    if( pol ){
+      //update the union find
+      Assert( d_uf_exp[ar].empty() );
+      Assert( d_uf_exp[br].empty() );
+
+      d_uf[ar] = br;
+      merge_exp( d_uf_exp[ar], exp_a );
+      merge_exp( d_uf_exp[ar], exp_b );
+      merge_exp( d_uf_exp[ar], reason );
+
+      d_uf[br] = br;
+      d_uf_exp[br].clear();
+
+      Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;
+      a = ar;
+      b = br;
+      return status;
+    }else{
+      //TODO?
+      return STATUS_NONE;
+    }
+  }
+}
+
+void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) {
+  if( is_prop ){
+    if( isLiteral( n ) ){
+      props.push_back( pol ? n : n.negate() );
+      return;
+    }
+  }
+  args.push_back( n );
+}
+
+bool EqualityQueryInstProp::isLiteral( Node n ) {
+  Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
+  Assert( ak!=NOT );
+  return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;
+}
+
+//this is identical to TermDb::evaluateTerm2, but tracks more information
+Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol,
+                                             std::map< Node, bool >& watch_list_out, std::vector< Node >& props ) {
+  std::map< Node, Node >::iterator itv = visited.find( n );
+  if( itv != visited.end() ){
+    return itv->second;
+  }else{
+    visited[n] = n;
+    Trace("qip-eval") << "evaluate term : " << n << std::endl;
+    std::vector< Node > exp_n;
+    Node ret = getRepresentativeExp( n, exp_n );
+    if( ret.isNull() ){
+      //term is not known to be equal to a representative in equality engine, evaluate it
+      Kind k = n.getKind();
+      if( k==FORALL ){
+        ret = Node::null();
+      }else{
+        std::map< Node, bool > watch_list_out_curr;
+        TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
+        std::vector< Node > args;
+        bool ret_set = false;
+        bool childChanged = false;
+        int abort_i = -1;
+        //get the child entailed polarity
+        Assert( n.getKind()!=IMPLIES );
+        bool newHasPol, newPol;
+        QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );
+        //for each child
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          Node c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props );
+          if( c.isNull() ){
+            ret = Node::null();
+            ret_set = true;
+            break;
+          }else if( c==d_true || c==d_false ){
+            //short-circuiting
+            if( k==kind::AND || k==kind::OR ){
+              if( (k==kind::AND)==(c==d_false) ){
+                ret = c;
+                ret_set = true;
+                break;
+              }else{
+                //redundant
+                c = Node::null();
+                childChanged = true;
+              }
+            }else if( k==kind::ITE && i==0 ){
+              Assert( watch_list_out_curr.empty() );
+              ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props );
+              ret_set = true;
+              break;
+            }else if( k==kind::NOT ){
+              ret = c==d_true ? d_false : d_true;
+              ret_set = true;
+              break;
+            }
+          }
+          if( !c.isNull() ){
+            childChanged = childChanged || n[i]!=c;
+            if( !f.isNull() && !watch_list_out_curr.empty() ){
+              // we are done if this is an UF application and an argument is unevaluated
+              args.push_back( c );
+              abort_i = i;
+              break;
+            }else if( ( k==kind::AND || k==kind::OR ) ){
+              if( c.getKind()==k ){
+                //flatten
+                for( unsigned j=0; j<c.getNumChildren(); j++ ){
+                  addArgument( args, props, c[j], newHasPol, newPol );
+                }
+              }else{
+                addArgument( args, props, c, newHasPol, newPol );
+              }
+              //if we are in a branching position
+              if( hasPol && !newHasPol && args.size()>=2 ){
+                //we are done if at least two args are unevaluated
+                abort_i = i;
+                break;
+              }
+            }else if( k==kind::ITE ){
+              //we are done if we are ITE and condition is unevaluated
+              Assert( i==0 );
+              args.push_back( c );
+              abort_i = i;
+              break;
+            }else{
+              args.push_back( c );
+            }
+          }
+        }
+        //add remaining children if we aborted
+        if( abort_i!=-1 ){
+          for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){
+            args.push_back( n[i] );
+          }
+        }
+        //copy over the watch list
+        for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){
+          watch_list_out[itc->first] = itc->second;
+        }
+
+        //if we have not short-circuited evaluation
+        if( !ret_set ){
+          //if it is an indexed term, return the congruent term
+          if( !f.isNull() && watch_list_out.empty() ){
+            std::vector< TNode > t_args;
+            for( unsigned i=0; i<args.size(); i++ ) {
+              t_args.push_back( args[i] );
+            }
+            Assert( args.size()==n.getNumChildren() );
+            //args contains terms known by the equality engine
+            TNode nn = getCongruentTerm( f, t_args );
+            Trace("qip-eval") << "  got congruent term " << nn << " from DB for " << n << std::endl;
+            if( !nn.isNull() ){
+              //successfully constructed representative in EE
+              Assert( exp_n.empty() );
+              ret = getRepresentativeExp( nn, exp_n );
+              Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl;
+              merge_exp( exp, exp_n );
+              ret_set = true;
+              Assert( !ret.isNull() );
+            }
+          }
+          if( !ret_set ){
+            if( childChanged ){
+              Trace("qip-eval") << "return rewrite" << std::endl;
+              if( ( k==kind::AND || k==kind::OR ) ){
+                if( args.empty() ){
+                  ret = k==kind::AND ? d_true : d_false;
+                  ret_set = true;
+                }else if( args.size()==1 ){
+                  ret = args[0];
+                  ret_set = true;
+                }
+              }else{
+                Assert( args.size()==n.getNumChildren() );
+              }
+              if( !ret_set ){
+                if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+                  args.insert( args.begin(), n.getOperator() );
+                }
+                ret = NodeManager::currentNM()->mkNode( k, args );
+                ret = Rewriter::rewrite( ret );
+                //re-evaluate
+                Node ret_eval = getRepresentativeExp( ret, exp_n );
+                if( !ret_eval.isNull() ){
+                  ret = ret_eval;
+                  watch_list_out.clear();
+                }else{            
+                  watch_list_out[ret] = true;
+                }
+              }
+            }else{
+              ret = n;
+              watch_list_out[ret] = true;
+            }
+          }
+        }
+      }
+    }else{
+      Trace("qip-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;
+      merge_exp( exp, exp_n );
+    }
+    Trace("qip-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl;
+    visited[n] = ret;
+    return ret;
+  }
+}
+
+void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {
+  //TODO : optimize
+  if( v.empty() ){
+    Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() );
+    v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );
+  }else{
+    //std::vector< Node >::iterator v_end = v.end();
+    up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;
+    for( int j=0; j<up_to_size; j++ ){
+      if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){
+        v.push_back( v_to_merge[j] );
+      }
+    }
+  }
+}
+
+
+void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {
+  d_active = true;
+  //information about the instance
+  d_q = q;
+  d_lem = lem;
+  Assert( d_terms.empty() );
+  d_terms.insert( d_terms.end(), terms.begin(), terms.end() );
+  //the current lemma
+  d_curr = body;
+  d_curr_exp.push_back( body );
+}
+
+InstPropagator::InstPropagator( QuantifiersEngine* qe ) :
+d_qe( qe ), d_notify(*this), d_qy( qe ){
+}
+
+bool InstPropagator::reset( Theory::Effort e ) {
+  d_icount = 1;
+  d_ii.clear();
+  for( unsigned i=0; i<2; i++ ){
+    d_conc_to_id[i].clear();
+    d_conc_to_id[i][d_qy.d_true] = 0;
+  }
+  d_conflict = false;
+  d_watch_list.clear();
+  d_update_list.clear();
+  d_relevant_inst.clear();
+  return d_qy.reset( e );
+}
+
+bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
+  if( !d_conflict ){
+    if( Trace.isOn("qip-prop") ){
+      Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;
+      for( unsigned i=0; i<terms.size(); i++ ){
+        Trace("qip-prop") << "  " << terms[i] << std::endl;
+      }
+    }
+    unsigned id = d_icount;
+    d_icount++;
+    Trace("qip-prop") << "...assign id=" << id << std::endl;
+    d_ii[id].init( q, lem, terms, body );
+    //initialize the information
+    if( cacheConclusion( id, body ) ){
+      Assert( d_update_list.empty() );
+      d_update_list.push_back( id );
+      bool firstTime = true;
+      //update infos in the update list until empty
+      do {
+        unsigned uid = d_update_list.back();
+        d_update_list.pop_back();
+        if( d_ii[uid].d_active ){
+          update( uid, d_ii[uid], firstTime );
+        }
+        firstTime = false;
+      }while( !d_conflict && !d_update_list.empty() );
+    }else{
+      d_ii[id].d_active = false;
+      Trace("qip-prop") << "...duplicate." << std::endl;
+    }
+    Trace("qip-prop") << "...finished notify instantiation." << std::endl;
+    return !d_conflict;
+  }else{
+    return true;
+  }
+}
+
+bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
+  Assert( !d_conflict );
+  Assert( ii.d_active );
+  Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;
+  //update the evaluation of the current lemma
+  std::map< Node, Node > visited;
+  std::map< Node, bool > watch_list;
+  std::vector< Node > props;
+  Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props );
+  if( eval.isNull() ){
+    ii.d_active = false;
+  }else if( firstTime || eval!=ii.d_curr ){
+    if( EqualityQueryInstProp::isLiteral( eval ) ){
+      props.push_back( eval );
+      eval = d_qy.d_true;
+      watch_list.clear();
+    }
+    if( Trace.isOn("qip-prop") ){
+      Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;
+      Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = ";
+      debugPrintExplanation( ii.d_curr_exp, "qip-prop" );
+      Trace("qip-prop") << std::endl;
+      Trace("qip-prop") << "...watch list: " << std::endl;
+      for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){
+        Trace("qip-prop") << "  " << itw->first << std::endl;
+      }
+      Trace("qip-prop") << "...new propagations: " << std::endl;
+      for( unsigned i=0; i<props.size(); i++ ){
+        Trace("qip-prop") << "  " << props[i] << std::endl;
+      }
+      Trace("qip-prop") << std::endl;
+    }
+    //determine the status of eval
+    if( eval==d_qy.d_false ){
+      Assert( props.empty() );
+      //we have inferred a conflict
+      conflict( ii.d_curr_exp );
+      return false;
+    }else{
+      for( unsigned i=0; i<props.size(); i++ ){
+        Trace("qip-prop-debug2")  << "Process propagation " << props[i] << std::endl;
+        //if we haven't propagated this literal yet
+        if( cacheConclusion( id, props[i], 1 ) ){
+          Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];
+          bool pol = props[i].getKind()!=NOT;
+          if( lit.getKind()==EQUAL ){
+            propagate( lit[0], lit[1], pol, ii.d_curr_exp );
+          }else{
+            propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );
+          }
+          if( d_conflict ){
+            return false;
+          }
+        }
+        Trace("qip-prop-debug2")  << "Done process propagation " << props[i] << std::endl;
+      }
+      //if we have not inferred this conclusion yet
+      if( cacheConclusion( id, eval ) ){
+        ii.d_curr = eval;
+        //update the watch list
+        Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;
+        //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations.
+        //  Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms.
+        for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){
+          d_watch_list[ itw->first ][ id ] = true;
+        }
+      }else{
+        Trace("qip-prop-debug") << "...conclusion " << eval << " is duplicate." << std::endl;
+        ii.d_active = false;
+      }
+    }
+  }else{
+    Trace("qip-prop-debug") << "...did not update." << std::endl;
+  }
+  Assert( !d_conflict );
+  return true;
+}
+
+void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {
+  if( Trace.isOn("qip-propagate") ){
+    Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";
+    debugPrintExplanation( exp, "qip-propagate" );
+    Trace("qip-propagate") << "..." << std::endl;
+  }
+  //set equal
+  int status = d_qy.setEqual( a, b, pol, exp );
+  if( status==EqualityQueryInstProp::STATUS_NONE ){
+    Trace("qip-prop-debug") << "...already equal/no conflict." << std::endl;
+    return;
+  }else if( status==EqualityQueryInstProp::STATUS_CONFLICT ){
+    Trace("qip-prop-debug") << "...conflict." << std::endl;
+    conflict( exp );
+    return;
+  }
+  if( pol ){
+    if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
+      Assert( d_qy.getEngine()->hasTerm( a ) );
+      Assert( d_qy.getEngine()->hasTerm( b ) );
+      Trace("qip-prop-debug") << "...equality between known terms." << std::endl;
+      addRelevantInstances( exp, "qip-propagate" );
+    }
+    Trace("qip-prop-debug") << "...merged representatives " << a << " and " << b << std::endl;
+    for( unsigned i=0; i<2; i++ ){
+      //update terms from watched lists
+      Node c = i==0 ? a : b;
+      std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );
+      if( it!=d_watch_list.end() ){
+        Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;
+        for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){
+          unsigned idw = itw->first;
+          if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){
+            Trace("qip-prop-debug") << "...will update " << idw << std::endl;
+            d_update_list.push_back( idw );
+          }
+        }
+        d_watch_list.erase( c );
+      }
+    }
+  }
+}
+
+void InstPropagator::conflict( std::vector< Node >& exp ) {
+  Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;
+  d_conflict = true;
+  d_relevant_inst.clear();
+  addRelevantInstances( exp, "qip-propagate" );
+
+  //now, inform quantifiers engine which instances should be retracted
+  for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
+    if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
+      if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
+        Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
+        Assert( false );
+      }
+    }
+  }
+  //will interupt the quantifiers engine
+  Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl;
+}
+
+bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
+  Assert( prop_index==0 || prop_index==1 );
+  //check if the conclusion is non-redundant
+  if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){
+    d_conc_to_id[prop_index][body] = id;
+    return true;
+  }else{
+    return false;
+  }
+}
+
+void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {
+  for( unsigned i=0; i<exp.size(); i++ ){
+    Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
+    Trace(c) << "  relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;
+    d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;
+  }
+}
+
+void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {
+  for( unsigned i=0; i<exp.size(); i++ ){
+    Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
+    Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";
+  }
+}
+
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 0e21dc0d4..a6f76ef44 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -1,160 +1,163 @@
-/*********************                                                        */

-/*! \file inst_propagator.h

- ** \verbatim

- ** Top contributors (to current version):

- **   Andrew Reynolds

- ** This file is part of the CVC4 project.

- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS

- ** in the top-level source directory) and their institutional affiliations.

- ** All rights reserved.  See the file COPYING in the top-level source

- ** directory for licensing information.\endverbatim

- **

- ** \brief Propagate mechanism for instantiations

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H

-#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H

-

-#include <iostream>

-#include <string>

-#include <vector>

-#include <map>

-#include "expr/node.h"

-#include "expr/type_node.h"

-#include "theory/quantifiers_engine.h"

-#include "theory/quantifiers/term_database.h"

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-class EqualityQueryInstProp : public EqualityQuery {

-private:

-  /** pointer to quantifiers engine */

-  QuantifiersEngine* d_qe;

-public:

-  EqualityQueryInstProp( QuantifiersEngine* qe );

-  ~EqualityQueryInstProp(){};

-  /** reset */

-  bool reset( Theory::Effort e );

-  /** identify */

-  std::string identify() const { return "EqualityQueryInstProp"; }

-  /** extends engine */

-  bool extendsEngine() { return true; }

-  /** contains term */

-  bool hasTerm( Node a );

-  /** get the representative of the equivalence class of a */

-  Node getRepresentative( Node a );

-  /** returns true if a and b are equal in the current context */

-  bool areEqual( Node a, Node b );

-  /** returns true is a and b are disequal in the current context */

-  bool areDisequal( Node a, Node b );

-  /** get the equality engine associated with this query */

-  eq::EqualityEngine* getEngine();

-  /** get the equivalence class of a */

-  void getEquivalenceClass( Node a, std::vector< Node >& eqc );

-  /** get congruent term */

-  TNode getCongruentTerm( Node f, std::vector< TNode >& args );

-public:

-  /** get the representative of the equivalence class of a, with explanation */

-  Node getRepresentativeExp( Node a, std::vector< Node >& exp );

-  /** returns true if a and b are equal in the current context */

-  bool areEqualExp( Node a, Node b, std::vector< Node >& exp );

-  /** returns true is a and b are disequal in the current context */

-  bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );

-private:

-  /** term index */

-  std::map< Node, TermArgTrie > d_func_map_trie;

-  /** union find for terms beyond what is stored in equality engine */

-  std::map< Node, Node > d_uf;

-  std::map< Node, std::vector< Node > > d_uf_exp;

-  Node getUfRepresentative( Node a, std::vector< Node >& exp );

-  /** disequality list, stores explanations */

-  std::map< Node, std::map< Node, Node > > d_diseq_list;

-  /** add arg */

-  void addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol );

-public:

-  enum {

-    STATUS_MERGED_KNOWN,

-    STATUS_MERGED_UNKNOWN,

-    STATUS_NONE,

-  };

-  /** set equal */

-  int setEqual( Node& a, Node& b, std::vector< Node >& reason );

-  Node d_true;

-  Node d_false;

-public:

-  //for explanations

-  static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );

-

-  Node evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,

-                        std::map< Node, bool >& watch_list_out, std::vector< TNode >& props );

-  static bool isLiteral( Node n );

-};

-

-class InstPropagator : public QuantifiersUtil {

-private:

-  /** pointer to quantifiers engine */

-  QuantifiersEngine* d_qe;

-  /** notify class */

-  class InstantiationNotifyInstPropagator : public InstantiationNotify {

-    InstPropagator& d_ip;

-  public:

-    InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}

-    virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); }

-  };

-  InstantiationNotifyInstPropagator d_notify;

-  /** notify instantiation method */

-  void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );

-  /** equality query */

-  EqualityQueryInstProp d_qy;

-  class InstInfo {

-  public:

-    bool d_active;

-    Node d_q;

-    Node d_lem;

-    std::vector< Node > d_terms;

-    // the current entailed body

-    Node d_curr;

-    //explanation for current entailed body

-    std::vector< Node > d_curr_exp;

-    void init( Node q, Node lem, std::vector< Node >& terms, Node body );

-  };

-  /** instantiation count/info */

-  unsigned d_icount;

-  std::map< unsigned, InstInfo > d_ii;

-  std::map< TNode, unsigned > d_conc_to_id[2];

-  /** are we in conflict */

-  bool d_conflict;

-  /** watch list */

-  std::map< Node, std::map< unsigned, bool > > d_watch_list;

-  /** update list */

-  std::vector< unsigned > d_update_list;

-  /** relevant instances */

-  std::map< unsigned, bool > d_relevant_inst;

-private:

-  bool update( unsigned id, InstInfo& i, bool firstTime = false );

-  void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );

-  void conflict( std::vector< Node >& exp );

-  bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );

-  void addRelevantInstances( std::vector< Node >& exp, const char * c );

-

-  void debugPrintExplanation( std::vector< Node >& exp, const char * c );

-public:

-  InstPropagator( QuantifiersEngine* qe );

-  ~InstPropagator(){}

-  /** reset */

-  bool reset( Theory::Effort e );

-  /** identify */

-  std::string identify() const { return "InstPropagator"; }

-  /** get the notify mechanism */

-  InstantiationNotify* getInstantiationNotify() { return &d_notify; }

-};

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file inst_propagator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Propagate mechanism for instantiations
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
+#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/term_database.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class EqualityQueryInstProp : public EqualityQuery {
+private:
+  /** pointer to quantifiers engine */
+  QuantifiersEngine* d_qe;
+public:
+  EqualityQueryInstProp( QuantifiersEngine* qe );
+  ~EqualityQueryInstProp(){};
+  /** reset */
+  bool reset( Theory::Effort e );
+  /** identify */
+  std::string identify() const { return "EqualityQueryInstProp"; }
+  /** extends engine */
+  bool extendsEngine() { return true; }
+  /** contains term */
+  bool hasTerm( Node a );
+  /** get the representative of the equivalence class of a */
+  Node getRepresentative( Node a );
+  /** returns true if a and b are equal in the current context */
+  bool areEqual( Node a, Node b );
+  /** returns true is a and b are disequal in the current context */
+  bool areDisequal( Node a, Node b );
+  /** get the equality engine associated with this query */
+  eq::EqualityEngine* getEngine();
+  /** get the equivalence class of a */
+  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+  /** get congruent term */
+  TNode getCongruentTerm( Node f, std::vector< TNode >& args );
+public:
+  /** get the representative of the equivalence class of a, with explanation */
+  Node getRepresentativeExp( Node a, std::vector< Node >& exp );
+  /** returns true if a and b are equal in the current context */
+  bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
+  /** returns true is a and b are disequal in the current context */
+  bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
+private:
+  /** term index */
+  std::map< Node, TermArgTrie > d_func_map_trie;
+  /** union find for terms beyond what is stored in equality engine */
+  std::map< Node, Node > d_uf;
+  std::map< Node, std::vector< Node > > d_uf_exp;
+  Node getUfRepresentative( Node a, std::vector< Node >& exp );
+  /** disequality list, stores explanations */
+  std::map< Node, std::map< Node, Node > > d_diseq_list;
+  /** add arg */
+  void addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol );
+public:
+  enum {
+    STATUS_CONFLICT,
+    STATUS_MERGED_KNOWN,
+    STATUS_MERGED_UNKNOWN,
+    STATUS_NONE,
+  };
+  /** set equal */
+  int setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason );
+  Node d_true;
+  Node d_false;
+public:
+  //for explanations
+  static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );
+
+  Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol,
+                        std::map< Node, bool >& watch_list_out, std::vector< Node >& props );
+  static bool isLiteral( Node n );
+};
+
+class InstPropagator : public QuantifiersUtil {
+private:
+  /** pointer to quantifiers engine */
+  QuantifiersEngine* d_qe;
+  /** notify class */
+  class InstantiationNotifyInstPropagator : public InstantiationNotify {
+    InstPropagator& d_ip;
+  public:
+    InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
+    virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { 
+      return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); 
+    }
+  };
+  InstantiationNotifyInstPropagator d_notify;
+  /** notify instantiation method */
+  bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+  /** equality query */
+  EqualityQueryInstProp d_qy;
+  class InstInfo {
+  public:
+    bool d_active;
+    Node d_q;
+    Node d_lem;
+    std::vector< Node > d_terms;
+    // the current entailed body
+    Node d_curr;
+    //explanation for current entailed body
+    std::vector< Node > d_curr_exp;
+    void init( Node q, Node lem, std::vector< Node >& terms, Node body );
+  };
+  /** instantiation count/info */
+  unsigned d_icount;
+  std::map< unsigned, InstInfo > d_ii;
+  std::map< Node, unsigned > d_conc_to_id[2];
+  /** are we in conflict */
+  bool d_conflict;
+  /** watch list */
+  std::map< Node, std::map< unsigned, bool > > d_watch_list;
+  /** update list */
+  std::vector< unsigned > d_update_list;
+  /** relevant instances */
+  std::map< unsigned, bool > d_relevant_inst;
+private:
+  bool update( unsigned id, InstInfo& i, bool firstTime = false );
+  void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );
+  void conflict( std::vector< Node >& exp );
+  bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );
+  void addRelevantInstances( std::vector< Node >& exp, const char * c );
+
+  void debugPrintExplanation( std::vector< Node >& exp, const char * c );
+public:
+  InstPropagator( QuantifiersEngine* qe );
+  ~InstPropagator(){}
+  /** reset */
+  bool reset( Theory::Effort e );
+  /** identify */
+  std::string identify() const { return "InstPropagator"; }
+  /** get the notify mechanism */
+  InstantiationNotify* getInstantiationNotify() { return &d_notify; }
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index e38304c68..cc9b56a7c 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -107,6 +107,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
 
 void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+    Assert( !d_quantEngine->inConflict() );
     double clSet = 0;
     if( Trace.isOn("cbqi-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
@@ -118,9 +119,12 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
         Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
         if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
           process( q, e, ee );
+          if( d_quantEngine->inConflict() ){
+            break;
+          }
         }
       }
-      if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+      if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
         break;
       }
     }
@@ -567,8 +571,8 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
 
 //new implementation
 
-bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs ) {
-  return d_out->addInstantiation( subs );
+bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) {
+  return d_out->doAddInstantiation( subs );
 }
 
 bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) {
@@ -636,13 +640,13 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
   }
 }
 
-bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) {
+bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   Assert( !d_curr_quant.isNull() );
   //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
   if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
     d_cbqi_set_quant_inactive = true;
     d_incomplete_check = true;
-    d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
+    d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false, true );
     return true;
   }else{
     //check if we need virtual term substitution (if used delta or infinity)
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index d53d9d81c..8ed59778b 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -122,7 +122,7 @@ class CegqiOutputInstStrategy : public CegqiOutput {
 public:
   CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
   InstStrategyCegqi * d_out;
-  bool addInstantiation( std::vector< Node >& subs );
+  bool doAddInstantiation( std::vector< Node >& subs );
   bool isEligibleForInstantiation( Node n );
   bool addLemma( Node lem );
 };
@@ -143,7 +143,7 @@ public:
   InstStrategyCegqi( QuantifiersEngine * qe );
   ~InstStrategyCegqi() throw();
 
-  bool addInstantiation( std::vector< Node >& subs );
+  bool doAddInstantiation( std::vector< Node >& subs );
   bool isEligibleForInstantiation( Node n );
   bool addLemma( Node lem );
   /** identify */
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 8c3154c1c..6d6991476 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -106,7 +106,9 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
           if( d_user_gen[f][i]->isMultiTrigger() ){
             d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
           }
-          //d_quantEngine->d_hasInstantiated[f] = true;
+          if( d_quantEngine->inConflict() ){
+            break;
+          }
         }
       }
     }
@@ -229,11 +231,13 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
               if( r==1 ){
                 d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
               }
-              //d_quantEngine->d_hasInstantiated[f] = true;
+              if( d_quantEngine->inConflict() ){
+                break;
+              }
             }
           }
         }
-        if( hasInst && options::multiTriggerPriority() ){
+        if( d_quantEngine->inConflict() || ( hasInst && options::multiTriggerPriority() ) ){
           break;
         }
       }
@@ -575,6 +579,9 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
         if( process( q, fullEffort ) ){
           //added lemma
           addedLemmas++;
+          if( d_quantEngine->inConflict() ){
+            break;
+          }
         }
       }
     }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 8e88d3434..b59734720 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -60,7 +60,7 @@ void InstantiationEngine::presolve() {
   }
 }
 
-bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
+void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
   //iterate over an internal effort level e
   int e = 0;
@@ -83,8 +83,10 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           InstStrategy* is = d_instStrategies[j];
           Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
           int quantStatus = is->process( q, effort, e_use );
-          Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
-          if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
+          Trace("inst-engine-debug") << " -> status is " << quantStatus << ", conflict=" << d_quantEngine->inConflict() << std::endl;
+          if( d_quantEngine->inConflict() ){
+            return;
+          }else if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
             finished = false;
           }
         }
@@ -96,13 +98,6 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
     }
     e++;
   }
-  //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
-  if( !d_quantEngine->hasAddedLemma() ){
-    return false;
-  }else{
-    Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->getNumLemmasWaiting()-lastWaiting)  << std::endl;
-    return true;
-  }
 }
 
 bool InstantiationEngine::needsCheck( Theory::Effort e ){
@@ -138,8 +133,18 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
     Trace("inst-engine-debug") << d_quantEngine->getModel()->getNumAssertedQuantifiers() << " " << quantActive << std::endl;
     if( quantActive ){
-      bool addedLemmas = doInstantiationRound( e );
-      Trace("inst-engine-debug") << "Add lemmas = " << addedLemmas << std::endl;
+      unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+      doInstantiationRound( e );
+      if( d_quantEngine->inConflict() ){
+        Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting );
+        Trace("inst-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting();
+        if( lastWaiting>0 ){
+          Trace("inst-engine") << " (prev " << lastWaiting << ")";
+        }
+        Trace("inst-engine") << std::endl;
+      }else if( d_quantEngine->hasAddedLemma() ){
+        Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting)  << std::endl;
+      }
     }else{
       d_quants.clear();
     }
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 4d1d4a20f..d2b3740a1 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -70,7 +70,7 @@ private:
   /** is the engine incomplete for this quantifier */
   bool isIncomplete( Node q );
   /** do instantiation round */
-  bool doInstantiationRound( Theory::Effort effort );
+  void doInstantiationRound( Theory::Effort effort );
 public:
   InstantiationEngine( QuantifiersEngine* qe );
   ~InstantiationEngine();
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index bcd36f37a..bdb416b6b 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -155,11 +155,15 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
           int lems = initializeQuantifier( f, f );
           d_statistics.d_init_inst_gen_lemmas += lems;
           d_addedLemmas += lems;
+          if( d_qe->inConflict() ){
+            break;
+          }
         }
       }
       if( d_addedLemmas>0 ){
         Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
       }else{
+        Assert( !d_qe->inConflict() );
         //initialize model
         fm->initialize();
         //analyze the functions
@@ -202,7 +206,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
               }else{
                 d_numQuantNoSelForm++;
               }
-              if( options::fmfInstGenOneQuantPerRound() && lems>0 ){
+              if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
                 break;
               }
             }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
@@ -428,6 +432,9 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
           //add as instantiation
           if( d_qe->addInstantiation( f, m ) ){
             d_addedLemmas++;
+            if( d_qe->inConflict() ){
+              break;
+            }
             //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
             if( eval==-1 ){
               riter.increment2( depIndex );
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 51dccae49..a7e272be0 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -62,6 +62,7 @@ void ModelEngine::reset_round( Theory::Effort e ) {
 
 void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
   if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
+    Assert( !d_quantEngine->inConflict() );
     int addedLemmas = 0;
     FirstOrderModel* fm = d_quantEngine->getModel();
 
@@ -100,8 +101,6 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       //CVC4 will answer SAT or unknown
       Trace("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
-    }else{
-      //otherwise, the search will continue
     }
   }
 }
@@ -194,33 +193,40 @@ int ModelEngine::checkModel(){
   // FMC uses two sub-effort levels
   int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
   for( int e=0; e<e_max; e++) {
-    if (d_addedLemmas==0) {
-      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-        Node f = fm->getAssertedQuantifier( i );
-        Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
-        //determine if we should check this quantifier
-        if( considerQuantifiedFormula( f ) ){
-          exhaustiveInstantiate( f, e );
-          if( Trace.isOn("model-engine-warn") ){
-            if( d_addedLemmas>10000 ){
-              Debug("fmf-exit") << std::endl;
-              debugPrint("fmf-exit");
-              exit( 0 );
-            }
-          }
-          if( optOneQuantPerRound() && d_addedLemmas>0 ){
-            break;
+    for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node f = fm->getAssertedQuantifier( i );
+      Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
+      //determine if we should check this quantifier
+      if( considerQuantifiedFormula( f ) ){
+        exhaustiveInstantiate( f, e );
+        if( Trace.isOn("model-engine-warn") ){
+          if( d_addedLemmas>10000 ){
+            Debug("fmf-exit") << std::endl;
+            debugPrint("fmf-exit");
+            exit( 0 );
           }
-        }else{
-          Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
         }
+        if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
+          break;
+        }
+      }else{
+        Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
       }
     }
+    if( d_addedLemmas>0 ){
+      break;
+    }else{
+      Assert( !d_quantEngine->inConflict() );
+    }
   }
 
   //print debug information
-  Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
-  Trace("model-engine") << d_totalLemmas << std::endl;
+  if( d_quantEngine->inConflict() ){
+    Trace("model-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting() << std::endl;
+  }else{
+    Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
+    Trace("model-engine") << d_totalLemmas << std::endl;
+  }
   return d_addedLemmas;
 }
 
@@ -266,11 +272,13 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
     d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
   }else{
-    Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
-    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-      Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+    if( Trace.isOn("fmf-exh-inst-debug") ){
+      Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
+      for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+        Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+      }
+      Trace("fmf-exh-inst-debug") << std::endl;
     }
-    Trace("fmf-exh-inst-debug") << std::endl;
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
@@ -289,6 +297,9 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
           //add as instantiation
           if( d_quantEngine->addInstantiation( f, m ) ){
             addedLemmas++;
+            if( d_quantEngine->inConflict() ){
+              break;
+            }
           }else{
             Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
           }
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index c5ccd9d82..5bf8d8a8d 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -68,7 +68,7 @@ bool RewriteEngine::needsCheck( Theory::Effort e ){
 
 void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
-  //if( e==Theory::EFFORT_FULL ){  
+    Assert( !d_quantEngine->inConflict() );
     Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl;
     //if( e==Theory::EFFORT_LAST_CALL ){
     //  if( !d_quantEngine->getModel()->isModelSet() ){
@@ -95,7 +95,7 @@ void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) {
     //per priority level
     int index = 0;
     bool success = true;
-    while( success && index<(int)d_priority_order.size() ) {
+    while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) {
       addedLemmas += checkRewriteRule( d_priority_order[index], e );
       index++;
       if( index<(int)d_priority_order.size() ){
@@ -104,11 +104,6 @@ void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) {
     }
 
     Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl;
-    if (addedLemmas==0) {
-
-    }else{
-      //otherwise, the search will continue
-    }
   }
 }
 
@@ -129,7 +124,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
         Trace("rewrite-engine-inst-debug") << "   Reset round..." << std::endl;
         qi->reset_round( qcf );
         Trace("rewrite-engine-inst-debug") << "   Get matches..." << std::endl;
-        while( qi->getNextMatch( qcf ) &&
+        while( !d_quantEngine->inConflict() && qi->getNextMatch( qcf ) &&
                ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
           Trace("rewrite-engine-inst-debug") << "   Got match to complete..." << std::endl;
           qi->debugPrintMatch( "rewrite-engine-inst-debug" );
@@ -138,7 +133,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
             bool doContinue = false;
             bool success = true;
             int tempAddedLemmas = 0;
-            while( tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
+            while( !d_quantEngine->inConflict() && tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
               success = qi->completeMatch( qcf, assigned, doContinue );
               doContinue = true;
               if( success ){