Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Expression.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_
2#define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_
3
4#include <functional>
5#include <map>
6#include <memory>
7#include <unordered_map>
8#include <vector>
9
13
14namespace storm {
15namespace expressions {
16// Foward-declare expression manager class.
17class ExpressionManager;
18class Variable;
19class ExpressionVisitor;
20class CompiledExpression;
21
23 public:
24 friend class ExpressionManager;
25 friend class Variable;
26 template<typename MapType>
27 friend class SubstitutionVisitor;
28
29 friend Expression operator+(Expression const& first, Expression const& second);
30 friend Expression operator+(Expression const& first, int64_t second);
31 friend Expression operator+(int64_t first, Expression const& second);
32 friend Expression operator-(Expression const& first, Expression const& second);
33 friend Expression operator-(Expression const& first, int64_t second);
34 friend Expression operator-(int64_t first, Expression const& second);
35 friend Expression operator-(Expression const& first);
36 friend Expression operator*(Expression const& first, Expression const& second);
37 friend Expression operator/(Expression const& first, Expression const& second);
38 friend Expression operator%(Expression const& first, Expression const& second);
39 friend Expression operator&&(Expression const& first, Expression const& second);
40 friend Expression operator||(Expression const& first, Expression const& second);
41 friend Expression operator!(Expression const& first);
42 friend Expression operator==(Expression const& first, Expression const& second);
43 friend Expression operator!=(Expression const& first, Expression const& second);
44 friend Expression operator>(Expression const& first, Expression const& second);
45 friend Expression operator>=(Expression const& first, Expression const& second);
46 friend Expression operator<(Expression const& first, Expression const& second);
47 friend Expression operator<=(Expression const& first, Expression const& second);
48 friend Expression operator>(Expression const& first, int64_t second);
49 friend Expression operator>=(Expression const& first, int64_t second);
50 friend Expression operator<(Expression const& first, int64_t second);
51 friend Expression operator<=(Expression const& first, int64_t second);
52 friend Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression);
53 friend Expression implies(Expression const& first, Expression const& second);
54 friend Expression iff(Expression const& first, Expression const& second);
55 friend Expression xclusiveor(Expression const& first, Expression const& second);
56 friend Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType);
57 friend Expression abs(Expression const& first);
58 friend Expression truncate(Expression const& first);
59 friend Expression sign(Expression const& first);
60 friend Expression floor(Expression const& first);
61 friend Expression ceil(Expression const& first);
62 friend Expression round(Expression const& first);
63 friend Expression minimum(Expression const& first, Expression const& second);
64 friend Expression maximum(Expression const& first, Expression const& second);
65
66 Expression() = default;
68
74 Expression(Variable const& variable);
75
81 Expression(std::shared_ptr<BaseExpression const> const& expressionPtr);
82
83 // Instantiate constructors and assignments with their default implementations.
84 Expression(Expression const& other) = default;
85 Expression& operator=(Expression const& other) = default;
86 Expression(Expression&&) = default;
88
92 Expression changeManager(ExpressionManager const& newExpressionManager) const;
93
103 Expression substitute(std::map<Variable, Expression> const& variableToExpressionMap) const;
104
119 Expression substitute(std::unordered_map<Variable, Expression> const& variableToExpressionMap) const;
120
128 bool evaluateAsBool(Valuation const* valuation = nullptr) const;
129
137 int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const;
138
146 double evaluateAsDouble(Valuation const* valuation = nullptr) const;
147
155 storm::RationalNumber evaluateAsRational() const;
156
162 Expression simplify() const;
163
170
178
184 bool isFunctionApplication() const;
185
191 uint_fast64_t getArity() const;
192
199 Expression getOperand(uint_fast64_t operandIndex) const;
200
207 std::string const& getIdentifier() const;
208
214 bool containsVariables() const;
215
221 bool isLiteral() const;
222
228 bool isVariable() const;
229
235 bool isTrue() const;
236
242 bool isFalse() const;
243
250 bool areSame(storm::expressions::Expression const& other) const;
251
258 bool isRelationalExpression() const;
259
265 bool isLinear() const;
266
272 std::set<storm::expressions::Variable> getVariables() const;
273
280 void gatherVariables(std::set<storm::expressions::Variable>& variables) const;
281
288 bool containsVariable(std::set<storm::expressions::Variable> const& variables) const;
289
297 bool containsVariableInITEGuard(std::set<storm::expressions::Variable> const& variables) const;
298
305 BaseExpression const& getBaseExpression() const;
306
312 std::shared_ptr<BaseExpression const> const& getBaseExpressionPointer() const;
313
319 ExpressionManager const& getManager() const;
320
326 Type const& getType() const;
327
333 bool hasNumericalType() const;
334
340 bool hasRationalType() const;
341
347 bool hasBooleanType() const;
348
354 bool hasIntegerType() const;
355
361 bool hasBitVectorType() const;
362
368 boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const;
369
375 std::string toString() const;
376
380 bool isInitialized() const;
381
386
390 bool hasCompiledExpression() const;
391
395 void setCompiledExpression(std::shared_ptr<CompiledExpression> const& compiledExpression) const;
396
401
402 friend std::ostream& operator<<(std::ostream& stream, Expression const& expression);
403
404 private:
405 // A pointer to the underlying base expression.
406 std::shared_ptr<BaseExpression const> expressionPtr;
407
408 // A pointer to an associated compiled expression object (if any).
409 mutable std::shared_ptr<CompiledExpression> compiledExpression;
410};
411
412// Provide operator overloads to conveniently construct new expressions from other expressions.
413Expression operator+(Expression const& first, Expression const& second);
414Expression operator+(Expression const& first, int64_t second);
415Expression operator+(int64_t first, Expression const& second);
416Expression operator-(Expression const& first, Expression const& second);
417Expression operator-(Expression const& first, int64_t second);
418Expression operator-(int64_t first, Expression const& second);
419Expression operator-(Expression const& first);
420Expression operator*(Expression const& first, Expression const& second);
421Expression operator/(Expression const& first, Expression const& second);
422Expression operator&&(Expression const& first, Expression const& second);
423Expression operator||(Expression const& first, Expression const& second);
424Expression operator!(Expression const& first);
425Expression operator==(Expression const& first, Expression const& second);
426Expression operator!=(Expression const& first, Expression const& second);
427Expression operator>(Expression const& first, Expression const& second);
428Expression operator>=(Expression const& first, Expression const& second);
429Expression operator<(Expression const& first, Expression const& second);
430Expression operator<=(Expression const& first, Expression const& second);
431Expression operator>(Expression const& first, int64_t second);
432Expression operator>=(Expression const& first, int64_t second);
433Expression operator<(Expression const& first, int64_t second);
434Expression operator<=(Expression const& first, int64_t second);
435Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression);
436Expression implies(Expression const& first, Expression const& second);
437Expression iff(Expression const& first, Expression const& second);
438Expression xclusiveor(Expression const& first, Expression const& second);
439
448Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType = false);
449Expression abs(Expression const& first);
450Expression truncate(Expression const& first);
451Expression sign(Expression const& first);
452Expression floor(Expression const& first);
453Expression ceil(Expression const& first);
454Expression round(Expression const& first);
455Expression modulo(Expression const& first, Expression const& second);
456Expression logarithm(Expression const& first, Expression const& second);
457Expression cos(Expression const& first);
458Expression sin(Expression const& first);
459Expression minimum(Expression const& first, Expression const& second);
460Expression maximum(Expression const& first, Expression const& second);
461Expression atLeastOneOf(std::vector<storm::expressions::Expression> const& expressions);
462Expression atMostOneOf(std::vector<storm::expressions::Expression> const& expressions);
463Expression exactlyOneOf(std::vector<storm::expressions::Expression> const& expressions);
464Expression disjunction(std::vector<storm::expressions::Expression> const& expressions);
465Expression conjunction(std::vector<storm::expressions::Expression> const& expressions);
466Expression sum(std::vector<storm::expressions::Expression> const& expressions);
467Expression apply(std::vector<storm::expressions::Expression> const& expressions,
468 std::function<Expression(Expression const&, Expression const&)> const& function);
469Expression applyAssociative(std::vector<storm::expressions::Expression> const& expressions,
470 std::function<Expression(Expression const&, Expression const&)> const& function);
471Expression makeBinaryRelationExpression(Expression const& lhs, Expression const& rhs, RelationType const& reltype);
472} // namespace expressions
473} // namespace storm
474
475namespace std {
476template<>
477struct less<storm::expressions::Expression> {
478 bool operator()(storm::expressions::Expression const& lhs, storm::expressions::Expression const& rhs) const {
480 }
481};
482
483template<>
484struct hash<storm::expressions::Expression> {
485 size_t operator()(storm::expressions::Expression const& e) const {
486 return reinterpret_cast<size_t>(e.getBaseExpressionPointer().get());
487 }
488};
489
490template<>
491struct equal_to<storm::expressions::Expression> {
492 bool operator()(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2) const {
493 return e1.areSame(e2);
494 }
495};
496} // namespace std
497
498#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ */
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.
Definition Valuation.h:16
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)
LabParser.cpp.
Definition cli.cpp:18