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/fset.h
10 : /// \brief The standard sort fset.
11 : ///
12 : /// This file was generated from the data sort specification
13 : /// mcrl2/data/build/fset.spec.
14 :
15 : #ifndef MCRL2_DATA_FSET_H
16 : #define MCRL2_DATA_FSET_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/container_sort.h"
27 : #include "mcrl2/data/bool.h"
28 : #include "mcrl2/data/nat.h"
29 :
30 : namespace mcrl2 {
31 :
32 : namespace data {
33 :
34 : /// \brief Namespace for system defined sort fset.
35 : namespace sort_fset {
36 :
37 : /// \brief Constructor for sort expression FSet(S)
38 : /// \param s A sort expression
39 : /// \return Sort expression fset(s)
40 : inline
41 314350 : container_sort fset(const sort_expression& s)
42 : {
43 314350 : container_sort fset(fset_container(), s);
44 314350 : return fset;
45 : }
46 :
47 : /// \brief Recogniser for sort expression FSet(s)
48 : /// \param e A sort expression
49 : /// \return true iff e is a container sort of which the name matches
50 : /// fset
51 : inline
52 39409 : bool is_fset(const sort_expression& e)
53 : {
54 39409 : if (is_container_sort(e))
55 : {
56 3144 : return container_sort(e).container_name() == fset_container();
57 : }
58 36265 : return false;
59 : }
60 :
61 :
62 : /// \brief Generate identifier {}.
63 : /// \return Identifier {}.
64 : inline
65 63099 : const core::identifier_string& empty_name()
66 : {
67 63099 : static core::identifier_string empty_name = core::identifier_string("{}");
68 63099 : return empty_name;
69 : }
70 :
71 : /// \brief Constructor for function symbol {}.
72 : /// \param s A sort expression.
73 : /// \return Function symbol empty.
74 : inline
75 16211 : function_symbol empty(const sort_expression& s)
76 : {
77 16211 : function_symbol empty(empty_name(), fset(s));
78 16211 : return empty;
79 : }
80 :
81 : /// \brief Recogniser for function {}.
82 : /// \param e A data expression.
83 : /// \return true iff e is the function symbol matching {}.
84 : inline
85 54408 : bool is_empty_function_symbol(const atermpp::aterm_appl& e)
86 : {
87 54408 : if (is_function_symbol(e))
88 : {
89 46888 : return atermpp::down_cast<function_symbol>(e).name() == empty_name();
90 : }
91 7520 : return false;
92 : }
93 :
94 : /// \brief Generate identifier \@fset_insert.
95 : /// \return Identifier \@fset_insert.
96 : inline
97 67455 : const core::identifier_string& insert_name()
98 : {
99 67455 : static core::identifier_string insert_name = core::identifier_string("@fset_insert");
100 67455 : return insert_name;
101 : }
102 :
103 : /// \brief Constructor for function symbol \@fset_insert.
104 : /// \param s A sort expression.
105 : /// \return Function symbol insert.
106 : inline
107 8097 : function_symbol insert(const sort_expression& s)
108 : {
109 16194 : function_symbol insert(insert_name(), make_function_sort_(s, fset(s), fset(s)));
110 8097 : return insert;
111 : }
112 :
113 : /// \brief Recogniser for function \@fset_insert.
114 : /// \param e A data expression.
115 : /// \return true iff e is the function symbol matching \@fset_insert.
116 : inline
117 8497 : bool is_insert_function_symbol(const atermpp::aterm_appl& e)
118 : {
119 8497 : if (is_function_symbol(e))
120 : {
121 7655 : return atermpp::down_cast<function_symbol>(e).name() == insert_name();
122 : }
123 842 : return false;
124 : }
125 :
126 : /// \brief Application of function symbol \@fset_insert.
127 : /// \param s A sort expression.
128 : /// \param arg0 A data expression.
129 : /// \param arg1 A data expression.
130 : /// \return Application of \@fset_insert to a number of arguments.
131 : inline
132 3116 : application insert(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
133 : {
134 6232 : return sort_fset::insert(s)(arg0, arg1);
135 : }
136 :
137 : /// \brief Make an application of function symbol \@fset_insert.
138 : /// \param result The data expression where the \@fset_insert expression is put.
139 : /// \param s A sort expression.
140 : /// \param arg0 A data expression.
141 : /// \param arg1 A data expression.
142 : inline
143 : void make_insert(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
144 : {
145 : make_application(result, sort_fset::insert(s),arg0, arg1);
146 : }
147 :
148 : /// \brief Recogniser for application of \@fset_insert.
149 : /// \param e A data expression.
150 : /// \return true iff e is an application of function symbol insert to a
151 : /// number of arguments.
152 : inline
153 8873 : bool is_insert_application(const atermpp::aterm_appl& e)
154 : {
155 8873 : return is_application(e) && is_insert_function_symbol(atermpp::down_cast<application>(e).head());
156 : }
157 : /// \brief Give all system defined constructors for fset.
158 : /// \param s A sort expression.
159 : /// \return All system defined constructors for fset.
160 : inline
161 332 : function_symbol_vector fset_generate_constructors_code(const sort_expression& s)
162 : {
163 332 : function_symbol_vector result;
164 332 : result.push_back(sort_fset::empty(s));
165 332 : result.push_back(sort_fset::insert(s));
166 :
167 332 : return result;
168 0 : }
169 : /// \brief Give all defined constructors which can be used in mCRL2 specs for fset.
170 : /// \param s A sort expression.
171 : /// \return All system defined constructors that can be used in an mCRL2 specification for fset.
172 : inline
173 4578 : function_symbol_vector fset_mCRL2_usable_constructors(const sort_expression& s)
174 : {
175 4578 : function_symbol_vector result;
176 4578 : result.push_back(sort_fset::empty(s));
177 4578 : result.push_back(sort_fset::insert(s));
178 :
179 4578 : return result;
180 0 : }
181 : // 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
182 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
183 : /// \brief Give all system defined constructors which have an implementation in C++ and not in rewrite rules for fset.
184 : /// \param s A sort expression.
185 : /// \return All system defined constructors that are to be implemented in C++ for fset.
186 : inline
187 332 : implementation_map fset_cpp_implementable_constructors(const sort_expression& s)
188 : {
189 332 : implementation_map result;
190 : static_cast< void >(s); // suppress unused variable warnings
191 332 : return result;
192 : }
193 :
194 : /// \brief Generate identifier \@fset_cons.
195 : /// \return Identifier \@fset_cons.
196 : inline
197 35804 : const core::identifier_string& cons_name()
198 : {
199 35804 : static core::identifier_string cons_name = core::identifier_string("@fset_cons");
200 35804 : return cons_name;
201 : }
202 :
203 : /// \brief Constructor for function symbol \@fset_cons.
204 : /// \param s A sort expression.
205 : /// \return Function symbol cons_.
206 : inline
207 28251 : function_symbol cons_(const sort_expression& s)
208 : {
209 56502 : function_symbol cons_(cons_name(), make_function_sort_(s, fset(s), fset(s)));
210 28251 : return cons_;
211 : }
212 :
213 : /// \brief Recogniser for function \@fset_cons.
214 : /// \param e A data expression.
215 : /// \return true iff e is the function symbol matching \@fset_cons.
216 : inline
217 8395 : bool is_cons_function_symbol(const atermpp::aterm_appl& e)
218 : {
219 8395 : if (is_function_symbol(e))
220 : {
221 7553 : return atermpp::down_cast<function_symbol>(e).name() == cons_name();
222 : }
223 842 : return false;
224 : }
225 :
226 : /// \brief Application of function symbol \@fset_cons.
227 : /// \param s A sort expression.
228 : /// \param arg0 A data expression.
229 : /// \param arg1 A data expression.
230 : /// \return Application of \@fset_cons to a number of arguments.
231 : inline
232 23341 : application cons_(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
233 : {
234 46682 : return sort_fset::cons_(s)(arg0, arg1);
235 : }
236 :
237 : /// \brief Make an application of function symbol \@fset_cons.
238 : /// \param result The data expression where the \@fset_cons expression is put.
239 : /// \param s A sort expression.
240 : /// \param arg0 A data expression.
241 : /// \param arg1 A data expression.
242 : inline
243 : void make_cons_(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
244 : {
245 : make_application(result, sort_fset::cons_(s),arg0, arg1);
246 : }
247 :
248 : /// \brief Recogniser for application of \@fset_cons.
249 : /// \param e A data expression.
250 : /// \return true iff e is an application of function symbol cons_ to a
251 : /// number of arguments.
252 : inline
253 8771 : bool is_cons_application(const atermpp::aterm_appl& e)
254 : {
255 8771 : return is_application(e) && is_cons_function_symbol(atermpp::down_cast<application>(e).head());
256 : }
257 :
258 : /// \brief Generate identifier \@fset_cinsert.
259 : /// \return Identifier \@fset_cinsert.
260 : inline
261 8472 : const core::identifier_string& cinsert_name()
262 : {
263 8472 : static core::identifier_string cinsert_name = core::identifier_string("@fset_cinsert");
264 8472 : return cinsert_name;
265 : }
266 :
267 : /// \brief Constructor for function symbol \@fset_cinsert.
268 : /// \param s A sort expression.
269 : /// \return Function symbol cinsert.
270 : inline
271 8472 : function_symbol cinsert(const sort_expression& s)
272 : {
273 16944 : function_symbol cinsert(cinsert_name(), make_function_sort_(s, sort_bool::bool_(), fset(s), fset(s)));
274 8472 : return cinsert;
275 : }
276 :
277 : /// \brief Recogniser for function \@fset_cinsert.
278 : /// \param e A data expression.
279 : /// \return true iff e is the function symbol matching \@fset_cinsert.
280 : inline
281 : bool is_cinsert_function_symbol(const atermpp::aterm_appl& e)
282 : {
283 : if (is_function_symbol(e))
284 : {
285 : return atermpp::down_cast<function_symbol>(e).name() == cinsert_name();
286 : }
287 : return false;
288 : }
289 :
290 : /// \brief Application of function symbol \@fset_cinsert.
291 : /// \param s A sort expression.
292 : /// \param arg0 A data expression.
293 : /// \param arg1 A data expression.
294 : /// \param arg2 A data expression.
295 : /// \return Application of \@fset_cinsert to a number of arguments.
296 : inline
297 3562 : application cinsert(const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
298 : {
299 7124 : return sort_fset::cinsert(s)(arg0, arg1, arg2);
300 : }
301 :
302 : /// \brief Make an application of function symbol \@fset_cinsert.
303 : /// \param result The data expression where the \@fset_cinsert expression is put.
304 : /// \param s A sort expression.
305 : /// \param arg0 A data expression.
306 : /// \param arg1 A data expression.
307 : /// \param arg2 A data expression.
308 : inline
309 : void make_cinsert(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
310 : {
311 : make_application(result, sort_fset::cinsert(s),arg0, arg1, arg2);
312 : }
313 :
314 : /// \brief Recogniser for application of \@fset_cinsert.
315 : /// \param e A data expression.
316 : /// \return true iff e is an application of function symbol cinsert to a
317 : /// number of arguments.
318 : inline
319 : bool is_cinsert_application(const atermpp::aterm_appl& e)
320 : {
321 : return is_application(e) && is_cinsert_function_symbol(atermpp::down_cast<application>(e).head());
322 : }
323 :
324 : /// \brief Generate identifier in.
325 : /// \return Identifier in.
326 : inline
327 13072 : const core::identifier_string& in_name()
328 : {
329 13072 : static core::identifier_string in_name = core::identifier_string("in");
330 13072 : return in_name;
331 : }
332 :
333 : /// \brief Constructor for function symbol in.
334 : /// \param s A sort expression.
335 : /// \return Function symbol in.
336 : inline
337 6579 : function_symbol in(const sort_expression& s)
338 : {
339 13158 : function_symbol in(in_name(), make_function_sort_(s, fset(s), sort_bool::bool_()));
340 6579 : return in;
341 : }
342 :
343 : /// \brief Recogniser for function in.
344 : /// \param e A data expression.
345 : /// \return true iff e is the function symbol matching in.
346 : inline
347 7335 : bool is_in_function_symbol(const atermpp::aterm_appl& e)
348 : {
349 7335 : if (is_function_symbol(e))
350 : {
351 6493 : return atermpp::down_cast<function_symbol>(e).name() == in_name();
352 : }
353 842 : return false;
354 : }
355 :
356 : /// \brief Application of function symbol in.
357 : /// \param s A sort expression.
358 : /// \param arg0 A data expression.
359 : /// \param arg1 A data expression.
360 : /// \return Application of in to a number of arguments.
361 : inline
362 1669 : application in(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
363 : {
364 3338 : return sort_fset::in(s)(arg0, arg1);
365 : }
366 :
367 : /// \brief Make an application of function symbol in.
368 : /// \param result The data expression where the in expression is put.
369 : /// \param s A sort expression.
370 : /// \param arg0 A data expression.
371 : /// \param arg1 A data expression.
372 : inline
373 : void make_in(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
374 : {
375 : make_application(result, sort_fset::in(s),arg0, arg1);
376 : }
377 :
378 : /// \brief Recogniser for application of in.
379 : /// \param e A data expression.
380 : /// \return true iff e is an application of function symbol in to a
381 : /// number of arguments.
382 : inline
383 7335 : bool is_in_application(const atermpp::aterm_appl& e)
384 : {
385 7335 : return is_application(e) && is_in_function_symbol(atermpp::down_cast<application>(e).head());
386 : }
387 :
388 : /// \brief Generate identifier -.
389 : /// \return Identifier -.
390 : inline
391 14507 : const core::identifier_string& difference_name()
392 : {
393 14507 : static core::identifier_string difference_name = core::identifier_string("-");
394 14507 : return difference_name;
395 : }
396 :
397 : /// \brief Constructor for function symbol -.
398 : /// \param s A sort expression.
399 : /// \return Function symbol difference.
400 : inline
401 7567 : function_symbol difference(const sort_expression& s)
402 : {
403 15134 : function_symbol difference(difference_name(), make_function_sort_(fset(s), fset(s), fset(s)));
404 7567 : return difference;
405 : }
406 :
407 : /// \brief Recogniser for function -.
408 : /// \param e A data expression.
409 : /// \return true iff e is the function symbol matching -.
410 : inline
411 7335 : bool is_difference_function_symbol(const atermpp::aterm_appl& e)
412 : {
413 7335 : if (is_function_symbol(e))
414 : {
415 6493 : return atermpp::down_cast<function_symbol>(e).name() == difference_name();
416 : }
417 842 : return false;
418 : }
419 :
420 : /// \brief Application of function symbol -.
421 : /// \param s A sort expression.
422 : /// \param arg0 A data expression.
423 : /// \param arg1 A data expression.
424 : /// \return Application of - to a number of arguments.
425 : inline
426 2657 : application difference(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
427 : {
428 5314 : return sort_fset::difference(s)(arg0, arg1);
429 : }
430 :
431 : /// \brief Make an application of function symbol -.
432 : /// \param result The data expression where the - expression is put.
433 : /// \param s A sort expression.
434 : /// \param arg0 A data expression.
435 : /// \param arg1 A data expression.
436 : inline
437 : void make_difference(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
438 : {
439 : make_application(result, sort_fset::difference(s),arg0, arg1);
440 : }
441 :
442 : /// \brief Recogniser for application of -.
443 : /// \param e A data expression.
444 : /// \return true iff e is an application of function symbol difference to a
445 : /// number of arguments.
446 : inline
447 7335 : bool is_difference_application(const atermpp::aterm_appl& e)
448 : {
449 7335 : return is_application(e) && is_difference_function_symbol(atermpp::down_cast<application>(e).head());
450 : }
451 :
452 : /// \brief Generate identifier +.
453 : /// \return Identifier +.
454 : inline
455 14506 : const core::identifier_string& union_name()
456 : {
457 14506 : static core::identifier_string union_name = core::identifier_string("+");
458 14506 : return union_name;
459 : }
460 :
461 : /// \brief Constructor for function symbol +.
462 : /// \param s A sort expression.
463 : /// \return Function symbol union_.
464 : inline
465 7566 : function_symbol union_(const sort_expression& s)
466 : {
467 15132 : function_symbol union_(union_name(), make_function_sort_(fset(s), fset(s), fset(s)));
468 7566 : return union_;
469 : }
470 :
471 : /// \brief Recogniser for function +.
472 : /// \param e A data expression.
473 : /// \return true iff e is the function symbol matching +.
474 : inline
475 7335 : bool is_union_function_symbol(const atermpp::aterm_appl& e)
476 : {
477 7335 : if (is_function_symbol(e))
478 : {
479 6493 : return atermpp::down_cast<function_symbol>(e).name() == union_name();
480 : }
481 842 : return false;
482 : }
483 :
484 : /// \brief Application of function symbol +.
485 : /// \param s A sort expression.
486 : /// \param arg0 A data expression.
487 : /// \param arg1 A data expression.
488 : /// \return Application of + to a number of arguments.
489 : inline
490 2656 : application union_(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
491 : {
492 5312 : return sort_fset::union_(s)(arg0, arg1);
493 : }
494 :
495 : /// \brief Make an application of function symbol +.
496 : /// \param result The data expression where the + expression is put.
497 : /// \param s A sort expression.
498 : /// \param arg0 A data expression.
499 : /// \param arg1 A data expression.
500 : inline
501 : void make_union_(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
502 : {
503 : make_application(result, sort_fset::union_(s),arg0, arg1);
504 : }
505 :
506 : /// \brief Recogniser for application of +.
507 : /// \param e A data expression.
508 : /// \return true iff e is an application of function symbol union_ to a
509 : /// number of arguments.
510 : inline
511 7335 : bool is_union_application(const atermpp::aterm_appl& e)
512 : {
513 7335 : return is_application(e) && is_union_function_symbol(atermpp::down_cast<application>(e).head());
514 : }
515 :
516 : /// \brief Generate identifier *.
517 : /// \return Identifier *.
518 : inline
519 14059 : const core::identifier_string& intersection_name()
520 : {
521 14059 : static core::identifier_string intersection_name = core::identifier_string("*");
522 14059 : return intersection_name;
523 : }
524 :
525 : /// \brief Constructor for function symbol *.
526 : /// \param s A sort expression.
527 : /// \return Function symbol intersection.
528 : inline
529 7566 : function_symbol intersection(const sort_expression& s)
530 : {
531 15132 : function_symbol intersection(intersection_name(), make_function_sort_(fset(s), fset(s), fset(s)));
532 7566 : return intersection;
533 : }
534 :
535 : /// \brief Recogniser for function *.
536 : /// \param e A data expression.
537 : /// \return true iff e is the function symbol matching *.
538 : inline
539 7335 : bool is_intersection_function_symbol(const atermpp::aterm_appl& e)
540 : {
541 7335 : if (is_function_symbol(e))
542 : {
543 6493 : return atermpp::down_cast<function_symbol>(e).name() == intersection_name();
544 : }
545 842 : return false;
546 : }
547 :
548 : /// \brief Application of function symbol *.
549 : /// \param s A sort expression.
550 : /// \param arg0 A data expression.
551 : /// \param arg1 A data expression.
552 : /// \return Application of * to a number of arguments.
553 : inline
554 2656 : application intersection(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
555 : {
556 5312 : return sort_fset::intersection(s)(arg0, arg1);
557 : }
558 :
559 : /// \brief Make an application of function symbol *.
560 : /// \param result The data expression where the * expression is put.
561 : /// \param s A sort expression.
562 : /// \param arg0 A data expression.
563 : /// \param arg1 A data expression.
564 : inline
565 : void make_intersection(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
566 : {
567 : make_application(result, sort_fset::intersection(s),arg0, arg1);
568 : }
569 :
570 : /// \brief Recogniser for application of *.
571 : /// \param e A data expression.
572 : /// \return true iff e is an application of function symbol intersection to a
573 : /// number of arguments.
574 : inline
575 7335 : bool is_intersection_application(const atermpp::aterm_appl& e)
576 : {
577 7335 : return is_application(e) && is_intersection_function_symbol(atermpp::down_cast<application>(e).head());
578 : }
579 :
580 : /// \brief Generate identifier #.
581 : /// \return Identifier #.
582 : inline
583 12470 : const core::identifier_string& count_name()
584 : {
585 12470 : static core::identifier_string count_name = core::identifier_string("#");
586 12470 : return count_name;
587 : }
588 :
589 : /// \brief Constructor for function symbol #.
590 : /// \param s A sort expression.
591 : /// \return Function symbol count.
592 : inline
593 5977 : function_symbol count(const sort_expression& s)
594 : {
595 11954 : function_symbol count(count_name(), make_function_sort_(fset(s), sort_nat::nat()));
596 5977 : return count;
597 : }
598 :
599 : /// \brief Recogniser for function #.
600 : /// \param e A data expression.
601 : /// \return true iff e is the function symbol matching #.
602 : inline
603 7335 : bool is_count_function_symbol(const atermpp::aterm_appl& e)
604 : {
605 7335 : if (is_function_symbol(e))
606 : {
607 6493 : return atermpp::down_cast<function_symbol>(e).name() == count_name();
608 : }
609 842 : return false;
610 : }
611 :
612 : /// \brief Application of function symbol #.
613 : /// \param s A sort expression.
614 : /// \param arg0 A data expression.
615 : /// \return Application of # to a number of arguments.
616 : inline
617 996 : application count(const sort_expression& s, const data_expression& arg0)
618 : {
619 1992 : return sort_fset::count(s)(arg0);
620 : }
621 :
622 : /// \brief Make an application of function symbol #.
623 : /// \param result The data expression where the # expression is put.
624 : /// \param s A sort expression.
625 : /// \param arg0 A data expression.
626 : inline
627 : void make_count(data_expression& result, const sort_expression& s, const data_expression& arg0)
628 : {
629 : make_application(result, sort_fset::count(s),arg0);
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 count to a
635 : /// number of arguments.
636 : inline
637 7335 : bool is_count_application(const atermpp::aterm_appl& e)
638 : {
639 7335 : return is_application(e) && is_count_function_symbol(atermpp::down_cast<application>(e).head());
640 : }
641 : /// \brief Give all system defined mappings for fset
642 : /// \param s A sort expression
643 : /// \return All system defined mappings for fset
644 : inline
645 332 : function_symbol_vector fset_generate_functions_code(const sort_expression& s)
646 : {
647 332 : function_symbol_vector result;
648 332 : result.push_back(sort_fset::cons_(s));
649 332 : result.push_back(sort_fset::cinsert(s));
650 332 : result.push_back(sort_fset::in(s));
651 332 : result.push_back(sort_fset::difference(s));
652 332 : result.push_back(sort_fset::union_(s));
653 332 : result.push_back(sort_fset::intersection(s));
654 332 : result.push_back(sort_fset::count(s));
655 332 : return result;
656 0 : }
657 :
658 : /// \brief Give all system defined mappings and constructors for fset
659 : /// \param s A sort expression
660 : /// \return All system defined mappings for fset
661 : inline
662 : function_symbol_vector fset_generate_constructors_and_functions_code(const sort_expression& s)
663 : {
664 : function_symbol_vector result=fset_generate_functions_code(s);
665 : for(const function_symbol& f: fset_generate_constructors_code(s))
666 : {
667 : result.push_back(f);
668 : }
669 : return result;
670 : }
671 :
672 : /// \brief Give all system defined mappings that can be used in mCRL2 specs for fset
673 : /// \param s A sort expression
674 : /// \return All system defined mappings for that can be used in mCRL2 specificationis fset
675 : inline
676 4578 : function_symbol_vector fset_mCRL2_usable_mappings(const sort_expression& s)
677 : {
678 4578 : function_symbol_vector result;
679 4578 : result.push_back(sort_fset::cons_(s));
680 4578 : result.push_back(sort_fset::cinsert(s));
681 4578 : result.push_back(sort_fset::in(s));
682 4578 : result.push_back(sort_fset::difference(s));
683 4578 : result.push_back(sort_fset::union_(s));
684 4578 : result.push_back(sort_fset::intersection(s));
685 4578 : result.push_back(sort_fset::count(s));
686 4578 : return result;
687 0 : }
688 :
689 :
690 : // 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
691 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
692 : /// \brief Give all system defined mappings that are to be implemented in C++ code for fset
693 : /// \param s A sort expression
694 : /// \return A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for fset
695 : inline
696 332 : implementation_map fset_cpp_implementable_mappings(const sort_expression& s)
697 : {
698 332 : implementation_map result;
699 : static_cast< void >(s); // suppress unused variable warnings
700 332 : return result;
701 : }
702 : ///\brief Function for projecting out argument.
703 : /// left from an application.
704 : /// \param e A data expression.
705 : /// \pre left is defined for e.
706 : /// \return The argument of e that corresponds to left.
707 : inline
708 283 : const data_expression& left(const data_expression& e)
709 : {
710 283 : assert(is_insert_application(e) || is_cons_application(e) || is_in_application(e) || is_difference_application(e) || is_union_application(e) || is_intersection_application(e));
711 283 : return atermpp::down_cast<application>(e)[0];
712 : }
713 :
714 : ///\brief Function for projecting out argument.
715 : /// right from an application.
716 : /// \param e A data expression.
717 : /// \pre right is defined for e.
718 : /// \return The argument of e that corresponds to right.
719 : inline
720 650 : const data_expression& right(const data_expression& e)
721 : {
722 650 : assert(is_insert_application(e) || is_cons_application(e) || is_in_application(e) || is_difference_application(e) || is_union_application(e) || is_intersection_application(e));
723 650 : return atermpp::down_cast<application>(e)[1];
724 : }
725 :
726 : ///\brief Function for projecting out argument.
727 : /// arg1 from an application.
728 : /// \param e A data expression.
729 : /// \pre arg1 is defined for e.
730 : /// \return The argument of e that corresponds to arg1.
731 : inline
732 : const data_expression& arg1(const data_expression& e)
733 : {
734 : assert(is_cinsert_application(e));
735 : return atermpp::down_cast<application>(e)[0];
736 : }
737 :
738 : ///\brief Function for projecting out argument.
739 : /// arg2 from an application.
740 : /// \param e A data expression.
741 : /// \pre arg2 is defined for e.
742 : /// \return The argument of e that corresponds to arg2.
743 : inline
744 : const data_expression& arg2(const data_expression& e)
745 : {
746 : assert(is_cinsert_application(e));
747 : return atermpp::down_cast<application>(e)[1];
748 : }
749 :
750 : ///\brief Function for projecting out argument.
751 : /// arg3 from an application.
752 : /// \param e A data expression.
753 : /// \pre arg3 is defined for e.
754 : /// \return The argument of e that corresponds to arg3.
755 : inline
756 : const data_expression& arg3(const data_expression& e)
757 : {
758 : assert(is_cinsert_application(e));
759 : return atermpp::down_cast<application>(e)[2];
760 : }
761 :
762 : ///\brief Function for projecting out argument.
763 : /// arg from an application.
764 : /// \param e A data expression.
765 : /// \pre arg is defined for e.
766 : /// \return The argument of e that corresponds to arg.
767 : inline
768 0 : const data_expression& arg(const data_expression& e)
769 : {
770 0 : assert(is_count_application(e));
771 0 : return atermpp::down_cast<application>(e)[0];
772 : }
773 :
774 : /// \brief Give all system defined equations for fset
775 : /// \param s A sort expression
776 : /// \return All system defined equations for sort fset
777 : inline
778 332 : data_equation_vector fset_generate_equations_code(const sort_expression& s)
779 : {
780 664 : variable vd("d",s);
781 664 : variable ve("e",s);
782 664 : variable vs("s",fset(s));
783 664 : variable vt("t",fset(s));
784 :
785 332 : data_equation_vector result;
786 996 : result.push_back(data_equation(variable_list({vd, vs}), equal_to(empty(s), cons_(s, vd, vs)), sort_bool::false_()));
787 996 : result.push_back(data_equation(variable_list({vd, vs}), equal_to(cons_(s, vd, vs), empty(s)), sort_bool::false_()));
788 1660 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), equal_to(cons_(s, vd, vs), cons_(s, ve, vt)), sort_bool::and_(equal_to(vd, ve), equal_to(vs, vt))));
789 996 : result.push_back(data_equation(variable_list({vd, vs}), less_equal(empty(s), cons_(s, vd, vs)), sort_bool::true_()));
790 996 : result.push_back(data_equation(variable_list({vd, vs}), less_equal(cons_(s, vd, vs), empty(s)), sort_bool::false_()));
791 1660 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less_equal(cons_(s, vd, vs), cons_(s, ve, vt)), if_(less(vd, ve), sort_bool::false_(), if_(equal_to(vd, ve), less_equal(vs, vt), less_equal(cons_(s, vd, vs), vt)))));
792 996 : result.push_back(data_equation(variable_list({vd, vs}), less(empty(s), cons_(s, vd, vs)), sort_bool::true_()));
793 996 : result.push_back(data_equation(variable_list({vd, vs}), less(cons_(s, vd, vs), empty(s)), sort_bool::false_()));
794 1660 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less(cons_(s, vd, vs), cons_(s, ve, vt)), if_(less(vd, ve), sort_bool::false_(), if_(equal_to(vd, ve), less(vs, vt), less_equal(cons_(s, vd, vs), vt)))));
795 664 : result.push_back(data_equation(variable_list({vd}), insert(s, vd, empty(s)), cons_(s, vd, empty(s))));
796 996 : result.push_back(data_equation(variable_list({vd, vs}), insert(s, vd, cons_(s, vd, vs)), cons_(s, vd, vs)));
797 1328 : result.push_back(data_equation(variable_list({vd, ve, vs}), less(vd, ve), insert(s, vd, cons_(s, ve, vs)), cons_(s, vd, cons_(s, ve, vs))));
798 1328 : result.push_back(data_equation(variable_list({vd, ve, vs}), less(ve, vd), insert(s, vd, cons_(s, ve, vs)), cons_(s, ve, insert(s, vd, vs))));
799 996 : result.push_back(data_equation(variable_list({vd, vs}), cinsert(s, vd, sort_bool::false_(), vs), vs));
800 996 : result.push_back(data_equation(variable_list({vd, vs}), cinsert(s, vd, sort_bool::true_(), vs), insert(s, vd, vs)));
801 664 : result.push_back(data_equation(variable_list({vd}), in(s, vd, empty(s)), sort_bool::false_()));
802 1328 : result.push_back(data_equation(variable_list({vd, ve, vs}), in(s, vd, cons_(s, ve, vs)), sort_bool::or_(equal_to(vd, ve), in(s, vd, vs))));
803 1328 : result.push_back(data_equation(variable_list({vd, ve, vs}), in(s, vd, insert(s, ve, vs)), sort_bool::or_(equal_to(vd, ve), in(s, vd, vs))));
804 664 : result.push_back(data_equation(variable_list({vs}), difference(s, vs, empty(s)), vs));
805 664 : result.push_back(data_equation(variable_list({vt}), difference(s, empty(s), vt), empty(s)));
806 1328 : result.push_back(data_equation(variable_list({vd, vs, vt}), difference(s, cons_(s, vd, vs), cons_(s, vd, vt)), difference(s, vs, vt)));
807 1660 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less(vd, ve), difference(s, cons_(s, vd, vs), cons_(s, ve, vt)), cons_(s, vd, difference(s, vs, cons_(s, ve, vt)))));
808 1660 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less(ve, vd), difference(s, cons_(s, vd, vs), cons_(s, ve, vt)), difference(s, cons_(s, vd, vs), vt)));
809 664 : result.push_back(data_equation(variable_list({vs}), union_(s, vs, empty(s)), vs));
810 664 : result.push_back(data_equation(variable_list({vt}), union_(s, empty(s), vt), vt));
811 1328 : result.push_back(data_equation(variable_list({vd, vs, vt}), union_(s, cons_(s, vd, vs), cons_(s, vd, vt)), cons_(s, vd, union_(s, vs, vt))));
812 1660 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less(vd, ve), union_(s, cons_(s, vd, vs), cons_(s, ve, vt)), cons_(s, vd, union_(s, vs, cons_(s, ve, vt)))));
813 1660 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less(ve, vd), union_(s, cons_(s, vd, vs), cons_(s, ve, vt)), cons_(s, ve, union_(s, cons_(s, vd, vs), vt))));
814 664 : result.push_back(data_equation(variable_list({vs}), intersection(s, vs, empty(s)), empty(s)));
815 664 : result.push_back(data_equation(variable_list({vt}), intersection(s, empty(s), vt), empty(s)));
816 1328 : result.push_back(data_equation(variable_list({vd, vs, vt}), intersection(s, cons_(s, vd, vs), cons_(s, vd, vt)), cons_(s, vd, intersection(s, vs, vt))));
817 1660 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less(vd, ve), intersection(s, cons_(s, vd, vs), cons_(s, ve, vt)), intersection(s, vs, cons_(s, ve, vt))));
818 1660 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less(ve, vd), intersection(s, cons_(s, vd, vs), cons_(s, ve, vt)), intersection(s, cons_(s, vd, vs), vt)));
819 332 : result.push_back(data_equation(variable_list(), count(s, empty(s)), sort_nat::c0()));
820 996 : result.push_back(data_equation(variable_list({vd, vs}), count(s, cons_(s, vd, vs)), sort_nat::cnat(sort_nat::succ(count(s, vs)))));
821 996 : result.push_back(data_equation(variable_list({vs, vt}), not_equal_to(vs, vt), sort_bool::not_(equal_to(vs, vt))));
822 664 : return result;
823 332 : }
824 :
825 : } // namespace sort_fset
826 :
827 : } // namespace data
828 :
829 : } // namespace mcrl2
830 :
831 : #endif // MCRL2_DATA_FSET_H
|
