From 53ff4829479bfe2c128e8ba9998a586e161baed0 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 17 Nov 2016 11:39:57 +0100 Subject: [PATCH] Caching of solvers can now be enabled/disabled Former-commit-id: 498622f45cf54f5fb0d0a7bbe8f8af303d09f72c [formerly 1713f554a03c96611fda0188056486de1fdaa393] Former-commit-id: 1015c7fef83b515337fbad6637c65f042002c097 --- .../csl/helper/SparseCtmcCslHelper.cpp | 7 +-- .../helper/SparseMarkovAutomatonCslHelper.cpp | 1 + .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 2 + src/solver/EigenLinearEquationSolver.cpp | 4 +- .../EliminationLinearEquationSolver.cpp | 4 +- src/solver/GmmxxLinearEquationSolver.cpp | 28 ++++++++---- src/solver/GmmxxLinearEquationSolver.h | 7 +-- src/solver/LinearEquationSolver.cpp | 42 ++++++++++++++---- src/solver/LinearEquationSolver.h | 22 ++++++++-- src/solver/MinMaxLinearEquationSolver.cpp | 18 +++++++- src/solver/MinMaxLinearEquationSolver.h | 20 ++++++++- src/solver/NativeLinearEquationSolver.cpp | 43 ++++++++++++------- src/solver/NativeLinearEquationSolver.h | 6 +-- .../StandardMinMaxLinearEquationSolver.cpp | 19 +++++++- .../StandardMinMaxLinearEquationSolver.h | 3 +- src/utility/policyguessing.cpp | 2 + 16 files changed, 167 insertions(+), 61 deletions(-) diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index df8e06c4a..7e968c345 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -629,6 +629,7 @@ namespace storm { } std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(uniformizedMatrix)); + solver->setCachingEnabled(true); if (!useMixedPoissonProbabilities && std::get<0>(foxGlynnResult) > 1) { // Perform the matrix-vector multiplications (without adding). @@ -735,12 +736,6 @@ namespace storm { template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); - - - - - - #endif } } diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 6b6ff0fa1..75012b672 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -86,6 +86,7 @@ namespace storm { } std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); + solver->setCachingEnabled(true); // Perform the actual value iteration // * loop until the step bound has been reached diff --git a/src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 2e4e13439..6bd3b76e6 100644 --- a/src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -307,6 +307,7 @@ namespace storm { result->solver = minMaxSolverFactory.create(PS.toPS); result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); result->solver->setTrackScheduler(true); + result->solver->setCachingEnabled(true); result->b.resize(PS.getNumberOfChoices()); @@ -365,6 +366,7 @@ namespace storm { storm::storage::SparseMatrix linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true); linEqMatrix.convertToEquationSystem(); linEq.solver = linEq.factory.create(std::move(linEqMatrix)); + linEq.solver->setCachingEnabled(true); } // Get the results for the individual objectives. diff --git a/src/solver/EigenLinearEquationSolver.cpp b/src/solver/EigenLinearEquationSolver.cpp index bdc6e6a07..0d3b9c7d7 100644 --- a/src/solver/EigenLinearEquationSolver.cpp +++ b/src/solver/EigenLinearEquationSolver.cpp @@ -117,7 +117,7 @@ namespace storm { template void EigenLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& A) { eigenA = storm::adapters::EigenAdapter::toEigenSparseMatrix(A); - this->resetAuxiliaryData(); + this->clearCache(); } template @@ -125,7 +125,7 @@ namespace storm { // Take ownership of the matrix so it is destroyed after we have translated it to Eigen's format. storm::storage::SparseMatrix localA(std::move(A)); this->setMatrix(localA); - this->resetAuxiliaryData(); + this->clearCache(); } template diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp index e46148b18..1f33d7bd0 100644 --- a/src/solver/EliminationLinearEquationSolver.cpp +++ b/src/solver/EliminationLinearEquationSolver.cpp @@ -47,14 +47,14 @@ namespace storm { void EliminationLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& A) { this->A = &A; localA.reset(); - this->resetAuxiliaryData(); + this->clearCache(); } template void EliminationLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& A) { localA = std::make_unique>(std::move(A)); this->A = localA.get(); - this->resetAuxiliaryData(); + this->clearCache(); } template diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index 7c58241b5..5d301fee5 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -124,14 +124,14 @@ namespace storm { void GmmxxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& A) { localA.reset(); this->A = &A; - resetAuxiliaryData(); + clearCache(); } template void GmmxxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& A) { localA = std::make_unique>(std::move(A)); this->A = localA.get(); - resetAuxiliaryData(); + clearCache(); } template @@ -187,6 +187,10 @@ namespace storm { } } + if(!this->isCachingEnabled()) { + clearCache(); + } + // Check if the solver converged and issue a warning otherwise. if (iter.converged()) { STORM_LOG_INFO("Iterative solver converged after " << iter.get_iteration() << " iterations."); @@ -221,6 +225,10 @@ namespace storm { } else { gmm::mult(*gmmxxA, x, result); } + + if(!this->isCachingEnabled()) { + clearCache(); + } } template @@ -238,10 +246,10 @@ namespace storm { std::vector* currentX = &x; - if(!this->auxiliaryRowVector) { - this->auxiliaryRowVector = std::make_unique>(getMatrixRowCount()); + if(!this->cachedRowVector) { + this->cachedRowVector = std::make_unique>(getMatrixRowCount()); } - std::vector* nextX = this->auxiliaryRowVector.get(); + std::vector* nextX = this->cachedRowVector.get(); // Set up additional environment variables. uint_fast64_t iterationCount = 0; @@ -264,10 +272,14 @@ namespace storm { // If the last iteration did not write to the original x we have to swap the contents, because the // output has to be written to the input parameter x. - if (currentX == this->auxiliaryRowVector.get()) { + if (currentX == this->cachedRowVector.get()) { std::swap(x, *currentX); } + if(!this->isCachingEnabled()) { + clearCache(); + } + return iterationCount; } @@ -282,12 +294,12 @@ namespace storm { } template - void GmmxxLinearEquationSolver::resetAuxiliaryData() const { + void GmmxxLinearEquationSolver::clearCache() const { gmmxxA.reset(); iluPreconditioner.reset(); diagonalPreconditioner.reset(); jacobiDecomposition.reset(); - LinearEquationSolver::resetAuxiliaryData(); + LinearEquationSolver::clearCache(); } template diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h index 09a50a92e..b607f76fa 100644 --- a/src/solver/GmmxxLinearEquationSolver.h +++ b/src/solver/GmmxxLinearEquationSolver.h @@ -98,11 +98,8 @@ namespace storm { void setSettings(GmmxxLinearEquationSolverSettings const& newSettings); GmmxxLinearEquationSolverSettings const& getSettings() const; - /* - * Clears auxiliary data that has possibly been stored during previous calls of the solver. - */ - virtual void resetAuxiliaryData() const override; + virtual void clearCache() const override; private: /*! @@ -130,7 +127,7 @@ namespace storm { // The settings used by the solver. GmmxxLinearEquationSolverSettings settings; - // Auxiliary data obtained during solving + // cached data obtained during solving mutable std::unique_ptr> gmmxxA; mutable std::unique_ptr>> iluPreconditioner; mutable std::unique_ptr>> diagonalPreconditioner; diff --git a/src/solver/LinearEquationSolver.cpp b/src/solver/LinearEquationSolver.cpp index 029e596fc..1e9e61deb 100644 --- a/src/solver/LinearEquationSolver.cpp +++ b/src/solver/LinearEquationSolver.cpp @@ -14,21 +14,26 @@ namespace storm { namespace solver { template - LinearEquationSolver::LinearEquationSolver() { + LinearEquationSolver::LinearEquationSolver() : cachingEnabled(false) { // Intentionally left empty. } template void LinearEquationSolver::repeatedMultiply(std::vector& x, std::vector const* b, uint_fast64_t n) const { - if(!auxiliaryRowVector) { - auxiliaryRowVector = std::make_unique>(getMatrixRowCount()); + if(!cachedRowVector) { + cachedRowVector = std::make_unique>(getMatrixRowCount()); } + // We enable caching for this. But remember how the old setting was + bool cachingWasEnabled = isCachingEnabled(); + setCachingEnabled(true); + // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. std::vector* currentX = &x; - std::vector* nextX = auxiliaryRowVector.get(); + std::vector* nextX = cachedRowVector.get(); + // Now perform matrix-vector multiplication as long as we meet the bound. for (uint_fast64_t i = 0; i < n; ++i) { @@ -38,16 +43,37 @@ namespace storm { // If we performed an odd number of repetitions, we need to swap the contents of currentVector and x, // because the output is supposed to be stored in the input vector x. - if (currentX == auxiliaryRowVector.get()) { + if (currentX == cachedRowVector.get()) { std::swap(x, *currentX); } + + // restore the old caching setting + setCachingEnabled(cachingWasEnabled); + + if(!isCachingEnabled()) { + clearCache(); + } } template - void LinearEquationSolver::resetAuxiliaryData() const { - auxiliaryRowVector.reset(); + void LinearEquationSolver::setCachingEnabled(bool value) const { + if(cachingEnabled && !value) { + // caching will be turned off. Hence we clear the cache at this point + clearCache(); + } + cachingEnabled = value; } - + + template + bool LinearEquationSolver::isCachingEnabled() const { + return cachingEnabled; + } + + template + void LinearEquationSolver::clearCache() const { + cachedRowVector.reset(); + } + template std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { return create(matrix); diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index 7988d2c6a..4c56005ee 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -67,15 +67,26 @@ namespace storm { * @param n The number of times to perform the multiplication. */ void repeatedMultiply(std::vector& x, std::vector const* b, uint_fast64_t n) const; - + + /*! + * Sets whether some of the generated data during solver calls should be cached. + * This possibly decreases the runtime of subsequent calls but also increases memory consumption. + */ + void setCachingEnabled(bool value) const; + + /*! + * Retrieves whether some of the generated data during solver calls should be cached. + */ + bool isCachingEnabled() const; + /* - * Clears auxiliary data that has possibly been stored during previous calls of the solver. + * Clears the currently cached data that has been stored during previous calls of the solver. */ - virtual void resetAuxiliaryData() const; + virtual void clearCache() const; protected: // auxiliary storage. If set, this vector has getMatrixRowCount() entries. - mutable std::unique_ptr> auxiliaryRowVector; + mutable std::unique_ptr> cachedRowVector; private: /*! @@ -87,6 +98,9 @@ namespace storm { * Retrieves the column count of the matrix associated with this solver. */ virtual uint64_t getMatrixColumnCount() const = 0; + + /// Whether some of the generated data during solver calls should be cached. + mutable bool cachingEnabled; }; diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 666e68319..29a5a0699 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -18,7 +18,7 @@ namespace storm { namespace solver { template - MinMaxLinearEquationSolver::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false) { + MinMaxLinearEquationSolver::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), cachingEnabled(false) { // Intentionally left empty. } @@ -80,7 +80,21 @@ namespace storm { } template - void MinMaxLinearEquationSolver::resetAuxiliaryData() const { + void MinMaxLinearEquationSolver::setCachingEnabled(bool value) { + if(cachingEnabled && !value) { + // caching will be turned off. Hence we clear the cache at this point + clearCache(); + } + cachingEnabled = value; + } + + template + bool MinMaxLinearEquationSolver::isCachingEnabled() const { + return cachingEnabled; + } + + template + void MinMaxLinearEquationSolver::clearCache() const { // Intentionally left empty. } diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index f3b332f3c..039c32343 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -128,11 +128,22 @@ namespace storm { * Gets whether the precision is taken to be absolute or relative */ virtual bool getRelative() const = 0; + + /*! + * Sets whether some of the generated data during solver calls should be cached. + * This possibly decreases the runtime of subsequent calls but also increases memory consumption. + */ + void setCachingEnabled(bool value); + + /*! + * Retrieves whether some of the generated data during solver calls should be cached. + */ + bool isCachingEnabled() const; /* - * Clears auxiliary data that has possibly been stored during previous calls of the solver. + * Clears the currently cached data that has been stored during previous calls of the solver. */ - virtual void resetAuxiliaryData() const; + virtual void clearCache() const; protected: @@ -144,6 +155,11 @@ namespace storm { /// The scheduler (if it could be successfully generated). mutable boost::optional> scheduler; + + private: + /// Whether some of the generated data during solver calls should be cached. + bool cachingEnabled; + }; template diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 31fe74227..63d82eff5 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -97,21 +97,21 @@ namespace storm { void NativeLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& A) { localA.reset(); this->A = &A; - resetAuxiliaryData(); + clearCache(); } template void NativeLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& A) { localA = std::make_unique>(std::move(A)); this->A = localA.get(); - resetAuxiliaryData(); + clearCache(); } template bool NativeLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { - if(!this->auxiliaryRowVector) { - this->auxiliaryRowVector = std::make_unique>(getMatrixRowCount()); + if(!this->cachedRowVector) { + this->cachedRowVector = std::make_unique>(getMatrixRowCount()); } if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::SOR || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::GaussSeidel) { @@ -126,16 +126,20 @@ namespace storm { A->performSuccessiveOverRelaxationStep(omega, x, b); // Now check if the process already converged within our precision. - converged = storm::utility::vector::equalModuloPrecision(*this->auxiliaryRowVector, x, static_cast(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)); + converged = storm::utility::vector::equalModuloPrecision(*this->cachedRowVector, x, static_cast(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)); // If we did not yet converge, we need to backup the contents of x. if (!converged) { - *this->auxiliaryRowVector = x; + *this->cachedRowVector = x; } // Increase iteration count so we can abort if convergence is too slow. ++iterationCount; } + + if(!this->isCachingEnabled()) { + clearCache(); + } return converged; @@ -148,7 +152,7 @@ namespace storm { std::vector const& jacobiD = jacobiDecomposition->second; std::vector* currentX = &x; - std::vector* nextX = this->auxiliaryRowVector.get(); + std::vector* nextX = this->cachedRowVector.get(); // Set up additional environment variables. uint_fast64_t iterationCount = 0; @@ -172,10 +176,14 @@ namespace storm { // If the last iteration did not write to the original x we have to swap the contents, because the // output has to be written to the input parameter x. - if (currentX == this->auxiliaryRowVector.get()) { + if (currentX == this->cachedRowVector.get()) { std::swap(x, *currentX); } + if(!this->isCachingEnabled()) { + clearCache(); + } + return iterationCount < this->getSettings().getMaximalNumberOfIterations(); } } @@ -189,14 +197,19 @@ namespace storm { } } else { // If the two vectors are aliases, we need to create a temporary. - if(!this->auxiliaryRowVector) { - this->auxiliaryRowVector = std::make_unique>(getMatrixRowCount()); + if(!this->cachedRowVector) { + this->cachedRowVector = std::make_unique>(getMatrixRowCount()); } - A->multiplyWithVector(x, *this->auxiliaryRowVector); + + A->multiplyWithVector(x, *this->cachedRowVector); if (b != nullptr) { - storm::utility::vector::addVectors(*this->auxiliaryRowVector, *b, result); + storm::utility::vector::addVectors(*this->cachedRowVector, *b, result); } else { - result.swap(*this->auxiliaryRowVector); + result.swap(*this->cachedRowVector); + } + + if(!this->isCachingEnabled()) { + clearCache(); } } } @@ -212,9 +225,9 @@ namespace storm { } template - void NativeLinearEquationSolver::resetAuxiliaryData() const { + void NativeLinearEquationSolver::clearCache() const { jacobiDecomposition.reset(); - LinearEquationSolver::resetAuxiliaryData(); + LinearEquationSolver::clearCache(); } template diff --git a/src/solver/NativeLinearEquationSolver.h b/src/solver/NativeLinearEquationSolver.h index df1b91a13..aeb0cc807 100644 --- a/src/solver/NativeLinearEquationSolver.h +++ b/src/solver/NativeLinearEquationSolver.h @@ -55,10 +55,7 @@ namespace storm { void setSettings(NativeLinearEquationSolverSettings const& newSettings); NativeLinearEquationSolverSettings const& getSettings() const; - /* - * Clears auxiliary data that has possibly been stored during previous calls of the solver. - */ - virtual void resetAuxiliaryData() const override; + virtual void clearCache() const override; private: virtual uint64_t getMatrixRowCount() const override; @@ -75,6 +72,7 @@ namespace storm { // The settings used by the solver. NativeLinearEquationSolverSettings settings; + // cached auxiliary data mutable std::unique_ptr, std::vector>> jacobiDecomposition; }; diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp index 637455a07..5162827f2 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/solver/StandardMinMaxLinearEquationSolver.cpp @@ -111,6 +111,7 @@ namespace storm { // Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration. auto solver = linearEquationSolverFactory->create(std::move(submatrix)); + solver->setCachingEnabled(true); Status status = Status::InProgress; uint64_t iterations = 0; @@ -170,6 +171,10 @@ namespace storm { this->scheduler = std::make_unique(std::move(scheduler)); } + if(!this->isCachingEnabled()) { + clearCache(); + } + if(status == Status::Converged || status == Status::TerminatedEarly) { return true; } else{ @@ -206,6 +211,7 @@ namespace storm { bool StandardMinMaxLinearEquationSolver::solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { if(!linEqSolverA) { linEqSolverA = linearEquationSolverFactory->create(A); + linEqSolverA->setCachingEnabled(true); } if (!auxiliaryRowVector.get()) { @@ -263,6 +269,10 @@ namespace storm { this->scheduler = std::make_unique(std::move(choices)); } + if(!this->isCachingEnabled()) { + clearCache(); + } + if(status == Status::Converged || status == Status::TerminatedEarly) { return true; } else{ @@ -274,6 +284,7 @@ namespace storm { void StandardMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n) const { if(!linEqSolverA) { linEqSolverA = linearEquationSolverFactory->create(A); + linEqSolverA->setCachingEnabled(true); } if (!auxiliaryRowVector.get()) { @@ -288,6 +299,10 @@ namespace storm { // element of the min/max operator stack. storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices()); } + + if(!this->isCachingEnabled()) { + clearCache(); + } } template @@ -324,11 +339,11 @@ namespace storm { } template - void StandardMinMaxLinearEquationSolver::resetAuxiliaryData() const { + void StandardMinMaxLinearEquationSolver::clearCache() const { linEqSolverA.reset(); auxiliaryRowVector.reset(); auxiliaryRowGroupVector.reset(); - MinMaxLinearEquationSolver::resetAuxiliaryData(); + MinMaxLinearEquationSolver::clearCache(); } template diff --git a/src/solver/StandardMinMaxLinearEquationSolver.h b/src/solver/StandardMinMaxLinearEquationSolver.h index 4cc381904..31be9c2ce 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/solver/StandardMinMaxLinearEquationSolver.h @@ -44,7 +44,7 @@ namespace storm { StandardMinMaxLinearEquationSolverSettings const& getSettings() const; void setSettings(StandardMinMaxLinearEquationSolverSettings const& newSettings); - virtual void resetAuxiliaryData() const override; + virtual void clearCache() const override; virtual ValueType getPrecision() const override; virtual bool getRelative() const override; @@ -58,6 +58,7 @@ namespace storm { Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress }; + // possibly cached data mutable std::unique_ptr> linEqSolverA; mutable std::unique_ptr> auxiliaryRowVector; // A.rowCount() entries mutable std::unique_ptr> auxiliaryRowGroupVector; // A.rowGroupCount() entries diff --git a/src/utility/policyguessing.cpp b/src/utility/policyguessing.cpp index 15335b36a..704b2b50c 100644 --- a/src/utility/policyguessing.cpp +++ b/src/utility/policyguessing.cpp @@ -68,6 +68,7 @@ namespace storm { solveLinearEquationSystem(inducedA, x, inducedB, probGreater0States, prob0Value, solver.getPrecision(), solver.getRelative()); solver.setTrackScheduler(); + solver.setCachingEnabled(true); bool resultCorrect = false; while(!resultCorrect){ solver.solveEquations(goal, x, b); @@ -171,6 +172,7 @@ namespace storm { storm::utility::vector::selectVectorValues(subB, probGreater0States, b); std::unique_ptr> linEqSysSolver(static_cast*>(storm::solver::GmmxxLinearEquationSolverFactory().create(eqSysA).release())); + linEqSysSolver->setCachingEnabled(true); auto eqSettings = linEqSysSolver->getSettings(); eqSettings.setRelativeTerminationCriterion(relative); eqSettings.setMaximalNumberOfIterations(500);