TopologicalLinearEquationSolver.h

Go to the documentation of this file.

#pragma once
 
#include "storm/solver/LinearEquationSolver.h"
 
#include "storm/solver/SolverSelectionOptions.h"
#include "storm/solver/multiplier/NativeMultiplier.h"
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
#include "storm/storage/SubmatrixBuilder.h"
 
namespace storm {
 
class Environment;
 
namespace solver {
 
template<typename ValueType>
class TopologicalLinearEquationSolver : public LinearEquationSolver<ValueType> {
   public:
    TopologicalLinearEquationSolver();
    TopologicalLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A);
    TopologicalLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A);
 
    virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& A) override;
    virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& A) override;
 
    virtual LinearEquationSolverProblemFormat getEquationProblemFormat(storm::Environment const& env) const override;
    virtual LinearEquationSolverRequirements getRequirements(Environment const& env) const override;
 
    virtual void clearCache() const override;
 
   protected:
    virtual bool internalSolveEquations(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
 
   private:
    virtual uint64_t getMatrixRowCount() const override;
    virtual uint64_t getMatrixColumnCount() const override;
 
    storm::Environment getEnvironmentForUnderlyingSolver(storm::Environment const& env, bool adaptPrecision = false) const;
 
    // Creates an SCC decomposition and sorts the SCCs according to a topological sort.
    void createSortedSccDecomposition(bool needLongestChainSize) const;
 
    // Reports what the SCC-wise solve established about the solution: the values themselves if every SCC was
    // solved exactly, otherwise the precision they were solved with, if every SCC was solved that accurately.
    void trySetSolutionBounds(Environment const& env, std::vector<ValueType> const& x, bool allSccsExact, bool allSccsPrecise) const;
 
    // Retrieves whether the SCC solver met the precision the given environment asked of it for the given values it
    // just produced. Adding up the errors of the SCCs relies on that.
    bool lastSccMetPrecision(Environment const& sccSolverEnvironment, std::vector<ValueType> const& sccValues) const;
 
    // Solves the SCC with the given index
    // ... for the case that the SCC is trivial
    bool solveTrivialScc(uint64_t const& sccState, std::vector<ValueType>& globalX, std::vector<ValueType> const& globalB) const;
    // ... for the case that there is just one large SCC
    bool solveFullyConnectedEquationSystem(storm::Environment const& sccSolverEnvironment, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
    // ... for the remaining cases (1 < scc.size() < x.size())
    bool solveScc(storm::Environment const& sccSolverEnvironment, storm::storage::StronglyConnectedComponent const& scc,
                  storm::storage::BitVector const& sccAsBitVector, std::vector<ValueType>& globalX, std::vector<ValueType> const& globalB,
                  std::optional<storm::storage::BitVector> const& globalRelevantValues, bool& metPrecision) 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<storm::storage::SparseMatrix<ValueType>> 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<ValueType> const* A;
 
    // cached auxiliary data
    mutable std::unique_ptr<storm::storage::StronglyConnectedComponentDecomposition<ValueType>> sortedSccDecomposition;
    mutable boost::optional<uint64_t> longestSccChainSize;
    mutable std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> sccSolver;
    // Builds the submatrices of all SCCs (reuses its internal lookup table between SCCs)
    mutable std::unique_ptr<storm::storage::SubmatrixBuilder<ValueType>> sccSubmatrixBuilder;
};
 
template<typename ValueType>
class TopologicalLinearEquationSolverFactory : public LinearEquationSolverFactory<ValueType> {
   public:
    using LinearEquationSolverFactory<ValueType>::create;
 
    virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(Environment const& env) const override;
 
    virtual std::unique_ptr<LinearEquationSolverFactory<ValueType>> clone() const override;
};
}  // namespace solver
}  // namespace storm