From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 3 Feb 2014 16:23:28 +0000 (-0600)
Subject: Handle nested (universal) quantifiers in QCF algorithm.  Make relevant domain instant... 
X-Git-Tag: cvc5-1.0.0~7108
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7b50c3f698cd2abdc4f3c2d57e63996419423938;p=cvc5.git

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

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;