CBMC
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
29 static void check(
30 const exprt &expr,
32 {
34 vm,
35 expr.operands().size() == 0,
36 "nullary expression must not have operands");
37 }
38
39 static void validate(
40 const exprt &expr,
41 const namespacet &,
43 {
44 check(expr, vm);
45 }
46
48 operandst &operands() = delete;
49 const operandst &operands() const = delete;
50
51 const exprt &op0() const = delete;
52 exprt &op0() = delete;
53 const exprt &op1() const = delete;
54 exprt &op1() = delete;
55 const exprt &op2() const = delete;
56 exprt &op2() = delete;
57 const exprt &op3() const = delete;
58 exprt &op3() = delete;
59
60 void copy_to_operands(const exprt &expr) = delete;
61 void copy_to_operands(const exprt &, const exprt &) = delete;
62 void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
63};
64
67{
68public:
69 // constructor
71 const irep_idt &_id,
72 exprt _op0,
73 exprt _op1,
74 exprt _op2,
75 typet _type)
77 _id,
78 std::move(_type),
79 {std::move(_op0), std::move(_op1), std::move(_op2)})
80 {
81 }
82
83 // make op0 to op2 public
84 using exprt::op0;
85 using exprt::op1;
86 using exprt::op2;
87
88 const exprt &op3() const = delete;
89 exprt &op3() = delete;
90
91 static void check(
92 const exprt &expr,
94 {
96 vm,
97 expr.operands().size() == 3,
98 "ternary expression must have three operands");
99 }
100
101 static void validate(
102 const exprt &expr,
103 const namespacet &,
105 {
106 check(expr, vm);
107 }
108};
109
116inline const ternary_exprt &to_ternary_expr(const exprt &expr)
117{
119 return static_cast<const ternary_exprt &>(expr);
120}
121
124{
126 return static_cast<ternary_exprt &>(expr);
127}
128
131{
132public:
135 {
136 }
137
140 symbol_exprt(const irep_idt &identifier, typet type)
142 {
143 set_identifier(identifier);
144 }
145
151 {
152 return symbol_exprt(id, typet());
153 }
154
155 void set_identifier(const irep_idt &identifier)
156 {
157 set(ID_identifier, identifier);
158 }
159
161 {
162 return get(ID_identifier);
163 }
164
167 {
168 if(location.is_not_nil())
169 add_source_location() = std::move(location);
170 return *this;
171 }
172
175 {
176 if(location.is_not_nil())
177 add_source_location() = std::move(location);
178 return std::move(*this);
179 }
180
183 {
184 if(other.source_location().is_not_nil())
185 add_source_location() = other.source_location();
186 return *this;
187 }
188
191 {
192 if(other.source_location().is_not_nil())
193 add_source_location() = other.source_location();
194 return std::move(*this);
195 }
196};
197
198// NOLINTNEXTLINE(readability/namespace)
199namespace std
200{
201template <>
202// NOLINTNEXTLINE(readability/identifiers)
203struct hash<::symbol_exprt>
204{
205 size_t operator()(const ::symbol_exprt &sym)
206 {
207 return irep_id_hash()(sym.get_identifier());
208 }
209};
210} // namespace std
211
215{
216public:
220 : symbol_exprt(identifier, std::move(type))
221 {
222 }
223
225 {
227 }
228
230 {
231 return set(ID_C_static_lifetime, true);
232 }
233
238
239 bool is_thread_local() const
240 {
242 }
243
245 {
246 return set(ID_C_thread_local, true);
247 }
248
253};
254
255template <>
256inline bool can_cast_expr<symbol_exprt>(const exprt &base)
257{
258 return base.id() == ID_symbol;
259}
260
261inline void validate_expr(const symbol_exprt &value)
262{
263 validate_operands(value, 0, "Symbols must not have operands");
264}
265
272inline const symbol_exprt &to_symbol_expr(const exprt &expr)
273{
274 PRECONDITION(expr.id()==ID_symbol);
275 const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
277 return ret;
278}
279
282{
283 PRECONDITION(expr.id()==ID_symbol);
284 symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
286 return ret;
287}
288
289
292{
293public:
298 {
299 set_identifier(identifier);
300 }
301
306 irep_idt identifier,
307 typet type,
308 source_locationt location)
310 {
311 set_identifier(std::move(identifier));
312 add_source_location() = std::move(location);
313 }
314
315 void set_identifier(const irep_idt &identifier)
316 {
317 set(ID_identifier, identifier);
318 }
319
321 {
322 return get(ID_identifier);
323 }
324};
325
326template <>
328{
329 return base.id() == ID_nondet_symbol;
330}
331
332inline void validate_expr(const nondet_symbol_exprt &value)
333{
334 validate_operands(value, 0, "Symbols must not have operands");
335}
336
344{
347 return static_cast<const nondet_symbol_exprt &>(expr);
348}
349
352{
353 PRECONDITION(expr.id()==ID_symbol);
355 return static_cast<nondet_symbol_exprt &>(expr);
356}
357
358
361{
362public:
365 {
366 }
367
369 : expr_protectedt(_id, std::move(_type), {std::move(_op)})
370 {
371 }
372
373 static void check(
374 const exprt &expr,
376 {
378 vm,
379 expr.operands().size() == 1,
380 "unary expression must have one operand");
381 }
382
383 static void validate(
384 const exprt &expr,
385 const namespacet &,
387 {
388 check(expr, vm);
389 }
390
391 const exprt &op() const
392 {
393 return op0();
394 }
395
397 {
398 return op0();
399 }
400
401 const exprt &op1() const = delete;
402 exprt &op1() = delete;
403 const exprt &op2() const = delete;
404 exprt &op2() = delete;
405 const exprt &op3() const = delete;
406 exprt &op3() = delete;
407};
408
409template <>
410inline bool can_cast_expr<unary_exprt>(const exprt &base)
411{
412 return base.operands().size() == 1;
413}
414
415inline void validate_expr(const unary_exprt &value)
416{
417 unary_exprt::check(value);
418}
419
426inline const unary_exprt &to_unary_expr(const exprt &expr)
427{
428 unary_exprt::check(expr);
429 return static_cast<const unary_exprt &>(expr);
430}
431
434{
435 unary_exprt::check(expr);
436 return static_cast<unary_exprt &>(expr);
437}
438
439
442{
443public:
445 {
446 }
447};
448
449template <>
450inline bool can_cast_expr<abs_exprt>(const exprt &base)
451{
452 return base.id() == ID_abs;
453}
454
455inline void validate_expr(const abs_exprt &value)
456{
457 validate_operands(value, 1, "Absolute value must have one operand");
458}
459
466inline const abs_exprt &to_abs_expr(const exprt &expr)
467{
468 PRECONDITION(expr.id()==ID_abs);
469 abs_exprt::check(expr);
470 return static_cast<const abs_exprt &>(expr);
471}
472
475{
476 PRECONDITION(expr.id()==ID_abs);
477 abs_exprt::check(expr);
478 return static_cast<abs_exprt &>(expr);
479}
480
481
484{
485public:
487 : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
488 {
489 }
490
493 {
494 }
495};
496
497template <>
499{
500 return base.id() == ID_unary_minus;
501}
502
503inline void validate_expr(const unary_minus_exprt &value)
504{
505 validate_operands(value, 1, "Unary minus must have one operand");
506}
507
515{
518 return static_cast<const unary_minus_exprt &>(expr);
519}
520
523{
526 return static_cast<unary_minus_exprt &>(expr);
527}
528
531{
532public:
535 {
536 }
537};
538
539template <>
541{
542 return base.id() == ID_unary_plus;
543}
544
545inline void validate_expr(const unary_plus_exprt &value)
546{
547 validate_operands(value, 1, "unary plus must have one operand");
548}
549
556inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
557{
558 PRECONDITION(expr.id() == ID_unary_plus);
560 return static_cast<const unary_plus_exprt &>(expr);
561}
562
565{
566 PRECONDITION(expr.id() == ID_unary_plus);
568 return static_cast<unary_plus_exprt &>(expr);
569}
570
574{
575public:
576 explicit predicate_exprt(const irep_idt &_id)
578 {
579 }
580};
581
585{
586public:
588 : unary_exprt(_id, std::move(_op), bool_typet())
589 {
590 }
591};
592
596{
597public:
600 {
601 }
602};
603
604template <>
605inline bool can_cast_expr<sign_exprt>(const exprt &base)
606{
607 return base.id() == ID_sign;
608}
609
610inline void validate_expr(const sign_exprt &expr)
611{
612 validate_operands(expr, 1, "sign expression must have one operand");
613}
614
621inline const sign_exprt &to_sign_expr(const exprt &expr)
622{
623 PRECONDITION(expr.id() == ID_sign);
624 sign_exprt::check(expr);
625 return static_cast<const sign_exprt &>(expr);
626}
627
630{
631 PRECONDITION(expr.id() == ID_sign);
632 sign_exprt::check(expr);
633 return static_cast<sign_exprt &>(expr);
634}
635
638{
639public:
641 : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
642 {
643 }
644
646 : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
647 {
648 }
649
650 static void check(
651 const exprt &expr,
653 {
655 vm,
656 expr.operands().size() == 2,
657 "binary expression must have two operands");
658 }
659
660 static void validate(
661 const exprt &expr,
662 const namespacet &,
664 {
665 check(expr, vm);
666 }
667
669 {
670 return exprt::op0();
671 }
672
673 const exprt &lhs() const
674 {
675 return exprt::op0();
676 }
677
679 {
680 return exprt::op1();
681 }
682
683 const exprt &rhs() const
684 {
685 return exprt::op1();
686 }
687
688 // make op0 and op1 public
689 using exprt::op0;
690 using exprt::op1;
691
692 const exprt &op2() const = delete;
693 exprt &op2() = delete;
694 const exprt &op3() const = delete;
695 exprt &op3() = delete;
696};
697
698template <>
699inline bool can_cast_expr<binary_exprt>(const exprt &base)
700{
701 return base.operands().size() == 2;
702}
703
704inline void validate_expr(const binary_exprt &value)
705{
706 binary_exprt::check(value);
707}
708
715inline const binary_exprt &to_binary_expr(const exprt &expr)
716{
718 return static_cast<const binary_exprt &>(expr);
719}
720
723{
725 return static_cast<binary_exprt &>(expr);
726}
727
731{
732public:
734 : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
735 {
736 }
737
738 static void check(
739 const exprt &expr,
741 {
742 binary_exprt::check(expr, vm);
743 }
744
745 static void validate(
746 const exprt &expr,
747 const namespacet &ns,
749 {
750 binary_exprt::validate(expr, ns, vm);
751
753 vm,
754 expr.is_boolean(),
755 "result of binary predicate expression should be of type bool");
756 }
757};
758
762{
763public:
768
769 static void check(
770 const exprt &expr,
772 {
774 }
775
776 static void validate(
777 const exprt &expr,
778 const namespacet &ns,
780 {
782
783 // we now can safely assume that 'expr' is a binary predicate
784 const auto &expr_binary = static_cast<const binary_predicate_exprt &>(expr);
785
786 // check that the types of the operands are the same
788 vm,
789 expr_binary.op0().type() == expr_binary.op1().type(),
790 "lhs and rhs of binary relation expression should have same type");
791 }
792};
793
794template <>
796{
797 return can_cast_expr<binary_exprt>(base);
798}
799
800inline void validate_expr(const binary_relation_exprt &value)
801{
803}
804
807{
808public:
813};
814
815template <>
817{
818 return base.id() == ID_gt;
819}
820
821inline void validate_expr(const greater_than_exprt &value)
822{
824}
825
835
836template <>
838{
839 return base.id() == ID_ge;
840}
841
843{
845}
846
849{
850public:
855};
856
857template <>
858inline bool can_cast_expr<less_than_exprt>(const exprt &base)
859{
860 return base.id() == ID_lt;
861}
862
863inline void validate_expr(const less_than_exprt &value)
864{
866}
867
877
878template <>
880{
881 return base.id() == ID_le;
882}
883
885{
887}
888
896{
898 return static_cast<const binary_relation_exprt &>(expr);
899}
900
903{
905 return static_cast<binary_relation_exprt &>(expr);
906}
907
908
912{
913public:
915 : expr_protectedt(_id, std::move(_type))
916 {
917 operands() = std::move(_operands);
918 }
919
921 : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
922 {
923 }
924
926 : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
927 {
928 }
929
930 // In contrast to exprt::opX, the methods
931 // below check the size.
933 {
934 PRECONDITION(operands().size() >= 1);
935 return operands().front();
936 }
937
939 {
940 PRECONDITION(operands().size() >= 2);
941 return operands()[1];
942 }
943
945 {
946 PRECONDITION(operands().size() >= 3);
947 return operands()[2];
948 }
949
951 {
952 PRECONDITION(operands().size() >= 4);
953 return operands()[3];
954 }
955
956 const exprt &op0() const
957 {
958 PRECONDITION(operands().size() >= 1);
959 return operands().front();
960 }
961
962 const exprt &op1() const
963 {
964 PRECONDITION(operands().size() >= 2);
965 return operands()[1];
966 }
967
968 const exprt &op2() const
969 {
970 PRECONDITION(operands().size() >= 3);
971 return operands()[2];
972 }
973
974 const exprt &op3() const
975 {
976 PRECONDITION(operands().size() >= 4);
977 return operands()[3];
978 }
979};
980
987inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
988{
989 return static_cast<const multi_ary_exprt &>(expr);
990}
991
994{
995 return static_cast<multi_ary_exprt &>(expr);
996}
997
998
1002{
1003public:
1005 : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
1006 {
1007 }
1008
1011 std::move(_lhs),
1012 ID_plus,
1013 std::move(_rhs),
1014 std::move(_type))
1015 {
1016 }
1017
1019 : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
1020 {
1021 }
1022};
1023
1024template <>
1025inline bool can_cast_expr<plus_exprt>(const exprt &base)
1026{
1027 return base.id() == ID_plus;
1028}
1029
1030inline void validate_expr(const plus_exprt &value)
1031{
1032 validate_operands(value, 2, "Plus must have two or more operands", true);
1033}
1034
1041inline const plus_exprt &to_plus_expr(const exprt &expr)
1042{
1043 PRECONDITION(expr.id()==ID_plus);
1044 const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
1046 return ret;
1047}
1048
1051{
1052 PRECONDITION(expr.id()==ID_plus);
1053 plus_exprt &ret = static_cast<plus_exprt &>(expr);
1055 return ret;
1056}
1057
1058
1061{
1062public:
1064 : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
1065 {
1066 }
1067};
1068
1069template <>
1070inline bool can_cast_expr<minus_exprt>(const exprt &base)
1071{
1072 return base.id() == ID_minus;
1073}
1074
1075inline void validate_expr(const minus_exprt &value)
1076{
1077 validate_operands(value, 2, "Minus must have two or more operands", true);
1078}
1079
1086inline const minus_exprt &to_minus_expr(const exprt &expr)
1087{
1088 PRECONDITION(expr.id()==ID_minus);
1089 const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
1091 return ret;
1092}
1093
1096{
1097 PRECONDITION(expr.id()==ID_minus);
1098 minus_exprt &ret = static_cast<minus_exprt &>(expr);
1100 return ret;
1101}
1102
1103
1107{
1108public:
1110 : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
1111 {
1112 }
1113
1118};
1119
1120template <>
1121inline bool can_cast_expr<mult_exprt>(const exprt &base)
1122{
1123 return base.id() == ID_mult;
1124}
1125
1126inline void validate_expr(const mult_exprt &value)
1127{
1128 validate_operands(value, 2, "Multiply must have two or more operands", true);
1129}
1130
1137inline const mult_exprt &to_mult_expr(const exprt &expr)
1138{
1139 PRECONDITION(expr.id()==ID_mult);
1140 const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1142 return ret;
1143}
1144
1147{
1148 PRECONDITION(expr.id()==ID_mult);
1149 mult_exprt &ret = static_cast<mult_exprt &>(expr);
1151 return ret;
1152}
1153
1154
1157{
1158public:
1160 : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1161 {
1162 }
1163
1166 {
1167 return op0();
1168 }
1169
1171 const exprt &dividend() const
1172 {
1173 return op0();
1174 }
1175
1178 {
1179 return op1();
1180 }
1181
1183 const exprt &divisor() const
1184 {
1185 return op1();
1186 }
1187};
1188
1189template <>
1190inline bool can_cast_expr<div_exprt>(const exprt &base)
1191{
1192 return base.id() == ID_div;
1193}
1194
1195inline void validate_expr(const div_exprt &value)
1196{
1197 validate_operands(value, 2, "Divide must have two operands");
1198}
1199
1206inline const div_exprt &to_div_expr(const exprt &expr)
1207{
1208 PRECONDITION(expr.id()==ID_div);
1209 const div_exprt &ret = static_cast<const div_exprt &>(expr);
1211 return ret;
1212}
1213
1216{
1217 PRECONDITION(expr.id()==ID_div);
1218 div_exprt &ret = static_cast<div_exprt &>(expr);
1220 return ret;
1221}
1222
1228{
1229public:
1231 : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1232 {
1233 }
1234
1237 {
1238 return op0();
1239 }
1240
1242 const exprt &dividend() const
1243 {
1244 return op0();
1245 }
1246
1249 {
1250 return op1();
1251 }
1252
1254 const exprt &divisor() const
1255 {
1256 return op1();
1257 }
1258};
1259
1260template <>
1261inline bool can_cast_expr<mod_exprt>(const exprt &base)
1262{
1263 return base.id() == ID_mod;
1264}
1265
1266inline void validate_expr(const mod_exprt &value)
1267{
1268 validate_operands(value, 2, "Modulo must have two operands");
1269}
1270
1277inline const mod_exprt &to_mod_expr(const exprt &expr)
1278{
1279 PRECONDITION(expr.id()==ID_mod);
1280 const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1282 return ret;
1283}
1284
1287{
1288 PRECONDITION(expr.id()==ID_mod);
1289 mod_exprt &ret = static_cast<mod_exprt &>(expr);
1291 return ret;
1292}
1293
1296{
1297public:
1302
1305 {
1306 return op0();
1307 }
1308
1310 const exprt &dividend() const
1311 {
1312 return op0();
1313 }
1314
1317 {
1318 return op1();
1319 }
1320
1322 const exprt &divisor() const
1323 {
1324 return op1();
1325 }
1326};
1327
1328template <>
1330{
1331 return base.id() == ID_euclidean_mod;
1332}
1333
1334inline void validate_expr(const euclidean_mod_exprt &value)
1335{
1336 validate_operands(value, 2, "Modulo must have two operands");
1337}
1338
1346{
1347 PRECONDITION(expr.id() == ID_euclidean_mod);
1348 const euclidean_mod_exprt &ret =
1349 static_cast<const euclidean_mod_exprt &>(expr);
1351 return ret;
1352}
1353
1356{
1357 PRECONDITION(expr.id() == ID_euclidean_mod);
1358 euclidean_mod_exprt &ret = static_cast<euclidean_mod_exprt &>(expr);
1360 return ret;
1361}
1362
1363
1366{
1367public:
1369 : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1370 {
1371 PRECONDITION(lhs().type() == rhs().type());
1372 }
1373
1374 static void check(
1375 const exprt &expr,
1377 {
1379 }
1380
1381 static void validate(
1382 const exprt &expr,
1383 const namespacet &ns,
1385 {
1386 binary_relation_exprt::validate(expr, ns, vm);
1387 }
1388};
1389
1390template <>
1391inline bool can_cast_expr<equal_exprt>(const exprt &base)
1392{
1393 return base.id() == ID_equal;
1394}
1395
1396inline void validate_expr(const equal_exprt &value)
1397{
1398 equal_exprt::check(value);
1399}
1400
1407inline const equal_exprt &to_equal_expr(const exprt &expr)
1408{
1409 PRECONDITION(expr.id()==ID_equal);
1410 equal_exprt::check(expr);
1411 return static_cast<const equal_exprt &>(expr);
1412}
1413
1416{
1417 PRECONDITION(expr.id()==ID_equal);
1418 equal_exprt::check(expr);
1419 return static_cast<equal_exprt &>(expr);
1420}
1421
1422
1425{
1426public:
1431};
1432
1433template <>
1434inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1435{
1436 return base.id() == ID_notequal;
1437}
1438
1439inline void validate_expr(const notequal_exprt &value)
1440{
1441 validate_operands(value, 2, "Inequality must have two operands");
1442}
1443
1450inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1451{
1452 PRECONDITION(expr.id()==ID_notequal);
1453 const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1455 return ret;
1456}
1457
1460{
1461 PRECONDITION(expr.id()==ID_notequal);
1462 notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1464 return ret;
1465}
1466
1467
1470{
1471public:
1472 // _array must have either index or vector type.
1473 // When _array has array_type, the type of _index
1474 // must be array_type.index_type().
1475 // This will eventually be enforced using a precondition.
1477 : binary_exprt(
1478 _array,
1479 ID_index,
1480 std::move(_index),
1481 to_type_with_subtype(_array.type()).subtype())
1482 {
1483 const auto &array_op_type = _array.type();
1485 array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1486 }
1487
1489 : binary_exprt(
1490 std::move(_array),
1491 ID_index,
1492 std::move(_index),
1493 std::move(_type))
1494 {
1495 const auto &array_op_type = array().type();
1497 array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1498 }
1499
1501 {
1502 return op0();
1503 }
1504
1505 const exprt &array() const
1506 {
1507 return op0();
1508 }
1509
1511 {
1512 return op1();
1513 }
1514
1515 const exprt &index() const
1516 {
1517 return op1();
1518 }
1519};
1520
1521template <>
1522inline bool can_cast_expr<index_exprt>(const exprt &base)
1523{
1524 return base.id() == ID_index;
1525}
1526
1527inline void validate_expr(const index_exprt &value)
1528{
1529 validate_operands(value, 2, "Array index must have two operands");
1530}
1531
1538inline const index_exprt &to_index_expr(const exprt &expr)
1539{
1540 PRECONDITION(expr.id()==ID_index);
1541 const index_exprt &ret = static_cast<const index_exprt &>(expr);
1543 return ret;
1544}
1545
1548{
1549 PRECONDITION(expr.id()==ID_index);
1550 index_exprt &ret = static_cast<index_exprt &>(expr);
1552 return ret;
1553}
1554
1555
1558{
1559public:
1561 : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1562 {
1563 }
1564
1565 const array_typet &type() const
1566 {
1567 return static_cast<const array_typet &>(unary_exprt::type());
1568 }
1569
1571 {
1572 return static_cast<array_typet &>(unary_exprt::type());
1573 }
1574
1576 {
1577 return op0();
1578 }
1579
1580 const exprt &what() const
1581 {
1582 return op0();
1583 }
1584};
1585
1586template <>
1587inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1588{
1589 return base.id() == ID_array_of;
1590}
1591
1592inline void validate_expr(const array_of_exprt &value)
1593{
1594 validate_operands(value, 1, "'Array of' must have one operand");
1595}
1596
1603inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1604{
1605 PRECONDITION(expr.id()==ID_array_of);
1607 return static_cast<const array_of_exprt &>(expr);
1608}
1609
1612{
1613 PRECONDITION(expr.id()==ID_array_of);
1615 return static_cast<array_of_exprt &>(expr);
1616}
1617
1618
1621{
1622public:
1624 : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1625 {
1626 }
1627
1628 const array_typet &type() const
1629 {
1630 return static_cast<const array_typet &>(multi_ary_exprt::type());
1631 }
1632
1634 {
1635 return static_cast<array_typet &>(multi_ary_exprt::type());
1636 }
1637
1639 {
1640 if(other.source_location().is_not_nil())
1641 add_source_location() = other.source_location();
1642 return *this;
1643 }
1644
1646 {
1647 if(other.source_location().is_not_nil())
1648 add_source_location() = other.source_location();
1649 return std::move(*this);
1650 }
1651};
1652
1653template <>
1654inline bool can_cast_expr<array_exprt>(const exprt &base)
1655{
1656 return base.id() == ID_array;
1657}
1658
1665inline const array_exprt &to_array_expr(const exprt &expr)
1666{
1667 PRECONDITION(expr.id()==ID_array);
1668 return static_cast<const array_exprt &>(expr);
1669}
1670
1673{
1674 PRECONDITION(expr.id()==ID_array);
1675 return static_cast<array_exprt &>(expr);
1676}
1677
1681{
1682public:
1684 : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1685 {
1686 }
1687
1688 const array_typet &type() const
1689 {
1690 return static_cast<const array_typet &>(multi_ary_exprt::type());
1691 }
1692
1694 {
1695 return static_cast<array_typet &>(multi_ary_exprt::type());
1696 }
1697
1699 void add(exprt index, exprt value)
1700 {
1701 add_to_operands(std::move(index), std::move(value));
1702 }
1703};
1704
1705template <>
1707{
1708 return base.id() == ID_array_list;
1709}
1710
1711inline void validate_expr(const array_list_exprt &value)
1712{
1713 PRECONDITION(value.operands().size() % 2 == 0);
1714}
1715
1717{
1719 auto &ret = static_cast<const array_list_exprt &>(expr);
1721 return ret;
1722}
1723
1725{
1727 auto &ret = static_cast<array_list_exprt &>(expr);
1729 return ret;
1730}
1731
1734{
1735public:
1737 : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1738 {
1739 }
1740};
1741
1742template <>
1743inline bool can_cast_expr<vector_exprt>(const exprt &base)
1744{
1745 return base.id() == ID_vector;
1746}
1747
1754inline const vector_exprt &to_vector_expr(const exprt &expr)
1755{
1756 PRECONDITION(expr.id()==ID_vector);
1757 return static_cast<const vector_exprt &>(expr);
1758}
1759
1762{
1763 PRECONDITION(expr.id()==ID_vector);
1764 return static_cast<vector_exprt &>(expr);
1765}
1766
1767
1770{
1771public:
1773 : unary_exprt(ID_union, std::move(_value), std::move(_type))
1774 {
1776 }
1777
1779 {
1780 return get(ID_component_name);
1781 }
1782
1783 void set_component_name(const irep_idt &component_name)
1784 {
1785 set(ID_component_name, component_name);
1786 }
1787
1788 std::size_t get_component_number() const
1789 {
1791 }
1792
1793 void set_component_number(std::size_t component_number)
1794 {
1795 set_size_t(ID_component_number, component_number);
1796 }
1797};
1798
1799template <>
1800inline bool can_cast_expr<union_exprt>(const exprt &base)
1801{
1802 return base.id() == ID_union;
1803}
1804
1805inline void validate_expr(const union_exprt &value)
1806{
1807 validate_operands(value, 1, "Union constructor must have one operand");
1808}
1809
1816inline const union_exprt &to_union_expr(const exprt &expr)
1817{
1818 PRECONDITION(expr.id()==ID_union);
1819 union_exprt::check(expr);
1820 return static_cast<const union_exprt &>(expr);
1821}
1822
1825{
1826 PRECONDITION(expr.id()==ID_union);
1827 union_exprt::check(expr);
1828 return static_cast<union_exprt &>(expr);
1829}
1830
1834{
1835public:
1836 explicit empty_union_exprt(typet _type)
1837 : nullary_exprt(ID_empty_union, std::move(_type))
1838 {
1839 }
1840};
1841
1842template <>
1844{
1845 return base.id() == ID_empty_union;
1846}
1847
1848inline void validate_expr(const empty_union_exprt &value)
1849{
1851 value, 0, "Empty-union constructor must not have any operand");
1852}
1853
1861{
1862 PRECONDITION(expr.id() == ID_empty_union);
1864 return static_cast<const empty_union_exprt &>(expr);
1865}
1866
1869{
1870 PRECONDITION(expr.id() == ID_empty_union);
1872 return static_cast<empty_union_exprt &>(expr);
1873}
1874
1877{
1878public:
1880 : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1881 {
1882 }
1883
1884 exprt &component(const irep_idt &name, const namespacet &ns);
1885 const exprt &component(const irep_idt &name, const namespacet &ns) const;
1886};
1887
1888template <>
1889inline bool can_cast_expr<struct_exprt>(const exprt &base)
1890{
1891 return base.id() == ID_struct;
1892}
1893
1900inline const struct_exprt &to_struct_expr(const exprt &expr)
1901{
1902 PRECONDITION(expr.id()==ID_struct);
1903 return static_cast<const struct_exprt &>(expr);
1904}
1905
1908{
1909 PRECONDITION(expr.id()==ID_struct);
1910 return static_cast<struct_exprt &>(expr);
1911}
1912
1913
1916{
1917public:
1919 : binary_exprt(
1920 std::move(_real),
1921 ID_complex,
1922 std::move(_imag),
1923 std::move(_type))
1924 {
1925 }
1926
1928 {
1929 return op0();
1930 }
1931
1932 const exprt &real() const
1933 {
1934 return op0();
1935 }
1936
1938 {
1939 return op1();
1940 }
1941
1942 const exprt &imag() const
1943 {
1944 return op1();
1945 }
1946};
1947
1948template <>
1949inline bool can_cast_expr<complex_exprt>(const exprt &base)
1950{
1951 return base.id() == ID_complex;
1952}
1953
1954inline void validate_expr(const complex_exprt &value)
1955{
1956 validate_operands(value, 2, "Complex constructor must have two operands");
1957}
1958
1965inline const complex_exprt &to_complex_expr(const exprt &expr)
1966{
1967 PRECONDITION(expr.id()==ID_complex);
1968 const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1970 return ret;
1971}
1972
1975{
1976 PRECONDITION(expr.id()==ID_complex);
1977 complex_exprt &ret = static_cast<complex_exprt &>(expr);
1979 return ret;
1980}
1981
1984{
1985public:
1986 explicit complex_real_exprt(const exprt &op)
1988 {
1989 }
1990};
1991
1992template <>
1994{
1995 return base.id() == ID_complex_real;
1996}
1997
1998inline void validate_expr(const complex_real_exprt &expr)
1999{
2001 expr, 1, "real part retrieval operation must have one operand");
2002}
2003
2011{
2012 PRECONDITION(expr.id() == ID_complex_real);
2014 return static_cast<const complex_real_exprt &>(expr);
2015}
2016
2019{
2020 PRECONDITION(expr.id() == ID_complex_real);
2022 return static_cast<complex_real_exprt &>(expr);
2023}
2024
2027{
2028public:
2029 explicit complex_imag_exprt(const exprt &op)
2031 {
2032 }
2033};
2034
2035template <>
2037{
2038 return base.id() == ID_complex_imag;
2039}
2040
2041inline void validate_expr(const complex_imag_exprt &expr)
2042{
2044 expr, 1, "imaginary part retrieval operation must have one operand");
2045}
2046
2054{
2055 PRECONDITION(expr.id() == ID_complex_imag);
2056 const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
2058 return ret;
2059}
2060
2063{
2064 PRECONDITION(expr.id() == ID_complex_imag);
2065 complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
2067 return ret;
2068}
2069
2070
2073{
2074public:
2076 : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2077 {
2078 }
2079
2080 // returns a typecast if the type doesn't already match
2081 static exprt conditional_cast(const exprt &expr, const typet &type)
2082 {
2083 if(expr.type() == type)
2084 return expr;
2085 else
2086 return typecast_exprt(expr, type);
2087 }
2088};
2089
2090template <>
2091inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2092{
2093 return base.id() == ID_typecast;
2094}
2095
2096inline void validate_expr(const typecast_exprt &value)
2097{
2098 validate_operands(value, 1, "Typecast must have one operand");
2099}
2100
2107inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2108{
2109 PRECONDITION(expr.id()==ID_typecast);
2111 return static_cast<const typecast_exprt &>(expr);
2112}
2113
2116{
2117 PRECONDITION(expr.id()==ID_typecast);
2119 return static_cast<typecast_exprt &>(expr);
2120}
2121
2122
2125{
2126public:
2128 : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2129 {
2130 }
2131
2134 ID_and,
2135 {std::move(op0), std::move(op1), std::move(op2)},
2136 bool_typet())
2137 {
2138 }
2139
2142 ID_and,
2143 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2144 bool_typet())
2145 {
2146 }
2147
2152};
2153
2157
2159
2160template <>
2161inline bool can_cast_expr<and_exprt>(const exprt &base)
2162{
2163 return base.id() == ID_and;
2164}
2165
2172inline const and_exprt &to_and_expr(const exprt &expr)
2173{
2174 PRECONDITION(expr.id()==ID_and);
2175 return static_cast<const and_exprt &>(expr);
2176}
2177
2180{
2181 PRECONDITION(expr.id()==ID_and);
2182 return static_cast<and_exprt &>(expr);
2183}
2184
2191{
2192public:
2194 : multi_ary_exprt(std::move(op0), ID_nand, std::move(op1), bool_typet())
2195 {
2196 }
2197
2202};
2203
2210inline const nand_exprt &to_nand_expr(const exprt &expr)
2211{
2212 PRECONDITION(expr.id() == ID_nand);
2213 return static_cast<const nand_exprt &>(expr);
2214}
2215
2218{
2219 PRECONDITION(expr.id() == ID_nand);
2220 return static_cast<nand_exprt &>(expr);
2221}
2222
2225{
2226public:
2228 : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2229 {
2230 }
2231};
2232
2233template <>
2234inline bool can_cast_expr<implies_exprt>(const exprt &base)
2235{
2236 return base.id() == ID_implies;
2237}
2238
2239inline void validate_expr(const implies_exprt &value)
2240{
2241 validate_operands(value, 2, "Implies must have two operands");
2242}
2243
2250inline const implies_exprt &to_implies_expr(const exprt &expr)
2251{
2252 PRECONDITION(expr.id()==ID_implies);
2253 const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2255 return ret;
2256}
2257
2260{
2261 PRECONDITION(expr.id()==ID_implies);
2262 implies_exprt &ret = static_cast<implies_exprt &>(expr);
2264 return ret;
2265}
2266
2267
2270{
2271public:
2273 : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2274 {
2275 }
2276
2279 ID_or,
2280 {std::move(op0), std::move(op1), std::move(op2)},
2281 bool_typet())
2282 {
2283 }
2284
2287 ID_or,
2288 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2289 bool_typet())
2290 {
2291 }
2292
2297};
2298
2302
2304
2305template <>
2306inline bool can_cast_expr<or_exprt>(const exprt &base)
2307{
2308 return base.id() == ID_or;
2309}
2310
2317inline const or_exprt &to_or_expr(const exprt &expr)
2318{
2319 PRECONDITION(expr.id()==ID_or);
2320 return static_cast<const or_exprt &>(expr);
2321}
2322
2325{
2326 PRECONDITION(expr.id()==ID_or);
2327 return static_cast<or_exprt &>(expr);
2328}
2329
2336{
2337public:
2339 : multi_ary_exprt(std::move(op0), ID_nor, std::move(op1), bool_typet())
2340 {
2341 }
2342
2347};
2348
2355inline const nor_exprt &to_nor_expr(const exprt &expr)
2356{
2357 PRECONDITION(expr.id() == ID_nor);
2358 return static_cast<const nor_exprt &>(expr);
2359}
2360
2363{
2364 PRECONDITION(expr.id() == ID_nor);
2365 return static_cast<nor_exprt &>(expr);
2366}
2367
2370{
2371public:
2373 : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2374 {
2375 }
2376
2381};
2382
2383template <>
2384inline bool can_cast_expr<xor_exprt>(const exprt &base)
2385{
2386 return base.id() == ID_xor;
2387}
2388
2395inline const xor_exprt &to_xor_expr(const exprt &expr)
2396{
2397 PRECONDITION(expr.id()==ID_xor);
2398 return static_cast<const xor_exprt &>(expr);
2399}
2400
2403{
2404 PRECONDITION(expr.id()==ID_xor);
2405 return static_cast<xor_exprt &>(expr);
2406}
2407
2414{
2415public:
2417 : multi_ary_exprt(std::move(_op0), ID_xnor, std::move(_op1), bool_typet())
2418 {
2419 }
2420
2425};
2426
2427template <>
2428inline bool can_cast_expr<xnor_exprt>(const exprt &base)
2429{
2430 return base.id() == ID_xnor;
2431}
2432
2439inline const xnor_exprt &to_xnor_expr(const exprt &expr)
2440{
2441 PRECONDITION(expr.id() == ID_xnor);
2442 return static_cast<const xnor_exprt &>(expr);
2443}
2444
2447{
2448 PRECONDITION(expr.id() == ID_xnor);
2449 return static_cast<xnor_exprt &>(expr);
2450}
2451
2454{
2455public:
2457 {
2458 PRECONDITION(as_const(*this).op().is_boolean());
2459 }
2460};
2461
2462template <>
2463inline bool can_cast_expr<not_exprt>(const exprt &base)
2464{
2465 return base.id() == ID_not;
2466}
2467
2468inline void validate_expr(const not_exprt &value)
2469{
2470 validate_operands(value, 1, "Not must have one operand");
2471}
2472
2479inline const not_exprt &to_not_expr(const exprt &expr)
2480{
2481 PRECONDITION(expr.id()==ID_not);
2482 not_exprt::check(expr);
2483 return static_cast<const not_exprt &>(expr);
2484}
2485
2488{
2489 PRECONDITION(expr.id()==ID_not);
2490 not_exprt::check(expr);
2491 return static_cast<not_exprt &>(expr);
2492}
2493
2494
2497{
2498public:
2500 : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2501 {
2502 }
2503
2505 : ternary_exprt(
2506 ID_if,
2507 std::move(cond),
2508 std::move(t),
2509 std::move(f),
2510 std::move(type))
2511 {
2512 }
2513
2515 {
2516 return op0();
2517 }
2518
2519 const exprt &cond() const
2520 {
2521 return op0();
2522 }
2523
2525 {
2526 return op1();
2527 }
2528
2529 const exprt &true_case() const
2530 {
2531 return op1();
2532 }
2533
2535 {
2536 return op2();
2537 }
2538
2539 const exprt &false_case() const
2540 {
2541 return op2();
2542 }
2543
2544 static void check(
2545 const exprt &expr,
2547 {
2548 ternary_exprt::check(expr, vm);
2549 }
2550
2551 static void validate(
2552 const exprt &expr,
2553 const namespacet &ns,
2555 {
2556 ternary_exprt::validate(expr, ns, vm);
2557 }
2558};
2559
2560template <>
2561inline bool can_cast_expr<if_exprt>(const exprt &base)
2562{
2563 return base.id() == ID_if;
2564}
2565
2566inline void validate_expr(const if_exprt &value)
2567{
2568 validate_operands(value, 3, "If-then-else must have three operands");
2569}
2570
2577inline const if_exprt &to_if_expr(const exprt &expr)
2578{
2579 PRECONDITION(expr.id()==ID_if);
2580 const if_exprt &ret = static_cast<const if_exprt &>(expr);
2582 return ret;
2583}
2584
2587{
2588 PRECONDITION(expr.id()==ID_if);
2589 if_exprt &ret = static_cast<if_exprt &>(expr);
2591 return ret;
2592}
2593
2598{
2599public:
2602 ID_with,
2603 _old.type(),
2604 {_old, std::move(_where), std::move(_new_value)})
2605 {
2606 }
2607
2609 {
2610 return op0();
2611 }
2612
2613 const exprt &old() const
2614 {
2615 return op0();
2616 }
2617
2619 {
2620 return op1();
2621 }
2622
2623 const exprt &where() const
2624 {
2625 return op1();
2626 }
2627
2629 {
2630 return op2();
2631 }
2632
2633 const exprt &new_value() const
2634 {
2635 return op2();
2636 }
2637};
2638
2639template <>
2640inline bool can_cast_expr<with_exprt>(const exprt &base)
2641{
2642 return base.id() == ID_with;
2643}
2644
2645inline void validate_expr(const with_exprt &value)
2646{
2648 value, 3, "array/structure update must have at least 3 operands", true);
2650 value.operands().size() % 2 == 1,
2651 "array/structure update must have an odd number of operands");
2652}
2653
2660inline const with_exprt &to_with_expr(const exprt &expr)
2661{
2662 PRECONDITION(expr.id()==ID_with);
2663 const with_exprt &ret = static_cast<const with_exprt &>(expr);
2665 return ret;
2666}
2667
2670{
2671 PRECONDITION(expr.id()==ID_with);
2672 with_exprt &ret = static_cast<with_exprt &>(expr);
2674 return ret;
2675}
2676
2678{
2679public:
2682 {
2683 }
2684
2685 const exprt &index() const
2686 {
2687 return op0();
2688 }
2689
2691 {
2692 return op0();
2693 }
2694};
2695
2696template <>
2698{
2699 return base.id() == ID_index_designator;
2700}
2701
2702inline void validate_expr(const index_designatort &value)
2703{
2704 validate_operands(value, 1, "Index designator must have one operand");
2705}
2706
2714{
2716 const index_designatort &ret = static_cast<const index_designatort &>(expr);
2718 return ret;
2719}
2720
2723{
2725 index_designatort &ret = static_cast<index_designatort &>(expr);
2727 return ret;
2728}
2729
2731{
2732public:
2738
2740 {
2741 return get(ID_component_name);
2742 }
2743};
2744
2745template <>
2747{
2748 return base.id() == ID_member_designator;
2749}
2750
2751inline void validate_expr(const member_designatort &value)
2752{
2753 validate_operands(value, 0, "Member designator must not have operands");
2754}
2755
2763{
2765 const member_designatort &ret = static_cast<const member_designatort &>(expr);
2767 return ret;
2768}
2769
2772{
2774 member_designatort &ret = static_cast<member_designatort &>(expr);
2776 return ret;
2777}
2778
2779
2782{
2783public:
2785 : ternary_exprt(
2786 ID_update,
2787 _old,
2788 std::move(_designator),
2789 std::move(_new_value),
2790 _old.type())
2791 {
2792 }
2793
2795 {
2796 return op0();
2797 }
2798
2799 const exprt &old() const
2800 {
2801 return op0();
2802 }
2803
2804 // the designator operands are either
2805 // 1) member_designator or
2806 // 2) index_designator
2807 // as defined above
2809 {
2810 return op1().operands();
2811 }
2812
2814 {
2815 return op1().operands();
2816 }
2817
2819 {
2820 return op2();
2821 }
2822
2823 const exprt &new_value() const
2824 {
2825 return op2();
2826 }
2827
2829 with_exprt make_with_expr() const;
2830
2831 static void check(
2832 const exprt &expr,
2834 {
2835 ternary_exprt::check(expr, vm);
2836 }
2837
2838 static void validate(
2839 const exprt &expr,
2840 const namespacet &ns,
2842 {
2843 ternary_exprt::validate(expr, ns, vm);
2844 }
2845};
2846
2847template <>
2848inline bool can_cast_expr<update_exprt>(const exprt &base)
2849{
2850 return base.id() == ID_update;
2851}
2852
2853inline void validate_expr(const update_exprt &value)
2854{
2856 value, 3, "Array/structure update must have three operands");
2857}
2858
2865inline const update_exprt &to_update_expr(const exprt &expr)
2866{
2867 PRECONDITION(expr.id()==ID_update);
2868 const update_exprt &ret = static_cast<const update_exprt &>(expr);
2870 return ret;
2871}
2872
2875{
2876 PRECONDITION(expr.id()==ID_update);
2877 update_exprt &ret = static_cast<update_exprt &>(expr);
2879 return ret;
2880}
2881
2882
2883#if 0
2886{
2887public:
2889 const exprt &_array,
2890 const exprt &_index,
2891 const exprt &_new_value):
2893 {
2894 add_to_operands(_array, _index, _new_value);
2895 }
2896
2898 {
2899 operands().resize(3);
2900 }
2901
2902 exprt &array()
2903 {
2904 return op0();
2905 }
2906
2907 const exprt &array() const
2908 {
2909 return op0();
2910 }
2911
2912 exprt &index()
2913 {
2914 return op1();
2915 }
2916
2917 const exprt &index() const
2918 {
2919 return op1();
2920 }
2921
2922 exprt &new_value()
2923 {
2924 return op2();
2925 }
2926
2927 const exprt &new_value() const
2928 {
2929 return op2();
2930 }
2931};
2932
2933template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2934{
2935 return base.id()==ID_array_update;
2936}
2937
2938inline void validate_expr(const array_update_exprt &value)
2939{
2940 validate_operands(value, 3, "Array update must have three operands");
2941}
2942
2949inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2950{
2952 const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2954 return ret;
2955}
2956
2959{
2961 array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2963 return ret;
2964}
2965
2966#endif
2967
2968
2971{
2972public:
2973 member_exprt(exprt op, const irep_idt &component_name, typet _type)
2974 : unary_exprt(ID_member, std::move(op), std::move(_type))
2975 {
2976 const auto &compound_type_id = compound().type().id();
2980 set_component_name(component_name);
2981 }
2982
2992
2994 {
2995 return get(ID_component_name);
2996 }
2997
2998 void set_component_name(const irep_idt &component_name)
2999 {
3000 set(ID_component_name, component_name);
3001 }
3002
3003 std::size_t get_component_number() const
3004 {
3006 }
3007
3008 // will go away, use compound()
3009 const exprt &struct_op() const
3010 {
3011 return op0();
3012 }
3013
3014 // will go away, use compound()
3016 {
3017 return op0();
3018 }
3019
3020 const exprt &compound() const
3021 {
3022 return op0();
3023 }
3024
3026 {
3027 return op0();
3028 }
3029
3030 static void check(
3031 const exprt &expr,
3033 {
3034 DATA_CHECK(
3035 vm,
3036 expr.operands().size() == 1,
3037 "member expression must have one operand");
3038 }
3039
3040 static void validate(
3041 const exprt &expr,
3042 const namespacet &ns,
3044};
3045
3046template <>
3047inline bool can_cast_expr<member_exprt>(const exprt &base)
3048{
3049 return base.id() == ID_member;
3050}
3051
3052inline void validate_expr(const member_exprt &value)
3053{
3054 validate_operands(value, 1, "Extract member must have one operand");
3055}
3056
3063inline const member_exprt &to_member_expr(const exprt &expr)
3064{
3065 PRECONDITION(expr.id()==ID_member);
3066 member_exprt::check(expr);
3067 return static_cast<const member_exprt &>(expr);
3068}
3069
3072{
3073 PRECONDITION(expr.id()==ID_member);
3074 member_exprt::check(expr);
3075 return static_cast<member_exprt &>(expr);
3076}
3077
3078
3081{
3082public:
3084 {
3085 }
3086};
3087
3088template <>
3089inline bool can_cast_expr<type_exprt>(const exprt &base)
3090{
3091 return base.id() == ID_type;
3092}
3093
3100inline const type_exprt &to_type_expr(const exprt &expr)
3101{
3103 type_exprt::check(expr);
3104 return static_cast<const type_exprt &>(expr);
3105}
3106
3109{
3111 type_exprt::check(expr);
3112 return static_cast<type_exprt &>(expr);
3113}
3114
3117{
3118public:
3119 constant_exprt(const irep_idt &_value, typet _type)
3120 : nullary_exprt(ID_constant, std::move(_type))
3121 {
3122 set_value(_value);
3123 }
3124
3125 const irep_idt &get_value() const
3126 {
3127 return get(ID_value);
3128 }
3129
3130 void set_value(const irep_idt &value)
3131 {
3132 set(ID_value, value);
3133 }
3134
3135 bool value_is_zero_string() const;
3136
3140 bool is_null_pointer() const;
3141
3142 static void check(
3143 const exprt &expr,
3145
3146 static void validate(
3147 const exprt &expr,
3148 const namespacet &,
3150 {
3151 check(expr, vm);
3152 }
3153};
3154
3155template <>
3156inline bool can_cast_expr<constant_exprt>(const exprt &base)
3157{
3158 return base.is_constant();
3159}
3160
3161inline void validate_expr(const constant_exprt &value)
3162{
3163 validate_operands(value, 0, "Constants must not have operands");
3164}
3165
3172inline const constant_exprt &to_constant_expr(const exprt &expr)
3173{
3174 PRECONDITION(expr.is_constant());
3176 return static_cast<const constant_exprt &>(expr);
3177}
3178
3181{
3182 PRECONDITION(expr.is_constant());
3184 return static_cast<constant_exprt &>(expr);
3185}
3186
3187
3190{
3191public:
3195};
3196
3199{
3200public:
3204};
3205
3208{
3209public:
3214};
3215
3216template <>
3217inline bool can_cast_expr<nil_exprt>(const exprt &base)
3218{
3219 return base.id() == ID_nil;
3220}
3221
3224{
3225public:
3226 explicit infinity_exprt(typet _type)
3227 : nullary_exprt(ID_infinity, std::move(_type))
3228 {
3229 }
3230};
3231
3234{
3235public:
3236 using variablest = std::vector<symbol_exprt>;
3237
3240 irep_idt _id,
3241 const variablest &_variables,
3242 exprt _where,
3243 typet _type)
3244 : binary_exprt(
3246 ID_tuple,
3248 typet(ID_tuple)),
3249 _id,
3250 std::move(_where),
3251 std::move(_type))
3252 {
3253 }
3254
3256 {
3257 return (variablest &)to_multi_ary_expr(op0()).operands();
3258 }
3259
3260 const variablest &variables() const
3261 {
3262 return (variablest &)to_multi_ary_expr(op0()).operands();
3263 }
3264
3266 {
3267 return op1();
3268 }
3269
3270 const exprt &where() const
3271 {
3272 return op1();
3273 }
3274
3277 exprt instantiate(const exprt::operandst &) const;
3278
3281 exprt instantiate(const variablest &) const;
3282};
3283
3284template <>
3285inline bool can_cast_expr<binding_exprt>(const exprt &base)
3286{
3287 return base.id() == ID_forall || base.id() == ID_exists ||
3288 base.id() == ID_lambda || base.id() == ID_array_comprehension;
3289}
3290
3292{
3294 binding_expr, 2, "Binding expressions must have two operands");
3295}
3296
3303inline const binding_exprt &to_binding_expr(const exprt &expr)
3304{
3306 expr.id() == ID_forall || expr.id() == ID_exists ||
3307 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3308 const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
3310 return ret;
3311}
3312
3320{
3322 expr.id() == ID_forall || expr.id() == ID_exists ||
3323 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3324 binding_exprt &ret = static_cast<binding_exprt &>(expr);
3326 return ret;
3327}
3328
3331{
3332public:
3336 const exprt &where)
3337 : binary_exprt(
3340 std::move(variables),
3341 where,
3342 where.type()),
3343 ID_let,
3345 where.type())
3346 {
3347 PRECONDITION(this->variables().size() == this->values().size());
3348 }
3349
3352 : let_exprt(
3354 operandst{std::move(value)},
3355 where)
3356 {
3357 }
3358
3360 {
3361 return static_cast<binding_exprt &>(op0());
3362 }
3363
3364 const binding_exprt &binding() const
3365 {
3366 return static_cast<const binding_exprt &>(op0());
3367 }
3368
3371 {
3372 auto &variables = binding().variables();
3373 PRECONDITION(variables.size() == 1);
3374 return variables.front();
3375 }
3376
3378 const symbol_exprt &symbol() const
3379 {
3380 const auto &variables = binding().variables();
3381 PRECONDITION(variables.size() == 1);
3382 return variables.front();
3383 }
3384
3387 {
3388 auto &values = this->values();
3389 PRECONDITION(values.size() == 1);
3390 return values.front();
3391 }
3392
3394 const exprt &value() const
3395 {
3396 const auto &values = this->values();
3397 PRECONDITION(values.size() == 1);
3398 return values.front();
3399 }
3400
3402 {
3403 return static_cast<multi_ary_exprt &>(op1()).operands();
3404 }
3405
3406 const operandst &values() const
3407 {
3408 return static_cast<const multi_ary_exprt &>(op1()).operands();
3409 }
3410
3413 {
3414 return binding().variables();
3415 }
3416
3419 {
3420 return binding().variables();
3421 }
3422
3425 {
3426 return binding().where();
3427 }
3428
3430 const exprt &where() const
3431 {
3432 return binding().where();
3433 }
3434
3435 static void validate(const exprt &, validation_modet);
3436};
3437
3438template <>
3439inline bool can_cast_expr<let_exprt>(const exprt &base)
3440{
3441 return base.id() == ID_let;
3442}
3443
3445{
3446 validate_operands(let_expr, 2, "Let must have two operands");
3447}
3448
3455inline const let_exprt &to_let_expr(const exprt &expr)
3456{
3457 PRECONDITION(expr.id()==ID_let);
3458 const let_exprt &ret = static_cast<const let_exprt &>(expr);
3460 return ret;
3461}
3462
3465{
3466 PRECONDITION(expr.id()==ID_let);
3467 let_exprt &ret = static_cast<let_exprt &>(expr);
3469 return ret;
3470}
3471
3472
3477{
3478public:
3480 : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3481 {
3482 }
3483
3487 void add_case(const exprt &condition, const exprt &value)
3488 {
3489 PRECONDITION(condition.is_boolean());
3490 operands().reserve(operands().size() + 2);
3491 operands().push_back(condition);
3492 operands().push_back(value);
3493 }
3494
3495 // a lowering to nested if_exprt
3496 exprt lower() const;
3497};
3498
3499template <>
3500inline bool can_cast_expr<cond_exprt>(const exprt &base)
3501{
3502 return base.id() == ID_cond;
3503}
3504
3505inline void validate_expr(const cond_exprt &value)
3506{
3508 value.operands().size() % 2 == 0, "cond must have even number of operands");
3509}
3510
3517inline const cond_exprt &to_cond_expr(const exprt &expr)
3518{
3519 PRECONDITION(expr.id() == ID_cond);
3520 const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3522 return ret;
3523}
3524
3527{
3528 PRECONDITION(expr.id() == ID_cond);
3529 cond_exprt &ret = static_cast<cond_exprt &>(expr);
3531 return ret;
3532}
3533
3543{
3544public:
3547 exprt body,
3548 array_typet _type)
3549 : binding_exprt(
3551 {std::move(arg)},
3552 std::move(body),
3553 std::move(_type))
3554 {
3555 }
3556
3557 const array_typet &type() const
3558 {
3559 return static_cast<const array_typet &>(binary_exprt::type());
3560 }
3561
3563 {
3564 return static_cast<array_typet &>(binary_exprt::type());
3565 }
3566
3567 const symbol_exprt &arg() const
3568 {
3569 auto &variables = this->variables();
3570 PRECONDITION(variables.size() == 1);
3571 return variables[0];
3572 }
3573
3575 {
3576 auto &variables = this->variables();
3577 PRECONDITION(variables.size() == 1);
3578 return variables[0];
3579 }
3580
3581 const exprt &body() const
3582 {
3583 return where();
3584 }
3585
3587 {
3588 return where();
3589 }
3590};
3591
3592template <>
3594{
3595 return base.id() == ID_array_comprehension;
3596}
3597
3599{
3600 validate_operands(value, 2, "'Array comprehension' must have two operands");
3601}
3602
3609inline const array_comprehension_exprt &
3611{
3614 static_cast<const array_comprehension_exprt &>(expr);
3616 return ret;
3617}
3618
3628
3629inline void validate_expr(const class class_method_descriptor_exprt &value);
3630
3633{
3634public:
3650 typet _type,
3654 : nullary_exprt(ID_virtual_function, std::move(_type))
3655 {
3658 set(ID_C_class, std::move(class_id));
3659 set(ID_C_base_name, std::move(base_method_name));
3660 set(ID_identifier, std::move(id));
3661 validate_expr(*this);
3662 }
3663
3671 {
3672 return get(ID_component_name);
3673 }
3674
3678 const irep_idt &class_id() const
3679 {
3680 return get(ID_C_class);
3681 }
3682
3686 {
3687 return get(ID_C_base_name);
3688 }
3689
3694 {
3695 return get(ID_identifier);
3696 }
3697};
3698
3699inline void validate_expr(const class class_method_descriptor_exprt &value)
3700{
3701 validate_operands(value, 0, "class method descriptor must not have operands");
3703 !value.mangled_method_name().empty(),
3704 "class method descriptor must have a mangled method name.");
3706 !value.class_id().empty(), "class method descriptor must have a class id.");
3708 !value.base_method_name().empty(),
3709 "class method descriptor must have a base method name.");
3711 value.get_identifier() == id2string(value.class_id()) + "." +
3713 "class method descriptor must have an identifier in the expected format.");
3714}
3715
3722inline const class_method_descriptor_exprt &
3724{
3727 return static_cast<const class_method_descriptor_exprt &>(expr);
3728}
3729
3730template <>
3732{
3733 return base.id() == ID_virtual_function;
3734}
3735
3742{
3743public:
3745 : binary_exprt(
3746 std::move(symbol),
3748 value, // not moved, for type
3749 value.type())
3750 {
3751 PRECONDITION(symbol.type() == type());
3752 }
3753
3754 const symbol_exprt &symbol() const
3755 {
3756 return static_cast<const symbol_exprt &>(op0());
3757 }
3758
3760 {
3761 return static_cast<symbol_exprt &>(op0());
3762 }
3763
3764 const exprt &value() const
3765 {
3766 return op1();
3767 }
3768
3770 {
3771 return op1();
3772 }
3773};
3774
3775template <>
3777{
3778 return base.id() == ID_named_term;
3779}
3780
3781inline void validate_expr(const named_term_exprt &value)
3782{
3783 validate_operands(value, 2, "'named term' must have two operands");
3784}
3785
3793{
3794 PRECONDITION(expr.id() == ID_named_term);
3795 const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
3797 return ret;
3798}
3799
3802{
3803 PRECONDITION(expr.id() == ID_named_term);
3804 named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
3806 return ret;
3807}
3808
3809#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:442
abs_exprt(exprt _op)
Definition std_expr.h:444
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ait()
Definition ai.h:565
Boolean AND.
Definition std_expr.h:2125
and_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2132
and_exprt(exprt op0, exprt op1)
Definition std_expr.h:2127
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2140
and_exprt(exprt::operandst _operands)
Definition std_expr.h:2148
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3543
const array_typet & type() const
Definition std_expr.h:3557
const symbol_exprt & arg() const
Definition std_expr.h:3567
const exprt & body() const
Definition std_expr.h:3581
array_typet & type()
Definition std_expr.h:3562
symbol_exprt & arg()
Definition std_expr.h:3574
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition std_expr.h:3545
Array constructor from list of elements.
Definition std_expr.h:1621
array_exprt && with_source_location(const exprt &other) &&
Definition std_expr.h:1645
const array_typet & type() const
Definition std_expr.h:1628
array_exprt & with_source_location(const exprt &other) &
Definition std_expr.h:1638
array_exprt(operandst _operands, array_typet _type)
Definition std_expr.h:1623
array_typet & type()
Definition std_expr.h:1633
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition std_expr.h:1681
void add(exprt index, exprt value)
add an index/value pair
Definition std_expr.h:1699
const array_typet & type() const
Definition std_expr.h:1688
array_list_exprt(operandst _operands, array_typet _type)
Definition std_expr.h:1683
array_typet & type()
Definition std_expr.h:1693
Array constructor from single element.
Definition std_expr.h:1558
array_typet & type()
Definition std_expr.h:1570
array_of_exprt(exprt _what, array_typet _type)
Definition std_expr.h:1560
const exprt & what() const
Definition std_expr.h:1580
const array_typet & type() const
Definition std_expr.h:1565
exprt & what()
Definition std_expr.h:1575
Arrays with given size.
Definition std_types.h:807
A base class for binary expressions.
Definition std_expr.h:638
exprt & lhs()
Definition std_expr.h:668
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:640
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:660
const exprt & op2() const =delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:650
exprt & rhs()
Definition std_expr.h:678
exprt & op0()
Definition expr.h:133
const exprt & lhs() const
Definition std_expr.h:673
exprt & op1()
Definition expr.h:136
exprt & op3()=delete
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition std_expr.h:645
const exprt & rhs() const
Definition std_expr.h:683
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:731
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:738
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition std_expr.h:733
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:745
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:764
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:769
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:776
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:3234
const variablest & variables() const
Definition std_expr.h:3260
const exprt & where() const
Definition std_expr.h:3270
exprt & where()
Definition std_expr.h:3265
variablest & variables()
Definition std_expr.h:3255
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition std_expr.h:3239
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:225
std::vector< symbol_exprt > variablest
Definition std_expr.h:3236
The Boolean type.
Definition std_types.h:36
An expression describing a method on a class.
Definition std_expr.h:3633
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:3685
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition std_expr.h:3670
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:3693
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition std_expr.h:3649
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:3678
Complex constructor from a pair of numbers.
Definition std_expr.h:1916
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition std_expr.h:1918
exprt real()
Definition std_expr.h:1927
exprt imag()
Definition std_expr.h:1937
const exprt & real() const
Definition std_expr.h:1932
const exprt & imag() const
Definition std_expr.h:1942
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
complex_imag_exprt(const exprt &op)
Definition std_expr.h:2029
Real part of the expression describing a complex number.
Definition std_expr.h:1984
complex_real_exprt(const exprt &op)
Definition std_expr.h:1986
Complex numbers made of pair of given subtype.
Definition std_types.h:1133
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition std_expr.h:3477
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition std_expr.h:3487
cond_exprt(operandst _operands, typet _type)
Definition std_expr.h:3479
exprt lower() const
Definition std_expr.cpp:264
A constant literal expression.
Definition std_expr.h:3117
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:3146
const irep_idt & get_value() const
Definition std_expr.h:3125
bool value_is_zero_string() const
Definition std_expr.cpp:19
constant_exprt(const irep_idt &_value, typet _type)
Definition std_expr.h:3119
void set_value(const irep_idt &value)
Definition std_expr.h:3130
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition std_expr.cpp:25
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.cpp:41
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition std_expr.h:215
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:219
bool is_static_lifetime() const
Definition std_expr.h:224
bool is_thread_local() const
Definition std_expr.h:239
Division.
Definition std_expr.h:1157
div_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1159
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1165
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1171
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1183
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1177
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1834
empty_union_exprt(typet _type)
Definition std_expr.h:1836
Equality.
Definition std_expr.h:1366
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:1374
equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1368
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:1381
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1296
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1316
euclidean_mod_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1298
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1322
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1304
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1310
Base class for all expressions.
Definition expr.h:344
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
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:224
static void check(const exprt &, const validation_modet)
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...
Definition expr.h:254
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
exprt & op2()
Definition expr.h:139
source_locationt & add_source_location()
Definition expr.h:236
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
The Boolean constant false.
Definition std_expr.h:3199
Binary greater than operator expression.
Definition std_expr.h:807
greater_than_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:809
Binary greater than or equal operator expression.
Definition std_expr.h:828
greater_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:830
The trinary if-then-else operator.
Definition std_expr.h:2497
const exprt & false_case() const
Definition std_expr.h:2539
exprt & cond()
Definition std_expr.h:2514
const exprt & cond() const
Definition std_expr.h:2519
if_exprt(exprt cond, const exprt &t, exprt f)
Definition std_expr.h:2499
const exprt & true_case() const
Definition std_expr.h:2529
exprt & false_case()
Definition std_expr.h:2534
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition std_expr.h:2504
exprt & true_case()
Definition std_expr.h:2524
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2544
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2551
Boolean implication.
Definition std_expr.h:2225
implies_exprt(exprt op0, exprt op1)
Definition std_expr.h:2227
const exprt & index() const
Definition std_expr.h:2685
index_designatort(exprt _index)
Definition std_expr.h:2680
exprt & index()
Definition std_expr.h:2690
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
index_exprt(exprt _array, exprt _index, typet _type)
Definition std_expr.h:1488
index_exprt(const exprt &_array, exprt _index)
Definition std_expr.h:1476
exprt & array()
Definition std_expr.h:1500
const exprt & index() const
Definition std_expr.h:1515
const exprt & array() const
Definition std_expr.h:1505
An expression denoting infinity.
Definition std_expr.h:3224
infinity_exprt(typet _type)
Definition std_expr.h:3226
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:87
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:82
const irep_idt & id() const
Definition irep.h:388
Binary less than operator expression.
Definition std_expr.h:849
less_than_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:851
Binary less than or equal operator expression.
Definition std_expr.h:870
less_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:872
A let expression.
Definition std_expr.h:3331
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3412
const binding_exprt & binding() const
Definition std_expr.h:3364
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition std_expr.h:3418
operandst & values()
Definition std_expr.h:3401
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition std_expr.h:3351
const exprt & where() const
convenience accessor for binding().where()
Definition std_expr.h:3430
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:168
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition std_expr.h:3378
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition std_expr.h:3333
exprt & value()
convenience accessor for the value of a single binding
Definition std_expr.h:3386
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3424
binding_exprt & binding()
Definition std_expr.h:3359
const operandst & values() const
Definition std_expr.h:3406
const exprt & value() const
convenience accessor for the value of a single binding
Definition std_expr.h:3394
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition std_expr.h:3370
irep_idt get_component_name() const
Definition std_expr.h:2739
member_designatort(const irep_idt &_component_name)
Definition std_expr.h:2733
Extract member of struct or union.
Definition std_expr.h:2971
const exprt & compound() const
Definition std_expr.h:3020
exprt & struct_op()
Definition std_expr.h:3015
const exprt & struct_op() const
Definition std_expr.h:3009
irep_idt get_component_name() const
Definition std_expr.h:2993
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:2998
exprt & compound()
Definition std_expr.h:3025
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:133
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:3030
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition std_expr.h:2973
std::size_t get_component_number() const
Definition std_expr.h:3003
member_exprt(exprt op, const struct_typet::componentt &c)
Definition std_expr.h:2983
Binary minus.
Definition std_expr.h:1061
minus_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1063
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1236
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1242
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1248
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1254
mod_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1230
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
mult_exprt(exprt::operandst factors, typet type)
Definition std_expr.h:1114
mult_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1109
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
exprt & op1()
Definition std_expr.h:938
const exprt & op0() const
Definition std_expr.h:956
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition std_expr.h:925
const exprt & op2() const
Definition std_expr.h:968
const exprt & op3() const
Definition std_expr.h:974
exprt & op0()
Definition std_expr.h:932
exprt & op2()
Definition std_expr.h:944
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:920
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition std_expr.h:914
const exprt & op1() const
Definition std_expr.h:962
exprt & op3()
Definition std_expr.h:950
Expression that introduces a new symbol that is equal to the operand.
Definition std_expr.h:3742
named_term_exprt(symbol_exprt symbol, exprt value)
Definition std_expr.h:3744
symbol_exprt & symbol()
Definition std_expr.h:3759
const exprt & value() const
Definition std_expr.h:3764
const symbol_exprt & symbol() const
Definition std_expr.h:3754
exprt & value()
Definition std_expr.h:3769
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean NAND.
Definition std_expr.h:2191
nand_exprt(exprt op0, exprt op1)
Definition std_expr.h:2193
nand_exprt(exprt::operandst _operands)
Definition std_expr.h:2198
The NIL expression.
Definition std_expr.h:3208
Expression to hold a nondeterministic choice.
Definition std_expr.h:292
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:315
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:296
const irep_idt & get_identifier() const
Definition std_expr.h:320
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition std_expr.h:305
Boolean NOR.
Definition std_expr.h:2336
nor_exprt(exprt op0, exprt op1)
Definition std_expr.h:2338
nor_exprt(exprt::operandst _operands)
Definition std_expr.h:2343
Boolean negation.
Definition std_expr.h:2454
not_exprt(exprt _op)
Definition std_expr.h:2456
Disequality.
Definition std_expr.h:1425
notequal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1427
An expression without operands.
Definition std_expr.h:22
exprt & op0()=delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:29
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:39
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:2270
or_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2277
or_exprt(exprt::operandst _operands)
Definition std_expr.h:2293
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2285
or_exprt(exprt op0, exprt op1)
Definition std_expr.h:2272
The plus expression Associativity is not specified.
Definition std_expr.h:1002
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition std_expr.h:1009
plus_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1004
plus_exprt(operandst _operands, typet _type)
Definition std_expr.h:1018
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition std_expr.h:574
predicate_exprt(const irep_idt &_id)
Definition std_expr.h:576
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:596
sign_exprt(exprt _op)
Definition std_expr.h:598
Struct constructor from list of elements.
Definition std_expr.h:1877
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:114
struct_exprt(operandst _operands, typet _type)
Definition std_expr.h:1879
Expression to hold a symbol (variable)
Definition std_expr.h:131
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:155
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:150
symbol_exprt & with_source_location(const exprt &other) &
Add the source location from other, if it has any.
Definition std_expr.h:182
symbol_exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition std_expr.h:166
symbol_exprt && with_source_location(source_locationt location) &&
Add the source location from location, if it is non-nil.
Definition std_expr.h:174
symbol_exprt && with_source_location(const exprt &other) &&
Add the source location from other, if it has any.
Definition std_expr.h:190
symbol_exprt(typet type)
Definition std_expr.h:134
symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:140
const irep_idt & get_identifier() const
Definition std_expr.h:160
An expression with three operands.
Definition std_expr.h:67
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:101
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition std_expr.h:70
const exprt & op3() const =delete
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
exprt & op3()=delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:91
The Boolean constant true.
Definition std_expr.h:3190
An expression denoting a type.
Definition std_expr.h:3081
type_exprt(typet type)
Definition std_expr.h:3083
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
typecast_exprt(exprt op, typet _type)
Definition std_expr.h:2075
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition std_expr.h:363
const exprt & op3() const =delete
exprt & op2()=delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:373
const exprt & op1() const =delete
exprt & op3()=delete
const exprt & op() const
Definition std_expr.h:391
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition std_expr.h:368
const exprt & op2() const =delete
exprt & op()
Definition std_expr.h:396
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:383
exprt & op1()=delete
The unary minus expression.
Definition std_expr.h:484
unary_minus_exprt(exprt _op)
Definition std_expr.h:491
unary_minus_exprt(exprt _op, typet _type)
Definition std_expr.h:486
The unary plus expression.
Definition std_expr.h:531
unary_plus_exprt(exprt op)
Definition std_expr.h:533
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:585
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition std_expr.h:587
Union constructor from single element.
Definition std_expr.h:1770
std::size_t get_component_number() const
Definition std_expr.h:1788
void set_component_number(std::size_t component_number)
Definition std_expr.h:1793
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:1783
irep_idt get_component_name() const
Definition std_expr.h:1778
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition std_expr.h:1772
Operator to update elements in structs and arrays.
Definition std_expr.h:2782
exprt & old()
Definition std_expr.h:2794
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
Definition std_expr.cpp:194
exprt::operandst & designator()
Definition std_expr.h:2808
exprt & new_value()
Definition std_expr.h:2818
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2838
const exprt & new_value() const
Definition std_expr.h:2823
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition std_expr.h:2784
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2831
const exprt & old() const
Definition std_expr.h:2799
const exprt::operandst & designator() const
Definition std_expr.h:2813
Vector constructor from list of elements.
Definition std_expr.h:1734
vector_exprt(operandst _operands, vector_typet _type)
Definition std_expr.h:1736
The vector type.
Definition std_types.h:1064
Operator to update elements in structs and arrays.
Definition std_expr.h:2598
const exprt & old() const
Definition std_expr.h:2613
const exprt & where() const
Definition std_expr.h:2623
exprt & new_value()
Definition std_expr.h:2628
exprt & where()
Definition std_expr.h:2618
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition std_expr.h:2600
const exprt & new_value() const
Definition std_expr.h:2633
exprt & old()
Definition std_expr.h:2608
Boolean XNOR.
Definition std_expr.h:2414
xnor_exprt(exprt::operandst _operands)
Definition std_expr.h:2421
xnor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2416
Boolean XOR.
Definition std_expr.h:2370
xor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2372
xor_exprt(exprt::operandst _operands)
Definition std_expr.h:2377
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:38
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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:1391
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition std_expr.h:1434
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition std_expr.h:1949
bool can_cast_expr< not_exprt >(const exprt &base)
Definition std_expr.h:2463
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1900
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition std_expr.h:1716
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition std_expr.h:2091
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition std_expr.h:3100
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1603
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition std_expr.h:1889
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition std_expr.h:556
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition std_expr.h:2384
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition std_expr.h:1121
bool can_cast_expr< if_exprt >(const exprt &base)
Definition std_expr.h:2561
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:3723
bool can_cast_expr< named_term_exprt >(const exprt &base)
Definition std_expr.h:3776
bool can_cast_expr< binding_exprt >(const exprt &base)
Definition std_expr.h:3285
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1277
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1137
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition std_expr.h:2172
bool can_cast_expr< member_designatort >(const exprt &base)
Definition std_expr.h:2746
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3610
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
Definition std_expr.h:116
const named_term_exprt & to_named_term_expr(const exprt &expr)
Cast an exprt to a named_term_exprt.
Definition std_expr.h:3792
const xnor_exprt & to_xnor_expr(const exprt &expr)
Cast an exprt to a xnor_exprt.
Definition std_expr.h:2439
bool can_cast_expr< xnor_exprt >(const exprt &base)
Definition std_expr.h:2428
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition std_expr.h:3593
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition std_expr.h:2395
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2317
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition std_expr.h:2036
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition std_expr.h:450
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition std_expr.h:605
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition std_expr.h:3517
bool can_cast_expr< type_exprt >(const exprt &base)
Definition std_expr.h:3089
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:71
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition std_expr.h:3731
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
void validate_expr(const symbol_exprt &value)
Definition std_expr.h:261
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1206
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition std_expr.h:498
bool can_cast_expr< less_than_exprt >(const exprt &base)
Definition std_expr.h:858
bool can_cast_expr< with_exprt >(const exprt &base)
Definition std_expr.h:2640
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition std_expr.h:1754
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:83
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition std_expr.h:1070
bool can_cast_expr< let_exprt >(const exprt &base)
Definition std_expr.h:3439
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition std_expr.h:1450
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition std_expr.h:1025
const nand_exprt & to_nand_expr(const exprt &expr)
Cast an exprt to a nand_exprt.
Definition std_expr.h:2210
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition std_expr.h:1587
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3455
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition std_expr.h:466
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition std_expr.h:327
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition std_expr.h:3156
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
bool can_cast_expr< index_exprt >(const exprt &base)
Definition std_expr.h:1522
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:256
const empty_union_exprt & to_empty_union_expr(const exprt &expr)
Cast an exprt to an empty_union_exprt.
Definition std_expr.h:1860
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1086
bool can_cast_expr< member_exprt >(const exprt &base)
Definition std_expr.h:3047
bool can_cast_expr< empty_union_exprt >(const exprt &base)
Definition std_expr.h:1843
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:2053
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition std_expr.h:3303
bool can_cast_expr< or_exprt >(const exprt &base)
Definition std_expr.h:2306
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition std_expr.h:1261
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2713
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1816
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition std_expr.h:3500
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:2010
bool can_cast_expr< update_exprt >(const exprt &base)
Definition std_expr.h:2848
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition std_expr.h:795
bool can_cast_expr< euclidean_mod_exprt >(const exprt &base)
Definition std_expr.h:1329
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition std_expr.h:1743
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition std_expr.h:1706
bool can_cast_expr< index_designatort >(const exprt &base)
Definition std_expr.h:2697
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2479
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2660
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1965
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition std_expr.h:540
bool can_cast_expr< and_exprt >(const exprt &base)
Definition std_expr.h:2161
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition std_expr.h:816
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2250
bool can_cast_expr< array_exprt >(const exprt &base)
Definition std_expr.h:1654
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition std_expr.h:699
bool can_cast_expr< div_exprt >(const exprt &base)
Definition std_expr.h:1190
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2865
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition std_expr.h:3217
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:514
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
Definition std_expr.h:837
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition std_expr.h:2234
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition std_expr.h:410
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
Definition std_expr.h:879
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition std_expr.h:343
bool can_cast_expr< union_exprt >(const exprt &base)
Definition std_expr.h:1800
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition std_expr.h:2762
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition std_expr.h:1993
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition std_expr.h:621
const nor_exprt & to_nor_expr(const exprt &expr)
Cast an exprt to a nor_exprt.
Definition std_expr.h:2355
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition std_expr.h:1345
Pre-defined types.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
size_t operator()(const ::symbol_exprt &sym)
Definition std_expr.h:205
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
#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