From f6e3c5ae79ea135a67b93a421366c357dadb623a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Jan 2025 11:49:12 -0800 Subject: [PATCH] re-enable fixed tabu Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_fixed.cpp | 2 +- src/ast/sls/sls_bv_lookahead.cpp | 13 +++++++------ src/ast/sls/sls_bv_lookahead.h | 2 ++ src/params/sls_params.pyg | 5 +++-- 4 files changed, 13 insertions(+), 9 deletions(-) diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp index b2d9f639ee..d8854a9d91 100644 --- 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 index 57b0732860..bc53da2172 100644 --- 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 index 8c3de7d24b..0849a1769f 100644 --- 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 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 index 75345379b2..29f64d5667 100644 --- 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') ))