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

allow a plateau mode

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-14 16:38:12 -08:00
parent 076d3dbf13
commit 11909cfdff
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2707,7 +2707,8 @@ namespace sls {
m_best_score = score; m_best_score = score;
m_best_expr = e; m_best_expr = e;
m_best_value = new_value; m_best_value = new_value;
insert_tabu_set(e, num_t(1)); insert_tabu_set(e, new_value);
//verbose_stream() << "plateau " << mk_bounded_pp(e, m) << " := " << m_best_value << "\n";
} }
// revert back to old value // revert back to old value
@ -2717,13 +2718,13 @@ namespace sls {
template<typename num_t> template<typename num_t>
bool arith_base<num_t>::in_tabu_set(expr* e, num_t const& n) { 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()); uint64_t h = hash_u_u(e->get_id(), n.hash());
return (m_tabu_set & (1ull << (h & 64ull))) != 0; return (m_tabu_set & (1ull << (h & 63ull))) != 0;
} }
template<typename num_t> template<typename num_t>
void arith_base<num_t>::insert_tabu_set(expr* e, num_t const& n) { 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()); uint64_t h = hash_u_u(e->get_id(), n.hash());
m_tabu_set |= (1ull << (h & 64ull)); m_tabu_set |= (1ull << (h & 63ull));
} }
template<typename num_t> template<typename num_t>
@ -2900,6 +2901,7 @@ namespace sls {
m_best_value = m_vars[v].m_finite_domain[ctx.rand() % m_vars[v].m_finite_domain.size()]; m_best_value = m_vars[v].m_finite_domain[ctx.rand() % m_vars[v].m_finite_domain.size()];
else else
m_best_value = value(v) + delta; m_best_value = value(v) + delta;
m_tabu_set = 0;
break; break;
} }
case arith_move_type::hillclimb_plateau: case arith_move_type::hillclimb_plateau:
@ -2911,7 +2913,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); flet<bool> _allow_plateau(m_config.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);
@ -2935,6 +2937,7 @@ namespace sls {
else else
m_best_value = value(v) - 1; m_best_value = value(v) - 1;
} }
m_tabu_set = 0;
break; break;
} }
} }
@ -3181,6 +3184,7 @@ namespace sls {
//m_config.max_moves_base = p.max_moves_base(); //m_config.max_moves_base = p.max_moves_base();
//m_config.max_moves = p.max_moves(); //m_config.max_moves = p.max_moves();
m_config.arith_use_lookahead = p.arith_use_lookahead(); m_config.arith_use_lookahead = p.arith_use_lookahead();
m_config.allow_plateau = p.arith_allow_plateau();
m_config.config_initialized = true; m_config.config_initialized = true;
} }

1
src/params/sls_params.pyg
View file

@ -26,6 +26,7 @@ def_module_params('sls',
('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'), ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
('random_seed', UINT, 0, 'random seed'), ('random_seed', UINT, 0, 'random seed'),
('arith_use_lookahead', BOOL, False, 'use lookahead solver for NIRA'), ('arith_use_lookahead', BOOL, False, 'use lookahead solver for NIRA'),
('arith_allow_plateau', BOOL, False, 'allow plateau moves during NIRA solving'),
('bv_use_top_level_assertions', BOOL, True, 'use top-level assertions for BV lookahead solver'), ('bv_use_top_level_assertions', BOOL, True, 'use top-level assertions for BV lookahead solver'),
('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'), ('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'),
('bv_allow_rotation', BOOL, True, 'allow model rotation when repairing literal assignment'), ('bv_allow_rotation', BOOL, True, 'allow model rotation when repairing literal assignment'),