mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 20:46:01 +00:00
Code Activity

Add enhanced conditional axioms for mod with ite expressions

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-08-15 00:17:06 +00:00
parent b38497ac91
commit 096a249ab5
2 changed files with 30 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/sat/smt/arith_axioms.cpp
View file

@ -208,11 +208,27 @@ namespace arith {
literal mod_eq_mod_neg = mk_literal(m.mk_eq(mod, mod_neg));
add_clause(eqz, mod_eq_mod_neg);
// Also add the axiom for abs: (mod x y) = (mod x abs(y)) when y != 0
// Also add the axiom for abs: (mod x y) = (mod x abs(y)) when y != 0
expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m);
expr_ref mod_abs(a.mk_mod(p, abs_q), m);
literal mod_eq_mod_abs = mk_literal(m.mk_eq(mod, mod_abs));
add_clause(eqz, mod_eq_mod_abs);
// Add conditional axioms for the ite form that abs gets rewritten to
// (mod x (ite (>= y 0) y (-y))) should equal (mod x y) when y >= 0
// (mod x (ite (>= y 0) y (-y))) should equal (mod x (-y)) when y < 0
expr_ref q_ge_0(a.mk_ge(q, zero), m);
expr_ref ite_divisor(m.mk_ite(q_ge_0, q, neg_q), m);
expr_ref mod_ite(a.mk_mod(p, ite_divisor), m);
// When y >= 0: mod(x, ite(...)) = mod(x, y)
literal q_ge_0_lit = mk_literal(q_ge_0);
literal mod_ite_eq_mod = mk_literal(m.mk_eq(mod_ite, mod));
add_clause(eqz, ~q_ge_0_lit, mod_ite_eq_mod);
// When y < 0: mod(x, ite(...)) = mod(x, -y)
literal mod_ite_eq_mod_neg = mk_literal(m.mk_eq(mod_ite, mod_neg));
add_clause(eqz, q_ge_0_lit, mod_ite_eq_mod_neg);
}

13
src/smt/theory_arith_core.h
View file

@ -623,6 +623,19 @@ namespace smt {
expr_ref abs_divisor(m.mk_ite(m_util.mk_ge(divisor, zero), divisor, m_util.mk_uminus(divisor)), m);
expr_ref mod_abs(m_util.mk_mod(dividend, abs_divisor), m);
mk_axiom(eqz, m.mk_eq(mod, mod_abs));
// Add conditional axioms for the ite form that abs gets rewritten to
expr_ref divisor_ge_0(m_util.mk_ge(divisor, zero), m);
expr_ref ite_divisor(m.mk_ite(divisor_ge_0, divisor, neg_divisor), m);
expr_ref mod_ite(m_util.mk_mod(dividend, ite_divisor), m);
// When y >= 0: mod(x, ite(...)) = mod(x, y)
expr_ref ante1(m.mk_and(m.mk_not(eqz), divisor_ge_0), m);
mk_axiom(ante1, m.mk_eq(mod_ite, mod));
// When y < 0: mod(x, ite(...)) = mod(x, -y)
expr_ref ante2(m.mk_and(m.mk_not(eqz), m.mk_not(divisor_ge_0)), m);
mk_axiom(ante2, m.mk_eq(mod_ite, mod_neg));
}
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&