1#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_
2#define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_
7#include <unordered_map>
15namespace expressions {
17class ExpressionManager;
19class ExpressionVisitor;
20class CompiledExpression;
26 template<
typename MapType>
81 Expression(std::shared_ptr<BaseExpression const>
const& expressionPtr);
119 Expression substitute(std::unordered_map<Variable, Expression>
const& variableToExpressionMap)
const;
272 std::set<storm::expressions::Variable>
getVariables()
const;
280 void gatherVariables(std::set<storm::expressions::Variable>& variables)
const;
288 bool containsVariable(std::set<storm::expressions::Variable>
const& variables)
const;
406 std::shared_ptr<BaseExpression const> expressionPtr;
409 mutable std::shared_ptr<CompiledExpression> compiledExpression;
466Expression sum(std::vector<storm::expressions::Expression>
const& expressions);
467Expression apply(std::vector<storm::expressions::Expression>
const& expressions,
477struct less<
storm::expressions::Expression> {
484struct hash<
storm::expressions::Expression> {
491struct equal_to<
storm::expressions::Expression> {
The base class of all expression classes.
friend Expression truncate(Expression const &first)
Expression simplify() const
Simplifies the expression according to some basic rules.
friend Expression operator==(Expression const &first, Expression const &second)
friend Expression maximum(Expression const &first, Expression const &second)
friend Expression implies(Expression const &first, Expression const &second)
int_fast64_t evaluateAsInt(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
bool isVariable() const
Retrieves whether the expression is a variable.
OperatorType getOperator() const
Retrieves the operator of a function application.
bool hasNumericalType() const
Retrieves whether the expression has a numerical return type, i.e., integer or double.
bool evaluateAsBool(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
friend Expression pow(Expression const &base, Expression const &exponent, bool allowIntegerType)
The type of the resulting expression is.
bool isLinear() const
Retrieves whether this expression is a linear expression.
friend Expression operator||(Expression const &first, Expression const &second)
Expression reduceNesting() const
Tries to flatten the syntax tree of the expression, e.g., 1 + (2 + (3 + 4)) becomes (1 + 2) + (3 + 4)
double evaluateAsDouble(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
storm::RationalNumber evaluateAsRational() const
Evaluates the expression and returns the resulting rational number.
bool hasBooleanType() const
Retrieves whether the expression has a boolean return type.
friend Expression operator>(Expression const &first, Expression const &second)
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 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-IfTh...
friend Expression minimum(Expression const &first, Expression const &second)
Expression(Expression &&)=default
void setCompiledExpression(std::shared_ptr< CompiledExpression > const &compiledExpression) const
Associates the given compiled expression with this expression object.
bool isFalse() const
Checks if the expression is equal to the boolean literal false.
Expression & operator=(Expression const &other)=default
bool containsVariables() const
Retrieves whether the expression contains a variable.
friend Expression operator+(Expression const &first, Expression const &second)
friend Expression ite(Expression const &condition, Expression const &thenExpression, Expression const &elseExpression)
friend Expression operator/(Expression const &first, Expression const &second)
boost::any accept(ExpressionVisitor &visitor, boost::any const &data) const
Accepts the given visitor.
std::set< storm::expressions::Variable > getVariables() const
Retrieves the set of all variables that appear in the expression.
friend Expression xclusiveor(Expression const &first, Expression const &second)
bool isRelationalExpression() const
Retrieves whether this expression is a relation expression, i.e., an expression that has a relation (...
Expression changeManager(ExpressionManager const &newExpressionManager) const
Converts the expression to an expression over the variables of the provided expression manager.
friend Expression operator<(Expression const &first, Expression const &second)
std::shared_ptr< BaseExpression const > const & getBaseExpressionPointer() const
Retrieves a pointer to the base expression underlying this expression object.
friend Expression operator&&(Expression const &first, Expression const &second)
bool hasIntegerType() const
Retrieves whether the expression has an integral return type.
BaseExpression const & getBaseExpression() const
Retrieves the base expression underlying this expression object.
friend Expression operator!=(Expression const &first, Expression const &second)
friend Expression floor(Expression const &first)
friend Expression operator<=(Expression const &first, Expression const &second)
bool isFunctionApplication() const
Checks if the expression is a function application (of any sort).
bool isLiteral() const
Retrieves whether the expression is a literal.
std::string toString() const
Converts the expression into a string.
friend Expression operator!(Expression const &first)
Type const & getType() const
Retrieves the type of the expression.
bool areSame(storm::expressions::Expression const &other) const
Checks whether the two expressions are the same.
friend Expression operator%(Expression const &first, Expression const &second)
ExpressionManager const & getManager() const
Retrieves the manager responsible for this expression.
friend Expression iff(Expression const &first, Expression const &second)
Expression substitute(std::map< Variable, Expression > const &variableToExpressionMap) const
Substitutes all occurrences of the variables according to the given map.
bool isSyntacticallyEqual(storm::expressions::Expression const &other) const
Checks whether the two expressions are syntatically the same.
friend Expression operator>=(Expression const &first, Expression const &second)
bool hasRationalType() const
Retrieves whether the expression has a rational return type.
bool isTrue() const
Checks if the expression is equal to the boolean literal true.
friend Expression operator-(Expression const &first, Expression const &second)
friend Expression ceil(Expression const &first)
void gatherVariables(std::set< storm::expressions::Variable > &variables) const
Retrieves the set of all variables that appear in the expression.
Expression(Expression const &other)=default
bool containsVariable(std::set< storm::expressions::Variable > const &variables) const
Retrieves whether the expression contains any of the given variables.
bool hasCompiledExpression() const
Retrieves whether this expression object has an associated compiled expression.
friend Expression round(Expression const &first)
friend Expression sign(Expression const &first)
bool hasBitVectorType() const
Retrieves whether the expression has an integral return type.
friend std::ostream & operator<<(std::ostream &stream, Expression const &expression)
Expression & operator=(Expression &&)=default
CompiledExpression const & getCompiledExpression() const
Retrieves the associated compiled expression object (if there is any).
uint_fast64_t getArity() const
Retrieves the arity of the expression.
bool isInitialized() const
Checks whether the object encapsulates a base-expression.
friend Expression abs(Expression const &first)
Expression substituteNonStandardPredicates() const
Eliminate nonstandard predicates from the expression.
friend Expression operator*(Expression const &first, Expression const &second)
This class is responsible for managing a set of typed variables and all expressions using these varia...
The base class of all valuations of variables.
Expression maximum(Expression const &first, Expression const &second)
Expression operator*(Expression const &first, Expression const &second)
Expression atLeastOneOf(std::vector< Expression > const &expressions)
Expression round(Expression const &first)
Expression makeBinaryRelationExpression(Expression const &first, Expression const &second, RelationType const &reltype)
Expression ceil(Expression const &first)
Expression operator!=(Expression const &first, Expression const &second)
Expression ite(Expression const &condition, Expression const &thenExpression, Expression const &elseExpression)
Expression operator<(Expression const &first, Expression const &second)
Expression apply(std::vector< storm::expressions::Expression > const &expressions, std::function< Expression(Expression const &, Expression const &)> const &function)
Expression iff(Expression const &first, Expression const &second)
Expression abs(Expression const &first)
Expression sum(std::vector< storm::expressions::Expression > const &expressions)
Expression conjunction(std::vector< storm::expressions::Expression > const &expressions)
Expression operator!(Expression const &first)
Expression operator-(Expression const &first, Expression const &second)
Expression applyAssociative(std::vector< storm::expressions::Expression > const &expressions, std::function< Expression(Expression const &, Expression const &)> const &function)
Expression exactlyOneOf(std::vector< Expression > const &expressions)
Expression operator==(Expression const &first, Expression const &second)
Expression operator>=(Expression const &first, Expression const &second)
Expression atMostOneOf(std::vector< Expression > const &expressions)
Expression operator/(Expression const &first, Expression const &second)
Expression minimum(Expression const &first, Expression const &second)
Expression disjunction(std::vector< storm::expressions::Expression > const &expressions)
Expression floor(Expression const &first)
Expression sin(Expression const &first)
Expression sign(Expression const &first)
Expression truncate(Expression const &first)
Expression pow(Expression const &base, Expression const &exponent, bool allowIntegerType)
The type of the resulting expression is.
RelationType
An enum type specifying the different relations applicable.
Expression operator&&(Expression const &first, Expression const &second)
Expression operator||(Expression const &first, Expression const &second)
Expression xclusiveor(Expression const &first, Expression const &second)
Expression operator<=(Expression const &first, Expression const &second)
Expression logarithm(Expression const &first, Expression const &second)
Expression operator>(Expression const &first, Expression const &second)
Expression cos(Expression const &first)
Expression implies(Expression const &first, Expression const &second)
Expression modulo(Expression const &first, Expression const &second)
Expression operator+(Expression const &first, Expression const &second)