storm::solver Namespace Reference

Namespaces
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
class	GmmxxLinearEquationSolver
	A class that uses the gmm++ library to implement the LinearEquationSolver interface. More...
class	GmmxxLinearEquationSolverFactory
class	GmmxxMultiplier
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	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
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, ViToPi, ViToLp, Acyclic) ExtendEnumsWithSelectionField(MultiplierType
Gmmxx	ExtendEnumsWithSelectionField (GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LraMethod
Gmmxx LraDistributionEquations	ExtendEnumsWithSelectionField (MaBoundedReachabilityMethod, Imca, UnifPlus) ExtendEnumsWithSelectionField(LpSolverType
Gmmxx LraDistributionEquations Soplex	ExtendEnumsWithSelectionField (EquationSolverType, Native, Gmmxx, Eigen, Elimination, Topological, Acyclic) ExtendEnumsWithSelectionField(SmtSolverType
Gmmxx LraDistributionEquations Soplex Mathsat	ExtendEnumsWithSelectionField (NativeLinearEquationSolverMethod, Jacobi, GaussSeidel, SOR, WalkerChae, Power, SoundValueIteration, OptimisticValueIteration, IntervalIteration, RationalSearch) ExtendEnumsWithSelectionField(GmmxxLinearEquationSolverMethod
Gmmxx LraDistributionEquations Soplex Mathsat Gmres	ExtendEnumsWithSelectionField (GmmxxLinearEquationSolverPreconditioner, Ilu, Diagonal, None) ExtendEnumsWithSelectionField(EigenLinearEquationSolverMethod
std::ostream &	operator<< (std::ostream &out, SolverStatus const &status)

Variables
	Native
Gmmxx	LinearProgramming
Gmmxx	ValueIteration
Gmmxx	GainBiasEquations
Gmmxx LraDistributionEquations	Gurobi
Gmmxx LraDistributionEquations	Glpk
Gmmxx LraDistributionEquations	Z3
Gmmxx LraDistributionEquations Soplex Mathsat	Bicgstab
Gmmxx LraDistributionEquations Soplex Mathsat	Qmr
Gmmxx LraDistributionEquations Soplex Mathsat Gmres	SparseLU
Gmmxx 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 158 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 411 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 412 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 400 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 402 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]

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

ExtendEnumsWithSelectionField() [2/6]

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

ExtendEnumsWithSelectionField() [3/6]

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

ExtendEnumsWithSelectionField() [4/6]

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

ExtendEnumsWithSelectionField() [5/6]

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

ExtendEnumsWithSelectionField() [6/6]

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

getGurobiSolverMethods()

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

(

)

Definition at line 946 of file GurobiLpSolver.cpp.

gurobiSolverMethodFromString()

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

(

std::string const &

method

)

Definition at line 937 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 558 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 397 of file NativeLinearEquationSolver.cpp.

toString() [1/14]

std::string storm::solver::toString

(

EigenLinearEquationSolverMethod

t

)

Definition at line 167 of file SolverSelectionOptions.cpp.

toString() [2/14]

std::string storm::solver::toString

(

EigenLinearEquationSolverPreconditioner

t

)

Definition at line 181 of file SolverSelectionOptions.cpp.

toString() [3/14]

std::string storm::solver::toString

(

EquationSolverType

t

)

Definition at line 91 of file SolverSelectionOptions.cpp.

toString() [4/14]

std::string storm::solver::toString

(

GameMethod

m

)

Definition at line 43 of file SolverSelectionOptions.cpp.

toString() [5/14]

std::string storm::solver::toString

(

GmmxxLinearEquationSolverMethod

t

)

Definition at line 143 of file SolverSelectionOptions.cpp.

toString() [6/14]

std::string storm::solver::toString

(

GmmxxLinearEquationSolverPreconditioner

t

)

Definition at line 155 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 917 of file GurobiLpSolver.cpp.

toString() [8/14]

std::string storm::solver::toString

(

LpSolverType

t

)

Definition at line 77 of file SolverSelectionOptions.cpp.

toString() [9/14]

std::string storm::solver::toString

(

LraMethod

m

)

Definition at line 53 of file SolverSelectionOptions.cpp.

toString() [10/14]

std::string storm::solver::toString

(

MaBoundedReachabilityMethod

m

)

Definition at line 67 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 33 of file SolverSelectionOptions.cpp.

toString() [13/14]

std::string storm::solver::toString

(

NativeLinearEquationSolverMethod

t

)

Definition at line 119 of file SolverSelectionOptions.cpp.

toString() [14/14]

std::string storm::solver::toString

(

SmtSolverType

t

)

Definition at line 109 of file SolverSelectionOptions.cpp.

Variable Documentation

Bicgstab

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

Definition at line 20 of file SolverSelectionOptions.h.

DGmres

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

Definition at line 22 of file SolverSelectionOptions.h.

GainBiasEquations

Gmmxx storm::solver::GainBiasEquations

Definition at line 11 of file SolverSelectionOptions.h.

Glpk

Gmmxx LraDistributionEquations storm::solver::Glpk

Definition at line 14 of file SolverSelectionOptions.h.

Gurobi

Gmmxx LraDistributionEquations storm::solver::Gurobi

Definition at line 14 of file SolverSelectionOptions.h.

LinearProgramming

Gmmxx storm::solver::LinearProgramming

Definition at line 11 of file SolverSelectionOptions.h.

Native

storm::solver::Native

Definition at line 10 of file SolverSelectionOptions.h.

Qmr

Gmmxx LraDistributionEquations Soplex Mathsat storm::solver::Qmr

Definition at line 20 of file SolverSelectionOptions.h.

SparseLU

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

Definition at line 22 of file SolverSelectionOptions.h.

ValueIteration

Gmmxx storm::solver::ValueIteration

Definition at line 11 of file SolverSelectionOptions.h.

Z3

Gmmxx LraDistributionEquations Soplex storm::solver::Z3

Definition at line 14 of file SolverSelectionOptions.h.