#ifndef STORM_UTILITY_VECTOR_H_ #define STORM_UTILITY_VECTOR_H_ #include "storm-config.h" #ifdef STORM_HAVE_INTELTBB #include "tbb/tbb.h" #endif #include "constants.h" #include #include #include #include "src/storage/BitVector.h" #include "src/utility/macros.h" template std::ostream& operator<<(std::ostream& out, std::vector const& vector); namespace storm { namespace utility { namespace vector { /*! * Sets the provided values at the provided positions in the given vector. * * @param vector The vector in which the values are to be set. * @param positions The positions at which the values are to be set. * @param values The values that are to be set. */ template void setVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& values) { uint_fast64_t oldPosition = 0; for (auto position : positions) { vector[position] = values[oldPosition++]; } } /*! * Sets the provided value at the provided positions in the given vector. * * @param vector The vector in which the value is to be set. * @param positions The positions at which the value is to be set. * @param value The value that is to be set. */ template void setVectorValues(std::vector& vector, storm::storage::BitVector const& positions, T value) { for (auto position : positions) { vector[position] = value; } } /*! * Selects the elements from a vector at the specified positions and writes them consecutively into another vector. * @param vector The vector into which the selected elements are to be written. * @param positions The positions at which to select the elements from the values vector. * @param values The vector from which to select the elements. */ template void selectVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& values) { uint_fast64_t oldPosition = 0; for (auto position : positions) { vector[oldPosition++] = values[position]; } } /*! * Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector. * * @param vector The vector into which the selected elements are to be written. * @param positions The positions of the groups of elements that are to be selected. * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. * @param values The vector from which to select groups of elements. */ template void selectVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& rowGrouping, std::vector const& values) { uint_fast64_t oldPosition = 0; for (auto position : positions) { for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) { vector[oldPosition++] = values[i]; } } } /*! * Selects one element out of each row group and writes it to the target vector. * * @param vector The target vector to which the values are written. * @param rowGroupToRowIndexMapping A mapping from row group indices to an offset that specifies which of the values to * take from the row group. * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. * @param values The vector from which to select the values. */ template void selectVectorValues(std::vector& vector, std::vector const& rowGroupToRowIndexMapping, std::vector const& rowGrouping, std::vector const& values) { for (uint_fast64_t i = 0; i < vector.size(); ++i) { vector[i] = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]]; } } /*! * Selects values from a vector at the specified positions and writes them into another vector as often as given by * the size of the corresponding group of elements. * * @param vector The vector into which the selected elements are written. * @param positions The positions at which to select the values. * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. This * implicitly defines the number of times any element is written to the output vector. */ template void selectVectorValuesRepeatedly(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& rowGrouping, std::vector const& values) { uint_fast64_t oldPosition = 0; for (auto position : positions) { for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) { vector[oldPosition++] = values[position]; } } } /*! * Subtracts the given vector from the constant one-vector and writes the result to the input vector. * * @param vector The vector that is to be subtracted from the constant one-vector. */ template void subtractFromConstantOneVector(std::vector& vector) { for (auto& element : vector) { element = storm::utility::one() - element; } } /*! * Applies the given operation pointwise on the two given vectors and writes the result to the third vector. * To botain an in-place operation, the third vector may be equal to any of the other two vectors. * * @param firstOperand The first operand. * @param secondOperand The second operand. * @param target The target vector. */ template void applyPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target, std::function function) { #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, target.size()), [&](tbb::blocked_range const& range) { std::transform(firstOperand.begin() + range.begin(), firstOperand.begin() + range.end(), secondOperand.begin() + range.begin(), target.begin() + range.begin(), function); }); #else std::transform(firstOperand.begin(), firstOperand.end(), secondOperand.begin(), target.begin(), function); #endif } /*! * Applies the given function pointwise on the given vector. * * @param operand The vector to which to apply the function. * @param target The target vector. * @param function The function to apply. */ template void applyPointwise(std::vector const& operand, std::vector& target, std::function const& function) { #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, target.size()), [&](tbb::blocked_range const& range) { std::transform(operand.begin() + range.begin(), operand.begin() + range.end(), target.begin() + range.begin(), function); }); #else std::transform(operand.begin(), operand.end(), target.begin(), function); #endif } /*! * Adds the two given vectors and writes the result to the target vector. * * @param firstOperand The first operand. * @param secondOperand The second operand * @param target The target vector. */ template void addVectors(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target) { applyPointwise(firstOperand, secondOperand, target, std::plus()); } /*! * Subtracts the two given vectors and writes the result to the target vector. * * @param firstOperand The first operand. * @param secondOperand The second operand * @param target The target vector. */ template void subtractVectors(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target) { applyPointwise(firstOperand, secondOperand, target, std::minus()); } /*! * Multiplies the two given vectors (pointwise) and writes the result to the target vector. * * @param firstOperand The first operand. * @param secondOperand The second operand * @param target The target vector. */ template void multiplyVectorsPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target) { applyPointwise(firstOperand, secondOperand, target, std::multiplies()); } /*! * Subtracts the two given vectors and writes the result into the first operand. * * @param target The first summand and target vector. * @param summand The second summand. */ template void scaleVectorInPlace(std::vector& target, T const& factor) { applyPointwise(target, target, [&] (T const& argument) { return argument * factor; }); } /*! * Retrieves a bit vector containing all the indices for which the value at this position makes the given * function evaluate to true. * * @param values The vector of values. * @param function The function that selects some elements. * @return The resulting bit vector. */ template storm::storage::BitVector filter(std::vector const& values, std::function const& function) { storm::storage::BitVector result(values.size()); uint_fast64_t currentIndex = 0; for (auto const& value : values) { result.set(currentIndex, function(value)); ++currentIndex; } return result; } /*! * Retrieves a bit vector containing all the indices for which the value at this position is greater than * zero * * @param values The vector of values. * @return The resulting bit vector. */ template storm::storage::BitVector filterGreaterZero(std::vector const& values) { std::function fnc = [] (T const& value) -> bool { return value > storm::utility::zero(); }; return filter(values, fnc); } /** * Sum the entries from values that are set to one in the filter vector. * @param values * @param filter * @return The sum of the values with a corresponding one in the filter. */ template VT sum_if(std::vector const& values, storm::storage::BitVector const& filter) { assert(values.size() >= filter.size()); VT sum = storm::utility::zero(); for(uint_fast64_t i : filter) { sum += values[i]; } return sum; } /*! * Reduces the given source vector by selecting an element according to the given filter out of each row group. * * @param source The source vector which is to be reduced. * @param target The target vector into which a single element from each row group is written. * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. * @param filter A function that compares two elements v1 and v2 according to some filter criterion. This function must * return true iff v1 is supposed to be taken instead of v2. * @param choices If non-null, this vector is used to store the choices made during the selection. */ template void reduceVector(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::function filter, std::vector* choices) { #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, target.size()), [&](tbb::blocked_range const& range) { uint_fast64_t startRow = range.begin(); uint_fast64_t endRow = range.end(); typename std::vector::iterator targetIt = target.begin() + startRow; typename std::vector::iterator targetIte = target.begin() + endRow; typename std::vector::const_iterator rowGroupingIt = rowGrouping.begin() + startRow; typename std::vector::const_iterator sourceIt = source.begin() + *rowGroupingIt; typename std::vector::const_iterator sourceIte; typename std::vector::iterator choiceIt; uint_fast64_t localChoice; if (choices != nullptr) { choiceIt = choices->begin(); } for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt) { *targetIt = *sourceIt; ++sourceIt; localChoice = 1; if (choices != nullptr) { *choiceIt = 0; } for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) { if (filter(*sourceIt, *targetIt)) { *targetIt = *sourceIt; if (choices != nullptr) { *choiceIt = localChoice; } } } if (choices != nullptr) { ++choiceIt; } } }); #else typename std::vector::iterator targetIt = target.begin(); typename std::vector::iterator targetIte = target.end(); typename std::vector::const_iterator rowGroupingIt = rowGrouping.begin(); typename std::vector::const_iterator sourceIt = source.begin(); typename std::vector::const_iterator sourceIte; typename std::vector::iterator choiceIt; uint_fast64_t localChoice; if (choices != nullptr) { choiceIt = choices->begin(); } for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt) { *targetIt = *sourceIt; ++sourceIt; localChoice = 1; if (choices != nullptr) { *choiceIt = 0; } for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) { if (filter(*sourceIt, *targetIt)) { *targetIt = *sourceIt; if (choices != nullptr) { *choiceIt = localChoice; } } } if (choices != nullptr) { ++choiceIt; } } #endif } /*! * Reduces the given source vector by selecting the smallest element out of each row group. * * @param source The source vector which is to be reduced. * @param target The target vector into which a single element from each row group is written. * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. * @param choices If non-null, this vector is used to store the choices made during the selection. */ template void reduceVectorMin(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { reduceVector(source, target, rowGrouping, std::less(), choices); } /*! * Reduces the given source vector by selecting the largest element out of each row group. * * @param source The source vector which is to be reduced. * @param target The target vector into which a single element from each row group is written. * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. * @param choices If non-null, this vector is used to store the choices made during the selection. */ template void reduceVectorMax(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { reduceVector(source, target, rowGrouping, std::greater(), choices); } /*! * Reduces the given source vector by selecting either the smallest or the largest out of each row group. * * @param minimize If true, select the smallest, else select the largest. * @param source The source vector which is to be reduced. * @param target The target vector into which a single element from each row group is written. * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. * @param choices If non-null, this vector is used to store the choices made during the selection. */ template void reduceVectorMinOrMax(bool minimize, std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { if(minimize) { reduceVectorMin(source, target, rowGrouping, choices); } else { reduceVectorMax(source, target, rowGrouping, choices); } } /*! * Compares the given elements and determines whether they are equal modulo the given precision. The provided flag * additionaly specifies whether the error is computed in relative or absolute terms. * * @param val1 The first value to compare. * @param val2 The second value to compare. * @param precision The precision up to which the elements are compared. * @param relativeError If set, the error is computed relative to the second value. * @return True iff the elements are considered equal. */ template bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) { if (relativeError) { if (val2 == 0) { return (std::abs(val1) <= precision); } if (std::abs((val1 - val2)/val2) > precision) { return false; } } else { if (std::abs(val1 - val2) > precision) return false; } return true; } /*! * Compares the two vectors and determines whether they are equal modulo the provided precision. Depending on whether the * flag is set, the difference between the vectors is computed relative to the value or in absolute terms. * * @param vectorLeft The first vector of the comparison. * @param vectorRight The second vector of the comparison. * @param precision The precision up to which the vectors are to be checked for equality. * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. */ template bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T precision, bool relativeError) { STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) { if (!equalModuloPrecision(vectorLeft[i], vectorRight[i], precision, relativeError)) { return false; } } return true; } /*! * Compares the two vectors at the specified positions and determines whether they are equal modulo the provided * precision. Depending on whether the flag is set, the difference between the vectors is computed relative to the value * or in absolute terms. * * @param vectorLeft The first vector of the comparison. * @param vectorRight The second vector of the comparison. * @param precision The precision up to which the vectors are to be checked for equality. * @param positions A vector representing a set of positions at which the vectors are compared. * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. */ template bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& positions, T precision, bool relativeError) { STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); for (uint_fast64_t position : positions) { if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) { return false; } } return true; } /*! * Takes the given offset vector and applies the given contraint. That is, it produces another offset vector that contains * the relative offsets of the entries given by the constraint. * * @param offsetVector The offset vector to constrain. * @param constraint The constraint to apply to the offset vector. * @return An offset vector that contains all selected relative offsets. */ template std::vector getConstrainedOffsetVector(std::vector const& offsetVector, storm::storage::BitVector const& constraint) { // Reserve the known amount of slots for the resulting vector. std::vector subVector(constraint.getNumberOfSetBits() + 1); uint_fast64_t currentRowCount = 0; uint_fast64_t currentIndexCount = 1; // Set the first element as this will clearly begin at offset 0. subVector[0] = 0; // Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over // to the resulting vector. for (auto index : constraint) { subVector[currentIndexCount] = currentRowCount + offsetVector[index + 1] - offsetVector[index]; currentRowCount += offsetVector[index + 1] - offsetVector[index]; ++currentIndexCount; } // Put a sentinel element at the end. subVector[constraint.getNumberOfSetBits()] = currentRowCount; return subVector; } /*! * Converts the given vector to the given ValueType */ template std::vector toValueType(std::vector const& oldVector) { std::vector resultVector; resultVector.resize(oldVector.size()); for (size_t i = 0, size = oldVector.size(); i < size; ++i) { resultVector.at(i) = static_cast(oldVector.at(i)); } return resultVector; } } // namespace vector } // namespace utility } // namespace storm #endif /* STORM_UTILITY_VECTOR_H_ */