From dea679ce032c130d210d54c2e5482f95db1ff04a Mon Sep 17 00:00:00 2001
From: Clark Barrett <clarkbarrett@google.com>
Date: Thu, 23 Apr 2015 09:43:52 -0700
Subject: A few more minor updates to match google repository with CVC4
 repository (mostly whitespace differences).

---
 src/theory/quantifiers/quant_conflict_find.cpp | 4454 ++++++++++++------------
 1 file changed, 2227 insertions(+), 2227 deletions(-)

(limited to 'src/theory/quantifiers/quant_conflict_find.cpp')

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index d465df4c0..18bffe908 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1,2227 +1,2227 @@
-/*********************                                                        */
-/*! \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-2014  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"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/trigger.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace std;
-
-namespace CVC4 {
-
-
-
-void QuantInfo::initialize( Node q, Node qn ) {
-  d_q = q;
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    d_match.push_back( TNode::null() );
-    d_match_term.push_back( TNode::null() );
-  }
-
-  //register the variables
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    d_var_num[q[0][i]] = i;
-    d_vars.push_back( q[0][i] );
-    d_var_types.push_back( q[0][i].getType() );
-  }
-
-  registerNode( qn, true, true );
-
-
-  Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
-  d_mg = new MatchGen( this, qn );
-
-  if( d_mg->isValid() ){
-    /*
-    for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
-      if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){
-        Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;
-        d_mg->setInvalid();
-        break;
-      }
-    }
-    */
-    if( d_mg->isValid() ){
-      for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
-        if( d_vars[j].getKind()!=BOUND_VARIABLE ){
-          d_var_mg[j] = NULL;
-          bool is_tsym = false;
-          if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){
-            is_tsym = true;
-            d_tsym_vars.push_back( j );
-          }
-          if( !is_tsym || options::qcfTConstraint() ){
-            d_var_mg[j] = new MatchGen( this, d_vars[j], true );
-          }
-          if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
-            Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
-            d_mg->setInvalid();
-            break;
-          }else{
-            std::vector< int > bvars;
-            d_var_mg[j]->determineVariableOrder( this, bvars );
-          }
-        }
-      }
-      if( d_mg->isValid() ){
-        std::vector< int > bvars;
-        d_mg->determineVariableOrder( this, bvars );
-      }
-    }
-  }else{
-    Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
-  }
-  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
-}
-
-void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
-  Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
-  if( n.getKind()==FORALL ){
-    registerNode( n[1], hasPol, pol, true );
-  }else{
-    if( !MatchGen::isHandledBoolConnective( n ) ){
-      if( n.hasBoundVar() ){
-        //literals
-        if( n.getKind()==EQUAL ){
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            flatten( n[i], beneathQuant );
-          }
-        }else if( MatchGen::isHandledUfTerm( n ) ){
-          flatten( n, beneathQuant );
-        }else if( n.getKind()==ITE ){
-          for( unsigned i=1; i<=2; i++ ){
-            flatten( n[i], beneathQuant );
-          }
-          registerNode( n[0], false, pol, beneathQuant );
-        }else if( options::qcfTConstraint() ){
-          //a theory-specific predicate
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            flatten( n[i], beneathQuant );
-          }
-        }
-      }
-    }else{
-      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;
-        registerNode( n[i], newHasPol, newPol, beneathQuant );
-      }
-    }
-  }
-}
-
-void QuantInfo::flatten( Node n, bool beneathQuant ) {
-  Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
-  if( n.hasBoundVar() ){
-    if( n.getKind()==BOUND_VARIABLE ){
-      d_inMatchConstraint[n] = true;
-    }
-    //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){
-    if( d_var_num.find( n )==d_var_num.end() ){
-      Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
-      d_var_num[n] = d_vars.size();
-      d_vars.push_back( n );
-      d_var_types.push_back( n.getType() );
-      d_match.push_back( TNode::null() );
-      d_match_term.push_back( TNode::null() );
-      if( n.getKind()==ITE ){
-        registerNode( n, false, false );
-      }else{
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          flatten( n[i], beneathQuant );
-        }
-      }
-    }else{
-      Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
-    }
-  }else{
-    Trace("qcf-qregister-debug2") << "...is ground." << std::endl;
-  }
-}
-
-
-void QuantInfo::reset_round( QuantConflictFind * p ) {
-  for( unsigned i=0; i<d_match.size(); i++ ){
-    d_match[i] = TNode::null();
-    d_match_term[i] = TNode::null();
-  }
-  d_curr_var_deq.clear();
-  d_tconstraints.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 );
-  for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
-    it->second->reset_round( p );
-  }
-  //now, reset for matching
-  d_mg->reset( p, false, this );
-}
-
-int QuantInfo::getCurrentRepVar( int v ) {
-  if( v!=-1 && !d_match[v].isNull() ){
-    int vn = getVarNum( d_match[v] );
-    if( vn!=-1 ){
-      //int vr = getCurrentRepVar( vn );
-      //d_match[v] = d_vars[vr];
-      //return vr;
-      return getCurrentRepVar( vn );
-    }
-  }
-  return v;
-}
-
-TNode QuantInfo::getCurrentValue( TNode n ) {
-  int v = getVarNum( n );
-  if( v==-1 ){
-    return n;
-  }else{
-    if( d_match[v].isNull() ){
-      return n;
-    }else{
-      Assert( getVarNum( d_match[v] )!=v );
-      return getCurrentValue( d_match[v] );
-    }
-  }
-}
-
-TNode QuantInfo::getCurrentExpValue( TNode n ) {
-  int v = getVarNum( n );
-  if( v==-1 ){
-    return n;
-  }else{
-    if( d_match[v].isNull() ){
-      return n;
-    }else{
-      Assert( getVarNum( d_match[v] )!=v );
-      if( d_match_term[v].isNull() ){
-        return getCurrentValue( d_match[v] );
-      }else{
-        return d_match_term[v];
-      }
-    }
-  }
-}
-
-bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {
-  //check disequalities
-  std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
-  if( itd!=d_curr_var_deq.end() ){
-    for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
-      Node cv = getCurrentValue( it->first );
-      Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
-      if( cv==n ){
-        return false;
-      }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){
-        //they must actually be disequal if we are looking for conflicts
-        if( !p->areDisequal( n, cv ) ){
-          //TODO : check for entailed disequal
-
-          return false;
-        }
-      }
-    }
-  }
-  return true;
-}
-
-int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode 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 QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode 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( doRemove || 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, TNode >::iterator itmn = d_match.find( vn );
-          if( d_match[vn]==d_vars[v] ){
-            return addConstraint( p, vn, d_vars[v], v, true, true );
-          }else{
-            //unsetting variables equal
-            std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( vn );
-            if( itd!=d_curr_var_deq.end() ){
-              //remove disequalities owned by this
-              std::vector< TNode > remDeq;
-              for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.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[v] = TNode::null();
-        return 1;
-      }else{
-        //std::map< int, TNode >::iterator itm = d_match.find( v );
-
-        if( vn!=-1 ){
-          Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;
-          //std::map< int, TNode >::iterator itmn = d_match.find( vn );
-          if( d_match[v].isNull() ){
-            //setting variables equal
-            bool alreadySet = false;
-            if( !d_match[vn].isNull() ){
-              alreadySet = true;
-              Assert( !isVar( d_match[vn] ) );
-            }
-
-            //copy or check disequalities
-            std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
-            if( itd!=d_curr_var_deq.end() ){
-              for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
-                Node dv = getCurrentValue( it->first );
-                if( !alreadySet ){
-                  if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){
-                    d_curr_var_deq[vn][dv] = v;
-                  }
-                }else{
-                  if( !p->areMatchDisequal( d_match[vn], dv ) ){
-                    Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
-                    return -1;
-                  }
-                }
-              }
-            }
-            if( alreadySet ){
-              n = getCurrentValue( n );
-            }
-          }else{
-            if( d_match[vn].isNull() ){
-              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 p->areMatchEqual( d_match[v], d_match[vn] ) ? 0 : -1;
-            }
-          }
-        }else{
-          Debug("qcf-match-debug") << "  ...Variable bound to ground" << std::endl;
-          if( d_match[v].isNull() ){
-          }else{
-            //compare ground values
-            Debug("qcf-match-debug") << "  -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
-            return p->areMatchEqual( d_match[v], 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, TNode >::iterator itm = d_match.find( v );
-          if( !d_match[v].isNull() ){
-            TNode nv = getCurrentValue( n );
-            if( !p->areMatchDisequal( nv, d_match[v] ) ){
-              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 QuantInfo::isConstrainedVar( int v ) {
-  if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){
-    return true;
-  }else{
-    Node vv = getVar( v );
-    //for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
-    for( unsigned i=0; i<d_match.size(); i++ ){
-      if( d_match[i]==vv ){
-        return true;
-      }
-    }
-    for( std::map< int, std::map< TNode, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){
-      for( std::map< TNode, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        if( it2->first==vv ){
-          return true;
-        }
-      }
-    }
-    return false;
-  }
-}
-
-bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode 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 QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
-  for( int i=0; i<getNumVars(); i++ ){
-    //std::map< int, TNode >::iterator it = d_match.find( i );
-    if( !d_match[i].isNull() ){
-      if( !getCurrentCanBeEqual( p, i, d_match[i], p->d_effort==QuantConflictFind::effort_conflict ) ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {
-  if( !d_tconstraints.empty() ){
-    //check constraints
-    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
-      //apply substitution to the tconstraint
-      Node cons = it->first.substitute( p->getTermDatabase()->d_vars[d_q].begin(),
-                                        p->getTermDatabase()->d_vars[d_q].end(),
-                                        terms.begin(), terms.end() );
-      cons = it->second ? cons : cons.negate();
-      if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
-  Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
-  Node rew = Rewriter::rewrite( lit );
-  if( rew==p->d_false ){
-    Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;
-    return false;
-  }else if( rew!=p->d_true ){
-    //if checking for conflicts, we must be sure that the constraint is entailed
-    if( chEnt ){
-      //check if it is entailed
-      Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
-      std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );
-      ++(p->d_statistics.d_entailment_checks);
-      Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
-      if( !et.first ){
-        Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
-        return false;
-      }else{
-        return true;
-      }
-    }else{
-      Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;
-      return true;
-    }
-  }else{
-    Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;
-    return true;
-  }
-}
-
-bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {
-  //assign values for variables that were unassigned (usually not necessary, but handles corner cases)
-  bool doFail = false;
-  bool success = true;
-  if( doContinue ){
-    doFail = true;
-    success = false;
-  }else{
-    //solve for interpreted symbol matches
-    //   this breaks the invariant that all introduced constraints are over existing terms
-    for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){
-      int index = d_tsym_vars[i];
-      TNode v = getCurrentValue( d_vars[index] );
-      int slv_v = -1;
-      if( v==d_vars[index] ){
-        slv_v = index;
-      }
-      Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;
-      if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){
-        Kind k = d_vars[index].getKind();
-        std::vector< TNode > children;
-        for( unsigned j=0; j<d_vars[index].getNumChildren(); j++ ){
-          int vn = getVarNum( d_vars[index][j] );
-          if( vn!=-1 ){
-            TNode vv = getCurrentValue( d_vars[index][j] );
-            if( vv==d_vars[index][j] ){
-              //we will assign this
-              if( slv_v==-1 ){
-                Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
-                slv_v = vn;
-                if( p->d_effort!=QuantConflictFind::effort_conflict ){
-                  break;
-                }
-              }else{
-                Node z = p->getZero( k );
-                if( !z.isNull() ){
-                  Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
-                  assigned.push_back( vn );
-                  if( !setMatch( p, vn, z ) ){
-                    success = false;
-                    break;
-                  }
-                }
-              }
-            }else{
-              Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;
-              children.push_back( vv );
-            }
-          }else{
-            Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl;
-            children.push_back( d_vars[index][j] );
-          }
-        }
-        if( success ){
-          if( slv_v!=-1 ){
-            Node lhs;
-            if( children.empty() ){
-              lhs = p->getZero( k );
-            }else if( children.size()==1 ){
-              lhs = children[0];
-            }else{
-              lhs = NodeManager::currentNM()->mkNode( k, children );
-            }
-            Node sum;
-            if( v==d_vars[index] ){
-              sum = lhs;
-            }else{
-              if( p->d_effort==QuantConflictFind::effort_conflict ){
-                Kind kn = k;
-                if( d_vars[index].getKind()==PLUS ){
-                  kn = MINUS;
-                }
-                if( kn!=k ){
-                  sum = NodeManager::currentNM()->mkNode( kn, v, lhs );
-                }
-              }
-            }
-            if( !sum.isNull() ){
-              assigned.push_back( slv_v );
-              Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
-              if( !setMatch( p, slv_v, sum ) ){
-                success = false;
-              }
-              p->d_tempCache.push_back( sum );
-            }
-          }else{
-            //must show that constraint is met
-            Node sum = NodeManager::currentNM()->mkNode( k, children );
-            Node eq = sum.eqNode( v );
-            if( !entailmentTest( p, eq ) ){
-              success = false;
-            }
-            p->d_tempCache.push_back( sum );
-          }
-        }
-      }
-
-      if( !success ){
-        break;
-      }
-    }
-    if( success ){
-      //check what is left to assign
-      d_unassigned.clear();
-      d_unassigned_tn.clear();
-      std::vector< int > unassigned[2];
-      std::vector< TypeNode > unassigned_tn[2];
-      for( int i=0; i<getNumVars(); i++ ){
-        if( d_match[i].isNull() ){
-          int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
-          unassigned[rindex].push_back( i );
-          unassigned_tn[rindex].push_back( getVar( i ).getType() );
-          assigned.push_back( i );
-        }
-      }
-      d_unassigned_nvar = unassigned[0].size();
-      for( unsigned i=0; i<2; i++ ){
-        d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );
-        d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );
-      }
-      d_una_eqc_count.clear();
-      d_una_index = 0;
-    }
-  }
-
-  if( !d_unassigned.empty() && ( success || doContinue ) ){
-    Trace("qcf-check") << "Assign to unassigned..." << std::endl;
-    do {
-      if( doFail ){
-        Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
-      }
-      bool invalidMatch = false;
-      while( ( d_una_index>=0 && (int)d_una_index<(int)d_unassigned.size() ) || invalidMatch || doFail ){
-        invalidMatch = false;
-        if( !doFail && d_una_index==(int)d_una_eqc_count.size() ){
-          //check if it has now been assigned
-          if( d_una_index<d_unassigned_nvar ){
-            if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
-              d_una_eqc_count.push_back( -1 );
-            }else{
-              d_var_mg[ d_unassigned[d_una_index] ]->reset( p, true, this );
-              d_una_eqc_count.push_back( 0 );
-            }
-          }else{
-            d_una_eqc_count.push_back( 0 );
-          }
-        }else{
-          bool failed = false;
-          if( !doFail ){
-            if( d_una_index<d_unassigned_nvar ){
-              if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
-                Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;
-                d_una_index++;
-              }else if( d_var_mg[d_unassigned[d_una_index]]->getNextMatch( p, this ) ){
-                Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl;
-                d_una_index++;
-              }else{
-                failed = true;
-                Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;
-              }
-            }else{
-              Assert( doFail || d_una_index==(int)d_una_eqc_count.size()-1 );
-              if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){
-                int currIndex = d_una_eqc_count[d_una_index];
-                d_una_eqc_count[d_una_index]++;
-                Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;
-                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){
-                  d_match_term[d_unassigned[d_una_index]] = TNode::null();
-                  Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
-                  d_una_index++;
-                }else{
-                  Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl;
-                  invalidMatch = true;
-                }
-              }else{
-                failed = true;
-                Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl;
-              }
-            }
-          }
-          if( doFail || failed ){
-            do{
-              if( !doFail ){
-                d_una_eqc_count.pop_back();
-              }else{
-                doFail = false;
-              }
-              d_una_index--;
-            }while( d_una_index>=0 && d_una_eqc_count[d_una_index]==-1 );
-          }
-        }
-      }
-      success = d_una_index>=0;
-      if( success ){
-        doFail = true;
-        Trace("qcf-check-unassign") << "  Try: " << std::endl;
-        for( unsigned i=0; i<d_unassigned.size(); i++ ){
-          int ui = d_unassigned[i];
-          if( !d_match[ui].isNull() ){
-            Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
-          }
-        }
-      }
-    }while( success && isMatchSpurious( p ) );
-  }
-  if( success ){
-    for( unsigned i=0; i<d_unassigned.size(); i++ ){
-      int ui = d_unassigned[i];
-      if( !d_match[ui].isNull() ){
-        Trace("qcf-check") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
-      }
-    }
-    return true;
-  }else{
-    for( unsigned i=0; i<assigned.size(); i++ ){
-      d_match[ assigned[i] ] = TNode::null();
-    }
-    assigned.clear();
-    return false;
-  }
-}
-
-void QuantInfo::getMatch( std::vector< Node >& terms ){
-  for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
-    //Node cv = qi->getCurrentValue( qi->d_match[i] );
-    int repVar = getCurrentRepVar( i );
-    Node cv;
-    //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
-    if( !d_match_term[repVar].isNull() ){
-      cv = d_match_term[repVar];
-    }else{
-      cv = d_match[repVar];
-    }
-    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_match[i] << std::endl;
-    terms.push_back( cv );
-  }
-}
-
-void QuantInfo::revertMatch( std::vector< int >& assigned ) {
-  for( unsigned i=0; i<assigned.size(); i++ ){
-    d_match[ assigned[i] ] = TNode::null();
-  }
-}
-
-void QuantInfo::debugPrintMatch( const char * c ) {
-  for( int i=0; i<getNumVars(); i++ ){
-    Trace(c) << "  " << d_vars[i] << " -> ";
-    if( !d_match[i].isNull() ){
-      Trace(c) << d_match[i];
-    }else{
-      Trace(c) << "(unassigned) ";
-    }
-    if( !d_curr_var_deq[i].empty() ){
-      Trace(c) << ", DEQ{ ";
-      for( std::map< TNode, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){
-        Trace(c) << it->first << " ";
-      }
-      Trace(c) << "}";
-    }
-    if( !d_match_term[i].isNull() && d_match_term[i]!=d_match[i] ){
-      Trace(c) << ", EXP : " << d_match_term[i];
-    }
-    Trace(c) <<  std::endl;
-  }
-  if( !d_tconstraints.empty() ){
-    Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;
-    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
-      Trace(c) << "   " << it->first << " -> " << it->second << std::endl;
-    }
-  }
-}
-
-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
-  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
-  std::vector< Node > qni_apps;
-  d_qni_size = 0;
-  if( isVar ){
-    Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
-    if( n.getKind()==ITE ){
-      d_type = typ_ite_var;
-      d_type_not = false;
-      d_n = n;
-      d_children.push_back( MatchGen( qi, d_n[0] ) );
-      if( d_children[0].isValid() ){
-        d_type = typ_ite_var;
-        for( unsigned i=1; i<=2; i++ ){
-          Node nn = n.eqNode( n[i] );
-          d_children.push_back( MatchGen( qi, nn ) );
-          d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 );
-          if( !d_children[d_children.size()-1].isValid() ){
-            setInvalid();
-            break;
-          }
-        }
-      }else{
-        d_type = typ_invalid;
-      }
-    }else{
-      d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
-      d_qni_var_num[0] = qi->getVarNum( n );
-      d_qni_size++;
-      d_type_not = false;
-      d_n = n;
-      //Node f = getOperator( n );
-      for( unsigned j=0; j<d_n.getNumChildren(); j++ ){
-        Node nn = d_n[j];
-        Trace("qcf-qregister-debug") << "  " << d_qni_size;
-        if( qi->isVar( nn ) ){
-          int v = qi->d_var_num[nn];
-          Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
-          d_qni_var_num[d_qni_size] = v;
-          //qi->addFuncParent( v, f, j );
-        }else{
-          Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
-          d_qni_gterm[d_qni_size] = nn;
-        }
-        d_qni_size++;
-      }
-    }
-  }else{
-    if( n.hasBoundVar() ){
-      d_type_not = false;
-      d_n = n;
-      if( d_n.getKind()==NOT ){
-        d_n = d_n[0];
-        d_type_not = !d_type_not;
-      }
-
-      if( isHandledBoolConnective( d_n ) ){
-        //non-literals
-        d_type = typ_formula;
-        for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
-          if( d_n.getKind()!=FORALL || i==1 ){
-            d_children.push_back( MatchGen( qi, d_n[i], false ) );
-            if( !d_children[d_children.size()-1].isValid() ){
-              setInvalid();
-              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( isHandledUfTerm( d_n ) ){
-          Assert( qi->isVar( d_n ) );
-          d_type = typ_pred;
-        }else if( d_n.getKind()==BOUND_VARIABLE ){
-          Assert( d_n.getType().isBoolean() );
-          d_type = typ_bool_var;
-        }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
-          for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
-            if( d_n[i].hasBoundVar() ){
-              if( !qi->isVar( d_n[i] ) ){
-                Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;
-              }
-              Assert( qi->isVar( d_n[i] ) );
-              if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){
-                d_qni_var_num[i+1] = qi->d_var_num[d_n[i]];
-              }
-            }else{
-              d_qni_gterm[i] = d_n[i];
-            }
-          }
-          d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;
-          Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
-        }
-      }
-    }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(), mgs );
-        //}
-      //}
-    //}
-  }
-  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 MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) {
-  int v = qi->getVarNum( n );
-  if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){
-    cbvars.push_back( v );
-  }
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    collectBoundVar( qi, n[i], cbvars );
-  }
-}
-
-void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {
-  Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl;
-  bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );
-  std::map< int, std::vector< int > > c_to_vars;
-  std::map< int, std::vector< int > > vars_to_c;
-  std::map< int, int > vb_count;
-  std::map< int, int > vu_count;
-  std::vector< bool > assigned;
-  Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
-  for( unsigned i=0; i<d_children.size(); i++ ){
-    collectBoundVar( qi, d_children[i].d_n, c_to_vars[i] );
-    assigned.push_back( false );
-    vb_count[i] = 0;
-    vu_count[i] = 0;
-    for( unsigned j=0; j<c_to_vars[i].size(); j++ ){
-      int v = c_to_vars[i][j];
-      vars_to_c[v].push_back( i );
-      if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
-        vu_count[i]++;
-        if( !isCom ){
-          bvars.push_back( v );
-        }
-      }else{
-        vb_count[i]++;
-      }
-    }
-  }
-  if( isCom ){
-    //children that bind the least number of unbound variables go first
-    do {
-      int min_score = -1;
-      int min_score_index = -1;
-      for( unsigned i=0; i<d_children.size(); i++ ){
-        if( !assigned[i] ){
-          int score = vu_count[i];
-          if( min_score==-1 || score<min_score ){
-            min_score = score;
-            min_score_index = i;
-          }
-        }
-      }
-      Trace("qcf-qregister-debug") << "...assign child " << min_score_index << "/" << d_children.size() << std::endl;
-      Assert( min_score_index!=-1 );
-      //add to children order
-      d_children_order.push_back( min_score_index );
-      assigned[min_score_index] = true;
-      //if( vb_count[min_score_index]==0 ){
-      //  d_independent.push_back( min_score_index );
-      //}
-      //determine order internal to children
-      d_children[min_score_index].determineVariableOrder( qi, bvars );
-      Trace("qcf-qregister-debug")  << "...bind variables" << std::endl;
-      //now, make it a bound variable
-      for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
-        int v = c_to_vars[min_score_index][i];
-        if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
-          for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
-            int vc = vars_to_c[v][j];
-            vu_count[vc]--;
-            vb_count[vc]++;
-          }
-          bvars.push_back( v );
-        }
-      }
-      Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
-    }while( d_children_order.size()!=d_children.size() );
-    Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl;
-  }else{
-    for( unsigned i=0; i<d_children.size(); i++ ){
-      d_children_order.push_back( i );
-      d_children[i].determineVariableOrder( qi, bvars );
-    }
-  }
-}
-
-
-void MatchGen::reset_round( QuantConflictFind * p ) {
-  d_wasSet = false;
-  for( unsigned i=0; i<d_children.size(); i++ ){
-    d_children[i].reset_round( p );
-  }
-  for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
-    d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
-  }
-  if( d_type==typ_ground ){
-    int e = p->evaluate( d_n );
-    if( e==1 ){
-      d_ground_eval[0] = p->d_true;
-    }else if( e==-1 ){
-      d_ground_eval[0] = p->d_false;
-    }
-  }else if( d_type==typ_eq ){
-    for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
-      if( !d_n[i].hasBoundVar() ){
-        d_ground_eval[i] = p->evaluateTerm( d_n[i] );
-      }
-    }
-  }
-  d_qni_bound_cons.clear();
-  d_qni_bound_cons_var.clear();
-  d_qni_bound.clear();
-}
-
-void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
-  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() << " " << d_children_order.size() << std::endl;
-  d_qn.clear();
-  d_qni.clear();
-  d_qni_bound.clear();
-  d_child_counter = -1;
-  d_tgt_orig = d_tgt;
-
-  //set up processing matches
-  if( d_type==typ_invalid ){
-    //do nothing
-  }else if( d_type==typ_ground ){
-    if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){
-      d_child_counter = 0;
-    }
-  }else if( d_type==typ_bool_var ){
-    //get current value of the variable
-    TNode n = qi->getCurrentValue( d_n );
-    int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );
-    if( vn==-1 ){
-      //evaluate the value, see if it is compatible
-      int e = p->evaluate( n );
-      if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
-        d_child_counter = 0;
-      }
-    }else{
-      //unassigned, set match to true/false
-      d_qni_bound[0] = vn;
-      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false );
-      d_child_counter = 0;
-    }
-    if( d_child_counter==0 ){
-      d_qn.push_back( NULL );
-    }
-  }else if( d_type==typ_var ){
-    Assert( isHandledUfTerm( d_n ) );
-    Node f = getOperator( p, d_n );
-    Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;
-    TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f );
-    if( qni!=NULL ){
-      d_qn.push_back( qni );
-    }
-    d_matched_basis = false;
-  }else if( d_type==typ_tsym || d_type==typ_tconstraint ){
-    for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){
-      int repVar = qi->getCurrentRepVar( it->second );
-      if( qi->d_match[repVar].isNull() ){
-        Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl;
-        d_qni_bound[it->first] = repVar;
-      }
-    }
-    d_qn.push_back( NULL );
-  }else if( d_type==typ_pred || d_type==typ_eq ){
-    //add initial constraint
-    Node nn[2];
-    int vn[2];
-    if( d_type==typ_pred ){
-      nn[0] = qi->getCurrentValue( d_n );
-      vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) );
-      nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );
-      vn[1] = -1;
-      d_tgt = true;
-    }else{
-      for( unsigned i=0; i<2; i++ ){
-        TNode nc;
-        std::map< int, TNode >::iterator it = d_qni_gterm_rep.find( i );
-        if( it!=d_qni_gterm_rep.end() ){
-          nc = it->second;
-        }else{
-          nc = d_n[i];
-        }
-        nn[i] = qi->getCurrentValue( nc );
-        vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) );
-      }
-    }
-    bool success;
-    if( vn[0]==-1 && vn[1]==-1 ){
-      //Trace("qcf-explain") << "    reset : " << d_n << " check ground values " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl;
-      Debug("qcf-match-debug") << "       reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;
-      //just compare values
-      if( d_tgt ){
-        success = p->areMatchEqual( nn[0], nn[1] );
-      }else{
-        if( p->d_effort==QuantConflictFind::effort_conflict ){
-          success = p->areDisequal( nn[0], nn[1] );
-        }else{
-          success = p->areMatchDisequal( nn[0], nn[1] );
-        }
-      }
-    }else{
-      //otherwise, add a constraint to a variable
-      if( vn[1]!=-1 && vn[0]==-1 ){
-        //swap
-        Node t = nn[1];
-        nn[1] = nn[0];
-        nn[0] = t;
-        vn[0] = vn[1];
-        vn[1] = -1;
-      }
-      Debug("qcf-match-debug") << "       reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;
-      //add some constraint
-      int addc = qi->addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );
-      success = addc!=-1;
-      //if successful and non-redundant, store that we need to cleanup this
-      if( addc==1 ){
-        //Trace("qcf-explain") << "       reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl;
-        for( unsigned i=0; i<2; i++ ){
-          if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){
-            d_qni_bound[vn[i]] = vn[i];
-          }
-        }
-        d_qni_bound_cons[vn[0]] = nn[1];
-        d_qni_bound_cons_var[vn[0]] = vn[1];
-      }
-    }
-    //if successful, we will bind values to variables
-    if( success ){
-      d_qn.push_back( NULL );
-    }
-  }else{
-    if( d_children.empty() ){
-      //add dummy
-      d_qn.push_back( NULL );
-    }else{
-      if( d_tgt && d_n.getKind()==FORALL ){
-        //do nothing
-      }else{
-        //reset the first child to d_tgt
-        d_child_counter = 0;
-        getChild( d_child_counter )->reset( p, d_tgt, qi );
-      }
-    }
-  }
-  d_binding = false;
-  d_wasSet = true;
-  Debug("qcf-match") << "     reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;
-}
-
-bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
-  Debug("qcf-match") << "     Get next match for : " << d_n << ", type = ";
-  debugPrintType( "qcf-match", d_type );
-  Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;
-  if( d_type==typ_invalid || d_type==typ_ground ){
-    if( d_child_counter==0 ){
-      d_child_counter = -1;
-      return true;
-    }else{
-      d_wasSet = false;
-      return false;
-    }
-  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var || d_type==typ_tconstraint || d_type==typ_tsym ){
-    bool success = false;
-    bool terminate = false;
-    do {
-      bool doReset = false;
-      bool doFail = false;
-      if( !d_binding ){
-        if( doMatching( p, qi ) ){
-          Debug("qcf-match-debug") << "     - Matching succeeded" << std::endl;
-          d_binding = true;
-          d_binding_it = d_qni_bound.begin();
-          doReset = true;
-          //for tconstraint, add constraint
-          if( d_type==typ_tconstraint ){
-            std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n );
-            if( it==qi->d_tconstraints.end() ){
-              qi->d_tconstraints[d_n] = d_tgt;
-              //store that we added this constraint
-              d_qni_bound_cons[0] = d_n;
-            }else if( d_tgt!=it->second ){
-              success = false;
-              terminate = true;
-            }
-          }
-        }else{
-          Debug("qcf-match-debug") << "     - Matching failed" << std::endl;
-          success = false;
-          terminate = true;
-        }
-      }else{
-        doFail = true;
-      }
-      if( d_binding ){
-        //also need to create match for each variable we bound
-        success = true;
-        Debug("qcf-match-debug") << "     Produce matches for bound variables by " << d_n << ", type = ";
-        debugPrintType( "qcf-match-debug", d_type );
-        Debug("qcf-match-debug") << "..." << std::endl;
-
-        while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){
-          std::map< int, MatchGen * >::iterator itm;
-          if( !doFail ){
-            Debug("qcf-match-debug") << "       check variable " << d_binding_it->second << std::endl;
-            itm = qi->d_var_mg.find( d_binding_it->second );
-          }
-          if( doFail || ( d_binding_it->first!=0 && itm!=qi->d_var_mg.end() ) ){
-            Debug("qcf-match-debug") << "       we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;
-            if( doReset ){
-              itm->second->reset( p, true, qi );
-            }
-            if( doFail || !itm->second->getNextMatch( p, qi ) ){
-              do {
-                if( d_binding_it==d_qni_bound.begin() ){
-                  Debug("qcf-match-debug") << "       failed." << std::endl;
-                  success = false;
-                }else{
-                  --d_binding_it;
-                  Debug("qcf-match-debug") << "       decrement..." << std::endl;
-                }
-              }while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) );
-              doReset = false;
-              doFail = false;
-            }else{
-              Debug("qcf-match-debug") << "       increment..." << std::endl;
-              ++d_binding_it;
-              doReset = true;
-            }
-          }else{
-            Debug("qcf-match-debug") << "       skip..." << d_binding_it->second << std::endl;
-            ++d_binding_it;
-            doReset = true;
-          }
-        }
-        if( !success ){
-          d_binding = false;
-        }else{
-          terminate = true;
-          if( d_binding_it==d_qni_bound.begin() ){
-            d_binding = false;
-          }
-        }
-      }
-    }while( !terminate );
-    //if not successful, clean up the variables you bound
-    if( !success ){
-      if( d_type==typ_eq || d_type==typ_pred ){
-        //clean up the constraints you added
-        for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){
-          if( !it->second.isNull() ){
-            Debug("qcf-match") << "       Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;
-            std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );
-            int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;
-            //Trace("qcf-explain") << "       cleanup: " << d_n << " remove constraint " << it->first << " -> " << it->second << " (vn=" << vn << ")" << ", d_tgt = " << d_tgt << std::endl;
-            qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );
-          }
-        }
-        d_qni_bound_cons.clear();
-        d_qni_bound_cons_var.clear();
-        d_qni_bound.clear();
-      }else{
-        //clean up the matches you set
-        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<qi->getNumVars() );
-          qi->d_match[ it->second ] = TNode::null();
-          qi->d_match_term[ it->second ] = TNode::null();
-        }
-        d_qni_bound.clear();
-      }
-      if( d_type==typ_tconstraint ){
-        //remove constraint if applicable
-        if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){
-          qi->d_tconstraints.erase( d_n );
-          d_qni_bound_cons.clear();
-        }
-      }
-      /*
-      if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){
-        d_matched_basis = true;
-        Node f = getOperator( d_n );
-        TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f );
-        if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){
-          success = true;
-          d_qni_bound[0] = d_qni_var_num[0];
-        }
-      }
-      */
-    }
-    Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
-    d_wasSet = success;
-    return success;
-  }else if( d_type==typ_formula || d_type==typ_ite_var ){
-    bool success = false;
-    if( d_child_counter<0 ){
-      if( d_child_counter<-1 ){
-        success = true;
-        d_child_counter = -1;
-      }
-    }else{
-      while( !success && d_child_counter>=0 ){
-        //transition system based on d_child_counter
-        if( 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, qi ) ){
-              if( d_child_counter<(int)(getNumChildren()-1) ){
-                d_child_counter++;
-                Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << std::endl;
-                getChild( d_child_counter )->reset( p, d_tgt, qi );
-              }else{
-                success = true;
-              }
-            }else{
-              //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){
-              //  d_child_counter--;
-              //}else{
-              d_child_counter--;
-              //}
-            }
-          }else{
-            //one child must match
-            if( !getChild( d_child_counter )->getNextMatch( p, qi ) ){
-              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, qi );
-              }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, qi ) ){
-              d_child_counter++;
-              getChild( 1 )->reset( p, d_child_counter==1, qi );
-            }else{
-              if( d_child_counter==0 ){
-                d_child_counter = 2;
-                getChild( 0 )->reset( p, !d_tgt, qi );
-              }else{
-                d_child_counter = -1;
-              }
-            }
-          }
-          if( d_child_counter>=0 && d_child_counter%2==1 ){
-            if( getChild( 1 )->getNextMatch( p, qi ) ){
-              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, qi ) ){
-              d_child_counter++;
-              getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );
-            }else{
-              if( d_child_counter==4 || ( d_type==typ_ite_var && d_child_counter==2 ) ){
-                d_child_counter = -1;
-              }else{
-                d_child_counter +=2;
-                getChild( d_child_counter==2 ? 0 : 1 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );
-              }
-            }
-          }
-          if( d_child_counter>=0 && d_child_counter%2==1 ){
-            int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2);
-            if( getChild( index2 )->getNextMatch( p, qi ) ){
-              success = true;
-            }else{
-              d_child_counter--;
-            }
-          }
-        }else if( d_n.getKind()==FORALL ){
-          if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
-            success = true;
-          }else{
-            d_child_counter = -1;
-          }
-        }
-      }
-        d_wasSet = success;
-      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 MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ) {
-  if( d_type==typ_eq ){
-    Node n[2];
-    for( unsigned i=0; i<2; i++ ){
-      Trace("qcf-explain") << "Explain term " << d_n[i] << "..." << std::endl;
-      n[i] = getExplanationTerm( p, qi, d_n[i], exp );
-    }
-    Node eq = n[0].eqNode( n[1] );
-    if( !d_tgt_orig ){
-      eq = eq.negate();
-    }
-    exp.push_back( eq );
-    Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << eq << ", set = " << d_wasSet << std::endl;
-    return true;
-  }else if( d_type==typ_pred ){
-    Trace("qcf-explain") << "Explain term " << d_n << "..." << std::endl;
-    Node n = getExplanationTerm( p, qi, d_n, exp );
-    if( !d_tgt_orig ){
-      n = n.negate();
-    }
-    exp.push_back( n );
-    Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << n << ", set = " << d_wasSet << std::endl;
-    return true;
-  }else if( d_type==typ_formula ){
-    Trace("qcf-explain") << "Explanation get for " << d_n << ", counter = " << d_child_counter << ", tgt = " << d_tgt_orig << ", set = " << d_wasSet << std::endl;
-    if( d_n.getKind()==OR || d_n.getKind()==AND ){
-      if( (d_n.getKind()==AND)==d_tgt ){
-        for( unsigned i=0; i<getNumChildren(); i++ ){
-          if( !getChild( i )->getExplanation( p, qi, exp ) ){
-            return false;
-          }
-        }
-      }else{
-        return getChild( d_child_counter )->getExplanation( p, qi, exp );
-      }
-    }else if( d_n.getKind()==IFF ){
-      for( unsigned i=0; i<2; i++ ){
-        if( !getChild( i )->getExplanation( p, qi, exp ) ){
-          return false;
-        }
-      }
-    }else if( d_n.getKind()==ITE ){
-      for( unsigned i=0; i<3; i++ ){
-        bool isActive = ( ( i==0 && d_child_counter!=5 ) ||
-                          ( i==1 && d_child_counter!=( d_tgt ? 3 : 1 ) ) ||
-                          ( i==2 && d_child_counter!=( d_tgt ? 1 : 3 ) ) );
-        if( isActive ){
-          if( !getChild( i )->getExplanation( p, qi, exp ) ){
-            return false;
-          }
-        }
-      }
-    }else{
-      return false;
-    }
-    return true;
-  }else{
-    return false;
-  }
-}
-
-Node MatchGen::getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ) {
-  Node v = qi->getCurrentExpValue( t );
-  if( isHandledUfTerm( t ) ){
-    for( unsigned i=0; i<t.getNumChildren(); i++ ){
-      Node vi = getExplanationTerm( p, qi, t[i], exp );
-      if( vi!=v[i] ){
-        Node eq = vi.eqNode( v[i] );
-        if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
-          Trace("qcf-explain") << "  add : " << eq << "." << std::endl;
-          exp.push_back( eq );
-        }
-      }
-    }
-  }
-  return v;
-}
-
-bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
-  if( !d_qn.empty() ){
-    if( d_qn[0]==NULL ){
-      d_qn.clear();
-      return true;
-    }else{
-      Assert( d_type==typ_var );
-      Assert( d_qni_size>0 );
-      bool invalidMatch;
-      do {
-        invalidMatch = false;
-        Debug("qcf-match-debug") << "       Do matching " << d_n << " " << d_qn.size() << " " << d_qni.size() << std::endl;
-        if( d_qn.size()==d_qni.size()+1 ) {
-          int index = (int)d_qni.size();
-          //initialize
-          TNode 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 = qi->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, TNode >::iterator itm = qi->d_match.find( repVar );
-            if( !qi->d_match[repVar].isNull() ){
-              val = qi->d_match[repVar];
-              Debug("qcf-match-debug") << "       Variable is already bound to " << val << std::endl;
-            }else{
-              //binding a variable
-              d_qni_bound[index] = repVar;
-              std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.begin();
-              if( it != d_qn[index]->d_data.end() ) {
-                d_qni.push_back( it );
-                //set the match
-                if( it->first.getType().isSubtypeOf( qi->d_var_types[repVar] ) && qi->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< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.find( val );
-            if( it!=d_qn[index]->d_data.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_data.end() ){
-              success = true;
-              if( qi->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{
-              qi->d_match[ itb->second ] = TNode::null();
-              qi->d_match_term[ itb->second ] = TNode::null();
-              Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;
-            }
-          }else{
-            //TODO : if it equal to something else, also try that
-          }
-          //if not incrementing, move to next
-          if( !success ){
-            d_qn.pop_back();
-            d_qni.pop_back();
-          }
-        }
-      }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );
-      if( d_qni.size()==d_qni_size ){
-        //Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
-        //Debug("qcf-match-debug") << "       We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;
-        Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
-        TNode t = d_qni[d_qni.size()-1]->second.d_data.begin()->first;
-        Debug("qcf-match-debug") << "       " << d_n << " matched " << t << std::endl;
-        qi->d_match_term[d_qni_var_num[0]] = t;
-        //set the match terms
-        for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
-          Debug("qcf-match-debug") << "       position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;
-          //if( it->second<(int)qi->d_q[0].getNumChildren() ){   //if it is an actual variable, we are interested in knowing the actual term
-          if( it->first>0 ){
-            Assert( !qi->d_match[ it->second ].isNull() );
-            Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );
-            qi->d_match_term[it->second] = t[it->first-1];
-          }
-          //}
-        }
-      }
-    }
-  }
-  return !d_qn.empty();
-}
-
-void 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_eq: Trace(c) << "eq";break;
-    case typ_pred: Trace(c) << "pred";break;
-    case typ_formula: Trace(c) << "formula";break;
-    case typ_var: Trace(c) << "var";break;
-    case typ_ite_var: Trace(c) << "ite_var";break;
-    case typ_bool_var: Trace(c) << "bool_var";break;
-    }
-  }else{
-    switch( typ ){
-    case typ_invalid: Debug(c) << "invalid";break;
-    case typ_ground: Debug(c) << "ground";break;
-    case typ_eq: Debug(c) << "eq";break;
-    case typ_pred: Debug(c) << "pred";break;
-    case typ_formula: Debug(c) << "formula";break;
-    case typ_var: Debug(c) << "var";break;
-    case typ_ite_var: Debug(c) << "ite_var";break;
-    case typ_bool_var: Debug(c) << "bool_var";break;
-    }
-  }
-}
-
-void MatchGen::setInvalid() {
-  d_type = typ_invalid;
-  d_children.clear();
-}
-
-bool MatchGen::isHandledBoolConnective( TNode n ) {
-  return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT );
-}
-
-bool MatchGen::isHandledUfTerm( TNode n ) {
-  //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
-  //       n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
-  return inst::Trigger::isAtomicTriggerKind( n.getKind() );
-}
-
-Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {
-  if( isHandledUfTerm( n ) ){
-    return p->getTermDatabase()->getOperator( n );
-  }else{
-    return Node::null();
-  }
-}
-
-bool MatchGen::isHandled( TNode n ) {
-  if( n.getKind()!=BOUND_VARIABLE && n.hasBoundVar() ){
-    if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){
-      return false;
-    }
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !isHandled( n[i] ) ){
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
-
-QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
-QuantifiersModule( qe ),
-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);
-}
-
-Node QuantConflictFind::mkEqNode( Node a, Node b ) {
-  if( a.getType().isBoolean() ){
-    return a.iffNode( b );
-  }else{
-    return a.eqNode( b );
-  }
-}
-
-//-------------------------------------------------- registration
-
-void QuantConflictFind::registerQuantifier( Node q ) {
-  if( d_quantEngine->hasOwnership( q, this ) ){
-    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;
-    //make QcfNode structure
-    Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
-    d_qinfo[q].initialize( q, q[1] );
-
-    //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") << "Done registering quantifier." << std::endl;
-  }
-}
-
-int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
-  int ret = 0;
-  if( n.getKind()==EQUAL ){
-    Node n1 = evaluateTerm( n[0] );
-    Node n2 = evaluateTerm( n[1] );
-    Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;
-    if( areEqual( n1, n2 ) ){
-      ret = 1;
-    }else if( areDisequal( n1, n2 ) ){
-      ret = -1;
-    }
-    //else if( d_effort>QuantConflictFind::effort_conflict ){
-    //  ret = -1;
-    //}
-  }else if( MatchGen::isHandledUfTerm( n ) ){  //predicate
-    Node nn = evaluateTerm( n );
-    Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;
-    if( areEqual( nn, d_true ) ){
-      ret = 1;
-    }else if( areEqual( nn, d_false ) ){
-      ret = -1;
-    }
-    //else if( d_effort>QuantConflictFind::effort_conflict ){
-    //  ret = -1;
-    //}
-  }else if( n.getKind()==NOT ){
-    return -evaluate( n[0] );
-  }else if( n.getKind()==ITE ){
-    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;
-}
-
-short QuantConflictFind::getMaxQcfEffort() {
-  if( options::qcfMode()==QCF_CONFLICT_ONLY ){
-    return effort_conflict;
-  }else if( options::qcfMode()==QCF_PROP_EQ ){
-    return effort_prop_eq;
-  }else if( options::qcfMode()==QCF_MC ){
-    return effort_mc;
-  }else{
-    return 0;
-  }
-}
-
-bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
-  //if( d_effort==QuantConflictFind::effort_mc ){
-  //  return n1==n2 || !areDisequal( n1, n2 );
-  //}else{
-  return n1==n2;
-  //}
-}
-
-bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
-  //if( d_effort==QuantConflictFind::effort_conflict ){
-  //  return areDisequal( n1, n2 );
-  //}else{
-  return n1!=n2;
-  //}
-}
-
-//-------------------------------------------------- handling assertions / eqc
-
-void QuantConflictFind::assertNode( Node q ) {
-  if( d_quantEngine->hasOwnership( q, this ) ){
-    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 );
-    //}
-  }
-}
-
-Node QuantConflictFind::evaluateTerm( Node n ) {
-  if( MatchGen::isHandledUfTerm( n ) ){
-    Node f = MatchGen::getOperator( this, n );
-    Node nn;
-    if( getEqualityEngine()->hasTerm( n ) ){
-      nn = getTermDatabase()->existsTerm( f, n );
-    }else{
-      std::vector< TNode > args;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node c = evaluateTerm( n[i] );
-        args.push_back( c );
-      }
-      nn = getTermDatabase()->d_func_map_trie[f].existsTerm( args );
-    }
-    if( !nn.isNull() ){
-      Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;
-      return getRepresentative( nn );
-    }else{
-      Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;
-      return n;
-    }
-  }else if( n.getKind()==ITE ){
-    int v = evaluate( n[0], false, false );
-    if( v==1 ){
-      return evaluateTerm( n[1] );
-    }else if( v==-1 ){
-      return evaluateTerm( n[2] );
-    }
-  }
-  return getRepresentative( n );
-}
-
-/** new node */
-void QuantConflictFind::newEqClass( Node n ) {
-
-}
-
-/** merge */
-void QuantConflictFind::merge( Node a, Node b ) {
-
-}
-
-/** assert disequal */
-void QuantConflictFind::assertDisequal( Node a, Node b ) {
-
-}
-
-//-------------------------------------------------- check function
-
-bool QuantConflictFind::needsCheck( Theory::Effort level ) {
-  bool performCheck = false;
-  if( options::quantConflictFind() && !d_conflict ){
-    if( level==Theory::EFFORT_LAST_CALL ){
-      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
-    }else if( level==Theory::EFFORT_FULL ){
-      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
-    }else if( level==Theory::EFFORT_STANDARD ){
-      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
-    }
-  }
-  return performCheck;
-}
-
-void QuantConflictFind::reset_round( Theory::Effort level ) {
-  d_needs_computeRelEqr = true;
-}
-
-/** check */
-void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
-  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
-    Trace("qcf-check") << "QCF : check : " << level << std::endl;
-    if( d_conflict ){
-      Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
-      if( level>=Theory::EFFORT_FULL ){
-        Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
-        //Assert( false );
-      }
-    }else{
-      int addedLemmas = 0;
-      ++(d_statistics.d_inst_rounds);
-      double clSet = 0;
-      int prevEt = 0;
-      if( Trace.isOn("qcf-engine") ){
-        prevEt = d_statistics.d_entailment_checks.getData();
-        clSet = double(clock())/double(CLOCKS_PER_SEC);
-        Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;
-      }
-      computeRelevantEqr();
-
-      //determine order for quantified formulas
-      std::vector< Node > qorder;
-      std::map< Node, bool > qassert;
-      //mark which are asserted
-      for( unsigned i=0; i<d_qassert.size(); i++ ){
-        qassert[d_qassert[i]] = true;
-      }
-      //add which ones are specified in the order
-      for( unsigned i=0; i<d_quant_order.size(); i++ ){
-        Node n = d_quant_order[i];
-        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() && qassert.find( n )!=qassert.end() ){
-          qorder.push_back( n );
-        }
-      }
-      d_quant_order.clear();
-      d_quant_order.insert( d_quant_order.begin(), qorder.begin(), qorder.end() );
-      //add remaining
-      for( unsigned i=0; i<d_qassert.size(); i++ ){
-        Node n = d_qassert[i];
-        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() ){
-          qorder.push_back( n );
-        }
-      }
-
-      if( Trace.isOn("qcf-debug") ){
-        Trace("qcf-debug") << std::endl;
-        debugPrint("qcf-debug");
-        Trace("qcf-debug") << std::endl;
-      }
-      short end_e = getMaxQcfEffort();
-      for( short e = effort_conflict; e<=end_e; e++ ){
-        d_effort = e;
-        Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
-        for( unsigned j=0; j<qorder.size(); j++ ){
-          Node q = qorder[j];
-          QuantInfo * qi = &d_qinfo[q];
-
-          Assert( d_qinfo.find( q )!=d_qinfo.end() );
-          if( qi->d_mg->isValid() ){
-            Trace("qcf-check") << "Check quantified formula ";
-            debugPrintQuant("qcf-check", q);
-            Trace("qcf-check") << " : " << q << "..." << std::endl;
-
-            Trace("qcf-check-debug") << "Reset round..." << std::endl;
-            qi->reset_round( this );
-            //try to make a matches making the body false
-            Trace("qcf-check-debug") << "Get next match..." << std::endl;
-            while( qi->d_mg->getNextMatch( this, qi ) ){
-              Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
-              qi->debugPrintMatch("qcf-inst");
-              Trace("qcf-inst") << std::endl;
-              std::vector< int > assigned;
-              if( !qi->isMatchSpurious( this ) ){
-                if( qi->completeMatch( this, assigned ) ){
-                  std::vector< Node > terms;
-                  qi->getMatch( terms );
-                  if( !qi->isTConstraintSpurious( this, terms ) ){
-                    if( Debug.isOn("qcf-check-inst") ){
-                      //if( e==effort_conflict ){
-                      Node inst = d_quantEngine->getInstantiation( q, terms );
-                      Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
-                      Assert( evaluate( inst )!=1 );
-                      Assert( evaluate( inst )==-1 || e>effort_conflict );
-                      //}
-                    }
-                    if( d_quantEngine->addInstantiation( q, terms, false ) ){
-                      Trace("qcf-check") << "   ... Added instantiation" << std::endl;
-                      Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
-                      qi->debugPrintMatch("qcf-inst");
-                      Trace("qcf-inst") << std::endl;
-                      ++addedLemmas;
-                      if( e==effort_conflict ){
-                        d_quant_order.insert( d_quant_order.begin(), q );
-                        d_conflict.set( true );
-                        ++(d_statistics.d_conflict_inst);
-                        break;
-                      }else if( e==effort_prop_eq ){
-                        ++(d_statistics.d_prop_inst);
-                      }
-                    }else{
-                      Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
-                      //Assert( false );
-                    }
-                  }
-                  //clean up assigned
-                  qi->revertMatch( assigned );
-                  d_tempCache.clear();
-                }else{
-                  Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
-                }
-              }else{
-                Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;
-              }
-            }
-            if( d_conflict ){
-              break;
-            }
-          }
-        }
-        if( addedLemmas>0 ){
-          break;
-        }
-      }
-      if( Trace.isOn("qcf-engine") ){
-        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-        Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
-        if( addedLemmas>0 ){
-          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) );
-          Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
-        }
-        Trace("qcf-engine") << std::endl;
-        int currEt = d_statistics.d_entailment_checks.getData();
-        if( currEt!=prevEt ){
-          Trace("qcf-engine") << "  Entailment checks = " << ( currEt - prevEt ) << std::endl;
-        }
-      }
-      Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
-    }
-  }
-}
-
-void QuantConflictFind::computeRelevantEqr() {
-  if( d_needs_computeRelEqr ){
-    d_needs_computeRelEqr = false;
-    Trace("qcf-check") << "Compute relevant equalities..." << std::endl;
-    //d_uf_terms.clear();
-    //d_eqc_uf_terms.clear();
-    d_eqcs.clear();
-    d_model_basis.clear();
-    //d_arg_reps.clear();
-    //double clSet = 0;
-    //if( Trace.isOn("qcf-opt") ){
-    //  clSet = double(clock())/double(CLOCKS_PER_SEC);
-    //}
-
-    //long nTermst = 0;
-    //long nTerms = 0;
-    //long nEqc = 0;
-
-    //which nodes are irrelevant for disequality matches
-    std::map< TNode, bool > irrelevant_dnode;
-    //now, store matches
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
-    while( !eqcs_i.isFinished() ){
-      //nEqc++;
-      Node r = (*eqcs_i);
-      if( getTermDatabase()->hasTermCurrent( r ) ){
-        TypeNode rtn = r.getType();
-        if( options::qcfMode()==QCF_MC ){
-          std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );
-          if( itt==d_eqcs.end() ){
-            Node mb = getTermDatabase()->getModelBasisTerm( rtn );
-            if( !getEqualityEngine()->hasTerm( mb ) ){
-              Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;
-              Assert( false );
-            }
-            Node mbr = getRepresentative( mb );
-            if( mbr!=r ){
-              d_eqcs[rtn].push_back( mbr );
-            }
-            d_eqcs[rtn].push_back( r );
-            d_model_basis[rtn] = mb;
-          }else{
-            itt->second.push_back( r );
-          }
-        }else{
-          d_eqcs[rtn].push_back( r );
-        }
-      }
-      ++eqcs_i;
-    }
-    /*
-    if( Trace.isOn("qcf-opt") ){
-      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
-      Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;
-      Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;
-      Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;
-    }
-    */
-  }
-}
-
-
-//-------------------------------------------------- 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;
-  }
-}
-
-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) << ")";
-  }
-}
-
-QuantConflictFind::Statistics::Statistics():
-  d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
-  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),
-  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),
-  d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
-{
-  StatisticsRegistry::registerStat(&d_inst_rounds);
-  StatisticsRegistry::registerStat(&d_conflict_inst);
-  StatisticsRegistry::registerStat(&d_prop_inst);
-  StatisticsRegistry::registerStat(&d_entailment_checks);
-}
-
-QuantConflictFind::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_inst_rounds);
-  StatisticsRegistry::unregisterStat(&d_conflict_inst);
-  StatisticsRegistry::unregisterStat(&d_prop_inst);
-  StatisticsRegistry::unregisterStat(&d_entailment_checks);
-}
-
-TNode QuantConflictFind::getZero( Kind k ) {
-  std::map< Kind, Node >::iterator it = d_zero.find( k );
-  if( it==d_zero.end() ){
-    Node nn;
-    if( k==PLUS ){
-      nn = NodeManager::currentNM()->mkConst( Rational(0) );
-    }
-    d_zero[k] = nn;
-    return nn;
-  }else{
-    return it->second;
-  }
-}
-
-
-}
+/*********************                                                        */
+/*! \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-2014  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"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/trigger.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+
+
+void QuantInfo::initialize( Node q, Node qn ) {
+  d_q = q;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    d_match.push_back( TNode::null() );
+    d_match_term.push_back( TNode::null() );
+  }
+
+  //register the variables
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    d_var_num[q[0][i]] = i;
+    d_vars.push_back( q[0][i] );
+    d_var_types.push_back( q[0][i].getType() );
+  }
+
+  registerNode( qn, true, true );
+
+
+  Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
+  d_mg = new MatchGen( this, qn );
+
+  if( d_mg->isValid() ){
+    /*
+    for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+      if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){
+        Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;
+        d_mg->setInvalid();
+        break;
+      }
+    }
+    */
+    if( d_mg->isValid() ){
+      for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
+        if( d_vars[j].getKind()!=BOUND_VARIABLE ){
+          d_var_mg[j] = NULL;
+          bool is_tsym = false;
+          if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){
+            is_tsym = true;
+            d_tsym_vars.push_back( j );
+          }
+          if( !is_tsym || options::qcfTConstraint() ){
+            d_var_mg[j] = new MatchGen( this, d_vars[j], true );
+          }
+          if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
+            Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
+            d_mg->setInvalid();
+            break;
+          }else{
+            std::vector< int > bvars;
+            d_var_mg[j]->determineVariableOrder( this, bvars );
+          }
+        }
+      }
+      if( d_mg->isValid() ){
+        std::vector< int > bvars;
+        d_mg->determineVariableOrder( this, bvars );
+      }
+    }
+  }else{
+    Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
+  }
+  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
+}
+
+void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
+  Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
+  if( n.getKind()==FORALL ){
+    registerNode( n[1], hasPol, pol, true );
+  }else{
+    if( !MatchGen::isHandledBoolConnective( n ) ){
+      if( n.hasBoundVar() ){
+        //literals
+        if( n.getKind()==EQUAL ){
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){
+            flatten( n[i], beneathQuant );
+          }
+        }else if( MatchGen::isHandledUfTerm( n ) ){
+          flatten( n, beneathQuant );
+        }else if( n.getKind()==ITE ){
+          for( unsigned i=1; i<=2; i++ ){
+            flatten( n[i], beneathQuant );
+          }
+          registerNode( n[0], false, pol, beneathQuant );
+        }else if( options::qcfTConstraint() ){
+          //a theory-specific predicate
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){
+            flatten( n[i], beneathQuant );
+          }
+        }
+      }
+    }else{
+      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;
+        registerNode( n[i], newHasPol, newPol, beneathQuant );
+      }
+    }
+  }
+}
+
+void QuantInfo::flatten( Node n, bool beneathQuant ) {
+  Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
+  if( n.hasBoundVar() ){
+    if( n.getKind()==BOUND_VARIABLE ){
+      d_inMatchConstraint[n] = true;
+    }
+    //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){
+    if( d_var_num.find( n )==d_var_num.end() ){
+      Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
+      d_var_num[n] = d_vars.size();
+      d_vars.push_back( n );
+      d_var_types.push_back( n.getType() );
+      d_match.push_back( TNode::null() );
+      d_match_term.push_back( TNode::null() );
+      if( n.getKind()==ITE ){
+        registerNode( n, false, false );
+      }else{
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          flatten( n[i], beneathQuant );
+        }
+      }
+    }else{
+      Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
+    }
+  }else{
+    Trace("qcf-qregister-debug2") << "...is ground." << std::endl;
+  }
+}
+
+
+void QuantInfo::reset_round( QuantConflictFind * p ) {
+  for( unsigned i=0; i<d_match.size(); i++ ){
+    d_match[i] = TNode::null();
+    d_match_term[i] = TNode::null();
+  }
+  d_curr_var_deq.clear();
+  d_tconstraints.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 );
+  for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
+    it->second->reset_round( p );
+  }
+  //now, reset for matching
+  d_mg->reset( p, false, this );
+}
+
+int QuantInfo::getCurrentRepVar( int v ) {
+  if( v!=-1 && !d_match[v].isNull() ){
+    int vn = getVarNum( d_match[v] );
+    if( vn!=-1 ){
+      //int vr = getCurrentRepVar( vn );
+      //d_match[v] = d_vars[vr];
+      //return vr;
+      return getCurrentRepVar( vn );
+    }
+  }
+  return v;
+}
+
+TNode QuantInfo::getCurrentValue( TNode n ) {
+  int v = getVarNum( n );
+  if( v==-1 ){
+    return n;
+  }else{
+    if( d_match[v].isNull() ){
+      return n;
+    }else{
+      Assert( getVarNum( d_match[v] )!=v );
+      return getCurrentValue( d_match[v] );
+    }
+  }
+}
+
+TNode QuantInfo::getCurrentExpValue( TNode n ) {
+  int v = getVarNum( n );
+  if( v==-1 ){
+    return n;
+  }else{
+    if( d_match[v].isNull() ){
+      return n;
+    }else{
+      Assert( getVarNum( d_match[v] )!=v );
+      if( d_match_term[v].isNull() ){
+        return getCurrentValue( d_match[v] );
+      }else{
+        return d_match_term[v];
+      }
+    }
+  }
+}
+
+bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {
+  //check disequalities
+  std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
+  if( itd!=d_curr_var_deq.end() ){
+    for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
+      Node cv = getCurrentValue( it->first );
+      Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
+      if( cv==n ){
+        return false;
+      }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){
+        //they must actually be disequal if we are looking for conflicts
+        if( !p->areDisequal( n, cv ) ){
+          //TODO : check for entailed disequal
+
+          return false;
+        }
+      }
+    }
+  }
+  return true;
+}
+
+int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode 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 QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode 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( doRemove || 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, TNode >::iterator itmn = d_match.find( vn );
+          if( d_match[vn]==d_vars[v] ){
+            return addConstraint( p, vn, d_vars[v], v, true, true );
+          }else{
+            //unsetting variables equal
+            std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( vn );
+            if( itd!=d_curr_var_deq.end() ){
+              //remove disequalities owned by this
+              std::vector< TNode > remDeq;
+              for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.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[v] = TNode::null();
+        return 1;
+      }else{
+        //std::map< int, TNode >::iterator itm = d_match.find( v );
+
+        if( vn!=-1 ){
+          Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;
+          //std::map< int, TNode >::iterator itmn = d_match.find( vn );
+          if( d_match[v].isNull() ){
+            //setting variables equal
+            bool alreadySet = false;
+            if( !d_match[vn].isNull() ){
+              alreadySet = true;
+              Assert( !isVar( d_match[vn] ) );
+            }
+
+            //copy or check disequalities
+            std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
+            if( itd!=d_curr_var_deq.end() ){
+              for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
+                Node dv = getCurrentValue( it->first );
+                if( !alreadySet ){
+                  if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){
+                    d_curr_var_deq[vn][dv] = v;
+                  }
+                }else{
+                  if( !p->areMatchDisequal( d_match[vn], dv ) ){
+                    Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
+                    return -1;
+                  }
+                }
+              }
+            }
+            if( alreadySet ){
+              n = getCurrentValue( n );
+            }
+          }else{
+            if( d_match[vn].isNull() ){
+              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 p->areMatchEqual( d_match[v], d_match[vn] ) ? 0 : -1;
+            }
+          }
+        }else{
+          Debug("qcf-match-debug") << "  ...Variable bound to ground" << std::endl;
+          if( d_match[v].isNull() ){
+          }else{
+            //compare ground values
+            Debug("qcf-match-debug") << "  -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
+            return p->areMatchEqual( d_match[v], 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, TNode >::iterator itm = d_match.find( v );
+          if( !d_match[v].isNull() ){
+            TNode nv = getCurrentValue( n );
+            if( !p->areMatchDisequal( nv, d_match[v] ) ){
+              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 QuantInfo::isConstrainedVar( int v ) {
+  if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){
+    return true;
+  }else{
+    Node vv = getVar( v );
+    //for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
+    for( unsigned i=0; i<d_match.size(); i++ ){
+      if( d_match[i]==vv ){
+        return true;
+      }
+    }
+    for( std::map< int, std::map< TNode, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){
+      for( std::map< TNode, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        if( it2->first==vv ){
+          return true;
+        }
+      }
+    }
+    return false;
+  }
+}
+
+bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode 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 QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
+  for( int i=0; i<getNumVars(); i++ ){
+    //std::map< int, TNode >::iterator it = d_match.find( i );
+    if( !d_match[i].isNull() ){
+      if( !getCurrentCanBeEqual( p, i, d_match[i], p->d_effort==QuantConflictFind::effort_conflict ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {
+  if( !d_tconstraints.empty() ){
+    //check constraints
+    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
+      //apply substitution to the tconstraint
+      Node cons = it->first.substitute( p->getTermDatabase()->d_vars[d_q].begin(),
+                                        p->getTermDatabase()->d_vars[d_q].end(),
+                                        terms.begin(), terms.end() );
+      cons = it->second ? cons : cons.negate();
+      if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
+  Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
+  Node rew = Rewriter::rewrite( lit );
+  if( rew==p->d_false ){
+    Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;
+    return false;
+  }else if( rew!=p->d_true ){
+    //if checking for conflicts, we must be sure that the constraint is entailed
+    if( chEnt ){
+      //check if it is entailed
+      Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
+      std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );
+      ++(p->d_statistics.d_entailment_checks);
+      Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
+      if( !et.first ){
+        Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
+        return false;
+      }else{
+        return true;
+      }
+    }else{
+      Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;
+      return true;
+    }
+  }else{
+    Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;
+    return true;
+  }
+}
+
+bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {
+  //assign values for variables that were unassigned (usually not necessary, but handles corner cases)
+  bool doFail = false;
+  bool success = true;
+  if( doContinue ){
+    doFail = true;
+    success = false;
+  }else{
+    //solve for interpreted symbol matches
+    //   this breaks the invariant that all introduced constraints are over existing terms
+    for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){
+      int index = d_tsym_vars[i];
+      TNode v = getCurrentValue( d_vars[index] );
+      int slv_v = -1;
+      if( v==d_vars[index] ){
+        slv_v = index;
+      }
+      Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;
+      if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){
+        Kind k = d_vars[index].getKind();
+        std::vector< TNode > children;
+        for( unsigned j=0; j<d_vars[index].getNumChildren(); j++ ){
+          int vn = getVarNum( d_vars[index][j] );
+          if( vn!=-1 ){
+            TNode vv = getCurrentValue( d_vars[index][j] );
+            if( vv==d_vars[index][j] ){
+              //we will assign this
+              if( slv_v==-1 ){
+                Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
+                slv_v = vn;
+                if( p->d_effort!=QuantConflictFind::effort_conflict ){
+                  break;
+                }
+              }else{
+                Node z = p->getZero( k );
+                if( !z.isNull() ){
+                  Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
+                  assigned.push_back( vn );
+                  if( !setMatch( p, vn, z ) ){
+                    success = false;
+                    break;
+                  }
+                }
+              }
+            }else{
+              Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;
+              children.push_back( vv );
+            }
+          }else{
+            Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl;
+            children.push_back( d_vars[index][j] );
+          }
+        }
+        if( success ){
+          if( slv_v!=-1 ){
+            Node lhs;
+            if( children.empty() ){
+              lhs = p->getZero( k );
+            }else if( children.size()==1 ){
+              lhs = children[0];
+            }else{
+              lhs = NodeManager::currentNM()->mkNode( k, children );
+            }
+            Node sum;
+            if( v==d_vars[index] ){
+              sum = lhs;
+            }else{
+              if( p->d_effort==QuantConflictFind::effort_conflict ){
+                Kind kn = k;
+                if( d_vars[index].getKind()==PLUS ){
+                  kn = MINUS;
+                }
+                if( kn!=k ){
+                  sum = NodeManager::currentNM()->mkNode( kn, v, lhs );
+                }
+              }
+            }
+            if( !sum.isNull() ){
+              assigned.push_back( slv_v );
+              Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
+              if( !setMatch( p, slv_v, sum ) ){
+                success = false;
+              }
+              p->d_tempCache.push_back( sum );
+            }
+          }else{
+            //must show that constraint is met
+            Node sum = NodeManager::currentNM()->mkNode( k, children );
+            Node eq = sum.eqNode( v );
+            if( !entailmentTest( p, eq ) ){
+              success = false;
+            }
+            p->d_tempCache.push_back( sum );
+          }
+        }
+      }
+
+      if( !success ){
+        break;
+      }
+    }
+    if( success ){
+      //check what is left to assign
+      d_unassigned.clear();
+      d_unassigned_tn.clear();
+      std::vector< int > unassigned[2];
+      std::vector< TypeNode > unassigned_tn[2];
+      for( int i=0; i<getNumVars(); i++ ){
+        if( d_match[i].isNull() ){
+          int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
+          unassigned[rindex].push_back( i );
+          unassigned_tn[rindex].push_back( getVar( i ).getType() );
+          assigned.push_back( i );
+        }
+      }
+      d_unassigned_nvar = unassigned[0].size();
+      for( unsigned i=0; i<2; i++ ){
+        d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );
+        d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );
+      }
+      d_una_eqc_count.clear();
+      d_una_index = 0;
+    }
+  }
+
+  if( !d_unassigned.empty() && ( success || doContinue ) ){
+    Trace("qcf-check") << "Assign to unassigned..." << std::endl;
+    do {
+      if( doFail ){
+        Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
+      }
+      bool invalidMatch = false;
+      while( ( d_una_index>=0 && (int)d_una_index<(int)d_unassigned.size() ) || invalidMatch || doFail ){
+        invalidMatch = false;
+        if( !doFail && d_una_index==(int)d_una_eqc_count.size() ){
+          //check if it has now been assigned
+          if( d_una_index<d_unassigned_nvar ){
+            if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
+              d_una_eqc_count.push_back( -1 );
+            }else{
+              d_var_mg[ d_unassigned[d_una_index] ]->reset( p, true, this );
+              d_una_eqc_count.push_back( 0 );
+            }
+          }else{
+            d_una_eqc_count.push_back( 0 );
+          }
+        }else{
+          bool failed = false;
+          if( !doFail ){
+            if( d_una_index<d_unassigned_nvar ){
+              if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
+                Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;
+                d_una_index++;
+              }else if( d_var_mg[d_unassigned[d_una_index]]->getNextMatch( p, this ) ){
+                Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl;
+                d_una_index++;
+              }else{
+                failed = true;
+                Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;
+              }
+            }else{
+              Assert( doFail || d_una_index==(int)d_una_eqc_count.size()-1 );
+              if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){
+                int currIndex = d_una_eqc_count[d_una_index];
+                d_una_eqc_count[d_una_index]++;
+                Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;
+                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){
+                  d_match_term[d_unassigned[d_una_index]] = TNode::null();
+                  Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
+                  d_una_index++;
+                }else{
+                  Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl;
+                  invalidMatch = true;
+                }
+              }else{
+                failed = true;
+                Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl;
+              }
+            }
+          }
+          if( doFail || failed ){
+            do{
+              if( !doFail ){
+                d_una_eqc_count.pop_back();
+              }else{
+                doFail = false;
+              }
+              d_una_index--;
+            }while( d_una_index>=0 && d_una_eqc_count[d_una_index]==-1 );
+          }
+        }
+      }
+      success = d_una_index>=0;
+      if( success ){
+        doFail = true;
+        Trace("qcf-check-unassign") << "  Try: " << std::endl;
+        for( unsigned i=0; i<d_unassigned.size(); i++ ){
+          int ui = d_unassigned[i];
+          if( !d_match[ui].isNull() ){
+            Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
+          }
+        }
+      }
+    }while( success && isMatchSpurious( p ) );
+  }
+  if( success ){
+    for( unsigned i=0; i<d_unassigned.size(); i++ ){
+      int ui = d_unassigned[i];
+      if( !d_match[ui].isNull() ){
+        Trace("qcf-check") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
+      }
+    }
+    return true;
+  }else{
+    for( unsigned i=0; i<assigned.size(); i++ ){
+      d_match[ assigned[i] ] = TNode::null();
+    }
+    assigned.clear();
+    return false;
+  }
+}
+
+void QuantInfo::getMatch( std::vector< Node >& terms ){
+  for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
+    //Node cv = qi->getCurrentValue( qi->d_match[i] );
+    int repVar = getCurrentRepVar( i );
+    Node cv;
+    //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
+    if( !d_match_term[repVar].isNull() ){
+      cv = d_match_term[repVar];
+    }else{
+      cv = d_match[repVar];
+    }
+    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_match[i] << std::endl;
+    terms.push_back( cv );
+  }
+}
+
+void QuantInfo::revertMatch( std::vector< int >& assigned ) {
+  for( unsigned i=0; i<assigned.size(); i++ ){
+    d_match[ assigned[i] ] = TNode::null();
+  }
+}
+
+void QuantInfo::debugPrintMatch( const char * c ) {
+  for( int i=0; i<getNumVars(); i++ ){
+    Trace(c) << "  " << d_vars[i] << " -> ";
+    if( !d_match[i].isNull() ){
+      Trace(c) << d_match[i];
+    }else{
+      Trace(c) << "(unassigned) ";
+    }
+    if( !d_curr_var_deq[i].empty() ){
+      Trace(c) << ", DEQ{ ";
+      for( std::map< TNode, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){
+        Trace(c) << it->first << " ";
+      }
+      Trace(c) << "}";
+    }
+    if( !d_match_term[i].isNull() && d_match_term[i]!=d_match[i] ){
+      Trace(c) << ", EXP : " << d_match_term[i];
+    }
+    Trace(c) <<  std::endl;
+  }
+  if( !d_tconstraints.empty() ){
+    Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;
+    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
+      Trace(c) << "   " << it->first << " -> " << it->second << std::endl;
+    }
+  }
+}
+
+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
+  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
+  std::vector< Node > qni_apps;
+  d_qni_size = 0;
+  if( isVar ){
+    Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
+    if( n.getKind()==ITE ){
+      d_type = typ_ite_var;
+      d_type_not = false;
+      d_n = n;
+      d_children.push_back( MatchGen( qi, d_n[0] ) );
+      if( d_children[0].isValid() ){
+        d_type = typ_ite_var;
+        for( unsigned i=1; i<=2; i++ ){
+          Node nn = n.eqNode( n[i] );
+          d_children.push_back( MatchGen( qi, nn ) );
+          d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 );
+          if( !d_children[d_children.size()-1].isValid() ){
+            setInvalid();
+            break;
+          }
+        }
+      }else{
+        d_type = typ_invalid;
+      }
+    }else{
+      d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
+      d_qni_var_num[0] = qi->getVarNum( n );
+      d_qni_size++;
+      d_type_not = false;
+      d_n = n;
+      //Node f = getOperator( n );
+      for( unsigned j=0; j<d_n.getNumChildren(); j++ ){
+        Node nn = d_n[j];
+        Trace("qcf-qregister-debug") << "  " << d_qni_size;
+        if( qi->isVar( nn ) ){
+          int v = qi->d_var_num[nn];
+          Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
+          d_qni_var_num[d_qni_size] = v;
+          //qi->addFuncParent( v, f, j );
+        }else{
+          Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
+          d_qni_gterm[d_qni_size] = nn;
+        }
+        d_qni_size++;
+      }
+    }
+  }else{
+    if( n.hasBoundVar() ){
+      d_type_not = false;
+      d_n = n;
+      if( d_n.getKind()==NOT ){
+        d_n = d_n[0];
+        d_type_not = !d_type_not;
+      }
+
+      if( isHandledBoolConnective( d_n ) ){
+        //non-literals
+        d_type = typ_formula;
+        for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
+          if( d_n.getKind()!=FORALL || i==1 ){
+            d_children.push_back( MatchGen( qi, d_n[i], false ) );
+            if( !d_children[d_children.size()-1].isValid() ){
+              setInvalid();
+              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( isHandledUfTerm( d_n ) ){
+          Assert( qi->isVar( d_n ) );
+          d_type = typ_pred;
+        }else if( d_n.getKind()==BOUND_VARIABLE ){
+          Assert( d_n.getType().isBoolean() );
+          d_type = typ_bool_var;
+        }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
+          for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
+            if( d_n[i].hasBoundVar() ){
+              if( !qi->isVar( d_n[i] ) ){
+                Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;
+              }
+              Assert( qi->isVar( d_n[i] ) );
+              if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){
+                d_qni_var_num[i+1] = qi->d_var_num[d_n[i]];
+              }
+            }else{
+              d_qni_gterm[i] = d_n[i];
+            }
+          }
+          d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;
+          Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
+        }
+      }
+    }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(), mgs );
+        //}
+      //}
+    //}
+  }
+  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 MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) {
+  int v = qi->getVarNum( n );
+  if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){
+    cbvars.push_back( v );
+  }
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    collectBoundVar( qi, n[i], cbvars );
+  }
+}
+
+void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {
+  Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl;
+  bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );
+  std::map< int, std::vector< int > > c_to_vars;
+  std::map< int, std::vector< int > > vars_to_c;
+  std::map< int, int > vb_count;
+  std::map< int, int > vu_count;
+  std::vector< bool > assigned;
+  Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    collectBoundVar( qi, d_children[i].d_n, c_to_vars[i] );
+    assigned.push_back( false );
+    vb_count[i] = 0;
+    vu_count[i] = 0;
+    for( unsigned j=0; j<c_to_vars[i].size(); j++ ){
+      int v = c_to_vars[i][j];
+      vars_to_c[v].push_back( i );
+      if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
+        vu_count[i]++;
+        if( !isCom ){
+          bvars.push_back( v );
+        }
+      }else{
+        vb_count[i]++;
+      }
+    }
+  }
+  if( isCom ){
+    //children that bind the least number of unbound variables go first
+    do {
+      int min_score = -1;
+      int min_score_index = -1;
+      for( unsigned i=0; i<d_children.size(); i++ ){
+        if( !assigned[i] ){
+          int score = vu_count[i];
+          if( min_score==-1 || score<min_score ){
+            min_score = score;
+            min_score_index = i;
+          }
+        }
+      }
+      Trace("qcf-qregister-debug") << "...assign child " << min_score_index << "/" << d_children.size() << std::endl;
+      Assert( min_score_index!=-1 );
+      //add to children order
+      d_children_order.push_back( min_score_index );
+      assigned[min_score_index] = true;
+      //if( vb_count[min_score_index]==0 ){
+      //  d_independent.push_back( min_score_index );
+      //}
+      //determine order internal to children
+      d_children[min_score_index].determineVariableOrder( qi, bvars );
+      Trace("qcf-qregister-debug")  << "...bind variables" << std::endl;
+      //now, make it a bound variable
+      for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
+        int v = c_to_vars[min_score_index][i];
+        if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
+          for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
+            int vc = vars_to_c[v][j];
+            vu_count[vc]--;
+            vb_count[vc]++;
+          }
+          bvars.push_back( v );
+        }
+      }
+      Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
+    }while( d_children_order.size()!=d_children.size() );
+    Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl;
+  }else{
+    for( unsigned i=0; i<d_children.size(); i++ ){
+      d_children_order.push_back( i );
+      d_children[i].determineVariableOrder( qi, bvars );
+    }
+  }
+}
+
+
+void MatchGen::reset_round( QuantConflictFind * p ) {
+  d_wasSet = false;
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    d_children[i].reset_round( p );
+  }
+  for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
+    d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
+  }
+  if( d_type==typ_ground ){
+    int e = p->evaluate( d_n );
+    if( e==1 ){
+      d_ground_eval[0] = p->d_true;
+    }else if( e==-1 ){
+      d_ground_eval[0] = p->d_false;
+    }
+  }else if( d_type==typ_eq ){
+    for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
+      if( !d_n[i].hasBoundVar() ){
+        d_ground_eval[i] = p->evaluateTerm( d_n[i] );
+      }
+    }
+  }
+  d_qni_bound_cons.clear();
+  d_qni_bound_cons_var.clear();
+  d_qni_bound.clear();
+}
+
+void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
+  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() << " " << d_children_order.size() << std::endl;
+  d_qn.clear();
+  d_qni.clear();
+  d_qni_bound.clear();
+  d_child_counter = -1;
+  d_tgt_orig = d_tgt;
+
+  //set up processing matches
+  if( d_type==typ_invalid ){
+    //do nothing
+  }else if( d_type==typ_ground ){
+    if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){
+      d_child_counter = 0;
+    }
+  }else if( d_type==typ_bool_var ){
+    //get current value of the variable
+    TNode n = qi->getCurrentValue( d_n );
+    int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );
+    if( vn==-1 ){
+      //evaluate the value, see if it is compatible
+      int e = p->evaluate( n );
+      if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
+        d_child_counter = 0;
+      }
+    }else{
+      //unassigned, set match to true/false
+      d_qni_bound[0] = vn;
+      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false );
+      d_child_counter = 0;
+    }
+    if( d_child_counter==0 ){
+      d_qn.push_back( NULL );
+    }
+  }else if( d_type==typ_var ){
+    Assert( isHandledUfTerm( d_n ) );
+    Node f = getOperator( p, d_n );
+    Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;
+    TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f );
+    if( qni!=NULL ){
+      d_qn.push_back( qni );
+    }
+    d_matched_basis = false;
+  }else if( d_type==typ_tsym || d_type==typ_tconstraint ){
+    for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){
+      int repVar = qi->getCurrentRepVar( it->second );
+      if( qi->d_match[repVar].isNull() ){
+        Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl;
+        d_qni_bound[it->first] = repVar;
+      }
+    }
+    d_qn.push_back( NULL );
+  }else if( d_type==typ_pred || d_type==typ_eq ){
+    //add initial constraint
+    Node nn[2];
+    int vn[2];
+    if( d_type==typ_pred ){
+      nn[0] = qi->getCurrentValue( d_n );
+      vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) );
+      nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );
+      vn[1] = -1;
+      d_tgt = true;
+    }else{
+      for( unsigned i=0; i<2; i++ ){
+        TNode nc;
+        std::map< int, TNode >::iterator it = d_qni_gterm_rep.find( i );
+        if( it!=d_qni_gterm_rep.end() ){
+          nc = it->second;
+        }else{
+          nc = d_n[i];
+        }
+        nn[i] = qi->getCurrentValue( nc );
+        vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) );
+      }
+    }
+    bool success;
+    if( vn[0]==-1 && vn[1]==-1 ){
+      //Trace("qcf-explain") << "    reset : " << d_n << " check ground values " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl;
+      Debug("qcf-match-debug") << "       reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;
+      //just compare values
+      if( d_tgt ){
+        success = p->areMatchEqual( nn[0], nn[1] );
+      }else{
+        if( p->d_effort==QuantConflictFind::effort_conflict ){
+          success = p->areDisequal( nn[0], nn[1] );
+        }else{
+          success = p->areMatchDisequal( nn[0], nn[1] );
+        }
+      }
+    }else{
+      //otherwise, add a constraint to a variable
+      if( vn[1]!=-1 && vn[0]==-1 ){
+        //swap
+        Node t = nn[1];
+        nn[1] = nn[0];
+        nn[0] = t;
+        vn[0] = vn[1];
+        vn[1] = -1;
+      }
+      Debug("qcf-match-debug") << "       reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;
+      //add some constraint
+      int addc = qi->addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );
+      success = addc!=-1;
+      //if successful and non-redundant, store that we need to cleanup this
+      if( addc==1 ){
+        //Trace("qcf-explain") << "       reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl;
+        for( unsigned i=0; i<2; i++ ){
+          if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){
+            d_qni_bound[vn[i]] = vn[i];
+          }
+        }
+        d_qni_bound_cons[vn[0]] = nn[1];
+        d_qni_bound_cons_var[vn[0]] = vn[1];
+      }
+    }
+    //if successful, we will bind values to variables
+    if( success ){
+      d_qn.push_back( NULL );
+    }
+  }else{
+    if( d_children.empty() ){
+      //add dummy
+      d_qn.push_back( NULL );
+    }else{
+      if( d_tgt && d_n.getKind()==FORALL ){
+        //do nothing
+      }else{
+        //reset the first child to d_tgt
+        d_child_counter = 0;
+        getChild( d_child_counter )->reset( p, d_tgt, qi );
+      }
+    }
+  }
+  d_binding = false;
+  d_wasSet = true;
+  Debug("qcf-match") << "     reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;
+}
+
+bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
+  Debug("qcf-match") << "     Get next match for : " << d_n << ", type = ";
+  debugPrintType( "qcf-match", d_type );
+  Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;
+  if( d_type==typ_invalid || d_type==typ_ground ){
+    if( d_child_counter==0 ){
+      d_child_counter = -1;
+      return true;
+    }else{
+      d_wasSet = false;
+      return false;
+    }
+  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var || d_type==typ_tconstraint || d_type==typ_tsym ){
+    bool success = false;
+    bool terminate = false;
+    do {
+      bool doReset = false;
+      bool doFail = false;
+      if( !d_binding ){
+        if( doMatching( p, qi ) ){
+          Debug("qcf-match-debug") << "     - Matching succeeded" << std::endl;
+          d_binding = true;
+          d_binding_it = d_qni_bound.begin();
+          doReset = true;
+          //for tconstraint, add constraint
+          if( d_type==typ_tconstraint ){
+            std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n );
+            if( it==qi->d_tconstraints.end() ){
+              qi->d_tconstraints[d_n] = d_tgt;
+              //store that we added this constraint
+              d_qni_bound_cons[0] = d_n;
+            }else if( d_tgt!=it->second ){
+              success = false;
+              terminate = true;
+            }
+          }
+        }else{
+          Debug("qcf-match-debug") << "     - Matching failed" << std::endl;
+          success = false;
+          terminate = true;
+        }
+      }else{
+        doFail = true;
+      }
+      if( d_binding ){
+        //also need to create match for each variable we bound
+        success = true;
+        Debug("qcf-match-debug") << "     Produce matches for bound variables by " << d_n << ", type = ";
+        debugPrintType( "qcf-match-debug", d_type );
+        Debug("qcf-match-debug") << "..." << std::endl;
+
+        while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){
+          std::map< int, MatchGen * >::iterator itm;
+          if( !doFail ){
+            Debug("qcf-match-debug") << "       check variable " << d_binding_it->second << std::endl;
+            itm = qi->d_var_mg.find( d_binding_it->second );
+          }
+          if( doFail || ( d_binding_it->first!=0 && itm!=qi->d_var_mg.end() ) ){
+            Debug("qcf-match-debug") << "       we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;
+            if( doReset ){
+              itm->second->reset( p, true, qi );
+            }
+            if( doFail || !itm->second->getNextMatch( p, qi ) ){
+              do {
+                if( d_binding_it==d_qni_bound.begin() ){
+                  Debug("qcf-match-debug") << "       failed." << std::endl;
+                  success = false;
+                }else{
+                  --d_binding_it;
+                  Debug("qcf-match-debug") << "       decrement..." << std::endl;
+                }
+              }while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) );
+              doReset = false;
+              doFail = false;
+            }else{
+              Debug("qcf-match-debug") << "       increment..." << std::endl;
+              ++d_binding_it;
+              doReset = true;
+            }
+          }else{
+            Debug("qcf-match-debug") << "       skip..." << d_binding_it->second << std::endl;
+            ++d_binding_it;
+            doReset = true;
+          }
+        }
+        if( !success ){
+          d_binding = false;
+        }else{
+          terminate = true;
+          if( d_binding_it==d_qni_bound.begin() ){
+            d_binding = false;
+          }
+        }
+      }
+    }while( !terminate );
+    //if not successful, clean up the variables you bound
+    if( !success ){
+      if( d_type==typ_eq || d_type==typ_pred ){
+        //clean up the constraints you added
+        for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){
+          if( !it->second.isNull() ){
+            Debug("qcf-match") << "       Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;
+            std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );
+            int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;
+            //Trace("qcf-explain") << "       cleanup: " << d_n << " remove constraint " << it->first << " -> " << it->second << " (vn=" << vn << ")" << ", d_tgt = " << d_tgt << std::endl;
+            qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );
+          }
+        }
+        d_qni_bound_cons.clear();
+        d_qni_bound_cons_var.clear();
+        d_qni_bound.clear();
+      }else{
+        //clean up the matches you set
+        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<qi->getNumVars() );
+          qi->d_match[ it->second ] = TNode::null();
+          qi->d_match_term[ it->second ] = TNode::null();
+        }
+        d_qni_bound.clear();
+      }
+      if( d_type==typ_tconstraint ){
+        //remove constraint if applicable
+        if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){
+          qi->d_tconstraints.erase( d_n );
+          d_qni_bound_cons.clear();
+        }
+      }
+      /*
+      if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){
+        d_matched_basis = true;
+        Node f = getOperator( d_n );
+        TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f );
+        if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){
+          success = true;
+          d_qni_bound[0] = d_qni_var_num[0];
+        }
+      }
+      */
+    }
+    Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
+    d_wasSet = success;
+    return success;
+  }else if( d_type==typ_formula || d_type==typ_ite_var ){
+    bool success = false;
+    if( d_child_counter<0 ){
+      if( d_child_counter<-1 ){
+        success = true;
+        d_child_counter = -1;
+      }
+    }else{
+      while( !success && d_child_counter>=0 ){
+        //transition system based on d_child_counter
+        if( 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, qi ) ){
+              if( d_child_counter<(int)(getNumChildren()-1) ){
+                d_child_counter++;
+                Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << std::endl;
+                getChild( d_child_counter )->reset( p, d_tgt, qi );
+              }else{
+                success = true;
+              }
+            }else{
+              //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){
+              //  d_child_counter--;
+              //}else{
+              d_child_counter--;
+              //}
+            }
+          }else{
+            //one child must match
+            if( !getChild( d_child_counter )->getNextMatch( p, qi ) ){
+              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, qi );
+              }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, qi ) ){
+              d_child_counter++;
+              getChild( 1 )->reset( p, d_child_counter==1, qi );
+            }else{
+              if( d_child_counter==0 ){
+                d_child_counter = 2;
+                getChild( 0 )->reset( p, !d_tgt, qi );
+              }else{
+                d_child_counter = -1;
+              }
+            }
+          }
+          if( d_child_counter>=0 && d_child_counter%2==1 ){
+            if( getChild( 1 )->getNextMatch( p, qi ) ){
+              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, qi ) ){
+              d_child_counter++;
+              getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );
+            }else{
+              if( d_child_counter==4 || ( d_type==typ_ite_var && d_child_counter==2 ) ){
+                d_child_counter = -1;
+              }else{
+                d_child_counter +=2;
+                getChild( d_child_counter==2 ? 0 : 1 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );
+              }
+            }
+          }
+          if( d_child_counter>=0 && d_child_counter%2==1 ){
+            int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2);
+            if( getChild( index2 )->getNextMatch( p, qi ) ){
+              success = true;
+            }else{
+              d_child_counter--;
+            }
+          }
+        }else if( d_n.getKind()==FORALL ){
+          if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
+            success = true;
+          }else{
+            d_child_counter = -1;
+          }
+        }
+      }
+        d_wasSet = success;
+      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 MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ) {
+  if( d_type==typ_eq ){
+    Node n[2];
+    for( unsigned i=0; i<2; i++ ){
+      Trace("qcf-explain") << "Explain term " << d_n[i] << "..." << std::endl;
+      n[i] = getExplanationTerm( p, qi, d_n[i], exp );
+    }
+    Node eq = n[0].eqNode( n[1] );
+    if( !d_tgt_orig ){
+      eq = eq.negate();
+    }
+    exp.push_back( eq );
+    Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << eq << ", set = " << d_wasSet << std::endl;
+    return true;
+  }else if( d_type==typ_pred ){
+    Trace("qcf-explain") << "Explain term " << d_n << "..." << std::endl;
+    Node n = getExplanationTerm( p, qi, d_n, exp );
+    if( !d_tgt_orig ){
+      n = n.negate();
+    }
+    exp.push_back( n );
+    Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << n << ", set = " << d_wasSet << std::endl;
+    return true;
+  }else if( d_type==typ_formula ){
+    Trace("qcf-explain") << "Explanation get for " << d_n << ", counter = " << d_child_counter << ", tgt = " << d_tgt_orig << ", set = " << d_wasSet << std::endl;
+    if( d_n.getKind()==OR || d_n.getKind()==AND ){
+      if( (d_n.getKind()==AND)==d_tgt ){
+        for( unsigned i=0; i<getNumChildren(); i++ ){
+          if( !getChild( i )->getExplanation( p, qi, exp ) ){
+            return false;
+          }
+        }
+      }else{
+        return getChild( d_child_counter )->getExplanation( p, qi, exp );
+      }
+    }else if( d_n.getKind()==IFF ){
+      for( unsigned i=0; i<2; i++ ){
+        if( !getChild( i )->getExplanation( p, qi, exp ) ){
+          return false;
+        }
+      }
+    }else if( d_n.getKind()==ITE ){
+      for( unsigned i=0; i<3; i++ ){
+        bool isActive = ( ( i==0 && d_child_counter!=5 ) ||
+                          ( i==1 && d_child_counter!=( d_tgt ? 3 : 1 ) ) ||
+                          ( i==2 && d_child_counter!=( d_tgt ? 1 : 3 ) ) );
+        if( isActive ){
+          if( !getChild( i )->getExplanation( p, qi, exp ) ){
+            return false;
+          }
+        }
+      }
+    }else{
+      return false;
+    }
+    return true;
+  }else{
+    return false;
+  }
+}
+
+Node MatchGen::getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ) {
+  Node v = qi->getCurrentExpValue( t );
+  if( isHandledUfTerm( t ) ){
+    for( unsigned i=0; i<t.getNumChildren(); i++ ){
+      Node vi = getExplanationTerm( p, qi, t[i], exp );
+      if( vi!=v[i] ){
+        Node eq = vi.eqNode( v[i] );
+        if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
+          Trace("qcf-explain") << "  add : " << eq << "." << std::endl;
+          exp.push_back( eq );
+        }
+      }
+    }
+  }
+  return v;
+}
+
+bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
+  if( !d_qn.empty() ){
+    if( d_qn[0]==NULL ){
+      d_qn.clear();
+      return true;
+    }else{
+      Assert( d_type==typ_var );
+      Assert( d_qni_size>0 );
+      bool invalidMatch;
+      do {
+        invalidMatch = false;
+        Debug("qcf-match-debug") << "       Do matching " << d_n << " " << d_qn.size() << " " << d_qni.size() << std::endl;
+        if( d_qn.size()==d_qni.size()+1 ) {
+          int index = (int)d_qni.size();
+          //initialize
+          TNode 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 = qi->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, TNode >::iterator itm = qi->d_match.find( repVar );
+            if( !qi->d_match[repVar].isNull() ){
+              val = qi->d_match[repVar];
+              Debug("qcf-match-debug") << "       Variable is already bound to " << val << std::endl;
+            }else{
+              //binding a variable
+              d_qni_bound[index] = repVar;
+              std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.begin();
+              if( it != d_qn[index]->d_data.end() ) {
+                d_qni.push_back( it );
+                //set the match
+                if( it->first.getType().isSubtypeOf( qi->d_var_types[repVar] ) && qi->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< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.find( val );
+            if( it!=d_qn[index]->d_data.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_data.end() ){
+              success = true;
+              if( qi->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{
+              qi->d_match[ itb->second ] = TNode::null();
+              qi->d_match_term[ itb->second ] = TNode::null();
+              Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;
+            }
+          }else{
+            //TODO : if it equal to something else, also try that
+          }
+          //if not incrementing, move to next
+          if( !success ){
+            d_qn.pop_back();
+            d_qni.pop_back();
+          }
+        }
+      }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );
+      if( d_qni.size()==d_qni_size ){
+        //Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
+        //Debug("qcf-match-debug") << "       We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;
+        Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
+        TNode t = d_qni[d_qni.size()-1]->second.d_data.begin()->first;
+        Debug("qcf-match-debug") << "       " << d_n << " matched " << t << std::endl;
+        qi->d_match_term[d_qni_var_num[0]] = t;
+        //set the match terms
+        for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
+          Debug("qcf-match-debug") << "       position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;
+          //if( it->second<(int)qi->d_q[0].getNumChildren() ){   //if it is an actual variable, we are interested in knowing the actual term
+          if( it->first>0 ){
+            Assert( !qi->d_match[ it->second ].isNull() );
+            Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );
+            qi->d_match_term[it->second] = t[it->first-1];
+          }
+          //}
+        }
+      }
+    }
+  }
+  return !d_qn.empty();
+}
+
+void 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_eq: Trace(c) << "eq";break;
+    case typ_pred: Trace(c) << "pred";break;
+    case typ_formula: Trace(c) << "formula";break;
+    case typ_var: Trace(c) << "var";break;
+    case typ_ite_var: Trace(c) << "ite_var";break;
+    case typ_bool_var: Trace(c) << "bool_var";break;
+    }
+  }else{
+    switch( typ ){
+    case typ_invalid: Debug(c) << "invalid";break;
+    case typ_ground: Debug(c) << "ground";break;
+    case typ_eq: Debug(c) << "eq";break;
+    case typ_pred: Debug(c) << "pred";break;
+    case typ_formula: Debug(c) << "formula";break;
+    case typ_var: Debug(c) << "var";break;
+    case typ_ite_var: Debug(c) << "ite_var";break;
+    case typ_bool_var: Debug(c) << "bool_var";break;
+    }
+  }
+}
+
+void MatchGen::setInvalid() {
+  d_type = typ_invalid;
+  d_children.clear();
+}
+
+bool MatchGen::isHandledBoolConnective( TNode n ) {
+  return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT );
+}
+
+bool MatchGen::isHandledUfTerm( TNode n ) {
+  //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
+  //       n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
+  return inst::Trigger::isAtomicTriggerKind( n.getKind() );
+}
+
+Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {
+  if( isHandledUfTerm( n ) ){
+    return p->getTermDatabase()->getOperator( n );
+  }else{
+    return Node::null();
+  }
+}
+
+bool MatchGen::isHandled( TNode n ) {
+  if( n.getKind()!=BOUND_VARIABLE && n.hasBoundVar() ){
+    if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){
+      return false;
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( !isHandled( n[i] ) ){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+
+QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
+QuantifiersModule( qe ),
+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);
+}
+
+Node QuantConflictFind::mkEqNode( Node a, Node b ) {
+  if( a.getType().isBoolean() ){
+    return a.iffNode( b );
+  }else{
+    return a.eqNode( b );
+  }
+}
+
+//-------------------------------------------------- registration
+
+void QuantConflictFind::registerQuantifier( Node q ) {
+  if( d_quantEngine->hasOwnership( q, this ) ){
+    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;
+    //make QcfNode structure
+    Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
+    d_qinfo[q].initialize( q, q[1] );
+
+    //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") << "Done registering quantifier." << std::endl;
+  }
+}
+
+int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
+  int ret = 0;
+  if( n.getKind()==EQUAL ){
+    Node n1 = evaluateTerm( n[0] );
+    Node n2 = evaluateTerm( n[1] );
+    Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;
+    if( areEqual( n1, n2 ) ){
+      ret = 1;
+    }else if( areDisequal( n1, n2 ) ){
+      ret = -1;
+    }
+    //else if( d_effort>QuantConflictFind::effort_conflict ){
+    //  ret = -1;
+    //}
+  }else if( MatchGen::isHandledUfTerm( n ) ){  //predicate
+    Node nn = evaluateTerm( n );
+    Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;
+    if( areEqual( nn, d_true ) ){
+      ret = 1;
+    }else if( areEqual( nn, d_false ) ){
+      ret = -1;
+    }
+    //else if( d_effort>QuantConflictFind::effort_conflict ){
+    //  ret = -1;
+    //}
+  }else if( n.getKind()==NOT ){
+    return -evaluate( n[0] );
+  }else if( n.getKind()==ITE ){
+    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;
+}
+
+short QuantConflictFind::getMaxQcfEffort() {
+  if( options::qcfMode()==QCF_CONFLICT_ONLY ){
+    return effort_conflict;
+  }else if( options::qcfMode()==QCF_PROP_EQ ){
+    return effort_prop_eq;
+  }else if( options::qcfMode()==QCF_MC ){
+    return effort_mc;
+  }else{
+    return 0;
+  }
+}
+
+bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
+  //if( d_effort==QuantConflictFind::effort_mc ){
+  //  return n1==n2 || !areDisequal( n1, n2 );
+  //}else{
+  return n1==n2;
+  //}
+}
+
+bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
+  //if( d_effort==QuantConflictFind::effort_conflict ){
+  //  return areDisequal( n1, n2 );
+  //}else{
+  return n1!=n2;
+  //}
+}
+
+//-------------------------------------------------- handling assertions / eqc
+
+void QuantConflictFind::assertNode( Node q ) {
+  if( d_quantEngine->hasOwnership( q, this ) ){
+    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 );
+    //}
+  }
+}
+
+Node QuantConflictFind::evaluateTerm( Node n ) {
+  if( MatchGen::isHandledUfTerm( n ) ){
+    Node f = MatchGen::getOperator( this, n );
+    Node nn;
+    if( getEqualityEngine()->hasTerm( n ) ){
+      nn = getTermDatabase()->existsTerm( f, n );
+    }else{
+      std::vector< TNode > args;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node c = evaluateTerm( n[i] );
+        args.push_back( c );
+      }
+      nn = getTermDatabase()->d_func_map_trie[f].existsTerm( args );
+    }
+    if( !nn.isNull() ){
+      Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;
+      return getRepresentative( nn );
+    }else{
+      Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;
+      return n;
+    }
+  }else if( n.getKind()==ITE ){
+    int v = evaluate( n[0], false, false );
+    if( v==1 ){
+      return evaluateTerm( n[1] );
+    }else if( v==-1 ){
+      return evaluateTerm( n[2] );
+    }
+  }
+  return getRepresentative( n );
+}
+
+/** new node */
+void QuantConflictFind::newEqClass( Node n ) {
+
+}
+
+/** merge */
+void QuantConflictFind::merge( Node a, Node b ) {
+
+}
+
+/** assert disequal */
+void QuantConflictFind::assertDisequal( Node a, Node b ) {
+
+}
+
+//-------------------------------------------------- check function
+
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {
+  bool performCheck = false;
+  if( options::quantConflictFind() && !d_conflict ){
+    if( level==Theory::EFFORT_LAST_CALL ){
+      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
+    }else if( level==Theory::EFFORT_FULL ){
+      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
+    }else if( level==Theory::EFFORT_STANDARD ){
+      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
+    }
+  }
+  return performCheck;
+}
+
+void QuantConflictFind::reset_round( Theory::Effort level ) {
+  d_needs_computeRelEqr = true;
+}
+
+/** check */
+void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
+  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
+    Trace("qcf-check") << "QCF : check : " << level << std::endl;
+    if( d_conflict ){
+      Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
+      if( level>=Theory::EFFORT_FULL ){
+        Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
+        //Assert( false );
+      }
+    }else{
+      int addedLemmas = 0;
+      ++(d_statistics.d_inst_rounds);
+      double clSet = 0;
+      int prevEt = 0;
+      if( Trace.isOn("qcf-engine") ){
+        prevEt = d_statistics.d_entailment_checks.getData();
+        clSet = double(clock())/double(CLOCKS_PER_SEC);
+        Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;
+      }
+      computeRelevantEqr();
+
+      //determine order for quantified formulas
+      std::vector< Node > qorder;
+      std::map< Node, bool > qassert;
+      //mark which are asserted
+      for( unsigned i=0; i<d_qassert.size(); i++ ){
+        qassert[d_qassert[i]] = true;
+      }
+      //add which ones are specified in the order
+      for( unsigned i=0; i<d_quant_order.size(); i++ ){
+        Node n = d_quant_order[i];
+        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() && qassert.find( n )!=qassert.end() ){
+          qorder.push_back( n );
+        }
+      }
+      d_quant_order.clear();
+      d_quant_order.insert( d_quant_order.begin(), qorder.begin(), qorder.end() );
+      //add remaining
+      for( unsigned i=0; i<d_qassert.size(); i++ ){
+        Node n = d_qassert[i];
+        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() ){
+          qorder.push_back( n );
+        }
+      }
+
+      if( Trace.isOn("qcf-debug") ){
+        Trace("qcf-debug") << std::endl;
+        debugPrint("qcf-debug");
+        Trace("qcf-debug") << std::endl;
+      }
+      short end_e = getMaxQcfEffort();
+      for( short e = effort_conflict; e<=end_e; e++ ){
+        d_effort = e;
+        Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
+        for( unsigned j=0; j<qorder.size(); j++ ){
+          Node q = qorder[j];
+          QuantInfo * qi = &d_qinfo[q];
+
+          Assert( d_qinfo.find( q )!=d_qinfo.end() );
+          if( qi->d_mg->isValid() ){
+            Trace("qcf-check") << "Check quantified formula ";
+            debugPrintQuant("qcf-check", q);
+            Trace("qcf-check") << " : " << q << "..." << std::endl;
+
+            Trace("qcf-check-debug") << "Reset round..." << std::endl;
+            qi->reset_round( this );
+            //try to make a matches making the body false
+            Trace("qcf-check-debug") << "Get next match..." << std::endl;
+            while( qi->d_mg->getNextMatch( this, qi ) ){
+              Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
+              qi->debugPrintMatch("qcf-inst");
+              Trace("qcf-inst") << std::endl;
+              std::vector< int > assigned;
+              if( !qi->isMatchSpurious( this ) ){
+                if( qi->completeMatch( this, assigned ) ){
+                  std::vector< Node > terms;
+                  qi->getMatch( terms );
+                  if( !qi->isTConstraintSpurious( this, terms ) ){
+                    if( Debug.isOn("qcf-check-inst") ){
+                      //if( e==effort_conflict ){
+                      Node inst = d_quantEngine->getInstantiation( q, terms );
+                      Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
+                      Assert( evaluate( inst )!=1 );
+                      Assert( evaluate( inst )==-1 || e>effort_conflict );
+                      //}
+                    }
+                    if( d_quantEngine->addInstantiation( q, terms, false ) ){
+                      Trace("qcf-check") << "   ... Added instantiation" << std::endl;
+                      Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
+                      qi->debugPrintMatch("qcf-inst");
+                      Trace("qcf-inst") << std::endl;
+                      ++addedLemmas;
+                      if( e==effort_conflict ){
+                        d_quant_order.insert( d_quant_order.begin(), q );
+                        d_conflict.set( true );
+                        ++(d_statistics.d_conflict_inst);
+                        break;
+                      }else if( e==effort_prop_eq ){
+                        ++(d_statistics.d_prop_inst);
+                      }
+                    }else{
+                      Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
+                      //Assert( false );
+                    }
+                  }
+                  //clean up assigned
+                  qi->revertMatch( assigned );
+                  d_tempCache.clear();
+                }else{
+                  Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
+                }
+              }else{
+                Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;
+              }
+            }
+            if( d_conflict ){
+              break;
+            }
+          }
+        }
+        if( addedLemmas>0 ){
+          break;
+        }
+      }
+      if( Trace.isOn("qcf-engine") ){
+        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+        Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
+        if( addedLemmas>0 ){
+          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) );
+          Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
+        }
+        Trace("qcf-engine") << std::endl;
+        int currEt = d_statistics.d_entailment_checks.getData();
+        if( currEt!=prevEt ){
+          Trace("qcf-engine") << "  Entailment checks = " << ( currEt - prevEt ) << std::endl;
+        }
+      }
+      Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
+    }
+  }
+}
+
+void QuantConflictFind::computeRelevantEqr() {
+  if( d_needs_computeRelEqr ){
+    d_needs_computeRelEqr = false;
+    Trace("qcf-check") << "Compute relevant equalities..." << std::endl;
+    //d_uf_terms.clear();
+    //d_eqc_uf_terms.clear();
+    d_eqcs.clear();
+    d_model_basis.clear();
+    //d_arg_reps.clear();
+    //double clSet = 0;
+    //if( Trace.isOn("qcf-opt") ){
+    //  clSet = double(clock())/double(CLOCKS_PER_SEC);
+    //}
+
+    //long nTermst = 0;
+    //long nTerms = 0;
+    //long nEqc = 0;
+
+    //which nodes are irrelevant for disequality matches
+    std::map< TNode, bool > irrelevant_dnode;
+    //now, store matches
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
+    while( !eqcs_i.isFinished() ){
+      //nEqc++;
+      Node r = (*eqcs_i);
+      if( getTermDatabase()->hasTermCurrent( r ) ){
+        TypeNode rtn = r.getType();
+        if( options::qcfMode()==QCF_MC ){
+          std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );
+          if( itt==d_eqcs.end() ){
+            Node mb = getTermDatabase()->getModelBasisTerm( rtn );
+            if( !getEqualityEngine()->hasTerm( mb ) ){
+              Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;
+              Assert( false );
+            }
+            Node mbr = getRepresentative( mb );
+            if( mbr!=r ){
+              d_eqcs[rtn].push_back( mbr );
+            }
+            d_eqcs[rtn].push_back( r );
+            d_model_basis[rtn] = mb;
+          }else{
+            itt->second.push_back( r );
+          }
+        }else{
+          d_eqcs[rtn].push_back( r );
+        }
+      }
+      ++eqcs_i;
+    }
+    /*
+    if( Trace.isOn("qcf-opt") ){
+      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
+      Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;
+      Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;
+      Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;
+    }
+    */
+  }
+}
+
+
+//-------------------------------------------------- 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;
+  }
+}
+
+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) << ")";
+  }
+}
+
+QuantConflictFind::Statistics::Statistics():
+  d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
+  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),
+  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),
+  d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
+{
+  StatisticsRegistry::registerStat(&d_inst_rounds);
+  StatisticsRegistry::registerStat(&d_conflict_inst);
+  StatisticsRegistry::registerStat(&d_prop_inst);
+  StatisticsRegistry::registerStat(&d_entailment_checks);
+}
+
+QuantConflictFind::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_inst_rounds);
+  StatisticsRegistry::unregisterStat(&d_conflict_inst);
+  StatisticsRegistry::unregisterStat(&d_prop_inst);
+  StatisticsRegistry::unregisterStat(&d_entailment_checks);
+}
+
+TNode QuantConflictFind::getZero( Kind k ) {
+  std::map< Kind, Node >::iterator it = d_zero.find( k );
+  if( it==d_zero.end() ){
+    Node nn;
+    if( k==PLUS ){
+      nn = NodeManager::currentNM()->mkConst( Rational(0) );
+    }
+    d_zero[k] = nn;
+    return nn;
+  }else{
+    return it->second;
+  }
+}
+
+
+}
-- 
cgit v1.2.3