src/util/bin_heap.h

   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 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     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   BinaryHeap(const CmpFcn& c = CmpFcn())
  68     : d_heap()
  69     , d_cmp(c)
  70   {}
  71
  72   ~BinaryHeap(){
  73     clear();
  74   }
  75
  76   class handle {
  77   private:
  78     HElement* d_pointer;
  79     handle(HElement* p) : d_pointer(p){}
  80     friend class BinaryHeap;
  81   public:
  82     handle() : d_pointer(NULL) {}
  83     const T& operator*() const {
  84       Assert(d_pointer != NULL);
  85       return d_pointer->d_elem;
  86     }
  87
  88     bool operator==(const handle& h) const {
  89       return d_pointer == h.d_pointer;
  90     }
  91
  92     bool operator!=(const handle& h) const {
  93       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     const_iterator(const typename ElementVector::const_iterator& iter)
 103       : d_iter(iter)
 104     {}
 105   public:
 106     const_iterator(){}
 107     inline bool operator==(const const_iterator& ci) const{
 108       return d_iter == ci.d_iter;
 109     }
 110     inline bool operator!=(const const_iterator& ci) const{
 111       return d_iter != ci.d_iter;
 112     }
 113     inline const_iterator& operator++(){
 114       ++d_iter;
 115       return *this;
 116     }
 117     inline const_iterator operator++(int){
 118       const_iterator i = *this;
 119       ++d_iter;
 120       return i;
 121     }
 122     inline const T& operator*() const{
 123       const HElement* he = *d_iter;
 124       return he->d_elem;
 125     }
 126
 127   };/* BinaryHeap<>::const_iterator */
 128
 129   typedef const_iterator iterator;
 130
 131   inline size_t size() const { return d_heap.size(); }
 132   inline bool empty() const { return d_heap.empty(); }
 133
 134   inline const_iterator begin() const {
 135     return const_iterator(d_heap.begin());
 136   }
 137
 138   inline const_iterator end() const {
 139     return const_iterator(d_heap.end());
 140   }
 141
 142   void clear(){
 143     typename ElementVector::iterator i=d_heap.begin(), iend=d_heap.end();
 144     for(; i!=iend; ++i){
 145       HElement* he = *i;
 146       delete he;
 147     }
 148     d_heap.clear();
 149   }
 150
 151   void swap(BinaryHeap& heap){
 152     std::swap(d_heap, heap.d_heap);
 153     std::swap(d_cmp, heap.d_cmp);
 154   }
 155
 156   handle push(const T& toAdded){
 157     Assert(size() < MAX_SIZE);
 158     HElement* he = new HElement(size(), toAdded);
 159     d_heap.push_back(he);
 160     up_heap(he);
 161     return handle(he);
 162   }
 163
 164   void erase(handle h){
 165     Assert(!empty());
 166     Assert(debugHandle(h));
 167
 168     HElement* he = h.d_pointer;
 169     size_t pos = he->d_pos;
 170     if(pos == root()){
 171       // the top element can be efficiently removed by pop
 172       pop();
 173     }else if(pos == last()){
 174       // the last element can be safely removed
 175       d_heap.pop_back();
 176       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       swapIndices(pos, last());
 183       d_heap.pop_back();
 184       delete he;
 185       update(handle(d_heap[pos]));
 186     }
 187   }
 188
 189   void pop(){
 190     Assert(!empty());
 191     swapIndices(root(), last());
 192     HElement* b = d_heap.back();
 193     d_heap.pop_back();
 194     delete b;
 195
 196     if(!empty()){
 197       down_heap(d_heap.front());
 198     }
 199   }
 200
 201   const T& top() const {
 202     Assert(!empty());
 203     return (d_heap.front())->d_elem;
 204   }
 205
 206 private:
 207   void update(handle h){
 208     Assert(!empty());
 209     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     Assert(!empty());
 216     HElement* he = h.d_pointer;
 217
 218     size_t pos = he->d_pos;
 219     if(pos == root()){
 220       // no parent
 221       down_heap(he);
 222     }else{
 223       size_t par = parent(pos);
 224       HElement* at_parent = d_heap[par];
 225       if(gt(he->d_elem, at_parent->d_elem)){
 226         // he > parent
 227         up_heap(he);
 228       }else{
 229         down_heap(he);
 230       }
 231     }
 232   }
 233
 234 public:
 235   void update(handle h, const T& val){
 236     Assert(!empty());
 237     Assert(debugHandle(h));
 238     h.d_pointer->d_elem = val;
 239     update(h);
 240   }
 241
 242   /** (std::numeric_limits<size_t>::max()-2)/2; */
 243   static const size_t MAX_SIZE;
 244
 245 private:
 246   inline bool gt(const T& a, const T& b) const{
 247     // cmp acts like an operator<
 248     return d_cmp(b, a);
 249   }
 250
 251   inline bool lt(const T& a, const T& b) const{
 252     return d_cmp(a, b);
 253   }
 254
 255   inline static size_t parent(size_t p){
 256     Assert(p != root());
 257     return (p-1)/2;
 258   }
 259   inline static size_t right(size_t p){ return 2*p+2; }
 260   inline static size_t left(size_t p){ return 2*p+1; }
 261   inline static size_t root(){ return 0; }
 262   inline size_t last() const{
 263     Assert(!empty());
 264     return size() - 1;
 265   }
 266
 267   inline void swapIndices(size_t i, size_t j){
 268     HElement* at_i = d_heap[i];
 269     HElement* at_j = d_heap[j];
 270     swap(i,j,at_i,at_j);
 271   }
 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   inline void swap(size_t i, size_t j, HElement* at_i, HElement* at_j){
 281     // still works if i == j
 282     Assert(i == at_i->d_pos);
 283     Assert(j == at_j->d_pos);
 284     d_heap[i] = at_j;
 285     d_heap[j] = at_i;
 286     at_i->d_pos = j;
 287     at_j->d_pos = i;
 288   }
 289
 290   void up_heap(HElement* he){
 291     const size_t& curr = he->d_pos;
 292     // The value of curr changes implicitly during swap operations.
 293     while(curr != root()){
 294       // he->d_elem > parent
 295       size_t par = parent(curr);
 296       HElement* at_parent = d_heap[par];
 297       if(gt(he->d_elem, at_parent->d_elem)){
 298         swap(curr, par, he, at_parent);
 299       }else{
 300         break;
 301       }
 302     }
 303   }
 304
 305   void down_heap(HElement* he){
 306     const size_t& curr = he->d_pos;
 307     // The value of curr changes implicitly during swap operations.
 308     size_t N = size();
 309     size_t r, l;
 310
 311     while((r = right(curr)) < N){
 312       l = left(curr);
 313
 314       // if at_left == at_right, favor left
 315       HElement* at_left = d_heap[l];
 316       HElement* at_right = d_heap[r];
 317       if(lt(he->d_elem, at_left->d_elem)){
 318         // he < at_left
 319         if(lt(at_left->d_elem, at_right->d_elem)){
 320           // he < at_left < at_right
 321           swap(curr, r, he, at_right);
 322         }else{
 323           //       he <  at_left
 324           // at_right <= at_left
 325           swap(curr, l, he, at_left);
 326         }
 327       }else{
 328         // at_left <= he
 329         if(lt(he->d_elem, at_right->d_elem)){
 330           // at_left <= he < at_right
 331           swap(curr, r, he, at_right);
 332         }else{
 333           // at_left  <= he
 334           // at_right <= he
 335           break;
 336         }
 337       }
 338     }
 339     l = left(curr);
 340     if(r >= N && l < N){
 341       // there is a left but not a right
 342       HElement* at_left = d_heap[l];
 343       if(lt(he->d_elem, at_left->d_elem)){
 344         // he < at_left
 345         swap(curr, l, he, at_left);
 346       }
 347     }
 348   }
 349
 350   bool debugHandle(handle h) const{
 351     HElement* he = h.d_pointer;
 352     if( he == NULL ){
 353       return true;
 354     }else if(he->d_pos >= size()){
 355       return false;
 356     }else{
 357       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 /* CVC4__BIN_HEAP_H */