Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Black box testing of cvc5::BinaryHeap.
11 : : */
12 : :
13 : : #include <iostream>
14 : : #include <sstream>
15 : :
16 : : #include "test.h"
17 : : #include "util/bin_heap.h"
18 : :
19 : : namespace cvc5::internal {
20 : : namespace test {
21 : :
22 : : class TestUtilBlackBinaryHeap : public TestInternal
23 : : {
24 : : protected:
25 : : struct Elem
26 : : {
27 : 42009 : Elem(int32_t y) : d_x(y) {}
28 : : int32_t d_x;
29 : : };
30 : :
31 : : struct Cmp
32 : : {
33 : : Cmp() : d_valid(false) {}
34 : 1 : Cmp(int32_t) : d_valid(true) {}
35 : :
36 : 369942 : bool operator()(Elem x, Elem y) const
37 : : {
38 : : // ensure BinaryHeap<> calls our Cmp instance and not some fresh one
39 [ - + ][ - + ]: 369942 : Assert(d_valid);
[ - - ]
40 : 369942 : return x.d_x > y.d_x;
41 : : }
42 : :
43 : : bool d_valid;
44 : : };
45 : : };
46 : :
47 : : /**
48 : : * Test a a series of simple heaps (push a few then pop all then do others).
49 : : * Done as a series to test if the heap structure falls into a bad state
50 : : * after prolonged use.
51 : : */
52 : 4 : TEST_F(TestUtilBlackBinaryHeap, heap_series)
53 : : {
54 : 1 : BinaryHeap<int32_t> heap;
55 : :
56 : : // First test a heap of 1 element
57 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 0u);
58 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.empty());
59 : : #ifdef CVC5_ASSERTIONS
60 : 1 : ASSERT_DEATH(heap.top(), "!empty\\(\\)");
61 : 1 : ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
62 : : #endif
63 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.begin() == heap.end());
64 : :
65 : 1 : BinaryHeap<int32_t>::handle h5 = heap.push(5);
66 [ - + ][ + - ]: 1 : ASSERT_TRUE(h5 == h5);
67 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), 5);
68 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 1u);
69 [ - + ][ + - ]: 1 : ASSERT_FALSE(heap.empty());
70 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.begin() != heap.end());
71 [ - + ][ + - ]: 1 : ASSERT_EQ(*h5, 5);
72 [ - + ][ + - ]: 1 : ASSERT_EQ(*heap.begin(), 5);
73 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(heap.erase(h5));
[ + - ][ - - ]
74 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.empty());
75 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 0u);
76 : : #ifdef CVC5_ASSERTIONS
77 : 1 : ASSERT_DEATH(heap.top(), "!empty\\(\\)");
78 : 1 : ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
79 : : #endif
80 : :
81 : : // Next test a heap of 4 elements
82 : 1 : h5 = heap.push(5);
83 : 1 : BinaryHeap<int32_t>::handle h3 = heap.push(3);
84 : 1 : BinaryHeap<int32_t>::handle h10 = heap.push(10);
85 : 1 : BinaryHeap<int32_t>::handle h2 = heap.push(2);
86 [ - + ][ + - ]: 1 : ASSERT_NE(h5, h3);
87 [ - + ][ + - ]: 1 : ASSERT_NE(h5, h10);
88 [ - + ][ + - ]: 1 : ASSERT_NE(h5, h2);
89 [ - + ][ + - ]: 1 : ASSERT_NE(h3, h10);
90 [ - + ][ + - ]: 1 : ASSERT_NE(h3, h2);
91 [ - + ][ + - ]: 1 : ASSERT_NE(h10, h2);
92 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.begin() != heap.end());
93 [ - + ][ + - ]: 1 : ASSERT_EQ(*heap.begin(), 10);
94 [ - + ][ + - ]: 1 : ASSERT_EQ(*h2, 2);
95 [ - + ][ + - ]: 1 : ASSERT_EQ(*h3, 3);
96 [ - + ][ + - ]: 1 : ASSERT_EQ(*h5, 5);
97 [ - + ][ + - ]: 1 : ASSERT_EQ(*h10, 10);
98 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), 10);
99 : : // test the iterator (note the order of elements isn't guaranteed!)
100 : 1 : BinaryHeap<int32_t>::const_iterator i = heap.begin();
101 [ - + ][ + - ]: 1 : ASSERT_TRUE(i != heap.end());
102 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(*i++);
[ + - ][ - - ]
103 [ - + ][ + - ]: 1 : ASSERT_TRUE(i != heap.end());
104 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(*i++);
[ + - ][ - - ]
105 [ - + ][ + - ]: 1 : ASSERT_TRUE(i != heap.end());
106 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(*i++);
[ + - ][ - - ]
107 [ - + ][ + - ]: 1 : ASSERT_TRUE(i != heap.end());
108 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(*i++);
[ + - ][ - - ]
109 [ - + ][ + - ]: 1 : ASSERT_TRUE(i == heap.end());
110 [ - + ][ + - ]: 1 : ASSERT_FALSE(heap.empty());
111 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 4u);
112 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(heap.pop());
[ + - ][ - - ]
113 [ - + ][ + - ]: 1 : ASSERT_TRUE(i != heap.end());
114 [ - + ][ + - ]: 1 : ASSERT_EQ(*heap.begin(), 5);
115 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), 5);
116 [ - + ][ + - ]: 1 : ASSERT_FALSE(heap.empty());
117 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 3u);
118 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(heap.pop());
[ + - ][ - - ]
119 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.begin() != heap.end());
120 [ - + ][ + - ]: 1 : ASSERT_EQ(*heap.begin(), 3);
121 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), 3);
122 [ - + ][ + - ]: 1 : ASSERT_FALSE(heap.empty());
123 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 2u);
124 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(heap.pop());
[ + - ][ - - ]
125 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.begin() != heap.end());
126 [ - + ][ + - ]: 1 : ASSERT_EQ(*heap.begin(), 2);
127 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), 2);
128 [ - + ][ + - ]: 1 : ASSERT_FALSE(heap.empty());
129 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 1u);
130 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(heap.pop());
[ + - ][ - - ]
131 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.begin() == heap.end());
132 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.empty());
133 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 0u);
134 : : #ifdef CVC5_ASSERTIONS
135 : 1 : ASSERT_DEATH(heap.top(), "!empty\\(\\)");
136 : 1 : ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
137 : : #endif
138 : :
139 : : // Now with a few updates
140 : 1 : h5 = heap.push(5);
141 : 1 : h3 = heap.push(3);
142 : 1 : h10 = heap.push(10);
143 : 1 : h2 = heap.push(2);
144 : :
145 [ - + ][ + - ]: 1 : ASSERT_EQ(*h5, 5);
146 [ - + ][ + - ]: 1 : ASSERT_EQ(*h3, 3);
147 [ - + ][ + - ]: 1 : ASSERT_EQ(*h10, 10);
148 [ - + ][ + - ]: 1 : ASSERT_EQ(*h2, 2);
149 : :
150 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), 10);
151 : 1 : heap.update(h10, -10);
152 [ - + ][ + - ]: 1 : ASSERT_EQ(*h10, -10);
153 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), 5);
154 : 1 : heap.erase(h2);
155 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), 5);
156 : 1 : heap.update(h3, -20);
157 [ - + ][ + - ]: 1 : ASSERT_EQ(*h3, -20);
158 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), 5);
159 : 1 : heap.pop();
160 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), -10);
161 : 1 : heap.pop();
162 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.top(), -20);
163 [ + - ]: 1 : }
164 : :
165 : 4 : TEST_F(TestUtilBlackBinaryHeap, large_heap)
166 : : {
167 : 1 : BinaryHeap<Elem, Cmp> heap(Cmp(0));
168 : 1 : std::vector<BinaryHeap<Elem, Cmp>::handle> handles;
169 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.empty());
170 [ + + ]: 1001 : for (int32_t x = 0; x < 1000; ++x)
171 : : {
172 : 1000 : handles.push_back(heap.push(Elem(x)));
173 : : }
174 [ - + ][ + - ]: 1 : ASSERT_FALSE(heap.empty());
175 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 1000u);
176 : 1 : heap.update(handles[100], 50);
177 : 1 : heap.update(handles[100], -50);
178 : 1 : heap.update(handles[600], 2);
179 : 1 : heap.update(handles[184], -9);
180 : 1 : heap.update(handles[987], 9555);
181 : 1 : heap.update(handles[672], -1003);
182 : 1 : heap.update(handles[781], 481);
183 : 1 : heap.update(handles[9], 9619);
184 : 1 : heap.update(handles[919], 111);
185 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 1000u);
186 : 1 : heap.erase(handles[10]);
187 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 999u);
188 [ - + ][ + - ]: 1 : ASSERT_FALSE(heap.empty());
189 : 1 : handles.clear();
190 : 1 : Elem last = heap.top();
191 [ + + ]: 801 : for (int32_t x = 0; x < 800; ++x)
192 : : {
193 [ - + ][ + - ]: 800 : ASSERT_LE(last.d_x, heap.top().d_x);
194 : 800 : last = heap.top();
195 : 800 : heap.pop();
196 [ - + ][ + - ]: 800 : ASSERT_EQ(heap.size(), 998u - x);
197 [ - + ][ + - ]: 800 : ASSERT_FALSE(heap.empty());
198 : : }
199 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 199u);
200 [ + + ]: 10001 : for (int32_t x = 0; x < 10000; ++x)
201 : : {
202 : : // two-thirds of the time insert large value, one-third insert small value
203 [ + + ]: 10000 : handles.push_back(heap.push(Elem(4 * ((x % 3 == 0) ? -x : x))));
204 [ + + ]: 10000 : if (x % 10 == 6)
205 : : {
206 : : // also every tenth insert somewhere in the middle
207 : 1000 : handles.push_back(heap.push(Elem(x / 10)));
208 : : }
209 : : // change a few
210 : 10000 : heap.update(handles[x / 10], 4 * (*handles[x / 10]).d_x);
211 : 10000 : heap.update(handles[x / 105], (*handles[x / 4]).d_x - 294);
212 : 10000 : heap.update(handles[x / 33], 6 * (*handles[x / 82]).d_x / 5 - 1);
213 [ - + ][ + - ]: 10000 : ASSERT_EQ(heap.size(), size_t(x) + ((x + 4) / 10) + 200);
214 : : }
215 [ - + ][ + - ]: 1 : ASSERT_EQ(heap.size(), 11199u);
216 [ - + ][ + - ]: 1 : ASSERT_FALSE(heap.empty());
217 : 1 : last = heap.top();
218 [ + + ]: 11200 : while (!heap.empty())
219 : : {
220 [ - + ][ + - ]: 11199 : ASSERT_LE(last.d_x, heap.top().d_x);
221 : 11199 : last = heap.top();
222 : 11199 : heap.pop();
223 : : }
224 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.empty());
225 : 1 : heap.clear();
226 [ - + ][ + - ]: 1 : ASSERT_TRUE(heap.empty());
227 [ + - ][ + - ]: 1 : }
228 : : } // namespace test
229 : : } // namespace cvc5::internal
|
