From 7e4681d8365a07c95698e1a9732ded33093b75d1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 3 Jan 2025 11:49:39 -0800
Subject: [PATCH] enable rotation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_bv_lookahead.cpp | 19 +++++++++++--------
 src/ast/sls/sls_bv_lookahead.h   |  7 ++++---
 2 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index 2e24d0c1a..1bdc5f260 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -39,7 +39,7 @@ namespace sls {
     */
     void bv_lookahead::start_propagation() {
         //verbose_stream() << "start_propagation " << m_stats.m_num_propagations << "\n";
-        if (m_stats.m_num_propagations++ % m_config.propagation_base == 0) 
+        if (m_stats.m_propagations++ % m_config.propagation_base == 0) 
             search();        
     }
 
@@ -117,7 +117,7 @@ namespace sls {
         auto& v = wval(e);
         m_v_updated.set_bw(v.bw);
         v.get_variant(m_v_updated, m_ev.m_rand);
-        ++m_stats.random_flip_count;
+        ++m_stats.m_random_flips;
         return apply_update(m_last_atom, e, m_v_updated, move_type::random_t);
     }
 
@@ -438,7 +438,7 @@ namespace sls {
         if (!wval(u).can_set(new_value))
             return;
         auto score = lookahead_update(u, new_value);
-        ++m_stats.m_num_lookaheads;
+        ++m_stats.m_lookaheads;
         //verbose_stream() << mk_bounded_pp(u, m) << " := " << new_value << " score: " << score << "\n";
         if (score > m_best_score) {
             m_best_score = score;
@@ -455,7 +455,7 @@ namespace sls {
             return;
         auto score = lookahead_flip(v);
         //verbose_stream() << "lookahead flip " << mk_bounded_pp(u, m) << " score: " << score << "\n";
-        ++m_stats.m_num_lookaheads;
+        ++m_stats.m_lookaheads;
         if (score > m_best_score) {
             m_best_score = score;
             m_best_expr = u;
@@ -589,13 +589,15 @@ namespace sls {
 #if 1
                         if (allow_costly_flips(mt))
                             ctx.flip(v);                        
-                        else if (false) {
+                        else if (true) {
                             sat::bool_var_set rotated;
                             unsigned budget = 100;
                             bool rot = ctx.try_rotate(v, rotated, budget);
+                            if (rot)
+                                ++m_stats.m_rotations;
                             (void)rot;
                             TRACE("bv", tout << "rotate " << v << " " << rot << " " << rotated << "\n";);
-                            verbose_stream() << "rotate " << v << " " << rot << " " << rotated << "\n";
+                            //verbose_stream() << "rotate " << v << " " << rot << " " << rotated << "\n";
                         }
 #endif
                         
@@ -625,7 +627,7 @@ namespace sls {
             return true;
         if (mt != move_type::random_t)
             return false;
-        return m_stats.random_flip_count % 100 == 0;
+        return m_stats.m_random_flips % 100 == 0;
     }
 
     void bv_lookahead::insert_update(expr* e) {
@@ -737,8 +739,9 @@ namespace sls {
     }
 
     void bv_lookahead::collect_statistics(statistics& st) const {
-        st.update("sls-bv-lookaheads", m_stats.m_num_lookaheads);
+        st.update("sls-bv-lookaheads", m_stats.m_lookaheads);
         st.update("sls-bv-moves", m_stats.m_moves);
         st.update("sls-bv-restarts", m_stats.m_restarts);
+        st.update("sls-bv-rotations", m_stats.m_rotations);
     }
 }
\ No newline at end of file
diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h
index 4b01d0e97..c15558d6f 100644
--- a/src/ast/sls/sls_bv_lookahead.h
+++ b/src/ast/sls/sls_bv_lookahead.h
@@ -49,11 +49,12 @@ namespace sls {
         };
 
         struct stats {
-            unsigned m_num_lookaheads = 0;
+            unsigned m_lookaheads = 0;
             unsigned m_moves = 0;
             unsigned m_restarts = 0;
-            unsigned m_num_propagations = 0;
-            unsigned random_flip_count = 0;
+            unsigned m_propagations = 0;
+            unsigned m_random_flips = 0;
+            unsigned m_rotations = 0;
         };
 
         struct bool_info {