mCRL2
Loading...
Searching...
No Matches
print.h
Go to the documentation of this file.
1// Author(s): Jeroen van der Wulp, Wieger Wesselink
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//
11
12#ifndef MCRL2_DATA_PRINT_H
13#define MCRL2_DATA_PRINT_H
14
19
20namespace mcrl2
21{
22
23namespace data
24{
25
26namespace detail {
27
28// Check that the argument, which must be of sort Pos, represents 1.
29inline
30bool is_one(const data_expression& x)
31{
32 assert(x.sort() == sort_pos::pos());
33#ifdef MCRL2_ENABLE_MACHINENUMBERS
35 (( is_machine_number(sort_pos::arg(x)) && atermpp::down_cast<machine_number>(sort_pos::arg(x)).value() == 1) ||
37 ) ||
39#else
41#endif
42}
43
44inline
46{
53#ifndef MCRL2_ENABLE_MACHINENUMBERS
56#endif
58 ;
59}
60
61inline bool look_through_numeric_casts(const data_expression& x, std::function<bool(const data_expression&)> f)
62{
63 if (is_numeric_cast(x))
64 {
65 return look_through_numeric_casts(atermpp::down_cast<application>(x)[0], f);
66 }
67 return f(x);
68}
69
70/* inline
71data_expression remove_numeric_casts(data_expression x)
72{
73 while (is_numeric_cast(x))
74 {
75 x = *atermpp::down_cast<application>(x).begin();
76 }
77 return x;
78} */
79
80inline
81bool is_plus(const application& x)
82{
84 x,
85 [](const data_expression& x)
90}
91
92inline
93bool is_minus(const application& x)
94{
96 x,
97 [](const data_expression& x)
100}
101
102inline
103bool is_mod(const application& x)
104{
106 x,
107 [](const data_expression& x)
108 { return sort_int::is_mod_application(x) ||
110}
111
112inline
113bool is_div(const application& x)
114{
116 x,
117 [](const data_expression& x)
118 { return sort_int::is_div_application(x) ||
120}
121
122#ifndef MCRL2_ENABLE_MACHINENUMBERS
123inline
124bool is_divmod(const application& x)
125{
127 x,
128 [](const data_expression& x)
129 { return sort_nat::is_divmod_application(x); });
130}
131#endif
132
133inline
135{
137 x,
138 [](const data_expression& x)
139 { return sort_real::is_divides_application(x); });
140}
141
142inline
144{
146}
147
148inline
150{
152}
153
154inline
156{
158}
159
160inline
162{
164}
165
166inline
168{
170}
171
172inline
173bool is_and(const application& x)
174{
176}
177
178inline
179bool is_or(const application& x)
180{
182}
183
184inline
186{
188}
189
190inline
192{
194}
195
196inline
197bool is_less(const application& x)
198{
200}
201
202inline
204{
206}
207
208inline
210{
212}
213
214inline
216{
218}
219
220inline
221bool is_in(const application& x)
222{
224}
225
226inline
227bool is_times(const application& x)
228{
230 x,
231 [](const data_expression& x)
232 { return sort_int::is_times_application(x); });
233}
234
235inline
237{
239}
240
241inline
243{
245}
246
247inline
249{
251}
252
253inline
254bool is_concat(const application& x)
255{
257}
258
259inline
261{
263 {
264 x = sort_list::right(x);
265 }
267}
268
269inline
271{
273 {
274 x = sort_list::left(x);
275 }
277}
278
279inline
280bool is_cons(const application& x)
281{
283}
284
285inline
286bool is_snoc(const application& x)
287{
289}
290
291} // namespace detail
292
293int precedence(const data_expression& x);
294
295inline
297{
298 // N.B. this code should match printing of a creal
300 {
301 const data_expression& numerator = sort_real::left(x);
302 const data_expression& denominator = sort_real::right(x);
303 // if (sort_pos::is_c1_function_symbol(denominator))
304 if (detail::is_one(denominator))
305 {
306 return precedence(numerator);
307 }
308 else
309 {
310 return precedence(sort_real::divides(numerator, sort_int::pos2int(denominator)));
311 }
312 }
313 else if (detail::is_implies(x))
314 {
315 return 2;
316 }
317 else if (detail::is_or(x))
318 {
319 return 3;
320 }
321 else if (detail::is_and(x))
322 {
323 return 4;
324 }
325 else if (detail::is_equal_to(x) ||
327 )
328 {
329 return 5;
330 }
331 else if ( detail::is_less(x)
335 || detail::is_in(x)
336 )
337 {
338 return 6;
339 }
340 else if (detail::is_cons(x))
341 {
342 return 7;
343 }
344 else if (detail::is_snoc(x))
345 {
346 return 8;
347 }
348 else if (detail::is_concat(x))
349 {
350 return 9;
351 }
352 else if ( detail::is_plus(x)
353 || detail::is_minus(x)
358 )
359 {
360 return 10;
361 }
362 else if ( detail::is_div(x)
363 || detail::is_mod(x)
364#ifndef MCRL2_ENABLE_MACHINENUMBERS
366#endif
368 )
369 {
370 return 11;
371 }
372 else if ( detail::is_times(x)
376 )
377 {
378 return 12;
379 }
381 {
382 return 13;
383 }
384 // TODO: add function application (there seems to be no recognizer for it)
385 return core::detail::max_precedence;
386}
387
388constexpr int precedence(const forall&) { return 1; }
389constexpr int precedence(const exists&) { return 1; }
390constexpr int precedence(const lambda&) { return 1; }
391constexpr int precedence(const set_comprehension&) { return core::detail::max_precedence; }
392constexpr int precedence(const bag_comprehension&) { return core::detail::max_precedence; }
393constexpr int precedence(const where_clause&) { return 0; }
394inline int precedence(const data_expression& x)
395{
396 if (data::is_application(x)) { return precedence(atermpp::down_cast<application>(x)); }
397 else if (data::is_forall(x)) { return precedence(atermpp::down_cast<forall>(x)); }
398 else if (data::is_exists(x)) { return precedence(atermpp::down_cast<exists>(x)); }
399 else if (data::is_lambda(x)) { return precedence(atermpp::down_cast<lambda>(x)); }
400 else if (data::is_set_comprehension(x)) { return precedence(atermpp::down_cast<set_comprehension>(x)); }
401 else if (data::is_bag_comprehension(x)) { return precedence(atermpp::down_cast<bag_comprehension>(x)); }
402 else if (data::is_where_clause(x)) { return precedence(atermpp::down_cast<where_clause>(x)); }
403 return core::detail::max_precedence;
404}
405
406inline
408{
410}
411
412inline
414{
415 if (!is_application(x))
416 {
417 return false;
418 }
419 const auto& x_ = atermpp::down_cast<application>(x);
420 return !detail::is_minus(x_) && !is_equal_to_application(x);
421}
422
423namespace detail
424{
425
426template <typename Derived>
427struct printer: public data::add_traverser_sort_expressions<core::detail::printer, Derived>
428{
430
431 using super::enter;
432 using super::leave;
433 using super::apply;
434 using super::derived;
435 using super::print_expression;
436 using super::print_unary_operand;
437 using super::print_list;
438
439 void print_unary_data_operation(const application& x, const std::string& op)
440 {
441 derived().print(op);
442 print_expression(x[0], precedence(x[0]) < precedence(x));
443 }
444
445 void print_binary_data_operation(const application& x, const data_expression& x1, const data_expression& x2, const std::string& op)
446 {
447 const int p = precedence(x);
448 const int p1 = precedence(x1);
449 const int p2 = precedence(x2);
450 print_expression(x1, (p1 < p) || (p1 == p && !is_left_associative(x)));
451 derived().print(op);
452 print_expression(x2, (p2 < p) || (p2 == p && !is_right_associative(x)));
453 }
454
455 void print_binary_data_operation(const application& x, const std::string& op)
456 {
457 const data_expression& x1 = x[0];
458 const data_expression& x2 = x[1];
459 print_binary_data_operation(x, x1, x2, op);
460 }
461
462 bool is_infix_operation(const application& x) const
463 {
464 if (x.size() != 2)
465 {
466 return false;
467 }
469 if (is_function_symbol(x.head()))
470 {
471 name = function_symbol(x.head()).name();
472 }
473 else if (is_untyped_identifier(x.head()))
474 {
475 name = untyped_identifier(x.head()).name();
476 }
477 else
478 {
479 return false;
480 }
481 return
482 (name == data::sort_bool::implies_name()) ||
483 (name == data::sort_bool::and_name()) ||
484 (name == data::sort_bool::or_name()) ||
485 data::detail::equal_symbol::is_symbol(name) ||
486 data::detail::not_equal_symbol::is_symbol(name) ||
487 data::detail::less_symbol::is_symbol(name) ||
488 data::detail::less_equal_symbol::is_symbol(name) ||
489 data::detail::greater_symbol::is_symbol(name) ||
490 data::detail::greater_equal_symbol::is_symbol(name) ||
491 (name == data::sort_list::in_name()) ||
492 (name == data::sort_list::cons_name()) ||
493 (name == data::sort_list::snoc_name()) ||
494 (name == data::sort_list::concat_name()) ||
495 (name == data::sort_real::plus_name()) ||
496 (name == data::sort_real::minus_name()) ||
497 (name == data::sort_set::union_name()) ||
498 (name == data::sort_fset::union_name()) ||
501 (name == data::sort_bag::union_name()) ||
502 (name == data::sort_fbag::union_name()) ||
505 (name == data::sort_int::div_name()) ||
506 (name == data::sort_int::mod_name()) ||
507 (name == data::sort_real::divides_name()) ||
508 (name == data::sort_int::times_name()) ||
512 }
513
514 core::identifier_string generate_identifier(const std::string& prefix, const data_expression& context) const
515 {
517 std::set<variable> variables = data::find_all_variables(context);
518 for (const variable& v: variables)
519 {
520 generator.add_identifier(v.name());
521 }
522 return generator(prefix);
523 }
524
525 template <typename Container>
526 void print_container(const Container& container,
527 int container_precedence = -1,
528 const std::string& separator = ", ",
529 const std::string& open_bracket = "(",
530 const std::string& close_bracket = ")"
531 )
532 {
533 for (auto i = container.begin(); i != container.end(); ++i)
534 {
535 if (i != container.begin())
536 {
537 derived().print(separator);
538 }
539 bool print_brackets = (container.size() > 1) && (precedence(*i) < container_precedence);
540 if (print_brackets)
541 {
542 derived().print(open_bracket);
543 }
544 derived().apply(*i);
545 if (print_brackets)
546 {
547 derived().print(close_bracket);
548 }
549 }
550 }
551
552 template <typename Variable>
553 void print_variable(const Variable& x, bool print_sort = false)
554 {
555 derived().apply(x);
556 if (print_sort)
557 {
558 derived().print(": ");
559 derived().apply(x.sort());
560 }
561 }
562
564 {
565 template <typename T>
566 sort_expression operator()(const T& t) const
567 {
568 return t.sort();
569 }
570 };
571
572 template <typename Container, typename SortAccessor>
573 void print_sorted_declarations(const Container& container,
574 bool print_sorts = true,
575 bool join_sorts = true,
576 bool maximally_shared = false,
577 const std::string& opener = "(",
578 const std::string& closer = ")",
579 const std::string& separator = ", ",
580 SortAccessor get_sort = get_sort_default()
581 )
582 {
583 auto first = container.begin();
584 auto last = container.end();
585 if (first == last)
586 {
587 return;
588 }
589
590 derived().print(opener);
591
592 if (maximally_shared)
593 {
594 typedef typename Container::value_type T;
595
596 // sort_map[s] will contain all elements t of container with t.sort() == s.
597 std::map<sort_expression, std::vector<T> > sort_map;
598
599 // sorts will contain all sort expressions s that appear as a key in sort_map,
600 // in the order they are encountered in container
601 std::vector<sort_expression> sorts;
602
603 for (auto i = container.begin(); i != container.end(); ++i)
604 {
605 if (sort_map.find(i->sort()) == sort_map.end())
606 {
607 sorts.push_back(i->sort());
608 }
609 sort_map[i->sort()].push_back(*i);
610 }
611
612 // do the actual printing
613 for (auto i = sorts.begin(); i != sorts.end(); ++i)
614 {
615 if (i != sorts.begin())
616 {
617 derived().print(separator);
618 }
619 const std::vector<T>& v = sort_map[*i];
620 print_list(v, "", "", ",");
621 derived().print(": ");
622 derived().apply(*i);
623 }
624 }
625 else
626 {
627 while (first != last)
628 {
629 if (first != container.begin())
630 {
631 derived().print(separator);
632 }
633
634 if (print_sorts && join_sorts)
635 {
636 // determine a consecutive interval [first, i) with elements of the same sorts
637 auto i = first;
638 do
639 {
640 ++i;
641 }
642
643 // print the elements of the interval [first, i)
644 while (i != last && i->sort() == first->sort());
645
646 for (auto j = first; j != i; ++j)
647 {
648 if (j != first)
649 {
650 derived().print(",");
651 }
652 derived().apply(*j);
653 }
654
655 // print the sort
656 if (print_sorts)
657 {
658 derived().print(": ");
659 derived().apply(get_sort(*first));
660 }
661
662 // update first
663 first = i;
664 }
665 else
666 {
667 derived().apply(*first);
668
669 // print the sort
670 if (print_sorts)
671 {
672 derived().print(": ");
673 derived().apply(get_sort(*first));
674 }
675
676 // update first
677 ++first;
678 }
679 }
680 }
681 derived().print(closer);
682 }
683
684 template <typename Container>
685 void print_variables(const Container& container,
686 bool print_sorts = true,
687 bool join_sorts = true,
688 bool maximally_shared = false,
689 const std::string& opener = "(",
690 const std::string& closer = ")",
691 const std::string& separator = ", "
692 )
693 {
694 print_sorted_declarations(container, print_sorts, join_sorts, maximally_shared, opener, closer, separator, get_sort_default());
695 }
696
697 template <typename Container>
698 void print_assignments(const Container& container,
699 bool print_lhs = true,
700 const std::string& opener = "",
701 const std::string& closer = "",
702 const std::string& separator = ", ",
703 const std::string& assignment_symbol = " = "
704 )
705 {
706 if (container.empty())
707 {
708 return;
709 }
710 derived().print(opener);
711 for (auto i = container.begin(); i != container.end(); ++i)
712 {
713 if (i != container.begin())
714 {
715 derived().print(separator);
716 }
717 if (print_lhs)
718 {
719 derived().apply(i->lhs());
720 derived().print(assignment_symbol);
721 }
722 derived().apply(i->rhs());
723 }
724 derived().print(closer);
725 }
726
727 template <typename T>
728 void print_condition(const T& x, const std::string& arrow = " -> ")
729 {
731 {
732 print_expression(x, true);
733 derived().print(arrow);
734 }
735 }
736
737 template <typename Container>
738 void print_sort_list(const Container& container,
739 const std::string& opener = "(",
740 const std::string& closer = ")",
741 const std::string& separator = ", "
742 )
743 {
744 if (container.empty())
745 {
746 return;
747 }
748 derived().print(opener);
749 for (auto i = container.begin(); i != container.end(); ++i)
750 {
751 if (i != container.begin())
752 {
753 derived().print(separator);
754 }
755 bool print_brackets = is_function_sort(*i);
756 if (print_brackets)
757 {
758 derived().print("(");
759 }
760 derived().apply(*i);
761 if (print_brackets)
762 {
763 derived().print(")");
764 }
765 }
766 derived().print(closer);
767 }
768
770 {
771 derived().print("[");
773 derived().print("]");
774 }
775
777 {
778 derived().print("{ ");
780 derived().print(" }");
781 }
782
784 {
785 derived().print("{ ");
787 while (i != x.end())
788 {
789 if (i != x.begin())
790 {
791 derived().print(", ");
792 }
793 derived().apply(*i++);
794 derived().print(": ");
795 derived().apply(*i++);
796 }
797 derived().print(" }");
798 }
799
801 {
802 derived().print("{ ");
803 print_variables(x.variables(), true, true, false, "", "", ", ");
804 derived().print(" | ");
805 derived().apply(x.body());
806 derived().print(" }");
807 }
808
810 {
811 return is_abstraction(x.head());
812 }
813
815 {
817 {
818 x = sort_list::right(x);
819 }
821 }
822
824 {
826 {
827 x = sort_list::left(x);
828 }
830 }
831
833 {
835 {
836 x = sort_fset::right(x);
837 }
839 }
840
843 {
845 {
846 x = sort_fbag::arg3(x);
847 }
849 }
850
852 {
853 return sort_pos::is_pos(x.sort())
854 || sort_nat::is_nat(x.sort())
855 || sort_int::is_int(x.sort())
856 || sort_real::is_real(x.sort());
857 }
858
860 {
861 return sort_pos::is_pos(x)
863 || sort_nat::is_nat(x)
864 || sort_int::is_int(x)
865 || sort_real::is_real(x);
866 }
867
869 {
871 }
872
874 {
876 }
877
879 {
881 }
882
884 {
886 }
887
889 {
891 }
892
894 {
896 }
897
899 {
900 data_expression_vector arguments;
902 {
903 arguments.push_back(sort_list::left(x));
904 x = sort_list::right(x);
905 }
906 derived().print("[");
907 print_container(arguments, 6);
908 derived().print("]");
909 }
910
912 {
913 data_expression_vector arguments;
915 {
916 arguments.insert(arguments.begin(), sort_list::right(x));
917 x = sort_list::left(x);
918 }
919 derived().print("[");
920 print_container(arguments, 7);
921 derived().print("]");
922 }
923
925 {
926 data_expression_vector arguments;
928 {
929 arguments.push_back(sort_fset::left(x));
930 x = sort_fset::right(x);
931 }
932 derived().print("{");
933 print_container(arguments, 6);
934 derived().print("}");
935 }
936
938 {
939 // TODO: check if this is the correct way to handle this case
942 {
943 derived().print("{:}");
944 }
945 else if (data::is_variable(y))
946 {
947 derived().print("@bagfbag(");
948 derived().apply(variable(y).name());
949 derived().print(")");
950 }
951 else
952 {
953 derived().apply(y);
954 }
955 }
956
958 {
959 sort_expression s = function_sort(sort_bag::left(x).sort()).domain().front(); // the sort of the bag elements
961 variable var(name, s);
962 data_expression body = number(sort_nat::nat(), "1");
964 {
966 }
967 derived().print("{ ");
968 print_variable(var, true);
969 derived().print(" | ");
970 derived().apply(body);
971 derived().print(" }");
972 }
973
975 {
976 sort_expression s = function_sort(sort_bag::left(x).sort()).domain().front(); // the sort of the bag elements
978 variable var(name, s);
980 data_expression body = left.body();
982 {
984 }
985 derived().print("{ ");
986 print_variables(left.variables(), true, true, false, "", "", ", ");
987 derived().print(" | ");
988 derived().apply(body);
989 derived().print(" }");
990 }
991
993 {
996 variable var(name, s);
997 data_expression body = sort_bag::left(x)(var);
999 {
1001 }
1002 derived().print("{ ");
1003 print_variable(var, true);
1004 derived().print(" | ");
1005 derived().apply(body);
1006 derived().print(" }");
1007 }
1008
1010 {
1011 std::vector<std::pair<data_expression, data_expression> > arguments;
1013 {
1015 {
1016 arguments.emplace_back(sort_fbag::arg1(x), sort_fbag::arg2(x));
1017 x = sort_fbag::arg3(x);
1018 }
1020 {
1021#ifdef MCRL2_ENABLE_MACHINENUMBERS
1022 arguments.emplace_back(sort_fbag::arg1(x), sort_nat::pos2nat(sort_fbag::arg2(x)));
1023#else
1024 arguments.emplace_back(sort_fbag::arg1(x), sort_nat::cnat(sort_fbag::arg2(x)));
1025#endif
1026 x = sort_fbag::arg3(x);
1027 }
1028 else // if (sort_fbag::is_fbagcinsert_application(x))
1029 {
1030 arguments.emplace_back(sort_fbag::arg1(x), sort_fbag::arg2(x));
1031 x = sort_fbag::arg3(x);
1032 }
1033 }
1034 print_list(arguments, "{", "}");
1035 }
1036
1038 {
1039 derived().print("!");
1040 derived().apply(sort_set::right(x));
1041 }
1042
1044 {
1046 {
1047 derived().print("{}");
1048 }
1049 else
1050 {
1051 derived().apply(sort_set::right(x));
1052 }
1053 }
1054
1056 {
1058 derived().print("{ ");
1059 print_variables(left.variables(), true, true, false, "", "", ", ");
1060 derived().print(" | ");
1061 derived().apply(left.body());
1062 derived().print(" }");
1063 }
1064
1065 void print_fset_set_operation(const data_expression& x, const std::string& op)
1066 {
1069
1070 // print lhs
1072 {
1073 derived().apply(sort_set::arg3(x));
1074 }
1076 {
1077 derived().print("!");
1078 derived().apply(sort_set::arg3(x));
1079 }
1080 else if (is_function_sort(sort_set::arg1(x).sort()))
1081 {
1082 const sort_expression sort = sort_set::arg1(x).sort();
1083 const sort_expression& s = atermpp::down_cast<function_sort>(sort).domain().front();
1085 variable var(name, s);
1087 derived().print("{ ");
1088 print_variable(var, true);
1089 derived().print(" | ");
1090 derived().apply(body);
1091 derived().print(" }");
1092 }
1093 else
1094 {
1095 // In this case the term is not well formed, for instance because it contains a "Rewritten@@term" function.
1096 // We print the residue as an aterm.
1097 derived().print(pp(atermpp::aterm(x)));
1098 return;
1099 }
1100
1101 // print operator
1102 derived().print(op);
1103
1104 // print rhs
1106 {
1107 derived().apply(sort_set::arg4(x));
1108 }
1110 {
1111 derived().print("!");
1112 derived().apply(sort_set::arg4(x));
1113 }
1114 else
1115 {
1118 variable var(name, s);
1120 derived().print("{ ");
1121 print_variable(var, true);
1122 derived().print(" | ");
1123 derived().apply(body);
1124 derived().print(" }");
1125 }
1126 }
1127
1129 {
1131 // TODO: check if this is the correct way to handle this case
1133 {
1136 variable var(name, s);
1137 data_expression body(sort_set::left(x)(var));
1138 derived().print("{ ");
1139 print_variable(var, true);
1140 derived().print(" | ");
1141 derived().apply(body);
1142 derived().print(" }");
1143 }
1144 else
1145 {
1148 variable var(name, s);
1149 data_expression lhs(sort_set::left(x)(var));
1150 data_expression rhs(sort_set::in(s, var, sort_set::set_fset(s, right)));
1151 data_expression body = not_equal_to(lhs, rhs);
1152 derived().print("{ ");
1153 print_variable(var, true);
1154 derived().print(" | ");
1155 derived().apply(body);
1156 derived().print(" }");
1157 }
1158 }
1159
1160 template <typename Abstraction>
1161 void print_abstraction(const Abstraction& x, const std::string& op)
1162 {
1163 derived().enter(x);
1164 derived().print(op + " ");
1165 print_variables(x.variables(), true, true, false, "", "", ", ");
1166 derived().print(". ");
1167 derived().apply(x.body());
1168 derived().leave(x);
1169 }
1170
1172 {
1173 // Add special handling of list/set/bag enumeration types. This case applies to printing
1174 // terms after parsing and before type checking.
1176 {
1178 return;
1179 }
1181 {
1183 return;
1184 }
1186 {
1188 return;
1189 }
1190
1191 if (is_infix_operation(x))
1192 {
1193 assert(detail::is_untyped(x));
1194 auto i = x.begin();
1195 data_expression left = *i++;
1196 data_expression right = *i;
1197 print_expression(left, false);
1198 derived().print(" ");
1199 derived().apply(x.head());
1200 derived().print(" ");
1201 print_expression(right, false);
1202 return;
1203 }
1204
1205 // print the head
1206 bool print_parentheses = is_abstraction(x.head());
1207 if (print_parentheses)
1208 {
1209 derived().print("(");
1210 }
1211 derived().apply(x.head());
1212 if (print_parentheses)
1213 {
1214 derived().print(")");
1215 }
1216
1217 // print the arguments
1218 print_parentheses = !x.empty();
1219 if (is_function_symbol(x.head()) && x.size() == 1)
1220 {
1221 std::string name(function_symbol(x.head()).name());
1222 if (name == "!" || name == "#")
1223 {
1224 print_parentheses = precedence(*x.begin()) < core::detail::max_precedence;
1225 }
1226 }
1227 if (print_parentheses)
1228 {
1229 derived().print("(");
1230 }
1231 print_container(x);
1232 if (print_parentheses)
1233 {
1234 derived().print(")");
1235 }
1236 }
1237
1238 // N.B. This is interpreted as the bag element 'x.first: x.second'
1239 void apply(const std::pair<data_expression, data_expression>& x)
1240 {
1241 derived().apply(x.first);
1242 derived().print(": ");
1243 derived().apply(x.second);
1244 }
1245
1246 // TODO: this code should be generated!
1248 {
1249 derived().enter(x);
1251 {
1252 derived().apply(data::list_container(atermpp::aterm(x)));
1253 }
1254 else if (data::is_set_container(x))
1255 {
1256 derived().apply(data::set_container(atermpp::aterm(x)));
1257 }
1258 else if (data::is_bag_container(x))
1259 {
1260 derived().apply(data::bag_container(atermpp::aterm(x)));
1261 }
1262 else if (data::is_fset_container(x))
1263 {
1264 derived().apply(data::fset_container(atermpp::aterm(x)));
1265 }
1266 else if (data::is_fbag_container(x))
1267 {
1268 derived().apply(data::fbag_container(atermpp::aterm(x)));
1269 }
1270 derived().leave(x);
1271 }
1272
1274 {
1275 derived().enter(x);
1276 derived().apply(x.lhs());
1277 derived().print(" = ");
1278 derived().apply(x.rhs());
1279 derived().leave(x);
1280 }
1281
1282 // variable lists have their own notation
1284 {
1285 derived().enter(x);
1286 print_list(x, "", "", ", ", false);
1287 derived().leave(x);
1288 }
1289
1291 {
1292 derived().enter(x);
1293 derived().apply(x.name());
1294 print_list(x.arguments(), "(", ")", ", ");
1295 derived().leave(x);
1296 }
1297
1299 {
1300 derived().enter(x);
1301 derived().apply(x.lhs());
1302 derived().print("=");
1303 derived().apply(x.rhs());
1304 derived().leave(x);
1305 }
1306
1308 {
1309 derived().enter(x);
1310 derived().leave(x);
1311 }
1312
1314 {
1315 derived().enter(x);
1316 derived().leave(x);
1317 }
1318
1320 {
1321 derived().enter(x);
1322 derived().leave(x);
1323 }
1324
1326 {
1327 derived().enter(x);
1328 derived().leave(x);
1329 }
1330
1332 {
1333 derived().enter(x);
1334 derived().leave(x);
1335 }
1336
1338 {
1339 derived().enter(x);
1340 derived().leave(x);
1341 }
1342
1344 {
1345 derived().enter(x);
1347 {
1348 derived().apply(x.name());
1349 derived().print(": ");
1350 }
1351 derived().apply(x.sort());
1352 derived().leave(x);
1353 }
1354
1356 {
1357 derived().enter(x);
1358 derived().apply(x.name());
1359 print_list(x.arguments(), "(", ")", ", ");
1361 {
1362 derived().print("?");
1363 derived().apply(x.recogniser());
1364 }
1365 derived().leave(x);
1366 }
1367
1368 void apply(const data::alias& x)
1369 {
1370 derived().enter(x);
1371 derived().apply(x.name());
1372 derived().print(" = ");
1373 derived().apply(x.reference());
1374 derived().leave(x);
1375 }
1376
1378 {
1379 derived().enter(x);
1380 derived().print("List");
1381 derived().leave(x);
1382 }
1383
1385 {
1386 derived().enter(x);
1387 derived().print("Set");
1388 derived().leave(x);
1389 }
1390
1392 {
1393 derived().enter(x);
1394 derived().print("Bag");
1395 derived().leave(x);
1396 }
1397
1399 {
1400 derived().enter(x);
1401 derived().print("FSet");
1402 derived().leave(x);
1403 }
1404
1406 {
1407 derived().enter(x);
1408 derived().print("FBag");
1409 derived().leave(x);
1410 }
1411
1413 {
1414 derived().enter(x);
1415 derived().apply(x.name());
1416 derived().leave(x);
1417 }
1418
1420 {
1421 derived().enter(x);
1422 derived().apply(x.container_name());
1423 derived().print("(");
1424 derived().apply(x.element_sort());
1425 derived().print(")");
1426 derived().leave(x);
1427 }
1428
1430 {
1431 derived().enter(x);
1432 print_list(x.constructors(), "struct ", "", " | ");
1433 derived().leave(x);
1434 }
1435
1437 {
1438 derived().enter(x);
1439 print_sort_list(x.domain(), "", " -> ", " # ");
1440 derived().apply(x.codomain());
1441 derived().leave(x);
1442 }
1443
1445 {
1446 derived().enter(x);
1447 derived().print("untyped_sort");
1448 derived().leave(x);
1449 }
1450
1452 {
1453 derived().enter(x);
1454 derived().print("@untyped_possible_sorts[");
1455 derived().apply(x.sorts());
1456 derived().print("]");
1457 derived().leave(x);
1458 }
1459
1461 {
1462 derived().enter(x);
1463 derived().print("@s");
1464 derived().apply(x.value());
1465 derived().leave(x);
1466 }
1467
1469 {
1470 derived().enter(x);
1471 derived().apply(x.name());
1472 derived().leave(x);
1473 }
1474
1475 void apply(const data::variable& x)
1476 {
1477 derived().enter(x);
1478 derived().apply(x.name());
1479 derived().leave(x);
1480 }
1481
1483 {
1484 derived().enter(x);
1486 {
1487 derived().print("0");
1488 }
1490 {
1491 derived().print("1");
1492 }
1494 {
1495 derived().print("{:}");
1496 }
1498 {
1499 derived().print("{}");
1500 }
1501 else
1502 {
1503 derived().print(x.name());
1504 }
1505 derived().leave(x);
1506 }
1507
1509 {
1510 derived().enter(x);
1511
1512 //-------------------------------------------------------------------//
1513 // bool
1514 //-------------------------------------------------------------------//
1515
1517 {
1519 }
1521 {
1522 print_binary_data_operation(x, " && ");
1523 }
1524 else if (sort_bool::is_or_application(x))
1525 {
1526 print_binary_data_operation(x, " || ");
1527 }
1529 {
1530 print_binary_data_operation(x, " => ");
1531 }
1532
1533 //-------------------------------------------------------------------//
1534 // data
1535 //-------------------------------------------------------------------//
1536
1538 {
1539 print_binary_data_operation(x, " == ");
1540 }
1542 {
1543 print_binary_data_operation(x, " != ");
1544 }
1545 else if (data::is_if_application(x))
1546 {
1547 // TODO: is this correct?
1549 }
1550 else if (data::is_less_application(x))
1551 {
1553 }
1555 {
1556 print_binary_data_operation(x, " <= ");
1557 }
1558 else if (data::is_greater_application(x))
1559 {
1561 }
1563 {
1564 print_binary_data_operation(x, " >= ");
1565 }
1566
1567#ifdef MCRL2_ENABLE_MACHINENUMBERS
1568 //-------------------------------------------------------------------//
1569 // machine_word
1570 //-------------------------------------------------------------------//
1571
1573 {
1574 derived().print(std::to_string(sort_machine_word::detail::zero_word().value()));
1575 }
1577 {
1578 derived().print(std::to_string(sort_machine_word::detail::one_word().value()));
1579 }
1581 {
1582 derived().print(std::to_string(sort_machine_word::detail::max_word().value()));
1583 }
1585 {
1586 derived().print("((");
1587 derived().apply(sort_machine_word::arg(x));
1588 derived().print(" + 1) mod ");
1589 derived().print(max_machine_number_string());
1590 derived().print(" )");
1591 }
1593 {
1594 derived().print("((");
1595 derived().apply(sort_machine_word::left(x));
1596 derived().print(" + ");
1597 derived().apply(sort_machine_word::right(x));
1598 derived().print(") mod ");
1599 derived().print(max_machine_number_string());
1600 derived().print(" )");
1601 }
1603 {
1604 derived().print("((");
1605 derived().apply(sort_machine_word::left(x));
1606 derived().print(" + ");
1607 derived().apply(sort_machine_word::right(x));
1608 derived().print(") div ");
1609 derived().print(max_machine_number_string());
1610 derived().print(" )");
1611 }
1613 {
1614 derived().print("((");
1615 derived().apply(sort_machine_word::left(x));
1616 derived().print(" * ");
1617 derived().apply(sort_machine_word::right(x));
1618 derived().print(") mod ");
1619 derived().print(max_machine_number_string());
1620 derived().print(" )");
1621 }
1623 {
1624 derived().print("((");
1625 derived().apply(sort_machine_word::left(x));
1626 derived().print(" * ");
1627 derived().apply(sort_machine_word::right(x));
1628 derived().print(") div ");
1629 derived().print(max_machine_number_string());
1630 derived().print(" )");
1631 }
1632 /* else if (sort_machine_word::is_minus_word_application(x))
1633 {
1634 derived().print("(if(");
1635 derived().print_binary_operation(x, " >= ");
1636 derived().print(", ");
1637 derived().print_binary_operation(x, " - ");
1638 derived().print(", ");
1639 derived().print(max_machine_number_string());
1640 derived().print(" + ");
1641 derived().print_binary_operation(x, " - ");
1642 derived().print(")");
1643 }
1644 else if (sort_machine_word::is_div_word_application(x))
1645 {
1646 derived().print_binary_operation(x, " div ");
1647 }
1648 else if (sort_machine_word::is_mod_word_application(x))
1649 {
1650 derived().print_binary_operation(x, " mod ");
1651 } */
1652
1653/* TODO: Handle the following cases.
1654
1655 @div_doubleword <"div_doubleword">: @word <"arg1"> # @word <"arg2"> # @word <"arg3"> -> @word
1656 @div_double_doubleword <"div_double_doubleword">: @word <"arg1"> # @word <"arg2"> # @word <"arg3"> # @word <"arg4"> -> @word
1657 @div_triple_doubleword <"div_triple_doubleword">: @word <"arg1"> # @word <"arg2"> # @word <"arg3"> # @word <"arg4"> # @word <"arg5"> -> @word
1658 @mod_doubleword <"mod_doubleword">: @word <"arg1"> # @word <"arg2"> # @word <"arg3"> -> @word
1659 @sqrt_doubleword <"sqrt_doubleword">: @word <"arg1"> # @word <"arg2"> -> @word
1660 @sqrt_tripleword <"sqrt_tripleword">: @word <"arg1"> # @word <"arg2"> # @word <"arg3"> -> @word
1661 @sqrt_tripleword_overflow <"sqrt_tripleword_overflow">: @word <"arg1"> # @word <"arg2"> # @word <"arg3"> -> @word
1662 @sqrt_quadrupleword <"sqrt_quadrupleword">: @word <"arg1"> # @word <"arg2"> # @word <"arg3"> # @word <"arg4"> -> @word
1663 @sqrt_quadrupleword_overflow <"sqrt_quadrupleword_overflow">: @word <"arg1"> # @word <"arg2"> # @word <"arg3"> # @word <"arg4"> -> @word
1664 @pred_word <"pred_word">: @word <"arg"> ->@word
1665*/
1666
1667
1668#endif
1669
1670 //-------------------------------------------------------------------//
1671 // pos
1672 //-------------------------------------------------------------------//
1673
1674#ifdef MCRL2_ENABLE_MACHINENUMBERS
1676 {
1678 }
1680 {
1681 derived().apply(sort_pos::arg(x));
1682 }
1684 {
1685 derived().print(max_machine_number_string() + "* (");
1686 derived().apply(sort_pos::arg1(x));
1687 derived().print(") + ");
1688 derived().apply(sort_pos::arg2(x));
1689 }
1690#else
1692 {
1694 {
1696 }
1697 else
1698 {
1699 std::vector<char> number = data::detail::string_to_vector_number("1");
1700 derived().apply(detail::reconstruct_pos_mult(x, number));
1701 }
1702 }
1703#endif
1704 // TODO: handle @pospred
1706 {
1708 }
1710 {
1711#ifdef MCRL2_ENABLE_MACHINENUMBERS
1712 const data_expression& x1 = sort_pos::left(x);
1713 const data_expression& x2 = sort_pos::right(x);
1714 derived().apply(sort_pos::plus(x1, x2));
1715#else
1716 const data_expression& b = sort_pos::arg1(x);
1717 const data_expression& x1 = sort_pos::arg2(x);
1718 const data_expression& x2 = sort_pos::arg3(x);
1719 if (b == data::sort_bool::true_())
1720 {
1721 derived().apply(sort_pos::succ(sort_pos::plus(x1, x2)));
1722 }
1723 else if (b == sort_bool::false_())
1724 {
1725 derived().apply(sort_pos::plus(x1, x2));
1726 }
1727 else
1728 {
1729 derived().apply(if_(b, x1, x2));
1730 }
1731#endif
1732 }
1734 {
1736 }
1737 // TODO: handle @powerlog2
1738
1739 //-------------------------------------------------------------------//
1740 // natpair
1741 //-------------------------------------------------------------------//
1742
1743#ifdef MCRL2_ENABLE_MACHINENUMBERS
1745 {
1746 // TODO: verify if this is the correct way of dealing with first/divmod
1749 {
1751 }
1752 else
1753 {
1754 print_expression(sort_nat::left(y), true); // Removed left_precedence(y) and replaced it with true, which may be undesireable. Happens 3x more below.
1755 derived().print(" div ");
1756 print_expression(sort_nat::right(y), true);
1757 }
1758 }
1760 {
1761 // TODO: verify if this is the correct way of dealing with last/divmod
1764 {
1766 }
1767 else
1768 {
1769 print_expression(sort_nat::left(y), true);
1770 derived().print(" mod ");
1771 print_expression(sort_nat::right(y), true);
1772 }
1773 }
1774#else
1776 {
1777 // TODO: verify if this is the correct way of dealing with first/divmod
1778 const auto& y = atermpp::down_cast<application>(sort_nat::arg(x));
1780 {
1782 }
1783 else
1784 {
1785 print_binary_data_operation(y, " div ");
1786 }
1787 }
1789 {
1790 // TODO: verify if this is the correct way of dealing with last/divmod
1791 const auto& y = atermpp::down_cast<application>(sort_nat::arg(x));
1793 {
1795 }
1796 else
1797 {
1798 print_binary_data_operation(y, " mod ");
1799 }
1800 }
1801#endif
1802
1803 //-------------------------------------------------------------------//
1804 // nat
1805 //-------------------------------------------------------------------//
1806
1807#ifdef MCRL2_ENABLE_MACHINENUMBERS
1809 {
1811 }
1813 {
1814 derived().apply(sort_nat::arg(x));
1815 }
1817 {
1818 derived().print("(" + max_machine_number_string() + "*");
1819 derived().apply(sort_nat::arg1(x));
1820 derived().print(") + ");
1821 derived().apply(sort_nat::arg2(x));
1822 }
1823#else
1825 {
1826 derived().apply(sort_nat::arg(x));
1827 }
1828#endif
1830 {
1831 derived().apply(*x.begin());
1832 }
1833 // TODO: handle @dub
1834 // TODO: handle @dubsucc
1836 {
1838 }
1839 // TODO: handle @gtesubtb
1841 {
1843 }
1844 else if (sort_nat::is_div_application(x))
1845 {
1847 }
1848 else if (sort_nat::is_mod_application(x))
1849 {
1851 }
1852 // TODO: handle @monus
1853 // TODO: handle @swap_zero*
1854 // TODO: handle @sqrt_nat
1855
1856 //-------------------------------------------------------------------//
1857 // int
1858 //-------------------------------------------------------------------//
1859
1861 {
1862 derived().apply(sort_int::arg(x));
1863 }
1865 {
1866 derived().apply(sort_int::negate(sort_int::arg(x)));
1867 }
1869 {
1870 derived().apply(*x.begin());
1871 }
1873 {
1874 derived().apply(sort_int::arg(x));
1875 }
1877 {
1879 }
1881 {
1883 }
1885 {
1887 }
1889 {
1891 }
1892 else if (sort_int::is_div_application(x))
1893 {
1895 }
1896 else if (sort_int::is_mod_application(x))
1897 {
1899 }
1900
1901 //-------------------------------------------------------------------//
1902 // real
1903 //-------------------------------------------------------------------//
1904
1906 {
1907 data_expression numerator = sort_real::left(x);
1908 const data_expression& denominator = sort_real::right(x);
1909 if (detail::is_one(denominator))
1910 {
1911 derived().apply(numerator);
1912 }
1913 else
1914 {
1916 }
1917 }
1919 {
1920 derived().apply(*x.begin());
1921 }
1923 {
1924 derived().apply(*x.begin());
1925 }
1927 {
1928 derived().apply(*x.begin());
1929 }
1931 {
1933 }
1935 {
1937 }
1939 {
1941 }
1943 {
1945 }
1947 {
1949 }
1951 {
1952 derived().apply(sort_real::divides(sort_real::left(x),sort_real::right(x)));
1953 }
1955 {
1957 }
1958 // TODO: handle @redfrachlp
1959
1960 //-------------------------------------------------------------------//
1961 // list
1962 //-------------------------------------------------------------------//
1963
1965 {
1967 }
1969 {
1970 if (is_cons_list(x))
1971 {
1972 print_cons_list(x);
1973 }
1974 else
1975 {
1976 print_binary_data_operation(x, " |> ");
1977 }
1978 }
1979 else if (sort_list::is_in_application(x))
1980 {
1981 print_binary_data_operation(x, " in ");
1982 }
1984 {
1985 derived().print("#");
1986 print_unary_operand(x, sort_list::arg(x));
1987 }
1989 {
1990 if (is_snoc_list(x))
1991 {
1992 print_snoc_list(x);
1993 }
1994 else
1995 {
1996 print_binary_data_operation(x, " <| ");
1997 }
1998 }
2000 {
2001 print_binary_data_operation(x, " ++ ");
2002 }
2004 {
2006 }
2007
2008 //-------------------------------------------------------------------//
2009 // set
2010 //-------------------------------------------------------------------//
2011
2013 {
2014 if (is_fset_true(x))
2015 {
2016 print_fset_true(x);
2017 }
2018 else if (is_fset_false(x))
2019 {
2021 }
2022 else if (is_fset_lambda(x))
2023 {
2025 }
2026 else
2027 {
2029 }
2030 }
2032 {
2035 {
2036 derived().print("{}");
2037 }
2038 else if (data::is_variable(y))
2039 {
2040 derived().print("@setfset(");
2041 derived().apply(variable(y).name());
2042 derived().print(")");
2043 }
2044 else
2045 {
2046 derived().apply(y);
2047 }
2048 }
2050 {
2053 variable var(name, s);
2054 data_expression body(sort_set::arg(x)(var));
2055 derived().print("{ ");
2056 print_variable(var, true);
2057 derived().print(" | ");
2058 derived().apply(body);
2059 derived().print(" }");
2060 }
2061 else if (sort_set::is_in_application(x))
2062 {
2063 print_binary_data_operation(x, " in ");
2064 }
2066 {
2068 }
2070 {
2072 }
2074 {
2076 }
2078 {
2080 }
2082 {
2083 print_fset_set_operation(x, " + ");
2084 }
2086 {
2087 print_fset_set_operation(x, " * ");
2088 }
2089
2090 //-------------------------------------------------------------------//
2091 // fset
2092 //-------------------------------------------------------------------//
2093
2094 else if (is_fset_cons_list(x))
2095 {
2097 }
2098 else if (sort_fset::is_in_application(x))
2099 {
2100 print_binary_data_operation(x, " in ");
2101 }
2103 {
2104 derived().apply(sort_fset::left(x));
2105 derived().print(" - ");
2106 derived().apply(sort_fset::right(x));
2107 }
2109 {
2110 derived().apply(sort_fset::left(x));
2111 derived().print(" + ");
2112 derived().apply(sort_fset::right(x));
2113 }
2115 {
2116 derived().apply(sort_fset::left(x));
2117 derived().print(" * ");
2118 derived().apply(sort_fset::right(x));
2119 }
2121 {
2122 derived().print("#");
2123 derived().apply(sort_fset::arg(x));
2124 }
2125
2126 //-------------------------------------------------------------------//
2127 // bag
2128 //-------------------------------------------------------------------//
2129
2131 {
2132 if (is_fbag_zero(x))
2133 {
2134 print_fbag_zero(x);
2135 }
2136 else if (is_fbag_one(x))
2137 {
2138 print_fbag_one(x);
2139 }
2140 else if (is_fbag_lambda(x))
2141 {
2143 }
2144 else
2145 {
2147 }
2148 }
2150 {
2153 {
2154 derived().print("{:}");
2155 }
2156 else if (data::is_variable(y))
2157 {
2158 derived().print("@bagfbag(");
2159 derived().apply(variable(y).name());
2160 derived().print(")");
2161 }
2162 else
2163 {
2164 derived().apply(y);
2165 }
2166 }
2168 {
2171 variable var(name, s);
2172 data_expression body(sort_bag::arg(x)(var));
2173 derived().print("{ ");
2174 print_variable(var, true);
2175 derived().print(" | ");
2176 derived().apply(body);
2177 derived().print(" }");
2178 }
2179 else if (sort_bag::is_in_application(x))
2180 {
2181 print_binary_data_operation(x, " in ");
2182 }
2184 {
2186 }
2188 {
2190 }
2192 {
2194 }
2195
2196 //-------------------------------------------------------------------//
2197 // fbag
2198 //-------------------------------------------------------------------//
2199
2200 // cons / insert / cinsert
2201 else if (is_fbag_cons_list(x))
2202 {
2204 }
2205 else if (sort_fbag::is_in_application(x))
2206 {
2207 print_binary_data_operation(x, " in ");
2208 }
2210 {
2212 }
2214 {
2216 }
2217
2219 {
2221 }
2223 {
2224 derived().print("#");
2225 derived().apply(sort_fbag::arg(x));
2226 }
2227
2228 //-------------------------------------------------------------------//
2229 // function update
2230 //-------------------------------------------------------------------//
2232 {
2236 bool print_parentheses = is_abstraction(x1);
2237 if (print_parentheses)
2238 {
2239 derived().print("(");
2240 }
2241 derived().apply(x1);
2242 if (print_parentheses)
2243 {
2244 derived().print(")");
2245 }
2246 derived().print("[");
2247 derived().apply(x2);
2248 derived().print(" -> ");
2249 derived().apply(x3);
2250 derived().print("]");
2251 }
2252
2253 //-------------------------------------------------------------------//
2254 // abstraction
2255 //-------------------------------------------------------------------//
2256 else if (is_abstraction_application(x))
2257 {
2258 if (!x.empty()) {
2259 derived().print("(");
2260 }
2261 derived().apply(x.head());
2262 if (!x.empty())
2263 {
2264 derived().print(")(");
2265 }
2266 print_container(x);
2267 if (!x.empty())
2268 {
2269 derived().print(")");
2270 }
2271 }
2272
2273 //-------------------------------------------------------------------//
2274 // function application
2275 //-------------------------------------------------------------------//
2276 else
2277 {
2279 }
2280 derived().leave(x);
2281 }
2282
2283 void apply(const machine_number& x)
2284 {
2285 derived().print(std::to_string(x.value()));
2286 }
2287
2289 {
2290 derived().enter(x);
2291 derived().apply(x.body());
2292 derived().print(" whr ");
2293 const assignment_expression_list& declarations = x.declarations();
2294 for (assignment_expression_list::const_iterator i = declarations.begin(); i != declarations.end(); ++i)
2295 {
2296 if (i != declarations.begin())
2297 {
2298 derived().print(", ");
2299 }
2300 derived().apply(*i);
2301 }
2302 derived().print(" end");
2303 derived().leave(x);
2304 }
2305
2306 void apply(const data::forall& x)
2307 {
2308 print_abstraction(x, "forall");
2309 }
2310
2311 void apply(const data::exists& x)
2312 {
2313 print_abstraction(x, "exists");
2314 }
2315
2316 void apply(const data::lambda& x)
2317 {
2318 print_abstraction(x, "lambda");
2319 }
2320
2322 {
2323 derived().enter(x);
2325 derived().apply(x.lhs());
2326 derived().print(" = ");
2327 derived().apply(x.rhs());
2328 derived().leave(x);
2329 }
2330
2331 // Adds variables v and function symbols f to variable_map and function_symbol_names respectively.
2333 std::vector<variable>& variables,
2334 std::map<core::identifier_string, variable>& variable_map,
2335 std::set<core::identifier_string>& function_symbol_names
2336 )
2337 {
2338 for (const function_symbol& f: data::find_function_symbols(eqn))
2339 {
2340 function_symbol_names.insert(f.name());
2341 }
2342 for (const variable& v: eqn.variables())
2343 {
2344 std::pair<std::map<core::identifier_string, variable>::iterator, bool> k = variable_map.insert(std::make_pair(v.name(), v));
2345 if (k.second) // new variable encountered
2346 {
2347 variables.push_back(v);
2348 }
2349 }
2350 }
2351
2353 const std::map<core::identifier_string, variable>& variable_map
2354 )
2355 {
2356 for (const variable& v: eqn.variables())
2357 {
2358 auto j = variable_map.find(v.name());
2359 if (j != variable_map.end() && v != j->second)
2360 {
2361 return true;
2362 }
2363 }
2364 return false;
2365 }
2366
2372 template <typename Iter>
2373 Iter find_conflicting_equation(Iter first, Iter last, std::vector<variable>& variables)
2374 {
2375 std::map<core::identifier_string, variable> variable_map;
2376 std::set<core::identifier_string> function_symbol_names;
2377 for (Iter i = first; i != last; ++i)
2378 {
2379 if (has_conflict(*i, variable_map))
2380 {
2381 return i;
2382 }
2383 else
2384 {
2385 update_mappings(*i, variables, variable_map, function_symbol_names);
2386 }
2387 }
2388 return last; // no conflict found
2389 }
2390
2391 template <typename AliasContainer, typename SortContainer>
2392 void print_sort_declarations(const AliasContainer& aliases,
2393 const SortContainer& sorts,
2394 const std::string& opener = "(",
2395 const std::string& closer = ")",
2396 const std::string& separator = ", "
2397 )
2398 {
2399 if (aliases.empty() && sorts.empty())
2400 {
2401 return;
2402 }
2403 bool first_element = true;
2404 derived().print(opener);
2405
2406 // print sorts
2407 for (auto i = sorts.begin(); i != sorts.end(); ++i)
2408 {
2409 if (!first_element)
2410 {
2411 derived().print(separator);
2412 }
2413 derived().apply(*i);
2414 first_element = false;
2415 }
2416
2417 // print aliases
2418 for (auto i = aliases.begin(); i != aliases.end(); ++i)
2419 {
2420 if (!first_element)
2421 {
2422 derived().print(separator);
2423 }
2424 derived().apply(*i);
2425 first_element = false;
2426 }
2427
2428 derived().print(closer);
2429 }
2430
2431 template <typename Container>
2432 void print_equations(const Container& equations,
2433 const data_specification& data_spec,
2434 const std::string& opener = "(",
2435 const std::string& closer = ")",
2436 const std::string& separator = ", "
2437 )
2438 {
2439 auto first = equations.begin();
2440 auto last = equations.end();
2441
2442 Container normalized_equations = equations;
2443 data::normalize_sorts(normalized_equations, data_spec);
2444
2445 while (first != last)
2446 {
2447 std::vector<variable> variables;
2448 auto i = find_conflicting_equation(first, last, variables);
2449 print_variables(variables, true, true, true, "var ", ";\n", ";\n ");
2450
2451 // N.B. We print normalized equations instead of user defined equations.
2452 // print_list(std::vector<data_equation>(first, i), opener, closer, separator);
2453 auto first1 = normalized_equations.begin() + (first - equations.begin());
2454 auto i1 = normalized_equations.begin() + (i - equations.begin());
2455 print_list(std::vector<data_equation>(first1, i1), opener, closer, separator);
2456
2457 first = i;
2458 }
2459 }
2460
2462 {
2463 derived().enter(x);
2464 print_sort_declarations(x.user_defined_aliases(), x.user_defined_sorts(), "sort ", ";\n\n", ";\n ");
2465 print_sorted_declarations(x.user_defined_constructors(), true, true, false, "cons ",";\n\n", ";\n ", get_sort_default());
2466 print_sorted_declarations(x.user_defined_mappings(), true, true, false, "map ",";\n\n", ";\n ", get_sort_default());
2467 print_equations(x.user_defined_equations(), x, "eqn ", ";\n\n", ";\n ");
2468 derived().leave(x);
2469 }
2470
2471 // Override, because there are set/bag/setbag comprehension classes that exist after parsing and before type checking.
2473 {
2474 derived().enter(x);
2475 if (data::is_forall(x))
2476 {
2477 derived().apply(atermpp::down_cast<data::forall>(x));
2478 }
2479 else if (data::is_exists(x))
2480 {
2481 derived().apply(atermpp::down_cast<data::exists>(x));
2482 }
2483 else if (data::is_lambda(x))
2484 {
2485 derived().apply(atermpp::down_cast<data::lambda>(x));
2486 }
2487 else if (data::is_set_comprehension(x))
2488 {
2490 }
2491 else if (data::is_bag_comprehension(x))
2492 {
2494 }
2496 {
2498 }
2499 derived().leave(x);
2500 }
2501};
2502
2503} // namespace detail
2504
2507{
2508 template <typename T>
2509 void operator()(const T& x, std::ostream& out)
2510 {
2511 core::detail::apply_printer<data::detail::printer> printer(out);
2512 printer.apply(x);
2513 }
2514};
2515
2517template <typename T>
2518std::string pp(const T& x)
2519{
2520 std::ostringstream out;
2521 stream_printer()(x, out);
2522 return out.str();
2523}
2524
2525} // namespace data
2526
2527} // namespace mcrl2
2528
2529#endif
Term containing a string.
bool empty() const
Returns true if the term has no arguments.
Definition aterm.h:158
Iterator for term_appl.
Iterator for term_list.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:239
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
\brief A sort alias
Definition alias.h:26
const basic_sort & name() const
Definition alias.h:52
const sort_expression & reference() const
Definition alias.h:57
An application of a data expression to a number of arguments.
const_iterator end() const
Returns an iterator pointing past the last argument of the application.
const_iterator begin() const
Returns an iterator pointing to the first argument of the application.
const data_expression & head() const
Get the function at the head of this expression.
std::size_t size() const
\brief Assignment of a data expression to a variable
Definition assignment.h:91
const data_expression & rhs() const
Definition assignment.h:122
const variable & lhs() const
Definition assignment.h:117
\brief Binder for bag comprehension
universal quantification.
\brief Container type for bags
\brief A basic sort
Definition basic_sort.h:26
const core::identifier_string & name() const
Definition basic_sort.h:57
\brief A container sort
const container_type & container_name() const
const sort_expression & element_sort() const
\brief Container type
\brief A data equation
const data_expression & lhs() const
const data_expression & condition() const
const data_expression & rhs() const
const variable_list & variables() const
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
const_iterator end() const
const_iterator begin() const
const function_symbol_vector & user_defined_constructors() const
Gets the constructors defined by the user, excluding those that are system defined.
const function_symbol_vector & user_defined_mappings() const
Gets all user defined mappings in this specification.
const data_equation_vector & user_defined_equations() const
Gets all user defined equations.
\brief Binder for existential quantification
existential quantification.
Definition exists.h:26
\brief Container type for finite bags
\brief Binder for universal quantification
universal quantification.
Definition forall.h:26
\brief Container type for finite sets
\brief A function sort
const sort_expression & codomain() const
const sort_expression_list & domain() const
\brief A function symbol
const core::identifier_string & name() const
const sort_expression & sort() const
\brief Binder for lambda abstraction
function symbol.
Definition lambda.h:27
\brief Container type for lists
\brief A machine number
std::size_t value() const
\brief Binder for set comprehension
universal quantification.
\brief Container type for sets
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
\brief A sort expression
const basic_sort_vector & user_defined_sorts() const
Gets all sorts defined by a user (excluding the system defined sorts).
const alias_vector & user_defined_aliases() const
Gets the user defined aliases.
\brief An argument of a constructor of a structured sort
\brief A constructor for a structured sort
const core::identifier_string & name() const
const core::identifier_string & recogniser() const
const structured_sort_constructor_argument_list & arguments() const
const structured_sort_constructor_list & constructors() const
const core::identifier_string & name() const
const data_expression_list & arguments() const
\brief Assignment of a data expression to a string
Definition assignment.h:182
const core::identifier_string & lhs() const
Definition assignment.h:213
const data_expression & rhs() const
Definition assignment.h:218
\brief An untyped identifier
const core::identifier_string & name() const
const sort_expression_list & sorts() const
\brief Binder for untyped set or bag comprehension
Definition binder_type.h:77
const atermpp::aterm_int & value() const
\brief Unknown sort expression
\brief A data variable
Definition variable.h:28
const core::identifier_string & name() const
Definition variable.h:38
\brief A where expression
const data_expression & body() const
const assignment_expression_list & declarations() const
add your file description here.
The class data_specification.
add your file description here.
identifier_string empty_identifier_string()
Provides the empty identifier string.
bool is_greater(const application &x)
Definition print.h:209
bool is_minus(const application &x)
Definition print.h:93
bool is_equal_to(const application &x)
Definition print.h:185
bool is_snoc_list(data_expression x)
Definition print.h:270
bool is_in(const application &x)
Definition print.h:221
bool is_bag_intersection(const application &x)
Definition print.h:248
bool is_set_difference(const application &x)
Definition print.h:155
bool is_not_equal_to(const application &x)
Definition print.h:191
bool is_numeric_cast(const data_expression &x)
Definition print.h:45
bool is_divides(const application &x)
Definition print.h:134
bool is_set_union(const application &x)
Definition print.h:149
bool is_bag_difference(const application &x)
Definition print.h:167
bool is_less_equal(const application &x)
Definition print.h:203
bool is_set_intersection(const application &x)
Definition print.h:242
bool is_plus(const application &x)
Definition print.h:81
bool is_or(const application &x)
Definition print.h:179
bool is_greater_equal(const application &x)
Definition print.h:215
data_expression reconstruct_pos_mult(const data_expression &x, const std::vector< char > &result)
bool is_untyped(const data_expression &x)
Definition is_untyped.h:73
bool is_one(const data_expression &x)
Definition print.h:30
std::string pp(const detail::lhs_t &lhs)
bool is_element_at(const application &x)
Definition print.h:236
bool is_bag_join(const application &x)
Definition print.h:161
bool is_concat(const application &x)
Definition print.h:254
bool is_and(const application &x)
Definition print.h:173
bool look_through_numeric_casts(const data_expression &x, std::function< bool(const data_expression &)> f)
Definition print.h:61
bool is_snoc(const application &x)
Definition print.h:286
bool is_implies(const application &x)
Definition print.h:143
bool is_cons_list(data_expression x)
Definition print.h:260
bool is_mod(const application &x)
Definition print.h:103
bool is_divmod(const application &x)
Definition print.h:124
bool is_div(const application &x)
Definition print.h:113
bool is_times(const application &x)
Definition print.h:227
bool is_cons(const application &x)
Definition print.h:280
bool is_less(const application &x)
Definition print.h:197
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bag1.h:1606
function_symbol bag_fbag(const sort_expression &s)
Constructor for function symbol @bagfbag.
Definition bag1.h:176
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition bag1.h:665
bool is_bag_fbag_application(const atermpp::aterm &e)
Recogniser for application of @bagfbag.
Definition bag1.h:220
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition bag1.h:495
function_symbol count(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:298
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition bag1.h:410
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bag1.h:1594
const core::identifier_string & intersection_name()
Generate identifier *.
Definition bag1.h:503
bool is_bag_enumeration_application(const atermpp::aterm &e)
Recogniser for application of bag_enumeration.
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
bool is_bag_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @bagcomp.
Definition bag1.h:282
const core::identifier_string & union_name()
Generate identifier +.
Definition bag1.h:418
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition bag1.h:580
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bag1.h:1618
const core::identifier_string & difference_name()
Generate identifier -.
Definition bag1.h:588
bool is_one_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @one_.
Definition bag1.h:879
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:345
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
const core::identifier_string & implies_name()
Generate identifier =>.
Definition bool.h:353
const core::identifier_string & or_name()
Generate identifier ||.
Definition bool.h:289
bool is_implies_application(const atermpp::aterm &e)
Recogniser for application of =>.
Definition bool.h:409
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
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:281
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
Definition bool.h:87
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:217
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
const core::identifier_string & and_name()
Generate identifier &&.
Definition bool.h:225
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function {:}.
Definition fbag1.h:87
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition fbag1.h:579
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition fbag1.h:868
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition fbag1.h:904
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition fbag1.h:643
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition fbag1.h:453
const core::identifier_string & difference_name()
Generate identifier -.
Definition fbag1.h:651
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition fbag1.h:707
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of @fbag_cons.
Definition fbag1.h:259
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition fbag1.h:856
bool is_count_all_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition fbag1.h:769
bool is_cinsert_application(const atermpp::aterm &e)
Recogniser for application of @fbag_cinsert.
Definition fbag1.h:325
const core::identifier_string & union_name()
Generate identifier +.
Definition fbag1.h:523
bool is_insert_application(const atermpp::aterm &e)
Recogniser for application of @fbag_insert.
Definition fbag1.h:157
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition fbag1.h:844
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function {}.
Definition fset1.h:85
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition fset1.h:383
const core::identifier_string & difference_name()
Generate identifier -.
Definition fset1.h:391
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition fset1.h:720
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition fset1.h:708
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition fset1.h:447
const core::identifier_string & union_name()
Generate identifier +.
Definition fset1.h:455
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition fset1.h:637
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of @fset_cons.
Definition fset1.h:253
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition fset1.h:575
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition fset1.h:768
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition fset1.h:511
bool is_insert_application(const atermpp::aterm &e)
Recogniser for application of @fset_insert.
Definition fset1.h:153
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition int1.h:1516
const function_symbol & pos2int()
Constructor for function symbol Pos2Int.
Definition int1.h:360
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition int1.h:1492
bool is_mod_application(const atermpp::aterm &e)
Recogniser for application of mod.
Definition int1.h:1309
bool is_int(const sort_expression &e)
Recogniser for sort expression Int.
Definition int1.h:57
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition int1.h:1168
bool is_cneg_application(const atermpp::aterm &e)
Recogniser for application of @cNeg.
Definition int1.h:186
bool is_cint_application(const atermpp::aterm &e)
Recogniser for application of @cInt.
Definition int1.h:124
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
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
const core::identifier_string & div_name()
Generate identifier div.
Definition int1.h:1176
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
bool is_pos2int_application(const atermpp::aterm &e)
Recogniser for application of Pos2Int.
Definition int1.h:404
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
const core::identifier_string & snoc_name()
Generate identifier <|.
Definition list1.h:324
bool is_list_enumeration_application(const atermpp::aterm &e)
Recogniser for application of list_enumeration.
const core::identifier_string & in_name()
Generate identifier in.
Definition list1.h:198
bool is_concat_application(const atermpp::aterm &e)
Recogniser for application of ++.
Definition list1.h:444
const core::identifier_string & cons_name()
Generate identifier |>.
Definition list1.h:98
const core::identifier_string & concat_name()
Generate identifier ++.
Definition list1.h:388
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition list1.h:254
const core::identifier_string & element_at_name()
Generate identifier ..
Definition list1.h:452
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of |>.
Definition list1.h:154
bool is_snoc_application(const atermpp::aterm &e)
Recogniser for application of <|.
Definition list1.h:380
bool is_element_at_application(const atermpp::aterm &e)
Recogniser for application of ..
Definition list1.h:508
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition list1.h:831
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition list1.h:316
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition list1.h:855
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition list1.h:843
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function [].
Definition list1.h:86
const machine_number & one_word()
const machine_number & max_word()
const machine_number & zero_word()
bool is_zero_word_function_symbol(const atermpp::aterm &e)
Recogniser for function @zero_word.
bool is_add_word_application(const atermpp::aterm &e)
Recogniser for application of @add_word.
bool is_max_word_function_symbol(const atermpp::aterm &e)
Recogniser for function @max_word.
bool is_succ_word_application(const atermpp::aterm &e)
Recogniser for application of @succ_word.
bool is_one_word_function_symbol(const atermpp::aterm &e)
Recogniser for function @one_word.
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
bool is_times_overflow_word_application(const atermpp::aterm &e)
Recogniser for application of @times_overflow_word.
bool is_times_word_application(const atermpp::aterm &e)
Recogniser for application of @times_word.
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
bool is_add_overflow_word_application(const atermpp::aterm &e)
Recogniser for application of @add_overflow_word.
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition nat1.h:2257
bool is_cnat_application(const atermpp::aterm &e)
Recogniser for application of @cNat.
Definition nat1.h:184
bool is_div_application(const atermpp::aterm &e)
Recogniser for application of div.
Definition nat1.h:1110
bool is_pos2nat_application(const atermpp::aterm &e)
Recogniser for application of Pos2Nat.
Definition nat1.h:344
const function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat1.h:140
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
bool is_nat(const sort_expression &e)
Recogniser for sort expression Nat.
Definition nat1.h:56
std::string natural_constant_as_string(const data_expression &n_in)
Return the string representation of a natural number.
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition nat1.h:2245
bool is_mod_application(const atermpp::aterm &e)
Recogniser for application of mod.
Definition nat1.h:1174
bool is_last_application(const atermpp::aterm &e)
Recogniser for application of @last.
Definition nat1.h:1897
bool is_first_application(const atermpp::aterm &e)
Recogniser for application of @first.
Definition nat1.h:1835
bool is_c0_function_symbol(const atermpp::aterm &e)
Recogniser for function @c0.
Definition nat1.h:118
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition nat1.h:2233
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition nat1.h:2221
bool is_concat_digit_application(const atermpp::aterm &e)
Recogniser for application of @concat_digit.
Definition nat64.h:422
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition nat1.h:2209
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition nat1.h:903
bool is_divmod_aux_application(const atermpp::aterm &e)
Recogniser for application of @divmod_aux.
Definition nat64.h:3064
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition nat1.h:1046
const function_symbol & pos2nat()
Constructor for function symbol Pos2Nat.
Definition nat1.h:300
bool is_natural_constant(const data_expression &n)
Determines whether n is a natural constant.
bool is_most_significant_digit_nat_application(const atermpp::aterm &e)
Recogniser for application of @most_significant_digitNat.
Definition nat64.h:345
bool is_divmod_application(const atermpp::aterm &e)
Recogniser for application of @divmod.
Definition nat1.h:1961
std::string positive_constant_as_string(const data_expression &n_in)
Return the string representation of a positive number.
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition pos1.h:788
bool is_positive_constant(const data_expression &n)
Determines whether n is a positive constant.
bool is_pos(const sort_expression &e)
Recogniser for sort expression Pos.
Definition pos1.h:55
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition pos1.h:824
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition pos1.h:800
bool is_cdub_application(const atermpp::aterm &e)
Recogniser for application of @cDub.
Definition pos1.h:156
const function_symbol & plus()
Constructor for function symbol +.
Definition pos1.h:458
bool is_add_with_carry_application(const atermpp::aterm &e)
Recogniser for application of @addc.
Definition pos1.h:570
bool is_c1_function_symbol(const atermpp::aterm &e)
Recogniser for function @c1.
Definition pos1.h:88
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition pos1.h:812
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition pos1.h:776
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition pos1.h:634
bool is_most_significant_digit_application(const atermpp::aterm &e)
Recogniser for application of @most_significant_digit.
Definition pos64.h:249
bool is_concat_digit_application(const atermpp::aterm &e)
Recogniser for application of @concat_digit.
Definition pos64.h:313
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition pos1.h:764
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition pos1.h:504
const function_symbol & succ()
Constructor for function symbol succ.
Definition pos1.h:334
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1059
const core::identifier_string & minus_name()
Generate identifier -.
Definition real1.h:1144
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1407
bool is_int2real_application(const atermpp::aterm &e)
Recogniser for application of Int2Real.
Definition real1.h:339
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition real1.h:1989
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1136
bool is_divides_application(const atermpp::aterm &e)
Recogniser for application of /.
Definition real1.h:1455
const core::identifier_string & divides_name()
Generate identifier /.
Definition real1.h:1399
bool is_reduce_fraction_where_application(const atermpp::aterm &e)
Recogniser for application of @redfracwhr.
Definition real1.h:1771
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:153
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:58
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition real1.h:1953
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition real1.h:1977
const core::identifier_string & plus_name()
Generate identifier +.
Definition real1.h:1051
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition real1.h:1941
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1306
bool is_reduce_fraction_application(const atermpp::aterm &e)
Recogniser for application of @redfrac.
Definition real1.h:1705
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:877
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1221
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition real1.h:2001
const function_symbol & int2real()
Constructor for function symbol Int2Real.
Definition real1.h:295
bool is_pos2real_application(const atermpp::aterm &e)
Recogniser for application of Pos2Real.
Definition real1.h:215
bool is_nat2real_application(const atermpp::aterm &e)
Recogniser for application of Nat2Real.
Definition real1.h:277
bool is_set_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @setcomp.
Definition set1.h:280
bool is_false_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @false_.
Definition set1.h:665
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition set1.h:483
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_fset_union_application(const atermpp::aterm &e)
Recogniser for application of @fset_union.
Definition set1.h:1019
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition set1.h:1172
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition set1.h:344
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
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
bool is_set_fset_application(const atermpp::aterm &e)
Recogniser for application of @setfset.
Definition set1.h:218
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition set1.h:1220
const core::identifier_string & intersection_name()
Generate identifier *.
Definition set1.h:491
bool is_set_enumeration_application(const atermpp::aterm &e)
Recogniser for application of set_enumeration.
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
const core::identifier_string & union_name()
Generate identifier +.
Definition set1.h:414
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:296
const core::identifier_string & difference_name()
Generate identifier -.
Definition set1.h:568
function_symbol set_fset(const sort_expression &s)
Constructor for function symbol @setfset.
Definition set1.h:174
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition set1.h:560
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition set1.h:1208
bool is_greater_application(const DataExpression &e)
Recogniser for application of >
Definition standard.h:343
bool is_set_container(const atermpp::aterm &x)
int precedence(const data_expression &x)
Definition print.h:394
data_expression number(const sort_expression &s, const std::string &n)
Construct numeric expression from a string representing a number in decimal notation.
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
bool is_list_container(const atermpp::aterm &x)
bool is_if_application(const DataExpression &e)
Recogniser for application of if.
Definition standard.h:232
bool is_not_equal_to_application(const DataExpression &e)
Recogniser for application of !=.
Definition standard.h:192
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:94
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
bool is_greater_equal_application(const DataExpression &e)
Recogniser for application of >=.
Definition standard.h:380
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
bool is_untyped_identifier(const atermpp::aterm &x)
Returns true if the term t is an identifier.
bool is_left_associative(const data_expression &x)
Definition print.h:407
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
std::string pp(const abstraction &x)
Definition data.cpp:39
bool is_right_associative(const data_expression &x)
Definition print.h:413
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
bool is_fset_container(const atermpp::aterm &x)
bool is_function_update_stable_application(const atermpp::aterm &e)
Recogniser for application of @func_update_stable.
std::set< data::function_symbol > find_function_symbols(const data::data_equation &x)
Definition data.cpp:101
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set/bag comprehension.
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
bool is_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a bag comprehension.
bool is_set_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set comprehension.
std::string max_machine_number_string()
A string representation indicating the maximal machine number + 1.
bool is_bag_container(const atermpp::aterm &x)
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
bool is_function_update_application(const atermpp::aterm &e)
Recogniser for application of @func_update.
bool is_fbag_container(const atermpp::aterm &x)
bool is_lambda(const atermpp::aterm &x)
Returns true if the term t is a lambda abstraction.
bool is_less_application(const DataExpression &e)
Recogniser for application of <.
Definition standard.h:269
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
bool is_less_equal_application(const DataExpression &e)
Recogniser for application of <=.
Definition standard.h:306
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
bool is_equal_to_application(const DataExpression &e)
Recogniser for application of ==.
Definition standard.h:155
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Provides utilities for working with data expressions of standard container sorts.
sort_expression operator()(const T &t) const
Definition print.h:566
void print_condition(const T &x, const std::string &arrow=" -> ")
Definition print.h:728
void apply(const data::untyped_set_or_bag_comprehension_binder &x)
Definition print.h:1307
void apply(const data::untyped_sort_variable &x)
Definition print.h:1460
void apply(const data::application &x)
Definition print.h:1508
bool is_cons_list(data_expression x) const
Definition print.h:814
void apply(const machine_number &x)
Definition print.h:2283
void print_container(const Container &container, int container_precedence=-1, const std::string &separator=", ", const std::string &open_bracket="(", const std::string &close_bracket=")")
Definition print.h:526
void apply(const data::untyped_identifier &x)
Definition print.h:1468
void print_sort_list(const Container &container, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ")
Definition print.h:738
void print_fset_default(const data_expression &x)
Definition print.h:1128
void apply(const data::bag_comprehension_binder &x)
Definition print.h:1319
void apply(const data::set_container &x)
Definition print.h:1384
void apply(const data::set_comprehension_binder &x)
Definition print.h:1313
void print_set_enumeration(const application &x)
Definition print.h:776
void print_binary_data_operation(const application &x, const std::string &op)
Definition print.h:455
void print_cons_list(data_expression x)
Definition print.h:898
void print_sort_declarations(const AliasContainer &aliases, const SortContainer &sorts, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ")
Definition print.h:2392
void update_mappings(const data_equation &eqn, std::vector< variable > &variables, std::map< core::identifier_string, variable > &variable_map, std::set< core::identifier_string > &function_symbol_names)
Definition print.h:2332
bool is_fbag_cons_list(data_expression x)
Returns true if x is a list composed of cons, insert and cinsert applications.
Definition print.h:842
void print_assignments(const Container &container, bool print_lhs=true, const std::string &opener="", const std::string &closer="", const std::string &separator=", ", const std::string &assignment_symbol=" = ")
Definition print.h:698
void apply(const data::list_container &x)
Definition print.h:1377
void apply(const data::exists &x)
Definition print.h:2311
void apply(const data::fbag_container &x)
Definition print.h:1405
void apply(const data::function_sort &x)
Definition print.h:1436
void print_fset_lambda(const data_expression &x)
Definition print.h:1055
core::identifier_string generate_identifier(const std::string &prefix, const data_expression &context) const
Definition print.h:514
void apply(const data::data_equation &x)
Definition print.h:2321
void apply(const data::alias &x)
Definition print.h:1368
void print_sorted_declarations(const Container &container, bool print_sorts=true, bool join_sorts=true, bool maximally_shared=false, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ", SortAccessor get_sort=get_sort_default())
Definition print.h:573
void apply(const data::where_clause &x)
Definition print.h:2288
void apply(const data::data_specification &x)
Definition print.h:2461
bool is_fbag_zero(const data_expression &x)
Definition print.h:883
void apply(const data::structured_sort &x)
Definition print.h:1429
void apply(const data::untyped_identifier_assignment &x)
Definition print.h:1298
void print_equations(const Container &equations, const data_specification &data_spec, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ")
Definition print.h:2432
bool is_fset_false(const data_expression &x)
Definition print.h:873
bool is_abstraction_application(const application &x) const
Definition print.h:809
void apply(const data::lambda_binder &x)
Definition print.h:1337
void apply(const data::structured_sort_constructor_argument &x)
Definition print.h:1343
void apply(const data::variable &x)
Definition print.h:1475
void apply(const data::container_type &x)
Definition print.h:1247
bool is_fbag_one(const data_expression &x)
Definition print.h:888
void apply(const data::basic_sort &x)
Definition print.h:1412
bool is_snoc_list(data_expression x) const
Definition print.h:823
void print_fbag_one(const data_expression &x)
Definition print.h:957
bool is_fbag_lambda(const data_expression &x)
Definition print.h:893
void print_abstraction(const Abstraction &x, const std::string &op)
Definition print.h:1161
void apply(const data::function_symbol &x)
Definition print.h:1482
void apply(const data::exists_binder &x)
Definition print.h:1331
void apply(const data::fset_container &x)
Definition print.h:1398
bool has_conflict(const data_equation &eqn, const std::map< core::identifier_string, variable > &variable_map)
Definition print.h:2352
bool is_numeric_expression(const application &x)
Definition print.h:851
bool is_infix_operation(const application &x) const
Definition print.h:462
void print_fbag_lambda(const data_expression &x)
Definition print.h:974
void apply(const data::untyped_data_parameter &x)
Definition print.h:1290
void apply(const data::abstraction &x)
Definition print.h:2472
void apply(const data::untyped_sort &x)
Definition print.h:1444
void apply(const data::container_sort &x)
Definition print.h:1419
void apply(const data::assignment &x)
Definition print.h:1273
void print_fbag_zero(const data_expression &x)
Definition print.h:937
data::add_traverser_sort_expressions< core::detail::printer, Derived > super
Definition print.h:429
bool is_fset_lambda(const data_expression &x)
Definition print.h:878
void print_snoc_list(data_expression x)
Definition print.h:911
void print_fset_false(const data_expression &x)
Definition print.h:1043
void print_fbag_cons_list(data_expression x)
Definition print.h:1009
bool is_standard_sort(const sort_expression &x)
Definition print.h:859
void apply(const data::untyped_possible_sorts &x)
Definition print.h:1451
void print_unary_data_operation(const application &x, const std::string &op)
Definition print.h:439
bool is_fset_cons_list(data_expression x)
Definition print.h:832
void print_setbag_comprehension(const abstraction &x)
Definition print.h:800
void print_fset_cons_list(data_expression x)
Definition print.h:924
void print_bag_enumeration(const application &x)
Definition print.h:783
void print_variables(const Container &container, bool print_sorts=true, bool join_sorts=true, bool maximally_shared=false, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ")
Definition print.h:685
void apply(const data::bag_container &x)
Definition print.h:1391
void print_function_application(const application &x)
Definition print.h:1171
void print_fbag_default(const data_expression &x)
Definition print.h:992
Iter find_conflicting_equation(Iter first, Iter last, std::vector< variable > &variables)
Searches in the range of equations [first, last) for the first equation that conflicts with one of th...
Definition print.h:2373
void print_variable(const Variable &x, bool print_sort=false)
Definition print.h:553
void apply(const data::variable_list &x)
Definition print.h:1283
void apply(const std::pair< data_expression, data_expression > &x)
Definition print.h:1239
void print_binary_data_operation(const application &x, const data_expression &x1, const data_expression &x2, const std::string &op)
Definition print.h:445
void print_list_enumeration(const application &x)
Definition print.h:769
void apply(const data::structured_sort_constructor &x)
Definition print.h:1355
void apply(const data::forall &x)
Definition print.h:2306
void apply(const data::forall_binder &x)
Definition print.h:1325
void apply(const data::lambda &x)
Definition print.h:2316
void print_fset_set_operation(const data_expression &x, const std::string &op)
Definition print.h:1065
void print_fset_true(const data_expression &x)
Definition print.h:1037
bool is_fset_true(const data_expression &x)
Definition print.h:868
Prints the object x to a stream.
Definition print.h:2507
void operator()(const T &x, std::ostream &out)
Definition print.h:2509