Fix ite and iff handling in QCF. Add option for heuristic instantiation in QCF ...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7ada9d35046d6617e79897bd57eb30ddc4aa40d5..4ab8cb548fe5cb13d606064beb658ed326a70ea2 100644 (file)
--- 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 63cb22f70a9883c3e2cb9fb94986fdeb07549014..dee8192c1387708546cafa2ad89ced24815cb8f0 100644 (file)
--- 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 38c9211a3a53d33f6c27f17efaf9d95e765c66c9..b37e48ec3e28a51bd05b3ce49051c4e10bbe872e 100644 (file)
--- 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 8962104e17092e236d7eee45ad757e4e8d5e3409..2041a91b8ed4342c982f2fde5dab91f0bcd1d680 100644 (file)
--- 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 eb2c05858b7158b63adf5ef793399ff3724cdfab..06f5d76009dd136ee77c31cffa8220646cf1b319 100644 (file)
--- 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 3120035195291a38bedc0e7afd9a40e32ce81269..1a47b3a02eebd37b10f0536cbe08a782349477de 100755 (executable)
--- 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() ){\r
     for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){\r
       if( d_vars[j].getKind()!=BOUND_VARIABLE ){\r
-        d_var_mg[j] = new MatchGen( this, d_vars[j], true );\r
-        if( !d_var_mg[j]->isValid() ){\r
+        bool beneathQuant = d_nbeneathQuant.find( d_vars[j] )==d_nbeneathQuant.end();\r
+        d_var_mg[j] = new MatchGen( this, d_vars[j], true, beneathQuant );\r
+        if( !d_var_mg[j]->isValid() && options::qcfMode()<QCF_PARTIAL ){\r
           d_mg->setInvalid();\r
           break;\r
         }else{\r
@@ -108,43 +109,44 @@ void QuantInfo::initialize( Node q, Node qn ) {
     }\r
 \r
     //must also contain all variables?\r
-    /*\r
-      if( d_mg->isValid() ){\r
-        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
-          if( d_has_var.find( q[0][i] )==d_has_var.end() ){\r
-            d_mg->setInvalid();\r
-            break;\r
-          }\r
+    if( d_isPartial ){\r
+      for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+        if( d_has_var.find( q[0][i] )==d_has_var.end() ){\r
+          d_isPartial = false;\r
+          d_mg->setInvalid();\r
+          break;\r
         }\r
       }\r
-    */\r
+    }\r
   }\r
-  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;\r
+  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? ( isPartial() ? "PARTIAL " : "VALID " ) : "INVALID" ) << " : " << q << std::endl;\r
 }\r
 \r
-void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {\r
+void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {\r
   Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;\r
   if( n.getKind()==FORALL ){\r
-    registerNode( n[1], hasPol, pol );\r
+    registerNode( n[1], hasPol, pol, true );\r
   }else{\r
     if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){\r
       if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
         //literals\r
         if( n.getKind()==EQUAL ){\r
           for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
-            flatten( n[i] );\r
+            flatten( n[i], beneathQuant );\r
           }\r
         }else if( MatchGen::isHandledUfTerm( n ) ){\r
-          flatten( n );\r
-        }else if( n.getKind()==ITE && !n[1].getType().isBoolean() ){\r
-          for( unsigned i=1; i<=2; i++ ){\r
-            flatten( n[i] );\r
+          flatten( n, beneathQuant );\r
+        }else if( n.getKind()==ITE ){\r
+          if( !n[1].getType().isBoolean() ){\r
+            for( unsigned i=1; i<=2; i++ ){\r
+              flatten( n[i], beneathQuant );\r
+            }\r
           }\r
         }\r
       }\r
     }\r
-    if( n.getKind()==BOUND_VARIABLE ){\r
-      d_has_var[n] = true;\r
+    if( isVar( n ) && !beneathQuant ){\r
+      d_nbeneathQuant[n] = true;\r
     }\r
     for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
       bool newHasPol;\r
@@ -153,12 +155,12 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
       //QcfNode * qcfc = new QcfNode( d_c );\r
       //qcfc->d_parent = qcf;\r
       //qcf->d_child[i] = qcfc;\r
-      registerNode( n[i], newHasPol, newPol );\r
+      registerNode( n[i], newHasPol, newPol, beneathQuant );\r
     }\r
   }\r
 }\r
 \r
-void QuantInfo::flatten( Node n ) {\r
+void QuantInfo::flatten( Node n, bool beneathQuant ) {\r
   Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;\r
   if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
     if( d_var_num.find( n )==d_var_num.end() ){\r
@@ -171,9 +173,12 @@ void QuantInfo::flatten( Node n ) {
         registerNode( n, false, false );\r
       }else{\r
         for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
-          flatten( n[i] );\r
+          flatten( n[i], beneathQuant );\r
         }\r
       }\r
+      if( !beneathQuant ){\r
+        d_nbeneathQuant[n] = true;\r
+      }\r
     }else{\r
       Trace("qcf-qregister-debug2") << "...already processed" << std::endl;\r
     }\r
@@ -582,15 +587,14 @@ void QuantInfo::debugPrintMatch( const char * c ) {
   }\r
 }\r
 \r
-\r
 //void QuantInfo::addFuncParent( int v, Node f, int arg ) {\r
 //  if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){\r
 //    d_f_parent[v][f].push_back( arg );\r
 //  }\r
 //}\r
 \r
-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){\r
-  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;\r
+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){\r
+  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << ", beneathQuant = " << beneathQuant << std::endl;\r
   std::vector< Node > qni_apps;\r
   d_qni_size = 0;\r
   if( isVar ){\r
@@ -610,6 +614,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
           Trace("qcf-qregister-debug") << " is var #" << v << std::endl;\r
           d_qni_var_num[d_qni_size] = v;\r
           //qi->addFuncParent( v, f, j );\r
+          if( nn.getKind()==BOUND_VARIABLE && !beneathQuant ){\r
+            qi->d_has_var[nn] = true;\r
+          }\r
         }else{\r
           Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;\r
           d_qni_gterm[d_qni_size] = nn;\r
@@ -627,7 +634,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
           Node nn = n.eqNode( n[i] );\r
           d_children.push_back( MatchGen( qi, nn ) );\r
           d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 );\r
-          if( !d_children[d_children.size()-1].isValid() ){\r
+          if( !d_children[d_children.size()-1].isValid() && options::qcfMode()<QCF_PARTIAL ){\r
             setInvalid();\r
             break;\r
           }\r
@@ -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 ){\r
         //non-literals\r
         d_type = typ_formula;\r
+        bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL;\r
         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
           if( d_n.getKind()!=FORALL || i==1 ){\r
-            d_children.push_back( MatchGen( qi, d_n[i] ) );\r
-            if( !d_children[d_children.size()-1].isValid() ){\r
+            d_children.push_back( MatchGen( qi, d_n[i], false, nBeneathQuant ) );\r
+            if( !d_children[d_children.size()-1].isValid() && options::qcfMode()<QCF_PARTIAL ){\r
               setInvalid();\r
               break;\r
             }\r
@@ -688,6 +696,8 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
             if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
               if( !qi->isVar( d_n[i] ) ){\r
                 Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;\r
+              }else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){\r
+                qi->d_has_var[d_n[i]] = true;\r
               }\r
               Assert( qi->isVar( d_n[i] ) );\r
             }else{\r
@@ -726,6 +736,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
   debugPrintType( "qcf-qregister-debug", d_type, true );\r
   Trace("qcf-qregister-debug") << std::endl;\r
   //Assert( d_children.size()==d_children_order.size() );\r
+\r
+  if( !isValid() && options::qcfMode()>=QCF_PARTIAL ){\r
+    qi->d_isPartial = true;\r
+  }\r
 }\r
 \r
 void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) {\r
@@ -849,7 +863,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
 \r
   //set up processing matches\r
   if( d_type==typ_invalid ){\r
-    if( p->d_effort>QuantConflictFind::effort_conflict ){\r
+    if( p->d_effort==QuantConflictFind::effort_partial ){\r
       d_child_counter = 0;\r
     }\r
   }else if( d_type==typ_ground ){\r
@@ -936,7 +950,10 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       d_qn.push_back( NULL );\r
     }else{\r
       if( d_tgt && d_n.getKind()==FORALL ){\r
-        //TODO\r
+        //return success once\r
+        if( p->d_effort==QuantConflictFind::effort_partial ){\r
+          d_child_counter = -2;\r
+        }\r
       }else{\r
         //reset the first child to d_tgt\r
         d_child_counter = 0;\r
@@ -983,7 +1000,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
         //also need to create match for each variable we bound\r
         success = true;\r
         Debug("qcf-match-debug") << "     Produce matches for bound variables by " << d_n << ", type = ";\r
-        debugPrintType( "qcf-match", d_type );\r
+        debugPrintType( "qcf-match-debug", d_type );\r
         Debug("qcf-match-debug") << "..." << std::endl;\r
 \r
         while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){\r
@@ -1070,8 +1087,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;\r
     return success;\r
   }else if( d_type==typ_formula || d_type==typ_ite_var ){\r
-    if( d_child_counter!=-1 ){\r
-      bool success = false;\r
+    bool success = false;\r
+    if( d_child_counter<0 ){\r
+      if( d_child_counter<-1 ){\r
+        success = true;\r
+        d_child_counter = -1;\r
+      }\r
+    }else{\r
       while( !success && d_child_counter>=0 ){\r
         //transition system based on d_child_counter\r
         if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){\r
@@ -1121,7 +1143,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
               }\r
             }\r
           }\r
-          if( d_child_counter%2==1 ){\r
+          if( d_child_counter>=0 && d_child_counter%2==1 ){\r
             if( getChild( 1 )->getNextMatch( p, qi ) ){\r
               success = true;\r
             }else{\r
@@ -1135,15 +1157,15 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
               d_child_counter++;\r
               getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );\r
             }else{\r
-              if( d_child_counter==4 ){\r
+              if( d_child_counter==4 || ( d_type==typ_ite_var && d_child_counter==2 ) ){\r
                 d_child_counter = -1;\r
               }else{\r
                 d_child_counter +=2;\r
-                getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );\r
+                getChild( d_child_counter==2 ? 0 : 1 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );\r
               }\r
             }\r
           }\r
-          if( d_child_counter%2==1 ){\r
+          if( d_child_counter>=0 && d_child_counter%2==1 ){\r
             int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2);\r
             if( getChild( index2 )->getNextMatch( p, qi ) ){\r
               success = true;\r
@@ -1153,7 +1175,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
           }\r
         }else if( d_n.getKind()==FORALL ){\r
           if( getChild( d_child_counter )->getNextMatch( p, qi ) ){\r
-            //TODO\r
             success = true;\r
           }else{\r
             d_child_counter = -1;\r
@@ -1706,86 +1727,100 @@ void QuantConflictFind::check( Theory::Effort level ) {
         debugPrint("qcf-debug");\r
         Trace("qcf-debug") << std::endl;\r
       }\r
-      short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : options::qcfMode()==QCF_PROP_EQ ? effort_prop_eq : effort_mc;\r
+      short end_e;\r
+      if( options::qcfMode()==QCF_CONFLICT_ONLY ){\r
+        end_e = effort_conflict;\r
+      }else if( options::qcfMode()==QCF_PROP_EQ ){\r
+        end_e = effort_prop_eq;\r
+      }else if( options::qcfMode()==QCF_PARTIAL ){\r
+        end_e = effort_partial;\r
+      }else{\r
+        end_e = effort_mc;\r
+      }\r
       for( short e = effort_conflict; e<=end_e; e++ ){\r
         d_effort = e;\r
         Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;\r
         for( unsigned j=0; j<qorder.size(); j++ ){\r
           Node q = qorder[j];\r
           QuantInfo * qi = &d_qinfo[q];\r
-          Trace("qcf-check") << "Check quantified formula ";\r
-          debugPrintQuant("qcf-check", q);\r
-          Trace("qcf-check") << " : " << q << "..." << std::endl;\r
 \r
           Assert( d_qinfo.find( q )!=d_qinfo.end() );\r
           if( qi->d_mg->isValid() ){\r
-            Trace("qcf-check-debug") << "Reset round..." << std::endl;\r
-            qi->reset_round( this );\r
-            //try to make a matches making the body false\r
-            Trace("qcf-check-debug") << "Reset..." << std::endl;\r
-            qi->d_mg->reset( this, false, qi );\r
-            Trace("qcf-check-debug") << "Get next match..." << std::endl;\r
-            while( qi->d_mg->getNextMatch( this, qi ) ){\r
-\r
-              Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;\r
-              qi->debugPrintMatch("qcf-check");\r
-              Trace("qcf-check") << std::endl;\r
-\r
-              if( !qi->isMatchSpurious( this ) ){\r
-                std::vector< int > assigned;\r
-                if( qi->completeMatch( this, assigned ) ){\r
-                  std::vector< Node > terms;\r
-                  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
-                    //Node cv = qi->getCurrentValue( qi->d_match[i] );\r
-                    int repVar = qi->getCurrentRepVar( i );\r
-                    Node cv;\r
-                    //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );\r
-                    if( !qi->d_match_term[repVar].isNull() ){\r
-                      cv = qi->d_match_term[repVar];\r
+            if( qi->isPartial()==(e==effort_partial) ){\r
+              Trace("qcf-check") << "Check quantified formula ";\r
+              debugPrintQuant("qcf-check", q);\r
+              Trace("qcf-check") << " : " << q << "..." << std::endl;\r
+\r
+              Trace("qcf-check-debug") << "Reset round..." << std::endl;\r
+              qi->reset_round( this );\r
+              //try to make a matches making the body false\r
+              Trace("qcf-check-debug") << "Reset..." << std::endl;\r
+              qi->d_mg->reset( this, false, qi );\r
+              Trace("qcf-check-debug") << "Get next match..." << std::endl;\r
+              while( qi->d_mg->getNextMatch( this, qi ) ){\r
+\r
+                Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;\r
+                qi->debugPrintMatch("qcf-check");\r
+                Trace("qcf-check") << std::endl;\r
+\r
+                if( !qi->isMatchSpurious( this ) ){\r
+                  std::vector< int > assigned;\r
+                  if( qi->completeMatch( this, assigned ) ){\r
+                    std::vector< Node > terms;\r
+                    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+                      //Node cv = qi->getCurrentValue( qi->d_match[i] );\r
+                      int repVar = qi->getCurrentRepVar( i );\r
+                      Node cv;\r
+                      //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );\r
+                      if( !qi->d_match_term[repVar].isNull() ){\r
+                        cv = qi->d_match_term[repVar];\r
+                      }else{\r
+                        cv = qi->d_match[repVar];\r
+                      }\r
+                      Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;\r
+                      terms.push_back( cv );\r
+                    }\r
+                    if( Debug.isOn("qcf-check-inst") ){\r
+                      //if( e==effort_conflict ){\r
+                      Node inst = d_quantEngine->getInstantiation( q, terms );\r
+                      Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
+                      Assert( evaluate( inst )!=1 );\r
+                      Assert( evaluate( inst )==-1 || e>effort_conflict );\r
+                      //}\r
+                    }\r
+                    if( d_quantEngine->addInstantiation( q, terms ) ){\r
+                      Trace("qcf-check") << "   ... Added instantiation" << std::endl;\r
+                      ++addedLemmas;\r
+                      if( e==effort_conflict ){\r
+                        d_quant_order.insert( d_quant_order.begin(), q );\r
+                        d_conflict.set( true );\r
+                        ++(d_statistics.d_conflict_inst);\r
+                        break;\r
+                      }else if( e==effort_prop_eq ){\r
+                        ++(d_statistics.d_prop_inst);\r
+                      }else if( e==effort_partial ){\r
+                        ++(d_statistics.d_partial_inst);\r
+                      }\r
                     }else{\r
-                      cv = qi->d_match[repVar];\r
+                      Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;\r
+                      //Assert( false );\r
                     }\r
-                    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;\r
-                    terms.push_back( cv );\r
-                  }\r
-                  if( Debug.isOn("qcf-check-inst") ){\r
-                    //if( e==effort_conflict ){\r
-                    Node inst = d_quantEngine->getInstantiation( q, terms );\r
-                    Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
-                    Assert( evaluate( inst )!=1 );\r
-                    Assert( evaluate( inst )==-1 || e>effort_conflict );\r
-                    //}\r
-                  }\r
-                  if( d_quantEngine->addInstantiation( q, terms ) ){\r
-                    Trace("qcf-check") << "   ... Added instantiation" << std::endl;\r
-                    ++addedLemmas;\r
-                    if( e==effort_conflict ){\r
-                      d_quant_order.insert( d_quant_order.begin(), q );\r
-                      d_conflict.set( true );\r
-                      ++(d_statistics.d_conflict_inst);\r
-                      break;\r
-                    }else if( e==effort_prop_eq ){\r
-                      ++(d_statistics.d_prop_inst);\r
+                    //clean up assigned\r
+                    for( unsigned i=0; i<assigned.size(); i++ ){\r
+                      qi->d_match[ assigned[i] ] = TNode::null();\r
                     }\r
                   }else{\r
-                    Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;\r
-                    //Assert( false );\r
-                  }\r
-                  //clean up assigned\r
-                  for( unsigned i=0; i<assigned.size(); i++ ){\r
-                    qi->d_match[ assigned[i] ] = TNode::null();\r
+                    Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
                   }\r
                 }else{\r
-                  Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
+                  Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
                 }\r
-              }else{\r
-                Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
+              }\r
+              if( d_conflict ){\r
+                break;\r
               }\r
             }\r
           }\r
-          if( d_conflict ){\r
-            break;\r
-          }\r
         }\r
         if( addedLemmas>0 ){\r
           d_quantEngine->flushLemmas();\r
@@ -1796,7 +1831,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
         double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
         Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);\r
         if( addedLemmas>0 ){\r
-          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) );\r
+          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : (d_effort==effort_partial ? "partial" : "mc" ) ) );\r
           Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;\r
         }\r
         Trace("qcf-engine") << std::endl;\r
@@ -1863,6 +1898,16 @@ void QuantConflictFind::computeRelevantEqr() {
     }else{\r
       d_eqcs[rtn].push_back( r );\r
     }\r
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
+    while( !eqc_i.isFinished() ){\r
+      TNode n = (*eqc_i);\r
+      if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+        std::cout << "BAD TERM IN DB : " << n << std::endl;\r
+        exit( 199 );\r
+      }\r
+      ++eqc_i;\r
+    }\r
+\r
     //if( r.getType().isInteger() ){\r
     //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;\r
     //}\r
@@ -2030,17 +2075,20 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
 QuantConflictFind::Statistics::Statistics():\r
   d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),\r
   d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),\r
-  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )\r
+  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),\r
+  d_partial_inst("QuantConflictFind::Instantiations_Partial", 0 )\r
 {\r
   StatisticsRegistry::registerStat(&d_inst_rounds);\r
   StatisticsRegistry::registerStat(&d_conflict_inst);\r
   StatisticsRegistry::registerStat(&d_prop_inst);\r
+  StatisticsRegistry::registerStat(&d_partial_inst);\r
 }\r
 \r
 QuantConflictFind::Statistics::~Statistics(){\r
   StatisticsRegistry::unregisterStat(&d_inst_rounds);\r
   StatisticsRegistry::unregisterStat(&d_conflict_inst);\r
   StatisticsRegistry::unregisterStat(&d_prop_inst);\r
+  StatisticsRegistry::unregisterStat(&d_partial_inst);\r
 }\r
 \r
 }
\ 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 9b64a312dab4a68dd8055244756eaf47181e981e..944cfa5845b1e7a49d98ccfbbafeb6f41151890e 100755 (executable)
--- 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 );\r
 public:\r
   MatchGen() : d_type( typ_invalid ){}\r
-  MatchGen( QuantInfo * qi, Node n, bool isVar = false );\r
+  MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false );\r
   bool d_tgt;\r
   Node d_n;\r
   std::vector< MatchGen > d_children;\r
@@ -108,14 +108,13 @@ public:
 //info for quantifiers\r
 class QuantInfo {\r
 private:\r
-  void registerNode( Node n, bool hasPol, bool pol );\r
-  void flatten( Node n );\r
-  //the variables that this quantified formula has not beneath nested quantifiers\r
-  std::map< TNode, bool > d_has_var;\r
+  void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );\r
+  void flatten( Node n, bool beneathQuant );\r
 public:\r
-  QuantInfo() : d_mg( NULL ) {}\r
+  QuantInfo() : d_mg( NULL ), d_isPartial( false ) {}\r
   std::vector< TNode > d_vars;\r
   std::map< TNode, int > d_var_num;\r
+  std::map< TNode, bool > d_nbeneathQuant;\r
   std::map< int, std::vector< Node > > d_var_constraint[2];\r
   int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }\r
   bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }\r
@@ -142,9 +141,12 @@ public:
   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned );\r
   void debugPrintMatch( const char * c );\r
   bool isConstrainedVar( int v );\r
-//public: //optimization : relevant domain\r
-  //std::map< int, std::map< Node, std::vector< int > > > d_f_parent;\r
-  //void addFuncParent( int v, Node f, int arg );\r
+public:\r
+  // is partial\r
+  bool d_isPartial;\r
+  //the variables that this quantified formula has not beneath nested quantifiers\r
+  std::map< TNode, bool > d_has_var;\r
+  bool isPartial() { return d_isPartial; }\r
 };\r
 \r
 class QuantConflictFind : public QuantifiersModule\r
@@ -212,6 +214,7 @@ public:
   enum {\r
     effort_conflict,\r
     effort_prop_eq,\r
+    effort_partial,\r
     effort_mc,\r
   };\r
   short d_effort;\r
@@ -250,6 +253,7 @@ public:
     IntStat d_inst_rounds;\r
     IntStat d_conflict_inst;\r
     IntStat d_prop_inst;\r
+    IntStat d_partial_inst;\r
     Statistics();\r
     ~Statistics();\r
   };\r