mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-02 02:48:47 +00:00
Code Activity

track active entries

Browse source
This commit is contained in:
Jakob Rath 2023-11-06 11:06:13 +01:00
parent 8e94608485
commit 5eb5313ac6
2 changed files with 11 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/viable.cpp
View file

@ -112,6 +112,8 @@ namespace polysat {
auto const& [v, k, e] = m_trail.back(); auto const& [v, k, e] = m_trail.back();
// display_one(verbose_stream() << "Pop entry: ", v, e) << "\n"; // display_one(verbose_stream() << "Pop entry: ", v, e) << "\n";
SASSERT(well_formed(m_units[v])); SASSERT(well_formed(m_units[v]));
SASSERT(e->active);
e->active = false;
switch (k) { switch (k) {
case entry_kind::unit_e: case entry_kind::unit_e:
entry::remove_from(m_units[v].get_layer(e)->entries, e); entry::remove_from(m_units[v].get_layer(e)->entries, e);
@ -138,6 +140,8 @@ namespace polysat {
SASSERT(e->prev() != e || !entries); SASSERT(e->prev() != e || !entries);
SASSERT(e->prev() != e || e->next() == e); SASSERT(e->prev() != e || e->next() == e);
SASSERT(k == entry_kind::unit_e); SASSERT(k == entry_kind::unit_e);
SASSERT(!e->active);
e->active = true;
(void)k; (void)k;
SASSERT(well_formed(m_units[v])); SASSERT(well_formed(m_units[v]));
if (e->prev() != e) { if (e->prev() != e) {
@ -313,6 +317,7 @@ namespace polysat {
m_trail.push_back({ v, entry_kind::unit_e, e }); m_trail.push_back({ v, entry_kind::unit_e, e });
s.m_trail.push_back(trail_instr_t::viable_rem_i); s.m_trail.push_back(trail_instr_t::viable_rem_i);
e->remove_from(entries, e); e->remove_from(entries, e);
e->active = false;
}; };
if (ne->interval.is_full()) { if (ne->interval.is_full()) {
@ -1751,6 +1756,9 @@ namespace polysat {
return true; return true;
entry* first = e; entry* first = e;
while (true) { while (true) {
if (!e->active)
return false;
if (e->interval.is_full()) if (e->interval.is_full())
return e->next() == e; return e->next() == e;
if (e->interval.is_currently_empty()) if (e->interval.is_currently_empty())

3
src/math/polysat/viable.h
View file

@ -52,11 +52,14 @@ namespace polysat {
struct entry final : public dll_base<entry>, public fi_record { struct entry final : public dll_base<entry>, public fi_record {
/// whether the entry has been created by refinement (from constraints in 'fi_record::src') /// whether the entry has been created by refinement (from constraints in 'fi_record::src')
bool refined = false; bool refined = false;
/// whether the entry is part of the current set of intervals, or stashed away for backtracking
bool active = true;
void reset() { void reset() {
// dll_base<entry>::init(this); // we never did this in alloc_entry either // dll_base<entry>::init(this); // we never did this in alloc_entry either
fi_record::reset(); fi_record::reset();
refined = false; refined = false;
active = true;
} }
}; };