From b0f19c0eeb62ddd3759aa73fe8ae7a85019c3709 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 17 Oct 2018 09:22:44 -0700 Subject: [PATCH] BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const. (#2647) --- src/theory/bv/theory_bv_rewrite_rules.h | 6 +-- .../theory_bv_rewrite_rules_simplification.h | 49 +++++++++++++++---- src/theory/bv/theory_bv_rewriter.cpp | 39 ++++++++------- 3 files changed, 63 insertions(+), 31 deletions(-) diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index b52cb91a4..c6cd9eb1c 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, - AndOrConcatPullUp, + AndOrXorConcatPullUp, 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 AndOrConcatPullUp: out << "AndOrConcatPullUp"; return out; + case AndOrXorConcatPullUp:out << "AndOrXorConcatPullUp";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 5e9d2b349..8ac3036cd 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -489,7 +489,7 @@ Node RewriteRule::apply(TNode node) { /* -------------------------------------------------------------------------- */ /** - * AndOrConcatPullUp + * AndOrXorConcatPullUp * * And: * ---------------------------------------------------------------- @@ -524,13 +524,32 @@ Node RewriteRule::apply(TNode node) { * Rewrites to: concat(x[m-1:m-my] | y, * ~0_n, * x[mz-1:0] | z) + * + * Xor: + * ---------------------------------------------------------------- + * 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], + * ~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, + * ~[m-my-1:mz], + * x[mz-1:0] ^ z) */ template <> -inline bool RewriteRule::applies(TNode node) +inline bool RewriteRule::applies(TNode node) { if (node.getKind() != kind::BITVECTOR_AND - && node.getKind() != kind::BITVECTOR_OR) + && node.getKind() != kind::BITVECTOR_OR + && node.getKind() != kind::BITVECTOR_XOR) { return false; } @@ -557,9 +576,9 @@ 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; @@ -646,7 +665,7 @@ inline Node RewriteRule::apply(TNode node) } else { - Assert(kind == kind::BITVECTOR_OR); + Assert(kind == kind::BITVECTOR_OR || kind == kind::BITVECTOR_XOR); res << utils::mkExtract(x, m - my - 1, mz); } } @@ -657,12 +676,17 @@ inline Node RewriteRule::apply(TNode node) if (n > 1) res << utils::mkZero(n - 1); res << utils::mkExtract(x, mz, mz); } - else + else if (kind == kind::BITVECTOR_OR) { - Assert(kind == kind::BITVECTOR_OR); if (n > 1) res << utils::mkExtract(x, m - my - 1, mz + 1); res << utils::mkOne(1); } + else + { + Assert(kind == kind::BITVECTOR_XOR); + if (n > 1) res << utils::mkExtract(x, m - my - 1, mz + 1); + res << nm->mkNode(kind::BITVECTOR_NOT, utils::mkExtract(x, mz, mz)); + } } else { @@ -671,11 +695,16 @@ inline Node RewriteRule::apply(TNode node) { res << utils::mkExtract(x, m - my - 1, mz); } - else + else if (kind == kind::BITVECTOR_OR) { - Assert(kind == kind::BITVECTOR_OR); res << c; } + else + { + Assert(kind == kind::BITVECTOR_XOR); + res << nm->mkNode(kind::BITVECTOR_NOT, + utils::mkExtract(x, m - my - 1, mz)); + } } if (mz) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 3f018f800..0c6f1d37a 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -253,7 +253,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) resultNode = LinearRewriteStrategy, RewriteRule, - RewriteRule>::apply(node); + RewriteRule>::apply(node); if (!prerewrite) { resultNode = @@ -274,7 +274,7 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite) resultNode = LinearRewriteStrategy, RewriteRule, - RewriteRule>::apply(node); + RewriteRule>::apply(node); if (!prerewrite) { @@ -290,27 +290,30 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite) return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) { +RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) +{ Node resultNode = node; - resultNode = LinearRewriteStrategy - < RewriteRule, // flatten the expression - RewriteRule, // simplify duplicates and constants - RewriteRule, // checks if the constant part is zero and eliminates it - RewriteRule - >::apply(node); + resultNode = LinearRewriteStrategy< + RewriteRule, // flatten the expression + RewriteRule, // simplify duplicates and constants + RewriteRule, // checks if the constant part is zero and + // eliminates it + RewriteRule, + RewriteRule>::apply(node); - if (!prerewrite) { - resultNode = LinearRewriteStrategy - < RewriteRule, - RewriteRule - >::apply(resultNode); - - if (resultNode.getKind() != node.getKind()) { - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + if (!prerewrite) + { + resultNode = + LinearRewriteStrategy, + RewriteRule>::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::RewriteXnor(TNode node, bool prerewrite) { -- 2.30.2