From 50e1fe0c15cf40d4fa1525289e1b5a26348fc3f6 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 14 Aug 2017 12:00:11 +0200
Subject: [PATCH] increment() function for BitVector

---
 src/storm/storage/BitVector.cpp          | 27 +++++++++++++++
 src/storm/storage/BitVector.h            |  7 ++++
 src/test/storm/storage/BitVectorTest.cpp | 43 ++++++++++++++++++++++++
 3 files changed, 77 insertions(+)

diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp
index 35735a228..1b1c3734e 100644
--- a/src/storm/storage/BitVector.cpp
+++ b/src/storm/storage/BitVector.cpp
@@ -337,6 +337,33 @@ namespace storm {
             std::transform(this->buckets, this->buckets + this->bucketCount(), this->buckets, [] (uint64_t const& a) { return ~a; });
             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.");
diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h
index dccfa0830..d2df0c4ae 100644
--- a/src/storm/storage/BitVector.h
+++ b/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.
diff --git a/src/test/storm/storage/BitVectorTest.cpp b/src/test/storm/storage/BitVectorTest.cpp
index 0bb9847f6..b329c9bee 100644
--- a/src/test/storm/storage/BitVectorTest.cpp
+++ b/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);