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

Add rewrite rule: (mod (- a b) m) = 0 ==> (mod a m) = (mod b m)

Browse source 
The identity (a - b) mod m = 0 ⟺ a mod m = b mod m is a basic
number theory fact. Without this rewrite, z3 could not solve formulas
like (mod (- x y) m) = 0 ∧ (mod x m) ≠ (mod y m) with symbolic m,
timing out instead of returning unsat.

The rewrite is added to mk_eq_mod in the arith rewriter, matching
the pattern (= (mod (+ a (* -1 b)) m) 0) in both argument orders.

Fixes #1618.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-02-28 12:00:24 -10:00
parent 38ab05e50a
commit cfd087293c
1 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -913,6 +913,22 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
return true;
}
}
// (mod (+ a (* -1 b)) m) = 0 ==> (mod a m) = (mod b m)
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));
return true;
}
}
return false;
}