From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 20 Feb 2014 16:37:32 +0000 (-0600)
Subject: Fix ite and iff handling in QCF.  Add option for heuristic instantiation in QCF ... 
X-Git-Tag: cvc5-1.0.0~7084
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f37804c3da98f4eb1888991fd8b7157437aeeb44;p=cvc5.git

Fix ite and iff handling in QCF.  Add option for heuristic instantiation in QCF (not working yet).  Improve automatic option setting for quantifiers.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7ada9d350..4ab8cb548 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1185,10 +1185,13 @@ void SmtEngine::setLogicInternal() throw() {
     }
   }
   if ( options::fmfBoundInt() ){
+    //must have finite model finding on
+    options::finiteModelFind.set( true );
     if( options::mbqiMode()!=quantifiers::MBQI_NONE &&
+        options::mbqiMode()!=quantifiers::MBQI_FMC &&
         options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){
-      //if bounded integers are set, must use full model check for MBQI
-      options::mbqiMode.set( quantifiers::MBQI_FMC );
+      //if bounded integers are set, use no MBQI by default
+      options::mbqiMode.set( quantifiers::MBQI_NONE );
     }
   }
   if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
@@ -1198,6 +1201,9 @@ void SmtEngine::setLogicInternal() throw() {
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
+  if( options::qcfMode.wasSetByUser() ){
+    options::quantConflictFind.set( true );
+  }
 
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
@@ -1572,13 +1578,13 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 			argTypes.push_back(NodeManager::currentNM()->stringType());
 			argTypes.push_back(NodeManager::currentNM()->integerType());
 			argTypes.push_back(NodeManager::currentNM()->integerType());
-			d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", 
+			d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
 								NodeManager::currentNM()->mkFunctionType(
 									argTypes, NodeManager::currentNM()->stringType()),
 								"uf substr",
 								NodeManager::SKOLEM_EXACT_NAME);
 		}
-		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, 
+		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
 							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] );
 		Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
 		Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], zero);
@@ -1595,13 +1601,13 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 			argTypes.push_back(NodeManager::currentNM()->stringType());
 			argTypes.push_back(NodeManager::currentNM()->integerType());
 			argTypes.push_back(NodeManager::currentNM()->integerType());
-			d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", 
+			d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
 								NodeManager::currentNM()->mkFunctionType(
 									argTypes, NodeManager::currentNM()->stringType()),
 								"uf substr",
 								NodeManager::SKOLEM_EXACT_NAME);
 		}
-		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
+		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
 							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
 							NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
 		Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 63cb22f70..dee8192c1 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -129,7 +129,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
   if( f.getNumChildren()==3 && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){
     return STATUS_UNKNOWN;
   }else{
-    int peffort = f.getNumChildren()==3 ? 2 : 1;
+    int peffort = ( f.getNumChildren()==3 && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ) ? 2 : 1;
     //int peffort = 1;
     if( e<peffort ){
       return STATUS_UNFINISHED;
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 38c9211a3..b37e48ec3 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -88,6 +88,8 @@ typedef enum {
   QCF_CONFLICT_ONLY,
   /** use qcf for conflicts and propagations */
   QCF_PROP_EQ,
+  /** use qcf for conflicts, propagations and heuristic instantiations */
+  QCF_PARTIAL,
   /** use qcf for model checking */
   QCF_MC,
 } QcfMode;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 8962104e1..2041a91b8 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -117,7 +117,7 @@ option fmfBoundInt --fmf-bound-int bool :default false :read-write
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
  policy for instantiating axioms
 
-option quantConflictFind --quant-cf bool :default false
+option quantConflictFind --quant-cf bool :read-write :default false
  enable conflict find mechanism for quantifiers
 option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_CONFLICT_ONLY :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h"
  what effort to apply conflict find mechanism
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index eb2c05858..06f5d7600 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -128,6 +128,9 @@ conflict \n\
 prop-eq \n\
 + Apply QCF to propagate equalities as well. \n\
 \n\
+partial \n\
++ Apply QCF to instantiate heuristically as well. \n\
+\n\
 mc \n\
 + Apply QCF in a complete way, so that a model is ensured when it fails. \n\
 \n\
@@ -258,6 +261,8 @@ inline QcfMode stringToQcfMode(std::string option, std::string optarg, SmtEngine
     return QCF_CONFLICT_ONLY;
   } else if(optarg == "prop-eq") {
     return QCF_PROP_EQ;
+  } else if(optarg == "partial") {
+    return QCF_PARTIAL;
   } else if(optarg == "mc" ) {
     return QCF_MC;
   } else if(optarg ==  "help") {
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 312003519..1a47b3a02 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -91,8 +91,9 @@ void QuantInfo::initialize( Node q, Node qn ) {
   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] = new MatchGen( this, d_vars[j], true );
-        if( !d_var_mg[j]->isValid() ){
+        bool beneathQuant = d_nbeneathQuant.find( d_vars[j] )==d_nbeneathQuant.end();
+        d_var_mg[j] = new MatchGen( this, d_vars[j], true, beneathQuant );
+        if( !d_var_mg[j]->isValid() && options::qcfMode()<QCF_PARTIAL ){
           d_mg->setInvalid();
           break;
         }else{
@@ -108,43 +109,44 @@ void QuantInfo::initialize( Node q, Node qn ) {
     }
 
     //must also contain all variables?
-    /*
-      if( d_mg->isValid() ){
-        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-          if( d_has_var.find( q[0][i] )==d_has_var.end() ){
-            d_mg->setInvalid();
-            break;
-          }
+    if( d_isPartial ){
+      for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+        if( d_has_var.find( q[0][i] )==d_has_var.end() ){
+          d_isPartial = false;
+          d_mg->setInvalid();
+          break;
         }
       }
-    */
+    }
   }
-  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
+  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? ( isPartial() ? "PARTIAL " : "VALID " ) : "INVALID" ) << " : " << q << std::endl;
 }
 
-void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
+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 );
+    registerNode( n[1], hasPol, pol, true );
   }else{
     if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){
       if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
         //literals
         if( n.getKind()==EQUAL ){
           for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            flatten( n[i] );
+            flatten( n[i], beneathQuant );
           }
         }else if( MatchGen::isHandledUfTerm( n ) ){
-          flatten( n );
-        }else if( n.getKind()==ITE && !n[1].getType().isBoolean() ){
-          for( unsigned i=1; i<=2; i++ ){
-            flatten( n[i] );
+          flatten( n, beneathQuant );
+        }else if( n.getKind()==ITE ){
+          if( !n[1].getType().isBoolean() ){
+            for( unsigned i=1; i<=2; i++ ){
+              flatten( n[i], beneathQuant );
+            }
           }
         }
       }
     }
-    if( n.getKind()==BOUND_VARIABLE ){
-      d_has_var[n] = true;
+    if( isVar( n ) && !beneathQuant ){
+      d_nbeneathQuant[n] = true;
     }
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       bool newHasPol;
@@ -153,12 +155,12 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
       //QcfNode * qcfc = new QcfNode( d_c );
       //qcfc->d_parent = qcf;
       //qcf->d_child[i] = qcfc;
-      registerNode( n[i], newHasPol, newPol );
+      registerNode( n[i], newHasPol, newPol, beneathQuant );
     }
   }
 }
 
-void QuantInfo::flatten( Node n ) {
+void QuantInfo::flatten( Node n, bool beneathQuant ) {
   Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
   if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
     if( d_var_num.find( n )==d_var_num.end() ){
@@ -171,9 +173,12 @@ void QuantInfo::flatten( Node n ) {
         registerNode( n, false, false );
       }else{
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          flatten( n[i] );
+          flatten( n[i], beneathQuant );
         }
       }
+      if( !beneathQuant ){
+        d_nbeneathQuant[n] = true;
+      }
     }else{
       Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
     }
@@ -582,15 +587,14 @@ void QuantInfo::debugPrintMatch( const char * c ) {
   }
 }
 
-
 //void QuantInfo::addFuncParent( int v, Node f, int arg ) {
 //  if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){
 //    d_f_parent[v][f].push_back( arg );
 //  }
 //}
 
-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
-  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
+  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << ", beneathQuant = " << beneathQuant << std::endl;
   std::vector< Node > qni_apps;
   d_qni_size = 0;
   if( isVar ){
@@ -610,6 +614,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
           Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
           d_qni_var_num[d_qni_size] = v;
           //qi->addFuncParent( v, f, j );
+          if( nn.getKind()==BOUND_VARIABLE && !beneathQuant ){
+            qi->d_has_var[nn] = true;
+          }
         }else{
           Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
           d_qni_gterm[d_qni_size] = nn;
@@ -627,7 +634,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
           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() ){
+          if( !d_children[d_children.size()-1].isValid() && options::qcfMode()<QCF_PARTIAL ){
             setInvalid();
             break;
           }
@@ -651,10 +658,11 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
       if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE || d_n.getKind()==FORALL ){
         //non-literals
         d_type = typ_formula;
+        bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL;
         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
           if( d_n.getKind()!=FORALL || i==1 ){
-            d_children.push_back( MatchGen( qi, d_n[i] ) );
-            if( !d_children[d_children.size()-1].isValid() ){
+            d_children.push_back( MatchGen( qi, d_n[i], false, nBeneathQuant ) );
+            if( !d_children[d_children.size()-1].isValid() && options::qcfMode()<QCF_PARTIAL ){
               setInvalid();
               break;
             }
@@ -688,6 +696,8 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
             if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){
               if( !qi->isVar( d_n[i] ) ){
                 Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;
+              }else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){
+                qi->d_has_var[d_n[i]] = true;
               }
               Assert( qi->isVar( d_n[i] ) );
             }else{
@@ -726,6 +736,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
   debugPrintType( "qcf-qregister-debug", d_type, true );
   Trace("qcf-qregister-debug") << std::endl;
   //Assert( d_children.size()==d_children_order.size() );
+
+  if( !isValid() && options::qcfMode()>=QCF_PARTIAL ){
+    qi->d_isPartial = true;
+  }
 }
 
 void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) {
@@ -849,7 +863,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
 
   //set up processing matches
   if( d_type==typ_invalid ){
-    if( p->d_effort>QuantConflictFind::effort_conflict ){
+    if( p->d_effort==QuantConflictFind::effort_partial ){
       d_child_counter = 0;
     }
   }else if( d_type==typ_ground ){
@@ -936,7 +950,10 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       d_qn.push_back( NULL );
     }else{
       if( d_tgt && d_n.getKind()==FORALL ){
-        //TODO
+        //return success once
+        if( p->d_effort==QuantConflictFind::effort_partial ){
+          d_child_counter = -2;
+        }
       }else{
         //reset the first child to d_tgt
         d_child_counter = 0;
@@ -983,7 +1000,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
         //also need to create match for each variable we bound
         success = true;
         Debug("qcf-match-debug") << "     Produce matches for bound variables by " << d_n << ", type = ";
-        debugPrintType( "qcf-match", d_type );
+        debugPrintType( "qcf-match-debug", d_type );
         Debug("qcf-match-debug") << "..." << std::endl;
 
         while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){
@@ -1070,8 +1087,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
     return success;
   }else if( d_type==typ_formula || d_type==typ_ite_var ){
-    if( d_child_counter!=-1 ){
-      bool success = false;
+    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_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){
@@ -1121,7 +1143,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
               }
             }
           }
-          if( d_child_counter%2==1 ){
+          if( d_child_counter>=0 && d_child_counter%2==1 ){
             if( getChild( 1 )->getNextMatch( p, qi ) ){
               success = true;
             }else{
@@ -1135,15 +1157,15 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * 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 ){
+              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==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );
+                getChild( d_child_counter==2 ? 0 : 1 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );
               }
             }
           }
-          if( d_child_counter%2==1 ){
+          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;
@@ -1153,7 +1175,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
           }
         }else if( d_n.getKind()==FORALL ){
           if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
-            //TODO
             success = true;
           }else{
             d_child_counter = -1;
@@ -1706,86 +1727,100 @@ void QuantConflictFind::check( Theory::Effort level ) {
         debugPrint("qcf-debug");
         Trace("qcf-debug") << std::endl;
       }
-      short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : options::qcfMode()==QCF_PROP_EQ ? effort_prop_eq : effort_mc;
+      short end_e;
+      if( options::qcfMode()==QCF_CONFLICT_ONLY ){
+        end_e = effort_conflict;
+      }else if( options::qcfMode()==QCF_PROP_EQ ){
+        end_e = effort_prop_eq;
+      }else if( options::qcfMode()==QCF_PARTIAL ){
+        end_e = effort_partial;
+      }else{
+        end_e = effort_mc;
+      }
       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];
-          Trace("qcf-check") << "Check quantified formula ";
-          debugPrintQuant("qcf-check", q);
-          Trace("qcf-check") << " : " << q << "..." << std::endl;
 
           Assert( d_qinfo.find( q )!=d_qinfo.end() );
           if( qi->d_mg->isValid() ){
-            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") << "Reset..." << std::endl;
-            qi->d_mg->reset( this, false, qi );
-            Trace("qcf-check-debug") << "Get next match..." << std::endl;
-            while( qi->d_mg->getNextMatch( this, qi ) ){
-
-              Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
-              qi->debugPrintMatch("qcf-check");
-              Trace("qcf-check") << std::endl;
-
-              if( !qi->isMatchSpurious( this ) ){
-                std::vector< int > assigned;
-                if( qi->completeMatch( this, assigned ) ){
-                  std::vector< Node > terms;
-                  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-                    //Node cv = qi->getCurrentValue( qi->d_match[i] );
-                    int repVar = qi->getCurrentRepVar( i );
-                    Node cv;
-                    //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
-                    if( !qi->d_match_term[repVar].isNull() ){
-                      cv = qi->d_match_term[repVar];
+            if( qi->isPartial()==(e==effort_partial) ){
+              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") << "Reset..." << std::endl;
+              qi->d_mg->reset( this, false, qi );
+              Trace("qcf-check-debug") << "Get next match..." << std::endl;
+              while( qi->d_mg->getNextMatch( this, qi ) ){
+
+                Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
+                qi->debugPrintMatch("qcf-check");
+                Trace("qcf-check") << std::endl;
+
+                if( !qi->isMatchSpurious( this ) ){
+                  std::vector< int > assigned;
+                  if( qi->completeMatch( this, assigned ) ){
+                    std::vector< Node > terms;
+                    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+                      //Node cv = qi->getCurrentValue( qi->d_match[i] );
+                      int repVar = qi->getCurrentRepVar( i );
+                      Node cv;
+                      //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
+                      if( !qi->d_match_term[repVar].isNull() ){
+                        cv = qi->d_match_term[repVar];
+                      }else{
+                        cv = qi->d_match[repVar];
+                      }
+                      Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;
+                      terms.push_back( cv );
+                    }
+                    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 ) ){
+                      Trace("qcf-check") << "   ... Added instantiation" << std::endl;
+                      ++addedLemmas;
+                      if( e==effort_conflict ){
+                        d_quant_order.insert( d_quant_order.begin(), q );
+                        d_conflict.set( true );
+                        ++(d_statistics.d_conflict_inst);
+                        break;
+                      }else if( e==effort_prop_eq ){
+                        ++(d_statistics.d_prop_inst);
+                      }else if( e==effort_partial ){
+                        ++(d_statistics.d_partial_inst);
+                      }
                     }else{
-                      cv = qi->d_match[repVar];
+                      Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;
+                      //Assert( false );
                     }
-                    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;
-                    terms.push_back( cv );
-                  }
-                  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 ) ){
-                    Trace("qcf-check") << "   ... Added instantiation" << std::endl;
-                    ++addedLemmas;
-                    if( e==effort_conflict ){
-                      d_quant_order.insert( d_quant_order.begin(), q );
-                      d_conflict.set( true );
-                      ++(d_statistics.d_conflict_inst);
-                      break;
-                    }else if( e==effort_prop_eq ){
-                      ++(d_statistics.d_prop_inst);
+                    //clean up assigned
+                    for( unsigned i=0; i<assigned.size(); i++ ){
+                      qi->d_match[ assigned[i] ] = TNode::null();
                     }
                   }else{
-                    Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;
-                    //Assert( false );
-                  }
-                  //clean up assigned
-                  for( unsigned i=0; i<assigned.size(); i++ ){
-                    qi->d_match[ assigned[i] ] = TNode::null();
+                    Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
                   }
                 }else{
-                  Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
+                  Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;
                 }
-              }else{
-                Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;
+              }
+              if( d_conflict ){
+                break;
               }
             }
           }
-          if( d_conflict ){
-            break;
-          }
         }
         if( addedLemmas>0 ){
           d_quantEngine->flushLemmas();
@@ -1796,7 +1831,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
         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") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : (d_effort==effort_partial ? "partial" : "mc" ) ) );
           Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
         }
         Trace("qcf-engine") << std::endl;
@@ -1863,6 +1898,16 @@ void QuantConflictFind::computeRelevantEqr() {
     }else{
       d_eqcs[rtn].push_back( r );
     }
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
+    while( !eqc_i.isFinished() ){
+      TNode n = (*eqc_i);
+      if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
+        std::cout << "BAD TERM IN DB : " << n << std::endl;
+        exit( 199 );
+      }
+      ++eqc_i;
+    }
+
     //if( r.getType().isInteger() ){
     //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;
     //}
@@ -2030,17 +2075,20 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
 QuantConflictFind::Statistics::Statistics():
   d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
   d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),
-  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )
+  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),
+  d_partial_inst("QuantConflictFind::Instantiations_Partial", 0 )
 {
   StatisticsRegistry::registerStat(&d_inst_rounds);
   StatisticsRegistry::registerStat(&d_conflict_inst);
   StatisticsRegistry::registerStat(&d_prop_inst);
+  StatisticsRegistry::registerStat(&d_partial_inst);
 }
 
 QuantConflictFind::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_inst_rounds);
   StatisticsRegistry::unregisterStat(&d_conflict_inst);
   StatisticsRegistry::unregisterStat(&d_prop_inst);
+  StatisticsRegistry::unregisterStat(&d_partial_inst);
 }
 
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 9b64a312d..944cfa584 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -88,7 +88,7 @@ public:
   void debugPrintType( const char * c, short typ, bool isTrace = false );
 public:
   MatchGen() : d_type( typ_invalid ){}
-  MatchGen( QuantInfo * qi, Node n, bool isVar = false );
+  MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false );
   bool d_tgt;
   Node d_n;
   std::vector< MatchGen > d_children;
@@ -108,14 +108,13 @@ public:
 //info for quantifiers
 class QuantInfo {
 private:
-  void registerNode( Node n, bool hasPol, bool pol );
-  void flatten( Node n );
-  //the variables that this quantified formula has not beneath nested quantifiers
-  std::map< TNode, bool > d_has_var;
+  void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );
+  void flatten( Node n, bool beneathQuant );
 public:
-  QuantInfo() : d_mg( NULL ) {}
+  QuantInfo() : d_mg( NULL ), d_isPartial( false ) {}
   std::vector< TNode > d_vars;
   std::map< TNode, int > d_var_num;
+  std::map< TNode, bool > d_nbeneathQuant;
   std::map< int, std::vector< Node > > d_var_constraint[2];
   int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
   bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }
@@ -142,9 +141,12 @@ public:
   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned );
   void debugPrintMatch( const char * c );
   bool isConstrainedVar( int v );
-//public: //optimization : relevant domain
-  //std::map< int, std::map< Node, std::vector< int > > > d_f_parent;
-  //void addFuncParent( int v, Node f, int arg );
+public:
+  // is partial
+  bool d_isPartial;
+  //the variables that this quantified formula has not beneath nested quantifiers
+  std::map< TNode, bool > d_has_var;
+  bool isPartial() { return d_isPartial; }
 };
 
 class QuantConflictFind : public QuantifiersModule
@@ -212,6 +214,7 @@ public:
   enum {
     effort_conflict,
     effort_prop_eq,
+    effort_partial,
     effort_mc,
   };
   short d_effort;
@@ -250,6 +253,7 @@ public:
     IntStat d_inst_rounds;
     IntStat d_conflict_inst;
     IntStat d_prop_inst;
+    IntStat d_partial_inst;
     Statistics();
     ~Statistics();
   };