cprover
std_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_STD_EXPR_H
11 #define CPROVER_UTIL_STD_EXPR_H
12 
20 #include "invariant.h"
21 #include "std_types.h"
22 
31 class transt:public exprt
32 {
33 public:
35  {
36  id(ID_trans);
37  operands().resize(3);
38  }
39 
40  exprt &invar() { return op0(); }
41  exprt &init() { return op1(); }
42  exprt &trans() { return op2(); }
43 
44  const exprt &invar() const { return op0(); }
45  const exprt &init() const { return op1(); }
46  const exprt &trans() const { return op2(); }
47 };
48 
59 inline const transt &to_trans_expr(const exprt &expr)
60 {
61  PRECONDITION(expr.id()==ID_trans);
63  expr.operands().size()==3,
64  "Transition systems must have three operands");
65  return static_cast<const transt &>(expr);
66 }
67 
71 inline transt &to_trans_expr(exprt &expr)
72 {
73  PRECONDITION(expr.id()==ID_trans);
75  expr.operands().size()==3,
76  "Transition systems must have three operands");
77  return static_cast<transt &>(expr);
78 }
79 
82 class symbol_exprt:public exprt
83 {
84 public:
85  symbol_exprt():exprt(ID_symbol)
86  {
87  }
88 
92  explicit symbol_exprt(const irep_idt &identifier):exprt(ID_symbol)
93  {
94  set_identifier(identifier);
95  }
96 
100  explicit symbol_exprt(const typet &type):exprt(ID_symbol, type)
101  {
102  }
103 
109  const irep_idt &identifier,
110  const typet &type):exprt(ID_symbol, type)
111  {
112  set_identifier(identifier);
113  }
114 
115  void set_identifier(const irep_idt &identifier)
116  {
117  set(ID_identifier, identifier);
118  }
119 
120  const irep_idt &get_identifier() const
121  {
122  return get(ID_identifier);
123  }
124 };
125 
129 {
130 public:
132  {
133  }
134 
138  explicit decorated_symbol_exprt(const irep_idt &identifier):
139  symbol_exprt(identifier)
140  {
141  }
142 
148  {
149  }
150 
156  const irep_idt &identifier,
157  const typet &type):symbol_exprt(identifier, type)
158  {
159  }
160 
161  bool is_static_lifetime() const
162  {
163  return get_bool(ID_C_static_lifetime);
164  }
165 
167  {
168  return set(ID_C_static_lifetime, true);
169  }
170 
172  {
173  remove(ID_C_static_lifetime);
174  }
175 
176  bool is_thread_local() const
177  {
178  return get_bool(ID_C_thread_local);
179  }
180 
182  {
183  return set(ID_C_thread_local, true);
184  }
185 
187  {
188  remove(ID_C_thread_local);
189  }
190 };
191 
202 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
203 {
204  PRECONDITION(expr.id()==ID_symbol);
205  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
206  return static_cast<const symbol_exprt &>(expr);
207 }
208 
213 {
214  PRECONDITION(expr.id()==ID_symbol);
215  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
216  return static_cast<symbol_exprt &>(expr);
217 }
218 
221 class unary_exprt:public exprt
222 {
223 public:
225  {
226  operands().resize(1);
227  }
228 
229  explicit unary_exprt(const irep_idt &_id):exprt(_id)
230  {
231  operands().resize(1);
232  }
233 
235  const irep_idt &_id,
236  const exprt &_op):
237  exprt(_id, _op.type())
238  {
239  copy_to_operands(_op);
240  }
241 
243  const irep_idt &_id,
244  const typet &_type):exprt(_id, _type)
245  {
246  operands().resize(1);
247  }
248 
250  const irep_idt &_id,
251  const exprt &_op,
252  const typet &_type):
253  exprt(_id, _type)
254  {
255  copy_to_operands(_op);
256  }
257 
258  const exprt &op() const
259  {
260  return op0();
261  }
262 
264  {
265  return op0();
266  }
267 };
268 
279 inline const unary_exprt &to_unary_expr(const exprt &expr)
280 {
282  expr.operands().size()==1,
283  "Unary expressions must have one operand");
284  return static_cast<const unary_exprt &>(expr);
285 }
286 
291 {
293  expr.operands().size()==1,
294  "Unary expressions must have one operand");
295  return static_cast<unary_exprt &>(expr);
296 }
297 
300 class abs_exprt:public unary_exprt
301 {
302 public:
304  {
305  }
306 
307  explicit abs_exprt(const exprt &_op):
308  unary_exprt(ID_abs, _op, _op.type())
309  {
310  }
311 };
312 
323 inline const abs_exprt &to_abs_expr(const exprt &expr)
324 {
325  PRECONDITION(expr.id()==ID_abs);
327  expr.operands().size()==1,
328  "Absolute value must have one operand");
329  return static_cast<const abs_exprt &>(expr);
330 }
331 
336 {
337  PRECONDITION(expr.id()==ID_abs);
339  expr.operands().size()==1,
340  "Absolute value must have one operand");
341  return static_cast<abs_exprt &>(expr);
342 }
343 
347 {
348 public:
349  unary_minus_exprt():unary_exprt(ID_unary_minus)
350  {
351  }
352 
354  const exprt &_op,
355  const typet &_type):
356  unary_exprt(ID_unary_minus, _op, _type)
357  {
358  }
359 
360  explicit unary_minus_exprt(const exprt &_op):
361  unary_exprt(ID_unary_minus, _op, _op.type())
362  {
363  }
364 };
365 
376 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
377 {
378  PRECONDITION(expr.id()==ID_unary_minus);
380  expr.operands().size()==1,
381  "Unary minus must have one operand");
382  return static_cast<const unary_minus_exprt &>(expr);
383 }
384 
389 {
390  PRECONDITION(expr.id()==ID_unary_minus);
392  expr.operands().size()==1,
393  "Unary minus must have one operand");
394  return static_cast<unary_minus_exprt &>(expr);
395 }
396 
400 class predicate_exprt:public exprt
401 {
402 public:
404  {
405  }
406 
407  explicit predicate_exprt(const irep_idt &_id):
408  exprt(_id, bool_typet())
409  {
410  }
411 
413  const irep_idt &_id,
414  const exprt &_op):exprt(_id, bool_typet())
415  {
416  copy_to_operands(_op);
417  }
418 
420  const irep_idt &_id,
421  const exprt &_op0,
422  const exprt &_op1):exprt(_id, bool_typet())
423  {
424  copy_to_operands(_op0, _op1);
425  }
426 };
427 
432 {
433 public:
435  {
436  }
437 
438  explicit unary_predicate_exprt(const irep_idt &_id):
439  unary_exprt(_id, bool_typet())
440  {
441  }
442 
444  const irep_idt &_id,
445  const exprt &_op):unary_exprt(_id, _op, bool_typet())
446  {
447  }
448 
449 protected:
450  using exprt::op1; // hide
451  using exprt::op2; // hide
452 };
453 
457 {
458 public:
460  {
461  }
462 
463  explicit sign_exprt(const exprt &_op):
464  unary_predicate_exprt(ID_sign, _op)
465  {
466  }
467 };
468 
471 class binary_exprt:public exprt
472 {
473 public:
475  {
476  operands().resize(2);
477  }
478 
479  explicit binary_exprt(const irep_idt &_id):exprt(_id)
480  {
481  operands().resize(2);
482  }
483 
485  const irep_idt &_id,
486  const typet &_type):exprt(_id, _type)
487  {
488  operands().resize(2);
489  }
490 
492  const exprt &_lhs,
493  const irep_idt &_id,
494  const exprt &_rhs):
495  exprt(_id, _lhs.type())
496  {
497  copy_to_operands(_lhs, _rhs);
498  }
499 
501  const exprt &_lhs,
502  const irep_idt &_id,
503  const exprt &_rhs,
504  const typet &_type):
505  exprt(_id, _type)
506  {
507  copy_to_operands(_lhs, _rhs);
508  }
509 
510 protected:
511  using exprt::op2; // hide
512 };
513 
524 inline const binary_exprt &to_binary_expr(const exprt &expr)
525 {
527  expr.operands().size()==2,
528  "Binary expressions must have two operands");
529  return static_cast<const binary_exprt &>(expr);
530 }
531 
536 {
538  expr.operands().size()==2,
539  "Binary expressions must have two operands");
540  return static_cast<binary_exprt &>(expr);
541 }
542 
547 {
548 public:
550  {
551  }
552 
553  explicit binary_predicate_exprt(const irep_idt &_id):
554  binary_exprt(_id, bool_typet())
555  {
556  }
557 
559  const exprt &_op0,
560  const irep_idt &_id,
561  const exprt &_op1):binary_exprt(_op0, _id, _op1, bool_typet())
562  {
563  }
564 };
565 
569 {
570 public:
572  {
573  }
574 
575  explicit binary_relation_exprt(const irep_idt &id):
577  {
578  }
579 
581  const exprt &_lhs,
582  const irep_idt &_id,
583  const exprt &_rhs):
584  binary_predicate_exprt(_lhs, _id, _rhs)
585  {
586  }
587 
589  {
590  return op0();
591  }
592 
593  const exprt &lhs() const
594  {
595  return op0();
596  }
597 
599  {
600  return op1();
601  }
602 
603  const exprt &rhs() const
604  {
605  return op1();
606  }
607 };
608 
620 {
622  expr.operands().size()==2,
623  "Binary relations must have two operands");
624  return static_cast<const binary_relation_exprt &>(expr);
625 }
626 
631 {
633  expr.operands().size()==2,
634  "Binary relations must have two operands");
635  return static_cast<binary_relation_exprt &>(expr);
636 }
637 
640 class multi_ary_exprt:public exprt
641 {
642 public:
644  {
645  }
646 
647  explicit multi_ary_exprt(const irep_idt &_id):exprt(_id)
648  {
649  }
650 
652  const irep_idt &_id,
653  const typet &_type):exprt(_id, _type)
654  {
655  }
656 
658  const exprt &_lhs,
659  const irep_idt &_id,
660  const exprt &_rhs):
661  exprt(_id, _lhs.type())
662  {
663  copy_to_operands(_lhs, _rhs);
664  }
665 
667  const exprt &_lhs,
668  const irep_idt &_id,
669  const exprt &_rhs,
670  const typet &_type):
671  exprt(_id, _type)
672  {
673  copy_to_operands(_lhs, _rhs);
674  }
675 };
676 
687 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
688 {
689  return static_cast<const multi_ary_exprt &>(expr);
690 }
691 
696 {
697  return static_cast<multi_ary_exprt &>(expr);
698 }
699 
703 {
704 public:
706  {
707  }
708 
710  const exprt &_lhs,
711  const exprt &_rhs):
712  multi_ary_exprt(_lhs, ID_plus, _rhs)
713  {
714  }
715 
717  const exprt &_lhs,
718  const exprt &_rhs,
719  const typet &_type):
720  multi_ary_exprt(_lhs, ID_plus, _rhs, _type)
721  {
722  }
723 };
724 
735 inline const plus_exprt &to_plus_expr(const exprt &expr)
736 {
737  PRECONDITION(expr.id()==ID_plus);
739  expr.operands().size()>=2,
740  "Plus must have two or more operands");
741  return static_cast<const plus_exprt &>(expr);
742 }
743 
748 {
749  PRECONDITION(expr.id()==ID_plus);
751  expr.operands().size()>=2,
752  "Plus must have two or more operands");
753  return static_cast<plus_exprt &>(expr);
754 }
755 
759 {
760 public:
762  {
763  }
764 
766  const exprt &_lhs,
767  const exprt &_rhs):
768  binary_exprt(_lhs, ID_minus, _rhs)
769  {
770  }
771 };
772 
783 inline const minus_exprt &to_minus_expr(const exprt &expr)
784 {
785  PRECONDITION(expr.id()==ID_minus);
787  expr.operands().size()>=2,
788  "Minus must have two or more operands");
789  return static_cast<const minus_exprt &>(expr);
790 }
791 
796 {
797  PRECONDITION(expr.id()==ID_minus);
799  expr.operands().size()>=2,
800  "Minus must have two or more operands");
801  return static_cast<minus_exprt &>(expr);
802 }
803 
807 {
808 public:
810  {
811  }
812 
814  const exprt &_lhs,
815  const exprt &_rhs):
816  multi_ary_exprt(_lhs, ID_mult, _rhs)
817  {
818  }
819 };
820 
831 inline const mult_exprt &to_mult_expr(const exprt &expr)
832 {
833  PRECONDITION(expr.id()==ID_mult);
835  expr.operands().size()>=2,
836  "Multiply must have two or more operands");
837  return static_cast<const mult_exprt &>(expr);
838 }
839 
844 {
845  PRECONDITION(expr.id()==ID_mult);
847  expr.operands().size()>=2,
848  "Multiply must have two or more operands");
849  return static_cast<mult_exprt &>(expr);
850 }
851 
855 {
856 public:
858  {
859  }
860 
862  const exprt &_lhs,
863  const exprt &_rhs):
864  binary_exprt(_lhs, ID_div, _rhs)
865  {
866  }
867 };
868 
879 inline const div_exprt &to_div_expr(const exprt &expr)
880 {
881  PRECONDITION(expr.id()==ID_div);
883  expr.operands().size()==2,
884  "Divide must have two operands");
885  return static_cast<const div_exprt &>(expr);
886 }
887 
892 {
893  PRECONDITION(expr.id()==ID_div);
895  expr.operands().size()==2,
896  "Divide must have two operands");
897  return static_cast<div_exprt &>(expr);
898 }
899 
903 {
904 public:
906  {
907  }
908 
910  const exprt &_lhs,
911  const exprt &_rhs):
912  binary_exprt(_lhs, ID_mod, _rhs)
913  {
914  }
915 };
916 
927 inline const mod_exprt &to_mod_expr(const exprt &expr)
928 {
929  PRECONDITION(expr.id()==ID_mod);
930  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
931  return static_cast<const mod_exprt &>(expr);
932 }
933 
938 {
939  PRECONDITION(expr.id()==ID_mod);
940  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
941  return static_cast<mod_exprt &>(expr);
942 }
943 
947 {
948 public:
950  {
951  }
952 
954  const exprt &_lhs,
955  const exprt &_rhs):
956  binary_exprt(_lhs, ID_rem, _rhs)
957  {
958  }
959 };
960 
971 inline const rem_exprt &to_rem_expr(const exprt &expr)
972 {
973  PRECONDITION(expr.id()==ID_rem);
974  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
975  return static_cast<const rem_exprt &>(expr);
976 }
977 
982 {
983  PRECONDITION(expr.id()==ID_rem);
984  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
985  return static_cast<rem_exprt &>(expr);
986 }
987 
991 {
992  public:
994  {
995  }
996 
998  const exprt &_base,
999  const exprt &_exp):
1000  binary_exprt(_base, ID_power, _exp)
1001  {
1002  }
1003 };
1004 
1015 inline const power_exprt &to_power_expr(const exprt &expr)
1016 {
1017  PRECONDITION(expr.id()==ID_power);
1018  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
1019  return static_cast<const power_exprt &>(expr);
1020 }
1021 
1026 {
1027  PRECONDITION(expr.id()==ID_power);
1028  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
1029  return static_cast<power_exprt &>(expr);
1030 }
1031 
1035 {
1036  public:
1037  factorial_power_exprt():binary_exprt(ID_factorial_power)
1038  {
1039  }
1040 
1042  const exprt &_base,
1043  const exprt &_exp):
1044  binary_exprt(_base, ID_factorial_power, _exp)
1045  {
1046  }
1047 };
1048 
1060 {
1061  PRECONDITION(expr.id()==ID_factorial_power);
1063  expr.operands().size()==2,
1064  "Factorial power must have two operands");
1065  return static_cast<const factorial_power_exprt &>(expr);
1066 }
1067 
1072 {
1073  PRECONDITION(expr.id()==ID_factorial_power);
1075  expr.operands().size()==2,
1076  "Factorial power must have two operands");
1077  return static_cast<factorial_power_exprt &>(expr);
1078 }
1079 
1083 {
1084 public:
1086  {
1087  }
1088 
1089  equal_exprt(const exprt &_lhs, const exprt &_rhs):
1090  binary_relation_exprt(_lhs, ID_equal, _rhs)
1091  {
1092  }
1093 };
1094 
1105 inline const equal_exprt &to_equal_expr(const exprt &expr)
1106 {
1107  PRECONDITION(expr.id()==ID_equal);
1108  DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands");
1109  return static_cast<const equal_exprt &>(expr);
1110 }
1111 
1116 {
1117  PRECONDITION(expr.id()==ID_equal);
1118  DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands");
1119  return static_cast<equal_exprt &>(expr);
1120 }
1121 
1125 {
1126 public:
1128  {
1129  }
1130 
1131  notequal_exprt(const exprt &_lhs, const exprt &_rhs):
1132  binary_relation_exprt(_lhs, ID_notequal, _rhs)
1133  {
1134  }
1135 };
1136 
1147 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1148 {
1149  PRECONDITION(expr.id()==ID_notequal);
1151  expr.operands().size()==2,
1152  "Inequality must have two operands");
1153  return static_cast<const notequal_exprt &>(expr);
1154 }
1155 
1160 {
1161  PRECONDITION(expr.id()==ID_notequal);
1163  expr.operands().size()==2,
1164  "Inequality must have two operands");
1165  return static_cast<notequal_exprt &>(expr);
1166 }
1167 
1170 class index_exprt:public exprt
1171 {
1172 public:
1173  index_exprt():exprt(ID_index)
1174  {
1175  operands().resize(2);
1176  }
1177 
1178  explicit index_exprt(const typet &_type):exprt(ID_index, _type)
1179  {
1180  operands().resize(2);
1181  }
1182 
1183  index_exprt(const exprt &_array, const exprt &_index):
1184  exprt(ID_index, _array.type().subtype())
1185  {
1186  copy_to_operands(_array, _index);
1187  }
1188 
1190  const exprt &_array,
1191  const exprt &_index,
1192  const typet &_type):
1193  exprt(ID_index, _type)
1194  {
1195  copy_to_operands(_array, _index);
1196  }
1197 
1199  {
1200  return op0();
1201  }
1202 
1203  const exprt &array() const
1204  {
1205  return op0();
1206  }
1207 
1209  {
1210  return op1();
1211  }
1212 
1213  const exprt &index() const
1214  {
1215  return op1();
1216  }
1217 };
1218 
1229 inline const index_exprt &to_index_expr(const exprt &expr)
1230 {
1231  PRECONDITION(expr.id()==ID_index);
1233  expr.operands().size()==2,
1234  "Array index must have two operands");
1235  return static_cast<const index_exprt &>(expr);
1236 }
1237 
1242 {
1243  PRECONDITION(expr.id()==ID_index);
1245  expr.operands().size()==2,
1246  "Array index must have two operands");
1247  return static_cast<index_exprt &>(expr);
1248 }
1249 
1253 {
1254 public:
1256  {
1257  }
1258 
1259  explicit array_of_exprt(
1260  const exprt &_what, const array_typet &_type):
1261  unary_exprt(ID_array_of, _what, _type)
1262  {
1263  }
1264 
1266  {
1267  return op0();
1268  }
1269 
1270  const exprt &what() const
1271  {
1272  return op0();
1273  }
1274 };
1275 
1286 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1287 {
1288  PRECONDITION(expr.id()==ID_array_of);
1290  expr.operands().size()==1,
1291  "'Array of' must have one operand");
1292  return static_cast<const array_of_exprt &>(expr);
1293 }
1294 
1299 {
1300  PRECONDITION(expr.id()==ID_array_of);
1302  expr.operands().size()==1,
1303  "'Array of' must have one operand");
1304  return static_cast<array_of_exprt &>(expr);
1305 }
1306 
1309 class array_exprt:public exprt
1310 {
1311 public:
1312  array_exprt():exprt(ID_array)
1313  {
1314  }
1315 
1316  explicit array_exprt(const array_typet &_type):
1317  exprt(ID_array, _type)
1318  {
1319  }
1320 };
1321 
1332 inline const array_exprt &to_array_expr(const exprt &expr)
1333 {
1334  PRECONDITION(expr.id()==ID_array);
1335  return static_cast<const array_exprt &>(expr);
1336 }
1337 
1342 {
1343  PRECONDITION(expr.id()==ID_array);
1344  return static_cast<array_exprt &>(expr);
1345 }
1346 
1349 class vector_exprt:public exprt
1350 {
1351 public:
1352  vector_exprt():exprt(ID_vector)
1353  {
1354  }
1355 
1356  explicit vector_exprt(const vector_typet &_type):
1357  exprt(ID_vector, _type)
1358  {
1359  }
1360 };
1361 
1372 inline const vector_exprt &to_vector_expr(const exprt &expr)
1373 {
1374  PRECONDITION(expr.id()==ID_vector);
1375  return static_cast<const vector_exprt &>(expr);
1376 }
1377 
1382 {
1383  PRECONDITION(expr.id()==ID_vector);
1384  return static_cast<vector_exprt &>(expr);
1385 }
1386 
1390 {
1391 public:
1393  {
1394  }
1395 
1396  explicit union_exprt(const typet &_type):
1397  unary_exprt(ID_union, _type)
1398  {
1399  }
1400 
1401  explicit union_exprt(
1402  const irep_idt &_component_name,
1403  const exprt &_value,
1404  const typet &_type):
1405  unary_exprt(ID_union, _value, _type)
1406  {
1407  set_component_name(_component_name);
1408  }
1409 
1411  {
1412  return get(ID_component_name);
1413  }
1414 
1415  void set_component_name(const irep_idt &component_name)
1416  {
1417  set(ID_component_name, component_name);
1418  }
1419 
1420  std::size_t get_component_number() const
1421  {
1422  return get_size_t(ID_component_number);
1423  }
1424 
1425  void set_component_number(std::size_t component_number)
1426  {
1427  set(ID_component_number, component_number);
1428  }
1429 };
1430 
1441 inline const union_exprt &to_union_expr(const exprt &expr)
1442 {
1443  PRECONDITION(expr.id()==ID_union);
1445  expr.operands().size()==1,
1446  "Union constructor must have one operand");
1447  return static_cast<const union_exprt &>(expr);
1448 }
1449 
1454 {
1455  PRECONDITION(expr.id()==ID_union);
1457  expr.operands().size()==1,
1458  "Union constructor must have one operand");
1459  return static_cast<union_exprt &>(expr);
1460 }
1461 
1464 class struct_exprt:public exprt
1465 {
1466 public:
1467  struct_exprt():exprt(ID_struct)
1468  {
1469  }
1470 
1471  explicit struct_exprt(const typet &_type):
1472  exprt(ID_struct, _type)
1473  {
1474  }
1475 };
1476 
1487 inline const struct_exprt &to_struct_expr(const exprt &expr)
1488 {
1489  PRECONDITION(expr.id()==ID_struct);
1490  return static_cast<const struct_exprt &>(expr);
1491 }
1492 
1497 {
1498  PRECONDITION(expr.id()==ID_struct);
1499  return static_cast<struct_exprt &>(expr);
1500 }
1501 
1505 {
1506 public:
1508  {
1509  }
1510 
1511  explicit complex_exprt(const complex_typet &_type):
1512  binary_exprt(ID_complex, _type)
1513  {
1514  }
1515 
1516  explicit complex_exprt(
1517  const exprt &_real, const exprt &_imag, const complex_typet &_type):
1518  binary_exprt(_real, ID_complex, _imag, _type)
1519  {
1520  }
1521 
1523  {
1524  return op0();
1525  }
1526 
1527  const exprt &real() const
1528  {
1529  return op0();
1530  }
1531 
1533  {
1534  return op1();
1535  }
1536 
1537  const exprt &imag() const
1538  {
1539  return op1();
1540  }
1541 };
1542 
1553 inline const complex_exprt &to_complex_expr(const exprt &expr)
1554 {
1555  PRECONDITION(expr.id()==ID_complex);
1557  expr.operands().size()==2,
1558  "Complex constructor must have two operands");
1559  return static_cast<const complex_exprt &>(expr);
1560 }
1561 
1566 {
1567  PRECONDITION(expr.id()==ID_complex);
1569  expr.operands().size()==2,
1570  "Complex constructor must have two operands");
1571  return static_cast<complex_exprt &>(expr);
1572 }
1573 
1574 class namespacet;
1575 
1579 {
1580 public:
1581  object_descriptor_exprt():exprt(ID_object_descriptor)
1582  {
1583  operands().resize(2);
1584  op0().id(ID_unknown);
1585  op1().id(ID_unknown);
1586  }
1587 
1588  void build(const exprt &expr, const namespacet &ns);
1589 
1591  {
1592  return op0();
1593  }
1594 
1595  const exprt &object() const
1596  {
1597  return op0();
1598  }
1599 
1600  const exprt &root_object() const
1601  {
1602  const exprt *p=&object();
1603 
1604  while(p->id()==ID_member || p->id()==ID_index)
1605  {
1606  assert(!p->operands().empty());
1607  p=&p->op0();
1608  }
1609 
1610  return *p;
1611  }
1612 
1614  {
1615  return op1();
1616  }
1617 
1618  const exprt &offset() const
1619  {
1620  return op1();
1621  }
1622 };
1623 
1635  const exprt &expr)
1636 {
1637  PRECONDITION(expr.id()==ID_object_descriptor);
1639  expr.operands().size()==2,
1640  "Object descriptor must have two operands");
1641  return static_cast<const object_descriptor_exprt &>(expr);
1642 }
1643 
1648 {
1649  PRECONDITION(expr.id()==ID_object_descriptor);
1651  expr.operands().size()==2,
1652  "Object descriptor must have two operands");
1653  return static_cast<object_descriptor_exprt &>(expr);
1654 }
1655 
1659 {
1660 public:
1661  dynamic_object_exprt():exprt(ID_dynamic_object)
1662  {
1663  operands().resize(2);
1664  op0().id(ID_unknown);
1665  op1().id(ID_unknown);
1666  }
1667 
1668  explicit dynamic_object_exprt(const typet &type):
1669  exprt(ID_dynamic_object, type)
1670  {
1671  operands().resize(2);
1672  op0().id(ID_unknown);
1673  op1().id(ID_unknown);
1674  }
1675 
1676  void set_instance(unsigned int instance);
1677 
1678  unsigned int get_instance() const;
1679 
1681  {
1682  return op1();
1683  }
1684 
1685  const exprt &valid() const
1686  {
1687  return op1();
1688  }
1689 };
1690 
1702  const exprt &expr)
1703 {
1704  PRECONDITION(expr.id()==ID_dynamic_object);
1706  expr.operands().size()==2,
1707  "Dynamic object must have two operands");
1708  return static_cast<const dynamic_object_exprt &>(expr);
1709 }
1710 
1715 {
1716  PRECONDITION(expr.id()==ID_dynamic_object);
1718  expr.operands().size()==2,
1719  "Dynamic object must have two operands");
1720  return static_cast<dynamic_object_exprt &>(expr);
1721 }
1722 
1725 class typecast_exprt:public exprt
1726 {
1727 public:
1728  explicit typecast_exprt(const typet &_type):exprt(ID_typecast, _type)
1729  {
1730  operands().resize(1);
1731  }
1732 
1733  typecast_exprt(const exprt &op, const typet &_type):
1734  exprt(ID_typecast, _type)
1735  {
1737  }
1738 
1740  {
1741  return op0();
1742  }
1743 
1744  const exprt &op() const
1745  {
1746  return op0();
1747  }
1748 };
1749 
1760 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
1761 {
1762  PRECONDITION(expr.id()==ID_typecast);
1764  expr.operands().size()==1,
1765  "Typecast must have one operand");
1766  return static_cast<const typecast_exprt &>(expr);
1767 }
1768 
1773 {
1774  PRECONDITION(expr.id()==ID_typecast);
1776  expr.operands().size()==1,
1777  "Typecast must have one operand");
1778  return static_cast<typecast_exprt &>(expr);
1779 }
1780 
1784 {
1785 public:
1786  floatbv_typecast_exprt():binary_exprt(ID_floatbv_typecast)
1787  {
1788  }
1789 
1791  const exprt &op,
1792  const exprt &rounding,
1793  const typet &_type):binary_exprt(ID_floatbv_typecast, _type)
1794  {
1795  copy_to_operands(op, rounding);
1796  }
1797 
1799  {
1800  return op0();
1801  }
1802 
1803  const exprt &op() const
1804  {
1805  return op0();
1806  }
1807 
1809  {
1810  return op1();
1811  }
1812 
1813  const exprt &rounding_mode() const
1814  {
1815  return op1();
1816  }
1817 };
1818 
1830 {
1831  PRECONDITION(expr.id()==ID_floatbv_typecast);
1833  expr.operands().size()==2,
1834  "Float typecast must have two operands");
1835  return static_cast<const floatbv_typecast_exprt &>(expr);
1836 }
1837 
1842 {
1843  PRECONDITION(expr.id()==ID_floatbv_typecast);
1845  expr.operands().size()==2,
1846  "Float typecast must have two operands");
1847  return static_cast<floatbv_typecast_exprt &>(expr);
1848 }
1849 
1853 {
1854 public:
1856  {
1857  }
1858 
1859  and_exprt(const exprt &op0, const exprt &op1):
1860  multi_ary_exprt(op0, ID_and, op1, bool_typet())
1861  {
1862  }
1863 
1864  and_exprt(const exprt &op0, const exprt &op1, const exprt &op2):
1865  multi_ary_exprt(ID_and, bool_typet())
1866  {
1868  }
1869 
1871  const exprt &op0,
1872  const exprt &op1,
1873  const exprt &op2,
1874  const exprt &op3):
1875  multi_ary_exprt(ID_and, bool_typet())
1876  {
1877  exprt::operandst &op=operands();
1878  op.resize(4);
1879  op[0]=op0;
1880  op[1]=op1;
1881  op[2]=op2;
1882  op[3]=op3;
1883  }
1884 };
1885 
1892 
1903 inline const and_exprt &to_and_expr(const exprt &expr)
1904 {
1905  PRECONDITION(expr.id()==ID_and);
1906  // DATA_INVARIANT(
1907  // expr.operands().size()>=2,
1908  // "And must have two or more operands");
1909  return static_cast<const and_exprt &>(expr);
1910 }
1911 
1916 {
1917  PRECONDITION(expr.id()==ID_and);
1918  // DATA_INVARIANT(
1919  // expr.operands().size()>=2,
1920  // "And must have two or more operands");
1921  return static_cast<and_exprt &>(expr);
1922 }
1923 
1927 {
1928 public:
1930  {
1931  }
1932 
1933  implies_exprt(const exprt &op0, const exprt &op1):
1934  binary_exprt(op0, ID_implies, op1, bool_typet())
1935  {
1936  }
1937 };
1938 
1949 inline const implies_exprt &to_implies_expr(const exprt &expr)
1950 {
1951  PRECONDITION(expr.id()==ID_implies);
1952  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
1953  return static_cast<const implies_exprt &>(expr);
1954 }
1955 
1960 {
1961  PRECONDITION(expr.id()==ID_implies);
1962  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
1963  return static_cast<implies_exprt &>(expr);
1964 }
1965 
1969 {
1970 public:
1972  {
1973  }
1974 
1975  or_exprt(const exprt &op0, const exprt &op1):
1976  multi_ary_exprt(op0, ID_or, op1, bool_typet())
1977  {
1978  }
1979 
1980  or_exprt(const exprt &op0, const exprt &op1, const exprt &op2):
1981  multi_ary_exprt(ID_or, bool_typet())
1982  {
1984  }
1985 
1987  const exprt &op0,
1988  const exprt &op1,
1989  const exprt &op2,
1990  const exprt &op3):
1991  multi_ary_exprt(ID_or, bool_typet())
1992  {
1993  exprt::operandst &op=operands();
1994  op.resize(4);
1995  op[0]=op0;
1996  op[1]=op1;
1997  op[2]=op2;
1998  op[3]=op3;
1999  }
2000 };
2001 
2008 
2019 inline const or_exprt &to_or_expr(const exprt &expr)
2020 {
2021  PRECONDITION(expr.id()==ID_or);
2022  // DATA_INVARIANT(
2023  // expr.operands().size()>=2,
2024  // "Or must have two or more operands");
2025  return static_cast<const or_exprt &>(expr);
2026 }
2027 
2031 inline or_exprt &to_or_expr(exprt &expr)
2032 {
2033  PRECONDITION(expr.id()==ID_or);
2034  // DATA_INVARIANT(
2035  // expr.operands().size()>=2,
2036  // "Or must have two or more operands");
2037  return static_cast<or_exprt &>(expr);
2038 }
2039 
2043 {
2044 public:
2046  {
2047  }
2048 
2049  explicit bitnot_exprt(const exprt &op):
2050  unary_exprt(ID_bitnot, op)
2051  {
2052  }
2053 };
2054 
2065 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
2066 {
2067  PRECONDITION(expr.id()==ID_bitnot);
2068  // DATA_INVARIANT(expr.operands().size()==1,
2069  // "Bit-wise not must have one operand");
2070  return static_cast<const bitnot_exprt &>(expr);
2071 }
2072 
2077 {
2078  PRECONDITION(expr.id()==ID_bitnot);
2079  // DATA_INVARIANT(expr.operands().size()==1,
2080  // "Bit-wise not must have one operand");
2081  return static_cast<bitnot_exprt &>(expr);
2082 }
2083 
2084 
2088 {
2089 public:
2091  {
2092  }
2093 
2094  bitor_exprt(const exprt &_op0, const exprt &_op1):
2095  multi_ary_exprt(ID_bitor, _op0.type())
2096  {
2097  copy_to_operands(_op0, _op1);
2098  }
2099 };
2100 
2111 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
2112 {
2113  PRECONDITION(expr.id()==ID_bitor);
2114  // DATA_INVARIANT(
2115  // expr.operands().size()>=2,
2116  // "Bit-wise or must have two or more operands");
2117  return static_cast<const bitor_exprt &>(expr);
2118 }
2119 
2124 {
2125  PRECONDITION(expr.id()==ID_bitor);
2126  // DATA_INVARIANT(
2127  // expr.operands().size()>=2,
2128  // "Bit-wise or must have two or more operands");
2129  return static_cast<bitor_exprt &>(expr);
2130 }
2131 
2135 {
2136 public:
2138  {
2139  }
2140 
2141  bitxor_exprt(const exprt &_op0, const exprt &_op1):
2142  multi_ary_exprt(_op0, ID_bitxor, _op1, _op0.type())
2143  {
2144  }
2145 };
2146 
2157 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
2158 {
2159  PRECONDITION(expr.id()==ID_bitxor);
2160  // DATA_INVARIANT(
2161  // expr.operands().size()>=2,
2162  // "Bit-wise xor must have two or more operands");
2163  return static_cast<const bitxor_exprt &>(expr);
2164 }
2165 
2170 {
2171  PRECONDITION(expr.id()==ID_bitxor);
2172  // DATA_INVARIANT(
2173  // expr.operands().size()>=2,
2174  // "Bit-wise xor must have two or more operands");
2175  return static_cast<bitxor_exprt &>(expr);
2176 }
2177 
2181 {
2182 public:
2184  {
2185  }
2186 
2187  bitand_exprt(const exprt &_op0, const exprt &_op1):
2188  multi_ary_exprt(ID_bitand, _op0.type())
2189  {
2190  copy_to_operands(_op0, _op1);
2191  }
2192 };
2193 
2204 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
2205 {
2206  PRECONDITION(expr.id()==ID_bitand);
2207  // DATA_INVARIANT(
2208  // expr.operands().size()>=2,
2209  // "Bit-wise and must have two or more operands");
2210  return static_cast<const bitand_exprt &>(expr);
2211 }
2212 
2217 {
2218  PRECONDITION(expr.id()==ID_bitand);
2219  // DATA_INVARIANT(
2220  // expr.operands().size()>=2,
2221  // "Bit-wise and must have two or more operands");
2222  return static_cast<bitand_exprt &>(expr);
2223 }
2224 
2228 {
2229 public:
2230  explicit shift_exprt(const irep_idt &_id):binary_exprt(_id)
2231  {
2232  }
2233 
2234  shift_exprt(const irep_idt &_id, const typet &_type):
2235  binary_exprt(_id, _type)
2236  {
2237  }
2238 
2239  shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance):
2240  binary_exprt(_src, _id, _distance)
2241  {
2242  }
2243 
2244  shift_exprt(
2245  const exprt &_src,
2246  const irep_idt &_id,
2247  const std::size_t _distance);
2248 
2250  {
2251  return op0();
2252  }
2253 
2254  const exprt &op() const
2255  {
2256  return op0();
2257  }
2258 
2260  {
2261  return op1();
2262  }
2263 
2264  const exprt &distance() const
2265  {
2266  return op1();
2267  }
2268 };
2269 
2280 inline const shift_exprt &to_shift_expr(const exprt &expr)
2281 {
2283  expr.operands().size()==2,
2284  "Shifts must have two operands");
2285  return static_cast<const shift_exprt &>(expr);
2286 }
2287 
2292 {
2294  expr.operands().size()==2,
2295  "Shifts must have two operands");
2296  return static_cast<shift_exprt &>(expr);
2297 }
2298 
2302 {
2303 public:
2305  {
2306  }
2307 
2308  shl_exprt(const exprt &_src, const exprt &_distance):
2309  shift_exprt(_src, ID_shl, _distance)
2310  {
2311  }
2312 
2313  shl_exprt(const exprt &_src, const std::size_t _distance):
2314  shift_exprt(_src, ID_shl, _distance)
2315  {
2316  }
2317 };
2318 
2322 {
2323 public:
2325  {
2326  }
2327 
2328  ashr_exprt(const exprt &_src, const exprt &_distance):
2329  shift_exprt(_src, ID_ashr, _distance)
2330  {
2331  }
2332 
2333  ashr_exprt(const exprt &_src, const std::size_t _distance):
2334  shift_exprt(_src, ID_ashr, _distance)
2335  {
2336  }
2337 };
2338 
2342 {
2343 public:
2345  {
2346  }
2347 
2348  lshr_exprt(const exprt &_src, const exprt &_distance):
2349  shift_exprt(_src, ID_lshr, _distance)
2350  {
2351  }
2352 
2353  lshr_exprt(const exprt &_src, const std::size_t _distance):
2354  shift_exprt(_src, ID_lshr, _distance)
2355  {
2356  }
2357 };
2358 
2362 {
2363 public:
2365  {
2366  }
2367 
2368  explicit replication_exprt(const typet &_type):
2369  binary_exprt(ID_replication, _type)
2370  {
2371  }
2372 
2373  replication_exprt(const exprt &_times, const exprt &_src):
2374  binary_exprt(_times, ID_replication, _src)
2375  {
2376  }
2377 
2378  replication_exprt(const unsigned _times, const exprt &_src);
2379 
2381  {
2382  return op0();
2383  }
2384 
2385  const exprt &times() const
2386  {
2387  return op0();
2388  }
2389 
2391  {
2392  return op1();
2393  }
2394 
2395  const exprt &op() const
2396  {
2397  return op1();
2398  }
2399 };
2400 
2411 inline const replication_exprt &to_replication_expr(const exprt &expr)
2412 {
2413  PRECONDITION(expr.id()==ID_replication);
2415  expr.operands().size()==2,
2416  "Bit-wise replication must have two operands");
2417  return static_cast<const replication_exprt &>(expr);
2418 }
2419 
2424 {
2425  PRECONDITION(expr.id()==ID_replication);
2427  expr.operands().size()==2,
2428  "Bit-wise replication must have two operands");
2429  return static_cast<replication_exprt &>(expr);
2430 }
2431 
2435 {
2436 public:
2438  {
2439  }
2440 
2442  const exprt &_src,
2443  const exprt &_index):binary_predicate_exprt(_src, ID_extractbit, _index)
2444  {
2445  }
2446 
2448  const exprt &_src,
2449  const std::size_t _index);
2450 
2452  {
2453  return op0();
2454  }
2455 
2457  {
2458  return op1();
2459  }
2460 
2461  const exprt &src() const
2462  {
2463  return op0();
2464  }
2465 
2466  const exprt &index() const
2467  {
2468  return op1();
2469  }
2470 };
2471 
2482 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
2483 {
2484  PRECONDITION(expr.id()==ID_extractbit);
2486  expr.operands().size()==2,
2487  "Extract bit must have two operands");
2488  return static_cast<const extractbit_exprt &>(expr);
2489 }
2490 
2495 {
2496  PRECONDITION(expr.id()==ID_extractbit);
2498  expr.operands().size()==2,
2499  "Extract bit must have two operands");
2500  return static_cast<extractbit_exprt &>(expr);
2501 }
2502 
2506 {
2507 public:
2508  extractbits_exprt():exprt(ID_extractbits)
2509  {
2510  operands().resize(3);
2511  }
2512 
2513  // the ordering upper-lower matches the SMT-LIB
2515  const exprt &_src,
2516  const exprt &_upper,
2517  const exprt &_lower,
2518  const typet &_type):exprt(ID_extractbits, _type)
2519  {
2520  copy_to_operands(_src, _upper, _lower);
2521  }
2522 
2524  const exprt &_src,
2525  const std::size_t _upper,
2526  const std::size_t _lower,
2527  const typet &_type);
2528 
2530  {
2531  return op0();
2532  }
2533 
2535  {
2536  return op1();
2537  }
2538 
2540  {
2541  return op2();
2542  }
2543 
2544  const exprt &src() const
2545  {
2546  return op0();
2547  }
2548 
2549  const exprt &upper() const
2550  {
2551  return op1();
2552  }
2553 
2554  const exprt &lower() const
2555  {
2556  return op2();
2557  }
2558 };
2559 
2570 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
2571 {
2572  PRECONDITION(expr.id()==ID_extractbits);
2574  expr.operands().size()==3,
2575  "Extract bits must have three operands");
2576  return static_cast<const extractbits_exprt &>(expr);
2577 }
2578 
2583 {
2584  PRECONDITION(expr.id()==ID_extractbits);
2586  expr.operands().size()==3,
2587  "Extract bits must have three operands");
2588  return static_cast<extractbits_exprt &>(expr);
2589 }
2590 
2594 {
2595 public:
2596  explicit address_of_exprt(const exprt &op);
2597 
2598  address_of_exprt(const exprt &op, const pointer_typet &_type):
2599  unary_exprt(ID_address_of, op, _type)
2600  {
2601  }
2602 
2604  unary_exprt(ID_address_of, pointer_typet())
2605  {
2606  }
2607 
2609  {
2610  return op0();
2611  }
2612 
2613  const exprt &object() const
2614  {
2615  return op0();
2616  }
2617 };
2618 
2629 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
2630 {
2631  PRECONDITION(expr.id()==ID_address_of);
2632  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
2633  return static_cast<const address_of_exprt &>(expr);
2634 }
2635 
2640 {
2641  PRECONDITION(expr.id()==ID_address_of);
2642  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
2643  return static_cast<address_of_exprt &>(expr);
2644 }
2645 
2648 class not_exprt:public exprt
2649 {
2650 public:
2651  explicit not_exprt(const exprt &op):exprt(ID_not, bool_typet())
2652  {
2654  }
2655 
2657  {
2658  operands().resize(1);
2659  }
2660 
2662  {
2663  return op0();
2664  }
2665 
2666  const exprt &op() const
2667  {
2668  return op0();
2669  }
2670 };
2671 
2682 inline const not_exprt &to_not_expr(const exprt &expr)
2683 {
2684  PRECONDITION(expr.id()==ID_not);
2685  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
2686  return static_cast<const not_exprt &>(expr);
2687 }
2688 
2693 {
2694  PRECONDITION(expr.id()==ID_not);
2695  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
2696  return static_cast<not_exprt &>(expr);
2697 }
2698 
2702 {
2703 public:
2704  explicit dereference_exprt(const typet &type):
2705  exprt(ID_dereference, type)
2706  {
2707  operands().resize(1);
2708  }
2709 
2710  explicit dereference_exprt(const exprt &op):
2711  exprt(ID_dereference)
2712  {
2713  copy_to_operands(op);
2714  }
2715 
2716  dereference_exprt(const exprt &op, const typet &type):
2717  exprt(ID_dereference, type)
2718  {
2719  copy_to_operands(op);
2720  }
2721 
2722  dereference_exprt():exprt(ID_dereference)
2723  {
2724  operands().resize(1);
2725  }
2726 
2728  {
2729  return op0();
2730  }
2731 
2732  const exprt &pointer() const
2733  {
2734  return op0();
2735  }
2736 };
2737 
2748 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
2749 {
2750  PRECONDITION(expr.id()==ID_dereference);
2752  expr.operands().size()==1,
2753  "Dereference must have one operand");
2754  return static_cast<const dereference_exprt &>(expr);
2755 }
2756 
2761 {
2762  PRECONDITION(expr.id()==ID_dereference);
2764  expr.operands().size()==1,
2765  "Dereference must have one operand");
2766  return static_cast<dereference_exprt &>(expr);
2767 }
2768 
2771 class if_exprt:public exprt
2772 {
2773 public:
2774  if_exprt(const exprt &cond, const exprt &t, const exprt &f):
2775  exprt(ID_if, t.type())
2776  {
2777  copy_to_operands(cond, t, f);
2778  }
2779 
2781  const exprt &cond,
2782  const exprt &t,
2783  const exprt &f,
2784  const typet &type):
2785  exprt(ID_if, type)
2786  {
2787  copy_to_operands(cond, t, f);
2788  }
2789 
2790  if_exprt():exprt(ID_if)
2791  {
2792  operands().resize(3);
2793  }
2794 
2796  {
2797  return op0();
2798  }
2799 
2800  const exprt &cond() const
2801  {
2802  return op0();
2803  }
2804 
2806  {
2807  return op1();
2808  }
2809 
2810  const exprt &true_case() const
2811  {
2812  return op1();
2813  }
2814 
2816  {
2817  return op2();
2818  }
2819 
2820  const exprt &false_case() const
2821  {
2822  return op2();
2823  }
2824 };
2825 
2836 inline const if_exprt &to_if_expr(const exprt &expr)
2837 {
2838  PRECONDITION(expr.id()==ID_if);
2840  expr.operands().size()==3,
2841  "If-then-else must have three operands");
2842  return static_cast<const if_exprt &>(expr);
2843 }
2844 
2848 inline if_exprt &to_if_expr(exprt &expr)
2849 {
2850  PRECONDITION(expr.id()==ID_if);
2852  expr.operands().size()==3,
2853  "If-then-else must have three operands");
2854  return static_cast<if_exprt &>(expr);
2855 }
2856 
2861 class with_exprt:public exprt
2862 {
2863 public:
2865  const exprt &_old,
2866  const exprt &_where,
2867  const exprt &_new_value):
2868  exprt(ID_with, _old.type())
2869  {
2870  copy_to_operands(_old, _where, _new_value);
2871  }
2872 
2873  with_exprt():exprt(ID_with)
2874  {
2875  operands().resize(3);
2876  }
2877 
2879  {
2880  return op0();
2881  }
2882 
2883  const exprt &old() const
2884  {
2885  return op0();
2886  }
2887 
2889  {
2890  return op1();
2891  }
2892 
2893  const exprt &where() const
2894  {
2895  return op1();
2896  }
2897 
2899  {
2900  return op2();
2901  }
2902 
2903  const exprt &new_value() const
2904  {
2905  return op2();
2906  }
2907 };
2908 
2919 inline const with_exprt &to_with_expr(const exprt &expr)
2920 {
2921  PRECONDITION(expr.id()==ID_with);
2923  expr.operands().size()==3,
2924  "Array/structure update must have three operands");
2925  return static_cast<const with_exprt &>(expr);
2926 }
2927 
2932 {
2933  PRECONDITION(expr.id()==ID_with);
2935  expr.operands().size()==3,
2936  "Array/structure update must have three operands");
2937  return static_cast<with_exprt &>(expr);
2938 }
2939 
2941 {
2942 public:
2943  explicit index_designatort(const exprt &_index):
2944  exprt(ID_index_designator)
2945  {
2946  copy_to_operands(_index);
2947  }
2948 
2949  const exprt &index() const
2950  {
2951  return op0();
2952  }
2953 
2955  {
2956  return op0();
2957  }
2958 };
2959 
2970 inline const index_designatort &to_index_designator(const exprt &expr)
2971 {
2972  PRECONDITION(expr.id()==ID_index_designator);
2974  expr.operands().size()==1,
2975  "Index designator must have one operand");
2976  return static_cast<const index_designatort &>(expr);
2977 }
2978 
2983 {
2984  PRECONDITION(expr.id()==ID_index_designator);
2986  expr.operands().size()==1,
2987  "Index designator must have one operand");
2988  return static_cast<index_designatort &>(expr);
2989 }
2990 
2992 {
2993 public:
2994  explicit member_designatort(const irep_idt &_component_name):
2995  exprt(ID_member_designator)
2996  {
2997  set(ID_component_name, _component_name);
2998  }
2999 
3001  {
3002  return get(ID_component_name);
3003  }
3004 };
3005 
3017 {
3018  PRECONDITION(expr.id()==ID_member_designator);
3020  !expr.has_operands(),
3021  "Member designator must not have operands");
3022  return static_cast<const member_designatort &>(expr);
3023 }
3024 
3029 {
3030  PRECONDITION(expr.id()==ID_member_designator);
3032  !expr.has_operands(),
3033  "Member designator must not have operands");
3034  return static_cast<member_designatort &>(expr);
3035 }
3036 
3039 class update_exprt:public exprt
3040 {
3041 public:
3043  const exprt &_old,
3044  const exprt &_designator,
3045  const exprt &_new_value):
3046  exprt(ID_update, _old.type())
3047  {
3048  copy_to_operands(_old, _designator, _new_value);
3049  }
3050 
3051  explicit update_exprt(const typet &_type):
3052  exprt(ID_update, _type)
3053  {
3054  operands().resize(3);
3055  }
3056 
3057  update_exprt():exprt(ID_update)
3058  {
3059  operands().resize(3);
3060  op1().id(ID_designator);
3061  }
3062 
3064  {
3065  return op0();
3066  }
3067 
3068  const exprt &old() const
3069  {
3070  return op0();
3071  }
3072 
3073  // the designator operands are either
3074  // 1) member_designator or
3075  // 2) index_designator
3076  // as defined above
3078  {
3079  return op1().operands();
3080  }
3081 
3083  {
3084  return op1().operands();
3085  }
3086 
3088  {
3089  return op2();
3090  }
3091 
3092  const exprt &new_value() const
3093  {
3094  return op2();
3095  }
3096 };
3097 
3108 inline const update_exprt &to_update_expr(const exprt &expr)
3109 {
3110  PRECONDITION(expr.id()==ID_update);
3112  expr.operands().size()==3,
3113  "Array/structure update must have three operands");
3114  return static_cast<const update_exprt &>(expr);
3115 }
3116 
3121 {
3122  PRECONDITION(expr.id()==ID_update);
3124  expr.operands().size()==3,
3125  "Array/structure update must have three operands");
3126  return static_cast<update_exprt &>(expr);
3127 }
3128 
3129 #if 0
3130 
3132 class array_update_exprt:public exprt
3133 {
3134 public:
3135  array_update_exprt(
3136  const exprt &_array,
3137  const exprt &_index,
3138  const exprt &_new_value):
3139  exprt(ID_array_update, _array.type())
3140  {
3141  copy_to_operands(_array, _index, _new_value);
3142  }
3143 
3144  array_update_exprt():exprt(ID_array_update)
3145  {
3146  operands().resize(3);
3147  }
3148 
3149  exprt &array()
3150  {
3151  return op0();
3152  }
3153 
3154  const exprt &array() const
3155  {
3156  return op0();
3157  }
3158 
3159  exprt &index()
3160  {
3161  return op1();
3162  }
3163 
3164  const exprt &index() const
3165  {
3166  return op1();
3167  }
3168 
3169  exprt &new_value()
3170  {
3171  return op2();
3172  }
3173 
3174  const exprt &new_value() const
3175  {
3176  return op2();
3177  }
3178 };
3179 
3190 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3191 {
3192  PRECONDITION(expr.id()==ID_array_update);
3194  expr.operands().size()==3,
3195  "Array update must have three operands");
3196  return static_cast<const array_update_exprt &>(expr);
3197 }
3198 
3202 inline array_update_exprt &to_array_update_expr(exprt &expr)
3203 {
3204  PRECONDITION(expr.id()==ID_array_update);
3206  expr.operands().size()==3,
3207  "Array update must have three operands");
3208  return static_cast<array_update_exprt &>(expr);
3209 }
3210 #endif
3211 
3214 class member_exprt:public exprt
3215 {
3216 public:
3217  explicit member_exprt(const exprt &op):exprt(ID_member)
3218  {
3219  copy_to_operands(op);
3220  }
3221 
3222  explicit member_exprt(const typet &_type):exprt(ID_member, _type)
3223  {
3224  operands().resize(1);
3225  }
3226 
3227  member_exprt(const exprt &op, const irep_idt &component_name):
3228  exprt(ID_member)
3229  {
3230  copy_to_operands(op);
3231  set_component_name(component_name);
3232  }
3233 
3235  const exprt &op,
3236  const irep_idt &component_name,
3237  const typet &_type):
3238  exprt(ID_member, _type)
3239  {
3240  copy_to_operands(op);
3241  set_component_name(component_name);
3242  }
3243 
3244  member_exprt():exprt(ID_member)
3245  {
3246  operands().resize(1);
3247  }
3248 
3250  {
3251  return get(ID_component_name);
3252  }
3253 
3254  void set_component_name(const irep_idt &component_name)
3255  {
3256  set(ID_component_name, component_name);
3257  }
3258 
3259  std::size_t get_component_number() const
3260  {
3261  return get_size_t(ID_component_number);
3262  }
3263 
3264  void set_component_number(std::size_t component_number)
3265  {
3266  set(ID_component_number, component_number);
3267  }
3268 
3269  // will go away, use compound()
3270  const exprt &struct_op() const
3271  {
3272  return op0();
3273  }
3274 
3275  // will go away, use compound()
3277  {
3278  return op0();
3279  }
3280 
3281  const exprt &compound() const
3282  {
3283  return op0();
3284  }
3285 
3287  {
3288  return op0();
3289  }
3290 };
3291 
3302 inline const member_exprt &to_member_expr(const exprt &expr)
3303 {
3304  PRECONDITION(expr.id()==ID_member);
3306  expr.operands().size()==1,
3307  "Extract member must have one operand");
3308  return static_cast<const member_exprt &>(expr);
3309 }
3310 
3315 {
3316  PRECONDITION(expr.id()==ID_member);
3318  expr.operands().size()==1,
3319  "Extract member must have one operand");
3320  return static_cast<member_exprt &>(expr);
3321 }
3322 
3326 {
3327 public:
3328  explicit isnan_exprt(const exprt &op):
3329  unary_predicate_exprt(ID_isnan, op)
3330  {
3331  }
3332 
3334  {
3335  }
3336 };
3337 
3348 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
3349 {
3350  PRECONDITION(expr.id()==ID_isnan);
3351  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
3352  return static_cast<const isnan_exprt &>(expr);
3353 }
3354 
3359 {
3360  PRECONDITION(expr.id()==ID_isnan);
3361  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
3362  return static_cast<isnan_exprt &>(expr);
3363 }
3364 
3368 {
3369 public:
3370  explicit isinf_exprt(const exprt &op):
3371  unary_predicate_exprt(ID_isinf, op)
3372  {
3373  }
3374 
3376  {
3377  }
3378 };
3379 
3390 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
3391 {
3392  PRECONDITION(expr.id()==ID_isinf);
3394  expr.operands().size()==1,
3395  "Is infinite must have one operand");
3396  return static_cast<const isinf_exprt &>(expr);
3397 }
3398 
3403 {
3404  PRECONDITION(expr.id()==ID_isinf);
3406  expr.operands().size()==1,
3407  "Is infinite must have one operand");
3408  return static_cast<isinf_exprt &>(expr);
3409 }
3410 
3414 {
3415 public:
3416  explicit isfinite_exprt(const exprt &op):
3417  unary_predicate_exprt(ID_isfinite, op)
3418  {
3419  }
3420 
3422  {
3423  }
3424 };
3425 
3436 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
3437 {
3438  PRECONDITION(expr.id()==ID_isfinite);
3439  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
3440  return static_cast<const isfinite_exprt &>(expr);
3441 }
3442 
3447 {
3448  PRECONDITION(expr.id()==ID_isfinite);
3449  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
3450  return static_cast<isfinite_exprt &>(expr);
3451 }
3452 
3456 {
3457 public:
3458  explicit isnormal_exprt(const exprt &op):
3459  unary_predicate_exprt(ID_isnormal, op)
3460  {
3461  }
3462 
3464  {
3465  }
3466 };
3467 
3478 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
3479 {
3480  PRECONDITION(expr.id()==ID_isnormal);
3481  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
3482  return static_cast<const isnormal_exprt &>(expr);
3483 }
3484 
3489 {
3490  PRECONDITION(expr.id()==ID_isnormal);
3491  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
3492  return static_cast<isnormal_exprt &>(expr);
3493 }
3494 
3498 {
3499 public:
3501  {
3502  }
3503 
3504  ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs):
3505  binary_relation_exprt(_lhs, ID_ieee_float_equal, _rhs)
3506  {
3507  }
3508 };
3509 
3521 {
3522  PRECONDITION(expr.id()==ID_ieee_float_equal);
3524  expr.operands().size()==2,
3525  "IEEE equality must have two operands");
3526  return static_cast<const ieee_float_equal_exprt &>(expr);
3527 }
3528 
3533 {
3534  PRECONDITION(expr.id()==ID_ieee_float_equal);
3536  expr.operands().size()==2,
3537  "IEEE equality must have two operands");
3538  return static_cast<ieee_float_equal_exprt &>(expr);
3539 }
3540 
3544 {
3545 public:
3547  binary_relation_exprt(ID_ieee_float_notequal)
3548  {
3549  }
3550 
3551  ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs):
3552  binary_relation_exprt(_lhs, ID_ieee_float_notequal, _rhs)
3553  {
3554  }
3555 };
3556 
3568  const exprt &expr)
3569 {
3570  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3572  expr.operands().size()==2,
3573  "IEEE inequality must have two operands");
3574  return static_cast<const ieee_float_notequal_exprt &>(expr);
3575 }
3576 
3581 {
3582  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3584  expr.operands().size()==2,
3585  "IEEE inequality must have two operands");
3586  return static_cast<ieee_float_notequal_exprt &>(expr);
3587 }
3588 
3592 {
3593 public:
3595  {
3596  operands().resize(3);
3597  }
3598 
3600  const exprt &_lhs,
3601  const irep_idt &_id,
3602  const exprt &_rhs,
3603  const exprt &_rm):
3604  exprt(_id)
3605  {
3606  copy_to_operands(_lhs, _rhs, _rm);
3607  }
3608 
3610  {
3611  return op0();
3612  }
3613 
3614  const exprt &lhs() const
3615  {
3616  return op0();
3617  }
3618 
3620  {
3621  return op1();
3622  }
3623 
3624  const exprt &rhs() const
3625  {
3626  return op1();
3627  }
3628 
3630  {
3631  return op2();
3632  }
3633 
3634  const exprt &rounding_mode() const
3635  {
3636  return op2();
3637  }
3638 };
3639 
3651 {
3653  expr.operands().size()==3,
3654  "IEEE float operations must have three arguments");
3655  return static_cast<const ieee_float_op_exprt &>(expr);
3656 }
3657 
3662 {
3664  expr.operands().size()==3,
3665  "IEEE float operations must have three arguments");
3666  return static_cast<ieee_float_op_exprt &>(expr);
3667 }
3668 
3671 class type_exprt:public exprt
3672 {
3673 public:
3674  type_exprt():exprt(ID_type)
3675  {
3676  }
3677 
3678  explicit type_exprt(const typet &type):exprt(ID_type, type)
3679  {
3680  }
3681 };
3682 
3685 class constant_exprt:public exprt
3686 {
3687 public:
3688  constant_exprt():exprt(ID_constant)
3689  {
3690  }
3691 
3692  explicit constant_exprt(const typet &type):exprt(ID_constant, type)
3693  {
3694  }
3695 
3696  constant_exprt(const irep_idt &_value, const typet &_type):
3697  exprt(ID_constant, _type)
3698  {
3699  set_value(_value);
3700  }
3701 
3702  const irep_idt &get_value() const
3703  {
3704  return get(ID_value);
3705  }
3706 
3707  void set_value(const irep_idt &value)
3708  {
3709  set(ID_value, value);
3710  }
3711 
3712  bool value_is_zero_string() const;
3713 };
3714 
3725 inline const constant_exprt &to_constant_expr(const exprt &expr)
3726 {
3727  PRECONDITION(expr.id()==ID_constant);
3728  return static_cast<const constant_exprt &>(expr);
3729 }
3730 
3735 {
3736  PRECONDITION(expr.id()==ID_constant);
3737  return static_cast<constant_exprt &>(expr);
3738 }
3739 
3743 {
3744 public:
3746  {
3747  set_value(ID_true);
3748  }
3749 };
3750 
3754 {
3755 public:
3757  {
3758  set_value(ID_false);
3759  }
3760 };
3761 
3764 class nil_exprt:public exprt
3765 {
3766 public:
3767  nil_exprt():exprt(static_cast<const exprt &>(get_nil_irep()))
3768  {
3769  }
3770 };
3771 
3775 {
3776 public:
3778  {
3779  set_value(ID_NULL);
3780  }
3781 };
3782 
3786 {
3787 public:
3788  function_application_exprt():exprt(ID_function_application)
3789  {
3790  operands().resize(2);
3791  }
3792 
3793  exprt &function()
3794  {
3795  return op0();
3796  }
3797 
3798  const exprt &function() const
3799  {
3800  return op0();
3801  }
3802 
3804 
3806  {
3807  return op1().operands();
3808  }
3809 
3810  const argumentst &arguments() const
3811  {
3812  return op1().operands();
3813  }
3814 };
3815 
3827  const exprt &expr)
3828 {
3829  PRECONDITION(expr.id()==ID_function_application);
3831  expr.operands().size()==2,
3832  "Function application must have two operands");
3833  return static_cast<const function_application_exprt &>(expr);
3834 }
3835 
3840 {
3841  PRECONDITION(expr.id()==ID_function_application);
3843  expr.operands().size()==2,
3844  "Function application must have two operands");
3845  return static_cast<function_application_exprt &>(expr);
3846 }
3847 
3856 {
3857 public:
3858  concatenation_exprt():exprt(ID_concatenation)
3859  {
3860  }
3861 
3862  explicit concatenation_exprt(const typet &_type):
3863  exprt(ID_concatenation, _type)
3864  {
3865  }
3866 
3868  const exprt &_op0, const exprt &_op1, const typet &_type):
3869  exprt(ID_concatenation, _type)
3870  {
3871  copy_to_operands(_op0, _op1);
3872  }
3873 };
3874 
3886 {
3887  PRECONDITION(expr.id()==ID_concatenation);
3888  // DATA_INVARIANT(
3889  // expr.operands().size()>=2,
3890  // "Concatenation must have two or more operands");
3891  return static_cast<const concatenation_exprt &>(expr);
3892 }
3893 
3898 {
3899  PRECONDITION(expr.id()==ID_concatenation);
3900  // DATA_INVARIANT(
3901  // expr.operands().size()>=2,
3902  // "Concatenation must have two or more operands");
3903  return static_cast<concatenation_exprt &>(expr);
3904 }
3905 
3908 class infinity_exprt:public exprt
3909 {
3910 public:
3911  explicit infinity_exprt(const typet &_type):
3912  exprt(ID_infinity, _type)
3913  {
3914  }
3915 };
3916 
3919 class let_exprt:public exprt
3920 {
3921 public:
3922  let_exprt():exprt(ID_let)
3923  {
3924  operands().resize(3);
3925  op0()=symbol_exprt();
3926  }
3927 
3929  {
3930  return static_cast<symbol_exprt &>(op0());
3931  }
3932 
3933  const symbol_exprt &symbol() const
3934  {
3935  return static_cast<const symbol_exprt &>(op0());
3936  }
3937 
3939  {
3940  return op1();
3941  }
3942 
3943  const exprt &value() const
3944  {
3945  return op1();
3946  }
3947 
3949  {
3950  return op2();
3951  }
3952 
3953  const exprt &where() const
3954  {
3955  return op2();
3956  }
3957 };
3958 
3969 inline const let_exprt &to_let_expr(const exprt &expr)
3970 {
3971  PRECONDITION(expr.id()==ID_let);
3972  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
3973  return static_cast<const let_exprt &>(expr);
3974 }
3975 
3980 {
3981  PRECONDITION(expr.id()==ID_let);
3982  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
3983  return static_cast<let_exprt &>(expr);
3984 }
3985 
3988 class forall_exprt:public exprt
3989 {
3990 public:
3991  forall_exprt():exprt(ID_forall)
3992  {
3993  operands().resize(2);
3994  op0()=symbol_exprt();
3995  }
3996 
3998  {
3999  return static_cast<symbol_exprt &>(op0());
4000  }
4001 
4002  const symbol_exprt &symbol() const
4003  {
4004  return static_cast<const symbol_exprt &>(op0());
4005  }
4006 
4008  {
4009  return op1();
4010  }
4011 
4012  const exprt &where() const
4013  {
4014  return op1();
4015  }
4016 };
4017 
4020 class exists_exprt:public exprt
4021 {
4022 public:
4023  exists_exprt():exprt(ID_exists)
4024  {
4025  operands().resize(2);
4026  op0()=symbol_exprt();
4027  }
4028 
4030  {
4031  return static_cast<symbol_exprt &>(op0());
4032  }
4033 
4034  const symbol_exprt &symbol() const
4035  {
4036  return static_cast<const symbol_exprt &>(op0());
4037  }
4038 
4040  {
4041  return op1();
4042  }
4043 
4044  const exprt &where() const
4045  {
4046  return op1();
4047  }
4048 };
4049 
4050 #endif // CPROVER_UTIL_STD_EXPR_H
const abs_exprt & to_abs_expr(const exprt &expr)
Cast a generic exprt to a abs_exprt.
Definition: std_expr.h:323
const irept & get_nil_irep()
Definition: irep.cpp:56
const exprt & where() const
Definition: std_expr.h:4044
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:2919
bitnot_exprt(const exprt &op)
Definition: std_expr.h:2049
The type of an expression.
Definition: type.h:20
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:666
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
exprt & invar()
Definition: std_expr.h:40
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast a generic exprt to a isnormal_exprt.
Definition: std_expr.h:3478
Boolean negation.
Definition: std_expr.h:2648
mult_exprt()
Definition: std_expr.h:809
unary_minus_exprt(const exprt &_op, const typet &_type)
Definition: std_expr.h:353
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
Definition: std_expr.h:3826
exprt & true_case()
Definition: std_expr.h:2805
semantic type conversion
Definition: std_expr.h:1725
or_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:1975
const exprt & rhs() const
Definition: std_expr.h:3624
binary_exprt(const irep_idt &_id)
Definition: std_expr.h:479
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast a generic exprt to an extractbits_exprt.
Definition: std_expr.h:2570
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
Definition: std_expr.h:1286
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:431
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast a generic exprt to a bitor_exprt.
Definition: std_expr.h:2111
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
const exprt & value() const
Definition: std_expr.h:3943
if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
Definition: std_expr.h:2780
const exprt & lhs() const
Definition: std_expr.h:593
shift_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:2234
mod_exprt()
Definition: std_expr.h:905
const member_designatort & to_member_designator(const exprt &expr)
Cast a generic exprt to an member_designatort.
Definition: std_expr.h:3016
application of (mathematical) function
Definition: std_expr.h:3785
binary_predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:553
exprt & object()
Definition: std_expr.h:2608
index_exprt(const exprt &_array, const exprt &_index)
Definition: std_expr.h:1183
ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:3551
boolean OR
Definition: std_expr.h:1968
const symbol_exprt & symbol() const
Definition: std_expr.h:4034
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
Definition: std_expr.h:1701
exprt & op0()
Definition: expr.h:84
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:500
const exprt & src() const
Definition: std_expr.h:2461
complex_exprt(const complex_typet &_type)
Definition: std_expr.h:1511
Operator to update elements in structs and arrays.
Definition: std_expr.h:3039
const exprt & op() const
Definition: std_expr.h:258
const minus_exprt & to_minus_expr(const exprt &expr)
Cast a generic exprt to a minus_exprt.
Definition: std_expr.h:783
const exprt & pointer() const
Definition: std_expr.h:2732
Evaluates to true if the operand is infinite.
Definition: std_expr.h:3367
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast a generic exprt to a multi_ary_exprt.
Definition: std_expr.h:687
const exprt & op() const
Definition: std_expr.h:2395
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
Definition: std_expr.h:1864
unsigned int get_instance() const
Definition: std_expr.cpp:45
exprt & struct_op()
Definition: std_expr.h:3276
symbol_exprt & symbol()
Definition: std_expr.h:3997
member_exprt(const exprt &op)
Definition: std_expr.h:3217
const exprt & real() const
Definition: std_expr.h:1527
const exprt & array() const
Definition: std_expr.h:1203
unary_predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:438
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
const irep_idt & get_identifier() const
Definition: std_expr.h:120
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
Definition: std_expr.h:1980
exprt::operandst & designator()
Definition: std_expr.h:3077
exprt & lower()
Definition: std_expr.h:2539
shift_exprt(const irep_idt &_id)
Definition: std_expr.h:2230
exprt imag()
Definition: std_expr.h:1532
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Definition: std_expr.h:2280
const irep_idt & get_value() const
Definition: std_expr.h:3702
const complex_exprt & to_complex_expr(const exprt &expr)
Cast a generic exprt to a complex_exprt.
Definition: std_expr.h:1553
The null pointer constant.
Definition: std_expr.h:3774
argumentst & arguments()
Definition: std_expr.h:3805
An expression denoting a type.
Definition: std_expr.h:3671
abs_exprt(const exprt &_op)
Definition: std_expr.h:307
type_exprt(const typet &type)
Definition: std_expr.h:3678
plus_exprt(const exprt &_lhs, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:716
A transition system, consisting of state invariant, initial state predicate, and transition predicate...
Definition: std_expr.h:31
bool is_thread_local() const
Definition: std_expr.h:176
const exprt & root_object() const
Definition: std_expr.h:1600
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1487
exprt real()
Definition: std_expr.h:1522
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1105
std::size_t get_component_number() const
Definition: std_expr.h:3259
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:3455
exprt & old()
Definition: std_expr.h:2878
if_exprt()
Definition: std_expr.h:2790
exprt & new_value()
Definition: std_expr.h:2898
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
const exprt & where() const
Definition: std_expr.h:2893
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast a generic exprt to a isfinite_exprt.
Definition: std_expr.h:3436
A constant literal expression.
Definition: std_expr.h:3685
exprt & distance()
Definition: std_expr.h:2259
exprt & rounding_mode()
Definition: std_expr.h:3629
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
exprt & op()
Definition: std_expr.h:1739
const exprt & index() const
Definition: std_expr.h:1213
symbol_exprt(const typet &type)
Constructor.
Definition: std_expr.h:100
const exprt & lower() const
Definition: std_expr.h:2554
const exprt & where() const
Definition: std_expr.h:3953
irep_idt get_component_name() const
Definition: std_expr.h:3000
index_exprt(const typet &_type)
Definition: std_expr.h:1178
boolean implication
Definition: std_expr.h:1926
bool value_is_zero_string() const
Definition: std_expr.cpp:20
exponentiation
Definition: std_expr.h:990
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
Definition: std_expr.h:2482
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1425
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const exprt &_rm)
Definition: std_expr.h:3599
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
Definition: std_expr.h:1986
const exprt & where() const
Definition: std_expr.h:4012
vector_exprt(const vector_typet &_type)
Definition: std_expr.h:1356
plus_exprt()
Definition: std_expr.h:705
Extract member of struct or union.
Definition: std_expr.h:3214
const exprt & imag() const
Definition: std_expr.h:1537
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:2748
const exprt & rounding_mode() const
Definition: std_expr.h:1813
extractbits_exprt(const exprt &_src, const exprt &_upper, const exprt &_lower, const typet &_type)
Definition: std_expr.h:2514
exprt & where()
Definition: std_expr.h:3948
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
Concatenation of bit-vector operands.
Definition: std_expr.h:3855
equality
Definition: std_expr.h:1082
const exprt & op() const
Definition: std_expr.h:2254
update_exprt(const typet &_type)
Definition: std_expr.h:3051
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
constant_exprt(const irep_idt &_value, const typet &_type)
Definition: std_expr.h:3696
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3254
div_exprt()
Definition: std_expr.h:857
binary_predicate_exprt(const exprt &_op0, const irep_idt &_id, const exprt &_op1)
Definition: std_expr.h:558
exprt conjunction(const exprt::operandst &)
Definition: std_expr.cpp:50
const exprt & compound() const
Definition: std_expr.h:3281
replication_exprt(const typet &_type)
Definition: std_expr.h:2368
exprt & op()
Definition: std_expr.h:263
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:491
decorated_symbol_exprt(const irep_idt &identifier)
Constructor.
Definition: std_expr.h:138
if_exprt(const exprt &cond, const exprt &t, const exprt &f)
Definition: std_expr.h:2774
const exprt & src() const
Definition: std_expr.h:2544
const irep_idt & id() const
Definition: irep.h:189
unary_exprt(const irep_idt &_id)
Definition: std_expr.h:229
dereference_exprt(const exprt &op, const typet &type)
Definition: std_expr.h:2716
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
Definition: std_expr.h:3969
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
const exprt & times() const
Definition: std_expr.h:2385
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3325
Bit-wise OR.
Definition: std_expr.h:2087
An expression denoting infinity.
Definition: std_expr.h:3908
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance)
Definition: std_expr.h:2239
The boolean constant true.
Definition: std_expr.h:3742
member_exprt(const exprt &op, const irep_idt &component_name)
Definition: std_expr.h:3227
unary_exprt(const irep_idt &_id, const exprt &_op, const typet &_type)
Definition: std_expr.h:249
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast a generic exprt to a factorial_power_exprt.
Definition: std_expr.h:1059
Expression to hold a symbol (variable)
Definition: std_expr.h:128
division (integer and real)
Definition: std_expr.h:854
binary_relation_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:580
A generic base class for binary expressions.
Definition: std_expr.h:471
const exprt & invar() const
Definition: std_expr.h:44
decorated_symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
Definition: std_expr.h:155
exprt & init()
Definition: std_expr.h:41
exprt & old()
Definition: std_expr.h:3063
const exprt & distance() const
Definition: std_expr.h:2264
exprt & times()
Definition: std_expr.h:2380
exprt::operandst argumentst
Definition: std_expr.h:3803
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
The NIL expression.
Definition: std_expr.h:3764
const and_exprt & to_and_expr(const exprt &expr)
Cast a generic exprt to a and_exprt.
Definition: std_expr.h:1903
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:123
unary_minus_exprt(const exprt &_op)
Definition: std_expr.h:360
The pointer type.
Definition: std_types.h:1343
IEEE floating-point disequality.
Definition: std_expr.h:3543
member_exprt(const typet &_type)
Definition: std_expr.h:3222
Operator to dereference a pointer.
Definition: std_expr.h:2701
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
Definition: std_expr.h:3108
exprt & rounding_mode()
Definition: std_expr.h:1808
A constant-size array type.
Definition: std_types.h:1554
exprt & src()
Definition: std_expr.h:2529
union constructor from single element
Definition: std_expr.h:1389
std::size_t get_component_number() const
Definition: std_expr.h:1420
boolean AND
Definition: std_expr.h:1852
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2505
factorial_power_exprt(const exprt &_base, const exprt &_exp)
Definition: std_expr.h:1041
const exprt & new_value() const
Definition: std_expr.h:3092
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast a generic exprt to a factorial_power_exprt.
Definition: std_expr.h:1071
not_exprt(const exprt &op)
Definition: std_expr.h:2651
exprt & op1()
Definition: expr.h:87
const exprt & lhs() const
Definition: std_expr.h:3614
and_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:1859
binary_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:484
Generic base class for unary expressions.
Definition: std_expr.h:221
inequality
Definition: std_expr.h:1124
TO_BE_DOCUMENTED.
Definition: namespace.h:62
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:657
const exprt & op() const
Definition: std_expr.h:1744
infinity_exprt(const typet &_type)
Definition: std_expr.h:3911
Left shift.
Definition: std_expr.h:2301
const exprt & what() const
Definition: std_expr.h:1270
predicate_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:412
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:234
#define PRECONDITION(CONDITION)
Definition: invariant.h:225
const exprt & false_case() const
Definition: std_expr.h:2820
typecast_exprt(const typet &_type)
Definition: std_expr.h:1728
lshr_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2353
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1578
const exprt & cond() const
Definition: std_expr.h:2800
A forall expression.
Definition: std_expr.h:3988
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast a generic exprt to a isinf_exprt.
Definition: std_expr.h:3390
with_exprt(const exprt &_old, const exprt &_where, const exprt &_new_value)
Definition: std_expr.h:2864
The plus expression.
Definition: std_expr.h:702
exprt & where()
Definition: std_expr.h:4007
symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
Definition: std_expr.h:108
const symbol_exprt & symbol() const
Definition: std_expr.h:3933
symbol_exprt(const irep_idt &identifier)
Constructor.
Definition: std_expr.h:92
null_pointer_exprt(const pointer_typet &type)
Definition: std_expr.h:3777
ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:3504
const exprt & op() const
Definition: std_expr.h:2666
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
Definition: std_expr.h:927
predicate_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:419
void set_static_lifetime()
Definition: std_expr.h:166
rem_exprt()
Definition: std_expr.h:949
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1441
array constructor from single element
Definition: std_expr.h:1252
exprt & upper()
Definition: std_expr.h:2534
multi_ary_exprt(const irep_idt &_id)
Definition: std_expr.h:647
exprt disjunction(const exprt::operandst &)
Definition: std_expr.cpp:26
power_exprt(const exprt &_base, const exprt &_exp)
Definition: std_expr.h:997
isfinite_exprt(const exprt &op)
Definition: std_expr.h:3416
Logical right shift.
Definition: std_expr.h:2341
exprt & compound()
Definition: std_expr.h:3286
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast a generic exprt to an notequal_exprt.
Definition: std_expr.h:1147
vector constructor from list of elements
Definition: std_expr.h:1349
const exprt & old() const
Definition: std_expr.h:2883
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
Definition: std_expr.h:1332
Operator to return the address of an object.
Definition: std_expr.h:2593
The unary minus expression.
Definition: std_expr.h:346
transt()
Definition: std_expr.h:34
exprt & false_case()
Definition: std_expr.h:2815
concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
Definition: std_expr.h:3867
void set_component_number(std::size_t component_number)
Definition: std_expr.h:3264
implies_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:1933
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:407
union_exprt(const irep_idt &_component_name, const exprt &_value, const typet &_type)
Definition: std_expr.h:1401
member_exprt(const exprt &op, const irep_idt &component_name, const typet &_type)
Definition: std_expr.h:3234
bool has_operands() const
Definition: expr.h:67
const exprt & index() const
Definition: std_expr.h:2949
The boolean constant false.
Definition: std_expr.h:3753
or_exprt()
Definition: std_expr.h:1971
const binary_exprt & to_binary_expr(const exprt &expr)
Cast a generic exprt to a binary_exprt.
Definition: std_expr.h:524
const exprt & init() const
Definition: std_expr.h:45
exprt & index()
Definition: std_expr.h:2456
const exprt & rhs() const
Definition: std_expr.h:603
exprt & trans()
Definition: std_expr.h:42
decorated_symbol_exprt(const typet &type)
Constructor.
Definition: std_expr.h:146
equal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1089
const exprt & trans() const
Definition: std_expr.h:46
std::vector< exprt > operandst
Definition: expr.h:49
binary multiplication
Definition: std_expr.h:806
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
Definition: std_expr.h:1634
const exprt::operandst & designator() const
Definition: std_expr.h:3082
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
Definition: std_expr.h:2682
constant_exprt(const typet &type)
Definition: std_expr.h:3692
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_equal_exprt.
Definition: std_expr.h:3520
const index_designatort & to_index_designator(const exprt &expr)
Cast a generic exprt to an index_designatort.
Definition: std_expr.h:2970
const exprt & object() const
Definition: std_expr.h:1595
multi_ary_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:651
const symbol_exprt & symbol() const
Definition: std_expr.h:4002
minus_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:765
index_designatort(const exprt &_index)
Definition: std_expr.h:2943
exprt & op()
Definition: std_expr.h:2661
Complex numbers made of pair of given subtype.
Definition: std_types.h:1606
Bit-wise XOR.
Definition: std_expr.h:2134
dynamic_object_exprt(const typet &type)
Definition: std_expr.h:1668
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast a generic exprt to a concatenation_exprt.
Definition: std_expr.h:3885
API to type classes.
typecast_exprt(const exprt &op, const typet &_type)
Definition: std_expr.h:1733
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast a generic exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:1829
const exprt & old() const
Definition: std_expr.h:3068
const exprt & object() const
Definition: std_expr.h:2613
unary_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:242
plus_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:709
update_exprt(const exprt &_old, const exprt &_designator, const exprt &_new_value)
Definition: std_expr.h:3042
exprt & value()
Definition: std_expr.h:3938
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
Definition: std_expr.h:879
bitand_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2187
const transt & to_trans_expr(const exprt &expr)
Cast a generic exprt to a transt.
Definition: std_expr.h:59
exprt & index()
Definition: std_expr.h:1208
shl_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2308
Evaluates to true if the operand is finite.
Definition: std_expr.h:3413
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_op_exprt.
Definition: std_expr.h:3650
const exprt & index() const
Definition: std_expr.h:2466
concatenation_exprt(const typet &_type)
Definition: std_expr.h:3862
ashr_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2328
exprt & op()
Definition: std_expr.h:2249
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast a generic exprt to a isnan_exprt.
Definition: std_expr.h:3348
binary_relation_exprt(const irep_idt &id)
Definition: std_expr.h:575
semantic type conversion from/to floating-point formats
Definition: std_expr.h:1783
div_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:861
shl_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2313
Base class for all expressions.
Definition: expr.h:46
exprt & pointer()
Definition: std_expr.h:2727
absolute value
Definition: std_expr.h:300
sign of an expression
Definition: std_expr.h:456
floatbv_typecast_exprt(const exprt &op, const exprt &rounding, const typet &_type)
Definition: std_expr.h:1790
const exprt & struct_op() const
Definition: std_expr.h:3270
const exprt & rounding_mode() const
Definition: std_expr.h:3634
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
isnormal_exprt(const exprt &op)
Definition: std_expr.h:3458
const rem_exprt & to_rem_expr(const exprt &expr)
Cast a generic exprt to a rem_exprt.
Definition: std_expr.h:971
const power_exprt & to_power_expr(const exprt &expr)
Cast a generic exprt to a power_exprt.
Definition: std_expr.h:1015
dereference_exprt(const exprt &op)
Definition: std_expr.h:2710
sign_exprt()
Definition: std_expr.h:459
dereference_exprt(const typet &type)
Definition: std_expr.h:2704
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
const vector_exprt & to_vector_expr(const exprt &expr)
Cast a generic exprt to an vector_exprt.
Definition: std_expr.h:1372
const exprt & upper() const
Definition: std_expr.h:2549
sign_exprt(const exprt &_op)
Definition: std_expr.h:463
lshr_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2348
unary_predicate_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:443
irep_idt get_component_name() const
Definition: std_expr.h:3249
symbol_exprt & symbol()
Definition: std_expr.h:4029
const exprt & offset() const
Definition: std_expr.h:1618
const plus_exprt & to_plus_expr(const exprt &expr)
Cast a generic exprt to a plus_exprt.
Definition: std_expr.h:735
abs_exprt()
Definition: std_expr.h:303
rem_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:953
const mult_exprt & to_mult_expr(const exprt &expr)
Cast a generic exprt to a mult_exprt.
Definition: std_expr.h:831
remainder of division
Definition: std_expr.h:946
const exprt & valid() const
Definition: std_expr.h:1685
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast a generic exprt to a bitand_exprt.
Definition: std_expr.h:2204
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_notequal_exprt.
Definition: std_expr.h:3567
bitor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2094
const exprt & true_case() const
Definition: std_expr.h:2810
exprt & index()
Definition: std_expr.h:2954
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
array_exprt(const array_typet &_type)
Definition: std_expr.h:1316
exprt & op()
Definition: std_expr.h:2390
irep_idt get_component_name() const
Definition: std_expr.h:1410
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1415
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
Definition: std_expr.h:1870
bool is_static_lifetime() const
Definition: std_expr.h:161
isinf_exprt(const exprt &op)
Definition: std_expr.h:3370
arrays with given size
Definition: std_types.h:901
binary minus
Definition: std_expr.h:758
Bit-wise AND.
Definition: std_expr.h:2180
isnan_exprt(const exprt &op)
Definition: std_expr.h:3328
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & what()
Definition: std_expr.h:1265
exprt & op2()
Definition: expr.h:90
symbol_exprt()
Definition: std_expr.h:85
ashr_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2333
exprt & new_value()
Definition: std_expr.h:3087
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast a generic exprt to a bitxor_exprt.
Definition: std_expr.h:2157
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast a generic exprt to a binary_relation_exprt.
Definition: std_expr.h:619
const replication_exprt & to_replication_expr(const exprt &expr)
Cast a generic exprt to a replication_exprt.
Definition: std_expr.h:2411
replication_exprt(const exprt &_times, const exprt &_src)
Definition: std_expr.h:2373
symbol_exprt & symbol()
Definition: std_expr.h:3928
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:546
Arithmetic right shift.
Definition: std_expr.h:2321
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
struct_exprt(const typet &_type)
Definition: std_expr.h:1471
An exists expression.
Definition: std_expr.h:4020
exprt & where()
Definition: std_expr.h:2888
A let expression.
Definition: std_expr.h:3919
void clear_static_lifetime()
Definition: std_expr.h:171
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:252
TO_BE_DOCUMENTED.
Definition: std_expr.h:1658
A generic base class for multi-ary expressions.
Definition: std_expr.h:640
operandst & operands()
Definition: expr.h:70
mult_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:813
mod_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:909
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast a generic exprt to a bitnot_exprt.
Definition: std_expr.h:2065
exprt & src()
Definition: std_expr.h:2451
bitxor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2141
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2042
index_exprt(const exprt &_array, const exprt &_index, const typet &_type)
Definition: std_expr.h:1189
struct constructor from list of elements
Definition: std_expr.h:1464
extractbit_exprt(const exprt &_src, const exprt &_index)
Definition: std_expr.h:2441
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
falling factorial power
Definition: std_expr.h:1034
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast a generic exprt to a unary_minus_exprt.
Definition: std_expr.h:376
union_exprt(const typet &_type)
Definition: std_expr.h:1396
notequal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1131
complex_exprt(const exprt &_real, const exprt &_imag, const complex_typet &_type)
Definition: std_expr.h:1516
IEEE floating-point operations.
Definition: std_expr.h:3591
Bit-vector replication.
Definition: std_expr.h:2361
exprt & array()
Definition: std_expr.h:1198
A base class for shift operators.
Definition: std_expr.h:2227
const argumentst & arguments() const
Definition: std_expr.h:3810
array constructor from list of elements
Definition: std_expr.h:1309
exprt & where()
Definition: std_expr.h:4039
complex constructor from a pair of numbers
Definition: std_expr.h:1504
binary modulo
Definition: std_expr.h:902
const implies_exprt & to_implies_expr(const exprt &expr)
Cast a generic exprt to a implies_exprt.
Definition: std_expr.h:1949
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:2994
array_of_exprt(const exprt &_what, const array_typet &_type)
Definition: std_expr.h:1259
const or_exprt & to_or_expr(const exprt &expr)
Cast a generic exprt to a or_exprt.
Definition: std_expr.h:2019
const unary_exprt & to_unary_expr(const exprt &expr)
Cast a generic exprt to a unary_exprt.
Definition: std_expr.h:279
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2434
A generic base class for expressions that are predicates, i.e., boolean-typed.
Definition: std_expr.h:400
IEEE-floating-point equality.
Definition: std_expr.h:3497
array index operator
Definition: std_expr.h:1170
exprt & op3()
Definition: expr.h:93
address_of_exprt(const exprt &op, const pointer_typet &_type)
Definition: std_expr.h:2598
const exprt & new_value() const
Definition: std_expr.h:2903
const exprt & op() const
Definition: std_expr.h:1803