SymbolicLinearEquationSolver.h

Go to the documentation of this file.

#ifndef STORM_SOLVER_SYMBOLICLINEAREQUATIONSOLVER_H_
#define STORM_SOLVER_SYMBOLICLINEAREQUATIONSOLVER_H_
 
#include <set>
#include <vector>
 
#include "storm/storage/dd/DdManager.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/expressions/Variable.h"
 
#include "storm/solver/LinearEquationSolverProblemFormat.h"
#include "storm/solver/LinearEquationSolverRequirements.h"
#include "storm/solver/SymbolicEquationSolver.h"
 
#include "storm/adapters/RationalFunctionAdapter.h"
 
namespace storm {
 
class Environment;
 
namespace dd {
template<storm::dd::DdType Type, typename ValueType>
class Add;
 
template<storm::dd::DdType Type>
class Bdd;
}  // namespace dd
 
namespace solver {
 
template<storm::dd::DdType DdType, typename ValueType = double>
class SymbolicLinearEquationSolver : public SymbolicEquationSolver<DdType, ValueType> {
   public:
    SymbolicLinearEquationSolver();
    virtual ~SymbolicLinearEquationSolver() = default;
 
    SymbolicLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows,
                                 std::set<storm::expressions::Variable> const& rowMetaVariables,
                                 std::set<storm::expressions::Variable> const& columnMetaVariables,
                                 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
 
    SymbolicLinearEquationSolver(storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables,
                                 std::set<storm::expressions::Variable> const& columnMetaVariables,
                                 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
 
    virtual storm::dd::Add<DdType, ValueType> solveEquations(Environment const& env, storm::dd::Add<DdType, ValueType> const& x,
                                                             storm::dd::Add<DdType, ValueType> const& b) const = 0;
 
    virtual storm::dd::Add<DdType, ValueType> multiply(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b = nullptr,
                                                       uint_fast64_t n = 1) const;
 
    virtual LinearEquationSolverProblemFormat getEquationProblemFormat(Environment const& env) const;
 
    virtual LinearEquationSolverRequirements getRequirements(Environment const& env) const;
 
    void setMatrix(storm::dd::Add<DdType, ValueType> const& newA);
    virtual void setData(storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables,
                         std::set<storm::expressions::Variable> const& columnMetaVariables,
                         std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
 
   protected:
    // The matrix defining the coefficients of the linear equation system.
    storm::dd::Add<DdType, ValueType> A;
 
    // The row variables.
    std::set<storm::expressions::Variable> rowMetaVariables;
 
    // The column variables.
    std::set<storm::expressions::Variable> columnMetaVariables;
 
    // The pairs of meta variables used for renaming.
    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
};
 
template<storm::dd::DdType DdType, typename ValueType>
class SymbolicLinearEquationSolverFactory {
   public:
    virtual ~SymbolicLinearEquationSolverFactory() = default;
 
    std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(
        Environment const& env, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables,
        std::set<storm::expressions::Variable> const& columnMetaVariables,
        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const;
 
    std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(
        Environment const& env, storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows,
        std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables,
        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const;
 
    LinearEquationSolverProblemFormat getEquationProblemFormat(Environment const& env) const;
    LinearEquationSolverRequirements getRequirements(Environment const& env) const;
 
    virtual std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(Environment const& env) const = 0;
};
 
template<storm::dd::DdType DdType, typename ValueType>
class GeneralSymbolicLinearEquationSolverFactory : public SymbolicLinearEquationSolverFactory<DdType, ValueType> {
   public:
    using SymbolicLinearEquationSolverFactory<DdType, ValueType>::create;
 
    virtual std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(Environment const& env) const override;
};
 
}  // namespace solver
}  // namespace storm
 
#endif /* STORM_SOLVER_SYMBOLICLINEAREQUATIONSOLVER_H_ */