1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Tim King, Morgan Deters, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* An implementation of a binary heap |
14 |
|
* |
15 |
|
* Attempts to roughly follow the contract of Boost's d_ary_heap. |
16 |
|
* (http://www.boost.org/doc/libs/1_49_0/doc/html/boost/heap/d_ary_heap.html) |
17 |
|
* Also attempts to generalize ext/pd_bs/priority_queue. |
18 |
|
* (http://gcc.gnu.org/onlinedocs/libstdc++/ext/pb_ds/priority_queue.html) |
19 |
|
*/ |
20 |
|
|
21 |
|
#include "cvc5_private.h" |
22 |
|
|
23 |
|
#ifndef CVC5__BIN_HEAP_H |
24 |
|
#define CVC5__BIN_HEAP_H |
25 |
|
|
26 |
|
#include <limits> |
27 |
|
#include <functional> |
28 |
|
|
29 |
|
#include "base/check.h" |
30 |
|
#include "base/exception.h" |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
|
34 |
|
/** |
35 |
|
* BinaryHeap that orders its elements greatest-first (i.e., in the opposite |
36 |
|
* direction of the provided comparator). Update of elements is permitted |
37 |
|
* via handles, which are not invalidated by mutation (pushes and pops etc.). |
38 |
|
* Handles are invalidted when their element is no longer a member of the |
39 |
|
* heap. Iteration over elements is supported but iteration is unsorted and |
40 |
|
* iterators are immutable. |
41 |
|
*/ |
42 |
|
template <class Elem, class CmpFcn = std::less<Elem> > |
43 |
|
class BinaryHeap { |
44 |
|
private: |
45 |
|
typedef Elem T; |
46 |
|
struct HElement; |
47 |
|
|
48 |
|
typedef std::vector<HElement*> ElementVector; |
49 |
|
|
50 |
|
struct HElement { |
51 |
685182 |
HElement(size_t pos, const T& elem): d_pos(pos), d_elem(elem) {} |
52 |
|
size_t d_pos; |
53 |
|
T d_elem; |
54 |
|
};/* struct HElement */ |
55 |
|
|
56 |
|
/** A 0 indexed binary heap. */ |
57 |
|
ElementVector d_heap; |
58 |
|
|
59 |
|
/** The comparator. */ |
60 |
|
CmpFcn d_cmp; |
61 |
|
|
62 |
|
// disallow copy and assignment |
63 |
|
BinaryHeap(const BinaryHeap&) = delete; |
64 |
|
BinaryHeap& operator=(const BinaryHeap&) = delete; |
65 |
|
|
66 |
|
public: |
67 |
216497 |
BinaryHeap(const CmpFcn& c = CmpFcn()) |
68 |
|
: d_heap() |
69 |
216497 |
, d_cmp(c) |
70 |
216497 |
{} |
71 |
|
|
72 |
216492 |
~BinaryHeap(){ |
73 |
216492 |
clear(); |
74 |
216492 |
} |
75 |
|
|
76 |
|
class handle { |
77 |
|
private: |
78 |
|
HElement* d_pointer; |
79 |
773665 |
handle(HElement* p) : d_pointer(p){} |
80 |
|
friend class BinaryHeap; |
81 |
|
public: |
82 |
1079823 |
handle() : d_pointer(NULL) {} |
83 |
60022 |
const T& operator*() const { |
84 |
60022 |
Assert(d_pointer != NULL); |
85 |
60022 |
return d_pointer->d_elem; |
86 |
|
} |
87 |
|
|
88 |
2 |
bool operator==(const handle& h) const { |
89 |
2 |
return d_pointer == h.d_pointer; |
90 |
|
} |
91 |
|
|
92 |
12 |
bool operator!=(const handle& h) const { |
93 |
12 |
return d_pointer != h.d_pointer; |
94 |
|
} |
95 |
|
|
96 |
|
}; /* BinaryHeap<>::handle */ |
97 |
|
|
98 |
|
class const_iterator { |
99 |
|
public: |
100 |
|
/* The following types are required by trait std::iterator_traits */ |
101 |
|
|
102 |
|
/** Iterator tag */ |
103 |
|
using iterator_category = std::forward_iterator_tag; |
104 |
|
|
105 |
|
/** The type of the item */ |
106 |
|
using value_type = Elem; |
107 |
|
|
108 |
|
/** The pointer type of the item */ |
109 |
|
using pointer = const Elem*; |
110 |
|
|
111 |
|
/** The reference type of the item */ |
112 |
|
using reference = const Elem&; |
113 |
|
|
114 |
|
/** The type returned when two iterators are subtracted */ |
115 |
|
using difference_type = std::ptrdiff_t; |
116 |
|
|
117 |
|
/* End of std::iterator_traits required types */ |
118 |
|
|
119 |
|
private: |
120 |
|
typename ElementVector::const_iterator d_iter; |
121 |
|
friend class BinaryHeap; |
122 |
402492 |
const_iterator(const typename ElementVector::const_iterator& iter) |
123 |
402492 |
: d_iter(iter) |
124 |
402492 |
{} |
125 |
|
public: |
126 |
|
const_iterator(){} |
127 |
6 |
inline bool operator==(const const_iterator& ci) const{ |
128 |
6 |
return d_iter == ci.d_iter; |
129 |
|
} |
130 |
401575 |
inline bool operator!=(const const_iterator& ci) const{ |
131 |
401575 |
return d_iter != ci.d_iter; |
132 |
|
} |
133 |
200335 |
inline const_iterator& operator++(){ |
134 |
200335 |
++d_iter; |
135 |
200335 |
return *this; |
136 |
|
} |
137 |
8 |
inline const_iterator operator++(int){ |
138 |
8 |
const_iterator i = *this; |
139 |
8 |
++d_iter; |
140 |
8 |
return i; |
141 |
|
} |
142 |
200353 |
inline const T& operator*() const{ |
143 |
200353 |
const HElement* he = *d_iter; |
144 |
200353 |
return he->d_elem; |
145 |
|
} |
146 |
|
|
147 |
|
};/* BinaryHeap<>::const_iterator */ |
148 |
|
|
149 |
|
typedef const_iterator iterator; |
150 |
|
|
151 |
2880764 |
inline size_t size() const { return d_heap.size(); } |
152 |
2861496 |
inline bool empty() const { return d_heap.empty(); } |
153 |
|
|
154 |
201246 |
inline const_iterator begin() const { |
155 |
201246 |
return const_iterator(d_heap.begin()); |
156 |
|
} |
157 |
|
|
158 |
201246 |
inline const_iterator end() const { |
159 |
201246 |
return const_iterator(d_heap.end()); |
160 |
|
} |
161 |
|
|
162 |
1250231 |
void clear(){ |
163 |
1250231 |
typename ElementVector::iterator i=d_heap.begin(), iend=d_heap.end(); |
164 |
1890387 |
for(; i!=iend; ++i){ |
165 |
320078 |
HElement* he = *i; |
166 |
320078 |
delete he; |
167 |
|
} |
168 |
1250231 |
d_heap.clear(); |
169 |
1250231 |
} |
170 |
|
|
171 |
201222 |
void swap(BinaryHeap& heap){ |
172 |
201222 |
std::swap(d_heap, heap.d_heap); |
173 |
201222 |
std::swap(d_cmp, heap.d_cmp); |
174 |
201222 |
} |
175 |
|
|
176 |
685182 |
handle push(const T& toAdded){ |
177 |
685182 |
Assert(size() < MAX_SIZE); |
178 |
685182 |
HElement* he = new HElement(size(), toAdded); |
179 |
685182 |
d_heap.push_back(he); |
180 |
685182 |
up_heap(he); |
181 |
685182 |
return handle(he); |
182 |
|
} |
183 |
|
|
184 |
341094 |
void erase(handle h){ |
185 |
341094 |
Assert(!empty()); |
186 |
341094 |
Assert(debugHandle(h)); |
187 |
|
|
188 |
341094 |
HElement* he = h.d_pointer; |
189 |
341094 |
size_t pos = he->d_pos; |
190 |
341094 |
if(pos == root()){ |
191 |
|
// the top element can be efficiently removed by pop |
192 |
213954 |
pop(); |
193 |
127140 |
}else if(pos == last()){ |
194 |
|
// the last element can be safely removed |
195 |
38657 |
d_heap.pop_back(); |
196 |
38657 |
delete he; |
197 |
|
}else{ |
198 |
|
// This corresponds to |
199 |
|
// 1) swapping the elements at pos with the element at last: |
200 |
|
// 2) deleting the new last element |
201 |
|
// 3) updating the position of the new element at pos |
202 |
88483 |
swapIndices(pos, last()); |
203 |
88483 |
d_heap.pop_back(); |
204 |
88483 |
delete he; |
205 |
88483 |
update(handle(d_heap[pos])); |
206 |
|
} |
207 |
341094 |
} |
208 |
|
|
209 |
237964 |
void pop(){ |
210 |
237964 |
Assert(!empty()); |
211 |
237964 |
swapIndices(root(), last()); |
212 |
237964 |
HElement* b = d_heap.back(); |
213 |
237964 |
d_heap.pop_back(); |
214 |
237964 |
delete b; |
215 |
|
|
216 |
237964 |
if(!empty()){ |
217 |
140220 |
down_heap(d_heap.front()); |
218 |
|
} |
219 |
237964 |
} |
220 |
|
|
221 |
272065 |
const T& top() const { |
222 |
272065 |
Assert(!empty()); |
223 |
272065 |
return (d_heap.front())->d_elem; |
224 |
|
} |
225 |
|
|
226 |
|
private: |
227 |
223619 |
void update(handle h){ |
228 |
223619 |
Assert(!empty()); |
229 |
223619 |
Assert(debugHandle(h)); |
230 |
|
|
231 |
|
// The relationship between h and its parent, left and right has become unknown. |
232 |
|
// But it is assumed that parent <= left, and parent <= right still hold. |
233 |
|
// Figure out whether to up_heap or down_heap. |
234 |
|
|
235 |
223619 |
Assert(!empty()); |
236 |
223619 |
HElement* he = h.d_pointer; |
237 |
|
|
238 |
223619 |
size_t pos = he->d_pos; |
239 |
223619 |
if(pos == root()){ |
240 |
|
// no parent |
241 |
5256 |
down_heap(he); |
242 |
|
}else{ |
243 |
218363 |
size_t par = parent(pos); |
244 |
218363 |
HElement* at_parent = d_heap[par]; |
245 |
218363 |
if(gt(he->d_elem, at_parent->d_elem)){ |
246 |
|
// he > parent |
247 |
28501 |
up_heap(he); |
248 |
|
}else{ |
249 |
189862 |
down_heap(he); |
250 |
|
} |
251 |
|
} |
252 |
223619 |
} |
253 |
|
|
254 |
|
public: |
255 |
135136 |
void update(handle h, const T& val){ |
256 |
135136 |
Assert(!empty()); |
257 |
135136 |
Assert(debugHandle(h)); |
258 |
135136 |
h.d_pointer->d_elem = val; |
259 |
135136 |
update(h); |
260 |
135136 |
} |
261 |
|
|
262 |
|
/** (std::numeric_limits<size_t>::max()-2)/2; */ |
263 |
|
static const size_t MAX_SIZE; |
264 |
|
|
265 |
|
private: |
266 |
972321 |
inline bool gt(const T& a, const T& b) const{ |
267 |
|
// cmp acts like an operator< |
268 |
972321 |
return d_cmp(b, a); |
269 |
|
} |
270 |
|
|
271 |
989765 |
inline bool lt(const T& a, const T& b) const{ |
272 |
989765 |
return d_cmp(a, b); |
273 |
|
} |
274 |
|
|
275 |
972321 |
inline static size_t parent(size_t p){ |
276 |
972321 |
Assert(p != root()); |
277 |
972321 |
return (p-1)/2; |
278 |
|
} |
279 |
746866 |
inline static size_t right(size_t p){ return 2*p+2; } |
280 |
807347 |
inline static size_t left(size_t p){ return 2*p+1; } |
281 |
2891554 |
inline static size_t root(){ return 0; } |
282 |
453587 |
inline size_t last() const{ |
283 |
453587 |
Assert(!empty()); |
284 |
453587 |
return size() - 1; |
285 |
|
} |
286 |
|
|
287 |
326447 |
inline void swapIndices(size_t i, size_t j){ |
288 |
326447 |
HElement* at_i = d_heap[i]; |
289 |
326447 |
HElement* at_j = d_heap[j]; |
290 |
326447 |
swap(i,j,at_i,at_j); |
291 |
326447 |
} |
292 |
|
|
293 |
|
inline void swapPointers(HElement* at_i, HElement* at_j){ |
294 |
|
// still works if at_i == at_j |
295 |
|
size_t i = at_i->d_pos; |
296 |
|
size_t j = at_j->d_pos; |
297 |
|
swap(i,j,at_i,at_j); |
298 |
|
} |
299 |
|
|
300 |
1158015 |
inline void swap(size_t i, size_t j, HElement* at_i, HElement* at_j){ |
301 |
|
// still works if i == j |
302 |
1158015 |
Assert(i == at_i->d_pos); |
303 |
1158015 |
Assert(j == at_j->d_pos); |
304 |
1158015 |
d_heap[i] = at_j; |
305 |
1158015 |
d_heap[j] = at_i; |
306 |
1158015 |
at_i->d_pos = j; |
307 |
1158015 |
at_j->d_pos = i; |
308 |
1158015 |
} |
309 |
|
|
310 |
713683 |
void up_heap(HElement* he){ |
311 |
713683 |
const size_t& curr = he->d_pos; |
312 |
|
// The value of curr changes implicitly during swap operations. |
313 |
1519429 |
while(curr != root()){ |
314 |
|
// he->d_elem > parent |
315 |
753958 |
size_t par = parent(curr); |
316 |
753958 |
HElement* at_parent = d_heap[par]; |
317 |
753958 |
if(gt(he->d_elem, at_parent->d_elem)){ |
318 |
402873 |
swap(curr, par, he, at_parent); |
319 |
|
}else{ |
320 |
351085 |
break; |
321 |
|
} |
322 |
|
} |
323 |
713683 |
} |
324 |
|
|
325 |
335338 |
void down_heap(HElement* he){ |
326 |
335338 |
const size_t& curr = he->d_pos; |
327 |
|
// The value of curr changes implicitly during swap operations. |
328 |
335338 |
size_t N = size(); |
329 |
|
size_t r, l; |
330 |
|
|
331 |
1158394 |
while((r = right(curr)) < N){ |
332 |
472009 |
l = left(curr); |
333 |
|
|
334 |
|
// if at_left == at_right, favor left |
335 |
472009 |
HElement* at_left = d_heap[l]; |
336 |
472009 |
HElement* at_right = d_heap[r]; |
337 |
472009 |
if(lt(he->d_elem, at_left->d_elem)){ |
338 |
|
// he < at_left |
339 |
392532 |
if(lt(at_left->d_elem, at_right->d_elem)){ |
340 |
|
// he < at_left < at_right |
341 |
173275 |
swap(curr, r, he, at_right); |
342 |
|
}else{ |
343 |
|
// he < at_left |
344 |
|
// at_right <= at_left |
345 |
219257 |
swap(curr, l, he, at_left); |
346 |
|
} |
347 |
|
}else{ |
348 |
|
// at_left <= he |
349 |
79477 |
if(lt(he->d_elem, at_right->d_elem)){ |
350 |
|
// at_left <= he < at_right |
351 |
18996 |
swap(curr, r, he, at_right); |
352 |
|
}else{ |
353 |
|
// at_left <= he |
354 |
|
// at_right <= he |
355 |
60481 |
break; |
356 |
|
} |
357 |
|
} |
358 |
|
} |
359 |
335338 |
l = left(curr); |
360 |
335338 |
if(r >= N && l < N){ |
361 |
|
// there is a left but not a right |
362 |
45747 |
HElement* at_left = d_heap[l]; |
363 |
45747 |
if(lt(he->d_elem, at_left->d_elem)){ |
364 |
|
// he < at_left |
365 |
17167 |
swap(curr, l, he, at_left); |
366 |
|
} |
367 |
|
} |
368 |
335338 |
} |
369 |
|
|
370 |
699849 |
bool debugHandle(handle h) const{ |
371 |
699849 |
HElement* he = h.d_pointer; |
372 |
699849 |
if( he == NULL ){ |
373 |
|
return true; |
374 |
699849 |
}else if(he->d_pos >= size()){ |
375 |
|
return false; |
376 |
|
}else{ |
377 |
699849 |
return he == d_heap[he->d_pos]; |
378 |
|
} |
379 |
|
} |
380 |
|
|
381 |
|
}; /* class BinaryHeap<> */ |
382 |
|
|
383 |
|
template <class Elem, class CmpFcn> |
384 |
|
const size_t BinaryHeap<Elem,CmpFcn>::MAX_SIZE = (std::numeric_limits<size_t>::max()-2)/2; |
385 |
|
|
386 |
|
} // namespace cvc5 |
387 |
|
|
388 |
|
#endif /* CVC5__BIN_HEAP_H */ |