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};
1114
1115template <>
1116inline bool can_cast_expr<mult_exprt>(const exprt &base)
1117{
1118 return base.id() == ID_mult;
1119}
1120
1121inline void validate_expr(const mult_exprt &value)
1122{
1123 validate_operands(value, 2, "Multiply must have two or more operands", true);
1124}
1125
1132inline const mult_exprt &to_mult_expr(const exprt &expr)
1133{
1134 PRECONDITION(expr.id()==ID_mult);
1135 const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1136 validate_expr(ret);
1137 return ret;
1138}
1139
1142{
1143 PRECONDITION(expr.id()==ID_mult);
1144 mult_exprt &ret = static_cast<mult_exprt &>(expr);
1145 validate_expr(ret);
1146 return ret;
1147}
1148
1149
1152{
1153public:
1155 : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1156 {
1157 }
1158
1161 {
1162 return op0();
1163 }
1164
1166 const exprt &dividend() const
1167 {
1168 return op0();
1169 }
1170
1173 {
1174 return op1();
1175 }
1176
1178 const exprt &divisor() const
1179 {
1180 return op1();
1181 }
1182};
1183
1184template <>
1185inline bool can_cast_expr<div_exprt>(const exprt &base)
1186{
1187 return base.id() == ID_div;
1188}
1189
1190inline void validate_expr(const div_exprt &value)
1191{
1192 validate_operands(value, 2, "Divide must have two operands");
1193}
1194
1201inline const div_exprt &to_div_expr(const exprt &expr)
1202{
1203 PRECONDITION(expr.id()==ID_div);
1204 const div_exprt &ret = static_cast<const div_exprt &>(expr);
1205 validate_expr(ret);
1206 return ret;
1207}
1208
1211{
1212 PRECONDITION(expr.id()==ID_div);
1213 div_exprt &ret = static_cast<div_exprt &>(expr);
1214 validate_expr(ret);
1215 return ret;
1216}
1217
1223{
1224public:
1226 : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1227 {
1228 }
1229
1232 {
1233 return op0();
1234 }
1235
1237 const exprt &dividend() const
1238 {
1239 return op0();
1240 }
1241
1244 {
1245 return op1();
1246 }
1247
1249 const exprt &divisor() const
1250 {
1251 return op1();
1252 }
1253};
1254
1255template <>
1256inline bool can_cast_expr<mod_exprt>(const exprt &base)
1257{
1258 return base.id() == ID_mod;
1259}
1260
1261inline void validate_expr(const mod_exprt &value)
1262{
1263 validate_operands(value, 2, "Modulo must have two operands");
1264}
1265
1272inline const mod_exprt &to_mod_expr(const exprt &expr)
1273{
1274 PRECONDITION(expr.id()==ID_mod);
1275 const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1276 validate_expr(ret);
1277 return ret;
1278}
1279
1282{
1283 PRECONDITION(expr.id()==ID_mod);
1284 mod_exprt &ret = static_cast<mod_exprt &>(expr);
1285 validate_expr(ret);
1286 return ret;
1287}
1288
1291{
1292public:
1294 : binary_exprt(std::move(_lhs), ID_euclidean_mod, std::move(_rhs))
1295 {
1296 }
1297
1300 {
1301 return op0();
1302 }
1303
1305 const exprt &dividend() const
1306 {
1307 return op0();
1308 }
1309
1312 {
1313 return op1();
1314 }
1315
1317 const exprt &divisor() const
1318 {
1319 return op1();
1320 }
1321};
1322
1323template <>
1325{
1326 return base.id() == ID_euclidean_mod;
1327}
1328
1329inline void validate_expr(const euclidean_mod_exprt &value)
1330{
1331 validate_operands(value, 2, "Modulo must have two operands");
1332}
1333
1341{
1342 PRECONDITION(expr.id() == ID_euclidean_mod);
1343 const euclidean_mod_exprt &ret =
1344 static_cast<const euclidean_mod_exprt &>(expr);
1345 validate_expr(ret);
1346 return ret;
1347}
1348
1351{
1352 PRECONDITION(expr.id() == ID_euclidean_mod);
1353 euclidean_mod_exprt &ret = static_cast<euclidean_mod_exprt &>(expr);
1354 validate_expr(ret);
1355 return ret;
1356}
1357
1358
1361{
1362public:
1364 : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1365 {
1366 PRECONDITION(lhs().type() == rhs().type());
1367 }
1368
1369 static void check(
1370 const exprt &expr,
1372 {
1374 }
1375
1376 static void validate(
1377 const exprt &expr,
1378 const namespacet &ns,
1380 {
1381 binary_relation_exprt::validate(expr, ns, vm);
1382 }
1383};
1384
1385template <>
1386inline bool can_cast_expr<equal_exprt>(const exprt &base)
1387{
1388 return base.id() == ID_equal;
1389}
1390
1391inline void validate_expr(const equal_exprt &value)
1392{
1393 equal_exprt::check(value);
1394}
1395
1402inline const equal_exprt &to_equal_expr(const exprt &expr)
1403{
1404 PRECONDITION(expr.id()==ID_equal);
1405 equal_exprt::check(expr);
1406 return static_cast<const equal_exprt &>(expr);
1407}
1408
1411{
1412 PRECONDITION(expr.id()==ID_equal);
1413 equal_exprt::check(expr);
1414 return static_cast<equal_exprt &>(expr);
1415}
1416
1417
1420{
1421public:
1423 : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1424 {
1425 }
1426};
1427
1428template <>
1429inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1430{
1431 return base.id() == ID_notequal;
1432}
1433
1434inline void validate_expr(const notequal_exprt &value)
1435{
1436 validate_operands(value, 2, "Inequality must have two operands");
1437}
1438
1445inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1446{
1447 PRECONDITION(expr.id()==ID_notequal);
1448 const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1449 validate_expr(ret);
1450 return ret;
1451}
1452
1455{
1456 PRECONDITION(expr.id()==ID_notequal);
1457 notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1458 validate_expr(ret);
1459 return ret;
1460}
1461
1462
1465{
1466public:
1467 // _array must have either index or vector type.
1468 // When _array has array_type, the type of _index
1469 // must be array_type.index_type().
1470 // This will eventually be enforced using a precondition.
1471 index_exprt(const exprt &_array, exprt _index)
1472 : binary_exprt(
1473 _array,
1474 ID_index,
1475 std::move(_index),
1476 to_type_with_subtype(_array.type()).subtype())
1477 {
1478 const auto &array_op_type = _array.type();
1480 array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1481 }
1482
1483 index_exprt(exprt _array, exprt _index, typet _type)
1484 : binary_exprt(
1485 std::move(_array),
1486 ID_index,
1487 std::move(_index),
1488 std::move(_type))
1489 {
1490 const auto &array_op_type = array().type();
1492 array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1493 }
1494
1496 {
1497 return op0();
1498 }
1499
1500 const exprt &array() const
1501 {
1502 return op0();
1503 }
1504
1506 {
1507 return op1();
1508 }
1509
1510 const exprt &index() const
1511 {
1512 return op1();
1513 }
1514};
1515
1516template <>
1517inline bool can_cast_expr<index_exprt>(const exprt &base)
1518{
1519 return base.id() == ID_index;
1520}
1521
1522inline void validate_expr(const index_exprt &value)
1523{
1524 validate_operands(value, 2, "Array index must have two operands");
1525}
1526
1533inline const index_exprt &to_index_expr(const exprt &expr)
1534{
1535 PRECONDITION(expr.id()==ID_index);
1536 const index_exprt &ret = static_cast<const index_exprt &>(expr);
1537 validate_expr(ret);
1538 return ret;
1539}
1540
1543{
1544 PRECONDITION(expr.id()==ID_index);
1545 index_exprt &ret = static_cast<index_exprt &>(expr);
1546 validate_expr(ret);
1547 return ret;
1548}
1549
1550
1553{
1554public:
1555 explicit array_of_exprt(exprt _what, array_typet _type)
1556 : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1557 {
1558 }
1559
1560 const array_typet &type() const
1561 {
1562 return static_cast<const array_typet &>(unary_exprt::type());
1563 }
1564
1566 {
1567 return static_cast<array_typet &>(unary_exprt::type());
1568 }
1569
1571 {
1572 return op0();
1573 }
1574
1575 const exprt &what() const
1576 {
1577 return op0();
1578 }
1579};
1580
1581template <>
1582inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1583{
1584 return base.id() == ID_array_of;
1585}
1586
1587inline void validate_expr(const array_of_exprt &value)
1588{
1589 validate_operands(value, 1, "'Array of' must have one operand");
1590}
1591
1598inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1599{
1600 PRECONDITION(expr.id()==ID_array_of);
1602 return static_cast<const array_of_exprt &>(expr);
1603}
1604
1607{
1608 PRECONDITION(expr.id()==ID_array_of);
1610 return static_cast<array_of_exprt &>(expr);
1611}
1612
1613
1616{
1617public:
1619 : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1620 {
1621 }
1622
1623 const array_typet &type() const
1624 {
1625 return static_cast<const array_typet &>(multi_ary_exprt::type());
1626 }
1627
1629 {
1630 return static_cast<array_typet &>(multi_ary_exprt::type());
1631 }
1632
1634 {
1635 if(other.source_location().is_not_nil())
1636 add_source_location() = other.source_location();
1637 return *this;
1638 }
1639
1641 {
1642 if(other.source_location().is_not_nil())
1643 add_source_location() = other.source_location();
1644 return std::move(*this);
1645 }
1646};
1647
1648template <>
1649inline bool can_cast_expr<array_exprt>(const exprt &base)
1650{
1651 return base.id() == ID_array;
1652}
1653
1660inline const array_exprt &to_array_expr(const exprt &expr)
1661{
1662 PRECONDITION(expr.id()==ID_array);
1663 return static_cast<const array_exprt &>(expr);
1664}
1665
1668{
1669 PRECONDITION(expr.id()==ID_array);
1670 return static_cast<array_exprt &>(expr);
1671}
1672
1676{
1677public:
1679 : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1680 {
1681 }
1682
1683 const array_typet &type() const
1684 {
1685 return static_cast<const array_typet &>(multi_ary_exprt::type());
1686 }
1687
1689 {
1690 return static_cast<array_typet &>(multi_ary_exprt::type());
1691 }
1692
1694 void add(exprt index, exprt value)
1695 {
1696 add_to_operands(std::move(index), std::move(value));
1697 }
1698};
1699
1700template <>
1702{
1703 return base.id() == ID_array_list;
1704}
1705
1706inline void validate_expr(const array_list_exprt &value)
1707{
1708 PRECONDITION(value.operands().size() % 2 == 0);
1709}
1710
1712{
1714 auto &ret = static_cast<const array_list_exprt &>(expr);
1715 validate_expr(ret);
1716 return ret;
1717}
1718
1720{
1722 auto &ret = static_cast<array_list_exprt &>(expr);
1723 validate_expr(ret);
1724 return ret;
1725}
1726
1729{
1730public:
1732 : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1733 {
1734 }
1735};
1736
1737template <>
1738inline bool can_cast_expr<vector_exprt>(const exprt &base)
1739{
1740 return base.id() == ID_vector;
1741}
1742
1749inline const vector_exprt &to_vector_expr(const exprt &expr)
1750{
1751 PRECONDITION(expr.id()==ID_vector);
1752 return static_cast<const vector_exprt &>(expr);
1753}
1754
1757{
1758 PRECONDITION(expr.id()==ID_vector);
1759 return static_cast<vector_exprt &>(expr);
1760}
1761
1762
1765{
1766public:
1767 union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1768 : unary_exprt(ID_union, std::move(_value), std::move(_type))
1769 {
1770 set_component_name(_component_name);
1771 }
1772
1774 {
1775 return get(ID_component_name);
1776 }
1777
1778 void set_component_name(const irep_idt &component_name)
1779 {
1780 set(ID_component_name, component_name);
1781 }
1782
1783 std::size_t get_component_number() const
1784 {
1785 return get_size_t(ID_component_number);
1786 }
1787
1788 void set_component_number(std::size_t component_number)
1789 {
1790 set_size_t(ID_component_number, component_number);
1791 }
1792};
1793
1794template <>
1795inline bool can_cast_expr<union_exprt>(const exprt &base)
1796{
1797 return base.id() == ID_union;
1798}
1799
1800inline void validate_expr(const union_exprt &value)
1801{
1802 validate_operands(value, 1, "Union constructor must have one operand");
1803}
1804
1811inline const union_exprt &to_union_expr(const exprt &expr)
1812{
1813 PRECONDITION(expr.id()==ID_union);
1814 union_exprt::check(expr);
1815 return static_cast<const union_exprt &>(expr);
1816}
1817
1820{
1821 PRECONDITION(expr.id()==ID_union);
1822 union_exprt::check(expr);
1823 return static_cast<union_exprt &>(expr);
1824}
1825
1829{
1830public:
1831 explicit empty_union_exprt(typet _type)
1832 : nullary_exprt(ID_empty_union, std::move(_type))
1833 {
1834 }
1835};
1836
1837template <>
1839{
1840 return base.id() == ID_empty_union;
1841}
1842
1843inline void validate_expr(const empty_union_exprt &value)
1844{
1846 value, 0, "Empty-union constructor must not have any operand");
1847}
1848
1856{
1857 PRECONDITION(expr.id() == ID_empty_union);
1859 return static_cast<const empty_union_exprt &>(expr);
1860}
1861
1864{
1865 PRECONDITION(expr.id() == ID_empty_union);
1867 return static_cast<empty_union_exprt &>(expr);
1868}
1869
1872{
1873public:
1874 struct_exprt(operandst _operands, typet _type)
1875 : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1876 {
1877 }
1878
1879 exprt &component(const irep_idt &name, const namespacet &ns);
1880 const exprt &component(const irep_idt &name, const namespacet &ns) const;
1881};
1882
1883template <>
1884inline bool can_cast_expr<struct_exprt>(const exprt &base)
1885{
1886 return base.id() == ID_struct;
1887}
1888
1895inline const struct_exprt &to_struct_expr(const exprt &expr)
1896{
1897 PRECONDITION(expr.id()==ID_struct);
1898 return static_cast<const struct_exprt &>(expr);
1899}
1900
1903{
1904 PRECONDITION(expr.id()==ID_struct);
1905 return static_cast<struct_exprt &>(expr);
1906}
1907
1908
1911{
1912public:
1914 : binary_exprt(
1915 std::move(_real),
1916 ID_complex,
1917 std::move(_imag),
1918 std::move(_type))
1919 {
1920 }
1921
1923 {
1924 return op0();
1925 }
1926
1927 const exprt &real() const
1928 {
1929 return op0();
1930 }
1931
1933 {
1934 return op1();
1935 }
1936
1937 const exprt &imag() const
1938 {
1939 return op1();
1940 }
1941};
1942
1943template <>
1944inline bool can_cast_expr<complex_exprt>(const exprt &base)
1945{
1946 return base.id() == ID_complex;
1947}
1948
1949inline void validate_expr(const complex_exprt &value)
1950{
1951 validate_operands(value, 2, "Complex constructor must have two operands");
1952}
1953
1960inline const complex_exprt &to_complex_expr(const exprt &expr)
1961{
1962 PRECONDITION(expr.id()==ID_complex);
1963 const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1964 validate_expr(ret);
1965 return ret;
1966}
1967
1970{
1971 PRECONDITION(expr.id()==ID_complex);
1972 complex_exprt &ret = static_cast<complex_exprt &>(expr);
1973 validate_expr(ret);
1974 return ret;
1975}
1976
1979{
1980public:
1981 explicit complex_real_exprt(const exprt &op)
1982 : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1983 {
1984 }
1985};
1986
1987template <>
1989{
1990 return base.id() == ID_complex_real;
1991}
1992
1993inline void validate_expr(const complex_real_exprt &expr)
1994{
1996 expr, 1, "real part retrieval operation must have one operand");
1997}
1998
2006{
2007 PRECONDITION(expr.id() == ID_complex_real);
2009 return static_cast<const complex_real_exprt &>(expr);
2010}
2011
2014{
2015 PRECONDITION(expr.id() == ID_complex_real);
2017 return static_cast<complex_real_exprt &>(expr);
2018}
2019
2022{
2023public:
2024 explicit complex_imag_exprt(const exprt &op)
2025 : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
2026 {
2027 }
2028};
2029
2030template <>
2032{
2033 return base.id() == ID_complex_imag;
2034}
2035
2036inline void validate_expr(const complex_imag_exprt &expr)
2037{
2039 expr, 1, "imaginary part retrieval operation must have one operand");
2040}
2041
2049{
2050 PRECONDITION(expr.id() == ID_complex_imag);
2051 const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
2052 validate_expr(ret);
2053 return ret;
2054}
2055
2058{
2059 PRECONDITION(expr.id() == ID_complex_imag);
2060 complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
2061 validate_expr(ret);
2062 return ret;
2063}
2064
2065
2068{
2069public:
2071 : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2072 {
2073 }
2074
2075 // returns a typecast if the type doesn't already match
2076 static exprt conditional_cast(const exprt &expr, const typet &type)
2077 {
2078 if(expr.type() == type)
2079 return expr;
2080 else
2081 return typecast_exprt(expr, type);
2082 }
2083};
2084
2085template <>
2086inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2087{
2088 return base.id() == ID_typecast;
2089}
2090
2091inline void validate_expr(const typecast_exprt &value)
2092{
2093 validate_operands(value, 1, "Typecast must have one operand");
2094}
2095
2102inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2103{
2104 PRECONDITION(expr.id()==ID_typecast);
2106 return static_cast<const typecast_exprt &>(expr);
2107}
2108
2111{
2112 PRECONDITION(expr.id()==ID_typecast);
2114 return static_cast<typecast_exprt &>(expr);
2115}
2116
2117
2120{
2121public:
2123 : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2124 {
2125 }
2126
2129 ID_and,
2130 {std::move(op0), std::move(op1), std::move(op2)},
2131 bool_typet())
2132 {
2133 }
2134
2137 ID_and,
2138 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2139 bool_typet())
2140 {
2141 }
2142
2143 explicit and_exprt(exprt::operandst _operands)
2144 : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2145 {
2146 }
2147};
2148
2152
2154
2155template <>
2156inline bool can_cast_expr<and_exprt>(const exprt &base)
2157{
2158 return base.id() == ID_and;
2159}
2160
2167inline const and_exprt &to_and_expr(const exprt &expr)
2168{
2169 PRECONDITION(expr.id()==ID_and);
2170 return static_cast<const and_exprt &>(expr);
2171}
2172
2175{
2176 PRECONDITION(expr.id()==ID_and);
2177 return static_cast<and_exprt &>(expr);
2178}
2179
2180
2183{
2184public:
2186 : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2187 {
2188 }
2189};
2190
2191template <>
2192inline bool can_cast_expr<implies_exprt>(const exprt &base)
2193{
2194 return base.id() == ID_implies;
2195}
2196
2197inline void validate_expr(const implies_exprt &value)
2198{
2199 validate_operands(value, 2, "Implies must have two operands");
2200}
2201
2208inline const implies_exprt &to_implies_expr(const exprt &expr)
2209{
2210 PRECONDITION(expr.id()==ID_implies);
2211 const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2212 validate_expr(ret);
2213 return ret;
2214}
2215
2218{
2219 PRECONDITION(expr.id()==ID_implies);
2220 implies_exprt &ret = static_cast<implies_exprt &>(expr);
2221 validate_expr(ret);
2222 return ret;
2223}
2224
2225
2228{
2229public:
2231 : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2232 {
2233 }
2234
2237 ID_or,
2238 {std::move(op0), std::move(op1), std::move(op2)},
2239 bool_typet())
2240 {
2241 }
2242
2245 ID_or,
2246 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2247 bool_typet())
2248 {
2249 }
2250
2251 explicit or_exprt(exprt::operandst _operands)
2252 : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2253 {
2254 }
2255};
2256
2260
2262
2263template <>
2264inline bool can_cast_expr<or_exprt>(const exprt &base)
2265{
2266 return base.id() == ID_or;
2267}
2268
2275inline const or_exprt &to_or_expr(const exprt &expr)
2276{
2277 PRECONDITION(expr.id()==ID_or);
2278 return static_cast<const or_exprt &>(expr);
2279}
2280
2283{
2284 PRECONDITION(expr.id()==ID_or);
2285 return static_cast<or_exprt &>(expr);
2286}
2287
2288
2291{
2292public:
2294 : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2295 {
2296 }
2297};
2298
2299template <>
2300inline bool can_cast_expr<xor_exprt>(const exprt &base)
2301{
2302 return base.id() == ID_xor;
2303}
2304
2311inline const xor_exprt &to_xor_expr(const exprt &expr)
2312{
2313 PRECONDITION(expr.id()==ID_xor);
2314 return static_cast<const xor_exprt &>(expr);
2315}
2316
2319{
2320 PRECONDITION(expr.id()==ID_xor);
2321 return static_cast<xor_exprt &>(expr);
2322}
2323
2324
2327{
2328public:
2329 explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2330 {
2331 PRECONDITION(as_const(*this).op().is_boolean());
2332 }
2333};
2334
2335template <>
2336inline bool can_cast_expr<not_exprt>(const exprt &base)
2337{
2338 return base.id() == ID_not;
2339}
2340
2341inline void validate_expr(const not_exprt &value)
2342{
2343 validate_operands(value, 1, "Not must have one operand");
2344}
2345
2352inline const not_exprt &to_not_expr(const exprt &expr)
2353{
2354 PRECONDITION(expr.id()==ID_not);
2355 not_exprt::check(expr);
2356 return static_cast<const not_exprt &>(expr);
2357}
2358
2361{
2362 PRECONDITION(expr.id()==ID_not);
2363 not_exprt::check(expr);
2364 return static_cast<not_exprt &>(expr);
2365}
2366
2367
2370{
2371public:
2373 : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2374 {
2375 }
2376
2378 : ternary_exprt(
2379 ID_if,
2380 std::move(cond),
2381 std::move(t),
2382 std::move(f),
2383 std::move(type))
2384 {
2385 }
2386
2388 {
2389 return op0();
2390 }
2391
2392 const exprt &cond() const
2393 {
2394 return op0();
2395 }
2396
2398 {
2399 return op1();
2400 }
2401
2402 const exprt &true_case() const
2403 {
2404 return op1();
2405 }
2406
2408 {
2409 return op2();
2410 }
2411
2412 const exprt &false_case() const
2413 {
2414 return op2();
2415 }
2416
2417 static void check(
2418 const exprt &expr,
2420 {
2421 ternary_exprt::check(expr, vm);
2422 }
2423
2424 static void validate(
2425 const exprt &expr,
2426 const namespacet &ns,
2428 {
2429 ternary_exprt::validate(expr, ns, vm);
2430 }
2431};
2432
2433template <>
2434inline bool can_cast_expr<if_exprt>(const exprt &base)
2435{
2436 return base.id() == ID_if;
2437}
2438
2439inline void validate_expr(const if_exprt &value)
2440{
2441 validate_operands(value, 3, "If-then-else must have three operands");
2442}
2443
2450inline const if_exprt &to_if_expr(const exprt &expr)
2451{
2452 PRECONDITION(expr.id()==ID_if);
2453 const if_exprt &ret = static_cast<const if_exprt &>(expr);
2454 validate_expr(ret);
2455 return ret;
2456}
2457
2460{
2461 PRECONDITION(expr.id()==ID_if);
2462 if_exprt &ret = static_cast<if_exprt &>(expr);
2463 validate_expr(ret);
2464 return ret;
2465}
2466
2471{
2472public:
2473 with_exprt(const exprt &_old, exprt _where, exprt _new_value)
2475 ID_with,
2476 _old.type(),
2477 {_old, std::move(_where), std::move(_new_value)})
2478 {
2479 }
2480
2482 {
2483 return op0();
2484 }
2485
2486 const exprt &old() const
2487 {
2488 return op0();
2489 }
2490
2492 {
2493 return op1();
2494 }
2495
2496 const exprt &where() const
2497 {
2498 return op1();
2499 }
2500
2502 {
2503 return op2();
2504 }
2505
2506 const exprt &new_value() const
2507 {
2508 return op2();
2509 }
2510};
2511
2512template <>
2513inline bool can_cast_expr<with_exprt>(const exprt &base)
2514{
2515 return base.id() == ID_with;
2516}
2517
2518inline void validate_expr(const with_exprt &value)
2519{
2521 value, 3, "array/structure update must have at least 3 operands", true);
2523 value.operands().size() % 2 == 1,
2524 "array/structure update must have an odd number of operands");
2525}
2526
2533inline const with_exprt &to_with_expr(const exprt &expr)
2534{
2535 PRECONDITION(expr.id()==ID_with);
2536 const with_exprt &ret = static_cast<const with_exprt &>(expr);
2537 validate_expr(ret);
2538 return ret;
2539}
2540
2543{
2544 PRECONDITION(expr.id()==ID_with);
2545 with_exprt &ret = static_cast<with_exprt &>(expr);
2546 validate_expr(ret);
2547 return ret;
2548}
2549
2551{
2552public:
2553 explicit index_designatort(exprt _index)
2554 : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
2555 {
2556 }
2557
2558 const exprt &index() const
2559 {
2560 return op0();
2561 }
2562
2564 {
2565 return op0();
2566 }
2567};
2568
2569template <>
2571{
2572 return base.id() == ID_index_designator;
2573}
2574
2575inline void validate_expr(const index_designatort &value)
2576{
2577 validate_operands(value, 1, "Index designator must have one operand");
2578}
2579
2587{
2588 PRECONDITION(expr.id()==ID_index_designator);
2589 const index_designatort &ret = static_cast<const index_designatort &>(expr);
2590 validate_expr(ret);
2591 return ret;
2592}
2593
2596{
2597 PRECONDITION(expr.id()==ID_index_designator);
2598 index_designatort &ret = static_cast<index_designatort &>(expr);
2599 validate_expr(ret);
2600 return ret;
2601}
2602
2604{
2605public:
2606 explicit member_designatort(const irep_idt &_component_name)
2607 : expr_protectedt(ID_member_designator, typet())
2608 {
2609 set(ID_component_name, _component_name);
2610 }
2611
2613 {
2614 return get(ID_component_name);
2615 }
2616};
2617
2618template <>
2620{
2621 return base.id() == ID_member_designator;
2622}
2623
2624inline void validate_expr(const member_designatort &value)
2625{
2626 validate_operands(value, 0, "Member designator must not have operands");
2627}
2628
2636{
2637 PRECONDITION(expr.id()==ID_member_designator);
2638 const member_designatort &ret = static_cast<const member_designatort &>(expr);
2639 validate_expr(ret);
2640 return ret;
2641}
2642
2645{
2646 PRECONDITION(expr.id()==ID_member_designator);
2647 member_designatort &ret = static_cast<member_designatort &>(expr);
2648 validate_expr(ret);
2649 return ret;
2650}
2651
2652
2655{
2656public:
2657 update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
2658 : ternary_exprt(
2659 ID_update,
2660 _old,
2661 std::move(_designator),
2662 std::move(_new_value),
2663 _old.type())
2664 {
2665 }
2666
2668 {
2669 return op0();
2670 }
2671
2672 const exprt &old() const
2673 {
2674 return op0();
2675 }
2676
2677 // the designator operands are either
2678 // 1) member_designator or
2679 // 2) index_designator
2680 // as defined above
2682 {
2683 return op1().operands();
2684 }
2685
2687 {
2688 return op1().operands();
2689 }
2690
2692 {
2693 return op2();
2694 }
2695
2696 const exprt &new_value() const
2697 {
2698 return op2();
2699 }
2700
2701 static void check(
2702 const exprt &expr,
2704 {
2705 ternary_exprt::check(expr, vm);
2706 }
2707
2708 static void validate(
2709 const exprt &expr,
2710 const namespacet &ns,
2712 {
2713 ternary_exprt::validate(expr, ns, vm);
2714 }
2715};
2716
2717template <>
2718inline bool can_cast_expr<update_exprt>(const exprt &base)
2719{
2720 return base.id() == ID_update;
2721}
2722
2723inline void validate_expr(const update_exprt &value)
2724{
2726 value, 3, "Array/structure update must have three operands");
2727}
2728
2735inline const update_exprt &to_update_expr(const exprt &expr)
2736{
2737 PRECONDITION(expr.id()==ID_update);
2738 const update_exprt &ret = static_cast<const update_exprt &>(expr);
2739 validate_expr(ret);
2740 return ret;
2741}
2742
2745{
2746 PRECONDITION(expr.id()==ID_update);
2747 update_exprt &ret = static_cast<update_exprt &>(expr);
2748 validate_expr(ret);
2749 return ret;
2750}
2751
2752
2753#if 0
2755class array_update_exprt:public expr_protectedt
2756{
2757public:
2758 array_update_exprt(
2759 const exprt &_array,
2760 const exprt &_index,
2761 const exprt &_new_value):
2762 exprt(ID_array_update, _array.type())
2763 {
2764 add_to_operands(_array, _index, _new_value);
2765 }
2766
2767 array_update_exprt():expr_protectedt(ID_array_update)
2768 {
2769 operands().resize(3);
2770 }
2771
2772 exprt &array()
2773 {
2774 return op0();
2775 }
2776
2777 const exprt &array() const
2778 {
2779 return op0();
2780 }
2781
2782 exprt &index()
2783 {
2784 return op1();
2785 }
2786
2787 const exprt &index() const
2788 {
2789 return op1();
2790 }
2791
2792 exprt &new_value()
2793 {
2794 return op2();
2795 }
2796
2797 const exprt &new_value() const
2798 {
2799 return op2();
2800 }
2801};
2802
2803template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2804{
2805 return base.id()==ID_array_update;
2806}
2807
2808inline void validate_expr(const array_update_exprt &value)
2809{
2810 validate_operands(value, 3, "Array update must have three operands");
2811}
2812
2819inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2820{
2821 PRECONDITION(expr.id()==ID_array_update);
2822 const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2823 validate_expr(ret);
2824 return ret;
2825}
2826
2828inline array_update_exprt &to_array_update_expr(exprt &expr)
2829{
2830 PRECONDITION(expr.id()==ID_array_update);
2831 array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2832 validate_expr(ret);
2833 return ret;
2834}
2835
2836#endif
2837
2838
2841{
2842public:
2843 member_exprt(exprt op, const irep_idt &component_name, typet _type)
2844 : unary_exprt(ID_member, std::move(op), std::move(_type))
2845 {
2846 const auto &compound_type_id = compound().type().id();
2848 compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2849 compound_type_id == ID_struct || compound_type_id == ID_union);
2850 set_component_name(component_name);
2851 }
2852
2854 : unary_exprt(ID_member, std::move(op), c.type())
2855 {
2856 const auto &compound_type_id = compound().type().id();
2858 compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2859 compound_type_id == ID_struct || compound_type_id == ID_union);
2861 }
2862
2864 {
2865 return get(ID_component_name);
2866 }
2867
2868 void set_component_name(const irep_idt &component_name)
2869 {
2870 set(ID_component_name, component_name);
2871 }
2872
2873 std::size_t get_component_number() const
2874 {
2875 return get_size_t(ID_component_number);
2876 }
2877
2878 // will go away, use compound()
2879 const exprt &struct_op() const
2880 {
2881 return op0();
2882 }
2883
2884 // will go away, use compound()
2886 {
2887 return op0();
2888 }
2889
2890 const exprt &compound() const
2891 {
2892 return op0();
2893 }
2894
2896 {
2897 return op0();
2898 }
2899
2900 static void check(
2901 const exprt &expr,
2903 {
2904 DATA_CHECK(
2905 vm,
2906 expr.operands().size() == 1,
2907 "member expression must have one operand");
2908 }
2909
2910 static void validate(
2911 const exprt &expr,
2912 const namespacet &ns,
2914};
2915
2916template <>
2917inline bool can_cast_expr<member_exprt>(const exprt &base)
2918{
2919 return base.id() == ID_member;
2920}
2921
2922inline void validate_expr(const member_exprt &value)
2923{
2924 validate_operands(value, 1, "Extract member must have one operand");
2925}
2926
2933inline const member_exprt &to_member_expr(const exprt &expr)
2934{
2935 PRECONDITION(expr.id()==ID_member);
2936 member_exprt::check(expr);
2937 return static_cast<const member_exprt &>(expr);
2938}
2939
2942{
2943 PRECONDITION(expr.id()==ID_member);
2944 member_exprt::check(expr);
2945 return static_cast<member_exprt &>(expr);
2946}
2947
2948
2951{
2952public:
2953 explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
2954 {
2955 }
2956};
2957
2958template <>
2959inline bool can_cast_expr<type_exprt>(const exprt &base)
2960{
2961 return base.id() == ID_type;
2962}
2963
2970inline const type_exprt &to_type_expr(const exprt &expr)
2971{
2973 type_exprt::check(expr);
2974 return static_cast<const type_exprt &>(expr);
2975}
2976
2979{
2981 type_exprt::check(expr);
2982 return static_cast<type_exprt &>(expr);
2983}
2984
2987{
2988public:
2989 constant_exprt(const irep_idt &_value, typet _type)
2990 : nullary_exprt(ID_constant, std::move(_type))
2991 {
2992 set_value(_value);
2993 }
2994
2995 const irep_idt &get_value() const
2996 {
2997 return get(ID_value);
2998 }
2999
3000 void set_value(const irep_idt &value)
3001 {
3002 set(ID_value, value);
3003 }
3004
3005 bool value_is_zero_string() const;
3006
3007 static void check(
3008 const exprt &expr,
3010
3011 static void validate(
3012 const exprt &expr,
3013 const namespacet &,
3015 {
3016 check(expr, vm);
3017 }
3018};
3019
3020template <>
3021inline bool can_cast_expr<constant_exprt>(const exprt &base)
3022{
3023 return base.is_constant();
3024}
3025
3026inline void validate_expr(const constant_exprt &value)
3027{
3028 validate_operands(value, 0, "Constants must not have operands");
3029}
3030
3037inline const constant_exprt &to_constant_expr(const exprt &expr)
3038{
3039 PRECONDITION(expr.is_constant());
3041 return static_cast<const constant_exprt &>(expr);
3042}
3043
3046{
3047 PRECONDITION(expr.is_constant());
3049 return static_cast<constant_exprt &>(expr);
3050}
3051
3052
3055{
3056public:
3058 {
3059 }
3060};
3061
3064{
3065public:
3067 {
3068 }
3069};
3070
3073{
3074public:
3076 : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
3077 {
3078 }
3079};
3080
3081template <>
3082inline bool can_cast_expr<nil_exprt>(const exprt &base)
3083{
3084 return base.id() == ID_nil;
3085}
3086
3089{
3090public:
3091 explicit infinity_exprt(typet _type)
3092 : nullary_exprt(ID_infinity, std::move(_type))
3093 {
3094 }
3095};
3096
3099{
3100public:
3101 using variablest = std::vector<symbol_exprt>;
3102
3105 irep_idt _id,
3106 const variablest &_variables,
3107 exprt _where,
3108 typet _type)
3109 : binary_exprt(
3111 ID_tuple,
3112 (const operandst &)_variables,
3113 typet(ID_tuple)),
3114 _id,
3115 std::move(_where),
3116 std::move(_type))
3117 {
3118 }
3119
3121 {
3123 }
3124
3125 const variablest &variables() const
3126 {
3128 }
3129
3131 {
3132 return op1();
3133 }
3134
3135 const exprt &where() const
3136 {
3137 return op1();
3138 }
3139
3142 exprt instantiate(const exprt::operandst &) const;
3143
3146 exprt instantiate(const variablest &) const;
3147};
3148
3149template <>
3150inline bool can_cast_expr<binding_exprt>(const exprt &base)
3151{
3152 return base.id() == ID_forall || base.id() == ID_exists ||
3153 base.id() == ID_lambda || base.id() == ID_array_comprehension;
3154}
3155
3156inline void validate_expr(const binding_exprt &binding_expr)
3157{
3159 binding_expr, 2, "Binding expressions must have two operands");
3160}
3161
3168inline const binding_exprt &to_binding_expr(const exprt &expr)
3169{
3171 expr.id() == ID_forall || expr.id() == ID_exists ||
3172 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3173 const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
3174 validate_expr(ret);
3175 return ret;
3176}
3177
3185{
3187 expr.id() == ID_forall || expr.id() == ID_exists ||
3188 expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3189 binding_exprt &ret = static_cast<binding_exprt &>(expr);
3190 validate_expr(ret);
3191 return ret;
3192}
3193
3196{
3197public:
3201 const exprt &where)
3202 : binary_exprt(
3204 ID_let_binding,
3205 std::move(variables),
3206 where,
3207 where.type()),
3208 ID_let,
3209 multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
3210 where.type())
3211 {
3212 PRECONDITION(this->variables().size() == this->values().size());
3213 }
3214
3217 : let_exprt(
3219 operandst{std::move(value)},
3220 where)
3221 {
3222 }
3223
3225 {
3226 return static_cast<binding_exprt &>(op0());
3227 }
3228
3229 const binding_exprt &binding() const
3230 {
3231 return static_cast<const binding_exprt &>(op0());
3232 }
3233
3236 {
3237 auto &variables = binding().variables();
3238 PRECONDITION(variables.size() == 1);
3239 return variables.front();
3240 }
3241
3243 const symbol_exprt &symbol() const
3244 {
3245 const auto &variables = binding().variables();
3246 PRECONDITION(variables.size() == 1);
3247 return variables.front();
3248 }
3249
3252 {
3253 auto &values = this->values();
3254 PRECONDITION(values.size() == 1);
3255 return values.front();
3256 }
3257
3259 const exprt &value() const
3260 {
3261 const auto &values = this->values();
3262 PRECONDITION(values.size() == 1);
3263 return values.front();
3264 }
3265
3267 {
3268 return static_cast<multi_ary_exprt &>(op1()).operands();
3269 }
3270
3271 const operandst &values() const
3272 {
3273 return static_cast<const multi_ary_exprt &>(op1()).operands();
3274 }
3275
3278 {
3279 return binding().variables();
3280 }
3281
3284 {
3285 return binding().variables();
3286 }
3287
3290 {
3291 return binding().where();
3292 }
3293
3295 const exprt &where() const
3296 {
3297 return binding().where();
3298 }
3299
3300 static void validate(const exprt &, validation_modet);
3301};
3302
3303template <>
3304inline bool can_cast_expr<let_exprt>(const exprt &base)
3305{
3306 return base.id() == ID_let;
3307}
3308
3309inline void validate_expr(const let_exprt &let_expr)
3310{
3311 validate_operands(let_expr, 2, "Let must have two operands");
3312}
3313
3320inline const let_exprt &to_let_expr(const exprt &expr)
3321{
3322 PRECONDITION(expr.id()==ID_let);
3323 const let_exprt &ret = static_cast<const let_exprt &>(expr);
3324 validate_expr(ret);
3325 return ret;
3326}
3327
3330{
3331 PRECONDITION(expr.id()==ID_let);
3332 let_exprt &ret = static_cast<let_exprt &>(expr);
3333 validate_expr(ret);
3334 return ret;
3335}
3336
3337
3342{
3343public:
3344 cond_exprt(operandst _operands, typet _type)
3345 : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3346 {
3347 }
3348
3352 void add_case(const exprt &condition, const exprt &value)
3353 {
3354 PRECONDITION(condition.is_boolean());
3355 operands().reserve(operands().size() + 2);
3356 operands().push_back(condition);
3357 operands().push_back(value);
3358 }
3359};
3360
3361template <>
3362inline bool can_cast_expr<cond_exprt>(const exprt &base)
3363{
3364 return base.id() == ID_cond;
3365}
3366
3367inline void validate_expr(const cond_exprt &value)
3368{
3370 value.operands().size() % 2 == 0, "cond must have even number of operands");
3371}
3372
3379inline const cond_exprt &to_cond_expr(const exprt &expr)
3380{
3381 PRECONDITION(expr.id() == ID_cond);
3382 const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3383 validate_expr(ret);
3384 return ret;
3385}
3386
3389{
3390 PRECONDITION(expr.id() == ID_cond);
3391 cond_exprt &ret = static_cast<cond_exprt &>(expr);
3392 validate_expr(ret);
3393 return ret;
3394}
3395
3405{
3406public:
3409 exprt body,
3410 array_typet _type)
3411 : binding_exprt(
3412 ID_array_comprehension,
3413 {std::move(arg)},
3414 std::move(body),
3415 std::move(_type))
3416 {
3417 }
3418
3419 const array_typet &type() const
3420 {
3421 return static_cast<const array_typet &>(binary_exprt::type());
3422 }
3423
3425 {
3426 return static_cast<array_typet &>(binary_exprt::type());
3427 }
3428
3429 const symbol_exprt &arg() const
3430 {
3431 auto &variables = this->variables();
3432 PRECONDITION(variables.size() == 1);
3433 return variables[0];
3434 }
3435
3437 {
3438 auto &variables = this->variables();
3439 PRECONDITION(variables.size() == 1);
3440 return variables[0];
3441 }
3442
3443 const exprt &body() const
3444 {
3445 return where();
3446 }
3447
3449 {
3450 return where();
3451 }
3452};
3453
3454template <>
3456{
3457 return base.id() == ID_array_comprehension;
3458}
3459
3461{
3462 validate_operands(value, 2, "'Array comprehension' must have two operands");
3463}
3464
3471inline const array_comprehension_exprt &
3473{
3474 PRECONDITION(expr.id() == ID_array_comprehension);
3475 const array_comprehension_exprt &ret =
3476 static_cast<const array_comprehension_exprt &>(expr);
3477 validate_expr(ret);
3478 return ret;
3479}
3480
3483{
3484 PRECONDITION(expr.id() == ID_array_comprehension);
3486 static_cast<array_comprehension_exprt &>(expr);
3487 validate_expr(ret);
3488 return ret;
3489}
3490
3491inline void validate_expr(const class class_method_descriptor_exprt &value);
3492
3495{
3496public:
3512 typet _type,
3516 : nullary_exprt(ID_virtual_function, std::move(_type))
3517 {
3519 set(ID_component_name, std::move(mangled_method_name));
3520 set(ID_C_class, std::move(class_id));
3521 set(ID_C_base_name, std::move(base_method_name));
3522 set(ID_identifier, std::move(id));
3523 validate_expr(*this);
3524 }
3525
3533 {
3534 return get(ID_component_name);
3535 }
3536
3540 const irep_idt &class_id() const
3541 {
3542 return get(ID_C_class);
3543 }
3544
3548 {
3549 return get(ID_C_base_name);
3550 }
3551
3556 {
3557 return get(ID_identifier);
3558 }
3559};
3560
3561inline void validate_expr(const class class_method_descriptor_exprt &value)
3562{
3563 validate_operands(value, 0, "class method descriptor must not have operands");
3565 !value.mangled_method_name().empty(),
3566 "class method descriptor must have a mangled method name.");
3568 !value.class_id().empty(), "class method descriptor must have a class id.");
3570 !value.base_method_name().empty(),
3571 "class method descriptor must have a base method name.");
3573 value.get_identifier() == id2string(value.class_id()) + "." +
3575 "class method descriptor must have an identifier in the expected format.");
3576}
3577
3584inline const class_method_descriptor_exprt &
3586{
3587 PRECONDITION(expr.id() == ID_virtual_function);
3589 return static_cast<const class_method_descriptor_exprt &>(expr);
3590}
3591
3592template <>
3594{
3595 return base.id() == ID_virtual_function;
3596}
3597
3604{
3605public:
3607 : binary_exprt(
3608 std::move(symbol),
3609 ID_named_term,
3610 value, // not moved, for type
3611 value.type())
3612 {
3613 PRECONDITION(symbol.type() == type());
3614 }
3615
3616 const symbol_exprt &symbol() const
3617 {
3618 return static_cast<const symbol_exprt &>(op0());
3619 }
3620
3622 {
3623 return static_cast<symbol_exprt &>(op0());
3624 }
3625
3626 const exprt &value() const
3627 {
3628 return op1();
3629 }
3630
3632 {
3633 return op1();
3634 }
3635};
3636
3637template <>
3639{
3640 return base.id() == ID_named_term;
3641}
3642
3643inline void validate_expr(const named_term_exprt &value)
3644{
3645 validate_operands(value, 2, "'named term' must have two operands");
3646}
3647
3655{
3656 PRECONDITION(expr.id() == ID_named_term);
3657 const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
3658 validate_expr(ret);
3659 return ret;
3660}
3661
3664{
3665 PRECONDITION(expr.id() == ID_named_term);
3666 named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
3667 validate_expr(ret);
3668 return ret;
3669}
3670
3671#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:2120
and_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2127
and_exprt(exprt op0, exprt op1)
Definition std_expr.h:2122
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2135
and_exprt(exprt::operandst _operands)
Definition std_expr.h:2143
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3405
const array_typet & type() const
Definition std_expr.h:3419
const symbol_exprt & arg() const
Definition std_expr.h:3429
const exprt & body() const
Definition std_expr.h:3443
array_typet & type()
Definition std_expr.h:3424
symbol_exprt & arg()
Definition std_expr.h:3436
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition std_expr.h:3407
Array constructor from list of elements.
Definition std_expr.h:1616
array_exprt && with_source_location(const exprt &other) &&
Definition std_expr.h:1640
const array_typet & type() const
Definition std_expr.h:1623
array_exprt & with_source_location(const exprt &other) &
Definition std_expr.h:1633
array_exprt(operandst _operands, array_typet _type)
Definition std_expr.h:1618
array_typet & type()
Definition std_expr.h:1628
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition std_expr.h:1676
void add(exprt index, exprt value)
add an index/value pair
Definition std_expr.h:1694
const array_typet & type() const
Definition std_expr.h:1683
array_list_exprt(operandst _operands, array_typet _type)
Definition std_expr.h:1678
array_typet & type()
Definition std_expr.h:1688
Array constructor from single element.
Definition std_expr.h:1553
array_typet & type()
Definition std_expr.h:1565
array_of_exprt(exprt _what, array_typet _type)
Definition std_expr.h:1555
const exprt & what() const
Definition std_expr.h:1575
const array_typet & type() const
Definition std_expr.h:1560
exprt & what()
Definition std_expr.h:1570
Arrays with given size.
Definition std_types.h:807
A base class for binary expressions.
Definition std_expr.h:638
exprt & lhs()
Definition std_expr.h:668
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:640
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:660
const exprt & op2() const =delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:650
exprt & rhs()
Definition std_expr.h:678
exprt & op0()
Definition expr.h:133
const exprt & lhs() const
Definition std_expr.h:673
exprt & op1()
Definition expr.h:136
exprt & op3()=delete
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition std_expr.h:645
const exprt & rhs() const
Definition std_expr.h:683
exprt & op2()=delete
const exprt & op3() const =delete
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:738
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition std_expr.h:733
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:745
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:764
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:769
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:776
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:3099
const variablest & variables() const
Definition std_expr.h:3125
const exprt & where() const
Definition std_expr.h:3135
exprt & where()
Definition std_expr.h:3130
variablest & variables()
Definition std_expr.h:3120
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition std_expr.h:3104
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:177
std::vector< symbol_exprt > variablest
Definition std_expr.h:3101
The Boolean type.
Definition std_types.h:36
An expression describing a method on a class.
Definition std_expr.h:3495
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:3547
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition std_expr.h:3532
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:3555
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition std_expr.h:3511
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:3540
Complex constructor from a pair of numbers.
Definition std_expr.h:1911
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition std_expr.h:1913
exprt real()
Definition std_expr.h:1922
exprt imag()
Definition std_expr.h:1932
const exprt & real() const
Definition std_expr.h:1927
const exprt & imag() const
Definition std_expr.h:1937
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2022
complex_imag_exprt(const exprt &op)
Definition std_expr.h:2024
Real part of the expression describing a complex number.
Definition std_expr.h:1979
complex_real_exprt(const exprt &op)
Definition std_expr.h:1981
Complex numbers made of pair of given subtype.
Definition std_types.h:1121
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition std_expr.h:3342
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition std_expr.h:3352
cond_exprt(operandst _operands, typet _type)
Definition std_expr.h:3344
A constant literal expression.
Definition std_expr.h:2987
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:3011
const irep_idt & get_value() const
Definition std_expr.h:2995
bool value_is_zero_string() const
Definition std_expr.cpp:18
constant_exprt(const irep_idt &_value, typet _type)
Definition std_expr.h:2989
void set_value(const irep_idt &value)
Definition std_expr.h:3000
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.cpp:24
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition std_expr.h:215
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:219
bool is_static_lifetime() const
Definition std_expr.h:224
bool is_thread_local() const
Definition std_expr.h:239
Division.
Definition std_expr.h:1152
div_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1154
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1160
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1166
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1178
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1172
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1829
empty_union_exprt(typet _type)
Definition std_expr.h:1831
Equality.
Definition std_expr.h:1361
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:1369
equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1363
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:1376
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1291
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1311
euclidean_mod_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1293
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1317
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1299
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1305
Base class for all expressions.
Definition expr.h:344
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
static void check(const exprt &, const validation_modet)
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...
Definition expr.h:254
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
exprt & op2()
Definition expr.h:139
source_locationt & add_source_location()
Definition expr.h:236
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
The Boolean constant false.
Definition std_expr.h:3064
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:2370
const exprt & false_case() const
Definition std_expr.h:2412
exprt & cond()
Definition std_expr.h:2387
const exprt & cond() const
Definition std_expr.h:2392
if_exprt(exprt cond, const exprt &t, exprt f)
Definition std_expr.h:2372
const exprt & true_case() const
Definition std_expr.h:2402
exprt & false_case()
Definition std_expr.h:2407
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition std_expr.h:2377
exprt & true_case()
Definition std_expr.h:2397
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2417
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2424
Boolean implication.
Definition std_expr.h:2183
implies_exprt(exprt op0, exprt op1)
Definition std_expr.h:2185
const exprt & index() const
Definition std_expr.h:2558
index_designatort(exprt _index)
Definition std_expr.h:2553
exprt & index()
Definition std_expr.h:2563
Array index operator.
Definition std_expr.h:1465
exprt & index()
Definition std_expr.h:1505
index_exprt(exprt _array, exprt _index, typet _type)
Definition std_expr.h:1483
index_exprt(const exprt &_array, exprt _index)
Definition std_expr.h:1471
exprt & array()
Definition std_expr.h:1495
const exprt & index() const
Definition std_expr.h:1510
const exprt & array() const
Definition std_expr.h:1500
An expression denoting infinity.
Definition std_expr.h:3089
infinity_exprt(typet _type)
Definition std_expr.h:3091
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:3196
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3277
const binding_exprt & binding() const
Definition std_expr.h:3229
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition std_expr.h:3283
operandst & values()
Definition std_expr.h:3266
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition std_expr.h:3216
const exprt & where() const
convenience accessor for binding().where()
Definition std_expr.h:3295
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:151
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition std_expr.h:3243
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition std_expr.h:3198
exprt & value()
convenience accessor for the value of a single binding
Definition std_expr.h:3251
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3289
binding_exprt & binding()
Definition std_expr.h:3224
const operandst & values() const
Definition std_expr.h:3271
const exprt & value() const
convenience accessor for the value of a single binding
Definition std_expr.h:3259
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition std_expr.h:3235
irep_idt get_component_name() const
Definition std_expr.h:2612
member_designatort(const irep_idt &_component_name)
Definition std_expr.h:2606
Extract member of struct or union.
Definition std_expr.h:2841
const exprt & compound() const
Definition std_expr.h:2890
exprt & struct_op()
Definition std_expr.h:2885
const exprt & struct_op() const
Definition std_expr.h:2879
irep_idt get_component_name() const
Definition std_expr.h:2863
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:2868
exprt & compound()
Definition std_expr.h:2895
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:116
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2900
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition std_expr.h:2843
std::size_t get_component_number() const
Definition std_expr.h:2873
member_exprt(exprt op, const struct_typet::componentt &c)
Definition std_expr.h:2853
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:1223
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1231
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1237
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1243
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1249
mod_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1225
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
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:3604
named_term_exprt(symbol_exprt symbol, exprt value)
Definition std_expr.h:3606
symbol_exprt & symbol()
Definition std_expr.h:3621
const exprt & value() const
Definition std_expr.h:3626
const symbol_exprt & symbol() const
Definition std_expr.h:3616
exprt & value()
Definition std_expr.h:3631
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
The NIL expression.
Definition std_expr.h:3073
Expression to hold a nondeterministic choice.
Definition std_expr.h:292
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:315
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:296
const irep_idt & get_identifier() const
Definition std_expr.h:320
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition std_expr.h:305
Boolean negation.
Definition std_expr.h:2327
not_exprt(exprt _op)
Definition std_expr.h:2329
Disequality.
Definition std_expr.h:1420
notequal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1422
An expression without operands.
Definition std_expr.h:22
exprt & op0()=delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:29
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:39
const exprt & op1() const =delete
nullary_exprt(const irep_idt &_id, typet _type)
Definition std_expr.h:24
const exprt & op0() const =delete
void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete
exprt & op3()=delete
void copy_to_operands(const exprt &expr)=delete
operandst & operands()=delete
remove all operand methods
void copy_to_operands(const exprt &, const exprt &)=delete
const operandst & operands() const =delete
exprt & op1()=delete
exprt & op2()=delete
const exprt & op3() const =delete
const exprt & op2() const =delete
Boolean OR.
Definition std_expr.h:2228
or_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2235
or_exprt(exprt::operandst _operands)
Definition std_expr.h:2251
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2243
or_exprt(exprt op0, exprt op1)
Definition std_expr.h:2230
The plus expression Associativity is not specified.
Definition std_expr.h:1002
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition std_expr.h:1009
plus_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1004
plus_exprt(operandst _operands, typet _type)
Definition std_expr.h:1018
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition std_expr.h:574
predicate_exprt(const irep_idt &_id)
Definition std_expr.h:576
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:596
sign_exprt(exprt _op)
Definition std_expr.h:598
Struct constructor from list of elements.
Definition std_expr.h:1872
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:97
struct_exprt(operandst _operands, typet _type)
Definition std_expr.h:1874
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
The Boolean constant true.
Definition std_expr.h:3055
An expression denoting a type.
Definition std_expr.h:2951
type_exprt(typet type)
Definition std_expr.h:2953
Semantic type conversion.
Definition std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2076
typecast_exprt(exprt op, typet _type)
Definition std_expr.h:2070
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition std_expr.h:363
const exprt & op3() const =delete
exprt & op2()=delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:373
const exprt & op1() const =delete
exprt & op3()=delete
const exprt & op() const
Definition std_expr.h:391
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition std_expr.h:368
const exprt & op2() const =delete
exprt & op()
Definition std_expr.h:396
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:383
exprt & op1()=delete
The unary minus expression.
Definition std_expr.h:484
unary_minus_exprt(exprt _op)
Definition std_expr.h:491
unary_minus_exprt(exprt _op, typet _type)
Definition std_expr.h:486
The unary plus expression.
Definition std_expr.h:531
unary_plus_exprt(exprt op)
Definition std_expr.h:533
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:585
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition std_expr.h:587
Union constructor from single element.
Definition std_expr.h:1765
std::size_t get_component_number() const
Definition std_expr.h:1783
void set_component_number(std::size_t component_number)
Definition std_expr.h:1788
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:1778
irep_idt get_component_name() const
Definition std_expr.h:1773
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition std_expr.h:1767
Operator to update elements in structs and arrays.
Definition std_expr.h:2655
exprt & old()
Definition std_expr.h:2667
exprt::operandst & designator()
Definition std_expr.h:2681
exprt & new_value()
Definition std_expr.h:2691
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2708
const exprt & new_value() const
Definition std_expr.h:2696
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition std_expr.h:2657
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2701
const exprt & old() const
Definition std_expr.h:2672
const exprt::operandst & designator() const
Definition std_expr.h:2686
Vector constructor from list of elements.
Definition std_expr.h:1729
vector_exprt(operandst _operands, vector_typet _type)
Definition std_expr.h:1731
The vector type.
Definition std_types.h:1052
Operator to update elements in structs and arrays.
Definition std_expr.h:2471
const exprt & old() const
Definition std_expr.h:2486
const exprt & where() const
Definition std_expr.h:2496
exprt & new_value()
Definition std_expr.h:2501
exprt & where()
Definition std_expr.h:2491
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition std_expr.h:2473
const exprt & new_value() const
Definition std_expr.h:2506
exprt & old()
Definition std_expr.h:2481
Boolean XOR.
Definition std_expr.h:2291
xor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2293
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
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:1386
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition std_expr.h:1429
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition std_expr.h:1944
bool can_cast_expr< not_exprt >(const exprt &base)
Definition std_expr.h:2336
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1895
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition std_expr.h:1711
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition std_expr.h:2086
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition std_expr.h:2970
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1598
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition std_expr.h:1884
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:2300
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1533
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition std_expr.h:1116
bool can_cast_expr< if_exprt >(const exprt &base)
Definition std_expr.h:2434
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:3585
bool can_cast_expr< named_term_exprt >(const exprt &base)
Definition std_expr.h:3638
bool can_cast_expr< binding_exprt >(const exprt &base)
Definition std_expr.h:3150
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1272
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1132
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition std_expr.h:2167
bool can_cast_expr< member_designatort >(const exprt &base)
Definition std_expr.h:2619
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3472
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:3654
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition std_expr.h:3455
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition std_expr.h:2311
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2275
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1660
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition std_expr.h:2031
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:3379
bool can_cast_expr< type_exprt >(const exprt &base)
Definition std_expr.h:2959
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:54
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition std_expr.h:3593
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2102
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:1201
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:2513
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition std_expr.h:1749
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:66
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:3304
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:1445
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition std_expr.h:1025
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition std_expr.h:1582
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3320
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:3021
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2450
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2933
bool can_cast_expr< index_exprt >(const exprt &base)
Definition std_expr.h:1517
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:1855
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:2917
bool can_cast_expr< empty_union_exprt >(const exprt &base)
Definition std_expr.h:1838
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:2048
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition std_expr.h:3168
bool can_cast_expr< or_exprt >(const exprt &base)
Definition std_expr.h:2264
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition std_expr.h:1256
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2586
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1811
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition std_expr.h:3362
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:2005
bool can_cast_expr< update_exprt >(const exprt &base)
Definition std_expr.h:2718
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:1324
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition std_expr.h:1738
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3037
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition std_expr.h:1701
bool can_cast_expr< index_designatort >(const exprt &base)
Definition std_expr.h:2570
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2352
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:2533
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1960
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:2156
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:2208
bool can_cast_expr< array_exprt >(const exprt &base)
Definition std_expr.h:1649
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:1185
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2735
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition std_expr.h:3082
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:1402
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:2192
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:1795
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition std_expr.h:2635
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition std_expr.h:1988
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition std_expr.h:621
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition std_expr.h:1340
Pre-defined types.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1146
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