From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 18 Jan 2014 17:27:45 +0000 (-0600)
Subject: Performance optimization for E-matching, working on using QCF module for propagations.
X-Git-Tag: cvc5-1.0.0~7142
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6f7c7e36c7897e9c9e6fd556bcdddcb9574d881;p=cvc5.git

Performance optimization for E-matching, working on using QCF module for propagations.
---

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 783f6284d..60fa672b3 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -68,35 +68,57 @@ void CandidateGeneratorQE::resetInstantiationRound(){
 void CandidateGeneratorQE::reset( Node eqc ){
   d_term_iter = 0;
   if( eqc.isNull() ){
-    d_using_term_db = true;
+    d_mode = cand_term_db;
   }else{
     //create an equivalence class iterator in eq class eqc
-    d_eqc.clear();
-    d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
-    d_using_term_db = false;
+    //d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
+
+    eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
+    if( ee->hasTerm( eqc ) ){
+      Node rep = ee->getRepresentative( eqc );
+      d_eqc_iter = eq::EqClassIterator( rep, ee );
+      d_mode = cand_term_eqc;
+    }else{
+      d_n = eqc;
+      d_mode = cand_term_ident;
+    }
+    //a should be in its equivalence class
+    //Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
+  }
+}
+bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
+  if( n.hasOperator() && n.getOperator()==d_op ){
+    if( isLegalCandidate( n ) ){
+      return true;
+    }
   }
+  return false;
 }
 
 Node CandidateGeneratorQE::getNextCandidate(){
-  if( d_term_iter>=0 ){
-    if( d_using_term_db ){
-      //get next candidate term in the uf term database
-      while( d_term_iter<d_term_iter_limit ){
-        Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
-        d_term_iter++;
-        if( isLegalCandidate( n ) ){
-          return n;
-        }
+  if( d_mode==cand_term_db ){
+    //get next candidate term in the uf term database
+    while( d_term_iter<d_term_iter_limit ){
+      Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+      d_term_iter++;
+      if( isLegalCandidate( n ) ){
+        return n;
       }
-    }else{
-      while( d_term_iter<(int)d_eqc.size() ){
-        Node n = d_eqc[d_term_iter];
-        d_term_iter++;
-        if( n.hasOperator() && n.getOperator()==d_op ){
-          if( isLegalCandidate( n ) ){
-            return n;
-          }
-        }
+    }
+  }else if( d_mode==cand_term_eqc ){
+    while( !d_eqc_iter.isFinished() ){
+      Node n = *d_eqc_iter;
+      ++d_eqc_iter;
+      if( isLegalOpCandidate( n ) ){
+        return n;
+      }
+    }
+  }else if( d_mode==cand_term_ident ){
+    if( !d_n.isNull() ){
+      Node n = d_n;
+      d_n = Node::null();
+      if( isLegalOpCandidate( n ) ){
+        return n;
       }
     }
   }
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index a87c24596..74029b633 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -79,10 +79,19 @@ private:
   //instantiator pointer
   QuantifiersEngine* d_qe;
   //the equality class iterator
-  std::vector< Node > d_eqc;
+  eq::EqClassIterator d_eqc_iter;
+  //std::vector< Node > d_eqc;
   int d_term_iter;
   int d_term_iter_limit;
   bool d_using_term_db;
+  enum {
+    cand_term_db,
+    cand_term_ident,
+    cand_term_eqc,
+  };
+  short d_mode;
+  bool isLegalOpCandidate( Node n );
+  Node d_n;
 public:
   CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
   ~CandidateGeneratorQE(){}
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 4cb62b523..66191107d 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -353,7 +353,7 @@ void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms
   }
 }
 
-int QuantConflictFind::evaluate( Node n ) {
+int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
   int ret = 0;
   if( n.getKind()==EQUAL ){
     Node n1 = getTerm( n[0] );
@@ -425,6 +425,33 @@ int QuantConflictFind::evaluate( Node n ) {
   return ret;
 }
 
+bool QuantConflictFind::isPropagationSet() {
+  return !d_prop_eq[0].isNull();
+}
+
+bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
+  return n1==n2;
+  /*
+  if( n1==n2 ){
+    return true;
+  }else if( isPropagationSet() && d_prop_pol ){
+    return ( d_prop_eq[0]==n1 && d_prop_eq[1]==n2 ) || ( d_prop_eq[0]==n2 && d_prop_eq[1]==n1 );
+  }
+  */
+}
+
+bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
+  //return n1!=n2;
+  return areDisequal( n1, n2 );
+  /*
+  if( n1!=n2 ){
+    return true;
+  }else if( isPropagationSet() && !d_prop_pol ){
+    return ( d_prop_eq[0]==n1 && d_prop_eq[1]==n2 ) || ( d_prop_eq[0]==n2 && d_prop_eq[1]==n1 );
+  }
+  */
+}
+
 //-------------------------------------------------- handling assertions / eqc
 
 void QuantConflictFind::assertNode( Node q ) {
@@ -467,20 +494,6 @@ Node QuantConflictFind::getTerm( Node n ) {
 }
 
 QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {
-  /*
-  NodeBoolMap::iterator it = d_eqc.find( n );
-  if( it==d_eqc.end() ){
-    if( doCreate ){
-      d_eqc[n] = true;
-    }else{
-      //equivalence class does not currently exist
-      return NULL;
-    }
-  }else{
-    //should only ask for valid equivalence classes
-    Assert( (*it).second );
-  }
-  */
   std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );
   if( it2==d_eqc_info.end() ){
     if( doCreate ){
@@ -494,6 +507,24 @@ QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreat
   return it2->second;
 }
 
+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {
+  std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms[ eqc ].find( f );
+  if( itut!=d_eqc_uf_terms[ eqc ].end() ){
+    return &itut->second;
+  }else{
+    return NULL;
+  }
+}
+
+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {
+  std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );
+  if( itut!=d_uf_terms.end() ){
+    return &itut->second;
+  }else{
+    return NULL;
+  }
+}
+
 /** new node */
 void QuantConflictFind::newEqClass( Node n ) {
   Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;
@@ -573,7 +604,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
       Assert( false );
     }
   }else{
-    bool addedLemma = false;
+    int addedLemmas = 0;
     if( d_performCheck ){
       ++(d_statistics.d_inst_rounds);
       double clSet = 0;
@@ -590,69 +621,82 @@ void QuantConflictFind::check( Theory::Effort level ) {
         Trace("qcf-debug") << std::endl;
       }
 
-
-      Trace("qcf-check") << "Checking quantified formulas..." << std::endl;
-      for( unsigned j=0; j<d_qassert.size(); j++ ){
-        Node q = d_qassert[j];
-        Trace("qcf-check") << "Check quantified formula ";
-        debugPrintQuant("qcf-check", q);
-        Trace("qcf-check") << " : " << q << "..." << std::endl;
-
-        Assert( d_qinfo.find( q )!=d_qinfo.end() );
-        if( d_qinfo[q].d_mg->isValid() ){
-          d_qinfo[q].reset_round( this );
-          //try to make a matches making the body false
-          d_qinfo[q].d_mg->reset( this, false, q );
-          while( d_qinfo[q].d_mg->getNextMatch( this, q ) ){
-
-            Trace("qcf-check") << "*** Produced match : " << std::endl;
-            d_qinfo[q].debugPrintMatch("qcf-check");
-            Trace("qcf-check") << std::endl;
-
-            if( !d_qinfo[q].isMatchSpurious( this ) ){
-              std::vector< int > assigned;
-              if( d_qinfo[q].completeMatch( this, q, assigned ) ){
-                InstMatch m;
-                for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-                  Node cv = d_qinfo[q].getCurrentValue( d_qinfo[q].d_match[i] );
-                  Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_qinfo[q].d_match[i] << std::endl;
-                  m.set( d_quantEngine, q, i, cv );
-                }
-                if( Debug.isOn("qcf-check-inst") ){
-                  Node inst = d_quantEngine->getInstantiation( q, m );
-                  Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
-                  Assert( evaluate( inst )==-1 );
-                }
-                if( d_quantEngine->addInstantiation( q, m ) ){
-                  Trace("qcf-check") << "   ... Added instantiation" << std::endl;
-                  d_quantEngine->flushLemmas();
-                  d_conflict.set( true );
-                  addedLemma = true;
-                  ++(d_statistics.d_conflict_inst);
-                  break;
+      for( short e = effort_conflict; e<=effort_conflict; e++ ){
+        d_effort = e;
+        if( e == effort_propagation ){
+          for( unsigned i=0; i<2; i++ ){
+            d_prop_eq[i] = Node::null();
+          }
+        }
+        Trace("qcf-check") << "Checking quantified formulas..." << std::endl;
+        for( unsigned j=0; j<d_qassert.size(); j++ ){
+          Node q = d_qassert[j];
+          Trace("qcf-check") << "Check quantified formula ";
+          debugPrintQuant("qcf-check", q);
+          Trace("qcf-check") << " : " << q << "..." << std::endl;
+
+          Assert( d_qinfo.find( q )!=d_qinfo.end() );
+          if( d_qinfo[q].d_mg->isValid() ){
+            d_qinfo[q].reset_round( this );
+            //try to make a matches making the body false
+            d_qinfo[q].d_mg->reset( this, false, q );
+            while( d_qinfo[q].d_mg->getNextMatch( this, q ) ){
+
+              Trace("qcf-check") << "*** Produced match : " << std::endl;
+              d_qinfo[q].debugPrintMatch("qcf-check");
+              Trace("qcf-check") << std::endl;
+
+              if( !d_qinfo[q].isMatchSpurious( this ) ){
+                std::vector< int > assigned;
+                if( d_qinfo[q].completeMatch( this, q, assigned ) ){
+                  InstMatch m;
+                  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+                    Node cv = d_qinfo[q].getCurrentValue( d_qinfo[q].d_match[i] );
+                    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_qinfo[q].d_match[i] << std::endl;
+                    m.set( d_quantEngine, q, i, cv );
+                  }
+                  if( Debug.isOn("qcf-check-inst") ){
+                    Node inst = d_quantEngine->getInstantiation( q, m );
+                    Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
+                    Assert( evaluate( inst )==-1 );
+                  }
+                  if( d_quantEngine->addInstantiation( q, m ) ){
+                    Trace("qcf-check") << "   ... Added instantiation" << std::endl;
+                    ++addedLemmas;
+                    if( e==effort_conflict ){
+                      d_conflict.set( true );
+                      ++(d_statistics.d_conflict_inst);
+                      break;
+                    }else if( e==effort_propagation ){
+                      ++(d_statistics.d_prop_inst);
+                    }
+                  }else{
+                    Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;
+                    Assert( false );
+                  }
+                  //clean up assigned
+                  for( unsigned i=0; i<assigned.size(); i++ ){
+                    d_qinfo[q].d_match.erase( assigned[i] );
+                  }
                 }else{
-                  Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;
-                  Assert( false );
-                }
-                //clean up assigned
-                for( unsigned i=0; i<assigned.size(); i++ ){
-                  d_qinfo[q].d_match.erase( assigned[i] );
+                  Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
                 }
               }else{
-                Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
+                Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;
               }
-            }else{
-              Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;
             }
           }
+          if( d_conflict ){
+            break;
+          }
         }
-        if( addedLemma ){
-          break;
+        if( Trace.isOn("qcf-engine") ){
+          double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+          Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet) << ", addedLemmas = " << addedLemmas << std::endl;
+        }
+        if( addedLemmas>0 ){
+          d_quantEngine->flushLemmas();
         }
-      }
-      if( Trace.isOn("qcf-engine") ){
-        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-        Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet) << ", addedLemma = " << addedLemma << std::endl;
       }
     }
     Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
@@ -955,7 +999,7 @@ bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p,
       return false;
     }else if( !isVar( n ) && !isVar( cv ) ){
       //they must actually be disequal
-      if( !p->areDisequal( n, cv ) ){
+      if( !p->areMatchDisequal( n, cv ) ){
         return false;
       }
     }
@@ -1022,16 +1066,14 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
             //copy or check disequalities
             std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( v );
             if( itd!=d_curr_var_deq.end() ){
-              //std::vector< Node > addDeq;
               for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
                 Node dv = getCurrentValue( it->first );
                 if( !alreadySet ){
                   if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){
                     d_curr_var_deq[vn][dv] = v;
-                    //addDeq.push_back( dv );
                   }
                 }else{
-                  if( itmn->second!=dv ){
+                  if( !p->areMatchDisequal( itmn->second, dv ) ){
                     Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
                     return -1;
                   }
@@ -1049,7 +1091,7 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
             }else{
               Debug("qcf-match-debug") << "  -> Both variables bound, compare" << std::endl;
               //are they currently equal
-              return itm->second==itmn->second ? 0 : -1;
+              return p->areMatchEqual( itm->second, itmn->second ) ? 0 : -1;
             }
           }
         }else{
@@ -1059,7 +1101,7 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
           }else{
             //compare ground values
             Debug("qcf-match-debug") << "  -> Ground value, compare " << itm->second << " "<< n << std::endl;
-            return itm->second==n ? 0 : -1;
+            return p->areMatchEqual( itm->second, n ) ? 0 : -1;
           }
         }
         if( setMatch( p, v, n ) ){
@@ -1088,7 +1130,8 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
           //check if it respects equality
           std::map< int, Node >::iterator itm = d_match.find( v );
           if( itm!=d_match.end() ){
-            if( getCurrentValue( n )==itm->second ){
+            Node nv = getCurrentValue( n );
+            if( !p->areMatchDisequal( nv, itm->second ) ){
               Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
               return -1;
             }
@@ -1230,13 +1273,14 @@ void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {
   }
 }
 
-
+/*
 struct MatchGenSort {
   QuantConflictFind::MatchGen * d_mg;
   bool operator() (int i,int j) {
     return d_mg->d_children[i].d_type<d_mg->d_children[j].d_type;
   }
 };
+*/
 
 QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){
   Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;
@@ -1255,19 +1299,6 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
       d_type = typ_invalid;
     }
   }else{
-    /*
-    if( isTop && n.getKind()!=OR && p->d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
-      //conjoin extra constraints based on flattening with quantifier body
-      d_children.push_back( MatchGen( p, q, n ) );
-      if( d_children[0].d_type==typ_invalid ){
-        d_children.clear();
-        d_type = typ_invalid;
-      }else{
-        d_type = typ_top;
-      }
-      d_type_not = false;
-    }else
-    */
     if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
       //we handle not immediately
       d_n = n.getKind()==NOT ? n[0] : n;
@@ -1338,56 +1369,20 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
       d_n = n;
       d_type = typ_ground;
     }
-    if( d_type!=typ_invalid ){
+    //if( d_type!=typ_invalid ){
       //determine an efficient children ordering
-      if( !d_children.empty() ){
-        for( unsigned i=0; i<d_children.size(); i++ ){
-          d_children_order.push_back( i );
-        }
+      //if( !d_children.empty() ){
+        //for( unsigned i=0; i<d_children.size(); i++ ){
+        //  d_children_order.push_back( i );
+        //}
         //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){
           //sort based on the type of the constraint : ground comes first, then literals, then others
           //MatchGenSort mgs;
           //mgs.d_mg = this;
           //std::sort( d_children_order.begin(), d_children_order.end(), mgs );
         //}
-      }
-      /*
-      if( isTop ){
-        int base = d_children.size();
-        //add additional constraints based on flattening
-        for( unsigned j=q[0].getNumChildren(); j<p->d_qinfo[q].d_vars.size(); j++ ){
-          d_children.push_back( MatchGen( p, q, p->d_qinfo[q].d_vars[j], false, true ) );
-        }
-
-        //choose variable order for variables based on when they are bound
-        std::vector< int > varOrder;
-        varOrder.insert( varOrder.end(), d_children_order.begin(), d_children_order.end() );
-        d_children_order.clear();
-        std::map< int, bool > bound;
-        for( unsigned i=0; i<varOrder.size(); i++ ){
-          int curr = varOrder[i];
-          Trace("qcf-qregister-debug") << "Var Order : " << curr << std::endl;
-          d_children_order.push_back( curr );
-          for( std::map< int, int >::iterator it = d_children[curr].d_qni_var_num.begin();
-               it != d_children[curr].d_qni_var_num.end(); ++it ){
-            if( it->second>=(int)q[0].getNumChildren() && bound.find( it->second )==bound.end() ){
-              bound[ it->second ] = true;
-              int var = base + it->second - (int)q[0].getNumChildren();
-              d_children_order.push_back( var );
-              Trace("qcf-qregister-debug") << "Var Order, bound : " << var << std::endl;
-            }
-          }
-        }
-        for( unsigned j=q[0].getNumChildren(); j<p->d_qinfo[q].d_vars.size(); j++ ){
-          if( bound.find( j )==bound.end() ){
-            int var = base + j - (int)q[0].getNumChildren();
-            d_children_order.push_back( var );
-            Trace("qcf-qregister-debug") << "Var Order, remaining : " << j << std::endl;
-          }
-        }
-      }
-      */
-    }
+      //}
+    //}
   }
   if( d_type!=typ_invalid ){
     if( !qni_apps.empty() ){
@@ -1411,7 +1406,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
   Trace("qcf-qregister-debug")  << "Done make match gen " << n << ", type = ";
   debugPrintType( "qcf-qregister-debug", d_type, true );
   Trace("qcf-qregister-debug") << std::endl;
-  Assert( d_children.size()==d_children_order.size() );
+  //Assert( d_children.size()==d_children_order.size() );
 }
 
 void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) {
@@ -1435,7 +1430,7 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q
 
   //set up processing matches
   if( d_type==typ_ground ){
-    if( p->evaluate( d_n )==( d_tgt ? 1 : -1 ) ){
+    if( p->evaluate( d_n, d_tgt, true )==( d_tgt ? 1 : -1 ) ){
       //store dummy variable
       d_qn.push_back( NULL );
     }
@@ -1450,18 +1445,18 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q
     if( it!=p->d_qinfo[q].d_match.end() && d_tgt ) {
       Debug("qcf-match") << "       will be matching var within eqc = " << it->second << std::endl;
       //f-applications in the equivalence class in match[ repVar ]
-      std::map< TNode, QcfNodeIndex >::iterator itut = p->d_eqc_uf_terms[ it->second ].find( f );
-      if( itut!=p->d_eqc_uf_terms[ it->second ].end() ){
-        d_qn.push_back( &itut->second );
+      QcfNodeIndex * qni = p->getQcfNodeIndex( it->second, f );
+      if( qni ){
+        d_qn.push_back( qni );
       }
     }else{
       Debug("qcf-match") << "       will be matching var within any eqc." << std::endl;
       //we are binding rep var
       d_qni_bound_cons[repVar] = Node::null();
       //must look at all f-applications
-      std::map< TNode, QcfNodeIndex >::iterator itut = p->d_uf_terms.find( f );
-      if( itut!=p->d_uf_terms.end() ){
-        d_qn.push_back( &itut->second );
+      QcfNodeIndex * qni = p->getQcfNodeIndex( f );
+      if( qni ){
+        d_qn.push_back( qni );
       }
     }
   }else if( d_type==typ_var_eq ){
@@ -1513,6 +1508,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
     bool success = doMatching( p, q );
     if( success ){
       Debug("qcf-match") << "     Produce matches for bound variables..." << std::endl;
+
       //also need to create match for each variable we bound
       std::map< int, int >::iterator it = d_qni_bound.begin();
       bool doReset = true;
@@ -1546,6 +1542,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
         }
       }
     }
+    //if not successful, clean up the variables you bound
     if( !success ){
       for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){
         if( !it->second.isNull() ){
@@ -1580,7 +1577,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
             if( getChild( d_child_counter )->getNextMatch( p, q ) ){
               if( d_child_counter<(int)(getNumChildren()-1) ){
                 d_child_counter++;
-                Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << ", all match " << d_children_order.size() << " " << d_children_order[d_child_counter] << std::endl;
+                Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << std::endl;
                 getChild( d_child_counter )->reset( p, d_tgt, q );
               }else{
                 success = true;
@@ -1724,6 +1721,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
               Debug("qcf-match-debug") << "       Failed to match" << std::endl;
               d_qn.pop_back();
             }
+            //TODO : if it is equal to something else, also try that
           }
         }else{
           Assert( d_qn.size()==d_qni.size() );
@@ -1747,6 +1745,8 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
             }else{
               Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;
             }
+          }else{
+            //TODO : if it equal to something else, also try that
           }
           //if not incrementing, move to next
           if( !success ){
@@ -1928,15 +1928,18 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
 
 QuantConflictFind::Statistics::Statistics():
   d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
-  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 )
+  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),
+  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )
 {
   StatisticsRegistry::registerStat(&d_inst_rounds);
   StatisticsRegistry::registerStat(&d_conflict_inst);
+  StatisticsRegistry::registerStat(&d_prop_inst);
 }
 
 QuantConflictFind::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_inst_rounds);
   StatisticsRegistry::unregisterStat(&d_conflict_inst);
+  StatisticsRegistry::unregisterStat(&d_prop_inst);
 }
 
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 657586d1a..15923b0ba 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -101,7 +101,7 @@ private:  //for ground terms
   std::map< int, std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > > > d_eqr[2];
   EqRegistry * getEqRegistry( bool polarity, Node lit, bool doCreate = true );
   void getEqRegistryApps( Node lit, std::vector< Node >& terms );
-  int evaluate( Node n );
+  int evaluate( Node n, bool pref = false, bool hasPref = false );
 public:  //for quantifiers
   //match generator
   class MatchGen {
@@ -109,9 +109,10 @@ public:  //for quantifiers
     //current children information
     int d_child_counter;
     //children of this object
-    std::vector< int > d_children_order;
+    //std::vector< int > d_children_order;
     unsigned getNumChildren() { return d_children.size(); }
-    MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
+    //MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
+    MatchGen * getChild( int i ) { return &d_children[i]; }
     //current matching information
     std::vector< QcfNodeIndex * > d_qn;
     std::vector< std::map< TNode, QcfNodeIndex >::iterator > d_qni;
@@ -203,6 +204,8 @@ private:  //for equivalence classes
   std::map< TNode, QcfNodeIndex > d_uf_terms;
   // eqc x operator -> index(terms)
   std::map< TNode, std::map< TNode, QcfNodeIndex > > d_eqc_uf_terms;
+  QcfNodeIndex * getQcfNodeIndex( Node eqc, Node f );
+  QcfNodeIndex * getQcfNodeIndex( Node f );
   // type -> list(eqc)
   std::map< TypeNode, std::vector< TNode > > d_eqcs;
   //mapping from UF terms to representatives of their arguments
@@ -211,6 +214,18 @@ private:  //for equivalence classes
   void computeArgReps( TNode n );
   // is this term treated as UF application?
   bool isHandledUfTerm( TNode n );
+public:
+  enum {
+    effort_conflict,
+    effort_propagation,
+  };
+  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:
   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
 
@@ -247,6 +262,7 @@ public:
   public:
     IntStat d_inst_rounds;
     IntStat d_conflict_inst;
+    IntStat d_prop_inst;
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2ddc83a4b..001d8b2b6 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -346,19 +346,28 @@ Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){
   if( n.getKind()==INST_CONSTANT ){
     Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
     return terms[n.getAttribute(InstVarNumAttribute())];
-  }else if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
-    Debug("check-inst") << "No inst const attr : " << n << std::endl;
-    return n;
   }else{
-    Debug("check-inst") << "Recurse on : " << n << std::endl;
+    //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
+      //Debug("check-inst") << "No inst const attr : " << n << std::endl;
+      //return n;
+    //}else{
+      //Debug("check-inst") << "Recurse on : " << n << std::endl;
     std::vector< Node > cc;
     if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
       cc.push_back( n.getOperator() );
     }
+    bool changed = false;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      cc.push_back( doSubstitute( n[i], terms ) );
+      Node c = doSubstitute( n[i], terms );
+      cc.push_back( c );
+      changed = changed || c!=n[i];
+    }
+    if( changed ){
+      Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
+      return ret;
+    }else{
+      return n;
     }
-    return NodeManager::currentNM()->mkNode( n.getKind(), cc );
   }
 }