From 4391c909609d0b03d3ad540e66338cc21fd2e43e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Feb 2024 15:32:53 +0700 Subject: [PATCH] na --- src/ast/sls/bv_sls.cpp | 58 +++++++++++++++++++++++------------ src/ast/sls/bv_sls.h | 5 +-- src/ast/sls/bv_sls_eval.cpp | 42 ++++++++++++++++++++++--- src/ast/sls/bv_sls_eval.h | 1 + src/ast/sls/bv_sls_fixed.cpp | 5 +-- src/ast/sls/sls_stats.h | 7 +++-- src/ast/sls/sls_valuation.cpp | 1 + src/ast/sls/sls_valuation.h | 23 +++++++++----- src/tactic/sls/sls_tactic.cpp | 40 +++++++++++++----------- 9 files changed, 126 insertions(+), 56 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index 0b136d3901b..7476c56e92f 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -21,6 +21,7 @@ Module Name: #include "ast/sls/bv_sls.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" +#include "params/sls_params.hpp" namespace bv { @@ -48,15 +49,17 @@ namespace bv { void sls::reinit_eval() { std::function eval = [&](expr* e, unsigned i) { + auto should_keep = [&]() { + return m_rand() % 100 >= 95; + }; if (m.is_bool(e)) { - if (m_eval.is_fixed0(e)) + if (m_eval.is_fixed0(e) || should_keep()) return m_eval.bval0(e); } else if (bv.is_bv(e)) { auto& w = m_eval.wval0(e); - if (w.get(w.fixed, i)) - return w.get(w.bits, i); - + if (w.get(w.fixed, i) || should_keep()) + return w.get(w.bits, i); } return m_rand() % 2 == 0; }; @@ -77,7 +80,7 @@ namespace bv { unsigned index = m_rand(m_repair_down.size()); e = m_terms.term(m_repair_down.elem_at(index)); } - else if (m_repair_up.empty()) { + else if (!m_repair_up.empty()) { unsigned index = m_rand(m_repair_up.size()); e = m_terms.term(m_repair_up.elem_at(index)); } @@ -85,43 +88,51 @@ namespace bv { } lbool sls::search() { - // init and init_eval were invoked. - unsigned& n = m_stats.m_moves; - n = 0; - for (; n < m_config.m_max_repairs && m.inc(); ++n) { + // init and init_eval were invoked + unsigned n = 0; + for (; n++ < m_config.m_max_repairs && m.inc(); ) { + ++m_stats.m_moves; auto [down, e] = next_to_repair(); if (!e) return l_true; - IF_VERBOSE(20, verbose_stream() << (down ? "d " : "u ") << mk_bounded_pp(e, m, 1) << "\n"); + 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); + verbose_stream() << "\n"); if (eval_is_correct(e)) { if (down) m_repair_down.remove(e->get_id()); else m_repair_up.remove(e->get_id()); } - else if (down) { - try_repair_down(e); - } + else 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; + m_stats.reset(); + m_stats.m_restarts = 0; do { - if (!m.inc()) - return l_undef; - res = search(); - if (res != l_undef) - return res; - + break; + trace(); reinit_eval(); } - while (m_stats.m_restarts++ < m_config.m_max_restarts); + while (m.inc() && m_stats.m_restarts++ < m_config.m_max_restarts); return res; } @@ -162,6 +173,8 @@ namespace bv { } bool sls::eval_is_correct(app* e) { + if (!m_eval.can_eval1(e)) + return false; if (m.is_bool(e)) return m_eval.bval0(e) == m_eval.bval1(e); if (bv.is_bv(e)) @@ -208,4 +221,9 @@ namespace bv { terms.reset(); return out; } + + void sls::updt_params(params_ref const& _p) { + sls_params p(_p); + m_config.m_max_restarts = p.max_restarts(); + } } diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index c91838a4c36..753cf58ffc7 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -36,7 +36,7 @@ namespace bv { struct config { unsigned m_max_restarts = 1000; - unsigned m_max_repairs = 100000; + unsigned m_max_repairs = 1000; }; ast_manager& m; @@ -59,6 +59,7 @@ namespace bv { lbool search(); void reinit_eval(); + void trace(); public: sls(ast_manager& m); @@ -85,7 +86,7 @@ namespace bv { */ lbool operator()(); - void updt_params(params_ref const& p) {} + void updt_params(params_ref const& p); void collect_statistics(statistics & st) const { m_stats.collect_statistics(st); } void reset_statistics() { m_stats.reset(); } diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 3f5d0e27075..7bd8316b5ad 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -171,15 +171,41 @@ namespace bv { auto const& vb = wval0(b); return va.eq(vb); } - UNREACHABLE(); - break; + return m.are_equal(a, b); } default: UNREACHABLE(); + break; } UNREACHABLE(); return false; } + + bool sls_eval::can_eval1(app* e) const { + expr* x, * y, * z; + if (m.is_eq(e, x, y)) + return m.is_bool(x) || bv.is_bv(x); + if (m.is_ite(e, x, y, z)) + return m.is_bool(y) || bv.is_bv(y); + if (e->get_family_id() == bv.get_fid()) { + switch (e->get_decl_kind()) { + case OP_BNEG_OVFL: + case OP_BSADD_OVFL: + case OP_BSDIV_OVFL: + case OP_BSMUL_NO_OVFL: + case OP_BSMUL_NO_UDFL: + case OP_BSMUL_OVFL: + return false; + default: + return true; + } + } + if (e->get_family_id() == basic_family_id) + return true; + if (is_uninterp_const(e)) + return m.is_bool(e) || bv.is_bv(e); + return false; + } bool sls_eval::bval1_bv(app* e) const { SASSERT(m.is_bool(e)); @@ -1182,8 +1208,8 @@ namespace bv { if (i == 0) { if (e.is_zero() && a.is_ones(a.fixed) && a.is_ones()) return false; - if (b.is_zero()) - return true; + if (b.is_zero()) + return false; if (!e.is_ones()) { for (unsigned i = 0; i < a.nw; ++i) m_tmp[i] = ~a.fixed[i] | a.bits[i]; @@ -1215,11 +1241,19 @@ namespace bv { a.set_repair(true, m_tmp3); } else { + if (e.is_one() && a.is_zero()) { + for (unsigned i = 0; i < a.nw; ++i) + m_tmp[i] = random_bits(); + a.clear_overflow_bits(m_tmp); + b.set_repair(true, m_tmp); + return true; + } if (e.is_one()) { b.set(m_tmp, a.bits); b.set_repair(true, m_tmp); return true; } + // e * b + r = a // b = (a - r) udiv e // random version of r: diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 6c7a2053d5d..d2c20e6add7 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -134,6 +134,7 @@ namespace bv { * Retrieve evaluation based on immediate children. */ bool bval1(app* e) const; + bool can_eval1(app* e) const; svector& wval1(app* e) const; diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index 0d51906bff2..f7cd4c23a64 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -11,6 +11,7 @@ Module Name: --*/ +#include "ast/ast_pp.h" #include "ast/sls/bv_sls_fixed.h" #include "ast/sls/bv_sls_eval.h" @@ -137,12 +138,12 @@ namespace bv { v.add_range(-b, a - b); } else if (!y) { - if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 1) + if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 0) return; auto& v = wval0(x); if (!sign) v.add_range(-a, b - a + 1); - else + else v.add_range(b - a + 1, -a); } else if (x == y) { diff --git a/src/ast/sls/sls_stats.h b/src/ast/sls/sls_stats.h index 8599a1f6489..9468e9c8d37 100644 --- a/src/ast/sls/sls_stats.h +++ b/src/ast/sls/sls_stats.h @@ -35,13 +35,16 @@ namespace bv { st.update("sls restarts", m_restarts); st.update("sls full evals", m_full_evals); st.update("sls incr evals", m_incr_evals); - st.update("sls incr evals/sec", m_incr_evals / seconds); + if (seconds > 0 && m_incr_evals > 0) + st.update("sls incr evals/sec", m_incr_evals / seconds); + if (seconds > 0 && m_moves > 0) + st.update("sls moves/sec", m_moves / seconds); st.update("sls FLIP moves", m_flips); st.update("sls INC moves", m_incs); st.update("sls DEC moves", m_decs); st.update("sls INV moves", m_invs); st.update("sls moves", m_moves); - st.update("sls moves/sec", m_moves / seconds); + } }; diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 3bafca7daa0..1954b177774 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -296,6 +296,7 @@ namespace bv { h = mod(h, rational::power_of_two(bw)); if (h == l) return; + if (eq(lo, hi)) { set_value(lo, l); set_value(hi, h); diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index ca68cf5a7ed..bb8100f7546 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -192,19 +192,26 @@ namespace bv { std::ostream& display(std::ostream& out) const { out << std::hex; - for (unsigned i = 0; i < nw; ++i) - out << bits[i]; + auto print_bits = [&](svector const& v) { + bool nz = false; + for (unsigned i = nw; i-- > 0;) + if (nz) + out << std::setw(8) << std::setfill('0') << v[i]; + else if (v[i] != 0) + out << v[i], nz = true; + if (!nz) + out << "0"; + }; + + print_bits(bits); out << " "; - for (unsigned i = 0; i < nw; ++i) - out << fixed[i]; + print_bits(fixed); if (!eq(lo, hi)) { out << " ["; - for (unsigned i = 0; i < nw; ++i) - out << lo[i]; + print_bits(lo); out << ", "; - for (unsigned i = 0; i < nw; ++i) - out << hi[i]; + print_bits(hi); out << "["; } out << std::dec; diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index ca3f46bc045..198204d90b0 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -126,14 +126,15 @@ class sls_tactic : public tactic { class bv_sls_tactic : public tactic { ast_manager& m; - params_ref m_params; - bv::sls* m_engine; + params_ref m_params; + bv::sls* m_sls; + statistics m_st; public: bv_sls_tactic(ast_manager& _m, params_ref const& p) : m(_m), m_params(p) { - m_engine = alloc(bv::sls, m); + m_sls = alloc(bv::sls, m); } tactic* translate(ast_manager& m) override { @@ -141,14 +142,14 @@ class bv_sls_tactic : public tactic { } ~bv_sls_tactic() override { - dealloc(m_engine); + dealloc(m_sls); } char const* name() const override { return "bv-sls"; } void updt_params(params_ref const& p) override { m_params.append(p); - m_engine->updt_params(m_params); + m_sls->updt_params(m_params); } void collect_param_descrs(param_descrs& r) override { @@ -162,23 +163,24 @@ class bv_sls_tactic : public tactic { } for (unsigned i = 0; i < g->size(); i++) - m_engine->assert_expr(g->form(i)); + m_sls->assert_expr(g->form(i)); - m_engine->init(); + m_sls->init(); std::function false_eval = [&](expr* e, unsigned idx) { return false; }; - m_engine->init_eval(false_eval); + m_sls->init_eval(false_eval); - lbool res = m_engine->operator()(); - auto const& stats = m_engine->get_stats(); + lbool res = m_sls->operator()(); + auto const& stats = m_sls->get_stats(); report_tactic_progress("Number of flips:", stats.m_moves); - IF_VERBOSE(0, verbose_stream() << res << "\n"); - IF_VERBOSE(0, m_engine->display(verbose_stream())); - if (res == l_true) { - + IF_VERBOSE(20, verbose_stream() << res << "\n"); + IF_VERBOSE(20, m_sls->display(verbose_stream())); + m_st.reset(); + m_sls->collect_statistics(m_st); + if (res == l_true) { if (g->models_enabled()) { - model_ref mdl = m_engine->get_model(); + model_ref mdl = m_sls->get_model(); mc = model2model_converter(mdl.get()); TRACE("sls_model", mc->display(tout);); } @@ -204,17 +206,19 @@ class bv_sls_tactic : public tactic { } void cleanup() override { + auto* d = alloc(bv::sls, m); - std::swap(d, m_engine); + std::swap(d, m_sls); dealloc(d); } void collect_statistics(statistics& st) const override { - m_engine->collect_statistics(st); + st.copy(m_st); } void reset_statistics() override { - m_engine->reset_statistics(); + m_sls->reset_statistics(); + m_st.reset(); } };