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
2164
2165template <>
2166inline bool can_cast_expr<and_exprt>(const exprt &base)
2167{
2168 return base.id() == ID_and;
2169}
2170
2177inline const and_exprt &to_and_expr(const exprt &expr)
2178{
2179 PRECONDITION(expr.id()==ID_and);
2180 return static_cast<const and_exprt &>(expr);
2181}
2182
2185{
2186 PRECONDITION(expr.id()==ID_and);
2187 return static_cast<and_exprt &>(expr);
2188}
2189
2196{
2197public:
2199 : multi_ary_exprt(std::move(op0), ID_nand, std::move(op1), bool_typet())
2200 {
2201 }
2202
2207};
2208
2215inline const nand_exprt &to_nand_expr(const exprt &expr)
2216{
2217 PRECONDITION(expr.id() == ID_nand);
2218 return static_cast<const nand_exprt &>(expr);
2219}
2220
2223{
2224 PRECONDITION(expr.id() == ID_nand);
2225 return static_cast<nand_exprt &>(expr);
2226}
2227
2230{
2231public:
2233 : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2234 {
2235 }
2236};
2237
2238template <>
2239inline bool can_cast_expr<implies_exprt>(const exprt &base)
2240{
2241 return base.id() == ID_implies;
2242}
2243
2244inline void validate_expr(const implies_exprt &value)
2245{
2246 validate_operands(value, 2, "Implies must have two operands");
2247}
2248
2255inline const implies_exprt &to_implies_expr(const exprt &expr)
2256{
2257 PRECONDITION(expr.id()==ID_implies);
2258 const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2260 return ret;
2261}
2262
2265{
2266 PRECONDITION(expr.id()==ID_implies);
2267 implies_exprt &ret = static_cast<implies_exprt &>(expr);
2269 return ret;
2270}
2271
2272
2275{
2276public:
2278 : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2279 {
2280 }
2281
2284 ID_or,
2285 {std::move(op0), std::move(op1), std::move(op2)},
2286 bool_typet())
2287 {
2288 }
2289
2292 ID_or,
2293 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2294 bool_typet())
2295 {
2296 }
2297
2302};
2303
2307
2309
2310template <>
2311inline bool can_cast_expr<or_exprt>(const exprt &base)
2312{
2313 return base.id() == ID_or;
2314}
2315
2322inline const or_exprt &to_or_expr(const exprt &expr)
2323{
2324 PRECONDITION(expr.id()==ID_or);
2325 return static_cast<const or_exprt &>(expr);
2326}
2327
2330{
2331 PRECONDITION(expr.id()==ID_or);
2332 return static_cast<or_exprt &>(expr);
2333}
2334
2341{
2342public:
2344 : multi_ary_exprt(std::move(op0), ID_nor, std::move(op1), bool_typet())
2345 {
2346 }
2347
2352};
2353
2360inline const nor_exprt &to_nor_expr(const exprt &expr)
2361{
2362 PRECONDITION(expr.id() == ID_nor);
2363 return static_cast<const nor_exprt &>(expr);
2364}
2365
2368{
2369 PRECONDITION(expr.id() == ID_nor);
2370 return static_cast<nor_exprt &>(expr);
2371}
2372
2375{
2376public:
2378 : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2379 {
2380 }
2381
2386};
2387
2388template <>
2389inline bool can_cast_expr<xor_exprt>(const exprt &base)
2390{
2391 return base.id() == ID_xor;
2392}
2393
2400inline const xor_exprt &to_xor_expr(const exprt &expr)
2401{
2402 PRECONDITION(expr.id()==ID_xor);
2403 return static_cast<const xor_exprt &>(expr);
2404}
2405
2408{
2409 PRECONDITION(expr.id()==ID_xor);
2410 return static_cast<xor_exprt &>(expr);
2411}
2412
2419{
2420public:
2422 : multi_ary_exprt(std::move(_op0), ID_xnor, std::move(_op1), bool_typet())
2423 {
2424 }
2425
2430};
2431
2432template <>
2433inline bool can_cast_expr<xnor_exprt>(const exprt &base)
2434{
2435 return base.id() == ID_xnor;
2436}
2437
2444inline const xnor_exprt &to_xnor_expr(const exprt &expr)
2445{
2446 PRECONDITION(expr.id() == ID_xnor);
2447 return static_cast<const xnor_exprt &>(expr);
2448}
2449
2452{
2453 PRECONDITION(expr.id() == ID_xnor);
2454 return static_cast<xnor_exprt &>(expr);
2455}
2456
2459{
2460public:
2462 {
2463 PRECONDITION(as_const(*this).op().is_boolean());
2464 }
2465};
2466
2467template <>
2468inline bool can_cast_expr<not_exprt>(const exprt &base)
2469{
2470 return base.id() == ID_not;
2471}
2472
2473inline void validate_expr(const not_exprt &value)
2474{
2475 validate_operands(value, 1, "Not must have one operand");
2476}
2477
2484inline const not_exprt &to_not_expr(const exprt &expr)
2485{
2486 PRECONDITION(expr.id()==ID_not);
2487 not_exprt::check(expr);
2488 return static_cast<const not_exprt &>(expr);
2489}
2490
2493{
2494 PRECONDITION(expr.id()==ID_not);
2495 not_exprt::check(expr);
2496 return static_cast<not_exprt &>(expr);
2497}
2498
2499
2502{
2503public:
2505 : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2506 {
2507 }
2508
2510 : ternary_exprt(
2511 ID_if,
2512 std::move(cond),
2513 std::move(t),
2514 std::move(f),
2515 std::move(type))
2516 {
2517 }
2518
2520 {
2521 return op0();
2522 }
2523
2524 const exprt &cond() const
2525 {
2526 return op0();
2527 }
2528
2530 {
2531 return op1();
2532 }
2533
2534 const exprt &true_case() const
2535 {
2536 return op1();
2537 }
2538
2540 {
2541 return op2();
2542 }
2543
2544 const exprt &false_case() const
2545 {
2546 return op2();
2547 }
2548
2549 static void check(
2550 const exprt &expr,
2552 {
2553 ternary_exprt::check(expr, vm);
2554 }
2555
2556 static void validate(
2557 const exprt &expr,
2558 const namespacet &ns,
2560 {
2561 ternary_exprt::validate(expr, ns, vm);
2562 }
2563};
2564
2565template <>
2566inline bool can_cast_expr<if_exprt>(const exprt &base)
2567{
2568 return base.id() == ID_if;
2569}
2570
2571inline void validate_expr(const if_exprt &value)
2572{
2573 validate_operands(value, 3, "If-then-else must have three operands");
2574}
2575
2582inline const if_exprt &to_if_expr(const exprt &expr)
2583{
2584 PRECONDITION(expr.id()==ID_if);
2585 const if_exprt &ret = static_cast<const if_exprt &>(expr);
2587 return ret;
2588}
2589
2592{
2593 PRECONDITION(expr.id()==ID_if);
2594 if_exprt &ret = static_cast<if_exprt &>(expr);
2596 return ret;
2597}
2598
2603{
2604public:
2607 ID_with,
2608 _old.type(),
2609 {_old, std::move(_where), std::move(_new_value)})
2610 {
2611 }
2612
2614 {
2615 return op0();
2616 }
2617
2618 const exprt &old() const
2619 {
2620 return op0();
2621 }
2622
2624 {
2625 return op1();
2626 }
2627
2628 const exprt &where() const
2629 {
2630 return op1();
2631 }
2632
2634 {
2635 return op2();
2636 }
2637
2638 const exprt &new_value() const
2639 {
2640 return op2();
2641 }
2642};
2643
2644template <>
2645inline bool can_cast_expr<with_exprt>(const exprt &base)
2646{
2647 return base.id() == ID_with;
2648}
2649
2650inline void validate_expr(const with_exprt &value)
2651{
2652 validate_operands(value, 3, "array/structure update must have 3 operands");
2653}
2654
2661inline const with_exprt &to_with_expr(const exprt &expr)
2662{
2663 PRECONDITION(expr.id()==ID_with);
2664 const with_exprt &ret = static_cast<const with_exprt &>(expr);
2666 return ret;
2667}
2668
2671{
2672 PRECONDITION(expr.id()==ID_with);
2673 with_exprt &ret = static_cast<with_exprt &>(expr);
2675 return ret;
2676}
2677
2679{
2680public:
2683 {
2684 }
2685
2686 const exprt &index() const
2687 {
2688 return op0();
2689 }
2690
2692 {
2693 return op0();
2694 }
2695};
2696
2697template <>
2699{
2700 return base.id() == ID_index_designator;
2701}
2702
2703inline void validate_expr(const index_designatort &value)
2704{
2705 validate_operands(value, 1, "Index designator must have one operand");
2706}
2707
2715{
2717 const index_designatort &ret = static_cast<const index_designatort &>(expr);
2719 return ret;
2720}
2721
2724{
2726 index_designatort &ret = static_cast<index_designatort &>(expr);
2728 return ret;
2729}
2730
2732{
2733public:
2739
2741 {
2742 return get(ID_component_name);
2743 }
2744};
2745
2746template <>
2748{
2749 return base.id() == ID_member_designator;
2750}
2751
2752inline void validate_expr(const member_designatort &value)
2753{
2754 validate_operands(value, 0, "Member designator must not have operands");
2755}
2756
2764{
2766 const member_designatort &ret = static_cast<const member_designatort &>(expr);
2768 return ret;
2769}
2770
2773{
2775 member_designatort &ret = static_cast<member_designatort &>(expr);
2777 return ret;
2778}
2779
2780
2783{
2784public:
2786 : ternary_exprt(
2787 ID_update,
2788 _old,
2789 std::move(_designator),
2790 std::move(_new_value),
2791 _old.type())
2792 {
2793 }
2794
2796 {
2797 return op0();
2798 }
2799
2800 const exprt &old() const
2801 {
2802 return op0();
2803 }
2804
2805 // the designator operands are either
2806 // 1) member_designator or
2807 // 2) index_designator
2808 // as defined above
2810 {
2811 return op1().operands();
2812 }
2813
2815 {
2816 return op1().operands();
2817 }
2818
2820 {
2821 return op2();
2822 }
2823
2824 const exprt &new_value() const
2825 {
2826 return op2();
2827 }
2828
2830 with_exprt make_with_expr() const;
2831
2832 static void check(
2833 const exprt &expr,
2835 {
2836 ternary_exprt::check(expr, vm);
2837 }
2838
2839 static void validate(
2840 const exprt &expr,
2841 const namespacet &ns,
2843 {
2844 ternary_exprt::validate(expr, ns, vm);
2845 }
2846};
2847
2848template <>
2849inline bool can_cast_expr<update_exprt>(const exprt &base)
2850{
2851 return base.id() == ID_update;
2852}
2853
2854inline void validate_expr(const update_exprt &value)
2855{
2857 value, 3, "Array/structure update must have three operands");
2858}
2859
2866inline const update_exprt &to_update_expr(const exprt &expr)
2867{
2868 PRECONDITION(expr.id()==ID_update);
2869 const update_exprt &ret = static_cast<const update_exprt &>(expr);
2871 return ret;
2872}
2873
2876{
2877 PRECONDITION(expr.id()==ID_update);
2878 update_exprt &ret = static_cast<update_exprt &>(expr);
2880 return ret;
2881}
2882
2883
2884#if 0
2887{
2888public:
2890 const exprt &_array,
2891 const exprt &_index,
2892 const exprt &_new_value):
2894 {
2895 add_to_operands(_array, _index, _new_value);
2896 }
2897
2899 {
2900 operands().resize(3);
2901 }
2902
2903 exprt &array()
2904 {
2905 return op0();
2906 }
2907
2908 const exprt &array() const
2909 {
2910 return op0();
2911 }
2912
2913 exprt &index()
2914 {
2915 return op1();
2916 }
2917
2918 const exprt &index() const
2919 {
2920 return op1();
2921 }
2922
2923 exprt &new_value()
2924 {
2925 return op2();
2926 }
2927
2928 const exprt &new_value() const
2929 {
2930 return op2();
2931 }
2932};
2933
2934template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2935{
2936 return base.id()==ID_array_update;
2937}
2938
2939inline void validate_expr(const array_update_exprt &value)
2940{
2941 validate_operands(value, 3, "Array update must have three operands");
2942}
2943
2950inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2951{
2953 const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2955 return ret;
2956}
2957
2960{
2962 array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2964 return ret;
2965}
2966
2967#endif
2968
2969
2972{
2973public:
2974 member_exprt(exprt op, const irep_idt &component_name, typet _type)
2975 : unary_exprt(ID_member, std::move(op), std::move(_type))
2976 {
2977 const auto &compound_type_id = compound().type().id();
2981 set_component_name(component_name);
2982 }
2983
2993
2995 {
2996 return get(ID_component_name);
2997 }
2998
2999 void set_component_name(const irep_idt &component_name)
3000 {
3001 set(ID_component_name, component_name);
3002 }
3003
3004 std::size_t get_component_number() const
3005 {
3007 }
3008
3009 // will go away, use compound()
3010 const exprt &struct_op() const
3011 {
3012 return op0();
3013 }
3014
3015 // will go away, use compound()
3017 {
3018 return op0();
3019 }
3020
3021 const exprt &compound() const
3022 {
3023 return op0();
3024 }
3025
3027 {
3028 return op0();
3029 }
3030
3031 static void check(
3032 const exprt &expr,
3034 {
3035 DATA_CHECK(
3036 vm,
3037 expr.operands().size() == 1,
3038 "member expression must have one operand");
3039 }
3040
3041 static void validate(
3042 const exprt &expr,
3043 const namespacet &ns,
3045};
3046
3047template <>
3048inline bool can_cast_expr<member_exprt>(const exprt &base)
3049{
3050 return base.id() == ID_member;
3051}
3052
3053inline void validate_expr(const member_exprt &value)
3054{
3055 validate_operands(value, 1, "Extract member must have one operand");
3056}
3057
3064inline const member_exprt &to_member_expr(const exprt &expr)
3065{
3066 PRECONDITION(expr.id()==ID_member);
3067 member_exprt::check(expr);
3068 return static_cast<const member_exprt &>(expr);
3069}
3070
3073{
3074 PRECONDITION(expr.id()==ID_member);
3075 member_exprt::check(expr);
3076 return static_cast<member_exprt &>(expr);
3077}
3078
3079
3082{
3083public:
3085 {
3086 }
3087};
3088
3089template <>
3090inline bool can_cast_expr<type_exprt>(const exprt &base)
3091{
3092 return base.id() == ID_type;
3093}
3094
3101inline const type_exprt &to_type_expr(const exprt &expr)
3102{
3104 type_exprt::check(expr);
3105 return static_cast<const type_exprt &>(expr);
3106}
3107
3110{
3112 type_exprt::check(expr);
3113 return static_cast<type_exprt &>(expr);
3114}
3115
3118{
3119public:
3120 constant_exprt(const irep_idt &_value, typet _type)
3121 : nullary_exprt(ID_constant, std::move(_type))
3122 {
3123 set_value(_value);
3124 }
3125
3126 const irep_idt &get_value() const
3127 {
3128 return get(ID_value);
3129 }
3130
3131 void set_value(const irep_idt &value)
3132 {
3133 set(ID_value, value);
3134 }
3135
3136 bool value_is_zero_string() const;
3137
3141 bool is_null_pointer() const;
3142
3143 static void check(
3144 const exprt &expr,
3146
3147 static void validate(
3148 const exprt &expr,
3149 const namespacet &,
3151 {
3152 check(expr, vm);
3153 }
3154};
3155
3156template <>
3157inline bool can_cast_expr<constant_exprt>(const exprt &base)
3158{
3159 return base.is_constant();
3160}
3161
3162inline void validate_expr(const constant_exprt &value)
3163{
3164 validate_operands(value, 0, "Constants must not have operands");
3165}
3166
3173inline const constant_exprt &to_constant_expr(const exprt &expr)
3174{
3175 PRECONDITION(expr.is_constant());
3177 return static_cast<const constant_exprt &>(expr);
3178}
3179
3182{
3183 PRECONDITION(expr.is_constant());
3185 return static_cast<constant_exprt &>(expr);
3186}
3187
3188
3191{
3192public:
3196};
3197
3200{
3201public:
3205};
3206
3209{
3210public:
3215};
3216
3217template <>
3218inline bool can_cast_expr<nil_exprt>(const exprt &base)
3219{
3220 return base.id() == ID_nil;
3221}
3222
3225{
3226public:
3227 explicit infinity_exprt(typet _type)
3228 : nullary_exprt(ID_infinity, std::move(_type))
3229 {
3230 }
3231};
3232
3235{
3236public:
3237 using variablest = std::vector<symbol_exprt>;
3238
3241 irep_idt _id,
3242 const variablest &_variables,
3243 exprt _where,
3244 typet _type)
3245 : binary_exprt(
3247 ID_tuple,
3249 typet(ID_tuple)),
3250 _id,
3251 std::move(_where),
3252 std::move(_type))
3253 {
3254 }
3255
3257 {
3258 return (variablest &)to_multi_ary_expr(op0()).operands();
3259 }
3260
3261 const variablest &variables() const
3262 {
3263 return (variablest &)to_multi_ary_expr(op0()).operands();
3264 }
3265
3267 {
3268 return op1();
3269 }
3270
3271 const exprt &where() const
3272 {
3273 return op1();
3274 }
3275
3278 exprt instantiate(const exprt::operandst &) const;
3279
3282 exprt instantiate(const variablest &) const;
3283};
3284
3285template <>
3286inline bool can_cast_expr<binding_exprt>(const exprt &base)
3287{
3288 return base.id() == ID_forall || base.id() == ID_exists ||
3289 base.id() == ID_lambda || base.id() == ID_array_comprehension;
3290}
3291
3293{
3295 binding_expr, 2, "Binding expressions must have two operands");
3296}
3297
3304inline const binding_exprt &to_binding_expr(const exprt &expr)
3305{
3307 expr.id() == ID_forall || expr.id() == ID_exists ||
3308 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3309 const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
3311 return ret;
3312}
3313
3321{
3323 expr.id() == ID_forall || expr.id() == ID_exists ||
3324 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3325 binding_exprt &ret = static_cast<binding_exprt &>(expr);
3327 return ret;
3328}
3329
3332{
3333public:
3337 const exprt &where)
3338 : binary_exprt(
3341 std::move(variables),
3342 where,
3343 where.type()),
3344 ID_let,
3346 where.type())
3347 {
3348 PRECONDITION(this->variables().size() == this->values().size());
3349 }
3350
3353 : let_exprt(
3355 operandst{std::move(value)},
3356 where)
3357 {
3358 }
3359
3361 {
3362 return static_cast<binding_exprt &>(op0());
3363 }
3364
3365 const binding_exprt &binding() const
3366 {
3367 return static_cast<const binding_exprt &>(op0());
3368 }
3369
3372 {
3373 auto &variables = binding().variables();
3374 PRECONDITION(variables.size() == 1);
3375 return variables.front();
3376 }
3377
3379 const symbol_exprt &symbol() const
3380 {
3381 const auto &variables = binding().variables();
3382 PRECONDITION(variables.size() == 1);
3383 return variables.front();
3384 }
3385
3388 {
3389 auto &values = this->values();
3390 PRECONDITION(values.size() == 1);
3391 return values.front();
3392 }
3393
3395 const exprt &value() const
3396 {
3397 const auto &values = this->values();
3398 PRECONDITION(values.size() == 1);
3399 return values.front();
3400 }
3401
3403 {
3404 return static_cast<multi_ary_exprt &>(op1()).operands();
3405 }
3406
3407 const operandst &values() const
3408 {
3409 return static_cast<const multi_ary_exprt &>(op1()).operands();
3410 }
3411
3414 {
3415 return binding().variables();
3416 }
3417
3420 {
3421 return binding().variables();
3422 }
3423
3426 {
3427 return binding().where();
3428 }
3429
3431 const exprt &where() const
3432 {
3433 return binding().where();
3434 }
3435
3436 static void validate(const exprt &, validation_modet);
3437};
3438
3439template <>
3440inline bool can_cast_expr<let_exprt>(const exprt &base)
3441{
3442 return base.id() == ID_let;
3443}
3444
3446{
3447 validate_operands(let_expr, 2, "Let must have two operands");
3448}
3449
3456inline const let_exprt &to_let_expr(const exprt &expr)
3457{
3458 PRECONDITION(expr.id()==ID_let);
3459 const let_exprt &ret = static_cast<const let_exprt &>(expr);
3461 return ret;
3462}
3463
3466{
3467 PRECONDITION(expr.id()==ID_let);
3468 let_exprt &ret = static_cast<let_exprt &>(expr);
3470 return ret;
3471}
3472
3473
3478{
3479public:
3481 : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3482 {
3483 }
3484
3488 void add_case(const exprt &condition, const exprt &value)
3489 {
3490 PRECONDITION(condition.is_boolean());
3491 operands().reserve(operands().size() + 2);
3492 operands().push_back(condition);
3493 operands().push_back(value);
3494 }
3495
3496 // a lowering to nested if_exprt
3497 exprt lower() const;
3498};
3499
3500template <>
3501inline bool can_cast_expr<cond_exprt>(const exprt &base)
3502{
3503 return base.id() == ID_cond;
3504}
3505
3506inline void validate_expr(const cond_exprt &value)
3507{
3509 value.operands().size() % 2 == 0, "cond must have even number of operands");
3510}
3511
3518inline const cond_exprt &to_cond_expr(const exprt &expr)
3519{
3520 PRECONDITION(expr.id() == ID_cond);
3521 const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3523 return ret;
3524}
3525
3528{
3529 PRECONDITION(expr.id() == ID_cond);
3530 cond_exprt &ret = static_cast<cond_exprt &>(expr);
3532 return ret;
3533}
3534
3544{
3545public:
3548 exprt body,
3549 array_typet _type)
3550 : binding_exprt(
3552 {std::move(arg)},
3553 std::move(body),
3554 std::move(_type))
3555 {
3556 }
3557
3558 const array_typet &type() const
3559 {
3560 return static_cast<const array_typet &>(binary_exprt::type());
3561 }
3562
3564 {
3565 return static_cast<array_typet &>(binary_exprt::type());
3566 }
3567
3568 const symbol_exprt &arg() const
3569 {
3570 auto &variables = this->variables();
3571 PRECONDITION(variables.size() == 1);
3572 return variables[0];
3573 }
3574
3576 {
3577 auto &variables = this->variables();
3578 PRECONDITION(variables.size() == 1);
3579 return variables[0];
3580 }
3581
3582 const exprt &body() const
3583 {
3584 return where();
3585 }
3586
3588 {
3589 return where();
3590 }
3591};
3592
3593template <>
3595{
3596 return base.id() == ID_array_comprehension;
3597}
3598
3600{
3601 validate_operands(value, 2, "'Array comprehension' must have two operands");
3602}
3603
3610inline const array_comprehension_exprt &
3612{
3615 static_cast<const array_comprehension_exprt &>(expr);
3617 return ret;
3618}
3619
3629
3630inline void validate_expr(const class class_method_descriptor_exprt &value);
3631
3634{
3635public:
3651 typet _type,
3655 : nullary_exprt(ID_virtual_function, std::move(_type))
3656 {
3659 set(ID_C_class, std::move(class_id));
3660 set(ID_C_base_name, std::move(base_method_name));
3661 set(ID_identifier, std::move(id));
3662 validate_expr(*this);
3663 }
3664
3672 {
3673 return get(ID_component_name);
3674 }
3675
3679 const irep_idt &class_id() const
3680 {
3681 return get(ID_C_class);
3682 }
3683
3687 {
3688 return get(ID_C_base_name);
3689 }
3690
3695 {
3696 return get(ID_identifier);
3697 }
3698};
3699
3700inline void validate_expr(const class class_method_descriptor_exprt &value)
3701{
3702 validate_operands(value, 0, "class method descriptor must not have operands");
3704 !value.mangled_method_name().empty(),
3705 "class method descriptor must have a mangled method name.");
3707 !value.class_id().empty(), "class method descriptor must have a class id.");
3709 !value.base_method_name().empty(),
3710 "class method descriptor must have a base method name.");
3712 value.get_identifier() == id2string(value.class_id()) + "." +
3714 "class method descriptor must have an identifier in the expected format.");
3715}
3716
3723inline const class_method_descriptor_exprt &
3725{
3728 return static_cast<const class_method_descriptor_exprt &>(expr);
3729}
3730
3731template <>
3733{
3734 return base.id() == ID_virtual_function;
3735}
3736
3743{
3744public:
3746 : binary_exprt(
3747 std::move(symbol),
3749 value, // not moved, for type
3750 value.type())
3751 {
3752 PRECONDITION(symbol.type() == type());
3753 }
3754
3755 const symbol_exprt &symbol() const
3756 {
3757 return static_cast<const symbol_exprt &>(op0());
3758 }
3759
3761 {
3762 return static_cast<symbol_exprt &>(op0());
3763 }
3764
3765 const exprt &value() const
3766 {
3767 return op1();
3768 }
3769
3771 {
3772 return op1();
3773 }
3774};
3775
3776template <>
3778{
3779 return base.id() == ID_named_term;
3780}
3781
3782inline void validate_expr(const named_term_exprt &value)
3783{
3784 validate_operands(value, 2, "'named term' must have two operands");
3785}
3786
3794{
3795 PRECONDITION(expr.id() == ID_named_term);
3796 const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
3798 return ret;
3799}
3800
3803{
3804 PRECONDITION(expr.id() == ID_named_term);
3805 named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
3807 return ret;
3808}
3809
3810#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:3544
const array_typet & type() const
Definition std_expr.h:3558
const symbol_exprt & arg() const
Definition std_expr.h:3568
const exprt & body() const
Definition std_expr.h:3582
array_typet & type()
Definition std_expr.h:3563
symbol_exprt & arg()
Definition std_expr.h:3575
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition std_expr.h:3546
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:3235
const variablest & variables() const
Definition std_expr.h:3261
const exprt & where() const
Definition std_expr.h:3271
exprt & where()
Definition std_expr.h:3266
variablest & variables()
Definition std_expr.h:3256
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition std_expr.h:3240
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:250
std::vector< symbol_exprt > variablest
Definition std_expr.h:3237
The Boolean type.
Definition std_types.h:36
An expression describing a method on a class.
Definition std_expr.h:3634
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:3686
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition std_expr.h:3671
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:3694
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition std_expr.h:3650
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:3679
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:3478
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition std_expr.h:3488
cond_exprt(operandst _operands, typet _type)
Definition std_expr.h:3480
exprt lower() const
Definition std_expr.cpp:289
A constant literal expression.
Definition std_expr.h:3118
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:3147
const irep_idt & get_value() const
Definition std_expr.h:3126
bool value_is_zero_string() const
Definition std_expr.cpp:19
constant_exprt(const irep_idt &_value, typet _type)
Definition std_expr.h:3120
void set_value(const irep_idt &value)
Definition std_expr.h:3131
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:3200
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:2502
const exprt & false_case() const
Definition std_expr.h:2544
exprt & cond()
Definition std_expr.h:2519
const exprt & cond() const
Definition std_expr.h:2524
if_exprt(exprt cond, const exprt &t, exprt f)
Definition std_expr.h:2504
const exprt & true_case() const
Definition std_expr.h:2534
exprt & false_case()
Definition std_expr.h:2539
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition std_expr.h:2509
exprt & true_case()
Definition std_expr.h:2529
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2549
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2556
Boolean implication.
Definition std_expr.h:2230
implies_exprt(exprt op0, exprt op1)
Definition std_expr.h:2232
const exprt & index() const
Definition std_expr.h:2686
index_designatort(exprt _index)
Definition std_expr.h:2681
exprt & index()
Definition std_expr.h:2691
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:3225
infinity_exprt(typet _type)
Definition std_expr.h:3227
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:3332
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3413
const binding_exprt & binding() const
Definition std_expr.h:3365
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition std_expr.h:3419
operandst & values()
Definition std_expr.h:3402
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition std_expr.h:3352
const exprt & where() const
convenience accessor for binding().where()
Definition std_expr.h:3431
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:193
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition std_expr.h:3379
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition std_expr.h:3334
exprt & value()
convenience accessor for the value of a single binding
Definition std_expr.h:3387
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3425
binding_exprt & binding()
Definition std_expr.h:3360
const operandst & values() const
Definition std_expr.h:3407
const exprt & value() const
convenience accessor for the value of a single binding
Definition std_expr.h:3395
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition std_expr.h:3371
irep_idt get_component_name() const
Definition std_expr.h:2740
member_designatort(const irep_idt &_component_name)
Definition std_expr.h:2734
Extract member of struct or union.
Definition std_expr.h:2972
const exprt & compound() const
Definition std_expr.h:3021
exprt & struct_op()
Definition std_expr.h:3016
const exprt & struct_op() const
Definition std_expr.h:3010
irep_idt get_component_name() const
Definition std_expr.h:2994
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:2999
exprt & compound()
Definition std_expr.h:3026
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:158
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:3031
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition std_expr.h:2974
std::size_t get_component_number() const
Definition std_expr.h:3004
member_exprt(exprt op, const struct_typet::componentt &c)
Definition std_expr.h:2984
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:3743
named_term_exprt(symbol_exprt symbol, exprt value)
Definition std_expr.h:3745
symbol_exprt & symbol()
Definition std_expr.h:3760
const exprt & value() const
Definition std_expr.h:3765
const symbol_exprt & symbol() const
Definition std_expr.h:3755
exprt & value()
Definition std_expr.h:3770
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:2196
nand_exprt(exprt op0, exprt op1)
Definition std_expr.h:2198
nand_exprt(exprt::operandst _operands)
Definition std_expr.h:2203
The NIL expression.
Definition std_expr.h:3209
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:2341
nor_exprt(exprt op0, exprt op1)
Definition std_expr.h:2343
nor_exprt(exprt::operandst _operands)
Definition std_expr.h:2348
Boolean negation.
Definition std_expr.h:2459
not_exprt(exprt _op)
Definition std_expr.h:2461
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:2275
or_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2282
or_exprt(exprt::operandst _operands)
Definition std_expr.h:2298
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2290
or_exprt(exprt op0, exprt op1)
Definition std_expr.h:2277
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:139
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:3191
An expression denoting a type.
Definition std_expr.h:3082
type_exprt(typet type)
Definition std_expr.h:3084
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:2783
exprt & old()
Definition std_expr.h:2795
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
Definition std_expr.cpp:219
exprt::operandst & designator()
Definition std_expr.h:2809
exprt & new_value()
Definition std_expr.h:2819
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2839
const exprt & new_value() const
Definition std_expr.h:2824
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition std_expr.h:2785
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2832
const exprt & old() const
Definition std_expr.h:2800
const exprt::operandst & designator() const
Definition std_expr.h:2814
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:2603
const exprt & old() const
Definition std_expr.h:2618
const exprt & where() const
Definition std_expr.h:2628
exprt & new_value()
Definition std_expr.h:2633
exprt & where()
Definition std_expr.h:2623
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition std_expr.h:2605
const exprt & new_value() const
Definition std_expr.h:2638
exprt & old()
Definition std_expr.h:2613
Boolean XNOR.
Definition std_expr.h:2419
xnor_exprt(exprt::operandst _operands)
Definition std_expr.h:2426
xnor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2421
Boolean XOR.
Definition std_expr.h:2375
xor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2377
xor_exprt(exprt::operandst _operands)
Definition std_expr.h:2382
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:2468
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:3101
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:2389
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:2566
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:3724
bool can_cast_expr< named_term_exprt >(const exprt &base)
Definition std_expr.h:3777
bool can_cast_expr< binding_exprt >(const exprt &base)
Definition std_expr.h:3286
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:2177
bool can_cast_expr< member_designatort >(const exprt &base)
Definition std_expr.h:2747
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3611
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:3793
const xnor_exprt & to_xnor_expr(const exprt &expr)
Cast an exprt to a xnor_exprt.
Definition std_expr.h:2444
bool can_cast_expr< xnor_exprt >(const exprt &base)
Definition std_expr.h:2433
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition std_expr.h:3594
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition std_expr.h:2400
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2322
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:3518
bool can_cast_expr< type_exprt >(const exprt &base)
Definition std_expr.h:3090
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:3732
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:2645
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:106
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:3440
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:2215
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:3456
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:3157
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
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:3048
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:3304
bool can_cast_expr< or_exprt >(const exprt &base)
Definition std_expr.h:2311
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:2714
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:3501
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:2849
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:3173
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:2698
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2484
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:2661
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:2166
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:2255
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:2866
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition std_expr.h:3218
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:2239
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:2763
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:2360
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