started work on bv1 to boolean lifting

2 files changed, 174 insertions, 0 deletions

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
new file mode 100644
index 000000000..fb25f4348
--- /dev/null
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -0,0 +1,103 @@
+/*********************                                                        */
+/*! \file bv_to_bool.h
+ ** \verbatim
+ ** Original author: Liana Hadarean 
+ ** Major contributors: None. 
+ ** Minor contributors (to current version): None. 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ **
+ ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. 
+ **/
+
+
+#include "util/node_visitor.h"
+
+
+void BVToBoolVisitor::addBvToBool(TNode bv_term, Node bool_term) {
+  Assert (!hasBoolTerm(bv_term));
+  Assert (bool_term.getType().isBoolean()); 
+  d_bvToBool[bv_term] = bool_term; 
+}
+
+Node BVToBoolVisitor::toBoolTerm(TNode bv_term) const {
+  Assert (hasBoolTerm(bv_term));
+  return d_bvToBool.find(bv_term)->second; 
+}
+
+bool BVToBoolVisitor::hasBoolTerm(TNode bv_term) const {
+  Assert (bv_term.getType().isBitVector()); 
+  return d_bvToBool.find(bv_term) != d_bvToBool.end(); 
+}
+
+void BVToBoolVisitor::start(TNode node) {}
+
+return_type BVToBoolVisitor::done(TNode node) {
+  return 0; 
+}
+
+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; 
+  }
+
+  Kind kind = current.getKind();
+  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_ULT ||
+      kind == kind::BITVECTOR_ULE) {
+    return current[0].getType().getBitVectorSize() == 1; 
+  }
+}
+
+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; 
+  }
+  
+  d_visited.insert(current);
+  
+  if (current.getNumChildren() == 0 &&
+      current.getType().isBitVector() &&
+      current.getType().getBitVectorSize() == 1) {
+    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);
+    return; 
+  }
+
+  // if it has more than one child
+  if (current.getKind().isBitVectorKind() && isConvertibleToBool(current)) {
+    Kind bool_kind = boolToBvKind(current.getKind());
+    NodeBuilder<> builder(bool_kind); 
+    for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+      builder << toBoolTerm(current[i]); 
+    }
+    Node bool_current = builder;
+    addBvToBool(current, bool_current); 
+  } 
+}
+
+return_type BvToBoolVisitor::done(TNode node) {}
+
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
new file mode 100644
index 000000000..6e865658f
--- /dev/null
+++ b/src/theory/bv/bv_to_bool.h
@@ -0,0 +1,71 @@
+/*********************                                                        */
+/*! \file bv_to_bool.h
+ ** \verbatim
+ ** Original author: Liana Hadarean 
+ ** Major contributors: None. 
+ ** Minor contributors (to current version): None. 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ **
+ ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. 
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
+#define __CVC4__THEORY__BV__BV_TO_BOOL_H
+
+namespace CVC4 {
+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;
+  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; 
+  
+public:
+  BvToBoolVisitor()
+    : d_substitution(),
+      d_visited,
+      d_one(utils::mkConst(BitVector(1, 1u))),
+      d_zero(utils::mkConst(BitVector(1, 0u)))
+  {}
+  void start(TNode node);
+  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
+  {}
+  ~BvToBoolPreprocessor() {}
+  Node liftBvToBool(TNode assertion); 
+}; 
+
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+
+}/* CVC4 namespace */
+
+
+#endif /* __CVC4__THEORY__BV__BV_TO_BOOL_H */