From 1cb0743e2bdfd83d73520aee0493d42e4aa8cee5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 10 Dec 2025 07:56:29 -1000 Subject: [PATCH] canonicalize polynomials in nlsat Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 2 +- src/nlsat/nlsat_common.h | 2 +- src/nlsat/nlsat_explain.cpp | 14 +++++++------- src/nlsat/nlsat_explain.h | 2 +- src/nlsat/nlsat_params.pyg | 3 ++- src/nlsat/nlsat_solver.cpp | 3 ++- 6 files changed, 14 insertions(+), 12 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index acd21d134..2f5b602ee 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -184,7 +184,7 @@ namespace nlsat { // max_x plays the role of n in algorith 1 of the levelwise paper. impl(solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am, polynomial::cache & cache) - : m_solver(solver), m_P(ps), m_n(max_x), m_pm(pm), m_am(am), m_cache(cache), m_todo_set(cache) { + : m_solver(solver), m_P(ps), m_n(max_x), m_pm(pm), m_am(am), m_cache(cache), m_todo_set(cache, true) { TRACE(lws, tout << "m_n:" << m_n << "\n";); m_I.reserve(m_n); // cannot just resize bcs of the absence of the default constructor of root_function_interval for (unsigned i = 0; i < m_n; ++i) diff --git a/src/nlsat/nlsat_common.h b/src/nlsat/nlsat_common.h index 26d14989f..5b50e2fc3 100644 --- a/src/nlsat/nlsat_common.h +++ b/src/nlsat/nlsat_common.h @@ -29,7 +29,7 @@ namespace nlsat { svector m_in_set; bool m_canonicalize; - todo_set(polynomial::cache& u, bool canonicalize = false); + todo_set(polynomial::cache& u, bool canonicalize); void reset(); void insert(poly* p); diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 32d6c3199..515e937c1 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -50,7 +50,7 @@ namespace nlsat { bool m_factor; bool m_add_all_coeffs; bool m_add_zero_disc; - bool m_cell_sample; + bool m_sample_cell_project; assignment const & sample() const { return m_solver.sample(); } assignment & sample() { return m_solver.sample(); } @@ -69,7 +69,7 @@ namespace nlsat { evaluator & m_evaluator; imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq, - evaluator & ev, bool is_sample): + evaluator & ev, bool sample_cell_project, bool canonicalize): m_solver(s), m_atoms(atoms), m_x2eq(x2eq), @@ -82,8 +82,8 @@ namespace nlsat { m_factors(m_pm), m_factors_save(m_pm), m_roots_tmp(m_am), - m_cell_sample(is_sample), - m_todo(u), + m_sample_cell_project(sample_cell_project), + m_todo(u, canonicalize), m_core1(s), m_core2(s), m_evaluator(ev) { @@ -1109,7 +1109,7 @@ namespace nlsat { } void project(polynomial_ref_vector & ps, var max_x) { - if (m_cell_sample) { + if (m_sample_cell_project) { project_cdcac(ps, max_x); } else { @@ -1791,8 +1791,8 @@ namespace nlsat { }; explain::explain(solver & s, assignment const & x2v, polynomial::cache & u, - atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample) { - m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, use_cell_sample); + atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample, bool canonicalize) { + m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, use_cell_sample, canonicalize); } explain::~explain() { diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index f423cab4a..41dd1c2c5 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -35,7 +35,7 @@ namespace nlsat { imp * m_imp; public: explain(solver & s, assignment const & x2v, polynomial::cache & u, - atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample_proj); + atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample_proj, bool canonicalize); ~explain(); diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 44a0254f0..b780a651b 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -23,5 +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.") + ('apply_levelwise', BOOL, True, "apply levelwise."), + ('canonicalize', BOOL, True, "canonicalize polynomials.") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 48a50759f..6e0550fde 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -266,7 +266,7 @@ namespace nlsat { m_simplify(s, m_atoms, m_clauses, m_learned, m_pm), m_display_var(m_perm), m_display_assumption(nullptr), - m_explain(s, m_assignment, m_cache, m_atoms, m_var2eq, m_evaluator, nlsat_params(c.m_params).cell_sample()), + m_explain(s, m_assignment, m_cache, m_atoms, m_var2eq, m_evaluator, nlsat_params(c.m_params).cell_sample(), nlsat_params(c.m_params).canonicalize()), m_scope_lvl(0), m_lemma(s), m_lazy_clause(s), @@ -4635,5 +4635,6 @@ namespace nlsat { } bool solver::apply_levelwise() const { return m_imp->m_apply_lws; } + };