This class is responsible for managing a set of typed variables and all expressions using these variables. More...

#include <ExpressionManager.h>

Inheritance diagram for storm::expressions::ExpressionManager:

Collaboration diagram for storm::expressions::ExpressionManager:

Public Types
typedef VariableIterator	const_iterator

Public Member Functions
	ExpressionManager ()
	Creates a new manager that is unaware of any variables.

	~ExpressionManager ()

std::shared_ptr< ExpressionManager >	clone () const
	Creates a new expression manager with the same set of variables.

	ExpressionManager (ExpressionManager &&other)=default

ExpressionManager &	operator= (ExpressionManager &&other)=default

Expression	boolean (bool value) const
	Creates an expression that characterizes the given boolean literal.

Expression	integer (int_fast64_t value) const
	Creates an expression that characterizes the given integer literal.

Expression	rational (double value) const
	Creates an expression that characterizes the given rational literal.

Expression	rational (storm::RationalNumber const &value) const
	Creates an expression that characterizes the given rational literal.

bool	operator== (ExpressionManager const &other) const
	Compares the two expression managers for equality, which holds iff they are the very same object.

Type const &	getBooleanType () const
	Retrieves the boolean type.

Type const &	getIntegerType () const
	Retrieves the unbounded integer type.

Type const &	getBitVectorType (std::size_t width) const
	Retrieves the bit vector type of the given width.

Type const &	getRationalType () const
	Retrieves the rational type.

Type const &	getArrayType (Type elementType) const
	Retrieves the array type with the given element type.

Type const &	getTranscendentalNumberType () const
	Retrieves the transcendental numbers type (i.e.

Variable	declareVariableCopy (Variable const &variable)
	Declares a variable that is a copy of the provided variable (i.e.

Variable	declareVariable (std::string const &name, storm::expressions::Type const &variableType, bool auxiliary=false)
	Declares a variable with a name that must not yet exist and its corresponding type.

Variable	declareBooleanVariable (std::string const &name, bool auxiliary=false)
	Declares a new boolean variable with a name that must not yet exist and its corresponding type.

Variable	declareIntegerVariable (std::string const &name, bool auxiliary=false)
	Declares a new integer variable with a name that must not yet exist and its corresponding type.

Variable	declareBitVectorVariable (std::string const &name, std::size_t width, bool auxiliary=false)
	Declares a new bit vector variable with a name that must not yet exist and the bounded type of the given bit width.

Variable	declareRationalVariable (std::string const &name, bool auxiliary=false)
	Declares a new rational variable with a name that must not yet exist and its corresponding type.

Variable	declareArrayVariable (std::string const &name, Type const &elementType, bool auxiliary=false)
	Declares a new array variable with the given name and the given element type.

Variable	declareOrGetVariable (std::string const &name, storm::expressions::Type const &variableType, bool auxiliary=false)
	Declares a variable with the given name if it does not yet exist.

Variable	getVariable (std::string const &name) const
	Retrieves the expression that represents the variable with the given name.

std::set< Variable > const &	getVariables () const
	Retrieves the set of all variables known to this manager.

bool	hasVariable (std::string const &name) const
	Retrieves whether a variable with the given name is known to the manager.

Expression	getVariableExpression (std::string const &name) const
	Retrieves an expression that represents the variable with the given name.

Variable	declareFreshVariable (storm::expressions::Type const &variableType, bool auxiliary=false, std::string const &prefix="_x")
	Declares a variable with the given type whose name is guaranteed to be unique and not yet in use.

Variable	declareFreshRationalVariable (bool auxiliary=false, std::string const &prefix="_x")
	Declares a variable with rational type whose name is guaranteed to be unique and not yet in use.

Variable	declareFreshBooleanVariable (bool auxiliary=false, std::string const &prefix="_x")
	Declares a variable with Boolean type whose name is guaranteed to be unique and not yet in use.

Variable	declareFreshIntegerVariable (bool auxiliary=false, std::string const &prefix="_x")
	Declares a variable with integer type whose name is guaranteed to be unique and not yet in use.

uint_fast64_t	getNumberOfVariables () const
	Retrieves the number of variables.

uint_fast64_t	getNumberOfBooleanVariables () const
	Retrieves the number of boolean variables.

uint_fast64_t	getNumberOfIntegerVariables () const
	Retrieves the number of integer variables.

uint_fast64_t	getNumberOfBitVectorVariables () const
	Retrieves the number of bit vector variables.

uint_fast64_t	getNumberOfRationalVariables () const
	Retrieves the number of rational variables.

uint_fast64_t	getNumberOfArrayVariables () const
	Retrieves the number of array variables.

std::string const &	getVariableName (uint_fast64_t index) const
	Retrieves the name of the variable with the given index.

Type const &	getVariableType (uint_fast64_t index) const
	Retrieves the type of the variable with the given index.

uint_fast64_t	getOffset (uint_fast64_t index) const
	Retrieves the offset of the variable with the given index within the group of equally typed variables.

const_iterator	begin () const
	Retrieves an iterator to all variables managed by this manager.

const_iterator	end () const
	Retrieves an iterator that points beyond the last variable managed by this manager.

std::shared_ptr< ExpressionManager >	getSharedPointer ()
	Retrieves a shared pointer to the expression manager.

std::shared_ptr< ExpressionManager const >	getSharedPointer () const
	Retrieves a shared pointer to the expression manager.

Friends
class	VariableIterator

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

Detailed Description

This class is responsible for managing a set of typed variables and all expressions using these variables.

Definition at line 72 of file ExpressionManager.h.

Member Typedef Documentation

◆ const_iterator

typedef VariableIterator storm::expressions::ExpressionManager::const_iterator

Definition at line 76 of file ExpressionManager.h.

Constructor & Destructor Documentation

◆ ExpressionManager() [1/2]

storm::expressions::ExpressionManager::ExpressionManager ( )

Creates a new manager that is unaware of any variables.

Definition at line 57 of file ExpressionManager.cpp.

◆ ~ExpressionManager()

storm::expressions::ExpressionManager::~ExpressionManager ( )

Definition at line 76 of file ExpressionManager.cpp.

◆ ExpressionManager() [2/2]

storm::expressions::ExpressionManager::ExpressionManager ( ExpressionManager && other )

default

Member Function Documentation

◆ begin()

ExpressionManager::const_iterator storm::expressions::ExpressionManager::begin ( ) const

Retrieves an iterator to all variables managed by this manager.

Returns: An iterator to all variables managed by this manager.

Definition at line 320 of file ExpressionManager.cpp.

◆ boolean()

Expression storm::expressions::ExpressionManager::boolean ( bool value ) const

Creates an expression that characterizes the given boolean literal.

Parameters

value The value of the boolean literal.

Returns: The resulting expression.

Definition at line 84 of file ExpressionManager.cpp.

◆ clone()

std::shared_ptr< ExpressionManager > storm::expressions::ExpressionManager::clone ( ) const

Creates a new expression manager with the same set of variables.

Definition at line 80 of file ExpressionManager.cpp.

◆ declareArrayVariable()

Variable storm::expressions::ExpressionManager::declareArrayVariable	(	std::string const &	name,
		Type const &	elementType,
		bool	auxiliary = `false`
	)

Declares a new array variable with the given name and the given element type.

Definition at line 182 of file ExpressionManager.cpp.

◆ declareBitVectorVariable()

Variable storm::expressions::ExpressionManager::declareBitVectorVariable	(	std::string const &	name,
		std::size_t	width,
		bool	auxiliary = `false`
	)

Declares a new bit vector variable with a name that must not yet exist and the bounded type of the given bit width.

Note that the name must not start with two underscores since these variables are reserved for internal use only.

Parameters

name	The name of the variable.
width	The bit width of the bit vector type.
auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.

Returns: The newly declared variable.

Definition at line 174 of file ExpressionManager.cpp.

◆ declareBooleanVariable()

Variable storm::expressions::ExpressionManager::declareBooleanVariable	(	std::string const &	name,
		bool	auxiliary = `false`
	)

Declares a new boolean variable with a name that must not yet exist and its corresponding type.

Note that the name must not start with two underscores since these variables are reserved for internal use only.

Parameters

name	The name of the variable.
auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.

Returns: The newly declared variable.

Definition at line 165 of file ExpressionManager.cpp.

◆ declareFreshBooleanVariable()

Variable storm::expressions::ExpressionManager::declareFreshBooleanVariable	(	bool	auxiliary = `false`,
		std::string const &	prefix = `"_x"`
	)

Declares a variable with Boolean type whose name is guaranteed to be unique and not yet in use.

Parameters

auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.
prefix	The prefix which should be used.

Returns: The variable.

Definition at line 253 of file ExpressionManager.cpp.

◆ declareFreshIntegerVariable()

Variable storm::expressions::ExpressionManager::declareFreshIntegerVariable	(	bool	auxiliary = `false`,
		std::string const &	prefix = `"_x"`
	)

Declares a variable with integer type whose name is guaranteed to be unique and not yet in use.

Parameters

auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.
prefix	The prefix which should be used.

Returns: The variable.

Definition at line 257 of file ExpressionManager.cpp.

◆ declareFreshRationalVariable()

Variable storm::expressions::ExpressionManager::declareFreshRationalVariable	(	bool	auxiliary = `false`,
		std::string const &	prefix = `"_x"`
	)

Declares a variable with rational type whose name is guaranteed to be unique and not yet in use.

Parameters

auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.
prefix	The prefix which should be used.

Returns: The variable.

Definition at line 261 of file ExpressionManager.cpp.

◆ declareFreshVariable()

Variable storm::expressions::ExpressionManager::declareFreshVariable	(	storm::expressions::Type const &	variableType,
		bool	auxiliary = `false`,
		std::string const &	prefix = `"_x"`
	)

Declares a variable with the given type whose name is guaranteed to be unique and not yet in use.

Parameters

variableType	The type of the variable to declare.
auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.
prefix	The prefix which should be used.

Returns: The variable.

Definition at line 248 of file ExpressionManager.cpp.

◆ declareIntegerVariable()

Variable storm::expressions::ExpressionManager::declareIntegerVariable	(	std::string const &	name,
		bool	auxiliary = `false`
	)

Declares a new integer variable with a name that must not yet exist and its corresponding type.

Note that the name must not start with two underscores since these variables are reserved for internal use only.

Parameters

name	The name of the variable.
auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.

Returns: The newly declared variable.

Definition at line 170 of file ExpressionManager.cpp.

◆ declareOrGetVariable()

Variable storm::expressions::ExpressionManager::declareOrGetVariable	(	std::string const &	name,
		storm::expressions::Type const &	variableType,
		bool	auxiliary = `false`
	)

Declares a variable with the given name if it does not yet exist.

Parameters

name	The name of the variable to declare.
variableType	The type of the variable to declare.
auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.

Returns: The variable.

Definition at line 186 of file ExpressionManager.cpp.

◆ declareRationalVariable()

Variable storm::expressions::ExpressionManager::declareRationalVariable	(	std::string const &	name,
		bool	auxiliary = `false`
	)

Declares a new rational variable with a name that must not yet exist and its corresponding type.

Note that the name must not start with two underscores since these variables are reserved for internal use only.

Parameters

name	The name of the variable.
auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.

Returns: The newly declared variable.

Definition at line 178 of file ExpressionManager.cpp.

◆ declareVariable()

Variable storm::expressions::ExpressionManager::declareVariable	(	std::string const &	name,
		storm::expressions::Type const &	variableType,
		bool	auxiliary = `false`
	)

Declares a variable with a name that must not yet exist and its corresponding type.

Note that the name must not start with two underscores since these variables are reserved for internal use only.

Parameters

name	The name of the variable.
variableType	The type of the variable.
auxiliary	A flag indicating whether the new variable should be tagged as an auxiliary variable.

Returns: The newly declared variable.

Definition at line 160 of file ExpressionManager.cpp.

◆ declareVariableCopy()

Variable storm::expressions::ExpressionManager::declareVariableCopy ( Variable const & variable )

Declares a variable that is a copy of the provided variable (i.e.

has the same type).

Parameters

variable The variable of which to create a copy.

Returns: The newly declared variable.

Definition at line 156 of file ExpressionManager.cpp.

◆ end()

ExpressionManager::const_iterator storm::expressions::ExpressionManager::end ( ) const

Retrieves an iterator that points beyond the last variable managed by this manager.

Returns: An iterator that points beyond the last variable managed by this manager.

Definition at line 325 of file ExpressionManager.cpp.

◆ getArrayType()

Type const & storm::expressions::ExpressionManager::getArrayType ( Type elementType ) const

Retrieves the array type with the given element type.

Definition at line 135 of file ExpressionManager.cpp.

◆ getBitVectorType()

Type const & storm::expressions::ExpressionManager::getBitVectorType ( std::size_t width ) const

Retrieves the bit vector type of the given width.

Parameters

width The bit width of the bounded type.

Returns: The bounded integer type.

Definition at line 118 of file ExpressionManager.cpp.

◆ getBooleanType()

Type const & storm::expressions::ExpressionManager::getBooleanType ( ) const

Retrieves the boolean type.

Returns: The boolean type.

Definition at line 104 of file ExpressionManager.cpp.

◆ getIntegerType()

Type const & storm::expressions::ExpressionManager::getIntegerType ( ) const

Retrieves the unbounded integer type.

Returns: The unbounded integer type.

Definition at line 111 of file ExpressionManager.cpp.

◆ getNumberOfArrayVariables()

uint_fast64_t storm::expressions::ExpressionManager::getNumberOfArrayVariables ( ) const

Retrieves the number of array variables.

Definition at line 300 of file ExpressionManager.cpp.

◆ getNumberOfBitVectorVariables()

uint_fast64_t storm::expressions::ExpressionManager::getNumberOfBitVectorVariables ( ) const

Retrieves the number of bit vector variables.

Returns: The number of bit vector variables.

Definition at line 292 of file ExpressionManager.cpp.

◆ getNumberOfBooleanVariables()

uint_fast64_t storm::expressions::ExpressionManager::getNumberOfBooleanVariables ( ) const

Retrieves the number of boolean variables.

Returns: The number of boolean variables.

Definition at line 284 of file ExpressionManager.cpp.

◆ getNumberOfIntegerVariables()

uint_fast64_t storm::expressions::ExpressionManager::getNumberOfIntegerVariables ( ) const

Retrieves the number of integer variables.

Returns: The number of integer variables.

Definition at line 288 of file ExpressionManager.cpp.

◆ getNumberOfRationalVariables()

uint_fast64_t storm::expressions::ExpressionManager::getNumberOfRationalVariables ( ) const

Retrieves the number of rational variables.

Returns: The number of rational variables.

Definition at line 296 of file ExpressionManager.cpp.

◆ getNumberOfVariables()

uint_fast64_t storm::expressions::ExpressionManager::getNumberOfVariables ( ) const

Retrieves the number of variables.

Returns: The number of variables.

Definition at line 280 of file ExpressionManager.cpp.

◆ getOffset()

uint64_t storm::expressions::ExpressionManager::getOffset ( uint_fast64_t index ) const

Retrieves the offset of the variable with the given index within the group of equally typed variables.

Parameters

index The index of the variable.

Returns: The offset of the variable.

Definition at line 316 of file ExpressionManager.cpp.

◆ getRationalType()

Type const & storm::expressions::ExpressionManager::getRationalType ( ) const

Retrieves the rational type.

Returns: The rational type.

Definition at line 128 of file ExpressionManager.cpp.

◆ getSharedPointer() [1/2]

std::shared_ptr< ExpressionManager > storm::expressions::ExpressionManager::getSharedPointer ( )

Retrieves a shared pointer to the expression manager.

Returns: A shared pointer to the expression manager.

Definition at line 330 of file ExpressionManager.cpp.

◆ getSharedPointer() [2/2]

std::shared_ptr< ExpressionManager const > storm::expressions::ExpressionManager::getSharedPointer ( ) const

Retrieves a shared pointer to the expression manager.

Returns: A shared pointer to the expression manager.

Definition at line 334 of file ExpressionManager.cpp.

◆ getTranscendentalNumberType()

Type const & storm::expressions::ExpressionManager::getTranscendentalNumberType ( ) const

Retrieves the transcendental numbers type (i.e.

pi and e)

Returns: The transcendental numbers type

Definition at line 140 of file ExpressionManager.cpp.

◆ getVariable()

Variable storm::expressions::ExpressionManager::getVariable ( std::string const & name ) const

Retrieves the expression that represents the variable with the given name.

Parameters

name	The name of the variable to retrieve.

Definition at line 230 of file ExpressionManager.cpp.

◆ getVariableExpression()

Expression storm::expressions::ExpressionManager::getVariableExpression ( std::string const & name ) const

Retrieves an expression that represents the variable with the given name.

Parameters

name	The name of the variable

Returns: An expression that represents the variable with the given name.

Definition at line 240 of file ExpressionManager.cpp.

◆ getVariableName()

std::string const & storm::expressions::ExpressionManager::getVariableName ( uint_fast64_t index ) const

Retrieves the name of the variable with the given index.

Parameters

index The index of the variable whose name to retrieve.

Returns: The name of the variable.

Definition at line 304 of file ExpressionManager.cpp.

◆ getVariables()

std::set< Variable > const & storm::expressions::ExpressionManager::getVariables ( ) const

Retrieves the set of all variables known to this manager.

Definition at line 236 of file ExpressionManager.cpp.

◆ getVariableType()

Type const & storm::expressions::ExpressionManager::getVariableType ( uint_fast64_t index ) const

Retrieves the type of the variable with the given index.

Parameters

index The index of the variable whose name to retrieve.

Returns: The type of the variable.

Definition at line 310 of file ExpressionManager.cpp.

◆ hasVariable()

bool storm::expressions::ExpressionManager::hasVariable ( std::string const & name ) const

Retrieves whether a variable with the given name is known to the manager.

Parameters

name	The name of the variable whose membership to query.

Returns: True iff a variable with the given name is known to the manager.

Definition at line 244 of file ExpressionManager.cpp.

◆ integer()

Expression storm::expressions::ExpressionManager::integer ( int_fast64_t value ) const

Creates an expression that characterizes the given integer literal.

Parameters

value The value of the integer literal.

Returns: The resulting expression.

Definition at line 88 of file ExpressionManager.cpp.

◆ operator=()

ExpressionManager & storm::expressions::ExpressionManager::operator= ( ExpressionManager && other )

default

◆ operator==()

bool storm::expressions::ExpressionManager::operator== ( ExpressionManager const & other ) const

Compares the two expression managers for equality, which holds iff they are the very same object.

Definition at line 100 of file ExpressionManager.cpp.

◆ rational() [1/2]

Expression storm::expressions::ExpressionManager::rational ( double value ) const

Creates an expression that characterizes the given rational literal.

Parameters

value The value of the rational literal.

Returns: The resulting expression.

Definition at line 92 of file ExpressionManager.cpp.

◆ rational() [2/2]

Expression storm::expressions::ExpressionManager::rational ( storm::RationalNumber const & value ) const

Creates an expression that characterizes the given rational literal.

Parameters

value The value of the rational literal.

Returns: The resulting expression.

Definition at line 96 of file ExpressionManager.cpp.

Friends And Related Symbol Documentation

◆ operator<<

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

friend

Definition at line 338 of file ExpressionManager.cpp.

◆ VariableIterator

friend class VariableIterator

friend

Definition at line 74 of file ExpressionManager.h.

The documentation for this class was generated from the following files:

src/storm/storage/expressions/ExpressionManager.h
src/storm/storage/expressions/ExpressionManager.cpp

Public Types

Public Member Functions

Friends

Detailed Description

Member Typedef Documentation

◆ const_iterator

Constructor & Destructor Documentation

◆ ExpressionManager() [1/2]

◆ ~ExpressionManager()

◆ ExpressionManager() [2/2]

Member Function Documentation

◆ begin()

◆ boolean()

◆ clone()

◆ declareArrayVariable()

◆ declareBitVectorVariable()

◆ declareBooleanVariable()

◆ declareFreshBooleanVariable()

◆ declareFreshIntegerVariable()

◆ declareFreshRationalVariable()

◆ declareFreshVariable()

◆ declareIntegerVariable()

◆ declareOrGetVariable()

◆ declareRationalVariable()

◆ declareVariable()

◆ declareVariableCopy()

◆ end()

◆ getArrayType()

◆ getBitVectorType()

◆ getBooleanType()

◆ getIntegerType()

◆ getNumberOfArrayVariables()

◆ getNumberOfBitVectorVariables()

◆ getNumberOfBooleanVariables()

◆ getNumberOfIntegerVariables()

◆ getNumberOfRationalVariables()

◆ getNumberOfVariables()

◆ getOffset()

◆ getRationalType()

◆ getSharedPointer() [1/2]

◆ getSharedPointer() [2/2]

◆ getTranscendentalNumberType()

◆ getVariable()

◆ getVariableExpression()

◆ getVariableName()

◆ getVariables()

◆ getVariableType()

◆ hasVariable()

◆ integer()

◆ operator=()

◆ operator==()

◆ rational() [1/2]

◆ rational() [2/2]

Friends And Related Symbol Documentation

◆ operator<<

◆ VariableIterator