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/nat.h
10 : /// \brief The standard sort nat.
11 : ///
12 : /// This file was generated from the data sort specification
13 : /// mcrl2/data/build/nat.spec.
14 :
15 : #ifndef MCRL2_DATA_NAT_H
16 : #define MCRL2_DATA_NAT_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 :
29 : namespace mcrl2 {
30 :
31 : namespace data {
32 :
33 : /// \brief Namespace for system defined sort nat.
34 : namespace sort_nat {
35 :
36 : inline
37 119 : const core::identifier_string& nat_name()
38 : {
39 119 : static core::identifier_string nat_name = core::identifier_string("Nat");
40 119 : return nat_name;
41 : }
42 :
43 : /// \brief Constructor for sort expression Nat.
44 : /// \return Sort expression Nat.
45 : inline
46 2088262 : const basic_sort& nat()
47 : {
48 2088262 : static basic_sort nat = basic_sort(nat_name());
49 2088262 : return nat;
50 : }
51 :
52 : /// \brief Recogniser for sort expression Nat
53 : /// \param e A sort expression
54 : /// \return true iff e == nat()
55 : inline
56 201312 : bool is_nat(const sort_expression& e)
57 : {
58 201312 : if (is_basic_sort(e))
59 : {
60 34237 : return basic_sort(e) == nat();
61 : }
62 167075 : return false;
63 : }
64 :
65 : inline
66 112 : const core::identifier_string& natpair_name()
67 : {
68 112 : static core::identifier_string natpair_name = core::identifier_string("@NatPair");
69 112 : return natpair_name;
70 : }
71 :
72 : /// \brief Constructor for sort expression \@NatPair.
73 : /// \return Sort expression \@NatPair.
74 : inline
75 2780 : const basic_sort& natpair()
76 : {
77 2780 : static basic_sort natpair = basic_sort(natpair_name());
78 2780 : return natpair;
79 : }
80 :
81 : /// \brief Recogniser for sort expression \@NatPair
82 : /// \param e A sort expression
83 : /// \return true iff e == natpair()
84 : inline
85 : bool is_natpair(const sort_expression& e)
86 : {
87 : if (is_basic_sort(e))
88 : {
89 : return basic_sort(e) == natpair();
90 : }
91 : return false;
92 : }
93 :
94 :
95 : /// \brief Generate identifier \@c0.
96 : /// \return Identifier \@c0.
97 : inline
98 113 : const core::identifier_string& c0_name()
99 : {
100 113 : static core::identifier_string c0_name = core::identifier_string("@c0");
101 113 : return c0_name;
102 : }
103 :
104 : /// \brief Constructor for function symbol \@c0.
105 :
106 : /// \return Function symbol c0.
107 : inline
108 597818 : const function_symbol& c0()
109 : {
110 597818 : static function_symbol c0(c0_name(), nat());
111 597818 : return c0;
112 : }
113 :
114 : /// \brief Recogniser for function \@c0.
115 : /// \param e A data expression.
116 : /// \return true iff e is the function symbol matching \@c0.
117 : inline
118 48999 : bool is_c0_function_symbol(const atermpp::aterm_appl& e)
119 : {
120 48999 : if (is_function_symbol(e))
121 : {
122 48858 : return atermpp::down_cast<function_symbol>(e) == c0();
123 : }
124 141 : return false;
125 : }
126 :
127 : /// \brief Generate identifier \@cNat.
128 : /// \return Identifier \@cNat.
129 : inline
130 113 : const core::identifier_string& cnat_name()
131 : {
132 113 : static core::identifier_string cnat_name = core::identifier_string("@cNat");
133 113 : return cnat_name;
134 : }
135 :
136 : /// \brief Constructor for function symbol \@cNat.
137 :
138 : /// \return Function symbol cnat.
139 : inline
140 1142423 : const function_symbol& cnat()
141 : {
142 1142423 : static function_symbol cnat(cnat_name(), make_function_sort_(sort_pos::pos(), nat()));
143 1142423 : return cnat;
144 : }
145 :
146 : /// \brief Recogniser for function \@cNat.
147 : /// \param e A data expression.
148 : /// \return true iff e is the function symbol matching \@cNat.
149 : inline
150 176884 : bool is_cnat_function_symbol(const atermpp::aterm_appl& e)
151 : {
152 176884 : if (is_function_symbol(e))
153 : {
154 173298 : return atermpp::down_cast<function_symbol>(e) == cnat();
155 : }
156 3586 : return false;
157 : }
158 :
159 : /// \brief Application of function symbol \@cNat.
160 :
161 : /// \param arg0 A data expression.
162 : /// \return Application of \@cNat to a number of arguments.
163 : inline
164 950864 : application cnat(const data_expression& arg0)
165 : {
166 950864 : return sort_nat::cnat()(arg0);
167 : }
168 :
169 : /// \brief Make an application of function symbol \@cNat.
170 : /// \param result The data expression where the \@cNat expression is put.
171 :
172 : /// \param arg0 A data expression.
173 : inline
174 : void make_cnat(data_expression& result, const data_expression& arg0)
175 : {
176 : make_application(result, sort_nat::cnat(),arg0);
177 : }
178 :
179 : /// \brief Recogniser for application of \@cNat.
180 : /// \param e A data expression.
181 : /// \return true iff e is an application of function symbol cnat to a
182 : /// number of arguments.
183 : inline
184 179712 : bool is_cnat_application(const atermpp::aterm_appl& e)
185 : {
186 179712 : return is_application(e) && is_cnat_function_symbol(atermpp::down_cast<application>(e).head());
187 : }
188 :
189 : /// \brief Generate identifier \@cPair.
190 : /// \return Identifier \@cPair.
191 : inline
192 112 : const core::identifier_string& cpair_name()
193 : {
194 112 : static core::identifier_string cpair_name = core::identifier_string("@cPair");
195 112 : return cpair_name;
196 : }
197 :
198 : /// \brief Constructor for function symbol \@cPair.
199 :
200 : /// \return Function symbol cpair.
201 : inline
202 99018 : const function_symbol& cpair()
203 : {
204 99018 : static function_symbol cpair(cpair_name(), make_function_sort_(nat(), nat(), natpair()));
205 99018 : return cpair;
206 : }
207 :
208 : /// \brief Recogniser for function \@cPair.
209 : /// \param e A data expression.
210 : /// \return true iff e is the function symbol matching \@cPair.
211 : inline
212 : bool is_cpair_function_symbol(const atermpp::aterm_appl& e)
213 : {
214 : if (is_function_symbol(e))
215 : {
216 : return atermpp::down_cast<function_symbol>(e) == cpair();
217 : }
218 : return false;
219 : }
220 :
221 : /// \brief Application of function symbol \@cPair.
222 :
223 : /// \param arg0 A data expression.
224 : /// \param arg1 A data expression.
225 : /// \return Application of \@cPair to a number of arguments.
226 : inline
227 88144 : application cpair(const data_expression& arg0, const data_expression& arg1)
228 : {
229 88144 : return sort_nat::cpair()(arg0, arg1);
230 : }
231 :
232 : /// \brief Make an application of function symbol \@cPair.
233 : /// \param result The data expression where the \@cPair expression is put.
234 :
235 : /// \param arg0 A data expression.
236 : /// \param arg1 A data expression.
237 : inline
238 : void make_cpair(data_expression& result, const data_expression& arg0, const data_expression& arg1)
239 : {
240 : make_application(result, sort_nat::cpair(),arg0, arg1);
241 : }
242 :
243 : /// \brief Recogniser for application of \@cPair.
244 : /// \param e A data expression.
245 : /// \return true iff e is an application of function symbol cpair to a
246 : /// number of arguments.
247 : inline
248 : bool is_cpair_application(const atermpp::aterm_appl& e)
249 : {
250 : return is_application(e) && is_cpair_function_symbol(atermpp::down_cast<application>(e).head());
251 : }
252 : /// \brief Give all system defined constructors for nat.
253 : /// \return All system defined constructors for nat.
254 : inline
255 6296 : function_symbol_vector nat_generate_constructors_code()
256 : {
257 6296 : function_symbol_vector result;
258 6296 : result.push_back(sort_nat::c0());
259 6296 : result.push_back(sort_nat::cnat());
260 6296 : result.push_back(sort_nat::cpair());
261 :
262 6296 : return result;
263 0 : }
264 : /// \brief Give all defined constructors which can be used in mCRL2 specs for nat.
265 : /// \return All system defined constructors that can be used in an mCRL2 specification for nat.
266 : inline
267 4578 : function_symbol_vector nat_mCRL2_usable_constructors()
268 : {
269 4578 : function_symbol_vector result;
270 4578 : result.push_back(sort_nat::c0());
271 4578 : result.push_back(sort_nat::cnat());
272 4578 : result.push_back(sort_nat::cpair());
273 :
274 4578 : return result;
275 0 : }
276 : // 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
277 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
278 : /// \brief Give all system defined constructors which have an implementation in C++ and not in rewrite rules for nat.
279 : /// \return All system defined constructors that are to be implemented in C++ for nat.
280 : inline
281 6296 : implementation_map nat_cpp_implementable_constructors()
282 : {
283 6296 : implementation_map result;
284 6296 : return result;
285 : }
286 :
287 : /// \brief Generate identifier Pos2Nat.
288 : /// \return Identifier Pos2Nat.
289 : inline
290 112 : const core::identifier_string& pos2nat_name()
291 : {
292 112 : static core::identifier_string pos2nat_name = core::identifier_string("Pos2Nat");
293 112 : return pos2nat_name;
294 : }
295 :
296 : /// \brief Constructor for function symbol Pos2Nat.
297 :
298 : /// \return Function symbol pos2nat.
299 : inline
300 184254 : const function_symbol& pos2nat()
301 : {
302 184254 : static function_symbol pos2nat(pos2nat_name(), make_function_sort_(sort_pos::pos(), nat()));
303 184254 : return pos2nat;
304 : }
305 :
306 : /// \brief Recogniser for function Pos2Nat.
307 : /// \param e A data expression.
308 : /// \return true iff e is the function symbol matching Pos2Nat.
309 : inline
310 170583 : bool is_pos2nat_function_symbol(const atermpp::aterm_appl& e)
311 : {
312 170583 : if (is_function_symbol(e))
313 : {
314 166997 : return atermpp::down_cast<function_symbol>(e) == pos2nat();
315 : }
316 3586 : return false;
317 : }
318 :
319 : /// \brief Application of function symbol Pos2Nat.
320 :
321 : /// \param arg0 A data expression.
322 : /// \return Application of Pos2Nat to a number of arguments.
323 : inline
324 6312 : application pos2nat(const data_expression& arg0)
325 : {
326 6312 : return sort_nat::pos2nat()(arg0);
327 : }
328 :
329 : /// \brief Make an application of function symbol Pos2Nat.
330 : /// \param result The data expression where the Pos2Nat expression is put.
331 :
332 : /// \param arg0 A data expression.
333 : inline
334 : void make_pos2nat(data_expression& result, const data_expression& arg0)
335 : {
336 : make_application(result, sort_nat::pos2nat(),arg0);
337 : }
338 :
339 : /// \brief Recogniser for application of Pos2Nat.
340 : /// \param e A data expression.
341 : /// \return true iff e is an application of function symbol pos2nat to a
342 : /// number of arguments.
343 : inline
344 173411 : bool is_pos2nat_application(const atermpp::aterm_appl& e)
345 : {
346 173411 : return is_application(e) && is_pos2nat_function_symbol(atermpp::down_cast<application>(e).head());
347 : }
348 :
349 : /// \brief Generate identifier Nat2Pos.
350 : /// \return Identifier Nat2Pos.
351 : inline
352 112 : const core::identifier_string& nat2pos_name()
353 : {
354 112 : static core::identifier_string nat2pos_name = core::identifier_string("Nat2Pos");
355 112 : return nat2pos_name;
356 : }
357 :
358 : /// \brief Constructor for function symbol Nat2Pos.
359 :
360 : /// \return Function symbol nat2pos.
361 : inline
362 29176 : const function_symbol& nat2pos()
363 : {
364 29176 : static function_symbol nat2pos(nat2pos_name(), make_function_sort_(nat(), sort_pos::pos()));
365 29176 : return nat2pos;
366 : }
367 :
368 : /// \brief Recogniser for function Nat2Pos.
369 : /// \param e A data expression.
370 : /// \return true iff e is the function symbol matching Nat2Pos.
371 : inline
372 4 : bool is_nat2pos_function_symbol(const atermpp::aterm_appl& e)
373 : {
374 4 : if (is_function_symbol(e))
375 : {
376 4 : return atermpp::down_cast<function_symbol>(e) == nat2pos();
377 : }
378 0 : return false;
379 : }
380 :
381 : /// \brief Application of function symbol Nat2Pos.
382 :
383 : /// \param arg0 A data expression.
384 : /// \return Application of Nat2Pos to a number of arguments.
385 : inline
386 18227 : application nat2pos(const data_expression& arg0)
387 : {
388 18227 : return sort_nat::nat2pos()(arg0);
389 : }
390 :
391 : /// \brief Make an application of function symbol Nat2Pos.
392 : /// \param result The data expression where the Nat2Pos expression is put.
393 :
394 : /// \param arg0 A data expression.
395 : inline
396 : void make_nat2pos(data_expression& result, const data_expression& arg0)
397 : {
398 : make_application(result, sort_nat::nat2pos(),arg0);
399 : }
400 :
401 : /// \brief Recogniser for application of Nat2Pos.
402 : /// \param e A data expression.
403 : /// \return true iff e is an application of function symbol nat2pos to a
404 : /// number of arguments.
405 : inline
406 4 : bool is_nat2pos_application(const atermpp::aterm_appl& e)
407 : {
408 4 : return is_application(e) && is_nat2pos_function_symbol(atermpp::down_cast<application>(e).head());
409 : }
410 :
411 : /// \brief Generate identifier max.
412 : /// \return Identifier max.
413 : inline
414 64149 : const core::identifier_string& maximum_name()
415 : {
416 64149 : static core::identifier_string maximum_name = core::identifier_string("max");
417 64149 : return maximum_name;
418 : }
419 :
420 : // This function is not intended for public use and therefore not documented in Doxygen.
421 : inline
422 64106 : function_symbol maximum(const sort_expression& s0, const sort_expression& s1)
423 : {
424 64106 : sort_expression target_sort;
425 64106 : if (s0 == sort_pos::pos() && s1 == nat())
426 : {
427 23466 : target_sort = sort_pos::pos();
428 : }
429 40640 : else if (s0 == nat() && s1 == sort_pos::pos())
430 : {
431 23466 : target_sort = sort_pos::pos();
432 : }
433 17174 : else if (s0 == nat() && s1 == nat())
434 : {
435 17174 : target_sort = nat();
436 : }
437 0 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
438 : {
439 0 : target_sort = sort_pos::pos();
440 : }
441 : else
442 : {
443 0 : throw mcrl2::runtime_error("Cannot compute target sort for maximum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
444 : }
445 :
446 64106 : function_symbol maximum(maximum_name(), make_function_sort_(s0, s1, target_sort));
447 128212 : return maximum;
448 64106 : }
449 :
450 : /// \brief Recogniser for function max.
451 : /// \param e A data expression.
452 : /// \return true iff e is the function symbol matching max.
453 : inline
454 43 : bool is_maximum_function_symbol(const atermpp::aterm_appl& e)
455 : {
456 43 : if (is_function_symbol(e))
457 : {
458 43 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
459 43 : return f.name() == maximum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == maximum(sort_pos::pos(), nat()) || f == maximum(nat(), sort_pos::pos()) || f == maximum(nat(), nat()) || f == maximum(sort_pos::pos(), sort_pos::pos()));
460 : }
461 0 : return false;
462 : }
463 :
464 : /// \brief Application of function symbol max.
465 :
466 : /// \param arg0 A data expression.
467 : /// \param arg1 A data expression.
468 : /// \return Application of max to a number of arguments.
469 : inline
470 31484 : application maximum(const data_expression& arg0, const data_expression& arg1)
471 : {
472 62968 : return sort_nat::maximum(arg0.sort(), arg1.sort())(arg0, arg1);
473 : }
474 :
475 : /// \brief Make an application of function symbol max.
476 : /// \param result The data expression where the max expression is put.
477 :
478 : /// \param arg0 A data expression.
479 : /// \param arg1 A data expression.
480 : inline
481 : void make_maximum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
482 : {
483 : make_application(result, sort_nat::maximum(arg0.sort(), arg1.sort()),arg0, arg1);
484 : }
485 :
486 : /// \brief Recogniser for application of max.
487 : /// \param e A data expression.
488 : /// \return true iff e is an application of function symbol maximum to a
489 : /// number of arguments.
490 : inline
491 43 : bool is_maximum_application(const atermpp::aterm_appl& e)
492 : {
493 43 : return is_application(e) && is_maximum_function_symbol(atermpp::down_cast<application>(e).head());
494 : }
495 :
496 : /// \brief Generate identifier min.
497 : /// \return Identifier min.
498 : inline
499 48840 : const core::identifier_string& minimum_name()
500 : {
501 48840 : static core::identifier_string minimum_name = core::identifier_string("min");
502 48840 : return minimum_name;
503 : }
504 :
505 : // This function is not intended for public use and therefore not documented in Doxygen.
506 : inline
507 48797 : function_symbol minimum(const sort_expression& s0, const sort_expression& s1)
508 : {
509 48797 : sort_expression target_sort;
510 48797 : if (s0 == nat() && s1 == nat())
511 : {
512 48725 : target_sort = nat();
513 : }
514 72 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
515 : {
516 72 : target_sort = sort_pos::pos();
517 : }
518 : else
519 : {
520 0 : throw mcrl2::runtime_error("Cannot compute target sort for minimum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
521 : }
522 :
523 48797 : function_symbol minimum(minimum_name(), make_function_sort_(s0, s1, target_sort));
524 97594 : return minimum;
525 48797 : }
526 :
527 : /// \brief Recogniser for function min.
528 : /// \param e A data expression.
529 : /// \return true iff e is the function symbol matching min.
530 : inline
531 43 : bool is_minimum_function_symbol(const atermpp::aterm_appl& e)
532 : {
533 43 : if (is_function_symbol(e))
534 : {
535 43 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
536 43 : return f.name() == minimum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minimum(nat(), nat()) || f == minimum(sort_pos::pos(), sort_pos::pos()));
537 : }
538 0 : return false;
539 : }
540 :
541 : /// \brief Application of function symbol min.
542 :
543 : /// \param arg0 A data expression.
544 : /// \param arg1 A data expression.
545 : /// \return Application of min to a number of arguments.
546 : inline
547 37923 : application minimum(const data_expression& arg0, const data_expression& arg1)
548 : {
549 75846 : return sort_nat::minimum(arg0.sort(), arg1.sort())(arg0, arg1);
550 : }
551 :
552 : /// \brief Make an application of function symbol min.
553 : /// \param result The data expression where the min expression is put.
554 :
555 : /// \param arg0 A data expression.
556 : /// \param arg1 A data expression.
557 : inline
558 : void make_minimum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
559 : {
560 : make_application(result, sort_nat::minimum(arg0.sort(), arg1.sort()),arg0, arg1);
561 : }
562 :
563 : /// \brief Recogniser for application of min.
564 : /// \param e A data expression.
565 : /// \return true iff e is an application of function symbol minimum to a
566 : /// number of arguments.
567 : inline
568 43 : bool is_minimum_application(const atermpp::aterm_appl& e)
569 : {
570 43 : return is_application(e) && is_minimum_function_symbol(atermpp::down_cast<application>(e).head());
571 : }
572 :
573 : /// \brief Generate identifier succ.
574 : /// \return Identifier succ.
575 : inline
576 31177 : const core::identifier_string& succ_name()
577 : {
578 31177 : static core::identifier_string succ_name = core::identifier_string("succ");
579 31177 : return succ_name;
580 : }
581 :
582 : // This function is not intended for public use and therefore not documented in Doxygen.
583 : inline
584 31173 : function_symbol succ(const sort_expression& s0)
585 : {
586 31173 : sort_expression target_sort(sort_pos::pos());
587 31173 : function_symbol succ(succ_name(), make_function_sort_(s0, target_sort));
588 62346 : return succ;
589 31173 : }
590 :
591 : /// \brief Recogniser for function succ.
592 : /// \param e A data expression.
593 : /// \return true iff e is the function symbol matching succ.
594 : inline
595 4 : bool is_succ_function_symbol(const atermpp::aterm_appl& e)
596 : {
597 4 : if (is_function_symbol(e))
598 : {
599 4 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
600 4 : return f.name() == succ_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == succ(nat()) || f == succ(sort_pos::pos()));
601 : }
602 0 : return false;
603 : }
604 :
605 : /// \brief Application of function symbol succ.
606 :
607 : /// \param arg0 A data expression.
608 : /// \return Application of succ to a number of arguments.
609 : inline
610 20299 : application succ(const data_expression& arg0)
611 : {
612 40598 : return sort_nat::succ(arg0.sort())(arg0);
613 : }
614 :
615 : /// \brief Make an application of function symbol succ.
616 : /// \param result The data expression where the succ expression is put.
617 :
618 : /// \param arg0 A data expression.
619 : inline
620 : void make_succ(data_expression& result, const data_expression& arg0)
621 : {
622 : make_application(result, sort_nat::succ(arg0.sort()),arg0);
623 : }
624 :
625 : /// \brief Recogniser for application of succ.
626 : /// \param e A data expression.
627 : /// \return true iff e is an application of function symbol succ to a
628 : /// number of arguments.
629 : inline
630 4 : bool is_succ_application(const atermpp::aterm_appl& e)
631 : {
632 4 : return is_application(e) && is_succ_function_symbol(atermpp::down_cast<application>(e).head());
633 : }
634 :
635 : /// \brief Generate identifier pred.
636 : /// \return Identifier pred.
637 : inline
638 112 : const core::identifier_string& pred_name()
639 : {
640 112 : static core::identifier_string pred_name = core::identifier_string("pred");
641 112 : return pred_name;
642 : }
643 :
644 : /// \brief Constructor for function symbol pred.
645 :
646 : /// \return Function symbol pred.
647 : inline
648 49733 : const function_symbol& pred()
649 : {
650 49733 : static function_symbol pred(pred_name(), make_function_sort_(sort_pos::pos(), nat()));
651 49733 : return pred;
652 : }
653 :
654 : /// \brief Recogniser for function pred.
655 : /// \param e A data expression.
656 : /// \return true iff e is the function symbol matching pred.
657 : inline
658 4 : bool is_pred_function_symbol(const atermpp::aterm_appl& e)
659 : {
660 4 : if (is_function_symbol(e))
661 : {
662 4 : return atermpp::down_cast<function_symbol>(e) == pred();
663 : }
664 0 : return false;
665 : }
666 :
667 : /// \brief Application of function symbol pred.
668 :
669 : /// \param arg0 A data expression.
670 : /// \return Application of pred to a number of arguments.
671 : inline
672 38855 : application pred(const data_expression& arg0)
673 : {
674 38855 : return sort_nat::pred()(arg0);
675 : }
676 :
677 : /// \brief Make an application of function symbol pred.
678 : /// \param result The data expression where the pred expression is put.
679 :
680 : /// \param arg0 A data expression.
681 : inline
682 : void make_pred(data_expression& result, const data_expression& arg0)
683 : {
684 : make_application(result, sort_nat::pred(),arg0);
685 : }
686 :
687 : /// \brief Recogniser for application of pred.
688 : /// \param e A data expression.
689 : /// \return true iff e is an application of function symbol pred to a
690 : /// number of arguments.
691 : inline
692 4 : bool is_pred_application(const atermpp::aterm_appl& e)
693 : {
694 4 : return is_application(e) && is_pred_function_symbol(atermpp::down_cast<application>(e).head());
695 : }
696 :
697 : /// \brief Generate identifier \@dub.
698 : /// \return Identifier \@dub.
699 : inline
700 112 : const core::identifier_string& dub_name()
701 : {
702 112 : static core::identifier_string dub_name = core::identifier_string("@dub");
703 112 : return dub_name;
704 : }
705 :
706 : /// \brief Constructor for function symbol \@dub.
707 :
708 : /// \return Function symbol dub.
709 : inline
710 73877 : const function_symbol& dub()
711 : {
712 73877 : static function_symbol dub(dub_name(), make_function_sort_(sort_bool::bool_(), nat(), nat()));
713 73877 : return dub;
714 : }
715 :
716 : /// \brief Recogniser for function \@dub.
717 : /// \param e A data expression.
718 : /// \return true iff e is the function symbol matching \@dub.
719 : inline
720 43 : bool is_dub_function_symbol(const atermpp::aterm_appl& e)
721 : {
722 43 : if (is_function_symbol(e))
723 : {
724 43 : return atermpp::down_cast<function_symbol>(e) == dub();
725 : }
726 0 : return false;
727 : }
728 :
729 : /// \brief Application of function symbol \@dub.
730 :
731 : /// \param arg0 A data expression.
732 : /// \param arg1 A data expression.
733 : /// \return Application of \@dub to a number of arguments.
734 : inline
735 62960 : application dub(const data_expression& arg0, const data_expression& arg1)
736 : {
737 62960 : return sort_nat::dub()(arg0, arg1);
738 : }
739 :
740 : /// \brief Make an application of function symbol \@dub.
741 : /// \param result The data expression where the \@dub expression is put.
742 :
743 : /// \param arg0 A data expression.
744 : /// \param arg1 A data expression.
745 : inline
746 : void make_dub(data_expression& result, const data_expression& arg0, const data_expression& arg1)
747 : {
748 : make_application(result, sort_nat::dub(),arg0, arg1);
749 : }
750 :
751 : /// \brief Recogniser for application of \@dub.
752 : /// \param e A data expression.
753 : /// \return true iff e is an application of function symbol dub to a
754 : /// number of arguments.
755 : inline
756 43 : bool is_dub_application(const atermpp::aterm_appl& e)
757 : {
758 43 : return is_application(e) && is_dub_function_symbol(atermpp::down_cast<application>(e).head());
759 : }
760 :
761 : /// \brief Generate identifier \@dubsucc.
762 : /// \return Identifier \@dubsucc.
763 : inline
764 112 : const core::identifier_string& dubsucc_name()
765 : {
766 112 : static core::identifier_string dubsucc_name = core::identifier_string("@dubsucc");
767 112 : return dubsucc_name;
768 : }
769 :
770 : /// \brief Constructor for function symbol \@dubsucc.
771 :
772 : /// \return Function symbol dubsucc.
773 : inline
774 29766 : const function_symbol& dubsucc()
775 : {
776 29766 : static function_symbol dubsucc(dubsucc_name(), make_function_sort_(nat(), sort_pos::pos()));
777 29766 : return dubsucc;
778 : }
779 :
780 : /// \brief Recogniser for function \@dubsucc.
781 : /// \param e A data expression.
782 : /// \return true iff e is the function symbol matching \@dubsucc.
783 : inline
784 4 : bool is_dubsucc_function_symbol(const atermpp::aterm_appl& e)
785 : {
786 4 : if (is_function_symbol(e))
787 : {
788 4 : return atermpp::down_cast<function_symbol>(e) == dubsucc();
789 : }
790 0 : return false;
791 : }
792 :
793 : /// \brief Application of function symbol \@dubsucc.
794 :
795 : /// \param arg0 A data expression.
796 : /// \return Application of \@dubsucc to a number of arguments.
797 : inline
798 18888 : application dubsucc(const data_expression& arg0)
799 : {
800 18888 : return sort_nat::dubsucc()(arg0);
801 : }
802 :
803 : /// \brief Make an application of function symbol \@dubsucc.
804 : /// \param result The data expression where the \@dubsucc expression is put.
805 :
806 : /// \param arg0 A data expression.
807 : inline
808 : void make_dubsucc(data_expression& result, const data_expression& arg0)
809 : {
810 : make_application(result, sort_nat::dubsucc(),arg0);
811 : }
812 :
813 : /// \brief Recogniser for application of \@dubsucc.
814 : /// \param e A data expression.
815 : /// \return true iff e is an application of function symbol dubsucc to a
816 : /// number of arguments.
817 : inline
818 4 : bool is_dubsucc_application(const atermpp::aterm_appl& e)
819 : {
820 4 : return is_application(e) && is_dubsucc_function_symbol(atermpp::down_cast<application>(e).head());
821 : }
822 :
823 : /// \brief Generate identifier +.
824 : /// \return Identifier +.
825 : inline
826 174180 : const core::identifier_string& plus_name()
827 : {
828 174180 : static core::identifier_string plus_name = core::identifier_string("+");
829 174180 : return plus_name;
830 : }
831 :
832 : // This function is not intended for public use and therefore not documented in Doxygen.
833 : inline
834 134610 : function_symbol plus(const sort_expression& s0, const sort_expression& s1)
835 : {
836 134610 : sort_expression target_sort;
837 134610 : if (s0 == sort_pos::pos() && s1 == nat())
838 : {
839 23961 : target_sort = sort_pos::pos();
840 : }
841 110649 : else if (s0 == nat() && s1 == sort_pos::pos())
842 : {
843 23731 : target_sort = sort_pos::pos();
844 : }
845 86918 : else if (s0 == nat() && s1 == nat())
846 : {
847 86777 : target_sort = nat();
848 : }
849 141 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
850 : {
851 141 : target_sort = sort_pos::pos();
852 : }
853 : else
854 : {
855 0 : throw mcrl2::runtime_error("Cannot compute target sort for plus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
856 : }
857 :
858 134610 : function_symbol plus(plus_name(), make_function_sort_(s0, s1, target_sort));
859 269220 : return plus;
860 134610 : }
861 :
862 : /// \brief Recogniser for function +.
863 : /// \param e A data expression.
864 : /// \return true iff e is the function symbol matching +.
865 : inline
866 40804 : bool is_plus_function_symbol(const atermpp::aterm_appl& e)
867 : {
868 40804 : if (is_function_symbol(e))
869 : {
870 39570 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
871 39570 : return f.name() == plus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == plus(sort_pos::pos(), nat()) || f == plus(nat(), sort_pos::pos()) || f == plus(nat(), nat()) || f == plus(sort_pos::pos(), sort_pos::pos()));
872 : }
873 1234 : return false;
874 : }
875 :
876 : /// \brief Application of function symbol +.
877 :
878 : /// \param arg0 A data expression.
879 : /// \param arg1 A data expression.
880 : /// \return Application of + to a number of arguments.
881 : inline
882 100837 : application plus(const data_expression& arg0, const data_expression& arg1)
883 : {
884 201674 : return sort_nat::plus(arg0.sort(), arg1.sort())(arg0, arg1);
885 : }
886 :
887 : /// \brief Make an application of function symbol +.
888 : /// \param result The data expression where the + expression is put.
889 :
890 : /// \param arg0 A data expression.
891 : /// \param arg1 A data expression.
892 : inline
893 : void make_plus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
894 : {
895 : make_application(result, sort_nat::plus(arg0.sort(), arg1.sort()),arg0, arg1);
896 : }
897 :
898 : /// \brief Recogniser for application of +.
899 : /// \param e A data expression.
900 : /// \return true iff e is an application of function symbol plus to a
901 : /// number of arguments.
902 : inline
903 41208 : bool is_plus_application(const atermpp::aterm_appl& e)
904 : {
905 41208 : return is_application(e) && is_plus_function_symbol(atermpp::down_cast<application>(e).head());
906 : }
907 :
908 : /// \brief Generate identifier \@gtesubtb.
909 : /// \return Identifier \@gtesubtb.
910 : inline
911 112 : const core::identifier_string& gte_subtract_with_borrow_name()
912 : {
913 112 : static core::identifier_string gte_subtract_with_borrow_name = core::identifier_string("@gtesubtb");
914 112 : return gte_subtract_with_borrow_name;
915 : }
916 :
917 : /// \brief Constructor for function symbol \@gtesubtb.
918 :
919 : /// \return Function symbol gte_subtract_with_borrow.
920 : inline
921 84872 : const function_symbol& gte_subtract_with_borrow()
922 : {
923 84872 : static function_symbol gte_subtract_with_borrow(gte_subtract_with_borrow_name(), make_function_sort_(sort_bool::bool_(), sort_pos::pos(), sort_pos::pos(), nat()));
924 84872 : return gte_subtract_with_borrow;
925 : }
926 :
927 : /// \brief Recogniser for function \@gtesubtb.
928 : /// \param e A data expression.
929 : /// \return true iff e is the function symbol matching \@gtesubtb.
930 : inline
931 : bool is_gte_subtract_with_borrow_function_symbol(const atermpp::aterm_appl& e)
932 : {
933 : if (is_function_symbol(e))
934 : {
935 : return atermpp::down_cast<function_symbol>(e) == gte_subtract_with_borrow();
936 : }
937 : return false;
938 : }
939 :
940 : /// \brief Application of function symbol \@gtesubtb.
941 :
942 : /// \param arg0 A data expression.
943 : /// \param arg1 A data expression.
944 : /// \param arg2 A data expression.
945 : /// \return Application of \@gtesubtb to a number of arguments.
946 : inline
947 73998 : application gte_subtract_with_borrow(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
948 : {
949 73998 : return sort_nat::gte_subtract_with_borrow()(arg0, arg1, arg2);
950 : }
951 :
952 : /// \brief Make an application of function symbol \@gtesubtb.
953 : /// \param result The data expression where the \@gtesubtb expression is put.
954 :
955 : /// \param arg0 A data expression.
956 : /// \param arg1 A data expression.
957 : /// \param arg2 A data expression.
958 : inline
959 : void make_gte_subtract_with_borrow(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
960 : {
961 : make_application(result, sort_nat::gte_subtract_with_borrow(),arg0, arg1, arg2);
962 : }
963 :
964 : /// \brief Recogniser for application of \@gtesubtb.
965 : /// \param e A data expression.
966 : /// \return true iff e is an application of function symbol gte_subtract_with_borrow to a
967 : /// number of arguments.
968 : inline
969 : bool is_gte_subtract_with_borrow_application(const atermpp::aterm_appl& e)
970 : {
971 : return is_application(e) && is_gte_subtract_with_borrow_function_symbol(atermpp::down_cast<application>(e).head());
972 : }
973 :
974 : /// \brief Generate identifier *.
975 : /// \return Identifier *.
976 : inline
977 89068 : const core::identifier_string& times_name()
978 : {
979 89068 : static core::identifier_string times_name = core::identifier_string("*");
980 89068 : return times_name;
981 : }
982 :
983 : // This function is not intended for public use and therefore not documented in Doxygen.
984 : inline
985 67738 : function_symbol times(const sort_expression& s0, const sort_expression& s1)
986 : {
987 67738 : sort_expression target_sort;
988 67738 : if (s0 == nat() && s1 == nat())
989 : {
990 42472 : target_sort = nat();
991 : }
992 25266 : else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
993 : {
994 25266 : target_sort = sort_pos::pos();
995 : }
996 : else
997 : {
998 0 : throw mcrl2::runtime_error("Cannot compute target sort for times with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
999 : }
1000 :
1001 67738 : function_symbol times(times_name(), make_function_sort_(s0, s1, target_sort));
1002 135476 : return times;
1003 67738 : }
1004 :
1005 : /// \brief Recogniser for function *.
1006 : /// \param e A data expression.
1007 : /// \return true iff e is the function symbol matching *.
1008 : inline
1009 22172 : bool is_times_function_symbol(const atermpp::aterm_appl& e)
1010 : {
1011 22172 : if (is_function_symbol(e))
1012 : {
1013 21330 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1014 21330 : return f.name() == times_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == times(nat(), nat()) || f == times(sort_pos::pos(), sort_pos::pos()));
1015 : }
1016 842 : return false;
1017 : }
1018 :
1019 : /// \brief Application of function symbol *.
1020 :
1021 : /// \param arg0 A data expression.
1022 : /// \param arg1 A data expression.
1023 : /// \return Application of * to a number of arguments.
1024 : inline
1025 56679 : application times(const data_expression& arg0, const data_expression& arg1)
1026 : {
1027 113358 : return sort_nat::times(arg0.sort(), arg1.sort())(arg0, arg1);
1028 : }
1029 :
1030 : /// \brief Make an application of function symbol *.
1031 : /// \param result The data expression where the * expression is put.
1032 :
1033 : /// \param arg0 A data expression.
1034 : /// \param arg1 A data expression.
1035 : inline
1036 : void make_times(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1037 : {
1038 : make_application(result, sort_nat::times(arg0.sort(), arg1.sort()),arg0, arg1);
1039 : }
1040 :
1041 : /// \brief Recogniser for application of *.
1042 : /// \param e A data expression.
1043 : /// \return true iff e is an application of function symbol times to a
1044 : /// number of arguments.
1045 : inline
1046 22172 : bool is_times_application(const atermpp::aterm_appl& e)
1047 : {
1048 22172 : return is_application(e) && is_times_function_symbol(atermpp::down_cast<application>(e).head());
1049 : }
1050 :
1051 : /// \brief Generate identifier div.
1052 : /// \return Identifier div.
1053 : inline
1054 112 : const core::identifier_string& div_name()
1055 : {
1056 112 : static core::identifier_string div_name = core::identifier_string("div");
1057 112 : return div_name;
1058 : }
1059 :
1060 : /// \brief Constructor for function symbol div.
1061 :
1062 : /// \return Function symbol div.
1063 : inline
1064 62506 : const function_symbol& div()
1065 : {
1066 62506 : static function_symbol div(div_name(), make_function_sort_(nat(), sort_pos::pos(), nat()));
1067 62506 : return div;
1068 : }
1069 :
1070 : /// \brief Recogniser for function div.
1071 : /// \param e A data expression.
1072 : /// \return true iff e is the function symbol matching div.
1073 : inline
1074 40271 : bool is_div_function_symbol(const atermpp::aterm_appl& e)
1075 : {
1076 40271 : if (is_function_symbol(e))
1077 : {
1078 39037 : return atermpp::down_cast<function_symbol>(e) == div();
1079 : }
1080 1234 : return false;
1081 : }
1082 :
1083 : /// \brief Application of function symbol div.
1084 :
1085 : /// \param arg0 A data expression.
1086 : /// \param arg1 A data expression.
1087 : /// \return Application of div to a number of arguments.
1088 : inline
1089 12595 : application div(const data_expression& arg0, const data_expression& arg1)
1090 : {
1091 12595 : return sort_nat::div()(arg0, arg1);
1092 : }
1093 :
1094 : /// \brief Make an application of function symbol div.
1095 : /// \param result The data expression where the div expression is put.
1096 :
1097 : /// \param arg0 A data expression.
1098 : /// \param arg1 A data expression.
1099 : inline
1100 : void make_div(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1101 : {
1102 : make_application(result, sort_nat::div(),arg0, arg1);
1103 : }
1104 :
1105 : /// \brief Recogniser for application of div.
1106 : /// \param e A data expression.
1107 : /// \return true iff e is an application of function symbol div to a
1108 : /// number of arguments.
1109 : inline
1110 40675 : bool is_div_application(const atermpp::aterm_appl& e)
1111 : {
1112 40675 : return is_application(e) && is_div_function_symbol(atermpp::down_cast<application>(e).head());
1113 : }
1114 :
1115 : /// \brief Generate identifier mod.
1116 : /// \return Identifier mod.
1117 : inline
1118 112 : const core::identifier_string& mod_name()
1119 : {
1120 112 : static core::identifier_string mod_name = core::identifier_string("mod");
1121 112 : return mod_name;
1122 : }
1123 :
1124 : /// \brief Constructor for function symbol mod.
1125 :
1126 : /// \return Function symbol mod.
1127 : inline
1128 62450 : const function_symbol& mod()
1129 : {
1130 62450 : static function_symbol mod(mod_name(), make_function_sort_(nat(), sort_pos::pos(), nat()));
1131 62450 : return mod;
1132 : }
1133 :
1134 : /// \brief Recogniser for function mod.
1135 : /// \param e A data expression.
1136 : /// \return true iff e is the function symbol matching mod.
1137 : inline
1138 40214 : bool is_mod_function_symbol(const atermpp::aterm_appl& e)
1139 : {
1140 40214 : if (is_function_symbol(e))
1141 : {
1142 38980 : return atermpp::down_cast<function_symbol>(e) == mod();
1143 : }
1144 1234 : return false;
1145 : }
1146 :
1147 : /// \brief Application of function symbol mod.
1148 :
1149 : /// \param arg0 A data expression.
1150 : /// \param arg1 A data expression.
1151 : /// \return Application of mod to a number of arguments.
1152 : inline
1153 12596 : application mod(const data_expression& arg0, const data_expression& arg1)
1154 : {
1155 12596 : return sort_nat::mod()(arg0, arg1);
1156 : }
1157 :
1158 : /// \brief Make an application of function symbol mod.
1159 : /// \param result The data expression where the mod expression is put.
1160 :
1161 : /// \param arg0 A data expression.
1162 : /// \param arg1 A data expression.
1163 : inline
1164 : void make_mod(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1165 : {
1166 : make_application(result, sort_nat::mod(),arg0, arg1);
1167 : }
1168 :
1169 : /// \brief Recogniser for application of mod.
1170 : /// \param e A data expression.
1171 : /// \return true iff e is an application of function symbol mod to a
1172 : /// number of arguments.
1173 : inline
1174 40618 : bool is_mod_application(const atermpp::aterm_appl& e)
1175 : {
1176 40618 : return is_application(e) && is_mod_function_symbol(atermpp::down_cast<application>(e).head());
1177 : }
1178 :
1179 : /// \brief Generate identifier exp.
1180 : /// \return Identifier exp.
1181 : inline
1182 84709 : const core::identifier_string& exp_name()
1183 : {
1184 84709 : static core::identifier_string exp_name = core::identifier_string("exp");
1185 84709 : return exp_name;
1186 : }
1187 :
1188 : // This function is not intended for public use and therefore not documented in Doxygen.
1189 : inline
1190 84709 : function_symbol exp(const sort_expression& s0, const sort_expression& s1)
1191 : {
1192 84709 : sort_expression target_sort;
1193 84709 : if (s0 == sort_pos::pos() && s1 == nat())
1194 : {
1195 54946 : target_sort = sort_pos::pos();
1196 : }
1197 29763 : else if (s0 == nat() && s1 == nat())
1198 : {
1199 29763 : target_sort = nat();
1200 : }
1201 : else
1202 : {
1203 0 : throw mcrl2::runtime_error("Cannot compute target sort for exp with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
1204 : }
1205 :
1206 84709 : function_symbol exp(exp_name(), make_function_sort_(s0, s1, target_sort));
1207 169418 : return exp;
1208 84709 : }
1209 :
1210 : /// \brief Recogniser for function exp.
1211 : /// \param e A data expression.
1212 : /// \return true iff e is the function symbol matching exp.
1213 : inline
1214 0 : bool is_exp_function_symbol(const atermpp::aterm_appl& e)
1215 : {
1216 0 : if (is_function_symbol(e))
1217 : {
1218 0 : const function_symbol& f = atermpp::down_cast<function_symbol>(e);
1219 0 : return f.name() == exp_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == exp(sort_pos::pos(), nat()) || f == exp(nat(), nat()));
1220 : }
1221 0 : return false;
1222 : }
1223 :
1224 : /// \brief Application of function symbol exp.
1225 :
1226 : /// \param arg0 A data expression.
1227 : /// \param arg1 A data expression.
1228 : /// \return Application of exp to a number of arguments.
1229 : inline
1230 62961 : application exp(const data_expression& arg0, const data_expression& arg1)
1231 : {
1232 125922 : return sort_nat::exp(arg0.sort(), arg1.sort())(arg0, arg1);
1233 : }
1234 :
1235 : /// \brief Make an application of function symbol exp.
1236 : /// \param result The data expression where the exp expression is put.
1237 :
1238 : /// \param arg0 A data expression.
1239 : /// \param arg1 A data expression.
1240 : inline
1241 : void make_exp(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1242 : {
1243 : make_application(result, sort_nat::exp(arg0.sort(), arg1.sort()),arg0, arg1);
1244 : }
1245 :
1246 : /// \brief Recogniser for application of exp.
1247 : /// \param e A data expression.
1248 : /// \return true iff e is an application of function symbol exp to a
1249 : /// number of arguments.
1250 : inline
1251 0 : bool is_exp_application(const atermpp::aterm_appl& e)
1252 : {
1253 0 : return is_application(e) && is_exp_function_symbol(atermpp::down_cast<application>(e).head());
1254 : }
1255 :
1256 : /// \brief Generate identifier \@even.
1257 : /// \return Identifier \@even.
1258 : inline
1259 112 : const core::identifier_string& even_name()
1260 : {
1261 112 : static core::identifier_string even_name = core::identifier_string("@even");
1262 112 : return even_name;
1263 : }
1264 :
1265 : /// \brief Constructor for function symbol \@even.
1266 :
1267 : /// \return Function symbol even.
1268 : inline
1269 40732 : const function_symbol& even()
1270 : {
1271 40732 : static function_symbol even(even_name(), make_function_sort_(nat(), sort_bool::bool_()));
1272 40732 : return even;
1273 : }
1274 :
1275 : /// \brief Recogniser for function \@even.
1276 : /// \param e A data expression.
1277 : /// \return true iff e is the function symbol matching \@even.
1278 : inline
1279 4 : bool is_even_function_symbol(const atermpp::aterm_appl& e)
1280 : {
1281 4 : if (is_function_symbol(e))
1282 : {
1283 4 : return atermpp::down_cast<function_symbol>(e) == even();
1284 : }
1285 0 : return false;
1286 : }
1287 :
1288 : /// \brief Application of function symbol \@even.
1289 :
1290 : /// \param arg0 A data expression.
1291 : /// \return Application of \@even to a number of arguments.
1292 : inline
1293 29854 : application even(const data_expression& arg0)
1294 : {
1295 29854 : return sort_nat::even()(arg0);
1296 : }
1297 :
1298 : /// \brief Make an application of function symbol \@even.
1299 : /// \param result The data expression where the \@even expression is put.
1300 :
1301 : /// \param arg0 A data expression.
1302 : inline
1303 : void make_even(data_expression& result, const data_expression& arg0)
1304 : {
1305 : make_application(result, sort_nat::even(),arg0);
1306 : }
1307 :
1308 : /// \brief Recogniser for application of \@even.
1309 : /// \param e A data expression.
1310 : /// \return true iff e is an application of function symbol even to a
1311 : /// number of arguments.
1312 : inline
1313 4 : bool is_even_application(const atermpp::aterm_appl& e)
1314 : {
1315 4 : return is_application(e) && is_even_function_symbol(atermpp::down_cast<application>(e).head());
1316 : }
1317 :
1318 : /// \brief Generate identifier \@monus.
1319 : /// \return Identifier \@monus.
1320 : inline
1321 112 : const core::identifier_string& monus_name()
1322 : {
1323 112 : static core::identifier_string monus_name = core::identifier_string("@monus");
1324 112 : return monus_name;
1325 : }
1326 :
1327 : /// \brief Constructor for function symbol \@monus.
1328 :
1329 : /// \return Function symbol monus.
1330 : inline
1331 78572 : const function_symbol& monus()
1332 : {
1333 78572 : static function_symbol monus(monus_name(), make_function_sort_(nat(), nat(), nat()));
1334 78572 : return monus;
1335 : }
1336 :
1337 : /// \brief Recogniser for function \@monus.
1338 : /// \param e A data expression.
1339 : /// \return true iff e is the function symbol matching \@monus.
1340 : inline
1341 0 : bool is_monus_function_symbol(const atermpp::aterm_appl& e)
1342 : {
1343 0 : if (is_function_symbol(e))
1344 : {
1345 0 : return atermpp::down_cast<function_symbol>(e) == monus();
1346 : }
1347 0 : return false;
1348 : }
1349 :
1350 : /// \brief Application of function symbol \@monus.
1351 :
1352 : /// \param arg0 A data expression.
1353 : /// \param arg1 A data expression.
1354 : /// \return Application of \@monus to a number of arguments.
1355 : inline
1356 67698 : application monus(const data_expression& arg0, const data_expression& arg1)
1357 : {
1358 67698 : return sort_nat::monus()(arg0, arg1);
1359 : }
1360 :
1361 : /// \brief Make an application of function symbol \@monus.
1362 : /// \param result The data expression where the \@monus expression is put.
1363 :
1364 : /// \param arg0 A data expression.
1365 : /// \param arg1 A data expression.
1366 : inline
1367 : void make_monus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1368 : {
1369 : make_application(result, sort_nat::monus(),arg0, arg1);
1370 : }
1371 :
1372 : /// \brief Recogniser for application of \@monus.
1373 : /// \param e A data expression.
1374 : /// \return true iff e is an application of function symbol monus to a
1375 : /// number of arguments.
1376 : inline
1377 0 : bool is_monus_application(const atermpp::aterm_appl& e)
1378 : {
1379 0 : return is_application(e) && is_monus_function_symbol(atermpp::down_cast<application>(e).head());
1380 : }
1381 :
1382 : /// \brief Generate identifier \@swap_zero.
1383 : /// \return Identifier \@swap_zero.
1384 : inline
1385 112 : const core::identifier_string& swap_zero_name()
1386 : {
1387 112 : static core::identifier_string swap_zero_name = core::identifier_string("@swap_zero");
1388 112 : return swap_zero_name;
1389 : }
1390 :
1391 : /// \brief Constructor for function symbol \@swap_zero.
1392 :
1393 : /// \return Function symbol swap_zero.
1394 : inline
1395 149470 : const function_symbol& swap_zero()
1396 : {
1397 149470 : static function_symbol swap_zero(swap_zero_name(), make_function_sort_(nat(), nat(), nat()));
1398 149470 : return swap_zero;
1399 : }
1400 :
1401 : /// \brief Recogniser for function \@swap_zero.
1402 : /// \param e A data expression.
1403 : /// \return true iff e is the function symbol matching \@swap_zero.
1404 : inline
1405 0 : bool is_swap_zero_function_symbol(const atermpp::aterm_appl& e)
1406 : {
1407 0 : if (is_function_symbol(e))
1408 : {
1409 0 : return atermpp::down_cast<function_symbol>(e) == swap_zero();
1410 : }
1411 0 : return false;
1412 : }
1413 :
1414 : /// \brief Application of function symbol \@swap_zero.
1415 :
1416 : /// \param arg0 A data expression.
1417 : /// \param arg1 A data expression.
1418 : /// \return Application of \@swap_zero to a number of arguments.
1419 : inline
1420 138596 : application swap_zero(const data_expression& arg0, const data_expression& arg1)
1421 : {
1422 138596 : return sort_nat::swap_zero()(arg0, arg1);
1423 : }
1424 :
1425 : /// \brief Make an application of function symbol \@swap_zero.
1426 : /// \param result The data expression where the \@swap_zero expression is put.
1427 :
1428 : /// \param arg0 A data expression.
1429 : /// \param arg1 A data expression.
1430 : inline
1431 : void make_swap_zero(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1432 : {
1433 : make_application(result, sort_nat::swap_zero(),arg0, arg1);
1434 : }
1435 :
1436 : /// \brief Recogniser for application of \@swap_zero.
1437 : /// \param e A data expression.
1438 : /// \return true iff e is an application of function symbol swap_zero to a
1439 : /// number of arguments.
1440 : inline
1441 0 : bool is_swap_zero_application(const atermpp::aterm_appl& e)
1442 : {
1443 0 : return is_application(e) && is_swap_zero_function_symbol(atermpp::down_cast<application>(e).head());
1444 : }
1445 :
1446 : /// \brief Generate identifier \@swap_zero_add.
1447 : /// \return Identifier \@swap_zero_add.
1448 : inline
1449 112 : const core::identifier_string& swap_zero_add_name()
1450 : {
1451 112 : static core::identifier_string swap_zero_add_name = core::identifier_string("@swap_zero_add");
1452 112 : return swap_zero_add_name;
1453 : }
1454 :
1455 : /// \brief Constructor for function symbol \@swap_zero_add.
1456 :
1457 : /// \return Function symbol swap_zero_add.
1458 : inline
1459 48990 : const function_symbol& swap_zero_add()
1460 : {
1461 48990 : static function_symbol swap_zero_add(swap_zero_add_name(), make_function_sort_(nat(), nat(), nat(), nat(), nat()));
1462 48990 : return swap_zero_add;
1463 : }
1464 :
1465 : /// \brief Recogniser for function \@swap_zero_add.
1466 : /// \param e A data expression.
1467 : /// \return true iff e is the function symbol matching \@swap_zero_add.
1468 : inline
1469 : bool is_swap_zero_add_function_symbol(const atermpp::aterm_appl& e)
1470 : {
1471 : if (is_function_symbol(e))
1472 : {
1473 : return atermpp::down_cast<function_symbol>(e) == swap_zero_add();
1474 : }
1475 : return false;
1476 : }
1477 :
1478 : /// \brief Application of function symbol \@swap_zero_add.
1479 :
1480 : /// \param arg0 A data expression.
1481 : /// \param arg1 A data expression.
1482 : /// \param arg2 A data expression.
1483 : /// \param arg3 A data expression.
1484 : /// \return Application of \@swap_zero_add to a number of arguments.
1485 : inline
1486 38116 : application swap_zero_add(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
1487 : {
1488 38116 : return sort_nat::swap_zero_add()(arg0, arg1, arg2, arg3);
1489 : }
1490 :
1491 : /// \brief Make an application of function symbol \@swap_zero_add.
1492 : /// \param result The data expression where the \@swap_zero_add expression is put.
1493 :
1494 : /// \param arg0 A data expression.
1495 : /// \param arg1 A data expression.
1496 : /// \param arg2 A data expression.
1497 : /// \param arg3 A data expression.
1498 : inline
1499 : void make_swap_zero_add(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
1500 : {
1501 : make_application(result, sort_nat::swap_zero_add(),arg0, arg1, arg2, arg3);
1502 : }
1503 :
1504 : /// \brief Recogniser for application of \@swap_zero_add.
1505 : /// \param e A data expression.
1506 : /// \return true iff e is an application of function symbol swap_zero_add to a
1507 : /// number of arguments.
1508 : inline
1509 : bool is_swap_zero_add_application(const atermpp::aterm_appl& e)
1510 : {
1511 : return is_application(e) && is_swap_zero_add_function_symbol(atermpp::down_cast<application>(e).head());
1512 : }
1513 :
1514 : /// \brief Generate identifier \@swap_zero_min.
1515 : /// \return Identifier \@swap_zero_min.
1516 : inline
1517 112 : const core::identifier_string& swap_zero_min_name()
1518 : {
1519 112 : static core::identifier_string swap_zero_min_name = core::identifier_string("@swap_zero_min");
1520 112 : return swap_zero_min_name;
1521 : }
1522 :
1523 : /// \brief Constructor for function symbol \@swap_zero_min.
1524 :
1525 : /// \return Function symbol swap_zero_min.
1526 : inline
1527 48990 : const function_symbol& swap_zero_min()
1528 : {
1529 48990 : static function_symbol swap_zero_min(swap_zero_min_name(), make_function_sort_(nat(), nat(), nat(), nat(), nat()));
1530 48990 : return swap_zero_min;
1531 : }
1532 :
1533 : /// \brief Recogniser for function \@swap_zero_min.
1534 : /// \param e A data expression.
1535 : /// \return true iff e is the function symbol matching \@swap_zero_min.
1536 : inline
1537 : bool is_swap_zero_min_function_symbol(const atermpp::aterm_appl& e)
1538 : {
1539 : if (is_function_symbol(e))
1540 : {
1541 : return atermpp::down_cast<function_symbol>(e) == swap_zero_min();
1542 : }
1543 : return false;
1544 : }
1545 :
1546 : /// \brief Application of function symbol \@swap_zero_min.
1547 :
1548 : /// \param arg0 A data expression.
1549 : /// \param arg1 A data expression.
1550 : /// \param arg2 A data expression.
1551 : /// \param arg3 A data expression.
1552 : /// \return Application of \@swap_zero_min to a number of arguments.
1553 : inline
1554 38116 : application swap_zero_min(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
1555 : {
1556 38116 : return sort_nat::swap_zero_min()(arg0, arg1, arg2, arg3);
1557 : }
1558 :
1559 : /// \brief Make an application of function symbol \@swap_zero_min.
1560 : /// \param result The data expression where the \@swap_zero_min expression is put.
1561 :
1562 : /// \param arg0 A data expression.
1563 : /// \param arg1 A data expression.
1564 : /// \param arg2 A data expression.
1565 : /// \param arg3 A data expression.
1566 : inline
1567 : void make_swap_zero_min(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
1568 : {
1569 : make_application(result, sort_nat::swap_zero_min(),arg0, arg1, arg2, arg3);
1570 : }
1571 :
1572 : /// \brief Recogniser for application of \@swap_zero_min.
1573 : /// \param e A data expression.
1574 : /// \return true iff e is an application of function symbol swap_zero_min to a
1575 : /// number of arguments.
1576 : inline
1577 : bool is_swap_zero_min_application(const atermpp::aterm_appl& e)
1578 : {
1579 : return is_application(e) && is_swap_zero_min_function_symbol(atermpp::down_cast<application>(e).head());
1580 : }
1581 :
1582 : /// \brief Generate identifier \@swap_zero_monus.
1583 : /// \return Identifier \@swap_zero_monus.
1584 : inline
1585 112 : const core::identifier_string& swap_zero_monus_name()
1586 : {
1587 112 : static core::identifier_string swap_zero_monus_name = core::identifier_string("@swap_zero_monus");
1588 112 : return swap_zero_monus_name;
1589 : }
1590 :
1591 : /// \brief Constructor for function symbol \@swap_zero_monus.
1592 :
1593 : /// \return Function symbol swap_zero_monus.
1594 : inline
1595 48990 : const function_symbol& swap_zero_monus()
1596 : {
1597 48990 : static function_symbol swap_zero_monus(swap_zero_monus_name(), make_function_sort_(nat(), nat(), nat(), nat(), nat()));
1598 48990 : return swap_zero_monus;
1599 : }
1600 :
1601 : /// \brief Recogniser for function \@swap_zero_monus.
1602 : /// \param e A data expression.
1603 : /// \return true iff e is the function symbol matching \@swap_zero_monus.
1604 : inline
1605 : bool is_swap_zero_monus_function_symbol(const atermpp::aterm_appl& e)
1606 : {
1607 : if (is_function_symbol(e))
1608 : {
1609 : return atermpp::down_cast<function_symbol>(e) == swap_zero_monus();
1610 : }
1611 : return false;
1612 : }
1613 :
1614 : /// \brief Application of function symbol \@swap_zero_monus.
1615 :
1616 : /// \param arg0 A data expression.
1617 : /// \param arg1 A data expression.
1618 : /// \param arg2 A data expression.
1619 : /// \param arg3 A data expression.
1620 : /// \return Application of \@swap_zero_monus to a number of arguments.
1621 : inline
1622 38116 : application swap_zero_monus(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
1623 : {
1624 38116 : return sort_nat::swap_zero_monus()(arg0, arg1, arg2, arg3);
1625 : }
1626 :
1627 : /// \brief Make an application of function symbol \@swap_zero_monus.
1628 : /// \param result The data expression where the \@swap_zero_monus expression is put.
1629 :
1630 : /// \param arg0 A data expression.
1631 : /// \param arg1 A data expression.
1632 : /// \param arg2 A data expression.
1633 : /// \param arg3 A data expression.
1634 : inline
1635 : void make_swap_zero_monus(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
1636 : {
1637 : make_application(result, sort_nat::swap_zero_monus(),arg0, arg1, arg2, arg3);
1638 : }
1639 :
1640 : /// \brief Recogniser for application of \@swap_zero_monus.
1641 : /// \param e A data expression.
1642 : /// \return true iff e is an application of function symbol swap_zero_monus to a
1643 : /// number of arguments.
1644 : inline
1645 : bool is_swap_zero_monus_application(const atermpp::aterm_appl& e)
1646 : {
1647 : return is_application(e) && is_swap_zero_monus_function_symbol(atermpp::down_cast<application>(e).head());
1648 : }
1649 :
1650 : /// \brief Generate identifier sqrt.
1651 : /// \return Identifier sqrt.
1652 : inline
1653 59240 : const core::identifier_string& sqrt_name()
1654 : {
1655 59240 : static core::identifier_string sqrt_name = core::identifier_string("sqrt");
1656 59240 : return sqrt_name;
1657 : }
1658 :
1659 : /// \brief Constructor for function symbol sqrt.
1660 :
1661 : /// \return Function symbol sqrt.
1662 : inline
1663 23541 : const function_symbol& sqrt()
1664 : {
1665 23541 : static function_symbol sqrt(sqrt_name(), make_function_sort_(nat(), nat()));
1666 23541 : return sqrt;
1667 : }
1668 :
1669 : /// \brief Recogniser for function sqrt.
1670 : /// \param e A data expression.
1671 : /// \return true iff e is the function symbol matching sqrt.
1672 : inline
1673 4 : bool is_sqrt_function_symbol(const atermpp::aterm_appl& e)
1674 : {
1675 4 : if (is_function_symbol(e))
1676 : {
1677 4 : return atermpp::down_cast<function_symbol>(e) == sqrt();
1678 : }
1679 0 : return false;
1680 : }
1681 :
1682 : /// \brief Application of function symbol sqrt.
1683 :
1684 : /// \param arg0 A data expression.
1685 : /// \return Application of sqrt to a number of arguments.
1686 : inline
1687 12592 : application sqrt(const data_expression& arg0)
1688 : {
1689 12592 : return sort_nat::sqrt()(arg0);
1690 : }
1691 :
1692 : /// \brief Make an application of function symbol sqrt.
1693 : /// \param result The data expression where the sqrt expression is put.
1694 :
1695 : /// \param arg0 A data expression.
1696 : inline
1697 : void make_sqrt(data_expression& result, const data_expression& arg0)
1698 : {
1699 : make_application(result, sort_nat::sqrt(),arg0);
1700 : }
1701 :
1702 : /// \brief Recogniser for application of sqrt.
1703 : /// \param e A data expression.
1704 : /// \return true iff e is an application of function symbol sqrt to a
1705 : /// number of arguments.
1706 : inline
1707 4 : bool is_sqrt_application(const atermpp::aterm_appl& e)
1708 : {
1709 4 : return is_application(e) && is_sqrt_function_symbol(atermpp::down_cast<application>(e).head());
1710 : }
1711 :
1712 : /// \brief Generate identifier \@sqrt_nat.
1713 : /// \return Identifier \@sqrt_nat.
1714 : inline
1715 112 : const core::identifier_string& sqrt_nat_aux_func_name()
1716 : {
1717 112 : static core::identifier_string sqrt_nat_aux_func_name = core::identifier_string("@sqrt_nat");
1718 112 : return sqrt_nat_aux_func_name;
1719 : }
1720 :
1721 : /// \brief Constructor for function symbol \@sqrt_nat.
1722 :
1723 : /// \return Function symbol sqrt_nat_aux_func.
1724 : inline
1725 42354 : const function_symbol& sqrt_nat_aux_func()
1726 : {
1727 42354 : static function_symbol sqrt_nat_aux_func(sqrt_nat_aux_func_name(), make_function_sort_(nat(), nat(), sort_pos::pos(), nat()));
1728 42354 : return sqrt_nat_aux_func;
1729 : }
1730 :
1731 : /// \brief Recogniser for function \@sqrt_nat.
1732 : /// \param e A data expression.
1733 : /// \return true iff e is the function symbol matching \@sqrt_nat.
1734 : inline
1735 : bool is_sqrt_nat_aux_func_function_symbol(const atermpp::aterm_appl& e)
1736 : {
1737 : if (is_function_symbol(e))
1738 : {
1739 : return atermpp::down_cast<function_symbol>(e) == sqrt_nat_aux_func();
1740 : }
1741 : return false;
1742 : }
1743 :
1744 : /// \brief Application of function symbol \@sqrt_nat.
1745 :
1746 : /// \param arg0 A data expression.
1747 : /// \param arg1 A data expression.
1748 : /// \param arg2 A data expression.
1749 : /// \return Application of \@sqrt_nat to a number of arguments.
1750 : inline
1751 31480 : application sqrt_nat_aux_func(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
1752 : {
1753 31480 : return sort_nat::sqrt_nat_aux_func()(arg0, arg1, arg2);
1754 : }
1755 :
1756 : /// \brief Make an application of function symbol \@sqrt_nat.
1757 : /// \param result The data expression where the \@sqrt_nat expression is put.
1758 :
1759 : /// \param arg0 A data expression.
1760 : /// \param arg1 A data expression.
1761 : /// \param arg2 A data expression.
1762 : inline
1763 : void make_sqrt_nat_aux_func(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
1764 : {
1765 : make_application(result, sort_nat::sqrt_nat_aux_func(),arg0, arg1, arg2);
1766 : }
1767 :
1768 : /// \brief Recogniser for application of \@sqrt_nat.
1769 : /// \param e A data expression.
1770 : /// \return true iff e is an application of function symbol sqrt_nat_aux_func to a
1771 : /// number of arguments.
1772 : inline
1773 : bool is_sqrt_nat_aux_func_application(const atermpp::aterm_appl& e)
1774 : {
1775 : return is_application(e) && is_sqrt_nat_aux_func_function_symbol(atermpp::down_cast<application>(e).head());
1776 : }
1777 :
1778 : /// \brief Generate identifier \@first.
1779 : /// \return Identifier \@first.
1780 : inline
1781 112 : const core::identifier_string& first_name()
1782 : {
1783 112 : static core::identifier_string first_name = core::identifier_string("@first");
1784 112 : return first_name;
1785 : }
1786 :
1787 : /// \brief Constructor for function symbol \@first.
1788 :
1789 : /// \return Function symbol first.
1790 : inline
1791 48351 : const function_symbol& first()
1792 : {
1793 48351 : static function_symbol first(first_name(), make_function_sort_(natpair(), nat()));
1794 48351 : return first;
1795 : }
1796 :
1797 : /// \brief Recogniser for function \@first.
1798 : /// \param e A data expression.
1799 : /// \return true iff e is the function symbol matching \@first.
1800 : inline
1801 25727 : bool is_first_function_symbol(const atermpp::aterm_appl& e)
1802 : {
1803 25727 : if (is_function_symbol(e))
1804 : {
1805 24885 : return atermpp::down_cast<function_symbol>(e) == first();
1806 : }
1807 842 : return false;
1808 : }
1809 :
1810 : /// \brief Application of function symbol \@first.
1811 :
1812 : /// \param arg0 A data expression.
1813 : /// \return Application of \@first to a number of arguments.
1814 : inline
1815 12592 : application first(const data_expression& arg0)
1816 : {
1817 12592 : return sort_nat::first()(arg0);
1818 : }
1819 :
1820 : /// \brief Make an application of function symbol \@first.
1821 : /// \param result The data expression where the \@first expression is put.
1822 :
1823 : /// \param arg0 A data expression.
1824 : inline
1825 : void make_first(data_expression& result, const data_expression& arg0)
1826 : {
1827 : make_application(result, sort_nat::first(),arg0);
1828 : }
1829 :
1830 : /// \brief Recogniser for application of \@first.
1831 : /// \param e A data expression.
1832 : /// \return true iff e is an application of function symbol first to a
1833 : /// number of arguments.
1834 : inline
1835 25727 : bool is_first_application(const atermpp::aterm_appl& e)
1836 : {
1837 25727 : return is_application(e) && is_first_function_symbol(atermpp::down_cast<application>(e).head());
1838 : }
1839 :
1840 : /// \brief Generate identifier \@last.
1841 : /// \return Identifier \@last.
1842 : inline
1843 112 : const core::identifier_string& last_name()
1844 : {
1845 112 : static core::identifier_string last_name = core::identifier_string("@last");
1846 112 : return last_name;
1847 : }
1848 :
1849 : /// \brief Constructor for function symbol \@last.
1850 :
1851 : /// \return Function symbol last.
1852 : inline
1853 48347 : const function_symbol& last()
1854 : {
1855 48347 : static function_symbol last(last_name(), make_function_sort_(natpair(), nat()));
1856 48347 : return last;
1857 : }
1858 :
1859 : /// \brief Recogniser for function \@last.
1860 : /// \param e A data expression.
1861 : /// \return true iff e is the function symbol matching \@last.
1862 : inline
1863 25723 : bool is_last_function_symbol(const atermpp::aterm_appl& e)
1864 : {
1865 25723 : if (is_function_symbol(e))
1866 : {
1867 24881 : return atermpp::down_cast<function_symbol>(e) == last();
1868 : }
1869 842 : return false;
1870 : }
1871 :
1872 : /// \brief Application of function symbol \@last.
1873 :
1874 : /// \param arg0 A data expression.
1875 : /// \return Application of \@last to a number of arguments.
1876 : inline
1877 12592 : application last(const data_expression& arg0)
1878 : {
1879 12592 : return sort_nat::last()(arg0);
1880 : }
1881 :
1882 : /// \brief Make an application of function symbol \@last.
1883 : /// \param result The data expression where the \@last expression is put.
1884 :
1885 : /// \param arg0 A data expression.
1886 : inline
1887 : void make_last(data_expression& result, const data_expression& arg0)
1888 : {
1889 : make_application(result, sort_nat::last(),arg0);
1890 : }
1891 :
1892 : /// \brief Recogniser for application of \@last.
1893 : /// \param e A data expression.
1894 : /// \return true iff e is an application of function symbol last to a
1895 : /// number of arguments.
1896 : inline
1897 25723 : bool is_last_application(const atermpp::aterm_appl& e)
1898 : {
1899 25723 : return is_application(e) && is_last_function_symbol(atermpp::down_cast<application>(e).head());
1900 : }
1901 :
1902 : /// \brief Generate identifier \@divmod.
1903 : /// \return Identifier \@divmod.
1904 : inline
1905 112 : const core::identifier_string& divmod_name()
1906 : {
1907 112 : static core::identifier_string divmod_name = core::identifier_string("@divmod");
1908 112 : return divmod_name;
1909 : }
1910 :
1911 : /// \brief Constructor for function symbol \@divmod.
1912 :
1913 : /// \return Function symbol divmod.
1914 : inline
1915 66336 : const function_symbol& divmod()
1916 : {
1917 66336 : static function_symbol divmod(divmod_name(), make_function_sort_(sort_pos::pos(), sort_pos::pos(), natpair()));
1918 66336 : return divmod;
1919 : }
1920 :
1921 : /// \brief Recogniser for function \@divmod.
1922 : /// \param e A data expression.
1923 : /// \return true iff e is the function symbol matching \@divmod.
1924 : inline
1925 18078 : bool is_divmod_function_symbol(const atermpp::aterm_appl& e)
1926 : {
1927 18078 : if (is_function_symbol(e))
1928 : {
1929 17686 : return atermpp::down_cast<function_symbol>(e) == divmod();
1930 : }
1931 392 : return false;
1932 : }
1933 :
1934 : /// \brief Application of function symbol \@divmod.
1935 :
1936 : /// \param arg0 A data expression.
1937 : /// \param arg1 A data expression.
1938 : /// \return Application of \@divmod to a number of arguments.
1939 : inline
1940 37776 : application divmod(const data_expression& arg0, const data_expression& arg1)
1941 : {
1942 37776 : return sort_nat::divmod()(arg0, arg1);
1943 : }
1944 :
1945 : /// \brief Make an application of function symbol \@divmod.
1946 : /// \param result The data expression where the \@divmod expression is put.
1947 :
1948 : /// \param arg0 A data expression.
1949 : /// \param arg1 A data expression.
1950 : inline
1951 : void make_divmod(data_expression& result, const data_expression& arg0, const data_expression& arg1)
1952 : {
1953 : make_application(result, sort_nat::divmod(),arg0, arg1);
1954 : }
1955 :
1956 : /// \brief Recogniser for application of \@divmod.
1957 : /// \param e A data expression.
1958 : /// \return true iff e is an application of function symbol divmod to a
1959 : /// number of arguments.
1960 : inline
1961 18482 : bool is_divmod_application(const atermpp::aterm_appl& e)
1962 : {
1963 18482 : return is_application(e) && is_divmod_function_symbol(atermpp::down_cast<application>(e).head());
1964 : }
1965 :
1966 : /// \brief Generate identifier \@gdivmod.
1967 : /// \return Identifier \@gdivmod.
1968 : inline
1969 112 : const core::identifier_string& generalised_divmod_name()
1970 : {
1971 112 : static core::identifier_string generalised_divmod_name = core::identifier_string("@gdivmod");
1972 112 : return generalised_divmod_name;
1973 : }
1974 :
1975 : /// \brief Constructor for function symbol \@gdivmod.
1976 :
1977 : /// \return Function symbol generalised_divmod.
1978 : inline
1979 23466 : const function_symbol& generalised_divmod()
1980 : {
1981 23466 : static function_symbol generalised_divmod(generalised_divmod_name(), make_function_sort_(natpair(), sort_bool::bool_(), sort_pos::pos(), natpair()));
1982 23466 : return generalised_divmod;
1983 : }
1984 :
1985 : /// \brief Recogniser for function \@gdivmod.
1986 : /// \param e A data expression.
1987 : /// \return true iff e is the function symbol matching \@gdivmod.
1988 : inline
1989 : bool is_generalised_divmod_function_symbol(const atermpp::aterm_appl& e)
1990 : {
1991 : if (is_function_symbol(e))
1992 : {
1993 : return atermpp::down_cast<function_symbol>(e) == generalised_divmod();
1994 : }
1995 : return false;
1996 : }
1997 :
1998 : /// \brief Application of function symbol \@gdivmod.
1999 :
2000 : /// \param arg0 A data expression.
2001 : /// \param arg1 A data expression.
2002 : /// \param arg2 A data expression.
2003 : /// \return Application of \@gdivmod to a number of arguments.
2004 : inline
2005 12592 : application generalised_divmod(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
2006 : {
2007 12592 : return sort_nat::generalised_divmod()(arg0, arg1, arg2);
2008 : }
2009 :
2010 : /// \brief Make an application of function symbol \@gdivmod.
2011 : /// \param result The data expression where the \@gdivmod expression is put.
2012 :
2013 : /// \param arg0 A data expression.
2014 : /// \param arg1 A data expression.
2015 : /// \param arg2 A data expression.
2016 : inline
2017 : void make_generalised_divmod(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
2018 : {
2019 : make_application(result, sort_nat::generalised_divmod(),arg0, arg1, arg2);
2020 : }
2021 :
2022 : /// \brief Recogniser for application of \@gdivmod.
2023 : /// \param e A data expression.
2024 : /// \return true iff e is an application of function symbol generalised_divmod to a
2025 : /// number of arguments.
2026 : inline
2027 : bool is_generalised_divmod_application(const atermpp::aterm_appl& e)
2028 : {
2029 : return is_application(e) && is_generalised_divmod_function_symbol(atermpp::down_cast<application>(e).head());
2030 : }
2031 :
2032 : /// \brief Generate identifier \@ggdivmod.
2033 : /// \return Identifier \@ggdivmod.
2034 : inline
2035 112 : const core::identifier_string& doubly_generalised_divmod_name()
2036 : {
2037 112 : static core::identifier_string doubly_generalised_divmod_name = core::identifier_string("@ggdivmod");
2038 112 : return doubly_generalised_divmod_name;
2039 : }
2040 :
2041 : /// \brief Constructor for function symbol \@ggdivmod.
2042 :
2043 : /// \return Function symbol doubly_generalised_divmod.
2044 : inline
2045 36058 : const function_symbol& doubly_generalised_divmod()
2046 : {
2047 36058 : static function_symbol doubly_generalised_divmod(doubly_generalised_divmod_name(), make_function_sort_(nat(), nat(), sort_pos::pos(), natpair()));
2048 36058 : return doubly_generalised_divmod;
2049 : }
2050 :
2051 : /// \brief Recogniser for function \@ggdivmod.
2052 : /// \param e A data expression.
2053 : /// \return true iff e is the function symbol matching \@ggdivmod.
2054 : inline
2055 : bool is_doubly_generalised_divmod_function_symbol(const atermpp::aterm_appl& e)
2056 : {
2057 : if (is_function_symbol(e))
2058 : {
2059 : return atermpp::down_cast<function_symbol>(e) == doubly_generalised_divmod();
2060 : }
2061 : return false;
2062 : }
2063 :
2064 : /// \brief Application of function symbol \@ggdivmod.
2065 :
2066 : /// \param arg0 A data expression.
2067 : /// \param arg1 A data expression.
2068 : /// \param arg2 A data expression.
2069 : /// \return Application of \@ggdivmod to a number of arguments.
2070 : inline
2071 25184 : application doubly_generalised_divmod(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
2072 : {
2073 25184 : return sort_nat::doubly_generalised_divmod()(arg0, arg1, arg2);
2074 : }
2075 :
2076 : /// \brief Make an application of function symbol \@ggdivmod.
2077 : /// \param result The data expression where the \@ggdivmod expression is put.
2078 :
2079 : /// \param arg0 A data expression.
2080 : /// \param arg1 A data expression.
2081 : /// \param arg2 A data expression.
2082 : inline
2083 : void make_doubly_generalised_divmod(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
2084 : {
2085 : make_application(result, sort_nat::doubly_generalised_divmod(),arg0, arg1, arg2);
2086 : }
2087 :
2088 : /// \brief Recogniser for application of \@ggdivmod.
2089 : /// \param e A data expression.
2090 : /// \return true iff e is an application of function symbol doubly_generalised_divmod to a
2091 : /// number of arguments.
2092 : inline
2093 : bool is_doubly_generalised_divmod_application(const atermpp::aterm_appl& e)
2094 : {
2095 : return is_application(e) && is_doubly_generalised_divmod_function_symbol(atermpp::down_cast<application>(e).head());
2096 : }
2097 : /// \brief Give all system defined mappings for nat
2098 : /// \return All system defined mappings for nat
2099 : inline
2100 6296 : function_symbol_vector nat_generate_functions_code()
2101 : {
2102 6296 : function_symbol_vector result;
2103 6296 : result.push_back(sort_nat::pos2nat());
2104 6296 : result.push_back(sort_nat::nat2pos());
2105 6296 : result.push_back(sort_nat::maximum(sort_pos::pos(), nat()));
2106 6296 : result.push_back(sort_nat::maximum(nat(), sort_pos::pos()));
2107 6296 : result.push_back(sort_nat::maximum(nat(), nat()));
2108 6296 : result.push_back(sort_nat::minimum(nat(), nat()));
2109 6296 : result.push_back(sort_nat::succ(nat()));
2110 6296 : result.push_back(sort_nat::pred());
2111 6296 : result.push_back(sort_nat::dub());
2112 6296 : result.push_back(sort_nat::dubsucc());
2113 6296 : result.push_back(sort_nat::plus(sort_pos::pos(), nat()));
2114 6296 : result.push_back(sort_nat::plus(nat(), sort_pos::pos()));
2115 6296 : result.push_back(sort_nat::plus(nat(), nat()));
2116 6296 : result.push_back(sort_nat::gte_subtract_with_borrow());
2117 6296 : result.push_back(sort_nat::times(nat(), nat()));
2118 6296 : result.push_back(sort_nat::div());
2119 6296 : result.push_back(sort_nat::mod());
2120 6296 : result.push_back(sort_nat::exp(sort_pos::pos(), nat()));
2121 6296 : result.push_back(sort_nat::exp(nat(), nat()));
2122 6296 : result.push_back(sort_nat::even());
2123 6296 : result.push_back(sort_nat::monus());
2124 6296 : result.push_back(sort_nat::swap_zero());
2125 6296 : result.push_back(sort_nat::swap_zero_add());
2126 6296 : result.push_back(sort_nat::swap_zero_min());
2127 6296 : result.push_back(sort_nat::swap_zero_monus());
2128 6296 : result.push_back(sort_nat::sqrt());
2129 6296 : result.push_back(sort_nat::sqrt_nat_aux_func());
2130 6296 : result.push_back(sort_nat::first());
2131 6296 : result.push_back(sort_nat::last());
2132 6296 : result.push_back(sort_nat::divmod());
2133 6296 : result.push_back(sort_nat::generalised_divmod());
2134 6296 : result.push_back(sort_nat::doubly_generalised_divmod());
2135 6296 : return result;
2136 0 : }
2137 :
2138 : /// \brief Give all system defined mappings and constructors for nat
2139 : /// \return All system defined mappings for nat
2140 : inline
2141 : function_symbol_vector nat_generate_constructors_and_functions_code()
2142 : {
2143 : function_symbol_vector result=nat_generate_functions_code();
2144 : for(const function_symbol& f: nat_generate_constructors_code())
2145 : {
2146 : result.push_back(f);
2147 : }
2148 : return result;
2149 : }
2150 :
2151 : /// \brief Give all system defined mappings that can be used in mCRL2 specs for nat
2152 : /// \return All system defined mappings for that can be used in mCRL2 specificationis nat
2153 : inline
2154 4578 : function_symbol_vector nat_mCRL2_usable_mappings()
2155 : {
2156 4578 : function_symbol_vector result;
2157 4578 : result.push_back(sort_nat::pos2nat());
2158 4578 : result.push_back(sort_nat::nat2pos());
2159 4578 : result.push_back(sort_nat::maximum(sort_pos::pos(), nat()));
2160 4578 : result.push_back(sort_nat::maximum(nat(), sort_pos::pos()));
2161 4578 : result.push_back(sort_nat::maximum(nat(), nat()));
2162 4578 : result.push_back(sort_nat::minimum(nat(), nat()));
2163 4578 : result.push_back(sort_nat::succ(nat()));
2164 4578 : result.push_back(sort_nat::pred());
2165 4578 : result.push_back(sort_nat::dub());
2166 4578 : result.push_back(sort_nat::dubsucc());
2167 4578 : result.push_back(sort_nat::plus(sort_pos::pos(), nat()));
2168 4578 : result.push_back(sort_nat::plus(nat(), sort_pos::pos()));
2169 4578 : result.push_back(sort_nat::plus(nat(), nat()));
2170 4578 : result.push_back(sort_nat::gte_subtract_with_borrow());
2171 4578 : result.push_back(sort_nat::times(nat(), nat()));
2172 4578 : result.push_back(sort_nat::div());
2173 4578 : result.push_back(sort_nat::mod());
2174 4578 : result.push_back(sort_nat::exp(sort_pos::pos(), nat()));
2175 4578 : result.push_back(sort_nat::exp(nat(), nat()));
2176 4578 : result.push_back(sort_nat::even());
2177 4578 : result.push_back(sort_nat::monus());
2178 4578 : result.push_back(sort_nat::swap_zero());
2179 4578 : result.push_back(sort_nat::swap_zero_add());
2180 4578 : result.push_back(sort_nat::swap_zero_min());
2181 4578 : result.push_back(sort_nat::swap_zero_monus());
2182 4578 : result.push_back(sort_nat::sqrt());
2183 4578 : result.push_back(sort_nat::sqrt_nat_aux_func());
2184 4578 : result.push_back(sort_nat::first());
2185 4578 : result.push_back(sort_nat::last());
2186 4578 : result.push_back(sort_nat::divmod());
2187 4578 : result.push_back(sort_nat::generalised_divmod());
2188 4578 : result.push_back(sort_nat::doubly_generalised_divmod());
2189 4578 : return result;
2190 0 : }
2191 :
2192 :
2193 : // 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
2194 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
2195 : /// \brief Give all system defined mappings that are to be implemented in C++ code for nat
2196 : /// \return A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for nat
2197 : inline
2198 6296 : implementation_map nat_cpp_implementable_mappings()
2199 : {
2200 6296 : implementation_map result;
2201 6296 : return result;
2202 : }
2203 : ///\brief Function for projecting out argument.
2204 : /// arg from an application.
2205 : /// \param e A data expression.
2206 : /// \pre arg is defined for e.
2207 : /// \return The argument of e that corresponds to arg.
2208 : inline
2209 3358 : const data_expression& arg(const data_expression& e)
2210 : {
2211 3358 : assert(is_cnat_application(e) || is_pos2nat_application(e) || is_nat2pos_application(e) || is_succ_application(e) || is_pred_application(e) || is_dubsucc_application(e) || is_even_application(e) || is_sqrt_application(e) || is_first_application(e) || is_last_application(e));
2212 3358 : return atermpp::down_cast<application>(e)[0];
2213 : }
2214 :
2215 : ///\brief Function for projecting out argument.
2216 : /// arg1 from an application.
2217 : /// \param e A data expression.
2218 : /// \pre arg1 is defined for e.
2219 : /// \return The argument of e that corresponds to arg1.
2220 : inline
2221 : const data_expression& arg1(const data_expression& e)
2222 : {
2223 : assert(is_cpair_application(e) || is_gte_subtract_with_borrow_application(e) || is_swap_zero_add_application(e) || is_swap_zero_min_application(e) || is_swap_zero_monus_application(e) || is_sqrt_nat_aux_func_application(e) || is_generalised_divmod_application(e) || is_doubly_generalised_divmod_application(e));
2224 : return atermpp::down_cast<application>(e)[0];
2225 : }
2226 :
2227 : ///\brief Function for projecting out argument.
2228 : /// arg2 from an application.
2229 : /// \param e A data expression.
2230 : /// \pre arg2 is defined for e.
2231 : /// \return The argument of e that corresponds to arg2.
2232 : inline
2233 : const data_expression& arg2(const data_expression& e)
2234 : {
2235 : assert(is_cpair_application(e) || is_gte_subtract_with_borrow_application(e) || is_swap_zero_add_application(e) || is_swap_zero_min_application(e) || is_swap_zero_monus_application(e) || is_sqrt_nat_aux_func_application(e) || is_generalised_divmod_application(e) || is_doubly_generalised_divmod_application(e));
2236 : return atermpp::down_cast<application>(e)[1];
2237 : }
2238 :
2239 : ///\brief Function for projecting out argument.
2240 : /// left from an application.
2241 : /// \param e A data expression.
2242 : /// \pre left is defined for e.
2243 : /// \return The argument of e that corresponds to left.
2244 : inline
2245 22 : const data_expression& left(const data_expression& e)
2246 : {
2247 22 : assert(is_maximum_application(e) || is_minimum_application(e) || is_dub_application(e) || is_plus_application(e) || is_times_application(e) || is_div_application(e) || is_mod_application(e) || is_exp_application(e) || is_monus_application(e) || is_swap_zero_application(e) || is_divmod_application(e));
2248 22 : return atermpp::down_cast<application>(e)[0];
2249 : }
2250 :
2251 : ///\brief Function for projecting out argument.
2252 : /// right from an application.
2253 : /// \param e A data expression.
2254 : /// \pre right is defined for e.
2255 : /// \return The argument of e that corresponds to right.
2256 : inline
2257 21 : const data_expression& right(const data_expression& e)
2258 : {
2259 21 : assert(is_maximum_application(e) || is_minimum_application(e) || is_dub_application(e) || is_plus_application(e) || is_times_application(e) || is_div_application(e) || is_mod_application(e) || is_exp_application(e) || is_monus_application(e) || is_swap_zero_application(e) || is_divmod_application(e));
2260 21 : return atermpp::down_cast<application>(e)[1];
2261 : }
2262 :
2263 : ///\brief Function for projecting out argument.
2264 : /// arg3 from an application.
2265 : /// \param e A data expression.
2266 : /// \pre arg3 is defined for e.
2267 : /// \return The argument of e that corresponds to arg3.
2268 : inline
2269 : const data_expression& arg3(const data_expression& e)
2270 : {
2271 : assert(is_gte_subtract_with_borrow_application(e) || is_swap_zero_add_application(e) || is_swap_zero_min_application(e) || is_swap_zero_monus_application(e) || is_sqrt_nat_aux_func_application(e) || is_generalised_divmod_application(e) || is_doubly_generalised_divmod_application(e));
2272 : return atermpp::down_cast<application>(e)[2];
2273 : }
2274 :
2275 : ///\brief Function for projecting out argument.
2276 : /// arg4 from an application.
2277 : /// \param e A data expression.
2278 : /// \pre arg4 is defined for e.
2279 : /// \return The argument of e that corresponds to arg4.
2280 : inline
2281 : const data_expression& arg4(const data_expression& e)
2282 : {
2283 : assert(is_swap_zero_add_application(e) || is_swap_zero_min_application(e) || is_swap_zero_monus_application(e));
2284 : return atermpp::down_cast<application>(e)[3];
2285 : }
2286 :
2287 : /// \brief Give all system defined equations for nat
2288 : /// \return All system defined equations for sort nat
2289 : inline
2290 6296 : data_equation_vector nat_generate_equations_code()
2291 : {
2292 12592 : variable vb("b",sort_bool::bool_());
2293 12592 : variable vc("c",sort_bool::bool_());
2294 12592 : variable vp("p",sort_pos::pos());
2295 12592 : variable vq("q",sort_pos::pos());
2296 12592 : variable vn("n",nat());
2297 12592 : variable vm("m",nat());
2298 12592 : variable vu("u",nat());
2299 12592 : variable vv("v",nat());
2300 :
2301 6296 : data_equation_vector result;
2302 12592 : result.push_back(data_equation(variable_list({vp}), equal_to(c0(), cnat(vp)), sort_bool::false_()));
2303 12592 : result.push_back(data_equation(variable_list({vp}), equal_to(cnat(vp), c0()), sort_bool::false_()));
2304 18888 : result.push_back(data_equation(variable_list({vp, vq}), equal_to(cnat(vp), cnat(vq)), equal_to(vp, vq)));
2305 12592 : result.push_back(data_equation(variable_list({vn}), less(vn, c0()), sort_bool::false_()));
2306 12592 : result.push_back(data_equation(variable_list({vp}), less(c0(), cnat(vp)), sort_bool::true_()));
2307 18888 : result.push_back(data_equation(variable_list({vp, vq}), less(cnat(vp), cnat(vq)), less(vp, vq)));
2308 12592 : result.push_back(data_equation(variable_list({vn}), less_equal(c0(), vn), sort_bool::true_()));
2309 12592 : result.push_back(data_equation(variable_list({vp}), less_equal(cnat(vp), c0()), sort_bool::false_()));
2310 18888 : result.push_back(data_equation(variable_list({vp, vq}), less_equal(cnat(vp), cnat(vq)), less_equal(vp, vq)));
2311 12592 : result.push_back(data_equation(variable_list({vp}), pos2nat(vp), cnat(vp)));
2312 12592 : result.push_back(data_equation(variable_list({vp}), nat2pos(cnat(vp)), vp));
2313 12592 : result.push_back(data_equation(variable_list({vp}), maximum(vp, c0()), vp));
2314 18888 : result.push_back(data_equation(variable_list({vp, vq}), maximum(vp, cnat(vq)), if_(less_equal(vp, vq), vq, vp)));
2315 12592 : result.push_back(data_equation(variable_list({vp}), maximum(c0(), vp), vp));
2316 18888 : result.push_back(data_equation(variable_list({vp, vq}), maximum(cnat(vp), vq), if_(less_equal(vp, vq), vq, vp)));
2317 18888 : result.push_back(data_equation(variable_list({vm, vn}), maximum(vm, vn), if_(less_equal(vm, vn), vn, vm)));
2318 18888 : result.push_back(data_equation(variable_list({vm, vn}), minimum(vm, vn), if_(less_equal(vm, vn), vm, vn)));
2319 6296 : result.push_back(data_equation(variable_list(), succ(c0()), sort_pos::c1()));
2320 12592 : result.push_back(data_equation(variable_list({vp}), succ(cnat(vp)), succ(vp)));
2321 6296 : result.push_back(data_equation(variable_list(), pred(sort_pos::c1()), c0()));
2322 18888 : result.push_back(data_equation(variable_list({vb, vp}), pred(sort_pos::cdub(vb, vp)), cnat(if_(vb, sort_pos::cdub(sort_bool::false_(), vp), dubsucc(pred(vp))))));
2323 6296 : result.push_back(data_equation(variable_list(), dubsucc(c0()), sort_pos::c1()));
2324 12592 : result.push_back(data_equation(variable_list({vp}), dubsucc(cnat(vp)), sort_pos::cdub(sort_bool::true_(), vp)));
2325 6296 : result.push_back(data_equation(variable_list(), dub(sort_bool::false_(), c0()), c0()));
2326 6296 : result.push_back(data_equation(variable_list(), dub(sort_bool::true_(), c0()), cnat(sort_pos::c1())));
2327 18888 : result.push_back(data_equation(variable_list({vb, vp}), dub(vb, cnat(vp)), cnat(sort_pos::cdub(vb, vp))));
2328 12592 : result.push_back(data_equation(variable_list({vp}), plus(vp, c0()), vp));
2329 18888 : result.push_back(data_equation(variable_list({vp, vq}), plus(vp, cnat(vq)), sort_pos::add_with_carry(sort_bool::false_(), vp, vq)));
2330 12592 : result.push_back(data_equation(variable_list({vp}), plus(c0(), vp), vp));
2331 18888 : result.push_back(data_equation(variable_list({vp, vq}), plus(cnat(vp), vq), sort_pos::add_with_carry(sort_bool::false_(), vp, vq)));
2332 12592 : result.push_back(data_equation(variable_list({vn}), plus(c0(), vn), vn));
2333 12592 : result.push_back(data_equation(variable_list({vn}), plus(vn, c0()), vn));
2334 18888 : result.push_back(data_equation(variable_list({vp, vq}), plus(cnat(vp), cnat(vq)), cnat(sort_pos::add_with_carry(sort_bool::false_(), vp, vq))));
2335 12592 : result.push_back(data_equation(variable_list({vp}), gte_subtract_with_borrow(sort_bool::false_(), vp, sort_pos::c1()), pred(vp)));
2336 12592 : result.push_back(data_equation(variable_list({vp}), gte_subtract_with_borrow(sort_bool::true_(), vp, sort_pos::c1()), pred(nat2pos(pred(vp)))));
2337 31480 : result.push_back(data_equation(variable_list({vb, vc, vp, vq}), gte_subtract_with_borrow(vb, sort_pos::cdub(vc, vp), sort_pos::cdub(vc, vq)), dub(vb, gte_subtract_with_borrow(vb, vp, vq))));
2338 25184 : result.push_back(data_equation(variable_list({vb, vp, vq}), gte_subtract_with_borrow(vb, sort_pos::cdub(sort_bool::false_(), vp), sort_pos::cdub(sort_bool::true_(), vq)), dub(sort_bool::not_(vb), gte_subtract_with_borrow(sort_bool::true_(), vp, vq))));
2339 25184 : result.push_back(data_equation(variable_list({vb, vp, vq}), gte_subtract_with_borrow(vb, sort_pos::cdub(sort_bool::true_(), vp), sort_pos::cdub(sort_bool::false_(), vq)), dub(sort_bool::not_(vb), gte_subtract_with_borrow(sort_bool::false_(), vp, vq))));
2340 12592 : result.push_back(data_equation(variable_list({vn}), times(c0(), vn), c0()));
2341 12592 : result.push_back(data_equation(variable_list({vn}), times(vn, c0()), c0()));
2342 18888 : result.push_back(data_equation(variable_list({vp, vq}), times(cnat(vp), cnat(vq)), cnat(times(vp, vq))));
2343 12592 : result.push_back(data_equation(variable_list({vp}), exp(vp, c0()), sort_pos::c1()));
2344 12592 : result.push_back(data_equation(variable_list({vp}), exp(vp, cnat(sort_pos::c1())), vp));
2345 18888 : result.push_back(data_equation(variable_list({vp, vq}), exp(vp, cnat(sort_pos::cdub(sort_bool::false_(), vq))), exp(times(vp, vp), cnat(vq))));
2346 18888 : result.push_back(data_equation(variable_list({vp, vq}), exp(vp, cnat(sort_pos::cdub(sort_bool::true_(), vq))), times(vp, exp(times(vp, vp), cnat(vq)))));
2347 12592 : result.push_back(data_equation(variable_list({vn}), exp(vn, c0()), cnat(sort_pos::c1())));
2348 12592 : result.push_back(data_equation(variable_list({vp}), exp(c0(), cnat(vp)), c0()));
2349 18888 : result.push_back(data_equation(variable_list({vn, vp}), exp(cnat(vp), vn), cnat(exp(vp, vn))));
2350 6296 : result.push_back(data_equation(variable_list(), even(c0()), sort_bool::true_()));
2351 6296 : result.push_back(data_equation(variable_list(), even(cnat(sort_pos::c1())), sort_bool::false_()));
2352 18888 : result.push_back(data_equation(variable_list({vb, vp}), even(cnat(sort_pos::cdub(vb, vp))), sort_bool::not_(vb)));
2353 12592 : result.push_back(data_equation(variable_list({vp}), div(c0(), vp), c0()));
2354 18888 : result.push_back(data_equation(variable_list({vp, vq}), div(cnat(vp), vq), first(divmod(vp, vq))));
2355 12592 : result.push_back(data_equation(variable_list({vp}), mod(c0(), vp), c0()));
2356 18888 : result.push_back(data_equation(variable_list({vp, vq}), mod(cnat(vp), vq), last(divmod(vp, vq))));
2357 12592 : result.push_back(data_equation(variable_list({vn}), monus(c0(), vn), c0()));
2358 12592 : result.push_back(data_equation(variable_list({vn}), monus(vn, c0()), vn));
2359 18888 : result.push_back(data_equation(variable_list({vp, vq}), monus(cnat(vp), cnat(vq)), gte_subtract_with_borrow(sort_bool::false_(), vp, vq)));
2360 12592 : result.push_back(data_equation(variable_list({vm}), swap_zero(vm, c0()), vm));
2361 12592 : result.push_back(data_equation(variable_list({vn}), swap_zero(c0(), vn), vn));
2362 12592 : result.push_back(data_equation(variable_list({vp}), swap_zero(cnat(vp), cnat(vp)), c0()));
2363 18888 : result.push_back(data_equation(variable_list({vp, vq}), not_equal_to(vp, vq), swap_zero(cnat(vp), cnat(vq)), cnat(vq)));
2364 18888 : result.push_back(data_equation(variable_list({vm, vn}), swap_zero_add(c0(), c0(), vm, vn), plus(vm, vn)));
2365 18888 : result.push_back(data_equation(variable_list({vm, vp}), swap_zero_add(cnat(vp), c0(), vm, c0()), vm));
2366 25184 : result.push_back(data_equation(variable_list({vm, vp, vq}), swap_zero_add(cnat(vp), c0(), vm, cnat(vq)), swap_zero(cnat(vp), plus(swap_zero(cnat(vp), vm), cnat(vq)))));
2367 18888 : result.push_back(data_equation(variable_list({vn, vp}), swap_zero_add(c0(), cnat(vp), c0(), vn), vn));
2368 25184 : result.push_back(data_equation(variable_list({vn, vp, vq}), swap_zero_add(c0(), cnat(vp), cnat(vq), vn), swap_zero(cnat(vp), plus(cnat(vq), swap_zero(cnat(vp), vn)))));
2369 31480 : result.push_back(data_equation(variable_list({vm, vn, vp, vq}), swap_zero_add(cnat(vp), cnat(vq), vm, vn), swap_zero(plus(cnat(vp), cnat(vq)), plus(swap_zero(cnat(vp), vm), swap_zero(cnat(vq), vn)))));
2370 18888 : result.push_back(data_equation(variable_list({vm, vn}), swap_zero_min(c0(), c0(), vm, vn), minimum(vm, vn)));
2371 18888 : result.push_back(data_equation(variable_list({vm, vp}), swap_zero_min(cnat(vp), c0(), vm, c0()), c0()));
2372 25184 : result.push_back(data_equation(variable_list({vm, vp, vq}), swap_zero_min(cnat(vp), c0(), vm, cnat(vq)), minimum(swap_zero(cnat(vp), vm), cnat(vq))));
2373 18888 : result.push_back(data_equation(variable_list({vn, vp}), swap_zero_min(c0(), cnat(vp), c0(), vn), c0()));
2374 25184 : result.push_back(data_equation(variable_list({vn, vp, vq}), swap_zero_min(c0(), cnat(vp), cnat(vq), vn), minimum(cnat(vq), swap_zero(cnat(vp), vn))));
2375 31480 : result.push_back(data_equation(variable_list({vm, vn, vp, vq}), swap_zero_min(cnat(vp), cnat(vq), vm, vn), swap_zero(minimum(cnat(vp), cnat(vq)), minimum(swap_zero(cnat(vp), vm), swap_zero(cnat(vq), vn)))));
2376 18888 : result.push_back(data_equation(variable_list({vm, vn}), swap_zero_monus(c0(), c0(), vm, vn), monus(vm, vn)));
2377 18888 : result.push_back(data_equation(variable_list({vm, vp}), swap_zero_monus(cnat(vp), c0(), vm, c0()), vm));
2378 25184 : result.push_back(data_equation(variable_list({vm, vp, vq}), swap_zero_monus(cnat(vp), c0(), vm, cnat(vq)), swap_zero(cnat(vp), monus(swap_zero(cnat(vp), vm), cnat(vq)))));
2379 18888 : result.push_back(data_equation(variable_list({vn, vp}), swap_zero_monus(c0(), cnat(vp), c0(), vn), c0()));
2380 25184 : result.push_back(data_equation(variable_list({vn, vp, vq}), swap_zero_monus(c0(), cnat(vp), cnat(vq), vn), monus(cnat(vq), swap_zero(cnat(vp), vn))));
2381 31480 : result.push_back(data_equation(variable_list({vm, vn, vp, vq}), swap_zero_monus(cnat(vp), cnat(vq), vm, vn), swap_zero(monus(cnat(vp), cnat(vq)), monus(swap_zero(cnat(vp), vm), swap_zero(cnat(vq), vn)))));
2382 6296 : result.push_back(data_equation(variable_list(), sqrt(c0()), c0()));
2383 12592 : result.push_back(data_equation(variable_list({vp}), sqrt(cnat(vp)), sqrt_nat_aux_func(cnat(vp), c0(), sort_pos::powerlog2_pos(vp))));
2384 18888 : result.push_back(data_equation(variable_list({vm, vn}), sqrt_nat_aux_func(vn, vm, sort_pos::c1()), if_(less_equal(vn, vm), c0(), cnat(sort_pos::c1()))));
2385 31480 : result.push_back(data_equation(variable_list({vb, vm, vn, vp}), sqrt_nat_aux_func(vn, vm, sort_pos::cdub(vb, vp)), if_(greater(times(plus(cnat(sort_pos::cdub(vb, vp)), vm), cnat(sort_pos::cdub(vb, vp))), vn), sqrt_nat_aux_func(vn, vm, vp), plus(cnat(sort_pos::cdub(vb, vp)), sqrt_nat_aux_func(monus(vn, times(plus(cnat(sort_pos::cdub(vb, vp)), vm), cnat(sort_pos::cdub(vb, vp)))), plus(vm, cnat(sort_pos::cdub(sort_bool::false_(), sort_pos::cdub(vb, vp)))), vp)))));
2386 31480 : result.push_back(data_equation(variable_list({vm, vn, vu, vv}), equal_to(cpair(vm, vn), cpair(vu, vv)), sort_bool::and_(equal_to(vm, vu), equal_to(vn, vv))));
2387 31480 : result.push_back(data_equation(variable_list({vm, vn, vu, vv}), less(cpair(vm, vn), cpair(vu, vv)), sort_bool::or_(less(vm, vu), sort_bool::and_(equal_to(vm, vu), less(vn, vv)))));
2388 31480 : result.push_back(data_equation(variable_list({vm, vn, vu, vv}), less_equal(cpair(vm, vn), cpair(vu, vv)), sort_bool::or_(less(vm, vu), sort_bool::and_(equal_to(vm, vu), less_equal(vn, vv)))));
2389 18888 : result.push_back(data_equation(variable_list({vm, vn}), first(cpair(vm, vn)), vm));
2390 18888 : result.push_back(data_equation(variable_list({vm, vn}), last(cpair(vm, vn)), vn));
2391 6296 : result.push_back(data_equation(variable_list(), divmod(sort_pos::c1(), sort_pos::c1()), cpair(cnat(sort_pos::c1()), c0())));
2392 18888 : result.push_back(data_equation(variable_list({vb, vp}), divmod(sort_pos::c1(), sort_pos::cdub(vb, vp)), cpair(c0(), cnat(sort_pos::c1()))));
2393 25184 : result.push_back(data_equation(variable_list({vb, vp, vq}), divmod(sort_pos::cdub(vb, vp), vq), generalised_divmod(divmod(vp, vq), vb, vq)));
2394 31480 : result.push_back(data_equation(variable_list({vb, vm, vn, vp}), generalised_divmod(cpair(vm, vn), vb, vp), doubly_generalised_divmod(dub(vb, vn), vm, vp)));
2395 18888 : result.push_back(data_equation(variable_list({vn, vp}), doubly_generalised_divmod(c0(), vn, vp), cpair(dub(sort_bool::false_(), vn), c0())));
2396 25184 : result.push_back(data_equation(variable_list({vn, vp, vq}), less(vp, vq), doubly_generalised_divmod(cnat(vp), vn, vq), cpair(dub(sort_bool::false_(), vn), cnat(vp))));
2397 25184 : result.push_back(data_equation(variable_list({vn, vp, vq}), less_equal(vq, vp), doubly_generalised_divmod(cnat(vp), vn, vq), cpair(dub(sort_bool::true_(), vn), gte_subtract_with_borrow(sort_bool::false_(), vp, vq))));
2398 12592 : return result;
2399 6296 : }
2400 :
2401 : } // namespace sort_nat
2402 :
2403 : } // namespace data
2404 :
2405 : } // namespace mcrl2
2406 :
2407 : #endif // MCRL2_DATA_NAT_H
|
