diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index bf9252450a..d87f5fe5c2 100644 --- a/src/math/lp/nla_core.h +++ b/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 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 5b4501e4e0..9506d49697 100644 --- a/src/math/lp/nla_divisions.cpp +++ b/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; + } + } + } } diff --git a/src/math/lp/nla_divisions.h b/src/math/lp/nla_divisions.h index 96a50c05a8..0888cf0d51 100644 --- a/src/math/lp/nla_divisions.h +++ b/src/math/lp/nla_divisions.h @@ -25,14 +25,18 @@ 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; 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(); }; } diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 5621434595..48b4c2a732 100644 --- a/src/math/lp/nla_solver.cpp +++ b/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& is_relevant) { m_core->set_relevant(is_relevant); } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 36d136d38c..1470e67265 100644 --- a/src/math/lp/nla_solver.h +++ b/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& is_relevant); void updt_params(params_ref const& p); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4999dcd265..6d5fdccb3b 100644 --- a/src/smt/theory_lra.cpp +++ b/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);