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  // When _array has array_type, the type of _index
1331  // must be array_type.index_type().
1332  // This will eventually be enforced using a precondition.
1333  index_exprt(const exprt &_array, exprt _index)
1334  : binary_exprt(
1335  _array,
1336  ID_index,
1337  std::move(_index),
1338  _array.type().has_subtype()
1339  ? to_type_with_subtype(_array.type()).subtype()
1340  : typet(ID_nil))
1341  {
1342  }
1343 
1344  index_exprt(exprt _array, exprt _index, typet _type)
1345  : binary_exprt(
1346  std::move(_array),
1347  ID_index,
1348  std::move(_index),
1349  std::move(_type))
1350  {
1351  }
1352 
1354  {
1355  return op0();
1356  }
1357 
1358  const exprt &array() const
1359  {
1360  return op0();
1361  }
1362 
1364  {
1365  return op1();
1366  }
1367 
1368  const exprt &index() const
1369  {
1370  return op1();
1371  }
1372 };
1373 
1374 template <>
1375 inline bool can_cast_expr<index_exprt>(const exprt &base)
1376 {
1377  return base.id() == ID_index;
1378 }
1379 
1380 inline void validate_expr(const index_exprt &value)
1381 {
1382  validate_operands(value, 2, "Array index must have two operands");
1383 }
1384 
1391 inline const index_exprt &to_index_expr(const exprt &expr)
1392 {
1393  PRECONDITION(expr.id()==ID_index);
1394  const index_exprt &ret = static_cast<const index_exprt &>(expr);
1395  validate_expr(ret);
1396  return ret;
1397 }
1398 
1401 {
1402  PRECONDITION(expr.id()==ID_index);
1403  index_exprt &ret = static_cast<index_exprt &>(expr);
1404  validate_expr(ret);
1405  return ret;
1406 }
1407 
1408 
1411 {
1412 public:
1413  explicit array_of_exprt(exprt _what, array_typet _type)
1414  : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1415  {
1416  }
1417 
1418  const array_typet &type() const
1419  {
1420  return static_cast<const array_typet &>(unary_exprt::type());
1421  }
1422 
1424  {
1425  return static_cast<array_typet &>(unary_exprt::type());
1426  }
1427 
1429  {
1430  return op0();
1431  }
1432 
1433  const exprt &what() const
1434  {
1435  return op0();
1436  }
1437 };
1438 
1439 template <>
1440 inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1441 {
1442  return base.id() == ID_array_of;
1443 }
1444 
1445 inline void validate_expr(const array_of_exprt &value)
1446 {
1447  validate_operands(value, 1, "'Array of' must have one operand");
1448 }
1449 
1456 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1457 {
1458  PRECONDITION(expr.id()==ID_array_of);
1459  const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1460  validate_expr(ret);
1461  return ret;
1462 }
1463 
1466 {
1467  PRECONDITION(expr.id()==ID_array_of);
1468  array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1469  validate_expr(ret);
1470  return ret;
1471 }
1472 
1473 
1476 {
1477 public:
1479  : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1480  {
1481  }
1482 
1483  const array_typet &type() const
1484  {
1485  return static_cast<const array_typet &>(multi_ary_exprt::type());
1486  }
1487 
1489  {
1490  return static_cast<array_typet &>(multi_ary_exprt::type());
1491  }
1492 };
1493 
1494 template <>
1495 inline bool can_cast_expr<array_exprt>(const exprt &base)
1496 {
1497  return base.id() == ID_array;
1498 }
1499 
1506 inline const array_exprt &to_array_expr(const exprt &expr)
1507 {
1508  PRECONDITION(expr.id()==ID_array);
1509  return static_cast<const array_exprt &>(expr);
1510 }
1511 
1514 {
1515  PRECONDITION(expr.id()==ID_array);
1516  return static_cast<array_exprt &>(expr);
1517 }
1518 
1522 {
1523 public:
1525  : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1526  {
1527  }
1528 
1529  const array_typet &type() const
1530  {
1531  return static_cast<const array_typet &>(multi_ary_exprt::type());
1532  }
1533 
1535  {
1536  return static_cast<array_typet &>(multi_ary_exprt::type());
1537  }
1538 
1540  void add(exprt index, exprt value)
1541  {
1542  add_to_operands(std::move(index), std::move(value));
1543  }
1544 };
1545 
1546 template <>
1547 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1548 {
1549  return base.id() == ID_array_list;
1550 }
1551 
1552 inline void validate_expr(const array_list_exprt &value)
1553 {
1554  PRECONDITION(value.operands().size() % 2 == 0);
1555 }
1556 
1557 inline const array_list_exprt &to_array_list_expr(const exprt &expr)
1558 {
1560  auto &ret = static_cast<const array_list_exprt &>(expr);
1561  validate_expr(ret);
1562  return ret;
1563 }
1564 
1566 {
1568  auto &ret = static_cast<array_list_exprt &>(expr);
1569  validate_expr(ret);
1570  return ret;
1571 }
1572 
1575 {
1576 public:
1578  : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1579  {
1580  }
1581 };
1582 
1583 template <>
1584 inline bool can_cast_expr<vector_exprt>(const exprt &base)
1585 {
1586  return base.id() == ID_vector;
1587 }
1588 
1595 inline const vector_exprt &to_vector_expr(const exprt &expr)
1596 {
1597  PRECONDITION(expr.id()==ID_vector);
1598  return static_cast<const vector_exprt &>(expr);
1599 }
1600 
1603 {
1604  PRECONDITION(expr.id()==ID_vector);
1605  return static_cast<vector_exprt &>(expr);
1606 }
1607 
1608 
1611 {
1612 public:
1613  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1614  : unary_exprt(ID_union, std::move(_value), std::move(_type))
1615  {
1616  set_component_name(_component_name);
1617  }
1618 
1620  {
1621  return get(ID_component_name);
1622  }
1623 
1624  void set_component_name(const irep_idt &component_name)
1625  {
1626  set(ID_component_name, component_name);
1627  }
1628 
1629  std::size_t get_component_number() const
1630  {
1631  return get_size_t(ID_component_number);
1632  }
1633 
1634  void set_component_number(std::size_t component_number)
1635  {
1636  set_size_t(ID_component_number, component_number);
1637  }
1638 };
1639 
1640 template <>
1641 inline bool can_cast_expr<union_exprt>(const exprt &base)
1642 {
1643  return base.id() == ID_union;
1644 }
1645 
1646 inline void validate_expr(const union_exprt &value)
1647 {
1648  validate_operands(value, 1, "Union constructor must have one operand");
1649 }
1650 
1657 inline const union_exprt &to_union_expr(const exprt &expr)
1658 {
1659  PRECONDITION(expr.id()==ID_union);
1660  const union_exprt &ret = static_cast<const union_exprt &>(expr);
1661  validate_expr(ret);
1662  return ret;
1663 }
1664 
1667 {
1668  PRECONDITION(expr.id()==ID_union);
1669  union_exprt &ret = static_cast<union_exprt &>(expr);
1670  validate_expr(ret);
1671  return ret;
1672 }
1673 
1677 {
1678 public:
1679  explicit empty_union_exprt(typet _type)
1680  : nullary_exprt(ID_empty_union, std::move(_type))
1681  {
1682  }
1683 };
1684 
1685 template <>
1686 inline bool can_cast_expr<empty_union_exprt>(const exprt &base)
1687 {
1688  return base.id() == ID_empty_union;
1689 }
1690 
1691 inline void validate_expr(const empty_union_exprt &value)
1692 {
1694  value, 0, "Empty-union constructor must not have any operand");
1695 }
1696 
1703 inline const empty_union_exprt &to_empty_union_expr(const exprt &expr)
1704 {
1705  PRECONDITION(expr.id() == ID_empty_union);
1706  const empty_union_exprt &ret = static_cast<const empty_union_exprt &>(expr);
1707  validate_expr(ret);
1708  return ret;
1709 }
1710 
1713 {
1714  PRECONDITION(expr.id() == ID_empty_union);
1715  empty_union_exprt &ret = static_cast<empty_union_exprt &>(expr);
1716  validate_expr(ret);
1717  return ret;
1718 }
1719 
1722 {
1723 public:
1724  struct_exprt(operandst _operands, typet _type)
1725  : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1726  {
1727  }
1728 
1729  exprt &component(const irep_idt &name, const namespacet &ns);
1730  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1731 };
1732 
1733 template <>
1734 inline bool can_cast_expr<struct_exprt>(const exprt &base)
1735 {
1736  return base.id() == ID_struct;
1737 }
1738 
1745 inline const struct_exprt &to_struct_expr(const exprt &expr)
1746 {
1747  PRECONDITION(expr.id()==ID_struct);
1748  return static_cast<const struct_exprt &>(expr);
1749 }
1750 
1753 {
1754  PRECONDITION(expr.id()==ID_struct);
1755  return static_cast<struct_exprt &>(expr);
1756 }
1757 
1758 
1761 {
1762 public:
1764  : binary_exprt(
1765  std::move(_real),
1766  ID_complex,
1767  std::move(_imag),
1768  std::move(_type))
1769  {
1770  }
1771 
1773  {
1774  return op0();
1775  }
1776 
1777  const exprt &real() const
1778  {
1779  return op0();
1780  }
1781 
1783  {
1784  return op1();
1785  }
1786 
1787  const exprt &imag() const
1788  {
1789  return op1();
1790  }
1791 };
1792 
1793 template <>
1794 inline bool can_cast_expr<complex_exprt>(const exprt &base)
1795 {
1796  return base.id() == ID_complex;
1797 }
1798 
1799 inline void validate_expr(const complex_exprt &value)
1800 {
1801  validate_operands(value, 2, "Complex constructor must have two operands");
1802 }
1803 
1810 inline const complex_exprt &to_complex_expr(const exprt &expr)
1811 {
1812  PRECONDITION(expr.id()==ID_complex);
1813  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1814  validate_expr(ret);
1815  return ret;
1816 }
1817 
1820 {
1821  PRECONDITION(expr.id()==ID_complex);
1822  complex_exprt &ret = static_cast<complex_exprt &>(expr);
1823  validate_expr(ret);
1824  return ret;
1825 }
1826 
1829 {
1830 public:
1831  explicit complex_real_exprt(const exprt &op)
1832  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1833  {
1834  }
1835 };
1836 
1837 template <>
1839 {
1840  return base.id() == ID_complex_real;
1841 }
1842 
1843 inline void validate_expr(const complex_real_exprt &expr)
1844 {
1846  expr, 1, "real part retrieval operation must have one operand");
1847 }
1848 
1856 {
1857  PRECONDITION(expr.id() == ID_complex_real);
1858  const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
1859  validate_expr(ret);
1860  return ret;
1861 }
1862 
1865 {
1866  PRECONDITION(expr.id() == ID_complex_real);
1867  complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
1868  validate_expr(ret);
1869  return ret;
1870 }
1871 
1874 {
1875 public:
1876  explicit complex_imag_exprt(const exprt &op)
1877  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
1878  {
1879  }
1880 };
1881 
1882 template <>
1884 {
1885  return base.id() == ID_complex_imag;
1886 }
1887 
1888 inline void validate_expr(const complex_imag_exprt &expr)
1889 {
1891  expr, 1, "imaginary part retrieval operation must have one operand");
1892 }
1893 
1901 {
1902  PRECONDITION(expr.id() == ID_complex_imag);
1903  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
1904  validate_expr(ret);
1905  return ret;
1906 }
1907 
1910 {
1911  PRECONDITION(expr.id() == ID_complex_imag);
1912  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
1913  validate_expr(ret);
1914  return ret;
1915 }
1916 
1917 
1920 {
1921 public:
1923  : unary_exprt(ID_typecast, std::move(op), std::move(_type))
1924  {
1925  }
1926 
1927  // returns a typecast if the type doesn't already match
1928  static exprt conditional_cast(const exprt &expr, const typet &type)
1929  {
1930  if(expr.type() == type)
1931  return expr;
1932  else
1933  return typecast_exprt(expr, type);
1934  }
1935 };
1936 
1937 template <>
1938 inline bool can_cast_expr<typecast_exprt>(const exprt &base)
1939 {
1940  return base.id() == ID_typecast;
1941 }
1942 
1943 inline void validate_expr(const typecast_exprt &value)
1944 {
1945  validate_operands(value, 1, "Typecast must have one operand");
1946 }
1947 
1954 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
1955 {
1956  PRECONDITION(expr.id()==ID_typecast);
1957  const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
1958  validate_expr(ret);
1959  return ret;
1960 }
1961 
1964 {
1965  PRECONDITION(expr.id()==ID_typecast);
1966  typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
1967  validate_expr(ret);
1968  return ret;
1969 }
1970 
1971 
1974 {
1975 public:
1977  : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
1978  {
1979  }
1980 
1982  : multi_ary_exprt(
1983  ID_and,
1984  {std::move(op0), std::move(op1), std::move(op2)},
1985  bool_typet())
1986  {
1987  }
1988 
1990  : multi_ary_exprt(
1991  ID_and,
1992  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
1993  bool_typet())
1994  {
1995  }
1996 
1997  explicit and_exprt(exprt::operandst _operands)
1998  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
1999  {
2000  }
2001 };
2002 
2006 
2008 
2009 template <>
2010 inline bool can_cast_expr<and_exprt>(const exprt &base)
2011 {
2012  return base.id() == ID_and;
2013 }
2014 
2021 inline const and_exprt &to_and_expr(const exprt &expr)
2022 {
2023  PRECONDITION(expr.id()==ID_and);
2024  return static_cast<const and_exprt &>(expr);
2025 }
2026 
2029 {
2030  PRECONDITION(expr.id()==ID_and);
2031  return static_cast<and_exprt &>(expr);
2032 }
2033 
2034 
2037 {
2038 public:
2040  : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2041  {
2042  }
2043 };
2044 
2045 template <>
2046 inline bool can_cast_expr<implies_exprt>(const exprt &base)
2047 {
2048  return base.id() == ID_implies;
2049 }
2050 
2051 inline void validate_expr(const implies_exprt &value)
2052 {
2053  validate_operands(value, 2, "Implies must have two operands");
2054 }
2055 
2062 inline const implies_exprt &to_implies_expr(const exprt &expr)
2063 {
2064  PRECONDITION(expr.id()==ID_implies);
2065  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2066  validate_expr(ret);
2067  return ret;
2068 }
2069 
2072 {
2073  PRECONDITION(expr.id()==ID_implies);
2074  implies_exprt &ret = static_cast<implies_exprt &>(expr);
2075  validate_expr(ret);
2076  return ret;
2077 }
2078 
2079 
2082 {
2083 public:
2085  : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2086  {
2087  }
2088 
2090  : multi_ary_exprt(
2091  ID_or,
2092  {std::move(op0), std::move(op1), std::move(op2)},
2093  bool_typet())
2094  {
2095  }
2096 
2098  : multi_ary_exprt(
2099  ID_or,
2100  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2101  bool_typet())
2102  {
2103  }
2104 
2105  explicit or_exprt(exprt::operandst _operands)
2106  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2107  {
2108  }
2109 };
2110 
2114 
2116 
2117 template <>
2118 inline bool can_cast_expr<or_exprt>(const exprt &base)
2119 {
2120  return base.id() == ID_or;
2121 }
2122 
2129 inline const or_exprt &to_or_expr(const exprt &expr)
2130 {
2131  PRECONDITION(expr.id()==ID_or);
2132  return static_cast<const or_exprt &>(expr);
2133 }
2134 
2136 inline or_exprt &to_or_expr(exprt &expr)
2137 {
2138  PRECONDITION(expr.id()==ID_or);
2139  return static_cast<or_exprt &>(expr);
2140 }
2141 
2142 
2145 {
2146 public:
2147  xor_exprt(exprt _op0, exprt _op1)
2148  : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2149  {
2150  }
2151 };
2152 
2153 template <>
2154 inline bool can_cast_expr<xor_exprt>(const exprt &base)
2155 {
2156  return base.id() == ID_xor;
2157 }
2158 
2165 inline const xor_exprt &to_xor_expr(const exprt &expr)
2166 {
2167  PRECONDITION(expr.id()==ID_xor);
2168  return static_cast<const xor_exprt &>(expr);
2169 }
2170 
2173 {
2174  PRECONDITION(expr.id()==ID_xor);
2175  return static_cast<xor_exprt &>(expr);
2176 }
2177 
2178 
2181 {
2182 public:
2183  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2184  {
2185  PRECONDITION(as_const(*this).op().type().id() == ID_bool);
2186  }
2187 };
2188 
2189 template <>
2190 inline bool can_cast_expr<not_exprt>(const exprt &base)
2191 {
2192  return base.id() == ID_not;
2193 }
2194 
2195 inline void validate_expr(const not_exprt &value)
2196 {
2197  validate_operands(value, 1, "Not must have one operand");
2198 }
2199 
2206 inline const not_exprt &to_not_expr(const exprt &expr)
2207 {
2208  PRECONDITION(expr.id()==ID_not);
2209  const not_exprt &ret = static_cast<const not_exprt &>(expr);
2210  validate_expr(ret);
2211  return ret;
2212 }
2213 
2216 {
2217  PRECONDITION(expr.id()==ID_not);
2218  not_exprt &ret = static_cast<not_exprt &>(expr);
2219  validate_expr(ret);
2220  return ret;
2221 }
2222 
2223 
2225 class if_exprt : public ternary_exprt
2226 {
2227 public:
2229  : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2230  {
2231  }
2232 
2234  : ternary_exprt(
2235  ID_if,
2236  std::move(cond),
2237  std::move(t),
2238  std::move(f),
2239  std::move(type))
2240  {
2241  }
2242 
2244  {
2245  return op0();
2246  }
2247 
2248  const exprt &cond() const
2249  {
2250  return op0();
2251  }
2252 
2254  {
2255  return op1();
2256  }
2257 
2258  const exprt &true_case() const
2259  {
2260  return op1();
2261  }
2262 
2264  {
2265  return op2();
2266  }
2267 
2268  const exprt &false_case() const
2269  {
2270  return op2();
2271  }
2272 };
2273 
2274 template <>
2275 inline bool can_cast_expr<if_exprt>(const exprt &base)
2276 {
2277  return base.id() == ID_if;
2278 }
2279 
2280 inline void validate_expr(const if_exprt &value)
2281 {
2282  validate_operands(value, 3, "If-then-else must have three operands");
2283 }
2284 
2291 inline const if_exprt &to_if_expr(const exprt &expr)
2292 {
2293  PRECONDITION(expr.id()==ID_if);
2294  const if_exprt &ret = static_cast<const if_exprt &>(expr);
2295  validate_expr(ret);
2296  return ret;
2297 }
2298 
2300 inline if_exprt &to_if_expr(exprt &expr)
2301 {
2302  PRECONDITION(expr.id()==ID_if);
2303  if_exprt &ret = static_cast<if_exprt &>(expr);
2304  validate_expr(ret);
2305  return ret;
2306 }
2307 
2312 {
2313 public:
2314  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
2315  : expr_protectedt(
2316  ID_with,
2317  _old.type(),
2318  {_old, std::move(_where), std::move(_new_value)})
2319  {
2320  }
2321 
2323  {
2324  return op0();
2325  }
2326 
2327  const exprt &old() const
2328  {
2329  return op0();
2330  }
2331 
2333  {
2334  return op1();
2335  }
2336 
2337  const exprt &where() const
2338  {
2339  return op1();
2340  }
2341 
2343  {
2344  return op2();
2345  }
2346 
2347  const exprt &new_value() const
2348  {
2349  return op2();
2350  }
2351 };
2352 
2353 template <>
2354 inline bool can_cast_expr<with_exprt>(const exprt &base)
2355 {
2356  return base.id() == ID_with;
2357 }
2358 
2359 inline void validate_expr(const with_exprt &value)
2360 {
2362  value, 3, "array/structure update must have at least 3 operands", true);
2364  value.operands().size() % 2 == 1,
2365  "array/structure update must have an odd number of operands");
2366 }
2367 
2374 inline const with_exprt &to_with_expr(const exprt &expr)
2375 {
2376  PRECONDITION(expr.id()==ID_with);
2377  const with_exprt &ret = static_cast<const with_exprt &>(expr);
2378  validate_expr(ret);
2379  return ret;
2380 }
2381 
2384 {
2385  PRECONDITION(expr.id()==ID_with);
2386  with_exprt &ret = static_cast<with_exprt &>(expr);
2387  validate_expr(ret);
2388  return ret;
2389 }
2390 
2392 {
2393 public:
2394  explicit index_designatort(exprt _index)
2395  : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
2396  {
2397  }
2398 
2399  const exprt &index() const
2400  {
2401  return op0();
2402  }
2403 
2405  {
2406  return op0();
2407  }
2408 };
2409 
2410 template <>
2411 inline bool can_cast_expr<index_designatort>(const exprt &base)
2412 {
2413  return base.id() == ID_index_designator;
2414 }
2415 
2416 inline void validate_expr(const index_designatort &value)
2417 {
2418  validate_operands(value, 1, "Index designator must have one operand");
2419 }
2420 
2427 inline const index_designatort &to_index_designator(const exprt &expr)
2428 {
2429  PRECONDITION(expr.id()==ID_index_designator);
2430  const index_designatort &ret = static_cast<const index_designatort &>(expr);
2431  validate_expr(ret);
2432  return ret;
2433 }
2434 
2437 {
2438  PRECONDITION(expr.id()==ID_index_designator);
2439  index_designatort &ret = static_cast<index_designatort &>(expr);
2440  validate_expr(ret);
2441  return ret;
2442 }
2443 
2445 {
2446 public:
2447  explicit member_designatort(const irep_idt &_component_name)
2448  : expr_protectedt(ID_member_designator, typet())
2449  {
2450  set(ID_component_name, _component_name);
2451  }
2452 
2454  {
2455  return get(ID_component_name);
2456  }
2457 };
2458 
2459 template <>
2461 {
2462  return base.id() == ID_member_designator;
2463 }
2464 
2465 inline void validate_expr(const member_designatort &value)
2466 {
2467  validate_operands(value, 0, "Member designator must not have operands");
2468 }
2469 
2477 {
2478  PRECONDITION(expr.id()==ID_member_designator);
2479  const member_designatort &ret = static_cast<const member_designatort &>(expr);
2480  validate_expr(ret);
2481  return ret;
2482 }
2483 
2486 {
2487  PRECONDITION(expr.id()==ID_member_designator);
2488  member_designatort &ret = static_cast<member_designatort &>(expr);
2489  validate_expr(ret);
2490  return ret;
2491 }
2492 
2493 
2496 {
2497 public:
2498  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
2499  : ternary_exprt(
2500  ID_update,
2501  _old,
2502  std::move(_designator),
2503  std::move(_new_value),
2504  _old.type())
2505  {
2506  }
2507 
2509  {
2510  return op0();
2511  }
2512 
2513  const exprt &old() const
2514  {
2515  return op0();
2516  }
2517 
2518  // the designator operands are either
2519  // 1) member_designator or
2520  // 2) index_designator
2521  // as defined above
2523  {
2524  return op1().operands();
2525  }
2526 
2528  {
2529  return op1().operands();
2530  }
2531 
2533  {
2534  return op2();
2535  }
2536 
2537  const exprt &new_value() const
2538  {
2539  return op2();
2540  }
2541 };
2542 
2543 template <>
2544 inline bool can_cast_expr<update_exprt>(const exprt &base)
2545 {
2546  return base.id() == ID_update;
2547 }
2548 
2549 inline void validate_expr(const update_exprt &value)
2550 {
2552  value, 3, "Array/structure update must have three operands");
2553 }
2554 
2561 inline const update_exprt &to_update_expr(const exprt &expr)
2562 {
2563  PRECONDITION(expr.id()==ID_update);
2564  const update_exprt &ret = static_cast<const update_exprt &>(expr);
2565  validate_expr(ret);
2566  return ret;
2567 }
2568 
2571 {
2572  PRECONDITION(expr.id()==ID_update);
2573  update_exprt &ret = static_cast<update_exprt &>(expr);
2574  validate_expr(ret);
2575  return ret;
2576 }
2577 
2578 
2579 #if 0
2581 class array_update_exprt:public expr_protectedt
2582 {
2583 public:
2584  array_update_exprt(
2585  const exprt &_array,
2586  const exprt &_index,
2587  const exprt &_new_value):
2588  exprt(ID_array_update, _array.type())
2589  {
2590  add_to_operands(_array, _index, _new_value);
2591  }
2592 
2593  array_update_exprt():expr_protectedt(ID_array_update)
2594  {
2595  operands().resize(3);
2596  }
2597 
2598  exprt &array()
2599  {
2600  return op0();
2601  }
2602 
2603  const exprt &array() const
2604  {
2605  return op0();
2606  }
2607 
2608  exprt &index()
2609  {
2610  return op1();
2611  }
2612 
2613  const exprt &index() const
2614  {
2615  return op1();
2616  }
2617 
2618  exprt &new_value()
2619  {
2620  return op2();
2621  }
2622 
2623  const exprt &new_value() const
2624  {
2625  return op2();
2626  }
2627 };
2628 
2629 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2630 {
2631  return base.id()==ID_array_update;
2632 }
2633 
2634 inline void validate_expr(const array_update_exprt &value)
2635 {
2636  validate_operands(value, 3, "Array update must have three operands");
2637 }
2638 
2645 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2646 {
2647  PRECONDITION(expr.id()==ID_array_update);
2648  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2649  validate_expr(ret);
2650  return ret;
2651 }
2652 
2654 inline array_update_exprt &to_array_update_expr(exprt &expr)
2655 {
2656  PRECONDITION(expr.id()==ID_array_update);
2657  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2658  validate_expr(ret);
2659  return ret;
2660 }
2661 
2662 #endif
2663 
2664 
2667 {
2668 public:
2669  member_exprt(exprt op, const irep_idt &component_name, typet _type)
2670  : unary_exprt(ID_member, std::move(op), std::move(_type))
2671  {
2672  set_component_name(component_name);
2673  }
2674 
2676  : unary_exprt(ID_member, std::move(op), c.type())
2677  {
2679  }
2680 
2682  {
2683  return get(ID_component_name);
2684  }
2685 
2686  void set_component_name(const irep_idt &component_name)
2687  {
2688  set(ID_component_name, component_name);
2689  }
2690 
2691  std::size_t get_component_number() const
2692  {
2693  return get_size_t(ID_component_number);
2694  }
2695 
2696  // will go away, use compound()
2697  const exprt &struct_op() const
2698  {
2699  return op0();
2700  }
2701 
2702  // will go away, use compound()
2704  {
2705  return op0();
2706  }
2707 
2708  const exprt &compound() const
2709  {
2710  return op0();
2711  }
2712 
2714  {
2715  return op0();
2716  }
2717 
2718  static void check(
2719  const exprt &expr,
2721  {
2722  DATA_CHECK(
2723  vm,
2724  expr.operands().size() == 1,
2725  "member expression must have one operand");
2726  }
2727 
2728  static void validate(
2729  const exprt &expr,
2730  const namespacet &ns,
2732 };
2733 
2734 template <>
2735 inline bool can_cast_expr<member_exprt>(const exprt &base)
2736 {
2737  return base.id() == ID_member;
2738 }
2739 
2740 inline void validate_expr(const member_exprt &value)
2741 {
2742  validate_operands(value, 1, "Extract member must have one operand");
2743 }
2744 
2751 inline const member_exprt &to_member_expr(const exprt &expr)
2752 {
2753  PRECONDITION(expr.id()==ID_member);
2754  const member_exprt &ret = static_cast<const member_exprt &>(expr);
2755  validate_expr(ret);
2756  return ret;
2757 }
2758 
2761 {
2762  PRECONDITION(expr.id()==ID_member);
2763  member_exprt &ret = static_cast<member_exprt &>(expr);
2764  validate_expr(ret);
2765  return ret;
2766 }
2767 
2768 
2771 {
2772 public:
2773  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
2774  {
2775  }
2776 };
2777 
2778 template <>
2779 inline bool can_cast_expr<type_exprt>(const exprt &base)
2780 {
2781  return base.id() == ID_type;
2782 }
2783 
2790 inline const type_exprt &to_type_expr(const exprt &expr)
2791 {
2793  const type_exprt &ret = static_cast<const type_exprt &>(expr);
2794  return ret;
2795 }
2796 
2799 {
2801  type_exprt &ret = static_cast<type_exprt &>(expr);
2802  return ret;
2803 }
2804 
2807 {
2808 public:
2809  constant_exprt(const irep_idt &_value, typet _type)
2810  : expr_protectedt(ID_constant, std::move(_type))
2811  {
2812  set_value(_value);
2813  }
2814 
2815  const irep_idt &get_value() const
2816  {
2817  return get(ID_value);
2818  }
2819 
2820  void set_value(const irep_idt &value)
2821  {
2822  set(ID_value, value);
2823  }
2824 
2825  bool value_is_zero_string() const;
2826 };
2827 
2828 template <>
2829 inline bool can_cast_expr<constant_exprt>(const exprt &base)
2830 {
2831  return base.id() == ID_constant;
2832 }
2833 
2840 inline const constant_exprt &to_constant_expr(const exprt &expr)
2841 {
2842  PRECONDITION(expr.id()==ID_constant);
2843  return static_cast<const constant_exprt &>(expr);
2844 }
2845 
2848 {
2849  PRECONDITION(expr.id()==ID_constant);
2850  return static_cast<constant_exprt &>(expr);
2851 }
2852 
2853 
2856 {
2857 public:
2859  {
2860  }
2861 };
2862 
2865 {
2866 public:
2868  {
2869  }
2870 };
2871 
2873 class nil_exprt : public nullary_exprt
2874 {
2875 public:
2877  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
2878  {
2879  }
2880 };
2881 
2882 template <>
2883 inline bool can_cast_expr<nil_exprt>(const exprt &base)
2884 {
2885  return base.id() == ID_nil;
2886 }
2887 
2890 {
2891 public:
2892  explicit infinity_exprt(typet _type)
2893  : nullary_exprt(ID_infinity, std::move(_type))
2894  {
2895  }
2896 };
2897 
2900 {
2901 public:
2902  using variablest = std::vector<symbol_exprt>;
2903 
2906  irep_idt _id,
2907  const variablest &_variables,
2908  exprt _where,
2909  typet _type)
2910  : binary_exprt(
2912  ID_tuple,
2913  (const operandst &)_variables,
2914  typet(ID_tuple)),
2915  _id,
2916  std::move(_where),
2917  std::move(_type))
2918  {
2919  }
2920 
2922  {
2923  return (variablest &)to_multi_ary_expr(op0()).operands();
2924  }
2925 
2926  const variablest &variables() const
2927  {
2928  return (variablest &)to_multi_ary_expr(op0()).operands();
2929  }
2930 
2932  {
2933  return op1();
2934  }
2935 
2936  const exprt &where() const
2937  {
2938  return op1();
2939  }
2940 
2943  exprt instantiate(const exprt::operandst &) const;
2944 
2947  exprt instantiate(const variablest &) const;
2948 };
2949 
2950 inline void validate_expr(const binding_exprt &binding_expr)
2951 {
2953  binding_expr, 2, "Binding expressions must have two operands");
2954 }
2955 
2962 inline const binding_exprt &to_binding_expr(const exprt &expr)
2963 {
2964  PRECONDITION(
2965  expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda);
2966  const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
2967  validate_expr(ret);
2968  return ret;
2969 }
2970 
2972 class let_exprt : public binary_exprt
2973 {
2974 public:
2977  operandst values,
2978  const exprt &where)
2979  : binary_exprt(
2980  binding_exprt(
2981  ID_let_binding,
2982  std::move(variables),
2983  where,
2984  where.type()),
2985  ID_let,
2986  multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
2987  where.type())
2988  {
2989  PRECONDITION(this->variables().size() == this->values().size());
2990  }
2991 
2994  : let_exprt(
2995  binding_exprt::variablest{std::move(symbol)},
2996  operandst{std::move(value)},
2997  where)
2998  {
2999  }
3000 
3002  {
3003  return static_cast<binding_exprt &>(op0());
3004  }
3005 
3006  const binding_exprt &binding() const
3007  {
3008  return static_cast<const binding_exprt &>(op0());
3009  }
3010 
3013  {
3014  auto &variables = binding().variables();
3015  PRECONDITION(variables.size() == 1);
3016  return variables.front();
3017  }
3018 
3020  const symbol_exprt &symbol() const
3021  {
3022  const auto &variables = binding().variables();
3023  PRECONDITION(variables.size() == 1);
3024  return variables.front();
3025  }
3026 
3029  {
3030  auto &values = this->values();
3031  PRECONDITION(values.size() == 1);
3032  return values.front();
3033  }
3034 
3036  const exprt &value() const
3037  {
3038  const auto &values = this->values();
3039  PRECONDITION(values.size() == 1);
3040  return values.front();
3041  }
3042 
3044  {
3045  return static_cast<multi_ary_exprt &>(op1()).operands();
3046  }
3047 
3048  const operandst &values() const
3049  {
3050  return static_cast<const multi_ary_exprt &>(op1()).operands();
3051  }
3052 
3055  {
3056  return binding().variables();
3057  }
3058 
3061  {
3062  return binding().variables();
3063  }
3064 
3067  {
3068  return binding().where();
3069  }
3070 
3072  const exprt &where() const
3073  {
3074  return binding().where();
3075  }
3076 
3077  static void validate(const exprt &, validation_modet);
3078 };
3079 
3080 template <>
3081 inline bool can_cast_expr<let_exprt>(const exprt &base)
3082 {
3083  return base.id() == ID_let;
3084 }
3085 
3086 inline void validate_expr(const let_exprt &let_expr)
3087 {
3088  validate_operands(let_expr, 2, "Let must have two operands");
3089 }
3090 
3097 inline const let_exprt &to_let_expr(const exprt &expr)
3098 {
3099  PRECONDITION(expr.id()==ID_let);
3100  const let_exprt &ret = static_cast<const let_exprt &>(expr);
3101  validate_expr(ret);
3102  return ret;
3103 }
3104 
3107 {
3108  PRECONDITION(expr.id()==ID_let);
3109  let_exprt &ret = static_cast<let_exprt &>(expr);
3110  validate_expr(ret);
3111  return ret;
3112 }
3113 
3114 
3119 {
3120 public:
3121  cond_exprt(operandst _operands, typet _type)
3122  : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3123  {
3124  }
3125 
3129  void add_case(const exprt &condition, const exprt &value)
3130  {
3131  PRECONDITION(condition.type().id() == ID_bool);
3132  operands().reserve(operands().size() + 2);
3133  operands().push_back(condition);
3134  operands().push_back(value);
3135  }
3136 };
3137 
3138 template <>
3139 inline bool can_cast_expr<cond_exprt>(const exprt &base)
3140 {
3141  return base.id() == ID_cond;
3142 }
3143 
3144 inline void validate_expr(const cond_exprt &value)
3145 {
3147  value.operands().size() % 2 == 0, "cond must have even number of operands");
3148 }
3149 
3156 inline const cond_exprt &to_cond_expr(const exprt &expr)
3157 {
3158  PRECONDITION(expr.id() == ID_cond);
3159  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3160  validate_expr(ret);
3161  return ret;
3162 }
3163 
3166 {
3167  PRECONDITION(expr.id() == ID_cond);
3168  cond_exprt &ret = static_cast<cond_exprt &>(expr);
3169  validate_expr(ret);
3170  return ret;
3171 }
3172 
3182 {
3183 public:
3185  symbol_exprt arg,
3186  exprt body,
3187  array_typet _type)
3188  : binding_exprt(
3189  ID_array_comprehension,
3190  {std::move(arg)},
3191  std::move(body),
3192  std::move(_type))
3193  {
3194  }
3195 
3196  const array_typet &type() const
3197  {
3198  return static_cast<const array_typet &>(binary_exprt::type());
3199  }
3200 
3202  {
3203  return static_cast<array_typet &>(binary_exprt::type());
3204  }
3205 
3206  const symbol_exprt &arg() const
3207  {
3208  auto &variables = this->variables();
3209  PRECONDITION(variables.size() == 1);
3210  return variables[0];
3211  }
3212 
3214  {
3215  auto &variables = this->variables();
3216  PRECONDITION(variables.size() == 1);
3217  return variables[0];
3218  }
3219 
3220  const exprt &body() const
3221  {
3222  return where();
3223  }
3224 
3226  {
3227  return where();
3228  }
3229 };
3230 
3231 template <>
3233 {
3234  return base.id() == ID_array_comprehension;
3235 }
3236 
3237 inline void validate_expr(const array_comprehension_exprt &value)
3238 {
3239  validate_operands(value, 2, "'Array comprehension' must have two operands");
3240 }
3241 
3248 inline const array_comprehension_exprt &
3250 {
3251  PRECONDITION(expr.id() == ID_array_comprehension);
3252  const array_comprehension_exprt &ret =
3253  static_cast<const array_comprehension_exprt &>(expr);
3254  validate_expr(ret);
3255  return ret;
3256 }
3257 
3260 {
3261  PRECONDITION(expr.id() == ID_array_comprehension);
3263  static_cast<array_comprehension_exprt &>(expr);
3264  validate_expr(ret);
3265  return ret;
3266 }
3267 
3268 inline void validate_expr(const class class_method_descriptor_exprt &value);
3269 
3272 {
3273 public:
3289  typet _type,
3293  : nullary_exprt(ID_virtual_function, std::move(_type))
3294  {
3296  set(ID_component_name, std::move(mangled_method_name));
3297  set(ID_C_class, std::move(class_id));
3298  set(ID_C_base_name, std::move(base_method_name));
3299  set(ID_identifier, std::move(id));
3300  validate_expr(*this);
3301  }
3302 
3310  {
3311  return get(ID_component_name);
3312  }
3313 
3317  const irep_idt &class_id() const
3318  {
3319  return get(ID_C_class);
3320  }
3321 
3325  {
3326  return get(ID_C_base_name);
3327  }
3328 
3332  const irep_idt &get_identifier() const
3333  {
3334  return get(ID_identifier);
3335  }
3336 };
3337 
3338 inline void validate_expr(const class class_method_descriptor_exprt &value)
3339 {
3340  validate_operands(value, 0, "class method descriptor must not have operands");
3342  !value.mangled_method_name().empty(),
3343  "class method descriptor must have a mangled method name.");
3345  !value.class_id().empty(), "class method descriptor must have a class id.");
3347  !value.base_method_name().empty(),
3348  "class method descriptor must have a base method name.");
3350  value.get_identifier() == id2string(value.class_id()) + "." +
3351  id2string(value.mangled_method_name()),
3352  "class method descriptor must have an identifier in the expected format.");
3353 }
3354 
3361 inline const class_method_descriptor_exprt &
3363 {
3364  PRECONDITION(expr.id() == ID_virtual_function);
3365  const class_method_descriptor_exprt &ret =
3366  static_cast<const class_method_descriptor_exprt &>(expr);
3367  validate_expr(ret);
3368  return ret;
3369 }
3370 
3371 template <>
3373 {
3374  return base.id() == ID_virtual_function;
3375 }
3376 
3377 #endif // CPROVER_UTIL_STD_EXPR_H
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
Absolute value.
Definition: std_expr.h:346
abs_exprt(exprt _op)
Definition: std_expr.h:348
Boolean AND.
Definition: std_expr.h:1974
and_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:1981
and_exprt(exprt op0, exprt op1)
Definition: std_expr.h:1976
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:1989
and_exprt(exprt::operandst _operands)
Definition: std_expr.h:1997
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3182
symbol_exprt & arg()
Definition: std_expr.h:3213
array_typet & type()
Definition: std_expr.h:3201
const exprt & body() const
Definition: std_expr.h:3220
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition: std_expr.h:3184
const array_typet & type() const
Definition: std_expr.h:3196
const symbol_exprt & arg() const
Definition: std_expr.h:3206
Array constructor from list of elements.
Definition: std_expr.h:1476
array_typet & type()
Definition: std_expr.h:1488
array_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1478
const array_typet & type() const
Definition: std_expr.h:1483
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1522
void add(exprt index, exprt value)
add an index/value pair
Definition: std_expr.h:1540
const array_typet & type() const
Definition: std_expr.h:1529
array_list_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1524
array_typet & type()
Definition: std_expr.h:1534
Array constructor from single element.
Definition: std_expr.h:1411
const exprt & what() const
Definition: std_expr.h:1433
exprt & what()
Definition: std_expr.h:1428
array_of_exprt(exprt _what, array_typet _type)
Definition: std_expr.h:1413
array_typet & type()
Definition: std_expr.h:1423
const array_typet & type() const
Definition: std_expr.h:1418
Arrays with given size.
Definition: std_types.h:763
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op2()=delete
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:552
exprt & op1()
Definition: expr.h:102
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:572
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:562
const exprt & lhs() const
Definition: std_expr.h:585
exprt & lhs()
Definition: std_expr.h:580
const exprt & rhs() const
Definition: std_expr.h:595
const exprt & op2() const =delete
exprt & op0()
Definition: expr.h:99
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:557
exprt & op3()=delete
exprt & rhs()
Definition: std_expr.h:590
const exprt & op3() const =delete
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:650
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition: std_expr.h:645
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:657
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:676
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:681
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:688
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:2900
exprt & where()
Definition: std_expr.h:2931
const exprt & where() const
Definition: std_expr.h:2936
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition: std_expr.h:2905
const variablest & variables() const
Definition: std_expr.h:2926
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition: std_expr.cpp:234
variablest & variables()
Definition: std_expr.h:2921
std::vector< symbol_exprt > variablest
Definition: std_expr.h:2902
The Boolean type.
Definition: std_types.h:36
An expression describing a method on a class.
Definition: std_expr.h:3272
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:3332
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:3317
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition: std_expr.h:3288
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:3324
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition: std_expr.h:3309
Complex constructor from a pair of numbers.
Definition: std_expr.h:1761
const exprt & imag() const
Definition: std_expr.h:1787
const exprt & real() const
Definition: std_expr.h:1777
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition: std_expr.h:1763
exprt real()
Definition: std_expr.h:1772
exprt imag()
Definition: std_expr.h:1782
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1874
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:1876
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
complex_real_exprt(const exprt &op)
Definition: std_expr.h:1831
Complex numbers made of pair of given subtype.
Definition: std_types.h:1057
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:3119
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:3129
cond_exprt(operandst _operands, typet _type)
Definition: std_expr.h:3121
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
bool value_is_zero_string() const
Definition: std_expr.cpp:16
constant_exprt(const irep_idt &_value, typet _type)
Definition: std_expr.h:2809
void set_value(const irep_idt &value)
Definition: std_expr.h:2820
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition: std_expr.h:132
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:136
void set_static_lifetime()
Definition: std_expr.h:146
bool is_static_lifetime() const
Definition: std_expr.h:141
bool is_thread_local() const
Definition: std_expr.h:156
void clear_static_lifetime()
Definition: std_expr.h:151
Division.
Definition: std_expr.h:1064
div_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1066
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1090
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1072
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1084
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1078
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Union constructor to support unions without any member (a GCC/Clang feature).
Definition: std_expr.h:1677
empty_union_exprt(typet _type)
Definition: std_expr.h:1679
Equality.
Definition: std_expr.h:1225
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1232
equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1227
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1239
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition: std_expr.h:1179
euclidean_mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1181
Base class for all expressions.
Definition: expr.h:343
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
exprt & op1()
Definition: expr.h:102
source_locationt & add_source_location()
Definition: expr.h:235
exprt & op2()
Definition: expr.h:105
typet & type()
Return the type of the expression.
Definition: expr.h:82
exprt & op0()
Definition: expr.h:99
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
The Boolean constant false.
Definition: std_expr.h:2865
Binary greater than operator expression.
Definition: std_expr.h:719
greater_than_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:721
Binary greater than or equal operator expression.
Definition: std_expr.h:740
greater_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:742
The trinary if-then-else operator.
Definition: std_expr.h:2226
const exprt & false_case() const
Definition: std_expr.h:2268
if_exprt(exprt cond, const exprt &t, exprt f)
Definition: std_expr.h:2228
const exprt & true_case() const
Definition: std_expr.h:2258
const exprt & cond() const
Definition: std_expr.h:2248
exprt & true_case()
Definition: std_expr.h:2253
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition: std_expr.h:2233
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Boolean implication.
Definition: std_expr.h:2037
implies_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2039
exprt & index()
Definition: std_expr.h:2404
index_designatort(exprt _index)
Definition: std_expr.h:2394
const exprt & index() const
Definition: std_expr.h:2399
Array index operator.
Definition: std_expr.h:1328
index_exprt(exprt _array, exprt _index, typet _type)
Definition: std_expr.h:1344
const exprt & index() const
Definition: std_expr.h:1368
index_exprt(const exprt &_array, exprt _index)
Definition: std_expr.h:1333
exprt & array()
Definition: std_expr.h:1353
const exprt & array() const
Definition: std_expr.h:1358
exprt & index()
Definition: std_expr.h:1363
An expression denoting infinity.
Definition: std_expr.h:2890
infinity_exprt(typet _type)
Definition: std_expr.h:2892
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
std::size_t get_size_t(const irep_idt &name) const
Definition: irep.cpp:68
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void remove(const irep_idt &name)
Definition: irep.cpp:96
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:87
const irep_idt & id() const
Definition: irep.h:396
Binary less than operator expression.
Definition: std_expr.h:761
less_than_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:763
Binary less than or equal operator expression.
Definition: std_expr.h:782
less_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:784
A let expression.
Definition: std_expr.h:2973
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition: std_expr.h:3060
const binding_exprt & binding() const
Definition: std_expr.h:3006
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3066
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition: std_expr.h:3020
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition: std_expr.h:2993
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:3054
const operandst & values() const
Definition: std_expr.h:3048
static void validate(const exprt &, validation_modet)
Definition: std_expr.cpp:114
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition: std_expr.h:2975
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:3012
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:3028
binding_exprt & binding()
Definition: std_expr.h:3001
operandst & values()
Definition: std_expr.h:3043
const exprt & value() const
convenience accessor for the value of a single binding
Definition: std_expr.h:3036
const exprt & where() const
convenience accessor for binding().where()
Definition: std_expr.h:3072
irep_idt get_component_name() const
Definition: std_expr.h:2453
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:2447
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & compound() const
Definition: std_expr.h:2708
const exprt & struct_op() const
Definition: std_expr.h:2697
exprt & struct_op()
Definition: std_expr.h:2703
irep_idt get_component_name() const
Definition: std_expr.h:2681
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:2686
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
Definition: std_expr.cpp:81
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2718
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition: std_expr.h:2669
std::size_t get_component_number() const
Definition: std_expr.h:2691
member_exprt(exprt op, const struct_typet::componentt &c)
Definition: std_expr.h:2675
exprt & compound()
Definition: std_expr.h:2713
Binary minus.
Definition: std_expr.h:973
minus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:975
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1137
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
mult_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1021
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
const exprt & op0() const
Definition: std_expr.h:868
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:837
exprt & op2()
Definition: std_expr.h:856
exprt & op3()
Definition: std_expr.h:862
const exprt & op3() const
Definition: std_expr.h:886
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:832
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition: std_expr.h:826
const exprt & op1() const
Definition: std_expr.h:874
exprt & op1()
Definition: std_expr.h:850
exprt & op0()
Definition: std_expr.h:844
const exprt & op2() const
Definition: std_expr.h:880
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
Expression to hold a nondeterministic choice.
Definition: std_expr.h:209
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:232
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:213
const irep_idt & get_identifier() const
Definition: std_expr.h:237
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition: std_expr.h:222
Boolean negation.
Definition: std_expr.h:2181
not_exprt(exprt _op)
Definition: std_expr.h:2183
Disequality.
Definition: std_expr.h:1283
notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1285
An expression without operands.
Definition: std_expr.h:22
void move_to_operands(exprt &, exprt &)=delete
const operandst & operands() const =delete
operandst & operands()=delete
remove all operand methods
exprt & op3()=delete
exprt & op1()=delete
nullary_exprt(const irep_idt &_id, typet _type)
Definition: std_expr.h:24
exprt & op0()=delete
const exprt & op0() const =delete
void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete
void move_to_operands(exprt &)=delete
void copy_to_operands(const exprt &expr)=delete
void copy_to_operands(const exprt &, const exprt &)=delete
void move_to_operands(exprt &, exprt &, exprt &)=delete
const exprt & op3() const =delete
const exprt & op1() const =delete
const exprt & op2() const =delete
exprt & op2()=delete
Boolean OR.
Definition: std_expr.h:2082
or_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2089
or_exprt(exprt::operandst _operands)
Definition: std_expr.h:2105
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2097
or_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2084
The plus expression Associativity is not specified.
Definition: std_expr.h:914
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition: std_expr.h:921
plus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:916
plus_exprt(operandst _operands, typet _type)
Definition: std_expr.h:930
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:484
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:486
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
sign_exprt(exprt _op)
Definition: std_expr.h:508
Struct constructor from list of elements.
Definition: std_expr.h:1722
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:62
struct_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1724
const irep_idt & get_name() const
Definition: std_types.h:79
Expression to hold a symbol (variable)
Definition: std_expr.h:80
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:104
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:99
symbol_exprt(typet type)
Definition: std_expr.h:83
symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:89
const irep_idt & get_identifier() const
Definition: std_expr.h:109
An expression with three operands.
Definition: std_expr.h:53
exprt & op3()=delete
exprt & op1()
Definition: expr.h:102
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition: std_expr.h:56
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
const exprt & op3() const =delete
The Boolean constant true.
Definition: std_expr.h:2856
An expression denoting a type.
Definition: std_expr.h:2771
type_exprt(typet type)
Definition: std_expr.h:2773
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
typecast_exprt(exprt op, typet _type)
Definition: std_expr.h:1922
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:281
exprt & op()
Definition: std_expr.h:298
const exprt & op1() const =delete
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:283
exprt & op2()=delete
const exprt & op() const
Definition: std_expr.h:293
exprt & op1()=delete
const exprt & op3() const =delete
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition: std_expr.h:288
const exprt & op2() const =delete
exprt & op3()=delete
The unary minus expression.
Definition: std_expr.h:390
unary_minus_exprt(exprt _op)
Definition: std_expr.h:397
unary_minus_exprt(exprt _op, typet _type)
Definition: std_expr.h:392
The unary plus expression.
Definition: std_expr.h:439
unary_plus_exprt(exprt op)
Definition: std_expr.h:441
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:495
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition: std_expr.h:497
Union constructor from single element.
Definition: std_expr.h:1611
std::size_t get_component_number() const
Definition: std_expr.h:1629
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1634
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1624
irep_idt get_component_name() const
Definition: std_expr.h:1619
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition: std_expr.h:1613
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
exprt::operandst & designator()
Definition: std_expr.h:2522
exprt & old()
Definition: std_expr.h:2508
const exprt & new_value() const
Definition: std_expr.h:2537
exprt & new_value()
Definition: std_expr.h:2532
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition: std_expr.h:2498
const exprt & old() const
Definition: std_expr.h:2513
const exprt::operandst & designator() const
Definition: std_expr.h:2527
Vector constructor from list of elements.
Definition: std_expr.h:1575
vector_exprt(operandst _operands, vector_typet _type)
Definition: std_expr.h:1577
The vector type.
Definition: std_types.h:996
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
const exprt & new_value() const
Definition: std_expr.h:2347
exprt & old()
Definition: std_expr.h:2322
const exprt & old() const
Definition: std_expr.h:2327
exprt & new_value()
Definition: std_expr.h:2342
exprt & where()
Definition: std_expr.h:2332
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition: std_expr.h:2314
const exprt & where() const
Definition: std_expr.h:2337
Boolean XOR.
Definition: std_expr.h:2145
xor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2147
Templated functions to cast to specific exprt-derived classes.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Definition: expr_util.cpp:152
const irept & get_nil_irep()
Definition: irep.cpp:20
dstring_hash irep_id_hash
Definition: irep.h:39
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1249
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2165
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2427
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1292
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:1794
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:2190
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1308
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:1938
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:2476
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1734
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2561
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2154
const empty_union_exprt & to_empty_union_expr(const exprt &expr)
Cast an exprt to an empty_union_exprt.
Definition: std_expr.h:1703
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1028
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3097
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:2275
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2129
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:464
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1160
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:2460
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition: std_expr.h:3232
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1506
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:1883
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3249
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:354
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:515
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2021
bool can_cast_expr< type_exprt >(const exprt &base)
Definition: std_expr.h:2779
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:3372
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1855
void validate_expr(const symbol_exprt &value)
Definition: std_expr.h:178
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:404
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1657
bool can_cast_expr< less_than_exprt >(const exprt &base)
Definition: std_expr.h:770
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1557
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:2354
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:34
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:982
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:3081
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:937
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1440
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1595
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:244
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2829
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1745
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1375
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:173
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition: std_expr.h:2790
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:2735
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1456
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition: std_expr.h:1204
bool can_cast_expr< empty_union_exprt >(const exprt &base)
Definition: std_expr.h:1686
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:2118
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1144
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition: std_expr.h:3139
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:2544
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:707
bool can_cast_expr< euclidean_mod_exprt >(const exprt &base)
Definition: std_expr.h:1188
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1584
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1810
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1547
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:2411
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:448
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2010
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:260
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition: std_expr.h:728
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2062
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1495
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1900
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:611
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1097
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition: std_expr.h:2883
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:3362
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition: std_expr.h:2962
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:531
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:749
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2046
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:312
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:370
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:791
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1641
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:1838
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:3156
Pre-defined types.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
size_t operator()(const ::symbol_exprt &sym)
Definition: std_expr.h:122
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet