diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 305 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.h | 79 | ||||
-rw-r--r-- | src/theory/bv/options | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 9 |
5 files changed, 395 insertions, 5 deletions
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index a70521791..8651f280b 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -12,6 +12,8 @@ libbv_la_SOURCES = \ type_enumerator.h \ bitblaster.h \ bitblaster.cpp \ + bv_to_bool.h \ + bv_to_bool.cpp \ bv_subtheory.h \ bv_subtheory_core.h \ bv_subtheory_core.cpp \ @@ -36,7 +38,7 @@ libbv_la_SOURCES = \ theory_bv_type_rules.h \ theory_bv_rewriter.h \ theory_bv_rewriter.cpp \ - cd_set_collection.h + cd_set_collection.h EXTRA_DIST = \ kinds diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp new file mode 100644 index 000000000..8084a7282 --- /dev/null +++ b/src/theory/bv/bv_to_bool.cpp @@ -0,0 +1,305 @@ +/********************* */ +/*! \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" +#include "theory/bv/bv_to_bool.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + +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) || term.getKind() == kind::CONST_BITVECTOR) { + 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) {} + +void BvToBoolVisitor::storeBvToBool(TNode bv_term, TNode bool_term) { + Assert (bv_term.getType().isBitVector() && + bv_term.getType().getBitVectorSize() == 1); + Assert (bool_term.getType().isBoolean() && d_bvToBoolMap.find(bv_term) == d_bvToBoolMap.end()); + d_bvToBoolMap[bv_term] = bool_term; +} + +Node BvToBoolVisitor::getBoolForBvTerm(TNode node) { + Assert (d_bvToBoolMap.find(node) != d_bvToBoolMap.end()); + return d_bvToBoolMap[node]; +} + +bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) { + return d_cache.find(current) != d_cache.end(); +} + +bool BvToBoolVisitor::isConvertibleBvAtom(TNode node) { + Kind kind = node.getKind(); + return (kind == kind::BITVECTOR_ULT || + kind == kind::BITVECTOR_ULE || + kind == kind::BITVECTOR_SLT || + kind == kind::BITVECTOR_SLE || + kind == kind::EQUAL) && + isConvertibleBvTerm(node[0]) && + isConvertibleBvTerm(node[1]); +} + +bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { + // we have already converted it and the result is cached + if (d_bvToBoolMap.find(node) != d_bvToBoolMap.end()) { + return true; + } + + Kind kind = node.getKind(); + if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1) + return false; + + if (kind == kind::CONST_BITVECTOR) { + return true; + } + + if (kind == kind::ITE) { + return isConvertibleBvTerm(node[1]) && isConvertibleBvTerm(node[2]); + } + + if (kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR || + kind == kind::BITVECTOR_NOT || kind == kind::BITVECTOR_XOR) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (!isConvertibleBvTerm(node[i])) + return false; + } + return true; + } + return false; +} + +Node BvToBoolVisitor::convertBvAtom(TNode node) { + Assert (node.getType().isBoolean()); + Kind kind = node.getKind(); + Node result; + switch(kind) { + case kind::BITVECTOR_ULT: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_0 = utils::mkNode(kind::IFF, a, utils::mkFalse()); + Node b_eq_1 = utils::mkNode(kind::IFF, b, utils::mkTrue()); + result = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + break; + } + case kind::BITVECTOR_ULE: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_0 = utils::mkNode(kind::IFF, a, utils::mkFalse()); + Node b_eq_1 = utils::mkNode(kind::IFF, b, utils::mkTrue()); + Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + Node a_eq_b = utils::mkNode(kind::IFF, a, b); + result = utils::mkNode(kind::OR, a_lt_b, a_eq_b); + break; + } + case kind::BITVECTOR_SLT: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_1 = utils::mkNode(kind::IFF, a, utils::mkTrue()); + Node b_eq_0 = utils::mkNode(kind::IFF, b, utils::mkFalse()); + result = utils::mkNode(kind::AND, a_eq_1, b_eq_0); + break; + } + case kind::BITVECTOR_SLE: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_1 = utils::mkNode(kind::IFF, a, utils::mkTrue()); + Node b_eq_0 = utils::mkNode(kind::IFF, b, utils::mkFalse()); + Node a_slt_b = utils::mkNode(kind::AND, a_eq_1, b_eq_0); + Node a_eq_b = utils::mkNode(kind::IFF, a, b); + result = utils::mkNode(kind::OR, a_slt_b, a_eq_b); + break; + } + case kind::EQUAL: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + result = utils::mkNode(kind::IFF, a, b); + break; + } + default: + Unhandled(); + } + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvAtom " << node <<" => " << result << "\n"; + Assert (result != Node()); + return result; +} + +Node BvToBoolVisitor::convertBvTerm(TNode node) { + Assert (node.getType().isBitVector() && + node.getType().getBitVectorSize() == 1); + Kind kind = node.getKind(); + + if (node.getNumChildren() == 0) { + if (node.getKind() == kind::VARIABLE) { + return getBoolForBvTerm(node); + } + if (node.getKind() == kind::CONST_BITVECTOR) { + Node result = node == d_one ? utils::mkTrue() : utils::mkFalse(); + storeBvToBool(node, result); + return result; + } + } + + if (kind == kind::ITE) { + Node cond = getCache(node[0]); + Node true_branch = getBoolForBvTerm(node[1]); + Node false_branch = getBoolForBvTerm(node[2]); + Node result = utils::mkNode(kind::ITE, cond, true_branch, false_branch); + storeBvToBool(node, result); + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n"; + return result; + } + + 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; + default: + Unhandled(); + } + + NodeBuilder<> builder(new_kind); + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + builder << getBoolForBvTerm(node[i]); + } + Node result = builder; + storeBvToBool(node, result); + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n"; + return result; +} + +void BvToBoolVisitor::check(TNode current, TNode parent) { + if (d_bvToBoolMap.find(current) != d_bvToBoolMap.end()) { + if (!isConvertibleBvTerm(parent) && !isConvertibleBvAtom(parent)) { + Debug("bv-to-bool") << "BvToBoolVisitor::check " << current << " in non boolean context: \n" + << " " << parent << "\n"; + } + } +} + +void BvToBoolVisitor::visit(TNode current, TNode parent) { + Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; + Assert (!alreadyVisited(current, parent) && + !hasCache(current)); + + Node result; + // make sure that the bv terms we are replacing to not occur in other contexts + check(current, parent); + + if (isConvertibleBvAtom(current)) { + result = convertBvAtom(current); + } else if (isConvertibleBvTerm(current)) { + result = convertBvTerm(current); + } else { + 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]); + Assert (converted.getType() == current[i].getType()); + builder << converted; + } + result = builder; + } + } + Assert (result != Node()); + Debug("bv-to-bool") << " =>" << result <<"\n"; + addToCache(current, result); +} + + +BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) { + Assert (hasCache(node)); + Node result = getCache(node); + return result; +} + +bool BvToBoolVisitor::hasBoolTerm(TNode node) { + return d_bvToBoolMap.find(node) != d_bvToBoolMap.end(); +} + +bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) { + // we are looking for something of the type (= (bvvar 1) (some predicate)) + if (current.getKind() == kind::IFF && + current[0].getKind() == kind::EQUAL && + current[0][0].getType().isBitVector() && + current[0][0].getType().getBitVectorSize() == 1 && + current[0][0].getKind() == kind::VARIABLE && + current[0][1].getKind() == kind::CONST_BITVECTOR) { + return true; + } + return false; +} + + +void BvToBoolPreprocessor::liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { + BvToBoolVisitor bvToBoolVisitor; + + for (unsigned i = 0; i < assertions.size(); ++i) { + if (matchesBooleanPatern(assertions[i])) { + TNode assertion = assertions[i]; + TNode bv_var = assertion[0][0]; + Assert (bv_var.getKind() == kind::VARIABLE && + bv_var.getType().isBitVector() && + bv_var.getType().getBitVectorSize() == 1); + Node bool_cond = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor, assertion[1]); + Assert (bool_cond.getType().isBoolean()); + if (!bvToBoolVisitor.hasBoolTerm(bv_var)) { + Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n"; + bvToBoolVisitor.storeBvToBool(bv_var, bool_cond); + } else { + Debug("bv-to-bool") << "BvToBoolPreprocessor::liftBvToBoolBV multiple def " << bv_var <<"\n"; + } + } + } + + for (unsigned i = 0; i < assertions.size(); ++i) { + Node new_assertion = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor, + assertions[i]); + new_assertions.push_back(new_assertion); + Trace("bv-to-bool") << " " << assertions[i] <<" => " << new_assertions[i] <<"\n"; + } +} diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h new file mode 100644 index 000000000..186f2b317 --- /dev/null +++ b/src/theory/bv/bv_to_bool.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \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" +#include "theory/bv/theory_bv_utils.h" + +#ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H +#define __CVC4__THEORY__BV__BV_TO_BOOL_H + +namespace CVC4 { +namespace theory { +namespace bv { + +typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef __gnu_cxx::hash_map<Node, Node, TNodeHashFunction> NodeNodeMap; + +class BvToBoolVisitor { + NodeNodeMap d_bvToBoolMap; + NodeNodeMap d_cache; + Node d_one; + Node d_zero; + + void addToCache(TNode term, Node new_term); + Node getCache(TNode term) const; + bool hasCache(TNode term) const; + + bool isConvertibleBvTerm(TNode node); + bool isConvertibleBvAtom(TNode node); + Node getBoolForBvTerm(TNode node); + Node convertBvAtom(TNode node); + Node convertBvTerm(TNode node); + void check(TNode current, TNode parent); +public: + typedef Node return_type; + BvToBoolVisitor() + : d_bvToBoolMap(), + d_cache(), + 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); + void storeBvToBool(TNode bv_term, TNode bool_term); + bool hasBoolTerm(TNode node); +}; + + +class BvToBoolPreprocessor { + bool matchesBooleanPatern(TNode node); +public: + BvToBoolPreprocessor() + {} + ~BvToBoolPreprocessor() {} + void liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); +}; + + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + + +#endif /* __CVC4__THEORY__BV__BV_TO_BOOL_H */ 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 433223308..fd2946d24 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -124,6 +124,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; @@ -244,10 +245,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; |