mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

Disable asserts

Browse source
This commit is contained in:
Jakob Rath 2022-11-30 11:48:39 +01:00
parent 032e7e0337
commit ceddb97bfd
1 changed files with 10 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/util/dlist.h
View file

@ -21,6 +21,8 @@ Revision History:
#include "util/debug.h" #include "util/debug.h"
#include "util/util.h" #include "util/util.h"
#define DLIST_EXTRA_ASSERTIONS 0
template <typename T> class dll_iterator; template <typename T> class dll_iterator;
template <typename T> template <typename T>
@ -58,7 +60,7 @@ public:
} }
void insert_after(T* other) { void insert_after(T* other) {
#ifndef NDEBUG #if DLIST_EXTRA_ASSERTIONS
SASSERT(other); SASSERT(other);
SASSERT(invariant()); SASSERT(invariant());
SASSERT(other->invariant()); SASSERT(other->invariant());
@ -74,7 +76,7 @@ public:
other->m_prev = static_cast<T*>(this); other->m_prev = static_cast<T*>(this);
other_end->m_next = next; other_end->m_next = next;
next->m_prev = other_end; next->m_prev = other_end;
#ifndef NDEBUG #if DLIST_EXTRA_ASSERTIONS
SASSERT(invariant()); SASSERT(invariant());
SASSERT(other->invariant()); SASSERT(other->invariant());
size_t const new_sz = count_if(*static_cast<T*>(this), [](T const&) { return true; }); size_t const new_sz = count_if(*static_cast<T*>(this), [](T const&) { return true; });
@ -83,7 +85,7 @@ public:
} }
void insert_before(T* other) { void insert_before(T* other) {
#ifndef NDEBUG #if DLIST_EXTRA_ASSERTIONS
SASSERT(other); SASSERT(other);
SASSERT(invariant()); SASSERT(invariant());
SASSERT(other->invariant()); SASSERT(other->invariant());
@ -99,7 +101,7 @@ public:
other->m_prev = prev; other->m_prev = prev;
other_end->m_next = static_cast<T*>(this); other_end->m_next = static_cast<T*>(this);
this->m_prev = other_end; this->m_prev = other_end;
#ifndef NDEBUG #if DLIST_EXTRA_ASSERTIONS
SASSERT(invariant()); SASSERT(invariant());
SASSERT(other->invariant()); SASSERT(other->invariant());
size_t const new_sz = count_if(*static_cast<T*>(this), [](T const&) { return true; }); size_t const new_sz = count_if(*static_cast<T*>(this), [](T const&) { return true; });
@ -108,10 +110,12 @@ public:
} }
static void remove_from(T*& list, T* elem) { static void remove_from(T*& list, T* elem) {
#if DLIST_EXTRA_ASSERTIONS
SASSERT(list); SASSERT(list);
SASSERT(elem); SASSERT(elem);
SASSERT(list->invariant()); SASSERT(list->invariant());
SASSERT(elem->invariant()); SASSERT(elem->invariant());
#endif
if (list->m_next == list) { if (list->m_next == list) {
SASSERT(elem == list); SASSERT(elem == list);
list = nullptr; list = nullptr;
@ -123,7 +127,9 @@ public:
auto* prev = elem->m_prev; auto* prev = elem->m_prev;
prev->m_next = next; prev->m_next = next;
next->m_prev = prev; next->m_prev = prev;
#if DLIST_EXTRA_ASSERTIONS
SASSERT(list->invariant()); SASSERT(list->invariant());
#endif
} }
static void push_to_front(T*& list, T* elem) { static void push_to_front(T*& list, T* elem) {