mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

Refactor bv_rewriter functions using unified variable assignment and early break logic

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-22 13:04:49 +03:00
parent d66609ea14
commit fa7fc8ef5e
1 changed files with 40 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -109,17 +109,20 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
break; break;
case OP_BNEG_OVFL: case OP_BNEG_OVFL:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_bvneg_overflow(args[0], result); st = mk_bvneg_overflow(args[0], result);
break;
case OP_BSHL: case OP_BSHL:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_shl(args[0], args[1], result); st = mk_bv_shl(args[0], args[1], result);
break;
case OP_BLSHR: case OP_BLSHR:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_lshr(args[0], args[1], result); st = mk_bv_lshr(args[0], args[1], result);
break;
case OP_BASHR: case OP_BASHR:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_ashr(args[0], args[1], result); st = mk_bv_ashr(args[0], args[1], result);
break;
case OP_BSDIV: case OP_BSDIV:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_sdiv(args[0], args[1], result); return mk_bv_sdiv(args[0], args[1], result);
@ -151,13 +154,16 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_smod_i(args[0], args[1], result); return mk_bv_smod_i(args[0], args[1], result);
case OP_CONCAT: case OP_CONCAT:
return mk_concat(num_args, args, result); st = mk_concat(num_args, args, result);
break;
case OP_EXTRACT: case OP_EXTRACT:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_extract(m_util.get_extract_high(f), m_util.get_extract_low(f), args[0], result); st = mk_extract(m_util.get_extract_high(f), m_util.get_extract_low(f), args[0], result);
break;
case OP_REPEAT: case OP_REPEAT:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_repeat(f->get_parameter(0).get_int(), args[0], result); st = mk_repeat(f->get_parameter(0).get_int(), args[0], result);
break;
case OP_ZERO_EXT: case OP_ZERO_EXT:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_zero_extend(f->get_parameter(0).get_int(), args[0], result); return mk_zero_extend(f->get_parameter(0).get_int(), args[0], result);
@ -596,53 +602,45 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
// //
// a <=_u #x000f // a <=_u #x000f
// //
unsigned bv_sz = m_util.get_bv_size(b); unsigned bv_sz = m_util.get_bv_size(a);
unsigned i = bv_sz; auto last_non_zero = [&](expr* x) {
unsigned first_non_zero = UINT_MAX; for (unsigned i = bv_sz; i-- > 0; )
while (i > 0) { if (!is_zero_bit(x, i))
--i; return i;
if (!is_zero_bit(b, i)) { return UINT_MAX;
first_non_zero = i; };
break;
} unsigned lnz = last_non_zero(b);
}
if (first_non_zero == UINT_MAX) { if (lnz == UINT_MAX) {
// all bits are zero // all bits are zero
result = m.mk_eq(a, mk_zero(bv_sz)); result = m.mk_eq(a, mk_zero(bv_sz));
return BR_REWRITE1; return BR_REWRITE1;
} }
else if (first_non_zero < bv_sz - 1 && m_le2extract) { else if (lnz < bv_sz - 1 && m_le2extract) {
result = m.mk_and(m.mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), mk_zero(bv_sz - first_non_zero - 1)), // a[sz-1:lnz+1] = 0 & a[lnz:0] <= b[lnz:0]
m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b))); result = m.mk_and(m.mk_eq(m_mk_extract(bv_sz - 1, lnz + 1, a), mk_zero(bv_sz - lnz - 1)),
m_util.mk_ule(m_mk_extract(lnz, 0, a), m_mk_extract(lnz, 0, b)));
return BR_REWRITE3; return BR_REWRITE3;
} }
// #x000f <=_u a <=> not (a <=_u #x000f) or a = #x000f
i = bv_sz;
first_non_zero = UINT_MAX;
while (i > 0) {
--i;
if (!is_zero_bit(a, i)) {
first_non_zero = i;
break;
}
}
if (first_non_zero == UINT_MAX) { lnz = last_non_zero(a);
if (lnz == UINT_MAX) {
// all bits are zero // all bits are zero
result = m.mk_eq(b, mk_zero(bv_sz)); result = m.mk_true();
return BR_REWRITE1; return BR_DONE;
} }
else if (first_non_zero < bv_sz - 1 && m_le2extract) { else if (lnz < bv_sz - 1 && m_le2extract) {
result = m.mk_and(m.mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, b), mk_zero(bv_sz - first_non_zero - 1)), // use the equivalence to simplify:
m_util.mk_ule(m_mk_extract(first_non_zero, 0, b), m_mk_extract(first_non_zero, 0, a))); // #x000f <=_u b <=> b[sz-1:lnz+1] != 0 or #xf <= b[lnz:0])
result = m.mk_or(m.mk_not(result), m.mk_eq(a, b));
result = m.mk_implies(m.mk_eq(m_mk_extract(bv_sz - 1, lnz + 1, b), mk_zero(bv_sz - lnz - 1)),
m_util.mk_ule(m_mk_extract(lnz, 0, a), m_mk_extract(lnz, 0, b)));
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
} }
#endif #endif