From bf32a437c1355fee734b5109b53de8b035fb063c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 8 Dec 2025 11:33:31 -1000 Subject: [PATCH] canonicalize polinomals in todo_set Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 34 +++++++---------- src/nlsat/nlsat_common.cpp | 75 +++++++++++++++++++++++++++++++++++++ src/nlsat/nlsat_common.h | 23 ++++++++++++ src/nlsat/nlsat_explain.cpp | 70 ---------------------------------- 4 files changed, 111 insertions(+), 91 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 2c2c31c74..bcd116daf 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -220,10 +220,10 @@ namespace nlsat { } /* - prepare the initial properties - */ - // Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n - void collect_top_level_properties(polynomial_ref_vector & ps_of_n_level) { + prepare the initial properties: + scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n + */ + void collect_top_level_properties(todo_set& ps_of_n_level) { for (unsigned i = 0; i < m_P.size(); ++i) { poly* p = m_P[i]; polynomial_ref pref(p, m_pm); @@ -235,7 +235,7 @@ namespace nlsat { m_Q[level].push(property(prop_enum::sgn_inv, prim)); else if (level == m_n){ m_Q[level].push(property(prop_enum::an_del, prim)); - ps_of_n_level.push_back(prim.get()); + ps_of_n_level.insert(f.get()); } else { UNREACHABLE(); @@ -245,8 +245,8 @@ namespace nlsat { } // isolate and collect algebraic roots for the given polynomials - void collect_roots_for_ps(polynomial_ref_vector & ps_of_n_level, std::vector> & root_vals) { - for (poly * p : ps_of_n_level) { + void collect_roots_for_ps(todo_set const& ps_of_n_level, std::vector> & root_vals) { + for (poly * p : ps_of_n_level.m_set) { scoped_anum_vector roots(m_am); m_am.isolate_roots(polynomial_ref(p, m_pm), undef_var_assignment(sample(), m_n), roots); TRACE(lws, @@ -262,7 +262,7 @@ namespace nlsat { } } - // Helper 3: given collected roots (possibly unsorted), sort them, and add ord_inv(resultant(...)) + // Given collected roots (possibly unsorted), sort them, and add ord_inv(resultant(...)) // for adjacent roots coming from different polynomials. Avoid adding the same unordered pair twice. // Returns false on failure (e.g. when encountering an ambiguous zero resultant). bool add_adjacent_resultants(std::vector> & root_vals) { @@ -317,7 +317,7 @@ namespace nlsat { ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent root functions }. */ void init_properties() { - polynomial_ref_vector ps_of_n_level(m_pm); + todo_set ps_of_n_level(m_cache, true); collect_top_level_properties(ps_of_n_level); std::vector> root_vals; collect_roots_for_ps(ps_of_n_level, root_vals); @@ -414,25 +414,19 @@ namespace nlsat { // Part B of construct_interval: build (I, E, ≼) representation for level i void build_representation() { - // collect non-null polynomials (up to polynomial_manager equality) - polynomial::polynomial_ref_vector p_non_null(m_pm); + // collect non-null polynomials (up to polynomial_manager equality and canonicalization) + todo_set p_non_null(m_cache, true); for (auto & pr: m_Q[m_level]) { if (!pr.m_poly) continue; SASSERT(max_var(pr.m_poly) == m_level); if (pr.m_prop_tag == prop_enum::sgn_inv && !coeffs_are_zeroes_on_sample(pr.m_poly, m_pm, sample(), m_am )) { TRACE(lws, tout << "adding:" << pr.m_poly.get() << "\n";); - poly* new_p = pr.m_poly.get(); - auto it = std::find_if(p_non_null.begin(), p_non_null.end(), - [this, new_p](const poly* q){ - return m_pm.eq(q, new_p); - }); - if (it == p_non_null.end()) - p_non_null.push_back(new_p); + p_non_null.insert(pr.m_poly.get()); } } - collect_E(p_non_null); + collect_E(p_non_null.m_set); // todo: this order needs to be abstracted: it does not have to be linear. // We need a boolean function E_rel(a, b) @@ -995,12 +989,10 @@ or SASSERT(max_var(a) == max_var(b) && max_var(b) == m_level) ; polynomial_ref r(m_pm); - enable_trace("lws"); r = resultant(polynomial_ref(a, m_pm), polynomial_ref(b, m_pm), m_level); TRACE(lws, tout << "resultant of (" << pair.first << "," << pair.second << "):"; ::nlsat::display(tout, m_solver, a) << "\n"; ::nlsat::display(tout,m_solver, b)<< "\nresultant:"; ::nlsat::display(tout, m_solver, r) << "\n"); - disable_trace("lws"); if (m_pm.is_zero(r)) { TRACE(lws, tout << "fail\n";); fail(); diff --git a/src/nlsat/nlsat_common.cpp b/src/nlsat/nlsat_common.cpp index 951d37718..24b5d331e 100644 --- a/src/nlsat/nlsat_common.cpp +++ b/src/nlsat/nlsat_common.cpp @@ -18,6 +18,81 @@ Revision History: --*/ #include "nlsat/nlsat_common.h" namespace nlsat { + + todo_set::todo_set(polynomial::cache& u, bool canonicalize): m_cache(u), m_set(u.pm()), m_canonicalize(canonicalize) {} + + void todo_set::reset() { + pmanager& pm = m_set.m(); + unsigned sz = m_set.size(); + for (unsigned i = 0; i < sz; i++) { + m_in_set[pm.id(m_set.get(i))] = false; + } + m_set.reset(); + } + + void todo_set::insert(poly* p) { + pmanager& pm = m_set.m(); + if (m_canonicalize) { + // Canonicalize content+sign so scalar multiples share the same representative. + if (!pm.is_zero(p) && !pm.is_const(p)) { + polynomial_ref prim(pm); + var x = pm.max_var(p); + pm.primitive(p, x, prim); + p = prim.get(); + } + p = pm.flip_sign_if_lm_neg(p); + } + p = m_cache.mk_unique(p); + unsigned pid = pm.id(p); + if (m_in_set.get(pid, false)) + return; + m_in_set.setx(pid, true, false); + m_set.push_back(p); + } + + bool todo_set::empty() const { return m_set.empty(); } + + // Return max variable in todo_set + var todo_set::max_var() const { + pmanager& pm = m_set.m(); + var max = null_var; + unsigned sz = m_set.size(); + for (unsigned i = 0; i < sz; i++) { + var x = pm.max_var(m_set.get(i)); + SASSERT(x != null_var); + if (max == null_var || x > max) + max = x; + } + return max; + } + + /** + \brief Remove the maximal polynomials from the set and store + them in max_polys. Return the maximal variable + */ + var todo_set::extract_max_polys(polynomial_ref_vector& max_polys) { + max_polys.reset(); + var x = max_var(); + pmanager& pm = m_set.m(); + unsigned sz = m_set.size(); + unsigned j = 0; + for (unsigned i = 0; i < sz; i++) { + poly* p = m_set.get(i); + var y = pm.max_var(p); + SASSERT(y <= x); + if (y == x) { + max_polys.push_back(p); + m_in_set[pm.id(p)] = false; + } + else { + m_set.set(j, p); + j++; + } + } + m_set.shrink(j); + return x; + } + /** \brief Wrapper for factorization */ diff --git a/src/nlsat/nlsat_common.h b/src/nlsat/nlsat_common.h index a0540e4d2..26d14989f 100644 --- a/src/nlsat/nlsat_common.h +++ b/src/nlsat/nlsat_common.h @@ -20,6 +20,29 @@ namespace nlsat { + // Lightweight set of polynomials that keeps elements unique (by cache id) and + // supports extracting all polynomials whose maximal variable is maximal. + // Optional canonicalization (primitive + sign) can be enabled per instance. + struct todo_set { + polynomial::cache& m_cache; + polynomial_ref_vector m_set; + svector m_in_set; + bool m_canonicalize; + + todo_set(polynomial::cache& u, bool canonicalize = false); + + void reset(); + void insert(poly* p); + bool empty() const; + // Return max variable in todo_set + var max_var() const; + /** + \brief Remove the maximal polynomials from the set and store + them in max_polys. Return the maximal variable + */ + var extract_max_polys(polynomial_ref_vector& max_polys); + }; + inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref const& p, display_var_proc const& proc) { pm.display(out, p, proc); return out; diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index d582524fb..32d6c3199 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -55,76 +55,6 @@ namespace nlsat { assignment const & sample() const { return m_solver.sample(); } assignment & sample() { return m_solver.sample(); } - struct todo_set { - polynomial::cache & m_cache; - polynomial_ref_vector m_set; - svector m_in_set; - - todo_set(polynomial::cache & u):m_cache(u), m_set(u.pm()) {} - - void reset() { - pmanager & pm = m_set.m(); - unsigned sz = m_set.size(); - for (unsigned i = 0; i < sz; i++) { - m_in_set[pm.id(m_set.get(i))] = false; - } - m_set.reset(); - } - - void insert(poly * p) { - pmanager & pm = m_set.m(); - p = m_cache.mk_unique(p); - unsigned pid = pm.id(p); - if (m_in_set.get(pid, false)) - return; - m_in_set.setx(pid, true, false); - m_set.push_back(p); - } - - bool empty() const { return m_set.empty(); } - - // Return max variable in todo_set - var max_var() const { - pmanager & pm = m_set.m(); - var max = null_var; - unsigned sz = m_set.size(); - for (unsigned i = 0; i < sz; i++) { - var x = pm.max_var(m_set.get(i)); - SASSERT(x != null_var); - if (max == null_var || x > max) - max = x; - } - return max; - } - - /** - \brief Remove the maximal polynomials from the set and store - them in max_polys. Return the maximal variable - */ - var extract_max_polys(polynomial_ref_vector & max_polys) { - max_polys.reset(); - var x = max_var(); - pmanager & pm = m_set.m(); - unsigned sz = m_set.size(); - unsigned j = 0; - for (unsigned i = 0; i < sz; i++) { - poly * p = m_set.get(i); - var y = pm.max_var(p); - SASSERT(y <= x); - if (y == x) { - max_polys.push_back(p); - m_in_set[pm.id(p)] = false; - } - else { - m_set.set(j, p); - j++; - } - } - m_set.shrink(j); - return x; - } - }; - // temporary field for store todo set of polynomials todo_set m_todo;