mCRL2
Loading...
Searching...
No Matches
int64.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_INT64_H
16#define MCRL2_DATA_INT64_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
30namespace mcrl2 {
31
32 namespace data {
33
35 namespace sort_int {
36
37 inline
39 {
41 return int_name;
42 }
43
46 inline
47 const basic_sort& int_()
48 {
49 static basic_sort int_ = basic_sort(int_name());
50 return int_;
51 }
52
56 inline
57 bool is_int(const sort_expression& e)
58 {
59 if (is_basic_sort(e))
60 {
61 return basic_sort(e) == int_();
62 }
63 return false;
64 }
65
66
69 inline
71 {
73 return cint_name;
74 }
75
77
79 inline
80 const function_symbol& cint()
81 {
83 return cint;
84 }
85
89 inline
91 {
92 if (is_function_symbol(e))
93 {
94 return atermpp::down_cast<function_symbol>(e) == cint();
95 }
96 return false;
97 }
98
100
103 inline
104 application cint(const data_expression& arg0)
105 {
106 return sort_int::cint()(arg0);
107 }
108
111
113 inline
114 void make_cint(data_expression& result, const data_expression& arg0)
115 {
116 make_application(result, sort_int::cint(),arg0);
117 }
118
123 inline
125 {
126 return is_application(e) && is_cint_function_symbol(atermpp::down_cast<application>(e).head());
127 }
128
131 inline
133 {
135 return cneg_name;
136 }
137
139
141 inline
142 const function_symbol& cneg()
143 {
145 return cneg;
146 }
147
151 inline
153 {
154 if (is_function_symbol(e))
155 {
156 return atermpp::down_cast<function_symbol>(e) == cneg();
157 }
158 return false;
159 }
160
162
165 inline
166 application cneg(const data_expression& arg0)
167 {
168 return sort_int::cneg()(arg0);
169 }
170
173
175 inline
176 void make_cneg(data_expression& result, const data_expression& arg0)
177 {
178 make_application(result, sort_int::cneg(),arg0);
179 }
180
185 inline
187 {
188 return is_application(e) && is_cneg_function_symbol(atermpp::down_cast<application>(e).head());
189 }
192 inline
194 {
196 result.push_back(sort_int::cint());
197 result.push_back(sort_int::cneg());
198
199 return result;
200 }
203 inline
205 {
207 result.push_back(sort_int::cint());
208 result.push_back(sort_int::cneg());
209
210 return result;
211 }
212 // 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
213 typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
216 inline
218 {
219 implementation_map result;
220 return result;
221 }
222
225 inline
227 {
229 return nat2int_name;
230 }
231
233
235 inline
236 const function_symbol& nat2int()
237 {
239 return nat2int;
240 }
241
245 inline
247 {
248 if (is_function_symbol(e))
249 {
250 return atermpp::down_cast<function_symbol>(e) == nat2int();
251 }
252 return false;
253 }
254
256
259 inline
260 application nat2int(const data_expression& arg0)
261 {
262 return sort_int::nat2int()(arg0);
263 }
264
267
269 inline
270 void make_nat2int(data_expression& result, const data_expression& arg0)
271 {
272 make_application(result, sort_int::nat2int(),arg0);
273 }
274
279 inline
281 {
282 return is_application(e) && is_nat2int_function_symbol(atermpp::down_cast<application>(e).head());
283 }
284
287 inline
289 {
291 return int2nat_name;
292 }
293
295
297 inline
298 const function_symbol& int2nat()
299 {
301 return int2nat;
302 }
303
307 inline
309 {
310 if (is_function_symbol(e))
311 {
312 return atermpp::down_cast<function_symbol>(e) == int2nat();
313 }
314 return false;
315 }
316
318
321 inline
322 application int2nat(const data_expression& arg0)
323 {
324 return sort_int::int2nat()(arg0);
325 }
326
329
331 inline
332 void make_int2nat(data_expression& result, const data_expression& arg0)
333 {
334 make_application(result, sort_int::int2nat(),arg0);
335 }
336
341 inline
343 {
344 return is_application(e) && is_int2nat_function_symbol(atermpp::down_cast<application>(e).head());
345 }
346
349 inline
351 {
353 return pos2int_name;
354 }
355
357
359 inline
360 const function_symbol& pos2int()
361 {
363 return pos2int;
364 }
365
369 inline
371 {
372 if (is_function_symbol(e))
373 {
374 return atermpp::down_cast<function_symbol>(e) == pos2int();
375 }
376 return false;
377 }
378
380
383 inline
384 application pos2int(const data_expression& arg0)
385 {
386 return sort_int::pos2int()(arg0);
387 }
388
391
393 inline
394 void make_pos2int(data_expression& result, const data_expression& arg0)
395 {
396 make_application(result, sort_int::pos2int(),arg0);
397 }
398
403 inline
405 {
406 return is_application(e) && is_pos2int_function_symbol(atermpp::down_cast<application>(e).head());
407 }
408
411 inline
413 {
415 return int2pos_name;
416 }
417
419
421 inline
422 const function_symbol& int2pos()
423 {
425 return int2pos;
426 }
427
431 inline
433 {
434 if (is_function_symbol(e))
435 {
436 return atermpp::down_cast<function_symbol>(e) == int2pos();
437 }
438 return false;
439 }
440
442
445 inline
446 application int2pos(const data_expression& arg0)
447 {
448 return sort_int::int2pos()(arg0);
449 }
450
453
455 inline
456 void make_int2pos(data_expression& result, const data_expression& arg0)
457 {
458 make_application(result, sort_int::int2pos(),arg0);
459 }
460
465 inline
467 {
468 return is_application(e) && is_int2pos_function_symbol(atermpp::down_cast<application>(e).head());
469 }
470
473 inline
475 {
477 return maximum_name;
478 }
479
480 // This function is not intended for public use and therefore not documented in Doxygen.
481 inline
482 function_symbol maximum(const sort_expression& s0, const sort_expression& s1)
483 {
484 sort_expression target_sort;
485 if (s0 == sort_pos::pos() && s1 == int_())
486 {
488 }
489 else if (s0 == int_() && s1 == sort_pos::pos())
490 {
492 }
493 else if (s0 == sort_nat::nat() && s1 == int_())
494 {
496 }
497 else if (s0 == int_() && s1 == sort_nat::nat())
498 {
500 }
501 else if (s0 == int_() && s1 == int_())
502 {
503 target_sort = int_();
504 }
505 else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
506 {
508 }
509 else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
510 {
512 }
513 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
514 {
516 }
517 else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
518 {
520 }
521 else
522 {
523 throw mcrl2::runtime_error("Cannot compute target sort for maximum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
524 }
525
527 return maximum;
528 }
529
533 inline
535 {
536 if (is_function_symbol(e))
537 {
538 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
539 return f.name() == maximum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == maximum(sort_pos::pos(), int_()) || f == maximum(int_(), sort_pos::pos()) || f == maximum(sort_nat::nat(), int_()) || f == maximum(int_(), sort_nat::nat()) || f == maximum(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()));
540 }
541 return false;
542 }
543
545
549 inline
550 application maximum(const data_expression& arg0, const data_expression& arg1)
551 {
552 return sort_int::maximum(arg0.sort(), arg1.sort())(arg0, arg1);
553 }
554
557
560 inline
561 void make_maximum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
562 {
563 make_application(result, sort_int::maximum(arg0.sort(), arg1.sort()),arg0, arg1);
564 }
565
570 inline
572 {
573 return is_application(e) && is_maximum_function_symbol(atermpp::down_cast<application>(e).head());
574 }
575
578 inline
580 {
582 return minimum_name;
583 }
584
585 // This function is not intended for public use and therefore not documented in Doxygen.
586 inline
587 function_symbol minimum(const sort_expression& s0, const sort_expression& s1)
588 {
589 sort_expression target_sort;
590 if (s0 == int_() && s1 == int_())
591 {
592 target_sort = int_();
593 }
594 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
595 {
597 }
598 else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
599 {
601 }
602 else
603 {
604 throw mcrl2::runtime_error("Cannot compute target sort for minimum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
605 }
606
608 return minimum;
609 }
610
614 inline
616 {
617 if (is_function_symbol(e))
618 {
619 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
620 return f.name() == minimum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minimum(int_(), int_()) || f == minimum(sort_nat::nat(), sort_nat::nat()) || f == minimum(sort_pos::pos(), sort_pos::pos()));
621 }
622 return false;
623 }
624
626
630 inline
631 application minimum(const data_expression& arg0, const data_expression& arg1)
632 {
633 return sort_int::minimum(arg0.sort(), arg1.sort())(arg0, arg1);
634 }
635
638
641 inline
642 void make_minimum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
643 {
644 make_application(result, sort_int::minimum(arg0.sort(), arg1.sort()),arg0, arg1);
645 }
646
651 inline
653 {
654 return is_application(e) && is_minimum_function_symbol(atermpp::down_cast<application>(e).head());
655 }
656
659 inline
661 {
663 return abs_name;
664 }
665
667
669 inline
670 const function_symbol& abs()
671 {
673 return abs;
674 }
675
679 inline
681 {
682 if (is_function_symbol(e))
683 {
684 return atermpp::down_cast<function_symbol>(e) == abs();
685 }
686 return false;
687 }
688
690
693 inline
694 application abs(const data_expression& arg0)
695 {
696 return sort_int::abs()(arg0);
697 }
698
701
703 inline
704 void make_abs(data_expression& result, const data_expression& arg0)
705 {
706 make_application(result, sort_int::abs(),arg0);
707 }
708
713 inline
715 {
716 return is_application(e) && is_abs_function_symbol(atermpp::down_cast<application>(e).head());
717 }
718
721 inline
723 {
725 return negate_name;
726 }
727
728 // This function is not intended for public use and therefore not documented in Doxygen.
729 inline
730 function_symbol negate(const sort_expression& s0)
731 {
732 sort_expression target_sort(int_());
734 return negate;
735 }
736
740 inline
742 {
743 if (is_function_symbol(e))
744 {
745 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
746 return f.name() == negate_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == negate(sort_pos::pos()) || f == negate(sort_nat::nat()) || f == negate(int_()));
747 }
748 return false;
749 }
750
752
755 inline
756 application negate(const data_expression& arg0)
757 {
758 return sort_int::negate(arg0.sort())(arg0);
759 }
760
763
765 inline
766 void make_negate(data_expression& result, const data_expression& arg0)
767 {
768 make_application(result, sort_int::negate(arg0.sort()),arg0);
769 }
770
775 inline
777 {
778 return is_application(e) && is_negate_function_symbol(atermpp::down_cast<application>(e).head());
779 }
780
783 inline
785 {
787 return succ_name;
788 }
789
790 // This function is not intended for public use and therefore not documented in Doxygen.
791 inline
792 function_symbol succ(const sort_expression& s0)
793 {
794 sort_expression target_sort;
795 if (s0 == int_())
796 {
797 target_sort = int_();
798 }
799 else if (s0 == sort_nat::nat())
800 {
802 }
803 else if (s0 == sort_pos::pos())
804 {
806 }
807 else
808 {
809 throw mcrl2::runtime_error("Cannot compute target sort for succ with domain sorts " + pp(s0) + ". ");
810 }
811
813 return succ;
814 }
815
819 inline
821 {
822 if (is_function_symbol(e))
823 {
824 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
825 return f.name() == succ_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == succ(int_()) || f == succ(sort_nat::nat()) || f == succ(sort_pos::pos()));
826 }
827 return false;
828 }
829
831
834 inline
835 application succ(const data_expression& arg0)
836 {
837 return sort_int::succ(arg0.sort())(arg0);
838 }
839
842
844 inline
845 void make_succ(data_expression& result, const data_expression& arg0)
846 {
847 make_application(result, sort_int::succ(arg0.sort()),arg0);
848 }
849
854 inline
856 {
857 return is_application(e) && is_succ_function_symbol(atermpp::down_cast<application>(e).head());
858 }
859
862 inline
864 {
866 return pred_name;
867 }
868
869 // This function is not intended for public use and therefore not documented in Doxygen.
870 inline
871 function_symbol pred(const sort_expression& s0)
872 {
873 sort_expression target_sort;
874 if (s0 == sort_nat::nat())
875 {
876 target_sort = int_();
877 }
878 else if (s0 == int_())
879 {
880 target_sort = int_();
881 }
882 else if (s0 == sort_pos::pos())
883 {
885 }
886 else
887 {
888 throw mcrl2::runtime_error("Cannot compute target sort for pred with domain sorts " + pp(s0) + ". ");
889 }
890
892 return pred;
893 }
894
898 inline
900 {
901 if (is_function_symbol(e))
902 {
903 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
904 return f.name() == pred_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == pred(sort_nat::nat()) || f == pred(int_()) || f == pred(sort_pos::pos()));
905 }
906 return false;
907 }
908
910
913 inline
914 application pred(const data_expression& arg0)
915 {
916 return sort_int::pred(arg0.sort())(arg0);
917 }
918
921
923 inline
924 void make_pred(data_expression& result, const data_expression& arg0)
925 {
926 make_application(result, sort_int::pred(arg0.sort()),arg0);
927 }
928
933 inline
935 {
936 return is_application(e) && is_pred_function_symbol(atermpp::down_cast<application>(e).head());
937 }
938
941 inline
943 {
945 return plus_name;
946 }
947
948 // This function is not intended for public use and therefore not documented in Doxygen.
949 inline
950 function_symbol plus(const sort_expression& s0, const sort_expression& s1)
951 {
952 sort_expression target_sort;
953 if (s0 == int_() && s1 == int_())
954 {
955 target_sort = int_();
956 }
957 else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
958 {
960 }
961 else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
962 {
964 }
965 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
966 {
968 }
969 else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
970 {
972 }
973 else
974 {
975 throw mcrl2::runtime_error("Cannot compute target sort for plus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
976 }
977
978 function_symbol plus(plus_name(), make_function_sort_(s0, s1, target_sort));
979 return plus;
980 }
981
985 inline
987 {
988 if (is_function_symbol(e))
989 {
990 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
991 return f.name() == plus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == plus(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()));
992 }
993 return false;
994 }
995
997
1001 inline
1002 application plus(const data_expression& arg0, const data_expression& arg1)
1003 {
1004 return sort_int::plus(arg0.sort(), arg1.sort())(arg0, arg1);
1005 }
1006
1009
1012 inline
1013 void make_plus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1014 {
1015 make_application(result, sort_int::plus(arg0.sort(), arg1.sort()),arg0, arg1);
1016 }
1017
1022 inline
1023 bool is_plus_application(const atermpp::aterm& e)
1024 {
1025 return is_application(e) && is_plus_function_symbol(atermpp::down_cast<application>(e).head());
1026 }
1027
1030 inline
1032 {
1034 return minus_name;
1035 }
1036
1037 // This function is not intended for public use and therefore not documented in Doxygen.
1038 inline
1039 function_symbol minus(const sort_expression& s0, const sort_expression& s1)
1040 {
1041 sort_expression target_sort(int_());
1042 function_symbol minus(minus_name(), make_function_sort_(s0, s1, target_sort));
1043 return minus;
1044 }
1045
1049 inline
1051 {
1052 if (is_function_symbol(e))
1053 {
1054 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1055 return f.name() == minus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minus(sort_pos::pos(), sort_pos::pos()) || f == minus(sort_nat::nat(), sort_nat::nat()) || f == minus(int_(), int_()));
1056 }
1057 return false;
1058 }
1059
1061
1065 inline
1066 application minus(const data_expression& arg0, const data_expression& arg1)
1067 {
1068 return sort_int::minus(arg0.sort(), arg1.sort())(arg0, arg1);
1069 }
1070
1073
1076 inline
1077 void make_minus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1078 {
1079 make_application(result, sort_int::minus(arg0.sort(), arg1.sort()),arg0, arg1);
1080 }
1081
1086 inline
1088 {
1089 return is_application(e) && is_minus_function_symbol(atermpp::down_cast<application>(e).head());
1090 }
1091
1094 inline
1096 {
1098 return times_name;
1099 }
1100
1101 // This function is not intended for public use and therefore not documented in Doxygen.
1102 inline
1103 function_symbol times(const sort_expression& s0, const sort_expression& s1)
1104 {
1105 sort_expression target_sort;
1106 if (s0 == int_() && s1 == int_())
1107 {
1108 target_sort = int_();
1109 }
1110 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1111 {
1113 }
1114 else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
1115 {
1117 }
1118 else
1119 {
1120 throw mcrl2::runtime_error("Cannot compute target sort for times with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1121 }
1122
1123 function_symbol times(times_name(), make_function_sort_(s0, s1, target_sort));
1124 return times;
1125 }
1126
1130 inline
1132 {
1133 if (is_function_symbol(e))
1134 {
1135 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1136 return f.name() == times_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == times(int_(), int_()) || f == times(sort_nat::nat(), sort_nat::nat()) || f == times(sort_pos::pos(), sort_pos::pos()));
1137 }
1138 return false;
1139 }
1140
1142
1146 inline
1147 application times(const data_expression& arg0, const data_expression& arg1)
1148 {
1149 return sort_int::times(arg0.sort(), arg1.sort())(arg0, arg1);
1150 }
1151
1154
1157 inline
1158 void make_times(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1159 {
1160 make_application(result, sort_int::times(arg0.sort(), arg1.sort()),arg0, arg1);
1161 }
1162
1167 inline
1169 {
1170 return is_application(e) && is_times_function_symbol(atermpp::down_cast<application>(e).head());
1171 }
1172
1175 inline
1177 {
1179 return div_name;
1180 }
1181
1182 // This function is not intended for public use and therefore not documented in Doxygen.
1183 inline
1184 function_symbol div(const sort_expression& s0, const sort_expression& s1)
1185 {
1186 sort_expression target_sort;
1187 if (s0 == int_() && s1 == sort_pos::pos())
1188 {
1189 target_sort = int_();
1190 }
1191 else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
1192 {
1194 }
1195 else
1196 {
1197 throw mcrl2::runtime_error("Cannot compute target sort for div with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1198 }
1199
1200 function_symbol div(div_name(), make_function_sort_(s0, s1, target_sort));
1201 return div;
1202 }
1203
1207 inline
1209 {
1210 if (is_function_symbol(e))
1211 {
1212 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1213 return f.name() == div_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == div(int_(), sort_pos::pos()) || f == div(sort_nat::nat(), sort_pos::pos()));
1214 }
1215 return false;
1216 }
1217
1219
1223 inline
1224 application div(const data_expression& arg0, const data_expression& arg1)
1225 {
1226 return sort_int::div(arg0.sort(), arg1.sort())(arg0, arg1);
1227 }
1228
1231
1234 inline
1235 void make_div(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1236 {
1237 make_application(result, sort_int::div(arg0.sort(), arg1.sort()),arg0, arg1);
1238 }
1239
1244 inline
1245 bool is_div_application(const atermpp::aterm& e)
1246 {
1247 return is_application(e) && is_div_function_symbol(atermpp::down_cast<application>(e).head());
1248 }
1249
1252 inline
1254 {
1256 return mod_name;
1257 }
1258
1259 // This function is not intended for public use and therefore not documented in Doxygen.
1260 inline
1261 function_symbol mod(const sort_expression& s0, const sort_expression& s1)
1262 {
1263 sort_expression target_sort(sort_nat::nat());
1264 function_symbol mod(mod_name(), make_function_sort_(s0, s1, target_sort));
1265 return mod;
1266 }
1267
1271 inline
1273 {
1274 if (is_function_symbol(e))
1275 {
1276 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1277 return f.name() == mod_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == mod(int_(), sort_pos::pos()) || f == mod(sort_nat::nat(), sort_pos::pos()));
1278 }
1279 return false;
1280 }
1281
1283
1287 inline
1288 application mod(const data_expression& arg0, const data_expression& arg1)
1289 {
1290 return sort_int::mod(arg0.sort(), arg1.sort())(arg0, arg1);
1291 }
1292
1295
1298 inline
1299 void make_mod(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1300 {
1301 make_application(result, sort_int::mod(arg0.sort(), arg1.sort()),arg0, arg1);
1302 }
1303
1308 inline
1309 bool is_mod_application(const atermpp::aterm& e)
1310 {
1311 return is_application(e) && is_mod_function_symbol(atermpp::down_cast<application>(e).head());
1312 }
1313
1316 inline
1318 {
1320 return exp_name;
1321 }
1322
1323 // This function is not intended for public use and therefore not documented in Doxygen.
1324 inline
1325 function_symbol exp(const sort_expression& s0, const sort_expression& s1)
1326 {
1327 sort_expression target_sort;
1328 if (s0 == int_() && s1 == sort_nat::nat())
1329 {
1330 target_sort = int_();
1331 }
1332 else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
1333 {
1335 }
1336 else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1337 {
1339 }
1340 else
1341 {
1342 throw mcrl2::runtime_error("Cannot compute target sort for exp with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1343 }
1344
1345 function_symbol exp(exp_name(), make_function_sort_(s0, s1, target_sort));
1346 return exp;
1347 }
1348
1352 inline
1354 {
1355 if (is_function_symbol(e))
1356 {
1357 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1358 return f.name() == exp_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == exp(int_(), sort_nat::nat()) || f == exp(sort_pos::pos(), sort_nat::nat()) || f == exp(sort_nat::nat(), sort_nat::nat()));
1359 }
1360 return false;
1361 }
1362
1364
1368 inline
1369 application exp(const data_expression& arg0, const data_expression& arg1)
1370 {
1371 return sort_int::exp(arg0.sort(), arg1.sort())(arg0, arg1);
1372 }
1373
1376
1379 inline
1380 void make_exp(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1381 {
1382 make_application(result, sort_int::exp(arg0.sort(), arg1.sort()),arg0, arg1);
1383 }
1384
1389 inline
1390 bool is_exp_application(const atermpp::aterm& e)
1391 {
1392 return is_application(e) && is_exp_function_symbol(atermpp::down_cast<application>(e).head());
1393 }
1396 inline
1398 {
1400 result.push_back(sort_int::nat2int());
1401 result.push_back(sort_int::int2nat());
1402 result.push_back(sort_int::pos2int());
1403 result.push_back(sort_int::int2pos());
1404 result.push_back(sort_int::maximum(sort_pos::pos(), int_()));
1405 result.push_back(sort_int::maximum(int_(), sort_pos::pos()));
1406 result.push_back(sort_int::maximum(sort_nat::nat(), int_()));
1407 result.push_back(sort_int::maximum(int_(), sort_nat::nat()));
1408 result.push_back(sort_int::maximum(int_(), int_()));
1409 result.push_back(sort_int::minimum(int_(), int_()));
1410 result.push_back(sort_int::abs());
1411 result.push_back(sort_int::negate(sort_pos::pos()));
1412 result.push_back(sort_int::negate(sort_nat::nat()));
1413 result.push_back(sort_int::negate(int_()));
1414 result.push_back(sort_int::succ(int_()));
1415 result.push_back(sort_int::pred(sort_nat::nat()));
1416 result.push_back(sort_int::pred(int_()));
1417 result.push_back(sort_int::plus(int_(), int_()));
1418 result.push_back(sort_int::minus(sort_pos::pos(), sort_pos::pos()));
1419 result.push_back(sort_int::minus(sort_nat::nat(), sort_nat::nat()));
1420 result.push_back(sort_int::minus(int_(), int_()));
1421 result.push_back(sort_int::times(int_(), int_()));
1422 result.push_back(sort_int::div(int_(), sort_pos::pos()));
1423 result.push_back(sort_int::mod(int_(), sort_pos::pos()));
1424 result.push_back(sort_int::exp(int_(), sort_nat::nat()));
1425 return result;
1426 }
1427
1430 inline
1432 {
1434 for(const function_symbol& f: int_generate_constructors_code())
1435 {
1436 result.push_back(f);
1437 }
1438 return result;
1439 }
1440
1443 inline
1445 {
1447 result.push_back(sort_int::nat2int());
1448 result.push_back(sort_int::int2nat());
1449 result.push_back(sort_int::pos2int());
1450 result.push_back(sort_int::int2pos());
1451 result.push_back(sort_int::maximum(sort_pos::pos(), int_()));
1452 result.push_back(sort_int::maximum(int_(), sort_pos::pos()));
1453 result.push_back(sort_int::maximum(sort_nat::nat(), int_()));
1454 result.push_back(sort_int::maximum(int_(), sort_nat::nat()));
1455 result.push_back(sort_int::maximum(int_(), int_()));
1456 result.push_back(sort_int::minimum(int_(), int_()));
1457 result.push_back(sort_int::abs());
1458 result.push_back(sort_int::negate(sort_pos::pos()));
1459 result.push_back(sort_int::negate(sort_nat::nat()));
1460 result.push_back(sort_int::negate(int_()));
1461 result.push_back(sort_int::succ(int_()));
1462 result.push_back(sort_int::pred(sort_nat::nat()));
1463 result.push_back(sort_int::pred(int_()));
1464 result.push_back(sort_int::plus(int_(), int_()));
1465 result.push_back(sort_int::minus(sort_pos::pos(), sort_pos::pos()));
1466 result.push_back(sort_int::minus(sort_nat::nat(), sort_nat::nat()));
1467 result.push_back(sort_int::minus(int_(), int_()));
1468 result.push_back(sort_int::times(int_(), int_()));
1469 result.push_back(sort_int::div(int_(), sort_pos::pos()));
1470 result.push_back(sort_int::mod(int_(), sort_pos::pos()));
1471 result.push_back(sort_int::exp(int_(), sort_nat::nat()));
1472 return result;
1473 }
1474
1475
1476 // 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
1477 typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
1480 inline
1482 {
1483 implementation_map result;
1484 return result;
1485 }
1491 inline
1492 const data_expression& arg(const data_expression& e)
1493 {
1495 return atermpp::down_cast<application>(e)[0];
1496 }
1497
1503 inline
1504 const data_expression& left(const data_expression& e)
1505 {
1507 return atermpp::down_cast<application>(e)[0];
1508 }
1509
1515 inline
1516 const data_expression& right(const data_expression& e)
1517 {
1519 return atermpp::down_cast<application>(e)[1];
1520 }
1521
1524 inline
1526 {
1527 variable vb("b",sort_bool::bool_());
1528 variable vn("n",sort_nat::nat());
1529 variable vm("m",sort_nat::nat());
1530 variable vp("p",sort_pos::pos());
1531 variable vq("q",sort_pos::pos());
1532 variable vx("x",int_());
1533 variable vy("y",int_());
1534
1535 data_equation_vector result;
1536 result.push_back(data_equation(variable_list({vm, vn}), equal_to(cint(vm), cint(vn)), equal_to(vm, vn)));
1537 result.push_back(data_equation(variable_list({vn, vp}), equal_to(cint(vn), cneg(vp)), sort_bool::false_()));
1538 result.push_back(data_equation(variable_list({vn, vp}), equal_to(cneg(vp), cint(vn)), sort_bool::false_()));
1539 result.push_back(data_equation(variable_list({vp, vq}), equal_to(cneg(vp), cneg(vq)), equal_to(vp, vq)));
1540 result.push_back(data_equation(variable_list({vm, vn}), less(cint(vm), cint(vn)), less(vm, vn)));
1541 result.push_back(data_equation(variable_list({vn, vp}), less(cint(vn), cneg(vp)), sort_bool::false_()));
1542 result.push_back(data_equation(variable_list({vn, vp}), less(cneg(vp), cint(vn)), sort_bool::true_()));
1543 result.push_back(data_equation(variable_list({vp, vq}), less(cneg(vp), cneg(vq)), less(vq, vp)));
1544 result.push_back(data_equation(variable_list({vm, vn}), less_equal(cint(vm), cint(vn)), less_equal(vm, vn)));
1545 result.push_back(data_equation(variable_list({vn, vp}), less_equal(cint(vn), cneg(vp)), sort_bool::false_()));
1546 result.push_back(data_equation(variable_list({vn, vp}), less_equal(cneg(vp), cint(vn)), sort_bool::true_()));
1547 result.push_back(data_equation(variable_list({vp, vq}), less_equal(cneg(vp), cneg(vq)), less_equal(vq, vp)));
1548 result.push_back(data_equation(variable_list({vn}), nat2int(vn), cint(vn)));
1549 result.push_back(data_equation(variable_list({vn}), int2nat(cint(vn)), vn));
1550 result.push_back(data_equation(variable_list({vp}), pos2int(vp), cint(sort_nat::pos2nat(vp))));
1551 result.push_back(data_equation(variable_list({vn}), int2pos(cint(vn)), sort_nat::nat2pos(vn)));
1552 result.push_back(data_equation(variable_list({vn, vp}), maximum(vp, cint(vn)), maximum(vp, vn)));
1553 result.push_back(data_equation(variable_list({vp, vq}), maximum(vp, cneg(vq)), vp));
1554 result.push_back(data_equation(variable_list({vn, vp}), maximum(cint(vn), vp), maximum(vn, vp)));
1555 result.push_back(data_equation(variable_list({vp, vq}), maximum(cneg(vq), vp), vp));
1556 result.push_back(data_equation(variable_list({vm, vn}), maximum(vm, cint(vn)), if_(less_equal(vm, vn), vn, vm)));
1557 result.push_back(data_equation(variable_list({vn, vp}), maximum(vn, cneg(vp)), vn));
1558 result.push_back(data_equation(variable_list({vm, vn}), maximum(cint(vm), vn), if_(less_equal(vm, vn), vn, vm)));
1559 result.push_back(data_equation(variable_list({vn, vp}), maximum(cneg(vp), vn), vn));
1560 result.push_back(data_equation(variable_list({vx, vy}), maximum(vx, vy), if_(less_equal(vx, vy), vy, vx)));
1561 result.push_back(data_equation(variable_list({vx, vy}), minimum(vx, vy), if_(less_equal(vx, vy), vx, vy)));
1562 result.push_back(data_equation(variable_list({vn}), abs(cint(vn)), vn));
1563 result.push_back(data_equation(variable_list({vp}), abs(cneg(vp)), sort_nat::pos2nat(vp)));
1564 result.push_back(data_equation(variable_list({vp}), negate(vp), cneg(vp)));
1565 result.push_back(data_equation(variable_list(), negate(sort_nat::c0()), cint(sort_nat::c0())));
1567 result.push_back(data_equation(variable_list({vn}), negate(cint(vn)), negate(vn)));
1568 result.push_back(data_equation(variable_list({vp}), negate(cneg(vp)), cint(sort_nat::pos2nat(vp))));
1569 result.push_back(data_equation(variable_list({vn}), succ(cint(vn)), cint(sort_nat::succ_nat(vn))));
1570 result.push_back(data_equation(variable_list({vp}), succ(cneg(vp)), negate(pred(vp))));
1572 result.push_back(data_equation(variable_list({vn}), pred(cint(vn)), pred(vn)));
1573 result.push_back(data_equation(variable_list({vp}), pred(cneg(vp)), cneg(succ(vp))));
1574 result.push_back(data_equation(variable_list({vm, vn}), plus(cint(vm), cint(vn)), cint(plus(vm, vn))));
1575 result.push_back(data_equation(variable_list({vn, vp}), plus(cint(vn), cneg(vp)), minus(vn, sort_nat::pos2nat(vp))));
1576 result.push_back(data_equation(variable_list({vn, vp}), plus(cneg(vp), cint(vn)), minus(vn, sort_nat::pos2nat(vp))));
1577 result.push_back(data_equation(variable_list({vp, vq}), plus(cneg(vp), cneg(vq)), cneg(plus(vp, vq))));
1578 result.push_back(data_equation(variable_list({vp, vq}), less_equal(vq, vp), minus(vp, vq), cint(sort_nat::monus(sort_nat::pos2nat(vp), sort_nat::pos2nat(vq)))));
1579 result.push_back(data_equation(variable_list({vp, vq}), less(vp, vq), minus(vp, vq), negate(sort_nat::monus(sort_nat::pos2nat(vq), sort_nat::pos2nat(vp)))));
1580 result.push_back(data_equation(variable_list({vm, vn}), less_equal(vn, vm), minus(vm, vn), cint(sort_nat::monus(vm, vn))));
1581 result.push_back(data_equation(variable_list({vm, vn}), less(vm, vn), minus(vm, vn), negate(sort_nat::monus(vn, vm))));
1582 result.push_back(data_equation(variable_list({vx, vy}), minus(vx, vy), plus(vx, negate(vy))));
1583 result.push_back(data_equation(variable_list({vm, vn}), times(cint(vm), cint(vn)), cint(times(vm, vn))));
1584 result.push_back(data_equation(variable_list({vn, vp}), times(cint(vn), cneg(vp)), negate(times(sort_nat::pos2nat(vp), vn))));
1585 result.push_back(data_equation(variable_list({vn, vp}), times(cneg(vp), cint(vn)), negate(times(sort_nat::pos2nat(vp), vn))));
1586 result.push_back(data_equation(variable_list({vp, vq}), times(cneg(vp), cneg(vq)), cint(sort_nat::pos2nat(times(vp, vq)))));
1587 result.push_back(data_equation(variable_list({vn, vp}), div(cint(vn), vp), cint(div(vn, vp))));
1588 result.push_back(data_equation(variable_list({vp, vq}), div(cneg(vp), vq), cneg(succ(div(pred(vp), vq)))));
1589 result.push_back(data_equation(variable_list({vn, vp}), mod(cint(vn), vp), mod(vn, vp)));
1590 result.push_back(data_equation(variable_list({vp, vq}), mod(cneg(vp), vq), int2nat(minus(vq, succ(mod(pred(vp), vq))))));
1591 result.push_back(data_equation(variable_list({vm, vn}), exp(cint(vm), vn), cint(exp(vm, vn))));
1592 result.push_back(data_equation(variable_list({vn, vp}), exp(cneg(vp), vn), if_(sort_nat::is_odd(vn), cneg(exp(vp, vn)), cint(sort_nat::pos2nat(exp(vp, vn))))));
1593 return result;
1594 }
1595
1596 } // namespace sort_int_
1597
1598 } // namespace data
1599
1600} // namespace mcrl2
1601
1602#endif // MCRL2_DATA_INT64_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 basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition int1.h:652
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition int1.h:1516
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition int1.h:642
const core::identifier_string & cint_name()
Generate identifier @cInt.
Definition int1.h:70
bool is_minus_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition int1.h:1050
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition int1.h:571
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition int1.h:820
const core::identifier_string & abs_name()
Generate identifier abs.
Definition int1.h:660
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition int1.h:615
bool is_int2pos_application(const atermpp::aterm &e)
Recogniser for application of Int2Pos.
Definition int1.h:466
const core::identifier_string & pred_name()
Generate identifier pred.
Definition int1.h:863
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition int1.h:1353
bool is_int2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Pos.
Definition int1.h:432
const function_symbol & pos2int()
Constructor for function symbol Pos2Int.
Definition int1.h:360
const core::identifier_string & nat2int_name()
Generate identifier Nat2Int.
Definition int1.h:226
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition int1.h:1492
void make_minus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition int1.h:1077
bool is_cneg_function_symbol(const atermpp::aterm &e)
Recogniser for function @cNeg.
Definition int1.h:152
const core::identifier_string & int2pos_name()
Generate identifier Int2Pos.
Definition int1.h:412
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:482
void make_cneg(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cNeg.
Definition int1.h:176
function_symbol pred(const sort_expression &s0)
Definition int1.h:871
const core::identifier_string & cneg_name()
Generate identifier @cNeg.
Definition int1.h:132
const core::identifier_string & exp_name()
Generate identifier exp.
Definition int1.h:1317
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition int1.h:1380
const core::identifier_string & minimum_name()
Generate identifier min.
Definition int1.h:579
bool is_mod_application(const atermpp::aterm &e)
Recogniser for application of mod.
Definition int1.h:1309
const core::identifier_string & int_name()
Definition int1.h:38
bool is_mod_function_symbol(const atermpp::aterm &e)
Recogniser for function mod.
Definition int1.h:1272
function_symbol_vector int_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for int_.
Definition int1.h:1444
const core::identifier_string & pos2int_name()
Generate identifier Pos2Int.
Definition int1.h:350
const function_symbol & int2nat()
Constructor for function symbol Int2Nat.
Definition int1.h:298
bool is_int(const sort_expression &e)
Recogniser for sort expression Int.
Definition int1.h:57
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1039
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition int1.h:934
const function_symbol & nat2int()
Constructor for function symbol Nat2Int.
Definition int1.h:236
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition int1.h:1168
const core::identifier_string & maximum_name()
Generate identifier max.
Definition int1.h:474
bool is_int2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Nat.
Definition int1.h:308
bool is_cneg_application(const atermpp::aterm &e)
Recogniser for application of @cNeg.
Definition int1.h:186
const core::identifier_string & succ_name()
Generate identifier succ.
Definition int1.h:784
const function_symbol & cneg()
Constructor for function symbol @cNeg.
Definition int1.h:142
void make_pos2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Int.
Definition int1.h:394
const function_symbol & abs()
Constructor for function symbol abs.
Definition int1.h:670
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1325
bool is_cint_application(const atermpp::aterm &e)
Recogniser for application of @cInt.
Definition int1.h:124
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition int1.h:1131
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition int1.h:1023
const core::identifier_string & mod_name()
Generate identifier mod.
Definition int1.h:1253
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition int1.h:1013
data_equation_vector int_generate_equations_code()
Give all system defined equations for int_.
Definition int1.h:1525
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:950
const function_symbol & int2pos()
Constructor for function symbol Int2Pos.
Definition int1.h:422
const core::identifier_string & plus_name()
Generate identifier +.
Definition int1.h:942
function_symbol_vector int_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for int_.
Definition int1.h:1431
void make_div(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol div.
Definition int1.h:1235
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition int1.h:776
function_symbol negate(const sort_expression &s0)
Definition int1.h:730
bool is_div_application(const atermpp::aterm &e)
Recogniser for application of div.
Definition int1.h:1245
void make_mod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol mod.
Definition int1.h:1299
bool is_pos2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Int.
Definition int1.h:370
function_symbol_vector int_generate_constructors_code()
Give all system defined constructors for int_.
Definition int1.h:193
bool is_abs_application(const atermpp::aterm &e)
Recogniser for application of abs.
Definition int1.h:714
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition int1.h:561
function_symbol_vector int_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for int_.
Definition int1.h:204
function_symbol succ(const sort_expression &s0)
Definition int1.h:792
void make_negate(data_expression &result, const data_expression &arg0)
Make an application of function symbol -.
Definition int1.h:766
const core::identifier_string & negate_name()
Generate identifier -.
Definition int1.h:722
bool is_cint_function_symbol(const atermpp::aterm &e)
Recogniser for function @cInt.
Definition int1.h:90
void make_abs(data_expression &result, const data_expression &arg0)
Make an application of function symbol abs.
Definition int1.h:704
function_symbol_vector int_generate_functions_code()
Give all system defined mappings for int_.
Definition int1.h:1397
implementation_map int_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition int1.h:217
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition int1.h:1390
void make_nat2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Int.
Definition int1.h:270
const function_symbol & cint()
Constructor for function symbol @cInt.
Definition int1.h:80
implementation_map int_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for int_.
Definition int1.h:1481
bool is_nat2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Int.
Definition int1.h:246
bool is_int2nat_application(const atermpp::aterm &e)
Recogniser for application of Int2Nat.
Definition int1.h:342
const core::identifier_string & minus_name()
Generate identifier -.
Definition int1.h:1031
function_symbol mod(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1261
const core::identifier_string & int2nat_name()
Generate identifier Int2Nat.
Definition int1.h:288
const core::identifier_string & div_name()
Generate identifier div.
Definition int1.h:1176
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition int1.h:534
bool is_div_function_symbol(const atermpp::aterm &e)
Recogniser for function div.
Definition int1.h:1208
bool is_negate_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition int1.h:741
void make_int2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Pos.
Definition int1.h:456
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1103
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition int1.h:986
bool is_nat2int_application(const atermpp::aterm &e)
Recogniser for application of Nat2Int.
Definition int1.h:280
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition int1.h:1087
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition int1.h:1158
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:587
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition int1.h:899
function_symbol div(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1184
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition int1.h:845
bool is_pos2int_application(const atermpp::aterm &e)
Recogniser for application of Pos2Int.
Definition int1.h:404
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition int1.h:924
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition int1.h:213
void make_cint(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cInt.
Definition int1.h:114
void make_int2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Nat.
Definition int1.h:332
bool is_abs_function_symbol(const atermpp::aterm &e)
Recogniser for function abs.
Definition int1.h:680
const core::identifier_string & times_name()
Generate identifier *.
Definition int1.h:1095
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition int1.h:1504
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition int1.h:855
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 & one_word()
Constructor for function symbol @one_word.
const function_symbol & zero_word()
Constructor for function symbol @zero_word.
const function_symbol & monus()
Constructor for function symbol @monus.
Definition nat1.h:1331
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 & natpred()
Constructor for function symbol @natpred.
Definition nat64.h:1824
const function_symbol & is_odd()
Constructor for function symbol @is_odd.
Definition nat64.h:1886
const function_symbol & succ_nat()
Constructor for function symbol @succ_nat.
Definition nat64.h:141
const function_symbol & nat2pos()
Constructor for function symbol Nat2Pos.
Definition nat1.h:362
const function_symbol & most_significant_digit_nat()
Constructor for function symbol @most_significant_digitNat.
Definition nat64.h:301
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 & most_significant_digit()
Constructor for function symbol @most_significant_digit.
Definition pos64.h:205
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
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.