more work on boolean lifting

1 files changed, 98 insertions, 37 deletions

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; 
+}