From a328366c7d0a533ac964080660b58ee63cbc1e1b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Feb 2024 19:05:16 -0800 Subject: [PATCH] move to single path mode for search Signed-off-by: Nikolaj Bjorner --- src/ast/sls/bv_sls.cpp | 108 ++++++++++++++++++++++------------------- src/ast/sls/bv_sls.h | 7 +-- 2 files changed, 61 insertions(+), 54 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index e091eb4b526..bdc2584623f 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -43,17 +43,18 @@ namespace bv { } void sls::init_repair() { - m_repair_down.reset(); + m_repair_down = UINT_MAX; m_repair_up.reset(); + m_repair_roots.reset(); for (auto* e : m_terms.assertions()) { if (!m_eval.bval0(e)) { m_eval.set(e, true); - m_repair_down.insert(e->get_id()); + m_repair_roots.insert(e->get_id()); } } for (app* t : m_terms.terms()) if (t && !eval_is_correct(t)) - m_repair_down.insert(t->get_id()); + m_repair_roots.insert(t->get_id()); } void sls::reinit_eval() { @@ -78,15 +79,27 @@ namespace bv { std::pair sls::next_to_repair() { app* e = nullptr; - if (!m_repair_down.empty()) { - unsigned index = m_rand(m_repair_down.size()); - e = m_terms.term(m_repair_down.elem_at(index)); + if (m_repair_down != UINT_MAX) { + e = m_terms.term(m_repair_down); + m_repair_down = UINT_MAX; + return { true, e }; } - else if (!m_repair_up.empty()) { + + if (!m_repair_up.empty()) { unsigned index = m_rand(m_repair_up.size()); + m_repair_up.remove(index); e = m_terms.term(m_repair_up.elem_at(index)); + return { false, e }; } - return { !m_repair_down.empty(), e }; + + if (!m_repair_roots.empty()) { + unsigned index = m_rand(m_repair_up.size()); + e = m_terms.term(m_repair_up.elem_at(index)); + m_repair_roots.remove(index); + return { true, e }; + } + + return { false, nullptr }; } lbool sls::search() { @@ -97,35 +110,19 @@ namespace bv { auto [down, e] = next_to_repair(); if (!e) return l_true; - bool is_correct = eval_is_correct(e); - if (is_correct) { - if (down) - m_repair_down.remove(e->get_id()); - else - m_repair_up.remove(e->get_id()); - } - else { - IF_VERBOSE(20, verbose_stream() << (down ? "d #" : "u #") - << e->get_id() << ": " - << mk_bounded_pp(e, m, 1) << " "; - if (bv.is_bv(e)) verbose_stream() << m_eval.wval0(e) << " " << (m_eval.is_fixed0(e)?"fixed ":" "); - if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " "; - verbose_stream() << "\n"); - if (down) - try_repair_down(e); - else - try_repair_up(e); - } + if (eval_is_correct(e)) + continue; + + trace_repair(down, e); + + if (down) + try_repair_down(e); + else + try_repair_up(e); } return l_undef; } - void sls::trace() { - IF_VERBOSE(2, verbose_stream() - << "(bvsls :restarts " << m_stats.m_restarts - << " :repair-down " << m_repair_down.size() - << " :repair-up " << m_repair_up.size() << ")\n"); - } lbool sls::operator()() { lbool res = l_undef; @@ -147,29 +144,21 @@ namespace bv { unsigned n = e->get_num_args(); if (n > 0) { unsigned s = m_rand(n); - for (unsigned i = 0; i < n; ++i) - if (try_repair_down(e, (i + s) % n)) + for (unsigned i = 0; i < n; ++i) { + auto j = (i + s) % n; + if (m_eval.try_repair(e, j)) { + set_repair_down(e->get_arg(j)); return; + } + } } - m_repair_down.remove(e->get_id()); m_repair_up.insert(e->get_id()); } - bool sls::try_repair_down(app* e, unsigned i) { - expr* child = e->get_arg(i); - bool was_repaired = m_eval.try_repair(e, i); - if (was_repaired) { - m_repair_down.insert(child->get_id()); - for (auto p : m_terms.parents(child)) - m_repair_up.insert(p->get_id()); - } - return was_repaired; - } - void sls::try_repair_up(app* e) { - m_repair_up.remove(e->get_id()); + if (m_terms.is_assertion(e) || !m_eval.repair_up(e)) - m_repair_down.insert(e->get_id()); + m_repair_roots.insert(e->get_id()); else { if (!eval_is_correct(e)) { verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; @@ -225,10 +214,10 @@ namespace bv { out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " "; if (m_eval.is_fixed0(e)) out << "f "; - if (m_repair_down.contains(e->get_id())) - out << "d "; if (m_repair_up.contains(e->get_id())) out << "u "; + if (m_repair_roots.contains(e->get_id())) + out << "r "; if (bv.is_bv(e)) out << m_eval.wval0(e); else if (m.is_bool(e)) @@ -244,4 +233,21 @@ namespace bv { m_config.m_max_restarts = p.max_restarts(); m_rand.set_seed(p.random_seed()); } + + void sls::trace_repair(bool down, expr* e) { + IF_VERBOSE(20, + verbose_stream() << (down ? "d #" : "u #") + << e->get_id() << ": " + << mk_bounded_pp(e, m, 1) << " "; + if (bv.is_bv(e)) verbose_stream() << m_eval.wval0(e) << " " << (m_eval.is_fixed0(e) ? "fixed " : " "); + if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " "; + verbose_stream() << "\n"); + } + + void sls::trace() { + IF_VERBOSE(2, verbose_stream() + << "(bvsls :restarts " << m_stats.m_restarts + << " :repair-up " << m_repair_up.size() + << " :repair-roots " << m_repair_roots.size() << ")\n"); + } } diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index be2e8feed0c..d92f991dba5 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -44,7 +44,8 @@ namespace bv { sls_terms m_terms; sls_eval m_eval; sls_stats m_stats; - indexed_uint_set m_repair_down, m_repair_up; + indexed_uint_set m_repair_up, m_repair_roots; + unsigned m_repair_down = UINT_MAX; ptr_vector m_todo; random_gen m_rand; config m_config; @@ -54,13 +55,13 @@ namespace bv { bool eval_is_correct(app* e); void try_repair_down(app* e); void try_repair_up(app* e); - - bool try_repair_down(app* e, unsigned i); + void set_repair_down(expr* e) { m_repair_down = e->get_id(); } lbool search(); void reinit_eval(); void init_repair(); void trace(); + void trace_repair(bool down, expr* e); public: sls(ast_manager& m);