mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 22:27:48 +00:00
Code Activity

fix #8099 (again)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-12-25 13:52:54 -08:00
parent ce2405aab6
commit c12425c86f
1 changed files with 21 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -64,9 +64,9 @@ struct solver::imp {
rational den(1); rational den(1);
if (m_nla_core.emons().is_monic_var(v)) { if (m_nla_core.emons().is_monic_var(v)) {
auto const &m = m_nla_core.emons()[v]; auto const &m = m_nla_core.emons()[v];
for (auto v2 : m.vars()) { for (auto w : m.vars()) {
den = denominators[v2] * den; den = denominators[w] * den;
polynomial_ref pw(definitions.get(v2), m_nlsat->pm()); polynomial_ref pw(definitions.get(w), m_nlsat->pm());
if (!p) if (!p)
p = pw; p = pw;
else else
@ -74,11 +74,10 @@ struct solver::imp {
} }
} }
else if (lra.column_has_term(v)) { else if (lra.column_has_term(v)) {
for (auto const &[w, coeff] : lra.get_term(v))
den = lcm(denominator(coeff / denominators[w]), den);
for (auto const &[w, coeff] : lra.get_term(v)) { for (auto const &[w, coeff] : lra.get_term(v)) {
den = lcm(denominators[w], lcm(denominator(coeff), den)); auto coeff1 = den * coeff / denominators[w];
}
for (auto const &[w, coeff] : lra.get_term(v)) {
auto coeff1 = den * coeff;
polynomial_ref pw(definitions.get(w), m_nlsat->pm()); polynomial_ref pw(definitions.get(w), m_nlsat->pm());
if (!p) if (!p)
p = constant(coeff1) * pw; p = constant(coeff1) * pw;
@ -118,8 +117,19 @@ struct solver::imp {
auto rhs = c.rhs(); auto rhs = c.rhs();
auto lhs = c.coeffs(); auto lhs = c.coeffs();
rational den = denominator(rhs); rational den = denominator(rhs);
//
// let v := p / denominators[v]
//
// sum(coeff[v] * v) k rhs
// ==
// sum(coeff[v] * (p / denominators[v])) k rhs
// ==
// sum((coeff[v] / denominators[v]) * p) k rhs
//
for (auto [coeff, v] : lhs) for (auto [coeff, v] : lhs)
den = lcm(lcm(den, denominator(coeff)), denominators[v]); den = lcm(den, denominator(coeff / denominators[v]));
polynomial::polynomial_ref p(pm); polynomial::polynomial_ref p(pm);
p = pm.mk_const(-den * rhs); p = pm.mk_const(-den * rhs);
@ -130,6 +140,8 @@ struct solver::imp {
p = p + poly; p = p + poly;
} }
add_constraint(p, ci, k); add_constraint(p, ci, k);
TRACE(nra, tout << "constraint " << ci << ": " << p << " " << k << " 0\n";
lra.constraints().display(tout, ci) << "\n");
} }
definitions.reset(); definitions.reset();
} }
@ -182,7 +194,7 @@ struct solver::imp {
smt_params_helper p(m_params); smt_params_helper p(m_params);
setup_solver_poly(); setup_solver_poly();
TRACE(nra, m_nlsat->display(tout)); TRACE(nra, m_nlsat->display(tout));