From d0b740bd175e7aac014de98e4111279261fd6d90 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 9 Jan 2026 13:29:46 -1000 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 1 - src/nlsat/nlsat_params.pyg | 2 +- src/nlsat/nlsat_solver.cpp | 2 +- 3 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 005ffd820..d72326c68 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -127,7 +127,6 @@ struct levelwise::impl { chain.reset(); m_cache.psc_chain(p, d, x, chain); polynomial_ref disc(m_pm); - // Iterate forward: S[0] is the resultant (after reverse in psc_chain) for (unsigned i = 0; i < chain.size(); ++i) { disc = polynomial_ref(chain.get(i), m_pm); if (!disc || is_zero(disc)) diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index b780a651b..d15294dac 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -23,6 +23,6 @@ def_module_params('nlsat', ('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"), - ('apply_levelwise', BOOL, True, "apply levelwise."), + ('lws', BOOL, True, "apply levelwise."), ('canonicalize', BOOL, True, "canonicalize polynomials.") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 6e0550fde..ba667c967 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -307,7 +307,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_apply_lws = p.lws(); m_check_lemmas |= !(m_debug_known_solution_file_name.empty()); m_cell_sample = p.cell_sample();