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/int.h
10 : /// \brief The standard sort int_.
11 : ///
12 : /// This file was generated from the data sort specification
13 : /// mcrl2/data/build/int.spec.
14 :
15 : #ifndef MCRL2_DATA_INT_H
16 : #define MCRL2_DATA_INT_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 : #include "mcrl2/data/pos.h"
28 : #include "mcrl2/data/nat.h"
29 :
30 : namespace mcrl2 {
31 :
32 : namespace data {
33 :
34 : /// \brief Namespace for system defined sort int_.
35 : namespace sort_int {
36 :
37 : inline
38 116 : const core::identifier_string& int_name()
39 : {
40 116 : static core::identifier_string int_name = core::identifier_string("Int");
41 116 : return int_name;
42 : }
43 :
44 : /// \brief Constructor for sort expression Int.
45 : /// \return Sort expression Int.
46 : inline
47 1867259 : const basic_sort& int_()
48 : {
49 1867259 : static basic_sort int_ = basic_sort(int_name());
50 1867259 : return int_;
51 : }
52 :
53 : /// \brief Recogniser for sort expression Int
54 : /// \param e A sort expression
55 : /// \return true iff e == int_()
56 : inline
57 185992 : bool is_int(const sort_expression& e)
58 : {
59 185992 : if (is_basic_sort(e))
60 : {
61 18917 : return basic_sort(e) == int_();
62 : }
63 167075 : return false;
64 : }
65 :
66 :
67 : /// \brief Generate identifier \@cInt.
68 : /// \return Identifier \@cInt.
69 : inline
70 113 : const core::identifier_string& cint_name()
71 : {
72 113 : static core::identifier_string cint_name = core::identifier_string("@cInt");
73 113 : return cint_name;
74 : }
75 :
76 : /// \brief Constructor for function symbol \@cInt.
77 :
78 : /// \return Function symbol cint.
79 : inline
80 648086 : const function_symbol& cint()
81 : {
82 648086 : static function_symbol cint(cint_name(), make_function_sort_(sort_nat::nat(), int_()));
83 648086 : return cint;
84 : }
85 :
86 : /// \brief Recogniser for function \@cInt.
87 : /// \param e A data expression.
88 : /// \return true iff e is the function symbol matching \@cInt.
89 : inline
90 151219 : bool is_cint_function_symbol(const atermpp::aterm_appl& e)
91 : {
92 151219 : if (is_function_symbol(e))
93 : {
94 147633 : return atermpp::down_cast<function_symbol>(e) == cint();
95 : }
96 3586 : return false;
97 : }
98 :
99 : /// \brief Application of function symbol \@cInt.
100 :
101 : /// \param arg0 A data expression.
102 : /// \return Application of \@cInt to a number of arguments.
103 : inline
104 485165 : application cint(const data_expression& arg0)
105 : {
106 485165 : return sort_int::cint()(arg0);
107 : }
108 :
109 : /// \brief Make an application of function symbol \@cInt.
110 : /// \param result The data expression where the \@cInt expression is put.
111 :
112 : /// \param arg0 A data expression.
113 : inline
114 : void make_cint(data_expression& result, const data_expression& arg0)
115 : {
116 : make_application(result, sort_int::cint(),arg0);
117 : }
118 :
119 : /// \brief Recogniser for application of \@cInt.
120 : /// \param e A data expression.
121 : /// \return true iff e is an application of function symbol cint to a
122 : /// number of arguments.
123 : inline
124 154047 : bool is_cint_application(const atermpp::aterm_appl& e)
125 : {
126 154047 : return is_application(e) && is_cint_function_symbol(atermpp::down_cast<application>(e).head());
127 : }
128 :
129 : /// \brief Generate identifier \@cNeg.
130 : /// \return Identifier \@cNeg.
131 : inline
132 112 : const core::identifier_string& cneg_name()
133 : {
134 112 : static core::identifier_string cneg_name = core::identifier_string("@cNeg");
135 112 : return cneg_name;
136 : }
137 :
138 : /// \brief Constructor for function symbol \@cNeg.
139 :
140 : /// \return Function symbol cneg.
141 : inline
142 255709 : const function_symbol& cneg()
143 : {
144 255709 : static function_symbol cneg(cneg_name(), make_function_sort_(sort_pos::pos(), int_()));
145 255709 : return cneg;
146 : }
147 :
148 : /// \brief Recogniser for function \@cNeg.
149 : /// \param e A data expression.
150 : /// \return true iff e is the function symbol matching \@cNeg.
151 : inline
152 21779 : bool is_cneg_function_symbol(const atermpp::aterm_appl& e)
153 : {
154 21779 : if (is_function_symbol(e))
155 : {
156 20937 : return atermpp::down_cast<function_symbol>(e) == cneg();
157 : }
158 842 : return false;
159 : }
160 :
161 : /// \brief Application of function symbol \@cNeg.
162 :
163 : /// \param arg0 A data expression.
164 : /// \return Application of \@cNeg to a number of arguments.
165 : inline
166 224711 : application cneg(const data_expression& arg0)
167 : {
168 224711 : return sort_int::cneg()(arg0);
169 : }
170 :
171 : /// \brief Make an application of function symbol \@cNeg.
172 : /// \param result The data expression where the \@cNeg expression is put.
173 :
174 : /// \param arg0 A data expression.
175 : inline
176 : void make_cneg(data_expression& result, const data_expression& arg0)
177 : {
178 : make_application(result, sort_int::cneg(),arg0);
179 : }
180 :
181 : /// \brief Recogniser for application of \@cNeg.
182 : /// \param e A data expression.
183 : /// \return true iff e is an application of function symbol cneg to a
184 : /// number of arguments.
185 : inline
186 21779 : bool is_cneg_application(const atermpp::aterm_appl& e)
187 : {
188 21779 : return is_application(e) && is_cneg_function_symbol(atermpp::down_cast<application>(e).head());
189 : }
190 : /// \brief Give all system defined constructors for int_.
191 : /// \return All system defined constructors for int_.
192 : inline
193 5483 : function_symbol_vector int_generate_constructors_code()
194 : {
195 5483 : function_symbol_vector result;
196 5483 : result.push_back(sort_int::cint());
197 5483 : result.push_back(sort_int::cneg());
198 :
199 5483 : return result;
200 0 : }
201 : /// \brief Give all defined constructors which can be used in mCRL2 specs for int_.
202 : /// \return All system defined constructors that can be used in an mCRL2 specification for int_.
203 : inline
204 4578 : function_symbol_vector int_mCRL2_usable_constructors()
205 : {
206 4578 : function_symbol_vector result;
207 4578 : result.push_back(sort_int::cint());
208 4578 : result.push_back(sort_int::cneg());
209 :
210 4578 : return result;
211 0 : }
212 : // 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
213 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
214 : /// \brief Give all system defined constructors which have an implementation in C++ and not in rewrite rules for int_.
215 : /// \return All system defined constructors that are to be implemented in C++ for int_.
216 : inline
217 10914 : implementation_map int_cpp_implementable_constructors()
218 : {
219 10914 : implementation_map result;
220 10914 : return result;
221 : }
222 :
223 : /// \brief Generate identifier Nat2Int.
224 : /// \return Identifier Nat2Int.
225 : inline
226 112 : const core::identifier_string& nat2int_name()
227 : {
228 112 : static core::identifier_string nat2int_name = core::identifier_string("Nat2Int");
229 112 : return nat2int_name;
230 : }
231 :
232 : /// \brief Constructor for function symbol Nat2Int.
233 :
234 : /// \return Function symbol nat2int.
235 : inline
236 181550 : const function_symbol& nat2int()
237 : {
238 181550 : static function_symbol nat2int(nat2int_name(), make_function_sort_(sort_nat::nat(), int_()));
239 181550 : return nat2int;
240 : }
241 :
242 : /// \brief Recogniser for function Nat2Int.
243 : /// \param e A data expression.
244 : /// \return true iff e is the function symbol matching Nat2Int.
245 : inline
246 169519 : bool is_nat2int_function_symbol(const atermpp::aterm_appl& e)
247 : {
248 169519 : if (is_function_symbol(e))
249 : {
250 165933 : return atermpp::down_cast<function_symbol>(e) == nat2int();
251 : }
252 3586 : return false;
253 : }
254 :
255 : /// \brief Application of function symbol Nat2Int.
256 :
257 : /// \param arg0 A data expression.
258 : /// \return Application of Nat2Int to a number of arguments.
259 : inline
260 5485 : application nat2int(const data_expression& arg0)
261 : {
262 5485 : return sort_int::nat2int()(arg0);
263 : }
264 :
265 : /// \brief Make an application of function symbol Nat2Int.
266 : /// \param result The data expression where the Nat2Int expression is put.
267 :
268 : /// \param arg0 A data expression.
269 : inline
270 : void make_nat2int(data_expression& result, const data_expression& arg0)
271 : {
272 : make_application(result, sort_int::nat2int(),arg0);
273 : }
274 :
275 : /// \brief Recogniser for application of Nat2Int.
276 : /// \param e A data expression.
277 : /// \return true iff e is an application of function symbol nat2int to a
278 : /// number of arguments.
279 : inline
280 172347 : bool is_nat2int_application(const atermpp::aterm_appl& e)
281 : {
282 172347 : return is_application(e) && is_nat2int_function_symbol(atermpp::down_cast<application>(e).head());
283 : }
284 :
285 : /// \brief Generate identifier Int2Nat.
286 : /// \return Identifier Int2Nat.
287 : inline
288 112 : const core::identifier_string& int2nat_name()
289 : {
290 112 : static core::identifier_string int2nat_name = core::identifier_string("Int2Nat");
291 112 : return int2nat_name;
292 : }
293 :
294 : /// \brief Constructor for function symbol Int2Nat.
295 :
296 : /// \return Function symbol int2nat.
297 : inline
298 26534 : const function_symbol& int2nat()
299 : {
300 26534 : static function_symbol int2nat(int2nat_name(), make_function_sort_(int_(), sort_nat::nat()));
301 26534 : return int2nat;
302 : }
303 :
304 : /// \brief Recogniser for function Int2Nat.
305 : /// \param e A data expression.
306 : /// \return true iff e is the function symbol matching Int2Nat.
307 : inline
308 0 : bool is_int2nat_function_symbol(const atermpp::aterm_appl& e)
309 : {
310 0 : if (is_function_symbol(e))
311 : {
312 0 : return atermpp::down_cast<function_symbol>(e) == int2nat();
313 : }
314 0 : return false;
315 : }
316 :
317 : /// \brief Application of function symbol Int2Nat.
318 :
319 : /// \param arg0 A data expression.
320 : /// \return Application of Int2Nat to a number of arguments.
321 : inline
322 16402 : application int2nat(const data_expression& arg0)
323 : {
324 16402 : return sort_int::int2nat()(arg0);
325 : }
326 :
327 : /// \brief Make an application of function symbol Int2Nat.
328 : /// \param result The data expression where the Int2Nat expression is put.
329 :
330 : /// \param arg0 A data expression.
331 : inline
332 : void make_int2nat(data_expression& result, const data_expression& arg0)
333 : {
334 : make_application(result, sort_int::int2nat(),arg0);
335 : }
336 :
337 : /// \brief Recogniser for application of Int2Nat.
338 : /// \param e A data expression.
339 : /// \return true iff e is an application of function symbol int2nat to a
340 : /// number of arguments.
341 : inline
342 0 : bool is_int2nat_application(const atermpp::aterm_appl& e)
343 : {
344 0 : return is_application(e) && is_int2nat_function_symbol(atermpp::down_cast<application>(e).head());
345 : }
346 :
347 : /// \brief Generate identifier Pos2Int.
348 : /// \return Identifier Pos2Int.
349 : inline
350 112 : const core::identifier_string& pos2int_name()
351 : {
352 112 : static core::identifier_string pos2int_name = core::identifier_string("Pos2Int");
353 112 : return pos2int_name;
354 : }
355 :
356 : /// \brief Constructor for function symbol Pos2Int.
357 :
358 : /// \return Function symbol pos2int.
359 : inline
360 181747 : const function_symbol& pos2int()
361 : {
362 181747 : static function_symbol pos2int(pos2int_name(), make_function_sort_(sort_pos::pos(), int_()));
363 181747 : return pos2int;
364 : }
365 :
366 : /// \brief Recogniser for function Pos2Int.
367 : /// \param e A data expression.
368 : /// \return true iff e is the function symbol matching Pos2Int.
369 : inline
370 169735 : bool is_pos2int_function_symbol(const atermpp::aterm_appl& e)
371 : {
372 169735 : if (is_function_symbol(e))
373 : {
374 166149 : return atermpp::down_cast<function_symbol>(e) == pos2int();
375 : }
376 3586 : return false;
377 : }
378 :
379 : /// \brief Application of function symbol Pos2Int.
380 :
381 : /// \param arg0 A data expression.
382 : /// \return Application of Pos2Int to a number of arguments.
383 : inline
384 5537 : application pos2int(const data_expression& arg0)
385 : {
386 5537 : return sort_int::pos2int()(arg0);
387 : }
388 :
389 : /// \brief Make an application of function symbol Pos2Int.
390 : /// \param result The data expression where the Pos2Int expression is put.
391 :
392 : /// \param arg0 A data expression.
393 : inline
394 : void make_pos2int(data_expression& result, const data_expression& arg0)
395 : {
396 : make_application(result, sort_int::pos2int(),arg0);
397 : }
398 :
399 : /// \brief Recogniser for application of Pos2Int.
400 : /// \param e A data expression.
401 : /// \return true iff e is an application of function symbol pos2int to a
402 : /// number of arguments.
403 : inline
404 172563 : bool is_pos2int_application(const atermpp::aterm_appl& e)
405 : {
406 172563 : return is_application(e) && is_pos2int_function_symbol(atermpp::down_cast<application>(e).head());
407 : }
408 :
409 : /// \brief Generate identifier Int2Pos.
410 : /// \return Identifier Int2Pos.
411 : inline
412 112 : const core::identifier_string& int2pos_name()
413 : {
414 112 : static core::identifier_string int2pos_name = core::identifier_string("Int2Pos");
415 112 : return int2pos_name;
416 : }
417 :
418 : /// \brief Constructor for function symbol Int2Pos.
419 :
420 : /// \return Function symbol int2pos.
421 : inline
422 26485 : const function_symbol& int2pos()
423 : {
424 26485 : static function_symbol int2pos(int2pos_name(), make_function_sort_(int_(), sort_pos::pos()));
425 26485 : return int2pos;
426 : }
427 :
428 : /// \brief Recogniser for function Int2Pos.
429 : /// \param e A data expression.
430 : /// \return true iff e is the function symbol matching Int2Pos.
431 : inline
432 0 : bool is_int2pos_function_symbol(const atermpp::aterm_appl& e)
433 : {
434 0 : if (is_function_symbol(e))
435 : {
436 0 : return atermpp::down_cast<function_symbol>(e) == int2pos();
437 : }
438 0 : return false;
439 : }
440 :
441 : /// \brief Application of function symbol Int2Pos.
442 :
443 : /// \param arg0 A data expression.
444 : /// \return Application of Int2Pos to a number of arguments.
445 : inline
446 16353 : application int2pos(const data_expression& arg0)
447 : {
448 16353 : return sort_int::int2pos()(arg0);
449 : }
450 :
451 : /// \brief Make an application of function symbol Int2Pos.
452 : /// \param result The data expression where the Int2Pos expression is put.
453 :
454 : /// \param arg0 A data expression.
455 : inline
456 : void make_int2pos(data_expression& result, const data_expression& arg0)
457 : {
458 : make_application(result, sort_int::int2pos(),arg0);
459 : }
460 :
461 : /// \brief Recogniser for application of Int2Pos.
462 : /// \param e A data expression.
463 : /// \return true iff e is an application of function symbol int2pos to a
464 : /// number of arguments.
465 : inline
466 0 : bool is_int2pos_application(const atermpp::aterm_appl& e)
467 : {
468 0 : return is_application(e) && is_int2pos_function_symbol(atermpp::down_cast<application>(e).head());
469 : }
470 :
471 : /// \brief Generate identifier max.
472 : /// \return Identifier max.
473 : inline
474 110667 : const core::identifier_string& maximum_name()
475 : {
476 110667 : static core::identifier_string maximum_name = core::identifier_string("max");
477 110667 : return maximum_name;
478 : }
479 :
480 : // This function is not intended for public use and therefore not documented in Doxygen.
481 : inline
482 110622 : function_symbol maximum(const sort_expression& s0, const sort_expression& s1)
483 : {
484 110622 : sort_expression target_sort;
485 110622 : if (s0 == sort_pos::pos() && s1 == int_())
486 : {
487 21027 : target_sort = sort_pos::pos();
488 : }
489 89595 : else if (s0 == int_() && s1 == sort_pos::pos())
490 : {
491 21027 : target_sort = sort_pos::pos();
492 : }
493 68568 : else if (s0 == sort_nat::nat() && s1 == int_())
494 : {
495 21027 : target_sort = sort_nat::nat();
496 : }
497 47541 : else if (s0 == int_() && s1 == sort_nat::nat())
498 : {
499 21027 : target_sort = sort_nat::nat();
500 : }
501 26514 : else if (s0 == int_() && s1 == int_())
502 : {
503 15548 : target_sort = int_();
504 : }
505 10966 : else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
506 : {
507 5483 : target_sort = sort_pos::pos();
508 : }
509 5483 : else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
510 : {
511 5483 : target_sort = sort_pos::pos();
512 : }
513 0 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
514 : {
515 0 : target_sort = sort_nat::nat();
516 : }
517 0 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
518 : {
519 0 : target_sort = sort_pos::pos();
520 : }
521 : else
522 : {
523 0 : throw mcrl2::runtime_error("Cannot compute target sort for maximum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
524 : }
525 :
526 110622 : function_symbol maximum(maximum_name(), make_function_sort_(s0, s1, target_sort));
527 221244 : return maximum;
528 110622 : }
529 :
530 : /// \brief Recogniser for function max.
531 : /// \param e A data expression.
532 : /// \return true iff e is the function symbol matching max.
533 : inline
534 45 : bool is_maximum_function_symbol(const atermpp::aterm_appl& e)
535 : {
536 45 : if (is_function_symbol(e))
537 : {
538 45 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
539 45 : return f.name() == maximum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == maximum(sort_pos::pos(), int_()) || f == maximum(int_(), sort_pos::pos()) || f == maximum(sort_nat::nat(), int_()) || f == maximum(int_(), sort_nat::nat()) || f == maximum(int_(), int_()) || f == maximum(sort_pos::pos(), sort_nat::nat()) || f == maximum(sort_nat::nat(), sort_pos::pos()) || f == maximum(sort_nat::nat(), sort_nat::nat()) || f == maximum(sort_pos::pos(), sort_pos::pos()));
540 : }
541 0 : return false;
542 : }
543 :
544 : /// \brief Application of function symbol max.
545 :
546 : /// \param arg0 A data expression.
547 : /// \param arg1 A data expression.
548 : /// \return Application of max to a number of arguments.
549 : inline
550 60317 : application maximum(const data_expression& arg0, const data_expression& arg1)
551 : {
552 120634 : return sort_int::maximum(arg0.sort(), arg1.sort())(arg0, arg1);
553 : }
554 :
555 : /// \brief Make an application of function symbol max.
556 : /// \param result The data expression where the max expression is put.
557 :
558 : /// \param arg0 A data expression.
559 : /// \param arg1 A data expression.
560 : inline
561 : void make_maximum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
562 : {
563 : make_application(result, sort_int::maximum(arg0.sort(), arg1.sort()),arg0, arg1);
564 : }
565 :
566 : /// \brief Recogniser for application of max.
567 : /// \param e A data expression.
568 : /// \return true iff e is an application of function symbol maximum to a
569 : /// number of arguments.
570 : inline
571 45 : bool is_maximum_application(const atermpp::aterm_appl& e)
572 : {
573 45 : return is_application(e) && is_maximum_function_symbol(atermpp::down_cast<application>(e).head());
574 : }
575 :
576 : /// \brief Generate identifier min.
577 : /// \return Identifier min.
578 : inline
579 15593 : const core::identifier_string& minimum_name()
580 : {
581 15593 : static core::identifier_string minimum_name = core::identifier_string("min");
582 15593 : return minimum_name;
583 : }
584 :
585 : // This function is not intended for public use and therefore not documented in Doxygen.
586 : inline
587 15548 : function_symbol minimum(const sort_expression& s0, const sort_expression& s1)
588 : {
589 15548 : sort_expression target_sort;
590 15548 : if (s0 == int_() && s1 == int_())
591 : {
592 15548 : target_sort = int_();
593 : }
594 0 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
595 : {
596 0 : target_sort = sort_nat::nat();
597 : }
598 0 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
599 : {
600 0 : target_sort = sort_pos::pos();
601 : }
602 : else
603 : {
604 0 : throw mcrl2::runtime_error("Cannot compute target sort for minimum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
605 : }
606 :
607 15548 : function_symbol minimum(minimum_name(), make_function_sort_(s0, s1, target_sort));
608 31096 : return minimum;
609 15548 : }
610 :
611 : /// \brief Recogniser for function min.
612 : /// \param e A data expression.
613 : /// \return true iff e is the function symbol matching min.
614 : inline
615 45 : bool is_minimum_function_symbol(const atermpp::aterm_appl& e)
616 : {
617 45 : if (is_function_symbol(e))
618 : {
619 45 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
620 45 : return f.name() == minimum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minimum(int_(), int_()) || f == minimum(sort_nat::nat(), sort_nat::nat()) || f == minimum(sort_pos::pos(), sort_pos::pos()));
621 : }
622 0 : return false;
623 : }
624 :
625 : /// \brief Application of function symbol min.
626 :
627 : /// \param arg0 A data expression.
628 : /// \param arg1 A data expression.
629 : /// \return Application of min to a number of arguments.
630 : inline
631 5487 : application minimum(const data_expression& arg0, const data_expression& arg1)
632 : {
633 10974 : return sort_int::minimum(arg0.sort(), arg1.sort())(arg0, arg1);
634 : }
635 :
636 : /// \brief Make an application of function symbol min.
637 : /// \param result The data expression where the min expression is put.
638 :
639 : /// \param arg0 A data expression.
640 : /// \param arg1 A data expression.
641 : inline
642 : void make_minimum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
643 : {
644 : make_application(result, sort_int::minimum(arg0.sort(), arg1.sort()),arg0, arg1);
645 : }
646 :
647 : /// \brief Recogniser for application of min.
648 : /// \param e A data expression.
649 : /// \return true iff e is an application of function symbol minimum to a
650 : /// number of arguments.
651 : inline
652 45 : bool is_minimum_application(const atermpp::aterm_appl& e)
653 : {
654 45 : return is_application(e) && is_minimum_function_symbol(atermpp::down_cast<application>(e).head());
655 : }
656 :
657 : /// \brief Generate identifier abs.
658 : /// \return Identifier abs.
659 : inline
660 112 : const core::identifier_string& abs_name()
661 : {
662 112 : static core::identifier_string abs_name = core::identifier_string("abs");
663 112 : return abs_name;
664 : }
665 :
666 : /// \brief Constructor for function symbol abs.
667 :
668 : /// \return Function symbol abs.
669 : inline
670 21028 : const function_symbol& abs()
671 : {
672 21028 : static function_symbol abs(abs_name(), make_function_sort_(int_(), sort_nat::nat()));
673 21028 : return abs;
674 : }
675 :
676 : /// \brief Recogniser for function abs.
677 : /// \param e A data expression.
678 : /// \return true iff e is the function symbol matching abs.
679 : inline
680 0 : bool is_abs_function_symbol(const atermpp::aterm_appl& e)
681 : {
682 0 : if (is_function_symbol(e))
683 : {
684 0 : return atermpp::down_cast<function_symbol>(e) == abs();
685 : }
686 0 : return false;
687 : }
688 :
689 : /// \brief Application of function symbol abs.
690 :
691 : /// \param arg0 A data expression.
692 : /// \return Application of abs to a number of arguments.
693 : inline
694 10967 : application abs(const data_expression& arg0)
695 : {
696 10967 : return sort_int::abs()(arg0);
697 : }
698 :
699 : /// \brief Make an application of function symbol abs.
700 : /// \param result The data expression where the abs expression is put.
701 :
702 : /// \param arg0 A data expression.
703 : inline
704 : void make_abs(data_expression& result, const data_expression& arg0)
705 : {
706 : make_application(result, sort_int::abs(),arg0);
707 : }
708 :
709 : /// \brief Recogniser for application of abs.
710 : /// \param e A data expression.
711 : /// \return true iff e is an application of function symbol abs to a
712 : /// number of arguments.
713 : inline
714 0 : bool is_abs_application(const atermpp::aterm_appl& e)
715 : {
716 0 : return is_application(e) && is_abs_function_symbol(atermpp::down_cast<application>(e).head());
717 : }
718 :
719 : /// \brief Generate identifier -.
720 : /// \return Identifier -.
721 : inline
722 116951 : const core::identifier_string& negate_name()
723 : {
724 116951 : static core::identifier_string negate_name = core::identifier_string("-");
725 116951 : return negate_name;
726 : }
727 :
728 : // This function is not intended for public use and therefore not documented in Doxygen.
729 : inline
730 96140 : function_symbol negate(const sort_expression& s0)
731 : {
732 96140 : sort_expression target_sort(int_());
733 96140 : function_symbol negate(negate_name(), make_function_sort_(s0, target_sort));
734 192280 : return negate;
735 96140 : }
736 :
737 : /// \brief Recogniser for function -.
738 : /// \param e A data expression.
739 : /// \return true iff e is the function symbol matching -.
740 : inline
741 21653 : bool is_negate_function_symbol(const atermpp::aterm_appl& e)
742 : {
743 21653 : if (is_function_symbol(e))
744 : {
745 20811 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
746 20811 : return f.name() == negate_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == negate(sort_pos::pos()) || f == negate(sort_nat::nat()) || f == negate(int_()));
747 : }
748 842 : return false;
749 : }
750 :
751 : /// \brief Application of function symbol -.
752 :
753 : /// \param arg0 A data expression.
754 : /// \return Application of - to a number of arguments.
755 : inline
756 65844 : application negate(const data_expression& arg0)
757 : {
758 131688 : return sort_int::negate(arg0.sort())(arg0);
759 : }
760 :
761 : /// \brief Make an application of function symbol -.
762 : /// \param result The data expression where the - expression is put.
763 :
764 : /// \param arg0 A data expression.
765 : inline
766 : void make_negate(data_expression& result, const data_expression& arg0)
767 : {
768 : make_application(result, sort_int::negate(arg0.sort()),arg0);
769 : }
770 :
771 : /// \brief Recogniser for application of -.
772 : /// \param e A data expression.
773 : /// \return true iff e is an application of function symbol negate to a
774 : /// number of arguments.
775 : inline
776 21653 : bool is_negate_application(const atermpp::aterm_appl& e)
777 : {
778 21653 : return is_application(e) && is_negate_function_symbol(atermpp::down_cast<application>(e).head());
779 : }
780 :
781 : /// \brief Generate identifier succ.
782 : /// \return Identifier succ.
783 : inline
784 42961 : const core::identifier_string& succ_name()
785 : {
786 42961 : static core::identifier_string succ_name = core::identifier_string("succ");
787 42961 : return succ_name;
788 : }
789 :
790 : // This function is not intended for public use and therefore not documented in Doxygen.
791 : inline
792 42961 : function_symbol succ(const sort_expression& s0)
793 : {
794 42961 : sort_expression target_sort;
795 42961 : if (s0 == int_())
796 : {
797 21029 : target_sort = int_();
798 : }
799 21932 : else if (s0 == sort_nat::nat())
800 : {
801 16449 : target_sort = sort_pos::pos();
802 : }
803 5483 : else if (s0 == sort_pos::pos())
804 : {
805 5483 : target_sort = sort_pos::pos();
806 : }
807 : else
808 : {
809 0 : throw mcrl2::runtime_error("Cannot compute target sort for succ with domain sorts " + pp(s0) + ". ");
810 : }
811 :
812 42961 : function_symbol succ(succ_name(), make_function_sort_(s0, target_sort));
813 85922 : return succ;
814 42961 : }
815 :
816 : /// \brief Recogniser for function succ.
817 : /// \param e A data expression.
818 : /// \return true iff e is the function symbol matching succ.
819 : inline
820 0 : bool is_succ_function_symbol(const atermpp::aterm_appl& e)
821 : {
822 0 : if (is_function_symbol(e))
823 : {
824 0 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
825 0 : return f.name() == succ_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == succ(int_()) || f == succ(sort_nat::nat()) || f == succ(sort_pos::pos()));
826 : }
827 0 : return false;
828 : }
829 :
830 : /// \brief Application of function symbol succ.
831 :
832 : /// \param arg0 A data expression.
833 : /// \return Application of succ to a number of arguments.
834 : inline
835 32900 : application succ(const data_expression& arg0)
836 : {
837 65800 : return sort_int::succ(arg0.sort())(arg0);
838 : }
839 :
840 : /// \brief Make an application of function symbol succ.
841 : /// \param result The data expression where the succ expression is put.
842 :
843 : /// \param arg0 A data expression.
844 : inline
845 : void make_succ(data_expression& result, const data_expression& arg0)
846 : {
847 : make_application(result, sort_int::succ(arg0.sort()),arg0);
848 : }
849 :
850 : /// \brief Recogniser for application of succ.
851 : /// \param e A data expression.
852 : /// \return true iff e is an application of function symbol succ to a
853 : /// number of arguments.
854 : inline
855 0 : bool is_succ_application(const atermpp::aterm_appl& e)
856 : {
857 0 : return is_application(e) && is_succ_function_symbol(atermpp::down_cast<application>(e).head());
858 : }
859 :
860 : /// \brief Generate identifier pred.
861 : /// \return Identifier pred.
862 : inline
863 69471 : const core::identifier_string& pred_name()
864 : {
865 69471 : static core::identifier_string pred_name = core::identifier_string("pred");
866 69471 : return pred_name;
867 : }
868 :
869 : // This function is not intended for public use and therefore not documented in Doxygen.
870 : inline
871 69471 : function_symbol pred(const sort_expression& s0)
872 : {
873 69471 : sort_expression target_sort;
874 69471 : if (s0 == sort_nat::nat())
875 : {
876 26510 : target_sort = int_();
877 : }
878 42961 : else if (s0 == int_())
879 : {
880 21029 : target_sort = int_();
881 : }
882 21932 : else if (s0 == sort_pos::pos())
883 : {
884 21932 : target_sort = sort_nat::nat();
885 : }
886 : else
887 : {
888 0 : throw mcrl2::runtime_error("Cannot compute target sort for pred with domain sorts " + pp(s0) + ". ");
889 : }
890 :
891 69471 : function_symbol pred(pred_name(), make_function_sort_(s0, target_sort));
892 138942 : return pred;
893 69471 : }
894 :
895 : /// \brief Recogniser for function pred.
896 : /// \param e A data expression.
897 : /// \return true iff e is the function symbol matching pred.
898 : inline
899 0 : bool is_pred_function_symbol(const atermpp::aterm_appl& e)
900 : {
901 0 : if (is_function_symbol(e))
902 : {
903 0 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
904 0 : return f.name() == pred_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == pred(sort_nat::nat()) || f == pred(int_()) || f == pred(sort_pos::pos()));
905 : }
906 0 : return false;
907 : }
908 :
909 : /// \brief Application of function symbol pred.
910 :
911 : /// \param arg0 A data expression.
912 : /// \return Application of pred to a number of arguments.
913 : inline
914 49349 : application pred(const data_expression& arg0)
915 : {
916 98698 : return sort_int::pred(arg0.sort())(arg0);
917 : }
918 :
919 : /// \brief Make an application of function symbol pred.
920 : /// \param result The data expression where the pred expression is put.
921 :
922 : /// \param arg0 A data expression.
923 : inline
924 : void make_pred(data_expression& result, const data_expression& arg0)
925 : {
926 : make_application(result, sort_int::pred(arg0.sort()),arg0);
927 : }
928 :
929 : /// \brief Recogniser for application of pred.
930 : /// \param e A data expression.
931 : /// \return true iff e is an application of function symbol pred to a
932 : /// number of arguments.
933 : inline
934 0 : bool is_pred_application(const atermpp::aterm_appl& e)
935 : {
936 0 : return is_application(e) && is_pred_function_symbol(atermpp::down_cast<application>(e).head());
937 : }
938 :
939 : /// \brief Generate identifier +.
940 : /// \return Identifier +.
941 : inline
942 84344 : const core::identifier_string& plus_name()
943 : {
944 84344 : static core::identifier_string plus_name = core::identifier_string("+");
945 84344 : return plus_name;
946 : }
947 :
948 : // This function is not intended for public use and therefore not documented in Doxygen.
949 : inline
950 45165 : function_symbol plus(const sort_expression& s0, const sort_expression& s1)
951 : {
952 45165 : sort_expression target_sort;
953 45165 : if (s0 == int_() && s1 == int_())
954 : {
955 38118 : target_sort = int_();
956 : }
957 7047 : else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
958 : {
959 606 : target_sort = sort_pos::pos();
960 : }
961 6441 : else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
962 : {
963 375 : target_sort = sort_pos::pos();
964 : }
965 6066 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
966 : {
967 5836 : target_sort = sort_nat::nat();
968 : }
969 230 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
970 : {
971 230 : target_sort = sort_pos::pos();
972 : }
973 : else
974 : {
975 0 : throw mcrl2::runtime_error("Cannot compute target sort for plus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
976 : }
977 :
978 45165 : function_symbol plus(plus_name(), make_function_sort_(s0, s1, target_sort));
979 90330 : return plus;
980 45165 : }
981 :
982 : /// \brief Recogniser for function +.
983 : /// \param e A data expression.
984 : /// \return true iff e is the function symbol matching +.
985 : inline
986 40413 : bool is_plus_function_symbol(const atermpp::aterm_appl& e)
987 : {
988 40413 : if (is_function_symbol(e))
989 : {
990 39179 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
991 39179 : return f.name() == plus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == plus(int_(), int_()) || f == plus(sort_pos::pos(), sort_nat::nat()) || f == plus(sort_nat::nat(), sort_pos::pos()) || f == plus(sort_nat::nat(), sort_nat::nat()) || f == plus(sort_pos::pos(), sort_pos::pos()));
992 : }
993 1234 : return false;
994 : }
995 :
996 : /// \brief Application of function symbol +.
997 :
998 : /// \param arg0 A data expression.
999 : /// \param arg1 A data expression.
1000 : /// \return Application of + to a number of arguments.
1001 : inline
1002 32903 : application plus(const data_expression& arg0, const data_expression& arg1)
1003 : {
1004 65806 : return sort_int::plus(arg0.sort(), arg1.sort())(arg0, arg1);
1005 : }
1006 :
1007 : /// \brief Make an application of function symbol +.
1008 : /// \param result The data expression where the + expression is put.
1009 :
1010 : /// \param arg0 A data expression.
1011 : /// \param arg1 A data expression.
1012 : inline
1013 : void make_plus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1014 : {
1015 : make_application(result, sort_int::plus(arg0.sort(), arg1.sort()),arg0, arg1);
1016 : }
1017 :
1018 : /// \brief Recogniser for application of +.
1019 : /// \param e A data expression.
1020 : /// \return true iff e is an application of function symbol plus to a
1021 : /// number of arguments.
1022 : inline
1023 40817 : bool is_plus_application(const atermpp::aterm_appl& e)
1024 : {
1025 40817 : return is_application(e) && is_plus_function_symbol(atermpp::down_cast<application>(e).head());
1026 : }
1027 :
1028 : /// \brief Generate identifier -.
1029 : /// \return Identifier -.
1030 : inline
1031 113078 : const core::identifier_string& minus_name()
1032 : {
1033 113078 : static core::identifier_string minus_name = core::identifier_string("-");
1034 113078 : return minus_name;
1035 : }
1036 :
1037 : // This function is not intended for public use and therefore not documented in Doxygen.
1038 : inline
1039 74345 : function_symbol minus(const sort_expression& s0, const sort_expression& s1)
1040 : {
1041 74345 : sort_expression target_sort(int_());
1042 74345 : function_symbol minus(minus_name(), make_function_sort_(s0, s1, target_sort));
1043 148690 : return minus;
1044 74345 : }
1045 :
1046 : /// \brief Recogniser for function -.
1047 : /// \param e A data expression.
1048 : /// \return true iff e is the function symbol matching -.
1049 : inline
1050 39967 : bool is_minus_function_symbol(const atermpp::aterm_appl& e)
1051 : {
1052 39967 : if (is_function_symbol(e))
1053 : {
1054 38733 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1055 38733 : return f.name() == minus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minus(sort_pos::pos(), sort_pos::pos()) || f == minus(sort_nat::nat(), sort_nat::nat()) || f == minus(int_(), int_()));
1056 : }
1057 1234 : return false;
1058 : }
1059 :
1060 : /// \brief Application of function symbol -.
1061 :
1062 : /// \param arg0 A data expression.
1063 : /// \param arg1 A data expression.
1064 : /// \return Application of - to a number of arguments.
1065 : inline
1066 43866 : application minus(const data_expression& arg0, const data_expression& arg1)
1067 : {
1068 87732 : return sort_int::minus(arg0.sort(), arg1.sort())(arg0, arg1);
1069 : }
1070 :
1071 : /// \brief Make an application of function symbol -.
1072 : /// \param result The data expression where the - expression is put.
1073 :
1074 : /// \param arg0 A data expression.
1075 : /// \param arg1 A data expression.
1076 : inline
1077 : void make_minus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1078 : {
1079 : make_application(result, sort_int::minus(arg0.sort(), arg1.sort()),arg0, arg1);
1080 : }
1081 :
1082 : /// \brief Recogniser for application of -.
1083 : /// \param e A data expression.
1084 : /// \return true iff e is an application of function symbol minus to a
1085 : /// number of arguments.
1086 : inline
1087 40371 : bool is_minus_application(const atermpp::aterm_appl& e)
1088 : {
1089 40371 : return is_application(e) && is_minus_function_symbol(atermpp::down_cast<application>(e).head());
1090 : }
1091 :
1092 : /// \brief Generate identifier *.
1093 : /// \return Identifier *.
1094 : inline
1095 95160 : const core::identifier_string& times_name()
1096 : {
1097 95160 : static core::identifier_string times_name = core::identifier_string("*");
1098 95160 : return times_name;
1099 : }
1100 :
1101 : // This function is not intended for public use and therefore not documented in Doxygen.
1102 : inline
1103 56375 : function_symbol times(const sort_expression& s0, const sort_expression& s1)
1104 : {
1105 56375 : sort_expression target_sort;
1106 56375 : if (s0 == int_() && s1 == int_())
1107 : {
1108 32867 : target_sort = int_();
1109 : }
1110 23508 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1111 : {
1112 17253 : target_sort = sort_nat::nat();
1113 : }
1114 6255 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
1115 : {
1116 6255 : target_sort = sort_pos::pos();
1117 : }
1118 : else
1119 : {
1120 0 : throw mcrl2::runtime_error("Cannot compute target sort for times with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1121 : }
1122 :
1123 56375 : function_symbol times(times_name(), make_function_sort_(s0, s1, target_sort));
1124 112750 : return times;
1125 56375 : }
1126 :
1127 : /// \brief Recogniser for function *.
1128 : /// \param e A data expression.
1129 : /// \return true iff e is the function symbol matching *.
1130 : inline
1131 39575 : bool is_times_function_symbol(const atermpp::aterm_appl& e)
1132 : {
1133 39575 : if (is_function_symbol(e))
1134 : {
1135 38341 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1136 38341 : return f.name() == times_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == times(int_(), int_()) || f == times(sort_nat::nat(), sort_nat::nat()) || f == times(sort_pos::pos(), sort_pos::pos()));
1137 : }
1138 1234 : return false;
1139 : }
1140 :
1141 : /// \brief Application of function symbol *.
1142 :
1143 : /// \param arg0 A data expression.
1144 : /// \param arg1 A data expression.
1145 : /// \return Application of * to a number of arguments.
1146 : inline
1147 43868 : application times(const data_expression& arg0, const data_expression& arg1)
1148 : {
1149 87736 : return sort_int::times(arg0.sort(), arg1.sort())(arg0, arg1);
1150 : }
1151 :
1152 : /// \brief Make an application of function symbol *.
1153 : /// \param result The data expression where the * expression is put.
1154 :
1155 : /// \param arg0 A data expression.
1156 : /// \param arg1 A data expression.
1157 : inline
1158 : void make_times(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1159 : {
1160 : make_application(result, sort_int::times(arg0.sort(), arg1.sort()),arg0, arg1);
1161 : }
1162 :
1163 : /// \brief Recogniser for application of *.
1164 : /// \param e A data expression.
1165 : /// \return true iff e is an application of function symbol times to a
1166 : /// number of arguments.
1167 : inline
1168 39979 : bool is_times_application(const atermpp::aterm_appl& e)
1169 : {
1170 39979 : return is_application(e) && is_times_function_symbol(atermpp::down_cast<application>(e).head());
1171 : }
1172 :
1173 : /// \brief Generate identifier div.
1174 : /// \return Identifier div.
1175 : inline
1176 81997 : const core::identifier_string& div_name()
1177 : {
1178 81997 : static core::identifier_string div_name = core::identifier_string("div");
1179 81997 : return div_name;
1180 : }
1181 :
1182 : // This function is not intended for public use and therefore not documented in Doxygen.
1183 : inline
1184 43056 : function_symbol div(const sort_expression& s0, const sort_expression& s1)
1185 : {
1186 43056 : sort_expression target_sort;
1187 43056 : if (s0 == int_() && s1 == sort_pos::pos())
1188 : {
1189 32015 : target_sort = int_();
1190 : }
1191 11041 : else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
1192 : {
1193 11041 : target_sort = sort_nat::nat();
1194 : }
1195 : else
1196 : {
1197 0 : throw mcrl2::runtime_error("Cannot compute target sort for div with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1198 : }
1199 :
1200 43056 : function_symbol div(div_name(), make_function_sort_(s0, s1, target_sort));
1201 86112 : return div;
1202 43056 : }
1203 :
1204 : /// \brief Recogniser for function div.
1205 : /// \param e A data expression.
1206 : /// \return true iff e is the function symbol matching div.
1207 : inline
1208 39728 : bool is_div_function_symbol(const atermpp::aterm_appl& e)
1209 : {
1210 39728 : if (is_function_symbol(e))
1211 : {
1212 38494 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1213 38494 : return f.name() == div_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == div(int_(), sort_pos::pos()) || f == div(sort_nat::nat(), sort_pos::pos()));
1214 : }
1215 1234 : return false;
1216 : }
1217 :
1218 : /// \brief Application of function symbol div.
1219 :
1220 : /// \param arg0 A data expression.
1221 : /// \param arg1 A data expression.
1222 : /// \return Application of div to a number of arguments.
1223 : inline
1224 32798 : application div(const data_expression& arg0, const data_expression& arg1)
1225 : {
1226 65596 : return sort_int::div(arg0.sort(), arg1.sort())(arg0, arg1);
1227 : }
1228 :
1229 : /// \brief Make an application of function symbol div.
1230 : /// \param result The data expression where the div expression is put.
1231 :
1232 : /// \param arg0 A data expression.
1233 : /// \param arg1 A data expression.
1234 : inline
1235 : void make_div(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1236 : {
1237 : make_application(result, sort_int::div(arg0.sort(), arg1.sort()),arg0, arg1);
1238 : }
1239 :
1240 : /// \brief Recogniser for application of div.
1241 : /// \param e A data expression.
1242 : /// \return true iff e is an application of function symbol div to a
1243 : /// number of arguments.
1244 : inline
1245 40132 : bool is_div_application(const atermpp::aterm_appl& e)
1246 : {
1247 40132 : return is_application(e) && is_div_function_symbol(atermpp::down_cast<application>(e).head());
1248 : }
1249 :
1250 : /// \brief Generate identifier mod.
1251 : /// \return Identifier mod.
1252 : inline
1253 76572 : const core::identifier_string& mod_name()
1254 : {
1255 76572 : static core::identifier_string mod_name = core::identifier_string("mod");
1256 76572 : return mod_name;
1257 : }
1258 :
1259 : // This function is not intended for public use and therefore not documented in Doxygen.
1260 : inline
1261 37681 : function_symbol mod(const sort_expression& s0, const sort_expression& s1)
1262 : {
1263 37681 : sort_expression target_sort(sort_nat::nat());
1264 37681 : function_symbol mod(mod_name(), make_function_sort_(s0, s1, target_sort));
1265 75362 : return mod;
1266 37681 : }
1267 :
1268 : /// \brief Recogniser for function mod.
1269 : /// \param e A data expression.
1270 : /// \return true iff e is the function symbol matching mod.
1271 : inline
1272 39678 : bool is_mod_function_symbol(const atermpp::aterm_appl& e)
1273 : {
1274 39678 : if (is_function_symbol(e))
1275 : {
1276 38444 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1277 38444 : return f.name() == mod_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == mod(int_(), sort_pos::pos()) || f == mod(sort_nat::nat(), sort_pos::pos()));
1278 : }
1279 1234 : return false;
1280 : }
1281 :
1282 : /// \brief Application of function symbol mod.
1283 :
1284 : /// \param arg0 A data expression.
1285 : /// \param arg1 A data expression.
1286 : /// \return Application of mod to a number of arguments.
1287 : inline
1288 27367 : application mod(const data_expression& arg0, const data_expression& arg1)
1289 : {
1290 54734 : return sort_int::mod(arg0.sort(), arg1.sort())(arg0, arg1);
1291 : }
1292 :
1293 : /// \brief Make an application of function symbol mod.
1294 : /// \param result The data expression where the mod expression is put.
1295 :
1296 : /// \param arg0 A data expression.
1297 : /// \param arg1 A data expression.
1298 : inline
1299 : void make_mod(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1300 : {
1301 : make_application(result, sort_int::mod(arg0.sort(), arg1.sort()),arg0, arg1);
1302 : }
1303 :
1304 : /// \brief Recogniser for application of mod.
1305 : /// \param e A data expression.
1306 : /// \return true iff e is an application of function symbol mod to a
1307 : /// number of arguments.
1308 : inline
1309 40082 : bool is_mod_application(const atermpp::aterm_appl& e)
1310 : {
1311 40082 : return is_application(e) && is_mod_function_symbol(atermpp::down_cast<application>(e).head());
1312 : }
1313 :
1314 : /// \brief Generate identifier exp.
1315 : /// \return Identifier exp.
1316 : inline
1317 42960 : const core::identifier_string& exp_name()
1318 : {
1319 42960 : static core::identifier_string exp_name = core::identifier_string("exp");
1320 42960 : return exp_name;
1321 : }
1322 :
1323 : // This function is not intended for public use and therefore not documented in Doxygen.
1324 : inline
1325 42960 : function_symbol exp(const sort_expression& s0, const sort_expression& s1)
1326 : {
1327 42960 : sort_expression target_sort;
1328 42960 : if (s0 == int_() && s1 == sort_nat::nat())
1329 : {
1330 26511 : target_sort = int_();
1331 : }
1332 16449 : else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
1333 : {
1334 10966 : target_sort = sort_pos::pos();
1335 : }
1336 5483 : else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
1337 : {
1338 5483 : target_sort = sort_nat::nat();
1339 : }
1340 : else
1341 : {
1342 0 : throw mcrl2::runtime_error("Cannot compute target sort for exp with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1343 : }
1344 :
1345 42960 : function_symbol exp(exp_name(), make_function_sort_(s0, s1, target_sort));
1346 85920 : return exp;
1347 42960 : }
1348 :
1349 : /// \brief Recogniser for function exp.
1350 : /// \param e A data expression.
1351 : /// \return true iff e is the function symbol matching exp.
1352 : inline
1353 0 : bool is_exp_function_symbol(const atermpp::aterm_appl& e)
1354 : {
1355 0 : if (is_function_symbol(e))
1356 : {
1357 0 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1358 0 : return f.name() == exp_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == exp(int_(), sort_nat::nat()) || f == exp(sort_pos::pos(), sort_nat::nat()) || f == exp(sort_nat::nat(), sort_nat::nat()));
1359 : }
1360 0 : return false;
1361 : }
1362 :
1363 : /// \brief Application of function symbol exp.
1364 :
1365 : /// \param arg0 A data expression.
1366 : /// \param arg1 A data expression.
1367 : /// \return Application of exp to a number of arguments.
1368 : inline
1369 32899 : application exp(const data_expression& arg0, const data_expression& arg1)
1370 : {
1371 65798 : return sort_int::exp(arg0.sort(), arg1.sort())(arg0, arg1);
1372 : }
1373 :
1374 : /// \brief Make an application of function symbol exp.
1375 : /// \param result The data expression where the exp expression is put.
1376 :
1377 : /// \param arg0 A data expression.
1378 : /// \param arg1 A data expression.
1379 : inline
1380 : void make_exp(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1381 : {
1382 : make_application(result, sort_int::exp(arg0.sort(), arg1.sort()),arg0, arg1);
1383 : }
1384 :
1385 : /// \brief Recogniser for application of exp.
1386 : /// \param e A data expression.
1387 : /// \return true iff e is an application of function symbol exp to a
1388 : /// number of arguments.
1389 : inline
1390 0 : bool is_exp_application(const atermpp::aterm_appl& e)
1391 : {
1392 0 : return is_application(e) && is_exp_function_symbol(atermpp::down_cast<application>(e).head());
1393 : }
1394 : /// \brief Give all system defined mappings for int_
1395 : /// \return All system defined mappings for int_
1396 : inline
1397 5483 : function_symbol_vector int_generate_functions_code()
1398 : {
1399 5483 : function_symbol_vector result;
1400 5483 : result.push_back(sort_int::nat2int());
1401 5483 : result.push_back(sort_int::int2nat());
1402 5483 : result.push_back(sort_int::pos2int());
1403 5483 : result.push_back(sort_int::int2pos());
1404 5483 : result.push_back(sort_int::maximum(sort_pos::pos(), int_()));
1405 5483 : result.push_back(sort_int::maximum(int_(), sort_pos::pos()));
1406 5483 : result.push_back(sort_int::maximum(sort_nat::nat(), int_()));
1407 5483 : result.push_back(sort_int::maximum(int_(), sort_nat::nat()));
1408 5483 : result.push_back(sort_int::maximum(int_(), int_()));
1409 5483 : result.push_back(sort_int::minimum(int_(), int_()));
1410 5483 : result.push_back(sort_int::abs());
1411 5483 : result.push_back(sort_int::negate(sort_pos::pos()));
1412 5483 : result.push_back(sort_int::negate(sort_nat::nat()));
1413 5483 : result.push_back(sort_int::negate(int_()));
1414 5483 : result.push_back(sort_int::succ(int_()));
1415 5483 : result.push_back(sort_int::pred(sort_nat::nat()));
1416 5483 : result.push_back(sort_int::pred(int_()));
1417 5483 : result.push_back(sort_int::plus(int_(), int_()));
1418 5483 : result.push_back(sort_int::minus(sort_pos::pos(), sort_pos::pos()));
1419 5483 : result.push_back(sort_int::minus(sort_nat::nat(), sort_nat::nat()));
1420 5483 : result.push_back(sort_int::minus(int_(), int_()));
1421 5483 : result.push_back(sort_int::times(int_(), int_()));
1422 5483 : result.push_back(sort_int::div(int_(), sort_pos::pos()));
1423 5483 : result.push_back(sort_int::mod(int_(), sort_pos::pos()));
1424 5483 : result.push_back(sort_int::exp(int_(), sort_nat::nat()));
1425 5483 : return result;
1426 0 : }
1427 :
1428 : /// \brief Give all system defined mappings and constructors for int_
1429 : /// \return All system defined mappings for int_
1430 : inline
1431 : function_symbol_vector int_generate_constructors_and_functions_code()
1432 : {
1433 : function_symbol_vector result=int_generate_functions_code();
1434 : for(const function_symbol& f: int_generate_constructors_code())
1435 : {
1436 : result.push_back(f);
1437 : }
1438 : return result;
1439 : }
1440 :
1441 : /// \brief Give all system defined mappings that can be used in mCRL2 specs for int_
1442 : /// \return All system defined mappings for that can be used in mCRL2 specificationis int_
1443 : inline
1444 4578 : function_symbol_vector int_mCRL2_usable_mappings()
1445 : {
1446 4578 : function_symbol_vector result;
1447 4578 : result.push_back(sort_int::nat2int());
1448 4578 : result.push_back(sort_int::int2nat());
1449 4578 : result.push_back(sort_int::pos2int());
1450 4578 : result.push_back(sort_int::int2pos());
1451 4578 : result.push_back(sort_int::maximum(sort_pos::pos(), int_()));
1452 4578 : result.push_back(sort_int::maximum(int_(), sort_pos::pos()));
1453 4578 : result.push_back(sort_int::maximum(sort_nat::nat(), int_()));
1454 4578 : result.push_back(sort_int::maximum(int_(), sort_nat::nat()));
1455 4578 : result.push_back(sort_int::maximum(int_(), int_()));
1456 4578 : result.push_back(sort_int::minimum(int_(), int_()));
1457 4578 : result.push_back(sort_int::abs());
1458 4578 : result.push_back(sort_int::negate(sort_pos::pos()));
1459 4578 : result.push_back(sort_int::negate(sort_nat::nat()));
1460 4578 : result.push_back(sort_int::negate(int_()));
1461 4578 : result.push_back(sort_int::succ(int_()));
1462 4578 : result.push_back(sort_int::pred(sort_nat::nat()));
1463 4578 : result.push_back(sort_int::pred(int_()));
1464 4578 : result.push_back(sort_int::plus(int_(), int_()));
1465 4578 : result.push_back(sort_int::minus(sort_pos::pos(), sort_pos::pos()));
1466 4578 : result.push_back(sort_int::minus(sort_nat::nat(), sort_nat::nat()));
1467 4578 : result.push_back(sort_int::minus(int_(), int_()));
1468 4578 : result.push_back(sort_int::times(int_(), int_()));
1469 4578 : result.push_back(sort_int::div(int_(), sort_pos::pos()));
1470 4578 : result.push_back(sort_int::mod(int_(), sort_pos::pos()));
1471 4578 : result.push_back(sort_int::exp(int_(), sort_nat::nat()));
1472 4578 : return result;
1473 0 : }
1474 :
1475 :
1476 : // 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
1477 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
1478 : /// \brief Give all system defined mappings that are to be implemented in C++ code for int_
1479 : /// \return A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for int_
1480 : inline
1481 10914 : implementation_map int_cpp_implementable_mappings()
1482 : {
1483 10914 : implementation_map result;
1484 10914 : return result;
1485 : }
1486 : ///\brief Function for projecting out argument.
1487 : /// arg from an application.
1488 : /// \param e A data expression.
1489 : /// \pre arg is defined for e.
1490 : /// \return The argument of e that corresponds to arg.
1491 : inline
1492 533 : const data_expression& arg(const data_expression& e)
1493 : {
1494 533 : assert(is_cint_application(e) || is_cneg_application(e) || is_nat2int_application(e) || is_int2nat_application(e) || is_pos2int_application(e) || is_int2pos_application(e) || is_abs_application(e) || is_negate_application(e) || is_succ_application(e) || is_pred_application(e));
1495 533 : return atermpp::down_cast<application>(e)[0];
1496 : }
1497 :
1498 : ///\brief Function for projecting out argument.
1499 : /// left from an application.
1500 : /// \param e A data expression.
1501 : /// \pre left is defined for e.
1502 : /// \return The argument of e that corresponds to left.
1503 : inline
1504 23 : const data_expression& left(const data_expression& e)
1505 : {
1506 23 : assert(is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_minus_application(e) || is_times_application(e) || is_div_application(e) || is_mod_application(e) || is_exp_application(e));
1507 23 : return atermpp::down_cast<application>(e)[0];
1508 : }
1509 :
1510 : ///\brief Function for projecting out argument.
1511 : /// right from an application.
1512 : /// \param e A data expression.
1513 : /// \pre right is defined for e.
1514 : /// \return The argument of e that corresponds to right.
1515 : inline
1516 22 : const data_expression& right(const data_expression& e)
1517 : {
1518 22 : assert(is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_minus_application(e) || is_times_application(e) || is_div_application(e) || is_mod_application(e) || is_exp_application(e));
1519 22 : return atermpp::down_cast<application>(e)[1];
1520 : }
1521 :
1522 : /// \brief Give all system defined equations for int_
1523 : /// \return All system defined equations for sort int_
1524 : inline
1525 5483 : data_equation_vector int_generate_equations_code()
1526 : {
1527 10966 : variable vb("b",sort_bool::bool_());
1528 10966 : variable vn("n",sort_nat::nat());
1529 10966 : variable vm("m",sort_nat::nat());
1530 10966 : variable vp("p",sort_pos::pos());
1531 10966 : variable vq("q",sort_pos::pos());
1532 10966 : variable vx("x",int_());
1533 10966 : variable vy("y",int_());
1534 :
1535 5483 : data_equation_vector result;
1536 16449 : result.push_back(data_equation(variable_list({vm, vn}), equal_to(cint(vm), cint(vn)), equal_to(vm, vn)));
1537 16449 : result.push_back(data_equation(variable_list({vn, vp}), equal_to(cint(vn), cneg(vp)), sort_bool::false_()));
1538 16449 : result.push_back(data_equation(variable_list({vn, vp}), equal_to(cneg(vp), cint(vn)), sort_bool::false_()));
1539 16449 : result.push_back(data_equation(variable_list({vp, vq}), equal_to(cneg(vp), cneg(vq)), equal_to(vp, vq)));
1540 16449 : result.push_back(data_equation(variable_list({vm, vn}), less(cint(vm), cint(vn)), less(vm, vn)));
1541 16449 : result.push_back(data_equation(variable_list({vn, vp}), less(cint(vn), cneg(vp)), sort_bool::false_()));
1542 16449 : result.push_back(data_equation(variable_list({vn, vp}), less(cneg(vp), cint(vn)), sort_bool::true_()));
1543 16449 : result.push_back(data_equation(variable_list({vp, vq}), less(cneg(vp), cneg(vq)), less(vq, vp)));
1544 16449 : result.push_back(data_equation(variable_list({vm, vn}), less_equal(cint(vm), cint(vn)), less_equal(vm, vn)));
1545 16449 : result.push_back(data_equation(variable_list({vn, vp}), less_equal(cint(vn), cneg(vp)), sort_bool::false_()));
1546 16449 : result.push_back(data_equation(variable_list({vn, vp}), less_equal(cneg(vp), cint(vn)), sort_bool::true_()));
1547 16449 : result.push_back(data_equation(variable_list({vp, vq}), less_equal(cneg(vp), cneg(vq)), less_equal(vq, vp)));
1548 10966 : result.push_back(data_equation(variable_list({vn}), nat2int(vn), cint(vn)));
1549 10966 : result.push_back(data_equation(variable_list({vn}), int2nat(cint(vn)), vn));
1550 10966 : result.push_back(data_equation(variable_list({vp}), pos2int(vp), cint(sort_nat::cnat(vp))));
1551 10966 : result.push_back(data_equation(variable_list({vn}), int2pos(cint(vn)), sort_nat::nat2pos(vn)));
1552 16449 : result.push_back(data_equation(variable_list({vn, vp}), maximum(vp, cint(vn)), maximum(vp, vn)));
1553 16449 : result.push_back(data_equation(variable_list({vp, vq}), maximum(vp, cneg(vq)), vp));
1554 16449 : result.push_back(data_equation(variable_list({vn, vp}), maximum(cint(vn), vp), maximum(vn, vp)));
1555 16449 : result.push_back(data_equation(variable_list({vp, vq}), maximum(cneg(vq), vp), vp));
1556 16449 : result.push_back(data_equation(variable_list({vm, vn}), maximum(vm, cint(vn)), if_(less_equal(vm, vn), vn, vm)));
1557 16449 : result.push_back(data_equation(variable_list({vn, vp}), maximum(vn, cneg(vp)), vn));
1558 16449 : result.push_back(data_equation(variable_list({vm, vn}), maximum(cint(vm), vn), if_(less_equal(vm, vn), vn, vm)));
1559 16449 : result.push_back(data_equation(variable_list({vn, vp}), maximum(cneg(vp), vn), vn));
1560 16449 : result.push_back(data_equation(variable_list({vx, vy}), maximum(vx, vy), if_(less_equal(vx, vy), vy, vx)));
1561 16449 : result.push_back(data_equation(variable_list({vx, vy}), minimum(vx, vy), if_(less_equal(vx, vy), vx, vy)));
1562 10966 : result.push_back(data_equation(variable_list({vn}), abs(cint(vn)), vn));
1563 10966 : result.push_back(data_equation(variable_list({vp}), abs(cneg(vp)), sort_nat::cnat(vp)));
1564 10966 : result.push_back(data_equation(variable_list({vp}), negate(vp), cneg(vp)));
1565 5483 : result.push_back(data_equation(variable_list(), negate(sort_nat::c0()), cint(sort_nat::c0())));
1566 10966 : result.push_back(data_equation(variable_list({vp}), negate(sort_nat::cnat(vp)), cneg(vp)));
1567 10966 : result.push_back(data_equation(variable_list({vn}), negate(cint(vn)), negate(vn)));
1568 10966 : result.push_back(data_equation(variable_list({vp}), negate(cneg(vp)), cint(sort_nat::cnat(vp))));
1569 10966 : result.push_back(data_equation(variable_list({vn}), succ(cint(vn)), cint(sort_nat::cnat(succ(vn)))));
1570 10966 : result.push_back(data_equation(variable_list({vp}), succ(cneg(vp)), negate(pred(vp))));
1571 5483 : result.push_back(data_equation(variable_list(), pred(sort_nat::c0()), cneg(sort_pos::c1())));
1572 10966 : result.push_back(data_equation(variable_list({vp}), pred(sort_nat::cnat(vp)), cint(pred(vp))));
1573 10966 : result.push_back(data_equation(variable_list({vn}), pred(cint(vn)), pred(vn)));
1574 10966 : result.push_back(data_equation(variable_list({vp}), pred(cneg(vp)), cneg(succ(vp))));
1575 16449 : result.push_back(data_equation(variable_list({vm, vn}), plus(cint(vm), cint(vn)), cint(plus(vm, vn))));
1576 16449 : result.push_back(data_equation(variable_list({vn, vp}), plus(cint(vn), cneg(vp)), minus(vn, sort_nat::cnat(vp))));
1577 16449 : result.push_back(data_equation(variable_list({vn, vp}), plus(cneg(vp), cint(vn)), minus(vn, sort_nat::cnat(vp))));
1578 16449 : result.push_back(data_equation(variable_list({vp, vq}), plus(cneg(vp), cneg(vq)), cneg(sort_pos::add_with_carry(sort_bool::false_(), vp, vq))));
1579 16449 : result.push_back(data_equation(variable_list({vp, vq}), less_equal(vq, vp), minus(vp, vq), cint(sort_nat::gte_subtract_with_borrow(sort_bool::false_(), vp, vq))));
1580 16449 : result.push_back(data_equation(variable_list({vp, vq}), less(vp, vq), minus(vp, vq), negate(sort_nat::gte_subtract_with_borrow(sort_bool::false_(), vq, vp))));
1581 16449 : result.push_back(data_equation(variable_list({vm, vn}), less_equal(vn, vm), minus(vm, vn), cint(sort_nat::monus(vm, vn))));
1582 16449 : result.push_back(data_equation(variable_list({vm, vn}), less(vm, vn), minus(vm, vn), negate(sort_nat::monus(vn, vm))));
1583 16449 : result.push_back(data_equation(variable_list({vx, vy}), minus(vx, vy), plus(vx, negate(vy))));
1584 16449 : result.push_back(data_equation(variable_list({vm, vn}), times(cint(vm), cint(vn)), cint(times(vm, vn))));
1585 16449 : result.push_back(data_equation(variable_list({vn, vp}), times(cint(vn), cneg(vp)), negate(times(sort_nat::cnat(vp), vn))));
1586 16449 : result.push_back(data_equation(variable_list({vn, vp}), times(cneg(vp), cint(vn)), negate(times(sort_nat::cnat(vp), vn))));
1587 16449 : result.push_back(data_equation(variable_list({vp, vq}), times(cneg(vp), cneg(vq)), cint(sort_nat::cnat(times(vp, vq)))));
1588 16449 : result.push_back(data_equation(variable_list({vn, vp}), div(cint(vn), vp), cint(div(vn, vp))));
1589 16449 : result.push_back(data_equation(variable_list({vp, vq}), div(cneg(vp), vq), cneg(succ(div(pred(vp), vq)))));
1590 16449 : result.push_back(data_equation(variable_list({vn, vp}), mod(cint(vn), vp), mod(vn, vp)));
1591 16449 : result.push_back(data_equation(variable_list({vp, vq}), mod(cneg(vp), vq), int2nat(minus(vq, succ(mod(pred(vp), vq))))));
1592 16449 : result.push_back(data_equation(variable_list({vm, vn}), exp(cint(vm), vn), cint(exp(vm, vn))));
1593 16449 : result.push_back(data_equation(variable_list({vn, vp}), sort_nat::even(vn), exp(cneg(vp), vn), cint(sort_nat::cnat(exp(vp, vn)))));
1594 16449 : result.push_back(data_equation(variable_list({vn, vp}), sort_bool::not_(sort_nat::even(vn)), exp(cneg(vp), vn), cneg(exp(vp, vn))));
1595 10966 : return result;
1596 5483 : }
1597 :
1598 : } // namespace sort_int_
1599 :
1600 : } // namespace data
1601 :
1602 : } // namespace mcrl2
1603 :
1604 : #endif // MCRL2_DATA_INT_H
|
