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

fix regression in top-sort fix #6060

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-14 09:49:25 -07:00
parent 637120ced5
commit 55421afd61
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/util/top_sort.h
View file

@ -87,8 +87,10 @@ class top_sort {
public: public:
virtual ~top_sort() { virtual ~top_sort() {
for (auto * t : m_dep_keys) for (auto * t : m_dep_keys) {
dealloc(get_dep(t)); dealloc(get_dep(t));
m_deps[t->get_small_id()] = nullptr;
}
} }
void topological_sort() { void topological_sort() {
@ -102,9 +104,12 @@ public:
m_dfs_num.reset(); m_dfs_num.reset();
} }
void insert(T* t, T_set* s) { void insert(T* t, T_set* s) {
if (contains_dep(t))
dealloc(get_dep(t));
else
m_dep_keys.push_back(t);
m_deps.setx(t->get_small_id(), add_tag(s), nullptr); m_deps.setx(t->get_small_id(), add_tag(s), nullptr);
m_dep_keys.push_back(t);
} }
ptr_vector<T> const& deps() { return m_dep_keys; } ptr_vector<T> const& deps() { return m_dep_keys; }
@ -126,7 +131,7 @@ public:
bool contains_dep(T* t) const { return m_deps.get(t->get_small_id(), nullptr) != nullptr; } bool contains_dep(T* t) const { return m_deps.get(t->get_small_id(), nullptr) != nullptr; }
T_set* get_dep(T* t) const { return del_tag(m_deps.get(t->get_small_id(), nullptr)); } T_set* get_dep(T* t) const { return del_tag(m_deps.get(t->get_small_id(), nullptr)); }
bool is_singleton_partition(T* f) const { bool is_singleton_partition(T* f) const {