GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/bin_heap.h Lines: 163 165 98.8 %
Date: 2021-03-23 Branches: 123 564 21.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bin_heap.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Morgan Deters, Mathias Preiner
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief An implementation of a binary heap
13
 **
14
 ** An implementation of a binary heap.
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 "cvc4_private.h"
22
23
#ifndef CVC4__BIN_HEAP_H
24
#define CVC4__BIN_HEAP_H
25
26
#include <limits>
27
#include <functional>
28
29
#include "base/check.h"
30
#include "base/exception.h"
31
32
namespace CVC4 {
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
593505
    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
171342
  BinaryHeap(const CmpFcn& c = CmpFcn())
68
    : d_heap()
69
171342
    , d_cmp(c)
70
171342
  {}
71
72
171339
  ~BinaryHeap(){
73
171339
    clear();
74
171339
  }
75
76
  class handle {
77
  private:
78
    HElement* d_pointer;
79
671998
    handle(HElement* p) : d_pointer(p){}
80
    friend class BinaryHeap;
81
  public:
82
932631
    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
324730
    const_iterator(const typename ElementVector::const_iterator& iter)
103
324730
      : d_iter(iter)
104
324730
    {}
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
330000
    inline bool operator!=(const const_iterator& ci) const{
111
330000
      return d_iter != ci.d_iter;
112
    }
113
167641
    inline const_iterator& operator++(){
114
167641
      ++d_iter;
115
167641
      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
167659
    inline const T& operator*() const{
123
167659
      const HElement* he = *d_iter;
124
167659
      return he->d_elem;
125
    }
126
127
  };/* BinaryHeap<>::const_iterator */
128
129
  typedef const_iterator iterator;
130
131
2541663
  inline size_t size() const { return d_heap.size(); }
132
2526389
  inline bool empty() const { return d_heap.empty(); }
133
134
162365
  inline const_iterator begin() const {
135
162365
    return const_iterator(d_heap.begin());
136
  }
137
138
162365
  inline const_iterator end() const {
139
162365
    return const_iterator(d_heap.end());
140
  }
141
142
965989
  void clear(){
143
965989
    typename ElementVector::iterator i=d_heap.begin(), iend=d_heap.end();
144
1506605
    for(; i!=iend; ++i){
145
270308
      HElement* he = *i;
146
270308
      delete he;
147
    }
148
965989
    d_heap.clear();
149
965989
  }
150
151
162341
  void swap(BinaryHeap& heap){
152
162341
    std::swap(d_heap, heap.d_heap);
153
162341
    std::swap(d_cmp, heap.d_cmp);
154
162341
  }
155
156
593505
  handle push(const T& toAdded){
157
593505
    Assert(size() < MAX_SIZE);
158
593505
    HElement* he = new HElement(size(), toAdded);
159
593505
    d_heap.push_back(he);
160
593505
    up_heap(he);
161
593505
    return handle(he);
162
  }
163
164
299187
  void erase(handle h){
165
299187
    Assert(!empty());
166
299187
    Assert(debugHandle(h));
167
168
299187
    HElement* he = h.d_pointer;
169
299187
    size_t pos = he->d_pos;
170
299187
    if(pos == root()){
171
      // the top element can be efficiently removed by pop
172
186735
      pop();
173
112452
    }else if(pos == last()){
174
      // the last element can be safely removed
175
33959
      d_heap.pop_back();
176
33959
      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
78493
      swapIndices(pos, last());
183
78493
      d_heap.pop_back();
184
78493
      delete he;
185
78493
      update(handle(d_heap[pos]));
186
    }
187
299187
  }
188
189
210745
  void pop(){
190
210745
    Assert(!empty());
191
210745
    swapIndices(root(), last());
192
210745
    HElement* b = d_heap.back();
193
210745
    d_heap.pop_back();
194
210745
    delete b;
195
196
210745
    if(!empty()){
197
129054
      down_heap(d_heap.front());
198
    }
199
210745
  }
200
201
242949
  const T& top() const {
202
242949
    Assert(!empty());
203
242949
    return (d_heap.front())->d_elem;
204
  }
205
206
private:
207
201851
  void update(handle h){
208
201851
    Assert(!empty());
209
201851
    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
201851
    Assert(!empty());
216
201851
    HElement* he = h.d_pointer;
217
218
201851
    size_t pos = he->d_pos;
219
201851
    if(pos == root()){
220
      // no parent
221
4685
      down_heap(he);
222
    }else{
223
197166
      size_t par = parent(pos);
224
197166
      HElement* at_parent = d_heap[par];
225
197166
      if(gt(he->d_elem, at_parent->d_elem)){
226
        // he > parent
227
23964
        up_heap(he);
228
      }else{
229
173202
        down_heap(he);
230
      }
231
    }
232
201851
  }
233
234
public:
235
123358
  void update(handle h, const T& val){
236
123358
    Assert(!empty());
237
123358
    Assert(debugHandle(h));
238
123358
    h.d_pointer->d_elem = val;
239
123358
    update(h);
240
123358
  }
241
242
  /** (std::numeric_limits<size_t>::max()-2)/2; */
243
  static const size_t MAX_SIZE;
244
245
private:
246
856448
  inline bool gt(const T& a, const T& b) const{
247
    // cmp acts like an operator<
248
856448
    return d_cmp(b, a);
249
  }
250
251
945660
  inline bool lt(const T& a, const T& b) const{
252
945660
    return d_cmp(a, b);
253
  }
254
255
856448
  inline static size_t parent(size_t p){
256
856448
    Assert(p != root());
257
856448
    return (p-1)/2;
258
  }
259
701132
  inline static size_t right(size_t p){ return 2*p+2; }
260
759020
  inline static size_t left(size_t p){ return 2*p+1; }
261
2539269
  inline static size_t root(){ return 0; }
262
401690
  inline size_t last() const{
263
401690
    Assert(!empty());
264
401690
    return size() - 1;
265
  }
266
267
289238
  inline void swapIndices(size_t i, size_t j){
268
289238
    HElement* at_i = d_heap[i];
269
289238
    HElement* at_j = d_heap[j];
270
289238
    swap(i,j,at_i,at_j);
271
289238
  }
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
1052580
  inline void swap(size_t i, size_t j, HElement* at_i, HElement* at_j){
281
    // still works if i == j
282
1052580
    Assert(i == at_i->d_pos);
283
1052580
    Assert(j == at_j->d_pos);
284
1052580
    d_heap[i] = at_j;
285
1052580
    d_heap[j] = at_i;
286
1052580
    at_i->d_pos = j;
287
1052580
    at_j->d_pos = i;
288
1052580
  }
289
290
617469
  void up_heap(HElement* he){
291
617469
    const size_t& curr = he->d_pos;
292
    // The value of curr changes implicitly during swap operations.
293
1324607
    while(curr != root()){
294
      // he->d_elem > parent
295
659282
      size_t par = parent(curr);
296
659282
      HElement* at_parent = d_heap[par];
297
659282
      if(gt(he->d_elem, at_parent->d_elem)){
298
353569
        swap(curr, par, he, at_parent);
299
      }else{
300
305713
        break;
301
      }
302
    }
303
617469
  }
304
305
306941
  void down_heap(HElement* he){
306
306941
    const size_t& curr = he->d_pos;
307
    // The value of curr changes implicitly during swap operations.
308
306941
    size_t N = size();
309
    size_t r, l;
310
311
1095323
    while((r = right(curr)) < N){
312
452079
      l = left(curr);
313
314
      // if at_left == at_right, favor left
315
452079
      HElement* at_left = d_heap[l];
316
452079
      HElement* at_right = d_heap[r];
317
452079
      if(lt(he->d_elem, at_left->d_elem)){
318
        // he < at_left
319
376555
        if(lt(at_left->d_elem, at_right->d_elem)){
320
          // he < at_left < at_right
321
167186
          swap(curr, r, he, at_right);
322
        }else{
323
          //       he <  at_left
324
          // at_right <= at_left
325
209369
          swap(curr, l, he, at_left);
326
        }
327
      }else{
328
        // at_left <= he
329
75524
        if(lt(he->d_elem, at_right->d_elem)){
330
          // at_left <= he < at_right
331
17636
          swap(curr, r, he, at_right);
332
        }else{
333
          // at_left  <= he
334
          // at_right <= he
335
57888
          break;
336
        }
337
      }
338
    }
339
306941
    l = left(curr);
340
306941
    if(r >= N && l < N){
341
      // there is a left but not a right
342
41502
      HElement* at_left = d_heap[l];
343
41502
      if(lt(he->d_elem, at_left->d_elem)){
344
        // he < at_left
345
15582
        swap(curr, l, he, at_left);
346
      }
347
    }
348
306941
  }
349
350
624396
  bool debugHandle(handle h) const{
351
624396
    HElement* he = h.d_pointer;
352
624396
    if( he == NULL ){
353
      return true;
354
624396
    }else if(he->d_pos >= size()){
355
      return false;
356
    }else{
357
624396
      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
}/* CVC4 namespace */
367
368
#endif /* CVC4__BIN_HEAP_H */