From: Mathias Preiner Date: Thu, 30 Sep 2021 19:52:09 +0000 (-0700) Subject: bv: Refactor ppRewrite and move to TheoryBV. (#7271) X-Git-Tag: cvc5-1.0.0~1147 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=31c108fadfd76419b57d89dae4ca5e8b4487c4af;p=cvc5.git bv: Refactor ppRewrite and move to TheoryBV. (#7271) This commit moves and refactors the ppRewrite() and ppStaticLearn() code from the layered solver to TheoryBV in order to apply a default set of preprocessing rules for each solver. BV solver can still implement additional rules. Note: Some of the rewrite rules in ppRewrite() have been removed since cluster runs showed that they don't improve anything, but actually makes the solver a lot worse. --- diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 17c65c290..dd7c1cd40 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -224,3 +224,11 @@ name = "Bitvector Theory" default = "false" help = "assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver" + +[[option]] + name = "rwExtendEq" + category = "expert" + long = "bv-rw-extend-eq" + type = "bool" + default = "false" + help = "enable additional rewrites over zero/sign extend over equalities with constants (useful on BV/2017-Preiner-scholl-smt08)" diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index b334a550d..fdc6d22d4 100644 --- a/src/preprocessing/passes/bv_intro_pow2.cpp +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -72,13 +72,11 @@ bool BvIntroPow2::isPowerOfTwo(TNode node) 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; + if (bv::utils::getSize(t) < 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))); + && (bv::utils::isOne(diff) || bv::utils::isOnes(diff))); } Node BvIntroPow2::rewritePowerOfTwo(TNode node) @@ -87,11 +85,11 @@ Node BvIntroPow2::rewritePowerOfTwo(TNode node) 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); + uint32_t 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 one = bv::utils::mkOne(size); + TNode x = diff == one ? a : b; 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); diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index 0f39474da..b3e23f70c 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -51,7 +51,7 @@ class BvIntroPow2 : public PreprocessingPass * Only to be called on top level assertions. */ Node rewritePowerOfTwo(TNode node); - /** Does the traversal of assertions and applies rweritePowerOfTwo. */ + /** Does the traversal of assertions and applies rewritePowerOfTwo. */ Node pow2Rewrite(Node node, std::unordered_map& cache); }; diff --git a/src/theory/bv/bv_solver_layered.cpp b/src/theory/bv/bv_solver_layered.cpp index 682c556cc..8427c1a50 100644 --- a/src/theory/bv/bv_solver_layered.cpp +++ b/src/theory/bv/bv_solver_layered.cpp @@ -51,7 +51,6 @@ BVSolverLayered::BVSolverLayered(Env& env, d_subtheories(), d_subtheoryMap(), d_statistics(), - d_staticLearnCache(), d_lemmasAdded(c, false), d_conflict(c, false), d_invalidateModelCache(c, true), @@ -391,103 +390,6 @@ void BVSolverLayered::propagate(Theory::Effort e) } } -TrustNode BVSolverLayered::ppRewrite(TNode t) -{ - Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n"; - Node res = t; - if (options().bv.bitwiseEq && RewriteRule::applies(t)) - { - Node result = RewriteRule::run(t); - res = rewrite(result); - } - else if (RewriteRule::applies(t)) - { - Node result = RewriteRule::run(t); - res = rewrite(result); - } - else if (res.getKind() == kind::EQUAL - && ((res[0].getKind() == kind::BITVECTOR_ADD - && RewriteRule::applies(res[1])) - || (res[1].getKind() == kind::BITVECTOR_ADD - && RewriteRule::applies(res[0])))) - { - Node mult = RewriteRule::applies(res[0]) - ? RewriteRule::run(res[0]) - : RewriteRule::run(res[1]); - Node factor = mult[0]; - Node sum = RewriteRule::applies(res[0]) ? res[1] : res[0]; - Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult); - Node rewr_eq = RewriteRule::run(new_eq); - if (rewr_eq[0].isVar() || rewr_eq[1].isVar()) - { - res = rewrite(rewr_eq); - } - else - { - res = t; - } - } - else if (RewriteRule::applies(t)) - { - res = RewriteRule::run(t); - } - else if (RewriteRule::applies(t)) - { - res = RewriteRule::run(t); - } - else if (RewriteRule::applies(t)) - { - res = RewriteRule::run(t); - } - - // if(t.getKind() == kind::EQUAL && - // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == - // kind::BITVECTOR_ADD) || - // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == - // kind::BITVECTOR_ADD))) { - // // if we have an equality between a multiplication and addition - // // try to express multiplication in terms of addition - // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1]; - // Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1]; - // if (RewriteRule::applies(mult)) { - // Node new_mult = RewriteRule::run(mult); - // Node new_eq = - // rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, - // new_mult, add)); - - // // the simplification can cause the formula to blow up - // // only apply if formula reduced - // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) { - // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST]; - // uint64_t old_size = bv->computeAtomWeight(t); - // Assert (old_size); - // uint64_t new_size = bv->computeAtomWeight(new_eq); - // double ratio = ((double)new_size)/old_size; - // if (ratio <= 0.4) { - // ++(d_statistics.d_numMultSlice); - // return new_eq; - // } - // } - - // if (new_eq.getKind() == kind::CONST_BOOLEAN) { - // ++(d_statistics.d_numMultSlice); - // return new_eq; - // } - // } - // } - - if (options().bv.bvAbstraction && t.getType().isBoolean()) - { - d_abstractionModule->addInputAtom(res); - } - Debug("bv-pp-rewrite") << "to " << res << "\n"; - if (res != t) - { - return TrustNode::mkTrustRewrite(t, res, nullptr); - } - return TrustNode::null(); -} - void BVSolverLayered::presolve() { Debug("bitvector") << "BVSolverLayered::presolve" << std::endl; @@ -611,56 +513,6 @@ EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b) ; } -void BVSolverLayered::ppStaticLearn(TNode in, NodeBuilder& learned) -{ - if (d_staticLearnCache.find(in) != d_staticLearnCache.end()) - { - return; - } - d_staticLearnCache.insert(in); - - if (in.getKind() == kind::EQUAL) - { - if ((in[0].getKind() == kind::BITVECTOR_ADD - && in[1].getKind() == kind::BITVECTOR_SHL) - || (in[1].getKind() == kind::BITVECTOR_ADD - && in[0].getKind() == kind::BITVECTOR_SHL)) - { - TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1]; - TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0]; - - if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL - && p[1].getKind() == kind::BITVECTOR_SHL) - { - unsigned size = utils::getSize(s); - Node one = utils::mkConst(size, 1u); - if (s[0] == one && p[0][0] == one && p[1][0] == one) - { - Node zero = utils::mkConst(size, 0u); - TNode b = p[0]; - TNode c = p[1]; - // (s : 1 << S) = (b : 1 << B) + (c : 1 << C) - Node b_eq_0 = b.eqNode(zero); - Node c_eq_0 = c.eqNode(zero); - Node b_eq_c = b.eqNode(c); - - Node dis = NodeManager::currentNM()->mkNode( - kind::OR, b_eq_0, c_eq_0, b_eq_c); - Node imp = in.impNode(dis); - learned << imp; - } - } - } - } - else if (in.getKind() == kind::AND) - { - for (size_t i = 0, N = in.getNumChildren(); i < N; ++i) - { - ppStaticLearn(in[i], learned); - } - } -} - bool BVSolverLayered::applyAbstraction(const std::vector& assertions, std::vector& new_assertions) { diff --git a/src/theory/bv/bv_solver_layered.h b/src/theory/bv/bv_solver_layered.h index 3b723b052..3870bc078 100644 --- a/src/theory/bv/bv_solver_layered.h +++ b/src/theory/bv/bv_solver_layered.h @@ -96,10 +96,6 @@ class BVSolverLayered : public BVSolver return std::string("BVSolverLayered"); } - TrustNode ppRewrite(TNode t) override; - - void ppStaticLearn(TNode in, NodeBuilder& learned) override; - void presolve() override; bool applyAbstraction(const std::vector& assertions, @@ -127,7 +123,6 @@ class BVSolverLayered : public BVSolver typedef std::unordered_set TNodeSet; typedef std::unordered_set NodeSet; - NodeSet d_staticLearnCache; typedef std::unordered_map NodeToNode; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index ba90c669e..f027b56fe 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -22,6 +22,8 @@ #include "theory/bv/bv_solver_bitblast.h" #include "theory/bv/bv_solver_bitblast_internal.h" #include "theory/bv/bv_solver_layered.h" +#include "theory/bv/theory_bv_rewrite_rules_normalization.h" +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/bv/theory_bv_utils.h" #include "theory/ee_setup_info.h" #include "theory/trust_substitutions.h" @@ -279,6 +281,37 @@ TrustNode TheoryBV::ppRewrite(TNode t, std::vector& lems) { return texp; } + + Debug("theory-bv-pp-rewrite") << "ppRewrite " << t << "\n"; + Node res = t; + if (options().bv.bitwiseEq && RewriteRule::applies(t)) + { + res = rewrite(RewriteRule::run(t)); + } + // useful on QF_BV/space/ndist + else if (RewriteRule::applies(t)) + { + res = rewrite(RewriteRule::run(t)); + } + // Useful for BV/2017-Preiner-scholl-smt08, but not for QF_BV + else if (options().bv.rwExtendEq) + { + if (RewriteRule::applies(t)) + { + res = RewriteRule::run(t); + } + else if (RewriteRule::applies(t)) + { + res = RewriteRule::run(t); + } + } + + Debug("theory-bv-pp-rewrite") << "to " << res << "\n"; + if (res != t) + { + return TrustNode::mkTrustRewrite(t, res, nullptr); + } + return d_internal->ppRewrite(t); } @@ -318,6 +351,47 @@ void TheoryBV::notifySharedTerm(TNode t) void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned) { + if (in.getKind() == kind::EQUAL) + { + // Only useful in combination with --bv-intro-pow2 on + // QF_BV/pspace/power2sum benchmarks. + // + // Matches for equality: + // + // (= (bvadd (bvshl 1 x) (bvshl 1 y)) (bvshl 1 z)) + // + // and does case analysis on the sum of two power of twos. + if ((in[0].getKind() == kind::BITVECTOR_ADD + && in[1].getKind() == kind::BITVECTOR_SHL) + || (in[1].getKind() == kind::BITVECTOR_ADD + && in[0].getKind() == kind::BITVECTOR_SHL)) + { + TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1]; + TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0]; + + if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL + && p[1].getKind() == kind::BITVECTOR_SHL) + { + if (utils::isOne(s[0]) && utils::isOne(p[0][0]) + && utils::isOne(p[1][0])) + { + Node zero = utils::mkZero(utils::getSize(s)); + TNode b = p[0]; + TNode c = p[1]; + // (s : 1 << S) = (b : 1 << B) + (c : 1 << C) + Node b_eq_0 = b.eqNode(zero); + Node c_eq_0 = c.eqNode(zero); + Node b_eq_c = b.eqNode(c); + + Node dis = NodeManager::currentNM()->mkNode( + kind::OR, b_eq_0, c_eq_0, b_eq_c); + Node imp = in.impNode(dis); + learned << imp; + } + } + } + } + d_internal->ppStaticLearn(in, learned); }