From 0b9ed925d65cdcd202d99454aa6b74191fc82e0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2024 13:34:48 -0800 Subject: [PATCH] try dual phase lookahead Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_eval.cpp | 11 ++++++++++- src/ast/sls/sls_bv_eval.h | 4 ++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index d2332deee..5522076a0 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/src/ast/sls/sls_bv_eval.cpp @@ -674,12 +674,21 @@ namespace sls { return false; } } + + bool bv_eval::is_lookahead_phase() { + ++m_lookahead_steps; + if (m_lookahead_steps < m_lookahead_phase_size) + return true; + if (m_lookahead_steps > 2 * m_lookahead_phase_size) + m_lookahead_steps = 0; + return false; + } bool bv_eval::repair_down(app* e, unsigned i) { expr* arg = e->get_arg(i); if (m.is_value(arg)) return false; - if (false && m.is_bool(e) && ctx.rand(10) == 0 && m_lookahead.try_repair_down(e)) + if (m.is_bool(e) && is_lookahead_phase() && m_lookahead.try_repair_down(e)) return true; if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) { commit_eval(e, to_app(arg)); diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h index 2314c2895..b6ac73e63 100644 --- a/src/ast/sls/sls_bv_eval.h +++ b/src/ast/sls/sls_bv_eval.h @@ -52,6 +52,8 @@ namespace sls { random_gen m_rand; config m_config; bool_vector m_fixed; + unsigned m_lookahead_steps = 0; + unsigned m_lookahead_phase_size = 100; scoped_ptr_vector m_values; // expr-id -> bv valuation @@ -147,6 +149,8 @@ namespace sls { void commit_eval(expr* p, app* e); + bool is_lookahead_phase(); + public: bv_eval(sls::bv_terms& terms, sls::context& ctx);