mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

remove a parameter

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-27 07:22:33 -08:00
parent 204560288e
commit 25d0386ade
1 changed files with 3 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/nlsat/nlsat_explain.cpp
View file

@ -943,8 +943,7 @@ namespace nlsat {
add_simple_assumption(k, p, lsign); add_simple_assumption(k, p, lsign);
} }
void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) { void cac_add_cell_lits(polynomial_ref_vector & ps, var y) {
res.reset();
SASSERT(sample().is_assigned(y)); SASSERT(sample().is_assigned(y));
bool lower_inf = true; bool lower_inf = true;
bool upper_inf = true; bool upper_inf = true;
@ -986,7 +985,6 @@ namespace nlsat {
// add literal // add literal
// ! (y = root_i(p)) // ! (y = root_i(p))
add_root_literal(atom::ROOT_EQ, y, i+1, p); add_root_literal(atom::ROOT_EQ, y, i+1, p);
res.push_back(p);
return; return;
} }
else if (s < 0) { else if (s < 0) {
@ -1023,11 +1021,9 @@ namespace nlsat {
} }
if (!lower_inf) { if (!lower_inf) {
res.push_back(p_lower);
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower); add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
} }
if (!upper_inf) { if (!upper_inf) {
res.push_back(p_upper);
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper); add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper);
} }
} }
@ -1206,13 +1202,12 @@ namespace nlsat {
var x = m_todo.extract_max_polys(ps); var x = m_todo.extract_max_polys(ps);
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
polynomial_ref_vector samples(m_pm);
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am); levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am);
auto cell = lws.single_cell(); auto cell = lws.single_cell();
TRACE(lws, for (unsigned i = 0; i < cell.size(); i++) TRACE(lws, for (unsigned i = 0; i < cell.size(); i++)
display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";); display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";);
if (x < max_x) if (x < max_x)
cac_add_cell_lits(ps, x, samples); cac_add_cell_lits(ps, x);
while (true) { while (true) {
if (all_univ(ps, x) && m_todo.empty()) { if (all_univ(ps, x) && m_todo.empty()) {
@ -1228,7 +1223,7 @@ namespace nlsat {
if (m_todo.empty()) if (m_todo.empty())
break; break;
x = m_todo.extract_max_polys(ps); x = m_todo.extract_max_polys(ps);
cac_add_cell_lits(ps, x, samples); cac_add_cell_lits(ps, x);
} }
} }