diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index a0004263a..532e923e3 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -22,7 +22,7 @@ namespace storm { 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 = getNextSetIndex(dataPtr, startIndex, endIndex); + currentIndex = getNextIndexWithValue(true, dataPtr, startIndex, endIndex); } else { currentIndex = startIndex; } @@ -43,13 +43,13 @@ namespace storm { } BitVector::const_iterator& BitVector::const_iterator::operator++() { - currentIndex = getNextSetIndex(dataPtr, ++currentIndex, endIndex); + currentIndex = getNextIndexWithValue(true, dataPtr, ++currentIndex, endIndex); return *this; } BitVector::const_iterator& BitVector::const_iterator::operator+=(size_t n) { for(size_t i = 0; i < n; ++i) { - currentIndex = getNextSetIndex(dataPtr, ++currentIndex, endIndex); + currentIndex = getNextIndexWithValue(true, dataPtr, ++currentIndex, endIndex); } return *this; } @@ -628,10 +628,17 @@ namespace storm { } uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex) const { - return getNextSetIndex(buckets, startingIndex, bitCount); + return getNextIndexWithValue(true, buckets, startingIndex, bitCount); } - uint_fast64_t BitVector::getNextSetIndex(uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex) { + uint_fast64_t BitVector::getNextUnsetIndex(uint_fast64_t startingIndex) const { +#ifdef ASSERT_BITVECTOR + STORM_LOG_ASSERT(getNextIndexWithValue(false, buckets, startingIndex, bitCount) == (~(*this)).getNextSetIndex(startingIndex), "The result is inconsistent with the next set index of the complement of this bitvector"); +#endif + return getNextIndexWithValue(false, buckets, startingIndex, bitCount); + } + + uint_fast64_t BitVector::getNextIndexWithValue(bool value, uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex) { uint_fast8_t currentBitInByte = startingIndex & mod64mask; uint64_t const* bucketIt = dataPtr + (startingIndex >> 6); startingIndex = (startingIndex >> 6 << 6); @@ -642,31 +649,62 @@ namespace storm { } else { mask = (1ull << (64 - currentBitInByte)) - 1ull; } - while (startingIndex < endIndex) { - // Compute the remaining bucket content. - uint64_t remainingInBucket = *bucketIt & mask; - - // Check if there is at least one bit in the remainder of the bucket that is set to true. - if (remainingInBucket != 0) { - // As long as the current bit is not set, move the current bit. - while ((remainingInBucket & (1ull << (63 - currentBitInByte))) == 0) { - ++currentBitInByte; + + // For efficiency reasons, we branch on the desired value at this point + if (value) { + while (startingIndex < endIndex) { + // Compute the remaining bucket content. + uint64_t remainingInBucket = *bucketIt & mask; + + // Check if there is at least one bit in the remainder of the bucket that is set to true. + if (remainingInBucket != 0) { + // As long as the current bit is not set, move the current bit. + while ((remainingInBucket & (1ull << (63 - currentBitInByte))) == 0) { + ++currentBitInByte; + } + + // Only return the index of the set bit if we are still in the valid range. + if (startingIndex + currentBitInByte < endIndex) { + return startingIndex + currentBitInByte; + } else { + return endIndex; + } } - - // Only return the index of the set bit if we are still in the valid range. - if (startingIndex + currentBitInByte < endIndex) { - return startingIndex + currentBitInByte; - } else { - return endIndex; + + // Advance to the next bucket. + startingIndex += 64; + ++bucketIt; + mask = -1ull; + currentBitInByte = 0; + } + } else { + while (startingIndex < endIndex) { + // Compute the remaining bucket content. + uint64_t remainingInBucket = *bucketIt & mask; + + // Check if there is at least one bit in the remainder of the bucket that is set to false. + if (remainingInBucket != (-1ull & mask)) { + // As long as the current bit is not false, move the current bit. + while ((remainingInBucket & (1ull << (63 - currentBitInByte))) != 0) { + ++currentBitInByte; + } + + // Only return the index of the set bit if we are still in the valid range. + if (startingIndex + currentBitInByte < endIndex) { + return startingIndex + currentBitInByte; + } else { + return endIndex; + } } + + // Advance to the next bucket. + startingIndex += 64; + ++bucketIt; + mask = -1ull; + currentBitInByte = 0; } - - // Advance to the next bucket. - startingIndex += 64; - ++bucketIt; - mask = -1ull; - currentBitInByte = 0; } + return endIndex; } diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index ecdd03536..dccfa0830 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -477,6 +477,17 @@ namespace storm { */ uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const; + /* + * Retrieves the index of the bit that is the next bit set to false 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 unset bit after the specified position. + * + * @param startingIndex The index at which to start the search for the next bit that is not set. The + * bit at this index itself is included in the search range. + * @return The index of the next bit that is set after the given index. + */ + uint_fast64_t getNextUnsetIndex(uint_fast64_t startingIndex) const; + /* * Compare two intervals [start1, start1+length] and [start2, start2+length] and swap them if the second * one is larger than the first one. After the method the intervals are sorted in decreasing order. @@ -502,15 +513,16 @@ namespace storm { BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount); /*! - * Retrieves the index of the next bit that is set to true after (and including) the given starting index. + * Retrieves the index of the next bit that is set to the given value after (and including) the given starting index. * + * @param value the value of the bit whose index is to be found. * @param dataPtr A pointer to the first bucket of the data storage. * @param startingIndex The index where to start the search. * @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. */ - static uint_fast64_t getNextSetIndex(uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex); + static uint_fast64_t getNextIndexWithValue(bool value, uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex); /*! * Truncate the last bucket so that no bits are set starting from bitCount. diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 6bf06a4f9..76fc58a5c 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -862,19 +862,18 @@ namespace storm { template void filterVectorInPlace(std::vector& v, storm::storage::BitVector const& filter) { STORM_LOG_ASSERT(v.size() == filter.size(), "The filter size does not match the size of the input vector"); - auto vIt = v.begin(); - auto filterIt = filter.begin(); - // get the first position where the filter has a 0. - // Note that we do not have to modify the entries of v on all positions before - for (uint_fast64_t i = 0; i == *filterIt && filterIt != filter.end(); ++i) { - ++filterIt; - ++vIt; - } - for (; filterIt != filter.end(); ++filterIt) { - *vIt = std::move(v[*filterIt]); - ++vIt; + uint_fast64_t size = v.size(); + // we can start our work at the first index where the filter has value zero + uint_fast64_t firstUnsetIndex = filter.getNextUnsetIndex(0); + if (firstUnsetIndex < size) { + auto vIt = v.begin() + firstUnsetIndex; + for (uint_fast64_t index = filter.getNextSetIndex(firstUnsetIndex + 1); index != size; index = filter.getNextSetIndex(index + 1)) { + *vIt = std::move(v[index]); + ++vIt; + } + v.resize(vIt - v.begin()); + v.shrink_to_fit(); } - v.resize(vIt - v.begin()); STORM_LOG_ASSERT(v.size() == filter.getNumberOfSetBits(), "Result does not match."); } diff --git a/src/test/storage/BitVectorTest.cpp b/src/test/storage/BitVectorTest.cpp index 9d2fd60c5..0bb9847f6 100644 --- a/src/test/storage/BitVectorTest.cpp +++ b/src/test/storage/BitVectorTest.cpp @@ -482,6 +482,21 @@ TEST(BitVectorTest, NextSetIndex) { ASSERT_EQ(vector.size(), vector.getNextSetIndex(18)); } +TEST(BitVectorTest, NextUnsetIndex) { + storm::storage::BitVector vector(32); + + vector.set(14); + vector.set(17); + + vector.complement(); + + ASSERT_EQ(14ul, vector.getNextUnsetIndex(14)); + ASSERT_EQ(17ul, vector.getNextUnsetIndex(15)); + ASSERT_EQ(17ul, vector.getNextUnsetIndex(16)); + ASSERT_EQ(17ul, vector.getNextUnsetIndex(17)); + ASSERT_EQ(vector.size(), vector.getNextUnsetIndex(18)); +} + TEST(BitVectorTest, Iterator) { storm::storage::BitVector vector(32);