From d87d1d009f197d3d3d102b8abcfbcfa98f5bb6bf Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 9 Jan 2026 14:33:59 -1000
Subject: [PATCH] hook up different relation build strategies for lws

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/levelwise.cpp    | 18 +++++++++++++++++-
 src/nlsat/nlsat_params.pyg |  1 +
 src/nlsat/nlsat_solver.cpp |  4 ++++
 src/nlsat/nlsat_solver.h   |  1 +
 4 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index d72326c68..cd494db01 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -103,6 +103,21 @@ struct levelwise::impl {
         m_I.reserve(m_n);
         for (unsigned i = 0; i < m_n; ++i)
             m_I.emplace_back(m_pm);
+
+        switch (m_solver.lws_relation_mode()) {
+        case 0:
+            m_relation_mode = biggest_cell;
+            break;
+        case 1:
+            m_relation_mode = chain;
+            break;
+        case 2:
+            m_relation_mode = lowest_degree;
+            break;
+        default:
+            m_relation_mode = chain;
+            break;
+        }
     }
 
     void fail() { throw nullified_poly_exception(); }
@@ -289,7 +304,8 @@ struct levelwise::impl {
             for (unsigned j = l + 1; j < n; ++j)
                 m_rel.add_pair(j - 1, j);
             break;
-        case lowest_degree: {
+        case lowest_degree:
+        {
             std::vector<unsigned> degs;
             degs.reserve(n);
             for (unsigned i = 0; i < n; ++i)
diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg
index d15294dac..2f89b09d3 100644
--- a/src/nlsat/nlsat_params.pyg
+++ b/src/nlsat/nlsat_params.pyg
@@ -24,5 +24,6 @@ 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"),
                           ('lws', BOOL, True, "apply levelwise."),
+                          ('lws_rel_mode', UINT, 1, "relation mode for levelwise: 0 for biggest_cell, 1 for chain, 2 for lowest_degree"),
                           ('canonicalize', BOOL, True, "canonicalize polynomials.")
                           ))         
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index ba667c967..1d5d17348 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -248,6 +248,7 @@ namespace nlsat {
         stats                  m_stats;
         std::string m_debug_known_solution_file_name;
         bool m_apply_lws;
+        unsigned m_lws_relation_mode = 1;
         imp(solver& s, ctx& c):
             m_ctx(c),
             m_solver(s),
@@ -308,6 +309,7 @@ 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.lws();
+            m_lws_relation_mode = p.lws_rel_mode();
             m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
             m_cell_sample = p.cell_sample();
   
@@ -4636,5 +4638,7 @@ namespace nlsat {
 
     bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
 
+    unsigned solver::lws_relation_mode() const { return m_imp->m_lws_relation_mode; }
+
         
 };
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index b1cc29179..e45c2fd93 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -248,6 +248,7 @@ namespace nlsat {
         const assignment& sample() const;
         assignment& sample(); 
         bool apply_levelwise() const;
+        unsigned lws_relation_mode() const;
         void reset();
         void collect_statistics(statistics & st);
         void reset_statistics();