Storm
A Modern Probabilistic Model Checker
|
This class is responsible for managing a set of typed variables and all expressions using these variables. More...
#include <ExpressionManager.h>
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) |
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.
Definition at line 76 of file ExpressionManager.h.
storm::expressions::ExpressionManager::ExpressionManager | ( | ) |
Creates a new manager that is unaware of any variables.
Definition at line 57 of file ExpressionManager.cpp.
storm::expressions::ExpressionManager::~ExpressionManager | ( | ) |
Definition at line 76 of file ExpressionManager.cpp.
|
default |
ExpressionManager::const_iterator storm::expressions::ExpressionManager::begin | ( | ) | const |
Retrieves an iterator to all variables managed by this manager.
Definition at line 320 of file ExpressionManager.cpp.
Expression storm::expressions::ExpressionManager::boolean | ( | bool | value | ) | const |
Creates an expression that characterizes the given boolean literal.
value | The value of the boolean literal. |
Definition at line 84 of file ExpressionManager.cpp.
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.
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.
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.
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. |
Definition at line 174 of file ExpressionManager.cpp.
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.
name | The name of the variable. |
auxiliary | A flag indicating whether the new variable should be tagged as an auxiliary variable. |
Definition at line 165 of file ExpressionManager.cpp.
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.
auxiliary | A flag indicating whether the new variable should be tagged as an auxiliary variable. |
prefix | The prefix which should be used. |
Definition at line 253 of file ExpressionManager.cpp.
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.
auxiliary | A flag indicating whether the new variable should be tagged as an auxiliary variable. |
prefix | The prefix which should be used. |
Definition at line 257 of file ExpressionManager.cpp.
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.
auxiliary | A flag indicating whether the new variable should be tagged as an auxiliary variable. |
prefix | The prefix which should be used. |
Definition at line 261 of file ExpressionManager.cpp.
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.
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. |
Definition at line 248 of file ExpressionManager.cpp.
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.
name | The name of the variable. |
auxiliary | A flag indicating whether the new variable should be tagged as an auxiliary variable. |
Definition at line 170 of file ExpressionManager.cpp.
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.
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. |
Definition at line 186 of file ExpressionManager.cpp.
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.
name | The name of the variable. |
auxiliary | A flag indicating whether the new variable should be tagged as an auxiliary variable. |
Definition at line 178 of file ExpressionManager.cpp.
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.
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. |
Definition at line 160 of file ExpressionManager.cpp.
Declares a variable that is a copy of the provided variable (i.e.
has the same type).
variable | The variable of which to create a copy. |
Definition at line 156 of file ExpressionManager.cpp.
ExpressionManager::const_iterator storm::expressions::ExpressionManager::end | ( | ) | const |
Retrieves an iterator that points beyond the last variable managed by this manager.
Definition at line 325 of file ExpressionManager.cpp.
Retrieves the array type with the given element type.
Definition at line 135 of file ExpressionManager.cpp.
Type const & storm::expressions::ExpressionManager::getBitVectorType | ( | std::size_t | width | ) | const |
Retrieves the bit vector type of the given width.
width | The bit width of the bounded type. |
Definition at line 118 of file ExpressionManager.cpp.
Type const & storm::expressions::ExpressionManager::getBooleanType | ( | ) | const |
Retrieves the boolean type.
Definition at line 104 of file ExpressionManager.cpp.
Type const & storm::expressions::ExpressionManager::getIntegerType | ( | ) | const |
Retrieves the unbounded integer type.
Definition at line 111 of file ExpressionManager.cpp.
uint_fast64_t storm::expressions::ExpressionManager::getNumberOfArrayVariables | ( | ) | const |
Retrieves the number of array variables.
Definition at line 300 of file ExpressionManager.cpp.
uint_fast64_t storm::expressions::ExpressionManager::getNumberOfBitVectorVariables | ( | ) | const |
Retrieves the number of bit vector variables.
Definition at line 292 of file ExpressionManager.cpp.
uint_fast64_t storm::expressions::ExpressionManager::getNumberOfBooleanVariables | ( | ) | const |
Retrieves the number of boolean variables.
Definition at line 284 of file ExpressionManager.cpp.
uint_fast64_t storm::expressions::ExpressionManager::getNumberOfIntegerVariables | ( | ) | const |
Retrieves the number of integer variables.
Definition at line 288 of file ExpressionManager.cpp.
uint_fast64_t storm::expressions::ExpressionManager::getNumberOfRationalVariables | ( | ) | const |
Retrieves the number of rational variables.
Definition at line 296 of file ExpressionManager.cpp.
uint_fast64_t storm::expressions::ExpressionManager::getNumberOfVariables | ( | ) | const |
Retrieves the number of variables.
Definition at line 280 of file ExpressionManager.cpp.
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.
index | The index of the variable. |
Definition at line 316 of file ExpressionManager.cpp.
Type const & storm::expressions::ExpressionManager::getRationalType | ( | ) | const |
Retrieves the rational type.
Definition at line 128 of file ExpressionManager.cpp.
std::shared_ptr< ExpressionManager > storm::expressions::ExpressionManager::getSharedPointer | ( | ) |
Retrieves a shared pointer to the expression manager.
Definition at line 330 of file ExpressionManager.cpp.
std::shared_ptr< ExpressionManager const > storm::expressions::ExpressionManager::getSharedPointer | ( | ) | const |
Retrieves a shared pointer to the expression manager.
Definition at line 334 of file ExpressionManager.cpp.
Type const & storm::expressions::ExpressionManager::getTranscendentalNumberType | ( | ) | const |
Retrieves the transcendental numbers type (i.e.
pi and e)
Definition at line 140 of file ExpressionManager.cpp.
Variable storm::expressions::ExpressionManager::getVariable | ( | std::string const & | name | ) | const |
Retrieves the expression that represents the variable with the given name.
name | The name of the variable to retrieve. |
Definition at line 230 of file ExpressionManager.cpp.
Expression storm::expressions::ExpressionManager::getVariableExpression | ( | std::string const & | name | ) | const |
Retrieves an expression that represents the variable with the given name.
name | The name of the variable |
Definition at line 240 of file ExpressionManager.cpp.
std::string const & storm::expressions::ExpressionManager::getVariableName | ( | uint_fast64_t | index | ) | const |
Retrieves the name of the variable with the given index.
index | The index of the variable whose name to retrieve. |
Definition at line 304 of file ExpressionManager.cpp.
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.
Type const & storm::expressions::ExpressionManager::getVariableType | ( | uint_fast64_t | index | ) | const |
Retrieves the type of the variable with the given index.
index | The index of the variable whose name to retrieve. |
Definition at line 310 of file ExpressionManager.cpp.
bool storm::expressions::ExpressionManager::hasVariable | ( | std::string const & | name | ) | const |
Retrieves whether a variable with the given name is known to the manager.
name | The name of the variable whose membership to query. |
Definition at line 244 of file ExpressionManager.cpp.
Expression storm::expressions::ExpressionManager::integer | ( | int_fast64_t | value | ) | const |
Creates an expression that characterizes the given integer literal.
value | The value of the integer literal. |
Definition at line 88 of file ExpressionManager.cpp.
|
default |
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.
Expression storm::expressions::ExpressionManager::rational | ( | double | value | ) | const |
Creates an expression that characterizes the given rational literal.
value | The value of the rational literal. |
Definition at line 92 of file ExpressionManager.cpp.
Expression storm::expressions::ExpressionManager::rational | ( | storm::RationalNumber const & | value | ) | const |
Creates an expression that characterizes the given rational literal.
value | The value of the rational literal. |
Definition at line 96 of file ExpressionManager.cpp.
|
friend |
Definition at line 338 of file ExpressionManager.cpp.
|
friend |
Definition at line 74 of file ExpressionManager.h.