From 73151f19606cc6569db250959751dde7f9b5078c Mon Sep 17 00:00:00 2001 From: Arie <123119895+1arie1@users.noreply.github.com> Date: Tue, 26 May 2026 21:12:38 -0400 Subject: [PATCH] nla_grobner: add mod_residue pattern to propagate_quotients (#9597) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds a new lemma pattern to nla_grobner::propagate_quotients that derives a modular-residue constraint from polynomial divisibility, filling a gap between quotient1-5 (model-value-driven case splits) and the polynomials Grobner actually produces on Skolem-encoded mod arithmetic. Pattern ------- For a polynomial p with all-integer free variables and a linear monomial c_v * v (single integer var), the pattern computes M = gcd(|c_i/c_v|) over the other monomials and K = c0/c_v for the constant term. When both are integers, dividing p by c_v gives v + M*Q + K = 0 with Q an integer so v ≡ -K (mod M). The pattern emits the sound disjunctive lemma (v < 0) ∨ (v ≥ M) ∨ (v = target) where target = (-K) mod M ∈ [0, M-1]. This encodes "v ∈ target + M·Z" in a form the LP / SAT layer can refute against current bounds. Motivation ---------- QF_UFNIA verification benchmarks over fixed-prime modular arithmetic (e.g. zk applications using the BabyBear prime 2013265921) regularly produce basis polynomials of the form -p*v_div + p*(v_a * v_b) - v_mod = 0 where v_mod is the result of (mod (* v_a v_b) p). The polynomial sits in the Grobner basis but none of quotient1-5 fires: they all require specific model-value alignments (r_value == 0, |v_value| > |r_value|, etc.) that don't hold when all variables in scope are similarly sized integers in [0, p). The proof spins on interval-tightening lemmas without ever extracting the modular conclusion. The author of propagate_quotients flagged this gap with the comment \"other division lemmas are possible\" preceding the fall-through \"no lemmas found\" CTRACE. This patch supplies one. Soundness --------- The lemma is sound regardless of v's LP bounds — the bound-negation disjuncts (v < 0) and (v ≥ M) make the disjunction unconditionally true under the polynomial identity, with v = target as the canonical residue in [0, M-1]. M is derived from the polynomial's coefficient gcd, not from any LP-side bound. Validated under smt.arith.validate=true on the mod-factor-propagation reproducers (PR #9235 follow-up), zk verifier benchmarks, and a broader QF_UFNIA sample — 50+ files total, zero validate_conflict() assertion violations. Performance ----------- A model-value gate (skip emission when v's current value already satisfies one of the disjuncts) prevents the pattern from short-circuiting the propagate_quotients || propagate_gcd_test || propagate_eqs || propagate_factorization || propagate_linear_equations chain with redundant emissions. Without the gate, a single (v, M, target) triple can re-emit each Grobner round and starve the downstream propagators — observed in regression testing as thousands of identical emissions on a small benchmark, turning a sub-second closure into a timeout. On six small mod-factor-propagation reproducers, the patch closes four cases that previously timed out at 30 s (~1 s typical under the Grobner-ramped config: smt.arith.nl.gr_q=50, smt.arith.nl.grobner_eqs_growth=50, smt.arith.nl.grobner_exp_delay=false, smt.arith.nl.grobner_frequency=1). The two remaining timeouts in that set are attributable to different gaps (Boolean-disjunction propagation, and the multi-bounded-mod-result polynomial shape that needs Grobner over Z/pZ), not to mod_residue itself. Diagnostics ----------- TRACE under the existing 'grobner' tag emits one line per lemma emission, recording v, M, c_v, c0, and target. --------- Co-authored-by: Claude Opus 4.7 (1M context) Co-authored-by: Nikolaj Bjorner --- src/math/lp/nla_grobner.cpp | 66 ++++++++++++++++++++++++++++++++++++- 1 file changed, 65 insertions(+), 1 deletion(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 19cb00c28..67e5a6050 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -386,6 +386,70 @@ namespace nla { nl_vars.insert(j); } + // mod_residue: derive v's residue mod M from polynomial divisibility. + // + // Common case. Given polynomial + // p = M*v1 + v - M*v2*v3 = 0, + // every monomial except v is M-divisible, so v ≡ 0 (mod M). + // Combined with 0 ≤ v < M, this forces v = 0. + // Emit: dependencies => (v < 0) ∨ (v ≥ M) ∨ (v = 0). + // + // General case. For a linear monomial c_v*v in p with c0 the constant + // term, require c_i/c_v integer for every non-v monomial and c0/c_v + // integer (call it K). Let M = gcd(|c_i/c_v|) over non-v monomials. + // Then p/c_v gives v + M*Q + K = 0 with Q integer, so v ≡ -K (mod M). + // With target = (-K) mod M ∈ [0, M-1], emit + // dependencies => (v < 0) ∨ (v ≥ M) ∨ (v = target). + for (auto const& mv : p) { + if (mv.vars.size() != 1) + continue; + lpvar vv = mv.vars[0]; + if (!c().var_is_int(vv)) + continue; + rational c_v = mv.coeff; + SASSERT(c_v != 0); + rational M(0); // 0 sentinel: "no non-v non-constant monomial seen yet". + rational c0(0); + bool ok = true; + for (auto const& mi : p) { + if (mi.vars.size() == 1 && mi.vars[0] == vv) + continue; // skip the mv monomial itself + if (mi.vars.empty()) { + c0 = mi.coeff; + continue; + } + rational quot = mi.coeff / c_v; + if (!quot.is_int()) { ok = false; break; } + rational a = abs(quot); + SASSERT(a != 0); + M = M == 0 ? a : gcd(M, a); + if (M == 1) { ok = false; break; } // trivial modulus, abort + } + if (!ok || M == 0) + continue; + rational K = c0 / c_v; + if (!K.is_int()) + continue; + rational target = mod(-K, M); // Euclidean: result in [0, M-1]. + SASSERT(target >= 0 && target < M); + // Skip if the lemma is already satisfied by the current model: + // any of (v < 0), (v ≥ M), (v = target) trivially holding means + // emission would be redundant. Without this guard, the lemma + // re-emits every Grobner round on the same polynomial. + rational v_val = c().val(vv); + if (v_val < 0 || v_val >= M || v_val == target) + continue; + lemma_builder lemma(c(), "grobner-mod-residue"); + add_dependencies(lemma, eq); + lemma |= ineq(vv, llc::LT, rational::zero()); + lemma |= ineq(vv, llc::GE, M); + lemma |= ineq(vv, llc::EQ, target); + TRACE(grobner, lemma.display(tout << "mod_residue v=" << vv + << " M=" << M << " c_v=" << c_v << " c0=" << c0 + << " target=" << target << "\n")); + return true; + } + bool found_lemma = false; for (auto v : nl_vars) { auto& m = p.manager(); @@ -613,7 +677,7 @@ namespace nla { for (auto* e : m_solver.equations()) { dd::pdd p = e->poly(); rational v = eval(p); - if (!v.is_zero()) { + if (v != 0) { out << p << " := " << v << "\n"; } }