From f38527124b9300221e5d0d4fbb9f61aec46dc952 Mon Sep 17 00:00:00 2001 From: Chuyue Sun Date: Thu, 18 Jul 2024 22:55:06 +0000 Subject: [PATCH] new hashtable invariants --- src/util/hashtable.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/util/hashtable.h b/src/util/hashtable.h index b59a2e7d8..f550ee917 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -639,6 +639,19 @@ public: #ifdef Z3DEBUG bool check_invariant() { + // The capacity must always be a power of two. + if (!is_power_of_two(m_capacity)) + return false; + + // The number of deleted plus the size must not exceed the capacity. + if (m_num_deleted + m_size > m_capacity) + return false; + + // Checking that m_num_deleted is less than or equal to m_size. + if (m_num_deleted > m_size) { + return false; + } + entry * curr = m_table; entry * end = m_table + m_capacity; unsigned num_deleted = 0;