nla_grobner: add mod_residue pattern to propagate_quotients

[1arie1]

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.

[Copilot]

Pull request overview

This PR extends Z3’s NLA Gröbner-based quotient propagation (nla::grobner::propagate_quotients) with a new “mod_residue” lemma pattern that detects when a linear integer variable’s value is determined modulo a computed gcd, and emits a disjunctive clause of the form (v < 0) ∨ (v ≥ M) ∨ (v = target) to enable bound-based refutations in the LP/SAT layers.

Changes:

• Add a new modular-residue detection pattern over integer polynomials in propagate_quotients, deriving v ≡ -K (mod M) from polynomial divisibility conditions.
• Emit a guarded disjunctive lemma encoding the residue class via two “out-of-range” disjuncts plus the canonical residue equality.
• Add tracing for the new lemma emissions under the existing grobner TRACE tag.

[NikolajBjorner]

Emit:

dependencies => (v < 0) ∨ (v ≥ M) ∨ (v = target).

[agurfinkel]

done

[NikolajBjorner]

you can just write v_val < 0

[agurfinkel]

done

[NikolajBjorner]

you can just write target >= 0, target == 0, etc

[agurfinkel]

done

[NikolajBjorner]

you can just write M == 0

[agurfinkel]

done

[NikolajBjorner]

M == 1

[agurfinkel]

done