diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-04-10 00:03:02 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
commit | e4f5359675972341858fe167f454ed5da4d8c115 (patch) | |
tree | 886a38c126ab7c4580087adaa80d2ebaa8ca22ab /src/theory/bv/bv_to_bool.cpp | |
parent | c52adaace77377e14b2eda5b557d97993e2f97dd (diff) |
more work on boolean lifting
Diffstat (limited to 'src/theory/bv/bv_to_bool.cpp')
-rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 135 |
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; +} |