increment() function for BitVector

src/storm/storage/BitVector.cpp

@@ -338,6 +338,33 @@ namespace storm {
             truncateLastBucket();
         }
         
+        void BitVector::increment() {
+            uint64_t firstUnsetIndex = getNextUnsetIndex(0);
+            
+            // If there is no unset index, we clear the whole vector
+            if (firstUnsetIndex == this->bitCount) {
+                this->clear();
+            } else {
+                
+                // All previous buckets have to be set to zero
+                uint64_t bucketIndex = firstUnsetIndex >> 6;
+                std::fill_n(buckets, bucketIndex, 0);
+                
+                // modify the bucket in which the unset entry lies in
+                uint64_t& bucket = this->buckets[bucketIndex];
+                uint64_t indexInBucket = firstUnsetIndex & mod64mask;
+                if (indexInBucket > 0) {
+                    // Clear all bits before the index
+                    uint64_t mask = ~(-1ull << (64 - indexInBucket));
+                    bucket &= mask;
+                }
+                
+                // Set the bit at the index
+                uint64_t mask = 1ull << (63 - indexInBucket);
+                bucket |= mask;
+            }
+        }
+
         BitVector BitVector::implies(BitVector const& other) const {
             STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
 

src/storm/storage/BitVector.h

@@ -316,6 +316,13 @@ namespace storm {
              */
             void complement();
             
+            /*!
+             * Increments the (unsigned) number represented by this BitVector by one.
+             * @note Index 0 is assumed to be the least significant bit.
+             * @note Wraps around, i.e., incrementing 11..1 yields 00..0.
+             */
+            void increment();
+            
             /*!
              * 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.

src/test/storm/storage/BitVectorTest.cpp

@@ -74,6 +74,7 @@ TEST(BitVectorTest, GetAsInt) {
     vector.set(64);
     vector.set(65);
 
+    EXPECT_EQ(3ul, vector.getAsInt(0, 64));
     EXPECT_EQ(1ul, vector.getAsInt(62, 1));
     EXPECT_EQ(3ul, vector.getAsInt(62, 2));
     EXPECT_EQ(7ul, vector.getAsInt(62, 3));
@@ -355,6 +356,48 @@ TEST(BitVectorTest, Complement) {
 	}
 }
 
+TEST(BitVectorTest, Increment) {
+	storm::storage::BitVector vector1(130, false);
+	storm::storage::BitVector vector2(130, false);
+    
+    vector1.increment();
+    EXPECT_EQ(1ull, vector1.getNumberOfSetBits());
+    vector2.set(0, true);
+    EXPECT_EQ(vector1, vector2);
+    
+    vector1.increment();
+    EXPECT_EQ(1ull, vector1.getNumberOfSetBits());
+    vector2.clear();
+    vector2.set(1, true);
+    EXPECT_EQ(vector1, vector2);
+    
+    vector1.increment();
+    EXPECT_EQ(2ull, vector1.getNumberOfSetBits());
+    vector2.set(0, true);
+    EXPECT_EQ(vector1, vector2);
+    
+    vector1.clear();
+	for (uint_fast64_t i = 0; i < 66; ++i) {
+        vector1.set(i, true);
+	}
+    vector1.increment();
+    EXPECT_EQ(1ull, vector1.getNumberOfSetBits());
+    vector2.clear();
+    vector2.set(66, true);
+    EXPECT_EQ(vector1, vector2);
+    
+    vector1.increment();
+    EXPECT_EQ(2ull, vector1.getNumberOfSetBits());
+    vector2.set(0, true);
+    EXPECT_EQ(vector1, vector2);
+    
+    vector1.clear();
+    vector1.complement();
+    EXPECT_TRUE(vector1.full());
+    vector1.increment();
+    EXPECT_TRUE(vector1.empty());
+}
+
 TEST(BitVectorTest, Implies) {
     storm::storage::BitVector vector1(32);
 	storm::storage::BitVector vector2(32, true);