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