2#include <unordered_map>
20namespace expressions {
127 return this->expressionPtr == other.expressionPtr;
131 std::set<storm::expressions::Variable> result;
141 std::set<storm::expressions::Variable> appearingVariables = this->
getVariables();
142 for (
auto const& v : variables) {
143 if (appearingVariables.count(v) > 0) {
152 return visitor.
check(*
this);
170 return *this->expressionPtr;
174 return this->expressionPtr;
225 return static_cast<bool>(compiledExpression);
229 this->compiledExpression = compiledExpression;
233 return *compiledExpression;
237 std::stringstream stream;
246 stream <<
"__storm::notinitialized__";
258 return Expression(std::shared_ptr<BaseExpression>(
268 return second + first;
349 return Expression(std::shared_ptr<BaseExpression>(
357 return Expression(std::shared_ptr<BaseExpression>(
369 return Expression(std::shared_ptr<BaseExpression>(
376 return Expression(std::shared_ptr<BaseExpression>(
383 return Expression(std::shared_ptr<BaseExpression>(
390 return Expression(std::shared_ptr<BaseExpression>(
428 return Expression(std::shared_ptr<BaseExpression>(
482 return ite(first < 0, -first, first);
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());
502 std::shared_ptr<BaseExpression>(
new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(),
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());
513 std::shared_ptr<BaseExpression>(
new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(),
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());
524 std::shared_ptr<BaseExpression>(
new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(),
536Expression sum(std::vector<storm::expressions::Expression>
const& expressions) {
541 return first % second;
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();
573 for (; it !=
ite; ++it) {
574 result = function(result, *it);
582 return Expression(std::shared_ptr<BaseExpression>(
589 STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException,
"Cannot build function application of empty expression list.");
592 if (expressions.size() >= 4) {
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);
601 nonliterals.push_back(expression);
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();
611 *opIt = function(*opIt, operands.back());
616 if (nonliterals.empty()) {
617 return literals.front();
618 }
else if (literals.empty()) {
619 return nonliterals.front();
621 return function(literals.front(), nonliterals.front());
624 return apply(expressions, function);
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 logicalConnective(Type const &other) const
Type modulo(Type const &other) const
Type logarithm(Type const &other) const
Type divide(Type const &other) const
Type power(Type const &other, bool allowIntegerType=false) const
Type numericalComparison(Type const &other) const
Type plusMinusTimes(Type const &other) const
Type ite(Type const &thenType, Type const &elseType) const
Type trigonometric() const
Type minimumMaximum(Type const &other) const
The base class of all valuations of variables.
#define STORM_LOG_THROW(cond, exception, message)
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)