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

new invariant for dlist: should be circular. avoid infinite loop

Browse source
This commit is contained in:
Chuyue Sun 2024-07-18 01:41:56 +00:00
parent aa7314ecb6
commit 62df40f0a6
1 changed files with 20 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/util/dlist.h
View file

@ -155,15 +155,25 @@ public:
elem->init(elem); elem->init(elem);
} }
bool invariant() const { bool invariant() const {
auto* e = this; auto* e = this;
do { const T* slow = static_cast<const T*>(this);
if (e->m_next->m_prev != e) const T* fast = m_next;
return false; bool looped = false;
e = e->m_next; // m_next of each node should point back to m_prev of the following node,
} // and m_prev of each node should point forward to m_next of the preceding node.
while (e != this); while (slow != fast) {
return true; if (fast->m_prev->m_next != fast || fast->m_next->m_prev != fast) {
return false;
}
fast = fast->m_next;
looped = looped || (fast == static_cast<const T*>(this));
if (!looped && fast == m_next) {
// We should be able to traverse back to the starting node.
return false;
}
}
return true;
} }
static bool contains(T const* list, T const* elem) { static bool contains(T const* list, T const* elem) {
@ -245,4 +255,4 @@ template < typename T
dll_iterator<T> end(T const& list) dll_iterator<T> end(T const& list)
{ {
return dll_iterator<T>::mk_end(&list); return dll_iterator<T>::mk_end(&list);
} }