diff options
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 22 |
1 files changed, 18 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index d40bbcfad..ea298d0e1 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -499,6 +499,11 @@ Node RewriteRule<AndOne>::apply(TNode node) { * 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) */ template <> @@ -524,7 +529,7 @@ inline bool RewriteRule<AndConcatPullUp>::applies(TNode node) } } if (n.isNull()) return false; - return utils::isZero(n) || utils::isOne(n); + return utils::isZero(n) || utils::isOne(n) || utils::isOnes(n); } template <> @@ -556,7 +561,7 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node) } x = xb.getNumChildren() > 1 ? xb.constructNode() : xb[0]; - is_const = -1; + is_const = -2; for (const TNode& child : concat) { if (c.isNull()) @@ -571,6 +576,11 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node) is_const = 1; c = child; } + else if (utils::isOnes(child)) + { + is_const = -1; + c = child; + } else { yb << child; @@ -608,12 +618,16 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node) { res << c; } - else + else if (is_const == 1) { - Assert(is_const == 1); if (n > 1) res << utils::mkZero(n-1); res << utils::mkExtract(x, m-my-n, m-my-n); } + else + { + Assert(is_const == -1); + res << utils::mkExtract(x, m-my-1, m-my-n); + } if (mz) { res << nm->mkNode( |