mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

have apply-update check can_set instead of caller

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-30 08:56:09 -08:00
parent bcf66f214f
commit d8741b4aec
2 changed files with 9 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -92,11 +92,7 @@ namespace sls {
for (unsigned i = 0; i < sz; ++i) for (unsigned i = 0; i < sz; ++i)
add_updates(vars[(start + i) % sz]); add_updates(vars[(start + i) % sz]);
CTRACE("bv", !m_best_expr, tout << "no guided move\n";); CTRACE("bv", !m_best_expr, tout << "no guided move\n";);
if (!m_best_expr) return apply_update(m_best_expr, m_best_value, "increasing move");
return false;
apply_update(m_best_expr, m_best_value, "increasing move");
return true;
} }
/** /**
@ -107,10 +103,7 @@ namespace sls {
auto& v = wval(e); auto& v = wval(e);
m_v_updated.set_bw(v.bw); m_v_updated.set_bw(v.bw);
v.get_variant(m_v_updated, m_ev.m_rand); v.get_variant(m_v_updated, m_ev.m_rand);
if (!v.can_set(m_v_updated)) return apply_update(e, m_v_updated, "random update");
return false;
apply_update(e, m_v_updated, "random update");
return true;
} }
/** /**
@ -135,11 +128,7 @@ namespace sls {
v.sub1(m_v_updated); v.sub1(m_v_updated);
break; break;
} }
return apply_update(e, m_v_updated, "random move");
if (!v.can_set(m_v_updated))
return false;
apply_update(e, m_v_updated, "random move");
return true;
} }
/** /**
@ -223,9 +212,7 @@ namespace sls {
auto& v = wval(e); auto& v = wval(e);
m_v_updated.set_bw(v.bw); m_v_updated.set_bw(v.bw);
m_v_updated.set_zero(); m_v_updated.set_zero();
if (v.can_set(m_v_updated)) { apply_update(e, m_v_updated, "reset");
apply_update(e, m_v_updated, "reset");
}
} }
} }
} }
@ -477,10 +464,12 @@ namespace sls {
* The update is committed. * The update is committed.
*/ */
void bv_lookahead::apply_update(expr* e, bvect const& new_value, char const* reason) { bool bv_lookahead::apply_update(expr* e, bvect const& new_value, char const* reason) {
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));
SASSERT(is_uninterp(e)); SASSERT(is_uninterp(e));
SASSERT(m_restore.empty()); SASSERT(m_restore.empty());
if (!e || !wval(e).can_set(new_value))
return false;
wval(e).eval = new_value; wval(e).eval = new_value;
double old_top_score = m_top_score; double old_top_score = m_top_score;
@ -520,6 +509,7 @@ namespace sls {
TRACE("bv", tout << reason << " " << mk_bounded_pp(m_best_expr, m) TRACE("bv", tout << reason << " " << mk_bounded_pp(m_best_expr, m)
<< " := " << new_value << " := " << new_value
<< " score " << m_top_score << "\n";); << " score " << m_top_score << "\n";);
return true;
} }
bool bv_lookahead::insert_update(expr* e) { bool bv_lookahead::insert_update(expr* e) {

2
src/ast/sls/sls_bv_lookahead.h
View file

@ -108,7 +108,7 @@ namespace sls {
void try_set(expr* u, bvect const& new_value); void try_set(expr* u, bvect const& new_value);
void add_updates(expr* u); void add_updates(expr* u);
void apply_update(expr* e, bvect const& new_value, char const* reason); bool apply_update(expr* e, bvect const& new_value, char const* reason);
bool apply_random_move(ptr_vector<expr> const& vars); bool apply_random_move(ptr_vector<expr> const& vars);
bool apply_guided_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_random_update(ptr_vector<expr> const& vars);