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 
2925  replication_exprt(const unsigned _times, const exprt &_src);
2926 
2928  {
2929  return op0();
2930  }
2931 
2932  const exprt &times() const
2933  {
2934  return op0();
2935  }
2936 
2938  {
2939  return op1();
2940  }
2941 
2942  const exprt &op() const
2943  {
2944  return op1();
2945  }
2946 };
2947 
2958 inline const replication_exprt &to_replication_expr(const exprt &expr)
2959 {
2960  PRECONDITION(expr.id()==ID_replication);
2962  expr.operands().size()==2,
2963  "Bit-wise replication must have two operands");
2964  return static_cast<const replication_exprt &>(expr);
2965 }
2966 
2971 {
2972  PRECONDITION(expr.id()==ID_replication);
2974  expr.operands().size()==2,
2975  "Bit-wise replication must have two operands");
2976  return static_cast<replication_exprt &>(expr);
2977 }
2978 
2979 template<> inline bool can_cast_expr<replication_exprt>(const exprt &base)
2980 {
2981  return base.id()==ID_replication;
2982 }
2983 inline void validate_expr(const replication_exprt &value)
2984 {
2985  validate_operands(value, 2, "Bit-wise replication must have two operands");
2986 }
2987 
2988 
2992 {
2993 public:
2995  {
2996  }
2997 
2999  const exprt &_src,
3000  const exprt &_index):binary_predicate_exprt(_src, ID_extractbit, _index)
3001  {
3002  }
3003 
3005  const exprt &_src,
3006  const std::size_t _index);
3007 
3009  {
3010  return op0();
3011  }
3012 
3014  {
3015  return op1();
3016  }
3017 
3018  const exprt &src() const
3019  {
3020  return op0();
3021  }
3022 
3023  const exprt &index() const
3024  {
3025  return op1();
3026  }
3027 };
3028 
3039 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
3040 {
3041  PRECONDITION(expr.id()==ID_extractbit);
3043  expr.operands().size()==2,
3044  "Extract bit must have two operands");
3045  return static_cast<const extractbit_exprt &>(expr);
3046 }
3047 
3052 {
3053  PRECONDITION(expr.id()==ID_extractbit);
3055  expr.operands().size()==2,
3056  "Extract bit must have two operands");
3057  return static_cast<extractbit_exprt &>(expr);
3058 }
3059 
3060 template<> inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
3061 {
3062  return base.id()==ID_extractbit;
3063 }
3064 inline void validate_expr(const extractbit_exprt &value)
3065 {
3066  validate_operands(value, 2, "Extract bit must have two operands");
3067 }
3068 
3069 
3073 {
3074 public:
3075  extractbits_exprt():exprt(ID_extractbits)
3076  {
3077  operands().resize(3);
3078  }
3079 
3080  // the ordering upper-lower matches the SMT-LIB
3082  const exprt &_src,
3083  const exprt &_upper,
3084  const exprt &_lower,
3085  const typet &_type):exprt(ID_extractbits, _type)
3086  {
3087  copy_to_operands(_src, _upper, _lower);
3088  }
3089 
3091  const exprt &_src,
3092  const std::size_t _upper,
3093  const std::size_t _lower,
3094  const typet &_type);
3095 
3097  {
3098  return op0();
3099  }
3100 
3102  {
3103  return op1();
3104  }
3105 
3107  {
3108  return op2();
3109  }
3110 
3111  const exprt &src() const
3112  {
3113  return op0();
3114  }
3115 
3116  const exprt &upper() const
3117  {
3118  return op1();
3119  }
3120 
3121  const exprt &lower() const
3122  {
3123  return op2();
3124  }
3125 };
3126 
3137 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
3138 {
3139  PRECONDITION(expr.id()==ID_extractbits);
3141  expr.operands().size()==3,
3142  "Extract bits must have three operands");
3143  return static_cast<const extractbits_exprt &>(expr);
3144 }
3145 
3150 {
3151  PRECONDITION(expr.id()==ID_extractbits);
3153  expr.operands().size()==3,
3154  "Extract bits must have three operands");
3155  return static_cast<extractbits_exprt &>(expr);
3156 }
3157 
3158 template<> inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
3159 {
3160  return base.id()==ID_extractbits;
3161 }
3162 inline void validate_expr(const extractbits_exprt &value)
3163 {
3164  validate_operands(value, 3, "Extract bits must have three operands");
3165 }
3166 
3167 
3171 {
3172 public:
3173  explicit address_of_exprt(const exprt &op);
3174 
3175  address_of_exprt(const exprt &op, const pointer_typet &_type):
3176  unary_exprt(ID_address_of, op, _type)
3177  {
3178  }
3179 
3181  {
3182  return op0();
3183  }
3184 
3185  const exprt &object() const
3186  {
3187  return op0();
3188  }
3189 };
3190 
3201 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
3202 {
3203  PRECONDITION(expr.id()==ID_address_of);
3204  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
3205  return static_cast<const address_of_exprt &>(expr);
3206 }
3207 
3212 {
3213  PRECONDITION(expr.id()==ID_address_of);
3214  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
3215  return static_cast<address_of_exprt &>(expr);
3216 }
3217 
3218 template<> inline bool can_cast_expr<address_of_exprt>(const exprt &base)
3219 {
3220  return base.id()==ID_address_of;
3221 }
3222 inline void validate_expr(const address_of_exprt &value)
3223 {
3224  validate_operands(value, 1, "Address of must have one operand");
3225 }
3226 
3227 
3231 {
3232 public:
3233  explicit not_exprt(const exprt &op):
3234  unary_exprt(ID_not, op) // type from op.type()
3235  {
3236  PRECONDITION(op.type().id()==ID_bool);
3237  }
3238 
3240  {
3241  }
3242 };
3243 
3254 inline const not_exprt &to_not_expr(const exprt &expr)
3255 {
3256  PRECONDITION(expr.id()==ID_not);
3257  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
3258  return static_cast<const not_exprt &>(expr);
3259 }
3260 
3265 {
3266  PRECONDITION(expr.id()==ID_not);
3267  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
3268  return static_cast<not_exprt &>(expr);
3269 }
3270 
3271 template<> inline bool can_cast_expr<not_exprt>(const exprt &base)
3272 {
3273  return base.id()==ID_not;
3274 }
3275 
3276 inline void validate_expr(const not_exprt &value)
3277 {
3278  validate_operands(value, 1, "Not must have one operand");
3279 }
3280 
3281 
3285 {
3286 public:
3287  dereference_exprt():unary_exprt(ID_dereference)
3288  {
3289  }
3290 
3291  explicit dereference_exprt(const typet &type):
3292  unary_exprt(ID_dereference, type)
3293  {
3294  }
3295 
3296  explicit dereference_exprt(const exprt &op):
3297  unary_exprt(ID_dereference, op, op.type().subtype())
3298  {
3299  PRECONDITION(op.type().id()==ID_pointer);
3300  }
3301 
3303  unary_exprt(ID_dereference, op, type)
3304  {
3305  }
3306 
3308  {
3309  return op0();
3310  }
3311 
3312  const exprt &pointer() const
3313  {
3314  return op0();
3315  }
3316 };
3317 
3328 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
3329 {
3330  PRECONDITION(expr.id()==ID_dereference);
3332  expr.operands().size()==1,
3333  "Dereference must have one operand");
3334  return static_cast<const dereference_exprt &>(expr);
3335 }
3336 
3341 {
3342  PRECONDITION(expr.id()==ID_dereference);
3344  expr.operands().size()==1,
3345  "Dereference must have one operand");
3346  return static_cast<dereference_exprt &>(expr);
3347 }
3348 
3349 template<> inline bool can_cast_expr<dereference_exprt>(const exprt &base)
3350 {
3351  return base.id()==ID_dereference;
3352 }
3353 inline void validate_expr(const dereference_exprt &value)
3354 {
3355  validate_operands(value, 1, "Dereference must have one operand");
3356 }
3357 
3358 
3361 class if_exprt:public exprt
3362 {
3363 public:
3364  if_exprt(const exprt &cond, const exprt &t, const exprt &f):
3365  exprt(ID_if, t.type())
3366  {
3367  copy_to_operands(cond, t, f);
3368  }
3369 
3371  const exprt &cond,
3372  const exprt &t,
3373  const exprt &f,
3374  const typet &type):
3375  exprt(ID_if, type)
3376  {
3377  copy_to_operands(cond, t, f);
3378  }
3379 
3380  if_exprt():exprt(ID_if)
3381  {
3382  operands().resize(3);
3383  }
3384 
3386  {
3387  return op0();
3388  }
3389 
3390  const exprt &cond() const
3391  {
3392  return op0();
3393  }
3394 
3396  {
3397  return op1();
3398  }
3399 
3400  const exprt &true_case() const
3401  {
3402  return op1();
3403  }
3404 
3406  {
3407  return op2();
3408  }
3409 
3410  const exprt &false_case() const
3411  {
3412  return op2();
3413  }
3414 };
3415 
3426 inline const if_exprt &to_if_expr(const exprt &expr)
3427 {
3428  PRECONDITION(expr.id()==ID_if);
3430  expr.operands().size()==3,
3431  "If-then-else must have three operands");
3432  return static_cast<const if_exprt &>(expr);
3433 }
3434 
3438 inline if_exprt &to_if_expr(exprt &expr)
3439 {
3440  PRECONDITION(expr.id()==ID_if);
3442  expr.operands().size()==3,
3443  "If-then-else must have three operands");
3444  return static_cast<if_exprt &>(expr);
3445 }
3446 
3447 template<> inline bool can_cast_expr<if_exprt>(const exprt &base)
3448 {
3449  return base.id()==ID_if;
3450 }
3451 inline void validate_expr(const if_exprt &value)
3452 {
3453  validate_operands(value, 3, "If-then-else must have three operands");
3454 }
3455 
3456 
3461 class with_exprt:public exprt
3462 {
3463 public:
3465  const exprt &_old,
3466  const exprt &_where,
3467  const exprt &_new_value):
3468  exprt(ID_with, _old.type())
3469  {
3470  copy_to_operands(_old, _where, _new_value);
3471  }
3472 
3473  with_exprt():exprt(ID_with)
3474  {
3475  operands().resize(3);
3476  }
3477 
3479  {
3480  return op0();
3481  }
3482 
3483  const exprt &old() const
3484  {
3485  return op0();
3486  }
3487 
3489  {
3490  return op1();
3491  }
3492 
3493  const exprt &where() const
3494  {
3495  return op1();
3496  }
3497 
3499  {
3500  return op2();
3501  }
3502 
3503  const exprt &new_value() const
3504  {
3505  return op2();
3506  }
3507 };
3508 
3519 inline const with_exprt &to_with_expr(const exprt &expr)
3520 {
3521  PRECONDITION(expr.id()==ID_with);
3523  expr.operands().size()==3,
3524  "Array/structure update must have three operands");
3525  return static_cast<const with_exprt &>(expr);
3526 }
3527 
3532 {
3533  PRECONDITION(expr.id()==ID_with);
3535  expr.operands().size()==3,
3536  "Array/structure update must have three operands");
3537  return static_cast<with_exprt &>(expr);
3538 }
3539 
3540 template<> inline bool can_cast_expr<with_exprt>(const exprt &base)
3541 {
3542  return base.id()==ID_with;
3543 }
3544 inline void validate_expr(const with_exprt &value)
3545 {
3547  value,
3548  3,
3549  "Array/structure update must have three operands");
3550 }
3551 
3552 
3554 {
3555 public:
3556  explicit index_designatort(const exprt &_index):
3557  exprt(ID_index_designator)
3558  {
3559  copy_to_operands(_index);
3560  }
3561 
3562  const exprt &index() const
3563  {
3564  return op0();
3565  }
3566 
3568  {
3569  return op0();
3570  }
3571 };
3572 
3583 inline const index_designatort &to_index_designator(const exprt &expr)
3584 {
3585  PRECONDITION(expr.id()==ID_index_designator);
3587  expr.operands().size()==1,
3588  "Index designator must have one operand");
3589  return static_cast<const index_designatort &>(expr);
3590 }
3591 
3596 {
3597  PRECONDITION(expr.id()==ID_index_designator);
3599  expr.operands().size()==1,
3600  "Index designator must have one operand");
3601  return static_cast<index_designatort &>(expr);
3602 }
3603 
3604 template<> inline bool can_cast_expr<index_designatort>(const exprt &base)
3605 {
3606  return base.id()==ID_index_designator;
3607 }
3608 inline void validate_expr(const index_designatort &value)
3609 {
3610  validate_operands(value, 1, "Index designator must have one operand");
3611 }
3612 
3613 
3615 {
3616 public:
3617  explicit member_designatort(const irep_idt &_component_name):
3618  exprt(ID_member_designator)
3619  {
3620  set(ID_component_name, _component_name);
3621  }
3622 
3624  {
3625  return get(ID_component_name);
3626  }
3627 };
3628 
3640 {
3641  PRECONDITION(expr.id()==ID_member_designator);
3643  !expr.has_operands(),
3644  "Member designator must not have operands");
3645  return static_cast<const member_designatort &>(expr);
3646 }
3647 
3652 {
3653  PRECONDITION(expr.id()==ID_member_designator);
3655  !expr.has_operands(),
3656  "Member designator must not have operands");
3657  return static_cast<member_designatort &>(expr);
3658 }
3659 
3660 template<> inline bool can_cast_expr<member_designatort>(const exprt &base)
3661 {
3662  return base.id()==ID_member_designator;
3663 }
3664 inline void validate_expr(const member_designatort &value)
3665 {
3666  validate_operands(value, 0, "Member designator must not have operands");
3667 }
3668 
3669 
3672 class update_exprt:public exprt
3673 {
3674 public:
3676  const exprt &_old,
3677  const exprt &_designator,
3678  const exprt &_new_value):
3679  exprt(ID_update, _old.type())
3680  {
3681  copy_to_operands(_old, _designator, _new_value);
3682  }
3683 
3684  explicit update_exprt(const typet &_type):
3685  exprt(ID_update, _type)
3686  {
3687  operands().resize(3);
3688  }
3689 
3690  update_exprt():exprt(ID_update)
3691  {
3692  operands().resize(3);
3693  op1().id(ID_designator);
3694  }
3695 
3697  {
3698  return op0();
3699  }
3700 
3701  const exprt &old() const
3702  {
3703  return op0();
3704  }
3705 
3706  // the designator operands are either
3707  // 1) member_designator or
3708  // 2) index_designator
3709  // as defined above
3711  {
3712  return op1().operands();
3713  }
3714 
3716  {
3717  return op1().operands();
3718  }
3719 
3721  {
3722  return op2();
3723  }
3724 
3725  const exprt &new_value() const
3726  {
3727  return op2();
3728  }
3729 };
3730 
3741 inline const update_exprt &to_update_expr(const exprt &expr)
3742 {
3743  PRECONDITION(expr.id()==ID_update);
3745  expr.operands().size()==3,
3746  "Array/structure update must have three operands");
3747  return static_cast<const update_exprt &>(expr);
3748 }
3749 
3754 {
3755  PRECONDITION(expr.id()==ID_update);
3757  expr.operands().size()==3,
3758  "Array/structure update must have three operands");
3759  return static_cast<update_exprt &>(expr);
3760 }
3761 
3762 template<> inline bool can_cast_expr<update_exprt>(const exprt &base)
3763 {
3764  return base.id()==ID_update;
3765 }
3766 inline void validate_expr(const update_exprt &value)
3767 {
3769  value,
3770  3,
3771  "Array/structure update must have three operands");
3772 }
3773 
3774 
3775 #if 0
3776 
3778 class array_update_exprt:public exprt
3779 {
3780 public:
3781  array_update_exprt(
3782  const exprt &_array,
3783  const exprt &_index,
3784  const exprt &_new_value):
3785  exprt(ID_array_update, _array.type())
3786  {
3787  copy_to_operands(_array, _index, _new_value);
3788  }
3789 
3790  array_update_exprt():exprt(ID_array_update)
3791  {
3792  operands().resize(3);
3793  }
3794 
3795  exprt &array()
3796  {
3797  return op0();
3798  }
3799 
3800  const exprt &array() const
3801  {
3802  return op0();
3803  }
3804 
3805  exprt &index()
3806  {
3807  return op1();
3808  }
3809 
3810  const exprt &index() const
3811  {
3812  return op1();
3813  }
3814 
3815  exprt &new_value()
3816  {
3817  return op2();
3818  }
3819 
3820  const exprt &new_value() const
3821  {
3822  return op2();
3823  }
3824 };
3825 
3836 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3837 {
3838  PRECONDITION(expr.id()==ID_array_update);
3840  expr.operands().size()==3,
3841  "Array update must have three operands");
3842  return static_cast<const array_update_exprt &>(expr);
3843 }
3844 
3848 inline array_update_exprt &to_array_update_expr(exprt &expr)
3849 {
3850  PRECONDITION(expr.id()==ID_array_update);
3852  expr.operands().size()==3,
3853  "Array update must have three operands");
3854  return static_cast<array_update_exprt &>(expr);
3855 }
3856 
3857 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
3858 {
3859  return base.id()==ID_array_update;
3860 }
3861 inline void validate_expr(const array_update_exprt &value)
3862 {
3863  validate_operands(value, 3, "Array update must have three operands");
3864 }
3865 
3866 #endif
3867 
3868 
3872 {
3873 public:
3875  const exprt &op,
3876  const irep_idt &component_name,
3877  const typet &_type):
3878  unary_exprt(ID_member, op, _type)
3879  {
3880  set_component_name(component_name);
3881  }
3882 
3884  const exprt &op,
3885  const struct_typet::componentt &c):
3886  unary_exprt(ID_member, op, c.type())
3887  {
3889  }
3890 
3892  {
3893  }
3894 
3896  {
3897  return get(ID_component_name);
3898  }
3899 
3900  void set_component_name(const irep_idt &component_name)
3901  {
3902  set(ID_component_name, component_name);
3903  }
3904 
3905  std::size_t get_component_number() const
3906  {
3907  return get_size_t(ID_component_number);
3908  }
3909 
3910  // will go away, use compound()
3911  const exprt &struct_op() const
3912  {
3913  return op0();
3914  }
3915 
3916  // will go away, use compound()
3918  {
3919  return op0();
3920  }
3921 
3922  const exprt &compound() const
3923  {
3924  return op0();
3925  }
3926 
3928  {
3929  return op0();
3930  }
3931 
3932  // Retrieves the object(symbol) this member corresponds to
3933  inline const symbol_exprt &symbol() const
3934  {
3935  const exprt &op=op0();
3936  if(op.id()==ID_member)
3937  {
3938  return static_cast<const member_exprt &>(op).symbol();
3939  }
3940 
3941  return to_symbol_expr(op);
3942  }
3943 };
3944 
3955 inline const member_exprt &to_member_expr(const exprt &expr)
3956 {
3957  PRECONDITION(expr.id()==ID_member);
3959  expr.operands().size()==1,
3960  "Extract member must have one operand");
3961  return static_cast<const member_exprt &>(expr);
3962 }
3963 
3968 {
3969  PRECONDITION(expr.id()==ID_member);
3971  expr.operands().size()==1,
3972  "Extract member must have one operand");
3973  return static_cast<member_exprt &>(expr);
3974 }
3975 
3976 template<> inline bool can_cast_expr<member_exprt>(const exprt &base)
3977 {
3978  return base.id()==ID_member;
3979 }
3980 inline void validate_expr(const member_exprt &value)
3981 {
3982  validate_operands(value, 1, "Extract member must have one operand");
3983 }
3984 
3985 
3989 {
3990 public:
3991  explicit isnan_exprt(const exprt &op):
3992  unary_predicate_exprt(ID_isnan, op)
3993  {
3994  }
3995 
3997  {
3998  }
3999 };
4000 
4011 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
4012 {
4013  PRECONDITION(expr.id()==ID_isnan);
4014  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
4015  return static_cast<const isnan_exprt &>(expr);
4016 }
4017 
4022 {
4023  PRECONDITION(expr.id()==ID_isnan);
4024  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
4025  return static_cast<isnan_exprt &>(expr);
4026 }
4027 
4028 template<> inline bool can_cast_expr<isnan_exprt>(const exprt &base)
4029 {
4030  return base.id()==ID_isnan;
4031 }
4032 inline void validate_expr(const isnan_exprt &value)
4033 {
4034  validate_operands(value, 1, "Is NaN must have one operand");
4035 }
4036 
4037 
4041 {
4042 public:
4043  explicit isinf_exprt(const exprt &op):
4044  unary_predicate_exprt(ID_isinf, op)
4045  {
4046  }
4047 
4049  {
4050  }
4051 };
4052 
4063 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
4064 {
4065  PRECONDITION(expr.id()==ID_isinf);
4067  expr.operands().size()==1,
4068  "Is infinite must have one operand");
4069  return static_cast<const isinf_exprt &>(expr);
4070 }
4071 
4076 {
4077  PRECONDITION(expr.id()==ID_isinf);
4079  expr.operands().size()==1,
4080  "Is infinite must have one operand");
4081  return static_cast<isinf_exprt &>(expr);
4082 }
4083 
4084 template<> inline bool can_cast_expr<isinf_exprt>(const exprt &base)
4085 {
4086  return base.id()==ID_isinf;
4087 }
4088 inline void validate_expr(const isinf_exprt &value)
4089 {
4090  validate_operands(value, 1, "Is infinite must have one operand");
4091 }
4092 
4093 
4097 {
4098 public:
4099  explicit isfinite_exprt(const exprt &op):
4100  unary_predicate_exprt(ID_isfinite, op)
4101  {
4102  }
4103 
4105  {
4106  }
4107 };
4108 
4119 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
4120 {
4121  PRECONDITION(expr.id()==ID_isfinite);
4122  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
4123  return static_cast<const isfinite_exprt &>(expr);
4124 }
4125 
4130 {
4131  PRECONDITION(expr.id()==ID_isfinite);
4132  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
4133  return static_cast<isfinite_exprt &>(expr);
4134 }
4135 
4136 template<> inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
4137 {
4138  return base.id()==ID_isfinite;
4139 }
4140 inline void validate_expr(const isfinite_exprt &value)
4141 {
4142  validate_operands(value, 1, "Is finite must have one operand");
4143 }
4144 
4145 
4149 {
4150 public:
4151  explicit isnormal_exprt(const exprt &op):
4152  unary_predicate_exprt(ID_isnormal, op)
4153  {
4154  }
4155 
4157  {
4158  }
4159 };
4160 
4171 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
4172 {
4173  PRECONDITION(expr.id()==ID_isnormal);
4174  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
4175  return static_cast<const isnormal_exprt &>(expr);
4176 }
4177 
4182 {
4183  PRECONDITION(expr.id()==ID_isnormal);
4184  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
4185  return static_cast<isnormal_exprt &>(expr);
4186 }
4187 
4188 template<> inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
4189 {
4190  return base.id()==ID_isnormal;
4191 }
4192 inline void validate_expr(const isnormal_exprt &value)
4193 {
4194  validate_operands(value, 1, "Is normal must have one operand");
4195 }
4196 
4197 
4201 {
4202 public:
4204  {
4205  }
4206 
4207  ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs):
4208  binary_relation_exprt(_lhs, ID_ieee_float_equal, _rhs)
4209  {
4210  }
4211 };
4212 
4224 {
4225  PRECONDITION(expr.id()==ID_ieee_float_equal);
4227  expr.operands().size()==2,
4228  "IEEE equality must have two operands");
4229  return static_cast<const ieee_float_equal_exprt &>(expr);
4230 }
4231 
4236 {
4237  PRECONDITION(expr.id()==ID_ieee_float_equal);
4239  expr.operands().size()==2,
4240  "IEEE equality must have two operands");
4241  return static_cast<ieee_float_equal_exprt &>(expr);
4242 }
4243 
4244 template<>
4246 {
4247  return base.id()==ID_ieee_float_equal;
4248 }
4249 inline void validate_expr(const ieee_float_equal_exprt &value)
4250 {
4251  validate_operands(value, 2, "IEEE equality must have two operands");
4252 }
4253 
4254 
4258 {
4259 public:
4261  binary_relation_exprt(ID_ieee_float_notequal)
4262  {
4263  }
4264 
4265  ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs):
4266  binary_relation_exprt(_lhs, ID_ieee_float_notequal, _rhs)
4267  {
4268  }
4269 };
4270 
4282  const exprt &expr)
4283 {
4284  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4286  expr.operands().size()==2,
4287  "IEEE inequality must have two operands");
4288  return static_cast<const ieee_float_notequal_exprt &>(expr);
4289 }
4290 
4295 {
4296  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4298  expr.operands().size()==2,
4299  "IEEE inequality must have two operands");
4300  return static_cast<ieee_float_notequal_exprt &>(expr);
4301 }
4302 
4303 template<>
4305 {
4306  return base.id()==ID_ieee_float_notequal;
4307 }
4308 inline void validate_expr(const ieee_float_notequal_exprt &value)
4309 {
4310  validate_operands(value, 2, "IEEE inequality must have two operands");
4311 }
4312 
4313 
4317 {
4318 public:
4320  {
4321  operands().resize(3);
4322  }
4323 
4325  const exprt &_lhs,
4326  const irep_idt &_id,
4327  const exprt &_rhs,
4328  const exprt &_rm):
4329  exprt(_id)
4330  {
4331  copy_to_operands(_lhs, _rhs, _rm);
4332  }
4333 
4335  {
4336  return op0();
4337  }
4338 
4339  const exprt &lhs() const
4340  {
4341  return op0();
4342  }
4343 
4345  {
4346  return op1();
4347  }
4348 
4349  const exprt &rhs() const
4350  {
4351  return op1();
4352  }
4353 
4355  {
4356  return op2();
4357  }
4358 
4359  const exprt &rounding_mode() const
4360  {
4361  return op2();
4362  }
4363 };
4364 
4376 {
4378  expr.operands().size()==3,
4379  "IEEE float operations must have three arguments");
4380  return static_cast<const ieee_float_op_exprt &>(expr);
4381 }
4382 
4387 {
4389  expr.operands().size()==3,
4390  "IEEE float operations must have three arguments");
4391  return static_cast<ieee_float_op_exprt &>(expr);
4392 }
4393 
4394 // The to_*_expr function for this type doesn't do any checks before casting,
4395 // therefore the implementation is essentially a static_cast.
4396 // Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
4397 // template<>
4398 // inline void validate_expr<ieee_float_op_exprt>(
4399 // const ieee_float_op_exprt &value)
4400 // {
4401 // validate_operands(
4402 // value,
4403 // 3,
4404 // "IEEE float operations must have three arguments");
4405 // }
4406 
4407 
4410 class type_exprt:public exprt
4411 {
4412 public:
4413  type_exprt():exprt(ID_type)
4414  {
4415  }
4416 
4417  explicit type_exprt(const typet &type):exprt(ID_type, type)
4418  {
4419  }
4420 };
4421 
4424 class constant_exprt:public exprt
4425 {
4426 public:
4427  constant_exprt():exprt(ID_constant)
4428  {
4429  }
4430 
4431  explicit constant_exprt(const typet &type):exprt(ID_constant, type)
4432  {
4433  }
4434 
4435  constant_exprt(const irep_idt &_value, const typet &_type):
4436  exprt(ID_constant, _type)
4437  {
4438  set_value(_value);
4439  }
4440 
4441  const irep_idt &get_value() const
4442  {
4443  return get(ID_value);
4444  }
4445 
4446  void set_value(const irep_idt &value)
4447  {
4448  set(ID_value, value);
4449  }
4450 
4451  bool value_is_zero_string() const;
4452 };
4453 
4454 
4465 inline const constant_exprt &to_constant_expr(const exprt &expr)
4466 {
4467  PRECONDITION(expr.id()==ID_constant);
4468  return static_cast<const constant_exprt &>(expr);
4469 }
4470 
4475 {
4476  PRECONDITION(expr.id()==ID_constant);
4477  return static_cast<constant_exprt &>(expr);
4478 }
4479 
4480 template<> inline bool can_cast_expr<constant_exprt>(const exprt &base)
4481 {
4482  return base.id()==ID_constant;
4483 }
4484 
4485 
4489 {
4490 public:
4492  {
4493  set_value(ID_true);
4494  }
4495 };
4496 
4500 {
4501 public:
4503  {
4504  set_value(ID_false);
4505  }
4506 };
4507 
4510 class nil_exprt:public exprt
4511 {
4512 public:
4513  nil_exprt():exprt(static_cast<const exprt &>(get_nil_irep()))
4514  {
4515  }
4516 };
4517 
4521 {
4522 public:
4524  {
4525  set_value(ID_NULL);
4526  }
4527 };
4528 
4532 {
4533 public:
4534  function_application_exprt():binary_exprt(ID_function_application)
4535  {
4536  op0()=symbol_exprt();
4537  }
4538 
4539  explicit function_application_exprt(const typet &_type):
4540  binary_exprt(ID_function_application, _type)
4541  {
4542  op0()=symbol_exprt();
4543  }
4544 
4546  const symbol_exprt &_function, const typet &_type):
4547  function_application_exprt(_type) // NOLINT(runtime/explicit)
4548  {
4549  function()=_function;
4550  }
4551 
4552  symbol_exprt &function()
4553  {
4554  return static_cast<symbol_exprt &>(op0());
4555  }
4556 
4557  const symbol_exprt &function() const
4558  {
4559  return static_cast<const symbol_exprt &>(op0());
4560  }
4561 
4563 
4565  {
4566  return op1().operands();
4567  }
4568 
4569  const argumentst &arguments() const
4570  {
4571  return op1().operands();
4572  }
4573 };
4574 
4586  const exprt &expr)
4587 {
4588  PRECONDITION(expr.id()==ID_function_application);
4590  expr.operands().size()==2,
4591  "Function application must have two operands");
4592  return static_cast<const function_application_exprt &>(expr);
4593 }
4594 
4599 {
4600  PRECONDITION(expr.id()==ID_function_application);
4602  expr.operands().size()==2,
4603  "Function application must have two operands");
4604  return static_cast<function_application_exprt &>(expr);
4605 }
4606 
4607 template<>
4609 {
4610  return base.id()==ID_function_application;
4611 }
4613 {
4614  validate_operands(value, 2, "Function application must have two operands");
4615 }
4616 
4617 
4626 {
4627 public:
4628  concatenation_exprt():exprt(ID_concatenation)
4629  {
4630  }
4631 
4632  explicit concatenation_exprt(const typet &_type):
4633  exprt(ID_concatenation, _type)
4634  {
4635  }
4636 
4638  const exprt &_op0, const exprt &_op1, const typet &_type):
4639  exprt(ID_concatenation, _type)
4640  {
4641  copy_to_operands(_op0, _op1);
4642  }
4643 };
4644 
4656 {
4657  PRECONDITION(expr.id()==ID_concatenation);
4658  // DATA_INVARIANT(
4659  // expr.operands().size()>=2,
4660  // "Concatenation must have two or more operands");
4661  return static_cast<const concatenation_exprt &>(expr);
4662 }
4663 
4668 {
4669  PRECONDITION(expr.id()==ID_concatenation);
4670  // DATA_INVARIANT(
4671  // expr.operands().size()>=2,
4672  // "Concatenation must have two or more operands");
4673  return static_cast<concatenation_exprt &>(expr);
4674 }
4675 
4676 template<> inline bool can_cast_expr<concatenation_exprt>(const exprt &base)
4677 {
4678  return base.id()==ID_concatenation;
4679 }
4680 // template<>
4681 // inline void validate_expr<concatenation_exprt>(
4682 // const concatenation_exprt &value)
4683 // {
4684 // validate_operands(
4685 // value,
4686 // 2,
4687 // "Concatenation must have two or more operands",
4688 // true);
4689 // }
4690 
4691 
4694 class infinity_exprt:public exprt
4695 {
4696 public:
4697  explicit infinity_exprt(const typet &_type):
4698  exprt(ID_infinity, _type)
4699  {
4700  }
4701 };
4702 
4705 class let_exprt:public exprt
4706 {
4707 public:
4708  let_exprt():exprt(ID_let)
4709  {
4710  operands().resize(3);
4711  op0()=symbol_exprt();
4712  }
4713 
4715  {
4716  return static_cast<symbol_exprt &>(op0());
4717  }
4718 
4719  const symbol_exprt &symbol() const
4720  {
4721  return static_cast<const symbol_exprt &>(op0());
4722  }
4723 
4725  {
4726  return op1();
4727  }
4728 
4729  const exprt &value() const
4730  {
4731  return op1();
4732  }
4733 
4735  {
4736  return op2();
4737  }
4738 
4739  const exprt &where() const
4740  {
4741  return op2();
4742  }
4743 };
4744 
4755 inline const let_exprt &to_let_expr(const exprt &expr)
4756 {
4757  PRECONDITION(expr.id()==ID_let);
4758  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
4759  return static_cast<const let_exprt &>(expr);
4760 }
4761 
4766 {
4767  PRECONDITION(expr.id()==ID_let);
4768  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
4769  return static_cast<let_exprt &>(expr);
4770 }
4771 
4772 template<> inline bool can_cast_expr<let_exprt>(const exprt &base)
4773 {
4774  return base.id()==ID_let;
4775 }
4776 inline void validate_expr(const let_exprt &value)
4777 {
4778  validate_operands(value, 3, "Let must have three operands");
4779 }
4780 
4784 {
4785 public:
4787  {
4788  op0()=symbol_exprt();
4789  }
4790 
4792  const irep_idt &_id,
4793  const symbol_exprt &_symbol,
4794  const exprt &_where)
4795  : binary_predicate_exprt(_symbol, _id, _where)
4796  {
4797  }
4798 
4800  {
4801  return static_cast<symbol_exprt &>(op0());
4802  }
4803 
4804  const symbol_exprt &symbol() const
4805  {
4806  return static_cast<const symbol_exprt &>(op0());
4807  }
4808 
4810  {
4811  return op1();
4812  }
4813 
4814  const exprt &where() const
4815  {
4816  return op1();
4817  }
4818 };
4819 
4830 inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
4831 {
4832  DATA_INVARIANT(expr.operands().size()==2,
4833  "quantifier expressions must have two operands");
4834  return static_cast<const quantifier_exprt &>(expr);
4835 }
4836 
4841 {
4842  DATA_INVARIANT(expr.operands().size()==2,
4843  "quantifier expressions must have two operands");
4844  return static_cast<quantifier_exprt &>(expr);
4845 }
4846 
4847 template<> inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
4848 {
4849  return base.id() == ID_forall || base.id() == ID_exists;
4850 }
4851 
4852 inline void validate_expr(const quantifier_exprt &value)
4853 {
4854  validate_operands(value, 2,
4855  "quantifier expressions must have two operands");
4856 }
4857 
4861 {
4862 public:
4864  {
4865  }
4866 
4867  forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
4868  : quantifier_exprt(ID_forall, _symbol, _where)
4869  {
4870  }
4871 };
4872 
4876 {
4877 public:
4879  {
4880  }
4881 
4882  exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
4883  : quantifier_exprt(ID_exists, _symbol, _where)
4884  {
4885  }
4886 };
4887 
4891 {
4892 public:
4893  popcount_exprt(): unary_exprt(ID_popcount)
4894  {
4895  }
4896 
4897  popcount_exprt(const exprt &_op, const typet &_type)
4898  : unary_exprt(ID_popcount, _op, _type)
4899  {
4900  }
4901 
4902  explicit popcount_exprt(const exprt &_op)
4903  : unary_exprt(ID_popcount, _op, _op.type())
4904  {
4905  }
4906 };
4907 
4918 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
4919 {
4920  PRECONDITION(expr.id() == ID_popcount);
4921  DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand");
4922  return static_cast<const popcount_exprt &>(expr);
4923 }
4924 
4929 {
4930  PRECONDITION(expr.id() == ID_popcount);
4931  DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand");
4932  return static_cast<popcount_exprt &>(expr);
4933 }
4934 
4935 template <>
4936 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
4937 {
4938  return base.id() == ID_popcount;
4939 }
4940 inline void validate_expr(const popcount_exprt &value)
4941 {
4942  validate_operands(value, 1, "popcount must have one operand");
4943 }
4944 
4945 #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:3426
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:4223
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:3762
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:4188
const symbol_exprt & symbol() const
Definition: std_expr.h:3933
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:3230
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:3395
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:4349
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:4847
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:4729
if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
Definition: std_expr.h:3370
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:4531
binary_predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:737
exprt & object()
Definition: std_expr.h:3180
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:4867
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:4265
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:3018
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:3672
const exprt & op() const
Definition: std_expr.h:340
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: std_expr.h:4676
const exprt & pointer() const
Definition: std_expr.h:3312
Evaluates to true if the operand is infinite.
Definition: std_expr.h:4040
const exprt & op() const
Definition: std_expr.h:2942
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:3540
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:3917
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:3710
exprt & lower()
Definition: std_expr.h:3106
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:4441
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:4520
argumentst & arguments()
Definition: std_expr.h:4564
An expression denoting a type.
Definition: std_expr.h:4410
abs_exprt(const exprt &_op)
Definition: std_expr.h:395
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:3660
type_exprt(const typet &type)
Definition: std_expr.h:4417
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:3361
exprt & cond()
Definition: std_expr.h:3385
std::size_t get_component_number() const
Definition: std_expr.h:3905
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:4148
exprt & old()
Definition: std_expr.h:3478
if_exprt()
Definition: std_expr.h:3380
exprt & new_value()
Definition: std_expr.h:3498
typet & type()
Definition: expr.h:56
const symbol_exprt & symbol() const
Definition: std_expr.h:4804
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:3060
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:3201
const exprt & where() const
Definition: std_expr.h:4814
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:3493
A constant literal expression.
Definition: std_expr.h:4424
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:4354
function_application_exprt(const symbol_exprt &_function, const typet &_type)
Definition: std_expr.h:4545
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:3604
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:3121
const exprt & where() const
Definition: std_expr.h:4739
irep_idt get_component_name() const
Definition: std_expr.h:3623
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:4281
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
Definition: std_expr.h:4755
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:4324
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
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:4245
plus_exprt()
Definition: std_expr.h:896
Extract member of struct or union.
Definition: std_expr.h:3871
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:3081
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:3271
exprt & where()
Definition: std_expr.h:4734
void set_instance(unsigned int instance)
Definition: std_expr.cpp:38
Concatenation of bit-vector operands.
Definition: std_expr.h:4625
equality
Definition: std_expr.h:1354
symbol_exprt & symbol()
Definition: std_expr.h:4799
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:3684
constant_exprt(const irep_idt &_value, const typet &_type)
Definition: std_expr.h:4435
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:3900
bool can_cast_expr< function_application_exprt >(const exprt &base)
Definition: std_expr.h:4608
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:4375
exprt conjunction(const exprt::operandst &)
Definition: std_expr.cpp:48
const exprt & compound() const
Definition: std_expr.h:3922
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:3364
const exprt & src() const
Definition: std_expr.h:3111
const irep_idt & id() const
Definition: irep.h:189
unary_exprt(const irep_idt &_id)
Definition: std_expr.h:311
dereference_exprt(const exprt &op, const typet &type)
Definition: std_expr.h:3302
popcount_exprt(const exprt &_op)
Definition: std_expr.h:4902
void set_value(const irep_idt &value)
Definition: std_expr.h:4446
const exprt & times() const
Definition: std_expr.h:2932
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3988
Bit-wise OR.
Definition: std_expr.h:2583
bool can_cast_expr< isnan_exprt >(const exprt &base)
Definition: std_expr.h:4028
An expression denoting infinity.
Definition: std_expr.h:4694
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:4488
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:2958
A generic base class for binary expressions.
Definition: std_expr.h:649
function_application_exprt(const typet &_type)
Definition: std_expr.h:4539
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:4655
exprt & init()
Definition: std_expr.h:39
exprt & old()
Definition: std_expr.h:3696
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:3741
exprt & times()
Definition: std_expr.h:2927
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:4562
The NIL expression.
Definition: std_expr.h:4510
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:1426
IEEE floating-point disequality.
Definition: std_expr.h:4257
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:3976
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
Definition: std_expr.h:3039
member_exprt(const exprt &op, const struct_typet::componentt &c)
Definition: std_expr.h:3883
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1722
Operator to dereference a pointer.
Definition: std_expr.h:3284
exprt & rounding_mode()
Definition: std_expr.h:2200
A constant-size array type.
Definition: std_types.h:1629
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:291
exprt & src()
Definition: std_expr.h:3096
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:3072
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:3725
popcount_exprt(const exprt &_op, const typet &_type)
Definition: std_expr.h:4897
not_exprt(const exprt &op)
Definition: std_expr.h:3233
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast a generic exprt to a isinf_exprt.
Definition: std_expr.h:4063
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:4585
const exprt & lhs() const
Definition: std_expr.h:4339
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:4697
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:3137
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:230
const exprt & false_case() const
Definition: std_expr.h:3410
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:3955
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: std_expr.h:3158
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:3390
A forall expression.
Definition: std_expr.h:4860
with_exprt(const exprt &_old, const exprt &_where, const exprt &_new_value)
Definition: std_expr.h:3464
The plus expression.
Definition: std_expr.h:893
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:4480
symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
Definition: std_expr.h:116
const symbol_exprt & symbol() const
Definition: std_expr.h:4719
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:4523
ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:4207
predicate_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:597
exprt & where()
Definition: std_expr.h:4809
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:3101
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast a generic exprt to a quantifier_exprt.
Definition: std_expr.h:4830
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:4099
Logical right shift.
Definition: std_expr.h:2888
exprt & compound()
Definition: std_expr.h:3927
const index_designatort & to_index_designator(const exprt &expr)
Cast a generic exprt to an index_designatort.
Definition: std_expr.h:3583
vector constructor from list of elements
Definition: std_expr.h:1684
const exprt & old() const
Definition: std_expr.h:3483
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast a generic exprt to a isfinite_exprt.
Definition: std_expr.h:4119
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:3349
Operator to return the address of an object.
Definition: std_expr.h:3170
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:3405
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:4637
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
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:3874
quantifier_exprt(const irep_idt &_id, const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4791
bool has_operands() const
Definition: expr.h:63
const exprt & index() const
Definition: std_expr.h:3562
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:3218
The boolean constant false.
Definition: std_expr.h:4499
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:2979
exprt & index()
Definition: std_expr.h:3013
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:3715
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: std_expr.h:4304
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1450
constant_exprt(const typet &type)
Definition: std_expr.h:4431
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:3556
Complex numbers made of pair of given subtype.
Definition: std_types.h:1677
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast a generic exprt to a popcount_exprt.
Definition: std_expr.h:4918
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:3519
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:3701
const exprt & object() const
Definition: std_expr.h:3185
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast a generic exprt to a isnan_exprt.
Definition: std_expr.h:4011
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:3675
exprt & value()
Definition: std_expr.h:4724
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:4890
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:4096
const exprt & index() const
Definition: std_expr.h:3023
concatenation_exprt(const typet &_type)
Definition: std_expr.h:4632
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:3307
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:3911
const exprt & rounding_mode() const
Definition: std_expr.h:4359
isnormal_exprt(const exprt &op)
Definition: std_expr.h:4151
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:3296
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:3291
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:3461
const exprt & upper() const
Definition: std_expr.h:3116
sign_exprt(const exprt &_op)
Definition: std_expr.h:641
A base class for quantifier expressions.
Definition: std_expr.h:4783
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:3895
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:4772
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:3254
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:3400
exprt & index()
Definition: std_expr.h:3567
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:2937
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:4043
arrays with given size
Definition: std_types.h:1004
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:4882
isnan_exprt(const exprt &op)
Definition: std_expr.h:3991
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: std_expr.h:4084
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:4136
exprt & new_value()
Definition: std_expr.h:3720
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:4714
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:4875
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1538
exprt & where()
Definition: std_expr.h:3488
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:4705
void clear_static_lifetime()
Definition: std_expr.h:179
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast a generic exprt to a isnormal_exprt.
Definition: std_expr.h:4171
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:3008
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:2998
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:3447
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:4316
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:4786
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:4569
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:3617
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: std_expr.h:4936
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:3639
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2991
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:4200
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:3175
const exprt & new_value() const
Definition: std_expr.h:3503
const exprt & op() const
Definition: std_expr.h:2195