#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:
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;
/** 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()
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;
++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;
};/* 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(); }
return (d_heap.front())->d_elem;
}
+private:
void update(handle h){
Assert(!empty());
Assert(debugHandle(h));
}
}
+public:
void update(handle h, const T& val){
Assert(!empty());
Assert(debugHandle(h));
/** (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);
return d_cmp(a, b);
}
-private:
inline static size_t parent(size_t p){
Assert(p != root());
return (p-1)/2;
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;
}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;
}
// 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 ){
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 */
--- /dev/null
+/********************* */
+/*! \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 */
projects / cvc5.git / commitdiff