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 "narrow.h"
19 #include "std_types.h"
20 
23 {
24 public:
25  nullary_exprt(const irep_idt &_id, typet _type)
26  : expr_protectedt(_id, std::move(_type))
27  {
28  }
29 
31  operandst &operands() = delete;
32  const operandst &operands() const = delete;
33 
34  const exprt &op0() const = delete;
35  exprt &op0() = delete;
36  const exprt &op1() const = delete;
37  exprt &op1() = delete;
38  const exprt &op2() const = delete;
39  exprt &op2() = delete;
40  const exprt &op3() const = delete;
41  exprt &op3() = delete;
42 
43  void move_to_operands(exprt &) = delete;
44  void move_to_operands(exprt &, exprt &) = delete;
45  void move_to_operands(exprt &, exprt &, exprt &) = delete;
46 
47  void copy_to_operands(const exprt &expr) = delete;
48  void copy_to_operands(const exprt &, const exprt &) = delete;
49  void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
50 };
51 
54 {
55 public:
56  // constructor
58  const irep_idt &_id,
59  exprt _op0,
60  exprt _op1,
61  exprt _op2,
62  typet _type)
64  _id,
65  std::move(_type),
66  {std::move(_op0), std::move(_op1), std::move(_op2)})
67  {
68  }
69 
70  // make op0 to op2 public
71  using exprt::op0;
72  using exprt::op1;
73  using exprt::op2;
74 
75  const exprt &op3() const = delete;
76  exprt &op3() = delete;
77 };
78 
81 {
82 public:
84  explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type))
85  {
86  }
87 
90  symbol_exprt(const irep_idt &identifier, typet type)
91  : nullary_exprt(ID_symbol, std::move(type))
92  {
93  set_identifier(identifier);
94  }
95 
100  static symbol_exprt typeless(const irep_idt &id)
101  {
102  return symbol_exprt(id, typet());
103  }
104 
105  void set_identifier(const irep_idt &identifier)
106  {
107  set(ID_identifier, identifier);
108  }
109 
110  const irep_idt &get_identifier() const
111  {
112  return get(ID_identifier);
113  }
114 };
115 
116 // NOLINTNEXTLINE(readability/namespace)
117 namespace std
118 {
119 template <>
120 // NOLINTNEXTLINE(readability/identifiers)
121 struct hash<::symbol_exprt>
122 {
123  size_t operator()(const ::symbol_exprt &sym)
124  {
125  return irep_id_hash()(sym.get_identifier());
126  }
127 };
128 } // namespace std
129 
133 {
134 public:
138  : symbol_exprt(identifier, std::move(type))
139  {
140  }
141 
142  bool is_static_lifetime() const
143  {
144  return get_bool(ID_C_static_lifetime);
145  }
146 
148  {
149  return set(ID_C_static_lifetime, true);
150  }
151 
153  {
154  remove(ID_C_static_lifetime);
155  }
156 
157  bool is_thread_local() const
158  {
159  return get_bool(ID_C_thread_local);
160  }
161 
163  {
164  return set(ID_C_thread_local, true);
165  }
166 
168  {
169  remove(ID_C_thread_local);
170  }
171 };
172 
173 template <>
174 inline bool can_cast_expr<symbol_exprt>(const exprt &base)
175 {
176  return base.id() == ID_symbol;
177 }
178 
179 inline void validate_expr(const symbol_exprt &value)
180 {
181  validate_operands(value, 0, "Symbols must not have operands");
182 }
183 
190 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
191 {
192  PRECONDITION(expr.id()==ID_symbol);
193  const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
194  validate_expr(ret);
195  return ret;
196 }
197 
200 {
201  PRECONDITION(expr.id()==ID_symbol);
202  symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
203  validate_expr(ret);
204  return ret;
205 }
206 
207 
210 {
211 public:
215  : nullary_exprt(ID_nondet_symbol, std::move(type))
216  {
217  set_identifier(identifier);
218  }
219 
224  irep_idt identifier,
225  typet type,
226  source_locationt location)
227  : nullary_exprt(ID_nondet_symbol, std::move(type))
228  {
229  set_identifier(std::move(identifier));
230  add_source_location() = std::move(location);
231  }
232 
233  void set_identifier(const irep_idt &identifier)
234  {
235  set(ID_identifier, identifier);
236  }
237 
238  const irep_idt &get_identifier() const
239  {
240  return get(ID_identifier);
241  }
242 };
243 
244 template <>
246 {
247  return base.id() == ID_nondet_symbol;
248 }
249 
250 inline void validate_expr(const nondet_symbol_exprt &value)
251 {
252  validate_operands(value, 0, "Symbols must not have operands");
253 }
254 
262 {
263  PRECONDITION(expr.id()==ID_nondet_symbol);
264  const nondet_symbol_exprt &ret =
265  static_cast<const nondet_symbol_exprt &>(expr);
266  validate_expr(ret);
267  return ret;
268 }
269 
272 {
273  PRECONDITION(expr.id()==ID_symbol);
274  nondet_symbol_exprt &ret = static_cast<nondet_symbol_exprt &>(expr);
275  validate_expr(ret);
276  return ret;
277 }
278 
279 
282 {
283 public:
284  unary_exprt(const irep_idt &_id, const exprt &_op)
285  : expr_protectedt(_id, _op.type(), {_op})
286  {
287  }
288 
289  unary_exprt(const irep_idt &_id, exprt _op, typet _type)
290  : expr_protectedt(_id, std::move(_type), {std::move(_op)})
291  {
292  }
293 
294  const exprt &op() const
295  {
296  return op0();
297  }
298 
300  {
301  return op0();
302  }
303 
304  const exprt &op1() const = delete;
305  exprt &op1() = delete;
306  const exprt &op2() const = delete;
307  exprt &op2() = delete;
308  const exprt &op3() const = delete;
309  exprt &op3() = delete;
310 };
311 
312 template <>
313 inline bool can_cast_expr<unary_exprt>(const exprt &base)
314 {
315  return base.operands().size() == 1;
316 }
317 
318 inline void validate_expr(const unary_exprt &value)
319 {
320  validate_operands(value, 1, "Unary expressions must have one operand");
321 }
322 
329 inline const unary_exprt &to_unary_expr(const exprt &expr)
330 {
331  const unary_exprt &ret = static_cast<const unary_exprt &>(expr);
332  validate_expr(ret);
333  return ret;
334 }
335 
338 {
339  unary_exprt &ret = static_cast<unary_exprt &>(expr);
340  validate_expr(ret);
341  return ret;
342 }
343 
344 
346 class abs_exprt:public unary_exprt
347 {
348 public:
349  explicit abs_exprt(exprt _op) : unary_exprt(ID_abs, std::move(_op))
350  {
351  }
352 };
353 
354 template <>
355 inline bool can_cast_expr<abs_exprt>(const exprt &base)
356 {
357  return base.id() == ID_abs;
358 }
359 
360 inline void validate_expr(const abs_exprt &value)
361 {
362  validate_operands(value, 1, "Absolute value must have one operand");
363 }
364 
371 inline const abs_exprt &to_abs_expr(const exprt &expr)
372 {
373  PRECONDITION(expr.id()==ID_abs);
374  const abs_exprt &ret = static_cast<const abs_exprt &>(expr);
375  validate_expr(ret);
376  return ret;
377 }
378 
381 {
382  PRECONDITION(expr.id()==ID_abs);
383  abs_exprt &ret = static_cast<abs_exprt &>(expr);
384  validate_expr(ret);
385  return ret;
386 }
387 
388 
391 {
392 public:
394  : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
395  {
396  }
397 
398  explicit unary_minus_exprt(exprt _op)
399  : unary_exprt(ID_unary_minus, std::move(_op))
400  {
401  }
402 };
403 
404 template <>
405 inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
406 {
407  return base.id() == ID_unary_minus;
408 }
409 
410 inline void validate_expr(const unary_minus_exprt &value)
411 {
412  validate_operands(value, 1, "Unary minus must have one operand");
413 }
414 
421 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
422 {
423  PRECONDITION(expr.id()==ID_unary_minus);
424  const unary_minus_exprt &ret = static_cast<const unary_minus_exprt &>(expr);
425  validate_expr(ret);
426  return ret;
427 }
428 
431 {
432  PRECONDITION(expr.id()==ID_unary_minus);
433  unary_minus_exprt &ret = static_cast<unary_minus_exprt &>(expr);
434  validate_expr(ret);
435  return ret;
436 }
437 
440 {
441 public:
443  : unary_exprt(ID_unary_plus, std::move(op))
444  {
445  }
446 };
447 
448 template <>
449 inline bool can_cast_expr<unary_plus_exprt>(const exprt &base)
450 {
451  return base.id() == ID_unary_plus;
452 }
453 
454 inline void validate_expr(const unary_plus_exprt &value)
455 {
456  validate_operands(value, 1, "unary plus must have one operand");
457 }
458 
465 inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
466 {
467  PRECONDITION(expr.id() == ID_unary_plus);
468  const unary_plus_exprt &ret = static_cast<const unary_plus_exprt &>(expr);
469  validate_expr(ret);
470  return ret;
471 }
472 
475 {
476  PRECONDITION(expr.id() == ID_unary_plus);
477  unary_plus_exprt &ret = static_cast<unary_plus_exprt &>(expr);
478  validate_expr(ret);
479  return ret;
480 }
481 
485 {
486 public:
487  explicit predicate_exprt(const irep_idt &_id)
488  : expr_protectedt(_id, bool_typet())
489  {
490  }
491 };
492 
496 {
497 public:
499  : unary_exprt(_id, std::move(_op), bool_typet())
500  {
501  }
502 };
503 
507 {
508 public:
509  explicit sign_exprt(exprt _op)
510  : unary_predicate_exprt(ID_sign, std::move(_op))
511  {
512  }
513 };
514 
515 template <>
516 inline bool can_cast_expr<sign_exprt>(const exprt &base)
517 {
518  return base.id() == ID_sign;
519 }
520 
521 inline void validate_expr(const sign_exprt &expr)
522 {
523  validate_operands(expr, 1, "sign expression must have one operand");
524 }
525 
532 inline const sign_exprt &to_sign_expr(const exprt &expr)
533 {
534  PRECONDITION(expr.id() == ID_sign);
535  const sign_exprt &ret = static_cast<const sign_exprt &>(expr);
536  validate_expr(ret);
537  return ret;
538 }
539 
542 {
543  PRECONDITION(expr.id() == ID_sign);
544  sign_exprt &ret = static_cast<sign_exprt &>(expr);
545  validate_expr(ret);
546  return ret;
547 }
548 
551 {
552 public:
553  binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
554  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
555  {
556  }
557 
558  binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
559  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
560  {
561  }
562 
563  static void check(
564  const exprt &expr,
566  {
567  DATA_CHECK(
568  vm,
569  expr.operands().size() == 2,
570  "binary expression must have two operands");
571  }
572 
573  static void validate(
574  const exprt &expr,
575  const namespacet &,
577  {
578  check(expr, vm);
579  }
580 
582  {
583  return exprt::op0();
584  }
585 
586  const exprt &lhs() const
587  {
588  return exprt::op0();
589  }
590 
592  {
593  return exprt::op1();
594  }
595 
596  const exprt &rhs() const
597  {
598  return exprt::op1();
599  }
600 
601  // make op0 and op1 public
602  using exprt::op0;
603  using exprt::op1;
604 
605  const exprt &op2() const = delete;
606  exprt &op2() = delete;
607  const exprt &op3() const = delete;
608  exprt &op3() = delete;
609 };
610 
611 template <>
612 inline bool can_cast_expr<binary_exprt>(const exprt &base)
613 {
614  return base.operands().size() == 2;
615 }
616 
617 inline void validate_expr(const binary_exprt &value)
618 {
619  binary_exprt::check(value);
620 }
621 
628 inline const binary_exprt &to_binary_expr(const exprt &expr)
629 {
630  binary_exprt::check(expr);
631  return static_cast<const binary_exprt &>(expr);
632 }
633 
636 {
637  binary_exprt::check(expr);
638  return static_cast<binary_exprt &>(expr);
639 }
640 
644 {
645 public:
646  binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
647  : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
648  {
649  }
650 
651  static void check(
652  const exprt &expr,
654  {
655  binary_exprt::check(expr, vm);
656  }
657 
658  static void validate(
659  const exprt &expr,
660  const namespacet &ns,
662  {
663  binary_exprt::validate(expr, ns, vm);
664 
665  DATA_CHECK(
666  vm,
667  expr.type().id() == ID_bool,
668  "result of binary predicate expression should be of type bool");
669  }
670 };
671 
675 {
676 public:
677  binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
678  : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
679  {
680  }
681 
682  static void check(
683  const exprt &expr,
685  {
687  }
688 
689  static void validate(
690  const exprt &expr,
691  const namespacet &ns,
693  {
694  binary_predicate_exprt::validate(expr, ns, vm);
695 
696  // we now can safely assume that 'expr' is a binary predicate
697  const auto &expr_binary = static_cast<const binary_predicate_exprt &>(expr);
698 
699  // check that the types of the operands are the same
700  DATA_CHECK(
701  vm,
702  expr_binary.op0().type() == expr_binary.op1().type(),
703  "lhs and rhs of binary relation expression should have same type");
704  }
705 };
706 
707 template <>
709 {
710  return can_cast_expr<binary_exprt>(base);
711 }
712 
713 inline void validate_expr(const binary_relation_exprt &value)
714 {
716 }
717 
725 {
727  return static_cast<const binary_relation_exprt &>(expr);
728 }
729 
732 {
734  return static_cast<binary_relation_exprt &>(expr);
735 }
736 
737 
741 {
742 public:
743  multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
744  : expr_protectedt(_id, std::move(_type))
745  {
746  operands() = std::move(_operands);
747  }
748 
749  multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
750  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
751  {
752  }
753 
754  multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
755  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
756  {
757  }
758 
759  // In contrast to exprt::opX, the methods
760  // below check the size.
762  {
763  PRECONDITION(operands().size() >= 1);
764  return operands().front();
765  }
766 
768  {
769  PRECONDITION(operands().size() >= 2);
770  return operands()[1];
771  }
772 
774  {
775  PRECONDITION(operands().size() >= 3);
776  return operands()[2];
777  }
778 
780  {
781  PRECONDITION(operands().size() >= 4);
782  return operands()[3];
783  }
784 
785  const exprt &op0() const
786  {
787  PRECONDITION(operands().size() >= 1);
788  return operands().front();
789  }
790 
791  const exprt &op1() const
792  {
793  PRECONDITION(operands().size() >= 2);
794  return operands()[1];
795  }
796 
797  const exprt &op2() const
798  {
799  PRECONDITION(operands().size() >= 3);
800  return operands()[2];
801  }
802 
803  const exprt &op3() const
804  {
805  PRECONDITION(operands().size() >= 4);
806  return operands()[3];
807  }
808 };
809 
816 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
817 {
818  return static_cast<const multi_ary_exprt &>(expr);
819 }
820 
823 {
824  return static_cast<multi_ary_exprt &>(expr);
825 }
826 
827 
831 {
832 public:
833  plus_exprt(exprt _lhs, exprt _rhs)
834  : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
835  {
836  }
837 
838  plus_exprt(exprt _lhs, exprt _rhs, typet _type)
839  : multi_ary_exprt(
840  std::move(_lhs),
841  ID_plus,
842  std::move(_rhs),
843  std::move(_type))
844  {
845  }
846 
847  plus_exprt(operandst _operands, typet _type)
848  : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
849  {
850  }
851 };
852 
853 template <>
854 inline bool can_cast_expr<plus_exprt>(const exprt &base)
855 {
856  return base.id() == ID_plus;
857 }
858 
859 inline void validate_expr(const plus_exprt &value)
860 {
861  validate_operands(value, 2, "Plus must have two or more operands", true);
862 }
863 
870 inline const plus_exprt &to_plus_expr(const exprt &expr)
871 {
872  PRECONDITION(expr.id()==ID_plus);
873  const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
874  validate_expr(ret);
875  return ret;
876 }
877 
880 {
881  PRECONDITION(expr.id()==ID_plus);
882  plus_exprt &ret = static_cast<plus_exprt &>(expr);
883  validate_expr(ret);
884  return ret;
885 }
886 
887 
890 {
891 public:
892  minus_exprt(exprt _lhs, exprt _rhs)
893  : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
894  {
895  }
896 };
897 
898 template <>
899 inline bool can_cast_expr<minus_exprt>(const exprt &base)
900 {
901  return base.id() == ID_minus;
902 }
903 
904 inline void validate_expr(const minus_exprt &value)
905 {
906  validate_operands(value, 2, "Minus must have two or more operands", true);
907 }
908 
915 inline const minus_exprt &to_minus_expr(const exprt &expr)
916 {
917  PRECONDITION(expr.id()==ID_minus);
918  const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
919  validate_expr(ret);
920  return ret;
921 }
922 
925 {
926  PRECONDITION(expr.id()==ID_minus);
927  minus_exprt &ret = static_cast<minus_exprt &>(expr);
928  validate_expr(ret);
929  return ret;
930 }
931 
932 
936 {
937 public:
938  mult_exprt(exprt _lhs, exprt _rhs)
939  : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
940  {
941  }
942 };
943 
944 template <>
945 inline bool can_cast_expr<mult_exprt>(const exprt &base)
946 {
947  return base.id() == ID_mult;
948 }
949 
950 inline void validate_expr(const mult_exprt &value)
951 {
952  validate_operands(value, 2, "Multiply must have two or more operands", true);
953 }
954 
961 inline const mult_exprt &to_mult_expr(const exprt &expr)
962 {
963  PRECONDITION(expr.id()==ID_mult);
964  const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
965  validate_expr(ret);
966  return ret;
967 }
968 
971 {
972  PRECONDITION(expr.id()==ID_mult);
973  mult_exprt &ret = static_cast<mult_exprt &>(expr);
974  validate_expr(ret);
975  return ret;
976 }
977 
978 
981 {
982 public:
983  div_exprt(exprt _lhs, exprt _rhs)
984  : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
985  {
986  }
987 
990  {
991  return op0();
992  }
993 
995  const exprt &dividend() const
996  {
997  return op0();
998  }
999 
1002  {
1003  return op1();
1004  }
1005 
1007  const exprt &divisor() const
1008  {
1009  return op1();
1010  }
1011 };
1012 
1013 template <>
1014 inline bool can_cast_expr<div_exprt>(const exprt &base)
1015 {
1016  return base.id() == ID_div;
1017 }
1018 
1019 inline void validate_expr(const div_exprt &value)
1020 {
1021  validate_operands(value, 2, "Divide must have two operands");
1022 }
1023 
1030 inline const div_exprt &to_div_expr(const exprt &expr)
1031 {
1032  PRECONDITION(expr.id()==ID_div);
1033  const div_exprt &ret = static_cast<const div_exprt &>(expr);
1034  validate_expr(ret);
1035  return ret;
1036 }
1037 
1040 {
1041  PRECONDITION(expr.id()==ID_div);
1042  div_exprt &ret = static_cast<div_exprt &>(expr);
1043  validate_expr(ret);
1044  return ret;
1045 }
1046 
1047 
1050 {
1051 public:
1052  mod_exprt(exprt _lhs, exprt _rhs)
1053  : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1054  {
1055  }
1056 };
1057 
1058 template <>
1059 inline bool can_cast_expr<mod_exprt>(const exprt &base)
1060 {
1061  return base.id() == ID_mod;
1062 }
1063 
1064 inline void validate_expr(const mod_exprt &value)
1065 {
1066  validate_operands(value, 2, "Modulo must have two operands");
1067 }
1068 
1075 inline const mod_exprt &to_mod_expr(const exprt &expr)
1076 {
1077  PRECONDITION(expr.id()==ID_mod);
1078  const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1079  validate_expr(ret);
1080  return ret;
1081 }
1082 
1085 {
1086  PRECONDITION(expr.id()==ID_mod);
1087  mod_exprt &ret = static_cast<mod_exprt &>(expr);
1088  validate_expr(ret);
1089  return ret;
1090 }
1091 
1092 
1095 {
1096 public:
1097  rem_exprt(exprt _lhs, exprt _rhs)
1098  : binary_exprt(std::move(_lhs), ID_rem, std::move(_rhs))
1099  {
1100  }
1101 };
1102 
1103 template <>
1104 inline bool can_cast_expr<rem_exprt>(const exprt &base)
1105 {
1106  return base.id() == ID_rem;
1107 }
1108 
1109 inline void validate_expr(const rem_exprt &value)
1110 {
1111  validate_operands(value, 2, "Remainder must have two operands");
1112 }
1113 
1120 inline const rem_exprt &to_rem_expr(const exprt &expr)
1121 {
1122  PRECONDITION(expr.id()==ID_rem);
1123  const rem_exprt &ret = static_cast<const rem_exprt &>(expr);
1124  validate_expr(ret);
1125  return ret;
1126 }
1127 
1130 {
1131  PRECONDITION(expr.id()==ID_rem);
1132  rem_exprt &ret = static_cast<rem_exprt &>(expr);
1133  validate_expr(ret);
1134  return ret;
1135 }
1136 
1137 
1140 {
1141 public:
1143  : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1144  {
1145  }
1146 
1147  static void check(
1148  const exprt &expr,
1150  {
1151  binary_relation_exprt::check(expr, vm);
1152  }
1153 
1154  static void validate(
1155  const exprt &expr,
1156  const namespacet &ns,
1158  {
1159  binary_relation_exprt::validate(expr, ns, vm);
1160  }
1161 };
1162 
1163 template <>
1164 inline bool can_cast_expr<equal_exprt>(const exprt &base)
1165 {
1166  return base.id() == ID_equal;
1167 }
1168 
1169 inline void validate_expr(const equal_exprt &value)
1170 {
1171  equal_exprt::check(value);
1172 }
1173 
1180 inline const equal_exprt &to_equal_expr(const exprt &expr)
1181 {
1182  PRECONDITION(expr.id()==ID_equal);
1183  equal_exprt::check(expr);
1184  return static_cast<const equal_exprt &>(expr);
1185 }
1186 
1189 {
1190  PRECONDITION(expr.id()==ID_equal);
1191  equal_exprt::check(expr);
1192  return static_cast<equal_exprt &>(expr);
1193 }
1194 
1195 
1198 {
1199 public:
1201  : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1202  {
1203  }
1204 };
1205 
1206 template <>
1207 inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1208 {
1209  return base.id() == ID_notequal;
1210 }
1211 
1212 inline void validate_expr(const notequal_exprt &value)
1213 {
1214  validate_operands(value, 2, "Inequality must have two operands");
1215 }
1216 
1223 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1224 {
1225  PRECONDITION(expr.id()==ID_notequal);
1226  const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1227  validate_expr(ret);
1228  return ret;
1229 }
1230 
1233 {
1234  PRECONDITION(expr.id()==ID_notequal);
1235  notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1236  validate_expr(ret);
1237  return ret;
1238 }
1239 
1240 
1243 {
1244 public:
1245  index_exprt(const exprt &_array, exprt _index)
1246  : binary_exprt(_array, ID_index, std::move(_index), _array.type().subtype())
1247  {
1248  }
1249 
1250  index_exprt(exprt _array, exprt _index, typet _type)
1251  : binary_exprt(
1252  std::move(_array),
1253  ID_index,
1254  std::move(_index),
1255  std::move(_type))
1256  {
1257  }
1258 
1260  {
1261  return op0();
1262  }
1263 
1264  const exprt &array() const
1265  {
1266  return op0();
1267  }
1268 
1270  {
1271  return op1();
1272  }
1273 
1274  const exprt &index() const
1275  {
1276  return op1();
1277  }
1278 };
1279 
1280 template <>
1281 inline bool can_cast_expr<index_exprt>(const exprt &base)
1282 {
1283  return base.id() == ID_index;
1284 }
1285 
1286 inline void validate_expr(const index_exprt &value)
1287 {
1288  validate_operands(value, 2, "Array index must have two operands");
1289 }
1290 
1297 inline const index_exprt &to_index_expr(const exprt &expr)
1298 {
1299  PRECONDITION(expr.id()==ID_index);
1300  const index_exprt &ret = static_cast<const index_exprt &>(expr);
1301  validate_expr(ret);
1302  return ret;
1303 }
1304 
1307 {
1308  PRECONDITION(expr.id()==ID_index);
1309  index_exprt &ret = static_cast<index_exprt &>(expr);
1310  validate_expr(ret);
1311  return ret;
1312 }
1313 
1314 
1317 {
1318 public:
1319  explicit array_of_exprt(exprt _what, array_typet _type)
1320  : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1321  {
1322  }
1323 
1324  const array_typet &type() const
1325  {
1326  return static_cast<const array_typet &>(unary_exprt::type());
1327  }
1328 
1330  {
1331  return static_cast<array_typet &>(unary_exprt::type());
1332  }
1333 
1335  {
1336  return op0();
1337  }
1338 
1339  const exprt &what() const
1340  {
1341  return op0();
1342  }
1343 };
1344 
1345 template <>
1346 inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1347 {
1348  return base.id() == ID_array_of;
1349 }
1350 
1351 inline void validate_expr(const array_of_exprt &value)
1352 {
1353  validate_operands(value, 1, "'Array of' must have one operand");
1354 }
1355 
1362 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1363 {
1364  PRECONDITION(expr.id()==ID_array_of);
1365  const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1366  validate_expr(ret);
1367  return ret;
1368 }
1369 
1372 {
1373  PRECONDITION(expr.id()==ID_array_of);
1374  array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1375  validate_expr(ret);
1376  return ret;
1377 }
1378 
1379 
1382 {
1383 public:
1385  : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1386  {
1387  }
1388 
1389  const array_typet &type() const
1390  {
1391  return static_cast<const array_typet &>(multi_ary_exprt::type());
1392  }
1393 
1395  {
1396  return static_cast<array_typet &>(multi_ary_exprt::type());
1397  }
1398 };
1399 
1400 template <>
1401 inline bool can_cast_expr<array_exprt>(const exprt &base)
1402 {
1403  return base.id() == ID_array;
1404 }
1405 
1412 inline const array_exprt &to_array_expr(const exprt &expr)
1413 {
1414  PRECONDITION(expr.id()==ID_array);
1415  return static_cast<const array_exprt &>(expr);
1416 }
1417 
1420 {
1421  PRECONDITION(expr.id()==ID_array);
1422  return static_cast<array_exprt &>(expr);
1423 }
1424 
1428 {
1429 public:
1431  : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1432  {
1433  }
1434 
1435  const array_typet &type() const
1436  {
1437  return static_cast<const array_typet &>(multi_ary_exprt::type());
1438  }
1439 
1441  {
1442  return static_cast<array_typet &>(multi_ary_exprt::type());
1443  }
1444 
1446  void add(exprt index, exprt value)
1447  {
1448  add_to_operands(std::move(index), std::move(value));
1449  }
1450 };
1451 
1452 template <>
1453 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1454 {
1455  return base.id() == ID_array_list;
1456 }
1457 
1458 inline void validate_expr(const array_list_exprt &value)
1459 {
1460  PRECONDITION(value.operands().size() % 2 == 0);
1461 }
1462 
1463 inline const array_list_exprt &to_array_list_expr(const exprt &expr)
1464 {
1466  auto &ret = static_cast<const array_list_exprt &>(expr);
1467  validate_expr(ret);
1468  return ret;
1469 }
1470 
1472 {
1474  auto &ret = static_cast<array_list_exprt &>(expr);
1475  validate_expr(ret);
1476  return ret;
1477 }
1478 
1481 {
1482 public:
1484  : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1485  {
1486  }
1487 };
1488 
1489 template <>
1490 inline bool can_cast_expr<vector_exprt>(const exprt &base)
1491 {
1492  return base.id() == ID_vector;
1493 }
1494 
1501 inline const vector_exprt &to_vector_expr(const exprt &expr)
1502 {
1503  PRECONDITION(expr.id()==ID_vector);
1504  return static_cast<const vector_exprt &>(expr);
1505 }
1506 
1509 {
1510  PRECONDITION(expr.id()==ID_vector);
1511  return static_cast<vector_exprt &>(expr);
1512 }
1513 
1514 
1517 {
1518 public:
1519  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1520  : unary_exprt(ID_union, std::move(_value), std::move(_type))
1521  {
1522  set_component_name(_component_name);
1523  }
1524 
1526  {
1527  return get(ID_component_name);
1528  }
1529 
1530  void set_component_name(const irep_idt &component_name)
1531  {
1532  set(ID_component_name, component_name);
1533  }
1534 
1535  std::size_t get_component_number() const
1536  {
1537  return get_size_t(ID_component_number);
1538  }
1539 
1540  void set_component_number(std::size_t component_number)
1541  {
1542  set(ID_component_number, narrow_cast<long long>(component_number));
1543  }
1544 };
1545 
1546 template <>
1547 inline bool can_cast_expr<union_exprt>(const exprt &base)
1548 {
1549  return base.id() == ID_union;
1550 }
1551 
1552 inline void validate_expr(const union_exprt &value)
1553 {
1554  validate_operands(value, 1, "Union constructor must have one operand");
1555 }
1556 
1563 inline const union_exprt &to_union_expr(const exprt &expr)
1564 {
1565  PRECONDITION(expr.id()==ID_union);
1566  const union_exprt &ret = static_cast<const union_exprt &>(expr);
1567  validate_expr(ret);
1568  return ret;
1569 }
1570 
1573 {
1574  PRECONDITION(expr.id()==ID_union);
1575  union_exprt &ret = static_cast<union_exprt &>(expr);
1576  validate_expr(ret);
1577  return ret;
1578 }
1579 
1580 
1583 {
1584 public:
1585  struct_exprt(operandst _operands, typet _type)
1586  : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1587  {
1588  }
1589 
1590  exprt &component(const irep_idt &name, const namespacet &ns);
1591  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1592 };
1593 
1594 template <>
1595 inline bool can_cast_expr<struct_exprt>(const exprt &base)
1596 {
1597  return base.id() == ID_struct;
1598 }
1599 
1606 inline const struct_exprt &to_struct_expr(const exprt &expr)
1607 {
1608  PRECONDITION(expr.id()==ID_struct);
1609  return static_cast<const struct_exprt &>(expr);
1610 }
1611 
1614 {
1615  PRECONDITION(expr.id()==ID_struct);
1616  return static_cast<struct_exprt &>(expr);
1617 }
1618 
1619 
1622 {
1623 public:
1625  : binary_exprt(
1626  std::move(_real),
1627  ID_complex,
1628  std::move(_imag),
1629  std::move(_type))
1630  {
1631  }
1632 
1634  {
1635  return op0();
1636  }
1637 
1638  const exprt &real() const
1639  {
1640  return op0();
1641  }
1642 
1644  {
1645  return op1();
1646  }
1647 
1648  const exprt &imag() const
1649  {
1650  return op1();
1651  }
1652 };
1653 
1654 template <>
1655 inline bool can_cast_expr<complex_exprt>(const exprt &base)
1656 {
1657  return base.id() == ID_complex;
1658 }
1659 
1660 inline void validate_expr(const complex_exprt &value)
1661 {
1662  validate_operands(value, 2, "Complex constructor must have two operands");
1663 }
1664 
1671 inline const complex_exprt &to_complex_expr(const exprt &expr)
1672 {
1673  PRECONDITION(expr.id()==ID_complex);
1674  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1675  validate_expr(ret);
1676  return ret;
1677 }
1678 
1681 {
1682  PRECONDITION(expr.id()==ID_complex);
1683  complex_exprt &ret = static_cast<complex_exprt &>(expr);
1684  validate_expr(ret);
1685  return ret;
1686 }
1687 
1690 {
1691 public:
1692  explicit complex_real_exprt(const exprt &op)
1693  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1694  {
1695  }
1696 };
1697 
1698 template <>
1700 {
1701  return base.id() == ID_complex_real;
1702 }
1703 
1704 inline void validate_expr(const complex_real_exprt &expr)
1705 {
1707  expr, 1, "real part retrieval operation must have one operand");
1708 }
1709 
1717 {
1718  PRECONDITION(expr.id() == ID_complex_real);
1719  const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
1720  validate_expr(ret);
1721  return ret;
1722 }
1723 
1726 {
1727  PRECONDITION(expr.id() == ID_complex_real);
1728  complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
1729  validate_expr(ret);
1730  return ret;
1731 }
1732 
1735 {
1736 public:
1737  explicit complex_imag_exprt(const exprt &op)
1738  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
1739  {
1740  }
1741 };
1742 
1743 template <>
1745 {
1746  return base.id() == ID_complex_imag;
1747 }
1748 
1749 inline void validate_expr(const complex_imag_exprt &expr)
1750 {
1752  expr, 1, "imaginary part retrieval operation must have one operand");
1753 }
1754 
1762 {
1763  PRECONDITION(expr.id() == ID_complex_imag);
1764  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
1765  validate_expr(ret);
1766  return ret;
1767 }
1768 
1771 {
1772  PRECONDITION(expr.id() == ID_complex_imag);
1773  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
1774  validate_expr(ret);
1775  return ret;
1776 }
1777 
1778 
1781 {
1782 public:
1784  : unary_exprt(ID_typecast, std::move(op), std::move(_type))
1785  {
1786  }
1787 
1788  // returns a typecast if the type doesn't already match
1789  static exprt conditional_cast(const exprt &expr, const typet &type)
1790  {
1791  if(expr.type() == type)
1792  return expr;
1793  else
1794  return typecast_exprt(expr, type);
1795  }
1796 };
1797 
1798 template <>
1799 inline bool can_cast_expr<typecast_exprt>(const exprt &base)
1800 {
1801  return base.id() == ID_typecast;
1802 }
1803 
1804 inline void validate_expr(const typecast_exprt &value)
1805 {
1806  validate_operands(value, 1, "Typecast must have one operand");
1807 }
1808 
1815 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
1816 {
1817  PRECONDITION(expr.id()==ID_typecast);
1818  const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
1819  validate_expr(ret);
1820  return ret;
1821 }
1822 
1825 {
1826  PRECONDITION(expr.id()==ID_typecast);
1827  typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
1828  validate_expr(ret);
1829  return ret;
1830 }
1831 
1832 
1835 {
1836 public:
1838  : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
1839  {
1840  }
1841 
1843  : multi_ary_exprt(
1844  ID_and,
1845  {std::move(op0), std::move(op1), std::move(op2)},
1846  bool_typet())
1847  {
1848  }
1849 
1851  : multi_ary_exprt(
1852  ID_and,
1853  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
1854  bool_typet())
1855  {
1856  }
1857 
1858  explicit and_exprt(exprt::operandst _operands)
1859  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
1860  {
1861  }
1862 };
1863 
1867 
1869 
1870 template <>
1871 inline bool can_cast_expr<and_exprt>(const exprt &base)
1872 {
1873  return base.id() == ID_and;
1874 }
1875 
1882 inline const and_exprt &to_and_expr(const exprt &expr)
1883 {
1884  PRECONDITION(expr.id()==ID_and);
1885  return static_cast<const and_exprt &>(expr);
1886 }
1887 
1890 {
1891  PRECONDITION(expr.id()==ID_and);
1892  return static_cast<and_exprt &>(expr);
1893 }
1894 
1895 
1898 {
1899 public:
1901  : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
1902  {
1903  }
1904 };
1905 
1906 template <>
1907 inline bool can_cast_expr<implies_exprt>(const exprt &base)
1908 {
1909  return base.id() == ID_implies;
1910 }
1911 
1912 inline void validate_expr(const implies_exprt &value)
1913 {
1914  validate_operands(value, 2, "Implies must have two operands");
1915 }
1916 
1923 inline const implies_exprt &to_implies_expr(const exprt &expr)
1924 {
1925  PRECONDITION(expr.id()==ID_implies);
1926  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
1927  validate_expr(ret);
1928  return ret;
1929 }
1930 
1933 {
1934  PRECONDITION(expr.id()==ID_implies);
1935  implies_exprt &ret = static_cast<implies_exprt &>(expr);
1936  validate_expr(ret);
1937  return ret;
1938 }
1939 
1940 
1943 {
1944 public:
1946  : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
1947  {
1948  }
1949 
1951  : multi_ary_exprt(
1952  ID_or,
1953  {std::move(op0), std::move(op1), std::move(op2)},
1954  bool_typet())
1955  {
1956  }
1957 
1959  : multi_ary_exprt(
1960  ID_or,
1961  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
1962  bool_typet())
1963  {
1964  }
1965 
1966  explicit or_exprt(exprt::operandst _operands)
1967  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
1968  {
1969  }
1970 };
1971 
1975 
1977 
1978 template <>
1979 inline bool can_cast_expr<or_exprt>(const exprt &base)
1980 {
1981  return base.id() == ID_or;
1982 }
1983 
1990 inline const or_exprt &to_or_expr(const exprt &expr)
1991 {
1992  PRECONDITION(expr.id()==ID_or);
1993  return static_cast<const or_exprt &>(expr);
1994 }
1995 
1997 inline or_exprt &to_or_expr(exprt &expr)
1998 {
1999  PRECONDITION(expr.id()==ID_or);
2000  return static_cast<or_exprt &>(expr);
2001 }
2002 
2003 
2006 {
2007 public:
2008  xor_exprt(exprt _op0, exprt _op1)
2009  : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2010  {
2011  }
2012 };
2013 
2014 template <>
2015 inline bool can_cast_expr<xor_exprt>(const exprt &base)
2016 {
2017  return base.id() == ID_xor;
2018 }
2019 
2026 inline const xor_exprt &to_xor_expr(const exprt &expr)
2027 {
2028  PRECONDITION(expr.id()==ID_xor);
2029  return static_cast<const xor_exprt &>(expr);
2030 }
2031 
2034 {
2035  PRECONDITION(expr.id()==ID_xor);
2036  return static_cast<xor_exprt &>(expr);
2037 }
2038 
2039 
2042 {
2043 public:
2044  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2045  {
2046  PRECONDITION(as_const(*this).op().type().id() == ID_bool);
2047  }
2048 };
2049 
2050 template <>
2051 inline bool can_cast_expr<not_exprt>(const exprt &base)
2052 {
2053  return base.id() == ID_not;
2054 }
2055 
2056 inline void validate_expr(const not_exprt &value)
2057 {
2058  validate_operands(value, 1, "Not must have one operand");
2059 }
2060 
2067 inline const not_exprt &to_not_expr(const exprt &expr)
2068 {
2069  PRECONDITION(expr.id()==ID_not);
2070  const not_exprt &ret = static_cast<const not_exprt &>(expr);
2071  validate_expr(ret);
2072  return ret;
2073 }
2074 
2077 {
2078  PRECONDITION(expr.id()==ID_not);
2079  not_exprt &ret = static_cast<not_exprt &>(expr);
2080  validate_expr(ret);
2081  return ret;
2082 }
2083 
2084 
2086 class if_exprt : public ternary_exprt
2087 {
2088 public:
2090  : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2091  {
2092  }
2093 
2095  : ternary_exprt(
2096  ID_if,
2097  std::move(cond),
2098  std::move(t),
2099  std::move(f),
2100  std::move(type))
2101  {
2102  }
2103 
2105  {
2106  return op0();
2107  }
2108 
2109  const exprt &cond() const
2110  {
2111  return op0();
2112  }
2113 
2115  {
2116  return op1();
2117  }
2118 
2119  const exprt &true_case() const
2120  {
2121  return op1();
2122  }
2123 
2125  {
2126  return op2();
2127  }
2128 
2129  const exprt &false_case() const
2130  {
2131  return op2();
2132  }
2133 };
2134 
2135 template <>
2136 inline bool can_cast_expr<if_exprt>(const exprt &base)
2137 {
2138  return base.id() == ID_if;
2139 }
2140 
2141 inline void validate_expr(const if_exprt &value)
2142 {
2143  validate_operands(value, 3, "If-then-else must have three operands");
2144 }
2145 
2152 inline const if_exprt &to_if_expr(const exprt &expr)
2153 {
2154  PRECONDITION(expr.id()==ID_if);
2155  const if_exprt &ret = static_cast<const if_exprt &>(expr);
2156  validate_expr(ret);
2157  return ret;
2158 }
2159 
2161 inline if_exprt &to_if_expr(exprt &expr)
2162 {
2163  PRECONDITION(expr.id()==ID_if);
2164  if_exprt &ret = static_cast<if_exprt &>(expr);
2165  validate_expr(ret);
2166  return ret;
2167 }
2168 
2173 {
2174 public:
2175  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
2176  : expr_protectedt(
2177  ID_with,
2178  _old.type(),
2179  {_old, std::move(_where), std::move(_new_value)})
2180  {
2181  }
2182 
2184  {
2185  return op0();
2186  }
2187 
2188  const exprt &old() const
2189  {
2190  return op0();
2191  }
2192 
2194  {
2195  return op1();
2196  }
2197 
2198  const exprt &where() const
2199  {
2200  return op1();
2201  }
2202 
2204  {
2205  return op2();
2206  }
2207 
2208  const exprt &new_value() const
2209  {
2210  return op2();
2211  }
2212 };
2213 
2214 template <>
2215 inline bool can_cast_expr<with_exprt>(const exprt &base)
2216 {
2217  return base.id() == ID_with;
2218 }
2219 
2220 inline void validate_expr(const with_exprt &value)
2221 {
2223  value, 3, "array/structure update must have at least 3 operands", true);
2225  value.operands().size() % 2 == 1,
2226  "array/structure update must have an odd number of operands");
2227 }
2228 
2235 inline const with_exprt &to_with_expr(const exprt &expr)
2236 {
2237  PRECONDITION(expr.id()==ID_with);
2238  const with_exprt &ret = static_cast<const with_exprt &>(expr);
2239  validate_expr(ret);
2240  return ret;
2241 }
2242 
2245 {
2246  PRECONDITION(expr.id()==ID_with);
2247  with_exprt &ret = static_cast<with_exprt &>(expr);
2248  validate_expr(ret);
2249  return ret;
2250 }
2251 
2253 {
2254 public:
2255  explicit index_designatort(exprt _index)
2256  : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
2257  {
2258  }
2259 
2260  const exprt &index() const
2261  {
2262  return op0();
2263  }
2264 
2266  {
2267  return op0();
2268  }
2269 };
2270 
2271 template <>
2272 inline bool can_cast_expr<index_designatort>(const exprt &base)
2273 {
2274  return base.id() == ID_index_designator;
2275 }
2276 
2277 inline void validate_expr(const index_designatort &value)
2278 {
2279  validate_operands(value, 1, "Index designator must have one operand");
2280 }
2281 
2288 inline const index_designatort &to_index_designator(const exprt &expr)
2289 {
2290  PRECONDITION(expr.id()==ID_index_designator);
2291  const index_designatort &ret = static_cast<const index_designatort &>(expr);
2292  validate_expr(ret);
2293  return ret;
2294 }
2295 
2298 {
2299  PRECONDITION(expr.id()==ID_index_designator);
2300  index_designatort &ret = static_cast<index_designatort &>(expr);
2301  validate_expr(ret);
2302  return ret;
2303 }
2304 
2306 {
2307 public:
2308  explicit member_designatort(const irep_idt &_component_name)
2309  : expr_protectedt(ID_member_designator, typet())
2310  {
2311  set(ID_component_name, _component_name);
2312  }
2313 
2315  {
2316  return get(ID_component_name);
2317  }
2318 };
2319 
2320 template <>
2322 {
2323  return base.id() == ID_member_designator;
2324 }
2325 
2326 inline void validate_expr(const member_designatort &value)
2327 {
2328  validate_operands(value, 0, "Member designator must not have operands");
2329 }
2330 
2338 {
2339  PRECONDITION(expr.id()==ID_member_designator);
2340  const member_designatort &ret = static_cast<const member_designatort &>(expr);
2341  validate_expr(ret);
2342  return ret;
2343 }
2344 
2347 {
2348  PRECONDITION(expr.id()==ID_member_designator);
2349  member_designatort &ret = static_cast<member_designatort &>(expr);
2350  validate_expr(ret);
2351  return ret;
2352 }
2353 
2354 
2357 {
2358 public:
2359  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
2360  : ternary_exprt(
2361  ID_update,
2362  _old,
2363  std::move(_designator),
2364  std::move(_new_value),
2365  _old.type())
2366  {
2367  }
2368 
2370  {
2371  return op0();
2372  }
2373 
2374  const exprt &old() const
2375  {
2376  return op0();
2377  }
2378 
2379  // the designator operands are either
2380  // 1) member_designator or
2381  // 2) index_designator
2382  // as defined above
2384  {
2385  return op1().operands();
2386  }
2387 
2389  {
2390  return op1().operands();
2391  }
2392 
2394  {
2395  return op2();
2396  }
2397 
2398  const exprt &new_value() const
2399  {
2400  return op2();
2401  }
2402 };
2403 
2404 template <>
2405 inline bool can_cast_expr<update_exprt>(const exprt &base)
2406 {
2407  return base.id() == ID_update;
2408 }
2409 
2410 inline void validate_expr(const update_exprt &value)
2411 {
2413  value, 3, "Array/structure update must have three operands");
2414 }
2415 
2422 inline const update_exprt &to_update_expr(const exprt &expr)
2423 {
2424  PRECONDITION(expr.id()==ID_update);
2425  const update_exprt &ret = static_cast<const update_exprt &>(expr);
2426  validate_expr(ret);
2427  return ret;
2428 }
2429 
2432 {
2433  PRECONDITION(expr.id()==ID_update);
2434  update_exprt &ret = static_cast<update_exprt &>(expr);
2435  validate_expr(ret);
2436  return ret;
2437 }
2438 
2439 
2440 #if 0
2441 class array_update_exprt:public expr_protectedt
2443 {
2444 public:
2445  array_update_exprt(
2446  const exprt &_array,
2447  const exprt &_index,
2448  const exprt &_new_value):
2449  exprt(ID_array_update, _array.type())
2450  {
2451  add_to_operands(_array, _index, _new_value);
2452  }
2453 
2454  array_update_exprt():expr_protectedt(ID_array_update)
2455  {
2456  operands().resize(3);
2457  }
2458 
2459  exprt &array()
2460  {
2461  return op0();
2462  }
2463 
2464  const exprt &array() const
2465  {
2466  return op0();
2467  }
2468 
2469  exprt &index()
2470  {
2471  return op1();
2472  }
2473 
2474  const exprt &index() const
2475  {
2476  return op1();
2477  }
2478 
2479  exprt &new_value()
2480  {
2481  return op2();
2482  }
2483 
2484  const exprt &new_value() const
2485  {
2486  return op2();
2487  }
2488 };
2489 
2490 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2491 {
2492  return base.id()==ID_array_update;
2493 }
2494 
2495 inline void validate_expr(const array_update_exprt &value)
2496 {
2497  validate_operands(value, 3, "Array update must have three operands");
2498 }
2499 
2506 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2507 {
2508  PRECONDITION(expr.id()==ID_array_update);
2509  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2510  validate_expr(ret);
2511  return ret;
2512 }
2513 
2515 inline array_update_exprt &to_array_update_expr(exprt &expr)
2516 {
2517  PRECONDITION(expr.id()==ID_array_update);
2518  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2519  validate_expr(ret);
2520  return ret;
2521 }
2522 
2523 #endif
2524 
2525 
2528 {
2529 public:
2530  member_exprt(exprt op, const irep_idt &component_name, typet _type)
2531  : unary_exprt(ID_member, std::move(op), std::move(_type))
2532  {
2533  set_component_name(component_name);
2534  }
2535 
2537  : unary_exprt(ID_member, std::move(op), c.type())
2538  {
2540  }
2541 
2543  {
2544  return get(ID_component_name);
2545  }
2546 
2547  void set_component_name(const irep_idt &component_name)
2548  {
2549  set(ID_component_name, component_name);
2550  }
2551 
2552  std::size_t get_component_number() const
2553  {
2554  return get_size_t(ID_component_number);
2555  }
2556 
2557  // will go away, use compound()
2558  const exprt &struct_op() const
2559  {
2560  return op0();
2561  }
2562 
2563  // will go away, use compound()
2565  {
2566  return op0();
2567  }
2568 
2569  const exprt &compound() const
2570  {
2571  return op0();
2572  }
2573 
2575  {
2576  return op0();
2577  }
2578 
2579  static void check(
2580  const exprt &expr,
2582  {
2583  DATA_CHECK(
2584  vm,
2585  expr.operands().size() == 1,
2586  "member expression must have one operand");
2587  }
2588 
2589  static void validate(
2590  const exprt &expr,
2591  const namespacet &ns,
2593 };
2594 
2595 template <>
2596 inline bool can_cast_expr<member_exprt>(const exprt &base)
2597 {
2598  return base.id() == ID_member;
2599 }
2600 
2601 inline void validate_expr(const member_exprt &value)
2602 {
2603  validate_operands(value, 1, "Extract member must have one operand");
2604 }
2605 
2612 inline const member_exprt &to_member_expr(const exprt &expr)
2613 {
2614  PRECONDITION(expr.id()==ID_member);
2615  const member_exprt &ret = static_cast<const member_exprt &>(expr);
2616  validate_expr(ret);
2617  return ret;
2618 }
2619 
2622 {
2623  PRECONDITION(expr.id()==ID_member);
2624  member_exprt &ret = static_cast<member_exprt &>(expr);
2625  validate_expr(ret);
2626  return ret;
2627 }
2628 
2629 
2632 {
2633 public:
2634  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
2635  {
2636  }
2637 };
2638 
2639 template <>
2640 inline bool can_cast_expr<type_exprt>(const exprt &base)
2641 {
2642  return base.id() == ID_type;
2643 }
2644 
2651 inline const type_exprt &to_type_expr(const exprt &expr)
2652 {
2654  const type_exprt &ret = static_cast<const type_exprt &>(expr);
2655  return ret;
2656 }
2657 
2660 {
2662  type_exprt &ret = static_cast<type_exprt &>(expr);
2663  return ret;
2664 }
2665 
2668 {
2669 public:
2670  constant_exprt(const irep_idt &_value, typet _type)
2671  : expr_protectedt(ID_constant, std::move(_type))
2672  {
2673  set_value(_value);
2674  }
2675 
2676  const irep_idt &get_value() const
2677  {
2678  return get(ID_value);
2679  }
2680 
2681  void set_value(const irep_idt &value)
2682  {
2683  set(ID_value, value);
2684  }
2685 
2686  bool value_is_zero_string() const;
2687 };
2688 
2689 template <>
2690 inline bool can_cast_expr<constant_exprt>(const exprt &base)
2691 {
2692  return base.id() == ID_constant;
2693 }
2694 
2701 inline const constant_exprt &to_constant_expr(const exprt &expr)
2702 {
2703  PRECONDITION(expr.id()==ID_constant);
2704  return static_cast<const constant_exprt &>(expr);
2705 }
2706 
2709 {
2710  PRECONDITION(expr.id()==ID_constant);
2711  return static_cast<constant_exprt &>(expr);
2712 }
2713 
2714 
2717 {
2718 public:
2720  {
2721  }
2722 };
2723 
2726 {
2727 public:
2729  {
2730  }
2731 };
2732 
2734 class nil_exprt : public nullary_exprt
2735 {
2736 public:
2738  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
2739  {
2740  }
2741 };
2742 
2743 template <>
2744 inline bool can_cast_expr<nil_exprt>(const exprt &base)
2745 {
2746  return base.id() == ID_nil;
2747 }
2748 
2751 {
2752 public:
2754  : constant_exprt(ID_NULL, std::move(type))
2755  {
2756  }
2757 };
2758 
2759 
2762 {
2763 public:
2764  explicit infinity_exprt(typet _type)
2765  : nullary_exprt(ID_infinity, std::move(_type))
2766  {
2767  }
2768 };
2769 
2772 {
2773 public:
2774  using variablest = std::vector<symbol_exprt>;
2775 
2778  irep_idt _id,
2779  const variablest &_variables,
2780  exprt _where,
2781  typet _type)
2782  : binary_exprt(
2784  ID_tuple,
2785  (const operandst &)_variables,
2786  typet(ID_tuple)),
2787  _id,
2788  std::move(_where),
2789  std::move(_type))
2790  {
2791  }
2792 
2794  {
2795  return (variablest &)to_multi_ary_expr(op0()).operands();
2796  }
2797 
2798  const variablest &variables() const
2799  {
2800  return (variablest &)to_multi_ary_expr(op0()).operands();
2801  }
2802 
2804  {
2805  return op1();
2806  }
2807 
2808  const exprt &where() const
2809  {
2810  return op1();
2811  }
2812 };
2813 
2815 class let_exprt : public binary_exprt
2816 {
2817 public:
2820  operandst values,
2821  const exprt &where)
2822  : binary_exprt(
2823  binding_exprt(
2824  ID_let_binding,
2825  std::move(variables),
2826  where,
2827  where.type()),
2828  ID_let,
2829  multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
2830  where.type())
2831  {
2832  PRECONDITION(this->variables().size() == this->values().size());
2833  }
2834 
2837  : let_exprt(
2838  binding_exprt::variablest{std::move(symbol)},
2839  operandst{std::move(value)},
2840  where)
2841  {
2842  }
2843 
2845  {
2846  return static_cast<binding_exprt &>(op0());
2847  }
2848 
2849  const binding_exprt &binding() const
2850  {
2851  return static_cast<const binding_exprt &>(op0());
2852  }
2853 
2856  {
2857  auto &variables = binding().variables();
2858  PRECONDITION(variables.size() == 1);
2859  return variables.front();
2860  }
2861 
2863  const symbol_exprt &symbol() const
2864  {
2865  const auto &variables = binding().variables();
2866  PRECONDITION(variables.size() == 1);
2867  return variables.front();
2868  }
2869 
2872  {
2873  auto &values = this->values();
2874  PRECONDITION(values.size() == 1);
2875  return values.front();
2876  }
2877 
2879  const exprt &value() const
2880  {
2881  const auto &values = this->values();
2882  PRECONDITION(values.size() == 1);
2883  return values.front();
2884  }
2885 
2887  {
2888  return static_cast<multi_ary_exprt &>(op1()).operands();
2889  }
2890 
2891  const operandst &values() const
2892  {
2893  return static_cast<const multi_ary_exprt &>(op1()).operands();
2894  }
2895 
2898  {
2899  return binding().variables();
2900  }
2901 
2904  {
2905  return binding().variables();
2906  }
2907 
2910  {
2911  return binding().where();
2912  }
2913 
2915  const exprt &where() const
2916  {
2917  return binding().where();
2918  }
2919 
2920  static void validate(const exprt &, validation_modet);
2921 };
2922 
2923 template <>
2924 inline bool can_cast_expr<let_exprt>(const exprt &base)
2925 {
2926  return base.id() == ID_let;
2927 }
2928 
2929 inline void validate_expr(const let_exprt &let_expr)
2930 {
2931  validate_operands(let_expr, 2, "Let must have two operands");
2932 }
2933 
2940 inline const let_exprt &to_let_expr(const exprt &expr)
2941 {
2942  PRECONDITION(expr.id()==ID_let);
2943  const let_exprt &ret = static_cast<const let_exprt &>(expr);
2944  validate_expr(ret);
2945  return ret;
2946 }
2947 
2950 {
2951  PRECONDITION(expr.id()==ID_let);
2952  let_exprt &ret = static_cast<let_exprt &>(expr);
2953  validate_expr(ret);
2954  return ret;
2955 }
2956 
2957 
2962 {
2963 public:
2964  cond_exprt(operandst _operands, typet _type)
2965  : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
2966  {
2967  }
2968 
2972  void add_case(const exprt &condition, const exprt &value)
2973  {
2974  PRECONDITION(condition.type().id() == ID_bool);
2975  operands().reserve(operands().size() + 2);
2976  operands().push_back(condition);
2977  operands().push_back(value);
2978  }
2979 };
2980 
2981 template <>
2982 inline bool can_cast_expr<cond_exprt>(const exprt &base)
2983 {
2984  return base.id() == ID_cond;
2985 }
2986 
2987 inline void validate_expr(const cond_exprt &value)
2988 {
2990  value.operands().size() % 2 == 0, "cond must have even number of operands");
2991 }
2992 
2999 inline const cond_exprt &to_cond_expr(const exprt &expr)
3000 {
3001  PRECONDITION(expr.id() == ID_cond);
3002  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3003  validate_expr(ret);
3004  return ret;
3005 }
3006 
3009 {
3010  PRECONDITION(expr.id() == ID_cond);
3011  cond_exprt &ret = static_cast<cond_exprt &>(expr);
3012  validate_expr(ret);
3013  return ret;
3014 }
3015 
3025 {
3026 public:
3028  symbol_exprt arg,
3029  exprt body,
3030  array_typet _type)
3031  : binary_exprt(
3032  std::move(arg),
3033  ID_array_comprehension,
3034  std::move(body),
3035  std::move(_type))
3036  {
3037  }
3038 
3039  const array_typet &type() const
3040  {
3041  return static_cast<const array_typet &>(binary_exprt::type());
3042  }
3043 
3045  {
3046  return static_cast<array_typet &>(binary_exprt::type());
3047  }
3048 
3049  const symbol_exprt &arg() const
3050  {
3051  return static_cast<const symbol_exprt &>(op0());
3052  }
3053 
3055  {
3056  return static_cast<symbol_exprt &>(op0());
3057  }
3058 
3059  const exprt &body() const
3060  {
3061  return op1();
3062  }
3063 
3065  {
3066  return op1();
3067  }
3068 };
3069 
3070 template <>
3072 {
3073  return base.id() == ID_array_comprehension;
3074 }
3075 
3076 inline void validate_expr(const array_comprehension_exprt &value)
3077 {
3078  validate_operands(value, 2, "'Array comprehension' must have two operands");
3079 }
3080 
3087 inline const array_comprehension_exprt &
3089 {
3090  PRECONDITION(expr.id() == ID_array_comprehension);
3091  const array_comprehension_exprt &ret =
3092  static_cast<const array_comprehension_exprt &>(expr);
3093  validate_expr(ret);
3094  return ret;
3095 }
3096 
3099 {
3100  PRECONDITION(expr.id() == ID_array_comprehension);
3102  static_cast<array_comprehension_exprt &>(expr);
3103  validate_expr(ret);
3104  return ret;
3105 }
3106 
3107 inline void validate_expr(const class class_method_descriptor_exprt &value);
3108 
3111 {
3112 public:
3128  typet _type,
3132  : nullary_exprt(ID_virtual_function, std::move(_type))
3133  {
3135  set(ID_component_name, std::move(mangled_method_name));
3136  set(ID_C_class, std::move(class_id));
3137  set(ID_C_base_name, std::move(base_method_name));
3138  set(ID_identifier, std::move(id));
3139  validate_expr(*this);
3140  }
3141 
3149  {
3150  return get(ID_component_name);
3151  }
3152 
3156  const irep_idt &class_id() const
3157  {
3158  return get(ID_C_class);
3159  }
3160 
3164  {
3165  return get(ID_C_base_name);
3166  }
3167 
3171  const irep_idt &get_identifier() const
3172  {
3173  return get(ID_identifier);
3174  }
3175 };
3176 
3177 inline void validate_expr(const class class_method_descriptor_exprt &value)
3178 {
3179  validate_operands(value, 0, "class method descriptor must not have operands");
3181  !value.mangled_method_name().empty(),
3182  "class method descriptor must have a mangled method name.");
3184  !value.class_id().empty(), "class method descriptor must have a class id.");
3186  !value.base_method_name().empty(),
3187  "class method descriptor must have a base method name.");
3189  value.get_identifier() == id2string(value.class_id()) + "." +
3190  id2string(value.mangled_method_name()),
3191  "class method descriptor must have an identifier in the expected format.");
3192 }
3193 
3200 inline const class_method_descriptor_exprt &
3202 {
3203  PRECONDITION(expr.id() == ID_virtual_function);
3204  const class_method_descriptor_exprt &ret =
3205  static_cast<const class_method_descriptor_exprt &>(expr);
3206  validate_expr(ret);
3207  return ret;
3208 }
3209 
3210 template <>
3212 {
3213  return base.id() == ID_virtual_function;
3214 }
3215 
3216 #endif // CPROVER_UTIL_STD_EXPR_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
nullary_exprt::op1
exprt & op1()=delete
index_exprt::array
const exprt & array() const
Definition: std_expr.h:1264
exprt::op2
exprt & op2()
Definition: expr.h:109
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
if_exprt::if_exprt
if_exprt(exprt cond, const exprt &t, exprt f)
Definition: std_expr.h:2089
can_cast_expr< symbol_exprt >
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:174
to_array_comprehension_expr
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3088
unary_exprt::op1
exprt & op1()=delete
to_vector_expr
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1501
can_cast_expr< union_exprt >
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1547
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2422
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
can_cast_expr< rem_exprt >
bool can_cast_expr< rem_exprt >(const exprt &base)
Definition: std_expr.h:1104
index_exprt::index
const exprt & index() const
Definition: std_expr.h:1274
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:741
binary_relation_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:682
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
let_exprt::let_exprt
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition: std_expr.h:2836
can_cast_expr< cond_exprt >
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition: std_expr.h:2982
member_exprt::member_exprt
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition: std_expr.h:2530
can_cast_expr< array_list_exprt >
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1453
can_cast_expr< mod_exprt >
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1059
binding_exprt::where
const exprt & where() const
Definition: std_expr.h:2808
if_exprt::if_exprt
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition: std_expr.h:2094
member_designatort::member_designatort
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:2308
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1030
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:591
can_cast_expr< index_designatort >
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:2272
class_method_descriptor_exprt::mangled_method_name
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition: std_expr.h:3148
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:1850
array_list_exprt::array_list_exprt
array_list_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1430
nullary_exprt::operands
const operandst & operands() const =delete
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1412
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:210
and_exprt::and_exprt
and_exprt(exprt::operandst _operands)
Definition: std_expr.h:1858
can_cast_expr< complex_imag_exprt >
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:1744
nullary_exprt::copy_to_operands
void copy_to_operands(const exprt &, const exprt &)=delete
nondet_symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:238
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1334
ternary_exprt::op2
exprt & op2()
Definition: expr.h:109
binary_exprt::rhs
const exprt & rhs() const
Definition: std_expr.h:596
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
complex_exprt::real
const exprt & real() const
Definition: std_expr.h:1638
unary_minus_exprt::unary_minus_exprt
unary_minus_exprt(exprt _op, typet _type)
Definition: std_expr.h:393
to_type_expr
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition: std_expr.h:2651
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:754
can_cast_expr< not_exprt >
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:2051
typet
The type of an expression, extends irept.
Definition: type.h:28
update_exprt::old
exprt & old()
Definition: std_expr.h:2369
binary_relation_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:689
ternary_exprt
An expression with three operands.
Definition: std_expr.h:54
true_exprt::true_exprt
true_exprt()
Definition: std_expr.h:2719
mult_exprt::mult_exprt
mult_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:938
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
can_cast_expr< sign_exprt >
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:516
symbol_exprt::symbol_exprt
symbol_exprt(typet type)
Definition: std_expr.h:84
can_cast_expr< unary_exprt >
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:313
if_exprt::true_case
const exprt & true_case() const
Definition: std_expr.h:2119
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2087
member_designatort
Definition: std_expr.h:2306
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:100
div_exprt::div_exprt
div_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:983
validate_operands
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
array_list_exprt::type
array_typet & type()
Definition: std_expr.h:1440
xor_exprt
Boolean XOR.
Definition: std_expr.h:2006
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2203
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:833
binary_predicate_exprt::binary_predicate_exprt
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition: std_expr.h:646
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1690
let_exprt::symbol
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:2855
and_exprt
Boolean AND.
Definition: std_expr.h:1835
union_exprt
Union constructor from single element.
Definition: std_expr.h:1517
array_comprehension_exprt::type
array_typet & type()
Definition: std_expr.h:3044
disjunction
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:29
ternary_exprt::op1
exprt & op1()
Definition: expr.h:106
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1362
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:831
can_cast_expr< xor_exprt >
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2015
rem_exprt
Remainder of division.
Definition: std_expr.h:1095
equal_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1154
can_cast_expr< unary_minus_exprt >
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:405
abs_exprt::abs_exprt
abs_exprt(exprt _op)
Definition: std_expr.h:349
exprt
Base class for all expressions.
Definition: expr.h:54
class_method_descriptor_exprt::class_method_descriptor_exprt
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition: std_expr.h:3127
unary_exprt::op1
const exprt & op1() const =delete
to_complex_expr
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1671
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:581
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:282
array_exprt::array_exprt
array_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1384
index_exprt::index_exprt
index_exprt(exprt _array, exprt _index, typet _type)
Definition: std_expr.h:1250
decorated_symbol_exprt::clear_static_lifetime
void clear_static_lifetime()
Definition: std_expr.h:152
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1563
array_of_exprt::type
array_typet & type()
Definition: std_expr.h:1329
member_designatort::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2314
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1804
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:1958
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:507
can_cast_expr< binary_exprt >
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:612
update_exprt::designator
const exprt::operandst & designator() const
Definition: std_expr.h:2388
array_of_exprt::type
const array_typet & type() const
Definition: std_expr.h:1324
exprt::op0
exprt & op0()
Definition: expr.h:103
predicate_exprt::predicate_exprt
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:487
update_exprt::old
const exprt & old() const
Definition: std_expr.h:2374
let_exprt::validate
static void validate(const exprt &, validation_modet)
Definition: std_expr.cpp:121
array_comprehension_exprt::arg
const symbol_exprt & arg() const
Definition: std_expr.h:3049
cond_exprt::cond_exprt
cond_exprt(operandst _operands, typet _type)
Definition: std_expr.h:2964
can_cast_expr< minus_exprt >
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:899
expr_protectedt::op1
exprt & op1()
Definition: expr.h:106
to_array_list_expr
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1463
vector_typet
The vector type.
Definition: std_types.h:1764
bool_typet
The Boolean type.
Definition: std_types.h:37
index_designatort::index_designatort
index_designatort(exprt _index)
Definition: std_expr.h:2255
nullary_exprt::copy_to_operands
void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete
nullary_exprt::move_to_operands
void move_to_operands(exprt &)=delete
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1481
binary_exprt::op3
exprt & op3()=delete
std::hash<::symbol_exprt >::operator()
size_t operator()(const ::symbol_exprt &sym)
Definition: std_expr.h:123
index_exprt::index_exprt
index_exprt(const exprt &_array, exprt _index)
Definition: std_expr.h:1245
type_exprt::type_exprt
type_exprt(typet type)
Definition: std_expr.h:2634
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1829
div_exprt
Division.
Definition: std_expr.h:981
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
can_cast_expr< array_exprt >
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1401
validate_expr
void validate_expr(const symbol_exprt &value)
Definition: std_expr.h:179
can_cast_expr< member_exprt >
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:2596
minus_exprt::minus_exprt
minus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:892
union_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:1535
equal_exprt
Equality.
Definition: std_expr.h:1140
array_comprehension_exprt::type
const array_typet & type() const
Definition: std_expr.h:3039
multi_ary_exprt::op2
exprt & op2()
Definition: std_expr.h:773
expanding_vectort
Definition: expanding_vector.h:17
to_rem_expr
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
Definition: std_expr.h:1120
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:915
can_cast_expr< equal_exprt >
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1164
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:2762
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2124
array_list_exprt::add
void add(exprt index, exprt value)
add an index/value pair
Definition: std_expr.h:1446
can_cast_expr< implies_exprt >
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:1907
notequal_exprt
Disequality.
Definition: std_expr.h:1198
binary_exprt::op3
const exprt & op3() const =delete
union_exprt::set_component_name
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1530
multi_ary_exprt::op3
exprt & op3()
Definition: std_expr.h:779
nullary_exprt::op3
const exprt & op3() const =delete
to_unary_plus_expr
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:465
array_comprehension_exprt::arg
symbol_exprt & arg()
Definition: std_expr.h:3054
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1716
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
binding_exprt::variables
variablest & variables()
Definition: std_expr.h:2793
narrow.h
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:3111
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1583
let_exprt::variables
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition: std_expr.h:2903
union_exprt::union_exprt
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition: std_expr.h:1519
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
complex_exprt::imag
exprt imag()
Definition: std_expr.h:1643
to_nondet_symbol_expr
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:261
let_exprt::variables
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:2897
class_method_descriptor_exprt::get_identifier
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:3171
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
let_exprt::value
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:2871
or_exprt::or_exprt
or_exprt(exprt::operandst _operands)
Definition: std_expr.h:1966
nullary_exprt
An expression without operands.
Definition: std_expr.h:23
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
can_cast_expr< let_exprt >
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:2924
not_exprt::not_exprt
not_exprt(exprt _op)
Definition: std_expr.h:2044
can_cast_expr< and_exprt >
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:1871
member_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:2552
array_exprt::type
const array_typet & type() const
Definition: std_expr.h:1389
with_exprt::where
const exprt & where() const
Definition: std_expr.h:2198
with_exprt::old
exprt & old()
Definition: std_expr.h:2183
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition: std_expr.h:838
expr_protectedt::op0
exprt & op0()
Definition: expr.h:103
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:1842
to_cond_expr
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:2999
with_exprt::with_exprt
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition: std_expr.h:2175
xor_exprt::xor_exprt
xor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2008
rem_exprt::rem_exprt
rem_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1097
notequal_exprt::notequal_exprt
notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1200
nullary_exprt::move_to_operands
void move_to_operands(exprt &, exprt &, exprt &)=delete
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
let_exprt::value
const exprt & value() const
convenience accessor for the value of a single binding
Definition: std_expr.h:2879
or_exprt
Boolean OR.
Definition: std_expr.h:1943
nullary_exprt::op2
exprt & op2()=delete
can_cast_expr< abs_exprt >
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:355
array_exprt::type
array_typet & type()
Definition: std_expr.h:1394
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1075
complex_real_exprt::complex_real_exprt
complex_real_exprt(const exprt &op)
Definition: std_expr.h:1692
member_exprt::struct_op
exprt & struct_op()
Definition: std_expr.h:2564
update_exprt::update_exprt
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition: std_expr.h:2359
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1)
Definition: std_expr.h:1837
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
class_method_descriptor_exprt::base_method_name
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:3163
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:961
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:2751
array_comprehension_exprt::array_comprehension_exprt
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition: std_expr.h:3027
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
member_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2579
decorated_symbol_exprt::set_static_lifetime
void set_static_lifetime()
Definition: std_expr.h:147
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:74
binary_exprt::op2
exprt & op2()=delete
symbol_exprt::symbol_exprt
symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:90
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2569
ternary_exprt::ternary_exprt
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition: std_expr.h:57
predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:485
multi_ary_exprt::op1
const exprt & op1() const
Definition: std_expr.h:791
can_cast_expr< plus_exprt >
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:854
update_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:2398
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2558
to_xor_expr
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2026
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:644
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:767
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nullary_exprt::operands
operandst & operands()=delete
remove all operand methods
can_cast_expr< array_of_exprt >
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1346
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
ternary_exprt::op0
exprt & op0()
Definition: expr.h:103
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1317
nondet_symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:233
index_designatort::index
const exprt & index() const
Definition: std_expr.h:2260
conjunction
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:41
decorated_symbol_exprt::is_thread_local
bool is_thread_local() const
Definition: std_expr.h:157
std_types.h
Pre-defined types.
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2940
can_cast_expr< notequal_exprt >
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1207
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:870
cond_exprt::add_case
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:2972
can_cast_expr< nil_exprt >
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition: std_expr.h:2744
array_comprehension_exprt::body
const exprt & body() const
Definition: std_expr.h:3059
member_exprt::compound
exprt & compound()
Definition: std_expr.h:2574
exprt::op1
exprt & op1()
Definition: expr.h:106
null_pointer_exprt::null_pointer_exprt
null_pointer_exprt(pointer_typet type)
Definition: std_expr.h:2753
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1223
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:936
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:2774
with_exprt::old
const exprt & old() const
Definition: std_expr.h:2188
index_exprt::index
exprt & index()
Definition: std_expr.h:1269
nil_exprt::nil_exprt
nil_exprt()
Definition: std_expr.h:2737
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:421
decorated_symbol_exprt::set_thread_local
void set_thread_local()
Definition: std_expr.h:162
mod_exprt::mod_exprt
mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1052
nullary_exprt::op3
exprt & op3()=delete
nondet_symbol_exprt::nondet_symbol_exprt
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition: std_expr.h:223
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:391
index_exprt::array
exprt & array()
Definition: std_expr.h:1259
ternary_exprt::op3
const exprt & op3() const =delete
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
binding_exprt::variables
const variablest & variables() const
Definition: std_expr.h:2798
member_exprt::validate
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:88
struct_exprt::struct_exprt
struct_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1585
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:407
binary_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:563
let_exprt::binding
const binding_exprt & binding() const
Definition: std_expr.h:2849
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
binding_exprt
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:2772
can_cast_expr< div_exprt >
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1014
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1622
dstringt::empty
bool empty() const
Definition: dstring.h:88
abs_exprt
Absolute value.
Definition: std_expr.h:347
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
let_exprt::values
const operandst & values() const
Definition: std_expr.h:2891
vector_exprt::vector_exprt
vector_exprt(operandst _operands, vector_typet _type)
Definition: std_expr.h:1483
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:440
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition: std_expr.h:743
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
if_exprt::cond
const exprt & cond() const
Definition: std_expr.h:2109
unary_exprt::op3
exprt & op3()=delete
let_exprt::let_exprt
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition: std_expr.h:2818
div_exprt::dividend
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:995
index_designatort
Definition: std_expr.h:2253
complex_exprt::imag
const exprt & imag() const
Definition: std_expr.h:1648
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1761
binary_predicate_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:651
array_list_exprt::type
const array_typet & type() const
Definition: std_expr.h:1435
div_exprt::divisor
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1001
binary_relation_exprt::binary_relation_exprt
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:677
unary_exprt::unary_exprt
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition: std_expr.h:289
minus_exprt
Binary minus.
Definition: std_expr.h:890
div_exprt::dividend
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:989
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2235
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2357
nullary_exprt::op0
const exprt & op0() const =delete
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:2383
binary_exprt::validate
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:573
multi_ary_exprt::op0
const exprt & op0() const
Definition: std_expr.h:785
source_locationt
Definition: source_location.h:20
unary_plus_exprt::unary_plus_exprt
unary_plus_exprt(exprt op)
Definition: std_expr.h:442
irep_id_hash
dstring_hash irep_id_hash
Definition: irep.h:40
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:1990
can_cast_expr< index_exprt >
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1281
unary_exprt::unary_exprt
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:284
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1525
unary_exprt::op2
exprt & op2()=delete
ternary_exprt::op3
exprt & op3()=delete
sign_exprt::sign_exprt
sign_exprt(exprt _op)
Definition: std_expr.h:509
unary_minus_exprt::unary_minus_exprt
unary_minus_exprt(exprt _op)
Definition: std_expr.h:398
nullary_exprt::op0
exprt & op0()=delete
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2528
struct_union_typet::componentt
Definition: std_types.h:64
can_cast_expr< binary_relation_exprt >
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:708
equal_exprt::equal_exprt
equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1142
decorated_symbol_exprt
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition: std_expr.h:133
can_cast_expr< complex_real_exprt >
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:1699
type_exprt
An expression denoting a type.
Definition: std_expr.h:2632
can_cast_expr< array_comprehension_exprt >
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition: std_expr.h:3071
plus_exprt::plus_exprt
plus_exprt(operandst _operands, typet _type)
Definition: std_expr.h:847
cond_exprt
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:2962
equal_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1147
infinity_exprt::infinity_exprt
infinity_exprt(typet _type)
Definition: std_expr.h:2764
binding_exprt::binding_exprt
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition: std_expr.h:2777
array_typet
Arrays with given size.
Definition: std_types.h:968
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2114
binding_exprt::where
exprt & where()
Definition: std_expr.h:2803
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:74
can_cast_expr< or_exprt >
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:1979
nullary_exprt::copy_to_operands
void copy_to_operands(const exprt &expr)=delete
decorated_symbol_exprt::decorated_symbol_exprt
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:137
to_sign_expr
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:532
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2067
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
can_cast_expr< class_method_descriptor_exprt >
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:3211
to_class_method_descriptor_expr
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:3201
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:23
update_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2393
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:1923
member_exprt::member_exprt
member_exprt(exprt op, const struct_typet::componentt &c)
Definition: std_expr.h:2536
unary_exprt::op2
const exprt & op2() const =delete
can_cast_expr< type_exprt >
bool can_cast_expr< type_exprt >(const exprt &base)
Definition: std_expr.h:2640
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
if_exprt::false_case
const exprt & false_case() const
Definition: std_expr.h:2129
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2104
binary_exprt::binary_exprt
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:558
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
typecast_exprt::typecast_exprt
typecast_exprt(exprt op, typet _type)
Definition: std_expr.h:1783
invariant.h
expr_cast.h
Templated functions to cast to specific exprt-derived classes.
nullary_exprt::op1
const exprt & op1() const =delete
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1735
can_cast_expr< nondet_symbol_exprt >
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:245
nullary_exprt::nullary_exprt
nullary_exprt(const irep_idt &_id, typet _type)
Definition: std_expr.h:25
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1180
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:140
binary_exprt::lhs
const exprt & lhs() const
Definition: std_expr.h:586
binary_exprt::binary_exprt
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:553
decorated_symbol_exprt::clear_thread_local
void clear_thread_local()
Definition: std_expr.h:167
array_comprehension_exprt::body
exprt & body()
Definition: std_expr.h:3064
class_method_descriptor_exprt::class_id
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:3156
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:1950
unary_exprt::op
exprt & op()
Definition: std_expr.h:299
multi_ary_exprt::op2
const exprt & op2() const
Definition: std_expr.h:797
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
can_cast_expr< typecast_exprt >
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:1799
can_cast_expr< vector_exprt >
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1490
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2542
complex_exprt::complex_exprt
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition: std_expr.h:1624
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
implies_exprt
Boolean implication.
Definition: std_expr.h:1898
let_exprt::where
const exprt & where() const
convenience accessor for binding().where()
Definition: std_expr.h:2915
can_cast_expr< if_exprt >
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:2136
array_of_exprt::what
const exprt & what() const
Definition: std_expr.h:1339
struct_exprt::component
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:69
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1428
constant_exprt::constant_exprt
constant_exprt(const irep_idt &_value, typet _type)
Definition: std_expr.h:2670
can_cast_expr< constant_exprt >
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2690
exprt::operands
operandst & operands()
Definition: expr.h:96
decorated_symbol_exprt::is_static_lifetime
bool is_static_lifetime() const
Definition: std_expr.h:142
can_cast_expr< complex_exprt >
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:1655
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1)
Definition: std_expr.h:1945
let_exprt::values
operandst & values()
Definition: std_expr.h:2886
false_exprt::false_exprt
false_exprt()
Definition: std_expr.h:2728
nullary_exprt::op2
const exprt & op2() const =delete
index_exprt
Array index operator.
Definition: std_expr.h:1243
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
can_cast_expr< unary_plus_exprt >
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:449
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
unary_predicate_exprt::unary_predicate_exprt
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition: std_expr.h:498
binary_predicate_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:658
complex_imag_exprt::complex_imag_exprt
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:1737
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3025
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
binary_exprt::op2
const exprt & op2() const =delete
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:761
unary_exprt::op3
const exprt & op3() const =delete
implies_exprt::implies_exprt
implies_exprt(exprt op0, exprt op1)
Definition: std_expr.h:1900
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
index_designatort::index
exprt & index()
Definition: std_expr.h:2265
can_cast_expr< struct_exprt >
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1595
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:816
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:2909
let_exprt::binding
binding_exprt & binding()
Definition: std_expr.h:2844
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:749
union_exprt::set_component_number
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1540
expr_protectedt::op2
exprt & op2()
Definition: expr.h:109
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:724
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:2681
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2676
let_exprt::symbol
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition: std_expr.h:2863
with_exprt::where
exprt & where()
Definition: std_expr.h:2193
array_of_exprt::array_of_exprt
array_of_exprt(exprt _what, array_typet _type)
Definition: std_expr.h:1319
to_member_designator
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:2337
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1382
can_cast_expr< with_exprt >
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:2215
member_exprt::set_component_name
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:2547
unary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:496
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:105
with_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:2208
let_exprt
A let expression.
Definition: std_expr.h:2816
to_and_expr
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:1882
div_exprt::divisor
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1007
complex_exprt::real
exprt real()
Definition: std_expr.h:1633
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
expr_protectedt
Base class for all expressions.
Definition: expr.h:347
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1606
can_cast_expr< member_designatort >
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:2321
to_abs_expr
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:371
mod_exprt
Modulo.
Definition: std_expr.h:1050
can_cast_expr< update_exprt >
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:2405
to_index_designator
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2288
nullary_exprt::move_to_operands
void move_to_operands(exprt &, exprt &)=delete
can_cast_expr< mult_exprt >
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:945
not_exprt
Boolean negation.
Definition: std_expr.h:2042
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
nondet_symbol_exprt::nondet_symbol_exprt
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:214
multi_ary_exprt::op3
const exprt & op3() const
Definition: std_expr.h:803