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 |
640891 |
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 |
187435 |
BinaryHeap(const CmpFcn& c = CmpFcn()) |
68 |
|
: d_heap() |
69 |
187435 |
, d_cmp(c) |
70 |
187435 |
{} |
71 |
|
|
72 |
187432 |
~BinaryHeap(){ |
73 |
187432 |
clear(); |
74 |
187432 |
} |
75 |
|
|
76 |
|
class handle { |
77 |
|
private: |
78 |
|
HElement* d_pointer; |
79 |
726292 |
handle(HElement* p) : d_pointer(p){} |
80 |
|
friend class BinaryHeap; |
81 |
|
public: |
82 |
1006161 |
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 : public std::iterator<std::input_iterator_tag, Elem> { |
99 |
|
private: |
100 |
|
typename ElementVector::const_iterator d_iter; |
101 |
|
friend class BinaryHeap; |
102 |
355080 |
const_iterator(const typename ElementVector::const_iterator& iter) |
103 |
355080 |
: d_iter(iter) |
104 |
355080 |
{} |
105 |
|
public: |
106 |
|
const_iterator(){} |
107 |
6 |
inline bool operator==(const const_iterator& ci) const{ |
108 |
6 |
return d_iter == ci.d_iter; |
109 |
|
} |
110 |
364140 |
inline bool operator!=(const const_iterator& ci) const{ |
111 |
364140 |
return d_iter != ci.d_iter; |
112 |
|
} |
113 |
186606 |
inline const_iterator& operator++(){ |
114 |
186606 |
++d_iter; |
115 |
186606 |
return *this; |
116 |
|
} |
117 |
8 |
inline const_iterator operator++(int){ |
118 |
8 |
const_iterator i = *this; |
119 |
8 |
++d_iter; |
120 |
8 |
return i; |
121 |
|
} |
122 |
186624 |
inline const T& operator*() const{ |
123 |
186624 |
const HElement* he = *d_iter; |
124 |
186624 |
return he->d_elem; |
125 |
|
} |
126 |
|
|
127 |
|
};/* BinaryHeap<>::const_iterator */ |
128 |
|
|
129 |
|
typedef const_iterator iterator; |
130 |
|
|
131 |
2741814 |
inline size_t size() const { return d_heap.size(); } |
132 |
2722931 |
inline bool empty() const { return d_heap.empty(); } |
133 |
|
|
134 |
177540 |
inline const_iterator begin() const { |
135 |
177540 |
return const_iterator(d_heap.begin()); |
136 |
|
} |
137 |
|
|
138 |
177540 |
inline const_iterator end() const { |
139 |
177540 |
return const_iterator(d_heap.end()); |
140 |
|
} |
141 |
|
|
142 |
990073 |
void clear(){ |
143 |
990073 |
typename ElementVector::iterator i=d_heap.begin(), iend=d_heap.end(); |
144 |
1578503 |
for(; i!=iend; ++i){ |
145 |
294215 |
HElement* he = *i; |
146 |
294215 |
delete he; |
147 |
|
} |
148 |
990073 |
d_heap.clear(); |
149 |
990073 |
} |
150 |
|
|
151 |
177516 |
void swap(BinaryHeap& heap){ |
152 |
177516 |
std::swap(d_heap, heap.d_heap); |
153 |
177516 |
std::swap(d_cmp, heap.d_cmp); |
154 |
177516 |
} |
155 |
|
|
156 |
640891 |
handle push(const T& toAdded){ |
157 |
640891 |
Assert(size() < MAX_SIZE); |
158 |
640891 |
HElement* he = new HElement(size(), toAdded); |
159 |
640891 |
d_heap.push_back(he); |
160 |
640891 |
up_heap(he); |
161 |
640891 |
return handle(he); |
162 |
|
} |
163 |
|
|
164 |
322666 |
void erase(handle h){ |
165 |
322666 |
Assert(!empty()); |
166 |
322666 |
Assert(debugHandle(h)); |
167 |
|
|
168 |
322666 |
HElement* he = h.d_pointer; |
169 |
322666 |
size_t pos = he->d_pos; |
170 |
322666 |
if(pos == root()){ |
171 |
|
// the top element can be efficiently removed by pop |
172 |
200259 |
pop(); |
173 |
122407 |
}else if(pos == last()){ |
174 |
|
// the last element can be safely removed |
175 |
37006 |
d_heap.pop_back(); |
176 |
37006 |
delete he; |
177 |
|
}else{ |
178 |
|
// This corresponds to |
179 |
|
// 1) swapping the elements at pos with the element at last: |
180 |
|
// 2) deleting the new last element |
181 |
|
// 3) updating the position of the new element at pos |
182 |
85401 |
swapIndices(pos, last()); |
183 |
85401 |
d_heap.pop_back(); |
184 |
85401 |
delete he; |
185 |
85401 |
update(handle(d_heap[pos])); |
186 |
|
} |
187 |
322666 |
} |
188 |
|
|
189 |
224269 |
void pop(){ |
190 |
224269 |
Assert(!empty()); |
191 |
224269 |
swapIndices(root(), last()); |
192 |
224269 |
HElement* b = d_heap.back(); |
193 |
224269 |
d_heap.pop_back(); |
194 |
224269 |
delete b; |
195 |
|
|
196 |
224269 |
if(!empty()){ |
197 |
134840 |
down_heap(d_heap.front()); |
198 |
|
} |
199 |
224269 |
} |
200 |
|
|
201 |
258095 |
const T& top() const { |
202 |
258095 |
Assert(!empty()); |
203 |
258095 |
return (d_heap.front())->d_elem; |
204 |
|
} |
205 |
|
|
206 |
|
private: |
207 |
220910 |
void update(handle h){ |
208 |
220910 |
Assert(!empty()); |
209 |
220910 |
Assert(debugHandle(h)); |
210 |
|
|
211 |
|
// The relationship between h and its parent, left and right has become unknown. |
212 |
|
// But it is assumed that parent <= left, and parent <= right still hold. |
213 |
|
// Figure out whether to up_heap or down_heap. |
214 |
|
|
215 |
220910 |
Assert(!empty()); |
216 |
220910 |
HElement* he = h.d_pointer; |
217 |
|
|
218 |
220910 |
size_t pos = he->d_pos; |
219 |
220910 |
if(pos == root()){ |
220 |
|
// no parent |
221 |
5064 |
down_heap(he); |
222 |
|
}else{ |
223 |
215846 |
size_t par = parent(pos); |
224 |
215846 |
HElement* at_parent = d_heap[par]; |
225 |
215846 |
if(gt(he->d_elem, at_parent->d_elem)){ |
226 |
|
// he > parent |
227 |
28506 |
up_heap(he); |
228 |
|
}else{ |
229 |
187340 |
down_heap(he); |
230 |
|
} |
231 |
|
} |
232 |
220910 |
} |
233 |
|
|
234 |
|
public: |
235 |
135509 |
void update(handle h, const T& val){ |
236 |
135509 |
Assert(!empty()); |
237 |
135509 |
Assert(debugHandle(h)); |
238 |
135509 |
h.d_pointer->d_elem = val; |
239 |
135509 |
update(h); |
240 |
135509 |
} |
241 |
|
|
242 |
|
/** (std::numeric_limits<size_t>::max()-2)/2; */ |
243 |
|
static const size_t MAX_SIZE; |
244 |
|
|
245 |
|
private: |
246 |
941077 |
inline bool gt(const T& a, const T& b) const{ |
247 |
|
// cmp acts like an operator< |
248 |
941077 |
return d_cmp(b, a); |
249 |
|
} |
250 |
|
|
251 |
972628 |
inline bool lt(const T& a, const T& b) const{ |
252 |
972628 |
return d_cmp(a, b); |
253 |
|
} |
254 |
|
|
255 |
941077 |
inline static size_t parent(size_t p){ |
256 |
941077 |
Assert(p != root()); |
257 |
941077 |
return (p-1)/2; |
258 |
|
} |
259 |
731237 |
inline static size_t right(size_t p){ return 2*p+2; } |
260 |
791526 |
inline static size_t left(size_t p){ return 2*p+1; } |
261 |
2765850 |
inline static size_t root(){ return 0; } |
262 |
432077 |
inline size_t last() const{ |
263 |
432077 |
Assert(!empty()); |
264 |
432077 |
return size() - 1; |
265 |
|
} |
266 |
|
|
267 |
309670 |
inline void swapIndices(size_t i, size_t j){ |
268 |
309670 |
HElement* at_i = d_heap[i]; |
269 |
309670 |
HElement* at_j = d_heap[j]; |
270 |
309670 |
swap(i,j,at_i,at_j); |
271 |
309670 |
} |
272 |
|
|
273 |
|
inline void swapPointers(HElement* at_i, HElement* at_j){ |
274 |
|
// still works if at_i == at_j |
275 |
|
size_t i = at_i->d_pos; |
276 |
|
size_t j = at_j->d_pos; |
277 |
|
swap(i,j,at_i,at_j); |
278 |
|
} |
279 |
|
|
280 |
1117730 |
inline void swap(size_t i, size_t j, HElement* at_i, HElement* at_j){ |
281 |
|
// still works if i == j |
282 |
1117730 |
Assert(i == at_i->d_pos); |
283 |
1117730 |
Assert(j == at_j->d_pos); |
284 |
1117730 |
d_heap[i] = at_j; |
285 |
1117730 |
d_heap[j] = at_i; |
286 |
1117730 |
at_i->d_pos = j; |
287 |
1117730 |
at_j->d_pos = i; |
288 |
1117730 |
} |
289 |
|
|
290 |
669397 |
void up_heap(HElement* he){ |
291 |
669397 |
const size_t& curr = he->d_pos; |
292 |
|
// The value of curr changes implicitly during swap operations. |
293 |
1444459 |
while(curr != root()){ |
294 |
|
// he->d_elem > parent |
295 |
725231 |
size_t par = parent(curr); |
296 |
725231 |
HElement* at_parent = d_heap[par]; |
297 |
725231 |
if(gt(he->d_elem, at_parent->d_elem)){ |
298 |
387531 |
swap(curr, par, he, at_parent); |
299 |
|
}else{ |
300 |
337700 |
break; |
301 |
|
} |
302 |
|
} |
303 |
669397 |
} |
304 |
|
|
305 |
327244 |
void down_heap(HElement* he){ |
306 |
327244 |
const size_t& curr = he->d_pos; |
307 |
|
// The value of curr changes implicitly during swap operations. |
308 |
327244 |
size_t N = size(); |
309 |
|
size_t r, l; |
310 |
|
|
311 |
1135230 |
while((r = right(curr)) < N){ |
312 |
464282 |
l = left(curr); |
313 |
|
|
314 |
|
// if at_left == at_right, favor left |
315 |
464282 |
HElement* at_left = d_heap[l]; |
316 |
464282 |
HElement* at_right = d_heap[r]; |
317 |
464282 |
if(lt(he->d_elem, at_left->d_elem)){ |
318 |
|
// he < at_left |
319 |
385644 |
if(lt(at_left->d_elem, at_right->d_elem)){ |
320 |
|
// he < at_left < at_right |
321 |
170669 |
swap(curr, r, he, at_right); |
322 |
|
}else{ |
323 |
|
// he < at_left |
324 |
|
// at_right <= at_left |
325 |
214975 |
swap(curr, l, he, at_left); |
326 |
|
} |
327 |
|
}else{ |
328 |
|
// at_left <= he |
329 |
78638 |
if(lt(he->d_elem, at_right->d_elem)){ |
330 |
|
// at_left <= he < at_right |
331 |
18349 |
swap(curr, r, he, at_right); |
332 |
|
}else{ |
333 |
|
// at_left <= he |
334 |
|
// at_right <= he |
335 |
60289 |
break; |
336 |
|
} |
337 |
|
} |
338 |
|
} |
339 |
327244 |
l = left(curr); |
340 |
327244 |
if(r >= N && l < N){ |
341 |
|
// there is a left but not a right |
342 |
44064 |
HElement* at_left = d_heap[l]; |
343 |
44064 |
if(lt(he->d_elem, at_left->d_elem)){ |
344 |
|
// he < at_left |
345 |
16536 |
swap(curr, l, he, at_left); |
346 |
|
} |
347 |
|
} |
348 |
327244 |
} |
349 |
|
|
350 |
679085 |
bool debugHandle(handle h) const{ |
351 |
679085 |
HElement* he = h.d_pointer; |
352 |
679085 |
if( he == NULL ){ |
353 |
|
return true; |
354 |
679085 |
}else if(he->d_pos >= size()){ |
355 |
|
return false; |
356 |
|
}else{ |
357 |
679085 |
return he == d_heap[he->d_pos]; |
358 |
|
} |
359 |
|
} |
360 |
|
|
361 |
|
}; /* class BinaryHeap<> */ |
362 |
|
|
363 |
|
template <class Elem, class CmpFcn> |
364 |
|
const size_t BinaryHeap<Elem,CmpFcn>::MAX_SIZE = (std::numeric_limits<size_t>::max()-2)/2; |
365 |
|
|
366 |
|
} // namespace cvc5 |
367 |
|
|
368 |
|
#endif /* CVC5__BIN_HEAP_H */ |