mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

add a bv rewrite pattern:

Browse source 
(bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1))
This commit is contained in:
Nuno Lopes 2016-02-18 17:45:55 +00:00
parent d32b4c71d1
commit 73da4dda07
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -320,6 +320,21 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
}
}
expr* a1, *a2, *a3, *a4, *a5, *a6;
// (bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1))
// (bvsle (+ x (* -1 (srem_i x c1))) c2)
// pre: (and (> c1 0) (> c2 0) (= c2 % c1 0) (<= (+ c1 c2 -1) max_int))
if (is_signed && is_num2 && m_util.is_bv_add(a, a1, a2) &&
m_util.is_bv_mul(a2, a3, a4) && is_numeral(a3, r1, sz) &&
m_util.norm(r1, sz, is_signed).is_minus_one() &&
m_util.is_bv_sremi(a4, a5, a6) && is_numeral(a6, r1, sz) &&
(r1 = m_util.norm(r1, sz, is_signed), r1.is_pos()) &&
r2.is_pos() &&
(r2 % r1).is_zero() && r1 + r2 - rational::one() < rational::power_of_two(sz-1)) {
result = m_util.mk_sle(a1, m_util.mk_numeral(r1 + r2 - rational::one(), sz));
return BR_REWRITE2;
}
#if 0
if (!is_signed && m_util.is_concat(b) && to_app(b)->get_num_args() == 2 && m_util.is_zero(to_app(b)->get_arg(0))) {
//