From e09cb8600180afca4f705224376a6fcca35a16a6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 23 Nov 2017 22:45:43 +0100 Subject: [PATCH] making sure that the default linear equation solver is not switched to native if we check e.g. an MDP with sound value iteration --- .../csl/helper/SparseCtmcCslHelper.cpp | 2 +- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 6 +++--- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 6 +++--- src/storm/solver/EigenLinearEquationSolver.cpp | 2 +- src/storm/solver/EigenLinearEquationSolver.h | 2 +- .../solver/EliminationLinearEquationSolver.cpp | 2 +- .../solver/EliminationLinearEquationSolver.h | 2 +- src/storm/solver/EquationSystemType.h | 13 ------------- src/storm/solver/GmmxxLinearEquationSolver.cpp | 2 +- src/storm/solver/GmmxxLinearEquationSolver.h | 2 +- .../IterativeMinMaxLinearEquationSolver.cpp | 12 ++++++------ src/storm/solver/LinearEquationSolver.cpp | 16 ++++++++-------- src/storm/solver/LinearEquationSolver.h | 13 +++++-------- src/storm/solver/LinearEquationSolverTask.cpp | 16 ++++++++++++++++ src/storm/solver/LinearEquationSolverTask.h | 13 +++++++++++++ src/storm/solver/NativeLinearEquationSolver.cpp | 2 +- src/storm/solver/NativeLinearEquationSolver.h | 2 +- src/storm/solver/SolveGoal.h | 9 +++++---- src/storm/solver/StandardGameSolver.cpp | 4 ++-- .../StandardMinMaxLinearEquationSolver.cpp | 2 +- .../solver/SymbolicMinMaxLinearEquationSolver.h | 1 - 21 files changed, 71 insertions(+), 58 deletions(-) delete mode 100644 src/storm/solver/EquationSystemType.h create mode 100644 src/storm/solver/LinearEquationSolverTask.cpp create mode 100644 src/storm/solver/LinearEquationSolverTask.h diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 2dfbfbaaa..1a19fca2c 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -664,7 +664,7 @@ namespace storm { } } - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(uniformizedMatrix)); + std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(uniformizedMatrix), storm::solver::LinearEquationSolverTask::Multiply); solver->setCachingEnabled(true); if (!useMixedPoissonProbabilities && std::get<0>(foxGlynnResult) > 1) { diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index a8742c1eb..189245d0b 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -140,7 +140,7 @@ namespace storm { storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); std::vector b = subvector.toVector(odd); - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitSubmatrix)); + std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitSubmatrix), storm::solver::LinearEquationSolverTask::Multiply); solver->repeatedMultiply(x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. @@ -165,7 +165,7 @@ namespace storm { storm::storage::SparseMatrix explicitMatrix = transitionMatrix.toMatrix(odd, odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix)); + std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix), storm::solver::LinearEquationSolverTask::Multiply); solver->repeatedMultiply(x, nullptr, stepBound); // Return a hybrid check result that stores the numerical values explicitly. @@ -191,7 +191,7 @@ namespace storm { std::vector b = totalRewardVector.toVector(odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix)); + std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix), storm::solver::LinearEquationSolverTask::Multiply); solver->repeatedMultiply(x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 50307f0cb..13f877bb4 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -58,7 +58,7 @@ namespace storm { // Perform the matrix vector multiplication as often as required by the formula bound. goal.restrictRelevantValues(maybeStates); - std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix)); + std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix), storm::solver::LinearEquationSolverTask::Multiply); solver->repeatedMultiply(subresult, &b, stepBound); // Set the values of the resulting vector accordingly. @@ -172,7 +172,7 @@ namespace storm { storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); // Perform one single matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, transitionMatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(env, transitionMatrix, storm::solver::LinearEquationSolverTask::Multiply); solver->repeatedMultiply(result, nullptr, 1); return result; } @@ -186,7 +186,7 @@ namespace storm { std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); // Perform the matrix vector multiplication as often as required by the formula bound. - std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, transitionMatrix); + std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, transitionMatrix, storm::solver::LinearEquationSolverTask::Multiply); solver->repeatedMultiply(result, &totalRewardVector, stepBound); return result; diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp index 2457ea99f..874d6f4c4 100644 --- a/src/storm/solver/EigenLinearEquationSolver.cpp +++ b/src/storm/solver/EigenLinearEquationSolver.cpp @@ -284,7 +284,7 @@ namespace storm { } template - std::unique_ptr> EigenLinearEquationSolverFactory::create(Environment const& env) const { + std::unique_ptr> EigenLinearEquationSolverFactory::create(Environment const& env, LinearEquationSolverTask const& task) const { return std::make_unique>(); } diff --git a/src/storm/solver/EigenLinearEquationSolver.h b/src/storm/solver/EigenLinearEquationSolver.h index 3efaf7d95..a6bbae91a 100644 --- a/src/storm/solver/EigenLinearEquationSolver.h +++ b/src/storm/solver/EigenLinearEquationSolver.h @@ -43,7 +43,7 @@ namespace storm { public: using LinearEquationSolverFactory::create; - virtual std::unique_ptr> create(Environment const& env) const override; + virtual std::unique_ptr> create(Environment const& env, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const override; virtual std::unique_ptr> clone() const override; }; diff --git a/src/storm/solver/EliminationLinearEquationSolver.cpp b/src/storm/solver/EliminationLinearEquationSolver.cpp index 46ec27327..3e84b7f0c 100644 --- a/src/storm/solver/EliminationLinearEquationSolver.cpp +++ b/src/storm/solver/EliminationLinearEquationSolver.cpp @@ -126,7 +126,7 @@ namespace storm { } template - std::unique_ptr> EliminationLinearEquationSolverFactory::create(Environment const& env) const { + std::unique_ptr> EliminationLinearEquationSolverFactory::create(Environment const& env, LinearEquationSolverTask const& task) const { return std::make_unique>(); } diff --git a/src/storm/solver/EliminationLinearEquationSolver.h b/src/storm/solver/EliminationLinearEquationSolver.h index 5d35eae76..60403336e 100644 --- a/src/storm/solver/EliminationLinearEquationSolver.h +++ b/src/storm/solver/EliminationLinearEquationSolver.h @@ -46,7 +46,7 @@ namespace storm { public: using LinearEquationSolverFactory::create; - virtual std::unique_ptr> create(Environment const& env) const override; + virtual std::unique_ptr> create(Environment const& env, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const override; virtual std::unique_ptr> clone() const override; diff --git a/src/storm/solver/EquationSystemType.h b/src/storm/solver/EquationSystemType.h deleted file mode 100644 index c68fd3f41..000000000 --- a/src/storm/solver/EquationSystemType.h +++ /dev/null @@ -1,13 +0,0 @@ -#pragma once - -namespace storm { - namespace solver { - - enum class EquationSystemType { - UntilProbabilities, - ReachabilityRewards, - StochasticShortestPath - }; - - } -} diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index c3ff0511a..0f517d5a9 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -168,7 +168,7 @@ namespace storm { } template - std::unique_ptr> GmmxxLinearEquationSolverFactory::create(Environment const& env) const { + std::unique_ptr> GmmxxLinearEquationSolverFactory::create(Environment const& env, LinearEquationSolverTask const& task) const { return std::make_unique>(); } diff --git a/src/storm/solver/GmmxxLinearEquationSolver.h b/src/storm/solver/GmmxxLinearEquationSolver.h index d9fc720bb..bb08cf007 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.h +++ b/src/storm/solver/GmmxxLinearEquationSolver.h @@ -63,7 +63,7 @@ namespace storm { public: using LinearEquationSolverFactory::create; - virtual std::unique_ptr> create(Environment const& env) const override; + virtual std::unique_ptr> create(Environment const& env, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const override; virtual std::unique_ptr> clone() const override; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index ce7100571..03b512915 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -289,7 +289,7 @@ namespace storm { template bool IterativeMinMaxLinearEquationSolver::solveEquationsValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { if (!this->linEqSolverA) { - this->linEqSolverA = this->linearEquationSolverFactory->create(env, *this->A); + this->createLinearEquationSolver(env); this->linEqSolverA->setCachingEnabled(true); } @@ -394,7 +394,7 @@ namespace storm { STORM_LOG_THROW(this->hasUpperBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given."); if (!this->linEqSolverA) { - this->linEqSolverA = this->linearEquationSolverFactory->create(env, *this->A); + this->createLinearEquationSolver(env); this->linEqSolverA->setCachingEnabled(true); } @@ -612,7 +612,7 @@ namespace storm { template void IterativeMinMaxLinearEquationSolver::createLinearEquationSolver(Environment const& env) const { - this->linEqSolverA = this->linearEquationSolverFactory->create(env, *this->A); + this->linEqSolverA = this->linearEquationSolverFactory->create(env, *this->A, LinearEquationSolverTask::Multiply); } template @@ -626,7 +626,7 @@ namespace storm { std::vector rationalB = storm::utility::vector::convertNumericVector(b); if (!this->linEqSolverA) { - this->linEqSolverA = this->linearEquationSolverFactory->create(env, *this->A); + this->createLinearEquationSolver(env); this->linEqSolverA->setCachingEnabled(true); } @@ -656,7 +656,7 @@ namespace storm { // Version for when the overall value type is exact and the same type is to be used for the imprecise part. if (!this->linEqSolverA) { - this->linEqSolverA = this->linearEquationSolverFactory->create(env, *this->A); + this->createLinearEquationSolver(env); this->linEqSolverA->setCachingEnabled(true); } @@ -734,7 +734,7 @@ namespace storm { impreciseA = storm::storage::SparseMatrix(); if (!this->linEqSolverA) { - this->linEqSolverA = this->linearEquationSolverFactory->create(env, *this->A); + createLinearEquationSolver(env); this->linEqSolverA->setCachingEnabled(true); } diff --git a/src/storm/solver/LinearEquationSolver.cpp b/src/storm/solver/LinearEquationSolver.cpp index 30cf11e8c..8ee143cf1 100644 --- a/src/storm/solver/LinearEquationSolver.cpp +++ b/src/storm/solver/LinearEquationSolver.cpp @@ -136,15 +136,15 @@ namespace storm { } template - std::unique_ptr> LinearEquationSolverFactory::create(Environment const& env, storm::storage::SparseMatrix const& matrix) const { - std::unique_ptr> solver = this->create(env); + std::unique_ptr> LinearEquationSolverFactory::create(Environment const& env, storm::storage::SparseMatrix const& matrix, LinearEquationSolverTask const& task) const { + std::unique_ptr> solver = this->create(env, task); solver->setMatrix(matrix); return solver; } template - std::unique_ptr> LinearEquationSolverFactory::create(Environment const& env, storm::storage::SparseMatrix&& matrix) const { - std::unique_ptr> solver = this->create(env); + std::unique_ptr> LinearEquationSolverFactory::create(Environment const& env, storm::storage::SparseMatrix&& matrix, LinearEquationSolverTask const& task) const { + std::unique_ptr> solver = this->create(env, task); solver->setMatrix(std::move(matrix)); return solver; } @@ -166,7 +166,7 @@ namespace storm { template<> - std::unique_ptr> GeneralLinearEquationSolverFactory::create(Environment const& env) const { + std::unique_ptr> GeneralLinearEquationSolverFactory::create(Environment const& env, LinearEquationSolverTask const& task) const { EquationSolverType type = env.solver().getLinearEquationSolverType(); // Adjust the solver type if it is not supported by this value type @@ -186,7 +186,7 @@ namespace storm { } template<> - std::unique_ptr> GeneralLinearEquationSolverFactory::create(Environment const& env) const { + std::unique_ptr> GeneralLinearEquationSolverFactory::create(Environment const& env, LinearEquationSolverTask const& task) const { EquationSolverType type = env.solver().getLinearEquationSolverType(); // Adjust the solver type if it is not supported by this value type @@ -206,11 +206,11 @@ namespace storm { } template - std::unique_ptr> GeneralLinearEquationSolverFactory::create(Environment const& env) const { + std::unique_ptr> GeneralLinearEquationSolverFactory::create(Environment const& env, LinearEquationSolverTask const& task) const { EquationSolverType type = env.solver().getLinearEquationSolverType(); // Adjust the solver type if none was specified and we want sound computations - if (env.solver().isForceSoundness() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination) { + if (env.solver().isForceSoundness() && task != LinearEquationSolverTask::Multiply, type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination) { if (env.solver().isLinearEquationSolverTypeSetFromDefaultValue()) { type = EquationSolverType::Native; STORM_LOG_INFO("Selecting '" + toString(type) + "' as the linear equation solver to guarantee sound results. If you want to override this, please explicitly specify a different solver."); diff --git a/src/storm/solver/LinearEquationSolver.h b/src/storm/solver/LinearEquationSolver.h index de17808c8..6b45ec491 100644 --- a/src/storm/solver/LinearEquationSolver.h +++ b/src/storm/solver/LinearEquationSolver.h @@ -8,6 +8,7 @@ #include "storm/solver/MultiplicationStyle.h" #include "storm/solver/LinearEquationSolverProblemFormat.h" #include "storm/solver/LinearEquationSolverRequirements.h" +#include "storm/solver/LinearEquationSolverTask.h" #include "storm/solver/OptimizationDirection.h" #include "storm/utility/VectorHelper.h" @@ -20,10 +21,6 @@ namespace storm { namespace solver { - enum class LinearEquationSolverOperation { - SolveEquations, MultiplyRepeatedly - }; - /*! * An interface that represents an abstract linear equation solver. In addition to solving a system of linear * equations, the functionality to repeatedly multiply a matrix with a given vector is provided. @@ -190,7 +187,7 @@ namespace storm { * @param matrix The matrix that defines the equation system. * @return A pointer to the newly created solver. */ - std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& matrix) const; + std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& matrix, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const; /*! * Creates a new linear equation solver instance with the given matrix. The caller gives up posession of the @@ -199,12 +196,12 @@ namespace storm { * @param matrix The matrix that defines the equation system. * @return A pointer to the newly created solver. */ - std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix&& matrix) const; + std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix&& matrix, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const; /*! * Creates an equation solver with the current settings, but without a matrix. */ - virtual std::unique_ptr> create(Environment const& env) const = 0; + virtual std::unique_ptr> create(Environment const& env, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const = 0; /*! * Creates a copy of this factory. @@ -230,7 +227,7 @@ namespace storm { using LinearEquationSolverFactory::create; - virtual std::unique_ptr> create(Environment const& env) const override; + virtual std::unique_ptr> create(Environment const& env, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const override; virtual std::unique_ptr> clone() const override; }; diff --git a/src/storm/solver/LinearEquationSolverTask.cpp b/src/storm/solver/LinearEquationSolverTask.cpp new file mode 100644 index 000000000..91783ae36 --- /dev/null +++ b/src/storm/solver/LinearEquationSolverTask.cpp @@ -0,0 +1,16 @@ +#include "storm/solver/LinearEquationSolverTask.h" + +namespace storm { + namespace solver { + + std::ostream& operator<<(std::ostream& out, LinearEquationSolverTask const& task) { + switch (task) { + case LinearEquationSolverTask::Unspecified: out << "unspecified"; break; + case LinearEquationSolverTask::SolveEquations: out << "solve equations"; break; + case LinearEquationSolverTask::Multiply: out << "multiply"; break; + } + return out; + } + + } +} diff --git a/src/storm/solver/LinearEquationSolverTask.h b/src/storm/solver/LinearEquationSolverTask.h new file mode 100644 index 000000000..5d3a401dd --- /dev/null +++ b/src/storm/solver/LinearEquationSolverTask.h @@ -0,0 +1,13 @@ +#pragma once + +#include + +namespace storm { + namespace solver { + + enum class LinearEquationSolverTask { Unspecified, SolveEquations, Multiply }; + + std::ostream& operator<<(std::ostream& out, LinearEquationSolverTask const& style); + + } +} diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 6517daef0..387935970 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -959,7 +959,7 @@ namespace storm { } template - std::unique_ptr> NativeLinearEquationSolverFactory::create(Environment const& env) const { + std::unique_ptr> NativeLinearEquationSolverFactory::create(Environment const& env, LinearEquationSolverTask const& task) const { return std::make_unique>(); } diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h index 3c17444fd..0fb4970e4 100644 --- a/src/storm/solver/NativeLinearEquationSolver.h +++ b/src/storm/solver/NativeLinearEquationSolver.h @@ -123,7 +123,7 @@ namespace storm { public: using LinearEquationSolverFactory::create; - virtual std::unique_ptr> create(Environment const& env) const override; + virtual std::unique_ptr> create(Environment const& env, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const override; virtual std::unique_ptr> clone() const override; diff --git a/src/storm/solver/SolveGoal.h b/src/storm/solver/SolveGoal.h index 9bd6f7e73..d93b86b91 100644 --- a/src/storm/solver/SolveGoal.h +++ b/src/storm/solver/SolveGoal.h @@ -7,6 +7,7 @@ #include "storm/solver/OptimizationDirection.h" #include "storm/logic/ComparisonType.h" #include "storm/storage/BitVector.h" +#include "storm/solver/LinearEquationSolverTask.h" #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/MinMaxLinearEquationSolver.h" @@ -110,8 +111,8 @@ namespace storm { } template - std::unique_ptr> configureLinearEquationSolver(Environment const& env, SolveGoal&& goal, storm::solver::LinearEquationSolverFactory const& factory, MatrixType&& matrix) { - std::unique_ptr> solver = factory.create(env, std::forward(matrix)); + std::unique_ptr> configureLinearEquationSolver(Environment const& env, SolveGoal&& goal, storm::solver::LinearEquationSolverFactory const& factory, MatrixType&& matrix, storm::solver::LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) { + std::unique_ptr> solver = factory.create(env, std::forward(matrix), task); if (goal.isBounded()) { solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize())); } @@ -119,8 +120,8 @@ namespace storm { } template - std::unique_ptr> configureLinearEquationSolver(Environment const& env, SolveGoal&& goal, storm::solver::LinearEquationSolverFactory const& factory, MatrixType&& matrix) { - std::unique_ptr> solver = factory.create(env, std::forward(matrix)); + std::unique_ptr> configureLinearEquationSolver(Environment const& env, SolveGoal&& goal, storm::solver::LinearEquationSolverFactory const& factory, MatrixType&& matrix, storm::solver::LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) { + std::unique_ptr> solver = factory.create(env, std::forward(matrix), task); return solver; } diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index f345dcb93..26d4cc3d0 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -139,7 +139,7 @@ namespace storm { bool StandardGameSolver::solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const { if(!linEqSolverPlayer2Matrix) { - linEqSolverPlayer2Matrix = linearEquationSolverFactory->create(env, player2Matrix); + linEqSolverPlayer2Matrix = linearEquationSolverFactory->create(env, player2Matrix, storm::solver::LinearEquationSolverTask::Multiply); linEqSolverPlayer2Matrix->setCachingEnabled(true); } @@ -222,7 +222,7 @@ namespace storm { void StandardGameSolver::repeatedMultiply(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { if(!linEqSolverPlayer2Matrix) { - linEqSolverPlayer2Matrix = linearEquationSolverFactory->create(env, player2Matrix); + linEqSolverPlayer2Matrix = linearEquationSolverFactory->create(env, player2Matrix, storm::solver::LinearEquationSolverTask::Multiply); linEqSolverPlayer2Matrix->setCachingEnabled(true); } diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index d1e946afd..a8b042dc7 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -46,7 +46,7 @@ namespace storm { template void StandardMinMaxLinearEquationSolver::repeatedMultiply(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { if (!linEqSolverA) { - linEqSolverA = linearEquationSolverFactory->create(env, *A); + linEqSolverA = linearEquationSolverFactory->create(env, *A, LinearEquationSolverTask::Multiply); linEqSolverA->setCachingEnabled(true); } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index 95be76a0c..d9c78466e 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -9,7 +9,6 @@ #include "storm/solver/SymbolicEquationSolver.h" #include "storm/solver/OptimizationDirection.h" #include "storm/solver/SymbolicLinearEquationSolver.h" -#include "storm/solver/EquationSystemType.h" #include "storm/solver/MinMaxLinearEquationSolverRequirements.h" #include "storm/solver/SolverStatus.h"