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 70 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 314 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 78 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 74 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 176 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 168 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 159 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 247 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 251 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 255 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 242 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 164 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 180 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 172 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 154 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 150 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 319 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 129 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 112 of file ExpressionManager.cpp.

◆ getBooleanType()

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

Retrieves the boolean type.

Returns: The boolean type.

Definition at line 98 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 105 of file ExpressionManager.cpp.

◆ getNumberOfArrayVariables()

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

Retrieves the number of array variables.

Definition at line 294 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 286 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 278 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 282 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 290 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 274 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 310 of file ExpressionManager.cpp.

◆ getRationalType()

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

Retrieves the rational type.

Returns: The rational type.

Definition at line 122 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 324 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 328 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 134 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 224 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 234 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 298 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 230 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 304 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 238 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 82 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 94 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 86 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 90 of file ExpressionManager.cpp.

Friends And Related Symbol Documentation

◆ operator<<

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

friend

Definition at line 332 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