From 2f48e355d848ac59915e85948c82afb9ca0bcf46 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Jul 2026 12:31:17 -0700 Subject: [PATCH] Add symbolic-modulus congruence rule to nla_divisions (#10119) Implement check_mod_congruence in nla_divisions: for two mod-atoms sharing a (possibly symbolic) divisor y, emit the model-guided tautology div(x,y) - div(s,y) = delta => mod(x,y) - mod(s,y) = (x - s) - delta*y. This discharges linear congruences over a symbolic modulus that the nonlinear core did not otherwise isolate. Thread the div(x,y) variable through add_divisibility (nla_core/nla_solver/nla_divisions) and register it in theory_lra for symbolic-divisor mod terms. Solves FStar.BitVector-1 (0.7s) and FStar.Matrix-1 (1.6s), previously 300s timeouts; all 92 unit tests pass. Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e --------- Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/math/lp/nla_core.h | 2 +- src/math/lp/nla_divisions.cpp | 66 ++++++++++++++++++++++++++++++++--- src/math/lp/nla_divisions.h | 7 ++-- src/math/lp/nla_solver.cpp | 4 +-- src/math/lp/nla_solver.h | 2 +- src/smt/theory_lra.cpp | 6 +++- 6 files changed, 74 insertions(+), 13 deletions(-) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index d87f5fe5c2..c4773ffa78 100644 --- a/src/math/lp/nla_core.h +++ b/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 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 9506d49697..c73795876e 100644 --- a/src/math/lp/nla_divisions.cpp +++ b/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) { - if (x == null_lpvar || y == null_lpvar || r == null_lpvar) + void divisions::add_divisibility(lpvar r, lpvar x, lpvar y, lpvar d) { + 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,59 @@ 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, "y != 0 & y = y2 & div(x,y) - div(s,y) = delta => mod(x,y) - mod(s,y) = (x - s) - delta*y"); + lemma |= ineq(y, llc::EQ, 0); // y = 0 (guard: mod/div uninterpreted when divisor is 0) + if (y2 != y) + lemma |= ineq(term(y, rational(-1), y2), llc::NE, 0); // y != y2 (guard: divisors must coincide symbolically) + 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; + } + } + } } diff --git a/src/math/lp/nla_divisions.h b/src/math/lp/nla_divisions.h index 0888cf0d51..3c687a0739 100644 --- a/src/math/lp/nla_divisions.h +++ b/src/math/lp/nla_divisions.h @@ -25,18 +25,19 @@ 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; + // divisibility facts (r, x, y, d) meaning r = mod(x, y) and d = div(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 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(); }; } diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 48b4c2a732..da1e1b3a95 100644 --- a/src/math/lp/nla_solver.cpp +++ b/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) { - m_core->add_divisibility(r, x, y); + void solver::add_divisibility(lpvar r, lpvar x, lpvar y, lpvar d) { + m_core->add_divisibility(r, x, y, d); } void solver::set_relevant(std::function& is_relevant) { diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 1470e67265..2e85bb18f4 100644 --- a/src/math/lp/nla_solver.h +++ b/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& is_relevant); void updt_params(params_ref const& p); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 6d5fdccb3b..ba1e0238c6 100644 --- a/src/smt/theory_lra.cpp +++ b/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)); } } }