mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 18:40:51 +00:00
Code Activity

add parameter to suppress/enable levelwise

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-03 12:54:53 -07:00
parent 1ff8cc24c8
commit 5ac4b8d06d
4 changed files with 14 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/nlsat/nlsat_explain.cpp
View file

@ -1160,8 +1160,10 @@ namespace nlsat {
var x = m_todo.extract_max_polys(ps);
if (!levelwise_single_cell(ps, max_x)) { // on levelwise_single_cell failure continue with cdcac
polynomial_ref_vector samples(m_pm);
if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x))
return;
polynomial_ref_vector samples(m_pm);
polynomial_ref_vector samples(m_pm);
if (x < max_x)
@ -1706,9 +1708,10 @@ namespace nlsat {
SASSERT(check_already_added());
SASSERT(num > 0);
TRACE(nlsat_explain,
tout << "[explain] set of literals is infeasible in the current interpretation\n";
tout << "the infeasible clause:\n";
display(tout, m_solver, num, ls) << "\n";
m_solver.display_assignment(tout);
m_solver.display_assignment(tout << "assignment:\n");
);
if (max_var(num, ls) == 0 && !m_assignment.is_assigned(0)) {
TRACE(nlsat_explain, tout << "all literals use unassigned max var; returning justification\n";);