mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

add opportunistic, missing, bv rewrites

Browse source 
- x >> x logical = 0
- ~x = -1 -x
- x * (y << z) = (x * y) << z
This commit is contained in:
Nikolaj Bjorner 2022-10-25 10:29:48 -07:00
parent 09a2ba4931
commit c62c5e9d23
1 changed files with 27 additions and 4 deletions

31
src/ast/rewriter/bv_rewriter.cpp
View file

@ -911,6 +911,11 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
return BR_REWRITE2;
}
if (arg1 == arg2) {
result = mk_numeral(0, bv_size);
return BR_DONE;
}
return BR_FAILED;
}
@ -2250,10 +2255,10 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
br_status st = mk_mul_core(num_args, args, result);
if (st != BR_FAILED && st != BR_DONE)
return st;
expr * x;
expr * y;
expr* x, * y, * z, * u;
if (st == BR_FAILED && num_args == 2) {
x = args[0]; y = args[1];
x = args[0];
y = args[1];
}
else if (st == BR_DONE && is_mul(result) && to_app(result)->get_num_args() == 2) {
x = to_app(result)->get_arg(0);
@ -2262,7 +2267,25 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
else {
return st;
}
// ~x = -1 - x
unsigned sz = m_util.get_bv_size(x);
if (m_util.is_bv_not(x, z)) {
result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(-1, sz), z), y);
return BR_REWRITE3;
}
if (m_util.is_bv_not(y, z)) {
result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(-1, sz), z), x);
return BR_REWRITE3;
}
// shl(z, u) * x = shl(x * z, u)
if (m_util.is_bv_shl(x, z, u)) {
result = m_util.mk_bv_shl(m_util.mk_bv_mul(z, y), u);
return BR_REWRITE2;
}
if (m_util.is_bv_shl(y, z, u)) {
result = m_util.mk_bv_shl(m_util.mk_bv_mul(z, x), u);
return BR_REWRITE2;
}
if (m_mul2concat) {
numeral v;
unsigned bv_size;