Fix for bounded integers when incremental, fixes bug 588. Add option --dt-binary...

diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index 7e56b4d7a77d72480f2d1711418c3a343d99d9ad..bc7552862a2a497c6132148c388b9f565bf9fc73 100644 (file)
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -13,6 +13,8 @@ expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false
  rewrite incorrectly applied selectors to arbitrary ground term
 option dtForceAssignment --dt-force-assignment bool :default false :read-write
  force the datatypes solver to give specific values to all datatypes terms before answering sat
+option dtBinarySplit --dt-binary-split bool :default false
+ do binary splits for datatype constructor types
 option cdtBisimilar --cdt-bisimilar bool :default true
  do bisimilarity check for co-datatypes
  

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index f717e7701aa43bb768ed9221b80a02e7bbc10056..b7e2e5eb38498a37408c1ca8aa05a1f4e1a62c0e 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -222,14 +222,25 @@ void TheoryDatatypes::check(Effort e) {
                 Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
                 d_infer.push_back( t );
               }else{
-                Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
-                std::vector< Node > children;
-                for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-                  Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n );
-                  children.push_back( test );
+                if( options::dtBinarySplit() ){
+                  Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
+                  Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
+                  test = Rewriter::rewrite( test );
+                  NodeBuilder<> nb(kind::OR);
+                  nb << test << test.notNode();
+                  Node lemma = nb;
+                  d_out->lemma( lemma );
+                  d_out->requirePhase( test, true );
+                }else{
+                  Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
+                  std::vector< Node > children;
+                  for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+                    Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n );
+                    children.push_back( test );
+                  }
+                  Node lemma = NodeManager::currentNM()->mkNode( kind::OR, children );
+                  d_out->lemma( lemma );
                 }
-                Node lemma = NodeManager::currentNM()->mkNode( kind::OR, children );
-                d_out->lemma( lemma );
                 return;
               }
             }else{

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 57799fd8edb976721fa83b83c593434fb459da4f..91c04bc80dea4d282665724f5069681d52260fa2 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -28,8 +28,8 @@ 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) { 
+BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi),
+      d_range(r), d_curr_max(-1), d_lit_to_range(u), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1), d_ranges_proxied(u) { 
   if( options::fmfBoundIntLazy() ){
     d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() );
   }else{
@@ -59,17 +59,18 @@ void BoundedIntegers::RangeModel::assertNode(Node n) {
   bool pol = n.getKind()!=NOT;
   Node nlit = n.getKind()==NOT ? n[0] : n;
   if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){
+    int vrange = d_lit_to_range[nlit];
     Trace("bound-int-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";
     Trace("bound-int-assert") << ", found literal " << nlit;
-    Trace("bound-int-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl;
+    Trace("bound-int-assert") << ", it is bound literal " << vrange << " for " << d_range << std::endl;
     d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]);
     if( pol!=d_lit_to_pol[nlit] ){
       //check if we need a new split?
       if( !d_has_range ){
         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;
+        for( NodeIntMap::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;
           }
@@ -79,9 +80,9 @@ void BoundedIntegers::RangeModel::assertNode(Node n) {
         }
       }
     }else{
-      if (!d_has_range || d_lit_to_range[nlit]<d_curr_range ){
-        Trace("bound-int-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;
-        d_curr_range = d_lit_to_range[nlit];
+      if (!d_has_range || vrange<d_curr_range ){
+        Trace("bound-int-bound") << "Successfully bound " << d_range << " to " << vrange << std::endl;
+        d_curr_range = vrange;
       }
       //set the range
       d_has_range = true;
@@ -111,13 +112,13 @@ void BoundedIntegers::RangeModel::allocateRange() {
 
 Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
   //request the current cardinality as a decision literal, if not already asserted
-  for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
-    int i = it->second;
+  for( NodeIntMap::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
+    int i = (*it).second;
     if( !d_has_range || i<d_curr_range ){
-      Node rn = it->first;
+      Node rn = (*it).first;
       Assert( !rn.isNull() );
       if( d_range_assertions.find( rn )==d_range_assertions.end() ){
-        if (!d_lit_to_pol[it->first]) {
+        if (!d_lit_to_pol[rn]) {
           rn = rn.negate();
         }
         Trace("bound-int-dec-debug") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;
@@ -335,7 +336,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
           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(), isProxy );
+            d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext(), d_quantEngine->getUserContext(), isProxy );
             d_rms[r]->initialize();
           }
         }

diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 355360e41f9e0801ba43d37805320c7d3f67543d..c09527f89e529aa203fd03fc9fe1b2949ecd7396 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -38,6 +38,7 @@ class BoundedIntegers : public QuantifiersModule
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+  typedef context::CDHashMap<int, bool> IntBoolMap;
 private:
   //for determining bounds
   bool isBound( Node f, Node v );
@@ -62,16 +63,16 @@ private:
     void allocateRange();
     Node d_proxy_range;
   public:
-    RangeModel(BoundedIntegers * bi, Node r, context::Context* c, bool isProxy);
+    RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy);
     Node d_range;
     int d_curr_max;
     std::map< int, Node > d_range_literal;
     std::map< Node, bool > d_lit_to_pol;
-    std::map< Node, int > d_lit_to_range;
+    NodeIntMap d_lit_to_range;
     NodeBoolMap d_range_assertions;
     context::CDO< bool > d_has_range;
     context::CDO< int > d_curr_range;
-    std::map< int, bool > d_ranges_proxied;
+    IntBoolMap d_ranges_proxied;
     void initialize();
     void assertNode(Node n);
     Node getNextDecisionRequest();