Browse Source

Finalized interface of bit vector. Added unit tests for all methods of the bit vector.

Former-commit-id: 6c7834ed20
main
dehnert 12 years ago
parent
commit
d5cadc0f4b
  1. 8
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  2. 2
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  3. 2
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  4. 2
      src/models/AtomicPropositionsLabeling.h
  5. 157
      src/storage/BitVector.cpp
  6. 288
      src/storage/BitVector.h
  7. 418
      test/functional/storage/BitVectorTest.cpp

8
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@ -209,10 +209,10 @@ namespace storm {
std::vector<ValueType> vAllMarkovian(markovianStates.getNumberOfSetBits()); std::vector<ValueType> vAllMarkovian(markovianStates.getNumberOfSetBits());
// Create the starting value vectors for the next value iteration based on the results of the previous one. // Create the starting value vectors for the next value iteration based on the results of the previous one.
storm::utility::vector::setVectorValues<ValueType>(vAllProbabilistic, ~markovianStates % goalStates, storm::utility::constGetOne<ValueType>()); storm::utility::vector::setVectorValues<ValueType>(vAllProbabilistic, goalStates % ~markovianStates, storm::utility::constGetOne<ValueType>());
storm::utility::vector::setVectorValues<ValueType>(vAllProbabilistic, ~markovianStates % ~goalStates, vProbabilistic); storm::utility::vector::setVectorValues<ValueType>(vAllProbabilistic, ~goalStates % ~markovianStates, vProbabilistic);
storm::utility::vector::setVectorValues<ValueType>(vAllMarkovian, markovianStates % goalStates, storm::utility::constGetOne<ValueType>()); storm::utility::vector::setVectorValues<ValueType>(vAllMarkovian, goalStates % markovianStates, storm::utility::constGetOne<ValueType>());
storm::utility::vector::setVectorValues<ValueType>(vAllMarkovian, markovianStates % ~goalStates, vMarkovian); storm::utility::vector::setVectorValues<ValueType>(vAllMarkovian, ~goalStates % markovianStates, vMarkovian);
// Compute the number of steps to reach the target interval. // Compute the number of steps to reach the target interval.
numberOfSteps = static_cast<uint_fast64_t>(std::ceil(lowerBound / delta)); numberOfSteps = static_cast<uint_fast64_t>(std::ceil(lowerBound / delta));

2
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@ -127,7 +127,7 @@ public:
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0); storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0);
// Compute the new set of target states in the reduced system. // 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. // Make all rows absorbing that satisfy the second sub-formula.
submatrix.makeRowsAbsorbing(rightStatesInReducedSystem); submatrix.makeRowsAbsorbing(rightStatesInReducedSystem);

2
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@ -119,7 +119,7 @@ namespace storm {
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), statesWithProbabilityGreater0); std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), statesWithProbabilityGreater0);
// Compute the new set of target states in the reduced system. // 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. // Make all rows absorbing that satisfy the second sub-formula.
submatrix.makeRowsAbsorbing(rightStatesInReducedSystem, subNondeterministicChoiceIndices); submatrix.makeRowsAbsorbing(rightStatesInReducedSystem, subNondeterministicChoiceIndices);

2
src/models/AtomicPropositionsLabeling.h

@ -71,7 +71,7 @@ public:
// Now we need to copy the fraction of the single labelings given by the substates. // Now we need to copy the fraction of the single labelings given by the substates.
singleLabelings.reserve(apCountMax); singleLabelings.reserve(apCountMax);
for (auto const& labeling : atomicPropositionsLabeling.singleLabelings) { for (auto const& labeling : atomicPropositionsLabeling.singleLabelings) {
singleLabelings.emplace_back(labeling, substates); singleLabelings.emplace_back(labeling % substates);
} }
} }

157
src/storage/BitVector.cpp

@ -13,17 +13,31 @@ extern log4cplus::Logger logger;
namespace storm { namespace storm {
namespace storage { 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) { if (setOnFirstBit) {
// Set the index of the first set bit in the vector. // Set the index of the first set bit in the vector.
currentIndex = bitVector.getNextSetIndex(startIndex, endIndex); currentIndex = getNextSetIndex(dataPtr, startIndex, endIndex);
} else { } else {
currentIndex = startIndex; 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++() { BitVector::const_iterator& BitVector::const_iterator::operator++() {
currentIndex = bitVector.getNextSetIndex(++currentIndex, endIndex); currentIndex = getNextSetIndex(dataPtr, ++currentIndex, endIndex);
return *this; return *this;
} }
@ -31,19 +45,19 @@ namespace storm {
return currentIndex; return currentIndex;
} }
bool BitVector::const_iterator::operator!=(const_iterator const& otherIterator) const { bool BitVector::const_iterator::operator!=(const_iterator const& other) const {
return currentIndex != otherIterator.currentIndex; return currentIndex != other.currentIndex;
} }
bool BitVector::const_iterator::operator==(const_iterator const& otherIterator) const { bool BitVector::const_iterator::operator==(const_iterator const& other) const {
return currentIndex == otherIterator.currentIndex; return currentIndex == other.currentIndex;
} }
BitVector::BitVector() : bitCount(0), bucketVector() { BitVector::BitVector() : bitCount(0), bucketVector() {
// Intentionally left empty. // 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. // Compute the correct number of buckets needed to store the given number of bits.
uint_fast64_t bucketCount = length >> 6; uint_fast64_t bucketCount = length >> 6;
if ((length & mod64mask) != 0) { if ((length & mod64mask) != 0) {
@ -51,7 +65,7 @@ namespace storm {
} }
// Initialize the storage with the required values. // Initialize the storage with the required values.
if (initTrue) { if (init) {
bucketVector = std::vector<uint64_t>(bucketCount, -1ll); bucketVector = std::vector<uint64_t>(bucketCount, -1ll);
truncateLastBucket(); truncateLastBucket();
} else { } else {
@ -68,21 +82,6 @@ namespace storm {
// Intentionally left empty. // 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<uint64_t>(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)) { BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), bucketVector(std::move(other.bucketVector)) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -92,7 +91,6 @@ namespace storm {
if (this != &other) { if (this != &other) {
bitCount = other.bitCount; bitCount = other.bitCount;
bucketVector = std::vector<uint64_t>(other.bucketVector); bucketVector = std::vector<uint64_t>(other.bucketVector);
updateSizeChange();
} }
return *this; return *this;
} }
@ -102,7 +100,6 @@ namespace storm {
if (this != &other) { if (this != &other) {
bitCount = other.bitCount; bitCount = other.bitCount;
bucketVector = std::move(other.bucketVector); bucketVector = std::move(other.bucketVector);
updateSizeChange();
} }
return *this; return *this;
@ -153,7 +150,7 @@ namespace storm {
return (*this)[index]; return (*this)[index];
} }
void BitVector::resize(uint_fast64_t newLength, bool initTrue) { void BitVector::resize(uint_fast64_t newLength, bool init) {
if (newLength > bitCount) { if (newLength > bitCount) {
uint_fast64_t newBucketCount = newLength >> 6; uint_fast64_t newBucketCount = newLength >> 6;
if ((newLength & mod64mask) != 0) { if ((newLength & mod64mask) != 0) {
@ -161,8 +158,8 @@ namespace storm {
} }
if (newBucketCount > bucketVector.size()) { if (newBucketCount > bucketVector.size()) {
if (initTrue) { if (init) {
bucketVector.back() |= (1ll << (bitCount * 64 - bitCount * 63 - bitCount & mod64mask)) - 1ll; bucketVector.back() |= ~((1ll << (bitCount & mod64mask)) - 1ll);
bucketVector.resize(newBucketCount, -1ll); bucketVector.resize(newBucketCount, -1ll);
} else { } else {
bucketVector.resize(newBucketCount, 0); bucketVector.resize(newBucketCount, 0);
@ -170,14 +167,12 @@ namespace storm {
bitCount = newLength; bitCount = newLength;
} else { } else {
// If the underlying storage does not need to grow, we have to insert the missing bits. // If the underlying storage does not need to grow, we have to insert the missing bits.
if (initTrue) { if (init) {
bucketVector.back() |= (1ll << (bitCount * 64 - bitCount * 63 - bitCount & mod64mask)) - 1ll; bucketVector.back() |= ~((1ll << (bitCount & mod64mask)) - 1ll);
bitCount = newLength;
} else {
bitCount = newLength;
} }
bitCount = newLength;
} }
updateSizeChange(); truncateLastBucket();
} else { } else {
bitCount = newLength; bitCount = newLength;
bitCount = newLength; bitCount = newLength;
@ -187,7 +182,7 @@ namespace storm {
} }
bucketVector.resize(newBucketCount); bucketVector.resize(newBucketCount);
updateSizeChange(); truncateLastBucket();
} }
} }
@ -252,6 +247,36 @@ namespace storm {
return result; 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 BitVector::operator~() const {
BitVector result(this->bitCount); BitVector result(this->bitCount);
std::vector<uint64_t>::iterator it = result.bucketVector.begin(); std::vector<uint64_t>::iterator it = result.bucketVector.begin();
@ -309,43 +334,27 @@ namespace storm {
return true; return true;
} }
BitVector BitVector::operator%(BitVector const& other) const { bool BitVector::empty() const {
if (bitCount != other.bitCount) { for (auto& element : bucketVector) {
throw storm::exceptions::InvalidArgumentException() << "Invalid call to BitVector::operator%: length mismatch of operands."; if (element != 0) {
} return false;
// 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));
}
} }
} }
return true;
return result;
} }
bool BitVector::empty() const { bool BitVector::full() const {
for (auto& element : bucketVector) { // Check that all buckets except the last one have all bits set.
if (element != 0) { for (uint_fast64_t index = 0; index < bucketVector.size() - 1; ++index) {
if (bucketVector[index] != -1ll) {
return false; 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; return true;
} }
@ -412,11 +421,11 @@ namespace storm {
} }
BitVector::const_iterator BitVector::begin() const { 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 { 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 { std::size_t BitVector::hash() const {
@ -433,13 +442,13 @@ namespace storm {
} }
uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex) const { 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; uint_fast8_t currentBitInByte = startingIndex & mod64mask;
startingIndex >>= 6; startingIndex >>= 6;
std::vector<uint64_t>::const_iterator bucketIt = bucketVector.begin() + startingIndex; uint64_t const* bucketIt = dataPtr + startingIndex;
while ((startingIndex << 6) < endIndex) { while ((startingIndex << 6) < endIndex) {
// Compute the remaining bucket content by a right shift // Compute the remaining bucket content by a right shift
@ -473,11 +482,7 @@ namespace storm {
bucketVector.back() &= (1ll << (bitCount & mod64mask)) - 1ll; bucketVector.back() &= (1ll << (bitCount & mod64mask)) - 1ll;
} }
} }
void BitVector::updateSizeChange() {
truncateLastBucket();
}
std::ostream& operator<<(std::ostream& out, BitVector const& bitVector) { std::ostream& operator<<(std::ostream& out, BitVector const& bitVector) {
out << "bit vector(" << bitVector.getNumberOfSetBits() << "/" << bitVector.bitCount << ") ["; out << "bit vector(" << bitVector.getNumberOfSetBits() << "/" << bitVector.bitCount << ") [";
for (auto index : bitVector) { for (auto index : bitVector) {

288
src/storage/BitVector.h

@ -16,8 +16,8 @@ namespace storm {
class BitVector { class BitVector {
public: public:
/*! /*!
* A class that enables iterating over the indices of the bit vector whose corresponding bits are set to true. * A class that enables iterating over the indices of the bit vector whose corresponding bits are set to
* Note that this is a const iterator, which cannot alter the bit vector. * true. Note that this is a const iterator, which cannot alter the bit vector.
*/ */
class const_iterator : public std::iterator<std::input_iterator_tag, uint_fast64_t> { class const_iterator : public std::iterator<std::input_iterator_tag, uint_fast64_t> {
// Declare the BitVector class as a friend class to access its internal storage. // Declare the BitVector class as a friend class to access its internal storage.
@ -25,20 +25,34 @@ namespace storm {
public: public:
/*! /*!
* Constructs an iterator over the indices of the set bits in the given bit vector, starting and stopping, * Constructs an iterator over the indices of the set bits in the given bit vector, starting and
* respectively, at the given indices. * 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 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 * @param setOnFirstBit A flag that indicates whether the iterator is to be moved to the index of the
* bit upon construction. * first bit upon construction.
* @param endIndex The index at which to abort the iteration process. * @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 * Constructs an iterator by copying the given iterator.
* bit vector. *
* @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. * @return A reference to this iterator.
*/ */
@ -54,22 +68,22 @@ namespace storm {
/*! /*!
* Compares the iterator with another iterator for inequality. * 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. * @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. * 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. * @return True if the two iterators are equal.
*/ */
bool operator==(const_iterator const& otherIterator) const; bool operator==(const_iterator const& other) const;
private: private:
// The underlying bit vector of this iterator. // The underlying bit vector of this iterator.
BitVector const& bitVector; uint64_t const* dataPtr;
// The index of the bit this iterator currently points to. // The index of the bit this iterator currently points to.
uint_fast64_t currentIndex; uint_fast64_t currentIndex;
@ -84,155 +98,170 @@ namespace storm {
BitVector(); BitVector();
/*! /*!
* Constructs a bit vector which can hold the given number of bits and * Constructs a bit vector which can hold the given number of bits and initializes all bits with the
* initializes all bits to the provided truth value. * provided truth value.
*
* @param length The number of bits the bit vector should be able to hold. * @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 The length of the bit vector.
* @param begin The begin of the iterator range. * @param first The begin of the iterator range.
* @param end The end of the iterator range. * @param last The end of the iterator range.
*/ */
template<typename InputIterator> template<typename InputIterator>
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. * Performs a deep copy of the given bit vector.
* @param bv A reference to the bit vector to be copied. *
* @param other A reference to the bit vector to be copied.
*/ */
BitVector(BitVector const& other); 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. * 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. * Assigns the contents of the given bit vector to the current bit vector via 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 * @param other The bit vector to assign to the current bit vector.
* given bit vector by means of a deep copy. * @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. * 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. * @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 * @return A reference to this bit vector after the contents of the given bit vector have been moved
* have been moved into it. * into it.
*/ */
BitVector& operator=(BitVector&& bv); BitVector& operator=(BitVector&& other);
/*! /*!
* Sets the given truth value at the given index. * Sets the given truth value at the given index.
*
* @param index The index where to set the truth value. * @param index The index where to set the truth value.
* @param value The truth value to set. * @param value The truth value to set.
*/ */
void set(const uint_fast64_t index, bool value = true); 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 first The begin of the iterator range.
* @param end The element past the last element of the iterator range. * @param last The element past the last element of the iterator range.
*/ */
template<typename InputIterator> template<typename InputIterator>
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 * Retrieves the truth value of the bit at the given index. Note: this does not check whether the given
* given index is within bounds. * index is within bounds.
* *
* @param index The index of the bit to access. * @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; 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. * @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; 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 * Resizes the bit vector to hold the given new number of bits. If the bit vector becomes smaller this way,
* bits are truncated. Otherwise, the new bits are initialized to the given value. * 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 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 * Performs a logical "and" with the given bit vector. In case the sizes of the bit vectors do not match,
* do not match, only the matching portion is considered and the overlapping bits * only the matching portion is considered and the overlapping bits are set to 0.
* 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 "and" of the two bit vectors. * @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 * Performs a logical "and" with the given bit vector and assigns the result to the current bit vector.
* current bit vector. In case the sizes of the bit vectors do not match, * In case the sizes of the bit vectors do not match, only the matching portion is considered and the
* only the matching portion is considered and the overlapping bits are set to 0. * 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 reference to the current bit vector corresponding to the logical "and" * @return A reference to the current bit vector corresponding to the logical "and"
* of the two bit vectors. * 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 * Performs a logical "or" with the given bit vector. In case the sizes of the bit vectors do not match,
* do not match, only the matching portion is considered and the overlapping bits * only the matching portion is considered and the overlapping bits are set to 0.
* 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 "or" of the two bit vectors. * @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 * Performs a logical "or" with the given bit vector and assigns the result to the current bit vector.
* current bit vector. In case the sizes of the bit vectors do not match, * In case the sizes of the bit vectors do not match, only the matching portion is considered and the
* only the matching portion is considered and the overlapping bits are set to 0. * 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 reference to the current bit vector corresponding to the logical "or" * @return A reference to the current bit vector corresponding to the logical "or"
* of the two bit vectors. * 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 * Performs a logical "xor" with the given bit vector. In case the sizes of the bit vectors do not match,
* do not match, only the matching portion is considered and the overlapping bits * only the matching portion is considered and the overlapping bits are set to 0.
* 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 "xor" of the two bit vectors. * @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. * Performs a logical "not" on the bit vector.
*
* @return A bit vector corresponding to the logical "not" of the bit vector. * @return A bit vector corresponding to the logical "not" of the bit vector.
*/ */
BitVector operator~() const; BitVector operator~() const;
@ -243,63 +272,58 @@ namespace storm {
void complement(); void complement();
/*! /*!
* Performs a logical "implies" with the given bit vector. In case the sizes of the bit vectors * Performs a logical "implies" with the given bit vector. In case the sizes of the bit vectors do not
* do not match, only the matching portion is considered and the overlapping bits * match, only the matching portion is considered and the overlapping bits are set to 0.
* 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. * @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 * Checks whether all bits that are set in the current bit vector are also set in the given bit vector.
* 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. * the current bit vector.
* @return True iff all bits that are set in the current bit vector are also set in the given bit * @return True iff all bits that are set in the current bit vector are also set in the given bit
* vector. * 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 * Checks whether none of the bits that are set in the current bit vector are also set in the given bit
* given bit vector. * 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. * 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. * 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 * Retrieves whether no bits are set to true in this bit vector.
* in the given bit vector.
* *
* @param bv A reference the bit vector to be used. * @return False iff there is at least one bit set in this vector.
* @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.
*/ */
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(); 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; uint_fast64_t getNumberOfSetBits() const;
@ -336,19 +360,19 @@ namespace storm {
const_iterator end() const; const_iterator end() const;
/*! /*!
* Calculates a hash over all values contained in this Sparse Matrix. * Calculates a hash value for this bit vector.
* @return size_t A Hash Value *
* @return The hash value of this bit vector.
*/ */
std::size_t hash() const; 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 * Retrieves the index of the bit that is the next bit set to true in the bit vector. If there is none,
* is none, this function returns the number of bits this vector holds in total. * this function returns the number of bits this vector holds in total. Put differently, if the return
* Put differently, if the return value is equal to a call to size(), then there is * value is equal to a call to size(), then there is no bit set after the specified position.
* 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 * @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. * @return The index of the next bit that is set after the given index.
*/ */
uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const; 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); friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector);
private: private:
/*! /*!
* Retrieves the index of the bit that is set after the given starting index, * Retrieves the index of the next bit that is set to true after (and including) the given starting index.
* but before the given end index in the given bit vector. *
* @param bitVector The bit vector to search. * @param dataPtr A pointer to the first bucket of the data storage.
* @param startingIndex The index where to start the search. * @param startingIndex The index where to start the search.
* @param endIndex The end index at which to stop 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, * @return The index of the bit that is set after the given starting index, but before the given end index
* but before the given end index in the given bit vector or endIndex in case * in the given bit vector or endIndex in case the end index was reached.
* 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(); void truncateLastBucket();
// The number of bits that this bit vector can hold.
/*!
* 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 */
uint_fast64_t bitCount; 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<uint64_t> bucketVector; std::vector<uint64_t> 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; static const uint_fast64_t mod64mask = (1 << 6) - 1;
}; };

418
test/functional/storage/BitVectorTest.cpp

@ -1,114 +1,412 @@
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/OutOfRangeException.h"
TEST(BitVectorTest, GetSetTest) { TEST(BitVectorTest, InitToZeroTest) {
storm::storage::BitVector *bv = NULL; storm::storage::BitVector vector(32);
ASSERT_NO_THROW(bv = new storm::storage::BitVector(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) { TEST(BitVectorTest, InitToOneTest) {
bv->set(i, i % 2 == 0); 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) { TEST(BitVectorTest, InitFromIteratorTest) {
ASSERT_EQ(bv->get(i), i % 2 == 0); std::vector<uint_fast64_t> 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) { TEST(BitVectorTest, GetSetTest) {
storm::storage::BitVector bvA(32); storm::storage::BitVector vector(32);
for (int i = 0; i < 32; ++i) { for (uint_fast64_t i = 0; i < 32; ++i) {
ASSERT_FALSE(bvA.get(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) { TEST(BitVectorTest, ResizeTest) {
storm::storage::BitVector bvA(32); storm::storage::BitVector vector(32);
for (int i = 0; i < 32; ++i) { for (uint_fast64_t i = 0; i < 32; ++i) {
bvA.set(i, true); 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) { for (uint_fast64_t i = 0; i < 32; ++i) {
ASSERT_TRUE(bvA.get(i)); ASSERT_TRUE(vector.get(i));
} }
bool result; bool result;
for (int i = 32; i < 70; ++i) { for (uint_fast64_t i = 32; i < 70; ++i) {
result = true; result = true;
ASSERT_NO_THROW(result = bvA.get(i)); ASSERT_NO_THROW(result = vector.get(i));
ASSERT_FALSE(result); 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) { TEST(BitVectorTest, OperatorAndTest) {
storm::storage::BitVector bvA(32); storm::storage::BitVector vector1(32);
storm::storage::BitVector bvB(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) { for (int i = 0; i < 32; ++i) {
bvA.set(i, i % 2 == 0); vector1.set(i, i % 2 == 0);
bvB.set(i, i % 2 == 1); 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) { TEST(BitVectorTest, OperatorOrTest) {
ASSERT_EQ(bvA.get(i), bvN.get(i)); 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) { TEST(BitVectorTest, OperatorOrEqualTest) {
storm::storage::BitVector bvA(32); storm::storage::BitVector vector1(32);
storm::storage::BitVector bvB(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) { TEST(BitVectorTest, OperatorXorTest) {
bvA.set(i, i % 2 == 0); storm::storage::BitVector vector1(32);
bvB.set(i, i % 2 == 1); 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) { TEST(BitVectorTest, OperatorNotTest) {
ASSERT_FALSE(bvN.get(i)); 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) { TEST(BitVectorTest, ComplementTest) {
storm::storage::BitVector bvA(32); storm::storage::BitVector vector1(32);
storm::storage::BitVector bvB(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) { TEST(BitVectorTest, ImpliesTest) {
bvA.set(i, i % 2 == 0); storm::storage::BitVector vector1(32);
bvB.set(i, i % 2 == 1); 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(vector1.isSubsetOf(vector2));
ASSERT_TRUE(bvN.get(i)); 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) { TEST(BitVectorTest, EmptyTest) {
storm::storage::BitVector bvA(32); storm::storage::BitVector vector(32);
storm::storage::BitVector bvB(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) { TEST(BitVectorTest, FullTest) {
bvA.set(i, true); storm::storage::BitVector vector(32, true);
bvB.set(i, i % 2 == 1); 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; ASSERT_EQ(vector.getNumberOfSetBits(), 16);
storm::storage::BitVector bvO = ~bvB; }
storm::storage::BitVector bvP = bvA ^ bvA;
for (int i = 0; i < 32; ++i) { TEST(BitVectorTest, NumberOfSetBitsBeforeIndexTest) {
ASSERT_EQ(bvN.get(i), bvO.get(i)); storm::storage::BitVector vector(32);
// A XOR A = 0 for (uint_fast64_t i = 0; i < 32; ++i) {
ASSERT_FALSE(bvP.get(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);
}
}
|||||||
100:0
Loading…
Cancel
Save