Line data Source code
1 : // Author(s): Jeroen Keiren
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/data/real.h
10 : /// \brief The standard sort real_.
11 : ///
12 : /// This file was generated from the data sort specification
13 : /// mcrl2/data/build/real.spec.
14 :
15 : #ifndef MCRL2_DATA_REAL_H
16 : #define MCRL2_DATA_REAL_H
17 :
18 : #include "functional" // std::function
19 : #include "mcrl2/utilities/exception.h"
20 : #include "mcrl2/data/basic_sort.h"
21 : #include "mcrl2/data/function_sort.h"
22 : #include "mcrl2/data/function_symbol.h"
23 : #include "mcrl2/data/application.h"
24 : #include "mcrl2/data/data_equation.h"
25 : #include "mcrl2/data/standard.h"
26 : #include "mcrl2/data/bool.h"
27 : #include "mcrl2/data/pos.h"
28 : #include "mcrl2/data/nat.h"
29 : #include "mcrl2/data/int.h"
30 :
31 : namespace mcrl2 {
32 :
33 : namespace data {
34 :
35 : /// \brief Namespace for system defined sort real_.
36 : namespace sort_real {
37 :
38 : inline
39 115 : const core::identifier_string& real_name()
40 : {
41 115 : static core::identifier_string real_name = core::identifier_string("Real");
42 115 : return real_name;
43 : }
44 :
45 : /// \brief Constructor for sort expression Real.
46 : /// \return Sort expression Real.
47 : inline
48 1111866 : const basic_sort& real_()
49 : {
50 1111866 : static basic_sort real_ = basic_sort(real_name());
51 1111866 : return real_;
52 : }
53 :
54 : /// \brief Recogniser for sort expression Real
55 : /// \param e A sort expression
56 : /// \return true iff e == real_()
57 : inline
58 232379 : bool is_real(const sort_expression& e)
59 : {
60 232379 : if (is_basic_sort(e))
61 : {
62 65304 : return basic_sort(e) == real_();
63 : }
64 167075 : return false;
65 : }
66 :
67 : /// \brief Give all system defined constructors for real_.
68 : /// \return All system defined constructors for real_.
69 : inline
70 5431 : function_symbol_vector real_generate_constructors_code()
71 : {
72 5431 : function_symbol_vector result;
73 5431 : return result;
74 : }
75 : /// \brief Give all defined constructors which can be used in mCRL2 specs for real_.
76 : /// \return All system defined constructors that can be used in an mCRL2 specification for real_.
77 : inline
78 4578 : function_symbol_vector real_mCRL2_usable_constructors()
79 : {
80 4578 : function_symbol_vector result;
81 4578 : return result;
82 : }
83 : // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
84 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
85 : /// \brief Give all system defined constructors which have an implementation in C++ and not in rewrite rules for real_.
86 : /// \return All system defined constructors that are to be implemented in C++ for real_.
87 : inline
88 : implementation_map real_cpp_implementable_constructors()
89 : {
90 : implementation_map result;
91 : return result;
92 : }
93 :
94 : /// \brief Generate identifier \@cReal.
95 : /// \return Identifier \@cReal.
96 : inline
97 113 : const core::identifier_string& creal_name()
98 : {
99 113 : static core::identifier_string creal_name = core::identifier_string("@cReal");
100 113 : return creal_name;
101 : }
102 :
103 : /// \brief Constructor for function symbol \@cReal.
104 :
105 : /// \return Function symbol creal.
106 : inline
107 411650 : const function_symbol& creal()
108 : {
109 411650 : static function_symbol creal(creal_name(), make_function_sort_(sort_int::int_(), sort_pos::pos(), real_()));
110 411650 : return creal;
111 : }
112 :
113 : /// \brief Recogniser for function \@cReal.
114 : /// \param e A data expression.
115 : /// \return true iff e is the function symbol matching \@cReal.
116 : inline
117 183813 : bool is_creal_function_symbol(const atermpp::aterm_appl& e)
118 : {
119 183813 : if (is_function_symbol(e))
120 : {
121 179835 : return atermpp::down_cast<function_symbol>(e) == creal();
122 : }
123 3978 : return false;
124 : }
125 :
126 : /// \brief Application of function symbol \@cReal.
127 :
128 : /// \param arg0 A data expression.
129 : /// \param arg1 A data expression.
130 : /// \return Application of \@cReal to a number of arguments.
131 : inline
132 216597 : application creal(const data_expression& arg0, const data_expression& arg1)
133 : {
134 216597 : return sort_real::creal()(arg0, arg1);
135 : }
136 :
137 : /// \brief Make an application of function symbol \@cReal.
138 : /// \param result The data expression where the \@cReal expression is put.
139 :
140 : /// \param arg0 A data expression.
141 : /// \param arg1 A data expression.
142 : inline
143 : void make_creal(data_expression& result, const data_expression& arg0, const data_expression& arg1)
144 : {
145 : make_application(result, sort_real::creal(),arg0, arg1);
146 : }
147 :
148 : /// \brief Recogniser for application of \@cReal.
149 : /// \param e A data expression.
150 : /// \return true iff e is an application of function symbol creal to a
151 : /// number of arguments.
152 : inline
153 186641 : bool is_creal_application(const atermpp::aterm_appl& e)
154 : {
155 186641 : return is_application(e) && is_creal_function_symbol(atermpp::down_cast<application>(e).head());
156 : }
157 :
158 : /// \brief Generate identifier Pos2Real.
159 : /// \return Identifier Pos2Real.
160 : inline
161 112 : const core::identifier_string& pos2real_name()
162 : {
163 112 : static core::identifier_string pos2real_name = core::identifier_string("Pos2Real");
164 112 : return pos2real_name;
165 : }
166 :
167 : /// \brief Constructor for function symbol Pos2Real.
168 :
169 : /// \return Function symbol pos2real.
170 : inline
171 181062 : const function_symbol& pos2real()
172 : {
173 181062 : static function_symbol pos2real(pos2real_name(), make_function_sort_(sort_pos::pos(), real_()));
174 181062 : return pos2real;
175 : }
176 :
177 : /// \brief Recogniser for function Pos2Real.
178 : /// \param e A data expression.
179 : /// \return true iff e is the function symbol matching Pos2Real.
180 : inline
181 169136 : bool is_pos2real_function_symbol(const atermpp::aterm_appl& e)
182 : {
183 169136 : if (is_function_symbol(e))
184 : {
185 165550 : return atermpp::down_cast<function_symbol>(e) == pos2real();
186 : }
187 3586 : return false;
188 : }
189 :
190 : /// \brief Application of function symbol Pos2Real.
191 :
192 : /// \param arg0 A data expression.
193 : /// \return Application of Pos2Real to a number of arguments.
194 : inline
195 5432 : application pos2real(const data_expression& arg0)
196 : {
197 5432 : return sort_real::pos2real()(arg0);
198 : }
199 :
200 : /// \brief Make an application of function symbol Pos2Real.
201 : /// \param result The data expression where the Pos2Real expression is put.
202 :
203 : /// \param arg0 A data expression.
204 : inline
205 : void make_pos2real(data_expression& result, const data_expression& arg0)
206 : {
207 : make_application(result, sort_real::pos2real(),arg0);
208 : }
209 :
210 : /// \brief Recogniser for application of Pos2Real.
211 : /// \param e A data expression.
212 : /// \return true iff e is an application of function symbol pos2real to a
213 : /// number of arguments.
214 : inline
215 171964 : bool is_pos2real_application(const atermpp::aterm_appl& e)
216 : {
217 171964 : return is_application(e) && is_pos2real_function_symbol(atermpp::down_cast<application>(e).head());
218 : }
219 :
220 : /// \brief Generate identifier Nat2Real.
221 : /// \return Identifier Nat2Real.
222 : inline
223 112 : const core::identifier_string& nat2real_name()
224 : {
225 112 : static core::identifier_string nat2real_name = core::identifier_string("Nat2Real");
226 112 : return nat2real_name;
227 : }
228 :
229 : /// \brief Constructor for function symbol Nat2Real.
230 :
231 : /// \return Function symbol nat2real.
232 : inline
233 181061 : const function_symbol& nat2real()
234 : {
235 181061 : static function_symbol nat2real(nat2real_name(), make_function_sort_(sort_nat::nat(), real_()));
236 181061 : return nat2real;
237 : }
238 :
239 : /// \brief Recogniser for function Nat2Real.
240 : /// \param e A data expression.
241 : /// \return true iff e is the function symbol matching Nat2Real.
242 : inline
243 169135 : bool is_nat2real_function_symbol(const atermpp::aterm_appl& e)
244 : {
245 169135 : if (is_function_symbol(e))
246 : {
247 165549 : return atermpp::down_cast<function_symbol>(e) == nat2real();
248 : }
249 3586 : return false;
250 : }
251 :
252 : /// \brief Application of function symbol Nat2Real.
253 :
254 : /// \param arg0 A data expression.
255 : /// \return Application of Nat2Real to a number of arguments.
256 : inline
257 5432 : application nat2real(const data_expression& arg0)
258 : {
259 5432 : return sort_real::nat2real()(arg0);
260 : }
261 :
262 : /// \brief Make an application of function symbol Nat2Real.
263 : /// \param result The data expression where the Nat2Real expression is put.
264 :
265 : /// \param arg0 A data expression.
266 : inline
267 : void make_nat2real(data_expression& result, const data_expression& arg0)
268 : {
269 : make_application(result, sort_real::nat2real(),arg0);
270 : }
271 :
272 : /// \brief Recogniser for application of Nat2Real.
273 : /// \param e A data expression.
274 : /// \return true iff e is an application of function symbol nat2real to a
275 : /// number of arguments.
276 : inline
277 171963 : bool is_nat2real_application(const atermpp::aterm_appl& e)
278 : {
279 171963 : return is_application(e) && is_nat2real_function_symbol(atermpp::down_cast<application>(e).head());
280 : }
281 :
282 : /// \brief Generate identifier Int2Real.
283 : /// \return Identifier Int2Real.
284 : inline
285 112 : const core::identifier_string& int2real_name()
286 : {
287 112 : static core::identifier_string int2real_name = core::identifier_string("Int2Real");
288 112 : return int2real_name;
289 : }
290 :
291 : /// \brief Constructor for function symbol Int2Real.
292 :
293 : /// \return Function symbol int2real.
294 : inline
295 181074 : const function_symbol& int2real()
296 : {
297 181074 : static function_symbol int2real(int2real_name(), make_function_sort_(sort_int::int_(), real_()));
298 181074 : return int2real;
299 : }
300 :
301 : /// \brief Recogniser for function Int2Real.
302 : /// \param e A data expression.
303 : /// \return true iff e is the function symbol matching Int2Real.
304 : inline
305 169134 : bool is_int2real_function_symbol(const atermpp::aterm_appl& e)
306 : {
307 169134 : if (is_function_symbol(e))
308 : {
309 165548 : return atermpp::down_cast<function_symbol>(e) == int2real();
310 : }
311 3586 : return false;
312 : }
313 :
314 : /// \brief Application of function symbol Int2Real.
315 :
316 : /// \param arg0 A data expression.
317 : /// \return Application of Int2Real to a number of arguments.
318 : inline
319 5446 : application int2real(const data_expression& arg0)
320 : {
321 5446 : return sort_real::int2real()(arg0);
322 : }
323 :
324 : /// \brief Make an application of function symbol Int2Real.
325 : /// \param result The data expression where the Int2Real expression is put.
326 :
327 : /// \param arg0 A data expression.
328 : inline
329 : void make_int2real(data_expression& result, const data_expression& arg0)
330 : {
331 : make_application(result, sort_real::int2real(),arg0);
332 : }
333 :
334 : /// \brief Recogniser for application of Int2Real.
335 : /// \param e A data expression.
336 : /// \return true iff e is an application of function symbol int2real to a
337 : /// number of arguments.
338 : inline
339 171962 : bool is_int2real_application(const atermpp::aterm_appl& e)
340 : {
341 171962 : return is_application(e) && is_int2real_function_symbol(atermpp::down_cast<application>(e).head());
342 : }
343 :
344 : /// \brief Generate identifier Real2Pos.
345 : /// \return Identifier Real2Pos.
346 : inline
347 112 : const core::identifier_string& real2pos_name()
348 : {
349 112 : static core::identifier_string real2pos_name = core::identifier_string("Real2Pos");
350 112 : return real2pos_name;
351 : }
352 :
353 : /// \brief Constructor for function symbol Real2Pos.
354 :
355 : /// \return Function symbol real2pos.
356 : inline
357 15511 : const function_symbol& real2pos()
358 : {
359 15511 : static function_symbol real2pos(real2pos_name(), make_function_sort_(real_(), sort_pos::pos()));
360 15511 : return real2pos;
361 : }
362 :
363 : /// \brief Recogniser for function Real2Pos.
364 : /// \param e A data expression.
365 : /// \return true iff e is the function symbol matching Real2Pos.
366 : inline
367 : bool is_real2pos_function_symbol(const atermpp::aterm_appl& e)
368 : {
369 : if (is_function_symbol(e))
370 : {
371 : return atermpp::down_cast<function_symbol>(e) == real2pos();
372 : }
373 : return false;
374 : }
375 :
376 : /// \brief Application of function symbol Real2Pos.
377 :
378 : /// \param arg0 A data expression.
379 : /// \return Application of Real2Pos to a number of arguments.
380 : inline
381 5431 : application real2pos(const data_expression& arg0)
382 : {
383 5431 : return sort_real::real2pos()(arg0);
384 : }
385 :
386 : /// \brief Make an application of function symbol Real2Pos.
387 : /// \param result The data expression where the Real2Pos expression is put.
388 :
389 : /// \param arg0 A data expression.
390 : inline
391 : void make_real2pos(data_expression& result, const data_expression& arg0)
392 : {
393 : make_application(result, sort_real::real2pos(),arg0);
394 : }
395 :
396 : /// \brief Recogniser for application of Real2Pos.
397 : /// \param e A data expression.
398 : /// \return true iff e is an application of function symbol real2pos to a
399 : /// number of arguments.
400 : inline
401 : bool is_real2pos_application(const atermpp::aterm_appl& e)
402 : {
403 : return is_application(e) && is_real2pos_function_symbol(atermpp::down_cast<application>(e).head());
404 : }
405 :
406 : /// \brief Generate identifier Real2Nat.
407 : /// \return Identifier Real2Nat.
408 : inline
409 112 : const core::identifier_string& real2nat_name()
410 : {
411 112 : static core::identifier_string real2nat_name = core::identifier_string("Real2Nat");
412 112 : return real2nat_name;
413 : }
414 :
415 : /// \brief Constructor for function symbol Real2Nat.
416 :
417 : /// \return Function symbol real2nat.
418 : inline
419 15511 : const function_symbol& real2nat()
420 : {
421 15511 : static function_symbol real2nat(real2nat_name(), make_function_sort_(real_(), sort_nat::nat()));
422 15511 : return real2nat;
423 : }
424 :
425 : /// \brief Recogniser for function Real2Nat.
426 : /// \param e A data expression.
427 : /// \return true iff e is the function symbol matching Real2Nat.
428 : inline
429 : bool is_real2nat_function_symbol(const atermpp::aterm_appl& e)
430 : {
431 : if (is_function_symbol(e))
432 : {
433 : return atermpp::down_cast<function_symbol>(e) == real2nat();
434 : }
435 : return false;
436 : }
437 :
438 : /// \brief Application of function symbol Real2Nat.
439 :
440 : /// \param arg0 A data expression.
441 : /// \return Application of Real2Nat to a number of arguments.
442 : inline
443 5431 : application real2nat(const data_expression& arg0)
444 : {
445 5431 : return sort_real::real2nat()(arg0);
446 : }
447 :
448 : /// \brief Make an application of function symbol Real2Nat.
449 : /// \param result The data expression where the Real2Nat expression is put.
450 :
451 : /// \param arg0 A data expression.
452 : inline
453 : void make_real2nat(data_expression& result, const data_expression& arg0)
454 : {
455 : make_application(result, sort_real::real2nat(),arg0);
456 : }
457 :
458 : /// \brief Recogniser for application of Real2Nat.
459 : /// \param e A data expression.
460 : /// \return true iff e is an application of function symbol real2nat to a
461 : /// number of arguments.
462 : inline
463 : bool is_real2nat_application(const atermpp::aterm_appl& e)
464 : {
465 : return is_application(e) && is_real2nat_function_symbol(atermpp::down_cast<application>(e).head());
466 : }
467 :
468 : /// \brief Generate identifier Real2Int.
469 : /// \return Identifier Real2Int.
470 : inline
471 112 : const core::identifier_string& real2int_name()
472 : {
473 112 : static core::identifier_string real2int_name = core::identifier_string("Real2Int");
474 112 : return real2int_name;
475 : }
476 :
477 : /// \brief Constructor for function symbol Real2Int.
478 :
479 : /// \return Function symbol real2int.
480 : inline
481 15512 : const function_symbol& real2int()
482 : {
483 15512 : static function_symbol real2int(real2int_name(), make_function_sort_(real_(), sort_int::int_()));
484 15512 : return real2int;
485 : }
486 :
487 : /// \brief Recogniser for function Real2Int.
488 : /// \param e A data expression.
489 : /// \return true iff e is the function symbol matching Real2Int.
490 : inline
491 : bool is_real2int_function_symbol(const atermpp::aterm_appl& e)
492 : {
493 : if (is_function_symbol(e))
494 : {
495 : return atermpp::down_cast<function_symbol>(e) == real2int();
496 : }
497 : return false;
498 : }
499 :
500 : /// \brief Application of function symbol Real2Int.
501 :
502 : /// \param arg0 A data expression.
503 : /// \return Application of Real2Int to a number of arguments.
504 : inline
505 5432 : application real2int(const data_expression& arg0)
506 : {
507 5432 : return sort_real::real2int()(arg0);
508 : }
509 :
510 : /// \brief Make an application of function symbol Real2Int.
511 : /// \param result The data expression where the Real2Int expression is put.
512 :
513 : /// \param arg0 A data expression.
514 : inline
515 : void make_real2int(data_expression& result, const data_expression& arg0)
516 : {
517 : make_application(result, sort_real::real2int(),arg0);
518 : }
519 :
520 : /// \brief Recogniser for application of Real2Int.
521 : /// \param e A data expression.
522 : /// \return true iff e is an application of function symbol real2int to a
523 : /// number of arguments.
524 : inline
525 : bool is_real2int_application(const atermpp::aterm_appl& e)
526 : {
527 : return is_application(e) && is_real2int_function_symbol(atermpp::down_cast<application>(e).head());
528 : }
529 :
530 : /// \brief Generate identifier max.
531 : /// \return Identifier max.
532 : inline
533 16503 : const core::identifier_string& maximum_name()
534 : {
535 16503 : static core::identifier_string maximum_name = core::identifier_string("max");
536 16503 : return maximum_name;
537 : }
538 :
539 : // This function is not intended for public use and therefore not documented in Doxygen.
540 : inline
541 16477 : function_symbol maximum(const sort_expression& s0, const sort_expression& s1)
542 : {
543 16477 : sort_expression target_sort;
544 16477 : if (s0 == real_() && s1 == real_())
545 : {
546 15838 : target_sort = real_();
547 : }
548 639 : else if (s0 == sort_pos::pos() && s1 == sort_int::int_())
549 : {
550 71 : target_sort = sort_pos::pos();
551 : }
552 568 : else if (s0 == sort_int::int_() && s1 == sort_pos::pos())
553 : {
554 71 : target_sort = sort_pos::pos();
555 : }
556 497 : else if (s0 == sort_nat::nat() && s1 == sort_int::int_())
557 : {
558 71 : target_sort = sort_nat::nat();
559 : }
560 426 : else if (s0 == sort_int::int_() && s1 == sort_nat::nat())
561 : {
562 71 : target_sort = sort_nat::nat();
563 : }
564 355 : else if (s0 == sort_int::int_() && s1 == sort_int::int_())
565 : {
566 71 : target_sort = sort_int::int_();
567 : }
568 284 : else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
569 : {
570 71 : target_sort = sort_pos::pos();
571 : }
572 213 : else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
573 : {
574 71 : target_sort = sort_pos::pos();
575 : }
576 142 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
577 : {
578 71 : target_sort = sort_nat::nat();
579 : }
580 71 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
581 : {
582 71 : target_sort = sort_pos::pos();
583 : }
584 : else
585 : {
586 0 : throw mcrl2::runtime_error("Cannot compute target sort for maximum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
587 : }
588 :
589 16477 : function_symbol maximum(maximum_name(), make_function_sort_(s0, s1, target_sort));
590 32954 : return maximum;
591 16477 : }
592 :
593 : /// \brief Recogniser for function max.
594 : /// \param e A data expression.
595 : /// \return true iff e is the function symbol matching max.
596 : inline
597 26 : bool is_maximum_function_symbol(const atermpp::aterm_appl& e)
598 : {
599 26 : if (is_function_symbol(e))
600 : {
601 26 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
602 26 : return f.name() == maximum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == maximum(real_(), real_()) || f == maximum(sort_pos::pos(), sort_int::int_()) || f == maximum(sort_int::int_(), sort_pos::pos()) || f == maximum(sort_nat::nat(), sort_int::int_()) || f == maximum(sort_int::int_(), sort_nat::nat()) || f == maximum(sort_int::int_(), sort_int::int_()) || f == maximum(sort_pos::pos(), sort_nat::nat()) || f == maximum(sort_nat::nat(), sort_pos::pos()) || f == maximum(sort_nat::nat(), sort_nat::nat()) || f == maximum(sort_pos::pos(), sort_pos::pos()));
603 : }
604 0 : return false;
605 : }
606 :
607 : /// \brief Application of function symbol max.
608 :
609 : /// \param arg0 A data expression.
610 : /// \param arg1 A data expression.
611 : /// \return Application of max to a number of arguments.
612 : inline
613 5748 : application maximum(const data_expression& arg0, const data_expression& arg1)
614 : {
615 11496 : return sort_real::maximum(arg0.sort(), arg1.sort())(arg0, arg1);
616 : }
617 :
618 : /// \brief Make an application of function symbol max.
619 : /// \param result The data expression where the max expression is put.
620 :
621 : /// \param arg0 A data expression.
622 : /// \param arg1 A data expression.
623 : inline
624 : void make_maximum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
625 : {
626 : make_application(result, sort_real::maximum(arg0.sort(), arg1.sort()),arg0, arg1);
627 : }
628 :
629 : /// \brief Recogniser for application of max.
630 : /// \param e A data expression.
631 : /// \return true iff e is an application of function symbol maximum to a
632 : /// number of arguments.
633 : inline
634 26 : bool is_maximum_application(const atermpp::aterm_appl& e)
635 : {
636 26 : return is_application(e) && is_maximum_function_symbol(atermpp::down_cast<application>(e).head());
637 : }
638 :
639 : /// \brief Generate identifier min.
640 : /// \return Identifier min.
641 : inline
642 15884 : const core::identifier_string& minimum_name()
643 : {
644 15884 : static core::identifier_string minimum_name = core::identifier_string("min");
645 15884 : return minimum_name;
646 : }
647 :
648 : // This function is not intended for public use and therefore not documented in Doxygen.
649 : inline
650 15858 : function_symbol minimum(const sort_expression& s0, const sort_expression& s1)
651 : {
652 15858 : sort_expression target_sort;
653 15858 : if (s0 == real_() && s1 == real_())
654 : {
655 15645 : target_sort = real_();
656 : }
657 213 : else if (s0 == sort_int::int_() && s1 == sort_int::int_())
658 : {
659 71 : target_sort = sort_int::int_();
660 : }
661 142 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
662 : {
663 71 : target_sort = sort_nat::nat();
664 : }
665 71 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
666 : {
667 71 : target_sort = sort_pos::pos();
668 : }
669 : else
670 : {
671 0 : throw mcrl2::runtime_error("Cannot compute target sort for minimum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
672 : }
673 :
674 15858 : function_symbol minimum(minimum_name(), make_function_sort_(s0, s1, target_sort));
675 31716 : return minimum;
676 15858 : }
677 :
678 : /// \brief Recogniser for function min.
679 : /// \param e A data expression.
680 : /// \return true iff e is the function symbol matching min.
681 : inline
682 26 : bool is_minimum_function_symbol(const atermpp::aterm_appl& e)
683 : {
684 26 : if (is_function_symbol(e))
685 : {
686 26 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
687 26 : return f.name() == minimum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minimum(real_(), real_()) || f == minimum(sort_int::int_(), sort_int::int_()) || f == minimum(sort_nat::nat(), sort_nat::nat()) || f == minimum(sort_pos::pos(), sort_pos::pos()));
688 : }
689 0 : return false;
690 : }
691 :
692 : /// \brief Application of function symbol min.
693 :
694 : /// \param arg0 A data expression.
695 : /// \param arg1 A data expression.
696 : /// \return Application of min to a number of arguments.
697 : inline
698 5555 : application minimum(const data_expression& arg0, const data_expression& arg1)
699 : {
700 11110 : return sort_real::minimum(arg0.sort(), arg1.sort())(arg0, arg1);
701 : }
702 :
703 : /// \brief Make an application of function symbol min.
704 : /// \param result The data expression where the min expression is put.
705 :
706 : /// \param arg0 A data expression.
707 : /// \param arg1 A data expression.
708 : inline
709 : void make_minimum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
710 : {
711 : make_application(result, sort_real::minimum(arg0.sort(), arg1.sort()),arg0, arg1);
712 : }
713 :
714 : /// \brief Recogniser for application of min.
715 : /// \param e A data expression.
716 : /// \return true iff e is an application of function symbol minimum to a
717 : /// number of arguments.
718 : inline
719 26 : bool is_minimum_application(const atermpp::aterm_appl& e)
720 : {
721 26 : return is_application(e) && is_minimum_function_symbol(atermpp::down_cast<application>(e).head());
722 : }
723 :
724 : /// \brief Generate identifier abs.
725 : /// \return Identifier abs.
726 : inline
727 15584 : const core::identifier_string& abs_name()
728 : {
729 15584 : static core::identifier_string abs_name = core::identifier_string("abs");
730 15584 : return abs_name;
731 : }
732 :
733 : // This function is not intended for public use and therefore not documented in Doxygen.
734 : inline
735 15584 : function_symbol abs(const sort_expression& s0)
736 : {
737 15584 : sort_expression target_sort;
738 15584 : if (s0 == real_())
739 : {
740 15513 : target_sort = real_();
741 : }
742 71 : else if (s0 == sort_int::int_())
743 : {
744 71 : target_sort = sort_nat::nat();
745 : }
746 : else
747 : {
748 0 : throw mcrl2::runtime_error("Cannot compute target sort for abs with domain sorts " + pp(s0) + ". ");
749 : }
750 :
751 15584 : function_symbol abs(abs_name(), make_function_sort_(s0, target_sort));
752 31168 : return abs;
753 15584 : }
754 :
755 : /// \brief Recogniser for function abs.
756 : /// \param e A data expression.
757 : /// \return true iff e is the function symbol matching abs.
758 : inline
759 0 : bool is_abs_function_symbol(const atermpp::aterm_appl& e)
760 : {
761 0 : if (is_function_symbol(e))
762 : {
763 0 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
764 0 : return f.name() == abs_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == abs(real_()) || f == abs(sort_int::int_()));
765 : }
766 0 : return false;
767 : }
768 :
769 : /// \brief Application of function symbol abs.
770 :
771 : /// \param arg0 A data expression.
772 : /// \return Application of abs to a number of arguments.
773 : inline
774 5432 : application abs(const data_expression& arg0)
775 : {
776 10864 : return sort_real::abs(arg0.sort())(arg0);
777 : }
778 :
779 : /// \brief Make an application of function symbol abs.
780 : /// \param result The data expression where the abs expression is put.
781 :
782 : /// \param arg0 A data expression.
783 : inline
784 : void make_abs(data_expression& result, const data_expression& arg0)
785 : {
786 : make_application(result, sort_real::abs(arg0.sort()),arg0);
787 : }
788 :
789 : /// \brief Recogniser for application of abs.
790 : /// \param e A data expression.
791 : /// \return true iff e is an application of function symbol abs to a
792 : /// number of arguments.
793 : inline
794 0 : bool is_abs_application(const atermpp::aterm_appl& e)
795 : {
796 0 : return is_application(e) && is_abs_function_symbol(atermpp::down_cast<application>(e).head());
797 : }
798 :
799 : /// \brief Generate identifier -.
800 : /// \return Identifier -.
801 : inline
802 63532 : const core::identifier_string& negate_name()
803 : {
804 63532 : static core::identifier_string negate_name = core::identifier_string("-");
805 63532 : return negate_name;
806 : }
807 :
808 : // This function is not intended for public use and therefore not documented in Doxygen.
809 : inline
810 42899 : function_symbol negate(const sort_expression& s0)
811 : {
812 42899 : sort_expression target_sort;
813 42899 : if (s0 == real_())
814 : {
815 26393 : target_sort = real_();
816 : }
817 16506 : else if (s0 == sort_pos::pos())
818 : {
819 71 : target_sort = sort_int::int_();
820 : }
821 16435 : else if (s0 == sort_nat::nat())
822 : {
823 71 : target_sort = sort_int::int_();
824 : }
825 16364 : else if (s0 == sort_int::int_())
826 : {
827 16364 : target_sort = sort_int::int_();
828 : }
829 : else
830 : {
831 0 : throw mcrl2::runtime_error("Cannot compute target sort for negate with domain sorts " + pp(s0) + ". ");
832 : }
833 :
834 42899 : function_symbol negate(negate_name(), make_function_sort_(s0, target_sort));
835 85798 : return negate;
836 42899 : }
837 :
838 : /// \brief Recogniser for function -.
839 : /// \param e A data expression.
840 : /// \return true iff e is the function symbol matching -.
841 : inline
842 21475 : bool is_negate_function_symbol(const atermpp::aterm_appl& e)
843 : {
844 21475 : if (is_function_symbol(e))
845 : {
846 20633 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
847 20633 : return f.name() == negate_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == negate(real_()) || f == negate(sort_pos::pos()) || f == negate(sort_nat::nat()) || f == negate(sort_int::int_()));
848 : }
849 842 : return false;
850 : }
851 :
852 : /// \brief Application of function symbol -.
853 :
854 : /// \param arg0 A data expression.
855 : /// \return Application of - to a number of arguments.
856 : inline
857 32587 : application negate(const data_expression& arg0)
858 : {
859 65174 : return sort_real::negate(arg0.sort())(arg0);
860 : }
861 :
862 : /// \brief Make an application of function symbol -.
863 : /// \param result The data expression where the - expression is put.
864 :
865 : /// \param arg0 A data expression.
866 : inline
867 : void make_negate(data_expression& result, const data_expression& arg0)
868 : {
869 : make_application(result, sort_real::negate(arg0.sort()),arg0);
870 : }
871 :
872 : /// \brief Recogniser for application of -.
873 : /// \param e A data expression.
874 : /// \return true iff e is an application of function symbol negate to a
875 : /// number of arguments.
876 : inline
877 21526 : bool is_negate_application(const atermpp::aterm_appl& e)
878 : {
879 21526 : return is_application(e) && is_negate_function_symbol(atermpp::down_cast<application>(e).head());
880 : }
881 :
882 : /// \brief Generate identifier succ.
883 : /// \return Identifier succ.
884 : inline
885 15726 : const core::identifier_string& succ_name()
886 : {
887 15726 : static core::identifier_string succ_name = core::identifier_string("succ");
888 15726 : return succ_name;
889 : }
890 :
891 : // This function is not intended for public use and therefore not documented in Doxygen.
892 : inline
893 15726 : function_symbol succ(const sort_expression& s0)
894 : {
895 15726 : sort_expression target_sort;
896 15726 : if (s0 == real_())
897 : {
898 15513 : target_sort = real_();
899 : }
900 213 : else if (s0 == sort_int::int_())
901 : {
902 71 : target_sort = sort_int::int_();
903 : }
904 142 : else if (s0 == sort_nat::nat())
905 : {
906 71 : target_sort = sort_pos::pos();
907 : }
908 71 : else if (s0 == sort_pos::pos())
909 : {
910 71 : target_sort = sort_pos::pos();
911 : }
912 : else
913 : {
914 0 : throw mcrl2::runtime_error("Cannot compute target sort for succ with domain sorts " + pp(s0) + ". ");
915 : }
916 :
917 15726 : function_symbol succ(succ_name(), make_function_sort_(s0, target_sort));
918 31452 : return succ;
919 15726 : }
920 :
921 : /// \brief Recogniser for function succ.
922 : /// \param e A data expression.
923 : /// \return true iff e is the function symbol matching succ.
924 : inline
925 0 : bool is_succ_function_symbol(const atermpp::aterm_appl& e)
926 : {
927 0 : if (is_function_symbol(e))
928 : {
929 0 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
930 0 : return f.name() == succ_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == succ(real_()) || f == succ(sort_int::int_()) || f == succ(sort_nat::nat()) || f == succ(sort_pos::pos()));
931 : }
932 0 : return false;
933 : }
934 :
935 : /// \brief Application of function symbol succ.
936 :
937 : /// \param arg0 A data expression.
938 : /// \return Application of succ to a number of arguments.
939 : inline
940 5433 : application succ(const data_expression& arg0)
941 : {
942 10866 : return sort_real::succ(arg0.sort())(arg0);
943 : }
944 :
945 : /// \brief Make an application of function symbol succ.
946 : /// \param result The data expression where the succ expression is put.
947 :
948 : /// \param arg0 A data expression.
949 : inline
950 : void make_succ(data_expression& result, const data_expression& arg0)
951 : {
952 : make_application(result, sort_real::succ(arg0.sort()),arg0);
953 : }
954 :
955 : /// \brief Recogniser for application of succ.
956 : /// \param e A data expression.
957 : /// \return true iff e is an application of function symbol succ to a
958 : /// number of arguments.
959 : inline
960 0 : bool is_succ_application(const atermpp::aterm_appl& e)
961 : {
962 0 : return is_application(e) && is_succ_function_symbol(atermpp::down_cast<application>(e).head());
963 : }
964 :
965 : /// \brief Generate identifier pred.
966 : /// \return Identifier pred.
967 : inline
968 15726 : const core::identifier_string& pred_name()
969 : {
970 15726 : static core::identifier_string pred_name = core::identifier_string("pred");
971 15726 : return pred_name;
972 : }
973 :
974 : // This function is not intended for public use and therefore not documented in Doxygen.
975 : inline
976 15726 : function_symbol pred(const sort_expression& s0)
977 : {
978 15726 : sort_expression target_sort;
979 15726 : if (s0 == real_())
980 : {
981 15513 : target_sort = real_();
982 : }
983 213 : else if (s0 == sort_nat::nat())
984 : {
985 71 : target_sort = sort_int::int_();
986 : }
987 142 : else if (s0 == sort_int::int_())
988 : {
989 71 : target_sort = sort_int::int_();
990 : }
991 71 : else if (s0 == sort_pos::pos())
992 : {
993 71 : target_sort = sort_nat::nat();
994 : }
995 : else
996 : {
997 0 : throw mcrl2::runtime_error("Cannot compute target sort for pred with domain sorts " + pp(s0) + ". ");
998 : }
999 :
1000 15726 : function_symbol pred(pred_name(), make_function_sort_(s0, target_sort));
1001 31452 : return pred;
1002 15726 : }
1003 :
1004 : /// \brief Recogniser for function pred.
1005 : /// \param e A data expression.
1006 : /// \return true iff e is the function symbol matching pred.
1007 : inline
1008 0 : bool is_pred_function_symbol(const atermpp::aterm_appl& e)
1009 : {
1010 0 : if (is_function_symbol(e))
1011 : {
1012 0 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1013 0 : return f.name() == pred_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == pred(real_()) || f == pred(sort_nat::nat()) || f == pred(sort_int::int_()) || f == pred(sort_pos::pos()));
1014 : }
1015 0 : return false;
1016 : }
1017 :
1018 : /// \brief Application of function symbol pred.
1019 :
1020 : /// \param arg0 A data expression.
1021 : /// \return Application of pred to a number of arguments.
1022 : inline
1023 5433 : application pred(const data_expression& arg0)
1024 : {
1025 10866 : return sort_real::pred(arg0.sort())(arg0);
1026 : }
1027 :
1028 : /// \brief Make an application of function symbol pred.
1029 : /// \param result The data expression where the pred expression is put.
1030 :
1031 : /// \param arg0 A data expression.
1032 : inline
1033 : void make_pred(data_expression& result, const data_expression& arg0)
1034 : {
1035 : make_application(result, sort_real::pred(arg0.sort()),arg0);
1036 : }
1037 :
1038 : /// \brief Recogniser for application of pred.
1039 : /// \param e A data expression.
1040 : /// \return true iff e is an application of function symbol pred to a
1041 : /// number of arguments.
1042 : inline
1043 0 : bool is_pred_application(const atermpp::aterm_appl& e)
1044 : {
1045 0 : return is_application(e) && is_pred_function_symbol(atermpp::down_cast<application>(e).head());
1046 : }
1047 :
1048 : /// \brief Generate identifier +.
1049 : /// \return Identifier +.
1050 : inline
1051 78554 : const core::identifier_string& plus_name()
1052 : {
1053 78554 : static core::identifier_string plus_name = core::identifier_string("+");
1054 78554 : return plus_name;
1055 : }
1056 :
1057 : // This function is not intended for public use and therefore not documented in Doxygen.
1058 : inline
1059 39247 : function_symbol plus(const sort_expression& s0, const sort_expression& s1)
1060 : {
1061 39247 : sort_expression target_sort;
1062 39247 : if (s0 == real_() && s1 == real_())
1063 : {
1064 21880 : target_sort = real_();
1065 : }
1066 17367 : else if (s0 == sort_int::int_() && s1 == sort_int::int_())
1067 : {
1068 16456 : target_sort = sort_int::int_();
1069 : }
1070 911 : else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
1071 : {
1072 383 : target_sort = sort_pos::pos();
1073 : }
1074 528 : else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
1075 : {
1076 163 : target_sort = sort_pos::pos();
1077 : }
1078 365 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1079 : {
1080 163 : target_sort = sort_nat::nat();
1081 : }
1082 202 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
1083 : {
1084 202 : target_sort = sort_pos::pos();
1085 : }
1086 : else
1087 : {
1088 0 : throw mcrl2::runtime_error("Cannot compute target sort for plus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1089 : }
1090 :
1091 39247 : function_symbol plus(plus_name(), make_function_sort_(s0, s1, target_sort));
1092 78494 : return plus;
1093 39247 : }
1094 :
1095 : /// \brief Recogniser for function +.
1096 : /// \param e A data expression.
1097 : /// \return true iff e is the function symbol matching +.
1098 : inline
1099 40056 : bool is_plus_function_symbol(const atermpp::aterm_appl& e)
1100 : {
1101 40056 : if (is_function_symbol(e))
1102 : {
1103 38822 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1104 38822 : return f.name() == plus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == plus(real_(), real_()) || f == plus(sort_int::int_(), sort_int::int_()) || f == plus(sort_pos::pos(), sort_nat::nat()) || f == plus(sort_nat::nat(), sort_pos::pos()) || f == plus(sort_nat::nat(), sort_nat::nat()) || f == plus(sort_pos::pos(), sort_pos::pos()));
1105 : }
1106 1234 : return false;
1107 : }
1108 :
1109 : /// \brief Application of function symbol +.
1110 :
1111 : /// \param arg0 A data expression.
1112 : /// \param arg1 A data expression.
1113 : /// \return Application of + to a number of arguments.
1114 : inline
1115 28202 : application plus(const data_expression& arg0, const data_expression& arg1)
1116 : {
1117 56404 : return sort_real::plus(arg0.sort(), arg1.sort())(arg0, arg1);
1118 : }
1119 :
1120 : /// \brief Make an application of function symbol +.
1121 : /// \param result The data expression where the + expression is put.
1122 :
1123 : /// \param arg0 A data expression.
1124 : /// \param arg1 A data expression.
1125 : inline
1126 0 : void make_plus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1127 : {
1128 0 : make_application(result, sort_real::plus(arg0.sort(), arg1.sort()),arg0, arg1);
1129 0 : }
1130 :
1131 : /// \brief Recogniser for application of +.
1132 : /// \param e A data expression.
1133 : /// \return true iff e is an application of function symbol plus to a
1134 : /// number of arguments.
1135 : inline
1136 40511 : bool is_plus_application(const atermpp::aterm_appl& e)
1137 : {
1138 40511 : return is_application(e) && is_plus_function_symbol(atermpp::down_cast<application>(e).head());
1139 : }
1140 :
1141 : /// \brief Generate identifier -.
1142 : /// \return Identifier -.
1143 : inline
1144 65875 : const core::identifier_string& minus_name()
1145 : {
1146 65875 : static core::identifier_string minus_name = core::identifier_string("-");
1147 65875 : return minus_name;
1148 : }
1149 :
1150 : // This function is not intended for public use and therefore not documented in Doxygen.
1151 : inline
1152 26862 : function_symbol minus(const sort_expression& s0, const sort_expression& s1)
1153 : {
1154 26862 : sort_expression target_sort;
1155 26862 : if (s0 == real_() && s1 == real_())
1156 : {
1157 15607 : target_sort = real_();
1158 : }
1159 11255 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
1160 : {
1161 131 : target_sort = sort_int::int_();
1162 : }
1163 11124 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1164 : {
1165 131 : target_sort = sort_int::int_();
1166 : }
1167 10993 : else if (s0 == sort_int::int_() && s1 == sort_int::int_())
1168 : {
1169 10993 : target_sort = sort_int::int_();
1170 : }
1171 : else
1172 : {
1173 0 : throw mcrl2::runtime_error("Cannot compute target sort for minus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1174 : }
1175 :
1176 26862 : function_symbol minus(minus_name(), make_function_sort_(s0, s1, target_sort));
1177 53724 : return minus;
1178 26862 : }
1179 :
1180 : /// \brief Recogniser for function -.
1181 : /// \param e A data expression.
1182 : /// \return true iff e is the function symbol matching -.
1183 : inline
1184 39800 : bool is_minus_function_symbol(const atermpp::aterm_appl& e)
1185 : {
1186 39800 : if (is_function_symbol(e))
1187 : {
1188 38566 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1189 38566 : return f.name() == minus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minus(real_(), real_()) || f == minus(sort_pos::pos(), sort_pos::pos()) || f == minus(sort_nat::nat(), sort_nat::nat()) || f == minus(sort_int::int_(), sort_int::int_()));
1190 : }
1191 1234 : return false;
1192 : }
1193 :
1194 : /// \brief Application of function symbol -.
1195 :
1196 : /// \param arg0 A data expression.
1197 : /// \param arg1 A data expression.
1198 : /// \return Application of - to a number of arguments.
1199 : inline
1200 16297 : application minus(const data_expression& arg0, const data_expression& arg1)
1201 : {
1202 32594 : return sort_real::minus(arg0.sort(), arg1.sort())(arg0, arg1);
1203 : }
1204 :
1205 : /// \brief Make an application of function symbol -.
1206 : /// \param result The data expression where the - expression is put.
1207 :
1208 : /// \param arg0 A data expression.
1209 : /// \param arg1 A data expression.
1210 : inline
1211 : void make_minus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1212 : {
1213 : make_application(result, sort_real::minus(arg0.sort(), arg1.sort()),arg0, arg1);
1214 : }
1215 :
1216 : /// \brief Recogniser for application of -.
1217 : /// \param e A data expression.
1218 : /// \return true iff e is an application of function symbol minus to a
1219 : /// number of arguments.
1220 : inline
1221 40255 : bool is_minus_application(const atermpp::aterm_appl& e)
1222 : {
1223 40255 : return is_application(e) && is_minus_function_symbol(atermpp::down_cast<application>(e).head());
1224 : }
1225 :
1226 : /// \brief Generate identifier *.
1227 : /// \return Identifier *.
1228 : inline
1229 140434 : const core::identifier_string& times_name()
1230 : {
1231 140434 : static core::identifier_string times_name = core::identifier_string("*");
1232 140434 : return times_name;
1233 : }
1234 :
1235 : // This function is not intended for public use and therefore not documented in Doxygen.
1236 : inline
1237 119824 : function_symbol times(const sort_expression& s0, const sort_expression& s1)
1238 : {
1239 119824 : sort_expression target_sort;
1240 119824 : if (s0 == real_() && s1 == real_())
1241 : {
1242 26807 : target_sort = real_();
1243 : }
1244 93017 : else if (s0 == sort_int::int_() && s1 == sort_int::int_())
1245 : {
1246 76157 : target_sort = sort_int::int_();
1247 : }
1248 16860 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1249 : {
1250 126 : target_sort = sort_nat::nat();
1251 : }
1252 16734 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
1253 : {
1254 16734 : target_sort = sort_pos::pos();
1255 : }
1256 : else
1257 : {
1258 0 : throw mcrl2::runtime_error("Cannot compute target sort for times with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1259 : }
1260 :
1261 119824 : function_symbol times(times_name(), make_function_sort_(s0, s1, target_sort));
1262 239648 : return times;
1263 119824 : }
1264 :
1265 : /// \brief Recogniser for function *.
1266 : /// \param e A data expression.
1267 : /// \return true iff e is the function symbol matching *.
1268 : inline
1269 21452 : bool is_times_function_symbol(const atermpp::aterm_appl& e)
1270 : {
1271 21452 : if (is_function_symbol(e))
1272 : {
1273 20610 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1274 20610 : return f.name() == times_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == times(real_(), real_()) || f == times(sort_int::int_(), sort_int::int_()) || f == times(sort_nat::nat(), sort_nat::nat()) || f == times(sort_pos::pos(), sort_pos::pos()));
1275 : }
1276 842 : return false;
1277 : }
1278 :
1279 : /// \brief Application of function symbol *.
1280 :
1281 : /// \param arg0 A data expression.
1282 : /// \param arg1 A data expression.
1283 : /// \return Application of * to a number of arguments.
1284 : inline
1285 109305 : application times(const data_expression& arg0, const data_expression& arg1)
1286 : {
1287 218610 : return sort_real::times(arg0.sort(), arg1.sort())(arg0, arg1);
1288 : }
1289 :
1290 : /// \brief Make an application of function symbol *.
1291 : /// \param result The data expression where the * expression is put.
1292 :
1293 : /// \param arg0 A data expression.
1294 : /// \param arg1 A data expression.
1295 : inline
1296 0 : void make_times(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1297 : {
1298 0 : make_application(result, sort_real::times(arg0.sort(), arg1.sort()),arg0, arg1);
1299 0 : }
1300 :
1301 : /// \brief Recogniser for application of *.
1302 : /// \param e A data expression.
1303 : /// \return true iff e is an application of function symbol times to a
1304 : /// number of arguments.
1305 : inline
1306 21503 : bool is_times_application(const atermpp::aterm_appl& e)
1307 : {
1308 21503 : return is_application(e) && is_times_function_symbol(atermpp::down_cast<application>(e).head());
1309 : }
1310 :
1311 : /// \brief Generate identifier exp.
1312 : /// \return Identifier exp.
1313 : inline
1314 42906 : const core::identifier_string& exp_name()
1315 : {
1316 42906 : static core::identifier_string exp_name = core::identifier_string("exp");
1317 42906 : return exp_name;
1318 : }
1319 :
1320 : // This function is not intended for public use and therefore not documented in Doxygen.
1321 : inline
1322 42880 : function_symbol exp(const sort_expression& s0, const sort_expression& s1)
1323 : {
1324 42880 : sort_expression target_sort;
1325 42880 : if (s0 == real_() && s1 == sort_int::int_())
1326 : {
1327 20943 : target_sort = real_();
1328 : }
1329 21937 : else if (s0 == sort_int::int_() && s1 == sort_nat::nat())
1330 : {
1331 10933 : target_sort = sort_int::int_();
1332 : }
1333 11004 : else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
1334 : {
1335 10933 : target_sort = sort_pos::pos();
1336 : }
1337 71 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1338 : {
1339 71 : target_sort = sort_nat::nat();
1340 : }
1341 : else
1342 : {
1343 0 : throw mcrl2::runtime_error("Cannot compute target sort for exp with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1344 : }
1345 :
1346 42880 : function_symbol exp(exp_name(), make_function_sort_(s0, s1, target_sort));
1347 85760 : return exp;
1348 42880 : }
1349 :
1350 : /// \brief Recogniser for function exp.
1351 : /// \param e A data expression.
1352 : /// \return true iff e is the function symbol matching exp.
1353 : inline
1354 26 : bool is_exp_function_symbol(const atermpp::aterm_appl& e)
1355 : {
1356 26 : if (is_function_symbol(e))
1357 : {
1358 26 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1359 26 : return f.name() == exp_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == exp(real_(), sort_int::int_()) || f == exp(sort_int::int_(), sort_nat::nat()) || f == exp(sort_pos::pos(), sort_nat::nat()) || f == exp(sort_nat::nat(), sort_nat::nat()));
1360 : }
1361 0 : return false;
1362 : }
1363 :
1364 : /// \brief Application of function symbol exp.
1365 :
1366 : /// \param arg0 A data expression.
1367 : /// \param arg1 A data expression.
1368 : /// \return Application of exp to a number of arguments.
1369 : inline
1370 32587 : application exp(const data_expression& arg0, const data_expression& arg1)
1371 : {
1372 65174 : return sort_real::exp(arg0.sort(), arg1.sort())(arg0, arg1);
1373 : }
1374 :
1375 : /// \brief Make an application of function symbol exp.
1376 : /// \param result The data expression where the exp expression is put.
1377 :
1378 : /// \param arg0 A data expression.
1379 : /// \param arg1 A data expression.
1380 : inline
1381 : void make_exp(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1382 : {
1383 : make_application(result, sort_real::exp(arg0.sort(), arg1.sort()),arg0, arg1);
1384 : }
1385 :
1386 : /// \brief Recogniser for application of exp.
1387 : /// \param e A data expression.
1388 : /// \return true iff e is an application of function symbol exp to a
1389 : /// number of arguments.
1390 : inline
1391 26 : bool is_exp_application(const atermpp::aterm_appl& e)
1392 : {
1393 26 : return is_application(e) && is_exp_function_symbol(atermpp::down_cast<application>(e).head());
1394 : }
1395 :
1396 : /// \brief Generate identifier /.
1397 : /// \return Identifier /.
1398 : inline
1399 101273 : const core::identifier_string& divides_name()
1400 : {
1401 101273 : static core::identifier_string divides_name = core::identifier_string("/");
1402 101273 : return divides_name;
1403 : }
1404 :
1405 : // This function is not intended for public use and therefore not documented in Doxygen.
1406 : inline
1407 62583 : function_symbol divides(const sort_expression& s0, const sort_expression& s1)
1408 : {
1409 62583 : sort_expression target_sort(real_());
1410 62583 : function_symbol divides(divides_name(), make_function_sort_(s0, s1, target_sort));
1411 125166 : return divides;
1412 62583 : }
1413 :
1414 : /// \brief Recogniser for function /.
1415 : /// \param e A data expression.
1416 : /// \return true iff e is the function symbol matching /.
1417 : inline
1418 39479 : bool is_divides_function_symbol(const atermpp::aterm_appl& e)
1419 : {
1420 39479 : if (is_function_symbol(e))
1421 : {
1422 38245 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1423 38245 : return f.name() == divides_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == divides(sort_pos::pos(), sort_pos::pos()) || f == divides(sort_nat::nat(), sort_nat::nat()) || f == divides(sort_int::int_(), sort_int::int_()) || f == divides(real_(), real_()));
1424 : }
1425 1234 : return false;
1426 : }
1427 :
1428 : /// \brief Application of function symbol /.
1429 :
1430 : /// \param arg0 A data expression.
1431 : /// \param arg1 A data expression.
1432 : /// \return Application of / to a number of arguments.
1433 : inline
1434 21805 : application divides(const data_expression& arg0, const data_expression& arg1)
1435 : {
1436 43610 : return sort_real::divides(arg0.sort(), arg1.sort())(arg0, arg1);
1437 : }
1438 :
1439 : /// \brief Make an application of function symbol /.
1440 : /// \param result The data expression where the / expression is put.
1441 :
1442 : /// \param arg0 A data expression.
1443 : /// \param arg1 A data expression.
1444 : inline
1445 : void make_divides(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1446 : {
1447 : make_application(result, sort_real::divides(arg0.sort(), arg1.sort()),arg0, arg1);
1448 : }
1449 :
1450 : /// \brief Recogniser for application of /.
1451 : /// \param e A data expression.
1452 : /// \return true iff e is an application of function symbol divides to a
1453 : /// number of arguments.
1454 : inline
1455 39883 : bool is_divides_application(const atermpp::aterm_appl& e)
1456 : {
1457 39883 : return is_application(e) && is_divides_function_symbol(atermpp::down_cast<application>(e).head());
1458 : }
1459 :
1460 : /// \brief Generate identifier floor.
1461 : /// \return Identifier floor.
1462 : inline
1463 112 : const core::identifier_string& floor_name()
1464 : {
1465 112 : static core::identifier_string floor_name = core::identifier_string("floor");
1466 112 : return floor_name;
1467 : }
1468 :
1469 : /// \brief Constructor for function symbol floor.
1470 :
1471 : /// \return Function symbol floor.
1472 : inline
1473 26374 : const function_symbol& floor()
1474 : {
1475 26374 : static function_symbol floor(floor_name(), make_function_sort_(real_(), sort_int::int_()));
1476 26374 : return floor;
1477 : }
1478 :
1479 : /// \brief Recogniser for function floor.
1480 : /// \param e A data expression.
1481 : /// \return true iff e is the function symbol matching floor.
1482 : inline
1483 : bool is_floor_function_symbol(const atermpp::aterm_appl& e)
1484 : {
1485 : if (is_function_symbol(e))
1486 : {
1487 : return atermpp::down_cast<function_symbol>(e) == floor();
1488 : }
1489 : return false;
1490 : }
1491 :
1492 : /// \brief Application of function symbol floor.
1493 :
1494 : /// \param arg0 A data expression.
1495 : /// \return Application of floor to a number of arguments.
1496 : inline
1497 16294 : application floor(const data_expression& arg0)
1498 : {
1499 16294 : return sort_real::floor()(arg0);
1500 : }
1501 :
1502 : /// \brief Make an application of function symbol floor.
1503 : /// \param result The data expression where the floor expression is put.
1504 :
1505 : /// \param arg0 A data expression.
1506 : inline
1507 : void make_floor(data_expression& result, const data_expression& arg0)
1508 : {
1509 : make_application(result, sort_real::floor(),arg0);
1510 : }
1511 :
1512 : /// \brief Recogniser for application of floor.
1513 : /// \param e A data expression.
1514 : /// \return true iff e is an application of function symbol floor to a
1515 : /// number of arguments.
1516 : inline
1517 : bool is_floor_application(const atermpp::aterm_appl& e)
1518 : {
1519 : return is_application(e) && is_floor_function_symbol(atermpp::down_cast<application>(e).head());
1520 : }
1521 :
1522 : /// \brief Generate identifier ceil.
1523 : /// \return Identifier ceil.
1524 : inline
1525 112 : const core::identifier_string& ceil_name()
1526 : {
1527 112 : static core::identifier_string ceil_name = core::identifier_string("ceil");
1528 112 : return ceil_name;
1529 : }
1530 :
1531 : /// \brief Constructor for function symbol ceil.
1532 :
1533 : /// \return Function symbol ceil.
1534 : inline
1535 15512 : const function_symbol& ceil()
1536 : {
1537 15512 : static function_symbol ceil(ceil_name(), make_function_sort_(real_(), sort_int::int_()));
1538 15512 : return ceil;
1539 : }
1540 :
1541 : /// \brief Recogniser for function ceil.
1542 : /// \param e A data expression.
1543 : /// \return true iff e is the function symbol matching ceil.
1544 : inline
1545 : bool is_ceil_function_symbol(const atermpp::aterm_appl& e)
1546 : {
1547 : if (is_function_symbol(e))
1548 : {
1549 : return atermpp::down_cast<function_symbol>(e) == ceil();
1550 : }
1551 : return false;
1552 : }
1553 :
1554 : /// \brief Application of function symbol ceil.
1555 :
1556 : /// \param arg0 A data expression.
1557 : /// \return Application of ceil to a number of arguments.
1558 : inline
1559 5432 : application ceil(const data_expression& arg0)
1560 : {
1561 5432 : return sort_real::ceil()(arg0);
1562 : }
1563 :
1564 : /// \brief Make an application of function symbol ceil.
1565 : /// \param result The data expression where the ceil expression is put.
1566 :
1567 : /// \param arg0 A data expression.
1568 : inline
1569 : void make_ceil(data_expression& result, const data_expression& arg0)
1570 : {
1571 : make_application(result, sort_real::ceil(),arg0);
1572 : }
1573 :
1574 : /// \brief Recogniser for application of ceil.
1575 : /// \param e A data expression.
1576 : /// \return true iff e is an application of function symbol ceil to a
1577 : /// number of arguments.
1578 : inline
1579 : bool is_ceil_application(const atermpp::aterm_appl& e)
1580 : {
1581 : return is_application(e) && is_ceil_function_symbol(atermpp::down_cast<application>(e).head());
1582 : }
1583 :
1584 : /// \brief Generate identifier round.
1585 : /// \return Identifier round.
1586 : inline
1587 112 : const core::identifier_string& round_name()
1588 : {
1589 112 : static core::identifier_string round_name = core::identifier_string("round");
1590 112 : return round_name;
1591 : }
1592 :
1593 : /// \brief Constructor for function symbol round.
1594 :
1595 : /// \return Function symbol round.
1596 : inline
1597 15513 : const function_symbol& round()
1598 : {
1599 15513 : static function_symbol round(round_name(), make_function_sort_(real_(), sort_int::int_()));
1600 15513 : return round;
1601 : }
1602 :
1603 : /// \brief Recogniser for function round.
1604 : /// \param e A data expression.
1605 : /// \return true iff e is the function symbol matching round.
1606 : inline
1607 : bool is_round_function_symbol(const atermpp::aterm_appl& e)
1608 : {
1609 : if (is_function_symbol(e))
1610 : {
1611 : return atermpp::down_cast<function_symbol>(e) == round();
1612 : }
1613 : return false;
1614 : }
1615 :
1616 : /// \brief Application of function symbol round.
1617 :
1618 : /// \param arg0 A data expression.
1619 : /// \return Application of round to a number of arguments.
1620 : inline
1621 5433 : application round(const data_expression& arg0)
1622 : {
1623 5433 : return sort_real::round()(arg0);
1624 : }
1625 :
1626 : /// \brief Make an application of function symbol round.
1627 : /// \param result The data expression where the round expression is put.
1628 :
1629 : /// \param arg0 A data expression.
1630 : inline
1631 : void make_round(data_expression& result, const data_expression& arg0)
1632 : {
1633 : make_application(result, sort_real::round(),arg0);
1634 : }
1635 :
1636 : /// \brief Recogniser for application of round.
1637 : /// \param e A data expression.
1638 : /// \return true iff e is an application of function symbol round to a
1639 : /// number of arguments.
1640 : inline
1641 : bool is_round_application(const atermpp::aterm_appl& e)
1642 : {
1643 : return is_application(e) && is_round_function_symbol(atermpp::down_cast<application>(e).head());
1644 : }
1645 :
1646 : /// \brief Generate identifier \@redfrac.
1647 : /// \return Identifier \@redfrac.
1648 : inline
1649 112 : const core::identifier_string& reduce_fraction_name()
1650 : {
1651 112 : static core::identifier_string reduce_fraction_name = core::identifier_string("@redfrac");
1652 112 : return reduce_fraction_name;
1653 : }
1654 :
1655 : /// \brief Constructor for function symbol \@redfrac.
1656 :
1657 : /// \return Function symbol reduce_fraction.
1658 : inline
1659 101105 : const function_symbol& reduce_fraction()
1660 : {
1661 101105 : static function_symbol reduce_fraction(reduce_fraction_name(), make_function_sort_(sort_int::int_(), sort_int::int_(), real_()));
1662 101105 : return reduce_fraction;
1663 : }
1664 :
1665 : /// \brief Recogniser for function \@redfrac.
1666 : /// \param e A data expression.
1667 : /// \return true iff e is the function symbol matching \@redfrac.
1668 : inline
1669 21335 : bool is_reduce_fraction_function_symbol(const atermpp::aterm_appl& e)
1670 : {
1671 21335 : if (is_function_symbol(e))
1672 : {
1673 20493 : return atermpp::down_cast<function_symbol>(e) == reduce_fraction();
1674 : }
1675 842 : return false;
1676 : }
1677 :
1678 : /// \brief Application of function symbol \@redfrac.
1679 :
1680 : /// \param arg0 A data expression.
1681 : /// \param arg1 A data expression.
1682 : /// \return Application of \@redfrac to a number of arguments.
1683 : inline
1684 70603 : application reduce_fraction(const data_expression& arg0, const data_expression& arg1)
1685 : {
1686 70603 : return sort_real::reduce_fraction()(arg0, arg1);
1687 : }
1688 :
1689 : /// \brief Make an application of function symbol \@redfrac.
1690 : /// \param result The data expression where the \@redfrac expression is put.
1691 :
1692 : /// \param arg0 A data expression.
1693 : /// \param arg1 A data expression.
1694 : inline
1695 : void make_reduce_fraction(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1696 : {
1697 : make_application(result, sort_real::reduce_fraction(),arg0, arg1);
1698 : }
1699 :
1700 : /// \brief Recogniser for application of \@redfrac.
1701 : /// \param e A data expression.
1702 : /// \return true iff e is an application of function symbol reduce_fraction to a
1703 : /// number of arguments.
1704 : inline
1705 21335 : bool is_reduce_fraction_application(const atermpp::aterm_appl& e)
1706 : {
1707 21335 : return is_application(e) && is_reduce_fraction_function_symbol(atermpp::down_cast<application>(e).head());
1708 : }
1709 :
1710 : /// \brief Generate identifier \@redfracwhr.
1711 : /// \return Identifier \@redfracwhr.
1712 : inline
1713 112 : const core::identifier_string& reduce_fraction_where_name()
1714 : {
1715 112 : static core::identifier_string reduce_fraction_where_name = core::identifier_string("@redfracwhr");
1716 112 : return reduce_fraction_where_name;
1717 : }
1718 :
1719 : /// \brief Constructor for function symbol \@redfracwhr.
1720 :
1721 : /// \return Function symbol reduce_fraction_where.
1722 : inline
1723 46783 : const function_symbol& reduce_fraction_where()
1724 : {
1725 46783 : static function_symbol reduce_fraction_where(reduce_fraction_where_name(), make_function_sort_(sort_pos::pos(), sort_int::int_(), sort_nat::nat(), real_()));
1726 46783 : return reduce_fraction_where;
1727 : }
1728 :
1729 : /// \brief Recogniser for function \@redfracwhr.
1730 : /// \param e A data expression.
1731 : /// \return true iff e is the function symbol matching \@redfracwhr.
1732 : inline
1733 21323 : bool is_reduce_fraction_where_function_symbol(const atermpp::aterm_appl& e)
1734 : {
1735 21323 : if (is_function_symbol(e))
1736 : {
1737 20481 : return atermpp::down_cast<function_symbol>(e) == reduce_fraction_where();
1738 : }
1739 842 : return false;
1740 : }
1741 :
1742 : /// \brief Application of function symbol \@redfracwhr.
1743 :
1744 : /// \param arg0 A data expression.
1745 : /// \param arg1 A data expression.
1746 : /// \param arg2 A data expression.
1747 : /// \return Application of \@redfracwhr to a number of arguments.
1748 : inline
1749 16293 : application reduce_fraction_where(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
1750 : {
1751 16293 : return sort_real::reduce_fraction_where()(arg0, arg1, arg2);
1752 : }
1753 :
1754 : /// \brief Make an application of function symbol \@redfracwhr.
1755 : /// \param result The data expression where the \@redfracwhr expression is put.
1756 :
1757 : /// \param arg0 A data expression.
1758 : /// \param arg1 A data expression.
1759 : /// \param arg2 A data expression.
1760 : inline
1761 : void make_reduce_fraction_where(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
1762 : {
1763 : make_application(result, sort_real::reduce_fraction_where(),arg0, arg1, arg2);
1764 : }
1765 :
1766 : /// \brief Recogniser for application of \@redfracwhr.
1767 : /// \param e A data expression.
1768 : /// \return true iff e is an application of function symbol reduce_fraction_where to a
1769 : /// number of arguments.
1770 : inline
1771 21323 : bool is_reduce_fraction_where_application(const atermpp::aterm_appl& e)
1772 : {
1773 21323 : return is_application(e) && is_reduce_fraction_where_function_symbol(atermpp::down_cast<application>(e).head());
1774 : }
1775 :
1776 : /// \brief Generate identifier \@redfrachlp.
1777 : /// \return Identifier \@redfrachlp.
1778 : inline
1779 112 : const core::identifier_string& reduce_fraction_helper_name()
1780 : {
1781 112 : static core::identifier_string reduce_fraction_helper_name = core::identifier_string("@redfrachlp");
1782 112 : return reduce_fraction_helper_name;
1783 : }
1784 :
1785 : /// \brief Constructor for function symbol \@redfrachlp.
1786 :
1787 : /// \return Function symbol reduce_fraction_helper.
1788 : inline
1789 20871 : const function_symbol& reduce_fraction_helper()
1790 : {
1791 20871 : static function_symbol reduce_fraction_helper(reduce_fraction_helper_name(), make_function_sort_(real_(), sort_int::int_(), real_()));
1792 20871 : return reduce_fraction_helper;
1793 : }
1794 :
1795 : /// \brief Recogniser for function \@redfrachlp.
1796 : /// \param e A data expression.
1797 : /// \return true iff e is the function symbol matching \@redfrachlp.
1798 : inline
1799 0 : bool is_reduce_fraction_helper_function_symbol(const atermpp::aterm_appl& e)
1800 : {
1801 0 : if (is_function_symbol(e))
1802 : {
1803 0 : return atermpp::down_cast<function_symbol>(e) == reduce_fraction_helper();
1804 : }
1805 0 : return false;
1806 : }
1807 :
1808 : /// \brief Application of function symbol \@redfrachlp.
1809 :
1810 : /// \param arg0 A data expression.
1811 : /// \param arg1 A data expression.
1812 : /// \return Application of \@redfrachlp to a number of arguments.
1813 : inline
1814 10862 : application reduce_fraction_helper(const data_expression& arg0, const data_expression& arg1)
1815 : {
1816 10862 : return sort_real::reduce_fraction_helper()(arg0, arg1);
1817 : }
1818 :
1819 : /// \brief Make an application of function symbol \@redfrachlp.
1820 : /// \param result The data expression where the \@redfrachlp expression is put.
1821 :
1822 : /// \param arg0 A data expression.
1823 : /// \param arg1 A data expression.
1824 : inline
1825 : void make_reduce_fraction_helper(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1826 : {
1827 : make_application(result, sort_real::reduce_fraction_helper(),arg0, arg1);
1828 : }
1829 :
1830 : /// \brief Recogniser for application of \@redfrachlp.
1831 : /// \param e A data expression.
1832 : /// \return true iff e is an application of function symbol reduce_fraction_helper to a
1833 : /// number of arguments.
1834 : inline
1835 0 : bool is_reduce_fraction_helper_application(const atermpp::aterm_appl& e)
1836 : {
1837 0 : return is_application(e) && is_reduce_fraction_helper_function_symbol(atermpp::down_cast<application>(e).head());
1838 : }
1839 : /// \brief Give all system defined mappings for real_
1840 : /// \return All system defined mappings for real_
1841 : inline
1842 5431 : function_symbol_vector real_generate_functions_code()
1843 : {
1844 5431 : function_symbol_vector result;
1845 5431 : result.push_back(sort_real::creal());
1846 5431 : result.push_back(sort_real::pos2real());
1847 5431 : result.push_back(sort_real::nat2real());
1848 5431 : result.push_back(sort_real::int2real());
1849 5431 : result.push_back(sort_real::real2pos());
1850 5431 : result.push_back(sort_real::real2nat());
1851 5431 : result.push_back(sort_real::real2int());
1852 5431 : result.push_back(sort_real::maximum(real_(), real_()));
1853 5431 : result.push_back(sort_real::minimum(real_(), real_()));
1854 5431 : result.push_back(sort_real::abs(real_()));
1855 5431 : result.push_back(sort_real::negate(real_()));
1856 5431 : result.push_back(sort_real::succ(real_()));
1857 5431 : result.push_back(sort_real::pred(real_()));
1858 5431 : result.push_back(sort_real::plus(real_(), real_()));
1859 5431 : result.push_back(sort_real::minus(real_(), real_()));
1860 5431 : result.push_back(sort_real::times(real_(), real_()));
1861 5431 : result.push_back(sort_real::exp(real_(), sort_int::int_()));
1862 5431 : result.push_back(sort_real::divides(sort_pos::pos(), sort_pos::pos()));
1863 5431 : result.push_back(sort_real::divides(sort_nat::nat(), sort_nat::nat()));
1864 5431 : result.push_back(sort_real::divides(sort_int::int_(), sort_int::int_()));
1865 5431 : result.push_back(sort_real::divides(real_(), real_()));
1866 5431 : result.push_back(sort_real::floor());
1867 5431 : result.push_back(sort_real::ceil());
1868 5431 : result.push_back(sort_real::round());
1869 5431 : result.push_back(sort_real::reduce_fraction());
1870 5431 : result.push_back(sort_real::reduce_fraction_where());
1871 5431 : result.push_back(sort_real::reduce_fraction_helper());
1872 5431 : return result;
1873 0 : }
1874 :
1875 : /// \brief Give all system defined mappings and constructors for real_
1876 : /// \return All system defined mappings for real_
1877 : inline
1878 : function_symbol_vector real_generate_constructors_and_functions_code()
1879 : {
1880 : function_symbol_vector result=real_generate_functions_code();
1881 : for(const function_symbol& f: real_generate_constructors_code())
1882 : {
1883 : result.push_back(f);
1884 : }
1885 : return result;
1886 : }
1887 :
1888 : /// \brief Give all system defined mappings that can be used in mCRL2 specs for real_
1889 : /// \return All system defined mappings for that can be used in mCRL2 specificationis real_
1890 : inline
1891 4578 : function_symbol_vector real_mCRL2_usable_mappings()
1892 : {
1893 4578 : function_symbol_vector result;
1894 4578 : result.push_back(sort_real::creal());
1895 4578 : result.push_back(sort_real::pos2real());
1896 4578 : result.push_back(sort_real::nat2real());
1897 4578 : result.push_back(sort_real::int2real());
1898 4578 : result.push_back(sort_real::real2pos());
1899 4578 : result.push_back(sort_real::real2nat());
1900 4578 : result.push_back(sort_real::real2int());
1901 4578 : result.push_back(sort_real::maximum(real_(), real_()));
1902 4578 : result.push_back(sort_real::minimum(real_(), real_()));
1903 4578 : result.push_back(sort_real::abs(real_()));
1904 4578 : result.push_back(sort_real::negate(real_()));
1905 4578 : result.push_back(sort_real::succ(real_()));
1906 4578 : result.push_back(sort_real::pred(real_()));
1907 4578 : result.push_back(sort_real::plus(real_(), real_()));
1908 4578 : result.push_back(sort_real::minus(real_(), real_()));
1909 4578 : result.push_back(sort_real::times(real_(), real_()));
1910 4578 : result.push_back(sort_real::exp(real_(), sort_int::int_()));
1911 4578 : result.push_back(sort_real::divides(sort_pos::pos(), sort_pos::pos()));
1912 4578 : result.push_back(sort_real::divides(sort_nat::nat(), sort_nat::nat()));
1913 4578 : result.push_back(sort_real::divides(sort_int::int_(), sort_int::int_()));
1914 4578 : result.push_back(sort_real::divides(real_(), real_()));
1915 4578 : result.push_back(sort_real::floor());
1916 4578 : result.push_back(sort_real::ceil());
1917 4578 : result.push_back(sort_real::round());
1918 4578 : result.push_back(sort_real::reduce_fraction());
1919 4578 : result.push_back(sort_real::reduce_fraction_where());
1920 4578 : result.push_back(sort_real::reduce_fraction_helper());
1921 4578 : return result;
1922 0 : }
1923 :
1924 :
1925 : // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
1926 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
1927 : /// \brief Give all system defined mappings that are to be implemented in C++ code for real_
1928 : /// \return A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for real_
1929 : inline
1930 : implementation_map real_cpp_implementable_mappings()
1931 : {
1932 : implementation_map result;
1933 : return result;
1934 : }
1935 : ///\brief Function for projecting out argument.
1936 : /// left from an application.
1937 : /// \param e A data expression.
1938 : /// \pre left is defined for e.
1939 : /// \return The argument of e that corresponds to left.
1940 : inline
1941 139 : const data_expression& left(const data_expression& e)
1942 : {
1943 139 : assert(is_creal_application(e) || is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_minus_application(e) || is_times_application(e) || is_exp_application(e) || is_divides_application(e) || is_reduce_fraction_application(e) || is_reduce_fraction_helper_application(e));
1944 139 : return atermpp::down_cast<application>(e)[0];
1945 : }
1946 :
1947 : ///\brief Function for projecting out argument.
1948 : /// right from an application.
1949 : /// \param e A data expression.
1950 : /// \pre right is defined for e.
1951 : /// \return The argument of e that corresponds to right.
1952 : inline
1953 139 : const data_expression& right(const data_expression& e)
1954 : {
1955 139 : assert(is_creal_application(e) || is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_minus_application(e) || is_times_application(e) || is_exp_application(e) || is_divides_application(e) || is_reduce_fraction_application(e) || is_reduce_fraction_helper_application(e));
1956 139 : return atermpp::down_cast<application>(e)[1];
1957 : }
1958 :
1959 : ///\brief Function for projecting out argument.
1960 : /// arg from an application.
1961 : /// \param e A data expression.
1962 : /// \pre arg is defined for e.
1963 : /// \return The argument of e that corresponds to arg.
1964 : inline
1965 : const data_expression& arg(const data_expression& e)
1966 : {
1967 : assert(is_pos2real_application(e) || is_nat2real_application(e) || is_int2real_application(e) || is_real2pos_application(e) || is_real2nat_application(e) || is_real2int_application(e) || is_abs_application(e) || is_negate_application(e) || is_succ_application(e) || is_pred_application(e) || is_floor_application(e) || is_ceil_application(e) || is_round_application(e));
1968 : return atermpp::down_cast<application>(e)[0];
1969 : }
1970 :
1971 : ///\brief Function for projecting out argument.
1972 : /// arg1 from an application.
1973 : /// \param e A data expression.
1974 : /// \pre arg1 is defined for e.
1975 : /// \return The argument of e that corresponds to arg1.
1976 : inline
1977 9 : const data_expression& arg1(const data_expression& e)
1978 : {
1979 9 : assert(is_reduce_fraction_where_application(e));
1980 9 : return atermpp::down_cast<application>(e)[0];
1981 : }
1982 :
1983 : ///\brief Function for projecting out argument.
1984 : /// arg2 from an application.
1985 : /// \param e A data expression.
1986 : /// \pre arg2 is defined for e.
1987 : /// \return The argument of e that corresponds to arg2.
1988 : inline
1989 9 : const data_expression& arg2(const data_expression& e)
1990 : {
1991 9 : assert(is_reduce_fraction_where_application(e));
1992 9 : return atermpp::down_cast<application>(e)[1];
1993 : }
1994 :
1995 : ///\brief Function for projecting out argument.
1996 : /// arg3 from an application.
1997 : /// \param e A data expression.
1998 : /// \pre arg3 is defined for e.
1999 : /// \return The argument of e that corresponds to arg3.
2000 : inline
2001 9 : const data_expression& arg3(const data_expression& e)
2002 : {
2003 9 : assert(is_reduce_fraction_where_application(e));
2004 9 : return atermpp::down_cast<application>(e)[2];
2005 : }
2006 :
2007 : /// \brief Give all system defined equations for real_
2008 : /// \return All system defined equations for sort real_
2009 : inline
2010 5431 : data_equation_vector real_generate_equations_code()
2011 : {
2012 10862 : variable vm("m",sort_nat::nat());
2013 10862 : variable vn("n",sort_nat::nat());
2014 10862 : variable vp("p",sort_pos::pos());
2015 10862 : variable vq("q",sort_pos::pos());
2016 10862 : variable vx("x",sort_int::int_());
2017 10862 : variable vy("y",sort_int::int_());
2018 10862 : variable vr("r",real_());
2019 10862 : variable vs("s",real_());
2020 :
2021 5431 : data_equation_vector result;
2022 27155 : result.push_back(data_equation(variable_list({vp, vq, vx, vy}), equal_to(creal(vx, vp), creal(vy, vq)), equal_to(times(vx, sort_int::cint(sort_nat::cnat(vq))), times(vy, sort_int::cint(sort_nat::cnat(vp))))));
2023 27155 : result.push_back(data_equation(variable_list({vp, vq, vx, vy}), less(creal(vx, vp), creal(vy, vq)), less(times(vx, sort_int::cint(sort_nat::cnat(vq))), times(vy, sort_int::cint(sort_nat::cnat(vp))))));
2024 27155 : result.push_back(data_equation(variable_list({vp, vq, vx, vy}), less_equal(creal(vx, vp), creal(vy, vq)), less_equal(times(vx, sort_int::cint(sort_nat::cnat(vq))), times(vy, sort_int::cint(sort_nat::cnat(vp))))));
2025 10862 : result.push_back(data_equation(variable_list({vx}), int2real(vx), creal(vx, sort_pos::c1())));
2026 10862 : result.push_back(data_equation(variable_list({vn}), nat2real(vn), creal(sort_int::cint(vn), sort_pos::c1())));
2027 10862 : result.push_back(data_equation(variable_list({vp}), pos2real(vp), creal(sort_int::cint(sort_nat::cnat(vp)), sort_pos::c1())));
2028 10862 : result.push_back(data_equation(variable_list({vx}), real2int(creal(vx, sort_pos::c1())), vx));
2029 10862 : result.push_back(data_equation(variable_list({vx}), real2nat(creal(vx, sort_pos::c1())), sort_int::int2nat(vx)));
2030 10862 : result.push_back(data_equation(variable_list({vx}), real2pos(creal(vx, sort_pos::c1())), sort_int::int2pos(vx)));
2031 16293 : result.push_back(data_equation(variable_list({vr, vs}), minimum(vr, vs), if_(less(vr, vs), vr, vs)));
2032 16293 : result.push_back(data_equation(variable_list({vr, vs}), maximum(vr, vs), if_(less(vr, vs), vs, vr)));
2033 10862 : result.push_back(data_equation(variable_list({vr}), abs(vr), if_(less(vr, creal(sort_int::cint(sort_nat::c0()), sort_pos::c1())), negate(vr), vr)));
2034 16293 : result.push_back(data_equation(variable_list({vp, vx}), negate(creal(vx, vp)), creal(negate(vx), vp)));
2035 16293 : result.push_back(data_equation(variable_list({vp, vx}), succ(creal(vx, vp)), creal(plus(vx, sort_int::cint(sort_nat::cnat(vp))), vp)));
2036 16293 : result.push_back(data_equation(variable_list({vp, vx}), pred(creal(vx, vp)), creal(minus(vx, sort_int::cint(sort_nat::cnat(vp))), vp)));
2037 27155 : result.push_back(data_equation(variable_list({vp, vq, vx, vy}), plus(creal(vx, vp), creal(vy, vq)), reduce_fraction(plus(times(vx, sort_int::cint(sort_nat::cnat(vq))), times(vy, sort_int::cint(sort_nat::cnat(vp)))), sort_int::cint(sort_nat::cnat(times(vp, vq))))));
2038 27155 : result.push_back(data_equation(variable_list({vp, vq, vx, vy}), minus(creal(vx, vp), creal(vy, vq)), reduce_fraction(minus(times(vx, sort_int::cint(sort_nat::cnat(vq))), times(vy, sort_int::cint(sort_nat::cnat(vp)))), sort_int::cint(sort_nat::cnat(times(vp, vq))))));
2039 27155 : result.push_back(data_equation(variable_list({vp, vq, vx, vy}), times(creal(vx, vp), creal(vy, vq)), reduce_fraction(times(vx, vy), sort_int::cint(sort_nat::cnat(times(vp, vq))))));
2040 16293 : result.push_back(data_equation(variable_list({vp, vr}), times(vr, creal(sort_int::cint(sort_nat::c0()), vp)), creal(sort_int::cint(sort_nat::c0()), sort_pos::c1())));
2041 16293 : result.push_back(data_equation(variable_list({vp, vr}), times(creal(sort_int::cint(sort_nat::c0()), vp), vr), creal(sort_int::cint(sort_nat::c0()), sort_pos::c1())));
2042 27155 : result.push_back(data_equation(variable_list({vp, vq, vx, vy}), not_equal_to(vy, sort_int::cint(sort_nat::c0())), divides(creal(vx, vp), creal(vy, vq)), reduce_fraction(times(vx, sort_int::cint(sort_nat::cnat(vq))), times(vy, sort_int::cint(sort_nat::cnat(vp))))));
2043 16293 : result.push_back(data_equation(variable_list({vp, vq}), divides(vp, vq), reduce_fraction(sort_int::cint(sort_nat::cnat(vp)), sort_int::cint(sort_nat::cnat(vq)))));
2044 16293 : result.push_back(data_equation(variable_list({vm, vn}), not_equal_to(vn, sort_nat::c0()), divides(vm, vn), reduce_fraction(sort_int::cint(vm), sort_int::cint(vn))));
2045 16293 : result.push_back(data_equation(variable_list({vx, vy}), not_equal_to(vy, sort_int::cint(sort_nat::c0())), divides(vx, vy), reduce_fraction(vx, vy)));
2046 21724 : result.push_back(data_equation(variable_list({vn, vp, vx}), exp(creal(vx, vp), sort_int::cint(vn)), reduce_fraction(exp(vx, vn), sort_int::cint(sort_nat::cnat(exp(vp, vn))))));
2047 21724 : result.push_back(data_equation(variable_list({vp, vq, vx}), not_equal_to(vx, sort_int::cint(sort_nat::c0())), exp(creal(vx, vp), sort_int::cneg(vq)), reduce_fraction(sort_int::cint(sort_nat::cnat(exp(vp, sort_nat::cnat(vq)))), exp(vx, sort_nat::cnat(vq)))));
2048 16293 : result.push_back(data_equation(variable_list({vp, vx}), floor(creal(vx, vp)), sort_int::div(vx, vp)));
2049 10862 : result.push_back(data_equation(variable_list({vr}), ceil(vr), negate(floor(negate(vr)))));
2050 10862 : result.push_back(data_equation(variable_list({vr}), round(vr), floor(plus(vr, creal(sort_int::cint(sort_nat::cnat(sort_pos::c1())), sort_pos::cdub(sort_bool::false_(), sort_pos::c1()))))));
2051 16293 : result.push_back(data_equation(variable_list({vp, vx}), reduce_fraction(vx, sort_int::cneg(vp)), reduce_fraction(negate(vx), sort_int::cint(sort_nat::cnat(vp)))));
2052 16293 : result.push_back(data_equation(variable_list({vp, vx}), reduce_fraction(vx, sort_int::cint(sort_nat::cnat(vp))), reduce_fraction_where(vp, sort_int::div(vx, vp), sort_int::mod(vx, vp))));
2053 16293 : result.push_back(data_equation(variable_list({vp, vx}), reduce_fraction_where(vp, vx, sort_nat::c0()), creal(vx, sort_pos::c1())));
2054 21724 : result.push_back(data_equation(variable_list({vp, vq, vx}), reduce_fraction_where(vp, vx, sort_nat::cnat(vq)), reduce_fraction_helper(reduce_fraction(sort_int::cint(sort_nat::cnat(vp)), sort_int::cint(sort_nat::cnat(vq))), vx)));
2055 21724 : result.push_back(data_equation(variable_list({vp, vx, vy}), reduce_fraction_helper(creal(vx, vp), vy), creal(plus(sort_int::cint(sort_nat::cnat(vp)), times(vy, vx)), sort_int::int2pos(vx))));
2056 10862 : return result;
2057 5431 : }
2058 :
2059 : } // namespace sort_real_
2060 :
2061 : } // namespace data
2062 :
2063 : } // namespace mcrl2
2064 :
2065 : #endif // MCRL2_DATA_REAL_H
|
