Wrote tests for the new necessary bit vector operations (they fail, because the bit vector is organized in a weird way and needs to be restructured.)

Former-commit-id: b80e4b6efa

src/storage/BitVector.cpp

@@ -152,9 +152,9 @@ namespace storm {
         
         void BitVector::set(uint_fast64_t index, bool value) {
             if (index >= bitCount) throw storm::exceptions::OutOfRangeException() << "Invalid call to BitVector::set: written index " << index << " out of bounds.";
-            uint_fast64_t bucket = index >> 6;
+            uint64_t bucket = index >> 6;
             
-            uint_fast64_t mask = static_cast<uint_fast64_t>(1) << (index & mod64mask);
+            uint64_t mask = 1ull << (index & mod64mask);
             if (value) {
                 bucketVector[bucket] |= mask;
             } else {
@@ -412,11 +412,11 @@ namespace storm {
             uint64_t bucket = bitIndex >> 6;
             uint64_t bitIndexInBucket = bitIndex & mod64mask;
             
-            uint64_t mask = (1ull << (64 - bitIndexInBucket + 1)) - 1;
+            uint64_t mask = (1ull << (64 - bitIndexInBucket)) - 1;
             
             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 + 1))) - 1);
+                mask &= ~((1ull << (64 - (bitIndexInBucket - numberOfBits + 2))) - 1);
                 return bucketVector[bucket] & mask;
             } else if (bitIndexInBucket + numberOfBits > 64) {
                 // In this case, the integer "crosses" the bucket line.

src/storage/BitVectorHashMap.cpp

@@ -55,7 +55,12 @@ namespace storm {
         }
         
         template<class ValueType, class Hash1, class Hash2>
-        std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAdd(storm::storage::BitVector const& key, ValueType value) {
+        ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAdd(storm::storage::BitVector const& key, ValueType value) {
+            return findOrAddAndGetBucket(key, value).first;
+        }
+        
+        template<class ValueType, class Hash1, class Hash2>
+        std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType value) {
             // If the load of the map is too high, we increase the size.
             if (numberOfElements >= loadFactor * *currentSizeIterator) {
                 this->increaseSize();
@@ -70,7 +75,7 @@ namespace storm {
                 }
                 bucket += hasher2(key);
                 bucket %= *currentSizeIterator;
-
+                
                 // If we arrived at the original position, this means that we have visited all possible locations, but
                 // could not find a suitable position. This implies that we have to enlarge the map in order to resolve
                 // the issue.

src/storage/BitVectorHashMap.h

@@ -35,7 +35,19 @@ namespace storm {
              * @param value The value that is inserted if the key is not already found in the map.
              * @return The found value if the key is already contained in the map and the provided new value otherwise.
              */
-            std::pair<ValueType, std::size_t> findOrAdd(storm::storage::BitVector const& key, ValueType value);
+            ValueType findOrAdd(storm::storage::BitVector const& key, ValueType value);
+
+            /*!
+             * Searches for the given key in the map. If it is found, the mapped-to value is returned. Otherwise, the
+             * key is inserted with the given value.
+             *
+             * @param key The key to search or insert.
+             * @param value The value that is inserted if the key is not already found in the map.
+             * @return A pair whose first component is the found value if the key is already contained in the map and
+             * the provided new value otherwise and whose second component is the index of the bucket into which the key
+             * was inserted.
+             */
+            std::pair<ValueType, std::size_t> findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType value);
             
             /*!
              * Retrieves the key stored in the given bucket (if any).

src/storage/prism/Update.cpp

@@ -5,7 +5,7 @@
 namespace storm {
     namespace prism {
         Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), variableToAssignmentIndexMap(), globalIndex(globalIndex) {
-            std::sort(assignments.begin(), assignments.end(), [] (storm::prism::Assignment const& assignment1, storm::prism::Assignment const& assignment2) { return assignment1.getVariable() < assignment2.getVariable(); } );
+            std::sort(this->assignments.begin(), this->assignments.end(), [] (storm::prism::Assignment const& assignment1, storm::prism::Assignment const& assignment2) { return assignment1.getVariable() < assignment2.getVariable(); } );
             this->createAssignmentMapping();
         }
         

test/functional/storage/BitVectorTest.cpp

@@ -51,6 +51,27 @@ TEST(BitVectorTest, GetSet) {
 	}
 }
 
+TEST(BitVectorTest, GetAsInt) {
+    storm::storage::BitVector vector(77);
+    
+    vector.set(62);
+    vector.set(63);
+    vector.set(64);
+    vector.set(65);
+
+    EXPECT_EQ(1, vector.getAsInt(62, 1));
+    EXPECT_EQ(3, vector.getAsInt(62, 2));
+    EXPECT_EQ(7, vector.getAsInt(62, 3));
+    EXPECT_EQ(15, vector.getAsInt(62, 4));
+    
+    vector.set(64, false);
+
+    EXPECT_EQ(1, vector.getAsInt(62, 1));
+    EXPECT_EQ(3, vector.getAsInt(62, 2));
+    EXPECT_EQ(5, vector.getAsInt(62, 3));
+    EXPECT_EQ(13, vector.getAsInt(62, 4));
+}
+
 TEST(BitVectorTest, GetSetException) {
 	storm::storage::BitVector vector(32);