diff options
| -rw-r--r-- | src/util/bin_heap.h | 81 | ||||
| -rw-r--r-- | test/unit/Makefile.am | 1 | ||||
| -rw-r--r-- | test/unit/util/binary_heap_black.h | 227 |
3 files changed, 273 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 */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 937a4e8c8..eccbd250f 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -41,6 +41,7 @@ UNIT_TESTS += \ context/stacking_vector_black \ util/array_store_all_black \ util/assert_white \ + util/binary_heap_black \ util/bitvector_black \ util/datatype_black \ util/configuration_black \ diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h new file mode 100644 index 000000000..41e4d0e75 --- /dev/null +++ b/test/unit/util/binary_heap_black.h @@ -0,0 +1,227 @@ +/********************* */ +/*! \file binary_heap_black.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::BinaryHeap + ** + ** Black box testing of CVC4::BinaryHeap. + **/ + +#include <cxxtest/TestSuite.h> + +#include <iostream> +#include <sstream> + +#include "util/bin_heap.h" + +using namespace CVC4; +using namespace std; + +class BinaryHeapBlack : public CxxTest::TestSuite { +public: + + void setUp() { + } + + void tearDown() { + } + + /** + * Test a a series of simple heaps (push a few then pop all then do others). + * Done as a series to test if the heap structure falls into a bad state + * after prolonged use. + */ + void testHeapSeries() { + BinaryHeap<int> heap; + + // First test a heap of 1 element + TS_ASSERT_EQUALS(heap.size(), 0u); + TS_ASSERT(heap.empty()); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS_ANYTHING(heap.top()); + TS_ASSERT_THROWS_ANYTHING(heap.pop()); +#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_EQUALS(heap.begin(), heap.end()); + + BinaryHeap<int>::handle h5 = heap.push(5); + TS_ASSERT(h5 == h5); + TS_ASSERT_EQUALS(heap.top(), 5); + TS_ASSERT_EQUALS(heap.size(), 1u); + TS_ASSERT(! heap.empty()); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*h5, 5); + TS_ASSERT_EQUALS(*heap.begin(), 5); + TS_ASSERT_THROWS_NOTHING(heap.erase(h5)); + TS_ASSERT(heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 0u); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS_ANYTHING(heap.top()); + TS_ASSERT_THROWS_ANYTHING(heap.pop()); +#endif /* CVC4_ASSERTIONS */ + + // Next test a heap of 4 elements + h5 = heap.push(5); + BinaryHeap<int>::handle h3 = heap.push(3); + BinaryHeap<int>::handle h10 = heap.push(10); + BinaryHeap<int>::handle h2 = heap.push(2); + TS_ASSERT_DIFFERS(h5, h3); + TS_ASSERT_DIFFERS(h5, h10); + TS_ASSERT_DIFFERS(h5, h2); + TS_ASSERT_DIFFERS(h3, h10); + TS_ASSERT_DIFFERS(h3, h2); + TS_ASSERT_DIFFERS(h10, h2); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*heap.begin(), 10); + TS_ASSERT_EQUALS(*h2, 2); + TS_ASSERT_EQUALS(*h3, 3); + TS_ASSERT_EQUALS(*h5, 5); + TS_ASSERT_EQUALS(*h10, 10); + TS_ASSERT_EQUALS(heap.top(), 10); + // test the iterator (note the order of elements isn't guaranteed!) + BinaryHeap<int>::const_iterator i = heap.begin(); + TS_ASSERT_DIFFERS(i, heap.end()); + TS_ASSERT_THROWS_NOTHING(*i++); + TS_ASSERT_DIFFERS(i, heap.end()); + TS_ASSERT_THROWS_NOTHING(*i++); + TS_ASSERT_DIFFERS(i, heap.end()); + TS_ASSERT_THROWS_NOTHING(*i++); + TS_ASSERT_DIFFERS(i, heap.end()); + TS_ASSERT_THROWS_NOTHING(*i++); + TS_ASSERT_EQUALS(i, heap.end()); + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 4u); + TS_ASSERT_THROWS_NOTHING(heap.pop()); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*heap.begin(), 5); + TS_ASSERT_EQUALS(heap.top(), 5); + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 3u); + TS_ASSERT_THROWS_NOTHING(heap.pop()); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*heap.begin(), 3); + TS_ASSERT_EQUALS(heap.top(), 3); + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 2u); + TS_ASSERT_THROWS_NOTHING(heap.pop()); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*heap.begin(), 2); + TS_ASSERT_EQUALS(heap.top(), 2); + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 1u); + TS_ASSERT_THROWS_NOTHING(heap.pop()); + TS_ASSERT_EQUALS(heap.begin(), heap.end()); + TS_ASSERT(heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 0u); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS_ANYTHING(heap.top()); + TS_ASSERT_THROWS_ANYTHING(heap.pop()); +#endif /* CVC4_ASSERTIONS */ + + // Now with a few updates + h5 = heap.push(5); + h3 = heap.push(3); + h10 = heap.push(10); + h2 = heap.push(2); + + TS_ASSERT_EQUALS(*h5, 5); + TS_ASSERT_EQUALS(*h3, 3); + TS_ASSERT_EQUALS(*h10, 10); + TS_ASSERT_EQUALS(*h2, 2); + + TS_ASSERT_EQUALS(heap.top(), 10); + heap.update(h10, -10); + TS_ASSERT_EQUALS(*h10, -10); + TS_ASSERT_EQUALS(heap.top(), 5); + heap.erase(h2); + TS_ASSERT_EQUALS(heap.top(), 5); + heap.update(h3, -20); + TS_ASSERT_EQUALS(*h3, -20); + TS_ASSERT_EQUALS(heap.top(), 5); + heap.pop(); + TS_ASSERT_EQUALS(heap.top(), -10); + heap.pop(); + TS_ASSERT_EQUALS(heap.top(), -20); + } + + struct Elem { + int x; + Elem(int y) : x(y) {} + };/* struct Elem */ + + struct Cmp { + bool valid; + Cmp() : valid(false) {} + Cmp(int x) : valid(true) {} + bool operator()(Elem x, Elem y) const { + // ensure BinaryHeap<> calls our Cmp instance and not some fresh one + TS_ASSERT(valid); + return x.x > y.x; + } + };/* struct Cmp */ + + void testLargeHeap() { + BinaryHeap<Elem, Cmp> heap(Cmp(0)); + vector<BinaryHeap<Elem, Cmp>::handle> handles; + TS_ASSERT(heap.empty()); + for(int x = 0; x < 1000; ++x) { + handles.push_back(heap.push(Elem(x))); + } + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 1000u); + heap.update(handles[100], 50); + heap.update(handles[100], -50); + heap.update(handles[600], 2); + heap.update(handles[184], -9); + heap.update(handles[987], 9555); + heap.update(handles[672], -1003); + heap.update(handles[781], 481); + heap.update(handles[9], 9619); + heap.update(handles[919], 111); + TS_ASSERT_EQUALS(heap.size(), 1000u); + heap.erase(handles[10]); + TS_ASSERT_EQUALS(heap.size(), 999u); + TS_ASSERT(!heap.empty()); + handles.clear(); + Elem last = heap.top(); + for(int x = 0; x < 800; ++x) { + TS_ASSERT_LESS_THAN_EQUALS(last.x, heap.top().x); + last = heap.top(); + heap.pop(); + TS_ASSERT_EQUALS(heap.size(), 998u - x); + TS_ASSERT(!heap.empty()); + } + TS_ASSERT_EQUALS(heap.size(), 199u); + for(int x = 0; x < 10000; ++x) { + // two-thirds of the time insert large value, one-third insert small value + handles.push_back(heap.push(Elem(4 * ((x % 3 == 0) ? -x : x)))); + if(x % 10 == 6) { + // also every tenth insert somewhere in the middle + handles.push_back(heap.push(Elem(x / 10))); + } + // change a few + heap.update(handles[x / 10], 4 * (*handles[x / 10]).x); + heap.update(handles[x / 105], (*handles[x / 4]).x - 294); + heap.update(handles[x / 33], 6 * (*handles[x / 82]).x / 5 - 1); + TS_ASSERT_EQUALS(heap.size(), size_t(x) + ((x + 4) / 10) + 200); + } + TS_ASSERT_EQUALS(heap.size(), 11199u); + TS_ASSERT(!heap.empty()); + last = heap.top(); + while(!heap.empty()) { + TS_ASSERT_LESS_THAN_EQUALS(last.x, heap.top().x); + last = heap.top(); + heap.pop(); + } + TS_ASSERT(heap.empty()); + heap.clear(); + TS_ASSERT(heap.empty()); + } + +};/* class BinaryHeapBlack */ |