mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Improve comment clarity in arith_rewriter mod fix

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 04:32:16 +00:00 • committed by GitHub
parent b544f7e58c
commit 26476c495f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1435,8 +1435,9 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
result = arg1;
return BR_DONE;
}
// Symbolic modulus: mod (mod x y) y = ite(y = 0, mod (mod x 0) 0, mod x y).
// Valid for all y: for y != 0, idempotency holds; for y = 0, both sides are mod0(mod0(x,0),0).
// Symbolic modulus: mod (mod x y) y → ite(y = 0, mod (mod x 0) 0, mod x y).
// Valid for all y: for y != 0, idempotency holds, returning mod x y (arg1);
// for y = 0, both sides evaluate to mod0(mod0(x,0),0).
if (!is_num2 && m_util.is_int(arg2)) {
expr_ref zero(m_util.mk_int(0), m);
result = m.mk_ite(m.mk_eq(arg2, zero),
@ -1503,6 +1504,8 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
}
if (change) {
expr_ref new_arg1(m);
// When all summands are multiples of the modulus, the sum reduces to 0.
// mod(0, y) will be further simplified by subsequent rewrites.
if (args.empty())
new_arg1 = m_util.mk_int(0);
else

8
src/test/arith_rewriter.cpp
View file

@ -84,17 +84,17 @@ void tst_arith_rewriter() {
std::cout << "consecutive product (minus) >= 0: " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
// Issue #7403: mod (a + b) b should simplify to mod a b for symbolic b
// Issue #7403: mod (a + y) y should simplify to mod a y for symbolic y
// i.e. (= (mod (+ I S) S) (mod I S)) should reduce to true
fml = parse_int_fml(m, "(= (mod (+ I S) S) (mod I S))");
rw(fml);
std::cout << "mod (a+b) b = mod a b: " << mk_pp(fml, m) << "\n";
std::cout << "mod (a+y) y = mod a y: " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
// mod (a + 2*b) b should simplify to mod a b (multiple of modulus dropped)
// mod (a + 2*y) y should simplify to mod a y (multiple of modulus dropped)
fml = parse_int_fml(m, "(= (mod (+ I (* 2 S)) S) (mod I S))");
rw(fml);
std::cout << "mod (a+2b) b = mod a b: " << mk_pp(fml, m) << "\n";
std::cout << "mod (a+2y) y = mod a y: " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
// mod (mod a b) b should simplify for non-zero numeral b