From 08ef4de4a6a71795df4f021d3fac0a83cf21ae2c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 23 Sep 2025 11:24:50 +0300
Subject: [PATCH] introduce shuffle

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_core.cpp | 20 ++++++++++++++------
 src/math/lp/nla_core.h   |  4 +++-
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index e5a398362..445dfe040 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -636,12 +636,20 @@ void core::erase_from_to_refine(lpvar j) {
 void core::init_to_refine() {
     TRACE(nla_solver_details, tout << "emons:" << pp_emons(*this, m_emons););
     m_to_refine.reset();
-    // Traversal order of monomials uses randomization to avoid bias.
-    // We can cache a shuffle of m_emons indices instead of using cyclic shifts
-    // The shuffle can survive backtracking points to enforce bias within a scope.
-    unsigned r = random(), sz = m_emons.number_of_monics();
-    for (unsigned k = 0; k < sz; k++) {
-        auto const & m = *(m_emons.begin() + (k + r)% sz);
+    unsigned sz = m_emons.number_of_monics();
+    // shuffle is sticky within a backtracking level
+    if (!m_emon_shuffle_valid || sz != m_emon_shuffle.size()) {
+        m_emon_shuffle.reset();
+        for (unsigned i = 0; i < sz; i++)
+            m_emon_shuffle.push_back(i);
+        random_gen rand(random());
+        shuffle(m_emon_shuffle.size(), m_emon_shuffle.data(), rand);
+        trail().push(value_trail(m_emon_shuffle_valid));
+        m_emon_shuffle_valid = true;
+    }
+
+    for (auto k : m_emon_shuffle) {
+        auto const & m = m_emons[k];
         if (!check_monic(m)) 
             insert_to_refine(m.var());
     }
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index d8fa9d78e..49d3e6900 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -78,6 +78,8 @@ class core {
     vector<ineq>             m_literals;
     vector<lp::equality>       m_equalities;
     vector<lp::fixed_equality> m_fixed_equalities;
+    unsigned_vector          m_emon_shuffle;
+    bool                     m_emon_shuffle_valid = false;
     indexed_uint_set         m_to_refine;
     indexed_uint_set         m_monics_with_changed_bounds;
     tangents                 m_tangents;
@@ -219,7 +221,7 @@ public:
 
     void set_relevant(std::function<bool(lpvar)>& is_relevant) { m_relevant = is_relevant; }
     bool is_relevant(lpvar v) const { return !m_relevant || m_relevant(v); }
-
+    
     void push();     
     void pop(unsigned n);