mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-27 20:36:26 +00:00
Code Activity

nla_grobner: add mod_residue pattern to propagate_quotients (#9597)

Browse source 
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) <noreply@anthropic.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Arie 2026-05-26 21:12:38 -04:00 • committed by GitHub
parent ec25b6a185
commit 73151f1960
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 65 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

66
src/math/lp/nla_grobner.cpp
View file

@ -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";
}
}