Line data Source code
1 : // Author(s): Jeroen Keiren
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/data/set.h
10 : /// \brief The standard sort set_.
11 : ///
12 : /// This file was generated from the data sort specification
13 : /// mcrl2/data/build/set.spec.
14 :
15 : #ifndef MCRL2_DATA_SET_H
16 : #define MCRL2_DATA_SET_H
17 :
18 : #include "functional" // std::function
19 : #include "mcrl2/utilities/exception.h"
20 : #include "mcrl2/data/basic_sort.h"
21 : #include "mcrl2/data/function_sort.h"
22 : #include "mcrl2/data/function_symbol.h"
23 : #include "mcrl2/data/application.h"
24 : #include "mcrl2/data/data_equation.h"
25 : #include "mcrl2/data/standard.h"
26 : #include "mcrl2/data/forall.h"
27 : #include "mcrl2/data/container_sort.h"
28 : #include "mcrl2/data/bool.h"
29 : #include "mcrl2/data/fset.h"
30 :
31 : namespace mcrl2 {
32 :
33 : namespace data {
34 :
35 : /// \brief Namespace for system defined sort set_.
36 : namespace sort_set {
37 :
38 : /// \brief Constructor for sort expression Set(S)
39 : /// \param s A sort expression
40 : /// \return Sort expression set_(s)
41 : inline
42 165009 : container_sort set_(const sort_expression& s)
43 : {
44 165009 : container_sort set_(set_container(), s);
45 165009 : return set_;
46 : }
47 :
48 : /// \brief Recogniser for sort expression Set(s)
49 : /// \param e A sort expression
50 : /// \return true iff e is a container sort of which the name matches
51 : /// set_
52 : inline
53 38210 : bool is_set(const sort_expression& e)
54 : {
55 38210 : if (is_container_sort(e))
56 : {
57 3853 : return container_sort(e).container_name() == set_container();
58 : }
59 34357 : return false;
60 : }
61 :
62 :
63 : /// \brief Generate identifier \@set.
64 : /// \return Identifier \@set.
65 : inline
66 67974 : const core::identifier_string& constructor_name()
67 : {
68 67974 : static core::identifier_string constructor_name = core::identifier_string("@set");
69 67974 : return constructor_name;
70 : }
71 :
72 : /// \brief Constructor for function symbol \@set.
73 : /// \param s A sort expression.
74 : /// \return Function symbol constructor.
75 : inline
76 8865 : function_symbol constructor(const sort_expression& s)
77 : {
78 17730 : function_symbol constructor(constructor_name(), make_function_sort_(make_function_sort_(s, sort_bool::bool_()), sort_fset::fset(s), set_(s)));
79 8865 : return constructor;
80 : }
81 :
82 : /// \brief Recogniser for function \@set.
83 : /// \param e A data expression.
84 : /// \return true iff e is the function symbol matching \@set.
85 : inline
86 8306 : bool is_constructor_function_symbol(const atermpp::aterm_appl& e)
87 : {
88 8306 : if (is_function_symbol(e))
89 : {
90 7464 : return atermpp::down_cast<function_symbol>(e).name() == constructor_name();
91 : }
92 842 : return false;
93 : }
94 :
95 : /// \brief Application of function symbol \@set.
96 : /// \param s A sort expression.
97 : /// \param arg0 A data expression.
98 : /// \param arg1 A data expression.
99 : /// \return Application of \@set to a number of arguments.
100 : inline
101 3933 : application constructor(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
102 : {
103 7866 : return sort_set::constructor(s)(arg0, arg1);
104 : }
105 :
106 : /// \brief Make an application of function symbol \@set.
107 : /// \param result The data expression where the \@set expression is put.
108 : /// \param s A sort expression.
109 : /// \param arg0 A data expression.
110 : /// \param arg1 A data expression.
111 : inline
112 : void make_constructor(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
113 : {
114 : make_application(result, sort_set::constructor(s),arg0, arg1);
115 : }
116 :
117 : /// \brief Recogniser for application of \@set.
118 : /// \param e A data expression.
119 : /// \return true iff e is an application of function symbol constructor to a
120 : /// number of arguments.
121 : inline
122 8306 : bool is_constructor_application(const atermpp::aterm_appl& e)
123 : {
124 8306 : return is_application(e) && is_constructor_function_symbol(atermpp::down_cast<application>(e).head());
125 : }
126 : /// \brief Give all system defined constructors for set_.
127 : /// \param s A sort expression.
128 : /// \return All system defined constructors for set_.
129 : inline
130 283 : function_symbol_vector set_generate_constructors_code(const sort_expression& s)
131 : {
132 283 : function_symbol_vector result;
133 283 : result.push_back(sort_set::constructor(s));
134 :
135 283 : return result;
136 0 : }
137 : /// \brief Give all defined constructors which can be used in mCRL2 specs for set_.
138 : /// \param s A sort expression.
139 : /// \return All system defined constructors that can be used in an mCRL2 specification for set_.
140 : inline
141 : function_symbol_vector set_mCRL2_usable_constructors(const sort_expression& s)
142 : {
143 : function_symbol_vector result;
144 : result.push_back(sort_set::constructor(s));
145 :
146 : return result;
147 : }
148 : // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
149 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
150 : /// \brief Give all system defined constructors which have an implementation in C++ and not in rewrite rules for set_.
151 : /// \param s A sort expression.
152 : /// \return All system defined constructors that are to be implemented in C++ for set_.
153 : inline
154 283 : implementation_map set_cpp_implementable_constructors(const sort_expression& s)
155 : {
156 283 : implementation_map result;
157 : static_cast< void >(s); // suppress unused variable warnings
158 283 : return result;
159 : }
160 :
161 : /// \brief Generate identifier \@setfset.
162 : /// \return Identifier \@setfset.
163 : inline
164 7587 : const core::identifier_string& set_fset_name()
165 : {
166 7587 : static core::identifier_string set_fset_name = core::identifier_string("@setfset");
167 7587 : return set_fset_name;
168 : }
169 :
170 : /// \brief Constructor for function symbol \@setfset.
171 : /// \param s A sort expression.
172 : /// \return Function symbol set_fset.
173 : inline
174 635 : function_symbol set_fset(const sort_expression& s)
175 : {
176 1270 : function_symbol set_fset(set_fset_name(), make_function_sort_(sort_fset::fset(s), set_(s)));
177 635 : return set_fset;
178 : }
179 :
180 : /// \brief Recogniser for function \@setfset.
181 : /// \param e A data expression.
182 : /// \return true iff e is the function symbol matching \@setfset.
183 : inline
184 7794 : bool is_set_fset_function_symbol(const atermpp::aterm_appl& e)
185 : {
186 7794 : if (is_function_symbol(e))
187 : {
188 6952 : return atermpp::down_cast<function_symbol>(e).name() == set_fset_name();
189 : }
190 842 : return false;
191 : }
192 :
193 : /// \brief Application of function symbol \@setfset.
194 : /// \param s A sort expression.
195 : /// \param arg0 A data expression.
196 : /// \return Application of \@setfset to a number of arguments.
197 : inline
198 352 : application set_fset(const sort_expression& s, const data_expression& arg0)
199 : {
200 704 : return sort_set::set_fset(s)(arg0);
201 : }
202 :
203 : /// \brief Make an application of function symbol \@setfset.
204 : /// \param result The data expression where the \@setfset expression is put.
205 : /// \param s A sort expression.
206 : /// \param arg0 A data expression.
207 : inline
208 : void make_set_fset(data_expression& result, const sort_expression& s, const data_expression& arg0)
209 : {
210 : make_application(result, sort_set::set_fset(s),arg0);
211 : }
212 :
213 : /// \brief Recogniser for application of \@setfset.
214 : /// \param e A data expression.
215 : /// \return true iff e is an application of function symbol set_fset to a
216 : /// number of arguments.
217 : inline
218 7794 : bool is_set_fset_application(const atermpp::aterm_appl& e)
219 : {
220 7794 : return is_application(e) && is_set_fset_function_symbol(atermpp::down_cast<application>(e).head());
221 : }
222 :
223 : /// \brief Generate identifier \@setcomp.
224 : /// \return Identifier \@setcomp.
225 : inline
226 7371 : const core::identifier_string& set_comprehension_name()
227 : {
228 7371 : static core::identifier_string set_comprehension_name = core::identifier_string("@setcomp");
229 7371 : return set_comprehension_name;
230 : }
231 :
232 : /// \brief Constructor for function symbol \@setcomp.
233 : /// \param s A sort expression.
234 : /// \return Function symbol set_comprehension.
235 : inline
236 567 : function_symbol set_comprehension(const sort_expression& s)
237 : {
238 1134 : function_symbol set_comprehension(set_comprehension_name(), make_function_sort_(make_function_sort_(s, sort_bool::bool_()), set_(s)));
239 567 : return set_comprehension;
240 : }
241 :
242 : /// \brief Recogniser for function \@setcomp.
243 : /// \param e A data expression.
244 : /// \return true iff e is the function symbol matching \@setcomp.
245 : inline
246 7646 : bool is_set_comprehension_function_symbol(const atermpp::aterm_appl& e)
247 : {
248 7646 : if (is_function_symbol(e))
249 : {
250 6804 : return atermpp::down_cast<function_symbol>(e).name() == set_comprehension_name();
251 : }
252 842 : return false;
253 : }
254 :
255 : /// \brief Application of function symbol \@setcomp.
256 : /// \param s A sort expression.
257 : /// \param arg0 A data expression.
258 : /// \return Application of \@setcomp to a number of arguments.
259 : inline
260 284 : application set_comprehension(const sort_expression& s, const data_expression& arg0)
261 : {
262 568 : return sort_set::set_comprehension(s)(arg0);
263 : }
264 :
265 : /// \brief Make an application of function symbol \@setcomp.
266 : /// \param result The data expression where the \@setcomp expression is put.
267 : /// \param s A sort expression.
268 : /// \param arg0 A data expression.
269 : inline
270 : void make_set_comprehension(data_expression& result, const sort_expression& s, const data_expression& arg0)
271 : {
272 : make_application(result, sort_set::set_comprehension(s),arg0);
273 : }
274 :
275 : /// \brief Recogniser for application of \@setcomp.
276 : /// \param e A data expression.
277 : /// \return true iff e is an application of function symbol set_comprehension to a
278 : /// number of arguments.
279 : inline
280 7646 : bool is_set_comprehension_application(const atermpp::aterm_appl& e)
281 : {
282 7646 : return is_application(e) && is_set_comprehension_function_symbol(atermpp::down_cast<application>(e).head());
283 : }
284 :
285 : /// \brief Generate identifier in.
286 : /// \return Identifier in.
287 : inline
288 17642 : const core::identifier_string& in_name()
289 : {
290 17642 : static core::identifier_string in_name = core::identifier_string("in");
291 17642 : return in_name;
292 : }
293 :
294 : // This function is not intended for public use and therefore not documented in Doxygen.
295 : inline
296 10840 : function_symbol in(const sort_expression& , const sort_expression& s0, const sort_expression& s1)
297 : {
298 10840 : sort_expression target_sort(sort_bool::bool_());
299 10840 : function_symbol in(in_name(), make_function_sort_(s0, s1, target_sort));
300 21680 : return in;
301 10840 : }
302 :
303 : /// \brief Recogniser for function in.
304 : /// \param e A data expression.
305 : /// \return true iff e is the function symbol matching in.
306 : inline
307 7644 : bool is_in_function_symbol(const atermpp::aterm_appl& e)
308 : {
309 7644 : if (is_function_symbol(e))
310 : {
311 6802 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
312 6802 : return f.name() == in_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
313 : }
314 842 : return false;
315 : }
316 :
317 : /// \brief Application of function symbol in.
318 : /// \param s A sort expression.
319 : /// \param arg0 A data expression.
320 : /// \param arg1 A data expression.
321 : /// \return Application of in to a number of arguments.
322 : inline
323 1259 : application in(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
324 : {
325 2518 : return sort_set::in(s, arg0.sort(), arg1.sort())(arg0, arg1);
326 : }
327 :
328 : /// \brief Make an application of function symbol in.
329 : /// \param result The data expression where the in expression is put.
330 : /// \param s A sort expression.
331 : /// \param arg0 A data expression.
332 : /// \param arg1 A data expression.
333 : inline
334 : void make_in(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
335 : {
336 : make_application(result, sort_set::in(s, arg0.sort(), arg1.sort()),arg0, arg1);
337 : }
338 :
339 : /// \brief Recogniser for application of in.
340 : /// \param e A data expression.
341 : /// \return true iff e is an application of function symbol in to a
342 : /// number of arguments.
343 : inline
344 7644 : bool is_in_application(const atermpp::aterm_appl& e)
345 : {
346 7644 : return is_application(e) && is_in_function_symbol(atermpp::down_cast<application>(e).head());
347 : }
348 :
349 : /// \brief Generate identifier !.
350 : /// \return Identifier !.
351 : inline
352 64007 : const core::identifier_string& complement_name()
353 : {
354 64007 : static core::identifier_string complement_name = core::identifier_string("!");
355 64007 : return complement_name;
356 : }
357 :
358 : /// \brief Constructor for function symbol !.
359 : /// \param s A sort expression.
360 : /// \return Function symbol complement.
361 : inline
362 5502 : function_symbol complement(const sort_expression& s)
363 : {
364 11004 : function_symbol complement(complement_name(), make_function_sort_(set_(s), set_(s)));
365 5502 : return complement;
366 : }
367 :
368 : /// \brief Recogniser for function !.
369 : /// \param e A data expression.
370 : /// \return true iff e is the function symbol matching !.
371 : inline
372 7644 : bool is_complement_function_symbol(const atermpp::aterm_appl& e)
373 : {
374 7644 : if (is_function_symbol(e))
375 : {
376 6802 : return atermpp::down_cast<function_symbol>(e).name() == complement_name();
377 : }
378 842 : return false;
379 : }
380 :
381 : /// \brief Application of function symbol !.
382 : /// \param s A sort expression.
383 : /// \param arg0 A data expression.
384 : /// \return Application of ! to a number of arguments.
385 : inline
386 570 : application complement(const sort_expression& s, const data_expression& arg0)
387 : {
388 1140 : return sort_set::complement(s)(arg0);
389 : }
390 :
391 : /// \brief Make an application of function symbol !.
392 : /// \param result The data expression where the ! expression is put.
393 : /// \param s A sort expression.
394 : /// \param arg0 A data expression.
395 : inline
396 : void make_complement(data_expression& result, const sort_expression& s, const data_expression& arg0)
397 : {
398 : make_application(result, sort_set::complement(s),arg0);
399 : }
400 :
401 : /// \brief Recogniser for application of !.
402 : /// \param e A data expression.
403 : /// \return true iff e is an application of function symbol complement to a
404 : /// number of arguments.
405 : inline
406 7644 : bool is_complement_application(const atermpp::aterm_appl& e)
407 : {
408 7644 : return is_application(e) && is_complement_function_symbol(atermpp::down_cast<application>(e).head());
409 : }
410 :
411 : /// \brief Generate identifier +.
412 : /// \return Identifier +.
413 : inline
414 97593 : const core::identifier_string& union_name()
415 : {
416 97593 : static core::identifier_string union_name = core::identifier_string("+");
417 97593 : return union_name;
418 : }
419 :
420 : // This function is not intended for public use and therefore not documented in Doxygen.
421 : inline
422 13546 : function_symbol union_(const sort_expression& s, const sort_expression& s0, const sort_expression& s1)
423 : {
424 13546 : sort_expression target_sort;
425 13546 : if (s0 == set_(s) && s1 == set_(s))
426 : {
427 8897 : target_sort = set_(s);
428 : }
429 4649 : else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
430 : {
431 4649 : target_sort = sort_fset::fset(s);
432 : }
433 : else
434 : {
435 0 : throw mcrl2::runtime_error("Cannot compute target sort for union_ with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
436 : }
437 :
438 13546 : function_symbol union_(union_name(), make_function_sort_(s0, s1, target_sort));
439 27092 : return union_;
440 13546 : }
441 :
442 : /// \brief Recogniser for function +.
443 : /// \param e A data expression.
444 : /// \return true iff e is the function symbol matching +.
445 : inline
446 26267 : bool is_union_function_symbol(const atermpp::aterm_appl& e)
447 : {
448 26267 : if (is_function_symbol(e))
449 : {
450 25033 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
451 25033 : return f.name() == union_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
452 : }
453 1234 : return false;
454 : }
455 :
456 : /// \brief Application of function symbol +.
457 : /// \param s A sort expression.
458 : /// \param arg0 A data expression.
459 : /// \param arg1 A data expression.
460 : /// \return Application of + to a number of arguments.
461 : inline
462 3965 : application union_(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
463 : {
464 7930 : return sort_set::union_(s, arg0.sort(), arg1.sort())(arg0, arg1);
465 : }
466 :
467 : /// \brief Make an application of function symbol +.
468 : /// \param result The data expression where the + expression is put.
469 : /// \param s A sort expression.
470 : /// \param arg0 A data expression.
471 : /// \param arg1 A data expression.
472 : inline
473 : void make_union_(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
474 : {
475 : make_application(result, sort_set::union_(s, arg0.sort(), arg1.sort()),arg0, arg1);
476 : }
477 :
478 : /// \brief Recogniser for application of +.
479 : /// \param e A data expression.
480 : /// \return true iff e is an application of function symbol union_ to a
481 : /// number of arguments.
482 : inline
483 26267 : bool is_union_application(const atermpp::aterm_appl& e)
484 : {
485 26267 : return is_application(e) && is_union_function_symbol(atermpp::down_cast<application>(e).head());
486 : }
487 :
488 : /// \brief Generate identifier *.
489 : /// \return Identifier *.
490 : inline
491 82598 : const core::identifier_string& intersection_name()
492 : {
493 82598 : static core::identifier_string intersection_name = core::identifier_string("*");
494 82598 : return intersection_name;
495 : }
496 :
497 : // This function is not intended for public use and therefore not documented in Doxygen.
498 : inline
499 14116 : function_symbol intersection(const sort_expression& s, const sort_expression& s0, const sort_expression& s1)
500 : {
501 14116 : sort_expression target_sort;
502 14116 : if (s0 == set_(s) && s1 == set_(s))
503 : {
504 9465 : target_sort = set_(s);
505 : }
506 4651 : else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
507 : {
508 4651 : target_sort = sort_fset::fset(s);
509 : }
510 : else
511 : {
512 0 : throw mcrl2::runtime_error("Cannot compute target sort for intersection with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
513 : }
514 :
515 14116 : function_symbol intersection(intersection_name(), make_function_sort_(s0, s1, target_sort));
516 28232 : return intersection;
517 14116 : }
518 :
519 : /// \brief Recogniser for function *.
520 : /// \param e A data expression.
521 : /// \return true iff e is the function symbol matching *.
522 : inline
523 25201 : bool is_intersection_function_symbol(const atermpp::aterm_appl& e)
524 : {
525 25201 : if (is_function_symbol(e))
526 : {
527 23967 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
528 23967 : return f.name() == intersection_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
529 : }
530 1234 : return false;
531 : }
532 :
533 : /// \brief Application of function symbol *.
534 : /// \param s A sort expression.
535 : /// \param arg0 A data expression.
536 : /// \param arg1 A data expression.
537 : /// \return Application of * to a number of arguments.
538 : inline
539 4533 : application intersection(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
540 : {
541 9066 : return sort_set::intersection(s, arg0.sort(), arg1.sort())(arg0, arg1);
542 : }
543 :
544 : /// \brief Make an application of function symbol *.
545 : /// \param result The data expression where the * expression is put.
546 : /// \param s A sort expression.
547 : /// \param arg0 A data expression.
548 : /// \param arg1 A data expression.
549 : inline
550 : void make_intersection(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
551 : {
552 : make_application(result, sort_set::intersection(s, arg0.sort(), arg1.sort()),arg0, arg1);
553 : }
554 :
555 : /// \brief Recogniser for application of *.
556 : /// \param e A data expression.
557 : /// \return true iff e is an application of function symbol intersection to a
558 : /// number of arguments.
559 : inline
560 25201 : bool is_intersection_application(const atermpp::aterm_appl& e)
561 : {
562 25201 : return is_application(e) && is_intersection_function_symbol(atermpp::down_cast<application>(e).head());
563 : }
564 :
565 : /// \brief Generate identifier -.
566 : /// \return Identifier -.
567 : inline
568 82980 : const core::identifier_string& difference_name()
569 : {
570 82980 : static core::identifier_string difference_name = core::identifier_string("-");
571 82980 : return difference_name;
572 : }
573 :
574 : // This function is not intended for public use and therefore not documented in Doxygen.
575 : inline
576 9868 : function_symbol difference(const sort_expression& s, const sort_expression& s0, const sort_expression& s1)
577 : {
578 9868 : sort_expression target_sort;
579 9868 : if (s0 == set_(s) && s1 == set_(s))
580 : {
581 5219 : target_sort = set_(s);
582 : }
583 4649 : else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
584 : {
585 4649 : target_sort = sort_fset::fset(s);
586 : }
587 : else
588 : {
589 0 : throw mcrl2::runtime_error("Cannot compute target sort for difference with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
590 : }
591 :
592 9868 : function_symbol difference(difference_name(), make_function_sort_(s0, s1, target_sort));
593 19736 : return difference;
594 9868 : }
595 :
596 : /// \brief Recogniser for function -.
597 : /// \param e A data expression.
598 : /// \return true iff e is the function symbol matching -.
599 : inline
600 26122 : bool is_difference_function_symbol(const atermpp::aterm_appl& e)
601 : {
602 26122 : if (is_function_symbol(e))
603 : {
604 24888 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
605 24888 : return f.name() == difference_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
606 : }
607 1234 : return false;
608 : }
609 :
610 : /// \brief Application of function symbol -.
611 : /// \param s A sort expression.
612 : /// \param arg0 A data expression.
613 : /// \param arg1 A data expression.
614 : /// \return Application of - to a number of arguments.
615 : inline
616 287 : application difference(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
617 : {
618 574 : return sort_set::difference(s, arg0.sort(), arg1.sort())(arg0, arg1);
619 : }
620 :
621 : /// \brief Make an application of function symbol -.
622 : /// \param result The data expression where the - expression is put.
623 : /// \param s A sort expression.
624 : /// \param arg0 A data expression.
625 : /// \param arg1 A data expression.
626 : inline
627 : void make_difference(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
628 : {
629 : make_application(result, sort_set::difference(s, arg0.sort(), arg1.sort()),arg0, arg1);
630 : }
631 :
632 : /// \brief Recogniser for application of -.
633 : /// \param e A data expression.
634 : /// \return true iff e is an application of function symbol difference to a
635 : /// number of arguments.
636 : inline
637 26122 : bool is_difference_application(const atermpp::aterm_appl& e)
638 : {
639 26122 : return is_application(e) && is_difference_function_symbol(atermpp::down_cast<application>(e).head());
640 : }
641 :
642 : /// \brief Generate identifier \@false_.
643 : /// \return Identifier \@false_.
644 : inline
645 60242 : const core::identifier_string& false_function_name()
646 : {
647 60242 : static core::identifier_string false_function_name = core::identifier_string("@false_");
648 60242 : return false_function_name;
649 : }
650 :
651 : /// \brief Constructor for function symbol \@false_.
652 : /// \param s A sort expression.
653 : /// \return Function symbol false_function.
654 : inline
655 8580 : function_symbol false_function(const sort_expression& s)
656 : {
657 8580 : function_symbol false_function(false_function_name(), make_function_sort_(s, sort_bool::bool_()));
658 8580 : return false_function;
659 : }
660 :
661 : /// \brief Recogniser for function \@false_.
662 : /// \param e A data expression.
663 : /// \return true iff e is the function symbol matching \@false_.
664 : inline
665 145 : bool is_false_function_function_symbol(const atermpp::aterm_appl& e)
666 : {
667 145 : if (is_function_symbol(e))
668 : {
669 33 : return atermpp::down_cast<function_symbol>(e).name() == false_function_name();
670 : }
671 112 : return false;
672 : }
673 :
674 : /// \brief Application of function symbol \@false_.
675 : /// \param s A sort expression.
676 : /// \param arg0 A data expression.
677 : /// \return Application of \@false_ to a number of arguments.
678 : inline
679 283 : application false_function(const sort_expression& s, const data_expression& arg0)
680 : {
681 566 : return sort_set::false_function(s)(arg0);
682 : }
683 :
684 : /// \brief Make an application of function symbol \@false_.
685 : /// \param result The data expression where the \@false_ expression is put.
686 : /// \param s A sort expression.
687 : /// \param arg0 A data expression.
688 : inline
689 : void make_false_function(data_expression& result, const sort_expression& s, const data_expression& arg0)
690 : {
691 : make_application(result, sort_set::false_function(s),arg0);
692 : }
693 :
694 : /// \brief Recogniser for application of \@false_.
695 : /// \param e A data expression.
696 : /// \return true iff e is an application of function symbol false_function to a
697 : /// number of arguments.
698 : inline
699 0 : bool is_false_function_application(const atermpp::aterm_appl& e)
700 : {
701 0 : return is_application(e) && is_false_function_function_symbol(atermpp::down_cast<application>(e).head());
702 : }
703 :
704 : /// \brief Generate identifier \@true_.
705 : /// \return Identifier \@true_.
706 : inline
707 3566 : const core::identifier_string& true_function_name()
708 : {
709 3566 : static core::identifier_string true_function_name = core::identifier_string("@true_");
710 3566 : return true_function_name;
711 : }
712 :
713 : /// \brief Constructor for function symbol \@true_.
714 : /// \param s A sort expression.
715 : /// \return Function symbol true_function.
716 : inline
717 3538 : function_symbol true_function(const sort_expression& s)
718 : {
719 3538 : function_symbol true_function(true_function_name(), make_function_sort_(s, sort_bool::bool_()));
720 3538 : return true_function;
721 : }
722 :
723 : /// \brief Recogniser for function \@true_.
724 : /// \param e A data expression.
725 : /// \return true iff e is the function symbol matching \@true_.
726 : inline
727 140 : bool is_true_function_function_symbol(const atermpp::aterm_appl& e)
728 : {
729 140 : if (is_function_symbol(e))
730 : {
731 28 : return atermpp::down_cast<function_symbol>(e).name() == true_function_name();
732 : }
733 112 : return false;
734 : }
735 :
736 : /// \brief Application of function symbol \@true_.
737 : /// \param s A sort expression.
738 : /// \param arg0 A data expression.
739 : /// \return Application of \@true_ to a number of arguments.
740 : inline
741 283 : application true_function(const sort_expression& s, const data_expression& arg0)
742 : {
743 566 : return sort_set::true_function(s)(arg0);
744 : }
745 :
746 : /// \brief Make an application of function symbol \@true_.
747 : /// \param result The data expression where the \@true_ expression is put.
748 : /// \param s A sort expression.
749 : /// \param arg0 A data expression.
750 : inline
751 : void make_true_function(data_expression& result, const sort_expression& s, const data_expression& arg0)
752 : {
753 : make_application(result, sort_set::true_function(s),arg0);
754 : }
755 :
756 : /// \brief Recogniser for application of \@true_.
757 : /// \param e A data expression.
758 : /// \return true iff e is an application of function symbol true_function to a
759 : /// number of arguments.
760 : inline
761 0 : bool is_true_function_application(const atermpp::aterm_appl& e)
762 : {
763 0 : return is_application(e) && is_true_function_function_symbol(atermpp::down_cast<application>(e).head());
764 : }
765 :
766 : /// \brief Generate identifier \@not_.
767 : /// \return Identifier \@not_.
768 : inline
769 1415 : const core::identifier_string& not_function_name()
770 : {
771 1415 : static core::identifier_string not_function_name = core::identifier_string("@not_");
772 1415 : return not_function_name;
773 : }
774 :
775 : /// \brief Constructor for function symbol \@not_.
776 : /// \param s A sort expression.
777 : /// \return Function symbol not_function.
778 : inline
779 1415 : function_symbol not_function(const sort_expression& s)
780 : {
781 2830 : function_symbol not_function(not_function_name(), make_function_sort_(make_function_sort_(s, sort_bool::bool_()), make_function_sort_(s, sort_bool::bool_())));
782 1415 : return not_function;
783 : }
784 :
785 : /// \brief Recogniser for function \@not_.
786 : /// \param e A data expression.
787 : /// \return true iff e is the function symbol matching \@not_.
788 : inline
789 0 : bool is_not_function_function_symbol(const atermpp::aterm_appl& e)
790 : {
791 0 : if (is_function_symbol(e))
792 : {
793 0 : return atermpp::down_cast<function_symbol>(e).name() == not_function_name();
794 : }
795 0 : return false;
796 : }
797 :
798 : /// \brief Application of function symbol \@not_.
799 : /// \param s A sort expression.
800 : /// \param arg0 A data expression.
801 : /// \return Application of \@not_ to a number of arguments.
802 : inline
803 1132 : application not_function(const sort_expression& s, const data_expression& arg0)
804 : {
805 2264 : return sort_set::not_function(s)(arg0);
806 : }
807 :
808 : /// \brief Make an application of function symbol \@not_.
809 : /// \param result The data expression where the \@not_ expression is put.
810 : /// \param s A sort expression.
811 : /// \param arg0 A data expression.
812 : inline
813 : void make_not_function(data_expression& result, const sort_expression& s, const data_expression& arg0)
814 : {
815 : make_application(result, sort_set::not_function(s),arg0);
816 : }
817 :
818 : /// \brief Recogniser for application of \@not_.
819 : /// \param e A data expression.
820 : /// \return true iff e is an application of function symbol not_function to a
821 : /// number of arguments.
822 : inline
823 0 : bool is_not_function_application(const atermpp::aterm_appl& e)
824 : {
825 0 : return is_application(e) && is_not_function_function_symbol(atermpp::down_cast<application>(e).head());
826 : }
827 :
828 : /// \brief Generate identifier \@and_.
829 : /// \return Identifier \@and_.
830 : inline
831 2264 : const core::identifier_string& and_function_name()
832 : {
833 2264 : static core::identifier_string and_function_name = core::identifier_string("@and_");
834 2264 : return and_function_name;
835 : }
836 :
837 : /// \brief Constructor for function symbol \@and_.
838 : /// \param s A sort expression.
839 : /// \return Function symbol and_function.
840 : inline
841 2264 : function_symbol and_function(const sort_expression& s)
842 : {
843 4528 : function_symbol and_function(and_function_name(), make_function_sort_(make_function_sort_(s, sort_bool::bool_()), make_function_sort_(s, sort_bool::bool_()), make_function_sort_(s, sort_bool::bool_())));
844 2264 : return and_function;
845 : }
846 :
847 : /// \brief Recogniser for function \@and_.
848 : /// \param e A data expression.
849 : /// \return true iff e is the function symbol matching \@and_.
850 : inline
851 0 : bool is_and_function_function_symbol(const atermpp::aterm_appl& e)
852 : {
853 0 : if (is_function_symbol(e))
854 : {
855 0 : return atermpp::down_cast<function_symbol>(e).name() == and_function_name();
856 : }
857 0 : return false;
858 : }
859 :
860 : /// \brief Application of function symbol \@and_.
861 : /// \param s A sort expression.
862 : /// \param arg0 A data expression.
863 : /// \param arg1 A data expression.
864 : /// \return Application of \@and_ to a number of arguments.
865 : inline
866 1981 : application and_function(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
867 : {
868 3962 : return sort_set::and_function(s)(arg0, arg1);
869 : }
870 :
871 : /// \brief Make an application of function symbol \@and_.
872 : /// \param result The data expression where the \@and_ expression is put.
873 : /// \param s A sort expression.
874 : /// \param arg0 A data expression.
875 : /// \param arg1 A data expression.
876 : inline
877 : void make_and_function(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
878 : {
879 : make_application(result, sort_set::and_function(s),arg0, arg1);
880 : }
881 :
882 : /// \brief Recogniser for application of \@and_.
883 : /// \param e A data expression.
884 : /// \return true iff e is an application of function symbol and_function to a
885 : /// number of arguments.
886 : inline
887 0 : bool is_and_function_application(const atermpp::aterm_appl& e)
888 : {
889 0 : return is_application(e) && is_and_function_function_symbol(atermpp::down_cast<application>(e).head());
890 : }
891 :
892 : /// \brief Generate identifier \@or_.
893 : /// \return Identifier \@or_.
894 : inline
895 2264 : const core::identifier_string& or_function_name()
896 : {
897 2264 : static core::identifier_string or_function_name = core::identifier_string("@or_");
898 2264 : return or_function_name;
899 : }
900 :
901 : /// \brief Constructor for function symbol \@or_.
902 : /// \param s A sort expression.
903 : /// \return Function symbol or_function.
904 : inline
905 2264 : function_symbol or_function(const sort_expression& s)
906 : {
907 4528 : function_symbol or_function(or_function_name(), make_function_sort_(make_function_sort_(s, sort_bool::bool_()), make_function_sort_(s, sort_bool::bool_()), make_function_sort_(s, sort_bool::bool_())));
908 2264 : return or_function;
909 : }
910 :
911 : /// \brief Recogniser for function \@or_.
912 : /// \param e A data expression.
913 : /// \return true iff e is the function symbol matching \@or_.
914 : inline
915 0 : bool is_or_function_function_symbol(const atermpp::aterm_appl& e)
916 : {
917 0 : if (is_function_symbol(e))
918 : {
919 0 : return atermpp::down_cast<function_symbol>(e).name() == or_function_name();
920 : }
921 0 : return false;
922 : }
923 :
924 : /// \brief Application of function symbol \@or_.
925 : /// \param s A sort expression.
926 : /// \param arg0 A data expression.
927 : /// \param arg1 A data expression.
928 : /// \return Application of \@or_ to a number of arguments.
929 : inline
930 1981 : application or_function(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
931 : {
932 3962 : return sort_set::or_function(s)(arg0, arg1);
933 : }
934 :
935 : /// \brief Make an application of function symbol \@or_.
936 : /// \param result The data expression where the \@or_ expression is put.
937 : /// \param s A sort expression.
938 : /// \param arg0 A data expression.
939 : /// \param arg1 A data expression.
940 : inline
941 : void make_or_function(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
942 : {
943 : make_application(result, sort_set::or_function(s),arg0, arg1);
944 : }
945 :
946 : /// \brief Recogniser for application of \@or_.
947 : /// \param e A data expression.
948 : /// \return true iff e is an application of function symbol or_function to a
949 : /// number of arguments.
950 : inline
951 0 : bool is_or_function_application(const atermpp::aterm_appl& e)
952 : {
953 0 : return is_application(e) && is_or_function_function_symbol(atermpp::down_cast<application>(e).head());
954 : }
955 :
956 : /// \brief Generate identifier \@fset_union.
957 : /// \return Identifier \@fset_union.
958 : inline
959 10556 : const core::identifier_string& fset_union_name()
960 : {
961 10556 : static core::identifier_string fset_union_name = core::identifier_string("@fset_union");
962 10556 : return fset_union_name;
963 : }
964 :
965 : /// \brief Constructor for function symbol \@fset_union.
966 : /// \param s A sort expression.
967 : /// \return Function symbol fset_union.
968 : inline
969 3682 : function_symbol fset_union(const sort_expression& s)
970 : {
971 7364 : function_symbol fset_union(fset_union_name(), make_function_sort_(make_function_sort_(s, sort_bool::bool_()), make_function_sort_(s, sort_bool::bool_()), sort_fset::fset(s), sort_fset::fset(s), sort_fset::fset(s)));
972 3682 : return fset_union;
973 : }
974 :
975 : /// \brief Recogniser for function \@fset_union.
976 : /// \param e A data expression.
977 : /// \return true iff e is the function symbol matching \@fset_union.
978 : inline
979 7716 : bool is_fset_union_function_symbol(const atermpp::aterm_appl& e)
980 : {
981 7716 : if (is_function_symbol(e))
982 : {
983 6874 : return atermpp::down_cast<function_symbol>(e).name() == fset_union_name();
984 : }
985 842 : return false;
986 : }
987 :
988 : /// \brief Application of function symbol \@fset_union.
989 : /// \param s A sort expression.
990 : /// \param arg0 A data expression.
991 : /// \param arg1 A data expression.
992 : /// \param arg2 A data expression.
993 : /// \param arg3 A data expression.
994 : /// \return Application of \@fset_union to a number of arguments.
995 : inline
996 3399 : application fset_union(const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
997 : {
998 6798 : return sort_set::fset_union(s)(arg0, arg1, arg2, arg3);
999 : }
1000 :
1001 : /// \brief Make an application of function symbol \@fset_union.
1002 : /// \param result The data expression where the \@fset_union expression is put.
1003 : /// \param s A sort expression.
1004 : /// \param arg0 A data expression.
1005 : /// \param arg1 A data expression.
1006 : /// \param arg2 A data expression.
1007 : /// \param arg3 A data expression.
1008 : inline
1009 : void make_fset_union(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
1010 : {
1011 : make_application(result, sort_set::fset_union(s),arg0, arg1, arg2, arg3);
1012 : }
1013 :
1014 : /// \brief Recogniser for application of \@fset_union.
1015 : /// \param e A data expression.
1016 : /// \return true iff e is an application of function symbol fset_union to a
1017 : /// number of arguments.
1018 : inline
1019 7716 : bool is_fset_union_application(const atermpp::aterm_appl& e)
1020 : {
1021 7716 : return is_application(e) && is_fset_union_function_symbol(atermpp::down_cast<application>(e).head());
1022 : }
1023 :
1024 : /// \brief Generate identifier \@fset_inter.
1025 : /// \return Identifier \@fset_inter.
1026 : inline
1027 10441 : const core::identifier_string& fset_intersection_name()
1028 : {
1029 10441 : static core::identifier_string fset_intersection_name = core::identifier_string("@fset_inter");
1030 10441 : return fset_intersection_name;
1031 : }
1032 :
1033 : /// \brief Constructor for function symbol \@fset_inter.
1034 : /// \param s A sort expression.
1035 : /// \return Function symbol fset_intersection.
1036 : inline
1037 3682 : function_symbol fset_intersection(const sort_expression& s)
1038 : {
1039 7364 : function_symbol fset_intersection(fset_intersection_name(), make_function_sort_(make_function_sort_(s, sort_bool::bool_()), make_function_sort_(s, sort_bool::bool_()), sort_fset::fset(s), sort_fset::fset(s), sort_fset::fset(s)));
1040 3682 : return fset_intersection;
1041 : }
1042 :
1043 : /// \brief Recogniser for function \@fset_inter.
1044 : /// \param e A data expression.
1045 : /// \return true iff e is the function symbol matching \@fset_inter.
1046 : inline
1047 7601 : bool is_fset_intersection_function_symbol(const atermpp::aterm_appl& e)
1048 : {
1049 7601 : if (is_function_symbol(e))
1050 : {
1051 6759 : return atermpp::down_cast<function_symbol>(e).name() == fset_intersection_name();
1052 : }
1053 842 : return false;
1054 : }
1055 :
1056 : /// \brief Application of function symbol \@fset_inter.
1057 : /// \param s A sort expression.
1058 : /// \param arg0 A data expression.
1059 : /// \param arg1 A data expression.
1060 : /// \param arg2 A data expression.
1061 : /// \param arg3 A data expression.
1062 : /// \return Application of \@fset_inter to a number of arguments.
1063 : inline
1064 3399 : application fset_intersection(const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
1065 : {
1066 6798 : return sort_set::fset_intersection(s)(arg0, arg1, arg2, arg3);
1067 : }
1068 :
1069 : /// \brief Make an application of function symbol \@fset_inter.
1070 : /// \param result The data expression where the \@fset_inter expression is put.
1071 : /// \param s A sort expression.
1072 : /// \param arg0 A data expression.
1073 : /// \param arg1 A data expression.
1074 : /// \param arg2 A data expression.
1075 : /// \param arg3 A data expression.
1076 : inline
1077 : void make_fset_intersection(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
1078 : {
1079 : make_application(result, sort_set::fset_intersection(s),arg0, arg1, arg2, arg3);
1080 : }
1081 :
1082 : /// \brief Recogniser for application of \@fset_inter.
1083 : /// \param e A data expression.
1084 : /// \return true iff e is an application of function symbol fset_intersection to a
1085 : /// number of arguments.
1086 : inline
1087 7601 : bool is_fset_intersection_application(const atermpp::aterm_appl& e)
1088 : {
1089 7601 : return is_application(e) && is_fset_intersection_function_symbol(atermpp::down_cast<application>(e).head());
1090 : }
1091 : /// \brief Give all system defined mappings for set_
1092 : /// \param s A sort expression
1093 : /// \return All system defined mappings for set_
1094 : inline
1095 283 : function_symbol_vector set_generate_functions_code(const sort_expression& s)
1096 : {
1097 283 : function_symbol_vector result;
1098 283 : result.push_back(sort_set::set_fset(s));
1099 283 : result.push_back(sort_set::set_comprehension(s));
1100 283 : result.push_back(sort_set::in(s, s, set_(s)));
1101 283 : result.push_back(sort_set::complement(s));
1102 283 : result.push_back(sort_set::union_(s, set_(s), set_(s)));
1103 283 : result.push_back(sort_set::intersection(s, set_(s), set_(s)));
1104 283 : result.push_back(sort_set::difference(s, set_(s), set_(s)));
1105 283 : result.push_back(sort_set::false_function(s));
1106 283 : result.push_back(sort_set::true_function(s));
1107 283 : result.push_back(sort_set::not_function(s));
1108 283 : result.push_back(sort_set::and_function(s));
1109 283 : result.push_back(sort_set::or_function(s));
1110 283 : result.push_back(sort_set::fset_union(s));
1111 283 : result.push_back(sort_set::fset_intersection(s));
1112 283 : return result;
1113 0 : }
1114 :
1115 : /// \brief Give all system defined mappings and constructors for set_
1116 : /// \param s A sort expression
1117 : /// \return All system defined mappings for set_
1118 : inline
1119 : function_symbol_vector set_generate_constructors_and_functions_code(const sort_expression& s)
1120 : {
1121 : function_symbol_vector result=set_generate_functions_code(s);
1122 : for(const function_symbol& f: set_generate_constructors_code(s))
1123 : {
1124 : result.push_back(f);
1125 : }
1126 : return result;
1127 : }
1128 :
1129 : /// \brief Give all system defined mappings that can be used in mCRL2 specs for set_
1130 : /// \param s A sort expression
1131 : /// \return All system defined mappings for that can be used in mCRL2 specificationis set_
1132 : inline
1133 : function_symbol_vector set_mCRL2_usable_mappings(const sort_expression& s)
1134 : {
1135 : function_symbol_vector result;
1136 : result.push_back(sort_set::set_fset(s));
1137 : result.push_back(sort_set::set_comprehension(s));
1138 : result.push_back(sort_set::in(s, s, set_(s)));
1139 : result.push_back(sort_set::complement(s));
1140 : result.push_back(sort_set::union_(s, set_(s), set_(s)));
1141 : result.push_back(sort_set::intersection(s, set_(s), set_(s)));
1142 : result.push_back(sort_set::difference(s, set_(s), set_(s)));
1143 : result.push_back(sort_set::false_function(s));
1144 : result.push_back(sort_set::true_function(s));
1145 : result.push_back(sort_set::not_function(s));
1146 : result.push_back(sort_set::and_function(s));
1147 : result.push_back(sort_set::or_function(s));
1148 : result.push_back(sort_set::fset_union(s));
1149 : result.push_back(sort_set::fset_intersection(s));
1150 : return result;
1151 : }
1152 :
1153 :
1154 : // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
1155 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
1156 : /// \brief Give all system defined mappings that are to be implemented in C++ code for set_
1157 : /// \param s A sort expression
1158 : /// \return A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for set_
1159 : inline
1160 283 : implementation_map set_cpp_implementable_mappings(const sort_expression& s)
1161 : {
1162 283 : implementation_map result;
1163 : static_cast< void >(s); // suppress unused variable warnings
1164 283 : return result;
1165 : }
1166 : ///\brief Function for projecting out argument.
1167 : /// left from an application.
1168 : /// \param e A data expression.
1169 : /// \pre left is defined for e.
1170 : /// \return The argument of e that corresponds to left.
1171 : inline
1172 359 : const data_expression& left(const data_expression& e)
1173 : {
1174 359 : assert(is_constructor_application(e) || is_in_application(e) || is_union_application(e) || is_intersection_application(e) || is_difference_application(e) || is_and_function_application(e) || is_or_function_application(e));
1175 359 : return atermpp::down_cast<application>(e)[0];
1176 : }
1177 :
1178 : ///\brief Function for projecting out argument.
1179 : /// right from an application.
1180 : /// \param e A data expression.
1181 : /// \pre right is defined for e.
1182 : /// \return The argument of e that corresponds to right.
1183 : inline
1184 142 : const data_expression& right(const data_expression& e)
1185 : {
1186 142 : assert(is_constructor_application(e) || is_in_application(e) || is_union_application(e) || is_intersection_application(e) || is_difference_application(e) || is_and_function_application(e) || is_or_function_application(e));
1187 142 : return atermpp::down_cast<application>(e)[1];
1188 : }
1189 :
1190 : ///\brief Function for projecting out argument.
1191 : /// arg from an application.
1192 : /// \param e A data expression.
1193 : /// \pre arg is defined for e.
1194 : /// \return The argument of e that corresponds to arg.
1195 : inline
1196 76 : const data_expression& arg(const data_expression& e)
1197 : {
1198 76 : assert(is_set_fset_application(e) || is_set_comprehension_application(e) || is_complement_application(e) || is_false_function_application(e) || is_true_function_application(e) || is_not_function_application(e));
1199 76 : return atermpp::down_cast<application>(e)[0];
1200 : }
1201 :
1202 : ///\brief Function for projecting out argument.
1203 : /// arg1 from an application.
1204 : /// \param e A data expression.
1205 : /// \pre arg1 is defined for e.
1206 : /// \return The argument of e that corresponds to arg1.
1207 : inline
1208 110 : const data_expression& arg1(const data_expression& e)
1209 : {
1210 110 : assert(is_fset_union_application(e) || is_fset_intersection_application(e));
1211 110 : return atermpp::down_cast<application>(e)[0];
1212 : }
1213 :
1214 : ///\brief Function for projecting out argument.
1215 : /// arg2 from an application.
1216 : /// \param e A data expression.
1217 : /// \pre arg2 is defined for e.
1218 : /// \return The argument of e that corresponds to arg2.
1219 : inline
1220 30 : const data_expression& arg2(const data_expression& e)
1221 : {
1222 30 : assert(is_fset_union_application(e) || is_fset_intersection_application(e));
1223 30 : return atermpp::down_cast<application>(e)[1];
1224 : }
1225 :
1226 : ///\brief Function for projecting out argument.
1227 : /// arg3 from an application.
1228 : /// \param e A data expression.
1229 : /// \pre arg3 is defined for e.
1230 : /// \return The argument of e that corresponds to arg3.
1231 : inline
1232 30 : const data_expression& arg3(const data_expression& e)
1233 : {
1234 30 : assert(is_fset_union_application(e) || is_fset_intersection_application(e));
1235 30 : return atermpp::down_cast<application>(e)[2];
1236 : }
1237 :
1238 : ///\brief Function for projecting out argument.
1239 : /// arg4 from an application.
1240 : /// \param e A data expression.
1241 : /// \pre arg4 is defined for e.
1242 : /// \return The argument of e that corresponds to arg4.
1243 : inline
1244 30 : const data_expression& arg4(const data_expression& e)
1245 : {
1246 30 : assert(is_fset_union_application(e) || is_fset_intersection_application(e));
1247 30 : return atermpp::down_cast<application>(e)[3];
1248 : }
1249 :
1250 : /// \brief Give all system defined equations for set_
1251 : /// \param s A sort expression
1252 : /// \return All system defined equations for sort set_
1253 : inline
1254 283 : data_equation_vector set_generate_equations_code(const sort_expression& s)
1255 : {
1256 566 : variable vd("d",s);
1257 566 : variable ve("e",s);
1258 566 : variable vs("s",sort_fset::fset(s));
1259 566 : variable vt("t",sort_fset::fset(s));
1260 566 : variable vf("f",make_function_sort_(s, sort_bool::bool_()));
1261 566 : variable vg("g",make_function_sort_(s, sort_bool::bool_()));
1262 566 : variable vx("x",set_(s));
1263 566 : variable vy("y",set_(s));
1264 566 : variable vc("c",s);
1265 :
1266 283 : data_equation_vector result;
1267 566 : result.push_back(data_equation(variable_list({vs}), set_fset(s, vs), constructor(s, false_function(s), vs)));
1268 566 : result.push_back(data_equation(variable_list({vf}), sort_set::set_comprehension(s, vf), constructor(s, vf, sort_fset::empty(s))));
1269 1132 : result.push_back(data_equation(variable_list({ve, vf, vs}), in(s, ve, constructor(s, vf, vs)), not_equal_to(vf(ve), in(s, ve, vs))));
1270 1698 : result.push_back(data_equation(variable_list({vf, vg, vs, vt}), equal_to(constructor(s, vf, vs), constructor(s, vg, vt)), forall(variable_list({vc}), equal_to(equal_to(vf(vc), vg(vc)), equal_to(in(s, vc, vs), in(s, vc, vt))))));
1271 849 : result.push_back(data_equation(variable_list({vx, vy}), less(vx, vy), sort_bool::and_(less_equal(vx, vy), not_equal_to(vx, vy))));
1272 849 : result.push_back(data_equation(variable_list({vx, vy}), less_equal(vx, vy), equal_to(intersection(s, vx, vy), vx)));
1273 849 : result.push_back(data_equation(variable_list({vf, vs}), complement(s, constructor(s, vf, vs)), constructor(s, not_function(s, vf), vs)));
1274 566 : result.push_back(data_equation(variable_list({vx}), union_(s, vx, vx), vx));
1275 849 : result.push_back(data_equation(variable_list({vx, vy}), union_(s, vx, union_(s, vx, vy)), union_(s, vx, vy)));
1276 849 : result.push_back(data_equation(variable_list({vx, vy}), union_(s, vx, union_(s, vy, vx)), union_(s, vy, vx)));
1277 849 : result.push_back(data_equation(variable_list({vx, vy}), union_(s, union_(s, vx, vy), vx), union_(s, vx, vy)));
1278 849 : result.push_back(data_equation(variable_list({vx, vy}), union_(s, union_(s, vy, vx), vx), union_(s, vy, vx)));
1279 1415 : result.push_back(data_equation(variable_list({vf, vg, vs, vt}), union_(s, constructor(s, vf, vs), constructor(s, vg, vt)), constructor(s, or_function(s, vf, vg), fset_union(s, vf, vg, vs, vt))));
1280 566 : result.push_back(data_equation(variable_list({vx}), intersection(s, vx, vx), vx));
1281 849 : result.push_back(data_equation(variable_list({vx, vy}), intersection(s, vx, intersection(s, vx, vy)), intersection(s, vx, vy)));
1282 849 : result.push_back(data_equation(variable_list({vx, vy}), intersection(s, vx, intersection(s, vy, vx)), intersection(s, vy, vx)));
1283 849 : result.push_back(data_equation(variable_list({vx, vy}), intersection(s, intersection(s, vx, vy), vx), intersection(s, vx, vy)));
1284 849 : result.push_back(data_equation(variable_list({vx, vy}), intersection(s, intersection(s, vy, vx), vx), intersection(s, vy, vx)));
1285 1415 : result.push_back(data_equation(variable_list({vf, vg, vs, vt}), intersection(s, constructor(s, vf, vs), constructor(s, vg, vt)), constructor(s, and_function(s, vf, vg), fset_intersection(s, vf, vg, vs, vt))));
1286 849 : result.push_back(data_equation(variable_list({vx, vy}), difference(s, vx, vy), intersection(s, vx, complement(s, vy))));
1287 566 : result.push_back(data_equation(variable_list({ve}), false_function(s, ve), sort_bool::false_()));
1288 566 : result.push_back(data_equation(variable_list({ve}), true_function(s, ve), sort_bool::true_()));
1289 283 : result.push_back(data_equation(variable_list(), equal_to(false_function(s), true_function(s)), sort_bool::false_()));
1290 283 : result.push_back(data_equation(variable_list(), equal_to(true_function(s), false_function(s)), sort_bool::false_()));
1291 849 : result.push_back(data_equation(variable_list({ve, vf}), not_function(s, vf)(ve), sort_bool::not_(vf(ve))));
1292 283 : result.push_back(data_equation(variable_list(), not_function(s, false_function(s)), true_function(s)));
1293 283 : result.push_back(data_equation(variable_list(), not_function(s, true_function(s)), false_function(s)));
1294 1132 : result.push_back(data_equation(variable_list({ve, vf, vg}), and_function(s, vf, vg)(ve), sort_bool::and_(vf(ve), vg(ve))));
1295 566 : result.push_back(data_equation(variable_list({vf}), and_function(s, vf, vf), vf));
1296 566 : result.push_back(data_equation(variable_list({vf}), and_function(s, vf, false_function(s)), false_function(s)));
1297 566 : result.push_back(data_equation(variable_list({vf}), and_function(s, false_function(s), vf), false_function(s)));
1298 566 : result.push_back(data_equation(variable_list({vf}), and_function(s, vf, true_function(s)), vf));
1299 566 : result.push_back(data_equation(variable_list({vf}), and_function(s, true_function(s), vf), vf));
1300 566 : result.push_back(data_equation(variable_list({vf}), or_function(s, vf, vf), vf));
1301 566 : result.push_back(data_equation(variable_list({vf}), or_function(s, vf, false_function(s)), vf));
1302 566 : result.push_back(data_equation(variable_list({vf}), or_function(s, false_function(s), vf), vf));
1303 566 : result.push_back(data_equation(variable_list({vf}), or_function(s, vf, true_function(s)), true_function(s)));
1304 566 : result.push_back(data_equation(variable_list({vf}), or_function(s, true_function(s), vf), true_function(s)));
1305 1132 : result.push_back(data_equation(variable_list({ve, vf, vg}), or_function(s, vf, vg)(ve), sort_bool::or_(vf(ve), vg(ve))));
1306 849 : result.push_back(data_equation(variable_list({vf, vg}), fset_union(s, vf, vg, sort_fset::empty(s), sort_fset::empty(s)), sort_fset::empty(s)));
1307 1415 : result.push_back(data_equation(variable_list({vd, vf, vg, vs}), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::empty(s)), sort_fset::cinsert(s, vd, sort_bool::not_(vg(vd)), fset_union(s, vf, vg, vs, sort_fset::empty(s)))));
1308 1415 : result.push_back(data_equation(variable_list({ve, vf, vg, vt}), fset_union(s, vf, vg, sort_fset::empty(s), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, ve, sort_bool::not_(vf(ve)), fset_union(s, vf, vg, sort_fset::empty(s), vt))));
1309 1698 : result.push_back(data_equation(variable_list({vd, vf, vg, vs, vt}), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, vd, vt)), sort_fset::cinsert(s, vd, equal_to(vf(vd), vg(vd)), fset_union(s, vf, vg, vs, vt))));
1310 1981 : result.push_back(data_equation(variable_list({vd, ve, vf, vg, vs, vt}), less(vd, ve), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, vd, sort_bool::not_(vg(vd)), fset_union(s, vf, vg, vs, sort_fset::cons_(s, ve, vt)))));
1311 1981 : result.push_back(data_equation(variable_list({vd, ve, vf, vg, vs, vt}), less(ve, vd), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, ve, sort_bool::not_(vf(ve)), fset_union(s, vf, vg, sort_fset::cons_(s, vd, vs), vt))));
1312 849 : result.push_back(data_equation(variable_list({vf, vg}), fset_intersection(s, vf, vg, sort_fset::empty(s), sort_fset::empty(s)), sort_fset::empty(s)));
1313 1415 : result.push_back(data_equation(variable_list({vd, vf, vg, vs}), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::empty(s)), sort_fset::cinsert(s, vd, vg(vd), fset_intersection(s, vf, vg, vs, sort_fset::empty(s)))));
1314 1415 : result.push_back(data_equation(variable_list({ve, vf, vg, vt}), fset_intersection(s, vf, vg, sort_fset::empty(s), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, ve, vf(ve), fset_intersection(s, vf, vg, sort_fset::empty(s), vt))));
1315 1698 : result.push_back(data_equation(variable_list({vd, vf, vg, vs, vt}), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, vd, vt)), sort_fset::cinsert(s, vd, equal_to(vf(vd), vg(vd)), fset_intersection(s, vf, vg, vs, vt))));
1316 1981 : result.push_back(data_equation(variable_list({vd, ve, vf, vg, vs, vt}), less(vd, ve), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, vd, vg(vd), fset_intersection(s, vf, vg, vs, sort_fset::cons_(s, ve, vt)))));
1317 1981 : result.push_back(data_equation(variable_list({vd, ve, vf, vg, vs, vt}), less(ve, vd), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), sort_fset::cons_(s, ve, vt)), sort_fset::cinsert(s, ve, vf(ve), fset_intersection(s, vf, vg, sort_fset::cons_(s, vd, vs), vt))));
1318 566 : return result;
1319 283 : }
1320 :
1321 : } // namespace sort_set_
1322 :
1323 : } // namespace data
1324 :
1325 : } // namespace mcrl2
1326 :
1327 : #endif // MCRL2_DATA_SET_H
|
