diff --git a/src/utility/Vector.h b/src/utility/Vector.h index 87ed40b29..fce8c18e1 100644 --- a/src/utility/Vector.h +++ b/src/utility/Vector.h @@ -54,12 +54,20 @@ void selectVectorValues(std::vector* vector, const storm::storage::BitVector& template void selectVectorValues(std::vector* vector, const storm::storage::BitVector& positions, const std::vector& rowMapping, std::vector const& values) { uint_fast64_t oldPosition = 0; - uint_fast64_t rowMappingPosition = 0; for (auto position : positions) { - for (uint_fast64_t i = rowMapping[rowMappingPosition]; i < rowMapping[rowMappingPosition + 1]; ++i) { + for (uint_fast64_t i = rowMapping[position]; i < rowMapping[position + 1]; ++i) { + (*vector)[oldPosition++] = values[i]; + } + } +} + +template +void selectVectorValuesRepeatedly(std::vector* vector, const storm::storage::BitVector& positions, const std::vector& rowMapping, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + for (uint_fast64_t i = rowMapping[position]; i < rowMapping[position + 1]; ++i) { (*vector)[oldPosition++] = values[position]; } - ++rowMappingPosition; } }