mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix #5929 - add parameter bv_le2extract to allow disabling the disassembly to extract
This commit is contained in:
parent
cb1e16fd76
commit
431c3af409
|
@ -37,6 +37,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
|
|||
m_extract_prop = p.bv_extract_prop();
|
||||
m_ite2id = p.bv_ite2id();
|
||||
m_le_extra = p.bv_le_extra();
|
||||
m_le2extract = p.bv_le2extract();
|
||||
set_sort_sums(p.bv_sort_ac());
|
||||
}
|
||||
|
||||
|
@ -577,7 +578,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
|
|||
result = m().mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz));
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else if (first_non_zero < bv_sz - 1) {
|
||||
else if (first_non_zero < bv_sz - 1 && m_le2extract) {
|
||||
result = m().mk_and(m().mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), m_util.mk_numeral(numeral(0), bv_sz - first_non_zero - 1)),
|
||||
m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b)));
|
||||
return BR_REWRITE3;
|
||||
|
|
|
@ -62,6 +62,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
|
|||
bool m_extract_prop;
|
||||
bool m_bvnot_simpl;
|
||||
bool m_le_extra;
|
||||
bool m_le2extract;
|
||||
|
||||
bool is_zero_bit(expr * x, unsigned idx);
|
||||
|
||||
|
|
|
@ -11,5 +11,6 @@ def_module_params(module_name='rewriter',
|
|||
("bv_extract_prop", BOOL, False, "attempt to partially propagate extraction inwards"),
|
||||
("bv_not_simpl", BOOL, False, "apply simplifications for bvnot"),
|
||||
("bv_ite2id", BOOL, False, "rewrite ite that can be simplified to identity"),
|
||||
("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications")
|
||||
("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications"),
|
||||
("bv_le2extract", BOOL, True, "disassemble bvule to extract")
|
||||
))
|
||||
|
|
Loading…
Reference in a new issue