mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

fix random update to a legal one

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-12-27 13:01:47 -08:00
parent c82518ca36
commit 1f55ec5cef
1 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -70,11 +70,17 @@ namespace sls {
}
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);
apply_update(e, m_v_updated);
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);
break;
}
return true;
}
@ -221,6 +227,7 @@ namespace sls {
SASSERT(is_uninterp(e));
SASSERT(m_restore.empty());
wval(e).eval = new_value;
VERIFY(wval(e).commit_eval());
insert_update_stack(e);
unsigned max_depth = get_depth(e);