From 3cff4d3410040dfd440dcde7ad6b1c8e57942ed8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 15 Aug 2025 11:44:57 -0700 Subject: [PATCH] refactor Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 17 ++++----- src/nlsat/nlsat_common.h | 71 +++++++++++++++++++++++++++++++++++++ src/nlsat/nlsat_explain.cpp | 37 +++++++------------ src/nlsat/nlsat_pp.h | 61 ------------------------------- src/nlsat/nlsat_solver.cpp | 5 +++ src/nlsat/nlsat_solver.h | 4 ++- 6 files changed, 99 insertions(+), 96 deletions(-) create mode 100644 src/nlsat/nlsat_common.h delete mode 100644 src/nlsat/nlsat_pp.h diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 5041ae2ed..435c0f6b7 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -6,7 +6,7 @@ #include #include #include "math/polynomial/algebraic_numbers.h" -#include "nlsat_pp.h" +#include "nlsat_common.h" namespace nlsat { // Local enums reused from previous scaffolding @@ -41,7 +41,6 @@ namespace nlsat { solver& m_solver; polynomial_ref_vector const& m_P; var m_n; - assignment const& sample() { return m_solver.get_assignment();} pmanager& m_pm; anum_manager& m_am; std::vector m_Q; // the set of properties to prove as in single_cell @@ -52,7 +51,11 @@ namespace nlsat { // Transitive closure matrix: dom[a][b] == true iff a ▹ b (a strictly dominates b). // Since m_p_relation holds (lesser -> greater), we invert edges when populating dom: greater ▹ lesser. std::vector> m_prop_dom; - // max_x plays the role of n in algorith 1 of the levelwise paper. + + assignment const& sample() const { return m_solver.get_assignment();} + assignment & sample() { return m_solver.get_assignment(); } + +// 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) : m_solver(solver), m_P(ps), m_n(max_x), m_pm(pm), m_am(am) { TRACE(levelwise, tout << "m_n:" << m_n << "\n";); @@ -181,12 +184,6 @@ namespace nlsat { return ret; } - ::sign sign(poly * p) { - polynomial_ref pr(p, m_P.m()); - auto s = m_am.eval_sign_at(pr, sample()); - TRACE(levelwise, tout << "p: " << p << " var: " << m_pm.max_var(p) << " sign: " << s << "\n";); - return s; - } result_struct construct_interval() { result_struct ret; @@ -212,7 +209,7 @@ namespace nlsat { std::vector p_non_null; for (const auto & pr: m_Q) { - if (pr.prop == prop_enum::sgn_inv_irreducible && m_pm.max_var(pr.p) < m_i && sign(pr.p) != 0) + if (pr.prop == prop_enum::sgn_inv_irreducible && m_pm.max_var(pr.p) < m_i && sign(polynomial_ref(pr.p, m_pm), sample(), m_am) != 0) p_non_null.push_back(pr.p); } diff --git a/src/nlsat/nlsat_common.h b/src/nlsat/nlsat_common.h new file mode 100644 index 000000000..17f7916b5 --- /dev/null +++ b/src/nlsat/nlsat_common.h @@ -0,0 +1,71 @@ +/*++ + Copyright (c) 2025 + + Module Name: + + nlsat_common.h + + Abstract: + + Pretty-print helpers for NLSAT components as free functions. + These forward to existing solver/pmanager display facilities. + + --*/ +#pragma once + +#include "nlsat/nlsat_solver.h" +#include "nlsat/nlsat_scoped_literal_vector.h" +namespace nlsat { + + 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; + } + + inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref_vector const& ps, display_var_proc const& proc, char const* delim = "\n") { + for (unsigned i = 0; i < ps.size(); ++i) { + if (i > 0) out << delim; + pm.display(out, ps.get(i), proc); + } + return out; + } + + inline std::ostream& display(std::ostream& out, solver& s, polynomial_ref const& p) { + return display(out, s.pm(), p, s.display_proc()); + } + + inline std::ostream& display(std::ostream& out, solver& s, polynomial_ref_vector const& ps, char const* delim = "\n") { + return display(out, s.pm(), ps, s.display_proc(), delim); + } + + inline std::ostream& display(std::ostream& out, solver& s, literal l) { + return s.display(out, l); + } + + inline std::ostream& display(std::ostream& out, solver& s, unsigned n, literal const* ls) { + return s.display(out, n, ls); + } + + inline std::ostream& display(std::ostream& out, solver& s, literal_vector const& ls) { + return s.display(out, ls); + } + + inline std::ostream& display(std::ostream& out, solver& s, scoped_literal_vector const& ls) { + return s.display(out, ls.size(), ls.data()); + } + + inline std::ostream& display_var(std::ostream& out, solver& s, var x) { + return s.display(out, x); + } + /** + \brief evaluate the given polynomial in the current interpretation. + max_var(p) must be assigned in the current interpretation. + */ + inline ::sign sign(polynomial_ref const & p, assignment & x2v, anum_manager& am) { + SASSERT(max_var(p) == null_var || x2v.is_assigned(max_var(p))); + auto s = am.eval_sign_at(p, x2v); + TRACE(nlsat_explain, tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";); + return s; + } + +} // namespace nlsat diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 7e4881d83..d78b88c98 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -21,7 +21,7 @@ Revision History: #include "nlsat/nlsat_assignment.h" #include "nlsat/nlsat_evaluator.h" #include "math/polynomial/algebraic_numbers.h" -#include "nlsat/nlsat_pp.h" +#include "nlsat/nlsat_common.h" #include "util/ref_buffer.h" #include "util/mpq.h" @@ -34,7 +34,6 @@ namespace nlsat { struct explain::imp { solver & m_solver; - assignment const & m_assignment; atom_vector const & m_atoms; atom_vector const & m_x2eq; anum_manager & m_am; @@ -53,6 +52,8 @@ namespace nlsat { bool m_add_zero_disc; bool m_cell_sample; + assignment const & sample() const { return m_solver.get_assignment(); } + assignment & sample() { return m_solver.get_assignment(); } struct todo_set { polynomial::cache & m_cache; @@ -140,7 +141,6 @@ namespace nlsat { imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq, evaluator & ev, bool is_sample): m_solver(s), - m_assignment(x2v), m_atoms(atoms), m_x2eq(x2eq), m_am(x2v.am()), @@ -164,7 +164,7 @@ namespace nlsat { m_add_zero_disc = true; } - // display helpers moved to free functions in nlsat_pp.h + // display helpers moved to free functions in nlsat_common.h /** \brief Add literal to the result vector. @@ -192,17 +192,6 @@ namespace nlsat { SASSERT(check_already_added()); } - - /** - \brief evaluate the given polynomial in the current interpretation. - max_var(p) must be assigned in the current interpretation. - */ - ::sign sign(polynomial_ref const & p) { - SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p))); - auto s = m_am.eval_sign_at(p, m_assignment); - TRACE(nlsat_explain, tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";); - return s; - } /** \brief Wrapper for factorization @@ -525,7 +514,7 @@ namespace nlsat { if (max_var(p) == max) elim_vanishing(p); // eliminate vanishing coefficients of max if (is_const(p) || max_var(p) < max) { - int s = sign(p); + int s = sign(p, m_solver.get_assignment(), m_am); if (!is_const(p)) { SASSERT(max_var(p) != null_var); SASSERT(max_var(p) < max); @@ -770,7 +759,7 @@ namespace nlsat { auto c = polynomial_ref(this->m_pm); for (unsigned j = 0; j <= n; j++) { c = m_pm.coeff(s, x, j); - SASSERT(sign(c) == 0); + SASSERT(sign(c, sample(), m_am) == 0); ensure_sign(c); } return true; @@ -783,7 +772,7 @@ namespace nlsat { auto c = polynomial_ref(this->m_pm); for (unsigned j = 0; j <= n; j++) { c = m_pm.coeff(s, x, j); - if (sign(c) != 0) + if (sign(c, sample(), m_am) != 0) return false; } return true; @@ -919,7 +908,7 @@ namespace nlsat { } polynomial_ref c(m_pm); c = m_pm.coeff(p, y, 1); - int s = sign(c); + int s = sign(c, sample(), m_am); if (s == 0) { return false; } @@ -952,7 +941,7 @@ namespace nlsat { return false; } - SASSERT(m_assignment.is_assigned(y)); + SASSERT(sample().is_assigned(y)); polynomial_ref A(m_pm), B(m_pm), C(m_pm), q(m_pm), p_diff(m_pm), yy(m_pm); A = m_pm.coeff(p, y, 2); B = m_pm.coeff(p, y, 1); @@ -1305,7 +1294,7 @@ namespace nlsat { } if (is_const(new_factor)) { TRACE(nlsat_simplify_core, tout << "new factor is const\n";); - auto s = sign(new_factor); + auto s = sign(new_factor, sample(), m_am); if (is_zero(s)) { bool atom_val = a->get_kind() == atom::EQ; bool lit_val = l.sign() ? !atom_val : atom_val; @@ -1421,7 +1410,7 @@ namespace nlsat { polynomial_ref lc_eq(m_pm); lc_eq = m_pm.coeff(eq, info.m_x, info.m_k); info.m_lc = lc_eq.get(); - info.m_lc_sign = sign(lc_eq); + info.m_lc_sign = sign(lc_eq, sample(), m_am); info.m_lc_add = false; info.m_lc_add_ineq = false; info.m_lc_const = m_pm.is_const(lc_eq); @@ -1832,12 +1821,12 @@ namespace nlsat { collect_polys(lits.size(), lits.data(), m_ps); unbounded = true; scoped_anum x_val(m_am); - x_val = m_assignment.value(x); + x_val = sample().value(x); for (unsigned i = 0; i < m_ps.size(); ++i) { p = m_ps.get(i); scoped_anum_vector & roots = m_roots_tmp; roots.reset(); - m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); + m_am.isolate_roots(p, undef_var_assignment(sample(), x), roots); for (unsigned j = 0; j < roots.size(); ++j) { int s = m_am.compare(x_val, roots[j]); if (s <= 0 && (unbounded || m_am.compare(roots[j], val) <= 0)) { diff --git a/src/nlsat/nlsat_pp.h b/src/nlsat/nlsat_pp.h deleted file mode 100644 index 4b86d775a..000000000 --- a/src/nlsat/nlsat_pp.h +++ /dev/null @@ -1,61 +0,0 @@ -/*++ -Copyright (c) 2025 - -Module Name: - - nlsat_pp.h - -Abstract: - - Pretty-print helpers for NLSAT components as free functions. - These forward to existing solver/pmanager display facilities. - ---*/ -#pragma once - -#include "nlsat/nlsat_solver.h" -#include "nlsat/nlsat_scoped_literal_vector.h" -namespace nlsat { - -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; -} - -inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref_vector const& ps, display_var_proc const& proc, char const* delim = "\n") { - for (unsigned i = 0; i < ps.size(); ++i) { - if (i > 0) out << delim; - pm.display(out, ps.get(i), proc); - } - return out; -} - -inline std::ostream& display(std::ostream& out, solver& s, polynomial_ref const& p) { - return display(out, s.pm(), p, s.display_proc()); -} - -inline std::ostream& display(std::ostream& out, solver& s, polynomial_ref_vector const& ps, char const* delim = "\n") { - return display(out, s.pm(), ps, s.display_proc(), delim); -} - -inline std::ostream& display(std::ostream& out, solver& s, literal l) { - return s.display(out, l); -} - -inline std::ostream& display(std::ostream& out, solver& s, unsigned n, literal const* ls) { - return s.display(out, n, ls); -} - -inline std::ostream& display(std::ostream& out, solver& s, literal_vector const& ls) { - return s.display(out, ls); -} - -inline std::ostream& display(std::ostream& out, solver& s, scoped_literal_vector const& ls) { - return s.display(out, ls.size(), ls.data()); -} - -inline std::ostream& display_var(std::ostream& out, solver& s, var x) { - return s.display(out, x); -} - -} // namespace nlsat diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 00004ebc8..abe222362 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -4351,6 +4351,11 @@ namespace nlsat { const assignment &solver::get_assignment() const { return m_imp->m_assignment; } + + assignment &solver::get_assignment() { + return m_imp->m_assignment; + } + unsynch_mpq_manager &solver::qm() { return m_imp->m_qm; diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 611b20ea7..a3656590d 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -244,7 +244,9 @@ namespace nlsat { // ----------------------- void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - const assignment& get_assignment() const; + const assignment& get_assignment() const; + assignment& get_assignment(); + void reset(); void collect_statistics(statistics & st); void reset_statistics();