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

5 files changed, 65 insertions, 8 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0604988d3..4deb43f42 100644
--- 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 a294eec5a..17446358c 100644
--- 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 4130bffee..a6e85b392 100644
--- 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 f02a3bce1..f8f1744ed 100644
--- 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 53163cd5f..83733da42 100644
--- 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;