From: makaimann Date: Tue, 10 Mar 2020 04:13:21 +0000 (-0700) Subject: Enhancement: make the bool-to-bv pass more robust and targeted (#3021) X-Git-Tag: cvc5-1.0.0~3537 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5cbc35e70c2a80094dade1a58605882e3eb1d326;p=cvc5.git Enhancement: make the bool-to-bv pass more robust and targeted (#3021) This pull request is an improvement to the bool-to-bv preprocessing pass. The existing pass is both too weak and too strong, depending on the circumstance. Throughout this description, "lower" refers to lowering a boolean to a bit-vector. --- diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index 30b64fd74..b4d638595 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -19,7 +19,6 @@ #include "base/map_util.h" #include "expr/node.h" -#include "options/bv_options.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -30,7 +29,10 @@ namespace passes { using namespace CVC4::theory; BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics(){}; + : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics() +{ + d_boolToBVMode = options::boolToBitvector(); +}; PreprocessingPassResult BoolToBV::applyInternal( AssertionPipeline* assertionsToPreprocess) @@ -38,31 +40,73 @@ PreprocessingPassResult BoolToBV::applyInternal( NodeManager::currentResourceManager()->spendResource( ResourceManager::Resource::PreprocessStep); - unsigned size = assertionsToPreprocess->size(); - for (unsigned i = 0; i < size; ++i) + size_t size = assertionsToPreprocess->size(); + + if (d_boolToBVMode == options::BoolToBVMode::ALL) + { + for (size_t i = 0; i < size; ++i) + { + Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true); + assertionsToPreprocess->replace(i, Rewriter::rewrite(newAssertion)); + } + } + else { - assertionsToPreprocess->replace( - i, Rewriter::rewrite(lowerAssertion((*assertionsToPreprocess)[i]))); + Assert(d_boolToBVMode == options::BoolToBVMode::ITE); + for (size_t i = 0; i < size; ++i) + { + assertionsToPreprocess->replace( + i, Rewriter::rewrite(lowerIte((*assertionsToPreprocess)[i]))); + } } return PreprocessingPassResult::NO_CONFLICT; } +void BoolToBV::updateCache(TNode n, TNode rebuilt) +{ + // check more likely case first + if ((n.getKind() != kind::ITE) || !n[1].getType().isBitVector()) + { + d_lowerCache[n] = rebuilt; + } + else + { + d_iteBVLowerCache[n] = rebuilt; + } +} + Node BoolToBV::fromCache(TNode n) const { - if (d_lowerCache.find(n) != d_lowerCache.end()) + // check more likely case first + if (n.getKind() != kind::ITE) { - return d_lowerCache.find(n)->second; + if (d_lowerCache.find(n) != d_lowerCache.end()) + { + return d_lowerCache.at(n); + } + } + else + { + if (d_iteBVLowerCache.find(n) != d_iteBVLowerCache.end()) + { + return d_iteBVLowerCache.at(n); + } } return n; } +inline bool BoolToBV::inCache(const Node& n) const +{ + return (ContainsKey(d_lowerCache, n) || ContainsKey(d_iteBVLowerCache, n)); +} + bool BoolToBV::needToRebuild(TNode n) const { // check if any children were rebuilt for (const Node& nn : n) { - if (ContainsKey(d_lowerCache, nn)) + if (inCache(nn)) { return true; } @@ -70,134 +114,82 @@ bool BoolToBV::needToRebuild(TNode n) const return false; } -Node BoolToBV::lowerAssertion(const TNode& a) +Node BoolToBV::lowerAssertion(const TNode& assertion, bool allowIteIntroduction) { - bool optionITE = options::boolToBitvector() == options::BoolToBVMode::ITE; - NodeManager* nm = NodeManager::currentNM(); - std::vector visit; - visit.push_back(a); + // first try to lower all the children + for (const Node& c : assertion) + { + lowerNode(c, allowIteIntroduction); + } + + // now try lowering the assertion, but don't force it with an ITE (even in mode all) + lowerNode(assertion, false); + Node newAssertion = fromCache(assertion); + TypeNode newAssertionType = newAssertion.getType(); + if (newAssertionType.isBitVector()) + { + Assert(newAssertionType.getBitVectorSize() == 1); + newAssertion = NodeManager::currentNM()->mkNode( + kind::EQUAL, newAssertion, bv::utils::mkOne(1)); + newAssertionType = newAssertion.getType(); + } + Assert(newAssertionType.isBoolean()); + return newAssertion; +} + +Node BoolToBV::lowerNode(const TNode& node, bool allowIteIntroduction) +{ + std::vector to_visit; + to_visit.push_back(node); std::unordered_set visited; - // for ite mode, keeps track of whether you're in an ite condition - // for all mode, unused - std::unordered_set ite_cond; - while (!visit.empty()) + while (!to_visit.empty()) { - TNode n = visit.back(); - visit.pop_back(); + TNode n = to_visit.back(); + to_visit.pop_back(); - int numChildren = n.getNumChildren(); - Kind k = n.getKind(); - Debug("bool-to-bv") << "BoolToBV::lowerAssertion Post-traversal with " << n - << " and visited = " << ContainsKey(visited, n) + Debug("bool-to-bv") << "BoolToBV::lowerNode: Post-order traversal with " + << n << " and visited = " << ContainsKey(visited, n) << std::endl; // Mark as visited - /* Optimization: if it's a leaf, don't need to wait to do the work */ - if (!ContainsKey(visited, n) && (numChildren > 0)) + if (ContainsKey(visited, n)) + { + visit(n, allowIteIntroduction); + } + else { visited.insert(n); - visit.push_back(n); + to_visit.push_back(n); // insert children in reverse order so that they're processed in order - // important for rewriting which sorts by node id - for (int i = numChildren - 1; i >= 0; --i) + // important for rewriting which sorts by node id + // NOTE: size_t is unsigned, so using underflow for termination condition + size_t numChildren = n.getNumChildren(); + for (size_t i = numChildren - 1; i < numChildren; --i) { - visit.push_back(n[i]); - } - - if (optionITE) - { - // check for ite-conditions - if (k == kind::ITE) - { - ite_cond.insert(n[0]); - } - else if (ContainsKey(ite_cond, n)) - { - // being part of an ite condition is inherited from the parent - ite_cond.insert(n.begin(), n.end()); - } + to_visit.push_back(n[i]); } } - /* Optimization for ite mode */ - else if (optionITE && !ContainsKey(ite_cond, n) && !needToRebuild(n)) - { - Debug("bool-to-bv") - << "BoolToBV::lowerAssertion Skipping because don't need to rebuild: " - << n << std::endl; - // in ite mode, if you've already visited the node but it's not - // in an ite condition and doesn't need to be rebuilt, then - // don't need to do anything - continue; - } - else - { - lowerNode(n); - } } - if (fromCache(a).getType().isBitVector()) - { - return nm->mkNode(kind::EQUAL, fromCache(a), bv::utils::mkOne(1)); - } - else - { - Assert(a == fromCache(a)); - return a; - } + return fromCache(node); } -void BoolToBV::lowerNode(const TNode& n) +void BoolToBV::visit(const TNode& n, bool allowIteIntroduction) { - NodeManager* nm = NodeManager::currentNM(); Kind k = n.getKind(); - bool all_bv = true; - // check if it was able to convert all children to bitvectors - for (const Node& nn : n) + // easy case -- just replace boolean constant + if (k == kind::CONST_BOOLEAN) { - all_bv = all_bv && fromCache(nn).getType().isBitVector(); - if (!all_bv) - { - break; - } - } - - if (!all_bv || (n.getNumChildren() == 0)) - { - if ((options::boolToBitvector() == options::BoolToBVMode::ALL) - && n.getType().isBoolean()) - { - if (k == kind::CONST_BOOLEAN) - { - d_lowerCache[n] = (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1) - : bv::utils::mkZero(1); - } - else - { - d_lowerCache[n] = - nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)); - } - - Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n" - << fromCache(n) << std::endl; - ++(d_statistics.d_numTermsForcedLowered); - return; - } - else - { - // invariant - // either one of the children is not a bit-vector or bool - // i.e. something that can't be 'forced' to a bitvector - // or it's in 'ite' mode which will give up on bools that - // can't be converted easily - - Debug("bool-to-bv") << "BoolToBV::lowerNode skipping: " << n << std::endl; - return; - } + updateCache(n, + (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1) + : bv::utils::mkZero(1)); + return; } + NodeManager* nm = NodeManager::currentNM(); Kind new_kind = k; switch (k) { @@ -221,9 +213,154 @@ void BoolToBV::lowerNode(const TNode& n) default: break; } + // check if it's safe to lower or rebuild the node + // Note: might have to rebuild to keep changes to children, even if this node + // isn't being lowered + + // it's safe to lower if all the children are bit-vectors + bool safe_to_lower = + (new_kind != k); // don't need to lower at all if kind hasn't changed + + // it's safe to rebuild if rebuilding doesn't change any of the types of the + // children + bool safe_to_rebuild = true; + + for (const Node& nn : n) + { + safe_to_lower = safe_to_lower && fromCache(nn).getType().isBitVector(); + safe_to_rebuild = safe_to_rebuild && (fromCache(nn).getType() == nn.getType()); + + // if it's already not safe to do either, stop checking + if (!safe_to_lower && !safe_to_rebuild) + { + break; + } + } + + Debug("bool-to-bv") << "safe_to_lower = " << safe_to_lower + << ", safe_to_rebuild = " << safe_to_rebuild << std::endl; + + if (new_kind != k && safe_to_lower) + { + // lower to BV + rebuildNode(n, new_kind); + return; + } + else if (new_kind != k && allowIteIntroduction && fromCache(n).getType().isBoolean()) + { + // lower to BV using an ITE + + if (safe_to_rebuild && needToRebuild(n)) + { + // need to rebuild to keep changes made to descendants + rebuildNode(n, k); + } + + updateCache(n, + nm->mkNode(kind::ITE, + fromCache(n), + bv::utils::mkOne(1), + bv::utils::mkZero(1))); + Debug("bool-to-bv") << "BoolToBV::visit forcing " << n + << " =>\n" + << fromCache(n) << std::endl; + ++(d_statistics.d_numIntroducedItes); + return; + } + else if (safe_to_rebuild && needToRebuild(n)) + { + // rebuild to incorporate changes to children + Assert(k == new_kind); + rebuildNode(n, k); + } + else if (allowIteIntroduction && fromCache(n).getType().isBoolean()) + { + // force booleans (which haven't already been converted) to bit-vector + // needed to maintain the invariant that all boolean children + // have been converted (even constants and variables) when forcing + // with ITE introductions + updateCache( + n, nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1))); + Debug("bool-to-bv") << "BoolToBV::visit forcing " << n + << " =>\n" + << fromCache(n) << std::endl; + ++(d_statistics.d_numIntroducedItes); + } + else + { + // do nothing + Debug("bool-to-bv") << "BoolToBV::visit skipping: " << n + << std::endl; + } +} + +Node BoolToBV::lowerIte(const TNode& node) +{ + std::vector visit; + visit.push_back(node); + std::unordered_set visited; + + while (!visit.empty()) + { + TNode n = visit.back(); + visit.pop_back(); + + Debug("bool-to-bv") << "BoolToBV::lowerIte: Post-order traversal with " << n + << " and visited = " << ContainsKey(visited, n) + << std::endl; + + // Look for ITEs and mark visited + if (!ContainsKey(visited, n)) + { + if ((n.getKind() == kind::ITE) && n[1].getType().isBitVector()) + { + Debug("bool-to-bv") << "BoolToBV::lowerIte: adding " << n[0] + << " to set of ite conditions" << std::endl; + // don't force in this case -- forcing only introduces more ITEs + Node loweredNode = lowerNode(n, false); + // some of the lowered nodes might appear elsewhere but not in an ITE + // reset the cache to prevent lowering them + // the bit-vector ITEs are still tracked in d_iteBVLowerCache though + d_lowerCache.clear(); + } + else + { + visit.push_back(n); + visited.insert(n); + // insert in reverse order so that they're processed in order + for (int i = n.getNumChildren() - 1; i >= 0; --i) + { + visit.push_back(n[i]); + } + } + } + else if (needToRebuild(n)) + { + // Note: it's always safe to rebuild here, because we've only lowered + // ITEs of type bit-vector to BITVECTOR_ITE + rebuildNode(n, n.getKind()); + } + else + { + Debug("bool-to-bv") + << "BoolToBV::lowerIte Skipping because don't need to rebuild: " << n + << std::endl; + } + } + return fromCache(node); +} + +void BoolToBV::rebuildNode(const TNode& n, Kind new_kind) +{ + Kind k = n.getKind(); + NodeManager* nm = NodeManager::currentNM(); NodeBuilder<> builder(new_kind); - if ((options::boolToBitvector() == options::BoolToBVMode::ALL) - && (new_kind != k)) + + Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n + << " and new_kind = " << kindToString(new_kind) + << std::endl; + + if ((d_boolToBVMode == options::BoolToBVMode::ALL) && (new_kind != k)) { ++(d_statistics.d_numTermsLowered); } @@ -234,7 +371,7 @@ void BoolToBV::lowerNode(const TNode& n) } // special case IMPLIES because needs to be rewritten - if (k == kind::IMPLIES) + if ((k == kind::IMPLIES) && (new_kind != k)) { builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0])); builder << fromCache(n[1]); @@ -247,16 +384,16 @@ void BoolToBV::lowerNode(const TNode& n) } } - Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n" + Debug("bool-to-bv") << "BoolToBV::rebuildNode " << n << " =>\n" << builder << std::endl; - d_lowerCache[n] = builder.constructNode(); + updateCache(n, builder.constructNode()); } BoolToBV::Statistics::Statistics() : d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0), d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0), - d_numTermsForcedLowered( + d_numIntroducedItes( "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0) { smtStatisticsRegistry()->registerStat(&d_numIteToBvite); @@ -266,7 +403,7 @@ BoolToBV::Statistics::Statistics() // because it might discard rebuilt nodes if it fails to // convert a bool to width-one bit-vector (never forces) smtStatisticsRegistry()->registerStat(&d_numTermsLowered); - smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered); + smtStatisticsRegistry()->registerStat(&d_numIntroducedItes); } } @@ -276,7 +413,7 @@ BoolToBV::Statistics::~Statistics() if (options::boolToBitvector() == options::BoolToBVMode::ALL) { smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered); - smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered); + smtStatisticsRegistry()->unregisterStat(&d_numIntroducedItes); } } diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index 11cb551fa..6e6d368eb 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -18,6 +18,7 @@ #ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H #define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H +#include "options/bv_options.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" #include "theory/bv/theory_bv_utils.h" @@ -41,29 +42,82 @@ class BoolToBV : public PreprocessingPass { IntStat d_numIteToBvite; IntStat d_numTermsLowered; - IntStat d_numTermsForcedLowered; + IntStat d_numIntroducedItes; Statistics(); ~Statistics(); }; - /* Takes an assertion and tries to create more bit-vector structure */ - Node lowerAssertion(const TNode& a); + /** Takes an assertion and attempts to create more bit-vector structure + by replacing boolean operators with bit-vector operators. - /* Tries to lower one node to a width-one bit-vector */ - void lowerNode(const TNode& n); + It passes the allowIteIntroduction argument down to lowerNode, however it + never allows ite introduction in the top-level assertion. There's no point + forcing the assertion to be a bit-vector when it will just be converted + back into a boolean. + */ + Node lowerAssertion(const TNode& node, bool allowIteIntroduction = false); + + /** Traverses subterms to turn booleans into bit-vectors using visit + * Passes the allowIteIntroduction argument to visit + * Returns the lowered node + */ + Node lowerNode(const TNode& node, bool allowIteIntroduction = false); + + /** Tries to lower one node to a width-one bit-vector + * Caches the result if successful + * + * allowIteIntroduction = true causes booleans to be converted to bit-vectors + * using an ITE this is only used by mode ALL currently, but could + * conceivably be used in new modes. + */ + void visit(const TNode& n, bool allowIteIntroduction = false); + + /* Traverses formula looking for ITEs to lower to BITVECTOR_ITE using + * lowerNode*/ + Node lowerIte(const TNode& node); + + /** Rebuilds node using the provided kind + * Note: The provided kind is not necessarily different from the + * existing one, but still might need to be rebuilt because + * of subterms + */ + void rebuildNode(const TNode& n, Kind new_kind); + + /** Updates the cache, the cache is actually supported by two maps + one for ITEs and one for everything else + + This is necessary so that when in ITE mode, the regular cache + can be cleared to prevent lowering boolean operators that are + not in an ITE + */ + void updateCache(TNode n, TNode rebuilt); /* Returns cached node if it exists, otherwise returns the node */ Node fromCache(TNode n) const; - /** Checks if any of the nodes children were rebuilt, + /* Checks both caches for membership */ + bool inCache(const Node& n) const; + + /** Checks if any of the node's children were rebuilt, * in which case n needs to be rebuilt as well */ bool needToRebuild(TNode n) const; Statistics d_statistics; - /* Keeps track of lowered nodes */ + /** Keeps track of lowered ITEs + Note: it only keeps mappings for ITEs of type bit-vector. + Other ITEs will be in the d_lowerCache + */ + std::unordered_map d_iteBVLowerCache; + + /** Keeps track of other lowered nodes + -- will be cleared periodically in ITE mode + */ std::unordered_map d_lowerCache; + + /** Stores the bool-to-bv mode option */ + options::BoolToBVMode d_boolToBVMode; }; // class BoolToBV } // namespace passes diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 046b073ff..e0e8b236e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -189,6 +189,9 @@ set(regress_0_tests regress0/bv/ackermann8.smt2 regress0/bv/bool-model.smt2 regress0/bv/bool-to-bv-all.smt2 + regress0/bv/bool-to-bv-all-array-bool.smt2 + regress0/bv/bool-to-bv-ite-array-bool.smt2 + regress0/bv/bool-to-bv-all-test.smt2 regress0/bv/bool-to-bv-ite.smt2 regress0/bv/bug260a.smtv1.smt2 regress0/bv/bug260b.smtv1.smt2 diff --git a/test/regress/regress0/bv/bool-to-bv-all-array-bool.smt2 b/test/regress/regress0/bv/bool-to-bv-all-array-bool.smt2 new file mode 100644 index 000000000..2a0c9d7b1 --- /dev/null +++ b/test/regress/regress0/bv/bool-to-bv-all-array-bool.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --bool-to-bv=all --simplification=none +; EXPECT: sat +; checks that bool-to-bv pass handles arrays over booleans correctly +(set-logic QF_ABV) + +(declare-const A (Array Bool Bool)) +(declare-const B (Array Bool Bool)) +(declare-const b1 Bool) +(declare-const b2 Bool) +(declare-const b3 Bool) +(declare-const b4 Bool) + +(assert (= A (store B b1 b2))) +(assert (= b3 (select A (select B b2)))) +(assert (=> b1 b2)) +(assert (not (and b2 (ite b3 b1 b2)))) +(assert (=> b3 b1)) +(assert (= b4 (select B b2))) +(assert (xor b4 b2)) + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/bv/bool-to-bv-all-test.smt2 b/test/regress/regress0/bv/bool-to-bv-all-test.smt2 new file mode 100644 index 000000000..d1ebf24ff --- /dev/null +++ b/test/regress/regress0/bv/bool-to-bv-all-test.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --bool-to-bv=all +; EXPECT: sat +; checks for a bug that can occur when forcing booleans to +; bit-vectors when other sorts are present +(set-logic QF_ABV) + +(declare-const A (Array (_ BitVec 32) (_ BitVec 32))) +(declare-const B (Array (_ BitVec 32) (_ BitVec 32))) +(declare-const sel Bool) +(declare-const idx (_ BitVec 32)) +(declare-const val (_ BitVec 32)) + +(assert (=> sel (bvult idx (_ bv15 32)))) +(assert (=> (= A (store B idx val)) sel)) +(assert (=> (= A (store B idx val)) (not (= idx val)))) +(assert (not (= A B))) +(assert (=> (not (= A (store B idx val))) (not sel))) +(assert (=> (not (= A (store B idx val))) (bvugt idx val))) + +(check-sat) diff --git a/test/regress/regress0/bv/bool-to-bv-ite-array-bool.smt2 b/test/regress/regress0/bv/bool-to-bv-ite-array-bool.smt2 new file mode 100644 index 000000000..2a0c9d7b1 --- /dev/null +++ b/test/regress/regress0/bv/bool-to-bv-ite-array-bool.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --bool-to-bv=all --simplification=none +; EXPECT: sat +; checks that bool-to-bv pass handles arrays over booleans correctly +(set-logic QF_ABV) + +(declare-const A (Array Bool Bool)) +(declare-const B (Array Bool Bool)) +(declare-const b1 Bool) +(declare-const b2 Bool) +(declare-const b3 Bool) +(declare-const b4 Bool) + +(assert (= A (store B b1 b2))) +(assert (= b3 (select A (select B b2)))) +(assert (=> b1 b2)) +(assert (not (and b2 (ite b3 b1 b2)))) +(assert (=> b3 b1)) +(assert (= b4 (select B b2))) +(assert (xor b4 b2)) + +(check-sat) \ No newline at end of file