more work on boolean lifting

3 files changed, 117 insertions, 52 deletions

diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index a70521791..8651f280b 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -12,6 +12,8 @@ libbv_la_SOURCES = \
 	type_enumerator.h \
 	bitblaster.h \
 	bitblaster.cpp \
+	bv_to_bool.h \
+	bv_to_bool.cpp \
 	bv_subtheory.h \
 	bv_subtheory_core.h \
 	bv_subtheory_core.cpp \
@@ -36,7 +38,7 @@ libbv_la_SOURCES = \
 	theory_bv_type_rules.h \
 	theory_bv_rewriter.h \
 	theory_bv_rewriter.cpp \
-	cd_set_collection.h 
+	cd_set_collection.h
 
 EXTRA_DIST = \
 	kinds
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index fb25f4348..f39d12a39 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -16,88 +16,149 @@
 
 
 #include "util/node_visitor.h"
+#include "theory/bv/bv_to_bool.h"
 
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
 
-void BVToBoolVisitor::addBvToBool(TNode bv_term, Node bool_term) {
-  Assert (!hasBoolTerm(bv_term));
+void BvToBoolVisitor::addToCache(TNode bv_term, Node bool_term) {
+  Assert (!hasCache(bv_term));
   Assert (bool_term.getType().isBoolean()); 
-  d_bvToBool[bv_term] = bool_term; 
+  d_cache[bv_term] = bool_term; 
 }
 
-Node BVToBoolVisitor::toBoolTerm(TNode bv_term) const {
-  Assert (hasBoolTerm(bv_term));
-  return d_bvToBool.find(bv_term)->second; 
+Node BvToBoolVisitor::getCache(TNode bv_term) const {
+  Assert (hasCache(bv_term));
+  return d_cache.find(bv_term)->second; 
 }
 
-bool BVToBoolVisitor::hasBoolTerm(TNode bv_term) const {
+bool BvToBoolVisitor::hasCache(TNode bv_term) const {
   Assert (bv_term.getType().isBitVector()); 
-  return d_bvToBool.find(bv_term) != d_bvToBool.end(); 
+  return d_cache.find(bv_term) != d_cache.end(); 
 }
 
-void BVToBoolVisitor::start(TNode node) {}
-
-return_type BVToBoolVisitor::done(TNode node) {
-  return 0; 
-}
+void BvToBoolVisitor::start(TNode node) {}
 
 bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) {
   return d_visited.find(current) != d_visited.end(); 
 }
 
 bool BvToBoolVisitor::isConvertibleToBool(TNode current) {
-  if (current.getNumChildren() == 0) {
-    return current.getType().getBitVectorSize() == 1; 
+  TypeNode type = current.getType(); 
+  if (current.getNumChildren() == 0 && type.isBitVector()) {
+    return type.getBitVectorSize() == 1; 
   }
 
+  if (current.getKind() == kind::NOT) {
+    current = current[0];
+  }
   Kind kind = current.getKind();
+  // checking bit-vector kinds 
   if (kind == kind::BITVECTOR_OR ||
       kind == kind::BITVECTOR_AND ||
       kind == kind::BITVECTOR_XOR ||
       kind == kind::BITVECTOR_NOT ||
-      kind == kind::BITVECTOR_ADD ||
-      kind == kind::BITVECTOR_NOT ||
+      // kind == kind::BITVECTOR_PLUS ||
+      // kind == kind::BITVECTOR_SUB ||
+      // kind == kind::BITVECTOR_NEG ||
       kind == kind::BITVECTOR_ULT ||
-      kind == kind::BITVECTOR_ULE) {
+      kind == kind::BITVECTOR_ULE ||
+      kind == kind::EQUAL) {
     return current[0].getType().getBitVectorSize() == 1; 
   }
+  if (kind == kind::ITE &&
+      type.isBitVector()) {
+    return type.getBitVectorSize() == 1; 
+  }
+  return false; 
 }
 
-void BvToBoolVisitor::visit(TNode current, TNode parent) {
-  Assert (!alreadyVisited());
-  
-  if (current.getType().isBitVector() &&
-      current.getType().getBitVectorSize() != 1) {
-    // we only care about bit-vector terms of size 1
-    d_visited.push_back(current);
-    return; 
+Node BvToBoolVisitor::convertToBool(TNode current) {
+  Kind kind = current.getKind();
+  if (kind == kind::BITVECTOR_ULT) {
+    TNode a = getCache(current[0]);
+    TNode b = getCache(current[1]);
+    Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero);
+    Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one);
+    Node new_current = utils::mkNode(kind::AND, a_eq_0, b_eq_1);
+    return new_current; 
+  }
+  if (kind == kind::BITVECTOR_ULE) {
+    TNode a = getCache(current[0]);
+    TNode b = getCache(current[1]);
+    Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero);
+    Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one);
+    Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); 
+    Node a_eq_b = utils::mkNode(kind::EQUAL, a, b);
+    Node new_current = utils::mkNode(kind::OR, a_lt_b, a_eq_b);
+    return new_current; 
   }
+
   
+  Kind new_kind; 
+  switch (kind) {
+  case kind::BITVECTOR_OR :
+    new_kind = kind::OR;
+  case kind::BITVECTOR_AND:
+    new_kind =  kind::AND;
+  case kind::BITVECTOR_XOR:
+    new_kind = kind::XOR;
+  case kind::BITVECTOR_NOT:
+    new_kind =  kind::NOT;
+  case kind::BITVECTOR_ULT:
+  default:
+    Unreachable();  
+  }
+  NodeBuilder<> builder(new_kind);
+  for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+    builder << getCache(current[i]); 
+  }
+  return builder; 
+}
+
+void BvToBoolVisitor::visit(TNode current, TNode parent) {
+  Assert (!alreadyVisited(current, parent));
   d_visited.insert(current);
   
   if (current.getNumChildren() == 0 &&
-      current.getType().isBitVector() &&
-      current.getType().getBitVectorSize() == 1) {
+      isConvertibleToBool(current)) {
     Node bool_current; 
     if (current.getKind() == kind::CONST_BITVECTOR) {
       bool_current = current == d_one? utils::mkTrue() : utils::mkFalse(); 
     } else {
       bool_current = utils::mkNode(kind::EQUAL, current, d_one); 
     }
-    addBvToBool(current, current_eq_one);
+    addToCache(current, bool_current);
     return; 
   }
 
   // if it has more than one child
-  if (current.getKind().isBitVectorKind() && isConvertibleToBool(current)) {
-    Kind bool_kind = boolToBvKind(current.getKind());
-    NodeBuilder<> builder(bool_kind); 
+  if (isConvertibleToBool(current)) {
+    Node bool_current = convertToBool(current); 
+    addToCache(current, bool_current); 
+  } else {
+    NodeBuilder<> builder(current.getKind());
     for (unsigned i = 0; i < current.getNumChildren(); ++i) {
-      builder << toBoolTerm(current[i]); 
+      Node converted = getCache(current[i]);
+      if (converted.getType() == current[i].getType()) {
+        builder << converted; 
+      } else {
+        builder << current[i]; 
+      }
     }
-    Node bool_current = builder;
-    addBvToBool(current, bool_current); 
-  } 
+    Node result = builder;
+    addToCache(current, result); 
+  }
 }
 
-return_type BvToBoolVisitor::done(TNode node) {}
+BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) {
+  Assert (hasCache(node)); 
+  return getCache(node); 
+}
 
+Node BvToBoolPreprocessor::liftBoolToBV(TNode assertion) {
+  Node result = NodeVisitor<BvToBoolVisitor>::run(d_visitor, assertion);
+  return result; 
+}
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index 6e865658f..ef80930b4 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -15,6 +15,7 @@
  **/
 
 #include "cvc4_private.h"
+#include "theory/bv/theory_bv_utils.h"
 
 #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
 #define __CVC4__THEORY__BV__BV_TO_BOOL_H
@@ -24,22 +25,25 @@ namespace theory {
 namespace bv {
 
 class BvToBoolVisitor {
-  typedef unsigned return_type;
-  typedef __gnu_cxx::hash_set<TNode> TNodeSet; 
-  typedef __gnu_cxx::hash_map<TNode, Node> TNodeNodeMap; 
-  TNodeNodeMap d_bvToBool;
+
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
+  typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap; 
+  TNodeNodeMap d_cache;
   TNodeSet d_visited;
   Node d_one;
   Node d_zero;
 
-  void addBvToBool(TNode bv_term, Node bool_term);
-  Node toBoolTerm(TNode bv_term) const;
-  bool hasBoolTerm(TNode bv_term) const; 
-  
+  void addToCache(TNode bv_term, Node bool_term);
+  Node getCache(TNode bv_term) const;
+  bool hasCache(TNode bv_term) const; 
+
+  bool isConvertibleToBool(TNode current);
+  Node convertToBool(TNode current);
 public:
+  typedef Node return_type;
   BvToBoolVisitor()
-    : d_substitution(),
-      d_visited,
+    : d_cache(),
+      d_visited(),
       d_one(utils::mkConst(BitVector(1, 1u))),
       d_zero(utils::mkConst(BitVector(1, 0u)))
   {}
@@ -47,18 +51,16 @@ public:
   bool alreadyVisited(TNode current, TNode parent);
   void visit(TNode current, TNode parent);
   return_type done(TNode node);
-  Node liftBoolToBV(TNode node);
-  
 }; 
 
 class BvToBoolPreprocessor {
   BvToBoolVisitor d_visitor; 
 public:
   BvToBoolPreprocessor()
-    : d_visitor
+    : d_visitor()
   {}
   ~BvToBoolPreprocessor() {}
-  Node liftBvToBool(TNode assertion); 
+  Node liftBoolToBV(TNode assertion);
 };