Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ToExprtkStringVisitor.cpp
Go to the documentation of this file.
2
4
5namespace storm {
6namespace expressions {
7std::string ToExprtkStringVisitor::toString(Expression const& expression) {
8 return toString(expression.getBaseExpressionPointer().get());
9}
10
11std::string ToExprtkStringVisitor::toString(BaseExpression const* expression) {
12 stream.str("");
13 stream.clear();
14 expression->accept(*this, boost::none);
15 return stream.str();
16}
17
18boost::any ToExprtkStringVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
19 stream << "if(";
20 expression.getCondition()->accept(*this, data);
21 stream << ",";
22 expression.getThenExpression()->accept(*this, data);
23 stream << ",";
24 expression.getElseExpression()->accept(*this, data);
25 stream << ")";
26 return boost::any();
27}
28
29boost::any ToExprtkStringVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
30 switch (expression.getOperatorType()) {
32 stream << "(";
33 expression.getFirstOperand()->accept(*this, data);
34 stream << " & ";
35 expression.getSecondOperand()->accept(*this, data);
36 stream << ")";
37 break;
39 stream << "(";
40 expression.getFirstOperand()->accept(*this, data);
41 stream << " | ";
42 expression.getSecondOperand()->accept(*this, data);
43 stream << ")";
44 break;
46 stream << "(";
47 expression.getFirstOperand()->accept(*this, data);
48 stream << " xor ";
49 expression.getSecondOperand()->accept(*this, data);
50 stream << ")";
51 break;
53 stream << "(not(";
54 expression.getFirstOperand()->accept(*this, data);
55 stream << ") | ";
56 expression.getSecondOperand()->accept(*this, data);
57 stream << ")";
58 break;
60 expression.getFirstOperand()->accept(*this, data);
61 stream << "==";
62 expression.getSecondOperand()->accept(*this, data);
63 break;
64 }
65 return boost::any();
66}
67
68boost::any ToExprtkStringVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
69 switch (expression.getOperatorType()) {
71 stream << "(";
72 expression.getFirstOperand()->accept(*this, data);
73 stream << "+";
74 expression.getSecondOperand()->accept(*this, data);
75 stream << ")";
76 break;
78 stream << "(";
79 expression.getFirstOperand()->accept(*this, data);
80 stream << "-";
81 expression.getSecondOperand()->accept(*this, data);
82 stream << ")";
83 break;
85 stream << "(";
86 expression.getFirstOperand()->accept(*this, data);
87 stream << "*";
88 expression.getSecondOperand()->accept(*this, data);
89 stream << ")";
90 break;
92 stream << "(";
93 expression.getFirstOperand()->accept(*this, data);
94 stream << "/";
95 expression.getSecondOperand()->accept(*this, data);
96 stream << ")";
97 break;
99 stream << "(";
100 expression.getFirstOperand()->accept(*this, data);
101 stream << "^";
102 expression.getSecondOperand()->accept(*this, data);
103 stream << ")";
104 break;
106 stream << "(";
107 expression.getFirstOperand()->accept(*this, data);
108 stream << "%";
109 expression.getSecondOperand()->accept(*this, data);
110 stream << ")";
111 break;
113 if (expression.getSecondOperand()->isLiteral()) {
114 auto base = expression.getSecondOperand()->evaluateAsRational();
115 if (base == storm::utility::convertNumber<storm::RationalNumber, uint64_t>(2ull)) {
116 stream << "log2(";
117 expression.getFirstOperand()->accept(*this, data);
118 stream << ")";
119 break;
120 } else if (base == storm::utility::convertNumber<storm::RationalNumber, uint64_t>(10ull)) {
121 stream << "log10(";
122 expression.getFirstOperand()->accept(*this, data);
123 stream << ")";
124 break;
125 }
126 }
127 stream << "logn(";
128 expression.getFirstOperand()->accept(*this, data);
129 stream << ",";
130 expression.getSecondOperand()->accept(*this, data);
131 stream << ")";
132 break;
134 stream << "max(";
135 expression.getFirstOperand()->accept(*this, data);
136 stream << ",";
137 expression.getSecondOperand()->accept(*this, data);
138 stream << ")";
139 break;
141 stream << "min(";
142 expression.getFirstOperand()->accept(*this, data);
143 stream << ",";
144 expression.getSecondOperand()->accept(*this, data);
145 stream << ")";
146 break;
147 }
148 return boost::any();
149}
150
151boost::any ToExprtkStringVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
152 switch (expression.getRelationType()) {
154 stream << "(";
155 expression.getFirstOperand()->accept(*this, data);
156 stream << "==";
157 expression.getSecondOperand()->accept(*this, data);
158 stream << ")";
159 break;
161 stream << "(";
162 expression.getFirstOperand()->accept(*this, data);
163 stream << "!=";
164 expression.getSecondOperand()->accept(*this, data);
165 stream << ")";
166 break;
168 stream << "(";
169 expression.getFirstOperand()->accept(*this, data);
170 stream << "<";
171 expression.getSecondOperand()->accept(*this, data);
172 stream << ")";
173 break;
175 stream << "(";
176 expression.getFirstOperand()->accept(*this, data);
177 stream << "<=";
178 expression.getSecondOperand()->accept(*this, data);
179 stream << ")";
180 break;
182 stream << "(";
183 expression.getFirstOperand()->accept(*this, data);
184 stream << ">";
185 expression.getSecondOperand()->accept(*this, data);
186 stream << ")";
187 break;
189 stream << "(";
190 expression.getFirstOperand()->accept(*this, data);
191 stream << ">=";
192 expression.getSecondOperand()->accept(*this, data);
193 stream << ")";
194 break;
195 }
196 return boost::any();
197}
198
199boost::any ToExprtkStringVisitor::visit(VariableExpression const& expression, boost::any const&) {
200 stream << "v" + std::to_string(expression.getVariable().getIndex());
201 return boost::any();
202}
203
204boost::any ToExprtkStringVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
205 switch (expression.getOperatorType()) {
207 stream << "not(";
208 expression.getOperand()->accept(*this, data);
209 stream << ")";
210 }
211 return boost::any();
212}
213
214boost::any ToExprtkStringVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
215 switch (expression.getOperatorType()) {
217 stream << "-(";
218 expression.getOperand()->accept(*this, data);
219 stream << ")";
220 break;
222 stream << "floor(";
223 expression.getOperand()->accept(*this, data);
224 stream << ")";
225 break;
227 stream << "ceil(";
228 expression.getOperand()->accept(*this, data);
229 stream << ")";
230 break;
232 stream << "cos(";
233 expression.getOperand()->accept(*this, data);
234 stream << ")";
235 break;
237 stream << "sin(";
238 expression.getOperand()->accept(*this, data);
239 stream << ")";
240 break;
241 }
242 return boost::any();
243}
244
245boost::any ToExprtkStringVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) {
246 stream << expression.getValue();
247 return boost::any();
248}
249
250boost::any ToExprtkStringVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) {
251 stream << expression.getValue();
252 return boost::any();
253}
254
255boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) {
256 stream << std::scientific << std::setprecision(std::numeric_limits<double>::max_digits10) << "(" << expression.getValueAsDouble() << ")";
257 return boost::any();
258}
259} // namespace expressions
260} // namespace storm
The base class of all expression classes.
virtual boost::any accept(ExpressionVisitor &visitor, boost::any const &data) const =0
Accepts the given visitor by calling its visit method.
OperatorType getOperatorType() const
Retrieves the operator associated with the expression.
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.
RelationType getRelationType() const
Retrieves the relation associated with the expression.
bool getValue() const
Retrieves the value of the boolean literal.
std::shared_ptr< BaseExpression const > const & getBaseExpressionPointer() const
Retrieves a pointer to the base expression underlying this expression object.
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.
double getValueAsDouble() const
Retrieves the value of the double literal.
std::string toString(Expression const &expression)
virtual boost::any visit(IfThenElseExpression const &expression, boost::any const &data) override
OperatorType getOperatorType() const
Retrieves the operator associated with this expression.
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.
uint_fast64_t getIndex() const
Retrieves the index of the variable.
Definition Variable.cpp:38
LabParser.cpp.
Definition cli.cpp:18