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

Formulas with mod/div by a variable divisor (e.g. mod(n,V)) were axiomatized
via the Euclidean identity n = V*(n div V) + (n mod V), whose nonlinear
V*(n div V) term is handed to the nlsat/Grobner branch, which can diverge.

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 c from the current model is
always sound; it is only emitted when all three literals are false in the
model, making it a real conflict/propagation that guarantees progress.

Variable-divisor mod terms, previously unregistered in nla, 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.

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