Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BitVector.h
Go to the documentation of this file.
1#pragma once
2
3#include <cmath>
4#include <cstdint>
5#include <functional>
6#include <iterator>
7#include <ostream>
8#include <ranges>
9#include <vector>
10
11namespace storm::storage {
12
16class BitVector {
17 public:
24 // Declare the BitVector class as a friend class to access its internal storage.
25 friend class BitVector;
26
27 public:
28 // Define iterator
29 using iterator_category = std::forward_iterator_tag;
30 using value_type = uint64_t;
31 using difference_type = std::ptrdiff_t;
32 using pointer = uint64_t*;
33 using reference = uint64_t&;
34
36
47 const_iterator(uint64_t const* dataPtr, uint64_t startIndex, uint64_t endIndex, bool setOnFirstBit = true);
48
54 const_iterator(const_iterator const& other);
55
62
70
78
83 const_iterator& operator+=(size_t n);
84
90 uint64_t operator*() const;
91
98 bool operator!=(const_iterator const& other) const;
99
106 bool operator==(const_iterator const& other) const;
107
108 private:
109 // The underlying bit vector of this iterator.
110 uint64_t const* dataPtr;
111
112 // The index of the bit this iterator currently points to.
113 uint64_t currentIndex;
114
115 // The index of the bit that is past the end of the range of this iterator.
116 uint64_t endIndex;
117 };
124 // Declare the BitVector class as a friend class to access its internal storage.
125 friend class BitVector;
126
127 public:
128 // Define iterator
129 using iterator_category = std::forward_iterator_tag;
130 using value_type = uint64_t;
131 using difference_type = std::ptrdiff_t;
132 using pointer = uint64_t*;
133 using reference = uint64_t&;
134
146 const_reverse_iterator(uint64_t const* dataPtr, uint64_t upperBound, uint64_t lowerBound = 0ull, bool setOnFirstBit = true);
149
155
161
166
172 uint64_t operator*() const;
173
180 bool operator!=(const_reverse_iterator const& other) const;
181
188 bool operator==(const_reverse_iterator const& other) const;
189
190 private:
192 uint64_t const* dataPtr;
193
195 uint64_t currentIndex;
196
198 uint64_t lowerBound;
199 };
200
204 BitVector();
205
209 ~BitVector();
210
218 explicit BitVector(uint64_t length, bool init = false);
219
228 template<typename InputIterator>
229 BitVector(uint64_t length, InputIterator first, InputIterator last);
230
234 BitVector(uint64_t length, std::vector<uint64_t> setEntries);
235
241 BitVector(BitVector const& other);
242
248 BitVector(BitVector&& other);
249
256 bool operator==(BitVector const& other) const;
257
264 bool operator!=(BitVector const& other) const;
265
273 BitVector& operator=(BitVector const& other);
274
282 BitVector& operator=(BitVector&& other);
283
290 bool operator<(BitVector const& other) const;
291
298 void set(uint64_t index, bool value = true);
299
306 template<typename InputIterator>
307 void set(InputIterator first, InputIterator last, bool value = true);
308
316 bool operator[](uint64_t index) const;
317
325 bool get(uint64_t index) const;
326
334 void resize(uint64_t newLength, bool init = false);
335
342 void concat(BitVector const& extension);
343
344 /*
345 * Expands the size to a multiple of 64.
346 */
347 void expandSize(bool init = false);
348
358 void grow(uint64_t minimumLength, bool init = false);
359
367 BitVector operator&(BitVector const& other) const;
368
378 BitVector& operator&=(BitVector const& other);
379
387 BitVector operator|(BitVector const& other) const;
388
398 BitVector& operator|=(BitVector const& other);
399
407 BitVector operator^(BitVector const& other) const;
408
420 BitVector operator%(BitVector const& filter) const;
421
427 BitVector operator~() const;
428
432 void complement();
433
439 void increment();
440
448 BitVector implies(BitVector const& other) const;
449
458 bool isSubsetOf(BitVector const& other) const;
459
469 bool isDisjointFrom(BitVector const& other) const;
470
479 bool matches(uint64_t bitIndex, BitVector const& other) const;
480
489 void set(uint64_t bitIndex, BitVector const& other);
490
494 void setMultiple(uint64_t bitIndex, uint64_t nrOfBits, bool newValue = true);
495
502 BitVector permute(std::vector<uint64_t> const& inversePermutation) const;
503
510 BitVector permuteGroupedVector(std::vector<uint64_t> const& inversePermutation, std::vector<uint64_t> const& rowGroupIndices) const;
511
520 storm::storage::BitVector get(uint64_t bitIndex, uint64_t numberOfBits) const;
521
529 uint64_t getAsInt(uint64_t bitIndex, uint64_t numberOfBits) const;
530
536 uint64_t getTwoBitsAligned(uint64_t bitIndex) const;
537
545 void setFromInt(uint64_t bitIndex, uint64_t numberOfBits, uint64_t value);
546
552 bool empty() const;
553
560 bool full() const;
561
565 void clear();
566
570 void fill();
571
577 uint64_t getNumberOfSetBits() const;
578
585 uint64_t getNumberOfSetBitsBeforeIndex(uint64_t index) const;
586
592 std::vector<uint64_t> getNumberOfSetBitsBeforeIndices() const;
593
594 /*
595 * @return True, if the number of set bits is 1, false otherwise.
596 */
597 bool hasUniqueSetBit() const;
598
604 size_t size() const;
605
611 std::size_t getSizeInBytes() const;
612
617 const_iterator begin() const;
618
623 const_iterator begin(uint64_t lowerBound) const;
624
628 const_iterator end() const;
629
635
640 const_reverse_iterator rbegin(uint64_t upperBound) const;
641
646
656 uint64_t getNextSetIndex(uint64_t startingIndex) const;
657
667 uint64_t getNextUnsetIndex(uint64_t startingIndex) const;
668
678 uint64_t getStartOfZeroSequenceBefore(uint64_t endIndex) const;
679
689 uint64_t getStartOfOneSequenceBefore(uint64_t endIndex) const;
690
700 bool compareAndSwap(uint64_t start1, uint64_t start2, uint64_t length);
701
702 friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector);
703
704 void store(std::ostream&) const;
705 static BitVector load(std::string const& description);
706
707 friend struct std::hash<storm::storage::BitVector>;
708 friend struct FNV1aBitVectorHash;
709
710 template<typename StateType>
711 friend struct Murmur3BitVectorHash;
712
713 private:
720 BitVector(uint64_t bucketCount, uint64_t bitCount);
721
735 template<bool Value, bool Backward = false>
736 static uint64_t getNextIndexWithValue(uint64_t const* dataPtr, uint64_t startingIndex, uint64_t endIndex);
737
741 void truncateLastBucket();
742
750 BitVector getAsBitVector(uint64_t start, uint64_t length) const;
751
759 void setFromBitVector(uint64_t start, BitVector const& other);
760
766 void printBits(std::ostream& out) const;
767
773 size_t bucketCount() const;
774
775 // The number of bits that this bit vector can hold.
776 uint64_t bitCount;
777
778 // The underlying storage of 64-bit buckets for all bits of this bit vector.
779 uint64_t* buckets;
780
781 // A bit mask that can be used to reduce a modulo 64 operation to a logical "and".
782 static const uint64_t mod64mask = (1 << 6) - 1;
783};
784
785static_assert(std::ranges::forward_range<BitVector>);
786
787struct FNV1aBitVectorHash {
788 std::size_t operator()(storm::storage::BitVector const& bv) const;
789};
790
791template<typename StateType>
792struct Murmur3BitVectorHash {
793 StateType operator()(storm::storage::BitVector const& bv) const;
794};
795
796} // namespace storm::storage
797
798namespace std {
799template<>
800struct hash<storm::storage::BitVector> {
801 std::size_t operator()(storm::storage::BitVector const& bv) const;
802};
803} // 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
std::forward_iterator_tag iterator_category
Definition BitVector.h:29
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...
friend std::ostream & operator<<(std::ostream &out, BitVector const &bitVector)
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.
LabParser.cpp.