From: Mathias Preiner Date: Sat, 11 Sep 2021 03:23:47 +0000 (-0700) Subject: bv: Move IsPowerOfTwo rule to preprocessing pass and use EnvObj. (#7179) X-Git-Tag: cvc5-1.0.0~1232 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87453ed0f6fd123a54c7f17b958b2c2c9ca9d47b;p=cvc5.git bv: Move IsPowerOfTwo rule to preprocessing pass and use EnvObj. (#7179) IsPowerOfTwo rule is specific to the BvIntroPow2 preprocessing pass and should not be a general bit-vector rewrite rule. --- diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index ff0657dcd..b334a550d 100644 --- a/src/preprocessing/passes/bv_intro_pow2.cpp +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -23,8 +23,7 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "theory/bv/theory_bv_rewrite_rules_simplification.h" -#include "theory/rewriter.h" +#include "theory/bv/theory_bv_utils.h" namespace cvc5 { namespace preprocessing { @@ -33,11 +32,75 @@ namespace passes { using NodeMap = std::unordered_map; using namespace cvc5::theory; -namespace { +BvIntroPow2::BvIntroPow2(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "bv-intro-pow2"){}; + +PreprocessingPassResult BvIntroPow2::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + std::unordered_map cache; + for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + Node cur = (*assertionsToPreprocess)[i]; + Node res = pow2Rewrite(cur, cache); + if (res != cur) + { + res = rewrite(res); + assertionsToPreprocess->replace(i, res); + } + } + return PreprocessingPassResult::NO_CONFLICT; +} -Node pow2Rewrite(Node node, NodeMap& cache) +bool BvIntroPow2::isPowerOfTwo(TNode node) { - NodeMap::const_iterator ci = cache.find(node); + if (node.getKind() != kind::EQUAL) + { + return false; + } + if (node[0].getKind() != kind::BITVECTOR_AND + && node[1].getKind() != kind::BITVECTOR_AND) + { + return false; + } + if (!bv::utils::isZero(node[0]) && !bv::utils::isZero(node[1])) + { + return false; + } + + TNode t = !bv::utils::isZero(node[0]) ? node[0] : node[1]; + if (t.getNumChildren() != 2) return false; + TNode a = t[0]; + TNode b = t[1]; + unsigned size = bv::utils::getSize(t); + if (size < 2) return false; + Node diff = + rewrite(NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, a, b)); + return (diff.isConst() + && (diff == bv::utils::mkConst(size, 1u) + || diff == bv::utils::mkOnes(size))); +} + +Node BvIntroPow2::rewritePowerOfTwo(TNode node) +{ + NodeManager* nm = NodeManager::currentNM(); + TNode term = bv::utils::isZero(node[0]) ? node[1] : node[0]; + TNode a = term[0]; + TNode b = term[1]; + unsigned size = bv::utils::getSize(term); + Node diff = rewrite(nm->mkNode(kind::BITVECTOR_SUB, a, b)); + Assert(diff.isConst()); + TNode x = diff == bv::utils::mkConst(size, 1u) ? a : b; + Node one = bv::utils::mkConst(size, 1u); + Node sk = bv::utils::mkVar(size); + Node sh = nm->mkNode(kind::BITVECTOR_SHL, one, sk); + Node x_eq_sh = nm->mkNode(kind::EQUAL, x, sh); + return x_eq_sh; +} + +Node BvIntroPow2::pow2Rewrite(Node node, std::unordered_map& cache) +{ + const auto& ci = cache.find(node); if (ci != cache.end()) { Node incache = (*ci).second; @@ -66,10 +129,9 @@ Node pow2Rewrite(Node node, NodeMap& cache) break; case kind::EQUAL: - if (node[0].getType().isBitVector() - && theory::bv::RewriteRule::applies(node)) + if (node[0].getType().isBitVector() && isPowerOfTwo(node)) { - res = theory::bv::RewriteRule::run(node); + res = rewritePowerOfTwo(node); } break; default: break; @@ -79,28 +141,6 @@ Node pow2Rewrite(Node node, NodeMap& cache) return res.isNull() ? node : res; } -} // namespace - -BvIntroPow2::BvIntroPow2(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "bv-intro-pow2"){}; - -PreprocessingPassResult BvIntroPow2::applyInternal( - AssertionPipeline* assertionsToPreprocess) -{ - std::unordered_map cache; - for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) - { - Node cur = (*assertionsToPreprocess)[i]; - Node res = pow2Rewrite(cur, cache); - if (res != cur) - { - res = rewrite(res); - assertionsToPreprocess->replace(i, res); - } - } - return PreprocessingPassResult::NO_CONFLICT; -} - } // namespace passes } // namespace preprocessing diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index 0ec0f4df6..0f39474da 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -36,6 +36,23 @@ class BvIntroPow2 : public PreprocessingPass protected: PreprocessingPassResult applyInternal( AssertionPipeline* assertionsToPreprocess) override; + + private: + /** Checks whether PowerOfTwo rewrite applies. */ + bool isPowerOfTwo(TNode node); + /** + * Applies PowerOfTwo rewrite. + * + * x & (x-1) = 0 => x = 1 << sk + * + * where sk is a fresh Skolem. + * + * WARNING: this is an **EQUISATISFIABLE** transformation! + * Only to be called on top level assertions. + */ + Node rewritePowerOfTwo(TNode node); + /** Does the traversal of assertions and applies rweritePowerOfTwo. */ + Node pow2Rewrite(Node node, std::unordered_map& cache); }; } // namespace passes diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index fb80d43d0..7553bcbb6 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -203,7 +203,6 @@ enum RewriteRuleId BBAddNeg, UltAddOne, ConcatToMult, - IsPowerOfTwo, MultSltMult, BitOfConst, }; @@ -370,7 +369,6 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case MultDistrib: out << "MultDistrib"; return out; case UltAddOne: out << "UltAddOne"; return out; case ConcatToMult: out << "ConcatToMult"; return out; - case IsPowerOfTwo: out << "IsPowerOfTwo"; return out; case MultSltMult: out << "MultSltMult"; return out; case NormalizeEqAddNeg: out << "NormalizeEqAddNeg"; return out; case BitOfConst: out << "BitOfConst"; return out; @@ -589,7 +587,6 @@ struct AllRewriteRules { RewriteRule rule118; RewriteRule rule119; RewriteRule rule120; - RewriteRule rule121; RewriteRule rule122; RewriteRule rule123; RewriteRule rule124; diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 6d2ed4477..330bdc85b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -23,7 +23,6 @@ #include "options/bv_options.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/rewriter.h" #include "util/bitvector.h" namespace cvc5 { @@ -2059,58 +2058,6 @@ inline Node RewriteRule::apply(TNode node) /* -------------------------------------------------------------------------- */ -/** - * x ^(x-1) = 0 => 1 << sk - * WARNING: this is an **EQUISATISFIABLE** transformation! - * Only to be called on top level assertions. - * - * @param node - * - * @return - */ -template<> inline -bool RewriteRule::applies(TNode node) { - if (node.getKind()!= kind::EQUAL) return false; - if (node[0].getKind() != kind::BITVECTOR_AND && - node[1].getKind() != kind::BITVECTOR_AND) - return false; - if (!utils::isZero(node[0]) && - !utils::isZero(node[1])) - return false; - - TNode t = !utils::isZero(node[0])? node[0]: node[1]; - if (t.getNumChildren() != 2) return false; - TNode a = t[0]; - TNode b = t[1]; - unsigned size = utils::getSize(t); - if(size < 2) return false; - Node diff = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, a, b)); - return (diff.isConst() && (diff == utils::mkConst(size, 1u) || diff == utils::mkOnes(size))); -} - -template <> -inline Node RewriteRule::apply(TNode node) -{ - Debug("bv-rewrite") << "RewriteRule(" << node << ")" - << std::endl; - NodeManager *nm = NodeManager::currentNM(); - TNode term = utils::isZero(node[0]) ? node[1] : node[0]; - TNode a = term[0]; - TNode b = term[1]; - unsigned size = utils::getSize(term); - Node diff = Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, a, b)); - Assert(diff.isConst()); - TNode x = diff == utils::mkConst(size, 1u) ? a : b; - Node one = utils::mkConst(size, 1u); - Node sk = utils::mkVar(size); - Node sh = nm->mkNode(kind::BITVECTOR_SHL, one, sk); - Node x_eq_sh = nm->mkNode(kind::EQUAL, x, sh); - return x_eq_sh; -} - -/* -------------------------------------------------------------------------- */ - /** * Rewrite * sign_extend(x+t,n) * sign_extend(a,m) < sign_extend(x,n) * sign_extend(a,m) diff --git a/test/regress/regress0/bv/test-bv_intro_pow2.smt2 b/test/regress/regress0/bv/test-bv_intro_pow2.smt2 index 465937b28..e89dd4c50 100644 --- a/test/regress/regress0/bv/test-bv_intro_pow2.smt2 +++ b/test/regress/regress0/bv/test-bv_intro_pow2.smt2 @@ -1,14 +1,14 @@ -; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores +; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores --bv-solver=layered (set-info :smt-lib-version 2.6) (set-logic QF_BV) (set-info :status unsat) -(declare-fun x () (_ BitVec 32)) -(declare-fun y () (_ BitVec 32)) -(declare-fun z () (_ BitVec 32)) +(declare-fun x () (_ BitVec 1024)) +(declare-fun y () (_ BitVec 1024)) +(declare-fun z () (_ BitVec 1024)) (assert (= z (bvadd x y))) (assert (distinct x y)) -(assert (and (distinct x (_ bv0 32)) (= (bvand x (bvsub x (_ bv1 32))) (_ bv0 32)))) -(assert (and (distinct y (_ bv0 32)) (= (bvand y (bvsub y (_ bv1 32))) (_ bv0 32)))) -(assert (and (distinct z (_ bv0 32)) (= (bvand z (bvsub z (_ bv1 32))) (_ bv0 32)))) +(assert (and (distinct x (_ bv0 1024)) (= (bvand x (bvsub x (_ bv1 1024))) (_ bv0 1024)))) +(assert (and (distinct y (_ bv0 1024)) (= (bvand y (bvsub y (_ bv1 1024))) (_ bv0 1024)))) +(assert (and (distinct z (_ bv0 1024)) (= (bvand z (bvsub z (_ bv1 1024))) (_ bv0 1024)))) (check-sat) (exit)