diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index df3bc1515..a53b9b520 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -631,9 +631,11 @@ namespace bv { return sls_valuation::random_bits(m_rand); } - bool sls_eval::try_repair(app* e, unsigned i) { - if (e->get_family_id() == bv.get_family_id()) - return try_repair_bv(e, i); + bool sls_eval::repair_down(app* e, unsigned i) { + if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) { + ctx.new_value_eh(e->get_arg(i)); + return true; + } return false; } @@ -985,7 +987,7 @@ namespace bv { return true; } // fall back to a random value - return a.set_random(m_rand); + return i == 0 ? a.set_random(m_rand) : b.set_random(m_rand); } /** diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 9c8218dce..0edb4ab5b 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -168,7 +168,7 @@ namespace bv { * Try to invert value of child to repair value assignment of parent. */ - bool try_repair(app* e, unsigned i); + bool repair_down(app* e, unsigned i); /* * Propagate repair up to parent diff --git a/src/ast/sls/sls_bv.cpp b/src/ast/sls/sls_bv.cpp deleted file mode 100644 index 1a6cf04cd..000000000 --- a/src/ast/sls/sls_bv.cpp +++ /dev/null @@ -1,93 +0,0 @@ - -#include "ast/sls/sls_bv.h" - -namespace sls { - - bv_plugin::bv_plugin(context& ctx): - plugin(ctx), - bv(m), - m_terms(m), - m_eval(m) - {} - - void bv_plugin::init_bool_var(sat::bool_var v) { - } - - void bv_plugin::register_term(expr* e) { - } - - expr_ref bv_plugin::get_value(expr* e) { - return expr_ref(m); - } - - lbool bv_plugin::check() { - return l_undef; - } - - bool bv_plugin::is_sat() { - return false; - } - - void bv_plugin::reset() { - } - - void bv_plugin::on_rescale() { - - } - - void bv_plugin::on_restart() { - } - - std::ostream& bv_plugin::display(std::ostream& out) const { - return out; - } - - void bv_plugin::mk_model(model& mdl) { - - } - - void bv_plugin::set_shared(expr* e) { - - } - - void bv_plugin::set_value(expr* e, expr* v) { - - } - - std::pair bv_plugin::next_to_repair() { - app* e = nullptr; - if (m_repair_down != UINT_MAX) { - e = m_terms.term(m_repair_down); - m_repair_down = UINT_MAX; - return { true, e }; - } - - if (!m_repair_up.empty()) { - unsigned index = m_repair_up.elem_at(ctx.rand(m_repair_up.size())); - m_repair_up.remove(index); - e = m_terms.term(index); - return { false, e }; - } - - while (!m_repair_roots.empty()) { - unsigned index = m_repair_roots.elem_at(ctx.rand(m_repair_roots.size())); - e = m_terms.term(index); - if (m_terms.is_assertion(e) && !m_eval.bval1(e)) { - SASSERT(m_eval.bval0(e)); - return { true, e }; - } - if (!m_eval.re_eval_is_correct(e)) { - init_repair_goal(e); - return { true, e }; - } - m_repair_roots.remove(index); - } - - return { false, nullptr }; - } - - void bv_plugin::init_repair_goal(app* e) { - m_eval.init_eval(e); - } - -} diff --git a/src/ast/sls/sls_bv.h b/src/ast/sls/sls_bv.h deleted file mode 100644 index c1ad0464a..000000000 --- a/src/ast/sls/sls_bv.h +++ /dev/null @@ -1,55 +0,0 @@ -/*++ -Copyright (c) 2020 Microsoft Corporation - -Module Name: - - sls_bv.h - -Abstract: - - Theory plugin for bit-vector local search - -Author: - - Nikolaj Bjorner (nbjorner) 2024-07-06 - ---*/ -#pragma once - -#include "ast/sls/sls_smt.h" -#include "ast/bv_decl_plugin.h" -#include "ast/sls/bv_sls_terms.h" -#include "ast/sls/bv_sls_eval.h" - -namespace sls { - - class bv_plugin : public plugin { - bv_util bv; - bv::sls_terms m_terms; - bv::sls_eval m_eval; - bv::sls_stats m_stats; - - indexed_uint_set m_repair_up, m_repair_roots; - unsigned m_repair_down = UINT_MAX; - - std::pair next_to_repair(); - void init_repair_goal(app* e); - public: - bv_plugin(context& ctx); - ~bv_plugin() override {} - void init_bool_var(sat::bool_var v) override; - void register_term(expr* e) override; - expr_ref get_value(expr* e) override; - lbool check() override; - bool is_sat() override; - void reset() override; - - void on_rescale() override; - void on_restart() override; - std::ostream& display(std::ostream& out) const override; - void mk_model(model& mdl) override; - void set_shared(expr* e) override; - void set_value(expr* e, expr* v) override; - }; - -} diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp index 209576fe9..d958500e2 100644 --- a/src/ast/sls/sls_bv_plugin.cpp +++ b/src/ast/sls/sls_bv_plugin.cpp @@ -99,7 +99,6 @@ namespace sls { } void bv_plugin::repair_down(app* e) { - unsigned n = e->get_num_args(); if (n == 0 || m_eval.eval_is_correct(e)) { m_eval.commit_eval(e); @@ -110,30 +109,25 @@ namespace sls { auto d1 = get_depth(e->get_arg(0)); auto d2 = get_depth(e->get_arg(1)); unsigned s = ctx.rand(d1 + d2 + 2); - if (s <= d1 && m_eval.try_repair(e, 0)) { - ctx.new_value_eh(e->get_arg(0)); + if (s <= d1 && m_eval.repair_down(e, 0)) return; - } - if (m_eval.try_repair(e, 1)) { - ctx.new_value_eh(e->get_arg(1)); + + if (m_eval.repair_down(e, 1)) return; - } - if (m_eval.try_repair(e, 0)) { - ctx.new_value_eh(e->get_arg(0)); - return; - } + + if (m_eval.repair_down(e, 0)) + return; } else { unsigned s = ctx.rand(n); for (unsigned i = 0; i < n; ++i) { auto j = (i + s) % n; - if (m_eval.try_repair(e, j)) { - ctx.new_value_eh(e->get_arg(j)); - return; - } + if (m_eval.repair_down(e, j)) + return; } } - IF_VERBOSE(3, verbose_stream() << "init-repair " << mk_bounded_pp(e, m) << "\n"); + IF_VERBOSE(3, verbose_stream() << "revert repair: " << mk_bounded_pp(e, m) << "\n"); + repair_up(e); } void bv_plugin::repair_up(app* e) {