Classes
class	ExpressionEvaluator
class	BaseExpression
	The base class of all expression classes. More...
class	BinaryBooleanFunctionExpression
class	BinaryExpression
	The base class of all binary expressions. More...
class	BinaryNumericalFunctionExpression
class	BinaryRelationExpression
class	BooleanLiteralExpression
class	ChangeManagerVisitor
class	CheckIfThenElseGuardVisitor
class	CompiledExpression
class	EquivalenceChecker
class	Expression
struct	ExpressionLess
class	ExpressionEvaluator< double >
class	ExpressionEvaluatorWithVariableToExpressionMap
class	ExpressionEvaluator< RationalNumber >
class	ExpressionEvaluator< RationalFunction >
class	ExpressionEvaluatorBase
class	VariableIterator
class	ExpressionManager
	This class is responsible for managing a set of typed variables and all expressions using these variables. More...
class	ExpressionVisitor
class	ExprtkCompiledExpression
class	ExprtkExpressionEvaluatorBase
class	ExprtkExpressionEvaluator
class	FullPredicateSplitter
class	HashVisitor
	Computes a hash of an expression such that syntactically equal expressions hash to the same value. More...
class	IfThenElseExpression
class	IntegerLiteralExpression
class	LinearCoefficientVisitor
	Computes the coefficients of a linear expression. More...
class	LinearityCheckVisitor
class	PredicateExpression
	The base class of all binary expressions. More...
class	RationalFunctionToExpression
class	RationalLiteralExpression
class	ReduceNestingVisitor
class	RestrictSyntaxVisitor
class	SimpleValuation
	A simple implementation of the valuation interface. More...
class	SimpleValuationPointerHash
	A helper class that can pe used as the hash functor for data structures that need to hash valuations given via pointers. More...
class	SimpleValuationPointerCompare
	A helper class that can be used as the comparison functor wrt. More...
class	SimpleValuationPointerLess
	A helper class that can be used as the comparison functor wrt. More...
class	SubstitutionVisitor
class	SyntacticalEqualityCheckVisitor
class	ToDiceStringVisitor
class	ToExprtkStringVisitor
class	ToRationalFunctionVisitor
class	ToRationalNumberVisitor
class	Type
class	BaseType
class	BooleanType
class	IntegerType
class	BitVectorType
class	RationalType
class	ArrayType
class	TranscendentalNumberType
class	StringType
class	ErrorType
class	UnaryBooleanFunctionExpression
class	UnaryExpression
class	UnaryNumericalFunctionExpression
class	Valuation
	The base class of all valuations of variables. More...
class	Variable
class	VariableExpression
class	VariableSetPredicateSplitter
class	ArrayAccessExpression
	Represents an access to an array. More...
class	ArrayExpression
	The base class of all array expressions. More...
class	ConstructorArrayExpression
	Represents an array of the given size, where the i'th entry is determined by the elementExpression, where occurrences of indexVar will be substituted by i. More...
class	FunctionCallExpression
	Represents an array with a given list of elements. More...
class	TranscendentalNumberLiteralExpression
class	ValueArrayExpression
	Represents an array with a given list of elements. More...
class	JaniExpressionSubstitutionVisitor
class	JaniExpressionVisitor
class	JaniReduceNestingExpressionVisitor
class	JaniSyntacticalEqualityCheckVisitor

Typedefs
using	ExpressionComparator = std::less<Expression>
using	ExpressionSet = std::set<Expression, ExpressionComparator>
template<typename Value>
using	ExpressionMap = std::map<Expression, Value, ExpressionComparator>

Enumerations
enum class	RelationType { Equal , NotEqual , Less , LessOrEqual , Greater , GreaterOrEqual }
	An enum type specifying the different relations applicable. More...
enum class	OperatorType { And , Or , Xor , Implies , Iff , Plus , Minus , Times , Divide , Min , Max , Power , Modulo , Logarithm , Cos , Sin , Equal , NotEqual , Less , LessOrEqual , Greater , GreaterOrEqual , Not , Floor , Ceil , Ite , AtLeastOneOf , AtMostOneOf , ExactlyOneOf }

Functions
std::ostream &	operator<< (std::ostream &stream, BaseExpression const &expression)
template<typename V>
V	logHelper (V const &x, V const &b)
static void	assertSameManager (BaseExpression const &a, BaseExpression const &b)
	Checks whether the two expressions share the same expression manager.
std::ostream &	operator<< (std::ostream &stream, Expression const &expression)
Expression	operator+ (Expression const &first, Expression const &second)
Expression	operator+ (Expression const &first, int64_t second)
Expression	operator+ (int64_t first, Expression const &second)
Expression	operator- (Expression const &first, Expression const &second)
Expression	operator- (Expression const &first, int64_t second)
Expression	operator- (int64_t first, Expression const &second)
Expression	operator- (Expression const &first)
Expression	operator* (Expression const &first, Expression const &second)
Expression	operator/ (Expression const &first, Expression const &second)
Expression	operator% (Expression const &first, Expression const &second)
Expression	operator&& (Expression const &first, Expression const &second)
Expression	operator\|\| (Expression const &first, Expression const &second)
Expression	operator! (Expression const &first)
Expression	operator== (Expression const &first, Expression const &second)
Expression	operator!= (Expression const &first, Expression const &second)
Expression	operator> (Expression const &first, Expression const &second)
Expression	operator>= (Expression const &first, Expression const &second)
Expression	operator< (Expression const &first, Expression const &second)
Expression	operator<= (Expression const &first, Expression const &second)
Expression	operator< (Expression const &first, int64_t second)
Expression	operator> (Expression const &first, int64_t second)
Expression	operator<= (Expression const &first, int64_t second)
Expression	operator>= (Expression const &first, int64_t second)
Expression	minimum (Expression const &first, Expression const &second)
Expression	maximum (Expression const &first, Expression const &second)
Expression	ite (Expression const &condition, Expression const &thenExpression, Expression const &elseExpression)
Expression	implies (Expression const &first, Expression const &second)
Expression	iff (Expression const &first, Expression const &second)
Expression	xclusiveor (Expression const &first, Expression const &second)
Expression	pow (Expression const &base, Expression const &exponent, bool allowIntegerType=false)
	The type of the resulting expression is.
Expression	floor (Expression const &first)
Expression	ceil (Expression const &first)
Expression	round (Expression const &first)
Expression	abs (Expression const &first)
Expression	sign (Expression const &first)
Expression	truncate (Expression const &first)
Expression	atLeastOneOf (std::vector< Expression > const &expressions)
Expression	atMostOneOf (std::vector< Expression > const &expressions)
Expression	exactlyOneOf (std::vector< Expression > const &expressions)
Expression	disjunction (std::vector< storm::expressions::Expression > const &expressions)
Expression	conjunction (std::vector< storm::expressions::Expression > const &expressions)
Expression	sum (std::vector< storm::expressions::Expression > const &expressions)
Expression	product (std::vector< storm::expressions::Expression > const &expressions)
Expression	modulo (Expression const &first, Expression const &second)
Expression	logarithm (Expression const &first, Expression const &second)
Expression	cos (Expression const &first)
Expression	sin (Expression const &first)
Expression	apply (std::vector< storm::expressions::Expression > const &expressions, std::function< Expression(Expression const &, Expression const &)> const &function)
Expression	makeBinaryRelationExpression (Expression const &first, Expression const &second, RelationType const &reltype)
Expression	applyAssociative (std::vector< storm::expressions::Expression > const &expressions, std::function< Expression(Expression const &, Expression const &)> const &function)
Expression	atLeastOneOf (std::vector< storm::expressions::Expression > const &expressions)
Expression	atMostOneOf (std::vector< storm::expressions::Expression > const &expressions)
Expression	exactlyOneOf (std::vector< storm::expressions::Expression > const &expressions)
std::ostream &	operator<< (std::ostream &out, ExpressionManager const &manager)
std::vector< storm::expressions::Expression > &	getAtomicExpressions (boost::any const &data)
std::ostream &	operator<< (std::ostream &stream, OperatorType const &operatorType)
template<typename PolynomialType>
Expression	polynomialToExpression (PolynomialType const &polynomial, std::shared_ptr< ExpressionManager > const &manager)
	Converts the given polynomial into a Storm expression.
OperatorType	toOperatorType (PredicateExpression::PredicateType tp)
template<typename BinaryFunc>
std::vector< std::shared_ptr< BaseExpression const > >	getAllOperands (BinaryFunc const &binaryExpression)
std::ostream &	operator<< (std::ostream &out, SimpleValuation const &valuation)
bool	operator< (BaseType const &first, BaseType const &second)
bool	operator< (storm::expressions::Type const &type1, storm::expressions::Type const &type2)
std::ostream &	operator<< (std::ostream &stream, Type const &type)

Typedef Documentation

◆ ExpressionComparator

using storm::expressions::ExpressionComparator = std::less<Expression>

Definition at line 513 of file Expression.h.

◆ ExpressionMap

template<typename Value>

using storm::expressions::ExpressionMap = std::map<Expression, Value, ExpressionComparator>

Definition at line 517 of file Expression.h.

◆ ExpressionSet

using storm::expressions::ExpressionSet = std::set<Expression, ExpressionComparator>

Definition at line 515 of file Expression.h.

Enumeration Type Documentation

◆ OperatorType

enum class storm::expressions::OperatorType

strong

Enumerator
And
Or
Xor
Implies
Iff
Plus
Minus
Times
Divide
Min
Max
Power
Modulo
Logarithm
Cos
Sin
Equal
NotEqual
Less
LessOrEqual
Greater
GreaterOrEqual
Not
Floor
Ceil
Ite
AtLeastOneOf
AtMostOneOf
ExactlyOneOf

Definition at line 8 of file OperatorType.h.

◆ RelationType

enum class storm::expressions::RelationType

strong

An enum type specifying the different relations applicable.

Enumerator
Equal
NotEqual
Less
LessOrEqual
Greater
GreaterOrEqual

Definition at line 7 of file BinaryRelationType.h.

Function Documentation

◆ abs()

Expression storm::expressions::abs ( Expression const & first )

Definition at line 480 of file Expression.cpp.

◆ apply()

Expression storm::expressions::apply	(	std::vector< storm::expressions::Expression > const &	expressions,
		std::function< Expression(Expression const &, Expression const &)> const &	function )

Definition at line 569 of file Expression.cpp.

◆ applyAssociative()

Expression storm::expressions::applyAssociative	(	std::vector< storm::expressions::Expression > const &	expressions,
		std::function< Expression(Expression const &, Expression const &)> const &	function )

Definition at line 591 of file Expression.cpp.

◆ assertSameManager()

void storm::expressions::assertSameManager	(	BaseExpression const &	a,
		BaseExpression const &	b )

static

Checks whether the two expressions share the same expression manager.

Parameters

a	The first expression.
b	The second expression.

Returns: True iff the expressions share the same manager.

Definition at line 28 of file Expression.cpp.

◆ atLeastOneOf() [1/2]

Expression storm::expressions::atLeastOneOf ( std::vector< Expression > const & expressions )

Definition at line 495 of file Expression.cpp.

◆ atLeastOneOf() [2/2]

Expression storm::expressions::atLeastOneOf ( std::vector< storm::expressions::Expression > const & expressions )

◆ atMostOneOf() [1/2]

Expression storm::expressions::atMostOneOf ( std::vector< Expression > const & expressions )

Definition at line 506 of file Expression.cpp.

◆ atMostOneOf() [2/2]

Expression storm::expressions::atMostOneOf ( std::vector< storm::expressions::Expression > const & expressions )

◆ ceil()

Expression storm::expressions::ceil ( Expression const & first )

Definition at line 468 of file Expression.cpp.

◆ conjunction()

Expression storm::expressions::conjunction ( std::vector< storm::expressions::Expression > const & expressions )

Definition at line 532 of file Expression.cpp.

◆ cos()

Expression storm::expressions::cos ( Expression const & first )

Definition at line 555 of file Expression.cpp.

◆ disjunction()

Expression storm::expressions::disjunction ( std::vector< storm::expressions::Expression > const & expressions )

Definition at line 528 of file Expression.cpp.

◆ exactlyOneOf() [1/2]

Expression storm::expressions::exactlyOneOf ( std::vector< Expression > const & expressions )

Definition at line 517 of file Expression.cpp.

◆ exactlyOneOf() [2/2]

Expression storm::expressions::exactlyOneOf ( std::vector< storm::expressions::Expression > const & expressions )

◆ floor()

Expression storm::expressions::floor ( Expression const & first )

Definition at line 461 of file Expression.cpp.

◆ getAllOperands()

template<typename BinaryFunc>

std::vector< std::shared_ptr< BaseExpression const > > storm::expressions::getAllOperands ( BinaryFunc const & binaryExpression )

Definition at line 36 of file ReduceNestingVisitor.cpp.

◆ getAtomicExpressions()

std::vector< storm::expressions::Expression > & storm::expressions::getAtomicExpressions ( boost::any const & data )

Definition at line 12 of file FullPredicateSplitter.cpp.

◆ iff()

Expression storm::expressions::iff	(	Expression const &	first,
		Expression const &	second )

Definition at line 440 of file Expression.cpp.

◆ implies()

Expression storm::expressions::implies	(	Expression const &	first,
		Expression const &	second )

Definition at line 433 of file Expression.cpp.

◆ ite()

Expression storm::expressions::ite	(	Expression const &	condition,
		Expression const &	thenExpression,
		Expression const &	elseExpression )

Definition at line 425 of file Expression.cpp.

◆ logarithm()

Expression storm::expressions::logarithm	(	Expression const &	first,
		Expression const &	second )

Definition at line 548 of file Expression.cpp.

◆ logHelper()

template<typename V>

V storm::expressions::logHelper	(	V const &	x,
		V const &	b )

Definition at line 65 of file BinaryNumericalFunctionExpression.cpp.

◆ makeBinaryRelationExpression()

Expression storm::expressions::makeBinaryRelationExpression	(	Expression const &	first,
		Expression const &	second,
		RelationType const &	reltype )

Definition at line 584 of file Expression.cpp.

◆ maximum()

Expression storm::expressions::maximum	(	Expression const &	first,
		Expression const &	second )

Definition at line 418 of file Expression.cpp.

◆ minimum()

Expression storm::expressions::minimum	(	Expression const &	first,
		Expression const &	second )

Definition at line 411 of file Expression.cpp.

◆ modulo()

Expression storm::expressions::modulo	(	Expression const &	first,
		Expression const &	second )

Definition at line 544 of file Expression.cpp.

◆ operator!()

Expression storm::expressions::operator! ( Expression const & first )

Definition at line 341 of file Expression.cpp.

◆ operator!=()

Expression storm::expressions::operator!=	(	Expression const &	first,
		Expression const &	second )

Definition at line 354 of file Expression.cpp.

◆ operator%()

Expression storm::expressions::operator%	(	Expression const &	first,
		Expression const &	second )

Definition at line 306 of file Expression.cpp.

◆ operator&&()

Expression storm::expressions::operator&&	(	Expression const &	first,
		Expression const &	second )

Definition at line 317 of file Expression.cpp.

◆ operator*()

Expression storm::expressions::operator*	(	Expression const &	first,
		Expression const &	second )

Definition at line 292 of file Expression.cpp.

◆ operator+() [1/3]

Expression storm::expressions::operator+	(	Expression const &	first,
		Expression const &	second )

Definition at line 251 of file Expression.cpp.

◆ operator+() [2/3]

Expression storm::expressions::operator+	(	Expression const &	first,
		int64_t	second )

Definition at line 263 of file Expression.cpp.

◆ operator+() [3/3]

Expression storm::expressions::operator+	(	int64_t	first,
		Expression const &	second )

Definition at line 267 of file Expression.cpp.

◆ operator-() [1/4]

Expression storm::expressions::operator- ( Expression const & first )

Definition at line 286 of file Expression.cpp.

◆ operator-() [2/4]

Expression storm::expressions::operator-	(	Expression const &	first,
		Expression const &	second )

Definition at line 271 of file Expression.cpp.

◆ operator-() [3/4]

Expression storm::expressions::operator-	(	Expression const &	first,
		int64_t	second )

Definition at line 278 of file Expression.cpp.

◆ operator-() [4/4]

Expression storm::expressions::operator-	(	int64_t	first,
		Expression const &	second )

Definition at line 282 of file Expression.cpp.

◆ operator/()

Expression storm::expressions::operator/	(	Expression const &	first,
		Expression const &	second )

Definition at line 299 of file Expression.cpp.

◆ operator<() [1/4]

bool storm::expressions::operator<	(	BaseType const &	first,
		BaseType const &	second )

Definition at line 165 of file Type.cpp.

◆ operator<() [2/4]

Expression storm::expressions::operator<	(	Expression const &	first,
		Expression const &	second )

Definition at line 381 of file Expression.cpp.

◆ operator<() [3/4]

Expression storm::expressions::operator<	(	Expression const &	first,
		int64_t	second )

Definition at line 395 of file Expression.cpp.

◆ operator<() [4/4]

bool storm::expressions::operator<	(	storm::expressions::Type const &	type1,
		storm::expressions::Type const &	type2 )

Definition at line 320 of file Type.cpp.

◆ operator<<() [1/6]

std::ostream & storm::expressions::operator<<	(	std::ostream &	out,
		ExpressionManager const &	manager )

Definition at line 353 of file ExpressionManager.cpp.

◆ operator<<() [2/6]

std::ostream & storm::expressions::operator<<	(	std::ostream &	out,
		SimpleValuation const &	valuation )

Definition at line 206 of file SimpleValuation.cpp.

◆ operator<<() [3/6]

std::ostream & storm::expressions::operator<<	(	std::ostream &	stream,
		BaseExpression const &	expression )

Definition at line 205 of file BaseExpression.cpp.

◆ operator<<() [4/6]

std::ostream & storm::expressions::operator<<	(	std::ostream &	stream,
		Expression const &	expression )

Definition at line 242 of file Expression.cpp.

◆ operator<<() [5/6]

std::ostream & storm::expressions::operator<<	(	std::ostream &	stream,
		OperatorType const &	operatorType )

Definition at line 6 of file OperatorType.cpp.

◆ operator<<() [6/6]

std::ostream & storm::expressions::operator<<	(	std::ostream &	stream,
		Type const &	type )

Definition at line 324 of file Type.cpp.

◆ operator<=() [1/2]

Expression storm::expressions::operator<=	(	Expression const &	first,
		Expression const &	second )

Definition at line 388 of file Expression.cpp.

◆ operator<=() [2/2]

Expression storm::expressions::operator<=	(	Expression const &	first,
		int64_t	second )

Definition at line 403 of file Expression.cpp.

◆ operator==()

Expression storm::expressions::operator==	(	Expression const &	first,
		Expression const &	second )

Definition at line 347 of file Expression.cpp.

◆ operator>() [1/2]

Expression storm::expressions::operator>	(	Expression const &	first,
		Expression const &	second )

Definition at line 367 of file Expression.cpp.

◆ operator>() [2/2]

Expression storm::expressions::operator>	(	Expression const &	first,
		int64_t	second )

Definition at line 399 of file Expression.cpp.

◆ operator>=() [1/2]

Expression storm::expressions::operator>=	(	Expression const &	first,
		Expression const &	second )

Definition at line 374 of file Expression.cpp.

◆ operator>=() [2/2]

Expression storm::expressions::operator>=	(	Expression const &	first,
		int64_t	second )

Definition at line 407 of file Expression.cpp.

◆ operator||()

Expression storm::expressions::operator\|\|	(	Expression const &	first,
		Expression const &	second )

Definition at line 329 of file Expression.cpp.

◆ polynomialToExpression()

template<typename PolynomialType>

Expression storm::expressions::polynomialToExpression	(	PolynomialType const &	polynomial,
		std::shared_ptr< ExpressionManager > const &	manager )

Converts the given polynomial into a Storm expression.

The coefficients of the polynomial are converted to rational literals and every variable occurring in the polynomial is looked up in (or declared in) the given expression manager. The mapping from the polynomial's variables to the expression manager's variables is performed by name, which mirrors the mapping performed by storm::expressions::ToRationalFunctionVisitor.

Parameters

polynomial	The polynomial to convert.
manager	The expression manager that owns the resulting expression. Variables occurring in the polynomial are declared in this manager if they are not known yet.

Returns: The expression representing the given polynomial.

Definition at line 28 of file PolynomialToExpression.h.

◆ pow()

Expression storm::expressions::pow	(	Expression const &	base,
		Expression const &	exponent,
		bool	allowIntegerType = false )

The type of the resulting expression is.

integer, if base and exponent are integer expressions and allowIntegerType is true (in this case it is assumed that exponent is always positive), and
rational, otherwise. The integer case is to reflect the PRISM semantics
See also
https://github.com/ahartmanns/qcomp/issues/103

Definition at line 454 of file Expression.cpp.

◆ product()

Expression storm::expressions::product ( std::vector< storm::expressions::Expression > const & expressions )

Definition at line 540 of file Expression.cpp.

◆ round()

Expression storm::expressions::round ( Expression const & first )

Definition at line 475 of file Expression.cpp.

◆ sign()

Expression storm::expressions::sign ( Expression const & first )

Definition at line 485 of file Expression.cpp.

◆ sin()

Expression storm::expressions::sin ( Expression const & first )

Definition at line 562 of file Expression.cpp.

◆ sum()

Expression storm::expressions::sum ( std::vector< storm::expressions::Expression > const & expressions )

Definition at line 536 of file Expression.cpp.

◆ toOperatorType()

OperatorType storm::expressions::toOperatorType ( PredicateExpression::PredicateType tp )

Definition at line 12 of file PredicateExpression.cpp.

◆ truncate()

Expression storm::expressions::truncate ( Expression const & first )

Definition at line 490 of file Expression.cpp.

◆ xclusiveor()

Expression storm::expressions::xclusiveor	(	Expression const &	first,
		Expression const &	second )

Definition at line 447 of file Expression.cpp.

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ ExpressionComparator

◆ ExpressionMap

◆ ExpressionSet

Enumeration Type Documentation

◆ OperatorType

◆ RelationType

Function Documentation

◆ abs()

◆ apply()

◆ applyAssociative()

◆ assertSameManager()

◆ atLeastOneOf() [1/2]

◆ atLeastOneOf() [2/2]

◆ atMostOneOf() [1/2]

◆ atMostOneOf() [2/2]

◆ ceil()

◆ conjunction()

◆ cos()

◆ disjunction()

◆ exactlyOneOf() [1/2]

◆ exactlyOneOf() [2/2]

◆ floor()

◆ getAllOperands()

◆ getAtomicExpressions()

◆ iff()

◆ implies()

◆ ite()

◆ logarithm()

◆ logHelper()

◆ makeBinaryRelationExpression()

◆ maximum()

◆ minimum()

◆ modulo()

◆ operator!()

◆ operator!=()

◆ operator%()

◆ operator&&()

◆ operator*()

◆ operator+() [1/3]

◆ operator+() [2/3]

◆ operator+() [3/3]

◆ operator-() [1/4]

◆ operator-() [2/4]

◆ operator-() [3/4]

◆ operator-() [4/4]

◆ operator/()

◆ operator<() [1/4]

◆ operator<() [2/4]

◆ operator<() [3/4]

◆ operator<() [4/4]

◆ operator<<() [1/6]

◆ operator<<() [2/6]

◆ operator<<() [3/6]

◆ operator<<() [4/6]

◆ operator<<() [5/6]

◆ operator<<() [6/6]

◆ operator<=() [1/2]

◆ operator<=() [2/2]

◆ operator==()

◆ operator>() [1/2]

◆ operator>() [2/2]

◆ operator>=() [1/2]

◆ operator>=() [2/2]

◆ operator||()

◆ polynomialToExpression()

◆ pow()

◆ product()

◆ round()

◆ sign()

◆ sin()

◆ sum()

◆ toOperatorType()

◆ truncate()

◆ xclusiveor()