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