mCRL2
Loading...
Searching...
No Matches
set1.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_SET1_H
16#define MCRL2_DATA_SET1_H
17
18#include "functional" // std::function
25#include "mcrl2/data/standard.h"
26#include "mcrl2/data/forall.h"
28#include "mcrl2/data/bool.h"
29#include "mcrl2/data/fset1.h"
30
31namespace mcrl2 {
32
33 namespace data {
34
36 namespace sort_set {
37
41 inline
43 {
45 return set_;
46 }
47
52 inline
53 bool is_set(const sort_expression& e)
54 {
55 if (is_container_sort(e))
56 {
58 }
59 return false;
60 }
61
62
65 inline
67 {
69 return constructor_name;
70 }
71
75 inline
77 {
79 return constructor;
80 }
81
85 inline
87 {
88 if (is_function_symbol(e))
89 {
90 return atermpp::down_cast<function_symbol>(e).name() == constructor_name();
91 }
92 return false;
93 }
94
100 inline
102 {
103 return sort_set::constructor(s)(arg0, arg1);
104 }
105
111 inline
113 {
115 }
116
121 inline
123 {
124 return is_application(e) && is_constructor_function_symbol(atermpp::down_cast<application>(e).head());
125 }
129 inline
131 {
133 result.push_back(sort_set::constructor(s));
134
135 return result;
136 }
140 inline
142 {
144 result.push_back(sort_set::constructor(s));
145
146 return result;
147 }
148 // 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
149 typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
153 inline
155 {
156 implementation_map result;
157 static_cast< void >(s); // suppress unused variable warnings
158 return result;
159 }
160
163 inline
165 {
167 return set_fset_name;
168 }
169
173 inline
175 {
177 return set_fset;
178 }
179
183 inline
185 {
186 if (is_function_symbol(e))
187 {
188 return atermpp::down_cast<function_symbol>(e).name() == set_fset_name();
189 }
190 return false;
191 }
192
197 inline
199 {
200 return sort_set::set_fset(s)(arg0);
201 }
202
207 inline
209 {
210 make_application(result, sort_set::set_fset(s),arg0);
211 }
212
217 inline
219 {
220 return is_application(e) && is_set_fset_function_symbol(atermpp::down_cast<application>(e).head());
221 }
222
225 inline
227 {
230 }
231
235 inline
237 {
239 return set_comprehension;
240 }
241
245 inline
247 {
248 if (is_function_symbol(e))
249 {
250 return atermpp::down_cast<function_symbol>(e).name() == set_comprehension_name();
251 }
252 return false;
253 }
254
259 inline
261 {
262 return sort_set::set_comprehension(s)(arg0);
263 }
264
269 inline
271 {
273 }
274
279 inline
281 {
282 return is_application(e) && is_set_comprehension_function_symbol(atermpp::down_cast<application>(e).head());
283 }
284
287 inline
289 {
291 return in_name;
292 }
293
294 // This function is not intended for public use and therefore not documented in Doxygen.
295 inline
297 {
298 sort_expression target_sort(sort_bool::bool_());
299 function_symbol in(in_name(), make_function_sort_(s0, s1, target_sort));
300 return in;
301 }
302
306 inline
308 {
309 if (is_function_symbol(e))
310 {
311 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
312 return f.name() == in_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
313 }
314 return false;
315 }
316
322 inline
324 {
325 return sort_set::in(s, arg0.sort(), arg1.sort())(arg0, arg1);
326 }
327
333 inline
334 void make_in(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
335 {
336 make_application(result, sort_set::in(s, arg0.sort(), arg1.sort()),arg0, arg1);
337 }
338
343 inline
345 {
346 return is_application(e) && is_in_function_symbol(atermpp::down_cast<application>(e).head());
347 }
348
351 inline
353 {
355 return complement_name;
356 }
357
361 inline
363 {
365 return complement;
366 }
367
371 inline
373 {
374 if (is_function_symbol(e))
375 {
376 return atermpp::down_cast<function_symbol>(e).name() == complement_name();
377 }
378 return false;
379 }
380
385 inline
387 {
388 return sort_set::complement(s)(arg0);
389 }
390
395 inline
397 {
398 make_application(result, sort_set::complement(s),arg0);
399 }
400
405 inline
407 {
408 return is_application(e) && is_complement_function_symbol(atermpp::down_cast<application>(e).head());
409 }
410
413 inline
415 {
417 return union_name;
418 }
419
420 // This function is not intended for public use and therefore not documented in Doxygen.
421 inline
423 {
424 sort_expression target_sort;
425 if (s0 == set_(s) && s1 == set_(s))
426 {
427 target_sort = set_(s);
428 }
429 else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
430 {
431 target_sort = sort_fset::fset(s);
432 }
433 else
434 {
435 throw mcrl2::runtime_error("Cannot compute target sort for union_ with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
436 }
437
438 function_symbol union_(union_name(), make_function_sort_(s0, s1, target_sort));
439 return union_;
440 }
441
445 inline
447 {
448 if (is_function_symbol(e))
449 {
450 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
451 return f.name() == union_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
452 }
453 return false;
454 }
455
461 inline
463 {
464 return sort_set::union_(s, arg0.sort(), arg1.sort())(arg0, arg1);
465 }
466
472 inline
474 {
475 make_application(result, sort_set::union_(s, arg0.sort(), arg1.sort()),arg0, arg1);
476 }
477
482 inline
484 {
485 return is_application(e) && is_union_function_symbol(atermpp::down_cast<application>(e).head());
486 }
487
490 inline
492 {
494 return intersection_name;
495 }
496
497 // This function is not intended for public use and therefore not documented in Doxygen.
498 inline
500 {
501 sort_expression target_sort;
502 if (s0 == set_(s) && s1 == set_(s))
503 {
504 target_sort = set_(s);
505 }
506 else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
507 {
508 target_sort = sort_fset::fset(s);
509 }
510 else
511 {
512 throw mcrl2::runtime_error("Cannot compute target sort for intersection with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
513 }
514
516 return intersection;
517 }
518
522 inline
524 {
525 if (is_function_symbol(e))
526 {
527 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
528 return f.name() == intersection_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
529 }
530 return false;
531 }
532
538 inline
540 {
541 return sort_set::intersection(s, arg0.sort(), arg1.sort())(arg0, arg1);
542 }
543
549 inline
551 {
552 make_application(result, sort_set::intersection(s, arg0.sort(), arg1.sort()),arg0, arg1);
553 }
554
559 inline
561 {
562 return is_application(e) && is_intersection_function_symbol(atermpp::down_cast<application>(e).head());
563 }
564
567 inline
569 {
571 return difference_name;
572 }
573
574 // This function is not intended for public use and therefore not documented in Doxygen.
575 inline
577 {
578 sort_expression target_sort;
579 if (s0 == set_(s) && s1 == set_(s))
580 {
581 target_sort = set_(s);
582 }
583 else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
584 {
585 target_sort = sort_fset::fset(s);
586 }
587 else
588 {
589 throw mcrl2::runtime_error("Cannot compute target sort for difference with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
590 }
591
593 return difference;
594 }
595
599 inline
601 {
602 if (is_function_symbol(e))
603 {
604 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
605 return f.name() == difference_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
606 }
607 return false;
608 }
609
615 inline
617 {
618 return sort_set::difference(s, arg0.sort(), arg1.sort())(arg0, arg1);
619 }
620
626 inline
628 {
629 make_application(result, sort_set::difference(s, arg0.sort(), arg1.sort()),arg0, arg1);
630 }
631
636 inline
638 {
639 return is_application(e) && is_difference_function_symbol(atermpp::down_cast<application>(e).head());
640 }
641
644 inline
646 {
648 return false_function_name;
649 }
650
654 inline
656 {
658 return false_function;
659 }
660
664 inline
666 {
667 if (is_function_symbol(e))
668 {
669 return atermpp::down_cast<function_symbol>(e).name() == false_function_name();
670 }
671 return false;
672 }
673
678 inline
680 {
681 return sort_set::false_function(s)(arg0);
682 }
683
688 inline
690 {
692 }
693
698 inline
700 {
701 return is_application(e) && is_false_function_function_symbol(atermpp::down_cast<application>(e).head());
702 }
703
706 inline
708 {
710 return true_function_name;
711 }
712
716 inline
718 {
720 return true_function;
721 }
722
726 inline
728 {
729 if (is_function_symbol(e))
730 {
731 return atermpp::down_cast<function_symbol>(e).name() == true_function_name();
732 }
733 return false;
734 }
735
740 inline
742 {
743 return sort_set::true_function(s)(arg0);
744 }
745
750 inline
752 {
754 }
755
760 inline
762 {
763 return is_application(e) && is_true_function_function_symbol(atermpp::down_cast<application>(e).head());
764 }
765
768 inline
770 {
772 return not_function_name;
773 }
774
778 inline
780 {
782 return not_function;
783 }
784
788 inline
790 {
791 if (is_function_symbol(e))
792 {
793 return atermpp::down_cast<function_symbol>(e).name() == not_function_name();
794 }
795 return false;
796 }
797
802 inline
804 {
805 return sort_set::not_function(s)(arg0);
806 }
807
812 inline
814 {
816 }
817
822 inline
824 {
825 return is_application(e) && is_not_function_function_symbol(atermpp::down_cast<application>(e).head());
826 }
827
830 inline
832 {
834 return and_function_name;
835 }
836
840 inline
842 {
844 return and_function;
845 }
846
850 inline
852 {
853 if (is_function_symbol(e))
854 {
855 return atermpp::down_cast<function_symbol>(e).name() == and_function_name();
856 }
857 return false;
858 }
859
865 inline
867 {
868 return sort_set::and_function(s)(arg0, arg1);
869 }
870
876 inline
878 {
880 }
881
886 inline
888 {
889 return is_application(e) && is_and_function_function_symbol(atermpp::down_cast<application>(e).head());
890 }
891
894 inline
896 {
898 return or_function_name;
899 }
900
904 inline
906 {
908 return or_function;
909 }
910
914 inline
916 {
917 if (is_function_symbol(e))
918 {
919 return atermpp::down_cast<function_symbol>(e).name() == or_function_name();
920 }
921 return false;
922 }
923
929 inline
931 {
932 return sort_set::or_function(s)(arg0, arg1);
933 }
934
940 inline
942 {
944 }
945
950 inline
952 {
953 return is_application(e) && is_or_function_function_symbol(atermpp::down_cast<application>(e).head());
954 }
955
958 inline
960 {
962 return fset_union_name;
963 }
964
968 inline
970 {
972 return fset_union;
973 }
974
978 inline
980 {
981 if (is_function_symbol(e))
982 {
983 return atermpp::down_cast<function_symbol>(e).name() == fset_union_name();
984 }
985 return false;
986 }
987
995 inline
997 {
998 return sort_set::fset_union(s)(arg0, arg1, arg2, arg3);
999 }
1000
1008 inline
1010 {
1012 }
1013
1018 inline
1020 {
1021 return is_application(e) && is_fset_union_function_symbol(atermpp::down_cast<application>(e).head());
1022 }
1023
1026 inline
1028 {
1031 }
1032
1036 inline
1038 {
1040 return fset_intersection;
1041 }
1042
1046 inline
1048 {
1049 if (is_function_symbol(e))
1050 {
1051 return atermpp::down_cast<function_symbol>(e).name() == fset_intersection_name();
1052 }
1053 return false;
1054 }
1055
1063 inline
1065 {
1066 return sort_set::fset_intersection(s)(arg0, arg1, arg2, arg3);
1067 }
1068
1076 inline
1078 {
1080 }
1081
1086 inline
1088 {
1089 return is_application(e) && is_fset_intersection_function_symbol(atermpp::down_cast<application>(e).head());
1090 }
1094 inline
1096 {
1098 result.push_back(sort_set::set_fset(s));
1099 result.push_back(sort_set::set_comprehension(s));
1100 result.push_back(sort_set::in(s, s, set_(s)));
1101 result.push_back(sort_set::complement(s));
1102 result.push_back(sort_set::union_(s, set_(s), set_(s)));
1103 result.push_back(sort_set::intersection(s, set_(s), set_(s)));
1104 result.push_back(sort_set::difference(s, set_(s), set_(s)));
1105 result.push_back(sort_set::false_function(s));
1106 result.push_back(sort_set::true_function(s));
1107 result.push_back(sort_set::not_function(s));
1108 result.push_back(sort_set::and_function(s));
1109 result.push_back(sort_set::or_function(s));
1110 result.push_back(sort_set::fset_union(s));
1111 result.push_back(sort_set::fset_intersection(s));
1112 return result;
1113 }
1114
1118 inline
1120 {
1123 {
1124 result.push_back(f);
1125 }
1126 return result;
1127 }
1128
1132 inline
1134 {
1136 result.push_back(sort_set::set_fset(s));
1137 result.push_back(sort_set::set_comprehension(s));
1138 result.push_back(sort_set::in(s, s, set_(s)));
1139 result.push_back(sort_set::complement(s));
1140 result.push_back(sort_set::union_(s, set_(s), set_(s)));
1141 result.push_back(sort_set::intersection(s, set_(s), set_(s)));
1142 result.push_back(sort_set::difference(s, set_(s), set_(s)));
1143 result.push_back(sort_set::false_function(s));
1144 result.push_back(sort_set::true_function(s));
1145 result.push_back(sort_set::not_function(s));
1146 result.push_back(sort_set::and_function(s));
1147 result.push_back(sort_set::or_function(s));
1148 result.push_back(sort_set::fset_union(s));
1149 result.push_back(sort_set::fset_intersection(s));
1150 return result;
1151 }
1152
1153
1154 // 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
1155 typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
1159 inline
1161 {
1162 implementation_map result;
1163 static_cast< void >(s); // suppress unused variable warnings
1164 return result;
1165 }
1171 inline
1173 {
1175 return atermpp::down_cast<application>(e)[0];
1176 }
1177
1183 inline
1185 {
1187 return atermpp::down_cast<application>(e)[1];
1188 }
1189
1195 inline
1197 {
1199 return atermpp::down_cast<application>(e)[0];
1200 }
1201
1207 inline
1209 {
1211 return atermpp::down_cast<application>(e)[0];
1212 }
1213
1219 inline
1221 {
1223 return atermpp::down_cast<application>(e)[1];
1224 }
1225
1231 inline
1233 {
1235 return atermpp::down_cast<application>(e)[2];
1236 }
1237
1243 inline
1245 {
1247 return atermpp::down_cast<application>(e)[3];
1248 }
1249
1253 inline
1255 {
1256 variable vd("d",s);
1257 variable ve("e",s);
1258 variable vs("s",sort_fset::fset(s));
1259 variable vt("t",sort_fset::fset(s));
1262 variable vx("x",set_(s));
1263 variable vy("y",set_(s));
1264 variable vc("c",s);
1265
1266 data_equation_vector result;
1267 result.push_back(data_equation(variable_list({vs}), set_fset(s, vs), constructor(s, false_function(s), vs)));
1268 result.push_back(data_equation(variable_list({vf}), sort_set::set_comprehension(s, vf), constructor(s, vf, sort_fset::empty(s))));
1269 result.push_back(data_equation(variable_list({ve, vf, vs}), in(s, ve, constructor(s, vf, vs)), not_equal_to(vf(ve), in(s, ve, vs))));
1270 result.push_back(data_equation(variable_list({vf, vg, vs, vt}), equal_to(constructor(s, vf, vs), constructor(s, vg, vt)), forall(variable_list({vc}), equal_to(equal_to(vf(vc), vg(vc)), equal_to(in(s, vc, vs), in(s, vc, vt))))));
1271 result.push_back(data_equation(variable_list({vx, vy}), less(vx, vy), sort_bool::and_(less_equal(vx, vy), not_equal_to(vx, vy))));
1272 result.push_back(data_equation(variable_list({vx, vy}), less_equal(vx, vy), equal_to(intersection(s, vx, vy), vx)));
1273 result.push_back(data_equation(variable_list({vf, vs}), complement(s, constructor(s, vf, vs)), constructor(s, not_function(s, vf), vs)));
1274 result.push_back(data_equation(variable_list({vx}), union_(s, vx, vx), vx));
1275 result.push_back(data_equation(variable_list({vx, vy}), union_(s, vx, union_(s, vx, vy)), union_(s, vx, vy)));
1276 result.push_back(data_equation(variable_list({vx, vy}), union_(s, vx, union_(s, vy, vx)), union_(s, vy, vx)));
1277 result.push_back(data_equation(variable_list({vx, vy}), union_(s, union_(s, vx, vy), vx), union_(s, vx, vy)));
1278 result.push_back(data_equation(variable_list({vx, vy}), union_(s, union_(s, vy, vx), vx), union_(s, vy, vx)));
1279 result.push_back(data_equation(variable_list({vf, vg, vs, vt}), union_(s, constructor(s, vf, vs), constructor(s, vg, vt)), constructor(s, or_function(s, vf, vg), fset_union(s, vf, vg, vs, vt))));
1280 result.push_back(data_equation(variable_list({vx}), intersection(s, vx, vx), vx));
1281 result.push_back(data_equation(variable_list({vx, vy}), intersection(s, vx, intersection(s, vx, vy)), intersection(s, vx, vy)));
1282 result.push_back(data_equation(variable_list({vx, vy}), intersection(s, vx, intersection(s, vy, vx)), intersection(s, vy, vx)));
1283 result.push_back(data_equation(variable_list({vx, vy}), intersection(s, intersection(s, vx, vy), vx), intersection(s, vx, vy)));
1284 result.push_back(data_equation(variable_list({vx, vy}), intersection(s, intersection(s, vy, vx), vx), intersection(s, vy, vx)));
1285 result.push_back(data_equation(variable_list({vf, vg, vs, vt}), intersection(s, constructor(s, vf, vs), constructor(s, vg, vt)), constructor(s, and_function(s, vf, vg), fset_intersection(s, vf, vg, vs, vt))));
1286 result.push_back(data_equation(variable_list({vx, vy}), difference(s, vx, vy), intersection(s, vx, complement(s, vy))));
1287 result.push_back(data_equation(variable_list({ve}), false_function(s, ve), sort_bool::false_()));
1288 result.push_back(data_equation(variable_list({ve}), true_function(s, ve), sort_bool::true_()));
1291 result.push_back(data_equation(variable_list({ve, vf}), not_function(s, vf)(ve), sort_bool::not_(vf(ve))));
1292 result.push_back(data_equation(variable_list(), not_function(s, false_function(s)), true_function(s)));
1293 result.push_back(data_equation(variable_list(), not_function(s, true_function(s)), false_function(s)));
1294 result.push_back(data_equation(variable_list({ve, vf, vg}), and_function(s, vf, vg)(ve), sort_bool::and_(vf(ve), vg(ve))));
1295 result.push_back(data_equation(variable_list({vf}), and_function(s, vf, vf), vf));
1296 result.push_back(data_equation(variable_list({vf}), and_function(s, vf, false_function(s)), false_function(s)));
1297 result.push_back(data_equation(variable_list({vf}), and_function(s, false_function(s), vf), false_function(s)));
1298 result.push_back(data_equation(variable_list({vf}), and_function(s, vf, true_function(s)), vf));
1299 result.push_back(data_equation(variable_list({vf}), and_function(s, true_function(s), vf), vf));
1300 result.push_back(data_equation(variable_list({vf}), or_function(s, vf, vf), vf));
1301 result.push_back(data_equation(variable_list({vf}), or_function(s, vf, false_function(s)), vf));
1302 result.push_back(data_equation(variable_list({vf}), or_function(s, false_function(s), vf), vf));
1303 result.push_back(data_equation(variable_list({vf}), or_function(s, vf, true_function(s)), true_function(s)));
1304 result.push_back(data_equation(variable_list({vf}), or_function(s, true_function(s), vf), true_function(s)));
1305 result.push_back(data_equation(variable_list({ve, vf, vg}), or_function(s, vf, vg)(ve), sort_bool::or_(vf(ve), vg(ve))));
1306 result.push_back(data_equation(variable_list({vf, vg}), fset_union(s, vf, vg, sort_fset::empty(s), sort_fset::empty(s)), sort_fset::empty(s)));
1307 result.push_back(data_equation(variable_list({vd, vf, vg, vs}), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::empty(s)), sort_fset::cinsert(s, vd, sort_bool::not_(vg(vd)), fset_union(s, vf, vg, vs, sort_fset::empty(s)))));
1308 result.push_back(data_equation(variable_list({ve, vf, vg, vt}), fset_union(s, vf, vg, sort_fset::empty(s), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, ve, sort_bool::not_(vf(ve)), fset_union(s, vf, vg, sort_fset::empty(s), vt))));
1309 result.push_back(data_equation(variable_list({vd, vf, vg, vs, vt}), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, vd, vt)), sort_fset::cinsert(s, vd, equal_to(vf(vd), vg(vd)), fset_union(s, vf, vg, vs, vt))));
1310 result.push_back(data_equation(variable_list({vd, ve, vf, vg, vs, vt}), less(vd, ve), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, vd, sort_bool::not_(vg(vd)), fset_union(s, vf, vg, vs, sort_fset::cons_(s, ve, vt)))));
1311 result.push_back(data_equation(variable_list({vd, ve, vf, vg, vs, vt}), less(ve, vd), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, ve, sort_bool::not_(vf(ve)), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), vt))));
1312 result.push_back(data_equation(variable_list({vf, vg}), fset_intersection(s, vf, vg, sort_fset::empty(s), sort_fset::empty(s)), sort_fset::empty(s)));
1313 result.push_back(data_equation(variable_list({vd, vf, vg, vs}), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::empty(s)), sort_fset::cinsert(s, vd, vg(vd), fset_intersection(s, vf, vg, vs, sort_fset::empty(s)))));
1314 result.push_back(data_equation(variable_list({ve, vf, vg, vt}), fset_intersection(s, vf, vg, sort_fset::empty(s), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, ve, vf(ve), fset_intersection(s, vf, vg, sort_fset::empty(s), vt))));
1315 result.push_back(data_equation(variable_list({vd, vf, vg, vs, vt}), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, vd, vt)), sort_fset::cinsert(s, vd, equal_to(vf(vd), vg(vd)), fset_intersection(s, vf, vg, vs, vt))));
1316 result.push_back(data_equation(variable_list({vd, ve, vf, vg, vs, vt}), less(vd, ve), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, vd, vg(vd), fset_intersection(s, vf, vg, vs, sort_fset::cons_(s, ve, vt)))));
1317 result.push_back(data_equation(variable_list({vd, ve, vf, vg, vs, vt}), less(ve, vd), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, ve, vf(ve), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), vt))));
1318 return result;
1319 }
1320
1321 } // namespace sort_set_
1322
1323 } // namespace data
1324
1325} // namespace mcrl2
1326
1327#endif // MCRL2_DATA_SET1_H
The class application.
The class basic_sort.
The standard sort bool_.
Term containing a string.
size_type size() const
Returns the number of arguments of this term.
Definition aterm.h:151
An application of a data expression to a number of arguments.
\brief A container sort
const container_type & container_name() const
\brief A data equation
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
universal quantification.
Definition forall.h:26
\brief A function symbol
const core::identifier_string & name() const
const sort_expression & sort() const
universal quantification.
\brief Container type for sets
\brief A sort expression
\brief A data variable
Definition variable.h:28
Standard exception class for reporting runtime errors.
Definition exception.h:27
The class container_sort.
The class function symbol.
The class data_equation.
Exception classes for use in libraries and tools.
The class forall.
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 & and_()
Constructor for function symbol &&.
Definition bool.h:235
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & or_()
Constructor for function symbol ||.
Definition bool.h:299
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fset_cinsert.
Definition fset1.h:271
function_symbol cons_(const sort_expression &s)
Constructor for function symbol @fset_cons.
Definition fset1.h:207
function_symbol empty(const sort_expression &s)
Constructor for function symbol {}.
Definition fset1.h:75
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset1.h:41
const core::identifier_string & fset_intersection_name()
Generate identifier @fset_inter.
Definition set1.h:1027
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition set1.h:334
function_symbol true_function(const sort_expression &s)
Constructor for function symbol @true_.
Definition set1.h:717
const core::identifier_string & or_function_name()
Generate identifier @or_.
Definition set1.h:895
bool is_set_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @setcomp.
Definition set1.h:280
const core::identifier_string & constructor_name()
Generate identifier @set.
Definition set1.h:66
bool is_false_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @false_.
Definition set1.h:665
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition set1.h:600
bool is_not_function_application(const atermpp::aterm &e)
Recogniser for application of @not_.
Definition set1.h:823
bool is_and_function_application(const atermpp::aterm &e)
Recogniser for application of @and_.
Definition set1.h:887
void make_or_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @or_.
Definition set1.h:941
function_symbol_vector set_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for set_.
Definition set1.h:1119
bool is_fset_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_inter.
Definition set1.h:1047
bool is_set(const sort_expression &e)
Recogniser for sort expression Set(s)
Definition set1.h:53
function_symbol or_function(const sort_expression &s)
Constructor for function symbol @or_.
Definition set1.h:905
void make_complement(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol !.
Definition set1.h:396
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition set1.h:483
const core::identifier_string & false_function_name()
Generate identifier @false_.
Definition set1.h:645
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition set1.h:307
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition set1.h:1244
bool is_true_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @true_.
Definition set1.h:727
bool is_complement_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition set1.h:406
bool is_or_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @or_.
Definition set1.h:915
function_symbol fset_intersection(const sort_expression &s)
Constructor for function symbol @fset_inter.
Definition set1.h:1037
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition set1.h:149
const core::identifier_string & set_comprehension_name()
Generate identifier @setcomp.
Definition set1.h:226
void make_fset_union(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fset_union.
Definition set1.h:1009
bool is_fset_union_application(const atermpp::aterm &e)
Recogniser for application of @fset_union.
Definition set1.h:1019
bool is_false_function_application(const atermpp::aterm &e)
Recogniser for application of @false_.
Definition set1.h:699
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition set1.h:1172
bool is_not_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @not_.
Definition set1.h:789
function_symbol and_function(const sort_expression &s)
Constructor for function symbol @and_.
Definition set1.h:841
bool is_set_comprehension_function_symbol(const atermpp::aterm &e)
Recogniser for function @setcomp.
Definition set1.h:246
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition set1.h:344
const core::identifier_string & not_function_name()
Generate identifier @not_.
Definition set1.h:769
const core::identifier_string & in_name()
Generate identifier in.
Definition set1.h:288
function_symbol_vector set_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for set_.
Definition set1.h:130
implementation_map set_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for set_.
Definition set1.h:1160
bool is_fset_intersection_application(const atermpp::aterm &e)
Recogniser for application of @fset_inter.
Definition set1.h:1087
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition set1.h:637
function_symbol not_function(const sort_expression &s)
Constructor for function symbol @not_.
Definition set1.h:779
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition set1.h:1196
bool is_constructor_application(const atermpp::aterm &e)
Recogniser for application of @set.
Definition set1.h:122
const core::identifier_string & fset_union_name()
Generate identifier @fset_union.
Definition set1.h:959
bool is_set_fset_application(const atermpp::aterm &e)
Recogniser for application of @setfset.
Definition set1.h:218
implementation_map set_cpp_implementable_constructors(const sort_expression &s)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition set1.h:154
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition set1.h:550
const core::identifier_string & complement_name()
Generate identifier !.
Definition set1.h:352
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:499
const core::identifier_string & and_function_name()
Generate identifier @and_.
Definition set1.h:831
bool is_fset_union_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_union.
Definition set1.h:979
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition set1.h:1220
function_symbol fset_union(const sort_expression &s)
Constructor for function symbol @fset_union.
Definition set1.h:969
void make_and_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @and_.
Definition set1.h:877
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set1.h:42
bool is_set_fset_function_symbol(const atermpp::aterm &e)
Recogniser for function @setfset.
Definition set1.h:184
const core::identifier_string & intersection_name()
Generate identifier *.
Definition set1.h:491
void make_fset_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fset_inter.
Definition set1.h:1077
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @set.
Definition set1.h:76
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition set1.h:1232
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition set1.h:1184
function_symbol false_function(const sort_expression &s)
Constructor for function symbol @false_.
Definition set1.h:655
void make_constructor(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @set.
Definition set1.h:112
const core::identifier_string & set_fset_name()
Generate identifier @setfset.
Definition set1.h:164
const core::identifier_string & union_name()
Generate identifier +.
Definition set1.h:414
bool is_complement_function_symbol(const atermpp::aterm &e)
Recogniser for function !.
Definition set1.h:372
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:296
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:422
bool is_constructor_function_symbol(const atermpp::aterm &e)
Recogniser for function @set.
Definition set1.h:86
function_symbol_vector set_generate_functions_code(const sort_expression &s)
Give all system defined mappings for set_.
Definition set1.h:1095
function_symbol_vector set_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for set_.
Definition set1.h:141
const core::identifier_string & difference_name()
Generate identifier -.
Definition set1.h:568
void make_set_comprehension(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @setcomp.
Definition set1.h:270
void make_not_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @not_.
Definition set1.h:813
bool is_or_function_application(const atermpp::aterm &e)
Recogniser for application of @or_.
Definition set1.h:951
const core::identifier_string & true_function_name()
Generate identifier @true_.
Definition set1.h:707
void make_false_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @false_.
Definition set1.h:689
void make_true_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @true_.
Definition set1.h:751
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:576
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition set1.h:446
function_symbol complement(const sort_expression &s)
Constructor for function symbol !.
Definition set1.h:362
bool is_true_function_application(const atermpp::aterm &e)
Recogniser for application of @true_.
Definition set1.h:761
function_symbol set_fset(const sort_expression &s)
Constructor for function symbol @setfset.
Definition set1.h:174
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition set1.h:627
void make_union_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition set1.h:473
function_symbol set_comprehension(const sort_expression &s)
Constructor for function symbol @setcomp.
Definition set1.h:236
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition set1.h:560
data_equation_vector set_generate_equations_code(const sort_expression &s)
Give all system defined equations for set_.
Definition set1.h:1254
function_symbol_vector set_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for set_.
Definition set1.h:1133
bool is_and_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @and_.
Definition set1.h:851
void make_set_fset(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @setfset.
Definition set1.h:208
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition set1.h:523
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition set1.h:1208
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_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
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
void make_application(atermpp::aterm &result)
Make function for an application.
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.