cprover
Loading...
Searching...
No Matches
std_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_STD_EXPR_H
11#define CPROVER_UTIL_STD_EXPR_H
12
15
16#include "expr_cast.h"
17#include "invariant.h"
18#include "std_types.h"
19
22{
23public:
25 : expr_protectedt(_id, std::move(_type))
26 {
27 }
28
30 operandst &operands() = delete;
31 const operandst &operands() const = delete;
32
33 const exprt &op0() const = delete;
34 exprt &op0() = delete;
35 const exprt &op1() const = delete;
36 exprt &op1() = delete;
37 const exprt &op2() const = delete;
38 exprt &op2() = delete;
39 const exprt &op3() const = delete;
40 exprt &op3() = delete;
41
42 void copy_to_operands(const exprt &expr) = delete;
43 void copy_to_operands(const exprt &, const exprt &) = delete;
44 void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
45};
46
49{
50public:
51 // constructor
53 const irep_idt &_id,
54 exprt _op0,
55 exprt _op1,
56 exprt _op2,
57 typet _type)
59 _id,
60 std::move(_type),
61 {std::move(_op0), std::move(_op1), std::move(_op2)})
62 {
63 }
64
65 // make op0 to op2 public
66 using exprt::op0;
67 using exprt::op1;
68 using exprt::op2;
69
70 const exprt &op3() const = delete;
71 exprt &op3() = delete;
72
73 static void check(
74 const exprt &expr,
76 {
78 vm,
79 expr.operands().size() == 3,
80 "ternary expression must have three operands");
81 }
82
83 static void validate(
84 const exprt &expr,
85 const namespacet &,
87 {
88 check(expr, vm);
89 }
90};
91
98inline const ternary_exprt &to_ternary_expr(const exprt &expr)
99{
101 return static_cast<const ternary_exprt &>(expr);
102}
103
106{
108 return static_cast<ternary_exprt &>(expr);
109}
110
113{
114public:
117 {
118 }
119
122 symbol_exprt(const irep_idt &identifier, typet type)
124 {
125 set_identifier(identifier);
126 }
127
133 {
134 return symbol_exprt(id, typet());
135 }
136
137 void set_identifier(const irep_idt &identifier)
138 {
139 set(ID_identifier, identifier);
140 }
141
143 {
144 return get(ID_identifier);
145 }
146};
147
148// NOLINTNEXTLINE(readability/namespace)
149namespace std
150{
151template <>
152// NOLINTNEXTLINE(readability/identifiers)
153struct hash<::symbol_exprt>
154{
155 size_t operator()(const ::symbol_exprt &sym)
156 {
157 return irep_id_hash()(sym.get_identifier());
158 }
159};
160} // namespace std
161
165{
166public:
170 : symbol_exprt(identifier, std::move(type))
171 {
172 }
173
175 {
177 }
178
180 {
181 return set(ID_C_static_lifetime, true);
182 }
183
188
189 bool is_thread_local() const
190 {
192 }
193
195 {
196 return set(ID_C_thread_local, true);
197 }
198
203};
204
205template <>
206inline bool can_cast_expr<symbol_exprt>(const exprt &base)
207{
208 return base.id() == ID_symbol;
209}
210
211inline void validate_expr(const symbol_exprt &value)
212{
213 validate_operands(value, 0, "Symbols must not have operands");
214}
215
222inline const symbol_exprt &to_symbol_expr(const exprt &expr)
223{
224 PRECONDITION(expr.id()==ID_symbol);
225 const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
227 return ret;
228}
229
232{
233 PRECONDITION(expr.id()==ID_symbol);
234 symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
236 return ret;
237}
238
239
242{
243public:
248 {
249 set_identifier(identifier);
250 }
251
256 irep_idt identifier,
257 typet type,
258 source_locationt location)
260 {
261 set_identifier(std::move(identifier));
262 add_source_location() = std::move(location);
263 }
264
265 void set_identifier(const irep_idt &identifier)
266 {
267 set(ID_identifier, identifier);
268 }
269
271 {
272 return get(ID_identifier);
273 }
274};
275
276template <>
278{
279 return base.id() == ID_nondet_symbol;
280}
281
282inline void validate_expr(const nondet_symbol_exprt &value)
283{
284 validate_operands(value, 0, "Symbols must not have operands");
285}
286
294{
296 const nondet_symbol_exprt &ret =
297 static_cast<const nondet_symbol_exprt &>(expr);
299 return ret;
300}
301
304{
305 PRECONDITION(expr.id()==ID_symbol);
306 nondet_symbol_exprt &ret = static_cast<nondet_symbol_exprt &>(expr);
308 return ret;
309}
310
311
314{
315public:
318 {
319 }
320
322 : expr_protectedt(_id, std::move(_type), {std::move(_op)})
323 {
324 }
325
326 const exprt &op() const
327 {
328 return op0();
329 }
330
332 {
333 return op0();
334 }
335
336 const exprt &op1() const = delete;
337 exprt &op1() = delete;
338 const exprt &op2() const = delete;
339 exprt &op2() = delete;
340 const exprt &op3() const = delete;
341 exprt &op3() = delete;
342};
343
344template <>
345inline bool can_cast_expr<unary_exprt>(const exprt &base)
346{
347 return base.operands().size() == 1;
348}
349
350inline void validate_expr(const unary_exprt &value)
351{
352 validate_operands(value, 1, "Unary expressions must have one operand");
353}
354
361inline const unary_exprt &to_unary_expr(const exprt &expr)
362{
363 const unary_exprt &ret = static_cast<const unary_exprt &>(expr);
365 return ret;
366}
367
370{
371 unary_exprt &ret = static_cast<unary_exprt &>(expr);
373 return ret;
374}
375
376
379{
380public:
382 {
383 }
384};
385
386template <>
387inline bool can_cast_expr<abs_exprt>(const exprt &base)
388{
389 return base.id() == ID_abs;
390}
391
392inline void validate_expr(const abs_exprt &value)
393{
394 validate_operands(value, 1, "Absolute value must have one operand");
395}
396
403inline const abs_exprt &to_abs_expr(const exprt &expr)
404{
405 PRECONDITION(expr.id()==ID_abs);
406 const abs_exprt &ret = static_cast<const abs_exprt &>(expr);
408 return ret;
409}
410
413{
414 PRECONDITION(expr.id()==ID_abs);
415 abs_exprt &ret = static_cast<abs_exprt &>(expr);
417 return ret;
418}
419
420
423{
424public:
426 : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
427 {
428 }
429
432 {
433 }
434};
435
436template <>
438{
439 return base.id() == ID_unary_minus;
440}
441
442inline void validate_expr(const unary_minus_exprt &value)
443{
444 validate_operands(value, 1, "Unary minus must have one operand");
445}
446
454{
456 const unary_minus_exprt &ret = static_cast<const unary_minus_exprt &>(expr);
458 return ret;
459}
460
463{
465 unary_minus_exprt &ret = static_cast<unary_minus_exprt &>(expr);
467 return ret;
468}
469
472{
473public:
476 {
477 }
478};
479
480template <>
482{
483 return base.id() == ID_unary_plus;
484}
485
486inline void validate_expr(const unary_plus_exprt &value)
487{
488 validate_operands(value, 1, "unary plus must have one operand");
489}
490
497inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
498{
499 PRECONDITION(expr.id() == ID_unary_plus);
500 const unary_plus_exprt &ret = static_cast<const unary_plus_exprt &>(expr);
502 return ret;
503}
504
507{
508 PRECONDITION(expr.id() == ID_unary_plus);
509 unary_plus_exprt &ret = static_cast<unary_plus_exprt &>(expr);
511 return ret;
512}
513
517{
518public:
519 explicit predicate_exprt(const irep_idt &_id)
521 {
522 }
523};
524
528{
529public:
531 : unary_exprt(_id, std::move(_op), bool_typet())
532 {
533 }
534};
535
539{
540public:
543 {
544 }
545};
546
547template <>
548inline bool can_cast_expr<sign_exprt>(const exprt &base)
549{
550 return base.id() == ID_sign;
551}
552
553inline void validate_expr(const sign_exprt &expr)
554{
555 validate_operands(expr, 1, "sign expression must have one operand");
556}
557
564inline const sign_exprt &to_sign_expr(const exprt &expr)
565{
566 PRECONDITION(expr.id() == ID_sign);
567 const sign_exprt &ret = static_cast<const sign_exprt &>(expr);
569 return ret;
570}
571
574{
575 PRECONDITION(expr.id() == ID_sign);
576 sign_exprt &ret = static_cast<sign_exprt &>(expr);
578 return ret;
579}
580
583{
584public:
586 : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
587 {
588 }
589
591 : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
592 {
593 }
594
595 static void check(
596 const exprt &expr,
598 {
600 vm,
601 expr.operands().size() == 2,
602 "binary expression must have two operands");
603 }
604
605 static void validate(
606 const exprt &expr,
607 const namespacet &,
609 {
610 check(expr, vm);
611 }
612
614 {
615 return exprt::op0();
616 }
617
618 const exprt &lhs() const
619 {
620 return exprt::op0();
621 }
622
624 {
625 return exprt::op1();
626 }
627
628 const exprt &rhs() const
629 {
630 return exprt::op1();
631 }
632
633 // make op0 and op1 public
634 using exprt::op0;
635 using exprt::op1;
636
637 const exprt &op2() const = delete;
638 exprt &op2() = delete;
639 const exprt &op3() const = delete;
640 exprt &op3() = delete;
641};
642
643template <>
644inline bool can_cast_expr<binary_exprt>(const exprt &base)
645{
646 return base.operands().size() == 2;
647}
648
649inline void validate_expr(const binary_exprt &value)
650{
651 binary_exprt::check(value);
652}
653
660inline const binary_exprt &to_binary_expr(const exprt &expr)
661{
663 return static_cast<const binary_exprt &>(expr);
664}
665
668{
670 return static_cast<binary_exprt &>(expr);
671}
672
676{
677public:
679 : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
680 {
681 }
682
683 static void check(
684 const exprt &expr,
686 {
687 binary_exprt::check(expr, vm);
688 }
689
690 static void validate(
691 const exprt &expr,
692 const namespacet &ns,
694 {
695 binary_exprt::validate(expr, ns, vm);
696
698 vm,
699 expr.is_boolean(),
700 "result of binary predicate expression should be of type bool");
701 }
702};
703
707{
708public:
713
714 static void check(
715 const exprt &expr,
717 {
719 }
720
721 static void validate(
722 const exprt &expr,
723 const namespacet &ns,
725 {
727
728 // we now can safely assume that 'expr' is a binary predicate
729 const auto &expr_binary = static_cast<const binary_predicate_exprt &>(expr);
730
731 // check that the types of the operands are the same
733 vm,
734 expr_binary.op0().type() == expr_binary.op1().type(),
735 "lhs and rhs of binary relation expression should have same type");
736 }
737};
738
739template <>
741{
742 return can_cast_expr<binary_exprt>(base);
743}
744
745inline void validate_expr(const binary_relation_exprt &value)
746{
748}
749
752{
753public:
758};
759
760template <>
762{
763 return base.id() == ID_gt;
764}
765
766inline void validate_expr(const greater_than_exprt &value)
767{
769}
770
780
781template <>
783{
784 return base.id() == ID_ge;
785}
786
788{
790}
791
794{
795public:
800};
801
802template <>
803inline bool can_cast_expr<less_than_exprt>(const exprt &base)
804{
805 return base.id() == ID_lt;
806}
807
808inline void validate_expr(const less_than_exprt &value)
809{
811}
812
822
823template <>
825{
826 return base.id() == ID_le;
827}
828
830{
832}
833
841{
843 return static_cast<const binary_relation_exprt &>(expr);
844}
845
848{
850 return static_cast<binary_relation_exprt &>(expr);
851}
852
853
857{
858public:
860 : expr_protectedt(_id, std::move(_type))
861 {
862 operands() = std::move(_operands);
863 }
864
866 : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
867 {
868 }
869
871 : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
872 {
873 }
874
875 // In contrast to exprt::opX, the methods
876 // below check the size.
878 {
879 PRECONDITION(operands().size() >= 1);
880 return operands().front();
881 }
882
884 {
885 PRECONDITION(operands().size() >= 2);
886 return operands()[1];
887 }
888
890 {
891 PRECONDITION(operands().size() >= 3);
892 return operands()[2];
893 }
894
896 {
897 PRECONDITION(operands().size() >= 4);
898 return operands()[3];
899 }
900
901 const exprt &op0() const
902 {
903 PRECONDITION(operands().size() >= 1);
904 return operands().front();
905 }
906
907 const exprt &op1() const
908 {
909 PRECONDITION(operands().size() >= 2);
910 return operands()[1];
911 }
912
913 const exprt &op2() const
914 {
915 PRECONDITION(operands().size() >= 3);
916 return operands()[2];
917 }
918
919 const exprt &op3() const
920 {
921 PRECONDITION(operands().size() >= 4);
922 return operands()[3];
923 }
924};
925
932inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
933{
934 return static_cast<const multi_ary_exprt &>(expr);
935}
936
939{
940 return static_cast<multi_ary_exprt &>(expr);
941}
942
943
947{
948public:
950 : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
951 {
952 }
953
956 std::move(_lhs),
957 ID_plus,
958 std::move(_rhs),
959 std::move(_type))
960 {
961 }
962
964 : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
965 {
966 }
967};
968
969template <>
970inline bool can_cast_expr<plus_exprt>(const exprt &base)
971{
972 return base.id() == ID_plus;
973}
974
975inline void validate_expr(const plus_exprt &value)
976{
977 validate_operands(value, 2, "Plus must have two or more operands", true);
978}
979
986inline const plus_exprt &to_plus_expr(const exprt &expr)
987{
988 PRECONDITION(expr.id()==ID_plus);
989 const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
991 return ret;
992}
993
996{
997 PRECONDITION(expr.id()==ID_plus);
998 plus_exprt &ret = static_cast<plus_exprt &>(expr);
1000 return ret;
1001}
1002
1003
1006{
1007public:
1009 : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
1010 {
1011 }
1012};
1013
1014template <>
1015inline bool can_cast_expr<minus_exprt>(const exprt &base)
1016{
1017 return base.id() == ID_minus;
1018}
1019
1020inline void validate_expr(const minus_exprt &value)
1021{
1022 validate_operands(value, 2, "Minus must have two or more operands", true);
1023}
1024
1031inline const minus_exprt &to_minus_expr(const exprt &expr)
1032{
1033 PRECONDITION(expr.id()==ID_minus);
1034 const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
1036 return ret;
1037}
1038
1041{
1042 PRECONDITION(expr.id()==ID_minus);
1043 minus_exprt &ret = static_cast<minus_exprt &>(expr);
1045 return ret;
1046}
1047
1048
1052{
1053public:
1055 : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
1056 {
1057 }
1058};
1059
1060template <>
1061inline bool can_cast_expr<mult_exprt>(const exprt &base)
1062{
1063 return base.id() == ID_mult;
1064}
1065
1066inline void validate_expr(const mult_exprt &value)
1067{
1068 validate_operands(value, 2, "Multiply must have two or more operands", true);
1069}
1070
1077inline const mult_exprt &to_mult_expr(const exprt &expr)
1078{
1079 PRECONDITION(expr.id()==ID_mult);
1080 const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1082 return ret;
1083}
1084
1087{
1088 PRECONDITION(expr.id()==ID_mult);
1089 mult_exprt &ret = static_cast<mult_exprt &>(expr);
1091 return ret;
1092}
1093
1094
1097{
1098public:
1100 : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1101 {
1102 }
1103
1106 {
1107 return op0();
1108 }
1109
1111 const exprt &dividend() const
1112 {
1113 return op0();
1114 }
1115
1118 {
1119 return op1();
1120 }
1121
1123 const exprt &divisor() const
1124 {
1125 return op1();
1126 }
1127};
1128
1129template <>
1130inline bool can_cast_expr<div_exprt>(const exprt &base)
1131{
1132 return base.id() == ID_div;
1133}
1134
1135inline void validate_expr(const div_exprt &value)
1136{
1137 validate_operands(value, 2, "Divide must have two operands");
1138}
1139
1146inline const div_exprt &to_div_expr(const exprt &expr)
1147{
1148 PRECONDITION(expr.id()==ID_div);
1149 const div_exprt &ret = static_cast<const div_exprt &>(expr);
1151 return ret;
1152}
1153
1156{
1157 PRECONDITION(expr.id()==ID_div);
1158 div_exprt &ret = static_cast<div_exprt &>(expr);
1160 return ret;
1161}
1162
1168{
1169public:
1171 : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1172 {
1173 }
1174
1177 {
1178 return op0();
1179 }
1180
1182 const exprt &dividend() const
1183 {
1184 return op0();
1185 }
1186
1189 {
1190 return op1();
1191 }
1192
1194 const exprt &divisor() const
1195 {
1196 return op1();
1197 }
1198};
1199
1200template <>
1201inline bool can_cast_expr<mod_exprt>(const exprt &base)
1202{
1203 return base.id() == ID_mod;
1204}
1205
1206inline void validate_expr(const mod_exprt &value)
1207{
1208 validate_operands(value, 2, "Modulo must have two operands");
1209}
1210
1217inline const mod_exprt &to_mod_expr(const exprt &expr)
1218{
1219 PRECONDITION(expr.id()==ID_mod);
1220 const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1222 return ret;
1223}
1224
1227{
1228 PRECONDITION(expr.id()==ID_mod);
1229 mod_exprt &ret = static_cast<mod_exprt &>(expr);
1231 return ret;
1232}
1233
1236{
1237public:
1242
1245 {
1246 return op0();
1247 }
1248
1250 const exprt &dividend() const
1251 {
1252 return op0();
1253 }
1254
1257 {
1258 return op1();
1259 }
1260
1262 const exprt &divisor() const
1263 {
1264 return op1();
1265 }
1266};
1267
1268template <>
1270{
1271 return base.id() == ID_euclidean_mod;
1272}
1273
1274inline void validate_expr(const euclidean_mod_exprt &value)
1275{
1276 validate_operands(value, 2, "Modulo must have two operands");
1277}
1278
1286{
1287 PRECONDITION(expr.id() == ID_euclidean_mod);
1288 const euclidean_mod_exprt &ret =
1289 static_cast<const euclidean_mod_exprt &>(expr);
1291 return ret;
1292}
1293
1296{
1297 PRECONDITION(expr.id() == ID_euclidean_mod);
1298 euclidean_mod_exprt &ret = static_cast<euclidean_mod_exprt &>(expr);
1300 return ret;
1301}
1302
1303
1306{
1307public:
1309 : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1310 {
1311 PRECONDITION(lhs().type() == rhs().type());
1312 }
1313
1314 static void check(
1315 const exprt &expr,
1317 {
1319 }
1320
1321 static void validate(
1322 const exprt &expr,
1323 const namespacet &ns,
1325 {
1326 binary_relation_exprt::validate(expr, ns, vm);
1327 }
1328};
1329
1330template <>
1331inline bool can_cast_expr<equal_exprt>(const exprt &base)
1332{
1333 return base.id() == ID_equal;
1334}
1335
1336inline void validate_expr(const equal_exprt &value)
1337{
1338 equal_exprt::check(value);
1339}
1340
1347inline const equal_exprt &to_equal_expr(const exprt &expr)
1348{
1349 PRECONDITION(expr.id()==ID_equal);
1350 equal_exprt::check(expr);
1351 return static_cast<const equal_exprt &>(expr);
1352}
1353
1356{
1357 PRECONDITION(expr.id()==ID_equal);
1358 equal_exprt::check(expr);
1359 return static_cast<equal_exprt &>(expr);
1360}
1361
1362
1365{
1366public:
1371};
1372
1373template <>
1374inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1375{
1376 return base.id() == ID_notequal;
1377}
1378
1379inline void validate_expr(const notequal_exprt &value)
1380{
1381 validate_operands(value, 2, "Inequality must have two operands");
1382}
1383
1390inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1391{
1392 PRECONDITION(expr.id()==ID_notequal);
1393 const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1395 return ret;
1396}
1397
1400{
1401 PRECONDITION(expr.id()==ID_notequal);
1402 notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1404 return ret;
1405}
1406
1407
1410{
1411public:
1412 // _array must have either index or vector type.
1413 // When _array has array_type, the type of _index
1414 // must be array_type.index_type().
1415 // This will eventually be enforced using a precondition.
1417 : binary_exprt(
1418 _array,
1419 ID_index,
1420 std::move(_index),
1421 to_type_with_subtype(_array.type()).subtype())
1422 {
1423 const auto &array_op_type = _array.type();
1425 array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1426 }
1427
1429 : binary_exprt(
1430 std::move(_array),
1431 ID_index,
1432 std::move(_index),
1433 std::move(_type))
1434 {
1435 const auto &array_op_type = array().type();
1437 array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1438 }
1439
1441 {
1442 return op0();
1443 }
1444
1445 const exprt &array() const
1446 {
1447 return op0();
1448 }
1449
1451 {
1452 return op1();
1453 }
1454
1455 const exprt &index() const
1456 {
1457 return op1();
1458 }
1459};
1460
1461template <>
1462inline bool can_cast_expr<index_exprt>(const exprt &base)
1463{
1464 return base.id() == ID_index;
1465}
1466
1467inline void validate_expr(const index_exprt &value)
1468{
1469 validate_operands(value, 2, "Array index must have two operands");
1470}
1471
1478inline const index_exprt &to_index_expr(const exprt &expr)
1479{
1480 PRECONDITION(expr.id()==ID_index);
1481 const index_exprt &ret = static_cast<const index_exprt &>(expr);
1483 return ret;
1484}
1485
1488{
1489 PRECONDITION(expr.id()==ID_index);
1490 index_exprt &ret = static_cast<index_exprt &>(expr);
1492 return ret;
1493}
1494
1495
1498{
1499public:
1501 : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1502 {
1503 }
1504
1505 const array_typet &type() const
1506 {
1507 return static_cast<const array_typet &>(unary_exprt::type());
1508 }
1509
1511 {
1512 return static_cast<array_typet &>(unary_exprt::type());
1513 }
1514
1516 {
1517 return op0();
1518 }
1519
1520 const exprt &what() const
1521 {
1522 return op0();
1523 }
1524};
1525
1526template <>
1527inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1528{
1529 return base.id() == ID_array_of;
1530}
1531
1532inline void validate_expr(const array_of_exprt &value)
1533{
1534 validate_operands(value, 1, "'Array of' must have one operand");
1535}
1536
1543inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1544{
1545 PRECONDITION(expr.id()==ID_array_of);
1546 const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1548 return ret;
1549}
1550
1553{
1554 PRECONDITION(expr.id()==ID_array_of);
1555 array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1557 return ret;
1558}
1559
1560
1563{
1564public:
1566 : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1567 {
1568 }
1569
1570 const array_typet &type() const
1571 {
1572 return static_cast<const array_typet &>(multi_ary_exprt::type());
1573 }
1574
1576 {
1577 return static_cast<array_typet &>(multi_ary_exprt::type());
1578 }
1579
1581 {
1582 return exprt::with_source_location<array_exprt>(other);
1583 }
1584
1586 {
1587 return std::move(*this).exprt::with_source_location<array_exprt>(other);
1588 }
1589};
1590
1591template <>
1592inline bool can_cast_expr<array_exprt>(const exprt &base)
1593{
1594 return base.id() == ID_array;
1595}
1596
1603inline const array_exprt &to_array_expr(const exprt &expr)
1604{
1605 PRECONDITION(expr.id()==ID_array);
1606 return static_cast<const array_exprt &>(expr);
1607}
1608
1611{
1612 PRECONDITION(expr.id()==ID_array);
1613 return static_cast<array_exprt &>(expr);
1614}
1615
1619{
1620public:
1622 : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1623 {
1624 }
1625
1626 const array_typet &type() const
1627 {
1628 return static_cast<const array_typet &>(multi_ary_exprt::type());
1629 }
1630
1632 {
1633 return static_cast<array_typet &>(multi_ary_exprt::type());
1634 }
1635
1637 void add(exprt index, exprt value)
1638 {
1639 add_to_operands(std::move(index), std::move(value));
1640 }
1641};
1642
1643template <>
1645{
1646 return base.id() == ID_array_list;
1647}
1648
1649inline void validate_expr(const array_list_exprt &value)
1650{
1651 PRECONDITION(value.operands().size() % 2 == 0);
1652}
1653
1655{
1657 auto &ret = static_cast<const array_list_exprt &>(expr);
1659 return ret;
1660}
1661
1663{
1665 auto &ret = static_cast<array_list_exprt &>(expr);
1667 return ret;
1668}
1669
1672{
1673public:
1675 : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1676 {
1677 }
1678};
1679
1680template <>
1681inline bool can_cast_expr<vector_exprt>(const exprt &base)
1682{
1683 return base.id() == ID_vector;
1684}
1685
1692inline const vector_exprt &to_vector_expr(const exprt &expr)
1693{
1694 PRECONDITION(expr.id()==ID_vector);
1695 return static_cast<const vector_exprt &>(expr);
1696}
1697
1700{
1701 PRECONDITION(expr.id()==ID_vector);
1702 return static_cast<vector_exprt &>(expr);
1703}
1704
1705
1708{
1709public:
1711 : unary_exprt(ID_union, std::move(_value), std::move(_type))
1712 {
1714 }
1715
1717 {
1718 return get(ID_component_name);
1719 }
1720
1721 void set_component_name(const irep_idt &component_name)
1722 {
1723 set(ID_component_name, component_name);
1724 }
1725
1726 std::size_t get_component_number() const
1727 {
1729 }
1730
1731 void set_component_number(std::size_t component_number)
1732 {
1733 set_size_t(ID_component_number, component_number);
1734 }
1735};
1736
1737template <>
1738inline bool can_cast_expr<union_exprt>(const exprt &base)
1739{
1740 return base.id() == ID_union;
1741}
1742
1743inline void validate_expr(const union_exprt &value)
1744{
1745 validate_operands(value, 1, "Union constructor must have one operand");
1746}
1747
1754inline const union_exprt &to_union_expr(const exprt &expr)
1755{
1756 PRECONDITION(expr.id()==ID_union);
1757 const union_exprt &ret = static_cast<const union_exprt &>(expr);
1759 return ret;
1760}
1761
1764{
1765 PRECONDITION(expr.id()==ID_union);
1766 union_exprt &ret = static_cast<union_exprt &>(expr);
1768 return ret;
1769}
1770
1774{
1775public:
1776 explicit empty_union_exprt(typet _type)
1777 : nullary_exprt(ID_empty_union, std::move(_type))
1778 {
1779 }
1780};
1781
1782template <>
1784{
1785 return base.id() == ID_empty_union;
1786}
1787
1788inline void validate_expr(const empty_union_exprt &value)
1789{
1791 value, 0, "Empty-union constructor must not have any operand");
1792}
1793
1801{
1802 PRECONDITION(expr.id() == ID_empty_union);
1803 const empty_union_exprt &ret = static_cast<const empty_union_exprt &>(expr);
1805 return ret;
1806}
1807
1810{
1811 PRECONDITION(expr.id() == ID_empty_union);
1812 empty_union_exprt &ret = static_cast<empty_union_exprt &>(expr);
1814 return ret;
1815}
1816
1819{
1820public:
1822 : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1823 {
1824 }
1825
1826 exprt &component(const irep_idt &name, const namespacet &ns);
1827 const exprt &component(const irep_idt &name, const namespacet &ns) const;
1828};
1829
1830template <>
1831inline bool can_cast_expr<struct_exprt>(const exprt &base)
1832{
1833 return base.id() == ID_struct;
1834}
1835
1842inline const struct_exprt &to_struct_expr(const exprt &expr)
1843{
1844 PRECONDITION(expr.id()==ID_struct);
1845 return static_cast<const struct_exprt &>(expr);
1846}
1847
1850{
1851 PRECONDITION(expr.id()==ID_struct);
1852 return static_cast<struct_exprt &>(expr);
1853}
1854
1855
1858{
1859public:
1861 : binary_exprt(
1862 std::move(_real),
1863 ID_complex,
1864 std::move(_imag),
1865 std::move(_type))
1866 {
1867 }
1868
1870 {
1871 return op0();
1872 }
1873
1874 const exprt &real() const
1875 {
1876 return op0();
1877 }
1878
1880 {
1881 return op1();
1882 }
1883
1884 const exprt &imag() const
1885 {
1886 return op1();
1887 }
1888};
1889
1890template <>
1891inline bool can_cast_expr<complex_exprt>(const exprt &base)
1892{
1893 return base.id() == ID_complex;
1894}
1895
1896inline void validate_expr(const complex_exprt &value)
1897{
1898 validate_operands(value, 2, "Complex constructor must have two operands");
1899}
1900
1907inline const complex_exprt &to_complex_expr(const exprt &expr)
1908{
1909 PRECONDITION(expr.id()==ID_complex);
1910 const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1912 return ret;
1913}
1914
1917{
1918 PRECONDITION(expr.id()==ID_complex);
1919 complex_exprt &ret = static_cast<complex_exprt &>(expr);
1921 return ret;
1922}
1923
1926{
1927public:
1928 explicit complex_real_exprt(const exprt &op)
1930 {
1931 }
1932};
1933
1934template <>
1936{
1937 return base.id() == ID_complex_real;
1938}
1939
1940inline void validate_expr(const complex_real_exprt &expr)
1941{
1943 expr, 1, "real part retrieval operation must have one operand");
1944}
1945
1953{
1954 PRECONDITION(expr.id() == ID_complex_real);
1955 const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
1957 return ret;
1958}
1959
1962{
1963 PRECONDITION(expr.id() == ID_complex_real);
1964 complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
1966 return ret;
1967}
1968
1971{
1972public:
1973 explicit complex_imag_exprt(const exprt &op)
1975 {
1976 }
1977};
1978
1979template <>
1981{
1982 return base.id() == ID_complex_imag;
1983}
1984
1985inline void validate_expr(const complex_imag_exprt &expr)
1986{
1988 expr, 1, "imaginary part retrieval operation must have one operand");
1989}
1990
1998{
1999 PRECONDITION(expr.id() == ID_complex_imag);
2000 const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
2002 return ret;
2003}
2004
2007{
2008 PRECONDITION(expr.id() == ID_complex_imag);
2009 complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
2011 return ret;
2012}
2013
2014
2017{
2018public:
2020 : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2021 {
2022 }
2023
2024 // returns a typecast if the type doesn't already match
2025 static exprt conditional_cast(const exprt &expr, const typet &type)
2026 {
2027 if(expr.type() == type)
2028 return expr;
2029 else
2030 return typecast_exprt(expr, type);
2031 }
2032};
2033
2034template <>
2035inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2036{
2037 return base.id() == ID_typecast;
2038}
2039
2040inline void validate_expr(const typecast_exprt &value)
2041{
2042 validate_operands(value, 1, "Typecast must have one operand");
2043}
2044
2051inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2052{
2053 PRECONDITION(expr.id()==ID_typecast);
2054 const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
2056 return ret;
2057}
2058
2061{
2062 PRECONDITION(expr.id()==ID_typecast);
2063 typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
2065 return ret;
2066}
2067
2068
2071{
2072public:
2074 : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2075 {
2076 }
2077
2080 ID_and,
2081 {std::move(op0), std::move(op1), std::move(op2)},
2082 bool_typet())
2083 {
2084 }
2085
2088 ID_and,
2089 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2090 bool_typet())
2091 {
2092 }
2093
2098};
2099
2103
2105
2106template <>
2107inline bool can_cast_expr<and_exprt>(const exprt &base)
2108{
2109 return base.id() == ID_and;
2110}
2111
2118inline const and_exprt &to_and_expr(const exprt &expr)
2119{
2120 PRECONDITION(expr.id()==ID_and);
2121 return static_cast<const and_exprt &>(expr);
2122}
2123
2126{
2127 PRECONDITION(expr.id()==ID_and);
2128 return static_cast<and_exprt &>(expr);
2129}
2130
2131
2134{
2135public:
2137 : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2138 {
2139 }
2140};
2141
2142template <>
2143inline bool can_cast_expr<implies_exprt>(const exprt &base)
2144{
2145 return base.id() == ID_implies;
2146}
2147
2148inline void validate_expr(const implies_exprt &value)
2149{
2150 validate_operands(value, 2, "Implies must have two operands");
2151}
2152
2159inline const implies_exprt &to_implies_expr(const exprt &expr)
2160{
2161 PRECONDITION(expr.id()==ID_implies);
2162 const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2164 return ret;
2165}
2166
2169{
2170 PRECONDITION(expr.id()==ID_implies);
2171 implies_exprt &ret = static_cast<implies_exprt &>(expr);
2173 return ret;
2174}
2175
2176
2179{
2180public:
2182 : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2183 {
2184 }
2185
2188 ID_or,
2189 {std::move(op0), std::move(op1), std::move(op2)},
2190 bool_typet())
2191 {
2192 }
2193
2196 ID_or,
2197 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2198 bool_typet())
2199 {
2200 }
2201
2206};
2207
2211
2213
2214template <>
2215inline bool can_cast_expr<or_exprt>(const exprt &base)
2216{
2217 return base.id() == ID_or;
2218}
2219
2226inline const or_exprt &to_or_expr(const exprt &expr)
2227{
2228 PRECONDITION(expr.id()==ID_or);
2229 return static_cast<const or_exprt &>(expr);
2230}
2231
2234{
2235 PRECONDITION(expr.id()==ID_or);
2236 return static_cast<or_exprt &>(expr);
2237}
2238
2239
2242{
2243public:
2245 : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2246 {
2247 }
2248};
2249
2250template <>
2251inline bool can_cast_expr<xor_exprt>(const exprt &base)
2252{
2253 return base.id() == ID_xor;
2254}
2255
2262inline const xor_exprt &to_xor_expr(const exprt &expr)
2263{
2264 PRECONDITION(expr.id()==ID_xor);
2265 return static_cast<const xor_exprt &>(expr);
2266}
2267
2270{
2271 PRECONDITION(expr.id()==ID_xor);
2272 return static_cast<xor_exprt &>(expr);
2273}
2274
2275
2278{
2279public:
2281 {
2282 PRECONDITION(as_const(*this).op().is_boolean());
2283 }
2284};
2285
2286template <>
2287inline bool can_cast_expr<not_exprt>(const exprt &base)
2288{
2289 return base.id() == ID_not;
2290}
2291
2292inline void validate_expr(const not_exprt &value)
2293{
2294 validate_operands(value, 1, "Not must have one operand");
2295}
2296
2303inline const not_exprt &to_not_expr(const exprt &expr)
2304{
2305 PRECONDITION(expr.id()==ID_not);
2306 const not_exprt &ret = static_cast<const not_exprt &>(expr);
2308 return ret;
2309}
2310
2313{
2314 PRECONDITION(expr.id()==ID_not);
2315 not_exprt &ret = static_cast<not_exprt &>(expr);
2317 return ret;
2318}
2319
2320
2323{
2324public:
2326 : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2327 {
2328 }
2329
2331 : ternary_exprt(
2332 ID_if,
2333 std::move(cond),
2334 std::move(t),
2335 std::move(f),
2336 std::move(type))
2337 {
2338 }
2339
2341 {
2342 return op0();
2343 }
2344
2345 const exprt &cond() const
2346 {
2347 return op0();
2348 }
2349
2351 {
2352 return op1();
2353 }
2354
2355 const exprt &true_case() const
2356 {
2357 return op1();
2358 }
2359
2361 {
2362 return op2();
2363 }
2364
2365 const exprt &false_case() const
2366 {
2367 return op2();
2368 }
2369
2370 static void check(
2371 const exprt &expr,
2373 {
2374 ternary_exprt::check(expr, vm);
2375 }
2376
2377 static void validate(
2378 const exprt &expr,
2379 const namespacet &ns,
2381 {
2382 ternary_exprt::validate(expr, ns, vm);
2383 }
2384};
2385
2386template <>
2387inline bool can_cast_expr<if_exprt>(const exprt &base)
2388{
2389 return base.id() == ID_if;
2390}
2391
2392inline void validate_expr(const if_exprt &value)
2393{
2394 validate_operands(value, 3, "If-then-else must have three operands");
2395}
2396
2403inline const if_exprt &to_if_expr(const exprt &expr)
2404{
2405 PRECONDITION(expr.id()==ID_if);
2406 const if_exprt &ret = static_cast<const if_exprt &>(expr);
2408 return ret;
2409}
2410
2413{
2414 PRECONDITION(expr.id()==ID_if);
2415 if_exprt &ret = static_cast<if_exprt &>(expr);
2417 return ret;
2418}
2419
2424{
2425public:
2428 ID_with,
2429 _old.type(),
2430 {_old, std::move(_where), std::move(_new_value)})
2431 {
2432 }
2433
2435 {
2436 return op0();
2437 }
2438
2439 const exprt &old() const
2440 {
2441 return op0();
2442 }
2443
2445 {
2446 return op1();
2447 }
2448
2449 const exprt &where() const
2450 {
2451 return op1();
2452 }
2453
2455 {
2456 return op2();
2457 }
2458
2459 const exprt &new_value() const
2460 {
2461 return op2();
2462 }
2463};
2464
2465template <>
2466inline bool can_cast_expr<with_exprt>(const exprt &base)
2467{
2468 return base.id() == ID_with;
2469}
2470
2471inline void validate_expr(const with_exprt &value)
2472{
2474 value, 3, "array/structure update must have at least 3 operands", true);
2476 value.operands().size() % 2 == 1,
2477 "array/structure update must have an odd number of operands");
2478}
2479
2486inline const with_exprt &to_with_expr(const exprt &expr)
2487{
2488 PRECONDITION(expr.id()==ID_with);
2489 const with_exprt &ret = static_cast<const with_exprt &>(expr);
2491 return ret;
2492}
2493
2496{
2497 PRECONDITION(expr.id()==ID_with);
2498 with_exprt &ret = static_cast<with_exprt &>(expr);
2500 return ret;
2501}
2502
2504{
2505public:
2508 {
2509 }
2510
2511 const exprt &index() const
2512 {
2513 return op0();
2514 }
2515
2517 {
2518 return op0();
2519 }
2520};
2521
2522template <>
2524{
2525 return base.id() == ID_index_designator;
2526}
2527
2528inline void validate_expr(const index_designatort &value)
2529{
2530 validate_operands(value, 1, "Index designator must have one operand");
2531}
2532
2540{
2542 const index_designatort &ret = static_cast<const index_designatort &>(expr);
2544 return ret;
2545}
2546
2549{
2551 index_designatort &ret = static_cast<index_designatort &>(expr);
2553 return ret;
2554}
2555
2557{
2558public:
2564
2566 {
2567 return get(ID_component_name);
2568 }
2569};
2570
2571template <>
2573{
2574 return base.id() == ID_member_designator;
2575}
2576
2577inline void validate_expr(const member_designatort &value)
2578{
2579 validate_operands(value, 0, "Member designator must not have operands");
2580}
2581
2589{
2591 const member_designatort &ret = static_cast<const member_designatort &>(expr);
2593 return ret;
2594}
2595
2598{
2600 member_designatort &ret = static_cast<member_designatort &>(expr);
2602 return ret;
2603}
2604
2605
2608{
2609public:
2611 : ternary_exprt(
2612 ID_update,
2613 _old,
2614 std::move(_designator),
2615 std::move(_new_value),
2616 _old.type())
2617 {
2618 }
2619
2621 {
2622 return op0();
2623 }
2624
2625 const exprt &old() const
2626 {
2627 return op0();
2628 }
2629
2630 // the designator operands are either
2631 // 1) member_designator or
2632 // 2) index_designator
2633 // as defined above
2635 {
2636 return op1().operands();
2637 }
2638
2640 {
2641 return op1().operands();
2642 }
2643
2645 {
2646 return op2();
2647 }
2648
2649 const exprt &new_value() const
2650 {
2651 return op2();
2652 }
2653
2654 static void check(
2655 const exprt &expr,
2657 {
2658 ternary_exprt::check(expr, vm);
2659 }
2660
2661 static void validate(
2662 const exprt &expr,
2663 const namespacet &ns,
2665 {
2666 ternary_exprt::validate(expr, ns, vm);
2667 }
2668};
2669
2670template <>
2671inline bool can_cast_expr<update_exprt>(const exprt &base)
2672{
2673 return base.id() == ID_update;
2674}
2675
2676inline void validate_expr(const update_exprt &value)
2677{
2679 value, 3, "Array/structure update must have three operands");
2680}
2681
2688inline const update_exprt &to_update_expr(const exprt &expr)
2689{
2690 PRECONDITION(expr.id()==ID_update);
2691 const update_exprt &ret = static_cast<const update_exprt &>(expr);
2693 return ret;
2694}
2695
2698{
2699 PRECONDITION(expr.id()==ID_update);
2700 update_exprt &ret = static_cast<update_exprt &>(expr);
2702 return ret;
2703}
2704
2705
2706#if 0
2709{
2710public:
2712 const exprt &_array,
2713 const exprt &_index,
2714 const exprt &_new_value):
2716 {
2717 add_to_operands(_array, _index, _new_value);
2718 }
2719
2721 {
2722 operands().resize(3);
2723 }
2724
2725 exprt &array()
2726 {
2727 return op0();
2728 }
2729
2730 const exprt &array() const
2731 {
2732 return op0();
2733 }
2734
2735 exprt &index()
2736 {
2737 return op1();
2738 }
2739
2740 const exprt &index() const
2741 {
2742 return op1();
2743 }
2744
2745 exprt &new_value()
2746 {
2747 return op2();
2748 }
2749
2750 const exprt &new_value() const
2751 {
2752 return op2();
2753 }
2754};
2755
2756template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2757{
2758 return base.id()==ID_array_update;
2759}
2760
2761inline void validate_expr(const array_update_exprt &value)
2762{
2763 validate_operands(value, 3, "Array update must have three operands");
2764}
2765
2772inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2773{
2775 const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2777 return ret;
2778}
2779
2782{
2784 array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2786 return ret;
2787}
2788
2789#endif
2790
2791
2794{
2795public:
2796 member_exprt(exprt op, const irep_idt &component_name, typet _type)
2797 : unary_exprt(ID_member, std::move(op), std::move(_type))
2798 {
2799 const auto &compound_type_id = compound().type().id();
2803 set_component_name(component_name);
2804 }
2805
2815
2817 {
2818 return get(ID_component_name);
2819 }
2820
2821 void set_component_name(const irep_idt &component_name)
2822 {
2823 set(ID_component_name, component_name);
2824 }
2825
2826 std::size_t get_component_number() const
2827 {
2829 }
2830
2831 // will go away, use compound()
2832 const exprt &struct_op() const
2833 {
2834 return op0();
2835 }
2836
2837 // will go away, use compound()
2839 {
2840 return op0();
2841 }
2842
2843 const exprt &compound() const
2844 {
2845 return op0();
2846 }
2847
2849 {
2850 return op0();
2851 }
2852
2853 static void check(
2854 const exprt &expr,
2856 {
2857 DATA_CHECK(
2858 vm,
2859 expr.operands().size() == 1,
2860 "member expression must have one operand");
2861 }
2862
2863 static void validate(
2864 const exprt &expr,
2865 const namespacet &ns,
2867};
2868
2869template <>
2870inline bool can_cast_expr<member_exprt>(const exprt &base)
2871{
2872 return base.id() == ID_member;
2873}
2874
2875inline void validate_expr(const member_exprt &value)
2876{
2877 validate_operands(value, 1, "Extract member must have one operand");
2878}
2879
2886inline const member_exprt &to_member_expr(const exprt &expr)
2887{
2888 PRECONDITION(expr.id()==ID_member);
2889 const member_exprt &ret = static_cast<const member_exprt &>(expr);
2891 return ret;
2892}
2893
2896{
2897 PRECONDITION(expr.id()==ID_member);
2898 member_exprt &ret = static_cast<member_exprt &>(expr);
2900 return ret;
2901}
2902
2903
2906{
2907public:
2909 {
2910 }
2911};
2912
2913template <>
2914inline bool can_cast_expr<type_exprt>(const exprt &base)
2915{
2916 return base.id() == ID_type;
2917}
2918
2925inline const type_exprt &to_type_expr(const exprt &expr)
2926{
2928 const type_exprt &ret = static_cast<const type_exprt &>(expr);
2929 return ret;
2930}
2931
2934{
2936 type_exprt &ret = static_cast<type_exprt &>(expr);
2937 return ret;
2938}
2939
2942{
2943public:
2944 constant_exprt(const irep_idt &_value, typet _type)
2945 : nullary_exprt(ID_constant, std::move(_type))
2946 {
2947 set_value(_value);
2948 }
2949
2950 const irep_idt &get_value() const
2951 {
2952 return get(ID_value);
2953 }
2954
2955 void set_value(const irep_idt &value)
2956 {
2957 set(ID_value, value);
2958 }
2959
2960 bool value_is_zero_string() const;
2961
2962 static void check(
2963 const exprt &expr,
2965
2966 static void validate(
2967 const exprt &expr,
2968 const namespacet &,
2970 {
2971 check(expr, vm);
2972 }
2973};
2974
2975template <>
2976inline bool can_cast_expr<constant_exprt>(const exprt &base)
2977{
2978 return base.is_constant();
2979}
2980
2981inline void validate_expr(const constant_exprt &value)
2982{
2983 validate_operands(value, 0, "Constants must not have operands");
2984}
2985
2992inline const constant_exprt &to_constant_expr(const exprt &expr)
2993{
2994 PRECONDITION(expr.is_constant());
2995 return static_cast<const constant_exprt &>(expr);
2996}
2997
3000{
3001 PRECONDITION(expr.is_constant());
3002 return static_cast<constant_exprt &>(expr);
3003}
3004
3005
3008{
3009public:
3013};
3014
3017{
3018public:
3022};
3023
3026{
3027public:
3032};
3033
3034template <>
3035inline bool can_cast_expr<nil_exprt>(const exprt &base)
3036{
3037 return base.id() == ID_nil;
3038}
3039
3042{
3043public:
3044 explicit infinity_exprt(typet _type)
3045 : nullary_exprt(ID_infinity, std::move(_type))
3046 {
3047 }
3048};
3049
3052{
3053public:
3054 using variablest = std::vector<symbol_exprt>;
3055
3058 irep_idt _id,
3059 const variablest &_variables,
3060 exprt _where,
3061 typet _type)
3062 : binary_exprt(
3064 ID_tuple,
3066 typet(ID_tuple)),
3067 _id,
3068 std::move(_where),
3069 std::move(_type))
3070 {
3071 }
3072
3074 {
3075 return (variablest &)to_multi_ary_expr(op0()).operands();
3076 }
3077
3078 const variablest &variables() const
3079 {
3080 return (variablest &)to_multi_ary_expr(op0()).operands();
3081 }
3082
3084 {
3085 return op1();
3086 }
3087
3088 const exprt &where() const
3089 {
3090 return op1();
3091 }
3092
3095 exprt instantiate(const exprt::operandst &) const;
3096
3099 exprt instantiate(const variablest &) const;
3100};
3101
3102template <>
3103inline bool can_cast_expr<binding_exprt>(const exprt &base)
3104{
3105 return base.id() == ID_forall || base.id() == ID_exists ||
3106 base.id() == ID_lambda || base.id() == ID_array_comprehension;
3107}
3108
3110{
3112 binding_expr, 2, "Binding expressions must have two operands");
3113}
3114
3121inline const binding_exprt &to_binding_expr(const exprt &expr)
3122{
3124 expr.id() == ID_forall || expr.id() == ID_exists ||
3125 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3126 const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
3128 return ret;
3129}
3130
3138{
3140 expr.id() == ID_forall || expr.id() == ID_exists ||
3141 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3142 binding_exprt &ret = static_cast<binding_exprt &>(expr);
3144 return ret;
3145}
3146
3149{
3150public:
3154 const exprt &where)
3155 : binary_exprt(
3158 std::move(variables),
3159 where,
3160 where.type()),
3161 ID_let,
3163 where.type())
3164 {
3165 PRECONDITION(this->variables().size() == this->values().size());
3166 }
3167
3170 : let_exprt(
3172 operandst{std::move(value)},
3173 where)
3174 {
3175 }
3176
3178 {
3179 return static_cast<binding_exprt &>(op0());
3180 }
3181
3182 const binding_exprt &binding() const
3183 {
3184 return static_cast<const binding_exprt &>(op0());
3185 }
3186
3189 {
3190 auto &variables = binding().variables();
3191 PRECONDITION(variables.size() == 1);
3192 return variables.front();
3193 }
3194
3196 const symbol_exprt &symbol() const
3197 {
3198 const auto &variables = binding().variables();
3199 PRECONDITION(variables.size() == 1);
3200 return variables.front();
3201 }
3202
3205 {
3206 auto &values = this->values();
3207 PRECONDITION(values.size() == 1);
3208 return values.front();
3209 }
3210
3212 const exprt &value() const
3213 {
3214 const auto &values = this->values();
3215 PRECONDITION(values.size() == 1);
3216 return values.front();
3217 }
3218
3220 {
3221 return static_cast<multi_ary_exprt &>(op1()).operands();
3222 }
3223
3224 const operandst &values() const
3225 {
3226 return static_cast<const multi_ary_exprt &>(op1()).operands();
3227 }
3228
3231 {
3232 return binding().variables();
3233 }
3234
3237 {
3238 return binding().variables();
3239 }
3240
3243 {
3244 return binding().where();
3245 }
3246
3248 const exprt &where() const
3249 {
3250 return binding().where();
3251 }
3252
3253 static void validate(const exprt &, validation_modet);
3254};
3255
3256template <>
3257inline bool can_cast_expr<let_exprt>(const exprt &base)
3258{
3259 return base.id() == ID_let;
3260}
3261
3263{
3264 validate_operands(let_expr, 2, "Let must have two operands");
3265}
3266
3273inline const let_exprt &to_let_expr(const exprt &expr)
3274{
3275 PRECONDITION(expr.id()==ID_let);
3276 const let_exprt &ret = static_cast<const let_exprt &>(expr);
3278 return ret;
3279}
3280
3283{
3284 PRECONDITION(expr.id()==ID_let);
3285 let_exprt &ret = static_cast<let_exprt &>(expr);
3287 return ret;
3288}
3289
3290
3295{
3296public:
3298 : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3299 {
3300 }
3301
3305 void add_case(const exprt &condition, const exprt &value)
3306 {
3307 PRECONDITION(condition.is_boolean());
3308 operands().reserve(operands().size() + 2);
3309 operands().push_back(condition);
3310 operands().push_back(value);
3311 }
3312};
3313
3314template <>
3315inline bool can_cast_expr<cond_exprt>(const exprt &base)
3316{
3317 return base.id() == ID_cond;
3318}
3319
3320inline void validate_expr(const cond_exprt &value)
3321{
3323 value.operands().size() % 2 == 0, "cond must have even number of operands");
3324}
3325
3332inline const cond_exprt &to_cond_expr(const exprt &expr)
3333{
3334 PRECONDITION(expr.id() == ID_cond);
3335 const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3337 return ret;
3338}
3339
3342{
3343 PRECONDITION(expr.id() == ID_cond);
3344 cond_exprt &ret = static_cast<cond_exprt &>(expr);
3346 return ret;
3347}
3348
3358{
3359public:
3362 exprt body,
3363 array_typet _type)
3364 : binding_exprt(
3366 {std::move(arg)},
3367 std::move(body),
3368 std::move(_type))
3369 {
3370 }
3371
3372 const array_typet &type() const
3373 {
3374 return static_cast<const array_typet &>(binary_exprt::type());
3375 }
3376
3378 {
3379 return static_cast<array_typet &>(binary_exprt::type());
3380 }
3381
3382 const symbol_exprt &arg() const
3383 {
3384 auto &variables = this->variables();
3385 PRECONDITION(variables.size() == 1);
3386 return variables[0];
3387 }
3388
3390 {
3391 auto &variables = this->variables();
3392 PRECONDITION(variables.size() == 1);
3393 return variables[0];
3394 }
3395
3396 const exprt &body() const
3397 {
3398 return where();
3399 }
3400
3402 {
3403 return where();
3404 }
3405};
3406
3407template <>
3409{
3410 return base.id() == ID_array_comprehension;
3411}
3412
3414{
3415 validate_operands(value, 2, "'Array comprehension' must have two operands");
3416}
3417
3424inline const array_comprehension_exprt &
3426{
3429 static_cast<const array_comprehension_exprt &>(expr);
3431 return ret;
3432}
3433
3443
3444inline void validate_expr(const class class_method_descriptor_exprt &value);
3445
3448{
3449public:
3465 typet _type,
3469 : nullary_exprt(ID_virtual_function, std::move(_type))
3470 {
3473 set(ID_C_class, std::move(class_id));
3474 set(ID_C_base_name, std::move(base_method_name));
3475 set(ID_identifier, std::move(id));
3476 validate_expr(*this);
3477 }
3478
3486 {
3487 return get(ID_component_name);
3488 }
3489
3493 const irep_idt &class_id() const
3494 {
3495 return get(ID_C_class);
3496 }
3497
3501 {
3502 return get(ID_C_base_name);
3503 }
3504
3509 {
3510 return get(ID_identifier);
3511 }
3512};
3513
3514inline void validate_expr(const class class_method_descriptor_exprt &value)
3515{
3516 validate_operands(value, 0, "class method descriptor must not have operands");
3518 !value.mangled_method_name().empty(),
3519 "class method descriptor must have a mangled method name.");
3521 !value.class_id().empty(), "class method descriptor must have a class id.");
3523 !value.base_method_name().empty(),
3524 "class method descriptor must have a base method name.");
3526 value.get_identifier() == id2string(value.class_id()) + "." +
3528 "class method descriptor must have an identifier in the expected format.");
3529}
3530
3537inline const class_method_descriptor_exprt &
3539{
3542 static_cast<const class_method_descriptor_exprt &>(expr);
3544 return ret;
3545}
3546
3547template <>
3549{
3550 return base.id() == ID_virtual_function;
3551}
3552
3559{
3560public:
3562 : binary_exprt(
3563 std::move(symbol),
3565 value, // not moved, for type
3566 value.type())
3567 {
3568 PRECONDITION(symbol.type() == type());
3569 }
3570
3571 const symbol_exprt &symbol() const
3572 {
3573 return static_cast<const symbol_exprt &>(op0());
3574 }
3575
3577 {
3578 return static_cast<symbol_exprt &>(op0());
3579 }
3580
3581 const exprt &value() const
3582 {
3583 return op1();
3584 }
3585
3587 {
3588 return op1();
3589 }
3590};
3591
3592template <>
3594{
3595 return base.id() == ID_named_term;
3596}
3597
3598inline void validate_expr(const named_term_exprt &value)
3599{
3600 validate_operands(value, 2, "'named term' must have two operands");
3601}
3602
3610{
3611 PRECONDITION(expr.id() == ID_named_term);
3612 const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
3614 return ret;
3615}
3616
3619{
3620 PRECONDITION(expr.id() == ID_named_term);
3621 named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
3623 return ret;
3624}
3625
3626#endif // CPROVER_UTIL_STD_EXPR_H
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
Absolute value.
Definition std_expr.h:379
abs_exprt(exprt _op)
Definition std_expr.h:381
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
ait()
Definition ai.h:566
Boolean AND.
Definition std_expr.h:2071
and_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2078
and_exprt(exprt op0, exprt op1)
Definition std_expr.h:2073
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2086
and_exprt(exprt::operandst _operands)
Definition std_expr.h:2094
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3358
const array_typet & type() const
Definition std_expr.h:3372
const symbol_exprt & arg() const
Definition std_expr.h:3382
const exprt & body() const
Definition std_expr.h:3396
array_typet & type()
Definition std_expr.h:3377
symbol_exprt & arg()
Definition std_expr.h:3389
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition std_expr.h:3360
Array constructor from list of elements.
Definition std_expr.h:1563
array_exprt && with_source_location(const exprt &other) &&
Definition std_expr.h:1585
const array_typet & type() const
Definition std_expr.h:1570
array_exprt & with_source_location(const exprt &other) &
Definition std_expr.h:1580
array_exprt(operandst _operands, array_typet _type)
Definition std_expr.h:1565
array_typet & type()
Definition std_expr.h:1575
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition std_expr.h:1619
void add(exprt index, exprt value)
add an index/value pair
Definition std_expr.h:1637
const array_typet & type() const
Definition std_expr.h:1626
array_list_exprt(operandst _operands, array_typet _type)
Definition std_expr.h:1621
array_typet & type()
Definition std_expr.h:1631
Array constructor from single element.
Definition std_expr.h:1498
array_typet & type()
Definition std_expr.h:1510
array_of_exprt(exprt _what, array_typet _type)
Definition std_expr.h:1500
const exprt & what() const
Definition std_expr.h:1520
const array_typet & type() const
Definition std_expr.h:1505
exprt & what()
Definition std_expr.h:1515
Arrays with given size.
Definition std_types.h:763
A base class for binary expressions.
Definition std_expr.h:583
exprt & lhs()
Definition std_expr.h:613
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:585
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:605
const exprt & op2() const =delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:595
exprt & rhs()
Definition std_expr.h:623
exprt & op0()
Definition expr.h:125
const exprt & lhs() const
Definition std_expr.h:618
exprt & op1()
Definition expr.h:128
exprt & op3()=delete
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition std_expr.h:590
const exprt & rhs() const
Definition std_expr.h:628
exprt & op2()=delete
const exprt & op3() const =delete
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:676
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:683
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition std_expr.h:678
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:690
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:709
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:714
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:721
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:3052
const variablest & variables() const
Definition std_expr.h:3078
const exprt & where() const
Definition std_expr.h:3088
exprt & where()
Definition std_expr.h:3083
variablest & variables()
Definition std_expr.h:3073
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition std_expr.h:3057
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:169
std::vector< symbol_exprt > variablest
Definition std_expr.h:3054
The Boolean type.
Definition std_types.h:36
An expression describing a method on a class.
Definition std_expr.h:3448
const irep_idt & base_method_name() const
The name of the method to which this expression is applied as would be seen in the source code.
Definition std_expr.h:3500
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition std_expr.h:3485
const irep_idt & get_identifier() const
A unique identifier of the combination of class and method overload to which this expression refers.
Definition std_expr.h:3508
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition std_expr.h:3464
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
Definition std_expr.h:3493
Complex constructor from a pair of numbers.
Definition std_expr.h:1858
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition std_expr.h:1860
exprt real()
Definition std_expr.h:1869
exprt imag()
Definition std_expr.h:1879
const exprt & real() const
Definition std_expr.h:1874
const exprt & imag() const
Definition std_expr.h:1884
Imaginary part of the expression describing a complex number.
Definition std_expr.h:1971
complex_imag_exprt(const exprt &op)
Definition std_expr.h:1973
Real part of the expression describing a complex number.
Definition std_expr.h:1926
complex_real_exprt(const exprt &op)
Definition std_expr.h:1928
Complex numbers made of pair of given subtype.
Definition std_types.h:1077
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition std_expr.h:3295
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition std_expr.h:3305
cond_exprt(operandst _operands, typet _type)
Definition std_expr.h:3297
A constant literal expression.
Definition std_expr.h:2942
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2966
const irep_idt & get_value() const
Definition std_expr.h:2950
bool value_is_zero_string() const
Definition std_expr.cpp:18
constant_exprt(const irep_idt &_value, typet _type)
Definition std_expr.h:2944
void set_value(const irep_idt &value)
Definition std_expr.h:2955
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.cpp:24
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition std_expr.h:165
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:169
bool is_static_lifetime() const
Definition std_expr.h:174
bool is_thread_local() const
Definition std_expr.h:189
Division.
Definition std_expr.h:1097
div_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1099
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1105
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1111
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1123
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1117
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1774
empty_union_exprt(typet _type)
Definition std_expr.h:1776
Equality.
Definition std_expr.h:1306
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:1314
equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1308
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:1321
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1236
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1256
euclidean_mod_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1238
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1262
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1244
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1250
Base class for all expressions.
Definition expr.h:336
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
exprt & op2()
Definition expr.h:131
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:216
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
exprt & op2()
Definition expr.h:131
source_locationt & add_source_location()
Definition expr.h:228
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
The Boolean constant false.
Definition std_expr.h:3017
Binary greater than operator expression.
Definition std_expr.h:752
greater_than_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:754
Binary greater than or equal operator expression.
Definition std_expr.h:773
greater_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:775
The trinary if-then-else operator.
Definition std_expr.h:2323
const exprt & false_case() const
Definition std_expr.h:2365
exprt & cond()
Definition std_expr.h:2340
const exprt & cond() const
Definition std_expr.h:2345
if_exprt(exprt cond, const exprt &t, exprt f)
Definition std_expr.h:2325
const exprt & true_case() const
Definition std_expr.h:2355
exprt & false_case()
Definition std_expr.h:2360
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition std_expr.h:2330
exprt & true_case()
Definition std_expr.h:2350
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2370
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2377
Boolean implication.
Definition std_expr.h:2134
implies_exprt(exprt op0, exprt op1)
Definition std_expr.h:2136
const exprt & index() const
Definition std_expr.h:2511
index_designatort(exprt _index)
Definition std_expr.h:2506
exprt & index()
Definition std_expr.h:2516
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
index_exprt(exprt _array, exprt _index, typet _type)
Definition std_expr.h:1428
index_exprt(const exprt &_array, exprt _index)
Definition std_expr.h:1416
exprt & array()
Definition std_expr.h:1440
const exprt & index() const
Definition std_expr.h:1455
const exprt & array() const
Definition std_expr.h:1445
An expression denoting infinity.
Definition std_expr.h:3042
infinity_exprt(typet _type)
Definition std_expr.h:3044
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:67
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:95
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:86
const irep_idt & id() const
Definition irep.h:396
Binary less than operator expression.
Definition std_expr.h:794
less_than_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:796
Binary less than or equal operator expression.
Definition std_expr.h:815
less_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:817
A let expression.
Definition std_expr.h:3149
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3230
const binding_exprt & binding() const
Definition std_expr.h:3182
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition std_expr.h:3236
operandst & values()
Definition std_expr.h:3219
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition std_expr.h:3169
const exprt & where() const
convenience accessor for binding().where()
Definition std_expr.h:3248
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:143
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition std_expr.h:3196
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition std_expr.h:3151
exprt & value()
convenience accessor for the value of a single binding
Definition std_expr.h:3204
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3242
binding_exprt & binding()
Definition std_expr.h:3177
const operandst & values() const
Definition std_expr.h:3224
const exprt & value() const
convenience accessor for the value of a single binding
Definition std_expr.h:3212
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition std_expr.h:3188
irep_idt get_component_name() const
Definition std_expr.h:2565
member_designatort(const irep_idt &_component_name)
Definition std_expr.h:2559
Extract member of struct or union.
Definition std_expr.h:2794
const exprt & compound() const
Definition std_expr.h:2843
exprt & struct_op()
Definition std_expr.h:2838
const exprt & struct_op() const
Definition std_expr.h:2832
irep_idt get_component_name() const
Definition std_expr.h:2816
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:2821
exprt & compound()
Definition std_expr.h:2848
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
Definition std_expr.cpp:110
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2853
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition std_expr.h:2796
std::size_t get_component_number() const
Definition std_expr.h:2826
member_exprt(exprt op, const struct_typet::componentt &c)
Definition std_expr.h:2806
Binary minus.
Definition std_expr.h:1006
minus_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1008
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1168
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1176
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1182
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1188
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1194
mod_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1170
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
mult_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1054
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:857
exprt & op1()
Definition std_expr.h:883
const exprt & op0() const
Definition std_expr.h:901
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition std_expr.h:870
const exprt & op2() const
Definition std_expr.h:913
const exprt & op3() const
Definition std_expr.h:919
exprt & op0()
Definition std_expr.h:877
exprt & op2()
Definition std_expr.h:889
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:865
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition std_expr.h:859
const exprt & op1() const
Definition std_expr.h:907
exprt & op3()
Definition std_expr.h:895
Expression that introduces a new symbol that is equal to the operand.
Definition std_expr.h:3559
named_term_exprt(symbol_exprt symbol, exprt value)
Definition std_expr.h:3561
symbol_exprt & symbol()
Definition std_expr.h:3576
const exprt & value() const
Definition std_expr.h:3581
const symbol_exprt & symbol() const
Definition std_expr.h:3571
exprt & value()
Definition std_expr.h:3586
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3026
Expression to hold a nondeterministic choice.
Definition std_expr.h:242
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:265
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:246
const irep_idt & get_identifier() const
Definition std_expr.h:270
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition std_expr.h:255
Boolean negation.
Definition std_expr.h:2278
not_exprt(exprt _op)
Definition std_expr.h:2280
Disequality.
Definition std_expr.h:1365
notequal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1367
An expression without operands.
Definition std_expr.h:22
exprt & op0()=delete
const exprt & op1() const =delete
nullary_exprt(const irep_idt &_id, typet _type)
Definition std_expr.h:24
const exprt & op0() const =delete
void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete
exprt & op3()=delete
void copy_to_operands(const exprt &expr)=delete
operandst & operands()=delete
remove all operand methods
void copy_to_operands(const exprt &, const exprt &)=delete
const operandst & operands() const =delete
exprt & op1()=delete
exprt & op2()=delete
const exprt & op3() const =delete
const exprt & op2() const =delete
Boolean OR.
Definition std_expr.h:2179
or_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2186
or_exprt(exprt::operandst _operands)
Definition std_expr.h:2202
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2194
or_exprt(exprt op0, exprt op1)
Definition std_expr.h:2181
The plus expression Associativity is not specified.
Definition std_expr.h:947
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition std_expr.h:954
plus_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:949
plus_exprt(operandst _operands, typet _type)
Definition std_expr.h:963
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition std_expr.h:517
predicate_exprt(const irep_idt &_id)
Definition std_expr.h:519
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:539
sign_exprt(exprt _op)
Definition std_expr.h:541
Struct constructor from list of elements.
Definition std_expr.h:1819
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:91
struct_exprt(operandst _operands, typet _type)
Definition std_expr.h:1821
Expression to hold a symbol (variable)
Definition std_expr.h:113
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:137
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:132
symbol_exprt(typet type)
Definition std_expr.h:116
symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:122
const irep_idt & get_identifier() const
Definition std_expr.h:142
An expression with three operands.
Definition std_expr.h:49
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:83
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition std_expr.h:52
const exprt & op3() const =delete
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
exprt & op2()
Definition expr.h:131
exprt & op3()=delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:73
The Boolean constant true.
Definition std_expr.h:3008
An expression denoting a type.
Definition std_expr.h:2906
type_exprt(typet type)
Definition std_expr.h:2908
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
typecast_exprt(exprt op, typet _type)
Definition std_expr.h:2019
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition std_expr.h:316
const exprt & op3() const =delete
exprt & op2()=delete
const exprt & op1() const =delete
exprt & op3()=delete
const exprt & op() const
Definition std_expr.h:326
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition std_expr.h:321
const exprt & op2() const =delete
exprt & op()
Definition std_expr.h:331
exprt & op1()=delete
The unary minus expression.
Definition std_expr.h:423
unary_minus_exprt(exprt _op)
Definition std_expr.h:430
unary_minus_exprt(exprt _op, typet _type)
Definition std_expr.h:425
The unary plus expression.
Definition std_expr.h:472
unary_plus_exprt(exprt op)
Definition std_expr.h:474
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:528
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition std_expr.h:530
Union constructor from single element.
Definition std_expr.h:1708
std::size_t get_component_number() const
Definition std_expr.h:1726
void set_component_number(std::size_t component_number)
Definition std_expr.h:1731
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:1721
irep_idt get_component_name() const
Definition std_expr.h:1716
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition std_expr.h:1710
Operator to update elements in structs and arrays.
Definition std_expr.h:2608
exprt & old()
Definition std_expr.h:2620
exprt::operandst & designator()
Definition std_expr.h:2634
exprt & new_value()
Definition std_expr.h:2644
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2661
const exprt & new_value() const
Definition std_expr.h:2649
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition std_expr.h:2610
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2654
const exprt & old() const
Definition std_expr.h:2625
const exprt::operandst & designator() const
Definition std_expr.h:2639
Vector constructor from list of elements.
Definition std_expr.h:1672
vector_exprt(operandst _operands, vector_typet _type)
Definition std_expr.h:1674
The vector type.
Definition std_types.h:1008
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
const exprt & old() const
Definition std_expr.h:2439
const exprt & where() const
Definition std_expr.h:2449
exprt & new_value()
Definition std_expr.h:2454
exprt & where()
Definition std_expr.h:2444
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition std_expr.h:2426
const exprt & new_value() const
Definition std_expr.h:2459
exprt & old()
Definition std_expr.h:2434
Boolean XOR.
Definition std_expr.h:2242
xor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2244
Templated functions to cast to specific exprt-derived classes.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
const irept & get_nil_irep()
Definition irep.cpp:19
dstring_hash irep_id_hash
Definition irep.h:39
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
STL namespace.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition std_expr.h:1331
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition std_expr.h:1374
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition std_expr.h:1891
bool can_cast_expr< not_exprt >(const exprt &base)
Definition std_expr.h:2287
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1842
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition std_expr.h:1654
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition std_expr.h:2035
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition std_expr.h:2925
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1543
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition std_expr.h:1831
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:840
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition std_expr.h:497
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition std_expr.h:2251
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition std_expr.h:1061
bool can_cast_expr< if_exprt >(const exprt &base)
Definition std_expr.h:2387
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
Definition std_expr.h:3538
bool can_cast_expr< named_term_exprt >(const exprt &base)
Definition std_expr.h:3593
bool can_cast_expr< binding_exprt >(const exprt &base)
Definition std_expr.h:3103
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1217
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1077
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition std_expr.h:2118
bool can_cast_expr< member_designatort >(const exprt &base)
Definition std_expr.h:2572
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3425
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
Definition std_expr.h:98
const named_term_exprt & to_named_term_expr(const exprt &expr)
Cast an exprt to a named_term_exprt.
Definition std_expr.h:3609
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition std_expr.h:3408
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition std_expr.h:2262
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2226
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1603
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition std_expr.h:1980
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition std_expr.h:387
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition std_expr.h:548
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition std_expr.h:3332
bool can_cast_expr< type_exprt >(const exprt &base)
Definition std_expr.h:2914
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:51
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition std_expr.h:3548
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
void validate_expr(const symbol_exprt &value)
Definition std_expr.h:211
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1146
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition std_expr.h:437
bool can_cast_expr< less_than_exprt >(const exprt &base)
Definition std_expr.h:803
bool can_cast_expr< with_exprt >(const exprt &base)
Definition std_expr.h:2466
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition std_expr.h:1692
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:63
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition std_expr.h:1015
bool can_cast_expr< let_exprt >(const exprt &base)
Definition std_expr.h:3257
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:986
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition std_expr.h:1390
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition std_expr.h:970
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:932
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition std_expr.h:1527
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3273
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition std_expr.h:403
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition std_expr.h:277
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition std_expr.h:2976
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
bool can_cast_expr< index_exprt >(const exprt &base)
Definition std_expr.h:1462
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:206
const empty_union_exprt & to_empty_union_expr(const exprt &expr)
Cast an exprt to an empty_union_exprt.
Definition std_expr.h:1800
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1031
bool can_cast_expr< member_exprt >(const exprt &base)
Definition std_expr.h:2870
bool can_cast_expr< empty_union_exprt >(const exprt &base)
Definition std_expr.h:1783
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:1997
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition std_expr.h:3121
bool can_cast_expr< or_exprt >(const exprt &base)
Definition std_expr.h:2215
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition std_expr.h:1201
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2539
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1754
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition std_expr.h:3315
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:1952
bool can_cast_expr< update_exprt >(const exprt &base)
Definition std_expr.h:2671
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition std_expr.h:740
bool can_cast_expr< euclidean_mod_exprt >(const exprt &base)
Definition std_expr.h:1269
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition std_expr.h:1681
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition std_expr.h:1644
bool can_cast_expr< index_designatort >(const exprt &base)
Definition std_expr.h:2523
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2303
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2486
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1907
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition std_expr.h:481
bool can_cast_expr< and_exprt >(const exprt &base)
Definition std_expr.h:2107
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition std_expr.h:761
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2159
bool can_cast_expr< array_exprt >(const exprt &base)
Definition std_expr.h:1592
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition std_expr.h:644
bool can_cast_expr< div_exprt >(const exprt &base)
Definition std_expr.h:1130
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2688
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition std_expr.h:3035
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:453
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1347
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
Definition std_expr.h:782
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition std_expr.h:2143
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition std_expr.h:345
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
Definition std_expr.h:824
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition std_expr.h:293
bool can_cast_expr< union_exprt >(const exprt &base)
Definition std_expr.h:1738
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition std_expr.h:2588
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition std_expr.h:1935
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition std_expr.h:564
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition std_expr.h:1285
Pre-defined types.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1102
size_t operator()(const ::symbol_exprt &sym)
Definition std_expr.h:155
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
validation_modet