From 99b2e481c2ef8b899cdbc30fee776983d04333c8 Mon Sep 17 00:00:00 2001 From: Chuyue Sun Date: Fri, 19 Jul 2024 09:14:05 +0000 Subject: [PATCH 1/3] new heap invariants --- src/util/heap.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/util/heap.h b/src/util/heap.h index c080c6ebde9..3bee2fe9f67 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(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(m_values.size())) { SASSERT(m_value2indices[m_values[idx]] == idx); SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)])); From dfac2b785762d76303591aee4592fb9b33ff2588 Mon Sep 17 00:00:00 2001 From: Chuyue Sun Date: Fri, 19 Jul 2024 12:15:21 +0000 Subject: [PATCH 2/3] change ENSURE to SASSERT for unit test heap --- src/test/heap.cpp | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/src/test/heap.cpp b/src/test/heap.cpp index 6a5bc7b9ffe..5a504862c18 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)); + SASSERT(!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)); + SASSERT(t.contains(val)); } } - ENSURE(h.check_invariant()); + SASSERT(h.check_invariant()); for (int v : t) { - ENSURE(h.contains(v)); + SASSERT(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); + SASSERT(m1 == m2); + SASSERT(-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 { SASSERT(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; typedef heap 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)); + SASSERT(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)); + SASSERT(!h.contains(val)); } } else if (cmd <= 8) { @@ -128,10 +128,12 @@ static void tst2() { } } else { - ENSURE(h.check_invariant()); + SASSERT(h.check_invariant()); } } - ENSURE(h.check_invariant()); + SASSERT(h.check_invariant()); + h.reset(); + SASSERT(h.check_invariant()); } void tst_heap() { From 751ef0561bf55126aaff1158c40fb109279a3b93 Mon Sep 17 00:00:00 2001 From: Chuyue Sun Date: Fri, 19 Jul 2024 16:59:40 +0000 Subject: [PATCH 3/3] change SASSERT to VERIFY --- src/test/heap.cpp | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/test/heap.cpp b/src/test/heap.cpp index 5a504862c18..f30f45c32cc 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)) { - SASSERT(!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"; } - SASSERT(t.contains(val)); + VERIFY(t.contains(val)); } } - SASSERT(h.check_invariant()); + VERIFY(h.check_invariant()); for (int v : t) { - SASSERT(h.contains(v)); + VERIFY(h.contains(v)); } while (!h.empty()) { int m1 = h.min_value(); int m2 = h.erase_min(); (void)m1; (void)m2; - SASSERT(m1 == m2); - SASSERT(-1 < m2); + VERIFY(m1 == m2); + VERIFY(-1 < m2); } } int g_value[N]; -struct lt_proc2 { bool operator()(int v1, int v2) const { SASSERT(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 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);); - SASSERT(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);); - SASSERT(!h.contains(val)); + VERIFY(!h.contains(val)); } } else if (cmd <= 8) { @@ -128,12 +128,12 @@ static void tst2() { } } else { - SASSERT(h.check_invariant()); + VERIFY(h.check_invariant()); } } - SASSERT(h.check_invariant()); + VERIFY(h.check_invariant()); h.reset(); - SASSERT(h.check_invariant()); + VERIFY(h.check_invariant()); } void tst_heap() {