Merge 9264c9cc26 into c4cb5bbc15

src/math/lp/nla_core.h

@@ -218,7 +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 add_divisibility(lpvar r, lpvar x, lpvar y, lpvar d) { m_divisions.add_divisibility(r, x, y, d); }
     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,10 +41,10 @@ namespace nla {
         m_core.trail().push(push_back_vector(m_bounded_divisions));
     }
 
-    void divisions::add_divisibility(lpvar r, lpvar x, lpvar y) {
+    void divisions::add_divisibility(lpvar r, lpvar x, lpvar y, lpvar d) {
-        if (x == null_lpvar || y == null_lpvar || r == null_lpvar)
+        if (x == null_lpvar || y == null_lpvar || r == null_lpvar || d == null_lpvar)
             return;
-        m_divisibility.push_back({ r, x, y });
+        m_divisibility.push_back({ r, x, y, d });
         m_core.trail().push(push_back_vector(m_divisibility));
     }
 
@@ -164,6 +164,7 @@ namespace nla {
 
         check_mod_mult();
         check_linear_divisibility();
+        check_mod_congruence();
     }
 
     // if p is bounded, q a value, r = eval(p):
@@ -264,7 +265,7 @@ namespace nla {
         core& c = m_core;
         unsigned sz = m_divisibility.size();
         for (unsigned i = 0; i < sz; ++i) {
-            auto const& [rx, x, y] = m_divisibility[i];
+            auto const& [rx, x, y, dx] = 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
@@ -275,7 +276,7 @@ namespace nla {
             for (unsigned j = 0; j < sz; ++j) {
                 if (i == j)
                     continue;
-                auto const& [ra, a, y2] = m_divisibility[j];
+                auto const& [ra, a, y2, da] = m_divisibility[j];
                 if (y2 != y && c.val(y2) != c.val(y)) // same divisor (by column or value)
                     continue;
                 if (!c.is_relevant(ra))
@@ -298,4 +299,56 @@ namespace nla {
             }
         }
     }
+
+    // Modular congruence over a shared (possibly symbolic) divisor.
+    //
+    // For each divisibility fact we have the Euclidean identities (asserted by
+    // theory_lra::mk_idiv_mod_axioms):
+    //      x = y * div(x,y) + mod(x,y),   0 <= mod(x,y) < |y|.
+    // For two facts (rx = mod(x,y), dx = div(x,y)) and (rs = mod(s,y), ds = div(s,y))
+    // sharing divisor y, subtracting the identities gives, for every integer delta,
+    //      div(x,y) - div(s,y) = delta   =>   mod(x,y) - mod(s,y) = (x - s) - delta*y.
+    // This is a tautology (entailed by the two identities) for any fixed integer
+    // delta, so choosing delta from the current model can never be unsound. We emit
+    // the clause
+    //      (div(x,y) - div(s,y) != delta) \/ (mod(x,y) - mod(s,y) - (x - s) + delta*y = 0)
+    // only when the equality literal is false in the model (delta taken as the model
+    // value of div(x,y) - div(s,y)), which makes the clause a real propagation and
+    // guarantees progress. This discharges linear congruences with a symbolic
+    // modulus (e.g. mod(i + s, n) = i + mod(s, n)) that the nonlinear core does not
+    // otherwise isolate.
+    void divisions::check_mod_congruence() {
+        core& c = m_core;
+        unsigned sz = m_divisibility.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            auto const& [rx, x, y, dx] = m_divisibility[i];
+            if (!c.is_relevant(rx))
+                continue;
+            auto yval = c.val(y);
+            if (yval.is_zero())   // mod/div uninterpreted when the divisor is 0
+                continue;
+            for (unsigned j = i + 1; j < sz; ++j) {
+                auto const& [rs, s, y2, ds] = m_divisibility[j];
+                if (!c.is_relevant(rs))
+                    continue;
+                if (y2 != y && c.val(y2) != yval) // same divisor (by column or value)
+                    continue;
+                rational delta = c.val(dx) - c.val(ds);
+                rational lhs = c.val(rx) - c.val(rs);
+                rational rhs = (c.val(x) - c.val(s)) - delta * yval;
+                if (lhs == rhs)   // residue equation already holds: nothing to propagate
+                    continue;
+                lemma_builder lemma(c, "div(x,y) - div(s,y) = delta => mod(x,y) - mod(s,y) = (x - s) - delta*y");
+                lemma |= ineq(term(dx, rational(-1), ds), llc::NE, delta); // div(x,y) - div(s,y) != delta
+                term t;
+                t.add_monomial(rational::one(), rx);
+                t.add_monomial(rational(-1), rs);
+                t.add_monomial(rational(-1), x);
+                t.add_monomial(rational::one(), s);
+                t.add_monomial(delta, y);
+                lemma |= ineq(t, llc::EQ, 0); // mod(x,y) - mod(s,y) - x + s + delta*y = 0
+                return;
+            }
+        }
+    }
 }

src/math/lp/nla_divisions.h

@@ -25,18 +25,19 @@ 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)
+        // divisibility facts (r, x, y, d) meaning r = mod(x, y) and d = div(x, y)
-        vector<std::tuple<lpvar, lpvar, lpvar>> m_divisibility;
+        vector<std::tuple<lpvar, 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 add_divisibility(lpvar r, lpvar x, lpvar y, lpvar d);
         void check();
         void check_bounded_divisions();
         void check_mod_mult();
         void check_linear_divisibility();
+        void check_mod_congruence();
     };
 }

src/math/lp/nla_solver.cpp

@@ -32,8 +32,8 @@ namespace nla {
         m_core->add_bounded_division(q, x, y, r);
     }
 
-    void solver::add_divisibility(lpvar r, lpvar x, lpvar y) {
+    void solver::add_divisibility(lpvar r, lpvar x, lpvar y, lpvar d) {
-        m_core->add_divisibility(r, x, y);
+        m_core->add_divisibility(r, x, y, d);
     }
 
     void solver::set_relevant(std::function<bool(lpvar)>& is_relevant) {

src/math/lp/nla_solver.h

@@ -31,7 +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 add_divisibility(lpvar r, lpvar x, lpvar y, lpvar d);
         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

@@ -489,13 +489,17 @@ class theory_lra::imp {
                         // register mod(x, y) with variable divisor for divisibility reasoning
                         ensure_nla();
                         if (m_nla) {
+                            app_ref div(a.mk_idiv(n1, n2), m);
+                            ctx().internalize(div, false);
+                            internalize_term(to_app(div));
                             internalize_term(to_app(n1));
                             internalize_term(to_app(n2));
                             internalize_term(t);
+                            theory_var d = mk_var(div);
                             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));
+                            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), register_theory_var_in_lar_solver(d));
                         }
                     }
                 }