More complete guess instantiation strategy, cvc4 now typically times out instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc

6 files changed, 164 insertions, 75 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index a05abfa29..8c00c5af4 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -603,15 +603,19 @@ void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
 
 
 bool FirstOrderModelFmc::isStar(Node n) {
-  return n==getStar(n.getType());
+  //return n==getStar(n.getType());
+  return n.getAttribute(IsStarAttribute());
 }
 
 Node FirstOrderModelFmc::getStar(TypeNode tn) {
-  if( d_type_star.find(tn)==d_type_star.end() ){
+  std::map<TypeNode, Node >::iterator it = d_type_star.find( tn );
+  if( it==d_type_star.end() ){
     Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );
     d_type_star[tn] = st;
+    st.setAttribute(IsStarAttribute(), true );
+    return st;
   }
-  return d_type_star[tn];
+  return it->second;
 }
 
 Node FirstOrderModelFmc::getStarElement(TypeNode tn) {
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index ab3a1aa52..2ac9dadcf 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -19,6 +19,7 @@
 
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
+#include "expr/attribute.h"
 
 namespace CVC4 {
 namespace theory {
@@ -35,6 +36,9 @@ namespace fmcheck {
 }
 class FirstOrderModelQInt;
 
+struct IsStarAttributeId {};
+typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
+
 class FirstOrderModel : public TheoryModel
 {
 protected:
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 25a62a4e8..5e2353e8a 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -359,65 +359,87 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
     return STATUS_UNFINISHED;
   }else{
     //first, try from relevant domain
-    Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
-    bool success;
-    ///*  TODO: add back
     RelevantDomain * rd = d_quantEngine->getRelevantDomain();
-    if( rd ){
-      rd->compute();
-      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;
+    for( unsigned r=0; r<2; r++ ){
+      if( rd || r==1 ){
+        if( r==0 ){
+          Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
+        }else{
+          Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
         }
-      }
+        rd->compute();
+        unsigned final_max_i = 0;
+        std::vector< unsigned > maxs;
+        for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
+          unsigned ts;
+          if( r==0 ){
+            ts = rd->getRDomain( f, i )->d_terms.size();
+          }else{
+            ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
+          }
+          maxs.push_back( ts );
+          Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
+          if( ts>final_max_i ){
+            final_max_i = ts;
+          }
+        }
+        Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
 
-      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{
-              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++;
+        unsigned max_i = 0;
+        bool success;
+        while( max_i<=final_max_i ){
+          Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
+          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<maxs[index] && 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 ){
+              Trace("inst-alg-rd") << "Try instantiation..." << std::endl;
+              index--;
+              //try instantiation
+              std::vector< Node > terms;
+              for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+                if( r==0 ){
+                  terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+                }else{
+                  terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+                }
+              }
+              if( d_quantEngine->addInstantiation( f, terms, false ) ){
+                Trace("inst-alg-rd") << "Success!" << std::endl;
+                ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+                return STATUS_UNKNOWN;
+              }
             }
-          }
-        }while( success );
-        max_i++;
+          }while( success );
+          max_i++;
+        }
       }
-    }
-    //*/
-
-    if( d_guessed.find( f )==d_guessed.end() ){
-      Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
-      d_guessed[f] = true;
-      InstMatch m( f );
-      if( d_quantEngine->addInstantiation( f, m ) ){
-        ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+      if( r==0 ){
+        if( d_guessed.find( f )==d_guessed.end() ){
+          Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
+          d_guessed[f] = true;
+          InstMatch m( f );
+          if( d_quantEngine->addInstantiation( f, m ) ){
+            ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+            return STATUS_UNKNOWN;
+          }
+        }
       }
     }
     return STATUS_UNKNOWN;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 4a5c92c7e..08bd0f179 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -116,6 +116,7 @@ void QuantInfo::initialize( Node q, Node qn ) {
       }

     */

   }

+  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;

 }

 

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

@@ -700,7 +701,7 @@ void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbva
 

 void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {

   Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl;

-  bool isCom = d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF;

+  bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );

   std::map< int, std::vector< int > > c_to_vars;

   std::map< int, std::vector< int > > vars_to_c;

   std::map< int, int > vb_count;

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 9166b81e8..0452278f2 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -34,9 +34,15 @@ void RelevantDomain::RDomain::merge( RDomain * r ) {
   d_terms.clear();
 }
 
-void RelevantDomain::RDomain::addTerm( Node t ) {
-  if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
-    d_terms.push_back( t );
+void RelevantDomain::RDomain::addTerm( Node t, bool nonGround ) {
+  if( !nonGround ){
+    if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
+      d_terms.push_back( t );
+    }
+  }else{
+    if( std::find( d_ng_terms.begin(), d_ng_terms.end(), t )==d_ng_terms.end() ){
+      d_ng_terms.push_back( t );
+    }
   }
 }
 
@@ -138,33 +144,83 @@ void RelevantDomain::compute(){
 }
 
 void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
-
+  Node op = d_qe->getTermDatabase()->getOperator( n );
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    Node op = d_qe->getTermDatabase()->getOperator( n );
     if( !op.isNull() ){
       RDomain * rf = getRDomain( op, i );
+      if( n[i].getKind()==ITE ){
+        for( unsigned j=1; j<=2; j++ ){
+          computeRelevantDomainOpCh( rf, n[i][j] );
+        }
+      }else{
+        computeRelevantDomainOpCh( rf, n[i] );
+      }
+    }
+    //TODO
+    if( n[i].getKind()!=FORALL ){
+      bool newHasPol;
+      bool newPol;
+      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+      computeRelevantDomain( n[i], newHasPol, newPol );
+    }
+  }
+
+  if( n.getKind()==EQUAL || n.getKind()==GEQ ){
+    int varCount = 0;
+    std::vector< RDomain * > rds;
+    int varCh = -1;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( n[i].getKind()==INST_CONSTANT ){
         Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] );
-        //merge the RDomains
         unsigned id = n[i].getAttribute(InstVarNumAttribute());
-        Trace("rel-dom-debug") << n[i] << " is variable # " << id << " for " << q;
-        Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl;
-        RDomain * rq = getRDomain( q, id );
-        if( rf!=rq ){
-          rq->merge( rf );
+        rds.push_back( getRDomain( q, id ) );
+        varCount++;
+        varCh = i;
+      }else{
+        rds.push_back( NULL );
+      }
+    }
+    if( varCount==2 ){
+      //merge the two relevant domains
+      if( ( !hasPol || pol ) && rds[0]!=rds[1] ){
+        rds[0]->merge( rds[1] );
+      }
+    }else if( varCount==1 ){
+      int oCh = varCh==0 ? 1 : 0;
+      bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] );
+      //the negative occurrence adds the term to the domain
+      if( !hasPol || !pol ){
+        rds[varCh]->addTerm( n[oCh] );
+      }
+      //the positive occurence adds other terms
+      if( ( !hasPol || pol ) && n[0].getType().isInteger() ){
+        if( n.getKind()==EQUAL ){
+          for( unsigned i=0; i<2; i++ ){
+            rds[varCh]->addTerm( QuantArith::offset( n[oCh], i==0 ? 1 : -1 ), ng  );
+          }
+        }else if( n.getKind()==GEQ ){
+          Node nt = QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 );
+          rds[varCh]->addTerm( QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ), ng );
         }
-      }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n[i] ) ){
-        //term to add
-        rf->addTerm( n[i] );
       }
     }
+  }
+}
 
-    //TODO
-    if( n[i].getKind()!=FORALL ){
-      bool newHasPol = hasPol;
-      bool newPol = pol;
-      computeRelevantDomain( n[i], newHasPol, newPol );
+void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
+  if( n.getKind()==INST_CONSTANT ){
+    Node q = d_qe->getTermDatabase()->getInstConstAttr( n );
+    //merge the RDomains
+    unsigned id = n.getAttribute(InstVarNumAttribute());
+    Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
+    Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl;
+    RDomain * rq = getRDomain( q, id );
+    if( rf!=rq ){
+      rq->merge( rf );
     }
+  }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n ) ){
+    //term to add
+    rf->addTerm( n );
   }
 }
 
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 0f5afcadd..200e49a72 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -33,8 +33,9 @@ private:
     void reset() { d_parent = NULL; d_terms.clear(); }
     RDomain * d_parent;
     std::vector< Node > d_terms;
+    std::vector< Node > d_ng_terms;
     void merge( RDomain * r );
-    void addTerm( Node t );
+    void addTerm( Node t, bool nonGround = false );
     RDomain * getParent();
     void removeRedundantTerms( FirstOrderModel * fm );
     bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }
@@ -45,6 +46,7 @@ private:
   QuantifiersEngine* d_qe;
   FirstOrderModel* d_model;
   void computeRelevantDomain( Node n, bool hasPol, bool pol );
+  void computeRelevantDomainOpCh( RDomain * rf, Node n );
   bool d_is_computed;
 public:
   RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );