From: Liana Hadarean Date: Wed, 10 Apr 2013 04:03:02 +0000 (-0400) Subject: more work on boolean lifting X-Git-Tag: cvc5-1.0.0~7303 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e4f5359675972341858fe167f454ed5da4d8c115;p=cvc5.git more work on boolean lifting --- 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 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::run(d_visitor, assertion); + return result; +} diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index 6e865658f..ef80930b4 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -15,6 +15,7 @@ **/ #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 @@ -24,22 +25,25 @@ namespace theory { namespace bv { class BvToBoolVisitor { - typedef unsigned return_type; - typedef __gnu_cxx::hash_set TNodeSet; - typedef __gnu_cxx::hash_map TNodeNodeMap; - TNodeNodeMap d_bvToBool; + + typedef __gnu_cxx::hash_set TNodeSet; + typedef __gnu_cxx::hash_map TNodeNodeMap; + TNodeNodeMap d_cache; 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; - + void addToCache(TNode bv_term, Node bool_term); + Node getCache(TNode bv_term) const; + bool hasCache(TNode bv_term) const; + + bool isConvertibleToBool(TNode current); + Node convertToBool(TNode current); public: + typedef Node return_type; BvToBoolVisitor() - : d_substitution(), - d_visited, + : d_cache(), + d_visited(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) {} @@ -47,18 +51,16 @@ public: 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 + : d_visitor() {} ~BvToBoolPreprocessor() {} - Node liftBvToBool(TNode assertion); + Node liftBoolToBV(TNode assertion); };