From f41134d1b6f7462df23eb572addcc4cd46e2bd7b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 Dec 2024 17:40:15 -0800 Subject: [PATCH] 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; }