mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

Revert "New invariant for dlist (#7294)" (#7301)

Browse source 
This reverts commit cf4d0e74a5.
This commit is contained in:
Nikolaj Bjorner 2024-07-19 19:11:54 -07:00 committed by GitHub
parent 80ac7b3438
commit 5003d41cdb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/util/dlist.h
View file

@ -155,23 +155,15 @@ public:
elem->init(elem); elem->init(elem);
} }
bool invariant() const { bool invariant() const {
auto* e = this; auto* e = this;
const T* slow = static_cast<const T*>(this); do {
const T* fast = m_next; if (e->m_next->m_prev != e)
bool looped = false; return false;
// m_next of each node should point back to m_prev of the following node, e = e->m_next;
// and m_prev of each node should point forward to m_next of the preceding node. }
while (slow != fast) { while (e != this);
if (fast->m_prev->m_next != fast || fast->m_next->m_prev != fast) return true;
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) {