Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/pbes/pbes_expression.h
10 : /// \brief The class pbes_expression.
11 :
12 : #ifndef MCRL2_PBES_PBES_EXPRESSION_H
13 : #define MCRL2_PBES_PBES_EXPRESSION_H
14 :
15 : #include "mcrl2/data/expression_traits.h"
16 : #include "mcrl2/data/optimized_boolean_operators.h"
17 : #include "mcrl2/pbes/propositional_variable.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace pbes_system
23 : {
24 :
25 : //--- start generated classes ---//
26 : /// \\brief A pbes expression
27 : class pbes_expression: public atermpp::aterm_appl
28 : {
29 : public:
30 : /// \\brief Default constructor.
31 64101 : pbes_expression()
32 64101 : : atermpp::aterm_appl(core::detail::default_values::PBExpr)
33 64101 : {}
34 :
35 : /// \\brief Constructor.
36 : /// \\param term A term
37 419941 : explicit pbes_expression(const atermpp::aterm& term)
38 419941 : : atermpp::aterm_appl(term)
39 : {
40 419941 : assert(core::detail::check_rule_PBExpr(*this));
41 419941 : }
42 :
43 : /// \\brief Constructor.
44 20544 : pbes_expression(const data::data_expression& x)
45 20544 : : atermpp::aterm_appl(x)
46 20544 : {}
47 :
48 : /// \\brief Constructor.
49 9 : pbes_expression(const data::variable& x)
50 9 : : atermpp::aterm_appl(x)
51 9 : {}
52 :
53 : /// \\brief Constructor.
54 787 : pbes_expression(const data::untyped_data_parameter& x)
55 787 : : atermpp::aterm_appl(x)
56 787 : {}
57 :
58 : /// Move semantics
59 80321 : pbes_expression(const pbes_expression&) noexcept = default;
60 22092 : pbes_expression(pbes_expression&&) noexcept = default;
61 60480 : pbes_expression& operator=(const pbes_expression&) noexcept = default;
62 29792 : pbes_expression& operator=(pbes_expression&&) noexcept = default;
63 : };
64 :
65 : /// \\brief list of pbes_expressions
66 : typedef atermpp::term_list<pbes_expression> pbes_expression_list;
67 :
68 : /// \\brief vector of pbes_expressions
69 : typedef std::vector<pbes_expression> pbes_expression_vector;
70 :
71 : // prototypes
72 : inline bool is_propositional_variable_instantiation(const atermpp::aterm_appl& x);
73 : inline bool is_not(const atermpp::aterm_appl& x);
74 : inline bool is_and(const atermpp::aterm_appl& x);
75 : inline bool is_or(const atermpp::aterm_appl& x);
76 : inline bool is_imp(const atermpp::aterm_appl& x);
77 : inline bool is_forall(const atermpp::aterm_appl& x);
78 : inline bool is_exists(const atermpp::aterm_appl& x);
79 :
80 : /// \\brief Test for a pbes_expression expression
81 : /// \\param x A term
82 : /// \\return True if \\a x is a pbes_expression expression
83 : inline
84 : bool is_pbes_expression(const atermpp::aterm_appl& x)
85 : {
86 : return data::is_data_expression(x) ||
87 : data::is_variable(x) ||
88 : data::is_untyped_data_parameter(x) ||
89 : pbes_system::is_propositional_variable_instantiation(x) ||
90 : pbes_system::is_not(x) ||
91 : pbes_system::is_and(x) ||
92 : pbes_system::is_or(x) ||
93 : pbes_system::is_imp(x) ||
94 : pbes_system::is_forall(x) ||
95 : pbes_system::is_exists(x);
96 : }
97 :
98 : // prototype declaration
99 : std::string pp(const pbes_expression& x);
100 :
101 : /// \\brief Outputs the object to a stream
102 : /// \\param out An output stream
103 : /// \\param x Object x
104 : /// \\return The output stream
105 : inline
106 6515 : std::ostream& operator<<(std::ostream& out, const pbes_expression& x)
107 : {
108 6515 : return out << pbes_system::pp(x);
109 : }
110 :
111 : /// \\brief swap overload
112 : inline void swap(pbes_expression& t1, pbes_expression& t2)
113 : {
114 : t1.swap(t2);
115 : }
116 :
117 :
118 : /// \\brief A propositional variable instantiation
119 : class propositional_variable_instantiation: public pbes_expression
120 : {
121 : public:
122 :
123 :
124 : /// Move semantics
125 17568 : propositional_variable_instantiation(const propositional_variable_instantiation&) noexcept = default;
126 321 : propositional_variable_instantiation(propositional_variable_instantiation&&) noexcept = default;
127 5804 : propositional_variable_instantiation& operator=(const propositional_variable_instantiation&) noexcept = default;
128 1103 : propositional_variable_instantiation& operator=(propositional_variable_instantiation&&) noexcept = default;
129 :
130 92214 : const core::identifier_string& name() const
131 : {
132 92214 : return atermpp::down_cast<core::identifier_string>((*this)[0]);
133 : }
134 :
135 64494 : const data::data_expression_list& parameters() const
136 : {
137 64494 : return atermpp::down_cast<data::data_expression_list>((*this)[1]);
138 : }
139 : //--- start user section propositional_variable_instantiation ---//
140 : /// \brief Default constructor.
141 8360 : propositional_variable_instantiation()
142 8360 : : pbes_expression(core::detail::default_values::PropVarInst)
143 8360 : {}
144 :
145 : /// \brief Constructor.
146 : /// \param term A term
147 71145 : explicit propositional_variable_instantiation(const atermpp::aterm& term)
148 71145 : : pbes_expression(term)
149 : {
150 71145 : assert(core::detail::check_term_PropVarInst(*this));
151 71145 : }
152 :
153 : /// \brief Constructor.
154 8769 : explicit propositional_variable_instantiation(const core::identifier_string& name, const data::data_expression_list& parameters)
155 8769 : {
156 8769 : atermpp::make_term_appl(*this,core::detail::function_symbol_PropVarInst(), name, parameters);
157 8769 : }
158 :
159 : /// \brief Constructor.
160 1966 : explicit propositional_variable_instantiation(const std::string& name, const data::data_expression_list& parameters)
161 1966 : : propositional_variable_instantiation(core::identifier_string(name), parameters)
162 : {
163 1966 : }
164 :
165 : /// \brief Constructor.
166 36 : explicit propositional_variable_instantiation(const core::identifier_string& name)
167 36 : : propositional_variable_instantiation(name, data::data_expression_list())
168 : {
169 36 : }
170 :
171 : /// \brief Constructor.
172 234 : explicit propositional_variable_instantiation(const std::string& name)
173 234 : : propositional_variable_instantiation(name, data::data_expression_list())
174 : {
175 234 : }
176 :
177 : //--- end user section propositional_variable_instantiation ---//
178 : };
179 :
180 : /// \\brief Make_propositional_variable_instantiation constructs a new term into a given address.
181 : /// \\ \param t The reference into which the new propositional_variable_instantiation is constructed.
182 : template <class... ARGUMENTS>
183 17220 : inline void make_propositional_variable_instantiation(atermpp::aterm_appl& t, const ARGUMENTS&... args)
184 : {
185 17220 : atermpp::make_term_appl(t, core::detail::function_symbol_PropVarInst(), args...);
186 17220 : }
187 :
188 : /// \\brief list of propositional_variable_instantiations
189 : typedef atermpp::term_list<propositional_variable_instantiation> propositional_variable_instantiation_list;
190 :
191 : /// \\brief vector of propositional_variable_instantiations
192 : typedef std::vector<propositional_variable_instantiation> propositional_variable_instantiation_vector;
193 :
194 : /// \\brief Test for a propositional_variable_instantiation expression
195 : /// \\param x A term
196 : /// \\return True if \\a x is a propositional_variable_instantiation expression
197 : inline
198 203030 : bool is_propositional_variable_instantiation(const atermpp::aterm_appl& x)
199 : {
200 203030 : return x.function() == core::detail::function_symbols::PropVarInst;
201 : }
202 :
203 : // prototype declaration
204 : std::string pp(const propositional_variable_instantiation& x);
205 :
206 : /// \\brief Outputs the object to a stream
207 : /// \\param out An output stream
208 : /// \\param x Object x
209 : /// \\return The output stream
210 : inline
211 74 : std::ostream& operator<<(std::ostream& out, const propositional_variable_instantiation& x)
212 : {
213 74 : return out << pbes_system::pp(x);
214 : }
215 :
216 : /// \\brief swap overload
217 : inline void swap(propositional_variable_instantiation& t1, propositional_variable_instantiation& t2)
218 : {
219 : t1.swap(t2);
220 : }
221 :
222 :
223 : /// \\brief The not operator for pbes expressions
224 : class not_: public pbes_expression
225 : {
226 : public:
227 : /// \\brief Default constructor.
228 : not_()
229 : : pbes_expression(core::detail::default_values::PBESNot)
230 : {}
231 :
232 : /// \\brief Constructor.
233 : /// \\param term A term
234 1668 : explicit not_(const atermpp::aterm& term)
235 1668 : : pbes_expression(term)
236 : {
237 1668 : assert(core::detail::check_term_PBESNot(*this));
238 1668 : }
239 :
240 : /// \\brief Constructor.
241 420 : explicit not_(const pbes_expression& operand)
242 420 : : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESNot(), operand))
243 420 : {}
244 :
245 : /// Move semantics
246 : not_(const not_&) noexcept = default;
247 : not_(not_&&) noexcept = default;
248 : not_& operator=(const not_&) noexcept = default;
249 : not_& operator=(not_&&) noexcept = default;
250 :
251 1630 : const pbes_expression& operand() const
252 : {
253 1630 : return atermpp::down_cast<pbes_expression>((*this)[0]);
254 : }
255 : };
256 :
257 : /// \\brief Make_not_ constructs a new term into a given address.
258 : /// \\ \param t The reference into which the new not_ is constructed.
259 : template <class... ARGUMENTS>
260 734 : inline void make_not_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
261 : {
262 734 : atermpp::make_term_appl(t, core::detail::function_symbol_PBESNot(), args...);
263 734 : }
264 :
265 : /// \\brief Test for a not expression
266 : /// \\param x A term
267 : /// \\return True if \\a x is a not expression
268 : inline
269 127803 : bool is_not(const atermpp::aterm_appl& x)
270 : {
271 127803 : return x.function() == core::detail::function_symbols::PBESNot;
272 : }
273 :
274 : // prototype declaration
275 : std::string pp(const not_& x);
276 :
277 : /// \\brief Outputs the object to a stream
278 : /// \\param out An output stream
279 : /// \\param x Object x
280 : /// \\return The output stream
281 : inline
282 : std::ostream& operator<<(std::ostream& out, const not_& x)
283 : {
284 : return out << pbes_system::pp(x);
285 : }
286 :
287 : /// \\brief swap overload
288 : inline void swap(not_& t1, not_& t2)
289 : {
290 : t1.swap(t2);
291 : }
292 :
293 :
294 : /// \\brief The and operator for pbes expressions
295 : class and_: public pbes_expression
296 : {
297 : public:
298 : /// \\brief Default constructor.
299 : and_()
300 : : pbes_expression(core::detail::default_values::PBESAnd)
301 : {}
302 :
303 : /// \\brief Constructor.
304 : /// \\param term A term
305 56287 : explicit and_(const atermpp::aterm& term)
306 56287 : : pbes_expression(term)
307 : {
308 56287 : assert(core::detail::check_term_PBESAnd(*this));
309 56287 : }
310 :
311 : /// \\brief Constructor.
312 672 : and_(const pbes_expression& left, const pbes_expression& right)
313 672 : : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESAnd(), left, right))
314 672 : {}
315 :
316 : /// Move semantics
317 : and_(const and_&) noexcept = default;
318 : and_(and_&&) noexcept = default;
319 : and_& operator=(const and_&) noexcept = default;
320 : and_& operator=(and_&&) noexcept = default;
321 :
322 53516 : const pbes_expression& left() const
323 : {
324 53516 : return atermpp::down_cast<pbes_expression>((*this)[0]);
325 : }
326 :
327 50238 : const pbes_expression& right() const
328 : {
329 50238 : return atermpp::down_cast<pbes_expression>((*this)[1]);
330 : }
331 : };
332 :
333 : /// \\brief Make_and_ constructs a new term into a given address.
334 : /// \\ \param t The reference into which the new and_ is constructed.
335 : template <class... ARGUMENTS>
336 13061 : inline void make_and_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
337 : {
338 13061 : atermpp::make_term_appl(t, core::detail::function_symbol_PBESAnd(), args...);
339 13061 : }
340 :
341 : /// \\brief Test for a and expression
342 : /// \\param x A term
343 : /// \\return True if \\a x is a and expression
344 : inline
345 150090 : bool is_and(const atermpp::aterm_appl& x)
346 : {
347 150090 : return x.function() == core::detail::function_symbols::PBESAnd;
348 : }
349 :
350 : // prototype declaration
351 : std::string pp(const and_& x);
352 :
353 : /// \\brief Outputs the object to a stream
354 : /// \\param out An output stream
355 : /// \\param x Object x
356 : /// \\return The output stream
357 : inline
358 : std::ostream& operator<<(std::ostream& out, const and_& x)
359 : {
360 : return out << pbes_system::pp(x);
361 : }
362 :
363 : /// \\brief swap overload
364 : inline void swap(and_& t1, and_& t2)
365 : {
366 : t1.swap(t2);
367 : }
368 :
369 :
370 : /// \\brief The or operator for pbes expressions
371 : class or_: public pbes_expression
372 : {
373 : public:
374 : /// \\brief Default constructor.
375 : or_()
376 : : pbes_expression(core::detail::default_values::PBESOr)
377 : {}
378 :
379 : /// \\brief Constructor.
380 : /// \\param term A term
381 50278 : explicit or_(const atermpp::aterm& term)
382 50278 : : pbes_expression(term)
383 : {
384 50278 : assert(core::detail::check_term_PBESOr(*this));
385 50278 : }
386 :
387 : /// \\brief Constructor.
388 445 : or_(const pbes_expression& left, const pbes_expression& right)
389 445 : : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESOr(), left, right))
390 445 : {}
391 :
392 : /// Move semantics
393 : or_(const or_&) noexcept = default;
394 : or_(or_&&) noexcept = default;
395 : or_& operator=(const or_&) noexcept = default;
396 : or_& operator=(or_&&) noexcept = default;
397 :
398 45658 : const pbes_expression& left() const
399 : {
400 45658 : return atermpp::down_cast<pbes_expression>((*this)[0]);
401 : }
402 :
403 28273 : const pbes_expression& right() const
404 : {
405 28273 : return atermpp::down_cast<pbes_expression>((*this)[1]);
406 : }
407 : };
408 :
409 : /// \\brief Make_or_ constructs a new term into a given address.
410 : /// \\ \param t The reference into which the new or_ is constructed.
411 : template <class... ARGUMENTS>
412 7440 : inline void make_or_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
413 : {
414 7440 : atermpp::make_term_appl(t, core::detail::function_symbol_PBESOr(), args...);
415 7440 : }
416 :
417 : /// \\brief Test for a or expression
418 : /// \\param x A term
419 : /// \\return True if \\a x is a or expression
420 : inline
421 84010 : bool is_or(const atermpp::aterm_appl& x)
422 : {
423 84010 : return x.function() == core::detail::function_symbols::PBESOr;
424 : }
425 :
426 : // prototype declaration
427 : std::string pp(const or_& x);
428 :
429 : /// \\brief Outputs the object to a stream
430 : /// \\param out An output stream
431 : /// \\param x Object x
432 : /// \\return The output stream
433 : inline
434 : std::ostream& operator<<(std::ostream& out, const or_& x)
435 : {
436 : return out << pbes_system::pp(x);
437 : }
438 :
439 : /// \\brief swap overload
440 : inline void swap(or_& t1, or_& t2)
441 : {
442 : t1.swap(t2);
443 : }
444 :
445 :
446 : /// \\brief The implication operator for pbes expressions
447 : class imp: public pbes_expression
448 : {
449 : public:
450 : /// \\brief Default constructor.
451 : imp()
452 : : pbes_expression(core::detail::default_values::PBESImp)
453 : {}
454 :
455 : /// \\brief Constructor.
456 : /// \\param term A term
457 5194 : explicit imp(const atermpp::aterm& term)
458 5194 : : pbes_expression(term)
459 : {
460 5194 : assert(core::detail::check_term_PBESImp(*this));
461 5194 : }
462 :
463 : /// \\brief Constructor.
464 186 : imp(const pbes_expression& left, const pbes_expression& right)
465 186 : : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESImp(), left, right))
466 186 : {}
467 :
468 : /// Move semantics
469 : imp(const imp&) noexcept = default;
470 : imp(imp&&) noexcept = default;
471 : imp& operator=(const imp&) noexcept = default;
472 : imp& operator=(imp&&) noexcept = default;
473 :
474 4869 : const pbes_expression& left() const
475 : {
476 4869 : return atermpp::down_cast<pbes_expression>((*this)[0]);
477 : }
478 :
479 4855 : const pbes_expression& right() const
480 : {
481 4855 : return atermpp::down_cast<pbes_expression>((*this)[1]);
482 : }
483 : };
484 :
485 : /// \\brief Make_imp constructs a new term into a given address.
486 : /// \\ \param t The reference into which the new imp is constructed.
487 : template <class... ARGUMENTS>
488 1069 : inline void make_imp(atermpp::aterm_appl& t, const ARGUMENTS&... args)
489 : {
490 1069 : atermpp::make_term_appl(t, core::detail::function_symbol_PBESImp(), args...);
491 1069 : }
492 :
493 : /// \\brief Test for a imp expression
494 : /// \\param x A term
495 : /// \\return True if \\a x is a imp expression
496 : inline
497 32725 : bool is_imp(const atermpp::aterm_appl& x)
498 : {
499 32725 : return x.function() == core::detail::function_symbols::PBESImp;
500 : }
501 :
502 : // prototype declaration
503 : std::string pp(const imp& x);
504 :
505 : /// \\brief Outputs the object to a stream
506 : /// \\param out An output stream
507 : /// \\param x Object x
508 : /// \\return The output stream
509 : inline
510 : std::ostream& operator<<(std::ostream& out, const imp& x)
511 : {
512 : return out << pbes_system::pp(x);
513 : }
514 :
515 : /// \\brief swap overload
516 : inline void swap(imp& t1, imp& t2)
517 : {
518 : t1.swap(t2);
519 : }
520 :
521 :
522 : /// \\brief The universal quantification operator for pbes expressions
523 : class forall: public pbes_expression
524 : {
525 : public:
526 : /// \\brief Default constructor.
527 : forall()
528 : : pbes_expression(core::detail::default_values::PBESForall)
529 : {}
530 :
531 : /// \\brief Constructor.
532 : /// \\param term A term
533 6290 : explicit forall(const atermpp::aterm& term)
534 6290 : : pbes_expression(term)
535 : {
536 6290 : assert(core::detail::check_term_PBESForall(*this));
537 6290 : }
538 :
539 : /// \\brief Constructor.
540 566 : forall(const data::variable_list& variables, const pbes_expression& body)
541 566 : : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESForall(), variables, body))
542 566 : {}
543 :
544 : /// Move semantics
545 119 : forall(const forall&) noexcept = default;
546 : forall(forall&&) noexcept = default;
547 : forall& operator=(const forall&) noexcept = default;
548 : forall& operator=(forall&&) noexcept = default;
549 :
550 10003 : const data::variable_list& variables() const
551 : {
552 10003 : return atermpp::down_cast<data::variable_list>((*this)[0]);
553 : }
554 :
555 5819 : const pbes_expression& body() const
556 : {
557 5819 : return atermpp::down_cast<pbes_expression>((*this)[1]);
558 : }
559 : };
560 :
561 : /// \\brief Make_forall constructs a new term into a given address.
562 : /// \\ \param t The reference into which the new forall is constructed.
563 : template <class... ARGUMENTS>
564 773 : inline void make_forall(atermpp::aterm_appl& t, const ARGUMENTS&... args)
565 : {
566 773 : atermpp::make_term_appl(t, core::detail::function_symbol_PBESForall(), args...);
567 773 : }
568 :
569 : /// \\brief Test for a forall expression
570 : /// \\param x A term
571 : /// \\return True if \\a x is a forall expression
572 : inline
573 28689 : bool is_forall(const atermpp::aterm_appl& x)
574 : {
575 28689 : return x.function() == core::detail::function_symbols::PBESForall;
576 : }
577 :
578 : // prototype declaration
579 : std::string pp(const forall& x);
580 :
581 : /// \\brief Outputs the object to a stream
582 : /// \\param out An output stream
583 : /// \\param x Object x
584 : /// \\return The output stream
585 : inline
586 0 : std::ostream& operator<<(std::ostream& out, const forall& x)
587 : {
588 0 : return out << pbes_system::pp(x);
589 : }
590 :
591 : /// \\brief swap overload
592 : inline void swap(forall& t1, forall& t2)
593 : {
594 : t1.swap(t2);
595 : }
596 :
597 :
598 : /// \\brief The existential quantification operator for pbes expressions
599 : class exists: public pbes_expression
600 : {
601 : public:
602 : /// \\brief Default constructor.
603 : exists()
604 : : pbes_expression(core::detail::default_values::PBESExists)
605 : {}
606 :
607 : /// \\brief Constructor.
608 : /// \\param term A term
609 4829 : explicit exists(const atermpp::aterm& term)
610 4829 : : pbes_expression(term)
611 : {
612 4829 : assert(core::detail::check_term_PBESExists(*this));
613 4829 : }
614 :
615 : /// \\brief Constructor.
616 443 : exists(const data::variable_list& variables, const pbes_expression& body)
617 443 : : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESExists(), variables, body))
618 443 : {}
619 :
620 : /// Move semantics
621 126 : exists(const exists&) noexcept = default;
622 : exists(exists&&) noexcept = default;
623 : exists& operator=(const exists&) noexcept = default;
624 : exists& operator=(exists&&) noexcept = default;
625 :
626 5877 : const data::variable_list& variables() const
627 : {
628 5877 : return atermpp::down_cast<data::variable_list>((*this)[0]);
629 : }
630 :
631 4672 : const pbes_expression& body() const
632 : {
633 4672 : return atermpp::down_cast<pbes_expression>((*this)[1]);
634 : }
635 : };
636 :
637 : /// \\brief Make_exists constructs a new term into a given address.
638 : /// \\ \param t The reference into which the new exists is constructed.
639 : template <class... ARGUMENTS>
640 375 : inline void make_exists(atermpp::aterm_appl& t, const ARGUMENTS&... args)
641 : {
642 375 : atermpp::make_term_appl(t, core::detail::function_symbol_PBESExists(), args...);
643 375 : }
644 :
645 : /// \\brief Test for a exists expression
646 : /// \\param x A term
647 : /// \\return True if \\a x is a exists expression
648 : inline
649 22251 : bool is_exists(const atermpp::aterm_appl& x)
650 : {
651 22251 : return x.function() == core::detail::function_symbols::PBESExists;
652 : }
653 :
654 : // prototype declaration
655 : std::string pp(const exists& x);
656 :
657 : /// \\brief Outputs the object to a stream
658 : /// \\param out An output stream
659 : /// \\param x Object x
660 : /// \\return The output stream
661 : inline
662 0 : std::ostream& operator<<(std::ostream& out, const exists& x)
663 : {
664 0 : return out << pbes_system::pp(x);
665 : }
666 :
667 : /// \\brief swap overload
668 : inline void swap(exists& t1, exists& t2)
669 : {
670 : t1.swap(t2);
671 : }
672 : //--- end generated classes ---//
673 :
674 : // template function overloads
675 : std::string pp(const pbes_expression_list& x);
676 : std::string pp(const pbes_expression_vector& x);
677 : std::string pp(const propositional_variable_instantiation_list& x);
678 : std::string pp(const propositional_variable_instantiation_vector& x);
679 : std::set<pbes_system::propositional_variable_instantiation> find_propositional_variable_instantiations(const pbes_system::pbes_expression& x);
680 : std::set<core::identifier_string> find_identifiers(const pbes_system::pbes_expression& x);
681 : std::set<data::variable> find_free_variables(const pbes_system::pbes_expression& x);
682 : bool search_variable(const pbes_system::pbes_expression& x, const data::variable& v);
683 : pbes_system::pbes_expression normalize_sorts(const pbes_system::pbes_expression& x, const data::sort_specification& sortspec);
684 : pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression& x);
685 :
686 : /// \return Returns the value true
687 : inline
688 22770 : const pbes_expression& true_()
689 : {
690 : /* The dynamic cast is required, to prevent copying the data term true to
691 : a local term on the stack. */
692 22770 : return reinterpret_cast<const pbes_expression&>(data::sort_bool::true_());
693 : }
694 :
695 : /// \return Returns the value false
696 : inline
697 10561 : const pbes_expression& false_()
698 : {
699 : /* The dynamic cast is required, to prevent copying the data term false to
700 : a local term on the stack. */
701 10561 : return reinterpret_cast<const pbes_expression&>(data::sort_bool::false_());
702 : }
703 :
704 : /// \brief Test for the value true
705 : /// \param t A PBES expression
706 : /// \return True if it is the value \p true
707 87843 : inline bool is_true(const pbes_expression& t)
708 : {
709 87843 : return data::sort_bool::is_true_function_symbol(t);
710 : }
711 :
712 : /// \brief Test for the value false
713 : /// \param t A PBES expression
714 : /// \return True if it is the value \p false
715 74150 : inline bool is_false(const pbes_expression& t)
716 : {
717 74150 : return data::sort_bool::is_false_function_symbol(t);
718 : }
719 :
720 : /// \brief Returns true if the term t is a not expression
721 : /// \param t A PBES expression
722 : /// \return True if the term t is a not expression
723 496 : inline bool is_pbes_not(const pbes_expression& t)
724 : {
725 496 : return pbes_system::is_not(t);
726 : }
727 :
728 : /// \brief Returns true if the term t is an and expression
729 : /// \param t A PBES expression
730 : /// \return True if the term t is an and expression
731 10617 : inline bool is_pbes_and(const pbes_expression& t)
732 : {
733 10617 : return pbes_system::is_and(t);
734 : }
735 :
736 : /// \brief Returns true if the term t is an or expression
737 : /// \param t A PBES expression
738 : /// \return True if the term t is an or expression
739 1970 : inline bool is_pbes_or(const pbes_expression& t)
740 : {
741 1970 : return pbes_system::is_or(t);
742 : }
743 :
744 : /// \brief Returns true if the term t is an imp expression
745 : /// \param t A PBES expression
746 : /// \return True if the term t is an imp expression
747 : inline bool is_pbes_imp(const pbes_expression& t)
748 : {
749 : return pbes_system::is_imp(t);
750 : }
751 :
752 : /// \brief Returns true if the term t is a universal quantification
753 : /// \param t A PBES expression
754 : /// \return True if the term t is a universal quantification
755 : inline bool is_pbes_forall(const pbes_expression& t)
756 : {
757 : return pbes_system::is_forall(t);
758 : }
759 :
760 : /// \brief Returns true if the term t is an existential quantification
761 : /// \param t A PBES expression
762 : /// \return True if the term t is an existential quantification
763 : inline bool is_pbes_exists(const pbes_expression& t)
764 : {
765 : return pbes_system::is_exists(t);
766 : }
767 :
768 : /// \brief Test for a conjunction
769 : /// \param t A PBES expression or a data expression
770 : /// \return True if it is a conjunction
771 110 : inline bool is_universal_not(const pbes_expression& t)
772 : {
773 110 : return is_pbes_not(t) || data::sort_bool::is_not_application(t);
774 : }
775 :
776 : /// \brief Test for a conjunction
777 : /// \param t A PBES expression or a data expression
778 : /// \return True if it is a conjunction
779 0 : inline bool is_universal_and(const pbes_expression& t)
780 : {
781 0 : return is_pbes_and(t) || data::sort_bool::is_and_application(t);
782 : }
783 :
784 : /// \brief Test for a disjunction
785 : /// \param t A PBES expression or a data expression
786 : /// \return True if it is a disjunction
787 0 : inline bool is_universal_or(const pbes_expression& t)
788 : {
789 0 : return is_pbes_or(t) || data::sort_bool::is_or_application(t);
790 : }
791 :
792 : /// \brief Returns true if the term t is a data expression
793 : /// \param t A PBES expression
794 : /// \return True if the term t is a data expression
795 17161 : inline bool is_data(const pbes_expression& t)
796 : {
797 17161 : return data::is_data_expression(t);
798 : }
799 :
800 : /// \brief The namespace for accessor functions on pbes expressions.
801 : namespace accessors
802 : {
803 :
804 : /// \brief Returns the pbes expression argument of expressions of type not, exists and forall.
805 : /// \param t A PBES expression
806 : /// \return The pbes expression argument of expressions of type not, exists and forall.
807 : inline
808 235 : const pbes_expression& arg(const pbes_expression& t)
809 : {
810 235 : if (is_pbes_not(t))
811 : {
812 3 : return atermpp::down_cast<const pbes_expression>(t[0]);
813 : }
814 : else
815 : {
816 232 : assert(is_forall(t) || is_exists(t));
817 232 : return atermpp::down_cast<const pbes_expression>(t[1]);
818 : }
819 : }
820 :
821 : /// \brief Returns the pbes expression argument of expressions of type not, exists and forall.
822 : /// \param t A PBES expression or a data expression
823 : /// \return The pbes expression argument of expressions of type not, exists and forall.
824 : inline
825 : pbes_expression data_arg(const pbes_expression& t)
826 : {
827 : if (data::is_data_expression(t))
828 : {
829 : assert(data::is_application(t));
830 : const auto& a = atermpp::down_cast<const data::application>(t);
831 : return *(a.begin());
832 : }
833 : else
834 : {
835 : return arg(t);
836 : }
837 : }
838 :
839 : /// \brief Returns the left hand side of an expression of type and, or or imp.
840 : /// \param t A PBES expression
841 : /// \return The left hand side of an expression of type and, or or imp.
842 : inline
843 5840 : const pbes_expression& left(const pbes_expression& t)
844 : {
845 5840 : assert(is_and(t) || is_or(t) || is_imp(t));
846 5840 : return atermpp::down_cast<pbes_expression>(t[0]);
847 : }
848 :
849 : /// \brief Returns the left hand side of an expression of type and, or or imp.
850 : /// \param x A PBES expression or a data expression
851 : /// \return The left hand side of an expression of type and, or or imp.
852 : inline
853 3 : pbes_expression data_left(const pbes_expression& x)
854 : {
855 3 : if (data::is_data_expression(x))
856 : {
857 2 : return data::binary_left(atermpp::down_cast<data::application>(x));
858 : }
859 : else
860 : {
861 1 : return left(x);
862 : }
863 : }
864 :
865 : /// \brief Returns the right hand side of an expression of type and, or or imp.
866 : /// \param t A PBES expression
867 : /// \return The right hand side of an expression of type and, or or imp.
868 : inline
869 5820 : const pbes_expression& right(const pbes_expression& t)
870 : {
871 5820 : return atermpp::down_cast<pbes_expression>(t[1]);
872 : }
873 :
874 : /// \brief Returns the left hand side of an expression of type and, or or imp.
875 : /// \param x A PBES expression or a data expression
876 : /// \return The left hand side of an expression of type and, or or imp.
877 : inline
878 3 : pbes_expression data_right(const pbes_expression& x)
879 : {
880 3 : if (data::is_data_expression(x))
881 : {
882 2 : return data::binary_right(atermpp::down_cast<data::application>(x));
883 : }
884 : else
885 : {
886 1 : return right(x);
887 : }
888 : }
889 :
890 : /// \brief Returns the variables of a quantification expression
891 : /// \param t A PBES expression
892 : /// \return The variables of a quantification expression
893 : inline
894 2 : const data::variable_list& var(const pbes_expression& t)
895 : {
896 2 : assert(is_forall(t) || is_exists(t));
897 2 : return atermpp::down_cast<data::variable_list>(t[0]);
898 : }
899 :
900 : /// \brief Returns the name of a propositional variable expression
901 : /// \param t A PBES expression
902 : /// \return The name of a propositional variable expression
903 : inline
904 2 : const core::identifier_string& name(const pbes_expression& t)
905 : {
906 2 : assert(is_propositional_variable_instantiation(t));
907 2 : return atermpp::down_cast<core::identifier_string>(t[0]);
908 : }
909 :
910 : /// \brief Returns the parameters of a propositional variable instantiation.
911 : /// \param t A PBES expression
912 : /// \return The parameters of a propositional variable instantiation.
913 : inline
914 2 : const data::data_expression_list& param(const pbes_expression& t)
915 : {
916 2 : assert(is_propositional_variable_instantiation(t));
917 2 : return atermpp::down_cast<data::data_expression_list>(t[1]);
918 : }
919 : } // namespace accessors
920 :
921 : /// \brief Make a universal quantification. It checks for an empty variable list,
922 : /// which is not allowed.
923 : /// \param l A sequence of data variables
924 : /// \param p A PBES expression
925 : /// \return The value <tt>forall l.p</tt>
926 : inline
927 739 : pbes_expression make_forall_(const data::variable_list& l, const pbes_expression& p)
928 : {
929 739 : if (l.empty())
930 : {
931 240 : return p;
932 : }
933 998 : return pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESForall(), l, p));
934 : }
935 :
936 : /// \brief Make an existential quantification. It checks for an empty variable list,
937 : /// which is not allowed.
938 : /// \param l A sequence of data variables
939 : /// \param p A PBES expression
940 : /// \return The value <tt>exists l.p</tt>
941 : inline
942 2971 : pbes_expression make_exists_(const data::variable_list& l, const pbes_expression& p)
943 : {
944 2971 : if (l.empty())
945 : {
946 2246 : return p;
947 : }
948 1450 : return pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESExists(), l, p));
949 : }
950 :
951 : /// \brief Make a negation
952 : /// \param p A PBES expression
953 : /// \return The value <tt>!p</tt>
954 : inline
955 : void optimized_not(pbes_expression& result, const pbes_expression& p)
956 : {
957 : data::optimized_not(result, p);
958 : }
959 :
960 : /// \brief Make a conjunction
961 : /// \param p A PBES expression
962 : /// \param q A PBES expression
963 : /// \return The value <tt>p && q</tt>
964 : inline
965 4874 : void optimized_and(pbes_expression& result, const pbes_expression& p, const pbes_expression& q)
966 : {
967 4874 : data::optimized_and(result, p, q);
968 4874 : }
969 :
970 : /// \brief Make a disjunction
971 : /// \param p A PBES expression
972 : /// \param q A PBES expression
973 : /// \return The value <tt>p || q</tt>
974 : inline
975 1406 : void optimized_or(pbes_expression& result, const pbes_expression& p, const pbes_expression& q)
976 : {
977 1406 : data::optimized_or(result, p, q);
978 1406 : }
979 :
980 : /// \brief Make an implication
981 : /// \param p A PBES expression
982 : /// \param q A PBES expression
983 : /// \return The value <tt>p => q</tt>
984 : inline
985 288 : void optimized_imp(pbes_expression& result, const pbes_expression& p, const pbes_expression& q)
986 : {
987 288 : data::optimized_imp(result, p, q);
988 288 : }
989 :
990 : /// \brief Make a universal quantification
991 : /// If l is empty, p is returned.
992 : /// \param l A sequence of data variables
993 : /// \param p A PBES expression
994 : /// \return The value <tt>forall l.p</tt>
995 : inline
996 : void optimized_forall(pbes_expression& result, const data::variable_list& l, const pbes_expression& p)
997 : {
998 : if (l.empty())
999 : {
1000 : result = p;
1001 : return;
1002 : }
1003 : if (is_false(p))
1004 : {
1005 : // N.B. Here we use the fact that mCRL2 data types are never empty.
1006 : result = data::sort_bool::false_();
1007 : return;
1008 : }
1009 : if (is_true(p))
1010 : {
1011 : result = true_();
1012 : return;
1013 : }
1014 : make_forall(result, l, p);
1015 : return;
1016 : }
1017 :
1018 : /// \brief Make an existential quantification
1019 : /// If l is empty, p is returned.
1020 : /// \param l A sequence of data variables
1021 : /// \param p A PBES expression
1022 : /// \return The value <tt>exists l.p</tt>
1023 : inline
1024 : void optimized_exists(pbes_expression& result, const data::variable_list& l, const pbes_expression& p)
1025 : {
1026 : if (l.empty())
1027 : {
1028 : result = p;
1029 : return;
1030 : }
1031 : if (is_false(p))
1032 : {
1033 : result = data::sort_bool::false_();
1034 : return;
1035 : }
1036 : if (is_true(p))
1037 : {
1038 : // N.B. Here we use the fact that mCRL2 data types are never empty.
1039 : result = data::sort_bool::true_();
1040 : return;
1041 : }
1042 : make_exists(result, l, p);
1043 : return;
1044 : }
1045 :
1046 : inline
1047 : bool is_constant(const pbes_expression& x)
1048 : {
1049 : return find_free_variables(x).empty();
1050 : }
1051 :
1052 : inline
1053 165 : const data::variable_list& quantifier_variables(const pbes_expression& x)
1054 : {
1055 165 : assert(is_exists(x) || is_forall(x));
1056 165 : if (is_exists(x))
1057 : {
1058 0 : return atermpp::down_cast<exists>(x).variables();
1059 : }
1060 : else
1061 : {
1062 165 : return atermpp::down_cast<forall>(x).variables();
1063 : }
1064 : }
1065 :
1066 : inline
1067 489 : data::variable_list free_variables(const pbes_expression& x)
1068 : {
1069 489 : std::set<data::variable> v = find_free_variables(x);
1070 978 : return data::variable_list(v.begin(), v.end());
1071 489 : }
1072 :
1073 : } // namespace pbes_system
1074 :
1075 : } // namespace mcrl2
1076 :
1077 : namespace mcrl2
1078 : {
1079 :
1080 : namespace core
1081 : {
1082 :
1083 : /// \brief Contains type information for pbes expressions.
1084 : template <>
1085 : struct term_traits<pbes_system::pbes_expression>
1086 : {
1087 : /// \brief The term type
1088 : typedef pbes_system::pbes_expression term_type;
1089 :
1090 : /// \brief The data term type
1091 : typedef data::data_expression data_term_type;
1092 :
1093 : /// \brief The data term sequence type
1094 : typedef data::data_expression_list data_term_sequence_type;
1095 :
1096 : /// \brief The variable type
1097 : typedef data::variable variable_type;
1098 :
1099 : /// \brief The variable sequence type
1100 : typedef data::variable_list variable_sequence_type;
1101 :
1102 : /// \brief The propositional variable declaration type
1103 : typedef pbes_system::propositional_variable propositional_variable_decl_type;
1104 :
1105 : /// \brief The propositional variable instantiation type
1106 : typedef pbes_system::propositional_variable_instantiation propositional_variable_type;
1107 :
1108 : /// \brief The string type
1109 : typedef core::identifier_string string_type;
1110 :
1111 : /// \brief Make the value true
1112 : /// \return The value \p true
1113 : static inline
1114 885 : term_type true_()
1115 : {
1116 885 : return pbes_system::true_();
1117 : }
1118 :
1119 : /// \brief Make the value false
1120 : /// \return The value \p false
1121 : static inline
1122 4591 : term_type false_()
1123 : {
1124 4591 : return pbes_system::false_();
1125 : }
1126 :
1127 : /// \brief Make a negation
1128 : /// \param p A term
1129 : /// \return The value <tt>!p</tt>
1130 : static inline
1131 1 : term_type not_(const term_type& p)
1132 : {
1133 1 : return pbes_system::not_(p);
1134 : }
1135 :
1136 : /// \brief Make a negation
1137 : /// \param result The value <tt>!p</tt>
1138 : /// \param p A term
1139 : static inline
1140 253 : void make_not_(term_type& result, const term_type& p)
1141 : {
1142 253 : pbes_system::make_not_(result, p);
1143 253 : }
1144 :
1145 : /// \brief Make a conjunction
1146 : /// \param p A term
1147 : /// \param q A term
1148 : /// \return The value <tt>p && q</tt>
1149 : static inline
1150 7 : term_type and_(const term_type& p, const term_type& q)
1151 : {
1152 7 : return pbes_system::and_(p, q);
1153 : }
1154 :
1155 : /// \brief Make a conjunction
1156 : /// \param result The value <tt>p && q</tt>
1157 : /// \param p A term
1158 : /// \param q A term
1159 : static inline
1160 2567 : void make_and_(term_type& result, const term_type& p, const term_type& q)
1161 : {
1162 2567 : pbes_system::make_and_(result, p, q);
1163 2567 : }
1164 :
1165 : /// \brief Make a disjunction
1166 : /// \param p A term
1167 : /// \param q A term
1168 : /// \return The value <tt>p || q</tt>
1169 : static inline
1170 2 : term_type or_(const term_type& p, const term_type& q)
1171 : {
1172 2 : return pbes_system::or_(p, q);
1173 : }
1174 :
1175 : /// \brief Make a disjunction
1176 : /// \param result The value <tt>p || q</tt>
1177 : /// \param p A term
1178 : /// \param q A term
1179 : static inline
1180 1025 : void make_or_(term_type& result, const term_type& p, const term_type& q)
1181 : {
1182 1025 : pbes_system::make_or_(result, p,q);
1183 1025 : }
1184 :
1185 : template <typename FwdIt>
1186 : static inline
1187 0 : term_type join_or(FwdIt first, FwdIt last)
1188 : {
1189 0 : return utilities::detail::join(first, last, or_, false_());
1190 : }
1191 :
1192 : template <typename FwdIt>
1193 : static inline
1194 0 : term_type join_and(FwdIt first, FwdIt last)
1195 : {
1196 0 : return utilities::detail::join(first, last, and_, true_());
1197 : }
1198 :
1199 : /// \brief Make an implication
1200 : /// \param p A term
1201 : /// \param q A term
1202 : /// \return The value <tt>p => q</tt>
1203 : static inline
1204 1 : term_type imp(const term_type& p, const term_type& q)
1205 : {
1206 1 : return pbes_system::imp(p, q);
1207 : }
1208 :
1209 : /// \brief Make an implication
1210 : /// \param result The value <tt>p => q</tt>
1211 : /// \param p A term
1212 : /// \param q A term
1213 : static inline
1214 535 : void make_imp(term_type& result, const term_type& p, const term_type& q)
1215 : {
1216 535 : pbes_system::make_imp(result, p, q);
1217 535 : }
1218 :
1219 : /// \brief Make a universal quantification
1220 : /// \param l A sequence of variables
1221 : /// \param p A term
1222 : /// \return The value <tt>forall l.p</tt>
1223 : static inline
1224 470 : term_type forall(const variable_sequence_type& l, const term_type& p)
1225 : {
1226 470 : if (l.empty())
1227 : {
1228 369 : return p;
1229 : }
1230 101 : return pbes_system::forall(l, p);
1231 : }
1232 :
1233 : /// \brief Make a universal quantification
1234 : /// \param result The value <tt>forall l.p</tt>
1235 : /// \param l A sequence of variables
1236 : /// \param p A term
1237 : static inline
1238 121 : void make_forall(term_type& result, const variable_sequence_type& l, const term_type& p)
1239 : {
1240 121 : if (l.empty())
1241 : {
1242 0 : result = p;
1243 0 : return;
1244 : }
1245 121 : pbes_system::make_forall(result, l, p);
1246 : }
1247 :
1248 : /// \brief Make an existential quantification
1249 : /// \param l A sequence of variables
1250 : /// \param p A term
1251 : /// \return The value <tt>exists l.p</tt>
1252 : static inline
1253 438 : term_type exists(const variable_sequence_type& l, const term_type& p)
1254 : {
1255 438 : if (l.empty())
1256 : {
1257 242 : return p;
1258 : }
1259 196 : return pbes_system::exists(l, p);
1260 : }
1261 :
1262 : /// \brief Make an existential quantification
1263 : /// \param result The value <tt>exists l.p</tt>
1264 : /// \param l A sequence of variables
1265 : /// \param p A term
1266 : static inline
1267 0 : void make_exists(term_type& result, const variable_sequence_type& l, const term_type& p)
1268 : {
1269 0 : if (l.empty())
1270 : {
1271 0 : result = p;
1272 0 : return;
1273 : }
1274 0 : pbes_system::make_exists(result, l, p);
1275 : }
1276 :
1277 : /// \brief Test for the value true
1278 : /// \param t A term
1279 : /// \return True if it is the value \p true
1280 : static inline
1281 25078 : bool is_true(const term_type& t)
1282 : {
1283 25078 : return data::sort_bool::is_true_function_symbol(t);
1284 : }
1285 :
1286 : /// \brief Test for the value false
1287 : /// \param t A term
1288 : /// \return True if it is the value \p false
1289 : static inline
1290 22408 : bool is_false(const term_type& t)
1291 : {
1292 22408 : return data::sort_bool::is_false_function_symbol(t);
1293 : }
1294 :
1295 : /// \brief Test for a negation
1296 : /// \param t A term
1297 : /// \return True if it is a negation
1298 : static inline
1299 411 : bool is_not(const term_type& t)
1300 : {
1301 411 : return pbes_system::is_not(t);
1302 : }
1303 :
1304 : /// \brief Test for a conjunction
1305 : /// \param t A term
1306 : /// \return True if it is a conjunction
1307 : static inline
1308 7 : bool is_and(const term_type& t)
1309 : {
1310 7 : return pbes_system::is_and(t);
1311 : }
1312 :
1313 : /// \brief Test for a disjunction
1314 : /// \param t A term
1315 : /// \return True if it is a disjunction
1316 : static inline
1317 7 : bool is_or(const term_type& t)
1318 : {
1319 7 : return pbes_system::is_or(t);
1320 : }
1321 :
1322 : /// \brief Test for an implication
1323 : /// \param t A term
1324 : /// \return True if it is an implication
1325 : static inline
1326 7 : bool is_imp(const term_type& t)
1327 : {
1328 7 : return pbes_system::is_imp(t);
1329 : }
1330 :
1331 : /// \brief Test for an universal quantification
1332 : /// \param t A term
1333 : /// \return True if it is a universal quantification
1334 : static inline
1335 1 : bool is_forall(const term_type& t)
1336 : {
1337 1 : return pbes_system::is_forall(t);
1338 : }
1339 :
1340 : /// \brief Test for an existential quantification
1341 : /// \param t A term
1342 : /// \return True if it is an existential quantification
1343 : static inline
1344 2 : bool is_exists(const term_type& t)
1345 : {
1346 2 : return pbes_system::is_exists(t);
1347 : }
1348 :
1349 : /// \brief Test for data term
1350 : /// \param t A term
1351 : /// \return True if the term is a data term
1352 : static inline
1353 : bool is_data(const term_type& t)
1354 : {
1355 : return data::is_data_expression(t);
1356 : }
1357 :
1358 : /// \brief Test for propositional variable instantiation
1359 : /// \param t A term
1360 : /// \return True if the term is a propositional variable instantiation
1361 : static inline
1362 2 : bool is_prop_var(const term_type& t)
1363 : {
1364 2 : return pbes_system::is_propositional_variable_instantiation(t);
1365 : }
1366 :
1367 : /// \brief Returns the left argument of a term of type and, or or imp
1368 : /// \param t A term
1369 : /// \return The left argument of the term. Also works for data terms
1370 : static inline
1371 0 : term_type left(const term_type& t)
1372 : {
1373 0 : return pbes_system::accessors::left(t);
1374 : }
1375 :
1376 : /// \brief Returns the right argument of a term of type and, or or imp
1377 : /// \param t A term
1378 : /// \return The right argument of the term. Also works for data terms
1379 : static inline
1380 0 : term_type right(const term_type& t)
1381 : {
1382 0 : return pbes_system::accessors::right(t);
1383 : }
1384 :
1385 : /// \brief Returns the argument of a term of type not
1386 : /// \param t A term
1387 : static inline
1388 151 : const term_type& not_arg(const term_type& t)
1389 : {
1390 151 : assert(is_pbes_not(t));
1391 151 : return atermpp::down_cast<term_type>(t[0]);
1392 : }
1393 :
1394 : /// \brief Returns the quantifier variables of a quantifier expression
1395 : /// \param t A term
1396 : /// \return The requested argument. Doesn't work for data terms
1397 : static inline
1398 2 : const variable_sequence_type& var(const term_type& t)
1399 : {
1400 : // Forall and exists are not fully supported by the data library
1401 2 : assert(!data::is_data_expression(t) || (!data::is_abstraction(t)
1402 : || (!data::is_forall(data::abstraction(t)) && !data::is_exists(data::abstraction(t)))));
1403 2 : assert(is_exists(t) || is_forall(t));
1404 :
1405 2 : return atermpp::down_cast<variable_sequence_type>(t[0]);
1406 : }
1407 :
1408 : /// \brief Returns the name of a propositional variable instantiation
1409 : /// \param t A term
1410 : /// \return The name of the propositional variable instantiation
1411 : static inline
1412 : const string_type &name(const term_type& t)
1413 : {
1414 : assert(is_prop_var(t));
1415 : return atermpp::down_cast<string_type>(t[0]);
1416 : }
1417 :
1418 : /// \brief Returns the parameter list of a propositional variable instantiation
1419 : /// \param t A term
1420 : /// \return The parameter list of the propositional variable instantiation
1421 : static inline
1422 : const data_term_sequence_type ¶m(const term_type& t)
1423 : {
1424 : assert(is_prop_var(t));
1425 : return atermpp::down_cast<data_term_sequence_type>(t[1]);
1426 : }
1427 :
1428 : /// \brief Conversion from variable to term
1429 : /// \param v A variable
1430 : /// \return The converted variable
1431 : static inline
1432 : const term_type& variable2term(const variable_type& v)
1433 : {
1434 : return atermpp::down_cast<term_type>(v);
1435 : }
1436 :
1437 : /// \brief Test if a term is a variable
1438 : /// \param t A term
1439 : /// \return True if the term is a variable
1440 : static inline
1441 : bool is_variable(const term_type& t)
1442 : {
1443 : return data::is_variable(t);
1444 : }
1445 :
1446 : /// \brief Pretty print function
1447 : /// \param t A term
1448 : /// \return Returns a pretty print representation of the term
1449 : static inline
1450 : std::string pp(const term_type& t)
1451 : {
1452 : return pbes_system::pp(t);
1453 : }
1454 : };
1455 :
1456 : } // namespace core
1457 :
1458 : } // namespace mcrl2
1459 :
1460 : namespace std
1461 : {
1462 :
1463 : template <>
1464 : struct hash<mcrl2::pbes_system::pbes_expression>
1465 : {
1466 23276 : std::size_t operator()(const mcrl2::pbes_system::pbes_expression& x) const
1467 : {
1468 23276 : return hash<atermpp::aterm>()(x);
1469 : }
1470 : };
1471 :
1472 : template <>
1473 : struct hash<mcrl2::pbes_system::propositional_variable_instantiation>
1474 : {
1475 22400 : std::size_t operator()(const mcrl2::pbes_system::propositional_variable_instantiation& x) const
1476 : {
1477 22400 : return hash<atermpp::aterm>()(x);
1478 : }
1479 : };
1480 :
1481 : } // namespace std
1482 :
1483 : #endif // MCRL2_PBES_PBES_EXPRESSION_H
|
