CBMC
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 copy_to_operands(const exprt &expr) = delete;
43  void copy_to_operands(const exprt &, const exprt &) = delete;
44  void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
45 };
46 
49 {
50 public:
51  // constructor
53  const irep_idt &_id,
54  exprt _op0,
55  exprt _op1,
56  exprt _op2,
57  typet _type)
59  _id,
60  std::move(_type),
61  {std::move(_op0), std::move(_op1), std::move(_op2)})
62  {
63  }
64 
65  // make op0 to op2 public
66  using exprt::op0;
67  using exprt::op1;
68  using exprt::op2;
69 
70  const exprt &op3() const = delete;
71  exprt &op3() = delete;
72 
73  static void check(
74  const exprt &expr,
76  {
77  DATA_CHECK(
78  vm,
79  expr.operands().size() == 3,
80  "ternary expression must have three operands");
81  }
82 
83  static void validate(
84  const exprt &expr,
85  const namespacet &,
87  {
88  check(expr, vm);
89  }
90 };
91 
98 inline const ternary_exprt &to_ternary_expr(const exprt &expr)
99 {
100  ternary_exprt::check(expr);
101  return static_cast<const ternary_exprt &>(expr);
102 }
103 
106 {
107  ternary_exprt::check(expr);
108  return static_cast<ternary_exprt &>(expr);
109 }
110 
113 {
114 public:
116  explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type))
117  {
118  }
119 
122  symbol_exprt(const irep_idt &identifier, typet type)
123  : nullary_exprt(ID_symbol, std::move(type))
124  {
125  set_identifier(identifier);
126  }
127 
132  static symbol_exprt typeless(const irep_idt &id)
133  {
134  return symbol_exprt(id, typet());
135  }
136 
137  void set_identifier(const irep_idt &identifier)
138  {
139  set(ID_identifier, identifier);
140  }
141 
142  const irep_idt &get_identifier() const
143  {
144  return get(ID_identifier);
145  }
146 };
147 
148 // NOLINTNEXTLINE(readability/namespace)
149 namespace std
150 {
151 template <>
152 // NOLINTNEXTLINE(readability/identifiers)
153 struct hash<::symbol_exprt>
154 {
155  size_t operator()(const ::symbol_exprt &sym)
156  {
157  return irep_id_hash()(sym.get_identifier());
158  }
159 };
160 } // namespace std
161 
165 {
166 public:
170  : symbol_exprt(identifier, std::move(type))
171  {
172  }
173 
174  bool is_static_lifetime() const
175  {
176  return get_bool(ID_C_static_lifetime);
177  }
178 
180  {
181  return set(ID_C_static_lifetime, true);
182  }
183 
185  {
186  remove(ID_C_static_lifetime);
187  }
188 
189  bool is_thread_local() const
190  {
191  return get_bool(ID_C_thread_local);
192  }
193 
195  {
196  return set(ID_C_thread_local, true);
197  }
198 
200  {
201  remove(ID_C_thread_local);
202  }
203 };
204 
205 template <>
206 inline bool can_cast_expr<symbol_exprt>(const exprt &base)
207 {
208  return base.id() == ID_symbol;
209 }
210 
211 inline void validate_expr(const symbol_exprt &value)
212 {
213  validate_operands(value, 0, "Symbols must not have operands");
214 }
215 
222 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
223 {
224  PRECONDITION(expr.id()==ID_symbol);
225  const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
226  validate_expr(ret);
227  return ret;
228 }
229 
232 {
233  PRECONDITION(expr.id()==ID_symbol);
234  symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
235  validate_expr(ret);
236  return ret;
237 }
238 
239 
242 {
243 public:
247  : nullary_exprt(ID_nondet_symbol, std::move(type))
248  {
249  set_identifier(identifier);
250  }
251 
256  irep_idt identifier,
257  typet type,
258  source_locationt location)
259  : nullary_exprt(ID_nondet_symbol, std::move(type))
260  {
261  set_identifier(std::move(identifier));
262  add_source_location() = std::move(location);
263  }
264 
265  void set_identifier(const irep_idt &identifier)
266  {
267  set(ID_identifier, identifier);
268  }
269 
270  const irep_idt &get_identifier() const
271  {
272  return get(ID_identifier);
273  }
274 };
275 
276 template <>
278 {
279  return base.id() == ID_nondet_symbol;
280 }
281 
282 inline void validate_expr(const nondet_symbol_exprt &value)
283 {
284  validate_operands(value, 0, "Symbols must not have operands");
285 }
286 
294 {
295  PRECONDITION(expr.id()==ID_nondet_symbol);
296  const nondet_symbol_exprt &ret =
297  static_cast<const nondet_symbol_exprt &>(expr);
298  validate_expr(ret);
299  return ret;
300 }
301 
304 {
305  PRECONDITION(expr.id()==ID_symbol);
306  nondet_symbol_exprt &ret = static_cast<nondet_symbol_exprt &>(expr);
307  validate_expr(ret);
308  return ret;
309 }
310 
311 
314 {
315 public:
316  unary_exprt(const irep_idt &_id, const exprt &_op)
317  : expr_protectedt(_id, _op.type(), {_op})
318  {
319  }
320 
321  unary_exprt(const irep_idt &_id, exprt _op, typet _type)
322  : expr_protectedt(_id, std::move(_type), {std::move(_op)})
323  {
324  }
325 
326  const exprt &op() const
327  {
328  return op0();
329  }
330 
332  {
333  return op0();
334  }
335 
336  const exprt &op1() const = delete;
337  exprt &op1() = delete;
338  const exprt &op2() const = delete;
339  exprt &op2() = delete;
340  const exprt &op3() const = delete;
341  exprt &op3() = delete;
342 };
343 
344 template <>
345 inline bool can_cast_expr<unary_exprt>(const exprt &base)
346 {
347  return base.operands().size() == 1;
348 }
349 
350 inline void validate_expr(const unary_exprt &value)
351 {
352  validate_operands(value, 1, "Unary expressions must have one operand");
353 }
354 
361 inline const unary_exprt &to_unary_expr(const exprt &expr)
362 {
363  const unary_exprt &ret = static_cast<const unary_exprt &>(expr);
364  validate_expr(ret);
365  return ret;
366 }
367 
370 {
371  unary_exprt &ret = static_cast<unary_exprt &>(expr);
372  validate_expr(ret);
373  return ret;
374 }
375 
376 
378 class abs_exprt:public unary_exprt
379 {
380 public:
381  explicit abs_exprt(exprt _op) : unary_exprt(ID_abs, std::move(_op))
382  {
383  }
384 };
385 
386 template <>
387 inline bool can_cast_expr<abs_exprt>(const exprt &base)
388 {
389  return base.id() == ID_abs;
390 }
391 
392 inline void validate_expr(const abs_exprt &value)
393 {
394  validate_operands(value, 1, "Absolute value must have one operand");
395 }
396 
403 inline const abs_exprt &to_abs_expr(const exprt &expr)
404 {
405  PRECONDITION(expr.id()==ID_abs);
406  const abs_exprt &ret = static_cast<const abs_exprt &>(expr);
407  validate_expr(ret);
408  return ret;
409 }
410 
413 {
414  PRECONDITION(expr.id()==ID_abs);
415  abs_exprt &ret = static_cast<abs_exprt &>(expr);
416  validate_expr(ret);
417  return ret;
418 }
419 
420 
423 {
424 public:
426  : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
427  {
428  }
429 
430  explicit unary_minus_exprt(exprt _op)
431  : unary_exprt(ID_unary_minus, std::move(_op))
432  {
433  }
434 };
435 
436 template <>
437 inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
438 {
439  return base.id() == ID_unary_minus;
440 }
441 
442 inline void validate_expr(const unary_minus_exprt &value)
443 {
444  validate_operands(value, 1, "Unary minus must have one operand");
445 }
446 
453 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
454 {
455  PRECONDITION(expr.id()==ID_unary_minus);
456  const unary_minus_exprt &ret = static_cast<const unary_minus_exprt &>(expr);
457  validate_expr(ret);
458  return ret;
459 }
460 
463 {
464  PRECONDITION(expr.id()==ID_unary_minus);
465  unary_minus_exprt &ret = static_cast<unary_minus_exprt &>(expr);
466  validate_expr(ret);
467  return ret;
468 }
469 
472 {
473 public:
475  : unary_exprt(ID_unary_plus, std::move(op))
476  {
477  }
478 };
479 
480 template <>
481 inline bool can_cast_expr<unary_plus_exprt>(const exprt &base)
482 {
483  return base.id() == ID_unary_plus;
484 }
485 
486 inline void validate_expr(const unary_plus_exprt &value)
487 {
488  validate_operands(value, 1, "unary plus must have one operand");
489 }
490 
497 inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
498 {
499  PRECONDITION(expr.id() == ID_unary_plus);
500  const unary_plus_exprt &ret = static_cast<const unary_plus_exprt &>(expr);
501  validate_expr(ret);
502  return ret;
503 }
504 
507 {
508  PRECONDITION(expr.id() == ID_unary_plus);
509  unary_plus_exprt &ret = static_cast<unary_plus_exprt &>(expr);
510  validate_expr(ret);
511  return ret;
512 }
513 
517 {
518 public:
519  explicit predicate_exprt(const irep_idt &_id)
520  : expr_protectedt(_id, bool_typet())
521  {
522  }
523 };
524 
528 {
529 public:
531  : unary_exprt(_id, std::move(_op), bool_typet())
532  {
533  }
534 };
535 
539 {
540 public:
541  explicit sign_exprt(exprt _op)
542  : unary_predicate_exprt(ID_sign, std::move(_op))
543  {
544  }
545 };
546 
547 template <>
548 inline bool can_cast_expr<sign_exprt>(const exprt &base)
549 {
550  return base.id() == ID_sign;
551 }
552 
553 inline void validate_expr(const sign_exprt &expr)
554 {
555  validate_operands(expr, 1, "sign expression must have one operand");
556 }
557 
564 inline const sign_exprt &to_sign_expr(const exprt &expr)
565 {
566  PRECONDITION(expr.id() == ID_sign);
567  const sign_exprt &ret = static_cast<const sign_exprt &>(expr);
568  validate_expr(ret);
569  return ret;
570 }
571 
574 {
575  PRECONDITION(expr.id() == ID_sign);
576  sign_exprt &ret = static_cast<sign_exprt &>(expr);
577  validate_expr(ret);
578  return ret;
579 }
580 
583 {
584 public:
585  binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
586  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
587  {
588  }
589 
590  binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
591  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
592  {
593  }
594 
595  static void check(
596  const exprt &expr,
598  {
599  DATA_CHECK(
600  vm,
601  expr.operands().size() == 2,
602  "binary expression must have two operands");
603  }
604 
605  static void validate(
606  const exprt &expr,
607  const namespacet &,
609  {
610  check(expr, vm);
611  }
612 
614  {
615  return exprt::op0();
616  }
617 
618  const exprt &lhs() const
619  {
620  return exprt::op0();
621  }
622 
624  {
625  return exprt::op1();
626  }
627 
628  const exprt &rhs() const
629  {
630  return exprt::op1();
631  }
632 
633  // make op0 and op1 public
634  using exprt::op0;
635  using exprt::op1;
636 
637  const exprt &op2() const = delete;
638  exprt &op2() = delete;
639  const exprt &op3() const = delete;
640  exprt &op3() = delete;
641 };
642 
643 template <>
644 inline bool can_cast_expr<binary_exprt>(const exprt &base)
645 {
646  return base.operands().size() == 2;
647 }
648 
649 inline void validate_expr(const binary_exprt &value)
650 {
651  binary_exprt::check(value);
652 }
653 
660 inline const binary_exprt &to_binary_expr(const exprt &expr)
661 {
662  binary_exprt::check(expr);
663  return static_cast<const binary_exprt &>(expr);
664 }
665 
668 {
669  binary_exprt::check(expr);
670  return static_cast<binary_exprt &>(expr);
671 }
672 
676 {
677 public:
678  binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
679  : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
680  {
681  }
682 
683  static void check(
684  const exprt &expr,
686  {
687  binary_exprt::check(expr, vm);
688  }
689 
690  static void validate(
691  const exprt &expr,
692  const namespacet &ns,
694  {
695  binary_exprt::validate(expr, ns, vm);
696 
697  DATA_CHECK(
698  vm,
699  expr.type().id() == ID_bool,
700  "result of binary predicate expression should be of type bool");
701  }
702 };
703 
707 {
708 public:
709  binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
710  : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
711  {
712  }
713 
714  static void check(
715  const exprt &expr,
717  {
719  }
720 
721  static void validate(
722  const exprt &expr,
723  const namespacet &ns,
725  {
726  binary_predicate_exprt::validate(expr, ns, vm);
727 
728  // we now can safely assume that 'expr' is a binary predicate
729  const auto &expr_binary = static_cast<const binary_predicate_exprt &>(expr);
730 
731  // check that the types of the operands are the same
732  DATA_CHECK(
733  vm,
734  expr_binary.op0().type() == expr_binary.op1().type(),
735  "lhs and rhs of binary relation expression should have same type");
736  }
737 };
738 
739 template <>
741 {
742  return can_cast_expr<binary_exprt>(base);
743 }
744 
745 inline void validate_expr(const binary_relation_exprt &value)
746 {
748 }
749 
752 {
753 public:
755  : binary_relation_exprt{std::move(_lhs), ID_gt, std::move(_rhs)}
756  {
757  }
758 };
759 
760 template <>
761 inline bool can_cast_expr<greater_than_exprt>(const exprt &base)
762 {
763  return base.id() == ID_gt;
764 }
765 
766 inline void validate_expr(const greater_than_exprt &value)
767 {
769 }
770 
773 {
774 public:
776  : binary_relation_exprt{std::move(_lhs), ID_ge, std::move(_rhs)}
777  {
778  }
779 };
780 
781 template <>
783 {
784  return base.id() == ID_ge;
785 }
786 
788 {
790 }
791 
794 {
795 public:
797  : binary_relation_exprt{std::move(_lhs), ID_lt, std::move(_rhs)}
798  {
799  }
800 };
801 
802 template <>
803 inline bool can_cast_expr<less_than_exprt>(const exprt &base)
804 {
805  return base.id() == ID_lt;
806 }
807 
808 inline void validate_expr(const less_than_exprt &value)
809 {
811 }
812 
815 {
816 public:
818  : binary_relation_exprt{std::move(_lhs), ID_le, std::move(_rhs)}
819  {
820  }
821 };
822 
823 template <>
825 {
826  return base.id() == ID_le;
827 }
828 
829 inline void validate_expr(const less_than_or_equal_exprt &value)
830 {
832 }
833 
841 {
843  return static_cast<const binary_relation_exprt &>(expr);
844 }
845 
848 {
850  return static_cast<binary_relation_exprt &>(expr);
851 }
852 
853 
857 {
858 public:
859  multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
860  : expr_protectedt(_id, std::move(_type))
861  {
862  operands() = std::move(_operands);
863  }
864 
865  multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
866  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
867  {
868  }
869 
870  multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
871  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
872  {
873  }
874 
875  // In contrast to exprt::opX, the methods
876  // below check the size.
878  {
879  PRECONDITION(operands().size() >= 1);
880  return operands().front();
881  }
882 
884  {
885  PRECONDITION(operands().size() >= 2);
886  return operands()[1];
887  }
888 
890  {
891  PRECONDITION(operands().size() >= 3);
892  return operands()[2];
893  }
894 
896  {
897  PRECONDITION(operands().size() >= 4);
898  return operands()[3];
899  }
900 
901  const exprt &op0() const
902  {
903  PRECONDITION(operands().size() >= 1);
904  return operands().front();
905  }
906 
907  const exprt &op1() const
908  {
909  PRECONDITION(operands().size() >= 2);
910  return operands()[1];
911  }
912 
913  const exprt &op2() const
914  {
915  PRECONDITION(operands().size() >= 3);
916  return operands()[2];
917  }
918 
919  const exprt &op3() const
920  {
921  PRECONDITION(operands().size() >= 4);
922  return operands()[3];
923  }
924 };
925 
932 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
933 {
934  return static_cast<const multi_ary_exprt &>(expr);
935 }
936 
939 {
940  return static_cast<multi_ary_exprt &>(expr);
941 }
942 
943 
947 {
948 public:
949  plus_exprt(exprt _lhs, exprt _rhs)
950  : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
951  {
952  }
953 
954  plus_exprt(exprt _lhs, exprt _rhs, typet _type)
955  : multi_ary_exprt(
956  std::move(_lhs),
957  ID_plus,
958  std::move(_rhs),
959  std::move(_type))
960  {
961  }
962 
963  plus_exprt(operandst _operands, typet _type)
964  : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
965  {
966  }
967 };
968 
969 template <>
970 inline bool can_cast_expr<plus_exprt>(const exprt &base)
971 {
972  return base.id() == ID_plus;
973 }
974 
975 inline void validate_expr(const plus_exprt &value)
976 {
977  validate_operands(value, 2, "Plus must have two or more operands", true);
978 }
979 
986 inline const plus_exprt &to_plus_expr(const exprt &expr)
987 {
988  PRECONDITION(expr.id()==ID_plus);
989  const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
990  validate_expr(ret);
991  return ret;
992 }
993 
996 {
997  PRECONDITION(expr.id()==ID_plus);
998  plus_exprt &ret = static_cast<plus_exprt &>(expr);
999  validate_expr(ret);
1000  return ret;
1001 }
1002 
1003 
1006 {
1007 public:
1009  : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
1010  {
1011  }
1012 };
1013 
1014 template <>
1015 inline bool can_cast_expr<minus_exprt>(const exprt &base)
1016 {
1017  return base.id() == ID_minus;
1018 }
1019 
1020 inline void validate_expr(const minus_exprt &value)
1021 {
1022  validate_operands(value, 2, "Minus must have two or more operands", true);
1023 }
1024 
1031 inline const minus_exprt &to_minus_expr(const exprt &expr)
1032 {
1033  PRECONDITION(expr.id()==ID_minus);
1034  const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
1035  validate_expr(ret);
1036  return ret;
1037 }
1038 
1041 {
1042  PRECONDITION(expr.id()==ID_minus);
1043  minus_exprt &ret = static_cast<minus_exprt &>(expr);
1044  validate_expr(ret);
1045  return ret;
1046 }
1047 
1048 
1052 {
1053 public:
1054  mult_exprt(exprt _lhs, exprt _rhs)
1055  : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
1056  {
1057  }
1058 };
1059 
1060 template <>
1061 inline bool can_cast_expr<mult_exprt>(const exprt &base)
1062 {
1063  return base.id() == ID_mult;
1064 }
1065 
1066 inline void validate_expr(const mult_exprt &value)
1067 {
1068  validate_operands(value, 2, "Multiply must have two or more operands", true);
1069 }
1070 
1077 inline const mult_exprt &to_mult_expr(const exprt &expr)
1078 {
1079  PRECONDITION(expr.id()==ID_mult);
1080  const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1081  validate_expr(ret);
1082  return ret;
1083 }
1084 
1087 {
1088  PRECONDITION(expr.id()==ID_mult);
1089  mult_exprt &ret = static_cast<mult_exprt &>(expr);
1090  validate_expr(ret);
1091  return ret;
1092 }
1093 
1094 
1097 {
1098 public:
1099  div_exprt(exprt _lhs, exprt _rhs)
1100  : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1101  {
1102  }
1103 
1106  {
1107  return op0();
1108  }
1109 
1111  const exprt &dividend() const
1112  {
1113  return op0();
1114  }
1115 
1118  {
1119  return op1();
1120  }
1121 
1123  const exprt &divisor() const
1124  {
1125  return op1();
1126  }
1127 };
1128 
1129 template <>
1130 inline bool can_cast_expr<div_exprt>(const exprt &base)
1131 {
1132  return base.id() == ID_div;
1133 }
1134 
1135 inline void validate_expr(const div_exprt &value)
1136 {
1137  validate_operands(value, 2, "Divide must have two operands");
1138 }
1139 
1146 inline const div_exprt &to_div_expr(const exprt &expr)
1147 {
1148  PRECONDITION(expr.id()==ID_div);
1149  const div_exprt &ret = static_cast<const div_exprt &>(expr);
1150  validate_expr(ret);
1151  return ret;
1152 }
1153 
1156 {
1157  PRECONDITION(expr.id()==ID_div);
1158  div_exprt &ret = static_cast<div_exprt &>(expr);
1159  validate_expr(ret);
1160  return ret;
1161 }
1162 
1168 {
1169 public:
1170  mod_exprt(exprt _lhs, exprt _rhs)
1171  : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1172  {
1173  }
1174 
1177  {
1178  return op0();
1179  }
1180 
1182  const exprt &dividend() const
1183  {
1184  return op0();
1185  }
1186 
1189  {
1190  return op1();
1191  }
1192 
1194  const exprt &divisor() const
1195  {
1196  return op1();
1197  }
1198 };
1199 
1200 template <>
1201 inline bool can_cast_expr<mod_exprt>(const exprt &base)
1202 {
1203  return base.id() == ID_mod;
1204 }
1205 
1206 inline void validate_expr(const mod_exprt &value)
1207 {
1208  validate_operands(value, 2, "Modulo must have two operands");
1209 }
1210 
1217 inline const mod_exprt &to_mod_expr(const exprt &expr)
1218 {
1219  PRECONDITION(expr.id()==ID_mod);
1220  const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1221  validate_expr(ret);
1222  return ret;
1223 }
1224 
1227 {
1228  PRECONDITION(expr.id()==ID_mod);
1229  mod_exprt &ret = static_cast<mod_exprt &>(expr);
1230  validate_expr(ret);
1231  return ret;
1232 }
1233 
1236 {
1237 public:
1239  : binary_exprt(std::move(_lhs), ID_euclidean_mod, std::move(_rhs))
1240  {
1241  }
1242 
1245  {
1246  return op0();
1247  }
1248 
1250  const exprt &dividend() const
1251  {
1252  return op0();
1253  }
1254 
1257  {
1258  return op1();
1259  }
1260 
1262  const exprt &divisor() const
1263  {
1264  return op1();
1265  }
1266 };
1267 
1268 template <>
1270 {
1271  return base.id() == ID_euclidean_mod;
1272 }
1273 
1274 inline void validate_expr(const euclidean_mod_exprt &value)
1275 {
1276  validate_operands(value, 2, "Modulo must have two operands");
1277 }
1278 
1286 {
1287  PRECONDITION(expr.id() == ID_euclidean_mod);
1288  const euclidean_mod_exprt &ret =
1289  static_cast<const euclidean_mod_exprt &>(expr);
1290  validate_expr(ret);
1291  return ret;
1292 }
1293 
1296 {
1297  PRECONDITION(expr.id() == ID_euclidean_mod);
1298  euclidean_mod_exprt &ret = static_cast<euclidean_mod_exprt &>(expr);
1299  validate_expr(ret);
1300  return ret;
1301 }
1302 
1303 
1306 {
1307 public:
1309  : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1310  {
1311  PRECONDITION(lhs().type() == rhs().type());
1312  }
1313 
1314  static void check(
1315  const exprt &expr,
1317  {
1318  binary_relation_exprt::check(expr, vm);
1319  }
1320 
1321  static void validate(
1322  const exprt &expr,
1323  const namespacet &ns,
1325  {
1326  binary_relation_exprt::validate(expr, ns, vm);
1327  }
1328 };
1329 
1330 template <>
1331 inline bool can_cast_expr<equal_exprt>(const exprt &base)
1332 {
1333  return base.id() == ID_equal;
1334 }
1335 
1336 inline void validate_expr(const equal_exprt &value)
1337 {
1338  equal_exprt::check(value);
1339 }
1340 
1347 inline const equal_exprt &to_equal_expr(const exprt &expr)
1348 {
1349  PRECONDITION(expr.id()==ID_equal);
1350  equal_exprt::check(expr);
1351  return static_cast<const equal_exprt &>(expr);
1352 }
1353 
1356 {
1357  PRECONDITION(expr.id()==ID_equal);
1358  equal_exprt::check(expr);
1359  return static_cast<equal_exprt &>(expr);
1360 }
1361 
1362 
1365 {
1366 public:
1368  : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1369  {
1370  }
1371 };
1372 
1373 template <>
1374 inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1375 {
1376  return base.id() == ID_notequal;
1377 }
1378 
1379 inline void validate_expr(const notequal_exprt &value)
1380 {
1381  validate_operands(value, 2, "Inequality must have two operands");
1382 }
1383 
1390 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1391 {
1392  PRECONDITION(expr.id()==ID_notequal);
1393  const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1394  validate_expr(ret);
1395  return ret;
1396 }
1397 
1400 {
1401  PRECONDITION(expr.id()==ID_notequal);
1402  notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1403  validate_expr(ret);
1404  return ret;
1405 }
1406 
1407 
1410 {
1411 public:
1412  // _array must have either index or vector type.
1413  // When _array has array_type, the type of _index
1414  // must be array_type.index_type().
1415  // This will eventually be enforced using a precondition.
1416  index_exprt(const exprt &_array, exprt _index)
1417  : binary_exprt(
1418  _array,
1419  ID_index,
1420  std::move(_index),
1421  to_type_with_subtype(_array.type()).subtype())
1422  {
1423  const auto &array_op_type = _array.type();
1424  PRECONDITION(
1425  array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1426  }
1427 
1428  index_exprt(exprt _array, exprt _index, typet _type)
1429  : binary_exprt(
1430  std::move(_array),
1431  ID_index,
1432  std::move(_index),
1433  std::move(_type))
1434  {
1435  const auto &array_op_type = array().type();
1436  PRECONDITION(
1437  array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1438  }
1439 
1441  {
1442  return op0();
1443  }
1444 
1445  const exprt &array() const
1446  {
1447  return op0();
1448  }
1449 
1451  {
1452  return op1();
1453  }
1454 
1455  const exprt &index() const
1456  {
1457  return op1();
1458  }
1459 };
1460 
1461 template <>
1462 inline bool can_cast_expr<index_exprt>(const exprt &base)
1463 {
1464  return base.id() == ID_index;
1465 }
1466 
1467 inline void validate_expr(const index_exprt &value)
1468 {
1469  validate_operands(value, 2, "Array index must have two operands");
1470 }
1471 
1478 inline const index_exprt &to_index_expr(const exprt &expr)
1479 {
1480  PRECONDITION(expr.id()==ID_index);
1481  const index_exprt &ret = static_cast<const index_exprt &>(expr);
1482  validate_expr(ret);
1483  return ret;
1484 }
1485 
1488 {
1489  PRECONDITION(expr.id()==ID_index);
1490  index_exprt &ret = static_cast<index_exprt &>(expr);
1491  validate_expr(ret);
1492  return ret;
1493 }
1494 
1495 
1498 {
1499 public:
1500  explicit array_of_exprt(exprt _what, array_typet _type)
1501  : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1502  {
1503  }
1504 
1505  const array_typet &type() const
1506  {
1507  return static_cast<const array_typet &>(unary_exprt::type());
1508  }
1509 
1511  {
1512  return static_cast<array_typet &>(unary_exprt::type());
1513  }
1514 
1516  {
1517  return op0();
1518  }
1519 
1520  const exprt &what() const
1521  {
1522  return op0();
1523  }
1524 };
1525 
1526 template <>
1527 inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1528 {
1529  return base.id() == ID_array_of;
1530 }
1531 
1532 inline void validate_expr(const array_of_exprt &value)
1533 {
1534  validate_operands(value, 1, "'Array of' must have one operand");
1535 }
1536 
1543 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1544 {
1545  PRECONDITION(expr.id()==ID_array_of);
1546  const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1547  validate_expr(ret);
1548  return ret;
1549 }
1550 
1553 {
1554  PRECONDITION(expr.id()==ID_array_of);
1555  array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1556  validate_expr(ret);
1557  return ret;
1558 }
1559 
1560 
1563 {
1564 public:
1566  : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1567  {
1568  }
1569 
1570  const array_typet &type() const
1571  {
1572  return static_cast<const array_typet &>(multi_ary_exprt::type());
1573  }
1574 
1576  {
1577  return static_cast<array_typet &>(multi_ary_exprt::type());
1578  }
1579 
1581  {
1582  return exprt::with_source_location<array_exprt>(other);
1583  }
1584 
1586  {
1587  return std::move(*this).exprt::with_source_location<array_exprt>(other);
1588  }
1589 };
1590 
1591 template <>
1592 inline bool can_cast_expr<array_exprt>(const exprt &base)
1593 {
1594  return base.id() == ID_array;
1595 }
1596 
1603 inline const array_exprt &to_array_expr(const exprt &expr)
1604 {
1605  PRECONDITION(expr.id()==ID_array);
1606  return static_cast<const array_exprt &>(expr);
1607 }
1608 
1611 {
1612  PRECONDITION(expr.id()==ID_array);
1613  return static_cast<array_exprt &>(expr);
1614 }
1615 
1619 {
1620 public:
1622  : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1623  {
1624  }
1625 
1626  const array_typet &type() const
1627  {
1628  return static_cast<const array_typet &>(multi_ary_exprt::type());
1629  }
1630 
1632  {
1633  return static_cast<array_typet &>(multi_ary_exprt::type());
1634  }
1635 
1637  void add(exprt index, exprt value)
1638  {
1639  add_to_operands(std::move(index), std::move(value));
1640  }
1641 };
1642 
1643 template <>
1644 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1645 {
1646  return base.id() == ID_array_list;
1647 }
1648 
1649 inline void validate_expr(const array_list_exprt &value)
1650 {
1651  PRECONDITION(value.operands().size() % 2 == 0);
1652 }
1653 
1654 inline const array_list_exprt &to_array_list_expr(const exprt &expr)
1655 {
1657  auto &ret = static_cast<const array_list_exprt &>(expr);
1658  validate_expr(ret);
1659  return ret;
1660 }
1661 
1663 {
1665  auto &ret = static_cast<array_list_exprt &>(expr);
1666  validate_expr(ret);
1667  return ret;
1668 }
1669 
1672 {
1673 public:
1675  : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1676  {
1677  }
1678 };
1679 
1680 template <>
1681 inline bool can_cast_expr<vector_exprt>(const exprt &base)
1682 {
1683  return base.id() == ID_vector;
1684 }
1685 
1692 inline const vector_exprt &to_vector_expr(const exprt &expr)
1693 {
1694  PRECONDITION(expr.id()==ID_vector);
1695  return static_cast<const vector_exprt &>(expr);
1696 }
1697 
1700 {
1701  PRECONDITION(expr.id()==ID_vector);
1702  return static_cast<vector_exprt &>(expr);
1703 }
1704 
1705 
1708 {
1709 public:
1710  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1711  : unary_exprt(ID_union, std::move(_value), std::move(_type))
1712  {
1713  set_component_name(_component_name);
1714  }
1715 
1717  {
1718  return get(ID_component_name);
1719  }
1720 
1721  void set_component_name(const irep_idt &component_name)
1722  {
1723  set(ID_component_name, component_name);
1724  }
1725 
1726  std::size_t get_component_number() const
1727  {
1728  return get_size_t(ID_component_number);
1729  }
1730 
1731  void set_component_number(std::size_t component_number)
1732  {
1733  set_size_t(ID_component_number, component_number);
1734  }
1735 };
1736 
1737 template <>
1738 inline bool can_cast_expr<union_exprt>(const exprt &base)
1739 {
1740  return base.id() == ID_union;
1741 }
1742 
1743 inline void validate_expr(const union_exprt &value)
1744 {
1745  validate_operands(value, 1, "Union constructor must have one operand");
1746 }
1747 
1754 inline const union_exprt &to_union_expr(const exprt &expr)
1755 {
1756  PRECONDITION(expr.id()==ID_union);
1757  const union_exprt &ret = static_cast<const union_exprt &>(expr);
1758  validate_expr(ret);
1759  return ret;
1760 }
1761 
1764 {
1765  PRECONDITION(expr.id()==ID_union);
1766  union_exprt &ret = static_cast<union_exprt &>(expr);
1767  validate_expr(ret);
1768  return ret;
1769 }
1770 
1774 {
1775 public:
1776  explicit empty_union_exprt(typet _type)
1777  : nullary_exprt(ID_empty_union, std::move(_type))
1778  {
1779  }
1780 };
1781 
1782 template <>
1783 inline bool can_cast_expr<empty_union_exprt>(const exprt &base)
1784 {
1785  return base.id() == ID_empty_union;
1786 }
1787 
1788 inline void validate_expr(const empty_union_exprt &value)
1789 {
1791  value, 0, "Empty-union constructor must not have any operand");
1792 }
1793 
1800 inline const empty_union_exprt &to_empty_union_expr(const exprt &expr)
1801 {
1802  PRECONDITION(expr.id() == ID_empty_union);
1803  const empty_union_exprt &ret = static_cast<const empty_union_exprt &>(expr);
1804  validate_expr(ret);
1805  return ret;
1806 }
1807 
1810 {
1811  PRECONDITION(expr.id() == ID_empty_union);
1812  empty_union_exprt &ret = static_cast<empty_union_exprt &>(expr);
1813  validate_expr(ret);
1814  return ret;
1815 }
1816 
1819 {
1820 public:
1821  struct_exprt(operandst _operands, typet _type)
1822  : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1823  {
1824  }
1825 
1826  exprt &component(const irep_idt &name, const namespacet &ns);
1827  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1828 };
1829 
1830 template <>
1831 inline bool can_cast_expr<struct_exprt>(const exprt &base)
1832 {
1833  return base.id() == ID_struct;
1834 }
1835 
1842 inline const struct_exprt &to_struct_expr(const exprt &expr)
1843 {
1844  PRECONDITION(expr.id()==ID_struct);
1845  return static_cast<const struct_exprt &>(expr);
1846 }
1847 
1850 {
1851  PRECONDITION(expr.id()==ID_struct);
1852  return static_cast<struct_exprt &>(expr);
1853 }
1854 
1855 
1858 {
1859 public:
1861  : binary_exprt(
1862  std::move(_real),
1863  ID_complex,
1864  std::move(_imag),
1865  std::move(_type))
1866  {
1867  }
1868 
1870  {
1871  return op0();
1872  }
1873 
1874  const exprt &real() const
1875  {
1876  return op0();
1877  }
1878 
1880  {
1881  return op1();
1882  }
1883 
1884  const exprt &imag() const
1885  {
1886  return op1();
1887  }
1888 };
1889 
1890 template <>
1891 inline bool can_cast_expr<complex_exprt>(const exprt &base)
1892 {
1893  return base.id() == ID_complex;
1894 }
1895 
1896 inline void validate_expr(const complex_exprt &value)
1897 {
1898  validate_operands(value, 2, "Complex constructor must have two operands");
1899 }
1900 
1907 inline const complex_exprt &to_complex_expr(const exprt &expr)
1908 {
1909  PRECONDITION(expr.id()==ID_complex);
1910  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1911  validate_expr(ret);
1912  return ret;
1913 }
1914 
1917 {
1918  PRECONDITION(expr.id()==ID_complex);
1919  complex_exprt &ret = static_cast<complex_exprt &>(expr);
1920  validate_expr(ret);
1921  return ret;
1922 }
1923 
1926 {
1927 public:
1928  explicit complex_real_exprt(const exprt &op)
1929  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1930  {
1931  }
1932 };
1933 
1934 template <>
1936 {
1937  return base.id() == ID_complex_real;
1938 }
1939 
1940 inline void validate_expr(const complex_real_exprt &expr)
1941 {
1943  expr, 1, "real part retrieval operation must have one operand");
1944 }
1945 
1953 {
1954  PRECONDITION(expr.id() == ID_complex_real);
1955  const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
1956  validate_expr(ret);
1957  return ret;
1958 }
1959 
1962 {
1963  PRECONDITION(expr.id() == ID_complex_real);
1964  complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
1965  validate_expr(ret);
1966  return ret;
1967 }
1968 
1971 {
1972 public:
1973  explicit complex_imag_exprt(const exprt &op)
1974  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
1975  {
1976  }
1977 };
1978 
1979 template <>
1981 {
1982  return base.id() == ID_complex_imag;
1983 }
1984 
1985 inline void validate_expr(const complex_imag_exprt &expr)
1986 {
1988  expr, 1, "imaginary part retrieval operation must have one operand");
1989 }
1990 
1998 {
1999  PRECONDITION(expr.id() == ID_complex_imag);
2000  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
2001  validate_expr(ret);
2002  return ret;
2003 }
2004 
2007 {
2008  PRECONDITION(expr.id() == ID_complex_imag);
2009  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
2010  validate_expr(ret);
2011  return ret;
2012 }
2013 
2014 
2017 {
2018 public:
2020  : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2021  {
2022  }
2023 
2024  // returns a typecast if the type doesn't already match
2025  static exprt conditional_cast(const exprt &expr, const typet &type)
2026  {
2027  if(expr.type() == type)
2028  return expr;
2029  else
2030  return typecast_exprt(expr, type);
2031  }
2032 };
2033 
2034 template <>
2035 inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2036 {
2037  return base.id() == ID_typecast;
2038 }
2039 
2040 inline void validate_expr(const typecast_exprt &value)
2041 {
2042  validate_operands(value, 1, "Typecast must have one operand");
2043 }
2044 
2051 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2052 {
2053  PRECONDITION(expr.id()==ID_typecast);
2054  const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
2055  validate_expr(ret);
2056  return ret;
2057 }
2058 
2061 {
2062  PRECONDITION(expr.id()==ID_typecast);
2063  typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
2064  validate_expr(ret);
2065  return ret;
2066 }
2067 
2068 
2071 {
2072 public:
2074  : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2075  {
2076  }
2077 
2079  : multi_ary_exprt(
2080  ID_and,
2081  {std::move(op0), std::move(op1), std::move(op2)},
2082  bool_typet())
2083  {
2084  }
2085 
2087  : multi_ary_exprt(
2088  ID_and,
2089  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2090  bool_typet())
2091  {
2092  }
2093 
2094  explicit and_exprt(exprt::operandst _operands)
2095  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2096  {
2097  }
2098 };
2099 
2103 
2105 
2106 template <>
2107 inline bool can_cast_expr<and_exprt>(const exprt &base)
2108 {
2109  return base.id() == ID_and;
2110 }
2111 
2118 inline const and_exprt &to_and_expr(const exprt &expr)
2119 {
2120  PRECONDITION(expr.id()==ID_and);
2121  return static_cast<const and_exprt &>(expr);
2122 }
2123 
2126 {
2127  PRECONDITION(expr.id()==ID_and);
2128  return static_cast<and_exprt &>(expr);
2129 }
2130 
2131 
2134 {
2135 public:
2137  : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2138  {
2139  }
2140 };
2141 
2142 template <>
2143 inline bool can_cast_expr<implies_exprt>(const exprt &base)
2144 {
2145  return base.id() == ID_implies;
2146 }
2147 
2148 inline void validate_expr(const implies_exprt &value)
2149 {
2150  validate_operands(value, 2, "Implies must have two operands");
2151 }
2152 
2159 inline const implies_exprt &to_implies_expr(const exprt &expr)
2160 {
2161  PRECONDITION(expr.id()==ID_implies);
2162  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2163  validate_expr(ret);
2164  return ret;
2165 }
2166 
2169 {
2170  PRECONDITION(expr.id()==ID_implies);
2171  implies_exprt &ret = static_cast<implies_exprt &>(expr);
2172  validate_expr(ret);
2173  return ret;
2174 }
2175 
2176 
2179 {
2180 public:
2182  : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2183  {
2184  }
2185 
2187  : multi_ary_exprt(
2188  ID_or,
2189  {std::move(op0), std::move(op1), std::move(op2)},
2190  bool_typet())
2191  {
2192  }
2193 
2195  : multi_ary_exprt(
2196  ID_or,
2197  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2198  bool_typet())
2199  {
2200  }
2201 
2202  explicit or_exprt(exprt::operandst _operands)
2203  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2204  {
2205  }
2206 };
2207 
2211 
2213 
2214 template <>
2215 inline bool can_cast_expr<or_exprt>(const exprt &base)
2216 {
2217  return base.id() == ID_or;
2218 }
2219 
2226 inline const or_exprt &to_or_expr(const exprt &expr)
2227 {
2228  PRECONDITION(expr.id()==ID_or);
2229  return static_cast<const or_exprt &>(expr);
2230 }
2231 
2233 inline or_exprt &to_or_expr(exprt &expr)
2234 {
2235  PRECONDITION(expr.id()==ID_or);
2236  return static_cast<or_exprt &>(expr);
2237 }
2238 
2239 
2242 {
2243 public:
2244  xor_exprt(exprt _op0, exprt _op1)
2245  : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2246  {
2247  }
2248 };
2249 
2250 template <>
2251 inline bool can_cast_expr<xor_exprt>(const exprt &base)
2252 {
2253  return base.id() == ID_xor;
2254 }
2255 
2262 inline const xor_exprt &to_xor_expr(const exprt &expr)
2263 {
2264  PRECONDITION(expr.id()==ID_xor);
2265  return static_cast<const xor_exprt &>(expr);
2266 }
2267 
2270 {
2271  PRECONDITION(expr.id()==ID_xor);
2272  return static_cast<xor_exprt &>(expr);
2273 }
2274 
2275 
2278 {
2279 public:
2280  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2281  {
2282  PRECONDITION(as_const(*this).op().type().id() == ID_bool);
2283  }
2284 };
2285 
2286 template <>
2287 inline bool can_cast_expr<not_exprt>(const exprt &base)
2288 {
2289  return base.id() == ID_not;
2290 }
2291 
2292 inline void validate_expr(const not_exprt &value)
2293 {
2294  validate_operands(value, 1, "Not must have one operand");
2295 }
2296 
2303 inline const not_exprt &to_not_expr(const exprt &expr)
2304 {
2305  PRECONDITION(expr.id()==ID_not);
2306  const not_exprt &ret = static_cast<const not_exprt &>(expr);
2307  validate_expr(ret);
2308  return ret;
2309 }
2310 
2313 {
2314  PRECONDITION(expr.id()==ID_not);
2315  not_exprt &ret = static_cast<not_exprt &>(expr);
2316  validate_expr(ret);
2317  return ret;
2318 }
2319 
2320 
2322 class if_exprt : public ternary_exprt
2323 {
2324 public:
2326  : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2327  {
2328  }
2329 
2331  : ternary_exprt(
2332  ID_if,
2333  std::move(cond),
2334  std::move(t),
2335  std::move(f),
2336  std::move(type))
2337  {
2338  }
2339 
2341  {
2342  return op0();
2343  }
2344 
2345  const exprt &cond() const
2346  {
2347  return op0();
2348  }
2349 
2351  {
2352  return op1();
2353  }
2354 
2355  const exprt &true_case() const
2356  {
2357  return op1();
2358  }
2359 
2361  {
2362  return op2();
2363  }
2364 
2365  const exprt &false_case() const
2366  {
2367  return op2();
2368  }
2369 
2370  static void check(
2371  const exprt &expr,
2373  {
2374  ternary_exprt::check(expr, vm);
2375  }
2376 
2377  static void validate(
2378  const exprt &expr,
2379  const namespacet &ns,
2381  {
2382  ternary_exprt::validate(expr, ns, vm);
2383  }
2384 };
2385 
2386 template <>
2387 inline bool can_cast_expr<if_exprt>(const exprt &base)
2388 {
2389  return base.id() == ID_if;
2390 }
2391 
2392 inline void validate_expr(const if_exprt &value)
2393 {
2394  validate_operands(value, 3, "If-then-else must have three operands");
2395 }
2396 
2403 inline const if_exprt &to_if_expr(const exprt &expr)
2404 {
2405  PRECONDITION(expr.id()==ID_if);
2406  const if_exprt &ret = static_cast<const if_exprt &>(expr);
2407  validate_expr(ret);
2408  return ret;
2409 }
2410 
2412 inline if_exprt &to_if_expr(exprt &expr)
2413 {
2414  PRECONDITION(expr.id()==ID_if);
2415  if_exprt &ret = static_cast<if_exprt &>(expr);
2416  validate_expr(ret);
2417  return ret;
2418 }
2419 
2424 {
2425 public:
2426  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
2427  : expr_protectedt(
2428  ID_with,
2429  _old.type(),
2430  {_old, std::move(_where), std::move(_new_value)})
2431  {
2432  }
2433 
2435  {
2436  return op0();
2437  }
2438 
2439  const exprt &old() const
2440  {
2441  return op0();
2442  }
2443 
2445  {
2446  return op1();
2447  }
2448 
2449  const exprt &where() const
2450  {
2451  return op1();
2452  }
2453 
2455  {
2456  return op2();
2457  }
2458 
2459  const exprt &new_value() const
2460  {
2461  return op2();
2462  }
2463 };
2464 
2465 template <>
2466 inline bool can_cast_expr<with_exprt>(const exprt &base)
2467 {
2468  return base.id() == ID_with;
2469 }
2470 
2471 inline void validate_expr(const with_exprt &value)
2472 {
2474  value, 3, "array/structure update must have at least 3 operands", true);
2476  value.operands().size() % 2 == 1,
2477  "array/structure update must have an odd number of operands");
2478 }
2479 
2486 inline const with_exprt &to_with_expr(const exprt &expr)
2487 {
2488  PRECONDITION(expr.id()==ID_with);
2489  const with_exprt &ret = static_cast<const with_exprt &>(expr);
2490  validate_expr(ret);
2491  return ret;
2492 }
2493 
2496 {
2497  PRECONDITION(expr.id()==ID_with);
2498  with_exprt &ret = static_cast<with_exprt &>(expr);
2499  validate_expr(ret);
2500  return ret;
2501 }
2502 
2504 {
2505 public:
2506  explicit index_designatort(exprt _index)
2507  : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
2508  {
2509  }
2510 
2511  const exprt &index() const
2512  {
2513  return op0();
2514  }
2515 
2517  {
2518  return op0();
2519  }
2520 };
2521 
2522 template <>
2523 inline bool can_cast_expr<index_designatort>(const exprt &base)
2524 {
2525  return base.id() == ID_index_designator;
2526 }
2527 
2528 inline void validate_expr(const index_designatort &value)
2529 {
2530  validate_operands(value, 1, "Index designator must have one operand");
2531 }
2532 
2539 inline const index_designatort &to_index_designator(const exprt &expr)
2540 {
2541  PRECONDITION(expr.id()==ID_index_designator);
2542  const index_designatort &ret = static_cast<const index_designatort &>(expr);
2543  validate_expr(ret);
2544  return ret;
2545 }
2546 
2549 {
2550  PRECONDITION(expr.id()==ID_index_designator);
2551  index_designatort &ret = static_cast<index_designatort &>(expr);
2552  validate_expr(ret);
2553  return ret;
2554 }
2555 
2557 {
2558 public:
2559  explicit member_designatort(const irep_idt &_component_name)
2560  : expr_protectedt(ID_member_designator, typet())
2561  {
2562  set(ID_component_name, _component_name);
2563  }
2564 
2566  {
2567  return get(ID_component_name);
2568  }
2569 };
2570 
2571 template <>
2573 {
2574  return base.id() == ID_member_designator;
2575 }
2576 
2577 inline void validate_expr(const member_designatort &value)
2578 {
2579  validate_operands(value, 0, "Member designator must not have operands");
2580 }
2581 
2589 {
2590  PRECONDITION(expr.id()==ID_member_designator);
2591  const member_designatort &ret = static_cast<const member_designatort &>(expr);
2592  validate_expr(ret);
2593  return ret;
2594 }
2595 
2598 {
2599  PRECONDITION(expr.id()==ID_member_designator);
2600  member_designatort &ret = static_cast<member_designatort &>(expr);
2601  validate_expr(ret);
2602  return ret;
2603 }
2604 
2605 
2608 {
2609 public:
2610  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
2611  : ternary_exprt(
2612  ID_update,
2613  _old,
2614  std::move(_designator),
2615  std::move(_new_value),
2616  _old.type())
2617  {
2618  }
2619 
2621  {
2622  return op0();
2623  }
2624 
2625  const exprt &old() const
2626  {
2627  return op0();
2628  }
2629 
2630  // the designator operands are either
2631  // 1) member_designator or
2632  // 2) index_designator
2633  // as defined above
2635  {
2636  return op1().operands();
2637  }
2638 
2640  {
2641  return op1().operands();
2642  }
2643 
2645  {
2646  return op2();
2647  }
2648 
2649  const exprt &new_value() const
2650  {
2651  return op2();
2652  }
2653 
2654  static void check(
2655  const exprt &expr,
2657  {
2658  ternary_exprt::check(expr, vm);
2659  }
2660 
2661  static void validate(
2662  const exprt &expr,
2663  const namespacet &ns,
2665  {
2666  ternary_exprt::validate(expr, ns, vm);
2667  }
2668 };
2669 
2670 template <>
2671 inline bool can_cast_expr<update_exprt>(const exprt &base)
2672 {
2673  return base.id() == ID_update;
2674 }
2675 
2676 inline void validate_expr(const update_exprt &value)
2677 {
2679  value, 3, "Array/structure update must have three operands");
2680 }
2681 
2688 inline const update_exprt &to_update_expr(const exprt &expr)
2689 {
2690  PRECONDITION(expr.id()==ID_update);
2691  const update_exprt &ret = static_cast<const update_exprt &>(expr);
2692  validate_expr(ret);
2693  return ret;
2694 }
2695 
2698 {
2699  PRECONDITION(expr.id()==ID_update);
2700  update_exprt &ret = static_cast<update_exprt &>(expr);
2701  validate_expr(ret);
2702  return ret;
2703 }
2704 
2705 
2706 #if 0
2707 class array_update_exprt:public expr_protectedt
2709 {
2710 public:
2711  array_update_exprt(
2712  const exprt &_array,
2713  const exprt &_index,
2714  const exprt &_new_value):
2715  exprt(ID_array_update, _array.type())
2716  {
2717  add_to_operands(_array, _index, _new_value);
2718  }
2719 
2720  array_update_exprt():expr_protectedt(ID_array_update)
2721  {
2722  operands().resize(3);
2723  }
2724 
2725  exprt &array()
2726  {
2727  return op0();
2728  }
2729 
2730  const exprt &array() const
2731  {
2732  return op0();
2733  }
2734 
2735  exprt &index()
2736  {
2737  return op1();
2738  }
2739 
2740  const exprt &index() const
2741  {
2742  return op1();
2743  }
2744 
2745  exprt &new_value()
2746  {
2747  return op2();
2748  }
2749 
2750  const exprt &new_value() const
2751  {
2752  return op2();
2753  }
2754 };
2755 
2756 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2757 {
2758  return base.id()==ID_array_update;
2759 }
2760 
2761 inline void validate_expr(const array_update_exprt &value)
2762 {
2763  validate_operands(value, 3, "Array update must have three operands");
2764 }
2765 
2772 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2773 {
2774  PRECONDITION(expr.id()==ID_array_update);
2775  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2776  validate_expr(ret);
2777  return ret;
2778 }
2779 
2781 inline array_update_exprt &to_array_update_expr(exprt &expr)
2782 {
2783  PRECONDITION(expr.id()==ID_array_update);
2784  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2785  validate_expr(ret);
2786  return ret;
2787 }
2788 
2789 #endif
2790 
2791 
2794 {
2795 public:
2796  member_exprt(exprt op, const irep_idt &component_name, typet _type)
2797  : unary_exprt(ID_member, std::move(op), std::move(_type))
2798  {
2799  const auto &compound_type_id = compound().type().id();
2800  PRECONDITION(
2801  compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2802  compound_type_id == ID_struct || compound_type_id == ID_union);
2803  set_component_name(component_name);
2804  }
2805 
2807  : unary_exprt(ID_member, std::move(op), c.type())
2808  {
2809  const auto &compound_type_id = compound().type().id();
2810  PRECONDITION(
2811  compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2812  compound_type_id == ID_struct || compound_type_id == ID_union);
2814  }
2815 
2817  {
2818  return get(ID_component_name);
2819  }
2820 
2821  void set_component_name(const irep_idt &component_name)
2822  {
2823  set(ID_component_name, component_name);
2824  }
2825 
2826  std::size_t get_component_number() const
2827  {
2828  return get_size_t(ID_component_number);
2829  }
2830 
2831  // will go away, use compound()
2832  const exprt &struct_op() const
2833  {
2834  return op0();
2835  }
2836 
2837  // will go away, use compound()
2839  {
2840  return op0();
2841  }
2842 
2843  const exprt &compound() const
2844  {
2845  return op0();
2846  }
2847 
2849  {
2850  return op0();
2851  }
2852 
2853  static void check(
2854  const exprt &expr,
2856  {
2857  DATA_CHECK(
2858  vm,
2859  expr.operands().size() == 1,
2860  "member expression must have one operand");
2861  }
2862 
2863  static void validate(
2864  const exprt &expr,
2865  const namespacet &ns,
2867 };
2868 
2869 template <>
2870 inline bool can_cast_expr<member_exprt>(const exprt &base)
2871 {
2872  return base.id() == ID_member;
2873 }
2874 
2875 inline void validate_expr(const member_exprt &value)
2876 {
2877  validate_operands(value, 1, "Extract member must have one operand");
2878 }
2879 
2886 inline const member_exprt &to_member_expr(const exprt &expr)
2887 {
2888  PRECONDITION(expr.id()==ID_member);
2889  const member_exprt &ret = static_cast<const member_exprt &>(expr);
2890  validate_expr(ret);
2891  return ret;
2892 }
2893 
2896 {
2897  PRECONDITION(expr.id()==ID_member);
2898  member_exprt &ret = static_cast<member_exprt &>(expr);
2899  validate_expr(ret);
2900  return ret;
2901 }
2902 
2903 
2906 {
2907 public:
2908  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
2909  {
2910  }
2911 };
2912 
2913 template <>
2914 inline bool can_cast_expr<type_exprt>(const exprt &base)
2915 {
2916  return base.id() == ID_type;
2917 }
2918 
2925 inline const type_exprt &to_type_expr(const exprt &expr)
2926 {
2928  const type_exprt &ret = static_cast<const type_exprt &>(expr);
2929  return ret;
2930 }
2931 
2934 {
2936  type_exprt &ret = static_cast<type_exprt &>(expr);
2937  return ret;
2938 }
2939 
2942 {
2943 public:
2944  constant_exprt(const irep_idt &_value, typet _type)
2945  : nullary_exprt(ID_constant, std::move(_type))
2946  {
2947  set_value(_value);
2948  }
2949 
2950  const irep_idt &get_value() const
2951  {
2952  return get(ID_value);
2953  }
2954 
2955  void set_value(const irep_idt &value)
2956  {
2957  set(ID_value, value);
2958  }
2959 
2960  bool value_is_zero_string() const;
2961 
2962  static void check(
2963  const exprt &expr,
2965 
2966  static void validate(
2967  const exprt &expr,
2968  const namespacet &,
2970  {
2971  check(expr, vm);
2972  }
2973 };
2974 
2975 template <>
2976 inline bool can_cast_expr<constant_exprt>(const exprt &base)
2977 {
2978  return base.id() == ID_constant;
2979 }
2980 
2981 inline void validate_expr(const constant_exprt &value)
2982 {
2983  validate_operands(value, 0, "Constants must not have operands");
2984 }
2985 
2992 inline const constant_exprt &to_constant_expr(const exprt &expr)
2993 {
2994  PRECONDITION(expr.id()==ID_constant);
2995  return static_cast<const constant_exprt &>(expr);
2996 }
2997 
3000 {
3001  PRECONDITION(expr.id()==ID_constant);
3002  return static_cast<constant_exprt &>(expr);
3003 }
3004 
3005 
3008 {
3009 public:
3011  {
3012  }
3013 };
3014 
3017 {
3018 public:
3020  {
3021  }
3022 };
3023 
3025 class nil_exprt : public nullary_exprt
3026 {
3027 public:
3029  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
3030  {
3031  }
3032 };
3033 
3034 template <>
3035 inline bool can_cast_expr<nil_exprt>(const exprt &base)
3036 {
3037  return base.id() == ID_nil;
3038 }
3039 
3042 {
3043 public:
3044  explicit infinity_exprt(typet _type)
3045  : nullary_exprt(ID_infinity, std::move(_type))
3046  {
3047  }
3048 };
3049 
3052 {
3053 public:
3054  using variablest = std::vector<symbol_exprt>;
3055 
3058  irep_idt _id,
3059  const variablest &_variables,
3060  exprt _where,
3061  typet _type)
3062  : binary_exprt(
3064  ID_tuple,
3065  (const operandst &)_variables,
3066  typet(ID_tuple)),
3067  _id,
3068  std::move(_where),
3069  std::move(_type))
3070  {
3071  }
3072 
3074  {
3075  return (variablest &)to_multi_ary_expr(op0()).operands();
3076  }
3077 
3078  const variablest &variables() const
3079  {
3080  return (variablest &)to_multi_ary_expr(op0()).operands();
3081  }
3082 
3084  {
3085  return op1();
3086  }
3087 
3088  const exprt &where() const
3089  {
3090  return op1();
3091  }
3092 
3095  exprt instantiate(const exprt::operandst &) const;
3096 
3099  exprt instantiate(const variablest &) const;
3100 };
3101 
3102 inline void validate_expr(const binding_exprt &binding_expr)
3103 {
3105  binding_expr, 2, "Binding expressions must have two operands");
3106 }
3107 
3114 inline const binding_exprt &to_binding_expr(const exprt &expr)
3115 {
3116  PRECONDITION(
3117  expr.id() == ID_forall || expr.id() == ID_exists ||
3118  expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3119  const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
3120  validate_expr(ret);
3121  return ret;
3122 }
3123 
3131 {
3132  PRECONDITION(
3133  expr.id() == ID_forall || expr.id() == ID_exists ||
3134  expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3135  binding_exprt &ret = static_cast<binding_exprt &>(expr);
3136  validate_expr(ret);
3137  return ret;
3138 }
3139 
3141 class let_exprt : public binary_exprt
3142 {
3143 public:
3146  operandst values,
3147  const exprt &where)
3148  : binary_exprt(
3149  binding_exprt(
3150  ID_let_binding,
3151  std::move(variables),
3152  where,
3153  where.type()),
3154  ID_let,
3155  multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
3156  where.type())
3157  {
3158  PRECONDITION(this->variables().size() == this->values().size());
3159  }
3160 
3163  : let_exprt(
3164  binding_exprt::variablest{std::move(symbol)},
3165  operandst{std::move(value)},
3166  where)
3167  {
3168  }
3169 
3171  {
3172  return static_cast<binding_exprt &>(op0());
3173  }
3174 
3175  const binding_exprt &binding() const
3176  {
3177  return static_cast<const binding_exprt &>(op0());
3178  }
3179 
3182  {
3183  auto &variables = binding().variables();
3184  PRECONDITION(variables.size() == 1);
3185  return variables.front();
3186  }
3187 
3189  const symbol_exprt &symbol() const
3190  {
3191  const auto &variables = binding().variables();
3192  PRECONDITION(variables.size() == 1);
3193  return variables.front();
3194  }
3195 
3198  {
3199  auto &values = this->values();
3200  PRECONDITION(values.size() == 1);
3201  return values.front();
3202  }
3203 
3205  const exprt &value() const
3206  {
3207  const auto &values = this->values();
3208  PRECONDITION(values.size() == 1);
3209  return values.front();
3210  }
3211 
3213  {
3214  return static_cast<multi_ary_exprt &>(op1()).operands();
3215  }
3216 
3217  const operandst &values() const
3218  {
3219  return static_cast<const multi_ary_exprt &>(op1()).operands();
3220  }
3221 
3224  {
3225  return binding().variables();
3226  }
3227 
3230  {
3231  return binding().variables();
3232  }
3233 
3236  {
3237  return binding().where();
3238  }
3239 
3241  const exprt &where() const
3242  {
3243  return binding().where();
3244  }
3245 
3246  static void validate(const exprt &, validation_modet);
3247 };
3248 
3249 template <>
3250 inline bool can_cast_expr<let_exprt>(const exprt &base)
3251 {
3252  return base.id() == ID_let;
3253 }
3254 
3255 inline void validate_expr(const let_exprt &let_expr)
3256 {
3257  validate_operands(let_expr, 2, "Let must have two operands");
3258 }
3259 
3266 inline const let_exprt &to_let_expr(const exprt &expr)
3267 {
3268  PRECONDITION(expr.id()==ID_let);
3269  const let_exprt &ret = static_cast<const let_exprt &>(expr);
3270  validate_expr(ret);
3271  return ret;
3272 }
3273 
3276 {
3277  PRECONDITION(expr.id()==ID_let);
3278  let_exprt &ret = static_cast<let_exprt &>(expr);
3279  validate_expr(ret);
3280  return ret;
3281 }
3282 
3283 
3288 {
3289 public:
3290  cond_exprt(operandst _operands, typet _type)
3291  : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3292  {
3293  }
3294 
3298  void add_case(const exprt &condition, const exprt &value)
3299  {
3300  PRECONDITION(condition.type().id() == ID_bool);
3301  operands().reserve(operands().size() + 2);
3302  operands().push_back(condition);
3303  operands().push_back(value);
3304  }
3305 };
3306 
3307 template <>
3308 inline bool can_cast_expr<cond_exprt>(const exprt &base)
3309 {
3310  return base.id() == ID_cond;
3311 }
3312 
3313 inline void validate_expr(const cond_exprt &value)
3314 {
3316  value.operands().size() % 2 == 0, "cond must have even number of operands");
3317 }
3318 
3325 inline const cond_exprt &to_cond_expr(const exprt &expr)
3326 {
3327  PRECONDITION(expr.id() == ID_cond);
3328  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3329  validate_expr(ret);
3330  return ret;
3331 }
3332 
3335 {
3336  PRECONDITION(expr.id() == ID_cond);
3337  cond_exprt &ret = static_cast<cond_exprt &>(expr);
3338  validate_expr(ret);
3339  return ret;
3340 }
3341 
3351 {
3352 public:
3354  symbol_exprt arg,
3355  exprt body,
3356  array_typet _type)
3357  : binding_exprt(
3358  ID_array_comprehension,
3359  {std::move(arg)},
3360  std::move(body),
3361  std::move(_type))
3362  {
3363  }
3364 
3365  const array_typet &type() const
3366  {
3367  return static_cast<const array_typet &>(binary_exprt::type());
3368  }
3369 
3371  {
3372  return static_cast<array_typet &>(binary_exprt::type());
3373  }
3374 
3375  const symbol_exprt &arg() const
3376  {
3377  auto &variables = this->variables();
3378  PRECONDITION(variables.size() == 1);
3379  return variables[0];
3380  }
3381 
3383  {
3384  auto &variables = this->variables();
3385  PRECONDITION(variables.size() == 1);
3386  return variables[0];
3387  }
3388 
3389  const exprt &body() const
3390  {
3391  return where();
3392  }
3393 
3395  {
3396  return where();
3397  }
3398 };
3399 
3400 template <>
3402 {
3403  return base.id() == ID_array_comprehension;
3404 }
3405 
3406 inline void validate_expr(const array_comprehension_exprt &value)
3407 {
3408  validate_operands(value, 2, "'Array comprehension' must have two operands");
3409 }
3410 
3417 inline const array_comprehension_exprt &
3419 {
3420  PRECONDITION(expr.id() == ID_array_comprehension);
3421  const array_comprehension_exprt &ret =
3422  static_cast<const array_comprehension_exprt &>(expr);
3423  validate_expr(ret);
3424  return ret;
3425 }
3426 
3429 {
3430  PRECONDITION(expr.id() == ID_array_comprehension);
3432  static_cast<array_comprehension_exprt &>(expr);
3433  validate_expr(ret);
3434  return ret;
3435 }
3436 
3437 inline void validate_expr(const class class_method_descriptor_exprt &value);
3438 
3441 {
3442 public:
3458  typet _type,
3462  : nullary_exprt(ID_virtual_function, std::move(_type))
3463  {
3465  set(ID_component_name, std::move(mangled_method_name));
3466  set(ID_C_class, std::move(class_id));
3467  set(ID_C_base_name, std::move(base_method_name));
3468  set(ID_identifier, std::move(id));
3469  validate_expr(*this);
3470  }
3471 
3479  {
3480  return get(ID_component_name);
3481  }
3482 
3486  const irep_idt &class_id() const
3487  {
3488  return get(ID_C_class);
3489  }
3490 
3494  {
3495  return get(ID_C_base_name);
3496  }
3497 
3501  const irep_idt &get_identifier() const
3502  {
3503  return get(ID_identifier);
3504  }
3505 };
3506 
3507 inline void validate_expr(const class class_method_descriptor_exprt &value)
3508 {
3509  validate_operands(value, 0, "class method descriptor must not have operands");
3511  !value.mangled_method_name().empty(),
3512  "class method descriptor must have a mangled method name.");
3514  !value.class_id().empty(), "class method descriptor must have a class id.");
3516  !value.base_method_name().empty(),
3517  "class method descriptor must have a base method name.");
3519  value.get_identifier() == id2string(value.class_id()) + "." +
3520  id2string(value.mangled_method_name()),
3521  "class method descriptor must have an identifier in the expected format.");
3522 }
3523 
3530 inline const class_method_descriptor_exprt &
3532 {
3533  PRECONDITION(expr.id() == ID_virtual_function);
3534  const class_method_descriptor_exprt &ret =
3535  static_cast<const class_method_descriptor_exprt &>(expr);
3536  validate_expr(ret);
3537  return ret;
3538 }
3539 
3540 template <>
3542 {
3543  return base.id() == ID_virtual_function;
3544 }
3545 
3552 {
3553 public:
3555  : binary_exprt(
3556  std::move(symbol),
3557  ID_named_term,
3558  value, // not moved, for type
3559  value.type())
3560  {
3561  PRECONDITION(symbol.type() == type());
3562  }
3563 
3564  const symbol_exprt &symbol() const
3565  {
3566  return static_cast<const symbol_exprt &>(op0());
3567  }
3568 
3570  {
3571  return static_cast<symbol_exprt &>(op0());
3572  }
3573 
3574  const exprt &value() const
3575  {
3576  return op1();
3577  }
3578 
3580  {
3581  return op1();
3582  }
3583 };
3584 
3585 template <>
3586 inline bool can_cast_expr<named_term_exprt>(const exprt &base)
3587 {
3588  return base.id() == ID_named_term;
3589 }
3590 
3591 inline void validate_expr(const named_term_exprt &value)
3592 {
3593  validate_operands(value, 2, "'named term' must have two operands");
3594 }
3595 
3602 inline const named_term_exprt &to_named_term_expr(const exprt &expr)
3603 {
3604  PRECONDITION(expr.id() == ID_named_term);
3605  const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
3606  validate_expr(ret);
3607  return ret;
3608 }
3609 
3612 {
3613  PRECONDITION(expr.id() == ID_named_term);
3614  named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
3615  validate_expr(ret);
3616  return ret;
3617 }
3618 
3619 #endif // CPROVER_UTIL_STD_EXPR_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2423
index_exprt::array
const exprt & array() const
Definition: std_expr.h:1445
named_term_exprt::value
const exprt & value() const
Definition: std_expr.h:3574
exprt::op2
exprt & op2()
Definition: expr.h:131
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
if_exprt::if_exprt
if_exprt(exprt cond, const exprt &t, exprt f)
Definition: std_expr.h:2325
can_cast_expr< symbol_exprt >
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:206
to_array_comprehension_expr
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3418
irept::get_size_t
std::size_t get_size_t(const irep_idt &name) const
Definition: irep.cpp:68
to_vector_expr
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1692
can_cast_expr< union_exprt >
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1738
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2688
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2025
index_exprt::index
const exprt & index() const
Definition: std_expr.h:1455
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:361
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:856
binary_relation_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:714
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
let_exprt::let_exprt
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition: std_expr.h:3162
can_cast_expr< cond_exprt >
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition: std_expr.h:3308
member_exprt::member_exprt
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition: std_expr.h:2796
can_cast_expr< array_list_exprt >
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1644
can_cast_expr< mod_exprt >
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1201
binding_exprt::where
const exprt & where() const
Definition: std_expr.h:3088
if_exprt::if_exprt
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition: std_expr.h:2330
member_designatort::member_designatort
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:2559
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1146
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:623
constant_exprt::validate
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2966
can_cast_expr< index_designatort >
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:2523
to_ternary_expr
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
Definition: std_expr.h:98
class_method_descriptor_exprt::mangled_method_name
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition: std_expr.h:3478
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2086
array_list_exprt::array_list_exprt
array_list_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1621
can_cast_expr< named_term_exprt >
bool can_cast_expr< named_term_exprt >(const exprt &base)
Definition: std_expr.h:3586
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1603
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:241
and_exprt::and_exprt
and_exprt(exprt::operandst _operands)
Definition: std_expr.h:2094
can_cast_expr< complex_imag_exprt >
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:1980
nondet_symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:270
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1515
to_euclidean_mod_expr
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition: std_expr.h:1285
can_cast_expr< greater_than_or_equal_exprt >
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:782
binary_exprt::rhs
const exprt & rhs() const
Definition: std_expr.h:628
complex_exprt::real
const exprt & real() const
Definition: std_expr.h:1874
unary_minus_exprt::unary_minus_exprt
unary_minus_exprt(exprt _op, typet _type)
Definition: std_expr.h:425
to_type_expr
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition: std_expr.h:2925
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:870
can_cast_expr< not_exprt >
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:2287
typet
The type of an expression, extends irept.
Definition: type.h:28
update_exprt::old
exprt & old()
Definition: std_expr.h:2620
binary_relation_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:721
ternary_exprt
An expression with three operands.
Definition: std_expr.h:48
true_exprt::true_exprt
true_exprt()
Definition: std_expr.h:3010
mult_exprt::mult_exprt
mult_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1054
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1478
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2403
ternary_exprt::validate
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:83
euclidean_mod_exprt::divisor
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1262
can_cast_expr< sign_exprt >
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:548
mod_exprt::divisor
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1194
symbol_exprt::symbol_exprt
symbol_exprt(typet type)
Definition: std_expr.h:116
can_cast_expr< unary_exprt >
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:345
if_exprt::true_case
const exprt & true_case() const
Definition: std_expr.h:2355
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2322
member_designatort
Definition: std_expr.h:2556
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:132
div_exprt::div_exprt
div_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1099
validate_operands
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
array_list_exprt::type
array_typet & type()
Definition: std_expr.h:1631
xor_exprt
Boolean XOR.
Definition: std_expr.h:2241
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2454
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:949
binary_predicate_exprt::binary_predicate_exprt
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition: std_expr.h:678
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1925
invariant.h
let_exprt::symbol
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:3181
and_exprt
Boolean AND.
Definition: std_expr.h:2070
union_exprt
Union constructor from single element.
Definition: std_expr.h:1707
array_comprehension_exprt::type
array_typet & type()
Definition: std_expr.h:3370
disjunction
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:51
greater_than_or_equal_exprt::greater_than_or_equal_exprt
greater_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:775
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1543
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:193
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:946
less_than_or_equal_exprt::less_than_or_equal_exprt
less_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:817
can_cast_expr< xor_exprt >
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2251
equal_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1321
can_cast_expr< unary_minus_exprt >
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:437
abs_exprt::abs_exprt
abs_exprt(exprt _op)
Definition: std_expr.h:381
exprt
Base class for all expressions.
Definition: expr.h:55
class_method_descriptor_exprt::class_method_descriptor_exprt
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition: std_expr.h:3457
unary_exprt::op1
const exprt & op1() const =delete
to_complex_expr
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1907
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:613
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:313
array_exprt::array_exprt
array_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1565
index_exprt::index_exprt
index_exprt(exprt _array, exprt _index, typet _type)
Definition: std_expr.h:1428
decorated_symbol_exprt::clear_static_lifetime
void clear_static_lifetime()
Definition: std_expr.h:184
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:582
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1754
greater_than_exprt::greater_than_exprt
greater_than_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:754
array_of_exprt::type
array_typet & type()
Definition: std_expr.h:1510
member_designatort::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2565
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1076
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2194
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:538
can_cast_expr< binary_exprt >
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:644
update_exprt::designator
const exprt::operandst & designator() const
Definition: std_expr.h:2639
array_of_exprt::type
const array_typet & type() const
Definition: std_expr.h:1505
exprt::op0
exprt & op0()
Definition: expr.h:125
predicate_exprt::predicate_exprt
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:519
update_exprt::old
const exprt & old() const
Definition: std_expr.h:2625
let_exprt::validate
static void validate(const exprt &, validation_modet)
Definition: std_expr.cpp:143
array_comprehension_exprt::arg
const symbol_exprt & arg() const
Definition: std_expr.h:3375
cond_exprt::cond_exprt
cond_exprt(operandst _operands, typet _type)
Definition: std_expr.h:3290
constant_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.cpp:24
can_cast_expr< minus_exprt >
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:1015
to_array_list_expr
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1654
vector_typet
The vector type.
Definition: std_types.h:1007
bool_typet
The Boolean type.
Definition: std_types.h:35
index_designatort::index_designatort
index_designatort(exprt _index)
Definition: std_expr.h:2506
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1671
std::hash<::symbol_exprt >::operator()
size_t operator()(const ::symbol_exprt &sym)
Definition: std_expr.h:155
index_exprt::index_exprt
index_exprt(const exprt &_array, exprt _index)
Definition: std_expr.h:1416
named_term_exprt
Expression that introduces a new symbol that is equal to the operand.
Definition: std_expr.h:3551
type_exprt::type_exprt
type_exprt(typet type)
Definition: std_expr.h:2908
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1102
div_exprt
Division.
Definition: std_expr.h:1096
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:112
can_cast_expr< array_exprt >
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1592
validate_expr
void validate_expr(const symbol_exprt &value)
Definition: std_expr.h:211
empty_union_exprt::empty_union_exprt
empty_union_exprt(typet _type)
Definition: std_expr.h:1776
can_cast_expr< member_exprt >
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:2870
minus_exprt::minus_exprt
minus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1008
union_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:1726
equal_exprt
Equality.
Definition: std_expr.h:1305
array_comprehension_exprt::type
const array_typet & type() const
Definition: std_expr.h:3365
multi_ary_exprt::op2
exprt & op2()
Definition: std_expr.h:889
expanding_vectort
Definition: expanding_vector.h:16
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1031
mod_exprt::dividend
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1176
can_cast_expr< equal_exprt >
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1331
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:3041
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2360
array_list_exprt::add
void add(exprt index, exprt value)
add an index/value pair
Definition: std_expr.h:1637
can_cast_expr< implies_exprt >
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2143
notequal_exprt
Disequality.
Definition: std_expr.h:1364
binary_exprt::op3
const exprt & op3() const =delete
union_exprt::set_component_name
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1721
multi_ary_exprt::op3
exprt & op3()
Definition: std_expr.h:895
irept::get
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
array_exprt::with_source_location
array_exprt && with_source_location(const exprt &other) &&
Definition: std_expr.h:1585
nullary_exprt::op3
const exprt & op3() const =delete
to_unary_plus_expr
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:497
array_comprehension_exprt::arg
symbol_exprt & arg()
Definition: std_expr.h:3382
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1952
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:660
binding_exprt::variables
variablest & variables()
Definition: std_expr.h:3073
euclidean_mod_exprt
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition: std_expr.h:1235
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:3440
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1818
let_exprt::variables
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition: std_expr.h:3229
union_exprt::union_exprt
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition: std_expr.h:1710
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
complex_exprt::imag
exprt imag()
Definition: std_expr.h:1879
to_nondet_symbol_expr
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:293
let_exprt::variables
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:3223
class_method_descriptor_exprt::get_identifier
const irep_idt & get_identifier() const
A unique identifier of the combination of class and method overload to which this expression refers.
Definition: std_expr.h:3501
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
let_exprt::value
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:3197
or_exprt::or_exprt
or_exprt(exprt::operandst _operands)
Definition: std_expr.h:2202
nullary_exprt
An expression without operands.
Definition: std_expr.h:21
can_cast_expr< let_exprt >
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:3250
not_exprt::not_exprt
not_exprt(exprt _op)
Definition: std_expr.h:2280
can_cast_expr< and_exprt >
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2107
member_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:2826
array_exprt::type
const array_typet & type() const
Definition: std_expr.h:1570
with_exprt::where
const exprt & where() const
Definition: std_expr.h:2449
with_exprt::old
exprt & old()
Definition: std_expr.h:2434
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition: std_expr.h:954
greater_than_exprt
Binary greater than operator expression.
Definition: std_expr.h:751
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2078
to_cond_expr
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:3325
with_exprt::with_exprt
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition: std_expr.h:2426
xor_exprt::xor_exprt
xor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2244
notequal_exprt::notequal_exprt
notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1367
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
let_exprt::value
const exprt & value() const
convenience accessor for the value of a single binding
Definition: std_expr.h:3205
or_exprt
Boolean OR.
Definition: std_expr.h:2178
can_cast_expr< abs_exprt >
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:387
array_exprt::type
array_typet & type()
Definition: std_expr.h:1575
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1217
complex_real_exprt::complex_real_exprt
complex_real_exprt(const exprt &op)
Definition: std_expr.h:1928
member_exprt::struct_op
exprt & struct_op()
Definition: std_expr.h:2838
update_exprt::update_exprt
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition: std_expr.h:2610
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2073
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
class_method_descriptor_exprt::base_method_name
const irep_idt & base_method_name() const
The name of the method to which this expression is applied as would be seen in the source code.
Definition: std_expr.h:3493
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1077
array_comprehension_exprt::array_comprehension_exprt
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition: std_expr.h:3353
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
member_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2853
decorated_symbol_exprt::set_static_lifetime
void set_static_lifetime()
Definition: std_expr.h:179
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:79
symbol_exprt::symbol_exprt
symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:122
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2843
ternary_exprt::ternary_exprt
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition: std_expr.h:52
predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:516
multi_ary_exprt::op1
const exprt & op1() const
Definition: std_expr.h:907
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
can_cast_expr< plus_exprt >
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:970
to_empty_union_expr
const empty_union_exprt & to_empty_union_expr(const exprt &expr)
Cast an exprt to an empty_union_exprt.
Definition: std_expr.h:1800
update_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:2649
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2832
to_xor_expr
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2262
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:675
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:883
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
nullary_exprt::operands
operandst & operands()=delete
remove all operand methods
can_cast_expr< array_of_exprt >
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1527
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:142
nil_exprt
The NIL expression.
Definition: std_expr.h:3025
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1497
named_term_exprt::named_term_exprt
named_term_exprt(symbol_exprt symbol, exprt value)
Definition: std_expr.h:3554
nondet_symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:265
index_designatort::index
const exprt & index() const
Definition: std_expr.h:2511
conjunction
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:63
decorated_symbol_exprt::is_thread_local
bool is_thread_local() const
Definition: std_expr.h:189
std_types.h
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3266
can_cast_expr< notequal_exprt >
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1374
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:986
cond_exprt::add_case
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:3298
can_cast_expr< nil_exprt >
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition: std_expr.h:3035
array_comprehension_exprt::body
const exprt & body() const
Definition: std_expr.h:3389
greater_than_or_equal_exprt
Binary greater than or equal operator expression.
Definition: std_expr.h:772
member_exprt::compound
exprt & compound()
Definition: std_expr.h:2848
exprt::op1
exprt & op1()
Definition: expr.h:128
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1390
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1051
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:3054
with_exprt::old
const exprt & old() const
Definition: std_expr.h:2439
named_term_exprt::symbol
symbol_exprt & symbol()
Definition: std_expr.h:3569
index_exprt::index
exprt & index()
Definition: std_expr.h:1450
nil_exprt::nil_exprt
nil_exprt()
Definition: std_expr.h:3028
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:453
can_cast_expr< less_than_or_equal_exprt >
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:824
decorated_symbol_exprt::set_thread_local
void set_thread_local()
Definition: std_expr.h:194
mod_exprt::mod_exprt
mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1170
nondet_symbol_exprt::nondet_symbol_exprt
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition: std_expr.h:255
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:422
index_exprt::array
exprt & array()
Definition: std_expr.h:1440
ternary_exprt::op3
const exprt & op3() const =delete
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:222
binding_exprt::variables
const variablest & variables() const
Definition: std_expr.h:3078
member_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
Definition: std_expr.cpp:110
struct_exprt::struct_exprt
struct_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1821
validation_modet
validation_modet
Definition: validation_mode.h:12
irept::id
const irep_idt & id() const
Definition: irep.h:396
binary_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:595
let_exprt::binding
const binding_exprt & binding() const
Definition: std_expr.h:3175
empty_union_exprt
Union constructor to support unions without any member (a GCC/Clang feature).
Definition: std_expr.h:1773
binding_exprt
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:3051
can_cast_expr< div_exprt >
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1130
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:58
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1857
dstringt::empty
bool empty() const
Definition: dstring.h:88
abs_exprt
Absolute value.
Definition: std_expr.h:378
false_exprt
The Boolean constant false.
Definition: std_expr.h:3016
let_exprt::values
const operandst & values() const
Definition: std_expr.h:3217
vector_exprt::vector_exprt
vector_exprt(operandst _operands, vector_typet _type)
Definition: std_expr.h:1674
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:471
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition: std_expr.h:859
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:326
if_exprt::cond
const exprt & cond() const
Definition: std_expr.h:2345
euclidean_mod_exprt::dividend
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1244
update_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2661
let_exprt::let_exprt
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition: std_expr.h:3144
irept::set_size_t
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:87
div_exprt::dividend
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1111
can_cast_expr< less_than_exprt >
bool can_cast_expr< less_than_exprt >(const exprt &base)
Definition: std_expr.h:803
index_designatort
Definition: std_expr.h:2503
complex_exprt::imag
const exprt & imag() const
Definition: std_expr.h:1884
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1997
binary_predicate_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:683
array_list_exprt::type
const array_typet & type() const
Definition: std_expr.h:1626
div_exprt::divisor
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1117
binary_relation_exprt::binary_relation_exprt
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:709
unary_exprt::unary_exprt
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition: std_expr.h:321
minus_exprt
Binary minus.
Definition: std_expr.h:1005
div_exprt::dividend
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1105
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2486
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2607
nullary_exprt::op0
const exprt & op0() const =delete
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:2634
euclidean_mod_exprt::euclidean_mod_exprt
euclidean_mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1238
binary_exprt::validate
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:605
multi_ary_exprt::op0
const exprt & op0() const
Definition: std_expr.h:901
source_locationt
Definition: source_location.h:18
unary_plus_exprt::unary_plus_exprt
unary_plus_exprt(exprt op)
Definition: std_expr.h:474
irep_id_hash
dstring_hash irep_id_hash
Definition: irep.h:39
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2226
can_cast_expr< index_exprt >
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1462
unary_exprt::unary_exprt
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:316
if_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2370
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1716
sign_exprt::sign_exprt
sign_exprt(exprt _op)
Definition: std_expr.h:541
unary_minus_exprt::unary_minus_exprt
unary_minus_exprt(exprt _op)
Definition: std_expr.h:430
can_cast_expr< euclidean_mod_exprt >
bool can_cast_expr< euclidean_mod_exprt >(const exprt &base)
Definition: std_expr.h:1269
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2793
euclidean_mod_exprt::dividend
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1250
struct_union_typet::componentt
Definition: std_types.h:68
mod_exprt::divisor
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1188
can_cast_expr< binary_relation_exprt >
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:740
named_term_exprt::value
exprt & value()
Definition: std_expr.h:3579
equal_exprt::equal_exprt
equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1308
decorated_symbol_exprt
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition: std_expr.h:164
can_cast_expr< complex_real_exprt >
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:1935
type_exprt
An expression denoting a type.
Definition: std_expr.h:2905
can_cast_expr< array_comprehension_exprt >
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition: std_expr.h:3401
plus_exprt::plus_exprt
plus_exprt(operandst _operands, typet _type)
Definition: std_expr.h:963
cond_exprt
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:3287
equal_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1314
infinity_exprt::infinity_exprt
infinity_exprt(typet _type)
Definition: std_expr.h:3044
binding_exprt::binding_exprt
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition: std_expr.h:3057
array_typet
Arrays with given size.
Definition: std_types.h:762
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2350
binding_exprt::where
exprt & where()
Definition: std_expr.h:3083
can_cast_expr< or_exprt >
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:2215
array_exprt::with_source_location
array_exprt & with_source_location(const exprt &other) &
Definition: std_expr.h:1580
nullary_exprt::copy_to_operands
void copy_to_operands(const exprt &expr)=delete
decorated_symbol_exprt::decorated_symbol_exprt
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:169
to_sign_expr
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:564
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2303
can_cast_expr< class_method_descriptor_exprt >
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:3541
to_class_method_descriptor_expr
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
Definition: std_expr.h:3531
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:18
update_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2644
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2159
member_exprt::member_exprt
member_exprt(exprt op, const struct_typet::componentt &c)
Definition: std_expr.h:2806
unary_exprt::op2
const exprt & op2() const =delete
can_cast_expr< type_exprt >
bool can_cast_expr< type_exprt >(const exprt &base)
Definition: std_expr.h:2914
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2051
if_exprt::false_case
const exprt & false_case() const
Definition: std_expr.h:2365
less_than_exprt
Binary less than operator expression.
Definition: std_expr.h:793
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2340
binary_exprt::binary_exprt
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:590
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:706
typecast_exprt::typecast_exprt
typecast_exprt(exprt op, typet _type)
Definition: std_expr.h:2019
update_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2654
binding_exprt::instantiate
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition: std_expr.cpp:169
expr_cast.h
Templated functions to cast to specific exprt-derived classes.
nullary_exprt::op1
const exprt & op1() const =delete
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1970
can_cast_expr< nondet_symbol_exprt >
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:277
nullary_exprt::nullary_exprt
nullary_exprt(const irep_idt &_id, typet _type)
Definition: std_expr.h:24
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1347
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:162
binary_exprt::lhs
const exprt & lhs() const
Definition: std_expr.h:618
if_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2377
binary_exprt::binary_exprt
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:585
decorated_symbol_exprt::clear_thread_local
void clear_thread_local()
Definition: std_expr.h:199
ternary_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:73
euclidean_mod_exprt::divisor
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1256
array_comprehension_exprt::body
exprt & body()
Definition: std_expr.h:3394
class_method_descriptor_exprt::class_id
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
Definition: std_expr.h:3486
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2186
unary_exprt::op
exprt & op()
Definition: std_expr.h:331
multi_ary_exprt::op2
const exprt & op2() const
Definition: std_expr.h:913
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2886
can_cast_expr< typecast_exprt >
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2035
can_cast_expr< vector_exprt >
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1681
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2816
complex_exprt::complex_exprt
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition: std_expr.h:1860
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:20
implies_exprt
Boolean implication.
Definition: std_expr.h:2133
let_exprt::where
const exprt & where() const
convenience accessor for binding().where()
Definition: std_expr.h:3241
can_cast_expr< if_exprt >
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:2387
array_of_exprt::what
const exprt & what() const
Definition: std_expr.h:1520
struct_exprt::component
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:91
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1618
constant_exprt::constant_exprt
constant_exprt(const irep_idt &_value, typet _type)
Definition: std_expr.h:2944
can_cast_expr< constant_exprt >
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2976
exprt::operands
operandst & operands()
Definition: expr.h:94
decorated_symbol_exprt::is_static_lifetime
bool is_static_lifetime() const
Definition: std_expr.h:174
less_than_or_equal_exprt
Binary less than or equal operator expression.
Definition: std_expr.h:814
can_cast_expr< complex_exprt >
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:1891
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2181
let_exprt::values
operandst & values()
Definition: std_expr.h:3212
false_exprt::false_exprt
false_exprt()
Definition: std_expr.h:3019
to_named_term_expr
const named_term_exprt & to_named_term_expr(const exprt &expr)
Cast an exprt to a named_term_exprt.
Definition: std_expr.h:3602
nullary_exprt::op2
const exprt & op2() const =delete
irept::remove
void remove(const irep_idt &name)
Definition: irep.cpp:96
index_exprt
Array index operator.
Definition: std_expr.h:1409
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:216
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2016
can_cast_expr< unary_plus_exprt >
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:481
unary_predicate_exprt::unary_predicate_exprt
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition: std_expr.h:530
binary_predicate_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:690
complex_imag_exprt::complex_imag_exprt
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:1973
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3350
true_exprt
The Boolean constant true.
Definition: std_expr.h:3007
constant_exprt
A constant literal expression.
Definition: std_expr.h:2941
binary_exprt::op2
const exprt & op2() const =delete
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:877
unary_exprt::op3
const exprt & op3() const =delete
implies_exprt::implies_exprt
implies_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2136
index_designatort::index
exprt & index()
Definition: std_expr.h:2516
can_cast_expr< struct_exprt >
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1831
named_term_exprt::symbol
const symbol_exprt & symbol() const
Definition: std_expr.h:3564
can_cast_expr< greater_than_exprt >
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition: std_expr.h:761
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:932
to_binding_expr
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition: std_expr.h:3114
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3235
let_exprt::binding
binding_exprt & binding()
Definition: std_expr.h:3170
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:865
union_exprt::set_component_number
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1731
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:840
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:2955
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2950
let_exprt::symbol
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition: std_expr.h:3189
with_exprt::where
exprt & where()
Definition: std_expr.h:2444
array_of_exprt::array_of_exprt
array_of_exprt(exprt _what, array_typet _type)
Definition: std_expr.h:1500
to_member_designator
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:2588
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1562
can_cast_expr< with_exprt >
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:2466
member_exprt::set_component_name
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:2821
unary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:527
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:137
can_cast_expr< empty_union_exprt >
bool can_cast_expr< empty_union_exprt >(const exprt &base)
Definition: std_expr.h:1783
with_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:2459
less_than_exprt::less_than_exprt
less_than_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:796
mod_exprt::dividend
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1182
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
let_exprt
A let expression.
Definition: std_expr.h:3141
to_and_expr
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2118
div_exprt::divisor
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1123
complex_exprt::real
exprt real()
Definition: std_expr.h:1869
expr_protectedt
Base class for all expressions.
Definition: expr.h:323
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1842
validation_modet::INVARIANT
@ INVARIANT
can_cast_expr< member_designatort >
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:2572
to_abs_expr
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:403
mod_exprt
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1167
can_cast_expr< update_exprt >
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:2671
to_index_designator
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2539
can_cast_expr< mult_exprt >
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1061
not_exprt
Boolean negation.
Definition: std_expr.h:2277
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2992
nondet_symbol_exprt::nondet_symbol_exprt
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:246
multi_ary_exprt::op3
const exprt & op3() const
Definition: std_expr.h:919