From 62101fef9002461ad4b15eecbaca73a699cf7587 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 14 Aug 2025 15:50:02 -0700
Subject: [PATCH] pass pmanager

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/levelwise.cpp     | 11 ++++++-----
 src/nlsat/levelwise.h       |  4 ++--
 src/nlsat/nlsat_explain.cpp |  2 +-
 3 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index fb39b6ab7..76603bc10 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -40,6 +40,7 @@ namespace nlsat {
         polynomial_ref_vector const& m_P;
         var                          m_n;
         assignment const&            m_s;
+            pmanager&                    m_pm;
         anum_manager&                m_am;
         std::vector<property>        m_Q; // the set of properties to prove as in single_cell
         bool                         m_fail = false;
@@ -50,8 +51,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, anum_manager& am)
-            : m_P(ps), m_n(max_x), m_s(s), m_am(am) {
+        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) {
             init_relation();
         }
 
@@ -176,7 +177,7 @@ namespace nlsat {
         ::sign sign(poly * p) {
             polynomial_ref pr(p, m_P.m());
             auto s = m_am.eval_sign_at(pr, m_s);
-            TRACE(nlsat_explain, tout << "p: " << p << " var: " << m_P.m().max_var(p) << " sign: " << s << "\n";);
+            TRACE(nlsat_explain, tout << "p: " << p << " var: " << m_pm.max_var(p) << " sign: " << s << "\n";);
             return s;
         }
         result_struct construct_interval() {
@@ -232,8 +233,8 @@ namespace nlsat {
         }
     };
 // constructor
-    levelwise::levelwise(polynomial_ref_vector const& ps, var n, assignment const& s, anum_manager& am)
-        : m_impl(new impl(ps, n, s, am)) {}
+    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() { delete m_impl; }
 
diff --git a/src/nlsat/levelwise.h b/src/nlsat/levelwise.h
index 26a16e70c..d20838b39 100644
--- a/src/nlsat/levelwise.h
+++ b/src/nlsat/levelwise.h
@@ -33,8 +33,8 @@ namespace nlsat {
         struct impl;
         impl* m_impl;
     public:
-    // Construct with polynomials ps, maximal variable max_x, current sample s, and algebraic-number manager am
-    levelwise(polynomial_ref_vector const& ps, var max_x, assignment const& s, anum_manager& am);
+    // 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();
 
         levelwise(levelwise const&) = delete;
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index f32776f9b..a5c25d7af 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1245,7 +1245,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_am);
+            levelwise lws(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);