Add lazy strategy for bounded integers to avoid non-terminating unsat cases. Add...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0604988d344ccdf68eb5739ca13ba5cb5c343cf1..4deb43f4257b23f5943f9b98df78171f1734381f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -941,6 +941,9 @@ void SmtEngine::setDefaults() {
       Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
     }
     if(! options::fmfBoundInt.wasSetByUser()) {
+      if(! options::fmfBoundIntLazy.wasSetByUser()) {
+        options::fmfBoundIntLazy.set( true );
+      }
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
@@ -1178,6 +1181,9 @@ void SmtEngine::setDefaults() {
   if( options::recurseCbqi() ){
     options::cbqi.set( true );
   }
+  if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) {
+    options::fmfBoundInt.set( true );
+  }
   if( options::fmfBoundInt() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index a294eec5ae544d49136da6f123221e5319bf4691..17446358c8af870865cbaba82d63fa143813dc53 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/options.h"
 
 using namespace CVC4;
 using namespace std;
@@ -26,9 +27,22 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
+
+BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::Context* c, bool isProxy) : d_bi(bi),
+      d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) { 
+  if( options::fmfBoundIntLazy() ){
+    d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() );
+  }else{
+    d_proxy_range = r;
+  }
+  if( !isProxy ){
+    Trace("bound-int") << "Introduce proxy " << d_proxy_range << " for " << d_range << std::endl;
+  }
+}
+
 void BoundedIntegers::RangeModel::initialize() {
   //add initial split lemma
-  Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) );
+  Node ltr = NodeManager::currentNM()->mkNode( LT, d_proxy_range, NodeManager::currentNM()->mkConst( Rational(0) ) );
   ltr = Rewriter::rewrite( ltr );
   Trace("bound-int-lemma") << " *** bound int: initial split on " << ltr << std::endl;
   d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
@@ -55,6 +69,7 @@ void BoundedIntegers::RangeModel::assertNode(Node n) {
         bool needsRange = true;
         for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
           if( d_range_assertions.find( it->first )==d_range_assertions.end() ){
+            Trace("bound-int-debug") << "Does not need range because of " << it->first << std::endl;
             needsRange = false;
             break;
           }
@@ -82,7 +97,7 @@ void BoundedIntegers::RangeModel::allocateRange() {
   int newBound = d_curr_max;
   Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
   //TODO: newBound should be chosen in a smarter way
-  Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );
+  Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_proxy_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );
   ltr = Rewriter::rewrite( ltr );
   Trace("bound-int-lemma") << " *** bound int: split on " << ltr << std::endl;
   d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
@@ -113,6 +128,24 @@ Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
   return Node::null();
 }
 
+bool BoundedIntegers::RangeModel::proxyCurrentRange() {
+  //Trace("model-engine") << "Range(" << d_range << ") currently is " << d_curr_max.get() << std::endl;
+  if( d_range!=d_proxy_range ){
+    //int curr = d_curr_range.get();
+    int curr = d_curr_max;
+    if( d_ranges_proxied.find( curr )==d_ranges_proxied.end() ){
+      d_ranges_proxied[curr] = true;
+      Assert( d_range_literal.find( curr )!=d_range_literal.end() );
+      Node lem = NodeManager::currentNM()->mkNode( IFF, d_range_literal[curr].negate(),
+                   NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(curr) ) ) );
+      Trace("bound-int-lemma") << "*** bound int : proxy lemma : " << lem << std::endl;
+      d_bi->getQuantifiersEngine()->addLemma( lem );
+      return true;
+    }
+  }
+  return false;
+}
+
 
 BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) :
 QuantifiersModule(qe), d_assertions(c){
@@ -211,7 +244,18 @@ void BoundedIntegers::process( Node f, Node n, bool pol,
 }
 
 void BoundedIntegers::check( Theory::Effort e ) {
-
+  if( e==Theory::EFFORT_LAST_CALL ){
+    bool addedLemma = false;
+    //make sure proxies are up-to-date with range
+    for( unsigned i=0; i<d_ranges.size(); i++) {
+      if( d_rms[d_ranges[i]]->proxyCurrentRange() ){
+        addedLemma = true;
+      }
+    }
+    if( addedLemma ){
+      d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
+    }
+  }
 }
 
 
@@ -275,18 +319,20 @@ void BoundedIntegers::registerQuantifier( Node f ) {
       for( unsigned i=0; i<d_set[f].size(); i++) {
         Node v = d_set[f][i];
         Node r = d_range[f][v];
+        bool isProxy = false;
         if( r.hasBoundVar() ){
           //introduce a new bound
           Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" );
           d_nground_range[f][v] = d_range[f][v];
           d_range[f][v] = new_range;
           r = new_range;
+          isProxy = true;
         }
         if( r.getKind()!=CONST_RATIONAL ){
           if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){
             Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl;
             d_ranges.push_back( r );
-            d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );
+            d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext(), isProxy );
             d_rms[r]->initialize();
           }
         }
@@ -387,3 +433,4 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
 bool BoundedIntegers::isGroundRange(Node f, Node v) {
   return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar();
 }
+

diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 4130bffeec25c670b8e791dcec6f79e641a5bbfe..a6e85b39235861646bd80d4336043e9e03dc0561 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -60,9 +60,9 @@ private:
   private:
     BoundedIntegers * d_bi;
     void allocateRange();
+    Node d_proxy_range;
   public:
-    RangeModel(BoundedIntegers * bi, Node r, context::Context* c) : d_bi(bi),
-      d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) {}
+    RangeModel(BoundedIntegers * bi, Node r, context::Context* c, bool isProxy);
     Node d_range;
     int d_curr_max;
     std::map< int, Node > d_range_literal;
@@ -71,9 +71,11 @@ private:
     NodeBoolMap d_range_assertions;
     context::CDO< bool > d_has_range;
     context::CDO< int > d_curr_range;
+    std::map< int, bool > d_ranges_proxied;
     void initialize();
     void assertNode(Node n);
     Node getNextDecisionRequest();
+    bool proxyCurrentRange();
   };
 private:
   //information for minimizing ranges

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index f02a3bce199a2826bb90d7949d5321577f30cf71..f8f1744edb81a62e97bf77c54ef1449e9a3a8ab1 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -119,6 +119,8 @@ option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
 option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
  finite model finding on bounded integer quantification
+option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write
+ enforce bounds for bounded integer quantification lazily via use of proxy variables
 
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
  policy for instantiating axioms

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 53163cd5f71e4e68017967951e9b3a235bdf6651..83733da428a63de0b20a79d95656d26cf5f0aa8f 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -91,14 +91,14 @@ d_lemmas_produced_c(u){
     d_inst_engine = NULL;
   }
   if( options::finiteModelFind()  ){
-    d_model_engine = new quantifiers::ModelEngine( c, this );
-    d_modules.push_back( d_model_engine );
     if( options::fmfBoundInt() ){
       d_bint = new quantifiers::BoundedIntegers( c, this );
       d_modules.push_back( d_bint );
     }else{
       d_bint = NULL;
     }
+    d_model_engine = new quantifiers::ModelEngine( c, this );
+    d_modules.push_back( d_model_engine );
   }else{
     d_model_engine = NULL;
     d_bint = NULL;

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index f12e67401e1ed72103d65ce5da3d09861124885c..e399b4b23b5b60b53c1404b2d0966eca69c07b9d 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -41,7 +41,8 @@ TESTS =       \
        qcft-smtlib3dbc51.smt2 \
        symmetric_unsat_7.smt2 \
        javafe.ast.StmtVec.009.smt2 \
-       ARI176e1.smt2
+       ARI176e1.smt2 \
+  bi-artm-s.smt2
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2

diff --git a/test/regress/regress0/quantifiers/bi-artm-s.smt2 b/test/regress/regress0/quantifiers/bi-artm-s.smt2
new file mode 100644 (file)
index 0000000..5fb7522
--- /dev/null
+++ b/test/regress/regress0/quantifiers/bi-artm-s.smt2
@@ -0,0 +1,29 @@
+; COMMAND-LINE: --fmf-bound-int-lazy
+; EXPECT: unsat
+(set-option :incremental "false")
+(set-info :status unsat)
+(set-logic ALL_SUPPORTED)
+(declare-fun Y () String)
+(set-info :notes "ufP_1 is uf type conv P")
+(declare-fun ufP_1 (Int) Int)
+(set-info :notes "ufM_2 is uf type conv M")
+(declare-fun ufM_2 (Int) Int)
+(declare-fun z1_3 () String)
+(declare-fun z2_4 () String)
+(declare-fun z3_5 () String)
+(declare-fun V_253 () String) 
+(declare-fun V_254 () String)
+
+(assert (or (= Y "1") (= Y "0")))
+(assert (>= (ufP_1 0) 32))
+(assert 
+
+(forall ((V_243 Int)) 
+(or 
+(not (and (>= V_243 0) (>= (+ (str.len Y) (* (- 1) V_243)) 1))) 
+(and 
+(or (not (= (str.len Y) (+ 1 V_243))) (= (ufP_1 V_243) (ufM_2 V_243))) 
+(not (>= (ufM_2 V_243) 10)) 
+(not (or (not (= (str.len Y) (+ 1 V_243 (str.len V_253)))) (not (= Y (str.++ V_253 (ite (= (ufM_2 V_243) 0) "0" "1") V_254)))) ))) ))
+
+(check-sat)

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index dd3c6b53a2f94691723f5fd05fb1fab13f4185c2..ddc0eae7c10a29e805ff5c4a8ddf24fe3c36b920 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -47,7 +47,8 @@ TESTS =       \
   loop007.smt2 \
   loop008.smt2 \
   loop009.smt2 \
-  reloop.smt2
+  reloop.smt2 \
+  artemis-0512-nonterm.smt2
 
 FAILING_TESTS =
 

diff --git a/test/regress/regress0/strings/artemis-0512-nonterm.smt2 b/test/regress/regress0/strings/artemis-0512-nonterm.smt2
new file mode 100644 (file)
index 0000000..ed97f36
--- /dev/null
+++ b/test/regress/regress0/strings/artemis-0512-nonterm.smt2
@@ -0,0 +1,25 @@
+(set-logic QF_S)
+(set-info :status unsat)
+
+(declare-const Y String)
+(assert
+  (or
+    (= Y "01")
+    (= Y "02")
+    (= Y "03")
+    (= Y "04")
+    (= Y "05")
+    (= Y "06")
+    (= Y "07")
+    (= Y "08")
+    (= Y "09")
+    (= Y "10")
+    (= Y "11")
+    (= Y "12")
+  )
+)
+ 
+(assert (= (<= (str.to.int Y) 31) false))
+ 
+(check-sat)
+