diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 3add9ad41..5143fcdef 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -10,17 +10,17 @@ namespace storm { namespace solver { template - LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { + LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(std::unique_ptr>&& lpSolverFactory) : lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty. } template - LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(A, std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { + LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(A), lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty. } template - LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(std::move(A), std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { + LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(std::move(A)), lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty. } @@ -113,7 +113,7 @@ namespace storm { template MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& hasInitialScheduler) const { - MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env, LinearEquationSolverTask::Multiply)); + MinMaxLinearEquationSolverRequirements requirements; // In case we need to retrieve a scheduler, the solution has to be unique if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) { @@ -127,38 +127,10 @@ namespace storm { return requirements; } - template - LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory(), lpSolverFactory(std::make_unique>()) { - // Intentionally left empty - } - - template - LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory(), lpSolverFactory(std::move(lpSolverFactory)) { - // Intentionally left empty - } - - template - LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory(std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { - // Intentionally left empty - } - - template - std::unique_ptr> LpMinMaxLinearEquationSolverFactory::create(Environment const& env) const { - STORM_LOG_THROW(env.solver().minMax().getMethod() == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidEnvironmentException, "This min max solver does not support the selected technique."); - STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized."); - STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); - - std::unique_ptr> result = std::make_unique>(this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); - result->setRequirementsChecked(this->isRequirementsCheckedSet()); - return result; - } - template class LpMinMaxLinearEquationSolver; - template class LpMinMaxLinearEquationSolverFactory; #ifdef STORM_HAVE_CARL template class LpMinMaxLinearEquationSolver; - template class LpMinMaxLinearEquationSolverFactory; #endif } } diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h index e8a531e67..72ba6871e 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.h +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -13,9 +13,9 @@ namespace storm { template class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver { public: - LpMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); - LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); - LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); + LpMinMaxLinearEquationSolver(std::unique_ptr>&& lpSolverFactory); + LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& lpSolverFactory); + LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& lpSolverFactory); virtual bool internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const override; @@ -27,20 +27,5 @@ namespace storm { std::unique_ptr> lpSolverFactory; }; - template - class LpMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { - public: - LpMinMaxLinearEquationSolverFactory(); - LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& lpSolverFactory); - LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); - - // Make the other create methods visible. - using MinMaxLinearEquationSolverFactory::create; - - virtual std::unique_ptr> create(Environment const& env) const override; - - private: - std::unique_ptr> lpSolverFactory; - }; } } diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 20194ec6b..f7cbf4bfe 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -40,12 +40,6 @@ namespace storm { solveEquations(env, convert(this->direction), x, b); } - template - void MinMaxLinearEquationSolver::repeatedMultiply(Environment const& env, std::vector& x, std::vector* b, uint_fast64_t n) const { - STORM_LOG_THROW(isSet(this->direction), storm::exceptions::IllegalFunctionCallException, "Optimization direction not set."); - return repeatedMultiply(env, convert(this->direction), x, b, n); - } - template void MinMaxLinearEquationSolver::setOptimizationDirection(OptimizationDirection d) { direction = convert(d); @@ -204,7 +198,7 @@ namespace storm { } else if (method == MinMaxMethod::TopologicalCuda) { result = std::make_unique>(); } else if (method == MinMaxMethod::LinearProgramming) { - result = std::make_unique>(std::make_unique>(), std::make_unique>()); + result = std::make_unique>(std::make_unique>()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } @@ -219,7 +213,7 @@ namespace storm { if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration) { result = std::make_unique>(std::make_unique>()); } else if (method == MinMaxMethod::LinearProgramming) { - result = std::make_unique>(std::make_unique>(), std::make_unique>()); + result = std::make_unique>(std::make_unique>()); } else if (method == MinMaxMethod::Topological) { result = std::make_unique>(); } else { diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 159b3e46e..00788089c 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -60,32 +60,6 @@ namespace storm { */ void solveEquations(Environment const& env, std::vector& x, std::vector const& b) const; - /*! - * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes - * x[i+1] = min/max(A*x[i] + b) until x[n], where x[0] = x. After each multiplication and addition, the - * minimal/maximal value out of each row group is selected to reduce the resulting vector to obtain the - * vector for the next iteration. Note that the matrix A has to be given upon construction time of the - * solver object. - * - * @param d For minimum, all the value of a group of rows is the taken as the minimum over all rows and as - * the maximum otherwise. - * @param x The initial vector that is to be multiplied with the matrix. This is also the output parameter, - * i.e. after the method returns, this vector will contain the computed values. - * @param b If not null, this vector is added after each multiplication. - * @param n Specifies the number of iterations the matrix-vector multiplication is performed. - * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this - * vector must be equal to the number of rows of A. - * @return The result of the repeated matrix-vector multiplication as the content of the vector x. - */ - virtual void repeatedMultiply(Environment const& env, OptimizationDirection d, std::vector& x, std::vector const* b, uint_fast64_t n = 1) const = 0; - - /*! - * Behaves the same as the other variant of multiply, with the - * distinction that instead of providing the optimization direction as an argument, the internally set - * optimization direction is used. Note: this method can only be called after setting the optimization direction. - */ - virtual void repeatedMultiply(Environment const& env, std::vector& x, std::vector* b , uint_fast64_t n) const; - /*! * Sets an optimization direction to use for calls to methods that do not explicitly provide one. */ diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 57120ef77..c2878cebb 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -18,17 +18,17 @@ namespace storm { namespace solver { template - StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), A(nullptr) { + StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver() : A(nullptr) { // Intentionally left empty. } template - StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(&A) { + StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : localA(nullptr), A(&A) { // Intentionally left empty. } template - StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique>(std::move(A))), A(localA.get()) { + StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A) : localA(std::make_unique>(std::move(A))), A(localA.get()) { // Intentionally left empty. } @@ -36,124 +36,20 @@ namespace storm { void StandardMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& matrix) { this->localA = nullptr; this->A = &matrix; - clearCache(); + this->clearCache(); } template void StandardMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& matrix) { this->localA = std::make_unique>(std::move(matrix)); this->A = this->localA.get(); - clearCache(); - } - - 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, LinearEquationSolverTask::Multiply); - linEqSolverA->setCachingEnabled(true); - } - - if (!auxiliaryRowGroupVector) { - auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); - } - - this->startMeasureProgress(); - for (uint64_t i = 0; i < n; ++i) { - linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, b, *auxiliaryRowGroupVector); - std::swap(x, *auxiliaryRowGroupVector); - - // Potentially show progress. - this->showProgressIterative(i, n); - } - - if (!this->isCachingEnabled()) { - clearCache(); - } - } - - template - void StandardMinMaxLinearEquationSolver::clearCache() const { - linEqSolverA.reset(); - auxiliaryRowVector.reset(); - MinMaxLinearEquationSolver::clearCache(); - } - - template - StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory() : MinMaxLinearEquationSolverFactory(), linearEquationSolverFactory(std::make_unique>()) { - // Intentionally left empty. - } - - template - StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory) : MinMaxLinearEquationSolverFactory(), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { - // Intentionally left empty. - } - - template - StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType) : MinMaxLinearEquationSolverFactory() { - switch (solverType) { - case EquationSolverType::Gmmxx: linearEquationSolverFactory = std::make_unique>(); break; - case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique>(); break; - case EquationSolverType::Native: linearEquationSolverFactory = std::make_unique>(); break; - case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique>(); break; - case EquationSolverType::Topological: linearEquationSolverFactory = std::make_unique>(); break; - } - } - - template<> - StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType) : MinMaxLinearEquationSolverFactory() { - switch (solverType) { - case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique>(); break; - case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique>(); break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported equation solver for this data type."); - } - } - - template - std::unique_ptr> StandardMinMaxLinearEquationSolverFactory::create(Environment const& env) const { - std::unique_ptr> result; - auto method = env.solver().minMax().getMethod(); - if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration) { - result = std::make_unique>(this->linearEquationSolverFactory->clone()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The selected min max method is not supported by this solver."); - } - result->setRequirementsChecked(this->isRequirementsCheckedSet()); - return result; - } - - template - GmmxxMinMaxLinearEquationSolverFactory::GmmxxMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Gmmxx) { - // Intentionally left empty. - } - - template - EigenMinMaxLinearEquationSolverFactory::EigenMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Eigen) { - // Intentionally left empty. - } - - template - NativeMinMaxLinearEquationSolverFactory::NativeMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Native) { - // Intentionally left empty. - } - - template - EliminationMinMaxLinearEquationSolverFactory::EliminationMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Elimination) { - // Intentionally left empty. + this->clearCache(); } template class StandardMinMaxLinearEquationSolver; - template class StandardMinMaxLinearEquationSolverFactory; - template class GmmxxMinMaxLinearEquationSolverFactory; - template class EigenMinMaxLinearEquationSolverFactory; - template class NativeMinMaxLinearEquationSolverFactory; - template class EliminationMinMaxLinearEquationSolverFactory; #ifdef STORM_HAVE_CARL template class StandardMinMaxLinearEquationSolver; - template class StandardMinMaxLinearEquationSolverFactory; - template class EigenMinMaxLinearEquationSolverFactory; - template class EliminationMinMaxLinearEquationSolverFactory; #endif } } diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.h b/src/storm/solver/StandardMinMaxLinearEquationSolver.h index 580e89347..9e79f482b 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.h @@ -12,29 +12,17 @@ namespace storm { template class StandardMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { public: - StandardMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory); - StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory); - StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory); + StandardMinMaxLinearEquationSolver(); + explicit StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); + explicit StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A); virtual void setMatrix(storm::storage::SparseMatrix const& matrix) override; virtual void setMatrix(storm::storage::SparseMatrix&& matrix) override; virtual ~StandardMinMaxLinearEquationSolver() = default; - virtual void repeatedMultiply(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const override; - - virtual void clearCache() const override; - protected: - // possibly cached data - mutable std::unique_ptr> linEqSolverA; - mutable std::unique_ptr> auxiliaryRowVector; // A.rowCount() entries - mutable std::unique_ptr> auxiliaryRowGroupVector; // A.rowCount() entries - - /// The factory used to obtain linear equation solvers. - std::unique_ptr> linearEquationSolverFactory; - // If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted // when the solver is destructed. std::unique_ptr> localA; @@ -44,48 +32,5 @@ namespace storm { storm::storage::SparseMatrix const* A; }; - template - class StandardMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { - public: - StandardMinMaxLinearEquationSolverFactory(); - StandardMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory); - StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType); - - // Make the other create methods visible. - using MinMaxLinearEquationSolverFactory::create; - - virtual std::unique_ptr> create(Environment const& env) const override; - - protected: - std::unique_ptr> linearEquationSolverFactory; - - private: - void createLinearEquationSolverFactory() const; - }; - - template - class GmmxxMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { - public: - GmmxxMinMaxLinearEquationSolverFactory(); - }; - - template - class EigenMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { - public: - EigenMinMaxLinearEquationSolverFactory(); - }; - - template - class NativeMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { - public: - NativeMinMaxLinearEquationSolverFactory(); - }; - - template - class EliminationMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { - public: - EliminationMinMaxLinearEquationSolverFactory(); - }; - } } diff --git a/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp index 839c9417f..f31d1cde3 100644 --- a/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp @@ -447,25 +447,6 @@ namespace storm { return result; } - template - void TopologicalCudaMinMaxLinearEquationSolver::repeatedMultiply(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { - std::unique_ptr> multiplyResult = std::make_unique>(this->A->getRowCount()); - - // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - for (uint_fast64_t i = 0; i < n; ++i) { - this->A->multiplyWithVector(x, *multiplyResult); - - // Add b if it is non-null. - if (b != nullptr) { - storm::utility::vector::addVectors(*multiplyResult, *b, *multiplyResult); - } - - // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost - // element of the min/max operator stack. - storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A->getRowGroupIndices()); - } - } - template TopologicalCudaMinMaxLinearEquationSolverFactory::TopologicalCudaMinMaxLinearEquationSolverFactory(bool trackScheduler) { // Intentionally left empty. diff --git a/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.h index f20f37b09..7005d9d8f 100644 --- a/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.h +++ b/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.h @@ -39,8 +39,6 @@ namespace storm { virtual bool internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const override; - virtual void repeatedMultiply(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const override; - private: storm::storage::SparseMatrix const* A; std::unique_ptr> localA; diff --git a/src/storm/solver/TopologicalLinearEquationSolver.h b/src/storm/solver/TopologicalLinearEquationSolver.h index 5a36ec9af..4c754c44e 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.h +++ b/src/storm/solver/TopologicalLinearEquationSolver.h @@ -56,9 +56,6 @@ namespace storm { // the pointer refers to localA. storm::storage::SparseMatrix const* A; - // An object to dispatch all multiplication operations. - NativeMultiplier multiplier; - // cached auxiliary data mutable std::unique_ptr> sortedSccDecomposition; mutable boost::optional longestSccChainSize; diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 43e080850..70c478ffd 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -14,32 +14,18 @@ namespace storm { namespace solver { template - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver() : localA(nullptr), A(nullptr) { + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver() { // Intentionally left empty. } template - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : localA(nullptr), A(nullptr) { - this->setMatrix(A); - } - - template - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A) : localA(nullptr), A(nullptr) { - this->setMatrix(std::move(A)); - } - - template - void TopologicalMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& A) { - localA.reset(); - this->A = &A; - clearCache(); + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : StandardMinMaxLinearEquationSolver(A) { + // Intentionally left empty. } template - void TopologicalMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& A) { - localA = std::make_unique>(std::move(A)); - this->A = localA.get(); - clearCache(); + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A) : StandardMinMaxLinearEquationSolver(std::move(A)) { + // Intentionally left empty. } template @@ -59,12 +45,6 @@ namespace storm { STORM_LOG_ASSERT(x.size() == this->A->getRowGroupCount(), "Provided x-vector has invalid size."); STORM_LOG_ASSERT(b.size() == this->A->getRowCount(), "Provided b-vector has invalid size."); - //std::cout << "Solving equation system with fixpoint characterization " << std::endl; - //std::cout << *this->A << std::endl; - //std::cout << storm::utility::vector::toString(b) << std::endl; - //std::cout << "Initial solution vector: " << std::endl; - //std::cout << storm::utility::vector::toString(x) << std::endl; - // For sound computations we need to increase the precision in each SCC bool needAdaptPrecision = env.solver().isForceSoundness(); @@ -307,24 +287,6 @@ namespace storm { return res; } - template - void TopologicalMinMaxLinearEquationSolver::repeatedMultiply(Environment const& env, OptimizationDirection d, std::vector& x, std::vector const* b, uint_fast64_t n) const { - - storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env); - - // Set up the SCC solver - if (!this->sccSolver) { - this->sccSolver = GeneralMinMaxLinearEquationSolverFactory().create(sccSolverEnvironment); - this->sccSolver->setCachingEnabled(true); - } - this->sccSolver->setMatrix(*this->A); - this->sccSolver->repeatedMultiply(sccSolverEnvironment, d, x, b, n); - - if (!this->isCachingEnabled()) { - clearCache(); - } - } - template MinMaxLinearEquationSolverRequirements TopologicalMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& hasInitialScheduler) const { // Return the requirements of the underlying solver @@ -337,21 +299,14 @@ namespace storm { longestSccChainSize = boost::none; sccSolver.reset(); auxiliaryRowGroupVector.reset(); - MinMaxLinearEquationSolver::clearCache(); - } - - template - std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::create(Environment const& env) const { - return std::make_unique>(); + StandardMinMaxLinearEquationSolver::clearCache(); } // Explicitly instantiate the min max linear equation solver. template class TopologicalMinMaxLinearEquationSolver; - template class TopologicalMinMaxLinearEquationSolverFactory; #ifdef STORM_HAVE_CARL template class TopologicalMinMaxLinearEquationSolver; - template class TopologicalMinMaxLinearEquationSolverFactory; #endif } } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h index 9cf3c3d11..cdbc781bc 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/solver/SolverSelectionOptions.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" @@ -12,18 +12,14 @@ namespace storm { namespace solver { template - class TopologicalMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { + class TopologicalMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver { public: TopologicalMinMaxLinearEquationSolver(); TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A); - virtual void setMatrix(storm::storage::SparseMatrix const& A) override; - virtual void setMatrix(storm::storage::SparseMatrix&& A) override; - virtual void clearCache() const override; - virtual void repeatedMultiply(Environment const& env, OptimizationDirection d, std::vector& x, std::vector const* b, uint_fast64_t n = 1) const override; virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& hasInitialScheduler = false) const override ; protected: @@ -44,29 +40,11 @@ namespace storm { // ... for the remaining cases (1 < scc.size() < x.size()) bool solveScc(storm::Environment const& sccSolverEnvironment, OptimizationDirection d, storm::storage::BitVector const& sccRowGroups, storm::storage::BitVector const& sccRows, std::vector& globalX, std::vector const& globalB) const; - // If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted - // when the solver is destructed. - std::unique_ptr> localA; - - // A pointer to the original sparse matrix given to this solver. If the solver takes posession of the matrix - // the pointer refers to localA. - storm::storage::SparseMatrix const* A; - // cached auxiliary data mutable std::unique_ptr> sortedSccDecomposition; mutable boost::optional longestSccChainSize; mutable std::unique_ptr> sccSolver; mutable std::unique_ptr> auxiliaryRowGroupVector; // A.rowGroupCount() entries }; - - template - class TopologicalMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { - public: - using MinMaxLinearEquationSolverFactory::create; - - virtual std::unique_ptr> create(Environment const& env) const override; - - }; - } }