mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add plateau option

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-14 13:54:20 -08:00
parent 648cf9602e
commit 8515cebd19
2 changed files with 32 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/ast/sls/sls_arith_base.cpp
View file

@ -2698,24 +2698,49 @@ namespace sls {
auto score = lookahead(e, false); auto score = lookahead(e, false);
TRACE("arith_verbose", tout << "lookahead " << v << " " << mk_bounded_pp(e, m) << " := " << delta + old_value << " " << score << " (" << m_best_score << ")\n";); TRACE("arith_verbose", tout << "lookahead " << v << " " << mk_bounded_pp(e, m) << " := " << delta + old_value << " " << score << " (" << m_best_score << ")\n";);
if (score > m_best_score) { if (score > m_best_score) {
m_tabu_set = 0;
m_best_score = score; m_best_score = score;
m_best_value = new_value; m_best_value = new_value;
m_best_expr = e; m_best_expr = e;
} }
else if (m_config.allow_plateau && score == m_best_score && !in_tabu_set(e, new_value)) {
m_best_score = score;
m_best_expr = e;
m_best_value = new_value;
insert_tabu_set(e, num_t(1));
}
// revert back to old value // revert back to old value
update_args_value(v, old_value); update_args_value(v, old_value);
} }
template<typename num_t>
bool arith_base<num_t>::in_tabu_set(expr* e, num_t const& n) {
uint64_t h = hash_u_u(e->get_id(), n.hash());
return (m_tabu_set & (1ull << (h & 64ull))) != 0;
}
template<typename num_t>
void arith_base<num_t>::insert_tabu_set(expr* e, num_t const& n) {
uint64_t h = hash_u_u(e->get_id(), n.hash());
m_tabu_set |= (1ull << (h & 64ull));
}
template<typename num_t> template<typename num_t>
void arith_base<num_t>::lookahead_bool(expr* e) { void arith_base<num_t>::lookahead_bool(expr* e) {
bool b = get_bool_value(e); bool b = get_bool_value(e);
set_bool_value(e, !b); set_bool_value(e, !b);
auto score = lookahead(e, false); auto score = lookahead(e, false);
if (score > m_best_score) { if (score > m_best_score) {
m_tabu_set = 0;
m_best_score = score; m_best_score = score;
m_best_expr = e; m_best_expr = e;
} }
else if (m_config.allow_plateau && score == m_best_score && !in_tabu_set(e, num_t(1))) {
m_best_score = score;
m_best_expr = e;
insert_tabu_set(e, num_t(1));
}
set_bool_value(e, b); set_bool_value(e, b);
lookahead(e, false); lookahead(e, false);
} }
@ -2877,6 +2902,7 @@ namespace sls {
m_best_value = value(v) + delta; m_best_value = value(v) + delta;
break; break;
} }
case arith_move_type::hillclimb_plateau:
case arith_move_type::hillclimb: { case arith_move_type::hillclimb: {
for (unsigned i = 0; i < sz; ++i) for (unsigned i = 0; i < sz; ++i)
add_lookahead(info, vars[(start + i) % sz]); add_lookahead(info, vars[(start + i) % sz]);
@ -2885,6 +2911,7 @@ namespace sls {
std::stable_sort(m_updates.begin(), m_updates.end(), [](auto const& a, auto const& b) { return a.m_var < b.m_var || (a.m_var == b.m_var && a.m_delta < b.m_delta); }); std::stable_sort(m_updates.begin(), m_updates.end(), [](auto const& a, auto const& b) { return a.m_var < b.m_var || (a.m_var == b.m_var && a.m_delta < b.m_delta); });
m_last_expr = nullptr; m_last_expr = nullptr;
sz = m_updates.size(); sz = m_updates.size();
flet<bool> _allow_plateau(m_config.allow_plateau, t == arith_move_type::hillclimb_plateau);
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
auto const& [v, delta, score] = m_updates[(start + i) % m_updates.size()]; auto const& [v, delta, score] = m_updates[(start + i) % m_updates.size()];
lookahead_num(v, delta); lookahead_num(v, delta);

5
src/ast/sls/sls_arith_base.h
View file

@ -29,6 +29,7 @@ namespace sls {
enum arith_move_type { enum arith_move_type {
hillclimb, hillclimb,
hillclimb_plateau,
random_update, random_update,
random_inc_dec random_inc_dec
}; };
@ -66,6 +67,7 @@ namespace sls {
unsigned restart_next = 1000; unsigned restart_next = 1000;
unsigned restart_init = 1000; unsigned restart_init = 1000;
bool arith_use_lookahead = false; bool arith_use_lookahead = false;
bool allow_plateau = false;
}; };
struct stats { struct stats {
@ -331,7 +333,10 @@ namespace sls {
expr_mark m_is_root; expr_mark m_is_root;
unsigned m_touched = 1; unsigned m_touched = 1;
sat::bool_var_set m_fixed_atoms; sat::bool_var_set m_fixed_atoms;
uint64_t m_tabu_set = 0;
bool in_tabu_set(expr* e, num_t const& n);
void insert_tabu_set(expr* e, num_t const& n);
bool_info& get_bool_info(expr* e); bool_info& get_bool_info(expr* e);
bool get_bool_value(expr* e); bool get_bool_value(expr* e);
bool get_bool_value_rec(expr* e); bool get_bool_value_rec(expr* e);