An interface that represents an abstract symbolic linear equation solver. More...

#include <SymbolicLinearEquationSolver.h>

Inheritance diagram for storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >:

[legend]

Collaboration diagram for storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >:

[legend]

Public Member Functions
	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)
	Constructs a symbolic linear equation solver with the given meta variable sets and pairs.

	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)
	Constructs a symbolic linear equation solver with the given meta variable sets and pairs.

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
	Solves the equation system A*x = b.

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
	Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b.

virtual LinearEquationSolverProblemFormat	getEquationProblemFormat (Environment const &env) const
	Retrieves the format in which this solver expects to solve equations.

virtual LinearEquationSolverRequirements	getRequirements (Environment const &env) const
	Retrieves the requirements of the solver under the current settings.

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)

Public Member Functions inherited from storm::solver::SymbolicEquationSolver< DdType, ValueType >
	SymbolicEquationSolver ()=default

	SymbolicEquationSolver (storm::dd::Bdd< DdType > const &allRows)

virtual	~SymbolicEquationSolver ()=default

virtual void	setLowerBounds (storm::dd::Add< DdType, ValueType > const &lowerBounds)

virtual void	setLowerBound (ValueType const &lowerBound)

virtual void	setUpperBounds (storm::dd::Add< DdType, ValueType > const &upperBounds)

virtual void	setUpperBound (ValueType const &lowerBound)

virtual void	setBounds (ValueType const &lowerBound, ValueType const &upperBound)

virtual void	setBounds (storm::dd::Add< DdType, ValueType > const &lowerBounds, storm::dd::Add< DdType, ValueType > const &upperBounds)

bool	hasLowerBound () const

ValueType const &	getLowerBound () const

bool	hasLowerBounds () const

storm::dd::Add< DdType, ValueType > const &	getLowerBounds () const

bool	hasUpperBound () const

ValueType const &	getUpperBound () const

bool	hasUpperBounds () const

storm::dd::Add< DdType, ValueType > const &	getUpperBounds () const

storm::dd::Add< DdType, ValueType >	getLowerBoundsVector () const
	Retrieves a vector of lower bounds for all values (if any lower bounds are known).

storm::dd::Add< DdType, ValueType >	getUpperBoundsVector () const
	Retrieves a vector of upper bounds for all values (if any lower bounds are known).

Protected Attributes
storm::dd::Add< DdType, ValueType >	A

std::set< storm::expressions::Variable >	rowMetaVariables

std::set< storm::expressions::Variable >	columnMetaVariables

std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > >	rowColumnMetaVariablePairs

Protected Attributes inherited from storm::solver::SymbolicEquationSolver< DdType, ValueType >
storm::dd::Bdd< DdType >	allRows

Additional Inherited Members
Protected Member Functions inherited from storm::solver::SymbolicEquationSolver< DdType, ValueType >
storm::dd::DdManager< DdType > &	getDdManager () const

void	setAllRows (storm::dd::Bdd< DdType > const &allRows)

storm::dd::Bdd< DdType > const &	getAllRows () const

Detailed Description

template<storm::dd::DdType DdType, typename ValueType = double>
class storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >

An interface that represents an abstract symbolic linear equation solver.

In addition to solving a system of linear equations, the functionality to repeatedly multiply a matrix with a given vector is provided.

Definition at line 36 of file SymbolicLinearEquationSolver.h.

Constructor & Destructor Documentation

◆ SymbolicLinearEquationSolver() [1/3]

template<storm::dd::DdType DdType, typename ValueType >

storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >::SymbolicLinearEquationSolver ( )

Definition at line 24 of file SymbolicLinearEquationSolver.cpp.

◆ ~SymbolicLinearEquationSolver()

template<storm::dd::DdType DdType, typename ValueType = double>

virtual storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >::~SymbolicLinearEquationSolver ( )

virtualdefault

◆ SymbolicLinearEquationSolver() [2/3]

template<storm::dd::DdType DdType, typename ValueType >

storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >::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
	)

Constructs a symbolic linear equation solver with the given meta variable sets and pairs.

Parameters

A	The matrix defining the coefficients of the linear equation system.
diagonal	An ADD characterizing the elements on the diagonal of the matrix.
allRows	A BDD characterizing all rows of the equation system.
rowMetaVariables	The meta variables used to encode the rows of the matrix.
columnMetaVariables	The meta variables used to encode the columns of the matrix.
rowColumnMetaVariablePairs	The pairs of row meta variables and the corresponding column meta variables.

Definition at line 29 of file SymbolicLinearEquationSolver.cpp.

◆ SymbolicLinearEquationSolver() [3/3]

template<storm::dd::DdType DdType, typename ValueType >

storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >::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
	)

Constructs a symbolic linear equation solver with the given meta variable sets and pairs.

Note that in this version, the coefficient matrix has to be set manually afterwards.

Parameters

diagonal	An ADD characterizing the elements on the diagonal of the matrix.
allRows	A BDD characterizing all rows of the equation system.
rowMetaVariables	The meta variables used to encode the rows of the matrix.
columnMetaVariables	The meta variables used to encode the columns of the matrix.
rowColumnMetaVariablePairs	The pairs of row meta variables and the corresponding column meta variables.

Definition at line 38 of file SymbolicLinearEquationSolver.cpp.

Member Function Documentation

◆ getEquationProblemFormat()

template<storm::dd::DdType DdType, typename ValueType >

LinearEquationSolverProblemFormat storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >::getEquationProblemFormat ( Environment const & env ) const

virtual

Retrieves the format in which this solver expects to solve equations.

If the solver expects the equation system format, it solves Ax = b. If it it expects a fixed point format, it solves Ax + b = x.

Reimplemented in storm::solver::SymbolicEliminationLinearEquationSolver< DdType, ValueType >, and storm::solver::SymbolicNativeLinearEquationSolver< DdType, ValueType >.

Definition at line 67 of file SymbolicLinearEquationSolver.cpp.

◆ getRequirements()

template<storm::dd::DdType DdType, typename ValueType >

LinearEquationSolverRequirements storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >::getRequirements ( Environment const & env ) const

virtual

Retrieves the requirements of the solver under the current settings.

Note that these requirements only apply to solving linear equations and not to the matrix vector multiplications.

Reimplemented in storm::solver::SymbolicNativeLinearEquationSolver< DdType, ValueType >.

Definition at line 72 of file SymbolicLinearEquationSolver.cpp.

◆ multiply()

template<storm::dd::DdType DdType, typename ValueType >

storm::dd::Add< DdType, ValueType > storm::solver::SymbolicLinearEquationSolver< 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

Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b.

After performing the necessary multiplications, the result is written to the input vector x. Note that the matrix A has to be given upon construction time of the solver object.

Parameters

x	The initial vector with which to perform matrix-vector multiplication. Its length must be equal to the number of rows of A.
b	If non-null, this vector is added after each multiplication. If given, its length must be equal to the number of rows of A.

Returns: The solution of the equation system.

Definition at line 50 of file SymbolicLinearEquationSolver.cpp.

◆ setData()

template<storm::dd::DdType DdType, typename ValueType >

void storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >::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
	)

virtual

Reimplemented in storm::solver::SymbolicEliminationLinearEquationSolver< DdType, ValueType >.

Definition at line 83 of file SymbolicLinearEquationSolver.cpp.

◆ setMatrix()

template<storm::dd::DdType DdType, typename ValueType >

void storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >::setMatrix ( storm::dd::Add< DdType, ValueType > const & newA )

Definition at line 78 of file SymbolicLinearEquationSolver.cpp.

◆ solveEquations()

template<storm::dd::DdType DdType, typename ValueType = double>

virtual storm::dd::Add< DdType, ValueType > storm::solver::SymbolicLinearEquationSolver< DdType, ValueType >::solveEquations	(	Environment const &	env,
		storm::dd::Add< DdType, ValueType > const &	x,
		storm::dd::Add< DdType, ValueType > const &	b
	)		const

pure virtual

Solves the equation system A*x = b.

The matrix A is required to be square and have a unique solution. The solution of the set of linear equations will be written to the vector x. Note that the matrix A has to be given upon construction time of the solver object.

Parameters

x	The initial guess for the solution vector. Its length must be equal to the number of rows of A.
b	The right-hand side of the equation system. Its length must be equal to the number of rows of A.