mCRL2
Loading...
Searching...
No Matches
data_specification.cpp
Go to the documentation of this file.
1// Author(s): Jeroen Keiren, Jeroen van der Wulp, Jan Friso Groote
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//
9
14#include "mcrl2/data/replace.h"
16
17// Predefined datatypes
19#include "mcrl2/data/list.h"
20
21namespace mcrl2
22{
23namespace data
24{
25
27{
28 protected:
29
31 std::set< sort_expression > m_visiting;
32
34 {
36 if (constructors.empty())
37 {
38 return false;
39 }
40
41 for(const function_symbol& f: constructors)
42 {
43 if (is_function_sort(f.sort()))
44 {
45 const function_sort& f_sort=atermpp::down_cast<function_sort>(f.sort());
46 const sort_expression_list& l=f_sort.domain();
47
48 for(const sort_expression& e: l)
49 {
50 if (!is_finite(e))
51 {
52 return false;
53 }
54 }
55 }
56 }
57 return true;
58 }
59
60 public:
61
62 finiteness_helper(const data_specification& specification) : m_specification(specification)
63 { }
64
66 {
67 assert(s==normalize_sorts(s,m_specification));
68 if (m_visiting.count(s)>0)
69 {
70 return false;
71 }
72
73 m_visiting.insert(s);
74
75 bool result=false;
76 if (is_basic_sort(s))
77 {
78 result=is_finite(basic_sort(s));
79 }
80 else if (is_container_sort(s))
81 {
82 result=is_finite(container_sort(s));
83 }
84 else if (is_function_sort(s))
85 {
86 result=is_finite(function_sort(s));
87 }
88 else if (is_structured_sort(s))
89 {
90 result=is_finite(structured_sort(s));
91 }
92
93 m_visiting.erase(s);
94 return result;
95 }
96
97 bool is_finite(const basic_sort& s)
98 {
99 return is_finite_aux(s);
100 }
101
103 {
104 for(const sort_expression& sort: s.domain())
105 {
106 if (!is_finite(sort))
107 {
108 return false;
109 }
110 }
111
112 return is_finite(s.codomain());
113 }
114
116 {
117 return (s.container_name() == set_container()) ? is_finite(s.element_sort()) : false;
118 }
119
120 bool is_finite(const alias&)
121 {
122 assert(0);
123 return false;
124 }
125
127 {
128 return is_finite_aux(s);
129 }
130};
131
138{
139 const bool result=finiteness_helper(*this).is_finite(s);
140 return result;
141}
142
143
144// The function below checks whether there is an alias loop, e.g. aliases
145// of the form A=B; B=A; or more complex A=B->C; B=Set(D); D=List(A); Loops
146// through structured sorts are allowed. If a loop is detected, an exception
147// is thrown.
149 const sort_expression& s,
150 std::set<sort_expression> sorts_already_seen,
151 const bool toplevel) const
152{
153 if (is_basic_sort(s))
154 {
155 if (sorts_already_seen.count(s)>0)
156 {
157 throw mcrl2::runtime_error("Sort alias " + pp(s) + " is defined in terms of itself.");
158 }
159 for(const alias& a: m_user_defined_aliases)
160 {
161 if (a.name() == s)
162 {
163 sorts_already_seen.insert(s);
164 check_for_alias_loop(a.reference(), sorts_already_seen, true);
165 sorts_already_seen.erase(s);
166 return;
167 }
168 }
169 return;
170 }
171
172 if (is_container_sort(s))
173 {
174 check_for_alias_loop(container_sort(s).element_sort(),sorts_already_seen,false);
175 return;
176 }
177
178 if (is_function_sort(s))
179 {
180 sort_expression_list s_domain(function_sort(s).domain());
181 for(const sort_expression& sort: s_domain)
182 {
183 check_for_alias_loop(sort,sorts_already_seen,false);
184 }
185
186 check_for_alias_loop(function_sort(s).codomain(),sorts_already_seen,false);
187 return;
188 }
189
190 // A sort declaration with a struct on toplevel can be recursive. Otherwise a
191 // check needs to be made.
192 if (is_structured_sort(s) && !toplevel)
193 {
194 const structured_sort ss(s);
196 for(const structured_sort_constructor& constructor: constructors)
197 {
198 structured_sort_constructor_argument_list ssca=constructor.arguments();
199 for(const structured_sort_constructor_argument& a: ssca)
200 {
201 check_for_alias_loop(a.sort(),sorts_already_seen,false);
202 }
203 }
204 }
205
206}
207
208
209// This function returns the normal form of e, under the the map map1.
210// This normal form is obtained by repeatedly applying map1, until this
211// is not possible anymore. It is assumed that this procedure terminates. There is
212// no check for loops.
214 const sort_expression& e,
215 const std::multimap< sort_expression, sort_expression >& map1,
216 std::set < sort_expression > sorts_already_seen = std::set < sort_expression >())
217{
218 assert(sorts_already_seen.find(e)==sorts_already_seen.end()); // e has not been seen already.
219 assert(!is_untyped_sort(e));
220 assert(!is_untyped_possible_sorts(e));
221
222 if (is_function_sort(e))
223 {
224 const function_sort fs(e);
225 const sort_expression normalised_codomain=
226 find_normal_form(fs.codomain(),map1,sorts_already_seen);
227 const sort_expression_list& domain=fs.domain();
228 sort_expression_list normalised_domain;
229 for(const sort_expression& s: domain)
230 {
231 normalised_domain.push_front(find_normal_form(s,map1,sorts_already_seen));
232 }
233 return function_sort(reverse(normalised_domain),normalised_codomain);
234 }
235
236 if (is_container_sort(e))
237 {
238 const container_sort cs(e);
239 return container_sort(cs.container_name(),find_normal_form(cs.element_sort(),map1,sorts_already_seen));
240 }
241
242 sort_expression result_sort;
243
244 if (is_structured_sort(e))
245 {
246 const structured_sort ss(e);
248 structured_sort_constructor_list normalised_constructors;
249 for(const structured_sort_constructor& constructor: constructors)
250 {
252 for(const structured_sort_constructor_argument& a: constructor.arguments())
253 {
254 normalised_ssa.push_front(structured_sort_constructor_argument(a.name(),
255 find_normal_form(a.sort(),map1,sorts_already_seen)));
256 }
257
258 normalised_constructors.push_front(
260 constructor.name(),
261 reverse(normalised_ssa),
262 constructor.recogniser()));
263
264 }
265 result_sort=structured_sort(reverse(normalised_constructors));
266 }
267
268 if (is_basic_sort(e))
269 {
270 result_sort=e;
271 }
272
273
274 assert(is_basic_sort(result_sort) || is_structured_sort(result_sort));
275 const std::multimap< sort_expression, sort_expression >::const_iterator i1=map1.find(result_sort);
276 if (i1!=map1.end()) // found
277 {
278#ifndef NDEBUG
279 sorts_already_seen.insert(result_sort);
280#endif
281 return find_normal_form(i1->second,map1,sorts_already_seen);
282 }
283 return result_sort;
284}
285
287{
290}
291
293{
295 {
296 mCRL2log(mcrl2::log::debug) << "Erroneous attempt to insert an untyped sort into the a sort specification\n";
297 return;
298 }
299 // Add an element, and stop if it was already added.
300 if (!m_sorts_in_context.insert(sort).second)
301 {
302 return;
303 }
304
306 // add the sorts on which this sorts depends.
307 if (sort == sort_real::real_())
308 {
309 // Int is required as the rewrite rules of Real rely on it.
311 }
312 else if (sort == sort_int::int_())
313 {
314 // See above, Int requires Nat.
316 }
317 else if (sort == sort_nat::nat())
318 {
319#ifdef MCRL2_ENABLE_MACHINENUMBERS
321#else
322 // Nat requires NatPair.
324#endif
325 }
326 else if (sort == sort_pos::pos())
327 {
328#ifdef MCRL2_ENABLE_MACHINENUMBERS
330#endif
331 }
332 else if (is_function_sort(sort))
333 {
334 const function_sort& fsort=atermpp::down_cast<function_sort>(sort);
337 }
338 else if (is_container_sort(sort))
339 {
340 const sort_expression element_sort(container_sort(sort).element_sort());
341 // Import the element sort (which may be a complex sort also).
342 import_system_defined_sort(element_sort);
343 if (sort_list::is_list(sort))
344 {
345 import_system_defined_sort(sort_nat::nat()); // Required for lists.
346 }
347 else if (sort_set::is_set(sort))
348 {
350 // Import the functions from element_sort->Bool.
351 sort_expression_list element_sorts;
352 element_sorts.push_front(element_sort);
354 }
355 else if (sort_fset::is_fset(sort))
356 {
357 }
358 else if (sort_bag::is_bag(sort))
359 {
360 // Add the sorts Nat and set_(element_sort) to the specification.
361 import_system_defined_sort(sort_nat::nat()); // Required for bags.
364
365 // Add the function sort element_sort->Nat to the specification
366 sort_expression_list element_sorts ;
367 element_sorts.push_front(element_sort);
369 }
370 else if (sort_fbag::is_fbag(sort))
371 {
372 import_system_defined_sort(sort_nat::nat()); // Required for bags.
373 }
374 }
375 else if (is_structured_sort(sort))
376 {
377 structured_sort s_sort(sort);
379 for(const function_symbol& f: s_sort.constructor_functions(sort))
380 {
382 }
383 }
384}
385
386// The function below recalculates m_normalised_aliases, such that
387// it forms a confluent terminating rewriting system using which
388// sorts can be normalised.
389// This algorithm is described in the document: algorithm-for-sort-equivalence.tex in
390// the developers library of the mCRL2 toolset.
392{
393 // First reset the normalised aliases and the mappings and constructors that have been
394 // inherited to basic sort aliases during a previous round of sort normalisation.
395 m_normalised_aliases.clear();
396
397 // This is the first step of the algorithm.
398 // Check for loops in the aliases. The type checker should already have done this,
399 // but we check it again here. If there is a loop m_normalised_aliases will not be
400 // built.
401 for(const alias& a: m_user_defined_aliases)
402 {
403 std::set < sort_expression > sorts_already_seen; // Empty set.
404 try
405 {
406 check_for_alias_loop(a.name(),sorts_already_seen,true);
407 }
408 catch (mcrl2::runtime_error &)
409 {
410 mCRL2log(log::debug) << "Encountered an alias loop in the alias for " << a.name() <<". The normalised aliases are not constructed\n";
411 return;
412 }
413 }
414
415 // This is the second step of the algorithm.
416 // Copy m_normalised_aliases. All aliases are stored from left to right,
417 // except structured sorts, which are stored from right to left. The reason is
418 // that structured sorts can be recursive, and therefore, they cannot be
419 // rewritten from left to right, as this can cause sorts to be infinitely rewritten.
420
421 std::multimap< sort_expression, sort_expression > sort_aliases_to_be_investigated;
422 std::multimap< sort_expression, sort_expression > resulting_normalized_sort_aliases;
423
424 for(const alias& a: m_user_defined_aliases)
425 {
426 if (is_structured_sort(a.reference()))
427 {
428 sort_aliases_to_be_investigated.insert(std::pair<sort_expression,sort_expression>(a.reference(),a.name()));
429 }
430 else
431 {
432 resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression>(a.name(),a.reference()));
433 }
434 }
435
436 // Apply Knuth-Bendix completion to the rules in m_normalised_aliases.
437 for(; !sort_aliases_to_be_investigated.empty() ;)
438 {
439 const std::multimap< sort_expression, sort_expression >::iterator it=sort_aliases_to_be_investigated.begin();
440 const sort_expression lhs=it->first;
441 const sort_expression rhs=it->second;
442 sort_aliases_to_be_investigated.erase(it);
443
444 for(const std::pair<const sort_expression, sort_expression >& p: resulting_normalized_sort_aliases)
445 {
447
448 if (s1!=lhs)
449 {
450 // There is a conflict between the two sort rewrite rules.
451 assert(is_basic_sort(rhs));
452 // Choose the normal form on the basis of a lexicographical ordering. This guarantees
453 // uniqueness of normal forms over different tools. Ordering on addresses (as used previously)
454 // proved to be unstable over different tools.
455 const bool rhs_to_s1 = is_basic_sort(s1) && pp(basic_sort(s1))<=pp(rhs);
456 const sort_expression left_hand_side=(rhs_to_s1?rhs:s1);
457 const sort_expression pre_normal_form=(rhs_to_s1?s1:rhs);
458 assert(is_basic_sort(pre_normal_form));
459 const sort_expression& e1=pre_normal_form;
460 if (e1!=left_hand_side)
461 {
462 const sort_expression normalised_lhs=find_normal_form(left_hand_side,resulting_normalized_sort_aliases);
463 // Check whether the inserted sort rewrite rule is already in sort_aliases_to_be_investigated.
464 if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
465 sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
466 [&rhs](const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
467 == sort_aliases_to_be_investigated.upper_bound(normalised_lhs)) // Not found.
468 {
469 sort_aliases_to_be_investigated.insert(
470 std::pair<sort_expression,sort_expression > (normalised_lhs, e1));
471 }
472 }
473 }
474 else
475 {
477 if (s2!=p.first)
478 {
479 assert(is_basic_sort(p.second));
480 // Choose the normal form on the basis of a lexicographical ordering. This guarantees
481 // uniqueness of normal forms over different tools.
482 const bool i_second_to_s2 = is_basic_sort(s2) && pp(basic_sort(s2))<=pp(p.second);
483 const sort_expression left_hand_side=(i_second_to_s2?p.second:s2);
484 const sort_expression pre_normal_form=(i_second_to_s2?s2:p.second);
485 assert(is_basic_sort(pre_normal_form));
486 const sort_expression& e2=pre_normal_form;
487 if (e2!=left_hand_side)
488 {
489 const sort_expression normalised_lhs=find_normal_form(left_hand_side,resulting_normalized_sort_aliases);
490 // Check whether the inserted sort rewrite rule is already in sort_aliases_to_be_investigated.
491 if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
492 sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
493 [&rhs](const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
494 == sort_aliases_to_be_investigated.upper_bound(normalised_lhs)) // Not found.
495 {
496 sort_aliases_to_be_investigated.insert(
497 std::pair<sort_expression,sort_expression > (normalised_lhs,e2));
498 }
499 }
500 }
501 }
502 }
503 assert(lhs!=rhs);
504 const sort_expression normalised_lhs = find_normal_form(lhs,resulting_normalized_sort_aliases);
505 const sort_expression normalised_rhs = find_normal_form(rhs,resulting_normalized_sort_aliases);
506 if (normalised_lhs!=normalised_rhs)
507 {
508 resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression >(normalised_lhs,normalised_rhs));
509 }
510 }
511 // Copy resulting_normalized_sort_aliases into m_normalised_aliases, i.e. from multimap to map.
512 // If there are rules with equal left hand side, only one is arbitrarily chosen. Rewrite the
513 // right hand side to normal form.
514
515 for(const std::pair<const sort_expression,sort_expression>& p: resulting_normalized_sort_aliases)
516 {
517 const sort_expression normalised_rhs = find_normal_form(p.second,resulting_normalized_sort_aliases);
518 m_normalised_aliases[p.first]=normalised_rhs;
519
520 assert(p.first!=normalised_rhs);
521 }
522}
523
525// a given sort. If the boolean skip_equations is true, no equations are added.
527 const sort_expression& sort,
528 std::set < function_symbol >& constructors,
529 std::set < function_symbol >& mappings,
530 std::set < data_equation >& equations,
531 implementation_map& cpp_implemented_functions,
532 const bool skip_equations) const
533{
534 // add sorts, constructors, mappings and equations
535 if (sort == sort_bool::bool_())
536 {
538 constructors.insert(f.begin(), f.end());
540 mappings.insert(f.begin(), f.end());
542 cpp_implemented_functions.insert(f1.begin(), f1.end());
544 cpp_implemented_functions.insert(f1.begin(), f1.end());
545 if (!skip_equations)
546 {
548 equations.insert(e.begin(),e.end());
549 }
550 }
551 else if (sort == sort_real::real_())
552 {
554 constructors.insert(f.begin(),f.end());
556 mappings.insert(f.begin(),f.end());
558 cpp_implemented_functions.insert(f1.begin(), f1.end());
560 cpp_implemented_functions.insert(f1.begin(), f1.end());
561 if (!skip_equations)
562 {
564 equations.insert(e.begin(),e.end());
565 }
566 }
567 else if (sort == sort_int::int_())
568 {
570 constructors.insert(f.begin(),f.end());
572 mappings.insert(f.begin(),f.end());
574 cpp_implemented_functions.insert(f1.begin(), f1.end());
576 cpp_implemented_functions.insert(f1.begin(), f1.end());
577 if (!skip_equations)
578 {
580 equations.insert(e.begin(),e.end());
581 }
582 }
583 else if (sort == sort_nat::nat())
584 {
586 constructors.insert(f.begin(),f.end());
588 mappings.insert(f.begin(),f.end());
590 cpp_implemented_functions.insert(f1.begin(), f1.end());
592 cpp_implemented_functions.insert(f1.begin(), f1.end());
593 if (!skip_equations)
594 {
596 equations.insert(e.begin(),e.end());
597 }
598 }
599 else if (sort == sort_pos::pos())
600 {
602 constructors.insert(f.begin(),f.end());
604 mappings.insert(f.begin(),f.end());
606 cpp_implemented_functions.insert(f1.begin(), f1.end());
608 cpp_implemented_functions.insert(f1.begin(), f1.end());
609 if (!skip_equations)
610 {
612 equations.insert(e.begin(),e.end());
613 }
614 }
615#ifdef MCRL2_ENABLE_MACHINENUMBERS
616 else if (sort == sort_machine_word::machine_word())
617 {
619 constructors.insert(f.begin(),f.end());
621 mappings.insert(f.begin(),f.end());
623 cpp_implemented_functions.insert(f1.begin(), f1.end());
625 cpp_implemented_functions.insert(f1.begin(), f1.end());
626 if (!skip_equations)
627 {
629 equations.insert(e.begin(),e.end());
630 }
631 }
632#endif
633 else if (is_function_sort(sort))
634 {
635 const sort_expression& t = static_cast<const function_sort&>(sort).codomain();
636 const sort_expression_list& l = static_cast<const function_sort&>(sort).domain();
637 if (l.size()==1)
638 {
640 mappings.insert(f.begin(),f.end());
642 cpp_implemented_functions.insert(f1.begin(), f1.end());
644 cpp_implemented_functions.insert(f1.begin(), f1.end());
645 if (!skip_equations)
646 {
648 equations.insert(e.begin(),e.end());
649 }
650 }
651 }
652 else if (is_container_sort(sort))
653 {
654 sort_expression element_sort(container_sort(sort).element_sort());
655 if (sort_list::is_list(sort))
656 {
658 constructors.insert(f.begin(),f.end());
660 mappings.insert(f.begin(),f.end());
662 cpp_implemented_functions.insert(f1.begin(), f1.end());
664 cpp_implemented_functions.insert(f1.begin(), f1.end());
665 if (!skip_equations)
666 {
668 equations.insert(e.begin(),e.end());
669 }
670 }
671 else if (sort_set::is_set(sort))
672 {
673 sort_expression_list element_sorts;
674 element_sorts.push_front(element_sort);
676 constructors.insert(f.begin(),f.end());
678 mappings.insert(f.begin(),f.end());
680 cpp_implemented_functions.insert(f1.begin(), f1.end());
682 cpp_implemented_functions.insert(f1.begin(), f1.end());
683 if (!skip_equations)
684 {
686 equations.insert(e.begin(),e.end());
687 }
688 }
689 else if (sort_fset::is_fset(sort))
690 {
692 constructors.insert(f.begin(),f.end());
694 mappings.insert(f.begin(),f.end());
696 cpp_implemented_functions.insert(f1.begin(), f1.end());
698 cpp_implemented_functions.insert(f1.begin(), f1.end());
699 if (!skip_equations)
700 {
702 equations.insert(e.begin(),e.end());
703 }
704 }
705 else if (sort_bag::is_bag(sort))
706 {
707 sort_expression_list element_sorts;
708 element_sorts.push_front(element_sort);
710 constructors.insert(f.begin(),f.end());
712 mappings.insert(f.begin(),f.end());
714 cpp_implemented_functions.insert(f1.begin(), f1.end());
716 cpp_implemented_functions.insert(f1.begin(), f1.end());
717 if (!skip_equations)
718 {
720 equations.insert(e.begin(),e.end());
721 }
722 }
723 else if (sort_fbag::is_fbag(sort))
724 {
726 constructors.insert(f.begin(),f.end());
728 mappings.insert(f.begin(),f.end());
730 cpp_implemented_functions.insert(f1.begin(), f1.end());
732 cpp_implemented_functions.insert(f1.begin(), f1.end());
733 if (!skip_equations)
734 {
736 equations.insert(e.begin(),e.end());
737 }
738 }
739 }
740 else if (is_structured_sort(sort))
741 {
743 atermpp::down_cast<structured_sort>(sort),
744 constructors, mappings, equations, skip_equations);
745 }
747}
748
750 std::set < sort_expression >& sorts,
751 std::set < function_symbol >& constructors,
752 std::set <function_symbol >& mappings) const
753{
755
756 sorts.insert(sort_bool::bool_());
757#ifdef MCRL2_ENABLE_MACHINENUMBERS
759#endif
760 sorts.insert(sort_pos::pos());
761 sorts.insert(sort_nat::nat());
762 sorts.insert(sort_int::int_());
763 sorts.insert(sort_real::real_());
769
770 std::set < data_equation > dummy_equations;
771 for(const sort_expression& s: sorts)
772 {
774 }
775 assert(dummy_equations.size()==0);
776}
777
779{
780 // check 1)
782 {
783 std::clog << "data_specification::is_well_typed() failed: not all of the sorts appearing in the constructors "
784 << data::pp(constructors()) << " are declared in " << data::pp(sorts()) << std::endl;
785 return false;
786 }
787
788 // check 2)
790 {
791 std::clog << "data_specification::is_well_typed() failed: not all of the sorts appearing in the mappings "
792 << data::pp(mappings()) << " are declared in " << data::pp(sorts()) << std::endl;
793 return false;
794 }
795
796 return true;
797}
798
806void data_specification::build_from_aterm(const atermpp::aterm& term)
807{
809
810 // Note backwards compatibility measure: alias is no longer a sort_expression
811 const atermpp::term_list<atermpp::aterm> term_sorts=
812 atermpp::down_cast<atermpp::term_list<atermpp::aterm> >(term[0][0]);
813 const data::function_symbol_list term_constructors=
814 atermpp::down_cast<data::function_symbol_list>(term[1][0]);
815 const data::function_symbol_list term_mappings=
816 atermpp::down_cast<data::function_symbol_list>(term[2][0]);
817 const data::data_equation_list term_equations=
818 atermpp::down_cast<data::data_equation_list>(term[3][0]);
819
820 // Store the sorts and aliases.
821 for(const atermpp::aterm& t: term_sorts)
822 {
823 if (data::is_alias(t)) // Compatibility with legacy code
824 {
825 add_alias(atermpp::down_cast<data::alias>(t));
826 }
827 else
828 {
829 add_sort(atermpp::down_cast<basic_sort>(t));
830 }
831 }
832
833 // Store the constructors.
834 for(const function_symbol& f: term_constructors)
835 {
837 }
838
839 // Store the mappings.
840 for(const function_symbol& f: term_mappings)
841 {
842 add_mapping(f);
843 }
844
845 // Store the equations.
846 for(const data_equation& e: term_equations)
847 {
848 add_equation(e);
849 }
850}
851
853 const alias_vector& aliases,
854 const function_symbol_vector& constructors,
855 const function_symbol_vector& user_defined_mappings,
856 const data_equation_vector& user_defined_equations)
857 : sort_specification(sorts, aliases)
858{
859 // Store the constructors.
860 for(const function_symbol& f: constructors)
861 {
863 }
864
865 // Store the mappings.
867 {
868 add_mapping(f);
869 }
870
871 // Store the equations.
873 {
874 add_equation(e);
875 }
876
877 assert(is_well_typed());
878}
879
880} // namespace data
881} // namespace mcrl2
A list of aterm objects.
Definition aterm_list.h:24
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:239
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
\brief A sort alias
Definition alias.h:26
\brief A basic sort
Definition basic_sort.h:26
\brief A container sort
const container_type & container_name() const
const sort_expression & element_sort() const
\brief A data equation
void add_mapping(const function_symbol &f)
Adds a mapping to this specification.
void add_equation(const data_equation &e)
Adds an equation to this specification.
void add_standard_mappings_and_equations(const sort_expression &sort, std::set< function_symbol > &mappings, std::set< data_equation > &equations, const bool skip_equations) const
const implementation_map & cpp_implemented_functions() const
Gets all equations in this specification including those that are system defined.
const function_symbol_vector & user_defined_mappings() const
Gets all user defined mappings in this specification.
const std::set< data_equation > & equations() const
Gets all equations in this specification including those that are system defined.
void find_associated_system_defined_data_types_for_a_sort(const sort_expression &sort, std::set< function_symbol > &constructors, std::set< function_symbol > &mappings, std::set< data_equation > &equations, implementation_map &cpp_implemented_functions, const bool skip_equations=false) const
Adds the system defined sorts to the sets with constructors, mappings, and equations for.
void insert_mappings_constructors_for_structured_sort(const structured_sort &sort, std::set< function_symbol > &constructors, std::set< function_symbol > &mappings, std::set< data_equation > &equations, const bool skip_equations) const
Adds constructors, mappings and equations for a structured sort to this specification,...
bool is_well_typed() const
Returns true if.
data_specification()
Default constructor. Generate a data specification that contains only booleans and positive numbers.
const data_equation_vector & user_defined_equations() const
Gets all user defined equations.
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
void add_constructor(const function_symbol &f)
Adds a constructor to this specification.
void get_system_defined_sorts_constructors_and_mappings(std::set< sort_expression > &sorts, std::set< function_symbol > &constructors, std::set< function_symbol > &mappings) const
This function provides a sample of all system defined sorts, constructors and mappings that contains ...
bool is_certainly_finite(const sort_expression &s) const
Checks whether a sort is certainly finite.
const function_symbol_vector & constructors() const
Gets all constructors including those that are system defined.
const function_symbol_vector & mappings() const
Gets all mappings in this specification including those that are system defined.
bool is_finite(const container_sort &s)
bool is_finite(const basic_sort &s)
bool is_finite_aux(const sort_expression &s)
bool is_finite(const sort_expression &s)
std::set< sort_expression > m_visiting
bool is_finite(const function_sort &s)
const data_specification & m_specification
finiteness_helper(const data_specification &specification)
bool is_finite(const structured_sort &s)
\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
\brief Container type for sets
\brief A sort expression
std::map< sort_expression, sort_expression > m_normalised_aliases
Table containing how sorts should be mapped to normalised sorts.
void add_system_defined_sort(const sort_expression &s)
Adds a sort to this specification, and marks it as system defined.
std::set< sort_expression > m_sorts_in_context
The sorts that occur are needed in this sort specification but are not explicitly defined as user def...
const std::set< sort_expression > & sorts() const
Gets the normalised sort declarations including those that are system defined. This is the set with a...
alias_vector m_user_defined_aliases
The basic sorts and structured sorts in the specification.
void sorts_are_not_necessarily_normalised_anymore() const
void add_alias(const alias &a)
Adds an alias (new name for a sort) to this specification.
void add_sort(const basic_sort &s)
Adds a sort to this specification.
void check_for_alias_loop(const sort_expression &s, std::set< sort_expression > sorts_already_seen, const bool toplevel=true) const
void import_system_defined_sorts(const CONTAINER &sorts)
void import_system_defined_sort(const sort_expression &sort)
Adds the system defined sorts in a sequence. The second argument is used to check which sorts are add...
\brief An argument of a constructor of a structured sort
\brief A constructor for a structured sort
function_symbol_vector constructor_functions(const sort_expression &s) const
const structured_sort_constructor_list & constructors() const
Standard exception class for reporting runtime errors.
Definition exception.h:27
add your file description here.
add your file description here.
The class data_specification.
Add your file description here.
The standard sort function_update.
The standard sort list.
add your file description here.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
bool check_rule_DataSpec(const Term &t)
bool check_data_spec_sorts(const Container &container, const SortContainer &sorts)
Returns true if the domain sorts and range sort of the given functions are contained in sorts.
function_symbol_vector bag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for bag.
Definition bag1.h:1529
data_equation_vector bag_generate_equations_code(const sort_expression &s)
Give all system defined equations for bag.
Definition bag1.h:1706
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:1612
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
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
function_symbol_vector bag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for bag.
Definition bag1.h:132
data_equation_vector bool_generate_equations_code()
Give all system defined equations for bool_.
Definition bool.h:502
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
implementation_map bool_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition bool.h:154
function_symbol_vector bool_generate_constructors_code()
Give all system defined constructors for bool_.
Definition bool.h:130
implementation_map bool_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for bool_.
Definition bool.h:458
function_symbol_vector bool_generate_functions_code()
Give all system defined mappings for bool_.
Definition bool.h:416
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
Definition fbag1.h:43
implementation_map fbag_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 fbag1.h:191
function_symbol_vector fbag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fbag.
Definition fbag1.h:165
implementation_map fbag_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for fbag.
Definition fbag1.h:832
bool is_fbag(const sort_expression &e)
Recogniser for sort expression FBag(s)
Definition fbag1.h:54
function_symbol_vector fbag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fbag.
Definition fbag1.h:777
data_equation_vector fbag_generate_equations_code(const sort_expression &s)
Give all system defined equations for fbag.
Definition fbag1.h:914
bool is_fset(const sort_expression &e)
Recogniser for sort expression FSet(s)
Definition fset1.h:52
function_symbol_vector fset_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fset.
Definition fset1.h:161
implementation_map fset_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 fset1.h:187
function_symbol_vector fset_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fset.
Definition fset1.h:645
implementation_map fset_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for fset.
Definition fset1.h:696
data_equation_vector fset_generate_equations_code(const sort_expression &s)
Give all system defined equations for fset.
Definition fset1.h:778
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset1.h:41
data_equation_vector int_generate_equations_code()
Give all system defined equations for int_.
Definition int1.h:1525
function_symbol_vector int_generate_constructors_code()
Give all system defined constructors for int_.
Definition int1.h:193
function_symbol_vector int_generate_functions_code()
Give all system defined mappings for int_.
Definition int1.h:1397
implementation_map int_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition int1.h:217
implementation_map int_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for int_.
Definition int1.h:1481
const basic_sort & int_()
Constructor for sort expression Int.
Definition int1.h:47
function_symbol_vector list_generate_functions_code(const sort_expression &s)
Give all system defined mappings for list.
Definition list1.h:764
implementation_map list_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for list.
Definition list1.h:819
data_equation_vector list_generate_equations_code(const sort_expression &s)
Give all system defined equations for list.
Definition list1.h:865
implementation_map list_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 list1.h:188
function_symbol_vector list_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for list.
Definition list1.h:162
container_sort list(const sort_expression &s)
Constructor for sort expression List(S)
Definition list1.h:42
bool is_list(const sort_expression &e)
Recogniser for sort expression List(s)
Definition list1.h:53
implementation_map machine_word_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for machine_word.
function_symbol_vector machine_word_generate_functions_code()
Give all system defined mappings for machine_word.
const basic_sort & machine_word()
Constructor for sort expression @word.
function_symbol_vector machine_word_generate_constructors_code()
Give all system defined constructors for machine_word.
implementation_map machine_word_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
data_equation_vector machine_word_generate_equations_code()
Give all system defined equations for machine_word.
data_equation_vector nat_generate_equations_code()
Give all system defined equations for nat.
Definition nat1.h:2290
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
implementation_map nat_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition nat1.h:281
function_symbol_vector nat_generate_functions_code()
Give all system defined mappings for nat.
Definition nat1.h:2100
implementation_map nat_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for nat.
Definition nat1.h:2198
const basic_sort & natpair()
Constructor for sort expression @NatPair.
Definition nat1.h:75
function_symbol_vector nat_generate_constructors_code()
Give all system defined constructors for nat.
Definition nat1.h:255
implementation_map pos_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for pos.
Definition pos1.h:753
function_symbol_vector pos_generate_functions_code()
Give all system defined mappings for pos.
Definition pos1.h:703
implementation_map pos_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition pos1.h:187
data_equation_vector pos_generate_equations_code()
Give all system defined equations for pos.
Definition pos1.h:833
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
function_symbol_vector pos_generate_constructors_code()
Give all system defined constructors for pos.
Definition pos1.h:163
data_equation_vector real_generate_equations_code()
Give all system defined equations for real_.
Definition real1.h:2010
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
function_symbol_vector real_generate_constructors_code()
Give all system defined constructors for real_.
Definition real1.h:70
function_symbol_vector real_generate_functions_code()
Give all system defined mappings for real_.
Definition real1.h:1842
bool is_set(const sort_expression &e)
Recogniser for sort expression Set(s)
Definition set1.h:53
function_symbol_vector set_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for set_.
Definition set1.h:130
implementation_map set_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for set_.
Definition set1.h:1178
implementation_map set_cpp_implementable_constructors(const sort_expression &s)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition set1.h:154
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set1.h:42
function_symbol_vector set_generate_functions_code(const sort_expression &s)
Give all system defined mappings for set_.
Definition set1.h:1107
data_equation_vector set_generate_equations_code(const sort_expression &s)
Give all system defined equations for set_.
Definition set1.h:1272
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
static sort_expression find_normal_form(const sort_expression &e, const std::multimap< sort_expression, sort_expression > &map1, std::set< sort_expression > sorts_already_seen=std::set< sort_expression >())
std::vector< alias > alias_vector
\brief vector of aliass
Definition alias.h:75
implementation_map function_update_cpp_implementable_mappings(const sort_expression &s, const sort_expression &t)
Give all system defined mappings that are to be implemented in C++ code for function_update.
bool is_untyped_possible_sorts(const atermpp::aterm &x)
Returns true if the term t is an expression for multiple possible sorts.
bool is_untyped_sort(const atermpp::aterm &x)
Returns true if the term t is the unknown sort.
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
std::string pp(const abstraction &x)
Definition data.cpp:39
void replace_sort_expressions(T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Definition replace.h:168
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
data_equation_vector function_update_generate_equations_code(const sort_expression &s, const sort_expression &t)
Give all system defined equations for function_update.
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
implementation_map function_update_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
function_symbol_vector function_update_generate_functions_code(const sort_expression &s, const sort_expression &t)
Give all system defined mappings for function_update.
bool is_alias(const atermpp::aterm &x)
Definition alias.h:81
std::vector< basic_sort > basic_sort_vector
vector of basic sorts
Definition basic_sort.h:94
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
add your file description here.
Substitution that maps a sort expression to a sort expression.