Line data Source code
1 : // Author(s): Jeroen Keiren
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/data/pos.h
10 : /// \brief The standard sort pos.
11 : ///
12 : /// This file was generated from the data sort specification
13 : /// mcrl2/data/build/pos.spec.
14 :
15 : #ifndef MCRL2_DATA_POS_H
16 : #define MCRL2_DATA_POS_H
17 :
18 : #include "functional" // std::function
19 : #include "mcrl2/utilities/exception.h"
20 : #include "mcrl2/data/basic_sort.h"
21 : #include "mcrl2/data/function_sort.h"
22 : #include "mcrl2/data/function_symbol.h"
23 : #include "mcrl2/data/application.h"
24 : #include "mcrl2/data/data_equation.h"
25 : #include "mcrl2/data/standard.h"
26 : #include "mcrl2/data/bool.h"
27 :
28 : namespace mcrl2 {
29 :
30 : namespace data {
31 :
32 : /// \brief Namespace for system defined sort pos.
33 : namespace sort_pos {
34 :
35 : inline
36 118 : const core::identifier_string& pos_name()
37 : {
38 118 : static core::identifier_string pos_name = core::identifier_string("Pos");
39 118 : return pos_name;
40 : }
41 :
42 : /// \brief Constructor for sort expression Pos.
43 : /// \return Sort expression Pos.
44 : inline
45 1612267 : const basic_sort& pos()
46 : {
47 1612267 : static basic_sort pos = basic_sort(pos_name());
48 1612267 : return pos;
49 : }
50 :
51 : /// \brief Recogniser for sort expression Pos
52 : /// \param e A sort expression
53 : /// \return true iff e == pos()
54 : inline
55 206695 : bool is_pos(const sort_expression& e)
56 : {
57 206695 : if (is_basic_sort(e))
58 : {
59 39620 : return basic_sort(e) == pos();
60 : }
61 167075 : return false;
62 : }
63 :
64 :
65 : /// \brief Generate identifier \@c1.
66 : /// \return Identifier \@c1.
67 : inline
68 115 : const core::identifier_string& c1_name()
69 : {
70 115 : static core::identifier_string c1_name = core::identifier_string("@c1");
71 115 : return c1_name;
72 : }
73 :
74 : /// \brief Constructor for function symbol \@c1.
75 :
76 : /// \return Function symbol c1.
77 : inline
78 555992 : const function_symbol& c1()
79 : {
80 555992 : static function_symbol c1(c1_name(), pos());
81 555992 : return c1;
82 : }
83 :
84 : /// \brief Recogniser for function \@c1.
85 : /// \param e A data expression.
86 : /// \return true iff e is the function symbol matching \@c1.
87 : inline
88 62903 : bool is_c1_function_symbol(const atermpp::aterm_appl& e)
89 : {
90 62903 : if (is_function_symbol(e))
91 : {
92 57093 : return atermpp::down_cast<function_symbol>(e) == c1();
93 : }
94 5810 : return false;
95 : }
96 :
97 : /// \brief Generate identifier \@cDub.
98 : /// \return Identifier \@cDub.
99 : inline
100 114 : const core::identifier_string& cdub_name()
101 : {
102 114 : static core::identifier_string cdub_name = core::identifier_string("@cDub");
103 114 : return cdub_name;
104 : }
105 :
106 : /// \brief Constructor for function symbol \@cDub.
107 :
108 : /// \return Function symbol cdub.
109 : inline
110 855400 : const function_symbol& cdub()
111 : {
112 855400 : static function_symbol cdub(cdub_name(), make_function_sort_(sort_bool::bool_(), pos(), pos()));
113 855400 : return cdub;
114 : }
115 :
116 : /// \brief Recogniser for function \@cDub.
117 : /// \param e A data expression.
118 : /// \return true iff e is the function symbol matching \@cDub.
119 : inline
120 60447 : bool is_cdub_function_symbol(const atermpp::aterm_appl& e)
121 : {
122 60447 : if (is_function_symbol(e))
123 : {
124 59605 : return atermpp::down_cast<function_symbol>(e) == cdub();
125 : }
126 842 : return false;
127 : }
128 :
129 : /// \brief Application of function symbol \@cDub.
130 :
131 : /// \param arg0 A data expression.
132 : /// \param arg1 A data expression.
133 : /// \return Application of \@cDub to a number of arguments.
134 : inline
135 780733 : application cdub(const data_expression& arg0, const data_expression& arg1)
136 : {
137 780733 : return sort_pos::cdub()(arg0, arg1);
138 : }
139 :
140 : /// \brief Make an application of function symbol \@cDub.
141 : /// \param result The data expression where the \@cDub expression is put.
142 :
143 : /// \param arg0 A data expression.
144 : /// \param arg1 A data expression.
145 : inline
146 : void make_cdub(data_expression& result, const data_expression& arg0, const data_expression& arg1)
147 : {
148 : make_application(result, sort_pos::cdub(),arg0, arg1);
149 : }
150 :
151 : /// \brief Recogniser for application of \@cDub.
152 : /// \param e A data expression.
153 : /// \return true iff e is an application of function symbol cdub to a
154 : /// number of arguments.
155 : inline
156 64797 : bool is_cdub_application(const atermpp::aterm_appl& e)
157 : {
158 64797 : return is_application(e) && is_cdub_function_symbol(atermpp::down_cast<application>(e).head());
159 : }
160 : /// \brief Give all system defined constructors for pos.
161 : /// \return All system defined constructors for pos.
162 : inline
163 10484 : function_symbol_vector pos_generate_constructors_code()
164 : {
165 10484 : function_symbol_vector result;
166 10484 : result.push_back(sort_pos::c1());
167 10484 : result.push_back(sort_pos::cdub());
168 :
169 10484 : return result;
170 0 : }
171 : /// \brief Give all defined constructors which can be used in mCRL2 specs for pos.
172 : /// \return All system defined constructors that can be used in an mCRL2 specification for pos.
173 : inline
174 4578 : function_symbol_vector pos_mCRL2_usable_constructors()
175 : {
176 4578 : function_symbol_vector result;
177 4578 : result.push_back(sort_pos::c1());
178 4578 : result.push_back(sort_pos::cdub());
179 :
180 4578 : return result;
181 0 : }
182 : // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
183 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
184 : /// \brief Give all system defined constructors which have an implementation in C++ and not in rewrite rules for pos.
185 : /// \return All system defined constructors that are to be implemented in C++ for pos.
186 : inline
187 10484 : implementation_map pos_cpp_implementable_constructors()
188 : {
189 10484 : implementation_map result;
190 10484 : return result;
191 : }
192 :
193 : /// \brief Generate identifier max.
194 : /// \return Identifier max.
195 : inline
196 113 : const core::identifier_string& maximum_name()
197 : {
198 113 : static core::identifier_string maximum_name = core::identifier_string("max");
199 113 : return maximum_name;
200 : }
201 :
202 : /// \brief Constructor for function symbol max.
203 :
204 : /// \return Function symbol maximum.
205 : inline
206 25548 : const function_symbol& maximum()
207 : {
208 25548 : static function_symbol maximum(maximum_name(), make_function_sort_(pos(), pos(), pos()));
209 25548 : return maximum;
210 : }
211 :
212 : /// \brief Recogniser for function max.
213 : /// \param e A data expression.
214 : /// \return true iff e is the function symbol matching max.
215 : inline
216 0 : bool is_maximum_function_symbol(const atermpp::aterm_appl& e)
217 : {
218 0 : if (is_function_symbol(e))
219 : {
220 0 : return atermpp::down_cast<function_symbol>(e) == maximum();
221 : }
222 0 : return false;
223 : }
224 :
225 : /// \brief Application of function symbol max.
226 :
227 : /// \param arg0 A data expression.
228 : /// \param arg1 A data expression.
229 : /// \return Application of max to a number of arguments.
230 : inline
231 10486 : application maximum(const data_expression& arg0, const data_expression& arg1)
232 : {
233 10486 : return sort_pos::maximum()(arg0, arg1);
234 : }
235 :
236 : /// \brief Make an application of function symbol max.
237 : /// \param result The data expression where the max expression is put.
238 :
239 : /// \param arg0 A data expression.
240 : /// \param arg1 A data expression.
241 : inline
242 : void make_maximum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
243 : {
244 : make_application(result, sort_pos::maximum(),arg0, arg1);
245 : }
246 :
247 : /// \brief Recogniser for application of max.
248 : /// \param e A data expression.
249 : /// \return true iff e is an application of function symbol maximum to a
250 : /// number of arguments.
251 : inline
252 0 : bool is_maximum_application(const atermpp::aterm_appl& e)
253 : {
254 0 : return is_application(e) && is_maximum_function_symbol(atermpp::down_cast<application>(e).head());
255 : }
256 :
257 : /// \brief Generate identifier min.
258 : /// \return Identifier min.
259 : inline
260 113 : const core::identifier_string& minimum_name()
261 : {
262 113 : static core::identifier_string minimum_name = core::identifier_string("min");
263 113 : return minimum_name;
264 : }
265 :
266 : /// \brief Constructor for function symbol min.
267 :
268 : /// \return Function symbol minimum.
269 : inline
270 25548 : const function_symbol& minimum()
271 : {
272 25548 : static function_symbol minimum(minimum_name(), make_function_sort_(pos(), pos(), pos()));
273 25548 : return minimum;
274 : }
275 :
276 : /// \brief Recogniser for function min.
277 : /// \param e A data expression.
278 : /// \return true iff e is the function symbol matching min.
279 : inline
280 0 : bool is_minimum_function_symbol(const atermpp::aterm_appl& e)
281 : {
282 0 : if (is_function_symbol(e))
283 : {
284 0 : return atermpp::down_cast<function_symbol>(e) == minimum();
285 : }
286 0 : return false;
287 : }
288 :
289 : /// \brief Application of function symbol min.
290 :
291 : /// \param arg0 A data expression.
292 : /// \param arg1 A data expression.
293 : /// \return Application of min to a number of arguments.
294 : inline
295 10486 : application minimum(const data_expression& arg0, const data_expression& arg1)
296 : {
297 10486 : return sort_pos::minimum()(arg0, arg1);
298 : }
299 :
300 : /// \brief Make an application of function symbol min.
301 : /// \param result The data expression where the min expression is put.
302 :
303 : /// \param arg0 A data expression.
304 : /// \param arg1 A data expression.
305 : inline
306 : void make_minimum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
307 : {
308 : make_application(result, sort_pos::minimum(),arg0, arg1);
309 : }
310 :
311 : /// \brief Recogniser for application of min.
312 : /// \param e A data expression.
313 : /// \return true iff e is an application of function symbol minimum to a
314 : /// number of arguments.
315 : inline
316 0 : bool is_minimum_application(const atermpp::aterm_appl& e)
317 : {
318 0 : return is_application(e) && is_minimum_function_symbol(atermpp::down_cast<application>(e).head());
319 : }
320 :
321 : /// \brief Generate identifier succ.
322 : /// \return Identifier succ.
323 : inline
324 113 : const core::identifier_string& succ_name()
325 : {
326 113 : static core::identifier_string succ_name = core::identifier_string("succ");
327 113 : return succ_name;
328 : }
329 :
330 : /// \brief Constructor for function symbol succ.
331 :
332 : /// \return Function symbol succ.
333 : inline
334 224745 : const function_symbol& succ()
335 : {
336 224745 : static function_symbol succ(succ_name(), make_function_sort_(pos(), pos()));
337 224745 : return succ;
338 : }
339 :
340 : /// \brief Recogniser for function succ.
341 : /// \param e A data expression.
342 : /// \return true iff e is the function symbol matching succ.
343 : inline
344 : bool is_succ_function_symbol(const atermpp::aterm_appl& e)
345 : {
346 : if (is_function_symbol(e))
347 : {
348 : return atermpp::down_cast<function_symbol>(e) == succ();
349 : }
350 : return false;
351 : }
352 :
353 : /// \brief Application of function symbol succ.
354 :
355 : /// \param arg0 A data expression.
356 : /// \return Application of succ to a number of arguments.
357 : inline
358 209683 : application succ(const data_expression& arg0)
359 : {
360 209683 : return sort_pos::succ()(arg0);
361 : }
362 :
363 : /// \brief Make an application of function symbol succ.
364 : /// \param result The data expression where the succ expression is put.
365 :
366 : /// \param arg0 A data expression.
367 : inline
368 : void make_succ(data_expression& result, const data_expression& arg0)
369 : {
370 : make_application(result, sort_pos::succ(),arg0);
371 : }
372 :
373 : /// \brief Recogniser for application of succ.
374 : /// \param e A data expression.
375 : /// \return true iff e is an application of function symbol succ to a
376 : /// number of arguments.
377 : inline
378 : bool is_succ_application(const atermpp::aterm_appl& e)
379 : {
380 : return is_application(e) && is_succ_function_symbol(atermpp::down_cast<application>(e).head());
381 : }
382 :
383 : /// \brief Generate identifier \@pospred.
384 : /// \return Identifier \@pospred.
385 : inline
386 113 : const core::identifier_string& pos_predecessor_name()
387 : {
388 113 : static core::identifier_string pos_predecessor_name = core::identifier_string("@pospred");
389 113 : return pos_predecessor_name;
390 : }
391 :
392 : /// \brief Constructor for function symbol \@pospred.
393 :
394 : /// \return Function symbol pos_predecessor.
395 : inline
396 109418 : const function_symbol& pos_predecessor()
397 : {
398 109418 : static function_symbol pos_predecessor(pos_predecessor_name(), make_function_sort_(pos(), pos()));
399 109418 : return pos_predecessor;
400 : }
401 :
402 : /// \brief Recogniser for function \@pospred.
403 : /// \param e A data expression.
404 : /// \return true iff e is the function symbol matching \@pospred.
405 : inline
406 : bool is_pos_predecessor_function_symbol(const atermpp::aterm_appl& e)
407 : {
408 : if (is_function_symbol(e))
409 : {
410 : return atermpp::down_cast<function_symbol>(e) == pos_predecessor();
411 : }
412 : return false;
413 : }
414 :
415 : /// \brief Application of function symbol \@pospred.
416 :
417 : /// \param arg0 A data expression.
418 : /// \return Application of \@pospred to a number of arguments.
419 : inline
420 94356 : application pos_predecessor(const data_expression& arg0)
421 : {
422 94356 : return sort_pos::pos_predecessor()(arg0);
423 : }
424 :
425 : /// \brief Make an application of function symbol \@pospred.
426 : /// \param result The data expression where the \@pospred expression is put.
427 :
428 : /// \param arg0 A data expression.
429 : inline
430 : void make_pos_predecessor(data_expression& result, const data_expression& arg0)
431 : {
432 : make_application(result, sort_pos::pos_predecessor(),arg0);
433 : }
434 :
435 : /// \brief Recogniser for application of \@pospred.
436 : /// \param e A data expression.
437 : /// \return true iff e is an application of function symbol pos_predecessor to a
438 : /// number of arguments.
439 : inline
440 : bool is_pos_predecessor_application(const atermpp::aterm_appl& e)
441 : {
442 : return is_application(e) && is_pos_predecessor_function_symbol(atermpp::down_cast<application>(e).head());
443 : }
444 :
445 : /// \brief Generate identifier +.
446 : /// \return Identifier +.
447 : inline
448 113 : const core::identifier_string& plus_name()
449 : {
450 113 : static core::identifier_string plus_name = core::identifier_string("+");
451 113 : return plus_name;
452 : }
453 :
454 : /// \brief Constructor for function symbol +.
455 :
456 : /// \return Function symbol plus.
457 : inline
458 68908 : const function_symbol& plus()
459 : {
460 68908 : static function_symbol plus(plus_name(), make_function_sort_(pos(), pos(), pos()));
461 68908 : return plus;
462 : }
463 :
464 : /// \brief Recogniser for function +.
465 : /// \param e A data expression.
466 : /// \return true iff e is the function symbol matching +.
467 : inline
468 44568 : bool is_plus_function_symbol(const atermpp::aterm_appl& e)
469 : {
470 44568 : if (is_function_symbol(e))
471 : {
472 43334 : return atermpp::down_cast<function_symbol>(e) == plus();
473 : }
474 1234 : return false;
475 : }
476 :
477 : /// \brief Application of function symbol +.
478 :
479 : /// \param arg0 A data expression.
480 : /// \param arg1 A data expression.
481 : /// \return Application of + to a number of arguments.
482 : inline
483 10512 : application plus(const data_expression& arg0, const data_expression& arg1)
484 : {
485 10512 : return sort_pos::plus()(arg0, arg1);
486 : }
487 :
488 : /// \brief Make an application of function symbol +.
489 : /// \param result The data expression where the + expression is put.
490 :
491 : /// \param arg0 A data expression.
492 : /// \param arg1 A data expression.
493 : inline
494 : void make_plus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
495 : {
496 : make_application(result, sort_pos::plus(),arg0, arg1);
497 : }
498 :
499 : /// \brief Recogniser for application of +.
500 : /// \param e A data expression.
501 : /// \return true iff e is an application of function symbol plus to a
502 : /// number of arguments.
503 : inline
504 44972 : bool is_plus_application(const atermpp::aterm_appl& e)
505 : {
506 44972 : return is_application(e) && is_plus_function_symbol(atermpp::down_cast<application>(e).head());
507 : }
508 :
509 : /// \brief Generate identifier \@addc.
510 : /// \return Identifier \@addc.
511 : inline
512 113 : const core::identifier_string& add_with_carry_name()
513 : {
514 113 : static core::identifier_string add_with_carry_name = core::identifier_string("@addc");
515 113 : return add_with_carry_name;
516 : }
517 :
518 : /// \brief Constructor for function symbol \@addc.
519 :
520 : /// \return Function symbol add_with_carry.
521 : inline
522 201642 : const function_symbol& add_with_carry()
523 : {
524 201642 : static function_symbol add_with_carry(add_with_carry_name(), make_function_sort_(sort_bool::bool_(), pos(), pos(), pos()));
525 201642 : return add_with_carry;
526 : }
527 :
528 : /// \brief Recogniser for function \@addc.
529 : /// \param e A data expression.
530 : /// \return true iff e is the function symbol matching \@addc.
531 : inline
532 26543 : bool is_add_with_carry_function_symbol(const atermpp::aterm_appl& e)
533 : {
534 26543 : if (is_function_symbol(e))
535 : {
536 25701 : return atermpp::down_cast<function_symbol>(e) == add_with_carry();
537 : }
538 842 : return false;
539 : }
540 :
541 : /// \brief Application of function symbol \@addc.
542 :
543 : /// \param arg0 A data expression.
544 : /// \param arg1 A data expression.
545 : /// \param arg2 A data expression.
546 : /// \return Application of \@addc to a number of arguments.
547 : inline
548 160879 : application add_with_carry(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
549 : {
550 160879 : return sort_pos::add_with_carry()(arg0, arg1, arg2);
551 : }
552 :
553 : /// \brief Make an application of function symbol \@addc.
554 : /// \param result The data expression where the \@addc expression is put.
555 :
556 : /// \param arg0 A data expression.
557 : /// \param arg1 A data expression.
558 : /// \param arg2 A data expression.
559 : inline
560 : void make_add_with_carry(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
561 : {
562 : make_application(result, sort_pos::add_with_carry(),arg0, arg1, arg2);
563 : }
564 :
565 : /// \brief Recogniser for application of \@addc.
566 : /// \param e A data expression.
567 : /// \return true iff e is an application of function symbol add_with_carry to a
568 : /// number of arguments.
569 : inline
570 26543 : bool is_add_with_carry_application(const atermpp::aterm_appl& e)
571 : {
572 26543 : return is_application(e) && is_add_with_carry_function_symbol(atermpp::down_cast<application>(e).head());
573 : }
574 :
575 : /// \brief Generate identifier *.
576 : /// \return Identifier *.
577 : inline
578 113 : const core::identifier_string& times_name()
579 : {
580 113 : static core::identifier_string times_name = core::identifier_string("*");
581 113 : return times_name;
582 : }
583 :
584 : /// \brief Constructor for function symbol *.
585 :
586 : /// \return Function symbol times.
587 : inline
588 124173 : const function_symbol& times()
589 : {
590 124173 : static function_symbol times(times_name(), make_function_sort_(pos(), pos(), pos()));
591 124173 : return times;
592 : }
593 :
594 : /// \brief Recogniser for function *.
595 : /// \param e A data expression.
596 : /// \return true iff e is the function symbol matching *.
597 : inline
598 26079 : bool is_times_function_symbol(const atermpp::aterm_appl& e)
599 : {
600 26079 : if (is_function_symbol(e))
601 : {
602 25237 : return atermpp::down_cast<function_symbol>(e) == times();
603 : }
604 842 : return false;
605 : }
606 :
607 : /// \brief Application of function symbol *.
608 :
609 : /// \param arg0 A data expression.
610 : /// \param arg1 A data expression.
611 : /// \return Application of * to a number of arguments.
612 : inline
613 83874 : application times(const data_expression& arg0, const data_expression& arg1)
614 : {
615 83874 : return sort_pos::times()(arg0, arg1);
616 : }
617 :
618 : /// \brief Make an application of function symbol *.
619 : /// \param result The data expression where the * expression is put.
620 :
621 : /// \param arg0 A data expression.
622 : /// \param arg1 A data expression.
623 : inline
624 : void make_times(data_expression& result, const data_expression& arg0, const data_expression& arg1)
625 : {
626 : make_application(result, sort_pos::times(),arg0, arg1);
627 : }
628 :
629 : /// \brief Recogniser for application of *.
630 : /// \param e A data expression.
631 : /// \return true iff e is an application of function symbol times to a
632 : /// number of arguments.
633 : inline
634 26079 : bool is_times_application(const atermpp::aterm_appl& e)
635 : {
636 26079 : return is_application(e) && is_times_function_symbol(atermpp::down_cast<application>(e).head());
637 : }
638 :
639 : /// \brief Generate identifier \@powerlog2.
640 : /// \return Identifier \@powerlog2.
641 : inline
642 113 : const core::identifier_string& powerlog2_pos_name()
643 : {
644 113 : static core::identifier_string powerlog2_pos_name = core::identifier_string("@powerlog2");
645 113 : return powerlog2_pos_name;
646 : }
647 :
648 : /// \brief Constructor for function symbol \@powerlog2.
649 :
650 : /// \return Function symbol powerlog2_pos.
651 : inline
652 63294 : const function_symbol& powerlog2_pos()
653 : {
654 63294 : static function_symbol powerlog2_pos(powerlog2_pos_name(), make_function_sort_(pos(), pos()));
655 63294 : return powerlog2_pos;
656 : }
657 :
658 : /// \brief Recogniser for function \@powerlog2.
659 : /// \param e A data expression.
660 : /// \return true iff e is the function symbol matching \@powerlog2.
661 : inline
662 : bool is_powerlog2_pos_function_symbol(const atermpp::aterm_appl& e)
663 : {
664 : if (is_function_symbol(e))
665 : {
666 : return atermpp::down_cast<function_symbol>(e) == powerlog2_pos();
667 : }
668 : return false;
669 : }
670 :
671 : /// \brief Application of function symbol \@powerlog2.
672 :
673 : /// \param arg0 A data expression.
674 : /// \return Application of \@powerlog2 to a number of arguments.
675 : inline
676 48232 : application powerlog2_pos(const data_expression& arg0)
677 : {
678 48232 : return sort_pos::powerlog2_pos()(arg0);
679 : }
680 :
681 : /// \brief Make an application of function symbol \@powerlog2.
682 : /// \param result The data expression where the \@powerlog2 expression is put.
683 :
684 : /// \param arg0 A data expression.
685 : inline
686 : void make_powerlog2_pos(data_expression& result, const data_expression& arg0)
687 : {
688 : make_application(result, sort_pos::powerlog2_pos(),arg0);
689 : }
690 :
691 : /// \brief Recogniser for application of \@powerlog2.
692 : /// \param e A data expression.
693 : /// \return true iff e is an application of function symbol powerlog2_pos to a
694 : /// number of arguments.
695 : inline
696 : bool is_powerlog2_pos_application(const atermpp::aterm_appl& e)
697 : {
698 : return is_application(e) && is_powerlog2_pos_function_symbol(atermpp::down_cast<application>(e).head());
699 : }
700 : /// \brief Give all system defined mappings for pos
701 : /// \return All system defined mappings for pos
702 : inline
703 10484 : function_symbol_vector pos_generate_functions_code()
704 : {
705 10484 : function_symbol_vector result;
706 10484 : result.push_back(sort_pos::maximum());
707 10484 : result.push_back(sort_pos::minimum());
708 10484 : result.push_back(sort_pos::succ());
709 10484 : result.push_back(sort_pos::pos_predecessor());
710 10484 : result.push_back(sort_pos::plus());
711 10484 : result.push_back(sort_pos::add_with_carry());
712 10484 : result.push_back(sort_pos::times());
713 10484 : result.push_back(sort_pos::powerlog2_pos());
714 10484 : return result;
715 0 : }
716 :
717 : /// \brief Give all system defined mappings and constructors for pos
718 : /// \return All system defined mappings for pos
719 : inline
720 : function_symbol_vector pos_generate_constructors_and_functions_code()
721 : {
722 : function_symbol_vector result=pos_generate_functions_code();
723 : for(const function_symbol& f: pos_generate_constructors_code())
724 : {
725 : result.push_back(f);
726 : }
727 : return result;
728 : }
729 :
730 : /// \brief Give all system defined mappings that can be used in mCRL2 specs for pos
731 : /// \return All system defined mappings for that can be used in mCRL2 specificationis pos
732 : inline
733 4578 : function_symbol_vector pos_mCRL2_usable_mappings()
734 : {
735 4578 : function_symbol_vector result;
736 4578 : result.push_back(sort_pos::maximum());
737 4578 : result.push_back(sort_pos::minimum());
738 4578 : result.push_back(sort_pos::succ());
739 4578 : result.push_back(sort_pos::pos_predecessor());
740 4578 : result.push_back(sort_pos::plus());
741 4578 : result.push_back(sort_pos::add_with_carry());
742 4578 : result.push_back(sort_pos::times());
743 4578 : result.push_back(sort_pos::powerlog2_pos());
744 4578 : return result;
745 0 : }
746 :
747 :
748 : // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
749 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
750 : /// \brief Give all system defined mappings that are to be implemented in C++ code for pos
751 : /// \return A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for pos
752 : inline
753 10484 : implementation_map pos_cpp_implementable_mappings()
754 : {
755 10484 : implementation_map result;
756 10484 : return result;
757 : }
758 : ///\brief Function for projecting out argument.
759 : /// left from an application.
760 : /// \param e A data expression.
761 : /// \pre left is defined for e.
762 : /// \return The argument of e that corresponds to left.
763 : inline
764 9916 : const data_expression& left(const data_expression& e)
765 : {
766 9916 : assert(is_cdub_application(e) || is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_times_application(e));
767 9916 : return atermpp::down_cast<application>(e)[0];
768 : }
769 :
770 : ///\brief Function for projecting out argument.
771 : /// right from an application.
772 : /// \param e A data expression.
773 : /// \pre right is defined for e.
774 : /// \return The argument of e that corresponds to right.
775 : inline
776 9697 : const data_expression& right(const data_expression& e)
777 : {
778 9697 : assert(is_cdub_application(e) || is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_times_application(e));
779 9697 : return atermpp::down_cast<application>(e)[1];
780 : }
781 :
782 : ///\brief Function for projecting out argument.
783 : /// arg from an application.
784 : /// \param e A data expression.
785 : /// \pre arg is defined for e.
786 : /// \return The argument of e that corresponds to arg.
787 : inline
788 : const data_expression& arg(const data_expression& e)
789 : {
790 : assert(is_succ_application(e) || is_pos_predecessor_application(e) || is_powerlog2_pos_application(e));
791 : return atermpp::down_cast<application>(e)[0];
792 : }
793 :
794 : ///\brief Function for projecting out argument.
795 : /// arg1 from an application.
796 : /// \param e A data expression.
797 : /// \pre arg1 is defined for e.
798 : /// \return The argument of e that corresponds to arg1.
799 : inline
800 116 : const data_expression& arg1(const data_expression& e)
801 : {
802 116 : assert(is_add_with_carry_application(e));
803 116 : return atermpp::down_cast<application>(e)[0];
804 : }
805 :
806 : ///\brief Function for projecting out argument.
807 : /// arg2 from an application.
808 : /// \param e A data expression.
809 : /// \pre arg2 is defined for e.
810 : /// \return The argument of e that corresponds to arg2.
811 : inline
812 116 : const data_expression& arg2(const data_expression& e)
813 : {
814 116 : assert(is_add_with_carry_application(e));
815 116 : return atermpp::down_cast<application>(e)[1];
816 : }
817 :
818 : ///\brief Function for projecting out argument.
819 : /// arg3 from an application.
820 : /// \param e A data expression.
821 : /// \pre arg3 is defined for e.
822 : /// \return The argument of e that corresponds to arg3.
823 : inline
824 116 : const data_expression& arg3(const data_expression& e)
825 : {
826 116 : assert(is_add_with_carry_application(e));
827 116 : return atermpp::down_cast<application>(e)[2];
828 : }
829 :
830 : /// \brief Give all system defined equations for pos
831 : /// \return All system defined equations for sort pos
832 : inline
833 10484 : data_equation_vector pos_generate_equations_code()
834 : {
835 20968 : variable vb("b",sort_bool::bool_());
836 20968 : variable vc("c",sort_bool::bool_());
837 20968 : variable vp("p",pos());
838 20968 : variable vq("q",pos());
839 20968 : variable vp1("p1",pos());
840 20968 : variable vq1("q1",pos());
841 :
842 10484 : data_equation_vector result;
843 31452 : result.push_back(data_equation(variable_list({vb, vp}), equal_to(c1(), cdub(vb, vp)), sort_bool::false_()));
844 31452 : result.push_back(data_equation(variable_list({vb, vp}), equal_to(cdub(vb, vp), c1()), sort_bool::false_()));
845 41936 : result.push_back(data_equation(variable_list({vb, vp, vq}), equal_to(cdub(vb, vp), cdub(vb, vq)), equal_to(vp, vq)));
846 31452 : result.push_back(data_equation(variable_list({vp, vq}), equal_to(cdub(sort_bool::false_(), vp), cdub(sort_bool::true_(), vq)), sort_bool::false_()));
847 31452 : result.push_back(data_equation(variable_list({vp, vq}), equal_to(cdub(sort_bool::true_(), vp), cdub(sort_bool::false_(), vq)), sort_bool::false_()));
848 20968 : result.push_back(data_equation(variable_list({vp}), equal_to(succ(vp), c1()), sort_bool::false_()));
849 20968 : result.push_back(data_equation(variable_list({vq}), equal_to(c1(), succ(vq)), sort_bool::false_()));
850 41936 : result.push_back(data_equation(variable_list({vc, vp, vq}), equal_to(succ(vp), cdub(vc, vq)), equal_to(vp, pos_predecessor(cdub(vc, vq)))));
851 41936 : result.push_back(data_equation(variable_list({vb, vp, vq}), equal_to(cdub(vb, vp), succ(vq)), equal_to(pos_predecessor(cdub(vb, vp)), vq)));
852 20968 : result.push_back(data_equation(variable_list({vp}), less(vp, c1()), sort_bool::false_()));
853 31452 : result.push_back(data_equation(variable_list({vb, vp}), less(c1(), cdub(vb, vp)), sort_bool::true_()));
854 52420 : result.push_back(data_equation(variable_list({vb, vc, vp, vq}), less(cdub(vb, vp), cdub(vc, vq)), if_(sort_bool::implies(vc, vb), less(vp, vq), less_equal(vp, vq))));
855 41936 : result.push_back(data_equation(variable_list({vc, vp, vq}), less(succ(vp), cdub(vc, vq)), less(vp, pos_predecessor(cdub(vc, vq)))));
856 41936 : result.push_back(data_equation(variable_list({vb, vp, vq}), less(cdub(vb, vp), succ(vq)), less_equal(cdub(vb, vp), vq)));
857 20968 : result.push_back(data_equation(variable_list({vq}), less(c1(), succ(vq)), sort_bool::true_()));
858 20968 : result.push_back(data_equation(variable_list({vp}), less_equal(c1(), vp), sort_bool::true_()));
859 31452 : result.push_back(data_equation(variable_list({vb, vp}), less_equal(cdub(vb, vp), c1()), sort_bool::false_()));
860 52420 : result.push_back(data_equation(variable_list({vb, vc, vp, vq}), less_equal(cdub(vb, vp), cdub(vc, vq)), if_(sort_bool::implies(vb, vc), less_equal(vp, vq), less(vp, vq))));
861 41936 : result.push_back(data_equation(variable_list({vc, vp, vq}), less_equal(succ(vp), cdub(vc, vq)), less(vp, cdub(vc, vq))));
862 41936 : result.push_back(data_equation(variable_list({vb, vp, vq}), less_equal(cdub(vb, vp), succ(vq)), less_equal(pos_predecessor(cdub(vb, vp)), vq)));
863 20968 : result.push_back(data_equation(variable_list({vp}), less_equal(succ(vp), c1()), sort_bool::false_()));
864 31452 : result.push_back(data_equation(variable_list({vp, vq}), maximum(vp, vq), if_(less_equal(vp, vq), vq, vp)));
865 31452 : result.push_back(data_equation(variable_list({vp, vq}), minimum(vp, vq), if_(less_equal(vp, vq), vp, vq)));
866 10484 : result.push_back(data_equation(variable_list(), succ(c1()), cdub(sort_bool::false_(), c1())));
867 20968 : result.push_back(data_equation(variable_list({vp}), succ(cdub(sort_bool::false_(), vp)), cdub(sort_bool::true_(), vp)));
868 20968 : result.push_back(data_equation(variable_list({vp}), succ(cdub(sort_bool::true_(), vp)), cdub(sort_bool::false_(), succ(vp))));
869 10484 : result.push_back(data_equation(variable_list(), pos_predecessor(c1()), c1()));
870 10484 : result.push_back(data_equation(variable_list(), pos_predecessor(cdub(sort_bool::false_(), c1())), c1()));
871 31452 : result.push_back(data_equation(variable_list({vb, vp}), pos_predecessor(cdub(sort_bool::false_(), cdub(vb, vp))), cdub(sort_bool::true_(), pos_predecessor(cdub(vb, vp)))));
872 20968 : result.push_back(data_equation(variable_list({vp}), pos_predecessor(cdub(sort_bool::true_(), vp)), cdub(sort_bool::false_(), vp)));
873 31452 : result.push_back(data_equation(variable_list({vp, vq}), plus(vp, vq), add_with_carry(sort_bool::false_(), vp, vq)));
874 20968 : result.push_back(data_equation(variable_list({vp}), add_with_carry(sort_bool::false_(), c1(), vp), succ(vp)));
875 20968 : result.push_back(data_equation(variable_list({vp}), add_with_carry(sort_bool::true_(), c1(), vp), succ(succ(vp))));
876 20968 : result.push_back(data_equation(variable_list({vp}), add_with_carry(sort_bool::false_(), vp, c1()), succ(vp)));
877 20968 : result.push_back(data_equation(variable_list({vp}), add_with_carry(sort_bool::true_(), vp, c1()), succ(succ(vp))));
878 52420 : result.push_back(data_equation(variable_list({vb, vc, vp, vq}), add_with_carry(vb, cdub(vc, vp), cdub(vc, vq)), cdub(vb, add_with_carry(vc, vp, vq))));
879 41936 : result.push_back(data_equation(variable_list({vb, vp, vq}), add_with_carry(vb, cdub(sort_bool::false_(), vp), cdub(sort_bool::true_(), vq)), cdub(sort_bool::not_(vb), add_with_carry(vb, vp, vq))));
880 41936 : result.push_back(data_equation(variable_list({vb, vp, vq}), add_with_carry(vb, cdub(sort_bool::true_(), vp), cdub(sort_bool::false_(), vq)), cdub(sort_bool::not_(vb), add_with_carry(vb, vp, vq))));
881 20968 : result.push_back(data_equation(variable_list({vp}), times(c1(), vp), vp));
882 20968 : result.push_back(data_equation(variable_list({vp}), times(vp, c1()), vp));
883 31452 : result.push_back(data_equation(variable_list({vp, vq}), times(cdub(sort_bool::false_(), vp), vq), cdub(sort_bool::false_(), times(vp, vq))));
884 31452 : result.push_back(data_equation(variable_list({vp, vq}), times(vp, cdub(sort_bool::false_(), vq)), cdub(sort_bool::false_(), times(vp, vq))));
885 31452 : result.push_back(data_equation(variable_list({vp, vq}), times(cdub(sort_bool::true_(), vp), cdub(sort_bool::true_(), vq)), cdub(sort_bool::true_(), add_with_carry(sort_bool::false_(), vp, add_with_carry(sort_bool::false_(), vq, cdub(sort_bool::false_(), times(vp, vq)))))));
886 10484 : result.push_back(data_equation(variable_list(), powerlog2_pos(c1()), c1()));
887 20968 : result.push_back(data_equation(variable_list({vb}), powerlog2_pos(cdub(vb, c1())), c1()));
888 41936 : result.push_back(data_equation(variable_list({vb, vc, vp}), powerlog2_pos(cdub(vb, cdub(vc, vp))), cdub(sort_bool::false_(), powerlog2_pos(vp))));
889 20968 : return result;
890 10484 : }
891 :
892 : } // namespace sort_pos
893 :
894 : } // namespace data
895 :
896 : } // namespace mcrl2
897 :
898 : #endif // MCRL2_DATA_POS_H
|
