From cb61af04968a24f86aae58d46862fe1183e21ab4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Jan 2025 14:34:09 -0800 Subject: [PATCH] fix restart counters Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_lookahead.cpp | 41 +++++++++++++++++++++----------- src/ast/sls/sls_bv_lookahead.h | 1 + src/ast/sls/sls_bv_plugin.cpp | 8 ++++--- 3 files changed, 33 insertions(+), 17 deletions(-) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 5559d3dbe..c19a0894a 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -56,7 +56,7 @@ namespace sls { rescore(); m_config.max_moves = m_stats.m_moves + m_config.max_moves_base; TRACE("bv", tout << "search " << m_stats.m_moves << " " << m_config.max_moves << "\n";); - IF_VERBOSE(3, verbose_stream() << "lookahead-search moves:" << m_stats.m_moves << " max-moves:" << m_config.max_moves << "\n"); + IF_VERBOSE(1, verbose_stream() << "lookahead-search moves:" << m_stats.m_moves << " max-moves:" << m_config.max_moves << "\n"); while (m.inc() && m_stats.m_moves < m_config.max_moves) { m_stats.m_moves++; @@ -106,6 +106,7 @@ namespace sls { return false; expr* e = vars[ctx.rand(vars.size())]; if (m.is_bool(e)) { + TRACE("bv", tout << "random flip " << mk_bounded_pp(e, m) << "\n";); ctx.flip(ctx.atom2bool_var(e)); return true; } @@ -124,6 +125,7 @@ namespace sls { return false; expr* e = vars[ctx.rand(vars.size())]; if (m.is_bool(e)) { + TRACE("bv", tout << "random move flip " << mk_bounded_pp(e, m) << "\n";); ctx.flip(ctx.atom2bool_var(e)); return true; } @@ -204,6 +206,7 @@ namespace sls { return; ++m_stats.m_restarts; + m_config.restart_next = std::max(m_config.restart_next, m_stats.m_moves); if (0x1 == (m_stats.m_restarts & 0x1)) m_config.restart_next += m_config.restart_base; @@ -259,6 +262,9 @@ namespace sls { void bv_lookahead::updt_params(params_ref const& _p) { sls_params p(_p); + if (m_config.updated) + return; + m_config.updated = true; m_config.walksat = p.walksat(); m_config.walksat_repick = p.walksat_repick(); m_config.paws_sp = p.paws_sp(); @@ -365,7 +371,7 @@ namespace sls { double bv_lookahead::lookahead_flip(sat::bool_var v) { auto a = ctx.atom(v); - return -1000; + return lookahead_update(a, m_v_updated); } /** @@ -373,16 +379,21 @@ namespace sls { * Walk all parents, until hitting predicates where their scores are computed. */ double bv_lookahead::lookahead_update(expr* t, bvect const& new_value) { - SASSERT(bv.is_bv(t)); + SASSERT(bv.is_bv(t) || m.is_bool(t)); SASSERT(is_uninterp(t)); SASSERT(m_restore.empty()); double score = m_top_score; - if (!wval(t).can_set(new_value)) - return -1000000; + if (bv.is_bv(t)) { + if (!wval(t).can_set(new_value)) + return -1000000; + wval(t).eval = new_value; + insert_update(t); + } + else if (m.is_bool(t)) { + m_ev.set_bool_value(t, !m_ev.bval0(t)); + } - wval(t).eval = new_value; - insert_update(t); insert_update_stack(t); unsigned max_depth = get_depth(t); for (unsigned depth = max_depth; depth <= max_depth; ++depth) { @@ -430,6 +441,7 @@ namespace sls { void bv_lookahead::try_flip(expr* u) { auto v = ctx.atom2bool_var(u); + //verbose_stream() << mk_bounded_pp(u, m) << " flip " << v << "\n"; if (v == sat::null_bool_var) return; auto score = lookahead_flip(v); @@ -526,14 +538,15 @@ namespace sls { wval(e).commit_eval_ignore_tabu(); } else if (m.is_bool(e)) { - auto v0 = m_ev.get_bool_value(to_app(e)); - auto v1 = m_ev.bval1(to_app(e)); - if (v0 == v1) - continue; - m_ev.set_bool_value(to_app(e), v1); auto v = ctx.atom2bool_var(e); - if (v != sat::null_bool_var) + auto v1 = m_ev.bval1(to_app(e)); + if (v != sat::null_bool_var) { + if (ctx.is_true(v) == v1) + continue; + TRACE("bv", tout << "update flip " << mk_bounded_pp(e, m) << "\n";); ctx.flip(v); + } + m_ev.set_bool_value(to_app(e), v1); } else continue; @@ -547,7 +560,7 @@ namespace sls { } m_in_update_stack.reset(); m_ev.clear_bool_values(); - TRACE("bv", tout << reason << " " << mk_bounded_pp(m_best_expr, m) + TRACE("bv", tout << reason << " " << mk_bounded_pp(e, m) << " := " << new_value << " score " << m_top_score << "\n";); return true; diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h index 9edb1bcdf..5cc951ee3 100644 --- a/src/ast/sls/sls_bv_lookahead.h +++ b/src/ast/sls/sls_bv_lookahead.h @@ -26,6 +26,7 @@ namespace sls { class bv_lookahead { struct config { + bool updated = false; double cb = 2.85; unsigned paws_init = 40; unsigned paws_sp = 52; diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp index 590d02570..c45c6bdd6 100644 --- a/src/ast/sls/sls_bv_plugin.cpp +++ b/src/ast/sls/sls_bv_plugin.cpp @@ -47,8 +47,9 @@ namespace sls { m_eval.start_propagation(); } - void bv_plugin::propagate_literal(sat::literal lit) { - SASSERT(ctx.is_true(lit)); + void bv_plugin::propagate_literal(sat::literal lit) { + if (!ctx.is_true(lit)) + return; auto e = ctx.atom(lit.var()); if (!is_bv_predicate(e)) return; @@ -157,7 +158,8 @@ namespace sls { } void bv_plugin::repair_literal(sat::literal lit) { - SASSERT(ctx.is_true(lit)); + if (!ctx.is_true(lit)) + return; auto e = ctx.atom(lit.var()); if (!is_bv_predicate(e)) return;