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 #include "expr_cast.h"
23 
24 
29 class transt:public exprt
30 {
31 public:
33  {
34  id(ID_trans);
35  operands().resize(3);
36  }
37 
38  exprt &invar() { return op0(); }
39  exprt &init() { return op1(); }
40  exprt &trans() { return op2(); }
41 
42  const exprt &invar() const { return op0(); }
43  const exprt &init() const { return op1(); }
44  const exprt &trans() const { return op2(); }
45 };
46 
57 inline const transt &to_trans_expr(const exprt &expr)
58 {
59  PRECONDITION(expr.id()==ID_trans);
61  expr.operands().size()==3,
62  "Transition systems must have three operands");
63  return static_cast<const transt &>(expr);
64 }
65 
69 inline transt &to_trans_expr(exprt &expr)
70 {
71  PRECONDITION(expr.id()==ID_trans);
73  expr.operands().size()==3,
74  "Transition systems must have three operands");
75  return static_cast<transt &>(expr);
76 }
77 
78 template<> inline bool can_cast_expr<transt>(const exprt &base)
79 {
80  return base.id()==ID_trans;
81 }
82 inline void validate_expr(const transt &value)
83 {
84  validate_operands(value, 3, "Transition systems must have three operands");
85 }
86 
87 
90 class symbol_exprt:public exprt
91 {
92 public:
93  symbol_exprt():exprt(ID_symbol)
94  {
95  }
96 
100  explicit symbol_exprt(const irep_idt &identifier):exprt(ID_symbol)
101  {
102  set_identifier(identifier);
103  }
104 
108  explicit symbol_exprt(const typet &type):exprt(ID_symbol, type)
109  {
110  }
111 
117  const irep_idt &identifier,
118  const typet &type):exprt(ID_symbol, type)
119  {
120  set_identifier(identifier);
121  }
122 
123  void set_identifier(const irep_idt &identifier)
124  {
125  set(ID_identifier, identifier);
126  }
127 
128  const irep_idt &get_identifier() const
129  {
130  return get(ID_identifier);
131  }
132 };
133 
137 {
138 public:
140  {
141  }
142 
146  explicit decorated_symbol_exprt(const irep_idt &identifier):
147  symbol_exprt(identifier)
148  {
149  }
150 
156  {
157  }
158 
164  const irep_idt &identifier,
165  const typet &type):symbol_exprt(identifier, type)
166  {
167  }
168 
169  bool is_static_lifetime() const
170  {
171  return get_bool(ID_C_static_lifetime);
172  }
173 
175  {
176  return set(ID_C_static_lifetime, true);
177  }
178 
180  {
181  remove(ID_C_static_lifetime);
182  }
183 
184  bool is_thread_local() const
185  {
186  return get_bool(ID_C_thread_local);
187  }
188 
190  {
191  return set(ID_C_thread_local, true);
192  }
193 
195  {
196  remove(ID_C_thread_local);
197  }
198 };
199 
210 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
211 {
212  PRECONDITION(expr.id()==ID_symbol);
213  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
214  return static_cast<const symbol_exprt &>(expr);
215 }
216 
221 {
222  PRECONDITION(expr.id()==ID_symbol);
223  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
224  return static_cast<symbol_exprt &>(expr);
225 }
226 
227 template<> inline bool can_cast_expr<symbol_exprt>(const exprt &base)
228 {
229  return base.id()==ID_symbol;
230 }
231 inline void validate_expr(const symbol_exprt &value)
232 {
233  validate_operands(value, 0, "Symbols must not have operands");
234 }
235 
236 
240 {
241 public:
247  const irep_idt &identifier,
248  const typet &type):exprt(ID_nondet_symbol, type)
249  {
250  set_identifier(identifier);
251  }
252 
253  void set_identifier(const irep_idt &identifier)
254  {
255  set(ID_identifier, identifier);
256  }
257 
258  const irep_idt &get_identifier() const
259  {
260  return get(ID_identifier);
261  }
262 };
263 
275 {
276  PRECONDITION(expr.id()==ID_nondet_symbol);
277  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
278  return static_cast<const nondet_symbol_exprt &>(expr);
279 }
280 
285 {
286  PRECONDITION(expr.id()==ID_symbol);
287  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
288  return static_cast<nondet_symbol_exprt &>(expr);
289 }
290 
291 template<> inline bool can_cast_expr<nondet_symbol_exprt>(const exprt &base)
292 {
293  return base.id()==ID_nondet_symbol;
294 }
295 inline void validate_expr(const nondet_symbol_exprt &value)
296 {
297  validate_operands(value, 0, "Symbols must not have operands");
298 }
299 
300 
303 class unary_exprt:public exprt
304 {
305 public:
307  {
308  operands().resize(1);
309  }
310 
311  explicit unary_exprt(const irep_idt &_id):exprt(_id)
312  {
313  operands().resize(1);
314  }
315 
317  const irep_idt &_id,
318  const exprt &_op):
319  exprt(_id, _op.type())
320  {
321  copy_to_operands(_op);
322  }
323 
325  const irep_idt &_id,
326  const typet &_type):exprt(_id, _type)
327  {
328  operands().resize(1);
329  }
330 
332  const irep_idt &_id,
333  const exprt &_op,
334  const typet &_type):
335  exprt(_id, _type)
336  {
337  copy_to_operands(_op);
338  }
339 
340  const exprt &op() const
341  {
342  return op0();
343  }
344 
346  {
347  return op0();
348  }
349 };
350 
361 inline const unary_exprt &to_unary_expr(const exprt &expr)
362 {
364  expr.operands().size()==1,
365  "Unary expressions must have one operand");
366  return static_cast<const unary_exprt &>(expr);
367 }
368 
373 {
375  expr.operands().size()==1,
376  "Unary expressions must have one operand");
377  return static_cast<unary_exprt &>(expr);
378 }
379 
380 template<> inline bool can_cast_expr<unary_exprt>(const exprt &base)
381 {
382  return base.operands().size()==1;
383 }
384 
385 
388 class abs_exprt:public unary_exprt
389 {
390 public:
392  {
393  }
394 
395  explicit abs_exprt(const exprt &_op):
396  unary_exprt(ID_abs, _op, _op.type())
397  {
398  }
399 };
400 
411 inline const abs_exprt &to_abs_expr(const exprt &expr)
412 {
413  PRECONDITION(expr.id()==ID_abs);
415  expr.operands().size()==1,
416  "Absolute value must have one operand");
417  return static_cast<const abs_exprt &>(expr);
418 }
419 
424 {
425  PRECONDITION(expr.id()==ID_abs);
427  expr.operands().size()==1,
428  "Absolute value must have one operand");
429  return static_cast<abs_exprt &>(expr);
430 }
431 
432 template<> inline bool can_cast_expr<abs_exprt>(const exprt &base)
433 {
434  return base.id()==ID_abs;
435 }
436 inline void validate_expr(const abs_exprt &value)
437 {
438  validate_operands(value, 1, "Absolute value must have one operand");
439 }
440 
441 
445 {
446 public:
447  unary_minus_exprt():unary_exprt(ID_unary_minus)
448  {
449  }
450 
452  const exprt &_op,
453  const typet &_type):
454  unary_exprt(ID_unary_minus, _op, _type)
455  {
456  }
457 
458  explicit unary_minus_exprt(const exprt &_op):
459  unary_exprt(ID_unary_minus, _op, _op.type())
460  {
461  }
462 };
463 
474 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
475 {
476  PRECONDITION(expr.id()==ID_unary_minus);
478  expr.operands().size()==1,
479  "Unary minus must have one operand");
480  return static_cast<const unary_minus_exprt &>(expr);
481 }
482 
487 {
488  PRECONDITION(expr.id()==ID_unary_minus);
490  expr.operands().size()==1,
491  "Unary minus must have one operand");
492  return static_cast<unary_minus_exprt &>(expr);
493 }
494 
495 template<> inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
496 {
497  return base.id()==ID_unary_minus;
498 }
499 inline void validate_expr(const unary_minus_exprt &value)
500 {
501  validate_operands(value, 1, "Unary minus must have one operand");
502 }
503 
507 {
508 public:
509  bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
510  : unary_exprt(ID_bswap, _op, _type)
511  {
512  set_bits_per_byte(bits_per_byte);
513  }
514 
515  bswap_exprt(const exprt &_op, std::size_t bits_per_byte)
516  : unary_exprt(ID_bswap, _op, _op.type())
517  {
518  set_bits_per_byte(bits_per_byte);
519  }
520 
521  std::size_t get_bits_per_byte() const
522  {
523  return get_size_t(ID_bits_per_byte);
524  }
525 
526  void set_bits_per_byte(std::size_t bits_per_byte)
527  {
528  set(ID_bits_per_byte, bits_per_byte);
529  }
530 };
531 
542 inline const bswap_exprt &to_bswap_expr(const exprt &expr)
543 {
544  PRECONDITION(expr.id() == ID_bswap);
545  DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand");
547  expr.op0().type() == expr.type(), "bswap type must match operand type");
548  return static_cast<const bswap_exprt &>(expr);
549 }
550 
555 {
556  PRECONDITION(expr.id() == ID_bswap);
557  DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand");
559  expr.op0().type() == expr.type(), "bswap type must match operand type");
560  return static_cast<bswap_exprt &>(expr);
561 }
562 
563 template <>
564 inline bool can_cast_expr<bswap_exprt>(const exprt &base)
565 {
566  return base.id() == ID_bswap;
567 }
568 inline void validate_expr(const bswap_exprt &value)
569 {
570  validate_operands(value, 1, "bswap must have one operand");
572  value.op().type() == value.type(), "bswap type must match operand type");
573 }
574 
578 class predicate_exprt:public exprt
579 {
580 public:
582  {
583  }
584 
585  explicit predicate_exprt(const irep_idt &_id):
586  exprt(_id, bool_typet())
587  {
588  }
589 
591  const irep_idt &_id,
592  const exprt &_op):exprt(_id, bool_typet())
593  {
594  copy_to_operands(_op);
595  }
596 
598  const irep_idt &_id,
599  const exprt &_op0,
600  const exprt &_op1):exprt(_id, bool_typet())
601  {
602  copy_to_operands(_op0, _op1);
603  }
604 };
605 
610 {
611 public:
613  {
614  }
615 
616  explicit unary_predicate_exprt(const irep_idt &_id):
617  unary_exprt(_id, bool_typet())
618  {
619  }
620 
622  const irep_idt &_id,
623  const exprt &_op):unary_exprt(_id, _op, bool_typet())
624  {
625  }
626 
627 protected:
628  using exprt::op1; // hide
629  using exprt::op2; // hide
630 };
631 
635 {
636 public:
638  {
639  }
640 
641  explicit sign_exprt(const exprt &_op):
642  unary_predicate_exprt(ID_sign, _op)
643  {
644  }
645 };
646 
649 class binary_exprt:public exprt
650 {
651 public:
653  {
654  operands().resize(2);
655  }
656 
657  explicit binary_exprt(const irep_idt &_id):exprt(_id)
658  {
659  operands().resize(2);
660  }
661 
663  const irep_idt &_id,
664  const typet &_type):exprt(_id, _type)
665  {
666  operands().resize(2);
667  }
668 
670  const exprt &_lhs,
671  const irep_idt &_id,
672  const exprt &_rhs):
673  exprt(_id, _lhs.type())
674  {
675  copy_to_operands(_lhs, _rhs);
676  }
677 
679  const exprt &_lhs,
680  const irep_idt &_id,
681  const exprt &_rhs,
682  const typet &_type):
683  exprt(_id, _type)
684  {
685  copy_to_operands(_lhs, _rhs);
686  }
687 
688 protected:
689  using exprt::op2; // hide
690 };
691 
702 inline const binary_exprt &to_binary_expr(const exprt &expr)
703 {
705  expr.operands().size()==2,
706  "Binary expressions must have two operands");
707  return static_cast<const binary_exprt &>(expr);
708 }
709 
714 {
716  expr.operands().size()==2,
717  "Binary expressions must have two operands");
718  return static_cast<binary_exprt &>(expr);
719 }
720 
721 template<> inline bool can_cast_expr<binary_exprt>(const exprt &base)
722 {
723  return base.operands().size()==2;
724 }
725 
726 
731 {
732 public:
734  {
735  }
736 
737  explicit binary_predicate_exprt(const irep_idt &_id):
738  binary_exprt(_id, bool_typet())
739  {
740  }
741 
743  const exprt &_op0,
744  const irep_idt &_id,
745  const exprt &_op1):binary_exprt(_op0, _id, _op1, bool_typet())
746  {
747  }
748 };
749 
753 {
754 public:
756  {
757  }
758 
759  explicit binary_relation_exprt(const irep_idt &id):
761  {
762  }
763 
765  const exprt &_lhs,
766  const irep_idt &_id,
767  const exprt &_rhs):
768  binary_predicate_exprt(_lhs, _id, _rhs)
769  {
770  }
771 
773  {
774  return op0();
775  }
776 
777  const exprt &lhs() const
778  {
779  return op0();
780  }
781 
783  {
784  return op1();
785  }
786 
787  const exprt &rhs() const
788  {
789  return op1();
790  }
791 };
792 
804 {
806  expr.operands().size()==2,
807  "Binary relations must have two operands");
808  return static_cast<const binary_relation_exprt &>(expr);
809 }
810 
815 {
817  expr.operands().size()==2,
818  "Binary relations must have two operands");
819  return static_cast<binary_relation_exprt &>(expr);
820 }
821 
822 template<> inline bool can_cast_expr<binary_relation_exprt>(const exprt &base)
823 {
824  return can_cast_expr<binary_exprt>(base);
825 }
826 
827 
830 class multi_ary_exprt:public exprt
831 {
832 public:
834  {
835  }
836 
837  explicit multi_ary_exprt(const irep_idt &_id):exprt(_id)
838  {
839  }
840 
842  const irep_idt &_id,
843  const typet &_type):exprt(_id, _type)
844  {
845  }
846 
848  const exprt &_lhs,
849  const irep_idt &_id,
850  const exprt &_rhs):
851  exprt(_id, _lhs.type())
852  {
853  copy_to_operands(_lhs, _rhs);
854  }
855 
857  const exprt &_lhs,
858  const irep_idt &_id,
859  const exprt &_rhs,
860  const typet &_type):
861  exprt(_id, _type)
862  {
863  copy_to_operands(_lhs, _rhs);
864  }
865 };
866 
877 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
878 {
879  return static_cast<const multi_ary_exprt &>(expr);
880 }
881 
886 {
887  return static_cast<multi_ary_exprt &>(expr);
888 }
889 
890 
894 {
895 public:
897  {
898  }
899 
901  const exprt &_lhs,
902  const exprt &_rhs):
903  multi_ary_exprt(_lhs, ID_plus, _rhs)
904  {
905  }
906 
908  const exprt &_lhs,
909  const exprt &_rhs,
910  const typet &_type):
911  multi_ary_exprt(_lhs, ID_plus, _rhs, _type)
912  {
913  }
914 };
915 
926 inline const plus_exprt &to_plus_expr(const exprt &expr)
927 {
928  PRECONDITION(expr.id()==ID_plus);
930  expr.operands().size()>=2,
931  "Plus must have two or more operands");
932  return static_cast<const plus_exprt &>(expr);
933 }
934 
939 {
940  PRECONDITION(expr.id()==ID_plus);
942  expr.operands().size()>=2,
943  "Plus must have two or more operands");
944  return static_cast<plus_exprt &>(expr);
945 }
946 
947 template<> inline bool can_cast_expr<plus_exprt>(const exprt &base)
948 {
949  return base.id()==ID_plus;
950 }
951 inline void validate_expr(const plus_exprt &value)
952 {
953  validate_operands(value, 2, "Plus must have two or more operands", true);
954 }
955 
956 
960 {
961 public:
963  {
964  }
965 
967  const exprt &_lhs,
968  const exprt &_rhs):
969  binary_exprt(_lhs, ID_minus, _rhs)
970  {
971  }
972 };
973 
984 inline const minus_exprt &to_minus_expr(const exprt &expr)
985 {
986  PRECONDITION(expr.id()==ID_minus);
988  expr.operands().size()>=2,
989  "Minus must have two or more operands");
990  return static_cast<const minus_exprt &>(expr);
991 }
992 
997 {
998  PRECONDITION(expr.id()==ID_minus);
1000  expr.operands().size()>=2,
1001  "Minus must have two or more operands");
1002  return static_cast<minus_exprt &>(expr);
1003 }
1004 
1005 template<> inline bool can_cast_expr<minus_exprt>(const exprt &base)
1006 {
1007  return base.id()==ID_minus;
1008 }
1009 inline void validate_expr(const minus_exprt &value)
1010 {
1011  validate_operands(value, 2, "Minus must have two or more operands", true);
1012 }
1013 
1014 
1018 {
1019 public:
1021  {
1022  }
1023 
1025  const exprt &_lhs,
1026  const exprt &_rhs):
1027  multi_ary_exprt(_lhs, ID_mult, _rhs)
1028  {
1029  }
1030 };
1031 
1042 inline const mult_exprt &to_mult_expr(const exprt &expr)
1043 {
1044  PRECONDITION(expr.id()==ID_mult);
1046  expr.operands().size()>=2,
1047  "Multiply must have two or more operands");
1048  return static_cast<const mult_exprt &>(expr);
1049 }
1050 
1055 {
1056  PRECONDITION(expr.id()==ID_mult);
1058  expr.operands().size()>=2,
1059  "Multiply must have two or more operands");
1060  return static_cast<mult_exprt &>(expr);
1061 }
1062 
1063 template<> inline bool can_cast_expr<mult_exprt>(const exprt &base)
1064 {
1065  return base.id()==ID_mult;
1066 }
1067 inline void validate_expr(const mult_exprt &value)
1068 {
1069  validate_operands(value, 2, "Multiply must have two or more operands", true);
1070 }
1071 
1072 
1076 {
1077 public:
1079  {
1080  }
1081 
1083  const exprt &_lhs,
1084  const exprt &_rhs):
1085  binary_exprt(_lhs, ID_div, _rhs)
1086  {
1087  }
1088 };
1089 
1100 inline const div_exprt &to_div_expr(const exprt &expr)
1101 {
1102  PRECONDITION(expr.id()==ID_div);
1104  expr.operands().size()==2,
1105  "Divide must have two operands");
1106  return static_cast<const div_exprt &>(expr);
1107 }
1108 
1113 {
1114  PRECONDITION(expr.id()==ID_div);
1116  expr.operands().size()==2,
1117  "Divide must have two operands");
1118  return static_cast<div_exprt &>(expr);
1119 }
1120 
1121 template<> inline bool can_cast_expr<div_exprt>(const exprt &base)
1122 {
1123  return base.id()==ID_div;
1124 }
1125 inline void validate_expr(const div_exprt &value)
1126 {
1127  validate_operands(value, 2, "Divide must have two operands");
1128 }
1129 
1130 
1134 {
1135 public:
1137  {
1138  }
1139 
1141  const exprt &_lhs,
1142  const exprt &_rhs):
1143  binary_exprt(_lhs, ID_mod, _rhs)
1144  {
1145  }
1146 };
1147 
1158 inline const mod_exprt &to_mod_expr(const exprt &expr)
1159 {
1160  PRECONDITION(expr.id()==ID_mod);
1161  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
1162  return static_cast<const mod_exprt &>(expr);
1163 }
1164 
1169 {
1170  PRECONDITION(expr.id()==ID_mod);
1171  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
1172  return static_cast<mod_exprt &>(expr);
1173 }
1174 
1175 template<> inline bool can_cast_expr<mod_exprt>(const exprt &base)
1176 {
1177  return base.id()==ID_mod;
1178 }
1179 inline void validate_expr(const mod_exprt &value)
1180 {
1181  validate_operands(value, 2, "Modulo must have two operands");
1182 }
1183 
1184 
1188 {
1189 public:
1191  {
1192  }
1193 
1195  const exprt &_lhs,
1196  const exprt &_rhs):
1197  binary_exprt(_lhs, ID_rem, _rhs)
1198  {
1199  }
1200 };
1201 
1212 inline const rem_exprt &to_rem_expr(const exprt &expr)
1213 {
1214  PRECONDITION(expr.id()==ID_rem);
1215  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
1216  return static_cast<const rem_exprt &>(expr);
1217 }
1218 
1223 {
1224  PRECONDITION(expr.id()==ID_rem);
1225  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
1226  return static_cast<rem_exprt &>(expr);
1227 }
1228 
1229 template<> inline bool can_cast_expr<rem_exprt>(const exprt &base)
1230 {
1231  return base.id()==ID_rem;
1232 }
1233 inline void validate_expr(const rem_exprt &value)
1234 {
1235  validate_operands(value, 2, "Remainder must have two operands");
1236 }
1237 
1238 
1242 {
1243  public:
1245  {
1246  }
1247 
1249  const exprt &_base,
1250  const exprt &_exp):
1251  binary_exprt(_base, ID_power, _exp)
1252  {
1253  }
1254 };
1255 
1266 inline const power_exprt &to_power_expr(const exprt &expr)
1267 {
1268  PRECONDITION(expr.id()==ID_power);
1269  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
1270  return static_cast<const power_exprt &>(expr);
1271 }
1272 
1277 {
1278  PRECONDITION(expr.id()==ID_power);
1279  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
1280  return static_cast<power_exprt &>(expr);
1281 }
1282 
1283 template<> inline bool can_cast_expr<power_exprt>(const exprt &base)
1284 {
1285  return base.id()==ID_power;
1286 }
1287 inline void validate_expr(const power_exprt &value)
1288 {
1289  validate_operands(value, 2, "Power must have two operands");
1290 }
1291 
1292 
1296 {
1297  public:
1298  factorial_power_exprt():binary_exprt(ID_factorial_power)
1299  {
1300  }
1301 
1303  const exprt &_base,
1304  const exprt &_exp):
1305  binary_exprt(_base, ID_factorial_power, _exp)
1306  {
1307  }
1308 };
1309 
1321 {
1322  PRECONDITION(expr.id()==ID_factorial_power);
1324  expr.operands().size()==2,
1325  "Factorial power must have two operands");
1326  return static_cast<const factorial_power_exprt &>(expr);
1327 }
1328 
1333 {
1334  PRECONDITION(expr.id()==ID_factorial_power);
1336  expr.operands().size()==2,
1337  "Factorial power must have two operands");
1338  return static_cast<factorial_power_exprt &>(expr);
1339 }
1340 
1342  const exprt &base)
1343 {
1344  return base.id()==ID_factorial_power;
1345 }
1346 inline void validate_expr(const factorial_power_exprt &value)
1347 {
1348  validate_operands(value, 2, "Factorial power must have two operands");
1349 }
1350 
1351 
1355 {
1356 public:
1358  {
1359  }
1360 
1361  equal_exprt(const exprt &_lhs, const exprt &_rhs):
1362  binary_relation_exprt(_lhs, ID_equal, _rhs)
1363  {
1364  }
1365 };
1366 
1377 inline const equal_exprt &to_equal_expr(const exprt &expr)
1378 {
1379  PRECONDITION(expr.id()==ID_equal);
1380  DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands");
1381  return static_cast<const equal_exprt &>(expr);
1382 }
1383 
1388 {
1389  PRECONDITION(expr.id()==ID_equal);
1390  DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands");
1391  return static_cast<equal_exprt &>(expr);
1392 }
1393 
1394 template<> inline bool can_cast_expr<equal_exprt>(const exprt &base)
1395 {
1396  return base.id()==ID_equal;
1397 }
1398 inline void validate_expr(const equal_exprt &value)
1399 {
1400  validate_operands(value, 2, "Equality must have two operands");
1401 }
1402 
1403 
1407 {
1408 public:
1410  {
1411  }
1412 
1413  notequal_exprt(const exprt &_lhs, const exprt &_rhs):
1414  binary_relation_exprt(_lhs, ID_notequal, _rhs)
1415  {
1416  }
1417 };
1418 
1429 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1430 {
1431  PRECONDITION(expr.id()==ID_notequal);
1433  expr.operands().size()==2,
1434  "Inequality must have two operands");
1435  return static_cast<const notequal_exprt &>(expr);
1436 }
1437 
1442 {
1443  PRECONDITION(expr.id()==ID_notequal);
1445  expr.operands().size()==2,
1446  "Inequality must have two operands");
1447  return static_cast<notequal_exprt &>(expr);
1448 }
1449 
1450 template<> inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1451 {
1452  return base.id()==ID_notequal;
1453 }
1454 inline void validate_expr(const notequal_exprt &value)
1455 {
1456  validate_operands(value, 2, "Inequality must have two operands");
1457 }
1458 
1459 
1463 {
1464 public:
1466  {
1467  }
1468 
1469  explicit index_exprt(const typet &_type):binary_exprt(ID_index, _type)
1470  {
1471  }
1472 
1473  index_exprt(const exprt &_array, const exprt &_index):
1474  binary_exprt(_array, ID_index, _index, _array.type().subtype())
1475  {
1476  }
1477 
1479  const exprt &_array,
1480  const exprt &_index,
1481  const typet &_type):
1482  binary_exprt(_array, ID_index, _index, _type)
1483  {
1484  }
1485 
1487  {
1488  return op0();
1489  }
1490 
1491  const exprt &array() const
1492  {
1493  return op0();
1494  }
1495 
1497  {
1498  return op1();
1499  }
1500 
1501  const exprt &index() const
1502  {
1503  return op1();
1504  }
1505 };
1506 
1517 inline const index_exprt &to_index_expr(const exprt &expr)
1518 {
1519  PRECONDITION(expr.id()==ID_index);
1521  expr.operands().size()==2,
1522  "Array index must have two operands");
1523  return static_cast<const index_exprt &>(expr);
1524 }
1525 
1530 {
1531  PRECONDITION(expr.id()==ID_index);
1533  expr.operands().size()==2,
1534  "Array index must have two operands");
1535  return static_cast<index_exprt &>(expr);
1536 }
1537 
1538 template<> inline bool can_cast_expr<index_exprt>(const exprt &base)
1539 {
1540  return base.id()==ID_index;
1541 }
1542 inline void validate_expr(const index_exprt &value)
1543 {
1544  validate_operands(value, 2, "Array index must have two operands");
1545 }
1546 
1547 
1551 {
1552 public:
1554  {
1555  }
1556 
1557  explicit array_of_exprt(
1558  const exprt &_what, const array_typet &_type):
1559  unary_exprt(ID_array_of, _what, _type)
1560  {
1561  }
1562 
1564  {
1565  return op0();
1566  }
1567 
1568  const exprt &what() const
1569  {
1570  return op0();
1571  }
1572 };
1573 
1584 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1585 {
1586  PRECONDITION(expr.id()==ID_array_of);
1588  expr.operands().size()==1,
1589  "'Array of' must have one operand");
1590  return static_cast<const array_of_exprt &>(expr);
1591 }
1592 
1597 {
1598  PRECONDITION(expr.id()==ID_array_of);
1600  expr.operands().size()==1,
1601  "'Array of' must have one operand");
1602  return static_cast<array_of_exprt &>(expr);
1603 }
1604 
1605 template<> inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1606 {
1607  return base.id()==ID_array_of;
1608 }
1609 inline void validate_expr(const array_of_exprt &value)
1610 {
1611  validate_operands(value, 1, "'Array of' must have one operand");
1612 }
1613 
1614 
1617 class array_exprt:public exprt
1618 {
1619 public:
1620  array_exprt():exprt(ID_array)
1621  {
1622  }
1623 
1624  explicit array_exprt(const array_typet &_type):
1625  exprt(ID_array, _type)
1626  {
1627  }
1628 };
1629 
1640 inline const array_exprt &to_array_expr(const exprt &expr)
1641 {
1642  PRECONDITION(expr.id()==ID_array);
1643  return static_cast<const array_exprt &>(expr);
1644 }
1645 
1650 {
1651  PRECONDITION(expr.id()==ID_array);
1652  return static_cast<array_exprt &>(expr);
1653 }
1654 
1655 template<> inline bool can_cast_expr<array_exprt>(const exprt &base)
1656 {
1657  return base.id()==ID_array;
1658 }
1659 
1662 class array_list_exprt : public exprt
1663 {
1664 public:
1665  explicit array_list_exprt(const array_typet &_type)
1666  : exprt(ID_array_list, _type)
1667  {
1668  }
1669 };
1670 
1671 template <>
1672 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1673 {
1674  return base.id() == ID_array_list;
1675 }
1676 
1677 inline void validate_expr(const array_list_exprt &value)
1678 {
1679  PRECONDITION(value.operands().size() % 2 == 0);
1680 }
1681 
1684 class vector_exprt:public exprt
1685 {
1686 public:
1687  vector_exprt():exprt(ID_vector)
1688  {
1689  }
1690 
1691  explicit vector_exprt(const vector_typet &_type):
1692  exprt(ID_vector, _type)
1693  {
1694  }
1695 };
1696 
1707 inline const vector_exprt &to_vector_expr(const exprt &expr)
1708 {
1709  PRECONDITION(expr.id()==ID_vector);
1710  return static_cast<const vector_exprt &>(expr);
1711 }
1712 
1717 {
1718  PRECONDITION(expr.id()==ID_vector);
1719  return static_cast<vector_exprt &>(expr);
1720 }
1721 
1722 template<> inline bool can_cast_expr<vector_exprt>(const exprt &base)
1723 {
1724  return base.id()==ID_vector;
1725 }
1726 
1727 
1731 {
1732 public:
1734  {
1735  }
1736 
1737  explicit union_exprt(const typet &_type):
1738  unary_exprt(ID_union, _type)
1739  {
1740  }
1741 
1742  explicit union_exprt(
1743  const irep_idt &_component_name,
1744  const exprt &_value,
1745  const typet &_type):
1746  unary_exprt(ID_union, _value, _type)
1747  {
1748  set_component_name(_component_name);
1749  }
1750 
1752  {
1753  return get(ID_component_name);
1754  }
1755 
1756  void set_component_name(const irep_idt &component_name)
1757  {
1758  set(ID_component_name, component_name);
1759  }
1760 
1761  std::size_t get_component_number() const
1762  {
1763  return get_size_t(ID_component_number);
1764  }
1765 
1766  void set_component_number(std::size_t component_number)
1767  {
1768  set(ID_component_number, component_number);
1769  }
1770 };
1771 
1782 inline const union_exprt &to_union_expr(const exprt &expr)
1783 {
1784  PRECONDITION(expr.id()==ID_union);
1786  expr.operands().size()==1,
1787  "Union constructor must have one operand");
1788  return static_cast<const union_exprt &>(expr);
1789 }
1790 
1795 {
1796  PRECONDITION(expr.id()==ID_union);
1798  expr.operands().size()==1,
1799  "Union constructor must have one operand");
1800  return static_cast<union_exprt &>(expr);
1801 }
1802 
1803 template<> inline bool can_cast_expr<union_exprt>(const exprt &base)
1804 {
1805  return base.id()==ID_union;
1806 }
1807 inline void validate_expr(const union_exprt &value)
1808 {
1809  validate_operands(value, 1, "Union constructor must have one operand");
1810 }
1811 
1812 
1815 class struct_exprt:public exprt
1816 {
1817 public:
1818  struct_exprt():exprt(ID_struct)
1819  {
1820  }
1821 
1822  explicit struct_exprt(const typet &_type):
1823  exprt(ID_struct, _type)
1824  {
1825  }
1826 };
1827 
1838 inline const struct_exprt &to_struct_expr(const exprt &expr)
1839 {
1840  PRECONDITION(expr.id()==ID_struct);
1841  return static_cast<const struct_exprt &>(expr);
1842 }
1843 
1848 {
1849  PRECONDITION(expr.id()==ID_struct);
1850  return static_cast<struct_exprt &>(expr);
1851 }
1852 
1853 template<> inline bool can_cast_expr<struct_exprt>(const exprt &base)
1854 {
1855  return base.id()==ID_struct;
1856 }
1857 
1858 
1862 {
1863 public:
1865  {
1866  }
1867 
1868  explicit complex_exprt(const complex_typet &_type):
1869  binary_exprt(ID_complex, _type)
1870  {
1871  }
1872 
1873  explicit complex_exprt(
1874  const exprt &_real, const exprt &_imag, const complex_typet &_type):
1875  binary_exprt(_real, ID_complex, _imag, _type)
1876  {
1877  }
1878 
1880  {
1881  return op0();
1882  }
1883 
1884  const exprt &real() const
1885  {
1886  return op0();
1887  }
1888 
1890  {
1891  return op1();
1892  }
1893 
1894  const exprt &imag() const
1895  {
1896  return op1();
1897  }
1898 };
1899 
1910 inline const complex_exprt &to_complex_expr(const exprt &expr)
1911 {
1912  PRECONDITION(expr.id()==ID_complex);
1914  expr.operands().size()==2,
1915  "Complex constructor must have two operands");
1916  return static_cast<const complex_exprt &>(expr);
1917 }
1918 
1923 {
1924  PRECONDITION(expr.id()==ID_complex);
1926  expr.operands().size()==2,
1927  "Complex constructor must have two operands");
1928  return static_cast<complex_exprt &>(expr);
1929 }
1930 
1931 template<> inline bool can_cast_expr<complex_exprt>(const exprt &base)
1932 {
1933  return base.id()==ID_complex;
1934 }
1935 inline void validate_expr(const complex_exprt &value)
1936 {
1937  validate_operands(value, 2, "Complex constructor must have two operands");
1938 }
1939 
1940 
1941 class namespacet;
1942 
1946 {
1947 public:
1948  object_descriptor_exprt():binary_exprt(ID_object_descriptor)
1949  {
1950  op0().id(ID_unknown);
1951  op1().id(ID_unknown);
1952  }
1953 
1954  void build(const exprt &expr, const namespacet &ns);
1955 
1957  {
1958  return op0();
1959  }
1960 
1961  const exprt &object() const
1962  {
1963  return op0();
1964  }
1965 
1966  const exprt &root_object() const
1967  {
1968  const exprt *p=&object();
1969 
1970  while(p->id()==ID_member || p->id()==ID_index)
1971  {
1972  assert(!p->operands().empty());
1973  p=&p->op0();
1974  }
1975 
1976  return *p;
1977  }
1978 
1980  {
1981  return op1();
1982  }
1983 
1984  const exprt &offset() const
1985  {
1986  return op1();
1987  }
1988 };
1989 
2001  const exprt &expr)
2002 {
2003  PRECONDITION(expr.id()==ID_object_descriptor);
2005  expr.operands().size()==2,
2006  "Object descriptor must have two operands");
2007  return static_cast<const object_descriptor_exprt &>(expr);
2008 }
2009 
2014 {
2015  PRECONDITION(expr.id()==ID_object_descriptor);
2017  expr.operands().size()==2,
2018  "Object descriptor must have two operands");
2019  return static_cast<object_descriptor_exprt &>(expr);
2020 }
2021 
2022 template<>
2024 {
2025  return base.id()==ID_object_descriptor;
2026 }
2027 inline void validate_expr(const object_descriptor_exprt &value)
2028 {
2029  validate_operands(value, 2, "Object descriptor must have two operands");
2030 }
2031 
2032 
2036 {
2037 public:
2038  dynamic_object_exprt():binary_exprt(ID_dynamic_object)
2039  {
2040  op0().id(ID_unknown);
2041  op1().id(ID_unknown);
2042  }
2043 
2044  explicit dynamic_object_exprt(const typet &type):
2045  binary_exprt(ID_dynamic_object, type)
2046  {
2047  op0().id(ID_unknown);
2048  op1().id(ID_unknown);
2049  }
2050 
2051  void set_instance(unsigned int instance);
2052 
2053  unsigned int get_instance() const;
2054 
2056  {
2057  return op1();
2058  }
2059 
2060  const exprt &valid() const
2061  {
2062  return op1();
2063  }
2064 };
2065 
2077  const exprt &expr)
2078 {
2079  PRECONDITION(expr.id()==ID_dynamic_object);
2081  expr.operands().size()==2,
2082  "Dynamic object must have two operands");
2083  return static_cast<const dynamic_object_exprt &>(expr);
2084 }
2085 
2090 {
2091  PRECONDITION(expr.id()==ID_dynamic_object);
2093  expr.operands().size()==2,
2094  "Dynamic object must have two operands");
2095  return static_cast<dynamic_object_exprt &>(expr);
2096 }
2097 
2098 template<> inline bool can_cast_expr<dynamic_object_exprt>(const exprt &base)
2099 {
2100  return base.id()==ID_dynamic_object;
2101 }
2102 
2103 inline void validate_expr(const dynamic_object_exprt &value)
2104 {
2105  validate_operands(value, 2, "Dynamic object must have two operands");
2106 }
2107 
2108 
2112 {
2113 public:
2114  explicit typecast_exprt(const typet &_type):unary_exprt(ID_typecast, _type)
2115  {
2116  }
2117 
2118  typecast_exprt(const exprt &op, const typet &_type):
2119  unary_exprt(ID_typecast, op, _type)
2120  {
2121  }
2122 
2123  // returns a typecast if the type doesn't already match
2124  static exprt conditional_cast(const exprt &expr, const typet &type)
2125  {
2126  if(expr.type() == type)
2127  return expr;
2128  else
2129  return typecast_exprt(expr, type);
2130  }
2131 };
2132 
2143 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2144 {
2145  PRECONDITION(expr.id()==ID_typecast);
2147  expr.operands().size()==1,
2148  "Typecast must have one operand");
2149  return static_cast<const typecast_exprt &>(expr);
2150 }
2151 
2156 {
2157  PRECONDITION(expr.id()==ID_typecast);
2159  expr.operands().size()==1,
2160  "Typecast must have one operand");
2161  return static_cast<typecast_exprt &>(expr);
2162 }
2163 
2164 template<> inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2165 {
2166  return base.id()==ID_typecast;
2167 }
2168 inline void validate_expr(const typecast_exprt &value)
2169 {
2170  validate_operands(value, 1, "Typecast must have one operand");
2171 }
2172 
2173 
2177 {
2178 public:
2179  floatbv_typecast_exprt():binary_exprt(ID_floatbv_typecast)
2180  {
2181  }
2182 
2184  const exprt &op,
2185  const exprt &rounding,
2186  const typet &_type):binary_exprt(op, ID_floatbv_typecast, rounding, _type)
2187  {
2188  }
2189 
2191  {
2192  return op0();
2193  }
2194 
2195  const exprt &op() const
2196  {
2197  return op0();
2198  }
2199 
2201  {
2202  return op1();
2203  }
2204 
2205  const exprt &rounding_mode() const
2206  {
2207  return op1();
2208  }
2209 };
2210 
2222 {
2223  PRECONDITION(expr.id()==ID_floatbv_typecast);
2225  expr.operands().size()==2,
2226  "Float typecast must have two operands");
2227  return static_cast<const floatbv_typecast_exprt &>(expr);
2228 }
2229 
2234 {
2235  PRECONDITION(expr.id()==ID_floatbv_typecast);
2237  expr.operands().size()==2,
2238  "Float typecast must have two operands");
2239  return static_cast<floatbv_typecast_exprt &>(expr);
2240 }
2241 
2242 template<>
2244 {
2245  return base.id()==ID_floatbv_typecast;
2246 }
2247 inline void validate_expr(const floatbv_typecast_exprt &value)
2248 {
2249  validate_operands(value, 2, "Float typecast must have two operands");
2250 }
2251 
2252 
2256 {
2257 public:
2259  {
2260  }
2261 
2262  and_exprt(const exprt &op0, const exprt &op1):
2263  multi_ary_exprt(op0, ID_and, op1, bool_typet())
2264  {
2265  }
2266 
2267  and_exprt(const exprt &op0, const exprt &op1, const exprt &op2):
2268  multi_ary_exprt(ID_and, bool_typet())
2269  {
2271  }
2272 
2274  const exprt &op0,
2275  const exprt &op1,
2276  const exprt &op2,
2277  const exprt &op3):
2278  multi_ary_exprt(ID_and, bool_typet())
2279  {
2280  exprt::operandst &op=operands();
2281  op.resize(4);
2282  op[0]=op0;
2283  op[1]=op1;
2284  op[2]=op2;
2285  op[3]=op3;
2286  }
2287 };
2288 
2295 
2306 inline const and_exprt &to_and_expr(const exprt &expr)
2307 {
2308  PRECONDITION(expr.id()==ID_and);
2309  // DATA_INVARIANT(
2310  // expr.operands().size()>=2,
2311  // "And must have two or more operands");
2312  return static_cast<const and_exprt &>(expr);
2313 }
2314 
2319 {
2320  PRECONDITION(expr.id()==ID_and);
2321  // DATA_INVARIANT(
2322  // expr.operands().size()>=2,
2323  // "And must have two or more operands");
2324  return static_cast<and_exprt &>(expr);
2325 }
2326 
2327 template<> inline bool can_cast_expr<and_exprt>(const exprt &base)
2328 {
2329  return base.id()==ID_and;
2330 }
2331 // inline void validate_expr(const and_exprt &value)
2332 // {
2333 // validate_operands(value, 2, "And must have two or more operands", true);
2334 // }
2335 
2336 
2340 {
2341 public:
2343  {
2344  }
2345 
2346  implies_exprt(const exprt &op0, const exprt &op1):
2347  binary_exprt(op0, ID_implies, op1, bool_typet())
2348  {
2349  }
2350 };
2351 
2362 inline const implies_exprt &to_implies_expr(const exprt &expr)
2363 {
2364  PRECONDITION(expr.id()==ID_implies);
2365  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
2366  return static_cast<const implies_exprt &>(expr);
2367 }
2368 
2373 {
2374  PRECONDITION(expr.id()==ID_implies);
2375  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
2376  return static_cast<implies_exprt &>(expr);
2377 }
2378 
2379 template<> inline bool can_cast_expr<implies_exprt>(const exprt &base)
2380 {
2381  return base.id()==ID_implies;
2382 }
2383 inline void validate_expr(const implies_exprt &value)
2384 {
2385  validate_operands(value, 2, "Implies must have two operands");
2386 }
2387 
2388 
2392 {
2393 public:
2395  {
2396  }
2397 
2398  or_exprt(const exprt &op0, const exprt &op1):
2399  multi_ary_exprt(op0, ID_or, op1, bool_typet())
2400  {
2401  }
2402 
2403  or_exprt(const exprt &op0, const exprt &op1, const exprt &op2):
2404  multi_ary_exprt(ID_or, bool_typet())
2405  {
2407  }
2408 
2410  const exprt &op0,
2411  const exprt &op1,
2412  const exprt &op2,
2413  const exprt &op3):
2414  multi_ary_exprt(ID_or, bool_typet())
2415  {
2416  exprt::operandst &op=operands();
2417  op.resize(4);
2418  op[0]=op0;
2419  op[1]=op1;
2420  op[2]=op2;
2421  op[3]=op3;
2422  }
2423 };
2424 
2431 
2442 inline const or_exprt &to_or_expr(const exprt &expr)
2443 {
2444  PRECONDITION(expr.id()==ID_or);
2445  // DATA_INVARIANT(
2446  // expr.operands().size()>=2,
2447  // "Or must have two or more operands");
2448  return static_cast<const or_exprt &>(expr);
2449 }
2450 
2454 inline or_exprt &to_or_expr(exprt &expr)
2455 {
2456  PRECONDITION(expr.id()==ID_or);
2457  // DATA_INVARIANT(
2458  // expr.operands().size()>=2,
2459  // "Or must have two or more operands");
2460  return static_cast<or_exprt &>(expr);
2461 }
2462 
2463 template<> inline bool can_cast_expr<or_exprt>(const exprt &base)
2464 {
2465  return base.id()==ID_or;
2466 }
2467 // inline void validate_expr(const or_exprt &value)
2468 // {
2469 // validate_operands(value, 2, "Or must have two or more operands", true);
2470 // }
2471 
2472 
2476 {
2477 public:
2479  {
2480  }
2481 
2482  xor_exprt(const exprt &_op0, const exprt &_op1):
2483  multi_ary_exprt(_op0, ID_xor, _op1, bool_typet())
2484  {
2485  }
2486 };
2487 
2498 inline const xor_exprt &to_xor_expr(const exprt &expr)
2499 {
2500  PRECONDITION(expr.id()==ID_xor);
2501  return static_cast<const xor_exprt &>(expr);
2502 }
2503 
2508 {
2509  PRECONDITION(expr.id()==ID_xor);
2510  return static_cast<xor_exprt &>(expr);
2511 }
2512 
2513 template<> inline bool can_cast_expr<xor_exprt>(const exprt &base)
2514 {
2515  return base.id()==ID_xor;
2516 }
2517 // inline void validate_expr(const bitxor_exprt &value)
2518 // {
2519 // validate_operands(
2520 // value,
2521 // 2,
2522 // "Bit-wise xor must have two or more operands",
2523 // true);
2524 // }
2525 
2526 
2530 {
2531 public:
2533  {
2534  }
2535 
2536  explicit bitnot_exprt(const exprt &op):
2537  unary_exprt(ID_bitnot, op)
2538  {
2539  }
2540 };
2541 
2552 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
2553 {
2554  PRECONDITION(expr.id()==ID_bitnot);
2555  // DATA_INVARIANT(expr.operands().size()==1,
2556  // "Bit-wise not must have one operand");
2557  return static_cast<const bitnot_exprt &>(expr);
2558 }
2559 
2564 {
2565  PRECONDITION(expr.id()==ID_bitnot);
2566  // DATA_INVARIANT(expr.operands().size()==1,
2567  // "Bit-wise not must have one operand");
2568  return static_cast<bitnot_exprt &>(expr);
2569 }
2570 
2571 template<> inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
2572 {
2573  return base.id()==ID_bitnot;
2574 }
2575 // inline void validate_expr(const bitnot_exprt &value)
2576 // {
2577 // validate_operands(value, 1, "Bit-wise not must have one operand");
2578 // }
2579 
2580 
2584 {
2585 public:
2587  {
2588  }
2589 
2590  bitor_exprt(const exprt &_op0, const exprt &_op1):
2591  multi_ary_exprt(ID_bitor, _op0.type())
2592  {
2593  copy_to_operands(_op0, _op1);
2594  }
2595 };
2596 
2607 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
2608 {
2609  PRECONDITION(expr.id()==ID_bitor);
2610  // DATA_INVARIANT(
2611  // expr.operands().size()>=2,
2612  // "Bit-wise or must have two or more operands");
2613  return static_cast<const bitor_exprt &>(expr);
2614 }
2615 
2620 {
2621  PRECONDITION(expr.id()==ID_bitor);
2622  // DATA_INVARIANT(
2623  // expr.operands().size()>=2,
2624  // "Bit-wise or must have two or more operands");
2625  return static_cast<bitor_exprt &>(expr);
2626 }
2627 
2628 template<> inline bool can_cast_expr<bitor_exprt>(const exprt &base)
2629 {
2630  return base.id()==ID_bitor;
2631 }
2632 // inline void validate_expr(const bitor_exprt &value)
2633 // {
2634 // validate_operands(
2635 // value,
2636 // 2,
2637 // "Bit-wise or must have two or more operands",
2638 // true);
2639 // }
2640 
2641 
2645 {
2646 public:
2648  {
2649  }
2650 
2651  bitxor_exprt(const exprt &_op0, const exprt &_op1):
2652  multi_ary_exprt(_op0, ID_bitxor, _op1, _op0.type())
2653  {
2654  }
2655 };
2656 
2667 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
2668 {
2669  PRECONDITION(expr.id()==ID_bitxor);
2670  // DATA_INVARIANT(
2671  // expr.operands().size()>=2,
2672  // "Bit-wise xor must have two or more operands");
2673  return static_cast<const bitxor_exprt &>(expr);
2674 }
2675 
2680 {
2681  PRECONDITION(expr.id()==ID_bitxor);
2682  // DATA_INVARIANT(
2683  // expr.operands().size()>=2,
2684  // "Bit-wise xor must have two or more operands");
2685  return static_cast<bitxor_exprt &>(expr);
2686 }
2687 
2688 template<> inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
2689 {
2690  return base.id()==ID_bitxor;
2691 }
2692 // inline void validate_expr(const bitxor_exprt &value)
2693 // {
2694 // validate_operands(
2695 // value,
2696 // 2,
2697 // "Bit-wise xor must have two or more operands",
2698 // true);
2699 // }
2700 
2701 
2705 {
2706 public:
2708  {
2709  }
2710 
2711  bitand_exprt(const exprt &_op0, const exprt &_op1):
2712  multi_ary_exprt(ID_bitand, _op0.type())
2713  {
2714  copy_to_operands(_op0, _op1);
2715  }
2716 };
2717 
2728 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
2729 {
2730  PRECONDITION(expr.id()==ID_bitand);
2731  // DATA_INVARIANT(
2732  // expr.operands().size()>=2,
2733  // "Bit-wise and must have two or more operands");
2734  return static_cast<const bitand_exprt &>(expr);
2735 }
2736 
2741 {
2742  PRECONDITION(expr.id()==ID_bitand);
2743  // DATA_INVARIANT(
2744  // expr.operands().size()>=2,
2745  // "Bit-wise and must have two or more operands");
2746  return static_cast<bitand_exprt &>(expr);
2747 }
2748 
2749 template<> inline bool can_cast_expr<bitand_exprt>(const exprt &base)
2750 {
2751  return base.id()==ID_bitand;
2752 }
2753 // inline void validate_expr(const bitand_exprt &value)
2754 // {
2755 // validate_operands(
2756 // value,
2757 // 2,
2758 // "Bit-wise and must have two or more operands",
2759 // true);
2760 // }
2761 
2762 
2766 {
2767 public:
2768  explicit shift_exprt(const irep_idt &_id):binary_exprt(_id)
2769  {
2770  }
2771 
2772  shift_exprt(const irep_idt &_id, const typet &_type):
2773  binary_exprt(_id, _type)
2774  {
2775  }
2776 
2777  shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance):
2778  binary_exprt(_src, _id, _distance)
2779  {
2780  }
2781 
2782  shift_exprt(
2783  const exprt &_src,
2784  const irep_idt &_id,
2785  const std::size_t _distance);
2786 
2788  {
2789  return op0();
2790  }
2791 
2792  const exprt &op() const
2793  {
2794  return op0();
2795  }
2796 
2798  {
2799  return op1();
2800  }
2801 
2802  const exprt &distance() const
2803  {
2804  return op1();
2805  }
2806 };
2807 
2818 inline const shift_exprt &to_shift_expr(const exprt &expr)
2819 {
2821  expr.operands().size()==2,
2822  "Shifts must have two operands");
2823  return static_cast<const shift_exprt &>(expr);
2824 }
2825 
2830 {
2832  expr.operands().size()==2,
2833  "Shifts must have two operands");
2834  return static_cast<shift_exprt &>(expr);
2835 }
2836 
2837 // The to_*_expr function for this type doesn't do any checks before casting,
2838 // therefore the implementation is essentially a static_cast.
2839 // Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
2840 // inline void validate_expr(const shift_exprt &value)
2841 // {
2842 // validate_operands(value, 2, "Shifts must have two operands");
2843 // }
2844 
2845 
2849 {
2850 public:
2852  {
2853  }
2854 
2855  shl_exprt(const exprt &_src, const exprt &_distance):
2856  shift_exprt(_src, ID_shl, _distance)
2857  {
2858  }
2859 
2860  shl_exprt(const exprt &_src, const std::size_t _distance):
2861  shift_exprt(_src, ID_shl, _distance)
2862  {
2863  }
2864 };
2865 
2869 {
2870 public:
2872  {
2873  }
2874 
2875  ashr_exprt(const exprt &_src, const exprt &_distance):
2876  shift_exprt(_src, ID_ashr, _distance)
2877  {
2878  }
2879 
2880  ashr_exprt(const exprt &_src, const std::size_t _distance):
2881  shift_exprt(_src, ID_ashr, _distance)
2882  {
2883  }
2884 };
2885 
2889 {
2890 public:
2892  {
2893  }
2894 
2895  lshr_exprt(const exprt &_src, const exprt &_distance):
2896  shift_exprt(_src, ID_lshr, _distance)
2897  {
2898  }
2899 
2900  lshr_exprt(const exprt &_src, const std::size_t _distance):
2901  shift_exprt(_src, ID_lshr, _distance)
2902  {
2903  }
2904 };
2905 
2909 {
2910 public:
2912  {
2913  }
2914 
2915  explicit replication_exprt(const typet &_type):
2916  binary_exprt(ID_replication, _type)
2917  {
2918  }
2919 
2920  replication_exprt(const exprt &_times, const exprt &_src):
2921  binary_exprt(_times, ID_replication, _src)
2922  {
2923  }
2924 
2926  {
2927  return op0();
2928  }
2929 
2930  const exprt &times() const
2931  {
2932  return op0();
2933  }
2934 
2936  {
2937  return op1();
2938  }
2939 
2940  const exprt &op() const
2941  {
2942  return op1();
2943  }
2944 };
2945 
2956 inline const replication_exprt &to_replication_expr(const exprt &expr)
2957 {
2958  PRECONDITION(expr.id()==ID_replication);
2960  expr.operands().size()==2,
2961  "Bit-wise replication must have two operands");
2962  return static_cast<const replication_exprt &>(expr);
2963 }
2964 
2969 {
2970  PRECONDITION(expr.id()==ID_replication);
2972  expr.operands().size()==2,
2973  "Bit-wise replication must have two operands");
2974  return static_cast<replication_exprt &>(expr);
2975 }
2976 
2977 template<> inline bool can_cast_expr<replication_exprt>(const exprt &base)
2978 {
2979  return base.id()==ID_replication;
2980 }
2981 inline void validate_expr(const replication_exprt &value)
2982 {
2983  validate_operands(value, 2, "Bit-wise replication must have two operands");
2984 }
2985 
2986 
2990 {
2991 public:
2993  {
2994  }
2995 
2997  const exprt &_src,
2998  const exprt &_index):binary_predicate_exprt(_src, ID_extractbit, _index)
2999  {
3000  }
3001 
3003  const exprt &_src,
3004  const std::size_t _index);
3005 
3007  {
3008  return op0();
3009  }
3010 
3012  {
3013  return op1();
3014  }
3015 
3016  const exprt &src() const
3017  {
3018  return op0();
3019  }
3020 
3021  const exprt &index() const
3022  {
3023  return op1();
3024  }
3025 };
3026 
3037 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
3038 {
3039  PRECONDITION(expr.id()==ID_extractbit);
3041  expr.operands().size()==2,
3042  "Extract bit must have two operands");
3043  return static_cast<const extractbit_exprt &>(expr);
3044 }
3045 
3050 {
3051  PRECONDITION(expr.id()==ID_extractbit);
3053  expr.operands().size()==2,
3054  "Extract bit must have two operands");
3055  return static_cast<extractbit_exprt &>(expr);
3056 }
3057 
3058 template<> inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
3059 {
3060  return base.id()==ID_extractbit;
3061 }
3062 inline void validate_expr(const extractbit_exprt &value)
3063 {
3064  validate_operands(value, 2, "Extract bit must have two operands");
3065 }
3066 
3067 
3071 {
3072 public:
3073  extractbits_exprt():exprt(ID_extractbits)
3074  {
3075  operands().resize(3);
3076  }
3077 
3078  // the ordering upper-lower matches the SMT-LIB
3080  const exprt &_src,
3081  const exprt &_upper,
3082  const exprt &_lower,
3083  const typet &_type):exprt(ID_extractbits, _type)
3084  {
3085  copy_to_operands(_src, _upper, _lower);
3086  }
3087 
3089  const exprt &_src,
3090  const std::size_t _upper,
3091  const std::size_t _lower,
3092  const typet &_type);
3093 
3095  {
3096  return op0();
3097  }
3098 
3100  {
3101  return op1();
3102  }
3103 
3105  {
3106  return op2();
3107  }
3108 
3109  const exprt &src() const
3110  {
3111  return op0();
3112  }
3113 
3114  const exprt &upper() const
3115  {
3116  return op1();
3117  }
3118 
3119  const exprt &lower() const
3120  {
3121  return op2();
3122  }
3123 };
3124 
3135 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
3136 {
3137  PRECONDITION(expr.id()==ID_extractbits);
3139  expr.operands().size()==3,
3140  "Extract bits must have three operands");
3141  return static_cast<const extractbits_exprt &>(expr);
3142 }
3143 
3148 {
3149  PRECONDITION(expr.id()==ID_extractbits);
3151  expr.operands().size()==3,
3152  "Extract bits must have three operands");
3153  return static_cast<extractbits_exprt &>(expr);
3154 }
3155 
3156 template<> inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
3157 {
3158  return base.id()==ID_extractbits;
3159 }
3160 inline void validate_expr(const extractbits_exprt &value)
3161 {
3162  validate_operands(value, 3, "Extract bits must have three operands");
3163 }
3164 
3165 
3169 {
3170 public:
3171  explicit address_of_exprt(const exprt &op);
3172 
3173  address_of_exprt(const exprt &op, const pointer_typet &_type):
3174  unary_exprt(ID_address_of, op, _type)
3175  {
3176  }
3177 
3179  {
3180  return op0();
3181  }
3182 
3183  const exprt &object() const
3184  {
3185  return op0();
3186  }
3187 };
3188 
3199 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
3200 {
3201  PRECONDITION(expr.id()==ID_address_of);
3202  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
3203  return static_cast<const address_of_exprt &>(expr);
3204 }
3205 
3210 {
3211  PRECONDITION(expr.id()==ID_address_of);
3212  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
3213  return static_cast<address_of_exprt &>(expr);
3214 }
3215 
3216 template<> inline bool can_cast_expr<address_of_exprt>(const exprt &base)
3217 {
3218  return base.id()==ID_address_of;
3219 }
3220 inline void validate_expr(const address_of_exprt &value)
3221 {
3222  validate_operands(value, 1, "Address of must have one operand");
3223 }
3224 
3225 
3229 {
3230 public:
3231  explicit not_exprt(const exprt &op):
3232  unary_exprt(ID_not, op) // type from op.type()
3233  {
3234  PRECONDITION(op.type().id()==ID_bool);
3235  }
3236 
3238  {
3239  }
3240 };
3241 
3252 inline const not_exprt &to_not_expr(const exprt &expr)
3253 {
3254  PRECONDITION(expr.id()==ID_not);
3255  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
3256  return static_cast<const not_exprt &>(expr);
3257 }
3258 
3263 {
3264  PRECONDITION(expr.id()==ID_not);
3265  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
3266  return static_cast<not_exprt &>(expr);
3267 }
3268 
3269 template<> inline bool can_cast_expr<not_exprt>(const exprt &base)
3270 {
3271  return base.id()==ID_not;
3272 }
3273 
3274 inline void validate_expr(const not_exprt &value)
3275 {
3276  validate_operands(value, 1, "Not must have one operand");
3277 }
3278 
3279 
3283 {
3284 public:
3285  dereference_exprt():unary_exprt(ID_dereference)
3286  {
3287  }
3288 
3289  explicit dereference_exprt(const typet &type):
3290  unary_exprt(ID_dereference, type)
3291  {
3292  }
3293 
3294  explicit dereference_exprt(const exprt &op):
3295  unary_exprt(ID_dereference, op, op.type().subtype())
3296  {
3297  PRECONDITION(op.type().id()==ID_pointer);
3298  }
3299 
3301  unary_exprt(ID_dereference, op, type)
3302  {
3303  }
3304 
3306  {
3307  return op0();
3308  }
3309 
3310  const exprt &pointer() const
3311  {
3312  return op0();
3313  }
3314 };
3315 
3326 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
3327 {
3328  PRECONDITION(expr.id()==ID_dereference);
3330  expr.operands().size()==1,
3331  "Dereference must have one operand");
3332  return static_cast<const dereference_exprt &>(expr);
3333 }
3334 
3339 {
3340  PRECONDITION(expr.id()==ID_dereference);
3342  expr.operands().size()==1,
3343  "Dereference must have one operand");
3344  return static_cast<dereference_exprt &>(expr);
3345 }
3346 
3347 template<> inline bool can_cast_expr<dereference_exprt>(const exprt &base)
3348 {
3349  return base.id()==ID_dereference;
3350 }
3351 inline void validate_expr(const dereference_exprt &value)
3352 {
3353  validate_operands(value, 1, "Dereference must have one operand");
3354 }
3355 
3356 
3359 class if_exprt:public exprt
3360 {
3361 public:
3362  if_exprt(const exprt &cond, const exprt &t, const exprt &f):
3363  exprt(ID_if, t.type())
3364  {
3365  copy_to_operands(cond, t, f);
3366  }
3367 
3369  const exprt &cond,
3370  const exprt &t,
3371  const exprt &f,
3372  const typet &type):
3373  exprt(ID_if, type)
3374  {
3375  copy_to_operands(cond, t, f);
3376  }
3377 
3378  if_exprt():exprt(ID_if)
3379  {
3380  operands().resize(3);
3381  }
3382 
3384  {
3385  return op0();
3386  }
3387 
3388  const exprt &cond() const
3389  {
3390  return op0();
3391  }
3392 
3394  {
3395  return op1();
3396  }
3397 
3398  const exprt &true_case() const
3399  {
3400  return op1();
3401  }
3402 
3404  {
3405  return op2();
3406  }
3407 
3408  const exprt &false_case() const
3409  {
3410  return op2();
3411  }
3412 };
3413 
3424 inline const if_exprt &to_if_expr(const exprt &expr)
3425 {
3426  PRECONDITION(expr.id()==ID_if);
3428  expr.operands().size()==3,
3429  "If-then-else must have three operands");
3430  return static_cast<const if_exprt &>(expr);
3431 }
3432 
3436 inline if_exprt &to_if_expr(exprt &expr)
3437 {
3438  PRECONDITION(expr.id()==ID_if);
3440  expr.operands().size()==3,
3441  "If-then-else must have three operands");
3442  return static_cast<if_exprt &>(expr);
3443 }
3444 
3445 template<> inline bool can_cast_expr<if_exprt>(const exprt &base)
3446 {
3447  return base.id()==ID_if;
3448 }
3449 inline void validate_expr(const if_exprt &value)
3450 {
3451  validate_operands(value, 3, "If-then-else must have three operands");
3452 }
3453 
3454 
3459 class with_exprt:public exprt
3460 {
3461 public:
3463  const exprt &_old,
3464  const exprt &_where,
3465  const exprt &_new_value):
3466  exprt(ID_with, _old.type())
3467  {
3468  copy_to_operands(_old, _where, _new_value);
3469  }
3470 
3471  with_exprt():exprt(ID_with)
3472  {
3473  operands().resize(3);
3474  }
3475 
3477  {
3478  return op0();
3479  }
3480 
3481  const exprt &old() const
3482  {
3483  return op0();
3484  }
3485 
3487  {
3488  return op1();
3489  }
3490 
3491  const exprt &where() const
3492  {
3493  return op1();
3494  }
3495 
3497  {
3498  return op2();
3499  }
3500 
3501  const exprt &new_value() const
3502  {
3503  return op2();
3504  }
3505 };
3506 
3517 inline const with_exprt &to_with_expr(const exprt &expr)
3518 {
3519  PRECONDITION(expr.id()==ID_with);
3521  expr.operands().size()==3,
3522  "Array/structure update must have three operands");
3523  return static_cast<const with_exprt &>(expr);
3524 }
3525 
3530 {
3531  PRECONDITION(expr.id()==ID_with);
3533  expr.operands().size()==3,
3534  "Array/structure update must have three operands");
3535  return static_cast<with_exprt &>(expr);
3536 }
3537 
3538 template<> inline bool can_cast_expr<with_exprt>(const exprt &base)
3539 {
3540  return base.id()==ID_with;
3541 }
3542 inline void validate_expr(const with_exprt &value)
3543 {
3545  value,
3546  3,
3547  "Array/structure update must have three operands");
3548 }
3549 
3550 
3552 {
3553 public:
3554  explicit index_designatort(const exprt &_index):
3555  exprt(ID_index_designator)
3556  {
3557  copy_to_operands(_index);
3558  }
3559 
3560  const exprt &index() const
3561  {
3562  return op0();
3563  }
3564 
3566  {
3567  return op0();
3568  }
3569 };
3570 
3581 inline const index_designatort &to_index_designator(const exprt &expr)
3582 {
3583  PRECONDITION(expr.id()==ID_index_designator);
3585  expr.operands().size()==1,
3586  "Index designator must have one operand");
3587  return static_cast<const index_designatort &>(expr);
3588 }
3589 
3594 {
3595  PRECONDITION(expr.id()==ID_index_designator);
3597  expr.operands().size()==1,
3598  "Index designator must have one operand");
3599  return static_cast<index_designatort &>(expr);
3600 }
3601 
3602 template<> inline bool can_cast_expr<index_designatort>(const exprt &base)
3603 {
3604  return base.id()==ID_index_designator;
3605 }
3606 inline void validate_expr(const index_designatort &value)
3607 {
3608  validate_operands(value, 1, "Index designator must have one operand");
3609 }
3610 
3611 
3613 {
3614 public:
3615  explicit member_designatort(const irep_idt &_component_name):
3616  exprt(ID_member_designator)
3617  {
3618  set(ID_component_name, _component_name);
3619  }
3620 
3622  {
3623  return get(ID_component_name);
3624  }
3625 };
3626 
3638 {
3639  PRECONDITION(expr.id()==ID_member_designator);
3641  !expr.has_operands(),
3642  "Member designator must not have operands");
3643  return static_cast<const member_designatort &>(expr);
3644 }
3645 
3650 {
3651  PRECONDITION(expr.id()==ID_member_designator);
3653  !expr.has_operands(),
3654  "Member designator must not have operands");
3655  return static_cast<member_designatort &>(expr);
3656 }
3657 
3658 template<> inline bool can_cast_expr<member_designatort>(const exprt &base)
3659 {
3660  return base.id()==ID_member_designator;
3661 }
3662 inline void validate_expr(const member_designatort &value)
3663 {
3664  validate_operands(value, 0, "Member designator must not have operands");
3665 }
3666 
3667 
3670 class update_exprt:public exprt
3671 {
3672 public:
3674  const exprt &_old,
3675  const exprt &_designator,
3676  const exprt &_new_value):
3677  exprt(ID_update, _old.type())
3678  {
3679  copy_to_operands(_old, _designator, _new_value);
3680  }
3681 
3682  explicit update_exprt(const typet &_type):
3683  exprt(ID_update, _type)
3684  {
3685  operands().resize(3);
3686  }
3687 
3688  update_exprt():exprt(ID_update)
3689  {
3690  operands().resize(3);
3691  op1().id(ID_designator);
3692  }
3693 
3695  {
3696  return op0();
3697  }
3698 
3699  const exprt &old() const
3700  {
3701  return op0();
3702  }
3703 
3704  // the designator operands are either
3705  // 1) member_designator or
3706  // 2) index_designator
3707  // as defined above
3709  {
3710  return op1().operands();
3711  }
3712 
3714  {
3715  return op1().operands();
3716  }
3717 
3719  {
3720  return op2();
3721  }
3722 
3723  const exprt &new_value() const
3724  {
3725  return op2();
3726  }
3727 };
3728 
3739 inline const update_exprt &to_update_expr(const exprt &expr)
3740 {
3741  PRECONDITION(expr.id()==ID_update);
3743  expr.operands().size()==3,
3744  "Array/structure update must have three operands");
3745  return static_cast<const update_exprt &>(expr);
3746 }
3747 
3752 {
3753  PRECONDITION(expr.id()==ID_update);
3755  expr.operands().size()==3,
3756  "Array/structure update must have three operands");
3757  return static_cast<update_exprt &>(expr);
3758 }
3759 
3760 template<> inline bool can_cast_expr<update_exprt>(const exprt &base)
3761 {
3762  return base.id()==ID_update;
3763 }
3764 inline void validate_expr(const update_exprt &value)
3765 {
3767  value,
3768  3,
3769  "Array/structure update must have three operands");
3770 }
3771 
3772 
3773 #if 0
3774 
3776 class array_update_exprt:public exprt
3777 {
3778 public:
3779  array_update_exprt(
3780  const exprt &_array,
3781  const exprt &_index,
3782  const exprt &_new_value):
3783  exprt(ID_array_update, _array.type())
3784  {
3785  copy_to_operands(_array, _index, _new_value);
3786  }
3787 
3788  array_update_exprt():exprt(ID_array_update)
3789  {
3790  operands().resize(3);
3791  }
3792 
3793  exprt &array()
3794  {
3795  return op0();
3796  }
3797 
3798  const exprt &array() const
3799  {
3800  return op0();
3801  }
3802 
3803  exprt &index()
3804  {
3805  return op1();
3806  }
3807 
3808  const exprt &index() const
3809  {
3810  return op1();
3811  }
3812 
3813  exprt &new_value()
3814  {
3815  return op2();
3816  }
3817 
3818  const exprt &new_value() const
3819  {
3820  return op2();
3821  }
3822 };
3823 
3834 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3835 {
3836  PRECONDITION(expr.id()==ID_array_update);
3838  expr.operands().size()==3,
3839  "Array update must have three operands");
3840  return static_cast<const array_update_exprt &>(expr);
3841 }
3842 
3846 inline array_update_exprt &to_array_update_expr(exprt &expr)
3847 {
3848  PRECONDITION(expr.id()==ID_array_update);
3850  expr.operands().size()==3,
3851  "Array update must have three operands");
3852  return static_cast<array_update_exprt &>(expr);
3853 }
3854 
3855 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
3856 {
3857  return base.id()==ID_array_update;
3858 }
3859 inline void validate_expr(const array_update_exprt &value)
3860 {
3861  validate_operands(value, 3, "Array update must have three operands");
3862 }
3863 
3864 #endif
3865 
3866 
3870 {
3871 public:
3873  const exprt &op,
3874  const irep_idt &component_name,
3875  const typet &_type):
3876  unary_exprt(ID_member, op, _type)
3877  {
3878  set_component_name(component_name);
3879  }
3880 
3882  const exprt &op,
3883  const struct_typet::componentt &c):
3884  unary_exprt(ID_member, op, c.type())
3885  {
3887  }
3888 
3890  {
3891  }
3892 
3894  {
3895  return get(ID_component_name);
3896  }
3897 
3898  void set_component_name(const irep_idt &component_name)
3899  {
3900  set(ID_component_name, component_name);
3901  }
3902 
3903  std::size_t get_component_number() const
3904  {
3905  return get_size_t(ID_component_number);
3906  }
3907 
3908  // will go away, use compound()
3909  const exprt &struct_op() const
3910  {
3911  return op0();
3912  }
3913 
3914  // will go away, use compound()
3916  {
3917  return op0();
3918  }
3919 
3920  const exprt &compound() const
3921  {
3922  return op0();
3923  }
3924 
3926  {
3927  return op0();
3928  }
3929 
3930  // Retrieves the object(symbol) this member corresponds to
3931  inline const symbol_exprt &symbol() const
3932  {
3933  const exprt &op=op0();
3934  if(op.id()==ID_member)
3935  {
3936  return static_cast<const member_exprt &>(op).symbol();
3937  }
3938 
3939  return to_symbol_expr(op);
3940  }
3941 };
3942 
3953 inline const member_exprt &to_member_expr(const exprt &expr)
3954 {
3955  PRECONDITION(expr.id()==ID_member);
3957  expr.operands().size()==1,
3958  "Extract member must have one operand");
3959  return static_cast<const member_exprt &>(expr);
3960 }
3961 
3966 {
3967  PRECONDITION(expr.id()==ID_member);
3969  expr.operands().size()==1,
3970  "Extract member must have one operand");
3971  return static_cast<member_exprt &>(expr);
3972 }
3973 
3974 template<> inline bool can_cast_expr<member_exprt>(const exprt &base)
3975 {
3976  return base.id()==ID_member;
3977 }
3978 inline void validate_expr(const member_exprt &value)
3979 {
3980  validate_operands(value, 1, "Extract member must have one operand");
3981 }
3982 
3983 
3987 {
3988 public:
3989  explicit isnan_exprt(const exprt &op):
3990  unary_predicate_exprt(ID_isnan, op)
3991  {
3992  }
3993 
3995  {
3996  }
3997 };
3998 
4009 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
4010 {
4011  PRECONDITION(expr.id()==ID_isnan);
4012  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
4013  return static_cast<const isnan_exprt &>(expr);
4014 }
4015 
4020 {
4021  PRECONDITION(expr.id()==ID_isnan);
4022  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
4023  return static_cast<isnan_exprt &>(expr);
4024 }
4025 
4026 template<> inline bool can_cast_expr<isnan_exprt>(const exprt &base)
4027 {
4028  return base.id()==ID_isnan;
4029 }
4030 inline void validate_expr(const isnan_exprt &value)
4031 {
4032  validate_operands(value, 1, "Is NaN must have one operand");
4033 }
4034 
4035 
4039 {
4040 public:
4041  explicit isinf_exprt(const exprt &op):
4042  unary_predicate_exprt(ID_isinf, op)
4043  {
4044  }
4045 
4047  {
4048  }
4049 };
4050 
4061 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
4062 {
4063  PRECONDITION(expr.id()==ID_isinf);
4065  expr.operands().size()==1,
4066  "Is infinite must have one operand");
4067  return static_cast<const isinf_exprt &>(expr);
4068 }
4069 
4074 {
4075  PRECONDITION(expr.id()==ID_isinf);
4077  expr.operands().size()==1,
4078  "Is infinite must have one operand");
4079  return static_cast<isinf_exprt &>(expr);
4080 }
4081 
4082 template<> inline bool can_cast_expr<isinf_exprt>(const exprt &base)
4083 {
4084  return base.id()==ID_isinf;
4085 }
4086 inline void validate_expr(const isinf_exprt &value)
4087 {
4088  validate_operands(value, 1, "Is infinite must have one operand");
4089 }
4090 
4091 
4095 {
4096 public:
4097  explicit isfinite_exprt(const exprt &op):
4098  unary_predicate_exprt(ID_isfinite, op)
4099  {
4100  }
4101 
4103  {
4104  }
4105 };
4106 
4117 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
4118 {
4119  PRECONDITION(expr.id()==ID_isfinite);
4120  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
4121  return static_cast<const isfinite_exprt &>(expr);
4122 }
4123 
4128 {
4129  PRECONDITION(expr.id()==ID_isfinite);
4130  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
4131  return static_cast<isfinite_exprt &>(expr);
4132 }
4133 
4134 template<> inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
4135 {
4136  return base.id()==ID_isfinite;
4137 }
4138 inline void validate_expr(const isfinite_exprt &value)
4139 {
4140  validate_operands(value, 1, "Is finite must have one operand");
4141 }
4142 
4143 
4147 {
4148 public:
4149  explicit isnormal_exprt(const exprt &op):
4150  unary_predicate_exprt(ID_isnormal, op)
4151  {
4152  }
4153 
4155  {
4156  }
4157 };
4158 
4169 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
4170 {
4171  PRECONDITION(expr.id()==ID_isnormal);
4172  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
4173  return static_cast<const isnormal_exprt &>(expr);
4174 }
4175 
4180 {
4181  PRECONDITION(expr.id()==ID_isnormal);
4182  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
4183  return static_cast<isnormal_exprt &>(expr);
4184 }
4185 
4186 template<> inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
4187 {
4188  return base.id()==ID_isnormal;
4189 }
4190 inline void validate_expr(const isnormal_exprt &value)
4191 {
4192  validate_operands(value, 1, "Is normal must have one operand");
4193 }
4194 
4195 
4199 {
4200 public:
4202  {
4203  }
4204 
4205  ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs):
4206  binary_relation_exprt(_lhs, ID_ieee_float_equal, _rhs)
4207  {
4208  }
4209 };
4210 
4222 {
4223  PRECONDITION(expr.id()==ID_ieee_float_equal);
4225  expr.operands().size()==2,
4226  "IEEE equality must have two operands");
4227  return static_cast<const ieee_float_equal_exprt &>(expr);
4228 }
4229 
4234 {
4235  PRECONDITION(expr.id()==ID_ieee_float_equal);
4237  expr.operands().size()==2,
4238  "IEEE equality must have two operands");
4239  return static_cast<ieee_float_equal_exprt &>(expr);
4240 }
4241 
4242 template<>
4244 {
4245  return base.id()==ID_ieee_float_equal;
4246 }
4247 inline void validate_expr(const ieee_float_equal_exprt &value)
4248 {
4249  validate_operands(value, 2, "IEEE equality must have two operands");
4250 }
4251 
4252 
4256 {
4257 public:
4259  binary_relation_exprt(ID_ieee_float_notequal)
4260  {
4261  }
4262 
4263  ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs):
4264  binary_relation_exprt(_lhs, ID_ieee_float_notequal, _rhs)
4265  {
4266  }
4267 };
4268 
4280  const exprt &expr)
4281 {
4282  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4284  expr.operands().size()==2,
4285  "IEEE inequality must have two operands");
4286  return static_cast<const ieee_float_notequal_exprt &>(expr);
4287 }
4288 
4293 {
4294  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4296  expr.operands().size()==2,
4297  "IEEE inequality must have two operands");
4298  return static_cast<ieee_float_notequal_exprt &>(expr);
4299 }
4300 
4301 template<>
4303 {
4304  return base.id()==ID_ieee_float_notequal;
4305 }
4306 inline void validate_expr(const ieee_float_notequal_exprt &value)
4307 {
4308  validate_operands(value, 2, "IEEE inequality must have two operands");
4309 }
4310 
4311 
4315 {
4316 public:
4318  {
4319  operands().resize(3);
4320  }
4321 
4323  const exprt &_lhs,
4324  const irep_idt &_id,
4325  const exprt &_rhs,
4326  const exprt &_rm):
4327  exprt(_id)
4328  {
4329  copy_to_operands(_lhs, _rhs, _rm);
4330  }
4331 
4333  {
4334  return op0();
4335  }
4336 
4337  const exprt &lhs() const
4338  {
4339  return op0();
4340  }
4341 
4343  {
4344  return op1();
4345  }
4346 
4347  const exprt &rhs() const
4348  {
4349  return op1();
4350  }
4351 
4353  {
4354  return op2();
4355  }
4356 
4357  const exprt &rounding_mode() const
4358  {
4359  return op2();
4360  }
4361 };
4362 
4374 {
4376  expr.operands().size()==3,
4377  "IEEE float operations must have three arguments");
4378  return static_cast<const ieee_float_op_exprt &>(expr);
4379 }
4380 
4385 {
4387  expr.operands().size()==3,
4388  "IEEE float operations must have three arguments");
4389  return static_cast<ieee_float_op_exprt &>(expr);
4390 }
4391 
4392 // The to_*_expr function for this type doesn't do any checks before casting,
4393 // therefore the implementation is essentially a static_cast.
4394 // Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
4395 // template<>
4396 // inline void validate_expr<ieee_float_op_exprt>(
4397 // const ieee_float_op_exprt &value)
4398 // {
4399 // validate_operands(
4400 // value,
4401 // 3,
4402 // "IEEE float operations must have three arguments");
4403 // }
4404 
4405 
4408 class type_exprt:public exprt
4409 {
4410 public:
4411  type_exprt():exprt(ID_type)
4412  {
4413  }
4414 
4415  explicit type_exprt(const typet &type):exprt(ID_type, type)
4416  {
4417  }
4418 };
4419 
4422 class constant_exprt:public exprt
4423 {
4424 public:
4425  constant_exprt():exprt(ID_constant)
4426  {
4427  }
4428 
4429  explicit constant_exprt(const typet &type):exprt(ID_constant, type)
4430  {
4431  }
4432 
4433  constant_exprt(const irep_idt &_value, const typet &_type):
4434  exprt(ID_constant, _type)
4435  {
4436  set_value(_value);
4437  }
4438 
4439  const irep_idt &get_value() const
4440  {
4441  return get(ID_value);
4442  }
4443 
4444  void set_value(const irep_idt &value)
4445  {
4446  set(ID_value, value);
4447  }
4448 
4449  bool value_is_zero_string() const;
4450 };
4451 
4452 
4463 inline const constant_exprt &to_constant_expr(const exprt &expr)
4464 {
4465  PRECONDITION(expr.id()==ID_constant);
4466  return static_cast<const constant_exprt &>(expr);
4467 }
4468 
4473 {
4474  PRECONDITION(expr.id()==ID_constant);
4475  return static_cast<constant_exprt &>(expr);
4476 }
4477 
4478 template<> inline bool can_cast_expr<constant_exprt>(const exprt &base)
4479 {
4480  return base.id()==ID_constant;
4481 }
4482 
4483 
4487 {
4488 public:
4490  {
4491  set_value(ID_true);
4492  }
4493 };
4494 
4498 {
4499 public:
4501  {
4502  set_value(ID_false);
4503  }
4504 };
4505 
4508 class nil_exprt:public exprt
4509 {
4510 public:
4511  nil_exprt():exprt(static_cast<const exprt &>(get_nil_irep()))
4512  {
4513  }
4514 };
4515 
4519 {
4520 public:
4522  {
4523  set_value(ID_NULL);
4524  }
4525 };
4526 
4530 {
4531 public:
4532  function_application_exprt():binary_exprt(ID_function_application)
4533  {
4534  op0()=symbol_exprt();
4535  }
4536 
4537  explicit function_application_exprt(const typet &_type):
4538  binary_exprt(ID_function_application, _type)
4539  {
4540  op0()=symbol_exprt();
4541  }
4542 
4544  const symbol_exprt &_function, const typet &_type):
4545  function_application_exprt(_type) // NOLINT(runtime/explicit)
4546  {
4547  function()=_function;
4548  }
4549 
4550  symbol_exprt &function()
4551  {
4552  return static_cast<symbol_exprt &>(op0());
4553  }
4554 
4555  const symbol_exprt &function() const
4556  {
4557  return static_cast<const symbol_exprt &>(op0());
4558  }
4559 
4561 
4563  {
4564  return op1().operands();
4565  }
4566 
4567  const argumentst &arguments() const
4568  {
4569  return op1().operands();
4570  }
4571 };
4572 
4584  const exprt &expr)
4585 {
4586  PRECONDITION(expr.id()==ID_function_application);
4588  expr.operands().size()==2,
4589  "Function application must have two operands");
4590  return static_cast<const function_application_exprt &>(expr);
4591 }
4592 
4597 {
4598  PRECONDITION(expr.id()==ID_function_application);
4600  expr.operands().size()==2,
4601  "Function application must have two operands");
4602  return static_cast<function_application_exprt &>(expr);
4603 }
4604 
4605 template<>
4607 {
4608  return base.id()==ID_function_application;
4609 }
4611 {
4612  validate_operands(value, 2, "Function application must have two operands");
4613 }
4614 
4615 
4624 {
4625 public:
4626  concatenation_exprt():exprt(ID_concatenation)
4627  {
4628  }
4629 
4630  explicit concatenation_exprt(const typet &_type):
4631  exprt(ID_concatenation, _type)
4632  {
4633  }
4634 
4636  const exprt &_op0, const exprt &_op1, const typet &_type):
4637  exprt(ID_concatenation, _type)
4638  {
4639  copy_to_operands(_op0, _op1);
4640  }
4641 };
4642 
4654 {
4655  PRECONDITION(expr.id()==ID_concatenation);
4656  // DATA_INVARIANT(
4657  // expr.operands().size()>=2,
4658  // "Concatenation must have two or more operands");
4659  return static_cast<const concatenation_exprt &>(expr);
4660 }
4661 
4666 {
4667  PRECONDITION(expr.id()==ID_concatenation);
4668  // DATA_INVARIANT(
4669  // expr.operands().size()>=2,
4670  // "Concatenation must have two or more operands");
4671  return static_cast<concatenation_exprt &>(expr);
4672 }
4673 
4674 template<> inline bool can_cast_expr<concatenation_exprt>(const exprt &base)
4675 {
4676  return base.id()==ID_concatenation;
4677 }
4678 // template<>
4679 // inline void validate_expr<concatenation_exprt>(
4680 // const concatenation_exprt &value)
4681 // {
4682 // validate_operands(
4683 // value,
4684 // 2,
4685 // "Concatenation must have two or more operands",
4686 // true);
4687 // }
4688 
4689 
4692 class infinity_exprt:public exprt
4693 {
4694 public:
4695  explicit infinity_exprt(const typet &_type):
4696  exprt(ID_infinity, _type)
4697  {
4698  }
4699 };
4700 
4703 class let_exprt:public exprt
4704 {
4705 public:
4706  let_exprt():exprt(ID_let)
4707  {
4708  operands().resize(3);
4709  op0()=symbol_exprt();
4710  }
4711 
4713  {
4714  return static_cast<symbol_exprt &>(op0());
4715  }
4716 
4717  const symbol_exprt &symbol() const
4718  {
4719  return static_cast<const symbol_exprt &>(op0());
4720  }
4721 
4723  {
4724  return op1();
4725  }
4726 
4727  const exprt &value() const
4728  {
4729  return op1();
4730  }
4731 
4733  {
4734  return op2();
4735  }
4736 
4737  const exprt &where() const
4738  {
4739  return op2();
4740  }
4741 };
4742 
4753 inline const let_exprt &to_let_expr(const exprt &expr)
4754 {
4755  PRECONDITION(expr.id()==ID_let);
4756  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
4757  return static_cast<const let_exprt &>(expr);
4758 }
4759 
4764 {
4765  PRECONDITION(expr.id()==ID_let);
4766  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
4767  return static_cast<let_exprt &>(expr);
4768 }
4769 
4770 template<> inline bool can_cast_expr<let_exprt>(const exprt &base)
4771 {
4772  return base.id()==ID_let;
4773 }
4774 inline void validate_expr(const let_exprt &value)
4775 {
4776  validate_operands(value, 3, "Let must have three operands");
4777 }
4778 
4782 {
4783 public:
4785  {
4786  op0()=symbol_exprt();
4787  }
4788 
4790  const irep_idt &_id,
4791  const symbol_exprt &_symbol,
4792  const exprt &_where)
4793  : binary_predicate_exprt(_symbol, _id, _where)
4794  {
4795  }
4796 
4798  {
4799  return static_cast<symbol_exprt &>(op0());
4800  }
4801 
4802  const symbol_exprt &symbol() const
4803  {
4804  return static_cast<const symbol_exprt &>(op0());
4805  }
4806 
4808  {
4809  return op1();
4810  }
4811 
4812  const exprt &where() const
4813  {
4814  return op1();
4815  }
4816 };
4817 
4828 inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
4829 {
4830  DATA_INVARIANT(expr.operands().size()==2,
4831  "quantifier expressions must have two operands");
4832  return static_cast<const quantifier_exprt &>(expr);
4833 }
4834 
4839 {
4840  DATA_INVARIANT(expr.operands().size()==2,
4841  "quantifier expressions must have two operands");
4842  return static_cast<quantifier_exprt &>(expr);
4843 }
4844 
4845 template<> inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
4846 {
4847  return base.id() == ID_forall || base.id() == ID_exists;
4848 }
4849 
4850 inline void validate_expr(const quantifier_exprt &value)
4851 {
4852  validate_operands(value, 2,
4853  "quantifier expressions must have two operands");
4854 }
4855 
4859 {
4860 public:
4862  {
4863  }
4864 
4865  forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
4866  : quantifier_exprt(ID_forall, _symbol, _where)
4867  {
4868  }
4869 };
4870 
4874 {
4875 public:
4877  {
4878  }
4879 
4880  exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
4881  : quantifier_exprt(ID_exists, _symbol, _where)
4882  {
4883  }
4884 };
4885 
4889 {
4890 public:
4891  popcount_exprt(): unary_exprt(ID_popcount)
4892  {
4893  }
4894 
4895  popcount_exprt(const exprt &_op, const typet &_type)
4896  : unary_exprt(ID_popcount, _op, _type)
4897  {
4898  }
4899 
4900  explicit popcount_exprt(const exprt &_op)
4901  : unary_exprt(ID_popcount, _op, _op.type())
4902  {
4903  }
4904 };
4905 
4916 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
4917 {
4918  PRECONDITION(expr.id() == ID_popcount);
4919  DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand");
4920  return static_cast<const popcount_exprt &>(expr);
4921 }
4922 
4927 {
4928  PRECONDITION(expr.id() == ID_popcount);
4929  DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand");
4930  return static_cast<popcount_exprt &>(expr);
4931 }
4932 
4933 template <>
4934 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
4935 {
4936  return base.id() == ID_popcount;
4937 }
4938 inline void validate_expr(const popcount_exprt &value)
4939 {
4940  validate_operands(value, 1, "popcount must have one operand");
4941 }
4942 
4943 #endif // CPROVER_UTIL_STD_EXPR_H
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
bool can_cast_expr< rem_exprt >(const exprt &base)
Definition: std_expr.h:1229
const irept & get_nil_irep()
Definition: irep.cpp:56
const transt & to_trans_expr(const exprt &expr)
Cast a generic exprt to a transt.
Definition: std_expr.h:57
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:4221
const irep_idt & get_name() const
Definition: std_types.h:182
bitnot_exprt(const exprt &op)
Definition: std_expr.h:2536
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:3760
bool can_cast_expr< bitxor_exprt >(const exprt &base)
Definition: std_expr.h:2688
The type of an expression.
Definition: type.h:22
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2379
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:856
exprt & invar()
Definition: std_expr.h:38
bool can_cast_expr< isnormal_exprt >(const exprt &base)
Definition: std_expr.h:4186
const symbol_exprt & symbol() const
Definition: std_expr.h:3931
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast a generic exprt to a factorial_power_exprt.
Definition: std_expr.h:1320
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:495
Boolean negation.
Definition: std_expr.h:3228
unary_minus_exprt(const exprt &_op, const typet &_type)
Definition: std_expr.h:451
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast a generic exprt to a bswap_exprt.
Definition: std_expr.h:542
exprt & true_case()
Definition: std_expr.h:3393
semantic type conversion
Definition: std_expr.h:2111
or_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:2398
const exprt & rhs() const
Definition: std_expr.h:4347
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1063
binary_exprt(const irep_idt &_id)
Definition: std_expr.h:657
bool can_cast_expr< quantifier_exprt >(const exprt &base)
Definition: std_expr.h:4845
bool can_cast_expr< bitnot_exprt >(const exprt &base)
Definition: std_expr.h:2571
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:609
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const exprt & value() const
Definition: std_expr.h:4727
if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
Definition: std_expr.h:3368
const exprt & lhs() const
Definition: std_expr.h:777
shift_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:2772
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast a generic exprt to a bitand_exprt.
Definition: std_expr.h:2728
const minus_exprt & to_minus_expr(const exprt &expr)
Cast a generic exprt to a minus_exprt.
Definition: std_expr.h:984
application of (mathematical) function
Definition: std_expr.h:4529
binary_predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:737
exprt & object()
Definition: std_expr.h:3178
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:253
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4865
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2164
index_exprt(const exprt &_array, const exprt &_index)
Definition: std_expr.h:1473
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
Definition: std_expr.h:1158
ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:4263
boolean OR
Definition: std_expr.h:2391
bool can_cast_expr< transt >(const exprt &base)
Definition: std_expr.h:78
exprt & op0()
Definition: expr.h:72
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:678
const exprt & src() const
Definition: std_expr.h:3016
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
Definition: std_expr.h:1100
complex_exprt(const complex_typet &_type)
Definition: std_expr.h:1868
const plus_exprt & to_plus_expr(const exprt &expr)
Cast a generic exprt to a plus_exprt.
Definition: std_expr.h:926
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
Definition: std_expr.h:2076
Operator to update elements in structs and arrays.
Definition: std_expr.h:3670
const exprt & op() const
Definition: std_expr.h:340
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: std_expr.h:4674
const exprt & pointer() const
Definition: std_expr.h:3310
Evaluates to true if the operand is infinite.
Definition: std_expr.h:4038
const exprt & op() const
Definition: std_expr.h:2940
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
Definition: std_expr.h:1640
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:166
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3538
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
Definition: std_expr.h:2267
unsigned int get_instance() const
Definition: std_expr.cpp:43
exprt & struct_op()
Definition: std_expr.h:3915
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast a generic exprt to a bitxor_exprt.
Definition: std_expr.h:2667
const exprt & real() const
Definition: std_expr.h:1884
const exprt & array() const
Definition: std_expr.h:1491
bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
Definition: std_expr.h:509
unary_predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:616
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1605
const irep_idt & get_identifier() const
Definition: std_expr.h:128
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
Definition: std_expr.h:2403
exprt::operandst & designator()
Definition: std_expr.h:3708
exprt & lower()
Definition: std_expr.h:3104
shift_exprt(const irep_idt &_id)
Definition: std_expr.h:2768
exprt imag()
Definition: std_expr.h:1889
const irep_idt & get_value() const
Definition: std_expr.h:4439
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
Definition: std_expr.h:2000
The null pointer constant.
Definition: std_expr.h:4518
argumentst & arguments()
Definition: std_expr.h:4562
An expression denoting a type.
Definition: std_expr.h:4408
abs_exprt(const exprt &_op)
Definition: std_expr.h:395
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:3658
type_exprt(const typet &type)
Definition: std_expr.h:4415
plus_exprt(const exprt &_lhs, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:907
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast a generic exprt to a bitor_exprt.
Definition: std_expr.h:2607
A transition system, consisting of state invariant, initial state predicate, and transition predicate...
Definition: std_expr.h:29
bool is_thread_local() const
Definition: std_expr.h:184
const exprt & root_object() const
Definition: std_expr.h:1966
exprt real()
Definition: std_expr.h:1879
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
std::size_t get_component_number() const
Definition: std_expr.h:3903
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:4146
exprt & old()
Definition: std_expr.h:3476
if_exprt()
Definition: std_expr.h:3378
exprt & new_value()
Definition: std_expr.h:3496
typet & type()
Definition: expr.h:56
const symbol_exprt & symbol() const
Definition: std_expr.h:4802
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
Definition: std_expr.h:1341
bool can_cast_expr< extractbit_exprt >(const exprt &base)
Definition: std_expr.h:3058
const or_exprt & to_or_expr(const exprt &expr)
Cast a generic exprt to a or_exprt.
Definition: std_expr.h:2442
bool can_cast_expr< bitand_exprt >(const exprt &base)
Definition: std_expr.h:2749
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3199
const exprt & where() const
Definition: std_expr.h:4812
The proper Booleans.
Definition: std_types.h:34
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1672
const exprt & where() const
Definition: std_expr.h:3491
A constant literal expression.
Definition: std_expr.h:4422
exprt & distance()
Definition: std_expr.h:2797
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1175
exprt & rounding_mode()
Definition: std_expr.h:4352
function_application_exprt(const symbol_exprt &_function, const typet &_type)
Definition: std_expr.h:4543
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2327
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:3602
const exprt & index() const
Definition: std_expr.h:1501
symbol_exprt(const typet &type)
Constructor.
Definition: std_expr.h:108
const exprt & lower() const
Definition: std_expr.h:3119
const exprt & where() const
Definition: std_expr.h:4737
irep_idt get_component_name() const
Definition: std_expr.h:3621
index_exprt(const typet &_type)
Definition: std_expr.h:1469
boolean implication
Definition: std_expr.h:2339
bool value_is_zero_string() const
Definition: std_expr.cpp:18
exponentiation
Definition: std_expr.h:1241
void set_bits_per_byte(std::size_t bits_per_byte)
Definition: std_expr.h:526
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:4279
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
Definition: std_expr.h:4753
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:206
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1766
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const exprt &_rm)
Definition: std_expr.h:4322
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3326
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
Definition: std_expr.h:2409
vector_exprt(const vector_typet &_type)
Definition: std_expr.h:1691
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Definition: std_expr.h:4243
plus_exprt()
Definition: std_expr.h:896
Extract member of struct or union.
Definition: std_expr.h:3869
const exprt & imag() const
Definition: std_expr.h:1894
const exprt & rounding_mode() const
Definition: std_expr.h:2205
extractbits_exprt(const exprt &_src, const exprt &_upper, const exprt &_lower, const typet &_type)
Definition: std_expr.h:3079
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:3269
exprt & where()
Definition: std_expr.h:4732
void set_instance(unsigned int instance)
Definition: std_expr.cpp:38
Concatenation of bit-vector operands.
Definition: std_expr.h:4623
equality
Definition: std_expr.h:1354
symbol_exprt & symbol()
Definition: std_expr.h:4797
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast a generic exprt to an notequal_exprt.
Definition: std_expr.h:1429
bool can_cast_expr< bitor_exprt >(const exprt &base)
Definition: std_expr.h:2628
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:947
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1121
const exprt & op() const
Definition: std_expr.h:2792
Templated functions to cast to specific exprt-derived classes.
update_exprt(const typet &_type)
Definition: std_expr.h:3682
constant_exprt(const irep_idt &_value, const typet &_type)
Definition: std_expr.h:4433
const implies_exprt & to_implies_expr(const exprt &expr)
Cast a generic exprt to a implies_exprt.
Definition: std_expr.h:2362
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3898
bool can_cast_expr< function_application_exprt >(const exprt &base)
Definition: std_expr.h:4606
binary_predicate_exprt(const exprt &_op0, const irep_idt &_id, const exprt &_op1)
Definition: std_expr.h:742
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:4373
exprt conjunction(const exprt::operandst &)
Definition: std_expr.cpp:48
const exprt & compound() const
Definition: std_expr.h:3920
replication_exprt(const typet &_type)
Definition: std_expr.h:2915
exprt & op()
Definition: std_expr.h:345
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:669
bswap_exprt(const exprt &_op, std::size_t bits_per_byte)
Definition: std_expr.h:515
decorated_symbol_exprt(const irep_idt &identifier)
Constructor.
Definition: std_expr.h:146
if_exprt(const exprt &cond, const exprt &t, const exprt &f)
Definition: std_expr.h:3362
const exprt & src() const
Definition: std_expr.h:3109
const irep_idt & id() const
Definition: irep.h:259
unary_exprt(const irep_idt &_id)
Definition: std_expr.h:311
dereference_exprt(const exprt &op, const typet &type)
Definition: std_expr.h:3300
popcount_exprt(const exprt &_op)
Definition: std_expr.h:4900
void set_value(const irep_idt &value)
Definition: std_expr.h:4444
const exprt & times() const
Definition: std_expr.h:2930
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3986
Bit-wise OR.
Definition: std_expr.h:2583
bool can_cast_expr< isnan_exprt >(const exprt &base)
Definition: std_expr.h:4026
An expression denoting infinity.
Definition: std_expr.h:4692
shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance)
Definition: std_expr.h:2777
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:1005
The boolean constant true.
Definition: std_expr.h:4486
unary_exprt(const irep_idt &_id, const exprt &_op, const typet &_type)
Definition: std_expr.h:331
Expression to hold a symbol (variable)
Definition: std_expr.h:136
division (integer and real)
Definition: std_expr.h:1075
binary_relation_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:764
const replication_exprt & to_replication_expr(const exprt &expr)
Cast a generic exprt to a replication_exprt.
Definition: std_expr.h:2956
A generic base class for binary expressions.
Definition: std_expr.h:649
function_application_exprt(const typet &_type)
Definition: std_expr.h:4537
const exprt & invar() const
Definition: std_expr.h:42
decorated_symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
Definition: std_expr.h:163
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast a generic exprt to a concatenation_exprt.
Definition: std_expr.h:4653
exprt & init()
Definition: std_expr.h:39
exprt & old()
Definition: std_expr.h:3694
const exprt & distance() const
Definition: std_expr.h:2802
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
Definition: std_expr.h:3739
exprt & times()
Definition: std_expr.h:2925
const irep_idt & get_identifier() const
Definition: std_expr.h:258
const vector_exprt & to_vector_expr(const exprt &expr)
Cast a generic exprt to an vector_exprt.
Definition: std_expr.h:1707
exprt::operandst argumentst
Definition: std_expr.h:4560
The NIL expression.
Definition: std_expr.h:4508
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:121
unary_minus_exprt(const exprt &_op)
Definition: std_expr.h:458
The pointer type.
Definition: std_types.h:1435
IEEE floating-point disequality.
Definition: std_expr.h:4255
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:3974
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
Definition: std_expr.h:3037
member_exprt(const exprt &op, const struct_typet::componentt &c)
Definition: std_expr.h:3881
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1722
Operator to dereference a pointer.
Definition: std_expr.h:3282
exprt & rounding_mode()
Definition: std_expr.h:2200
A constant-size array type.
Definition: std_types.h:1638
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:291
exprt & src()
Definition: std_expr.h:3094
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
Definition: std_expr.h:1584
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:1931
union constructor from single element
Definition: std_expr.h:1730
std::size_t get_component_number() const
Definition: std_expr.h:1761
boolean AND
Definition: std_expr.h:2255
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3070
factorial_power_exprt(const exprt &_base, const exprt &_exp)
Definition: std_expr.h:1302
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:721
const exprt & new_value() const
Definition: std_expr.h:3723
popcount_exprt(const exprt &_op, const typet &_type)
Definition: std_expr.h:4895
not_exprt(const exprt &op)
Definition: std_expr.h:3231
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast a generic exprt to a isinf_exprt.
Definition: std_expr.h:4061
exprt & op1()
Definition: expr.h:75
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
Definition: std_expr.h:4583
const exprt & lhs() const
Definition: std_expr.h:4337
and_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:2262
binary_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:662
Generic base class for unary expressions.
Definition: std_expr.h:303
inequality
Definition: std_expr.h:1406
TO_BE_DOCUMENTED.
Definition: namespace.h:74
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:847
infinity_exprt(const typet &_type)
Definition: std_expr.h:4695
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:2023
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1803
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast a generic exprt to an extractbits_exprt.
Definition: std_expr.h:3135
Left shift.
Definition: std_expr.h:2848
const exprt & what() const
Definition: std_expr.h:1568
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast a generic exprt to a binary_relation_exprt.
Definition: std_expr.h:803
predicate_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:590
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:316
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const exprt & false_case() const
Definition: std_expr.h:3408
typecast_exprt(const typet &_type)
Definition: std_expr.h:2114
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: std_expr.h:3156
lshr_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2900
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
const exprt & cond() const
Definition: std_expr.h:3388
A forall expression.
Definition: std_expr.h:4858
with_exprt(const exprt &_old, const exprt &_where, const exprt &_new_value)
Definition: std_expr.h:3462
The plus expression.
Definition: std_expr.h:893
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:4478
symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
Definition: std_expr.h:116
const symbol_exprt & symbol() const
Definition: std_expr.h:4717
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
Definition: std_expr.h:2243
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
symbol_exprt(const irep_idt &identifier)
Constructor.
Definition: std_expr.h:100
null_pointer_exprt(const pointer_typet &type)
Definition: std_expr.h:4521
ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:4205
predicate_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:597
exprt & where()
Definition: std_expr.h:4807
void set_static_lifetime()
Definition: std_expr.h:174
array constructor from single element
Definition: std_expr.h:1550
exprt & upper()
Definition: std_expr.h:3099
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast a generic exprt to a quantifier_exprt.
Definition: std_expr.h:4828
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2513
multi_ary_exprt(const irep_idt &_id)
Definition: std_expr.h:837
exprt disjunction(const exprt::operandst &)
Definition: std_expr.cpp:24
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:432
power_exprt(const exprt &_base, const exprt &_exp)
Definition: std_expr.h:1248
isfinite_exprt(const exprt &op)
Definition: std_expr.h:4097
Logical right shift.
Definition: std_expr.h:2888
exprt & compound()
Definition: std_expr.h:3925
const index_designatort & to_index_designator(const exprt &expr)
Cast a generic exprt to an index_designatort.
Definition: std_expr.h:3581
vector constructor from list of elements
Definition: std_expr.h:1684
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const exprt & old() const
Definition: std_expr.h:3481
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast a generic exprt to a isfinite_exprt.
Definition: std_expr.h:4117
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:2463
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: std_expr.h:3347
Operator to return the address of an object.
Definition: std_expr.h:3168
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1838
The unary minus expression.
Definition: std_expr.h:444
transt()
Definition: std_expr.h:32
exprt & false_case()
Definition: std_expr.h:3403
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: std_expr.h:2098
concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
Definition: std_expr.h:4635
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
implies_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:2346
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:585
union_exprt(const irep_idt &_component_name, const exprt &_value, const typet &_type)
Definition: std_expr.h:1742
member_exprt(const exprt &op, const irep_idt &component_name, const typet &_type)
Definition: std_expr.h:3872
quantifier_exprt(const irep_idt &_id, const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4789
bool has_operands() const
Definition: expr.h:63
const exprt & index() const
Definition: std_expr.h:3560
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:3216
The boolean constant false.
Definition: std_expr.h:4497
or_exprt()
Definition: std_expr.h:2394
const exprt & init() const
Definition: std_expr.h:43
bool can_cast_expr< replication_exprt >(const exprt &base)
Definition: std_expr.h:2977
exprt & index()
Definition: std_expr.h:3011
const exprt & rhs() const
Definition: std_expr.h:787
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast a generic exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2221
exprt & trans()
Definition: std_expr.h:40
decorated_symbol_exprt(const typet &type)
Constructor.
Definition: std_expr.h:154
equal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1361
void validate_expr(const transt &value)
Definition: std_expr.h:82
const exprt & trans() const
Definition: std_expr.h:44
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2124
const xor_exprt & to_xor_expr(const exprt &expr)
Cast a generic exprt to a xor_exprt.
Definition: std_expr.h:2498
std::vector< exprt > operandst
Definition: expr.h:45
binary multiplication
Definition: std_expr.h:1017
const exprt::operandst & designator() const
Definition: std_expr.h:3713
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: std_expr.h:4302
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1450
constant_exprt(const typet &type)
Definition: std_expr.h:4429
const mult_exprt & to_mult_expr(const exprt &expr)
Cast a generic exprt to a mult_exprt.
Definition: std_expr.h:1042
const exprt & object() const
Definition: std_expr.h:1961
multi_ary_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:841
const power_exprt & to_power_expr(const exprt &expr)
Cast a generic exprt to a power_exprt.
Definition: std_expr.h:1266
minus_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:966
Boolean XOR.
Definition: std_expr.h:2475
index_designatort(const exprt &_index)
Definition: std_expr.h:3554
Complex numbers made of pair of given subtype.
Definition: std_types.h:1686
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast a generic exprt to a popcount_exprt.
Definition: std_expr.h:4916
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:3517
Bit-wise XOR.
Definition: std_expr.h:2644
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast a generic exprt to a multi_ary_exprt.
Definition: std_expr.h:877
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1377
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:227
dynamic_object_exprt(const typet &type)
Definition: std_expr.h:2044
API to type classes.
typecast_exprt(const exprt &op, const typet &_type)
Definition: std_expr.h:2118
const exprt & old() const
Definition: std_expr.h:3699
const exprt & object() const
Definition: std_expr.h:3183
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast a generic exprt to a isnan_exprt.
Definition: std_expr.h:4009
unary_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:324
plus_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:900
update_exprt(const exprt &_old, const exprt &_designator, const exprt &_new_value)
Definition: std_expr.h:3673
exprt & value()
Definition: std_expr.h:4722
Expression to hold a nondeterministic choice.
Definition: std_expr.h:239
bitand_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2711
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Definition: std_expr.h:2818
const and_exprt & to_and_expr(const exprt &expr)
Cast a generic exprt to a and_exprt.
Definition: std_expr.h:2306
exprt & index()
Definition: std_expr.h:1496
shl_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2855
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4888
const rem_exprt & to_rem_expr(const exprt &expr)
Cast a generic exprt to a rem_exprt.
Definition: std_expr.h:1212
Evaluates to true if the operand is finite.
Definition: std_expr.h:4094
const exprt & index() const
Definition: std_expr.h:3021
concatenation_exprt(const typet &_type)
Definition: std_expr.h:4630
ashr_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2875
exprt & op()
Definition: std_expr.h:2787
std::size_t get_bits_per_byte() const
Definition: std_expr.h:521
xor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2482
binary_relation_exprt(const irep_idt &id)
Definition: std_expr.h:759
semantic type conversion from/to floating-point formats
Definition: std_expr.h:2176
div_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1082
shl_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2860
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3305
absolute value
Definition: std_expr.h:388
sign of an expression
Definition: std_expr.h:634
floatbv_typecast_exprt(const exprt &op, const exprt &rounding, const typet &_type)
Definition: std_expr.h:2183
const exprt & struct_op() const
Definition: std_expr.h:3909
const exprt & rounding_mode() const
Definition: std_expr.h:4357
isnormal_exprt(const exprt &op)
Definition: std_expr.h:4149
nondet_symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
Definition: std_expr.h:246
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:822
dereference_exprt(const exprt &op)
Definition: std_expr.h:3294
const complex_exprt & to_complex_expr(const exprt &expr)
Cast a generic exprt to a complex_exprt.
Definition: std_expr.h:1910
sign_exprt()
Definition: std_expr.h:637
dereference_exprt(const typet &type)
Definition: std_expr.h:3289
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1782
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast a generic exprt to a factorial_power_exprt.
Definition: std_expr.h:1332
Operator to update elements in structs and arrays.
Definition: std_expr.h:3459
const exprt & upper() const
Definition: std_expr.h:3114
sign_exprt(const exprt &_op)
Definition: std_expr.h:641
A base class for quantifier expressions.
Definition: std_expr.h:4781
lshr_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2895
unary_predicate_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:621
irep_idt get_component_name() const
Definition: std_expr.h:3893
const exprt & offset() const
Definition: std_expr.h:1984
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
abs_exprt()
Definition: std_expr.h:391
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:4770
rem_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1194
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
Definition: std_expr.h:3252
remainder of division
Definition: std_expr.h:1187
const exprt & valid() const
Definition: std_expr.h:2060
bitor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2590
const exprt & true_case() const
Definition: std_expr.h:3398
exprt & index()
Definition: std_expr.h:3565
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:123
array_exprt(const array_typet &_type)
Definition: std_expr.h:1624
exprt & op()
Definition: std_expr.h:2935
irep_idt get_component_name() const
Definition: std_expr.h:1751
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:380
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1756
const abs_exprt & to_abs_expr(const exprt &expr)
Cast a generic exprt to a abs_exprt.
Definition: std_expr.h:411
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
Definition: std_expr.h:2273
bool is_static_lifetime() const
Definition: std_expr.h:169
isinf_exprt(const exprt &op)
Definition: std_expr.h:4041
arrays with given size
Definition: std_types.h:1013
bool can_cast_expr< bswap_exprt >(const exprt &base)
Definition: std_expr.h:564
binary minus
Definition: std_expr.h:959
Bit-wise AND.
Definition: std_expr.h:2704
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4880
isnan_exprt(const exprt &op)
Definition: std_expr.h:3989
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: std_expr.h:4082
exprt & what()
Definition: std_expr.h:1563
exprt & op2()
Definition: expr.h:78
symbol_exprt()
Definition: std_expr.h:93
bool can_cast_expr< power_exprt >(const exprt &base)
Definition: std_expr.h:1283
ashr_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2880
bool can_cast_expr< isfinite_exprt >(const exprt &base)
Definition: std_expr.h:4134
exprt & new_value()
Definition: std_expr.h:3718
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1853
replication_exprt(const exprt &_times, const exprt &_src)
Definition: std_expr.h:2920
symbol_exprt & symbol()
Definition: std_expr.h:4712
const binary_exprt & to_binary_expr(const exprt &expr)
Cast a generic exprt to a binary_exprt.
Definition: std_expr.h:702
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:730
Arithmetic right shift.
Definition: std_expr.h:2868
struct_exprt(const typet &_type)
Definition: std_expr.h:1822
An exists expression.
Definition: std_expr.h:4873
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1538
exprt & where()
Definition: std_expr.h:3486
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast a generic exprt to a bitnot_exprt.
Definition: std_expr.h:2552
A let expression.
Definition: std_expr.h:4703
void clear_static_lifetime()
Definition: std_expr.h:179
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast a generic exprt to a isnormal_exprt.
Definition: std_expr.h:4169
TO_BE_DOCUMENTED.
Definition: std_expr.h:2035
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast a generic exprt to a nondet_symbol_exprt.
Definition: std_expr.h:274
A generic base class for multi-ary expressions.
Definition: std_expr.h:830
const unary_exprt & to_unary_expr(const exprt &expr)
Cast a generic exprt to a unary_exprt.
Definition: std_expr.h:361
operandst & operands()
Definition: expr.h:66
mult_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1024
mod_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1140
exprt & src()
Definition: std_expr.h:3006
bitxor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2651
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2529
index_exprt(const exprt &_array, const exprt &_index, const typet &_type)
Definition: std_expr.h:1478
struct constructor from list of elements
Definition: std_expr.h:1815
extractbit_exprt(const exprt &_src, const exprt &_index)
Definition: std_expr.h:2996
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:3445
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
falling factorial power
Definition: std_expr.h:1295
union_exprt(const typet &_type)
Definition: std_expr.h:1737
notequal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1413
complex_exprt(const exprt &_real, const exprt &_imag, const complex_typet &_type)
Definition: std_expr.h:1873
IEEE floating-point operations.
Definition: std_expr.h:4314
Bit-vector replication.
Definition: std_expr.h:2908
exprt & array()
Definition: std_expr.h:1486
quantifier_exprt(const irep_idt &_id)
Definition: std_expr.h:4784
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
array_list_exprt(const array_typet &_type)
Definition: std_expr.h:1665
A base class for shift operators.
Definition: std_expr.h:2765
const argumentst & arguments() const
Definition: std_expr.h:4567
array constructor from list of elements
Definition: std_expr.h:1617
complex constructor from a pair of numbers
Definition: std_expr.h:1861
binary modulo
Definition: std_expr.h:1133
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1655
The byte swap expression.
Definition: std_expr.h:506
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast a generic exprt to a unary_minus_exprt.
Definition: std_expr.h:474
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:3615
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: std_expr.h:4934
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
Definition: std_expr.h:1662
array_of_exprt(const exprt &_what, const array_typet &_type)
Definition: std_expr.h:1557
const member_designatort & to_member_designator(const exprt &expr)
Cast a generic exprt to an member_designatort.
Definition: std_expr.h:3637
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2989
A generic base class for expressions that are predicates, i.e., boolean-typed.
Definition: std_expr.h:578
IEEE-floating-point equality.
Definition: std_expr.h:4198
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1394
array index operator
Definition: std_expr.h:1462
exprt & op3()
Definition: expr.h:81
address_of_exprt(const exprt &op, const pointer_typet &_type)
Definition: std_expr.h:3173
const exprt & new_value() const
Definition: std_expr.h:3501
const exprt & op() const
Definition: std_expr.h:2195