diff options
author | lianah <lianahady@gmail.com> | 2013-04-12 16:15:30 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
commit | 6a86536bd25fc7ffa305f25990cf37b8c6566c52 (patch) | |
tree | 197b931f8f391a21eebbf097fd0f4b5adeb53c09 /src/theory/bv | |
parent | e4f5359675972341858fe167f454ed5da4d8c115 (diff) |
finished implementing bv to bool lifting and added --bv-to-bool option
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 179 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.h | 13 | ||||
-rw-r--r-- | src/theory/bv/options | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 9 |
4 files changed, 132 insertions, 72 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; |