From 80ac7b34387cddb88f2286b0716dd44ede982b78 Mon Sep 17 00:00:00 2001
From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com>
Date: Fri, 19 Jul 2024 14:03:21 -0700
Subject: [PATCH] new heap invariants (#7298)

* new heap invariants

* change ENSURE to SASSERT for unit test heap

* change SASSERT to VERIFY
---
 src/test/heap.cpp | 24 +++++++++++++-----------
 src/util/heap.h   | 13 +++++++++++++
 2 files changed, 26 insertions(+), 11 deletions(-)

diff --git a/src/test/heap.cpp b/src/test/heap.cpp
index 6a5bc7b9f..f30f45c32 100644
--- a/src/test/heap.cpp
+++ b/src/test/heap.cpp
@@ -38,7 +38,7 @@ 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);
         }
@@ -46,26 +46,26 @@ static void tst1() {
             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
index c080c6ebd..3bee2fe9f 100644
--- 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)]));