From: lianah Date: Tue, 16 Apr 2013 14:57:04 +0000 (-0400) Subject: uncompiling new bv to bool lifting X-Git-Tag: cvc5-1.0.0~7301 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=95a876e4931b94ab97ff40988ce23e34a046387d;p=cvc5.git uncompiling new bv to bool lifting --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f3d5d446e..0f79da82a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1926,9 +1926,10 @@ bool SmtEnginePrivate::nonClausalSimplify() { void SmtEnginePrivate::bvToBool() { Trace("simplify") << "SmtEnginePrivate::bvToBool()" << endl; - + std::vector new_assertions; + d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck[i]); + d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); } } @@ -2481,16 +2482,6 @@ bool SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - // Lift bit-vectors of size 1 to bool - if(options::bvToBool()) { - Chat() << "...doing bvToBool..." << endl; - bvToBool(); - } - - Trace("smt") << "POST bvToBool" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { Chat() << "...doing another round of nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -2789,6 +2780,17 @@ void SmtEnginePrivate::processAssertions() { } dumpAssertions("post-static-learning", d_assertionsToCheck); + // Lift bit-vectors of size 1 to bool + if(options::bvToBool()) { + Chat() << "...doing bvToBool..." << endl; + bvToBool(); + } + + Trace("smt") << "POST bvToBool" << endl; + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + + dumpAssertions("pre-ite-removal", d_assertionsToCheck); { Chat() << "removing term ITEs..." << endl; diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 5ab7cf144..7d3f58c8e 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -23,22 +23,6 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; -void BvToBoolVisitor::storeBvToBool(TNode bv_term, Node bool_term) { - Assert (!hasBoolTerm(bv_term)); - Assert (bool_term.getType().isBoolean()); - d_bvToBoolTerm[bv_term] = bool_term; -} - -Node BvToBoolVisitor::getBoolTerm(TNode bv_term) const { - Assert(hasBoolTerm(bv_term)); - return d_bvToBoolTerm.find(bv_term)->second; -} - -bool BvToBoolVisitor::hasBoolTerm(TNode bv_term) const { - Assert (bv_term.getType().isBitVector()); - return d_bvToBoolTerm.find(bv_term) != d_bvToBoolTerm.end(); -} - void BvToBoolVisitor::addToCache(TNode term, Node new_term) { Assert (new_term != Node()); Assert (!hasCache(term)); @@ -56,130 +40,167 @@ 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_visited.find(current) != d_visited.end(); + 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::EQUAL) && + node[0].getType().isBitVector() && + node[0].getType().getBitVectorSize() == 1; } -bool BvToBoolVisitor::isConvertibleToBool(TNode current) { - 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_ULT || - kind == kind::BITVECTOR_ULE || - kind == kind::EQUAL) { - // 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])) +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::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; } - if (kind == kind::ITE && - type.isBitVector()) { - 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(); - - 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); - 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 BvToBoolVisitor::convertBvAtom(TNode node) { + Assert (node.getType().isBoolean()); + Kind kind = node.getKind(); + 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_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); - Node a_eq_b = utils::mkNode(kind::EQUAL, a, b); - 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(); + 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_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + Node a_eq_b = utils::mkNode(kind::EQUAL, a, b); + result = utils::mkNode(kind::OR, a_lt_b, a_eq_b); + break; + } + case kind::EQUAL: { + TNode a = getBoolForBvTerm(node[0]); + TNode b = getBoolForBvTerm(node[1]); + result = utils::mkNode(kind::IFF, a, b); + break; + } + default: + Unhandled(); + } + 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); } - for (unsigned i = 0; i < current.getNumChildren(); ++i) { - builder << getBoolTerm(current[i]); + if (node.getKind() == kind::CONST_BITVECTOR) { + return (node == d_one ? utils::mkTrue() : utils::mkFalse()); } - new_current = builder; } - Debug("bv-to-bool") << "=> " << new_current << "\n"; - if (current.getType().isBitVector()) { - storeBvToBool(current, new_current); - } else { - addToCache(current, new_current); + if (kind == kind::ITE) { + TNode cond = getCache(node[0]); + TNode true_branch = getBoolForBvTerm(node[1]); + TNode false_branch = getBoolForBvTerm(node[2]); + Node result = utils::mkNode(kind::ITE, cond, true_branch, false_branch); + storeBvToBool(node, result); + 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); + 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"; + } } - 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); + Assert (!alreadyVisited(current, parent) && + !hasCache(current)); + + Node result; - Node result; - // if it has more than one child - if (isConvertibleToBool(current)) { - result = convertToBool(current); + // 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; @@ -190,24 +211,60 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { } 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]; - } + Assert (converted.getType() == current[i].getType()); + builder << converted; } result = builder; } - addToCache(current, result); } + Assert (result != Node()); + addToCache(current, result); } + 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; +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& assertions, std::vector& new_assertions) { + TNodeNodeMap candidates; + 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_bar.getType().getBitVectorSize() == 1); + TNode bool_cond = assertion[1]; + Assert (bool_cond.getType().isBoolean()); + if (candidates.find(bv_var) == candidates.end()) { + Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n"; + candidates[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::run(bvToBoolVisitor, + assertions[i]); + new_assertions.push_back(new_assertion); + } } diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index d5673a295..9b1534b41 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -24,33 +24,31 @@ namespace CVC4 { namespace theory { namespace bv { -class BvToBoolVisitor { +typedef __gnu_cxx::hash_set TNodeSet; +typedef __gnu_cxx::hash_map TNodeNodeMap; - typedef __gnu_cxx::hash_set TNodeSet; - typedef __gnu_cxx::hash_map TNodeNodeMap; +class BvToBoolVisitor { + TNodeNodeMap d_bvToBoolMap; TNodeNodeMap d_cache; - TNodeNodeMap d_bvToBoolTerm; - TNodeSet d_visited; Node d_one; Node d_zero; - 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); + 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() - : d_cache(), - d_bvToBoolTerm(), - d_visited(), + BvToBoolVisitor(TNodeNodeMap& bvToBool) + : d_bvToBoolMap(bvToBool), + d_cache(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) {} @@ -60,14 +58,14 @@ public: return_type done(TNode node); }; + class BvToBoolPreprocessor { - BvToBoolVisitor d_visitor; + bool matchesBooleanPatern(TNode node); public: BvToBoolPreprocessor() - : d_visitor() {} ~BvToBoolPreprocessor() {} - Node liftBoolToBV(TNode assertion); + void liftBoolToBV(const std::vector& assertions, std::vector& new_assertions); }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6f965879d..8c430d6d4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1277,10 +1277,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } -Node TheoryEngine::ppBvToBool(TNode assertion) { - Node result = d_bvToBoolPreprocessor.liftBoolToBV(assertion); - result = Rewriter::rewrite(result); - return result; +void TheoryEngine::ppBvToBool(const std::vector& assertions, std::vector new_assertions) { + d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions); } Node TheoryEngine::ppSimpITE(TNode assertion) diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 324b952b0..d581aeda2 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -753,7 +753,7 @@ private: theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: - Node ppBvToBool(TNode assertion); + void ppBvToBool(const std::vector& assertions, std::vector new_assertions); Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector& assertions);