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
2164
2165template <>
2166inline bool can_cast_expr<and_exprt>(const exprt &base)
2167{
2168 return base.id() == ID_and;
2169}
2170
2177inline const and_exprt &to_and_expr(const exprt &expr)
2178{
2179 PRECONDITION(expr.id()==ID_and);
2180 return static_cast<const and_exprt &>(expr);
2181}
2182
2185{
2186 PRECONDITION(expr.id()==ID_and);
2187 return static_cast<and_exprt &>(expr);
2188}
2189
2196{
2197public:
2199 : multi_ary_exprt(std::move(op0), ID_nand, std::move(op1), bool_typet())
2200 {
2201 }
2202
2203 explicit nand_exprt(exprt::operandst _operands)
2204 : multi_ary_exprt(ID_nand, std::move(_operands), bool_typet())
2205 {
2206 }
2207};
2208
2215inline const nand_exprt &to_nand_expr(const exprt &expr)
2216{
2217 PRECONDITION(expr.id() == ID_nand);
2218 return static_cast<const nand_exprt &>(expr);
2219}
2220
2223{
2224 PRECONDITION(expr.id() == ID_nand);
2225 return static_cast<nand_exprt &>(expr);
2226}
2227
2230{
2231public:
2233 : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2234 {
2235 }
2236};
2237
2238template <>
2239inline bool can_cast_expr<implies_exprt>(const exprt &base)
2240{
2241 return base.id() == ID_implies;
2242}
2243
2244inline void validate_expr(const implies_exprt &value)
2245{
2246 validate_operands(value, 2, "Implies must have two operands");
2247}
2248
2255inline const implies_exprt &to_implies_expr(const exprt &expr)
2256{
2257 PRECONDITION(expr.id()==ID_implies);
2258 const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2259 validate_expr(ret);
2260 return ret;
2261}
2262
2265{
2266 PRECONDITION(expr.id()==ID_implies);
2267 implies_exprt &ret = static_cast<implies_exprt &>(expr);
2268 validate_expr(ret);
2269 return ret;
2270}
2271
2272
2275{
2276public:
2278 : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2279 {
2280 }
2281
2284 ID_or,
2285 {std::move(op0), std::move(op1), std::move(op2)},
2286 bool_typet())
2287 {
2288 }
2289
2292 ID_or,
2293 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2294 bool_typet())
2295 {
2296 }
2297
2298 explicit or_exprt(exprt::operandst _operands)
2299 : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2300 {
2301 }
2302};
2303
2307
2309
2310template <>
2311inline bool can_cast_expr<or_exprt>(const exprt &base)
2312{
2313 return base.id() == ID_or;
2314}
2315
2322inline const or_exprt &to_or_expr(const exprt &expr)
2323{
2324 PRECONDITION(expr.id()==ID_or);
2325 return static_cast<const or_exprt &>(expr);
2326}
2327
2330{
2331 PRECONDITION(expr.id()==ID_or);
2332 return static_cast<or_exprt &>(expr);
2333}
2334
2341{
2342public:
2344 : multi_ary_exprt(std::move(op0), ID_nor, std::move(op1), bool_typet())
2345 {
2346 }
2347
2348 explicit nor_exprt(exprt::operandst _operands)
2349 : multi_ary_exprt(ID_nor, std::move(_operands), bool_typet())
2350 {
2351 }
2352};
2353
2360inline const nor_exprt &to_nor_expr(const exprt &expr)
2361{
2362 PRECONDITION(expr.id() == ID_nor);
2363 return static_cast<const nor_exprt &>(expr);
2364}
2365
2368{
2369 PRECONDITION(expr.id() == ID_nor);
2370 return static_cast<nor_exprt &>(expr);
2371}
2372
2375{
2376public:
2378 : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2379 {
2380 }
2381
2382 explicit xor_exprt(exprt::operandst _operands)
2383 : multi_ary_exprt(ID_xor, std::move(_operands), bool_typet())
2384 {
2385 }
2386};
2387
2388template <>
2389inline bool can_cast_expr<xor_exprt>(const exprt &base)
2390{
2391 return base.id() == ID_xor;
2392}
2393
2400inline const xor_exprt &to_xor_expr(const exprt &expr)
2401{
2402 PRECONDITION(expr.id()==ID_xor);
2403 return static_cast<const xor_exprt &>(expr);
2404}
2405
2408{
2409 PRECONDITION(expr.id()==ID_xor);
2410 return static_cast<xor_exprt &>(expr);
2411}
2412
2419{
2420public:
2422 : multi_ary_exprt(std::move(_op0), ID_xnor, std::move(_op1), bool_typet())
2423 {
2424 }
2425
2426 explicit xnor_exprt(exprt::operandst _operands)
2427 : multi_ary_exprt(ID_xnor, std::move(_operands), bool_typet())
2428 {
2429 }
2430};
2431
2432template <>
2433inline bool can_cast_expr<xnor_exprt>(const exprt &base)
2434{
2435 return base.id() == ID_xnor;
2436}
2437
2444inline const xnor_exprt &to_xnor_expr(const exprt &expr)
2445{
2446 PRECONDITION(expr.id() == ID_xnor);
2447 return static_cast<const xnor_exprt &>(expr);
2448}
2449
2452{
2453 PRECONDITION(expr.id() == ID_xnor);
2454 return static_cast<xnor_exprt &>(expr);
2455}
2456
2459{
2460public:
2461 explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2462 {
2463 PRECONDITION(as_const(*this).op().is_boolean());
2464 }
2465};
2466
2467template <>
2468inline bool can_cast_expr<not_exprt>(const exprt &base)
2469{
2470 return base.id() == ID_not;
2471}
2472
2473inline void validate_expr(const not_exprt &value)
2474{
2475 validate_operands(value, 1, "Not must have one operand");
2476}
2477
2484inline const not_exprt &to_not_expr(const exprt &expr)
2485{
2486 PRECONDITION(expr.id()==ID_not);
2487 not_exprt::check(expr);
2488 return static_cast<const not_exprt &>(expr);
2489}
2490
2493{
2494 PRECONDITION(expr.id()==ID_not);
2495 not_exprt::check(expr);
2496 return static_cast<not_exprt &>(expr);
2497}
2498
2499
2502{
2503public:
2505 : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2506 {
2507 }
2508
2510 : ternary_exprt(
2511 ID_if,
2512 std::move(cond),
2513 std::move(t),
2514 std::move(f),
2515 std::move(type))
2516 {
2517 }
2518
2520 {
2521 return op0();
2522 }
2523
2524 const exprt &cond() const
2525 {
2526 return op0();
2527 }
2528
2530 {
2531 return op1();
2532 }
2533
2534 const exprt &true_case() const
2535 {
2536 return op1();
2537 }
2538
2540 {
2541 return op2();
2542 }
2543
2544 const exprt &false_case() const
2545 {
2546 return op2();
2547 }
2548
2549 static void check(
2550 const exprt &expr,
2552 {
2553 ternary_exprt::check(expr, vm);
2554 }
2555
2556 static void validate(
2557 const exprt &expr,
2558 const namespacet &ns,
2560 {
2561 ternary_exprt::validate(expr, ns, vm);
2562 }
2563};
2564
2565template <>
2566inline bool can_cast_expr<if_exprt>(const exprt &base)
2567{
2568 return base.id() == ID_if;
2569}
2570
2571inline void validate_expr(const if_exprt &value)
2572{
2573 validate_operands(value, 3, "If-then-else must have three operands");
2574}
2575
2582inline const if_exprt &to_if_expr(const exprt &expr)
2583{
2584 PRECONDITION(expr.id()==ID_if);
2585 const if_exprt &ret = static_cast<const if_exprt &>(expr);
2586 validate_expr(ret);
2587 return ret;
2588}
2589
2592{
2593 PRECONDITION(expr.id()==ID_if);
2594 if_exprt &ret = static_cast<if_exprt &>(expr);
2595 validate_expr(ret);
2596 return ret;
2597}
2598
2603{
2604public:
2605 with_exprt(const exprt &_old, exprt _where, exprt _new_value)
2607 ID_with,
2608 _old.type(),
2609 {_old, std::move(_where), std::move(_new_value)})
2610 {
2611 }
2612
2614 {
2615 return op0();
2616 }
2617
2618 const exprt &old() const
2619 {
2620 return op0();
2621 }
2622
2624 {
2625 return op1();
2626 }
2627
2628 const exprt &where() const
2629 {
2630 return op1();
2631 }
2632
2634 {
2635 return op2();
2636 }
2637
2638 const exprt &new_value() const
2639 {
2640 return op2();
2641 }
2642};
2643
2644template <>
2645inline bool can_cast_expr<with_exprt>(const exprt &base)
2646{
2647 return base.id() == ID_with;
2648}
2649
2650inline void validate_expr(const with_exprt &value)
2651{
2653 value, 3, "array/structure update must have at least 3 operands", true);
2655 value.operands().size() % 2 == 1,
2656 "array/structure update must have an odd number of operands");
2657}
2658
2665inline const with_exprt &to_with_expr(const exprt &expr)
2666{
2667 PRECONDITION(expr.id()==ID_with);
2668 const with_exprt &ret = static_cast<const with_exprt &>(expr);
2669 validate_expr(ret);
2670 return ret;
2671}
2672
2675{
2676 PRECONDITION(expr.id()==ID_with);
2677 with_exprt &ret = static_cast<with_exprt &>(expr);
2678 validate_expr(ret);
2679 return ret;
2680}
2681
2683{
2684public:
2685 explicit index_designatort(exprt _index)
2686 : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
2687 {
2688 }
2689
2690 const exprt &index() const
2691 {
2692 return op0();
2693 }
2694
2696 {
2697 return op0();
2698 }
2699};
2700
2701template <>
2703{
2704 return base.id() == ID_index_designator;
2705}
2706
2707inline void validate_expr(const index_designatort &value)
2708{
2709 validate_operands(value, 1, "Index designator must have one operand");
2710}
2711
2719{
2720 PRECONDITION(expr.id()==ID_index_designator);
2721 const index_designatort &ret = static_cast<const index_designatort &>(expr);
2722 validate_expr(ret);
2723 return ret;
2724}
2725
2728{
2729 PRECONDITION(expr.id()==ID_index_designator);
2730 index_designatort &ret = static_cast<index_designatort &>(expr);
2731 validate_expr(ret);
2732 return ret;
2733}
2734
2736{
2737public:
2738 explicit member_designatort(const irep_idt &_component_name)
2739 : expr_protectedt(ID_member_designator, typet())
2740 {
2741 set(ID_component_name, _component_name);
2742 }
2743
2745 {
2746 return get(ID_component_name);
2747 }
2748};
2749
2750template <>
2752{
2753 return base.id() == ID_member_designator;
2754}
2755
2756inline void validate_expr(const member_designatort &value)
2757{
2758 validate_operands(value, 0, "Member designator must not have operands");
2759}
2760
2768{
2769 PRECONDITION(expr.id()==ID_member_designator);
2770 const member_designatort &ret = static_cast<const member_designatort &>(expr);
2771 validate_expr(ret);
2772 return ret;
2773}
2774
2777{
2778 PRECONDITION(expr.id()==ID_member_designator);
2779 member_designatort &ret = static_cast<member_designatort &>(expr);
2780 validate_expr(ret);
2781 return ret;
2782}
2783
2784
2787{
2788public:
2789 update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
2790 : ternary_exprt(
2791 ID_update,
2792 _old,
2793 std::move(_designator),
2794 std::move(_new_value),
2795 _old.type())
2796 {
2797 }
2798
2800 {
2801 return op0();
2802 }
2803
2804 const exprt &old() const
2805 {
2806 return op0();
2807 }
2808
2809 // the designator operands are either
2810 // 1) member_designator or
2811 // 2) index_designator
2812 // as defined above
2814 {
2815 return op1().operands();
2816 }
2817
2819 {
2820 return op1().operands();
2821 }
2822
2824 {
2825 return op2();
2826 }
2827
2828 const exprt &new_value() const
2829 {
2830 return op2();
2831 }
2832
2834 with_exprt make_with_expr() const;
2835
2836 static void check(
2837 const exprt &expr,
2839 {
2840 ternary_exprt::check(expr, vm);
2841 }
2842
2843 static void validate(
2844 const exprt &expr,
2845 const namespacet &ns,
2847 {
2848 ternary_exprt::validate(expr, ns, vm);
2849 }
2850};
2851
2852template <>
2853inline bool can_cast_expr<update_exprt>(const exprt &base)
2854{
2855 return base.id() == ID_update;
2856}
2857
2858inline void validate_expr(const update_exprt &value)
2859{
2861 value, 3, "Array/structure update must have three operands");
2862}
2863
2870inline const update_exprt &to_update_expr(const exprt &expr)
2871{
2872 PRECONDITION(expr.id()==ID_update);
2873 const update_exprt &ret = static_cast<const update_exprt &>(expr);
2874 validate_expr(ret);
2875 return ret;
2876}
2877
2880{
2881 PRECONDITION(expr.id()==ID_update);
2882 update_exprt &ret = static_cast<update_exprt &>(expr);
2883 validate_expr(ret);
2884 return ret;
2885}
2886
2887
2888#if 0
2890class array_update_exprt:public expr_protectedt
2891{
2892public:
2893 array_update_exprt(
2894 const exprt &_array,
2895 const exprt &_index,
2896 const exprt &_new_value):
2897 exprt(ID_array_update, _array.type())
2898 {
2899 add_to_operands(_array, _index, _new_value);
2900 }
2901
2902 array_update_exprt():expr_protectedt(ID_array_update)
2903 {
2904 operands().resize(3);
2905 }
2906
2907 exprt &array()
2908 {
2909 return op0();
2910 }
2911
2912 const exprt &array() const
2913 {
2914 return op0();
2915 }
2916
2917 exprt &index()
2918 {
2919 return op1();
2920 }
2921
2922 const exprt &index() const
2923 {
2924 return op1();
2925 }
2926
2927 exprt &new_value()
2928 {
2929 return op2();
2930 }
2931
2932 const exprt &new_value() const
2933 {
2934 return op2();
2935 }
2936};
2937
2938template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2939{
2940 return base.id()==ID_array_update;
2941}
2942
2943inline void validate_expr(const array_update_exprt &value)
2944{
2945 validate_operands(value, 3, "Array update must have three operands");
2946}
2947
2954inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2955{
2956 PRECONDITION(expr.id()==ID_array_update);
2957 const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2958 validate_expr(ret);
2959 return ret;
2960}
2961
2963inline array_update_exprt &to_array_update_expr(exprt &expr)
2964{
2965 PRECONDITION(expr.id()==ID_array_update);
2966 array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2967 validate_expr(ret);
2968 return ret;
2969}
2970
2971#endif
2972
2973
2976{
2977public:
2978 member_exprt(exprt op, const irep_idt &component_name, typet _type)
2979 : unary_exprt(ID_member, std::move(op), std::move(_type))
2980 {
2981 const auto &compound_type_id = compound().type().id();
2983 compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2984 compound_type_id == ID_struct || compound_type_id == ID_union);
2985 set_component_name(component_name);
2986 }
2987
2989 : unary_exprt(ID_member, std::move(op), c.type())
2990 {
2991 const auto &compound_type_id = compound().type().id();
2993 compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2994 compound_type_id == ID_struct || compound_type_id == ID_union);
2996 }
2997
2999 {
3000 return get(ID_component_name);
3001 }
3002
3003 void set_component_name(const irep_idt &component_name)
3004 {
3005 set(ID_component_name, component_name);
3006 }
3007
3008 std::size_t get_component_number() const
3009 {
3010 return get_size_t(ID_component_number);
3011 }
3012
3013 // will go away, use compound()
3014 const exprt &struct_op() const
3015 {
3016 return op0();
3017 }
3018
3019 // will go away, use compound()
3021 {
3022 return op0();
3023 }
3024
3025 const exprt &compound() const
3026 {
3027 return op0();
3028 }
3029
3031 {
3032 return op0();
3033 }
3034
3035 static void check(
3036 const exprt &expr,
3038 {
3039 DATA_CHECK(
3040 vm,
3041 expr.operands().size() == 1,
3042 "member expression must have one operand");
3043 }
3044
3045 static void validate(
3046 const exprt &expr,
3047 const namespacet &ns,
3049};
3050
3051template <>
3052inline bool can_cast_expr<member_exprt>(const exprt &base)
3053{
3054 return base.id() == ID_member;
3055}
3056
3057inline void validate_expr(const member_exprt &value)
3058{
3059 validate_operands(value, 1, "Extract member must have one operand");
3060}
3061
3068inline const member_exprt &to_member_expr(const exprt &expr)
3069{
3070 PRECONDITION(expr.id()==ID_member);
3071 member_exprt::check(expr);
3072 return static_cast<const member_exprt &>(expr);
3073}
3074
3077{
3078 PRECONDITION(expr.id()==ID_member);
3079 member_exprt::check(expr);
3080 return static_cast<member_exprt &>(expr);
3081}
3082
3083
3086{
3087public:
3088 explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
3089 {
3090 }
3091};
3092
3093template <>
3094inline bool can_cast_expr<type_exprt>(const exprt &base)
3095{
3096 return base.id() == ID_type;
3097}
3098
3105inline const type_exprt &to_type_expr(const exprt &expr)
3106{
3108 type_exprt::check(expr);
3109 return static_cast<const type_exprt &>(expr);
3110}
3111
3114{
3116 type_exprt::check(expr);
3117 return static_cast<type_exprt &>(expr);
3118}
3119
3122{
3123public:
3124 constant_exprt(const irep_idt &_value, typet _type)
3125 : nullary_exprt(ID_constant, std::move(_type))
3126 {
3127 set_value(_value);
3128 }
3129
3130 const irep_idt &get_value() const
3131 {
3132 return get(ID_value);
3133 }
3134
3135 void set_value(const irep_idt &value)
3136 {
3137 set(ID_value, value);
3138 }
3139
3140 bool value_is_zero_string() const;
3141
3145 bool is_null_pointer() const;
3146
3147 static void check(
3148 const exprt &expr,
3150
3151 static void validate(
3152 const exprt &expr,
3153 const namespacet &,
3155 {
3156 check(expr, vm);
3157 }
3158};
3159
3160template <>
3161inline bool can_cast_expr<constant_exprt>(const exprt &base)
3162{
3163 return base.is_constant();
3164}
3165
3166inline void validate_expr(const constant_exprt &value)
3167{
3168 validate_operands(value, 0, "Constants must not have operands");
3169}
3170
3177inline const constant_exprt &to_constant_expr(const exprt &expr)
3178{
3179 PRECONDITION(expr.is_constant());
3181 return static_cast<const constant_exprt &>(expr);
3182}
3183
3186{
3187 PRECONDITION(expr.is_constant());
3189 return static_cast<constant_exprt &>(expr);
3190}
3191
3192
3195{
3196public:
3198 {
3199 }
3200};
3201
3204{
3205public:
3207 {
3208 }
3209};
3210
3213{
3214public:
3216 : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
3217 {
3218 }
3219};
3220
3221template <>
3222inline bool can_cast_expr<nil_exprt>(const exprt &base)
3223{
3224 return base.id() == ID_nil;
3225}
3226
3229{
3230public:
3231 explicit infinity_exprt(typet _type)
3232 : nullary_exprt(ID_infinity, std::move(_type))
3233 {
3234 }
3235};
3236
3239{
3240public:
3241 using variablest = std::vector<symbol_exprt>;
3242
3245 irep_idt _id,
3246 const variablest &_variables,
3247 exprt _where,
3248 typet _type)
3249 : binary_exprt(
3251 ID_tuple,
3252 (const operandst &)_variables,
3253 typet(ID_tuple)),
3254 _id,
3255 std::move(_where),
3256 std::move(_type))
3257 {
3258 }
3259
3261 {
3263 }
3264
3265 const variablest &variables() const
3266 {
3268 }
3269
3271 {
3272 return op1();
3273 }
3274
3275 const exprt &where() const
3276 {
3277 return op1();
3278 }
3279
3282 exprt instantiate(const exprt::operandst &) const;
3283
3286 exprt instantiate(const variablest &) const;
3287};
3288
3289template <>
3290inline bool can_cast_expr<binding_exprt>(const exprt &base)
3291{
3292 return base.id() == ID_forall || base.id() == ID_exists ||
3293 base.id() == ID_lambda || base.id() == ID_array_comprehension;
3294}
3295
3296inline void validate_expr(const binding_exprt &binding_expr)
3297{
3299 binding_expr, 2, "Binding expressions must have two operands");
3300}
3301
3308inline const binding_exprt &to_binding_expr(const exprt &expr)
3309{
3311 expr.id() == ID_forall || expr.id() == ID_exists ||
3312 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3313 const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
3314 validate_expr(ret);
3315 return ret;
3316}
3317
3325{
3327 expr.id() == ID_forall || expr.id() == ID_exists ||
3328 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3329 binding_exprt &ret = static_cast<binding_exprt &>(expr);
3330 validate_expr(ret);
3331 return ret;
3332}
3333
3336{
3337public:
3341 const exprt &where)
3342 : binary_exprt(
3344 ID_let_binding,
3345 std::move(variables),
3346 where,
3347 where.type()),
3348 ID_let,
3349 multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
3350 where.type())
3351 {
3352 PRECONDITION(this->variables().size() == this->values().size());
3353 }
3354
3357 : let_exprt(
3359 operandst{std::move(value)},
3360 where)
3361 {
3362 }
3363
3365 {
3366 return static_cast<binding_exprt &>(op0());
3367 }
3368
3369 const binding_exprt &binding() const
3370 {
3371 return static_cast<const binding_exprt &>(op0());
3372 }
3373
3376 {
3377 auto &variables = binding().variables();
3378 PRECONDITION(variables.size() == 1);
3379 return variables.front();
3380 }
3381
3383 const symbol_exprt &symbol() const
3384 {
3385 const auto &variables = binding().variables();
3386 PRECONDITION(variables.size() == 1);
3387 return variables.front();
3388 }
3389
3392 {
3393 auto &values = this->values();
3394 PRECONDITION(values.size() == 1);
3395 return values.front();
3396 }
3397
3399 const exprt &value() const
3400 {
3401 const auto &values = this->values();
3402 PRECONDITION(values.size() == 1);
3403 return values.front();
3404 }
3405
3407 {
3408 return static_cast<multi_ary_exprt &>(op1()).operands();
3409 }
3410
3411 const operandst &values() const
3412 {
3413 return static_cast<const multi_ary_exprt &>(op1()).operands();
3414 }
3415
3418 {
3419 return binding().variables();
3420 }
3421
3424 {
3425 return binding().variables();
3426 }
3427
3430 {
3431 return binding().where();
3432 }
3433
3435 const exprt &where() const
3436 {
3437 return binding().where();
3438 }
3439
3440 static void validate(const exprt &, validation_modet);
3441};
3442
3443template <>
3444inline bool can_cast_expr<let_exprt>(const exprt &base)
3445{
3446 return base.id() == ID_let;
3447}
3448
3449inline void validate_expr(const let_exprt &let_expr)
3450{
3451 validate_operands(let_expr, 2, "Let must have two operands");
3452}
3453
3460inline const let_exprt &to_let_expr(const exprt &expr)
3461{
3462 PRECONDITION(expr.id()==ID_let);
3463 const let_exprt &ret = static_cast<const let_exprt &>(expr);
3464 validate_expr(ret);
3465 return ret;
3466}
3467
3470{
3471 PRECONDITION(expr.id()==ID_let);
3472 let_exprt &ret = static_cast<let_exprt &>(expr);
3473 validate_expr(ret);
3474 return ret;
3475}
3476
3477
3482{
3483public:
3484 cond_exprt(operandst _operands, typet _type)
3485 : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3486 {
3487 }
3488
3492 void add_case(const exprt &condition, const exprt &value)
3493 {
3494 PRECONDITION(condition.is_boolean());
3495 operands().reserve(operands().size() + 2);
3496 operands().push_back(condition);
3497 operands().push_back(value);
3498 }
3499
3500 // a lowering to nested if_exprt
3501 exprt lower() const;
3502};
3503
3504template <>
3505inline bool can_cast_expr<cond_exprt>(const exprt &base)
3506{
3507 return base.id() == ID_cond;
3508}
3509
3510inline void validate_expr(const cond_exprt &value)
3511{
3513 value.operands().size() % 2 == 0, "cond must have even number of operands");
3514}
3515
3522inline const cond_exprt &to_cond_expr(const exprt &expr)
3523{
3524 PRECONDITION(expr.id() == ID_cond);
3525 const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3526 validate_expr(ret);
3527 return ret;
3528}
3529
3532{
3533 PRECONDITION(expr.id() == ID_cond);
3534 cond_exprt &ret = static_cast<cond_exprt &>(expr);
3535 validate_expr(ret);
3536 return ret;
3537}
3538
3548{
3549public:
3552 exprt body,
3553 array_typet _type)
3554 : binding_exprt(
3555 ID_array_comprehension,
3556 {std::move(arg)},
3557 std::move(body),
3558 std::move(_type))
3559 {
3560 }
3561
3562 const array_typet &type() const
3563 {
3564 return static_cast<const array_typet &>(binary_exprt::type());
3565 }
3566
3568 {
3569 return static_cast<array_typet &>(binary_exprt::type());
3570 }
3571
3572 const symbol_exprt &arg() const
3573 {
3574 auto &variables = this->variables();
3575 PRECONDITION(variables.size() == 1);
3576 return variables[0];
3577 }
3578
3580 {
3581 auto &variables = this->variables();
3582 PRECONDITION(variables.size() == 1);
3583 return variables[0];
3584 }
3585
3586 const exprt &body() const
3587 {
3588 return where();
3589 }
3590
3592 {
3593 return where();
3594 }
3595};
3596
3597template <>
3599{
3600 return base.id() == ID_array_comprehension;
3601}
3602
3604{
3605 validate_operands(value, 2, "'Array comprehension' must have two operands");
3606}
3607
3614inline const array_comprehension_exprt &
3616{
3617 PRECONDITION(expr.id() == ID_array_comprehension);
3618 const array_comprehension_exprt &ret =
3619 static_cast<const array_comprehension_exprt &>(expr);
3620 validate_expr(ret);
3621 return ret;
3622}
3623
3626{
3627 PRECONDITION(expr.id() == ID_array_comprehension);
3629 static_cast<array_comprehension_exprt &>(expr);
3630 validate_expr(ret);
3631 return ret;
3632}
3633
3634inline void validate_expr(const class class_method_descriptor_exprt &value);
3635
3638{
3639public:
3655 typet _type,
3659 : nullary_exprt(ID_virtual_function, std::move(_type))
3660 {
3662 set(ID_component_name, std::move(mangled_method_name));
3663 set(ID_C_class, std::move(class_id));
3664 set(ID_C_base_name, std::move(base_method_name));
3665 set(ID_identifier, std::move(id));
3666 validate_expr(*this);
3667 }
3668
3676 {
3677 return get(ID_component_name);
3678 }
3679
3683 const irep_idt &class_id() const
3684 {
3685 return get(ID_C_class);
3686 }
3687
3691 {
3692 return get(ID_C_base_name);
3693 }
3694
3699 {
3700 return get(ID_identifier);
3701 }
3702};
3703
3704inline void validate_expr(const class class_method_descriptor_exprt &value)
3705{
3706 validate_operands(value, 0, "class method descriptor must not have operands");
3708 !value.mangled_method_name().empty(),
3709 "class method descriptor must have a mangled method name.");
3711 !value.class_id().empty(), "class method descriptor must have a class id.");
3713 !value.base_method_name().empty(),
3714 "class method descriptor must have a base method name.");
3716 value.get_identifier() == id2string(value.class_id()) + "." +
3718 "class method descriptor must have an identifier in the expected format.");
3719}
3720
3727inline const class_method_descriptor_exprt &
3729{
3730 PRECONDITION(expr.id() == ID_virtual_function);
3732 return static_cast<const class_method_descriptor_exprt &>(expr);
3733}
3734
3735template <>
3737{
3738 return base.id() == ID_virtual_function;
3739}
3740
3747{
3748public:
3750 : binary_exprt(
3751 std::move(symbol),
3752 ID_named_term,
3753 value, // not moved, for type
3754 value.type())
3755 {
3756 PRECONDITION(symbol.type() == type());
3757 }
3758
3759 const symbol_exprt &symbol() const
3760 {
3761 return static_cast<const symbol_exprt &>(op0());
3762 }
3763
3765 {
3766 return static_cast<symbol_exprt &>(op0());
3767 }
3768
3769 const exprt &value() const
3770 {
3771 return op1();
3772 }
3773
3775 {
3776 return op1();
3777 }
3778};
3779
3780template <>
3782{
3783 return base.id() == ID_named_term;
3784}
3785
3786inline void validate_expr(const named_term_exprt &value)
3787{
3788 validate_operands(value, 2, "'named term' must have two operands");
3789}
3790
3798{
3799 PRECONDITION(expr.id() == ID_named_term);
3800 const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
3801 validate_expr(ret);
3802 return ret;
3803}
3804
3807{
3808 PRECONDITION(expr.id() == ID_named_term);
3809 named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
3810 validate_expr(ret);
3811 return ret;
3812}
3813
3814#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:3548
const array_typet & type() const
Definition std_expr.h:3562
const symbol_exprt & arg() const
Definition std_expr.h:3572
const exprt & body() const
Definition std_expr.h:3586
array_typet & type()
Definition std_expr.h:3567
symbol_exprt & arg()
Definition std_expr.h:3579
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition std_expr.h:3550
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:3239
const variablest & variables() const
Definition std_expr.h:3265
const exprt & where() const
Definition std_expr.h:3275
exprt & where()
Definition std_expr.h:3270
variablest & variables()
Definition std_expr.h:3260
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition std_expr.h:3244
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:250
std::vector< symbol_exprt > variablest
Definition std_expr.h:3241
The Boolean type.
Definition std_types.h:36
An expression describing a method on a class.
Definition std_expr.h:3638
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:3690
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition std_expr.h:3675
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:3698
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition std_expr.h:3654
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:3683
Complex constructor from a pair of numbers.
Definition std_expr.h:1916
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition std_expr.h:1918
exprt real()
Definition std_expr.h:1927
exprt imag()
Definition std_expr.h:1937
const exprt & real() const
Definition std_expr.h:1932
const exprt & imag() const
Definition std_expr.h:1942
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
complex_imag_exprt(const exprt &op)
Definition std_expr.h:2029
Real part of the expression describing a complex number.
Definition std_expr.h:1984
complex_real_exprt(const exprt &op)
Definition std_expr.h:1986
Complex numbers made of pair of given subtype.
Definition std_types.h:1133
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition std_expr.h:3482
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition std_expr.h:3492
cond_exprt(operandst _operands, typet _type)
Definition std_expr.h:3484
exprt lower() const
Definition std_expr.cpp:289
A constant literal expression.
Definition std_expr.h:3122
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:3151
const irep_idt & get_value() const
Definition std_expr.h:3130
bool value_is_zero_string() const
Definition std_expr.cpp:19
constant_exprt(const irep_idt &_value, typet _type)
Definition std_expr.h:3124
void set_value(const irep_idt &value)
Definition std_expr.h:3135
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:2502
const exprt & false_case() const
Definition std_expr.h:2544
exprt & cond()
Definition std_expr.h:2519
const exprt & cond() const
Definition std_expr.h:2524
if_exprt(exprt cond, const exprt &t, exprt f)
Definition std_expr.h:2504
const exprt & true_case() const
Definition std_expr.h:2534
exprt & false_case()
Definition std_expr.h:2539
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition std_expr.h:2509
exprt & true_case()
Definition std_expr.h:2529
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2549
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2556
Boolean implication.
Definition std_expr.h:2230
implies_exprt(exprt op0, exprt op1)
Definition std_expr.h:2232
const exprt & index() const
Definition std_expr.h:2690
index_designatort(exprt _index)
Definition std_expr.h:2685
exprt & index()
Definition std_expr.h:2695
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:3231
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:3336
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3417
const binding_exprt & binding() const
Definition std_expr.h:3369
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition std_expr.h:3423
operandst & values()
Definition std_expr.h:3406
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition std_expr.h:3356
const exprt & where() const
convenience accessor for binding().where()
Definition std_expr.h:3435
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:193
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition std_expr.h:3383
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition std_expr.h:3338
exprt & value()
convenience accessor for the value of a single binding
Definition std_expr.h:3391
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3429
binding_exprt & binding()
Definition std_expr.h:3364
const operandst & values() const
Definition std_expr.h:3411
const exprt & value() const
convenience accessor for the value of a single binding
Definition std_expr.h:3399
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition std_expr.h:3375
irep_idt get_component_name() const
Definition std_expr.h:2744
member_designatort(const irep_idt &_component_name)
Definition std_expr.h:2738
Extract member of struct or union.
Definition std_expr.h:2976
const exprt & compound() const
Definition std_expr.h:3025
exprt & struct_op()
Definition std_expr.h:3020
const exprt & struct_op() const
Definition std_expr.h:3014
irep_idt get_component_name() const
Definition std_expr.h:2998
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:3003
exprt & compound()
Definition std_expr.h:3030
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
Definition std_expr.cpp:158
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:3035
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition std_expr.h:2978
std::size_t get_component_number() const
Definition std_expr.h:3008
member_exprt(exprt op, const struct_typet::componentt &c)
Definition std_expr.h:2988
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:3747
named_term_exprt(symbol_exprt symbol, exprt value)
Definition std_expr.h:3749
symbol_exprt & symbol()
Definition std_expr.h:3764
const exprt & value() const
Definition std_expr.h:3769
const symbol_exprt & symbol() const
Definition std_expr.h:3759
exprt & value()
Definition std_expr.h:3774
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean NAND.
Definition std_expr.h:2196
nand_exprt(exprt op0, exprt op1)
Definition std_expr.h:2198
nand_exprt(exprt::operandst _operands)
Definition std_expr.h:2203
Expression to hold a nondeterministic choice.
Definition std_expr.h:292
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:315
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:296
const irep_idt & get_identifier() const
Definition std_expr.h:320
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition std_expr.h:305
Boolean NOR.
Definition std_expr.h:2341
nor_exprt(exprt op0, exprt op1)
Definition std_expr.h:2343
nor_exprt(exprt::operandst _operands)
Definition std_expr.h:2348
Boolean negation.
Definition std_expr.h:2459
not_exprt(exprt _op)
Definition std_expr.h:2461
Disequality.
Definition std_expr.h:1425
notequal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1427
exprt & op0()=delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:29
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:39
const exprt & op1() const =delete
nullary_exprt(const irep_idt &_id, typet _type)
Definition std_expr.h:24
const exprt & op0() const =delete
void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete
exprt & op3()=delete
void copy_to_operands(const exprt &expr)=delete
operandst & operands()=delete
remove all operand methods
void copy_to_operands(const exprt &, const exprt &)=delete
const operandst & operands() const =delete
exprt & op1()=delete
exprt & op2()=delete
const exprt & op3() const =delete
const exprt & op2() const =delete
Boolean OR.
Definition std_expr.h:2275
or_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2282
or_exprt(exprt::operandst _operands)
Definition std_expr.h:2298
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2290
or_exprt(exprt op0, exprt op1)
Definition std_expr.h:2277
The plus expression Associativity is not specified.
Definition std_expr.h:1002
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition std_expr.h:1009
plus_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1004
plus_exprt(operandst _operands, typet _type)
Definition std_expr.h:1018
predicate_exprt(const irep_idt &_id)
Definition std_expr.h:576
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:596
sign_exprt(exprt _op)
Definition std_expr.h:598
Struct constructor from list of elements.
Definition std_expr.h:1877
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:139
struct_exprt(operandst _operands, typet _type)
Definition std_expr.h:1879
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:3086
type_exprt(typet type)
Definition std_expr.h:3088
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:2787
exprt & old()
Definition std_expr.h:2799
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
Definition std_expr.cpp:219
exprt::operandst & designator()
Definition std_expr.h:2813
exprt & new_value()
Definition std_expr.h:2823
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2843
const exprt & new_value() const
Definition std_expr.h:2828
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition std_expr.h:2789
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2836
const exprt & old() const
Definition std_expr.h:2804
const exprt::operandst & designator() const
Definition std_expr.h:2818
Vector constructor from list of elements.
Definition std_expr.h:1734
vector_exprt(operandst _operands, vector_typet _type)
Definition std_expr.h:1736
The vector type.
Definition std_types.h:1064
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
const exprt & old() const
Definition std_expr.h:2618
const exprt & where() const
Definition std_expr.h:2628
exprt & new_value()
Definition std_expr.h:2633
exprt & where()
Definition std_expr.h:2623
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition std_expr.h:2605
const exprt & new_value() const
Definition std_expr.h:2638
exprt & old()
Definition std_expr.h:2613
Boolean XNOR.
Definition std_expr.h:2419
xnor_exprt(exprt::operandst _operands)
Definition std_expr.h:2426
xnor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2421
Boolean XOR.
Definition std_expr.h:2375
xor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2377
xor_exprt(exprt::operandst _operands)
Definition std_expr.h:2382
Templated functions to cast to specific exprt-derived classes.
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:2468
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1900
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition std_expr.h:1716
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition std_expr.h:2091
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition std_expr.h:3105
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1603
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition std_expr.h:1889
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition std_expr.h:556
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition std_expr.h:2389
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition std_expr.h:1121
bool can_cast_expr< if_exprt >(const exprt &base)
Definition std_expr.h:2566
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
Definition std_expr.h:3728
bool can_cast_expr< named_term_exprt >(const exprt &base)
Definition std_expr.h:3781
bool can_cast_expr< binding_exprt >(const exprt &base)
Definition std_expr.h:3290
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1277
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1137
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition std_expr.h:2177
bool can_cast_expr< member_designatort >(const exprt &base)
Definition std_expr.h:2751
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3615
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:3797
const xnor_exprt & to_xnor_expr(const exprt &expr)
Cast an exprt to a xnor_exprt.
Definition std_expr.h:2444
bool can_cast_expr< xnor_exprt >(const exprt &base)
Definition std_expr.h:2433
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition std_expr.h:3598
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition std_expr.h:2400
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2322
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition std_expr.h:2036
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition std_expr.h:450
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition std_expr.h:605
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition std_expr.h:3522
bool can_cast_expr< type_exprt >(const exprt &base)
Definition std_expr.h:3094
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:3736
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
void validate_expr(const symbol_exprt &value)
Definition std_expr.h:261
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1206
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition std_expr.h:498
bool can_cast_expr< less_than_exprt >(const exprt &base)
Definition std_expr.h:858
bool can_cast_expr< with_exprt >(const exprt &base)
Definition std_expr.h:2645
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition std_expr.h:1754
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:106
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition std_expr.h:1070
bool can_cast_expr< let_exprt >(const exprt &base)
Definition std_expr.h:3444
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition std_expr.h:1450
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition std_expr.h:1025
const nand_exprt & to_nand_expr(const exprt &expr)
Cast an exprt to a nand_exprt.
Definition std_expr.h:2215
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition std_expr.h:1587
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3460
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:3161
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3068
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:3052
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:3308
bool can_cast_expr< or_exprt >(const exprt &base)
Definition std_expr.h:2311
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition std_expr.h:1261
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2718
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:3505
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:2853
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:3177
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:2702
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2484
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2665
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1965
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition std_expr.h:540
bool can_cast_expr< and_exprt >(const exprt &base)
Definition std_expr.h:2166
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition std_expr.h:816
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2255
bool can_cast_expr< array_exprt >(const exprt &base)
Definition std_expr.h:1654
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition std_expr.h:699
bool can_cast_expr< div_exprt >(const exprt &base)
Definition std_expr.h:1190
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2870
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition std_expr.h:3222
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:514
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
Definition std_expr.h:837
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition std_expr.h:2239
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition std_expr.h:410
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
Definition std_expr.h:879
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition std_expr.h:343
bool can_cast_expr< union_exprt >(const exprt &base)
Definition std_expr.h:1800
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition std_expr.h:2767
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition std_expr.h:1993
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition std_expr.h:621
const nor_exprt & to_nor_expr(const exprt &expr)
Cast an exprt to a nor_exprt.
Definition std_expr.h:2360
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition std_expr.h:1345
Pre-defined types.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
size_t operator()(const ::symbol_exprt &sym)
Definition std_expr.h:205
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
validation_modet
dstringt irep_idt