mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-05 03:26:45 +00:00
Code Activity

fix #8054

Browse source 
inherit denominators when evaluating polynomials
This commit is contained in:
Nikolaj Bjorner 2025-11-30 07:51:06 -08:00
parent 3712d1e0f1
commit a5488cf6e7
1 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -65,6 +65,7 @@ struct solver::imp {
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 v2 : m.vars()) {
den = lcm(denominators[v2], den);
polynomial_ref pw(definitions.get(v2), m_nlsat->pm()); polynomial_ref pw(definitions.get(v2), m_nlsat->pm());
if (!p) if (!p)
p = pw; p = pw;
@ -74,7 +75,7 @@ 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)) { for (auto const &[w, coeff] : lra.get_term(v)) {
den = lcm(denominator(coeff), den); den = lcm(denominators[w], lcm(denominator(coeff), den));
} }
for (auto const &[w, coeff] : lra.get_term(v)) { for (auto const &[w, coeff] : lra.get_term(v)) {
auto coeff1 = den * coeff; auto coeff1 = den * coeff;
@ -128,7 +129,7 @@ struct solver::imp {
poly = poly * constant(den * coeff / denominators[v]); poly = poly * constant(den * coeff / denominators[v]);
p = p + poly; p = p + poly;
} }
add_constraint(p, ci, k); add_constraint(p, ci, k);
} }
definitions.reset(); definitions.reset();
} }
@ -223,6 +224,7 @@ struct solver::imp {
for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";); for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";);
switch (r) { switch (r) {
case l_true: case l_true:
m_nlsat->restore_order();
m_nla_core.set_use_nra_model(true); m_nla_core.set_use_nra_model(true);
lra.init_model(); lra.init_model();
for (lp::constraint_index ci : lra.constraints().indices()) for (lp::constraint_index ci : lra.constraints().indices())
@ -427,6 +429,7 @@ struct solver::imp {
switch (r) { switch (r) {
case l_true: case l_true:
m_nlsat->restore_order();
m_nla_core.set_use_nra_model(true); m_nla_core.set_use_nra_model(true);
lra.init_model(); lra.init_model();
for (lp::constraint_index ci : lra.constraints().indices()) for (lp::constraint_index ci : lra.constraints().indices())
@ -628,9 +631,10 @@ struct solver::imp {
unsigned w; unsigned w;
scoped_anum a(am()); scoped_anum a(am());
for (unsigned v = m_values->size(); v < sz; ++v) { for (unsigned v = m_values->size(); v < sz; ++v) {
if (m_nla_core.emons().is_monic_var(v)) { if (m_nla_core.emons().is_monic_var(v)) {
am().set(a, 1); am().set(a, 1);
auto &m = m_nla_core.emon(v); auto &m = m_nla_core.emon(v);
for (auto x : m.vars()) for (auto x : m.vars())
am().mul(a, (*m_values)[x], a); am().mul(a, (*m_values)[x], a);
m_values->push_back(a); m_values->push_back(a);
@ -638,7 +642,7 @@ struct solver::imp {
else if (lra.column_has_term(v)) { else if (lra.column_has_term(v)) {
scoped_anum b(am()); scoped_anum b(am());
am().set(a, 0); am().set(a, 0);
for (auto const &[w, coeff] : lra.get_term(v)) { for (auto const &[w, coeff] : lra.get_term(v)) {
am().set(b, coeff.to_mpq()); am().set(b, coeff.to_mpq());
am().mul(b, (*m_values)[w], b); am().mul(b, (*m_values)[w], b);
am().add(a, b, a); am().add(a, b, a);