From 5cb046f9fb8169c527ba7b26aab0667e00c36d6d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 14 Aug 2025 16:24:58 -0700 Subject: [PATCH] pass nlsat::solver to levelwise Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 9 +++++---- src/nlsat/levelwise.h | 2 +- src/nlsat/nlsat_explain.cpp | 2 +- 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 76603bc10..dd6550080 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -37,6 +37,7 @@ namespace nlsat { unsigned s_idx = 0; // index into current sample roots on level, if applicable unsigned level = 0; }; + solver& m_solver; polynomial_ref_vector const& m_P; var m_n; assignment const& m_s; @@ -51,8 +52,8 @@ namespace nlsat { // 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. - impl(polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am) - : m_P(ps), m_n(max_x), m_s(s), m_pm(pm), m_am(am) { + 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_s(s), m_pm(pm), m_am(am) { init_relation(); } @@ -233,8 +234,8 @@ namespace nlsat { } }; // constructor - levelwise::levelwise(polynomial_ref_vector const& ps, var n, assignment const& s, pmanager& pm, anum_manager& am) - : m_impl(new impl(ps, n, s, pm, am)) {} + levelwise::levelwise(nlsat::solver& solver, polynomial_ref_vector const& ps, var n, assignment const& s, pmanager& pm, anum_manager& am) + : m_impl(new impl(solver, ps, n, s, pm, am)) {} levelwise::~levelwise() { delete m_impl; } diff --git a/src/nlsat/levelwise.h b/src/nlsat/levelwise.h index d20838b39..a06fee04e 100644 --- a/src/nlsat/levelwise.h +++ b/src/nlsat/levelwise.h @@ -34,7 +34,7 @@ namespace nlsat { impl* m_impl; public: // Construct with polynomials ps, maximal variable max_x, current sample s, polynomial manager pm, and algebraic-number manager am - levelwise(polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am); + levelwise(nlsat::solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am); ~levelwise(); levelwise(levelwise const&) = delete; diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 21946f925..9b7f369a4 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1228,7 +1228,7 @@ namespace nlsat { // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore polynomial_ref_vector samples(m_pm); - levelwise lws(ps, max_x, m_assignment, m_pm, m_am); + levelwise lws(m_solver, ps, max_x, m_assignment, m_pm, m_am); auto cell = lws.single_cell(); if (x < max_x) cac_add_cell_lits(ps, x, samples);