mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

Remove abs axioms and change uminus calls as requested

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-08-15 01:25:11 +00:00
parent 3bfc01f875
commit 3811c4baa1
2 changed files with 4 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -170,7 +170,7 @@ namespace arith {
// Add basic mod axiom for abs handling
// (mod x y) = (mod x -y) when y != 0 - fundamental property for divisibility
expr_ref neg_q(a.mk_uminus(q), m);
expr_ref neg_q(a.mk_add(a.mk_int(-1), 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);
@ -210,32 +210,10 @@ namespace arith {
// 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 neg_q(a.mk_add(a.mk_int(-1), 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);
// 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);
}

22
src/smt/theory_arith_core.h
View file

@ -584,7 +584,7 @@ namespace smt {
// Add basic mod axioms for abs handling
// (mod x y) = (mod x -y) when y != 0 - fundamental property for divisibility
expr_ref neg_divisor(m_util.mk_uminus(divisor), m);
expr_ref neg_divisor(m_util.mk_add(m_util.mk_int(-1), divisor), m);
expr_ref mod_neg(m_util.mk_mod(dividend, neg_divisor), m);
mk_axiom(eqz, m.mk_eq(mod, mod_neg));
@ -621,27 +621,9 @@ namespace smt {
// 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 neg_divisor(m_util.mk_add(m_util.mk_int(-1), 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));
// 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) &&