re-enable fixed tabu

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Jan 5, 2025 · f6e3c5a · f6e3c5a
1 parent 6b17862
commit f6e3c5a
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 9 deletions.
diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp
@@ -30,7 +30,7 @@ namespace sls {
 
     void bv_fixed::init() {
 
-        return;
+        //return;
 
         for (auto e : ctx.subterms())
             set_fixed(e);

diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
@@ -318,8 +318,9 @@ namespace sls {
         m_config.ucb_forget = p.walksat_ucb_forget();
         m_config.ucb_init = p.walksat_ucb_init();
         m_config.ucb_noise = p.walksat_ucb_noise();
-        m_config.use_top_level_assertions = p.use_top_level_assertions_bv();
-        m_config.use_lookahead_bv = p.use_lookahead_bv();
+        m_config.use_top_level_assertions = p.bv_use_top_level_assertions();
+        m_config.use_lookahead_bv = p.bv_use_lookahead();
+        m_config.allow_rotation = p.bv_allow_rotation();
     }
 
     /**
@@ -659,13 +660,13 @@ namespace sls {
                                 ;
                             else if (allow_costly_flips(mt))
                                 ctx.flip(v);
-                            else if (true) {
-                                sat::bool_var_set rotated;
+                            else if (m_config.allow_rotation) {
+                                m_rotated.reset();
                                 unsigned budget = 100;
-                                bool rot = ctx.try_rotate(v, rotated, budget);
+                                bool rot = ctx.try_rotate(v, m_rotated, budget);
                                 if (rot)
                                     ++m_stats.m_rotations;
-                                CTRACE("bv", rot, tout << "rotated: " << rotated << "\n";);
+                                CTRACE("bv", rot, tout << "rotated: " << m_rotated << "\n";);
                             }
                         }
                     }

diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h
@@ -48,6 +48,7 @@ namespace sls {
             double ucb_noise = 0.1;
             bool   use_top_level_assertions = true;
             bool   use_lookahead_bv = true;
+            bool   allow_rotation = true;
         };
 
         struct stats {
@@ -83,6 +84,7 @@ namespace sls {
         vector<bool_info> m_bool_info;
         expr_mark m_is_root;
         unsigned m_touched = 1;
+        sat::bool_var_set m_rotated;            
 
         std::ostream& display_weights(std::ostream& out);
 

diff --git a/src/params/sls_params.pyg b/src/params/sls_params.pyg
@@ -25,7 +25,8 @@ def_module_params('sls',
                         ('dt_axiomatic', BOOL, True, 'use axiomatic mode or model reduction for datatype solver'),
                         ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
                         ('random_seed', UINT, 0, 'random seed'),
-                        ('use_top_level_assertions_bv', BOOL, False, 'use top-level assertions for BV lookahead solver'),
-                        ('use_lookahead_bv', BOOL, True, 'use lookahead solver for BV'),
+                        ('bv_use_top_level_assertions', BOOL, False, 'use top-level assertions for BV lookahead solver'),
+                        ('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'),
+                        ('bv_allow_rotation', BOOL, True, 'allow model rotation when repairing literal assignment'),
                         ('str_update_strategy', UINT, 1, 'string update candidate selection: 0 - single character based update, 1 - subsequence based update')
               ))