From fb97043cb2e7b540aad03114025be70361b08313 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 3 Oct 2025 12:54:53 -0700 Subject: [PATCH] add parameter to suppress/enable levelwise Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 9 ++------ src/nlsat/nlsat_explain.cpp | 44 +++++++++++++++++++------------------ src/nlsat/nlsat_params.pyg | 3 ++- src/nlsat/nlsat_solver.cpp | 6 +++-- src/nlsat/nlsat_solver.h | 2 +- 5 files changed, 32 insertions(+), 32 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 5073bbd0f..802e94e8b 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -155,12 +155,9 @@ namespace nlsat { - For factors with level == m_n: add an_del(p) and isolate their indexed roots over the sample; sort those roots and for each adjacent pair coming from distinct polynomials add ord_inv(resultant(p_j, p_{j+1})) to Q. - - If any constructed polynomial (resultant, discriminant, etc.) is nullified on the sample, - fail immediately. + - If any constructed polynomial is nullified on the sample, that is all coefficients are zeroes, then fail. - Result: Q = { sgn_inv(p) | level(p) < m_n } - ∪ { an_del(p) | level(p) == m_n } - ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent roots }. + Result: Q = { sgn_inv(p) | level(p) < m_n } ∪ { an_del(p) | level(p) == m_n } ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent roots }. */ // Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n void collect_level_properties(std::vector & ps_of_n_level) { @@ -342,8 +339,6 @@ namespace nlsat { } collect_E(p_non_null); - // Ensure m_I can hold interval for this level - SASSERT(m_I.size() > m_level); std::sort(m_E.begin(), m_E.end(), [&](root_function const& a, root_function const& b){ return m_am.lt(a.val, b.val); }); diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 209b7b261..2dd9a3055 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1229,28 +1229,29 @@ 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); - if (x < max_x) - cac_add_cell_lits(ps, x); + if (x < max_x) + cac_add_cell_lits(ps, x); - 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, m_solver, x); tout << "\npolynomials\n"; - display(tout, m_solver, ps); tout << "\n";); - add_lcs(ps, x); - psc_discriminant(ps, x); - psc_resultant(ps, x); - - if (m_todo.empty()) - break; - x = m_todo.extract_max_polys(ps); - cac_add_cell_lits(ps, x); + 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, m_solver, x); tout << "\npolynomials\n"; + display(tout, m_solver, ps); tout << "\n";); + add_lcs(ps, x); + psc_discriminant(ps, x); + psc_resultant(ps, x); + + if (m_todo.empty()) + break; + x = m_todo.extract_max_polys(ps); + cac_add_cell_lits(ps, x); } } @@ -1731,9 +1732,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"); ); m_result = &result; process(num, ls); diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 6a0f50cd3..6d2e44ed1 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -19,5 +19,6 @@ def_module_params('nlsat', ('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"), ('seed', UINT, 0, "random seed."), ('factor', BOOL, True, "factor polynomials produced during conflict resolution."), - ('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 ed468f12b..1783ab80a 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -242,7 +242,7 @@ namespace nlsat { // statistics stats m_stats; std::string m_debug_known_solution_file_name; - + bool m_apply_lws; imp(solver& s, ctx& c): m_ctx(c), m_solver(s), @@ -300,6 +300,7 @@ namespace nlsat { m_check_lemmas = p.check_lemmas(); m_variable_ordering_strategy = p.variable_ordering_strategy(); m_debug_known_solution_file_name = p.known_sat_assignment_file_name(); + m_apply_lws = p.apply_levelwise(); m_check_lemmas |= !(m_debug_known_solution_file_name.empty()); m_cell_sample = p.cell_sample(); @@ -4397,6 +4398,7 @@ namespace nlsat { assumption solver::join(assumption a, assumption b) { return (m_imp->m_asm.mk_join(static_cast(a), static_cast(b))); } - + + bool solver::apply_levelwise() const { return m_imp->m_apply_lws; } }; diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 67335a2c8..4e6957e2b 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -246,7 +246,7 @@ namespace nlsat { static void collect_param_descrs(param_descrs & d); const assignment& sample() const; assignment& sample(); - + bool apply_levelwise() const; void reset(); void collect_statistics(statistics & st); void reset_statistics();