Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ToRationalFunctionVisitor.cpp
Go to the documentation of this file.
2
7
8namespace storm {
9namespace expressions {
10
11template<typename RationalFunctionType>
16
17template<typename RationalFunctionType>
19 return boost::any_cast<RationalFunctionType>(expression.accept(*this, boost::none));
21
22template<typename RationalFunctionType>
23boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
24 bool conditionValue = evaluator.asBool(expression.getCondition());
25 if (conditionValue) {
26 return expression.getThenExpression()->accept(*this, data);
27 } else {
28 return expression.getElseExpression()->accept(*this, data);
29 }
32template<typename RationalFunctionType>
34 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
35}
36
37template<typename RationalFunctionType>
39 RationalFunctionType firstOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getFirstOperand()->accept(*this, data));
40 RationalFunctionType secondOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getSecondOperand()->accept(*this, data));
41 switch (expression.getOperatorType()) {
43 return firstOperandAsRationalFunction + secondOperandAsRationalFunction;
45 return firstOperandAsRationalFunction - secondOperandAsRationalFunction;
47 return firstOperandAsRationalFunction * secondOperandAsRationalFunction;
49 return firstOperandAsRationalFunction / secondOperandAsRationalFunction;
51 STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalFunction), storm::exceptions::InvalidArgumentException,
52 "Exponent of power operator must be an integer but is " << secondOperandAsRationalFunction << ".");
53 auto exponentAsInteger = storm::utility::convertNumber<carl::sint>(secondOperandAsRationalFunction);
54 return storm::utility::pow(firstOperandAsRationalFunction, exponentAsInteger);
55 }
56 default:
57 STORM_LOG_ASSERT(false, "Illegal operator type " << expression.getOperator() << " in expression" << expression << ".");
58 }
59
60 // Return a dummy. This point must, however, never be reached.
61 return boost::any();
62}
63
64template<typename RationalFunctionType>
66 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
67}
68
69template<typename RationalFunctionType>
70boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(VariableExpression const& expression, boost::any const&) {
71 auto valueIt = valueMapping.find(expression.getVariable());
72 if (valueIt != valueMapping.end()) {
73 return valueIt->second;
74 }
75
76 auto variablePair = variableToVariableMap.find(expression.getVariable());
77 if (variablePair != variableToVariableMap.end()) {
78 return convertVariableToPolynomial(variablePair->second);
79 } else {
81 variableToVariableMap.emplace(expression.getVariable(), carlVariable);
82 return convertVariableToPolynomial(carlVariable);
83 }
84}
85
86template<typename RationalFunctionType>
88 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
89}
90
91template<typename RationalFunctionType>
93 RationalFunctionType operandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getOperand()->accept(*this, data));
94 switch (expression.getOperatorType()) {
96 return -operandAsRationalFunction;
97 default:
98 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
99 }
100 return boost::any();
101}
102
103template<typename RationalFunctionType>
105 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
106}
107
108template<typename RationalFunctionType>
110 return RationalFunctionType(storm::utility::convertNumber<storm::RationalFunction>(expression.getValue()));
111}
112
113template<typename RationalFunctionType>
115 return storm::utility::convertNumber<storm::RationalFunction>(expression.getValue());
116}
117
118template<typename RationalFunctionType>
120 valueMapping[variable] = value;
121}
122
124} // namespace expressions
125} // namespace storm
std::shared_ptr< BaseExpression const > const & getSecondOperand() const
Retrieves the second operand of the expression.
std::shared_ptr< BaseExpression const > const & getFirstOperand() const
Retrieves the first operand of the expression.
OperatorType getOperatorType() const
Retrieves the operator associated with the expression.
virtual storm::expressions::OperatorType getOperator() const override
Retrieves the operator of a function application.
boost::any accept(ExpressionVisitor &visitor, boost::any const &data) const
Accepts the given visitor.
std::shared_ptr< BaseExpression const > getElseExpression() const
Retrieves the else expression of the if-then-else expression.
std::shared_ptr< BaseExpression const > getCondition() const
Retrieves the condition expression of the if-then-else expression.
std::shared_ptr< BaseExpression const > getThenExpression() const
Retrieves the then expression of the if-then-else expression.
int_fast64_t getValue() const
Retrieves the value of the integer literal.
storm::RationalNumber getValue() const
Retrieves the value of the double literal.
ToRationalFunctionVisitor(ExpressionEvaluatorBase< RationalFunctionType > const &evaluator)
virtual boost::any visit(IfThenElseExpression const &expression, boost::any const &data) override
RationalFunctionType toRationalFunction(Expression const &expression)
void setMapping(storm::expressions::Variable const &variable, RationalFunctionType const &value)
virtual std::shared_ptr< BaseExpression const > getOperand(uint_fast64_t operandIndex) const override
Retrieves the given operand from the expression.
OperatorType getOperatorType() const
Retrieves the operator associated with this expression.
Variable const & getVariable() const
Retrieves the variable associated with this expression.
std::string const & getVariableName() const
Retrieves the name of the variable associated with this expression.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
bool isInteger(ValueType const &number)
ValueType pow(ValueType const &value, int_fast64_t exponent)
RationalFunctionVariable createRFVariable(std::string const &name)
carl::Variable RationalFunctionVariable