storm::expressions Namespace Reference

Classes
class	ArrayAccessExpression
	Represents an access to an array. More...
class	ArrayExpression
	The base class of all array expressions. More...
class	ArrayType
class	BaseExpression
	The base class of all expression classes. More...
class	BaseType
class	BinaryBooleanFunctionExpression
class	BinaryExpression
	The base class of all binary expressions. More...
class	BinaryNumericalFunctionExpression
class	BinaryRelationExpression
class	BitVectorType
class	BooleanLiteralExpression
class	BooleanType
class	ChangeManagerVisitor
class	CheckIfThenElseGuardVisitor
class	CompiledExpression
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	EquivalenceChecker
class	ErrorType
class	Expression
class	ExpressionEvaluator
class	ExpressionEvaluator< double >
class	ExpressionEvaluatorBase
class	ExpressionEvaluatorWithVariableToExpressionMap
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	ExprtkExpressionEvaluator
class	ExprtkExpressionEvaluatorBase
class	FullPredicateSplitter
class	FunctionCallExpression
	Represents an array with a given list of elements. More...
class	IfThenElseExpression
class	IntegerLiteralExpression
class	IntegerType
class	JaniExpressionSubstitutionVisitor
class	JaniExpressionVisitor
class	JaniReduceNestingExpressionVisitor
class	JaniSyntacticalEqualityCheckVisitor
class	LinearCoefficientVisitor
class	LinearityCheckVisitor
class	PredicateExpression
	The base class of all binary expressions. More...
class	RationalFunctionToExpression
class	RationalLiteralExpression
class	RationalType
class	ReduceNestingVisitor
class	RestrictSyntaxVisitor
class	SimpleValuation
	A simple implementation of the valuation interface. More...
class	SimpleValuationPointerCompare
	A helper class that can be used as the comparison functor wrt. 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	SimpleValuationPointerLess
	A helper class that can be used as the comparison functor wrt. More...
class	SubstitutionVisitor
class	SyntacticalEqualityCheckVisitor
class	ToCppTranslationOptions
class	ToCppVisitor
class	ToDiceStringVisitor
class	ToExprtkStringVisitor
class	ToRationalNumberVisitor
class	TranscendentalNumberLiteralExpression
class	TranscendentalNumberType
class	Type
class	UnaryBooleanFunctionExpression
class	UnaryExpression
class	UnaryNumericalFunctionExpression
class	Valuation
	The base class of all valuations of variables. More...
class	ValueArrayExpression
	Represents an array with a given list of elements. More...
class	Variable
class	VariableExpression
class	VariableIterator
class	VariableSetPredicateSplitter

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 }
enum class	ToCppTranslationMode { KeepType , CastDouble , CastRationalNumber , CastRationalFunction }

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	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)
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)
std::string	getVariableName (storm::expressions::Variable const &variable, std::unordered_map< storm::expressions::Variable, std::string > const &prefixes, std::unordered_map< storm::expressions::Variable, std::string > const &names)
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)

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 9 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.

ToCppTranslationMode

enum class storm::expressions::ToCppTranslationMode

strong

Enumerator
KeepType
CastDouble
CastRationalNumber
CastRationalFunction

Definition at line 13 of file ToCppVisitor.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 565 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 587 of file Expression.cpp.

assertSameManager()

static 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 551 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.

getVariableName()

std::string storm::expressions::getVariableName	(	storm::expressions::Variable const &	variable,
		std::unordered_map< storm::expressions::Variable, std::string > const &	prefixes,
		std::unordered_map< storm::expressions::Variable, std::string > const &	names
	)

Definition at line 210 of file ToCppVisitor.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 544 of file Expression.cpp.

logHelper()

template<typename V >

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

Definition at line 66 of file BinaryNumericalFunctionExpression.cpp.

makeBinaryRelationExpression()

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

Definition at line 580 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 540 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 149 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 301 of file Type.cpp.

operator<<() [1/6]

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

Definition at line 338 of file ExpressionManager.cpp.

operator<<() [2/6]

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

Definition at line 170 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 305 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.

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.

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 558 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.