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.

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) {