mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 10:50:24 +00:00
Code Activity

#7750

Browse source 
add pre-processing simplification
This commit is contained in:
Nikolaj Bjorner 2025-07-27 10:21:39 -07:00
parent eb24488c3e
commit e3139d4e03
1 changed files with 28 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2265,6 +2265,20 @@ br_status bv_rewriter::mk_bv_ext_rotate_left(expr * arg1, expr * arg2, expr_ref
unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64_t>(bv_size));
return mk_bv_rotate_left(shift, arg1, result);
}
expr* x = nullptr, * y = nullptr;
if (m_util.is_ext_rotate_right(arg1, x, y) && arg2 == y) {
// bv_ext_rotate_left(bv_ext_rotate_right(x, y), y) --> x
result = x;
return BR_DONE;
}
if (m_util.is_ext_rotate_left(arg1, x, y)) {
result = m_util.mk_bv_rotate_left(x, m_util.mk_bv_add(y, arg2));
return BR_REWRITE2;
}
if (m_util.is_ext_rotate_right(arg1, x, y)) {
result = m_util.mk_bv_rotate_left(x, m_util.mk_bv_sub(arg2, y));
return BR_REWRITE2;
}
return BR_FAILED;
}
@ -2275,6 +2289,20 @@ br_status bv_rewriter::mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref
unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64_t>(bv_size));
return mk_bv_rotate_right(shift, arg1, result);
}
expr* x = nullptr, * y = nullptr;
if (m_util.is_ext_rotate_left(arg1, x, y) && arg2 == y) {
// bv_ext_rotate_right(bv_ext_rotate_left(x, y), y) --> x
result = x;
return BR_DONE;
}
if (m_util.is_ext_rotate_right(arg1, x, y)) {
result = m_util.mk_bv_rotate_right(x, m_util.mk_bv_add(y, arg2));
return BR_REWRITE2;
}
if (m_util.is_ext_rotate_left(arg1, x, y)) {
result = m_util.mk_bv_rotate_right(x, m_util.mk_bv_sub(arg2, y));
return BR_REWRITE2;
}
return BR_FAILED;
}