mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-24 19:14:00 +00:00
Code Activity

call levelwise on a correct set of polynomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-04 16:55:49 -10:00
parent fc11b7cb9e
commit 230ee01fe2
2 changed files with 12 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/nlsat/nlsat_explain.cpp
View file

@ -1129,7 +1129,7 @@ namespace nlsat {
bool first = true;
if (ps.empty())
return;
TRACE(nlsat_explain, ::nlsat::display(tout << "ps:", m_solver, ps)<< "\n";);
m_todo.reset();
for (unsigned i = 0; i < ps.size(); i++) {
polynomial_ref p(m_pm);
@ -1140,19 +1140,18 @@ namespace nlsat {
ps.reset();
for (auto p: m_todo.m_set)
ps.push_back(p);
var x = m_todo.extract_max_polys(ps);
TRACE(nlsat_explain, tout << "m_solver.apply_levelwise():" << m_solver.apply_levelwise() << "\n";);
if (m_solver.apply_levelwise()) {
bool levelwise_ok = levelwise_single_cell(ps, max_x, m_cache);
m_solver.record_levelwise_result(levelwise_ok);
if (levelwise_ok)
return;
}
TRACE(nlsat_explain, ::nlsat::display(tout << "ps before extract:", m_solver, ps)<< "\n";);
var x = m_todo.extract_max_polys(ps);
TRACE(nlsat_explain, ::nlsat::display(tout << "ps:", m_solver, ps)<< "\n";);
polynomial_ref_vector samples(m_pm);
if (x < max_x)
cac_add_cell_lits(ps, x, samples);