From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 24 Jan 2014 19:58:52 +0000 (-0600)
Subject: Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry approach... 
X-Git-Tag: cvc5-1.0.0~7129
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f32765c4777a55d0e078aeb575a0811676613fad;p=cvc5.git

Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry approach.  Minor change to quantifier macros.  Add option --quant-cf-mode.
---

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index e3ed8d0e0..c19172b3b 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -195,7 +195,7 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
 }
 
 void InstantiationEngine::check( Theory::Effort e ){
-  if( d_performCheck ){
+  if( d_performCheck && !d_quantEngine->hasAddedLemma() ){
     Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl;
     double clSet = 0;
     if( Trace.isOn("inst-engine") ){
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 600f8c0b9..435bf7221 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -124,7 +124,16 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
 
 void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){
   if( n.getKind()==APPLY_UF ){
-    candidates.push_back( n );
+    bool allBoundVar = true;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( n[i].getKind()!=BOUND_VARIABLE ){
+        allBoundVar = false;
+        break;
+      }
+    }
+    if( allBoundVar ){
+      candidates.push_back( n );
+    }
   }else if( n.getKind()==PLUS ){
     for( size_t i=0; i<n.getNumChildren(); i++ ){
       getMacroCandidates( n[i], candidates );
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 4eb12c98d..c36a565ea 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -73,12 +73,21 @@ typedef enum {
 typedef enum {
   /** default, apply at full effort */
   QCF_WHEN_MODE_DEFAULT,
+  /** apply at last call */
+  QCF_WHEN_MODE_LAST_CALL,
   /** apply at standard effort */
   QCF_WHEN_MODE_STD,
   /** apply based on heuristics */
   QCF_WHEN_MODE_STD_H,
 } QcfWhenMode;
 
+typedef enum {
+  /** default, use qcf for conflicts only */
+  QCF_CONFLICT_ONLY,
+  /** use qcf for conflicts and propagations */
+  QCF_PROP_EQ,
+} QcfMode;
+
 typedef enum {
   /** default, use but do not trust */
   USER_PAT_MODE_DEFAULT,
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index bfb1d6f65..00d3cf234 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -121,6 +121,8 @@ option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode
 
 option quantConflictFind --quant-cf bool :default false
  enable conflict find mechanism for quantifiers
+option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_CONFLICT_ONLY :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h"
+ what effort to apply conflict find mechanism
 option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h"
  when to invoke conflict find mechanism for quantifiers
 
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 5bd710a79..37362982c 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -37,7 +37,8 @@ full-last-call\n\
   call.  In other words, interleave instantiation and theory combination.\n\
 \n\
 last-call\n\
-+ Run instantiation at last call effort, after theory combination.\n\
++ Run instantiation at last call effort, after theory combination and\n\
+  and theories report sat.\n\
 \n\
 ";
 
@@ -103,6 +104,10 @@ Quantifier conflict find modes currently supported by the --quant-cf-when option
 default \n\
 + Default, apply conflict finding at full effort.\n\
 \n\
+last-call \n\
++ Apply conflict finding at last call, after theory combination and \n\
+  and all theories report sat. \n\
+\n\
 std \n\
 + Apply conflict finding at standard effort.\n\
 \n\
@@ -110,6 +115,16 @@ std-h \n\
 + Apply conflict finding at standard effort when heuristic says to. \n\
 \n\
 ";
+static const std::string qcfModeHelp = "\
+Quantifier conflict find modes currently supported by the --quant-cf option:\n\
+\n\
+conflict \n\
++ Default, apply conflict finding for finding conflicts only.\n\
+\n\
+prop-eq \n\
++ Apply conflict finding to propagate equalities as well. \n\
+\n\
+";
 static const std::string userPatModeHelp = "\
 User pattern modes currently supported by the --user-pat option:\n\
 \n\
@@ -215,6 +230,8 @@ inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) thr
 inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg ==  "default") {
     return QCF_WHEN_MODE_DEFAULT;
+  } else if(optarg ==  "last-call") {
+    return QCF_WHEN_MODE_LAST_CALL;
   } else if(optarg ==  "std") {
     return QCF_WHEN_MODE_STD;
   } else if(optarg ==  "std-h") {
@@ -227,6 +244,19 @@ inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, S
                           optarg + "'.  Try --quant-cf-when help.");
   }
 }
+inline QcfMode stringToQcfMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "default" || optarg ==  "conflict") {
+    return QCF_CONFLICT_ONLY;
+  } else if(optarg ==  "prop-eq") {
+    return QCF_PROP_EQ;
+  } else if(optarg ==  "help") {
+    puts(qcfModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --quant-cf-mode: `") +
+                          optarg + "'.  Try --quant-cf-mode help.");
+  }
+}
 
 inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg ==  "default") {
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 66191107d..198ec3bbf 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -35,10 +35,11 @@ Node QcfNodeIndex::existsTerm( TNode n, std::vector< TNode >& reps, int index )
       return d_children.begin()->first;
     }
   }else{
-    if( d_children.find( reps[index] )==d_children.end() ){
+    std::map< TNode, QcfNodeIndex >::iterator it = d_children.find( reps[index] );
+    if( it==d_children.end() ){
       return Node::null();
     }else{
-      return d_children[reps[index]].existsTerm( n, reps, index+1 );
+      return it->second.existsTerm( n, reps, index+1 );
     }
   }
 }
@@ -56,16 +57,6 @@ Node QcfNodeIndex::addTerm( TNode n, std::vector< TNode >& reps, int index ) {
   }
 }
 
-bool QcfNodeIndex::addTermEq( TNode n1, TNode n2, std::vector< TNode >& reps1, std::vector< TNode >& reps2, int index ) {
-  if( index==(int)reps1.size() ){
-    Node n = addTerm( n2, reps2 );
-    return n==n2;
-  }else{
-    return d_children[reps1[index]].addTermEq( n1, n2, reps1, reps2, index+1 );
-  }
-}
-
-
 
 void QcfNodeIndex::debugPrint( const char * c, int t ) {
   for( std::map< TNode, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
@@ -77,19 +68,6 @@ void QcfNodeIndex::debugPrint( const char * c, int t ) {
   }
 }
 
-EqRegistry::EqRegistry( context::Context* c ) : d_active( c, false ){//: d_t_eqc( c ){
-
-}
-
-void EqRegistry::debugPrint( const char * c, int t ) {
-  d_qni.debugPrint( c, t );
-}
-
-//QcfNode::QcfNode( context::Context* c ) : d_parent( NULL ){
-//  d_reg[0] = NULL;
-//  d_reg[1] = NULL;
-//}
-
 QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
 QuantifiersModule( qe ),
 d_c( c ),
@@ -98,39 +76,6 @@ d_qassert( c ) {
   d_fid_count = 0;
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
-  getFunctionId( d_true );
-  getFunctionId( d_false );
-}
-
-int QuantConflictFind::getFunctionId( Node f ) {
-  std::map< Node, int >::iterator it = d_fid.find( f );
-  if( it==d_fid.end() ){
-    d_fid[f] = d_fid_count;
-    d_fid_count++;
-    return d_fid[f];
-  }
-  return it->second;
-}
-
-bool QuantConflictFind::isLessThan( Node a, Node b ) {
-  //Assert( a.getKind()==APPLY_UF );
-  //Assert( b.getKind()==APPLY_UF );
-  /*
-  if( a.getOperator()==b.getOperator() ){
-    for( unsigned i=0; i<a.getNumChildren(); i++ ){
-      Node acr = getRepresentative( a[i] );
-      Node bcr = getRepresentative( b[i] );
-      if( acr<bcr ){
-        return true;
-      }else if( acr>bcr ){
-        return false;
-      }
-    }
-    return false;
-  }else{
-    */
-  return getFunctionId( a )<getFunctionId( b );
-  //}
 }
 
 Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {
@@ -159,15 +104,6 @@ Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {
   }
 }
 
-Node QuantConflictFind::getFv( TypeNode tn ) {
-  if( d_fv.find( tn )==d_fv.end() ){
-    std::stringstream ss;
-    ss << "_u";
-    d_fv[tn] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is for QCF" );
-  }
-  return d_fv[tn];
-}
-
 Node QuantConflictFind::mkEqNode( Node a, Node b ) {
   if( a.getType().isBoolean() ){
     return a.iffNode( b );
@@ -178,47 +114,36 @@ Node QuantConflictFind::mkEqNode( Node a, Node b ) {
 
 //-------------------------------------------------- registration
 
-/*
-void QuantConflictFind::registerAssertions( std::vector< Node >& assertions ) {
-  for( unsigned i=0; i<assertions.size(); i++ ){
-    registerAssertion( assertions[i] );
-  }
-}
-
-void QuantConflictFind::registerAssertion( Node n ) {
-  if( n.getKind()==FORALL ){
-    registerNode( Node::null(), n[1], NULL, true, true );
-  }else{
-    if( n.getType().isBoolean() ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        registerAssertion( n[i] );
-      }
-    }
-  }
-}
-*/
 void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {
   //qcf->d_node = n;
   bool recurse = true;
   if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){
     if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
       //literals
-      for( unsigned i=0; i<2; i++ ){
-        if( !hasPol || ( pol!=(i==0) ) ){
-          EqRegistry * eqr = getEqRegistry( i==0, n );
-          if( eqr ){
-            d_qinfo[q].d_rel_eqr[ eqr ] = true;
+
+      /*
+        if( n.getKind()==APPLY_UF || ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){
+            flatten( q, n[i] );
+          }
+        }else if( n.getKind()==EQUAL ){
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){
+            for( unsigned j=0; j<n[i].getNumChildren(); j++ ){
+              flatten( q, n[i][j] );
+            }
           }
         }
-      }
-      if( n.getKind()==APPLY_UF ||
-          ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){
+
+        */
+
+      if( n.getKind()==APPLY_UF ){
         flatten( q, n );
-      }else{
+      }else if( n.getKind()==EQUAL ){
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           flatten( q, n[i] );
         }
       }
+
     }else{
       Trace("qcf-qregister") << "    RegisterGroundLit : " << n;
     }
@@ -238,14 +163,14 @@ void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {
 }
 
 void QuantConflictFind::flatten( Node q, Node n ) {
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    if( quantifiers::TermDb::hasBoundVarAttr( n[i] ) && n.getKind()!=BOUND_VARIABLE ){
-      if( d_qinfo[q].d_var_num.find( n[i] )==d_qinfo[q].d_var_num.end() ){
-        //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;
-        d_qinfo[q].d_var_num[n[i]] = d_qinfo[q].d_vars.size();
-        d_qinfo[q].d_vars.push_back( n[i] );
-        flatten( q, n[i] );
-      }
+  if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){
+    if( d_qinfo[q].d_var_num.find( n )==d_qinfo[q].d_var_num.end() ){
+      //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;
+      d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();
+      d_qinfo[q].d_vars.push_back( n );
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      flatten( q, n[i] );
     }
   }
 }
@@ -296,82 +221,31 @@ void QuantConflictFind::registerQuantifier( Node q ) {
   Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
 }
 
-EqRegistry * QuantConflictFind::getEqRegistry( bool polarity, Node lit, bool doCreate ) {
-  Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) );
-  int i;
-  Node f1;
-  Node f2;
-  int f1Index;
-  int f2Index;
-  if( lit.getKind()==EQUAL ){
-    i = polarity ? 0 : 1;
-    f1 = getFunction( lit[0], f1Index, true );
-    f2 = getFunction( lit[1], f2Index, true );
-  }else if( lit.getKind()==APPLY_UF ){
-    i = 0;
-    f1 = getFunction( lit, f1Index, true );
-    f2 = polarity ? d_true : d_false;
-    f2Index = 0;
-  }
-  if( !f1.isNull() && !f2.isNull() ){
-    if( d_eqr[i][f1Index][f1][f2Index].find( f2 )==d_eqr[i][f1Index][f1][f2Index].end() ){
-      if( doCreate ){
-        Trace("qcf-register") << "RegisterEqr : " << f1 << " " << f2 << ", polarity = " << (i==0) << ", indices : " << f1Index << " " << f2Index << std::endl;
-        d_eqr[i][f1Index][f1][f2Index][f2] = new EqRegistry( d_c );
-        d_eqr[i][f2Index][f2][f1Index][f1] = d_eqr[i][f1Index][f1][f2Index][f2];
-      }else{
-        return NULL;
-      }
-    }
-    return d_eqr[i][f1Index][f1][f2Index][f2];
-  }else{
-    return NULL;
-  }
-}
-
-void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms ) {
-  Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) );
-  if( lit.getKind()==EQUAL ){
-    for( unsigned i=0; i<2; i++ ){
-      if( quantifiers::TermDb::hasBoundVarAttr( lit[i] ) ){
-        if( lit[i].getKind()==BOUND_VARIABLE ){
-          //do not handle variable equalities
-          terms.clear();
-          return;
-        }else{
-          terms.push_back( lit[i] );
-        }
-      }
-    }
-    if( terms.size()==2 && isLessThan( terms[1].getOperator(), terms[0].getOperator() ) ){
-      Node t = terms[0];
-      terms[0] = terms[1];
-      terms[1] = t;
-    }
-  }else if( lit.getKind()==APPLY_UF ){
-    terms.push_back( lit );
-  }
-}
-
 int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
   int ret = 0;
   if( n.getKind()==EQUAL ){
-    Node n1 = getTerm( n[0] );
-    Node n2 = getTerm( n[1] );
+    Node n1 = evaluateTerm( n[0] );
+    Node n2 = evaluateTerm( n[1] );
     Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;
     if( areEqual( n1, n2 ) ){
       ret = 1;
     }else if( areDisequal( n1, n2 ) ){
       ret = -1;
     }
+    //else if( d_effort>QuantConflictFind::effort_conflict ){
+    //  ret = -1;
+    //}
   }else if( n.getKind()==APPLY_UF ){  //predicate
-    Node nn = getTerm( n );
+    Node nn = evaluateTerm( n );
     Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;
     if( areEqual( nn, d_true ) ){
       ret = 1;
     }else if( areEqual( nn, d_false ) ){
       ret = -1;
     }
+    //else if( d_effort>QuantConflictFind::effort_conflict ){
+    //  ret = -1;
+    //}
   }else if( n.getKind()==NOT ){
     return -evaluate( n[0] );
   }else if( n.getKind()==ITE ){
@@ -430,26 +304,19 @@ bool QuantConflictFind::isPropagationSet() {
 }
 
 bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
+  //if( d_effort==QuantConflictFind::effort_prop_deq ){
+  //  return n1==n2 || !areDisequal( n1, n2 );
+  //}else{
   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 );
-  }
-  */
+  //if( d_effort==QuantConflictFind::effort_conflict ){
+  //  return areDisequal( n1, n2 );
+  //}else{
+  return n1!=n2;
+  //}
 }
 
 //-------------------------------------------------- handling assertions / eqc
@@ -460,9 +327,9 @@ void QuantConflictFind::assertNode( Node q ) {
   Trace("qcf-proc") << std::endl;
   d_qassert.push_back( q );
   //set the eqRegistries that this depends on to true
-  for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){
-    it->first->d_active.set( true );
-  }
+  //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){
+  //  it->first->d_active.set( true );
+  //}
 }
 
 eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {
@@ -482,17 +349,32 @@ Node QuantConflictFind::getRepresentative( Node n ) {
     return n;
   }
 }
-Node QuantConflictFind::getTerm( Node n ) {
+Node QuantConflictFind::evaluateTerm( Node n ) {
   if( isHandledUfTerm( n ) ){
-    computeArgReps( n );
-    Node nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );
+    Node nn;
+    if( getEqualityEngine()->hasTerm( n ) ){
+      computeArgReps( n );
+      nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );
+    }else{
+      std::vector< TNode > args;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node c = evaluateTerm( n[i] );
+        args.push_back( c );
+      }
+      nn = d_uf_terms[n.getOperator()].existsTerm( n, args );
+    }
     if( !nn.isNull() ){
-      return nn;
+      Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;
+      return getRepresentative( nn );
+    }else{
+      Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;
+      return n;
     }
   }
-  return n;
+  return getRepresentative( n );
 }
 
+/*
 QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {
   std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );
   if( it2==d_eqc_info.end() ){
@@ -506,13 +388,23 @@ 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{
+  std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms.find( f );
+  if( itut==d_eqc_uf_terms.end() ){
     return NULL;
+  }else{
+    if( eqc.isNull() ){
+      return &itut->second;
+    }else{
+      std::map< TNode, QcfNodeIndex >::iterator itute = itut->second.d_children.find( eqc );
+      if( itute!=itut->second.d_children.end() ){
+        return &itute->second;
+      }else{
+        return NULL;
+      }
+    }
   }
 }
 
@@ -527,13 +419,13 @@ QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {
 
 /** new node */
 void QuantConflictFind::newEqClass( Node n ) {
-  Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;
-
-  Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;
+  //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;
+  //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;
 }
 
 /** merge */
 void QuantConflictFind::merge( Node a, Node b ) {
+  /*
   if( b.getKind()==EQUAL ){
     if( a==d_true ){
       //will merge anyways
@@ -562,23 +454,23 @@ void QuantConflictFind::merge( Node a, Node b ) {
           eqc_n->setDisequal( b, false );
         }
       }
-      /*
-      //move all previous EqcRegistry's regarding equalities within b
-      for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){
-        if( (*it).second ){
-          eqc_a->d_rel_eqr_e[(*it).first] = true;
-        }
-      }
-      */
+      ////move all previous EqcRegistry's regarding equalities within b
+      //for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){
+      //  if( (*it).second ){
+      //    eqc_a->d_rel_eqr_e[(*it).first] = true;
+      //  }
+      //}
     }
     //process new equalities
     //setEqual( eqc_a, eqc_b, a, b, true );
     Trace("qcf-proc2") << "QCF : finished merge : " << a << " " << b << std::endl;
   }
+  */
 }
 
 /** assert disequal */
 void QuantConflictFind::assertDisequal( Node a, Node b ) {
+  /*
   a = getRepresentative( a );
   b = getRepresentative( b );
   Trace("qcf-proc") << "QCF : assert disequal : " << a << " " << b << std::endl;
@@ -591,6 +483,7 @@ void QuantConflictFind::assertDisequal( Node a, Node b ) {
     //setEqual( eqc_a, eqc_b, a, b, false );
   }
   Trace("qcf-proc2") << "QCF : finished assert disequal : " << a << " " << b << std::endl;
+  */
 }
 
 //-------------------------------------------------- check function
@@ -620,15 +513,15 @@ void QuantConflictFind::check( Theory::Effort level ) {
         debugPrint("qcf-debug");
         Trace("qcf-debug") << std::endl;
       }
-
-      for( short e = effort_conflict; e<=effort_conflict; e++ ){
+      short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;
+      for( short e = effort_conflict; e<=end_e; e++ ){
         d_effort = e;
-        if( e == effort_propagation ){
+        if( e == effort_prop_eq ){
           for( unsigned i=0; i<2; i++ ){
             d_prop_eq[i] = Node::null();
           }
         }
-        Trace("qcf-check") << "Checking quantified formulas..." << std::endl;
+        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];
           Trace("qcf-check") << "Check quantified formula ";
@@ -642,7 +535,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
             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;
+              Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
               d_qinfo[q].debugPrintMatch("qcf-check");
               Trace("qcf-check") << std::endl;
 
@@ -651,14 +544,27 @@ void QuantConflictFind::check( Theory::Effort level ) {
                 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] );
+                    //Node cv = d_qinfo[q].getCurrentValue( d_qinfo[q].d_match[i] );
+                    int repVar = d_qinfo[q].getCurrentRepVar( i );
+                    Node cv;
+                    std::map< int, Node >::iterator itmt = d_qinfo[q].d_match_term.find( repVar );
+                    if( itmt!=d_qinfo[q].d_match_term.end() ){
+                      cv = itmt->second;
+                    }else{
+                      cv = d_qinfo[q].d_match[repVar];
+                    }
+
+
                     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") ){
+                    //if( e==effort_conflict ){
                     Node inst = d_quantEngine->getInstantiation( q, m );
                     Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
-                    Assert( evaluate( inst )==-1 );
+                    Assert( evaluate( inst )!=1 );
+                    Assert( evaluate( inst )==-1 || e>effort_conflict );
+                    //}
                   }
                   if( d_quantEngine->addInstantiation( q, m ) ){
                     Trace("qcf-check") << "   ... Added instantiation" << std::endl;
@@ -667,7 +573,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
                       d_conflict.set( true );
                       ++(d_statistics.d_conflict_inst);
                       break;
-                    }else if( e==effort_propagation ){
+                    }else if( e==effort_prop_eq ){
                       ++(d_statistics.d_prop_inst);
                     }
                   }else{
@@ -690,13 +596,19 @@ void QuantConflictFind::check( Theory::Effort level ) {
             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();
+          break;
+        }
+      }
+      if( Trace.isOn("qcf-engine") ){
+        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+        Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
+        if( addedLemmas>0 ){
+          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "prop_deq" ) );
+          Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
         }
+        Trace("qcf-engine") << std::endl;
       }
     }
     Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
@@ -706,7 +618,9 @@ void QuantConflictFind::check( Theory::Effort level ) {
 bool QuantConflictFind::needsCheck( Theory::Effort level ) {
   d_performCheck = false;
   if( !d_conflict ){
-    if( level==Theory::EFFORT_FULL ){
+    if( level==Theory::EFFORT_LAST_CALL ){
+      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
+    }else if( level==Theory::EFFORT_FULL ){
       d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
     }else if( level==Theory::EFFORT_STANDARD ){
       d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
@@ -716,18 +630,6 @@ bool QuantConflictFind::needsCheck( Theory::Effort level ) {
 }
 
 void QuantConflictFind::computeRelevantEqr() {
-  //first, reset information
-  for( unsigned i=0; i<2; i++ ){
-    for( unsigned j=0; j<2; j++ ){
-      for( std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > >::iterator it = d_eqr[i][j].begin(); it != d_eqr[i][j].end(); ++it ){
-        for( unsigned jj=0; jj<2; jj++ ){
-          for( std::map< TNode, EqRegistry * >::iterator it2 = it->second[jj].begin(); it2 != it->second[jj].end(); ++it2 ){
-            it2->second->clear();
-          }
-        }
-      }
-    }
-  }
   d_uf_terms.clear();
   d_eqc_uf_terms.clear();
   d_eqcs.clear();
@@ -740,13 +642,6 @@ void QuantConflictFind::computeRelevantEqr() {
   long nTermst = 0;
   long nTerms = 0;
   long nEqc = 0;
-  long nEq1 = 0;
-  long nEq2 = 0;
-  long nEq1t = 0;
-  long nEq2t = 0;
-  long nComp = 0;
-  //relevant nodes for eq registries
-  std::map< TNode, std::map< TNode, std::vector< TNode > > > eqr_to_node[2];
 
   //which nodes are irrelevant for disequality matches
   std::map< TNode, bool > irrelevant_dnode;
@@ -756,8 +651,9 @@ void QuantConflictFind::computeRelevantEqr() {
     nEqc++;
     Node r = (*eqcs_i);
     d_eqcs[r.getType()].push_back( r );
-    EqcInfo * eqcir = getEqcInfo( r, false );
+    //EqcInfo * eqcir = getEqcInfo( r, false );
     //get relevant nodes that we are disequal from
+    /*
     std::vector< Node > deqc;
     if( eqcir ){
       for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){
@@ -771,8 +667,7 @@ void QuantConflictFind::computeRelevantEqr() {
         }
       }
     }
-    //the relevant nodes in this eqc
-    std::vector< Node > eqc;
+    */
     //process disequalities
     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
     while( !eqc_i.isFinished() ){
@@ -793,7 +688,7 @@ void QuantConflictFind::computeRelevantEqr() {
           computeArgReps( n );
           it_na = d_arg_reps.find( n );
           Assert( it_na!=d_arg_reps.end() );
-          Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( n, d_arg_reps[n] );
+          Node nadd = d_eqc_uf_terms[n.getOperator()].d_children[r].addTerm( n, d_arg_reps[n] );
           isRedundant = (nadd!=n);
           d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );
           if( !isRedundant ){
@@ -804,102 +699,6 @@ void QuantConflictFind::computeRelevantEqr() {
           isRedundant = false;
         }
         nTerms += isRedundant ? 0 : 1;
-
-        Trace("qcf-reqr") << "^ Process " << n << std::endl;
-        //process all relevant equalities and disequalities to n
-        for( unsigned index=0; index<2; index++ ){
-          std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > >::iterator itn[2];
-          itn[0] = d_eqr[index][0].find( n );
-          if( !fn.isNull() ){
-            itn[1] = d_eqr[index][1].find( fn );
-          }
-          //for n, fn...
-          bool relevant = false;
-          for( unsigned j=0; j<2; j++ ){
-            //if this node is relevant as an ground term or f-application
-            if( ( j==0 || !fn.isNull() ) && itn[j]!=d_eqr[index][j].end() ){
-              relevant = true;
-              for( unsigned jj=0; jj<2; jj++ ){
-                if( j==1 || jj==1 ){
-                  Trace("qcf-reqr") << "^^ " << index << " " << j << " " << jj << std::endl;
-                  //check with others
-                  for( std::map< TNode, EqRegistry * >::iterator itm = itn[j]->second[jj].begin(); itm != itn[j]->second[jj].end(); ++itm ){
-                    std::map< TNode, std::map< TNode, std::vector< TNode > > >::iterator itv = eqr_to_node[index].find( itm->first );
-                    if( itv!=eqr_to_node[index].end() ){
-                      //for( unsigned k=0; k<itv->second.size(); k++ ){
-                      for( std::map< TNode, std::vector< TNode > >::iterator itvr = itv->second.begin(); itvr != itv->second.end(); ++itvr ){
-                        TNode mr = itvr->first;
-                        //Assert( j==0 || getFunction( m )==itm->first );
-                        nComp++;
-                        //if it is equal or disequal to this
-                        if( ( index==0 && mr==r ) ||
-                            ( index==1 && std::find( deqc.begin(), deqc.end(), mr )!=deqc.end() ) ){
-                          Debug("qcf-reqr") << "^^ Check with : " << itv->first << ", # = " << itvr->second.size() << std::endl;
-                          for( unsigned k=0; k<itvr->second.size(); k++ ){
-                            TNode m = itvr->second[k];
-                            Debug("qcf-reqr") << "Comparing " << n << " and " << m << ", j = " << j << ", index = " << index << std::endl;
-                            Debug("qcf-reqr") << "Meets the criteria of " << itn[j]->first << " " << itm->first << std::endl;
-                            //process equality/disequality
-                            if( j==0 ){
-                              Assert( d_arg_reps.find( m )!=d_arg_reps.end() );
-                              //n with fm
-                              nEq1t++;
-                              if( itm->second->d_qni.addTerm( m, d_arg_reps[m] )==m ){
-                                nEq1++;
-                                Debug("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";
-                                Debug("qcf-reqr") << n << " " << itm->first << std::endl;
-                              }
-                            }else{
-                              if( jj==0 ){
-                                //fn with m
-                                nEq1t++;
-                                if( itm->second->d_qni.addTerm( n, it_na->second )==n ){
-                                  nEq1++;
-                                  Debug("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";
-                                  Debug("qcf-reqr") << fn << " " << m << std::endl;
-                                }
-                              }else{
-                                Assert( d_arg_reps.find( m )!=d_arg_reps.end() );
-                                //fn with fm
-                                bool mltn = isLessThan( itm->first, fn );
-                                for( unsigned i=0; i<2; i++ ){
-                                  if( i==0 || itm->first==fn ){
-                                    TNode am = ((i==0)==mltn) ? n : m;
-                                    TNode an = ((i==0)==mltn) ? m : n;
-                                    nEq2t++;
-                                    if( itm->second->d_qni.addTermEq( an, am, it_na->second, d_arg_reps[m] ) ){
-                                      nEq2++;
-                                      Debug("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for ";
-                                      Debug("qcf-reqr") << fn << " " << itm->first << std::endl;
-                                    }
-                                  }
-                                }
-                              }
-                            }
-                          }
-                        }
-                      }
-                    }
-                  }
-                }
-              }
-              Trace("qcf-reqr") << "- Node " << n << " is relevant for " << (j==0 ? n : fn) << ", index = " << index << std::endl;
-              //add it to relevant
-              eqr_to_node[index][j==0 ? n : fn][r].push_back( n );
-            }
-          }
-          if( !relevant ){
-            //if not relevant for disequalities, store it
-            if( index==1 ){
-              irrelevant_dnode[n] = true;
-            }
-          }else{
-            //if relevant for equalities, store it
-            if( index==0 ){
-              eqc.push_back( n );
-            }
-          }
-        }
       }
       ++eqc_i;
     }
@@ -911,9 +710,6 @@ void QuantConflictFind::computeRelevantEqr() {
     Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
     Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;
     Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;
-    Trace("qcf-opt") << "   " << nEq1 << " / " << nEq1t << " pattern terms." << std::endl;
-    Trace("qcf-opt") << "   " << nEq2 << " / " << nEq2t << " pattern equalities." << std::endl;
-    Trace("qcf-opt") << "   " << nComp << " compares." << std::endl;
     Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;
   }
 }
@@ -932,6 +728,7 @@ bool QuantConflictFind::isHandledUfTerm( TNode n ) {
 
 void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {
   d_match.clear();
+  d_match_term.clear();
   d_curr_var_deq.clear();
   //add built-in variable constraints
   for( unsigned r=0; r<2; r++ ){
@@ -990,16 +787,16 @@ Node QuantConflictFind::QuantInfo::getCurrentValue( Node n ) {
   }
 }
 
-bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n ) {
+bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n, bool chDiseq ) {
   //check disequalities
   for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].end(); ++it ){
     Node cv = getCurrentValue( it->first );
     Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
     if( cv==n ){
       return false;
-    }else if( !isVar( n ) && !isVar( cv ) ){
-      //they must actually be disequal
-      if( !p->areMatchDisequal( n, cv ) ){
+    }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){
+      //they must actually be disequal if we are looking for conflicts
+      if( !p->areDisequal( n, cv ) ){
         return false;
       }
     }
@@ -1148,6 +945,31 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
   }
 }
 
+bool QuantConflictFind::QuantInfo::isConstrainedVar( int v ) {
+  //if( options::qcfMode()==QCF_CONFLICT_ONLY ){
+  //  return true;
+  //}else{
+    if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){
+      return true;
+    }else{
+      Node vv = getVar( v );
+      for( std::map< int, Node >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
+        if( it->second==vv ){
+          return true;
+        }
+      }
+      for( std::map< int, std::map< Node, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){
+        for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+          if( it2->first==vv ){
+            return true;
+          }
+        }
+      }
+      return false;
+    }
+  //}
+}
+
 bool QuantConflictFind::QuantInfo::setMatch( QuantConflictFind * p, int v, Node n ) {
   if( getCurrentCanBeEqual( p, v, n ) ){
     Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " <<  d_curr_var_deq[v].size() << " disequalities" << std::endl;
@@ -1162,7 +984,7 @@ bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   for( int i=0; i<getNumVars(); i++ ){
     std::map< int, Node >::iterator it = d_match.find( i );
     if( it!=d_match.end() ){
-      if( !getCurrentCanBeEqual( p, i, it->second ) ){
+      if( !getCurrentCanBeEqual( p, i, it->second, p->d_effort==QuantConflictFind::effort_conflict ) ){
         return true;
       }
     }
@@ -1190,42 +1012,62 @@ bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q,
       Trace("qcf-check") << "Assign to unassigned, rep = " << r << "..." << std::endl;
       int index = 0;
       std::vector< int > eqc_count;
+      bool doFail = false;
       do {
-        bool invalidMatch;
-        while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch ){
+        bool invalidMatch = false;
+        while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch || doFail ){
           invalidMatch = false;
-          if( index==(int)eqc_count.size() ){
+          if( !doFail && index==(int)eqc_count.size() ){
             //check if it has now been assigned
             if( r==0 ){
-              d_var_mg[ unassigned[r][index] ]->reset( p, true, q );
+              if( !isConstrainedVar( unassigned[r][index] ) ){
+                eqc_count.push_back( -1 );
+              }else{
+                d_var_mg[ unassigned[r][index] ]->reset( p, true, q );
+                eqc_count.push_back( 0 );
+              }
+            }else{
+              eqc_count.push_back( 0 );
             }
-            eqc_count.push_back( 0 );
           }else{
             if( r==0 ){
-              if( d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){
-                Trace("qcf-check-unassign") << "Succeeded match with mg" << std::endl;
+              if( !doFail && !isConstrainedVar( unassigned[r][index] ) ){
+                Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << index << std::endl;
+                index++;
+              }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){
+                Trace("qcf-check-unassign") << "Succeeded match with mg at " << index << std::endl;
                 index++;
               }else{
-                Trace("qcf-check-unassign") << "Failed match with mg" << std::endl;
-                eqc_count.pop_back();
-                index--;
+                Trace("qcf-check-unassign") << "Failed match with mg at " << index << std::endl;
+                do{
+                  if( !doFail ){
+                    eqc_count.pop_back();
+                  }else{
+                    doFail = false;
+                  }
+                  index--;
+                }while( index>=0 && eqc_count[index]==-1 );
               }
             }else{
               Assert( index==(int)eqc_count.size()-1 );
-              if( eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){
+              if( !doFail && eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){
                 int currIndex = eqc_count[index];
                 eqc_count[index]++;
                 Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl;
                 if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){
-                  Trace("qcf-check-unassign") << "Succeeded match" << std::endl;
+                  Trace("qcf-check-unassign") << "Succeeded match " << index << std::endl;
                   index++;
                 }else{
-                  Trace("qcf-check-unassign") << "Failed match" << std::endl;
+                  Trace("qcf-check-unassign") << "Failed match " << index << std::endl;
                   invalidMatch = true;
                 }
               }else{
-                Trace("qcf-check-unassign") << "No more matches" << std::endl;
-                eqc_count.pop_back();
+                Trace("qcf-check-unassign") << "No more matches " << index << std::endl;
+                if( !doFail ){
+                  eqc_count.pop_back();
+                }else{
+                  doFail = false;
+                }
                 index--;
               }
             }
@@ -1233,11 +1075,13 @@ bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q,
         }
         success = index>=0;
         if( success ){
-          index = (int)unassigned[r].size()-1;
+          doFail = true;
           Trace("qcf-check-unassign") << "  Try: " << std::endl;
           for( unsigned i=0; i<unassigned[r].size(); i++ ){
             int ui = unassigned[r][i];
-            Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
+            if( d_match.find( ui )!=d_match.end() ){
+              Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
+            }
           }
         }
       }while( success && isMatchSpurious( p ) );
@@ -1289,11 +1133,23 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
   if( isVar ){
     Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() );
     if( p->isHandledUfTerm( n ) ){
+      d_qni_var_num[0] = p->d_qinfo[q].getVarNum( n );
+      d_qni_size++;
       d_type = typ_var;
-      //d_type_not = true;  //implicit disequality, in disjunction at top level
       d_type_not = false;
       d_n = n;
-      qni_apps.push_back( n );
+      for( unsigned j=0; j<d_n.getNumChildren(); j++ ){
+        Node nn = d_n[j];
+        Trace("qcf-qregister-debug") << "  " << d_qni_size;
+        if( p->d_qinfo[q].isVar( nn ) ){
+          Trace("qcf-qregister-debug") << " is var #" << p->d_qinfo[q].d_var_num[nn] << std::endl;
+          d_qni_var_num[d_qni_size] = p->d_qinfo[q].d_var_num[nn];
+        }else{
+          Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
+          d_qni_gterm[d_qni_size] = nn;
+        }
+        d_qni_size++;
+      }
     }else{
       //for now, unknown term
       d_type = typ_invalid;
@@ -1305,13 +1161,15 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
       d_type_not = n.getKind()==NOT;
       if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE ){
         //non-literals
-        d_type = typ_valid;
+        d_type = typ_formula;
         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
           d_children.push_back( MatchGen( p, q, d_n[i] ) );
           if( d_children[d_children.size()-1].d_type==typ_invalid ){
             setInvalid();
             break;
-          }else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){
+          }
+          /*
+          else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){
             Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl;
             //if variable equality/disequality at top level, remove immediately
             bool cIsNot = d_children[d_children.size()-1].d_type_not;
@@ -1329,39 +1187,21 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
             }
             d_children.pop_back();
           }
+          */
         }
       }else{
         d_type = typ_invalid;
         //literals
-        if( d_n.getKind()==APPLY_UF || d_n.getKind()==EQUAL ){
-          //get the applications (in order) that will be matching
-          p->getEqRegistryApps( d_n, qni_apps );
-          bool isValid = true;
-          if( qni_apps.size()>0 ){
-            for( unsigned i=0; i<qni_apps.size(); i++ ){
-              if( !p->isHandledUfTerm( qni_apps[i] ) ){
-                //for now, cannot handle anything besides uf
-                isValid = false;
-                qni_apps.clear();
-                break;
-              }
-            }
-            if( isValid ){
-              d_type = typ_valid_lit;
-            }
-          }else if( d_n.getKind()==EQUAL ){
-            for( unsigned i=0; i<2; i++ ){
-              if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) && !p->d_qinfo[q].isVar( d_n[i] ) ){
-                isValid = false;
-                break;
-              }
-            }
-            if( isValid ){
-              Assert( p->d_qinfo[q].isVar( d_n[0] ) || p->d_qinfo[q].isVar( d_n[1] ) );
-              // variable equality
-              d_type = typ_var_eq;
+        if( d_n.getKind()==APPLY_UF ){
+          Assert( p->d_qinfo[q].isVar( d_n ) );
+          d_type = typ_pred;
+        }else if( d_n.getKind()==EQUAL ){
+          for( unsigned i=0; i<2; i++ ){
+            if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){
+              Assert( p->d_qinfo[q].isVar( d_n[i] ) );
             }
           }
+          d_type = typ_eq;
         }
       }
     }else{
@@ -1384,37 +1224,33 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
       //}
     //}
   }
-  if( d_type!=typ_invalid ){
-    if( !qni_apps.empty() ){
-      Trace("qcf-qregister-debug") << "Initialize matching..." << std::endl;
-      for( unsigned i=0; i<qni_apps.size(); i++ ){
-        for( unsigned j=0; j<qni_apps[i].getNumChildren(); j++ ){
-          Node nn = qni_apps[i][j];
-          Trace("qcf-qregister-debug") << "  " << d_qni_size;
-          if( p->d_qinfo[q].isVar( nn ) ){
-            Trace("qcf-qregister-debug") << " is var #" << p->d_qinfo[q].d_var_num[nn] << std::endl;
-            d_qni_var_num[d_qni_size] = p->d_qinfo[q].d_var_num[nn];
-          }else{
-            Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
-            d_qni_gterm[d_qni_size] = nn;
-          }
-          d_qni_size++;
-        }
-      }
-    }
-  }
   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() );
 }
 
+
 void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) {
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    d_children[i].reset_round( p );
+  }
   for( std::map< int, Node >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
     d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
   }
-  for( unsigned i=0; i<d_children.size(); i++ ){
-    d_children[i].reset_round( p );
+  if( d_type==typ_ground ){
+    int e = p->evaluate( d_n );
+    if( e==1 ){
+      d_ground_eval[0] = p->d_true;
+    }else if( e==-1 ){
+      d_ground_eval[0] = p->d_false;
+    }
+  }else if( d_type==typ_eq ){
+    for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
+      if( !quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){
+        d_ground_eval[i] = p->evaluateTerm( d_n[i] );
+      }
+    }
   }
 }
 
@@ -1430,63 +1266,67 @@ 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, true )==( d_tgt ? 1 : -1 ) ){
-      //store dummy variable
-      d_qn.push_back( NULL );
+    if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){
+      d_child_counter = 0;
     }
   }else if( d_type==typ_var ){
-    //check if variable is bound by now
-    int vi = p->d_qinfo[q].getVarNum( d_n );
-    Assert( vi!=-1 );
-    int repVar = p->d_qinfo[q].getCurrentRepVar( vi );
     Assert( p->isHandledUfTerm( d_n ) );
     Node f = d_n.getOperator();
-    std::map< int, Node >::iterator it = p->d_qinfo[q].d_match.find( repVar );
-    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 ]
-      QcfNodeIndex * qni = p->getQcfNodeIndex( it->second, f );
-      if( qni ){
-        d_qn.push_back( qni );
-      }
+    Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;
+    QcfNodeIndex * qni = p->getQcfNodeIndex( Node::null(), f );
+    if( qni!=NULL ){
+      d_qn.push_back( qni );
+    }
+  }else if( d_type==typ_pred || d_type==typ_eq ){
+    //add initial constraint
+    Node nn[2];
+    int vn[2];
+    if( d_type==typ_pred ){
+      nn[0] = p->d_qinfo[q].getCurrentValue( d_n );
+      vn[0] = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( nn[0] ) );
+      nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );
+      vn[1] = -1;
+      d_tgt = true;
     }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
-      QcfNodeIndex * qni = p->getQcfNodeIndex( f );
-      if( qni ){
-        d_qn.push_back( qni );
+      for( unsigned i=0; i<2; i++ ){
+        nn[i] = p->d_qinfo[q].getCurrentValue( d_n[i] );
+        vn[i] = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( nn[i] ) );
       }
     }
-  }else if( d_type==typ_var_eq ){
-    bool success = false;
-    for( unsigned i=0; i<2; i++ ){
-      int var = p->d_qinfo[q].getVarNum( d_n[i] );
-      if( var!=-1 ){
-        int repVar = p->d_qinfo[q].getCurrentRepVar( var );
-        Node o = d_n[ i==0 ? 1 : 0 ];
-        o = p->d_qinfo[q].getCurrentValue( o );
-        int vo = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( o ) );
-        int addCons = p->d_qinfo[q].addConstraint( p, repVar, o, vo, d_tgt, false );
-        success = addCons!=-1;
-        //if successful and non-redundant, store that we need to cleanup this
-        if( addCons==1 ){
-          d_qni_bound_cons[repVar] = o;
-          d_qni_bound[repVar] = vo;
+    bool success;
+    if( vn[0]==-1 && vn[1]==-1 ){
+      Debug("qcf-match-debug") << "       reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;
+      //just compare values
+      success = d_tgt ? p->areMatchEqual( nn[0], nn[1] ) : p->areMatchDisequal( nn[0], nn[1] );
+    }else{
+      //otherwise, add a constraint to a variable
+      if( vn[1]!=-1 && vn[0]==-1 ){
+        //swap
+        Node t = nn[1];
+        nn[1] = nn[0];
+        nn[0] = t;
+        vn[0] = vn[1];
+        vn[1] = -1;
+      }
+      Debug("qcf-match-debug") << "       reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;
+      //add some constraint
+      int addc = p->d_qinfo[q].addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );
+      success = addc!=-1;
+      //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 ){
+            d_qni_bound[vn[i]] = vn[i];
+          }
         }
-        break;
+        d_qni_bound_cons[vn[0]] = nn[1];
+        d_qni_bound_cons_var[vn[0]] = vn[1];
       }
     }
+    //if successful, we will bind values to variables
     if( success ){
-      //store dummy
       d_qn.push_back( NULL );
     }
-  }else if( d_type==typ_valid_lit ){
-    //literal
-    EqRegistry * er = p->getEqRegistry( d_tgt, d_n, false );
-    Assert( er );
-    d_qn.push_back( &(er->d_qni) );
   }else{
     if( d_children.empty() ){
       //add dummy
@@ -1497,76 +1337,120 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q
       getChild( d_child_counter )->reset( p, d_tgt, q );
     }
   }
-  Debug("qcf-match") << "     Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;
+  d_binding = false;
+  Debug("qcf-match") << "     reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;
 }
 
 bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) {
   Debug("qcf-match") << "     Get next match for : " << d_n << ", type = ";
   debugPrintType( "qcf-match", d_type );
-  Debug("qcf-match") << ", children = " << d_children.size() << std::endl;
-  if( d_children.empty() ){
-    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;
-      while( success && it!=d_qni_bound.end() ){
-        std::map< int, MatchGen * >::iterator itm = p->d_qinfo[q].d_var_mg.find( it->second );
-        if( itm!=p->d_qinfo[q].d_var_mg.end() ){
-          Debug("qcf-match-debug") << "       process variable " << it->second << ", reset = " << doReset << std::endl;
-          if( doReset ){
-            itm->second->reset( p, true, q );
+  Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;
+  if( d_type==typ_ground ){
+    if( d_child_counter==0 ){
+      d_child_counter = -1;
+      return true;
+    }else{
+      return false;
+    }
+  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred ){
+    bool success = false;
+    bool terminate = false;
+    do {
+      bool doReset = false;
+      bool doFail = false;
+      if( !d_binding ){
+        if( doMatching( p, q ) ){
+          Debug("qcf-match-debug") << "     - Matching succeeded" << std::endl;
+          d_binding = true;
+          d_binding_it = d_qni_bound.begin();
+          doReset = true;
+        }else{
+          Debug("qcf-match-debug") << "     - Matching failed" << std::endl;
+          success = false;
+          terminate = true;
+        }
+      }else{
+        doFail = true;
+      }
+      if( d_binding ){
+        //also need to create match for each variable we bound
+        success = true;
+        Debug("qcf-match-debug") << "     Produce matches for bound variables by " << d_n << ", type = ";
+        debugPrintType( "qcf-match", d_type );
+        Debug("qcf-match-debug") << "..." << std::endl;
+
+        while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){
+          std::map< int, MatchGen * >::iterator itm;
+          if( !doFail ){
+            Debug("qcf-match-debug") << "       check variable " << d_binding_it->second << std::endl;
+            itm = p->d_qinfo[q].d_var_mg.find( d_binding_it->second );
           }
-          if( !itm->second->getNextMatch( p, q ) ){
-            do {
-              if( it==d_qni_bound.begin() ){
-                Debug("qcf-match-debug") << "       failed." << std::endl;
-                success = false;
-              }else{
-                Debug("qcf-match-debug") << "       decrement..." << std::endl;
-                --it;
-              }
-            }while( success && p->d_qinfo[q].d_var_mg.find( it->second )==p->d_qinfo[q].d_var_mg.end() );
-            doReset = false;
+          if( doFail || ( d_binding_it->first!=0 && itm!=p->d_qinfo[q].d_var_mg.end() ) ){
+            Debug("qcf-match-debug") << "       we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;
+            if( doReset ){
+              itm->second->reset( p, true, q );
+            }
+            if( doFail || !itm->second->getNextMatch( p, q ) ){
+              do {
+                if( d_binding_it==d_qni_bound.begin() ){
+                  Debug("qcf-match-debug") << "       failed." << std::endl;
+                  success = false;
+                }else{
+                  Debug("qcf-match-debug") << "       decrement..." << std::endl;
+                  --d_binding_it;
+                }
+              }while( success && ( d_binding_it->first==0 || p->d_qinfo[q].d_var_mg.find( d_binding_it->second )==p->d_qinfo[q].d_var_mg.end() ) );
+              doReset = false;
+              doFail = false;
+            }else{
+              Debug("qcf-match-debug") << "       increment..." << std::endl;
+              ++d_binding_it;
+              doReset = true;
+            }
           }else{
-            Debug("qcf-match-debug") << "       increment..." << std::endl;
-            ++it;
+            Debug("qcf-match-debug") << "       skip..." << d_binding_it->second << std::endl;
+            ++d_binding_it;
             doReset = true;
           }
+        }
+        if( !success ){
+          d_binding = false;
         }else{
-          Debug("qcf-match-debug") << "       skip..." << std::endl;
-          ++it;
-          doReset = true;
+          terminate = true;
+          if( d_binding_it==d_qni_bound.begin() ){
+            d_binding = false;
+          }
         }
       }
-    }
+    }while( !terminate );
     //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() ){
-          Debug("qcf-match") << "       Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;
-          std::map< int, int >::iterator itb = d_qni_bound.find( it->first );
-          int vn = itb!=d_qni_bound.end() ? itb->second : -1;
-          p->d_qinfo[q].addConstraint( p, it->first, it->second, vn, d_tgt, true );
-          if( vn!=-1 ){
-            d_qni_bound.erase( vn );
+      if( d_type==typ_eq || d_type==typ_pred ){
+        for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){
+          if( !it->second.isNull() ){
+            Debug("qcf-match") << "       Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;
+            std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );
+            int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;
+            p->d_qinfo[q].addConstraint( p, it->first, it->second, vn, d_tgt, true );
           }
         }
+        d_qni_bound_cons.clear();
+        d_qni_bound_cons_var.clear();
+        d_qni_bound.clear();
+      }else{
+        //clean up the match : remove equalities/disequalities
+        for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
+          Debug("qcf-match") << "       Clean up bound var " << it->second << std::endl;
+          Assert( it->second<p->d_qinfo[q].getNumVars() );
+          p->d_qinfo[q].d_match.erase( it->second );
+          p->d_qinfo[q].d_match_term.erase( it->second );
+        }
+        d_qni_bound.clear();
       }
-      d_qni_bound_cons.clear();
-      //clean up the match : remove equalities/disequalities
-      for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
-        Debug("qcf-match") << "       Clean up bound var " << it->second << std::endl;
-        Assert( it->second<p->d_qinfo[q].getNumVars() );
-        p->d_qinfo[q].d_match.erase( it->second );
-      }
-      d_qni_bound.clear();
     }
     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
     return success;
-  }else{
+  }else if( d_type==typ_formula ){
     if( d_child_counter!=-1 ){
       bool success = false;
       while( !success && d_child_counter>=0 ){
@@ -1664,7 +1548,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
       bool invalidMatch;
       do {
         invalidMatch = false;
-        Debug("qcf-match-debug") << "       Do matching " << d_qn.size() << " " << d_qni.size() << std::endl;
+        Debug("qcf-match-debug") << "       Do matching " << d_n << " " << d_qn.size() << " " << d_qni.size() << std::endl;
         if( d_qn.size()==d_qni.size()+1 ) {
           int index = (int)d_qni.size();
           //initialize
@@ -1721,7 +1605,6 @@ 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() );
@@ -1754,35 +1637,23 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
             d_qni.pop_back();
           }
         }
-        if( d_type==typ_var ){
-          if( !invalidMatch && d_qni.size()==d_qni_size ){
-            //if in the act of binding the variable by this term, bind the variable
-            std::map< int, Node >::iterator itb = d_qni_bound_cons.begin();
-            if( itb!=d_qni_bound_cons.end() ){
-              QcfNodeIndex * v_qni = &d_qni[d_qni.size()-1]->second;
-              Assert( v_qni->d_children.begin()!=v_qni->d_children.end() );
-              Node vb = v_qni->d_children.begin()->first;
-              Assert( !vb.isNull() );
-              vb = p->getRepresentative( vb );
-              Debug("qcf-match-debug") << "       For var, require binding " << itb->first << " to " << vb << ", d_tgt = " << d_tgt << std::endl;
-              if( !itb->second.isNull() ){
-                p->d_qinfo[q].addConstraint( p, itb->first, itb->second, -1, d_tgt, true );
-              }
-              int addCons = p->d_qinfo[q].addConstraint( p, itb->first, vb, -1, d_tgt, false );
-              if( addCons==-1 ){
-                Debug("qcf-match-debug") << "       Failed set for var." << std::endl;
-                invalidMatch = true;
-                d_qni_bound_cons[itb->first] = Node::null();
-              }else{
-                Debug("qcf-match-debug") << "       Succeeded set for var." << std::endl;
-                if( addCons==1 ){
-                  d_qni_bound_cons[itb->first] = vb;
-                }
-              }
-            }
+      }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );
+      if( d_qni.size()==d_qni_size ){
+        //Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );
+        //Debug("qcf-match-debug") << "       We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;
+        Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );
+        Node t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;
+        Debug("qcf-match-debug") << "       We matched " << t << std::endl;
+        //set the match terms
+        for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
+          if( it->second<(int)q[0].getNumChildren() ){   //if it is an actual variable, we are interested in knowing the actual term
+            Assert( it->first>0 );
+            Assert( p->d_qinfo[q].d_match.find( it->second )!=p->d_qinfo[q].d_match.end() );
+            Assert( p->areEqual( t[it->first-1], p->d_qinfo[q].d_match[ it->second ] ) );
+            p->d_qinfo[q].d_match_term[it->second] = t[it->first-1];
           }
         }
-      }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );
+      }
     }
   }
   return !d_qn.empty();
@@ -1793,20 +1664,20 @@ void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, boo
     switch( typ ){
     case typ_invalid: Trace(c) << "invalid";break;
     case typ_ground: Trace(c) << "ground";break;
-    case typ_valid_lit: Trace(c) << "valid_lit";break;
-    case typ_valid: Trace(c) << "valid";break;
+    case typ_eq: Trace(c) << "eq";break;
+    case typ_pred: Trace(c) << "pred";break;
+    case typ_formula: Trace(c) << "formula";break;
     case typ_var: Trace(c) << "var";break;
-    case typ_var_eq: Trace(c) << "var_eq";break;
     case typ_top: Trace(c) << "top";break;
     }
   }else{
     switch( typ ){
     case typ_invalid: Debug(c) << "invalid";break;
     case typ_ground: Debug(c) << "ground";break;
-    case typ_valid_lit: Debug(c) << "valid_lit";break;
-    case typ_valid: Debug(c) << "valid";break;
+    case typ_eq: Debug(c) << "eq";break;
+    case typ_pred: Debug(c) << "pred";break;
+    case typ_formula: Debug(c) << "formula";break;
     case typ_var: Debug(c) << "var";break;
-    case typ_var_eq: Debug(c) << "var_eq";break;
     case typ_top: Debug(c) << "top";break;
     }
   }
@@ -1827,79 +1698,36 @@ void QuantConflictFind::debugPrint( const char * c ) {
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
   while( !eqcs_i.isFinished() ){
     Node n = (*eqcs_i);
-    if( !n.getType().isInteger() ){
-      Trace(c) << "  - " << n << " : {";
-      eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() );
-      bool pr = false;
-      while( !eqc_i.isFinished() ){
-        Node nn = (*eqc_i);
-        if( nn.getKind()!=EQUAL && nn!=n ){
-          Trace(c) << (pr ? "," : "" ) << " " << nn;
+    //if( !n.getType().isInteger() ){
+    Trace(c) << "  - " << n << " : {";
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() );
+    bool pr = false;
+    while( !eqc_i.isFinished() ){
+      Node nn = (*eqc_i);
+      if( nn.getKind()!=EQUAL && nn!=n ){
+        Trace(c) << (pr ? "," : "" ) << " " << nn;
+        pr = true;
+      }
+      ++eqc_i;
+    }
+    Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
+    /*
+    EqcInfo * eqcn = getEqcInfo( n, false );
+    if( eqcn ){
+      Trace(c) << "    DEQ : {";
+      pr = false;
+      for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){
+        if( (*it).second ){
+          Trace(c) << (pr ? "," : "" ) << " " << (*it).first;
           pr = true;
         }
-        ++eqc_i;
       }
       Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
-      EqcInfo * eqcn = getEqcInfo( n, false );
-      if( eqcn ){
-        Trace(c) << "    DEQ : {";
-        pr = false;
-        for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){
-          if( (*it).second ){
-            Trace(c) << (pr ? "," : "" ) << " " << (*it).first;
-            pr = true;
-          }
-        }
-        Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
-      }
     }
+    //}
+    */
     ++eqcs_i;
   }
-  std::map< Node, std::map< Node, bool > > printed;
-  //print the equality registries
-  for( unsigned i=0; i<2; i++ ){
-    printed.clear();
-    Trace(c) << "----------EQR, polarity = " << (i==0) << std::endl;
-    for( unsigned j=0; j<2; j++ ){
-      for( std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > >::iterator it = d_eqr[i][j].begin(); it != d_eqr[i][j].end(); ++it ){
-        bool prHead = false;
-        for( unsigned jj=0; jj<2; jj++ ){
-          for( std::map< TNode, EqRegistry * >::iterator it2 = it->second[jj].begin(); it2 != it->second[jj].end(); ++it2 ){
-            bool print;
-            if( isHandledUfTerm( it->first ) && isHandledUfTerm( it2->first ) &&
-                it->first.getOperator()!=it2->first.getOperator() ){
-              print = isLessThan( it->first.getOperator(), it2->first.getOperator() );
-            }else{
-              print = printed[it->first].find( it2->first )==printed[it->first].end();
-            }
-            if( print ){
-              printed[it->first][it2->first] = true;
-              printed[it2->first][it->first] = true;
-              if( !prHead ){
-                Trace(c) << "- " << it->first << std::endl;
-                prHead = true;
-              }
-              Trace(c) << "    " << it2->first << ", terms : " << std::endl;
-
-              /*
-              Trace(c) << "    " << it2->first << " : {";
-              bool pr = false;
-              for( NodeBoolMap::iterator it3 = it2->second->d_t_eqc.begin(); it3 != it2->second->d_t_eqc.end(); ++it3 ){
-                if( (*it3).second ){
-                  Trace(c) << (pr ? "," : "" ) << " " << (*it3).first;
-                  pr = true;
-                }
-              }
-              Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
-              */
-              //print qni structure
-              it2->second->debugPrint( c, 3 );
-            }
-          }
-        }
-      }
-    }
-  }
 }
 
 void QuantConflictFind::debugPrintQuant( const char * c, Node q ) {
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 15923b0ba..d8fe1e808 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -33,46 +33,11 @@ class QcfNodeIndex {
 public:
   std::map< TNode, QcfNodeIndex > d_children;
   void clear() { d_children.clear(); }
-  //Node existsTerm( QuantConflictFind * qcf, Node n, int index = 0 );
-  //Node addTerm( QuantConflictFind * qcf, Node n, int index = 0 );
-  //bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 );
   void debugPrint( const char * c, int t );
-  //optimized versions
   Node existsTerm( TNode n, std::vector< TNode >& reps, int index = 0 );
   Node addTerm( TNode n, std::vector< TNode >& reps, int index = 0 );
-  bool addTermEq( TNode n1, TNode n2, std::vector< TNode >& reps1, std::vector< TNode >& reps2, int index = 0 );
 };
 
-class EqRegistry {
-  typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-public:
-  EqRegistry( context::Context* c );
-  //active
-  context::CDO< bool > d_active;
-  //NodeIndex describing pairs that meet the criteria of the EqRegistry
-  QcfNodeIndex d_qni;
-
-  //qcf nodes that this helps to 1:satisfy -1:falsify 0:both a quantifier conflict node
-  //std::map< QcfNode *, int > d_qcf;
-  //has eqc
-  //bool hasEqc( Node n ) { return d_t_eqc.find( n )!=d_t_eqc.end() && d_t_eqc[n]; }
-  //void setEqc( Node n, bool val = true ) { d_t_eqc[n] = val; }
-  void clear() { d_qni.clear(); }
-  void debugPrint( const char * c, int t );
-};
-
-/*
-class QcfNode {
-public:
-  QcfNode( context::Context* c );
-  QcfNode * d_parent;
-  std::map< int, QcfNode * > d_child;
-  Node d_node;
-  EqRegistry * d_reg[2];
-};
-*/
-
 class QuantConflictFind : public QuantifiersModule
 {
   friend class QcfNodeIndex;
@@ -86,21 +51,16 @@ private:
   void registerNode( Node q, Node n, bool hasPol, bool pol );
   void flatten( Node q, Node n );
 private:
-  std::map< TypeNode, Node > d_fv;
-  Node getFv( TypeNode tn );
   std::map< Node, Node > d_op_node;
-  int getFunctionId( Node f );
-  bool isLessThan( Node a, Node b );
   Node getFunction( Node n, int& index, bool isQuant = false );
   int d_fid_count;
   std::map< Node, int > d_fid;
   Node mkEqNode( Node a, Node b );
-private:  //for ground terms
+public:  //for ground terms
   Node d_true;
   Node d_false;
-  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 );
+private:
+  Node evaluateTerm( Node n );
   int evaluate( Node n, bool pref = false, bool hasPref = false );
 public:  //for quantifiers
   //match generator
@@ -124,14 +84,19 @@ public:  //for quantifiers
     std::map< int, Node > d_qni_gterm_rep;
     std::map< int, int > d_qni_bound;
     std::map< int, Node > d_qni_bound_cons;
+    std::map< int, int > d_qni_bound_cons_var;
+    std::map< int, int >::iterator d_binding_it;
+    bool d_binding;
+    //int getVarBindingVar();
+    std::map< int, Node > d_ground_eval;
   public:
     //type of the match generator
     enum {
       typ_invalid,
       typ_ground,
-      typ_var_eq,
-      typ_valid_lit,
-      typ_valid,
+      typ_pred,
+      typ_eq,
+      typ_formula,
       typ_var,
       typ_top,
     };
@@ -159,7 +124,7 @@ private:
     QuantInfo() : d_mg( NULL ) {}
     std::vector< Node > d_vars;
     std::map< Node, int > d_var_num;
-    std::map< EqRegistry *, bool > d_rel_eqr;
+    //std::map< EqRegistry *, bool > d_rel_eqr;
     std::map< int, std::vector< Node > > d_var_constraint[2];
     int getVarNum( Node v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
     bool isVar( Node v ) { return d_var_num.find( v )!=d_var_num.end(); }
@@ -171,16 +136,18 @@ private:
   public:
     //current constraints
     std::map< int, Node > d_match;
+    std::map< int, Node > d_match_term;
     std::map< int, std::map< Node, int > > d_curr_var_deq;
     int getCurrentRepVar( int v );
     Node getCurrentValue( Node n );
-    bool getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n );
+    bool getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n, bool chDiseq = false );
     int addConstraint( QuantConflictFind * p, int v, Node n, bool polarity );
     int addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove );
     bool setMatch( QuantConflictFind * p, int v, Node n );
     bool isMatchSpurious( QuantConflictFind * p );
     bool completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned );
     void debugPrintMatch( const char * c );
+    bool isConstrainedVar( int v );
   };
   std::map< Node, QuantInfo > d_qinfo;
 private:  //for equivalence classes
@@ -188,8 +155,8 @@ private:  //for equivalence classes
   bool areDisequal( Node n1, Node n2 );
   bool areEqual( Node n1, Node n2 );
   Node getRepresentative( Node n );
-  Node getTerm( Node n );
 
+/*
   class EqcInfo {
   public:
     EqcInfo( context::Context* c ) : d_diseq( c ) {}
@@ -200,10 +167,12 @@ private:  //for equivalence classes
   };
   std::map< Node, EqcInfo * > d_eqc_info;
   EqcInfo * getEqcInfo( Node n, bool doCreate = true );
+*/
   // operator -> index(terms)
   std::map< TNode, QcfNodeIndex > d_uf_terms;
-  // eqc x operator -> index(terms)
-  std::map< TNode, std::map< TNode, QcfNodeIndex > > d_eqc_uf_terms;
+  // operator -> index(eqc -> terms)
+  std::map< TNode, QcfNodeIndex > d_eqc_uf_terms;
+  //get qcf node index
   QcfNodeIndex * getQcfNodeIndex( Node eqc, Node f );
   QcfNodeIndex * getQcfNodeIndex( Node f );
   // type -> list(eqc)
@@ -217,7 +186,8 @@ private:  //for equivalence classes
 public:
   enum {
     effort_conflict,
-    effort_propagation,
+    effort_prop_eq,
+    effort_prop_deq,
   };
   short d_effort;
   //for effort_prop
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 3a6785d00..ac847678d 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -269,7 +269,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
           children.push_back( computeNNF( body[0][i].notNode() ) );
         }
         k = body[0].getKind()==AND ? OR : AND;
-      }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){
+      }else if( body[0].getKind()==IFF ){
         for( int i=0; i<2; i++ ){
           Node nn = i==0 ? body[0][i] : body[0][i].notNode();
           children.push_back( computeNNF( nn ) );