Handle nested (universal) quantifiers in QCF algorithm. Make relevant domain instant...

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 460f71f7ecae29717234202015fc5eab84c7ed6c..96ea46b6b37f2f9804bd9f9aca808475ffbbdc94 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -365,37 +365,50 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
     RelevantDomain * rd = d_quantEngine->getRelevantDomain();
     if( rd ){
       rd->compute();
-      std::vector< unsigned > childIndex;
-      int index = 0;
-      do {
-        while( index>=0 && index<(int)f[0].getNumChildren() ){
-          if( index==(int)childIndex.size() ){
-            childIndex.push_back( -1 );
-          }else{
-            Assert( index==(int)(childIndex.size())-1 );
-            if( (childIndex[index]+1)<rd->getRDomain( f, index )->d_terms.size() ){
-              childIndex[index]++;
-              index++;
+      unsigned final_max_i = 0;
+      for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
+        unsigned ts = rd->getRDomain( f, i )->d_terms.size();
+        if( ts>final_max_i ){
+          final_max_i = ts;
+        }
+      }
+
+      unsigned max_i = 0;
+      while( max_i<=final_max_i ){
+        std::vector< unsigned > childIndex;
+        int index = 0;
+        do {
+          while( index>=0 && index<(int)f[0].getNumChildren() ){
+            if( index==(int)childIndex.size() ){
+              childIndex.push_back( -1 );
             }else{
-              childIndex.pop_back();
-              index--;
+              Assert( index==(int)(childIndex.size())-1 );
+              unsigned nv = childIndex[index]+1;
+              if( nv<rd->getRDomain( f, index )->d_terms.size() && nv<max_i ){
+                childIndex[index]++;
+                index++;
+              }else{
+                childIndex.pop_back();
+                index--;
+              }
             }
           }
-        }
-        success = index>=0;
-        if( success ){
-          index--;
-          //try instantiation
-          std::vector< Node > terms;
-          for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-            terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
-          }
-          if( d_quantEngine->addInstantiation( f, terms, false ) ){
-            ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
-            return STATUS_UNKNOWN;
+          success = index>=0;
+          if( success ){
+            index--;
+            //try instantiation
+            std::vector< Node > terms;
+            for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+              terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+            }
+            if( d_quantEngine->addInstantiation( f, terms, false ) ){
+              ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+              return STATUS_UNKNOWN;
+            }
           }
-        }
-      }while( success );
+        }while( success );
+        max_i++;
+      }
     }
     //*/
 

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index d2920f6caa6bce9186d3552ecf42b8f71423adcb..91c9b665309f19d4a140ca1424e31c591c20375a 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -90,10 +90,12 @@ void QuantInfo::initialize( Node q, Node qn ) {
 \r
   if( d_mg->isValid() ){\r
     for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){\r
-      d_var_mg[j] = new MatchGen( this, d_vars[j], false, true );\r
-      if( !d_var_mg[j]->isValid() ){\r
-        d_mg->setInvalid();\r
-        break;\r
+      if( d_vars[j].getKind()!=BOUND_VARIABLE ){\r
+        d_var_mg[j] = new MatchGen( this, d_vars[j], false, true );\r
+        if( !d_var_mg[j]->isValid() ){\r
+          d_mg->setInvalid();\r
+          break;\r
+        }\r
       }\r
     }\r
     //must also contain all variables?\r
@@ -112,7 +114,7 @@ void QuantInfo::initialize( Node q, Node qn ) {
 \r
 void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {\r
   if( n.getKind()==FORALL ){\r
-    //do nothing\r
+    registerNode( n[1], hasPol, pol );\r
   }else{\r
     if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){\r
       if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
@@ -142,7 +144,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
 }\r
 \r
 void QuantInfo::flatten( Node n ) {\r
-  if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){\r
+  if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
     if( d_var_num.find( n )==d_var_num.end() ){\r
       //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;\r
       d_var_num[n] = d_vars.size();\r
@@ -590,17 +592,23 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isTop, bool isVar ){
     }\r
   }else{\r
     if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
-      //we handle not immediately\r
-      d_n = n.getKind()==NOT ? n[0] : n;\r
-      d_type_not = n.getKind()==NOT;\r
-      if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE ){\r
+      d_type_not = false;\r
+      d_n = n;\r
+      if( d_n.getKind()==NOT ){\r
+        d_n = d_n[0];\r
+        d_type_not = !d_type_not;\r
+      }\r
+\r
+      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
         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
-          d_children.push_back( MatchGen( qi, d_n[i] ) );\r
-          if( d_children[d_children.size()-1].d_type==typ_invalid ){\r
-            setInvalid();\r
-            break;\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].d_type==typ_invalid ){\r
+              setInvalid();\r
+              break;\r
+            }\r
           }\r
           /*\r
           else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){\r
@@ -787,9 +795,13 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       //add dummy\r
       d_qn.push_back( NULL );\r
     }else{\r
-      //reset the first child to d_tgt\r
-      d_child_counter = 0;\r
-      getChild( d_child_counter )->reset( p, d_tgt, qi );\r
+      if( d_tgt && d_n.getKind()==FORALL ){\r
+        //TODO\r
+      }else{\r
+        //reset the first child to d_tgt\r
+        d_child_counter = 0;\r
+        getChild( d_child_counter )->reset( p, d_tgt, qi );\r
+      }\r
     }\r
   }\r
   d_binding = false;\r
@@ -983,6 +995,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
               d_child_counter--;\r
             }\r
           }\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
+          }\r
         }\r
       }\r
       Debug("qcf-match") << "    ...finished construct match for " << d_n << ", success = " << success << std::endl;\r