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<storm::settings::modules::MultiplierSettings>();
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<storm::storage::BitVector> 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 <boost/optional.hpp>
+
#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<storm::storage::BitVector> const& getOptimizationDirectionOverride() const;
+
private:
storm::solver::MultiplierType type;
bool typeSetFromDefault;
+
+ boost::optional<storm::storage::BitVector> 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<typename ValueType>
Multiplier<ValueType>::Multiplier(storm::storage::SparseMatrix<ValueType> const& matrix) : matrix(matrix) {
// Intentionally left empty.
}
-
+
template<typename ValueType>
void Multiplier<ValueType>::clearCache() const {
cachedVector.reset();
}
-
+
template<typename ValueType>
void Multiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices);
@@ -38,7 +38,7 @@ namespace storm {
void Multiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, backwards);
}
-
+
template<typename ValueType>
void Multiplier<ValueType>::repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
storm::utility::ProgressMeasurement progress("multiplications");
@@ -53,7 +53,7 @@ namespace storm {
}
}
}
-
+
template<typename ValueType>
void Multiplier<ValueType>::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
storm::utility::ProgressMeasurement progress("multiplications");
@@ -67,17 +67,27 @@ namespace storm {
}
}
}
-
+
template<typename ValueType>
void Multiplier<ValueType>::multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const {
multiplyRow(rowIndex, x1, val1);
multiplyRow(rowIndex, x2, val2);
}
-
+
+ template<typename ValueType>
+ void Multiplier<ValueType>::setOptimizationDirectionOverride(storm::storage::BitVector const& optDirOverride) {
+ optimizationDirectionOverride = optDirOverride;
+ }
+
+ template<typename ValueType>
+ boost::optional<storm::storage::BitVector> Multiplier<ValueType>::getOptimizationDirectionOverride() const {
+ return optimizationDirectionOverride;
+ }
+
template<typename ValueType>
std::unique_ptr<Multiplier<ValueType>> MultiplierFactory<ValueType>::create(Environment const& env, storm::storage::SparseMatrix<ValueType> 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<GmmxxMultiplier<ValueType>>(matrix);
@@ -99,16 +109,16 @@ namespace storm {
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType");
}
-
+
template class Multiplier<double>;
template class MultiplierFactory<double>;
-
+
#ifdef STORM_HAVE_CARL
template class Multiplier<storm::RationalNumber>;
template class MultiplierFactory<storm::RationalNumber>;
template class Multiplier<storm::RationalFunction>;
template class MultiplierFactory<storm::RationalFunction>;
#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 <vector>
#include <memory>
+#include <boost/optional.hpp>
+
+#include "storm/storage/BitVector.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/solver/MultiplicationStyle.h"
namespace storm {
-
+
class Environment;
-
+
namespace storage {
template<typename ValueType>
class SparseMatrix;
}
-
+
namespace solver {
-
+
template<typename ValueType>
class Multiplier {
public:
-
+
Multiplier(storm::storage::SparseMatrix<ValueType> 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<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& 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<ValueType>& x, std::vector<ValueType> 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<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const;
virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* 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<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, bool backwards = true) const;
virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* 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<ValueType>& x, std::vector<ValueType> 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<ValueType>& x, std::vector<ValueType> 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<ValueType> 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<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const;
-
+
+ /*
+ * TODO
+ */
+ void setOptimizationDirectionOverride(storm::storage::BitVector const& optimizationDirectionOverride);
+
+ /*
+ * TODO
+ */
+ boost::optional<storm::storage::BitVector> getOptimizationDirectionOverride() const;
+
protected:
mutable std::unique_ptr<std::vector<ValueType>> cachedVector;
storm::storage::SparseMatrix<ValueType> const& matrix;
+
+ boost::optional<storm::storage::BitVector> optimizationDirectionOverride = boost::none;
};
-
+
template<typename ValueType>
class MultiplierFactory {
public:
@@ -147,6 +162,6 @@ namespace storm {
std::unique_ptr<Multiplier<ValueType>> create(Environment const& env, storm::storage::SparseMatrix<ValueType> const& matrix);
};
-
+
}
}