Handle nested (universal) quantifiers in QCF algorithm. Make relevant domain instantiation breadth-first.

2 files changed, 76 insertions, 44 deletions

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 460f71f7e..96ea46b6b 100644
--- 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 d2920f6ca..91c9b6653 100755
--- 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 ) {
 

   if( d_mg->isValid() ){

     for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){

-      d_var_mg[j] = new MatchGen( this, d_vars[j], false, true );

-      if( !d_var_mg[j]->isValid() ){

-        d_mg->setInvalid();

-        break;

+      if( d_vars[j].getKind()!=BOUND_VARIABLE ){

+        d_var_mg[j] = new MatchGen( this, d_vars[j], false, true );

+        if( !d_var_mg[j]->isValid() ){

+          d_mg->setInvalid();

+          break;

+        }

       }

     }

     //must also contain all variables?

@@ -112,7 +114,7 @@ void QuantInfo::initialize( Node q, Node qn ) {
 

 void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {

   if( n.getKind()==FORALL ){

-    //do nothing

+    registerNode( n[1], hasPol, pol );

   }else{

     if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){

       if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

@@ -142,7 +144,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
 }

 

 void QuantInfo::flatten( Node n ) {

-  if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){

+  if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

     if( d_var_num.find( n )==d_var_num.end() ){

       //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;

       d_var_num[n] = d_vars.size();

@@ -590,17 +592,23 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isTop, bool isVar ){
     }

   }else{

     if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

-      //we handle not immediately

-      d_n = n.getKind()==NOT ? n[0] : n;

-      d_type_not = n.getKind()==NOT;

-      if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE ){

+      d_type_not = false;

+      d_n = n;

+      if( d_n.getKind()==NOT ){

+        d_n = d_n[0];

+        d_type_not = !d_type_not;

+      }

+

+      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;

         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){

-          d_children.push_back( MatchGen( qi, d_n[i] ) );

-          if( d_children[d_children.size()-1].d_type==typ_invalid ){

-            setInvalid();

-            break;

+          if( d_n.getKind()!=FORALL || i==1 ){

+            d_children.push_back( MatchGen( qi, d_n[i] ) );

+            if( d_children[d_children.size()-1].d_type==typ_invalid ){

+              setInvalid();

+              break;

+            }

           }

           /*

           else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){

@@ -787,9 +795,13 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       //add dummy

       d_qn.push_back( NULL );

     }else{

-      //reset the first child to d_tgt

-      d_child_counter = 0;

-      getChild( d_child_counter )->reset( p, d_tgt, qi );

+      if( d_tgt && d_n.getKind()==FORALL ){

+        //TODO

+      }else{

+        //reset the first child to d_tgt

+        d_child_counter = 0;

+        getChild( d_child_counter )->reset( p, d_tgt, qi );

+      }

     }

   }

   d_binding = false;

@@ -983,6 +995,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
               d_child_counter--;

             }

           }

+        }else if( d_n.getKind()==FORALL ){

+          if( getChild( d_child_counter )->getNextMatch( p, qi ) ){

+            //TODO

+            success = true;

+          }else{

+            d_child_counter = -1;

+          }

         }

       }

       Debug("qcf-match") << "    ...finished construct match for " << d_n << ", success = " << success << std::endl;