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 
29  static void check(
30  const exprt &expr,
32  {
33  DATA_CHECK(
34  vm,
35  expr.operands().size() == 0,
36  "nullary expression must not have operands");
37  }
38 
39  static void validate(
40  const exprt &expr,
41  const namespacet &,
43  {
44  check(expr, vm);
45  }
46 
48  operandst &operands() = delete;
49  const operandst &operands() const = delete;
50 
51  const exprt &op0() const = delete;
52  exprt &op0() = delete;
53  const exprt &op1() const = delete;
54  exprt &op1() = delete;
55  const exprt &op2() const = delete;
56  exprt &op2() = delete;
57  const exprt &op3() const = delete;
58  exprt &op3() = delete;
59 
60  void copy_to_operands(const exprt &expr) = delete;
61  void copy_to_operands(const exprt &, const exprt &) = delete;
62  void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
63 };
64 
67 {
68 public:
69  // constructor
71  const irep_idt &_id,
72  exprt _op0,
73  exprt _op1,
74  exprt _op2,
75  typet _type)
77  _id,
78  std::move(_type),
79  {std::move(_op0), std::move(_op1), std::move(_op2)})
80  {
81  }
82 
83  // make op0 to op2 public
84  using exprt::op0;
85  using exprt::op1;
86  using exprt::op2;
87 
88  const exprt &op3() const = delete;
89  exprt &op3() = delete;
90 
91  static void check(
92  const exprt &expr,
94  {
95  DATA_CHECK(
96  vm,
97  expr.operands().size() == 3,
98  "ternary expression must have three operands");
99  }
100 
101  static void validate(
102  const exprt &expr,
103  const namespacet &,
105  {
106  check(expr, vm);
107  }
108 };
109 
116 inline const ternary_exprt &to_ternary_expr(const exprt &expr)
117 {
118  ternary_exprt::check(expr);
119  return static_cast<const ternary_exprt &>(expr);
120 }
121 
124 {
125  ternary_exprt::check(expr);
126  return static_cast<ternary_exprt &>(expr);
127 }
128 
131 {
132 public:
134  explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type))
135  {
136  }
137 
140  symbol_exprt(const irep_idt &identifier, typet type)
141  : nullary_exprt(ID_symbol, std::move(type))
142  {
143  set_identifier(identifier);
144  }
145 
150  static symbol_exprt typeless(const irep_idt &id)
151  {
152  return symbol_exprt(id, typet());
153  }
154 
155  void set_identifier(const irep_idt &identifier)
156  {
157  set(ID_identifier, identifier);
158  }
159 
160  const irep_idt &get_identifier() const
161  {
162  return get(ID_identifier);
163  }
164 
167  {
168  if(location.is_not_nil())
169  add_source_location() = std::move(location);
170  return *this;
171  }
172 
175  {
176  if(location.is_not_nil())
177  add_source_location() = std::move(location);
178  return std::move(*this);
179  }
180 
183  {
184  if(other.source_location().is_not_nil())
185  add_source_location() = other.source_location();
186  return *this;
187  }
188 
191  {
192  if(other.source_location().is_not_nil())
193  add_source_location() = other.source_location();
194  return std::move(*this);
195  }
196 };
197 
198 // NOLINTNEXTLINE(readability/namespace)
199 namespace std
200 {
201 template <>
202 // NOLINTNEXTLINE(readability/identifiers)
203 struct hash<::symbol_exprt>
204 {
205  size_t operator()(const ::symbol_exprt &sym)
206  {
207  return irep_id_hash()(sym.get_identifier());
208  }
209 };
210 } // namespace std
211 
215 {
216 public:
220  : symbol_exprt(identifier, std::move(type))
221  {
222  }
223 
224  bool is_static_lifetime() const
225  {
226  return get_bool(ID_C_static_lifetime);
227  }
228 
230  {
231  return set(ID_C_static_lifetime, true);
232  }
233 
235  {
236  remove(ID_C_static_lifetime);
237  }
238 
239  bool is_thread_local() const
240  {
241  return get_bool(ID_C_thread_local);
242  }
243 
245  {
246  return set(ID_C_thread_local, true);
247  }
248 
250  {
251  remove(ID_C_thread_local);
252  }
253 };
254 
255 template <>
256 inline bool can_cast_expr<symbol_exprt>(const exprt &base)
257 {
258  return base.id() == ID_symbol;
259 }
260 
261 inline void validate_expr(const symbol_exprt &value)
262 {
263  validate_operands(value, 0, "Symbols must not have operands");
264 }
265 
272 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
273 {
274  PRECONDITION(expr.id()==ID_symbol);
275  const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
276  validate_expr(ret);
277  return ret;
278 }
279 
282 {
283  PRECONDITION(expr.id()==ID_symbol);
284  symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
285  validate_expr(ret);
286  return ret;
287 }
288 
289 
292 {
293 public:
297  : nullary_exprt(ID_nondet_symbol, std::move(type))
298  {
299  set_identifier(identifier);
300  }
301 
306  irep_idt identifier,
307  typet type,
308  source_locationt location)
309  : nullary_exprt(ID_nondet_symbol, std::move(type))
310  {
311  set_identifier(std::move(identifier));
312  add_source_location() = std::move(location);
313  }
314 
315  void set_identifier(const irep_idt &identifier)
316  {
317  set(ID_identifier, identifier);
318  }
319 
320  const irep_idt &get_identifier() const
321  {
322  return get(ID_identifier);
323  }
324 };
325 
326 template <>
328 {
329  return base.id() == ID_nondet_symbol;
330 }
331 
332 inline void validate_expr(const nondet_symbol_exprt &value)
333 {
334  validate_operands(value, 0, "Symbols must not have operands");
335 }
336 
344 {
345  PRECONDITION(expr.id()==ID_nondet_symbol);
347  return static_cast<const nondet_symbol_exprt &>(expr);
348 }
349 
352 {
353  PRECONDITION(expr.id()==ID_symbol);
355  return static_cast<nondet_symbol_exprt &>(expr);
356 }
357 
358 
361 {
362 public:
363  unary_exprt(const irep_idt &_id, const exprt &_op)
364  : expr_protectedt(_id, _op.type(), {_op})
365  {
366  }
367 
368  unary_exprt(const irep_idt &_id, exprt _op, typet _type)
369  : expr_protectedt(_id, std::move(_type), {std::move(_op)})
370  {
371  }
372 
373  static void check(
374  const exprt &expr,
376  {
377  DATA_CHECK(
378  vm,
379  expr.operands().size() == 1,
380  "unary expression must have one operand");
381  }
382 
383  static void validate(
384  const exprt &expr,
385  const namespacet &,
387  {
388  check(expr, vm);
389  }
390 
391  const exprt &op() const
392  {
393  return op0();
394  }
395 
397  {
398  return op0();
399  }
400 
401  const exprt &op1() const = delete;
402  exprt &op1() = delete;
403  const exprt &op2() const = delete;
404  exprt &op2() = delete;
405  const exprt &op3() const = delete;
406  exprt &op3() = delete;
407 };
408 
409 template <>
410 inline bool can_cast_expr<unary_exprt>(const exprt &base)
411 {
412  return base.operands().size() == 1;
413 }
414 
415 inline void validate_expr(const unary_exprt &value)
416 {
417  unary_exprt::check(value);
418 }
419 
426 inline const unary_exprt &to_unary_expr(const exprt &expr)
427 {
428  unary_exprt::check(expr);
429  return static_cast<const unary_exprt &>(expr);
430 }
431 
434 {
435  unary_exprt::check(expr);
436  return static_cast<unary_exprt &>(expr);
437 }
438 
439 
441 class abs_exprt:public unary_exprt
442 {
443 public:
444  explicit abs_exprt(exprt _op) : unary_exprt(ID_abs, std::move(_op))
445  {
446  }
447 };
448 
449 template <>
450 inline bool can_cast_expr<abs_exprt>(const exprt &base)
451 {
452  return base.id() == ID_abs;
453 }
454 
455 inline void validate_expr(const abs_exprt &value)
456 {
457  validate_operands(value, 1, "Absolute value must have one operand");
458 }
459 
466 inline const abs_exprt &to_abs_expr(const exprt &expr)
467 {
468  PRECONDITION(expr.id()==ID_abs);
469  abs_exprt::check(expr);
470  return static_cast<const abs_exprt &>(expr);
471 }
472 
475 {
476  PRECONDITION(expr.id()==ID_abs);
477  abs_exprt::check(expr);
478  return static_cast<abs_exprt &>(expr);
479 }
480 
481 
484 {
485 public:
487  : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
488  {
489  }
490 
491  explicit unary_minus_exprt(exprt _op)
492  : unary_exprt(ID_unary_minus, std::move(_op))
493  {
494  }
495 };
496 
497 template <>
498 inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
499 {
500  return base.id() == ID_unary_minus;
501 }
502 
503 inline void validate_expr(const unary_minus_exprt &value)
504 {
505  validate_operands(value, 1, "Unary minus must have one operand");
506 }
507 
514 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
515 {
516  PRECONDITION(expr.id()==ID_unary_minus);
518  return static_cast<const unary_minus_exprt &>(expr);
519 }
520 
523 {
524  PRECONDITION(expr.id()==ID_unary_minus);
526  return static_cast<unary_minus_exprt &>(expr);
527 }
528 
531 {
532 public:
534  : unary_exprt(ID_unary_plus, std::move(op))
535  {
536  }
537 };
538 
539 template <>
540 inline bool can_cast_expr<unary_plus_exprt>(const exprt &base)
541 {
542  return base.id() == ID_unary_plus;
543 }
544 
545 inline void validate_expr(const unary_plus_exprt &value)
546 {
547  validate_operands(value, 1, "unary plus must have one operand");
548 }
549 
556 inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
557 {
558  PRECONDITION(expr.id() == ID_unary_plus);
560  return static_cast<const unary_plus_exprt &>(expr);
561 }
562 
565 {
566  PRECONDITION(expr.id() == ID_unary_plus);
568  return static_cast<unary_plus_exprt &>(expr);
569 }
570 
574 {
575 public:
576  explicit predicate_exprt(const irep_idt &_id)
577  : expr_protectedt(_id, bool_typet())
578  {
579  }
580 };
581 
585 {
586 public:
588  : unary_exprt(_id, std::move(_op), bool_typet())
589  {
590  }
591 };
592 
596 {
597 public:
598  explicit sign_exprt(exprt _op)
599  : unary_predicate_exprt(ID_sign, std::move(_op))
600  {
601  }
602 };
603 
604 template <>
605 inline bool can_cast_expr<sign_exprt>(const exprt &base)
606 {
607  return base.id() == ID_sign;
608 }
609 
610 inline void validate_expr(const sign_exprt &expr)
611 {
612  validate_operands(expr, 1, "sign expression must have one operand");
613 }
614 
621 inline const sign_exprt &to_sign_expr(const exprt &expr)
622 {
623  PRECONDITION(expr.id() == ID_sign);
624  sign_exprt::check(expr);
625  return static_cast<const sign_exprt &>(expr);
626 }
627 
630 {
631  PRECONDITION(expr.id() == ID_sign);
632  sign_exprt::check(expr);
633  return static_cast<sign_exprt &>(expr);
634 }
635 
638 {
639 public:
640  binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
641  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
642  {
643  }
644 
645  binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
646  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
647  {
648  }
649 
650  static void check(
651  const exprt &expr,
653  {
654  DATA_CHECK(
655  vm,
656  expr.operands().size() == 2,
657  "binary expression must have two operands");
658  }
659 
660  static void validate(
661  const exprt &expr,
662  const namespacet &,
664  {
665  check(expr, vm);
666  }
667 
669  {
670  return exprt::op0();
671  }
672 
673  const exprt &lhs() const
674  {
675  return exprt::op0();
676  }
677 
679  {
680  return exprt::op1();
681  }
682 
683  const exprt &rhs() const
684  {
685  return exprt::op1();
686  }
687 
688  // make op0 and op1 public
689  using exprt::op0;
690  using exprt::op1;
691 
692  const exprt &op2() const = delete;
693  exprt &op2() = delete;
694  const exprt &op3() const = delete;
695  exprt &op3() = delete;
696 };
697 
698 template <>
699 inline bool can_cast_expr<binary_exprt>(const exprt &base)
700 {
701  return base.operands().size() == 2;
702 }
703 
704 inline void validate_expr(const binary_exprt &value)
705 {
706  binary_exprt::check(value);
707 }
708 
715 inline const binary_exprt &to_binary_expr(const exprt &expr)
716 {
717  binary_exprt::check(expr);
718  return static_cast<const binary_exprt &>(expr);
719 }
720 
723 {
724  binary_exprt::check(expr);
725  return static_cast<binary_exprt &>(expr);
726 }
727 
731 {
732 public:
733  binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
734  : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
735  {
736  }
737 
738  static void check(
739  const exprt &expr,
741  {
742  binary_exprt::check(expr, vm);
743  }
744 
745  static void validate(
746  const exprt &expr,
747  const namespacet &ns,
749  {
750  binary_exprt::validate(expr, ns, vm);
751 
752  DATA_CHECK(
753  vm,
754  expr.is_boolean(),
755  "result of binary predicate expression should be of type bool");
756  }
757 };
758 
762 {
763 public:
764  binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
765  : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
766  {
767  }
768 
769  static void check(
770  const exprt &expr,
772  {
774  }
775 
776  static void validate(
777  const exprt &expr,
778  const namespacet &ns,
780  {
781  binary_predicate_exprt::validate(expr, ns, vm);
782 
783  // we now can safely assume that 'expr' is a binary predicate
784  const auto &expr_binary = static_cast<const binary_predicate_exprt &>(expr);
785 
786  // check that the types of the operands are the same
787  DATA_CHECK(
788  vm,
789  expr_binary.op0().type() == expr_binary.op1().type(),
790  "lhs and rhs of binary relation expression should have same type");
791  }
792 };
793 
794 template <>
796 {
797  return can_cast_expr<binary_exprt>(base);
798 }
799 
800 inline void validate_expr(const binary_relation_exprt &value)
801 {
803 }
804 
807 {
808 public:
810  : binary_relation_exprt{std::move(_lhs), ID_gt, std::move(_rhs)}
811  {
812  }
813 };
814 
815 template <>
816 inline bool can_cast_expr<greater_than_exprt>(const exprt &base)
817 {
818  return base.id() == ID_gt;
819 }
820 
821 inline void validate_expr(const greater_than_exprt &value)
822 {
824 }
825 
828 {
829 public:
831  : binary_relation_exprt{std::move(_lhs), ID_ge, std::move(_rhs)}
832  {
833  }
834 };
835 
836 template <>
838 {
839  return base.id() == ID_ge;
840 }
841 
843 {
845 }
846 
849 {
850 public:
852  : binary_relation_exprt{std::move(_lhs), ID_lt, std::move(_rhs)}
853  {
854  }
855 };
856 
857 template <>
858 inline bool can_cast_expr<less_than_exprt>(const exprt &base)
859 {
860  return base.id() == ID_lt;
861 }
862 
863 inline void validate_expr(const less_than_exprt &value)
864 {
866 }
867 
870 {
871 public:
873  : binary_relation_exprt{std::move(_lhs), ID_le, std::move(_rhs)}
874  {
875  }
876 };
877 
878 template <>
880 {
881  return base.id() == ID_le;
882 }
883 
884 inline void validate_expr(const less_than_or_equal_exprt &value)
885 {
887 }
888 
896 {
898  return static_cast<const binary_relation_exprt &>(expr);
899 }
900 
903 {
905  return static_cast<binary_relation_exprt &>(expr);
906 }
907 
908 
912 {
913 public:
914  multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
915  : expr_protectedt(_id, std::move(_type))
916  {
917  operands() = std::move(_operands);
918  }
919 
920  multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
921  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
922  {
923  }
924 
925  multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
926  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
927  {
928  }
929 
930  // In contrast to exprt::opX, the methods
931  // below check the size.
933  {
934  PRECONDITION(operands().size() >= 1);
935  return operands().front();
936  }
937 
939  {
940  PRECONDITION(operands().size() >= 2);
941  return operands()[1];
942  }
943 
945  {
946  PRECONDITION(operands().size() >= 3);
947  return operands()[2];
948  }
949 
951  {
952  PRECONDITION(operands().size() >= 4);
953  return operands()[3];
954  }
955 
956  const exprt &op0() const
957  {
958  PRECONDITION(operands().size() >= 1);
959  return operands().front();
960  }
961 
962  const exprt &op1() const
963  {
964  PRECONDITION(operands().size() >= 2);
965  return operands()[1];
966  }
967 
968  const exprt &op2() const
969  {
970  PRECONDITION(operands().size() >= 3);
971  return operands()[2];
972  }
973 
974  const exprt &op3() const
975  {
976  PRECONDITION(operands().size() >= 4);
977  return operands()[3];
978  }
979 };
980 
987 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
988 {
989  return static_cast<const multi_ary_exprt &>(expr);
990 }
991 
994 {
995  return static_cast<multi_ary_exprt &>(expr);
996 }
997 
998 
1002 {
1003 public:
1004  plus_exprt(exprt _lhs, exprt _rhs)
1005  : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
1006  {
1007  }
1008 
1009  plus_exprt(exprt _lhs, exprt _rhs, typet _type)
1010  : multi_ary_exprt(
1011  std::move(_lhs),
1012  ID_plus,
1013  std::move(_rhs),
1014  std::move(_type))
1015  {
1016  }
1017 
1018  plus_exprt(operandst _operands, typet _type)
1019  : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
1020  {
1021  }
1022 };
1023 
1024 template <>
1025 inline bool can_cast_expr<plus_exprt>(const exprt &base)
1026 {
1027  return base.id() == ID_plus;
1028 }
1029 
1030 inline void validate_expr(const plus_exprt &value)
1031 {
1032  validate_operands(value, 2, "Plus must have two or more operands", true);
1033 }
1034 
1041 inline const plus_exprt &to_plus_expr(const exprt &expr)
1042 {
1043  PRECONDITION(expr.id()==ID_plus);
1044  const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
1045  validate_expr(ret);
1046  return ret;
1047 }
1048 
1051 {
1052  PRECONDITION(expr.id()==ID_plus);
1053  plus_exprt &ret = static_cast<plus_exprt &>(expr);
1054  validate_expr(ret);
1055  return ret;
1056 }
1057 
1058 
1061 {
1062 public:
1064  : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
1065  {
1066  }
1067 };
1068 
1069 template <>
1070 inline bool can_cast_expr<minus_exprt>(const exprt &base)
1071 {
1072  return base.id() == ID_minus;
1073 }
1074 
1075 inline void validate_expr(const minus_exprt &value)
1076 {
1077  validate_operands(value, 2, "Minus must have two or more operands", true);
1078 }
1079 
1086 inline const minus_exprt &to_minus_expr(const exprt &expr)
1087 {
1088  PRECONDITION(expr.id()==ID_minus);
1089  const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
1090  validate_expr(ret);
1091  return ret;
1092 }
1093 
1096 {
1097  PRECONDITION(expr.id()==ID_minus);
1098  minus_exprt &ret = static_cast<minus_exprt &>(expr);
1099  validate_expr(ret);
1100  return ret;
1101 }
1102 
1103 
1107 {
1108 public:
1109  mult_exprt(exprt _lhs, exprt _rhs)
1110  : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
1111  {
1112  }
1113 
1115  : multi_ary_exprt(ID_mult, std::move(factors), std::move(type))
1116  {
1117  }
1118 };
1119 
1120 template <>
1121 inline bool can_cast_expr<mult_exprt>(const exprt &base)
1122 {
1123  return base.id() == ID_mult;
1124 }
1125 
1126 inline void validate_expr(const mult_exprt &value)
1127 {
1128  validate_operands(value, 2, "Multiply must have two or more operands", true);
1129 }
1130 
1137 inline const mult_exprt &to_mult_expr(const exprt &expr)
1138 {
1139  PRECONDITION(expr.id()==ID_mult);
1140  const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1141  validate_expr(ret);
1142  return ret;
1143 }
1144 
1147 {
1148  PRECONDITION(expr.id()==ID_mult);
1149  mult_exprt &ret = static_cast<mult_exprt &>(expr);
1150  validate_expr(ret);
1151  return ret;
1152 }
1153 
1154 
1157 {
1158 public:
1159  div_exprt(exprt _lhs, exprt _rhs)
1160  : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1161  {
1162  }
1163 
1166  {
1167  return op0();
1168  }
1169 
1171  const exprt &dividend() const
1172  {
1173  return op0();
1174  }
1175 
1178  {
1179  return op1();
1180  }
1181 
1183  const exprt &divisor() const
1184  {
1185  return op1();
1186  }
1187 };
1188 
1189 template <>
1190 inline bool can_cast_expr<div_exprt>(const exprt &base)
1191 {
1192  return base.id() == ID_div;
1193 }
1194 
1195 inline void validate_expr(const div_exprt &value)
1196 {
1197  validate_operands(value, 2, "Divide must have two operands");
1198 }
1199 
1206 inline const div_exprt &to_div_expr(const exprt &expr)
1207 {
1208  PRECONDITION(expr.id()==ID_div);
1209  const div_exprt &ret = static_cast<const div_exprt &>(expr);
1210  validate_expr(ret);
1211  return ret;
1212 }
1213 
1216 {
1217  PRECONDITION(expr.id()==ID_div);
1218  div_exprt &ret = static_cast<div_exprt &>(expr);
1219  validate_expr(ret);
1220  return ret;
1221 }
1222 
1228 {
1229 public:
1230  mod_exprt(exprt _lhs, exprt _rhs)
1231  : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1232  {
1233  }
1234 
1237  {
1238  return op0();
1239  }
1240 
1242  const exprt &dividend() const
1243  {
1244  return op0();
1245  }
1246 
1249  {
1250  return op1();
1251  }
1252 
1254  const exprt &divisor() const
1255  {
1256  return op1();
1257  }
1258 };
1259 
1260 template <>
1261 inline bool can_cast_expr<mod_exprt>(const exprt &base)
1262 {
1263  return base.id() == ID_mod;
1264 }
1265 
1266 inline void validate_expr(const mod_exprt &value)
1267 {
1268  validate_operands(value, 2, "Modulo must have two operands");
1269 }
1270 
1277 inline const mod_exprt &to_mod_expr(const exprt &expr)
1278 {
1279  PRECONDITION(expr.id()==ID_mod);
1280  const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1281  validate_expr(ret);
1282  return ret;
1283 }
1284 
1287 {
1288  PRECONDITION(expr.id()==ID_mod);
1289  mod_exprt &ret = static_cast<mod_exprt &>(expr);
1290  validate_expr(ret);
1291  return ret;
1292 }
1293 
1296 {
1297 public:
1299  : binary_exprt(std::move(_lhs), ID_euclidean_mod, std::move(_rhs))
1300  {
1301  }
1302 
1305  {
1306  return op0();
1307  }
1308 
1310  const exprt &dividend() const
1311  {
1312  return op0();
1313  }
1314 
1317  {
1318  return op1();
1319  }
1320 
1322  const exprt &divisor() const
1323  {
1324  return op1();
1325  }
1326 };
1327 
1328 template <>
1330 {
1331  return base.id() == ID_euclidean_mod;
1332 }
1333 
1334 inline void validate_expr(const euclidean_mod_exprt &value)
1335 {
1336  validate_operands(value, 2, "Modulo must have two operands");
1337 }
1338 
1346 {
1347  PRECONDITION(expr.id() == ID_euclidean_mod);
1348  const euclidean_mod_exprt &ret =
1349  static_cast<const euclidean_mod_exprt &>(expr);
1350  validate_expr(ret);
1351  return ret;
1352 }
1353 
1356 {
1357  PRECONDITION(expr.id() == ID_euclidean_mod);
1358  euclidean_mod_exprt &ret = static_cast<euclidean_mod_exprt &>(expr);
1359  validate_expr(ret);
1360  return ret;
1361 }
1362 
1363 
1366 {
1367 public:
1369  : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1370  {
1371  PRECONDITION(lhs().type() == rhs().type());
1372  }
1373 
1374  static void check(
1375  const exprt &expr,
1377  {
1378  binary_relation_exprt::check(expr, vm);
1379  }
1380 
1381  static void validate(
1382  const exprt &expr,
1383  const namespacet &ns,
1385  {
1386  binary_relation_exprt::validate(expr, ns, vm);
1387  }
1388 };
1389 
1390 template <>
1391 inline bool can_cast_expr<equal_exprt>(const exprt &base)
1392 {
1393  return base.id() == ID_equal;
1394 }
1395 
1396 inline void validate_expr(const equal_exprt &value)
1397 {
1398  equal_exprt::check(value);
1399 }
1400 
1407 inline const equal_exprt &to_equal_expr(const exprt &expr)
1408 {
1409  PRECONDITION(expr.id()==ID_equal);
1410  equal_exprt::check(expr);
1411  return static_cast<const equal_exprt &>(expr);
1412 }
1413 
1416 {
1417  PRECONDITION(expr.id()==ID_equal);
1418  equal_exprt::check(expr);
1419  return static_cast<equal_exprt &>(expr);
1420 }
1421 
1422 
1425 {
1426 public:
1428  : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1429  {
1430  }
1431 };
1432 
1433 template <>
1434 inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1435 {
1436  return base.id() == ID_notequal;
1437 }
1438 
1439 inline void validate_expr(const notequal_exprt &value)
1440 {
1441  validate_operands(value, 2, "Inequality must have two operands");
1442 }
1443 
1450 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1451 {
1452  PRECONDITION(expr.id()==ID_notequal);
1453  const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1454  validate_expr(ret);
1455  return ret;
1456 }
1457 
1460 {
1461  PRECONDITION(expr.id()==ID_notequal);
1462  notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1463  validate_expr(ret);
1464  return ret;
1465 }
1466 
1467 
1470 {
1471 public:
1472  // _array must have either index or vector type.
1473  // When _array has array_type, the type of _index
1474  // must be array_type.index_type().
1475  // This will eventually be enforced using a precondition.
1476  index_exprt(const exprt &_array, exprt _index)
1477  : binary_exprt(
1478  _array,
1479  ID_index,
1480  std::move(_index),
1481  to_type_with_subtype(_array.type()).subtype())
1482  {
1483  const auto &array_op_type = _array.type();
1484  PRECONDITION(
1485  array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1486  }
1487 
1488  index_exprt(exprt _array, exprt _index, typet _type)
1489  : binary_exprt(
1490  std::move(_array),
1491  ID_index,
1492  std::move(_index),
1493  std::move(_type))
1494  {
1495  const auto &array_op_type = array().type();
1496  PRECONDITION(
1497  array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
1498  }
1499 
1501  {
1502  return op0();
1503  }
1504 
1505  const exprt &array() const
1506  {
1507  return op0();
1508  }
1509 
1511  {
1512  return op1();
1513  }
1514 
1515  const exprt &index() const
1516  {
1517  return op1();
1518  }
1519 };
1520 
1521 template <>
1522 inline bool can_cast_expr<index_exprt>(const exprt &base)
1523 {
1524  return base.id() == ID_index;
1525 }
1526 
1527 inline void validate_expr(const index_exprt &value)
1528 {
1529  validate_operands(value, 2, "Array index must have two operands");
1530 }
1531 
1538 inline const index_exprt &to_index_expr(const exprt &expr)
1539 {
1540  PRECONDITION(expr.id()==ID_index);
1541  const index_exprt &ret = static_cast<const index_exprt &>(expr);
1542  validate_expr(ret);
1543  return ret;
1544 }
1545 
1548 {
1549  PRECONDITION(expr.id()==ID_index);
1550  index_exprt &ret = static_cast<index_exprt &>(expr);
1551  validate_expr(ret);
1552  return ret;
1553 }
1554 
1555 
1558 {
1559 public:
1560  explicit array_of_exprt(exprt _what, array_typet _type)
1561  : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1562  {
1563  }
1564 
1565  const array_typet &type() const
1566  {
1567  return static_cast<const array_typet &>(unary_exprt::type());
1568  }
1569 
1571  {
1572  return static_cast<array_typet &>(unary_exprt::type());
1573  }
1574 
1576  {
1577  return op0();
1578  }
1579 
1580  const exprt &what() const
1581  {
1582  return op0();
1583  }
1584 };
1585 
1586 template <>
1587 inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1588 {
1589  return base.id() == ID_array_of;
1590 }
1591 
1592 inline void validate_expr(const array_of_exprt &value)
1593 {
1594  validate_operands(value, 1, "'Array of' must have one operand");
1595 }
1596 
1603 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1604 {
1605  PRECONDITION(expr.id()==ID_array_of);
1606  array_of_exprt::check(expr);
1607  return static_cast<const array_of_exprt &>(expr);
1608 }
1609 
1612 {
1613  PRECONDITION(expr.id()==ID_array_of);
1614  array_of_exprt::check(expr);
1615  return static_cast<array_of_exprt &>(expr);
1616 }
1617 
1618 
1621 {
1622 public:
1624  : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1625  {
1626  }
1627 
1628  const array_typet &type() const
1629  {
1630  return static_cast<const array_typet &>(multi_ary_exprt::type());
1631  }
1632 
1634  {
1635  return static_cast<array_typet &>(multi_ary_exprt::type());
1636  }
1637 
1639  {
1640  if(other.source_location().is_not_nil())
1641  add_source_location() = other.source_location();
1642  return *this;
1643  }
1644 
1646  {
1647  if(other.source_location().is_not_nil())
1648  add_source_location() = other.source_location();
1649  return std::move(*this);
1650  }
1651 };
1652 
1653 template <>
1654 inline bool can_cast_expr<array_exprt>(const exprt &base)
1655 {
1656  return base.id() == ID_array;
1657 }
1658 
1665 inline const array_exprt &to_array_expr(const exprt &expr)
1666 {
1667  PRECONDITION(expr.id()==ID_array);
1668  return static_cast<const array_exprt &>(expr);
1669 }
1670 
1673 {
1674  PRECONDITION(expr.id()==ID_array);
1675  return static_cast<array_exprt &>(expr);
1676 }
1677 
1681 {
1682 public:
1684  : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1685  {
1686  }
1687 
1688  const array_typet &type() const
1689  {
1690  return static_cast<const array_typet &>(multi_ary_exprt::type());
1691  }
1692 
1694  {
1695  return static_cast<array_typet &>(multi_ary_exprt::type());
1696  }
1697 
1699  void add(exprt index, exprt value)
1700  {
1701  add_to_operands(std::move(index), std::move(value));
1702  }
1703 };
1704 
1705 template <>
1706 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1707 {
1708  return base.id() == ID_array_list;
1709 }
1710 
1711 inline void validate_expr(const array_list_exprt &value)
1712 {
1713  PRECONDITION(value.operands().size() % 2 == 0);
1714 }
1715 
1716 inline const array_list_exprt &to_array_list_expr(const exprt &expr)
1717 {
1719  auto &ret = static_cast<const array_list_exprt &>(expr);
1720  validate_expr(ret);
1721  return ret;
1722 }
1723 
1725 {
1727  auto &ret = static_cast<array_list_exprt &>(expr);
1728  validate_expr(ret);
1729  return ret;
1730 }
1731 
1734 {
1735 public:
1737  : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1738  {
1739  }
1740 };
1741 
1742 template <>
1743 inline bool can_cast_expr<vector_exprt>(const exprt &base)
1744 {
1745  return base.id() == ID_vector;
1746 }
1747 
1754 inline const vector_exprt &to_vector_expr(const exprt &expr)
1755 {
1756  PRECONDITION(expr.id()==ID_vector);
1757  return static_cast<const vector_exprt &>(expr);
1758 }
1759 
1762 {
1763  PRECONDITION(expr.id()==ID_vector);
1764  return static_cast<vector_exprt &>(expr);
1765 }
1766 
1767 
1770 {
1771 public:
1772  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1773  : unary_exprt(ID_union, std::move(_value), std::move(_type))
1774  {
1775  set_component_name(_component_name);
1776  }
1777 
1779  {
1780  return get(ID_component_name);
1781  }
1782 
1783  void set_component_name(const irep_idt &component_name)
1784  {
1785  set(ID_component_name, component_name);
1786  }
1787 
1788  std::size_t get_component_number() const
1789  {
1790  return get_size_t(ID_component_number);
1791  }
1792 
1793  void set_component_number(std::size_t component_number)
1794  {
1795  set_size_t(ID_component_number, component_number);
1796  }
1797 };
1798 
1799 template <>
1800 inline bool can_cast_expr<union_exprt>(const exprt &base)
1801 {
1802  return base.id() == ID_union;
1803 }
1804 
1805 inline void validate_expr(const union_exprt &value)
1806 {
1807  validate_operands(value, 1, "Union constructor must have one operand");
1808 }
1809 
1816 inline const union_exprt &to_union_expr(const exprt &expr)
1817 {
1818  PRECONDITION(expr.id()==ID_union);
1819  union_exprt::check(expr);
1820  return static_cast<const union_exprt &>(expr);
1821 }
1822 
1825 {
1826  PRECONDITION(expr.id()==ID_union);
1827  union_exprt::check(expr);
1828  return static_cast<union_exprt &>(expr);
1829 }
1830 
1834 {
1835 public:
1836  explicit empty_union_exprt(typet _type)
1837  : nullary_exprt(ID_empty_union, std::move(_type))
1838  {
1839  }
1840 };
1841 
1842 template <>
1843 inline bool can_cast_expr<empty_union_exprt>(const exprt &base)
1844 {
1845  return base.id() == ID_empty_union;
1846 }
1847 
1848 inline void validate_expr(const empty_union_exprt &value)
1849 {
1851  value, 0, "Empty-union constructor must not have any operand");
1852 }
1853 
1860 inline const empty_union_exprt &to_empty_union_expr(const exprt &expr)
1861 {
1862  PRECONDITION(expr.id() == ID_empty_union);
1864  return static_cast<const empty_union_exprt &>(expr);
1865 }
1866 
1869 {
1870  PRECONDITION(expr.id() == ID_empty_union);
1872  return static_cast<empty_union_exprt &>(expr);
1873 }
1874 
1877 {
1878 public:
1879  struct_exprt(operandst _operands, typet _type)
1880  : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1881  {
1882  }
1883 
1884  exprt &component(const irep_idt &name, const namespacet &ns);
1885  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1886 };
1887 
1888 template <>
1889 inline bool can_cast_expr<struct_exprt>(const exprt &base)
1890 {
1891  return base.id() == ID_struct;
1892 }
1893 
1900 inline const struct_exprt &to_struct_expr(const exprt &expr)
1901 {
1902  PRECONDITION(expr.id()==ID_struct);
1903  return static_cast<const struct_exprt &>(expr);
1904 }
1905 
1908 {
1909  PRECONDITION(expr.id()==ID_struct);
1910  return static_cast<struct_exprt &>(expr);
1911 }
1912 
1913 
1916 {
1917 public:
1919  : binary_exprt(
1920  std::move(_real),
1921  ID_complex,
1922  std::move(_imag),
1923  std::move(_type))
1924  {
1925  }
1926 
1928  {
1929  return op0();
1930  }
1931 
1932  const exprt &real() const
1933  {
1934  return op0();
1935  }
1936 
1938  {
1939  return op1();
1940  }
1941 
1942  const exprt &imag() const
1943  {
1944  return op1();
1945  }
1946 };
1947 
1948 template <>
1949 inline bool can_cast_expr<complex_exprt>(const exprt &base)
1950 {
1951  return base.id() == ID_complex;
1952 }
1953 
1954 inline void validate_expr(const complex_exprt &value)
1955 {
1956  validate_operands(value, 2, "Complex constructor must have two operands");
1957 }
1958 
1965 inline const complex_exprt &to_complex_expr(const exprt &expr)
1966 {
1967  PRECONDITION(expr.id()==ID_complex);
1968  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1969  validate_expr(ret);
1970  return ret;
1971 }
1972 
1975 {
1976  PRECONDITION(expr.id()==ID_complex);
1977  complex_exprt &ret = static_cast<complex_exprt &>(expr);
1978  validate_expr(ret);
1979  return ret;
1980 }
1981 
1984 {
1985 public:
1986  explicit complex_real_exprt(const exprt &op)
1987  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1988  {
1989  }
1990 };
1991 
1992 template <>
1994 {
1995  return base.id() == ID_complex_real;
1996 }
1997 
1998 inline void validate_expr(const complex_real_exprt &expr)
1999 {
2001  expr, 1, "real part retrieval operation must have one operand");
2002 }
2003 
2011 {
2012  PRECONDITION(expr.id() == ID_complex_real);
2014  return static_cast<const complex_real_exprt &>(expr);
2015 }
2016 
2019 {
2020  PRECONDITION(expr.id() == ID_complex_real);
2022  return static_cast<complex_real_exprt &>(expr);
2023 }
2024 
2027 {
2028 public:
2029  explicit complex_imag_exprt(const exprt &op)
2030  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
2031  {
2032  }
2033 };
2034 
2035 template <>
2037 {
2038  return base.id() == ID_complex_imag;
2039 }
2040 
2041 inline void validate_expr(const complex_imag_exprt &expr)
2042 {
2044  expr, 1, "imaginary part retrieval operation must have one operand");
2045 }
2046 
2054 {
2055  PRECONDITION(expr.id() == ID_complex_imag);
2056  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
2057  validate_expr(ret);
2058  return ret;
2059 }
2060 
2063 {
2064  PRECONDITION(expr.id() == ID_complex_imag);
2065  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
2066  validate_expr(ret);
2067  return ret;
2068 }
2069 
2070 
2073 {
2074 public:
2076  : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2077  {
2078  }
2079 
2080  // returns a typecast if the type doesn't already match
2081  static exprt conditional_cast(const exprt &expr, const typet &type)
2082  {
2083  if(expr.type() == type)
2084  return expr;
2085  else
2086  return typecast_exprt(expr, type);
2087  }
2088 };
2089 
2090 template <>
2091 inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2092 {
2093  return base.id() == ID_typecast;
2094 }
2095 
2096 inline void validate_expr(const typecast_exprt &value)
2097 {
2098  validate_operands(value, 1, "Typecast must have one operand");
2099 }
2100 
2107 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2108 {
2109  PRECONDITION(expr.id()==ID_typecast);
2110  typecast_exprt::check(expr);
2111  return static_cast<const typecast_exprt &>(expr);
2112 }
2113 
2116 {
2117  PRECONDITION(expr.id()==ID_typecast);
2118  typecast_exprt::check(expr);
2119  return static_cast<typecast_exprt &>(expr);
2120 }
2121 
2122 
2125 {
2126 public:
2128  : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2129  {
2130  }
2131 
2133  : multi_ary_exprt(
2134  ID_and,
2135  {std::move(op0), std::move(op1), std::move(op2)},
2136  bool_typet())
2137  {
2138  }
2139 
2141  : multi_ary_exprt(
2142  ID_and,
2143  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2144  bool_typet())
2145  {
2146  }
2147 
2148  explicit and_exprt(exprt::operandst _operands)
2149  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2150  {
2151  }
2152 };
2153 
2157 
2159 
2160 template <>
2161 inline bool can_cast_expr<and_exprt>(const exprt &base)
2162 {
2163  return base.id() == ID_and;
2164 }
2165 
2172 inline const and_exprt &to_and_expr(const exprt &expr)
2173 {
2174  PRECONDITION(expr.id()==ID_and);
2175  return static_cast<const and_exprt &>(expr);
2176 }
2177 
2180 {
2181  PRECONDITION(expr.id()==ID_and);
2182  return static_cast<and_exprt &>(expr);
2183 }
2184 
2185 
2188 {
2189 public:
2191  : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2192  {
2193  }
2194 };
2195 
2196 template <>
2197 inline bool can_cast_expr<implies_exprt>(const exprt &base)
2198 {
2199  return base.id() == ID_implies;
2200 }
2201 
2202 inline void validate_expr(const implies_exprt &value)
2203 {
2204  validate_operands(value, 2, "Implies must have two operands");
2205 }
2206 
2213 inline const implies_exprt &to_implies_expr(const exprt &expr)
2214 {
2215  PRECONDITION(expr.id()==ID_implies);
2216  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2217  validate_expr(ret);
2218  return ret;
2219 }
2220 
2223 {
2224  PRECONDITION(expr.id()==ID_implies);
2225  implies_exprt &ret = static_cast<implies_exprt &>(expr);
2226  validate_expr(ret);
2227  return ret;
2228 }
2229 
2230 
2233 {
2234 public:
2236  : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2237  {
2238  }
2239 
2241  : multi_ary_exprt(
2242  ID_or,
2243  {std::move(op0), std::move(op1), std::move(op2)},
2244  bool_typet())
2245  {
2246  }
2247 
2249  : multi_ary_exprt(
2250  ID_or,
2251  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2252  bool_typet())
2253  {
2254  }
2255 
2256  explicit or_exprt(exprt::operandst _operands)
2257  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2258  {
2259  }
2260 };
2261 
2265 
2267 
2268 template <>
2269 inline bool can_cast_expr<or_exprt>(const exprt &base)
2270 {
2271  return base.id() == ID_or;
2272 }
2273 
2280 inline const or_exprt &to_or_expr(const exprt &expr)
2281 {
2282  PRECONDITION(expr.id()==ID_or);
2283  return static_cast<const or_exprt &>(expr);
2284 }
2285 
2287 inline or_exprt &to_or_expr(exprt &expr)
2288 {
2289  PRECONDITION(expr.id()==ID_or);
2290  return static_cast<or_exprt &>(expr);
2291 }
2292 
2293 
2296 {
2297 public:
2298  xor_exprt(exprt _op0, exprt _op1)
2299  : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2300  {
2301  }
2302 
2303  explicit xor_exprt(exprt::operandst _operands)
2304  : multi_ary_exprt(ID_xor, std::move(_operands), bool_typet())
2305  {
2306  }
2307 };
2308 
2309 template <>
2310 inline bool can_cast_expr<xor_exprt>(const exprt &base)
2311 {
2312  return base.id() == ID_xor;
2313 }
2314 
2321 inline const xor_exprt &to_xor_expr(const exprt &expr)
2322 {
2323  PRECONDITION(expr.id()==ID_xor);
2324  return static_cast<const xor_exprt &>(expr);
2325 }
2326 
2329 {
2330  PRECONDITION(expr.id()==ID_xor);
2331  return static_cast<xor_exprt &>(expr);
2332 }
2333 
2334 
2337 {
2338 public:
2339  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2340  {
2341  PRECONDITION(as_const(*this).op().is_boolean());
2342  }
2343 };
2344 
2345 template <>
2346 inline bool can_cast_expr<not_exprt>(const exprt &base)
2347 {
2348  return base.id() == ID_not;
2349 }
2350 
2351 inline void validate_expr(const not_exprt &value)
2352 {
2353  validate_operands(value, 1, "Not must have one operand");
2354 }
2355 
2362 inline const not_exprt &to_not_expr(const exprt &expr)
2363 {
2364  PRECONDITION(expr.id()==ID_not);
2365  not_exprt::check(expr);
2366  return static_cast<const not_exprt &>(expr);
2367 }
2368 
2371 {
2372  PRECONDITION(expr.id()==ID_not);
2373  not_exprt::check(expr);
2374  return static_cast<not_exprt &>(expr);
2375 }
2376 
2377 
2379 class if_exprt : public ternary_exprt
2380 {
2381 public:
2383  : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2384  {
2385  }
2386 
2388  : ternary_exprt(
2389  ID_if,
2390  std::move(cond),
2391  std::move(t),
2392  std::move(f),
2393  std::move(type))
2394  {
2395  }
2396 
2398  {
2399  return op0();
2400  }
2401 
2402  const exprt &cond() const
2403  {
2404  return op0();
2405  }
2406 
2408  {
2409  return op1();
2410  }
2411 
2412  const exprt &true_case() const
2413  {
2414  return op1();
2415  }
2416 
2418  {
2419  return op2();
2420  }
2421 
2422  const exprt &false_case() const
2423  {
2424  return op2();
2425  }
2426 
2427  static void check(
2428  const exprt &expr,
2430  {
2431  ternary_exprt::check(expr, vm);
2432  }
2433 
2434  static void validate(
2435  const exprt &expr,
2436  const namespacet &ns,
2438  {
2439  ternary_exprt::validate(expr, ns, vm);
2440  }
2441 };
2442 
2443 template <>
2444 inline bool can_cast_expr<if_exprt>(const exprt &base)
2445 {
2446  return base.id() == ID_if;
2447 }
2448 
2449 inline void validate_expr(const if_exprt &value)
2450 {
2451  validate_operands(value, 3, "If-then-else must have three operands");
2452 }
2453 
2460 inline const if_exprt &to_if_expr(const exprt &expr)
2461 {
2462  PRECONDITION(expr.id()==ID_if);
2463  const if_exprt &ret = static_cast<const if_exprt &>(expr);
2464  validate_expr(ret);
2465  return ret;
2466 }
2467 
2469 inline if_exprt &to_if_expr(exprt &expr)
2470 {
2471  PRECONDITION(expr.id()==ID_if);
2472  if_exprt &ret = static_cast<if_exprt &>(expr);
2473  validate_expr(ret);
2474  return ret;
2475 }
2476 
2481 {
2482 public:
2483  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
2484  : expr_protectedt(
2485  ID_with,
2486  _old.type(),
2487  {_old, std::move(_where), std::move(_new_value)})
2488  {
2489  }
2490 
2492  {
2493  return op0();
2494  }
2495 
2496  const exprt &old() const
2497  {
2498  return op0();
2499  }
2500 
2502  {
2503  return op1();
2504  }
2505 
2506  const exprt &where() const
2507  {
2508  return op1();
2509  }
2510 
2512  {
2513  return op2();
2514  }
2515 
2516  const exprt &new_value() const
2517  {
2518  return op2();
2519  }
2520 };
2521 
2522 template <>
2523 inline bool can_cast_expr<with_exprt>(const exprt &base)
2524 {
2525  return base.id() == ID_with;
2526 }
2527 
2528 inline void validate_expr(const with_exprt &value)
2529 {
2531  value, 3, "array/structure update must have at least 3 operands", true);
2533  value.operands().size() % 2 == 1,
2534  "array/structure update must have an odd number of operands");
2535 }
2536 
2543 inline const with_exprt &to_with_expr(const exprt &expr)
2544 {
2545  PRECONDITION(expr.id()==ID_with);
2546  const with_exprt &ret = static_cast<const with_exprt &>(expr);
2547  validate_expr(ret);
2548  return ret;
2549 }
2550 
2553 {
2554  PRECONDITION(expr.id()==ID_with);
2555  with_exprt &ret = static_cast<with_exprt &>(expr);
2556  validate_expr(ret);
2557  return ret;
2558 }
2559 
2561 {
2562 public:
2563  explicit index_designatort(exprt _index)
2564  : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
2565  {
2566  }
2567 
2568  const exprt &index() const
2569  {
2570  return op0();
2571  }
2572 
2574  {
2575  return op0();
2576  }
2577 };
2578 
2579 template <>
2580 inline bool can_cast_expr<index_designatort>(const exprt &base)
2581 {
2582  return base.id() == ID_index_designator;
2583 }
2584 
2585 inline void validate_expr(const index_designatort &value)
2586 {
2587  validate_operands(value, 1, "Index designator must have one operand");
2588 }
2589 
2596 inline const index_designatort &to_index_designator(const exprt &expr)
2597 {
2598  PRECONDITION(expr.id()==ID_index_designator);
2599  const index_designatort &ret = static_cast<const index_designatort &>(expr);
2600  validate_expr(ret);
2601  return ret;
2602 }
2603 
2606 {
2607  PRECONDITION(expr.id()==ID_index_designator);
2608  index_designatort &ret = static_cast<index_designatort &>(expr);
2609  validate_expr(ret);
2610  return ret;
2611 }
2612 
2614 {
2615 public:
2616  explicit member_designatort(const irep_idt &_component_name)
2617  : expr_protectedt(ID_member_designator, typet())
2618  {
2619  set(ID_component_name, _component_name);
2620  }
2621 
2623  {
2624  return get(ID_component_name);
2625  }
2626 };
2627 
2628 template <>
2630 {
2631  return base.id() == ID_member_designator;
2632 }
2633 
2634 inline void validate_expr(const member_designatort &value)
2635 {
2636  validate_operands(value, 0, "Member designator must not have operands");
2637 }
2638 
2646 {
2647  PRECONDITION(expr.id()==ID_member_designator);
2648  const member_designatort &ret = static_cast<const member_designatort &>(expr);
2649  validate_expr(ret);
2650  return ret;
2651 }
2652 
2655 {
2656  PRECONDITION(expr.id()==ID_member_designator);
2657  member_designatort &ret = static_cast<member_designatort &>(expr);
2658  validate_expr(ret);
2659  return ret;
2660 }
2661 
2662 
2665 {
2666 public:
2667  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
2668  : ternary_exprt(
2669  ID_update,
2670  _old,
2671  std::move(_designator),
2672  std::move(_new_value),
2673  _old.type())
2674  {
2675  }
2676 
2678  {
2679  return op0();
2680  }
2681 
2682  const exprt &old() const
2683  {
2684  return op0();
2685  }
2686 
2687  // the designator operands are either
2688  // 1) member_designator or
2689  // 2) index_designator
2690  // as defined above
2692  {
2693  return op1().operands();
2694  }
2695 
2697  {
2698  return op1().operands();
2699  }
2700 
2702  {
2703  return op2();
2704  }
2705 
2706  const exprt &new_value() const
2707  {
2708  return op2();
2709  }
2710 
2712  with_exprt make_with_expr() const;
2713 
2714  static void check(
2715  const exprt &expr,
2717  {
2718  ternary_exprt::check(expr, vm);
2719  }
2720 
2721  static void validate(
2722  const exprt &expr,
2723  const namespacet &ns,
2725  {
2726  ternary_exprt::validate(expr, ns, vm);
2727  }
2728 };
2729 
2730 template <>
2731 inline bool can_cast_expr<update_exprt>(const exprt &base)
2732 {
2733  return base.id() == ID_update;
2734 }
2735 
2736 inline void validate_expr(const update_exprt &value)
2737 {
2739  value, 3, "Array/structure update must have three operands");
2740 }
2741 
2748 inline const update_exprt &to_update_expr(const exprt &expr)
2749 {
2750  PRECONDITION(expr.id()==ID_update);
2751  const update_exprt &ret = static_cast<const update_exprt &>(expr);
2752  validate_expr(ret);
2753  return ret;
2754 }
2755 
2758 {
2759  PRECONDITION(expr.id()==ID_update);
2760  update_exprt &ret = static_cast<update_exprt &>(expr);
2761  validate_expr(ret);
2762  return ret;
2763 }
2764 
2765 
2766 #if 0
2768 class array_update_exprt:public expr_protectedt
2769 {
2770 public:
2771  array_update_exprt(
2772  const exprt &_array,
2773  const exprt &_index,
2774  const exprt &_new_value):
2775  exprt(ID_array_update, _array.type())
2776  {
2777  add_to_operands(_array, _index, _new_value);
2778  }
2779 
2780  array_update_exprt():expr_protectedt(ID_array_update)
2781  {
2782  operands().resize(3);
2783  }
2784 
2785  exprt &array()
2786  {
2787  return op0();
2788  }
2789 
2790  const exprt &array() const
2791  {
2792  return op0();
2793  }
2794 
2795  exprt &index()
2796  {
2797  return op1();
2798  }
2799 
2800  const exprt &index() const
2801  {
2802  return op1();
2803  }
2804 
2805  exprt &new_value()
2806  {
2807  return op2();
2808  }
2809 
2810  const exprt &new_value() const
2811  {
2812  return op2();
2813  }
2814 };
2815 
2816 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
2817 {
2818  return base.id()==ID_array_update;
2819 }
2820 
2821 inline void validate_expr(const array_update_exprt &value)
2822 {
2823  validate_operands(value, 3, "Array update must have three operands");
2824 }
2825 
2832 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
2833 {
2834  PRECONDITION(expr.id()==ID_array_update);
2835  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
2836  validate_expr(ret);
2837  return ret;
2838 }
2839 
2841 inline array_update_exprt &to_array_update_expr(exprt &expr)
2842 {
2843  PRECONDITION(expr.id()==ID_array_update);
2844  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
2845  validate_expr(ret);
2846  return ret;
2847 }
2848 
2849 #endif
2850 
2851 
2854 {
2855 public:
2856  member_exprt(exprt op, const irep_idt &component_name, typet _type)
2857  : unary_exprt(ID_member, std::move(op), std::move(_type))
2858  {
2859  const auto &compound_type_id = compound().type().id();
2860  PRECONDITION(
2861  compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2862  compound_type_id == ID_struct || compound_type_id == ID_union);
2863  set_component_name(component_name);
2864  }
2865 
2867  : unary_exprt(ID_member, std::move(op), c.type())
2868  {
2869  const auto &compound_type_id = compound().type().id();
2870  PRECONDITION(
2871  compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
2872  compound_type_id == ID_struct || compound_type_id == ID_union);
2874  }
2875 
2877  {
2878  return get(ID_component_name);
2879  }
2880 
2881  void set_component_name(const irep_idt &component_name)
2882  {
2883  set(ID_component_name, component_name);
2884  }
2885 
2886  std::size_t get_component_number() const
2887  {
2888  return get_size_t(ID_component_number);
2889  }
2890 
2891  // will go away, use compound()
2892  const exprt &struct_op() const
2893  {
2894  return op0();
2895  }
2896 
2897  // will go away, use compound()
2899  {
2900  return op0();
2901  }
2902 
2903  const exprt &compound() const
2904  {
2905  return op0();
2906  }
2907 
2909  {
2910  return op0();
2911  }
2912 
2913  static void check(
2914  const exprt &expr,
2916  {
2917  DATA_CHECK(
2918  vm,
2919  expr.operands().size() == 1,
2920  "member expression must have one operand");
2921  }
2922 
2923  static void validate(
2924  const exprt &expr,
2925  const namespacet &ns,
2927 };
2928 
2929 template <>
2930 inline bool can_cast_expr<member_exprt>(const exprt &base)
2931 {
2932  return base.id() == ID_member;
2933 }
2934 
2935 inline void validate_expr(const member_exprt &value)
2936 {
2937  validate_operands(value, 1, "Extract member must have one operand");
2938 }
2939 
2946 inline const member_exprt &to_member_expr(const exprt &expr)
2947 {
2948  PRECONDITION(expr.id()==ID_member);
2949  member_exprt::check(expr);
2950  return static_cast<const member_exprt &>(expr);
2951 }
2952 
2955 {
2956  PRECONDITION(expr.id()==ID_member);
2957  member_exprt::check(expr);
2958  return static_cast<member_exprt &>(expr);
2959 }
2960 
2961 
2964 {
2965 public:
2966  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
2967  {
2968  }
2969 };
2970 
2971 template <>
2972 inline bool can_cast_expr<type_exprt>(const exprt &base)
2973 {
2974  return base.id() == ID_type;
2975 }
2976 
2983 inline const type_exprt &to_type_expr(const exprt &expr)
2984 {
2986  type_exprt::check(expr);
2987  return static_cast<const type_exprt &>(expr);
2988 }
2989 
2992 {
2994  type_exprt::check(expr);
2995  return static_cast<type_exprt &>(expr);
2996 }
2997 
3000 {
3001 public:
3002  constant_exprt(const irep_idt &_value, typet _type)
3003  : nullary_exprt(ID_constant, std::move(_type))
3004  {
3005  set_value(_value);
3006  }
3007 
3008  const irep_idt &get_value() const
3009  {
3010  return get(ID_value);
3011  }
3012 
3013  void set_value(const irep_idt &value)
3014  {
3015  set(ID_value, value);
3016  }
3017 
3018  bool value_is_zero_string() const;
3019 
3023  bool is_null_pointer() const;
3024 
3025  static void check(
3026  const exprt &expr,
3028 
3029  static void validate(
3030  const exprt &expr,
3031  const namespacet &,
3033  {
3034  check(expr, vm);
3035  }
3036 };
3037 
3038 template <>
3039 inline bool can_cast_expr<constant_exprt>(const exprt &base)
3040 {
3041  return base.is_constant();
3042 }
3043 
3044 inline void validate_expr(const constant_exprt &value)
3045 {
3046  validate_operands(value, 0, "Constants must not have operands");
3047 }
3048 
3055 inline const constant_exprt &to_constant_expr(const exprt &expr)
3056 {
3057  PRECONDITION(expr.is_constant());
3058  constant_exprt::check(expr);
3059  return static_cast<const constant_exprt &>(expr);
3060 }
3061 
3064 {
3065  PRECONDITION(expr.is_constant());
3066  constant_exprt::check(expr);
3067  return static_cast<constant_exprt &>(expr);
3068 }
3069 
3070 
3073 {
3074 public:
3076  {
3077  }
3078 };
3079 
3082 {
3083 public:
3085  {
3086  }
3087 };
3088 
3090 class nil_exprt : public nullary_exprt
3091 {
3092 public:
3094  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
3095  {
3096  }
3097 };
3098 
3099 template <>
3100 inline bool can_cast_expr<nil_exprt>(const exprt &base)
3101 {
3102  return base.id() == ID_nil;
3103 }
3104 
3107 {
3108 public:
3109  explicit infinity_exprt(typet _type)
3110  : nullary_exprt(ID_infinity, std::move(_type))
3111  {
3112  }
3113 };
3114 
3117 {
3118 public:
3119  using variablest = std::vector<symbol_exprt>;
3120 
3123  irep_idt _id,
3124  const variablest &_variables,
3125  exprt _where,
3126  typet _type)
3127  : binary_exprt(
3129  ID_tuple,
3130  (const operandst &)_variables,
3131  typet(ID_tuple)),
3132  _id,
3133  std::move(_where),
3134  std::move(_type))
3135  {
3136  }
3137 
3139  {
3140  return (variablest &)to_multi_ary_expr(op0()).operands();
3141  }
3142 
3143  const variablest &variables() const
3144  {
3145  return (variablest &)to_multi_ary_expr(op0()).operands();
3146  }
3147 
3149  {
3150  return op1();
3151  }
3152 
3153  const exprt &where() const
3154  {
3155  return op1();
3156  }
3157 
3160  exprt instantiate(const exprt::operandst &) const;
3161 
3164  exprt instantiate(const variablest &) const;
3165 };
3166 
3167 template <>
3168 inline bool can_cast_expr<binding_exprt>(const exprt &base)
3169 {
3170  return base.id() == ID_forall || base.id() == ID_exists ||
3171  base.id() == ID_lambda || base.id() == ID_array_comprehension;
3172 }
3173 
3174 inline void validate_expr(const binding_exprt &binding_expr)
3175 {
3177  binding_expr, 2, "Binding expressions must have two operands");
3178 }
3179 
3186 inline const binding_exprt &to_binding_expr(const exprt &expr)
3187 {
3188  PRECONDITION(
3189  expr.id() == ID_forall || expr.id() == ID_exists ||
3190  expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3191  const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
3192  validate_expr(ret);
3193  return ret;
3194 }
3195 
3203 {
3204  PRECONDITION(
3205  expr.id() == ID_forall || expr.id() == ID_exists ||
3206  expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
3207  binding_exprt &ret = static_cast<binding_exprt &>(expr);
3208  validate_expr(ret);
3209  return ret;
3210 }
3211 
3213 class let_exprt : public binary_exprt
3214 {
3215 public:
3218  operandst values,
3219  const exprt &where)
3220  : binary_exprt(
3221  binding_exprt(
3222  ID_let_binding,
3223  std::move(variables),
3224  where,
3225  where.type()),
3226  ID_let,
3227  multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
3228  where.type())
3229  {
3230  PRECONDITION(this->variables().size() == this->values().size());
3231  }
3232 
3235  : let_exprt(
3236  binding_exprt::variablest{std::move(symbol)},
3237  operandst{std::move(value)},
3238  where)
3239  {
3240  }
3241 
3243  {
3244  return static_cast<binding_exprt &>(op0());
3245  }
3246 
3247  const binding_exprt &binding() const
3248  {
3249  return static_cast<const binding_exprt &>(op0());
3250  }
3251 
3254  {
3255  auto &variables = binding().variables();
3256  PRECONDITION(variables.size() == 1);
3257  return variables.front();
3258  }
3259 
3261  const symbol_exprt &symbol() const
3262  {
3263  const auto &variables = binding().variables();
3264  PRECONDITION(variables.size() == 1);
3265  return variables.front();
3266  }
3267 
3270  {
3271  auto &values = this->values();
3272  PRECONDITION(values.size() == 1);
3273  return values.front();
3274  }
3275 
3277  const exprt &value() const
3278  {
3279  const auto &values = this->values();
3280  PRECONDITION(values.size() == 1);
3281  return values.front();
3282  }
3283 
3285  {
3286  return static_cast<multi_ary_exprt &>(op1()).operands();
3287  }
3288 
3289  const operandst &values() const
3290  {
3291  return static_cast<const multi_ary_exprt &>(op1()).operands();
3292  }
3293 
3296  {
3297  return binding().variables();
3298  }
3299 
3302  {
3303  return binding().variables();
3304  }
3305 
3308  {
3309  return binding().where();
3310  }
3311 
3313  const exprt &where() const
3314  {
3315  return binding().where();
3316  }
3317 
3318  static void validate(const exprt &, validation_modet);
3319 };
3320 
3321 template <>
3322 inline bool can_cast_expr<let_exprt>(const exprt &base)
3323 {
3324  return base.id() == ID_let;
3325 }
3326 
3327 inline void validate_expr(const let_exprt &let_expr)
3328 {
3329  validate_operands(let_expr, 2, "Let must have two operands");
3330 }
3331 
3338 inline const let_exprt &to_let_expr(const exprt &expr)
3339 {
3340  PRECONDITION(expr.id()==ID_let);
3341  const let_exprt &ret = static_cast<const let_exprt &>(expr);
3342  validate_expr(ret);
3343  return ret;
3344 }
3345 
3348 {
3349  PRECONDITION(expr.id()==ID_let);
3350  let_exprt &ret = static_cast<let_exprt &>(expr);
3351  validate_expr(ret);
3352  return ret;
3353 }
3354 
3355 
3360 {
3361 public:
3362  cond_exprt(operandst _operands, typet _type)
3363  : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
3364  {
3365  }
3366 
3370  void add_case(const exprt &condition, const exprt &value)
3371  {
3372  PRECONDITION(condition.is_boolean());
3373  operands().reserve(operands().size() + 2);
3374  operands().push_back(condition);
3375  operands().push_back(value);
3376  }
3377 };
3378 
3379 template <>
3380 inline bool can_cast_expr<cond_exprt>(const exprt &base)
3381 {
3382  return base.id() == ID_cond;
3383 }
3384 
3385 inline void validate_expr(const cond_exprt &value)
3386 {
3388  value.operands().size() % 2 == 0, "cond must have even number of operands");
3389 }
3390 
3397 inline const cond_exprt &to_cond_expr(const exprt &expr)
3398 {
3399  PRECONDITION(expr.id() == ID_cond);
3400  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
3401  validate_expr(ret);
3402  return ret;
3403 }
3404 
3407 {
3408  PRECONDITION(expr.id() == ID_cond);
3409  cond_exprt &ret = static_cast<cond_exprt &>(expr);
3410  validate_expr(ret);
3411  return ret;
3412 }
3413 
3423 {
3424 public:
3426  symbol_exprt arg,
3427  exprt body,
3428  array_typet _type)
3429  : binding_exprt(
3430  ID_array_comprehension,
3431  {std::move(arg)},
3432  std::move(body),
3433  std::move(_type))
3434  {
3435  }
3436 
3437  const array_typet &type() const
3438  {
3439  return static_cast<const array_typet &>(binary_exprt::type());
3440  }
3441 
3443  {
3444  return static_cast<array_typet &>(binary_exprt::type());
3445  }
3446 
3447  const symbol_exprt &arg() const
3448  {
3449  auto &variables = this->variables();
3450  PRECONDITION(variables.size() == 1);
3451  return variables[0];
3452  }
3453 
3455  {
3456  auto &variables = this->variables();
3457  PRECONDITION(variables.size() == 1);
3458  return variables[0];
3459  }
3460 
3461  const exprt &body() const
3462  {
3463  return where();
3464  }
3465 
3467  {
3468  return where();
3469  }
3470 };
3471 
3472 template <>
3474 {
3475  return base.id() == ID_array_comprehension;
3476 }
3477 
3478 inline void validate_expr(const array_comprehension_exprt &value)
3479 {
3480  validate_operands(value, 2, "'Array comprehension' must have two operands");
3481 }
3482 
3489 inline const array_comprehension_exprt &
3491 {
3492  PRECONDITION(expr.id() == ID_array_comprehension);
3493  const array_comprehension_exprt &ret =
3494  static_cast<const array_comprehension_exprt &>(expr);
3495  validate_expr(ret);
3496  return ret;
3497 }
3498 
3501 {
3502  PRECONDITION(expr.id() == ID_array_comprehension);
3504  static_cast<array_comprehension_exprt &>(expr);
3505  validate_expr(ret);
3506  return ret;
3507 }
3508 
3509 inline void validate_expr(const class class_method_descriptor_exprt &value);
3510 
3513 {
3514 public:
3530  typet _type,
3534  : nullary_exprt(ID_virtual_function, std::move(_type))
3535  {
3537  set(ID_component_name, std::move(mangled_method_name));
3538  set(ID_C_class, std::move(class_id));
3539  set(ID_C_base_name, std::move(base_method_name));
3540  set(ID_identifier, std::move(id));
3541  validate_expr(*this);
3542  }
3543 
3551  {
3552  return get(ID_component_name);
3553  }
3554 
3558  const irep_idt &class_id() const
3559  {
3560  return get(ID_C_class);
3561  }
3562 
3566  {
3567  return get(ID_C_base_name);
3568  }
3569 
3573  const irep_idt &get_identifier() const
3574  {
3575  return get(ID_identifier);
3576  }
3577 };
3578 
3579 inline void validate_expr(const class class_method_descriptor_exprt &value)
3580 {
3581  validate_operands(value, 0, "class method descriptor must not have operands");
3583  !value.mangled_method_name().empty(),
3584  "class method descriptor must have a mangled method name.");
3586  !value.class_id().empty(), "class method descriptor must have a class id.");
3588  !value.base_method_name().empty(),
3589  "class method descriptor must have a base method name.");
3591  value.get_identifier() == id2string(value.class_id()) + "." +
3592  id2string(value.mangled_method_name()),
3593  "class method descriptor must have an identifier in the expected format.");
3594 }
3595 
3602 inline const class_method_descriptor_exprt &
3604 {
3605  PRECONDITION(expr.id() == ID_virtual_function);
3607  return static_cast<const class_method_descriptor_exprt &>(expr);
3608 }
3609 
3610 template <>
3612 {
3613  return base.id() == ID_virtual_function;
3614 }
3615 
3622 {
3623 public:
3625  : binary_exprt(
3626  std::move(symbol),
3627  ID_named_term,
3628  value, // not moved, for type
3629  value.type())
3630  {
3631  PRECONDITION(symbol.type() == type());
3632  }
3633 
3634  const symbol_exprt &symbol() const
3635  {
3636  return static_cast<const symbol_exprt &>(op0());
3637  }
3638 
3640  {
3641  return static_cast<symbol_exprt &>(op0());
3642  }
3643 
3644  const exprt &value() const
3645  {
3646  return op1();
3647  }
3648 
3650  {
3651  return op1();
3652  }
3653 };
3654 
3655 template <>
3656 inline bool can_cast_expr<named_term_exprt>(const exprt &base)
3657 {
3658  return base.id() == ID_named_term;
3659 }
3660 
3661 inline void validate_expr(const named_term_exprt &value)
3662 {
3663  validate_operands(value, 2, "'named term' must have two operands");
3664 }
3665 
3672 inline const named_term_exprt &to_named_term_expr(const exprt &expr)
3673 {
3674  PRECONDITION(expr.id() == ID_named_term);
3675  const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
3676  validate_expr(ret);
3677  return ret;
3678 }
3679 
3682 {
3683  PRECONDITION(expr.id() == ID_named_term);
3684  named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
3685  validate_expr(ret);
3686  return ret;
3687 }
3688 
3689 #endif // CPROVER_UTIL_STD_EXPR_H
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
Absolute value.
Definition: std_expr.h:442
abs_exprt(exprt _op)
Definition: std_expr.h:444
Boolean AND.
Definition: std_expr.h:2125
and_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2132
and_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2127
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2140
and_exprt(exprt::operandst _operands)
Definition: std_expr.h:2148
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3423
symbol_exprt & arg()
Definition: std_expr.h:3454
array_typet & type()
Definition: std_expr.h:3442
const exprt & body() const
Definition: std_expr.h:3461
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition: std_expr.h:3425
const array_typet & type() const
Definition: std_expr.h:3437
const symbol_exprt & arg() const
Definition: std_expr.h:3447
Array constructor from list of elements.
Definition: std_expr.h:1621
array_exprt && with_source_location(const exprt &other) &&
Definition: std_expr.h:1645
array_exprt & with_source_location(const exprt &other) &
Definition: std_expr.h:1638
array_typet & type()
Definition: std_expr.h:1633
array_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1623
const array_typet & type() const
Definition: std_expr.h:1628
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1681
void add(exprt index, exprt value)
add an index/value pair
Definition: std_expr.h:1699
const array_typet & type() const
Definition: std_expr.h:1688
array_list_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1683
array_typet & type()
Definition: std_expr.h:1693
Array constructor from single element.
Definition: std_expr.h:1558
const exprt & what() const
Definition: std_expr.h:1580
exprt & what()
Definition: std_expr.h:1575
array_of_exprt(exprt _what, array_typet _type)
Definition: std_expr.h:1560
array_typet & type()
Definition: std_expr.h:1570
const array_typet & type() const
Definition: std_expr.h:1565
Arrays with given size.
Definition: std_types.h:807
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op2()=delete
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:640
exprt & op1()
Definition: expr.h:136
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:660
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:650
const exprt & lhs() const
Definition: std_expr.h:673
exprt & lhs()
Definition: std_expr.h:668
const exprt & rhs() const
Definition: std_expr.h:683
const exprt & op2() const =delete
exprt & op0()
Definition: expr.h:133
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:645
exprt & op3()=delete
exprt & rhs()
Definition: std_expr.h:678
const exprt & op3() const =delete
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:731
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:738
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition: std_expr.h:733
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:745
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:764
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:769
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:776
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:3117
exprt & where()
Definition: std_expr.h:3148
const exprt & where() const
Definition: std_expr.h:3153
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition: std_expr.h:3122
const variablest & variables() const
Definition: std_expr.h:3143
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition: std_expr.cpp:225
variablest & variables()
Definition: std_expr.h:3138
std::vector< symbol_exprt > variablest
Definition: std_expr.h:3119
The Boolean type.
Definition: std_types.h:36
An expression describing a method on a class.
Definition: std_expr.h:3513
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:3573
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:3558
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition: std_expr.h:3529
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:3565
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition: std_expr.h:3550
Complex constructor from a pair of numbers.
Definition: std_expr.h:1916
const exprt & imag() const
Definition: std_expr.h:1942
const exprt & real() const
Definition: std_expr.h:1932
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition: std_expr.h:1918
exprt real()
Definition: std_expr.h:1927
exprt imag()
Definition: std_expr.h:1937
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2027
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:2029
Real part of the expression describing a complex number.
Definition: std_expr.h:1984
complex_real_exprt(const exprt &op)
Definition: std_expr.h:1986
Complex numbers made of pair of given subtype.
Definition: std_types.h:1130
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:3360
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:3370
cond_exprt(operandst _operands, typet _type)
Definition: std_expr.h:3362
A constant literal expression.
Definition: std_expr.h:3000
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3029
const irep_idt & get_value() const
Definition: std_expr.h:3008
bool value_is_zero_string() const
Definition: std_expr.cpp:19
constant_exprt(const irep_idt &_value, typet _type)
Definition: std_expr.h:3002
void set_value(const irep_idt &value)
Definition: std_expr.h:3013
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition: std_expr.cpp:25
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.cpp:41
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition: std_expr.h:215
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:219
void set_static_lifetime()
Definition: std_expr.h:229
bool is_static_lifetime() const
Definition: std_expr.h:224
bool is_thread_local() const
Definition: std_expr.h:239
void clear_static_lifetime()
Definition: std_expr.h:234
Division.
Definition: std_expr.h:1157
div_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1159
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1183
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1165
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1177
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1171
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Union constructor to support unions without any member (a GCC/Clang feature).
Definition: std_expr.h:1834
empty_union_exprt(typet _type)
Definition: std_expr.h:1836
Equality.
Definition: std_expr.h:1366
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1374
equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1368
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1381
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition: std_expr.h:1296
euclidean_mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1298
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1316
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1304
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1322
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1310
Base class for all expressions.
Definition: expr.h:344
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
exprt & op1()
Definition: expr.h:136
source_locationt & add_source_location()
Definition: expr.h:236
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
exprt & op2()
Definition: expr.h:139
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
exprt & op0()
Definition: expr.h:133
operandst & operands()
Definition: expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
The Boolean constant false.
Definition: std_expr.h:3082
Binary greater than operator expression.
Definition: std_expr.h:807
greater_than_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:809
Binary greater than or equal operator expression.
Definition: std_expr.h:828
greater_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:830
The trinary if-then-else operator.
Definition: std_expr.h:2380
const exprt & false_case() const
Definition: std_expr.h:2422
if_exprt(exprt cond, const exprt &t, exprt f)
Definition: std_expr.h:2382
const exprt & true_case() const
Definition: std_expr.h:2412
const exprt & cond() const
Definition: std_expr.h:2402
exprt & true_case()
Definition: std_expr.h:2407
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition: std_expr.h:2387
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2427
exprt & false_case()
Definition: std_expr.h:2417
exprt & cond()
Definition: std_expr.h:2397
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2434
Boolean implication.
Definition: std_expr.h:2188
implies_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2190
exprt & index()
Definition: std_expr.h:2573
index_designatort(exprt _index)
Definition: std_expr.h:2563
const exprt & index() const
Definition: std_expr.h:2568
Array index operator.
Definition: std_expr.h:1470
index_exprt(exprt _array, exprt _index, typet _type)
Definition: std_expr.h:1488
const exprt & index() const
Definition: std_expr.h:1515
index_exprt(const exprt &_array, exprt _index)
Definition: std_expr.h:1476
exprt & array()
Definition: std_expr.h:1500
const exprt & array() const
Definition: std_expr.h:1505
exprt & index()
Definition: std_expr.h:1510
An expression denoting infinity.
Definition: std_expr.h:3107
infinity_exprt(typet _type)
Definition: std_expr.h:3109
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
std::size_t get_size_t(const irep_idt &name) const
Definition: irep.cpp:67
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void remove(const irep_idt &name)
Definition: irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:82
const irep_idt & id() const
Definition: irep.h:388
Binary less than operator expression.
Definition: std_expr.h:849
less_than_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:851
Binary less than or equal operator expression.
Definition: std_expr.h:870
less_than_or_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:872
A let expression.
Definition: std_expr.h:3214
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition: std_expr.h:3301
const binding_exprt & binding() const
Definition: std_expr.h:3247
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3307
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition: std_expr.h:3261
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition: std_expr.h:3234
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:3295
const operandst & values() const
Definition: std_expr.h:3289
static void validate(const exprt &, validation_modet)
Definition: std_expr.cpp:168
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition: std_expr.h:3216
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:3253
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:3269
binding_exprt & binding()
Definition: std_expr.h:3242
operandst & values()
Definition: std_expr.h:3284
const exprt & value() const
convenience accessor for the value of a single binding
Definition: std_expr.h:3277
const exprt & where() const
convenience accessor for binding().where()
Definition: std_expr.h:3313
irep_idt get_component_name() const
Definition: std_expr.h:2622
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:2616
Extract member of struct or union.
Definition: std_expr.h:2854
const exprt & compound() const
Definition: std_expr.h:2903
const exprt & struct_op() const
Definition: std_expr.h:2892
exprt & struct_op()
Definition: std_expr.h:2898
irep_idt get_component_name() const
Definition: std_expr.h:2876
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:2881
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:133
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2913
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition: std_expr.h:2856
std::size_t get_component_number() const
Definition: std_expr.h:2886
member_exprt(exprt op, const struct_typet::componentt &c)
Definition: std_expr.h:2866
exprt & compound()
Definition: std_expr.h:2908
Binary minus.
Definition: std_expr.h:1061
minus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1063
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1228
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1242
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1254
mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1230
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1236
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1248
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1107
mult_exprt(exprt::operandst factors, typet type)
Definition: std_expr.h:1114
mult_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1109
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:912
const exprt & op0() const
Definition: std_expr.h:956
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:925
exprt & op2()
Definition: std_expr.h:944
exprt & op3()
Definition: std_expr.h:950
const exprt & op3() const
Definition: std_expr.h:974
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:920
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition: std_expr.h:914
const exprt & op1() const
Definition: std_expr.h:962
exprt & op1()
Definition: std_expr.h:938
exprt & op0()
Definition: std_expr.h:932
const exprt & op2() const
Definition: std_expr.h:968
Expression that introduces a new symbol that is equal to the operand.
Definition: std_expr.h:3622
symbol_exprt & symbol()
Definition: std_expr.h:3639
named_term_exprt(symbol_exprt symbol, exprt value)
Definition: std_expr.h:3624
exprt & value()
Definition: std_expr.h:3649
const symbol_exprt & symbol() const
Definition: std_expr.h:3634
const exprt & value() const
Definition: std_expr.h:3644
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3091
Expression to hold a nondeterministic choice.
Definition: std_expr.h:292
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:315
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:296
const irep_idt & get_identifier() const
Definition: std_expr.h:320
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition: std_expr.h:305
Boolean negation.
Definition: std_expr.h:2337
not_exprt(exprt _op)
Definition: std_expr.h:2339
Disequality.
Definition: std_expr.h:1425
notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1427
An expression without operands.
Definition: std_expr.h:22
const operandst & operands() const =delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:29
operandst & operands()=delete
remove all operand methods
exprt & op3()=delete
exprt & op1()=delete
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:39
nullary_exprt(const irep_idt &_id, typet _type)
Definition: std_expr.h:24
exprt & op0()=delete
const exprt & op0() const =delete
void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete
void copy_to_operands(const exprt &expr)=delete
void copy_to_operands(const exprt &, const exprt &)=delete
const exprt & op3() const =delete
const exprt & op1() const =delete
const exprt & op2() const =delete
exprt & op2()=delete
Boolean OR.
Definition: std_expr.h:2233
or_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2240
or_exprt(exprt::operandst _operands)
Definition: std_expr.h:2256
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2248
or_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2235
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition: std_expr.h:1009
plus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1004
plus_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1018
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:574
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:576
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:596
sign_exprt(exprt _op)
Definition: std_expr.h:598
Struct constructor from list of elements.
Definition: std_expr.h:1877
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:114
struct_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1879
const irep_idt & get_name() const
Definition: std_types.h:79
Expression to hold a symbol (variable)
Definition: std_expr.h:131
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:155
symbol_exprt && with_source_location(const exprt &other) &&
Add the source location from other, if it has any.
Definition: std_expr.h:190
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:150
symbol_exprt && with_source_location(source_locationt location) &&
Add the source location from location, if it is non-nil.
Definition: std_expr.h:174
symbol_exprt(typet type)
Definition: std_expr.h:134
symbol_exprt & with_source_location(const exprt &other) &
Add the source location from other, if it has any.
Definition: std_expr.h:182
symbol_exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition: std_expr.h:166
symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:140
const irep_idt & get_identifier() const
Definition: std_expr.h:160
An expression with three operands.
Definition: std_expr.h:67
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:101
exprt & op3()=delete
exprt & op1()
Definition: expr.h:136
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition: std_expr.h:70
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
const exprt & op3() const =delete
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:91
The Boolean constant true.
Definition: std_expr.h:3073
An expression denoting a type.
Definition: std_expr.h:2964
type_exprt(typet type)
Definition: std_expr.h:2966
Semantic type conversion.
Definition: std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
typecast_exprt(exprt op, typet _type)
Definition: std_expr.h:2075
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:361
exprt & op()
Definition: std_expr.h:396
const exprt & op1() const =delete
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:363
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:373
exprt & op2()=delete
const exprt & op() const
Definition: std_expr.h:391
exprt & op1()=delete
const exprt & op3() const =delete
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition: std_expr.h:368
const exprt & op2() const =delete
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:383
exprt & op3()=delete
The unary minus expression.
Definition: std_expr.h:484
unary_minus_exprt(exprt _op)
Definition: std_expr.h:491
unary_minus_exprt(exprt _op, typet _type)
Definition: std_expr.h:486
The unary plus expression.
Definition: std_expr.h:531
unary_plus_exprt(exprt op)
Definition: std_expr.h:533
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:585
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition: std_expr.h:587
Union constructor from single element.
Definition: std_expr.h:1770
std::size_t get_component_number() const
Definition: std_expr.h:1788
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1793
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1783
irep_idt get_component_name() const
Definition: std_expr.h:1778
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition: std_expr.h:1772
Operator to update elements in structs and arrays.
Definition: std_expr.h:2665
exprt::operandst & designator()
Definition: std_expr.h:2691
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
Definition: std_expr.cpp:194
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2721
exprt & old()
Definition: std_expr.h:2677
const exprt & new_value() const
Definition: std_expr.h:2706
exprt & new_value()
Definition: std_expr.h:2701
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition: std_expr.h:2667
const exprt & old() const
Definition: std_expr.h:2682
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2714
const exprt::operandst & designator() const
Definition: std_expr.h:2696
Vector constructor from list of elements.
Definition: std_expr.h:1734
vector_exprt(operandst _operands, vector_typet _type)
Definition: std_expr.h:1736
The vector type.
Definition: std_types.h:1061
Operator to update elements in structs and arrays.
Definition: std_expr.h:2481
const exprt & new_value() const
Definition: std_expr.h:2516
exprt & old()
Definition: std_expr.h:2491
const exprt & old() const
Definition: std_expr.h:2496
exprt & new_value()
Definition: std_expr.h:2511
exprt & where()
Definition: std_expr.h:2501
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition: std_expr.h:2483
const exprt & where() const
Definition: std_expr.h:2506
Boolean XOR.
Definition: std_expr.h:2296
xor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2298
xor_exprt(exprt::operandst _operands)
Definition: std_expr.h:2303
Templated functions to cast to specific exprt-derived classes.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
const irept & get_nil_irep()
Definition: irep.cpp:19
dstring_hash irep_id_hash
Definition: irep.h:38
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1391
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2321
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2596
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1434
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:1949
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:2346
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1450
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2091
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:2645
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2460
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1889
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2748
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2310
const empty_union_exprt & to_empty_union_expr(const exprt &expr)
Cast an exprt to an empty_union_exprt.
Definition: std_expr.h:1860
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1121
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3338
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:2444
bool can_cast_expr< named_term_exprt >(const exprt &base)
Definition: std_expr.h:3656
bool can_cast_expr< binding_exprt >(const exprt &base)
Definition: std_expr.h:3168
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2280
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:556
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3055
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1277
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:2629
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition: std_expr.h:3473
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1665
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:2036
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3490
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:450
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:605
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2172
bool can_cast_expr< type_exprt >(const exprt &base)
Definition: std_expr.h:2972
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2107
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:71
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:3611
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:2010
void validate_expr(const symbol_exprt &value)
Definition: std_expr.h:261
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2362
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:498
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1816
bool can_cast_expr< less_than_exprt >(const exprt &base)
Definition: std_expr.h:858
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1716
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:2523
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:514
const named_term_exprt & to_named_term_expr(const exprt &expr)
Cast an exprt to a named_term_exprt.
Definition: std_expr.h:3672
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:83
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1206
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1086
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:1070
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:3322
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:1025
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1587
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1754
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:327
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:3039
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:987
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2543
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1900
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1522
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:256
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition: std_expr.h:2983
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
Definition: std_expr.h:116
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:2930
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1603
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition: std_expr.h:1345
bool can_cast_expr< empty_union_exprt >(const exprt &base)
Definition: std_expr.h:1843
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:2269
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1261
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition: std_expr.h:3380
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1407
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:2731
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:795
bool can_cast_expr< euclidean_mod_exprt >(const exprt &base)
Definition: std_expr.h:1329
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1041
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1743
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1965
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1706
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:2580
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2946
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:426
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:540
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2161
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:343
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition: std_expr.h:816
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2213
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1654
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:2053
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:699
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1190
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition: std_expr.h:3100
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:3603
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition: std_expr.h:3186
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:621
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:837
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2197
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:410
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:466
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:879
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1800
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:895
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1538
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1137
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:1993
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:3397
Pre-defined types.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1155
size_t operator()(const ::symbol_exprt &sym)
Definition: std_expr.h:205
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:208
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet