storm::solver Namespace Reference

Namespaces
namespace	detail
namespace	helper
namespace	stateelimination

Classes
class	AbstractEquationSolver
class	AcyclicLinearEquationSolver
	This solver can be used on equation systems that are known to be acyclic. More...
class	AcyclicMinMaxLinearEquationSolver
	This solver can be used on equation systems that are known to be acyclic. More...
class	EigenLinearEquationSolver
	A class that uses the Eigen library to implement the LinearEquationSolver interface. More...
class	EigenLinearEquationSolverFactory
class	EliminationLinearEquationSolver
	A class that uses gaussian elimination to implement the LinearEquationSolver interface. More...
class	EliminationLinearEquationSolverFactory
class	GameSolver
	A class representing the interface that all game solvers shall implement. More...
class	GameSolverFactory
class	GeneralLinearEquationSolverFactory
class	GeneralMinMaxLinearEquationSolverFactory
class	GeneralSymbolicLinearEquationSolverFactory
class	GeneralSymbolicMinMaxLinearEquationSolverFactory
class	GlpkLpSolver
	A class that implements the LpSolver interface using glpk as the background solver. More...
class	GmmxxLinearEquationSolver
	A class that uses the gmm++ library to implement the LinearEquationSolver interface. More...
class	GmmxxLinearEquationSolverFactory
class	GurobiEnvironment
class	GurobiLpSolver
	A class that implements the LpSolver interface using Gurobi. More...
class	IterativeMinMaxLinearEquationSolver
class	LinearEquationSolver
	An interface that represents an abstract linear equation solver. More...
class	LinearEquationSolverFactory
class	LinearEquationSolverRequirements
class	LpMinMaxLinearEquationSolver
	Solves a MinMaxLinearEquationSystem using a linear programming solver. More...
class	LpSolver
	An interface that captures the functionality of an LP solver. More...
class	MathsatSmtSolver
class	MinMaxLinearEquationSolver
	A class representing the interface that all min-max linear equation solvers shall implement. More...
class	MinMaxLinearEquationSolverFactory
class	MinMaxLinearEquationSolverRequirements
class	Multiplier
class	MultiplierFactory
class	NativeLinearEquationSolver
	A class that uses storm's native matrix operations to implement the LinearEquationSolver interface. More...
class	NativeLinearEquationSolverFactory
class	NativeMultiplier
class	NoTerminationCondition
struct	RawLpConstraint
class	SmtlibSmtSolver
	This class represents an SMT-LIBv2 conforming solver. More...
class	SmtSolver
	An interface that captures the functionality of an SMT solver. More...
class	SolveGoal
class	SolverRequirement
class	SoplexLpSolver
class	StandardGameSolver
class	StandardMinMaxLinearEquationSolver
class	SymbolicEliminationLinearEquationSolver
class	SymbolicEliminationLinearEquationSolverFactory
class	SymbolicEquationSolver
class	SymbolicGameSolver
	An interface that represents an abstract symbolic game solver. More...
class	SymbolicGameSolverFactory
class	SymbolicLinearEquationSolver
	An interface that represents an abstract symbolic linear equation solver. More...
class	SymbolicLinearEquationSolverFactory
class	SymbolicMinMaxLinearEquationSolver
	An interface that represents an abstract symbolic linear equation solver. More...
class	SymbolicMinMaxLinearEquationSolverFactory
class	SymbolicNativeLinearEquationSolver
	An interface that represents an abstract symbolic linear equation solver. More...
class	SymbolicNativeLinearEquationSolverFactory
class	TerminateIfFilteredExtremumBelowThreshold
class	TerminateIfFilteredExtremumExceedsThreshold
class	TerminateIfFilteredSumExceedsThreshold
class	TerminationCondition
class	TopologicalLinearEquationSolver
class	TopologicalLinearEquationSolverFactory
class	TopologicalMinMaxLinearEquationSolver
class	ViOperatorMultiplier
class	Z3LpSolver
	A class that implements the LpSolver interface using Z3. More...
class	Z3SmtSolver

Enumerations
enum class	GurobiSolverMethod {   AUTOMATIC = -1 , PRIMALSIMPLEX = 0 , DUALSIMPLEX = 1 , BARRIER = 2 ,   CONCURRENT = 3 , DETCONCURRENT = 4 , DETCONCURRENTSIMPLEX = 5 }
enum class	LinearEquationSolverProblemFormat { EquationSystem , FixedPointSystem }
enum class	MultiplicationStyle { GaussSeidel , Regular }
enum class	OptimizationDirection { Minimize = 0 , Maximize = 1 }
enum class	OptimizationDirectionSetting { Minimize = 0 , Maximize = 1 , Unset }
enum class	SolverGuarantee { GreaterOrEqual , LessOrEqual , None }
enum class	SolverStatus {   Converged , TerminatedEarly , MaximalIterationsExceeded , InProgress ,   Aborted }

Functions
template<typename ValueType , bool RawMode>
int	getGlpkType (typename GlpkLpSolver< ValueType, RawMode >::VariableType const &type)
std::string	toString (GurobiSolverMethod const &method)
	Yields a string representation of the GurobiSolverMethod.
std::optional< GurobiSolverMethod >	gurobiSolverMethodFromString (std::string const &method)
std::vector< GurobiSolverMethod >	getGurobiSolverMethods ()
template<typename ValueType , typename SolutionType >
ValueType	computeMaxAbsDiff (std::vector< ValueType > const &allValues, storm::storage::BitVector const &relevantValues, std::vector< ValueType > const &oldValues)
template<typename ValueType , typename SolutionType >
ValueType	computeMaxAbsDiff (std::vector< ValueType > const &allOldValues, std::vector< ValueType > const &allNewValues, storm::storage::BitVector const &relevantValues)
template<typename ValueType , typename SolutionType >
void	preserveOldRelevantValues (std::vector< ValueType > const &allValues, storm::storage::BitVector const &relevantValues, std::vector< ValueType > &oldValues)
std::ostream &	operator<< (std::ostream &out, LinearEquationSolverProblemFormat const &format)
std::ostream &	operator<< (std::ostream &out, MultiplicationStyle const &style)
template<typename ValueType >
void	preserveOldRelevantValues (std::vector< ValueType > const &allValues, storm::storage::BitVector const &relevantValues, std::vector< ValueType > &oldValues)
template<typename ValueType >
ValueType	computeMaxAbsDiff (std::vector< ValueType > const &allValues, storm::storage::BitVector const &relevantValues, std::vector< ValueType > const &oldValues)
template<typename ValueType >
ValueType	computeMaxAbsDiff (std::vector< ValueType > const &allOldValues, std::vector< ValueType > const &allNewValues, storm::storage::BitVector const &relevantValues)
bool	isSet (OptimizationDirectionSetting s)
OptimizationDirection	convert (OptimizationDirectionSetting s)
OptimizationDirectionSetting	convert (OptimizationDirection d)
std::ostream &	operator<< (std::ostream &out, OptimizationDirection d)
bool constexpr	minimize (OptimizationDirection d)
bool constexpr	maximize (OptimizationDirection d)
OptimizationDirection constexpr	invert (OptimizationDirection d)
template<typename ValueType , typename MatrixType , typename SolutionType >
std::unique_ptr< storm::solver::MinMaxLinearEquationSolver< ValueType, SolutionType > >	configureMinMaxLinearEquationSolver (Environment const &env, SolveGoal< ValueType, SolutionType > &&goal, storm::solver::MinMaxLinearEquationSolverFactory< ValueType, SolutionType > const &factory, MatrixType &&matrix)
template<typename ValueType , typename MatrixType , typename SolutionType >
std::unique_ptr< storm::solver::LinearEquationSolver< ValueType > >	configureLinearEquationSolver (Environment const &env, SolveGoal< ValueType, SolutionType > &&goal, storm::solver::LinearEquationSolverFactory< ValueType > const &factory, MatrixType &&matrix)
template<typename MatrixType >
std::unique_ptr< storm::solver::LinearEquationSolver< storm::RationalFunction > >	configureLinearEquationSolver (Environment const &env, SolveGoal< storm::RationalFunction > &&, storm::solver::LinearEquationSolverFactory< storm::RationalFunction > const &factory, MatrixType &&matrix)
std::ostream &	operator<< (std::ostream &out, SolverGuarantee const &guarantee)
std::string	toString (MinMaxMethod m)
std::string	toString (MultiplierType t)
std::string	toString (GameMethod m)
std::string	toString (LraMethod m)
std::string	toString (MaBoundedReachabilityMethod m)
std::string	toString (LpSolverType t)
std::string	toString (EquationSolverType t)
std::string	toString (SmtSolverType t)
std::string	toString (NativeLinearEquationSolverMethod t)
std::string	toString (GmmxxLinearEquationSolverMethod t)
std::string	toString (GmmxxLinearEquationSolverPreconditioner t)
std::string	toString (EigenLinearEquationSolverMethod t)
std::string	toString (EigenLinearEquationSolverPreconditioner t)
	ExtendEnumsWithSelectionField (MinMaxMethod, ValueIteration, PolicyIteration, LinearProgramming, Topological, RationalSearch, IntervalIteration, SoundValueIteration, OptimisticValueIteration, GuessingValueIteration, ViToPi, ViToLp, Acyclic) ExtendEnumsWithSelectionField(MultiplierType
ViOperator	ExtendEnumsWithSelectionField (GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LraMethod
ViOperator LraDistributionEquations	ExtendEnumsWithSelectionField (MaBoundedReachabilityMethod, Imca, UnifPlus) ExtendEnumsWithSelectionField(LpSolverType
ViOperator LraDistributionEquations Soplex	ExtendEnumsWithSelectionField (EquationSolverType, Native, Gmmxx, Eigen, Elimination, Topological, Acyclic) ExtendEnumsWithSelectionField(SmtSolverType
ViOperator LraDistributionEquations Soplex Mathsat	ExtendEnumsWithSelectionField (NativeLinearEquationSolverMethod, Jacobi, GaussSeidel, SOR, WalkerChae, Power, SoundValueIteration, OptimisticValueIteration, GuessingValueIteration, IntervalIteration, RationalSearch) ExtendEnumsWithSelectionField(GmmxxLinearEquationSolverMethod
ViOperator LraDistributionEquations Soplex Mathsat Gmres	ExtendEnumsWithSelectionField (GmmxxLinearEquationSolverPreconditioner, Ilu, Diagonal, None) ExtendEnumsWithSelectionField(EigenLinearEquationSolverMethod
std::ostream &	operator<< (std::ostream &out, SolverStatus const &status)

Variables
	Native
ViOperator	LinearProgramming
ViOperator	ValueIteration
ViOperator	GainBiasEquations
ViOperator LraDistributionEquations	Gurobi
ViOperator LraDistributionEquations	Glpk
ViOperator LraDistributionEquations	Z3
ViOperator LraDistributionEquations Soplex Mathsat	Bicgstab
ViOperator LraDistributionEquations Soplex Mathsat	Qmr
ViOperator LraDistributionEquations Soplex Mathsat Gmres	SparseLU
ViOperator LraDistributionEquations Soplex Mathsat Gmres	DGmres

Enumeration Type Documentation

GurobiSolverMethod

enum class storm::solver::GurobiSolverMethod

strong

Enumerator
AUTOMATIC
PRIMALSIMPLEX
DUALSIMPLEX
BARRIER
CONCURRENT
DETCONCURRENT
DETCONCURRENTSIMPLEX

Definition at line 169 of file GurobiLpSolver.h.

LinearEquationSolverProblemFormat

enum class storm::solver::LinearEquationSolverProblemFormat

strong

Enumerator
EquationSystem
FixedPointSystem

Definition at line 8 of file LinearEquationSolverProblemFormat.h.

MultiplicationStyle

enum class storm::solver::MultiplicationStyle

strong

Enumerator
GaussSeidel
Regular

Definition at line 8 of file MultiplicationStyle.h.

OptimizationDirection

enum class storm::solver::OptimizationDirection

strong

Enumerator
Minimize
Maximize

Definition at line 8 of file OptimizationDirection.h.

OptimizationDirectionSetting

enum class storm::solver::OptimizationDirectionSetting

strong

Enumerator
Minimize
Maximize
Unset

Definition at line 23 of file OptimizationDirection.h.

SolverGuarantee

enum class storm::solver::SolverGuarantee

strong

Enumerator
GreaterOrEqual
LessOrEqual
None

Definition at line 12 of file SolverGuarantee.h.

SolverStatus

enum class storm::solver::SolverStatus

strong

Enumerator
Converged
TerminatedEarly
MaximalIterationsExceeded
InProgress
Aborted

Definition at line 8 of file SolverStatus.h.

Function Documentation

computeMaxAbsDiff() [1/4]

template<typename ValueType , typename SolutionType >

ValueType storm::solver::computeMaxAbsDiff	(	std::vector< ValueType > const &	allOldValues,
		std::vector< ValueType > const &	allNewValues,
		storm::storage::BitVector const &	relevantValues
	)

Definition at line 544 of file IterativeMinMaxLinearEquationSolver.cpp.

computeMaxAbsDiff() [2/4]

template<typename ValueType >

ValueType storm::solver::computeMaxAbsDiff	(	std::vector< ValueType > const &	allOldValues,
		std::vector< ValueType > const &	allNewValues,
		storm::storage::BitVector const &	relevantValues
	)

Definition at line 413 of file NativeLinearEquationSolver.cpp.

computeMaxAbsDiff() [3/4]

template<typename ValueType , typename SolutionType >

ValueType storm::solver::computeMaxAbsDiff	(	std::vector< ValueType > const &	allValues,
		storm::storage::BitVector const &	relevantValues,
		std::vector< ValueType > const &	oldValues
	)

Definition at line 533 of file IterativeMinMaxLinearEquationSolver.cpp.

computeMaxAbsDiff() [4/4]

template<typename ValueType >

ValueType storm::solver::computeMaxAbsDiff	(	std::vector< ValueType > const &	allValues,
		storm::storage::BitVector const &	relevantValues,
		std::vector< ValueType > const &	oldValues
	)

Definition at line 403 of file NativeLinearEquationSolver.cpp.

configureLinearEquationSolver() [1/2]

template<typename MatrixType >

std::unique_ptr< storm::solver::LinearEquationSolver< storm::RationalFunction > > storm::solver::configureLinearEquationSolver	(	Environment const &	env,
		SolveGoal< storm::RationalFunction > &&	,
		storm::solver::LinearEquationSolverFactory< storm::RationalFunction > const &	factory,
		MatrixType &&	matrix
	)

Definition at line 140 of file SolveGoal.h.

configureLinearEquationSolver() [2/2]

template<typename ValueType , typename MatrixType , typename SolutionType >

std::unique_ptr< storm::solver::LinearEquationSolver< ValueType > > storm::solver::configureLinearEquationSolver	(	Environment const &	env,
		SolveGoal< ValueType, SolutionType > &&	goal,
		storm::solver::LinearEquationSolverFactory< ValueType > const &	factory,
		MatrixType &&	matrix
	)

Definition at line 128 of file SolveGoal.h.

configureMinMaxLinearEquationSolver()

template<typename ValueType , typename MatrixType , typename SolutionType >

std::unique_ptr< storm::solver::MinMaxLinearEquationSolver< ValueType, SolutionType > > storm::solver::configureMinMaxLinearEquationSolver	(	Environment const &	env,
		SolveGoal< ValueType, SolutionType > &&	goal,
		storm::solver::MinMaxLinearEquationSolverFactory< ValueType, SolutionType > const &	factory,
		MatrixType &&	matrix
	)

Definition at line 107 of file SolveGoal.h.

convert() [1/2]

OptimizationDirectionSetting storm::solver::convert

(

OptimizationDirection

d

)

Definition at line 17 of file OptimizationDirection.cpp.

convert() [2/2]

OptimizationDirection storm::solver::convert

(

OptimizationDirectionSetting

s

)

Definition at line 12 of file OptimizationDirection.cpp.

ExtendEnumsWithSelectionField() [1/6]

ViOperator LraDistributionEquations Soplex storm::solver::ExtendEnumsWithSelectionField	(	EquationSolverType	,
		Native	,
		Gmmxx	,
		Eigen	,
		Elimination	,
		Topological	,
		Acyclic
	)

ExtendEnumsWithSelectionField() [2/6]

ViOperator storm::solver::ExtendEnumsWithSelectionField	(	GameMethod	,
		PolicyIteration	,
		ValueIteration
	)

ExtendEnumsWithSelectionField() [3/6]

ViOperator LraDistributionEquations Soplex Mathsat Gmres storm::solver::ExtendEnumsWithSelectionField	(	GmmxxLinearEquationSolverPreconditioner	,
		Ilu	,
		Diagonal	,
		None
	)

ExtendEnumsWithSelectionField() [4/6]

ViOperator LraDistributionEquations storm::solver::ExtendEnumsWithSelectionField	(	MaBoundedReachabilityMethod	,
		Imca	,
		UnifPlus
	)

ExtendEnumsWithSelectionField() [5/6]

storm::solver::ExtendEnumsWithSelectionField	(	MinMaxMethod	,
		ValueIteration	,
		PolicyIteration	,
		LinearProgramming	,
		Topological	,
		RationalSearch	,
		IntervalIteration	,
		SoundValueIteration	,
		OptimisticValueIteration	,
		GuessingValueIteration	,
		ViToPi	,
		ViToLp	,
		Acyclic
	)

ExtendEnumsWithSelectionField() [6/6]

ViOperator LraDistributionEquations Soplex Mathsat storm::solver::ExtendEnumsWithSelectionField	(	NativeLinearEquationSolverMethod	,
		Jacobi	,
		GaussSeidel	,
		SOR	,
		WalkerChae	,
		Power	,
		SoundValueIteration	,
		OptimisticValueIteration	,
		GuessingValueIteration	,
		IntervalIteration	,
		RationalSearch
	)

getGlpkType()

template<typename ValueType , bool RawMode>

int storm::solver::getGlpkType

(

typename GlpkLpSolver< ValueType, RawMode >::VariableType const &

type

)

Definition at line 91 of file GlpkLpSolver.cpp.

getGurobiSolverMethods()

std::vector< GurobiSolverMethod > storm::solver::getGurobiSolverMethods

(

)

Definition at line 987 of file GurobiLpSolver.cpp.

gurobiSolverMethodFromString()

std::optional< GurobiSolverMethod > storm::solver::gurobiSolverMethodFromString

(

std::string const &

method

)

Definition at line 978 of file GurobiLpSolver.cpp.

invert()

OptimizationDirection constexpr storm::solver::invert ( OptimizationDirection  d )

constexpr

Definition at line 18 of file OptimizationDirection.h.

isSet()

bool storm::solver::isSet

(

OptimizationDirectionSetting

s

)

Definition at line 8 of file OptimizationDirection.cpp.

maximize()

bool constexpr storm::solver::maximize ( OptimizationDirection  d )

constexpr

Definition at line 14 of file OptimizationDirection.h.

minimize()

bool constexpr storm::solver::minimize ( OptimizationDirection  d )

constexpr

Definition at line 10 of file OptimizationDirection.h.

operator<<() [1/5]

std::ostream & storm::solver::operator<<	(	std::ostream &	out,
		LinearEquationSolverProblemFormat const &	format
	)

Definition at line 6 of file LinearEquationSolverProblemFormat.cpp.

operator<<() [2/5]

std::ostream & storm::solver::operator<<	(	std::ostream &	out,
		MultiplicationStyle const &	style
	)

Definition at line 6 of file MultiplicationStyle.cpp.

operator<<() [3/5]

std::ostream & storm::solver::operator<<	(	std::ostream &	out,
		OptimizationDirection	d
	)

Definition at line 21 of file OptimizationDirection.cpp.

operator<<() [4/5]

std::ostream & storm::solver::operator<<	(	std::ostream &	out,
		SolverGuarantee const &	guarantee
	)

Definition at line 6 of file SolverGuarantee.cpp.

operator<<() [5/5]

std::ostream & storm::solver::operator<<	(	std::ostream &	out,
		SolverStatus const &	status
	)

Definition at line 6 of file SolverStatus.cpp.

preserveOldRelevantValues() [1/2]

template<typename ValueType , typename SolutionType >

void storm::solver::preserveOldRelevantValues	(	std::vector< ValueType > const &	allValues,
		storm::storage::BitVector const &	relevantValues,
		std::vector< ValueType > &	oldValues
	)

Definition at line 762 of file IterativeMinMaxLinearEquationSolver.cpp.

preserveOldRelevantValues() [2/2]

template<typename ValueType >

void storm::solver::preserveOldRelevantValues	(	std::vector< ValueType > const &	allValues,
		storm::storage::BitVector const &	relevantValues,
		std::vector< ValueType > &	oldValues
	)

Definition at line 398 of file NativeLinearEquationSolver.cpp.

toString() [1/14]

std::string storm::solver::toString

(

EigenLinearEquationSolverMethod

t

)

Definition at line 171 of file SolverSelectionOptions.cpp.

toString() [2/14]

std::string storm::solver::toString

(

EigenLinearEquationSolverPreconditioner

t

)

Definition at line 185 of file SolverSelectionOptions.cpp.

toString() [3/14]

std::string storm::solver::toString

(

EquationSolverType

t

)

Definition at line 93 of file SolverSelectionOptions.cpp.

toString() [4/14]

std::string storm::solver::toString

(

GameMethod

m

)

Definition at line 45 of file SolverSelectionOptions.cpp.

toString() [5/14]

std::string storm::solver::toString

(

GmmxxLinearEquationSolverMethod

t

)

Definition at line 147 of file SolverSelectionOptions.cpp.

toString() [6/14]

std::string storm::solver::toString

(

GmmxxLinearEquationSolverPreconditioner

t

)

Definition at line 159 of file SolverSelectionOptions.cpp.

toString() [7/14]

std::string storm::solver::toString

(

GurobiSolverMethod const &

method

)

Yields a string representation of the GurobiSolverMethod.

Parameters

method

Returns

Definition at line 958 of file GurobiLpSolver.cpp.

toString() [8/14]

std::string storm::solver::toString

(

LpSolverType

t

)

Definition at line 79 of file SolverSelectionOptions.cpp.

toString() [9/14]

std::string storm::solver::toString

(

LraMethod

m

)

Definition at line 55 of file SolverSelectionOptions.cpp.

toString() [10/14]

std::string storm::solver::toString

(

MaBoundedReachabilityMethod

m

)

Definition at line 69 of file SolverSelectionOptions.cpp.

toString() [11/14]

std::string storm::solver::toString

(

MinMaxMethod

m

)

Definition at line 5 of file SolverSelectionOptions.cpp.

toString() [12/14]

std::string storm::solver::toString

(

MultiplierType

t

)

Definition at line 35 of file SolverSelectionOptions.cpp.

toString() [13/14]

std::string storm::solver::toString

(

NativeLinearEquationSolverMethod

t

)

Definition at line 121 of file SolverSelectionOptions.cpp.

toString() [14/14]

std::string storm::solver::toString

(

SmtSolverType

t

)

Definition at line 111 of file SolverSelectionOptions.cpp.

Variable Documentation

Bicgstab

ViOperator LraDistributionEquations Soplex Mathsat Gmres storm::solver::Bicgstab

Definition at line 20 of file SolverSelectionOptions.h.

DGmres

ViOperator LraDistributionEquations Soplex Mathsat Gmres storm::solver::DGmres

Definition at line 22 of file SolverSelectionOptions.h.

GainBiasEquations

ViOperator storm::solver::GainBiasEquations

Definition at line 11 of file SolverSelectionOptions.h.

Glpk

ViOperator LraDistributionEquations storm::solver::Glpk

Definition at line 14 of file SolverSelectionOptions.h.

Gurobi

ViOperator LraDistributionEquations storm::solver::Gurobi

Definition at line 14 of file SolverSelectionOptions.h.

LinearProgramming

ViOperator storm::solver::LinearProgramming

Definition at line 11 of file SolverSelectionOptions.h.

Native

storm::solver::Native

Definition at line 10 of file SolverSelectionOptions.h.

Qmr

ViOperator LraDistributionEquations Soplex Mathsat storm::solver::Qmr

Definition at line 20 of file SolverSelectionOptions.h.

SparseLU

ViOperator LraDistributionEquations Soplex Mathsat Gmres storm::solver::SparseLU

Definition at line 22 of file SolverSelectionOptions.h.

ValueIteration

ViOperator storm::solver::ValueIteration

Definition at line 11 of file SolverSelectionOptions.h.

Z3

ViOperator LraDistributionEquations Soplex storm::solver::Z3

Definition at line 14 of file SolverSelectionOptions.h.