mCRL2
Loading...
Searching...
No Matches
real64.h
Go to the documentation of this file.
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//
14
15#ifndef MCRL2_DATA_REAL64_H
16#define MCRL2_DATA_REAL64_H
17
18#include "functional" // std::function
25#include "mcrl2/data/standard.h"
26#include "mcrl2/data/bool.h"
27#include "mcrl2/data/pos64.h"
28#include "mcrl2/data/nat64.h"
29#include "mcrl2/data/int64.h"
30
31namespace mcrl2 {
32
33 namespace data {
34
36 namespace sort_real {
37
38 inline
40 {
42 return real_name;
43 }
44
47 inline
48 const basic_sort& real_()
49 {
50 static basic_sort real_ = basic_sort(real_name());
51 return real_;
52 }
53
57 inline
58 bool is_real(const sort_expression& e)
59 {
60 if (is_basic_sort(e))
61 {
62 return basic_sort(e) == real_();
63 }
64 return false;
65 }
66
69 inline
71 {
73 return result;
74 }
77 inline
79 {
81 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<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
87 inline
89 {
90 implementation_map result;
91 return result;
92 }
93
96 inline
98 {
100 return creal_name;
101 }
102
104
106 inline
107 const function_symbol& creal()
108 {
110 return creal;
111 }
112
116 inline
118 {
119 if (is_function_symbol(e))
120 {
121 return atermpp::down_cast<function_symbol>(e) == creal();
122 }
123 return false;
124 }
125
127
131 inline
132 application creal(const data_expression& arg0, const data_expression& arg1)
133 {
134 return sort_real::creal()(arg0, arg1);
135 }
136
139
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
152 inline
154 {
155 return is_application(e) && is_creal_function_symbol(atermpp::down_cast<application>(e).head());
156 }
157
160 inline
162 {
164 return pos2real_name;
165 }
166
168
170 inline
172 {
174 return pos2real;
175 }
176
180 inline
182 {
183 if (is_function_symbol(e))
184 {
185 return atermpp::down_cast<function_symbol>(e) == pos2real();
186 }
187 return false;
188 }
189
191
194 inline
195 application pos2real(const data_expression& arg0)
196 {
197 return sort_real::pos2real()(arg0);
198 }
199
202
204 inline
205 void make_pos2real(data_expression& result, const data_expression& arg0)
206 {
208 }
209
214 inline
216 {
217 return is_application(e) && is_pos2real_function_symbol(atermpp::down_cast<application>(e).head());
218 }
219
222 inline
224 {
226 return nat2real_name;
227 }
228
230
232 inline
234 {
236 return nat2real;
237 }
238
242 inline
244 {
245 if (is_function_symbol(e))
246 {
247 return atermpp::down_cast<function_symbol>(e) == nat2real();
248 }
249 return false;
250 }
251
253
256 inline
257 application nat2real(const data_expression& arg0)
258 {
259 return sort_real::nat2real()(arg0);
260 }
261
264
266 inline
267 void make_nat2real(data_expression& result, const data_expression& arg0)
268 {
270 }
271
276 inline
278 {
279 return is_application(e) && is_nat2real_function_symbol(atermpp::down_cast<application>(e).head());
280 }
281
284 inline
286 {
288 return int2real_name;
289 }
290
292
294 inline
296 {
298 return int2real;
299 }
300
304 inline
306 {
307 if (is_function_symbol(e))
308 {
309 return atermpp::down_cast<function_symbol>(e) == int2real();
310 }
311 return false;
312 }
313
315
318 inline
319 application int2real(const data_expression& arg0)
320 {
321 return sort_real::int2real()(arg0);
322 }
323
326
328 inline
329 void make_int2real(data_expression& result, const data_expression& arg0)
330 {
332 }
333
338 inline
340 {
341 return is_application(e) && is_int2real_function_symbol(atermpp::down_cast<application>(e).head());
342 }
343
346 inline
348 {
350 return real2pos_name;
351 }
352
354
356 inline
358 {
360 return real2pos;
361 }
362
366 inline
368 {
369 if (is_function_symbol(e))
370 {
371 return atermpp::down_cast<function_symbol>(e) == real2pos();
372 }
373 return false;
374 }
375
377
380 inline
381 application real2pos(const data_expression& arg0)
382 {
383 return sort_real::real2pos()(arg0);
384 }
385
388
390 inline
391 void make_real2pos(data_expression& result, const data_expression& arg0)
392 {
394 }
395
400 inline
402 {
403 return is_application(e) && is_real2pos_function_symbol(atermpp::down_cast<application>(e).head());
404 }
405
408 inline
410 {
412 return real2nat_name;
413 }
414
416
418 inline
420 {
422 return real2nat;
423 }
424
428 inline
430 {
431 if (is_function_symbol(e))
432 {
433 return atermpp::down_cast<function_symbol>(e) == real2nat();
434 }
435 return false;
436 }
437
439
442 inline
443 application real2nat(const data_expression& arg0)
444 {
445 return sort_real::real2nat()(arg0);
446 }
447
450
452 inline
453 void make_real2nat(data_expression& result, const data_expression& arg0)
454 {
456 }
457
462 inline
464 {
465 return is_application(e) && is_real2nat_function_symbol(atermpp::down_cast<application>(e).head());
466 }
467
470 inline
472 {
474 return real2int_name;
475 }
476
478
480 inline
482 {
484 return real2int;
485 }
486
490 inline
492 {
493 if (is_function_symbol(e))
494 {
495 return atermpp::down_cast<function_symbol>(e) == real2int();
496 }
497 return false;
498 }
499
501
504 inline
505 application real2int(const data_expression& arg0)
506 {
507 return sort_real::real2int()(arg0);
508 }
509
512
514 inline
515 void make_real2int(data_expression& result, const data_expression& arg0)
516 {
518 }
519
524 inline
526 {
527 return is_application(e) && is_real2int_function_symbol(atermpp::down_cast<application>(e).head());
528 }
529
532 inline
534 {
536 return maximum_name;
537 }
538
539 // This function is not intended for public use and therefore not documented in Doxygen.
540 inline
541 function_symbol maximum(const sort_expression& s0, const sort_expression& s1)
542 {
543 sort_expression target_sort;
544 if (s0 == real_() && s1 == real_())
545 {
546 target_sort = real_();
547 }
548 else if (s0 == sort_pos::pos() && s1 == sort_int::int_())
549 {
551 }
552 else if (s0 == sort_int::int_() && s1 == sort_pos::pos())
553 {
555 }
556 else if (s0 == sort_nat::nat() && s1 == sort_int::int_())
557 {
559 }
560 else if (s0 == sort_int::int_() && s1 == sort_nat::nat())
561 {
563 }
564 else if (s0 == sort_int::int_() && s1 == sort_int::int_())
565 {
567 }
568 else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
569 {
571 }
572 else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
573 {
575 }
576 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
577 {
579 }
580 else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
581 {
583 }
584 else
585 {
586 throw mcrl2::runtime_error("Cannot compute target sort for maximum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
587 }
588
590 return maximum;
591 }
592
596 inline
598 {
599 if (is_function_symbol(e))
600 {
601 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
602 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 return false;
605 }
606
608
612 inline
613 application maximum(const data_expression& arg0, const data_expression& arg1)
614 {
615 return sort_real::maximum(arg0.sort(), arg1.sort())(arg0, arg1);
616 }
617
620
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
633 inline
635 {
636 return is_application(e) && is_maximum_function_symbol(atermpp::down_cast<application>(e).head());
637 }
638
641 inline
643 {
645 return minimum_name;
646 }
647
648 // This function is not intended for public use and therefore not documented in Doxygen.
649 inline
650 function_symbol minimum(const sort_expression& s0, const sort_expression& s1)
651 {
652 sort_expression target_sort;
653 if (s0 == real_() && s1 == real_())
654 {
655 target_sort = real_();
656 }
657 else if (s0 == sort_int::int_() && s1 == sort_int::int_())
658 {
660 }
661 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
662 {
664 }
665 else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
666 {
668 }
669 else
670 {
671 throw mcrl2::runtime_error("Cannot compute target sort for minimum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
672 }
673
675 return minimum;
676 }
677
681 inline
683 {
684 if (is_function_symbol(e))
685 {
686 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
687 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 return false;
690 }
691
693
697 inline
698 application minimum(const data_expression& arg0, const data_expression& arg1)
699 {
700 return sort_real::minimum(arg0.sort(), arg1.sort())(arg0, arg1);
701 }
702
705
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
718 inline
720 {
721 return is_application(e) && is_minimum_function_symbol(atermpp::down_cast<application>(e).head());
722 }
723
726 inline
728 {
730 return abs_name;
731 }
732
733 // This function is not intended for public use and therefore not documented in Doxygen.
734 inline
735 function_symbol abs(const sort_expression& s0)
736 {
737 sort_expression target_sort;
738 if (s0 == real_())
739 {
740 target_sort = real_();
741 }
742 else if (s0 == sort_int::int_())
743 {
745 }
746 else
747 {
748 throw mcrl2::runtime_error("Cannot compute target sort for abs with domain sorts " + pp(s0) + ". ");
749 }
750
751 function_symbol abs(abs_name(), make_function_sort_(s0, target_sort));
752 return abs;
753 }
754
758 inline
760 {
761 if (is_function_symbol(e))
762 {
763 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
764 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 return false;
767 }
768
770
773 inline
774 application abs(const data_expression& arg0)
775 {
776 return sort_real::abs(arg0.sort())(arg0);
777 }
778
781
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
793 inline
795 {
796 return is_application(e) && is_abs_function_symbol(atermpp::down_cast<application>(e).head());
797 }
798
801 inline
803 {
805 return negate_name;
806 }
807
808 // This function is not intended for public use and therefore not documented in Doxygen.
809 inline
810 function_symbol negate(const sort_expression& s0)
811 {
812 sort_expression target_sort;
813 if (s0 == real_())
814 {
815 target_sort = real_();
816 }
817 else if (s0 == sort_pos::pos())
818 {
820 }
821 else if (s0 == sort_nat::nat())
822 {
824 }
825 else if (s0 == sort_int::int_())
826 {
828 }
829 else
830 {
831 throw mcrl2::runtime_error("Cannot compute target sort for negate with domain sorts " + pp(s0) + ". ");
832 }
833
835 return negate;
836 }
837
841 inline
843 {
844 if (is_function_symbol(e))
845 {
846 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
847 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 return false;
850 }
851
853
856 inline
857 application negate(const data_expression& arg0)
858 {
859 return sort_real::negate(arg0.sort())(arg0);
860 }
861
864
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
876 inline
878 {
879 return is_application(e) && is_negate_function_symbol(atermpp::down_cast<application>(e).head());
880 }
881
884 inline
886 {
888 return succ_name;
889 }
890
891 // This function is not intended for public use and therefore not documented in Doxygen.
892 inline
893 function_symbol succ(const sort_expression& s0)
894 {
895 sort_expression target_sort;
896 if (s0 == real_())
897 {
898 target_sort = real_();
899 }
900 else if (s0 == sort_int::int_())
901 {
903 }
904 else if (s0 == sort_nat::nat())
905 {
907 }
908 else if (s0 == sort_pos::pos())
909 {
911 }
912 else
913 {
914 throw mcrl2::runtime_error("Cannot compute target sort for succ with domain sorts " + pp(s0) + ". ");
915 }
916
918 return succ;
919 }
920
924 inline
926 {
927 if (is_function_symbol(e))
928 {
929 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
930 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 return false;
933 }
934
936
939 inline
940 application succ(const data_expression& arg0)
941 {
942 return sort_real::succ(arg0.sort())(arg0);
943 }
944
947
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
959 inline
961 {
962 return is_application(e) && is_succ_function_symbol(atermpp::down_cast<application>(e).head());
963 }
964
967 inline
969 {
971 return pred_name;
972 }
973
974 // This function is not intended for public use and therefore not documented in Doxygen.
975 inline
976 function_symbol pred(const sort_expression& s0)
977 {
978 sort_expression target_sort;
979 if (s0 == real_())
980 {
981 target_sort = real_();
982 }
983 else if (s0 == sort_nat::nat())
984 {
986 }
987 else if (s0 == sort_int::int_())
988 {
990 }
991 else if (s0 == sort_pos::pos())
992 {
994 }
995 else
996 {
997 throw mcrl2::runtime_error("Cannot compute target sort for pred with domain sorts " + pp(s0) + ". ");
998 }
999
1001 return pred;
1002 }
1003
1007 inline
1009 {
1010 if (is_function_symbol(e))
1011 {
1012 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1013 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 return false;
1016 }
1017
1019
1022 inline
1023 application pred(const data_expression& arg0)
1024 {
1025 return sort_real::pred(arg0.sort())(arg0);
1026 }
1027
1030
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
1042 inline
1043 bool is_pred_application(const atermpp::aterm& e)
1044 {
1045 return is_application(e) && is_pred_function_symbol(atermpp::down_cast<application>(e).head());
1046 }
1047
1050 inline
1052 {
1054 return plus_name;
1055 }
1056
1057 // This function is not intended for public use and therefore not documented in Doxygen.
1058 inline
1059 function_symbol plus(const sort_expression& s0, const sort_expression& s1)
1060 {
1061 sort_expression target_sort;
1062 if (s0 == real_() && s1 == real_())
1063 {
1064 target_sort = real_();
1065 }
1066 else if (s0 == sort_int::int_() && s1 == sort_int::int_())
1067 {
1069 }
1070 else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
1071 {
1073 }
1074 else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
1075 {
1077 }
1078 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1079 {
1081 }
1082 else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
1083 {
1085 }
1086 else
1087 {
1088 throw mcrl2::runtime_error("Cannot compute target sort for plus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1089 }
1090
1091 function_symbol plus(plus_name(), make_function_sort_(s0, s1, target_sort));
1092 return plus;
1093 }
1094
1098 inline
1100 {
1101 if (is_function_symbol(e))
1102 {
1103 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1104 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 return false;
1107 }
1108
1110
1114 inline
1115 application plus(const data_expression& arg0, const data_expression& arg1)
1116 {
1117 return sort_real::plus(arg0.sort(), arg1.sort())(arg0, arg1);
1118 }
1119
1122
1125 inline
1126 void make_plus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1127 {
1128 make_application(result, sort_real::plus(arg0.sort(), arg1.sort()),arg0, arg1);
1129 }
1130
1135 inline
1136 bool is_plus_application(const atermpp::aterm& e)
1137 {
1138 return is_application(e) && is_plus_function_symbol(atermpp::down_cast<application>(e).head());
1139 }
1140
1143 inline
1145 {
1147 return minus_name;
1148 }
1149
1150 // This function is not intended for public use and therefore not documented in Doxygen.
1151 inline
1152 function_symbol minus(const sort_expression& s0, const sort_expression& s1)
1153 {
1154 sort_expression target_sort;
1155 if (s0 == real_() && s1 == real_())
1156 {
1157 target_sort = real_();
1158 }
1159 else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
1160 {
1162 }
1163 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1164 {
1166 }
1167 else if (s0 == sort_int::int_() && s1 == sort_int::int_())
1168 {
1170 }
1171 else
1172 {
1173 throw mcrl2::runtime_error("Cannot compute target sort for minus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1174 }
1175
1176 function_symbol minus(minus_name(), make_function_sort_(s0, s1, target_sort));
1177 return minus;
1178 }
1179
1183 inline
1185 {
1186 if (is_function_symbol(e))
1187 {
1188 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1189 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 return false;
1192 }
1193
1195
1199 inline
1200 application minus(const data_expression& arg0, const data_expression& arg1)
1201 {
1202 return sort_real::minus(arg0.sort(), arg1.sort())(arg0, arg1);
1203 }
1204
1207
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
1220 inline
1222 {
1223 return is_application(e) && is_minus_function_symbol(atermpp::down_cast<application>(e).head());
1224 }
1225
1228 inline
1230 {
1232 return times_name;
1233 }
1234
1235 // This function is not intended for public use and therefore not documented in Doxygen.
1236 inline
1237 function_symbol times(const sort_expression& s0, const sort_expression& s1)
1238 {
1239 sort_expression target_sort;
1240 if (s0 == real_() && s1 == real_())
1241 {
1242 target_sort = real_();
1243 }
1244 else if (s0 == sort_int::int_() && s1 == sort_int::int_())
1245 {
1247 }
1248 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1249 {
1251 }
1252 else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
1253 {
1255 }
1256 else
1257 {
1258 throw mcrl2::runtime_error("Cannot compute target sort for times with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1259 }
1260
1261 function_symbol times(times_name(), make_function_sort_(s0, s1, target_sort));
1262 return times;
1263 }
1264
1268 inline
1270 {
1271 if (is_function_symbol(e))
1272 {
1273 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1274 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 return false;
1277 }
1278
1280
1284 inline
1285 application times(const data_expression& arg0, const data_expression& arg1)
1286 {
1287 return sort_real::times(arg0.sort(), arg1.sort())(arg0, arg1);
1288 }
1289
1292
1295 inline
1296 void make_times(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1297 {
1298 make_application(result, sort_real::times(arg0.sort(), arg1.sort()),arg0, arg1);
1299 }
1300
1305 inline
1307 {
1308 return is_application(e) && is_times_function_symbol(atermpp::down_cast<application>(e).head());
1309 }
1310
1313 inline
1315 {
1317 return exp_name;
1318 }
1319
1320 // This function is not intended for public use and therefore not documented in Doxygen.
1321 inline
1322 function_symbol exp(const sort_expression& s0, const sort_expression& s1)
1323 {
1324 sort_expression target_sort;
1325 if (s0 == real_() && s1 == sort_int::int_())
1326 {
1327 target_sort = real_();
1328 }
1329 else if (s0 == sort_int::int_() && s1 == sort_nat::nat())
1330 {
1332 }
1333 else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
1334 {
1336 }
1337 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1338 {
1340 }
1341 else
1342 {
1343 throw mcrl2::runtime_error("Cannot compute target sort for exp with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1344 }
1345
1346 function_symbol exp(exp_name(), make_function_sort_(s0, s1, target_sort));
1347 return exp;
1348 }
1349
1353 inline
1355 {
1356 if (is_function_symbol(e))
1357 {
1358 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1359 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 return false;
1362 }
1363
1365
1369 inline
1370 application exp(const data_expression& arg0, const data_expression& arg1)
1371 {
1372 return sort_real::exp(arg0.sort(), arg1.sort())(arg0, arg1);
1373 }
1374
1377
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
1390 inline
1391 bool is_exp_application(const atermpp::aterm& e)
1392 {
1393 return is_application(e) && is_exp_function_symbol(atermpp::down_cast<application>(e).head());
1394 }
1395
1398 inline
1400 {
1402 return divides_name;
1403 }
1404
1405 // This function is not intended for public use and therefore not documented in Doxygen.
1406 inline
1407 function_symbol divides(const sort_expression& s0, const sort_expression& s1)
1408 {
1409 sort_expression target_sort(real_());
1411 return divides;
1412 }
1413
1417 inline
1419 {
1420 if (is_function_symbol(e))
1421 {
1422 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1423 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 return false;
1426 }
1427
1429
1433 inline
1434 application divides(const data_expression& arg0, const data_expression& arg1)
1435 {
1436 return sort_real::divides(arg0.sort(), arg1.sort())(arg0, arg1);
1437 }
1438
1441
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
1454 inline
1456 {
1457 return is_application(e) && is_divides_function_symbol(atermpp::down_cast<application>(e).head());
1458 }
1459
1462 inline
1464 {
1466 return floor_name;
1467 }
1468
1470
1472 inline
1473 const function_symbol& floor()
1474 {
1476 return floor;
1477 }
1478
1482 inline
1484 {
1485 if (is_function_symbol(e))
1486 {
1487 return atermpp::down_cast<function_symbol>(e) == floor();
1488 }
1489 return false;
1490 }
1491
1493
1496 inline
1497 application floor(const data_expression& arg0)
1498 {
1499 return sort_real::floor()(arg0);
1500 }
1501
1504
1506 inline
1507 void make_floor(data_expression& result, const data_expression& arg0)
1508 {
1509 make_application(result, sort_real::floor(),arg0);
1510 }
1511
1516 inline
1518 {
1519 return is_application(e) && is_floor_function_symbol(atermpp::down_cast<application>(e).head());
1520 }
1521
1524 inline
1526 {
1528 return ceil_name;
1529 }
1530
1532
1534 inline
1535 const function_symbol& ceil()
1536 {
1538 return ceil;
1539 }
1540
1544 inline
1546 {
1547 if (is_function_symbol(e))
1548 {
1549 return atermpp::down_cast<function_symbol>(e) == ceil();
1550 }
1551 return false;
1552 }
1553
1555
1558 inline
1559 application ceil(const data_expression& arg0)
1560 {
1561 return sort_real::ceil()(arg0);
1562 }
1563
1566
1568 inline
1569 void make_ceil(data_expression& result, const data_expression& arg0)
1570 {
1571 make_application(result, sort_real::ceil(),arg0);
1572 }
1573
1578 inline
1579 bool is_ceil_application(const atermpp::aterm& e)
1580 {
1581 return is_application(e) && is_ceil_function_symbol(atermpp::down_cast<application>(e).head());
1582 }
1583
1586 inline
1588 {
1590 return round_name;
1591 }
1592
1594
1596 inline
1597 const function_symbol& round()
1598 {
1600 return round;
1601 }
1602
1606 inline
1608 {
1609 if (is_function_symbol(e))
1610 {
1611 return atermpp::down_cast<function_symbol>(e) == round();
1612 }
1613 return false;
1614 }
1615
1617
1620 inline
1621 application round(const data_expression& arg0)
1622 {
1623 return sort_real::round()(arg0);
1624 }
1625
1628
1630 inline
1631 void make_round(data_expression& result, const data_expression& arg0)
1632 {
1633 make_application(result, sort_real::round(),arg0);
1634 }
1635
1640 inline
1642 {
1643 return is_application(e) && is_round_function_symbol(atermpp::down_cast<application>(e).head());
1644 }
1645
1648 inline
1650 {
1652 return reduce_fraction_name;
1653 }
1654
1656
1658 inline
1660 {
1662 return reduce_fraction;
1663 }
1664
1668 inline
1670 {
1671 if (is_function_symbol(e))
1672 {
1673 return atermpp::down_cast<function_symbol>(e) == reduce_fraction();
1674 }
1675 return false;
1676 }
1677
1679
1683 inline
1684 application reduce_fraction(const data_expression& arg0, const data_expression& arg1)
1685 {
1686 return sort_real::reduce_fraction()(arg0, arg1);
1687 }
1688
1691
1694 inline
1695 void make_reduce_fraction(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1696 {
1698 }
1699
1704 inline
1706 {
1707 return is_application(e) && is_reduce_fraction_function_symbol(atermpp::down_cast<application>(e).head());
1708 }
1709
1712 inline
1714 {
1717 }
1718
1720
1722 inline
1724 {
1726 return reduce_fraction_where;
1727 }
1728
1732 inline
1734 {
1735 if (is_function_symbol(e))
1736 {
1737 return atermpp::down_cast<function_symbol>(e) == reduce_fraction_where();
1738 }
1739 return false;
1740 }
1741
1743
1748 inline
1749 application reduce_fraction_where(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
1750 {
1752 }
1753
1756
1760 inline
1761 void make_reduce_fraction_where(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
1762 {
1764 }
1765
1770 inline
1772 {
1773 return is_application(e) && is_reduce_fraction_where_function_symbol(atermpp::down_cast<application>(e).head());
1774 }
1775
1778 inline
1780 {
1783 }
1784
1786
1788 inline
1790 {
1793 }
1794
1798 inline
1800 {
1801 if (is_function_symbol(e))
1802 {
1803 return atermpp::down_cast<function_symbol>(e) == reduce_fraction_helper();
1804 }
1805 return false;
1806 }
1807
1809
1813 inline
1814 application reduce_fraction_helper(const data_expression& arg0, const data_expression& arg1)
1815 {
1817 }
1818
1821
1824 inline
1825 void make_reduce_fraction_helper(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1826 {
1828 }
1829
1834 inline
1836 {
1837 return is_application(e) && is_reduce_fraction_helper_function_symbol(atermpp::down_cast<application>(e).head());
1838 }
1841 inline
1843 {
1845 result.push_back(sort_real::creal());
1846 result.push_back(sort_real::pos2real());
1847 result.push_back(sort_real::nat2real());
1848 result.push_back(sort_real::int2real());
1849 result.push_back(sort_real::real2pos());
1850 result.push_back(sort_real::real2nat());
1851 result.push_back(sort_real::real2int());
1852 result.push_back(sort_real::maximum(real_(), real_()));
1853 result.push_back(sort_real::minimum(real_(), real_()));
1854 result.push_back(sort_real::abs(real_()));
1855 result.push_back(sort_real::negate(real_()));
1856 result.push_back(sort_real::succ(real_()));
1857 result.push_back(sort_real::pred(real_()));
1858 result.push_back(sort_real::plus(real_(), real_()));
1859 result.push_back(sort_real::minus(real_(), real_()));
1860 result.push_back(sort_real::times(real_(), real_()));
1861 result.push_back(sort_real::exp(real_(), sort_int::int_()));
1862 result.push_back(sort_real::divides(sort_pos::pos(), sort_pos::pos()));
1863 result.push_back(sort_real::divides(sort_nat::nat(), sort_nat::nat()));
1864 result.push_back(sort_real::divides(sort_int::int_(), sort_int::int_()));
1865 result.push_back(sort_real::divides(real_(), real_()));
1866 result.push_back(sort_real::floor());
1867 result.push_back(sort_real::ceil());
1868 result.push_back(sort_real::round());
1869 result.push_back(sort_real::reduce_fraction());
1870 result.push_back(sort_real::reduce_fraction_where());
1871 result.push_back(sort_real::reduce_fraction_helper());
1872 return result;
1873 }
1874
1877 inline
1879 {
1881 for(const function_symbol& f: real_generate_constructors_code())
1882 {
1883 result.push_back(f);
1884 }
1885 return result;
1886 }
1887
1890 inline
1892 {
1894 result.push_back(sort_real::creal());
1895 result.push_back(sort_real::pos2real());
1896 result.push_back(sort_real::nat2real());
1897 result.push_back(sort_real::int2real());
1898 result.push_back(sort_real::real2pos());
1899 result.push_back(sort_real::real2nat());
1900 result.push_back(sort_real::real2int());
1901 result.push_back(sort_real::maximum(real_(), real_()));
1902 result.push_back(sort_real::minimum(real_(), real_()));
1903 result.push_back(sort_real::abs(real_()));
1904 result.push_back(sort_real::negate(real_()));
1905 result.push_back(sort_real::succ(real_()));
1906 result.push_back(sort_real::pred(real_()));
1907 result.push_back(sort_real::plus(real_(), real_()));
1908 result.push_back(sort_real::minus(real_(), real_()));
1909 result.push_back(sort_real::times(real_(), real_()));
1910 result.push_back(sort_real::exp(real_(), sort_int::int_()));
1911 result.push_back(sort_real::divides(sort_pos::pos(), sort_pos::pos()));
1912 result.push_back(sort_real::divides(sort_nat::nat(), sort_nat::nat()));
1913 result.push_back(sort_real::divides(sort_int::int_(), sort_int::int_()));
1914 result.push_back(sort_real::divides(real_(), real_()));
1915 result.push_back(sort_real::floor());
1916 result.push_back(sort_real::ceil());
1917 result.push_back(sort_real::round());
1918 result.push_back(sort_real::reduce_fraction());
1919 result.push_back(sort_real::reduce_fraction_where());
1920 result.push_back(sort_real::reduce_fraction_helper());
1921 return result;
1922 }
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<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
1929 inline
1931 {
1932 implementation_map result;
1933 return result;
1934 }
1940 inline
1941 const data_expression& left(const data_expression& e)
1942 {
1944 return atermpp::down_cast<application>(e)[0];
1945 }
1946
1952 inline
1953 const data_expression& right(const data_expression& e)
1954 {
1956 return atermpp::down_cast<application>(e)[1];
1957 }
1958
1964 inline
1965 const data_expression& arg(const data_expression& e)
1966 {
1968 return atermpp::down_cast<application>(e)[0];
1969 }
1970
1976 inline
1977 const data_expression& arg1(const data_expression& e)
1978 {
1980 return atermpp::down_cast<application>(e)[0];
1981 }
1982
1988 inline
1989 const data_expression& arg2(const data_expression& e)
1990 {
1992 return atermpp::down_cast<application>(e)[1];
1993 }
1994
2000 inline
2001 const data_expression& arg3(const data_expression& e)
2002 {
2004 return atermpp::down_cast<application>(e)[2];
2005 }
2006
2009 inline
2011 {
2012 variable vm("m",sort_nat::nat());
2013 variable vn("n",sort_nat::nat());
2014 variable vp("p",sort_pos::pos());
2015 variable vq("q",sort_pos::pos());
2016 variable vx("x",sort_int::int_());
2017 variable vy("y",sort_int::int_());
2018 variable vr("r",real_());
2019 variable vs("s",real_());
2020
2021 data_equation_vector result;
2022 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::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp))))));
2023 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::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp))))));
2024 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::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp))))));
2025 result.push_back(data_equation(variable_list({vx}), int2real(vx), creal(vx, sort_pos::c1())));
2026 result.push_back(data_equation(variable_list({vn}), nat2real(vn), creal(sort_int::cint(vn), sort_pos::c1())));
2027 result.push_back(data_equation(variable_list({vp}), pos2real(vp), creal(sort_int::cint(sort_nat::pos2nat(vp)), sort_pos::c1())));
2028 result.push_back(data_equation(variable_list({vp, vx}), equal_to(vp, sort_pos::c1()), real2int(creal(vx, vp)), vx));
2029 result.push_back(data_equation(variable_list({vp, vx}), equal_to(vp, sort_pos::c1()), real2nat(creal(vx, vp)), sort_int::int2nat(vx)));
2030 result.push_back(data_equation(variable_list({vp, vx}), equal_to(vp, sort_pos::c1()), real2pos(creal(vx, vp)), sort_int::int2pos(vx)));
2031 result.push_back(data_equation(variable_list({vr, vs}), minimum(vr, vs), if_(less(vr, vs), vr, vs)));
2032 result.push_back(data_equation(variable_list({vr, vs}), maximum(vr, vs), if_(less(vr, vs), vs, vr)));
2033 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 result.push_back(data_equation(variable_list({vp, vx}), negate(creal(vx, vp)), creal(negate(vx), vp)));
2035 result.push_back(data_equation(variable_list({vp, vx}), succ(creal(vx, vp)), creal(plus(vx, sort_int::cint(sort_nat::pos2nat(vp))), vp)));
2036 result.push_back(data_equation(variable_list({vp, vx}), pred(creal(vx, vp)), creal(minus(vx, sort_int::cint(sort_nat::pos2nat(vp))), vp)));
2037 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::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp)))), sort_int::cint(sort_nat::pos2nat(times(vp, vq))))));
2038 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::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp)))), sort_int::cint(sort_nat::pos2nat(times(vp, vq))))));
2039 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::pos2nat(times(vp, vq))))));
2040 result.push_back(data_equation(variable_list({vm, vp, vr}), sort_nat::equals_zero(vm), times(vr, creal(sort_int::cint(vm), vp)), creal(sort_int::cint(sort_nat::c0()), sort_pos::c1())));
2041 result.push_back(data_equation(variable_list({vm, vp, vr}), sort_nat::equals_zero(vm), times(creal(sort_int::cint(vm), vp), vr), creal(sort_int::cint(sort_nat::c0()), sort_pos::c1())));
2042 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::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp))))));
2043 result.push_back(data_equation(variable_list({vp, vq}), divides(vp, vq), reduce_fraction(sort_int::cint(sort_nat::pos2nat(vp)), sort_int::cint(sort_nat::pos2nat(vq)))));
2044 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 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 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::pos2nat(exp(vp, vn))))));
2047 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::pos2nat(exp(vp, sort_nat::pos2nat(vq)))), exp(vx, sort_nat::pos2nat(vq)))));
2048 result.push_back(data_equation(variable_list({vp, vx}), floor(creal(vx, vp)), sort_int::div(vx, vp)));
2049 result.push_back(data_equation(variable_list({vr}), ceil(vr), negate(floor(negate(vr)))));
2050 result.push_back(data_equation(variable_list({vr}), round(vr), floor(plus(vr, creal(sort_int::cint(sort_nat::pos2nat(sort_pos::c1())), plus(sort_pos::c1(), sort_pos::c1()))))));
2051 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::pos2nat(vp)))));
2052 result.push_back(data_equation(variable_list({vn, vx}), reduce_fraction(vx, sort_int::cint(vn)), reduce_fraction_where(vn, sort_int::div(vx, sort_nat::nat2pos(vn)), sort_int::mod(vx, sort_nat::nat2pos(vn)))));
2053 result.push_back(data_equation(variable_list({vm, vn, vx}), sort_nat::equals_zero(vm), reduce_fraction_where(vn, vx, vm), creal(vx, sort_pos::c1())));
2054 result.push_back(data_equation(variable_list({vm, vn, vx}), sort_nat::not_equals_zero(vm), reduce_fraction_where(vn, vx, vm), reduce_fraction_helper(reduce_fraction(sort_int::cint(vn), sort_int::cint(vm)), vx)));
2055 result.push_back(data_equation(variable_list({vp, vx, vy}), reduce_fraction_helper(creal(vx, vp), vy), creal(plus(sort_int::cint(sort_nat::pos2nat(vp)), times(vy, vx)), sort_int::int2pos(vx))));
2056 return result;
2057 }
2058
2059 } // namespace sort_real_
2060
2061 } // namespace data
2062
2063} // namespace mcrl2
2064
2065#endif // MCRL2_DATA_REAL64_H
The class application.
The class basic_sort.
The standard sort bool_.
size_type size() const
Returns the number of arguments of this term.
Definition aterm.h:151
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
Standard exception class for reporting runtime errors.
Definition exception.h:27
The class function symbol.
The class data_equation.
Exception classes for use in libraries and tools.
The class function_sort.
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
const function_symbol & int2nat()
Constructor for function symbol Int2Nat.
Definition int1.h:298
const function_symbol & cneg()
Constructor for function symbol @cNeg.
Definition int1.h:142
const function_symbol & int2pos()
Constructor for function symbol Int2Pos.
Definition int1.h:422
const function_symbol & cint()
Constructor for function symbol @cInt.
Definition int1.h:80
function_symbol mod(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1261
function_symbol div(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1184
const basic_sort & int_()
Constructor for sort expression Int.
Definition int1.h:47
function_symbol head(const sort_expression &s)
Constructor for function symbol head.
Definition list1.h:526
const function_symbol & c0()
Constructor for function symbol @c0.
Definition nat1.h:108
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
const function_symbol & not_equals_zero()
Constructor for function symbol @not_equals_zero.
Definition nat64.h:502
const function_symbol & nat2pos()
Constructor for function symbol Nat2Pos.
Definition nat1.h:362
const function_symbol & equals_zero()
Constructor for function symbol @equals_zero.
Definition nat64.h:440
const function_symbol & pos2nat()
Constructor for function symbol Pos2Nat.
Definition nat1.h:300
const function_symbol & c1()
Constructor for function symbol @c1.
Definition pos1.h:78
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:650
void make_abs(data_expression &result, const data_expression &arg0)
Make an application of function symbol abs.
Definition real1.h:784
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1059
bool is_real2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Int.
Definition real1.h:491
void make_minus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition real1.h:1211
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real1.h:107
void make_reduce_fraction(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @redfrac.
Definition real1.h:1695
const core::identifier_string & maximum_name()
Generate identifier max.
Definition real1.h:533
void make_negate(data_expression &result, const data_expression &arg0)
Make an application of function symbol -.
Definition real1.h:867
const core::identifier_string & minus_name()
Generate identifier -.
Definition real1.h:1144
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition real1.h:925
const core::identifier_string & real_name()
Definition real1.h:39
const function_symbol & pos2real()
Constructor for function symbol Pos2Real.
Definition real1.h:171
const core::identifier_string & reduce_fraction_where_name()
Generate identifier @redfracwhr.
Definition real1.h:1713
const function_symbol & round()
Constructor for function symbol round.
Definition real1.h:1597
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition real1.h:1099
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1237
bool is_abs_application(const atermpp::aterm &e)
Recogniser for application of abs.
Definition real1.h:794
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1407
const core::identifier_string & int2real_name()
Generate identifier Int2Real.
Definition real1.h:285
const function_symbol & real2nat()
Constructor for function symbol Real2Nat.
Definition real1.h:419
bool is_divides_function_symbol(const atermpp::aterm &e)
Recogniser for function /.
Definition real1.h:1418
const core::identifier_string & creal_name()
Generate identifier @cReal.
Definition real1.h:97
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition real1.h:950
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition real1.h:1391
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition real1.h:1965
bool is_int2real_application(const atermpp::aterm &e)
Recogniser for application of Int2Real.
Definition real1.h:339
const function_symbol & ceil()
Constructor for function symbol ceil.
Definition real1.h:1535
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition real1.h:1989
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1136
bool is_divides_application(const atermpp::aterm &e)
Recogniser for application of /.
Definition real1.h:1455
bool is_reduce_fraction_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfrac.
Definition real1.h:1669
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition real1.h:597
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition real1.h:1381
const core::identifier_string & divides_name()
Generate identifier /.
Definition real1.h:1399
bool is_real2int_application(const atermpp::aterm &e)
Recogniser for application of Real2Int.
Definition real1.h:525
const core::identifier_string & ceil_name()
Generate identifier ceil.
Definition real1.h:1525
bool is_creal_function_symbol(const atermpp::aterm &e)
Recogniser for function @cReal.
Definition real1.h:117
void make_real2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Nat.
Definition real1.h:453
bool is_minus_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition real1.h:1184
bool is_reduce_fraction_where_application(const atermpp::aterm &e)
Recogniser for application of @redfracwhr.
Definition real1.h:1771
function_symbol succ(const sort_expression &s0)
Definition real1.h:893
bool is_floor_function_symbol(const atermpp::aterm &e)
Recogniser for function floor.
Definition real1.h:1483
void make_int2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Real.
Definition real1.h:329
void make_divides(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol /.
Definition real1.h:1445
const core::identifier_string & floor_name()
Generate identifier floor.
Definition real1.h:1463
const core::identifier_string & times_name()
Generate identifier *.
Definition real1.h:1229
bool is_abs_function_symbol(const atermpp::aterm &e)
Recogniser for function abs.
Definition real1.h:759
bool is_ceil_application(const atermpp::aterm &e)
Recogniser for application of ceil.
Definition real1.h:1579
const function_symbol & real2int()
Constructor for function symbol Real2Int.
Definition real1.h:481
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition real1.h:634
const function_symbol & reduce_fraction()
Constructor for function symbol @redfrac.
Definition real1.h:1659
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:153
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition real1.h:1043
const core::identifier_string & negate_name()
Generate identifier -.
Definition real1.h:802
void make_reduce_fraction_helper(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @redfrachlp.
Definition real1.h:1825
void make_pos2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Real.
Definition real1.h:205
function_symbol pred(const sort_expression &s0)
Definition real1.h:976
bool is_round_function_symbol(const atermpp::aterm &e)
Recogniser for function round.
Definition real1.h:1607
const core::identifier_string & succ_name()
Generate identifier succ.
Definition real1.h:885
const function_symbol & reduce_fraction_helper()
Constructor for function symbol @redfrachlp.
Definition real1.h:1789
const core::identifier_string & abs_name()
Generate identifier abs.
Definition real1.h:727
data_equation_vector real_generate_equations_code()
Give all system defined equations for real_.
Definition real1.h:2010
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition real1.h:1269
const core::identifier_string & round_name()
Generate identifier round.
Definition real1.h:1587
bool is_negate_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition real1.h:842
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1152
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition real1.h:682
const function_symbol & floor()
Constructor for function symbol floor.
Definition real1.h:1473
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition real1.h:709
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition real1.h:1296
const core::identifier_string & reduce_fraction_helper_name()
Generate identifier @redfrachlp.
Definition real1.h:1779
function_symbol_vector real_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for real_.
Definition real1.h:78
bool is_real2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Pos.
Definition real1.h:367
void make_real2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Int.
Definition real1.h:515
function_symbol_vector real_generate_constructors_code()
Give all system defined constructors for real_.
Definition real1.h:70
void make_nat2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Real.
Definition real1.h:267
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition real1.h:624
bool is_floor_application(const atermpp::aterm &e)
Recogniser for application of floor.
Definition real1.h:1517
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:58
const function_symbol & reduce_fraction_where()
Constructor for function symbol @redfracwhr.
Definition real1.h:1723
implementation_map real_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for real_.
Definition real1.h:1930
bool is_ceil_function_symbol(const atermpp::aterm &e)
Recogniser for function ceil.
Definition real1.h:1545
const core::identifier_string & pred_name()
Generate identifier pred.
Definition real1.h:968
const function_symbol & nat2real()
Constructor for function symbol Nat2Real.
Definition real1.h:233
const core::identifier_string & minimum_name()
Generate identifier min.
Definition real1.h:642
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition real1.h:1953
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition real1.h:960
void make_round(data_expression &result, const data_expression &arg0)
Make an application of function symbol round.
Definition real1.h:1631
bool is_pos2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Real.
Definition real1.h:181
function_symbol_vector real_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for real_.
Definition real1.h:1891
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition real1.h:1977
const core::identifier_string & plus_name()
Generate identifier +.
Definition real1.h:1051
function_symbol abs(const sort_expression &s0)
Definition real1.h:735
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition real1.h:1941
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1306
void make_ceil(data_expression &result, const data_expression &arg0)
Make an application of function symbol ceil.
Definition real1.h:1569
const core::identifier_string & reduce_fraction_name()
Generate identifier @redfrac.
Definition real1.h:1649
function_symbol negate(const sort_expression &s0)
Definition real1.h:810
bool is_real2pos_application(const atermpp::aterm &e)
Recogniser for application of Real2Pos.
Definition real1.h:401
bool is_reduce_fraction_application(const atermpp::aterm &e)
Recogniser for application of @redfrac.
Definition real1.h:1705
bool is_int2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Real.
Definition real1.h:305
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:877
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition real1.h:84
bool is_reduce_fraction_helper_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfrachlp.
Definition real1.h:1799
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition real1.h:719
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1221
const core::identifier_string & pos2real_name()
Generate identifier Pos2Real.
Definition real1.h:161
bool is_round_application(const atermpp::aterm &e)
Recogniser for application of round.
Definition real1.h:1641
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition real1.h:2001
const core::identifier_string & exp_name()
Generate identifier exp.
Definition real1.h:1314
bool is_real2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Nat.
Definition real1.h:429
const core::identifier_string & real2nat_name()
Generate identifier Real2Nat.
Definition real1.h:409
const core::identifier_string & real2int_name()
Generate identifier Real2Int.
Definition real1.h:471
const function_symbol & int2real()
Constructor for function symbol Int2Real.
Definition real1.h:295
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition real1.h:1008
const core::identifier_string & nat2real_name()
Generate identifier Nat2Real.
Definition real1.h:223
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1322
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition real1.h:1033
bool is_real2nat_application(const atermpp::aterm &e)
Recogniser for application of Real2Nat.
Definition real1.h:463
bool is_pos2real_application(const atermpp::aterm &e)
Recogniser for application of Pos2Real.
Definition real1.h:215
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition real1.h:1126
bool is_reduce_fraction_helper_application(const atermpp::aterm &e)
Recogniser for application of @redfrachlp.
Definition real1.h:1835
void make_floor(data_expression &result, const data_expression &arg0)
Make an application of function symbol floor.
Definition real1.h:1507
const function_symbol & real2pos()
Constructor for function symbol Real2Pos.
Definition real1.h:357
implementation_map real_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition real1.h:88
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:541
function_symbol_vector real_generate_functions_code()
Give all system defined mappings for real_.
Definition real1.h:1842
void make_reduce_fraction_where(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @redfracwhr.
Definition real1.h:1761
function_symbol_vector real_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for real_.
Definition real1.h:1878
const core::identifier_string & real2pos_name()
Generate identifier Real2Pos.
Definition real1.h:347
void make_real2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Pos.
Definition real1.h:391
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition real1.h:1354
void make_creal(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cReal.
Definition real1.h:143
bool is_reduce_fraction_where_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfracwhr.
Definition real1.h:1733
bool is_nat2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Real.
Definition real1.h:243
bool is_nat2real_application(const atermpp::aterm &e)
Recogniser for application of Nat2Real.
Definition real1.h:277
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:240
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
std::string pp(const abstraction &x)
Definition data.cpp:39
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
atermpp::term_list< variable > variable_list
\brief list of variables
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
void make_application(atermpp::aterm &result)
Make function for an application.
data::sort_expression target_sort(const data::sort_expression &s)
Definition absinthe.h:101
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Standard functions that are available for all sorts.