From 9b8558ed925ec0d5e2248c2645bdfbc57232adb9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 30 Dec 2025 17:32:21 -0800
Subject: [PATCH] throttle decision rounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/lp_settings.h       |  2 ++
 src/math/lp/nla_stellensatz.cpp | 11 ++++++++++-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 784237603..7f18e2359 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -146,6 +146,7 @@ struct statistics {
         unsigned m_num_vanishings = 0;
         unsigned m_num_model_repairs = 0;
         unsigned m_num_backtracks = 0;
+        unsigned m_num_decisions = 0;
     };
     stellensatz m_stellensatz;
 
@@ -195,6 +196,7 @@ struct statistics {
         st.update("arith-nla-stellensatz-model-repairs", m_stellensatz.m_num_model_repairs);
         st.update("arith-nla-stellensatz-backtracks", m_stellensatz.m_num_backtracks);
         st.update("arith-nla-stellensatz-constraints", m_stellensatz.m_num_constraints);
+        st.update("arith-nla-stellensatz-decisions", m_stellensatz.m_num_decisions);
         st.copy(m_st);
     }
 };
diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp
index 34b4f02a9..13fab9456 100644
--- a/src/math/lp/nla_stellensatz.cpp
+++ b/src/math/lp/nla_stellensatz.cpp
@@ -1236,9 +1236,13 @@ namespace nla {
         lp::lconstraint_kind k;       
 
         unsigned num_fixed = 0;
+        unsigned num_levels = m_level2var.size();
+        unsigned num_rounds = 0;
+        unsigned max_rounds = num_levels * 5;
         m_tabu.reset();
-        for (unsigned level = 0; level < m_level2var.size(); ++level) {
+        for (unsigned level = 0; level < num_levels && c().reslim().inc() && num_rounds < max_rounds; ++level) {
             auto w = m_level2var[level];
+            ++num_rounds;
             lp::constraint_index conflict = repair_variable(w);
             TRACE(arith, display_constraint(tout << "repair lvl:" << level << " v" << w << ": ", conflict) 
                 << " in bounds " << in_bounds(w) 
@@ -1265,6 +1269,7 @@ namespace nla {
             }
 
             if (is_fixed(w) && level > num_fixed) {
+                // swap this variable level with another so it is solved before non-fixed variables
                 IF_VERBOSE(3, verbose_stream() << "fixed v" << w << " cannot be repaired " << level << "\n";
                            display_constraint(verbose_stream(), conflict) << "\n");
                 move_up(w);
@@ -1273,6 +1278,9 @@ namespace nla {
                 continue;
             }
             
+            // TODO: figure out when to apply splits.
+            // they can be deferred to after repair has finished and some
+            // constraint remains false.
             find_split(w, value, k, conflict);
             if (is_fixed(w))
                 continue;
@@ -1292,6 +1300,7 @@ namespace nla {
             SASSERT(in_bounds(w));
             SASSERT(well_formed_var(w));
             SASSERT(well_formed_last_bound());
+            ++c().lp_settings().stats().m_stellensatz.m_num_decisions;
             return true;
         }
         return false;