diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 6f9cc4d73..f6598a7a2 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -414,8 +414,8 @@ namespace storm { if (bitIndexInBucket + numberOfBits < 64) { // If the value stops before the end of the bucket, we need to erase some lower bits. - mask &= ~((1ull << (64 - (bitIndexInBucket - numberOfBits + 2))) - 1); - return (bucketVector[bucket] & mask) >> (64 - (bitIndexInBucket - numberOfBits + 2)); + mask &= ~((1ull << (64 - (bitIndexInBucket + numberOfBits))) - 1ull); + return (bucketVector[bucket] & mask) >> (64 - (bitIndexInBucket + numberOfBits)); } else if (bitIndexInBucket + numberOfBits > 64) { // In this case, the integer "crosses" the bucket line. uint64_t result = (bucketVector[bucket] & mask); @@ -440,6 +440,42 @@ namespace storm { } } + void BitVector::setFromInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits, uint64_t value) { + STORM_LOG_ASSERT((value >> numberOfBits) == 0, "Integer value to large to fit in the given number of bits."); + + uint64_t bucket = bitIndex >> 6; + uint64_t bitIndexInBucket = bitIndex & mod64mask; + + uint64_t mask; + if (bitIndexInBucket == 0) { + mask = -1ull; + } else { + mask = (1ull << (64 - bitIndexInBucket)) - 1ull; + } + + if (bitIndexInBucket + numberOfBits < 64) { + // If the value stops before the end of the bucket, we need to erase some lower bits. + mask &= ~((1ull << (64 - (bitIndexInBucket + numberOfBits))) - 1ull); + bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value << (64 - (bitIndexInBucket + numberOfBits))); + } else if (bitIndexInBucket + numberOfBits > 64) { + // Write the part of the value that falls into the first bucket. + bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value >> (64 - bitIndexInBucket)); + ++bucket; + + // Compute the remaining number of bits. + numberOfBits -= (64 - bitIndexInBucket); + + // Shift the bits of the value such that the already set bits disappear. + value <<= (64 - numberOfBits); + + // Put the remaining bits in their place. + mask = ((1ull << (64 - numberOfBits)) - 1ull); + bucketVector[bucket] = (bucketVector[bucket] & mask) | value; + } else { + bucketVector[bucket] = (bucketVector[bucket] & ~mask) | value; + } + } + bool BitVector::empty() const { for (auto& element : bucketVector) { if (element != 0) { diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index d8fc7e51a..f5b0f6de9 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -358,6 +358,15 @@ namespace storm { */ uint_fast64_t getAsInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const; + /*! + * Sets the selected number of lowermost bits of the provided value at the given bit index. + * + * @param bitIndex The index of the first bit to set. + * @param numberOfBits The number of bits to set. + * @param value The integer whose lowermost bits to set. + */ + void setFromInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits, uint64_t value); + /*! * Retrieves whether no bits are set to true in this bit vector. * diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp index a90558524..0854f364e 100644 --- a/test/functional/storage/BitVectorTest.cpp +++ b/test/functional/storage/BitVectorTest.cpp @@ -70,6 +70,42 @@ TEST(BitVectorTest, GetAsInt) { EXPECT_EQ(3, vector.getAsInt(62, 2)); EXPECT_EQ(6, vector.getAsInt(62, 3)); EXPECT_EQ(13, vector.getAsInt(62, 4)); + + vector.set(61); + vector.set(62, false); + EXPECT_EQ(2, vector.getAsInt(61, 2)); +} + +TEST(BitVectorTest, SetFromInt) { + storm::storage::BitVector vector(77); + + vector.setFromInt(62, 1, 1); + + EXPECT_TRUE(vector.get(62)); + EXPECT_FALSE(vector.get(63)); + EXPECT_FALSE(vector.get(64)); + EXPECT_FALSE(vector.get(65)); + + vector.setFromInt(61, 2, 2); + + EXPECT_TRUE(vector.get(61)); + EXPECT_FALSE(vector.get(62)); + EXPECT_FALSE(vector.get(63)); + + vector.setFromInt(61, 3, 5); + + EXPECT_TRUE(vector.get(61)); + EXPECT_FALSE(vector.get(62)); + EXPECT_TRUE(vector.get(63)); + + vector.setFromInt(62, 4, 15); + + EXPECT_TRUE(vector.get(62)); + EXPECT_TRUE(vector.get(63)); + EXPECT_TRUE(vector.get(64)); + EXPECT_TRUE(vector.get(65)); + + vector.setFromInt(62, 5, 17); } TEST(BitVectorDeathTest, GetSetAssertion) {