Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::expressions::ExpressionManager Class Reference

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< ExpressionManagerclone () const
 Creates a new expression manager with the same set of variables.
 
 ExpressionManager (ExpressionManager &&other)=default
 
ExpressionManageroperator= (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< ExpressionManagergetSharedPointer ()
 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

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
valueThe 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
nameThe name of the variable.
widthThe bit width of the bit vector type.
auxiliaryA 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
nameThe name of the variable.
auxiliaryA 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
auxiliaryA flag indicating whether the new variable should be tagged as an auxiliary variable.
prefixThe 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
auxiliaryA flag indicating whether the new variable should be tagged as an auxiliary variable.
prefixThe 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
auxiliaryA flag indicating whether the new variable should be tagged as an auxiliary variable.
prefixThe 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
variableTypeThe type of the variable to declare.
auxiliaryA flag indicating whether the new variable should be tagged as an auxiliary variable.
prefixThe 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
nameThe name of the variable.
auxiliaryA 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
nameThe name of the variable to declare.
variableTypeThe type of the variable to declare.
auxiliaryA 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
nameThe name of the variable.
auxiliaryA 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
nameThe name of the variable.
variableTypeThe type of the variable.
auxiliaryA 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
variableThe 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
widthThe 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
indexThe 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
nameThe 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
nameThe 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
indexThe 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
indexThe 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
nameThe 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
valueThe 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
valueThe 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
valueThe 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: