mCRL2
Loading...
Searching...
No Matches
pbes_expression.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_PBES_PBES_EXPRESSION_H
13#define MCRL2_PBES_PBES_EXPRESSION_H
14
18
19namespace mcrl2
20{
21
22namespace pbes_system
23{
24
25//--- start generated classes ---//
28{
29 public:
32 : atermpp::aterm_appl(core::detail::default_values::PBExpr)
33 {}
34
37 explicit pbes_expression(const atermpp::aterm& term)
38 : atermpp::aterm_appl(term)
39 {
41 }
42
45 : atermpp::aterm_appl(x)
46 {}
47
50 : atermpp::aterm_appl(x)
51 {}
52
55 : atermpp::aterm_appl(x)
56 {}
57
59 pbes_expression(const pbes_expression&) noexcept = default;
60 pbes_expression(pbes_expression&&) noexcept = default;
61 pbes_expression& operator=(const pbes_expression&) noexcept = default;
62 pbes_expression& operator=(pbes_expression&&) noexcept = default;
63};
64
67
70
71// prototypes
72inline bool is_propositional_variable_instantiation(const atermpp::aterm_appl& x);
73inline bool is_not(const atermpp::aterm_appl& x);
74inline bool is_and(const atermpp::aterm_appl& x);
75inline bool is_or(const atermpp::aterm_appl& x);
76inline bool is_imp(const atermpp::aterm_appl& x);
77inline bool is_forall(const atermpp::aterm_appl& x);
78inline bool is_exists(const atermpp::aterm_appl& x);
79
83inline
84bool is_pbes_expression(const atermpp::aterm_appl& x)
85{
86 return data::is_data_expression(x) ||
96}
97
98// prototype declaration
99std::string pp(const pbes_expression& x);
100
105inline
106std::ostream& operator<<(std::ostream& out, const pbes_expression& x)
107{
108 return out << pbes_system::pp(x);
109}
110
113{
114 t1.swap(t2);
115}
116
117
120{
121 public:
122
123
129
130 const core::identifier_string& name() const
131 {
132 return atermpp::down_cast<core::identifier_string>((*this)[0]);
133 }
134
136 {
137 return atermpp::down_cast<data::data_expression_list>((*this)[1]);
138 }
139//--- start user section propositional_variable_instantiation ---//
142 : pbes_expression(core::detail::default_values::PropVarInst)
143 {}
144
148 : pbes_expression(term)
149 {
150 assert(core::detail::check_term_PropVarInst(*this));
151 }
152
155 {
156 atermpp::make_term_appl(*this,core::detail::function_symbol_PropVarInst(), name, parameters);
157 }
158
160 explicit propositional_variable_instantiation(const std::string& name, const data::data_expression_list& parameters)
161 : propositional_variable_instantiation(core::identifier_string(name), parameters)
162 {
163 }
164
167 : propositional_variable_instantiation(name, data::data_expression_list())
168 {
169 }
170
172 explicit propositional_variable_instantiation(const std::string& name)
173 : propositional_variable_instantiation(name, data::data_expression_list())
174 {
175 }
176
177//--- end user section propositional_variable_instantiation ---//
178};
179
182template <class... ARGUMENTS>
183inline void make_propositional_variable_instantiation(atermpp::aterm_appl& t, const ARGUMENTS&... args)
184{
186}
187
190
192typedef std::vector<propositional_variable_instantiation> propositional_variable_instantiation_vector;
193
197inline
199{
201}
202
203// prototype declaration
204std::string pp(const propositional_variable_instantiation& x);
205
210inline
211std::ostream& operator<<(std::ostream& out, const propositional_variable_instantiation& x)
212{
213 return out << pbes_system::pp(x);
214}
215
218{
219 t1.swap(t2);
220}
221
222
225{
226 public:
229 : pbes_expression(core::detail::default_values::PBESNot)
230 {}
231
234 explicit not_(const atermpp::aterm& term)
235 : pbes_expression(term)
236 {
237 assert(core::detail::check_term_PBESNot(*this));
238 }
239
241 explicit not_(const pbes_expression& operand)
242 : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESNot(), operand))
243 {}
244
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 const pbes_expression& operand() const
252 {
253 return atermpp::down_cast<pbes_expression>((*this)[0]);
254 }
255};
256
259template <class... ARGUMENTS>
260inline void make_not_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
261{
263}
264
268inline
270{
272}
273
274// prototype declaration
275std::string pp(const not_& x);
276
281inline
282std::ostream& operator<<(std::ostream& out, const not_& x)
283{
284 return out << pbes_system::pp(x);
285}
286
288inline void swap(not_& t1, not_& t2)
289{
290 t1.swap(t2);
291}
292
293
296{
297 public:
300 : pbes_expression(core::detail::default_values::PBESAnd)
301 {}
302
305 explicit and_(const atermpp::aterm& term)
306 : pbes_expression(term)
307 {
308 assert(core::detail::check_term_PBESAnd(*this));
309 }
310
312 and_(const pbes_expression& left, const pbes_expression& right)
313 : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESAnd(), left, right))
314 {}
315
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 const pbes_expression& left() const
323 {
324 return atermpp::down_cast<pbes_expression>((*this)[0]);
325 }
326
327 const pbes_expression& right() const
328 {
329 return atermpp::down_cast<pbes_expression>((*this)[1]);
330 }
331};
332
335template <class... ARGUMENTS>
336inline void make_and_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
337{
339}
340
344inline
346{
348}
349
350// prototype declaration
351std::string pp(const and_& x);
352
357inline
358std::ostream& operator<<(std::ostream& out, const and_& x)
359{
360 return out << pbes_system::pp(x);
361}
362
364inline void swap(and_& t1, and_& t2)
365{
366 t1.swap(t2);
367}
368
369
371class or_: public pbes_expression
372{
373 public:
376 : pbes_expression(core::detail::default_values::PBESOr)
377 {}
378
381 explicit or_(const atermpp::aterm& term)
382 : pbes_expression(term)
383 {
384 assert(core::detail::check_term_PBESOr(*this));
385 }
386
388 or_(const pbes_expression& left, const pbes_expression& right)
389 : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESOr(), left, right))
390 {}
391
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 const pbes_expression& left() const
399 {
400 return atermpp::down_cast<pbes_expression>((*this)[0]);
401 }
402
403 const pbes_expression& right() const
404 {
405 return atermpp::down_cast<pbes_expression>((*this)[1]);
406 }
407};
408
411template <class... ARGUMENTS>
412inline void make_or_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
413{
415}
416
420inline
422{
424}
425
426// prototype declaration
427std::string pp(const or_& x);
428
433inline
434std::ostream& operator<<(std::ostream& out, const or_& x)
435{
436 return out << pbes_system::pp(x);
437}
438
440inline void swap(or_& t1, or_& t2)
441{
442 t1.swap(t2);
443}
444
445
447class imp: public pbes_expression
448{
449 public:
452 : pbes_expression(core::detail::default_values::PBESImp)
453 {}
454
457 explicit imp(const atermpp::aterm& term)
458 : pbes_expression(term)
459 {
460 assert(core::detail::check_term_PBESImp(*this));
461 }
462
464 imp(const pbes_expression& left, const pbes_expression& right)
465 : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESImp(), left, right))
466 {}
467
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 const pbes_expression& left() const
475 {
476 return atermpp::down_cast<pbes_expression>((*this)[0]);
477 }
478
479 const pbes_expression& right() const
480 {
481 return atermpp::down_cast<pbes_expression>((*this)[1]);
482 }
483};
484
487template <class... ARGUMENTS>
488inline void make_imp(atermpp::aterm_appl& t, const ARGUMENTS&... args)
489{
491}
492
496inline
498{
500}
501
502// prototype declaration
503std::string pp(const imp& x);
504
509inline
510std::ostream& operator<<(std::ostream& out, const imp& x)
511{
512 return out << pbes_system::pp(x);
513}
514
516inline void swap(imp& t1, imp& t2)
517{
518 t1.swap(t2);
519}
520
521
524{
525 public:
528 : pbes_expression(core::detail::default_values::PBESForall)
529 {}
530
533 explicit forall(const atermpp::aterm& term)
534 : pbes_expression(term)
535 {
536 assert(core::detail::check_term_PBESForall(*this));
537 }
538
540 forall(const data::variable_list& variables, const pbes_expression& body)
541 : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESForall(), variables, body))
542 {}
543
545 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 const data::variable_list& variables() const
551 {
552 return atermpp::down_cast<data::variable_list>((*this)[0]);
553 }
554
555 const pbes_expression& body() const
556 {
557 return atermpp::down_cast<pbes_expression>((*this)[1]);
558 }
559};
560
563template <class... ARGUMENTS>
564inline void make_forall(atermpp::aterm_appl& t, const ARGUMENTS&... args)
565{
567}
568
572inline
574{
576}
577
578// prototype declaration
579std::string pp(const forall& x);
580
585inline
586std::ostream& operator<<(std::ostream& out, const forall& x)
587{
588 return out << pbes_system::pp(x);
589}
590
592inline void swap(forall& t1, forall& t2)
593{
594 t1.swap(t2);
595}
596
597
600{
601 public:
604 : pbes_expression(core::detail::default_values::PBESExists)
605 {}
606
609 explicit exists(const atermpp::aterm& term)
610 : pbes_expression(term)
611 {
612 assert(core::detail::check_term_PBESExists(*this));
613 }
614
616 exists(const data::variable_list& variables, const pbes_expression& body)
617 : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESExists(), variables, body))
618 {}
619
621 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 const data::variable_list& variables() const
627 {
628 return atermpp::down_cast<data::variable_list>((*this)[0]);
629 }
630
631 const pbes_expression& body() const
632 {
633 return atermpp::down_cast<pbes_expression>((*this)[1]);
634 }
635};
636
639template <class... ARGUMENTS>
640inline void make_exists(atermpp::aterm_appl& t, const ARGUMENTS&... args)
641{
643}
644
648inline
650{
652}
653
654// prototype declaration
655std::string pp(const exists& x);
656
661inline
662std::ostream& operator<<(std::ostream& out, const exists& x)
663{
664 return out << pbes_system::pp(x);
665}
666
668inline void swap(exists& t1, exists& t2)
669{
670 t1.swap(t2);
671}
672//--- end generated classes ---//
673
674// template function overloads
675std::string pp(const pbes_expression_list& x);
676std::string pp(const pbes_expression_vector& x);
679std::set<pbes_system::propositional_variable_instantiation> find_propositional_variable_instantiations(const pbes_system::pbes_expression& x);
680std::set<core::identifier_string> find_identifiers(const pbes_system::pbes_expression& x);
681std::set<data::variable> find_free_variables(const pbes_system::pbes_expression& x);
685
687inline
689{
690 /* The dynamic cast is required, to prevent copying the data term true to
691 a local term on the stack. */
692 return reinterpret_cast<const pbes_expression&>(data::sort_bool::true_());
693}
694
696inline
698{
699 /* The dynamic cast is required, to prevent copying the data term false to
700 a local term on the stack. */
701 return reinterpret_cast<const pbes_expression&>(data::sort_bool::false_());
702}
703
707inline bool is_true(const pbes_expression& t)
708{
710}
711
715inline bool is_false(const pbes_expression& t)
716{
718}
719
723inline bool is_pbes_not(const pbes_expression& t)
724{
725 return pbes_system::is_not(t);
726}
727
731inline bool is_pbes_and(const pbes_expression& t)
732{
733 return pbes_system::is_and(t);
734}
735
739inline bool is_pbes_or(const pbes_expression& t)
740{
741 return pbes_system::is_or(t);
742}
743
747inline bool is_pbes_imp(const pbes_expression& t)
748{
749 return pbes_system::is_imp(t);
750}
751
755inline bool is_pbes_forall(const pbes_expression& t)
756{
757 return pbes_system::is_forall(t);
758}
759
763inline bool is_pbes_exists(const pbes_expression& t)
764{
765 return pbes_system::is_exists(t);
766}
767
772{
774}
775
780{
782}
783
787inline bool is_universal_or(const pbes_expression& t)
788{
790}
791
795inline bool is_data(const pbes_expression& t)
796{
797 return data::is_data_expression(t);
798}
799
801namespace accessors
802{
803
807inline
809{
810 if (is_pbes_not(t))
811 {
812 return atermpp::down_cast<const pbes_expression>(t[0]);
813 }
814 else
815 {
816 assert(is_forall(t) || is_exists(t));
817 return atermpp::down_cast<const pbes_expression>(t[1]);
818 }
819}
820
824inline
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
842inline
843const pbes_expression& left(const pbes_expression& t)
844{
845 assert(is_and(t) || is_or(t) || is_imp(t));
846 return atermpp::down_cast<pbes_expression>(t[0]);
847}
848
852inline
854{
855 if (data::is_data_expression(x))
856 {
857 return data::binary_left(atermpp::down_cast<data::application>(x));
858 }
859 else
860 {
861 return left(x);
862 }
863}
864
868inline
869const pbes_expression& right(const pbes_expression& t)
870{
871 return atermpp::down_cast<pbes_expression>(t[1]);
872}
873
877inline
879{
880 if (data::is_data_expression(x))
881 {
882 return data::binary_right(atermpp::down_cast<data::application>(x));
883 }
884 else
885 {
886 return right(x);
887 }
888}
889
893inline
895{
896 assert(is_forall(t) || is_exists(t));
897 return atermpp::down_cast<data::variable_list>(t[0]);
898}
899
903inline
905{
907 return atermpp::down_cast<core::identifier_string>(t[0]);
908}
909
913inline
915{
917 return atermpp::down_cast<data::data_expression_list>(t[1]);
918}
919} // namespace accessors
920
926inline
928{
929 if (l.empty())
930 {
931 return p;
932 }
934}
935
941inline
943{
944 if (l.empty())
945 {
946 return p;
947 }
949}
950
954inline
956{
957 data::optimized_not(result, p);
958}
959
964inline
966{
967 data::optimized_and(result, p, q);
968}
969
974inline
976{
977 data::optimized_or(result, p, q);
978}
979
984inline
986{
987 data::optimized_imp(result, p, q);
988}
989
995inline
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
1023inline
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
1046inline
1048{
1049 return find_free_variables(x).empty();
1050}
1051
1052inline
1054{
1055 assert(is_exists(x) || is_forall(x));
1056 if (is_exists(x))
1057 {
1058 return atermpp::down_cast<exists>(x).variables();
1059 }
1060 else
1061 {
1062 return atermpp::down_cast<forall>(x).variables();
1063 }
1064}
1065
1066inline
1068{
1069 std::set<data::variable> v = find_free_variables(x);
1070 return data::variable_list(v.begin(), v.end());
1071}
1072
1073} // namespace pbes_system
1074
1075} // namespace mcrl2
1076
1077namespace mcrl2
1078{
1079
1080namespace core
1081{
1082
1084template <>
1085struct term_traits<pbes_system::pbes_expression>
1086{
1089
1092
1095
1098
1101
1104
1107
1110
1113 static inline
1115 {
1116 return pbes_system::true_();
1117 }
1118
1121 static inline
1123 {
1124 return pbes_system::false_();
1125 }
1126
1130 static inline
1132 {
1133 return pbes_system::not_(p);
1134 }
1135
1139 static inline
1140 void make_not_(term_type& result, const term_type& p)
1141 {
1142 pbes_system::make_not_(result, p);
1143 }
1144
1149 static inline
1150 term_type and_(const term_type& p, const term_type& q)
1151 {
1152 return pbes_system::and_(p, q);
1153 }
1154
1159 static inline
1160 void make_and_(term_type& result, const term_type& p, const term_type& q)
1161 {
1162 pbes_system::make_and_(result, p, q);
1163 }
1164
1169 static inline
1170 term_type or_(const term_type& p, const term_type& q)
1171 {
1172 return pbes_system::or_(p, q);
1173 }
1174
1179 static inline
1180 void make_or_(term_type& result, const term_type& p, const term_type& q)
1181 {
1182 pbes_system::make_or_(result, p,q);
1183 }
1184
1185 template <typename FwdIt>
1186 static inline
1187 term_type join_or(FwdIt first, FwdIt last)
1188 {
1189 return utilities::detail::join(first, last, or_, false_());
1190 }
1191
1192 template <typename FwdIt>
1193 static inline
1194 term_type join_and(FwdIt first, FwdIt last)
1195 {
1196 return utilities::detail::join(first, last, and_, true_());
1197 }
1198
1203 static inline
1204 term_type imp(const term_type& p, const term_type& q)
1205 {
1206 return pbes_system::imp(p, q);
1207 }
1208
1213 static inline
1214 void make_imp(term_type& result, const term_type& p, const term_type& q)
1215 {
1216 pbes_system::make_imp(result, p, q);
1217 }
1218
1223 static inline
1225 {
1226 if (l.empty())
1227 {
1228 return p;
1229 }
1230 return pbes_system::forall(l, p);
1231 }
1232
1237 static inline
1238 void make_forall(term_type& result, const variable_sequence_type& l, const term_type& p)
1239 {
1240 if (l.empty())
1241 {
1242 result = p;
1243 return;
1244 }
1245 pbes_system::make_forall(result, l, p);
1246 }
1247
1252 static inline
1254 {
1255 if (l.empty())
1256 {
1257 return p;
1258 }
1259 return pbes_system::exists(l, p);
1260 }
1261
1266 static inline
1267 void make_exists(term_type& result, const variable_sequence_type& l, const term_type& p)
1268 {
1269 if (l.empty())
1270 {
1271 result = p;
1272 return;
1273 }
1274 pbes_system::make_exists(result, l, p);
1275 }
1276
1280 static inline
1281 bool is_true(const term_type& t)
1282 {
1284 }
1285
1289 static inline
1290 bool is_false(const term_type& t)
1291 {
1293 }
1294
1298 static inline
1299 bool is_not(const term_type& t)
1300 {
1301 return pbes_system::is_not(t);
1302 }
1303
1307 static inline
1308 bool is_and(const term_type& t)
1309 {
1310 return pbes_system::is_and(t);
1311 }
1312
1316 static inline
1317 bool is_or(const term_type& t)
1318 {
1319 return pbes_system::is_or(t);
1320 }
1321
1325 static inline
1326 bool is_imp(const term_type& t)
1327 {
1328 return pbes_system::is_imp(t);
1329 }
1330
1334 static inline
1335 bool is_forall(const term_type& t)
1336 {
1337 return pbes_system::is_forall(t);
1338 }
1339
1343 static inline
1344 bool is_exists(const term_type& t)
1345 {
1346 return pbes_system::is_exists(t);
1347 }
1348
1352 static inline
1353 bool is_data(const term_type& t)
1354 {
1355 return data::is_data_expression(t);
1356 }
1357
1361 static inline
1362 bool is_prop_var(const term_type& t)
1363 {
1365 }
1366
1370 static inline
1372 {
1374 }
1375
1379 static inline
1381 {
1383 }
1384
1387 static inline
1388 const term_type& not_arg(const term_type& t)
1389 {
1390 assert(is_pbes_not(t));
1391 return atermpp::down_cast<term_type>(t[0]);
1392 }
1393
1397 static inline
1399 {
1400 // Forall and exists are not fully supported by the data library
1403 assert(is_exists(t) || is_forall(t));
1404
1405 return atermpp::down_cast<variable_sequence_type>(t[0]);
1406 }
1407
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
1421 static inline
1423 {
1424 assert(is_prop_var(t));
1425 return atermpp::down_cast<data_term_sequence_type>(t[1]);
1426 }
1427
1431 static inline
1433 {
1434 return atermpp::down_cast<term_type>(v);
1435 }
1436
1440 static inline
1441 bool is_variable(const term_type& t)
1442 {
1443 return data::is_variable(t);
1444 }
1445
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
1460namespace std
1461{
1462
1463 template <>
1464 struct hash<mcrl2::pbes_system::pbes_expression>
1465 {
1467 {
1468 return hash<atermpp::aterm>()(x);
1469 }
1470 };
1471
1472 template <>
1473 struct hash<mcrl2::pbes_system::propositional_variable_instantiation>
1474 {
1476 {
1477 return hash<atermpp::aterm>()(x);
1478 }
1479 };
1480
1481} // namespace std
1482
1483#endif // MCRL2_PBES_PBES_EXPRESSION_H
Term containing a string.
The aterm base class that provides protection of the underlying shared terms.
Definition aterm.h:186
const function_symbol & function() const
Returns the function symbol belonging to an aterm_appl.
Definition aterm_appl.h:174
A list of aterm objects.
Definition aterm_list.h:23
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:267
void swap(unprotected_aterm &t) noexcept
Swaps this term with its argument.
Definition aterm.h:156
An abstraction expression.
Definition abstraction.h:26
\brief A data variable
Definition variable.h:28
\brief The and operator for pbes expressions
and_(const pbes_expression &left, const pbes_expression &right)
\brief Constructor.
and_(const and_ &) noexcept=default
Move semantics.
and_(and_ &&) noexcept=default
and_(const atermpp::aterm &term)
const pbes_expression & right() const
and_()
\brief Default constructor.
\brief The existential quantification operator for pbes expressions
exists(const atermpp::aterm &term)
exists(exists &&) noexcept=default
exists(const data::variable_list &variables, const pbes_expression &body)
\brief Constructor.
exists()
\brief Default constructor.
exists(const exists &) noexcept=default
Move semantics.
const pbes_expression & body() const
\brief The universal quantification operator for pbes expressions
forall()
\brief Default constructor.
const pbes_expression & body() const
forall(const data::variable_list &variables, const pbes_expression &body)
\brief Constructor.
forall(const atermpp::aterm &term)
forall(const forall &) noexcept=default
Move semantics.
forall(forall &&) noexcept=default
\brief The implication operator for pbes expressions
imp(const imp &) noexcept=default
Move semantics.
imp(imp &&) noexcept=default
imp(const atermpp::aterm &term)
imp()
\brief Default constructor.
imp(const pbes_expression &left, const pbes_expression &right)
\brief Constructor.
const pbes_expression & right() const
\brief The not operator for pbes expressions
not_()
\brief Default constructor.
not_(const pbes_expression &operand)
\brief Constructor.
not_(const not_ &) noexcept=default
Move semantics.
not_(not_ &&) noexcept=default
not_(const atermpp::aterm &term)
\brief The or operator for pbes expressions
or_(const or_ &) noexcept=default
Move semantics.
or_(const pbes_expression &left, const pbes_expression &right)
\brief Constructor.
const pbes_expression & right() const
or_(or_ &&) noexcept=default
or_(const atermpp::aterm &term)
or_()
\brief Default constructor.
pbes_expression(const atermpp::aterm &term)
pbes_expression(const pbes_expression &) noexcept=default
Move semantics.
pbes_expression(const data::data_expression &x)
\brief Constructor.
pbes_expression(const data::untyped_data_parameter &x)
\brief Constructor.
pbes_expression(const data::variable &x)
\brief Constructor.
pbes_expression()
\brief Default constructor.
pbes_expression(pbes_expression &&) noexcept=default
\brief A propositional variable instantiation
const data::data_expression_list & parameters() const
propositional_variable_instantiation(const propositional_variable_instantiation &) noexcept=default
Move semantics.
propositional_variable_instantiation(const std::string &name)
Constructor.
propositional_variable_instantiation(propositional_variable_instantiation &&) noexcept=default
propositional_variable_instantiation(const core::identifier_string &name, const data::data_expression_list &parameters)
Constructor.
propositional_variable_instantiation(const core::identifier_string &name)
Constructor.
propositional_variable_instantiation(const std::string &name, const data::data_expression_list &parameters)
Constructor.
propositional_variable_instantiation(const atermpp::aterm &term)
Constructor.
\brief A propositional variable declaration
Contains term traits for data_expression.
The main namespace for the aterm++ library.
Definition algorithm.h:21
void make_term_appl(Term &target, const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
Constructor an aterm_appl in a variable based on a function symbol and an forward iterator providing ...
Definition aterm_appl.h:239
const atermpp::function_symbol & function_symbol_PBESExists()
const atermpp::function_symbol & function_symbol_PBESNot()
const atermpp::function_symbol & function_symbol_PBESAnd()
const atermpp::function_symbol & function_symbol_PBESOr()
const atermpp::function_symbol & function_symbol_PBESImp()
const atermpp::function_symbol & function_symbol_PBESForall()
bool check_rule_PBExpr(const Term &t)
const atermpp::function_symbol & function_symbol_PropVarInst()
bool is_or_application(const atermpp::aterm_appl &e)
Recogniser for application of ||.
Definition bool.h:345
bool is_not_application(const atermpp::aterm_appl &e)
Recogniser for application of !.
Definition bool.h:217
bool is_false_function_symbol(const atermpp::aterm_appl &e)
Recogniser for function false.
Definition bool.h:119
bool is_and_application(const atermpp::aterm_appl &e)
Recogniser for application of &&.
Definition bool.h:281
bool is_true_function_symbol(const atermpp::aterm_appl &e)
Recogniser for function true.
Definition bool.h:87
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
bool is_exists(const atermpp::aterm_appl &x)
Returns true if the term t is an existential quantification.
void optimized_or(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
bool is_data_expression(const atermpp::aterm_appl &x)
Test for a data_expression expression.
void optimized_imp(Term &result, const Term &p, const Term &q)
Make an implication.
bool is_forall(const atermpp::aterm_appl &x)
Returns true if the term t is a universal quantification.
atermpp::term_list< variable > variable_list
\brief list of variables
void optimized_not(Term &result, const Term &arg)
Make a negation.
void optimized_and(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
bool is_untyped_data_parameter(const atermpp::aterm_appl &x)
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
pbes_expression data_left(const pbes_expression &x)
Returns the left hand side of an expression of type and, or or imp.
pbes_expression data_arg(const pbes_expression &t)
Returns the pbes expression argument of expressions of type not, exists and forall.
const pbes_expression & left(const pbes_expression &t)
Returns the left hand side of an expression of type and, or or imp.
const pbes_expression & right(const pbes_expression &t)
Returns the right hand side of an expression of type and, or or imp.
pbes_expression data_right(const pbes_expression &x)
Returns the left hand side of an expression of type and, or or imp.
const data::data_expression_list & param(const pbes_expression &t)
Returns the parameters of a propositional variable instantiation.
const core::identifier_string & name(const pbes_expression &t)
Returns the name of a propositional variable expression.
const data::variable_list & var(const pbes_expression &t)
Returns the variables of a quantification expression.
bool is_pbes_exists(const pbes_expression &t)
Returns true if the term t is an existential quantification.
atermpp::term_list< pbes_expression > pbes_expression_list
\brief list of pbes_expressions
bool is_universal_or(const pbes_expression &t)
Test for a disjunction.
bool is_data(const pbes_expression &t)
Returns true if the term t is a data expression.
bool is_forall(const atermpp::aterm_appl &x)
bool is_or(const atermpp::aterm_appl &x)
bool is_pbes_expression(const atermpp::aterm_appl &x)
void normalize_sorts(T &x, const data::sort_specification &sortspec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
bool is_universal_and(const pbes_expression &t)
Test for a conjunction.
bool is_pbes_not(const pbes_expression &t)
Returns true if the term t is a not expression.
const pbes_expression & true_()
bool is_pbes_forall(const pbes_expression &t)
Returns true if the term t is a universal quantification.
pbes_expression make_exists_(const data::variable_list &l, const pbes_expression &p)
Make an existential quantification. It checks for an empty variable list, which is not allowed.
bool is_propositional_variable_instantiation(const atermpp::aterm_appl &x)
void optimized_not(pbes_expression &result, const pbes_expression &p)
Make a negation.
void make_or_(atermpp::aterm_appl &t, const ARGUMENTS &... args)
std::vector< propositional_variable_instantiation > propositional_variable_instantiation_vector
\brief vector of propositional_variable_instantiations
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:131
void make_exists(atermpp::aterm_appl &t, const ARGUMENTS &... args)
data::variable_list free_variables(const pbes_expression &x)
bool is_constant(const pbes_expression &x)
void find_free_variables(const T &x, OutputIterator o)
Definition find.h:87
atermpp::term_list< propositional_variable_instantiation > propositional_variable_instantiation_list
\brief list of propositional_variable_instantiations
void make_propositional_variable_instantiation(atermpp::aterm_appl &t, const ARGUMENTS &... args)
const data::variable_list & quantifier_variables(const pbes_expression &x)
void optimized_exists(pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
Make an existential quantification If l is empty, p is returned.
std::ostream & operator<<(std::ostream &os, const absinthe_strategy strategy)
bool is_imp(const atermpp::aterm_appl &x)
bool is_not(const atermpp::aterm_appl &x)
bool is_universal_not(const pbes_expression &t)
Test for a conjunction.
void make_imp(atermpp::aterm_appl &t, const ARGUMENTS &... args)
bool search_variable(const T &x, const data::variable &v)
Returns true if the term has a given variable as subterm.
Definition find.h:217
std::vector< pbes_expression > pbes_expression_vector
\brief vector of pbes_expressions
bool is_pbes_or(const pbes_expression &t)
Returns true if the term t is an or expression.
bool is_false(const pbes_expression &t)
Test for the value false.
void optimized_forall(pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
Make a universal quantification If l is empty, p is returned.
bool is_pbes_imp(const pbes_expression &t)
Returns true if the term t is an imp expression.
void optimized_or(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a disjunction.
bool is_pbes_and(const pbes_expression &t)
Returns true if the term t is an and expression.
void make_and_(atermpp::aterm_appl &t, const ARGUMENTS &... args)
pbes_expression make_forall_(const data::variable_list &l, const pbes_expression &p)
Make a universal quantification. It checks for an empty variable list, which is not allowed.
void make_forall(atermpp::aterm_appl &t, const ARGUMENTS &... args)
bool is_exists(const atermpp::aterm_appl &x)
void swap(fixpoint_symbol &t1, fixpoint_symbol &t2)
\brief swap overload
std::string pp(const fixpoint_symbol &x)
Definition pbes.cpp:37
void make_not_(atermpp::aterm_appl &t, const ARGUMENTS &... args)
void optimized_and(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a conjunction.
void translate_user_notation(pbes_system::pbes &x)
Definition pbes.cpp:50
void find_propositional_variable_instantiations(Container const &container, OutputIterator o)
Returns all data variables that occur in a range of expressions.
Definition find.h:196
void optimized_imp(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make an implication.
bool is_true(const pbes_expression &t)
Test for the value true.
const pbes_expression & false_()
bool is_and(const atermpp::aterm_appl &x)
T join(FwdIt first, FwdIt last, BinaryOperation op, T empty_sequence_result)
Given a sequence [t1, t2, ..., tn] of elements of type T, returns op(t1, op(t2, .....
Definition join.h:55
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
add your file description here.
The classes propositional_variable and propositional_variable_instantiation.
static const atermpp::function_symbol PBESForall
static const atermpp::function_symbol PBESNot
static const atermpp::function_symbol PBESImp
static const atermpp::function_symbol PBESAnd
static const atermpp::function_symbol PropVarInst
static const atermpp::function_symbol PBESExists
static const atermpp::function_symbol PBESOr
static bool is_false(const term_type &t)
Test for the value false.
static void make_or_(term_type &result, const term_type &p, const term_type &q)
Make a disjunction.
static bool is_imp(const term_type &t)
Test for an implication.
static void make_exists(term_type &result, const variable_sequence_type &l, const term_type &p)
Make an existential quantification.
static bool is_data(const term_type &t)
Test for data term.
static term_type forall(const variable_sequence_type &l, const term_type &p)
Make a universal quantification.
static std::string pp(const term_type &t)
Pretty print function.
static term_type exists(const variable_sequence_type &l, const term_type &p)
Make an existential quantification.
static term_type or_(const term_type &p, const term_type &q)
Make a disjunction.
static const data_term_sequence_type & param(const term_type &t)
Returns the parameter list of a propositional variable instantiation.
static bool is_not(const term_type &t)
Test for a negation.
static void make_imp(term_type &result, const term_type &p, const term_type &q)
Make an implication.
static term_type join_and(FwdIt first, FwdIt last)
pbes_system::propositional_variable propositional_variable_decl_type
The propositional variable declaration type.
static bool is_and(const term_type &t)
Test for a conjunction.
static bool is_variable(const term_type &t)
Test if a term is a variable.
pbes_system::pbes_expression term_type
The term type.
static term_type not_(const term_type &p)
Make a negation.
static bool is_exists(const term_type &t)
Test for an existential quantification.
pbes_system::propositional_variable_instantiation propositional_variable_type
The propositional variable instantiation type.
static void make_and_(term_type &result, const term_type &p, const term_type &q)
Make a conjunction.
static term_type left(const term_type &t)
Returns the left argument of a term of type and, or or imp.
static const string_type & name(const term_type &t)
Returns the name of a propositional variable instantiation.
static term_type right(const term_type &t)
Returns the right argument of a term of type and, or or imp.
data::data_expression data_term_type
The data term type.
core::identifier_string string_type
The string type.
static term_type and_(const term_type &p, const term_type &q)
Make a conjunction.
static const variable_sequence_type & var(const term_type &t)
Returns the quantifier variables of a quantifier expression.
static const term_type & variable2term(const variable_type &v)
Conversion from variable to term.
static void make_forall(term_type &result, const variable_sequence_type &l, const term_type &p)
Make a universal quantification.
static void make_not_(term_type &result, const term_type &p)
Make a negation.
static const term_type & not_arg(const term_type &t)
Returns the argument of a term of type not.
data::variable_list variable_sequence_type
The variable sequence type.
static term_type imp(const term_type &p, const term_type &q)
Make an implication.
data::data_expression_list data_term_sequence_type
The data term sequence type.
static term_type join_or(FwdIt first, FwdIt last)
static bool is_forall(const term_type &t)
Test for an universal quantification.
static bool is_prop_var(const term_type &t)
Test for propositional variable instantiation.
static bool is_true(const term_type &t)
Test for the value true.
static bool is_or(const term_type &t)
Test for a disjunction.
Contains type information for terms.
Definition term_traits.h:24
std::size_t operator()(const mcrl2::pbes_system::pbes_expression &x) const
std::size_t operator()(const mcrl2::pbes_system::propositional_variable_instantiation &x) const
#define hash(l, r, m)
Definition tree_set.cpp:23