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