mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 13:39:28 +00:00
Code Activity

fix linear projection

Browse source
This commit is contained in:
Valentin Promies 2025-08-21 14:52:06 +02:00
parent 6ef8a0b7bb
commit d05961a021
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_explain.cpp
View file

@ -1424,7 +1424,7 @@ namespace nlsat {
polynomial_ref_vector ps_above_sample(m_pm); polynomial_ref_vector ps_above_sample(m_pm);
polynomial_ref_vector ps_equal_sample(m_pm); polynomial_ref_vector ps_equal_sample(m_pm);
var x = m_todo.extract_max_polys(ps); var x = m_todo.extract_max_polys(ps);
if (x == max_x) { if (!m_assignment.is_assigned(x)) {
// top level projection like original // top level projection like original
// we could also do a covering-style projection, sparing some resultants // we could also do a covering-style projection, sparing some resultants
add_lcs(ps, x); add_lcs(ps, x);
@ -1433,7 +1433,7 @@ namespace nlsat {
x = m_todo.extract_max_polys(ps); x = m_todo.extract_max_polys(ps);
} }
while (!m_todo.empty()) { while (true) {
add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample); add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample);
if (all_univ(ps, x) && m_todo.empty()) { if (all_univ(ps, x) && m_todo.empty()) {
m_todo.reset(); m_todo.reset();
@ -1463,6 +1463,8 @@ namespace nlsat {
} }
} }
} }
if (m_todo.empty())
break;
x = m_todo.extract_max_polys(ps); x = m_todo.extract_max_polys(ps);
} }
} }