diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 22297d4e6..80409754c 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -55,8 +55,6 @@ namespace nlsat { unsigned m_level = 0; // current level being processed unsigned m_spanning_tree_threshold = 3; // minimum both-side count for spanning tree - bool m_null_coeffs = true; - bool m_null_derivs = true; unsigned m_l_rf = UINT_MAX; // position of lower bound in m_rel.m_rfunc unsigned m_u_rf = UINT_MAX; // position of upper bound in m_rel.m_rfunc, UINT_MAX in section case @@ -262,8 +260,6 @@ namespace nlsat { m_I.emplace_back(m_pm); m_spanning_tree_threshold = m_solver.lws_spt_threshold(); - m_null_coeffs = m_solver.lws_null_coeffs(); - m_null_derivs = m_solver.lws_null_derivs(); } // Handle a polynomial whose every coefficient evaluates to zero at the sample. @@ -272,48 +268,46 @@ namespace nlsat { // When a non-vanishing derivative is found, request_factorized it and stop. void handle_nullified_poly(polynomial_ref const& p) { // Add all coefficients of p (w.r.t. m_level) to m_todo. - if (m_null_coeffs) { - unsigned deg = m_pm.degree(p, m_level); - for (unsigned j = 0; j <= deg; ++j) { - polynomial_ref coeff(m_pm.coeff(p, m_level, j), m_pm); - if (!coeff || is_zero(coeff) || is_const(coeff)) - continue; - request_factorized(coeff); - } + unsigned deg = m_pm.degree(p, m_level); + for (unsigned j = 0; j <= deg; ++j) { + polynomial_ref coeff(m_pm.coeff(p, m_level, j), m_pm); + if (!coeff || is_zero(coeff) || is_const(coeff)) + continue; + request_factorized(coeff); } + // Compute partial derivatives level by level. If all derivatives at a level vanish, // request_factorized each of them and continue to the next level. // When a non-vanishing derivative is found, request_factorized it and stop. - if (m_null_derivs) { - polynomial_ref_vector current(m_pm); - current.push_back(p); - while (!current.empty()) { - polynomial_ref_vector next_derivs(m_pm); - for (unsigned i = 0; i < current.size(); ++i) { - polynomial_ref q(current.get(i), m_pm); - unsigned mv = m_pm.max_var(q); - if (mv == null_var) + polynomial_ref_vector current(m_pm); + current.push_back(p); + while (!current.empty()) { + polynomial_ref_vector next_derivs(m_pm); + for (unsigned i = 0; i < current.size(); ++i) { + polynomial_ref q(current.get(i), m_pm); + unsigned mv = m_pm.max_var(q); + if (mv == null_var) + continue; + for (unsigned x = 0; x <= mv; ++x) { + if (m_pm.degree(q, x) == 0) continue; - for (unsigned x = 0; x <= mv; ++x) { - if (m_pm.degree(q, x) == 0) - continue; - polynomial_ref dq = derivative(q, x); - if (!dq || is_zero(dq) || is_const(dq)) - continue; - if (m_am.eval_sign_at(dq, sample()) != 0) { - request_factorized(dq); - return; - } - next_derivs.push_back(dq); + polynomial_ref dq = derivative(q, x); + if (!dq || is_zero(dq) || is_const(dq)) + continue; + if (m_am.eval_sign_at(dq, sample()) != 0) { + request_factorized(dq); + return; } + next_derivs.push_back(dq); } - for (unsigned i = 0; i < next_derivs.size(); ++i) { - polynomial_ref dq(next_derivs.get(i), m_pm); - request_factorized(dq); - } - current = std::move(next_derivs); } + for (unsigned i = 0; i < next_derivs.size(); ++i) { + polynomial_ref dq(next_derivs.get(i), m_pm); + request_factorized(dq); + } + current = std::move(next_derivs); } + } static void reset_interval(root_function_interval& I) { diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index c29bd648c..1ab305984 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -24,7 +24,5 @@ def_module_params('nlsat', ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"), ('lws', BOOL, True, "apply levelwise."), ('lws_spt_threshold', UINT, 2, "minimum both-side polynomial count to apply spanning tree optimization; < 2 disables spanning tree"), - ('lws_null_coeffs', BOOL, True, "add coefficients of nullified polynomials during projection."), - ('lws_null_derivs', BOOL, True, "add derivatives of nullified polynomials during projection."), ('canonicalize', BOOL, True, "canonicalize polynomials.") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index ee875440f..1c83b5e10 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -251,8 +251,6 @@ namespace nlsat { bool m_apply_lws; bool m_last_conflict_used_lws = false; // Track if last conflict explanation used levelwise unsigned m_lws_spt_threshold = 3; - bool m_lws_null_coeffs = true; - bool m_lws_null_derivs = true; imp(solver& s, ctx& c): m_ctx(c), m_solver(s), @@ -314,8 +312,6 @@ namespace nlsat { m_debug_known_solution_file_name = p.known_sat_assignment_file_name(); m_apply_lws = p.lws(); m_lws_spt_threshold = p.lws_spt_threshold(); // 0 disables spanning tree - m_lws_null_coeffs = p.lws_null_coeffs(); - m_lws_null_derivs = p.lws_null_derivs(); m_check_lemmas |= !(m_debug_known_solution_file_name.empty()); m_ism.set_seed(m_random_seed); @@ -4720,13 +4716,8 @@ 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; } - + unsigned solver::lws_spt_threshold() const { return m_imp->m_lws_spt_threshold; } - - bool solver::lws_null_coeffs() const { return m_imp->m_lws_null_coeffs; } - - bool solver::lws_null_derivs() const { return m_imp->m_lws_null_derivs; } - + }; diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 44cc56cb9..566a7c09e 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -249,8 +249,6 @@ namespace nlsat { assignment& sample(); bool apply_levelwise() const; unsigned lws_spt_threshold() const; - bool lws_null_coeffs() const; - bool lws_null_derivs() const; void reset(); void collect_statistics(statistics & st); void reset_statistics();