Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ConsecutiveUint64DynamicPriorityQueue.h
Go to the documentation of this file.
1#pragma once
2
3#include <algorithm>
4#include <cstdint>
5#include <numeric>
6#include <vector>
7
8#include "storm-config.h"
9
11
12namespace storm {
13namespace storage {
14
15template<typename Compare = std::less<uint64_t>>
17 public:
18 typedef uint64_t T;
19 typedef std::vector<T> Container;
20
21 private:
22 Container container;
23 Compare compare;
24
25 std::vector<uint64_t> positions;
26
27 public:
28 explicit ConsecutiveUint64DynamicPriorityQueue(uint64_t numberOfIntegers, Compare const& compare)
29 : container(numberOfIntegers), compare(compare), positions(numberOfIntegers) {
30 std::iota(container.begin(), container.end(), 0);
31 std::make_heap(container.begin(), container.end(), compare);
32 updatePositions();
33 }
34
35 void increase(uint64_t element) {
36 uint64_t position = positions[element];
37 if (position >= container.size()) {
38 return;
39 }
40
41 uint64_t parentPosition = (position - 1) / 2;
42 while (position > 0 && compare(container[parentPosition], container[position])) {
43 std::swap(positions[container[parentPosition]], positions[container[position]]);
44 std::swap(container[parentPosition], container[position]);
45
46 position = parentPosition;
47 parentPosition = (position - 1) / 2;
48 }
49
50 STORM_LOG_ASSERT(std::is_heap(container.begin(), container.end(), compare), "Heap structure lost.");
51 }
52
53 bool contains(uint64_t element) const {
54 return positions[element] < container.size();
55 }
56
57 bool empty() const {
58 return container.empty();
59 }
60
61 std::size_t size() const {
62 return container.size();
63 }
64
65 const T& top() const {
66 return container.front();
67 }
68
69 void push(uint64_t const& item) {
70 container.emplace_back(item);
71 std::push_heap(container.begin(), container.end(), compare);
72 }
73
74 void pop() {
75 if (container.size() > 1) {
76 // Swap max element to back.
77 std::swap(positions[container.front()], positions[container.back()]);
78 std::swap(container.front(), container.back());
79 container.pop_back();
80
81 // Sift down the element from the top.
82 uint64_t positionToSift = 0;
83 uint64_t child = 2 * positionToSift + 1;
84
85 while (child < container.size()) {
86 if (child + 1 < container.size()) {
87 // Figure out larger child.
88 child = compare(container[child], container[child + 1]) ? child + 1 : child;
89
90 // Check if we need to sift down.
91 if (compare(container[positionToSift], container[child])) {
92 std::swap(positions[container[positionToSift]], positions[container[child]]);
93 std::swap(container[positionToSift], container[child]);
94
95 positionToSift = child;
96 child = 2 * positionToSift + 1;
97 } else {
98 break;
99 }
100 } else if (compare(container[positionToSift], container[child])) {
101 std::swap(positions[container[positionToSift]], positions[container[child]]);
102 std::swap(container[positionToSift], container[child]);
103
104 positionToSift = child;
105 child = 2 * positionToSift + 1;
106 } else {
107 break;
108 }
109 }
110
111 } else {
112 container.pop_back();
113 }
114
115 STORM_LOG_ASSERT(std::is_heap(container.begin(), container.end(), compare), "Heap structure lost.");
116 }
117
119 T item = top();
120 pop();
121 return item;
122 }
123
124 private:
125 bool checkPositions() const {
126 uint64_t position = 0;
127 for (auto const& e : container) {
128 if (positions[e] != position) {
129 return false;
130 }
131 ++position;
132 }
133 return true;
134 }
135
136 void updatePositions() {
137 uint64_t position = 0;
138 for (auto const& e : container) {
139 positions[e] = position;
140 ++position;
141 }
142 }
143};
144} // namespace storage
145} // namespace storm
ConsecutiveUint64DynamicPriorityQueue(uint64_t numberOfIntegers, Compare const &compare)
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:9