From 5d4ee83cd9b245810c35b0aa17bb51b5a456c24b Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 1 Dec 2012 01:48:40 +0000
Subject: [PATCH] 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.)
---
 src/smt/boolean_terms.cpp         | 45 ++++++++++++++++++++++++++++---
 src/smt/model_postprocessor.cpp   |  2 --
 test/regress/regress0/Makefile.am |  1 +
 test/regress/regress0/bug411.smt2 |  8 ++++++
 4 files changed, 50 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/regress0/bug411.smt2

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 15a1244e2..816aba8a6 100644
--- 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 fb0ee808e..26f5c9c60 100644
--- 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 ffc9a4204..0f6c11be9 100644
--- 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
index 000000000..af9acb97a
--- /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)
-- 
2.30.2