mCRL2
Loading...
Searching...
No Matches
traverser.h
Go to the documentation of this file.
1// Author(s): Jeroen van der Wulp, Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/data/traverser.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_DATA_TRAVERSER_H
13#define MCRL2_DATA_TRAVERSER_H
14
15#include "mcrl2/core/traverser.h"
16#include "mcrl2/data/alias.h"
17#include "mcrl2/data/bag_comprehension.h"
18#include "mcrl2/data/exists.h"
19#include "mcrl2/data/forall.h"
20#include "mcrl2/data/lambda.h"
21#include "mcrl2/data/set_comprehension.h"
22#include "mcrl2/data/structured_sort.h"
23#include "mcrl2/data/untyped_data_parameter.h"
24#include "mcrl2/data/untyped_possible_sorts.h"
25#include "mcrl2/data/untyped_set_or_bag_comprehension.h"
26#include "mcrl2/data/untyped_sort_variable.h"
27#include "mcrl2/data/where_clause.h"
28#include "mcrl2/data/machine_number.h"
29
30
31
32namespace mcrl2::data
33{
34
35// Adds sort expression traversal to a traverser
36//--- start generated add_traverser_sort_expressions code ---//
37template <template <class> class Traverser, class Derived>
38struct add_traverser_sort_expressions: public Traverser<Derived>
39{
40 using super = Traverser<Derived>;
41 using super::enter;
42 using super::leave;
43 using super::apply;
44
45 void apply(const data::variable& x)
46 {
47 static_cast<Derived&>(*this).enter(x);
48 static_cast<Derived&>(*this).apply(x.sort());
49 static_cast<Derived&>(*this).leave(x);
50 }
51
52 void apply(const data::function_symbol& x)
53 {
54 static_cast<Derived&>(*this).enter(x);
55 static_cast<Derived&>(*this).apply(x.sort());
56 static_cast<Derived&>(*this).leave(x);
57 }
58
59 void apply(const data::application& x)
60 {
61 static_cast<Derived&>(*this).enter(x);
62 static_cast<Derived&>(*this).apply(x.head());
63 for (const data_expression& t: x) { static_cast<Derived&>(*this).apply(t); }
64 static_cast<Derived&>(*this).leave(x);
65 }
66
67 void apply(const data::where_clause& x)
68 {
69 static_cast<Derived&>(*this).enter(x);
70 static_cast<Derived&>(*this).apply(x.body());
71 static_cast<Derived&>(*this).apply(x.declarations());
72 static_cast<Derived&>(*this).leave(x);
73 }
74
75 void apply(const data::machine_number& x)
76 {
77 static_cast<Derived&>(*this).enter(x);
78 // skip
79 static_cast<Derived&>(*this).leave(x);
80 }
81
83 {
84 static_cast<Derived&>(*this).enter(x);
85 // skip
86 static_cast<Derived&>(*this).leave(x);
87 }
88
89 void apply(const data::assignment& x)
90 {
91 static_cast<Derived&>(*this).enter(x);
92 static_cast<Derived&>(*this).apply(x.lhs());
93 static_cast<Derived&>(*this).apply(x.rhs());
94 static_cast<Derived&>(*this).leave(x);
95 }
96
98 {
99 static_cast<Derived&>(*this).enter(x);
100 static_cast<Derived&>(*this).apply(x.rhs());
101 static_cast<Derived&>(*this).leave(x);
102 }
103
104 void apply(const data::basic_sort& x)
105 {
106 static_cast<Derived&>(*this).enter(x);
107 // skip
108 static_cast<Derived&>(*this).leave(x);
109 }
110
111 void apply(const data::container_sort& x)
112 {
113 static_cast<Derived&>(*this).enter(x);
114 static_cast<Derived&>(*this).apply(x.element_sort());
115 static_cast<Derived&>(*this).leave(x);
116 }
117
118 void apply(const data::structured_sort& x)
119 {
120 static_cast<Derived&>(*this).enter(x);
121 static_cast<Derived&>(*this).apply(x.constructors());
122 static_cast<Derived&>(*this).leave(x);
123 }
124
125 void apply(const data::function_sort& x)
126 {
127 static_cast<Derived&>(*this).enter(x);
128 static_cast<Derived&>(*this).apply(x.domain());
129 static_cast<Derived&>(*this).apply(x.codomain());
130 static_cast<Derived&>(*this).leave(x);
131 }
132
133 void apply(const data::untyped_sort& x)
134 {
135 static_cast<Derived&>(*this).enter(x);
136 // skip
137 static_cast<Derived&>(*this).leave(x);
138 }
139
141 {
142 static_cast<Derived&>(*this).enter(x);
143 static_cast<Derived&>(*this).apply(x.sorts());
144 static_cast<Derived&>(*this).leave(x);
145 }
146
148 {
149 static_cast<Derived&>(*this).enter(x);
150 // skip
151 static_cast<Derived&>(*this).leave(x);
152 }
153
154 void apply(const data::forall& x)
155 {
156 static_cast<Derived&>(*this).enter(x);
157 static_cast<Derived&>(*this).apply(x.variables());
158 static_cast<Derived&>(*this).apply(x.body());
159 static_cast<Derived&>(*this).leave(x);
160 }
161
162 void apply(const data::exists& x)
163 {
164 static_cast<Derived&>(*this).enter(x);
165 static_cast<Derived&>(*this).apply(x.variables());
166 static_cast<Derived&>(*this).apply(x.body());
167 static_cast<Derived&>(*this).leave(x);
168 }
169
170 void apply(const data::lambda& x)
171 {
172 static_cast<Derived&>(*this).enter(x);
173 static_cast<Derived&>(*this).apply(x.variables());
174 static_cast<Derived&>(*this).apply(x.body());
175 static_cast<Derived&>(*this).leave(x);
176 }
177
179 {
180 static_cast<Derived&>(*this).enter(x);
181 static_cast<Derived&>(*this).apply(x.variables());
182 static_cast<Derived&>(*this).apply(x.body());
183 static_cast<Derived&>(*this).leave(x);
184 }
185
187 {
188 static_cast<Derived&>(*this).enter(x);
189 static_cast<Derived&>(*this).apply(x.variables());
190 static_cast<Derived&>(*this).apply(x.body());
191 static_cast<Derived&>(*this).leave(x);
192 }
193
195 {
196 static_cast<Derived&>(*this).enter(x);
197 static_cast<Derived&>(*this).apply(x.variables());
198 static_cast<Derived&>(*this).apply(x.body());
199 static_cast<Derived&>(*this).leave(x);
200 }
201
203 {
204 static_cast<Derived&>(*this).enter(x);
205 static_cast<Derived&>(*this).apply(x.sort());
206 static_cast<Derived&>(*this).leave(x);
207 }
208
210 {
211 static_cast<Derived&>(*this).enter(x);
212 static_cast<Derived&>(*this).apply(x.arguments());
213 static_cast<Derived&>(*this).leave(x);
214 }
215
216 void apply(const data::alias& x)
217 {
218 static_cast<Derived&>(*this).enter(x);
219 static_cast<Derived&>(*this).apply(x.reference());
220 static_cast<Derived&>(*this).leave(x);
221 }
222
223 void apply(const data::data_equation& x)
224 {
225 static_cast<Derived&>(*this).enter(x);
226 static_cast<Derived&>(*this).apply(x.variables());
227 static_cast<Derived&>(*this).apply(x.condition());
228 static_cast<Derived&>(*this).apply(x.lhs());
229 static_cast<Derived&>(*this).apply(x.rhs());
230 static_cast<Derived&>(*this).leave(x);
231 }
232
234 {
235 static_cast<Derived&>(*this).enter(x);
236 static_cast<Derived&>(*this).apply(x.arguments());
237 static_cast<Derived&>(*this).leave(x);
238 }
239
240 void apply(const data::data_expression& x)
241 {
242 static_cast<Derived&>(*this).enter(x);
244 {
245 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::abstraction>(x));
246 }
247 else if (data::is_variable(x))
248 {
249 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
250 }
252 {
253 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_symbol>(x));
254 }
255 else if (data::is_application(x))
256 {
257 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::application>(x));
258 }
259 else if (data::is_where_clause(x))
260 {
261 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::where_clause>(x));
262 }
264 {
265 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::machine_number>(x));
266 }
268 {
269 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier>(x));
270 }
271 static_cast<Derived&>(*this).leave(x);
272 }
273
275 {
276 static_cast<Derived&>(*this).enter(x);
278 {
279 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::assignment>(x));
280 }
282 {
283 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier_assignment>(x));
284 }
285 static_cast<Derived&>(*this).leave(x);
286 }
287
288 void apply(const data::sort_expression& x)
289 {
290 static_cast<Derived&>(*this).enter(x);
292 {
293 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::basic_sort>(x));
294 }
296 {
297 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::container_sort>(x));
298 }
300 {
301 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::structured_sort>(x));
302 }
303 else if (data::is_function_sort(x))
304 {
305 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_sort>(x));
306 }
307 else if (data::is_untyped_sort(x))
308 {
309 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_sort>(x));
310 }
312 {
313 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_possible_sorts>(x));
314 }
316 {
317 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_sort_variable>(x));
318 }
319 static_cast<Derived&>(*this).leave(x);
320 }
321
322 void apply(const data::abstraction& x)
323 {
324 static_cast<Derived&>(*this).enter(x);
326 {
327 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::forall>(x));
328 }
329 else if (data::is_exists(x))
330 {
331 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::exists>(x));
332 }
333 else if (data::is_lambda(x))
334 {
335 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::lambda>(x));
336 }
338 {
339 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::set_comprehension>(x));
340 }
342 {
343 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::bag_comprehension>(x));
344 }
346 {
347 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
348 }
349 static_cast<Derived&>(*this).leave(x);
350 }
351
352};
353
354/// \\brief Traverser class
355template <typename Derived>
357{
358};
359//--- end generated add_traverser_sort_expressions code ---//
360
361//--- start generated add_traverser_data_expressions code ---//
362template <template <class> class Traverser, class Derived>
363struct add_traverser_data_expressions: public Traverser<Derived>
364{
365 using super = Traverser<Derived>;
366 using super::enter;
367 using super::leave;
368 using super::apply;
369
370 void apply(const data::variable& x)
371 {
372 static_cast<Derived&>(*this).enter(x);
373 // skip
374 static_cast<Derived&>(*this).leave(x);
375 }
376
377 void apply(const data::function_symbol& x)
378 {
379 static_cast<Derived&>(*this).enter(x);
380 // skip
381 static_cast<Derived&>(*this).leave(x);
382 }
383
384 void apply(const data::application& x)
385 {
386 static_cast<Derived&>(*this).enter(x);
387 static_cast<Derived&>(*this).apply(x.head());
388 for (const data_expression& t: x) { static_cast<Derived&>(*this).apply(t); }
389 static_cast<Derived&>(*this).leave(x);
390 }
391
392 void apply(const data::where_clause& x)
393 {
394 static_cast<Derived&>(*this).enter(x);
395 static_cast<Derived&>(*this).apply(x.body());
396 static_cast<Derived&>(*this).apply(x.declarations());
397 static_cast<Derived&>(*this).leave(x);
398 }
399
400 void apply(const data::machine_number& x)
401 {
402 static_cast<Derived&>(*this).enter(x);
403 // skip
404 static_cast<Derived&>(*this).leave(x);
405 }
406
408 {
409 static_cast<Derived&>(*this).enter(x);
410 // skip
411 static_cast<Derived&>(*this).leave(x);
412 }
413
414 void apply(const data::assignment& x)
415 {
416 static_cast<Derived&>(*this).enter(x);
417 static_cast<Derived&>(*this).apply(x.rhs());
418 static_cast<Derived&>(*this).leave(x);
419 }
420
422 {
423 static_cast<Derived&>(*this).enter(x);
424 static_cast<Derived&>(*this).apply(x.rhs());
425 static_cast<Derived&>(*this).leave(x);
426 }
427
428 void apply(const data::forall& x)
429 {
430 static_cast<Derived&>(*this).enter(x);
431 static_cast<Derived&>(*this).apply(x.body());
432 static_cast<Derived&>(*this).leave(x);
433 }
434
435 void apply(const data::exists& x)
436 {
437 static_cast<Derived&>(*this).enter(x);
438 static_cast<Derived&>(*this).apply(x.body());
439 static_cast<Derived&>(*this).leave(x);
440 }
441
442 void apply(const data::lambda& x)
443 {
444 static_cast<Derived&>(*this).enter(x);
445 static_cast<Derived&>(*this).apply(x.body());
446 static_cast<Derived&>(*this).leave(x);
447 }
448
450 {
451 static_cast<Derived&>(*this).enter(x);
452 static_cast<Derived&>(*this).apply(x.body());
453 static_cast<Derived&>(*this).leave(x);
454 }
455
457 {
458 static_cast<Derived&>(*this).enter(x);
459 static_cast<Derived&>(*this).apply(x.body());
460 static_cast<Derived&>(*this).leave(x);
461 }
462
464 {
465 static_cast<Derived&>(*this).enter(x);
466 static_cast<Derived&>(*this).apply(x.body());
467 static_cast<Derived&>(*this).leave(x);
468 }
469
470 void apply(const data::data_equation& x)
471 {
472 static_cast<Derived&>(*this).enter(x);
473 static_cast<Derived&>(*this).apply(x.condition());
474 static_cast<Derived&>(*this).apply(x.lhs());
475 static_cast<Derived&>(*this).apply(x.rhs());
476 static_cast<Derived&>(*this).leave(x);
477 }
478
480 {
481 static_cast<Derived&>(*this).enter(x);
482 static_cast<Derived&>(*this).apply(x.arguments());
483 static_cast<Derived&>(*this).leave(x);
484 }
485
486 void apply(const data::data_expression& x)
487 {
488 static_cast<Derived&>(*this).enter(x);
490 {
491 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::abstraction>(x));
492 }
493 else if (data::is_variable(x))
494 {
495 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
496 }
498 {
499 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_symbol>(x));
500 }
501 else if (data::is_application(x))
502 {
503 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::application>(x));
504 }
505 else if (data::is_where_clause(x))
506 {
507 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::where_clause>(x));
508 }
510 {
511 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::machine_number>(x));
512 }
514 {
515 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier>(x));
516 }
517 static_cast<Derived&>(*this).leave(x);
518 }
519
521 {
522 static_cast<Derived&>(*this).enter(x);
524 {
525 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::assignment>(x));
526 }
528 {
529 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier_assignment>(x));
530 }
531 static_cast<Derived&>(*this).leave(x);
532 }
533
534 void apply(const data::abstraction& x)
535 {
536 static_cast<Derived&>(*this).enter(x);
538 {
539 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::forall>(x));
540 }
541 else if (data::is_exists(x))
542 {
543 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::exists>(x));
544 }
545 else if (data::is_lambda(x))
546 {
547 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::lambda>(x));
548 }
550 {
551 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::set_comprehension>(x));
552 }
554 {
555 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::bag_comprehension>(x));
556 }
558 {
559 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
560 }
561 static_cast<Derived&>(*this).leave(x);
562 }
563
564};
565
566/// \\brief Traverser class
567template <typename Derived>
569{
570};
571//--- end generated add_traverser_data_expressions code ---//
572
573//--- start generated add_traverser_variables code ---//
574template <template <class> class Traverser, class Derived>
575struct add_traverser_variables: public Traverser<Derived>
576{
577 using super = Traverser<Derived>;
578 using super::enter;
579 using super::leave;
580 using super::apply;
581
582 void apply(const data::variable& x)
583 {
584 static_cast<Derived&>(*this).enter(x);
585 // skip
586 static_cast<Derived&>(*this).leave(x);
587 }
588
589 void apply(const data::function_symbol& x)
590 {
591 static_cast<Derived&>(*this).enter(x);
592 // skip
593 static_cast<Derived&>(*this).leave(x);
594 }
595
596 void apply(const data::application& x)
597 {
598 static_cast<Derived&>(*this).enter(x);
599 static_cast<Derived&>(*this).apply(x.head());
600 for (const data_expression& t: x) { static_cast<Derived&>(*this).apply(t); }
601 static_cast<Derived&>(*this).leave(x);
602 }
603
604 void apply(const data::where_clause& x)
605 {
606 static_cast<Derived&>(*this).enter(x);
607 static_cast<Derived&>(*this).apply(x.body());
608 static_cast<Derived&>(*this).apply(x.declarations());
609 static_cast<Derived&>(*this).leave(x);
610 }
611
612 void apply(const data::machine_number& x)
613 {
614 static_cast<Derived&>(*this).enter(x);
615 // skip
616 static_cast<Derived&>(*this).leave(x);
617 }
618
620 {
621 static_cast<Derived&>(*this).enter(x);
622 // skip
623 static_cast<Derived&>(*this).leave(x);
624 }
625
626 void apply(const data::assignment& x)
627 {
628 static_cast<Derived&>(*this).enter(x);
629 static_cast<Derived&>(*this).apply(x.lhs());
630 static_cast<Derived&>(*this).apply(x.rhs());
631 static_cast<Derived&>(*this).leave(x);
632 }
633
635 {
636 static_cast<Derived&>(*this).enter(x);
637 static_cast<Derived&>(*this).apply(x.rhs());
638 static_cast<Derived&>(*this).leave(x);
639 }
640
641 void apply(const data::forall& x)
642 {
643 static_cast<Derived&>(*this).enter(x);
644 static_cast<Derived&>(*this).apply(x.variables());
645 static_cast<Derived&>(*this).apply(x.body());
646 static_cast<Derived&>(*this).leave(x);
647 }
648
649 void apply(const data::exists& x)
650 {
651 static_cast<Derived&>(*this).enter(x);
652 static_cast<Derived&>(*this).apply(x.variables());
653 static_cast<Derived&>(*this).apply(x.body());
654 static_cast<Derived&>(*this).leave(x);
655 }
656
657 void apply(const data::lambda& x)
658 {
659 static_cast<Derived&>(*this).enter(x);
660 static_cast<Derived&>(*this).apply(x.variables());
661 static_cast<Derived&>(*this).apply(x.body());
662 static_cast<Derived&>(*this).leave(x);
663 }
664
666 {
667 static_cast<Derived&>(*this).enter(x);
668 static_cast<Derived&>(*this).apply(x.variables());
669 static_cast<Derived&>(*this).apply(x.body());
670 static_cast<Derived&>(*this).leave(x);
671 }
672
674 {
675 static_cast<Derived&>(*this).enter(x);
676 static_cast<Derived&>(*this).apply(x.variables());
677 static_cast<Derived&>(*this).apply(x.body());
678 static_cast<Derived&>(*this).leave(x);
679 }
680
682 {
683 static_cast<Derived&>(*this).enter(x);
684 static_cast<Derived&>(*this).apply(x.variables());
685 static_cast<Derived&>(*this).apply(x.body());
686 static_cast<Derived&>(*this).leave(x);
687 }
688
689 void apply(const data::data_equation& x)
690 {
691 static_cast<Derived&>(*this).enter(x);
692 static_cast<Derived&>(*this).apply(x.variables());
693 static_cast<Derived&>(*this).apply(x.condition());
694 static_cast<Derived&>(*this).apply(x.lhs());
695 static_cast<Derived&>(*this).apply(x.rhs());
696 static_cast<Derived&>(*this).leave(x);
697 }
698
700 {
701 static_cast<Derived&>(*this).enter(x);
702 static_cast<Derived&>(*this).apply(x.arguments());
703 static_cast<Derived&>(*this).leave(x);
704 }
705
706 void apply(const data::data_expression& x)
707 {
708 static_cast<Derived&>(*this).enter(x);
710 {
711 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::abstraction>(x));
712 }
713 else if (data::is_variable(x))
714 {
715 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
716 }
718 {
719 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_symbol>(x));
720 }
721 else if (data::is_application(x))
722 {
723 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::application>(x));
724 }
725 else if (data::is_where_clause(x))
726 {
727 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::where_clause>(x));
728 }
730 {
731 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::machine_number>(x));
732 }
734 {
735 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier>(x));
736 }
737 static_cast<Derived&>(*this).leave(x);
738 }
739
741 {
742 static_cast<Derived&>(*this).enter(x);
744 {
745 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::assignment>(x));
746 }
748 {
749 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier_assignment>(x));
750 }
751 static_cast<Derived&>(*this).leave(x);
752 }
753
754 void apply(const data::abstraction& x)
755 {
756 static_cast<Derived&>(*this).enter(x);
758 {
759 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::forall>(x));
760 }
761 else if (data::is_exists(x))
762 {
763 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::exists>(x));
764 }
765 else if (data::is_lambda(x))
766 {
767 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::lambda>(x));
768 }
770 {
771 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::set_comprehension>(x));
772 }
774 {
775 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::bag_comprehension>(x));
776 }
778 {
779 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
780 }
781 static_cast<Derived&>(*this).leave(x);
782 }
783
784};
785
786/// \\brief Traverser class
787template <typename Derived>
789{
790};
791//--- end generated add_traverser_variables code ---//
792
793//--- start generated add_traverser_identifier_strings code ---//
794template <template <class> class Traverser, class Derived>
795struct add_traverser_identifier_strings: public Traverser<Derived>
796{
797 using super = Traverser<Derived>;
798 using super::enter;
799 using super::leave;
800 using super::apply;
801
802 void apply(const data::variable& x)
803 {
804 static_cast<Derived&>(*this).enter(x);
805 static_cast<Derived&>(*this).apply(x.name());
806 static_cast<Derived&>(*this).apply(x.sort());
807 static_cast<Derived&>(*this).leave(x);
808 }
809
810 void apply(const data::function_symbol& x)
811 {
812 static_cast<Derived&>(*this).enter(x);
813 static_cast<Derived&>(*this).apply(x.name());
814 static_cast<Derived&>(*this).apply(x.sort());
815 static_cast<Derived&>(*this).leave(x);
816 }
817
818 void apply(const data::application& x)
819 {
820 static_cast<Derived&>(*this).enter(x);
821 static_cast<Derived&>(*this).apply(x.head());
822 for (const data_expression& t: x) { static_cast<Derived&>(*this).apply(t); }
823 static_cast<Derived&>(*this).leave(x);
824 }
825
826 void apply(const data::where_clause& x)
827 {
828 static_cast<Derived&>(*this).enter(x);
829 static_cast<Derived&>(*this).apply(x.body());
830 static_cast<Derived&>(*this).apply(x.declarations());
831 static_cast<Derived&>(*this).leave(x);
832 }
833
834 void apply(const data::machine_number& x)
835 {
836 static_cast<Derived&>(*this).enter(x);
837 // skip
838 static_cast<Derived&>(*this).leave(x);
839 }
840
842 {
843 static_cast<Derived&>(*this).enter(x);
844 static_cast<Derived&>(*this).apply(x.name());
845 static_cast<Derived&>(*this).leave(x);
846 }
847
848 void apply(const data::assignment& x)
849 {
850 static_cast<Derived&>(*this).enter(x);
851 static_cast<Derived&>(*this).apply(x.lhs());
852 static_cast<Derived&>(*this).apply(x.rhs());
853 static_cast<Derived&>(*this).leave(x);
854 }
855
857 {
858 static_cast<Derived&>(*this).enter(x);
859 static_cast<Derived&>(*this).apply(x.lhs());
860 static_cast<Derived&>(*this).apply(x.rhs());
861 static_cast<Derived&>(*this).leave(x);
862 }
863
864 void apply(const data::basic_sort& x)
865 {
866 static_cast<Derived&>(*this).enter(x);
867 static_cast<Derived&>(*this).apply(x.name());
868 static_cast<Derived&>(*this).leave(x);
869 }
870
871 void apply(const data::container_sort& x)
872 {
873 static_cast<Derived&>(*this).enter(x);
874 static_cast<Derived&>(*this).apply(x.element_sort());
875 static_cast<Derived&>(*this).leave(x);
876 }
877
878 void apply(const data::structured_sort& x)
879 {
880 static_cast<Derived&>(*this).enter(x);
881 static_cast<Derived&>(*this).apply(x.constructors());
882 static_cast<Derived&>(*this).leave(x);
883 }
884
885 void apply(const data::function_sort& x)
886 {
887 static_cast<Derived&>(*this).enter(x);
888 static_cast<Derived&>(*this).apply(x.domain());
889 static_cast<Derived&>(*this).apply(x.codomain());
890 static_cast<Derived&>(*this).leave(x);
891 }
892
893 void apply(const data::untyped_sort& x)
894 {
895 static_cast<Derived&>(*this).enter(x);
896 // skip
897 static_cast<Derived&>(*this).leave(x);
898 }
899
901 {
902 static_cast<Derived&>(*this).enter(x);
903 static_cast<Derived&>(*this).apply(x.sorts());
904 static_cast<Derived&>(*this).leave(x);
905 }
906
908 {
909 static_cast<Derived&>(*this).enter(x);
910 // skip
911 static_cast<Derived&>(*this).leave(x);
912 }
913
914 void apply(const data::forall& x)
915 {
916 static_cast<Derived&>(*this).enter(x);
917 static_cast<Derived&>(*this).apply(x.variables());
918 static_cast<Derived&>(*this).apply(x.body());
919 static_cast<Derived&>(*this).leave(x);
920 }
921
922 void apply(const data::exists& x)
923 {
924 static_cast<Derived&>(*this).enter(x);
925 static_cast<Derived&>(*this).apply(x.variables());
926 static_cast<Derived&>(*this).apply(x.body());
927 static_cast<Derived&>(*this).leave(x);
928 }
929
930 void apply(const data::lambda& x)
931 {
932 static_cast<Derived&>(*this).enter(x);
933 static_cast<Derived&>(*this).apply(x.variables());
934 static_cast<Derived&>(*this).apply(x.body());
935 static_cast<Derived&>(*this).leave(x);
936 }
937
939 {
940 static_cast<Derived&>(*this).enter(x);
941 static_cast<Derived&>(*this).apply(x.variables());
942 static_cast<Derived&>(*this).apply(x.body());
943 static_cast<Derived&>(*this).leave(x);
944 }
945
947 {
948 static_cast<Derived&>(*this).enter(x);
949 static_cast<Derived&>(*this).apply(x.variables());
950 static_cast<Derived&>(*this).apply(x.body());
951 static_cast<Derived&>(*this).leave(x);
952 }
953
955 {
956 static_cast<Derived&>(*this).enter(x);
957 static_cast<Derived&>(*this).apply(x.variables());
958 static_cast<Derived&>(*this).apply(x.body());
959 static_cast<Derived&>(*this).leave(x);
960 }
961
963 {
964 static_cast<Derived&>(*this).enter(x);
965 static_cast<Derived&>(*this).apply(x.name());
966 static_cast<Derived&>(*this).apply(x.sort());
967 static_cast<Derived&>(*this).leave(x);
968 }
969
971 {
972 static_cast<Derived&>(*this).enter(x);
973 static_cast<Derived&>(*this).apply(x.name());
974 static_cast<Derived&>(*this).apply(x.arguments());
975 static_cast<Derived&>(*this).apply(x.recogniser());
976 static_cast<Derived&>(*this).leave(x);
977 }
978
979 void apply(const data::alias& x)
980 {
981 static_cast<Derived&>(*this).enter(x);
982 static_cast<Derived&>(*this).apply(x.name());
983 static_cast<Derived&>(*this).apply(x.reference());
984 static_cast<Derived&>(*this).leave(x);
985 }
986
987 void apply(const data::data_equation& x)
988 {
989 static_cast<Derived&>(*this).enter(x);
990 static_cast<Derived&>(*this).apply(x.variables());
991 static_cast<Derived&>(*this).apply(x.condition());
992 static_cast<Derived&>(*this).apply(x.lhs());
993 static_cast<Derived&>(*this).apply(x.rhs());
994 static_cast<Derived&>(*this).leave(x);
995 }
996
998 {
999 static_cast<Derived&>(*this).enter(x);
1000 static_cast<Derived&>(*this).apply(x.name());
1001 static_cast<Derived&>(*this).apply(x.arguments());
1002 static_cast<Derived&>(*this).leave(x);
1003 }
1004
1006 {
1007 static_cast<Derived&>(*this).enter(x);
1009 {
1010 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::abstraction>(x));
1011 }
1012 else if (data::is_variable(x))
1013 {
1014 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
1015 }
1017 {
1018 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_symbol>(x));
1019 }
1020 else if (data::is_application(x))
1021 {
1022 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::application>(x));
1023 }
1024 else if (data::is_where_clause(x))
1025 {
1026 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::where_clause>(x));
1027 }
1028 else if (data::is_machine_number(x))
1029 {
1030 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::machine_number>(x));
1031 }
1033 {
1034 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier>(x));
1035 }
1036 static_cast<Derived&>(*this).leave(x);
1037 }
1038
1040 {
1041 static_cast<Derived&>(*this).enter(x);
1043 {
1044 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::assignment>(x));
1045 }
1047 {
1048 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier_assignment>(x));
1049 }
1050 static_cast<Derived&>(*this).leave(x);
1051 }
1052
1054 {
1055 static_cast<Derived&>(*this).enter(x);
1057 {
1058 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::basic_sort>(x));
1059 }
1060 else if (data::is_container_sort(x))
1061 {
1062 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::container_sort>(x));
1063 }
1065 {
1066 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::structured_sort>(x));
1067 }
1068 else if (data::is_function_sort(x))
1069 {
1070 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_sort>(x));
1071 }
1072 else if (data::is_untyped_sort(x))
1073 {
1074 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_sort>(x));
1075 }
1077 {
1078 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_possible_sorts>(x));
1079 }
1081 {
1082 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_sort_variable>(x));
1083 }
1084 static_cast<Derived&>(*this).leave(x);
1085 }
1086
1087 void apply(const data::abstraction& x)
1088 {
1089 static_cast<Derived&>(*this).enter(x);
1090 if (data::is_forall(x))
1091 {
1092 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::forall>(x));
1093 }
1094 else if (data::is_exists(x))
1095 {
1096 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::exists>(x));
1097 }
1098 else if (data::is_lambda(x))
1099 {
1100 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::lambda>(x));
1101 }
1103 {
1104 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::set_comprehension>(x));
1105 }
1107 {
1108 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::bag_comprehension>(x));
1109 }
1111 {
1112 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
1113 }
1114 static_cast<Derived&>(*this).leave(x);
1115 }
1116
1117};
1118
1119/// \\brief Traverser class
1120template <typename Derived>
1122{
1123};
1124//--- end generated add_traverser_identifier_strings code ---//
1125
1126} // namespace mcrl2::data
1127
1128
1129
1130#endif // MCRL2_DATA_TRAVERSER_H
An integer term stores a single std::size_t value. It carries no arguments.
Definition aterm_int.h:26
aterm_string & operator=(aterm_string &&t) noexcept=default
aterm & operator=(const aterm &other) noexcept=default
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
A list of aterm objects.
Definition aterm_list.h:26
A unordered_map class in which aterms can be stored.
apply_builder_arg1(const Arg1 &arg1)
Definition builder.h:120
apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:144
singleton_expression & operator=(singleton_expression &&)=delete
singleton_expression & operator=(const singleton_expression &)=delete
singleton_expression(singleton_expression &&)=delete
singleton_expression(const singleton_expression &)=delete
parse_node_exception(const std::string &message)
Definition parse.h:47
parse_node_exception(const parse_node &node, const std::string &message)
Definition parse.h:52
static std::string get_error_message(const parse_node &node, const std::string &user_message)
Definition parse.h:35
parse_node_unexpected_exception(const parser &p, const parse_node &node)
Definition parse.h:76
static std::string get_error_message(const parser &p, const parse_node &node)
Definition parse.h:60
update_apply_builder_arg1(const Function &f, const Arg1 &arg1)
Definition builder.h:212
void apply(T &result, const argument_type &x)
Definition builder.h:207
An abstraction expression.
Definition abstraction.h:23
const variable_list & variables() const
Definition abstraction.h:60
abstraction(const atermpp::aterm &term)
Constructor.
Definition abstraction.h:32
abstraction(const binder_type &binding_operator, const variable_list &variables, const data_expression &body)
Constructor.
Definition abstraction.h:39
abstraction(const abstraction &) noexcept=default
Move semantics.
abstraction(const binder_type &binding_operator, const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Constructor.
Definition abstraction.h:45
abstraction & operator=(abstraction &&) noexcept=default
const data_expression & body() const
Definition abstraction.h:65
abstraction(abstraction &&) noexcept=default
abstraction()
Default constructor.
Definition abstraction.h:26
const binder_type & binding_operator() const
Definition abstraction.h:55
abstraction & operator=(const abstraction &) noexcept=default
\brief A sort alias
Definition alias.h:23
alias()
\brief Default constructor X3.
Definition alias.h:26
alias(const alias &) noexcept=default
Move semantics.
alias & operator=(const alias &) noexcept=default
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
Definition alias.h:39
alias(alias &&) noexcept=default
alias(const atermpp::aterm &term)
Definition alias.h:32
alias & operator=(alias &&) noexcept=default
const basic_sort & name() const
Definition alias.h:49
const sort_expression & reference() const
Definition alias.h:54
\brief Assignment expression
Definition assignment.h:24
assignment_expression(assignment_expression &&) noexcept=default
assignment_expression()
\brief Default constructor X3.
Definition assignment.h:27
assignment_expression & operator=(const assignment_expression &) noexcept=default
assignment_expression(const assignment_expression &) noexcept=default
Move semantics.
assignment_expression & operator=(assignment_expression &&) noexcept=default
assignment_expression(const atermpp::aterm &term)
Definition assignment.h:33
\brief Assignment of a data expression to a variable
Definition assignment.h:88
assignment(const variable &lhs, const data_expression &rhs)
\brief Constructor Z14.
Definition assignment.h:104
const data_expression & rhs() const
Definition assignment.h:119
assignment(const atermpp::aterm &term)
Definition assignment.h:97
assignment(assignment &&) noexcept=default
assignment & operator=(assignment &&) noexcept=default
const variable & lhs() const
Definition assignment.h:114
assignment & operator=(const assignment &) noexcept=default
assignment(const assignment &) noexcept=default
Move semantics.
assignment()
\brief Default constructor X3.
Definition assignment.h:91
const data_expression & operator()(const variable &x) const
Applies the assignment to a variable.
Definition assignment.h:127
\brief Binder for bag comprehension
bag_comprehension_binder(const atermpp::aterm &term)
bag_comprehension_binder & operator=(const bag_comprehension_binder &) noexcept=default
bag_comprehension_binder(const bag_comprehension_binder &) noexcept=default
Move semantics.
bag_comprehension_binder()
\brief Default constructor X3.
bag_comprehension_binder(bag_comprehension_binder &&) noexcept=default
bag_comprehension_binder & operator=(bag_comprehension_binder &&) noexcept=default
universal quantification.
bag_comprehension(const bag_comprehension &) noexcept=default
Move semantics.
bag_comprehension & operator=(bag_comprehension &&) noexcept=default
bag_comprehension & operator=(const bag_comprehension &) noexcept=default
bag_comprehension(bag_comprehension &&) noexcept=default
bag_comprehension(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
\brief Container type for bags
bag_container(const bag_container &) noexcept=default
Move semantics.
bag_container(bag_container &&) noexcept=default
bag_container & operator=(bag_container &&) noexcept=default
bag_container()
\brief Default constructor X3.
bag_container(const atermpp::aterm &term)
bag_container & operator=(const bag_container &) noexcept=default
\brief A basic sort
Definition basic_sort.h:25
basic_sort(const basic_sort &) noexcept=default
Move semantics.
basic_sort()
\brief Default constructor X3.
Definition basic_sort.h:28
basic_sort & operator=(const basic_sort &) noexcept=default
const core::identifier_string & name() const
Definition basic_sort.h:56
basic_sort(basic_sort &&) noexcept=default
basic_sort(const core::identifier_string &name)
\brief Constructor Z14.
Definition basic_sort.h:41
basic_sort(const std::string &name)
\brief Constructor Z2.
Definition basic_sort.h:46
basic_sort & operator=(basic_sort &&) noexcept=default
basic_sort(const atermpp::aterm &term)
Definition basic_sort.h:34
binder_type()
\brief Default constructor X3.
Definition binder_type.h:27
binder_type(binder_type &&) noexcept=default
binder_type & operator=(const binder_type &) noexcept=default
binder_type & operator=(binder_type &&) noexcept=default
binder_type(const binder_type &) noexcept=default
Move semantics.
binder_type(const atermpp::aterm &term)
Definition binder_type.h:33
\brief A container sort
container_sort()
\brief Default constructor X3.
container_sort & operator=(container_sort &&) noexcept=default
container_sort(const container_sort &) noexcept=default
Move semantics.
container_sort(const container_type &container_name, const sort_expression &element_sort)
\brief Constructor Z14.
container_sort(container_sort &&) noexcept=default
container_sort & operator=(const container_sort &) noexcept=default
const container_type & container_name() const
const sort_expression & element_sort() const
container_sort(const atermpp::aterm &term)
\brief Container type
container_type(container_type &&) noexcept=default
container_type(const atermpp::aterm &term)
container_type & operator=(const container_type &) noexcept=default
container_type & operator=(container_type &&) noexcept=default
container_type(const container_type &) noexcept=default
Move semantics.
container_type()
\brief Default constructor X3.
\brief A data equation
data_equation(const atermpp::aterm &term)
data_equation()
\brief Default constructor X3.
const data_expression & lhs() const
const data_expression & condition() const
data_equation & operator=(data_equation &&) noexcept=default
data_equation(const Container &variables, const data_expression &lhs, const data_expression &rhs, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Constructor.
const data_expression & rhs() const
data_equation(data_equation &&) noexcept=default
data_equation(const variable_list &variables, const data_expression &condition, const data_expression &lhs, const data_expression &rhs)
\brief Constructor Z12.
const variable_list & variables() const
data_equation & operator=(const data_equation &) noexcept=default
data_equation(const data_expression &lhs, const data_expression &rhs)
Constructor.
data_expression & operator=(const data_expression &) noexcept=default
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4) const
Apply a data expression to four data expressions.
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3) const
Apply a data expression to three data expressions.
data_expression(const atermpp::aterm &term)
data_expression()
\brief Default constructor X3.
application operator()(const data_expression &e1, const data_expression &e2) const
Apply a data expression to two data expressions.
data_expression & operator=(data_expression &&) noexcept=default
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
const_iterator end() const
application operator()(const data_expression &e) const
Apply a data expression to a data expression.
data_expression(const data_expression &) noexcept=default
Move semantics.
data_expression(data_expression &&) noexcept=default
const_iterator begin() const
bool is_default_data_expression() const
A function to efficiently determine whether a data expression is made by the default constructor.
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5) const
Apply a data expression to five data expressions.
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5, const data_expression &e6) const
Apply a data expression to six data expressions.
\brief Binder for existential quantification
exists_binder(const exists_binder &) noexcept=default
Move semantics.
exists_binder & operator=(exists_binder &&) noexcept=default
exists_binder(exists_binder &&) noexcept=default
exists_binder & operator=(const exists_binder &) noexcept=default
exists_binder()
\brief Default constructor X3.
exists_binder(const atermpp::aterm &term)
existential quantification.
Definition exists.h:23
exists(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Definition exists.h:44
exists & operator=(exists &&) noexcept=default
exists(const aterm &d)
Definition exists.h:31
exists(exists &&) noexcept=default
exists & operator=(const exists &) noexcept=default
exists(const exists &) noexcept=default
Move semantics.
\brief Container type for finite bags
fbag_container & operator=(const fbag_container &) noexcept=default
fbag_container()
\brief Default constructor X3.
fbag_container(const fbag_container &) noexcept=default
Move semantics.
fbag_container & operator=(fbag_container &&) noexcept=default
fbag_container(const atermpp::aterm &term)
fbag_container(fbag_container &&) noexcept=default
\brief Binder for universal quantification
forall_binder(const forall_binder &) noexcept=default
Move semantics.
forall_binder & operator=(forall_binder &&) noexcept=default
forall_binder(const atermpp::aterm &term)
forall_binder()
\brief Default constructor X3.
forall_binder(forall_binder &&) noexcept=default
forall_binder & operator=(const forall_binder &) noexcept=default
universal quantification.
Definition forall.h:25
forall(forall &&) noexcept=default
forall(const aterm &d)
Definition forall.h:33
forall & operator=(const forall &) noexcept=default
forall(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Definition forall.h:46
forall & operator=(forall &&) noexcept=default
forall(const forall &) noexcept=default
Move semantics.
\brief Container type for finite sets
fset_container(fset_container &&) noexcept=default
fset_container(const fset_container &) noexcept=default
Move semantics.
fset_container(const atermpp::aterm &term)
fset_container()
\brief Default constructor X3.
fset_container & operator=(fset_container &&) noexcept=default
fset_container & operator=(const fset_container &) noexcept=default
\brief A function sort
const sort_expression & codomain() const
function_sort()
\brief Default constructor X3.
function_sort(const sort_expression_list &domain, const sort_expression &codomain)
\brief Constructor Z14.
function_sort & operator=(const function_sort &) noexcept=default
function_sort(const atermpp::aterm &term)
function_sort & operator=(function_sort &&) noexcept=default
function_sort(function_sort &&) noexcept=default
const sort_expression_list & domain() const
\brief A function symbol
function_symbol(const core::identifier_string &name, const sort_expression &sort)
Constructor.
function_symbol(const function_symbol &) noexcept=default
Move semantics.
function_symbol & operator=(function_symbol &&) noexcept=default
function_symbol()
Default constructor.
function_symbol(function_symbol &&) noexcept=default
function_symbol(const atermpp::aterm &term)
Constructor.
const core::identifier_string & name() const
const sort_expression & sort() const
function_symbol & operator=(const function_symbol &) noexcept=default
function_symbol(const std::string &name, const sort_expression &sort)
Constructor.
Abstract base class for identifier generators. Identifier generators generate fresh names that do not...
virtual core::identifier_string operator()(const std::string &hint, bool add_to_context=true)
Returns a fresh identifier, with the given hint as prefix. The returned identifier is added to the co...
virtual ~identifier_generator()=default
Destructor.
virtual void add_identifier(const core::identifier_string &s)=0
Adds the identifier s to the context.
virtual bool has_identifier(const core::identifier_string &s) const =0
Returns true if the identifier s appears in the context.
identifier_generator()=default
Constructor.
void remove_identifiers(const std::set< core::identifier_string > &ids)
Remove a set of identifiers from the context.
virtual void remove_identifier(const core::identifier_string &s)=0
Removes the identifier s from the context.
virtual void clear_context()=0
Clears the context.
void add_identifiers(const std::set< core::identifier_string > &ids)
Add a set of identifiers to the context.
\brief Binder for lambda abstraction
lambda_binder & operator=(lambda_binder &&) noexcept=default
lambda_binder(const atermpp::aterm &term)
lambda_binder()
\brief Default constructor X3.
lambda_binder(lambda_binder &&) noexcept=default
lambda_binder & operator=(const lambda_binder &) noexcept=default
lambda_binder(const lambda_binder &) noexcept=default
Move semantics.
function symbol.
Definition lambda.h:24
lambda(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Definition lambda.h:57
lambda(const variable &variable, const data_expression &body)
Definition lambda.h:45
lambda & operator=(const lambda &) noexcept=default
lambda(const aterm &d)
Definition lambda.h:33
lambda()=default
Constructor.
lambda(const lambda &) noexcept=default
Move semantics.
lambda(lambda &&) noexcept=default
lambda & operator=(lambda &&) noexcept=default
\brief Container type for lists
list_container(list_container &&) noexcept=default
list_container()
\brief Default constructor X3.
list_container & operator=(list_container &&) noexcept=default
list_container & operator=(const list_container &) noexcept=default
list_container(const list_container &) noexcept=default
Move semantics.
list_container(const atermpp::aterm &term)
\brief A machine number
machine_number()
\brief Default constructor X2.
machine_number & operator=(machine_number &&) noexcept=default
machine_number & operator=(const machine_number &) noexcept=default
std::size_t value() const
machine_number(const machine_number &) noexcept=default
Move semantics.
machine_number(std::size_t value)
\brief Constructor Z13.
machine_number(machine_number &&) noexcept=default
machine_number(const atermpp::aterm &term)
Identifier generator that stores the identifiers of the context in a multiset. If an identifier occur...
bool has_identifier(const core::identifier_string &s) const override
Returns true if the identifier s appears in the context.
void remove_identifier(const core::identifier_string &s) override
Removes one occurrence of the identifier s from the context.
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
void clear_context() override
Clears the context.
const std::multiset< core::identifier_string > & context() const
Returns the context.
std::multiset< core::identifier_string > m_identifiers
The context of the identifier generator.
multiset_identifier_generator()=default
Constructor.
\brief Binder for set comprehension
set_comprehension_binder(const atermpp::aterm &term)
set_comprehension_binder & operator=(set_comprehension_binder &&) noexcept=default
set_comprehension_binder & operator=(const set_comprehension_binder &) noexcept=default
set_comprehension_binder()
\brief Default constructor X3.
set_comprehension_binder(set_comprehension_binder &&) noexcept=default
set_comprehension_binder(const set_comprehension_binder &) noexcept=default
Move semantics.
universal quantification.
set_comprehension & operator=(set_comprehension &&) noexcept=default
set_comprehension(set_comprehension &&) noexcept=default
set_comprehension(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
set_comprehension & operator=(const set_comprehension &) noexcept=default
set_comprehension(const set_comprehension &) noexcept=default
Move semantics.
\brief Container type for sets
set_container()
\brief Default constructor X3.
set_container(const set_container &) noexcept=default
Move semantics.
set_container(set_container &&) noexcept=default
set_container & operator=(set_container &&) noexcept=default
set_container & operator=(const set_container &) noexcept=default
set_container(const atermpp::aterm &term)
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
const std::set< core::identifier_string > & context() const
Returns the context.
void remove_identifier(const core::identifier_string &s) override
Removes one occurrence of the identifier s from the context.
set_identifier_generator()=default
Constructor.
void clear_context() override
Clears the context.
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
std::set< core::identifier_string > m_identifiers
The context of the identifier generator.
bool has_identifier(const core::identifier_string &s) const override
Returns true if the identifier s appears in the context.
\brief A sort expression
sort_expression & operator=(const sort_expression &) noexcept=default
sort_expression(const sort_expression &) noexcept=default
Move semantics.
sort_expression & operator=(sort_expression &&) noexcept=default
const sort_expression & target_sort() const
Returns the target sort of this expression.
sort_expression(sort_expression &&) noexcept=default
sort_expression()
\brief Default constructor X3.
sort_expression(const atermpp::aterm &term)
std::map< sort_expression, sort_expression > m_normalised_aliases
Table containing how sorts should be mapped to normalised sorts.
const std::set< sort_expression > & context_sorts() const
Return the user defined context sorts of the current specification.
void remove_sort(const sort_expression &s)
Removes sort from the user defined sorts in the specification. Note that this does not remove aliases...
void add_system_defined_sort(const sort_expression &s)
Adds a sort to this specification, and marks it as system defined.
basic_sort_vector m_user_defined_sorts
The basic sorts and structured sorts in the specification.
bool operator==(const sort_specification &other) const
std::set< sort_expression > m_sorts_in_context
The sorts that occur are needed in this sort specification but are not explicitly defined as user def...
const std::map< sort_expression, sort_expression > & sort_alias_map() const
Gets a normalisation mapping that maps each sort to its unique normalised sort.
const std::set< sort_expression > & sorts() const
Gets the normalised sort declarations including those that are system defined. This is the set with a...
void add_context_sorts(const Container &c, typename atermpp::enable_if_container< Container >::type *=nullptr)
Adds the sorts in c to the context sorts.
const basic_sort_vector & user_defined_sorts() const
Gets all sorts defined by a user (excluding the system defined sorts).
void check_for_alias_loop(const sort_expression &s, std::set< sort_expression > sorts_already_seen, bool toplevel=true) const
bool m_normalised_data_is_up_to_date
The variable below indicates whether a surrounding data specification is up to data with respect to s...
alias_vector m_user_defined_aliases
The basic sorts and structured sorts in the specification.
sort_specification()
Default constructor.
void sorts_are_not_necessarily_normalised_anymore() const
void data_is_not_necessarily_normalised_anymore() const
void add_alias(const alias &a)
Adds an alias (new name for a sort) to this specification.
void add_sort(const basic_sort &s)
Adds a sort to this specification.
sort_specification(const basic_sort_vector &sorts, const alias_vector &aliases)
std::set< sort_expression > m_normalised_sorts
Set containing all the sorts, including the system defined ones.
void remove_alias(const alias &a)
Removes a user defined //alias from specification.
void add_context_sort(const sort_expression &s)
Adds the sort s to the context sorts.
void import_system_defined_sorts(const CONTAINER &sorts)
const alias_vector & user_defined_aliases() const
Gets the user defined aliases.
bool m_normalised_sorts_are_up_to_date
This boolean indicates whether the variables m_normalised_constructors, m_mappings,...
void import_system_defined_sort(const sort_expression &sort)
Adds the system defined sorts in a sequence. The second argument is used to check which sorts are add...
\brief An argument of a constructor of a structured sort
structured_sort_constructor_argument(const sort_expression &sort)
Constructor.
structured_sort_constructor_argument(const std::string &name, const sort_expression &sort)
\brief Constructor Z1.
structured_sort_constructor_argument(const core::identifier_string &name, const sort_expression &sort)
\brief Constructor Z12.
structured_sort_constructor_argument(structured_sort_constructor_argument &&) noexcept=default
structured_sort_constructor_argument(const char(&name)[S], const sort_expression &sort)
structured_sort_constructor_argument & operator=(const structured_sort_constructor_argument &) noexcept=default
structured_sort_constructor_argument(const structured_sort_constructor_argument &) noexcept=default
Move semantics.
structured_sort_constructor_argument & operator=(structured_sort_constructor_argument &&) noexcept=default
\brief A constructor for a structured sort
function_symbol constructor_function(const sort_expression &s) const
Returns the constructor function for this constructor, assuming it is internally represented with sor...
const core::identifier_string & name() const
structured_sort_constructor(const std::string &name, const structured_sort_constructor_argument_list &arguments, typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=0)
Constructor.
structured_sort_constructor & operator=(structured_sort_constructor &&) noexcept=default
structured_sort_constructor(const char(&name)[S], const Container &arguments, const char(&recogniser)[S0], typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=nullptr)
structured_sort_constructor & operator=(const structured_sort_constructor &) noexcept=default
structured_sort_constructor(const core::identifier_string &name, const structured_sort_constructor_argument_list &arguments, core::identifier_string &recogniser)
\brief Constructor Z12.
structured_sort_constructor(const core::identifier_string &name, const core::identifier_string &recogniser)
Constructor.
structured_sort_constructor(const std::string &name, const std::string &recogniser)
Constructor.
function_symbol_vector projection_functions(const sort_expression &s) const
Returns the projection functions for this constructor.
structured_sort_constructor(const std::string &name)
Constructor.
structured_sort_constructor(structured_sort_constructor &&) noexcept=default
const core::identifier_string & recogniser() const
function_symbol recogniser_function(const sort_expression &s) const
Returns the function corresponding to the recogniser of this constructor, such that it is usable in t...
structured_sort_constructor(const std::string &name, const Container &arguments, typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=nullptr)
Constructor.
const structured_sort_constructor_argument_list & arguments() const
structured_sort_constructor()
\brief Default constructor X3.
void argument_sorts(OutIter out) const
Returns the sorts of the arguments in an output iterator.
structured_sort_constructor(const core::identifier_string &name)
Constructor.
data_equation_vector recogniser_equations() const
Generate equations for the recognisers of this sort, assuming that this sort is referred to with s.
function_symbol smaller_arguments_function(const sort_expression &s) const
structured_sort & operator=(const structured_sort &) noexcept=default
function_symbol_vector recogniser_functions(const sort_expression &s) const
function_symbol to_pos_function(const sort_expression &s) const
function_symbol_vector constructor_functions(const sort_expression &s) const
data_equation_vector comparison_equations() const
Returns the equations for the functions used to implement comparison operators on this sort....
data_equation_vector constructor_equations(const sort_expression &s) const
data_equation_vector recogniser_equations(const sort_expression &s) const
static bool has_recogniser(structured_sort_constructor const &s)
data_equation_vector projection_equations() const
Generate equations for the projection functions of this sort.
function_symbol equal_arguments_function(const sort_expression &s) const
const structured_sort_constructor_list & constructors() const
function_symbol_vector constructor_functions() const
Returns the constructor functions of this sort, such that the result can be used by the rewriter.
function_symbol_vector projection_functions() const
Returns the projection functions of this sort, such that the result can be used by the rewriter.
function_symbol_vector comparison_functions(const sort_expression &s) const
function_symbol_vector comparison_functions() const
Returns the additional functions of this sort, used to implement its comparison operators.
data_equation_vector comparison_equations(const sort_expression &s) const
structured_sort(const structured_sort_constructor_list &constructors)
\brief Constructor Z14.
function_symbol_vector recogniser_functions() const
Returns the recogniser functions of this sort, such that the result can be used by the rewriter.
function_symbol_vector projection_functions(const sort_expression &s) const
structured_sort()
\brief Default constructor X3.
structured_sort(structured_sort &&) noexcept=default
data_equation_vector projection_equations(const sort_expression &s) const
structured_sort(const atermpp::aterm &term)
structured_sort & operator=(structured_sort &&) noexcept=default
data_equation_vector constructor_equations() const
Returns the equations for ==, < and <= for this sort, such that the result can be used by the rewrite...
function_symbol smaller_equal_arguments_function(const sort_expression &s) const
untyped_data_parameter(const core::identifier_string &name, const data_expression_list &arguments)
\brief Constructor Z12.
const core::identifier_string & name() const
untyped_data_parameter(const std::string &name, const data_expression_list &arguments)
\brief Constructor Z1.
const data_expression_list & arguments() const
untyped_data_parameter(const untyped_data_parameter &) noexcept=default
Move semantics.
untyped_data_parameter & operator=(untyped_data_parameter &&) noexcept=default
untyped_data_parameter & operator=(const untyped_data_parameter &) noexcept=default
untyped_data_parameter(const atermpp::aterm &term)
untyped_data_parameter(untyped_data_parameter &&) noexcept=default
untyped_data_parameter()
\brief Default constructor X3.
\brief Assignment of a data expression to a string
Definition assignment.h:179
const core::identifier_string & lhs() const
Definition assignment.h:210
untyped_identifier_assignment(const std::string &lhs, const data_expression &rhs)
\brief Constructor Z2.
Definition assignment.h:200
untyped_identifier_assignment(const atermpp::aterm &term)
Definition assignment.h:188
untyped_identifier_assignment()
\brief Default constructor X3.
Definition assignment.h:182
const data_expression & rhs() const
Definition assignment.h:215
untyped_identifier_assignment & operator=(untyped_identifier_assignment &&) noexcept=default
untyped_identifier_assignment & operator=(const untyped_identifier_assignment &) noexcept=default
untyped_identifier_assignment(const core::identifier_string &lhs, const data_expression &rhs)
\brief Constructor Z14.
Definition assignment.h:195
untyped_identifier_assignment(untyped_identifier_assignment &&) noexcept=default
untyped_identifier_assignment(const untyped_identifier_assignment &) noexcept=default
Move semantics.
data_expression operator()(const untyped_identifier &x) const
Applies the assignment to a variable.
Definition assignment.h:223
\brief An untyped identifier
untyped_identifier(const atermpp::aterm &term)
untyped_identifier(const untyped_identifier &) noexcept=default
Move semantics.
untyped_identifier(const std::string &name)
\brief Constructor Z2.
untyped_identifier & operator=(untyped_identifier &&) noexcept=default
const core::identifier_string & name() const
untyped_identifier(untyped_identifier &&) noexcept=default
untyped_identifier & operator=(const untyped_identifier &) noexcept=default
untyped_identifier()
\brief Default constructor X3.
untyped_identifier(const core::identifier_string &name)
\brief Constructor Z14.
untyped_possible_sorts & operator=(const untyped_possible_sorts &) noexcept=default
untyped_possible_sorts & operator=(untyped_possible_sorts &&) noexcept=default
untyped_possible_sorts(const sort_expression_list &sorts)
\brief Constructor Z14.
untyped_possible_sorts(const atermpp::aterm &term)
untyped_possible_sorts(untyped_possible_sorts &&) noexcept=default
untyped_possible_sorts()
\brief Default constructor X3.
const sort_expression_list & sorts() const
\brief Binder for untyped set or bag comprehension
Definition binder_type.h:74
untyped_set_or_bag_comprehension_binder(untyped_set_or_bag_comprehension_binder &&) noexcept=default
untyped_set_or_bag_comprehension_binder(const atermpp::aterm &term)
Definition binder_type.h:83
untyped_set_or_bag_comprehension_binder()
\brief Default constructor X3.
Definition binder_type.h:77
untyped_set_or_bag_comprehension_binder(const untyped_set_or_bag_comprehension_binder &) noexcept=default
Move semantics.
untyped_set_or_bag_comprehension_binder & operator=(const untyped_set_or_bag_comprehension_binder &) noexcept=default
untyped_set_or_bag_comprehension_binder & operator=(untyped_set_or_bag_comprehension_binder &&) noexcept=default
untyped_set_or_bag_comprehension & operator=(untyped_set_or_bag_comprehension &&) noexcept=default
untyped_set_or_bag_comprehension(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
untyped_set_or_bag_comprehension(const untyped_set_or_bag_comprehension &) noexcept=default
Move semantics.
untyped_set_or_bag_comprehension(untyped_set_or_bag_comprehension &&) noexcept=default
untyped_set_or_bag_comprehension & operator=(const untyped_set_or_bag_comprehension &) noexcept=default
untyped_sort_variable & operator=(const untyped_sort_variable &) noexcept=default
untyped_sort_variable(const untyped_sort_variable &) noexcept=default
Move semantics.
untyped_sort_variable(const atermpp::aterm &term)
untyped_sort_variable & operator=(untyped_sort_variable &&) noexcept=default
untyped_sort_variable(untyped_sort_variable &&) noexcept=default
untyped_sort_variable(std::size_t value)
Constructor.
untyped_sort_variable(const atermpp::aterm_int &value)
\brief Constructor Z14.
untyped_sort_variable()
\brief Default constructor X3.
const atermpp::aterm_int & value() const
\brief Unknown sort expression
untyped_sort & operator=(const untyped_sort &) noexcept=default
untyped_sort(const atermpp::aterm &term)
untyped_sort(const untyped_sort &) noexcept=default
Move semantics.
untyped_sort & operator=(untyped_sort &&) noexcept=default
untyped_sort(untyped_sort &&) noexcept=default
untyped_sort()
\brief Default constructor X3.
\brief A data variable
Definition variable.h:25
variable(const variable &) noexcept=default
Move semantics.
variable(const std::string &name, const sort_expression &sort)
Constructor.
Definition variable.h:66
variable(variable &&) noexcept=default
variable()
Default constructor.
Definition variable.h:46
const core::identifier_string & name() const
Definition variable.h:35
variable & operator=(variable &&) noexcept=default
const sort_expression & sort() const
Definition variable.h:40
variable & operator=(const variable &) noexcept=default
variable(const core::identifier_string &name, const sort_expression &sort)
Constructor.
Definition variable.h:59
variable(const atermpp::aterm &term)
Constructor.
Definition variable.h:52
\brief A where expression
where_clause & operator=(where_clause &&) noexcept=default
const assignment_list & assignments() const
where_clause(const atermpp::aterm &term)
const data_expression & body() const
const assignment_expression_list & declarations() const
where_clause & operator=(const where_clause &) noexcept=default
where_clause()
\brief Default constructor X3.
where_clause(where_clause &&) noexcept=default
where_clause(const data_expression &body, const assignment_expression_list &declarations)
\brief Constructor Z14.
D_ParserTables parser_tables_fsm
D_ParserTables parser_tables_dot
D_ParserTables parser_tables_mcrl2
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:435
const aterm_string & empty_string()
Returns the empty aterm_string.
bool check_term_PREqnSpec(const Term &t)
bool check_term_MapSpec(const Term &t)
bool check_term_PBESTrue(const Term &t)
bool check_term_Seq(const Term &t)
bool check_term_DataVarIdInit(const Term &t)
bool check_rule_DataVarIdInit(const Term &t)
bool check_term_Action(const Term &t)
bool check_term_PRESOr(const Term &t)
bool check_term_SortId(const Term &t)
bool check_term_Sum(const Term &t)
bool check_term_Whr(const Term &t)
bool check_term_ActAt(const Term &t)
bool check_rule_WhrDecl(const Term &t)
bool check_term_StateInfimum(const Term &t)
bool check_term_CommExpr(const Term &t)
bool check_rule_ActSpec(const Term &t)
bool check_term_UntypedSortUnknown(const Term &t)
bool check_term_ActFalse(const Term &t)
bool check_term_ActId(const Term &t)
bool check_term_RegTrans(const Term &t)
bool check_rule_Distribution(const Term &t)
bool check_term_LinearProcessSummand(const Term &t)
bool check_rule_Number(const Term &t)
bool check_term_StateFalse(const Term &t)
bool check_term_argument(const Term &t, CheckFunction f)
bool check_term_UntypedSortVariable(const Term &t)
bool check_rule_ActFrm(const Term &t)
bool check_term_MultAct(const Term &t)
bool check_term_Tau(const Term &t)
bool check_rule_ActId(const Term &t)
bool check_term_UntypedProcessAssignment(const Term &t)
bool check_term_StateDelayTimed(const Term &t)
bool check_term_Delta(const Term &t)
bool check_rule_PBEqn(const Term &t)
bool check_rule_Action(const Term &t)
bool check_term_PRESTrue(const Term &t)
bool check_rule_ActionRenameSpec(const Term &t)
bool check_rule_FixPoint(const Term &t)
bool check_list_argument(const Term &t, CheckFunction f, unsigned int minimum_size)
bool check_rule_DataEqn(const Term &t)
bool check_rule_LinProcSpec(const Term &t)
bool check_term_PRES(const Term &t)
bool check_rule_SortDecl(const Term &t)
bool check_rule_RenameExpr(const Term &t)
bool check_term_ActImp(const Term &t)
bool check_term_Allow(const Term &t)
bool check_term_Choice(const Term &t)
bool check_term_LinProcSpec(const Term &t)
bool check_rule_SortId(const Term &t)
bool check_term_PBESNot(const Term &t)
bool check_term_Sync(const Term &t)
bool check_rule_String(const Term &t)
bool check_term_ActMultAct(const Term &t)
bool check_term_PRESCondEq(const Term &t)
bool check_term_RegTransOrNil(const Term &t)
bool check_term_GlobVarSpec(const Term &t)
bool check_term_StateSupremum(const Term &t)
bool check_term_Mu(const Term &t)
bool check_rule_BindingOperator(const Term &t)
bool check_rule_CommExpr(const Term &t)
bool check_term_UntypedIdentifierAssignment(const Term &t)
bool check_term_RegNil(const Term &t)
bool check_term_DataEqn(const Term &t)
bool check_term_UntypedIdentifier(const Term &t)
bool check_term_StateMust(const Term &t)
bool check_rule_StructProj(const Term &t)
bool check_rule_ConsSpec(const Term &t)
bool check_term_ProcEqnSpec(const Term &t)
bool check_term_LMerge(const Term &t)
bool check_term_ConsSpec(const Term &t)
bool check_rule_SortConsType(const Term &t)
bool check_term_SortSet(const Term &t)
bool check_rule_SortSpec(const Term &t)
bool check_rule_PRES(const Term &t)
bool check_term_Binder(const Term &t)
bool check_term_SortArrow(const Term &t)
bool check_rule_DataExpr(const Term &t)
bool check_term_StateSum(const Term &t)
bool check_term_DataVarId(const Term &t)
bool check_term_UntypedDataParameter(const Term &t)
bool check_term_PRESConstantMultiply(const Term &t)
bool check_term_PBESForall(const Term &t)
bool check_rule_DataEqnSpec(const Term &t)
bool check_term_ActTrue(const Term &t)
bool check_rule_MultActOrDelta(const Term &t)
bool check_rule_LinearProcess(const Term &t)
bool check_term_ProcessInit(const Term &t)
bool check_term_BagComp(const Term &t)
bool check_rule_ProcVarId(const Term &t)
bool check_term_SortFBag(const Term &t)
bool check_rule_PRExpr(const Term &t)
bool check_term_StateYaled(const Term &t)
bool check_term_MultActName(const Term &t)
bool check_term_Nu(const Term &t)
bool check_term_PBESExists(const Term &t)
bool check_term_BInit(const Term &t)
bool check_term_ProcessAssignment(const Term &t)
bool check_term_Lambda(const Term &t)
bool check_term_StateMay(const Term &t)
bool check_term_PRESAnd(const Term &t)
bool check_term_StateVar(const Term &t)
bool check_term_SortRef(const Term &t)
bool check_term_PRESEqInf(const Term &t)
bool check_rule_StateFrm(const Term &t)
bool check_term_ProcSpec(const Term &t)
bool check_term_SortBag(const Term &t)
bool check_term_ProcEqn(const Term &t)
bool check_rule_MultActName(const Term &t)
bool check_term_StatePlus(const Term &t)
bool check_term_TimedMultAct(const Term &t)
bool check_term_PRESInfimum(const Term &t)
bool check_term_Rename(const Term &t)
bool check_rule_MapSpec(const Term &t)
bool check_rule_ProcEqnSpec(const Term &t)
bool check_rule_ProcEqn(const Term &t)
bool check_rule_PREqn(const Term &t)
bool check_term_StateYaledTimed(const Term &t)
bool check_term_StateImp(const Term &t)
bool check_term_StateConstantMultiply(const Term &t)
bool check_rule_DataVarId(const Term &t)
bool check_rule_UntypedIdentifierAssignment(const Term &t)
bool check_term_SortCons(const Term &t)
bool check_term_PRESSupremum(const Term &t)
bool check_term_PropVarInst(const Term &t)
bool check_term_UntypedRegFrm(const Term &t)
bool check_rule_PBES(const Term &t)
bool check_term_IfThen(const Term &t)
bool check_term_ActForall(const Term &t)
bool check_term_StateTrue(const Term &t)
bool check_term_SortSpec(const Term &t)
bool check_term_StateOr(const Term &t)
bool check_term_Forall(const Term &t)
bool check_term_UntypedSetBagComp(const Term &t)
bool check_term_LinearProcess(const Term &t)
bool check_term_PBInit(const Term &t)
bool check_rule_ProcExpr(const Term &t)
bool check_term_Comm(const Term &t)
bool check_term_StateAnd(const Term &t)
bool check_term_PBESOr(const Term &t)
bool check_term_StateMinus(const Term &t)
bool check_term_RenameExpr(const Term &t)
bool check_term_ActExists(const Term &t)
bool check_term_LinearProcessInit(const Term &t)
bool check_rule_SortExpr(const Term &t)
bool check_term_PREqn(const Term &t)
bool check_term_UntypedMultiAction(const Term &t)
bool check_term_PBES(const Term &t)
bool check_rule_GlobVarSpec(const Term &t)
bool check_rule_ActionRenameRuleRHS(const Term &t)
bool check_term_ActAnd(const Term &t)
bool check_rule_DataSpec(const Term &t)
bool check_term_AtTime(const Term &t)
bool check_term_ActSpec(const Term &t)
bool check_term_StateMu(const Term &t)
bool check_rule_LinearProcessSummand(const Term &t)
bool check_rule_StringOrEmpty(const Term &t)
bool check_term_StateNu(const Term &t)
bool check_term_PBEqn(const Term &t)
bool check_term_PRESSum(const Term &t)
bool check_term_ActionRenameSpec(const Term &t)
bool check_term_StateDelay(const Term &t)
bool check_rule_PBEqnSpec(const Term &t)
bool check_term_SortStruct(const Term &t)
bool check_rule_RegFrm(const Term &t)
bool check_rule_ActionRenameRules(const Term &t)
bool check_term_StochasticOperator(const Term &t)
bool check_rule_ProcSpec(const Term &t)
bool check_term_PBESImp(const Term &t)
bool gsIsDataAppl(const atermpp::aterm &Term)
bool check_rule_PropVarDecl(const Term &t)
bool check_term_StateForall(const Term &t)
bool check_term_PRInit(const Term &t)
bool check_term_DataEqnSpec(const Term &t)
bool check_term_StructCons(const Term &t)
bool check_rule_ParamIdOrAction(const Term &t)
bool check_term_ProcVarId(const Term &t)
bool check_term_PRESConstantMultiplyAlt(const Term &t)
bool check_term_DataSpec(const Term &t)
bool check_term_Process(const Term &t)
bool gsIsDataAppl_no_check(const atermpp::aterm &Term)
bool check_term_ActionRenameRule(const Term &t)
bool check_rule_ActionRenameRule(const Term &t)
bool check_rule_PBExpr(const Term &t)
bool check_term_StateNot(const Term &t)
bool check_term_PRESFalse(const Term &t)
bool check_rule_UntypedMultiAction(const Term &t)
bool check_term_OpId(const Term &t)
bool check_term_Distribution(const Term &t)
bool check_term_ActNot(const Term &t)
bool check_term_PRESEqNInf(const Term &t)
bool check_term_UntypedSortsPossible(const Term &t)
bool check_rule_UntypedDataParameter(const Term &t)
bool check_term_Hide(const Term &t)
bool check_rule_PREqnSpec(const Term &t)
bool check_rule_TimedMultAct(const Term &t)
bool check_term_Merge(const Term &t)
bool check_rule_PropVarInst(const Term &t)
bool check_term_Exists(const Term &t)
void foreach_parse_node(const parse_node &x, Function f)
Calls the function f on each node in the parse tree with x as root.
bool check_term_SetComp(const Term &t)
bool check_term_ActOr(const Term &t)
bool check_term_StructProj(const Term &t)
bool check_term_PRESMinus(const Term &t)
bool check_rule_MultAct(const Term &t)
bool check_term_SortList(const Term &t)
bool check_term_PBEqnSpec(const Term &t)
bool check_rule_LinearProcessInit(const Term &t)
bool check_rule_PBInit(const Term &t)
bool check_term_IfThenElse(const Term &t)
bool check_term_PBESAnd(const Term &t)
bool check_rule_ProcInit(const Term &t)
bool check_term_PBESFalse(const Term &t)
bool check_rule_StructCons(const Term &t)
bool check_term_PRESPlus(const Term &t)
bool check_rule_OpId(const Term &t)
bool check_term_PropVarDecl(const Term &t)
bool check_term_SortFSet(const Term &t)
bool check_term_PRESCondSm(const Term &t)
bool check_term_Block(const Term &t)
bool check_term_StateExists(const Term &t)
bool check_term_ActionRenameRules(const Term &t)
bool check_term_StateConstantMultiplyAlt(const Term &t)
bool check_term_DataAppl(const Term &t)
bool check_term_RegSeq(const Term &t)
bool check_term_PRESImp(const Term &t)
bool check_term_RegAlt(const Term &t)
bool check_rule_PRInit(const Term &t)
void warn_left_merge_merge(const parse_node &)
Prints a warning for each occurrence of 'x ||_ y || z' in the parse tree.
apply_builder< Builder > make_apply_builder()
Definition builder.h:103
update_apply_builder_arg1< Builder, Function, Arg1 > make_update_apply_builder_arg1(const Function &f)
Definition builder.h:220
void print_aterm(const T &)
Definition parse.h:248
void print_aterm(const atermpp::aterm &x)
Definition parse.h:254
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
apply_builder_arg1< Builder, Arg1 > make_apply_builder_arg1(const Arg1 &arg1)
Definition builder.h:127
identifier_string parse_identifier(const std::string &text)
Parse an identifier.
Definition parse.h:261
update_apply_builder< Builder, Function > make_update_apply_builder(const Function &f)
Definition builder.h:186
bool is_user_identifier(std::string const &s)
Definition parse.h:272
apply_builder_arg2< Builder, Arg1, Arg2 > make_apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:151
data_expression parse_data_expression(const std::string &text)
Definition data.cpp:217
data_specification parse_data_specification_new(const std::string &text)
Definition data.cpp:228
variable_list parse_variable_declaration_list(const std::string &text)
Definition data.cpp:239
variable_list parse_variables(const std::string &text)
Definition data.cpp:206
sort_expression parse_sort_expression(const std::string &text)
Definition data.cpp:196
A collection of utilities for lazy expression construction.
data_expression implies(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p implies q.
data_expression join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns and applied to the sequence of data expressions [first, last)
data_expression not_(data_expression const &p)
Returns an expression equivalent to not p.
data_expression equal_to(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p == q.
data_expression not_equal_to(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p == q.
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
data_expression or_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p and q.
data_expression join_or(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns or applied to the sequence of data expressions [first, last)
data_expression if_(const data_expression &cond, const data_expression &then, const data_expression &else_)
Returns an expression equivalent to if(cond,then,else_)
Namespace for system defined sort bag.
Definition bag1.h:35
function_symbol fbag2fset(const sort_expression &s)
Constructor for function symbol @fbag2fset.
Definition bag1.h:1471
bool is_bag2set_application(const atermpp::aterm &e)
Recogniser for application of Bag2Set.
Definition bag1.h:747
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition bag1.h:555
void make_bool2nat_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @Bool2Nat_.
Definition bag1.h:1239
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition bag1.h:664
const core::identifier_string & fbag2fset_name()
Generate identifier @fbag2fset.
Definition bag1.h:1461
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bag1.h:1631
bool is_min_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @min_.
Definition bag1.h:1025
function_symbol bag_fbag(const sort_expression &s)
Constructor for function symbol @bagfbag.
Definition bag1.h:172
bool is_min_function_application(const atermpp::aterm &e)
Recogniser for application of @min_.
Definition bag1.h:1061
function_symbol monus_function(const sort_expression &s)
Constructor for function symbol @monus_.
Definition bag1.h:1079
const core::identifier_string & fbag_intersect_name()
Generate identifier @fbag_inter.
Definition bag1.h:1325
void make_bag2set(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Bag2Set.
Definition bag1.h:737
bool is_fbag_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_diff.
Definition bag1.h:1413
bool is_fbag_join_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_join.
Definition bag1.h:1277
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol count.
Definition bag1.h:332
function_symbol_vector bag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for bag.
Definition bag1.h:1525
application zero_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @zero_.
Definition bag1.h:851
const core::identifier_string & bool2nat_function_name()
Generate identifier @Bool2Nat_.
Definition bag1.h:1195
void make_one_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @one_.
Definition bag1.h:923
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition bag1.h:1679
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition bag1.h:685
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:608
const core::identifier_string & set2bag_name()
Generate identifier Set2Bag.
Definition bag1.h:755
bool is_bag_fbag_application(const atermpp::aterm &e)
Recogniser for application of @bagfbag.
Definition bag1.h:216
application fbag2fset(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fbag2fset.
Definition bag1.h:1496
function_symbol_vector bag_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for bag.
Definition bag1.h:1558
void make_add_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @add_.
Definition bag1.h:987
data_equation_vector bag_generate_equations_code(const sort_expression &s)
Give all system defined equations for bag.
Definition bag1.h:1701
bool is_fbag_difference_application(const atermpp::aterm &e)
Recogniser for application of @fbag_diff.
Definition bag1.h:1453
bool is_bag_fbag_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagfbag.
Definition bag1.h:182
const core::identifier_string & zero_function_name()
Generate identifier @zero_.
Definition bag1.h:817
const core::identifier_string & add_function_name()
Generate identifier @add_.
Definition bag1.h:941
application bag2set(const sort_expression &s, const data_expression &arg0)
Application of function symbol Bag2Set.
Definition bag1.h:727
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition bag1.h:385
function_symbol_vector bag_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for bag.
Definition bag1.h:140
bool is_fbag2fset_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag2fset.
Definition bag1.h:1481
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition bag1.h:491
function_symbol bag2set(const sort_expression &s)
Constructor for function symbol Bag2Set.
Definition bag1.h:703
bool is_monus_function_application(const atermpp::aterm &e)
Recogniser for application of @monus_.
Definition bag1.h:1125
const core::identifier_string & nat2bool_function_name()
Generate identifier @Nat2Bool_.
Definition bag1.h:1133
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:507
bool is_zero_function_application(const atermpp::aterm &e)
Recogniser for application of @zero_.
Definition bag1.h:871
const core::identifier_string & fbag_difference_name()
Generate identifier @fbag_diff.
Definition bag1.h:1393
void make_monus_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @monus_.
Definition bag1.h:1115
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function count.
Definition bag1.h:305
function_symbol count(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:294
function_symbol add_function(const sort_expression &s)
Constructor for function symbol @add_.
Definition bag1.h:951
bool is_nat2bool_function_application(const atermpp::aterm &e)
Recogniser for application of @Nat2Bool_.
Definition bag1.h:1187
function_symbol fbag_intersect(const sort_expression &s)
Constructor for function symbol @fbag_inter.
Definition bag1.h:1335
void make_fbag_intersect(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fbag_inter.
Definition bag1.h:1375
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition bag1.h:454
void make_nat2bool_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @Nat2Bool_.
Definition bag1.h:1177
application bag_fbag(const sort_expression &s, const data_expression &arg0)
Application of function symbol @bagfbag.
Definition bag1.h:196
bool is_fbag_intersect_application(const atermpp::aterm &e)
Recogniser for application of @fbag_inter.
Definition bag1.h:1385
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition bag1.h:406
function_symbol fbag_difference(const sort_expression &s)
Constructor for function symbol @fbag_diff.
Definition bag1.h:1403
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition bag1.h:369
application bool2nat_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @Bool2Nat_.
Definition bag1.h:1229
bool is_bag_comprehension_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagcomp.
Definition bag1.h:244
void make_min_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @min_.
Definition bag1.h:1051
data_expression bag_enumeration(const sort_expression &s, data_expression_list const &range)
Application of function symbol bag_enumeration.
const core::identifier_string & min_function_name()
Generate identifier @min_.
Definition bag1.h:1005
bool is_set2bag_function_symbol(const atermpp::aterm &e)
Recogniser for function Set2Bag.
Definition bag1.h:775
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition bag1.h:470
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bag1.h:1619
function_symbol_vector bag_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for bag.
Definition bag1.h:1572
bool is_nat2bool_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Nat2Bool_.
Definition bag1.h:1153
application one_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @one_.
Definition bag1.h:913
const core::identifier_string & monus_function_name()
Generate identifier @monus_.
Definition bag1.h:1069
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition bag1.h:1691
bool is_add_function_application(const atermpp::aterm &e)
Recogniser for application of @add_.
Definition bag1.h:997
void make_fbag2fset(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @fbag2fset.
Definition bag1.h:1507
void make_fbag_join(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fbag_join.
Definition bag1.h:1307
function_symbol min_function(const sort_expression &s)
Constructor for function symbol @min_.
Definition bag1.h:1015
function_symbol set2bag(const sort_expression &s)
Constructor for function symbol Set2Bag.
Definition bag1.h:765
const core::identifier_string & bag_fbag_name()
Generate identifier @bagfbag.
Definition bag1.h:162
const core::identifier_string & bag2set_name()
Generate identifier Bag2Set.
Definition bag1.h:693
const core::identifier_string & intersection_name()
Generate identifier *.
Definition bag1.h:499
application nat2bool_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @Nat2Bool_.
Definition bag1.h:1167
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition bag1.h:396
application constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @bag.
Definition bag1.h:100
application fbag_intersect(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fbag_inter.
Definition bag1.h:1362
function_symbol bag_comprehension(const sort_expression &s)
Constructor for function symbol @bagcomp.
Definition bag1.h:234
bool is_bag2set_function_symbol(const atermpp::aterm &e)
Recogniser for function Bag2Set.
Definition bag1.h:713
implementation_map bag_cpp_implementable_constructors(const sort_expression &)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition bag1.h:153
bool is_bool2nat_function_application(const atermpp::aterm &e)
Recogniser for application of @Bool2Nat_.
Definition bag1.h:1249
const core::identifier_string & fbag_join_name()
Generate identifier @fbag_join.
Definition bag1.h:1257
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition bag1.h:582
function_symbol fbag_join(const sort_expression &s)
Constructor for function symbol @fbag_join.
Definition bag1.h:1267
bool is_constructor_application(const atermpp::aterm &e)
Recogniser for application of @bag.
Definition bag1.h:121
bool is_zero_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @zero_.
Definition bag1.h:837
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @bag.
Definition bag1.h:75
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition bag1.h:1667
const core::identifier_string & constructor_name()
Generate identifier @bag.
Definition bag1.h:65
bool is_bag_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @bagcomp.
Definition bag1.h:278
bool is_set2bag_application(const atermpp::aterm &e)
Recogniser for application of Set2Bag.
Definition bag1.h:809
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:358
void make_zero_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @zero_.
Definition bag1.h:861
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition bag1.h:1655
void make_bag_fbag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @bagfbag.
Definition bag1.h:206
function_symbol bool2nat_function(const sort_expression &s)
Constructor for function symbol @Bool2Nat_.
Definition bag1.h:1205
void make_set2bag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Set2Bag.
Definition bag1.h:799
const core::identifier_string & union_name()
Generate identifier +.
Definition bag1.h:414
bool is_fbag_intersect_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_inter.
Definition bag1.h:1345
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:422
implementation_map bag_cpp_implementable_mappings(const sort_expression &)
Give all system defined mappings that are to be implemented in C++ code for bag.
Definition bag1.h:1608
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition bag1.h:592
void make_bag_comprehension(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @bagcomp.
Definition bag1.h:268
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bag1.h:1643
void make_fbag_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fbag_diff.
Definition bag1.h:1443
const core::identifier_string & count_name()
Generate identifier count.
Definition bag1.h:286
function_symbol nat2bool_function(const sort_expression &s)
Constructor for function symbol @Nat2Bool_.
Definition bag1.h:1143
bool is_one_function_application(const atermpp::aterm &e)
Recogniser for application of @one_.
Definition bag1.h:933
application fbag_difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fbag_diff.
Definition bag1.h:1430
application add_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @add_.
Definition bag1.h:976
const core::identifier_string & difference_name()
Generate identifier -.
Definition bag1.h:600
application set2bag(const sort_expression &s, const data_expression &arg0)
Application of function symbol Set2Bag.
Definition bag1.h:789
bool is_bool2nat_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Bool2Nat_.
Definition bag1.h:1215
bool is_bag(const sort_expression &e)
Recogniser for sort expression Bag(s)
Definition bag1.h:52
application monus_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @monus_.
Definition bag1.h:1104
container_sort bag(const sort_expression &s)
Constructor for sort expression Bag(S)
Definition bag1.h:41
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition bag1.h:648
bool is_fbag2fset_application(const atermpp::aterm &e)
Recogniser for application of @fbag2fset.
Definition bag1.h:1517
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition bag1.h:571
const core::identifier_string & in_name()
Generate identifier in.
Definition bag1.h:350
bool is_constructor_function_symbol(const atermpp::aterm &e)
Recogniser for function @bag.
Definition bag1.h:85
const core::identifier_string & bag_comprehension_name()
Generate identifier @bagcomp.
Definition bag1.h:224
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of count.
Definition bag1.h:342
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition bag1.h:675
application fbag_join(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fbag_join.
Definition bag1.h:1294
const core::identifier_string & one_function_name()
Generate identifier @one_.
Definition bag1.h:879
bool is_add_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @add_.
Definition bag1.h:961
void make_constructor(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @bag.
Definition bag1.h:111
function_symbol zero_function(const sort_expression &s)
Constructor for function symbol @zero_.
Definition bag1.h:827
bool is_one_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @one_.
Definition bag1.h:899
application bag_comprehension(const sort_expression &s, const data_expression &arg0)
Application of function symbol @bagcomp.
Definition bag1.h:258
function_symbol one_function(const sort_expression &s)
Constructor for function symbol @one_.
Definition bag1.h:889
application count(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol count.
Definition bag1.h:321
application min_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @min_.
Definition bag1.h:1040
void make_union(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition bag1.h:481
function_symbol_vector bag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for bag.
Definition bag1.h:129
bool is_fbag_join_application(const atermpp::aterm &e)
Recogniser for application of @fbag_join.
Definition bag1.h:1317
bool is_monus_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @monus_.
Definition bag1.h:1089
Namespace for system defined sort bool_.
Definition bool.h:29
void make_not(data_expression &result, const data_expression &arg0)
Make an application of function symbol !.
Definition bool.h:204
data_equation_vector bool_generate_equations_code()
Give all system defined equations for bool_.
Definition bool.h:499
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
Definition bool.h:116
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bool.h:466
void make_and(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol &&.
Definition bool.h:268
function_symbol_vector bool_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for bool_.
Definition bool.h:439
function_symbol_vector bool_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for bool_.
Definition bool.h:138
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:342
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:51
const core::identifier_string & implies_name()
Generate identifier =>.
Definition bool.h:350
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:41
const core::identifier_string & or_name()
Generate identifier ||.
Definition bool.h:286
implementation_map bool_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition bool.h:151
const function_symbol & implies()
Constructor for function symbol =>.
Definition bool.h:360
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bool.h:490
bool is_not_function_symbol(const atermpp::aterm &e)
Recogniser for function !.
Definition bool.h:180
bool is_implies_application(const atermpp::aterm &e)
Recogniser for application of =>.
Definition bool.h:406
application not_(const data_expression &arg0)
Application of function symbol !.
Definition bool.h:194
bool is_boolean_constant(data_expression const &b)
Determines whether b is a Boolean constant.
const function_symbol & and_()
Constructor for function symbol &&.
Definition bool.h:232
application and_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol &&.
Definition bool.h:257
function_symbol_vector bool_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for bool_.
Definition bool.h:426
const core::identifier_string & not_name()
Generate identifier !.
Definition bool.h:160
application implies(const data_expression &arg0, const data_expression &arg1)
Application of function symbol =>.
Definition bool.h:385
function_symbol_vector bool_generate_constructors_code()
Give all system defined constructors for bool_.
Definition bool.h:127
implementation_map bool_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for bool_.
Definition bool.h:455
application or_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ||.
Definition bool.h:321
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:106
const core::identifier_string & bool_name()
Definition bool.h:32
bool is_and_function_symbol(const atermpp::aterm &e)
Recogniser for function &&.
Definition bool.h:242
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:278
void make_or(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol ||.
Definition bool.h:332
data_expression bool_(bool b)
Constructs expression of type Bool from an integral type.
const function_symbol & or_()
Constructor for function symbol ||.
Definition bool.h:296
bool is_or_function_symbol(const atermpp::aterm &e)
Recogniser for function ||.
Definition bool.h:306
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
Definition bool.h:84
const core::identifier_string & false_name()
Generate identifier false.
Definition bool.h:96
const core::identifier_string & true_name()
Generate identifier true.
Definition bool.h:64
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:214
function_symbol_vector bool_generate_functions_code()
Give all system defined mappings for bool_.
Definition bool.h:413
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:170
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:74
bool is_implies_function_symbol(const atermpp::aterm &e)
Recogniser for function =>.
Definition bool.h:370
void make_implies(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol =>.
Definition bool.h:396
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bool.h:478
const core::identifier_string & and_name()
Generate identifier &&.
Definition bool.h:222
Namespace for system defined sort fbag.
Definition fbag1.h:34
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function {:}.
Definition fbag1.h:84
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol count.
Definition fbag1.h:375
const core::identifier_string & count_all_name()
Generate identifier #.
Definition fbag1.h:711
function_symbol_vector fbag_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for fbag.
Definition fbag1.h:855
implementation_map fbag_cpp_implementable_constructors(const sort_expression &)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition fbag1.h:188
const core::identifier_string & fset2fbag_name()
Generate identifier @fset2fbag.
Definition fbag1.h:457
application fset2fbag(const sort_expression &s, const data_expression &arg0)
Application of function symbol @fset2fbag.
Definition fbag1.h:491
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
Definition fbag1.h:40
application pick(const sort_expression &s, const data_expression &arg0)
Application of function symbol pick.
Definition fbag1.h:807
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition fbag1.h:554
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition fbag1.h:413
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition fbag1.h:667
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition fbag1.h:618
function_symbol pick(const sort_expression &s)
Constructor for function symbol pick.
Definition fbag1.h:783
const core::identifier_string & count_name()
Generate identifier count.
Definition fbag1.h:329
const core::identifier_string & cinsert_name()
Generate identifier @fbag_cinsert.
Definition fbag1.h:263
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition fbag1.h:575
function_symbol intersection(const sort_expression &s)
Constructor for function symbol *.
Definition fbag1.h:593
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition fbag1.h:927
function_symbol union_(const sort_expression &s)
Constructor for function symbol +.
Definition fbag1.h:529
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition fbag1.h:963
bool is_cinsert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_cinsert.
Definition fbag1.h:283
function_symbol cons_(const sort_expression &s)
Constructor for function symbol @fbag_cons.
Definition fbag1.h:207
bool is_insert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_insert.
Definition fbag1.h:116
implementation_map fbag_cpp_implementable_mappings(const sort_expression &)
Give all system defined mappings that are to be implemented in C++ code for fbag.
Definition fbag1.h:892
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition fbag1.h:639
function_symbol count_all(const sort_expression &s)
Constructor for function symbol #.
Definition fbag1.h:721
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition fbag1.h:629
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_cons.
Definition fbag1.h:217
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition fbag1.h:428
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fbag_insert.
Definition fbag1.h:106
application insert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fbag_insert.
Definition fbag1.h:132
void make_fset2fbag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @fset2fbag.
Definition fbag1.h:501
void make_union(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition fbag1.h:565
const core::identifier_string & cons_name()
Generate identifier @fbag_cons.
Definition fbag1.h:197
application cinsert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fbag_cinsert.
Definition fbag1.h:299
bool is_fset2fbag_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset2fbag.
Definition fbag1.h:477
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition fbag1.h:449
const core::identifier_string & empty_name()
Generate identifier {:}.
Definition fbag1.h:64
const core::identifier_string & difference_name()
Generate identifier -.
Definition fbag1.h:647
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition fbag1.h:703
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of count.
Definition fbag1.h:385
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of @fbag_cons.
Definition fbag1.h:255
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition fbag1.h:439
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition fbag1.h:939
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition fbag1.h:915
void make_count_all(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
Definition fbag1.h:755
bool is_pick_function_symbol(const atermpp::aterm &e)
Recogniser for function pick.
Definition fbag1.h:793
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function count.
Definition fbag1.h:349
application count_all(const sort_expression &s, const data_expression &arg0)
Application of function symbol #.
Definition fbag1.h:745
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition fbag1.h:603
application cons_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fbag_cons.
Definition fbag1.h:233
const core::identifier_string & intersection_name()
Generate identifier *.
Definition fbag1.h:583
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition fbag1.h:951
bool is_pick_application(const atermpp::aterm &e)
Recogniser for application of pick.
Definition fbag1.h:827
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition fbag1.h:403
function_symbol_vector fbag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fbag.
Definition fbag1.h:162
bool is_count_all_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition fbag1.h:765
function_symbol count(const sort_expression &s)
Constructor for function symbol count.
Definition fbag1.h:339
bool is_fbag(const sort_expression &e)
Recogniser for sort expression FBag(s)
Definition fbag1.h:51
void make_cinsert(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @fbag_cinsert.
Definition fbag1.h:311
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition fbag1.h:682
function_symbol empty(const sort_expression &s)
Constructor for function symbol {:}.
Definition fbag1.h:74
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition fbag1.h:693
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fbag_cinsert.
Definition fbag1.h:273
bool is_cinsert_application(const atermpp::aterm &e)
Recogniser for application of @fbag_cinsert.
Definition fbag1.h:321
void make_insert(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @fbag_insert.
Definition fbag1.h:144
bool is_fset2fbag_application(const atermpp::aterm &e)
Recogniser for application of @fset2fbag.
Definition fbag1.h:511
bool is_count_all_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
Definition fbag1.h:731
function_symbol_vector fbag_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for fbag.
Definition fbag1.h:869
void make_cons(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @fbag_cons.
Definition fbag1.h:245
function_symbol fset2fbag(const sort_expression &s)
Constructor for function symbol @fset2fbag.
Definition fbag1.h:467
const core::identifier_string & pick_name()
Generate identifier pick.
Definition fbag1.h:773
const core::identifier_string & union_name()
Generate identifier +.
Definition fbag1.h:519
application count(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol count.
Definition fbag1.h:364
function_symbol difference(const sort_expression &s)
Constructor for function symbol -.
Definition fbag1.h:657
function_symbol_vector fbag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fbag.
Definition fbag1.h:835
bool is_insert_application(const atermpp::aterm &e)
Recogniser for application of @fbag_insert.
Definition fbag1.h:154
const core::identifier_string & insert_name()
Generate identifier @fbag_insert.
Definition fbag1.h:96
data_equation_vector fbag_generate_equations_code(const sort_expression &s)
Give all system defined equations for fbag.
Definition fbag1.h:973
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition fbag1.h:539
void make_pick(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol pick.
Definition fbag1.h:817
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition fbag1.h:903
function_symbol_vector fbag_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for fbag.
Definition fbag1.h:174
const core::identifier_string & in_name()
Generate identifier in.
Definition fbag1.h:393
Namespace for system defined sort fset.
Definition fset1.h:32
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fset_insert.
Definition fset1.h:104
bool is_fset(const sort_expression &e)
Recogniser for sort expression FSet(s)
Definition fset1.h:49
function_symbol_vector fset_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for fset.
Definition fset1.h:735
void make_pick(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol pick.
Definition fset1.h:685
const core::identifier_string & pick_name()
Generate identifier pick.
Definition fset1.h:641
application count(const sort_expression &s, const data_expression &arg0)
Application of function symbol #.
Definition fset1.h:613
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function {}.
Definition fset1.h:82
application insert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fset_insert.
Definition fset1.h:129
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition fset1.h:379
bool is_cinsert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_cinsert.
Definition fset1.h:277
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
Definition fset1.h:599
void make_cons(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @fset_cons.
Definition fset1.h:239
function_symbol_vector fset_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for fset.
Definition fset1.h:721
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fset_cinsert.
Definition fset1.h:267
function_symbol_vector fset_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for fset.
Definition fset1.h:170
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_cons.
Definition fset1.h:213
function_symbol_vector fset_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fset.
Definition fset1.h:158
const core::identifier_string & empty_name()
Generate identifier {}.
Definition fset1.h:62
const core::identifier_string & intersection_name()
Generate identifier *.
Definition fset1.h:515
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition fset1.h:358
bool is_insert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_insert.
Definition fset1.h:114
function_symbol_vector fset_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fset.
Definition fset1.h:703
application cons_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fset_cons.
Definition fset1.h:228
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition fset1.h:407
function_symbol cons_(const sort_expression &s)
Constructor for function symbol @fset_cons.
Definition fset1.h:203
void make_union(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition fset1.h:497
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition fset1.h:561
implementation_map fset_cpp_implementable_mappings(const sort_expression &)
Give all system defined mappings that are to be implemented in C++ code for fset.
Definition fset1.h:756
function_symbol empty(const sort_expression &s)
Constructor for function symbol {}.
Definition fset1.h:72
const core::identifier_string & difference_name()
Generate identifier -.
Definition fset1.h:387
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition fset1.h:471
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition fset1.h:433
function_symbol intersection(const sort_expression &s)
Constructor for function symbol *.
Definition fset1.h:525
void make_cinsert(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @fset_cinsert.
Definition fset1.h:305
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition fset1.h:779
function_symbol difference(const sort_expression &s)
Constructor for function symbol -.
Definition fset1.h:397
void make_insert(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @fset_insert.
Definition fset1.h:140
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition fset1.h:535
const core::identifier_string & cinsert_name()
Generate identifier @fset_cinsert.
Definition fset1.h:257
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition fset1.h:343
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
Definition fset1.h:623
bool is_pick_application(const atermpp::aterm &e)
Recogniser for application of pick.
Definition fset1.h:695
implementation_map fset_cpp_implementable_constructors(const sort_expression &)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition fset1.h:184
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition fset1.h:767
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition fset1.h:333
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition fset1.h:443
const core::identifier_string & count_name()
Generate identifier #.
Definition fset1.h:579
bool is_pick_function_symbol(const atermpp::aterm &e)
Recogniser for function pick.
Definition fset1.h:661
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition fset1.h:803
data_equation_vector fset_generate_equations_code(const sort_expression &s)
Give all system defined equations for fset.
Definition fset1.h:837
const core::identifier_string & union_name()
Generate identifier +.
Definition fset1.h:451
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition fset1.h:791
function_symbol pick(const sort_expression &s)
Constructor for function symbol pick.
Definition fset1.h:651
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition fset1.h:369
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition fset1.h:815
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition fset1.h:633
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition fset1.h:589
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of @fset_cons.
Definition fset1.h:249
application cinsert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fset_cinsert.
Definition fset1.h:293
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition fset1.h:571
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition fset1.h:422
const core::identifier_string & insert_name()
Generate identifier @fset_insert.
Definition fset1.h:94
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset1.h:38
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition fset1.h:486
const core::identifier_string & cons_name()
Generate identifier @fset_cons.
Definition fset1.h:193
application pick(const sort_expression &s, const data_expression &arg0)
Application of function symbol pick.
Definition fset1.h:675
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition fset1.h:827
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition fset1.h:550
function_symbol union_(const sort_expression &s)
Constructor for function symbol +.
Definition fset1.h:461
const core::identifier_string & in_name()
Generate identifier in.
Definition fset1.h:323
bool is_cinsert_application(const atermpp::aterm &e)
Recogniser for application of @fset_cinsert.
Definition fset1.h:315
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition fset1.h:507
bool is_insert_application(const atermpp::aterm &e)
Recogniser for application of @fset_insert.
Definition fset1.h:150
Namespace for system defined sort int_.
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition int1.h:649
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition int1.h:1513
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition int1.h:639
const core::identifier_string & cint_name()
Generate identifier @cInt.
Definition int1.h:67
application cint(const data_expression &arg0)
Application of function symbol @cInt.
Definition int1.h:101
application abs(const data_expression &arg0)
Application of function symbol abs.
Definition int1.h:691
application nat2int(const data_expression &arg0)
Application of function symbol Nat2Int.
Definition int1.h:257
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition int1.h:832
application cneg(const data_expression &arg0)
Application of function symbol @cNeg.
Definition int1.h:163
bool is_minus_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition int1.h:1047
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition int1.h:568
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition int1.h:817
const core::identifier_string & abs_name()
Generate identifier abs.
Definition int1.h:657
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition int1.h:612
bool is_int2pos_application(const atermpp::aterm &e)
Recogniser for application of Int2Pos.
Definition int1.h:463
const core::identifier_string & pred_name()
Generate identifier pred.
Definition int1.h:860
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition int1.h:1350
bool is_int2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Pos.
Definition int1.h:429
const function_symbol & pos2int()
Constructor for function symbol Pos2Int.
Definition int1.h:357
const core::identifier_string & nat2int_name()
Generate identifier Nat2Int.
Definition int1.h:223
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition int1.h:1489
void make_minus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition int1.h:1074
application negate(const data_expression &arg0)
Application of function symbol -.
Definition int1.h:753
bool is_cneg_function_symbol(const atermpp::aterm &e)
Recogniser for function @cNeg.
Definition int1.h:149
const core::identifier_string & int2pos_name()
Generate identifier Int2Pos.
Definition int1.h:409
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:479
void make_cneg(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cNeg.
Definition int1.h:173
application int2nat(const data_expression &arg0)
Application of function symbol Int2Nat.
Definition int1.h:319
function_symbol pred(const sort_expression &s0)
Definition int1.h:868
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition int1.h:999
const core::identifier_string & cneg_name()
Generate identifier @cNeg.
Definition int1.h:129
const core::identifier_string & exp_name()
Generate identifier exp.
Definition int1.h:1314
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition int1.h:1377
const core::identifier_string & minimum_name()
Generate identifier min.
Definition int1.h:576
bool is_mod_application(const atermpp::aterm &e)
Recogniser for application of mod.
Definition int1.h:1306
const core::identifier_string & int_name()
Definition int1.h:35
bool is_mod_function_symbol(const atermpp::aterm &e)
Recogniser for function mod.
Definition int1.h:1269
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition int1.h:547
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition int1.h:1144
function_symbol_vector int_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for int_.
Definition int1.h:1441
const core::identifier_string & pos2int_name()
Generate identifier Pos2Int.
Definition int1.h:347
const function_symbol & int2nat()
Constructor for function symbol Int2Nat.
Definition int1.h:295
bool is_int(const sort_expression &e)
Recogniser for sort expression Int.
Definition int1.h:54
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1036
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition int1.h:931
const function_symbol & nat2int()
Constructor for function symbol Nat2Int.
Definition int1.h:233
application div(const data_expression &arg0, const data_expression &arg1)
Application of function symbol div.
Definition int1.h:1221
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition int1.h:1165
const core::identifier_string & maximum_name()
Generate identifier max.
Definition int1.h:471
bool is_int2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Nat.
Definition int1.h:305
bool is_cneg_application(const atermpp::aterm &e)
Recogniser for application of @cNeg.
Definition int1.h:183
const core::identifier_string & succ_name()
Generate identifier succ.
Definition int1.h:781
const function_symbol & cneg()
Constructor for function symbol @cNeg.
Definition int1.h:139
void make_pos2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Int.
Definition int1.h:391
const function_symbol & abs()
Constructor for function symbol abs.
Definition int1.h:667
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1322
bool is_cint_application(const atermpp::aterm &e)
Recogniser for application of @cInt.
Definition int1.h:121
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition int1.h:1128
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition int1.h:1020
const core::identifier_string & mod_name()
Generate identifier mod.
Definition int1.h:1250
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition int1.h:1010
data_equation_vector int_generate_equations_code()
Give all system defined equations for int_.
Definition int1.h:1522
application minus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition int1.h:1063
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:947
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition int1.h:628
const function_symbol & int2pos()
Constructor for function symbol Int2Pos.
Definition int1.h:419
bool is_integer_constant(const data_expression &n)
Determines whether n is an integer constant.
const core::identifier_string & plus_name()
Generate identifier +.
Definition int1.h:939
function_symbol_vector int_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for int_.
Definition int1.h:1428
void make_div(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol div.
Definition int1.h:1232
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition int1.h:773
function_symbol negate(const sort_expression &s0)
Definition int1.h:727
bool is_div_application(const atermpp::aterm &e)
Recogniser for application of div.
Definition int1.h:1242
void make_mod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol mod.
Definition int1.h:1296
bool is_pos2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Int.
Definition int1.h:367
function_symbol_vector int_generate_constructors_code()
Give all system defined constructors for int_.
Definition int1.h:190
bool is_abs_application(const atermpp::aterm &e)
Recogniser for application of abs.
Definition int1.h:711
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition int1.h:558
function_symbol_vector int_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for int_.
Definition int1.h:201
application int2pos(const data_expression &arg0)
Application of function symbol Int2Pos.
Definition int1.h:443
function_symbol succ(const sort_expression &s0)
Definition int1.h:789
void make_negate(data_expression &result, const data_expression &arg0)
Make an application of function symbol -.
Definition int1.h:763
const core::identifier_string & negate_name()
Generate identifier -.
Definition int1.h:719
bool is_cint_function_symbol(const atermpp::aterm &e)
Recogniser for function @cInt.
Definition int1.h:87
std::string integer_constant_as_string(const data_expression &n)
Return the string representation of an integer number.
void make_abs(data_expression &result, const data_expression &arg0)
Make an application of function symbol abs.
Definition int1.h:701
function_symbol_vector int_generate_functions_code()
Give all system defined mappings for int_.
Definition int1.h:1394
data_expression int_(const std::string &n)
Constructs expression of type Int from a string.
implementation_map int_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition int1.h:214
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition int1.h:1387
application mod(const data_expression &arg0, const data_expression &arg1)
Application of function symbol mod.
Definition int1.h:1285
void make_nat2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Int.
Definition int1.h:267
const function_symbol & cint()
Constructor for function symbol @cInt.
Definition int1.h:77
implementation_map int_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for int_.
Definition int1.h:1478
application pos2int(const data_expression &arg0)
Application of function symbol Pos2Int.
Definition int1.h:381
bool is_nat2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Int.
Definition int1.h:243
bool is_int2nat_application(const atermpp::aterm &e)
Recogniser for application of Int2Nat.
Definition int1.h:339
const core::identifier_string & minus_name()
Generate identifier -.
Definition int1.h:1028
data_expression int_(T t)
Constructs expression of type pos from an integral type.
function_symbol mod(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1258
const core::identifier_string & int2nat_name()
Generate identifier Int2Nat.
Definition int1.h:285
const core::identifier_string & div_name()
Generate identifier div.
Definition int1.h:1173
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition int1.h:531
application exp(const data_expression &arg0, const data_expression &arg1)
Application of function symbol exp.
Definition int1.h:1366
bool is_div_function_symbol(const atermpp::aterm &e)
Recogniser for function div.
Definition int1.h:1205
application pred(const data_expression &arg0)
Application of function symbol pred.
Definition int1.h:911
bool is_negate_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition int1.h:738
void make_int2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Pos.
Definition int1.h:453
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1100
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition int1.h:983
bool is_nat2int_application(const atermpp::aterm &e)
Recogniser for application of Nat2Int.
Definition int1.h:277
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition int1.h:1084
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition int1.h:1155
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:584
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition int1.h:896
function_symbol div(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1181
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition int1.h:842
bool is_pos2int_application(const atermpp::aterm &e)
Recogniser for application of Pos2Int.
Definition int1.h:401
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition int1.h:921
void make_cint(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cInt.
Definition int1.h:111
void make_int2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Nat.
Definition int1.h:329
bool is_abs_function_symbol(const atermpp::aterm &e)
Recogniser for function abs.
Definition int1.h:677
const core::identifier_string & times_name()
Generate identifier *.
Definition int1.h:1092
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition int1.h:1501
NUMERIC_VALUE integer_constant_to_value(const data_expression &n)
Return the NUMERIC_VALUE representation of an integer number.
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition int1.h:852
const basic_sort & int_()
Constructor for sort expression Int.
Definition int1.h:44
Namespace for system defined sort list.
Definition list1.h:33
container_sort list(const sort_expression &s)
Constructor for sort expression List(S)
Definition list1.h:39
data_expression list_enumeration(const sort_expression &s, data_expression_list const &range)
Application of function symbol list_enumeration.
Namespace for system defined sort nat.
const core::identifier_string & succ_name()
Generate identifier succ.
Definition nat1.h:573
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition nat1.h:2316
application cpair(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cPair.
Definition nat1.h:224
bool is_cpair_application(const atermpp::aterm &e)
Recogniser for application of @cPair.
Definition nat1.h:245
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition nat1.h:952
const function_symbol & generalised_divmod()
Constructor for function symbol @gdivmod.
Definition nat1.h:2036
bool is_natpred_function_symbol(const atermpp::aterm &e)
Recogniser for function @natpred.
Definition nat1.h:717
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:419
const core::identifier_string & sqrt_nat_aux_func_name()
Generate identifier @sqrt_nat.
Definition nat1.h:1772
bool is_pos2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Nat.
Definition nat1.h:307
function_symbol succ(const sort_expression &s0)
Definition nat1.h:581
const function_symbol & monus()
Constructor for function symbol @monus.
Definition nat1.h:1388
void make_sqrt(data_expression &result, const data_expression &arg0)
Make an application of function symbol sqrt.
Definition nat1.h:1754
void make_generalised_divmod(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @gdivmod.
Definition nat1.h:2074
const function_symbol & c0()
Constructor for function symbol @c0.
Definition nat1.h:105
bool is_swap_zero_add_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero_add.
Definition nat1.h:1566
void make_dub(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @dub.
Definition nat1.h:805
void make_div(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol div.
Definition nat1.h:1157
application sqrt_nat_aux_func(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @sqrt_nat.
Definition nat1.h:1808
const core::identifier_string & maximum_name()
Generate identifier max.
Definition nat1.h:411
void make_mod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol mod.
Definition nat1.h:1221
application generalised_divmod(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @gdivmod.
Definition nat1.h:2062
bool is_swap_zero_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero.
Definition nat1.h:1462
bool is_cnat_application(const atermpp::aterm &e)
Recogniser for application of @cNat.
Definition nat1.h:181
const core::identifier_string & mod_name()
Generate identifier mod.
Definition nat1.h:1175
bool is_generalised_divmod_application(const atermpp::aterm &e)
Recogniser for application of @gdivmod.
Definition nat1.h:2084
bool is_div_application(const atermpp::aterm &e)
Recogniser for application of div.
Definition nat1.h:1167
void make_doubly_generalised_divmod(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @ggdivmod.
Definition nat1.h:2140
const core::identifier_string & swap_zero_min_name()
Generate identifier @swap_zero_min.
Definition nat1.h:1574
const function_symbol & divmod()
Constructor for function symbol @divmod.
Definition nat1.h:1972
bool is_pos2nat_application(const atermpp::aterm &e)
Recogniser for application of Pos2Nat.
Definition nat1.h:341
const function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat1.h:137
application dubsucc(const data_expression &arg0)
Application of function symbol @dubsucc.
Definition nat1.h:857
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition nat1.h:679
bool is_nat2pos_application(const atermpp::aterm &e)
Recogniser for application of Nat2Pos.
Definition nat1.h:403
bool is_mod_function_symbol(const atermpp::aterm &e)
Recogniser for function mod.
Definition nat1.h:1195
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:1247
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition nat1.h:544
const core::identifier_string & times_name()
Generate identifier *.
Definition nat1.h:1034
const function_symbol & dubsucc()
Constructor for function symbol @dubsucc.
Definition nat1.h:833
const function_symbol & swap_zero_add()
Constructor for function symbol @swap_zero_add.
Definition nat1.h:1516
function_symbol_vector nat_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for nat.
Definition nat1.h:2212
data_equation_vector nat_generate_equations_code()
Give all system defined equations for nat.
Definition nat1.h:2349
const function_symbol & cpair()
Constructor for function symbol @cPair.
Definition nat1.h:199
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:43
const core::identifier_string & nat_name()
Definition nat1.h:34
const function_symbol & monus_on_pos()
Constructor for function symbol @monuspos.
Definition nat1.h:980
application exp(const data_expression &arg0, const data_expression &arg1)
Application of function symbol exp.
Definition nat1.h:1287
const core::identifier_string & exp_name()
Generate identifier exp.
Definition nat1.h:1239
const function_symbol & swap_zero()
Constructor for function symbol @swap_zero.
Definition nat1.h:1452
application swap_zero(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @swap_zero.
Definition nat1.h:1477
bool is_first_function_symbol(const atermpp::aterm &e)
Recogniser for function @first.
Definition nat1.h:1858
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition nat1.h:488
void make_cpair(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cPair.
Definition nat1.h:235
implementation_map nat_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition nat1.h:278
bool is_nat(const sort_expression &e)
Recogniser for sort expression Nat.
Definition nat1.h:53
bool is_doubly_generalised_divmod_function_symbol(const atermpp::aterm &e)
Recogniser for function @ggdivmod.
Definition nat1.h:2112
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition nat1.h:925
function_symbol_vector nat_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for nat.
Definition nat1.h:2199
std::string natural_constant_as_string(const data_expression &n_in)
Return the string representation of a natural number.
application sqrt(const data_expression &arg0)
Application of function symbol sqrt.
Definition nat1.h:1744
application pos2nat(const data_expression &arg0)
Application of function symbol Pos2Nat.
Definition nat1.h:321
void make_nat2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Pos.
Definition nat1.h:393
application first(const data_expression &arg0)
Application of function symbol @first.
Definition nat1.h:1872
const core::identifier_string & plus_name()
Generate identifier +.
Definition nat1.h:885
const core::identifier_string & natpair_name()
Definition nat1.h:63
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition nat1.h:2304
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition nat1.h:592
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition nat1.h:478
const core::identifier_string & div_name()
Generate identifier div.
Definition nat1.h:1111
bool is_monus_on_pos_application(const atermpp::aterm &e)
Recogniser for application of @monuspos.
Definition nat1.h:1026
const function_symbol & mod()
Constructor for function symbol mod.
Definition nat1.h:1185
void make_monus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @monus.
Definition nat1.h:1424
const function_symbol & sqrt()
Constructor for function symbol sqrt.
Definition nat1.h:1720
void make_dubsucc(data_expression &result, const data_expression &arg0)
Make an application of function symbol @dubsucc.
Definition nat1.h:867
application even(const data_expression &arg0)
Application of function symbol @even.
Definition nat1.h:1350
const function_symbol & doubly_generalised_divmod()
Constructor for function symbol @ggdivmod.
Definition nat1.h:2102
const function_symbol & pred()
Constructor for function symbol pred.
Definition nat1.h:645
void make_even(data_expression &result, const data_expression &arg0)
Make an application of function symbol @even.
Definition nat1.h:1360
bool is_sqrt_nat_aux_func_function_symbol(const atermpp::aterm &e)
Recogniser for function @sqrt_nat.
Definition nat1.h:1792
const function_symbol & even()
Constructor for function symbol @even.
Definition nat1.h:1326
const core::identifier_string & first_name()
Generate identifier @first.
Definition nat1.h:1838
void make_swap_zero_monus(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @swap_zero_monus.
Definition nat1.h:1692
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition nat1.h:627
bool is_dub_function_symbol(const atermpp::aterm &e)
Recogniser for function @dub.
Definition nat1.h:779
application cnat(const data_expression &arg0)
Application of function symbol @cNat.
Definition nat1.h:161
const function_symbol & natpred()
Constructor for function symbol @natpred.
Definition nat1.h:707
bool is_swap_zero_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero.
Definition nat1.h:1498
const core::identifier_string & even_name()
Generate identifier @even.
Definition nat1.h:1316
const core::identifier_string & swap_zero_name()
Generate identifier @swap_zero.
Definition nat1.h:1442
void make_pos2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Nat.
Definition nat1.h:331
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition nat1.h:565
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition nat1.h:1271
bool is_monus_function_symbol(const atermpp::aterm &e)
Recogniser for function @monus.
Definition nat1.h:1398
bool is_mod_application(const atermpp::aterm &e)
Recogniser for application of mod.
Definition nat1.h:1231
bool is_even_function_symbol(const atermpp::aterm &e)
Recogniser for function @even.
Definition nat1.h:1336
const core::identifier_string & pred_name()
Generate identifier pred.
Definition nat1.h:635
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition nat1.h:1308
const function_symbol & swap_zero_min()
Constructor for function symbol @swap_zero_min.
Definition nat1.h:1584
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:504
const function_symbol & sqrt_nat_aux_func()
Constructor for function symbol @sqrt_nat.
Definition nat1.h:1782
bool is_last_application(const atermpp::aterm &e)
Recogniser for application of @last.
Definition nat1.h:1954
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition nat1.h:1298
const function_symbol & div()
Constructor for function symbol div.
Definition nat1.h:1121
application last(const data_expression &arg0)
Application of function symbol @last.
Definition nat1.h:1934
const core::identifier_string & doubly_generalised_divmod_name()
Generate identifier @ggdivmod.
Definition nat1.h:2092
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition nat1.h:617
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition nat1.h:451
bool is_swap_zero_min_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero_min.
Definition nat1.h:1634
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:893
const core::identifier_string & dubsucc_name()
Generate identifier @dubsucc.
Definition nat1.h:823
bool is_first_application(const atermpp::aterm &e)
Recogniser for application of @first.
Definition nat1.h:1892
bool is_sqrt_application(const atermpp::aterm &e)
Recogniser for application of sqrt.
Definition nat1.h:1764
const function_symbol & first()
Constructor for function symbol @first.
Definition nat1.h:1848
void make_first(data_expression &result, const data_expression &arg0)
Make an application of function symbol @first.
Definition nat1.h:1882
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition nat1.h:655
bool is_generalised_divmod_function_symbol(const atermpp::aterm &e)
Recogniser for function @gdivmod.
Definition nat1.h:2046
application swap_zero_add(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @swap_zero_add.
Definition nat1.h:1543
void make_swap_zero_add(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @swap_zero_add.
Definition nat1.h:1556
const core::identifier_string & swap_zero_monus_name()
Generate identifier @swap_zero_monus.
Definition nat1.h:1642
function_symbol_vector nat_generate_functions_code()
Give all system defined mappings for nat.
Definition nat1.h:2157
bool is_cpair_function_symbol(const atermpp::aterm &e)
Recogniser for function @cPair.
Definition nat1.h:209
application div(const data_expression &arg0, const data_expression &arg1)
Application of function symbol div.
Definition nat1.h:1146
bool is_divmod_function_symbol(const atermpp::aterm &e)
Recogniser for function @divmod.
Definition nat1.h:1982
const function_symbol & swap_zero_monus()
Constructor for function symbol @swap_zero_monus.
Definition nat1.h:1652
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition nat1.h:1093
application swap_zero_min(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @swap_zero_min.
Definition nat1.h:1611
bool is_c0_function_symbol(const atermpp::aterm &e)
Recogniser for function @c0.
Definition nat1.h:115
const core::identifier_string & generalised_divmod_name()
Generate identifier @gdivmod.
Definition nat1.h:2026
application doubly_generalised_divmod(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @ggdivmod.
Definition nat1.h:2128
const function_symbol & nat2pos()
Constructor for function symbol Nat2Pos.
Definition nat1.h:359
const core::identifier_string & monus_name()
Generate identifier @monus.
Definition nat1.h:1378
application monus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @monus.
Definition nat1.h:1413
const core::identifier_string & cpair_name()
Generate identifier @cPair.
Definition nat1.h:189
const core::identifier_string & nat2pos_name()
Generate identifier Nat2Pos.
Definition nat1.h:349
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition nat1.h:2328
void make_divmod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @divmod.
Definition nat1.h:2008
application dub(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @dub.
Definition nat1.h:794
implementation_map nat_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for nat.
Definition nat1.h:2257
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition nat1.h:2292
const basic_sort & natpair()
Constructor for sort expression @NatPair.
Definition nat1.h:72
application pred(const data_expression &arg0)
Application of function symbol pred.
Definition nat1.h:669
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition nat1.h:607
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition nat1.h:2280
bool is_swap_zero_monus_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero_monus.
Definition nat1.h:1702
void make_swap_zero_min(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @swap_zero_min.
Definition nat1.h:1624
const core::identifier_string & dub_name()
Generate identifier @dub.
Definition nat1.h:759
const core::identifier_string & cnat_name()
Generate identifier @cNat.
Definition nat1.h:127
const core::identifier_string & c0_name()
Generate identifier @c0.
Definition nat1.h:95
application natpred(const data_expression &arg0)
Application of function symbol @natpred.
Definition nat1.h:731
application divmod(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @divmod.
Definition nat1.h:1997
bool is_swap_zero_add_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero_add.
Definition nat1.h:1526
bool is_natpair(const sort_expression &e)
Recogniser for sort expression @NatPair.
Definition nat1.h:82
bool is_swap_zero_monus_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero_monus.
Definition nat1.h:1662
const core::identifier_string & pos2nat_name()
Generate identifier Pos2Nat.
Definition nat1.h:287
const core::identifier_string & last_name()
Generate identifier @last.
Definition nat1.h:1900
const core::identifier_string & minimum_name()
Generate identifier min.
Definition nat1.h:496
void make_sqrt_nat_aux_func(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @sqrt_nat.
Definition nat1.h:1820
bool is_sqrt_nat_aux_func_application(const atermpp::aterm &e)
Recogniser for application of @sqrt_nat.
Definition nat1.h:1830
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition nat1.h:2268
bool is_sqrt_function_symbol(const atermpp::aterm &e)
Recogniser for function sqrt.
Definition nat1.h:1730
application mod(const data_expression &arg0, const data_expression &arg1)
Application of function symbol mod.
Definition nat1.h:1210
bool is_cnat_function_symbol(const atermpp::aterm &e)
Recogniser for function @cNat.
Definition nat1.h:147
NUMERIC_TYPE natural_constant_to_value(const data_expression &n)
Return the NUMERIC_VALUE representation of a natural number.
void make_monus_on_pos(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @monuspos.
Definition nat1.h:1016
function_symbol_vector nat_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for nat.
Definition nat1.h:264
const function_symbol & last()
Constructor for function symbol @last.
Definition nat1.h:1910
const core::identifier_string & monus_on_pos_name()
Generate identifier @monuspos.
Definition nat1.h:970
bool is_natpred_application(const atermpp::aterm &e)
Recogniser for application of @natpred.
Definition nat1.h:751
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition nat1.h:689
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition nat1.h:962
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition nat1.h:467
data_expression nat(T t)
Constructs expression of type pos from an integral type.
bool is_monus_on_pos_function_symbol(const atermpp::aterm &e)
Recogniser for function @monuspos.
Definition nat1.h:990
void make_swap_zero(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @swap_zero.
Definition nat1.h:1488
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition nat1.h:555
const core::identifier_string & swap_zero_add_name()
Generate identifier @swap_zero_add.
Definition nat1.h:1506
bool is_dubsucc_function_symbol(const atermpp::aterm &e)
Recogniser for function @dubsucc.
Definition nat1.h:843
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition nat1.h:941
bool is_dubsucc_application(const atermpp::aterm &e)
Recogniser for application of @dubsucc.
Definition nat1.h:877
bool is_swap_zero_min_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero_min.
Definition nat1.h:1594
function_symbol_vector nat_generate_constructors_code()
Give all system defined constructors for nat.
Definition nat1.h:252
const core::identifier_string & sqrt_name()
Generate identifier sqrt.
Definition nat1.h:1710
bool is_doubly_generalised_divmod_application(const atermpp::aterm &e)
Recogniser for application of @ggdivmod.
Definition nat1.h:2150
application monus_on_pos(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @monuspos.
Definition nat1.h:1005
bool is_last_function_symbol(const atermpp::aterm &e)
Recogniser for function @last.
Definition nat1.h:1920
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition nat1.h:1082
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition nat1.h:1103
bool is_div_function_symbol(const atermpp::aterm &e)
Recogniser for function div.
Definition nat1.h:1131
const core::identifier_string & divmod_name()
Generate identifier @divmod.
Definition nat1.h:1962
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition nat1.h:528
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:1042
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition nat1.h:1066
void make_natpred(data_expression &result, const data_expression &arg0)
Make an application of function symbol @natpred.
Definition nat1.h:741
data_expression nat(const std::string &n)
Constructs expression of type Nat from a string.
bool is_dub_application(const atermpp::aterm &e)
Recogniser for application of @dub.
Definition nat1.h:815
bool is_nat2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Pos.
Definition nat1.h:369
const function_symbol & dub()
Constructor for function symbol @dub.
Definition nat1.h:769
void make_cnat(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cNat.
Definition nat1.h:171
application swap_zero_monus(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @swap_zero_monus.
Definition nat1.h:1679
const core::identifier_string & natpred_name()
Generate identifier @natpred.
Definition nat1.h:697
const function_symbol & pos2nat()
Constructor for function symbol Pos2Nat.
Definition nat1.h:297
void make_last(data_expression &result, const data_expression &arg0)
Make an application of function symbol @last.
Definition nat1.h:1944
application nat2pos(const data_expression &arg0)
Application of function symbol Nat2Pos.
Definition nat1.h:383
bool is_natural_constant(const data_expression &n)
Determines whether n is a natural constant.
bool is_monus_application(const atermpp::aterm &e)
Recogniser for application of @monus.
Definition nat1.h:1434
bool is_divmod_application(const atermpp::aterm &e)
Recogniser for application of @divmod.
Definition nat1.h:2018
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition nat1.h:2340
bool is_even_application(const atermpp::aterm &e)
Recogniser for application of @even.
Definition nat1.h:1370
Namespace for system defined sort pos.
void make_powerlog2_pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol @powerlog2.
Definition pos1.h:683
bool is_pos_predecessor_function_symbol(const atermpp::aterm &e)
Recogniser for function @pospred.
Definition pos1.h:403
bool is_add_with_carry_function_symbol(const atermpp::aterm &e)
Recogniser for function @addc.
Definition pos1.h:529
std::string positive_constant_as_string(const data_expression &n_in)
Return the string representation of a positive number.
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition pos1.h:292
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition pos1.h:785
void make_add_with_carry(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @addc.
Definition pos1.h:557
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition pos1.h:621
data_expression pos(const T t)
Constructs expression of type Bool from an integral type Type T is an unsigned integral type.
bool is_cdub_function_symbol(const atermpp::aterm &e)
Recogniser for function @cDub.
Definition pos1.h:117
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition pos1.h:213
implementation_map pos_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for pos.
Definition pos1.h:750
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition pos1.h:355
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition pos1.h:239
const function_symbol & powerlog2_pos()
Constructor for function symbol @powerlog2.
Definition pos1.h:649
bool is_positive_constant(const data_expression &n)
Determines whether n is a positive constant.
bool is_pos(const sort_expression &e)
Recogniser for sort expression Pos.
Definition pos1.h:52
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition pos1.h:821
const function_symbol & c1()
Constructor for function symbol @c1.
Definition pos1.h:75
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition pos1.h:365
const function_symbol & add_with_carry()
Constructor for function symbol @addc.
Definition pos1.h:519
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition pos1.h:797
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition pos1.h:610
bool is_cdub_application(const atermpp::aterm &e)
Recogniser for application of @cDub.
Definition pos1.h:153
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition pos1.h:303
function_symbol_vector pos_generate_functions_code()
Give all system defined mappings for pos.
Definition pos1.h:700
const function_symbol & pos_predecessor()
Constructor for function symbol @pospred.
Definition pos1.h:393
data_expression pos(const std::string &n)
Constructs expression of type Pos from a string.
const core::identifier_string & cdub_name()
Generate identifier @cDub.
Definition pos1.h:97
const core::identifier_string & c1_name()
Generate identifier @c1.
Definition pos1.h:65
const function_symbol & plus()
Constructor for function symbol +.
Definition pos1.h:455
bool is_add_with_carry_application(const atermpp::aterm &e)
Recogniser for application of @addc.
Definition pos1.h:567
const function_symbol & maximum()
Constructor for function symbol max.
Definition pos1.h:203
const core::identifier_string & powerlog2_pos_name()
Generate identifier @powerlog2.
Definition pos1.h:639
bool is_powerlog2_pos_application(const atermpp::aterm &e)
Recogniser for application of @powerlog2.
Definition pos1.h:693
const core::identifier_string & times_name()
Generate identifier *.
Definition pos1.h:575
function_symbol_vector pos_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for pos.
Definition pos1.h:171
bool is_c1_function_symbol(const atermpp::aterm &e)
Recogniser for function @c1.
Definition pos1.h:85
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition pos1.h:809
const core::identifier_string & plus_name()
Generate identifier +.
Definition pos1.h:445
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition pos1.h:277
const function_symbol & cdub()
Constructor for function symbol @cDub.
Definition pos1.h:107
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition pos1.h:773
application add_with_carry(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @addc.
Definition pos1.h:545
implementation_map pos_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition pos1.h:184
application powerlog2_pos(const data_expression &arg0)
Application of function symbol @powerlog2.
Definition pos1.h:673
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition pos1.h:480
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition pos1.h:631
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition pos1.h:595
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition pos1.h:491
const core::identifier_string & add_with_carry_name()
Generate identifier @addc.
Definition pos1.h:509
const function_symbol & times()
Constructor for function symbol *.
Definition pos1.h:585
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition pos1.h:341
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition pos1.h:465
const core::identifier_string & minimum_name()
Generate identifier min.
Definition pos1.h:257
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition pos1.h:313
data_equation_vector pos_generate_equations_code()
Give all system defined equations for pos.
Definition pos1.h:830
application pos_predecessor(const data_expression &arg0)
Application of function symbol @pospred.
Definition pos1.h:417
bool is_powerlog2_pos_function_symbol(const atermpp::aterm &e)
Recogniser for function @powerlog2.
Definition pos1.h:659
application cdub(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cDub.
Definition pos1.h:132
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition pos1.h:375
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition pos1.h:228
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:42
const core::identifier_string & maximum_name()
Generate identifier max.
Definition pos1.h:193
const core::identifier_string & pos_name()
Definition pos1.h:33
const function_symbol & minimum()
Constructor for function symbol min.
Definition pos1.h:267
NUMERIC_TYPE positive_constant_to_value(const data_expression &n)
Returns the NUMERIC_TYPE representation of a positive number.
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition pos1.h:761
function_symbol_vector pos_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for pos.
Definition pos1.h:717
function_symbol_vector pos_generate_constructors_code()
Give all system defined constructors for pos.
Definition pos1.h:160
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition pos1.h:249
bool is_pos_predecessor_application(const atermpp::aterm &e)
Recogniser for application of @pospred.
Definition pos1.h:437
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition pos1.h:501
const function_symbol & succ()
Constructor for function symbol succ.
Definition pos1.h:331
void make_cdub(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cDub.
Definition pos1.h:143
const core::identifier_string & pos_predecessor_name()
Generate identifier @pospred.
Definition pos1.h:383
function_symbol_vector pos_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for pos.
Definition pos1.h:730
const core::identifier_string & succ_name()
Generate identifier succ.
Definition pos1.h:321
void make_pos_predecessor(data_expression &result, const data_expression &arg0)
Make an application of function symbol @pospred.
Definition pos1.h:427
Namespace for system defined sort real_.
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:647
void make_abs(data_expression &result, const data_expression &arg0)
Make an application of function symbol abs.
Definition real1.h:781
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1056
bool is_real2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Int.
Definition real1.h:488
data_expression real_(T numerator, T denominator)
Constructs expression of type Real from an integral type.
application exp(const data_expression &arg0, const data_expression &arg1)
Application of function symbol exp.
Definition real1.h:1367
void make_minus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition real1.h:1208
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real1.h:104
void make_reduce_fraction(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @redfrac.
Definition real1.h:1692
const core::identifier_string & maximum_name()
Generate identifier max.
Definition real1.h:530
void make_negate(data_expression &result, const data_expression &arg0)
Make an application of function symbol -.
Definition real1.h:864
const core::identifier_string & minus_name()
Generate identifier -.
Definition real1.h:1141
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition real1.h:922
application reduce_fraction_helper(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @redfrachlp.
Definition real1.h:1811
const core::identifier_string & real_name()
Definition real1.h:36
const function_symbol & pos2real()
Constructor for function symbol Pos2Real.
Definition real1.h:168
const core::identifier_string & reduce_fraction_where_name()
Generate identifier @redfracwhr.
Definition real1.h:1710
const function_symbol & round()
Constructor for function symbol round.
Definition real1.h:1594
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition real1.h:1096
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1234
application divides(const data_expression &arg0, const data_expression &arg1)
Application of function symbol /.
Definition real1.h:1431
bool is_abs_application(const atermpp::aterm &e)
Recogniser for application of abs.
Definition real1.h:791
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1404
const core::identifier_string & int2real_name()
Generate identifier Int2Real.
Definition real1.h:282
data_expression real_(T t)
Constructs expression of type Real from an integral type.
const function_symbol & real2nat()
Constructor for function symbol Real2Nat.
Definition real1.h:416
bool is_divides_function_symbol(const atermpp::aterm &e)
Recogniser for function /.
Definition real1.h:1415
const core::identifier_string & creal_name()
Generate identifier @cReal.
Definition real1.h:94
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition real1.h:947
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition real1.h:1388
application real2nat(const data_expression &arg0)
Application of function symbol Real2Nat.
Definition real1.h:440
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition real1.h:1962
bool is_int2real_application(const atermpp::aterm &e)
Recogniser for application of Int2Real.
Definition real1.h:336
const function_symbol & ceil()
Constructor for function symbol ceil.
Definition real1.h:1532
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition real1.h:1986
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1133
bool is_divides_application(const atermpp::aterm &e)
Recogniser for application of /.
Definition real1.h:1452
bool is_reduce_fraction_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfrac.
Definition real1.h:1666
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition real1.h:594
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition real1.h:1378
const core::identifier_string & divides_name()
Generate identifier /.
Definition real1.h:1396
bool is_real2int_application(const atermpp::aterm &e)
Recogniser for application of Real2Int.
Definition real1.h:522
const core::identifier_string & ceil_name()
Generate identifier ceil.
Definition real1.h:1522
bool is_creal_function_symbol(const atermpp::aterm &e)
Recogniser for function @cReal.
Definition real1.h:114
void make_real2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Nat.
Definition real1.h:450
bool is_minus_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition real1.h:1181
application creal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cReal.
Definition real1.h:129
bool is_reduce_fraction_where_application(const atermpp::aterm &e)
Recogniser for application of @redfracwhr.
Definition real1.h:1768
function_symbol succ(const sort_expression &s0)
Definition real1.h:890
application negate(const data_expression &arg0)
Application of function symbol -.
Definition real1.h:854
bool is_floor_function_symbol(const atermpp::aterm &e)
Recogniser for function floor.
Definition real1.h:1480
void make_int2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Real.
Definition real1.h:326
void make_divides(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol /.
Definition real1.h:1442
const core::identifier_string & floor_name()
Generate identifier floor.
Definition real1.h:1460
const core::identifier_string & times_name()
Generate identifier *.
Definition real1.h:1226
bool is_abs_function_symbol(const atermpp::aterm &e)
Recogniser for function abs.
Definition real1.h:756
bool is_ceil_application(const atermpp::aterm &e)
Recogniser for application of ceil.
Definition real1.h:1576
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition real1.h:937
const function_symbol & real2int()
Constructor for function symbol Real2Int.
Definition real1.h:478
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition real1.h:631
application nat2real(const data_expression &arg0)
Application of function symbol Nat2Real.
Definition real1.h:254
const function_symbol & reduce_fraction()
Constructor for function symbol @redfrac.
Definition real1.h:1656
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:150
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition real1.h:1040
const core::identifier_string & negate_name()
Generate identifier -.
Definition real1.h:799
void make_reduce_fraction_helper(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @redfrachlp.
Definition real1.h:1822
void make_pos2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Real.
Definition real1.h:202
function_symbol pred(const sort_expression &s0)
Definition real1.h:973
bool is_round_function_symbol(const atermpp::aterm &e)
Recogniser for function round.
Definition real1.h:1604
const core::identifier_string & succ_name()
Generate identifier succ.
Definition real1.h:882
const function_symbol & reduce_fraction_helper()
Constructor for function symbol @redfrachlp.
Definition real1.h:1786
const core::identifier_string & abs_name()
Generate identifier abs.
Definition real1.h:724
data_equation_vector real_generate_equations_code()
Give all system defined equations for real_.
Definition real1.h:2007
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition real1.h:1266
const core::identifier_string & round_name()
Generate identifier round.
Definition real1.h:1584
bool is_negate_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition real1.h:839
application int2real(const data_expression &arg0)
Application of function symbol Int2Real.
Definition real1.h:316
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1149
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:45
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition real1.h:679
const function_symbol & floor()
Constructor for function symbol floor.
Definition real1.h:1470
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition real1.h:706
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition real1.h:1293
const core::identifier_string & reduce_fraction_helper_name()
Generate identifier @redfrachlp.
Definition real1.h:1776
function_symbol_vector real_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for real_.
Definition real1.h:75
bool is_real2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Pos.
Definition real1.h:364
void make_real2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Int.
Definition real1.h:512
function_symbol_vector real_generate_constructors_code()
Give all system defined constructors for real_.
Definition real1.h:67
void make_nat2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Real.
Definition real1.h:264
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition real1.h:621
bool is_floor_application(const atermpp::aterm &e)
Recogniser for application of floor.
Definition real1.h:1514
application reduce_fraction_where(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @redfracwhr.
Definition real1.h:1746
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:55
const function_symbol & reduce_fraction_where()
Constructor for function symbol @redfracwhr.
Definition real1.h:1720
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition real1.h:1112
implementation_map real_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for real_.
Definition real1.h:1927
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition real1.h:1282
bool is_ceil_function_symbol(const atermpp::aterm &e)
Recogniser for function ceil.
Definition real1.h:1542
data_expression real_(const std::string &numerator, const std::string &denominator)
Constructs expression of type Real from two number strings.
application real2int(const data_expression &arg0)
Application of function symbol Real2Int.
Definition real1.h:502
const core::identifier_string & pred_name()
Generate identifier pred.
Definition real1.h:965
const function_symbol & nat2real()
Constructor for function symbol Nat2Real.
Definition real1.h:230
const core::identifier_string & minimum_name()
Generate identifier min.
Definition real1.h:639
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition real1.h:1950
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition real1.h:957
application pos2real(const data_expression &arg0)
Application of function symbol Pos2Real.
Definition real1.h:192
void make_round(data_expression &result, const data_expression &arg0)
Make an application of function symbol round.
Definition real1.h:1628
bool is_pos2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Real.
Definition real1.h:178
function_symbol_vector real_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for real_.
Definition real1.h:1888
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition real1.h:1974
const core::identifier_string & plus_name()
Generate identifier +.
Definition real1.h:1048
function_symbol abs(const sort_expression &s0)
Definition real1.h:732
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition real1.h:1938
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1303
void make_ceil(data_expression &result, const data_expression &arg0)
Make an application of function symbol ceil.
Definition real1.h:1566
const core::identifier_string & reduce_fraction_name()
Generate identifier @redfrac.
Definition real1.h:1646
function_symbol negate(const sort_expression &s0)
Definition real1.h:807
application minus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition real1.h:1197
application abs(const data_expression &arg0)
Application of function symbol abs.
Definition real1.h:771
bool is_real2pos_application(const atermpp::aterm &e)
Recogniser for application of Real2Pos.
Definition real1.h:398
bool is_reduce_fraction_application(const atermpp::aterm &e)
Recogniser for application of @redfrac.
Definition real1.h:1702
bool is_int2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Real.
Definition real1.h:302
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:874
bool is_reduce_fraction_helper_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfrachlp.
Definition real1.h:1796
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition real1.h:716
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1218
const core::identifier_string & pos2real_name()
Generate identifier Pos2Real.
Definition real1.h:158
bool is_round_application(const atermpp::aterm &e)
Recogniser for application of round.
Definition real1.h:1638
application reduce_fraction(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @redfrac.
Definition real1.h:1681
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition real1.h:1998
const core::identifier_string & exp_name()
Generate identifier exp.
Definition real1.h:1311
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition real1.h:610
bool is_real2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Nat.
Definition real1.h:426
const core::identifier_string & real2nat_name()
Generate identifier Real2Nat.
Definition real1.h:406
const core::identifier_string & real2int_name()
Generate identifier Real2Int.
Definition real1.h:468
const function_symbol & int2real()
Constructor for function symbol Int2Real.
Definition real1.h:292
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition real1.h:1005
const core::identifier_string & nat2real_name()
Generate identifier Nat2Real.
Definition real1.h:220
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1319
application real2pos(const data_expression &arg0)
Application of function symbol Real2Pos.
Definition real1.h:378
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition real1.h:1030
bool is_real2nat_application(const atermpp::aterm &e)
Recogniser for application of Real2Nat.
Definition real1.h:460
bool is_pos2real_application(const atermpp::aterm &e)
Recogniser for application of Pos2Real.
Definition real1.h:212
application floor(const data_expression &arg0)
Application of function symbol floor.
Definition real1.h:1494
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition real1.h:695
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition real1.h:1123
bool is_reduce_fraction_helper_application(const atermpp::aterm &e)
Recogniser for application of @redfrachlp.
Definition real1.h:1832
void make_floor(data_expression &result, const data_expression &arg0)
Make an application of function symbol floor.
Definition real1.h:1504
const function_symbol & real2pos()
Constructor for function symbol Real2Pos.
Definition real1.h:354
implementation_map real_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition real1.h:85
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:538
function_symbol_vector real_generate_functions_code()
Give all system defined mappings for real_.
Definition real1.h:1839
void make_reduce_fraction_where(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @redfracwhr.
Definition real1.h:1758
function_symbol_vector real_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for real_.
Definition real1.h:1875
const core::identifier_string & real2pos_name()
Generate identifier Real2Pos.
Definition real1.h:344
data_expression real_(const std::string &n)
Constructs expression of type Real from a string.
void make_real2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Pos.
Definition real1.h:388
application round(const data_expression &arg0)
Application of function symbol round.
Definition real1.h:1618
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition real1.h:1351
application pred(const data_expression &arg0)
Application of function symbol pred.
Definition real1.h:1020
void make_creal(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cReal.
Definition real1.h:140
application ceil(const data_expression &arg0)
Application of function symbol ceil.
Definition real1.h:1556
bool is_reduce_fraction_where_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfracwhr.
Definition real1.h:1730
bool is_nat2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Real.
Definition real1.h:240
bool is_nat2real_application(const atermpp::aterm &e)
Recogniser for application of Nat2Real.
Definition real1.h:274
Namespace for system defined sort set_.
Definition set1.h:33
const core::identifier_string & fset_intersection_name()
Generate identifier @fset_inter.
Definition set1.h:1035
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition set1.h:330
function_symbol true_function(const sort_expression &s)
Constructor for function symbol @true_.
Definition set1.h:725
const core::identifier_string & or_function_name()
Generate identifier @or_.
Definition set1.h:903
bool is_set_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @setcomp.
Definition set1.h:276
const core::identifier_string & constructor_name()
Generate identifier @set.
Definition set1.h:63
implementation_map set_cpp_implementable_mappings(const sort_expression &)
Give all system defined mappings that are to be implemented in C++ code for set_.
Definition set1.h:1174
application fset_intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fset_inter.
Definition set1.h:1072
bool is_false_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @false_.
Definition set1.h:673
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition set1.h:608
bool is_not_function_application(const atermpp::aterm &e)
Recogniser for application of @not_.
Definition set1.h:831
bool is_and_function_application(const atermpp::aterm &e)
Recogniser for application of @and_.
Definition set1.h:895
void make_or_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @or_.
Definition set1.h:949
function_symbol_vector set_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for set_.
Definition set1.h:1130
application or_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @or_.
Definition set1.h:938
bool is_fset_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_inter.
Definition set1.h:1055
bool is_set(const sort_expression &e)
Recogniser for sort expression Set(s)
Definition set1.h:50
function_symbol or_function(const sort_expression &s)
Constructor for function symbol @or_.
Definition set1.h:913
void make_complement(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol !.
Definition set1.h:392
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition set1.h:479
const core::identifier_string & false_function_name()
Generate identifier @false_.
Definition set1.h:653
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition set1.h:303
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition set1.h:1257
bool is_true_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @true_.
Definition set1.h:735
bool is_complement_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition set1.h:402
bool is_or_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @or_.
Definition set1.h:923
function_symbol fset_intersection(const sort_expression &s)
Constructor for function symbol @fset_inter.
Definition set1.h:1045
const core::identifier_string & set_comprehension_name()
Generate identifier @setcomp.
Definition set1.h:222
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)
Make an application of function symbol @fset_union.
Definition set1.h:1017
bool is_fset_union_application(const atermpp::aterm &e)
Recogniser for application of @fset_union.
Definition set1.h:1027
bool is_false_function_application(const atermpp::aterm &e)
Recogniser for application of @false_.
Definition set1.h:707
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition set1.h:1185
bool is_not_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @not_.
Definition set1.h:797
function_symbol and_function(const sort_expression &s)
Constructor for function symbol @and_.
Definition set1.h:849
bool is_set_comprehension_function_symbol(const atermpp::aterm &e)
Recogniser for function @setcomp.
Definition set1.h:242
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition set1.h:340
const core::identifier_string & not_function_name()
Generate identifier @not_.
Definition set1.h:777
application not_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @not_.
Definition set1.h:811
const core::identifier_string & in_name()
Generate identifier in.
Definition set1.h:284
function_symbol_vector set_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for set_.
Definition set1.h:127
bool is_fset_intersection_application(const atermpp::aterm &e)
Recogniser for application of @fset_inter.
Definition set1.h:1095
data_expression set_enumeration(const sort_expression &s, data_expression_list const &range)
Application of function symbol set_enumeration.
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition set1.h:645
function_symbol not_function(const sort_expression &s)
Constructor for function symbol @not_.
Definition set1.h:787
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition set1.h:1209
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition set1.h:458
bool is_constructor_application(const atermpp::aterm &e)
Recogniser for application of @set.
Definition set1.h:119
const core::identifier_string & fset_union_name()
Generate identifier @fset_union.
Definition set1.h:967
bool is_set_fset_application(const atermpp::aterm &e)
Recogniser for application of @setfset.
Definition set1.h:214
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition set1.h:554
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition set1.h:624
application complement(const sort_expression &s, const data_expression &arg0)
Application of function symbol !.
Definition set1.h:382
const core::identifier_string & complement_name()
Generate identifier !.
Definition set1.h:348
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:495
application set_fset(const sort_expression &s, const data_expression &arg0)
Application of function symbol @setfset.
Definition set1.h:194
const core::identifier_string & and_function_name()
Generate identifier @and_.
Definition set1.h:839
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition set1.h:543
bool is_fset_union_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_union.
Definition set1.h:987
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition set1.h:1233
function_symbol fset_union(const sort_expression &s)
Constructor for function symbol @fset_union.
Definition set1.h:977
void make_and_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @and_.
Definition set1.h:885
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set1.h:39
bool is_set_fset_function_symbol(const atermpp::aterm &e)
Recogniser for function @setfset.
Definition set1.h:180
application set_comprehension(const sort_expression &s, const data_expression &arg0)
Application of function symbol @setcomp.
Definition set1.h:256
const core::identifier_string & intersection_name()
Generate identifier *.
Definition set1.h:487
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)
Make an application of function symbol @fset_inter.
Definition set1.h:1085
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @set.
Definition set1.h:73
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition set1.h:1245
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition set1.h:1197
function_symbol false_function(const sort_expression &s)
Constructor for function symbol @false_.
Definition set1.h:663
void make_constructor(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @set.
Definition set1.h:109
const core::identifier_string & set_fset_name()
Generate identifier @setfset.
Definition set1.h:160
const core::identifier_string & union_name()
Generate identifier +.
Definition set1.h:410
bool is_complement_function_symbol(const atermpp::aterm &e)
Recogniser for function !.
Definition set1.h:368
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:292
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:418
bool is_constructor_function_symbol(const atermpp::aterm &e)
Recogniser for function @set.
Definition set1.h:83
function_symbol_vector set_generate_functions_code(const sort_expression &s)
Give all system defined mappings for set_.
Definition set1.h:1103
application fset_union(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fset_union.
Definition set1.h:1004
function_symbol_vector set_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for set_.
Definition set1.h:138
const core::identifier_string & difference_name()
Generate identifier -.
Definition set1.h:572
void make_set_comprehension(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @setcomp.
Definition set1.h:266
application true_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @true_.
Definition set1.h:749
void make_not_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @not_.
Definition set1.h:821
bool is_or_function_application(const atermpp::aterm &e)
Recogniser for application of @or_.
Definition set1.h:959
const core::identifier_string & true_function_name()
Generate identifier @true_.
Definition set1.h:715
void make_false_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @false_.
Definition set1.h:697
void make_true_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @true_.
Definition set1.h:759
application false_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @false_.
Definition set1.h:687
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:580
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition set1.h:442
function_symbol complement(const sort_expression &s)
Constructor for function symbol !.
Definition set1.h:358
bool is_true_function_application(const atermpp::aterm &e)
Recogniser for application of @true_.
Definition set1.h:769
function_symbol set_fset(const sort_expression &s)
Constructor for function symbol @setfset.
Definition set1.h:170
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition set1.h:635
implementation_map set_cpp_implementable_constructors(const sort_expression &)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition set1.h:151
function_symbol set_comprehension(const sort_expression &s)
Constructor for function symbol @setcomp.
Definition set1.h:232
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition set1.h:319
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition set1.h:564
data_equation_vector set_generate_equations_code(const sort_expression &s)
Give all system defined equations for set_.
Definition set1.h:1267
application and_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @and_.
Definition set1.h:874
function_symbol_vector set_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for set_.
Definition set1.h:1144
bool is_and_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @and_.
Definition set1.h:859
void make_set_fset(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @setfset.
Definition set1.h:204
void make_union(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition set1.h:469
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition set1.h:527
application constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @set.
Definition set1.h:98
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition set1.h:1221
std::string pp(const data::structured_sort_constructor_argument &x, bool arg0)
Definition data.cpp:71
void make_set_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
std::set< data::variable > find_free_variables(const T &x)
Returns all free variables that occur in an object.
Definition find.h:329
void swap(fset_container &t1, fset_container &t2) noexcept
\brief swap overload
void make_data_expression(data_expression &result)
bool is_convertible(const sort_expression &s1, const sort_expression &s2)
Returns true if and only if s1 == s2, or if s1 is a less specific numeric type than s2.
void make_function_symbol(atermpp::aterm &t, const ARGUMENTS &... args)
data::data_equation normalize_sorts(const data::data_equation &x, const data::sort_specification &sortspec)
Definition data.cpp:82
constexpr std::size_t undefined_index()
Returns an index that corresponds to 'undefined'.
Definition undefined.h:27
void swap(assignment &t1, assignment &t2) noexcept
\brief swap overload
Definition assignment.h:171
bool is_greater_application(const DataExpression &e)
Recogniser for application of >
Definition standard.h:348
bool is_less_total_application(const DataExpression &e)
Recogniser for application of less_total.
Definition standard.h:422
void normalize_sorts(data::data_equation_vector &x, const data::sort_specification &sortspec)
Definition data.cpp:84
void swap(function_sort &t1, function_sort &t2) noexcept
\brief swap overload
bool is_greater_function_symbol(const DataExpression &e)
Recogniser for function >
Definition standard.h:328
void swap(container_sort &t1, container_sort &t2) noexcept
\brief swap overload
void if_always_else_manual_implementation(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
The data expression of an application of the function symbol @if_always_else.
const data::data_expression & undefined_real()
Returns a data expression of type Real that corresponds to 'undefined'.
Definition undefined.h:66
void swap(untyped_identifier_assignment &t1, untyped_identifier_assignment &t2) noexcept
\brief swap overload
Definition assignment.h:267
bool is_if_always_else_function_symbol(const atermpp::aterm &e)
Recogniser for function @if_always_else.
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
bool is_less_total_function_symbol(const DataExpression &e)
Recogniser for function less_total.
Definition standard.h:402
data::data_equation_list normalize_sorts(const data::data_equation_list &x, const data::sort_specification &sortspec)
Definition data.cpp:83
std::string pp(const data::exists &x, bool arg0)
Definition data.cpp:53
std::ostream & operator<<(std::ostream &out, const untyped_sort_variable &x)
bool is_data_equation(const atermpp::aterm &t)
Recognizer function.
std::set< data::data_expression > find_data_expressions(const T &x)
Returns all data expressions that occur in an object.
Definition find.h:443
std::ostream & operator<<(std::ostream &out, const untyped_data_parameter &x)
std::string pp(const data::untyped_identifier_assignment &x, bool arg0)
Definition data.cpp:74
application function_update(const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @func_update.
void find_identifiers(const T &x, OutputIterator o)
Writes all identifiers that occur in an object to an output iterator.
Definition find.h:352
std::set< data::function_symbol > find_function_symbols(const T &x)
Returns all function symbols that occur in an object.
Definition find.h:401
function_symbol_vector function_update_mCRL2_usable_mappings(const sort_expression &s, const sort_expression &t)
Give all system defined mappings that can be used in mCRL2 specs for function_update.
std::ostream & operator<<(std::ostream &out, const bag_comprehension_binder &x)
void swap(structured_sort_constructor &t1, structured_sort_constructor &t2) noexcept
\brief swap overload
bool is_is_not_a_function_update_application(const atermpp::aterm &e)
Recogniser for application of @is_not_an_update.
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:282
std::set< data::sort_expression > find_sort_expressions(const T &x)
Returns all sort expressions that occur in an object.
Definition find.h:381
void make_bag_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
void swap(exists &t1, exists &t2) noexcept
\brief swap overload
Definition exists.h:82
std::ostream & operator<<(std::ostream &out, const set_comprehension_binder &x)
bool is_set_container(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const container_sort &x)
void swap(untyped_sort &t1, untyped_sort &t2) noexcept
\brief swap overload
data_expression number(const sort_expression &s, const std::string &n)
Construct numeric expression from a string representing a number in decimal notation.
std::ostream & operator<<(std::ostream &out, const basic_sort &x)
Definition basic_sort.h:78
function_symbol_vector standard_generate_functions_code(const sort_expression &s)
Give all standard system defined functions for sort s.
Definition standard.h:430
void swap(structured_sort_constructor_argument &t1, structured_sort_constructor_argument &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const machine_number &x)
void find_free_variables_with_bound(const T &x, OutputIterator o, const VariableContainer &bound)
Writes all free variables that occur in an object to an output iterator.
Definition find.h:320
void make_machine_number(atermpp::aterm &t, size_t n)
std::set< data::variable > find_all_variables(const data::data_expression_list &x)
Definition data.cpp:94
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
std::string pp(const data::list_container &x, bool arg0)
Definition data.cpp:63
void swap(untyped_identifier &t1, untyped_identifier &t2) noexcept
\brief swap overload
bool is_application_no_check(const atermpp::aterm &x)
Returns true if the term t is an application, but it does not check whether an application symbol of ...
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:168
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
void make_where_clause(atermpp::aterm &t, const ARGUMENTS &... args)
void make_untyped_data_parameter(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_equal_to_function_symbol(const DataExpression &e)
Recogniser for function ==.
Definition standard.h:140
function_symbol_vector function_update_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for function_update.
data_expression_list make_data_expression_list(Container const &r, typename atermpp::enable_if_container< Container, data_expression >::type *=nullptr)
Converts an container with data expressions to data_expression_list.
std::set< data::sort_expression > find_sort_expressions(const data::data_expression &x)
Definition data.cpp:91
void swap(set_comprehension_binder &t1, set_comprehension_binder &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const container_type &x)
const data::variable & undefined_variable()
Returns a data variable that corresponds to 'undefined'.
Definition undefined.h:34
void swap(structured_sort &t1, structured_sort &t2) noexcept
\brief swap overload
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:89
std::ostream & operator<<(std::ostream &out, const list_container &x)
std::ostream & operator<<(std::ostream &out, const structured_sort_constructor &x)
std::ostream & operator<<(std::ostream &out, const untyped_set_or_bag_comprehension_binder &x)
bool is_application(const data_expression &t)
Returns true if the term t is an application.
bool is_list_container(const atermpp::aterm &x)
bool is_if_application(const DataExpression &e)
Recogniser for application of if.
Definition standard.h:237
void make_basic_sort(atermpp::aterm &t, const ARGUMENTS &... args)
Definition basic_sort.h:65
void make_function_update_stable(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @func_update_stable.
bool search_data_expression(Container const &container, const data_expression &s)
Returns true if the term has a given data expression as subterm.
Definition find.h:490
std::set< data::variable > find_all_variables(const T &x)
Returns all variables that occur in an object.
Definition find.h:299
void swap(untyped_sort_variable &t1, untyped_sort_variable &t2) noexcept
\brief swap overload
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &dom4, const sort_expression &codomain)
Convenience constructor for function sort with domain size 4.
implementation_map function_update_cpp_implementable_mappings(const sort_expression &s, const sort_expression &t)
Give all system defined mappings that are to be implemented in C++ code for function_update.
void swap(fbag_container &t1, fbag_container &t2) noexcept
\brief swap overload
bool is_not_equal_to_application(const DataExpression &e)
Recogniser for application of !=.
Definition standard.h:197
void swap(basic_sort &t1, basic_sort &t2) noexcept
\brief swap overload
Definition basic_sort.h:84
std::string pp(const data::container_type &x, bool arg0)
Definition data.cpp:49
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:93
void find_all_variables(const T &x, OutputIterator o)
Writes all variables that occur in an object to an output iterator.
Definition find.h:290
function_symbol if_always_else(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @if_always_else.
void swap(list_container &t1, list_container &t2) noexcept
\brief swap overload
void swap(exists_binder &t1, exists_binder &t2) noexcept
\brief swap overload
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:245
void make_function_update(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @func_update.
void swap(assignment_expression &t1, assignment_expression &t2) noexcept
\brief swap overload
Definition assignment.h:80
void make_untyped_set_or_bag_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
std::string pp(const data::set_container &x, bool arg0)
Definition data.cpp:67
const core::identifier_string & function_update_name()
Generate identifier @func_update.
bool is_untyped_possible_sorts(const atermpp::aterm &x)
Returns true if the term t is an expression for multiple possible sorts.
bool is_untyped_sort(const atermpp::aterm &x)
Returns true if the term t is the unknown sort.
application less_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <=.
Definition standard.h:300
function_symbol less_total(const sort_expression &s)
Constructor for function symbol less_total.
Definition standard.h:393
const data_expression & find_rhs(const variable &v, const ASSIGNMENT_CONTAINER &c)
Returns the right hand sides of an assignment list.
Definition assignment.h:324
std::string pp(const structured_sort_constructor_vector &x)
void if_always_else_application(data_expression &result, const data_expression &a1)
Application of a function that is user defined instead of by rewrite rules. It does not have sort par...
std::ostream & operator<<(std::ostream &out, const fset_container &x)
void swap(where_clause &t1, where_clause &t2) noexcept
\brief swap overload
bool search_free_variable(const T &x, const variable &v)
Returns true if the term has a given free variable as subterm.
Definition find.h:467
bool is_greater_equal_application(const DataExpression &e)
Recogniser for application of >=.
Definition standard.h:385
std::string pp(const data::untyped_set_or_bag_comprehension_binder &x, bool arg0)
Definition data.cpp:77
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
Definition standard.h:263
std::ostream & operator<<(std::ostream &out, const untyped_possible_sorts &x)
data::data_expression translate_user_notation(const data::data_expression &x)
Definition data.cpp:88
std::string pp(const data::sort_expression_vector &x, bool arg0)
Definition data.cpp:25
function_symbol_vector function_update_generate_constructors_and_functions_code(const sort_expression &s, const sort_expression &t)
Give all system defined mappings and constructors for function_update.
std::string pp(const data::untyped_sort &x, bool arg0)
Definition data.cpp:78
std::string pp(const data::data_equation &x, bool arg0)
Definition data.cpp:50
bool is_if_always_else_application(const atermpp::aterm &e)
Recogniser for application of @if_always_else.
application less_total(const data_expression &arg0, const data_expression &arg1)
Application of function symbol less_total.
Definition standard.h:411
std::string pp(const data::forall &x, bool arg0)
Definition data.cpp:56
void swap(set_container &t1, set_container &t2) noexcept
\brief swap overload
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
void make_variable(atermpp::aterm &t, const ARGUMENTS &... args)
Definition variable.h:77
std::string pp(const data::assignment_list &x, bool arg0)
Definition data.cpp:28
std::ostream & operator<<(std::ostream &out, const assignment_expression &x)
Definition assignment.h:74
std::string pp(const data::untyped_identifier &x, bool arg0)
Definition data.cpp:73
application not_equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol !=.
Definition standard.h:186
std::string pp(const data::function_symbol_list &x, bool arg0)
Definition data.cpp:32
std::ostream & operator<<(std::ostream &out, const untyped_sort &x)
function_symbol_vector function_update_generate_constructors_code()
Give all system defined constructors for function_update.
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
void swap(container_type &t1, container_type &t2) noexcept
\brief swap overload
application if_(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol if.
Definition standard.h:224
std::ostream & operator<<(std::ostream &out, const forall &x)
Definition forall.h:77
bool is_untyped_identifier(const atermpp::aterm &x)
Returns true if the term t is an identifier.
data_equation_vector standard_generate_equations_code(const sort_expression &s)
Give all standard system defined equations for sort s.
Definition standard.h:448
void swap(bag_container &t1, bag_container &t2) noexcept
\brief swap overload
std::string pp(const data::lambda_binder &x, bool arg0)
Definition data.cpp:62
void make_untyped_identifier(atermpp::aterm &t, const ARGUMENTS &... args)
void find_function_symbols(const T &x, OutputIterator o)
Writes all function symbols that occur in an object to an output iterator.
Definition find.h:392
void make_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
Definition assignment.h:137
std::ostream & operator<<(std::ostream &out, const untyped_identifier_assignment &x)
Definition assignment.h:261
const core::identifier_string & if_always_else_name()
Generate identifier @if_always_else.
void swap(untyped_set_or_bag_comprehension_binder &t1, untyped_set_or_bag_comprehension_binder &t2) noexcept
\brief swap overload
std::string pp(const structured_sort_constructor_list &x)
void make_untyped_identifier_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
Definition assignment.h:233
void swap(bag_comprehension_binder &t1, bag_comprehension_binder &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const exists &x)
Definition exists.h:76
bool is_set_comprehension_binder(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const alias &x)
Definition alias.h:91
void swap(forall_binder &t1, forall_binder &t2) noexcept
\brief swap overload
void swap(data_equation &t1, data_equation &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const lambda &x)
Definition lambda.h:89
void find_free_variables(const T &x, OutputIterator o)
Writes all free variables that occur in an object to an output iterator.
Definition find.h:310
std::ostream & operator<<(std::ostream &out, const forall_binder &x)
bool is_exists_binder(const atermpp::aterm &x)
std::set< data::variable > find_all_variables(const data::function_symbol &x)
Definition data.cpp:95
std::vector< data::variable > find_free_variables_in_order(const T &x)
Returns all variables that occur in an object.
Definition find.h:414
std::string pp(const data::application &x, bool arg0)
Definition data.cpp:40
bool is_not_equal_to_function_symbol(const DataExpression &e)
Recogniser for function !=.
Definition standard.h:177
void make_structured_sort_constructor_argument(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(lambda &t1, lambda &t2) noexcept
\brief swap overload
Definition lambda.h:95
std::string pp(const data::function_sort &x, bool arg0)
Definition data.cpp:59
void swap(untyped_data_parameter &t1, untyped_data_parameter &t2) noexcept
\brief swap overload
void make_alias(atermpp::aterm &t, const ARGUMENTS &... args)
Definition alias.h:63
std::string pp(const data::abstraction &x, bool arg0)
Definition data.cpp:38
const core::identifier_string & is_not_a_function_update_name()
Generate identifier @is_not_an_update.
std::string pp(const data::bag_comprehension_binder &x, bool arg0)
Definition data.cpp:44
void make_lambda(atermpp::aterm &result, ARGUMENTS... arguments)
Definition lambda.h:74
application function_update_stable(const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @func_update_stable.
function_symbol greater_equal(const sort_expression &s)
Constructor for function symbol >=.
Definition standard.h:356
std::ostream & operator<<(std::ostream &out, const structured_sort &x)
std::ostream & operator<<(std::ostream &out, const set_container &x)
std::string pp(const data::set_comprehension_binder &x, bool arg0)
Definition data.cpp:66
bool is_assignment_expression(const atermpp::aterm &x)
Definition assignment.h:60
std::string pp(const data::assignment &x, bool arg0)
Definition data.cpp:41
bool search_sort_expression(Container const &container, const sort_expression &s)
Returns true if the term has a given sort expression as subterm.
Definition find.h:479
std::string pp(const data::structured_sort &x, bool arg0)
Definition data.cpp:69
std::ostream & operator<<(std::ostream &out, const bag_container &x)
std::string pp(const data::basic_sort &x, bool arg0)
Definition data.cpp:46
bool is_structured_sort_constructor_argument(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const exists_binder &x)
bool is_function_update_function_symbol(const atermpp::aterm &e)
Recogniser for function @func_update.
void swap(bag_comprehension &t1, bag_comprehension &t2) noexcept
\brief swap overload
void is_not_a_function_update_application(data_expression &result, const data_expression &a1)
Application of a function that is user defined instead of by rewrite rules. It does not have sort par...
std::ostream & operator<<(std::ostream &out, const assignment &x)
Definition assignment.h:165
application is_not_a_function_update(const sort_expression &s, const sort_expression &t, const data_expression &arg0)
Application of function symbol @is_not_an_update.
void make_if_always_else(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @if_always_else.
bool is_system_defined(const sort_expression &s)
Returns true iff the expression represents a standard sort.
std::string pp(const data::exists_binder &x, bool arg0)
Definition data.cpp:54
void swap(forall &t1, forall &t2) noexcept
\brief swap overload
Definition forall.h:83
bool is_function_update_stable_function_symbol(const atermpp::aterm &e)
Recogniser for function @func_update_stable.
void swap(binder_type &t1, binder_type &t2) noexcept
\brief swap overload
Definition binder_type.h:66
std::string pp(const data::bag_comprehension &x, bool arg0)
Definition data.cpp:43
void make_forall(atermpp::aterm &result, ARGUMENTS... arguments)
Definition forall.h:63
bool is_structured_sort_constructor(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const lambda_binder &x)
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
variable_list left_hand_sides(const assignment_list &x)
Returns the left hand sides of an assignment list.
Definition assignment.h:307
bool is_lambda_binder(const atermpp::aterm &x)
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
std::string pp(const data::variable &x, bool arg0)
Definition data.cpp:80
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
void swap(set_comprehension &t1, set_comprehension &t2) noexcept
\brief swap overload
std::set< data::variable > find_all_variables(const data::machine_number &x)
bool is_fset_container(const atermpp::aterm &x)
bool is_less_function_symbol(const DataExpression &e)
Recogniser for function <.
Definition standard.h:254
std::ostream & operator<<(std::ostream &out, const data_equation &x)
std::ostream & operator<<(std::ostream &out, const bag_comprehension &x)
std::set< core::identifier_string > find_identifiers(const T &x)
Returns all identifiers that occur in an object.
Definition find.h:361
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
bool is_untyped_sort_variable(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const structured_sort_constructor_argument &x)
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &dom4, const sort_expression &dom5, const sort_expression &dom6, const sort_expression &codomain)
Convenience constructor for function sort with domain size 6.
data_equation_vector function_update_generate_equations_code(const sort_expression &s, const sort_expression &t)
Give all system defined equations for function_update.
bool is_untyped_set_or_bag_comprehension_binder(const atermpp::aterm &x)
std::string pp(const data::where_clause &x, bool arg0)
Definition data.cpp:81
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
Definition data.cpp:90
std::ostream & operator<<(std::ostream &out, const function_sort &x)
bool is_function_update_stable_application(const atermpp::aterm &e)
Recogniser for application of @func_update_stable.
std::set< data::function_symbol > find_function_symbols(const data::data_equation &x)
Definition data.cpp:100
application if_always_else(const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @if_always_else.
std::string pp(const data::bag_container &x, bool arg0)
Definition data.cpp:45
void swap(function_symbol &t1, function_symbol &t2) noexcept
\brief swap overload
std::string pp(const data::alias &x, bool arg0)
Definition data.cpp:39
bool is_if_function_symbol(const DataExpression &e)
Recogniser for function if.
Definition standard.h:214
std::ostream & operator<<(std::ostream &out, const fbag_container &x)
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:98
application greater(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >
Definition standard.h:337
void make_abstraction(atermpp::aterm &result, ARGUMENTS... arguments)
Definition abstraction.h:72
void swap(sort_expression &t1, sort_expression &t2) noexcept
\brief swap overload
std::set< data::variable > find_all_variables(const data::variable_list &x)
Definition data.cpp:97
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set/bag comprehension.
void swap(abstraction &t1, abstraction &t2) noexcept
\brief swap overload
Definition abstraction.h:97
bool is_untyped_data_parameter(const atermpp::aterm &x)
void swap(alias &t1, alias &t2) noexcept
\brief swap overload
Definition alias.h:97
bool is_assignment(const atermpp::aterm &x)
Definition assignment.h:152
std::string pp(const data::structured_sort_constructor &x, bool arg0)
Definition data.cpp:70
std::set< data::sort_expression > find_sort_expressions(const data::sort_expression &x)
Definition data.cpp:92
std::string pp(const data::data_specification &x, bool arg0)
Definition data.cpp:52
std::string pp(const data::data_equation_list &x, bool arg0)
Definition data.cpp:36
void find_data_expressions(const T &x, OutputIterator o)
Returns all data expressions that occur in an object.
Definition find.h:434
std::string pp(const data::fset_container &x, bool arg0)
Definition data.cpp:58
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &codomain)
Convenience constructor for function sort with domain size 3.
std::string pp(const data::sort_expression &x, bool arg0)
Definition data.cpp:68
std::ostream & operator<<(std::ostream &out, const binder_type &x)
Definition binder_type.h:60
std::string pp(const data::untyped_set_or_bag_comprehension &x, bool arg0)
Definition data.cpp:76
void is_not_a_function_update_manual_implementation(data_expression &result, const data_expression &arg0)
The data expression of an application of the function symbol @is_not_an_update.
std::pair< basic_sort_vector, alias_vector > parse_sort_specification(const std::string &text)
Definition data.cpp:251
void swap(lambda_binder &t1, lambda_binder &t2) noexcept
\brief swap overload
data::sort_expression normalize_sorts(const data::sort_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
std::string pp(const data::variable_list &x, bool arg0)
Definition data.cpp:30
std::ostream & operator<<(std::ostream &out, const data_expression &x)
application greater_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >=.
Definition standard.h:374
void find_sort_expressions(const T &x, OutputIterator o)
Writes all sort expressions that occur in an object to an output iterator.
Definition find.h:372
bool is_less_equal_function_symbol(const DataExpression &e)
Recogniser for function <=.
Definition standard.h:291
void make_data_equation(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
bool is_greater_equal_function_symbol(const DataExpression &e)
Recogniser for function >=.
Definition standard.h:365
assignment_vector make_assignment_vector(VariableSequence const &variables, ExpressionSequence const &expressions)
Constructs an assignment_list by pairwise combining a variable and expression.
Definition assignment.h:278
std::set< data::variable > find_free_variables(const data::data_expression_list &x)
Definition data.cpp:99
void swap(untyped_set_or_bag_comprehension &t1, untyped_set_or_bag_comprehension &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const untyped_identifier &x)
implementation_map function_update_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
std::string pp(const machine_number_list &x, bool precedence_aware=true)
std::string pp(const data::data_expression &x, bool arg0)
Definition data.cpp:51
std::string pp(const data::lambda &x, bool arg0)
Definition data.cpp:61
bool is_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a bag comprehension.
std::string pp(const data::fbag_container &x, bool arg0)
Definition data.cpp:55
bool is_set_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set comprehension.
std::ostream & operator<<(std::ostream &out, const function_symbol &x)
std::string max_machine_number_string()
A string representation indicating the maximal machine number + 1.
std::ostream & operator<<(std::ostream &out, const where_clause &x)
bool is_bag_container(const atermpp::aterm &x)
std::string pp(const data::structured_sort_constructor_list &x, bool arg0)
Definition data.cpp:34
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:131
std::string pp(const data::container_sort &x, bool arg0)
Definition data.cpp:48
data::variable_list normalize_sorts(const data::variable_list &x, const data::sort_specification &sortspec)
Definition data.cpp:87
const data_expression_list & variable_list_to_data_expression_list(const variable_list &l)
Transform a variable_list into a data_expression_list.
function_symbol function_update_stable(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @func_update_stable.
bool is_function_update_application(const atermpp::aterm &e)
Recogniser for application of @func_update.
data::data_expression normalize_sorts(const data::data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:85
std::ostream & operator<<(std::ostream &out, const variable &x)
Definition variable.h:96
data_expression_list right_hand_sides(const assignment_list &x)
Returns the right hand sides of an assignment list.
Definition assignment.h:315
void make_is_not_a_function_update(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0)
Make an application of function symbol @is_not_an_update.
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &codomain)
Convenience constructor for function sort with domain size 2.
std::string pp(const data::untyped_sort_variable &x, bool arg0)
Definition data.cpp:79
std::string pp(const data::untyped_data_parameter &x, bool arg0)
Definition data.cpp:72
std::string pp(const data::binder_type &x, bool arg0)
Definition data.cpp:47
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
Definition standard.h:149
bool is_fbag_container(const atermpp::aterm &x)
bool is_lambda(const atermpp::aterm &x)
Returns true if the term t is a lambda abstraction.
const data::variable & undefined_real_variable()
Returns a data variable that corresponds to 'undefined'.
Definition undefined.h:42
bool is_untyped_identifier_assignment(const atermpp::aterm &x)
Definition assignment.h:248
function_symbol_vector function_update_generate_functions_code(const sort_expression &s, const sort_expression &t)
Give all system defined mappings for function_update.
bool is_alias(const atermpp::aterm &x)
Definition alias.h:78
bool is_is_not_a_function_update_function_symbol(const atermpp::aterm &e)
Recogniser for function @is_not_an_update.
std::set< data::variable > find_all_variables(const data::variable &x)
Definition data.cpp:96
void make_exists(atermpp::aterm &result, ARGUMENTS... arguments)
Definition exists.h:61
function_symbol function_update(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @func_update.
bool is_constant(const data_expression &x)
bool is_forall_binder(const atermpp::aterm &x)
const core::identifier_string & function_update_stable_name()
Generate identifier @func_update_stable.
bool search_variable(const T &x, const variable &v)
Returns true if the term has a given variable as subterm.
Definition find.h:455
assignment_list make_assignment_list(const VariableSequence &variables, const ExpressionSequence &expressions)
Converts an iterator range to data_expression_list.
Definition assignment.h:298
bool is_less_application(const DataExpression &e)
Recogniser for application of <.
Definition standard.h:274
void make_structured_sort(atermpp::aterm &t, const ARGUMENTS &... args)
std::set< core::identifier_string > find_identifiers(const data::variable_list &x)
Definition data.cpp:101
std::ostream & operator<<(std::ostream &out, const sort_expression &x)
bool search_variable(const data::data_expression &x, const data::variable &v)
Definition data.cpp:102
const data::data_expression & undefined_data_expression()
Returns a data expression that corresponds to 'undefined'.
Definition undefined.h:58
const data::sort_expression & undefined_sort_expression()
Returns a sort expression that corresponds to 'undefined'.
Definition undefined.h:50
void make_container_sort(atermpp::aterm &t, const ARGUMENTS &... args)
void make_function_sort(atermpp::aterm &t, const ARGUMENTS &... args)
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &dom4, const sort_expression &dom5, const sort_expression &codomain)
Convenience constructor for function sort with domain size 5.
std::string pp(const data::sort_expression_list &x, bool arg0)
Definition data.cpp:24
void make_structured_sort_constructor(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const data::forall_binder &x, bool arg0)
Definition data.cpp:57
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
void make_untyped_possible_sorts(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const data::untyped_possible_sorts &x, bool arg0)
Definition data.cpp:75
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
void swap(machine_number &t1, machine_number &t2) noexcept
\brief swap overload
std::string pp(const data::function_symbol &x, bool arg0)
Definition data.cpp:60
std::ostream & operator<<(std::ostream &out, const set_comprehension &x)
std::set< data::variable > substitution_variables(const mutable_map_substitution<> &sigma)
Definition data.cpp:184
bool is_less_equal_application(const DataExpression &e)
Recogniser for application of <=.
Definition standard.h:311
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
bool is_bag_comprehension_binder(const atermpp::aterm &x)
std::set< data::variable > find_free_variables_with_bound(const T &x, VariableContainer const &bound)
Returns all free variables that occur in an object.
Definition find.h:341
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:205
std::ostream & operator<<(std::ostream &out, const untyped_set_or_bag_comprehension &x)
function_symbol is_not_a_function_update(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @is_not_an_update.
std::string pp(const data::machine_number &x, bool arg0)
Definition data.cpp:64
bool is_equal_to_application(const DataExpression &e)
Recogniser for application of ==.
Definition standard.h:160
void swap(data_expression &t1, data_expression &t2) noexcept
\brief swap overload
void swap(variable &t1, variable &t2) noexcept
\brief swap overload
Definition variable.h:102
std::string pp(const data::assignment_expression &x, bool arg0)
Definition data.cpp:42
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
void swap(untyped_possible_sorts &t1, untyped_possible_sorts &t2) noexcept
\brief swap overload
bool is_sort_expression(const atermpp::aterm &x)
Test for a sort_expression expression.
std::string pp(const data::set_comprehension &x, bool arg0)
Definition data.cpp:65
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:91
void make_untyped_sort_variable(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const data::data_expression_list &x, bool arg0)
Definition data.cpp:26
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:319
expression builder that visits all sub expressions
Definition builder.h:32
void leave(const T &)
Definition builder.h:40
void enter(const T &)
Definition builder.h:35
core::identifier_string parse_Id(const parse_node &node) const
Definition parse.h:231
atermpp::term_list< T > parse_list(const parse_node &node, const std::string &type, const Function &f) const
Definition parse.h:216
default_parser_actions(const parser &parser_)
Definition parse.h:211
std::vector< T > parse_vector(const parse_node &node, const std::string &type, const Function &f) const
Definition parse.h:224
core::identifier_string_list parse_IdList(const parse_node &node) const
Definition parse.h:241
core::identifier_string parse_Number(const parse_node &node) const
Definition parse.h:236
static const atermpp::aterm DataVarIdInit
static const atermpp::aterm SortFSet
static const atermpp::aterm DataVarId
static const atermpp::aterm BindingOperator
static const atermpp::aterm SortArrow
static const atermpp::aterm UntypedSetBagComp
static const atermpp::aterm Lambda
static const atermpp::aterm SortExpr
static const atermpp::aterm SortConsType
static const atermpp::aterm SortId
static const atermpp::aterm UntypedSortsPossible
static const atermpp::aterm Binder
static const atermpp::aterm UntypedSortVariable
static const atermpp::aterm DataEqn
static const atermpp::aterm SortRef
static const atermpp::aterm DataExpr
static const atermpp::aterm UntypedSortUnknown
static const atermpp::aterm SortSet
static const atermpp::aterm Exists
static const atermpp::aterm SortCons
static const atermpp::aterm SortBag
static const atermpp::aterm OpId
static const atermpp::aterm StructProj
static const atermpp::aterm Whr
static const atermpp::aterm UntypedIdentifierAssignment
static const atermpp::aterm SortStruct
static const atermpp::aterm SetComp
static const atermpp::aterm StructCons
static const atermpp::aterm BagComp
static const atermpp::aterm UntypedIdentifier
static const atermpp::aterm SortFBag
static const atermpp::aterm SortList
static const atermpp::aterm WhrDecl
static const atermpp::aterm Forall
static const atermpp::aterm UntypedDataParameter
void operator()(const parse_node &x)
find_and_or(const parser_table &table_)
find_left_merge_merge(const parser_table &table_)
Checks if a node is the binary operation '&&'.
is_and_node(const parser_table &table_)
Checks if a node is of type 'x && (y || z)'.
is_and_or_node(const parser_table &table_)
bool operator()(const parse_node &x)
Checks if a node is the binary operation op.
is_binary_operator_node(const parser_table &table_, const std::string &op_)
Checks if a node is of type 'x ||_ (y || z)'.
is_left_merge_merge(const parser_table &table_)
Checks if a node is the left merge operation '||_'.
is_left_merge_node(const parser_table &table_)
Checks if a node is the merge operation '||'.
is_merge_node(const parser_table &table_)
Checks if a node is the binary operation '||'.
is_or_node(const parser_table &table_)
bool operator()(const parse_node &node) const
Definition parse.h:153
collector(const parser_table &table_, const std::string &type_, Container &container_, const Function &f_)
Definition parse.h:146
set_collector(const parser_table &table_, const std::string &type_, SetContainer &container_, const Function &f_)
Definition parse.h:179
bool operator()(const parse_node &node) const
Definition parse.h:186
visitor(const parser_table &table_, const std::string &type_, const Function &f_)
Definition parse.h:114
const parser_table & table
Definition parse.h:110
bool operator()(const parse_node &node) const
Definition parse.h:120
std::string symbol_name(const parse_node &node) const
Definition parse.h:203
parser_actions(const parser &parser_)
Definition parse.h:85
void traverse(const parse_node &node, const Function &f) const
Definition parse.h:91
const parser & m_parser
Definition parse.h:83
set_collector< SetContainer, Function > make_set_collector(const parser_table &table, const std::string &type, SetContainer &container, const Function &f) const
Definition parse.h:198
visitor< Function > make_visitor(const parser_table &table, const std::string &type, const Function &f) const
Definition parse.h:132
collector< Container, Function > make_collector(const parser_table &table, const std::string &type, Container &container, const Function &f) const
Definition parse.h:165
void apply(T &result, const argument_type &x)
Definition builder.h:173
update_apply_builder(const Function &f)
Definition builder.h:179
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:511
void apply(T &result, const data::machine_number &x)
Definition builder.h:445
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:471
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:578
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:519
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:454
void apply(T &result, const data::data_equation &x)
Definition builder.h:527
void apply(T &result, const data::function_symbol &x)
Definition builder.h:416
void apply(T &result, const data::assignment &x)
Definition builder.h:463
void apply(T &result, const data::abstraction &x)
Definition builder.h:593
void apply(T &result, const data::forall &x)
Definition builder.h:479
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:535
void apply(T &result, const data::exists &x)
Definition builder.h:487
void apply(T &result, const data::where_clause &x)
Definition builder.h:437
void apply(T &result, const data::application &x)
Definition builder.h:425
void apply(T &result, const data::variable &x)
Definition builder.h:407
void apply(T &result, const data::data_expression &x)
Definition builder.h:543
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:503
void apply(T &result, const data::lambda &x)
Definition builder.h:495
Maintains a multiset of bound data variables during traversal.
Definition add_binding.h:30
void decrease_bind_count(const assignment_list &assignments)
Definition add_binding.h:47
void leave(const data::exists &x)
Definition add_binding.h:80
void enter(const data::forall &x)
Definition add_binding.h:65
void leave(const data::forall &x)
Definition add_binding.h:70
void leave(const data::data_equation &x)
void enter(const data::set_comprehension &x)
Definition add_binding.h:95
void enter(const data::data_equation &x)
void leave(const data::set_comprehension &x)
void enter(const data::exists &x)
Definition add_binding.h:75
void leave(const data::bag_comprehension &x)
void enter(const data::lambda &x)
Definition add_binding.h:85
void leave(const data::untyped_set_or_bag_comprehension &x)
void increase_bind_count(const assignment_list &assignments)
Definition add_binding.h:39
void enter(const data::bag_comprehension &x)
void leave(const data::lambda &x)
Definition add_binding.h:90
void enter(const data::untyped_set_or_bag_comprehension &x)
void enter(const data::where_clause &x)
Definition add_binding.h:55
void leave(const data::where_clause &x)
Definition add_binding.h:60
void apply(T &result, const data::where_clause &x)
void apply(const data::where_clause &x)
void apply(T &result, const data::assignment &x)
Definition builder.h:108
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:207
void apply(T &result, const data::structured_sort_constructor_argument &x)
Definition builder.h:231
void apply(T &result, const data::container_sort &x)
Definition builder.h:133
void apply(T &result, const data::alias &x)
Definition builder.h:247
void apply(T &result, const data::exists &x)
Definition builder.h:191
void apply(T &result, const data::machine_number &x)
Definition builder.h:90
void apply(T &result, const data::function_symbol &x)
Definition builder.h:62
void apply(T &result, const data::untyped_possible_sorts &x)
Definition builder.h:166
void apply(T &result, const data::forall &x)
Definition builder.h:183
void apply(T &result, const data::basic_sort &x)
Definition builder.h:124
void apply(T &result, const data::data_equation &x)
Definition builder.h:255
void apply(T &result, const data::untyped_sort &x)
Definition builder.h:157
void apply(T &result, const data::abstraction &x)
Definition builder.h:356
void apply(T &result, const data::application &x)
Definition builder.h:70
void apply(T &result, const data::variable &x)
Definition builder.h:54
void apply(T &result, const data::structured_sort &x)
Definition builder.h:141
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:116
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:263
void apply(T &result, const data::function_sort &x)
Definition builder.h:149
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:99
void apply(T &result, const data::structured_sort_constructor &x)
Definition builder.h:239
void apply(T &result, const data::lambda &x)
Definition builder.h:199
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:223
void apply(T &result, const data::where_clause &x)
Definition builder.h:82
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:306
void apply(T &result, const data::data_expression &x)
Definition builder.h:271
void apply(T &result, const data::sort_expression &x)
Definition builder.h:321
void apply(T &result, const data::untyped_sort_variable &x)
Definition builder.h:174
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:215
void apply(const data::function_symbol &x)
Definition traverser.h:377
void apply(const data::set_comprehension &x)
Definition traverser.h:449
void apply(const data::untyped_identifier &x)
Definition traverser.h:407
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:463
void apply(const data::application &x)
Definition traverser.h:384
void apply(const data::forall &x)
Definition traverser.h:428
void apply(const data::data_equation &x)
Definition traverser.h:470
void apply(const data::exists &x)
Definition traverser.h:435
void apply(const data::lambda &x)
Definition traverser.h:442
void apply(const data::machine_number &x)
Definition traverser.h:400
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:421
void apply(const data::data_expression &x)
Definition traverser.h:486
void apply(const data::where_clause &x)
Definition traverser.h:392
void apply(const data::bag_comprehension &x)
Definition traverser.h:456
void apply(const data::abstraction &x)
Definition traverser.h:534
void apply(const data::assignment_expression &x)
Definition traverser.h:520
void apply(const data::variable &x)
Definition traverser.h:370
void apply(const data::assignment &x)
Definition traverser.h:414
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:479
void apply(const data::untyped_possible_sorts &x)
Definition traverser.h:900
void apply(const data::structured_sort_constructor_argument &x)
Definition traverser.h:962
void apply(const data::application &x)
Definition traverser.h:818
void apply(const data::untyped_sort_variable &x)
Definition traverser.h:907
void apply(const data::basic_sort &x)
Definition traverser.h:864
void apply(const data::bag_comprehension &x)
Definition traverser.h:946
void apply(const data::assignment_expression &x)
Definition traverser.h:1039
void apply(const data::untyped_sort &x)
Definition traverser.h:893
void apply(const data::assignment &x)
Definition traverser.h:848
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:954
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:997
void apply(const data::structured_sort &x)
Definition traverser.h:878
void apply(const data::function_sort &x)
Definition traverser.h:885
void apply(const data::data_equation &x)
Definition traverser.h:987
void apply(const data::container_sort &x)
Definition traverser.h:871
void apply(const data::machine_number &x)
Definition traverser.h:834
void apply(const data::abstraction &x)
Definition traverser.h:1087
void apply(const data::structured_sort_constructor &x)
Definition traverser.h:970
void apply(const data::variable &x)
Definition traverser.h:802
void apply(const data::function_symbol &x)
Definition traverser.h:810
void apply(const data::untyped_identifier &x)
Definition traverser.h:841
void apply(const data::data_expression &x)
Definition traverser.h:1005
void apply(const data::set_comprehension &x)
Definition traverser.h:938
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:856
void apply(const data::sort_expression &x)
Definition traverser.h:1053
void apply(const data::where_clause &x)
Definition traverser.h:826
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:97
void apply(const data::assignment &x)
Definition traverser.h:89
void apply(const data::sort_expression &x)
Definition traverser.h:288
void apply(const data::where_clause &x)
Definition traverser.h:67
void apply(const data::data_expression &x)
Definition traverser.h:240
void apply(const data::lambda &x)
Definition traverser.h:170
void apply(const data::basic_sort &x)
Definition traverser.h:104
void apply(const data::variable &x)
Definition traverser.h:45
void apply(const data::untyped_possible_sorts &x)
Definition traverser.h:140
void apply(const data::untyped_identifier &x)
Definition traverser.h:82
void apply(const data::untyped_sort_variable &x)
Definition traverser.h:147
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:194
void apply(const data::forall &x)
Definition traverser.h:154
void apply(const data::application &x)
Definition traverser.h:59
void apply(const data::structured_sort_constructor_argument &x)
Definition traverser.h:202
void apply(const data::structured_sort_constructor &x)
Definition traverser.h:209
void apply(const data::untyped_sort &x)
Definition traverser.h:133
void apply(const data::machine_number &x)
Definition traverser.h:75
void apply(const data::function_sort &x)
Definition traverser.h:125
void apply(const data::container_sort &x)
Definition traverser.h:111
void apply(const data::set_comprehension &x)
Definition traverser.h:178
void apply(const data::data_equation &x)
Definition traverser.h:223
void apply(const data::structured_sort &x)
Definition traverser.h:118
void apply(const data::assignment_expression &x)
Definition traverser.h:274
void apply(const data::bag_comprehension &x)
Definition traverser.h:186
void apply(const data::exists &x)
Definition traverser.h:162
void apply(const data::abstraction &x)
Definition traverser.h:322
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:233
void apply(const data::function_symbol &x)
Definition traverser.h:52
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:681
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:634
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:699
void apply(const data::data_expression &x)
Definition traverser.h:706
void apply(const data::bag_comprehension &x)
Definition traverser.h:673
void apply(const data::data_equation &x)
Definition traverser.h:689
void apply(const data::where_clause &x)
Definition traverser.h:604
void apply(const data::set_comprehension &x)
Definition traverser.h:665
void apply(const data::exists &x)
Definition traverser.h:649
void apply(const data::untyped_identifier &x)
Definition traverser.h:619
void apply(const data::variable &x)
Definition traverser.h:582
void apply(const data::abstraction &x)
Definition traverser.h:754
void apply(const data::forall &x)
Definition traverser.h:641
void apply(const data::assignment_expression &x)
Definition traverser.h:740
void apply(const data::assignment &x)
Definition traverser.h:626
void apply(const data::application &x)
Definition traverser.h:596
void apply(const data::function_symbol &x)
Definition traverser.h:589
void apply(const data::lambda &x)
Definition traverser.h:657
void apply(const data::machine_number &x)
Definition traverser.h:612
void apply(T &result, const data::abstraction &x)
Definition builder.h:829
void apply(T &result, const data::application &x)
Definition builder.h:661
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:771
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:690
void apply(T &result, const data::data_expression &x)
Definition builder.h:779
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:814
void apply(T &result, const data::where_clause &x)
Definition builder.h:673
void apply(T &result, const data::forall &x)
Definition builder.h:715
void apply(T &result, const data::function_symbol &x)
Definition builder.h:652
void apply(T &result, const data::exists &x)
Definition builder.h:723
void apply(T &result, const data::lambda &x)
Definition builder.h:731
void apply(T &result, const data::variable &x)
Definition builder.h:643
void apply(T &result, const data::assignment &x)
Definition builder.h:699
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:707
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:755
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:739
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:747
void apply(T &result, const data::machine_number &x)
Definition builder.h:681
void apply(T &result, const data::data_equation &x)
Definition builder.h:763
data_expression make_untyped_set_or_bag_comprehension(const variable &v, const data_expression &x) const
Definition parse_impl.h:142
data::variable_list parse_VarsDeclList(const core::parse_node &node) const
Definition parse_impl.h:201
data::data_expression_list parse_DataExprList(const core::parse_node &node) const
Definition parse_impl.h:284
data_expression make_list_enumeration(const data_expression_list &x) const
Definition parse_impl.h:147
data_expression make_function_update(const data_expression &x, const data_expression &y, const data_expression &z) const
Definition parse_impl.h:165
data_expression make_set_enumeration(const data_expression_list &x) const
Definition parse_impl.h:153
data::sort_expression_list get_sorts(const ExpressionContainer &x) const
Definition parse_impl.h:171
data_expression_actions(const core::parser &parser_)
Definition parse_impl.h:138
bool callback_VarsDecl(const core::parse_node &node, variable_vector &result) const
Definition parse_impl.h:186
data::variable parse_VarDecl(const core::parse_node &node) const
Definition parse_impl.h:181
data::untyped_identifier_assignment parse_Assignment(const core::parse_node &node) const
Definition parse_impl.h:274
data::data_expression parse_DataValExpr(const core::parse_node &node) const
Definition parse_impl.h:269
data::data_expression_list parse_BagEnumEltList(const core::parse_node &node) const
Definition parse_impl.h:289
data::untyped_identifier_assignment_list parse_AssignmentList(const core::parse_node &node) const
Definition parse_impl.h:279
data_expression make_bag_enumeration(const data_expression_list &x) const
Definition parse_impl.h:159
data::data_expression parse_DataExprUnit(const core::parse_node &node) const
Definition parse_impl.h:255
data::data_expression parse_DataExpr(const core::parse_node &node) const
Definition parse_impl.h:208
bool callback_IdsDecl(const core::parse_node &node, function_symbol_vector &result) const
Definition parse_impl.h:338
data::variable_list parse_GlobVarSpec(const core::parse_node &node) const
Definition parse_impl.h:370
data_specification_actions(const core::parser &parser_)
Definition parse_impl.h:297
data::function_symbol_vector parse_MapSpec(const core::parse_node &node) const
Definition parse_impl.h:365
data::data_equation_vector parse_EqnDeclList(const core::parse_node &node, const variable_list &variables) const
Definition parse_impl.h:396
data::variable_list parse_VarSpec(const core::parse_node &node) const
Definition parse_impl.h:375
std::vector< atermpp::aterm > parse_SortDeclList(const core::parse_node &node) const
Definition parse_impl.h:326
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
Definition parse_impl.h:458
bool callback_SortDecl(const core::parse_node &node, std::vector< atermpp::aterm > &result) const
Definition parse_impl.h:301
data::data_equation_vector parse_EqnSpec(const core::parse_node &node) const
Definition parse_impl.h:403
data::function_symbol_vector parse_IdsDeclList(const core::parse_node &node) const
Definition parse_impl.h:353
bool callback_DataSpecElement(const core::parse_node &node, untyped_data_specification &result) const
Definition parse_impl.h:410
bool callback_EqnDecl(const core::parse_node &node, const variable_list &variables, data_equation_vector &result) const
Definition parse_impl.h:380
std::vector< atermpp::aterm > parse_SortSpec(const core::parse_node &node) const
Definition parse_impl.h:333
data::function_symbol_vector parse_ConsSpec(const core::parse_node &node) const
Definition parse_impl.h:360
normalize_sorts_function(const sort_specification &sort_spec)
sort_expression operator()(const sort_expression &e) const
Normalise sorts.
const std::map< sort_expression, sort_expression > & m_normalised_aliases
data::structured_sort_constructor parse_ConstrDecl(const core::parse_node &node) const
Definition parse_impl.h:93
data::sort_expression parse_SortExpr(const core::parse_node &node, data::sort_expression_list *product=nullptr) const
Definition parse_impl.h:32
data::structured_sort_constructor_list parse_ConstrDeclList(const core::parse_node &node) const
Definition parse_impl.h:113
data::sort_expression_list parse_SortProduct(const core::parse_node &node) const
Definition parse_impl.h:84
data::sort_expression_list parse_SortExpr_as_SortProduct(const core::parse_node &node) const
Definition parse_impl.h:73
data::structured_sort_constructor_argument_list parse_ProjDeclList(const core::parse_node &node) const
Definition parse_impl.h:130
sort_expression_actions(const core::parser &parser_)
Definition parse_impl.h:28
data::structured_sort_constructor_argument parse_ProjDecl(const core::parse_node &node) const
Definition parse_impl.h:118
sort_expression operator()(structured_sort_constructor_argument const &s) const
\brief Builder class
Definition builder.h:864
\brief Traverser class
Definition traverser.h:789
std::size_t operator()(const mcrl2::data::container_type &v) const
std::size_t operator()(const mcrl2::data::data_expression &v) const
std::size_t operator()(const mcrl2::data::function_sort &v) const
std::size_t operator()(const mcrl2::data::sort_expression &x) const
std::size_t operator()(const mcrl2::data::variable &v) const
Definition variable.h:128