Storm
A Modern Probabilistic Model Checker
|
The base class of all expression classes. More...
#include <BaseExpression.h>
Public Member Functions | |
BaseExpression (ExpressionManager const &manager, Type const &type) | |
Constructs a base expression with the given return type. | |
BaseExpression (BaseExpression const &)=default | |
BaseExpression & | operator= (BaseExpression const &)=delete |
BaseExpression (BaseExpression &&)=default | |
BaseExpression & | operator= (BaseExpression &&)=delete |
virtual | ~BaseExpression ()=default |
Expression | toExpression () const |
Converts the base expression to a proper expression. | |
virtual bool | evaluateAsBool (Valuation const *valuation=nullptr) const |
Evaluates the expression under the valuation of unknowns (variables and constants) given by the valuation and returns the resulting boolean value. | |
virtual int_fast64_t | evaluateAsInt (Valuation const *valuation=nullptr) const |
Evaluates the expression under the valuation of unknowns (variables and constants) given by the valuation and returns the resulting integer value. | |
virtual double | evaluateAsDouble (Valuation const *valuation=nullptr) const |
Evaluates the expression under the valuation of unknowns (variables and constants) given by the valuation and returns the resulting double value. | |
virtual storm::RationalNumber | evaluateAsRational () const |
Evaluates the expression and returns the resulting rational number. | |
virtual uint_fast64_t | getArity () const |
Returns the arity of the expression. | |
virtual std::shared_ptr< BaseExpression const > | getOperand (uint_fast64_t operandIndex) const |
Retrieves the given operand from the expression. | |
virtual std::string const & | getIdentifier () const |
Retrieves the identifier associated with this expression. | |
virtual OperatorType | getOperator () const |
Retrieves the operator of a function application. | |
virtual bool | containsVariables () const |
Retrieves whether the expression contains a variable. | |
virtual bool | isLiteral () const |
Retrieves whether the expression is a literal. | |
virtual bool | isVariable () const |
Retrieves whether the expression is a variable. | |
virtual bool | isTrue () const |
Checks if the expression is equal to the boolean literal true. | |
virtual bool | isFalse () const |
Checks if the expression is equal to the boolean literal false. | |
virtual bool | isFunctionApplication () const |
Checks if the expression is a function application (of any sort). | |
virtual void | gatherVariables (std::set< storm::expressions::Variable > &variables) const =0 |
Retrieves the set of all variables that appear in the expression. | |
virtual std::shared_ptr< BaseExpression const > | simplify () const =0 |
Simplifies the expression according to some simple rules. | |
std::shared_ptr< BaseExpression const > | reduceNesting () const |
Tries to flatten the syntax tree of the expression, e.g., 1 + (2 + (3 + 4)) becomes (1 + 2) + (3 + 4) | |
virtual boost::any | accept (ExpressionVisitor &visitor, boost::any const &data) const =0 |
Accepts the given visitor by calling its visit method. | |
bool | hasNumericalType () const |
Retrieves whether the expression has a numerical type, i.e., integer or double. | |
bool | hasIntegerType () const |
Retrieves whether the expression has an integer type. | |
bool | hasBitVectorType () const |
Retrieves whether the expression has a bitvector type. | |
bool | hasBooleanType () const |
Retrieves whether the expression has a boolean type. | |
bool | hasRationalType () const |
Retrieves whether the expression has a rational return type. | |
std::shared_ptr< BaseExpression const > | getSharedPointer () const |
Retrieves a shared pointer to this expression. | |
ExpressionManager const & | getManager () const |
Retrieves the manager responsible for this expression. | |
Type const & | getType () const |
Retrieves the type of the expression. | |
virtual bool | isIfThenElseExpression () const |
IfThenElseExpression const & | asIfThenElseExpression () const |
virtual bool | isBinaryBooleanFunctionExpression () const |
BinaryBooleanFunctionExpression const & | asBinaryBooleanFunctionExpression () const |
virtual bool | isBinaryNumericalFunctionExpression () const |
BinaryNumericalFunctionExpression const & | asBinaryNumericalFunctionExpression () const |
virtual bool | isBinaryRelationExpression () const |
BinaryRelationExpression const & | asBinaryRelationExpression () const |
virtual bool | isBooleanLiteralExpression () const |
BooleanLiteralExpression const & | asBooleanLiteralExpression () const |
virtual bool | isIntegerLiteralExpression () const |
IntegerLiteralExpression const & | asIntegerLiteralExpression () const |
virtual bool | isRationalLiteralExpression () const |
RationalLiteralExpression const & | asRationalLiteralExpression () const |
virtual bool | isUnaryBooleanFunctionExpression () const |
UnaryBooleanFunctionExpression const & | asUnaryBooleanFunctionExpression () const |
virtual bool | isUnaryNumericalFunctionExpression () const |
UnaryNumericalFunctionExpression const & | asUnaryNumericalFunctionExpression () const |
virtual bool | isVariableExpression () const |
VariableExpression const & | asVariableExpression () const |
virtual bool | isPredicateExpression () const |
PredicateExpression const & | asPredicateExpression () const |
Protected Member Functions | |
virtual void | printToStream (std::ostream &stream) const =0 |
Prints the expression to the given stream. | |
Friends | |
std::ostream & | operator<< (std::ostream &stream, BaseExpression const &expression) |
The base class of all expression classes.
Definition at line 43 of file BaseExpression.h.
storm::expressions::BaseExpression::BaseExpression | ( | ExpressionManager const & | manager, |
Type const & | type | ||
) |
Constructs a base expression with the given return type.
type | The type of the expression. |
Definition at line 14 of file BaseExpression.cpp.
|
default |
|
default |
|
virtualdefault |
|
pure virtual |
Accepts the given visitor by calling its visit method.
visitor | The visitor that is to be accepted. |
Implemented in storm::expressions::BinaryBooleanFunctionExpression, storm::expressions::BinaryNumericalFunctionExpression, storm::expressions::BinaryRelationExpression, storm::expressions::BooleanLiteralExpression, storm::expressions::IfThenElseExpression, storm::expressions::IntegerLiteralExpression, storm::expressions::PredicateExpression, storm::expressions::RationalLiteralExpression, storm::expressions::UnaryBooleanFunctionExpression, storm::expressions::UnaryNumericalFunctionExpression, storm::expressions::VariableExpression, storm::expressions::ArrayAccessExpression, storm::expressions::ConstructorArrayExpression, storm::expressions::FunctionCallExpression, storm::expressions::TranscendentalNumberLiteralExpression, and storm::expressions::ValueArrayExpression.
BinaryBooleanFunctionExpression const & storm::expressions::BaseExpression::asBinaryBooleanFunctionExpression | ( | ) | const |
Definition at line 129 of file BaseExpression.cpp.
BinaryNumericalFunctionExpression const & storm::expressions::BaseExpression::asBinaryNumericalFunctionExpression | ( | ) | const |
Definition at line 137 of file BaseExpression.cpp.
BinaryRelationExpression const & storm::expressions::BaseExpression::asBinaryRelationExpression | ( | ) | const |
Definition at line 145 of file BaseExpression.cpp.
BooleanLiteralExpression const & storm::expressions::BaseExpression::asBooleanLiteralExpression | ( | ) | const |
Definition at line 153 of file BaseExpression.cpp.
IfThenElseExpression const & storm::expressions::BaseExpression::asIfThenElseExpression | ( | ) | const |
Definition at line 121 of file BaseExpression.cpp.
IntegerLiteralExpression const & storm::expressions::BaseExpression::asIntegerLiteralExpression | ( | ) | const |
Definition at line 161 of file BaseExpression.cpp.
PredicateExpression const & storm::expressions::BaseExpression::asPredicateExpression | ( | ) | const |
Definition at line 201 of file BaseExpression.cpp.
RationalLiteralExpression const & storm::expressions::BaseExpression::asRationalLiteralExpression | ( | ) | const |
Definition at line 169 of file BaseExpression.cpp.
UnaryBooleanFunctionExpression const & storm::expressions::BaseExpression::asUnaryBooleanFunctionExpression | ( | ) | const |
Definition at line 177 of file BaseExpression.cpp.
UnaryNumericalFunctionExpression const & storm::expressions::BaseExpression::asUnaryNumericalFunctionExpression | ( | ) | const |
Definition at line 185 of file BaseExpression.cpp.
VariableExpression const & storm::expressions::BaseExpression::asVariableExpression | ( | ) | const |
Definition at line 193 of file BaseExpression.cpp.
|
virtual |
Retrieves whether the expression contains a variable.
Reimplemented in storm::expressions::BinaryExpression, storm::expressions::IfThenElseExpression, storm::expressions::PredicateExpression, storm::expressions::UnaryExpression, storm::expressions::VariableExpression, storm::expressions::ConstructorArrayExpression, storm::expressions::FunctionCallExpression, and storm::expressions::ValueArrayExpression.
Definition at line 85 of file BaseExpression.cpp.
|
virtual |
Evaluates the expression under the valuation of unknowns (variables and constants) 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. |
Reimplemented in storm::expressions::BinaryBooleanFunctionExpression, storm::expressions::BinaryRelationExpression, storm::expressions::BooleanLiteralExpression, storm::expressions::IfThenElseExpression, storm::expressions::PredicateExpression, storm::expressions::UnaryBooleanFunctionExpression, and storm::expressions::VariableExpression.
Definition at line 50 of file BaseExpression.cpp.
|
virtual |
Evaluates the expression under the valuation of unknowns (variables and constants) 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. |
Reimplemented in storm::expressions::BinaryNumericalFunctionExpression, storm::expressions::IfThenElseExpression, storm::expressions::IntegerLiteralExpression, storm::expressions::RationalLiteralExpression, storm::expressions::UnaryNumericalFunctionExpression, storm::expressions::VariableExpression, and storm::expressions::TranscendentalNumberLiteralExpression.
Definition at line 54 of file BaseExpression.cpp.
|
virtual |
Evaluates the expression under the valuation of unknowns (variables and constants) 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. |
Reimplemented in storm::expressions::BinaryNumericalFunctionExpression, storm::expressions::IfThenElseExpression, storm::expressions::IntegerLiteralExpression, storm::expressions::UnaryNumericalFunctionExpression, and storm::expressions::VariableExpression.
Definition at line 46 of file BaseExpression.cpp.
|
virtual |
Evaluates the expression and returns the resulting rational number.
If the return type of the expression is not a rational number or the expression could not be evaluated, an exception is thrown.
Definition at line 58 of file BaseExpression.cpp.
|
pure virtual |
Retrieves the set of all variables that appear in the expression.
The | set into which all variables in this expresson are inserted. |
Implemented in storm::expressions::BinaryExpression, storm::expressions::BooleanLiteralExpression, storm::expressions::IfThenElseExpression, storm::expressions::IntegerLiteralExpression, storm::expressions::PredicateExpression, storm::expressions::RationalLiteralExpression, storm::expressions::UnaryExpression, storm::expressions::VariableExpression, storm::expressions::ConstructorArrayExpression, storm::expressions::FunctionCallExpression, storm::expressions::TranscendentalNumberLiteralExpression, and storm::expressions::ValueArrayExpression.
|
virtual |
Returns the arity of the expression.
Reimplemented in storm::expressions::BinaryExpression, storm::expressions::IfThenElseExpression, storm::expressions::PredicateExpression, and storm::expressions::UnaryExpression.
Definition at line 63 of file BaseExpression.cpp.
|
virtual |
Retrieves the identifier associated with this expression.
This is only legal to call if the expression is a variable.
Reimplemented in storm::expressions::VariableExpression.
Definition at line 72 of file BaseExpression.cpp.
ExpressionManager const & storm::expressions::BaseExpression::getManager | ( | ) | const |
Retrieves the manager responsible for this expression.
Definition at line 109 of file BaseExpression.cpp.
|
virtual |
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. |
Reimplemented in storm::expressions::BinaryExpression, storm::expressions::IfThenElseExpression, storm::expressions::PredicateExpression, and storm::expressions::UnaryExpression.
Definition at line 67 of file BaseExpression.cpp.
|
virtual |
Retrieves the operator of a function application.
This is only legal to call if the expression is function application.
Reimplemented in storm::expressions::BinaryBooleanFunctionExpression, storm::expressions::BinaryNumericalFunctionExpression, storm::expressions::BinaryRelationExpression, storm::expressions::IfThenElseExpression, storm::expressions::PredicateExpression, storm::expressions::UnaryBooleanFunctionExpression, and storm::expressions::UnaryNumericalFunctionExpression.
Definition at line 76 of file BaseExpression.cpp.
std::shared_ptr< BaseExpression const > storm::expressions::BaseExpression::getSharedPointer | ( | ) | const |
Retrieves a shared pointer to this expression.
Definition at line 113 of file BaseExpression.cpp.
Type const & storm::expressions::BaseExpression::getType | ( | ) | const |
Retrieves the type of the expression.
Definition at line 22 of file BaseExpression.cpp.
bool storm::expressions::BaseExpression::hasBitVectorType | ( | ) | const |
Retrieves whether the expression has a bitvector type.
Definition at line 30 of file BaseExpression.cpp.
bool storm::expressions::BaseExpression::hasBooleanType | ( | ) | const |
Retrieves whether the expression has a boolean type.
Definition at line 38 of file BaseExpression.cpp.
bool storm::expressions::BaseExpression::hasIntegerType | ( | ) | const |
Retrieves whether the expression has an integer type.
Definition at line 26 of file BaseExpression.cpp.
bool storm::expressions::BaseExpression::hasNumericalType | ( | ) | const |
Retrieves whether the expression has a numerical type, i.e., integer or double.
Definition at line 34 of file BaseExpression.cpp.
bool storm::expressions::BaseExpression::hasRationalType | ( | ) | const |
Retrieves whether the expression has a rational return type.
Definition at line 42 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::BinaryBooleanFunctionExpression.
Definition at line 125 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::BinaryNumericalFunctionExpression.
Definition at line 133 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::BinaryRelationExpression.
Definition at line 141 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::BooleanLiteralExpression.
Definition at line 149 of file BaseExpression.cpp.
|
virtual |
Checks if the expression is equal to the boolean literal false.
Reimplemented in storm::expressions::BooleanLiteralExpression.
Definition at line 101 of file BaseExpression.cpp.
|
virtual |
Checks if the expression is a function application (of any sort).
Reimplemented in storm::expressions::BinaryExpression, storm::expressions::IfThenElseExpression, storm::expressions::PredicateExpression, and storm::expressions::UnaryExpression.
Definition at line 105 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::IfThenElseExpression.
Definition at line 117 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::IntegerLiteralExpression.
Definition at line 157 of file BaseExpression.cpp.
|
virtual |
Retrieves whether the expression is a literal.
Reimplemented in storm::expressions::BooleanLiteralExpression, storm::expressions::IntegerLiteralExpression, storm::expressions::RationalLiteralExpression, and storm::expressions::TranscendentalNumberLiteralExpression.
Definition at line 89 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::PredicateExpression.
Definition at line 197 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::RationalLiteralExpression.
Definition at line 165 of file BaseExpression.cpp.
|
virtual |
Checks if the expression is equal to the boolean literal true.
Reimplemented in storm::expressions::BooleanLiteralExpression.
Definition at line 97 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::UnaryBooleanFunctionExpression.
Definition at line 173 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::UnaryNumericalFunctionExpression.
Definition at line 181 of file BaseExpression.cpp.
|
virtual |
Retrieves whether the expression is a variable.
Reimplemented in storm::expressions::VariableExpression.
Definition at line 93 of file BaseExpression.cpp.
|
virtual |
Reimplemented in storm::expressions::VariableExpression.
Definition at line 189 of file BaseExpression.cpp.
|
delete |
|
delete |
|
protectedpure virtual |
Prints the expression to the given stream.
stream | The stream to which to write the expression. |
Implemented in storm::expressions::BinaryBooleanFunctionExpression, storm::expressions::BinaryNumericalFunctionExpression, storm::expressions::BinaryRelationExpression, storm::expressions::BooleanLiteralExpression, storm::expressions::IfThenElseExpression, storm::expressions::IntegerLiteralExpression, storm::expressions::PredicateExpression, storm::expressions::RationalLiteralExpression, storm::expressions::UnaryBooleanFunctionExpression, storm::expressions::UnaryNumericalFunctionExpression, storm::expressions::VariableExpression, storm::expressions::ArrayAccessExpression, storm::expressions::ConstructorArrayExpression, storm::expressions::FunctionCallExpression, storm::expressions::TranscendentalNumberLiteralExpression, and storm::expressions::ValueArrayExpression.
std::shared_ptr< BaseExpression const > storm::expressions::BaseExpression::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 80 of file BaseExpression.cpp.
|
pure virtual |
Simplifies the expression according to some simple rules.
Implemented in storm::expressions::BinaryBooleanFunctionExpression, storm::expressions::BinaryNumericalFunctionExpression, storm::expressions::BinaryRelationExpression, storm::expressions::BooleanLiteralExpression, storm::expressions::IfThenElseExpression, storm::expressions::IntegerLiteralExpression, storm::expressions::PredicateExpression, storm::expressions::RationalLiteralExpression, storm::expressions::UnaryBooleanFunctionExpression, storm::expressions::UnaryNumericalFunctionExpression, storm::expressions::VariableExpression, storm::expressions::ArrayAccessExpression, storm::expressions::ConstructorArrayExpression, storm::expressions::FunctionCallExpression, storm::expressions::TranscendentalNumberLiteralExpression, and storm::expressions::ValueArrayExpression.
Expression storm::expressions::BaseExpression::toExpression | ( | ) | const |
Converts the base expression to a proper expression.
Definition at line 18 of file BaseExpression.cpp.
|
friend |
Definition at line 205 of file BaseExpression.cpp.