From 89f35c95c8aa6e55755bdb76d74498b8aa3f2e07 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 18 Dec 2025 10:47:40 -1000
Subject: [PATCH] Revert "make normalize optional"

This reverts commit c80cfb0b8e3e260aec6dabaf2e686e347b514896.
---
 src/nlsat/levelwise.cpp    | 2 --
 src/nlsat/nlsat_params.pyg | 1 -
 src/nlsat/nlsat_solver.cpp | 3 ---
 src/nlsat/nlsat_solver.h   | 1 -
 4 files changed, 7 deletions(-)

diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index 3afad027b..9da662566 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -508,8 +508,6 @@ namespace nlsat {
         }
 
         void normalize(polynomial_ref & p) {
-            if (!m_solver.lws_norm())
-                return;
             unsigned level = max_var(p);
             if (find_in_Q(p, level)) return;
             TRACE(lws_norm, tout << "p:" << p << std::endl;);
diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg
index ec55ca561..b780a651b 100644
--- a/src/nlsat/nlsat_params.pyg
+++ b/src/nlsat/nlsat_params.pyg
@@ -24,6 +24,5 @@ def_module_params('nlsat',
                           ('zero_disc', BOOL, False, "add_zero_assumption to the vanishing discriminant."),
                           ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"),
                           ('apply_levelwise', BOOL, True, "apply levelwise."),
-                          ('lws_norm', BOOL, True, "normalize polynomials in levelwise."),
                           ('canonicalize', BOOL, True, "canonicalize polynomials.")
                           ))         
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 9c25d6d91..6e0550fde 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -248,7 +248,6 @@ namespace nlsat {
         stats                  m_stats;
         std::string m_debug_known_solution_file_name;
         bool m_apply_lws;
-        bool m_lws_norm;
         imp(solver& s, ctx& c):
             m_ctx(c),
             m_solver(s),
@@ -309,7 +308,6 @@ namespace nlsat {
             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_lws_norm = p.lws_norm();
             m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
             m_cell_sample = p.cell_sample();
   
@@ -4637,7 +4635,6 @@ namespace nlsat {
     }
 
     bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
-    bool solver::lws_norm() const { return m_imp->m_lws_norm; }
 
         
 };
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index a40c2d4d0..b1cc29179 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -248,7 +248,6 @@ namespace nlsat {
         const assignment& sample() const;
         assignment& sample(); 
         bool apply_levelwise() const;
-        bool lws_norm() const;
         void reset();
         void collect_statistics(statistics & st);
         void reset_statistics();