From 8de0005ab3f3108a0c96416a91dde80546878bb7 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Fri, 27 Dec 2024 17:40:34 +0100 Subject: [PATCH 01/12] Bugfix seq-eq sls (#7495) * Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping * Removed debug code * One check was missing --- src/ast/sls/sls_seq_plugin.cpp | 44 ++++++++++++++++++++++++---------- src/ast/sls/sls_seq_plugin.h | 2 +- 2 files changed, 32 insertions(+), 14 deletions(-) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 9ed98d467..b8835650f 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -114,10 +114,10 @@ namespace sls { auto e = ctx.atom(lit.var()); if (!is_seq_predicate(e)) return; - auto a = to_app(e); if (bval1(e) != lit.sign()) return; - ctx.new_value_eh(e); + // Literal not currently satisfied => report back to context + ctx.new_value_eh(e); } expr_ref seq_plugin::get_value(expr* e) { @@ -265,6 +265,7 @@ namespace sls { return e.rhs; } + // Gets the currently assumed value for e zstring& seq_plugin::strval0(expr* e) { SASSERT(seq.is_string(e->get_sort())); return get_eval(e).val0.svalue; @@ -343,8 +344,8 @@ namespace sls { return false; } + // Evaluate e using the assumed values of its arguments and cache + return the result zstring const& seq_plugin::strval1(expr* e) { - SASSERT(is_app(e)); SASSERT(seq.is_string(e->get_sort())); auto & ev = get_eval(e); if (ev.is_value) @@ -608,6 +609,7 @@ namespace sls { VERIFY(m.is_eq(e, x, y)); IF_VERBOSE(3, verbose_stream() << is_true << ": " << mk_bounded_pp(e, m, 3) << "\n"); if (ctx.is_true(e)) { + // equality if (false && ctx.rand(2) != 0 && repair_down_str_eq_edit_distance_incremental(e)) return true; if (ctx.rand(2) != 0 && repair_down_str_eq_edit_distance(e)) @@ -620,6 +622,7 @@ namespace sls { m_str_updates.push_back({ y, strval1(x), 1 }); } else { + // disequality if (!is_value(x) && !m_chars.empty()) { zstring ch(m_chars[ctx.rand(m_chars.size())]); m_str_updates.push_back({ x, strval1(y) + ch, 1 }); @@ -672,15 +675,28 @@ namespace sls { m_str_updates.push_back({ x, a + zstring(ch), 1 }); for (auto ch : chars) m_str_updates.push_back({ x, zstring(ch) + a, 1 }); - if (a.length() > 0) { + if (!a.empty()) { zstring b = a.extract(0, a.length() - 1); + unsigned remC = a[a.length() - 1]; m_str_updates.push_back({ x, b, 1 }); // truncate a - for (auto ch : chars) + for (auto ch : chars) { + if (ch == remC) + // We would end up with the initial string + // => this "no-op" could be spuriously considered a solution (also it does not help) + continue; m_str_updates.push_back({ x, b + zstring(ch), 1 }); // replace last character in a by ch - b = a.extract(1, a.length() - 1); - m_str_updates.push_back({ x, b, 1 }); // truncate a - for (auto ch : chars) - m_str_updates.push_back({ x, zstring(ch) + b, 1 }); // replace first character in a by ch + } + if (a.length() > 1) { + // Otw. we just get the same set of candidates another time + b = a.extract(1, a.length() - 1); + remC = a[0]; + m_str_updates.push_back({ x, b, 1 }); // truncate a + for (auto ch : chars) { + if (ch == remC) + continue; + m_str_updates.push_back({ x, zstring(ch) + b, 1 }); // replace first character in a by ch + } + } } } unsigned first_diff = UINT_MAX; @@ -699,7 +715,8 @@ namespace sls { if (is_value(x)) break; auto new_val = val_x.extract(0, first_diff) + zstring(val_other[first_diff]) + val_x.extract(first_diff + 1, val_x.length()); - m_str_updates.push_back({ x, new_val, 1 }); + if (val_x != new_val) + m_str_updates.push_back({ x, new_val, 1 }); break; } index -= len_x; @@ -1468,7 +1485,7 @@ namespace sls { uint_set chars; for (auto ch : value0) - chars.insert(ch); + chars.insert(ch); add_edit_updates(es, value, value0, chars); @@ -1606,8 +1623,9 @@ namespace sls { } bool seq_plugin::update(expr* e, zstring const& value) { - if (value == strval0(e)) - return true; + SASSERT(value != strval0(e)); + // if (value == strval0(e)) + // return true; if (is_value(e)) return false; if (get_eval(e).min_length > value.length() || get_eval(e).max_length < value.length()) diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h index cabfa6d9a..bd34b3449 100644 --- a/src/ast/sls/sls_seq_plugin.h +++ b/src/ast/sls/sls_seq_plugin.h @@ -47,7 +47,7 @@ namespace sls { seq_rewriter rw; th_rewriter thrw; scoped_ptr_vector m_values; - indexed_uint_set m_chars; + indexed_uint_set m_chars; // set of characters in the problem bool m_initialized = false; struct str_update { From b0eee161099b4baff1048774f099db74bbe49025 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2024 12:26:11 -0800 Subject: [PATCH 02/12] fix double override bug in bv_lookahead, integrate with bv_eval --- src/ast/sls/sls_arith_base.cpp | 4 +- src/ast/sls/sls_bv_eval.cpp | 6 +- src/ast/sls/sls_bv_eval.h | 1 + src/ast/sls/sls_bv_lookahead.cpp | 127 +++++++++++++++++++++---------- src/ast/sls/sls_bv_lookahead.h | 34 +++++++-- src/ast/sls/sls_bv_plugin.cpp | 4 + src/ast/sls/sls_bv_plugin.h | 2 +- src/ast/sls/sls_bv_valuation.cpp | 2 +- src/ast/sls/sls_context.cpp | 4 +- 9 files changed, 128 insertions(+), 56 deletions(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index a31304831..7515c58de 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -1656,9 +1656,9 @@ namespace sls { } if (result < 0) - return 0.1; + return 0.0000001; else if (result == 0) - return 0.2; + return 0.000002; for (int i = m_prob_break.size(); i <= breaks; ++i) m_prob_break.push_back(std::pow(m_config.cb, -i)); return m_prob_break[breaks]; diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index 997b3c4b3..d2332deee 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/src/ast/sls/sls_bv_eval.cpp @@ -679,7 +679,7 @@ namespace sls { expr* arg = e->get_arg(i); if (m.is_value(arg)) return false; - if (m.is_bool(e) && false && m_rand(10) == 0 && m_lookahead.try_repair_down(e)) + if (false && m.is_bool(e) && ctx.rand(10) == 0 && m_lookahead.try_repair_down(e)) return true; if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) { commit_eval(e, to_app(arg)); @@ -2024,6 +2024,10 @@ namespace sls { return expr_ref(m); } + void bv_eval::collect_statistics(statistics& st) const { + m_lookahead.collect_statistics(st); + } + std::ostream& bv_eval::display(std::ostream& out) const { auto& terms = ctx.subterms(); for (expr* e : terms) { diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h index 6dc2d35e4..2314c2895 100644 --- a/src/ast/sls/sls_bv_eval.h +++ b/src/ast/sls/sls_bv_eval.h @@ -190,6 +190,7 @@ namespace sls { */ bool repair_up(expr* e); + void collect_statistics(statistics& st) const; std::ostream& display(std::ostream& out) const; diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 6341f1e0e..2ad3cc535 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -36,25 +36,45 @@ namespace sls { auto const& uninterp = m_ev.terms.uninterp_occurs(e); if (uninterp.empty()) return false; + + if (false && ctx.rand(10) == 0 && apply_random_update(uninterp)) + return true; + reset_updates(); - IF_VERBOSE(4, - verbose_stream() << mk_bounded_pp(e, m) << "\n"; - for (auto e : uninterp) - verbose_stream() << mk_bounded_pp(e, m) << " "; - verbose_stream() << "\n"); + TRACE("sls", tout << mk_bounded_pp(e, m) << " contains "; + for (auto e : uninterp) + tout << mk_bounded_pp(e, m) << " "; + tout << "\n";); - for (auto e : uninterp) + for (auto e : uninterp) add_updates(e); -#if 0 + m_stats.m_num_lookahead += 1; + m_stats.m_num_updates += m_num_updates; + + TRACE("sls", display_updates(tout)); + + if (apply_update()) + return true; + + return apply_random_update(uninterp); + } + + void bv_lookahead::display_updates(std::ostream& out) { for (unsigned i = 0; i < m_num_updates; ++i) { auto const& [e, score, new_value] = m_updates[i]; - verbose_stream() << mk_bounded_pp(e, m) << " " << new_value << " score: " << score << "\n"; + out << mk_bounded_pp(e, m) << " " << new_value << " score: " << score << "\n"; } -#endif - - return apply_update(); + } + + bool bv_lookahead::apply_random_update(ptr_vector const& vars) { + expr* e = vars[ctx.rand(vars.size())]; + auto& v = wval(e); + m_v_updated.set_bw(v.bw); + v.get_variant(m_v_updated, m_ev.m_rand); + apply_update(e, m_v_updated); + return true; } double bv_lookahead::lookahead(expr* e, bvect const& new_value) { @@ -63,22 +83,23 @@ namespace sls { SASSERT(m_restore.empty()); bool has_tabu = false; - double break_count = 0, make_count = 0; + int result = 0; + int breaks = 0; wval(e).eval = new_value; if (!insert_update(e)) { restore_lookahead(); + m_in_update_stack.reset(); return -1000000; } insert_update_stack(e); unsigned max_depth = get_depth(e); for (unsigned depth = max_depth; depth <= max_depth; ++depth) { for (unsigned i = 0; !has_tabu && i < m_update_stack[depth].size(); ++i) { - auto e = m_update_stack[depth][i]; - if (bv.is_bv(e)) { - auto& v = m_ev.eval(to_app(e)); - if (insert_update(e)) { - for (auto p : ctx.parents(e)) { + auto a = m_update_stack[depth][i]; + if (bv.is_bv(a)) { + if (a == e || (m_ev.eval(a), insert_update(a))) { // do not insert e twice + for (auto p : ctx.parents(a)) { insert_update_stack(p); max_depth = std::max(max_depth, get_depth(p)); } @@ -86,32 +107,43 @@ namespace sls { else has_tabu = true; } - else if (m.is_bool(e) && m_ev.can_eval1(to_app(e))) { - if (!ctx.is_relevant(e)) + else if (m.is_bool(a) && m_ev.can_eval1(a)) { + if (!ctx.is_relevant(a)) continue; - bool is_true = ctx.is_true(e); - bool is_true_new = m_ev.bval1(to_app(e)); - bool is_true_old = m_ev.bval1_tmp(to_app(e)); + bool is_true = ctx.is_true(a); + bool is_true_new = m_ev.bval1(a); + bool is_true_old = m_ev.bval1_tmp(a); + TRACE("sls_verbose", tout << mk_bounded_pp(a, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n"); if (is_true_new == is_true_old) continue; if (is_true == is_true_new) - ++make_count; - if (is_true == is_true_old) - ++break_count; + ++result; + if (is_true == is_true_old) { + --result; + ++breaks; + } } else { - IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(e, m) << "\n"); + IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(a, m) << "\n"); has_tabu = true; } } m_update_stack[depth].reset(); } + m_in_update_stack.reset(); restore_lookahead(); - // verbose_stream() << has_tabu << " " << new_value << " " << make_count << " " << break_count << "\n"; + + TRACE("sls_verbose", tout << mk_bounded_pp(e, m) << " " << new_value << " " << result << " " << breaks << "\n"); if (has_tabu) return -10000; - return make_count - break_count; + if (result < 0) + return 0.0000001; + else if (result == 0) + return 0.000002; + for (int i = m_prob_break.size(); i <= breaks; ++i) + m_prob_break.push_back(std::pow(m_config.cb, -i)); + return m_prob_break[breaks]; } void bv_lookahead::try_set(expr* e, bvect const& new_value) { @@ -125,7 +157,6 @@ namespace sls { void bv_lookahead::add_updates(expr* e) { SASSERT(bv.is_bv(e)); auto& v = wval(e); - double d = 0; while (m_v_saved.size() < v.bits().size()) { m_v_saved.push_back(0); m_v_updated.push_back(0); @@ -161,9 +192,9 @@ namespace sls { v.sub1(m_v_updated); try_set(e, m_v_updated); - // random - v.get_variant(m_v_updated, m_ev.m_rand); - try_set(e, m_v_updated); + // random, deffered to failure path + // v.get_variant(m_v_updated, m_ev.m_rand); + // try_set(e, m_v_updated); } bool bv_lookahead::apply_update() { @@ -174,12 +205,13 @@ namespace sls { for (unsigned i = 0; i < m_num_updates; ++i) { auto const& [e, score, new_value] = m_updates[i]; pos -= score; - if (pos <= 0) { - //verbose_stream() << "apply " << mk_bounded_pp(e, m) << " new value " << new_value << " " << score << "\n"; + if (pos <= 0.00000000001) { + TRACE("sls", tout << "apply " << mk_bounded_pp(e, m) << " new value " << new_value << " " << score << "\n"); apply_update(e, new_value); return true; } } + TRACE("sls", tout << "no update " << m_num_updates << "\n"); return false; } @@ -195,14 +227,18 @@ namespace sls { for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) { auto e = m_update_stack[depth][i]; if (bv.is_bv(e)) { - m_ev.eval(to_app(e)); // updates wval(e).eval - VERIFY(wval(e).commit_eval()); + m_ev.eval(e); // updates wval(e).eval + if (!wval(e).commit_eval()) { + TRACE("sls", tout << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); + // bv_plugin::is_sat picks up discrepancies + continue; + } for (auto p : ctx.parents(e)) { insert_update_stack(p); max_depth = std::max(max_depth, get_depth(p)); } } - else if (m.is_bool(e) && m_ev.can_eval1(to_app(e))) { + else if (m.is_bool(e) && m_ev.can_eval1(e)) { VERIFY(m_ev.repair_up(e)); } else { @@ -215,9 +251,10 @@ namespace sls { } bool bv_lookahead::insert_update(expr* e) { + auto& v = wval(e); m_restore.push_back(e); m_on_restore.mark(e); - auto& v = wval(e); + TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << " " << v << "\n"); v.save_value(); return v.commit_eval(); } @@ -225,18 +262,19 @@ namespace sls { void bv_lookahead::insert_update_stack(expr* e) { unsigned depth = get_depth(e); m_update_stack.reserve(depth + 1); - if (!m_in_update_stack.is_marked(e)) { + if (!m_in_update_stack.is_marked(e) && is_app(e)) { m_in_update_stack.mark(e); - m_update_stack[depth].push_back(e); + m_update_stack[depth].push_back(to_app(e)); } } void bv_lookahead::restore_lookahead() { - for (auto e : m_restore) + for (auto e : m_restore) { wval(e).restore_value(); + TRACE("sls_verbose", tout << "restore value " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); + } m_restore.reset(); m_on_restore.reset(); - m_in_update_stack.reset(); } sls::bv_valuation& bv_lookahead::wval(expr* e) const { @@ -246,4 +284,9 @@ namespace sls { bool bv_lookahead::on_restore(expr* e) const { return m_on_restore.is_marked(e); } + + void bv_lookahead::collect_statistics(statistics& st) const { + st.update("sls-bv-lookahead", m_stats.m_num_lookahead); + st.update("sls-bv-updates", m_stats.m_num_updates); + } } \ No newline at end of file diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h index 15b810ec0..c60ad1362 100644 --- a/src/ast/sls/sls_bv_lookahead.h +++ b/src/ast/sls/sls_bv_lookahead.h @@ -24,23 +24,38 @@ namespace sls { class bv_eval; class bv_lookahead { + struct config { + double cb = 2.85; + }; + + struct update { + expr* e; + double score; + bvect value; + }; + + struct stats { + unsigned m_num_lookahead = 0; + unsigned m_num_updates = 0; + }; + + bv_util bv; bv_eval& m_ev; context& ctx; ast_manager& m; + config m_config; + stats m_stats; bvect m_v_saved, m_v_updated; - + svector m_prob_break; ptr_vector m_restore; - vector> m_update_stack; + vector> m_update_stack; expr_mark m_on_restore, m_in_update_stack; - struct update { - expr* e; - double score; - bvect value; - }; vector m_updates; unsigned m_num_updates = 0; + void reset_updates() { m_num_updates = 0; } + void add_update(double score, expr* e, bvect const& value) { if (m_num_updates == m_updates.size()) m_updates.push_back({ e, score, value }); @@ -65,13 +80,18 @@ namespace sls { void add_updates(expr* e); void apply_update(expr* e, bvect const& new_value); bool apply_update(); + bool apply_random_update(ptr_vector const& vars); + void display_updates(std::ostream& out); public: bv_lookahead(bv_eval& ev); + bool on_restore(expr* e) const; bool try_repair_down(app* e); + void collect_statistics(statistics& st) const; + }; } \ No newline at end of file diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp index 4c2877235..78d367770 100644 --- a/src/ast/sls/sls_bv_plugin.cpp +++ b/src/ast/sls/sls_bv_plugin.cpp @@ -167,6 +167,10 @@ namespace sls { ctx.flip(lit.var()); } + void bv_plugin::collect_statistics(statistics& st) const { + m_eval.collect_statistics(st); + } + std::ostream& bv_plugin::trace_repair(bool down, expr* e) { verbose_stream() << (down ? "d #" : "u #") << e->get_id() << ": " diff --git a/src/ast/sls/sls_bv_plugin.h b/src/ast/sls/sls_bv_plugin.h index ea750163e..7bcc4c329 100644 --- a/src/ast/sls/sls_bv_plugin.h +++ b/src/ast/sls/sls_bv_plugin.h @@ -53,7 +53,7 @@ namespace sls { void on_restart() override {} std::ostream& display(std::ostream& out) const override; bool set_value(expr* e, expr* v) override; - void collect_statistics(statistics& st) const override {} + void collect_statistics(statistics& st) const override; void reset_statistics() override {} }; diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp index 29fc6b517..d23471a2c 100644 --- a/src/ast/sls/sls_bv_valuation.cpp +++ b/src/ast/sls/sls_bv_valuation.cpp @@ -33,7 +33,7 @@ namespace sls { bool operator==(bvect const& a, bvect const& b) { SASSERT(a.nw > 0); - return 0 == mpn_manager().compare(a.data(), a.nw, b.data(), a.nw); + return 0 == memcmp(a.data(), b.data(), a.nw * sizeof(digit_t)); } bool operator<(bvect const& a, bvect const& b) { diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index b177bfb0c..cab031d52 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -565,8 +565,8 @@ namespace sls { SASSERT(m.is_true(get_value(e)) == is_true(v)); } } - ); - + ); + m_repair_down.reserve(e->get_id() + 1); m_repair_up.reserve(e->get_id() + 1); if (!term(e->get_id())) From c82518ca36751aff2fed1838f85b3dce2c0fbcdd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2024 12:29:44 -0800 Subject: [PATCH 03/12] include cmath to define std::pow Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_lookahead.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 2ad3cc535..dde03265d 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -19,6 +19,7 @@ Author: #include "ast/sls/sls_bv_eval.h" #include "ast/sls/sls_bv_terms.h" #include "ast/ast_pp.h" +#include namespace sls { From 1f55ec5cefca2e42e8fe8eee871710e9f1551d9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2024 13:01:47 -0800 Subject: [PATCH 04/12] fix random update to a legal one Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_lookahead.cpp | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index dde03265d..37ca06b26 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -70,11 +70,17 @@ namespace sls { } bool bv_lookahead::apply_random_update(ptr_vector const& vars) { - expr* e = vars[ctx.rand(vars.size())]; - auto& v = wval(e); - m_v_updated.set_bw(v.bw); - v.get_variant(m_v_updated, m_ev.m_rand); - apply_update(e, m_v_updated); + while (true) { + expr* e = vars[ctx.rand(vars.size())]; + auto& v = wval(e); + m_v_updated.set_bw(v.bw); + v.get_variant(m_v_updated, m_ev.m_rand); + v.eval = m_v_updated; + if (!v.commit_eval()) + continue; + apply_update(e, m_v_updated); + break; + } return true; } @@ -221,6 +227,7 @@ namespace sls { SASSERT(is_uninterp(e)); SASSERT(m_restore.empty()); wval(e).eval = new_value; + VERIFY(wval(e).commit_eval()); insert_update_stack(e); unsigned max_depth = get_depth(e); From 0b9ed925d65cdcd202d99454aa6b74191fc82e0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2024 13:34:48 -0800 Subject: [PATCH 05/12] try dual phase lookahead Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_eval.cpp | 11 ++++++++++- src/ast/sls/sls_bv_eval.h | 4 ++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index d2332deee..5522076a0 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/src/ast/sls/sls_bv_eval.cpp @@ -674,12 +674,21 @@ namespace sls { return false; } } + + bool bv_eval::is_lookahead_phase() { + ++m_lookahead_steps; + if (m_lookahead_steps < m_lookahead_phase_size) + return true; + if (m_lookahead_steps > 2 * m_lookahead_phase_size) + m_lookahead_steps = 0; + return false; + } bool bv_eval::repair_down(app* e, unsigned i) { expr* arg = e->get_arg(i); if (m.is_value(arg)) return false; - if (false && m.is_bool(e) && ctx.rand(10) == 0 && m_lookahead.try_repair_down(e)) + if (m.is_bool(e) && is_lookahead_phase() && m_lookahead.try_repair_down(e)) return true; if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) { commit_eval(e, to_app(arg)); diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h index 2314c2895..b6ac73e63 100644 --- a/src/ast/sls/sls_bv_eval.h +++ b/src/ast/sls/sls_bv_eval.h @@ -52,6 +52,8 @@ namespace sls { random_gen m_rand; config m_config; bool_vector m_fixed; + unsigned m_lookahead_steps = 0; + unsigned m_lookahead_phase_size = 100; scoped_ptr_vector m_values; // expr-id -> bv valuation @@ -147,6 +149,8 @@ namespace sls { void commit_eval(expr* p, app* e); + bool is_lookahead_phase(); + public: bv_eval(sls::bv_terms& terms, sls::context& ctx); From bd8c870bbee49da9756c1408b3f162897ad74ffa Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sat, 28 Dec 2024 09:42:54 +0000 Subject: [PATCH 06/12] api: avoid some string copies when using mk_external_string --- scripts/update_api.py | 2 +- src/api/api_context.cpp | 15 ++------------- src/api/api_context.h | 4 +--- src/api/api_datalog.cpp | 2 +- src/api/api_log.cpp | 2 +- src/api/api_numeral.cpp | 10 +++++----- src/api/api_opt.cpp | 2 +- src/api/api_params.cpp | 2 +- src/api/api_parsers.cpp | 8 +++----- src/api/api_rcf.cpp | 4 ++-- src/api/api_tactic.cpp | 14 +++++++------- 11 files changed, 25 insertions(+), 40 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 79f144142..cbea973b3 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1799,7 +1799,7 @@ def write_log_h_preamble(log_h): log_h.write('extern atomic g_z3_log_enabled;\n') log_h.write('void ctx_enable_logging();\n') log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n') - log_h.write('void SetR(void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n') + log_h.write('void SetR(const void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n') log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) { SetR(tmp_ret); } return tmp_ret; } while (0)\n') diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 6f7a424ea..acc4d7016 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -209,21 +209,10 @@ namespace api { invoke_error_handler(err); } } - - char * context::mk_external_string(char const * str) { - m_string_buffer = str?str:""; - return const_cast(m_string_buffer.c_str()); - } - - char * context::mk_external_string(char const * str, unsigned n) { - m_string_buffer.clear(); - m_string_buffer.append(str, n); - return const_cast(m_string_buffer.c_str()); - } - char * context::mk_external_string(std::string && str) { + const char * context::mk_external_string(std::string && str) { m_string_buffer = std::move(str); - return const_cast(m_string_buffer.c_str()); + return m_string_buffer.c_str(); } expr * context::mk_numeral_core(rational const & n, sort * s) { diff --git a/src/api/api_context.h b/src/api/api_context.h index 8b049ce16..2838bcb05 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -199,9 +199,7 @@ namespace api { // Store a copy of str in m_string_buffer, and return a reference to it. // This method is used to communicate local/internal strings with the "external world" - char * mk_external_string(char const * str, unsigned n); - char * mk_external_string(char const * str); - char * mk_external_string(std::string && str); + const char * mk_external_string(std::string && str); sbuffer m_char_buffer; diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 8f436bf8a..3d437e983 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -559,7 +559,7 @@ extern "C" { param_descrs descrs; to_fixedpoint_ref(d)->collect_param_descrs(descrs); descrs.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index ed5f68e8a..e84ece780 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -34,7 +34,7 @@ static mutex g_log_mux; #endif // functions called from api_log_macros.* -void SetR(void * obj) { +void SetR(const void * obj) { *g_z3_log << "= " << obj << '\n'; } diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index b90a84bb7..4e99e05f0 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -217,20 +217,20 @@ extern "C" { if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) { switch (rm) { case MPF_ROUND_NEAREST_TEVEN: - return mk_c(c)->mk_external_string("roundNearestTiesToEven"); + return "roundNearestTiesToEven"; break; case MPF_ROUND_NEAREST_TAWAY: - return mk_c(c)->mk_external_string("roundNearestTiesToAway"); + return "roundNearestTiesToAway"; break; case MPF_ROUND_TOWARD_POSITIVE: - return mk_c(c)->mk_external_string("roundTowardPositive"); + return "roundTowardPositive"; break; case MPF_ROUND_TOWARD_NEGATIVE: - return mk_c(c)->mk_external_string("roundTowardNegative"); + return "roundTowardNegative"; break; case MPF_ROUND_TOWARD_ZERO: default: - return mk_c(c)->mk_external_string("roundTowardZero"); + return "roundTowardZero"; break; } } diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 556b1345b..ef215941e 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -313,7 +313,7 @@ extern "C" { param_descrs descrs; to_optimize_ptr(d)->collect_param_descrs(descrs); descrs.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp index 2d0770903..aa44e56ee 100644 --- a/src/api/api_params.cpp +++ b/src/api/api_params.cpp @@ -191,7 +191,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } - return mk_c(c)->mk_external_string(result); + return result; Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index ae245fbdc..8f6c76958 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -235,9 +235,9 @@ extern "C" { Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) { std::stringstream ous; - Z3_TRY; RESET_ERROR_CODE(); LOG_Z3_eval_smtlib2_string(c, str); + Z3_TRY; if (!mk_c(c)->cmd()) { auto* ctx = alloc(cmd_context, false, &(mk_c(c)->m())); mk_c(c)->cmd() = ctx; @@ -257,15 +257,13 @@ extern "C" { // See api::context::m_parser for a motivation about the reuse of the parser if (!parse_smt2_commands_with_parser(mk_c(c)->m_parser, *ctx.get(), is)) { SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str()); - RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); } } catch (z3_exception& e) { if (ous.str().empty()) ous << e.what(); SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str()); - RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); } - RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); - Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str())); + Z3_CATCH_CORE(); + RETURN_Z3(mk_c(c)->mk_external_string(std::move(ous).str())); } } diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index ccc79bc46..684e8c617 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -274,7 +274,7 @@ extern "C" { reset_rcf_cancel(c); std::ostringstream buffer; rcfm(c).display(buffer, to_rcnumeral(a), compact, html); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } @@ -285,7 +285,7 @@ extern "C" { reset_rcf_cancel(c); std::ostringstream buffer; rcfm(c).display_decimal(buffer, to_rcnumeral(a), prec); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 351b3d1b9..af5696132 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -339,7 +339,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } - return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str().c_str()); + return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str()); Z3_CATCH_RETURN(""); } @@ -359,7 +359,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } - return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str().c_str()); + return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str()); Z3_CATCH_RETURN(""); } @@ -371,7 +371,7 @@ extern "C" { param_descrs descrs; to_tactic_ref(t)->collect_param_descrs(descrs); descrs.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } @@ -499,8 +499,8 @@ extern "C" { for (unsigned i = 0; i < sz; i++) { to_apply_result(r)->m_subgoals[i]->display(buffer); } - buffer << ")"; - return mk_c(c)->mk_external_string(buffer.str()); + buffer << ')'; + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } @@ -578,7 +578,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } - return mk_c(c)->mk_external_string(mk_c(c)->get_simplifier(idx)->get_name().str().c_str()); + return mk_c(c)->mk_external_string(mk_c(c)->get_simplifier(idx)->get_name().str()); Z3_CATCH_RETURN(""); } @@ -634,7 +634,7 @@ extern "C" { scoped_ptr simp = (*to_simplifier_ref(t))(m, p, st); simp->collect_param_descrs(descrs); descrs.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } From 3aacc6222972fb68436beba307fdec431d95c239 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sat, 28 Dec 2024 09:52:36 +0000 Subject: [PATCH 07/12] api: hint the compiler that logging enabled is unlikely --- scripts/update_api.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index cbea973b3..153052deb 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1798,9 +1798,9 @@ def write_log_h_preamble(log_h): log_h.write('#include "util/mutex.h"\n') log_h.write('extern atomic g_z3_log_enabled;\n') log_h.write('void ctx_enable_logging();\n') - log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n') + log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) [[unlikely]] g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n') log_h.write('void SetR(const void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n') - log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) { SetR(tmp_ret); } return tmp_ret; } while (0)\n') + log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) [[unlikely]] { SetR(tmp_ret); } return tmp_ret; } while (0)\n') def write_log_c_preamble(log_c): From a5bc5ed813543872dd5fd53d80ad766d071e5db9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2024 13:55:22 -0800 Subject: [PATCH 08/12] try uneven lookahead skew Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_eval.cpp | 2 +- src/ast/sls/sls_bv_eval.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index 5522076a0..c4f2dbb64 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/src/ast/sls/sls_bv_eval.cpp @@ -679,7 +679,7 @@ namespace sls { ++m_lookahead_steps; if (m_lookahead_steps < m_lookahead_phase_size) return true; - if (m_lookahead_steps > 2 * m_lookahead_phase_size) + if (m_lookahead_steps > 10 * m_lookahead_phase_size) m_lookahead_steps = 0; return false; } diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h index b6ac73e63..3f5f87024 100644 --- a/src/ast/sls/sls_bv_eval.h +++ b/src/ast/sls/sls_bv_eval.h @@ -53,7 +53,7 @@ namespace sls { config m_config; bool_vector m_fixed; unsigned m_lookahead_steps = 0; - unsigned m_lookahead_phase_size = 100; + unsigned m_lookahead_phase_size = 10; scoped_ptr_vector m_values; // expr-id -> bv valuation From f41134d1b6f7462df23eb572addcc4cd46e2bd7b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 Dec 2024 17:40:15 -0800 Subject: [PATCH 09/12] h - avoid more platform specific behavior when using m_mk_extract, - rename mk_eq in bool_rewriter to mk_eq_plain to distinguish it from mk_eq_rw - rework bv_lookahead to be more closely based on sls_engine, which has much better heuristic behavior than attempt 1. --- src/ast/rewriter/bool_rewriter.cpp | 13 +- src/ast/rewriter/bool_rewriter.h | 4 +- src/ast/rewriter/bv_rewriter.cpp | 20 +- src/ast/sls/sls_basic_plugin.cpp | 8 +- src/ast/sls/sls_bv_engine.cpp | 4 +- src/ast/sls/sls_bv_eval.cpp | 8 +- src/ast/sls/sls_bv_eval.h | 2 + src/ast/sls/sls_bv_evaluator.h | 1 + src/ast/sls/sls_bv_fixed.cpp | 2 + src/ast/sls/sls_bv_lookahead.cpp | 414 +++++++++++++++++++++-------- src/ast/sls/sls_bv_lookahead.h | 78 ++++-- src/ast/sls/sls_bv_plugin.cpp | 4 + src/ast/sls/sls_bv_plugin.h | 1 + src/ast/sls/sls_bv_terms.cpp | 48 +++- src/ast/sls/sls_bv_terms.h | 10 +- src/ast/sls/sls_bv_tracker.h | 144 ++++------ src/ast/sls/sls_context.cpp | 2 +- 17 files changed, 506 insertions(+), 257 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 2732bd7e0..9c8eeed85 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -671,12 +671,12 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) expr* cond2 = nullptr, *t2 = nullptr, *e2 = nullptr; if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2) && BR_FAILED != try_ite_value(to_app(t), val, result)) { - result = m().mk_ite(cond, result, mk_eq(e, val)); + result = m().mk_ite(cond, result, mk_eq_plain(e, val)); return BR_REWRITE2; } if (m().is_ite(e, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2) && BR_FAILED != try_ite_value(to_app(e), val, result)) { - result = m().mk_ite(cond, mk_eq(t, val), result); + result = m().mk_ite(cond, mk_eq_plain(t, val), result); return BR_REWRITE2; } @@ -684,11 +684,15 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) } -app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) { +app* bool_rewriter::mk_eq_plain(expr* lhs, expr* rhs) { if (m().are_equal(lhs, rhs)) return m().mk_true(); if (m().are_distinct(lhs, rhs)) return m().mk_false(); + if (m().is_false(rhs)) { + verbose_stream() << "here\n"; + } + VERIFY(!m().is_false(rhs)); return m().mk_eq(lhs, rhs); } @@ -775,7 +779,8 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { std::swap(lhs, rhs); if (m().is_not(lhs, lhs)) { - result = m().mk_not(m().mk_eq(lhs, rhs)); + mk_eq(lhs, rhs, result); + mk_not(result, result); return BR_REWRITE2; } diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 421811ed4..aec8e0700 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -135,11 +135,11 @@ public: br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result); br_status mk_not_core(expr * t, expr_ref & result); - app* mk_eq(expr* lhs, expr* rhs); + app* mk_eq_plain(expr* lhs, expr* rhs); void mk_eq(expr * lhs, expr * rhs, expr_ref & result) { if (mk_eq_core(lhs, rhs, result) == BR_FAILED) - result = mk_eq(lhs, rhs); + result = mk_eq_plain(lhs, rhs); } expr_ref mk_eq_rw(expr* lhs, expr* rhs) { expr_ref r(m()), _lhs(lhs, m()), _rhs(rhs, m()); diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 3636e2b88..a53ba90c1 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -640,8 +640,13 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref // use the equivalence to simplify: // #x000f <=_u b <=> b[sz-1:lnz+1] != 0 or #xf <= b[lnz:0]) - result = m.mk_implies(m.mk_eq(m_mk_extract(bv_sz - 1, lnz + 1, b), mk_zero(bv_sz - lnz - 1)), - m_util.mk_ule(m_mk_extract(lnz, 0, a), m_mk_extract(lnz, 0, b))); + expr_ref e1(m_mk_extract(bv_sz - 1, lnz + 1, b), m); + expr_ref e2(mk_zero(bv_sz - lnz - 1), m); + e1 = m.mk_eq(e1, e2); + expr_ref e3(m_mk_extract(lnz, 0, a), m); + expr_ref e4(m_mk_extract(lnz, 0, b), m); + e2 = m_util.mk_ule(e3, e4); + result = m.mk_implies(e1, e2); return BR_REWRITE_FULL; } } @@ -866,6 +871,13 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ return BR_REWRITE2; } + // [....][xx] -> [yy][....] hi <= |[....]| then can extract [hi + k:lo + k] + // (ashr t k)[hi:0] -> t[hi+k:k] + if (low == 0 && m_util.is_bv_ashr(arg, t, c) && m_util.is_numeral(c, v, sz) && high < sz - v) { + result = m_mk_extract(high + v.get_unsigned(), low + v.get_unsigned(), t); + return BR_REWRITE1; + } + return BR_FAILED; } @@ -2498,8 +2510,8 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { expr* a = nullptr, *b = nullptr, *c = nullptr; if (m.is_ite(lhs, a, b, c)) { bool_rewriter rw(m); - expr_ref e1(rw.mk_eq(b, rhs), m); - expr_ref e2(rw.mk_eq(c, rhs), m); + expr_ref e1(rw.mk_eq_rw(b, rhs), m); + expr_ref e2(rw.mk_eq_rw(c, rhs), m); result = rw.mk_ite(a, e1, e2); return BR_REWRITE2; } diff --git a/src/ast/sls/sls_basic_plugin.cpp b/src/ast/sls/sls_basic_plugin.cpp index bb876c44f..50fa9d25d 100644 --- a/src/ast/sls/sls_basic_plugin.cpp +++ b/src/ast/sls/sls_basic_plugin.cpp @@ -29,7 +29,7 @@ namespace sls { bool basic_plugin::is_basic(expr* e) const { if (!e || !is_app(e)) return false; - if (m.is_ite(e) && !m.is_bool(e) && false) + if (m.is_ite(e) && !m.is_bool(e)) return true; if (m.is_xor(e) && to_app(e)->get_num_args() != 2) return true; @@ -149,7 +149,6 @@ namespace sls { if (m.is_value(child)) return false; bool r = ctx.set_value(child, ctx.get_value(e)); - verbose_stream() << "repair-ite-down " << mk_bounded_pp(e, m) << " @ " << mk_bounded_pp(child, m) << " := " << ctx.get_value(e) << " success " << r << "\n"; return r; } @@ -166,7 +165,6 @@ namespace sls { val = eval_distinct(e); else return; - verbose_stream() << "repair-up " << mk_bounded_pp(e, m) << " " << val << "\n"; if (!ctx.set_value(e, val)) ctx.new_value_eh(e); } @@ -176,14 +174,14 @@ namespace sls { bool basic_plugin::repair_down(app* e) { if (!is_basic(e)) - return true; + return true; + if (m.is_xor(e) && eval_xor(e) == ctx.get_value(e)) return true; if (m.is_ite(e) && eval_ite(e) == ctx.get_value(e)) return true; if (m.is_distinct(e) && eval_distinct(e) == ctx.get_value(e)) return true; - verbose_stream() << "basic repair down " << mk_bounded_pp(e, m) << "\n"; unsigned n = e->get_num_args(); unsigned s = ctx.rand(n); for (unsigned i = 0; i < n; ++i) { diff --git a/src/ast/sls/sls_bv_engine.cpp b/src/ast/sls/sls_bv_engine.cpp index 124a5ea77..f9d1da552 100644 --- a/src/ast/sls/sls_bv_engine.cpp +++ b/src/ast/sls/sls_bv_engine.cpp @@ -477,9 +477,7 @@ lbool sls_engine::search() { // update assertion weights if a weighting is enabled (sp < 1024) if (m_paws) { - for (unsigned i = 0; i < sz; i++) - { - expr * q = m_assertions[i]; + for (auto q : m_assertions) { // smooth weights with probability sp / 1024 if (m_tracker.get_random_uint(10) < m_paws_sp) { diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index c4f2dbb64..a78dba875 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/src/ast/sls/sls_bv_eval.cpp @@ -48,6 +48,10 @@ namespace sls { } } + void bv_eval::start_propagation() { + m_lookahead.start_propagation(); + } + void bv_eval::add_bit_vector(app* e) { if (!bv.is_bv(e)) return; @@ -688,8 +692,6 @@ namespace sls { expr* arg = e->get_arg(i); if (m.is_value(arg)) return false; - if (m.is_bool(e) && is_lookahead_phase() && m_lookahead.try_repair_down(e)) - return true; if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) { commit_eval(e, to_app(arg)); IF_VERBOSE(11, verbose_stream() << "repair " << mk_bounded_pp(e, m) << " : " << mk_bounded_pp(arg, m) << " := " << wval(arg) << "\n";); @@ -702,8 +704,6 @@ namespace sls { ctx.new_value_eh(arg); return true; } - if (m.is_bool(e) && m_lookahead.try_repair_down(e)) - return true; return false; } diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h index 3f5f87024..b9729f196 100644 --- a/src/ast/sls/sls_bv_eval.h +++ b/src/ast/sls/sls_bv_eval.h @@ -156,6 +156,8 @@ namespace sls { void init() { m_fix.init(); } + void start_propagation(); + void register_term(expr* e); /** diff --git a/src/ast/sls/sls_bv_evaluator.h b/src/ast/sls/sls_bv_evaluator.h index 77fbf9121..13aff4a97 100644 --- a/src/ast/sls/sls_bv_evaluator.h +++ b/src/ast/sls/sls_bv_evaluator.h @@ -658,6 +658,7 @@ public: } void serious_update(func_decl * fd, const mpz & new_value) { + TRACE("sls", tout << "set: " << fd->get_name() << " to " << m_mpz_manager.to_string(new_value) << std::endl;); m_tracker.set_value(fd, new_value); expr * ep = m_tracker.get_entry_point(fd); unsigned cur_depth = m_tracker.get_distance(ep); diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp index 784576992..3439c7637 100644 --- a/src/ast/sls/sls_bv_fixed.cpp +++ b/src/ast/sls/sls_bv_fixed.cpp @@ -29,6 +29,8 @@ namespace sls { void bv_fixed::init() { + return; + for (auto e : ctx.subterms()) set_fixed(e); diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 37ca06b26..36c36d25c 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -3,11 +3,13 @@ Copyright (c) 2024 Microsoft Corporation Module Name: - sls_bv_lookahead.h + sls_bv_lookahead Abstract: - Lookahead solver for BV, modeled after sls_engine/sls_tracker/sls_evaluator. + Lookahead solver for BV, modeled after + sls_bv_engine/sls_bv_tracker/sls_bv_evaluator + by Froelich and Wintersteiger. Author: @@ -18,57 +20,86 @@ Author: #include "ast/sls/sls_bv_lookahead.h" #include "ast/sls/sls_bv_eval.h" #include "ast/sls/sls_bv_terms.h" +#include "params/sls_params.hpp" #include "ast/ast_pp.h" #include namespace sls { - bv_lookahead::bv_lookahead(bv_eval& ev) : - bv(ev.m), - m_ev(ev), - ctx(ev.ctx), - m(ev.m) {} - - bool bv_lookahead::try_repair_down(app* e) { - if (!m.is_bool(e)) - return false; - if (m_ev.bval1(e) == m_ev.bval0(e)) - return true; - auto const& uninterp = m_ev.terms.uninterp_occurs(e); - if (uninterp.empty()) - return false; - - if (false && ctx.rand(10) == 0 && apply_random_update(uninterp)) - return true; - - reset_updates(); - - TRACE("sls", tout << mk_bounded_pp(e, m) << " contains "; - for (auto e : uninterp) - tout << mk_bounded_pp(e, m) << " "; - tout << "\n";); - - for (auto e : uninterp) - add_updates(e); - - m_stats.m_num_lookahead += 1; - m_stats.m_num_updates += m_num_updates; - - TRACE("sls", display_updates(tout)); - - if (apply_update()) - return true; - - return apply_random_update(uninterp); + bv_lookahead::bv_lookahead(bv_eval& ev) : + bv(ev.m), + m_ev(ev), + ctx(ev.ctx), + m(ev.m) { } - void bv_lookahead::display_updates(std::ostream& out) { - for (unsigned i = 0; i < m_num_updates; ++i) { - auto const& [e, score, new_value] = m_updates[i]; - out << mk_bounded_pp(e, m) << " " << new_value << " score: " << score << "\n"; + void bv_lookahead::init_updates() { + m_best_expr = nullptr; + } + + lbool bv_lookahead::search() { + updt_params(ctx.get_params()); + rescore(); + m_config.max_moves = m_stats.m_moves + m_config.max_moves_base; + + while (m.inc() && m_stats.m_moves < m_config.max_moves) { + m_stats.m_moves++; + check_restart(); + + // get candidate variables + auto& vars = get_candidate_uninterp(); + + if (vars.empty()) + return l_true; + + // random walk with probability 1000/wp + if (ctx.rand(10) < m_config.wp && apply_random_update(vars)) + continue; + + if (apply_guided_update(vars)) + continue; + + apply_random_update(vars); + recalibrate_weights(); } + m_config.max_moves_base += 100; + return l_undef; } + bool bv_lookahead::apply_guided_update(ptr_vector const& vars) { + init_updates(); + double old_top_score = m_top_score; + for (auto u : vars) + add_updates(u); + m_top_score = old_top_score; + return apply_update(); + } + + ptr_vector const& bv_lookahead::get_candidate_uninterp() { + auto const& lits = ctx.root_literals(); + unsigned start = ctx.rand(lits.size()); + for (unsigned i = 0; i < lits.size(); ++i) { + auto lit = lits[(i + start) % lits.size()]; + auto e = ctx.atom(lit.var()); + if (!e || !is_app(e)) + continue; + app* a = to_app(e); + if (!m_ev.can_eval1(a)) + continue; + if (m_ev.bval0(a) == m_ev.bval1(a)) + continue; + auto const& vars = m_ev.terms.uninterp_occurs(a); + VERIFY(!vars.empty()); + TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": "; + for (auto e : vars) + tout << mk_bounded_pp(e, m) << " "; + tout << "\n";); + return vars; + } + return m_vars; + } + + bool bv_lookahead::apply_random_update(ptr_vector const& vars) { while (true) { expr* e = vars[ctx.rand(vars.size())]; @@ -76,22 +107,135 @@ namespace sls { m_v_updated.set_bw(v.bw); v.get_variant(m_v_updated, m_ev.m_rand); v.eval = m_v_updated; - if (!v.commit_eval()) - continue; + if (!v.commit_eval()) + continue; apply_update(e, m_v_updated); break; } return true; } + void bv_lookahead::check_restart() { + + if (m_stats.m_moves % m_config.restart_base == 0) + // ucb_forget(); + rescore(); + + if (m_stats.m_moves < m_config.restart_next) + return; + + if (m_stats.m_restarts & 1) + m_config.restart_next += m_config.restart_base; + else + m_config.restart_next += (2 << (m_stats.m_restarts >> 1)) * m_config.restart_base; + + m_stats.m_restarts++; + + // TODO: reset values of uninterpreted to 0 + } + + void bv_lookahead::updt_params(params_ref const& _p) { + sls_params p(_p); + //m_config.max_restarts = p.max_restarts(); + m_config.walksat = p.walksat(); + m_config.walksat_repick = p.walksat_repick(); + m_config.paws_sp = p.paws_sp(); + m_config.paws = m_config.paws_sp < 1024; + m_config.wp = p.wp(); + m_config.restart_base = p.restart_base(); + m_config.restart_next = m_config.restart_base; + m_config.restart_init = p.restart_init(); + m_config.early_prune = p.early_prune(); + } + + double bv_lookahead::new_score(app* a) { + bool is_true = ctx.is_true(a); + bool is_true_new = m_ev.bval1(a); + if (!ctx.is_relevant(a)) + return 0; + if (is_true == is_true_new) + return 1; + expr* x, * y; + if (is_true && m.is_eq(a, x, y) && bv.is_bv(x)) { + auto const& vx = wval(x); + auto const& vy = wval(y); + // hamming distance between vx.bits() and vy.bits(): + double delta = 0; + for (unsigned i = 0; i < vx.bw; ++i) + if (vx.bits().get(i) != vy.bits().get(i)) + ++delta; + return 1 - (delta / vx.bw); + } + else if (bv.is_ule(a, x, y)) { + auto const& vx = wval(x); + auto const& vy = wval(y); + + if (is_true) + // x > y as unsigned. + // x - y > 0 + // score = (x - y) / 2^bw + vx.set_sub(m_ev.m_tmp, vx.bits(), vy.bits()); + else { + // x <= y as unsigned. + // y - x >= 0 + // score = (y - x + 1) / 2^bw + vx.set_sub(m_ev.m_tmp, vy.bits(), vx.bits()); + vx.add1(m_ev.m_tmp); + } + rational n = m_ev.m_tmp.get_value(vx.nw); + n /= rational(rational::power_of_two(vx.bw)); + double dbl = n.get_double(); + return (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + } + else if (bv.is_sle(a, x, y)) { + auto const& vx = wval(x); + auto const& vy = wval(y); + // x += 2^bw-1 + // y += 2^bw-1 + vy.bits().copy_to(vy.nw, m_ev.m_tmp); + vx.bits().copy_to(vx.nw, m_ev.m_tmp2); + m_ev.m_tmp.set(vy.bw - 1, !m_ev.m_tmp.get(vy.bw - 1)); + m_ev.m_tmp2.set(vx.bw - 1, !m_ev.m_tmp2.get(vx.bw - 1)); + + if (is_true) { + // x >s y + // x' - y' > 0 + vx.set_sub(m_ev.m_tmp3, m_ev.m_tmp2, m_ev.m_tmp); + } + else { + // x <=s y + // y' - x' >= 0 + vx.set_sub(m_ev.m_tmp3, m_ev.m_tmp, m_ev.m_tmp2); + vx.add1(m_ev.m_tmp3); + } + rational n = m_ev.m_tmp3.get_value(vx.nw); + n /= rational(rational::power_of_two(vx.bw)); + double dbl = n.get_double(); + return (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + } + else if (is_true && m.is_distinct(a) && bv.is_bv(a->get_arg(0))) { + double np = 0, nd = 0; + for (unsigned i = 0; i < a->get_num_args(); ++i) { + auto const& vi = wval(a->get_arg(i)); + for (unsigned j = i + 1; j < a->get_num_args(); ++j) { + ++np; + auto const& vj = wval(a->get_arg(j)); + if (vi.bits() != vj.bits()) + nd++; + } + } + return nd / np; + } + + return 0; + } + double bv_lookahead::lookahead(expr* e, bvect const& new_value) { SASSERT(bv.is_bv(e)); SASSERT(is_uninterp(e)); SASSERT(m_restore.empty()); bool has_tabu = false; - int result = 0; - int breaks = 0; wval(e).eval = new_value; if (!insert_update(e)) { @@ -115,20 +259,8 @@ namespace sls { has_tabu = true; } else if (m.is_bool(a) && m_ev.can_eval1(a)) { - if (!ctx.is_relevant(a)) - continue; - bool is_true = ctx.is_true(a); - bool is_true_new = m_ev.bval1(a); - bool is_true_old = m_ev.bval1_tmp(a); - TRACE("sls_verbose", tout << mk_bounded_pp(a, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n"); - if (is_true_new == is_true_old) - continue; - if (is_true == is_true_new) - ++result; - if (is_true == is_true_old) { - --result; - ++breaks; - } + + rescore(a); } else { IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(a, m) << "\n"); @@ -140,46 +272,55 @@ namespace sls { m_in_update_stack.reset(); restore_lookahead(); - TRACE("sls_verbose", tout << mk_bounded_pp(e, m) << " " << new_value << " " << result << " " << breaks << "\n"); + TRACE("sls_verbose", tout << mk_bounded_pp(e, m) << " := " << new_value << " score: " << m_top_score << "\n"); if (has_tabu) return -10000; - if (result < 0) - return 0.0000001; - else if (result == 0) - return 0.000002; - for (int i = m_prob_break.size(); i <= breaks; ++i) - m_prob_break.push_back(std::pow(m_config.cb, -i)); - return m_prob_break[breaks]; + if (m_top_score <= 0.000001) + return -10000; + return m_top_score; } - void bv_lookahead::try_set(expr* e, bvect const& new_value) { - if (!wval(e).can_set(new_value)) + void bv_lookahead::try_set(expr* u, bvect const& new_value) { + if (!wval(u).can_set(new_value)) return; - auto d = lookahead(e, new_value); - if (d > 0) - add_update(d, e, new_value); + auto score = lookahead(u, new_value); + ++m_stats.m_num_updates; + verbose_stream() << mk_bounded_pp(u, m) << " " << new_value << " score: " << score << "\n"; + if (score > m_best_score) { + m_best_score = score; + m_best_expr = u; + m_best_value.set_bw(new_value.bw); + new_value.copy_to(new_value.nw, m_best_value); + } } - void bv_lookahead::add_updates(expr* e) { - SASSERT(bv.is_bv(e)); - auto& v = wval(e); + void bv_lookahead::add_updates(expr* u) { + SASSERT(bv.is_bv(u)); + auto& v = wval(u); while (m_v_saved.size() < v.bits().size()) { m_v_saved.push_back(0); m_v_updated.push_back(0); + m_best_value.push_back(0); } + m_v_saved.set_bw(v.bw); m_v_updated.set_bw(v.bw); v.bits().copy_to(v.nw, m_v_saved); m_v_saved.copy_to(v.nw, m_v_updated); // flip a single bit - for (unsigned i = 0; i < v.bw; ++i) { + for (unsigned i = 0; i < v.bw && i <= 32; ++i) { m_v_updated.set(i, !m_v_updated.get(i)); - try_set(e, m_v_updated); - //verbose_stream() << "flip " << d << " " << m_v_updated << "\n"; + try_set(u, m_v_updated); m_v_updated.set(i, !m_v_updated.get(i)); } + if (v.bw > 32) { + unsigned j = ctx.rand(v.bw - 32) + 32; + m_v_updated.set(j, !m_v_updated.get(j)); + try_set(u, m_v_updated); + m_v_updated.set(j, !m_v_updated.get(j)); + } if (v.bw <= 1) return; @@ -187,47 +328,39 @@ namespace sls { for (unsigned i = 0; i < v.nw; ++i) m_v_updated[i] = ~m_v_updated[i]; v.clear_overflow_bits(m_v_updated); - try_set(e, m_v_updated); + try_set(u, m_v_updated); // increment m_v_saved.copy_to(v.nw, m_v_updated); v.add1(m_v_updated); - try_set(e, m_v_updated); + try_set(u, m_v_updated); // decrement m_v_saved.copy_to(v.nw, m_v_updated); v.sub1(m_v_updated); - try_set(e, m_v_updated); + try_set(u, m_v_updated); - // random, deffered to failure path - // v.get_variant(m_v_updated, m_ev.m_rand); - // try_set(e, m_v_updated); + // reset to original value + try_set(u, m_v_saved); } bool bv_lookahead::apply_update() { - double sum_score = 0; - for (unsigned i = 0; i < m_num_updates; ++i) - sum_score += m_updates[i].score; - double pos = (sum_score * m_ev.m_rand()) / (double)m_ev.m_rand.max_value(); - for (unsigned i = 0; i < m_num_updates; ++i) { - auto const& [e, score, new_value] = m_updates[i]; - pos -= score; - if (pos <= 0.00000000001) { - TRACE("sls", tout << "apply " << mk_bounded_pp(e, m) << " new value " << new_value << " " << score << "\n"); - apply_update(e, new_value); - return true; - } - } - TRACE("sls", tout << "no update " << m_num_updates << "\n"); - return false; + CTRACE("bv", !m_best_expr, tout << "no update\n"); + if (!m_best_expr) + return false; + apply_update(m_best_expr, m_best_value); + return true; } void bv_lookahead::apply_update(expr* e, bvect const& new_value) { + TRACE("bv", tout << "apply " << mk_bounded_pp(e, m) << " new value " << new_value << "\n"); SASSERT(bv.is_bv(e)); SASSERT(is_uninterp(e)); SASSERT(m_restore.empty()); wval(e).eval = new_value; + //verbose_stream() << mk_bounded_pp(e, m) << " := " << new_value << "\n"; + VERIFY(wval(e).commit_eval()); insert_update_stack(e); unsigned max_depth = get_depth(e); @@ -237,25 +370,25 @@ namespace sls { if (bv.is_bv(e)) { m_ev.eval(e); // updates wval(e).eval if (!wval(e).commit_eval()) { - TRACE("sls", tout << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); + TRACE("bv", tout << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); // bv_plugin::is_sat picks up discrepancies continue; } for (auto p : ctx.parents(e)) { insert_update_stack(p); max_depth = std::max(max_depth, get_depth(p)); - } + } } else if (m.is_bool(e) && m_ev.can_eval1(e)) { - VERIFY(m_ev.repair_up(e)); + rescore(e); } else { - UNREACHABLE(); + UNREACHABLE(); } } m_update_stack[depth].reset(); } - m_in_update_stack.reset(); + m_in_update_stack.reset(); } bool bv_lookahead::insert_update(expr* e) { @@ -273,7 +406,7 @@ namespace sls { if (!m_in_update_stack.is_marked(e) && is_app(e)) { m_in_update_stack.mark(e); m_update_stack[depth].push_back(to_app(e)); - } + } } void bv_lookahead::restore_lookahead() { @@ -293,8 +426,75 @@ namespace sls { return m_on_restore.is_marked(e); } + unsigned bv_lookahead::get_weight(expr* e) { + return m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0 }).weight; + } + + void bv_lookahead::inc_weight(expr* e) { + m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0 }).weight += 1; + } + + void bv_lookahead::dec_weight(expr* e) { + auto& w = m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0 }).weight; + w = w > m_config.paws_init ? w - 1 : m_config.paws_init; + } + + void bv_lookahead::set_score(app* a, double d) { + m_bool_info.insert_if_not_there(a, { m_config.paws_init, 0 }).score = d; + } + + double bv_lookahead::old_score(app* a) { + return m_bool_info.insert_if_not_there(a, { m_config.paws_init, 0 }).score; + } + + void bv_lookahead::rescore() { + m_top_score = 0; + m_rescore = false; + for (auto lit : ctx.root_literals()) { + auto e = ctx.atom(lit.var()); + if (!e || !is_app(e)) + continue; + app* a = to_app(e); + if (!m_ev.can_eval1(a)) + continue; + + double score = new_score(a); + set_score(a, score); + m_top_score += score; + } + verbose_stream() << "top score " << m_top_score << "\n"; + + } + + void bv_lookahead::rescore(app* e) { + double score = new_score(e); + m_top_score += get_weight(e) * (score - old_score(e)); + set_score(e, score); + } + + void bv_lookahead::recalibrate_weights() { + for (auto lit : ctx.root_literals()) { + auto e = ctx.atom(lit.var()); + if (!e || !is_app(e)) + continue; + app* a = to_app(e); + if (!m_ev.can_eval1(a)) + continue; + bool is_true = ctx.is_true(lit); + bool is_true_a = m_ev.bval1(a); + if (ctx.rand(10) < m_config.paws_sp) { + if (is_true == is_true_a) + dec_weight(a); + } + else if (is_true != is_true_a) + inc_weight(a); + } + m_best_score = 0; + } + void bv_lookahead::collect_statistics(statistics& st) const { st.update("sls-bv-lookahead", m_stats.m_num_lookahead); st.update("sls-bv-updates", m_stats.m_num_updates); + st.update("sls-bv-moves", m_stats.m_moves); } } \ No newline at end of file diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h index c60ad1362..57a4ea1eb 100644 --- a/src/ast/sls/sls_bv_lookahead.h +++ b/src/ast/sls/sls_bv_lookahead.h @@ -24,21 +24,34 @@ namespace sls { class bv_eval; class bv_lookahead { + struct config { double cb = 2.85; - }; - - struct update { - expr* e; - double score; - bvect value; + unsigned paws_init = 40; + unsigned paws_sp = 52; + bool paws = true; + bool walksat = true; + bool walksat_repick = false; + unsigned wp = 100; + unsigned restart_base = 1000; + unsigned restart_next = 1000; + unsigned restart_init = 1000; + bool early_prune = true; + unsigned max_moves = 0; + unsigned max_moves_base = 200; }; struct stats { unsigned m_num_lookahead = 0; unsigned m_num_updates = 0; + unsigned m_moves = 0; + unsigned m_restarts = 0; }; + struct bool_info { + unsigned weight = 0; + double score = 0; + }; bv_util bv; bv_eval& m_ev; @@ -47,49 +60,56 @@ namespace sls { config m_config; stats m_stats; bvect m_v_saved, m_v_updated; - svector m_prob_break; ptr_vector m_restore; vector> m_update_stack; expr_mark m_on_restore, m_in_update_stack; - vector m_updates; - unsigned m_num_updates = 0; + double m_best_score = 0, m_top_score = 0; + bvect m_best_value; + expr* m_best_expr = nullptr; + bool m_rescore = true; + ptr_vector m_vars; - void reset_updates() { m_num_updates = 0; } - - void add_update(double score, expr* e, bvect const& value) { - if (m_num_updates == m_updates.size()) - m_updates.push_back({ e, score, value }); - else { - auto& u = m_updates[m_num_updates]; - u.e = e; - u.score = score; - u.value = value; - } - m_num_updates++; - } - + void init_updates(); bv_valuation& wval(expr* e) const; void insert_update_stack(expr* e); bool insert_update(expr* e); void restore_lookahead(); - double lookahead(expr* e, bvect const& new_value); + double lookahead(expr* u, bvect const& new_value); + double old_score(app* c); + double new_score(app* c); + void set_score(app* c, double d); + void rescore(app* c); - void try_set(expr* e, bvect const& new_value); - void add_updates(expr* e); + void rescore(); + + obj_map m_bool_info; + unsigned get_weight(expr* e); + void inc_weight(expr* e); + void dec_weight(expr* e); + void recalibrate_weights(); + + void try_set(expr* u, bvect const& new_value); + void add_updates(expr* u); void apply_update(expr* e, bvect const& new_value); bool apply_update(); bool apply_random_update(ptr_vector const& vars); + bool apply_guided_update(ptr_vector const& vars); + ptr_vector const& get_candidate_uninterp(); - void display_updates(std::ostream& out); + void check_restart(); public: bv_lookahead(bv_eval& ev); - bool on_restore(expr* e) const; + void updt_params(params_ref const& p); - bool try_repair_down(app* e); + lbool search(); + + void start_propagation() { m_rescore = true; } + + bool on_restore(expr* e) const; void collect_statistics(statistics& st) const; diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp index 78d367770..3342dcba2 100644 --- a/src/ast/sls/sls_bv_plugin.cpp +++ b/src/ast/sls/sls_bv_plugin.cpp @@ -50,6 +50,10 @@ namespace sls { return false; } + void bv_plugin::start_propagation() { + m_eval.start_propagation(); + } + void bv_plugin::propagate_literal(sat::literal lit) { SASSERT(ctx.is_true(lit)); auto e = ctx.atom(lit.var()); diff --git a/src/ast/sls/sls_bv_plugin.h b/src/ast/sls/sls_bv_plugin.h index 7bcc4c329..4ad2df806 100644 --- a/src/ast/sls/sls_bv_plugin.h +++ b/src/ast/sls/sls_bv_plugin.h @@ -41,6 +41,7 @@ namespace sls { ~bv_plugin() override {} void register_term(expr* e) override; expr_ref get_value(expr* e) override; + void start_propagation() override; void initialize() override; void propagate_literal(sat::literal lit) override; bool propagate() override; diff --git a/src/ast/sls/sls_bv_terms.cpp b/src/ast/sls/sls_bv_terms.cpp index a28af9992..76a392e78 100644 --- a/src/ast/sls/sls_bv_terms.cpp +++ b/src/ast/sls/sls_bv_terms.cpp @@ -16,6 +16,7 @@ Author: --*/ #include "ast/ast_ll_pp.h" +#include "ast/ast_pp.h" #include "ast/sls/sls_bv_terms.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/bv_rewriter.h" @@ -23,15 +24,17 @@ Author: namespace sls { bv_terms::bv_terms(sls::context& ctx): + ctx(ctx), m(ctx.get_manager()), bv(m), m_axioms(m) {} void bv_terms::register_term(expr* e) { auto r = ensure_binary(e); - if (r != e) - m_axioms.push_back(m.mk_eq(e, r)); - register_uninterp(e); + if (r != e) { + bool_rewriter br(m); + m_axioms.push_back(br.mk_eq_rw(e, r)); + } } expr_ref bv_terms::ensure_binary(expr* e) { @@ -69,10 +72,10 @@ namespace sls { expr_ref absx = br.mk_ite(signx, bvr.mk_bv_neg(x), x); expr_ref absy = br.mk_ite(signy, bvr.mk_bv_neg(y), y); expr_ref d = expr_ref(bv.mk_bv_udiv(absx, absy), m); - expr_ref r = br.mk_ite(br.mk_eq(signx, signy), d, bvr.mk_bv_neg(d)); - r = br.mk_ite(br.mk_eq(z, y), + expr_ref r = br.mk_ite(br.mk_eq_rw(signx, signy), d, bvr.mk_bv_neg(d)); + r = br.mk_ite(br.mk_eq_rw(z, y), br.mk_ite(signx, o, n1), - br.mk_ite(br.mk_eq(x, z), z, r)); + br.mk_ite(br.mk_eq_rw(x, z), z, r)); return r; } @@ -92,8 +95,8 @@ namespace sls { expr_ref abs_y = br.mk_ite(bvr.mk_sle(z, y), y, bvr.mk_bv_neg(y)); expr_ref u = bvr.mk_bv_urem(abs_x, abs_y); expr_ref r(m); - r = br.mk_ite(br.mk_eq(u, z), z, - br.mk_ite(br.mk_eq(y, z), x, + r = br.mk_ite(br.mk_eq_rw(u, z), z, + br.mk_ite(br.mk_eq_rw(y, z), x, br.mk_ite(br.mk_and(bvr.mk_sle(z, x), bvr.mk_sle(z, x)), u, br.mk_ite(bvr.mk_sle(z, x), bvr.mk_bv_add(y, u), br.mk_ite(bv.mk_sle(z, y), bvr.mk_bv_sub(y, u), bvr.mk_bv_neg(u)))))); @@ -107,10 +110,28 @@ namespace sls { bool_rewriter br(m); bv_rewriter bvr(m); expr_ref z(bv.mk_zero(bv.get_bv_size(x)), m); - r = br.mk_ite(br.mk_eq(y, z), x, bvr.mk_bv_sub(x, bvr.mk_bv_mul(y, mk_sdiv(x, y)))); + r = br.mk_ite(br.mk_eq_rw(y, z), x, bvr.mk_bv_sub(x, bvr.mk_bv_mul(y, mk_sdiv(x, y)))); return r; } + ptr_vector const& bv_terms::uninterp_occurs(expr* e) { + unsigned id = e->get_id(); + m_uninterp_occurs.reserve(id + 1); + if (!m_uninterp_occurs[id].empty()) + return m_uninterp_occurs[id]; + register_uninterp(e); + return m_uninterp_occurs[id]; + } + + ptr_vector const& bv_terms::condition_occurs(expr* e) { + unsigned id = e->get_id(); + m_condition_occurs.reserve(id + 1); + if (!m_condition_occurs[id].empty()) + return m_condition_occurs[id]; + register_uninterp(e); + return m_condition_occurs[id]; + } + void bv_terms::register_uninterp(expr* e) { if (!m.is_bool(e)) return; @@ -123,7 +144,9 @@ namespace sls { else return; m_uninterp_occurs.reserve(e->get_id() + 1); + m_condition_occurs.reserve(e->get_id() + 1); auto& occs = m_uninterp_occurs[e->get_id()]; + auto& cond_occs = m_condition_occurs[e->get_id()]; ptr_vector todo; todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); expr_mark marked; @@ -138,8 +161,11 @@ namespace sls { todo.push_back(arg); } else if (m.is_ite(e, c, th, el)) { - todo.push_back(th); - todo.push_back(el); + cond_occs.push_back(c); + if (ctx.is_true(c)) + todo.push_back(th); + else + todo.push_back(el); } else if (bv.is_bv(e)) occs.push_back(e); diff --git a/src/ast/sls/sls_bv_terms.h b/src/ast/sls/sls_bv_terms.h index effd74eeb..8728ed9d4 100644 --- a/src/ast/sls/sls_bv_terms.h +++ b/src/ast/sls/sls_bv_terms.h @@ -29,10 +29,12 @@ Author: namespace sls { class bv_terms { + context& ctx; ast_manager& m; bv_util bv; expr_ref_vector m_axioms; vector> m_uninterp_occurs; + vector> m_condition_occurs; expr_ref ensure_binary(expr* e); @@ -43,12 +45,16 @@ namespace sls { void register_uninterp(expr* e); public: - bv_terms(sls::context& ctx); + bv_terms(context& ctx); void register_term(expr* e); expr_ref_vector& axioms() { return m_axioms; } - ptr_vector const& uninterp_occurs(expr* e) { m_uninterp_occurs.reserve(e->get_id() + 1); return m_uninterp_occurs[e->get_id()]; } + ptr_vector const& uninterp_occurs(expr* e); + + ptr_vector const& condition_occurs(expr* e); + + }; } diff --git a/src/ast/sls/sls_bv_tracker.h b/src/ast/sls/sls_bv_tracker.h index 67723828f..3d74d55df 100644 --- a/src/ast/sls/sls_bv_tracker.h +++ b/src/ast/sls/sls_bv_tracker.h @@ -23,6 +23,7 @@ Notes: #include "ast/for_each_expr.h" #include "ast/ast_smt2_pp.h" #include "ast/bv_decl_plugin.h" +#include "ast/ast_ll_pp.h" #include "model/model.h" #include "params/sls_params.hpp" @@ -34,23 +35,23 @@ class sls_tracker { bv_util & m_bv_util; powers & m_powers; random_gen m_rng; - unsigned m_random_bits; - unsigned m_random_bits_cnt; + unsigned m_random_bits = 0; + unsigned m_random_bits_cnt = 0; mpz m_zero, m_one, m_two; struct value_score { - value_score() : m(nullptr), value(unsynch_mpz_manager::mk_z(0)), score(0.0), score_prune(0.0), has_pos_occ(0), has_neg_occ(0), distance(0), touched(1) {}; + value_score() : value(unsynch_mpz_manager::mk_z(0)) {}; value_score(value_score&&) noexcept = default; ~value_score() { if (m) m->del(value); } value_score& operator=(value_score&&) = default; - unsynch_mpz_manager * m; + unsynch_mpz_manager * m = nullptr; mpz value; - double score; - double score_prune; - unsigned has_pos_occ; - unsigned has_neg_occ; - unsigned distance; // max distance from any root - unsigned touched; + double score = 0.0; + double score_prune = 0.0; + unsigned has_pos_occ = 0; + unsigned has_neg_occ = 0; + unsigned distance = 0; // max distance from any root + unsigned touched = 1; }; public: @@ -67,21 +68,21 @@ private: ptr_vector m_constants; ptr_vector m_temp_constants; occ_type m_constants_occ; - unsigned m_last_pos; - unsigned m_walksat; - unsigned m_ucb; - double m_ucb_constant; - unsigned m_ucb_init; - double m_ucb_forget; - double m_ucb_noise; - unsigned m_touched; - double m_scale_unsat; - unsigned m_paws_init; + unsigned m_last_pos = 0; + unsigned m_walksat = 0; + unsigned m_ucb = 0; + double m_ucb_constant = 0; + unsigned m_ucb_init = 0; + double m_ucb_forget = 0; + double m_ucb_noise = 0; + unsigned m_touched = 0; + double m_scale_unsat = 0; + unsigned m_paws_init = 0; obj_map m_where_false; - expr** m_list_false; - unsigned m_track_unsat; + expr** m_list_false = nullptr; + unsigned m_track_unsat = 0; obj_map m_weights; - double m_top_sum; + double m_top_sum = 0; obj_hashtable m_temp_seen; public: @@ -89,8 +90,7 @@ public: m_manager(m), m_mpz_manager(mm), m_bv_util(bvu), - m_powers(p), - m_random_bits_cnt(0), + m_powers(p), m_zero(m_mpz_manager.mk_z(0)), m_one(m_mpz_manager.mk_z(1)), m_two(m_mpz_manager.mk_z(2)) { @@ -144,7 +144,7 @@ public: }*/ inline void adapt_top_sum(expr * e, double add, double sub) { - m_top_sum += m_weights.find(e) * (add - sub); + m_top_sum += get_weight(e) * (add - sub); } inline void set_top_sum(double new_score) { @@ -160,12 +160,7 @@ public: } inline bool is_sat() { - for (obj_hashtable::iterator it = m_top_expr.begin(); - it != m_top_expr.end(); - it++) - if (!m_mpz_manager.is_one(get_value(*it))) - return false; - return true; + return all_of(m_top_expr, [this](expr* e) { return m_mpz_manager.is_one(get_value(e)); }); } inline void set_value(expr * n, const mpz & r) { @@ -290,12 +285,9 @@ public: } // Update uplinks - unsigned na = n->get_num_args(); - for (unsigned i = 0; i < na; i++) { - expr * c = n->get_arg(i); + for (auto c : *n) m_uplinks.insert_if_not_there(c, ptr_vector()).push_back(n); - } - + func_decl * d = n->get_decl(); if (n->get_num_args() == 0) { @@ -414,8 +406,7 @@ public: init_proc proc(m_manager, *this); expr_mark visited; unsigned sz = as.size(); - for (unsigned i = 0; i < sz; i++) { - expr * e = as[i]; + for (auto e : as) { if (!m_top_expr.contains(e)) m_top_expr.insert(e); for_each_expr(proc, visited, e); @@ -423,8 +414,7 @@ public: visited.reset(); - for (unsigned i = 0; i < sz; i++) { - expr * e = as[i]; + for (auto e : as) { ptr_vector t; m_constants_occ.insert_if_not_there(e, t); find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); @@ -447,16 +437,14 @@ public: } m_temp_seen.reset(); - for (unsigned i = 0; i < sz; i++) - { - expr * e = as[i]; + for (auto e : as) { // initialize weights if (!m_weights.contains(e)) m_weights.insert(e, m_paws_init); // positive/negative occurrences used for early pruning - setup_occs(as[i]); + setup_occs(e); } // initialize ucb total touched value (individual ones are always initialized to 1) @@ -629,7 +617,7 @@ public: } void randomize(ptr_vector const & as) { - TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); + TRACE("sls_verbose", tout << "Abandoned model:" << std::endl; show_model(tout); ); for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { func_decl * fd = it->m_key; @@ -643,7 +631,7 @@ public: } void reset(ptr_vector const & as) { - TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); + TRACE("sls_verbose", tout << "Abandoned model:" << std::endl; show_model(tout); ); for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { set_value(it->m_value, m_zero); @@ -656,11 +644,7 @@ public: if (m_manager.is_and(n) || m_manager.is_or(n)) { SASSERT(!negated); - app * a = to_app(n); - expr * const * args = a->get_args(); - for (unsigned i = 0; i < a->get_num_args(); i++) - { - expr * child = args[i]; + for (auto child : *to_app(n)) { if (!m_temp_seen.contains(child)) { setup_occs(child, false); @@ -706,29 +690,22 @@ public: } else if (m_manager.is_and(n)) { SASSERT(!negated); - app * a = to_app(n); - expr * const * args = a->get_args(); /* Andreas: Seems to have no effect. But maybe you want to try it again at some point. double sum = 0.0; for (unsigned i = 0; i < a->get_num_args(); i++) sum += get_score(args[i]); res = sum / (double) a->get_num_args(); */ double min = 1.0; - for (unsigned i = 0; i < a->get_num_args(); i++) { - double cur = get_score(args[i]); - if (cur < min) min = cur; - } + for (auto arg : *to_app(n)) + min = std::min(get_score(arg), min); + res = min; } else if (m_manager.is_or(n)) { SASSERT(!negated); - app * a = to_app(n); - expr * const * args = a->get_args(); double max = 0.0; - for (unsigned i = 0; i < a->get_num_args(); i++) { - double cur = get_score(args[i]); - if (cur > max) max = cur; - } + for (auto arg : *to_app(n)) + max = std::max(get_score(arg), max); res = max; } else if (m_manager.is_ite(n)) { @@ -776,6 +753,7 @@ public: " ; SZ = " << bv_sz << std::endl; ); m_mpz_manager.del(diff); m_mpz_manager.del(diff_m1); + //verbose_stream() << "hamming distance: " << mk_bounded_pp(n, m_manager) << " := " << res << "\n"; } else NOT_IMPLEMENTED_YET(); @@ -967,39 +945,35 @@ public: ptr_vector & get_unsat_constants_gsat(ptr_vector const & as) { unsigned sz = as.size(); - if (sz == 1) { - if (m_mpz_manager.neq(get_value(as[0]), m_one)) - return get_constants(); - } + if (sz == 1 && m_mpz_manager.neq(get_value(as[0]), m_one)) + return get_constants(); m_temp_constants.reset(); - for (unsigned i = 0; i < sz; i++) { - expr * q = as[i]; + for (auto q : as) { if (m_mpz_manager.eq(get_value(q), m_one)) continue; ptr_vector const & this_decls = m_constants_occ.find(q); - unsigned sz2 = this_decls.size(); - for (unsigned j = 0; j < sz2; j++) { - func_decl * fd = this_decls[j]; + for (auto fd : this_decls) if (!m_temp_constants.contains(fd)) - m_temp_constants.push_back(fd); - } + m_temp_constants.push_back(fd); } + TRACE("sls", tout << "candidates "; for (auto f : m_temp_constants) tout << f->get_name() << " "; tout << std::endl;); return m_temp_constants; } - ptr_vector & get_unsat_constants_walksat(expr * e) { - if (!e || !m_temp_constants.empty()) - return m_temp_constants; - ptr_vector const & this_decls = m_constants_occ.find(e); - unsigned sz = this_decls.size(); - for (unsigned j = 0; j < sz; j++) { - func_decl * fd = this_decls[j]; - if (!m_temp_constants.contains(fd)) - m_temp_constants.push_back(fd); - } + ptr_vector& get_unsat_constants_walksat(expr* e) { + if (!e || !m_temp_constants.empty()) return m_temp_constants; + ptr_vector const& this_decls = m_constants_occ.find(e); + for (auto fd : this_decls) + if (!m_temp_constants.contains(fd)) + m_temp_constants.push_back(fd); + + TRACE("sls", tout << "candidates " << mk_bounded_pp(e, m_manager) << " "; + for (auto f : m_temp_constants) tout << f->get_name() << " "; tout << std::endl;); + + return m_temp_constants; } ptr_vector & get_unsat_constants(ptr_vector const & as) { diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index cab031d52..5cdb0934c 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -327,7 +327,7 @@ namespace sls { m_constraint_trail.push_back(e); add_clause(e); m_new_constraint = true; - verbose_stream() << "add constraint\n"; + IF_VERBOSE(3, verbose_stream() << "add constraint " << mk_bounded_pp(e, m) << "\n"); ++m_stats.m_num_constraints; } From 3526d03cca34b47b3fc4a2af8560c16effbbb195 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 Dec 2024 18:01:32 -0800 Subject: [PATCH 10/12] remove VERIFY output Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bool_rewriter.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 9c8eeed85..9884c4d18 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -689,10 +689,6 @@ app* bool_rewriter::mk_eq_plain(expr* lhs, expr* rhs) { return m().mk_true(); if (m().are_distinct(lhs, rhs)) return m().mk_false(); - if (m().is_false(rhs)) { - verbose_stream() << "here\n"; - } - VERIFY(!m().is_false(rhs)); return m().mk_eq(lhs, rhs); } From 6ea68310c971027b3bd788aa4ff6a6e0e195c398 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 Dec 2024 18:21:59 -0800 Subject: [PATCH 11/12] fix stack overflow regression in bool_rewriter Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bool_rewriter.cpp | 3 +-- src/ast/sls/sls_bv_lookahead.cpp | 19 +++++++++++-------- src/ast/sls/sls_bv_lookahead.h | 7 +++++-- 3 files changed, 17 insertions(+), 12 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 9884c4d18..e5d5f9110 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -775,8 +775,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { std::swap(lhs, rhs); if (m().is_not(lhs, lhs)) { - mk_eq(lhs, rhs, result); - mk_not(result, result); + result = m().mk_not(m().mk_eq(lhs, rhs)); return BR_REWRITE2; } diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 36c36d25c..46f52ec33 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -91,12 +91,11 @@ namespace sls { auto const& vars = m_ev.terms.uninterp_occurs(a); VERIFY(!vars.empty()); TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": "; - for (auto e : vars) - tout << mk_bounded_pp(e, m) << " "; - tout << "\n";); + for (auto e : vars) tout << mk_bounded_pp(e, m) << " "; + tout << "\n";); return vars; } - return m_vars; + return m_empty_vars; } @@ -258,10 +257,10 @@ namespace sls { else has_tabu = true; } - else if (m.is_bool(a) && m_ev.can_eval1(a)) { - + else if (is_root(a)) rescore(a); - } + else if (m.is_bool(a)) + continue; else { IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(a, m) << "\n"); has_tabu = true; @@ -379,9 +378,11 @@ namespace sls { max_depth = std::max(max_depth, get_depth(p)); } } - else if (m.is_bool(e) && m_ev.can_eval1(e)) { + else if (is_root(e)) { rescore(e); } + else if (m.is_bool(e)) + continue; else { UNREACHABLE(); } @@ -450,6 +451,7 @@ namespace sls { void bv_lookahead::rescore() { m_top_score = 0; m_rescore = false; + m_is_root.reset(); for (auto lit : ctx.root_literals()) { auto e = ctx.atom(lit.var()); if (!e || !is_app(e)) @@ -461,6 +463,7 @@ namespace sls { double score = new_score(a); set_score(a, score); m_top_score += score; + m_is_root.mark(a); } verbose_stream() << "top score " << m_top_score << "\n"; diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h index 57a4ea1eb..2b3aed8d4 100644 --- a/src/ast/sls/sls_bv_lookahead.h +++ b/src/ast/sls/sls_bv_lookahead.h @@ -67,7 +67,9 @@ namespace sls { bvect m_best_value; expr* m_best_expr = nullptr; bool m_rescore = true; - ptr_vector m_vars; + ptr_vector m_empty_vars; + obj_map m_bool_info; + expr_mark m_is_root; void init_updates(); @@ -84,11 +86,12 @@ namespace sls { void rescore(); - obj_map m_bool_info; + unsigned get_weight(expr* e); void inc_weight(expr* e); void dec_weight(expr* e); void recalibrate_weights(); + bool is_root(expr* e) { return m_is_root.is_marked(e); } void try_set(expr* u, bvect const& new_value); void add_updates(expr* u); From d81de1a67ecb8e7c808f69a9dc209bd06a2bf4d8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Dec 2024 21:22:32 -0800 Subject: [PATCH 12/12] align updated version of lookahead with legacy heuristics --- src/ast/sls/sls_bv_engine.cpp | 8 +- src/ast/sls/sls_bv_fixed.cpp | 4 +- src/ast/sls/sls_bv_lookahead.cpp | 340 ++++++++++++++++++++----------- src/ast/sls/sls_bv_lookahead.h | 50 +++-- 4 files changed, 257 insertions(+), 145 deletions(-) diff --git a/src/ast/sls/sls_bv_engine.cpp b/src/ast/sls/sls_bv_engine.cpp index f9d1da552..8d009b500 100644 --- a/src/ast/sls/sls_bv_engine.cpp +++ b/src/ast/sls/sls_bv_engine.cpp @@ -96,7 +96,6 @@ double sls_engine::top_score() { for (expr* e : m_assertions) { top_sum += m_tracker.get_score(e); } - TRACE("sls_top", tout << "Score distribution:"; for (expr* e : m_assertions) tout << " " << m_tracker.get_score(e); @@ -466,7 +465,6 @@ lbool sls_engine::search() { // randomize if no increasing move was found if (new_const == static_cast(-1)) { - score = old_score; if (m_walksat_repick) m_evaluator.randomize_local(m_assertions); else @@ -481,16 +479,16 @@ lbool sls_engine::search() { // smooth weights with probability sp / 1024 if (m_tracker.get_random_uint(10) < m_paws_sp) { - if (m_mpz_manager.eq(m_tracker.get_value(q),m_one)) + if (m_mpz_manager.eq(m_tracker.get_value(q), m_one)) m_tracker.decrease_weight(q); } // increase weights otherwise else { - if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero)) + if (m_mpz_manager.eq(m_tracker.get_value(q), m_zero)) m_tracker.increase_weight(q); } - } + } } } // otherwise, apply most increasing move diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp index 3439c7637..96e9e1579 100644 --- a/src/ast/sls/sls_bv_fixed.cpp +++ b/src/ast/sls/sls_bv_fixed.cpp @@ -27,9 +27,7 @@ namespace sls { ctx(ctx) {} - void bv_fixed::init() { - - return; + void bv_fixed::init() { for (auto e : ctx.subterms()) set_fixed(e); diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 46f52ec33..13e0146e6 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -33,11 +33,12 @@ namespace sls { m(ev.m) { } - void bv_lookahead::init_updates() { - m_best_expr = nullptr; + void bv_lookahead::start_propagation() { + if (m_stats.m_num_propagations++ % m_config.propagation_base == 0) + search(); } - lbool bv_lookahead::search() { + void bv_lookahead::search() { updt_params(ctx.get_params()); rescore(); m_config.max_moves = m_stats.m_moves + m_config.max_moves_base; @@ -50,92 +51,181 @@ namespace sls { auto& vars = get_candidate_uninterp(); if (vars.empty()) - return l_true; + return; - // random walk with probability 1000/wp - if (ctx.rand(10) < m_config.wp && apply_random_update(vars)) + // random walk with probability 1024/wp + if (ctx.rand(2047) < m_config.wp && apply_random_move(vars)) continue; - if (apply_guided_update(vars)) + if (apply_guided_move(vars)) continue; - apply_random_update(vars); - recalibrate_weights(); + if (apply_random_update(get_candidate_uninterp())) + recalibrate_weights(); } m_config.max_moves_base += 100; - return l_undef; } - bool bv_lookahead::apply_guided_update(ptr_vector const& vars) { - init_updates(); - double old_top_score = m_top_score; - for (auto u : vars) - add_updates(u); - m_top_score = old_top_score; - return apply_update(); + bool bv_lookahead::apply_guided_move(ptr_vector const& vars) { + m_best_expr = nullptr; + m_best_score = m_top_score; + unsigned sz = vars.size(); + unsigned start = ctx.rand(sz); + for (unsigned i = 0; i < sz; ++i) + add_updates(vars[(start + i) % sz]); + TRACE("bv", tout << "guided update " << m_best_score << " " << (m_best_expr?"no update":"") << "\n";); + if (!m_best_expr) + return false; + + apply_update(m_best_expr, m_best_value); + //verbose_stream() << "increasing move " << mk_bounded_pp(m_best_expr, m) + // << " := " << m_best_value << " score: " << m_top_score << "\n"; + return true; } ptr_vector const& bv_lookahead::get_candidate_uninterp() { auto const& lits = ctx.root_literals(); - unsigned start = ctx.rand(lits.size()); - for (unsigned i = 0; i < lits.size(); ++i) { - auto lit = lits[(i + start) % lits.size()]; - auto e = ctx.atom(lit.var()); - if (!e || !is_app(e)) - continue; - app* a = to_app(e); - if (!m_ev.can_eval1(a)) - continue; - if (m_ev.bval0(a) == m_ev.bval1(a)) - continue; - auto const& vars = m_ev.terms.uninterp_occurs(a); - VERIFY(!vars.empty()); - TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": "; - for (auto e : vars) tout << mk_bounded_pp(e, m) << " "; - tout << "\n";); - return vars; + app* e = nullptr; + if (m_config.ucb) { + double max = -1.0; + for (auto lit : ctx.root_literals()) { + if (!is_false_bv_literal(lit)) + continue; + auto a = to_app(ctx.atom(lit.var())); + auto score = old_score(a); + auto q = score + + m_config.ucb_constant * sqrt(log((double)m_touched) / get_touched(a)) + + m_config.ucb_noise * ctx.rand(512); + if (q > max) + max = q, e = a; + } + if (e) { + m_touched++; + inc_touched(e); + } } - return m_empty_vars; + else { + unsigned n = 0; + for (auto lit : ctx.root_literals()) + if (is_false_bv_literal(lit) && ctx.rand() % ++n == 0) + e = to_app(ctx.atom(lit.var())); + } + if (!e) + return m_empty_vars; + + auto const& vars = m_ev.terms.uninterp_occurs(e); + VERIFY(!vars.empty()); + TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": "; + for (auto e : vars) tout << mk_bounded_pp(e, m) << " "; + tout << "\n";); + return vars; } + bool bv_lookahead::apply_random_update(ptr_vector const& vars) { + expr* e = vars[ctx.rand(vars.size())]; + auto& v = wval(e); + m_v_updated.set_bw(v.bw); + v.get_variant(m_v_updated, m_ev.m_rand); + if (!v.can_set(m_v_updated)) + return false; + apply_update(e, m_v_updated); - bool bv_lookahead::apply_random_update(ptr_vector const& vars) { - while (true) { - expr* e = vars[ctx.rand(vars.size())]; - auto& v = wval(e); - m_v_updated.set_bw(v.bw); - v.get_variant(m_v_updated, m_ev.m_rand); - v.eval = m_v_updated; - if (!v.commit_eval()) - continue; - apply_update(e, m_v_updated); + //verbose_stream() << "random update " << mk_bounded_pp(e, m) << " := " << m_v_updated << " score " << m_top_score << "\n"; + return true; + } + + bool bv_lookahead::apply_random_move(ptr_vector const& vars) { + expr* e = vars[ctx.rand(vars.size())]; + auto& v = wval(e); + m_v_updated.set_bw(v.bw); + v.bits().copy_to(v.nw, m_v_updated); + switch (ctx.rand(3)) { + case 0: { + // flip a random bit + auto bit = ctx.rand(v.bw); + m_v_updated.set(bit, !m_v_updated.get(bit)); break; } + case 1: + v.add1(m_v_updated); + break; + default: + v.sub1(m_v_updated); + break; + } + + if (!v.can_set(m_v_updated)) + return false; + apply_update(e, m_v_updated); + TRACE("bv", tout << "random move " << mk_bounded_pp(e, m) << " := " << m_v_updated << "\n";); + // verbose_stream() << "random move " << mk_bounded_pp(e, m) << " := " << m_v_updated << " score " << m_top_score << "\n"; return true; } void bv_lookahead::check_restart() { - - if (m_stats.m_moves % m_config.restart_base == 0) - // ucb_forget(); + + if (m_stats.m_moves % m_config.restart_base == 0) { + ucb_forget(); rescore(); + } if (m_stats.m_moves < m_config.restart_next) return; - if (m_stats.m_restarts & 1) + ++m_stats.m_restarts; + + if (0x1 == (m_stats.m_restarts & 0x1)) m_config.restart_next += m_config.restart_base; else m_config.restart_next += (2 << (m_stats.m_restarts >> 1)) * m_config.restart_base; - m_stats.m_restarts++; - - // TODO: reset values of uninterpreted to 0 + reset_uninterp_in_false_literals(); + rescore(); } + void bv_lookahead::reset_uninterp_in_false_literals() { + auto const& lits = ctx.root_literals(); + expr_mark marked; + for (auto lit : ctx.root_literals()) { + if (!is_false_bv_literal(lit)) + continue; + app* a = to_app(ctx.atom(lit.var())); + auto const& occs = m_ev.terms.uninterp_occurs(a); + for (auto e : occs) { + if (marked.is_marked(e)) + continue; + marked.mark(e); + auto& v = wval(e); + m_v_updated.set_bw(v.bw); + m_v_updated.set_zero(); + if (v.can_set(m_v_updated)) { + apply_update(e, m_v_updated); + } + } + } + } + + bool bv_lookahead::is_bv_literal(sat::literal lit) { + if (!ctx.is_true(lit)) + return false; + auto e = ctx.atom(lit.var()); + if (!e || !is_app(e)) + return false; + app* a = to_app(e); + return m_ev.can_eval1(a); + } + + bool bv_lookahead::is_false_bv_literal(sat::literal lit) { + if (!is_bv_literal(lit)) + return false; + app* a = to_app(ctx.atom(lit.var())); + return (m_ev.bval0(a) != m_ev.bval1(a)); + } + + void bv_lookahead::updt_params(params_ref const& _p) { sls_params p(_p); - //m_config.max_restarts = p.max_restarts(); + m_config.walksat = p.walksat(); m_config.walksat_repick = p.walksat_repick(); m_config.paws_sp = p.paws_sp(); @@ -145,6 +235,12 @@ namespace sls { m_config.restart_next = m_config.restart_base; m_config.restart_init = p.restart_init(); m_config.early_prune = p.early_prune(); + m_config.ucb = p.walksat_ucb(); + + m_config.ucb_constant = p.walksat_ucb_constant(); + m_config.ucb_forget = p.walksat_ucb_forget(); + m_config.ucb_init = p.walksat_ucb_init(); + m_config.ucb_noise = p.walksat_ucb_noise(); } double bv_lookahead::new_score(app* a) { @@ -163,7 +259,9 @@ namespace sls { for (unsigned i = 0; i < vx.bw; ++i) if (vx.bits().get(i) != vy.bits().get(i)) ++delta; - return 1 - (delta / vx.bw); + auto d = 1.0 - (delta / (double)vx.bw); + //verbose_stream() << "hamming distance " << mk_bounded_pp(a, m) << " " << d << "\n"; + return d; } else if (bv.is_ule(a, x, y)) { auto const& vx = wval(x); @@ -229,12 +327,13 @@ namespace sls { return 0; } - double bv_lookahead::lookahead(expr* e, bvect const& new_value) { + double bv_lookahead::lookahead_update(expr* e, bvect const& new_value) { SASSERT(bv.is_bv(e)); SASSERT(is_uninterp(e)); SASSERT(m_restore.empty()); bool has_tabu = false; + double score = m_top_score; wval(e).eval = new_value; if (!insert_update(e)) { @@ -254,11 +353,14 @@ namespace sls { max_depth = std::max(max_depth, get_depth(p)); } } - else + else { + IF_VERBOSE(1, verbose_stream() << "tabu " << mk_bounded_pp(a, m) << "\n"); has_tabu = true; + } + } + else if (is_root(a)) { + score += get_weight(a) * (new_score(a) - old_score(a)); } - else if (is_root(a)) - rescore(a); else if (m.is_bool(a)) continue; else { @@ -275,17 +377,15 @@ namespace sls { if (has_tabu) return -10000; - if (m_top_score <= 0.000001) - return -10000; - return m_top_score; + return score; } void bv_lookahead::try_set(expr* u, bvect const& new_value) { if (!wval(u).can_set(new_value)) return; - auto score = lookahead(u, new_value); + auto score = lookahead_update(u, new_value); ++m_stats.m_num_updates; - verbose_stream() << mk_bounded_pp(u, m) << " " << new_value << " score: " << score << "\n"; + //verbose_stream() << mk_bounded_pp(u, m) << " := " << new_value << " score: " << score << "\n"; if (score > m_best_score) { m_best_score = score; m_best_expr = u; @@ -323,12 +423,6 @@ namespace sls { if (v.bw <= 1) return; - // invert - for (unsigned i = 0; i < v.nw; ++i) - m_v_updated[i] = ~m_v_updated[i]; - v.clear_overflow_bits(m_v_updated); - try_set(u, m_v_updated); - // increment m_v_saved.copy_to(v.nw, m_v_updated); v.add1(m_v_updated); @@ -339,16 +433,12 @@ namespace sls { v.sub1(m_v_updated); try_set(u, m_v_updated); - // reset to original value - try_set(u, m_v_saved); - } - - bool bv_lookahead::apply_update() { - CTRACE("bv", !m_best_expr, tout << "no update\n"); - if (!m_best_expr) - return false; - apply_update(m_best_expr, m_best_value); - return true; + // invert + m_v_saved.copy_to(v.nw, m_v_updated); + for (unsigned i = 0; i < v.nw; ++i) + m_v_updated[i] = ~m_v_updated[i]; + v.clear_overflow_bits(m_v_updated); + try_set(u, m_v_updated); } void bv_lookahead::apply_update(expr* e, bvect const& new_value) { @@ -357,6 +447,7 @@ namespace sls { SASSERT(is_uninterp(e)); SASSERT(m_restore.empty()); wval(e).eval = new_value; + double old_top_score = m_top_score; //verbose_stream() << mk_bounded_pp(e, m) << " := " << new_value << "\n"; @@ -370,6 +461,7 @@ namespace sls { m_ev.eval(e); // updates wval(e).eval if (!wval(e).commit_eval()) { TRACE("bv", tout << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); + IF_VERBOSE(0, verbose_stream() << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); // bv_plugin::is_sat picks up discrepancies continue; } @@ -379,7 +471,9 @@ namespace sls { } } else if (is_root(e)) { - rescore(e); + double score = new_score(e); + m_top_score += get_weight(e) * (score - old_score(e)); + set_score(e, score); } else if (m.is_bool(e)) continue; @@ -390,6 +484,8 @@ namespace sls { m_update_stack[depth].reset(); } m_in_update_stack.reset(); + TRACE("bv", tout << mk_bounded_pp(e, m) << " := " + << new_value << " " << m_top_score << " (" << old_top_score << ")\n"); } bool bv_lookahead::insert_update(expr* e) { @@ -427,77 +523,79 @@ namespace sls { return m_on_restore.is_marked(e); } - unsigned bv_lookahead::get_weight(expr* e) { - return m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0 }).weight; - } - - void bv_lookahead::inc_weight(expr* e) { - m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0 }).weight += 1; + bv_lookahead::bool_info& bv_lookahead::get_bool_info(expr* e) { + return m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0, 1}); } void bv_lookahead::dec_weight(expr* e) { - auto& w = m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0 }).weight; + auto& w = get_bool_info(e).weight; w = w > m_config.paws_init ? w - 1 : m_config.paws_init; } - void bv_lookahead::set_score(app* a, double d) { - m_bool_info.insert_if_not_there(a, { m_config.paws_init, 0 }).score = d; - } - - double bv_lookahead::old_score(app* a) { - return m_bool_info.insert_if_not_there(a, { m_config.paws_init, 0 }).score; - } - void bv_lookahead::rescore() { m_top_score = 0; - m_rescore = false; m_is_root.reset(); for (auto lit : ctx.root_literals()) { - auto e = ctx.atom(lit.var()); - if (!e || !is_app(e)) + if (!is_bv_literal(lit)) continue; - app* a = to_app(e); - if (!m_ev.can_eval1(a)) - continue; - + auto a = to_app(ctx.atom(lit.var())); double score = new_score(a); set_score(a, score); m_top_score += score; m_is_root.mark(a); } - verbose_stream() << "top score " << m_top_score << "\n"; - - } - - void bv_lookahead::rescore(app* e) { - double score = new_score(e); - m_top_score += get_weight(e) * (score - old_score(e)); - set_score(e, score); } void bv_lookahead::recalibrate_weights() { for (auto lit : ctx.root_literals()) { - auto e = ctx.atom(lit.var()); - if (!e || !is_app(e)) + if (!is_bv_literal(lit)) continue; - app* a = to_app(e); - if (!m_ev.can_eval1(a)) - continue; - bool is_true = ctx.is_true(lit); - bool is_true_a = m_ev.bval1(a); - if (ctx.rand(10) < m_config.paws_sp) { - if (is_true == is_true_a) + auto a = to_app(ctx.atom(lit.var())); + bool is_true0 = m_ev.bval0(a); + bool is_true1 = m_ev.bval1(a); + if (ctx.rand(2047) < m_config.paws_sp) { + if (is_true0 == is_true1) dec_weight(a); } - else if (is_true != is_true_a) + else if (is_true0 != is_true1) inc_weight(a); } - m_best_score = 0; + + IF_VERBOSE(20, display_weights(verbose_stream())); + } + + std::ostream& bv_lookahead::display_weights(std::ostream& out) { + + for (auto lit : ctx.root_literals()) { + if (!is_bv_literal(lit)) + continue; + auto a = to_app(ctx.atom(lit.var())); + out + << get_weight(a) << " " + << mk_bounded_pp(a, m) << " " + << old_score(a) << "\n"; + } + return out; + } + + void bv_lookahead::ucb_forget() { + if (m_config.ucb_forget >= 1.0) + return; + for (auto lit : ctx.root_literals()) { + if (!is_bv_literal(lit)) + continue; + auto a = to_app(ctx.atom(lit.var())); + auto touched_old = get_touched(a); + auto touched_new = static_cast((touched_old - 1) * m_config.ucb_forget + 1); + set_touched(a, touched_new); + m_touched += touched_new - touched_old; + } } void bv_lookahead::collect_statistics(statistics& st) const { st.update("sls-bv-lookahead", m_stats.m_num_lookahead); st.update("sls-bv-updates", m_stats.m_num_updates); st.update("sls-bv-moves", m_stats.m_moves); + st.update("sls-bv-restarts", m_stats.m_restarts); } } \ No newline at end of file diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h index 2b3aed8d4..bc34800e4 100644 --- a/src/ast/sls/sls_bv_lookahead.h +++ b/src/ast/sls/sls_bv_lookahead.h @@ -38,7 +38,13 @@ namespace sls { unsigned restart_init = 1000; bool early_prune = true; unsigned max_moves = 0; - unsigned max_moves_base = 200; + unsigned max_moves_base = 800; + unsigned propagation_base = 10000; + bool ucb = true; + double ucb_constant = 1.0; + double ucb_forget = 0.1; + bool ucb_init = false; + double ucb_noise = 0.1; }; struct stats { @@ -46,11 +52,13 @@ namespace sls { unsigned m_num_updates = 0; unsigned m_moves = 0; unsigned m_restarts = 0; + unsigned m_num_propagations = 0; }; struct bool_info { - unsigned weight = 0; + unsigned weight = 40; double score = 0; + unsigned touched = 1; }; bv_util bv; @@ -66,51 +74,61 @@ namespace sls { double m_best_score = 0, m_top_score = 0; bvect m_best_value; expr* m_best_expr = nullptr; - bool m_rescore = true; ptr_vector m_empty_vars; obj_map m_bool_info; expr_mark m_is_root; + unsigned m_touched = 1; - void init_updates(); + std::ostream& display_weights(std::ostream& out); bv_valuation& wval(expr* e) const; void insert_update_stack(expr* e); bool insert_update(expr* e); void restore_lookahead(); - double lookahead(expr* u, bvect const& new_value); - double old_score(app* c); + + bool_info& get_bool_info(expr* e); + double lookahead_update(expr* u, bvect const& new_value); + double old_score(app* c) { return get_bool_info(c).score; } + void set_score(app* c, double d) { get_bool_info(c).score = d; } double new_score(app* c); - void set_score(app* c, double d); - void rescore(app* c); void rescore(); - - unsigned get_weight(expr* e); - void inc_weight(expr* e); + unsigned get_weight(expr* e) { return get_bool_info(e).weight; } + void inc_weight(expr* e) { ++get_bool_info(e).weight; } void dec_weight(expr* e); void recalibrate_weights(); bool is_root(expr* e) { return m_is_root.is_marked(e); } + void ucb_forget(); + unsigned get_touched(app* e) { return get_bool_info(e).touched; } + void set_touched(app* e, unsigned t) { get_bool_info(e).touched = t; } + void inc_touched(app* e) { ++get_bool_info(e).touched; } + void try_set(expr* u, bvect const& new_value); void add_updates(expr* u); void apply_update(expr* e, bvect const& new_value); - bool apply_update(); + bool apply_random_move(ptr_vector const& vars); + bool apply_guided_move(ptr_vector const& vars); bool apply_random_update(ptr_vector const& vars); - bool apply_guided_update(ptr_vector const& vars); ptr_vector const& get_candidate_uninterp(); void check_restart(); + void reset_uninterp_in_false_literals(); + bool is_bv_literal(sat::literal lit); + bool is_false_bv_literal(sat::literal lit); + + void search(); + + public: bv_lookahead(bv_eval& ev); void updt_params(params_ref const& p); - lbool search(); - - void start_propagation() { m_rescore = true; } + void start_propagation(); bool on_restore(expr* e) const;