From 7b26fe135a51e7dd9fecacf22386706c0e100c75 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Jul 2026 21:20:50 -0700 Subject: [PATCH] Add linear divisibility closure lemma for lp/nla solver (#7464) (#10107) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Fixes the divergence in issue #7464: formulas involving `mod`/`div` by a **variable** divisor could send `smt.arith.solver=6` into a non-terminating nonlinear search. Minimal reproducer (UNSAT, previously timed out; now solved in <0.5s): ```smt2 (declare-fun V () Int) (declare-fun n () Int) (declare-fun l () Int) (assert (and (> V 0) (= 0 (mod n 2)) (= (div n 2) (div n l)) (= 0 (mod (div n l) V)))) (assert (distinct 0 (mod n V))) (check-sat) ``` ## Root cause A variable-divisor `mod n V` is axiomatized by the Euclidean identity `n = V*(n div V) + (n mod V)`. The `V*(n div V)` term is nonlinear, so arith.solver=6 hands the problem to the nlsat/Gröbner branch, which branches on values of `V` with no termination bound and diverges. ## Fix Add a **linear divisibility closure** lemma in `nla_divisions`: > `mod(a, y) = 0 & x = c*a` (c an integer constant) ⟹ `mod(x, y) = 0`. The emitted clause ``` (x - c*a != 0) \/ (mod(a, y) != 0) \/ (mod(x, y) = 0) ``` is a **tautology for every integer `c`**, so mining a candidate `c = val(x)/val(a)` from the current model can never be unsound. It is only emitted when all three literals are false in the current model, so the clause is a genuine conflict/propagation and always makes progress. This lets the theory refute the instance directly instead of entering the divergent nonlinear branch. Variable-divisor `mod` terms were previously **not registered** in nla at all; they are now registered into a new `m_divisibility` list in `theory_lra`, so the reasoner can pair a violated `mod(x, y)` with a satisfied `mod(a, y)` of the same divisor. ## Changes - `src/math/lp/nla_divisions.{h,cpp}` — new `m_divisibility` list `{r=mod, x=dividend, y=divisor}`, `add_divisibility(...)`, and `check_linear_divisibility()`; invoked from `divisions::check()`. - `src/math/lp/nla_core.h`, `src/math/lp/nla_solver.{h,cpp}` — forwarding of `add_divisibility`. - `src/smt/theory_lra.cpp` — register variable-divisor `mod` into the divisibility list. ## Validation - `min.smt2` → `unsat` in 0.46s, minimized core → 0.15s (were timeouts). - Soundness: 350 differential fuzz formulas (arith.solver=6 vs arith.solver=2), **0 mismatches**. - Spot checks correct (divisor-3 variant → unsat; non-divisible variants → sat). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/nla_core.h | 1 + src/math/lp/nla_divisions.cpp | 55 +++++++++++++++++++++++++++++++++++ src/math/lp/nla_divisions.h | 4 +++ src/math/lp/nla_solver.cpp | 4 +++ src/math/lp/nla_solver.h | 1 + src/smt/theory_lra.cpp | 13 +++++++++ 6 files changed, 78 insertions(+) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index bf9252450a..d87f5fe5c2 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -218,6 +218,7 @@ public: void add_idivision(lpvar q, lpvar x, lpvar y, lpvar r) { m_divisions.add_idivision(q, x, y, r); } void add_rdivision(lpvar q, lpvar x, lpvar y, lpvar r) { m_divisions.add_rdivision(q, x, y, r); } void add_bounded_division(lpvar q, lpvar x, lpvar y, lpvar r) { m_divisions.add_bounded_division(q, x, y, r); } + void add_divisibility(lpvar r, lpvar x, lpvar y) { m_divisions.add_divisibility(r, x, y); } void set_add_mul_def_hook(std::function const& f) { m_add_mul_def_hook = f; } lpvar add_mul_def(unsigned sz, lpvar const* vs) { SASSERT(m_add_mul_def_hook); lpvar v = m_add_mul_def_hook(sz, vs); add_monic(v, sz, vs); return v; } diff --git a/src/math/lp/nla_divisions.cpp b/src/math/lp/nla_divisions.cpp index 5b4501e4e0..9506d49697 100644 --- a/src/math/lp/nla_divisions.cpp +++ b/src/math/lp/nla_divisions.cpp @@ -41,6 +41,13 @@ namespace nla { m_core.trail().push(push_back_vector(m_bounded_divisions)); } + void divisions::add_divisibility(lpvar r, lpvar x, lpvar y) { + if (x == null_lpvar || y == null_lpvar || r == null_lpvar) + return; + m_divisibility.push_back({ r, x, y }); + m_core.trail().push(push_back_vector(m_divisibility)); + } + typedef lp::lar_term term; // y1 >= y2 > 0 & x1 <= x2 => x1/y1 <= x2/y2 @@ -156,6 +163,7 @@ namespace nla { } check_mod_mult(); + check_linear_divisibility(); } // if p is bounded, q a value, r = eval(p): @@ -243,4 +251,51 @@ namespace nla { } } } + + // Linear divisibility closure: + // mod(a, y) = 0 & x = c * a (c an integer constant) => mod(x, y) = 0. + // The emitted clause + // (x - c*a != 0) \/ (mod(a, y) != 0) \/ (mod(x, y) = 0) + // is a tautology for every integer c (under the Euclidean semantics of mod), + // so the choice of c/a from the current model can never be unsound. We only + // emit it when all three literals are false in the current model, which makes + // the clause a real conflict/propagation and guarantees progress. + void divisions::check_linear_divisibility() { + core& c = m_core; + unsigned sz = m_divisibility.size(); + for (unsigned i = 0; i < sz; ++i) { + auto const& [rx, x, y] = m_divisibility[i]; + if (!c.is_relevant(rx)) + continue; + if (c.val(rx).is_zero()) // mod(x, y) already 0 in model: nothing to refute + continue; + auto xval = c.val(x); + if (xval.is_zero()) + continue; + for (unsigned j = 0; j < sz; ++j) { + if (i == j) + continue; + auto const& [ra, a, y2] = m_divisibility[j]; + if (y2 != y && c.val(y2) != c.val(y)) // same divisor (by column or value) + continue; + if (!c.is_relevant(ra)) + continue; + if (!c.val(ra).is_zero()) // need mod(a, y) = 0 in model + continue; + auto aval = c.val(a); + if (aval.is_zero()) + continue; + rational cc = xval / aval; + if (!cc.is_int() || cc.is_zero()) + continue; + if (xval != cc * aval) // ensure x = c*a holds exactly in the model + continue; + lemma_builder lemma(c, "mod(a,y) = 0 & x = c*a => mod(x,y) = 0"); + lemma |= ineq(term(x, -cc, a), llc::NE, 0); // x - c*a != 0 + lemma |= ineq(ra, llc::NE, 0); // mod(a, y) != 0 + lemma |= ineq(rx, llc::EQ, 0); // mod(x, y) = 0 + return; + } + } + } } diff --git a/src/math/lp/nla_divisions.h b/src/math/lp/nla_divisions.h index 96a50c05a8..0888cf0d51 100644 --- a/src/math/lp/nla_divisions.h +++ b/src/math/lp/nla_divisions.h @@ -25,14 +25,18 @@ namespace nla { vector> m_idivisions; vector> m_rdivisions; vector> m_bounded_divisions; + // divisibility facts (r, x, y) meaning r = mod(x, y) + vector> m_divisibility; public: divisions(core& c):m_core(c) {} void add_idivision(lpvar q, lpvar x, lpvar y, lpvar r); void add_rdivision(lpvar q, lpvar x, lpvar y, lpvar r); void add_bounded_division(lpvar q, lpvar x, lpvar y, lpvar r); + void add_divisibility(lpvar r, lpvar x, lpvar y); void check(); void check_bounded_divisions(); void check_mod_mult(); + void check_linear_divisibility(); }; } diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 5621434595..48b4c2a732 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -32,6 +32,10 @@ namespace nla { m_core->add_bounded_division(q, x, y, r); } + void solver::add_divisibility(lpvar r, lpvar x, lpvar y) { + m_core->add_divisibility(r, x, y); + } + void solver::set_relevant(std::function& is_relevant) { m_core->set_relevant(is_relevant); } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 36d136d38c..1470e67265 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -31,6 +31,7 @@ namespace nla { void add_idivision(lpvar q, lpvar x, lpvar y, lpvar r); void add_rdivision(lpvar q, lpvar x, lpvar y, lpvar r); void add_bounded_division(lpvar q, lpvar x, lpvar y, lpvar r); + void add_divisibility(lpvar r, lpvar x, lpvar y); void check_bounded_divisions(); void set_relevant(std::function& is_relevant); void updt_params(params_ref const& p); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4999dcd265..6d5fdccb3b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -485,6 +485,19 @@ class theory_lra::imp { theory_var rv = mk_var(n); m_nla->add_bounded_division(register_theory_var_in_lar_solver(q), register_theory_var_in_lar_solver(x), register_theory_var_in_lar_solver(y), register_theory_var_in_lar_solver(rv)); } + if (!a.is_numeral(n2) && is_app(n1) && is_app(n2)) { + // register mod(x, y) with variable divisor for divisibility reasoning + ensure_nla(); + if (m_nla) { + internalize_term(to_app(n1)); + internalize_term(to_app(n2)); + internalize_term(t); + theory_var x = mk_var(n1); + theory_var y = mk_var(n2); + theory_var rv = mk_var(n); + m_nla->add_divisibility(register_theory_var_in_lar_solver(rv), register_theory_var_in_lar_solver(x), register_theory_var_in_lar_solver(y)); + } + } } else if (a.is_rem(n, n1, n2)) { if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);