SymbolicNativeLinearEquationSolver.h

Go to the documentation of this file.

#pragma once
 
#include "storm/solver/SolverSelectionOptions.h"
#include "storm/solver/SolverStatus.h"
#include "storm/solver/SymbolicLinearEquationSolver.h"
 
#include "storm/utility/NumberTraits.h"
 
namespace storm {
namespace solver {
 
template<storm::dd::DdType DdType, typename ValueType = double>
class SymbolicNativeLinearEquationSolver : public SymbolicLinearEquationSolver<DdType, ValueType> {
   public:
    SymbolicNativeLinearEquationSolver();
 
    SymbolicNativeLinearEquationSolver(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);
 
    SymbolicNativeLinearEquationSolver(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 override;
 
    virtual LinearEquationSolverProblemFormat getEquationProblemFormat(Environment const& env) const override;
    virtual LinearEquationSolverRequirements getRequirements(Environment const& env) const override;
 
   private:
    NativeLinearEquationSolverMethod getMethod(Environment const& env, bool isExactMode) const;
 
    storm::dd::Add<DdType, ValueType> solveEquationsJacobi(Environment const& env, storm::dd::Add<DdType, ValueType> const& x,
                                                           storm::dd::Add<DdType, ValueType> const& b) const;
    storm::dd::Add<DdType, ValueType> solveEquationsPower(Environment const& env, storm::dd::Add<DdType, ValueType> const& x,
                                                          storm::dd::Add<DdType, ValueType> const& b) const;
    storm::dd::Add<DdType, ValueType> solveEquationsRationalSearch(Environment const& env, storm::dd::Add<DdType, ValueType> const& x,
                                                                   storm::dd::Add<DdType, ValueType> const& b) const;
 
    bool isSolutionFixedPoint(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
 
    template<typename RationalType, typename ImpreciseType>
    static storm::dd::Add<DdType, RationalType> sharpen(uint64_t precision, SymbolicNativeLinearEquationSolver<DdType, RationalType> const& rationalSolver,
                                                        storm::dd::Add<DdType, ImpreciseType> const& x, storm::dd::Add<DdType, RationalType> const& rationalB,
                                                        bool& isSolution);
 
    template<typename RationalType, typename ImpreciseType>
    storm::dd::Add<DdType, RationalType> solveEquationsRationalSearchHelper(Environment const& env,
                                                                            SymbolicNativeLinearEquationSolver<DdType, RationalType> const& rationalSolver,
                                                                            SymbolicNativeLinearEquationSolver<DdType, ImpreciseType> const& impreciseSolver,
                                                                            storm::dd::Add<DdType, RationalType> const& rationalB,
                                                                            storm::dd::Add<DdType, ImpreciseType> const& x,
                                                                            storm::dd::Add<DdType, ImpreciseType> const& b) const;
    template<typename ImpreciseType>
    typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type
    solveEquationsRationalSearchHelper(Environment const& env, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
    template<typename ImpreciseType>
    typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && !storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type
    solveEquationsRationalSearchHelper(Environment const& env, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
    template<typename ImpreciseType>
    typename std::enable_if<!std::is_same<ValueType, ImpreciseType>::value, storm::dd::Add<DdType, ValueType>>::type solveEquationsRationalSearchHelper(
        Environment const& env, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
 
    template<storm::dd::DdType DdTypePrime, typename ValueTypePrime>
    friend class SymbolicNativeLinearEquationSolver;
 
    struct PowerIterationResult {
        PowerIterationResult(SolverStatus status, uint64_t iterations, storm::dd::Add<DdType, ValueType> const& values)
            : status(status), iterations(iterations), values(values) {
            // Intentionally left empty.
        }
 
        SolverStatus status;
        uint64_t iterations;
        storm::dd::Add<DdType, ValueType> values;
    };
 
    PowerIterationResult performPowerIteration(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b,
                                               ValueType const& precision, bool relativeTerminationCriterion, uint64_t maximalIterations) const;
};
 
template<storm::dd::DdType DdType, typename ValueType>
class SymbolicNativeLinearEquationSolverFactory : 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