From eb5debabce433774a0dbfd46745efb8fcf38b8ab Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 14 Feb 2014 15:44:21 -0600
Subject: [PATCH] Make QCF more incremental.  Fix bug in QCF handling of ITE
 formulas, add support for ITE terms.  Add full-delay inst-when mode.  Make
 strings come before quantifiers in check.  Minor cleanup.

---
 src/Makefile.am                               |   2 +-
 .../quantifiers/inst_strategy_e_matching.cpp  |   4 +-
 .../quantifiers/instantiation_engine.cpp      |   2 +
 src/theory/quantifiers/modes.h                |   2 +
 src/theory/quantifiers/options_handlers.h     |   6 +
 .../quantifiers/quant_conflict_find.cpp       | 189 +++++++++++++-----
 src/theory/quantifiers/quant_conflict_find.h  |  10 +-
 src/theory/quantifiers/trigger.h              |   9 +-
 8 files changed, 170 insertions(+), 54 deletions(-)

diff --git a/src/Makefile.am b/src/Makefile.am
index e5e1b9346..f20fabf6b 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -20,7 +20,7 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
-THEORIES = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules idl strings
+THEORIES = builtin booleans uf arith bv arrays datatypes strings quantifiers rewriterules idl
 
 lib_LTLIBRARIES = libcvc4.la
 
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 5e2353e8a..63cb22f70 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -168,7 +168,9 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
           if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){
             d_processed_trigger[f][tr] = true;
             //if( tr->isMultiTrigger() )
-              Trace("process-trigger") << "  Process " << (*tr) << "..." << std::endl;
+              Trace("process-trigger") << "  Process ";
+              tr->debugPrint("process-trigger");
+              Trace("process-trigger") << "..." << std::endl;
             InstMatch baseMatch( f );
             int numInst = tr->addInstantiations( baseMatch );
             //if( tr->isMultiTrigger() )
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 41198c1f4..199d3233c 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -173,6 +173,8 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
   d_performCheck = false;
   if( options::instWhenMode()==INST_WHEN_FULL ){
     d_performCheck = ( e >= Theory::EFFORT_FULL );
+  }else if( options::instWhenMode()==INST_WHEN_FULL_DELAY ){
+    d_performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck();
   }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
     d_performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
   }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 75b9eba3e..38c9211a3 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -31,6 +31,8 @@ typedef enum {
   INST_WHEN_PRE_FULL,
   /** Apply instantiation round at full effort or above  */
   INST_WHEN_FULL,
+  /** Apply instantiation round at full effort, after all other theories finish, or above  */
+  INST_WHEN_FULL_DELAY,
   /** Apply instantiation round at full effort half the time, and last call always */
   INST_WHEN_FULL_LAST_CALL,
   /** Apply instantiation round at last call only */
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 15d52cc96..eb2c05858 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -32,6 +32,10 @@ Modes currently supported by the --inst-when option:\n\
 full (default)\n\
 + Run instantiation round at full effort, before theory combination.\n\
 \n\
+full-delay \n\
++ Run instantiation round at full effort, before theory combination, after\n\
+  all other theories have finished.\n\
+\n\
 full-last-call\n\
 + Alternate running instantiation rounds at full effort and last\n\
   call.  In other words, interleave instantiation and theory combination.\n\
@@ -147,6 +151,8 @@ inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg,
     return INST_WHEN_PRE_FULL;
   } else if(optarg == "full") {
     return INST_WHEN_FULL;
+  } else if(optarg == "full-delay") {
+    return INST_WHEN_FULL_DELAY;
   } else if(optarg == "full-last-call") {
     return INST_WHEN_FULL_LAST_CALL;
   } else if(optarg == "last-call") {
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 08bd0f179..312003519 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -95,6 +95,9 @@ void QuantInfo::initialize( Node q, Node qn ) {
         if( !d_var_mg[j]->isValid() ){
           d_mg->setInvalid();
           break;
+        }else{
+          std::vector< int > bvars;
+          d_var_mg[j]->determineVariableOrder( this, bvars );
         }
       }
     }
@@ -120,10 +123,11 @@ void QuantInfo::initialize( Node q, Node qn ) {
 }
 
 void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
+  Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
   if( n.getKind()==FORALL ){
     registerNode( n[1], hasPol, pol );
   }else{
-    if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){
+    if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){
       if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
         //literals
         if( n.getKind()==EQUAL ){
@@ -132,6 +136,10 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
           }
         }else if( MatchGen::isHandledUfTerm( n ) ){
           flatten( n );
+        }else if( n.getKind()==ITE && !n[1].getType().isBoolean() ){
+          for( unsigned i=1; i<=2; i++ ){
+            flatten( n[i] );
+          }
         }
       }
     }
@@ -151,17 +159,26 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
 }
 
 void QuantInfo::flatten( Node n ) {
+  Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
   if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
     if( d_var_num.find( n )==d_var_num.end() ){
-      //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;
+      Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
       d_var_num[n] = d_vars.size();
       d_vars.push_back( n );
       d_match.push_back( TNode::null() );
       d_match_term.push_back( TNode::null() );
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        flatten( n[i] );
+      if( n.getKind()==ITE ){
+        registerNode( n, false, false );
+      }else{
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          flatten( n[i] );
+        }
       }
+    }else{
+      Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
     }
+  }else{
+    Trace("qcf-qregister-debug2") << "...is ground." << std::endl;
   }
 }
 
@@ -599,6 +616,25 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
         }
         d_qni_size++;
       }
+    }else if( n.getKind()==ITE ){
+      d_type = typ_ite_var;
+      d_type_not = false;
+      d_n = n;
+      d_children.push_back( MatchGen( qi, d_n[0] ) );
+      if( d_children[0].isValid() ){
+        d_type = typ_ite_var;
+        for( unsigned i=1; i<=2; i++ ){
+          Node nn = n.eqNode( n[i] );
+          d_children.push_back( MatchGen( qi, nn ) );
+          d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 );
+          if( !d_children[d_children.size()-1].isValid() ){
+            setInvalid();
+            break;
+          }
+        }
+      }else{
+        d_type = typ_invalid;
+      }
     }else{
       //for now, unknown term
       d_type = typ_invalid;
@@ -618,7 +654,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
           if( d_n.getKind()!=FORALL || i==1 ){
             d_children.push_back( MatchGen( qi, d_n[i] ) );
-            if( d_children[d_children.size()-1].d_type==typ_invalid ){
+            if( !d_children[d_children.size()-1].isValid() ){
               setInvalid();
               break;
             }
@@ -650,6 +686,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
         if( d_n.getKind()==EQUAL ){
           for( unsigned i=0; i<2; i++ ){
             if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){
+              if( !qi->isVar( d_n[i] ) ){
+                Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;
+              }
               Assert( qi->isVar( d_n[i] ) );
             }else{
               d_qni_gterm[i] = d_n[i];
@@ -727,9 +766,7 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars
     }
   }
   if( isCom ){
-    //first, do those that do not bind any new variables
-    //second, do those with common variables
-    //last, do those with no common variables
+    //children that bind the least number of unbound variables go first
     do {
       int min_score = -1;
       int min_score_index = -1;
@@ -881,7 +918,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       //if successful and non-redundant, store that we need to cleanup this
       if( addc==1 ){
         for( unsigned i=0; i<2; i++ ){
-          if( vn[i]!=-1 ){
+          if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){
             d_qni_bound[vn[i]] = vn[i];
           }
         }
@@ -1032,7 +1069,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
     }
     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
     return success;
-  }else if( d_type==typ_formula ){
+  }else if( d_type==typ_formula || d_type==typ_ite_var ){
     if( d_child_counter!=-1 ){
       bool success = false;
       while( !success && d_child_counter>=0 ){
@@ -1096,7 +1133,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
             int index1 = d_child_counter==4 ? 1 : 0;
             if( getChild( index1 )->getNextMatch( p, qi ) ){
               d_child_counter++;
-              getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, qi );
+              getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );
             }else{
               if( d_child_counter==4 ){
                 d_child_counter = -1;
@@ -1107,7 +1144,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
             }
           }
           if( d_child_counter%2==1 ){
-            int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2);
+            int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2);
             if( getChild( index2 )->getNextMatch( p, qi ) ){
               success = true;
             }else{
@@ -1261,6 +1298,7 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
     case typ_pred: Trace(c) << "pred";break;
     case typ_formula: Trace(c) << "formula";break;
     case typ_var: Trace(c) << "var";break;
+    case typ_ite_var: Trace(c) << "ite_var";break;
     case typ_top: Trace(c) << "top";break;
     }
   }else{
@@ -1271,6 +1309,7 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
     case typ_pred: Debug(c) << "pred";break;
     case typ_formula: Debug(c) << "formula";break;
     case typ_var: Debug(c) << "var";break;
+    case typ_ite_var: Debug(c) << "ite_var";break;
     case typ_top: Debug(c) << "top";break;
     }
   }
@@ -1419,10 +1458,6 @@ int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
   return ret;
 }
 
-bool QuantConflictFind::isPropagationSet() {
-  return !d_prop_eq[0].isNull();
-}
-
 bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
   //if( d_effort==QuantConflictFind::effort_mc ){
   //  return n1==n2 || !areDisequal( n1, n2 );
@@ -1473,6 +1508,7 @@ Node QuantConflictFind::evaluateTerm( Node n ) {
   if( MatchGen::isHandledUfTerm( n ) ){
     Node f = MatchGen::getOperator( this, n );
     Node nn;
+    computeUfTerms( f );
     if( getEqualityEngine()->hasTerm( n ) ){
       computeArgReps( n );
       nn = d_uf_terms[f].existsTerm( n, d_arg_reps[n] );
@@ -1491,6 +1527,13 @@ Node QuantConflictFind::evaluateTerm( Node n ) {
       Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;
       return n;
     }
+  }else if( n.getKind()==ITE ){
+    int v = evaluate( n[0], false, false );
+    if( v==1 ){
+      return evaluateTerm( n[1] );
+    }else if( v==-1 ){
+      return evaluateTerm( n[2] );
+    }
   }
   return getRepresentative( n );
 }
@@ -1512,6 +1555,7 @@ QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreat
 */
 
 QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {
+  computeUfTerms( f );
   std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms.find( f );
   if( itut==d_eqc_uf_terms.end() ){
     return NULL;
@@ -1530,6 +1574,7 @@ QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {
 }
 
 QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {
+  computeUfTerms( f );
   std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );
   if( itut!=d_uf_terms.end() ){
     return &itut->second;
@@ -1630,6 +1675,32 @@ void QuantConflictFind::check( Theory::Effort level ) {
       Trace("qcf-check") << "Compute relevant equalities..." << std::endl;
       computeRelevantEqr();
 
+      //determine order for quantified formulas
+      std::vector< Node > qorder;
+      std::map< Node, bool > qassert;
+      //mark which are asserted
+      for( unsigned i=0; i<d_qassert.size(); i++ ){
+        qassert[d_qassert[i]] = true;
+      }
+      //add which ones are specified in the order
+      for( unsigned i=0; i<d_quant_order.size(); i++ ){
+        Node n = d_quant_order[i];
+        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() && qassert.find( n )!=qassert.end() ){
+          qorder.push_back( n );
+        }
+      }
+      d_quant_order.clear();
+      d_quant_order.insert( d_quant_order.begin(), qorder.begin(), qorder.end() );
+      //add remaining
+      for( unsigned i=0; i<d_qassert.size(); i++ ){
+        Node n = d_qassert[i];
+        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() ){
+          qorder.push_back( n );
+        }
+      }
+
+
+
       if( Trace.isOn("qcf-debug") ){
         Trace("qcf-debug") << std::endl;
         debugPrint("qcf-debug");
@@ -1638,14 +1709,9 @@ void QuantConflictFind::check( Theory::Effort level ) {
       short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : options::qcfMode()==QCF_PROP_EQ ? effort_prop_eq : effort_mc;
       for( short e = effort_conflict; e<=end_e; e++ ){
         d_effort = e;
-        if( e == effort_prop_eq ){
-          for( unsigned i=0; i<2; i++ ){
-            d_prop_eq[i] = Node::null();
-          }
-        }
         Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
-        for( unsigned j=0; j<d_qassert.size(); j++ ){
-          Node q = d_qassert[j];
+        for( unsigned j=0; j<qorder.size(); j++ ){
+          Node q = qorder[j];
           QuantInfo * qi = &d_qinfo[q];
           Trace("qcf-check") << "Check quantified formula ";
           debugPrintQuant("qcf-check", q);
@@ -1694,6 +1760,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
                     Trace("qcf-check") << "   ... Added instantiation" << std::endl;
                     ++addedLemmas;
                     if( e==effort_conflict ){
+                      d_quant_order.insert( d_quant_order.begin(), q );
                       d_conflict.set( true );
                       ++(d_statistics.d_conflict_inst);
                       break;
@@ -1759,21 +1826,21 @@ void QuantConflictFind::computeRelevantEqr() {
   d_eqcs.clear();
   d_model_basis.clear();
   d_arg_reps.clear();
-  double clSet = 0;
-  if( Trace.isOn("qcf-opt") ){
-    clSet = double(clock())/double(CLOCKS_PER_SEC);
-  }
+  //double clSet = 0;
+  //if( Trace.isOn("qcf-opt") ){
+  //  clSet = double(clock())/double(CLOCKS_PER_SEC);
+  //}
 
-  long nTermst = 0;
-  long nTerms = 0;
-  long nEqc = 0;
+  //long nTermst = 0;
+  //long nTerms = 0;
+  //long nEqc = 0;
 
   //which nodes are irrelevant for disequality matches
   std::map< TNode, bool > irrelevant_dnode;
   //now, store matches
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
   while( !eqcs_i.isFinished() ){
-    nEqc++;
+    //nEqc++;
     Node r = (*eqcs_i);
     TypeNode rtn = r.getType();
     if( options::qcfMode()==QCF_MC ){
@@ -1796,6 +1863,9 @@ void QuantConflictFind::computeRelevantEqr() {
     }else{
       d_eqcs[rtn].push_back( r );
     }
+    //if( r.getType().isInteger() ){
+    //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;
+    //}
     //EqcInfo * eqcir = getEqcInfo( r, false );
     //get relevant nodes that we are disequal from
     /*
@@ -1814,6 +1884,7 @@ void QuantConflictFind::computeRelevantEqr() {
     }
     */
     //process disequalities
+    /*
     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
     while( !eqc_i.isFinished() ){
       TNode n = (*eqc_i);
@@ -1825,28 +1896,36 @@ void QuantConflictFind::computeRelevantEqr() {
         //    std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;
         //  }
         //}
-
-        bool isRedundant;
-        std::map< TNode, std::vector< TNode > >::iterator it_na;
-        TNode fn;
-        if( MatchGen::isHandledUfTerm( n ) ){
-          Node f = MatchGen::getOperator( this, n );
-          computeArgReps( n );
-          it_na = d_arg_reps.find( n );
-          Assert( it_na!=d_arg_reps.end() );
-          Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );
-          isRedundant = (nadd!=n);
-          d_uf_terms[f].addTerm( n, d_arg_reps[n] );
+        if( !quantifiers::TermDb::hasBoundVarAttr( n ) ){    //temporary
+
+          bool isRedundant;
+          std::map< TNode, std::vector< TNode > >::iterator it_na;
+          TNode fn;
+          if( MatchGen::isHandledUfTerm( n ) ){
+            Node f = MatchGen::getOperator( this, n );
+            computeArgReps( n );
+            it_na = d_arg_reps.find( n );
+            Assert( it_na!=d_arg_reps.end() );
+            Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );
+            isRedundant = (nadd!=n);
+            d_uf_terms[f].addTerm( n, d_arg_reps[n] );
+          }else{
+            isRedundant = false;
+          }
+          nTerms += isRedundant ? 0 : 1;
         }else{
-          isRedundant = false;
+          if( Debug.isOn("qcf-nground") ){
+            Debug("qcf-nground") << "Non-ground term in eqc : " << n << std::endl;
+            Assert( false );
+          }
         }
-        nTerms += isRedundant ? 0 : 1;
       }
       ++eqc_i;
     }
-    //process_eqc[r] = true;
+    */
     ++eqcs_i;
   }
+  /*
   if( Trace.isOn("qcf-opt") ){
     double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
     Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
@@ -1854,6 +1933,7 @@ void QuantConflictFind::computeRelevantEqr() {
     Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;
     Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;
   }
+  */
 }
 
 void QuantConflictFind::computeArgReps( TNode n ) {
@@ -1865,6 +1945,23 @@ void QuantConflictFind::computeArgReps( TNode n ) {
   }
 }
 
+void QuantConflictFind::computeUfTerms( TNode f ) {
+  if( d_uf_terms.find( f )==d_uf_terms.end() ){
+    d_uf_terms[f].clear();
+    unsigned nt = d_quantEngine->getTermDatabase()->d_op_map[f].size();
+    for( unsigned i=0; i<nt; i++ ){
+      Node n = d_quantEngine->getTermDatabase()->d_op_map[f][i];
+      if( !n.getAttribute(NoMatchAttribute()) ){
+        Assert( getEqualityEngine()->hasTerm( n ) );
+        Node r = getRepresentative( n );
+        computeArgReps( n );
+        d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );
+        d_uf_terms[f].addTerm( n, d_arg_reps[n] );
+      }
+    }
+  }
+}
+
 //-------------------------------------------------- debugging
 
 
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 80e56acbd..9b64a312d 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -61,6 +61,7 @@ private:
   std::map< int, TNode > d_qni_gterm;
   std::map< int, TNode > d_qni_gterm_rep;
   std::map< int, int > d_qni_bound;
+  std::vector< int > d_qni_bound_except;
   std::map< int, TNode > d_qni_bound_cons;
   std::map< int, int > d_qni_bound_cons_var;
   std::map< int, int >::iterator d_binding_it;
@@ -81,6 +82,7 @@ public:
     typ_eq,
     typ_formula,
     typ_var,
+    typ_ite_var,
     typ_top,
   };
   void debugPrintType( const char * c, short typ, bool isTrace = false );
@@ -156,7 +158,7 @@ private:
   context::Context* d_c;
   context::CDO< bool > d_conflict;
   bool d_performCheck;
-  //void registerAssertion( Node n );
+  std::vector< Node > d_quant_order;
 private:
   std::map< Node, Node > d_op_node;
   int d_fid_count;
@@ -204,6 +206,8 @@ private:  //for equivalence classes
   std::map< TNode, std::vector< TNode > > d_arg_reps;
   //compute arg reps
   void computeArgReps( TNode n );
+  //compute
+  void computeUfTerms( TNode f );
 public:
   enum {
     effort_conflict,
@@ -211,10 +215,6 @@ public:
     effort_mc,
   };
   short d_effort;
-  //for effort_prop
-  TNode d_prop_eq[2];
-  bool d_prop_pol;
-  bool isPropagationSet();
   bool areMatchEqual( TNode n1, TNode n2 );
   bool areMatchDisequal( TNode n1, TNode n2 );
 public:
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 23cf5f5d0..74fc16764 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -48,7 +48,6 @@ public:
 public:
   std::vector< Node > d_nodes;
 public:
-  void debugPrint( const char* c );
   IMGenerator* getGenerator() { return d_mg; }
 public:
   /** reset instantiation round (call this whenever equivalence classes have changed) */
@@ -123,6 +122,14 @@ public:
     out << " )";
     */
   }
+  void debugPrint( const char * c ) {
+    Trace(c) << "TRIGGER( ";
+    for( int i=0; i<(int)d_nodes.size(); i++ ){
+      if( i>0 ){ Trace(c) << ", "; }
+      Trace(c) << d_nodes[i];
+    }
+    Trace(c) << " )";
+  }
 };
 
 inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) {
-- 
2.30.2