Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BitVector.cpp
Go to the documentation of this file.
1#include <algorithm>
2#include <bit>
3#include <bitset>
4#include <iostream>
5
7
11
12// Uncomment the following line to enable additional assertions for debugging bitvector operations.
13// #define ASSERT_BITVECTOR
14
15namespace storm {
16namespace storage {
17
18BitVector::const_iterator::const_iterator() : dataPtr(nullptr), currentIndex(0), endIndex(0) {};
19
20BitVector::const_iterator::const_iterator(uint64_t const* dataPtr, uint64_t startIndex, uint64_t endIndex, bool setOnFirstBit)
21 : dataPtr(dataPtr), endIndex(endIndex) {
22 if (setOnFirstBit) {
23 // Set the index of the first set bit in the vector.
24 currentIndex = getNextIndexWithValue<true>(dataPtr, startIndex, endIndex);
25 } else {
26 currentIndex = startIndex;
27 }
28}
29
30BitVector::const_iterator::const_iterator(const_iterator const& other) : dataPtr(other.dataPtr), currentIndex(other.currentIndex), endIndex(other.endIndex) {
31 // Intentionally left empty.
32}
33
35 // Only assign contents if the source and target are not the same.
36 if (this != &other) {
37 dataPtr = other.dataPtr;
38 currentIndex = other.currentIndex;
39 endIndex = other.endIndex;
40 }
41 return *this;
42}
43
45 currentIndex = getNextIndexWithValue<true>(dataPtr, ++currentIndex, endIndex);
46 return *this;
47}
48
50 BitVector::const_iterator copy{*this};
51 ++(*this);
52 return copy;
53}
54
56 for (size_t i = 0; i < n; ++i) {
57 currentIndex = getNextIndexWithValue<true>(dataPtr, ++currentIndex, endIndex);
58 }
59 return *this;
60}
61
63 return currentIndex;
64}
65
67 return currentIndex != other.currentIndex;
68}
69
71 return currentIndex == other.currentIndex;
72}
73
74BitVector::const_reverse_iterator::const_reverse_iterator() : dataPtr(nullptr), currentIndex(0), lowerBound(0) {};
75
76BitVector::const_reverse_iterator::const_reverse_iterator(uint64_t const* dataPtr, uint64_t upperBound, uint64_t lowerBound, bool setOnFirstBit)
77 : dataPtr(dataPtr), lowerBound(lowerBound) {
78 if (setOnFirstBit) {
79 // Set the index of the first set bit in the vector.
80 currentIndex = getNextIndexWithValue<true, true>(dataPtr, lowerBound, upperBound);
81 } else {
82 currentIndex = upperBound;
83 }
84}
85
87 : dataPtr(other.dataPtr), currentIndex(other.currentIndex), lowerBound(other.lowerBound) {
88 // Intentionally left empty.
89}
90
92 // Only assign contents if the source and target are not the same.
93 if (this != &other) {
94 dataPtr = other.dataPtr;
95 currentIndex = other.currentIndex;
96 lowerBound = other.lowerBound;
97 }
98 return *this;
99}
100
102 currentIndex = getNextIndexWithValue<true, true>(dataPtr, lowerBound, --currentIndex);
103 return *this;
104}
110
112 for (size_t i = 0; i < n; ++i) {
113 currentIndex = getNextIndexWithValue<true, true>(dataPtr, lowerBound, --currentIndex);
114 }
115 return *this;
116}
117
119 return currentIndex - 1; // the stored index is off-by-one!
120}
121
123 return currentIndex != other.currentIndex;
124}
125
127 return currentIndex == other.currentIndex;
128}
129
130BitVector::BitVector() : bitCount(0), buckets(nullptr) {
131 // Intentionally left empty.
132}
133
134BitVector::BitVector(uint64_t length, bool init) : bitCount(length), buckets(nullptr) {
135 // Compute the correct number of buckets needed to store the given number of bits.
136 uint64_t bucketCount = length >> 6;
137 if ((length & mod64mask) != 0) {
138 ++bucketCount;
139 }
140
141 // Initialize the storage with the required values.
142 if (init) {
143 buckets = new uint64_t[bucketCount];
144 std::fill_n(buckets, bucketCount, -1ull);
145 truncateLastBucket();
146 } else {
147 buckets = new uint64_t[bucketCount]();
148 }
149}
150
152 delete[] buckets;
153}
154
155template<typename InputIterator>
156BitVector::BitVector(uint64_t length, InputIterator begin, InputIterator end) : BitVector(length) {
157 set(begin, end);
158}
159
160BitVector::BitVector(uint64_t length, std::vector<uint64_t> setEntries) : BitVector(length, setEntries.begin(), setEntries.end()) {
161 // Intentionally left empty.
162}
163
164BitVector::BitVector(uint64_t bucketCount, uint64_t bitCount) : bitCount(bitCount), buckets(nullptr) {
165 STORM_LOG_ASSERT((bucketCount << 6) == bitCount, "Bit count does not match number of buckets.");
166 buckets = new uint64_t[bucketCount]();
167}
168
169BitVector::BitVector(BitVector const& other) : bitCount(other.bitCount), buckets(nullptr) {
170 buckets = new uint64_t[other.bucketCount()];
171 std::copy_n(other.buckets, other.bucketCount(), buckets);
172}
173
175 // Only perform the assignment if the source and target are not identical.
176 if (this != &other) {
177 if (buckets && bucketCount() != other.bucketCount()) {
178 delete[] buckets;
179 buckets = nullptr;
180 }
181 bitCount = other.bitCount;
182 if (!buckets) {
183 buckets = new uint64_t[other.bucketCount()];
184 }
185 std::copy_n(other.buckets, other.bucketCount(), buckets);
186 }
187 return *this;
188}
189
190bool BitVector::operator<(BitVector const& other) const {
191 if (this->size() < other.size()) {
192 return true;
193 } else if (this->size() > other.size()) {
194 return false;
195 }
196
197 uint64_t* first1 = this->buckets;
198 uint64_t* last1 = this->buckets + this->bucketCount();
199 uint64_t* first2 = other.buckets;
200
201 for (; first1 != last1; ++first1, ++first2) {
202 if (*first1 < *first2) {
203 return true;
204 } else if (*first1 > *first2) {
205 return false;
206 }
207 }
208 return false;
209}
210
211BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), buckets(other.buckets) {
212 other.bitCount = 0;
213 other.buckets = nullptr;
214}
215
217 // Only perform the assignment if the source and target are not identical.
218 if (this != &other) {
219 bitCount = other.bitCount;
220 other.bitCount = 0;
221 delete[] this->buckets;
222 this->buckets = other.buckets;
223 other.buckets = nullptr;
224 }
225
226 return *this;
227}
228
229bool BitVector::operator==(BitVector const& other) const {
230 // If the lengths of the vectors do not match, they are considered unequal.
231 if (this->bitCount != other.bitCount)
232 return false;
233
234 // If the lengths match, we compare the buckets one by one.
235 return std::equal(this->buckets, this->buckets + this->bucketCount(), other.buckets);
236}
237
238bool BitVector::operator!=(BitVector const& other) const {
239 return !(*this == other);
240}
241
242void BitVector::set(uint64_t index, bool value) {
243 STORM_LOG_ASSERT(index < bitCount, "Invalid call to BitVector::set: written index " << index << " out of bounds.");
244 uint64_t bucket = index >> 6;
245
246 uint64_t mask = 1ull << (63 - (index & mod64mask));
247 if (value) {
248 buckets[bucket] |= mask;
249 } else {
250 buckets[bucket] &= ~mask;
251 }
252}
253
254template<typename InputIterator>
255void BitVector::set(InputIterator begin, InputIterator end, bool value) {
256 for (InputIterator it = begin; it != end; ++it) {
257 this->set(*it, value);
258 }
259}
260
261bool BitVector::operator[](uint64_t index) const {
262 uint64_t bucket = index >> 6;
263 uint64_t mask = 1ull << (63 - (index & mod64mask));
264 return (this->buckets[bucket] & mask) == mask;
265}
266
267bool BitVector::get(uint64_t index) const {
268 STORM_LOG_ASSERT(index < bitCount, "Invalid call to BitVector::get: read index " << index << " out of bounds.");
269 return (*this)[index];
270}
271
272void BitVector::resize(uint64_t newLength, bool init) {
273 if (newLength > bitCount) {
274 uint64_t newBucketCount = newLength >> 6;
275 if ((newLength & mod64mask) != 0) {
276 ++newBucketCount;
277 }
278
279 if (newBucketCount > this->bucketCount()) {
280 uint64_t* newBuckets = new uint64_t[newBucketCount];
281 std::copy_n(buckets, this->bucketCount(), newBuckets);
282 if (init) {
283 if (this->bucketCount() > 0) {
284 newBuckets[this->bucketCount() - 1] |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
285 }
286 std::fill_n(newBuckets + this->bucketCount(), newBucketCount - this->bucketCount(), -1ull);
287 } else {
288 std::fill_n(newBuckets + this->bucketCount(), newBucketCount - this->bucketCount(), 0);
289 }
290 delete[] buckets;
291 buckets = newBuckets;
292 bitCount = newLength;
293 } else {
294 // If the underlying storage does not need to grow, we have to insert the missing bits.
295 if (init) {
296 buckets[this->bucketCount() - 1] |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
297 }
298 bitCount = newLength;
299 }
300 truncateLastBucket();
301 } else {
302 uint64_t newBucketCount = newLength >> 6;
303 if ((newLength & mod64mask) != 0) {
304 ++newBucketCount;
305 }
306
307 // If the number of buckets needs to be reduced, we resize it now. Otherwise, we can just truncate the
308 // last bucket.
309 if (newBucketCount < this->bucketCount()) {
310 uint64_t* newBuckets = new uint64_t[newBucketCount];
311 std::copy_n(buckets, newBucketCount, newBuckets);
312 delete[] buckets;
313 buckets = newBuckets;
314 bitCount = newLength;
315 }
316 bitCount = newLength;
317 truncateLastBucket();
318 }
319}
320
321void BitVector::concat(BitVector const& other) {
322 STORM_LOG_ASSERT(size() % 64 == 0, "We expect the length of the left bitvector to be a multiple of 64.");
323 // TODO this assumption is due to the implementation of BitVector::set().
324 BitVector tmp(size() + other.size());
325 tmp.set(size(), other);
326 resize(size() + other.size(), false);
327 *this |= tmp;
328}
329
330void BitVector::expandSize(bool init) {
331 // size_t oldBitCount = bitCount;
332 bitCount = bucketCount() * 64;
333 if (init) {
334 STORM_LOG_ASSERT(false, "Not implemented as we do not foresee any need");
335 }
336}
337
338void BitVector::grow(uint64_t minimumLength, bool init) {
339 if (minimumLength > bitCount) {
340 // We double the bitcount as long as it is less then the minimum length.
341 uint64_t newLength = std::max(static_cast<uint64_t>(64), bitCount);
342 // Note that newLength has to be initialized with a non-zero number.
343 while (newLength < minimumLength) {
344 newLength = newLength << 1;
345 }
346 resize(newLength, init);
347 }
348}
349
351 STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
352 BitVector result(bitCount);
353 std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets,
354 [](uint64_t const& a, uint64_t const& b) { return a & b; });
355 return result;
356}
357
359 STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
360 std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, this->buckets,
361 [](uint64_t const& a, uint64_t const& b) { return a & b; });
362 return *this;
363}
364
366 STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
367 BitVector result(bitCount);
368 std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets,
369 [](uint64_t const& a, uint64_t const& b) { return a | b; });
370 return result;
371}
372
374 STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
375 std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, this->buckets,
376 [](uint64_t const& a, uint64_t const& b) { return a | b; });
377 return *this;
378}
379
381 STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
382 BitVector result(bitCount);
383 std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets,
384 [](uint64_t const& a, uint64_t const& b) { return a ^ b; });
385 result.truncateLastBucket();
386 return result;
387}
388
390 STORM_LOG_ASSERT(bitCount == filter.bitCount, "Length of the bit vectors does not match.");
391
392 BitVector result(filter.getNumberOfSetBits());
393
394 // If the current bit vector has not too many elements compared to the given bit vector we prefer iterating
395 // over its elements.
396 if (filter.getNumberOfSetBits() / 10 < this->getNumberOfSetBits()) {
397 uint64_t position = 0;
398 for (auto bit : filter) {
399 if ((*this)[bit]) {
400 result.set(position);
401 }
402 ++position;
403 }
404 } else {
405 // If the given bit vector had much fewer elements, we iterate over its elements and accept calling the
406 // more costly operation getNumberOfSetBitsBeforeIndex on the current bit vector.
407 for (auto bit : (*this)) {
408 if (filter[bit]) {
409 result.set(filter.getNumberOfSetBitsBeforeIndex(bit));
410 }
411 }
412 }
413
414 return result;
415}
416
418 BitVector result(this->bitCount);
419 std::transform(this->buckets, this->buckets + this->bucketCount(), result.buckets, [](uint64_t const& a) { return ~a; });
420 result.truncateLastBucket();
421 return result;
422}
423
425 std::transform(this->buckets, this->buckets + this->bucketCount(), this->buckets, [](uint64_t const& a) { return ~a; });
426 truncateLastBucket();
427}
428
430 uint64_t firstUnsetIndex = getNextUnsetIndex(0);
431
432 // If there is no unset index, we clear the whole vector
433 if (firstUnsetIndex == this->bitCount) {
434 this->clear();
435 } else {
436 // All previous buckets have to be set to zero
437 uint64_t bucketIndex = firstUnsetIndex >> 6;
438 std::fill_n(buckets, bucketIndex, 0);
439
440 // modify the bucket in which the unset entry lies in
441 uint64_t& bucket = this->buckets[bucketIndex];
442 uint64_t indexInBucket = firstUnsetIndex & mod64mask;
443 if (indexInBucket > 0) {
444 // Clear all bits before the index
445 uint64_t mask = ~(-1ull << (64 - indexInBucket));
446 bucket &= mask;
447 }
448
449 // Set the bit at the index
450 uint64_t mask = 1ull << (63 - indexInBucket);
451 bucket |= mask;
452 }
453}
454
456 STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
457
458 BitVector result(bitCount);
459 std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets,
460 [](uint64_t const& a, uint64_t const& b) { return (~a | b); });
461 result.truncateLastBucket();
462 return result;
463}
464
465bool BitVector::isSubsetOf(BitVector const& other) const {
466 STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
467
468 uint64_t const* it1 = buckets;
469 uint64_t const* ite1 = buckets + bucketCount();
470 uint64_t const* it2 = other.buckets;
471
472 for (; it1 != ite1; ++it1, ++it2) {
473 if ((*it1 & *it2) != *it1) {
474 return false;
475 }
476 }
477 return true;
478}
479
480bool BitVector::isDisjointFrom(BitVector const& other) const {
481 STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
482
483 uint64_t const* it1 = buckets;
484 uint64_t const* ite1 = buckets + bucketCount();
485 uint64_t const* it2 = other.buckets;
486
487 for (; it1 != ite1; ++it1, ++it2) {
488 if ((*it1 & *it2) != 0) {
489 return false;
490 }
491 }
492 return true;
493}
494
495bool BitVector::matches(uint64_t bitIndex, BitVector const& other) const {
496 STORM_LOG_ASSERT((bitIndex & mod64mask) == 0, "Bit index must be a multiple of 64.");
497 STORM_LOG_ASSERT(other.size() <= this->size() - bitIndex, "Bit vector argument is too long.");
498
499 // Compute the first bucket that needs to be checked and the number of buckets.
500 uint64_t index = bitIndex >> 6;
501
502 uint64_t const* first1 = buckets + index;
503 uint64_t const* first2 = other.buckets;
504 uint64_t const* last2 = other.buckets + other.bucketCount();
505
506 for (; first2 != last2; ++first1, ++first2) {
507 if (*first1 != *first2) {
508 return false;
509 }
510 }
511 return true;
512}
513
514BitVector BitVector::permute(std::vector<uint64_t> const& inversePermutation) const {
515 BitVector result(this->size());
516 for (uint64_t i = 0; i < this->size(); ++i) {
517 if (this->get(inversePermutation[i])) {
518 result.set(i, true);
519 }
520 }
521 return result;
522}
523
524BitVector BitVector::permuteGroupedVector(const std::vector<uint64_t>& inversePermutation, const std::vector<uint64_t>& rowGroupIndices) const {
525 STORM_LOG_ASSERT(inversePermutation.size() == rowGroupIndices.size() - 1, "Inverse permutation and row group indices do not match.");
526 BitVector result(this->size(), false);
527 uint64_t targetIndex = 0u;
528 for (auto const sourceGroupIndex : inversePermutation) {
529 for (uint64_t sourceIndex = rowGroupIndices[sourceGroupIndex]; sourceIndex < rowGroupIndices[sourceGroupIndex + 1]; ++sourceIndex, ++targetIndex) {
530 if (this->get(sourceIndex)) {
531 result.set(targetIndex, true);
532 }
533 }
534 }
535 STORM_LOG_ASSERT(targetIndex == result.size(), "Target index does not match the size of the result.");
536 return result;
537}
538
539void BitVector::set(uint64_t bitIndex, BitVector const& other) {
540 STORM_LOG_ASSERT((bitIndex & mod64mask) == 0, "Bit index must be a multiple of 64.");
541 STORM_LOG_ASSERT(other.size() <= this->size() - bitIndex, "Bit vector argument is too long.");
542
543 // Compute the first bucket that needs to be checked and the number of buckets.
544 uint64_t index = bitIndex >> 6;
545
546 uint64_t* first1 = buckets + index;
547 uint64_t const* first2 = other.buckets;
548 uint64_t const* last2 = other.buckets + other.bucketCount();
549
550 for (; first2 != last2; ++first1, ++first2) {
551 *first1 = *first2;
552 }
553}
554
555void BitVector::setMultiple(uint64_t bitIndex, uint64_t nrOfBits, bool newValue) {
556 // TODO we may want to optimize this code for large nrs of bits.
557 uint64_t endPos = std::min(bitIndex + nrOfBits, bitCount);
558 for (uint64_t tmpIndex = bitIndex; tmpIndex < endPos; ++tmpIndex) {
559 set(tmpIndex, newValue);
560 }
561}
562
563storm::storage::BitVector BitVector::get(uint64_t bitIndex, uint64_t numberOfBits) const {
564 uint64_t numberOfBuckets = numberOfBits >> 6;
565 uint64_t index = bitIndex >> 6;
566 STORM_LOG_ASSERT(index + numberOfBuckets <= this->bucketCount(), "Argument is out-of-range.");
567
568 storm::storage::BitVector result(numberOfBuckets, numberOfBits);
569 std::copy(this->buckets + index, this->buckets + index + numberOfBuckets, result.buckets);
570 result.truncateLastBucket();
571 return result;
572}
573
574uint64_t BitVector::getAsInt(uint64_t bitIndex, uint64_t numberOfBits) const {
575 if (numberOfBits == 0) { // It is necessary to catch this case as we might have an empty bitvector (i.e. uninitialized buckets).
576 return 0;
577 }
578 STORM_LOG_ASSERT(numberOfBits <= 64, "Number of bits must be <= 64.");
579 uint64_t const firstBucket = bitIndex >> 6; // the bucket where the value starts
580 uint8_t const bitIndexInFirstBucket = bitIndex & mod64mask; // the index within that bucket
581 uint8_t const availableBitsInFirstBucket = static_cast<uint8_t>(64 - bitIndexInFirstBucket); // number of available bits in that bucket
582
583 // First get the result in the form rr...rrxx...xx (r = result, x = garbage)
584 uint64_t result = buckets[firstBucket] << bitIndexInFirstBucket;
585 // We might have to look at the next bucket, too
586 if (availableBitsInFirstBucket < numberOfBits) {
587 result |= buckets[firstBucket + 1] >> availableBitsInFirstBucket;
588 }
589 // Get rid of the garbage bits and return the result.
590 return result >> (64 - numberOfBits);
591}
592
593uint64_t BitVector::getTwoBitsAligned(uint64_t bitIndex) const {
594 // Check whether it is aligned.
595 STORM_LOG_ASSERT(bitIndex % 64 != 63, "Bits not aligned.");
596 uint64_t bucket = bitIndex >> 6;
597 uint64_t bitIndexInBucket = bitIndex & mod64mask;
598
599 uint64_t mask;
600 if (bitIndexInBucket == 0) {
601 mask = -1ull;
602 } else {
603 mask = (1ull << (64 - bitIndexInBucket)) - 1ull;
604 }
605
606 if (bitIndexInBucket < 62) { // bitIndexInBucket + 2 < 64
607 // If the value stops before the end of the bucket, we need to erase some lower bits.
608 mask &= ~((1ull << (62 - (bitIndexInBucket))) - 1ull);
609 return (buckets[bucket] & mask) >> (62 - bitIndexInBucket);
610 } else {
611 // In this case, it suffices to take the current mask.
612 return buckets[bucket] & mask;
613 }
614}
615
616void BitVector::setFromInt(uint64_t bitIndex, uint64_t numberOfBits, uint64_t value) {
617 STORM_LOG_ASSERT(numberOfBits <= 64, "Number of bits must be <= 64.");
618 STORM_LOG_ASSERT(numberOfBits == 64 || (value >> numberOfBits) == 0,
619 "Integer value (" << value << ") too large to fit in the given number of bits (" << numberOfBits << ").");
620
621 uint64_t bucket = bitIndex >> 6;
622 uint64_t bitIndexInBucket = bitIndex & mod64mask;
623
624 uint64_t mask;
625 if (bitIndexInBucket == 0) {
626 mask = -1ull;
627 } else {
628 mask = (1ull << (64 - bitIndexInBucket)) - 1ull;
629 }
630
631 if (bitIndexInBucket + numberOfBits < 64) {
632 // If the value stops before the end of the bucket, we need to erase some lower bits.
633 mask &= ~((1ull << (64 - (bitIndexInBucket + numberOfBits))) - 1ull);
634 buckets[bucket] = (buckets[bucket] & ~mask) | (value << (64 - (bitIndexInBucket + numberOfBits)));
635 } else if (bitIndexInBucket + numberOfBits > 64) {
636 // Write the part of the value that falls into the first bucket.
637 buckets[bucket] = (buckets[bucket] & ~mask) | (value >> (numberOfBits + (bitIndexInBucket - 64)));
638 ++bucket;
639
640 // Compute the remaining number of bits.
641 numberOfBits -= (64 - bitIndexInBucket);
642
643 // Shift the bits of the value such that the already set bits disappear.
644 value <<= (64 - numberOfBits);
645
646 // Put the remaining bits in their place.
647 mask = ((1ull << (64 - numberOfBits)) - 1ull);
648 buckets[bucket] = (buckets[bucket] & mask) | value;
649 } else {
650 buckets[bucket] = (buckets[bucket] & ~mask) | value;
651 }
652}
653
654bool BitVector::empty() const {
655 uint64_t* last = buckets + bucketCount();
656 uint64_t* it = std::find_if(buckets, last, [](uint64_t const& a) { return a != 0; });
657 return it == last;
658}
659
660bool BitVector::full() const {
661 if (bitCount == 0) {
662 return true;
663 }
664 // Check that all buckets except the last one have all bits set.
665 uint64_t* last = buckets + bucketCount() - 1;
666 for (uint64_t const* it = buckets; it < last; ++it) {
667 if (*it != -1ull) {
668 return false;
669 }
670 }
671
672 // Now check whether the relevant bits are set in the last bucket.
673 uint64_t mask = ~((1ull << (64 - (bitCount & mod64mask))) - 1ull);
674 if ((*last & mask) != mask) {
675 return false;
676 }
677 return true;
678}
679
681 std::fill_n(buckets, this->bucketCount(), 0);
682}
683
685 std::fill_n(buckets, this->bucketCount(), -1ull);
686 truncateLastBucket();
687}
688
690 return getNumberOfSetBitsBeforeIndex(bitCount);
691}
692
693uint64_t BitVector::getNumberOfSetBitsBeforeIndex(uint64_t index) const {
694 STORM_LOG_ASSERT(index <= bitCount, "Invalid call to BitVector::getNumberOfSetBitsBeforeIndex: read index " << index << " out of bounds.");
695 uint64_t const lastBucketIndex = index >> 6;
696 uint64_t result = 0;
697
698 // First, count all full buckets.
699 for (uint64_t i = 0; i < lastBucketIndex; ++i) {
700 result += std::popcount(buckets[i]);
701 }
702
703 // Now check if we have to count part of a bucket.
704 uint8_t const endIndexInLastBucket = index & mod64mask;
705 if (endIndexInLastBucket != 0) {
706 result += std::popcount(buckets[lastBucketIndex] >> (64 - endIndexInLastBucket));
707 }
708
709 return result;
710}
711
712std::vector<uint64_t> BitVector::getNumberOfSetBitsBeforeIndices() const {
713 std::vector<uint64_t> bitsSetBeforeIndices;
714 bitsSetBeforeIndices.reserve(this->size());
715 uint64_t lastIndex = 0;
716 uint64_t currentNumberOfSetBits = 0;
717 for (auto index : *this) {
718 while (lastIndex <= index) {
719 bitsSetBeforeIndices.push_back(currentNumberOfSetBits);
720 ++lastIndex;
721 }
722 ++currentNumberOfSetBits;
723 }
724 return bitsSetBeforeIndices;
725}
726
728 return getNumberOfSetBits() == 1;
729}
730
731size_t BitVector::size() const {
732 return static_cast<size_t>(bitCount);
733}
734
735std::size_t BitVector::getSizeInBytes() const {
736 return sizeof(*this) + sizeof(uint64_t) * bucketCount();
737}
738
740 return const_iterator(buckets, 0, bitCount);
741}
742
743BitVector::const_iterator BitVector::begin(uint64_t lowerBound) const {
744 return const_iterator(buckets, lowerBound, bitCount);
745}
746
748 return const_iterator(buckets, bitCount, bitCount, false);
749}
750
755 return const_reverse_iterator(buckets, upperBound);
756}
757
759 return const_reverse_iterator(buckets, 0ull, 0ull, false);
760}
761
762uint64_t BitVector::getNextSetIndex(uint64_t startingIndex) const {
763 return getNextIndexWithValue<true>(buckets, startingIndex, bitCount);
764}
765
766uint64_t BitVector::getNextUnsetIndex(uint64_t startingIndex) const {
767#ifdef ASSERT_BITVECTOR
768 STORM_LOG_ASSERT(getNextIndexWithValue<false>(buckets, startingIndex, bitCount) == (~(*this)).getNextSetIndex(startingIndex),
769 "The result is inconsistent with the next set index of the complement of this bitvector");
770#endif
771 return getNextIndexWithValue<false>(buckets, startingIndex, bitCount);
772}
773
774uint64_t BitVector::getStartOfZeroSequenceBefore(uint64_t endIndex) const {
775 return getNextIndexWithValue<true, true>(buckets, 0, endIndex);
776}
777
778uint64_t BitVector::getStartOfOneSequenceBefore(uint64_t endIndex) const {
779#ifdef ASSERT_BITVECTOR
780 STORM_LOG_ASSERT((getNextIndexWithValue<false, true>(buckets, 0, endIndex) == (~(*this)).getStartOfZeroSequenceBefore(endIndex)),
781 "The result is inconsistent with the next set index of the complement of this bitvector");
782#endif
783 return getNextIndexWithValue<false, true>(buckets, 0, endIndex);
784}
785
786template<bool Value, bool Backward>
787uint64_t BitVector::getNextIndexWithValue(uint64_t const* dataPtr, uint64_t startingIndex, uint64_t endIndex) {
788 if (startingIndex >= endIndex) {
789 return Backward ? startingIndex : endIndex;
790 }
791
792 uint64_t currentBucketIndexOffset = Backward ? endIndex - 1 : startingIndex;
793 uint_fast8_t currentBitInBucket = currentBucketIndexOffset & mod64mask;
794 uint64_t const* bucketIt = dataPtr + (currentBucketIndexOffset >> 6);
795 currentBucketIndexOffset = (currentBucketIndexOffset >> 6 << 6);
796
797 // Get relevant contents of the first bucket (the one that contains the bit with index currentBucketIndexOffset + currentBitInBucket)
798 uint64_t relevantBitsInBucket;
799 if constexpr (Backward) {
800 relevantBitsInBucket = -1ull << (63 - currentBitInBucket); // 111..111'1'000...000 where the last '1' is at the currentBitInBucket
801 } else {
802 relevantBitsInBucket = -1ull >> currentBitInBucket; // 000..000'1'111..111 where the first '1' is at the currentBitInBucket
803 }
804 uint64_t currentBucket = Value ? (*bucketIt & relevantBitsInBucket) : (*bucketIt | ~relevantBitsInBucket);
805
806 // Find the right bucket
807 if (currentBucket == (Value ? 0ull : -1ull)) {
808 // The first bucket does not contain a bit with the desired value...
809 do {
810 // Move to next bucket (if there is some)
811 if constexpr (Backward) {
812 if (currentBucketIndexOffset <= startingIndex) {
813 // No bucket found!
814 return startingIndex;
815 }
816 --bucketIt;
817 currentBucketIndexOffset -= 64; // does not underflow: currentBucketIndexOffset is greater than startIndex and always a multiple of 64
818 } else {
819 ++bucketIt;
820 currentBucketIndexOffset += 64;
821 if (currentBucketIndexOffset >= endIndex) {
822 // No bucket found!
823 return endIndex;
824 }
825 }
826 // Check if the bucket contains our bit
827 } while ((*bucketIt) == (Value ? 0ull : -1ull));
828 // At this point we have found our bucket, but it is not the first one
829 currentBucket = *bucketIt;
830 currentBitInBucket = Backward ? 63u : 0u; // search within the bucket starting at the last or at the first bit
831 }
832
833 if constexpr (!Value) {
834 currentBucket = ~currentBucket; // invert so that we always search for a '1' from this point
835 }
836 // At this point, currentBucket definitely contains a 1-bit and all bits (Backward ? after : before) the currentBitInBucket are zero
837 STORM_LOG_ASSERT(currentBucket != 0ull, "Bitvector's getNextIndexWithValue method in invalid state.");
838
839#if (defined(__GNUG__) || defined(__clang__))
840 // Use fast and easy builtin functions to find the correct bit index
841 if constexpr (Backward) {
842 // take max since the startIndex might point somewhere into the current bucket so the found bit might come before the startIndex
843 return std::max<uint64_t>(startingIndex,
844 currentBucketIndexOffset + 64ull - __builtin_ctzll(currentBucket)); // make sure to return +1 index after the found 1
845 } else {
846 // take min since the endIndex might point somewhere into the current bucket so the found bit might come after the endIndex
847 return std::min<uint64_t>(endIndex, currentBucketIndexOffset + __builtin_clzll(currentBucket));
848 }
849#else
850 // Find the correct bit index manually
851 uint64_t compareMask = 1ull << (63 - currentBitInBucket); // 000..000'1'000..000 with '1' at currentBitInBucket position
852 while (!static_cast<bool>(currentBucket & compareMask)) {
853 if constexpr (Backward) {
854 compareMask <<= 1ull;
855 --currentBitInBucket;
856 } else {
857 compareMask >>= 1ull;
858 ++currentBitInBucket;
859 }
860 }
861 if constexpr (Backward) {
862 return std::max(startingIndex, currentBucketIndexOffset + currentBitInBucket + 1ull); // make sure to return +1 index after the found 1
863 } else {
864 return std::min(endIndex, currentBucketIndexOffset + currentBitInBucket);
865 }
866#endif
867}
868
869storm::storage::BitVector BitVector::getAsBitVector(uint64_t start, uint64_t length) const {
870 STORM_LOG_ASSERT(start + length <= bitCount, "Invalid range.");
871#ifdef ASSERT_BITVECTOR
872 BitVector original(*this);
873#endif
874 storm::storage::BitVector result(length, false);
875
876 uint64_t offset = start % 64;
877 uint64_t* getBucket = buckets + (start / 64);
878 uint64_t* insertBucket = result.buckets;
879 uint64_t getValue;
880 uint64_t writeValue = 0;
881 uint64_t noBits = 0;
882 if (offset == 0) {
883 // Copy complete buckets
884 for (; noBits + 64 <= length; ++getBucket, ++insertBucket, noBits += 64) {
885 *insertBucket = *getBucket;
886 }
887 } else {
888 // Get first bits up until next bucket
889 getValue = *getBucket;
890 writeValue = (getValue << offset);
891 noBits += (64 - offset);
892 ++getBucket;
893
894 // Get complete buckets
895 for (; noBits + 64 <= length; ++getBucket, ++insertBucket, noBits += 64) {
896 getValue = *getBucket;
897 // Get bits till write bucket is full
898 writeValue |= (getValue >> (64 - offset));
899 *insertBucket = writeValue;
900 // Get bits up until next bucket
901 writeValue = (getValue << offset);
902 }
903 }
904
905 // Write last bits
906 uint64_t remainingBits = length - noBits;
907 STORM_LOG_ASSERT(getBucket != buckets + bucketCount(), "Bucket index incorrect.");
908 // Get remaining bits
909 getValue = (*getBucket >> (64 - remainingBits)) << (64 - remainingBits);
910 STORM_LOG_ASSERT(remainingBits < 64, "Too many remaining bits.");
911 // Write bucket
912 STORM_LOG_ASSERT(insertBucket != result.buckets + result.bucketCount(), "Bucket index incorrect.");
913 if (offset == 0) {
914 *insertBucket = getValue;
915 } else {
916 writeValue |= getValue >> (64 - offset);
917 *insertBucket = writeValue;
918 if (remainingBits > offset) {
919 // Write last bits in new value
920 writeValue = (getValue << offset);
921 ++insertBucket;
922 STORM_LOG_ASSERT(insertBucket != result.buckets + result.bucketCount(), "Bucket index incorrect.");
923 *insertBucket = writeValue;
924 }
925 }
926
927#ifdef ASSERT_BITVECTOR
928 // Check correctness of getter
929 for (uint64_t i = 0; i < length; ++i) {
930 if (result.get(i) != get(start + i)) {
931 STORM_LOG_ERROR("Getting of bits not correct for index " << i);
932 STORM_LOG_ERROR("Getting from " << start << " with length " << length);
933 std::stringstream stream;
934 printBits(stream);
935 stream << '\n';
936 result.printBits(stream);
937 STORM_LOG_ERROR(stream.str());
938 STORM_LOG_ASSERT(false, "Getting of bits not correct.");
939 }
940 }
941 for (uint64_t i = 0; i < bitCount; ++i) {
942 if (i < start || i >= start + length) {
943 if (original.get(i) != get(i)) {
944 STORM_LOG_ERROR("Getting did change bitvector at index " << i);
945 STORM_LOG_ERROR("Getting from " << start << " with length " << length);
946 std::stringstream stream;
947 printBits(stream);
948 stream << '\n';
949 original.printBits(stream);
950 STORM_LOG_ERROR(stream.str());
951 STORM_LOG_ASSERT(false, "Getting of bits not correct.");
952 }
953 }
954 }
955
956#endif
957 return result;
958}
959
960void BitVector::setFromBitVector(uint64_t start, BitVector const& other) {
961#ifdef ASSERT_BITVECTOR
962 BitVector original(*this);
963#endif
964 STORM_LOG_ASSERT(start + other.bitCount <= bitCount, "Range invalid.");
965
966 uint64_t offset = start % 64;
967 uint64_t* insertBucket = buckets + (start / 64);
968 uint64_t* getBucket = other.buckets;
969 uint64_t getValue;
970 uint64_t writeValue = 0;
971 uint64_t noBits = 0;
972 if (offset == 0) {
973 // Copy complete buckets
974 for (; noBits + 64 <= other.bitCount; ++insertBucket, ++getBucket, noBits += 64) {
975 *insertBucket = *getBucket;
976 }
977 } else {
978 // Get first bits up until next bucket
979 getValue = *getBucket;
980 writeValue = (*insertBucket >> (64 - offset)) << (64 - offset);
981 writeValue |= (getValue >> offset);
982 *insertBucket = writeValue;
983 noBits += (64 - offset);
984 ++insertBucket;
985
986 // Get complete buckets
987 for (; noBits + 64 <= other.bitCount; ++insertBucket, noBits += 64) {
988 // Get all remaining bits from other bucket
989 writeValue = getValue << (64 - offset);
990 // Get bits from next bucket
991 ++getBucket;
992 getValue = *getBucket;
993 writeValue |= getValue >> offset;
994 *insertBucket = writeValue;
995 }
996 }
997
998 // Write last bits
999 uint64_t remainingBits = other.bitCount - noBits;
1000 STORM_LOG_ASSERT(remainingBits < 64, "Too many remaining bits.");
1001 STORM_LOG_ASSERT(insertBucket != buckets + bucketCount(), "Bucket index incorrect.");
1002 STORM_LOG_ASSERT(getBucket != other.buckets + other.bucketCount(), "Bucket index incorrect.");
1003 // Get remaining bits of bucket
1004 getValue = *getBucket;
1005 if (offset > 0) {
1006 getValue = getValue << (64 - offset);
1007 }
1008 // Get unchanged part of bucket
1009 writeValue = (*insertBucket << remainingBits) >> remainingBits;
1010 if (remainingBits > offset && offset > 0) {
1011 // Remaining bits do not come from one bucket -> consider next bucket
1012 ++getBucket;
1013 STORM_LOG_ASSERT(getBucket != other.buckets + other.bucketCount(), "Bucket index incorrect.");
1014 getValue |= *getBucket >> offset;
1015 }
1016 // Write completely
1017 writeValue |= getValue;
1018 *insertBucket = writeValue;
1019
1020#ifdef ASSERT_BITVECTOR
1021 // Check correctness of setter
1022 for (uint64_t i = 0; i < other.bitCount; ++i) {
1023 if (other.get(i) != get(start + i)) {
1024 STORM_LOG_ERROR("Setting of bits not correct for index " << i);
1025 STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount);
1026 std::stringstream stream;
1027 printBits(stream);
1028 stream << '\n';
1029 other.printBits(stream);
1030 STORM_LOG_ERROR(stream.str());
1031 STORM_LOG_ASSERT(false, "Setting of bits not correct.");
1032 }
1033 }
1034 for (uint64_t i = 0; i < bitCount; ++i) {
1035 if (i < start || i >= start + other.bitCount) {
1036 if (original.get(i) != get(i)) {
1037 STORM_LOG_ERROR("Setting did change bitvector at index " << i);
1038 STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount);
1039 std::stringstream stream;
1040 printBits(stream);
1041 stream << '\n';
1042 original.printBits(stream);
1043 STORM_LOG_ERROR(stream.str());
1044 STORM_LOG_ASSERT(false, "Setting of bits not correct.");
1045 }
1046 }
1047 }
1048#endif
1049}
1050
1051bool BitVector::compareAndSwap(uint64_t start1, uint64_t start2, uint64_t length) {
1052 if (length < 64) {
1053 // Just use one number
1054 uint64_t elem1 = getAsInt(start1, length);
1055 uint64_t elem2 = getAsInt(start2, length);
1056 if (elem1 < elem2) {
1057 // Swap elements
1058 setFromInt(start1, length, elem2);
1059 setFromInt(start2, length, elem1);
1060 return true;
1061 }
1062 return false;
1063 } else {
1064 // Use bit vectors
1065 BitVector elem1 = getAsBitVector(start1, length);
1066 BitVector elem2 = getAsBitVector(start2, length);
1067
1068 if (!(elem1 < elem2)) {
1069 // Elements already sorted
1070#ifdef ASSERT_BITVECTOR
1071 // Check that sorted
1072 for (uint64_t i = 0; i < length; ++i) {
1073 if (get(start1 + i) > get(start2 + i)) {
1074 break;
1075 }
1076 STORM_LOG_ASSERT(get(start1 + i) >= get(start2 + i), "Bit vector not sorted for indices " << start1 + i << " and " << start2 + i);
1077 }
1078#endif
1079 return false;
1080 }
1081
1082#ifdef ASSERT_BITVECTOR
1083 BitVector check(*this);
1084#endif
1085
1086 // Swap elements
1087 setFromBitVector(start1, elem2);
1088 setFromBitVector(start2, elem1);
1089
1090#ifdef ASSERT_BITVECTOR
1091 // Check correctness of swapping
1092 bool tmp;
1093 for (uint64_t i = 0; i < length; ++i) {
1094 tmp = check.get(i + start1);
1095 check.set(i + start1, check.get(i + start2));
1096 check.set(i + start2, tmp);
1097 }
1098 STORM_LOG_ASSERT(*this == check, "Swapping not correct");
1099
1100 // Check that sorted
1101 for (uint64_t i = 0; i < length; ++i) {
1102 if (get(start1 + i) > get(start2 + i)) {
1103 break;
1104 }
1105 STORM_LOG_ASSERT(get(start1 + i) >= get(start2 + i), "Bit vector not sorted for indices " << start1 + i << " and " << start2 + i);
1106 }
1107#endif
1108
1109 return true;
1110 }
1111}
1112
1113void BitVector::truncateLastBucket() {
1114 if ((bitCount & mod64mask) != 0) {
1115 buckets[bucketCount() - 1] &= ~((1ll << (64 - (bitCount & mod64mask))) - 1ll);
1116 }
1117}
1118
1119size_t BitVector::bucketCount() const {
1120 size_t result = (bitCount >> 6);
1121 if ((bitCount & mod64mask) != 0) {
1122 ++result;
1123 }
1124 return result;
1125}
1126
1127std::ostream& operator<<(std::ostream& out, BitVector const& bitvector) {
1128 out << "bit vector(" << bitvector.getNumberOfSetBits() << "/" << bitvector.bitCount << ") [";
1129 for (auto index : bitvector) {
1130 out << index << " ";
1131 }
1132 out << "]";
1133
1134 return out;
1135}
1136
1137void BitVector::printBits(std::ostream& out) const {
1138 out << "bit vector(" << getNumberOfSetBits() << "/" << bitCount << ") ";
1139 uint64_t index = 0;
1140 for (; index * 64 + 64 <= bitCount; ++index) {
1141 std::bitset<64> tmp(buckets[index]);
1142 out << tmp << "|";
1143 }
1144
1145 // Print last bits
1146 if (index * 64 < bitCount) {
1147 STORM_LOG_ASSERT(index == bucketCount() - 1, "Not last bucket.");
1148 std::bitset<64> tmp(buckets[index]);
1149 for (size_t i = 0; i + index * 64 < bitCount; ++i) {
1150 // Bits are counted from rightmost in bitset
1151 out << tmp[63 - i];
1152 }
1153 }
1154 out << '\n';
1155}
1156
1158 std::size_t seed = 14695981039346656037ull;
1159
1160 uint8_t* it = reinterpret_cast<uint8_t*>(bv.buckets);
1161 uint8_t const* ite = it + 8 * bv.bucketCount();
1162
1163 while (it < ite) {
1164 seed ^= *it++;
1165
1166 // Multiplication with magic prime.
1167 seed += (seed << 1) + (seed << 4) + (seed << 5) + (seed << 7) + (seed << 8) + (seed << 40);
1168 }
1169
1170 return seed;
1171}
1172
1173inline __attribute__((always_inline)) uint32_t fmix32(uint32_t h) {
1174 h ^= h >> 16;
1175 h *= 0x85ebca6b;
1176 h ^= h >> 13;
1177 h *= 0xc2b2ae35;
1178 h ^= h >> 16;
1179
1180 return h;
1181}
1182
1183inline __attribute__((always_inline)) uint64_t fmix64(uint64_t k) {
1184 k ^= k >> 33;
1185 k *= 0xff51afd7ed558ccdull;
1186 k ^= k >> 33;
1187 k *= 0xc4ceb9fe1a85ec53ull;
1188 k ^= k >> 33;
1189
1190 return k;
1191}
1192
1193inline uint32_t rotl32(uint32_t x, int8_t r) {
1194 return (x << r) | (x >> (32 - r));
1195}
1196
1197inline uint64_t rotl64(uint64_t x, int8_t r) {
1198 return (x << r) | (x >> (64 - r));
1199}
1200
1201inline __attribute__((always_inline)) uint32_t getblock32(uint32_t const* p, int i) {
1202 return p[i];
1203}
1204
1205inline __attribute__((always_inline)) uint32_t getblock64(uint64_t const* p, int i) {
1206 return p[i];
1207}
1208
1209template<>
1211 uint8_t const* data = reinterpret_cast<uint8_t const*>(bv.buckets);
1212 uint32_t len = bv.bucketCount() * 8;
1213 const int nblocks = bv.bucketCount() * 2;
1214
1215 // Using 0 as seed.
1216 uint32_t h1 = 0;
1217
1218 const uint32_t c1 = 0xcc9e2d51;
1219 const uint32_t c2 = 0x1b873593;
1220
1221 //----------
1222 // body
1223
1224 const uint32_t* blocks = reinterpret_cast<uint32_t const*>(data + nblocks * 4);
1225
1226 for (int i = -nblocks; i; i++) {
1227 uint32_t k1 = getblock32(blocks, i);
1228
1229 k1 *= c1;
1230 k1 = rotl32(k1, 15);
1231 k1 *= c2;
1232
1233 h1 ^= k1;
1234 h1 = rotl32(h1, 13);
1235 h1 = h1 * 5 + 0xe6546b64;
1236 }
1237
1238 //----------
1239 // finalization
1240
1241 h1 ^= len;
1242
1243 h1 = fmix32(h1);
1244
1245 return h1;
1246}
1247
1248template<>
1250 uint8_t const* data = reinterpret_cast<uint8_t const*>(bv.buckets);
1251 uint64_t len = bv.bucketCount() * 8;
1252 const int nblocks = bv.bucketCount() / 2;
1253
1254 uint64_t h1 = 0;
1255 uint64_t h2 = 0;
1256
1257 const uint64_t c1 = 0x87c37b91114253d5ull;
1258 const uint64_t c2 = 0x4cf5ad432745937full;
1259
1260 //----------
1261 // body
1262
1263 const uint64_t* blocks = (const uint64_t*)(data);
1264
1265 for (int i = 0; i < nblocks; i++) {
1266 uint64_t k1 = getblock64(blocks, i * 2 + 0);
1267 uint64_t k2 = getblock64(blocks, i * 2 + 1);
1268
1269 k1 *= c1;
1270 k1 = rotl64(k1, 31);
1271 k1 *= c2;
1272 h1 ^= k1;
1273
1274 h1 = rotl64(h1, 27);
1275 h1 += h2;
1276 h1 = h1 * 5 + 0x52dce729;
1277
1278 k2 *= c2;
1279 k2 = rotl64(k2, 33);
1280 k2 *= c1;
1281 h2 ^= k2;
1282
1283 h2 = rotl64(h2, 31);
1284 h2 += h1;
1285 h2 = h2 * 5 + 0x38495ab5;
1286 }
1287
1288 //----------
1289 // tail
1290
1291 uint8_t const* tail = reinterpret_cast<uint8_t const*>(data + nblocks * 16);
1292
1293 uint64_t k1 = 0;
1294 uint64_t k2 = 0;
1295 // Loop unrolling via Duff's device
1296 // Cases are supposed to fall-through
1297 switch (len & 15) {
1298 case 15:
1299 k2 ^= ((uint64_t)tail[14]) << 48;
1300 // fallthrough
1301 case 14:
1302 k2 ^= ((uint64_t)tail[13]) << 40;
1303 // fallthrough
1304 case 13:
1305 k2 ^= ((uint64_t)tail[12]) << 32;
1306 // fallthrough
1307 case 12:
1308 k2 ^= ((uint64_t)tail[11]) << 24;
1309 // fallthrough
1310 case 11:
1311 k2 ^= ((uint64_t)tail[10]) << 16;
1312 // fallthrough
1313 case 10:
1314 k2 ^= ((uint64_t)tail[9]) << 8;
1315 // fallthrough
1316 case 9:
1317 k2 ^= ((uint64_t)tail[8]) << 0;
1318 k2 *= c2;
1319 k2 = rotl64(k2, 33);
1320 k2 *= c1;
1321 h2 ^= k2;
1322 // fallthrough
1323
1324 case 8:
1325 k1 ^= ((uint64_t)tail[7]) << 56;
1326 // fallthrough
1327 case 7:
1328 k1 ^= ((uint64_t)tail[6]) << 48;
1329 // fallthrough
1330 case 6:
1331 k1 ^= ((uint64_t)tail[5]) << 40;
1332 // fallthrough
1333 case 5:
1334 k1 ^= ((uint64_t)tail[4]) << 32;
1335 // fallthrough
1336 case 4:
1337 k1 ^= ((uint64_t)tail[3]) << 24;
1338 // fallthrough
1339 case 3:
1340 k1 ^= ((uint64_t)tail[2]) << 16;
1341 // fallthrough
1342 case 2:
1343 k1 ^= ((uint64_t)tail[1]) << 8;
1344 // fallthrough
1345 case 1:
1346 k1 ^= ((uint64_t)tail[0]) << 0;
1347 // fallthrough
1348 k1 *= c1;
1349 k1 = rotl64(k1, 31);
1350 k1 *= c2;
1351 h1 ^= k1;
1352 };
1353
1354 //----------
1355 // finalization
1356
1357 h1 ^= len;
1358 h2 ^= len;
1359
1360 h1 += h2;
1361 h2 += h1;
1362
1363 h1 = fmix64(h1);
1364 h2 = fmix64(h2);
1365
1366 h1 += h2;
1367 h2 += h1;
1368
1369 return h1 ^ h2;
1370}
1371
1372void BitVector::store(std::ostream& os) const {
1373 os << bitCount;
1374 for (uint64_t i = 0; i < bucketCount(); ++i) {
1375 os << " " << buckets[i];
1376 }
1377}
1378
1379BitVector BitVector::load(std::string const& description) {
1380 std::vector<std::string> splitted;
1381 std::stringstream ss(description);
1382 ss >> std::noskipws;
1383 std::string field;
1384 char ws_delim;
1385 while (true) {
1386 if (ss >> field)
1387 splitted.push_back(field);
1388 else if (ss.eof())
1389 break;
1390 else
1391 splitted.push_back(std::string());
1392 ss.clear();
1393 ss >> ws_delim;
1394 }
1395 BitVector bv(std::stoul(splitted[0]));
1396 for (uint64_t i = 0; i < splitted.size() - 1; ++i) {
1397 bv.buckets[i] = std::stoul(splitted[i + 1]);
1398 }
1399 return bv;
1400}
1401
1402// All necessary explicit template instantiations.
1403template BitVector::BitVector(uint64_t length, std::vector<uint64_t>::iterator begin, std::vector<uint64_t>::iterator end);
1404template BitVector::BitVector(uint64_t length, std::vector<uint64_t>::const_iterator begin, std::vector<uint64_t>::const_iterator end);
1407template void BitVector::set(std::vector<uint64_t>::iterator begin, std::vector<uint64_t>::iterator end, bool value);
1408template void BitVector::set(std::vector<uint64_t>::const_iterator begin, std::vector<uint64_t>::const_iterator end, bool value);
1411
1412template struct Murmur3BitVectorHash<uint32_t>;
1413template struct Murmur3BitVectorHash<uint64_t>;
1414} // namespace storage
1415} // namespace storm
1416
1417namespace std {
1418std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bitvector) const {
1419 return boost::hash_range(bitvector.buckets, bitvector.buckets + bitvector.bucketCount());
1420}
1421} // namespace std
A class that enables iterating over the indices of the bit vector whose corresponding bits are set to...
Definition BitVector.h:23
uint64_t operator*() const
Returns the index of the current bit to which this iterator points.
Definition BitVector.cpp:62
const_iterator & operator++()
Increases the position of the iterator to the position of the next bit that is set to true in the und...
Definition BitVector.cpp:44
bool operator==(const_iterator const &other) const
Compares the iterator with another iterator for equality.
Definition BitVector.cpp:70
const_iterator & operator+=(size_t n)
Increases the position of the iterator to the position of the n'th next bit that is set to true in th...
Definition BitVector.cpp:55
const_iterator & operator=(const_iterator const &other)
Assigns the contents of the given iterator to the current one via copying the former's contents.
Definition BitVector.cpp:34
bool operator!=(const_iterator const &other) const
Compares the iterator with another iterator for inequality.
Definition BitVector.cpp:66
A class that enables iterating over the indices of the bit vector whose corresponding bits are set to...
Definition BitVector.h:123
bool operator==(const_reverse_iterator const &other) const
Compares the iterator with another iterator for equality.
uint64_t operator*() const
Returns the index of the current bit to which this iterator points.
const_reverse_iterator()
Constructs a reverse iterator over the indices of the set bits in the given bit vector,...
Definition BitVector.cpp:74
const_reverse_iterator & operator+=(size_t n)
Lets the iterator point to the n'th previous bit with value 1.
const_reverse_iterator & operator++()
Lets the iterator point to the previous bit with value 1.
const_reverse_iterator & operator=(const_reverse_iterator const &other)
Definition BitVector.cpp:91
bool operator!=(const_reverse_iterator const &other) const
Compares the iterator with another iterator for inequality.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
~BitVector()
Deconstructs a bit vector by deleting the underlying storage.
void complement()
Negates all bits in the bit vector.
BitVector & operator|=(BitVector const &other)
Performs a logical "or" with the given bit vector and assigns the result to the current bit vector.
BitVector operator^(BitVector const &other) const
Performs a logical "xor" with the given bit vector.
void setMultiple(uint64_t bitIndex, uint64_t nrOfBits, bool newValue=true)
Sets multiple bits to the given value.
bool operator<(BitVector const &other) const
Retrieves whether the current bit vector is (in some order) smaller than the given one.
const_reverse_iterator rbegin() const
Returns a reverse iterator to the indices of the set bits in the bit vector.
void fill()
Sets all bits from the bit vector.
uint64_t getNextSetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
uint64_t getTwoBitsAligned(uint64_t bitIndex) const
bool isDisjointFrom(BitVector const &other) const
Checks whether none of the bits that are set in the current bit vector are also set in the given bit ...
bool full() const
Retrieves whether all bits are set in this bit vector.
std::vector< uint64_t > getNumberOfSetBitsBeforeIndices() const
Retrieves a vector that holds at position i the number of bits set before index i.
const_reverse_iterator rend() const
Returns a reverse iterator pointing at the element past the front of the bit vector.
BitVector()
Constructs an empty bit vector of length 0.
const_iterator end() const
Returns an iterator pointing at the element past the back of the bit vector.
void grow(uint64_t minimumLength, bool init=false)
Enlarges the bit vector such that it holds at least the given number of bits (but possibly more).
void store(std::ostream &) const
BitVector operator%(BitVector const &filter) const
Computes a bit vector that contains only the values of the bits given by the filter.
BitVector operator|(BitVector const &other) const
Performs a logical "or" with the given bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
std::size_t getSizeInBytes() const
Returns (an approximation of) the size of the bit vector measured in bytes.
void clear()
Removes all set bits from the bit vector.
bool isSubsetOf(BitVector const &other) const
Checks whether all bits that are set in the current bit vector are also set in the given bit vector.
BitVector implies(BitVector const &other) const
Performs a logical "implies" with the given bit vector.
BitVector & operator=(BitVector const &other)
Assigns the contents of the given bit vector to the current bit vector via a deep copy.
uint64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
uint64_t getNextUnsetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to false in the bit vector.
bool compareAndSwap(uint64_t start1, uint64_t start2, uint64_t length)
Compare two intervals [start1, start1+length] and [start2, start2+length] and swap them if the second...
BitVector operator&(BitVector const &other) const
Performs a logical "and" with the given bit vector.
void setFromInt(uint64_t bitIndex, uint64_t numberOfBits, uint64_t value)
Sets the selected number of lowermost bits of the provided value at the given bit index.
BitVector permute(std::vector< uint64_t > const &inversePermutation) const
Apply a permutation of entries.
void set(uint64_t index, bool value=true)
Sets the given truth value at the given index.
void increment()
Increments the (unsigned) number represented by this BitVector by one.
bool matches(uint64_t bitIndex, BitVector const &other) const
Checks whether the given bit vector matches the bits starting from the given index in the current bit...
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
uint64_t getStartOfZeroSequenceBefore(uint64_t endIndex) const
Retrieves the smallest index i such that all bits in the range [i,endIndex) are 0.
uint64_t getAsInt(uint64_t bitIndex, uint64_t numberOfBits) const
Retrieves the content of the current bit vector at the given index for the given number of bits as an...
BitVector operator~() const
Performs a logical "not" on the bit vector.
bool operator!=(BitVector const &other) const
Compares the given bit vector with the current one.
size_t size() const
Retrieves the number of bits this bit vector can store.
void resize(uint64_t newLength, bool init=false)
Resizes the bit vector to hold the given new number of bits.
BitVector & operator&=(BitVector const &other)
Performs a logical "and" with the given bit vector and assigns the result to the current bit vector.
static BitVector load(std::string const &description)
void expandSize(bool init=false)
bool get(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
bool operator==(BitVector const &other) const
Compares the given bit vector with the current one.
uint64_t getNumberOfSetBitsBeforeIndex(uint64_t index) const
Retrieves the number of bits set in this bit vector with an index strictly smaller than the given one...
BitVector permuteGroupedVector(std::vector< uint64_t > const &inversePermutation, std::vector< uint64_t > const &rowGroupIndices) const
Apply a permutation of entries assuming a grouped vector.
uint64_t getStartOfOneSequenceBefore(uint64_t endIndex) const
Retrieves the smallest index i such that all bits in the range [i,endIndex) are 1.
bool operator[](uint64_t index) const
Retrieves the truth value of the bit at the given index.
void concat(BitVector const &extension)
Concatenate this bitvector with another bitvector.
#define STORM_LOG_ERROR(message)
Definition logging.h:26
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
void writeValue(std::ostream &os, ValueType value, std::unordered_map< ValueType, std::string > const &placeholders)
Write value to stream while using the placeholders.
uint32_t rotl32(uint32_t x, int8_t r)
uint64_t rotl64(uint64_t x, int8_t r)
boost::container::flat_set< Key, std::less< Key >, boost::container::new_allocator< Key > > FlatSet
Redefinition of flat_set was needed, because from Boost 1.70 on the default allocator is set to void.
Definition BoostTypes.h:13
__attribute__((always_inline)) uint32_t fmix32(uint32_t h)
LabParser.cpp.
std::size_t operator()(storm::storage::BitVector const &bv) const
StateType operator()(storm::storage::BitVector const &bv) const