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 "as_const.h"
17 #include "expr_cast.h"
18 #include "invariant.h"
19 #include "narrow.h"
20 #include "std_types.h"
21 
24 {
25 public:
26  nullary_exprt(const irep_idt &_id, typet _type)
27  : expr_protectedt(_id, std::move(_type))
28  {
29  }
30 
32  operandst &operands() = delete;
33  const operandst &operands() const = delete;
34 
35  const exprt &op0() const = delete;
36  exprt &op0() = delete;
37  const exprt &op1() const = delete;
38  exprt &op1() = delete;
39  const exprt &op2() const = delete;
40  exprt &op2() = delete;
41  const exprt &op3() const = delete;
42  exprt &op3() = delete;
43 
44  void move_to_operands(exprt &) = delete;
45  void move_to_operands(exprt &, exprt &) = delete;
46  void move_to_operands(exprt &, exprt &, exprt &) = delete;
47 
48  void copy_to_operands(const exprt &expr) = delete;
49  void copy_to_operands(const exprt &, const exprt &) = delete;
50  void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
51 };
52 
55 {
56 public:
57  // constructors
58  DEPRECATED(
59  SINCE(2018, 9, 21, "use ternary_exprt(id, op0, op1, op2, type) instead"))
60  explicit ternary_exprt(const irep_idt &_id) : expr_protectedt(_id, type())
61  {
62  operands().resize(3);
63  }
64 
66  const irep_idt &_id,
67  exprt _op0,
68  exprt _op1,
69  exprt _op2,
70  typet _type)
72  _id,
73  std::move(_type),
74  {std::move(_op0), std::move(_op1), std::move(_op2)})
75  {
76  }
77 
78  // make op0 to op2 public
79  using exprt::op0;
80  using exprt::op1;
81  using exprt::op2;
82 
83  const exprt &op3() const = delete;
84  exprt &op3() = delete;
85 };
86 
89 {
90 public:
92  explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type))
93  {
94  }
95 
98  symbol_exprt(const irep_idt &identifier, typet type)
99  : nullary_exprt(ID_symbol, std::move(type))
100  {
101  set_identifier(identifier);
102  }
103 
108  static symbol_exprt typeless(const irep_idt &id)
109  {
110  return symbol_exprt(id, typet());
111  }
112 
113  void set_identifier(const irep_idt &identifier)
114  {
115  set(ID_identifier, identifier);
116  }
117 
118  const irep_idt &get_identifier() const
119  {
120  return get(ID_identifier);
121  }
122 };
123 
127 {
128 public:
132  : symbol_exprt(identifier, std::move(type))
133  {
134  }
135 
136  bool is_static_lifetime() const
137  {
138  return get_bool(ID_C_static_lifetime);
139  }
140 
142  {
143  return set(ID_C_static_lifetime, true);
144  }
145 
147  {
148  remove(ID_C_static_lifetime);
149  }
150 
151  bool is_thread_local() const
152  {
153  return get_bool(ID_C_thread_local);
154  }
155 
157  {
158  return set(ID_C_thread_local, true);
159  }
160 
162  {
163  remove(ID_C_thread_local);
164  }
165 };
166 
167 template <>
168 inline bool can_cast_expr<symbol_exprt>(const exprt &base)
169 {
170  return base.id() == ID_symbol;
171 }
172 
173 inline void validate_expr(const symbol_exprt &value)
174 {
175  validate_operands(value, 0, "Symbols must not have operands");
176 }
177 
184 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
185 {
186  PRECONDITION(expr.id()==ID_symbol);
187  const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
188  validate_expr(ret);
189  return ret;
190 }
191 
194 {
195  PRECONDITION(expr.id()==ID_symbol);
196  symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
197  validate_expr(ret);
198  return ret;
199 }
200 
201 
204 {
205 public:
209  : nullary_exprt(ID_nondet_symbol, std::move(type))
210  {
211  set_identifier(identifier);
212  }
213 
218  irep_idt identifier,
219  typet type,
220  source_locationt location)
221  : nullary_exprt(ID_nondet_symbol, std::move(type))
222  {
223  set_identifier(std::move(identifier));
224  add_source_location() = std::move(location);
225  }
226 
227  void set_identifier(const irep_idt &identifier)
228  {
229  set(ID_identifier, identifier);
230  }
231 
232  const irep_idt &get_identifier() const
233  {
234  return get(ID_identifier);
235  }
236 };
237 
238 template <>
240 {
241  return base.id() == ID_nondet_symbol;
242 }
243 
244 inline void validate_expr(const nondet_symbol_exprt &value)
245 {
246  validate_operands(value, 0, "Symbols must not have operands");
247 }
248 
256 {
257  PRECONDITION(expr.id()==ID_nondet_symbol);
258  const nondet_symbol_exprt &ret =
259  static_cast<const nondet_symbol_exprt &>(expr);
260  validate_expr(ret);
261  return ret;
262 }
263 
266 {
267  PRECONDITION(expr.id()==ID_symbol);
268  nondet_symbol_exprt &ret = static_cast<nondet_symbol_exprt &>(expr);
269  validate_expr(ret);
270  return ret;
271 }
272 
273 
276 {
277 public:
278  unary_exprt(const irep_idt &_id, const exprt &_op)
279  : expr_protectedt(_id, _op.type(), {_op})
280  {
281  }
282 
283  DEPRECATED(SINCE(2018, 12, 2, "use unary_exprt(id, op, type) instead"))
284  unary_exprt(const irep_idt &_id, const typet &_type)
285  : expr_protectedt(_id, _type)
286  {
287  operands().resize(1);
288  }
289 
290  unary_exprt(const irep_idt &_id, exprt _op, typet _type)
291  : expr_protectedt(_id, std::move(_type), {std::move(_op)})
292  {
293  }
294 
295  const exprt &op() const
296  {
297  return op0();
298  }
299 
301  {
302  return op0();
303  }
304 
305  const exprt &op1() const = delete;
306  exprt &op1() = delete;
307  const exprt &op2() const = delete;
308  exprt &op2() = delete;
309  const exprt &op3() const = delete;
310  exprt &op3() = delete;
311 };
312 
313 template <>
314 inline bool can_cast_expr<unary_exprt>(const exprt &base)
315 {
316  return base.operands().size() == 1;
317 }
318 
319 inline void validate_expr(const unary_exprt &value)
320 {
321  validate_operands(value, 1, "Unary expressions must have one operand");
322 }
323 
330 inline const unary_exprt &to_unary_expr(const exprt &expr)
331 {
332  const unary_exprt &ret = static_cast<const unary_exprt &>(expr);
333  validate_expr(ret);
334  return ret;
335 }
336 
339 {
340  unary_exprt &ret = static_cast<unary_exprt &>(expr);
341  validate_expr(ret);
342  return ret;
343 }
344 
345 
347 class abs_exprt:public unary_exprt
348 {
349 public:
350  explicit abs_exprt(exprt _op) : unary_exprt(ID_abs, std::move(_op))
351  {
352  }
353 };
354 
355 template <>
356 inline bool can_cast_expr<abs_exprt>(const exprt &base)
357 {
358  return base.id() == ID_abs;
359 }
360 
361 inline void validate_expr(const abs_exprt &value)
362 {
363  validate_operands(value, 1, "Absolute value must have one operand");
364 }
365 
372 inline const abs_exprt &to_abs_expr(const exprt &expr)
373 {
374  PRECONDITION(expr.id()==ID_abs);
375  const abs_exprt &ret = static_cast<const abs_exprt &>(expr);
376  validate_expr(ret);
377  return ret;
378 }
379 
382 {
383  PRECONDITION(expr.id()==ID_abs);
384  abs_exprt &ret = static_cast<abs_exprt &>(expr);
385  validate_expr(ret);
386  return ret;
387 }
388 
389 
392 {
393 public:
395  : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
396  {
397  }
398 
399  explicit unary_minus_exprt(exprt _op)
400  : unary_exprt(ID_unary_minus, std::move(_op))
401  {
402  }
403 };
404 
405 template <>
406 inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
407 {
408  return base.id() == ID_unary_minus;
409 }
410 
411 inline void validate_expr(const unary_minus_exprt &value)
412 {
413  validate_operands(value, 1, "Unary minus must have one operand");
414 }
415 
422 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
423 {
424  PRECONDITION(expr.id()==ID_unary_minus);
425  const unary_minus_exprt &ret = static_cast<const unary_minus_exprt &>(expr);
426  validate_expr(ret);
427  return ret;
428 }
429 
432 {
433  PRECONDITION(expr.id()==ID_unary_minus);
434  unary_minus_exprt &ret = static_cast<unary_minus_exprt &>(expr);
435  validate_expr(ret);
436  return ret;
437 }
438 
441 {
442 public:
444  : unary_exprt(ID_unary_plus, std::move(op))
445  {
446  }
447 };
448 
449 template <>
450 inline bool can_cast_expr<unary_plus_exprt>(const exprt &base)
451 {
452  return base.id() == ID_unary_plus;
453 }
454 
455 inline void validate_expr(const unary_plus_exprt &value)
456 {
457  validate_operands(value, 1, "unary plus must have one operand");
458 }
459 
466 inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
467 {
468  PRECONDITION(expr.id() == ID_unary_plus);
469  const unary_plus_exprt &ret = static_cast<const unary_plus_exprt &>(expr);
470  validate_expr(ret);
471  return ret;
472 }
473 
476 {
477  PRECONDITION(expr.id() == ID_unary_plus);
478  unary_plus_exprt &ret = static_cast<unary_plus_exprt &>(expr);
479  validate_expr(ret);
480  return ret;
481 }
482 
485 {
486 public:
487  bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
488  : unary_exprt(ID_bswap, std::move(_op), std::move(_type))
489  {
490  set_bits_per_byte(bits_per_byte);
491  }
492 
493  bswap_exprt(exprt _op, std::size_t bits_per_byte)
494  : unary_exprt(ID_bswap, std::move(_op))
495  {
496  set_bits_per_byte(bits_per_byte);
497  }
498 
499  std::size_t get_bits_per_byte() const
500  {
501  return get_size_t(ID_bits_per_byte);
502  }
503 
504  void set_bits_per_byte(std::size_t bits_per_byte)
505  {
506  set(ID_bits_per_byte, narrow_cast<long long>(bits_per_byte));
507  }
508 };
509 
510 template <>
511 inline bool can_cast_expr<bswap_exprt>(const exprt &base)
512 {
513  return base.id() == ID_bswap;
514 }
515 
516 inline void validate_expr(const bswap_exprt &value)
517 {
518  validate_operands(value, 1, "bswap must have one operand");
520  value.op().type() == value.type(), "bswap type must match operand type");
521 }
522 
529 inline const bswap_exprt &to_bswap_expr(const exprt &expr)
530 {
531  PRECONDITION(expr.id() == ID_bswap);
532  const bswap_exprt &ret = static_cast<const bswap_exprt &>(expr);
533  validate_expr(ret);
534  return ret;
535 }
536 
539 {
540  PRECONDITION(expr.id() == ID_bswap);
541  bswap_exprt &ret = static_cast<bswap_exprt &>(expr);
542  validate_expr(ret);
543  return ret;
544 }
545 
549 {
550 public:
551  DEPRECATED(SINCE(2018, 12, 2, "use predicate_exprt(id) instead"))
553  {
554  }
555 
556  explicit predicate_exprt(const irep_idt &_id)
557  : expr_protectedt(_id, bool_typet())
558  {
559  }
560 
561  DEPRECATED(SINCE(2018, 12, 2, "use unary_predicate_exprt(id, op) instead"))
562  predicate_exprt(const irep_idt &_id, const exprt &_op)
563  : expr_protectedt(_id, bool_typet())
564  {
565  add_to_operands(_op);
566  }
567 
568  DEPRECATED(
569  SINCE(2018, 12, 2, "use binary_predicate_exprt(op1, id, op2) instead"))
570  predicate_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1)
571  : expr_protectedt(_id, bool_typet())
572  {
573  add_to_operands(_op0, _op1);
574  }
575 };
576 
580 {
581 public:
582  DEPRECATED(SINCE(2018, 12, 2, "use unary_predicate_exprt(id, op) instead"))
584  {
585  }
586 
587  DEPRECATED(SINCE(2018, 12, 2, "use unary_predicate_exprt(id, op) instead"))
588  explicit unary_predicate_exprt(const irep_idt &_id):
589  unary_exprt(_id, bool_typet())
590  {
591  }
592 
594  : unary_exprt(_id, std::move(_op), bool_typet())
595  {
596  }
597 };
598 
602 {
603 public:
604  DEPRECATED(SINCE(2018, 12, 2, "use sign_exprt(op) instead"))
606  {
607  }
608 
609  explicit sign_exprt(exprt _op)
610  : unary_predicate_exprt(ID_sign, std::move(_op))
611  {
612  }
613 };
614 
615 template <>
616 inline bool can_cast_expr<sign_exprt>(const exprt &base)
617 {
618  return base.id() == ID_sign;
619 }
620 
621 inline void validate_expr(const sign_exprt &expr)
622 {
623  validate_operands(expr, 1, "sign expression must have one operand");
624 }
625 
632 inline const sign_exprt &to_sign_expr(const exprt &expr)
633 {
634  PRECONDITION(expr.id() == ID_sign);
635  const sign_exprt &ret = static_cast<const sign_exprt &>(expr);
636  validate_expr(ret);
637  return ret;
638 }
639 
642 {
643  PRECONDITION(expr.id() == ID_sign);
644  sign_exprt &ret = static_cast<sign_exprt &>(expr);
645  validate_expr(ret);
646  return ret;
647 }
648 
651 {
652 public:
653  DEPRECATED(SINCE(2018, 9, 21, "use binary_exprt(lhs, id, rhs) instead"))
654  explicit binary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet())
655  {
656  operands().resize(2);
657  }
658 
659  DEPRECATED(SINCE(2018, 12, 2, "use binary_exprt(lhs, id, rhs, type) instead"))
660  binary_exprt(const irep_idt &_id, const typet &_type)
661  : expr_protectedt(_id, _type)
662  {
663  operands().resize(2);
664  }
665 
666  binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
667  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
668  {
669  }
670 
671  binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
672  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
673  {
674  }
675 
676  static void check(
677  const exprt &expr,
679  {
680  DATA_CHECK(
681  vm,
682  expr.operands().size() == 2,
683  "binary expression must have two operands");
684  }
685 
686  static void validate(
687  const exprt &expr,
688  const namespacet &,
690  {
691  check(expr, vm);
692  }
693 
695  {
696  return exprt::op0();
697  }
698 
699  const exprt &lhs() const
700  {
701  return exprt::op0();
702  }
703 
705  {
706  return exprt::op1();
707  }
708 
709  const exprt &rhs() const
710  {
711  return exprt::op1();
712  }
713 
714  // make op0 and op1 public
715  using exprt::op0;
716  using exprt::op1;
717 
718  const exprt &op2() const = delete;
719  exprt &op2() = delete;
720  const exprt &op3() const = delete;
721  exprt &op3() = delete;
722 };
723 
724 template <>
725 inline bool can_cast_expr<binary_exprt>(const exprt &base)
726 {
727  return base.operands().size() == 2;
728 }
729 
730 inline void validate_expr(const binary_exprt &value)
731 {
732  binary_exprt::check(value);
733 }
734 
741 inline const binary_exprt &to_binary_expr(const exprt &expr)
742 {
743  binary_exprt::check(expr);
744  return static_cast<const binary_exprt &>(expr);
745 }
746 
749 {
750  binary_exprt::check(expr);
751  return static_cast<binary_exprt &>(expr);
752 }
753 
757 {
758 public:
759  DEPRECATED(
760  SINCE(2018, 12, 2, "use binary_predicate_exprt(lhs, id, rhs) instead"))
762  {
763  }
764 
765  DEPRECATED(
766  SINCE(2018, 12, 2, "use binary_predicate_exprt(lhs, id, rhs) instead"))
767  explicit binary_predicate_exprt(const irep_idt &_id):
768  binary_exprt(_id, bool_typet())
769  {
770  }
771 
772  binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
773  : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
774  {
775  }
776 
777  static void check(
778  const exprt &expr,
780  {
781  binary_exprt::check(expr, vm);
782  }
783 
784  static void validate(
785  const exprt &expr,
786  const namespacet &ns,
788  {
789  binary_exprt::validate(expr, ns, vm);
790 
791  DATA_CHECK(
792  vm,
793  expr.type().id() == ID_bool,
794  "result of binary predicate expression should be of type bool");
795  }
796 };
797 
801 {
802 public:
803  DEPRECATED(
804  SINCE(2018, 12, 2, "use binary_relation_exprt(lhs, id, rhs) instead"))
806  {
807  }
808 
809  DEPRECATED(
810  SINCE(2018, 12, 2, "use binary_relation_exprt(lhs, id, rhs) instead"))
811  explicit binary_relation_exprt(const irep_idt &id):
813  {
814  }
815 
816  binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
817  : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
818  {
819  }
820 
821  static void check(
822  const exprt &expr,
824  {
826  }
827 
828  static void validate(
829  const exprt &expr,
830  const namespacet &ns,
832  {
833  binary_predicate_exprt::validate(expr, ns, vm);
834 
835  // we now can safely assume that 'expr' is a binary predicate
836  const auto &expr_binary = static_cast<const binary_predicate_exprt &>(expr);
837 
838  // check that the types of the operands are the same
839  DATA_CHECK(
840  vm,
841  expr_binary.op0().type() == expr_binary.op1().type(),
842  "lhs and rhs of binary relation expression should have same type");
843  }
844 };
845 
846 template <>
848 {
849  return can_cast_expr<binary_exprt>(base);
850 }
851 
852 inline void validate_expr(const binary_relation_exprt &value)
853 {
855 }
856 
864 {
866  return static_cast<const binary_relation_exprt &>(expr);
867 }
868 
871 {
873  return static_cast<binary_relation_exprt &>(expr);
874 }
875 
876 
880 {
881 public:
882  DEPRECATED(SINCE(2018, 9, 21, "use multi_ary_exprt(id, op, type) instead"))
883  explicit multi_ary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet())
884  {
885  }
886 
887  DEPRECATED(SINCE(2018, 12, 7, "use multi_ary_exprt(id, op, type) instead"))
888  multi_ary_exprt(const irep_idt &_id, const typet &_type)
889  : expr_protectedt(_id, _type)
890  {
891  }
892 
893  multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
894  : expr_protectedt(_id, std::move(_type))
895  {
896  operands() = std::move(_operands);
897  }
898 
899  multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
900  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
901  {
902  }
903 
904  multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
905  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
906  {
907  }
908 
909  // In contrast to exprt::opX, the methods
910  // below check the size.
912  {
913  PRECONDITION(operands().size() >= 1);
914  return operands().front();
915  }
916 
918  {
919  PRECONDITION(operands().size() >= 2);
920  return operands()[1];
921  }
922 
924  {
925  PRECONDITION(operands().size() >= 3);
926  return operands()[2];
927  }
928 
930  {
931  PRECONDITION(operands().size() >= 4);
932  return operands()[3];
933  }
934 
935  const exprt &op0() const
936  {
937  PRECONDITION(operands().size() >= 1);
938  return operands().front();
939  }
940 
941  const exprt &op1() const
942  {
943  PRECONDITION(operands().size() >= 2);
944  return operands()[1];
945  }
946 
947  const exprt &op2() const
948  {
949  PRECONDITION(operands().size() >= 3);
950  return operands()[2];
951  }
952 
953  const exprt &op3() const
954  {
955  PRECONDITION(operands().size() >= 4);
956  return operands()[3];
957  }
958 };
959 
966 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
967 {
968  return static_cast<const multi_ary_exprt &>(expr);
969 }
970 
973 {
974  return static_cast<multi_ary_exprt &>(expr);
975 }
976 
977 
981 {
982 public:
983  DEPRECATED(SINCE(2019, 1, 12, "use plus_exprt(lhs, rhs, type) instead"))
985  {
986  }
987 
988  plus_exprt(exprt _lhs, exprt _rhs)
989  : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
990  {
991  }
992 
993  plus_exprt(exprt _lhs, exprt _rhs, typet _type)
994  : multi_ary_exprt(
995  std::move(_lhs),
996  ID_plus,
997  std::move(_rhs),
998  std::move(_type))
999  {
1000  }
1001 
1002  plus_exprt(operandst _operands, typet _type)
1003  : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
1004  {
1005  }
1006 };
1007 
1008 template <>
1009 inline bool can_cast_expr<plus_exprt>(const exprt &base)
1010 {
1011  return base.id() == ID_plus;
1012 }
1013 
1014 inline void validate_expr(const plus_exprt &value)
1015 {
1016  validate_operands(value, 2, "Plus must have two or more operands", true);
1017 }
1018 
1025 inline const plus_exprt &to_plus_expr(const exprt &expr)
1026 {
1027  PRECONDITION(expr.id()==ID_plus);
1028  const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
1029  validate_expr(ret);
1030  return ret;
1031 }
1032 
1035 {
1036  PRECONDITION(expr.id()==ID_plus);
1037  plus_exprt &ret = static_cast<plus_exprt &>(expr);
1038  validate_expr(ret);
1039  return ret;
1040 }
1041 
1042 
1045 {
1046 public:
1048  : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
1049  {
1050  }
1051 };
1052 
1053 template <>
1054 inline bool can_cast_expr<minus_exprt>(const exprt &base)
1055 {
1056  return base.id() == ID_minus;
1057 }
1058 
1059 inline void validate_expr(const minus_exprt &value)
1060 {
1061  validate_operands(value, 2, "Minus must have two or more operands", true);
1062 }
1063 
1070 inline const minus_exprt &to_minus_expr(const exprt &expr)
1071 {
1072  PRECONDITION(expr.id()==ID_minus);
1073  const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
1074  validate_expr(ret);
1075  return ret;
1076 }
1077 
1080 {
1081  PRECONDITION(expr.id()==ID_minus);
1082  minus_exprt &ret = static_cast<minus_exprt &>(expr);
1083  validate_expr(ret);
1084  return ret;
1085 }
1086 
1087 
1091 {
1092 public:
1093  mult_exprt(exprt _lhs, exprt _rhs)
1094  : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
1095  {
1096  }
1097 };
1098 
1099 template <>
1100 inline bool can_cast_expr<mult_exprt>(const exprt &base)
1101 {
1102  return base.id() == ID_mult;
1103 }
1104 
1105 inline void validate_expr(const mult_exprt &value)
1106 {
1107  validate_operands(value, 2, "Multiply must have two or more operands", true);
1108 }
1109 
1116 inline const mult_exprt &to_mult_expr(const exprt &expr)
1117 {
1118  PRECONDITION(expr.id()==ID_mult);
1119  const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1120  validate_expr(ret);
1121  return ret;
1122 }
1123 
1126 {
1127  PRECONDITION(expr.id()==ID_mult);
1128  mult_exprt &ret = static_cast<mult_exprt &>(expr);
1129  validate_expr(ret);
1130  return ret;
1131 }
1132 
1133 
1136 {
1137 public:
1138  div_exprt(exprt _lhs, exprt _rhs)
1139  : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1140  {
1141  }
1142 
1145  {
1146  return op0();
1147  }
1148 
1150  const exprt &dividend() const
1151  {
1152  return op0();
1153  }
1154 
1157  {
1158  return op1();
1159  }
1160 
1162  const exprt &divisor() const
1163  {
1164  return op1();
1165  }
1166 };
1167 
1168 template <>
1169 inline bool can_cast_expr<div_exprt>(const exprt &base)
1170 {
1171  return base.id() == ID_div;
1172 }
1173 
1174 inline void validate_expr(const div_exprt &value)
1175 {
1176  validate_operands(value, 2, "Divide must have two operands");
1177 }
1178 
1185 inline const div_exprt &to_div_expr(const exprt &expr)
1186 {
1187  PRECONDITION(expr.id()==ID_div);
1188  const div_exprt &ret = static_cast<const div_exprt &>(expr);
1189  validate_expr(ret);
1190  return ret;
1191 }
1192 
1195 {
1196  PRECONDITION(expr.id()==ID_div);
1197  div_exprt &ret = static_cast<div_exprt &>(expr);
1198  validate_expr(ret);
1199  return ret;
1200 }
1201 
1202 
1205 {
1206 public:
1207  mod_exprt(exprt _lhs, exprt _rhs)
1208  : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1209  {
1210  }
1211 };
1212 
1213 template <>
1214 inline bool can_cast_expr<mod_exprt>(const exprt &base)
1215 {
1216  return base.id() == ID_mod;
1217 }
1218 
1219 inline void validate_expr(const mod_exprt &value)
1220 {
1221  validate_operands(value, 2, "Modulo must have two operands");
1222 }
1223 
1230 inline const mod_exprt &to_mod_expr(const exprt &expr)
1231 {
1232  PRECONDITION(expr.id()==ID_mod);
1233  const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1234  validate_expr(ret);
1235  return ret;
1236 }
1237 
1240 {
1241  PRECONDITION(expr.id()==ID_mod);
1242  mod_exprt &ret = static_cast<mod_exprt &>(expr);
1243  validate_expr(ret);
1244  return ret;
1245 }
1246 
1247 
1250 {
1251 public:
1252  rem_exprt(exprt _lhs, exprt _rhs)
1253  : binary_exprt(std::move(_lhs), ID_rem, std::move(_rhs))
1254  {
1255  }
1256 };
1257 
1258 template <>
1259 inline bool can_cast_expr<rem_exprt>(const exprt &base)
1260 {
1261  return base.id() == ID_rem;
1262 }
1263 
1264 inline void validate_expr(const rem_exprt &value)
1265 {
1266  validate_operands(value, 2, "Remainder must have two operands");
1267 }
1268 
1275 inline const rem_exprt &to_rem_expr(const exprt &expr)
1276 {
1277  PRECONDITION(expr.id()==ID_rem);
1278  const rem_exprt &ret = static_cast<const rem_exprt &>(expr);
1279  validate_expr(ret);
1280  return ret;
1281 }
1282 
1285 {
1286  PRECONDITION(expr.id()==ID_rem);
1287  rem_exprt &ret = static_cast<rem_exprt &>(expr);
1288  validate_expr(ret);
1289  return ret;
1290 }
1291 
1292 
1295 {
1296 public:
1298  : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1299  {
1300  }
1301 
1302  static void check(
1303  const exprt &expr,
1305  {
1306  binary_relation_exprt::check(expr, vm);
1307  }
1308 
1309  static void validate(
1310  const exprt &expr,
1311  const namespacet &ns,
1313  {
1314  binary_relation_exprt::validate(expr, ns, vm);
1315  }
1316 };
1317 
1318 template <>
1319 inline bool can_cast_expr<equal_exprt>(const exprt &base)
1320 {
1321  return base.id() == ID_equal;
1322 }
1323 
1324 inline void validate_expr(const equal_exprt &value)
1325 {
1326  equal_exprt::check(value);
1327 }
1328 
1335 inline const equal_exprt &to_equal_expr(const exprt &expr)
1336 {
1337  PRECONDITION(expr.id()==ID_equal);
1338  equal_exprt::check(expr);
1339  return static_cast<const equal_exprt &>(expr);
1340 }
1341 
1344 {
1345  PRECONDITION(expr.id()==ID_equal);
1346  equal_exprt::check(expr);
1347  return static_cast<equal_exprt &>(expr);
1348 }
1349 
1350 
1353 {
1354 public:
1356  : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1357  {
1358  }
1359 };
1360 
1361 template <>
1362 inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1363 {
1364  return base.id() == ID_notequal;
1365 }
1366 
1367 inline void validate_expr(const notequal_exprt &value)
1368 {
1369  validate_operands(value, 2, "Inequality must have two operands");
1370 }
1371 
1378 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1379 {
1380  PRECONDITION(expr.id()==ID_notequal);
1381  const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1382  validate_expr(ret);
1383  return ret;
1384 }
1385 
1388 {
1389  PRECONDITION(expr.id()==ID_notequal);
1390  notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1391  validate_expr(ret);
1392  return ret;
1393 }
1394 
1395 
1398 {
1399 public:
1400  index_exprt(const exprt &_array, exprt _index)
1401  : binary_exprt(_array, ID_index, std::move(_index), _array.type().subtype())
1402  {
1403  }
1404 
1405  index_exprt(exprt _array, exprt _index, typet _type)
1406  : binary_exprt(
1407  std::move(_array),
1408  ID_index,
1409  std::move(_index),
1410  std::move(_type))
1411  {
1412  }
1413 
1415  {
1416  return op0();
1417  }
1418 
1419  const exprt &array() const
1420  {
1421  return op0();
1422  }
1423 
1425  {
1426  return op1();
1427  }
1428 
1429  const exprt &index() const
1430  {
1431  return op1();
1432  }
1433 };
1434 
1435 template <>
1436 inline bool can_cast_expr<index_exprt>(const exprt &base)
1437 {
1438  return base.id() == ID_index;
1439 }
1440 
1441 inline void validate_expr(const index_exprt &value)
1442 {
1443  validate_operands(value, 2, "Array index must have two operands");
1444 }
1445 
1452 inline const index_exprt &to_index_expr(const exprt &expr)
1453 {
1454  PRECONDITION(expr.id()==ID_index);
1455  const index_exprt &ret = static_cast<const index_exprt &>(expr);
1456  validate_expr(ret);
1457  return ret;
1458 }
1459 
1462 {
1463  PRECONDITION(expr.id()==ID_index);
1464  index_exprt &ret = static_cast<index_exprt &>(expr);
1465  validate_expr(ret);
1466  return ret;
1467 }
1468 
1469 
1472 {
1473 public:
1474  explicit array_of_exprt(exprt _what, array_typet _type)
1475  : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1476  {
1477  }
1478 
1479  const array_typet &type() const
1480  {
1481  return static_cast<const array_typet &>(unary_exprt::type());
1482  }
1483 
1485  {
1486  return static_cast<array_typet &>(unary_exprt::type());
1487  }
1488 
1490  {
1491  return op0();
1492  }
1493 
1494  const exprt &what() const
1495  {
1496  return op0();
1497  }
1498 };
1499 
1500 template <>
1501 inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1502 {
1503  return base.id() == ID_array_of;
1504 }
1505 
1506 inline void validate_expr(const array_of_exprt &value)
1507 {
1508  validate_operands(value, 1, "'Array of' must have one operand");
1509 }
1510 
1517 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1518 {
1519  PRECONDITION(expr.id()==ID_array_of);
1520  const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1521  validate_expr(ret);
1522  return ret;
1523 }
1524 
1527 {
1528  PRECONDITION(expr.id()==ID_array_of);
1529  array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1530  validate_expr(ret);
1531  return ret;
1532 }
1533 
1534 
1537 {
1538 public:
1539  DEPRECATED(SINCE(2019, 1, 12, "use array_exprt(operands, type) instead"))
1540  explicit array_exprt(const array_typet &_type)
1541  : multi_ary_exprt(ID_array, _type)
1542  {
1543  }
1544 
1546  : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1547  {
1548  }
1549 
1550  const array_typet &type() const
1551  {
1552  return static_cast<const array_typet &>(multi_ary_exprt::type());
1553  }
1554 
1556  {
1557  return static_cast<array_typet &>(multi_ary_exprt::type());
1558  }
1559 };
1560 
1561 template <>
1562 inline bool can_cast_expr<array_exprt>(const exprt &base)
1563 {
1564  return base.id() == ID_array;
1565 }
1566 
1573 inline const array_exprt &to_array_expr(const exprt &expr)
1574 {
1575  PRECONDITION(expr.id()==ID_array);
1576  return static_cast<const array_exprt &>(expr);
1577 }
1578 
1581 {
1582  PRECONDITION(expr.id()==ID_array);
1583  return static_cast<array_exprt &>(expr);
1584 }
1585 
1589 {
1590 public:
1591  DEPRECATED(SINCE(2019, 1, 12, "use array_list_exprt(operands, type) instead"))
1592  explicit array_list_exprt(const array_typet &_type)
1593  : multi_ary_exprt(ID_array_list, _type)
1594  {
1595  }
1596 
1598  : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1599  {
1600  }
1601 
1602  const array_typet &type() const
1603  {
1604  return static_cast<const array_typet &>(multi_ary_exprt::type());
1605  }
1606 
1608  {
1609  return static_cast<array_typet &>(multi_ary_exprt::type());
1610  }
1611 
1613  void add(exprt index, exprt value)
1614  {
1615  add_to_operands(std::move(index), std::move(value));
1616  }
1617 };
1618 
1619 template <>
1620 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1621 {
1622  return base.id() == ID_array_list;
1623 }
1624 
1625 inline void validate_expr(const array_list_exprt &value)
1626 {
1627  PRECONDITION(value.operands().size() % 2 == 0);
1628 }
1629 
1630 inline const array_list_exprt &to_array_list_expr(const exprt &expr)
1631 {
1633  auto &ret = static_cast<const array_list_exprt &>(expr);
1634  validate_expr(ret);
1635  return ret;
1636 }
1637 
1639 {
1641  auto &ret = static_cast<array_list_exprt &>(expr);
1642  validate_expr(ret);
1643  return ret;
1644 }
1645 
1648 {
1649 public:
1650  DEPRECATED(SINCE(2019, 1, 12, "use vector_exprt(operands, type) instead"))
1651  explicit vector_exprt(const vector_typet &_type)
1652  : multi_ary_exprt(ID_vector, _type)
1653  {
1654  }
1655 
1657  : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1658  {
1659  }
1660 };
1661 
1662 template <>
1663 inline bool can_cast_expr<vector_exprt>(const exprt &base)
1664 {
1665  return base.id() == ID_vector;
1666 }
1667 
1674 inline const vector_exprt &to_vector_expr(const exprt &expr)
1675 {
1676  PRECONDITION(expr.id()==ID_vector);
1677  return static_cast<const vector_exprt &>(expr);
1678 }
1679 
1682 {
1683  PRECONDITION(expr.id()==ID_vector);
1684  return static_cast<vector_exprt &>(expr);
1685 }
1686 
1687 
1690 {
1691 public:
1692  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1693  : unary_exprt(ID_union, std::move(_value), std::move(_type))
1694  {
1695  set_component_name(_component_name);
1696  }
1697 
1699  {
1700  return get(ID_component_name);
1701  }
1702 
1703  void set_component_name(const irep_idt &component_name)
1704  {
1705  set(ID_component_name, component_name);
1706  }
1707 
1708  std::size_t get_component_number() const
1709  {
1710  return get_size_t(ID_component_number);
1711  }
1712 
1713  void set_component_number(std::size_t component_number)
1714  {
1715  set(ID_component_number, narrow_cast<long long>(component_number));
1716  }
1717 };
1718 
1719 template <>
1720 inline bool can_cast_expr<union_exprt>(const exprt &base)
1721 {
1722  return base.id() == ID_union;
1723 }
1724 
1725 inline void validate_expr(const union_exprt &value)
1726 {
1727  validate_operands(value, 1, "Union constructor must have one operand");
1728 }
1729 
1736 inline const union_exprt &to_union_expr(const exprt &expr)
1737 {
1738  PRECONDITION(expr.id()==ID_union);
1739  const union_exprt &ret = static_cast<const union_exprt &>(expr);
1740  validate_expr(ret);
1741  return ret;
1742 }
1743 
1746 {
1747  PRECONDITION(expr.id()==ID_union);
1748  union_exprt &ret = static_cast<union_exprt &>(expr);
1749  validate_expr(ret);
1750  return ret;
1751 }
1752 
1753 
1756 {
1757 public:
1758  DEPRECATED(SINCE(2019, 1, 12, "use struct_exprt(operands, type) instead"))
1759  explicit struct_exprt(const typet &_type) : multi_ary_exprt(ID_struct, _type)
1760  {
1761  }
1762 
1763  struct_exprt(operandst _operands, typet _type)
1764  : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1765  {
1766  }
1767 
1768  exprt &component(const irep_idt &name, const namespacet &ns);
1769  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1770 };
1771 
1772 template <>
1773 inline bool can_cast_expr<struct_exprt>(const exprt &base)
1774 {
1775  return base.id() == ID_struct;
1776 }
1777 
1784 inline const struct_exprt &to_struct_expr(const exprt &expr)
1785 {
1786  PRECONDITION(expr.id()==ID_struct);
1787  return static_cast<const struct_exprt &>(expr);
1788 }
1789 
1792 {
1793  PRECONDITION(expr.id()==ID_struct);
1794  return static_cast<struct_exprt &>(expr);
1795 }
1796 
1797 
1800 {
1801 public:
1803  : binary_exprt(
1804  std::move(_real),
1805  ID_complex,
1806  std::move(_imag),
1807  std::move(_type))
1808  {
1809  }
1810 
1812  {
1813  return op0();
1814  }
1815 
1816  const exprt &real() const
1817  {
1818  return op0();
1819  }
1820 
1822  {
1823  return op1();
1824  }
1825 
1826  const exprt &imag() const
1827  {
1828  return op1();
1829  }
1830 };
1831 
1832 template <>
1833 inline bool can_cast_expr<complex_exprt>(const exprt &base)
1834 {
1835  return base.id() == ID_complex;
1836 }
1837 
1838 inline void validate_expr(const complex_exprt &value)
1839 {
1840  validate_operands(value, 2, "Complex constructor must have two operands");
1841 }
1842 
1849 inline const complex_exprt &to_complex_expr(const exprt &expr)
1850 {
1851  PRECONDITION(expr.id()==ID_complex);
1852  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1853  validate_expr(ret);
1854  return ret;
1855 }
1856 
1859 {
1860  PRECONDITION(expr.id()==ID_complex);
1861  complex_exprt &ret = static_cast<complex_exprt &>(expr);
1862  validate_expr(ret);
1863  return ret;
1864 }
1865 
1868 {
1869 public:
1870  explicit complex_real_exprt(const exprt &op)
1871  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1872  {
1873  }
1874 };
1875 
1876 template <>
1878 {
1879  return base.id() == ID_complex_real;
1880 }
1881 
1882 inline void validate_expr(const complex_real_exprt &expr)
1883 {
1885  expr, 1, "real part retrieval operation must have one operand");
1886 }
1887 
1895 {
1896  PRECONDITION(expr.id() == ID_complex_real);
1897  const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
1898  validate_expr(ret);
1899  return ret;
1900 }
1901 
1904 {
1905  PRECONDITION(expr.id() == ID_complex_real);
1906  complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
1907  validate_expr(ret);
1908  return ret;
1909 }
1910 
1913 {
1914 public:
1915  explicit complex_imag_exprt(const exprt &op)
1916  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
1917  {
1918  }
1919 };
1920 
1921 template <>
1923 {
1924  return base.id() == ID_complex_imag;
1925 }
1926 
1927 inline void validate_expr(const complex_imag_exprt &expr)
1928 {
1930  expr, 1, "imaginary part retrieval operation must have one operand");
1931 }
1932 
1940 {
1941  PRECONDITION(expr.id() == ID_complex_imag);
1942  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
1943  validate_expr(ret);
1944  return ret;
1945 }
1946 
1949 {
1950  PRECONDITION(expr.id() == ID_complex_imag);
1951  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
1952  validate_expr(ret);
1953  return ret;
1954 }
1955 
1956 class namespacet;
1957 
1960 {
1961 public:
1963  : binary_exprt(
1964  exprt(ID_unknown),
1965  ID_object_descriptor,
1966  exprt(ID_unknown),
1967  typet())
1968  {
1969  }
1970 
1971  explicit object_descriptor_exprt(exprt _object)
1972  : binary_exprt(
1973  std::move(_object),
1974  ID_object_descriptor,
1975  exprt(ID_unknown),
1976  typet())
1977  {
1978  }
1979 
1984  void build(const exprt &expr, const namespacet &ns);
1985 
1987  {
1988  return op0();
1989  }
1990 
1991  const exprt &object() const
1992  {
1993  return op0();
1994  }
1995 
1996  const exprt &root_object() const;
1997 
1999  {
2000  return op1();
2001  }
2002 
2003  const exprt &offset() const
2004  {
2005  return op1();
2006  }
2007 };
2008 
2009 template <>
2011 {
2012  return base.id() == ID_object_descriptor;
2013 }
2014 
2015 inline void validate_expr(const object_descriptor_exprt &value)
2016 {
2017  validate_operands(value, 2, "Object descriptor must have two operands");
2018 }
2019 
2027  const exprt &expr)
2028 {
2029  PRECONDITION(expr.id()==ID_object_descriptor);
2030  const object_descriptor_exprt &ret =
2031  static_cast<const object_descriptor_exprt &>(expr);
2032  validate_expr(ret);
2033  return ret;
2034 }
2035 
2038 {
2039  PRECONDITION(expr.id()==ID_object_descriptor);
2040  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
2041  validate_expr(ret);
2042  return ret;
2043 }
2044 
2045 
2048 {
2049 public:
2050  DEPRECATED(SINCE(2019, 2, 11, "use dynamic_object_exprt(type) instead"))
2052  : binary_exprt(exprt(ID_unknown), ID_dynamic_object, exprt(ID_unknown))
2053  {
2054  }
2055 
2057  : binary_exprt(
2058  exprt(ID_unknown),
2059  ID_dynamic_object,
2060  exprt(ID_unknown),
2061  std::move(type))
2062  {
2063  }
2064 
2065  void set_instance(unsigned int instance);
2066 
2067  unsigned int get_instance() const;
2068 
2070  {
2071  return op1();
2072  }
2073 
2074  const exprt &valid() const
2075  {
2076  return op1();
2077  }
2078 };
2079 
2080 template <>
2082 {
2083  return base.id() == ID_dynamic_object;
2084 }
2085 
2086 inline void validate_expr(const dynamic_object_exprt &value)
2087 {
2088  validate_operands(value, 2, "Dynamic object must have two operands");
2089 }
2090 
2098  const exprt &expr)
2099 {
2100  PRECONDITION(expr.id()==ID_dynamic_object);
2101  const dynamic_object_exprt &ret =
2102  static_cast<const dynamic_object_exprt &>(expr);
2103  validate_expr(ret);
2104  return ret;
2105 }
2106 
2109 {
2110  PRECONDITION(expr.id()==ID_dynamic_object);
2111  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
2112  validate_expr(ret);
2113  return ret;
2114 }
2115 
2118 {
2119 public:
2121  {
2122  }
2123 
2125  : unary_predicate_exprt(ID_is_dynamic_object, op)
2126  {
2127  }
2128 };
2129 
2130 inline const is_dynamic_object_exprt &
2132 {
2133  PRECONDITION(expr.id() == ID_is_dynamic_object);
2135  expr.operands().size() == 1, "is_dynamic_object must have one operand");
2136  return static_cast<const is_dynamic_object_exprt &>(expr);
2137 }
2138 
2142 {
2143  PRECONDITION(expr.id() == ID_is_dynamic_object);
2145  expr.operands().size() == 1, "is_dynamic_object must have one operand");
2146  return static_cast<is_dynamic_object_exprt &>(expr);
2147 }
2148 
2151 {
2152 public:
2154  : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2155  {
2156  }
2157 
2158  // returns a typecast if the type doesn't already match
2159  static exprt conditional_cast(const exprt &expr, const typet &type)
2160  {
2161  if(expr.type() == type)
2162  return expr;
2163  else
2164  return typecast_exprt(expr, type);
2165  }
2166 };
2167 
2168 template <>
2169 inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2170 {
2171  return base.id() == ID_typecast;
2172 }
2173 
2174 inline void validate_expr(const typecast_exprt &value)
2175 {
2176  validate_operands(value, 1, "Typecast must have one operand");
2177 }
2178 
2185 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2186 {
2187  PRECONDITION(expr.id()==ID_typecast);
2188  const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
2189  validate_expr(ret);
2190  return ret;
2191 }
2192 
2195 {
2196  PRECONDITION(expr.id()==ID_typecast);
2197  typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
2198  validate_expr(ret);
2199  return ret;
2200 }
2201 
2202 
2205 {
2206 public:
2208  : binary_exprt(
2209  std::move(op),
2210  ID_floatbv_typecast,
2211  std::move(rounding),
2212  std::move(_type))
2213  {
2214  }
2215 
2217  {
2218  return op0();
2219  }
2220 
2221  const exprt &op() const
2222  {
2223  return op0();
2224  }
2225 
2227  {
2228  return op1();
2229  }
2230 
2231  const exprt &rounding_mode() const
2232  {
2233  return op1();
2234  }
2235 };
2236 
2237 template <>
2239 {
2240  return base.id() == ID_floatbv_typecast;
2241 }
2242 
2243 inline void validate_expr(const floatbv_typecast_exprt &value)
2244 {
2245  validate_operands(value, 2, "Float typecast must have two operands");
2246 }
2247 
2255 {
2256  PRECONDITION(expr.id()==ID_floatbv_typecast);
2257  const floatbv_typecast_exprt &ret =
2258  static_cast<const floatbv_typecast_exprt &>(expr);
2259  validate_expr(ret);
2260  return ret;
2261 }
2262 
2265 {
2266  PRECONDITION(expr.id()==ID_floatbv_typecast);
2267  floatbv_typecast_exprt &ret = static_cast<floatbv_typecast_exprt &>(expr);
2268  validate_expr(ret);
2269  return ret;
2270 }
2271 
2272 
2275 {
2276 public:
2277  DEPRECATED(SINCE(2019, 1, 12, "use and_exprt(op, op) instead"))
2279  {
2280  }
2281 
2283  : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2284  {
2285  }
2286 
2288  : multi_ary_exprt(
2289  ID_and,
2290  {std::move(op0), std::move(op1), std::move(op2)},
2291  bool_typet())
2292  {
2293  }
2294 
2296  : multi_ary_exprt(
2297  ID_and,
2298  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2299  bool_typet())
2300  {
2301  }
2302 
2303  explicit and_exprt(exprt::operandst _operands)
2304  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2305  {
2306  }
2307 };
2308 
2312 
2314 
2315 template <>
2316 inline bool can_cast_expr<and_exprt>(const exprt &base)
2317 {
2318  return base.id() == ID_and;
2319 }
2320 
2327 inline const and_exprt &to_and_expr(const exprt &expr)
2328 {
2329  PRECONDITION(expr.id()==ID_and);
2330  return static_cast<const and_exprt &>(expr);
2331 }
2332 
2335 {
2336  PRECONDITION(expr.id()==ID_and);
2337  return static_cast<and_exprt &>(expr);
2338 }
2339 
2340 
2343 {
2344 public:
2346  : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2347  {
2348  }
2349 };
2350 
2351 template <>
2352 inline bool can_cast_expr<implies_exprt>(const exprt &base)
2353 {
2354  return base.id() == ID_implies;
2355 }
2356 
2357 inline void validate_expr(const implies_exprt &value)
2358 {
2359  validate_operands(value, 2, "Implies must have two operands");
2360 }
2361 
2368 inline const implies_exprt &to_implies_expr(const exprt &expr)
2369 {
2370  PRECONDITION(expr.id()==ID_implies);
2371  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2372  validate_expr(ret);
2373  return ret;
2374 }
2375 
2378 {
2379  PRECONDITION(expr.id()==ID_implies);
2380  implies_exprt &ret = static_cast<implies_exprt &>(expr);
2381  validate_expr(ret);
2382  return ret;
2383 }
2384 
2385 
2388 {
2389 public:
2390  DEPRECATED(SINCE(2019, 1, 12, "use or_exprt(op, op) instead"))
2392  {
2393  }
2394 
2396  : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2397  {
2398  }
2399 
2401  : multi_ary_exprt(
2402  ID_or,
2403  {std::move(op0), std::move(op1), std::move(op2)},
2404  bool_typet())
2405  {
2406  }
2407 
2409  : multi_ary_exprt(
2410  ID_or,
2411  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2412  bool_typet())
2413  {
2414  }
2415 
2416  explicit or_exprt(exprt::operandst _operands)
2417  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2418  {
2419  }
2420 };
2421 
2425 
2427 
2428 template <>
2429 inline bool can_cast_expr<or_exprt>(const exprt &base)
2430 {
2431  return base.id() == ID_or;
2432 }
2433 
2440 inline const or_exprt &to_or_expr(const exprt &expr)
2441 {
2442  PRECONDITION(expr.id()==ID_or);
2443  return static_cast<const or_exprt &>(expr);
2444 }
2445 
2447 inline or_exprt &to_or_expr(exprt &expr)
2448 {
2449  PRECONDITION(expr.id()==ID_or);
2450  return static_cast<or_exprt &>(expr);
2451 }
2452 
2453 
2456 {
2457 public:
2458  DEPRECATED(SINCE(2019, 1, 12, "use xor_exprt(op, op) instead"))
2460  {
2461  }
2462 
2463  xor_exprt(exprt _op0, exprt _op1)
2464  : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2465  {
2466  }
2467 };
2468 
2469 template <>
2470 inline bool can_cast_expr<xor_exprt>(const exprt &base)
2471 {
2472  return base.id() == ID_xor;
2473 }
2474 
2481 inline const xor_exprt &to_xor_expr(const exprt &expr)
2482 {
2483  PRECONDITION(expr.id()==ID_xor);
2484  return static_cast<const xor_exprt &>(expr);
2485 }
2486 
2489 {
2490  PRECONDITION(expr.id()==ID_xor);
2491  return static_cast<xor_exprt &>(expr);
2492 }
2493 
2494 
2497 {
2498 public:
2499  explicit bitnot_exprt(exprt op) : unary_exprt(ID_bitnot, std::move(op))
2500  {
2501  }
2502 };
2503 
2504 template <>
2505 inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
2506 {
2507  return base.id() == ID_bitnot;
2508 }
2509 
2510 inline void validate_expr(const bitnot_exprt &value)
2511 {
2512  validate_operands(value, 1, "Bit-wise not must have one operand");
2513 }
2514 
2521 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
2522 {
2523  PRECONDITION(expr.id()==ID_bitnot);
2524  const bitnot_exprt &ret = static_cast<const bitnot_exprt &>(expr);
2525  validate_expr(ret);
2526  return ret;
2527 }
2528 
2531 {
2532  PRECONDITION(expr.id()==ID_bitnot);
2533  bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
2534  validate_expr(ret);
2535  return ret;
2536 }
2537 
2538 
2541 {
2542 public:
2543  bitor_exprt(const exprt &_op0, exprt _op1)
2544  : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
2545  {
2546  }
2547 };
2548 
2549 template <>
2550 inline bool can_cast_expr<bitor_exprt>(const exprt &base)
2551 {
2552  return base.id() == ID_bitor;
2553 }
2554 
2561 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
2562 {
2563  PRECONDITION(expr.id()==ID_bitor);
2564  return static_cast<const bitor_exprt &>(expr);
2565 }
2566 
2569 {
2570  PRECONDITION(expr.id()==ID_bitor);
2571  return static_cast<bitor_exprt &>(expr);
2572 }
2573 
2574 
2577 {
2578 public:
2580  : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
2581  {
2582  }
2583 };
2584 
2585 template <>
2586 inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
2587 {
2588  return base.id() == ID_bitxor;
2589 }
2590 
2597 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
2598 {
2599  PRECONDITION(expr.id()==ID_bitxor);
2600  return static_cast<const bitxor_exprt &>(expr);
2601 }
2602 
2605 {
2606  PRECONDITION(expr.id()==ID_bitxor);
2607  return static_cast<bitxor_exprt &>(expr);
2608 }
2609 
2610 
2613 {
2614 public:
2615  bitand_exprt(const exprt &_op0, exprt _op1)
2616  : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
2617  {
2618  }
2619 };
2620 
2621 template <>
2622 inline bool can_cast_expr<bitand_exprt>(const exprt &base)
2623 {
2624  return base.id() == ID_bitand;
2625 }
2626 
2633 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
2634 {
2635  PRECONDITION(expr.id()==ID_bitand);
2636  return static_cast<const bitand_exprt &>(expr);
2637 }
2638 
2641 {
2642  PRECONDITION(expr.id()==ID_bitand);
2643  return static_cast<bitand_exprt &>(expr);
2644 }
2645 
2646 
2649 {
2650 public:
2651  shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
2652  : binary_exprt(std::move(_src), _id, std::move(_distance))
2653  {
2654  }
2655 
2656  shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
2657 
2659  {
2660  return op0();
2661  }
2662 
2663  const exprt &op() const
2664  {
2665  return op0();
2666  }
2667 
2669  {
2670  return op1();
2671  }
2672 
2673  const exprt &distance() const
2674  {
2675  return op1();
2676  }
2677 };
2678 
2679 template <>
2680 inline bool can_cast_expr<shift_exprt>(const exprt &base)
2681 {
2682  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr;
2683 }
2684 
2685 inline void validate_expr(const shift_exprt &value)
2686 {
2687  validate_operands(value, 2, "Shifts must have two operands");
2688 }
2689 
2696 inline const shift_exprt &to_shift_expr(const exprt &expr)
2697 {
2698  const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
2699  validate_expr(ret);
2700  return ret;
2701 }
2702 
2705 {
2706  shift_exprt &ret = static_cast<shift_exprt &>(expr);
2707  validate_expr(ret);
2708  return ret;
2709 }
2710 
2711 
2714 {
2715 public:
2716  shl_exprt(exprt _src, exprt _distance)
2717  : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
2718  {
2719  }
2720 
2721  shl_exprt(exprt _src, const std::size_t _distance)
2722  : shift_exprt(std::move(_src), ID_shl, _distance)
2723  {
2724  }
2725 };
2726 
2733 inline const shl_exprt &to_shl_expr(const exprt &expr)
2734 {
2735  PRECONDITION(expr.id() == ID_shl);
2736  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
2737  validate_expr(ret);
2738  return ret;
2739 }
2740 
2743 {
2744  PRECONDITION(expr.id() == ID_shl);
2745  shl_exprt &ret = static_cast<shl_exprt &>(expr);
2746  validate_expr(ret);
2747  return ret;
2748 }
2749 
2752 {
2753 public:
2754  ashr_exprt(exprt _src, exprt _distance)
2755  : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
2756  {
2757  }
2758 
2759  ashr_exprt(exprt _src, const std::size_t _distance)
2760  : shift_exprt(std::move(_src), ID_ashr, _distance)
2761  {
2762  }
2763 };
2764 
2767 {
2768 public:
2769  lshr_exprt(exprt _src, exprt _distance)
2770  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2771  {
2772  }
2773 
2774  lshr_exprt(exprt _src, const std::size_t _distance)
2775  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2776  {
2777  }
2778 };
2779 
2782 {
2783 public:
2786  : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
2787  {
2788  }
2789 
2790  extractbit_exprt(exprt _src, const std::size_t _index);
2791 
2793  {
2794  return op0();
2795  }
2796 
2798  {
2799  return op1();
2800  }
2801 
2802  const exprt &src() const
2803  {
2804  return op0();
2805  }
2806 
2807  const exprt &index() const
2808  {
2809  return op1();
2810  }
2811 };
2812 
2813 template <>
2814 inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
2815 {
2816  return base.id() == ID_extractbit;
2817 }
2818 
2819 inline void validate_expr(const extractbit_exprt &value)
2820 {
2821  validate_operands(value, 2, "Extract bit must have two operands");
2822 }
2823 
2830 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
2831 {
2832  PRECONDITION(expr.id()==ID_extractbit);
2833  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
2834  validate_expr(ret);
2835  return ret;
2836 }
2837 
2840 {
2841  PRECONDITION(expr.id()==ID_extractbit);
2842  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
2843  validate_expr(ret);
2844  return ret;
2845 }
2846 
2847 
2850 {
2851 public:
2857  extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
2858  : expr_protectedt(
2859  ID_extractbits,
2860  std::move(_type),
2861  {std::move(_src), std::move(_upper), std::move(_lower)})
2862  {
2863  }
2864 
2866  exprt _src,
2867  const std::size_t _upper,
2868  const std::size_t _lower,
2869  typet _type);
2870 
2872  {
2873  return op0();
2874  }
2875 
2877  {
2878  return op1();
2879  }
2880 
2882  {
2883  return op2();
2884  }
2885 
2886  const exprt &src() const
2887  {
2888  return op0();
2889  }
2890 
2891  const exprt &upper() const
2892  {
2893  return op1();
2894  }
2895 
2896  const exprt &lower() const
2897  {
2898  return op2();
2899  }
2900 };
2901 
2902 template <>
2903 inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
2904 {
2905  return base.id() == ID_extractbits;
2906 }
2907 
2908 inline void validate_expr(const extractbits_exprt &value)
2909 {
2910  validate_operands(value, 3, "Extract bits must have three operands");
2911 }
2912 
2919 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
2920 {
2921  PRECONDITION(expr.id()==ID_extractbits);
2922  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
2923  validate_expr(ret);
2924  return ret;
2925 }
2926 
2929 {
2930  PRECONDITION(expr.id()==ID_extractbits);
2931  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
2932  validate_expr(ret);
2933  return ret;
2934 }
2935 
2936 
2939 {
2940 public:
2941  explicit address_of_exprt(const exprt &op);
2942 
2944  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
2945  {
2946  }
2947 
2949  {
2950  return op0();
2951  }
2952 
2953  const exprt &object() const
2954  {
2955  return op0();
2956  }
2957 };
2958 
2959 template <>
2960 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
2961 {
2962  return base.id() == ID_address_of;
2963 }
2964 
2965 inline void validate_expr(const address_of_exprt &value)
2966 {
2967  validate_operands(value, 1, "Address of must have one operand");
2968 }
2969 
2976 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
2977 {
2978  PRECONDITION(expr.id()==ID_address_of);
2979  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
2980  validate_expr(ret);
2981  return ret;
2982 }
2983 
2986 {
2987  PRECONDITION(expr.id()==ID_address_of);
2988  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
2989  validate_expr(ret);
2990  return ret;
2991 }
2992 
2993 
2996 {
2997 public:
2998  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2999  {
3000  PRECONDITION(as_const(*this).op().type().id() == ID_bool);
3001  }
3002 
3003  DEPRECATED(SINCE(2019, 1, 12, "use not_exprt(op) instead"))
3005  {
3006  }
3007 };
3008 
3009 template <>
3010 inline bool can_cast_expr<not_exprt>(const exprt &base)
3011 {
3012  return base.id() == ID_not;
3013 }
3014 
3015 inline void validate_expr(const not_exprt &value)
3016 {
3017  validate_operands(value, 1, "Not must have one operand");
3018 }
3019 
3026 inline const not_exprt &to_not_expr(const exprt &expr)
3027 {
3028  PRECONDITION(expr.id()==ID_not);
3029  const not_exprt &ret = static_cast<const not_exprt &>(expr);
3030  validate_expr(ret);
3031  return ret;
3032 }
3033 
3036 {
3037  PRECONDITION(expr.id()==ID_not);
3038  not_exprt &ret = static_cast<not_exprt &>(expr);
3039  validate_expr(ret);
3040  return ret;
3041 }
3042 
3043 
3046 {
3047 public:
3048  explicit dereference_exprt(const exprt &op):
3049  unary_exprt(ID_dereference, op, op.type().subtype())
3050  {
3051  PRECONDITION(op.type().id()==ID_pointer);
3052  }
3053 
3055  : unary_exprt(ID_dereference, std::move(op), std::move(type))
3056  {
3057  }
3058 
3060  {
3061  return op0();
3062  }
3063 
3064  const exprt &pointer() const
3065  {
3066  return op0();
3067  }
3068 
3069  static void check(
3070  const exprt &expr,
3072  {
3073  DATA_CHECK(
3074  vm,
3075  expr.operands().size() == 1,
3076  "dereference expression must have one operand");
3077  }
3078 
3079  static void validate(
3080  const exprt &expr,
3081  const namespacet &ns,
3083 };
3084 
3085 template <>
3086 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
3087 {
3088  return base.id() == ID_dereference;
3089 }
3090 
3091 inline void validate_expr(const dereference_exprt &value)
3092 {
3093  validate_operands(value, 1, "Dereference must have one operand");
3094 }
3095 
3102 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
3103 {
3104  PRECONDITION(expr.id()==ID_dereference);
3105  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
3106  validate_expr(ret);
3107  return ret;
3108 }
3109 
3112 {
3113  PRECONDITION(expr.id()==ID_dereference);
3114  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
3115  validate_expr(ret);
3116  return ret;
3117 }
3118 
3119 
3121 class if_exprt : public ternary_exprt
3122 {
3123 public:
3125  : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
3126  {
3127  }
3128 
3130  : ternary_exprt(
3131  ID_if,
3132  std::move(cond),
3133  std::move(t),
3134  std::move(f),
3135  std::move(type))
3136  {
3137  }
3138 
3140  {
3141  return op0();
3142  }
3143 
3144  const exprt &cond() const
3145  {
3146  return op0();
3147  }
3148 
3150  {
3151  return op1();
3152  }
3153 
3154  const exprt &true_case() const
3155  {
3156  return op1();
3157  }
3158 
3160  {
3161  return op2();
3162  }
3163 
3164  const exprt &false_case() const
3165  {
3166  return op2();
3167  }
3168 };
3169 
3170 template <>
3171 inline bool can_cast_expr<if_exprt>(const exprt &base)
3172 {
3173  return base.id() == ID_if;
3174 }
3175 
3176 inline void validate_expr(const if_exprt &value)
3177 {
3178  validate_operands(value, 3, "If-then-else must have three operands");
3179 }
3180 
3187 inline const if_exprt &to_if_expr(const exprt &expr)
3188 {
3189  PRECONDITION(expr.id()==ID_if);
3190  const if_exprt &ret = static_cast<const if_exprt &>(expr);
3191  validate_expr(ret);
3192  return ret;
3193 }
3194 
3196 inline if_exprt &to_if_expr(exprt &expr)
3197 {
3198  PRECONDITION(expr.id()==ID_if);
3199  if_exprt &ret = static_cast<if_exprt &>(expr);
3200  validate_expr(ret);
3201  return ret;
3202 }
3203 
3208 {
3209 public:
3210  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
3211  : expr_protectedt(
3212  ID_with,
3213  _old.type(),
3214  {_old, std::move(_where), std::move(_new_value)})
3215  {
3216  }
3217 
3219  {
3220  return op0();
3221  }
3222 
3223  const exprt &old() const
3224  {
3225  return op0();
3226  }
3227 
3229  {
3230  return op1();
3231  }
3232 
3233  const exprt &where() const
3234  {
3235  return op1();
3236  }
3237 
3239  {
3240  return op2();
3241  }
3242 
3243  const exprt &new_value() const
3244  {
3245  return op2();
3246  }
3247 };
3248 
3249 template <>
3250 inline bool can_cast_expr<with_exprt>(const exprt &base)
3251 {
3252  return base.id() == ID_with;
3253 }
3254 
3255 inline void validate_expr(const with_exprt &value)
3256 {
3258  value, 3, "array/structure update must have at least 3 operands", true);
3260  value.operands().size() % 2 == 1,
3261  "array/structure update must have an odd number of operands");
3262 }
3263 
3270 inline const with_exprt &to_with_expr(const exprt &expr)
3271 {
3272  PRECONDITION(expr.id()==ID_with);
3273  const with_exprt &ret = static_cast<const with_exprt &>(expr);
3274  validate_expr(ret);
3275  return ret;
3276 }
3277 
3280 {
3281  PRECONDITION(expr.id()==ID_with);
3282  with_exprt &ret = static_cast<with_exprt &>(expr);
3283  validate_expr(ret);
3284  return ret;
3285 }
3286 
3288 {
3289 public:
3290  explicit index_designatort(exprt _index)
3291  : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
3292  {
3293  }
3294 
3295  const exprt &index() const
3296  {
3297  return op0();
3298  }
3299 
3301  {
3302  return op0();
3303  }
3304 };
3305 
3306 template <>
3307 inline bool can_cast_expr<index_designatort>(const exprt &base)
3308 {
3309  return base.id() == ID_index_designator;
3310 }
3311 
3312 inline void validate_expr(const index_designatort &value)
3313 {
3314  validate_operands(value, 1, "Index designator must have one operand");
3315 }
3316 
3323 inline const index_designatort &to_index_designator(const exprt &expr)
3324 {
3325  PRECONDITION(expr.id()==ID_index_designator);
3326  const index_designatort &ret = static_cast<const index_designatort &>(expr);
3327  validate_expr(ret);
3328  return ret;
3329 }
3330 
3333 {
3334  PRECONDITION(expr.id()==ID_index_designator);
3335  index_designatort &ret = static_cast<index_designatort &>(expr);
3336  validate_expr(ret);
3337  return ret;
3338 }
3339 
3341 {
3342 public:
3343  explicit member_designatort(const irep_idt &_component_name)
3344  : expr_protectedt(ID_member_designator, typet())
3345  {
3346  set(ID_component_name, _component_name);
3347  }
3348 
3350  {
3351  return get(ID_component_name);
3352  }
3353 };
3354 
3355 template <>
3357 {
3358  return base.id() == ID_member_designator;
3359 }
3360 
3361 inline void validate_expr(const member_designatort &value)
3362 {
3363  validate_operands(value, 0, "Member designator must not have operands");
3364 }
3365 
3373 {
3374  PRECONDITION(expr.id()==ID_member_designator);
3375  const member_designatort &ret = static_cast<const member_designatort &>(expr);
3376  validate_expr(ret);
3377  return ret;
3378 }
3379 
3382 {
3383  PRECONDITION(expr.id()==ID_member_designator);
3384  member_designatort &ret = static_cast<member_designatort &>(expr);
3385  validate_expr(ret);
3386  return ret;
3387 }
3388 
3389 
3392 {
3393 public:
3394  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
3395  : ternary_exprt(
3396  ID_update,
3397  _old,
3398  std::move(_designator),
3399  std::move(_new_value),
3400  _old.type())
3401  {
3402  }
3403 
3405  {
3406  return op0();
3407  }
3408 
3409  const exprt &old() const
3410  {
3411  return op0();
3412  }
3413 
3414  // the designator operands are either
3415  // 1) member_designator or
3416  // 2) index_designator
3417  // as defined above
3419  {
3420  return op1().operands();
3421  }
3422 
3424  {
3425  return op1().operands();
3426  }
3427 
3429  {
3430  return op2();
3431  }
3432 
3433  const exprt &new_value() const
3434  {
3435  return op2();
3436  }
3437 };
3438 
3439 template <>
3440 inline bool can_cast_expr<update_exprt>(const exprt &base)
3441 {
3442  return base.id() == ID_update;
3443 }
3444 
3445 inline void validate_expr(const update_exprt &value)
3446 {
3448  value, 3, "Array/structure update must have three operands");
3449 }
3450 
3457 inline const update_exprt &to_update_expr(const exprt &expr)
3458 {
3459  PRECONDITION(expr.id()==ID_update);
3460  const update_exprt &ret = static_cast<const update_exprt &>(expr);
3461  validate_expr(ret);
3462  return ret;
3463 }
3464 
3467 {
3468  PRECONDITION(expr.id()==ID_update);
3469  update_exprt &ret = static_cast<update_exprt &>(expr);
3470  validate_expr(ret);
3471  return ret;
3472 }
3473 
3474 
3475 #if 0
3476 class array_update_exprt:public expr_protectedt
3478 {
3479 public:
3480  array_update_exprt(
3481  const exprt &_array,
3482  const exprt &_index,
3483  const exprt &_new_value):
3484  exprt(ID_array_update, _array.type())
3485  {
3486  add_to_operands(_array, _index, _new_value);
3487  }
3488 
3489  array_update_exprt():expr_protectedt(ID_array_update)
3490  {
3491  operands().resize(3);
3492  }
3493 
3494  exprt &array()
3495  {
3496  return op0();
3497  }
3498 
3499  const exprt &array() const
3500  {
3501  return op0();
3502  }
3503 
3504  exprt &index()
3505  {
3506  return op1();
3507  }
3508 
3509  const exprt &index() const
3510  {
3511  return op1();
3512  }
3513 
3514  exprt &new_value()
3515  {
3516  return op2();
3517  }
3518 
3519  const exprt &new_value() const
3520  {
3521  return op2();
3522  }
3523 };
3524 
3525 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
3526 {
3527  return base.id()==ID_array_update;
3528 }
3529 
3530 inline void validate_expr(const array_update_exprt &value)
3531 {
3532  validate_operands(value, 3, "Array update must have three operands");
3533 }
3534 
3541 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3542 {
3543  PRECONDITION(expr.id()==ID_array_update);
3544  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
3545  validate_expr(ret);
3546  return ret;
3547 }
3548 
3550 inline array_update_exprt &to_array_update_expr(exprt &expr)
3551 {
3552  PRECONDITION(expr.id()==ID_array_update);
3553  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
3554  validate_expr(ret);
3555  return ret;
3556 }
3557 
3558 #endif
3559 
3560 
3563 {
3564 public:
3565  member_exprt(exprt op, const irep_idt &component_name, typet _type)
3566  : unary_exprt(ID_member, std::move(op), std::move(_type))
3567  {
3568  set_component_name(component_name);
3569  }
3570 
3572  : unary_exprt(ID_member, std::move(op), c.type())
3573  {
3575  }
3576 
3578  {
3579  return get(ID_component_name);
3580  }
3581 
3582  void set_component_name(const irep_idt &component_name)
3583  {
3584  set(ID_component_name, component_name);
3585  }
3586 
3587  std::size_t get_component_number() const
3588  {
3589  return get_size_t(ID_component_number);
3590  }
3591 
3592  // will go away, use compound()
3593  const exprt &struct_op() const
3594  {
3595  return op0();
3596  }
3597 
3598  // will go away, use compound()
3600  {
3601  return op0();
3602  }
3603 
3604  const exprt &compound() const
3605  {
3606  return op0();
3607  }
3608 
3610  {
3611  return op0();
3612  }
3613 
3614  static void check(
3615  const exprt &expr,
3617  {
3618  DATA_CHECK(
3619  vm,
3620  expr.operands().size() == 1,
3621  "member expression must have one operand");
3622  }
3623 
3624  static void validate(
3625  const exprt &expr,
3626  const namespacet &ns,
3628 };
3629 
3630 template <>
3631 inline bool can_cast_expr<member_exprt>(const exprt &base)
3632 {
3633  return base.id() == ID_member;
3634 }
3635 
3636 inline void validate_expr(const member_exprt &value)
3637 {
3638  validate_operands(value, 1, "Extract member must have one operand");
3639 }
3640 
3647 inline const member_exprt &to_member_expr(const exprt &expr)
3648 {
3649  PRECONDITION(expr.id()==ID_member);
3650  const member_exprt &ret = static_cast<const member_exprt &>(expr);
3651  validate_expr(ret);
3652  return ret;
3653 }
3654 
3657 {
3658  PRECONDITION(expr.id()==ID_member);
3659  member_exprt &ret = static_cast<member_exprt &>(expr);
3660  validate_expr(ret);
3661  return ret;
3662 }
3663 
3664 
3667 {
3668 public:
3670  : unary_predicate_exprt(ID_isnan, std::move(op))
3671  {
3672  }
3673 
3674  DEPRECATED(SINCE(2018, 12, 2, "use isnan_exprt(op) instead"))
3676  {
3677  }
3678 };
3679 
3680 template <>
3681 inline bool can_cast_expr<isnan_exprt>(const exprt &base)
3682 {
3683  return base.id() == ID_isnan;
3684 }
3685 
3686 inline void validate_expr(const isnan_exprt &value)
3687 {
3688  validate_operands(value, 1, "Is NaN must have one operand");
3689 }
3690 
3697 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
3698 {
3699  PRECONDITION(expr.id()==ID_isnan);
3700  const isnan_exprt &ret = static_cast<const isnan_exprt &>(expr);
3701  validate_expr(ret);
3702  return ret;
3703 }
3704 
3707 {
3708  PRECONDITION(expr.id()==ID_isnan);
3709  isnan_exprt &ret = static_cast<isnan_exprt &>(expr);
3710  validate_expr(ret);
3711  return ret;
3712 }
3713 
3714 
3717 {
3718 public:
3720  : unary_predicate_exprt(ID_isinf, std::move(op))
3721  {
3722  }
3723 
3724  DEPRECATED(SINCE(2018, 12, 2, "use isinf_exprt(op) instead"))
3726  {
3727  }
3728 };
3729 
3730 template <>
3731 inline bool can_cast_expr<isinf_exprt>(const exprt &base)
3732 {
3733  return base.id() == ID_isinf;
3734 }
3735 
3736 inline void validate_expr(const isinf_exprt &value)
3737 {
3738  validate_operands(value, 1, "Is infinite must have one operand");
3739 }
3740 
3747 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
3748 {
3749  PRECONDITION(expr.id()==ID_isinf);
3750  const isinf_exprt &ret = static_cast<const isinf_exprt &>(expr);
3751  validate_expr(ret);
3752  return ret;
3753 }
3754 
3757 {
3758  PRECONDITION(expr.id()==ID_isinf);
3759  isinf_exprt &ret = static_cast<isinf_exprt &>(expr);
3760  validate_expr(ret);
3761  return ret;
3762 }
3763 
3764 
3767 {
3768 public:
3770  : unary_predicate_exprt(ID_isfinite, std::move(op))
3771  {
3772  }
3773 
3774  DEPRECATED(SINCE(2018, 12, 2, "use isfinite_exprt(op) instead"))
3776  {
3777  }
3778 };
3779 
3780 template <>
3781 inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
3782 {
3783  return base.id() == ID_isfinite;
3784 }
3785 
3786 inline void validate_expr(const isfinite_exprt &value)
3787 {
3788  validate_operands(value, 1, "Is finite must have one operand");
3789 }
3790 
3797 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
3798 {
3799  PRECONDITION(expr.id()==ID_isfinite);
3800  const isfinite_exprt &ret = static_cast<const isfinite_exprt &>(expr);
3801  validate_expr(ret);
3802  return ret;
3803 }
3804 
3807 {
3808  PRECONDITION(expr.id()==ID_isfinite);
3809  isfinite_exprt &ret = static_cast<isfinite_exprt &>(expr);
3810  validate_expr(ret);
3811  return ret;
3812 }
3813 
3814 
3817 {
3818 public:
3820  : unary_predicate_exprt(ID_isnormal, std::move(op))
3821  {
3822  }
3823 
3824  DEPRECATED(SINCE(2018, 12, 2, "use isnormal_exprt(op) instead"))
3826  {
3827  }
3828 };
3829 
3830 template <>
3831 inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
3832 {
3833  return base.id() == ID_isnormal;
3834 }
3835 
3836 inline void validate_expr(const isnormal_exprt &value)
3837 {
3838  validate_operands(value, 1, "Is normal must have one operand");
3839 }
3840 
3847 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
3848 {
3849  PRECONDITION(expr.id()==ID_isnormal);
3850  const isnormal_exprt &ret = static_cast<const isnormal_exprt &>(expr);
3851  validate_expr(ret);
3852  return ret;
3853 }
3854 
3857 {
3858  PRECONDITION(expr.id()==ID_isnormal);
3859  isnormal_exprt &ret = static_cast<isnormal_exprt &>(expr);
3860  validate_expr(ret);
3861  return ret;
3862 }
3863 
3864 
3867 {
3868 public:
3869  DEPRECATED(SINCE(2018, 12, 2, "use ieee_float_equal_exprt(lhs, rhs) instead"))
3871  {
3872  }
3873 
3876  std::move(_lhs),
3877  ID_ieee_float_equal,
3878  std::move(_rhs))
3879  {
3880  }
3881 };
3882 
3883 template <>
3885 {
3886  return base.id() == ID_ieee_float_equal;
3887 }
3888 
3889 inline void validate_expr(const ieee_float_equal_exprt &value)
3890 {
3891  validate_operands(value, 2, "IEEE equality must have two operands");
3892 }
3893 
3901 {
3902  PRECONDITION(expr.id()==ID_ieee_float_equal);
3903  const ieee_float_equal_exprt &ret =
3904  static_cast<const ieee_float_equal_exprt &>(expr);
3905  validate_expr(ret);
3906  return ret;
3907 }
3908 
3911 {
3912  PRECONDITION(expr.id()==ID_ieee_float_equal);
3913  ieee_float_equal_exprt &ret = static_cast<ieee_float_equal_exprt &>(expr);
3914  validate_expr(ret);
3915  return ret;
3916 }
3917 
3918 
3921 {
3922 public:
3923  DEPRECATED(
3924  SINCE(2018, 12, 2, "use ieee_float_notequal_exprt(lhs, rhs) instead"))
3926  binary_relation_exprt(ID_ieee_float_notequal)
3927  {
3928  }
3929 
3932  std::move(_lhs),
3933  ID_ieee_float_notequal,
3934  std::move(_rhs))
3935  {
3936  }
3937 };
3938 
3939 template <>
3941 {
3942  return base.id() == ID_ieee_float_notequal;
3943 }
3944 
3945 inline void validate_expr(const ieee_float_notequal_exprt &value)
3946 {
3947  validate_operands(value, 2, "IEEE inequality must have two operands");
3948 }
3949 
3957  const exprt &expr)
3958 {
3959  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3960  const ieee_float_notequal_exprt &ret =
3961  static_cast<const ieee_float_notequal_exprt &>(expr);
3962  validate_expr(ret);
3963  return ret;
3964 }
3965 
3968 {
3969  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3971  static_cast<ieee_float_notequal_exprt &>(expr);
3972  validate_expr(ret);
3973  return ret;
3974 }
3975 
3980 {
3981 public:
3983  const exprt &_lhs,
3984  const irep_idt &_id,
3985  exprt _rhs,
3986  exprt _rm)
3987  : ternary_exprt(_id, _lhs, std::move(_rhs), std::move(_rm), _lhs.type())
3988  {
3989  }
3990 
3992  {
3993  return op0();
3994  }
3995 
3996  const exprt &lhs() const
3997  {
3998  return op0();
3999  }
4000 
4002  {
4003  return op1();
4004  }
4005 
4006  const exprt &rhs() const
4007  {
4008  return op1();
4009  }
4010 
4012  {
4013  return op2();
4014  }
4015 
4016  const exprt &rounding_mode() const
4017  {
4018  return op2();
4019  }
4020 };
4021 
4022 template <>
4024 {
4025  return base.id() == ID_floatbv_plus || base.id() == ID_floatbv_minus ||
4026  base.id() == ID_floatbv_div || base.id() == ID_floatbv_mult;
4027 }
4028 
4029 inline void validate_expr(const ieee_float_op_exprt &value)
4030 {
4032  value, 3, "IEEE float operations must have three arguments");
4033 }
4034 
4042 {
4043  const ieee_float_op_exprt &ret =
4044  static_cast<const ieee_float_op_exprt &>(expr);
4045  validate_expr(ret);
4046  return ret;
4047 }
4048 
4051 {
4052  ieee_float_op_exprt &ret = static_cast<ieee_float_op_exprt &>(expr);
4053  validate_expr(ret);
4054  return ret;
4055 }
4056 
4057 
4060 {
4061 public:
4062  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
4063  {
4064  }
4065 };
4066 
4067 template <>
4068 inline bool can_cast_expr<type_exprt>(const exprt &base)
4069 {
4070  return base.id() == ID_type;
4071 }
4072 
4079 inline const type_exprt &to_type_expr(const exprt &expr)
4080 {
4082  const type_exprt &ret = static_cast<const type_exprt &>(expr);
4083  return ret;
4084 }
4085 
4088 {
4090  type_exprt &ret = static_cast<type_exprt &>(expr);
4091  return ret;
4092 }
4093 
4096 {
4097 public:
4098  constant_exprt(const irep_idt &_value, typet _type)
4099  : expr_protectedt(ID_constant, std::move(_type))
4100  {
4101  set_value(_value);
4102  }
4103 
4104  const irep_idt &get_value() const
4105  {
4106  return get(ID_value);
4107  }
4108 
4109  void set_value(const irep_idt &value)
4110  {
4111  set(ID_value, value);
4112  }
4113 
4114  bool value_is_zero_string() const;
4115 };
4116 
4117 template <>
4118 inline bool can_cast_expr<constant_exprt>(const exprt &base)
4119 {
4120  return base.id() == ID_constant;
4121 }
4122 
4129 inline const constant_exprt &to_constant_expr(const exprt &expr)
4130 {
4131  PRECONDITION(expr.id()==ID_constant);
4132  return static_cast<const constant_exprt &>(expr);
4133 }
4134 
4137 {
4138  PRECONDITION(expr.id()==ID_constant);
4139  return static_cast<constant_exprt &>(expr);
4140 }
4141 
4142 
4145 {
4146 public:
4148  {
4149  }
4150 };
4151 
4154 {
4155 public:
4157  {
4158  }
4159 };
4160 
4162 class nil_exprt : public nullary_exprt
4163 {
4164 public:
4166  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
4167  {
4168  }
4169 };
4170 
4171 template <>
4172 inline bool can_cast_expr<nil_exprt>(const exprt &base)
4173 {
4174  return base.id() == ID_nil;
4175 }
4176 
4179 {
4180 public:
4182  : constant_exprt(ID_NULL, std::move(type))
4183  {
4184  }
4185 };
4186 
4189 {
4190 public:
4191  replication_exprt(const constant_exprt &_times, const exprt &_src)
4192  : binary_exprt(_times, ID_replication, _src)
4193  {
4194  }
4195 
4197  {
4198  return static_cast<constant_exprt &>(op0());
4199  }
4200 
4201  const constant_exprt &times() const
4202  {
4203  return static_cast<const constant_exprt &>(op0());
4204  }
4205 
4207  {
4208  return op1();
4209  }
4210 
4211  const exprt &op() const
4212  {
4213  return op1();
4214  }
4215 };
4216 
4217 template <>
4218 inline bool can_cast_expr<replication_exprt>(const exprt &base)
4219 {
4220  return base.id() == ID_replication;
4221 }
4222 
4223 inline void validate_expr(const replication_exprt &value)
4224 {
4225  validate_operands(value, 2, "Bit-wise replication must have two operands");
4226 }
4227 
4234 inline const replication_exprt &to_replication_expr(const exprt &expr)
4235 {
4236  PRECONDITION(expr.id() == ID_replication);
4237  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
4238  validate_expr(ret);
4239  return ret;
4240 }
4241 
4244 {
4245  PRECONDITION(expr.id() == ID_replication);
4246  replication_exprt &ret = static_cast<replication_exprt &>(expr);
4247  validate_expr(ret);
4248  return ret;
4249 }
4250 
4257 {
4258 public:
4260  : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
4261  {
4262  }
4263 
4265  : multi_ary_exprt(
4266  ID_concatenation,
4267  {std::move(_op0), std::move(_op1)},
4268  std::move(_type))
4269  {
4270  }
4271 };
4272 
4273 template <>
4275 {
4276  return base.id() == ID_concatenation;
4277 }
4278 
4286 {
4287  PRECONDITION(expr.id()==ID_concatenation);
4288  return static_cast<const concatenation_exprt &>(expr);
4289 }
4290 
4293 {
4294  PRECONDITION(expr.id()==ID_concatenation);
4295  return static_cast<concatenation_exprt &>(expr);
4296 }
4297 
4298 
4301 {
4302 public:
4303  explicit infinity_exprt(typet _type)
4304  : nullary_exprt(ID_infinity, std::move(_type))
4305  {
4306  }
4307 };
4308 
4310 class let_exprt : public ternary_exprt
4311 {
4312 public:
4314  : ternary_exprt(
4315  ID_let,
4316  std::move(symbol),
4317  std::move(value),
4318  where,
4319  where.type())
4320  {
4321  }
4322 
4324  {
4325  return static_cast<symbol_exprt &>(op0());
4326  }
4327 
4328  const symbol_exprt &symbol() const
4329  {
4330  return static_cast<const symbol_exprt &>(op0());
4331  }
4332 
4334  {
4335  return op1();
4336  }
4337 
4338  const exprt &value() const
4339  {
4340  return op1();
4341  }
4342 
4344  {
4345  return op2();
4346  }
4347 
4348  const exprt &where() const
4349  {
4350  return op2();
4351  }
4352 };
4353 
4354 template <>
4355 inline bool can_cast_expr<let_exprt>(const exprt &base)
4356 {
4357  return base.id() == ID_let;
4358 }
4359 
4360 inline void validate_expr(const let_exprt &value)
4361 {
4362  validate_operands(value, 3, "Let must have three operands");
4363 }
4364 
4371 inline const let_exprt &to_let_expr(const exprt &expr)
4372 {
4373  PRECONDITION(expr.id()==ID_let);
4374  const let_exprt &ret = static_cast<const let_exprt &>(expr);
4375  validate_expr(ret);
4376  return ret;
4377 }
4378 
4381 {
4382  PRECONDITION(expr.id()==ID_let);
4383  let_exprt &ret = static_cast<let_exprt &>(expr);
4384  validate_expr(ret);
4385  return ret;
4386 }
4387 
4390 {
4391 public:
4393  : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
4394  {
4395  }
4396 
4397  explicit popcount_exprt(const exprt &_op)
4398  : unary_exprt(ID_popcount, _op, _op.type())
4399  {
4400  }
4401 };
4402 
4403 template <>
4404 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
4405 {
4406  return base.id() == ID_popcount;
4407 }
4408 
4409 inline void validate_expr(const popcount_exprt &value)
4410 {
4411  validate_operands(value, 1, "popcount must have one operand");
4412 }
4413 
4420 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
4421 {
4422  PRECONDITION(expr.id() == ID_popcount);
4423  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
4424  validate_expr(ret);
4425  return ret;
4426 }
4427 
4430 {
4431  PRECONDITION(expr.id() == ID_popcount);
4432  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
4433  validate_expr(ret);
4434  return ret;
4435 }
4436 
4441 {
4442 public:
4443  DEPRECATED(SINCE(2019, 1, 12, "use cond_exprt(operands, type) instead"))
4444  explicit cond_exprt(const typet &_type) : multi_ary_exprt(ID_cond, _type)
4445  {
4446  }
4447 
4448  cond_exprt(operandst _operands, typet _type)
4449  : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
4450  {
4451  }
4452 
4456  void add_case(const exprt &condition, const exprt &value)
4457  {
4458  PRECONDITION(condition.type().id() == ID_bool);
4459  operands().reserve(operands().size() + 2);
4460  operands().push_back(condition);
4461  operands().push_back(value);
4462  }
4463 };
4464 
4465 template <>
4466 inline bool can_cast_expr<cond_exprt>(const exprt &base)
4467 {
4468  return base.id() == ID_cond;
4469 }
4470 
4471 inline void validate_expr(const cond_exprt &value)
4472 {
4474  value.operands().size() % 2 == 0, "cond must have even number of operands");
4475 }
4476 
4483 inline const cond_exprt &to_cond_expr(const exprt &expr)
4484 {
4485  PRECONDITION(expr.id() == ID_cond);
4486  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
4487  validate_expr(ret);
4488  return ret;
4489 }
4490 
4493 {
4494  PRECONDITION(expr.id() == ID_cond);
4495  cond_exprt &ret = static_cast<cond_exprt &>(expr);
4496  validate_expr(ret);
4497  return ret;
4498 }
4499 
4509 {
4510 public:
4512  symbol_exprt arg,
4513  exprt body,
4514  array_typet _type)
4515  : binary_exprt(
4516  std::move(arg),
4517  ID_array_comprehension,
4518  std::move(body),
4519  std::move(_type))
4520  {
4521  }
4522 
4523  const array_typet &type() const
4524  {
4525  return static_cast<const array_typet &>(binary_exprt::type());
4526  }
4527 
4529  {
4530  return static_cast<array_typet &>(binary_exprt::type());
4531  }
4532 
4533  const symbol_exprt &arg() const
4534  {
4535  return static_cast<const symbol_exprt &>(op0());
4536  }
4537 
4539  {
4540  return static_cast<symbol_exprt &>(op0());
4541  }
4542 
4543  const exprt &body() const
4544  {
4545  return op1();
4546  }
4547 
4549  {
4550  return op1();
4551  }
4552 };
4553 
4554 template <>
4556 {
4557  return base.id() == ID_array_comprehension;
4558 }
4559 
4560 inline void validate_expr(const array_comprehension_exprt &value)
4561 {
4562  validate_operands(value, 2, "'Array comprehension' must have two operands");
4563 }
4564 
4571 inline const array_comprehension_exprt &
4573 {
4574  PRECONDITION(expr.id() == ID_array_comprehension);
4575  const array_comprehension_exprt &ret =
4576  static_cast<const array_comprehension_exprt &>(expr);
4577  validate_expr(ret);
4578  return ret;
4579 }
4580 
4583 {
4584  PRECONDITION(expr.id() == ID_array_comprehension);
4586  static_cast<array_comprehension_exprt &>(expr);
4587  validate_expr(ret);
4588  return ret;
4589 }
4590 
4591 #endif // CPROVER_UTIL_STD_EXPR_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3207
index_exprt::array
const exprt & array() const
Definition: std_expr.h:1419
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4420
exprt::op2
exprt & op2()
Definition: expr.h:103
dynamic_object_exprt::dynamic_object_exprt
dynamic_object_exprt(typet type)
Definition: std_expr.h:2056
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
if_exprt::if_exprt
if_exprt(exprt cond, const exprt &t, exprt f)
Definition: std_expr.h:3124
can_cast_expr< symbol_exprt >
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:168
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:4572
to_vector_expr
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1674
can_cast_expr< union_exprt >
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1720
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3457
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2159
can_cast_expr< rem_exprt >
bool can_cast_expr< rem_exprt >(const exprt &base)
Definition: std_expr.h:1259
index_exprt::index
const exprt & index() const
Definition: std_expr.h:1429
shl_exprt::shl_exprt
shl_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2721
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:330
can_cast_expr< isnan_exprt >
bool can_cast_expr< isnan_exprt >(const exprt &base)
Definition: std_expr.h:3681
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:879
binary_relation_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:821
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)
Definition: std_expr.h:4313
can_cast_expr< cond_exprt >
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition: std_expr.h:4466
member_exprt::member_exprt
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition: std_expr.h:3565
can_cast_expr< array_list_exprt >
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1620
can_cast_expr< mod_exprt >
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1214
extractbits_exprt::lower
exprt & lower()
Definition: std_expr.h:2881
if_exprt::if_exprt
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition: std_expr.h:3129
member_designatort::member_designatort
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:3343
shift_exprt::shift_exprt
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Definition: std_expr.h:2651
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1185
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:704
can_cast_expr< index_designatort >
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:3307
can_cast_expr< isinf_exprt >
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: std_expr.h:3731
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2295
array_list_exprt::array_list_exprt
array_list_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1597
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1573
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:203
and_exprt::and_exprt
and_exprt(exprt::operandst _operands)
Definition: std_expr.h:2303
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: std_expr.cpp:140
can_cast_expr< complex_imag_exprt >
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:1922
lshr_exprt::lshr_exprt
lshr_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2769
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2948
can_cast_expr< concatenation_exprt >
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: std_expr.h:4274
nondet_symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:232
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1489
binary_exprt::rhs
const exprt & rhs() const
Definition: std_expr.h:709
can_cast_expr< floatbv_typecast_exprt >
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
Definition: std_expr.h:2238
complex_exprt::real
const exprt & real() const
Definition: std_expr.h:1816
unary_minus_exprt::unary_minus_exprt
unary_minus_exprt(exprt _op, typet _type)
Definition: std_expr.h:394
to_type_expr
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition: std_expr.h:4079
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:904
can_cast_expr< bitor_exprt >
bool can_cast_expr< bitor_exprt >(const exprt &base)
Definition: std_expr.h:2550
floatbv_typecast_exprt::op
exprt & op()
Definition: std_expr.h:2216
can_cast_expr< not_exprt >
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:3010
typet
The type of an expression, extends irept.
Definition: type.h:28
ieee_float_notequal_exprt::ieee_float_notequal_exprt
ieee_float_notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:3930
update_exprt::old
exprt & old()
Definition: std_expr.h:3404
binary_relation_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:828
ternary_exprt
An expression with three operands.
Definition: std_expr.h:54
true_exprt::true_exprt
true_exprt()
Definition: std_expr.h:4147
mult_exprt::mult_exprt
mult_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1093
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1452
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3187
isnormal_exprt::isnormal_exprt
isnormal_exprt(exprt op)
Definition: std_expr.h:3819
can_cast_expr< sign_exprt >
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:616
ieee_float_equal_exprt::ieee_float_equal_exprt
ieee_float_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:3874
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:3045
extractbits_exprt::src
const exprt & src() const
Definition: std_expr.h:2886
dynamic_object_exprt
Representation of heap-allocated objects.
Definition: std_expr.h:2047
symbol_exprt::symbol_exprt
symbol_exprt(typet type)
Definition: std_expr.h:92
can_cast_expr< unary_exprt >
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:314
if_exprt::true_case
const exprt & true_case() const
Definition: std_expr.h:3154
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3121
member_designatort
Definition: std_expr.h:3340
is_dynamic_object_exprt
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: std_expr.h:2117
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:108
can_cast_expr< isfinite_exprt >
bool can_cast_expr< isfinite_exprt >(const exprt &base)
Definition: std_expr.h:3781
replication_exprt::times
constant_exprt & times()
Definition: std_expr.h:4196
div_exprt::div_exprt
div_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1138
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:1607
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1959
xor_exprt
Boolean XOR.
Definition: std_expr.h:2455
dereference_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
Definition: std_expr.cpp:281
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:3238
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:988
binary_predicate_exprt::binary_predicate_exprt
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition: std_expr.h:772
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1867
invariant.h
address_of_exprt::address_of_exprt
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:184
let_exprt::symbol
symbol_exprt & symbol()
Definition: std_expr.h:4323
and_exprt
Boolean AND.
Definition: std_expr.h:2274
union_exprt
Union constructor from single element.
Definition: std_expr.h:1689
array_comprehension_exprt::type
array_typet & type()
Definition: std_expr.h:4528
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:28
bitxor_exprt::bitxor_exprt
bitxor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2579
can_cast_expr< bitxor_exprt >
bool can_cast_expr< bitxor_exprt >(const exprt &base)
Definition: std_expr.h:2586
to_ieee_float_equal_expr
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
Definition: std_expr.h:3900
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:1517
can_cast_expr< ieee_float_notequal_exprt >
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: std_expr.h:3940
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:980
can_cast_expr< xor_exprt >
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2470
rem_exprt
Remainder of division.
Definition: std_expr.h:1249
equal_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1309
can_cast_expr< unary_minus_exprt >
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:406
abs_exprt::abs_exprt
abs_exprt(exprt _op)
Definition: std_expr.h:350
exprt
Base class for all expressions.
Definition: expr.h:52
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:1849
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:694
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:275
ashr_exprt::ashr_exprt
ashr_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2754
array_exprt::array_exprt
array_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1545
dereference_exprt::dereference_exprt
dereference_exprt(const exprt &op)
Definition: std_expr.h:3048
index_exprt::index_exprt
index_exprt(exprt _array, exprt _index, typet _type)
Definition: std_expr.h:1405
decorated_symbol_exprt::clear_static_lifetime
void clear_static_lifetime()
Definition: std_expr.h:146
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:650
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1736
bswap_exprt::bswap_exprt
bswap_exprt(exprt _op, std::size_t bits_per_byte)
Definition: std_expr.h:493
array_of_exprt::type
array_typet & type()
Definition: std_expr.h:1484
member_designatort::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3349
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1789
bswap_exprt::get_bits_per_byte
std::size_t get_bits_per_byte() const
Definition: std_expr.h:499
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2408
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:601
can_cast_expr< binary_exprt >
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:725
update_exprt::designator
const exprt::operandst & designator() const
Definition: std_expr.h:3423
array_of_exprt::type
const array_typet & type() const
Definition: std_expr.h:1479
exprt::op0
exprt & op0()
Definition: expr.h:97
predicate_exprt::predicate_exprt
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:556
update_exprt::old
const exprt & old() const
Definition: std_expr.h:3409
extractbits_exprt::upper
const exprt & upper() const
Definition: std_expr.h:2891
replication_exprt::op
const exprt & op() const
Definition: std_expr.h:4211
array_comprehension_exprt::arg
const symbol_exprt & arg() const
Definition: std_expr.h:4533
cond_exprt::cond_exprt
cond_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4448
can_cast_expr< minus_exprt >
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:1054
to_array_list_expr
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1630
vector_typet
The vector type.
Definition: std_types.h:1749
bool_typet
The Boolean type.
Definition: std_types.h:36
concatenation_exprt
Concatenation of bit-vector operands.
Definition: std_expr.h:4256
index_designatort::index_designatort
index_designatort(exprt _index)
Definition: std_expr.h:3290
nullary_exprt::move_to_operands
void move_to_operands(exprt &)=delete
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1647
to_isnormal_expr
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: std_expr.h:3847
lshr_exprt
Logical right shift.
Definition: std_expr.h:2766
index_exprt::index_exprt
index_exprt(const exprt &_array, exprt _index)
Definition: std_expr.h:1400
type_exprt::type_exprt
type_exprt(typet type)
Definition: std_expr.h:4062
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1820
can_cast_expr< bitand_exprt >
bool can_cast_expr< bitand_exprt >(const exprt &base)
Definition: std_expr.h:2622
to_bitand_expr
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
Definition: std_expr.h:2633
div_exprt
Division.
Definition: std_expr.h:1135
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:88
shift_exprt::op
exprt & op()
Definition: std_expr.h:2658
can_cast_expr< array_exprt >
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1562
validate_expr
void validate_expr(const symbol_exprt &value)
Definition: std_expr.h:173
can_cast_expr< member_exprt >
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:3631
minus_exprt::minus_exprt
minus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1047
union_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:1708
equal_exprt
Equality.
Definition: std_expr.h:1294
array_comprehension_exprt::type
const array_typet & type() const
Definition: std_expr.h:4523
multi_ary_exprt::op2
exprt & op2()
Definition: std_expr.h:923
to_rem_expr
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
Definition: std_expr.h:1275
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1070
floatbv_typecast_exprt::rounding_mode
const exprt & rounding_mode() const
Definition: std_expr.h:2231
replication_exprt
Bit-vector replication.
Definition: std_expr.h:4188
can_cast_expr< equal_exprt >
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1319
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4300
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3159
array_list_exprt::add
void add(exprt index, exprt value)
add an index/value pair
Definition: std_expr.h:1613
isfinite_exprt
Evaluates to true if the operand is finite.
Definition: std_expr.h:3766
can_cast_expr< implies_exprt >
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2352
notequal_exprt
Disequality.
Definition: std_expr.h:1352
replication_exprt::op
exprt & op()
Definition: std_expr.h:4206
extractbits_exprt::upper
exprt & upper()
Definition: std_expr.h:2876
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:1703
multi_ary_exprt::op3
exprt & op3()
Definition: std_expr.h:929
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:466
array_comprehension_exprt::arg
symbol_exprt & arg()
Definition: std_expr.h:4538
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:1894
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:741
narrow.h
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4285
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1755
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2696
union_exprt::union_exprt
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition: std_expr.h:1692
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
complex_exprt::imag
exprt imag()
Definition: std_expr.h:1821
ieee_float_notequal_exprt
IEEE floating-point disequality.
Definition: std_expr.h:3920
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:255
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
let_exprt::value
exprt & value()
Definition: std_expr.h:4333
or_exprt::or_exprt
or_exprt(exprt::operandst _operands)
Definition: std_expr.h:2416
nullary_exprt
An expression without operands.
Definition: std_expr.h:23
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:4355
not_exprt::not_exprt
not_exprt(exprt _op)
Definition: std_expr.h:2998
can_cast_expr< bitnot_exprt >
bool can_cast_expr< bitnot_exprt >(const exprt &base)
Definition: std_expr.h:2505
can_cast_expr< and_exprt >
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2316
member_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:3587
array_exprt::type
const array_typet & type() const
Definition: std_expr.h:1550
with_exprt::where
const exprt & where() const
Definition: std_expr.h:3233
with_exprt::old
exprt & old()
Definition: std_expr.h:3218
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition: std_expr.h:993
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2287
dynamic_object_exprt::get_instance
unsigned int get_instance() const
Definition: std_expr.cpp:45
address_of_exprt::address_of_exprt
address_of_exprt(exprt op, pointer_typet _type)
Definition: std_expr.h:2943
to_cond_expr
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:4483
with_exprt::with_exprt
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition: std_expr.h:3210
xor_exprt::xor_exprt
xor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2463
rem_exprt::rem_exprt
rem_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1252
notequal_exprt::notequal_exprt
notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1355
bitxor_exprt
Bit-wise XOR.
Definition: std_expr.h:2576
bitor_exprt
Bit-wise OR.
Definition: std_expr.h:2540
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
Definition: std_expr.h:4338
dereference_exprt::pointer
const exprt & pointer() const
Definition: std_expr.h:3064
or_exprt
Boolean OR.
Definition: std_expr.h:2387
can_cast_expr< abs_exprt >
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:356
array_exprt::type
array_typet & type()
Definition: std_expr.h:1555
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1230
complex_real_exprt::complex_real_exprt
complex_real_exprt(const exprt &op)
Definition: std_expr.h:1870
member_exprt::struct_op
exprt & struct_op()
Definition: std_expr.h:3599
update_exprt::update_exprt
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition: std_expr.h:3394
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2282
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
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1116
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4178
array_comprehension_exprt::array_comprehension_exprt
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition: std_expr.h:4511
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2976
member_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3614
decorated_symbol_exprt::set_static_lifetime
void set_static_lifetime()
Definition: std_expr.h:141
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:74
symbol_exprt::symbol_exprt
symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:98
to_replication_expr
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: std_expr.h:4234
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2204
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3604
ternary_exprt::ternary_exprt
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition: std_expr.h:65
predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:548
bitor_exprt::bitor_exprt
bitor_exprt(const exprt &_op0, exprt _op1)
Definition: std_expr.h:2543
multi_ary_exprt::op1
const exprt & op1() const
Definition: std_expr.h:941
can_cast_expr< address_of_exprt >
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:2960
can_cast_expr< plus_exprt >
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:1009
update_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:3433
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3593
to_xor_expr
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2481
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:756
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:917
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
extractbits_exprt::lower
const exprt & lower() const
Definition: std_expr.h:2896
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:1501
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:118
dereference_exprt::dereference_exprt
dereference_exprt(exprt op, typet type)
Definition: std_expr.h:3054
nil_exprt
The NIL expression.
Definition: std_expr.h:4162
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1471
nondet_symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:227
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:3059
index_designatort::index
const exprt & index() const
Definition: std_expr.h:3295
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:50
shl_exprt::shl_exprt
shl_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2716
decorated_symbol_exprt::is_thread_local
bool is_thread_local() const
Definition: std_expr.h:151
std_types.h
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4371
can_cast_expr< bswap_exprt >
bool can_cast_expr< bswap_exprt >(const exprt &base)
Definition: std_expr.h:511
floatbv_typecast_exprt::floatbv_typecast_exprt
floatbv_typecast_exprt(exprt op, exprt rounding, typet _type)
Definition: std_expr.h:2207
can_cast_expr< notequal_exprt >
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1362
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1025
to_isfinite_expr
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: std_expr.h:3797
isfinite_exprt::isfinite_exprt
isfinite_exprt(exprt op)
Definition: std_expr.h:3769
cond_exprt::add_case
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:4456
to_object_descriptor_expr
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:2026
can_cast_expr< nil_exprt >
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition: std_expr.h:4172
extractbits_exprt::src
exprt & src()
Definition: std_expr.h:2871
can_cast_expr< ieee_float_op_exprt >
bool can_cast_expr< ieee_float_op_exprt >(const exprt &base)
Definition: std_expr.h:4023
array_comprehension_exprt::body
const exprt & body() const
Definition: std_expr.h:4543
member_exprt::compound
exprt & compound()
Definition: std_expr.h:3609
to_is_dynamic_object_expr
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: std_expr.h:2131
exprt::op1
exprt & op1()
Definition: expr.h:100
null_pointer_exprt::null_pointer_exprt
null_pointer_exprt(pointer_typet type)
Definition: std_expr.h:4181
dynamic_object_exprt::valid
const exprt & valid() const
Definition: std_expr.h:2074
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1378
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1090
with_exprt::old
const exprt & old() const
Definition: std_expr.h:3223
isnan_exprt::isnan_exprt
isnan_exprt(exprt op)
Definition: std_expr.h:3669
concatenation_exprt::concatenation_exprt
concatenation_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4259
index_exprt::index
exprt & index()
Definition: std_expr.h:1424
nil_exprt::nil_exprt
nil_exprt()
Definition: std_expr.h:4165
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:422
is_dynamic_object_exprt::is_dynamic_object_exprt
is_dynamic_object_exprt(const exprt &op)
Definition: std_expr.h:2124
decorated_symbol_exprt::set_thread_local
void set_thread_local()
Definition: std_expr.h:156
mod_exprt::mod_exprt
mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1207
nondet_symbol_exprt::nondet_symbol_exprt
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition: std_expr.h:217
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:391
index_exprt::array
exprt & array()
Definition: std_expr.h:1414
to_ieee_float_op_expr
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: std_expr.h:4041
ternary_exprt::op3
const exprt & op3() const =delete
extractbit_exprt::index
exprt & index()
Definition: std_expr.h:2797
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:184
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:241
struct_exprt::struct_exprt
struct_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1763
validation_modet
validation_modet
Definition: validation_mode.h:12
ieee_float_op_exprt::rounding_mode
const exprt & rounding_mode() const
Definition: std_expr.h:4016
irept::id
const irep_idt & id() const
Definition: irep.h:418
binary_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:676
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
popcount_exprt::popcount_exprt
popcount_exprt(const exprt &_op)
Definition: std_expr.h:4397
can_cast_expr< div_exprt >
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1169
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1799
abs_exprt
Absolute value.
Definition: std_expr.h:347
false_exprt
The Boolean constant false.
Definition: std_expr.h:4153
vector_exprt::vector_exprt
vector_exprt(operandst _operands, vector_typet _type)
Definition: std_expr.h:1656
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:440
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition: std_expr.h:893
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:295
bitand_exprt
Bit-wise AND.
Definition: std_expr.h:2612
if_exprt::cond
const exprt & cond() const
Definition: std_expr.h:3144
to_dynamic_object_expr
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: std_expr.h:2097
object_descriptor_exprt::object
const exprt & object() const
Definition: std_expr.h:1991
div_exprt::dividend
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1150
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:217
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
index_designatort
Definition: std_expr.h:3287
complex_exprt::imag
const exprt & imag() const
Definition: std_expr.h:1826
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:1939
binary_predicate_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:777
to_bswap_expr
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: std_expr.h:529
to_ieee_float_notequal_expr
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
Definition: std_expr.h:3956
to_isinf_expr
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: std_expr.h:3747
array_list_exprt::type
const array_typet & type() const
Definition: std_expr.h:1602
div_exprt::divisor
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1156
isinf_exprt::isinf_exprt
isinf_exprt(exprt op)
Definition: std_expr.h:3719
binary_relation_exprt::binary_relation_exprt
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:816
unary_exprt::unary_exprt
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition: std_expr.h:290
minus_exprt
Binary minus.
Definition: std_expr.h:1044
div_exprt::dividend
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1144
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3270
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3391
nullary_exprt::op0
const exprt & op0() const =delete
can_cast_expr< extractbit_exprt >
bool can_cast_expr< extractbit_exprt >(const exprt &base)
Definition: std_expr.h:2814
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:3418
object_descriptor_exprt::object_descriptor_exprt
object_descriptor_exprt(exprt _object)
Definition: std_expr.h:1971
binary_exprt::validate
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:686
multi_ary_exprt::op0
const exprt & op0() const
Definition: std_expr.h:935
source_locationt
Definition: source_location.h:19
unary_plus_exprt::unary_plus_exprt
unary_plus_exprt(exprt op)
Definition: std_expr.h:443
can_cast_expr< replication_exprt >
bool can_cast_expr< replication_exprt >(const exprt &base)
Definition: std_expr.h:4218
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2440
can_cast_expr< index_exprt >
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1436
unary_exprt::unary_exprt
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:278
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1698
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2496
to_isnan_expr
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: std_expr.h:3697
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2781
to_bitxor_expr
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
Definition: std_expr.h:2597
sign_exprt::sign_exprt
sign_exprt(exprt _op)
Definition: std_expr.h:609
unary_minus_exprt::unary_minus_exprt
unary_minus_exprt(exprt _op)
Definition: std_expr.h:399
to_bitor_expr
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
Definition: std_expr.h:2561
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3562
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:847
extractbit_exprt::extractbit_exprt
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
Definition: std_expr.h:2785
equal_exprt::equal_exprt
equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1297
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3102
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:126
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2648
dynamic_object_exprt::set_instance
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
can_cast_expr< complex_real_exprt >
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:1877
type_exprt
An expression denoting a type.
Definition: std_expr.h:4059
can_cast_expr< array_comprehension_exprt >
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition: std_expr.h:4555
plus_exprt::plus_exprt
plus_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1002
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:4440
ieee_float_op_exprt::rounding_mode
exprt & rounding_mode()
Definition: std_expr.h:4011
equal_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1302
infinity_exprt::infinity_exprt
infinity_exprt(typet _type)
Definition: std_expr.h:4303
dynamic_object_exprt::valid
exprt & valid()
Definition: std_expr.h:2069
array_typet
Arrays with given size.
Definition: std_types.h:964
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
object_descriptor_exprt::offset
const exprt & offset() const
Definition: std_expr.h:2003
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3149
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:2429
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:2919
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:131
floatbv_typecast_exprt::rounding_mode
exprt & rounding_mode()
Definition: std_expr.h:2226
extractbits_exprt::extractbits_exprt
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
Definition: std_expr.h:2857
bitand_exprt::bitand_exprt
bitand_exprt(const exprt &_op0, exprt _op1)
Definition: std_expr.h:2615
to_sign_expr
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:632
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3026
shift_exprt::distance
exprt & distance()
Definition: std_expr.h:2668
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
isinf_exprt
Evaluates to true if the operand is infinite.
Definition: std_expr.h:3716
to_floatbv_typecast_expr
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2254
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:22
update_exprt::new_value
exprt & new_value()
Definition: std_expr.h:3428
replication_exprt::replication_exprt
replication_exprt(const constant_exprt &_times, const exprt &_src)
Definition: std_expr.h:4191
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2368
ieee_float_op_exprt::lhs
const exprt & lhs() const
Definition: std_expr.h:3996
member_exprt::member_exprt
member_exprt(exprt op, const struct_typet::componentt &c)
Definition: std_expr.h:3571
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:4068
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
extractbit_exprt::src
exprt & src()
Definition: std_expr.h:2792
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2185
can_cast_expr< popcount_exprt >
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: std_expr.h:4404
ashr_exprt
Arithmetic right shift.
Definition: std_expr.h:2751
if_exprt::false_case
const exprt & false_case() const
Definition: std_expr.h:3164
lshr_exprt::lshr_exprt
lshr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2774
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3139
floatbv_typecast_exprt::op
const exprt & op() const
Definition: std_expr.h:2221
binary_exprt::binary_exprt
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:671
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:800
typecast_exprt::typecast_exprt
typecast_exprt(exprt op, typet _type)
Definition: std_expr.h:2153
extractbit_exprt::index
const exprt & index() const
Definition: std_expr.h:2807
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:1912
ieee_float_op_exprt::lhs
exprt & lhs()
Definition: std_expr.h:3991
can_cast_expr< shift_exprt >
bool can_cast_expr< shift_exprt >(const exprt &base)
Definition: std_expr.h:2680
can_cast_expr< nondet_symbol_exprt >
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:239
nullary_exprt::nullary_exprt
nullary_exprt(const irep_idt &_id, typet _type)
Definition: std_expr.h:26
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1335
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:151
binary_exprt::lhs
const exprt & lhs() const
Definition: std_expr.h:699
binary_exprt::binary_exprt
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:666
decorated_symbol_exprt::clear_thread_local
void clear_thread_local()
Definition: std_expr.h:161
can_cast_expr< isnormal_exprt >
bool can_cast_expr< isnormal_exprt >(const exprt &base)
Definition: std_expr.h:3831
bswap_exprt::set_bits_per_byte
void set_bits_per_byte(std::size_t bits_per_byte)
Definition: std_expr.h:504
array_comprehension_exprt::body
exprt & body()
Definition: std_expr.h:4548
to_bitnot_expr
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: std_expr.h:2521
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:3979
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2400
unary_exprt::op
exprt & op()
Definition: std_expr.h:300
multi_ary_exprt::op2
const exprt & op2() const
Definition: std_expr.h:947
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3647
concatenation_exprt::concatenation_exprt
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
Definition: std_expr.h:4264
can_cast_expr< object_descriptor_exprt >
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:2010
can_cast_expr< typecast_exprt >
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2169
bswap_exprt
The byte swap expression.
Definition: std_expr.h:484
shift_exprt::distance
const exprt & distance() const
Definition: std_expr.h:2673
can_cast_expr< vector_exprt >
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1663
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3577
complex_exprt::complex_exprt
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition: std_expr.h:1802
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
implies_exprt
Boolean implication.
Definition: std_expr.h:2342
let_exprt::where
const exprt & where() const
Definition: std_expr.h:4348
shift_exprt::op
const exprt & op() const
Definition: std_expr.h:2663
can_cast_expr< if_exprt >
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:3171
array_of_exprt::what
const exprt & what() const
Definition: std_expr.h:1494
struct_exprt::component
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:205
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1588
constant_exprt::constant_exprt
constant_exprt(const irep_idt &_value, typet _type)
Definition: std_expr.h:4098
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2849
can_cast_expr< constant_exprt >
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:4118
exprt::operands
operandst & operands()
Definition: expr.h:91
decorated_symbol_exprt::is_static_lifetime
bool is_static_lifetime() const
Definition: std_expr.h:136
can_cast_expr< complex_exprt >
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:1833
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2395
ashr_exprt::ashr_exprt
ashr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2759
false_exprt::false_exprt
false_exprt()
Definition: std_expr.h:4156
nullary_exprt::op2
const exprt & op2() const =delete
ieee_float_op_exprt::rhs
const exprt & rhs() const
Definition: std_expr.h:4006
index_exprt
Array index operator.
Definition: std_expr.h:1397
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2938
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:256
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4389
object_descriptor_exprt::object_descriptor_exprt
object_descriptor_exprt()
Definition: std_expr.h:1962
address_of_exprt::object
const exprt & object() const
Definition: std_expr.h:2953
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2150
can_cast_expr< unary_plus_exprt >
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:450
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1487
unary_predicate_exprt::unary_predicate_exprt
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition: std_expr.h:593
binary_predicate_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:784
complex_imag_exprt::complex_imag_exprt
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:1915
is_dynamic_object_exprt::is_dynamic_object_exprt
is_dynamic_object_exprt()
Definition: std_expr.h:2120
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:4508
replication_exprt::times
const constant_exprt & times() const
Definition: std_expr.h:4201
object_descriptor_exprt::object
exprt & object()
Definition: std_expr.h:1986
true_exprt
The Boolean constant true.
Definition: std_expr.h:4144
constant_exprt
A constant literal expression.
Definition: std_expr.h:4095
can_cast_expr< extractbits_exprt >
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: std_expr.h:2903
ieee_float_equal_exprt
IEEE-floating-point equality.
Definition: std_expr.h:3866
binary_exprt::op2
const exprt & op2() const =delete
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:911
unary_exprt::op3
const exprt & op3() const =delete
implies_exprt::implies_exprt
implies_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2345
index_designatort::index
exprt & index()
Definition: std_expr.h:3300
can_cast_expr< struct_exprt >
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1773
bswap_exprt::bswap_exprt
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
Definition: std_expr.h:487
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:966
let_exprt::where
exprt & where()
Definition: std_expr.h:4343
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:899
union_exprt::set_component_number
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1713
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:863
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:4109
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4104
let_exprt::symbol
const symbol_exprt & symbol() const
Definition: std_expr.h:4328
with_exprt::where
exprt & where()
Definition: std_expr.h:3228
array_of_exprt::array_of_exprt
array_of_exprt(exprt _what, array_typet _type)
Definition: std_expr.h:1474
to_member_designator
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:3372
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1536
can_cast_expr< with_exprt >
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3250
ieee_float_op_exprt::rhs
exprt & rhs()
Definition: std_expr.h:4001
isnormal_exprt
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:3816
member_exprt::set_component_name
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3582
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:579
popcount_exprt::popcount_exprt
popcount_exprt(exprt _op, typet _type)
Definition: std_expr.h:4392
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:113
bitnot_exprt::bitnot_exprt
bitnot_exprt(exprt op)
Definition: std_expr.h:2499
with_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:3243
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:2830
to_shl_expr
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: std_expr.h:2733
as_const.h
extractbit_exprt::src
const exprt & src() const
Definition: std_expr.h:2802
let_exprt
A let expression.
Definition: std_expr.h:4310
to_and_expr
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2327
ieee_float_op_exprt::ieee_float_op_exprt
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs, exprt _rm)
Definition: std_expr.h:3982
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:1162
complex_exprt::real
exprt real()
Definition: std_expr.h:1811
expr_protectedt
Base class for all expressions.
Definition: expr.h:358
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1784
validation_modet::INVARIANT
can_cast_expr< member_designatort >
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:3356
to_abs_expr
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:372
mod_exprt
Modulo.
Definition: std_expr.h:1204
dereference_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3069
can_cast_expr< update_exprt >
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:3440
to_index_designator
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:3323
shl_exprt
Left shift.
Definition: std_expr.h:2713
can_cast_expr< dereference_exprt >
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: std_expr.h:3086
can_cast_expr< ieee_float_equal_exprt >
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Definition: std_expr.h:3884
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3666
can_cast_expr< dynamic_object_exprt >
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: std_expr.h:2081
can_cast_expr< mult_exprt >
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1100
not_exprt
Boolean negation.
Definition: std_expr.h:2995
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4129
nondet_symbol_exprt::nondet_symbol_exprt
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:208
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1998
multi_ary_exprt::op3
const exprt & op3() const
Definition: std_expr.h:953