From d15c0e396e37fc7b001be8a6705664d3a3170e25 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 20 Aug 2025 07:53:43 -0700
Subject: [PATCH] updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/nlsat/nlsat_explain.cpp | 30 +++++++++++++-----------------
 src/nlsat/nlsat_explain.h   |  2 ++
 src/nlsat/nlsat_solver.cpp  |  5 +----
 3 files changed, 16 insertions(+), 21 deletions(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 55c5f5315..234109939 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -45,8 +45,8 @@ namespace nlsat {
         bool                    m_minimize_cores;
         bool                    m_factor;
         bool                    m_signed_project;
-        bool                    m_linear_project;
         bool                    m_cell_sample;
+        bool                    m_linear_project = false;
 
 
         struct todo_set {
@@ -156,7 +156,6 @@ namespace nlsat {
             m_full_dimensional = false;
             m_minimize_cores   = false;
             m_signed_project   = false;
-            m_linear_project   = false;
         }
 
         std::ostream& display(std::ostream & out, polynomial_ref const & p) const {
@@ -1413,7 +1412,7 @@ namespace nlsat {
          * "More is Less: Adding Polynomials for Faster Explanations in NLSAT"
          * in CADE30, 2025
          */
-        void project_linear(polynomial_ref_vector & ps, var max_x) {
+        void linear_project(polynomial_ref_vector & ps, var max_x) {
             if (ps.empty())
                 return;
             m_todo.reset();
@@ -1434,7 +1433,7 @@ namespace nlsat {
                 x = m_todo.extract_max_polys(ps);
             }
 
-            while(!m_todo.empty()) {
+            while (!m_todo.empty()) {
                 add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample);
                 if (all_univ(ps, x) && m_todo.empty()) {
                     m_todo.reset();
@@ -1470,15 +1469,12 @@ namespace nlsat {
 
 
         void project(polynomial_ref_vector & ps, var max_x) {
-            if (m_linear_project) {
-                project_linear(ps, max_x);
-            }
-            else if (m_cell_sample) {
-                project_cdcac(ps, max_x);
-            }
-            else {
-                project_original(ps, max_x);
-            }
+            if (m_linear_project)
+                linear_project(ps, max_x);
+            else if (m_cell_sample) 
+                project_cdcac(ps, max_x);            
+            else 
+                project_original(ps, max_x);            
         }
 
         bool check_already_added() const {
@@ -2336,14 +2332,14 @@ namespace nlsat {
         m_imp->m_signed_project = f;
     }
 
-    void explain::set_linear_project(bool f) {
-        m_imp->m_linear_project = f;
-    }
-
     void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) {
         (*m_imp)(n, ls, result);
     }
 
+    void explain::linear_project(unsigned n, literal const* ls, scoped_literal_vector& result) {
+        m_imp->linear_project(n, ls, result);
+    }
+
     void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
         m_imp->project(x, n, ls, result);
     }
diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h
index 316a1367e..de9502c9b 100644
--- a/src/nlsat/nlsat_explain.h
+++ b/src/nlsat/nlsat_explain.h
@@ -66,6 +66,8 @@ namespace nlsat {
         */
         void main_operator(unsigned n, literal const * ls, scoped_literal_vector & result);
 
+        void linear_project(unsigned n, literal const* ls, scoped_literal_vector& result);
+
         
         /**
            \brief projection for a given variable.
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 8631fa0b8..a6f11256a 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -2074,14 +2074,11 @@ namespace nlsat {
 
             if (best_literal == null_literal)
                 return satisfied;
-                return l_undef;
 
             // assignment does not satisfy the constraints -> create lemma
             SASSERT(best_literal != null_literal);
             m_lazy_clause.reset();
-            m_explain.set_linear_project(true);
-            m_explain.main_operator(1, &best_literal, m_lazy_clause);
-            m_explain.set_linear_project(false); // TODO: there should be a better way to control this.
+            m_explain.linear_project(1, &best_literal, m_lazy_clause);
             m_lazy_clause.push_back(~best_literal);
 
             core.clear();