new heap invariants (#7298)

* new heap invariants * change ENSURE to SASSERT for unit test heap * change SASSERT to VERIFY
Z3Prover · Jul 19, 2024 · 80ac7b3 · 80ac7b3
1 parent bc636d7
commit 80ac7b3
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 11 deletions.
diff --git a/src/test/heap.cpp b/src/test/heap.cpp
@@ -38,34 +38,34 @@ static void tst1() {
     for (int i = 0; i < N * 3; i++) {
         int val = heap_rand() % N;
         if (!h.contains(val)) {
-            ENSURE(!t.contains(val));
+            VERIFY(!t.contains(val));
             h.insert(val);
             t.insert(val);
         }
         else {
             if (!t.contains(val)) {
                 for (int v : t) std::cout << v << "\n";
             }
-            ENSURE(t.contains(val));
+            VERIFY(t.contains(val));
         }
     }
-    ENSURE(h.check_invariant());
+    VERIFY(h.check_invariant());
     for (int v : t) {
-        ENSURE(h.contains(v));
+        VERIFY(h.contains(v));
     }
     while (!h.empty()) {
         int m1 = h.min_value();
         int m2 = h.erase_min();
         (void)m1;
         (void)m2;
-        ENSURE(m1 == m2);
-        ENSURE(-1 < m2);
+        VERIFY(m1 == m2);
+        VERIFY(-1 < m2);
     }
 }
 
 int g_value[N];
 
-struct lt_proc2 { bool operator()(int v1, int v2) const { ENSURE(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } };
+struct lt_proc2 { bool operator()(int v1, int v2) const { VERIFY(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } };
 typedef heap<lt_proc2> int_heap2;
 
 static void init_values() {
@@ -98,7 +98,7 @@ static void tst2() {
                 TRACE("heap", tout << "inserting: " << val << "\n";);
                 h.insert(val);
                 TRACE("heap", dump_heap(h, tout););
-                ENSURE(h.contains(val));
+                VERIFY(h.contains(val));
             }
         }
         else if (cmd <= 6) {
@@ -107,7 +107,7 @@ static void tst2() {
                 TRACE("heap", tout << "removing: " << val << "\n";);
                 h.erase(val);
                 TRACE("heap", dump_heap(h, tout););
-                ENSURE(!h.contains(val));
+                VERIFY(!h.contains(val));
             }
         }
         else if (cmd <= 8) {
@@ -128,10 +128,12 @@ static void tst2() {
             }
         }
         else {
-            ENSURE(h.check_invariant());
+            VERIFY(h.check_invariant());
         }
     }
-    ENSURE(h.check_invariant());
+    VERIFY(h.check_invariant());
+    h.reset();
+    VERIFY(h.check_invariant());
 }
 
 void tst_heap() {

diff --git a/src/util/heap.h b/src/util/heap.h
@@ -55,6 +55,19 @@ class heap : private LT {
     }
 
     bool check_invariant_core(int idx) const {
+
+        // Check that m_values starts with a dummy value at index 0.
+        if (m_values.empty() || m_values[0] != -1) {
+            return false;
+        }
+
+        // All indices in m_value2indices that are not used in m_values should be 0
+        for (int val = 0; val < static_cast<int>(m_value2indices.size()); ++val) {
+            if (std::find(m_values.begin(), m_values.end(), val) == m_values.end() && m_value2indices[val] != 0) {
+                return false; // Unused indices should have a 0 value
+            }
+        }
+
         if (idx < static_cast<int>(m_values.size())) {
             SASSERT(m_value2indices[m_values[idx]] == idx);
             SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)]));