Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Expression.cpp
Go to the documentation of this file.
1#include <map>
2#include <unordered_map>
3
18
19namespace storm {
20namespace expressions {
28static void assertSameManager(BaseExpression const& a, BaseExpression const& b) {
29 STORM_LOG_THROW(a.getManager() == b.getManager(), storm::exceptions::InvalidArgumentException, "Expressions are managed by different manager.");
30}
31
32// Spell out destructor explicitly so we can use forward declarations in the header.
34 // Intentionally left empty.
35}
36
37Expression::Expression(std::shared_ptr<BaseExpression const> const& expressionPtr) : expressionPtr(expressionPtr) {
38 // Intentionally left empty.
39}
40
41Expression::Expression(Variable const& variable) : expressionPtr(std::shared_ptr<BaseExpression>(new VariableExpression(variable))) {
42 // Intentionally left empty.
43}
44
45Expression Expression::changeManager(ExpressionManager const& newExpressionManager) const {
46 ChangeManagerVisitor visitor(newExpressionManager);
47 return visitor.changeManager(*this);
48}
49
50Expression Expression::substitute(std::map<Variable, Expression> const& identifierToExpressionMap) const {
51 return SubstitutionVisitor<std::map<Variable, Expression>>(identifierToExpressionMap).substitute(*this);
52}
53
54Expression Expression::substitute(std::unordered_map<Variable, Expression> const& identifierToExpressionMap) const {
55 return SubstitutionVisitor<std::unordered_map<Variable, Expression>>(identifierToExpressionMap).substitute(*this);
56}
57
61
62bool Expression::evaluateAsBool(Valuation const* valuation) const {
63 return this->getBaseExpression().evaluateAsBool(valuation);
64}
65
66int_fast64_t Expression::evaluateAsInt(Valuation const* valuation) const {
67 return this->getBaseExpression().evaluateAsInt(valuation);
68}
69
70double Expression::evaluateAsDouble(Valuation const* valuation) const {
71 return this->getBaseExpression().evaluateAsDouble(valuation);
72}
73
74storm::RationalNumber Expression::evaluateAsRational() const {
76}
77
81
85
89
93
94uint_fast64_t Expression::getArity() const {
95 return this->getBaseExpression().getArity();
96}
97
98Expression Expression::getOperand(uint_fast64_t operandIndex) const {
99 return Expression(this->getBaseExpression().getOperand(operandIndex));
100}
101
102std::string const& Expression::getIdentifier() const {
103 return this->getBaseExpression().getIdentifier();
104}
105
107 return this->getBaseExpression().containsVariables();
108}
109
111 return this->getBaseExpression().isLiteral();
112}
113
115 return this->getBaseExpression().isVariable();
116}
117
118bool Expression::isTrue() const {
119 return this->getBaseExpression().isTrue();
120}
121
123 return this->getBaseExpression().isFalse();
124}
125
127 return this->expressionPtr == other.expressionPtr;
128}
129
130std::set<storm::expressions::Variable> Expression::getVariables() const {
131 std::set<storm::expressions::Variable> result;
132 this->getBaseExpression().gatherVariables(result);
133 return result;
134}
135
136void Expression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
137 this->getBaseExpression().gatherVariables(variables);
138}
139
140bool Expression::containsVariable(std::set<storm::expressions::Variable> const& variables) const {
141 std::set<storm::expressions::Variable> appearingVariables = this->getVariables();
142 for (auto const& v : variables) {
143 if (appearingVariables.count(v) > 0) {
144 return true;
145 }
146 }
147 return false;
148}
149
150bool Expression::containsVariableInITEGuard(std::set<storm::expressions::Variable> const& variables) const {
151 CheckIfThenElseGuardVisitor visitor(variables);
152 return visitor.check(*this);
153}
154
156 if (!this->isFunctionApplication()) {
157 return false;
158 }
159
163}
164
166 return LinearityCheckVisitor().check(*this);
167}
168
170 return *this->expressionPtr;
171}
172
173std::shared_ptr<BaseExpression const> const& Expression::getBaseExpressionPointer() const {
174 return this->expressionPtr;
175}
176
178 return this->getBaseExpression().getManager();
179}
180
181Type const& Expression::getType() const {
182 return this->getBaseExpression().getType();
183}
184
186 return this->getBaseExpression().hasNumericalType();
187}
188
190 return this->getBaseExpression().hasRationalType();
191}
192
194 return this->getBaseExpression().hasBooleanType();
195}
196
198 return this->getBaseExpression().hasIntegerType();
199}
200
202 return this->getBaseExpression().hasBitVectorType();
203}
204
205boost::any Expression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
206 return this->getBaseExpression().accept(visitor, data);
207}
208
210 if (this->getBaseExpressionPointer()) {
211 return true;
212 }
213 return false;
214}
215
217 if (this->getBaseExpressionPointer() == other.getBaseExpressionPointer()) {
218 return true;
219 }
221 return checker.isSyntacticallyEqual(*this, other);
222}
223
225 return static_cast<bool>(compiledExpression);
226}
227
228void Expression::setCompiledExpression(std::shared_ptr<CompiledExpression> const& compiledExpression) const {
229 this->compiledExpression = compiledExpression;
230}
231
233 return *compiledExpression;
234}
235
236std::string Expression::toString() const {
237 std::stringstream stream;
238 stream << *this;
239 return stream.str();
240}
241
242std::ostream& operator<<(std::ostream& stream, Expression const& expression) {
243 if (expression.isInitialized()) {
244 stream << expression.getBaseExpression();
245 } else {
246 stream << "__storm::notinitialized__";
247 }
248 return stream;
249}
250
251Expression operator+(Expression const& first, Expression const& second) {
252 if (!first.isInitialized()) {
253 return second;
254 } else if (!second.isInitialized()) {
255 return first;
256 }
258 return Expression(std::shared_ptr<BaseExpression>(
261}
262
263Expression operator+(Expression const& first, int64_t second) {
264 return first + Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second)));
265}
266
267Expression operator+(int64_t first, Expression const& second) {
268 return second + first;
269}
270
277
278Expression operator-(Expression const& first, int64_t second) {
279 return first - Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second)));
280}
281
282Expression operator-(int64_t first, Expression const& second) {
283 return Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(second.getBaseExpression().getManager(), first))) - second;
284}
285
291
298
305
306Expression operator%(Expression const& first, Expression const& second) {
308 // First we compute the remainder
309 Expression remainder(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(
312
313 // Deal with negative `first` in accordance with Prism
314 return storm::expressions::ite(first >= 0, remainder, remainder + second);
315}
316
317Expression operator&&(Expression const& first, Expression const& second) {
318 if (!first.isInitialized()) {
319 return second;
320 } else if (!second.isInitialized()) {
321 return first;
322 }
324 return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(
327}
328
329Expression operator||(Expression const& first, Expression const& second) {
330 if (!first.isInitialized()) {
331 return second;
332 } else if (!second.isInitialized()) {
333 return first;
334 }
336 return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(
339}
340
346
347Expression operator==(Expression const& first, Expression const& second) {
349 return Expression(std::shared_ptr<BaseExpression>(
352}
353
354Expression operator!=(Expression const& first, Expression const& second) {
356 if (first.hasNumericalType() && second.hasNumericalType()) {
357 return Expression(std::shared_ptr<BaseExpression>(
360 } else {
361 return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(
364 }
365}
366
367Expression operator>(Expression const& first, Expression const& second) {
369 return Expression(std::shared_ptr<BaseExpression>(
372}
373
374Expression operator>=(Expression const& first, Expression const& second) {
376 return Expression(std::shared_ptr<BaseExpression>(
379}
380
381Expression operator<(Expression const& first, Expression const& second) {
383 return Expression(std::shared_ptr<BaseExpression>(
386}
387
388Expression operator<=(Expression const& first, Expression const& second) {
390 return Expression(std::shared_ptr<BaseExpression>(
393}
394
395Expression operator<(Expression const& first, int64_t second) {
396 return first < Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second)));
397}
398
399Expression operator>(Expression const& first, int64_t second) {
400 return first > Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second)));
401}
402
403Expression operator<=(Expression const& first, int64_t second) {
404 return first <= Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second)));
405}
406
407Expression operator>=(Expression const& first, int64_t second) {
408 return first >= Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second)));
409}
410
417
424
425Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression) {
426 assertSameManager(condition.getBaseExpression(), thenExpression.getBaseExpression());
427 assertSameManager(thenExpression.getBaseExpression(), elseExpression.getBaseExpression());
428 return Expression(std::shared_ptr<BaseExpression>(
429 new IfThenElseExpression(condition.getBaseExpression().getManager(), condition.getType().ite(thenExpression.getType(), elseExpression.getType()),
430 condition.getBaseExpressionPointer(), thenExpression.getBaseExpressionPointer(), elseExpression.getBaseExpressionPointer())));
431}
432
439
446
453
454Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType) {
456 return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(
457 base.getBaseExpression().getManager(), base.getType().power(exponent.getType(), allowIntegerType), base.getBaseExpressionPointer(),
459}
460
462 STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand.");
463 return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(),
466}
467
469 STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'ceil' requires numerical operand.");
470 return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(),
473}
474
476 STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'round' requires numerical operand.");
477 return floor(first + first.getManager().rational(0.5));
478}
479
480Expression abs(Expression const& first) {
481 STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Abs is only defined for numerical operands");
482 return ite(first < 0, -first, first);
483}
484
486 STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Sign is only defined for numerical operands");
487 return ite(first > 0, first.getManager().integer(1), ite(first < 0, first.getManager().integer(0), first.getManager().integer(0)));
488}
489
491 STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Truncate is only defined for numerical operands");
492 return ite(first < 0, floor(first), ceil(first));
493}
494
495Expression atLeastOneOf(std::vector<Expression> const& expressions) {
496 STORM_LOG_THROW(expressions.size() > 0, storm::exceptions::InvalidArgumentException, "AtLeastOneOf requires arguments");
497 std::vector<std::shared_ptr<BaseExpression const>> baseexpressions;
498 for (auto const& expr : expressions) {
499 baseexpressions.push_back(expr.getBaseExpressionPointer());
500 }
501 return Expression(
502 std::shared_ptr<BaseExpression>(new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(),
504}
505
506Expression atMostOneOf(std::vector<Expression> const& expressions) {
507 STORM_LOG_THROW(expressions.size() > 0, storm::exceptions::InvalidArgumentException, "AtMostOneOf requires arguments");
508 std::vector<std::shared_ptr<BaseExpression const>> baseexpressions;
509 for (auto const& expr : expressions) {
510 baseexpressions.push_back(expr.getBaseExpressionPointer());
511 }
512 return Expression(
513 std::shared_ptr<BaseExpression>(new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(),
515}
516
517Expression exactlyOneOf(std::vector<Expression> const& expressions) {
518 STORM_LOG_THROW(expressions.size() > 0, storm::exceptions::InvalidArgumentException, "ExactlyOneOf requires arguments");
519 std::vector<std::shared_ptr<BaseExpression const>> baseexpressions;
520 for (auto const& expr : expressions) {
521 baseexpressions.push_back(expr.getBaseExpressionPointer());
522 }
523 return Expression(
524 std::shared_ptr<BaseExpression>(new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(),
526}
527
528Expression disjunction(std::vector<storm::expressions::Expression> const& expressions) {
529 return applyAssociative(expressions, [](Expression const& e1, Expression const& e2) { return e1 || e2; });
530}
531
532Expression conjunction(std::vector<storm::expressions::Expression> const& expressions) {
533 return applyAssociative(expressions, [](Expression const& e1, Expression const& e2) { return e1 && e2; });
534}
535
536Expression sum(std::vector<storm::expressions::Expression> const& expressions) {
537 return applyAssociative(expressions, [](Expression const& e1, Expression const& e2) { return e1 + e2; });
538}
539
540Expression modulo(Expression const& first, Expression const& second) {
541 return first % second;
542}
543
550
551Expression cos(Expression const& first) {
552 STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'cos' requires numerical operand.");
553 return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(),
556}
557
558Expression sin(Expression const& first) {
559 STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'sin' requires numerical operand.");
560 return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(),
563}
564
565Expression apply(std::vector<storm::expressions::Expression> const& expressions,
566 std::function<Expression(Expression const&, Expression const&)> const& function) {
567 STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build function application of empty expression list.");
568 auto it = expressions.begin();
569 auto ite = expressions.end();
570 Expression result = *it;
571 ++it;
572
573 for (; it != ite; ++it) {
574 result = function(result, *it);
575 }
576
577 return result;
578}
579
580Expression makeBinaryRelationExpression(Expression const& first, Expression const& second, RelationType const& reltype) {
582 return Expression(std::shared_ptr<BaseExpression>(
584 first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), reltype)));
585}
586
587Expression applyAssociative(std::vector<storm::expressions::Expression> const& expressions,
588 std::function<Expression(Expression const&, Expression const&)> const& function) {
589 STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build function application of empty expression list.");
590
591 // Balance the syntax tree if there are enough operands
592 if (expressions.size() >= 4) {
593 // we treat operands and literals seperately so that a subsequent call to simplify() is more successful (see, e.g., (a + 1) + (b + 1))
594 std::vector<std::vector<storm::expressions::Expression>> operandTypes(2);
595 auto& nonliterals = operandTypes[0];
596 auto& literals = operandTypes[1];
597 for (auto const& expression : expressions) {
598 if (expression.isLiteral()) {
599 literals.push_back(expression);
600 } else {
601 nonliterals.push_back(expression);
602 }
603 }
604
605 for (auto& operands : operandTypes) {
606 auto opIt = operands.begin();
607 while (operands.size() > 1) {
608 if (opIt == operands.end() || opIt == operands.end() - 1) {
609 opIt = operands.begin();
610 }
611 *opIt = function(*opIt, operands.back());
612 operands.pop_back();
613 ++opIt;
614 }
615 }
616 if (nonliterals.empty()) {
617 return literals.front();
618 } else if (literals.empty()) {
619 return nonliterals.front();
620 } else {
621 return function(literals.front(), nonliterals.front());
622 }
623 } else {
624 return apply(expressions, function);
625 }
626}
627} // namespace expressions
628} // namespace storm
The base class of all expression classes.
bool hasBooleanType() const
Retrieves whether the expression has a boolean type.
virtual storm::RationalNumber evaluateAsRational() const
Evaluates the expression and returns the resulting rational number.
virtual boost::any accept(ExpressionVisitor &visitor, boost::any const &data) const =0
Accepts the given visitor by calling its visit method.
virtual std::string const & getIdentifier() const
Retrieves the identifier associated with this expression.
virtual void gatherVariables(std::set< storm::expressions::Variable > &variables) const =0
Retrieves the set of all variables that appear in the expression.
virtual bool isFunctionApplication() const
Checks if the expression is a function application (of any sort).
virtual bool isFalse() const
Checks if the expression is equal to the boolean literal false.
ExpressionManager const & getManager() const
Retrieves the manager responsible for this expression.
virtual double evaluateAsDouble(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of unknowns (variables and constants) given by the valua...
virtual bool isVariable() const
Retrieves whether the expression is a variable.
bool hasIntegerType() const
Retrieves whether the expression has an integer type.
bool hasBitVectorType() const
Retrieves whether the expression has a bitvector type.
virtual bool evaluateAsBool(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of unknowns (variables and constants) given by the valua...
virtual bool isLiteral() const
Retrieves whether the expression is a literal.
bool hasRationalType() const
Retrieves whether the expression has a rational return type.
bool hasNumericalType() const
Retrieves whether the expression has a numerical type, i.e., integer or double.
virtual bool isTrue() const
Checks if the expression is equal to the boolean literal true.
Type const & getType() const
Retrieves the type of the expression.
virtual uint_fast64_t getArity() const
Returns the arity of the expression.
virtual bool containsVariables() const
Retrieves whether the expression contains a variable.
virtual OperatorType getOperator() const
Retrieves the operator of a function application.
virtual int_fast64_t evaluateAsInt(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of unknowns (variables and constants) given by the valua...
Expression changeManager(storm::expressions::Expression const &expression)
bool check(storm::expressions::Expression const &expression)
Expression simplify() const
Simplifies the expression according to some basic rules.
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...
bool isLinear() const
Retrieves whether this expression is a linear expression.
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.
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...
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.
bool containsVariables() const
Retrieves whether the expression contains a variable.
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.
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.
std::shared_ptr< BaseExpression const > const & getBaseExpressionPointer() const
Retrieves a pointer to the base expression underlying this expression object.
bool hasIntegerType() const
Retrieves whether the expression has an integral return type.
BaseExpression const & getBaseExpression() const
Retrieves the base expression underlying this expression object.
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.
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.
ExpressionManager const & getManager() const
Retrieves the manager responsible for this expression.
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.
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.
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 hasCompiledExpression() const
Retrieves whether this expression object has an associated compiled expression.
bool hasBitVectorType() const
Retrieves whether the expression has an integral return type.
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.
Expression substituteNonStandardPredicates() const
Eliminate nonstandard predicates from the expression.
This class is responsible for managing a set of typed variables and all expressions using these varia...
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.
bool check(Expression const &expression, bool booleanIsLinear=false)
Checks that the given expression is linear.
The base class of all binary expressions.
Expression substitute(Expression const &expression)
Simplifies based on the configuration.
bool isSyntacticallyEqual(storm::expressions::Expression const &expression1, storm::expressions::Expression const &expression2)
Type minus() const
Definition Type.cpp:227
Type logicalConnective(Type const &other) const
Definition Type.cpp:264
Type modulo(Type const &other) const
Definition Type.cpp:239
Type logarithm(Type const &other) const
Definition Type.cpp:244
Type divide(Type const &other) const
Definition Type.cpp:232
Type power(Type const &other, bool allowIntegerType=false) const
Definition Type.cpp:249
Type numericalComparison(Type const &other) const
Definition Type.cpp:274
Type plusMinusTimes(Type const &other) const
Definition Type.cpp:222
Type ite(Type const &thenType, Type const &elseType) const
Definition Type.cpp:279
Type trigonometric() const
Definition Type.cpp:259
Type minimumMaximum(Type const &other) const
Definition Type.cpp:296
Type floorCeil() const
Definition Type.cpp:291
The base class of all valuations of variables.
Definition Valuation.h:16
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
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)
std::ostream & operator<<(std::ostream &stream, BaseExpression const &expression)
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)
static void assertSameManager(BaseExpression const &a, BaseExpression const &b)
Checks whether the two expressions share the same expression manager.
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 operator%(Expression const &first, Expression const &second)
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