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