diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/util/bin_heap.h | 81 |
1 files changed, 45 insertions, 36 deletions
diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h index f8bfe9137..e666611a4 100644 --- a/src/util/bin_heap.h +++ b/src/util/bin_heap.h @@ -20,8 +20,24 @@ #include "cvc4_private.h" +#ifndef __CVC4__BIN_HEAP_H +#define __CVC4__BIN_HEAP_H + +#include <limits> +#include <functional> + +#include "util/exception.h" + namespace CVC4 { +/** + * BinaryHeap that orders its elements greatest-first (i.e., in the opposite + * direction of the provided comparator). Update of elements is permitted + * via handles, which are not invalidated by mutation (pushes and pops etc.). + * Handles are invalidted when their element is no longer a member of the + * heap. Iteration over elements is supported but iteration is unsorted and + * iterators are immutable. + */ template <class Elem, class CmpFcn = std::less<Elem> > class BinaryHeap { private: @@ -34,7 +50,7 @@ private: HElement(size_t pos, const T& elem): d_pos(pos), d_elem(elem) {} size_t d_pos; T d_elem; - }; + };/* struct HElement */ /** A 0 indexed binary heap. */ ElementVector d_heap; @@ -42,6 +58,10 @@ private: /** The comparator. */ CmpFcn d_cmp; + // disallow copy and assignment + BinaryHeap(const BinaryHeap&) CVC4_UNDEFINED; + BinaryHeap& operator=(const BinaryHeap&) CVC4_UNDEFINED; + public: BinaryHeap(const CmpFcn& c = CmpFcn()) : d_heap() @@ -52,28 +72,29 @@ public: clear(); } - BinaryHeap& operator=(const BinaryHeap& other); - - class handle { private: HElement* d_pointer; handle(HElement* p) : d_pointer(p){} - friend class const_handle; friend class BinaryHeap; public: handle() : d_pointer(NULL) {} const T& operator*() const { Assert(d_pointer != NULL); - return *d_pointer; + return d_pointer->d_elem; } bool operator==(const handle& h) const { return d_pointer == h.d_pointer; } + + bool operator!=(const handle& h) const { + return d_pointer != h.d_pointer; + } + }; /* BinaryHeap<>::handle */ - class const_iterator { + class const_iterator : public std::iterator<std::input_iterator_tag, Elem> { private: typename ElementVector::const_iterator d_iter; friend class BinaryHeap; @@ -92,6 +113,11 @@ public: ++d_iter; return *this; } + inline const_iterator operator++(int){ + const_iterator i = *this; + ++d_iter; + return i; + } inline const T& operator*() const{ const HElement* he = *d_iter; return he->d_elem; @@ -99,28 +125,7 @@ public: };/* BinaryHeap<>::const_iterator */ - class const_handle { - private: - const HElement* d_pointer; - const_handle(const HElement* p) : d_pointer(p){} - friend class BinaryHeap; - public: - const_handle() : d_pointer(NULL) {} - const_handle(const handle& h) : d_pointer(h.d_pointer) { } - - const T& operator*() const { - Assert(d_pointer != NULL); - return *d_pointer; - } - - bool operator==(const handle& h) const { - return d_pointer == h.d_pointer; - } - bool operator!=(const handle& h) const { - return d_pointer != h.d_pointer; - } - }; /* BinaryHeap<>::const_handle */ - + typedef const_iterator iterator; inline size_t size() const { return d_heap.size(); } inline bool empty() const { return d_heap.empty(); } @@ -197,6 +202,7 @@ public: return (d_heap.front())->d_elem; } +private: void update(handle h){ Assert(!empty()); Assert(debugHandle(h)); @@ -224,6 +230,7 @@ public: } } +public: void update(handle h, const T& val){ Assert(!empty()); Assert(debugHandle(h)); @@ -234,6 +241,7 @@ public: /** (std::numeric_limits<size_t>::max()-2)/2; */ static const size_t MAX_SIZE; +private: inline bool gt(const T& a, const T& b) const{ // cmp acts like an operator< return d_cmp(b, a); @@ -243,7 +251,6 @@ public: return d_cmp(a, b); } -private: inline static size_t parent(size_t p){ Assert(p != root()); return (p-1)/2; @@ -271,6 +278,8 @@ private: inline void swap(size_t i, size_t j, HElement* at_i, HElement* at_j){ // still works if i == j + Assert(i == at_i->d_pos); + Assert(j == at_j->d_pos); d_heap[i] = at_j; d_heap[j] = at_i; at_i->d_pos = j; @@ -317,10 +326,10 @@ private: }else{ // at_left <= he if(lt(he->d_elem, at_right->d_elem)){ - // left <= he < at_right + // at_left <= he < at_right swap(curr, r, he, at_right); }else{ - // left <= he + // at_left <= he // at_right <= he break; } @@ -331,14 +340,12 @@ private: // there is a left but not a right HElement* at_left = d_heap[l]; if(lt(he->d_elem, at_left->d_elem)){ - // he < at_left + // he < at_left swap(curr, l, he, at_left); } } - } - bool debugHandle(handle h) const{ HElement* he = h.d_pointer; if( he == NULL ){ @@ -355,4 +362,6 @@ private: template <class Elem, class CmpFcn> const size_t BinaryHeap<Elem,CmpFcn>::MAX_SIZE = (std::numeric_limits<size_t>::max()-2)/2; -} /* namespace CVC4 */ +}/* CVC4 namespace */ + +#endif /* __CVC4__BIN_HEAP_H */ |