From d5cadc0f4b810dae4066d79eceee33fdd8e21fbe Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 5 Dec 2013 14:09:06 +0100 Subject: [PATCH] Finalized interface of bit vector. Added unit tests for all methods of the bit vector. Former-commit-id: 6c7834ed20fcf34789860bf68149b3aae7a84aa5 --- .../SparseMarkovAutomatonCslModelChecker.h | 8 +- .../prctl/SparseDtmcPrctlModelChecker.h | 2 +- .../prctl/SparseMdpPrctlModelChecker.h | 2 +- src/models/AtomicPropositionsLabeling.h | 2 +- src/storage/BitVector.cpp | 157 +++---- src/storage/BitVector.h | 288 ++++++------ test/functional/storage/BitVectorTest.cpp | 418 +++++++++++++++--- 7 files changed, 598 insertions(+), 279 deletions(-) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index f050a2286..d4feb1e88 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -209,10 +209,10 @@ namespace storm { std::vector vAllMarkovian(markovianStates.getNumberOfSetBits()); // Create the starting value vectors for the next value iteration based on the results of the previous one. - storm::utility::vector::setVectorValues(vAllProbabilistic, ~markovianStates % goalStates, storm::utility::constGetOne()); - storm::utility::vector::setVectorValues(vAllProbabilistic, ~markovianStates % ~goalStates, vProbabilistic); - storm::utility::vector::setVectorValues(vAllMarkovian, markovianStates % goalStates, storm::utility::constGetOne()); - storm::utility::vector::setVectorValues(vAllMarkovian, markovianStates % ~goalStates, vMarkovian); + storm::utility::vector::setVectorValues(vAllProbabilistic, goalStates % ~markovianStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(vAllProbabilistic, ~goalStates % ~markovianStates, vProbabilistic); + storm::utility::vector::setVectorValues(vAllMarkovian, goalStates % markovianStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(vAllMarkovian, ~goalStates % markovianStates, vMarkovian); // Compute the number of steps to reach the target interval. numberOfSteps = static_cast(std::ceil(lowerBound / delta)); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 45ae525c7..8505b3ca9 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -127,7 +127,7 @@ public: storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0); // Compute the new set of target states in the reduced system. - storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % psiStates; + storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0; // Make all rows absorbing that satisfy the second sub-formula. submatrix.makeRowsAbsorbing(rightStatesInReducedSystem); diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 008ea3606..2ffcba987 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -119,7 +119,7 @@ namespace storm { std::vector subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), statesWithProbabilityGreater0); // Compute the new set of target states in the reduced system. - storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % psiStates; + storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0; // Make all rows absorbing that satisfy the second sub-formula. submatrix.makeRowsAbsorbing(rightStatesInReducedSystem, subNondeterministicChoiceIndices); diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index fdb9e8757..f102a8038 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -71,7 +71,7 @@ public: // Now we need to copy the fraction of the single labelings given by the substates. singleLabelings.reserve(apCountMax); for (auto const& labeling : atomicPropositionsLabeling.singleLabelings) { - singleLabelings.emplace_back(labeling, substates); + singleLabelings.emplace_back(labeling % substates); } } diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 6b4542fed..154043fff 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -13,17 +13,31 @@ extern log4cplus::Logger logger; namespace storm { namespace storage { - BitVector::const_iterator::const_iterator(const BitVector& bitVector, uint_fast64_t startIndex, uint_fast64_t endIndex, bool setOnFirstBit) : bitVector(bitVector), endIndex(endIndex) { + BitVector::const_iterator::const_iterator(uint64_t const* dataPtr, uint_fast64_t startIndex, uint_fast64_t endIndex, bool setOnFirstBit) : dataPtr(dataPtr), endIndex(endIndex) { if (setOnFirstBit) { // Set the index of the first set bit in the vector. - currentIndex = bitVector.getNextSetIndex(startIndex, endIndex); + currentIndex = getNextSetIndex(dataPtr, startIndex, endIndex); } else { currentIndex = startIndex; } } + BitVector::const_iterator::const_iterator(const_iterator const& other) : dataPtr(other.dataPtr), currentIndex(other.currentIndex), endIndex(other.endIndex) { + // Intentionally left empty. + } + + BitVector::const_iterator& BitVector::const_iterator::operator=(const_iterator const& other) { + // Only assign contents if the source and target are not the same. + if (this != &other) { + dataPtr = other.dataPtr; + currentIndex = other.currentIndex; + endIndex = other.endIndex; + } + return *this; + } + BitVector::const_iterator& BitVector::const_iterator::operator++() { - currentIndex = bitVector.getNextSetIndex(++currentIndex, endIndex); + currentIndex = getNextSetIndex(dataPtr, ++currentIndex, endIndex); return *this; } @@ -31,19 +45,19 @@ namespace storm { return currentIndex; } - bool BitVector::const_iterator::operator!=(const_iterator const& otherIterator) const { - return currentIndex != otherIterator.currentIndex; + bool BitVector::const_iterator::operator!=(const_iterator const& other) const { + return currentIndex != other.currentIndex; } - bool BitVector::const_iterator::operator==(const_iterator const& otherIterator) const { - return currentIndex == otherIterator.currentIndex; + bool BitVector::const_iterator::operator==(const_iterator const& other) const { + return currentIndex == other.currentIndex; } BitVector::BitVector() : bitCount(0), bucketVector() { // Intentionally left empty. } - BitVector::BitVector(uint_fast64_t length, bool initTrue) : bitCount(length) { + BitVector::BitVector(uint_fast64_t length, bool init) : bitCount(length) { // Compute the correct number of buckets needed to store the given number of bits. uint_fast64_t bucketCount = length >> 6; if ((length & mod64mask) != 0) { @@ -51,7 +65,7 @@ namespace storm { } // Initialize the storage with the required values. - if (initTrue) { + if (init) { bucketVector = std::vector(bucketCount, -1ll); truncateLastBucket(); } else { @@ -68,21 +82,6 @@ namespace storm { // Intentionally left empty. } - BitVector::BitVector(BitVector const& other, BitVector const& filter) : bitCount(filter.getNumberOfSetBits()) { - uint_fast64_t bucketCount = bitCount >> 6; - if ((bitCount & mod64mask) != 0) { - ++bucketCount; - } - bucketVector = std::vector(bucketCount); - - // Now copy over all bits given by the filter. - uint_fast64_t nextPosition = 0; - for (auto position : filter) { - set(nextPosition, other.get(position)); - nextPosition++; - } - } - BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), bucketVector(std::move(other.bucketVector)) { // Intentionally left empty. } @@ -92,7 +91,6 @@ namespace storm { if (this != &other) { bitCount = other.bitCount; bucketVector = std::vector(other.bucketVector); - updateSizeChange(); } return *this; } @@ -102,7 +100,6 @@ namespace storm { if (this != &other) { bitCount = other.bitCount; bucketVector = std::move(other.bucketVector); - updateSizeChange(); } return *this; @@ -153,7 +150,7 @@ namespace storm { return (*this)[index]; } - void BitVector::resize(uint_fast64_t newLength, bool initTrue) { + void BitVector::resize(uint_fast64_t newLength, bool init) { if (newLength > bitCount) { uint_fast64_t newBucketCount = newLength >> 6; if ((newLength & mod64mask) != 0) { @@ -161,8 +158,8 @@ namespace storm { } if (newBucketCount > bucketVector.size()) { - if (initTrue) { - bucketVector.back() |= (1ll << (bitCount * 64 - bitCount * 63 - bitCount & mod64mask)) - 1ll; + if (init) { + bucketVector.back() |= ~((1ll << (bitCount & mod64mask)) - 1ll); bucketVector.resize(newBucketCount, -1ll); } else { bucketVector.resize(newBucketCount, 0); @@ -170,14 +167,12 @@ namespace storm { bitCount = newLength; } else { // If the underlying storage does not need to grow, we have to insert the missing bits. - if (initTrue) { - bucketVector.back() |= (1ll << (bitCount * 64 - bitCount * 63 - bitCount & mod64mask)) - 1ll; - bitCount = newLength; - } else { - bitCount = newLength; + if (init) { + bucketVector.back() |= ~((1ll << (bitCount & mod64mask)) - 1ll); } + bitCount = newLength; } - updateSizeChange(); + truncateLastBucket(); } else { bitCount = newLength; bitCount = newLength; @@ -187,7 +182,7 @@ namespace storm { } bucketVector.resize(newBucketCount); - updateSizeChange(); + truncateLastBucket(); } } @@ -252,6 +247,36 @@ namespace storm { return result; } + BitVector BitVector::operator%(BitVector const& filter) const { + if (bitCount != filter.bitCount) { + throw storm::exceptions::InvalidArgumentException() << "Invalid call to BitVector::operator%: length mismatch of operands."; + } + + BitVector result(filter.getNumberOfSetBits()); + + // If the current bit vector has not too many elements compared to the given bit vector we prefer iterating + // over its elements. + if (filter.getNumberOfSetBits() / 10 < this->getNumberOfSetBits()) { + uint_fast64_t position = 0; + for (auto bit : filter) { + if ((*this)[bit]) { + result.set(position); + } + ++position; + } + } else { + // If the given bit vector had much less elements, we iterate over its elements and accept calling the more + // costly operation getNumberOfSetBitsBeforeIndex on the current bit vector. + for (auto bit : (*this)) { + if (filter[bit]) { + result.set(filter.getNumberOfSetBitsBeforeIndex(bit)); + } + } + } + + return result; + } + BitVector BitVector::operator~() const { BitVector result(this->bitCount); std::vector::iterator it = result.bucketVector.begin(); @@ -309,43 +334,27 @@ namespace storm { return true; } - BitVector BitVector::operator%(BitVector const& other) const { - if (bitCount != other.bitCount) { - throw storm::exceptions::InvalidArgumentException() << "Invalid call to BitVector::operator%: length mismatch of operands."; - } - - // Create resulting bit vector. - BitVector result(this->getNumberOfSetBits()); - - // If the current bit vector has not too many elements compared to the given bit vector we prefer iterating - // over its elements. - if (this->getNumberOfSetBits() / 10 < other.getNumberOfSetBits()) { - uint_fast64_t position = 0; - for (auto bit : *this) { - if (other[bit]) { - result.set(position); - } - ++position; - } - } else { - // If the given bit vector had much less elements, we iterate over its elements and accept calling the more - // costly operation getNumberOfSetBitsBeforeIndex on the current bit vector. - for (auto bit : other) { - if ((*this)[bit]) { - result.set(this->getNumberOfSetBitsBeforeIndex(bit)); - } + bool BitVector::empty() const { + for (auto& element : bucketVector) { + if (element != 0) { + return false; } } - - return result; + return true; } - bool BitVector::empty() const { - for (auto& element : bucketVector) { - if (element != 0) { + bool BitVector::full() const { + // Check that all buckets except the last one have all bits set. + for (uint_fast64_t index = 0; index < bucketVector.size() - 1; ++index) { + if (bucketVector[index] != -1ll) { return false; } } + + // Now check whether the relevant bits are set in the last bucket. + if ((bucketVector.back() & ((1ll << (bitCount & mod64mask)) - 1ll)) != ((1ll << (bitCount & mod64mask)) - 1ll)) { + return false; + } return true; } @@ -412,11 +421,11 @@ namespace storm { } BitVector::const_iterator BitVector::begin() const { - return const_iterator(*this, 0, bitCount); + return const_iterator(bucketVector.data(), 0, bitCount); } BitVector::const_iterator BitVector::end() const { - return const_iterator(*this, bitCount, bitCount, false); + return const_iterator(bucketVector.data(), bitCount, bitCount, false); } std::size_t BitVector::hash() const { @@ -433,13 +442,13 @@ namespace storm { } uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex) const { - return getNextSetIndex(startingIndex, bitCount); + return getNextSetIndex(bucketVector.data(), startingIndex, bitCount); } - uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex, uint_fast64_t endIndex) const { + uint_fast64_t BitVector::getNextSetIndex(uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex) { uint_fast8_t currentBitInByte = startingIndex & mod64mask; startingIndex >>= 6; - std::vector::const_iterator bucketIt = bucketVector.begin() + startingIndex; + uint64_t const* bucketIt = dataPtr + startingIndex; while ((startingIndex << 6) < endIndex) { // Compute the remaining bucket content by a right shift @@ -473,11 +482,7 @@ namespace storm { bucketVector.back() &= (1ll << (bitCount & mod64mask)) - 1ll; } } - - void BitVector::updateSizeChange() { - truncateLastBucket(); - } - + std::ostream& operator<<(std::ostream& out, BitVector const& bitVector) { out << "bit vector(" << bitVector.getNumberOfSetBits() << "/" << bitVector.bitCount << ") ["; for (auto index : bitVector) { diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 7e0d26c9b..de73dc07c 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -16,8 +16,8 @@ namespace storm { class BitVector { public: /*! - * A class that enables iterating over the indices of the bit vector whose corresponding bits are set to true. - * Note that this is a const iterator, which cannot alter the bit vector. + * A class that enables iterating over the indices of the bit vector whose corresponding bits are set to + * true. Note that this is a const iterator, which cannot alter the bit vector. */ class const_iterator : public std::iterator { // Declare the BitVector class as a friend class to access its internal storage. @@ -25,20 +25,34 @@ namespace storm { public: /*! - * Constructs an iterator over the indices of the set bits in the given bit vector, starting and stopping, - * respectively, at the given indices. + * Constructs an iterator over the indices of the set bits in the given bit vector, starting and + * stopping, respectively, at the given indices. * - * @param bitVector The bit vector over whose bits to iterate. + * @param dataPtr A pointer to the first bucket of the underlying bit vector. * @param startIndex The index where to begin looking for set bits. - * @param setOnFirstBit A flag that indicates whether the iterator is to be moved to the index of the first - * bit upon construction. + * @param setOnFirstBit A flag that indicates whether the iterator is to be moved to the index of the + * first bit upon construction. * @param endIndex The index at which to abort the iteration process. */ - const_iterator(BitVector const& bitVector, uint_fast64_t startIndex, uint_fast64_t endIndex, bool setOnFirstBit = true); + const_iterator(uint64_t const* dataPtr, uint_fast64_t startIndex, uint_fast64_t endIndex, bool setOnFirstBit = true); /*! - * Increases the position of the iterator to the position of the next bit that is set to true in the underlying - * bit vector. + * Constructs an iterator by copying the given iterator. + * + * @param other The iterator to copy. + */ + const_iterator(const_iterator const& other); + + /*! + * Assigns the contents of the given iterator to the current one via copying the former's contents. + * + * @param other The iterator from which to copy-assign. + */ + const_iterator& operator=(const_iterator const& other); + + /*! + * Increases the position of the iterator to the position of the next bit that is set to true in the + * underlying bit vector. * * @return A reference to this iterator. */ @@ -54,22 +68,22 @@ namespace storm { /*! * Compares the iterator with another iterator for inequality. * - * @param otherIterator The iterator with respect to which inequality is checked. + * @param other The iterator with respect to which inequality is checked. * @return True if the two iterators are unequal. */ - bool operator!=(const_iterator const& otherIterator) const; + bool operator!=(const_iterator const& other) const; /*! * Compares the iterator with another iterator for equality. * - * @param otherIterator The iterator with respect to which equality is checked. + * @param other The iterator with respect to which equality is checked. * @return True if the two iterators are equal. */ - bool operator==(const_iterator const& otherIterator) const; + bool operator==(const_iterator const& other) const; private: // The underlying bit vector of this iterator. - BitVector const& bitVector; + uint64_t const* dataPtr; // The index of the bit this iterator currently points to. uint_fast64_t currentIndex; @@ -84,155 +98,170 @@ namespace storm { BitVector(); /*! - * Constructs a bit vector which can hold the given number of bits and - * initializes all bits to the provided truth value. + * Constructs a bit vector which can hold the given number of bits and initializes all bits with the + * provided truth value. + * * @param length The number of bits the bit vector should be able to hold. - * @param initTrue The initial value of the first |length| bits. + * @param init The initial value of the first |length| bits. */ - BitVector(uint_fast64_t length, bool initTrue = false); + BitVector(uint_fast64_t length, bool init = false); /*! - * Creates a bit vector that has exactly the bits set that are given by the provided iterator range. + * Creates a bit vector that has exactly the bits set that are given by the provided input iterator range + * [first, last). * * @param The length of the bit vector. - * @param begin The begin of the iterator range. - * @param end The end of the iterator range. + * @param first The begin of the iterator range. + * @param last The end of the iterator range. */ template - BitVector(uint_fast64_t length, InputIterator begin, InputIterator end); + BitVector(uint_fast64_t length, InputIterator first, InputIterator last); /*! - * Copy Constructor. Performs a deep copy of the given bit vector. - * @param bv A reference to the bit vector to be copied. + * Performs a deep copy of the given bit vector. + * + * @param other A reference to the bit vector to be copied. */ BitVector(BitVector const& other); - - /*! - * Copy Constructor. Performs a deep copy of the bits in the given bit vector that are given by the filter. - * @param bv A reference to the bit vector to be copied. - * @param filter The filter to apply for copying. - */ - BitVector(BitVector const& other, BitVector const& filter); - + /*! - * Move constructor. Move constructs the bit vector from the given bit vector. + * Move constructs the bit vector from the given bit vector. * + * @param other The bit vector from which to move-construct. */ - BitVector(BitVector&& bv); + BitVector(BitVector&& other); /*! * Compares the given bit vector with the current one. + * + * @param other The bitvector with which to compare the current one. */ - bool operator==(BitVector const& bv); + bool operator==(BitVector const& other); /*! - * Assigns the given bit vector to the current bit vector by a deep copy. - * @param bv The bit vector to assign to the current bit vector. - * @return A reference to this bit vector after it has been assigned the - * given bit vector by means of a deep copy. + * Assigns the contents of the given bit vector to the current bit vector via a deep copy. + * + * @param other The bit vector to assign to the current bit vector. + * @return A reference to this bit vector after it has been assigned the given bit vector by means of a + * deep copy. */ - BitVector& operator=(BitVector const& bv); + BitVector& operator=(BitVector const& other); /*! * Move assigns the given bit vector to the current bit vector. * - * @param bv The bit vector whose content is moved to the current bit vector. - * @return A reference to this bit vector after the contents of the given bit vector - * have been moved into it. + * @param other The bit vector whose content is moved to the current bit vector. + * @return A reference to this bit vector after the contents of the given bit vector have been moved + * into it. */ - BitVector& operator=(BitVector&& bv); + BitVector& operator=(BitVector&& other); /*! * Sets the given truth value at the given index. + * * @param index The index where to set the truth value. * @param value The truth value to set. */ void set(const uint_fast64_t index, bool value = true); /*! - * Sets all bits in the given iterator range. + * Sets all bits in the given iterator range [first, last). * - * @param begin The begin of the iterator range. - * @param end The element past the last element of the iterator range. + * @param first The begin of the iterator range. + * @param last The element past the last element of the iterator range. */ template - void set(InputIterator begin, InputIterator end); + void set(InputIterator first, InputIterator last); /*! - * Retrieves the truth value of the bit at the given index. Note: this does not check whether the - * given index is within bounds. + * Retrieves the truth value of the bit at the given index. Note: this does not check whether the given + * index is within bounds. * * @param index The index of the bit to access. - * @return True if the bit at the given index is set. + * @return True iff the bit at the given index is set. */ bool operator[](uint_fast64_t index) const; /*! - * Retrieves the truth value of the bit at the given index and performs a bound check. + * Retrieves the truth value of the bit at the given index and performs a bound check. If the access is + * out-of-bounds an OutOfBoundsException is thrown. * * @param index The index of the bit to access. - * @return True if the bit at the given index is set. + * @return True iff the bit at the given index is set. */ bool get(const uint_fast64_t index) const; /*! - * Resizes the bit vector to hold the given new number of bits. If the bit vector becomes smaller this way, the - * bits are truncated. Otherwise, the new bits are initialized to the given value. + * Resizes the bit vector to hold the given new number of bits. If the bit vector becomes smaller this way, + * the bits are truncated. Otherwise, the new bits are initialized to the given value. * * @param newLength The new number of bits the bit vector can hold. - * @param initTrue Sets whether newly created bits are initialized to true instead of false. + * @param init The truth value to which to initialize newly created bits. */ - void resize(uint_fast64_t newLength, bool initTrue = false); + void resize(uint_fast64_t newLength, bool init = false); /*! - * Performs a logical "and" with the given bit vector. In case the sizes of the bit vectors - * do not match, only the matching portion is considered and the overlapping bits - * are set to 0. - * @param bv A reference to the bit vector to use for the operation. + * Performs a logical "and" with the given bit vector. In case the sizes of the bit vectors do not match, + * only the matching portion is considered and the overlapping bits are set to 0. + * + * @param other A reference to the bit vector to use for the operation. * @return A bit vector corresponding to the logical "and" of the two bit vectors. */ - BitVector operator&(BitVector const& bv) const; + BitVector operator&(BitVector const& other) const; /*! - * Performs a logical "and" with the given bit vector and assigns the result to the - * current bit vector. In case the sizes of the bit vectors do not match, - * only the matching portion is considered and the overlapping bits are set to 0. - * @param bv A reference to the bit vector to use for the operation. + * Performs a logical "and" with the given bit vector and assigns the result to the current bit vector. + * In case the sizes of the bit vectors do not match, only the matching portion is considered and the + * overlapping bits are set to 0. + * + * @param other A reference to the bit vector to use for the operation. * @return A reference to the current bit vector corresponding to the logical "and" * of the two bit vectors. */ - BitVector& operator&=(BitVector const& bv); + BitVector& operator&=(BitVector const& other); /*! - * Performs a logical "or" with the given bit vector. In case the sizes of the bit vectors - * do not match, only the matching portion is considered and the overlapping bits - * are set to 0. - * @param bv A reference to the bit vector to use for the operation. + * Performs a logical "or" with the given bit vector. In case the sizes of the bit vectors do not match, + * only the matching portion is considered and the overlapping bits are set to 0. + * + * @param other A reference to the bit vector to use for the operation. * @return A bit vector corresponding to the logical "or" of the two bit vectors. */ - BitVector operator|(BitVector const& bv) const; + BitVector operator|(BitVector const& other) const; /*! - * Performs a logical "or" with the given bit vector and assigns the result to the - * current bit vector. In case the sizes of the bit vectors do not match, - * only the matching portion is considered and the overlapping bits are set to 0. - * @param bv A reference to the bit vector to use for the operation. + * Performs a logical "or" with the given bit vector and assigns the result to the current bit vector. + * In case the sizes of the bit vectors do not match, only the matching portion is considered and the + * overlapping bits are set to 0. + * + * @param other A reference to the bit vector to use for the operation. * @return A reference to the current bit vector corresponding to the logical "or" * of the two bit vectors. */ - BitVector& operator|=(BitVector const& bv); + BitVector& operator|=(BitVector const& other); /*! - * Performs a logical "xor" with the given bit vector. In case the sizes of the bit vectors - * do not match, only the matching portion is considered and the overlapping bits - * are set to 0. - * @param bv A reference to the bit vector to use for the operation. + * Performs a logical "xor" with the given bit vector. In case the sizes of the bit vectors do not match, + * only the matching portion is considered and the overlapping bits are set to 0. + * + * @param other A reference to the bit vector to use for the operation. * @return A bit vector corresponding to the logical "xor" of the two bit vectors. */ - BitVector operator^(BitVector const& bv) const; + BitVector operator^(BitVector const& other) const; + + /*! + * Computes a bit vector that is as long as the number of set bits in the given filter that has bit i is set + * iff the i-th set bit of the current bit vector is set in the filter. + * + * @param filter A reference the bit vector to use as the filter. + * @return A bit vector that is as long as the number of set bits in the given filter that has bit i is set + * iff the i-th set bit of the current bit vector is set in the filter. + */ + BitVector operator%(BitVector const& filter) const; /*! * Performs a logical "not" on the bit vector. + * * @return A bit vector corresponding to the logical "not" of the bit vector. */ BitVector operator~() const; @@ -243,63 +272,58 @@ namespace storm { void complement(); /*! - * Performs a logical "implies" with the given bit vector. In case the sizes of the bit vectors - * do not match, only the matching portion is considered and the overlapping bits - * are set to 0. + * Performs a logical "implies" with the given bit vector. In case the sizes of the bit vectors do not + * match, only the matching portion is considered and the overlapping bits are set to 0. * - * @param bv A reference to the bit vector to use for the operation. + * @param other A reference to the bit vector to use for the operation. * @return A bit vector corresponding to the logical "implies" of the two bit vectors. */ - BitVector implies(BitVector const& bv) const; + BitVector implies(BitVector const& other) const; /*! - * Checks whether all bits that are set in the current bit vector are also set in the given bit - * vector. + * Checks whether all bits that are set in the current bit vector are also set in the given bit vector. * - * @param bv A reference to the bit vector whose bits are (possibly) a superset of the bits of + * @param other A reference to the bit vector whose bits are (possibly) a superset of the bits of * the current bit vector. * @return True iff all bits that are set in the current bit vector are also set in the given bit * vector. */ - bool isSubsetOf(BitVector const& bv) const; + bool isSubsetOf(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 vector. + * Checks whether none of the bits that are set in the current bit vector are also set in the given bit + * vector. * - * @param bv A reference to the bit vector whose bits are (possibly) disjoint from the bits in + * @param other A reference to the bit vector whose bits are (possibly) disjoint from the bits in * the current bit vector. - * @returns True iff none of the bits that are set in the current bit vector are also set in the + * @return True iff none of the bits that are set in the current bit vector are also set in the * given bit vector. */ - bool isDisjointFrom(BitVector const& bv) const; + bool isDisjointFrom(BitVector const& other) const; /*! - * Computes a bit vector such that bit i is set iff the i-th set bit of the current bit vector is also contained - * in the given bit vector. + * Retrieves whether no bits are set to true in this bit vector. * - * @param bv A reference the bit vector to be used. - * @return A bit vector whose i-th bit is set iff the i-th set bit of the current bit vector is also contained - * in the given bit vector. + * @return False iff there is at least one bit set in this vector. */ - BitVector operator%(BitVector const& bv) const; + bool empty() const; /*! - * Retrieves whether there is at least one bit set in the vector. + * Retrievs whether all bits are set in this bit vector. * - * @return True if there is at least one bit set in this vector. + * @return True iff all bits in the bit vector are set. */ - bool empty() const; + bool full() const; /*! - * Removes all set bits from the bit vector. + * Removes all set bits from the bit vector. Calling empty() after this operation will yield true. */ void clear(); /*! - * Returns the number of bits that are set (to one) in this bit vector. + * Returns the number of bits that are set to true in this bit vector. * - * @return The number of bits that are set (to one) in this bit vector. + * @return The number of bits that are set to true in this bit vector. */ uint_fast64_t getNumberOfSetBits() const; @@ -336,19 +360,19 @@ namespace storm { const_iterator end() const; /*! - * Calculates a hash over all values contained in this Sparse Matrix. - * @return size_t A Hash Value + * Calculates a hash value for this bit vector. + * + * @return The hash value of this bit vector. */ std::size_t hash() const; /* - * Retrieves the index of the bit that is the next bit set to true in the bit vector. If there - * is none, this function returns the number of bits this vector holds in total. - * Put differently, if the return value is equal to a call to size(), then there is - * no bit set after the specified position. + * Retrieves the index of the bit that is the next bit set to true in the bit vector. If there is none, + * this function returns the number of bits this vector holds in total. Put differently, if the return + * value is equal to a call to size(), then there is no bit set after the specified position. * * @param startingIndex The index at which to start the search for the next bit that is set. The - * bit at this index itself is not considered. + * bit at this index itself is already considered. * @return The index of the next bit that is set after the given index. */ uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const; @@ -356,37 +380,29 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); private: - /*! - * Retrieves the index of the bit that is set after the given starting index, - * but before the given end index in the given bit vector. - * @param bitVector The bit vector to search. + * Retrieves the index of the next bit that is set to true after (and including) the given starting index. + * + * @param dataPtr A pointer to the first bucket of the data storage. * @param startingIndex The index where to start the search. - * @param endIndex The end index at which to stop the search. - * @return The index of the bit that is set after the given starting index, - * but before the given end index in the given bit vector or endIndex in case - * the end index was reached. + * @param endIndex The index at which to stop the search. + * @return The index of the bit that is set after the given starting index, but before the given end index + * in the given bit vector or endIndex in case the end index was reached. */ - uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex, uint_fast64_t endIndex) const; + static uint_fast64_t getNextSetIndex(uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex); /*! - * Truncate the last bucket so that no bits are set in the range starting from (bitCount + 1). + * Truncate the last bucket so that no bits are set starting from bitCount. */ void truncateLastBucket(); - - /*! - * Updates internal structures in case the size of the bit vector changed. Needs to be called - * after the size of the bit vector changed. - */ - void updateSizeChange(); - - /*! The number of bits that have to be stored */ + + // The number of bits that this bit vector can hold. uint_fast64_t bitCount; - /*! Array of 64-bit buckets to store the bits. */ + // The underlying storage of 64-bit buckets for all bits of this bit vector. std::vector bucketVector; - /*! A bit mask that can be used to reduce a modulo operation to a logical "and". */ + // A bit mask that can be used to reduce a modulo 64 operation to a logical "and". static const uint_fast64_t mod64mask = (1 << 6) - 1; }; diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp index 2127b73da..226c44421 100644 --- a/test/functional/storage/BitVectorTest.cpp +++ b/test/functional/storage/BitVectorTest.cpp @@ -1,114 +1,412 @@ #include "gtest/gtest.h" #include "src/storage/BitVector.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/OutOfRangeException.h" -TEST(BitVectorTest, GetSetTest) { - storm::storage::BitVector *bv = NULL; - ASSERT_NO_THROW(bv = new storm::storage::BitVector(32)); +TEST(BitVectorTest, InitToZeroTest) { + storm::storage::BitVector vector(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + ASSERT_FALSE(vector.get(i)); + } + + ASSERT_TRUE(vector.empty()); + ASSERT_FALSE(vector.full()); +} - for (int i = 0; i < 32; ++i) { - bv->set(i, i % 2 == 0); +TEST(BitVectorTest, InitToOneTest) { + storm::storage::BitVector vector(32, true); + + for (uint_fast64_t i = 0; i < 32; ++i) { + ASSERT_TRUE(vector.get(i)); } + ASSERT_FALSE(vector.empty()); + ASSERT_TRUE(vector.full()); +} - for (int i = 0; i < 32; ++i) { - ASSERT_EQ(bv->get(i), i % 2 == 0); +TEST(BitVectorTest, InitFromIteratorTest) { + std::vector valueVector = {0, 4, 10}; + storm::storage::BitVector vector(32, valueVector.begin(), valueVector.end()); + + ASSERT_EQ(vector.size(), 32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + if (i == 0 || i == 4 || i == 10) { + ASSERT_TRUE(vector.get(i)); + } else { + ASSERT_FALSE(vector.get(i)); + } } - delete bv; } -TEST(BitVectorTest, InitialZeroTest) { - storm::storage::BitVector bvA(32); +TEST(BitVectorTest, GetSetTest) { + storm::storage::BitVector vector(32); - for (int i = 0; i < 32; ++i) { - ASSERT_FALSE(bvA.get(i)); + for (uint_fast64_t i = 0; i < 32; ++i) { + vector.set(i, i % 2 == 0); } + + for (uint_fast64_t i = 0; i < 32; ++i) { + ASSERT_EQ(vector.get(i), i % 2 == 0); + } +} + +TEST(BitVectorTest, GetSetExceptionTest) { + storm::storage::BitVector vector(32); + + ASSERT_THROW(vector.get(32), storm::exceptions::OutOfRangeException); + ASSERT_THROW(vector.set(32), storm::exceptions::OutOfRangeException); } TEST(BitVectorTest, ResizeTest) { - storm::storage::BitVector bvA(32); + storm::storage::BitVector vector(32); - for (int i = 0; i < 32; ++i) { - bvA.set(i, true); + for (uint_fast64_t i = 0; i < 32; ++i) { + vector.set(i); } - bvA.resize(70); + vector.resize(70); + + ASSERT_EQ(vector.size(), 70); + ASSERT_EQ(vector.getNumberOfSetBits(), 32); - for (int i = 0; i < 32; ++i) { - ASSERT_TRUE(bvA.get(i)); + for (uint_fast64_t i = 0; i < 32; ++i) { + ASSERT_TRUE(vector.get(i)); } - bool result; - for (int i = 32; i < 70; ++i) { + for (uint_fast64_t i = 32; i < 70; ++i) { result = true; - ASSERT_NO_THROW(result = bvA.get(i)); + ASSERT_NO_THROW(result = vector.get(i)); ASSERT_FALSE(result); } + + vector.resize(72, true); + + ASSERT_EQ(vector.size(), 72); + ASSERT_EQ(vector.getNumberOfSetBits(), 34); + + for (uint_fast64_t i = 0; i < 32; ++i) { + ASSERT_TRUE(vector.get(i)); + } + for (uint_fast64_t i = 32; i < 70; ++i) { + result = true; + ASSERT_NO_THROW(result = vector.get(i)); + ASSERT_FALSE(result); + } + for (uint_fast64_t i = 70; i < 72; ++i) { + ASSERT_TRUE(vector.get(i)); + } + + vector.resize(16, 0); + ASSERT_EQ(vector.size(), 16); + ASSERT_EQ(vector.getNumberOfSetBits(), 16); + + for (uint_fast64_t i = 0; i < 16; ++i) { + ASSERT_TRUE(vector.get(i)); + } + + vector.resize(65, 1); + ASSERT_EQ(vector.size(), 65); + ASSERT_TRUE(vector.full()); } -TEST(BitVectorTest, OperatorNotTest) { - storm::storage::BitVector bvA(32); - storm::storage::BitVector bvB(32); +TEST(BitVectorTest, OperatorAndTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32); + + for (int i = 0; i < 32; ++i) { + vector1.set(i, i % 2 == 0); + vector2.set(i, i % 2 == 1); + } + vector1.set(31); + vector2.set(31); + + storm::storage::BitVector andResult = vector1 & vector2; + + for (uint_fast64_t i = 0; i < 31; ++i) { + ASSERT_FALSE(andResult.get(i)); + } + ASSERT_TRUE(andResult.get(31)); +} +TEST(BitVectorTest, OperatorAndEqualTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32); + for (int i = 0; i < 32; ++i) { - bvA.set(i, i % 2 == 0); - bvB.set(i, i % 2 == 1); + vector1.set(i, i % 2 == 0); + vector2.set(i, i % 2 == 1); + } + vector1.set(31); + vector2.set(31); + + vector1 &= vector2; + + for (uint_fast64_t i = 0; i < 31; ++i) { + ASSERT_FALSE(vector1.get(i)); } + ASSERT_TRUE(vector1.get(31)); +} - storm::storage::BitVector bvN = ~bvB; - for (int i = 0; i < 32; ++i) { - ASSERT_EQ(bvA.get(i), bvN.get(i)); +TEST(BitVectorTest, OperatorOrTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector1.set(i, i % 2 == 0); + vector2.set(i, i % 2 == 1); + } + vector1.set(31, false); + vector2.set(31, false); + + storm::storage::BitVector orResult = vector1 | vector2; + + for (uint_fast64_t i = 0; i < 31; ++i) { + ASSERT_TRUE(orResult.get(i)); } + ASSERT_FALSE(orResult.get(31)); } -TEST(BitVectorTest, OperatorAndTest) { - storm::storage::BitVector bvA(32); - storm::storage::BitVector bvB(32); +TEST(BitVectorTest, OperatorOrEqualTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector1.set(i, i % 2 == 0); + vector2.set(i, i % 2 == 1); + } + vector1.set(31, false); + vector2.set(31, false); + + vector1 |= vector2; + + for (uint_fast64_t i = 0; i < 31; ++i) { + ASSERT_TRUE(vector1.get(i)); + } + ASSERT_FALSE(vector1.get(31)); +} - for (int i = 0; i < 32; ++i) { - bvA.set(i, i % 2 == 0); - bvB.set(i, i % 2 == 1); +TEST(BitVectorTest, OperatorXorTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector1.set(i); + vector2.set(i, i % 2 == 1); + } + + storm::storage::BitVector vector3 = vector1 ^ vector2; + storm::storage::BitVector vector4 = ~vector2; + storm::storage::BitVector vector5 = vector1 ^ vector1; + + for (uint_fast64_t i = 0; i < 32; ++i) { + ASSERT_EQ(vector3.get(i), vector4.get(i)); + ASSERT_FALSE(vector5.get(i)); } +} - storm::storage::BitVector bvN = bvA & bvB; +TEST(BitVectorTest, OperatorModuloTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32); + + for (uint_fast64_t i = 0; i < 15; ++i) { + vector2.set(i, i % 2 == 0); + } + + vector1.set(2); + vector1.set(5); + vector1.set(6); + + storm::storage::BitVector moduloResult = vector1 % vector2; + + ASSERT_EQ(moduloResult.size(), 8); + ASSERT_EQ(moduloResult.getNumberOfSetBits(), 2); + + for (uint_fast64_t i = 0; i < 8; ++i) { + if (i == 1 || i == 3) { + ASSERT_TRUE(moduloResult.get(i)); + } else { + ASSERT_FALSE(moduloResult.get(i)); + } + } + + storm::storage::BitVector vector3(31); + + for (uint_fast64_t i = 0; i < 15; ++i) { + vector3.set(i, i % 2 == 0); + } + + ASSERT_THROW(vector1 % vector3, storm::exceptions::InvalidArgumentException); +} - for (int i = 0; i < 32; ++i) { - ASSERT_FALSE(bvN.get(i)); +TEST(BitVectorTest, OperatorNotTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector1.set(i, i % 2 == 0); + vector2.set(i, i % 2 == 1); + } + + storm::storage::BitVector notResult = ~vector2; + + for (uint_fast64_t i = 0; i < 32; ++i) { + ASSERT_EQ(vector1.get(i), notResult.get(i)); } } -TEST(BitVectorTest, OperatorOrTest) { - storm::storage::BitVector bvA(32); - storm::storage::BitVector bvB(32); +TEST(BitVectorTest, ComplementTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector1.set(i, i % 2 == 0); + vector2.set(i, i % 2 == 1); + } + + vector2.complement(); + + for (uint_fast64_t i = 0; i < 32; ++i) { + ASSERT_EQ(vector1.get(i), vector2.get(i)); + } +} - for (int i = 0; i < 32; ++i) { - bvA.set(i, i % 2 == 0); - bvB.set(i, i % 2 == 1); +TEST(BitVectorTest, ImpliesTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32, true); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector1.set(i, i % 2 == 0); } + vector2.set(31, false); + vector2.set(30, false); + + storm::storage::BitVector impliesResult = vector1.implies(vector2); + + for (uint_fast64_t i = 0; i < 30; ++i) { + ASSERT_TRUE(impliesResult.get(i)); + } + ASSERT_FALSE(impliesResult.get(30)); + ASSERT_TRUE(impliesResult.get(31)); +} - storm::storage::BitVector bvN = bvA | bvB; +TEST(BitVectorTest, SubsetTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32, true); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector1.set(i, i % 2 == 0); + } - for (int i = 0; i < 32; ++i) { - ASSERT_TRUE(bvN.get(i)); + ASSERT_TRUE(vector1.isSubsetOf(vector2)); + + vector2.set(16, false); + + ASSERT_FALSE(vector1.isSubsetOf(vector2)); +} + +TEST(BitVectorTest, DisjointTest) { + storm::storage::BitVector vector1(32); + storm::storage::BitVector vector2(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector1.set(i, i % 2 == 0); + vector2.set(i, i % 2 == 1); } + + ASSERT_TRUE(vector1.isDisjointFrom(vector2)); + + vector2.set(16, true); + + ASSERT_FALSE(vector1.isDisjointFrom(vector2)); } -TEST(BitVectorTest, OperatorXorTest) { - storm::storage::BitVector bvA(32); - storm::storage::BitVector bvB(32); +TEST(BitVectorTest, EmptyTest) { + storm::storage::BitVector vector(32); + + ASSERT_TRUE(vector.empty()); + + vector.set(17, true); + + ASSERT_FALSE(vector.empty()); + + vector.set(17, false); + vector.set(18, false); + + ASSERT_TRUE(vector.empty()); +} - for (int i = 0; i < 32; ++i) { - bvA.set(i, true); - bvB.set(i, i % 2 == 1); +TEST(BitVectorTest, FullTest) { + storm::storage::BitVector vector(32, true); + + ASSERT_TRUE(vector.full()); + + vector.set(17, false); + + ASSERT_FALSE(vector.full()); + + vector.set(17, true); + vector.set(18, true); + + ASSERT_TRUE(vector.full()); +} + +TEST(BitVectorTest, NumberOfSetBitsTest) { + storm::storage::BitVector vector(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector.set(i, i % 2 == 0); } - storm::storage::BitVector bvN = bvA ^ bvB; - storm::storage::BitVector bvO = ~bvB; - storm::storage::BitVector bvP = bvA ^ bvA; + ASSERT_EQ(vector.getNumberOfSetBits(), 16); +} - for (int i = 0; i < 32; ++i) { - ASSERT_EQ(bvN.get(i), bvO.get(i)); - // A XOR A = 0 - ASSERT_FALSE(bvP.get(i)); +TEST(BitVectorTest, NumberOfSetBitsBeforeIndexTest) { + storm::storage::BitVector vector(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector.set(i, i % 2 == 0); } + + ASSERT_EQ(vector.getNumberOfSetBitsBeforeIndex(14), 7); +} + +TEST(BitVectorTest, BeginEndTest) { + storm::storage::BitVector vector(32); + + ASSERT_TRUE(vector.begin() == vector.end()); + + vector.set(17); + + ASSERT_FALSE(vector.begin() == vector.end()); + + vector.set(17, false); + + ASSERT_TRUE(vector.begin() == vector.end()); } + +TEST(BitVectorTest, NextSetIndexTest) { + storm::storage::BitVector vector(32); + + vector.set(14); + vector.set(17); + + ASSERT_EQ(vector.getNextSetIndex(14), 14); + ASSERT_EQ(vector.getNextSetIndex(15), 17); + ASSERT_EQ(vector.getNextSetIndex(16), 17); + ASSERT_EQ(vector.getNextSetIndex(17), 17); + ASSERT_EQ(vector.getNextSetIndex(18), vector.size()); +} + +TEST(BitVectorTest, IteratorTest) { + storm::storage::BitVector vector(32); + + for (uint_fast64_t i = 0; i < 32; ++i) { + vector.set(i, i % 2 == 0); + } + + for (auto bit : vector) { + ASSERT_TRUE(bit % 2 == 0); + } +} \ No newline at end of file