From 14cdad13cd1cea784b07133366d913b29735a0b2 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 3 Oct 2025 12:54:53 -0700
Subject: [PATCH] add parameter to suppress/enable levelwise

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

diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index 5073bbd0f..802e94e8b 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -155,12 +155,9 @@ namespace nlsat {
           - For factors with level == m_n: add an_del(p) and isolate their indexed roots over the sample;
           sort those roots and for each adjacent pair coming from distinct polynomials add
           ord_inv(resultant(p_j, p_{j+1})) to Q.
-          - If any constructed polynomial (resultant, discriminant, etc.) is nullified on the sample,
-          fail immediately.
+          - If any constructed polynomial is nullified on the sample, that is all coefficients are zeroes, then fail.
 
-          Result: Q = { sgn_inv(p) | level(p) < m_n }
-          ∪ { an_del(p)  | level(p) == m_n }
-          ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent roots }.
+          Result: Q = { sgn_inv(p) | level(p) < m_n } ∪ { an_del(p)  | level(p) == m_n } ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent roots }.
         */
         // Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n
         void collect_level_properties(std::vector<poly*> & ps_of_n_level) {
@@ -342,8 +339,6 @@ namespace nlsat {
              }
 
              collect_E(p_non_null);
-             // Ensure m_I can hold interval for this level
-             SASSERT(m_I.size() > m_level);
              std::sort(m_E.begin(), m_E.end(), [&](root_function const& a, root_function const& b){
                  return m_am.lt(a.val, b.val);
              });
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 2e646c4cb..d47204f2b 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1146,8 +1146,10 @@ namespace nlsat {
             
             var x = m_todo.extract_max_polys(ps);
 
-            if (!levelwise_single_cell(ps, max_x)) { // on levelwise_single_cell failure continue with cdcac
-                polynomial_ref_vector samples(m_pm);
+            if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x))
+                return;
+
+            polynomial_ref_vector samples(m_pm);
             
             polynomial_ref_vector samples(m_pm);
             if (x < max_x)
@@ -1692,9 +1694,10 @@ namespace nlsat {
             SASSERT(check_already_added());
             SASSERT(num > 0);
             TRACE(nlsat_explain, 
-                  tout << "[explain] set of literals is infeasible in the current interpretation\n"; 
+                  tout << "the infeasible clause:\n"; 
                   display(tout, m_solver, num, ls) << "\n";
-                  m_solver.display_assignment(tout);
+                  
+                  m_solver.display_assignment(tout << "assignment:\n");
                   );
             if (max_var(num, ls) == 0 && !m_assignment.is_assigned(0)) {
                 TRACE(nlsat_explain, tout << "all literals use unassigned max var; returning justification\n";);
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index c0ecd97d3..30c844d6c 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -244,7 +244,7 @@ namespace nlsat {
         // statistics
         stats                  m_stats;
         std::string m_debug_known_solution_file_name;
-
+        bool m_apply_lws;
         imp(solver& s, ctx& c):
             m_ctx(c),
             m_solver(s),
@@ -304,6 +304,7 @@ namespace nlsat {
             m_check_lemmas   = p.check_lemmas();
             m_variable_ordering_strategy = p.variable_ordering_strategy();
             m_debug_known_solution_file_name = p.known_sat_assignment_file_name();
+            m_apply_lws = p.apply_levelwise();
             m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
             m_cell_sample = p.cell_sample();
   
@@ -4621,6 +4622,7 @@ namespace nlsat {
     assumption solver::join(assumption a, assumption b) {
         return (m_imp->m_asm.mk_join(static_cast<imp::_assumption_set>(a), static_cast<imp::_assumption_set>(b)));
     }
-    
+
+    bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
         
 };
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index 67335a2c8..4e6957e2b 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -246,7 +246,7 @@ namespace nlsat {
         static void collect_param_descrs(param_descrs & d);
         const assignment& sample() const;
         assignment& sample(); 
-
+        bool apply_levelwise() const;
         void reset();
         void collect_statistics(statistics & st);
         void reset_statistics();