Add new method --quant-cf for finding conflicts eagerly for quantified formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.

author: Andrew Reynolds <andrew.j.reynolds@gmail.com> 2014-01-10 02:04:51 -0600
committer: Andrew Reynolds <andrew.j.reynolds@gmail.com> 2014-01-10 02:07:39 -0600
commit: 841b7951f41f399859afab13a81e04599308da61 (patch)
tree: 8c6eb70b498b0a01f00c1a77b96d00ff2f61c21b /src/theory
parent: 18fed5592fb769d12ba2901a0fdc00c5c02863b9 (diff)
18 files changed, 2077 insertions, 53 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 28485a979..d4faf41fe 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -198,10 +198,9 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,
 void BoundedIntegers::process( Node f, Node n, bool pol,
                                std::map< int, std::map< Node, Node > >& bound_lit_map,
                                std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){
-  if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){
+  if( (n.getKind()==OR && pol) || (n.getKind()==AND && !pol) ){
     for( unsigned i=0; i<n.getNumChildren(); i++) {
-      bool newPol = n.getKind()==IMPLIES && i==0 ? !pol : pol;
-      process( f, n[i], newPol, bound_lit_map, bound_lit_pol_map );
+      process( f, n[i], pol, bound_lit_map, bound_lit_pol_map );
     }
   }else if( n.getKind()==NOT ){
     process( f, n[0], !pol, bound_lit_map, bound_lit_pol_map );
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 797ca8f70..a05abfa29 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -174,7 +174,7 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
   if( n.getKind()==NOT ){
     int val = evaluate( n[0], depIndex, ri );
     return val==1 ? -1 : ( val==-1 ? 1 : 0 );
-  }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){
+  }else if( n.getKind()==OR || n.getKind()==AND ){
     int baseVal = n.getKind()==AND ? 1 : -1;
     int eVal = baseVal;
     int posDepIndex = ri->getNumTerms();
@@ -182,7 +182,7 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
       //evaluate subterm
       int childDepIndex;
-      Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];
+      Node nn = n[i];
       int eValT = evaluate( nn, childDepIndex, ri );
       if( eValT==baseVal ){
         if( eVal==baseVal ){
@@ -210,12 +210,12 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
     }else{
       return 0;
     }
-  }else if( n.getKind()==IFF || n.getKind()==XOR ){
+  }else if( n.getKind()==IFF ){
     int depIndex1;
     int eVal = evaluate( n[0], depIndex1, ri );
     if( eVal!=0 ){
       int depIndex2;
-      int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2, ri );
+      int eVal2 = evaluate( n[1], depIndex2, ri );
       if( eVal2!=0 ){
         depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
         return eVal==eVal2 ? 1 : -1;
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 9cd12fbfb..600f8c0b9 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -233,7 +233,7 @@ bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map<
 void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
   if( n.getKind()==NOT ){
     process( n[0], !pol, args, f );
-  }else if( n.getKind()==AND || n.getKind()==OR || n.getKind()==IMPLIES ){
+  }else if( n.getKind()==AND || n.getKind()==OR ){
     //bool favorPol = (n.getKind()==AND)==pol;
     //conditional?
   }else if( n.getKind()==ITE ){
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index cb63ccd45..493d54b53 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -929,13 +929,13 @@ Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity,
   Node ret;
   if( n.getKind()==NOT ){
     ret = getSelectionFormula( fn[0], n[0], !polarity, useOption );
-  }else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){
+  }else if( n.getKind()==OR || n.getKind()==AND ){
     //whether we only need to find one or all
     bool favorPol = ( n.getKind()!=AND && polarity ) || ( n.getKind()==AND && !polarity );
     std::vector< Node > children;
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i];
-      Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i];
+      Node fnc = fn[i];
+      Node nc = n[i];
       Node nn = getSelectionFormula( fnc, nc, polarity, useOption );
       if( nn.isNull() && !favorPol ){
         //cannot make selection formula
@@ -993,8 +993,8 @@ Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity,
     if( ret.isNull() && !nc[0].isNull() && !nc[1].isNull() ){
       ret = mkAndSelectionFormula( nc[0], nc[1] );
     }
-  }else if( n.getKind()==IFF || n.getKind()==XOR ){
-    bool opPol = polarity ? n.getKind()==XOR : n.getKind()==IFF;
+  }else if( n.getKind()==IFF ){
+    bool opPol = !polarity;
     for( int p=0; p<2; p++ ){
       Node nn[2];
       for( int i=0; i<2; i++ ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index f314584cd..bc717bbbc 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -178,15 +178,17 @@ int ModelEngine::checkModel(){
          it != fm->d_rep_set.d_type_reps.end(); ++it ){
       if( it->first.isSort() ){
         Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
-        Trace("model-engine-debug") << "   ";
-        Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
-        for( size_t i=0; i<it->second.size(); i++ ){
-          //Trace("model-engine-debug") << it->second[i] << "  ";
-          Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
-          Trace("model-engine-debug") << r << " ";
+        if( Trace.isOn("model-engine-debug") ){
+          Trace("model-engine-debug") << "   ";
+          Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+          for( size_t i=0; i<it->second.size(); i++ ){
+            //Trace("model-engine-debug") << it->second[i] << "  ";
+            Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
+            Trace("model-engine-debug") << r << " ";
+          }
+          Trace("model-engine-debug") << std::endl;
+          Trace("model-engine-debug") << "  Model basis term : " << mbt << std::endl;
         }
-        Trace("model-engine-debug") << std::endl;
-        Trace("model-engine-debug") << "  Model basis term : " << mbt << std::endl;
       }
     }
   }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 190c7ddc9..652526cc9 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -40,7 +40,7 @@ option clauseSplit --clause-split bool :default false
 # Whether to pre-skolemize quantifier bodies.
 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
 #   forall x. P( x ) => f( S( x ) ) = x
-option preSkolemQuant --pre-skolem-quant bool :default false
+option preSkolemQuant --pre-skolem-quant bool :read-write :default false
  apply skolemization eagerly to bodies of quantified formulas
 option iteRemoveQuant --ite-remove-quant bool :default false
  apply ite removal to bodies of quantifiers
@@ -119,5 +119,7 @@ option fmfBoundInt --fmf-bound-int bool :default false
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
  policy for instantiating axioms
 
+option quantConflictFind --quant-cf bool :default false
+ enable eager conflict find mechanism for quantifiers
 
 endmodule
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
new file mode 100755
index 000000000..58840989d
--- /dev/null
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -0,0 +1,1712 @@
+/*********************                                                        */
+/*! \file quant_conflict_find.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief quant conflict find class
+ **
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/quant_conflict_find.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, bool doAdd, int index ) {
+  if( index==(int)n.getNumChildren() ){
+    if( d_children.empty() ){
+      if( doAdd ){
+        d_children[ n ].clear();
+        return n;
+      }else{
+        return Node::null();
+      }
+    }else{
+      return d_children.begin()->first;
+    }
+  }else{
+    Node r = qcf->getRepresentative( n[index] );
+    return d_children[r].addTerm( qcf, n, doAdd, index+1 );
+  }
+}
+
+bool QcfNodeIndex::addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index ) {
+  if( index==(int)n1.getNumChildren() ){
+    Node n = addTerm( qcf, n2 );
+    return n==n2;
+  }else{
+    Node r = qcf->getRepresentative( n1[index] );
+    return d_children[r].addTermEq( qcf, n1, n2, index+1 );
+  }
+}
+
+void QcfNodeIndex::debugPrint( const char * c, int t ) {
+  for( std::map< Node, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
+    if( !it->first.isNull() ){
+      for( int j=0; j<t; j++ ){ Trace(c) << "  "; }
+      Trace(c) << it->first << " : " << std::endl;
+      it->second.debugPrint( c, t+1 );
+    }
+  }
+}
+
+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 ),
+d_conflict( c, false ),
+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.getOperator() )<getFunctionId( b.getOperator() );
+  //}
+}
+
+Node QuantConflictFind::getFunction( Node n, bool isQuant ) {
+  if( isQuant && !quantifiers::TermDb::hasBoundVarAttr( n ) ){
+    return n;
+  }else if( n.getKind()==APPLY_UF ){
+    std::map< Node, Node >::iterator it = d_op_node.find( n.getOperator() );
+    if( it==d_op_node.end() ){
+      std::vector< Node > children;
+      children.push_back( n.getOperator() );
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        children.push_back( getFv( n[i].getType() ) );
+      }
+      Node nn = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+      d_op_node[n.getOperator()] = nn;
+      return nn;
+    }else{
+      return it->second;
+    }
+  }else{
+    //should be a variable
+    return Node::null();
+  }
+}
+
+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 );
+  }else{
+    return a.eqNode( 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 ){
+    registerQuant( 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::registerQuant( 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 ) ) ){
+        flatten( q, n );
+      }else{
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          flatten( q, n[i] );
+        }
+      }
+    }else{
+      Trace("qcf-qregister") << "    RegisterGroundLit : " << n;
+    }
+    recurse = false;
+  }
+  if( recurse ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      bool newHasPol;
+      bool newPol;
+      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+      //QcfNode * qcfc = new QcfNode( d_c );
+      //qcfc->d_parent = qcf;
+      //qcf->d_child[i] = qcfc;
+      registerQuant( q, n[i], newHasPol, newPol );
+    }
+  }
+}
+
+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] );
+      }
+    }
+  }
+}
+
+void QuantConflictFind::registerQuantifier( Node q ) {
+  d_quants.push_back( q );
+  d_quant_id[q] = d_quants.size();
+  Trace("qcf-qregister") << "Register ";
+  debugPrintQuant( "qcf-qregister", q );
+  Trace("qcf-qregister") << " : " << q << std::endl;
+
+  //register the variables
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    d_qinfo[q].d_var_num[q[0][i]] = i;
+    d_qinfo[q].d_vars.push_back( q[0][i] );
+  }
+
+  //make QcfNode structure
+  Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
+  //d_qinfo[q].d_cf = new QcfNode( d_c );
+  registerQuant( q, q[1], true, true );
+
+  //debug print
+  Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
+  Trace("qcf-qregister") << "    ";
+  debugPrintQuantBody( "qcf-qregister", q, q[1] );
+  Trace("qcf-qregister") << std::endl;
+  if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
+    Trace("qcf-qregister") << "  with additional constraints : " << std::endl;
+    for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
+      Trace("qcf-qregister") << "    ?x" << j << " = ";
+      debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
+      Trace("qcf-qregister") << std::endl;
+    }
+  }
+
+  Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
+  d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true );
+
+  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;
+  if( lit.getKind()==EQUAL ){
+    i = polarity ? 0 : 1;
+    f1 = getFunction( lit[0], true );
+    f2 = getFunction( lit[1], true );
+  }else if( lit.getKind()==APPLY_UF ){
+    i = 0;
+    f1 = getFunction( lit, true );
+    f2 = polarity ? d_true : d_false;
+  }
+  if( !f1.isNull() && !f2.isNull() ){
+    if( d_eqr[i][f1].find( f2 )==d_eqr[i][f1].end() ){
+      if( doCreate ){
+        Trace("qcf-register") << "RegisterEqr : " << f1 << " " << f2 << ", polarity = " << (i==0) << std::endl;
+        d_eqr[i][f1][f2] = new EqRegistry( d_c );
+        d_eqr[i][f2][f1] = d_eqr[i][f1][f2];
+      }else{
+        return NULL;
+      }
+    }
+    return d_eqr[i][f1][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()==APPLY_UF ){
+          terms.push_back( lit[i] );
+        }else if( lit[i].getKind()==BOUND_VARIABLE ){
+          //do not handle variable equalities
+          terms.clear();
+          return;
+        }
+      }
+    }
+    if( terms.size()==2 && isLessThan( terms[1], terms[0] ) ){
+      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 ) {
+  int ret = 0;
+  if( n.getKind()==EQUAL ){
+    Node n1 = getTerm( n[0] );
+    Node n2 = getTerm( 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( n.getKind()==APPLY_UF ){
+    Node nn = getTerm( 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( n.getKind()==NOT ){
+    return -evaluate( n[0] );
+  }else if( n.getKind()==ITE ){
+    int cev1 = evaluate( n[0] );
+    int cevc[2] = { 0, 0 };
+    for( unsigned i=0; i<2; i++ ){
+      if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){
+        cevc[i] = evaluate( n[i+1] );
+        if( cev1!=0 ){
+          ret = cevc[i];
+          break;
+        }else if( cevc[i]==0 ){
+          break;
+        }
+      }
+    }
+    if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){
+      ret = cevc[0];
+    }
+  }else if( n.getKind()==IFF ){
+    int cev1 = evaluate( n[0] );
+    if( cev1!=0 ){
+      int cev2 = evaluate( n[1] );
+      if( cev2!=0 ){
+        ret = cev1==cev2 ? 1 : -1;
+      }
+    }
+
+  }else{
+    int ssval = 0;
+    if( n.getKind()==OR ){
+      ssval = 1;
+    }else if( n.getKind()==AND ){
+      ssval = -1;
+    }
+    bool isUnk = false;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      int cev = evaluate( n[i] );
+      if( cev==ssval ){
+        ret = ssval;
+        break;
+      }else if( cev==0 ){
+        isUnk = true;
+      }
+    }
+    if( ret==0 && !isUnk ){
+      ret = -ssval;
+    }
+  }
+  Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;
+  return ret;
+}
+
+//-------------------------------------------------- handling assertions / eqc
+
+void QuantConflictFind::assertNode( Node q ) {
+  Trace("qcf-proc") << "QCF : assertQuantifier : ";
+  debugPrintQuant("qcf-proc", 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 );
+  }
+}
+
+eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {
+  //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
+  return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+}
+bool QuantConflictFind::areEqual( Node n1, Node n2 ) {
+  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );
+}
+bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {
+  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );
+}
+Node QuantConflictFind::getRepresentative( Node n ) {
+  if( getEqualityEngine()->hasTerm( n ) ){
+    return getEqualityEngine()->getRepresentative( n );
+  }else{
+    return n;
+  }
+}
+Node QuantConflictFind::getTerm( Node n ) {
+  if( n.getKind()==APPLY_UF ){
+    Node nn = d_uf_terms[n.getOperator()].addTerm( this, n, false );
+    if( !nn.isNull() ){
+      return nn;
+    }
+  }
+  return 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 ){
+      EqcInfo * eqci = new EqcInfo( d_c );
+      d_eqc_info[n] = eqci;
+      return eqci;
+    }else{
+      return NULL;
+    }
+  }
+  return it2->second;
+}
+
+/** 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;
+}
+
+/** merge */
+void QuantConflictFind::merge( Node a, Node b ) {
+  if( b.getKind()==EQUAL ){
+    if( a==d_true ){
+      //will merge anyways
+      //merge( b[0], b[1] );
+    }else if( a==d_false ){
+      assertDisequal( b[0], b[1] );
+    }
+  }else{
+    Trace("qcf-proc") << "QCF : merge : " << a << " " << b << std::endl;
+    EqcInfo * eqc_b = getEqcInfo( b, false );
+    EqcInfo * eqc_a = NULL;
+    if( eqc_b ){
+      eqc_a = getEqcInfo( a );
+      //move disequalities of b into a
+      for( NodeBoolMap::iterator it = eqc_b->d_diseq.begin(); it != eqc_b->d_diseq.end(); ++it ){
+        if( (*it).second ){
+          Node n = (*it).first;
+          EqcInfo * eqc_n = getEqcInfo( n, false );
+          Assert( eqc_n );
+          if( !eqc_n->isDisequal( a ) ){
+            Assert( !eqc_a->isDisequal( n ) );
+            eqc_n->setDisequal( a );
+            eqc_a->setDisequal( n );
+            //setEqual( eqc_a, eqc_b, a, n, false );
+          }
+          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;
+        }
+      }
+      */
+    }
+    //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;
+  EqcInfo * eqc_a = getEqcInfo( a );
+  EqcInfo * eqc_b = getEqcInfo( b );
+  if( !eqc_a->isDisequal( b ) ){
+    Assert( !eqc_b->isDisequal( a ) );
+    eqc_b->setDisequal( a );
+    eqc_a->setDisequal( b );
+    //setEqual( eqc_a, eqc_b, a, b, false );
+  }
+  Trace("qcf-proc2") << "QCF : finished assert disequal : " << a << " " << b << std::endl;
+}
+
+//-------------------------------------------------- check function
+
+/** check */
+void QuantConflictFind::check( Theory::Effort level ) {
+  Trace("qcf-check") << "QCF : check : " << level << std::endl;
+  if( d_conflict ){
+    Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
+  }else{
+    bool addedLemma = false;
+    if( level==Theory::EFFORT_FULL ){
+      double clSet = 0;
+      if( Trace.isOn("qcf-engine") ){
+        clSet = double(clock())/double(CLOCKS_PER_SEC);
+        Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;
+      }
+      Trace("qcf-check") << "Compute relevant equalities..." << std::endl;
+      computeRelevantEqr();
+
+      Trace("qcf-debug") << std::endl;
+      debugPrint("qcf-debug");
+      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 ) ){
+              //assign values for variables that were unassigned (usually not necessary, but handles corner cases)
+              Trace("qcf-check") << std::endl;
+              std::vector< int > unassigned;
+              std::vector< TypeNode > unassigned_tn;
+              for( int i=0; i<d_qinfo[q].getNumVars(); i++ ){
+                if( d_qinfo[q].d_match.find( i )==d_qinfo[q].d_match.end() ){
+                  Assert( i<(int)q[0].getNumChildren() );
+                  unassigned.push_back( i );
+                  unassigned_tn.push_back( d_qinfo[q].getVar( i ).getType() );
+                }
+              }
+              bool success = true;
+              if( !unassigned.empty() ){
+                Trace("qcf-check") << "Assign to unassigned..." << std::endl;
+                int index = 0;
+                std::vector< int > eqc_count;
+                do {
+                  bool invalidMatch;
+                  while( ( index>=0 && (int)index<(int)unassigned.size() ) || invalidMatch ){
+                    invalidMatch = false;
+                    if( index==(int)eqc_count.size() ){
+                      eqc_count.push_back( 0 );
+                    }else{
+                      Assert( index==(int)eqc_count.size()-1 );
+                      if( eqc_count[index]<(int)d_eqcs[unassigned_tn[index]].size() ){
+                        int currIndex = eqc_count[index];
+                        eqc_count[index]++;
+                        Trace("qcf-check-unassign") << unassigned[index] << "->" << d_eqcs[unassigned_tn[index]][currIndex] << std::endl;
+                        if( d_qinfo[q].setMatch( this, unassigned[index], d_eqcs[unassigned_tn[index]][currIndex] ) ){
+                          Trace("qcf-check-unassign") << "Succeeded match" << std::endl;
+                          index++;
+                        }else{
+                          Trace("qcf-check-unassign") << "Failed match" << std::endl;
+                          invalidMatch = true;
+                        }
+                      }else{
+                        Trace("qcf-check-unassign") << "No more matches" << std::endl;
+                        eqc_count.pop_back();
+                        index--;
+                      }
+                    }
+                  }
+                  success = index>=0;
+                  if( success ){
+                    index = (int)unassigned.size()-1;
+                    Trace("qcf-check-unassign") << "  Try: " << std::endl;
+                    for( unsigned i=0; i<unassigned.size(); i++ ){
+                      int ui = unassigned[i];
+                      Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_qinfo[q].d_vars[ui] << " -> " << d_qinfo[q].d_match[ui] << std::endl;
+                    }
+                  }
+                }while( success && d_qinfo[q].isMatchSpurious( this ) );
+              }
+
+              if( success ){
+                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;
+                  break;
+                }else{
+                  Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;
+                  Assert( false );
+                }
+              }else{
+                Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
+              }
+              for( unsigned i=0; i<unassigned.size(); i++ ){
+                d_qinfo[q].d_match.erase( unassigned[i] );
+              }
+            }else{
+              Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;
+            }
+          }
+        }
+        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) << ", addedLemma = " << addedLemma << std::endl;
+      }
+    }
+    Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
+  }
+}
+
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {
+  return !d_conflict && level==Theory::EFFORT_FULL;
+}
+
+void QuantConflictFind::computeRelevantEqr() {
+  //first, reset information
+  for( unsigned i=0; i<2; i++ ){
+    for( std::map< Node, std::map< Node, EqRegistry * > >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){
+      for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        it2->second->clear();
+      }
+    }
+  }
+  d_uf_terms.clear();
+  d_eqc_uf_terms.clear();
+  d_eqcs.clear();
+
+  //which nodes are irrelevant for disequality matches
+  std::map< Node, bool > irrelevant_dnode;
+  //which eqc we have processed
+  std::map< Node, bool > process_eqc;
+  //now, store matches
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
+  while( !eqcs_i.isFinished() ){
+    Node r = (*eqcs_i);
+    d_eqcs[r.getType()].push_back( r );
+    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 ){
+        if( (*it).second ){
+          Node rd = (*it).first;
+          //if we have processed the other direction
+          if( process_eqc.find( rd )!=process_eqc.end() ){
+            eq::EqClassIterator eqcd_i = eq::EqClassIterator( rd, getEqualityEngine() );
+            while( !eqcd_i.isFinished() ){
+              Node nd = (*eqcd_i);
+              if( irrelevant_dnode.find( nd )==irrelevant_dnode.end() ){
+                deqc.push_back( nd );
+              }
+              ++eqcd_i;
+            }
+          }
+        }
+      }
+    }
+    //the relevant nodes in this eqc
+    std::vector< Node > eqc;
+    //process disequalities
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
+    while( !eqc_i.isFinished() ){
+      Node n = (*eqc_i);
+      bool isRedundant;
+      if( n.getKind()==APPLY_UF ){
+        Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( this, n );
+        isRedundant = (nadd!=n);
+        d_uf_terms[n.getOperator()].addTerm( this, n );
+      }else{
+        isRedundant = false;
+      }
+      //process all relevant equalities and disequalities to n
+      for( unsigned index=0; index<2; index++ ){
+        std::map< Node, std::map< Node, EqRegistry * > >::iterator itn[2];
+        itn[0] = d_eqr[index].find( n );
+        Node fn;
+        if( n.getKind()==APPLY_UF && !isRedundant ){
+          fn = getFunction( n );
+          itn[1] = d_eqr[index].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].end() ){
+            relevant = true;
+            std::vector< Node >& rel_nodes = index==0 ? eqc : deqc;
+            for( unsigned i=0; i<rel_nodes.size(); i++ ){
+              Node m = rel_nodes[i];
+              Node fm;
+              if( m.getKind()==APPLY_UF ){
+                fm = getFunction( m );
+              }
+              //process equality/disequality
+              if( j==1 ){
+                //fn with m
+                std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( m );
+                if( itm!=itn[j]->second.end() ){
+                  if( itm->second->d_qni.addTerm( this, n )==n ){
+                    Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";
+                    Trace("qcf-reqr") << fn << " " << m << std::endl;
+                  }
+                }
+              }
+              if( !fm.isNull() ){
+                std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( fm );
+                if( itm!=itn[j]->second.end() ){
+                  if( j==0 ){
+                    //n with fm
+                    if( itm->second->d_qni.addTerm( this, m )==m ){
+                      Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";
+                      Trace("qcf-reqr") << n << " " << fm << std::endl;
+                    }
+                  }else{
+                    //fn with fm
+                    bool mltn = isLessThan( m, n );
+                    for( unsigned i=0; i<2; i++ ){
+                      if( i==0 || m.getOperator()==n.getOperator() ){
+                        Node am = ((i==0)==mltn) ? n : m;
+                        Node an = ((i==0)==mltn) ? m : n;
+                        if( itm->second->d_qni.addTermEq( this, an, am ) ){
+                          Trace("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for ";
+                          Trace("qcf-reqr") << fn << " " << fm << std::endl;
+                        }
+                      }
+                    }
+                  }
+                }
+              }
+            }
+          }
+        }
+        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;
+    }
+    process_eqc[r] = true;
+    ++eqcs_i;
+  }
+}
+
+
+void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {
+  d_match.clear();
+  d_curr_var_deq.clear();
+  //add built-in variable constraints
+  for( unsigned r=0; r<2; r++ ){
+    for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();
+         it != d_var_constraint[r].end(); ++it ){
+      for( unsigned j=0; j<it->second.size(); j++ ){
+        Node rr = it->second[j];
+        if( !isVar( rr ) ){
+          rr = p->getRepresentative( rr );
+        }
+        if( addConstraint( p, it->first, rr, r==0 )==-1 ){
+          d_var_constraint[0].clear();
+          d_var_constraint[1].clear();
+          //quantified formula is actually equivalent to true
+          Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl;
+          d_mg->d_children.clear();
+          d_mg->d_n = NodeManager::currentNM()->mkConst( true );
+          d_mg->d_type = MatchGen::typ_ground;
+          return;
+        }
+      }
+    }
+  }
+  d_mg->reset_round( p );
+}
+
+int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) {
+  std::map< int, Node >::iterator it = d_match.find( v );
+  if( it!=d_match.end() ){
+    int vn = getVarNum( it->second );
+    if( vn!=-1 ){
+      //int vr = getCurrentRepVar( vn );
+      //d_match[v] = d_vars[vr];
+      //return vr;
+      return getCurrentRepVar( vn );
+    }
+  }
+  return v;
+}
+
+Node QuantConflictFind::QuantInfo::getCurrentValue( Node n ) {
+  int v = getVarNum( n );
+  if( v==-1 ){
+    return n;
+  }else{
+    std::map< int, Node >::iterator it = d_match.find( v );
+    if( it==d_match.end() ){
+      return n;
+    }else{
+      Assert( getVarNum( it->second )!=v );
+      return getCurrentValue( it->second );
+    }
+  }
+}
+
+bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n ) {
+  //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->areDisequal( n, cv ) ){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, bool polarity ) {
+  v = getCurrentRepVar( v );
+  int vn = getVarNum( n );
+  vn = vn==-1 ? -1 : getCurrentRepVar( vn );
+  n = getCurrentValue( n );
+  return addConstraint( p, v, n, vn, polarity, false );
+}
+
+int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove ) {
+  //for handling equalities between variables, and disequalities involving variables
+  Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";
+  Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;
+  Assert( n==getCurrentValue( n ) );
+  Assert( doRemove || v==getCurrentRepVar( v ) );
+  Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );
+  if( polarity ){
+    if( vn!=v ){
+      if( doRemove ){
+        if( vn!=-1 ){
+          //if set to this in the opposite direction, clean up opposite instead
+          std::map< int, Node >::iterator itmn = d_match.find( vn );
+          if( itmn!=d_match.end() && itmn->second==d_vars[v] ){
+            return addConstraint( p, vn, d_vars[v], v, true, true );
+          }else{
+            //unsetting variables equal
+
+            //remove disequalities owned by this
+            std::vector< Node > remDeq;
+            for( std::map< Node, int >::iterator it = d_curr_var_deq[vn].begin(); it != d_curr_var_deq[vn].end(); ++it ){
+              if( it->second==v ){
+                remDeq.push_back( it->first );
+              }
+            }
+            for( unsigned i=0; i<remDeq.size(); i++ ){
+              d_curr_var_deq[vn].erase( remDeq[i] );
+            }
+          }
+        }
+        d_match.erase( v );
+        return 1;
+      }else{
+        std::map< int, Node >::iterator itm = d_match.find( v );
+
+        if( vn!=-1 ){
+          Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;
+          std::map< int, Node >::iterator itmn = d_match.find( vn );
+          if( itm==d_match.end() ){
+            //setting variables equal
+            bool alreadySet = false;
+            if( itmn!=d_match.end() ){
+              alreadySet = true;
+              Assert( !itmn->second.isNull() && !isVar( itmn->second ) );
+            }
+
+            //copy or check disequalities
+            std::vector< Node > addDeq;
+            for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].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 ){
+                  Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
+                  return -1;
+                }
+              }
+            }
+            if( alreadySet ){
+              n = getCurrentValue( n );
+            }
+          }else{
+            if( itmn==d_match.end() ){
+              Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;
+              //set the opposite direction
+              return addConstraint( p, vn, d_vars[v], v, true, false );
+            }else{
+              Debug("qcf-match-debug") << "  -> Both variables bound, compare" << std::endl;
+              //are they currently equal
+              return itm->second==itmn->second ? 0 : -1;
+            }
+          }
+        }else{
+          Debug("qcf-match-debug") << "  ...Variable bound to ground" << std::endl;
+          if( itm==d_match.end() ){
+
+          }else{
+            //compare ground values
+            Debug("qcf-match-debug") << "  -> Ground value, compare " << itm->second << " "<< n << std::endl;
+            return itm->second==n ? 0 : -1;
+          }
+        }
+        if( setMatch( p, v, n ) ){
+          Debug("qcf-match-debug") << "  -> success" << std::endl;
+          return 1;
+        }else{
+          Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
+          return -1;
+        }
+      }
+    }else{
+      Debug("qcf-match-debug") << "  -> redundant, variable identity" << std::endl;
+      return 0;
+    }
+  }else{
+    if( vn==v ){
+      Debug("qcf-match-debug") << "  -> fail, variable identity" << std::endl;
+      return -1;
+    }else{
+      if( doRemove ){
+        Assert( d_curr_var_deq[v].find( n )!=d_curr_var_deq[v].end() );
+        d_curr_var_deq[v].erase( n );
+        return 1;
+      }else{
+        if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){
+          //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 ){
+              Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
+              return -1;
+            }
+          }
+          d_curr_var_deq[v][n] = v;
+          Debug("qcf-match-debug") << "  -> success" << std::endl;
+          return 1;
+        }else{
+          Debug("qcf-match-debug") << "  -> redundant disequality" << std::endl;
+          return 0;
+        }
+      }
+    }
+  }
+}
+
+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;
+    d_match[v] = n;
+    return true;
+  }else{
+    return false;
+  }
+}
+
+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 ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {
+  for( int i=0; i<getNumVars(); i++ ){
+    Trace(c) << "  " << d_vars[i] << " -> ";
+    if( d_match.find( i )!=d_match.end() ){
+      Trace(c) << d_match[i];
+    }else{
+      Trace(c) << "(unassigned) ";
+    }
+    if( !d_curr_var_deq[i].empty() ){
+      Trace(c) << ", DEQ{ ";
+      for( std::map< Node, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){
+        Trace(c) << it->first << " ";
+      }
+      Trace(c) << "}";
+    }
+    Trace(c) << std::endl;
+  }
+}
+
+
+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;
+  std::vector< Node > qni_apps;
+  d_qni_size = 0;
+  if( isVar ){
+    Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() );
+    if( n.getKind()==APPLY_UF ){
+      d_type = typ_var;
+      d_type_not = true;  //implicit disequality, in disjunction at top level
+      d_n = n;
+      qni_apps.push_back( n );
+    }else{
+      //unknown term
+      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;
+      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;
+        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 ){
+            d_type = typ_invalid;
+            d_children.clear();
+            break;
+          }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;
+            Node cn = d_children[d_children.size()-1].d_n;
+            Assert( cn.getKind()==EQUAL );
+            Assert( p->d_qinfo[q].isVar( cn[0] ) || p->d_qinfo[q].isVar( cn[1] ) );
+            //make it a built-in constraint instead
+            for( unsigned i=0; i<2; i++ ){
+              if( p->d_qinfo[q].isVar( cn[i] ) ){
+                int v = p->d_qinfo[q].getVarNum( cn[i] );
+                Node cno = cn[i==0 ? 1 : 0];
+                p->d_qinfo[q].d_var_constraint[ cIsNot ? 0 : 1 ][v].push_back( cno );
+                break;
+              }
+            }
+            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 );
+          if( qni_apps.size()>0 ){
+            d_type =typ_valid_lit;
+          }else if( d_n.getKind()==EQUAL ){
+            bool isValid = true;
+            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;
+            }
+          }
+        }
+      }
+    }else{
+      //we will just evaluate
+      d_n = n;
+      d_type = typ_ground;
+    }
+    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_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(), mbas );
+
+        }
+      }
+      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() ){
+      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( 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 );
+  }
+}
+
+void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q ) {
+  d_tgt = d_type_not ? !tgt : tgt;
+  Debug("qcf-match") << "     Reset for : " << d_n << ", type : ";
+  debugPrintType( "qcf-match", d_type );
+  Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << std::endl;
+  d_qn.clear();
+  d_qni.clear();
+  d_qni_bound.clear();
+  d_child_counter = -1;
+
+  //set up processing matches
+  if( d_type==typ_ground ){
+    if( p->evaluate( d_n )==( d_tgt ? 1 : -1 ) ){
+      //store dummy variable
+      d_qn.push_back( NULL );
+    }
+  }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( d_n.getKind()==APPLY_UF );
+    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 ]
+      std::map< Node, 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 );
+      }
+    }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< Node, QcfNodeIndex >::iterator itut = p->d_uf_terms.find( f );
+      if( itut!=p->d_uf_terms.end() ){
+        d_qn.push_back( &itut->second );
+      }
+    }
+  }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;
+        }
+        break;
+      }
+    }
+    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
+      d_qn.push_back( NULL );
+    }else{
+      //reset the first child to d_tgt
+      d_child_counter = 0;
+      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;
+}
+
+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 ){
+      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 );
+          }
+        }
+      }
+      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{
+    if( d_child_counter!=-1 ){
+      bool success = false;
+      while( !success && d_child_counter>=0 ){
+        //transition system based on d_child_counter
+        if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){
+          if( (d_n.getKind()==AND)==d_tgt ){
+            //all children must match simultaneously
+            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;
+                getChild( d_child_counter )->reset( p, d_tgt, q );
+              }else{
+                success = true;
+              }
+            }else{
+              d_child_counter--;
+            }
+          }else{
+            //one child must match
+            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 << ", one match" << std::endl;
+                getChild( d_child_counter )->reset( p, d_tgt, q );
+              }else{
+                d_child_counter = -1;
+              }
+            }else{
+              success = true;
+            }
+          }
+        }else if( d_n.getKind()==IFF ){
+          //construct match based on both children
+          if( d_child_counter%2==0 ){
+            if( getChild( 0 )->getNextMatch( p, q ) ){
+              d_child_counter++;
+              getChild( 1 )->reset( p, d_child_counter==1, q );
+            }else{
+              if( d_child_counter==0 ){
+                d_child_counter = 2;
+                getChild( 0 )->reset( p, !d_tgt, q );
+              }else{
+                d_child_counter = -1;
+              }
+            }
+          }
+          if( d_child_counter%2==1 ){
+            if( getChild( 1 )->getNextMatch( p, q ) ){
+              success = true;
+            }else{
+              d_child_counter--;
+            }
+          }
+        }else if( d_n.getKind()==ITE ){
+          if( d_child_counter%2==0 ){
+            int index1 = d_child_counter==4 ? 1 : 0;
+            if( getChild( index1 )->getNextMatch( p, q ) ){
+              d_child_counter++;
+              getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, q );
+            }else{
+              if( d_child_counter==4 ){
+                d_child_counter = -1;
+              }else{
+                d_child_counter +=2;
+                getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, q );
+              }
+            }
+          }
+          if( d_child_counter%2==1 ){
+            int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2);
+            if( getChild( index2 )->getNextMatch( p, q ) ){
+              success = true;
+            }else{
+              d_child_counter--;
+            }
+          }
+        }
+      }
+      Debug("qcf-match") << "    ...finished construct match for " << d_n << ", success = " << success << std::endl;
+      return success;
+    }
+  }
+  Debug("qcf-match") << "    ...already finished for " << d_n << std::endl;
+  return false;
+}
+
+bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
+  if( !d_qn.empty() ){
+    if( d_qn[0]==NULL ){
+      d_qn.clear();
+      return true;
+    }else{
+      Assert( d_qni_size>0 );
+      bool invalidMatch;
+      do {
+        invalidMatch = false;
+        Debug("qcf-match-debug") << "       Do matching " << d_qn.size() << " " << d_qni.size() << std::endl;
+        if( d_qn.size()==d_qni.size()+1 ) {
+          int index = (int)d_qni.size();
+          //initialize
+          Node val;
+          std::map< int, int >::iterator itv = d_qni_var_num.find( index );
+          if( itv!=d_qni_var_num.end() ){
+            //get the representative variable this variable is equal to
+            int repVar = p->d_qinfo[q].getCurrentRepVar( itv->second );
+            Debug("qcf-match-debug") << "       Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;
+            //get the value the rep variable
+            std::map< int, Node >::iterator itm = p->d_qinfo[q].d_match.find( repVar );
+            if( itm!=p->d_qinfo[q].d_match.end() ){
+              val = itm->second;
+              Assert( !val.isNull() );
+              Debug("qcf-match-debug") << "       Variable is already bound to " << val << std::endl;
+            }else{
+              //binding a variable
+              d_qni_bound[index] = repVar;
+              std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.begin();
+              if( it != d_qn[index]->d_children.end() ) {
+                d_qni.push_back( it );
+                //set the match
+                if( p->d_qinfo[q].setMatch( p, d_qni_bound[index], it->first ) ){
+                  Debug("qcf-match-debug") << "       Binding variable" << std::endl;
+                  if( d_qn.size()<d_qni_size ){
+                    d_qn.push_back( &it->second );
+                  }
+                }else{
+                  Debug("qcf-match") << "       Binding variable, currently fail." << std::endl;
+                  invalidMatch = true;
+                }
+              }else{
+                Debug("qcf-match-debug") << "       Binding variable, fail, no more variables to bind" << std::endl;
+                d_qn.pop_back();
+              }
+            }
+          }else{
+            Debug("qcf-match-debug") << "       Match " << index << " is ground term" << std::endl;
+            Assert( d_qni_gterm.find( index )!=d_qni_gterm.end() );
+            Assert( d_qni_gterm_rep.find( index )!=d_qni_gterm_rep.end() );
+            val = d_qni_gterm_rep[index];
+            Assert( !val.isNull() );
+          }
+          if( !val.isNull() ){
+            //constrained by val
+            std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.find( val );
+            if( it!=d_qn[index]->d_children.end() ){
+              Debug("qcf-match-debug") << "       Match" << std::endl;
+              d_qni.push_back( it );
+              if( d_qn.size()<d_qni_size ){
+                d_qn.push_back( &it->second );
+              }
+            }else{
+              Debug("qcf-match-debug") << "       Failed to match" << std::endl;
+              d_qn.pop_back();
+            }
+          }
+        }else{
+          Assert( d_qn.size()==d_qni.size() );
+          int index = d_qni.size()-1;
+          //increment if binding this variable
+          bool success = false;
+          std::map< int, int >::iterator itb = d_qni_bound.find( index );
+          if( itb!=d_qni_bound.end() ){
+            d_qni[index]++;
+            if( d_qni[index]!=d_qn[index]->d_children.end() ){
+              success = true;
+              if( p->d_qinfo[q].setMatch( p, itb->second, d_qni[index]->first ) ){
+                Debug("qcf-match-debug") << "       Bind next variable" << std::endl;
+                if( d_qn.size()<d_qni_size ){
+                  d_qn.push_back( &d_qni[index]->second );
+                }
+              }else{
+                Debug("qcf-match-debug") << "       Bind next variable, currently fail" << std::endl;
+                invalidMatch = true;
+              }
+            }else{
+              Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;
+            }
+          }
+          //if not incrementing, move to next
+          if( !success ){
+            d_qn.pop_back();
+            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 );
+    }
+  }
+  return !d_qn.empty();
+}
+
+void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
+  if( isTrace ){
+    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_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_var: Debug(c) << "var";break;
+    case typ_var_eq: Debug(c) << "var_eq";break;
+    case typ_top: Debug(c) << "top";break;
+    }
+  }
+}
+
+
+//-------------------------------------------------- debugging
+
+
+void QuantConflictFind::debugPrint( const char * c ) {
+  //print the equivalance classes
+  Trace(c) << "----------EQ classes" << std::endl;
+  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;
+          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( std::map< Node, std::map< Node, EqRegistry * > >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){
+      bool prHead = false;
+      for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        bool print;
+        if( it->first.getKind()==APPLY_UF && it2->first.getKind()==APPLY_UF &&
+            it->first.getOperator()!=it2->first.getOperator() ){
+          print = isLessThan( it->first, it2->first );
+        }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 ) {
+  Trace(c) << "Q" << d_quant_id[q];
+}
+
+void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum ) {
+  if( n.getNumChildren()==0 ){
+    Trace(c) << n;
+  }else if( doVarNum && d_qinfo[q].d_var_num.find( n )!=d_qinfo[q].d_var_num.end() ){
+    Trace(c) << "?x" << d_qinfo[q].d_var_num[n];
+  }else{
+    Trace(c) << "(";
+    if( n.getKind()==APPLY_UF ){
+      Trace(c) << n.getOperator();
+    }else{
+      Trace(c) << n.getKind();
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      Trace(c) << " ";
+      debugPrintQuantBody( c, q, n[i] );
+    }
+    Trace(c) << ")";
+  }
+}
+
+}
+\ No newline at end of file
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
new file mode 100755
index 000000000..a43e2f70d
--- /dev/null
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -0,0 +1,235 @@
+/*********************                                                        */
+/*! \file quant_conflict_find.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief quantifiers conflict find class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef QUANT_CONFLICT_FIND
+#define QUANT_CONFLICT_FIND
+
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QcfNode;
+
+class QuantConflictFind;
+
+class QcfNodeIndex {
+public:
+  std::map< Node, QcfNodeIndex > d_children;
+  void clear() { d_children.clear(); }
+  Node addTerm( QuantConflictFind * qcf, Node n, bool doAdd = true, int index = 0 );
+  bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 );
+  void debugPrint( const char * c, int t );
+};
+
+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;
+  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+private:
+  context::Context* d_c;
+  context::CDO< bool > d_conflict;
+  //void registerAssertion( Node n );
+  void registerQuant( 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, bool isQuant = false );
+  int d_fid_count;
+  std::map< Node, int > d_fid;
+  Node mkEqNode( Node a, Node b );
+private:  //for ground terms
+  Node d_true;
+  Node d_false;
+  std::map< Node, std::map< Node, 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 );
+public:  //for quantifiers
+  //match generator
+  class MatchGen {
+  private:
+    //current children information
+    int d_child_counter;
+    //children of this object
+    std::vector< int > d_children_order;
+    unsigned getNumChildren() { return d_children.size(); }
+    MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
+    //current matching information
+    std::vector< QcfNodeIndex * > d_qn;
+    std::vector< std::map< Node, QcfNodeIndex >::iterator > d_qni;
+    bool doMatching( QuantConflictFind * p, Node q );
+    //for matching : each index is either a variable or a ground term
+    unsigned d_qni_size;
+    std::map< int, int > d_qni_var_num;
+    std::map< int, Node > d_qni_gterm;
+    std::map< int, Node > d_qni_gterm_rep;
+    std::map< int, int > d_qni_bound;
+    std::map< int, Node > d_qni_bound_cons;
+  public:
+    //type of the match generator
+    enum {
+      typ_invalid,
+      typ_ground,
+      typ_var_eq,
+      typ_valid_lit,
+      typ_valid,
+      typ_var,
+      typ_top,
+    };
+    void debugPrintType( const char * c, short typ, bool isTrace = false );
+  public:
+    MatchGen() : d_type( typ_invalid ){}
+    MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop = false, bool isVar = false );
+    bool d_tgt;
+    Node d_n;
+    std::vector< MatchGen > d_children;
+    short d_type;
+    bool d_type_not;
+    void reset_round( QuantConflictFind * p );
+    void reset( QuantConflictFind * p, bool tgt, Node q );
+    bool getNextMatch( QuantConflictFind * p, Node q );
+    bool isValid() { return d_type!=typ_invalid; }
+  };
+private:
+  //currently asserted quantifiers
+  NodeList d_qassert;
+  //info for quantifiers
+  class QuantInfo {
+  public:
+    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< 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(); }
+    int getNumVars() { return (int)d_vars.size(); }
+    Node getVar( int i ) { return d_vars[i]; }
+    MatchGen * d_mg;
+    void reset_round( QuantConflictFind * p );
+  public:
+    //current constraints
+    std::map< int, Node > d_match;
+    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 );
+    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 );
+    void debugPrintMatch( const char * c );
+  };
+  std::map< Node, QuantInfo > d_qinfo;
+private:  //for equivalence classes
+  eq::EqualityEngine * getEqualityEngine();
+  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 ) {}
+    NodeBoolMap d_diseq;
+    bool isDisequal( Node n ) { return d_diseq.find( n )!=d_diseq.end() && d_diseq[n]; }
+    void setDisequal( Node n, bool val = true ) { d_diseq[n] = val; }
+    //NodeBoolMap& getRelEqr( int index ) { return index==0 ? d_rel_eqr_e : d_rel_eqr_d; }
+  };
+  std::map< Node, EqcInfo * > d_eqc_info;
+  EqcInfo * getEqcInfo( Node n, bool doCreate = true );
+  // operator -> index(terms)
+  std::map< Node, QcfNodeIndex > d_uf_terms;
+  // eqc x operator -> index(terms)
+  std::map< Node, std::map< Node, QcfNodeIndex > > d_eqc_uf_terms;
+  // type -> list(eqc)
+  std::map< TypeNode, std::vector< Node > > d_eqcs;
+public:
+  QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
+
+  /** register assertions */
+  //void registerAssertions( std::vector< Node >& assertions );
+  /** register quantifier */
+  void registerQuantifier( Node q );
+
+public:
+  /** assert quantifier */
+  void assertNode( Node q );
+  /** new node */
+  void newEqClass( Node n );
+  /** merge */
+  void merge( Node a, Node b );
+  /** assert disequal */
+  void assertDisequal( Node a, Node b );
+  /** check */
+  void check( Theory::Effort level );
+  /** needs check */
+  bool needsCheck( Theory::Effort level );
+private:
+  void computeRelevantEqr();
+private:
+  void debugPrint( const char * c );
+  //for debugging
+  std::vector< Node > d_quants;
+  std::map< Node, int > d_quant_id;
+  void debugPrintQuant( const char * c, Node q );
+  void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true );
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 59995a510..31a95fb8a 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -239,3 +239,17 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int
     }
   }
 }
+
+void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
+  newHasPol = hasPol;
+  newPol = pol;
+  if( n.getKind()==NOT ){
+    newPol = !pol;
+  }else if( n.getKind()==IFF ){
+    newHasPol = false;
+  }else if( n.getKind()==ITE ){
+    if( child==0 ){
+      newHasPol = false;
+    }
+  }
+}
+\ No newline at end of file
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 86c7bc3a0..711144e7e 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -82,6 +82,8 @@ public:
   std::map< Node, bool > d_phase_reqs;
   std::map< Node, bool > d_phase_reqs_equality;
   std::map< Node, Node > d_phase_reqs_equality_term;
+
+  static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
 };
 
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index ecc3c02bc..3a6785d00 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -229,6 +229,32 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   return RewriteResponse(REWRITE_DONE, in);
 }
 
+Node QuantifiersRewriter::computeElimSymbols( Node body ) {
+  if( isLiteral( body ) ){
+    return body;
+  }else{
+    bool childrenChanged = false;
+    std::vector< Node > children;
+    for( unsigned i=0; i<body.getNumChildren(); i++ ){
+      Node c = computeElimSymbols( body[i] );
+      if( i==0 && ( body.getKind()==IMPLIES || body.getKind()==XOR ) ){
+        c = c.negate();
+      }
+      children.push_back( c );
+      childrenChanged = childrenChanged || c!=body[i];
+    }
+    if( body.getKind()==IMPLIES ){
+      return NodeManager::currentNM()->mkNode( OR, children );
+    }else if( body.getKind()==XOR ){
+      return NodeManager::currentNM()->mkNode( IFF, children );
+    }else if( childrenChanged ){
+      return NodeManager::currentNM()->mkNode( body.getKind(), children );
+    }else{
+      return body;
+    }
+  }
+}
+
 Node QuantifiersRewriter::computeNNF( Node body ){
   if( body.getKind()==NOT ){
     if( body[0].getKind()==NOT ){
@@ -238,10 +264,9 @@ Node QuantifiersRewriter::computeNNF( Node body ){
     }else{
       std::vector< Node > children;
       Kind k = body[0].getKind();
-      if( body[0].getKind()==OR || body[0].getKind()==IMPLIES || body[0].getKind()==AND ){
+      if( body[0].getKind()==OR || body[0].getKind()==AND ){
         for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-          Node nn = body[0].getKind()==IMPLIES && i==0 ? body[0][i] : body[0][i].notNode();
-          children.push_back( computeNNF( nn ) );
+          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 ){
@@ -376,8 +401,7 @@ Node QuantifiersRewriter::computeClause( Node n ){
       }
     }else{
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        Node nc = ( ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i] );
-        Node nn = computeClause( nc );
+        Node nn = computeClause( n[i] );
         addNodeToOrBuilder( nn, t );
       }
     }
@@ -391,10 +415,10 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui
   }else if( !forcePred && isClause( n ) ){
     return computeClause( n );
   }else{
-    Kind k = ( n.getKind()==IMPLIES ? OR : ( n.getKind()==XOR ? IFF : n.getKind() ) );
+    Kind k = n.getKind();
     NodeBuilder<> t(k);
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      Node nc = ( i==0 && ( n.getKind()==IMPLIES || n.getKind()==XOR ) ) ? n[i].notNode() : n[i];
+      Node nc = n[i];
       Node ncnf = computeCNF( nc, args, defs, k!=OR );
       if( k==OR ){
         addNodeToOrBuilder( ncnf, t );
@@ -523,7 +547,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
     bool childrenChanged = false;
     std::vector< Node > newChildren;
     for( int i=0; i<(int)body.getNumChildren(); i++ ){
-      bool newPol = ( body.getKind()==NOT || ( body.getKind()==IMPLIES && i==0 ) ) ? !pol : pol;
+      bool newPol = body.getKind()==NOT  ? !pol : pol;
       Node n = computePrenex( body[i], args, newPol );
       newChildren.push_back( n );
       if( n!=body[i] ){
@@ -661,7 +685,9 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
     if( f.getNumChildren()==3 ){
       ipl = f[2];
     }
-    if( computeOption==COMPUTE_MINISCOPING ){
+    if( computeOption==COMPUTE_ELIM_SYMBOLS ){
+      n = computeElimSymbols( n );
+    }else if( computeOption==COMPUTE_MINISCOPING ){
       //return directly
       return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) );
     }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
@@ -746,11 +772,11 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
           }
           return computeMiniscoping( args, t.constructNode(), ipl );
         }
-      }else if( body[0].getKind()==OR || body[0].getKind()==IMPLIES ){
+      }else if( body[0].getKind()==OR ){
         if( doMiniscopingAnd() ){
           NodeBuilder<> t(kind::AND);
           for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-            Node trm = ( body[0].getKind()==IMPLIES && i==0 ) ? body[0][i] : ( body[0][i].getKind()==NOT  ? body[0][i][0] : body[0][i].notNode() );
+            Node trm = body[0][i].negate();
             t << computeMiniscoping( args, trm, ipl );
           }
           return t.constructNode();
@@ -766,13 +792,13 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
         Node retVal = t;
         return retVal;
       }
-    }else if( body.getKind()==OR || body.getKind()==IMPLIES ){
+    }else if( body.getKind()==OR ){
       if( doMiniscopingNoFreeVar() ){
         Node newBody = body;
         NodeBuilder<> body_split(kind::OR);
         NodeBuilder<> tb(kind::OR);
         for( int i=0; i<(int)body.getNumChildren(); i++ ){
-          Node trm = ( body.getKind()==IMPLIES && i==0 ) ? ( body[i].getKind()==NOT ? body[i][0] : body[i].notNode() ) : body[i];
+          Node trm = body[i];
           if( hasArg( args, body[i] ) ){
             tb << trm;
           }else{
@@ -916,7 +942,9 @@ bool QuantifiersRewriter::doMiniscopingAnd(){
 }
 
 bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){
-  if( computeOption==COMPUTE_MINISCOPING ){
+  if( computeOption==COMPUTE_ELIM_SYMBOLS ){
+    return true;
+  }else if( computeOption==COMPUTE_MINISCOPING ){
     return true;
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
     return options::aggressiveMiniscopeQuant();
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 40234904f..e97d84701 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -44,6 +44,7 @@ private:
   static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed );
   static Node computeClause( Node n );
 private:
+  static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false );
   static Node computeNNF( Node body );
@@ -54,7 +55,8 @@ private:
   static Node computeSplit( Node f, Node body, std::vector< Node >& args );
 private:
   enum{
-    COMPUTE_MINISCOPING = 0,
+    COMPUTE_ELIM_SYMBOLS = 0,
+    COMPUTE_MINISCOPING,
     COMPUTE_AGGRESSIVE_MINISCOPING,
     COMPUTE_NNF,
     COMPUTE_SIMPLE_ITE_LIFT,
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 39063942d..b13e76afb 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -342,7 +342,7 @@ bool Trigger::isSimpleTrigger( Node n ){
 bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){
   if( patMap.find( n )==patMap.end() ){
     patMap[ n ] = false;
-    bool newHasPol = (n.getKind()==IFF || n.getKind()==XOR) ? false : hasPol;
+    bool newHasPol = n.getKind()==IFF ? false : hasPol;
     bool newPol = n.getKind()==NOT ? !pol : pol;
     if( tstrt==TS_MIN_TRIGGER ){
       if( n.getKind()==FORALL ){
@@ -350,9 +350,8 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
       }else{
         bool retVal = false;
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol;
           bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){
+          if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){
             retVal = true;
           }
         }
@@ -381,9 +380,8 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
       }
       if( n.getKind()!=FORALL ){
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol;
           bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){
+          if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){
             retVal = true;
           }
         }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5def2a832..2ddc83a4b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -29,6 +29,7 @@
 #include "theory/rewriterules/rr_trigger.h"
 #include "theory/quantifiers/bounded_integers.h"
 #include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/uf/options.h"
 
 using namespace std;
@@ -61,6 +62,12 @@ d_lemmas_produced_c(u){
   }
 
   //add quantifiers modules
+  if( options::quantConflictFind() ){
+    d_qcf = new quantifiers::QuantConflictFind( this, c);
+    d_modules.push_back( d_qcf );
+  }else{
+    d_qcf = NULL;
+  }
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
     //the instantiation must set incomplete flag unless finite model finding is turned on
     d_inst_engine = new quantifiers::InstantiationEngine( this, !options::finiteModelFind() );
@@ -393,6 +400,10 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
   return getInstantiation( f, vars, terms );
 }
 
+Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
+  return getInstantiation( f, d_term_db->d_inst_constants[f], terms );
+}
+
 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
   if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
     if( d_inst_match_trie[f]->existsInstMatch( this, f, m, modEq, modInst ) ){
@@ -497,12 +508,13 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool
 
 void QuantifiersEngine::flushLemmas( OutputChannel* out ){
   if( !d_lemmas_waiting.empty() ){
+    if( !out ){
+      out = &getOutputChannel();
+    }
     //take default output channel if none is provided
     d_hasAddedLemma = true;
     for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
-      if( out ){
-        out->lemma( d_lemmas_waiting[i] );
-      }
+      out->lemma( d_lemmas_waiting[i] );
     }
     d_lemmas_waiting.clear();
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 6de13ff3c..ee7e6e6d8 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -52,7 +52,7 @@ public:
   /* Call during quantifier engine's check */
   virtual void check( Theory::Effort e ) = 0;
   /* Called for new quantifiers */
-  virtual void registerQuantifier( Node n ) = 0;
+  virtual void registerQuantifier( Node q ) = 0;
   virtual void assertNode( Node n ) = 0;
   virtual void propagate( Theory::Effort level ){}
   virtual Node getNextDecisionRequest() { return TNode::null(); }
@@ -66,6 +66,7 @@ namespace quantifiers {
   class InstantiationEngine;
   class ModelEngine;
   class BoundedIntegers;
+  class QuantConflictFind;
   class RewriteEngine;
 }/* CVC4::theory::quantifiers */
 
@@ -105,6 +106,8 @@ private:
   quantifiers::ModelEngine* d_model_engine;
   /** bounded integers utility */
   quantifiers::BoundedIntegers * d_bint;
+  /** Conflict find mechanism for quantifiers */
+  quantifiers::QuantConflictFind* d_qcf;
   /** rewrite rules utility */
   quantifiers::RewriteEngine * d_rr_engine;
 private:
@@ -165,6 +168,8 @@ public:
   EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
   /** get bounded integers utility */
   quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
+  /** Conflict find mechanism for quantifiers */
+  quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
 public:
   /** initialize */
   void finishInit();
@@ -194,6 +199,8 @@ public:
   Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
   /** get instantiation */
   Node getInstantiation( Node f, InstMatch& m );
+  /** get instantiation */
+  Node getInstantiation( Node f, std::vector< Node >& terms );
   /** exist instantiation ? */
   bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
   /** add lemma lem */
@@ -207,7 +214,7 @@ public:
   /** has added lemma */
   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
   /** flush lemmas */
-  void flushLemmas( OutputChannel* out );
+  void flushLemmas( OutputChannel* out = NULL );
   /** get number of waiting lemmas */
   int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
 public:
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c598fd01b..e55d6a9c9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -75,12 +75,18 @@ void TheoryEngine::finishInit() {
 
 void TheoryEngine::eqNotifyNewClass(TNode t){
   d_quantEngine->addTermToDatabase( t );
+  if( d_logicInfo.isQuantified() && options::quantConflictFind() ){
+    d_quantEngine->getConflictFind()->newEqClass( t );
+  }
 }
 
 void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
   //TODO: add notification to efficient E-matching
-  if (d_logicInfo.isQuantified()) {
+  if( d_logicInfo.isQuantified() ){
     d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
+    if( options::quantConflictFind() ){
+      d_quantEngine->getConflictFind()->merge( t1, t2 );
+    }
   }
 }
 
@@ -89,7 +95,11 @@ void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
 }
 
 void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
-
+  if( d_logicInfo.isQuantified() ){
+    if( options::quantConflictFind() ){
+      d_quantEngine->getConflictFind()->assertDisequal( t1, t2 );
+    }
+  }
 }
 
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 92469aa31..8f292e008 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -39,6 +39,7 @@
 #include "util/statistics_registry.h"
 #include "util/cvc4_assert.h"
 #include "util/sort_inference.h"
+#include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/bv/bv_to_bool.h"
 #include "theory/atom_requests.h"
@@ -778,10 +779,10 @@ private:
   UnconstrainedSimplifier* d_unconstrainedSimp;
 
   /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
-  theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; 
+  theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor;
 public:
 
-  void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
+  void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
   Node ppSimpITE(TNode assertion);
   /** Returns false if an assertion simplified to false. */
   bool donePPSimpITE(std::vector<Node>& assertions);
@@ -790,6 +791,8 @@ public:
 
   SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
 
+  theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
+
   SortInference* getSortInference() { return &d_sortInfer; }
 private:
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 3ed1ea985..51783c1e3 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -44,8 +44,6 @@ protected:
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
-  typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDList<bool> BoolList;
   typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap;
 public:
   /** information for incremental conflict/clique finding for a particular sort */
author	Andrew Reynolds <andrew.j.reynolds@gmail.com>	2014-01-10 02:04:51 -0600
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>	2014-01-10 02:07:39 -0600
commit	841b7951f41f399859afab13a81e04599308da61 (patch)
tree	8c6eb70b498b0a01f00c1a77b96d00ff2f61c21b /src/theory
parent	18fed5592fb769d12ba2901a0fdc00c5c02863b9 (diff)