mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 04:28:17 +00:00
align updated version of lookahead with legacy heuristics
This commit is contained in:
Nikolaj Bjorner
parent
6ea68310c9
commit
d81de1a67e
|
|
@ -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<unsigned>(-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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<unsigned>((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);
|
||||
}
|
||||
}
|
||||
|
|
@ -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<expr> m_empty_vars;
|
||||
obj_map<expr, bool_info> 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<expr> const& vars);
|
||||
bool apply_guided_move(ptr_vector<expr> const& vars);
|
||||
bool apply_random_update(ptr_vector<expr> const& vars);
|
||||
bool apply_guided_update(ptr_vector<expr> const& vars);
|
||||
ptr_vector<expr> 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;
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue