summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/smt/smt_engine.cpp4
-rw-r--r--src/theory/bv/bv_to_bool.cpp91
-rw-r--r--src/theory/bv/bv_to_bool.h13
-rw-r--r--src/theory/term_registration_visitor.h6
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/theory_engine.h2
6 files changed, 79 insertions, 39 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0f79da82a..bc89e8d44 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1925,11 +1925,11 @@ bool SmtEnginePrivate::nonClausalSimplify() {
void SmtEnginePrivate::bvToBool() {
- Trace("simplify") << "SmtEnginePrivate::bvToBool()" << endl;
+ Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
std::vector<Node> new_assertions;
d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions);
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]);
+ d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]);
}
}
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 44c4bd021..8084a7282 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -30,7 +30,7 @@ void BvToBoolVisitor::addToCache(TNode term, Node new_term) {
}
Node BvToBoolVisitor::getCache(TNode term) const {
- if (!hasCache(term)) {
+ if (!hasCache(term) || term.getKind() == kind::CONST_BITVECTOR) {
return term;
}
return d_cache.find(term)->second;
@@ -62,9 +62,11 @@ 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) &&
- node[0].getType().isBitVector() &&
- node[0].getType().getBitVectorSize() == 1;
+ isConvertibleBvTerm(node[0]) &&
+ isConvertibleBvTerm(node[1]);
}
bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) {
@@ -81,6 +83,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) {
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) {
@@ -98,32 +104,51 @@ Node BvToBoolVisitor::convertBvAtom(TNode node) {
Node result;
switch(kind) {
case kind::BITVECTOR_ULT: {
- TNode a = getBoolForBvTerm(node[0]);
- TNode b = getBoolForBvTerm(node[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 = 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: {
- TNode a = getBoolForBvTerm(node[0]);
- TNode b = getBoolForBvTerm(node[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 = 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::EQUAL, a, b);
+ 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: {
- TNode a = getBoolForBvTerm(node[0]);
- TNode b = getBoolForBvTerm(node[1]);
+ 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;
}
@@ -138,16 +163,19 @@ Node BvToBoolVisitor::convertBvTerm(TNode node) {
return getBoolForBvTerm(node);
}
if (node.getKind() == kind::CONST_BITVECTOR) {
- return (node == d_one ? utils::mkTrue() : utils::mkFalse());
+ Node result = node == d_one ? utils::mkTrue() : utils::mkFalse();
+ storeBvToBool(node, result);
+ return result;
}
}
if (kind == kind::ITE) {
- TNode cond = getCache(node[0]);
- TNode true_branch = getBoolForBvTerm(node[1]);
- TNode false_branch = getBoolForBvTerm(node[2]);
+ 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;
}
@@ -175,6 +203,7 @@ Node BvToBoolVisitor::convertBvTerm(TNode node) {
}
Node result = builder;
storeBvToBool(node, result);
+ Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n";
return result;
}
@@ -191,9 +220,8 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) {
Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n";
Assert (!alreadyVisited(current, parent) &&
!hasCache(current));
-
- Node result;
+ Node result;
// make sure that the bv terms we are replacing to not occur in other contexts
check(current, parent);
@@ -217,14 +245,20 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) {
result = builder;
}
}
- Assert (result != Node());
+ Assert (result != Node());
+ Debug("bv-to-bool") << " =>" << result <<"\n";
addToCache(current, result);
}
BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) {
Assert (hasCache(node));
- return getCache(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) {
@@ -242,7 +276,8 @@ bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) {
void BvToBoolPreprocessor::liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- TNodeNodeMap candidates;
+ BvToBoolVisitor bvToBoolVisitor;
+
for (unsigned i = 0; i < assertions.size(); ++i) {
if (matchesBooleanPatern(assertions[i])) {
TNode assertion = assertions[i];
@@ -250,21 +285,21 @@ void BvToBoolPreprocessor::liftBoolToBV(const std::vector<Node>& assertions, std
Assert (bv_var.getKind() == kind::VARIABLE &&
bv_var.getType().isBitVector() &&
bv_var.getType().getBitVectorSize() == 1);
- TNode bool_cond = assertion[1];
+ Node bool_cond = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor, assertion[1]);
Assert (bool_cond.getType().isBoolean());
- if (candidates.find(bv_var) == candidates.end()) {
+ if (!bvToBoolVisitor.hasBoolTerm(bv_var)) {
Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n";
- candidates[bv_var] = bool_cond;
+ bvToBoolVisitor.storeBvToBool(bv_var, bool_cond);
} else {
Debug("bv-to-bool") << "BvToBoolPreprocessor::liftBvToBoolBV multiple def " << bv_var <<"\n";
}
}
}
- BvToBoolVisitor bvToBoolVisitor(candidates);
for (unsigned i = 0; i < assertions.size(); ++i) {
Node new_assertion = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor,
assertions[i]);
- new_assertions.push_back(new_assertion);
+ 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
index 39c6b4251..186f2b317 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -25,11 +25,11 @@ namespace theory {
namespace bv {
typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap;
+typedef __gnu_cxx::hash_map<Node, Node, TNodeHashFunction> NodeNodeMap;
class BvToBoolVisitor {
- TNodeNodeMap d_bvToBoolMap;
- TNodeNodeMap d_cache;
+ NodeNodeMap d_bvToBoolMap;
+ NodeNodeMap d_cache;
Node d_one;
Node d_zero;
@@ -40,14 +40,13 @@ class BvToBoolVisitor {
bool isConvertibleBvTerm(TNode node);
bool isConvertibleBvAtom(TNode node);
Node getBoolForBvTerm(TNode node);
- void storeBvToBool(TNode bv_term, TNode bool_term);
Node convertBvAtom(TNode node);
Node convertBvTerm(TNode node);
void check(TNode current, TNode parent);
public:
typedef Node return_type;
- BvToBoolVisitor(TNodeNodeMap& bvToBool)
- : d_bvToBoolMap(bvToBool),
+ BvToBoolVisitor()
+ : d_bvToBoolMap(),
d_cache(),
d_one(utils::mkConst(BitVector(1, 1u))),
d_zero(utils::mkConst(BitVector(1, 0u)))
@@ -56,6 +55,8 @@ public:
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);
};
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 768508d2c..5f89af9c6 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -95,7 +95,11 @@ public:
* Notifies the engine of all the theories used.
*/
bool done(TNode node);
-
+ ~PreRegisterVisitor() {
+ for (TNodeToTheorySetMap::const_iterator it = d_visited.begin(); it != d_visited.end(); ++it) {
+ std::cout << it->first <<"\n";
+ }
+ }
};
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 22a0b00ed..6c8341345 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1277,7 +1277,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
}
}
-void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node> new_assertions) {
+void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions);
}
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 6d355ccce..c21819ea1 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -753,7 +753,7 @@ private:
theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor;
public:
- void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node> new_assertions);
+ void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
Node ppSimpITE(TNode assertion);
void ppUnconstrainedSimp(std::vector<Node>& assertions);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback