Some fixes for boolean arrays

also a regression for bug 411

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 15a1244e297fa8181ceb35a8f2187679d6294ab8..816aba8a6b450906570265c3bed6fce1b73f0510 100644 (file)
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -31,6 +31,27 @@ using namespace CVC4::theory;
 namespace CVC4 {
 namespace smt {
 
+static inline bool isBoolean(TNode top, unsigned i) {
+  switch(top.getKind()) {
+  case kind::NOT:
+  case kind::AND:
+  case kind::IFF:
+  case kind::IMPLIES:
+  case kind::OR:
+  case kind::XOR:
+    return true;
+
+  case kind::ITE:
+    if(i == 0) {
+      return true;
+    }
+    return top.getType().isBoolean();
+
+  default:
+    return false;
+  }
+}
+
 const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype& dt) throw() {
   return dt;
   // boolean terms not supported in datatypes, yet
@@ -156,6 +177,17 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
                               NodeManager::SKOLEM_EXACT_NAME);
         top.setAttribute(BooleanTermAttr(), n);
         Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+        Node one = nm->mkConst(BitVector(1u, 1u));
+        Node zero = nm->mkConst(BitVector(1u, 0u));
+        Node n_zero = nm->mkNode(kind::SELECT, n, zero);
+        Node n_one = nm->mkNode(kind::SELECT, n, one);
+        Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr()));
+        Node repl = nm->mkNode(kind::STORE,
+                    nm->mkNode(kind::STORE, base, nm->mkConst(false),
+                               nm->mkNode(kind::EQUAL, n_zero, one)), nm->mkConst(true),
+                               nm->mkNode(kind::EQUAL, n_one, one));
+        Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
+        d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
         d_booleanTermCache[make_pair(top, boolParent)] = n;
         return n;
       }
@@ -252,19 +284,24 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
          k != kind::RECORD_UPDATE &&
          k != kind::RECORD) {
         Debug("bt") << "rewriting: " << top.getOperator() << std::endl;
-        b << rewriteBooleanTerms(top.getOperator(), kindToTheoryId(k) == THEORY_BOOL);
+        b << rewriteBooleanTerms(top.getOperator(), false);
         Debug("bt") << "got: " << b.getOperator() << std::endl;
       } else {
         b << top.getOperator();
       }
     }
-    for(TNode::const_iterator i = top.begin(); i != top.end(); ++i) {
-      Debug("bt") << "rewriting: " << *i << std::endl;
-      b << rewriteBooleanTerms(*i, kindToTheoryId(k) == THEORY_BOOL);
+    for(unsigned i = 0; i < top.getNumChildren(); ++i) {
+      Debug("bt") << "rewriting: " << top[i] << std::endl;
+      b << rewriteBooleanTerms(top[i], isBoolean(top, i));
       Debug("bt") << "got: " << b[b.getNumChildren() - 1] << std::endl;
     }
     Node n = b;
     Debug("boolean-terms") << "constructed: " << n << endl;
+    if(boolParent &&
+       n.getType().isBitVector() &&
+       n.getType().getBitVectorSize() == 1) {
+      n = nm->mkNode(kind::EQUAL, n, nm->mkConst(BitVector(1u, 1u)));
+    }
     d_booleanTermCache[make_pair(top, boolParent)] = n;
     return n;
   }

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index fb0ee808e517dac51e247d37b99d4225624e8966..26f5c9c6052d84ed137ad5df5f268e91409157b5 100644 (file)
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -44,8 +44,6 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     }
     d_nodes[current] = b;
     Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
-  } else if(current.hasAttribute(smt::BooleanTermAttr())) {
-    Debug("boolean-terms") << "found bool-term attr on: " << current << std::endl;
   } else {
     Debug("tuprec") << "returning self" << std::endl;
     // rewrite to self

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index ffc9a420494cbc94aff571d79db42d6ce2ec9b2d..0f6c11be96d4881eb1bda2c441a3fd0b6ad346cb 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -139,6 +139,7 @@ BUG_TESTS = \
        bug382.smt2 \
        bug383.smt2 \
        bug398.smt2 \
+       bug411.smt2 \
        bug421.smt2 \
        bug421b.smt2 \
        bug425.cvc

diff --git a/test/regress/regress0/bug411.smt2 b/test/regress/regress0/bug411.smt2
new file mode 100644 (file)
index 0000000..af9acb9
--- /dev/null
+++ b/test/regress/regress0/bug411.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+; EXPECT: (define-fun x () Int 5)
+; EXIT: 10
+(set-option :produce-models true)
+(set-logic QF_UFLIA)
+(define-fun x () Int 5)
+(check-sat)
+(get-model)