Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BinaryNumericalFunctionExpression.cpp
Go to the documentation of this file.
1#include "storm/storage/expressions/BinaryNumericalFunctionExpression.h"
2
3#include <algorithm>
4#include <cmath>
5#include <optional>
6
7#include "storm/adapters/RationalNumberAdapter.h"
8#include "storm/exceptions/InvalidTypeException.h"
9#include "storm/storage/expressions/ExpressionVisitor.h"
10#include "storm/storage/expressions/IntegerLiteralExpression.h"
11#include "storm/storage/expressions/OperatorType.h"
12#include "storm/storage/expressions/RationalLiteralExpression.h"
13#include "storm/utility/NumberTraits.h"
14#include "storm/utility/constants.h"
15#include "storm/utility/macros.h"
16
17namespace storm {
18namespace expressions {
19BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ExpressionManager const& manager, Type const& type,
20 std::shared_ptr<BaseExpression const> const& firstOperand,
21 std::shared_ptr<BaseExpression const> const& secondOperand, OperatorType operatorType)
22 : BinaryExpression(manager, type, firstOperand, secondOperand), operatorType(operatorType) {
23 // Intentionally left empty.
24}
25
29
63
64template<typename V>
65V logHelper(V const& x, V const& b) {
66 // There is no std::log method for arbitrary bases.
67 // This catches common cases which should yield more accurate results
68 if (b == static_cast<V>(2)) {
69 return std::log2(x);
70 } else if (b == static_cast<V>(10)) {
71 return std::log10(x);
72 } else {
73 return std::log2(x) / std::log2(b);
74 }
75}
76
77int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const {
78 STORM_LOG_THROW(this->hasIntegerType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
79
80 int_fast64_t firstOperandEvaluation = this->getFirstOperand()->evaluateAsInt(valuation);
81 int_fast64_t secondOperandEvaluation = this->getSecondOperand()->evaluateAsInt(valuation);
82 int_fast64_t result = 0;
83 switch (this->getOperatorType()) {
84 case OperatorType::Plus:
85 result = firstOperandEvaluation + secondOperandEvaluation;
86 break;
87 case OperatorType::Minus:
88 result = firstOperandEvaluation - secondOperandEvaluation;
89 break;
90 case OperatorType::Times:
91 result = firstOperandEvaluation * secondOperandEvaluation;
92 break;
93 case OperatorType::Divide:
94 result = firstOperandEvaluation / secondOperandEvaluation;
95 break;
96 case OperatorType::Min:
97 result = std::min(firstOperandEvaluation, secondOperandEvaluation);
98 break;
99 case OperatorType::Max:
100 result = std::max(firstOperandEvaluation, secondOperandEvaluation);
101 break;
102 case OperatorType::Power:
103 result = static_cast<int_fast64_t>(std::pow(firstOperandEvaluation, secondOperandEvaluation));
104 break;
105 case OperatorType::Modulo:
106 result = firstOperandEvaluation % secondOperandEvaluation;
107 break;
108 case OperatorType::Logarithm:
109 result = logHelper(firstOperandEvaluation, secondOperandEvaluation);
110 break;
111 }
112 return result;
113}
114
115double BinaryNumericalFunctionExpression::evaluateAsDouble(Valuation const* valuation) const {
116 STORM_LOG_THROW(this->hasNumericalType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
117
118 double firstOperandEvaluation = this->getFirstOperand()->evaluateAsDouble(valuation);
119 double secondOperandEvaluation = this->getSecondOperand()->evaluateAsDouble(valuation);
120 double result = 0;
121 switch (this->getOperatorType()) {
122 case OperatorType::Plus:
123 result = firstOperandEvaluation + secondOperandEvaluation;
124 break;
125 case OperatorType::Minus:
126 result = firstOperandEvaluation - secondOperandEvaluation;
127 break;
128 case OperatorType::Times:
129 result = firstOperandEvaluation * secondOperandEvaluation;
130 break;
131 case OperatorType::Divide:
132 result = firstOperandEvaluation / secondOperandEvaluation;
133 break;
134 case OperatorType::Min:
135 result = std::min(firstOperandEvaluation, secondOperandEvaluation);
136 break;
137 case OperatorType::Max:
138 result = std::max(firstOperandEvaluation, secondOperandEvaluation);
139 break;
140 case OperatorType::Power:
141 result = std::pow(firstOperandEvaluation, secondOperandEvaluation);
142 break;
143 case OperatorType::Modulo:
144 result = std::fmod(firstOperandEvaluation, secondOperandEvaluation);
145 break;
146 case OperatorType::Logarithm:
147 result = logHelper(firstOperandEvaluation, secondOperandEvaluation);
148 break;
149 }
150 return result;
151}
152
153std::shared_ptr<BaseExpression const> BinaryNumericalFunctionExpression::simplify() const {
154 std::shared_ptr<BaseExpression const> firstOperandSimplified = this->getFirstOperand()->simplify();
155 std::shared_ptr<BaseExpression const> secondOperandSimplified = this->getSecondOperand()->simplify();
156
157 if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) {
158 if (this->hasIntegerType()) {
159 int_fast64_t firstOperandEvaluation = firstOperandSimplified->evaluateAsInt();
160 int_fast64_t secondOperandEvaluation = secondOperandSimplified->evaluateAsInt();
161 std::optional<int_fast64_t> newValue;
162 switch (this->getOperatorType()) {
163 case OperatorType::Plus:
164 newValue = firstOperandEvaluation + secondOperandEvaluation;
165 break;
166 case OperatorType::Minus:
167 newValue = firstOperandEvaluation - secondOperandEvaluation;
168 break;
169 case OperatorType::Times:
170 newValue = firstOperandEvaluation * secondOperandEvaluation;
171 break;
172 case OperatorType::Min:
173 newValue = std::min(firstOperandEvaluation, secondOperandEvaluation);
174 break;
175 case OperatorType::Max:
176 newValue = std::max(firstOperandEvaluation, secondOperandEvaluation);
177 break;
178 case OperatorType::Power:
179 if (secondOperandEvaluation >= 0) {
180 // Only simplify if this evaluates to an integer.
181 // Otherwise, we note that the type of this expression could change due to simplifications (which might or might not be expected)
182 newValue = static_cast<int_fast64_t>(std::pow(firstOperandEvaluation, secondOperandEvaluation));
183 }
184 break;
185 case OperatorType::Modulo:
186 newValue = firstOperandEvaluation % secondOperandEvaluation;
187 break;
188 case OperatorType::Logarithm:
189 // Do not simplify as it is not clear how a non-integer result should be treated.
190 break;
191 case OperatorType::Divide:
192 if (firstOperandEvaluation % secondOperandEvaluation == 0) {
193 // Only simplify if there is no remainder, because otherwise it is not clear whether we want integer division or floating point
194 // division. Otherwise, we note that the type of this expression could change due to simplifications (which might or might not be
195 // expected)
196 newValue = firstOperandEvaluation / secondOperandEvaluation;
197 }
198 break;
199 }
200 if (newValue) {
201 return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), newValue.value()));
202 }
203 } else if (this->hasRationalType()) {
204 storm::RationalNumber firstOperandEvaluation = firstOperandSimplified->evaluateAsRational();
205 storm::RationalNumber secondOperandEvaluation = secondOperandSimplified->evaluateAsRational();
206 std::optional<storm::RationalNumber> newValue;
207 switch (this->getOperatorType()) {
208 case OperatorType::Plus:
209 newValue = firstOperandEvaluation + secondOperandEvaluation;
210 break;
211 case OperatorType::Minus:
212 newValue = firstOperandEvaluation - secondOperandEvaluation;
213 break;
214 case OperatorType::Times:
215 newValue = firstOperandEvaluation * secondOperandEvaluation;
216 break;
217 case OperatorType::Min:
218 newValue = std::min(firstOperandEvaluation, secondOperandEvaluation);
219 break;
220 case OperatorType::Max:
221 newValue = std::max(firstOperandEvaluation, secondOperandEvaluation);
222 break;
223 case OperatorType::Divide:
224 newValue = firstOperandEvaluation / secondOperandEvaluation;
225 break;
226 case OperatorType::Power: {
227 if (carl::isInteger(secondOperandEvaluation)) {
228 auto exponent = carl::toInt<carl::sint>(secondOperandEvaluation);
229 if (exponent >= 0) {
230 newValue = carl::pow(firstOperandEvaluation, exponent);
231 } else {
232 storm::RationalNumber power = carl::pow(firstOperandEvaluation, -exponent);
233 newValue = storm::utility::one<storm::RationalNumber>() / power;
234 }
235 }
236 break;
237 }
238 case OperatorType::Modulo: {
239 if (carl::isInteger(firstOperandEvaluation) && carl::isInteger(secondOperandEvaluation)) {
240 newValue = storm::utility::mod(storm::utility::numerator(firstOperandEvaluation), storm::utility::numerator(secondOperandEvaluation));
241 }
242 break;
243 }
244 case OperatorType::Logarithm:
245 // Do not simplify as it is not clear how a non-rational result should be treated.
246 break;
247 }
248 if (newValue) {
249 return std::shared_ptr<BaseExpression>(new RationalLiteralExpression(this->getManager(), newValue.value()));
250 }
251 }
252 }
253
254 if (firstOperandSimplified.get() == this->getFirstOperand().get() && secondOperandSimplified.get() == this->getSecondOperand().get()) {
255 return this->shared_from_this();
256 } else {
257 return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getManager(), this->getType(), firstOperandSimplified,
258 secondOperandSimplified, this->getOperatorType()));
259 }
260}
261
262boost::any BinaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
263 return visitor.visit(*this, data);
264}
265
269
270void BinaryNumericalFunctionExpression::printToStream(std::ostream& stream) const {
271 stream << "(";
272 switch (this->getOperatorType()) {
273 case OperatorType::Plus:
274 stream << *this->getFirstOperand() << " + " << *this->getSecondOperand();
275 break;
276 case OperatorType::Minus:
277 stream << *this->getFirstOperand() << " - " << *this->getSecondOperand();
278 break;
279 case OperatorType::Times:
280 stream << *this->getFirstOperand() << " * " << *this->getSecondOperand();
281 break;
282 case OperatorType::Divide:
283 stream << *this->getFirstOperand() << " / " << *this->getSecondOperand();
284 break;
285 case OperatorType::Min:
286 stream << "min(" << *this->getFirstOperand() << ", " << *this->getSecondOperand() << ")";
287 break;
288 case OperatorType::Max:
289 stream << "max(" << *this->getFirstOperand() << ", " << *this->getSecondOperand() << ")";
290 break;
291 case OperatorType::Power:
292 stream << *this->getFirstOperand() << " ^ " << *this->getSecondOperand();
293 break;
294 case OperatorType::Modulo:
295 stream << *this->getFirstOperand() << " % " << *this->getSecondOperand();
296 break;
297 case OperatorType::Logarithm:
298 stream << "log(" << *this->getFirstOperand() << ", " << *this->getSecondOperand() << ")";
299 break;
300 }
301 stream << ")";
302}
303} // namespace expressions
304} // namespace storm
storm::expressions::BaseExpression::getManager
ExpressionManager const & getManager() const
Retrieves the manager responsible for this expression.
Definition BaseExpression.cpp:109
storm::expressions::BaseExpression::hasIntegerType
bool hasIntegerType() const
Retrieves whether the expression has an integer type.
Definition BaseExpression.cpp:26
storm::expressions::BaseExpression::hasRationalType
bool hasRationalType() const
Retrieves whether the expression has a rational return type.
Definition BaseExpression.cpp:42
storm::expressions::BaseExpression::hasNumericalType
bool hasNumericalType() const
Retrieves whether the expression has a numerical type, i.e., integer or double.
Definition BaseExpression.cpp:34
storm::expressions::BaseExpression::getType
Type const & getType() const
Retrieves the type of the expression.
Definition BaseExpression.cpp:22
storm::expressions::BinaryExpression
The base class of all binary expressions.
Definition BinaryExpression.h:12
storm::expressions::BinaryExpression::getSecondOperand
std::shared_ptr< BaseExpression const > const & getSecondOperand() const
Retrieves the second operand of the expression.
Definition BinaryExpression.cpp:31
storm::expressions::BinaryExpression::getFirstOperand
std::shared_ptr< BaseExpression const > const & getFirstOperand() const
Retrieves the first operand of the expression.
Definition BinaryExpression.cpp:27
storm::expressions::BinaryNumericalFunctionExpression::evaluateAsDouble
virtual double evaluateAsDouble(Valuation const *valuation=nullptr) const override
Evaluates the expression under the valuation of unknowns (variables and constants) given by the valua...
Definition BinaryNumericalFunctionExpression.cpp:115
storm::expressions::BinaryNumericalFunctionExpression::getOperatorType
OperatorType getOperatorType() const
Retrieves the operator associated with the expression.
Definition BinaryNumericalFunctionExpression.cpp:26
storm::expressions::BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression
BinaryNumericalFunctionExpression(ExpressionManager const &manager, Type const &type, std::shared_ptr< BaseExpression const > const &firstOperand, std::shared_ptr< BaseExpression const > const &secondOperand, OperatorType operatorType)
Constructs a binary numerical function expression with the given return type, operands and operator.
Definition BinaryNumericalFunctionExpression.cpp:19
storm::expressions::BinaryNumericalFunctionExpression::accept
virtual boost::any accept(ExpressionVisitor &visitor, boost::any const &data) const override
Accepts the given visitor by calling its visit method.
Definition BinaryNumericalFunctionExpression.cpp:262
storm::expressions::BinaryNumericalFunctionExpression::printToStream
virtual void printToStream(std::ostream &stream) const override
Prints the expression to the given stream.
Definition BinaryNumericalFunctionExpression.cpp:270
storm::expressions::BinaryNumericalFunctionExpression::getOperator
virtual storm::expressions::OperatorType getOperator() const override
Retrieves the operator of a function application.
Definition BinaryNumericalFunctionExpression.cpp:30
storm::expressions::BinaryNumericalFunctionExpression::evaluateAsInt
virtual int_fast64_t evaluateAsInt(Valuation const *valuation=nullptr) const override
Evaluates the expression under the valuation of unknowns (variables and constants) given by the valua...
Definition BinaryNumericalFunctionExpression.cpp:77
storm::expressions::BinaryNumericalFunctionExpression::OperatorType
OperatorType
An enum type specifying the different operators applicable.
Definition BinaryNumericalFunctionExpression.h:14
storm::expressions::BinaryNumericalFunctionExpression::simplify
virtual std::shared_ptr< BaseExpression const > simplify() const override
Simplifies the expression according to some simple rules.
Definition BinaryNumericalFunctionExpression.cpp:153
storm::expressions::ExpressionManager
This class is responsible for managing a set of typed variables and all expressions using these varia...
Definition ExpressionManager.h:72
storm::expressions::ExpressionVisitor::visit
virtual boost::any visit(IfThenElseExpression const &expression, boost::any const &data)=0
storm::expressions::Valuation
The base class of all valuations of variables.
Definition Valuation.h:16
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
storm::expressions::logHelper
V logHelper(V const &x, V const &b)
Definition BinaryNumericalFunctionExpression.cpp:65
storm::utility::numerator
NumberTraits< RationalType >::IntegerType numerator(RationalType const &number)
storm::utility::mod
IntegerType mod(IntegerType const &first, IntegerType const &second)
Definition constants.cpp:321