finished implementing bv to bool lifting and added --bv-to-bool option

6 files changed, 144 insertions, 73 deletions

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index f39d12a39..5ab7cf144 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -23,22 +23,40 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
-void BvToBoolVisitor::addToCache(TNode bv_term, Node bool_term) {
-  Assert (!hasCache(bv_term));
+void BvToBoolVisitor::storeBvToBool(TNode bv_term, Node bool_term) {
+  Assert (!hasBoolTerm(bv_term));
   Assert (bool_term.getType().isBoolean()); 
-  d_cache[bv_term] = bool_term; 
+  d_bvToBoolTerm[bv_term] = bool_term; 
 }
 
-Node BvToBoolVisitor::getCache(TNode bv_term) const {
-  Assert (hasCache(bv_term));
-  return d_cache.find(bv_term)->second; 
+Node BvToBoolVisitor::getBoolTerm(TNode bv_term) const {
+  Assert(hasBoolTerm(bv_term));
+  return d_bvToBoolTerm.find(bv_term)->second; 
 }
 
-bool BvToBoolVisitor::hasCache(TNode bv_term) const {
+bool BvToBoolVisitor::hasBoolTerm(TNode bv_term) const {
   Assert (bv_term.getType().isBitVector()); 
-  return d_cache.find(bv_term) != d_cache.end(); 
+  return d_bvToBoolTerm.find(bv_term) != d_bvToBoolTerm.end(); 
 }
 
+void BvToBoolVisitor::addToCache(TNode term, Node new_term) {
+  Assert (new_term != Node()); 
+  Assert (!hasCache(term));
+  d_cache[term] = new_term; 
+}
+
+Node BvToBoolVisitor::getCache(TNode term) const {
+  if (!hasCache(term)) {
+    return term; 
+  }
+  return d_cache.find(term)->second; 
+}
+
+bool BvToBoolVisitor::hasCache(TNode term) const {
+  return d_cache.find(term) != d_cache.end(); 
+}
+
+
 void BvToBoolVisitor::start(TNode node) {}
 
 bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) {
@@ -60,95 +78,126 @@ bool BvToBoolVisitor::isConvertibleToBool(TNode current) {
       kind == kind::BITVECTOR_AND ||
       kind == kind::BITVECTOR_XOR ||
       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::EQUAL) {
-    return current[0].getType().getBitVectorSize() == 1; 
+    // we can convert it to bool if all of the children can also be converted
+    // to bool
+    if (! current[0].getType().getBitVectorSize() == 1)
+      return false; 
+    for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+      // we assume that the children have been visited
+      if (!hasBoolTerm(current[i]))
+        return false; 
+    }
+    return true; 
   }
   if (kind == kind::ITE &&
       type.isBitVector()) {
-    return type.getBitVectorSize() == 1; 
+    return type.getBitVectorSize() == 1 && hasBoolTerm(current[1]) && hasBoolTerm(current[2]); 
   }
   return false; 
 }
 
+
 Node BvToBoolVisitor::convertToBool(TNode current) {
+  Debug("bv-to-bool") << "BvToBoolVisitor::convertToBool (" << current << ") "; 
   Kind kind = current.getKind();
-  if (kind == kind::BITVECTOR_ULT) {
-    TNode a = getCache(current[0]);
-    TNode b = getCache(current[1]);
+
+  Node new_current; 
+  if (current.getNumChildren() == 0) {
+    if (current.getKind() == kind::CONST_BITVECTOR) {
+      new_current = current == d_one? utils::mkTrue() : utils::mkFalse(); 
+    } else {
+      new_current = utils::mkNode(kind::EQUAL, current, d_one); 
+    }
+    Debug("bv-to-bool") << "=> " << new_current << "\n"; 
+  } else if (kind == kind::BITVECTOR_ULT) {
+    TNode a = getBoolTerm(current[0]);
+    TNode b = getBoolTerm(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]);
+    new_current = utils::mkNode(kind::AND, a_eq_0, b_eq_1);
+  }  else if (kind == kind::BITVECTOR_ULE) {
+    TNode a = getBoolTerm(current[0]);
+    TNode b = getBoolTerm(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; 
+    new_current = utils::mkNode(kind::OR, a_lt_b, a_eq_b);
+  } else if (kind == kind::ITE) {
+    TNode cond = current[0];
+    TNode a = getBoolTerm(current[1]);
+    TNode b = getBoolTerm(current[2]);
+    new_current = utils::mkNode(kind::ITE, cond, a, b);
+  } else {
+    Kind new_kind; 
+    switch (kind) {
+    case kind::BITVECTOR_OR :
+      new_kind = kind::OR;
+      break; 
+    case kind::BITVECTOR_AND:
+      new_kind =  kind::AND;
+      break; 
+    case kind::BITVECTOR_XOR:
+      new_kind = kind::XOR;
+      break; 
+    case kind::BITVECTOR_NOT:
+      new_kind =  kind::NOT;
+      break; 
+    case kind::EQUAL:
+      new_kind = kind::IFF;
+      break; 
+    default:
+      Unreachable("Unknown kind ", kind);  
+    }
+    NodeBuilder<> builder(new_kind);
+    if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      builder << current.getOperator();
+    }
+    for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+      builder << getBoolTerm(current[i]); 
+    }
+    new_current = builder;
   }
-
   
-  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]); 
+  Debug("bv-to-bool") << "=> " << new_current << "\n";
+  if (current.getType().isBitVector()) {
+    storeBvToBool(current, new_current); 
+  } else {
+    addToCache(current, new_current); 
   }
-  return builder; 
+  return new_current; 
 }
 
 void BvToBoolVisitor::visit(TNode current, TNode parent) {
+  Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; 
   Assert (!alreadyVisited(current, parent));
   d_visited.insert(current);
-  
-  if (current.getNumChildren() == 0 &&
-      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); 
-    }
-    addToCache(current, bool_current);
-    return; 
-  }
 
+  Node result; 
   // if it has more than one child
   if (isConvertibleToBool(current)) {
-    Node bool_current = convertToBool(current); 
-    addToCache(current, bool_current); 
+    result = convertToBool(current); 
   } else {
-    NodeBuilder<> builder(current.getKind());
-    for (unsigned i = 0; i < current.getNumChildren(); ++i) {
-      Node converted = getCache(current[i]);
-      if (converted.getType() == current[i].getType()) {
-        builder << converted; 
-      } else {
-        builder << current[i]; 
+    if (current.getNumChildren() == 0) {
+      result = current; 
+    } else {
+      NodeBuilder<> builder(current.getKind());
+      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        builder << current.getOperator();
+      }
+      for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+        Node converted = getCache(current[i]);
+        if (converted.getType() == current[i].getType()) {
+          builder << converted; 
+        } else {
+          builder << current[i]; 
+        }
       }
+      result = builder;
     }
-    Node result = builder;
     addToCache(current, result); 
   }
 }
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index ef80930b4..d5673a295 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -29,20 +29,27 @@ class BvToBoolVisitor {
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
   typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap; 
   TNodeNodeMap d_cache;
+  TNodeNodeMap d_bvToBoolTerm; 
   TNodeSet d_visited;
   Node d_one;
   Node d_zero;
 
-  void addToCache(TNode bv_term, Node bool_term);
-  Node getCache(TNode bv_term) const;
-  bool hasCache(TNode bv_term) const; 
+  void storeBvToBool(TNode bv_term, Node bool_term);
+  Node getBoolTerm(TNode bv_term) const;
+  bool hasBoolTerm(TNode bv_term) const; 
 
+  void addToCache(TNode term, Node new_term);
+  Node getCache(TNode term) const;
+  bool hasCache(TNode term) const; 
+
+  
   bool isConvertibleToBool(TNode current);
   Node convertToBool(TNode current);
 public:
   typedef Node return_type;
   BvToBoolVisitor()
     : d_cache(),
+      d_bvToBoolTerm(),
       d_visited(),
       d_one(utils::mkConst(BitVector(1, 1u))),
       d_zero(utils::mkConst(BitVector(1, 0u)))
diff --git a/src/theory/bv/options b/src/theory/bv/options
index 2e53b029c..7b87baa21 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -19,5 +19,8 @@ option bitvectorInequalitySolver --bv-inequality-solver bool :default true
 
 option bitvectorCoreSolver --bv-core-solver bool
  turn on the core solver for the bit-vector theory 
+
+option bvToBool --bv-to-bool bool
+ lift bit-vectors of size 1 to booleans when possible
  
 endmodule
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index c597cb083..c46af5196 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -127,6 +127,7 @@ void TheoryBV::sendConflict() {
 
 void TheoryBV::check(Effort e)
 {
+  Trace("bitvector") <<"TheoryBV::check (" << e << ")\n"; 
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
   if (options::bitvectorEagerBitblast()) {
     return;
@@ -248,10 +249,10 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 
 Node TheoryBV::ppRewrite(TNode t)
 {
-  if (RewriteRule<BitwiseEq>::applies(t)) {
-    Node result = RewriteRule<BitwiseEq>::run<false>(t);
-    return Rewriter::rewrite(result);
-  }
+  // if (RewriteRule<BitwiseEq>::applies(t)) {
+  //   Node result = RewriteRule<BitwiseEq>::run<false>(t);
+  //   return Rewriter::rewrite(result);
+  // }
 
   if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) {
     std::vector<Node> equalities;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 442b1ef1c..6f965879d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -119,7 +119,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms),
-  d_unconstrainedSimp(context, logicInfo)
+  d_unconstrainedSimp(context, logicInfo),
+  d_bvToBoolPreprocessor()
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
     d_theoryTable[theoryId] = NULL;
@@ -1276,6 +1277,12 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   }
 }
 
+Node TheoryEngine::ppBvToBool(TNode assertion) {
+  Node result = d_bvToBoolPreprocessor.liftBoolToBV(assertion);
+  result = Rewriter::rewrite(result);
+  return result; 
+}
+
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
   Node result = d_iteSimplifier.simpITE(assertion);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 9abdaa034..324b952b0 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -45,6 +45,7 @@
 #include "theory/ite_simplifier.h"
 #include "theory/unconstrained_simplifier.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/bv/bv_to_bool.h"
 
 namespace CVC4 {
 
@@ -748,8 +749,11 @@ private:
   /** For preprocessing pass simplifying unconstrained expressions */
   UnconstrainedSimplifier d_unconstrainedSimp;
 
+  /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
+  theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; 
 public:
 
+  Node ppBvToBool(TNode assertion); 
   Node ppSimpITE(TNode assertion);
   void ppUnconstrainedSimp(std::vector<Node>& assertions);