mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 13:54:53 +00:00
Code Activity

Guard mod rewrite rule for y=0: skip when concrete zero, use ite for symbolic y

Browse source 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-28 22:36:34 +00:00
parent 59db146641
commit a05520f261
1 changed files with 20 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/ast/rewriter/arith_rewriter.cpp
View file

@ -914,18 +914,30 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
}
}
// (mod (+ a (* -1 b)) m) = 0 ==> (mod a m) = (mod b m)
// guarded by ite(m = 0, original, rewritten) when m is symbolic,
// because mod is uninterpreted for divisor 0
if (m_util.is_mod(arg1, x, y) && m_util.is_zero(arg2) && is_add(x) && to_app(x)->get_num_args() == 2) {
expr* a = to_app(x)->get_arg(0);
expr* b_neg = to_app(x)->get_arg(1);
expr* b = nullptr;
rational coeff;
if (m_util.is_mul(b_neg, z, b) && m_util.is_numeral(z, coeff) && coeff.is_minus_one()) {
result = m.mk_eq(m_util.mk_mod(a, y), m_util.mk_mod(b, y));
return true;
}
// also handle (+ (* -1 a) b) = 0
if (m_util.is_mul(a, z, u) && m_util.is_numeral(z, coeff) && coeff.is_minus_one()) {
result = m.mk_eq(m_util.mk_mod(u, y), m_util.mk_mod(b_neg, y));
rational coeff, yval;
bool y_is_numeral = m_util.is_numeral(y, yval);
if (y_is_numeral && yval.is_zero())
return false;
expr_ref eq(m);
if (m_util.is_mul(b_neg, z, b) && m_util.is_numeral(z, coeff) && coeff.is_minus_one())
eq = m.mk_eq(m_util.mk_mod(a, y), m_util.mk_mod(b, y));
else if (m_util.is_mul(a, z, u) && m_util.is_numeral(z, coeff) && coeff.is_minus_one())
eq = m.mk_eq(m_util.mk_mod(u, y), m_util.mk_mod(b_neg, y));
if (eq) {
if (!y_is_numeral) {
// guard: when y = 0, mod is uninterpreted, so keep the original constraint
// use concrete zero so the then-branch is not re-rewritten by this rule
expr_ref zero(m_util.mk_int(0), m);
eq = m.mk_ite(m.mk_eq(y, zero),
m.mk_eq(m_util.mk_mod(x, zero), arg2), eq);
}
result = eq;
return true;
}
}