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