From 2a6661846c8db34cc1f7efa928211e5fa240717f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 3 Dec 2025 11:56:07 -1000 Subject: [PATCH] rebase with master Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 71 +++++++++++++++++++------------------ src/nlsat/nlsat_params.pyg | 4 +-- src/nlsat/nlsat_solver.cpp | 2 +- src/test/nlsat.cpp | 2 +- src/util/trace_tags.def | 1 - 5 files changed, 41 insertions(+), 39 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 7ff333cb7..fdf2c1d51 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -269,14 +269,14 @@ namespace nlsat { void find_cell_roots(polynomial_ref_vector & ps, var y, cell_root_info & info) { info.reset(); - SASSERT(m_assignment.is_assigned(y)); + SASSERT(m_solver.sample().is_assigned(y)); bool lower_inf = true; bool upper_inf = true; scoped_anum_vector & roots = m_roots_tmp; scoped_anum lower(m_am); scoped_anum upper(m_am); - anum const & y_val = m_assignment.value(y); - TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, y); tout << " -> "; + anum const & y_val = m_solver.sample().value(y); + TRACE(nlsat_explain, tout << "adding literals for "; m_solver.display_var(tout, y); tout << " -> "; m_am.display_decimal(tout, y_val); tout << "\n";); polynomial_ref p(m_pm); unsigned sz = ps.size(); @@ -285,12 +285,12 @@ namespace nlsat { if (max_var(p) != y) continue; roots.reset(); - // Variable y is assigned in m_assignment. We must temporarily unassign it. + // Variable y is assigned in m_solver.sample(). We must temporarily unassign it. // Otherwise, the isolate_roots procedure will assume p is a constant polynomial. - m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots); + m_am.isolate_roots(p, undef_var_assignment(m_solver.sample(), y), roots); unsigned num_roots = roots.size(); TRACE(nlsat_explain, - tout << "isolated roots for "; display_var(tout, y); + tout << "isolated roots for "; m_solver.display_var(tout, y); tout << " with polynomial: " << p << "\n"; for (unsigned ri = 0; ri < num_roots; ++ri) { m_am.display_decimal(tout << " root[" << (ri+1) << "] = ", roots[ri]); @@ -349,6 +349,11 @@ namespace nlsat { } } + ::sign sign(polynomial_ref const & p) { + return ::nlsat::sign(p, m_solver.sample(), m_am); + } + + void add_zero_assumption(polynomial_ref& p) { // Build a square-free representative of p so that we can speak about // a specific root that coincides with the current assignment. @@ -363,7 +368,7 @@ namespace nlsat { SASSERT(maxx != null_var); if (maxx == null_var) return; - SASSERT(m_assignment.is_assigned(maxx)); + SASSERT(m_solver.sample().is_assigned(maxx)); polynomial_ref_vector singleton(m_pm); singleton.push_back(q); @@ -374,7 +379,7 @@ namespace nlsat { TRACE(nlsat_explain, tout << "adding zero-assumption root literal for "; - display_var(tout, maxx); tout << " using root[" << info.m_eq_idx << "] of " << q << "\n";); + m_solver.display_var(tout, maxx); tout << " using root[" << info.m_eq_idx << "] of " << q << "\n";); add_root_literal(atom::ROOT_EQ, maxx, info.m_eq_idx, info.m_eq); } @@ -505,7 +510,7 @@ namespace nlsat { if (max_var(p) == max) elim_vanishing(p); // eliminate vanishing coefficients of max if (is_const(p) || max_var(p) < max) { - int s = sign(p, m_solver.sample(), m_am); + int s = sign(p); if (!is_const(p)) { SASSERT(max_var(p) != null_var); SASSERT(max_var(p) < max); @@ -701,7 +706,7 @@ namespace nlsat { unsigned k_deg = m_pm.degree(p, x); if (k_deg == 0) continue; // p depends on x - TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p) << "\n";); + TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; m_solver.display(tout, p) << "\n";); for (int j_coeff_deg = k_deg; j_coeff_deg >= 0; j_coeff_deg--) { coeff = m_pm.coeff(p, x, j_coeff_deg); TRACE(nlsat_explain, tout << " coeff deg " << j_coeff_deg << ": "; display(tout, m_solver, coeff) << "\n";); @@ -751,7 +756,7 @@ namespace nlsat { auto c = polynomial_ref(this->m_pm); for (unsigned j = 0; j <= n; j++) { c = m_pm.coeff(s, x, j); - SASSERT(sign(c, sample(), m_am) == 0); + SASSERT(sign(c) == 0); ensure_sign(c); } return true; @@ -887,7 +892,7 @@ namespace nlsat { } polynomial_ref c(m_pm); c = m_pm.coeff(p, y, 1); - int s = sign(c, sample(), m_am); + int s = sign(c); if (s == 0) { return false; } @@ -965,7 +970,7 @@ namespace nlsat { */ void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) { - TRACE(nlsat_explain, display_var(tout, m_solver, y); m_pm.display(tout << ": ", p, m_solver.display_proc()); tout << "\n"); + TRACE(nlsat_explain, m_solver.display_var(tout, y); m_pm.display(tout << ": ", p, m_solver.display_proc()); tout << "\n"); polynomial_ref p_prime(m_pm); p_prime = p; bool lsign = false; @@ -1072,7 +1077,7 @@ namespace nlsat { m_todo.reset(); break; } - TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, m_solver, x); + TRACE(nlsat_explain, tout << "project loop, processing var "; m_solver.display_var(tout, x); tout << "\npolynomials\n"; display(tout, m_solver, ps); tout << "\n";); add_lcs(ps, x); @@ -1124,7 +1129,6 @@ namespace nlsat { bool first = true; if (ps.empty()) return; - } m_todo.reset(); for (unsigned i = 0; i < ps.size(); i++) { @@ -1147,17 +1151,16 @@ namespace nlsat { std::cout << "f"; polynomial_ref_vector samples(m_pm); - polynomial_ref_vector samples(m_pm); if (x < max_x) - cac_add_cell_lits(ps, x); + cac_add_cell_lits(ps, x, samples); while (true) { if (all_univ(ps, x) && m_todo.empty()) { m_todo.reset(); break; } - TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; - display(tout, ps); tout << "\n";); + TRACE(nlsat_explain, tout << "project loop, processing var "; m_solver.display_var(tout, x); tout << "\npolynomials\n"; + display(tout, m_solver, ps); tout << "\n";); if (first) { // The first run is special because x is not constrained by the sample, we cannot surround it by the root functions. // we make the polynomials in ps delinable add_lcs(ps, x); @@ -1174,7 +1177,7 @@ namespace nlsat { if (m_todo.empty()) break; x = m_todo.extract_max_polys(ps); - cac_add_cell_lits(ps, x); + cac_add_cell_lits(ps, x, samples); } } @@ -1309,7 +1312,7 @@ namespace nlsat { } if (is_const(new_factor)) { TRACE(nlsat_simplify_core, tout << "new factor is const\n";); - auto s = sign(new_factor, sample(), m_am); + auto s = sign(new_factor); if (is_zero(s)) { bool atom_val = a->get_kind() == atom::EQ; bool lit_val = l.sign() ? !atom_val : atom_val; @@ -1368,8 +1371,8 @@ namespace nlsat { if (m_solver.value(new_lit) == l_true) { TRACE(nlsat_simplify_bug, tout << "literal normalized away because it is already true after rewriting:\n"; - display(tout << " original: ", l) << "\n"; - display(tout << " rewritten: ", new_lit) << "\n"; + m_solver.display(tout << " original: ", l) << "\n"; + m_solver.display(tout << " rewritten: ", new_lit) << "\n"; if (info.m_eq) { polynomial_ref eq_ref(const_cast(info.m_eq), m_pm); m_pm.display(tout << " equation used: ", eq_ref, m_solver.display_proc()); @@ -1381,8 +1384,8 @@ namespace nlsat { literal assumption = new_lit; TRACE(nlsat_simplify_bug, tout << "literal replaced by lower-stage assumption due to rewriting:\n"; - display(tout << " original: ", l) << "\n"; - display(tout << " assumption: ", assumption) << "\n"; + m_solver.display(tout << " original: ", l) << "\n"; + m_solver.display(tout << " assumption: ", assumption) << "\n"; if (info.m_eq) { polynomial_ref eq_ref(const_cast(info.m_eq), m_pm); m_pm.display(tout << " equation used: ", eq_ref, m_solver.display_proc()); @@ -1396,12 +1399,12 @@ namespace nlsat { literal before = new_lit; (void)before; new_lit = normalize(new_lit, max); - TRACE(nlsat_simplify_core, tout << "simplified literal after normalization:\n"; display(tout, new_lit); tout << " " << m_solver.value(new_lit) << "\n";); + TRACE(nlsat_simplify_core, tout << "simplified literal after normalization:\n"; m_solver.display(tout, new_lit); tout << " " << m_solver.value(new_lit) << "\n";); if (new_lit == true_literal || new_lit == false_literal) { TRACE(nlsat_simplify_bug, tout << "normalize() turned rewritten literal into constant value:\n"; - display(tout << " original: ", l) << "\n"; - display(tout << " rewritten: ", before) << "\n"; + m_solver.display(tout << " original: ", l) << "\n"; + m_solver.display(tout << " rewritten: ", before) << "\n"; tout << " result: " << (new_lit == true_literal ? "true" : "false") << "\n"; if (info.m_eq) { polynomial_ref eq_ref(const_cast(info.m_eq), m_pm); @@ -1425,7 +1428,7 @@ namespace nlsat { polynomial_ref lc_eq(m_pm); lc_eq = m_pm.coeff(eq, info.m_x, info.m_k); info.m_lc = lc_eq.get(); - info.m_lc_sign = sign(lc_eq, sample(), m_am); + info.m_lc_sign = sign(lc_eq); info.m_lc_add = false; info.m_lc_add_ineq = false; info.m_lc_const = m_pm.is_const(lc_eq); @@ -1582,7 +1585,7 @@ namespace nlsat { var max_x = max_var(m_ps); TRACE(nlsat_explain, tout << "polynomials in the conflict:\n"; display(tout, m_solver, m_ps); tout << "\n";); elim_vanishing(m_ps); - TRACE(nlsat_explain, tout << "after elim_vanishing m_ps:\n"; display(tout, m_ps); tout << "\n";); + TRACE(nlsat_explain, tout << "after elim_vanishing m_ps:\n"; display(tout, m_solver, m_ps); tout << "\n";); project(m_ps, max_x); TRACE(nlsat_explain, tout << "after projection\n"; display(tout, m_solver, m_ps); tout << "\n";); } @@ -1594,7 +1597,7 @@ namespace nlsat { m_core2.append(num, ls); var max = max_var(num, ls); SASSERT(max != null_var); - TRACE(nlsat_explain, display(tout << "core before normalization\n", m_core2) << "\n";); + TRACE(nlsat_explain, display(tout << "core before normalization\n", m_solver, m_core2) << "\n";); normalize(m_core2, max); TRACE(nlsat_explain, display(tout << "core after normalization\n", m_solver, m_core2) << "\n";); simplify(m_core2, max); @@ -1603,7 +1606,7 @@ namespace nlsat { m_core2.reset(); } else { - TRACE(nlsat_explain, display(tout << "core befor normalization\n", m_core2) << "\n";); + TRACE(nlsat_explain, display(tout << "core befor normalization\n", m_solver, m_core2) << "\n";); main(num, ls); } } @@ -1700,7 +1703,7 @@ namespace nlsat { m_solver.display_assignment(tout << "assignment:\n"); ); - if (max_var(num, ls) == 0 && !m_assignment.is_assigned(0)) { + if (max_var(num, ls) == 0 && !m_solver.sample().is_assigned(0)) { TRACE(nlsat_explain, tout << "all literals use unassigned max var; returning justification\n";); result.reset(); return; @@ -1712,7 +1715,7 @@ namespace nlsat { process(num, ls); reset_already_added(); m_result = nullptr; - TRACE(nlsat_explain, display(tout << "[explain] result\n", result) << "\n";); + TRACE(nlsat_explain, display(tout << "[explain] result\n", m_solver, result) << "\n";); CASSERT("nlsat", check_already_added()); break; } diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 2403f94b2..44a0254f0 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -22,6 +22,6 @@ def_module_params('nlsat', ('factor', BOOL, True, "factor polynomials produced during conflict resolution."), ('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."), ('zero_disc', BOOL, False, "add_zero_assumption to the vanishing discriminant."), - ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only") - + ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"), + ('apply_levelwise', BOOL, True, "apply levelwise.") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index eb75eefc4..794b2e265 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2315,7 +2315,7 @@ namespace nlsat { m_lazy_clause.reset(); - m_explain.main_operator(jst.num_lits(), jst.lits(), m_lazy_clause); + m_explain.compute_conflict_explanation(jst.num_lits(), jst.lits(), m_lazy_clause); for (unsigned i = 0; i < sz; i++) m_lazy_clause.push_back(~jst.lit(i)); diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index a47d40867..c513a3955 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -849,7 +849,7 @@ void tst_nlsat_mv() { s.set_rvalues(assignment); nlsat::scoped_literal_vector result(s); - ex.main_operator(lits.size(), lits.data(), result); + ex.compute_conflict_explanation(lits.size(), lits.data(), result); std::cout << "main_operator root regression core:\n"; s.display(std::cout, lits.size(), lits.data()); diff --git a/src/util/trace_tags.def b/src/util/trace_tags.def index ba9779129..b62c0a20f 100644 --- a/src/util/trace_tags.def +++ b/src/util/trace_tags.def @@ -692,7 +692,6 @@ X(Global, nlsat_bug, "nlsat bug") X(Global, nlsat_evaluator, "nlsat evaluator") X(Global, nlsat_evaluator_bug, "nlsat evaluator bug") X(Global, nlsat_explain, "nlsat explain") -X(Global, levelwise, "levelwise") X(Global, nlsat_factor, "nlsat factor") X(Global, nlsat_fd, "nlsat fd") X(Global, nlsat_inf_set, "nlsat inf set")