Storm
A Modern Probabilistic Model Checker
|
#include <Expression.h>
Public Member Functions | |
Expression ()=default | |
~Expression () | |
Expression (Variable const &variable) | |
Creates an expression representing the given variable. | |
Expression (std::shared_ptr< BaseExpression const > const &expressionPtr) | |
Creates an expression with the given underlying base expression. | |
Expression (Expression const &other)=default | |
Expression & | operator= (Expression const &other)=default |
Expression (Expression &&)=default | |
Expression & | operator= (Expression &&)=default |
Expression | changeManager (ExpressionManager const &newExpressionManager) const |
Converts the expression to an expression over the variables of the provided expression manager. | |
Expression | substitute (std::map< Variable, Expression > const &variableToExpressionMap) const |
Substitutes all occurrences of the variables according to the given map. | |
Expression | substituteNonStandardPredicates () const |
Eliminate nonstandard predicates from the expression. | |
Expression | substitute (std::unordered_map< Variable, Expression > const &variableToExpressionMap) const |
Substitutes all occurrences of the variables according to the given map. | |
bool | evaluateAsBool (Valuation const *valuation=nullptr) const |
Evaluates the expression under the valuation of variables given by the valuation and returns the resulting boolean value. | |
int_fast64_t | evaluateAsInt (Valuation const *valuation=nullptr) const |
Evaluates the expression under the valuation of variables given by the valuation and returns the resulting integer value. | |
double | evaluateAsDouble (Valuation const *valuation=nullptr) const |
Evaluates the expression under the valuation of variables given by the valuation and returns the resulting double value. | |
storm::RationalNumber | evaluateAsRational () const |
Evaluates the expression and returns the resulting rational number. | |
Expression | simplify () const |
Simplifies the expression according to some basic rules. | |
Expression | reduceNesting () const |
Tries to flatten the syntax tree of the expression, e.g., 1 + (2 + (3 + 4)) becomes (1 + 2) + (3 + 4) | |
OperatorType | getOperator () const |
Retrieves the operator of a function application. | |
bool | isFunctionApplication () const |
Checks if the expression is a function application (of any sort). | |
uint_fast64_t | getArity () const |
Retrieves the arity of the expression. | |
Expression | getOperand (uint_fast64_t operandIndex) const |
Retrieves the given operand from the expression. | |
std::string const & | getIdentifier () const |
Retrieves the identifier associated with this expression. | |
bool | containsVariables () const |
Retrieves whether the expression contains a variable. | |
bool | isLiteral () const |
Retrieves whether the expression is a literal. | |
bool | isVariable () const |
Retrieves whether the expression is a variable. | |
bool | isTrue () const |
Checks if the expression is equal to the boolean literal true. | |
bool | isFalse () const |
Checks if the expression is equal to the boolean literal false. | |
bool | areSame (storm::expressions::Expression const &other) const |
Checks whether the two expressions are the same. | |
bool | isRelationalExpression () const |
Retrieves whether this expression is a relation expression, i.e., an expression that has a relation (equal, not equal, less, less or equal, etc.) as its top-level operator. | |
bool | isLinear () const |
Retrieves whether this expression is a linear expression. | |
std::set< storm::expressions::Variable > | getVariables () const |
Retrieves the set of all variables that appear in the expression. | |
void | gatherVariables (std::set< storm::expressions::Variable > &variables) const |
Retrieves the set of all variables that appear in the expression. | |
bool | containsVariable (std::set< storm::expressions::Variable > const &variables) const |
Retrieves whether the expression contains any of the given variables. | |
bool | containsVariableInITEGuard (std::set< storm::expressions::Variable > const &variables) const |
Retrieves whether the expression contains any of the given variables in the 'if' part of any sub-IfThenElseExpressions. | |
BaseExpression const & | getBaseExpression () const |
Retrieves the base expression underlying this expression object. | |
std::shared_ptr< BaseExpression const > const & | getBaseExpressionPointer () const |
Retrieves a pointer to the base expression underlying this expression object. | |
ExpressionManager const & | getManager () const |
Retrieves the manager responsible for this expression. | |
Type const & | getType () const |
Retrieves the type of the expression. | |
bool | hasNumericalType () const |
Retrieves whether the expression has a numerical return type, i.e., integer or double. | |
bool | hasRationalType () const |
Retrieves whether the expression has a rational return type. | |
bool | hasBooleanType () const |
Retrieves whether the expression has a boolean return type. | |
bool | hasIntegerType () const |
Retrieves whether the expression has an integral return type. | |
bool | hasBitVectorType () const |
Retrieves whether the expression has an integral return type. | |
boost::any | accept (ExpressionVisitor &visitor, boost::any const &data) const |
Accepts the given visitor. | |
std::string | toString () const |
Converts the expression into a string. | |
bool | isInitialized () const |
Checks whether the object encapsulates a base-expression. | |
bool | isSyntacticallyEqual (storm::expressions::Expression const &other) const |
Checks whether the two expressions are syntatically the same. | |
bool | hasCompiledExpression () const |
Retrieves whether this expression object has an associated compiled expression. | |
void | setCompiledExpression (std::shared_ptr< CompiledExpression > const &compiledExpression) const |
Associates the given compiled expression with this expression object. | |
CompiledExpression const & | getCompiledExpression () const |
Retrieves the associated compiled expression object (if there is any). | |
Friends | |
class | ExpressionManager |
class | Variable |
template<typename MapType > | |
class | SubstitutionVisitor |
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 | 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) |
The type of the resulting expression is. | |
Expression | abs (Expression const &first) |
Expression | truncate (Expression const &first) |
Expression | sign (Expression const &first) |
Expression | floor (Expression const &first) |
Expression | ceil (Expression const &first) |
Expression | round (Expression const &first) |
Expression | minimum (Expression const &first, Expression const &second) |
Expression | maximum (Expression const &first, Expression const &second) |
std::ostream & | operator<< (std::ostream &stream, Expression const &expression) |
Definition at line 22 of file Expression.h.
|
default |
storm::expressions::Expression::~Expression | ( | ) |
Definition at line 33 of file Expression.cpp.
storm::expressions::Expression::Expression | ( | Variable const & | variable | ) |
Creates an expression representing the given variable.
variable | The variable to represent. |
Definition at line 41 of file Expression.cpp.
storm::expressions::Expression::Expression | ( | std::shared_ptr< BaseExpression const > const & | expressionPtr | ) |
Creates an expression with the given underlying base expression.
expressionPtr | A pointer to the underlying base expression. |
Definition at line 37 of file Expression.cpp.
|
default |
|
default |
boost::any storm::expressions::Expression::accept | ( | ExpressionVisitor & | visitor, |
boost::any const & | data | ||
) | const |
Accepts the given visitor.
visitor | The visitor to accept. |
Definition at line 205 of file Expression.cpp.
bool storm::expressions::Expression::areSame | ( | storm::expressions::Expression const & | other | ) | const |
Checks whether the two expressions are the same.
Note that this does not check for syntactical or even semantical equivalence, but only returns true if both are the very same expressions.
Definition at line 126 of file Expression.cpp.
Expression storm::expressions::Expression::changeManager | ( | ExpressionManager const & | newExpressionManager | ) | const |
Converts the expression to an expression over the variables of the provided expression manager.
Definition at line 45 of file Expression.cpp.
bool storm::expressions::Expression::containsVariable | ( | std::set< storm::expressions::Variable > const & | variables | ) | const |
Retrieves whether the expression contains any of the given variables.
variables | The variables to search for. |
Definition at line 140 of file Expression.cpp.
bool storm::expressions::Expression::containsVariableInITEGuard | ( | std::set< storm::expressions::Variable > const & | variables | ) | const |
Retrieves whether the expression contains any of the given variables in the 'if' part of any sub-IfThenElseExpressions.
variables | The variables to search for. |
Definition at line 150 of file Expression.cpp.
bool storm::expressions::Expression::containsVariables | ( | ) | const |
Retrieves whether the expression contains a variable.
Definition at line 106 of file Expression.cpp.
bool storm::expressions::Expression::evaluateAsBool | ( | Valuation const * | valuation = nullptr | ) | const |
Evaluates the expression under the valuation of variables given by the valuation and returns the resulting boolean value.
If the return type of the expression is not a boolean an exception is thrown.
valuation | The valuation of unknowns under which to evaluate the expression. |
Definition at line 62 of file Expression.cpp.
double storm::expressions::Expression::evaluateAsDouble | ( | Valuation const * | valuation = nullptr | ) | const |
Evaluates the expression under the valuation of variables given by the valuation and returns the resulting double value.
If the return type of the expression is not a double an exception is thrown.
valuation | The valuation of unknowns under which to evaluate the expression. |
Definition at line 70 of file Expression.cpp.
int_fast64_t storm::expressions::Expression::evaluateAsInt | ( | Valuation const * | valuation = nullptr | ) | const |
Evaluates the expression under the valuation of variables given by the valuation and returns the resulting integer value.
If the return type of the expression is not an integer an exception is thrown.
valuation | The valuation of unknowns under which to evaluate the expression. |
Definition at line 66 of file Expression.cpp.
storm::RationalNumber storm::expressions::Expression::evaluateAsRational | ( | ) | const |
Evaluates the expression and returns the resulting rational number.
If the return type of the expression is not a rational an exception is thrown.
valuation | The valuation of unknowns under which to evaluate the expression. |
Definition at line 74 of file Expression.cpp.
void storm::expressions::Expression::gatherVariables | ( | std::set< storm::expressions::Variable > & | variables | ) | const |
Retrieves the set of all variables that appear in the expression.
These variables are added to the given set.
variables | The set to which to add the variables. |
Definition at line 136 of file Expression.cpp.
uint_fast64_t storm::expressions::Expression::getArity | ( | ) | const |
Retrieves the arity of the expression.
Definition at line 94 of file Expression.cpp.
BaseExpression const & storm::expressions::Expression::getBaseExpression | ( | ) | const |
Retrieves the base expression underlying this expression object.
Note that prior to calling this, the expression object must be properly initialized.
Definition at line 169 of file Expression.cpp.
std::shared_ptr< BaseExpression const > const & storm::expressions::Expression::getBaseExpressionPointer | ( | ) | const |
Retrieves a pointer to the base expression underlying this expression object.
Definition at line 173 of file Expression.cpp.
CompiledExpression const & storm::expressions::Expression::getCompiledExpression | ( | ) | const |
Retrieves the associated compiled expression object (if there is any).
Definition at line 232 of file Expression.cpp.
std::string const & storm::expressions::Expression::getIdentifier | ( | ) | const |
Retrieves the identifier associated with this expression.
This is only legal to call if the expression is a variable.
Definition at line 102 of file Expression.cpp.
ExpressionManager const & storm::expressions::Expression::getManager | ( | ) | const |
Retrieves the manager responsible for this expression.
Definition at line 177 of file Expression.cpp.
Expression storm::expressions::Expression::getOperand | ( | uint_fast64_t | operandIndex | ) | const |
Retrieves the given operand from the expression.
operandIndex | The index of the operand to retrieve. This must be lower than the arity of the expression. |
Definition at line 98 of file Expression.cpp.
OperatorType storm::expressions::Expression::getOperator | ( | ) | const |
Retrieves the operator of a function application.
This is only legal to call if the expression is function application.
Definition at line 86 of file Expression.cpp.
Type const & storm::expressions::Expression::getType | ( | ) | const |
Retrieves the type of the expression.
Definition at line 181 of file Expression.cpp.
std::set< storm::expressions::Variable > storm::expressions::Expression::getVariables | ( | ) | const |
Retrieves the set of all variables that appear in the expression.
Definition at line 130 of file Expression.cpp.
bool storm::expressions::Expression::hasBitVectorType | ( | ) | const |
Retrieves whether the expression has an integral return type.
Definition at line 201 of file Expression.cpp.
bool storm::expressions::Expression::hasBooleanType | ( | ) | const |
Retrieves whether the expression has a boolean return type.
Definition at line 193 of file Expression.cpp.
bool storm::expressions::Expression::hasCompiledExpression | ( | ) | const |
Retrieves whether this expression object has an associated compiled expression.
Definition at line 224 of file Expression.cpp.
bool storm::expressions::Expression::hasIntegerType | ( | ) | const |
Retrieves whether the expression has an integral return type.
Definition at line 197 of file Expression.cpp.
bool storm::expressions::Expression::hasNumericalType | ( | ) | const |
Retrieves whether the expression has a numerical return type, i.e., integer or double.
Definition at line 185 of file Expression.cpp.
bool storm::expressions::Expression::hasRationalType | ( | ) | const |
Retrieves whether the expression has a rational return type.
Definition at line 189 of file Expression.cpp.
bool storm::expressions::Expression::isFalse | ( | ) | const |
Checks if the expression is equal to the boolean literal false.
Definition at line 122 of file Expression.cpp.
bool storm::expressions::Expression::isFunctionApplication | ( | ) | const |
Checks if the expression is a function application (of any sort).
Definition at line 90 of file Expression.cpp.
bool storm::expressions::Expression::isInitialized | ( | ) | const |
Checks whether the object encapsulates a base-expression.
Definition at line 209 of file Expression.cpp.
bool storm::expressions::Expression::isLinear | ( | ) | const |
Retrieves whether this expression is a linear expression.
Definition at line 165 of file Expression.cpp.
bool storm::expressions::Expression::isLiteral | ( | ) | const |
Retrieves whether the expression is a literal.
Definition at line 110 of file Expression.cpp.
bool storm::expressions::Expression::isRelationalExpression | ( | ) | const |
Retrieves whether this expression is a relation expression, i.e., an expression that has a relation (equal, not equal, less, less or equal, etc.) as its top-level operator.
Definition at line 155 of file Expression.cpp.
bool storm::expressions::Expression::isSyntacticallyEqual | ( | storm::expressions::Expression const & | other | ) | const |
Checks whether the two expressions are syntatically the same.
Definition at line 216 of file Expression.cpp.
bool storm::expressions::Expression::isTrue | ( | ) | const |
Checks if the expression is equal to the boolean literal true.
Definition at line 118 of file Expression.cpp.
bool storm::expressions::Expression::isVariable | ( | ) | const |
Retrieves whether the expression is a variable.
Definition at line 114 of file Expression.cpp.
|
default |
|
default |
Expression storm::expressions::Expression::reduceNesting | ( | ) | const |
Tries to flatten the syntax tree of the expression, e.g., 1 + (2 + (3 + 4)) becomes (1 + 2) + (3 + 4)
Definition at line 82 of file Expression.cpp.
void storm::expressions::Expression::setCompiledExpression | ( | std::shared_ptr< CompiledExpression > const & | compiledExpression | ) | const |
Associates the given compiled expression with this expression object.
Definition at line 228 of file Expression.cpp.
Expression storm::expressions::Expression::simplify | ( | ) | const |
Simplifies the expression according to some basic rules.
Definition at line 78 of file Expression.cpp.
Expression storm::expressions::Expression::substitute | ( | std::map< Variable, Expression > const & | variableToExpressionMap | ) | const |
Substitutes all occurrences of the variables according to the given map.
Note that this substitution is done simultaneously, i.e., variables appearing in the expressions that were "plugged in" are not substituted.
variableToExpressionMap | A mapping from variables to the expression they are substituted with. |
Definition at line 50 of file Expression.cpp.
Expression storm::expressions::Expression::substitute | ( | std::unordered_map< Variable, Expression > const & | variableToExpressionMap | ) | const |
Substitutes all occurrences of the variables according to the given map.
Note that this substitution is done simultaneously, i.e., variables appearing in the expressions that were "plugged in" are not substituted.
variableToExpressionMap | A mapping from variables to the expression they are substituted with. |
Definition at line 54 of file Expression.cpp.
Expression storm::expressions::Expression::substituteNonStandardPredicates | ( | ) | const |
Eliminate nonstandard predicates from the expression.
Definition at line 58 of file Expression.cpp.
std::string storm::expressions::Expression::toString | ( | ) | const |
Converts the expression into a string.
Definition at line 236 of file Expression.cpp.
|
friend |
Definition at line 480 of file Expression.cpp.
|
friend |
Definition at line 468 of file Expression.cpp.
|
friend |
Definition at line 24 of file Expression.h.
|
friend |
Definition at line 461 of file Expression.cpp.
|
friend |
Definition at line 440 of file Expression.cpp.
|
friend |
Definition at line 433 of file Expression.cpp.
|
friend |
Definition at line 425 of file Expression.cpp.
|
friend |
Definition at line 418 of file Expression.cpp.
|
friend |
Definition at line 411 of file Expression.cpp.
|
friend |
Definition at line 341 of file Expression.cpp.
|
friend |
Definition at line 354 of file Expression.cpp.
|
friend |
Definition at line 306 of file Expression.cpp.
|
friend |
Definition at line 317 of file Expression.cpp.
|
friend |
Definition at line 292 of file Expression.cpp.
|
friend |
Definition at line 251 of file Expression.cpp.
|
friend |
Definition at line 263 of file Expression.cpp.
|
friend |
Definition at line 267 of file Expression.cpp.
|
friend |
Definition at line 286 of file Expression.cpp.
|
friend |
Definition at line 271 of file Expression.cpp.
|
friend |
Definition at line 278 of file Expression.cpp.
|
friend |
Definition at line 282 of file Expression.cpp.
|
friend |
Definition at line 299 of file Expression.cpp.
|
friend |
Definition at line 381 of file Expression.cpp.
|
friend |
Definition at line 395 of file Expression.cpp.
|
friend |
Definition at line 242 of file Expression.cpp.
|
friend |
Definition at line 388 of file Expression.cpp.
|
friend |
Definition at line 403 of file Expression.cpp.
|
friend |
Definition at line 347 of file Expression.cpp.
|
friend |
Definition at line 367 of file Expression.cpp.
|
friend |
Definition at line 399 of file Expression.cpp.
|
friend |
Definition at line 374 of file Expression.cpp.
|
friend |
Definition at line 407 of file Expression.cpp.
|
friend |
Definition at line 329 of file Expression.cpp.
|
friend |
The type of the resulting expression is.
Definition at line 454 of file Expression.cpp.
|
friend |
Definition at line 475 of file Expression.cpp.
|
friend |
Definition at line 485 of file Expression.cpp.
|
friend |
Definition at line 27 of file Expression.h.
|
friend |
Definition at line 490 of file Expression.cpp.
|
friend |
Definition at line 25 of file Expression.h.
|
friend |
Definition at line 447 of file Expression.cpp.