More complete guess instantiation strategy, cvc4 now typically times out instead...

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index a05abfa29120e98ce2f9eadf4ca6bc19346e5be4..8c00c5af46ccc4e52edb8fef84f56d50f55bf16a 100644 (file)
--- 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 ab3a1aa520e2431791ae807b638104052230a7cd..2ac9dadcfdb2907bbff13391802f5a0baffea1ed 100644 (file)
--- 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 25a62a4e8a8fc3d567b4e61885a71ff5e6f09237..5e2353e8a3e1e74acbde5da6fd62c8583550a8ad 100644 (file)
--- 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 4a5c92c7e4faaf5de9f690ffdd31293762a5b67b..08bd0f1794d4ad684c6dff5d717b15638b72d53b 100755 (executable)
--- 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 ) {
       }\r
     */\r
   }\r
+  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;\r
 }\r
 \r
 void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {\r
@@ -700,7 +701,7 @@ void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbva
 \r
 void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {\r
   Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl;\r
-  bool isCom = d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF;\r
+  bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );\r
   std::map< int, std::vector< int > > c_to_vars;\r
   std::map< int, std::vector< int > > vars_to_c;\r
   std::map< int, int > vb_count;\r

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 9166b81e880da1c99b13cdc78a3a59b703cdd982..0452278f28f7f93351e6150b75fa69c2967bd1cc 100644 (file)
--- 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 0f5afcaddd689626aa047ebc028acf6f3b3b4965..200e49a72cb0062e987d344e589f534e152961ef 100644 (file)
--- 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 );

diff --git a/test/regress/regress0/bug512.minimized.smt2 b/test/regress/regress0/bug512.minimized.smt2
index 0b19f26df408d38982d3977742bccfdcf4c1d042..1a2aaf56f55afcebb6fd6c465cd7b164c90a1a37 100644 (file)
--- a/test/regress/regress0/bug512.minimized.smt2
+++ b/test/regress/regress0/bug512.minimized.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --tlimit-per 1000
 ; EXPECT: unknown
 (set-logic UF)
 (declare-sort T 0)

diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress0/bug519.smt2
index 22fdff674426288d476f717ab86c648ae677adda..406cb0c1b64a90029a268742903831b39d570594 100644 (file)
--- a/test/regress/regress0/bug519.smt2
+++ b/test/regress/regress0/bug519.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -mi
+; COMMAND-LINE: -mi --tlimit-per 1000
 ; EXPECT: unknown
 ; EXPECT: unsat
 

diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 36620419108834a373bc07e5210e9aa57e5a1da1..90a18f0e2ea5e8fa0588d61500f1a69a3f388c76 100644 (file)
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -25,7 +25,6 @@ TESTS =       \
        bitvec5.smt \
        quant-Arrays_Q1-noinfer.smt2 \
        quant-ex1.smt2 \
-       quant-ex1.disable_miniscope.smt2 \
        uflia-xs-09-16-3-4-1-5.delta03.smt \
        aufbv-fuzz01.smt \
        bug347.smt \

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 93d513d9f589b131649658461ea7daa216c9e7d6..c478248da0d75b80513642aabdc4f4af3d5eeff1 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -28,10 +28,8 @@ TESTS =      \
        bug269.smt2 \
        burns13.smt2 \
        burns4.smt2 \
-       ex1.smt2 \
        ex3.smt2 \
        ex6.smt2 \
-       ex7.smt2 \
        opisavailable-12.smt2 \
        ricart-agrawala6.smt2 \
        set8.smt2 \

diff --git a/test/regress/regress0/quantifiers/ex1.smt2 b/test/regress/regress0/quantifiers/ex1.smt2
deleted file mode 100644 (file)
index 20230a6..0000000
--- a/test/regress/regress0/quantifiers/ex1.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-sort U 0)
-(declare-fun a () U)
-(declare-fun b () U)
-(declare-fun f (U) U)
-(declare-fun p () Bool)
-(assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
-(check-sat)
-(get-info :reason-unknown)
-(exit)

diff --git a/test/regress/regress0/quantifiers/ex1.smt2.expect b/test/regress/regress0/quantifiers/ex1.smt2.expect
deleted file mode 100644 (file)
index 2bd8349..0000000
--- a/test/regress/regress0/quantifiers/ex1.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)

diff --git a/test/regress/regress0/quantifiers/ex7.smt2 b/test/regress/regress0/quantifiers/ex7.smt2
deleted file mode 100644 (file)
index 11a83fd..0000000
--- a/test/regress/regress0/quantifiers/ex7.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-sort U 0)
-(declare-fun a () U)
-(declare-fun b () U)
-(declare-fun c () U)
-(declare-fun f (U) U)
-(assert (and (= a b) (forall ((x U)) (=> (or (= (f x) c) (= x a)) (= x b)))))
-(check-sat)
-(get-info :reason-unknown)
-(exit)

diff --git a/test/regress/regress0/quantifiers/ex7.smt2.expect b/test/regress/regress0/quantifiers/ex7.smt2.expect
deleted file mode 100644 (file)
index 2bd8349..0000000
--- a/test/regress/regress0/quantifiers/ex7.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)