mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

parameter evaluation order

Browse source
This commit is contained in:
Lev Nachmanson 2025-10-07 08:53:49 -07:00 • committed by Nikolaj Bjorner
parent 28c625a170
commit e113d39aa8
1 changed files with 29 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1557,17 +1557,20 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
} }
if (str().is_empty(b)) { if (str().is_empty(b)) {
result = m().mk_ite(m().mk_and(m_autil.mk_le(zero(), c), // enforce deterministic evaluation order for bounds checks
m_autil.mk_le(c, str().mk_length(a))), auto a1 = m_autil.mk_le(zero(), c);
c, auto b1 = m_autil.mk_le(c, str().mk_length(a));
minus_one()); auto cond = m().mk_and(a1, b1);
result = m().mk_ite(cond, c, minus_one());
return BR_REWRITE2; return BR_REWRITE2;
} }
if (str().is_empty(a)) { if (str().is_empty(a)) {
expr* emp = str().mk_is_empty(b); expr* emp = str().mk_is_empty(b);
result = m().mk_ite(m().mk_and(m().mk_eq(c, zero()), emp), zero(), minus_one()); auto a1 = m().mk_eq(c, zero());
auto cond = m().mk_and(a1, emp);
result = m().mk_ite(cond, zero(), minus_one());
return BR_REWRITE2; return BR_REWRITE2;
} }
@ -2732,11 +2735,15 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
return BR_REWRITE2; return BR_REWRITE2;
} }
else if (re().is_intersection(r, r1, r2)) { else if (re().is_intersection(r, r1, r2)) {
result = re().mk_inter(re().mk_reverse(r1), re().mk_reverse(r2)); auto a = re().mk_reverse(r1);
auto b = re().mk_reverse(r2);
result = re().mk_inter(a, b);
return BR_REWRITE2; return BR_REWRITE2;
} }
else if (re().is_diff(r, r1, r2)) { else if (re().is_diff(r, r1, r2)) {
result = re().mk_diff(re().mk_reverse(r1), re().mk_reverse(r2)); auto a = re().mk_reverse(r1);
auto b = re().mk_reverse(r2);
result = re().mk_diff(a, b);
return BR_REWRITE2; return BR_REWRITE2;
} }
else if (m().is_ite(r, p, r1, r2)) { else if (m().is_ite(r, p, r1, r2)) {
@ -3031,7 +3038,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
// SASSERT(u().is_char(c1)); // SASSERT(u().is_char(c1));
// SASSERT(u().is_char(c2)); // SASSERT(u().is_char(c2));
// case: c1 <= e <= c2 // case: c1 <= e <= c2
range = simplify_path(e, m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2))); // deterministic evaluation for range bounds
auto a_le = u().mk_le(c1, e);
auto b_le = u().mk_le(e, c2);
auto rng_cond = m().mk_and(a_le, b_le);
range = simplify_path(e, rng_cond);
psi = simplify_path(e, m().mk_and(path, range)); psi = simplify_path(e, m().mk_and(path, range));
} }
else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) { else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) {
@ -4005,8 +4016,13 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
// if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else [] // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else []
// //
hd = mk_seq_first(r1); hd = mk_seq_first(r1);
m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), // isolate nested conjunction for deterministic evaluation
m().mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele)), result); auto a0 = u().mk_le(m_util.mk_char('0'), ele);
auto a1 = u().mk_le(ele, m_util.mk_char('9'));
auto a2 = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
auto a3 = m().mk_eq(hd, ele);
auto inner = m().mk_and(a2, a3);
m_br.mk_and(a0, a1, inner, result);
tl = re().mk_to_re(mk_seq_rest(r1)); tl = re().mk_to_re(mk_seq_rest(r1));
return re_and(result, tl); return re_and(result, tl);
} }
@ -5040,7 +5056,9 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
rep.insert(elem, solution); rep.insert(elem, solution);
rep(cond); rep(cond);
if (!is_uninterp_const(elem)) { if (!is_uninterp_const(elem)) {
cond = m().mk_and(m().mk_eq(elem, solution), cond); // ensure deterministic evaluation order when augmenting condition
auto eq_sol = m().mk_eq(elem, solution);
cond = m().mk_and(eq_sol, cond);
} }
} }
else if (all_ranges) { else if (all_ranges) {