diff options
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 123 |
1 files changed, 10 insertions, 113 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 8ac3036cd..7efdc2c81 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -491,57 +491,12 @@ Node RewriteRule<AndOne>::apply(TNode node) { /** * AndOrXorConcatPullUp * - * 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 <op> concat(y_my, <const>_n, z_mz) + * <const>_n in { 0_n, 1_n, ~0_n } * - * 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) - * - * 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) + * Rewrites to: concat(x[m-1:m-my] <op> y, + * x[m-my-1:mz] <op> <const>_n, + * x[mz-1:0] <op> z) */ template <> @@ -580,7 +535,6 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<AndOrXorConcatPullUp>(" << node << ")" << std::endl; - int32_t is_const; uint32_t m, my, mz, n; size_t nc; Kind kind = node.getKind(); @@ -605,24 +559,12 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) } x = xb.getNumChildren() > 1 ? xb.constructNode() : xb[0]; - is_const = -2; for (const TNode& child : concat) { if (c.isNull()) { - if (utils::isZero(child)) + if (utils::isZero(child) || utils::isOne(child) || utils::isOnes(child)) { - is_const = 0; - c = child; - } - else if (utils::isOne(child)) - { - is_const = 1; - c = child; - } - else if (utils::isOnes(child)) - { - is_const = -1; c = child; } else @@ -657,59 +599,14 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) { res << nm->mkNode(kind, utils::mkExtract(x, m - 1, m - my), y); } - if (is_const == 0) - { - if (kind == kind::BITVECTOR_AND) - { - res << c; - } - else - { - Assert(kind == kind::BITVECTOR_OR || kind == kind::BITVECTOR_XOR); - res << utils::mkExtract(x, m - my - 1, mz); - } - } - else if (is_const == 1) - { - if (kind == kind::BITVECTOR_AND) - { - if (n > 1) res << utils::mkZero(n - 1); - res << utils::mkExtract(x, mz, mz); - } - else if (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 - { - Assert(is_const == -1); - if (kind == kind::BITVECTOR_AND) - { - res << utils::mkExtract(x, m - my - 1, mz); - } - else if (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)); - } - } + + res << nm->mkNode(kind, utils::mkExtract(x, m - my - 1, mz), c); + if (mz) { res << nm->mkNode(kind, utils::mkExtract(x, mz - 1, 0), z); } + return res; } |