From 7abc84449b65f326ab0884b0b8fde502dc98a24f Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 22 Dec 2020 16:07:02 +0100 Subject: [PATCH] added opt dir override bitvector to multiplier This is mainly used by the SMG model checker to override row group optimization directions. --- .../solver/MultiplierEnvironment.cpp | 20 +++++--- .../solver/MultiplierEnvironment.h | 18 +++++-- src/storm/solver/Multiplier.cpp | 34 ++++++++----- src/storm/solver/Multiplier.h | 51 ++++++++++++------- 4 files changed, 82 insertions(+), 41 deletions(-) diff --git a/src/storm/environment/solver/MultiplierEnvironment.cpp b/src/storm/environment/solver/MultiplierEnvironment.cpp index 85e3bac77..0dd7f031a 100644 --- a/src/storm/environment/solver/MultiplierEnvironment.cpp +++ b/src/storm/environment/solver/MultiplierEnvironment.cpp @@ -6,28 +6,36 @@ #include "storm/utility/macros.h" namespace storm { - + MultiplierEnvironment::MultiplierEnvironment() { auto const& multiplierSettings = storm::settings::getModule(); type = multiplierSettings.getMultiplierType(); typeSetFromDefault = multiplierSettings.isMultiplierTypeSetFromDefaultValue(); } - + MultiplierEnvironment::~MultiplierEnvironment() { // Intentionally left empty } - + storm::solver::MultiplierType const& MultiplierEnvironment::getType() const { return type; } - + bool const& MultiplierEnvironment::isTypeSetFromDefault() const { return typeSetFromDefault; } - + void MultiplierEnvironment::setType(storm::solver::MultiplierType value, bool isSetFromDefault) { type = value; typeSetFromDefault = isSetFromDefault; } - + + void MultiplierEnvironment::setOptimizationDirectionOverride(storm::storage::BitVector optDirOverride) { + optimizationDirectionOverride = optDirOverride; + } + + boost::optional const& MultiplierEnvironment::getOptimizationDirectionOverride() const { + return optimizationDirectionOverride; + } + } diff --git a/src/storm/environment/solver/MultiplierEnvironment.h b/src/storm/environment/solver/MultiplierEnvironment.h index d9e35f5fb..945b62602 100644 --- a/src/storm/environment/solver/MultiplierEnvironment.h +++ b/src/storm/environment/solver/MultiplierEnvironment.h @@ -1,23 +1,31 @@ #pragma once +#include + #include "storm/environment/solver/SolverEnvironment.h" #include "storm/solver/SolverSelectionOptions.h" +#include "storm/storage/BitVector.h" + namespace storm { - + class MultiplierEnvironment { public: - + MultiplierEnvironment(); ~MultiplierEnvironment(); - + storm::solver::MultiplierType const& getType() const; bool const& isTypeSetFromDefault() const; void setType(storm::solver::MultiplierType value, bool isSetFromDefault = false); - + + void setOptimizationDirectionOverride(storm::storage::BitVector optimizationDirectionOverride); + boost::optional const& getOptimizationDirectionOverride() const; + private: storm::solver::MultiplierType type; bool typeSetFromDefault; + + boost::optional optimizationDirectionOverride = boost::none; }; } - diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 4049b56ca..87e74b16a 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -18,17 +18,17 @@ namespace storm { namespace solver { - + template Multiplier::Multiplier(storm::storage::SparseMatrix const& matrix) : matrix(matrix) { // Intentionally left empty. } - + template void Multiplier::clearCache() const { cachedVector.reset(); } - + template void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices); @@ -38,7 +38,7 @@ namespace storm { void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices, bool backwards) const { multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, backwards); } - + template void Multiplier::repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, uint64_t n) const { storm::utility::ProgressMeasurement progress("multiplications"); @@ -53,7 +53,7 @@ namespace storm { } } } - + template void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n) const { storm::utility::ProgressMeasurement progress("multiplications"); @@ -67,17 +67,27 @@ namespace storm { } } } - + template void Multiplier::multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const { multiplyRow(rowIndex, x1, val1); multiplyRow(rowIndex, x2, val2); } - + + template + void Multiplier::setOptimizationDirectionOverride(storm::storage::BitVector const& optDirOverride) { + optimizationDirectionOverride = optDirOverride; + } + + template + boost::optional Multiplier::getOptimizationDirectionOverride() const { + return optimizationDirectionOverride; + } + template std::unique_ptr> MultiplierFactory::create(Environment const& env, storm::storage::SparseMatrix const& matrix) { auto type = env.solver().multiplier().getType(); - + // Adjust the multiplier type if an eqsolver was specified but not a multiplier if (!env.solver().isLinearEquationSolverTypeSetFromDefaultValue() && env.solver().multiplier().isTypeSetFromDefault()) { bool changed = false; @@ -90,7 +100,7 @@ namespace storm { } STORM_LOG_INFO_COND(!changed, "Selecting '" + toString(type) + "' as the multiplier type to match the selected equation solver. If you want to override this, please explicitly specify a different multiplier type."); } - + switch (type) { case MultiplierType::Gmmxx: return std::make_unique>(matrix); @@ -99,16 +109,16 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType"); } - + 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 index 58aeb4e38..552a427dd 100644 --- a/src/storm/solver/Multiplier.h +++ b/src/storm/solver/Multiplier.h @@ -2,34 +2,37 @@ #include #include +#include + +#include "storm/storage/BitVector.h" #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); - + virtual ~Multiplier() = default; - + /* * 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. * @@ -41,7 +44,7 @@ namespace storm { * to the number of rows of A. Can be the same as the x vector. */ virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const = 0; - + /*! * Performs a matrix-vector multiplication in gauss-seidel style. * @@ -52,7 +55,7 @@ namespace storm { * @param backwards if true, the iterations will be performed beginning from the last row and ending at the first row. */ virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) 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. @@ -69,7 +72,7 @@ namespace storm { */ void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const = 0; - + /*! * Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups * so that the resulting vector has the size of number of row groups of A. @@ -87,7 +90,7 @@ namespace storm { */ void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) const; virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) 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 @@ -100,7 +103,7 @@ namespace storm { * @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. @@ -115,7 +118,7 @@ namespace storm { * @param n The number of times to perform the multiplication. */ void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n) const; - + /*! * Multiplies the row with the given index with x and adds the result to the provided value * @param rowIndex The index of the considered row @@ -123,7 +126,7 @@ namespace storm { * @param value The multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix. */ virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const = 0; - + /*! * Multiplies the row with the given index with x1 and x2 and adds the given offset o1 and o2, respectively * @param rowIndex The index of the considered row @@ -133,12 +136,24 @@ namespace storm { * @param val2 The second multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix. */ virtual void multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const; - + + /* + * TODO + */ + void setOptimizationDirectionOverride(storm::storage::BitVector const& optimizationDirectionOverride); + + /* + * TODO + */ + boost::optional getOptimizationDirectionOverride() const; + protected: mutable std::unique_ptr> cachedVector; storm::storage::SparseMatrix const& matrix; + + boost::optional optimizationDirectionOverride = boost::none; }; - + template class MultiplierFactory { public: @@ -147,6 +162,6 @@ namespace storm { std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& matrix); }; - + } }