diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 106 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 33 |
3 files changed, 97 insertions, 48 deletions
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<BvIteMergeElseIf> rule136; RewriteRule<BvIteMergeThenElse> rule137; RewriteRule<BvIteMergeElseElse> rule138; - RewriteRule<AndConcatPullUp> rule139; + RewriteRule<AndOrConcatPullUp> 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<AndOne>::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<AndConcatPullUp>::applies(TNode node) +inline bool RewriteRule<AndOrConcatPullUp>::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<AndConcatPullUp>::applies(TNode node) } template <> -inline Node RewriteRule<AndConcatPullUp>::apply(TNode node) +inline Node RewriteRule<AndOrConcatPullUp>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<AndConcatPullUp>(" << node << ")" + Debug("bv-rewrite") << "RewriteRule<AndOrConcatPullUp>(" << 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<AndConcatPullUp>::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<FlattenAssocCommutNoDuplicates>, RewriteRule<AndSimplify>, - RewriteRule<AndConcatPullUp>>::apply(node); - + RewriteRule<AndOrConcatPullUp>>::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<FlattenAssocCommutNoDuplicates>, - RewriteRule<OrSimplify> - >::apply(node); + resultNode = + LinearRewriteStrategy<RewriteRule<FlattenAssocCommutNoDuplicates>, + RewriteRule<OrSimplify>, + RewriteRule<AndOrConcatPullUp>>::apply(node); - if (!prerewrite) { - resultNode = LinearRewriteStrategy - < RewriteRule<BitwiseSlicing> - >::apply(resultNode); - - if (resultNode.getKind() != node.getKind()) { - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + if (!prerewrite) + { + resultNode = + LinearRewriteStrategy<RewriteRule<BitwiseSlicing>>::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) { |