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

remove m_level attribute, use s->get_scope_level directly

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-08 19:56:57 -07:00
parent 6bd46b0922
commit da614c65e5
1 changed files with 8 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/solver/slice_solver.cpp
View file

@ -40,7 +40,6 @@ class slice_solver : public solver {
ptr_vector<func_decl> m_used_funs_trail; ptr_vector<func_decl> m_used_funs_trail;
unsigned_vector m_used_funs_lim; unsigned_vector m_used_funs_lim;
bool m_has_query = false; bool m_has_query = false;
unsigned m_level = 0;
ast_mark m_mark; ast_mark m_mark;
@ -210,18 +209,17 @@ class slice_solver : public solver {
return; return;
unsigned idx = m_new_idx[0]; unsigned idx = m_new_idx[0];
auto const& f0 = m_assertions[idx]; auto const& f0 = m_assertions[idx];
if (f0.level < m_level) { if (f0.level < s->get_scope_level()) {
// pop to f.level // pop to f.level
// add m_new_idx within f.level // add m_new_idx within f.level
// replay push and assertions above f.level // replay push and assertions above f.level
s->pop(m_level - f0.level); s->pop(s->get_scope_level() - f0.level);
m_level = f0.level;
unsigned last_idx = idx; unsigned last_idx = idx;
for (unsigned idx : m_new_idx) { for (unsigned idx : m_new_idx) {
// add only new assertions within lowest scope level. // add only new assertions within lowest scope level.
auto const& f = m_assertions[idx]; auto const& f = m_assertions[idx];
if (m_level != f.level) if (s->get_scope_level() != f.level)
break; break;
last_idx = idx; last_idx = idx;
assert_expr(f); assert_expr(f);
@ -231,10 +229,9 @@ class slice_solver : public solver {
auto const& f = m_assertions[i]; auto const& f = m_assertions[i];
if (f0.level == f.level) if (f0.level == f.level)
continue; continue;
while (f.level > m_level) { while (f.level > s->get_scope_level())
s->push(); s->push();
++m_level;
}
if (f.active) if (f.active)
assert_expr(f); assert_expr(f);
} }
@ -242,10 +239,8 @@ class slice_solver : public solver {
else { else {
for (unsigned idx : m_new_idx) { for (unsigned idx : m_new_idx) {
auto const& f = m_assertions[idx]; auto const& f = m_assertions[idx];
while (f.level > m_level) { while (f.level > s->get_scope_level())
s->push(); s->push();
++m_level;
}
assert_expr(f); assert_expr(f);
} }
} }
@ -294,10 +289,8 @@ public:
unsigned old_sz = m_assertions_lim[m_assertions_lim.size() - n]; unsigned old_sz = m_assertions_lim[m_assertions_lim.size() - n];
for (unsigned i = m_assertions.size(); i-- > old_sz; ) { for (unsigned i = m_assertions.size(); i-- > old_sz; ) {
auto const& f = m_assertions[i]; auto const& f = m_assertions[i];
if (f.level < m_level) { if (f.level < s->get_scope_level())
s->pop(m_level - f.level); s->pop(s->get_scope_level() - f.level);
m_level = f.level;
}
} }
m_assertions_lim.shrink(m_assertions_lim.size() - n); m_assertions_lim.shrink(m_assertions_lim.size() - n);
m_assertions.shrink(old_sz); m_assertions.shrink(old_sz);