mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-19 03:23:10 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Valentin Promies 2026-02-23 14:45:03 +01:00
parent 95afda383c
commit 3a995bbb0c
2 changed files with 22 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/nlsat/levelwise.cpp
View file

@ -999,11 +999,23 @@ namespace nlsat {
}
void mk_linear_poly_from_root(anum const& a, polynomial_ref& p) {
void add_linear_poly_from_root(anum const& a, bool lower, polynomial_ref& p) {
rational r;
m_am.to_rational(a, r);
p = m_pm.mk_polynomial(m_level);
p = denominator(r)*p - numerator(r);
if (lower) {
m_I[m_level].l = p;
m_I[m_level].l_index = 1;
} else {
m_I[m_level].u = p;
m_I[m_level].u_index = 1;
}
m_level_ps.push_back(p);
m_poly_has_roots.push_back(true);
polynomial_ref w = choose_nonzero_coeff(p, m_level);
m_witnesses.push_back(w);
}
// Ensure that the interval bounds will be described by linear polynomials.
@ -1016,17 +1028,12 @@ namespace nlsat {
auto& r = m_rel.m_rfunc;
if (m_I[m_level].is_section()) {
if (!m_am.is_rational(v)) {
// TODO: FAIL
NOT_IMPLEMENTED_YET();
}
else if (m_pm.total_degree(m_I[m_level].l) > 1) {
mk_linear_poly_from_root(v, p_lower);
// add p_lower and according i.r.e. to relevant places
m_I[m_level].l = p_lower;
m_I[m_level].l_index = 1;
m_level_ps.push_back(p_lower);
add_linear_poly_from_root(v, true, p_lower);
// update root function ordering
r.emplace((r.begin() + m_l_rf), m_am, p_lower, 1, v, m_level_ps.size()-1);
m_poly_has_roots.push_back(true);
}
return;
}
@ -1035,26 +1042,19 @@ namespace nlsat {
if (!m_I[m_level].l_inf() && m_pm.total_degree(m_I[m_level].l) > 1) {
scoped_anum between(m_am);
m_am.select(r[m_l_rf].val, v, between);
mk_linear_poly_from_root(between, p_lower);
// add p_lower and according i.r.e. to relevant places
m_I[m_level].l = p_lower;
m_I[m_level].l_index = 1;
m_level_ps.push_back(p_lower);
add_linear_poly_from_root(between, true, p_lower);
// update root function ordering
r.emplace((r.begin() + m_l_rf + 1), m_am, p_lower, 1, between, m_level_ps.size()-1);
m_poly_has_roots.push_back(true);
++m_l_rf;
++m_u_rf;
if (is_set(m_u_rf))
++m_u_rf;
}
if (!m_I[m_level].u_inf() && m_pm.total_degree(m_I[m_level].u) > 1) {
scoped_anum between(m_am);
m_am.select(v, r[m_u_rf].val, between);
mk_linear_poly_from_root(between, p_upper);
// add p_lower and according i.r.e. to relevant places
m_I[m_level].u = p_upper;
m_I[m_level].u_index = 1;
m_level_ps.push_back(p_lower);
// update root function ordering
add_linear_poly_from_root(between, false, p_upper);
r.emplace((r.begin() + m_u_rf), m_am, p_upper, 1, between, m_level_ps.size()-1);
m_poly_has_roots.push_back(true);
}
}

2
src/nlsat/nlsat_explain.cpp
View file

@ -1733,7 +1733,7 @@ namespace nlsat {
// We call levelwise directly without normalize, simplify, elim_vanishing to preserve the original polynomials
var max_x = max_var(m_ps);
bool levelwise_ok = levelwise_single_cell(m_ps, max_x, m_cache); // TODO: make lws call linear
bool levelwise_ok = levelwise_single_cell(m_ps, max_x, m_cache, true);
SASSERT(levelwise_ok);
m_solver.record_levelwise_result(levelwise_ok);