mCRL2
Loading...
Searching...
No Matches
bag1.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_BAG1_H
16#define MCRL2_DATA_BAG1_H
17
18#include "functional" // std::function
25#include "mcrl2/data/standard.h"
26#include "mcrl2/data/forall.h"
28#include "mcrl2/data/nat1.h"
29#include "mcrl2/data/fbag1.h"
30#include "mcrl2/data/fset1.h"
31#include "mcrl2/data/set1.h"
32
33namespace mcrl2 {
34
35 namespace data {
36
38 namespace sort_bag {
39
43 inline
45 {
47 return bag;
48 }
49
54 inline
55 bool is_bag(const sort_expression& e)
56 {
57 if (is_container_sort(e))
58 {
60 }
61 return false;
62 }
63
64
67 inline
69 {
71 return constructor_name;
72 }
73
77 inline
79 {
81 return constructor;
82 }
83
87 inline
89 {
90 if (is_function_symbol(e))
91 {
92 return atermpp::down_cast<function_symbol>(e).name() == constructor_name();
93 }
94 return false;
95 }
96
102 inline
104 {
105 return sort_bag::constructor(s)(arg0, arg1);
106 }
107
113 inline
115 {
117 }
118
123 inline
125 {
126 return is_application(e) && is_constructor_function_symbol(atermpp::down_cast<application>(e).head());
127 }
131 inline
133 {
135 result.push_back(sort_bag::constructor(s));
136
137 return result;
138 }
142 inline
144 {
146 result.push_back(sort_bag::constructor(s));
147
148 return result;
149 }
150 // 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
151 typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
155 inline
157 {
158 implementation_map result;
159 static_cast< void >(s); // suppress unused variable warnings
160 return result;
161 }
162
165 inline
167 {
169 return bag_fbag_name;
170 }
171
175 inline
177 {
179 return bag_fbag;
180 }
181
185 inline
187 {
188 if (is_function_symbol(e))
189 {
190 return atermpp::down_cast<function_symbol>(e).name() == bag_fbag_name();
191 }
192 return false;
193 }
194
199 inline
201 {
202 return sort_bag::bag_fbag(s)(arg0);
203 }
204
209 inline
211 {
212 make_application(result, sort_bag::bag_fbag(s),arg0);
213 }
214
219 inline
221 {
222 return is_application(e) && is_bag_fbag_function_symbol(atermpp::down_cast<application>(e).head());
223 }
224
227 inline
229 {
232 }
233
237 inline
239 {
241 return bag_comprehension;
242 }
243
247 inline
249 {
250 if (is_function_symbol(e))
251 {
252 return atermpp::down_cast<function_symbol>(e).name() == bag_comprehension_name();
253 }
254 return false;
255 }
256
261 inline
263 {
264 return sort_bag::bag_comprehension(s)(arg0);
265 }
266
271 inline
273 {
275 }
276
281 inline
283 {
284 return is_application(e) && is_bag_comprehension_function_symbol(atermpp::down_cast<application>(e).head());
285 }
286
289 inline
291 {
293 return count_name;
294 }
295
296 // This function is not intended for public use and therefore not documented in Doxygen.
297 inline
299 {
300 sort_expression target_sort(sort_nat::nat());
301 function_symbol count(count_name(), make_function_sort_(s0, s1, target_sort));
302 return count;
303 }
304
308 inline
310 {
311 if (is_function_symbol(e))
312 {
313 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
314 return f.name() == count_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
315 }
316 return false;
317 }
318
324 inline
326 {
327 return sort_bag::count(s, arg0.sort(), arg1.sort())(arg0, arg1);
328 }
329
335 inline
337 {
338 make_application(result, sort_bag::count(s, arg0.sort(), arg1.sort()),arg0, arg1);
339 }
340
345 inline
347 {
348 return is_application(e) && is_count_function_symbol(atermpp::down_cast<application>(e).head());
349 }
350
353 inline
355 {
357 return in_name;
358 }
359
360 // This function is not intended for public use and therefore not documented in Doxygen.
361 inline
363 {
364 sort_expression target_sort(sort_bool::bool_());
365 function_symbol in(in_name(), make_function_sort_(s0, s1, target_sort));
366 return in;
367 }
368
372 inline
374 {
375 if (is_function_symbol(e))
376 {
377 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
378 return f.name() == in_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
379 }
380 return false;
381 }
382
388 inline
390 {
391 return sort_bag::in(s, arg0.sort(), arg1.sort())(arg0, arg1);
392 }
393
399 inline
400 void make_in(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
401 {
402 make_application(result, sort_bag::in(s, arg0.sort(), arg1.sort()),arg0, arg1);
403 }
404
409 inline
411 {
412 return is_application(e) && is_in_function_symbol(atermpp::down_cast<application>(e).head());
413 }
414
417 inline
419 {
421 return union_name;
422 }
423
424 // This function is not intended for public use and therefore not documented in Doxygen.
425 inline
427 {
428 sort_expression target_sort;
429 if (s0 == bag(s) && s1 == bag(s))
430 {
431 target_sort = bag(s);
432 }
433 else if (s0 == sort_set::set_(s) && s1 == sort_set::set_(s))
434 {
435 target_sort = sort_set::set_(s);
436 }
437 else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
438 {
439 target_sort = sort_fset::fset(s);
440 }
441 else if (s0 == sort_fbag::fbag(s) && s1 == sort_fbag::fbag(s))
442 {
443 target_sort = sort_fbag::fbag(s);
444 }
445 else
446 {
447 throw mcrl2::runtime_error("Cannot compute target sort for union_ with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
448 }
449
450 function_symbol union_(union_name(), make_function_sort_(s0, s1, target_sort));
451 return union_;
452 }
453
457 inline
459 {
460 if (is_function_symbol(e))
461 {
462 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
463 return f.name() == union_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
464 }
465 return false;
466 }
467
473 inline
475 {
476 return sort_bag::union_(s, arg0.sort(), arg1.sort())(arg0, arg1);
477 }
478
484 inline
486 {
487 make_application(result, sort_bag::union_(s, arg0.sort(), arg1.sort()),arg0, arg1);
488 }
489
494 inline
496 {
497 return is_application(e) && is_union_function_symbol(atermpp::down_cast<application>(e).head());
498 }
499
502 inline
504 {
506 return intersection_name;
507 }
508
509 // This function is not intended for public use and therefore not documented in Doxygen.
510 inline
512 {
513 sort_expression target_sort;
514 if (s0 == bag(s) && s1 == bag(s))
515 {
516 target_sort = bag(s);
517 }
518 else if (s0 == sort_set::set_(s) && s1 == sort_set::set_(s))
519 {
520 target_sort = sort_set::set_(s);
521 }
522 else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
523 {
524 target_sort = sort_fset::fset(s);
525 }
526 else if (s0 == sort_fbag::fbag(s) && s1 == sort_fbag::fbag(s))
527 {
528 target_sort = sort_fbag::fbag(s);
529 }
530 else
531 {
532 throw mcrl2::runtime_error("Cannot compute target sort for intersection with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
533 }
534
536 return intersection;
537 }
538
542 inline
544 {
545 if (is_function_symbol(e))
546 {
547 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
548 return f.name() == intersection_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
549 }
550 return false;
551 }
552
558 inline
560 {
561 return sort_bag::intersection(s, arg0.sort(), arg1.sort())(arg0, arg1);
562 }
563
569 inline
571 {
572 make_application(result, sort_bag::intersection(s, arg0.sort(), arg1.sort()),arg0, arg1);
573 }
574
579 inline
581 {
582 return is_application(e) && is_intersection_function_symbol(atermpp::down_cast<application>(e).head());
583 }
584
587 inline
589 {
591 return difference_name;
592 }
593
594 // This function is not intended for public use and therefore not documented in Doxygen.
595 inline
597 {
598 sort_expression target_sort;
599 if (s0 == bag(s) && s1 == bag(s))
600 {
601 target_sort = bag(s);
602 }
603 else if (s0 == sort_set::set_(s) && s1 == sort_set::set_(s))
604 {
605 target_sort = sort_set::set_(s);
606 }
607 else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
608 {
609 target_sort = sort_fset::fset(s);
610 }
611 else if (s0 == sort_fbag::fbag(s) && s1 == sort_fbag::fbag(s))
612 {
613 target_sort = sort_fbag::fbag(s);
614 }
615 else
616 {
617 throw mcrl2::runtime_error("Cannot compute target sort for difference with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
618 }
619
621 return difference;
622 }
623
627 inline
629 {
630 if (is_function_symbol(e))
631 {
632 const function_symbol& f = atermpp::down_cast<function_symbol>(e);
633 return f.name() == difference_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
634 }
635 return false;
636 }
637
643 inline
645 {
646 return sort_bag::difference(s, arg0.sort(), arg1.sort())(arg0, arg1);
647 }
648
654 inline
656 {
657 make_application(result, sort_bag::difference(s, arg0.sort(), arg1.sort()),arg0, arg1);
658 }
659
664 inline
666 {
667 return is_application(e) && is_difference_function_symbol(atermpp::down_cast<application>(e).head());
668 }
669
672 inline
674 {
676 return bag2set_name;
677 }
678
682 inline
684 {
686 return bag2set;
687 }
688
692 inline
694 {
695 if (is_function_symbol(e))
696 {
697 return atermpp::down_cast<function_symbol>(e).name() == bag2set_name();
698 }
699 return false;
700 }
701
706 inline
708 {
709 return sort_bag::bag2set(s)(arg0);
710 }
711
716 inline
717 void make_bag2set(data_expression& result, const sort_expression& s, const data_expression& arg0)
718 {
719 make_application(result, sort_bag::bag2set(s),arg0);
720 }
721
726 inline
728 {
729 return is_application(e) && is_bag2set_function_symbol(atermpp::down_cast<application>(e).head());
730 }
731
734 inline
736 {
738 return set2bag_name;
739 }
740
744 inline
746 {
748 return set2bag;
749 }
750
754 inline
756 {
757 if (is_function_symbol(e))
758 {
759 return atermpp::down_cast<function_symbol>(e).name() == set2bag_name();
760 }
761 return false;
762 }
763
768 inline
770 {
771 return sort_bag::set2bag(s)(arg0);
772 }
773
778 inline
779 void make_set2bag(data_expression& result, const sort_expression& s, const data_expression& arg0)
780 {
781 make_application(result, sort_bag::set2bag(s),arg0);
782 }
783
788 inline
790 {
791 return is_application(e) && is_set2bag_function_symbol(atermpp::down_cast<application>(e).head());
792 }
793
796 inline
798 {
800 return zero_function_name;
801 }
802
806 inline
808 {
810 return zero_function;
811 }
812
816 inline
818 {
819 if (is_function_symbol(e))
820 {
821 return atermpp::down_cast<function_symbol>(e).name() == zero_function_name();
822 }
823 return false;
824 }
825
830 inline
832 {
833 return sort_bag::zero_function(s)(arg0);
834 }
835
840 inline
842 {
844 }
845
850 inline
852 {
853 return is_application(e) && is_zero_function_function_symbol(atermpp::down_cast<application>(e).head());
854 }
855
858 inline
860 {
862 return one_function_name;
863 }
864
868 inline
870 {
872 return one_function;
873 }
874
878 inline
880 {
881 if (is_function_symbol(e))
882 {
883 return atermpp::down_cast<function_symbol>(e).name() == one_function_name();
884 }
885 return false;
886 }
887
892 inline
894 {
895 return sort_bag::one_function(s)(arg0);
896 }
897
902 inline
904 {
906 }
907
912 inline
914 {
915 return is_application(e) && is_one_function_function_symbol(atermpp::down_cast<application>(e).head());
916 }
917
920 inline
922 {
924 return add_function_name;
925 }
926
930 inline
932 {
934 return add_function;
935 }
936
940 inline
942 {
943 if (is_function_symbol(e))
944 {
945 return atermpp::down_cast<function_symbol>(e).name() == add_function_name();
946 }
947 return false;
948 }
949
955 inline
957 {
958 return sort_bag::add_function(s)(arg0, arg1);
959 }
960
966 inline
968 {
970 }
971
976 inline
978 {
979 return is_application(e) && is_add_function_function_symbol(atermpp::down_cast<application>(e).head());
980 }
981
984 inline
986 {
988 return min_function_name;
989 }
990
994 inline
996 {
998 return min_function;
999 }
1000
1004 inline
1006 {
1007 if (is_function_symbol(e))
1008 {
1009 return atermpp::down_cast<function_symbol>(e).name() == min_function_name();
1010 }
1011 return false;
1012 }
1013
1019 inline
1021 {
1022 return sort_bag::min_function(s)(arg0, arg1);
1023 }
1024
1030 inline
1032 {
1034 }
1035
1040 inline
1042 {
1043 return is_application(e) && is_min_function_function_symbol(atermpp::down_cast<application>(e).head());
1044 }
1045
1048 inline
1050 {
1052 return monus_function_name;
1053 }
1054
1058 inline
1060 {
1062 return monus_function;
1063 }
1064
1068 inline
1070 {
1071 if (is_function_symbol(e))
1072 {
1073 return atermpp::down_cast<function_symbol>(e).name() == monus_function_name();
1074 }
1075 return false;
1076 }
1077
1083 inline
1085 {
1086 return sort_bag::monus_function(s)(arg0, arg1);
1087 }
1088
1094 inline
1096 {
1098 }
1099
1104 inline
1106 {
1107 return is_application(e) && is_monus_function_function_symbol(atermpp::down_cast<application>(e).head());
1108 }
1109
1112 inline
1114 {
1117 }
1118
1122 inline
1124 {
1126 return nat2bool_function;
1127 }
1128
1132 inline
1134 {
1135 if (is_function_symbol(e))
1136 {
1137 return atermpp::down_cast<function_symbol>(e).name() == nat2bool_function_name();
1138 }
1139 return false;
1140 }
1141
1146 inline
1148 {
1149 return sort_bag::nat2bool_function(s)(arg0);
1150 }
1151
1156 inline
1158 {
1160 }
1161
1166 inline
1168 {
1169 return is_application(e) && is_nat2bool_function_function_symbol(atermpp::down_cast<application>(e).head());
1170 }
1171
1174 inline
1176 {
1179 }
1180
1184 inline
1186 {
1188 return bool2nat_function;
1189 }
1190
1194 inline
1196 {
1197 if (is_function_symbol(e))
1198 {
1199 return atermpp::down_cast<function_symbol>(e).name() == bool2nat_function_name();
1200 }
1201 return false;
1202 }
1203
1208 inline
1210 {
1211 return sort_bag::bool2nat_function(s)(arg0);
1212 }
1213
1218 inline
1220 {
1222 }
1223
1228 inline
1230 {
1231 return is_application(e) && is_bool2nat_function_function_symbol(atermpp::down_cast<application>(e).head());
1232 }
1233
1236 inline
1238 {
1240 return fbag_join_name;
1241 }
1242
1246 inline
1248 {
1250 return fbag_join;
1251 }
1252
1256 inline
1258 {
1259 if (is_function_symbol(e))
1260 {
1261 return atermpp::down_cast<function_symbol>(e).name() == fbag_join_name();
1262 }
1263 return false;
1264 }
1265
1273 inline
1275 {
1276 return sort_bag::fbag_join(s)(arg0, arg1, arg2, arg3);
1277 }
1278
1286 inline
1288 {
1290 }
1291
1296 inline
1298 {
1299 return is_application(e) && is_fbag_join_function_symbol(atermpp::down_cast<application>(e).head());
1300 }
1301
1304 inline
1306 {
1308 return fbag_intersect_name;
1309 }
1310
1314 inline
1316 {
1318 return fbag_intersect;
1319 }
1320
1324 inline
1326 {
1327 if (is_function_symbol(e))
1328 {
1329 return atermpp::down_cast<function_symbol>(e).name() == fbag_intersect_name();
1330 }
1331 return false;
1332 }
1333
1341 inline
1343 {
1344 return sort_bag::fbag_intersect(s)(arg0, arg1, arg2, arg3);
1345 }
1346
1354 inline
1356 {
1358 }
1359
1364 inline
1366 {
1367 return is_application(e) && is_fbag_intersect_function_symbol(atermpp::down_cast<application>(e).head());
1368 }
1369
1372 inline
1374 {
1376 return fbag_difference_name;
1377 }
1378
1382 inline
1384 {
1386 return fbag_difference;
1387 }
1388
1392 inline
1394 {
1395 if (is_function_symbol(e))
1396 {
1397 return atermpp::down_cast<function_symbol>(e).name() == fbag_difference_name();
1398 }
1399 return false;
1400 }
1401
1409 inline
1411 {
1412 return sort_bag::fbag_difference(s)(arg0, arg1, arg2, arg3);
1413 }
1414
1422 inline
1424 {
1426 }
1427
1432 inline
1434 {
1435 return is_application(e) && is_fbag_difference_function_symbol(atermpp::down_cast<application>(e).head());
1436 }
1437
1440 inline
1442 {
1444 return fbag2fset_name;
1445 }
1446
1450 inline
1452 {
1454 return fbag2fset;
1455 }
1456
1460 inline
1462 {
1463 if (is_function_symbol(e))
1464 {
1465 return atermpp::down_cast<function_symbol>(e).name() == fbag2fset_name();
1466 }
1467 return false;
1468 }
1469
1475 inline
1477 {
1478 return sort_bag::fbag2fset(s)(arg0, arg1);
1479 }
1480
1486 inline
1488 {
1489 make_application(result, sort_bag::fbag2fset(s),arg0, arg1);
1490 }
1491
1496 inline
1498 {
1499 return is_application(e) && is_fbag2fset_function_symbol(atermpp::down_cast<application>(e).head());
1500 }
1504 inline
1506 {
1508 result.push_back(sort_bag::bag_fbag(s));
1509 result.push_back(sort_bag::bag_comprehension(s));
1510 result.push_back(sort_bag::count(s, s, bag(s)));
1511 result.push_back(sort_bag::in(s, s, bag(s)));
1512 result.push_back(sort_bag::union_(s, bag(s), bag(s)));
1513 result.push_back(sort_bag::intersection(s, bag(s), bag(s)));
1514 result.push_back(sort_bag::difference(s, bag(s), bag(s)));
1515 result.push_back(sort_bag::bag2set(s));
1516 result.push_back(sort_bag::set2bag(s));
1517 result.push_back(sort_bag::zero_function(s));
1518 result.push_back(sort_bag::one_function(s));
1519 result.push_back(sort_bag::add_function(s));
1520 result.push_back(sort_bag::min_function(s));
1521 result.push_back(sort_bag::monus_function(s));
1522 result.push_back(sort_bag::nat2bool_function(s));
1523 result.push_back(sort_bag::bool2nat_function(s));
1524 result.push_back(sort_bag::fbag_join(s));
1525 result.push_back(sort_bag::fbag_intersect(s));
1526 result.push_back(sort_bag::fbag_difference(s));
1527 result.push_back(sort_bag::fbag2fset(s));
1528 return result;
1529 }
1530
1534 inline
1536 {
1539 {
1540 result.push_back(f);
1541 }
1542 return result;
1543 }
1544
1548 inline
1550 {
1552 result.push_back(sort_bag::bag_fbag(s));
1553 result.push_back(sort_bag::bag_comprehension(s));
1554 result.push_back(sort_bag::count(s, s, bag(s)));
1555 result.push_back(sort_bag::in(s, s, bag(s)));
1556 result.push_back(sort_bag::union_(s, bag(s), bag(s)));
1557 result.push_back(sort_bag::intersection(s, bag(s), bag(s)));
1558 result.push_back(sort_bag::difference(s, bag(s), bag(s)));
1559 result.push_back(sort_bag::bag2set(s));
1560 result.push_back(sort_bag::set2bag(s));
1561 result.push_back(sort_bag::zero_function(s));
1562 result.push_back(sort_bag::one_function(s));
1563 result.push_back(sort_bag::add_function(s));
1564 result.push_back(sort_bag::min_function(s));
1565 result.push_back(sort_bag::monus_function(s));
1566 result.push_back(sort_bag::nat2bool_function(s));
1567 result.push_back(sort_bag::bool2nat_function(s));
1568 result.push_back(sort_bag::fbag_join(s));
1569 result.push_back(sort_bag::fbag_intersect(s));
1570 result.push_back(sort_bag::fbag_difference(s));
1571 result.push_back(sort_bag::fbag2fset(s));
1572 return result;
1573 }
1574
1575
1576 // 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
1577 typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
1581 inline
1583 {
1584 implementation_map result;
1585 static_cast< void >(s); // suppress unused variable warnings
1586 return result;
1587 }
1593 inline
1595 {
1597 return atermpp::down_cast<application>(e)[0];
1598 }
1599
1605 inline
1607 {
1609 return atermpp::down_cast<application>(e)[1];
1610 }
1611
1617 inline
1619 {
1621 return atermpp::down_cast<application>(e)[0];
1622 }
1623
1629 inline
1631 {
1633 return atermpp::down_cast<application>(e)[0];
1634 }
1635
1641 inline
1643 {
1645 return atermpp::down_cast<application>(e)[1];
1646 }
1647
1653 inline
1655 {
1657 return atermpp::down_cast<application>(e)[2];
1658 }
1659
1665 inline
1667 {
1669 return atermpp::down_cast<application>(e)[3];
1670 }
1671
1675 inline
1677 {
1678 variable vb("b",sort_fbag::fbag(s));
1679 variable vc("c",sort_fbag::fbag(s));
1680 variable vd("d",s);
1681 variable ve("e",s);
1685 variable vp("p",sort_pos::pos());
1686 variable vq("q",sort_pos::pos());
1687 variable vs("s",sort_fset::fset(s));
1688 variable vx("x",bag(s));
1689 variable vy("y",bag(s));
1690
1691 data_equation_vector result;
1692 result.push_back(data_equation(variable_list({vb}), bag_fbag(s, vb), constructor(s, zero_function(s), vb)));
1693 result.push_back(data_equation(variable_list({vf}), sort_bag::bag_comprehension(s, vf), constructor(s, vf, sort_fbag::empty(s))));
1694 result.push_back(data_equation(variable_list({vb, ve, vf}), count(s, ve, constructor(s, vf, vb)), sort_nat::swap_zero(vf(ve), count(s, ve, vb))));
1695 result.push_back(data_equation(variable_list({ve, vx}), in(s, ve, vx), greater(count(s, ve, vx), sort_nat::c0())));
1696 result.push_back(data_equation(variable_list({vb, vc, vf, vg}), equal_to(constructor(s, vf, vb), constructor(s, vg, vc)), if_(equal_to(vf, vg), equal_to(vb, vc), forall(variable_list({vd}), equal_to(count(s, vd, constructor(s, vf, vb)), count(s, vd, constructor(s, vg, vc)))))));
1697 result.push_back(data_equation(variable_list({vx, vy}), less(vx, vy), sort_bool::and_(less_equal(vx, vy), not_equal_to(vx, vy))));
1698 result.push_back(data_equation(variable_list({vx, vy}), less_equal(vx, vy), equal_to(intersection(s, vx, vy), vx)));
1699 result.push_back(data_equation(variable_list({vb, vc, vf, vg}), union_(s, constructor(s, vf, vb), constructor(s, vg, vc)), constructor(s, add_function(s, vf, vg), fbag_join(s, vf, vg, vb, vc))));
1700 result.push_back(data_equation(variable_list({vx}), intersection(s, vx, vx), vx));
1701 result.push_back(data_equation(variable_list({vx, vy}), intersection(s, vx, intersection(s, vx, vy)), intersection(s, vx, vy)));
1702 result.push_back(data_equation(variable_list({vx, vy}), intersection(s, vx, intersection(s, vy, vx)), intersection(s, vy, vx)));
1703 result.push_back(data_equation(variable_list({vx, vy}), intersection(s, intersection(s, vx, vy), vx), intersection(s, vx, vy)));
1704 result.push_back(data_equation(variable_list({vx, vy}), intersection(s, intersection(s, vy, vx), vx), intersection(s, vy, vx)));
1705 result.push_back(data_equation(variable_list({vb, vc, vf, vg}), intersection(s, constructor(s, vf, vb), constructor(s, vg, vc)), constructor(s, min_function(s, vf, vg), fbag_intersect(s, vf, vg, vb, vc))));
1706 result.push_back(data_equation(variable_list({vb, vc, vf, vg}), difference(s, constructor(s, vf, vb), constructor(s, vg, vc)), constructor(s, monus_function(s, vf, vg), fbag_difference(s, vf, vg, vb, vc))));
1707 result.push_back(data_equation(variable_list({vb, vf}), bag2set(s, constructor(s, vf, vb)), sort_set::constructor(s, nat2bool_function(s, vf), fbag2fset(s, vf, vb))));
1708 result.push_back(data_equation(variable_list({vh, vs}), set2bag(s, sort_set::constructor(s, vh, vs)), constructor(s, bool2nat_function(s, vh), sort_fbag::fset2fbag(s, vs))));
1709 result.push_back(data_equation(variable_list({ve}), zero_function(s, ve), sort_nat::c0()));
1710 result.push_back(data_equation(variable_list({ve}), one_function(s, ve), sort_nat::cnat(sort_pos::c1())));
1713 result.push_back(data_equation(variable_list({ve, vf, vg}), add_function(s, vf, vg)(ve), sort_nat::plus(vf(ve), vg(ve))));
1714 result.push_back(data_equation(variable_list({vf}), add_function(s, vf, zero_function(s)), vf));
1715 result.push_back(data_equation(variable_list({vf}), add_function(s, zero_function(s), vf), vf));
1716 result.push_back(data_equation(variable_list({ve, vf, vg}), min_function(s, vf, vg)(ve), sort_nat::minimum(vf(ve), vg(ve))));
1717 result.push_back(data_equation(variable_list({vf}), min_function(s, vf, vf), vf));
1718 result.push_back(data_equation(variable_list({vf}), min_function(s, vf, zero_function(s)), zero_function(s)));
1719 result.push_back(data_equation(variable_list({vf}), min_function(s, zero_function(s), vf), zero_function(s)));
1720 result.push_back(data_equation(variable_list({ve, vf, vg}), monus_function(s, vf, vg)(ve), sort_nat::monus(vf(ve), vg(ve))));
1721 result.push_back(data_equation(variable_list({vf}), monus_function(s, vf, vf), zero_function(s)));
1722 result.push_back(data_equation(variable_list({vf}), monus_function(s, vf, zero_function(s)), vf));
1723 result.push_back(data_equation(variable_list({vf}), monus_function(s, zero_function(s), vf), zero_function(s)));
1724 result.push_back(data_equation(variable_list({ve, vf}), nat2bool_function(s, vf)(ve), greater(vf(ve), sort_nat::c0())));
1727 result.push_back(data_equation(variable_list({ve, vh}), bool2nat_function(s, vh)(ve), if_(vh(ve), sort_nat::cnat(sort_pos::c1()), sort_nat::c0())));
1730 result.push_back(data_equation(variable_list({vf, vg}), fbag_join(s, vf, vg, sort_fbag::empty(s), sort_fbag::empty(s)), sort_fbag::empty(s)));
1731 result.push_back(data_equation(variable_list({vb, vd, vf, vg, vp}), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::empty(s)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_add(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_join(s, vf, vg, vb, sort_fbag::empty(s)))));
1732 result.push_back(data_equation(variable_list({vc, ve, vf, vg, vq}), fbag_join(s, vf, vg, sort_fbag::empty(s), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_add(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_join(s, vf, vg, sort_fbag::empty(s), vc))));
1733 result.push_back(data_equation(variable_list({vb, vc, vd, vf, vg, vp, vq}), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, vd, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_add(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::cnat(vq)), fbag_join(s, vf, vg, vb, vc))));
1734 result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(vd, ve), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_add(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_join(s, vf, vg, vb, sort_fbag::cons_(s, ve, vq, vc)))));
1735 result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(ve, vd), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_add(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), vc))));
1736 result.push_back(data_equation(variable_list({vf, vg}), fbag_intersect(s, vf, vg, sort_fbag::empty(s), sort_fbag::empty(s)), sort_fbag::empty(s)));
1737 result.push_back(data_equation(variable_list({vb, vd, vf, vg, vp}), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::empty(s)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_min(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_intersect(s, vf, vg, vb, sort_fbag::empty(s)))));
1738 result.push_back(data_equation(variable_list({vc, ve, vf, vg, vq}), fbag_intersect(s, vf, vg, sort_fbag::empty(s), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_min(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_intersect(s, vf, vg, sort_fbag::empty(s), vc))));
1739 result.push_back(data_equation(variable_list({vb, vc, vd, vf, vg, vp, vq}), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, vd, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_min(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::cnat(vq)), fbag_intersect(s, vf, vg, vb, vc))));
1740 result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(vd, ve), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_min(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_intersect(s, vf, vg, vb, sort_fbag::cons_(s, ve, vq, vc)))));
1741 result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(ve, vd), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_min(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), vc))));
1742 result.push_back(data_equation(variable_list({vf, vg}), fbag_difference(s, vf, vg, sort_fbag::empty(s), sort_fbag::empty(s)), sort_fbag::empty(s)));
1743 result.push_back(data_equation(variable_list({vb, vd, vf, vg, vp}), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::empty(s)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_monus(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_difference(s, vf, vg, vb, sort_fbag::empty(s)))));
1744 result.push_back(data_equation(variable_list({vc, ve, vf, vg, vq}), fbag_difference(s, vf, vg, sort_fbag::empty(s), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_monus(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_difference(s, vf, vg, sort_fbag::empty(s), vc))));
1745 result.push_back(data_equation(variable_list({vb, vc, vd, vf, vg, vp, vq}), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, vd, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_monus(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::cnat(vq)), fbag_difference(s, vf, vg, vb, vc))));
1746 result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(vd, ve), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_monus(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_difference(s, vf, vg, vb, sort_fbag::cons_(s, ve, vq, vc)))));
1747 result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(ve, vd), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_monus(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), vc))));
1748 result.push_back(data_equation(variable_list({vf}), fbag2fset(s, vf, sort_fbag::empty(s)), sort_fset::empty(s)));
1749 result.push_back(data_equation(variable_list({vb, vd, vf, vp}), fbag2fset(s, vf, sort_fbag::cons_(s, vd, vp, vb)), sort_fset::cinsert(s, vd, equal_to(equal_to(vf(vd), sort_nat::cnat(vp)), greater(vf(vd), sort_nat::c0())), fbag2fset(s, vf, vb))));
1750 return result;
1751 }
1752
1753 } // namespace sort_bag
1754
1755 } // namespace data
1756
1757} // namespace mcrl2
1758
1759#endif // MCRL2_DATA_BAG1_H
The class application.
The class basic_sort.
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.
universal quantification.
\brief Container type for bags
\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
\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.
function_symbol fbag2fset(const sort_expression &s)
Constructor for function symbol @fbag2fset.
Definition bag1.h:1451
bool is_bag2set_application(const atermpp::aterm &e)
Recogniser for application of Bag2Set.
Definition bag1.h:727
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition bag1.h:543
void make_bool2nat_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @Bool2Nat_.
Definition bag1.h:1219
const core::identifier_string & fbag2fset_name()
Generate identifier @fbag2fset.
Definition bag1.h:1441
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bag1.h:1606
bool is_min_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @min_.
Definition bag1.h:1005
function_symbol bag_fbag(const sort_expression &s)
Constructor for function symbol @bagfbag.
Definition bag1.h:176
bool is_min_function_application(const atermpp::aterm &e)
Recogniser for application of @min_.
Definition bag1.h:1041
function_symbol monus_function(const sort_expression &s)
Constructor for function symbol @monus_.
Definition bag1.h:1059
const core::identifier_string & fbag_intersect_name()
Generate identifier @fbag_inter.
Definition bag1.h:1305
void make_bag2set(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Bag2Set.
Definition bag1.h:717
bool is_fbag_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_diff.
Definition bag1.h:1393
bool is_fbag_join_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_join.
Definition bag1.h:1257
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol count.
Definition bag1.h:336
function_symbol_vector bag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for bag.
Definition bag1.h:1505
const core::identifier_string & bool2nat_function_name()
Generate identifier @Bool2Nat_.
Definition bag1.h:1175
void make_one_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @one_.
Definition bag1.h:903
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition bag1.h:1654
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition bag1.h:665
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:596
const core::identifier_string & set2bag_name()
Generate identifier Set2Bag.
Definition bag1.h:735
bool is_bag_fbag_application(const atermpp::aterm &e)
Recogniser for application of @bagfbag.
Definition bag1.h:220
function_symbol_vector bag_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for bag.
Definition bag1.h:1535
void make_add_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @add_.
Definition bag1.h:967
data_equation_vector bag_generate_equations_code(const sort_expression &s)
Give all system defined equations for bag.
Definition bag1.h:1676
bool is_fbag_difference_application(const atermpp::aterm &e)
Recogniser for application of @fbag_diff.
Definition bag1.h:1433
bool is_bag_fbag_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagfbag.
Definition bag1.h:186
const core::identifier_string & zero_function_name()
Generate identifier @zero_.
Definition bag1.h:797
const core::identifier_string & add_function_name()
Generate identifier @add_.
Definition bag1.h:921
function_symbol_vector bag_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for bag.
Definition bag1.h:143
bool is_fbag2fset_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag2fset.
Definition bag1.h:1461
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition bag1.h:495
function_symbol bag2set(const sort_expression &s)
Constructor for function symbol Bag2Set.
Definition bag1.h:683
bool is_monus_function_application(const atermpp::aterm &e)
Recogniser for application of @monus_.
Definition bag1.h:1105
const core::identifier_string & nat2bool_function_name()
Generate identifier @Nat2Bool_.
Definition bag1.h:1113
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:511
bool is_zero_function_application(const atermpp::aterm &e)
Recogniser for application of @zero_.
Definition bag1.h:851
const core::identifier_string & fbag_difference_name()
Generate identifier @fbag_diff.
Definition bag1.h:1373
void make_monus_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @monus_.
Definition bag1.h:1095
implementation_map bag_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for bag.
Definition bag1.h:1582
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function count.
Definition bag1.h:309
function_symbol count(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:298
implementation_map bag_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 bag1.h:156
function_symbol add_function(const sort_expression &s)
Constructor for function symbol @add_.
Definition bag1.h:931
bool is_nat2bool_function_application(const atermpp::aterm &e)
Recogniser for application of @Nat2Bool_.
Definition bag1.h:1167
function_symbol fbag_intersect(const sort_expression &s)
Constructor for function symbol @fbag_inter.
Definition bag1.h:1315
void make_fbag_intersect(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 @fbag_inter.
Definition bag1.h:1355
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition bag1.h:458
void make_nat2bool_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @Nat2Bool_.
Definition bag1.h:1157
bool is_fbag_intersect_application(const atermpp::aterm &e)
Recogniser for application of @fbag_inter.
Definition bag1.h:1365
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition bag1.h:410
function_symbol fbag_difference(const sort_expression &s)
Constructor for function symbol @fbag_diff.
Definition bag1.h:1383
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition bag1.h:373
bool is_bag_comprehension_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagcomp.
Definition bag1.h:248
void make_min_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @min_.
Definition bag1.h:1031
const core::identifier_string & min_function_name()
Generate identifier @min_.
Definition bag1.h:985
bool is_set2bag_function_symbol(const atermpp::aterm &e)
Recogniser for function Set2Bag.
Definition bag1.h:755
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bag1.h:1594
function_symbol_vector bag_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for bag.
Definition bag1.h:1549
bool is_nat2bool_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Nat2Bool_.
Definition bag1.h:1133
const core::identifier_string & monus_function_name()
Generate identifier @monus_.
Definition bag1.h:1049
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition bag1.h:1666
bool is_add_function_application(const atermpp::aterm &e)
Recogniser for application of @add_.
Definition bag1.h:977
void make_fbag2fset(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @fbag2fset.
Definition bag1.h:1487
void make_fbag_join(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 @fbag_join.
Definition bag1.h:1287
function_symbol min_function(const sort_expression &s)
Constructor for function symbol @min_.
Definition bag1.h:995
function_symbol set2bag(const sort_expression &s)
Constructor for function symbol Set2Bag.
Definition bag1.h:745
const core::identifier_string & bag_fbag_name()
Generate identifier @bagfbag.
Definition bag1.h:166
const core::identifier_string & bag2set_name()
Generate identifier Bag2Set.
Definition bag1.h:673
const core::identifier_string & intersection_name()
Generate identifier *.
Definition bag1.h:503
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 bag1.h:400
function_symbol bag_comprehension(const sort_expression &s)
Constructor for function symbol @bagcomp.
Definition bag1.h:238
bool is_bag2set_function_symbol(const atermpp::aterm &e)
Recogniser for function Bag2Set.
Definition bag1.h:693
bool is_bool2nat_function_application(const atermpp::aterm &e)
Recogniser for application of @Bool2Nat_.
Definition bag1.h:1229
const core::identifier_string & fbag_join_name()
Generate identifier @fbag_join.
Definition bag1.h:1237
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 bag1.h:570
function_symbol fbag_join(const sort_expression &s)
Constructor for function symbol @fbag_join.
Definition bag1.h:1247
bool is_constructor_application(const atermpp::aterm &e)
Recogniser for application of @bag.
Definition bag1.h:124
bool is_zero_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @zero_.
Definition bag1.h:817
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @bag.
Definition bag1.h:78
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition bag1.h:1642
const core::identifier_string & constructor_name()
Generate identifier @bag.
Definition bag1.h:68
bool is_bag_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @bagcomp.
Definition bag1.h:282
bool is_set2bag_application(const atermpp::aterm &e)
Recogniser for application of Set2Bag.
Definition bag1.h:789
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:362
void make_zero_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @zero_.
Definition bag1.h:841
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition bag1.h:1630
void make_bag_fbag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @bagfbag.
Definition bag1.h:210
function_symbol bool2nat_function(const sort_expression &s)
Constructor for function symbol @Bool2Nat_.
Definition bag1.h:1185
void make_set2bag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Set2Bag.
Definition bag1.h:779
const core::identifier_string & union_name()
Generate identifier +.
Definition bag1.h:418
bool is_fbag_intersect_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_inter.
Definition bag1.h:1325
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:426
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition bag1.h:580
void make_bag_comprehension(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @bagcomp.
Definition bag1.h:272
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bag1.h:1618
void make_fbag_difference(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 @fbag_diff.
Definition bag1.h:1423
const core::identifier_string & count_name()
Generate identifier count.
Definition bag1.h:290
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 bag1.h:485
function_symbol nat2bool_function(const sort_expression &s)
Constructor for function symbol @Nat2Bool_.
Definition bag1.h:1123
bool is_one_function_application(const atermpp::aterm &e)
Recogniser for application of @one_.
Definition bag1.h:913
const core::identifier_string & difference_name()
Generate identifier -.
Definition bag1.h:588
bool is_bool2nat_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Bool2Nat_.
Definition bag1.h:1195
bool is_bag(const sort_expression &e)
Recogniser for sort expression Bag(s)
Definition bag1.h:55
container_sort bag(const sort_expression &s)
Constructor for sort expression Bag(S)
Definition bag1.h:44
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition bag1.h:628
bool is_fbag2fset_application(const atermpp::aterm &e)
Recogniser for application of @fbag2fset.
Definition bag1.h:1497
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition bag1.h:151
const core::identifier_string & in_name()
Generate identifier in.
Definition bag1.h:354
bool is_constructor_function_symbol(const atermpp::aterm &e)
Recogniser for function @bag.
Definition bag1.h:88
const core::identifier_string & bag_comprehension_name()
Generate identifier @bagcomp.
Definition bag1.h:228
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of count.
Definition bag1.h:346
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 bag1.h:655
const core::identifier_string & one_function_name()
Generate identifier @one_.
Definition bag1.h:859
bool is_add_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @add_.
Definition bag1.h:941
void make_constructor(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @bag.
Definition bag1.h:114
function_symbol zero_function(const sort_expression &s)
Constructor for function symbol @zero_.
Definition bag1.h:807
bool is_one_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @one_.
Definition bag1.h:879
function_symbol one_function(const sort_expression &s)
Constructor for function symbol @one_.
Definition bag1.h:869
function_symbol_vector bag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for bag.
Definition bag1.h:132
bool is_fbag_join_application(const atermpp::aterm &e)
Recogniser for application of @fbag_join.
Definition bag1.h:1297
bool is_monus_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @monus_.
Definition bag1.h:1069
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
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
Definition fbag1.h:43
function_symbol cons_(const sort_expression &s)
Constructor for function symbol @fbag_cons.
Definition fbag1.h:211
function_symbol empty(const sort_expression &s)
Constructor for function symbol {:}.
Definition fbag1.h:77
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fbag_cinsert.
Definition fbag1.h:277
function_symbol fset2fbag(const sort_expression &s)
Constructor for function symbol @fset2fbag.
Definition fbag1.h:471
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fset_cinsert.
Definition fset1.h:271
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 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 function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat1.h:140
const function_symbol & swap_zero_add()
Constructor for function symbol @swap_zero_add.
Definition nat1.h:1459
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
const function_symbol & swap_zero()
Constructor for function symbol @swap_zero.
Definition nat1.h:1395
const function_symbol & swap_zero_min()
Constructor for function symbol @swap_zero_min.
Definition nat1.h:1527
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:507
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:834
const function_symbol & swap_zero_monus()
Constructor for function symbol @swap_zero_monus.
Definition nat1.h:1595
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 true_function(const sort_expression &s)
Constructor for function symbol @true_.
Definition set1.h:717
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set1.h:42
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @set.
Definition set1.h:76
function_symbol false_function(const sort_expression &s)
Constructor for function symbol @false_.
Definition set1.h:655
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
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.
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:314
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.