mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 11:35:42 +00:00
Code Activity

Add symbolic-modulus congruence rule to nla_divisions (#10119)

Browse source 
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>
This commit is contained in:
Nikolaj Bjorner 2026-07-14 12:31:17 -07:00 • committed by GitHub
parent 82a0d42970
commit 2f48e355d8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 74 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_core.h
View file

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

66
src/math/lp/nla_divisions.cpp
View file

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

7
src/math/lp/nla_divisions.h
View file

@ -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)
vector<std::tuple<lpvar, lpvar, lpvar>> m_divisibility;
// divisibility facts (r, x, y, d) meaning r = mod(x, y) and d = div(x, y)
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();
};
}

4
src/math/lp/nla_solver.cpp
View file

@ -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<bool(lpvar)>& is_relevant) {

2
src/math/lp/nla_solver.h
View file

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

6
src/smt/theory_lra.cpp
View file

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