From 7e29e6a9d929b3fd999499fd0aa97343c9c9fce5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 16 Oct 2018 17:48:58 -0700 Subject: BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643) Match: `x_m | concat(y_my, 0_n, z_mz)` Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)` Match: `x_m | concat(y_my, 1_n, z_mz)` Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)` Match: `x_m | concat(y_my, ~0_n, z_mz)` Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)` On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s): ``` | CVC4-base | CVC4-concatpullup-or | BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] | totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 | ``` --- src/theory/bv/theory_bv_rewrite_rules.h | 6 +- .../bv/theory_bv_rewrite_rules_simplification.h | 106 +++++++++++++++------ src/theory/bv/theory_bv_rewriter.cpp | 33 +++---- 3 files changed, 97 insertions(+), 48 deletions(-) (limited to 'src') diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 991d30824..b52cb91a4 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -119,7 +119,7 @@ enum RewriteRuleId BitwiseIdemp, AndZero, AndOne, - AndConcatPullUp, + AndOrConcatPullUp, OrZero, OrOne, XorDuplicate, @@ -201,7 +201,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case ConcatFlatten: out << "ConcatFlatten"; return out; case ConcatExtractMerge: out << "ConcatExtractMerge"; return out; case ConcatConstantMerge: out << "ConcatConstantMerge"; return out; - case AndConcatPullUp: out << "AndConcatPullUp"; return out; + case AndOrConcatPullUp: out << "AndOrConcatPullUp"; return out; case ExtractExtract: out << "ExtractExtract"; return out; case ExtractWhole: out << "ExtractWhole"; return out; case ExtractConcat: out << "ExtractConcat"; return out; @@ -581,7 +581,7 @@ struct AllRewriteRules { RewriteRule rule136; RewriteRule rule137; RewriteRule rule138; - RewriteRule rule139; + RewriteRule rule139; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index ea298d0e1..5e9d2b349 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -489,27 +489,51 @@ Node RewriteRule::apply(TNode node) { /* -------------------------------------------------------------------------- */ /** - * AndConcatPullUp - * - * Match: x_m & concat(y_my, 0_n, z_mz) - * Rewrites to: concat(x[m-1:m-my] & y, 0_n, x[m-my-n-1:0] & z) - * - * Match: x_m & concat(y_my, 1_n, z_mz) - * Rewrites to: concat(x[m-1:m-my] & y, - * 0_[n-1], - * x[m-my-n:m-my-n], - * x[m-my-n-1:0] & z) - * - * Match: x_m & concat(y_my, ~0_n, z_mz) - * Rewrites to: concat(x[m-1:m-my] & y, - * x[m-my-1:m-my-n], - * x[m-my-n-1:0] & z) + * AndOrConcatPullUp + * + * And: + * ---------------------------------------------------------------- + * Match: x_m & concat(y_my, 0_n, z_mz) + * Rewrites to: concat(x[m-1:m-my] & y, 0_n, x[mz-1:0] & z) + * + * Match: x_m & concat(y_my, 1_n, z_mz) + * Rewrites to: concat(x[m-1:m-my] & y, + * 0_[n-1], + * x[mz:mz], + * x[mz-1:0] & z) + * + * Match: x_m & concat(y_my, ~0_n, z_mz) + * Rewrites to: concat(x[m-1:m-my] & y, + * x[m-my-1:mz], + * x[mz-1:0] & z) + * + * Or: + * ---------------------------------------------------------------- + * Match: x_m | concat(y_my, 0_n, z_mz) + * Rewrites to: concat(x[m-1:m-my] | y, + * x[m-my-1:mz], + * x[mz-1:0] | z) + * + * Match: x_m | concat(y_my, 1_n, z_mz) + * Rewrites to: concat(x[m-1:m-my] | y, + * x[m-my-1:mz+1], + * 1_1, + * x[mz-1:0] | z) + * + * Match: x_m | concat(y_my, ~0_n, z_mz) + * Rewrites to: concat(x[m-1:m-my] | y, + * ~0_n, + * x[mz-1:0] | z) */ template <> -inline bool RewriteRule::applies(TNode node) +inline bool RewriteRule::applies(TNode node) { - if (node.getKind() != kind::BITVECTOR_AND) return false; + if (node.getKind() != kind::BITVECTOR_AND + && node.getKind() != kind::BITVECTOR_OR) + { + return false; + } TNode n; @@ -533,20 +557,21 @@ inline bool RewriteRule::applies(TNode node) } template <> -inline Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; int32_t is_const; uint32_t m, my, mz, n; size_t nc; + Kind kind = node.getKind(); TNode concat; Node x, y, z, c; - NodeBuilder<> xb(kind::BITVECTOR_AND); + NodeBuilder<> xb(kind); NodeBuilder<> yb(kind::BITVECTOR_CONCAT); NodeBuilder<> zb(kind::BITVECTOR_CONCAT); NodeBuilder<> res(kind::BITVECTOR_CONCAT); - NodeManager *nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); for (const TNode& child : node) { @@ -611,27 +636,50 @@ inline Node RewriteRule::apply(TNode node) if (my) { - res << nm->mkNode( - kind::BITVECTOR_AND, utils::mkExtract(x, m - 1, m - my), y); + res << nm->mkNode(kind, utils::mkExtract(x, m - 1, m - my), y); } if (is_const == 0) { - res << c; + if (kind == kind::BITVECTOR_AND) + { + res << c; + } + else + { + Assert(kind == kind::BITVECTOR_OR); + res << utils::mkExtract(x, m - my - 1, mz); + } } else if (is_const == 1) { - if (n > 1) res << utils::mkZero(n-1); - res << utils::mkExtract(x, m-my-n, m-my-n); + if (kind == kind::BITVECTOR_AND) + { + if (n > 1) res << utils::mkZero(n - 1); + res << utils::mkExtract(x, mz, mz); + } + else + { + Assert(kind == kind::BITVECTOR_OR); + if (n > 1) res << utils::mkExtract(x, m - my - 1, mz + 1); + res << utils::mkOne(1); + } } else { Assert(is_const == -1); - res << utils::mkExtract(x, m-my-1, m-my-n); + if (kind == kind::BITVECTOR_AND) + { + res << utils::mkExtract(x, m - my - 1, mz); + } + else + { + Assert(kind == kind::BITVECTOR_OR); + res << c; + } } if (mz) { - res << nm->mkNode( - kind::BITVECTOR_AND, utils::mkExtract(x, m - my - n - 1, 0), z); + res << nm->mkNode(kind, utils::mkExtract(x, mz - 1, 0), z); } return res; } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index cfcd8f692..3f018f800 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -253,8 +253,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) resultNode = LinearRewriteStrategy, RewriteRule, - RewriteRule>::apply(node); - + RewriteRule>::apply(node); if (!prerewrite) { resultNode = @@ -269,24 +268,26 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){ +RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite) +{ Node resultNode = node; - resultNode = LinearRewriteStrategy - < RewriteRule, - RewriteRule - >::apply(node); + resultNode = + LinearRewriteStrategy, + RewriteRule, + RewriteRule>::apply(node); - if (!prerewrite) { - resultNode = LinearRewriteStrategy - < RewriteRule - >::apply(resultNode); - - if (resultNode.getKind() != node.getKind()) { - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + if (!prerewrite) + { + resultNode = + LinearRewriteStrategy>::apply(resultNode); + + if (resultNode.getKind() != node.getKind()) + { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } } - - return RewriteResponse(REWRITE_DONE, resultNode); + + return RewriteResponse(REWRITE_DONE, resultNode); } RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) { -- cgit v1.2.3