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 basic mod sign axiom for all mod operations

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:25:10 +00:00
parent 096a249ab5
commit 3bfc01f875
2 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -168,6 +168,13 @@ namespace arith {
add_clause(eqz, mod_ge_0);
add_clause(eqz, mod_lt_q);
// 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 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);
#if 0
/*literal div_ge_0 = */ mk_literal(a.mk_ge(div, zero));
/*literal div_le_0 = */ mk_literal(a.mk_le(div, zero));

6
src/smt/theory_arith_core.h
View file

@ -582,6 +582,12 @@ namespace smt {
mk_axiom(eqz, lower, false);
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
// 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 mod_neg(m_util.mk_mod(dividend, neg_divisor), m);
mk_axiom(eqz, m.mk_eq(mod, mod_neg));
rational k;
m_arith_eq_adapter.mk_axioms(ensure_enode(qr), ensure_enode(dividend));