mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

Fix: add mod simplification rule for (mod (+ ... k*y ...) y) = (mod (+ ...) y)

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/16d3a058-5225-44d4-8080-d1a641c181ff

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-12 23:52:29 +00:00 • committed by GitHub
parent 0814bcb7e4
commit bb9a714124
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 50 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1465,6 +1465,41 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
}
}
// (mod (+ ... k*y ...) y) = (mod (+ ...) y) for integer k
// Remove summands that are integer multiples of arg2 from the sum.
if (!is_num2 && m_util.is_int(arg2) && is_add(arg1)) {
expr_ref_buffer new_args(m);
bool change = false;
for (expr* arg : *to_app(arg1)) {
expr* s1 = nullptr, *s2 = nullptr;
rational k;
if (arg == arg2) {
// summand equals the modulus (k=1 case), drop it
change = true;
}
else if (m_util.is_mul(arg, s1, s2) &&
((m_util.is_numeral(s1, k) && s2 == arg2) ||
(m_util.is_numeral(s2, k) && s1 == arg2))) {
// k * arg2 or arg2 * k, drop it
change = true;
}
else {
new_args.push_back(arg);
}
}
if (change) {
expr_ref sum(m);
if (new_args.empty())
sum = m_util.mk_int(0);
else if (new_args.size() == 1)
sum = expr_ref(new_args[0], m);
else
sum = m.mk_app(to_app(arg1)->get_decl(), new_args.size(), new_args.data());
result = m_util.mk_mod(sum, arg2);
return BR_REWRITE3;
}
}
expr* x = nullptr, * y = nullptr, * z = nullptr;
if (is_num2 && v2.is_pos() && m_util.is_mul(arg1, x, y) && m_util.is_numeral(x, v1, is_int) && v1 > 0 && divides(v1, v2)) {
result = m_util.mk_mul(m_util.mk_int(v1), m_util.mk_mod(y, m_util.mk_int(v2/v1)));

15
src/test/arith_rewriter.cpp
View file

@ -40,6 +40,8 @@ static expr_ref parse_int_fml(ast_manager& m, char const* str) {
std::ostringstream buffer;
buffer << "(declare-const I Int)\n"
<< "(declare-const S Int)\n"
<< "(declare-const x Int)\n"
<< "(declare-const y Int)\n"
<< "(assert " << str << ")\n";
std::istringstream is(buffer.str());
VERIFY(parse_smt2_commands(ctx, is));
@ -83,4 +85,17 @@ void tst_arith_rewriter() {
rw(fml);
std::cout << "consecutive product (minus) >= 0: " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
// Issue: (mod (+ x y) y) should simplify to (mod x y)
// This is the key identity: (a + k*b) mod b = a mod b
fml = parse_int_fml(m, "(= (mod (+ x y) y) (mod x y))");
rw(fml);
std::cout << "mod congruence (mod (+ x y) y) = (mod x y): " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
// (mod (+ x (* 3 y)) y) should simplify to (mod x y)
fml = parse_int_fml(m, "(= (mod (+ x (* 3 y)) y) (mod x y))");
rw(fml);
std::cout << "mod congruence (mod (+ x (* 3 y)) y) = (mod x y): " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
}