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 // Nat requires NatPair.
321 }
322 else if (is_function_sort(sort))
323 {
324 const function_sort& fsort=atermpp::down_cast<function_sort>(sort);
327 }
328 else if (is_container_sort(sort))
329 {
330 const sort_expression element_sort(container_sort(sort).element_sort());
331 // Import the element sort (which may be a complex sort also).
332 import_system_defined_sort(element_sort);
333 if (sort_list::is_list(sort))
334 {
335 import_system_defined_sort(sort_nat::nat()); // Required for lists.
336 }
337 else if (sort_set::is_set(sort))
338 {
340 // Import the functions from element_sort->Bool.
341 sort_expression_list element_sorts;
342 element_sorts.push_front(element_sort);
344 }
345 else if (sort_fset::is_fset(sort))
346 {
347 }
348 else if (sort_bag::is_bag(sort))
349 {
350 // Add the sorts Nat and set_(element_sort) to the specification.
351 import_system_defined_sort(sort_nat::nat()); // Required for bags.
354
355 // Add the function sort element_sort->Nat to the specification
356 sort_expression_list element_sorts ;
357 element_sorts.push_front(element_sort);
359 }
360 else if (sort_fbag::is_fbag(sort))
361 {
362 import_system_defined_sort(sort_nat::nat()); // Required for bags.
363 }
364 }
365 else if (is_structured_sort(sort))
366 {
367 structured_sort s_sort(sort);
369 for(const function_symbol& f: s_sort.constructor_functions(sort))
370 {
372 }
373 }
374}
375
376// The function below recalculates m_normalised_aliases, such that
377// it forms a confluent terminating rewriting system using which
378// sorts can be normalised.
379// This algorithm is described in the document: algorithm-for-sort-equivalence.tex in
380// the developers library of the mCRL2 toolset.
382{
383 // First reset the normalised aliases and the mappings and constructors that have been
384 // inherited to basic sort aliases during a previous round of sort normalisation.
385 m_normalised_aliases.clear();
386
387 // This is the first step of the algorithm.
388 // Check for loops in the aliases. The type checker should already have done this,
389 // but we check it again here. If there is a loop m_normalised_aliases will not be
390 // built.
391 for(const alias& a: m_user_defined_aliases)
392 {
393 std::set < sort_expression > sorts_already_seen; // Empty set.
394 try
395 {
396 check_for_alias_loop(a.name(),sorts_already_seen,true);
397 }
398 catch (mcrl2::runtime_error &)
399 {
400 mCRL2log(log::debug) << "Encountered an alias loop in the alias for " << a.name() <<". The normalised aliases are not constructed\n";
401 return;
402 }
403 }
404
405 // This is the second step of the algorithm.
406 // Copy m_normalised_aliases. All aliases are stored from left to right,
407 // except structured sorts, which are stored from right to left. The reason is
408 // that structured sorts can be recursive, and therefore, they cannot be
409 // rewritten from left to right, as this can cause sorts to be infinitely rewritten.
410
411 std::multimap< sort_expression, sort_expression > sort_aliases_to_be_investigated;
412 std::multimap< sort_expression, sort_expression > resulting_normalized_sort_aliases;
413
414 for(const alias& a: m_user_defined_aliases)
415 {
416 if (is_structured_sort(a.reference()))
417 {
418 sort_aliases_to_be_investigated.insert(std::pair<sort_expression,sort_expression>(a.reference(),a.name()));
419 }
420 else
421 {
422 resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression>(a.name(),a.reference()));
423 }
424 }
425
426 // Apply Knuth-Bendix completion to the rules in m_normalised_aliases.
427 for(; !sort_aliases_to_be_investigated.empty() ;)
428 {
429 const std::multimap< sort_expression, sort_expression >::iterator it=sort_aliases_to_be_investigated.begin();
430 const sort_expression lhs=it->first;
431 const sort_expression rhs=it->second;
432 sort_aliases_to_be_investigated.erase(it);
433
434 for(const std::pair<const sort_expression, sort_expression >& p: resulting_normalized_sort_aliases)
435 {
437
438 if (s1!=lhs)
439 {
440 // There is a conflict between the two sort rewrite rules.
441 assert(is_basic_sort(rhs));
442 // Choose the normal form on the basis of a lexicographical ordering. This guarantees
443 // uniqueness of normal forms over different tools. Ordering on addresses (as used previously)
444 // proved to be unstable over different tools.
445 const bool rhs_to_s1 = is_basic_sort(s1) && pp(basic_sort(s1))<=pp(rhs);
446 const sort_expression left_hand_side=(rhs_to_s1?rhs:s1);
447 const sort_expression pre_normal_form=(rhs_to_s1?s1:rhs);
448 assert(is_basic_sort(pre_normal_form));
449 const sort_expression& e1=pre_normal_form;
450 if (e1!=left_hand_side)
451 {
452 const sort_expression normalised_lhs=find_normal_form(left_hand_side,resulting_normalized_sort_aliases);
453 // Check whether the inserted sort rewrite rule is already in sort_aliases_to_be_investigated.
454 if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
455 sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
456 [&rhs](const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
457 == sort_aliases_to_be_investigated.upper_bound(normalised_lhs)) // Not found.
458 {
459 sort_aliases_to_be_investigated.insert(
460 std::pair<sort_expression,sort_expression > (normalised_lhs, e1));
461 }
462 }
463 }
464 else
465 {
467 if (s2!=p.first)
468 {
469 assert(is_basic_sort(p.second));
470 // Choose the normal form on the basis of a lexicographical ordering. This guarantees
471 // uniqueness of normal forms over different tools.
472 const bool i_second_to_s2 = is_basic_sort(s2) && pp(basic_sort(s2))<=pp(p.second);
473 const sort_expression left_hand_side=(i_second_to_s2?p.second:s2);
474 const sort_expression pre_normal_form=(i_second_to_s2?s2:p.second);
475 assert(is_basic_sort(pre_normal_form));
476 const sort_expression& e2=pre_normal_form;
477 if (e2!=left_hand_side)
478 {
479 const sort_expression normalised_lhs=find_normal_form(left_hand_side,resulting_normalized_sort_aliases);
480 // Check whether the inserted sort rewrite rule is already in sort_aliases_to_be_investigated.
481 if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
482 sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
483 [&rhs](const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
484 == sort_aliases_to_be_investigated.upper_bound(normalised_lhs)) // Not found.
485 {
486 sort_aliases_to_be_investigated.insert(
487 std::pair<sort_expression,sort_expression > (normalised_lhs,e2));
488 }
489 }
490 }
491 }
492 }
493 assert(lhs!=rhs);
494 const sort_expression normalised_lhs = find_normal_form(lhs,resulting_normalized_sort_aliases);
495 const sort_expression normalised_rhs = find_normal_form(rhs,resulting_normalized_sort_aliases);
496 if (normalised_lhs!=normalised_rhs)
497 {
498 resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression >(normalised_lhs,normalised_rhs));
499 }
500 }
501 // Copy resulting_normalized_sort_aliases into m_normalised_aliases, i.e. from multimap to map.
502 // If there are rules with equal left hand side, only one is arbitrarily chosen. Rewrite the
503 // right hand side to normal form.
504
505 for(const std::pair<const sort_expression,sort_expression>& p: resulting_normalized_sort_aliases)
506 {
507 const sort_expression normalised_rhs = find_normal_form(p.second,resulting_normalized_sort_aliases);
508 m_normalised_aliases[p.first]=normalised_rhs;
509
510 assert(p.first!=normalised_rhs);
511 }
512}
513
515// a given sort. If the boolean skip_equations is true, no equations are added.
517 const sort_expression& sort,
518 std::set < function_symbol >& constructors,
519 std::set < function_symbol >& mappings,
520 std::set < data_equation >& equations,
521 implementation_map& cpp_implemented_functions,
522 const bool skip_equations) const
523{
524 // add sorts, constructors, mappings and equations
525 if (sort == sort_bool::bool_())
526 {
528 constructors.insert(f.begin(), f.end());
530 mappings.insert(f.begin(), f.end());
532 cpp_implemented_functions.insert(f1.begin(), f1.end());
534 cpp_implemented_functions.insert(f1.begin(), f1.end());
535 if (!skip_equations)
536 {
538 equations.insert(e.begin(),e.end());
539 }
540 }
541 else if (sort == sort_real::real_())
542 {
544 constructors.insert(f.begin(),f.end());
546 mappings.insert(f.begin(),f.end());
548 cpp_implemented_functions.insert(f1.begin(), f1.end());
550 cpp_implemented_functions.insert(f1.begin(), f1.end());
551 if (!skip_equations)
552 {
554 equations.insert(e.begin(),e.end());
555 }
556 }
557 else if (sort == sort_int::int_())
558 {
560 constructors.insert(f.begin(),f.end());
562 mappings.insert(f.begin(),f.end());
564 cpp_implemented_functions.insert(f1.begin(), f1.end());
566 cpp_implemented_functions.insert(f1.begin(), f1.end());
567 if (!skip_equations)
568 {
570 equations.insert(e.begin(),e.end());
571 }
572 }
573 else if (sort == sort_nat::nat())
574 {
576 constructors.insert(f.begin(),f.end());
578 mappings.insert(f.begin(),f.end());
580 cpp_implemented_functions.insert(f1.begin(), f1.end());
582 cpp_implemented_functions.insert(f1.begin(), f1.end());
583 if (!skip_equations)
584 {
586 equations.insert(e.begin(),e.end());
587 }
588 }
589 else if (sort == sort_pos::pos())
590 {
592 constructors.insert(f.begin(),f.end());
594 mappings.insert(f.begin(),f.end());
596 cpp_implemented_functions.insert(f1.begin(), f1.end());
598 cpp_implemented_functions.insert(f1.begin(), f1.end());
599 if (!skip_equations)
600 {
602 equations.insert(e.begin(),e.end());
603 }
604 }
605 else if (is_function_sort(sort))
606 {
607 const sort_expression& t=function_sort(sort).codomain();
609 if (l.size()==1)
610 {
612 mappings.insert(f.begin(),f.end());
614 cpp_implemented_functions.insert(f1.begin(), f1.end());
616 cpp_implemented_functions.insert(f1.begin(), f1.end());
617 if (!skip_equations)
618 {
620 equations.insert(e.begin(),e.end());
621 }
622 }
623 }
624 else if (is_container_sort(sort))
625 {
626 sort_expression element_sort(container_sort(sort).element_sort());
627 if (sort_list::is_list(sort))
628 {
630 constructors.insert(f.begin(),f.end());
632 mappings.insert(f.begin(),f.end());
634 cpp_implemented_functions.insert(f1.begin(), f1.end());
636 cpp_implemented_functions.insert(f1.begin(), f1.end());
637 if (!skip_equations)
638 {
640 equations.insert(e.begin(),e.end());
641 }
642 }
643 else if (sort_set::is_set(sort))
644 {
645 sort_expression_list element_sorts;
646 element_sorts.push_front(element_sort);
648 constructors.insert(f.begin(),f.end());
650 mappings.insert(f.begin(),f.end());
652 cpp_implemented_functions.insert(f1.begin(), f1.end());
654 cpp_implemented_functions.insert(f1.begin(), f1.end());
655 if (!skip_equations)
656 {
658 equations.insert(e.begin(),e.end());
659 }
660 }
661 else if (sort_fset::is_fset(sort))
662 {
664 constructors.insert(f.begin(),f.end());
666 mappings.insert(f.begin(),f.end());
668 cpp_implemented_functions.insert(f1.begin(), f1.end());
670 cpp_implemented_functions.insert(f1.begin(), f1.end());
671 if (!skip_equations)
672 {
674 equations.insert(e.begin(),e.end());
675 }
676 }
677 else if (sort_bag::is_bag(sort))
678 {
679 sort_expression_list element_sorts;
680 element_sorts.push_front(element_sort);
682 constructors.insert(f.begin(),f.end());
684 mappings.insert(f.begin(),f.end());
686 cpp_implemented_functions.insert(f1.begin(), f1.end());
688 cpp_implemented_functions.insert(f1.begin(), f1.end());
689 if (!skip_equations)
690 {
692 equations.insert(e.begin(),e.end());
693 }
694 }
695 else if (sort_fbag::is_fbag(sort))
696 {
698 constructors.insert(f.begin(),f.end());
700 mappings.insert(f.begin(),f.end());
702 cpp_implemented_functions.insert(f1.begin(), f1.end());
704 cpp_implemented_functions.insert(f1.begin(), f1.end());
705 if (!skip_equations)
706 {
708 equations.insert(e.begin(),e.end());
709 }
710 }
711 }
712 else if (is_structured_sort(sort))
713 {
715 atermpp::down_cast<structured_sort>(sort),
716 constructors, mappings, equations, skip_equations);
717 }
719}
720
722 std::set < sort_expression >& sorts,
723 std::set < function_symbol >& constructors,
724 std::set <function_symbol >& mappings) const
725{
727
728 sorts.insert(sort_bool::bool_());
729 sorts.insert(sort_pos::pos());
730 sorts.insert(sort_nat::nat());
731 sorts.insert(sort_int::int_());
732 sorts.insert(sort_real::real_());
738
739 std::set < data_equation > dummy_equations;
740 for(const sort_expression& s: sorts)
741 {
743 }
744 assert(dummy_equations.size()==0);
745}
746
748{
749 // check 1)
751 {
752 std::clog << "data_specification::is_well_typed() failed: not all of the sorts appearing in the constructors "
753 << data::pp(constructors()) << " are declared in " << data::pp(sorts()) << std::endl;
754 return false;
755 }
756
757 // check 2)
759 {
760 std::clog << "data_specification::is_well_typed() failed: not all of the sorts appearing in the mappings "
761 << data::pp(mappings()) << " are declared in " << data::pp(sorts()) << std::endl;
762 return false;
763 }
764
765 return true;
766}
767
775void data_specification::build_from_aterm(const atermpp::aterm_appl& term)
776{
778
779 // Note backwards compatibility measure: alias is no longer a sort_expression
781 atermpp::down_cast<atermpp::term_list<atermpp::aterm_appl> >(atermpp::down_cast<atermpp::aterm_appl>(term[0])[0]);
782 const data::function_symbol_list term_constructors=
783 atermpp::down_cast<data::function_symbol_list>(atermpp::down_cast<atermpp::aterm_appl>(term[1])[0]);
784 const data::function_symbol_list term_mappings=
785 atermpp::down_cast<data::function_symbol_list>(atermpp::down_cast<atermpp::aterm_appl>(term[2])[0]);
786 const data::data_equation_list term_equations=
787 atermpp::down_cast<data::data_equation_list>(atermpp::down_cast<atermpp::aterm_appl>(term[3])[0]);
788
789 // Store the sorts and aliases.
790 for(const atermpp::aterm_appl& t: term_sorts)
791 {
792 if (data::is_alias(t)) // Compatibility with legacy code
793 {
794 add_alias(atermpp::down_cast<data::alias>(t));
795 }
796 else
797 {
798 add_sort(atermpp::down_cast<basic_sort>(t));
799 }
800 }
801
802 // Store the constructors.
803 for(const function_symbol& f: term_constructors)
804 {
806 }
807
808 // Store the mappings.
809 for(const function_symbol& f: term_mappings)
810 {
811 add_mapping(f);
812 }
813
814 // Store the equations.
815 for(const data_equation& e: term_equations)
816 {
817 add_equation(e);
818 }
819}
820
822 const alias_vector& aliases,
823 const function_symbol_vector& constructors,
824 const function_symbol_vector& user_defined_mappings,
825 const data_equation_vector& user_defined_equations)
826 : sort_specification(sorts, aliases)
827{
828 // Store the constructors.
829 for(const function_symbol& f: constructors)
830 {
832 }
833
834 // Store the mappings.
836 {
837 add_mapping(f);
838 }
839
840 // Store the equations.
842 {
843 add_equation(e);
844 }
845
846 assert(is_well_typed());
847}
848
849} // namespace data
850} // namespace mcrl2
A list of aterm objects.
Definition aterm_list.h:23
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:255
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:238
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.
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 ...
std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > > implementation_map
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:395
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 bag.h:1505
data_equation_vector bag_generate_equations_code(const sort_expression &s)
Give all system defined equations for bag.
Definition bag.h:1676
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 bag.h:1582
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 bag.h:156
bool is_bag(const sort_expression &e)
Recogniser for sort expression Bag(s)
Definition bag.h:55
container_sort bag(const sort_expression &s)
Constructor for sort expression Bag(S)
Definition bag.h:44
function_symbol_vector bag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for bag.
Definition bag.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 fbag.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 fbag.h:191
function_symbol_vector fbag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fbag.
Definition fbag.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 fbag.h:832
bool is_fbag(const sort_expression &e)
Recogniser for sort expression FBag(s)
Definition fbag.h:54
function_symbol_vector fbag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fbag.
Definition fbag.h:777
data_equation_vector fbag_generate_equations_code(const sort_expression &s)
Give all system defined equations for fbag.
Definition fbag.h:914
bool is_fset(const sort_expression &e)
Recogniser for sort expression FSet(s)
Definition fset.h:52
function_symbol_vector fset_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fset.
Definition fset.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 fset.h:187
function_symbol_vector fset_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fset.
Definition fset.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 fset.h:696
data_equation_vector fset_generate_equations_code(const sort_expression &s)
Give all system defined equations for fset.
Definition fset.h:778
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset.h:41
data_equation_vector int_generate_equations_code()
Give all system defined equations for int_.
Definition int.h:1525
function_symbol_vector int_generate_constructors_code()
Give all system defined constructors for int_.
Definition int.h:193
function_symbol_vector int_generate_functions_code()
Give all system defined mappings for int_.
Definition int.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 int.h:217
implementation_map int_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for int_.
Definition int.h:1481
const basic_sort & int_()
Constructor for sort expression Int.
Definition int.h:47
function_symbol_vector list_generate_functions_code(const sort_expression &s)
Give all system defined mappings for list.
Definition list.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 list.h:819
data_equation_vector list_generate_equations_code(const sort_expression &s)
Give all system defined equations for list.
Definition list.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 list.h:188
function_symbol_vector list_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for list.
Definition list.h:162
container_sort list(const sort_expression &s)
Constructor for sort expression List(S)
Definition list.h:42
bool is_list(const sort_expression &e)
Recogniser for sort expression List(s)
Definition list.h:53
data_equation_vector nat_generate_equations_code()
Give all system defined equations for nat.
Definition nat.h:2290
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat.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 nat.h:281
function_symbol_vector nat_generate_functions_code()
Give all system defined mappings for nat.
Definition nat.h:2100
implementation_map nat_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for nat.
Definition nat.h:2198
const basic_sort & natpair()
Constructor for sort expression @NatPair.
Definition nat.h:75
function_symbol_vector nat_generate_constructors_code()
Give all system defined constructors for nat.
Definition nat.h:255
implementation_map pos_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for pos.
Definition pos.h:753
function_symbol_vector pos_generate_functions_code()
Give all system defined mappings for pos.
Definition pos.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 pos.h:187
data_equation_vector pos_generate_equations_code()
Give all system defined equations for pos.
Definition pos.h:833
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos.h:45
function_symbol_vector pos_generate_constructors_code()
Give all system defined constructors for pos.
Definition pos.h:163
data_equation_vector real_generate_equations_code()
Give all system defined equations for real_.
Definition real.h:2010
const basic_sort & real_()
Constructor for sort expression Real.
Definition real.h:48
function_symbol_vector real_generate_constructors_code()
Give all system defined constructors for real_.
Definition real.h:70
function_symbol_vector real_generate_functions_code()
Give all system defined mappings for real_.
Definition real.h:1842
bool is_set(const sort_expression &e)
Recogniser for sort expression Set(s)
Definition set.h:53
function_symbol_vector set_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for set_.
Definition set.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 set.h:1160
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 set.h:154
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set.h:42
function_symbol_vector set_generate_functions_code(const sort_expression &s)
Give all system defined mappings for set_.
Definition set.h:1095
data_equation_vector set_generate_equations_code(const sort_expression &s)
Give all system defined equations for set_.
Definition set.h:1254
bool is_alias(const atermpp::aterm_appl &x)
Definition alias.h:81
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_appl &x)
Returns true if the term t is an expression for multiple possible sorts.
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
bool is_untyped_sort(const atermpp::aterm_appl &x)
Returns true if the term t is the unknown sort.
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_structured_sort(const atermpp::aterm_appl &x)
Returns true if the term t is a structured sort.
bool is_basic_sort(const atermpp::aterm_appl &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.
implementation_map function_update_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
bool is_function_sort(const atermpp::aterm_appl &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:85
function_symbol_vector function_update_generate_functions_code(const sort_expression &s, const sort_expression &t)
Give all system defined mappings for function_update.
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
bool is_container_sort(const atermpp::aterm_appl &x)
Returns true if the term t is a container sort.
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.