mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Iss9139 fix (#9577)

Browse source 
Preserve the de-linearization of the linear constraints but fixing the
den bug. @ValentinPromies, that is what you had in mind.

---------

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-05-21 06:33:14 -07:00 • committed by GitHub
parent 8e3be3ad1f
commit 43791ebf2a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 45 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

91
src/math/lp/nra_solver.cpp
View file

@ -64,8 +64,10 @@ struct solver::imp {
m_lp2nl.reset();
}
// Create polynomial definition for variable v used in setup_assignment_solver.
// Side-effects: updates m_vars2mon when v is a monic variable.
// Create polynomial definition for variable v used in setup_solver_poly.
// The definition recursively expands monic and term variables into
// polynomials in leaf variables, scaled by an integer denominator
// tracked in `denominators` to keep the coefficients integral.
void mk_definition(unsigned v, polynomial_ref_vector &definitions, vector<rational>& denominators) {
auto &pm = m_nlsat->pm();
polynomial::polynomial_ref p(pm);
@ -100,44 +102,6 @@ struct solver::imp {
denominators.push_back(den);
}
// Create polynomial definition for variable v used in setup_assignment_solver.
// Side-effects: updates m_vars2mon when v is a monic variable.
void mk_definition_assignment(unsigned v, polynomial_ref_vector &definitions) {
auto &pm = m_nlsat->pm();
polynomial::polynomial_ref p(pm);
if (m_nla_core.emons().is_monic_var(v)) {
auto const &m = m_nla_core.emons()[v];
auto vars = m.vars();
std::sort(vars.begin(), vars.end());
m_vars2mon.insert(vars, v);
for (auto v2 : vars) {
auto pv = definitions.get(v2);
if (!p)
p = pv;
else
p = pm.mul(p, pv);
}
}
else if (lra.column_has_term(v)) {
rational den(1);
for (auto const& [w, coeff] : lra.get_term(v))
den = lcm(den, denominator(coeff));
for (auto const& [w, coeff] : lra.get_term(v)) {
auto pw = definitions.get(w);
polynomial::polynomial_ref term(pm);
term = pm.mul(den * coeff, pw);
if (!p)
p = term;
else
p = pm.add(p, term);
}
}
else {
p = pm.mk_polynomial(lp2nl(v));
}
definitions.push_back(p);
}
void setup_solver_poly() {
m_coi.init();
auto &pm = m_nlsat->pm();
@ -318,6 +282,24 @@ struct solver::imp {
m_coi.init();
auto &pm = m_nlsat->pm();
polynomial_ref_vector definitions(pm);
vector<rational> denominators;
// Create an NLSAT polyvar for each LRA variable (identity mapping),
// seed the assignment from the current LRA model, populate
// m_vars2mon, and build the inlined polynomial definition of v.
//
// The definition expands monic and term variables into polynomials
// over leaf variables. Each definition is scaled by denominators[v]
// so that all coefficients stay integral; the scaling cancels on
// both sides of every constraint we build below (just like in
// setup_solver_poly).
//
// This "de-linearized" representation is what the linear-cell
// construction in NLSAT needs: a cell built around a constraint
// polynomial that mentions several multiplications at once can
// yield a lemma constraining all of them simultaneously, which is
// strictly stronger than the per-multiplication lemmas we would
// get from asserting `v_mon - v1*...*vk = 0` separately.
for (unsigned v = 0; v < lra.number_of_vars(); ++v) {
auto j = m_nlsat->mk_var(lra.var_is_int(v));
VERIFY(j == v);
@ -325,29 +307,47 @@ struct solver::imp {
scoped_anum a(am());
am().set(a, m_nla_core.val(v).to_mpq());
m_values->push_back(a);
mk_definition_assignment(v, definitions);
if (m_nla_core.emons().is_monic_var(v)) {
auto const &m = m_nla_core.emons()[v];
auto vars = m.vars();
std::sort(vars.begin(), vars.end());
m_vars2mon.insert(vars, v);
}
mk_definition(v, definitions, denominators);
}
// Substitute each variable in the LRA constraint by its definition
// and rescale to keep integer coefficients. Symbolically:
//
// v == definitions[v] / denominators[v]
//
// sum(coeff_v * v) k rhs
// == sum((coeff_v / denominators[v]) * definitions[v]) k rhs
//
// We pick den := lcm of all denominators(coeff_v / denominators[v])
// together with denominator(rhs), so that den * coeff_v / denominators[v]
// and den * rhs are all integers. The relation kind k is preserved
// because den > 0.
for (auto ci : m_coi.constraints()) {
auto &c = lra.constraints()[ci];
auto &pm = m_nlsat->pm();
auto k = c.kind();
auto rhs = c.rhs();
auto lhs = c.coeffs();
rational den = denominator(rhs);
for (auto [coeff, v] : lhs)
den = lcm(den, denominator(coeff));
den = lcm(den, denominator(coeff / denominators[v]));
polynomial::polynomial_ref p(pm);
p = pm.mk_const(-den * rhs);
for (auto [coeff, v] : lhs) {
polynomial_ref poly(pm);
poly = pm.mul(den * coeff, definitions.get(v));
poly = definitions.get(v);
poly = poly * constant(den * coeff / denominators[v]);
p = p + poly;
}
auto lit = add_constraint(p, ci, k);
m_literal2constraint.setx(lit.index(), ci, lp::null_ci);
}
definitions.reset();
}
void process_polynomial_check_assignment(polynomial::polynomial const* p, rational& bound, const u_map<lp::lpvar>& nl2lp, lp::lar_term& t) {
@ -428,7 +428,6 @@ struct solver::imp {
lbool add_lemma(nlsat::literal_vector const &clause) {
u_map<lp::lpvar> nl2lp = reverse_lp2nl();
polynomial::manager &pm = m_nlsat->pm();
lbool result = l_false;
{
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);