From 1066f3ea3ba7053a22c05b08331d322309d8c056 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 14 Aug 2025 16:24:58 -0700
Subject: [PATCH] pass nlsat::solver to levelwise

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/levelwise.cpp | 9 +++++----
 src/nlsat/levelwise.h   | 2 +-
 2 files changed, 6 insertions(+), 5 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<std::vector<bool>> 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;