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

skip update stack items that are not Bool/bv

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-28 15:02:33 -08:00
parent 632e2b56e4
commit 2ebc647079
1 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -516,14 +516,15 @@ namespace sls {
void bv_lookahead::populate_update_stack(expr* t) { void bv_lookahead::populate_update_stack(expr* t) {
SASSERT(m_bv_restore.empty()); SASSERT(m_bv_restore.empty());
insert_update_stack(t); if (!insert_update_stack(t))
return;
m_min_depth = m_max_depth = get_depth(t); m_min_depth = m_max_depth = get_depth(t);
for (unsigned depth = m_max_depth; depth <= m_max_depth; ++depth) { for (unsigned depth = m_max_depth; depth <= m_max_depth; ++depth) {
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) { for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
auto [a, is_bv] = m_update_stack[depth][i]; auto [a, is_bv] = m_update_stack[depth][i];
for (auto p : ctx.parents(a)) { for (auto p : ctx.parents(a)) {
insert_update_stack(p); if (insert_update_stack(p))
m_max_depth = std::max(m_max_depth, get_depth(p)); m_max_depth = std::max(m_max_depth, get_depth(p));
} }
if (is_bv) { if (is_bv) {
wval(a).save_value(); wval(a).save_value();
@ -581,7 +582,7 @@ namespace sls {
try_flip(u); try_flip(u);
clear_update_stack(); clear_update_stack();
return; return;
} }
SASSERT(bv.is_bv(u)); SASSERT(bv.is_bv(u));
auto& v = wval(u); auto& v = wval(u);
while (m_v_saved.size() < v.bits().size()) { while (m_v_saved.size() < v.bits().size()) {
@ -669,7 +670,7 @@ namespace sls {
} }
} }
insert_update_stack(t); VERIFY(insert_update_stack(t));
unsigned max_depth = get_depth(t); unsigned max_depth = get_depth(t);
unsigned restore_point = m_ev.bool_value_restore_point(); unsigned restore_point = m_ev.bool_value_restore_point();
for (unsigned depth = max_depth; depth <= max_depth; ++depth) { for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
@ -719,8 +720,8 @@ namespace sls {
} }
for (auto p : ctx.parents(e)) { for (auto p : ctx.parents(e)) {
insert_update_stack(p); if (insert_update_stack(p))
max_depth = std::max(max_depth, get_depth(p)); max_depth = std::max(max_depth, get_depth(p));
} }
if (is_root(e)) { if (is_root(e)) {
@ -764,15 +765,16 @@ namespace sls {
} }
} }
void bv_lookahead::insert_update_stack(expr* e) { bool bv_lookahead::insert_update_stack(expr* e) {
if (!bv.is_bv(e) && !m.is_bool(e)) if (!bv.is_bv(e) && !m.is_bool(e))
return; return false;
unsigned depth = get_depth(e); unsigned depth = get_depth(e);
m_update_stack.reserve(depth + 1); m_update_stack.reserve(depth + 1);
if (!m_in_update_stack.is_marked(e) && is_app(e)) { if (!m_in_update_stack.is_marked(e) && is_app(e)) {
m_in_update_stack.mark(e); m_in_update_stack.mark(e);
m_update_stack[depth].push_back({ to_app(e), bv.is_bv(e) }); m_update_stack[depth].push_back({ to_app(e), bv.is_bv(e) });
} }
return true;
} }
sls::bv_valuation& bv_lookahead::wval(expr* e) const { sls::bv_valuation& bv_lookahead::wval(expr* e) const {