Namespaces
namespace	pfinternal
namespace	resources
namespace	solver
namespace	parameterlifting
namespace	parametric
namespace	cstring
namespace	permutation
namespace	builder
namespace	combinatorics
namespace	detail
namespace	dd
namespace	graph
namespace	kwek_mehlhorn
namespace	numerical
namespace	vector
namespace	ksp
namespace	string

Classes
class	AutomaticSettings
class	ModelInstantiator
	This class allows efficient instantiation of the given parametric model. More...
class	ConstantsComparator
class	ExtendedNumber
	A value of ValueType extended with the two infinities -infinity and +infinity. More...
class	Extremum
	Stores and manages an extremal (maximal or minimal) value. More...
class	FilteredRewardModel
class	ProgressMeasurement
	A class that provides convenience operations to display run times. More...
class	RandomProbabilityGenerator
class	RandomProbabilityGenerator< double >
class	RandomProbabilityGenerator< storm::RationalNumber >
class	BernoulliDistributionGenerator
class	ExponentialDistributionGenerator
class	Stopwatch
	A class that provides convenience operations to display run times. More...

Typedefs
template<typename ValueType>
using	ElementLess = typename detail::ElementLess<ValueType>::type
template<typename ValueType>
using	ElementGreater = typename detail::ElementGreater<ValueType>::type
template<typename ValueType>
using	ExtendedValueType = std::conditional_t<storm::NumberTraits<ValueType>::HasInfinity, ValueType, ExtendedNumber<ValueType>>
	The type to use for values that may be infinite.
template<typename ValueType>
using	FiniteValueType = typename detail::FiniteValueType<ValueType>::type
	The finite value type underlying a (possibly extended) type.
template<typename ValueType>
using	Maximum = Extremum<storm::OptimizationDirection::Maximize, ValueType>
template<typename ValueType>
using	Minimum = Extremum<storm::OptimizationDirection::Minimize, ValueType>

Enumerations
enum class	Engine { Sparse , Hybrid , Dd , DdSparse , Exploration , AbstractionRefinement , Automatic , Unknown }
	An enumeration of all engines. More...

Functions
template<typename T>
T	byteSwap (T const t)
	Swaps the byte representation of the given value, (i.e., swaps endianness) Taken from https://en.cppreference.com/w/cpp/numeric/byteswap.
template<typename T, bool ReverseBytes = true>
T	reverseBits (T const t)
	Swaps the bits in the bit representation of the given value.
template<typename ValueType>
ValueType	one ()
template<typename ValueType>
ValueType	zero ()
template<typename ValueType>
ValueType	infinity ()
template<typename ValueType>
bool	isOne (ValueType const &a)
template<typename ValueType>
bool	isZero (ValueType const &a)
template<typename ValueType>
bool	isNan (ValueType const &)
template<>
bool	isNan (double const &value)
template<typename ValueType>
bool	isApproxEqual (ValueType const &a, ValueType const &b, ValueType const &precision, bool relative)
template<typename ValueType>
bool	isPositive (ValueType const &a)
template<typename ValueType>
bool	isNonNegative (ValueType const &a)
template<typename ValueType>
bool	isBetween (ValueType const &a, ValueType const &b, ValueType const &c, bool strict)
	Compare whether a <= b <= c or a < b < c, based on the strictness parameter.
template<typename ValueType>
bool	isAlmostZero (ValueType const &a)
template<typename ValueType>
bool	isAlmostOne (ValueType const &a)
template<typename ValueType>
bool	isConstant (ValueType const &)
template<typename ValueType>
bool	isInfinity (ValueType const &a)
template<typename ValueType>
bool	isInteger (ValueType const &number)
template<>
bool	isInteger (int const &)
template<>
bool	isInteger (uint32_t const &)
template<>
bool	isInteger (storm::storage::sparse::state_type const &)
template<typename TargetType, typename SourceType>
TargetType	convertNumber (SourceType const &number)
template<>
uint_fast64_t	convertNumber (double const &number)
template<>
int_fast64_t	convertNumber (double const &number)
template<>
double	convertNumber (uint_fast64_t const &number)
template<>
double	convertNumber (double const &number)
template<>
double	convertNumber (long long const &number)
template<>
storm::storage::sparse::state_type	convertNumber (long long const &number)
template<typename ValueType>
ValueType	simplify (ValueType value)
template<typename ValueType>
std::pair< ValueType, ValueType >	minmax (std::vector< ValueType > const &values)
template<typename ValueType>
ValueType	minimum (std::vector< ValueType > const &values)
template<typename ValueType>
ValueType	maximum (std::vector< ValueType > const &values)
template<typename K, typename ValueType>
std::pair< ValueType, ValueType >	minmax (std::map< K, ValueType > const &values)
template<typename K, typename ValueType>
ValueType	minimum (std::map< K, ValueType > const &values)
template<typename K, typename ValueType>
ValueType	maximum (std::map< K, ValueType > const &values)
template<typename ValueType>
ValueType	pow (ValueType const &value, int_fast64_t exponent)
template<typename ValueType>
ValueType	max (ValueType const &first, ValueType const &second)
template<typename ValueType>
ValueType	min (ValueType const &first, ValueType const &second)
template<typename ValueType>
ValueType	sqrt (ValueType const &number)
template<typename ValueType>
ValueType	abs (ValueType const &number)
template<typename ValueType>
ValueType	floor (ValueType const &number)
template<typename ValueType>
ValueType	ceil (ValueType const &number)
template<typename ValueType>
ValueType	round (ValueType const &number)
template<typename ValueType>
ValueType	log (ValueType const &number)
template<typename ValueType>
ValueType	log10 (ValueType const &number)
template<typename ValueType>
ValueType	cos (ValueType const &number)
template<typename ValueType>
ValueType	sin (ValueType const &number)
template<typename ValueType>
uint64_t	numDigits (ValueType const &number)
template<typename ValueType>
uint64_t	bitsize (ValueType const &number)
	Returns the minimum number of bits to represent the given number.
template<typename ValueType>
NumberTraits< ValueType >::IntegerType	trunc (ValueType const &number)
template<typename IntegerType>
IntegerType	mod (IntegerType const &first, IntegerType const &second)
template<typename IntegerType>
std::pair< IntegerType, IntegerType >	divide (IntegerType const &dividend, IntegerType const &divisor)
	(Integer-)Divides the dividend by the divisor and returns the result plus the remainder.
template<typename IntegerType>
IntegerType	gcd (IntegerType const &first, IntegerType const &second)
template<typename IntegerType>
IntegerType	lcm (IntegerType const &first, IntegerType const &second)
template<typename ValueType>
std::string	to_string (ValueType const &value)
template<>
storm::RationalFunction	infinity ()
template<>
bool	isOne (storm::RationalFunction const &a)
template<>
bool	isOne (storm::Polynomial const &a)
template<>
bool	isZero (storm::RationalFunction const &a)
template<>
bool	isZero (storm::Polynomial const &a)
template<>
bool	isConstant (storm::RationalFunction const &a)
template<>
bool	isConstant (storm::Polynomial const &a)
template<>
bool	isApproxEqual (storm::RationalFunction const &a, storm::RationalFunction const &b, storm::RationalFunction const &precision, bool relative)
template<>
bool	isConstant (storm::Interval const &a)
template<>
bool	isConstant (storm::RationalInterval const &a)
template<>
bool	isInfinity (storm::RationalFunction const &a)
template<>
bool	isInteger (storm::RationalFunction const &func)
template<>
RationalFunction	convertNumber (double const &number)
template<>
RationalFunction	convertNumber (int_fast64_t const &number)
template<>
carl::uint	convertNumber (RationalFunction const &func)
template<>
carl::sint	convertNumber (RationalFunction const &func)
template<>
double	convertNumber (RationalFunction const &func)
template<>
RationalFunction	convertNumber (RationalFunction const &number)
template<>
RationalFunction	convertNumber (std::string const &number)
template<>
RationalFunction	convertNumber (storm::storage::sparse::state_type const &number)
template<>
RationalFunction &	simplify (RationalFunction &value)
template<>
RationalFunction &&	simplify (RationalFunction &&value)
template<>
RationalFunction	simplify (RationalFunction value)
template<>
RationalFunction &	simplify (RationalFunction &value)
template<>
RationalFunction &&	simplify (RationalFunction &&value)
template<>
bool	isAlmostZero (storm::RationalFunction const &a)
template<>
bool	isAlmostOne (storm::RationalFunction const &a)
template<>
bool	isNonNegative (storm::RationalFunction const &a)
template<>
bool	isPositive (storm::RationalFunction const &a)
template<>
bool	isBetween (storm::RationalFunction const &a, storm::RationalFunction const &b, storm::RationalFunction const &c, bool strict)
template<>
std::pair< storm::RationalFunction, storm::RationalFunction >	minmax (std::vector< storm::RationalFunction > const &)
template<>
storm::RationalFunction	minimum (std::vector< storm::RationalFunction > const &)
template<>
storm::RationalFunction	maximum (std::vector< storm::RationalFunction > const &)
template<>
std::pair< storm::RationalFunction, storm::RationalFunction >	minmax (std::map< uint64_t, storm::RationalFunction > const &)
template<>
storm::RationalFunction	minimum (std::map< uint64_t, storm::RationalFunction > const &)
template<>
storm::RationalFunction	maximum (std::map< uint64_t, storm::RationalFunction > const &)
template<>
RationalFunction	pow (RationalFunction const &value, int_fast64_t exponent)
template<>
std::string	to_string (RationalFunction const &f)
template<>
double	convertNumber (std::string const &value)
template<>
storm::Interval	convertNumber (double const &number)
template<>
storm::Interval	convertNumber (uint64_t const &number)
template<>
storm::RationalInterval	convertNumber (double const &number)
template<>
storm::RationalInterval	convertNumber (uint64_t const &number)
template<>
double	convertNumber (storm::Interval const &number)
template<>
double	convertNumber (storm::RationalInterval const &number)
template<>
storm::Interval	convertNumber (storm::RationalInterval const &number)
template<>
storm::RationalInterval	convertNumber (storm::Interval const &number)
template<>
storm::Interval	abs (storm::Interval const &interval)
template<>
storm::Interval	pow (storm::Interval const &value, int_fast64_t exponent)
template<>
bool	isApproxEqual (storm::Interval const &a, storm::Interval const &b, storm::Interval const &precision, bool relative)
template<>
bool	isApproxEqual (storm::RationalInterval const &a, storm::RationalInterval const &b, storm::RationalInterval const &precision, bool relative)
template<>
storm::RationalInterval	abs (storm::RationalInterval const &interval)
template<>
storm::RationalInterval	pow (storm::RationalInterval const &value, int_fast64_t exponent)
template double	one ()
template double	zero ()
template bool	isOne (double const &value)
template bool	isZero (double const &value)
template bool	isNonNegative (double const &value)
template bool	isPositive (double const &value)
template bool	isAlmostZero (double const &value)
template bool	isAlmostOne (double const &value)
template bool	isConstant (double const &value)
template bool	isInfinity (double const &value)
template bool	isInteger (double const &number)
template bool	isBetween (double const &a, double const &b, double const &c, bool strict)
template bool	isApproxEqual (double const &a, double const &b, double const &precision, bool relative)
template double	simplify (double value)
template std::pair< double, double >	minmax (std::vector< double > const &)
template double	minimum (std::vector< double > const &)
template double	maximum (std::vector< double > const &)
template std::pair< double, double >	minmax (std::map< uint64_t, double > const &)
template double	minimum (std::map< uint64_t, double > const &)
template double	maximum (std::map< uint64_t, double > const &)
template double	pow (double const &value, int_fast64_t exponent)
template double	max (double const &first, double const &second)
template double	min (double const &first, double const &second)
template double	sqrt (double const &number)
template double	abs (double const &number)
template double	floor (double const &number)
template double	ceil (double const &number)
template double	round (double const &number)
template double	log (double const &number)
template double	log10 (double const &number)
template double	cos (double const &number)
template double	sin (double const &number)
template NumberTraits< double >::IntegerType	trunc (double const &number)
template double	mod (double const &first, double const &second)
template std::string	to_string (double const &value)
template bool	isOne (int const &value)
template bool	isZero (int const &value)
template bool	isConstant (int const &value)
template bool	isInfinity (int const &value)
template bool	isNonNegative (int const &value)
template bool	isPositive (int const &value)
template bool	isApproxEqual (int const &a, int const &b, int const &precision, bool relative)
template bool	isBetween (int const &a, int const &b, int const &c, bool strict)
template bool	isOne (uint32_t const &value)
template bool	isZero (uint32_t const &value)
template bool	isConstant (uint32_t const &value)
template bool	isNonNegative (uint32_t const &value)
template bool	isPositive (uint32_t const &value)
template bool	isInfinity (uint32_t const &value)
template bool	isBetween (uint32_t const &a, uint32_t const &b, uint32_t const &c, bool strict)
template bool	isApproxEqual (storm::storage::sparse::state_type const &a, storm::storage::sparse::state_type const &b, storm::storage::sparse::state_type const &precision, bool relative)
template bool	isOne (storm::storage::sparse::state_type const &value)
template bool	isZero (storm::storage::sparse::state_type const &value)
template bool	isConstant (storm::storage::sparse::state_type const &value)
template bool	isPositive (storm::storage::sparse::state_type const &value)
template bool	isNonNegative (storm::storage::sparse::state_type const &value)
template bool	isInfinity (storm::storage::sparse::state_type const &value)
template bool	isBetween (storm::storage::sparse::state_type const &a, storm::storage::sparse::state_type const &b, storm::storage::sparse::state_type const &c, bool strict)
template uint64_t	bitsize (storm::storage::sparse::state_type const &number)
template int64_t	convertNumber (int64_t const &)
template unsigned long	convertNumber (long const &)
template bool	isNan (RationalFunction const &)
template bool	isOne (Interval const &value)
template bool	isZero (Interval const &value)
template bool	isInfinity (Interval const &value)
template bool	isAlmostZero (Interval const &value)
template bool	isNonNegative (Interval const &value)
template bool	isPositive (Interval const &value)
template bool	isBetween (Interval const &, Interval const &, Interval const &value, bool)
template std::string	to_string (storm::Interval const &value)
template bool	isOne (RationalInterval const &value)
template bool	isZero (RationalInterval const &value)
template bool	isInfinity (RationalInterval const &value)
template bool	isAlmostZero (RationalInterval const &value)
template bool	isNonNegative (RationalInterval const &value)
template bool	isPositive (RationalInterval const &value)
template bool	isBetween (RationalInterval const &, RationalInterval const &, RationalInterval const &value, bool)
template std::string	to_string (storm::RationalInterval const &value)
template std::pair< storm::ExtendedRationalNumber, storm::ExtendedRationalNumber >	minmax (std::vector< storm::ExtendedRationalNumber > const &values)
template storm::ExtendedRationalNumber	minimum (std::vector< storm::ExtendedRationalNumber > const &values)
template storm::ExtendedRationalNumber	maximum (std::vector< storm::ExtendedRationalNumber > const &values)
template std::pair< storm::ExtendedRationalNumber, storm::ExtendedRationalNumber >	minmax (std::map< uint64_t, storm::ExtendedRationalNumber > const &values)
template storm::ExtendedRationalNumber	minimum (std::map< uint64_t, storm::ExtendedRationalNumber > const &values)
template storm::ExtendedRationalNumber	maximum (std::map< uint64_t, storm::ExtendedRationalNumber > const &values)
template std::pair< storm::ExtendedRationalFunction, storm::ExtendedRationalFunction >	minmax (std::vector< storm::ExtendedRationalFunction > const &values)
template storm::ExtendedRationalFunction	minimum (std::vector< storm::ExtendedRationalFunction > const &values)
template storm::ExtendedRationalFunction	maximum (std::vector< storm::ExtendedRationalFunction > const &values)
template std::pair< storm::ExtendedRationalFunction, storm::ExtendedRationalFunction >	minmax (std::map< uint64_t, storm::ExtendedRationalFunction > const &values)
template storm::ExtendedRationalFunction	minimum (std::map< uint64_t, storm::ExtendedRationalFunction > const &values)
template storm::ExtendedRationalFunction	maximum (std::map< uint64_t, storm::ExtendedRationalFunction > const &values)
template<typename RationalType>
bool	tryParseNumber (std::string const &input, RationalType &result)
	Tries to parse a number from its string representation.
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry< IndexType, ValueType > &	simplify (storm::storage::MatrixEntry< IndexType, ValueType > &matrixEntry)
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry< IndexType, ValueType > &&	simplify (storm::storage::MatrixEntry< IndexType, ValueType > &&matrixEntry)
template<typename RationalType>
NumberTraits< RationalType >::IntegerType	numerator (RationalType const &number)
template<typename RationalType>
NumberTraits< RationalType >::IntegerType	denominator (RationalType const &number)
std::vector< Engine >	getEngines ()
	Returns a list of all available engines (excluding Unknown).
std::string	toString (Engine const &engine)
	Returns a string representation of the given engine.
std::ostream &	operator<< (std::ostream &os, Engine const &engine)
	Writes the string representation of the given engine to the given stream.
Engine	engineFromString (std::string const &engineStr)
	Parses the string representation of an engine and returns the corresponding engine.
storm::builder::BuilderType	getBuilderType (storm::utility::Engine const &engine)
	Returns the builder type used for the given engine.
template<typename ValueType>
bool	canHandle (storm::utility::Engine const &engine, storm::storage::SymbolicModelDescription::ModelType const &modelType, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask)
template<>
bool	canHandle< storm::RationalFunction > (storm::utility::Engine const &engine, storm::storage::SymbolicModelDescription::ModelType const &modelType, storm::modelchecker::CheckTask< storm::logic::Formula, storm::RationalFunction > const &checkTask)
template<typename ValueType>
bool	canHandle (storm::utility::Engine const &engine, std::vector< storm::jani::Property > const &properties, storm::storage::SymbolicModelDescription const &modelDescription)
	Returns false if the given model description and one of the given properties can certainly not be handled by the given engine.
template bool	canHandle< double > (storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)
template bool	canHandle< storm::RationalNumber > (storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)
template bool	canHandle< storm::RationalFunction > (storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)
template<typename ValueType>
ExtendedValueType< ValueType >	positiveInfinity ()
template<typename ValueType>
ExtendedValueType< ValueType >	negativeInfinity ()
template<typename ValueType>
ValueType const &	getFinite (ExtendedNumber< ValueType > const &value)
template<typename ValueType> requires (!detail::IsExtendedNumber<ValueType>::value)
ValueType const &	getFinite (ValueType const &value)
template<typename ValueType>
bool	isFinite (ExtendedNumber< ValueType > const &value)
template<typename ValueType> requires (!detail::IsExtendedNumber<ValueType>::value)
bool	isFinite (ValueType const &value)
template<typename ValueType>
std::vector< ValueType >	narrowFinite (std::vector< ExtendedValueType< ValueType > > &&values)
	The counterpart of widen for a vector all of whose values are finite.
template<typename ValueType>
std::vector< ValueType >	narrowFinite (std::vector< ExtendedValueType< ValueType > > const &values)
	The counterpart of widen for a vector all of whose values are finite.
template<typename ValueType>
std::vector< ValueType >	narrowFinite (std::vector< ExtendedValueType< ValueType > > &&values, ValueType const &defaultValue)
	The counterpart of widen for a vector, falling back to the given value wherever a value is infinite.
template<typename ValueType>
ValueType	narrow (ExtendedValueType< ValueType > const &value)
	Narrows an extended value back into the plain value type, for the interfaces that cannot hold an infinite one – a coordinate of a polytope, say.
template<typename ValueType>
std::vector< ExtendedValueType< ValueType > >	widen (std::vector< ValueType > &&values)
	Widens a vector of finite values into the extended value type.
template<typename ValueType> requires (!std::is_reference_v<ValueType>)
ExtendedValueType< ValueType >	fromSentinel (ValueType &&value)
	Recognises the value that storm::utility::infinity still yields for the value types that have no infinity of their own – the literal 100000000000 – and turns it into a real infinity.
template<typename ValueType>
std::vector< ExtendedValueType< ValueType > >	fromSentinel (std::vector< ValueType > &&values)
	The vector form.
template<typename ValueType>
ExtendedValueType< ValueType >	fromSentinel (ValueType const &value)
template<typename ValueType>
ValueType	toSentinel (ExtendedValueType< ValueType > const &value)
	The counterpart of fromSentinel: hands an extended value back to a part of Storm that still expects the sentinel, most of all a decision diagram leaf.
template<typename ValueType> requires (detail::IsExtendedNumber<ValueType>::value)
ValueType	zero ()
	The generic storm::utility::zero, one and infinity are declared for every value type but defined only for the ones that are explicitly instantiated.
template<typename ValueType> requires (detail::IsExtendedNumber<ValueType>::value)
ValueType	one ()
template<typename ValueType> requires (detail::IsExtendedNumber<ValueType>::value)
ValueType	infinity ()
template<typename ValueType>
bool	isInfinity (ExtendedNumber< ValueType > const &number)
template<typename ValueType>
bool	isNegativeInfinity (ExtendedNumber< ValueType > const &number)
template<typename ValueType> requires (!detail::IsExtendedNumber<ValueType>::value)
bool	isNegativeInfinity (ValueType const &value)
template<typename ValueType>
bool	isZero (ExtendedNumber< ValueType > const &number)
template<typename ValueType>
bool	isOne (ExtendedNumber< ValueType > const &number)
template<typename ValueType>
bool	isConstant (ExtendedNumber< ValueType > const &number)
template<typename ValueType>
ExtendedNumber< ValueType >	abs (ExtendedNumber< ValueType > const &number)
template<typename TargetType, typename SourceType>
TargetType	convertNumber (ExtendedNumber< SourceType > const &number)
	Converts a possibly infinite value to another type, which may itself be an ExtendedNumber or a type that has its own infinity.
template<typename TargetType, typename SourceType> requires (detail::IsExtendedNumber<TargetType>::value && !detail::IsExtendedNumber<SourceType>::value)
TargetType	convertNumber (SourceType const &number)
	Converts a value into an extended one.
template<typename RewardModelType>
FilteredRewardModel< RewardModelType >	createFilteredRewardModel (RewardModelType const &baseRewardModel, storm::logic::RewardAccumulation const &acc, bool isDiscreteTimeModel)
template<typename RewardModelType, typename FormulaType>
FilteredRewardModel< RewardModelType >	createFilteredRewardModel (RewardModelType const &baseRewardModel, bool isDiscreteTimeModel, FormulaType const &formula)
template<typename ModelType, typename CheckTaskType>
FilteredRewardModel< typename ModelType::RewardModelType >	createFilteredRewardModel (ModelType const &model, CheckTaskType const &checkTask)
void	initializeLogger ()
	Initializes the logging framework and sets up logging to console.
void	setOutputDigits (int digits)
	Set number of digits for printing output.
void	setUp ()
	Performs some necessary initializations.
void	cleanUp ()
	Performs some necessary clean-up.
void	setOutputDigitsFromGeneralPrecision (double precision)
	Set number of digits for printing output from given precision requirement.
l3pp::LogLevel	getLogLevel ()
	Gets the global log level.
void	setLogLevel (l3pp::LogLevel level)
	Set the global log level.
void	setStatisticsLogLevel (l3pp::LogLevel level)
	Set the log level for the statistics channel, independently of the global log level.
void	setProgressLogLevel (l3pp::LogLevel level)
	Set the log level for the progress channel, independently of the global log level.
void	initializeFileLogging (std::string const &logfileName)
	Sets up the logging to file.
template<std::predicate< uint64_t, uint64_t > EdgePredicate>
std::optional< std::vector< uint64_t > >	findPerfectMatching (uint64_t const n, EdgePredicate &&hasEdge)
storm::RationalNumber	findRational (storm::RationalNumber const &lowerBound, bool lowerInclusive, storm::RationalNumber const &upperBound, bool upperInclusive)
	Finds the "simplest" rational number in the given interval, where "simplest" means having the smallest denominator.
std::ostream &	operator<< (std::ostream &out, Stopwatch const &stopwatch)
uint64_t	getNumberOfThreads ()

Variables
constexpr const char *	STATISTICS_LOG_CHANNEL = "storm.statistics"
constexpr const char *	PROGRESS_LOG_CHANNEL = "storm.progress"
constexpr uint64_t	defaultProgressMeasurementDelay = 5

Typedef Documentation

◆ ElementGreater

template<typename ValueType>

using storm::utility::ElementGreater = typename detail::ElementGreater<ValueType>::type

Definition at line 69 of file constants.h.

◆ ElementLess

template<typename ValueType>

using storm::utility::ElementLess = typename detail::ElementLess<ValueType>::type

Definition at line 66 of file constants.h.

◆ ExtendedValueType

template<typename ValueType>

using storm::utility::ExtendedValueType = std::conditional_t<storm::NumberTraits<ValueType>::HasInfinity, ValueType, ExtendedNumber<ValueType>>

The type to use for values that may be infinite.

For value types that have their own infinity, this is the value type itself, so that in particular double keeps using its IEEE infinity and pays nothing for this.

Definition at line 331 of file ExtendedNumber.h.

◆ FiniteValueType

template<typename ValueType>

using storm::utility::FiniteValueType = typename detail::FiniteValueType<ValueType>::type

The finite value type underlying a (possibly extended) type.

This is what a solver or a matrix operates on once the infinite entries have been split off.

Definition at line 357 of file ExtendedNumber.h.

◆ Maximum

template<typename ValueType>

using storm::utility::Maximum = Extremum<storm::OptimizationDirection::Maximize, ValueType>

Definition at line 166 of file Extremum.h.

◆ Minimum

template<typename ValueType>

using storm::utility::Minimum = Extremum<storm::OptimizationDirection::Minimize, ValueType>

Definition at line 168 of file Extremum.h.

Enumeration Type Documentation

◆ Engine

enum class storm::utility::Engine

strong

An enumeration of all engines.

Enumerator
Sparse
Hybrid
Dd
DdSparse
Exploration
AbstractionRefinement
Automatic
Unknown

Definition at line 31 of file Engine.h.

Function Documentation

◆ abs() [1/5]

template double storm::utility::abs ( double const & number )

◆ abs() [2/5]

template<typename ValueType>

ExtendedNumber< ValueType > storm::utility::abs ( ExtendedNumber< ValueType > const & number )

Definition at line 651 of file ExtendedNumber.h.

◆ abs() [3/5]

template<>

storm::Interval storm::utility::abs ( storm::Interval const & interval )

Definition at line 1190 of file constants.cpp.

◆ abs() [4/5]

template<>

storm::RationalInterval storm::utility::abs ( storm::RationalInterval const & interval )

Definition at line 1218 of file constants.cpp.

◆ abs() [5/5]

template<typename ValueType>

ValueType storm::utility::abs ( ValueType const & number )

Definition at line 273 of file constants.cpp.

◆ bitsize() [1/2]

template uint64_t storm::utility::bitsize ( storm::storage::sparse::state_type const & number )

◆ bitsize() [2/2]

template<typename ValueType>

uint64_t storm::utility::bitsize ( ValueType const & number )

Returns the minimum number of bits to represent the given number.

Ignores sign, i.e. number and -number have the same size.

Definition at line 326 of file constants.cpp.

◆ byteSwap()

template<typename T>

T storm::utility::byteSwap ( T const t )

inline

Swaps the byte representation of the given value, (i.e., swaps endianness) Taken from https://en.cppreference.com/w/cpp/numeric/byteswap.

Definition at line 16 of file bitoperations.h.

◆ canHandle() [1/2]

template<typename ValueType>

bool storm::utility::canHandle	(	storm::utility::Engine const &	engine,
		std::vector< storm::jani::Property > const &	properties,
		storm::storage::SymbolicModelDescription const &	modelDescription )

Returns false if the given model description and one of the given properties can certainly not be handled by the given engine.

Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true, the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need to actually build the model in order to decide whether it is supported.

Definition at line 258 of file Engine.cpp.

◆ canHandle() [2/2]

template<typename ValueType>

bool storm::utility::canHandle	(	storm::utility::Engine const &	engine,
		storm::storage::SymbolicModelDescription::ModelType const &	modelType,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	checkTask )

Definition at line 99 of file Engine.cpp.

◆ canHandle< double >()

template bool storm::utility::canHandle< double >	(	storm::utility::Engine const &	,
		std::vector< storm::jani::Property > const &	,
		storm::storage::SymbolicModelDescription const &	)

◆ canHandle< storm::RationalFunction >() [1/2]

template bool storm::utility::canHandle< storm::RationalFunction >	(	storm::utility::Engine const &	,
		std::vector< storm::jani::Property > const &	,
		storm::storage::SymbolicModelDescription const &	)

◆ canHandle< storm::RationalFunction >() [2/2]

template<>

bool storm::utility::canHandle< storm::RationalFunction >	(	storm::utility::Engine const &	engine,
		storm::storage::SymbolicModelDescription::ModelType const &	modelType,
		storm::modelchecker::CheckTask< storm::logic::Formula, storm::RationalFunction > const &	checkTask )

Definition at line 196 of file Engine.cpp.

◆ canHandle< storm::RationalNumber >()

template bool storm::utility::canHandle< storm::RationalNumber >	(	storm::utility::Engine const &	,
		std::vector< storm::jani::Property > const &	,
		storm::storage::SymbolicModelDescription const &	)

◆ ceil() [1/2]

template double storm::utility::ceil ( double const & number )

◆ ceil() [2/2]

template<typename ValueType>

ValueType storm::utility::ceil ( ValueType const & number )

Definition at line 283 of file constants.cpp.

◆ cleanUp()

void storm::utility::cleanUp ( )

Performs some necessary clean-up.

Definition at line 37 of file initialize.cpp.

◆ convertNumber() [1/28]

template<>

storm::RationalInterval storm::utility::convertNumber ( double const & number )

Definition at line 1108 of file constants.cpp.

◆ convertNumber() [2/28]

template<>

storm::Interval storm::utility::convertNumber ( double const & number )

Definition at line 1098 of file constants.cpp.

◆ convertNumber() [3/28]

template<>

RationalFunction storm::utility::convertNumber ( double const & number )

Definition at line 919 of file constants.cpp.

◆ convertNumber() [4/28]

template<>

double storm::utility::convertNumber ( double const & number )

Definition at line 165 of file constants.cpp.

◆ convertNumber() [5/28]

template<>

int_fast64_t storm::utility::convertNumber ( double const & number )

Definition at line 155 of file constants.cpp.

◆ convertNumber() [6/28]

template<>

uint_fast64_t storm::utility::convertNumber ( double const & number )

Definition at line 150 of file constants.cpp.

◆ convertNumber() [7/28]

template<typename TargetType, typename SourceType>

TargetType storm::utility::convertNumber ( ExtendedNumber< SourceType > const & number )

Converts a possibly infinite value to another type, which may itself be an ExtendedNumber or a type that has its own infinity.

This is what lets an infinite value cross value types without every call site restating what infinity means in the source and in the target type.

Definition at line 664 of file ExtendedNumber.h.

◆ convertNumber() [8/28]

template int64_t storm::utility::convertNumber ( int64_t const & )

◆ convertNumber() [9/28]

template<>

RationalFunction storm::utility::convertNumber ( int_fast64_t const & number )

Definition at line 924 of file constants.cpp.

◆ convertNumber() [10/28]

template double storm::utility::convertNumber ( long const & )

◆ convertNumber() [11/28]

template<>

storm::storage::sparse::state_type storm::utility::convertNumber ( long long const & number )

Definition at line 175 of file constants.cpp.

◆ convertNumber() [12/28]

template<>

double storm::utility::convertNumber ( long long const & number )

Definition at line 170 of file constants.cpp.

◆ convertNumber() [13/28]

template<>

double storm::utility::convertNumber ( RationalFunction const & func )

Definition at line 965 of file constants.cpp.

◆ convertNumber() [14/28]

template<>

carl::sint storm::utility::convertNumber ( RationalFunction const & func )

Definition at line 960 of file constants.cpp.

◆ convertNumber() [15/28]

template<>

carl::uint storm::utility::convertNumber ( RationalFunction const & func )

Definition at line 955 of file constants.cpp.

◆ convertNumber() [16/28]

template<>

RationalFunction storm::utility::convertNumber ( RationalFunction const & number )

Definition at line 970 of file constants.cpp.

◆ convertNumber() [17/28]

template<typename TargetType, typename SourceType>

TargetType storm::utility::convertNumber ( SourceType const & number )

Definition at line 145 of file constants.cpp.

◆ convertNumber() [18/28]

template<typename TargetType, typename SourceType>
requires (detail::IsExtendedNumber<TargetType>::value && !detail::IsExtendedNumber<SourceType>::value)

TargetType storm::utility::convertNumber ( SourceType const & number )

Converts a value into an extended one.

If the source type has an infinity of its own it is carried over; otherwise this is just the underlying conversion followed by the implicit constructor.

Definition at line 682 of file ExtendedNumber.h.

◆ convertNumber() [19/28]

template<>

RationalFunction storm::utility::convertNumber ( std::string const & number )

Definition at line 975 of file constants.cpp.

◆ convertNumber() [20/28]

template<>

double storm::utility::convertNumber ( std::string const & value )

Definition at line 1093 of file constants.cpp.

◆ convertNumber() [21/28]

template<>

storm::RationalInterval storm::utility::convertNumber ( storm::Interval const & number )

Definition at line 1184 of file constants.cpp.

◆ convertNumber() [22/28]

template<>

template Interval storm::utility::convertNumber ( storm::Interval const & number )

Definition at line 1166 of file constants.cpp.

◆ convertNumber() [23/28]

template<>

storm::Interval storm::utility::convertNumber ( storm::RationalInterval const & number )

Definition at line 1178 of file constants.cpp.

◆ convertNumber() [24/28]

template<>

template RationalInterval storm::utility::convertNumber ( storm::RationalInterval const & number )

Definition at line 1172 of file constants.cpp.

◆ convertNumber() [25/28]

template<>

RationalFunction storm::utility::convertNumber ( storm::storage::sparse::state_type const & number )

Definition at line 980 of file constants.cpp.

◆ convertNumber() [26/28]

template<>

storm::RationalInterval storm::utility::convertNumber ( uint64_t const & number )

Definition at line 1113 of file constants.cpp.

◆ convertNumber() [27/28]

template<>

storm::Interval storm::utility::convertNumber ( uint64_t const & number )

Definition at line 1103 of file constants.cpp.

◆ convertNumber() [28/28]

template<>

double storm::utility::convertNumber ( uint_fast64_t const & number )

Definition at line 160 of file constants.cpp.

◆ cos() [1/2]

template double storm::utility::cos ( double const & number )

◆ cos() [2/2]

template<typename ValueType>

ValueType storm::utility::cos ( ValueType const & number )

Definition at line 304 of file constants.cpp.

◆ createFilteredRewardModel() [1/3]

template<typename ModelType, typename CheckTaskType>

FilteredRewardModel< typename ModelType::RewardModelType > storm::utility::createFilteredRewardModel	(	ModelType const &	model,
		CheckTaskType const &	checkTask )

Definition at line 99 of file FilteredRewardModel.h.

◆ createFilteredRewardModel() [2/3]

template<typename RewardModelType, typename FormulaType>

FilteredRewardModel< RewardModelType > storm::utility::createFilteredRewardModel	(	RewardModelType const &	baseRewardModel,
		bool	isDiscreteTimeModel,
		FormulaType const &	formula )

Definition at line 90 of file FilteredRewardModel.h.

◆ createFilteredRewardModel() [3/3]

template<typename RewardModelType>

FilteredRewardModel< RewardModelType > storm::utility::createFilteredRewardModel	(	RewardModelType const &	baseRewardModel,
		storm::logic::RewardAccumulation const &	acc,
		bool	isDiscreteTimeModel )

Definition at line 78 of file FilteredRewardModel.h.

◆ denominator()

template<typename RationalType>

NumberTraits< RationalType >::IntegerType storm::utility::denominator ( RationalType const & number )

◆ divide()

template<typename IntegerType>

std::pair< IntegerType, IntegerType > storm::utility::divide	(	IntegerType const &	dividend,
		IntegerType const &	divisor )

(Integer-)Divides the dividend by the divisor and returns the result plus the remainder.

Definition at line 351 of file constants.cpp.

◆ engineFromString()

Engine storm::utility::engineFromString ( std::string const & engineStr )

Parses the string representation of an engine and returns the corresponding engine.

If the engine is not found, we print an error and return Engine::Unknown.

Definition at line 64 of file Engine.cpp.

◆ findPerfectMatching()

template<std::predicate< uint64_t, uint64_t > EdgePredicate>

std::optional< std::vector< uint64_t > > storm::utility::findPerfectMatching	(	uint64_t const	n,
		EdgePredicate &&	hasEdge )

Definition at line 18 of file matching.h.

◆ findRational()

storm::RationalNumber storm::utility::findRational	(	storm::RationalNumber const &	lowerBound,
		bool	lowerInclusive,
		storm::RationalNumber const &	upperBound,
		bool	upperInclusive )

Finds the "simplest" rational number in the given interval, where "simplest" means having the smallest denominator.

Precondition: lowerBound < upperBound or (lowerBound == upperBound and lowerInclusive and upperInclusive)

Parameters

lowerBound	The lower bound of the interval
lowerInclusive	Whether the lower bound itself is included
upperBound	the upper bound of the interval
upperInclusive	Whether the upper bound itself is included

Returns: the rational number in the given interval with the smallest denominator

Definition at line 11 of file RationalApproximation.cpp.

◆ floor() [1/2]

template double storm::utility::floor ( double const & number )

◆ floor() [2/2]

template<typename ValueType>

ValueType storm::utility::floor ( ValueType const & number )

Definition at line 278 of file constants.cpp.

◆ fromSentinel() [1/3]

template<typename ValueType>

std::vector< ExtendedValueType< ValueType > > storm::utility::fromSentinel ( std::vector< ValueType > && values )

The vector form.

It builds the sentinel once instead of once per element: for a value type whose infinity is a number rather than a bit pattern, constructing it allocates, and doing that per element costs more than the widening itself. The values are taken over rather than copied.

Definition at line 534 of file ExtendedNumber.h.

◆ fromSentinel() [2/3]

template<typename ValueType>
requires (!std::is_reference_v<ValueType>)

ExtendedValueType< ValueType > storm::utility::fromSentinel ( ValueType && value )

Recognises the value that storm::utility::infinity still yields for the value types that have no infinity of their own – the literal 100000000000 – and turns it into a real infinity.

This is a bridge for the parts of Storm that still produce that sentinel, most of all the decision diagram leaves. It inherits the sentinel's weaknesses, so it is not a place to build on; it disappears together with the sentinel.

Definition at line 518 of file ExtendedNumber.h.

◆ fromSentinel() [3/3]

template<typename ValueType>

ExtendedValueType< ValueType > storm::utility::fromSentinel ( ValueType const & value )

Definition at line 555 of file ExtendedNumber.h.

◆ gcd()

template<typename IntegerType>

IntegerType storm::utility::gcd	(	IntegerType const &	first,
		IntegerType const &	second )

Definition at line 356 of file constants.cpp.

◆ getBuilderType()

storm::builder::BuilderType storm::utility::getBuilderType ( Engine const & engine )

Returns the builder type used for the given engine.

Definition at line 78 of file Engine.cpp.

◆ getEngines()

std::vector< Engine > storm::utility::getEngines ( )

Returns a list of all available engines (excluding Unknown).

Definition at line 27 of file Engine.cpp.

◆ getFinite() [1/2]

template<typename ValueType>

ValueType const & storm::utility::getFinite ( ExtendedNumber< ValueType > const & value )

Precondition: the value is finite

Returns: the finite value, whether or not the type it is held in is an extended one. This is for the places that read a single entry out of a result they know to be finite, where copying the whole vector would be wasteful.

Definition at line 389 of file ExtendedNumber.h.

◆ getFinite() [2/2]

template<typename ValueType>
requires (!detail::IsExtendedNumber<ValueType>::value)

ValueType const & storm::utility::getFinite ( ValueType const & value )

Definition at line 395 of file ExtendedNumber.h.

◆ getLogLevel()

l3pp::LogLevel storm::utility::getLogLevel ( )

Gets the global log level.

Definition at line 55 of file initialize.cpp.

◆ getNumberOfThreads()

uint64_t storm::utility::getNumberOfThreads ( )

Definition at line 55 of file threads.cpp.

◆ infinity() [1/3]

template<>

storm::RationalFunction storm::utility::infinity ( )

Definition at line 853 of file constants.cpp.

◆ infinity() [2/3]

template<typename ValueType>

ValueType storm::utility::infinity ( )

Definition at line 31 of file constants.cpp.

◆ infinity() [3/3]

template<typename ValueType>
requires (detail::IsExtendedNumber<ValueType>::value)

ValueType storm::utility::infinity ( )

Definition at line 603 of file ExtendedNumber.h.

◆ initializeFileLogging()

void storm::utility::initializeFileLogging ( std::string const & logfileName )

Sets up the logging to file.

Definition at line 76 of file initialize.cpp.

◆ initializeLogger()

void storm::utility::initializeLogger ( )

Initializes the logging framework and sets up logging to console.

Definition at line 10 of file initialize.cpp.

◆ isAlmostOne() [1/3]

template bool storm::utility::isAlmostOne ( double const & value )

◆ isAlmostOne() [2/3]

template<>

bool storm::utility::isAlmostOne ( storm::RationalFunction const & a )

Definition at line 1014 of file constants.cpp.

◆ isAlmostOne() [3/3]

template<typename ValueType>

bool storm::utility::isAlmostOne ( ValueType const & a )

Definition at line 103 of file constants.cpp.

◆ isAlmostZero() [1/5]

template bool storm::utility::isAlmostZero ( double const & value )

◆ isAlmostZero() [2/5]

template bool storm::utility::isAlmostZero ( Interval const & value )

◆ isAlmostZero() [3/5]

template bool storm::utility::isAlmostZero ( RationalInterval const & value )

◆ isAlmostZero() [4/5]

template<>

bool storm::utility::isAlmostZero ( storm::RationalFunction const & a )

Definition at line 1009 of file constants.cpp.

◆ isAlmostZero() [5/5]

template<typename ValueType>

bool storm::utility::isAlmostZero ( ValueType const & a )

Definition at line 98 of file constants.cpp.

◆ isApproxEqual() [1/7]

template bool storm::utility::isApproxEqual	(	double const &	a,
		double const &	b,
		double const &	precision,
		bool	relative )

◆ isApproxEqual() [2/7]

template bool storm::utility::isApproxEqual	(	int const &	a,
		int const &	b,
		int const &	precision,
		bool	relative )

◆ isApproxEqual() [3/7]

template<>

bool storm::utility::isApproxEqual	(	storm::Interval const &	a,
		storm::Interval const &	b,
		storm::Interval const &	precision,
		bool	relative )

Definition at line 1204 of file constants.cpp.

◆ isApproxEqual() [4/7]

template<>

bool storm::utility::isApproxEqual	(	storm::RationalFunction const &	a,
		storm::RationalFunction const &	b,
		storm::RationalFunction const &	precision,
		bool	relative )

Definition at line 892 of file constants.cpp.

◆ isApproxEqual() [5/7]

template<>

bool storm::utility::isApproxEqual	(	storm::RationalInterval const &	a,
		storm::RationalInterval const &	b,
		storm::RationalInterval const &	precision,
		bool	relative )

Definition at line 1211 of file constants.cpp.

◆ isApproxEqual() [6/7]

template bool storm::utility::isApproxEqual	(	storm::storage::sparse::state_type const &	a,
		storm::storage::sparse::state_type const &	b,
		storm::storage::sparse::state_type const &	precision,
		bool	relative )

◆ isApproxEqual() [7/7]

template<typename ValueType>

bool storm::utility::isApproxEqual	(	ValueType const &	a,
		ValueType const &	b,
		ValueType const &	precision,
		bool	relative )

Definition at line 59 of file constants.cpp.

◆ isBetween() [1/8]

template bool storm::utility::isBetween	(	double const &	a,
		double const &	b,
		double const &	c,
		bool	strict )

◆ isBetween() [2/8]

template bool storm::utility::isBetween	(	int const &	a,
		int const &	b,
		int const &	c,
		bool	strict )

◆ isBetween() [3/8]

template bool storm::utility::isBetween	(	Interval const &	,
		Interval const &	,
		Interval const &	value,
		bool	)

◆ isBetween() [4/8]

template bool storm::utility::isBetween	(	RationalInterval const &	,
		RationalInterval const &	,
		RationalInterval const &	value,
		bool	)

◆ isBetween() [5/8]

template<>

bool storm::utility::isBetween	(	storm::RationalFunction const &	a,
		storm::RationalFunction const &	b,
		storm::RationalFunction const &	c,
		bool	strict )

Definition at line 1029 of file constants.cpp.

◆ isBetween() [6/8]

template bool storm::utility::isBetween	(	storm::storage::sparse::state_type const &	a,
		storm::storage::sparse::state_type const &	b,
		storm::storage::sparse::state_type const &	c,
		bool	strict )

◆ isBetween() [7/8]

template bool storm::utility::isBetween	(	uint32_t const &	a,
		uint32_t const &	b,
		uint32_t const &	c,
		bool	strict )

◆ isBetween() [8/8]

template<typename ValueType>

bool storm::utility::isBetween	(	ValueType const &	a,
		ValueType const &	b,
		ValueType const &	c,
		bool	strict )

Compare whether a <= b <= c or a < b < c, based on the strictness parameter.

Check whether a <= b <= c holds (if not strict, the default) or a < b < c (if strict).

Parameters

a	A constant value
b	Some value
c	A constant value
strict	Changes the type of the comparison

Returns: true if b is between a and c.

Definition at line 87 of file constants.cpp.

◆ isConstant() [1/10]

template bool storm::utility::isConstant ( double const & value )

◆ isConstant() [2/10]

template<typename ValueType>

bool storm::utility::isConstant ( ExtendedNumber< ValueType > const & number )

Definition at line 646 of file ExtendedNumber.h.

◆ isConstant() [3/10]

template bool storm::utility::isConstant ( int const & value )

◆ isConstant() [4/10]

template<>

bool storm::utility::isConstant ( storm::Interval const & a )

Definition at line 898 of file constants.cpp.

◆ isConstant() [5/10]

template<>

bool storm::utility::isConstant ( storm::Polynomial const & a )

Definition at line 887 of file constants.cpp.

◆ isConstant() [6/10]

template<>

bool storm::utility::isConstant ( storm::RationalFunction const & a )

Definition at line 882 of file constants.cpp.

◆ isConstant() [7/10]

template<>

bool storm::utility::isConstant ( storm::RationalInterval const & a )

Definition at line 903 of file constants.cpp.

◆ isConstant() [8/10]

template bool storm::utility::isConstant ( storm::storage::sparse::state_type const & value )

◆ isConstant() [9/10]

template bool storm::utility::isConstant ( uint32_t const & value )

◆ isConstant() [10/10]

template<typename ValueType>

bool storm::utility::isConstant ( ValueType const & )

Definition at line 108 of file constants.cpp.

◆ isFinite() [1/2]

template<typename ValueType>

bool storm::utility::isFinite ( ExtendedNumber< ValueType > const & value )

Returns: whether the value is neither of the two infinities, whether or not the type it is held in is an extended one.

Definition at line 403 of file ExtendedNumber.h.

◆ isFinite() [2/2]

template<typename ValueType>
requires (!detail::IsExtendedNumber<ValueType>::value)

bool storm::utility::isFinite ( ValueType const & value )

Definition at line 409 of file ExtendedNumber.h.

◆ isInfinity() [1/9]

template bool storm::utility::isInfinity ( double const & value )

◆ isInfinity() [2/9]

template<typename ValueType>

bool storm::utility::isInfinity ( ExtendedNumber< ValueType > const & number )

Returns: true if the given value is +infinity. This mirrors the meaning that isInfinity has for the value types that bring their own infinity, where -infinity is not reported either.

Definition at line 612 of file ExtendedNumber.h.

◆ isInfinity() [3/9]

template bool storm::utility::isInfinity ( int const & value )

◆ isInfinity() [4/9]

template bool storm::utility::isInfinity ( Interval const & value )

◆ isInfinity() [5/9]

template bool storm::utility::isInfinity ( RationalInterval const & value )

◆ isInfinity() [6/9]

template<>

bool storm::utility::isInfinity ( storm::RationalFunction const & a )

Definition at line 908 of file constants.cpp.

◆ isInfinity() [7/9]

template bool storm::utility::isInfinity ( storm::storage::sparse::state_type const & value )

◆ isInfinity() [8/9]

template bool storm::utility::isInfinity ( uint32_t const & value )

◆ isInfinity() [9/9]

template<typename ValueType>

bool storm::utility::isInfinity ( ValueType const & a )

Definition at line 113 of file constants.cpp.

◆ isInteger() [1/6]

template bool storm::utility::isInteger ( double const & number )

◆ isInteger() [2/6]

template<>

bool storm::utility::isInteger ( int const & )

Definition at line 130 of file constants.cpp.

◆ isInteger() [3/6]

template<>

bool storm::utility::isInteger ( storm::RationalFunction const & func )

Definition at line 914 of file constants.cpp.

◆ isInteger() [4/6]

template<>

bool storm::utility::isInteger ( storm::storage::sparse::state_type const & )

Definition at line 140 of file constants.cpp.

◆ isInteger() [5/6]

template<>

bool storm::utility::isInteger ( uint32_t const & )

Definition at line 135 of file constants.cpp.

◆ isInteger() [6/6]

template<typename ValueType>

bool storm::utility::isInteger ( ValueType const & number )

Definition at line 123 of file constants.cpp.

◆ isNan() [1/3]

template<>

bool storm::utility::isNan ( double const & value )

Definition at line 54 of file constants.cpp.

◆ isNan() [2/3]

template bool storm::utility::isNan ( RationalFunction const & )

◆ isNan() [3/3]

template<typename ValueType>

bool storm::utility::isNan ( ValueType const & )

Definition at line 49 of file constants.cpp.

◆ isNegativeInfinity() [1/2]

template<typename ValueType>

bool storm::utility::isNegativeInfinity ( ExtendedNumber< ValueType > const & number )

Returns: true if the given value is -infinity, whether or not the type it is held in is an extended one. This is the counterpart of isInfinity for the places that have to tell the two infinities apart, such as writing a result out.

Definition at line 621 of file ExtendedNumber.h.

◆ isNegativeInfinity() [2/2]

template<typename ValueType>
requires (!detail::IsExtendedNumber<ValueType>::value)

bool storm::utility::isNegativeInfinity ( ValueType const & value )

Definition at line 627 of file ExtendedNumber.h.

◆ isNonNegative() [1/8]

template bool storm::utility::isNonNegative ( double const & value )

◆ isNonNegative() [2/8]

template bool storm::utility::isNonNegative ( int const & value )

◆ isNonNegative() [3/8]

template bool storm::utility::isNonNegative ( Interval const & value )

◆ isNonNegative() [4/8]

template bool storm::utility::isNonNegative ( RationalInterval const & value )

◆ isNonNegative() [5/8]

template<>

bool storm::utility::isNonNegative ( storm::RationalFunction const & a )

Definition at line 1019 of file constants.cpp.

◆ isNonNegative() [6/8]

template bool storm::utility::isNonNegative ( storm::storage::sparse::state_type const & value )

◆ isNonNegative() [7/8]

template bool storm::utility::isNonNegative ( uint32_t const & value )

◆ isNonNegative() [8/8]

template<typename ValueType>

bool storm::utility::isNonNegative ( ValueType const & a )

Definition at line 74 of file constants.cpp.

◆ isOne() [1/10]

template bool storm::utility::isOne ( double const & value )

◆ isOne() [2/10]

template<typename ValueType>

bool storm::utility::isOne ( ExtendedNumber< ValueType > const & number )

Definition at line 641 of file ExtendedNumber.h.

◆ isOne() [3/10]

template bool storm::utility::isOne ( int const & value )

◆ isOne() [4/10]

template bool storm::utility::isOne ( Interval const & value )

◆ isOne() [5/10]

template bool storm::utility::isOne ( RationalInterval const & value )

◆ isOne() [6/10]

template<>

bool storm::utility::isOne ( storm::Polynomial const & a )

Definition at line 867 of file constants.cpp.

◆ isOne() [7/10]

template<>

bool storm::utility::isOne ( storm::RationalFunction const & a )

Definition at line 862 of file constants.cpp.

◆ isOne() [8/10]

template bool storm::utility::isOne ( storm::storage::sparse::state_type const & value )

◆ isOne() [9/10]

template bool storm::utility::isOne ( uint32_t const & value )

◆ isOne() [10/10]

template<typename ValueType>

bool storm::utility::isOne ( ValueType const & a )

Definition at line 39 of file constants.cpp.

◆ isPositive() [1/8]

template bool storm::utility::isPositive ( double const & value )

◆ isPositive() [2/8]

template bool storm::utility::isPositive ( int const & value )

◆ isPositive() [3/8]

template bool storm::utility::isPositive ( Interval const & value )

◆ isPositive() [4/8]

template bool storm::utility::isPositive ( RationalInterval const & value )

◆ isPositive() [5/8]

template<>

bool storm::utility::isPositive ( storm::RationalFunction const & a )

Definition at line 1024 of file constants.cpp.

◆ isPositive() [6/8]

template bool storm::utility::isPositive ( storm::storage::sparse::state_type const & value )

◆ isPositive() [7/8]

template bool storm::utility::isPositive ( uint32_t const & value )

◆ isPositive() [8/8]

template<typename ValueType>

bool storm::utility::isPositive ( ValueType const & a )

Definition at line 69 of file constants.cpp.

◆ isZero() [1/10]

template bool storm::utility::isZero ( double const & value )

◆ isZero() [2/10]

template<typename ValueType>

bool storm::utility::isZero ( ExtendedNumber< ValueType > const & number )

Definition at line 636 of file ExtendedNumber.h.

◆ isZero() [3/10]

template bool storm::utility::isZero ( int const & value )

◆ isZero() [4/10]

template bool storm::utility::isZero ( Interval const & value )

◆ isZero() [5/10]

template bool storm::utility::isZero ( RationalInterval const & value )

◆ isZero() [6/10]

template<>

bool storm::utility::isZero ( storm::Polynomial const & a )

Definition at line 877 of file constants.cpp.

◆ isZero() [7/10]

template<>

bool storm::utility::isZero ( storm::RationalFunction const & a )

Definition at line 872 of file constants.cpp.

◆ isZero() [8/10]

template bool storm::utility::isZero ( storm::storage::sparse::state_type const & value )

◆ isZero() [9/10]

template bool storm::utility::isZero ( uint32_t const & value )

◆ isZero() [10/10]

template<typename ValueType>

bool storm::utility::isZero ( ValueType const & a )

Definition at line 44 of file constants.cpp.

◆ lcm()

template<typename IntegerType>

IntegerType storm::utility::lcm	(	IntegerType const &	first,
		IntegerType const &	second )

Definition at line 361 of file constants.cpp.

◆ log() [1/2]

template double storm::utility::log ( double const & number )

◆ log() [2/2]

template<typename ValueType>

ValueType storm::utility::log ( ValueType const & number )

Definition at line 294 of file constants.cpp.

◆ log10() [1/2]

template double storm::utility::log10 ( double const & number )

◆ log10() [2/2]

template<typename ValueType>

ValueType storm::utility::log10 ( ValueType const & number )

Definition at line 299 of file constants.cpp.

◆ max() [1/2]

template double storm::utility::max	(	double const &	first,
		double const &	second )

◆ max() [2/2]

template<typename ValueType>

ValueType storm::utility::max	(	ValueType const &	first,
		ValueType const &	second )

Definition at line 258 of file constants.cpp.

◆ maximum() [1/10]

template<typename K, typename ValueType>

ValueType storm::utility::maximum ( std::map< K, ValueType > const & values )

Definition at line 248 of file constants.cpp.

◆ maximum() [2/10]

template double storm::utility::maximum ( std::map< uint64_t, double > const & )

◆ maximum() [3/10]

template storm::ExtendedRationalFunction storm::utility::maximum ( std::map< uint64_t, storm::ExtendedRationalFunction > const & values )

◆ maximum() [4/10]

template storm::ExtendedRationalNumber storm::utility::maximum ( std::map< uint64_t, storm::ExtendedRationalNumber > const & values )

◆ maximum() [5/10]

template<>

storm::RationalFunction storm::utility::maximum ( std::map< uint64_t, storm::RationalFunction > const & )

Definition at line 1062 of file constants.cpp.

◆ maximum() [6/10]

template double storm::utility::maximum ( std::vector< double > const & )

◆ maximum() [7/10]

template storm::ExtendedRationalFunction storm::utility::maximum ( std::vector< storm::ExtendedRationalFunction > const & values )

◆ maximum() [8/10]

template storm::ExtendedRationalNumber storm::utility::maximum ( std::vector< storm::ExtendedRationalNumber > const & values )

◆ maximum() [9/10]

template<>

storm::RationalFunction storm::utility::maximum ( std::vector< storm::RationalFunction > const & )

Definition at line 1047 of file constants.cpp.

◆ maximum() [10/10]

template<typename ValueType>

ValueType storm::utility::maximum ( std::vector< ValueType > const & values )

Definition at line 215 of file constants.cpp.

◆ min() [1/2]

template double storm::utility::min	(	double const &	first,
		double const &	second )

◆ min() [2/2]

template<typename ValueType>

ValueType storm::utility::min	(	ValueType const &	first,
		ValueType const &	second )

Definition at line 263 of file constants.cpp.

◆ minimum() [1/10]

template<typename K, typename ValueType>

ValueType storm::utility::minimum ( std::map< K, ValueType > const & values )

Definition at line 243 of file constants.cpp.

◆ minimum() [2/10]

template double storm::utility::minimum ( std::map< uint64_t, double > const & )

◆ minimum() [3/10]

template storm::ExtendedRationalFunction storm::utility::minimum ( std::map< uint64_t, storm::ExtendedRationalFunction > const & values )

◆ minimum() [4/10]

template storm::ExtendedRationalNumber storm::utility::minimum ( std::map< uint64_t, storm::ExtendedRationalNumber > const & values )

◆ minimum() [5/10]

template<>

storm::RationalFunction storm::utility::minimum ( std::map< uint64_t, storm::RationalFunction > const & )

Definition at line 1057 of file constants.cpp.

◆ minimum() [6/10]

template double storm::utility::minimum ( std::vector< double > const & )

◆ minimum() [7/10]

template storm::ExtendedRationalFunction storm::utility::minimum ( std::vector< storm::ExtendedRationalFunction > const & values )

◆ minimum() [8/10]

template storm::ExtendedRationalNumber storm::utility::minimum ( std::vector< storm::ExtendedRationalNumber > const & values )

◆ minimum() [9/10]

template<>

storm::RationalFunction storm::utility::minimum ( std::vector< storm::RationalFunction > const & )

Definition at line 1042 of file constants.cpp.

◆ minimum() [10/10]

template<typename ValueType>

ValueType storm::utility::minimum ( std::vector< ValueType > const & values )

Definition at line 203 of file constants.cpp.

◆ minmax() [1/10]

template<typename K, typename ValueType>

std::pair< ValueType, ValueType > storm::utility::minmax ( std::map< K, ValueType > const & values )

Definition at line 227 of file constants.cpp.

◆ minmax() [2/10]

template std::pair< double, double > storm::utility::minmax ( std::map< uint64_t, double > const & )

◆ minmax() [3/10]

template std::pair< storm::ExtendedRationalFunction, storm::ExtendedRationalFunction > storm::utility::minmax ( std::map< uint64_t, storm::ExtendedRationalFunction > const & values )

◆ minmax() [4/10]

template std::pair< storm::ExtendedRationalNumber, storm::ExtendedRationalNumber > storm::utility::minmax ( std::map< uint64_t, storm::ExtendedRationalNumber > const & values )

◆ minmax() [5/10]

template<>

std::pair< storm::RationalFunction, storm::RationalFunction > storm::utility::minmax ( std::map< uint64_t, storm::RationalFunction > const & )

Definition at line 1052 of file constants.cpp.

◆ minmax() [6/10]

template std::pair< double, double > storm::utility::minmax ( std::vector< double > const & )

◆ minmax() [7/10]

template std::pair< storm::ExtendedRationalFunction, storm::ExtendedRationalFunction > storm::utility::minmax ( std::vector< storm::ExtendedRationalFunction > const & values )

◆ minmax() [8/10]

template std::pair< storm::ExtendedRationalNumber, storm::ExtendedRationalNumber > storm::utility::minmax ( std::vector< storm::ExtendedRationalNumber > const & values )

◆ minmax() [9/10]

template<>

std::pair< storm::RationalFunction, storm::RationalFunction > storm::utility::minmax ( std::vector< storm::RationalFunction > const & )

Definition at line 1037 of file constants.cpp.

◆ minmax() [10/10]

template<typename ValueType>

std::pair< ValueType, ValueType > storm::utility::minmax ( std::vector< ValueType > const & values )

Definition at line 187 of file constants.cpp.

◆ mod() [1/2]

template double storm::utility::mod	(	double const &	first,
		double const &	second )

◆ mod() [2/2]

template<typename IntegerType>

IntegerType storm::utility::mod	(	IntegerType const &	first,
		IntegerType const &	second )

Definition at line 346 of file constants.cpp.

◆ narrow()

template<typename ValueType>

ValueType storm::utility::narrow ( ExtendedValueType< ValueType > const & value )

Narrows an extended value back into the plain value type, for the interfaces that cannot hold an infinite one – a coordinate of a polytope, say.

A plain type that has an infinity of its own keeps the value; one that has none has nothing to narrow an infinite value to, so this throws rather than inventing a number for it.

Definition at line 481 of file ExtendedNumber.h.

◆ narrowFinite() [1/3]

template<typename ValueType>

std::vector< ValueType > storm::utility::narrowFinite ( std::vector< ExtendedValueType< ValueType > > && values )

The counterpart of widen for a vector all of whose values are finite.

The values are taken over rather than copied.

Precondition: none of the values is infinite

Definition at line 424 of file ExtendedNumber.h.

◆ narrowFinite() [2/3]

template<typename ValueType>

std::vector< ValueType > storm::utility::narrowFinite	(	std::vector< ExtendedValueType< ValueType > > &&	values,
		ValueType const &	defaultValue )

The counterpart of widen for a vector, falling back to the given value wherever a value is infinite.

The values are taken over rather than copied.

Definition at line 462 of file ExtendedNumber.h.

◆ narrowFinite() [3/3]

template<typename ValueType>

std::vector< ValueType > storm::utility::narrowFinite ( std::vector< ExtendedValueType< ValueType > > const & values )

The counterpart of widen for a vector all of whose values are finite.

Precondition: none of the values is infinite

Definition at line 443 of file ExtendedNumber.h.

◆ negativeInfinity()

template<typename ValueType>

ExtendedValueType< ValueType > storm::utility::negativeInfinity ( )

Returns: -infinity, expressed in whichever type is used to extend ValueType with infinities.

Definition at line 375 of file ExtendedNumber.h.

◆ numDigits()

template<typename ValueType>

uint64_t storm::utility::numDigits ( ValueType const & number )

Definition at line 314 of file constants.cpp.

◆ numerator()

template<typename RationalType>

NumberTraits< RationalType >::IntegerType storm::utility::numerator ( RationalType const & number )

◆ one() [1/3]

template double storm::utility::one ( )

◆ one() [2/3]

template<typename ValueType>

ValueType storm::utility::one ( )

Definition at line 21 of file constants.cpp.

◆ one() [3/3]

template<typename ValueType>
requires (detail::IsExtendedNumber<ValueType>::value)

ValueType storm::utility::one ( )

Definition at line 597 of file ExtendedNumber.h.

◆ operator<<() [1/2]

std::ostream & storm::utility::operator<<	(	std::ostream &	os,
		Engine const &	engine )

Writes the string representation of the given engine to the given stream.

Definition at line 59 of file Engine.cpp.

◆ operator<<() [2/2]

std::ostream & storm::utility::operator<<	(	std::ostream &	out,
		Stopwatch const &	stopwatch )

Definition at line 68 of file Stopwatch.cpp.

◆ positiveInfinity()

template<typename ValueType>

ExtendedValueType< ValueType > storm::utility::positiveInfinity ( )

Returns: +infinity, expressed in whichever type is used to extend ValueType with infinities.

Definition at line 363 of file ExtendedNumber.h.

◆ pow() [1/5]

template double storm::utility::pow	(	double const &	value,
		int_fast64_t	exponent )

◆ pow() [2/5]

template<>

RationalFunction storm::utility::pow	(	RationalFunction const &	value,
		int_fast64_t	exponent )

Definition at line 1067 of file constants.cpp.

◆ pow() [3/5]

template<>

storm::Interval storm::utility::pow	(	storm::Interval const &	value,
		int_fast64_t	exponent )

Definition at line 1195 of file constants.cpp.

◆ pow() [4/5]

template<>

storm::RationalInterval storm::utility::pow	(	storm::RationalInterval const &	value,
		int_fast64_t	exponent )

Definition at line 1223 of file constants.cpp.

◆ pow() [5/5]

template<typename ValueType>

ValueType storm::utility::pow	(	ValueType const &	value,
		int_fast64_t	exponent )

Definition at line 253 of file constants.cpp.

◆ reverseBits()

template<typename T, bool ReverseBytes = true>

T storm::utility::reverseBits ( T const t )

inline

Swaps the bits in the bit representation of the given value.

Template Parameters

ReverseBytes If true, the byte representation is also swapped (i.e., endianness is swapped)

Definition at line 29 of file bitoperations.h.

◆ round() [1/2]

template double storm::utility::round ( double const & number )

◆ round() [2/2]

template<typename ValueType>

ValueType storm::utility::round ( ValueType const & number )

Definition at line 288 of file constants.cpp.

◆ setLogLevel()

void storm::utility::setLogLevel ( l3pp::LogLevel level )

Set the global log level.

Definition at line 59 of file initialize.cpp.

◆ setOutputDigits()

void storm::utility::setOutputDigits ( int digits )

Set number of digits for printing output.

Parameters

digits Number of digits to print.

Definition at line 28 of file initialize.cpp.

◆ setOutputDigitsFromGeneralPrecision()

void storm::utility::setOutputDigitsFromGeneralPrecision ( double precision )

Set number of digits for printing output from given precision requirement.

For a precision of 1e-n we output at least n digits.

Parameters

precision General precision.

Definition at line 41 of file initialize.cpp.

◆ setProgressLogLevel()

void storm::utility::setProgressLogLevel ( l3pp::LogLevel level )

Set the log level for the progress channel, independently of the global log level.

Definition at line 72 of file initialize.cpp.

◆ setStatisticsLogLevel()

void storm::utility::setStatisticsLogLevel ( l3pp::LogLevel level )

Set the log level for the statistics channel, independently of the global log level.

Definition at line 68 of file initialize.cpp.

◆ setUp()

void storm::utility::setUp ( )

Performs some necessary initializations.

Definition at line 32 of file initialize.cpp.

◆ simplify() [1/9]

template double storm::utility::simplify ( double value )

◆ simplify() [2/9]

template<>

RationalFunction && storm::utility::simplify ( RationalFunction && value )

Definition at line 1003 of file constants.cpp.

◆ simplify() [3/9]

template<>

RationalFunction && storm::utility::simplify ( RationalFunction && value )

Definition at line 1003 of file constants.cpp.

◆ simplify() [4/9]

template<>

RationalFunction & storm::utility::simplify ( RationalFunction & value )

Definition at line 997 of file constants.cpp.

◆ simplify() [5/9]

template<>

RationalFunction & storm::utility::simplify ( RationalFunction & value )

Definition at line 997 of file constants.cpp.

◆ simplify() [6/9]

template<>

RationalFunction storm::utility::simplify ( RationalFunction value )

Definition at line 991 of file constants.cpp.

◆ simplify() [7/9]

template<typename IndexType, typename ValueType>

storm::storage::MatrixEntry< IndexType, ValueType > && storm::utility::simplify ( storm::storage::MatrixEntry< IndexType, ValueType > && matrixEntry )

◆ simplify() [8/9]

template<typename IndexType, typename ValueType>

storm::storage::MatrixEntry< IndexType, ValueType > & storm::utility::simplify ( storm::storage::MatrixEntry< IndexType, ValueType > & matrixEntry )

◆ simplify() [9/9]

template<typename ValueType>

ValueType storm::utility::simplify ( ValueType value )

Definition at line 180 of file constants.cpp.

◆ sin() [1/2]

template double storm::utility::sin ( double const & number )

◆ sin() [2/2]

template<typename ValueType>

ValueType storm::utility::sin ( ValueType const & number )

Definition at line 309 of file constants.cpp.

◆ sqrt() [1/2]

template double storm::utility::sqrt ( double const & number )

◆ sqrt() [2/2]

template<typename ValueType>

ValueType storm::utility::sqrt ( ValueType const & number )

Definition at line 268 of file constants.cpp.

◆ to_string() [1/5]

template std::string storm::utility::to_string ( double const & value )

◆ to_string() [2/5]

template<>

std::string storm::utility::to_string ( RationalFunction const & f )

Definition at line 1076 of file constants.cpp.

◆ to_string() [3/5]

template std::string storm::utility::to_string ( storm::Interval const & value )

◆ to_string() [4/5]

template std::string storm::utility::to_string ( storm::RationalInterval const & value )

◆ to_string() [5/5]

template<typename ValueType>

std::string storm::utility::to_string ( ValueType const & value )

Definition at line 366 of file constants.cpp.

◆ toSentinel()

template<typename ValueType>

ValueType storm::utility::toSentinel ( ExtendedValueType< ValueType > const & value )

The counterpart of fromSentinel: hands an extended value back to a part of Storm that still expects the sentinel, most of all a decision diagram leaf.

The sentinel has no negative infinity, so that direction is rejected rather than silently turned into something else.

Definition at line 570 of file ExtendedNumber.h.

◆ toString()

std::string storm::utility::toString ( Engine const & engine )

Returns a string representation of the given engine.

Definition at line 35 of file Engine.cpp.

◆ trunc() [1/2]

template NumberTraits< double >::IntegerType storm::utility::trunc ( double const & number )

◆ trunc() [2/2]

template<typename ValueType>

NumberTraits< ValueType >::IntegerType storm::utility::trunc ( ValueType const & number )

Definition at line 341 of file constants.cpp.

◆ tryParseNumber()

template<typename RationalType>

bool storm::utility::tryParseNumber	(	std::string const &	input,
		RationalType &	result )

Tries to parse a number from its string representation.

Parameters

input	String representation of the number.
result	The parsed number (only valid if parsing succeeded).

Returns: True iff the string could be parsed as a number of the given type.

◆ widen()

template<typename ValueType>

std::vector< ExtendedValueType< ValueType > > storm::utility::widen ( std::vector< ValueType > && values )

Widens a vector of finite values into the extended value type.

Used where a computation that cannot produce an infinite value feeds an interface that can hold one.

Definition at line 496 of file ExtendedNumber.h.

◆ zero() [1/3]

template double storm::utility::zero ( )

◆ zero() [2/3]

template<typename ValueType>

ValueType storm::utility::zero ( )

Definition at line 26 of file constants.cpp.

◆ zero() [3/3]

template<typename ValueType>
requires (detail::IsExtendedNumber<ValueType>::value)

ValueType storm::utility::zero ( )

The generic storm::utility::zero, one and infinity are declared for every value type but defined only for the ones that are explicitly instantiated.

These overloads are more constrained than those declarations, so they are picked for the extended types and the extended types alone.

Definition at line 591 of file ExtendedNumber.h.

Variable Documentation

◆ defaultProgressMeasurementDelay

uint64_t storm::utility::defaultProgressMeasurementDelay = 5

constexpr

Definition at line 12 of file ProgressMeasurement.h.

◆ PROGRESS_LOG_CHANNEL

const char* storm::utility::PROGRESS_LOG_CHANNEL = "storm.progress"

constexpr

Definition at line 42 of file logging.h.

◆ STATISTICS_LOG_CHANNEL

const char* storm::utility::STATISTICS_LOG_CHANNEL = "storm.statistics"

constexpr

Definition at line 41 of file logging.h.

Namespaces

Classes

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

◆ ElementGreater

◆ ElementLess

◆ ExtendedValueType

◆ FiniteValueType

◆ Maximum

◆ Minimum

Enumeration Type Documentation

◆ Engine

Function Documentation

◆ abs() [1/5]

◆ abs() [2/5]

◆ abs() [3/5]

◆ abs() [4/5]

◆ abs() [5/5]

◆ bitsize() [1/2]

◆ bitsize() [2/2]

◆ byteSwap()

◆ canHandle() [1/2]

◆ canHandle() [2/2]

◆ canHandle< double >()

◆ canHandle< storm::RationalFunction >() [1/2]

◆ canHandle< storm::RationalFunction >() [2/2]

◆ canHandle< storm::RationalNumber >()

◆ ceil() [1/2]

◆ ceil() [2/2]

◆ cleanUp()

◆ convertNumber() [1/28]

◆ convertNumber() [2/28]

◆ convertNumber() [3/28]

◆ convertNumber() [4/28]

◆ convertNumber() [5/28]

◆ convertNumber() [6/28]

◆ convertNumber() [7/28]

◆ convertNumber() [8/28]

◆ convertNumber() [9/28]

◆ convertNumber() [10/28]

◆ convertNumber() [11/28]

◆ convertNumber() [12/28]

◆ convertNumber() [13/28]

◆ convertNumber() [14/28]

◆ convertNumber() [15/28]

◆ convertNumber() [16/28]

◆ convertNumber() [17/28]

◆ convertNumber() [18/28]

◆ convertNumber() [19/28]

◆ convertNumber() [20/28]

◆ convertNumber() [21/28]

◆ convertNumber() [22/28]

◆ convertNumber() [23/28]

◆ convertNumber() [24/28]

◆ convertNumber() [25/28]

◆ convertNumber() [26/28]

◆ convertNumber() [27/28]

◆ convertNumber() [28/28]

◆ cos() [1/2]

◆ cos() [2/2]

◆ createFilteredRewardModel() [1/3]

◆ createFilteredRewardModel() [2/3]

◆ createFilteredRewardModel() [3/3]

◆ denominator()

◆ divide()

◆ engineFromString()

◆ findPerfectMatching()

◆ findRational()

◆ floor() [1/2]

◆ floor() [2/2]

◆ fromSentinel() [1/3]

◆ fromSentinel() [2/3]

◆ fromSentinel() [3/3]

◆ gcd()

◆ getBuilderType()

◆ getEngines()

◆ getFinite() [1/2]