Add linear divisibility closure lemma for lp/nla solver (#7464) (#10107)

## 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

@@ -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<lpvar(unsigned, lpvar const*)> 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; }
 

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;
+            }
+        }
+    }
 }

src/math/lp/nla_divisions.h

@@ -25,14 +25,18 @@ namespace nla {
         vector<std::tuple<lpvar, lpvar, lpvar, lpvar>> m_idivisions;
         vector<std::tuple<lpvar, lpvar, lpvar, lpvar>> m_rdivisions;
         vector<std::tuple<lpvar, lpvar, lpvar, lpvar>> m_bounded_divisions;
+        // divisibility facts (r, x, y) meaning r = mod(x, y)
+        vector<std::tuple<lpvar, lpvar, lpvar>> 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();
     };
 }

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<bool(lpvar)>& is_relevant) {
         m_core->set_relevant(is_relevant);
     }

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<bool(lpvar)>& is_relevant);
         void updt_params(params_ref const& p);

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);