diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index d66af49b0..b0a7f9556 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -433,6 +433,16 @@ namespace storm { return true; } + BitVector BitVector::permute(std::vector const& inversePermutation) const { + BitVector result(this->size()); + for (uint64_t i = 0; i < this->size(); ++i) { + if(this->get(inversePermutation[i])) { + result.set(i, true); + } + } + return result; + } + void BitVector::set(uint_fast64_t bitIndex, BitVector const& other) { STORM_LOG_ASSERT((bitIndex & mod64mask) == 0, "Bit index must be a multiple of 64."); STORM_LOG_ASSERT(other.size() <= this->size() - bitIndex, "Bit vector argument is too long."); diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index 6fd4a79aa..9561895a8 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -372,6 +372,14 @@ namespace storm { * @param other The bit vector whose pattern to set. */ void set(uint_fast64_t bitIndex, BitVector const& other); + + /*! + * Apply a permutation of entries. That is, in row i, write the entry of row inversePermutation[i]. + * @param inversePermutation. + * @return + * TODO this operation is slow. + */ + BitVector permute(std::vector const& inversePermutation) const; /*! * Retrieves the content of the current bit vector at the given index for the given number of bits as a new diff --git a/src/test/storm/storage/BitVectorTest.cpp b/src/test/storm/storage/BitVectorTest.cpp index 3bfcacf7a..d3b65e04c 100644 --- a/src/test/storm/storage/BitVectorTest.cpp +++ b/src/test/storm/storage/BitVectorTest.cpp @@ -398,6 +398,15 @@ TEST(BitVectorTest, Increment) { EXPECT_TRUE(vector1.empty()); } +TEST(BitVectorTest, permute) { + storm::storage::BitVector vector1(9, {3, 5}); + std::vector inversePermutation = {0, 1, 3, 2, 4, 6, 5, 8, 7}; + storm::storage::BitVector vector2 = vector1.permute(inversePermutation); + EXPECT_EQ(vector1.getNumberOfSetBits(), vector2.getNumberOfSetBits()); + EXPECT_TRUE(vector2.get(2)); + EXPECT_TRUE(vector2.get(6)); +} + TEST(BitVectorTest, Implies) { storm::storage::BitVector vector1(32); storm::storage::BitVector vector2(32, true);