mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

minor code simplification in bv rewriter

Browse source
This commit is contained in:
Nuno Lopes 2020-03-31 11:04:04 +01:00
parent 91497f923a
commit 0b6b267ec4
1 changed files with 2 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1978,14 +1978,8 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
if (m_util.is_bv_mul(arg, s, t)) {
// ~(-1 * x) --> (x - 1)
bv_size = m_util.get_bv_size(s);
if (m_util.is_allone(s)) {
rational minus_one = (rational::power_of_two(bv_size) - rational::one());
result = m_util.mk_bv_add(m_util.mk_numeral(minus_one, bv_size), t);
return BR_REWRITE1;
}
if (m_util.is_allone(t)) {
rational minus_one = (rational::power_of_two(bv_size) - rational::one());
result = m_util.mk_bv_add(m_util.mk_numeral(minus_one, bv_size), s);
if (m_util.is_allone(s) || m_util.is_allone(t)) {
result = m_util.mk_bv_add(s, t);
return BR_REWRITE1;
}
}