mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 04:56:03 +00:00
Code Activity

Add mod axioms for abs divisor handling

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:10:06 +00:00
parent f69e875fc6
commit b38497ac91
2 changed files with 24 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -200,6 +200,19 @@ namespace arith {
else if (!a.is_numeral(q)) { else if (!a.is_numeral(q)) {
// (or (= y 0) (<= (* y (div x y)) x)) // (or (= y 0) (<= (* y (div x y)) x))
add_clause(eqz, mk_literal(a.mk_le(a.mk_mul(q, div), p))); add_clause(eqz, mk_literal(a.mk_le(a.mk_mul(q, div), p)));
// Add axiom: (mod x y) = (mod x -y) when y != 0
// This is needed for divisibility problems to work correctly with abs(y)
expr_ref neg_q(a.mk_uminus(q), m);
expr_ref mod_neg(a.mk_mod(p, neg_q), m);
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
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);
} }

11
src/smt/theory_arith_core.h
View file

@ -612,6 +612,17 @@ namespace smt {
s(div_ge); s(div_ge);
mk_axiom(eqz, div_ge, false); mk_axiom(eqz, div_ge, false);
TRACE(arith, tout << eqz << " " << div_ge << "\n"); TRACE(arith, tout << eqz << " " << div_ge << "\n");
// Add axiom: (mod x y) = (mod x -y) when y != 0
// This is needed for divisibility problems to work correctly with abs(y)
expr_ref neg_divisor(m_util.mk_uminus(divisor), m);
expr_ref mod_neg(m_util.mk_mod(dividend, neg_divisor), m);
mk_axiom(eqz, m.mk_eq(mod, mod_neg));
// Also add the axiom for abs: (mod x y) = (mod x abs(y)) when y != 0
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));
} }
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) && if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&