From 04ad63c732376240c06891b61ececb72eee3e444 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Jul 2024 14:23:47 -0700 Subject: [PATCH] fix unit test build Signed-off-by: Nikolaj Bjorner --- src/ast/sls/bv_sls.cpp | 284 ------------------------------------ src/ast/sls/bv_sls.h | 122 ---------------- src/ast/sls/bv_sls_eval.cpp | 6 +- src/ast/sls/bv_sls_eval.h | 2 + src/sat/smt/sls_solver.h | 1 - src/test/sls_test.cpp | 40 ++++- 6 files changed, 40 insertions(+), 415 deletions(-) delete mode 100644 src/ast/sls/bv_sls.cpp delete mode 100644 src/ast/sls/bv_sls.h diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp deleted file mode 100644 index 700436a8d..000000000 --- a/src/ast/sls/bv_sls.cpp +++ /dev/null @@ -1,284 +0,0 @@ -/*++ -Copyright (c) 2024 Microsoft Corporation - -Module Name: - - bv_sls.cpp - -Abstract: - - A Stochastic Local Search (SLS) engine - Uses invertibility conditions, - interval annotations - don't care annotations - -Author: - - Nikolaj Bjorner (nbjorner) 2024-02-07 - ---*/ - -#include "ast/sls/bv_sls.h" -#include "ast/ast_pp.h" -#include "ast/ast_ll_pp.h" -#include "params/sls_params.hpp" - -namespace bvu { - - sls::sls(ast_manager& m, params_ref const& p): - m(m), - bv(m), - m_terms(m), - m_eval(m) - { - updt_params(p); - } - - void sls::init() { - m_terms.init(); - } - - void sls::init_eval(std::function& eval) { - m_eval.init_eval(m_terms.assertions(), eval); - m_eval.tighten_range(m_terms.assertions()); - init_repair(); - } - - void sls::init_repair() { - 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_roots.insert(e->get_id()); - } - } - for (auto* t : m_terms.terms()) { - if (t && !m_eval.re_eval_is_correct(t)) - m_repair_roots.insert(t->get_id()); - } - } - - - void sls::set_model() { - if (!m_set_model) - return; - if (m_repair_roots.size() >= m_min_repair_size) - return; - m_min_repair_size = m_repair_roots.size(); - IF_VERBOSE(2, verbose_stream() << "(sls-update-model :num-unsat " << m_min_repair_size << ")\n"); - m_set_model(*get_model()); - } - - void sls::init_repair_goal(app* t) { - m_eval.init_eval(t); - } - - void sls::init_repair_candidates() { - m_to_repair.reset(); - ptr_vector todo; - expr_fast_mark1 mark; - for (auto index : m_repair_roots) - todo.push_back(m_terms.term(index)); - for (unsigned i = 0; i < todo.size(); ++i) { - expr* e = todo[i]; - if (mark.is_marked(e)) - continue; - mark.mark(e); - if (!is_app(e)) - continue; - for (expr* arg : *to_app(e)) - todo.push_back(arg); - - if (is_uninterp_const(e)) - m_to_repair.insert(e->get_id()); - - } - } - - - void sls::reinit_eval() { - init_repair(); - } - - - std::pair sls::next_to_repair() { -#if 0 - 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(m_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(m_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); - } -#endif - return { false, nullptr }; - } - - lbool sls::search1() { - // init and init_eval were invoked - unsigned n = 0; - for (; n < m_config.m_max_repairs && m.inc(); ++n) { - auto [down, e] = next_to_repair(); - if (!e) - return l_true; - - IF_VERBOSE(20, trace_repair(down, e)); - - ++m_stats.m_moves; - if (down) - try_repair_down(e); - else - try_repair_up(e); - } - return l_undef; - } - - - lbool sls::operator()() { - lbool res = l_undef; - m_stats.reset(); - m_stats.m_restarts = 0; - - do { - res = search1(); - if (res != l_undef) - break; - trace(); - reinit_eval(); - } - while (m.inc() && m_stats.m_restarts++ < m_config.m_max_restarts); - - return res; - } - - void sls::try_repair_down(app* e) { - unsigned n = e->get_num_args(); - if (n == 0) { - m_eval.commit_eval(e); - for (auto p : m_terms.parents(e)) - m_repair_up.insert(p->get_id()); - - return; - } - - if (n == 2) { - auto d1 = get_depth(e->get_arg(0)); - auto d2 = get_depth(e->get_arg(1)); - unsigned s = m_rand(d1 + d2 + 2); - if (s <= d1 && m_eval.try_repair(e, 0)) { - set_repair_down(e->get_arg(0)); - return; - } - if (m_eval.try_repair(e, 1)) { - set_repair_down(e->get_arg(1)); - return; - } - if (m_eval.try_repair(e, 0)) { - set_repair_down(e->get_arg(0)); - return; - } - } - else { - unsigned s = m_rand(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; - } - } - } - IF_VERBOSE(3, verbose_stream() << "init-repair " << mk_bounded_pp(e, m) << "\n"); - // repair was not successful, so reset the state to find a different way to repair - init_repair(); - } - - void sls::try_repair_up(app* e) { - - if (m_terms.is_assertion(e)) - m_repair_roots.insert(e->get_id()); - else if (!m_eval.repair_up(e)) { - IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e)); - if (m_rand(10) != 0) { - m_eval.set_random(e); - m_repair_roots.insert(e->get_id()); - } - else - init_repair(); - } - else { - if (!m_eval.eval_is_correct(e)) { - verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; - } - SASSERT(m_eval.eval_is_correct(e)); - for (auto p : m_terms.parents(e)) - m_repair_up.insert(p->get_id()); - } - } - - std::ostream& sls::display(std::ostream& out) { -#if 0 - auto& terms = m_eval.sort_assertions(m_terms.assertions()); - for (expr* e : terms) { - out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " "; - if (m_eval.is_fixed0(e)) - out << "f "; - if (m_repair_up.contains(e->get_id())) - out << "u "; - if (m_repair_roots.contains(e->get_id())) - out << "r "; - m_eval.display_value(out, e); - out << "\n"; - } - terms.reset(); -#endif - return out; - } - - void sls::updt_params(params_ref const& _p) { - sls_params p(_p); - m_config.m_max_restarts = p.max_restarts(); - m_config.m_max_repairs = p.max_repairs(); - m_rand.set_seed(p.random_seed()); - m_terms.updt_params(_p); - params_ref q = _p; - q.set_uint("max_restarts", 10); - } - - std::ostream& sls::trace_repair(bool down, expr* e) { - verbose_stream() << (down ? "d #" : "u #") - << e->get_id() << ": " - << mk_bounded_pp(e, m, 1) << " "; - m_eval.display_value(verbose_stream(), e) << "\n"; - return verbose_stream(); - } - - 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 deleted file mode 100644 index c72e1d172..000000000 --- a/src/ast/sls/bv_sls.h +++ /dev/null @@ -1,122 +0,0 @@ -/*++ -Copyright (c) 2024 Microsoft Corporation - -Module Name: - - bv_sls.h - -Abstract: - - A Stochastic Local Search (SLS) engine - -Author: - - Nikolaj Bjorner (nbjorner) 2024-02-07 - ---*/ -#pragma once - -#include "util/lbool.h" -#include "util/params.h" -#include "util/scoped_ptr_vector.h" -#include "util/uint_set.h" -#include "ast/ast.h" -#include "ast/sls/sls_stats.h" -#include "ast/sls/sls_powers.h" -#include "ast/sls/sls_valuation.h" -#include "ast/sls/bv_sls_terms.h" -#include "ast/sls/bv_sls_eval.h" -#include "ast/bv_decl_plugin.h" -#include "model/model.h" - -namespace bvu { - - - class sls { - - struct config { - unsigned m_max_restarts = 1000; - unsigned m_max_repairs = 1000; - }; - - ast_manager& m; - 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; - ptr_vector m_todo; - random_gen m_rand; - config m_config; - bool m_engine_model = false; - bool m_engine_init = false; - std::function m_get_unit; - std::function m_set_model; - unsigned m_min_repair_size = UINT_MAX; - - std::pair next_to_repair(); - - void init_repair_goal(app* e); - void set_model(); - void try_repair_down(app* e); - void try_repair_up(app* e); - void set_repair_down(expr* e) { m_repair_down = e->get_id(); } - - lbool search1(); - lbool search2(); - void reinit_eval(); - void init_repair(); - void trace(); - std::ostream& trace_repair(bool down, expr* e); - - indexed_uint_set m_to_repair; - void init_repair_candidates(); - - public: - sls(ast_manager& m, params_ref const& p); - - /* - * Invoke init after all expressions are asserted. - */ - void init(); - - /** - * Invoke init_eval to initialize, or re-initialize, values of - * uninterpreted constants. - */ - void init_eval(std::function& eval); - - /** - * add callback to retrieve new units - */ - void init_unit(std::function get_unit) { m_get_unit = get_unit; } - - /** - * Add callback to set model - */ - void set_model(std::function f) { m_set_model = f; } - - /** - * Run (bounded) local search to find feasible assignments. - */ - lbool operator()(); - - void updt_params(params_ref const& p); - void collect_statistics(statistics& st) const { m_stats.collect_statistics(st); } - void reset_statistics() { m_stats.reset(); } - - unsigned get_num_moves() { return m_stats.m_moves; } - - std::ostream& display(std::ostream& out); - - /** - * Retrieve valuation - */ - bv::sls_valuation const& wval(expr* e) const { return m_eval.wval(e); } - - model_ref get_model(); - - void cancel() { m.limit().cancel(); } - }; -} diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 28bb2153b..df3bc1515 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -13,7 +13,7 @@ Author: #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" -#include "ast/sls/bv_sls.h" +#include "ast/sls/bv_sls_eval.h" #include "ast/rewriter/th_rewriter.h" namespace bv { @@ -206,6 +206,10 @@ namespace bv { return val; } + void sls_eval::set(expr* e, sls_valuation const& val) { + m_values[e->get_id()]->set(val.bits()); + } + void sls_eval::eval(app* e, sls_valuation& val) const { SASSERT(bv.is_bv(e)); if (m.is_ite(e)) { diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 794f5f2bd..9c8218dce 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -148,6 +148,8 @@ namespace bv { sls_valuation& wval(expr* e) const; + void set(expr* e, sls_valuation const& val); + bool is_fixed0(expr* e) const { return m_fixed.get(e->get_id(), false); } sls_valuation& eval(app* e) const; diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h index e04b82055..696867157 100644 --- a/src/sat/smt/sls_solver.h +++ b/src/sat/smt/sls_solver.h @@ -18,7 +18,6 @@ Author: #include "util/rlimit.h" -#include "ast/sls/bv_sls.h" #include "ast/sls/sat_ddfw.h" #include "sat/smt/sat_th.h" diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp index d99035398..74f5c17df 100644 --- a/src/test/sls_test.cpp +++ b/src/test/sls_test.cpp @@ -1,10 +1,32 @@ #include "ast/sls/bv_sls_eval.h" +#include "ast/sls/bv_sls_terms.h" #include "ast/rewriter/th_rewriter.h" #include "ast/reg_decl_plugins.h" #include "ast/ast_pp.h" namespace bv { + + class my_sat_solver_context : public sls::sat_solver_context { + vector m_clauses; + indexed_uint_set s; + public: + my_sat_solver_context() {} + + vector const& clauses() const override { return m_clauses; } + sat::clause_info const& get_clause(unsigned idx) const override { return m_clauses[idx]; } + ptr_iterator get_use_list(sat::literal lit) override { return ptr_iterator(nullptr, nullptr); } + void flip(sat::bool_var v) override {} + double reward(sat::bool_var v) override { return 0; } + double get_weigth(unsigned clause_idx) override { return 0; } + bool is_true(sat::literal lit) override { return true; } + unsigned num_vars() const override { return 0; } + indexed_uint_set const& unsat() const override { return s; } + void on_model(model_ref& mdl) override {} + sat::bool_var add_var() override { return sat::null_bool_var;} + void add_clause(unsigned n, sat::literal const* lits) override {} + }; + class sls_test { ast_manager& m; bv_util bv; @@ -28,9 +50,11 @@ namespace bv { expr_ref_vector es(m); bv_util bv(m); es.push_back(e); - sls_eval ev(m); - ev.init_eval(es, value); - ev.tighten_range(es); + + my_sat_solver_context solver; + sls::context ctx(m, solver); + sls_terms terms(ctx); + sls_eval ev(terms, ctx); th_rewriter rw(m); expr_ref r(e, m); rw(r); @@ -142,9 +166,11 @@ namespace bv { rw(r); es.push_back(m.is_false(r) ? m.mk_not(e1) : e1); es.push_back(m.is_false(r) ? m.mk_not(e2) : e2); - sls_eval ev(m); - ev.init_eval(es, value); - ev.tighten_range(es); + + my_sat_solver_context solver; + sls::context ctx(m, solver); + sls_terms terms(ctx); + sls_eval ev(terms, ctx); if (m.is_bool(e1)) { SASSERT(m.is_true(r) || m.is_false(r)); @@ -159,7 +185,7 @@ namespace bv { auto val3 = ev.bval0(e2); if (val3 != val) { verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n"; - ev.display(std::cout, es); + ev.display(std::cout); exit(0); } //SASSERT(rep1);