cprover
Loading...
Searching...
No Matches
std_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_STD_EXPR_H
11#define CPROVER_UTIL_STD_EXPR_H
12
15
16#include "expr_cast.h"
17#include "invariant.h"
18#include "std_types.h"
19
22{
23public:
24 nullary_exprt(const irep_idt &_id, typet _type)
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:
134 explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type))
135 {
136 }
137
140 symbol_exprt(const irep_idt &identifier, typet type)
141 : nullary_exprt(ID_symbol, std::move(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 {
226 return get_bool(ID_C_static_lifetime);
227 }
228
230 {
231 return set(ID_C_static_lifetime, true);
232 }
233
235 {
236 remove(ID_C_static_lifetime);
237 }
238
239 bool is_thread_local() const
240 {
241 return get_bool(ID_C_thread_local);
242 }
243
245 {
246 return set(ID_C_thread_local, true);
247 }
248
250 {
251 remove(ID_C_thread_local);
252 }
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);
276 validate_expr(ret);
277 return ret;
278}
279
282{
283 PRECONDITION(expr.id()==ID_symbol);
284 symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
285 validate_expr(ret);
286 return ret;
287}
288
289
292{
293public:
297 : nullary_exprt(ID_nondet_symbol, std::move(type))
298 {
299 set_identifier(identifier);
300 }
301
306 irep_idt identifier,
307 typet type,
308 source_locationt location)
309 : nullary_exprt(ID_nondet_symbol, std::move(type))
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{
345 PRECONDITION(expr.id()==ID_nondet_symbol);
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:
363 unary_exprt(const irep_idt &_id, const exprt &_op)
364 : expr_protectedt(_id, _op.type(), {_op})
365 {
366 }
367
368 unary_exprt(const irep_idt &_id, exprt _op, typet _type)
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:
444 explicit abs_exprt(exprt _op) : unary_exprt(ID_abs, std::move(_op))
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
492 : unary_exprt(ID_unary_minus, std::move(_op))
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{
516 PRECONDITION(expr.id()==ID_unary_minus);
518 return static_cast<const unary_minus_exprt &>(expr);
519}
520
523{
524 PRECONDITION(expr.id()==ID_unary_minus);
526 return static_cast<unary_minus_exprt &>(expr);
527}
528
531{
532public:
534 : unary_exprt(ID_unary_plus, std::move(op))
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:
598 explicit sign_exprt(exprt _op)
599 : unary_predicate_exprt(ID_sign, std::move(_op))
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:
640 binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
641 : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
642 {
643 }
644
645 binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
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:
765 : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
766 {
767 }
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:
810 : binary_relation_exprt{std::move(_lhs), ID_gt, std::move(_rhs)}
811 {
812 }
813};
814
815template <>
817{
818 return base.id() == ID_gt;
819}
820
821inline void validate_expr(const greater_than_exprt &value)
822{
824}
825
828{
829public:
831 : binary_relation_exprt{std::move(_lhs), ID_ge, std::move(_rhs)}
832 {
833 }
834};
835
836template <>
838{
839 return base.id() == ID_ge;
840}
841
843{
845}
846
849{
850public:
852 : binary_relation_exprt{std::move(_lhs), ID_lt, std::move(_rhs)}
853 {
854 }
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
870{
871public:
873 : binary_relation_exprt{std::move(_lhs), ID_le, std::move(_rhs)}
874 {
875 }
876};
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:
914 multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
915 : expr_protectedt(_id, std::move(_type))
916 {
917 operands() = std::move(_operands);
918 }
919
920 multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
921 : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
922 {
923 }
924
925 multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
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
1009 plus_exprt(exprt _lhs, exprt _rhs, typet _type)
1011 std::move(_lhs),
1012 ID_plus,
1013 std::move(_rhs),
1014 std::move(_type))
1015 {
1016 }
1017
1018 plus_exprt(operandst _operands, typet _type)
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);
1045 validate_expr(ret);
1046 return ret;
1047}
1048
1051{
1052 PRECONDITION(expr.id()==ID_plus);
1053 plus_exprt &ret = static_cast<plus_exprt &>(expr);
1054 validate_expr(ret);
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);
1090 validate_expr(ret);
1091 return ret;
1092}
1093
1096{
1097 PRECONDITION(expr.id()==ID_minus);
1098 minus_exprt &ret = static_cast<minus_exprt &>(expr);
1099 validate_expr(ret);
1100 return ret;
1101}
1102
1103
1107{
1108public:
1110 : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
1111 {
1112 }
1113
1115 : multi_ary_exprt(ID_mult, std::move(factors), std::move(type))
1116 {
1117 }
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);
1141 validate_expr(ret);
1142 return ret;
1143}
1144
1147{
1148 PRECONDITION(expr.id()==ID_mult);
1149 mult_exprt &ret = static_cast<mult_exprt &>(expr);
1150 validate_expr(ret);
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);
1210 validate_expr(ret);
1211 return ret;
1212}
1213
1216{
1217 PRECONDITION(expr.id()==ID_div);
1218 div_exprt &ret = static_cast<div_exprt &>(expr);
1219 validate_expr(ret);
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);
1281 validate_expr(ret);
1282 return ret;
1283}
1284
1287{
1288 PRECONDITION(expr.id()==ID_mod);
1289 mod_exprt &ret = static_cast<mod_exprt &>(expr);
1290 validate_expr(ret);
1291 return ret;
1292}
1293
1296{
1297public:
1299 : binary_exprt(std::move(_lhs), ID_euclidean_mod, std::move(_rhs))
1300 {
1301 }
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);
1350 validate_expr(ret);
1351 return ret;
1352}
1353
1356{
1357 PRECONDITION(expr.id() == ID_euclidean_mod);
1358 euclidean_mod_exprt &ret = static_cast<euclidean_mod_exprt &>(expr);
1359 validate_expr(ret);
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:
1428 : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1429 {
1430 }
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);
1454 validate_expr(ret);
1455 return ret;
1456}
1457
1460{
1461 PRECONDITION(expr.id()==ID_notequal);
1462 notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1463 validate_expr(ret);
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.
1476 index_exprt(const exprt &_array, exprt _index)
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
1488 index_exprt(exprt _array, exprt _index, typet _type)
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);
1542 validate_expr(ret);
1543 return ret;
1544}
1545
1548{
1549 PRECONDITION(expr.id()==ID_index);
1550 index_exprt &ret = static_cast<index_exprt &>(expr);
1551 validate_expr(ret);
1552 return ret;
1553}
1554
1555
1558{
1559public:
1560 explicit array_of_exprt(exprt _what, array_typet _type)
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);
1720 validate_expr(ret);
1721 return ret;
1722}
1723
1725{
1727 auto &ret = static_cast<array_list_exprt &>(expr);
1728 validate_expr(ret);
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:
1772 union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1773 : unary_exprt(ID_union, std::move(_value), std::move(_type))
1774 {
1775 set_component_name(_component_name);
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 {
1790 return get_size_t(ID_component_number);
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:
1879 struct_exprt(operandst _operands, typet _type)
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);
1969 validate_expr(ret);
1970 return ret;
1971}
1972
1975{
1976 PRECONDITION(expr.id()==ID_complex);
1977 complex_exprt &ret = static_cast<complex_exprt &>(expr);
1978 validate_expr(ret);
1979 return ret;
1980}
1981
1984{
1985public:
1986 explicit complex_real_exprt(const exprt &op)
1987 : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
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)
2030 : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
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);
2057 validate_expr(ret);
2058 return ret;
2059}
2060
2063{
2064 PRECONDITION(expr.id() == ID_complex_imag);
2065 complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
2066 validate_expr(ret);
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
2148 explicit and_exprt(exprt::operandst _operands)
2149 : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2150 {
2151 }
2152};
2153
2157
2159
2160template <>
2161inline bool can_cast_expr<and_exprt>(const exprt &base)
2162{
2163 return base.id() == ID_and;
2164}
2165
2172inline const and_exprt &to_and_expr(const exprt &expr)
2173{
2174 PRECONDITION(expr.id()==ID_and);
2175 return static_cast<const and_exprt &>(expr);
2176}
2177
2180{
2181 PRECONDITION(expr.id()==ID_and);
2182 return static_cast<and_exprt &>(expr);
2183}
2184
2185
2188{
2189public:
2191 : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2192 {
2193 }
2194};
2195
2196template <>
2197inline bool can_cast_expr<implies_exprt>(const exprt &base)
2198{
2199 return base.id() == ID_implies;
2200}
2201
2202inline void validate_expr(const implies_exprt &value)
2203{
2204 validate_operands(value, 2, "Implies must have two operands");
2205}
2206
2213inline const implies_exprt &to_implies_expr(const exprt &expr)
2214{
2215 PRECONDITION(expr.id()==ID_implies);
2216 const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2217 validate_expr(ret);
2218 return ret;
2219}
2220
2223{
2224 PRECONDITION(expr.id()==ID_implies);
2225 implies_exprt &ret = static_cast<implies_exprt &>(expr);
2226 validate_expr(ret);
2227 return ret;
2228}
2229
2230
2233{
2234public:
2236 : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2237 {
2238 }
2239
2242 ID_or,
2243 {std::move(op0), std::move(op1), std::move(op2)},
2244 bool_typet())
2245 {
2246 }
2247
2250 ID_or,
2251 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2252 bool_typet())
2253 {
2254 }
2255
2256 explicit or_exprt(exprt::operandst _operands)
2257 : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2258 {
2259 }
2260};
2261
2265
2267
2268template <>
2269inline bool can_cast_expr<or_exprt>(const exprt &base)
2270{
2271 return base.id() == ID_or;
2272}
2273
2280inline const or_exprt &to_or_expr(const exprt &expr)
2281{
2282 PRECONDITION(expr.id()==ID_or);
2283 return static_cast<const or_exprt &>(expr);
2284}
2285
2288{
2289 PRECONDITION(expr.id()==ID_or);
2290 return static_cast<or_exprt &>(expr);
2291}
2292
2293
2296{
2297public:
2299 : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2300 {
2301 }
2302};
2303
2304template <>
2305inline bool can_cast_expr<xor_exprt>(const exprt &base)
2306{
2307 return base.id() == ID_xor;
2308}
2309
2316inline const xor_exprt &to_xor_expr(const exprt &expr)
2317{
2318 PRECONDITION(expr.id()==ID_xor);
2319 return static_cast<const xor_exprt &>(expr);
2320}
2321
2324{
2325 PRECONDITION(expr.id()==ID_xor);
2326 return static_cast<xor_exprt &>(expr);
2327}
2328
2329
2332{
2333public:
2334 explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2335 {
2336 PRECONDITION(as_const(*this).op().is_boolean());
2337 }
2338};
2339
2340template <>
2341inline bool can_cast_expr<not_exprt>(const exprt &base)
2342{
2343 return base.id() == ID_not;
2344}
2345
2346inline void validate_expr(const not_exprt &value)
2347{
2348 validate_operands(value, 1, "Not must have one operand");
2349}
2350
2357inline const not_exprt &to_not_expr(const exprt &expr)
2358{
2359 PRECONDITION(expr.id()==ID_not);
2360 not_exprt::check(expr);
2361 return static_cast<const not_exprt &>(expr);
2362}
2363
2366{
2367 PRECONDITION(expr.id()==ID_not);
2368 not_exprt::check(expr);
2369 return static_cast<not_exprt &>(expr);
2370}
2371
2372
2375{
2376public:
2378 : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2379 {
2380 }
2381
2383 : ternary_exprt(
2384 ID_if,
2385 std::move(cond),
2386 std::move(t),
2387 std::move(f),
2388 std::move(type))
2389 {
2390 }
2391
2393 {
2394 return op0();
2395 }
2396
2397 const exprt &cond() const
2398 {
2399 return op0();
2400 }
2401
2403 {
2404 return op1();
2405 }
2406
2407 const exprt &true_case() const
2408 {
2409 return op1();
2410 }
2411
2413 {
2414 return op2();
2415 }
2416
2417 const exprt &false_case() const
2418 {
2419 return op2();
2420 }
2421
2422 static void check(
2423 const exprt &expr,
2425 {
2426 ternary_exprt::check(expr, vm);
2427 }
2428
2429 static void validate(
2430 const exprt &expr,
2431 const namespacet &ns,
2433 {
2434 ternary_exprt::validate(expr, ns, vm);
2435 }
2436};
2437
2438template <>
2439inline bool can_cast_expr<if_exprt>(const exprt &base)
2440{
2441 return base.id() == ID_if;
2442}
2443
2444inline void validate_expr(const if_exprt &value)
2445{
2446 validate_operands(value, 3, "If-then-else must have three operands");
2447}
2448
2455inline const if_exprt &to_if_expr(const exprt &expr)
2456{
2457 PRECONDITION(expr.id()==ID_if);
2458 const if_exprt &ret = static_cast<const if_exprt &>(expr);
2459 validate_expr(ret);
2460 return ret;
2461}
2462
2465{
2466 PRECONDITION(expr.id()==ID_if);
2467 if_exprt &ret = static_cast<if_exprt &>(expr);
2468 validate_expr(ret);
2469 return ret;
2470}
2471
2476{
2477public:
2478 with_exprt(const exprt &_old, exprt _where, exprt _new_value)
2480 ID_with,
2481 _old.type(),
2482 {_old, std::move(_where), std::move(_new_value)})
2483 {
2484 }
2485
2487 {
2488 return op0();
2489 }
2490
2491 const exprt &old() const
2492 {
2493 return op0();
2494 }
2495
2497 {
2498 return op1();
2499 }
2500
2501 const exprt &where() const
2502 {
2503 return op1();
2504 }
2505
2507 {
2508 return op2();
2509 }
2510
2511 const exprt &new_value() const
2512 {
2513 return op2();
2514 }
2515};
2516
2517template <>
2518inline bool can_cast_expr<with_exprt>(const exprt &base)
2519{
2520 return base.id() == ID_with;
2521}
2522
2523inline void validate_expr(const with_exprt &value)
2524{
2526 value, 3, "array/structure update must have at least 3 operands", true);
2528 value.operands().size() % 2 == 1,
2529 "array/structure update must have an odd number of operands");
2530}
2531
2538inline const with_exprt &to_with_expr(const exprt &expr)
2539{
2540 PRECONDITION(expr.id()==ID_with);
2541 const with_exprt &ret = static_cast<const with_exprt &>(expr);
2542 validate_expr(ret);
2543 return ret;
2544}
2545
2548{
2549 PRECONDITION(expr.id()==ID_with);
2550 with_exprt &ret = static_cast<with_exprt &>(expr);
2551 validate_expr(ret);
2552 return ret;
2553}
2554
2556{
2557public:
2558 explicit index_designatort(exprt _index)
2559 : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
2560 {
2561 }
2562
2563 const exprt &index() const
2564 {
2565 return op0();
2566 }
2567
2569 {
2570 return op0();
2571 }
2572};
2573
2574template <>
2576{
2577 return base.id() == ID_index_designator;
2578}
2579
2580inline void validate_expr(const index_designatort &value)
2581{
2582 validate_operands(value, 1, "Index designator must have one operand");
2583}
2584
2592{
2593 PRECONDITION(expr.id()==ID_index_designator);
2594 const index_designatort &ret = static_cast<const index_designatort &>(expr);
2595 validate_expr(ret);
2596 return ret;
2597}
2598
2601{
2602 PRECONDITION(expr.id()==ID_index_designator);
2603 index_designatort &ret = static_cast<index_designatort &>(expr);
2604 validate_expr(ret);
2605 return ret;
2606}
2607
2609{
2610public:
2611 explicit member_designatort(const irep_idt &_component_name)
2612 : expr_protectedt(ID_member_designator, typet())
2613 {
2614 set(ID_component_name, _component_name);
2615 }
2616
2618 {
2619 return get(ID_component_name);
2620 }
2621};
2622
2623template <>
2625{
2626 return base.id() == ID_member_designator;
2627}
2628
2629inline void validate_expr(const member_designatort &value)
2630{
2631 validate_operands(value, 0, "Member designator must not have operands");
2632}
2633
2641{
2642 PRECONDITION(expr.id()==ID_member_designator);
2643 const member_designatort &ret = static_cast<const member_designatort &>(expr);
2644 validate_expr(ret);
2645 return ret;
2646}
2647
2650{
2651 PRECONDITION(expr.id()==ID_member_designator);
2652 member_designatort &ret = static_cast<member_designatort &>(expr);
2653 validate_expr(ret);
2654 return ret;
2655}
2656
2657
2660{
2661public:
2662 update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
2663 : ternary_exprt(
2664 ID_update,
2665 _old,
2666 std::move(_designator),
2667 std::move(_new_value),
2668 _old.type())
2669 {
2670 }
2671
2673 {
2674 return op0();
2675 }
2676
2677 const exprt &old() const
2678 {
2679 return op0();
2680 }
2681
2682 // the designator operands are either
2683 // 1) member_designator or
2684 // 2) index_designator
2685 // as defined above
2687 {
2688 return op1().operands();
2689 }
2690
2692 {
2693 return op1().operands();
2694 }
2695
2697 {
2698 return op2();
2699 }
2700
2701 const exprt &new_value() const
2702 {
2703 return op2();
2704 }
2705
2707 with_exprt make_with_expr() const;
2708
2709 static void check(
2710 const exprt &expr,
2712 {
2713 ternary_exprt::check(expr, vm);
2714 }
2715
2716 static void validate(
2717 const exprt &expr,
2718 const namespacet &ns,
2720 {
2721 ternary_exprt::validate(expr, ns, vm);
2722 }
2723};
2724
2725template <>
2726inline bool can_cast_expr<update_exprt>(const exprt &base)
2727{
2728 return base.id() == ID_update;
2729}
2730
2731inline void validate_expr(const update_exprt &value)
2732{
2734 value, 3, "Array/structure update must have three operands");
2735}
2736
2743inline const update_exprt &to_update_expr(const exprt &expr)
2744{
2745 PRECONDITION(expr.id()==ID_update);
2746 const update_exprt &ret = static_cast<const update_exprt &>(expr);
2747 validate_expr(ret);
2748 return ret;
2749}
2750
2753{
2754 PRECONDITION(expr.id()==ID_update);
2755 update_exprt &ret = static_cast<update_exprt &>(expr);
2756 validate_expr(ret);
2757 return ret;
2758}
2759
2760
2761#if 0
2763class array_update_exprt:public expr_protectedt
2764{
2765public:
2766 array_update_exprt(
2767 const exprt &_array,
2768 const exprt &_index,
2769 const exprt &_new_value):
2770 exprt(ID_array_update, _array.type())
2771 {
2772 add_to_operands(_array, _index, _new_value);
2773 }
2774
2775 array_update_exprt():expr_protectedt(ID_array_update)
2776 {
2777 operands().resize(3);
2778 }
2779
2780 exprt &array()
2781 {
2782 return op0();
2783 }
2784
2785 const exprt &array() const
2786 {
2787 return op0();
2788 }
2789
2790 exprt &index()
2791 {
2792 return op1();
2793 }
2794
2795 const exprt &index() const
2796 {
2797 return op1();
2798 }
2799
2800 exprt &new_value()
2801 {
2802 return op2();
2803 }
2804
2805 const exprt &new_value() const
2806 {
2807 return op2();
2808 }
2809};
2810
2811template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2812{
2813 return base.id()==ID_array_update;
2814}
2815
2816inline void validate_expr(const array_update_exprt &value)
2817{
2818 validate_operands(value, 3, "Array update must have three operands");
2819}
2820
2827inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2828{
2829 PRECONDITION(expr.id()==ID_array_update);
2830 const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2831 validate_expr(ret);
2832 return ret;
2833}
2834
2836inline array_update_exprt &to_array_update_expr(exprt &expr)
2837{
2838 PRECONDITION(expr.id()==ID_array_update);
2839 array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2840 validate_expr(ret);
2841 return ret;
2842}
2843
2844#endif
2845
2846
2849{
2850public:
2851 member_exprt(exprt op, const irep_idt &component_name, typet _type)
2852 : unary_exprt(ID_member, std::move(op), std::move(_type))
2853 {
2854 const auto &compound_type_id = compound().type().id();
2856 compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2857 compound_type_id == ID_struct || compound_type_id == ID_union);
2858 set_component_name(component_name);
2859 }
2860
2862 : unary_exprt(ID_member, std::move(op), c.type())
2863 {
2864 const auto &compound_type_id = compound().type().id();
2866 compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2867 compound_type_id == ID_struct || compound_type_id == ID_union);
2869 }
2870
2872 {
2873 return get(ID_component_name);
2874 }
2875
2876 void set_component_name(const irep_idt &component_name)
2877 {
2878 set(ID_component_name, component_name);
2879 }
2880
2881 std::size_t get_component_number() const
2882 {
2883 return get_size_t(ID_component_number);
2884 }
2885
2886 // will go away, use compound()
2887 const exprt &struct_op() const
2888 {
2889 return op0();
2890 }
2891
2892 // will go away, use compound()
2894 {
2895 return op0();
2896 }
2897
2898 const exprt &compound() const
2899 {
2900 return op0();
2901 }
2902
2904 {
2905 return op0();
2906 }
2907
2908 static void check(
2909 const exprt &expr,
2911 {
2912 DATA_CHECK(
2913 vm,
2914 expr.operands().size() == 1,
2915 "member expression must have one operand");
2916 }
2917
2918 static void validate(
2919 const exprt &expr,
2920 const namespacet &ns,
2922};
2923
2924template <>
2925inline bool can_cast_expr<member_exprt>(const exprt &base)
2926{
2927 return base.id() == ID_member;
2928}
2929
2930inline void validate_expr(const member_exprt &value)
2931{
2932 validate_operands(value, 1, "Extract member must have one operand");
2933}
2934
2941inline const member_exprt &to_member_expr(const exprt &expr)
2942{
2943 PRECONDITION(expr.id()==ID_member);
2944 member_exprt::check(expr);
2945 return static_cast<const member_exprt &>(expr);
2946}
2947
2950{
2951 PRECONDITION(expr.id()==ID_member);
2952 member_exprt::check(expr);
2953 return static_cast<member_exprt &>(expr);
2954}
2955
2956
2959{
2960public:
2961 explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
2962 {
2963 }
2964};
2965
2966template <>
2967inline bool can_cast_expr<type_exprt>(const exprt &base)
2968{
2969 return base.id() == ID_type;
2970}
2971
2978inline const type_exprt &to_type_expr(const exprt &expr)
2979{
2981 type_exprt::check(expr);
2982 return static_cast<const type_exprt &>(expr);
2983}
2984
2987{
2989 type_exprt::check(expr);
2990 return static_cast<type_exprt &>(expr);
2991}
2992
2995{
2996public:
2997 constant_exprt(const irep_idt &_value, typet _type)
2998 : nullary_exprt(ID_constant, std::move(_type))
2999 {
3000 set_value(_value);
3001 }
3002
3003 const irep_idt &get_value() const
3004 {
3005 return get(ID_value);
3006 }
3007
3008 void set_value(const irep_idt &value)
3009 {
3010 set(ID_value, value);
3011 }
3012
3013 bool value_is_zero_string() const;
3014
3018 bool is_null_pointer() const;
3019
3020 static void check(
3021 const exprt &expr,
3023
3024 static void validate(
3025 const exprt &expr,
3026 const namespacet &,
3028 {
3029 check(expr, vm);
3030 }
3031};
3032
3033template <>
3034inline bool can_cast_expr<constant_exprt>(const exprt &base)
3035{
3036 return base.is_constant();
3037}
3038
3039inline void validate_expr(const constant_exprt &value)
3040{
3041 validate_operands(value, 0, "Constants must not have operands");
3042}
3043
3050inline const constant_exprt &to_constant_expr(const exprt &expr)
3051{
3052 PRECONDITION(expr.is_constant());
3054 return static_cast<const constant_exprt &>(expr);
3055}
3056
3059{
3060 PRECONDITION(expr.is_constant());
3062 return static_cast<constant_exprt &>(expr);
3063}
3064
3065
3068{
3069public:
3071 {
3072 }
3073};
3074
3077{
3078public:
3080 {
3081 }
3082};
3083
3086{
3087public:
3089 : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
3090 {
3091 }
3092};
3093
3094template <>
3095inline bool can_cast_expr<nil_exprt>(const exprt &base)
3096{
3097 return base.id() == ID_nil;
3098}
3099
3102{
3103public:
3104 explicit infinity_exprt(typet _type)
3105 : nullary_exprt(ID_infinity, std::move(_type))
3106 {
3107 }
3108};
3109
3112{
3113public:
3114 using variablest = std::vector<symbol_exprt>;
3115
3118 irep_idt _id,
3119 const variablest &_variables,
3120 exprt _where,
3121 typet _type)
3122 : binary_exprt(
3124 ID_tuple,
3125 (const operandst &)_variables,
3126 typet(ID_tuple)),
3127 _id,
3128 std::move(_where),
3129 std::move(_type))
3130 {
3131 }
3132
3134 {
3136 }
3137
3138 const variablest &variables() const
3139 {
3141 }
3142
3144 {
3145 return op1();
3146 }
3147
3148 const exprt &where() const
3149 {
3150 return op1();
3151 }
3152
3155 exprt instantiate(const exprt::operandst &) const;
3156
3159 exprt instantiate(const variablest &) const;
3160};
3161
3162template <>
3163inline bool can_cast_expr<binding_exprt>(const exprt &base)
3164{
3165 return base.id() == ID_forall || base.id() == ID_exists ||
3166 base.id() == ID_lambda || base.id() == ID_array_comprehension;
3167}
3168
3169inline void validate_expr(const binding_exprt &binding_expr)
3170{
3172 binding_expr, 2, "Binding expressions must have two operands");
3173}
3174
3181inline const binding_exprt &to_binding_expr(const exprt &expr)
3182{
3184 expr.id() == ID_forall || expr.id() == ID_exists ||
3185 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3186 const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
3187 validate_expr(ret);
3188 return ret;
3189}
3190
3198{
3200 expr.id() == ID_forall || expr.id() == ID_exists ||
3201 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3202 binding_exprt &ret = static_cast<binding_exprt &>(expr);
3203 validate_expr(ret);
3204 return ret;
3205}
3206
3209{
3210public:
3214 const exprt &where)
3215 : binary_exprt(
3217 ID_let_binding,
3218 std::move(variables),
3219 where,
3220 where.type()),
3221 ID_let,
3222 multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
3223 where.type())
3224 {
3225 PRECONDITION(this->variables().size() == this->values().size());
3226 }
3227
3230 : let_exprt(
3232 operandst{std::move(value)},
3233 where)
3234 {
3235 }
3236
3238 {
3239 return static_cast<binding_exprt &>(op0());
3240 }
3241
3242 const binding_exprt &binding() const
3243 {
3244 return static_cast<const binding_exprt &>(op0());
3245 }
3246
3249 {
3250 auto &variables = binding().variables();
3251 PRECONDITION(variables.size() == 1);
3252 return variables.front();
3253 }
3254
3256 const symbol_exprt &symbol() const
3257 {
3258 const auto &variables = binding().variables();
3259 PRECONDITION(variables.size() == 1);
3260 return variables.front();
3261 }
3262
3265 {
3266 auto &values = this->values();
3267 PRECONDITION(values.size() == 1);
3268 return values.front();
3269 }
3270
3272 const exprt &value() const
3273 {
3274 const auto &values = this->values();
3275 PRECONDITION(values.size() == 1);
3276 return values.front();
3277 }
3278
3280 {
3281 return static_cast<multi_ary_exprt &>(op1()).operands();
3282 }
3283
3284 const operandst &values() const
3285 {
3286 return static_cast<const multi_ary_exprt &>(op1()).operands();
3287 }
3288
3291 {
3292 return binding().variables();
3293 }
3294
3297 {
3298 return binding().variables();
3299 }
3300
3303 {
3304 return binding().where();
3305 }
3306
3308 const exprt &where() const
3309 {
3310 return binding().where();
3311 }
3312
3313 static void validate(const exprt &, validation_modet);
3314};
3315
3316template <>
3317inline bool can_cast_expr<let_exprt>(const exprt &base)
3318{
3319 return base.id() == ID_let;
3320}
3321
3322inline void validate_expr(const let_exprt &let_expr)
3323{
3324 validate_operands(let_expr, 2, "Let must have two operands");
3325}
3326
3333inline const let_exprt &to_let_expr(const exprt &expr)
3334{
3335 PRECONDITION(expr.id()==ID_let);
3336 const let_exprt &ret = static_cast<const let_exprt &>(expr);
3337 validate_expr(ret);
3338 return ret;
3339}
3340
3343{
3344 PRECONDITION(expr.id()==ID_let);
3345 let_exprt &ret = static_cast<let_exprt &>(expr);
3346 validate_expr(ret);
3347 return ret;
3348}
3349
3350
3355{
3356public:
3357 cond_exprt(operandst _operands, typet _type)
3358 : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3359 {
3360 }
3361
3365 void add_case(const exprt &condition, const exprt &value)
3366 {
3367 PRECONDITION(condition.is_boolean());
3368 operands().reserve(operands().size() + 2);
3369 operands().push_back(condition);
3370 operands().push_back(value);
3371 }
3372};
3373
3374template <>
3375inline bool can_cast_expr<cond_exprt>(const exprt &base)
3376{
3377 return base.id() == ID_cond;
3378}
3379
3380inline void validate_expr(const cond_exprt &value)
3381{
3383 value.operands().size() % 2 == 0, "cond must have even number of operands");
3384}
3385
3392inline const cond_exprt &to_cond_expr(const exprt &expr)
3393{
3394 PRECONDITION(expr.id() == ID_cond);
3395 const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3396 validate_expr(ret);
3397 return ret;
3398}
3399
3402{
3403 PRECONDITION(expr.id() == ID_cond);
3404 cond_exprt &ret = static_cast<cond_exprt &>(expr);
3405 validate_expr(ret);
3406 return ret;
3407}
3408
3418{
3419public:
3422 exprt body,
3423 array_typet _type)
3424 : binding_exprt(
3425 ID_array_comprehension,
3426 {std::move(arg)},
3427 std::move(body),
3428 std::move(_type))
3429 {
3430 }
3431
3432 const array_typet &type() const
3433 {
3434 return static_cast<const array_typet &>(binary_exprt::type());
3435 }
3436
3438 {
3439 return static_cast<array_typet &>(binary_exprt::type());
3440 }
3441
3442 const symbol_exprt &arg() const
3443 {
3444 auto &variables = this->variables();
3445 PRECONDITION(variables.size() == 1);
3446 return variables[0];
3447 }
3448
3450 {
3451 auto &variables = this->variables();
3452 PRECONDITION(variables.size() == 1);
3453 return variables[0];
3454 }
3455
3456 const exprt &body() const
3457 {
3458 return where();
3459 }
3460
3462 {
3463 return where();
3464 }
3465};
3466
3467template <>
3469{
3470 return base.id() == ID_array_comprehension;
3471}
3472
3474{
3475 validate_operands(value, 2, "'Array comprehension' must have two operands");
3476}
3477
3484inline const array_comprehension_exprt &
3486{
3487 PRECONDITION(expr.id() == ID_array_comprehension);
3488 const array_comprehension_exprt &ret =
3489 static_cast<const array_comprehension_exprt &>(expr);
3490 validate_expr(ret);
3491 return ret;
3492}
3493
3496{
3497 PRECONDITION(expr.id() == ID_array_comprehension);
3499 static_cast<array_comprehension_exprt &>(expr);
3500 validate_expr(ret);
3501 return ret;
3502}
3503
3504inline void validate_expr(const class class_method_descriptor_exprt &value);
3505
3508{
3509public:
3525 typet _type,
3529 : nullary_exprt(ID_virtual_function, std::move(_type))
3530 {
3532 set(ID_component_name, std::move(mangled_method_name));
3533 set(ID_C_class, std::move(class_id));
3534 set(ID_C_base_name, std::move(base_method_name));
3535 set(ID_identifier, std::move(id));
3536 validate_expr(*this);
3537 }
3538
3546 {
3547 return get(ID_component_name);
3548 }
3549
3553 const irep_idt &class_id() const
3554 {
3555 return get(ID_C_class);
3556 }
3557
3561 {
3562 return get(ID_C_base_name);
3563 }
3564
3569 {
3570 return get(ID_identifier);
3571 }
3572};
3573
3574inline void validate_expr(const class class_method_descriptor_exprt &value)
3575{
3576 validate_operands(value, 0, "class method descriptor must not have operands");
3578 !value.mangled_method_name().empty(),
3579 "class method descriptor must have a mangled method name.");
3581 !value.class_id().empty(), "class method descriptor must have a class id.");
3583 !value.base_method_name().empty(),
3584 "class method descriptor must have a base method name.");
3586 value.get_identifier() == id2string(value.class_id()) + "." +
3588 "class method descriptor must have an identifier in the expected format.");
3589}
3590
3597inline const class_method_descriptor_exprt &
3599{
3600 PRECONDITION(expr.id() == ID_virtual_function);
3602 return static_cast<const class_method_descriptor_exprt &>(expr);
3603}
3604
3605template <>
3607{
3608 return base.id() == ID_virtual_function;
3609}
3610
3617{
3618public:
3620 : binary_exprt(
3621 std::move(symbol),
3622 ID_named_term,
3623 value, // not moved, for type
3624 value.type())
3625 {
3626 PRECONDITION(symbol.type() == type());
3627 }
3628
3629 const symbol_exprt &symbol() const
3630 {
3631 return static_cast<const symbol_exprt &>(op0());
3632 }
3633
3635 {
3636 return static_cast<symbol_exprt &>(op0());
3637 }
3638
3639 const exprt &value() const
3640 {
3641 return op1();
3642 }
3643
3645 {
3646 return op1();
3647 }
3648};
3649
3650template <>
3652{
3653 return base.id() == ID_named_term;
3654}
3655
3656inline void validate_expr(const named_term_exprt &value)
3657{
3658 validate_operands(value, 2, "'named term' must have two operands");
3659}
3660
3668{
3669 PRECONDITION(expr.id() == ID_named_term);
3670 const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
3671 validate_expr(ret);
3672 return ret;
3673}
3674
3677{
3678 PRECONDITION(expr.id() == ID_named_term);
3679 named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
3680 validate_expr(ret);
3681 return ret;
3682}
3683
3684#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
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:3418
const array_typet & type() const
Definition std_expr.h:3432
const symbol_exprt & arg() const
Definition std_expr.h:3442
const exprt & body() const
Definition std_expr.h:3456
array_typet & type()
Definition std_expr.h:3437
symbol_exprt & arg()
Definition std_expr.h:3449
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition std_expr.h:3420
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
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:3112
const variablest & variables() const
Definition std_expr.h:3138
const exprt & where() const
Definition std_expr.h:3148
exprt & where()
Definition std_expr.h:3143
variablest & variables()
Definition std_expr.h:3133
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition std_expr.h:3117
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:225
std::vector< symbol_exprt > variablest
Definition std_expr.h:3114
The Boolean type.
Definition std_types.h:36
An expression describing a method on a class.
Definition std_expr.h:3508
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:3560
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition std_expr.h:3545
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:3568
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition std_expr.h:3524
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:3553
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:1130
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition std_expr.h:3355
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition std_expr.h:3365
cond_exprt(operandst _operands, typet _type)
Definition std_expr.h:3357
A constant literal expression.
Definition std_expr.h:2995
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:3024
const irep_idt & get_value() const
Definition std_expr.h:3003
bool value_is_zero_string() const
Definition std_expr.cpp:19
constant_exprt(const irep_idt &_value, typet _type)
Definition std_expr.h:2997
void set_value(const irep_idt &value)
Definition std_expr.h:3008
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
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
bool empty() const
Definition dstring.h:89
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
expr_protectedt(irep_idt _id, typet _type)
Definition expr.h:347
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
exprt()
Definition expr.h:61
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
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:2375
const exprt & false_case() const
Definition std_expr.h:2417
exprt & cond()
Definition std_expr.h:2392
const exprt & cond() const
Definition std_expr.h:2397
if_exprt(exprt cond, const exprt &t, exprt f)
Definition std_expr.h:2377
const exprt & true_case() const
Definition std_expr.h:2407
exprt & false_case()
Definition std_expr.h:2412
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition std_expr.h:2382
exprt & true_case()
Definition std_expr.h:2402
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2422
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2429
Boolean implication.
Definition std_expr.h:2188
implies_exprt(exprt op0, exprt op1)
Definition std_expr.h:2190
const exprt & index() const
Definition std_expr.h:2563
index_designatort(exprt _index)
Definition std_expr.h:2558
exprt & index()
Definition std_expr.h:2568
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
infinity_exprt(typet _type)
Definition std_expr.h:3104
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:3209
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3290
const binding_exprt & binding() const
Definition std_expr.h:3242
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition std_expr.h:3296
operandst & values()
Definition std_expr.h:3279
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition std_expr.h:3229
const exprt & where() const
convenience accessor for binding().where()
Definition std_expr.h:3308
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:168
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition std_expr.h:3256
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition std_expr.h:3211
exprt & value()
convenience accessor for the value of a single binding
Definition std_expr.h:3264
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3302
binding_exprt & binding()
Definition std_expr.h:3237
const operandst & values() const
Definition std_expr.h:3284
const exprt & value() const
convenience accessor for the value of a single binding
Definition std_expr.h:3272
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition std_expr.h:3248
irep_idt get_component_name() const
Definition std_expr.h:2617
member_designatort(const irep_idt &_component_name)
Definition std_expr.h:2611
Extract member of struct or union.
Definition std_expr.h:2849
const exprt & compound() const
Definition std_expr.h:2898
exprt & struct_op()
Definition std_expr.h:2893
const exprt & struct_op() const
Definition std_expr.h:2887
irep_idt get_component_name() const
Definition std_expr.h:2871
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:2876
exprt & compound()
Definition std_expr.h:2903
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
Definition std_expr.cpp:133
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2908
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition std_expr.h:2851
std::size_t get_component_number() const
Definition std_expr.h:2881
member_exprt(exprt op, const struct_typet::componentt &c)
Definition std_expr.h:2861
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:3617
named_term_exprt(symbol_exprt symbol, exprt value)
Definition std_expr.h:3619
symbol_exprt & symbol()
Definition std_expr.h:3634
const exprt & value() const
Definition std_expr.h:3639
const symbol_exprt & symbol() const
Definition std_expr.h:3629
exprt & value()
Definition std_expr.h:3644
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
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 negation.
Definition std_expr.h:2332
not_exprt(exprt _op)
Definition std_expr.h:2334
Disequality.
Definition std_expr.h:1425
notequal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1427
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:2233
or_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2240
or_exprt(exprt::operandst _operands)
Definition std_expr.h:2256
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2248
or_exprt(exprt op0, exprt op1)
Definition std_expr.h:2235
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
predicate_exprt(const irep_idt &_id)
Definition std_expr.h:576
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:596
sign_exprt(exprt _op)
Definition std_expr.h:598
Struct constructor from list of elements.
Definition std_expr.h:1877
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:114
struct_exprt(operandst _operands, typet _type)
Definition std_expr.h:1879
const irep_idt & get_name() const
Definition std_types.h:79
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
An expression denoting a type.
Definition std_expr.h:2959
type_exprt(typet type)
Definition std_expr.h:2961
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
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:2660
exprt & old()
Definition std_expr.h:2672
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
Definition std_expr.cpp:194
exprt::operandst & designator()
Definition std_expr.h:2686
exprt & new_value()
Definition std_expr.h:2696
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2716
const exprt & new_value() const
Definition std_expr.h:2701
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition std_expr.h:2662
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2709
const exprt & old() const
Definition std_expr.h:2677
const exprt::operandst & designator() const
Definition std_expr.h:2691
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:1061
Operator to update elements in structs and arrays.
Definition std_expr.h:2476
const exprt & old() const
Definition std_expr.h:2491
const exprt & where() const
Definition std_expr.h:2501
exprt & new_value()
Definition std_expr.h:2506
exprt & where()
Definition std_expr.h:2496
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition std_expr.h:2478
const exprt & new_value() const
Definition std_expr.h:2511
exprt & old()
Definition std_expr.h:2486
Boolean XOR.
Definition std_expr.h:2296
xor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2298
Templated functions to cast to specific exprt-derived classes.
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
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
expanding_vectort< std::vector< java_bytecode_convert_methodt::variablet > > variablest
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:2341
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:2978
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:2305
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:2439
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:3598
bool can_cast_expr< named_term_exprt >(const exprt &base)
Definition std_expr.h:3651
bool can_cast_expr< binding_exprt >(const exprt &base)
Definition std_expr.h:3163
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1277
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1137
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition std_expr.h:2172
bool can_cast_expr< member_designatort >(const exprt &base)
Definition std_expr.h:2624
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3485
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:3667
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition std_expr.h:3468
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition std_expr.h:2316
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2280
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:3392
bool can_cast_expr< type_exprt >(const exprt &base)
Definition std_expr.h:2967
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:3606
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:2518
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition std_expr.h:1754
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:83
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition std_expr.h:1070
bool can_cast_expr< let_exprt >(const exprt &base)
Definition std_expr.h:3317
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 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:3333
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:3034
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2455
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2941
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:2925
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:3181
bool can_cast_expr< or_exprt >(const exprt &base)
Definition std_expr.h:2269
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:2591
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:3375
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:2726
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:3050
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:2575
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2357
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:2538
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1965
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition std_expr.h:540
bool can_cast_expr< and_exprt >(const exprt &base)
Definition std_expr.h:2161
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition std_expr.h:816
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2213
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:2743
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition std_expr.h:3095
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:2197
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:2640
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 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:1155
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
dstringt irep_idt