From 3bfc01f8753f590d7db162307b83f3e0f87f250f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 15 Aug 2025 00:25:10 +0000 Subject: [PATCH] Add basic mod sign axiom for all mod operations Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/sat/smt/arith_axioms.cpp | 7 +++++++ src/smt/theory_arith_core.h | 6 ++++++ 2 files changed, 13 insertions(+) diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 677fd703c..875a65619 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -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)); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index c657e4671..8b941a3d8 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -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));