diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp new file mode 100644 index 000000000..0375449bf --- /dev/null +++ b/src/storm/solver/Multiplier.cpp @@ -0,0 +1,75 @@ +#include "storm/solver/Multiplier.h" + +#include "storm-config.h" + +#include "storm/storage/SparseMatrix.h" + +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" + +#include "storm/utility/macros.h" +#include "storm/solver/SolverSelectionOptions.h" +#include "storm/solver/NativeMultiplier.h" +#include "storm/environment/solver/MultiplierEnvironment.h" + +namespace storm { + namespace solver { + + template + Multiplier::Multiplier(storm::storage::SparseMatrix const& matrix) : matrix(matrix), allowGaussSeidelMultiplications(false) { + // Intentionally left empty. + } + + template + bool Multiplier::getAllowGaussSeidelMultiplications() const { + return allowGaussSeidelMultiplications; + } + + template + void Multiplier::setAllowGaussSeidelMultiplications(bool value) { + allowGaussSeidelMultiplications = value; + } + + template + void Multiplier::clearCache() const { + cachedVector.reset(); + } + + template + void Multiplier::repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, uint64_t n) const { + for (uint64_t i = 0; i < n; ++i) { + multiply(env, x, b, x); + } + } + + template + void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, uint64_t n) const { + for (uint64_t i = 0; i < n; ++i) { + multiplyAndReduce(env, dir, rowGroupIndices, x, b, x); + } + } + + template + std::unique_ptr> MultiplierFactory::create(Environment const& env, storm::storage::SparseMatrix const& matrix) { + switch (env.solver().multiplier().getType()) { + case MultiplierType::Gmmxx: + //return std::make_unique>(matrix); + STORM_PRINT_AND_LOG("gmm mult not yet supported"); + case MultiplierType::Native: + return std::make_unique>(matrix); + } + } + + + template class Multiplier; + template class MultiplierFactory; + +#ifdef STORM_HAVE_CARL + template class Multiplier; + template class MultiplierFactory; + template class Multiplier; + template class MultiplierFactory; +#endif + + } +} diff --git a/src/storm/solver/Multiplier.h b/src/storm/solver/Multiplier.h new file mode 100644 index 000000000..432bce2ed --- /dev/null +++ b/src/storm/solver/Multiplier.h @@ -0,0 +1,126 @@ +#pragma once + +#include "storm/solver/OptimizationDirection.h" +#include "storm/solver/MultiplicationStyle.h" + +namespace storm { + + class Environment; + + namespace storage { + template + class SparseMatrix; + } + + namespace solver { + + template + class Multiplier { + public: + + Multiplier(storm::storage::SparseMatrix const& matrix); + + /*! + * Retrieves whether Gauss Seidel style multiplications are allowed. + */ + bool getAllowGaussSeidelMultiplications() const; + + /*! + * Sets whether Gauss Seidel style multiplications are allowed. + */ + void setAllowGaussSeidelMultiplications(bool value); + + /*! + * Returns the multiplication style performed by this multiplier + */ + virtual MultiplicationStyle getMultiplicationStyle() const = 0; + + /* + * Clears the currently cached data of this multiplier in order to free some memory. + */ + virtual void clearCache() const; + + /*! + * Performs a matrix-vector multiplication x' = A*x + b. + * + * @param x The input vector with which to multiply the matrix. Its length must be equal + * to the number of columns of A. + * @param b If non-null, this vector is added after the multiplication. If given, its length must be equal + * to the number of rows of A. + * @param result The target vector into which to write the multiplication result. Its length must be equal + * to the number of rows of A. Can be the same as the x vector. + */ + virtual void multiply(Environment const& env, std::vector& x, std::vector const* b, std::vector& result) const = 0; + + /*! + * Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups + * so that the resulting vector has the size of number of row groups of A. + * + * @param dir The direction for the reduction step. + * @param rowGroupIndices A vector storing the row groups over which to reduce. + * @param x The input vector with which to multiply the matrix. Its length must be equal + * to the number of columns of A. + * @param b If non-null, this vector is added after the multiplication. If given, its length must be equal + * to the number of rows of A. + * @param result The target vector into which to write the multiplication result. Its length must be equal + * to the number of rows of A. Can be the same as the x vector. + * @param choices If given, the choices made in the reduction process are written to this vector. + */ + virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const = 0; + + /*! + * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After + * performing the necessary multiplications, the result is written to the input vector x. Note that the + * matrix A has to be given upon construction time of the solver object. + * + * @param x The initial vector with which to perform matrix-vector multiplication. Its length must be equal + * to the number of columns of A. + * @param b If non-null, this vector is added after each multiplication. If given, its length must be equal + * to the number of rows of A. + * @param n The number of times to perform the multiplication. + */ + void repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, uint64_t n) const; + + /*! + * Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups + * so that the resulting vector has the size of number of row groups of A. + * + * @param dir The direction for the reduction step. + * @param rowGroupIndices A vector storing the row groups over which to reduce. + * @param x The input vector with which to multiply the matrix. Its length must be equal + * to the number of columns of A. + * @param b If non-null, this vector is added after the multiplication. If given, its length must be equal + * to the number of rows of A. + * @param result The target vector into which to write the multiplication result. Its length must be equal + * to the number of rows of A. + * @param n The number of times to perform the multiplication. + */ + void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, uint64_t n) const; + + /*! + * Multiplies the row with the given index with x and adds the given offset + * @param rowIndex The index of the considered row + * @param x The input vector with which the row is multiplied + */ + virtual ValueType multiplyRow(Environment const& env, uint64_t const& rowIndex, std::vector const& x, ValueType const& offset) const = 0; + + protected: + mutable std::unique_ptr> cachedVector; + storm::storage::SparseMatrix const& matrix; + private: + bool allowGaussSeidelMultiplications; + }; + + template + class MultiplierFactory { + public: + MultiplierFactory() = default; + ~MultiplierFactory() = default; + + std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& matrix); + + + }; + + } +} diff --git a/src/storm/solver/NativeMultiplier.cpp b/src/storm/solver/NativeMultiplier.cpp index ddbeb235f..c4155fcbf 100644 --- a/src/storm/solver/NativeMultiplier.cpp +++ b/src/storm/solver/NativeMultiplier.cpp @@ -2,6 +2,10 @@ #include "storm-config.h" +#include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/CoreSettings.h" + #include "storm/storage/SparseMatrix.h" #include "storm/adapters/RationalNumberAdapter.h" @@ -13,89 +17,132 @@ namespace storm { namespace solver { template - NativeMultiplier::NativeMultiplier() : storm::utility::VectorHelper() { + NativeMultiplier::NativeMultiplier(storm::storage::SparseMatrix const& matrix) : Multiplier(matrix) { // Intentionally left empty. } - + template - void NativeMultiplier::multAdd(storm::storage::SparseMatrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result) const { - std::vector* target = &result; - std::unique_ptr> temporary; - if (&x == &result) { - STORM_LOG_WARN("Using temporary in 'multAdd'."); - temporary = std::make_unique>(x.size()); - target = temporary.get(); - } - - if (this->parallelize()) { - multAddParallel(matrix, x, b, result); + bool NativeMultiplier::parallelize(Environment const& env) const { +#ifdef STORM_HAVE_INTELTBB + return storm::settings::getModule().isUseIntelTbbSet(); +#else + return false; +#endif + } + + template + MultiplicationStyle NativeMultiplier::getMultiplicationStyle() const { + if (this->getAllowGaussSeidelMultiplications()) { + return MultiplicationStyle::GaussSeidel; } else { - matrix.multiplyWithVector(x, result, b); - } - - if (target == temporary.get()) { - std::swap(result, *temporary); + return MultiplicationStyle::Regular; } } template - void NativeMultiplier::multAddGaussSeidelBackward(storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const* b) const { - matrix.multiplyWithVectorBackward(x, x, b); + void NativeMultiplier::multiply(Environment const& env, std::vector& x, std::vector const* b, std::vector& result) const { + if (getMultiplicationStyle() == MultiplicationStyle::GaussSeidel) { + multAddGaussSeidelBackward(x, b); + if (&x != &result) { + result = x; + } + } else { + STORM_LOG_ASSERT(getMultiplicationStyle() == MultiplicationStyle::Regular, "Unexpected Multiplicationstyle."); + std::vector* target = &result; + if (&x == &result) { + if (this->cachedVector) { + this->cachedVector->resize(x.size()); + } else { + this->cachedVector = std::make_unique>(x.size()); + } + target = this->cachedVector.get(); + } + if (parallelize(env)) { + multAddParallel(x, b, *target); + } else { + multAdd(x, b, *target); + } + if (&x == &result) { + std::swap(result, *this->cachedVector); + } + } } template - void NativeMultiplier::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, storm::storage::SparseMatrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { - std::vector* target = &result; - std::unique_ptr> temporary; - if (&x == &result) { - STORM_LOG_WARN("Using temporary in 'multAddReduce'."); - temporary = std::make_unique>(x.size()); - target = temporary.get(); - } - - if (this->parallelize()) { - multAddReduceParallel(dir, rowGroupIndices, matrix, x, b, *target, choices); + void NativeMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector& result, std::vector* choices) const { + if (getMultiplicationStyle() == MultiplicationStyle::GaussSeidel) { + multAddReduceGaussSeidelBackward(dir, rowGroupIndices, x, b, choices); + if (&x != &result) { + result = x; + } } else { - matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, *target, choices); - } - - if (target == temporary.get()) { - std::swap(result, *temporary); + STORM_LOG_ASSERT(getMultiplicationStyle() == MultiplicationStyle::Regular, "Unexpected Multiplicationstyle."); + std::vector* target = &result; + if (&x == &result) { + if (this->cachedVector) { + this->cachedVector->resize(x.size()); + } else { + this->cachedVector = std::make_unique>(x.size()); + } + target = this->cachedVector.get(); + } + if (parallelize(env)) { + multAddReduceParallel(dir, rowGroupIndices, x, b, *target, choices); + } else { + multAddReduce(dir, rowGroupIndices, x, b, *target, choices); + } + if (&x == &result) { + std::swap(result, *this->cachedVector); + } } } template - void NativeMultiplier::multAddReduceGaussSeidelBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const* b, std::vector* choices) const { - matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices); + ValueType NativeMultiplier::multiplyRow(Environment const& env, uint64_t const& rowIndex, std::vector const& x, ValueType const& offset) const { + return this->matrix.multiplyRowWithVector(rowIndex, x); + } + + template + void NativeMultiplier::multAdd(std::vector const& x, std::vector const* b, std::vector& result) const { + this->matrix.multiplyWithVector(x, result, b); + } + + template + void NativeMultiplier::multAddGaussSeidelBackward(std::vector& x, std::vector const* b) const { + this->matrix.multiplyWithVectorBackward(x, x, b); + } + + template + void NativeMultiplier::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices); + } + + template + void NativeMultiplier::multAddReduceGaussSeidelBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices) const { + this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices); } template - void NativeMultiplier::multAddParallel(storm::storage::SparseMatrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result) const { + void NativeMultiplier::multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const { #ifdef STORM_HAVE_INTELTBB matrix.multiplyWithVectorParallel(x, result, b); #else STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version."); - multAdd(matrix, x, b, result); + multAdd(x, b, result); #endif } template - void NativeMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, storm::storage::SparseMatrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + void NativeMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { #ifdef STORM_HAVE_INTELTBB matrix.multiplyAndReduceParallel(dir, rowGroupIndices, x, b, result, choices); #else STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version."); - multAddReduce(dir, rowGroupIndices, matrix, x, b, result, choices); + multAddReduce(dir, rowGroupIndices, x, b, result, choices); #endif } - template - ValueType NativeMultiplier::multiplyRow(storm::storage::SparseMatrix const& matrix, uint64_t const& rowIndex, std::vector const& x) const { - return matrix.multiplyRowWithVector(rowIndex, x); - } - template class NativeMultiplier; - #ifdef STORM_HAVE_CARL template class NativeMultiplier; template class NativeMultiplier; diff --git a/src/storm/solver/NativeMultiplier.h b/src/storm/solver/NativeMultiplier.h index ea8f543d4..b82598b0d 100644 --- a/src/storm/solver/NativeMultiplier.h +++ b/src/storm/solver/NativeMultiplier.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/utility/VectorHelper.h" +#include "storm/solver/Multiplier.h" #include "storm/solver/OptimizationDirection.h" @@ -13,20 +13,28 @@ namespace storm { namespace solver { template - class NativeMultiplier : public storm::utility::VectorHelper { + class NativeMultiplier : public Multiplier { public: - NativeMultiplier(); + NativeMultiplier(storm::storage::SparseMatrix const& matrix); - void multAdd(storm::storage::SparseMatrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddGaussSeidelBackward(storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const* b) const; + virtual MultiplicationStyle getMultiplicationStyle() const override; + + virtual void multiply(Environment const& env, std::vector& x, std::vector const* b, std::vector& result) const override; + virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const override; + virtual ValueType multiplyRow(Environment const& env, uint64_t const& rowIndex, std::vector const& x, ValueType const& offset) const override; + + private: + bool parallelize(Environment const& env) const; + + void multAdd(std::vector const& x, std::vector const* b, std::vector& result) const; + void multAddGaussSeidelBackward(std::vector& x, std::vector const* b) const; - void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, storm::storage::SparseMatrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; - void multAddReduceGaussSeidelBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const* b, std::vector* choices = nullptr) const; + void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; + void multAddReduceGaussSeidelBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr) const; - void multAddParallel(storm::storage::SparseMatrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, storm::storage::SparseMatrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; + void multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const; + void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; - ValueType multiplyRow(storm::storage::SparseMatrix const& matrix, uint64_t const& rowIndex, std::vector const& x) const; }; }