From beb9d2e55316e3b8de00bad5b821861996bc388c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Jan 2025 21:40:35 -0800 Subject: [PATCH] update restart next Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sat_ddfw.cpp | 2 +- src/ast/sls/sls_smt_plugin.cpp | 4 ++-- src/smt/theory_sls.cpp | 1 - 3 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp index 390296098..a70f455f7 100644 --- a/src/ast/sls/sat_ddfw.cpp +++ b/src/ast/sls/sat_ddfw.cpp @@ -232,7 +232,7 @@ namespace sat { m_reinit_next = m_config.m_reinit_base; m_restart_count = 0; - m_restart_next = m_config.m_restart_base*2; + m_restart_next = m_config.m_restart_base; m_min_sz = m_clauses.size(); m_flips = 0; diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp index bd5b669ad..09a2f3a38 100644 --- a/src/ast/sls/sls_smt_plugin.cpp +++ b/src/ast/sls/sls_smt_plugin.cpp @@ -211,7 +211,7 @@ namespace sls { m_sat_phase[v] = ctx.get_best_phase(v); } - bool smt_plugin::export_to_sls() { + bool smt_plugin::export_to_sls() { bool updated = false; if (m_has_units) { std::lock_guard lock(m_mutex); @@ -275,7 +275,7 @@ namespace sls { void smt_plugin::sls_phase_to_smt() { if (!m_has_new_sls_phase) return; - IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase " << m_min_unsat_size << "\n"); + IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase. unsat size: " << m_min_unsat_size << "\n"); for (auto v : m_shared_bool_vars) ctx.force_phase(sat::literal(v, !m_sls_phase[v])); m_has_new_sls_phase = false; diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp index cd144ce48..8a9e1a581 100644 --- a/src/smt/theory_sls.cpp +++ b/src/smt/theory_sls.cpp @@ -243,7 +243,6 @@ namespace smt { verbose_stream() << "\n"; } #endif - for (auto const& cl : m_shared_clauses) if (all_of(cl, [this](sat::literal lit) { return ctx.get_assignment(lit) != l_true; })) return false;