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
30 operandst &operands() = delete;
31 const operandst &operands() const = delete;
32
33 const exprt &op0() const = delete;
34 exprt &op0() = delete;
35 const exprt &op1() const = delete;
36 exprt &op1() = delete;
37 const exprt &op2() const = delete;
38 exprt &op2() = delete;
39 const exprt &op3() const = delete;
40 exprt &op3() = delete;
41
42 void move_to_operands(exprt &) = delete;
43 void move_to_operands(exprt &, exprt &) = delete;
44 void move_to_operands(exprt &, exprt &, exprt &) = delete;
45
46 void copy_to_operands(const exprt &expr) = delete;
47 void copy_to_operands(const exprt &, const exprt &) = delete;
48 void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
49};
50
53{
54public:
55 // constructor
57 const irep_idt &_id,
58 exprt _op0,
59 exprt _op1,
60 exprt _op2,
61 typet _type)
63 _id,
64 std::move(_type),
65 {std::move(_op0), std::move(_op1), std::move(_op2)})
66 {
67 }
68
69 // make op0 to op2 public
70 using exprt::op0;
71 using exprt::op1;
72 using exprt::op2;
73
74 const exprt &op3() const = delete;
75 exprt &op3() = delete;
76};
77
80{
81public:
83 explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type))
84 {
85 }
86
89 symbol_exprt(const irep_idt &identifier, typet type)
90 : nullary_exprt(ID_symbol, std::move(type))
91 {
92 set_identifier(identifier);
93 }
94
99 static symbol_exprt typeless(const irep_idt &id)
100 {
101 return symbol_exprt(id, typet());
102 }
103
104 void set_identifier(const irep_idt &identifier)
105 {
106 set(ID_identifier, identifier);
107 }
108
110 {
111 return get(ID_identifier);
112 }
113};
114
115// NOLINTNEXTLINE(readability/namespace)
116namespace std
117{
118template <>
119// NOLINTNEXTLINE(readability/identifiers)
120struct hash<::symbol_exprt>
121{
122 size_t operator()(const ::symbol_exprt &sym)
123 {
124 return irep_id_hash()(sym.get_identifier());
125 }
126};
127} // namespace std
128
132{
133public:
137 : symbol_exprt(identifier, std::move(type))
138 {
139 }
140
142 {
143 return get_bool(ID_C_static_lifetime);
144 }
145
147 {
148 return set(ID_C_static_lifetime, true);
149 }
150
152 {
153 remove(ID_C_static_lifetime);
154 }
155
156 bool is_thread_local() const
157 {
158 return get_bool(ID_C_thread_local);
159 }
160
162 {
163 return set(ID_C_thread_local, true);
164 }
165
167 {
168 remove(ID_C_thread_local);
169 }
170};
171
172template <>
173inline bool can_cast_expr<symbol_exprt>(const exprt &base)
174{
175 return base.id() == ID_symbol;
176}
177
178inline void validate_expr(const symbol_exprt &value)
179{
180 validate_operands(value, 0, "Symbols must not have operands");
181}
182
189inline const symbol_exprt &to_symbol_expr(const exprt &expr)
190{
191 PRECONDITION(expr.id()==ID_symbol);
192 const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
193 validate_expr(ret);
194 return ret;
195}
196
199{
200 PRECONDITION(expr.id()==ID_symbol);
201 symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
202 validate_expr(ret);
203 return ret;
204}
205
206
209{
210public:
214 : nullary_exprt(ID_nondet_symbol, std::move(type))
215 {
216 set_identifier(identifier);
217 }
218
223 irep_idt identifier,
224 typet type,
225 source_locationt location)
226 : nullary_exprt(ID_nondet_symbol, std::move(type))
227 {
228 set_identifier(std::move(identifier));
229 add_source_location() = std::move(location);
230 }
231
232 void set_identifier(const irep_idt &identifier)
233 {
234 set(ID_identifier, identifier);
235 }
236
238 {
239 return get(ID_identifier);
240 }
241};
242
243template <>
245{
246 return base.id() == ID_nondet_symbol;
247}
248
249inline void validate_expr(const nondet_symbol_exprt &value)
250{
251 validate_operands(value, 0, "Symbols must not have operands");
252}
253
261{
262 PRECONDITION(expr.id()==ID_nondet_symbol);
263 const nondet_symbol_exprt &ret =
264 static_cast<const nondet_symbol_exprt &>(expr);
265 validate_expr(ret);
266 return ret;
267}
268
271{
272 PRECONDITION(expr.id()==ID_symbol);
273 nondet_symbol_exprt &ret = static_cast<nondet_symbol_exprt &>(expr);
274 validate_expr(ret);
275 return ret;
276}
277
278
281{
282public:
283 unary_exprt(const irep_idt &_id, const exprt &_op)
284 : expr_protectedt(_id, _op.type(), {_op})
285 {
286 }
287
288 unary_exprt(const irep_idt &_id, exprt _op, typet _type)
289 : expr_protectedt(_id, std::move(_type), {std::move(_op)})
290 {
291 }
292
293 const exprt &op() const
294 {
295 return op0();
296 }
297
299 {
300 return op0();
301 }
302
303 const exprt &op1() const = delete;
304 exprt &op1() = delete;
305 const exprt &op2() const = delete;
306 exprt &op2() = delete;
307 const exprt &op3() const = delete;
308 exprt &op3() = delete;
309};
310
311template <>
312inline bool can_cast_expr<unary_exprt>(const exprt &base)
313{
314 return base.operands().size() == 1;
315}
316
317inline void validate_expr(const unary_exprt &value)
318{
319 validate_operands(value, 1, "Unary expressions must have one operand");
320}
321
328inline const unary_exprt &to_unary_expr(const exprt &expr)
329{
330 const unary_exprt &ret = static_cast<const unary_exprt &>(expr);
331 validate_expr(ret);
332 return ret;
333}
334
337{
338 unary_exprt &ret = static_cast<unary_exprt &>(expr);
339 validate_expr(ret);
340 return ret;
341}
342
343
346{
347public:
348 explicit abs_exprt(exprt _op) : unary_exprt(ID_abs, std::move(_op))
349 {
350 }
351};
352
353template <>
354inline bool can_cast_expr<abs_exprt>(const exprt &base)
355{
356 return base.id() == ID_abs;
357}
358
359inline void validate_expr(const abs_exprt &value)
360{
361 validate_operands(value, 1, "Absolute value must have one operand");
362}
363
370inline const abs_exprt &to_abs_expr(const exprt &expr)
371{
372 PRECONDITION(expr.id()==ID_abs);
373 const abs_exprt &ret = static_cast<const abs_exprt &>(expr);
374 validate_expr(ret);
375 return ret;
376}
377
380{
381 PRECONDITION(expr.id()==ID_abs);
382 abs_exprt &ret = static_cast<abs_exprt &>(expr);
383 validate_expr(ret);
384 return ret;
385}
386
387
390{
391public:
393 : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
394 {
395 }
396
398 : unary_exprt(ID_unary_minus, std::move(_op))
399 {
400 }
401};
402
403template <>
405{
406 return base.id() == ID_unary_minus;
407}
408
409inline void validate_expr(const unary_minus_exprt &value)
410{
411 validate_operands(value, 1, "Unary minus must have one operand");
412}
413
421{
422 PRECONDITION(expr.id()==ID_unary_minus);
423 const unary_minus_exprt &ret = static_cast<const unary_minus_exprt &>(expr);
424 validate_expr(ret);
425 return ret;
426}
427
430{
431 PRECONDITION(expr.id()==ID_unary_minus);
432 unary_minus_exprt &ret = static_cast<unary_minus_exprt &>(expr);
433 validate_expr(ret);
434 return ret;
435}
436
439{
440public:
442 : unary_exprt(ID_unary_plus, std::move(op))
443 {
444 }
445};
446
447template <>
449{
450 return base.id() == ID_unary_plus;
451}
452
453inline void validate_expr(const unary_plus_exprt &value)
454{
455 validate_operands(value, 1, "unary plus must have one operand");
456}
457
464inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
465{
466 PRECONDITION(expr.id() == ID_unary_plus);
467 const unary_plus_exprt &ret = static_cast<const unary_plus_exprt &>(expr);
468 validate_expr(ret);
469 return ret;
470}
471
474{
475 PRECONDITION(expr.id() == ID_unary_plus);
476 unary_plus_exprt &ret = static_cast<unary_plus_exprt &>(expr);
477 validate_expr(ret);
478 return ret;
479}
480
484{
485public:
486 explicit predicate_exprt(const irep_idt &_id)
488 {
489 }
490};
491
495{
496public:
498 : unary_exprt(_id, std::move(_op), bool_typet())
499 {
500 }
501};
502
506{
507public:
508 explicit sign_exprt(exprt _op)
509 : unary_predicate_exprt(ID_sign, std::move(_op))
510 {
511 }
512};
513
514template <>
515inline bool can_cast_expr<sign_exprt>(const exprt &base)
516{
517 return base.id() == ID_sign;
518}
519
520inline void validate_expr(const sign_exprt &expr)
521{
522 validate_operands(expr, 1, "sign expression must have one operand");
523}
524
531inline const sign_exprt &to_sign_expr(const exprt &expr)
532{
533 PRECONDITION(expr.id() == ID_sign);
534 const sign_exprt &ret = static_cast<const sign_exprt &>(expr);
535 validate_expr(ret);
536 return ret;
537}
538
541{
542 PRECONDITION(expr.id() == ID_sign);
543 sign_exprt &ret = static_cast<sign_exprt &>(expr);
544 validate_expr(ret);
545 return ret;
546}
547
550{
551public:
552 binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
553 : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
554 {
555 }
556
557 binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
558 : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
559 {
560 }
561
562 static void check(
563 const exprt &expr,
565 {
567 vm,
568 expr.operands().size() == 2,
569 "binary expression must have two operands");
570 }
571
572 static void validate(
573 const exprt &expr,
574 const namespacet &,
576 {
577 check(expr, vm);
578 }
579
581 {
582 return exprt::op0();
583 }
584
585 const exprt &lhs() const
586 {
587 return exprt::op0();
588 }
589
591 {
592 return exprt::op1();
593 }
594
595 const exprt &rhs() const
596 {
597 return exprt::op1();
598 }
599
600 // make op0 and op1 public
601 using exprt::op0;
602 using exprt::op1;
603
604 const exprt &op2() const = delete;
605 exprt &op2() = delete;
606 const exprt &op3() const = delete;
607 exprt &op3() = delete;
608};
609
610template <>
611inline bool can_cast_expr<binary_exprt>(const exprt &base)
612{
613 return base.operands().size() == 2;
614}
615
616inline void validate_expr(const binary_exprt &value)
617{
618 binary_exprt::check(value);
619}
620
627inline const binary_exprt &to_binary_expr(const exprt &expr)
628{
630 return static_cast<const binary_exprt &>(expr);
631}
632
635{
637 return static_cast<binary_exprt &>(expr);
638}
639
643{
644public:
646 : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
647 {
648 }
649
650 static void check(
651 const exprt &expr,
653 {
654 binary_exprt::check(expr, vm);
655 }
656
657 static void validate(
658 const exprt &expr,
659 const namespacet &ns,
661 {
662 binary_exprt::validate(expr, ns, vm);
663
665 vm,
666 expr.type().id() == ID_bool,
667 "result of binary predicate expression should be of type bool");
668 }
669};
670
674{
675public:
677 : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
678 {
679 }
680
681 static void check(
682 const exprt &expr,
684 {
686 }
687
688 static void validate(
689 const exprt &expr,
690 const namespacet &ns,
692 {
694
695 // we now can safely assume that 'expr' is a binary predicate
696 const auto &expr_binary = static_cast<const binary_predicate_exprt &>(expr);
697
698 // check that the types of the operands are the same
700 vm,
701 expr_binary.op0().type() == expr_binary.op1().type(),
702 "lhs and rhs of binary relation expression should have same type");
703 }
704};
705
706template <>
708{
709 return can_cast_expr<binary_exprt>(base);
710}
711
712inline void validate_expr(const binary_relation_exprt &value)
713{
715}
716
719{
720public:
722 : binary_relation_exprt{std::move(_lhs), ID_gt, std::move(_rhs)}
723 {
724 }
725};
726
727template <>
729{
730 return base.id() == ID_gt;
731}
732
733inline void validate_expr(const greater_than_exprt &value)
734{
736}
737
740{
741public:
743 : binary_relation_exprt{std::move(_lhs), ID_ge, std::move(_rhs)}
744 {
745 }
746};
747
748template <>
750{
751 return base.id() == ID_ge;
752}
753
755{
757}
758
761{
762public:
764 : binary_relation_exprt{std::move(_lhs), ID_lt, std::move(_rhs)}
765 {
766 }
767};
768
769template <>
770inline bool can_cast_expr<less_than_exprt>(const exprt &base)
771{
772 return base.id() == ID_lt;
773}
774
775inline void validate_expr(const less_than_exprt &value)
776{
778}
779
782{
783public:
785 : binary_relation_exprt{std::move(_lhs), ID_le, std::move(_rhs)}
786 {
787 }
788};
789
790template <>
792{
793 return base.id() == ID_le;
794}
795
797{
799}
800
808{
810 return static_cast<const binary_relation_exprt &>(expr);
811}
812
815{
817 return static_cast<binary_relation_exprt &>(expr);
818}
819
820
824{
825public:
826 multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
827 : expr_protectedt(_id, std::move(_type))
828 {
829 operands() = std::move(_operands);
830 }
831
832 multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
833 : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
834 {
835 }
836
837 multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
838 : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
839 {
840 }
841
842 // In contrast to exprt::opX, the methods
843 // below check the size.
845 {
846 PRECONDITION(operands().size() >= 1);
847 return operands().front();
848 }
849
851 {
852 PRECONDITION(operands().size() >= 2);
853 return operands()[1];
854 }
855
857 {
858 PRECONDITION(operands().size() >= 3);
859 return operands()[2];
860 }
861
863 {
864 PRECONDITION(operands().size() >= 4);
865 return operands()[3];
866 }
867
868 const exprt &op0() const
869 {
870 PRECONDITION(operands().size() >= 1);
871 return operands().front();
872 }
873
874 const exprt &op1() const
875 {
876 PRECONDITION(operands().size() >= 2);
877 return operands()[1];
878 }
879
880 const exprt &op2() const
881 {
882 PRECONDITION(operands().size() >= 3);
883 return operands()[2];
884 }
885
886 const exprt &op3() const
887 {
888 PRECONDITION(operands().size() >= 4);
889 return operands()[3];
890 }
891};
892
899inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
900{
901 return static_cast<const multi_ary_exprt &>(expr);
902}
903
906{
907 return static_cast<multi_ary_exprt &>(expr);
908}
909
910
914{
915public:
917 : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
918 {
919 }
920
921 plus_exprt(exprt _lhs, exprt _rhs, typet _type)
923 std::move(_lhs),
924 ID_plus,
925 std::move(_rhs),
926 std::move(_type))
927 {
928 }
929
930 plus_exprt(operandst _operands, typet _type)
931 : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
932 {
933 }
934};
935
936template <>
937inline bool can_cast_expr<plus_exprt>(const exprt &base)
938{
939 return base.id() == ID_plus;
940}
941
942inline void validate_expr(const plus_exprt &value)
943{
944 validate_operands(value, 2, "Plus must have two or more operands", true);
945}
946
953inline const plus_exprt &to_plus_expr(const exprt &expr)
954{
955 PRECONDITION(expr.id()==ID_plus);
956 const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
957 validate_expr(ret);
958 return ret;
959}
960
963{
964 PRECONDITION(expr.id()==ID_plus);
965 plus_exprt &ret = static_cast<plus_exprt &>(expr);
966 validate_expr(ret);
967 return ret;
968}
969
970
973{
974public:
976 : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
977 {
978 }
979};
980
981template <>
982inline bool can_cast_expr<minus_exprt>(const exprt &base)
983{
984 return base.id() == ID_minus;
985}
986
987inline void validate_expr(const minus_exprt &value)
988{
989 validate_operands(value, 2, "Minus must have two or more operands", true);
990}
991
998inline const minus_exprt &to_minus_expr(const exprt &expr)
999{
1000 PRECONDITION(expr.id()==ID_minus);
1001 const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
1002 validate_expr(ret);
1003 return ret;
1004}
1005
1008{
1009 PRECONDITION(expr.id()==ID_minus);
1010 minus_exprt &ret = static_cast<minus_exprt &>(expr);
1011 validate_expr(ret);
1012 return ret;
1013}
1014
1015
1019{
1020public:
1022 : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
1023 {
1024 }
1025};
1026
1027template <>
1028inline bool can_cast_expr<mult_exprt>(const exprt &base)
1029{
1030 return base.id() == ID_mult;
1031}
1032
1033inline void validate_expr(const mult_exprt &value)
1034{
1035 validate_operands(value, 2, "Multiply must have two or more operands", true);
1036}
1037
1044inline const mult_exprt &to_mult_expr(const exprt &expr)
1045{
1046 PRECONDITION(expr.id()==ID_mult);
1047 const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1048 validate_expr(ret);
1049 return ret;
1050}
1051
1054{
1055 PRECONDITION(expr.id()==ID_mult);
1056 mult_exprt &ret = static_cast<mult_exprt &>(expr);
1057 validate_expr(ret);
1058 return ret;
1059}
1060
1061
1064{
1065public:
1067 : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1068 {
1069 }
1070
1073 {
1074 return op0();
1075 }
1076
1078 const exprt &dividend() const
1079 {
1080 return op0();
1081 }
1082
1085 {
1086 return op1();
1087 }
1088
1090 const exprt &divisor() const
1091 {
1092 return op1();
1093 }
1094};
1095
1096template <>
1097inline bool can_cast_expr<div_exprt>(const exprt &base)
1098{
1099 return base.id() == ID_div;
1100}
1101
1102inline void validate_expr(const div_exprt &value)
1103{
1104 validate_operands(value, 2, "Divide must have two operands");
1105}
1106
1113inline const div_exprt &to_div_expr(const exprt &expr)
1114{
1115 PRECONDITION(expr.id()==ID_div);
1116 const div_exprt &ret = static_cast<const div_exprt &>(expr);
1117 validate_expr(ret);
1118 return ret;
1119}
1120
1123{
1124 PRECONDITION(expr.id()==ID_div);
1125 div_exprt &ret = static_cast<div_exprt &>(expr);
1126 validate_expr(ret);
1127 return ret;
1128}
1129
1135{
1136public:
1138 : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1139 {
1140 }
1141};
1142
1143template <>
1144inline bool can_cast_expr<mod_exprt>(const exprt &base)
1145{
1146 return base.id() == ID_mod;
1147}
1148
1149inline void validate_expr(const mod_exprt &value)
1150{
1151 validate_operands(value, 2, "Modulo must have two operands");
1152}
1153
1160inline const mod_exprt &to_mod_expr(const exprt &expr)
1161{
1162 PRECONDITION(expr.id()==ID_mod);
1163 const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1164 validate_expr(ret);
1165 return ret;
1166}
1167
1170{
1171 PRECONDITION(expr.id()==ID_mod);
1172 mod_exprt &ret = static_cast<mod_exprt &>(expr);
1173 validate_expr(ret);
1174 return ret;
1175}
1176
1179{
1180public:
1182 : binary_exprt(std::move(_lhs), ID_euclidean_mod, std::move(_rhs))
1183 {
1184 }
1185};
1186
1187template <>
1189{
1190 return base.id() == ID_euclidean_mod;
1191}
1192
1193inline void validate_expr(const euclidean_mod_exprt &value)
1194{
1195 validate_operands(value, 2, "Modulo must have two operands");
1196}
1197
1205{
1206 PRECONDITION(expr.id() == ID_euclidean_mod);
1207 const euclidean_mod_exprt &ret =
1208 static_cast<const euclidean_mod_exprt &>(expr);
1209 validate_expr(ret);
1210 return ret;
1211}
1212
1215{
1216 PRECONDITION(expr.id() == ID_euclidean_mod);
1217 euclidean_mod_exprt &ret = static_cast<euclidean_mod_exprt &>(expr);
1218 validate_expr(ret);
1219 return ret;
1220}
1221
1222
1225{
1226public:
1228 : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1229 {
1230 }
1231
1232 static void check(
1233 const exprt &expr,
1235 {
1237 }
1238
1239 static void validate(
1240 const exprt &expr,
1241 const namespacet &ns,
1243 {
1244 binary_relation_exprt::validate(expr, ns, vm);
1245 }
1246};
1247
1248template <>
1249inline bool can_cast_expr<equal_exprt>(const exprt &base)
1250{
1251 return base.id() == ID_equal;
1252}
1253
1254inline void validate_expr(const equal_exprt &value)
1255{
1256 equal_exprt::check(value);
1257}
1258
1265inline const equal_exprt &to_equal_expr(const exprt &expr)
1266{
1267 PRECONDITION(expr.id()==ID_equal);
1268 equal_exprt::check(expr);
1269 return static_cast<const equal_exprt &>(expr);
1270}
1271
1274{
1275 PRECONDITION(expr.id()==ID_equal);
1276 equal_exprt::check(expr);
1277 return static_cast<equal_exprt &>(expr);
1278}
1279
1280
1283{
1284public:
1286 : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1287 {
1288 }
1289};
1290
1291template <>
1292inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1293{
1294 return base.id() == ID_notequal;
1295}
1296
1297inline void validate_expr(const notequal_exprt &value)
1298{
1299 validate_operands(value, 2, "Inequality must have two operands");
1300}
1301
1308inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1309{
1310 PRECONDITION(expr.id()==ID_notequal);
1311 const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1312 validate_expr(ret);
1313 return ret;
1314}
1315
1318{
1319 PRECONDITION(expr.id()==ID_notequal);
1320 notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1321 validate_expr(ret);
1322 return ret;
1323}
1324
1325
1328{
1329public:
1330 // When _array has array_type, the type of _index
1331 // must be array_type.index_type().
1332 // This will eventually be enforced using a precondition.
1333 index_exprt(const exprt &_array, exprt _index)
1334 : binary_exprt(
1335 _array,
1336 ID_index,
1337 std::move(_index),
1338 _array.type().has_subtype()
1339 ? to_type_with_subtype(_array.type()).subtype()
1340 : typet(ID_nil))
1341 {
1342 }
1343
1344 index_exprt(exprt _array, exprt _index, typet _type)
1345 : binary_exprt(
1346 std::move(_array),
1347 ID_index,
1348 std::move(_index),
1349 std::move(_type))
1350 {
1351 }
1352
1354 {
1355 return op0();
1356 }
1357
1358 const exprt &array() const
1359 {
1360 return op0();
1361 }
1362
1364 {
1365 return op1();
1366 }
1367
1368 const exprt &index() const
1369 {
1370 return op1();
1371 }
1372};
1373
1374template <>
1375inline bool can_cast_expr<index_exprt>(const exprt &base)
1376{
1377 return base.id() == ID_index;
1378}
1379
1380inline void validate_expr(const index_exprt &value)
1381{
1382 validate_operands(value, 2, "Array index must have two operands");
1383}
1384
1391inline const index_exprt &to_index_expr(const exprt &expr)
1392{
1393 PRECONDITION(expr.id()==ID_index);
1394 const index_exprt &ret = static_cast<const index_exprt &>(expr);
1395 validate_expr(ret);
1396 return ret;
1397}
1398
1401{
1402 PRECONDITION(expr.id()==ID_index);
1403 index_exprt &ret = static_cast<index_exprt &>(expr);
1404 validate_expr(ret);
1405 return ret;
1406}
1407
1408
1411{
1412public:
1413 explicit array_of_exprt(exprt _what, array_typet _type)
1414 : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1415 {
1416 }
1417
1418 const array_typet &type() const
1419 {
1420 return static_cast<const array_typet &>(unary_exprt::type());
1421 }
1422
1424 {
1425 return static_cast<array_typet &>(unary_exprt::type());
1426 }
1427
1429 {
1430 return op0();
1431 }
1432
1433 const exprt &what() const
1434 {
1435 return op0();
1436 }
1437};
1438
1439template <>
1440inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1441{
1442 return base.id() == ID_array_of;
1443}
1444
1445inline void validate_expr(const array_of_exprt &value)
1446{
1447 validate_operands(value, 1, "'Array of' must have one operand");
1448}
1449
1456inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1457{
1458 PRECONDITION(expr.id()==ID_array_of);
1459 const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1460 validate_expr(ret);
1461 return ret;
1462}
1463
1466{
1467 PRECONDITION(expr.id()==ID_array_of);
1468 array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1469 validate_expr(ret);
1470 return ret;
1471}
1472
1473
1476{
1477public:
1479 : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1480 {
1481 }
1482
1483 const array_typet &type() const
1484 {
1485 return static_cast<const array_typet &>(multi_ary_exprt::type());
1486 }
1487
1489 {
1490 return static_cast<array_typet &>(multi_ary_exprt::type());
1491 }
1492};
1493
1494template <>
1495inline bool can_cast_expr<array_exprt>(const exprt &base)
1496{
1497 return base.id() == ID_array;
1498}
1499
1506inline const array_exprt &to_array_expr(const exprt &expr)
1507{
1508 PRECONDITION(expr.id()==ID_array);
1509 return static_cast<const array_exprt &>(expr);
1510}
1511
1514{
1515 PRECONDITION(expr.id()==ID_array);
1516 return static_cast<array_exprt &>(expr);
1517}
1518
1522{
1523public:
1525 : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1526 {
1527 }
1528
1529 const array_typet &type() const
1530 {
1531 return static_cast<const array_typet &>(multi_ary_exprt::type());
1532 }
1533
1535 {
1536 return static_cast<array_typet &>(multi_ary_exprt::type());
1537 }
1538
1540 void add(exprt index, exprt value)
1541 {
1542 add_to_operands(std::move(index), std::move(value));
1543 }
1544};
1545
1546template <>
1548{
1549 return base.id() == ID_array_list;
1550}
1551
1552inline void validate_expr(const array_list_exprt &value)
1553{
1554 PRECONDITION(value.operands().size() % 2 == 0);
1555}
1556
1558{
1560 auto &ret = static_cast<const array_list_exprt &>(expr);
1561 validate_expr(ret);
1562 return ret;
1563}
1564
1566{
1568 auto &ret = static_cast<array_list_exprt &>(expr);
1569 validate_expr(ret);
1570 return ret;
1571}
1572
1575{
1576public:
1578 : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1579 {
1580 }
1581};
1582
1583template <>
1584inline bool can_cast_expr<vector_exprt>(const exprt &base)
1585{
1586 return base.id() == ID_vector;
1587}
1588
1595inline const vector_exprt &to_vector_expr(const exprt &expr)
1596{
1597 PRECONDITION(expr.id()==ID_vector);
1598 return static_cast<const vector_exprt &>(expr);
1599}
1600
1603{
1604 PRECONDITION(expr.id()==ID_vector);
1605 return static_cast<vector_exprt &>(expr);
1606}
1607
1608
1611{
1612public:
1613 union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1614 : unary_exprt(ID_union, std::move(_value), std::move(_type))
1615 {
1616 set_component_name(_component_name);
1617 }
1618
1620 {
1621 return get(ID_component_name);
1622 }
1623
1624 void set_component_name(const irep_idt &component_name)
1625 {
1626 set(ID_component_name, component_name);
1627 }
1628
1629 std::size_t get_component_number() const
1630 {
1631 return get_size_t(ID_component_number);
1632 }
1633
1634 void set_component_number(std::size_t component_number)
1635 {
1636 set_size_t(ID_component_number, component_number);
1637 }
1638};
1639
1640template <>
1641inline bool can_cast_expr<union_exprt>(const exprt &base)
1642{
1643 return base.id() == ID_union;
1644}
1645
1646inline void validate_expr(const union_exprt &value)
1647{
1648 validate_operands(value, 1, "Union constructor must have one operand");
1649}
1650
1657inline const union_exprt &to_union_expr(const exprt &expr)
1658{
1659 PRECONDITION(expr.id()==ID_union);
1660 const union_exprt &ret = static_cast<const union_exprt &>(expr);
1661 validate_expr(ret);
1662 return ret;
1663}
1664
1667{
1668 PRECONDITION(expr.id()==ID_union);
1669 union_exprt &ret = static_cast<union_exprt &>(expr);
1670 validate_expr(ret);
1671 return ret;
1672}
1673
1677{
1678public:
1679 explicit empty_union_exprt(typet _type)
1680 : nullary_exprt(ID_empty_union, std::move(_type))
1681 {
1682 }
1683};
1684
1685template <>
1687{
1688 return base.id() == ID_empty_union;
1689}
1690
1691inline void validate_expr(const empty_union_exprt &value)
1692{
1694 value, 0, "Empty-union constructor must not have any operand");
1695}
1696
1704{
1705 PRECONDITION(expr.id() == ID_empty_union);
1706 const empty_union_exprt &ret = static_cast<const empty_union_exprt &>(expr);
1707 validate_expr(ret);
1708 return ret;
1709}
1710
1713{
1714 PRECONDITION(expr.id() == ID_empty_union);
1715 empty_union_exprt &ret = static_cast<empty_union_exprt &>(expr);
1716 validate_expr(ret);
1717 return ret;
1718}
1719
1722{
1723public:
1724 struct_exprt(operandst _operands, typet _type)
1725 : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1726 {
1727 }
1728
1729 exprt &component(const irep_idt &name, const namespacet &ns);
1730 const exprt &component(const irep_idt &name, const namespacet &ns) const;
1731};
1732
1733template <>
1734inline bool can_cast_expr<struct_exprt>(const exprt &base)
1735{
1736 return base.id() == ID_struct;
1737}
1738
1745inline const struct_exprt &to_struct_expr(const exprt &expr)
1746{
1747 PRECONDITION(expr.id()==ID_struct);
1748 return static_cast<const struct_exprt &>(expr);
1749}
1750
1753{
1754 PRECONDITION(expr.id()==ID_struct);
1755 return static_cast<struct_exprt &>(expr);
1756}
1757
1758
1761{
1762public:
1764 : binary_exprt(
1765 std::move(_real),
1766 ID_complex,
1767 std::move(_imag),
1768 std::move(_type))
1769 {
1770 }
1771
1773 {
1774 return op0();
1775 }
1776
1777 const exprt &real() const
1778 {
1779 return op0();
1780 }
1781
1783 {
1784 return op1();
1785 }
1786
1787 const exprt &imag() const
1788 {
1789 return op1();
1790 }
1791};
1792
1793template <>
1794inline bool can_cast_expr<complex_exprt>(const exprt &base)
1795{
1796 return base.id() == ID_complex;
1797}
1798
1799inline void validate_expr(const complex_exprt &value)
1800{
1801 validate_operands(value, 2, "Complex constructor must have two operands");
1802}
1803
1810inline const complex_exprt &to_complex_expr(const exprt &expr)
1811{
1812 PRECONDITION(expr.id()==ID_complex);
1813 const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1814 validate_expr(ret);
1815 return ret;
1816}
1817
1820{
1821 PRECONDITION(expr.id()==ID_complex);
1822 complex_exprt &ret = static_cast<complex_exprt &>(expr);
1823 validate_expr(ret);
1824 return ret;
1825}
1826
1829{
1830public:
1831 explicit complex_real_exprt(const exprt &op)
1832 : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1833 {
1834 }
1835};
1836
1837template <>
1839{
1840 return base.id() == ID_complex_real;
1841}
1842
1843inline void validate_expr(const complex_real_exprt &expr)
1844{
1846 expr, 1, "real part retrieval operation must have one operand");
1847}
1848
1856{
1857 PRECONDITION(expr.id() == ID_complex_real);
1858 const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
1859 validate_expr(ret);
1860 return ret;
1861}
1862
1865{
1866 PRECONDITION(expr.id() == ID_complex_real);
1867 complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
1868 validate_expr(ret);
1869 return ret;
1870}
1871
1874{
1875public:
1876 explicit complex_imag_exprt(const exprt &op)
1877 : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
1878 {
1879 }
1880};
1881
1882template <>
1884{
1885 return base.id() == ID_complex_imag;
1886}
1887
1888inline void validate_expr(const complex_imag_exprt &expr)
1889{
1891 expr, 1, "imaginary part retrieval operation must have one operand");
1892}
1893
1901{
1902 PRECONDITION(expr.id() == ID_complex_imag);
1903 const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
1904 validate_expr(ret);
1905 return ret;
1906}
1907
1910{
1911 PRECONDITION(expr.id() == ID_complex_imag);
1912 complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
1913 validate_expr(ret);
1914 return ret;
1915}
1916
1917
1920{
1921public:
1923 : unary_exprt(ID_typecast, std::move(op), std::move(_type))
1924 {
1925 }
1926
1927 // returns a typecast if the type doesn't already match
1928 static exprt conditional_cast(const exprt &expr, const typet &type)
1929 {
1930 if(expr.type() == type)
1931 return expr;
1932 else
1933 return typecast_exprt(expr, type);
1934 }
1935};
1936
1937template <>
1938inline bool can_cast_expr<typecast_exprt>(const exprt &base)
1939{
1940 return base.id() == ID_typecast;
1941}
1942
1943inline void validate_expr(const typecast_exprt &value)
1944{
1945 validate_operands(value, 1, "Typecast must have one operand");
1946}
1947
1954inline const typecast_exprt &to_typecast_expr(const exprt &expr)
1955{
1956 PRECONDITION(expr.id()==ID_typecast);
1957 const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
1958 validate_expr(ret);
1959 return ret;
1960}
1961
1964{
1965 PRECONDITION(expr.id()==ID_typecast);
1966 typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
1967 validate_expr(ret);
1968 return ret;
1969}
1970
1971
1974{
1975public:
1977 : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
1978 {
1979 }
1980
1983 ID_and,
1984 {std::move(op0), std::move(op1), std::move(op2)},
1985 bool_typet())
1986 {
1987 }
1988
1991 ID_and,
1992 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
1993 bool_typet())
1994 {
1995 }
1996
1997 explicit and_exprt(exprt::operandst _operands)
1998 : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
1999 {
2000 }
2001};
2002
2006
2008
2009template <>
2010inline bool can_cast_expr<and_exprt>(const exprt &base)
2011{
2012 return base.id() == ID_and;
2013}
2014
2021inline const and_exprt &to_and_expr(const exprt &expr)
2022{
2023 PRECONDITION(expr.id()==ID_and);
2024 return static_cast<const and_exprt &>(expr);
2025}
2026
2029{
2030 PRECONDITION(expr.id()==ID_and);
2031 return static_cast<and_exprt &>(expr);
2032}
2033
2034
2037{
2038public:
2040 : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2041 {
2042 }
2043};
2044
2045template <>
2046inline bool can_cast_expr<implies_exprt>(const exprt &base)
2047{
2048 return base.id() == ID_implies;
2049}
2050
2051inline void validate_expr(const implies_exprt &value)
2052{
2053 validate_operands(value, 2, "Implies must have two operands");
2054}
2055
2062inline const implies_exprt &to_implies_expr(const exprt &expr)
2063{
2064 PRECONDITION(expr.id()==ID_implies);
2065 const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2066 validate_expr(ret);
2067 return ret;
2068}
2069
2072{
2073 PRECONDITION(expr.id()==ID_implies);
2074 implies_exprt &ret = static_cast<implies_exprt &>(expr);
2075 validate_expr(ret);
2076 return ret;
2077}
2078
2079
2082{
2083public:
2085 : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2086 {
2087 }
2088
2091 ID_or,
2092 {std::move(op0), std::move(op1), std::move(op2)},
2093 bool_typet())
2094 {
2095 }
2096
2099 ID_or,
2100 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2101 bool_typet())
2102 {
2103 }
2104
2105 explicit or_exprt(exprt::operandst _operands)
2106 : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2107 {
2108 }
2109};
2110
2114
2116
2117template <>
2118inline bool can_cast_expr<or_exprt>(const exprt &base)
2119{
2120 return base.id() == ID_or;
2121}
2122
2129inline const or_exprt &to_or_expr(const exprt &expr)
2130{
2131 PRECONDITION(expr.id()==ID_or);
2132 return static_cast<const or_exprt &>(expr);
2133}
2134
2137{
2138 PRECONDITION(expr.id()==ID_or);
2139 return static_cast<or_exprt &>(expr);
2140}
2141
2142
2145{
2146public:
2148 : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2149 {
2150 }
2151};
2152
2153template <>
2154inline bool can_cast_expr<xor_exprt>(const exprt &base)
2155{
2156 return base.id() == ID_xor;
2157}
2158
2165inline const xor_exprt &to_xor_expr(const exprt &expr)
2166{
2167 PRECONDITION(expr.id()==ID_xor);
2168 return static_cast<const xor_exprt &>(expr);
2169}
2170
2173{
2174 PRECONDITION(expr.id()==ID_xor);
2175 return static_cast<xor_exprt &>(expr);
2176}
2177
2178
2181{
2182public:
2183 explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2184 {
2185 PRECONDITION(as_const(*this).op().type().id() == ID_bool);
2186 }
2187};
2188
2189template <>
2190inline bool can_cast_expr<not_exprt>(const exprt &base)
2191{
2192 return base.id() == ID_not;
2193}
2194
2195inline void validate_expr(const not_exprt &value)
2196{
2197 validate_operands(value, 1, "Not must have one operand");
2198}
2199
2206inline const not_exprt &to_not_expr(const exprt &expr)
2207{
2208 PRECONDITION(expr.id()==ID_not);
2209 const not_exprt &ret = static_cast<const not_exprt &>(expr);
2210 validate_expr(ret);
2211 return ret;
2212}
2213
2216{
2217 PRECONDITION(expr.id()==ID_not);
2218 not_exprt &ret = static_cast<not_exprt &>(expr);
2219 validate_expr(ret);
2220 return ret;
2221}
2222
2223
2226{
2227public:
2229 : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2230 {
2231 }
2232
2234 : ternary_exprt(
2235 ID_if,
2236 std::move(cond),
2237 std::move(t),
2238 std::move(f),
2239 std::move(type))
2240 {
2241 }
2242
2244 {
2245 return op0();
2246 }
2247
2248 const exprt &cond() const
2249 {
2250 return op0();
2251 }
2252
2254 {
2255 return op1();
2256 }
2257
2258 const exprt &true_case() const
2259 {
2260 return op1();
2261 }
2262
2264 {
2265 return op2();
2266 }
2267
2268 const exprt &false_case() const
2269 {
2270 return op2();
2271 }
2272};
2273
2274template <>
2275inline bool can_cast_expr<if_exprt>(const exprt &base)
2276{
2277 return base.id() == ID_if;
2278}
2279
2280inline void validate_expr(const if_exprt &value)
2281{
2282 validate_operands(value, 3, "If-then-else must have three operands");
2283}
2284
2291inline const if_exprt &to_if_expr(const exprt &expr)
2292{
2293 PRECONDITION(expr.id()==ID_if);
2294 const if_exprt &ret = static_cast<const if_exprt &>(expr);
2295 validate_expr(ret);
2296 return ret;
2297}
2298
2301{
2302 PRECONDITION(expr.id()==ID_if);
2303 if_exprt &ret = static_cast<if_exprt &>(expr);
2304 validate_expr(ret);
2305 return ret;
2306}
2307
2312{
2313public:
2314 with_exprt(const exprt &_old, exprt _where, exprt _new_value)
2316 ID_with,
2317 _old.type(),
2318 {_old, std::move(_where), std::move(_new_value)})
2319 {
2320 }
2321
2323 {
2324 return op0();
2325 }
2326
2327 const exprt &old() const
2328 {
2329 return op0();
2330 }
2331
2333 {
2334 return op1();
2335 }
2336
2337 const exprt &where() const
2338 {
2339 return op1();
2340 }
2341
2343 {
2344 return op2();
2345 }
2346
2347 const exprt &new_value() const
2348 {
2349 return op2();
2350 }
2351};
2352
2353template <>
2354inline bool can_cast_expr<with_exprt>(const exprt &base)
2355{
2356 return base.id() == ID_with;
2357}
2358
2359inline void validate_expr(const with_exprt &value)
2360{
2362 value, 3, "array/structure update must have at least 3 operands", true);
2364 value.operands().size() % 2 == 1,
2365 "array/structure update must have an odd number of operands");
2366}
2367
2374inline const with_exprt &to_with_expr(const exprt &expr)
2375{
2376 PRECONDITION(expr.id()==ID_with);
2377 const with_exprt &ret = static_cast<const with_exprt &>(expr);
2378 validate_expr(ret);
2379 return ret;
2380}
2381
2384{
2385 PRECONDITION(expr.id()==ID_with);
2386 with_exprt &ret = static_cast<with_exprt &>(expr);
2387 validate_expr(ret);
2388 return ret;
2389}
2390
2392{
2393public:
2394 explicit index_designatort(exprt _index)
2395 : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
2396 {
2397 }
2398
2399 const exprt &index() const
2400 {
2401 return op0();
2402 }
2403
2405 {
2406 return op0();
2407 }
2408};
2409
2410template <>
2412{
2413 return base.id() == ID_index_designator;
2414}
2415
2416inline void validate_expr(const index_designatort &value)
2417{
2418 validate_operands(value, 1, "Index designator must have one operand");
2419}
2420
2428{
2429 PRECONDITION(expr.id()==ID_index_designator);
2430 const index_designatort &ret = static_cast<const index_designatort &>(expr);
2431 validate_expr(ret);
2432 return ret;
2433}
2434
2437{
2438 PRECONDITION(expr.id()==ID_index_designator);
2439 index_designatort &ret = static_cast<index_designatort &>(expr);
2440 validate_expr(ret);
2441 return ret;
2442}
2443
2445{
2446public:
2447 explicit member_designatort(const irep_idt &_component_name)
2448 : expr_protectedt(ID_member_designator, typet())
2449 {
2450 set(ID_component_name, _component_name);
2451 }
2452
2454 {
2455 return get(ID_component_name);
2456 }
2457};
2458
2459template <>
2461{
2462 return base.id() == ID_member_designator;
2463}
2464
2465inline void validate_expr(const member_designatort &value)
2466{
2467 validate_operands(value, 0, "Member designator must not have operands");
2468}
2469
2477{
2478 PRECONDITION(expr.id()==ID_member_designator);
2479 const member_designatort &ret = static_cast<const member_designatort &>(expr);
2480 validate_expr(ret);
2481 return ret;
2482}
2483
2486{
2487 PRECONDITION(expr.id()==ID_member_designator);
2488 member_designatort &ret = static_cast<member_designatort &>(expr);
2489 validate_expr(ret);
2490 return ret;
2491}
2492
2493
2496{
2497public:
2498 update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
2499 : ternary_exprt(
2500 ID_update,
2501 _old,
2502 std::move(_designator),
2503 std::move(_new_value),
2504 _old.type())
2505 {
2506 }
2507
2509 {
2510 return op0();
2511 }
2512
2513 const exprt &old() const
2514 {
2515 return op0();
2516 }
2517
2518 // the designator operands are either
2519 // 1) member_designator or
2520 // 2) index_designator
2521 // as defined above
2523 {
2524 return op1().operands();
2525 }
2526
2528 {
2529 return op1().operands();
2530 }
2531
2533 {
2534 return op2();
2535 }
2536
2537 const exprt &new_value() const
2538 {
2539 return op2();
2540 }
2541};
2542
2543template <>
2544inline bool can_cast_expr<update_exprt>(const exprt &base)
2545{
2546 return base.id() == ID_update;
2547}
2548
2549inline void validate_expr(const update_exprt &value)
2550{
2552 value, 3, "Array/structure update must have three operands");
2553}
2554
2561inline const update_exprt &to_update_expr(const exprt &expr)
2562{
2563 PRECONDITION(expr.id()==ID_update);
2564 const update_exprt &ret = static_cast<const update_exprt &>(expr);
2565 validate_expr(ret);
2566 return ret;
2567}
2568
2571{
2572 PRECONDITION(expr.id()==ID_update);
2573 update_exprt &ret = static_cast<update_exprt &>(expr);
2574 validate_expr(ret);
2575 return ret;
2576}
2577
2578
2579#if 0
2581class array_update_exprt:public expr_protectedt
2582{
2583public:
2584 array_update_exprt(
2585 const exprt &_array,
2586 const exprt &_index,
2587 const exprt &_new_value):
2588 exprt(ID_array_update, _array.type())
2589 {
2590 add_to_operands(_array, _index, _new_value);
2591 }
2592
2593 array_update_exprt():expr_protectedt(ID_array_update)
2594 {
2595 operands().resize(3);
2596 }
2597
2598 exprt &array()
2599 {
2600 return op0();
2601 }
2602
2603 const exprt &array() const
2604 {
2605 return op0();
2606 }
2607
2608 exprt &index()
2609 {
2610 return op1();
2611 }
2612
2613 const exprt &index() const
2614 {
2615 return op1();
2616 }
2617
2618 exprt &new_value()
2619 {
2620 return op2();
2621 }
2622
2623 const exprt &new_value() const
2624 {
2625 return op2();
2626 }
2627};
2628
2629template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2630{
2631 return base.id()==ID_array_update;
2632}
2633
2634inline void validate_expr(const array_update_exprt &value)
2635{
2636 validate_operands(value, 3, "Array update must have three operands");
2637}
2638
2645inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2646{
2647 PRECONDITION(expr.id()==ID_array_update);
2648 const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2649 validate_expr(ret);
2650 return ret;
2651}
2652
2654inline array_update_exprt &to_array_update_expr(exprt &expr)
2655{
2656 PRECONDITION(expr.id()==ID_array_update);
2657 array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2658 validate_expr(ret);
2659 return ret;
2660}
2661
2662#endif
2663
2664
2667{
2668public:
2669 member_exprt(exprt op, const irep_idt &component_name, typet _type)
2670 : unary_exprt(ID_member, std::move(op), std::move(_type))
2671 {
2672 set_component_name(component_name);
2673 }
2674
2676 : unary_exprt(ID_member, std::move(op), c.type())
2677 {
2679 }
2680
2682 {
2683 return get(ID_component_name);
2684 }
2685
2686 void set_component_name(const irep_idt &component_name)
2687 {
2688 set(ID_component_name, component_name);
2689 }
2690
2691 std::size_t get_component_number() const
2692 {
2693 return get_size_t(ID_component_number);
2694 }
2695
2696 // will go away, use compound()
2697 const exprt &struct_op() const
2698 {
2699 return op0();
2700 }
2701
2702 // will go away, use compound()
2704 {
2705 return op0();
2706 }
2707
2708 const exprt &compound() const
2709 {
2710 return op0();
2711 }
2712
2714 {
2715 return op0();
2716 }
2717
2718 static void check(
2719 const exprt &expr,
2721 {
2722 DATA_CHECK(
2723 vm,
2724 expr.operands().size() == 1,
2725 "member expression must have one operand");
2726 }
2727
2728 static void validate(
2729 const exprt &expr,
2730 const namespacet &ns,
2732};
2733
2734template <>
2735inline bool can_cast_expr<member_exprt>(const exprt &base)
2736{
2737 return base.id() == ID_member;
2738}
2739
2740inline void validate_expr(const member_exprt &value)
2741{
2742 validate_operands(value, 1, "Extract member must have one operand");
2743}
2744
2751inline const member_exprt &to_member_expr(const exprt &expr)
2752{
2753 PRECONDITION(expr.id()==ID_member);
2754 const member_exprt &ret = static_cast<const member_exprt &>(expr);
2755 validate_expr(ret);
2756 return ret;
2757}
2758
2761{
2762 PRECONDITION(expr.id()==ID_member);
2763 member_exprt &ret = static_cast<member_exprt &>(expr);
2764 validate_expr(ret);
2765 return ret;
2766}
2767
2768
2771{
2772public:
2773 explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
2774 {
2775 }
2776};
2777
2778template <>
2779inline bool can_cast_expr<type_exprt>(const exprt &base)
2780{
2781 return base.id() == ID_type;
2782}
2783
2790inline const type_exprt &to_type_expr(const exprt &expr)
2791{
2793 const type_exprt &ret = static_cast<const type_exprt &>(expr);
2794 return ret;
2795}
2796
2799{
2801 type_exprt &ret = static_cast<type_exprt &>(expr);
2802 return ret;
2803}
2804
2807{
2808public:
2809 constant_exprt(const irep_idt &_value, typet _type)
2810 : expr_protectedt(ID_constant, std::move(_type))
2811 {
2812 set_value(_value);
2813 }
2814
2815 const irep_idt &get_value() const
2816 {
2817 return get(ID_value);
2818 }
2819
2820 void set_value(const irep_idt &value)
2821 {
2822 set(ID_value, value);
2823 }
2824
2825 bool value_is_zero_string() const;
2826};
2827
2828template <>
2829inline bool can_cast_expr<constant_exprt>(const exprt &base)
2830{
2831 return base.id() == ID_constant;
2832}
2833
2840inline const constant_exprt &to_constant_expr(const exprt &expr)
2841{
2842 PRECONDITION(expr.id()==ID_constant);
2843 return static_cast<const constant_exprt &>(expr);
2844}
2845
2848{
2849 PRECONDITION(expr.id()==ID_constant);
2850 return static_cast<constant_exprt &>(expr);
2851}
2852
2853
2856{
2857public:
2859 {
2860 }
2861};
2862
2865{
2866public:
2868 {
2869 }
2870};
2871
2874{
2875public:
2877 : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
2878 {
2879 }
2880};
2881
2882template <>
2883inline bool can_cast_expr<nil_exprt>(const exprt &base)
2884{
2885 return base.id() == ID_nil;
2886}
2887
2890{
2891public:
2892 explicit infinity_exprt(typet _type)
2893 : nullary_exprt(ID_infinity, std::move(_type))
2894 {
2895 }
2896};
2897
2900{
2901public:
2902 using variablest = std::vector<symbol_exprt>;
2903
2906 irep_idt _id,
2907 const variablest &_variables,
2908 exprt _where,
2909 typet _type)
2910 : binary_exprt(
2912 ID_tuple,
2913 (const operandst &)_variables,
2914 typet(ID_tuple)),
2915 _id,
2916 std::move(_where),
2917 std::move(_type))
2918 {
2919 }
2920
2922 {
2924 }
2925
2926 const variablest &variables() const
2927 {
2929 }
2930
2932 {
2933 return op1();
2934 }
2935
2936 const exprt &where() const
2937 {
2938 return op1();
2939 }
2940
2943 exprt instantiate(const exprt::operandst &) const;
2944
2947 exprt instantiate(const variablest &) const;
2948};
2949
2950inline void validate_expr(const binding_exprt &binding_expr)
2951{
2953 binding_expr, 2, "Binding expressions must have two operands");
2954}
2955
2962inline const binding_exprt &to_binding_expr(const exprt &expr)
2963{
2965 expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda);
2966 const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
2967 validate_expr(ret);
2968 return ret;
2969}
2970
2973{
2974public:
2978 const exprt &where)
2979 : binary_exprt(
2981 ID_let_binding,
2982 std::move(variables),
2983 where,
2984 where.type()),
2985 ID_let,
2986 multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
2987 where.type())
2988 {
2989 PRECONDITION(this->variables().size() == this->values().size());
2990 }
2991
2994 : let_exprt(
2996 operandst{std::move(value)},
2997 where)
2998 {
2999 }
3000
3002 {
3003 return static_cast<binding_exprt &>(op0());
3004 }
3005
3006 const binding_exprt &binding() const
3007 {
3008 return static_cast<const binding_exprt &>(op0());
3009 }
3010
3013 {
3014 auto &variables = binding().variables();
3015 PRECONDITION(variables.size() == 1);
3016 return variables.front();
3017 }
3018
3020 const symbol_exprt &symbol() const
3021 {
3022 const auto &variables = binding().variables();
3023 PRECONDITION(variables.size() == 1);
3024 return variables.front();
3025 }
3026
3029 {
3030 auto &values = this->values();
3031 PRECONDITION(values.size() == 1);
3032 return values.front();
3033 }
3034
3036 const exprt &value() const
3037 {
3038 const auto &values = this->values();
3039 PRECONDITION(values.size() == 1);
3040 return values.front();
3041 }
3042
3044 {
3045 return static_cast<multi_ary_exprt &>(op1()).operands();
3046 }
3047
3048 const operandst &values() const
3049 {
3050 return static_cast<const multi_ary_exprt &>(op1()).operands();
3051 }
3052
3055 {
3056 return binding().variables();
3057 }
3058
3061 {
3062 return binding().variables();
3063 }
3064
3067 {
3068 return binding().where();
3069 }
3070
3072 const exprt &where() const
3073 {
3074 return binding().where();
3075 }
3076
3077 static void validate(const exprt &, validation_modet);
3078};
3079
3080template <>
3081inline bool can_cast_expr<let_exprt>(const exprt &base)
3082{
3083 return base.id() == ID_let;
3084}
3085
3086inline void validate_expr(const let_exprt &let_expr)
3087{
3088 validate_operands(let_expr, 2, "Let must have two operands");
3089}
3090
3097inline const let_exprt &to_let_expr(const exprt &expr)
3098{
3099 PRECONDITION(expr.id()==ID_let);
3100 const let_exprt &ret = static_cast<const let_exprt &>(expr);
3101 validate_expr(ret);
3102 return ret;
3103}
3104
3107{
3108 PRECONDITION(expr.id()==ID_let);
3109 let_exprt &ret = static_cast<let_exprt &>(expr);
3110 validate_expr(ret);
3111 return ret;
3112}
3113
3114
3119{
3120public:
3121 cond_exprt(operandst _operands, typet _type)
3122 : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3123 {
3124 }
3125
3129 void add_case(const exprt &condition, const exprt &value)
3130 {
3131 PRECONDITION(condition.type().id() == ID_bool);
3132 operands().reserve(operands().size() + 2);
3133 operands().push_back(condition);
3134 operands().push_back(value);
3135 }
3136};
3137
3138template <>
3139inline bool can_cast_expr<cond_exprt>(const exprt &base)
3140{
3141 return base.id() == ID_cond;
3142}
3143
3144inline void validate_expr(const cond_exprt &value)
3145{
3147 value.operands().size() % 2 == 0, "cond must have even number of operands");
3148}
3149
3156inline const cond_exprt &to_cond_expr(const exprt &expr)
3157{
3158 PRECONDITION(expr.id() == ID_cond);
3159 const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3160 validate_expr(ret);
3161 return ret;
3162}
3163
3166{
3167 PRECONDITION(expr.id() == ID_cond);
3168 cond_exprt &ret = static_cast<cond_exprt &>(expr);
3169 validate_expr(ret);
3170 return ret;
3171}
3172
3182{
3183public:
3186 exprt body,
3187 array_typet _type)
3188 : binding_exprt(
3189 ID_array_comprehension,
3190 {std::move(arg)},
3191 std::move(body),
3192 std::move(_type))
3193 {
3194 }
3195
3196 const array_typet &type() const
3197 {
3198 return static_cast<const array_typet &>(binary_exprt::type());
3199 }
3200
3202 {
3203 return static_cast<array_typet &>(binary_exprt::type());
3204 }
3205
3206 const symbol_exprt &arg() const
3207 {
3208 auto &variables = this->variables();
3209 PRECONDITION(variables.size() == 1);
3210 return variables[0];
3211 }
3212
3214 {
3215 auto &variables = this->variables();
3216 PRECONDITION(variables.size() == 1);
3217 return variables[0];
3218 }
3219
3220 const exprt &body() const
3221 {
3222 return where();
3223 }
3224
3226 {
3227 return where();
3228 }
3229};
3230
3231template <>
3233{
3234 return base.id() == ID_array_comprehension;
3235}
3236
3238{
3239 validate_operands(value, 2, "'Array comprehension' must have two operands");
3240}
3241
3248inline const array_comprehension_exprt &
3250{
3251 PRECONDITION(expr.id() == ID_array_comprehension);
3252 const array_comprehension_exprt &ret =
3253 static_cast<const array_comprehension_exprt &>(expr);
3254 validate_expr(ret);
3255 return ret;
3256}
3257
3260{
3261 PRECONDITION(expr.id() == ID_array_comprehension);
3263 static_cast<array_comprehension_exprt &>(expr);
3264 validate_expr(ret);
3265 return ret;
3266}
3267
3268inline void validate_expr(const class class_method_descriptor_exprt &value);
3269
3272{
3273public:
3289 typet _type,
3293 : nullary_exprt(ID_virtual_function, std::move(_type))
3294 {
3296 set(ID_component_name, std::move(mangled_method_name));
3297 set(ID_C_class, std::move(class_id));
3298 set(ID_C_base_name, std::move(base_method_name));
3299 set(ID_identifier, std::move(id));
3300 validate_expr(*this);
3301 }
3302
3310 {
3311 return get(ID_component_name);
3312 }
3313
3317 const irep_idt &class_id() const
3318 {
3319 return get(ID_C_class);
3320 }
3321
3325 {
3326 return get(ID_C_base_name);
3327 }
3328
3333 {
3334 return get(ID_identifier);
3335 }
3336};
3337
3338inline void validate_expr(const class class_method_descriptor_exprt &value)
3339{
3340 validate_operands(value, 0, "class method descriptor must not have operands");
3342 !value.mangled_method_name().empty(),
3343 "class method descriptor must have a mangled method name.");
3345 !value.class_id().empty(), "class method descriptor must have a class id.");
3347 !value.base_method_name().empty(),
3348 "class method descriptor must have a base method name.");
3350 value.get_identifier() == id2string(value.class_id()) + "." +
3352 "class method descriptor must have an identifier in the expected format.");
3353}
3354
3361inline const class_method_descriptor_exprt &
3363{
3364 PRECONDITION(expr.id() == ID_virtual_function);
3366 static_cast<const class_method_descriptor_exprt &>(expr);
3367 validate_expr(ret);
3368 return ret;
3369}
3370
3371template <>
3373{
3374 return base.id() == ID_virtual_function;
3375}
3376
3377#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:346
abs_exprt(exprt _op)
Definition std_expr.h:348
Boolean AND.
Definition std_expr.h:1974
and_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:1981
and_exprt(exprt op0, exprt op1)
Definition std_expr.h:1976
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:1989
and_exprt(exprt::operandst _operands)
Definition std_expr.h:1997
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3182
const array_typet & type() const
Definition std_expr.h:3196
const symbol_exprt & arg() const
Definition std_expr.h:3206
const exprt & body() const
Definition std_expr.h:3220
array_typet & type()
Definition std_expr.h:3201
symbol_exprt & arg()
Definition std_expr.h:3213
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition std_expr.h:3184
Array constructor from list of elements.
Definition std_expr.h:1476
const array_typet & type() const
Definition std_expr.h:1483
array_exprt(operandst _operands, array_typet _type)
Definition std_expr.h:1478
array_typet & type()
Definition std_expr.h:1488
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition std_expr.h:1522
void add(exprt index, exprt value)
add an index/value pair
Definition std_expr.h:1540
const array_typet & type() const
Definition std_expr.h:1529
array_list_exprt(operandst _operands, array_typet _type)
Definition std_expr.h:1524
array_typet & type()
Definition std_expr.h:1534
Array constructor from single element.
Definition std_expr.h:1411
array_typet & type()
Definition std_expr.h:1423
array_of_exprt(exprt _what, array_typet _type)
Definition std_expr.h:1413
const exprt & what() const
Definition std_expr.h:1433
const array_typet & type() const
Definition std_expr.h:1418
exprt & what()
Definition std_expr.h:1428
Arrays with given size.
Definition std_types.h:763
A base class for binary expressions.
Definition std_expr.h:550
exprt & lhs()
Definition std_expr.h:580
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:552
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:572
const exprt & op2() const =delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:562
exprt & rhs()
Definition std_expr.h:590
exprt & op0()
Definition expr.h:99
const exprt & lhs() const
Definition std_expr.h:585
exprt & op1()
Definition expr.h:102
exprt & op3()=delete
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition std_expr.h:557
const exprt & rhs() const
Definition std_expr.h:595
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:643
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:650
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition std_expr.h:645
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:657
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:676
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:681
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:688
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:2900
const variablest & variables() const
Definition std_expr.h:2926
const exprt & where() const
Definition std_expr.h:2936
exprt & where()
Definition std_expr.h:2931
variablest & variables()
Definition std_expr.h:2921
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition std_expr.h:2905
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:234
std::vector< symbol_exprt > variablest
Definition std_expr.h:2902
The Boolean type.
Definition std_types.h:36
An expression describing a method on a class.
Definition std_expr.h:3272
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:3324
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition std_expr.h:3309
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:3332
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition std_expr.h:3288
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:3317
Complex constructor from a pair of numbers.
Definition std_expr.h:1761
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition std_expr.h:1763
exprt real()
Definition std_expr.h:1772
exprt imag()
Definition std_expr.h:1782
const exprt & real() const
Definition std_expr.h:1777
const exprt & imag() const
Definition std_expr.h:1787
Imaginary part of the expression describing a complex number.
Definition std_expr.h:1874
complex_imag_exprt(const exprt &op)
Definition std_expr.h:1876
Real part of the expression describing a complex number.
Definition std_expr.h:1829
complex_real_exprt(const exprt &op)
Definition std_expr.h:1831
Complex numbers made of pair of given subtype.
Definition std_types.h:1057
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition std_expr.h:3119
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition std_expr.h:3129
cond_exprt(operandst _operands, typet _type)
Definition std_expr.h:3121
A constant literal expression.
Definition std_expr.h:2807
const irep_idt & get_value() const
Definition std_expr.h:2815
bool value_is_zero_string() const
Definition std_expr.cpp:16
constant_exprt(const irep_idt &_value, typet _type)
Definition std_expr.h:2809
void set_value(const irep_idt &value)
Definition std_expr.h:2820
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition std_expr.h:132
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:136
bool is_static_lifetime() const
Definition std_expr.h:141
bool is_thread_local() const
Definition std_expr.h:156
Division.
Definition std_expr.h:1064
div_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1066
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition std_expr.h:1072
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition std_expr.h:1078
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1090
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1084
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1677
empty_union_exprt(typet _type)
Definition std_expr.h:1679
Equality.
Definition std_expr.h:1225
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:1232
equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1227
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:1239
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1179
euclidean_mod_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1181
Base class for all expressions.
Definition expr.h:343
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
exprt & op2()
Definition expr.h:105
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
exprt & op2()
Definition expr.h:105
source_locationt & add_source_location()
Definition expr.h:235
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:136
The Boolean constant false.
Definition std_expr.h:2865
Binary greater than operator expression.
Definition std_expr.h:719
greater_than_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:721
Binary greater than or equal operator expression.
Definition std_expr.h:740
greater_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:742
The trinary if-then-else operator.
Definition std_expr.h:2226
const exprt & false_case() const
Definition std_expr.h:2268
exprt & cond()
Definition std_expr.h:2243
const exprt & cond() const
Definition std_expr.h:2248
if_exprt(exprt cond, const exprt &t, exprt f)
Definition std_expr.h:2228
const exprt & true_case() const
Definition std_expr.h:2258
exprt & false_case()
Definition std_expr.h:2263
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition std_expr.h:2233
exprt & true_case()
Definition std_expr.h:2253
Boolean implication.
Definition std_expr.h:2037
implies_exprt(exprt op0, exprt op1)
Definition std_expr.h:2039
const exprt & index() const
Definition std_expr.h:2399
index_designatort(exprt _index)
Definition std_expr.h:2394
exprt & index()
Definition std_expr.h:2404
Array index operator.
Definition std_expr.h:1328
exprt & index()
Definition std_expr.h:1363
index_exprt(exprt _array, exprt _index, typet _type)
Definition std_expr.h:1344
index_exprt(const exprt &_array, exprt _index)
Definition std_expr.h:1333
exprt & array()
Definition std_expr.h:1353
const exprt & index() const
Definition std_expr.h:1368
const exprt & array() const
Definition std_expr.h:1358
An expression denoting infinity.
Definition std_expr.h:2890
infinity_exprt(typet _type)
Definition std_expr.h:2892
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:68
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void remove(const irep_idt &name)
Definition irep.cpp:96
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:87
const irep_idt & id() const
Definition irep.h:396
Binary less than operator expression.
Definition std_expr.h:761
less_than_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:763
Binary less than or equal operator expression.
Definition std_expr.h:782
less_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:784
A let expression.
Definition std_expr.h:2973
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3054
const binding_exprt & binding() const
Definition std_expr.h:3006
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition std_expr.h:3060
operandst & values()
Definition std_expr.h:3043
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition std_expr.h:2993
const exprt & where() const
convenience accessor for binding().where()
Definition std_expr.h:3072
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:114
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition std_expr.h:3020
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition std_expr.h:2975
exprt & value()
convenience accessor for the value of a single binding
Definition std_expr.h:3028
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3066
binding_exprt & binding()
Definition std_expr.h:3001
const operandst & values() const
Definition std_expr.h:3048
const exprt & value() const
convenience accessor for the value of a single binding
Definition std_expr.h:3036
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition std_expr.h:3012
irep_idt get_component_name() const
Definition std_expr.h:2453
member_designatort(const irep_idt &_component_name)
Definition std_expr.h:2447
Extract member of struct or union.
Definition std_expr.h:2667
const exprt & compound() const
Definition std_expr.h:2708
exprt & struct_op()
Definition std_expr.h:2703
const exprt & struct_op() const
Definition std_expr.h:2697
irep_idt get_component_name() const
Definition std_expr.h:2681
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:2686
exprt & compound()
Definition std_expr.h:2713
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:81
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2718
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition std_expr.h:2669
std::size_t get_component_number() const
Definition std_expr.h:2691
member_exprt(exprt op, const struct_typet::componentt &c)
Definition std_expr.h:2675
Binary minus.
Definition std_expr.h:973
minus_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:975
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1135
mod_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1137
Binary multiplication Associativity is not specified.
Definition std_expr.h:1019
mult_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1021
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:824
exprt & op1()
Definition std_expr.h:850
const exprt & op0() const
Definition std_expr.h:868
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition std_expr.h:837
const exprt & op2() const
Definition std_expr.h:880
const exprt & op3() const
Definition std_expr.h:886
exprt & op0()
Definition std_expr.h:844
exprt & op2()
Definition std_expr.h:856
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:832
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition std_expr.h:826
const exprt & op1() const
Definition std_expr.h:874
exprt & op3()
Definition std_expr.h:862
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:2874
Expression to hold a nondeterministic choice.
Definition std_expr.h:209
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:232
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:213
const irep_idt & get_identifier() const
Definition std_expr.h:237
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition std_expr.h:222
Boolean negation.
Definition std_expr.h:2181
not_exprt(exprt _op)
Definition std_expr.h:2183
Disequality.
Definition std_expr.h:1283
notequal_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:1285
An expression without operands.
Definition std_expr.h:22
exprt & op0()=delete
void move_to_operands(exprt &, exprt &)=delete
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 move_to_operands(exprt &)=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
void move_to_operands(exprt &, exprt &, 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:2082
or_exprt(exprt op0, exprt op1, exprt op2)
Definition std_expr.h:2089
or_exprt(exprt::operandst _operands)
Definition std_expr.h:2105
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition std_expr.h:2097
or_exprt(exprt op0, exprt op1)
Definition std_expr.h:2084
The plus expression Associativity is not specified.
Definition std_expr.h:914
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition std_expr.h:921
plus_exprt(exprt _lhs, exprt _rhs)
Definition std_expr.h:916
plus_exprt(operandst _operands, typet _type)
Definition std_expr.h:930
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition std_expr.h:484
predicate_exprt(const irep_idt &_id)
Definition std_expr.h:486
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:506
sign_exprt(exprt _op)
Definition std_expr.h:508
Struct constructor from list of elements.
Definition std_expr.h:1722
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:62
struct_exprt(operandst _operands, typet _type)
Definition std_expr.h:1724
const irep_idt & get_name() const
Definition std_types.h:79
Expression to hold a symbol (variable)
Definition std_expr.h:80
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:104
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:99
symbol_exprt(typet type)
Definition std_expr.h:83
symbol_exprt(const irep_idt &identifier, typet type)
Definition std_expr.h:89
const irep_idt & get_identifier() const
Definition std_expr.h:109
An expression with three operands.
Definition std_expr.h:53
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition std_expr.h:56
const exprt & op3() const =delete
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
exprt & op2()
Definition expr.h:105
exprt & op3()=delete
The Boolean constant true.
Definition std_expr.h:2856
An expression denoting a type.
Definition std_expr.h:2771
type_exprt(typet type)
Definition std_expr.h:2773
Semantic type conversion.
Definition std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
typecast_exprt(exprt op, typet _type)
Definition std_expr.h:1922
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:281
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition std_expr.h:283
const exprt & op3() const =delete
exprt & op2()=delete
const exprt & op1() const =delete
exprt & op3()=delete
const exprt & op() const
Definition std_expr.h:293
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition std_expr.h:288
const exprt & op2() const =delete
exprt & op()
Definition std_expr.h:298
exprt & op1()=delete
The unary minus expression.
Definition std_expr.h:390
unary_minus_exprt(exprt _op)
Definition std_expr.h:397
unary_minus_exprt(exprt _op, typet _type)
Definition std_expr.h:392
The unary plus expression.
Definition std_expr.h:439
unary_plus_exprt(exprt op)
Definition std_expr.h:441
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:495
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition std_expr.h:497
Union constructor from single element.
Definition std_expr.h:1611
std::size_t get_component_number() const
Definition std_expr.h:1629
void set_component_number(std::size_t component_number)
Definition std_expr.h:1634
void set_component_name(const irep_idt &component_name)
Definition std_expr.h:1624
irep_idt get_component_name() const
Definition std_expr.h:1619
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition std_expr.h:1613
Operator to update elements in structs and arrays.
Definition std_expr.h:2496
exprt & old()
Definition std_expr.h:2508
exprt::operandst & designator()
Definition std_expr.h:2522
exprt & new_value()
Definition std_expr.h:2532
const exprt & new_value() const
Definition std_expr.h:2537
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition std_expr.h:2498
const exprt & old() const
Definition std_expr.h:2513
const exprt::operandst & designator() const
Definition std_expr.h:2527
Vector constructor from list of elements.
Definition std_expr.h:1575
vector_exprt(operandst _operands, vector_typet _type)
Definition std_expr.h:1577
The vector type.
Definition std_types.h:996
Operator to update elements in structs and arrays.
Definition std_expr.h:2312
const exprt & old() const
Definition std_expr.h:2327
const exprt & where() const
Definition std_expr.h:2337
exprt & new_value()
Definition std_expr.h:2342
exprt & where()
Definition std_expr.h:2332
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition std_expr.h:2314
const exprt & new_value() const
Definition std_expr.h:2347
exprt & old()
Definition std_expr.h:2322
Boolean XOR.
Definition std_expr.h:2145
xor_exprt(exprt _op0, exprt _op1)
Definition std_expr.h:2147
Templated functions to cast to specific exprt-derived classes.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
const irept & get_nil_irep()
Definition irep.cpp:20
dstring_hash irep_id_hash
Definition irep.h:39
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition std_expr.h:1249
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition std_expr.h:1292
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition std_expr.h:1794
bool can_cast_expr< not_exprt >(const exprt &base)
Definition std_expr.h:2190
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1745
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition std_expr.h:1557
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition std_expr.h:1938
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition std_expr.h:2790
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1456
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition std_expr.h:1734
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:807
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition std_expr.h:464
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition std_expr.h:2154
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition std_expr.h:1028
bool can_cast_expr< if_exprt >(const exprt &base)
Definition std_expr.h:2275
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:3362
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1160
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1044
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition std_expr.h:2021
bool can_cast_expr< member_designatort >(const exprt &base)
Definition std_expr.h:2460
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3249
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition std_expr.h:3232
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition std_expr.h:2165
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2129
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1506
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition std_expr.h:1883
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition std_expr.h:354
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition std_expr.h:515
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition std_expr.h:3156
bool can_cast_expr< type_exprt >(const exprt &base)
Definition std_expr.h:2779
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:22
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition std_expr.h:3372
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
void validate_expr(const symbol_exprt &value)
Definition std_expr.h:178
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1113
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition std_expr.h:404
bool can_cast_expr< less_than_exprt >(const exprt &base)
Definition std_expr.h:770
bool can_cast_expr< with_exprt >(const exprt &base)
Definition std_expr.h:2354
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition std_expr.h:1595
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:34
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition std_expr.h:982
bool can_cast_expr< let_exprt >(const exprt &base)
Definition std_expr.h:3081
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:953
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition std_expr.h:1308
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition std_expr.h:937
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:899
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition std_expr.h:1440
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3097
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition std_expr.h:370
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition std_expr.h:244
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition std_expr.h:2829
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
bool can_cast_expr< index_exprt >(const exprt &base)
Definition std_expr.h:1375
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:173
const empty_union_exprt & to_empty_union_expr(const exprt &expr)
Cast an exprt to an empty_union_exprt.
Definition std_expr.h:1703
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:998
bool can_cast_expr< member_exprt >(const exprt &base)
Definition std_expr.h:2735
bool can_cast_expr< empty_union_exprt >(const exprt &base)
Definition std_expr.h:1686
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:1900
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition std_expr.h:2962
bool can_cast_expr< or_exprt >(const exprt &base)
Definition std_expr.h:2118
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition std_expr.h:1144
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2427
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1657
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition std_expr.h:3139
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:1855
bool can_cast_expr< update_exprt >(const exprt &base)
Definition std_expr.h:2544
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition std_expr.h:707
bool can_cast_expr< euclidean_mod_exprt >(const exprt &base)
Definition std_expr.h:1188
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition std_expr.h:1584
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition std_expr.h:1547
bool can_cast_expr< index_designatort >(const exprt &base)
Definition std_expr.h:2411
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2374
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1810
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition std_expr.h:448
bool can_cast_expr< and_exprt >(const exprt &base)
Definition std_expr.h:2010
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition std_expr.h:728
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2062
bool can_cast_expr< array_exprt >(const exprt &base)
Definition std_expr.h:1495
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition std_expr.h:611
bool can_cast_expr< div_exprt >(const exprt &base)
Definition std_expr.h:1097
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2561
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition std_expr.h:2883
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:420
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1265
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
Definition std_expr.h:749
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition std_expr.h:2046
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition std_expr.h:312
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
Definition std_expr.h:791
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition std_expr.h:260
bool can_cast_expr< union_exprt >(const exprt &base)
Definition std_expr.h:1641
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition std_expr.h:2476
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition std_expr.h:1838
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition std_expr.h:531
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition std_expr.h:1204
Pre-defined types.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1082
size_t operator()(const ::symbol_exprt &sym)
Definition std_expr.h:122
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177
#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