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 : : * An implementation of a binary heap
11 : : *
12 : : * Attempts to roughly follow the contract of Boost's d_ary_heap.
13 : : * (http://www.boost.org/doc/libs/1_49_0/doc/html/boost/heap/d_ary_heap.html)
14 : : * Also attempts to generalize ext/pd_bs/priority_queue.
15 : : * (http://gcc.gnu.org/onlinedocs/libstdc++/ext/pb_ds/priority_queue.html)
16 : : */
17 : :
18 : : #include "cvc5_private.h"
19 : :
20 : : #ifndef CVC5__BIN_HEAP_H
21 : : #define CVC5__BIN_HEAP_H
22 : :
23 : : #include <functional>
24 : : #include <limits>
25 : :
26 : : #include "base/check.h"
27 : : #include "base/exception.h"
28 : :
29 : : namespace cvc5::internal {
30 : :
31 : : /**
32 : : * BinaryHeap that orders its elements greatest-first (i.e., in the opposite
33 : : * direction of the provided comparator). Update of elements is permitted
34 : : * via handles, which are not invalidated by mutation (pushes and pops etc.).
35 : : * Handles are invalidted when their element is no longer a member of the
36 : : * heap. Iteration over elements is supported but iteration is unsorted and
37 : : * iterators are immutable.
38 : : */
39 : : template <class Elem, class CmpFcn = std::less<Elem> >
40 : : class BinaryHeap
41 : : {
42 : : private:
43 : : typedef Elem T;
44 : : struct HElement;
45 : :
46 : : typedef std::vector<HElement*> ElementVector;
47 : :
48 : : struct HElement
49 : : {
50 : 1026972 : HElement(size_t pos, const T& elem) : d_pos(pos), d_elem(elem) {}
51 : : size_t d_pos;
52 : : T d_elem;
53 : : }; /* struct HElement */
54 : :
55 : : /** A 0 indexed binary heap. */
56 : : ElementVector d_heap;
57 : :
58 : : /** The comparator. */
59 : : CmpFcn d_cmp;
60 : :
61 : : // disallow copy and assignment
62 : : BinaryHeap(const BinaryHeap&) = delete;
63 : : BinaryHeap& operator=(const BinaryHeap&) = delete;
64 : :
65 : : public:
66 : 431758 : BinaryHeap(const CmpFcn& c = CmpFcn()) : d_heap(), d_cmp(c) {}
67 : :
68 : 431410 : ~BinaryHeap() { clear(); }
69 : :
70 : : class handle
71 : : {
72 : : private:
73 : : HElement* d_pointer;
74 : 1156107 : handle(HElement* p) : d_pointer(p) {}
75 : : friend class BinaryHeap;
76 : :
77 : : public:
78 : 1662890 : handle() : d_pointer(nullptr) {}
79 : 30011 : const T& operator*() const
80 : : {
81 [ - + ][ - + ]: 30011 : Assert(d_pointer != nullptr);
[ - - ]
82 : 30011 : return d_pointer->d_elem;
83 : : }
84 : :
85 : 1 : bool operator==(const handle& h) const { return d_pointer == h.d_pointer; }
86 : :
87 : 6 : bool operator!=(const handle& h) const { return d_pointer != h.d_pointer; }
88 : :
89 : : }; /* BinaryHeap<>::handle */
90 : :
91 : : class const_iterator
92 : : {
93 : : public:
94 : : /* The following types are required by trait std::iterator_traits */
95 : :
96 : : /** Iterator tag */
97 : : using iterator_category = std::forward_iterator_tag;
98 : :
99 : : /** The type of the item */
100 : : using value_type = Elem;
101 : :
102 : : /** The pointer type of the item */
103 : : using pointer = const Elem*;
104 : :
105 : : /** The reference type of the item */
106 : : using reference = const Elem&;
107 : :
108 : : /** The type returned when two iterators are subtracted */
109 : : using difference_type = std::ptrdiff_t;
110 : :
111 : : /* End of std::iterator_traits required types */
112 : :
113 : : private:
114 : : typename ElementVector::const_iterator d_iter;
115 : : friend class BinaryHeap;
116 : 769074 : const_iterator(const typename ElementVector::const_iterator& iter)
117 : 769074 : : d_iter(iter)
118 : : {
119 : 769074 : }
120 : :
121 : : public:
122 : : const_iterator() {}
123 : 3 : inline bool operator==(const const_iterator& ci) const
124 : : {
125 : 3 : return d_iter == ci.d_iter;
126 : : }
127 : 737283 : inline bool operator!=(const const_iterator& ci) const
128 : : {
129 : 737283 : return d_iter != ci.d_iter;
130 : : }
131 : 352749 : inline const_iterator& operator++()
132 : : {
133 : 352749 : ++d_iter;
134 : 352749 : return *this;
135 : : }
136 : 4 : inline const_iterator operator++(int)
137 : : {
138 : 4 : const_iterator i = *this;
139 : 4 : ++d_iter;
140 : 4 : return i;
141 : : }
142 : 352758 : inline const T& operator*() const
143 : : {
144 : 352758 : const HElement* he = *d_iter;
145 : 352758 : return he->d_elem;
146 : : }
147 : :
148 : : }; /* BinaryHeap<>::const_iterator */
149 : :
150 : : typedef const_iterator iterator;
151 : :
152 : 4125628 : inline size_t size() const { return d_heap.size(); }
153 : 4103592 : inline bool empty() const { return d_heap.empty(); }
154 : :
155 : 384537 : inline const_iterator begin() const { return const_iterator(d_heap.begin()); }
156 : :
157 : 384537 : inline const_iterator end() const { return const_iterator(d_heap.end()); }
158 : :
159 : 1888627 : void clear()
160 : : {
161 : 1888627 : typename ElementVector::iterator i = d_heap.begin(), iend = d_heap.end();
162 [ + + ]: 2385730 : for (; i != iend; ++i)
163 : : {
164 : 497103 : HElement* he = *i;
165 [ + - ]: 497103 : delete he;
166 : : }
167 : 1888627 : d_heap.clear();
168 : 1888627 : }
169 : :
170 : 380429 : void swap(BinaryHeap& heap)
171 : : {
172 : 380429 : std::swap(d_heap, heap.d_heap);
173 : 380429 : std::swap(d_cmp, heap.d_cmp);
174 : 380429 : }
175 : :
176 : 1026972 : handle push(const T& toAdded)
177 : : {
178 [ - + ][ - + ]: 1026972 : Assert(size() < MAX_SIZE);
[ - - ]
179 : 1026972 : HElement* he = new HElement(size(), toAdded);
180 : 1026972 : d_heap.push_back(he);
181 : 1026972 : up_heap(he);
182 : 1026972 : return handle(he);
183 : : }
184 : :
185 : 517857 : void erase(handle h)
186 : : {
187 [ - + ][ - + ]: 517857 : Assert(!empty());
[ - - ]
188 [ - + ][ - + ]: 517857 : Assert(debugHandle(h));
[ - - ]
189 : :
190 : 517857 : HElement* he = h.d_pointer;
191 : 517857 : size_t pos = he->d_pos;
192 [ + + ]: 517857 : if (pos == root())
193 : : {
194 : : // the top element can be efficiently removed by pop
195 : 331250 : pop();
196 : : }
197 [ + + ]: 186607 : else if (pos == last())
198 : : {
199 : : // the last element can be safely removed
200 : 57472 : d_heap.pop_back();
201 [ + - ]: 57472 : delete he;
202 : : }
203 : : else
204 : : {
205 : : // This corresponds to
206 : : // 1) swapping the elements at pos with the element at last:
207 : : // 2) deleting the new last element
208 : : // 3) updating the position of the new element at pos
209 : 129135 : swapIndices(pos, last());
210 : 129135 : d_heap.pop_back();
211 [ + - ]: 129135 : delete he;
212 : 129135 : update(handle(d_heap[pos]));
213 : : }
214 : 517857 : }
215 : :
216 : 343255 : void pop()
217 : : {
218 [ - + ][ - + ]: 343255 : Assert(!empty());
[ - - ]
219 : 343255 : swapIndices(root(), last());
220 : 343255 : HElement* b = d_heap.back();
221 : 343255 : d_heap.pop_back();
222 [ + - ]: 343255 : delete b;
223 : :
224 [ + + ]: 343255 : if (!empty())
225 : : {
226 : 175861 : down_heap(d_heap.front());
227 : : }
228 : 343255 : }
229 : :
230 : 355588 : const T& top() const
231 : : {
232 [ - + ][ - + ]: 355588 : Assert(!empty());
[ - - ]
233 : 355588 : return (d_heap.front())->d_elem;
234 : : }
235 : :
236 : : private:
237 : 294393 : void update(handle h)
238 : : {
239 [ - + ][ - + ]: 294393 : Assert(!empty());
[ - - ]
240 [ - + ][ - + ]: 294393 : Assert(debugHandle(h));
[ - - ]
241 : :
242 : : // The relationship between h and its parent, left and right has become
243 : : // unknown. But it is assumed that parent <= left, and parent <= right still
244 : : // hold. Figure out whether to up_heap or down_heap.
245 : :
246 [ - + ][ - + ]: 294393 : Assert(!empty());
[ - - ]
247 : 294393 : HElement* he = h.d_pointer;
248 : :
249 : 294393 : size_t pos = he->d_pos;
250 [ + + ]: 294393 : if (pos == root())
251 : : {
252 : : // no parent
253 : 14132 : down_heap(he);
254 : : }
255 : : else
256 : : {
257 : 280261 : size_t par = parent(pos);
258 : 280261 : HElement* at_parent = d_heap[par];
259 [ + + ]: 280261 : if (gt(he->d_elem, at_parent->d_elem))
260 : : {
261 : : // he > parent
262 : 45888 : up_heap(he);
263 : : }
264 : : else
265 : : {
266 : 234373 : down_heap(he);
267 : : }
268 : : }
269 : 294393 : }
270 : :
271 : : public:
272 : 165258 : void update(handle h, const T& val)
273 : : {
274 [ - + ][ - + ]: 165258 : Assert(!empty());
[ - - ]
275 [ - + ][ - + ]: 165258 : Assert(debugHandle(h));
[ - - ]
276 : 165258 : h.d_pointer->d_elem = val;
277 : 165258 : update(h);
278 : 165258 : }
279 : :
280 : : /** (std::numeric_limits<size_t>::max()-2)/2; */
281 : : static const size_t MAX_SIZE;
282 : :
283 : : private:
284 : 1335335 : inline bool gt(const T& a, const T& b) const
285 : : {
286 : : // cmp acts like an operator<
287 : 1335335 : return d_cmp(b, a);
288 : : }
289 : :
290 : 875572 : inline bool lt(const T& a, const T& b) const { return d_cmp(a, b); }
291 : :
292 : 1335335 : inline static size_t parent(size_t p)
293 : : {
294 [ - + ][ - + ]: 1335335 : Assert(p != root());
[ - - ]
295 : 1335335 : return (p - 1) / 2;
296 : : }
297 : 776920 : inline static size_t right(size_t p) { return 2 * p + 2; }
298 : 830319 : inline static size_t left(size_t p) { return 2 * p + 1; }
299 : 4116237 : inline static size_t root() { return 0; }
300 : 658997 : inline size_t last() const
301 : : {
302 [ - + ][ - + ]: 658997 : Assert(!empty());
[ - - ]
303 : 658997 : return size() - 1;
304 : : }
305 : :
306 : 472390 : inline void swapIndices(size_t i, size_t j)
307 : : {
308 : 472390 : HElement* at_i = d_heap[i];
309 : 472390 : HElement* at_j = d_heap[j];
310 : 472390 : swap(i, j, at_i, at_j);
311 : 472390 : }
312 : :
313 : : inline void swapPointers(HElement* at_i, HElement* at_j)
314 : : {
315 : : // still works if at_i == at_j
316 : : size_t i = at_i->d_pos;
317 : : size_t j = at_j->d_pos;
318 : : swap(i, j, at_i, at_j);
319 : : }
320 : :
321 : 1401781 : inline void swap(size_t i, size_t j, HElement* at_i, HElement* at_j)
322 : : {
323 : : // still works if i == j
324 [ - + ][ - + ]: 1401781 : Assert(i == at_i->d_pos);
[ - - ]
325 [ - + ][ - + ]: 1401781 : Assert(j == at_j->d_pos);
[ - - ]
326 : 1401781 : d_heap[i] = at_j;
327 : 1401781 : d_heap[j] = at_i;
328 : 1401781 : at_i->d_pos = j;
329 : 1401781 : at_j->d_pos = i;
330 : 1401781 : }
331 : :
332 : 1072860 : void up_heap(HElement* he)
333 : : {
334 : 1072860 : const size_t& curr = he->d_pos;
335 : : // The value of curr changes implicitly during swap operations.
336 [ + + ]: 1625397 : while (curr != root())
337 : : {
338 : : // he->d_elem > parent
339 : 1055074 : size_t par = parent(curr);
340 : 1055074 : HElement* at_parent = d_heap[par];
341 [ + + ]: 1055074 : if (gt(he->d_elem, at_parent->d_elem))
342 : : {
343 : 552537 : swap(curr, par, he, at_parent);
344 : : }
345 : : else
346 : : {
347 : 502537 : break;
348 : : }
349 : : }
350 : 1072860 : }
351 : :
352 : 424366 : void down_heap(HElement* he)
353 : : {
354 : 424366 : const size_t& curr = he->d_pos;
355 : : // The value of curr changes implicitly during swap operations.
356 : 424366 : size_t N = size();
357 : : size_t r, l;
358 : :
359 [ + + ]: 776920 : while ((r = right(curr)) < N)
360 : : {
361 : 405953 : l = left(curr);
362 : :
363 : : // if at_left == at_right, favor left
364 : 405953 : HElement* at_left = d_heap[l];
365 : 405953 : HElement* at_right = d_heap[r];
366 [ + + ]: 405953 : if (lt(he->d_elem, at_left->d_elem))
367 : : {
368 : : // he < at_left
369 [ + + ]: 330460 : if (lt(at_left->d_elem, at_right->d_elem))
370 : : {
371 : : // he < at_left < at_right
372 : 141142 : swap(curr, r, he, at_right);
373 : : }
374 : : else
375 : : {
376 : : // he < at_left
377 : : // at_right <= at_left
378 : 189318 : swap(curr, l, he, at_left);
379 : : }
380 : : }
381 : : else
382 : : {
383 : : // at_left <= he
384 [ + + ]: 75493 : if (lt(he->d_elem, at_right->d_elem))
385 : : {
386 : : // at_left <= he < at_right
387 : 22094 : swap(curr, r, he, at_right);
388 : : }
389 : : else
390 : : {
391 : : // at_left <= he
392 : : // at_right <= he
393 : 53399 : break;
394 : : }
395 : : }
396 : : }
397 : 424366 : l = left(curr);
398 [ + + ][ + + ]: 424366 : if (r >= N && l < N)
399 : : {
400 : : // there is a left but not a right
401 : 63666 : HElement* at_left = d_heap[l];
402 [ + + ]: 63666 : if (lt(he->d_elem, at_left->d_elem))
403 : : {
404 : : // he < at_left
405 : 24300 : swap(curr, l, he, at_left);
406 : : }
407 : : }
408 : 424366 : }
409 : :
410 : 977508 : bool debugHandle(handle h) const
411 : : {
412 : 977508 : HElement* he = h.d_pointer;
413 [ - + ]: 977508 : if (he == nullptr)
414 : : {
415 : 0 : return true;
416 : : }
417 [ - + ]: 977508 : else if (he->d_pos >= size())
418 : : {
419 : 0 : return false;
420 : : }
421 : : else
422 : : {
423 : 977508 : return he == d_heap[he->d_pos];
424 : : }
425 : : }
426 : :
427 : : }; /* class BinaryHeap<> */
428 : :
429 : : template <class Elem, class CmpFcn>
430 : : const size_t BinaryHeap<Elem, CmpFcn>::MAX_SIZE =
431 : : (std::numeric_limits<size_t>::max() - 2) / 2;
432 : :
433 : : } // namespace cvc5::internal
434 : :
435 : : #endif /* CVC5__BIN_HEAP_H */
|
