From 88293bf45ba201f57b9e1340792166e4fbe00b63 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 7 Aug 2025 16:22:46 -0700
Subject: [PATCH] get the finest factorizations before project

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/nlsat_explain.cpp | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 92a0428a2..248e4d4e9 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -593,7 +593,7 @@ namespace nlsat {
         /**
            \brief Add factors of p to todo
         */
-        void add_factors(polynomial_ref & p) {
+        void insert_fresh_factors_in_todo(polynomial_ref & p) {
             if (is_const(p))
                 return;
             elim_vanishing(p);
@@ -646,27 +646,21 @@ namespace nlsat {
             return true;
         }
         
-	// For each p in ps add the leading or all the coefficients of p to the projection,
-        // depending on the well-orientedness of ps.
+	// For each p in ps add the leading or coefficent to the projection,
         void add_lcs(polynomial_ref_vector &ps, var x) {
             polynomial_ref p(m_pm);
             polynomial_ref coeff(m_pm);
 
-            bool sqf = is_square_free_at_sample(ps, x);
             // Add coefficients based on well-orientedness
             for (unsigned i = 0; i < ps.size(); i++) {
                 p = ps.get(i);
                 unsigned k_deg = m_pm.degree(p, x);
                 if (k_deg == 0) continue;
                 // p depends on x
-                TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p); tout << (sqf ? " (sqf)" : " (!sqf)") << "\n";);
-                for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) { 
-                    coeff = m_pm.coeff(p, x, j_coeff_deg);
-                    TRACE(nlsat_explain, tout << "    coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";);
-                    add_factors(coeff);
-                    if (sqf)
-                        break;
-                }
+                TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p) << "\n";);
+                coeff = m_pm.coeff(p, x, k_deg);
+                TRACE(nlsat_explain, tout << "    coeff deg " << k_deg << ": "; display(tout, coeff) << "\n";);
+                insert_fresh_factors_in_todo(coeff);
                 
             }
         }
@@ -772,7 +766,7 @@ namespace nlsat {
                       display(tout, s);
                       tout << "\n";);
                 // s did not vanish completely, but its leading coefficient may have vanished
-                add_factors(s);
+                insert_fresh_factors_in_todo(s);
                 return; 
             }
         }
@@ -1231,18 +1225,24 @@ namespace nlsat {
                 return;
 
             m_todo.reset();
-            for (poly* p : ps) {
-                m_todo.insert(p);
+            for (unsigned i = 0; i < ps.size(); i++) {
+                polynomial_ref p(m_pm);
+                p = ps.get(i);
+                insert_fresh_factors_in_todo(p);
             }
+            // replace ps by the fresh factors
+            ps.reset();
+            for (auto p: m_todo.m_set)
+                ps.push_back(p);
+            
             var x = m_todo.extract_max_polys(ps);
             // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
             
             polynomial_ref_vector samples(m_pm);
 
             
-            if (x < max_x){
+            if (x < max_x)
                 cac_add_cell_lits(ps, x, samples);
-            }
 
             while (true) {
                 if (all_univ(ps, x) && m_todo.empty()) {