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 
694  // make op0 and op1 public
695  using exprt::op0;
696  using exprt::op1;
697 
698  const exprt &op2() const = delete;
699  exprt &op2() = delete;
700  const exprt &op3() const = delete;
701  exprt &op3() = delete;
702 };
703 
704 template <>
705 inline bool can_cast_expr<binary_exprt>(const exprt &base)
706 {
707  return base.operands().size() == 2;
708 }
709 
710 inline void validate_expr(const binary_exprt &value)
711 {
712  binary_exprt::check(value);
713 }
714 
721 inline const binary_exprt &to_binary_expr(const exprt &expr)
722 {
723  binary_exprt::check(expr);
724  return static_cast<const binary_exprt &>(expr);
725 }
726 
729 {
730  binary_exprt::check(expr);
731  return static_cast<binary_exprt &>(expr);
732 }
733 
737 {
738 public:
739  DEPRECATED(
740  SINCE(2018, 12, 2, "use binary_predicate_exprt(lhs, id, rhs) instead"))
742  {
743  }
744 
745  DEPRECATED(
746  SINCE(2018, 12, 2, "use binary_predicate_exprt(lhs, id, rhs) instead"))
747  explicit binary_predicate_exprt(const irep_idt &_id):
748  binary_exprt(_id, bool_typet())
749  {
750  }
751 
752  binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
753  : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
754  {
755  }
756 
757  static void check(
758  const exprt &expr,
760  {
761  binary_exprt::check(expr, vm);
762  }
763 
764  static void validate(
765  const exprt &expr,
766  const namespacet &ns,
768  {
769  binary_exprt::validate(expr, ns, vm);
770 
771  DATA_CHECK(
772  vm,
773  expr.type().id() == ID_bool,
774  "result of binary predicate expression should be of type bool");
775  }
776 };
777 
780 {
781 public:
782  DEPRECATED(
783  SINCE(2018, 12, 2, "use binary_relation_exprt(lhs, id, rhs) instead"))
785  {
786  }
787 
788  DEPRECATED(
789  SINCE(2018, 12, 2, "use binary_relation_exprt(lhs, id, rhs) instead"))
790  explicit binary_relation_exprt(const irep_idt &id):
792  {
793  }
794 
795  binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
796  : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
797  {
798  }
799 
800  static void check(
801  const exprt &expr,
803  {
805  }
806 
807  static void validate(
808  const exprt &expr,
809  const namespacet &ns,
811  {
812  binary_predicate_exprt::validate(expr, ns, vm);
813 
814  // check types
815  DATA_CHECK(
816  vm,
817  expr.op0().type() == expr.op1().type(),
818  "lhs and rhs of binary relation expression should have same type");
819  }
820 
822  {
823  return op0();
824  }
825 
826  const exprt &lhs() const
827  {
828  return op0();
829  }
830 
832  {
833  return op1();
834  }
835 
836  const exprt &rhs() const
837  {
838  return op1();
839  }
840 };
841 
842 template <>
844 {
845  return can_cast_expr<binary_exprt>(base);
846 }
847 
848 inline void validate_expr(const binary_relation_exprt &value)
849 {
851 }
852 
860 {
862  return static_cast<const binary_relation_exprt &>(expr);
863 }
864 
867 {
869  return static_cast<binary_relation_exprt &>(expr);
870 }
871 
872 
876 {
877 public:
878  DEPRECATED(SINCE(2018, 9, 21, "use multi_ary_exprt(id, op, type) instead"))
879  explicit multi_ary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet())
880  {
881  }
882 
883  DEPRECATED(SINCE(2018, 12, 7, "use multi_ary_exprt(id, op, type) instead"))
884  multi_ary_exprt(const irep_idt &_id, const typet &_type)
885  : expr_protectedt(_id, _type)
886  {
887  }
888 
889  multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
890  : expr_protectedt(_id, std::move(_type))
891  {
892  operands() = std::move(_operands);
893  }
894 
895  multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
896  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
897  {
898  }
899 
900  multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
901  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
902  {
903  }
904 
905  // In contrast to exprt::opX, the methods
906  // below check the size.
908  {
909  PRECONDITION(operands().size() >= 1);
910  return operands().front();
911  }
912 
914  {
915  PRECONDITION(operands().size() >= 2);
916  return operands()[1];
917  }
918 
920  {
921  PRECONDITION(operands().size() >= 3);
922  return operands()[2];
923  }
924 
926  {
927  PRECONDITION(operands().size() >= 4);
928  return operands()[3];
929  }
930 
931  const exprt &op0() const
932  {
933  PRECONDITION(operands().size() >= 1);
934  return operands().front();
935  }
936 
937  const exprt &op1() const
938  {
939  PRECONDITION(operands().size() >= 2);
940  return operands()[1];
941  }
942 
943  const exprt &op2() const
944  {
945  PRECONDITION(operands().size() >= 3);
946  return operands()[2];
947  }
948 
949  const exprt &op3() const
950  {
951  PRECONDITION(operands().size() >= 4);
952  return operands()[3];
953  }
954 };
955 
962 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
963 {
964  return static_cast<const multi_ary_exprt &>(expr);
965 }
966 
969 {
970  return static_cast<multi_ary_exprt &>(expr);
971 }
972 
973 
977 {
978 public:
979  DEPRECATED(SINCE(2019, 1, 12, "use plus_exprt(lhs, rhs, type) instead"))
981  {
982  }
983 
984  plus_exprt(exprt _lhs, exprt _rhs)
985  : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
986  {
987  }
988 
989  plus_exprt(exprt _lhs, exprt _rhs, typet _type)
990  : multi_ary_exprt(
991  std::move(_lhs),
992  ID_plus,
993  std::move(_rhs),
994  std::move(_type))
995  {
996  }
997 
998  plus_exprt(operandst _operands, typet _type)
999  : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
1000  {
1001  }
1002 };
1003 
1004 template <>
1005 inline bool can_cast_expr<plus_exprt>(const exprt &base)
1006 {
1007  return base.id() == ID_plus;
1008 }
1009 
1010 inline void validate_expr(const plus_exprt &value)
1011 {
1012  validate_operands(value, 2, "Plus must have two or more operands", true);
1013 }
1014 
1021 inline const plus_exprt &to_plus_expr(const exprt &expr)
1022 {
1023  PRECONDITION(expr.id()==ID_plus);
1024  const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
1025  validate_expr(ret);
1026  return ret;
1027 }
1028 
1031 {
1032  PRECONDITION(expr.id()==ID_plus);
1033  plus_exprt &ret = static_cast<plus_exprt &>(expr);
1034  validate_expr(ret);
1035  return ret;
1036 }
1037 
1038 
1041 {
1042 public:
1044  : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
1045  {
1046  }
1047 };
1048 
1049 template <>
1050 inline bool can_cast_expr<minus_exprt>(const exprt &base)
1051 {
1052  return base.id() == ID_minus;
1053 }
1054 
1055 inline void validate_expr(const minus_exprt &value)
1056 {
1057  validate_operands(value, 2, "Minus must have two or more operands", true);
1058 }
1059 
1066 inline const minus_exprt &to_minus_expr(const exprt &expr)
1067 {
1068  PRECONDITION(expr.id()==ID_minus);
1069  const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
1070  validate_expr(ret);
1071  return ret;
1072 }
1073 
1076 {
1077  PRECONDITION(expr.id()==ID_minus);
1078  minus_exprt &ret = static_cast<minus_exprt &>(expr);
1079  validate_expr(ret);
1080  return ret;
1081 }
1082 
1083 
1087 {
1088 public:
1089  mult_exprt(exprt _lhs, exprt _rhs)
1090  : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
1091  {
1092  }
1093 };
1094 
1095 template <>
1096 inline bool can_cast_expr<mult_exprt>(const exprt &base)
1097 {
1098  return base.id() == ID_mult;
1099 }
1100 
1101 inline void validate_expr(const mult_exprt &value)
1102 {
1103  validate_operands(value, 2, "Multiply must have two or more operands", true);
1104 }
1105 
1112 inline const mult_exprt &to_mult_expr(const exprt &expr)
1113 {
1114  PRECONDITION(expr.id()==ID_mult);
1115  const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1116  validate_expr(ret);
1117  return ret;
1118 }
1119 
1122 {
1123  PRECONDITION(expr.id()==ID_mult);
1124  mult_exprt &ret = static_cast<mult_exprt &>(expr);
1125  validate_expr(ret);
1126  return ret;
1127 }
1128 
1129 
1132 {
1133 public:
1134  div_exprt(exprt _lhs, exprt _rhs)
1135  : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1136  {
1137  }
1138 
1141  {
1142  return op0();
1143  }
1144 
1146  const exprt &dividend() const
1147  {
1148  return op0();
1149  }
1150 
1153  {
1154  return op1();
1155  }
1156 
1158  const exprt &divisor() const
1159  {
1160  return op1();
1161  }
1162 };
1163 
1164 template <>
1165 inline bool can_cast_expr<div_exprt>(const exprt &base)
1166 {
1167  return base.id() == ID_div;
1168 }
1169 
1170 inline void validate_expr(const div_exprt &value)
1171 {
1172  validate_operands(value, 2, "Divide must have two operands");
1173 }
1174 
1181 inline const div_exprt &to_div_expr(const exprt &expr)
1182 {
1183  PRECONDITION(expr.id()==ID_div);
1184  const div_exprt &ret = static_cast<const div_exprt &>(expr);
1185  validate_expr(ret);
1186  return ret;
1187 }
1188 
1191 {
1192  PRECONDITION(expr.id()==ID_div);
1193  div_exprt &ret = static_cast<div_exprt &>(expr);
1194  validate_expr(ret);
1195  return ret;
1196 }
1197 
1198 
1201 {
1202 public:
1203  mod_exprt(exprt _lhs, exprt _rhs)
1204  : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1205  {
1206  }
1207 };
1208 
1209 template <>
1210 inline bool can_cast_expr<mod_exprt>(const exprt &base)
1211 {
1212  return base.id() == ID_mod;
1213 }
1214 
1215 inline void validate_expr(const mod_exprt &value)
1216 {
1217  validate_operands(value, 2, "Modulo must have two operands");
1218 }
1219 
1226 inline const mod_exprt &to_mod_expr(const exprt &expr)
1227 {
1228  PRECONDITION(expr.id()==ID_mod);
1229  const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1230  validate_expr(ret);
1231  return ret;
1232 }
1233 
1236 {
1237  PRECONDITION(expr.id()==ID_mod);
1238  mod_exprt &ret = static_cast<mod_exprt &>(expr);
1239  validate_expr(ret);
1240  return ret;
1241 }
1242 
1243 
1246 {
1247 public:
1248  rem_exprt(exprt _lhs, exprt _rhs)
1249  : binary_exprt(std::move(_lhs), ID_rem, std::move(_rhs))
1250  {
1251  }
1252 };
1253 
1254 template <>
1255 inline bool can_cast_expr<rem_exprt>(const exprt &base)
1256 {
1257  return base.id() == ID_rem;
1258 }
1259 
1260 inline void validate_expr(const rem_exprt &value)
1261 {
1262  validate_operands(value, 2, "Remainder must have two operands");
1263 }
1264 
1271 inline const rem_exprt &to_rem_expr(const exprt &expr)
1272 {
1273  PRECONDITION(expr.id()==ID_rem);
1274  const rem_exprt &ret = static_cast<const rem_exprt &>(expr);
1275  validate_expr(ret);
1276  return ret;
1277 }
1278 
1281 {
1282  PRECONDITION(expr.id()==ID_rem);
1283  rem_exprt &ret = static_cast<rem_exprt &>(expr);
1284  validate_expr(ret);
1285  return ret;
1286 }
1287 
1288 
1291 {
1292 public:
1294  : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1295  {
1296  }
1297 
1298  static void check(
1299  const exprt &expr,
1301  {
1302  binary_relation_exprt::check(expr, vm);
1303  }
1304 
1305  static void validate(
1306  const exprt &expr,
1307  const namespacet &ns,
1309  {
1310  binary_relation_exprt::validate(expr, ns, vm);
1311  }
1312 };
1313 
1314 template <>
1315 inline bool can_cast_expr<equal_exprt>(const exprt &base)
1316 {
1317  return base.id() == ID_equal;
1318 }
1319 
1320 inline void validate_expr(const equal_exprt &value)
1321 {
1322  equal_exprt::check(value);
1323 }
1324 
1331 inline const equal_exprt &to_equal_expr(const exprt &expr)
1332 {
1333  PRECONDITION(expr.id()==ID_equal);
1334  equal_exprt::check(expr);
1335  return static_cast<const equal_exprt &>(expr);
1336 }
1337 
1340 {
1341  PRECONDITION(expr.id()==ID_equal);
1342  equal_exprt::check(expr);
1343  return static_cast<equal_exprt &>(expr);
1344 }
1345 
1346 
1349 {
1350 public:
1352  : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1353  {
1354  }
1355 };
1356 
1357 template <>
1358 inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1359 {
1360  return base.id() == ID_notequal;
1361 }
1362 
1363 inline void validate_expr(const notequal_exprt &value)
1364 {
1365  validate_operands(value, 2, "Inequality must have two operands");
1366 }
1367 
1374 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1375 {
1376  PRECONDITION(expr.id()==ID_notequal);
1377  const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1378  validate_expr(ret);
1379  return ret;
1380 }
1381 
1384 {
1385  PRECONDITION(expr.id()==ID_notequal);
1386  notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1387  validate_expr(ret);
1388  return ret;
1389 }
1390 
1391 
1394 {
1395 public:
1396  index_exprt(const exprt &_array, exprt _index)
1397  : binary_exprt(_array, ID_index, std::move(_index), _array.type().subtype())
1398  {
1399  }
1400 
1401  index_exprt(exprt _array, exprt _index, typet _type)
1402  : binary_exprt(
1403  std::move(_array),
1404  ID_index,
1405  std::move(_index),
1406  std::move(_type))
1407  {
1408  }
1409 
1411  {
1412  return op0();
1413  }
1414 
1415  const exprt &array() const
1416  {
1417  return op0();
1418  }
1419 
1421  {
1422  return op1();
1423  }
1424 
1425  const exprt &index() const
1426  {
1427  return op1();
1428  }
1429 };
1430 
1431 template <>
1432 inline bool can_cast_expr<index_exprt>(const exprt &base)
1433 {
1434  return base.id() == ID_index;
1435 }
1436 
1437 inline void validate_expr(const index_exprt &value)
1438 {
1439  validate_operands(value, 2, "Array index must have two operands");
1440 }
1441 
1448 inline const index_exprt &to_index_expr(const exprt &expr)
1449 {
1450  PRECONDITION(expr.id()==ID_index);
1451  const index_exprt &ret = static_cast<const index_exprt &>(expr);
1452  validate_expr(ret);
1453  return ret;
1454 }
1455 
1458 {
1459  PRECONDITION(expr.id()==ID_index);
1460  index_exprt &ret = static_cast<index_exprt &>(expr);
1461  validate_expr(ret);
1462  return ret;
1463 }
1464 
1465 
1468 {
1469 public:
1470  explicit array_of_exprt(exprt _what, array_typet _type)
1471  : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1472  {
1473  }
1474 
1475  const array_typet &type() const
1476  {
1477  return static_cast<const array_typet &>(unary_exprt::type());
1478  }
1479 
1481  {
1482  return static_cast<array_typet &>(unary_exprt::type());
1483  }
1484 
1486  {
1487  return op0();
1488  }
1489 
1490  const exprt &what() const
1491  {
1492  return op0();
1493  }
1494 };
1495 
1496 template <>
1497 inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1498 {
1499  return base.id() == ID_array_of;
1500 }
1501 
1502 inline void validate_expr(const array_of_exprt &value)
1503 {
1504  validate_operands(value, 1, "'Array of' must have one operand");
1505 }
1506 
1513 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1514 {
1515  PRECONDITION(expr.id()==ID_array_of);
1516  const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1517  validate_expr(ret);
1518  return ret;
1519 }
1520 
1523 {
1524  PRECONDITION(expr.id()==ID_array_of);
1525  array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1526  validate_expr(ret);
1527  return ret;
1528 }
1529 
1530 
1533 {
1534 public:
1535  DEPRECATED(SINCE(2019, 1, 12, "use array_exprt(operands, type) instead"))
1536  explicit array_exprt(const array_typet &_type)
1537  : multi_ary_exprt(ID_array, _type)
1538  {
1539  }
1540 
1542  : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1543  {
1544  }
1545 
1546  const array_typet &type() const
1547  {
1548  return static_cast<const array_typet &>(multi_ary_exprt::type());
1549  }
1550 
1552  {
1553  return static_cast<array_typet &>(multi_ary_exprt::type());
1554  }
1555 };
1556 
1557 template <>
1558 inline bool can_cast_expr<array_exprt>(const exprt &base)
1559 {
1560  return base.id() == ID_array;
1561 }
1562 
1569 inline const array_exprt &to_array_expr(const exprt &expr)
1570 {
1571  PRECONDITION(expr.id()==ID_array);
1572  return static_cast<const array_exprt &>(expr);
1573 }
1574 
1577 {
1578  PRECONDITION(expr.id()==ID_array);
1579  return static_cast<array_exprt &>(expr);
1580 }
1581 
1585 {
1586 public:
1587  DEPRECATED(SINCE(2019, 1, 12, "use array_list_exprt(operands, type) instead"))
1588  explicit array_list_exprt(const array_typet &_type)
1589  : multi_ary_exprt(ID_array_list, _type)
1590  {
1591  }
1592 
1594  : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1595  {
1596  }
1597 
1598  const array_typet &type() const
1599  {
1600  return static_cast<const array_typet &>(multi_ary_exprt::type());
1601  }
1602 
1604  {
1605  return static_cast<array_typet &>(multi_ary_exprt::type());
1606  }
1607 
1609  void add(exprt index, exprt value)
1610  {
1611  add_to_operands(std::move(index), std::move(value));
1612  }
1613 };
1614 
1615 template <>
1616 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1617 {
1618  return base.id() == ID_array_list;
1619 }
1620 
1621 inline void validate_expr(const array_list_exprt &value)
1622 {
1623  PRECONDITION(value.operands().size() % 2 == 0);
1624 }
1625 
1626 inline const array_list_exprt &to_array_list_expr(const exprt &expr)
1627 {
1629  auto &ret = static_cast<const array_list_exprt &>(expr);
1630  validate_expr(ret);
1631  return ret;
1632 }
1633 
1635 {
1637  auto &ret = static_cast<array_list_exprt &>(expr);
1638  validate_expr(ret);
1639  return ret;
1640 }
1641 
1644 {
1645 public:
1646  DEPRECATED(SINCE(2019, 1, 12, "use vector_exprt(operands, type) instead"))
1647  explicit vector_exprt(const vector_typet &_type)
1648  : multi_ary_exprt(ID_vector, _type)
1649  {
1650  }
1651 
1653  : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1654  {
1655  }
1656 };
1657 
1658 template <>
1659 inline bool can_cast_expr<vector_exprt>(const exprt &base)
1660 {
1661  return base.id() == ID_vector;
1662 }
1663 
1670 inline const vector_exprt &to_vector_expr(const exprt &expr)
1671 {
1672  PRECONDITION(expr.id()==ID_vector);
1673  return static_cast<const vector_exprt &>(expr);
1674 }
1675 
1678 {
1679  PRECONDITION(expr.id()==ID_vector);
1680  return static_cast<vector_exprt &>(expr);
1681 }
1682 
1683 
1686 {
1687 public:
1688  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1689  : unary_exprt(ID_union, std::move(_value), std::move(_type))
1690  {
1691  set_component_name(_component_name);
1692  }
1693 
1695  {
1696  return get(ID_component_name);
1697  }
1698 
1699  void set_component_name(const irep_idt &component_name)
1700  {
1701  set(ID_component_name, component_name);
1702  }
1703 
1704  std::size_t get_component_number() const
1705  {
1706  return get_size_t(ID_component_number);
1707  }
1708 
1709  void set_component_number(std::size_t component_number)
1710  {
1711  set(ID_component_number, narrow_cast<long long>(component_number));
1712  }
1713 };
1714 
1715 template <>
1716 inline bool can_cast_expr<union_exprt>(const exprt &base)
1717 {
1718  return base.id() == ID_union;
1719 }
1720 
1721 inline void validate_expr(const union_exprt &value)
1722 {
1723  validate_operands(value, 1, "Union constructor must have one operand");
1724 }
1725 
1732 inline const union_exprt &to_union_expr(const exprt &expr)
1733 {
1734  PRECONDITION(expr.id()==ID_union);
1735  const union_exprt &ret = static_cast<const union_exprt &>(expr);
1736  validate_expr(ret);
1737  return ret;
1738 }
1739 
1742 {
1743  PRECONDITION(expr.id()==ID_union);
1744  union_exprt &ret = static_cast<union_exprt &>(expr);
1745  validate_expr(ret);
1746  return ret;
1747 }
1748 
1749 
1752 {
1753 public:
1754  DEPRECATED(
1755  SINCE(2018, 9, 21, "use struct_exprt(component_name, value, type) instead"))
1757  {
1758  }
1759 
1760  DEPRECATED(
1761  SINCE(2019, 1, 12, "use struct_exprt(component_name, value, type) instead"))
1762  explicit struct_exprt(const typet &_type) : multi_ary_exprt(ID_struct, _type)
1763  {
1764  }
1765 
1766  struct_exprt(operandst _operands, typet _type)
1767  : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1768  {
1769  }
1770 
1771  exprt &component(const irep_idt &name, const namespacet &ns);
1772  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1773 };
1774 
1775 template <>
1776 inline bool can_cast_expr<struct_exprt>(const exprt &base)
1777 {
1778  return base.id() == ID_struct;
1779 }
1780 
1787 inline const struct_exprt &to_struct_expr(const exprt &expr)
1788 {
1789  PRECONDITION(expr.id()==ID_struct);
1790  return static_cast<const struct_exprt &>(expr);
1791 }
1792 
1795 {
1796  PRECONDITION(expr.id()==ID_struct);
1797  return static_cast<struct_exprt &>(expr);
1798 }
1799 
1800 
1803 {
1804 public:
1806  : binary_exprt(
1807  std::move(_real),
1808  ID_complex,
1809  std::move(_imag),
1810  std::move(_type))
1811  {
1812  }
1813 
1815  {
1816  return op0();
1817  }
1818 
1819  const exprt &real() const
1820  {
1821  return op0();
1822  }
1823 
1825  {
1826  return op1();
1827  }
1828 
1829  const exprt &imag() const
1830  {
1831  return op1();
1832  }
1833 };
1834 
1835 template <>
1836 inline bool can_cast_expr<complex_exprt>(const exprt &base)
1837 {
1838  return base.id() == ID_complex;
1839 }
1840 
1841 inline void validate_expr(const complex_exprt &value)
1842 {
1843  validate_operands(value, 2, "Complex constructor must have two operands");
1844 }
1845 
1852 inline const complex_exprt &to_complex_expr(const exprt &expr)
1853 {
1854  PRECONDITION(expr.id()==ID_complex);
1855  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1856  validate_expr(ret);
1857  return ret;
1858 }
1859 
1862 {
1863  PRECONDITION(expr.id()==ID_complex);
1864  complex_exprt &ret = static_cast<complex_exprt &>(expr);
1865  validate_expr(ret);
1866  return ret;
1867 }
1868 
1871 {
1872 public:
1873  explicit complex_real_exprt(const exprt &op)
1874  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1875  {
1876  }
1877 };
1878 
1879 template <>
1881 {
1882  return base.id() == ID_complex_real;
1883 }
1884 
1885 inline void validate_expr(const complex_real_exprt &expr)
1886 {
1888  expr, 1, "real part retrieval operation must have one operand");
1889 }
1890 
1898 {
1899  PRECONDITION(expr.id() == ID_complex_real);
1900  const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
1901  validate_expr(ret);
1902  return ret;
1903 }
1904 
1907 {
1908  PRECONDITION(expr.id() == ID_complex_real);
1909  complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
1910  validate_expr(ret);
1911  return ret;
1912 }
1913 
1916 {
1917 public:
1918  explicit complex_imag_exprt(const exprt &op)
1919  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
1920  {
1921  }
1922 };
1923 
1924 template <>
1926 {
1927  return base.id() == ID_complex_imag;
1928 }
1929 
1930 inline void validate_expr(const complex_imag_exprt &expr)
1931 {
1933  expr, 1, "imaginary part retrieval operation must have one operand");
1934 }
1935 
1943 {
1944  PRECONDITION(expr.id() == ID_complex_imag);
1945  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
1946  validate_expr(ret);
1947  return ret;
1948 }
1949 
1952 {
1953  PRECONDITION(expr.id() == ID_complex_imag);
1954  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
1955  validate_expr(ret);
1956  return ret;
1957 }
1958 
1959 class namespacet;
1960 
1963 {
1964 public:
1966  : binary_exprt(
1967  exprt(ID_unknown),
1968  ID_object_descriptor,
1969  exprt(ID_unknown),
1970  typet())
1971  {
1972  }
1973 
1974  explicit object_descriptor_exprt(exprt _object)
1975  : binary_exprt(
1976  std::move(_object),
1977  ID_object_descriptor,
1978  exprt(ID_unknown),
1979  typet())
1980  {
1981  }
1982 
1987  void build(const exprt &expr, const namespacet &ns);
1988 
1990  {
1991  return op0();
1992  }
1993 
1994  const exprt &object() const
1995  {
1996  return op0();
1997  }
1998 
1999  const exprt &root_object() const;
2000 
2002  {
2003  return op1();
2004  }
2005 
2006  const exprt &offset() const
2007  {
2008  return op1();
2009  }
2010 };
2011 
2012 template <>
2014 {
2015  return base.id() == ID_object_descriptor;
2016 }
2017 
2018 inline void validate_expr(const object_descriptor_exprt &value)
2019 {
2020  validate_operands(value, 2, "Object descriptor must have two operands");
2021 }
2022 
2030  const exprt &expr)
2031 {
2032  PRECONDITION(expr.id()==ID_object_descriptor);
2033  const object_descriptor_exprt &ret =
2034  static_cast<const object_descriptor_exprt &>(expr);
2035  validate_expr(ret);
2036  return ret;
2037 }
2038 
2041 {
2042  PRECONDITION(expr.id()==ID_object_descriptor);
2043  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
2044  validate_expr(ret);
2045  return ret;
2046 }
2047 
2048 
2051 {
2052 public:
2053  DEPRECATED(SINCE(2019, 2, 11, "use dynamic_object_exprt(type) instead"))
2055  : binary_exprt(exprt(ID_unknown), ID_dynamic_object, exprt(ID_unknown))
2056  {
2057  }
2058 
2060  : binary_exprt(
2061  exprt(ID_unknown),
2062  ID_dynamic_object,
2063  exprt(ID_unknown),
2064  std::move(type))
2065  {
2066  }
2067 
2068  void set_instance(unsigned int instance);
2069 
2070  unsigned int get_instance() const;
2071 
2073  {
2074  return op1();
2075  }
2076 
2077  const exprt &valid() const
2078  {
2079  return op1();
2080  }
2081 };
2082 
2083 template <>
2085 {
2086  return base.id() == ID_dynamic_object;
2087 }
2088 
2089 inline void validate_expr(const dynamic_object_exprt &value)
2090 {
2091  validate_operands(value, 2, "Dynamic object must have two operands");
2092 }
2093 
2101  const exprt &expr)
2102 {
2103  PRECONDITION(expr.id()==ID_dynamic_object);
2104  const dynamic_object_exprt &ret =
2105  static_cast<const dynamic_object_exprt &>(expr);
2106  validate_expr(ret);
2107  return ret;
2108 }
2109 
2112 {
2113  PRECONDITION(expr.id()==ID_dynamic_object);
2114  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
2115  validate_expr(ret);
2116  return ret;
2117 }
2118 
2121 {
2122 public:
2124  {
2125  }
2126 
2128  : unary_predicate_exprt(ID_is_dynamic_object, op)
2129  {
2130  }
2131 };
2132 
2133 inline const is_dynamic_object_exprt &
2135 {
2136  PRECONDITION(expr.id() == ID_is_dynamic_object);
2138  expr.operands().size() == 1, "is_dynamic_object must have one operand");
2139  return static_cast<const is_dynamic_object_exprt &>(expr);
2140 }
2141 
2145 {
2146  PRECONDITION(expr.id() == ID_is_dynamic_object);
2148  expr.operands().size() == 1, "is_dynamic_object must have one operand");
2149  return static_cast<is_dynamic_object_exprt &>(expr);
2150 }
2151 
2154 {
2155 public:
2157  : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2158  {
2159  }
2160 
2161  // returns a typecast if the type doesn't already match
2162  static exprt conditional_cast(const exprt &expr, const typet &type)
2163  {
2164  if(expr.type() == type)
2165  return expr;
2166  else
2167  return typecast_exprt(expr, type);
2168  }
2169 };
2170 
2171 template <>
2172 inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2173 {
2174  return base.id() == ID_typecast;
2175 }
2176 
2177 inline void validate_expr(const typecast_exprt &value)
2178 {
2179  validate_operands(value, 1, "Typecast must have one operand");
2180 }
2181 
2188 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2189 {
2190  PRECONDITION(expr.id()==ID_typecast);
2191  const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
2192  validate_expr(ret);
2193  return ret;
2194 }
2195 
2198 {
2199  PRECONDITION(expr.id()==ID_typecast);
2200  typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
2201  validate_expr(ret);
2202  return ret;
2203 }
2204 
2205 
2208 {
2209 public:
2211  : binary_exprt(
2212  std::move(op),
2213  ID_floatbv_typecast,
2214  std::move(rounding),
2215  std::move(_type))
2216  {
2217  }
2218 
2220  {
2221  return op0();
2222  }
2223 
2224  const exprt &op() const
2225  {
2226  return op0();
2227  }
2228 
2230  {
2231  return op1();
2232  }
2233 
2234  const exprt &rounding_mode() const
2235  {
2236  return op1();
2237  }
2238 };
2239 
2240 template <>
2242 {
2243  return base.id() == ID_floatbv_typecast;
2244 }
2245 
2246 inline void validate_expr(const floatbv_typecast_exprt &value)
2247 {
2248  validate_operands(value, 2, "Float typecast must have two operands");
2249 }
2250 
2258 {
2259  PRECONDITION(expr.id()==ID_floatbv_typecast);
2260  const floatbv_typecast_exprt &ret =
2261  static_cast<const floatbv_typecast_exprt &>(expr);
2262  validate_expr(ret);
2263  return ret;
2264 }
2265 
2268 {
2269  PRECONDITION(expr.id()==ID_floatbv_typecast);
2270  floatbv_typecast_exprt &ret = static_cast<floatbv_typecast_exprt &>(expr);
2271  validate_expr(ret);
2272  return ret;
2273 }
2274 
2275 
2278 {
2279 public:
2280  DEPRECATED(SINCE(2019, 1, 12, "use and_exprt(op, op) instead"))
2282  {
2283  }
2284 
2286  : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2287  {
2288  }
2289 
2291  : multi_ary_exprt(
2292  ID_and,
2293  {std::move(op0), std::move(op1), std::move(op2)},
2294  bool_typet())
2295  {
2296  }
2297 
2299  : multi_ary_exprt(
2300  ID_and,
2301  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2302  bool_typet())
2303  {
2304  }
2305 
2306  explicit and_exprt(exprt::operandst _operands)
2307  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2308  {
2309  }
2310 };
2311 
2315 
2317 
2318 template <>
2319 inline bool can_cast_expr<and_exprt>(const exprt &base)
2320 {
2321  return base.id() == ID_and;
2322 }
2323 
2330 inline const and_exprt &to_and_expr(const exprt &expr)
2331 {
2332  PRECONDITION(expr.id()==ID_and);
2333  return static_cast<const and_exprt &>(expr);
2334 }
2335 
2338 {
2339  PRECONDITION(expr.id()==ID_and);
2340  return static_cast<and_exprt &>(expr);
2341 }
2342 
2343 
2346 {
2347 public:
2349  : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2350  {
2351  }
2352 };
2353 
2354 template <>
2355 inline bool can_cast_expr<implies_exprt>(const exprt &base)
2356 {
2357  return base.id() == ID_implies;
2358 }
2359 
2360 inline void validate_expr(const implies_exprt &value)
2361 {
2362  validate_operands(value, 2, "Implies must have two operands");
2363 }
2364 
2371 inline const implies_exprt &to_implies_expr(const exprt &expr)
2372 {
2373  PRECONDITION(expr.id()==ID_implies);
2374  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2375  validate_expr(ret);
2376  return ret;
2377 }
2378 
2381 {
2382  PRECONDITION(expr.id()==ID_implies);
2383  implies_exprt &ret = static_cast<implies_exprt &>(expr);
2384  validate_expr(ret);
2385  return ret;
2386 }
2387 
2388 
2391 {
2392 public:
2393  DEPRECATED(SINCE(2019, 1, 12, "use or_exprt(op, op) instead"))
2395  {
2396  }
2397 
2399  : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2400  {
2401  }
2402 
2404  : multi_ary_exprt(
2405  ID_or,
2406  {std::move(op0), std::move(op1), std::move(op2)},
2407  bool_typet())
2408  {
2409  }
2410 
2412  : multi_ary_exprt(
2413  ID_or,
2414  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2415  bool_typet())
2416  {
2417  }
2418 
2419  explicit or_exprt(exprt::operandst _operands)
2420  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2421  {
2422  }
2423 };
2424 
2428 
2430 
2431 template <>
2432 inline bool can_cast_expr<or_exprt>(const exprt &base)
2433 {
2434  return base.id() == ID_or;
2435 }
2436 
2443 inline const or_exprt &to_or_expr(const exprt &expr)
2444 {
2445  PRECONDITION(expr.id()==ID_or);
2446  return static_cast<const or_exprt &>(expr);
2447 }
2448 
2450 inline or_exprt &to_or_expr(exprt &expr)
2451 {
2452  PRECONDITION(expr.id()==ID_or);
2453  return static_cast<or_exprt &>(expr);
2454 }
2455 
2456 
2459 {
2460 public:
2461  DEPRECATED(SINCE(2019, 1, 12, "use xor_exprt(op, op) instead"))
2463  {
2464  }
2465 
2466  xor_exprt(exprt _op0, exprt _op1)
2467  : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2468  {
2469  }
2470 };
2471 
2472 template <>
2473 inline bool can_cast_expr<xor_exprt>(const exprt &base)
2474 {
2475  return base.id() == ID_xor;
2476 }
2477 
2484 inline const xor_exprt &to_xor_expr(const exprt &expr)
2485 {
2486  PRECONDITION(expr.id()==ID_xor);
2487  return static_cast<const xor_exprt &>(expr);
2488 }
2489 
2492 {
2493  PRECONDITION(expr.id()==ID_xor);
2494  return static_cast<xor_exprt &>(expr);
2495 }
2496 
2497 
2500 {
2501 public:
2502  explicit bitnot_exprt(exprt op) : unary_exprt(ID_bitnot, std::move(op))
2503  {
2504  }
2505 };
2506 
2507 template <>
2508 inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
2509 {
2510  return base.id() == ID_bitnot;
2511 }
2512 
2513 inline void validate_expr(const bitnot_exprt &value)
2514 {
2515  validate_operands(value, 1, "Bit-wise not must have one operand");
2516 }
2517 
2524 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
2525 {
2526  PRECONDITION(expr.id()==ID_bitnot);
2527  const bitnot_exprt &ret = static_cast<const bitnot_exprt &>(expr);
2528  validate_expr(ret);
2529  return ret;
2530 }
2531 
2534 {
2535  PRECONDITION(expr.id()==ID_bitnot);
2536  bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
2537  validate_expr(ret);
2538  return ret;
2539 }
2540 
2541 
2544 {
2545 public:
2546  bitor_exprt(const exprt &_op0, exprt _op1)
2547  : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
2548  {
2549  }
2550 };
2551 
2552 template <>
2553 inline bool can_cast_expr<bitor_exprt>(const exprt &base)
2554 {
2555  return base.id() == ID_bitor;
2556 }
2557 
2564 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
2565 {
2566  PRECONDITION(expr.id()==ID_bitor);
2567  return static_cast<const bitor_exprt &>(expr);
2568 }
2569 
2572 {
2573  PRECONDITION(expr.id()==ID_bitor);
2574  return static_cast<bitor_exprt &>(expr);
2575 }
2576 
2577 
2580 {
2581 public:
2583  : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
2584  {
2585  }
2586 };
2587 
2588 template <>
2589 inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
2590 {
2591  return base.id() == ID_bitxor;
2592 }
2593 
2600 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
2601 {
2602  PRECONDITION(expr.id()==ID_bitxor);
2603  return static_cast<const bitxor_exprt &>(expr);
2604 }
2605 
2608 {
2609  PRECONDITION(expr.id()==ID_bitxor);
2610  return static_cast<bitxor_exprt &>(expr);
2611 }
2612 
2613 
2616 {
2617 public:
2618  bitand_exprt(const exprt &_op0, exprt _op1)
2619  : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
2620  {
2621  }
2622 };
2623 
2624 template <>
2625 inline bool can_cast_expr<bitand_exprt>(const exprt &base)
2626 {
2627  return base.id() == ID_bitand;
2628 }
2629 
2636 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
2637 {
2638  PRECONDITION(expr.id()==ID_bitand);
2639  return static_cast<const bitand_exprt &>(expr);
2640 }
2641 
2644 {
2645  PRECONDITION(expr.id()==ID_bitand);
2646  return static_cast<bitand_exprt &>(expr);
2647 }
2648 
2649 
2652 {
2653 public:
2654  shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
2655  : binary_exprt(std::move(_src), _id, std::move(_distance))
2656  {
2657  }
2658 
2659  shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
2660 
2662  {
2663  return op0();
2664  }
2665 
2666  const exprt &op() const
2667  {
2668  return op0();
2669  }
2670 
2672  {
2673  return op1();
2674  }
2675 
2676  const exprt &distance() const
2677  {
2678  return op1();
2679  }
2680 };
2681 
2682 template <>
2683 inline bool can_cast_expr<shift_exprt>(const exprt &base)
2684 {
2685  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr;
2686 }
2687 
2688 inline void validate_expr(const shift_exprt &value)
2689 {
2690  validate_operands(value, 2, "Shifts must have two operands");
2691 }
2692 
2699 inline const shift_exprt &to_shift_expr(const exprt &expr)
2700 {
2701  const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
2702  validate_expr(ret);
2703  return ret;
2704 }
2705 
2708 {
2709  shift_exprt &ret = static_cast<shift_exprt &>(expr);
2710  validate_expr(ret);
2711  return ret;
2712 }
2713 
2714 
2717 {
2718 public:
2719  shl_exprt(exprt _src, exprt _distance)
2720  : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
2721  {
2722  }
2723 
2724  shl_exprt(exprt _src, const std::size_t _distance)
2725  : shift_exprt(std::move(_src), ID_shl, _distance)
2726  {
2727  }
2728 };
2729 
2736 inline const shl_exprt &to_shl_expr(const exprt &expr)
2737 {
2738  PRECONDITION(expr.id() == ID_shl);
2739  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
2740  validate_expr(ret);
2741  return ret;
2742 }
2743 
2746 {
2747  PRECONDITION(expr.id() == ID_shl);
2748  shl_exprt &ret = static_cast<shl_exprt &>(expr);
2749  validate_expr(ret);
2750  return ret;
2751 }
2752 
2755 {
2756 public:
2757  ashr_exprt(exprt _src, exprt _distance)
2758  : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
2759  {
2760  }
2761 
2762  ashr_exprt(exprt _src, const std::size_t _distance)
2763  : shift_exprt(std::move(_src), ID_ashr, _distance)
2764  {
2765  }
2766 };
2767 
2770 {
2771 public:
2772  lshr_exprt(exprt _src, exprt _distance)
2773  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2774  {
2775  }
2776 
2777  lshr_exprt(exprt _src, const std::size_t _distance)
2778  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2779  {
2780  }
2781 };
2782 
2785 {
2786 public:
2789  : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
2790  {
2791  }
2792 
2793  extractbit_exprt(exprt _src, const std::size_t _index);
2794 
2796  {
2797  return op0();
2798  }
2799 
2801  {
2802  return op1();
2803  }
2804 
2805  const exprt &src() const
2806  {
2807  return op0();
2808  }
2809 
2810  const exprt &index() const
2811  {
2812  return op1();
2813  }
2814 };
2815 
2816 template <>
2817 inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
2818 {
2819  return base.id() == ID_extractbit;
2820 }
2821 
2822 inline void validate_expr(const extractbit_exprt &value)
2823 {
2824  validate_operands(value, 2, "Extract bit must have two operands");
2825 }
2826 
2833 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
2834 {
2835  PRECONDITION(expr.id()==ID_extractbit);
2836  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
2837  validate_expr(ret);
2838  return ret;
2839 }
2840 
2843 {
2844  PRECONDITION(expr.id()==ID_extractbit);
2845  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
2846  validate_expr(ret);
2847  return ret;
2848 }
2849 
2850 
2853 {
2854 public:
2860  extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
2861  : expr_protectedt(
2862  ID_extractbits,
2863  std::move(_type),
2864  {std::move(_src), std::move(_upper), std::move(_lower)})
2865  {
2866  }
2867 
2869  exprt _src,
2870  const std::size_t _upper,
2871  const std::size_t _lower,
2872  typet _type);
2873 
2875  {
2876  return op0();
2877  }
2878 
2880  {
2881  return op1();
2882  }
2883 
2885  {
2886  return op2();
2887  }
2888 
2889  const exprt &src() const
2890  {
2891  return op0();
2892  }
2893 
2894  const exprt &upper() const
2895  {
2896  return op1();
2897  }
2898 
2899  const exprt &lower() const
2900  {
2901  return op2();
2902  }
2903 };
2904 
2905 template <>
2906 inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
2907 {
2908  return base.id() == ID_extractbits;
2909 }
2910 
2911 inline void validate_expr(const extractbits_exprt &value)
2912 {
2913  validate_operands(value, 3, "Extract bits must have three operands");
2914 }
2915 
2922 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
2923 {
2924  PRECONDITION(expr.id()==ID_extractbits);
2925  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
2926  validate_expr(ret);
2927  return ret;
2928 }
2929 
2932 {
2933  PRECONDITION(expr.id()==ID_extractbits);
2934  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
2935  validate_expr(ret);
2936  return ret;
2937 }
2938 
2939 
2942 {
2943 public:
2944  explicit address_of_exprt(const exprt &op);
2945 
2947  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
2948  {
2949  }
2950 
2952  {
2953  return op0();
2954  }
2955 
2956  const exprt &object() const
2957  {
2958  return op0();
2959  }
2960 };
2961 
2962 template <>
2963 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
2964 {
2965  return base.id() == ID_address_of;
2966 }
2967 
2968 inline void validate_expr(const address_of_exprt &value)
2969 {
2970  validate_operands(value, 1, "Address of must have one operand");
2971 }
2972 
2979 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
2980 {
2981  PRECONDITION(expr.id()==ID_address_of);
2982  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
2983  validate_expr(ret);
2984  return ret;
2985 }
2986 
2989 {
2990  PRECONDITION(expr.id()==ID_address_of);
2991  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
2992  validate_expr(ret);
2993  return ret;
2994 }
2995 
2996 
2999 {
3000 public:
3001  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
3002  {
3003  PRECONDITION(as_const(*this).op().type().id() == ID_bool);
3004  }
3005 
3006  DEPRECATED(SINCE(2019, 1, 12, "use not_exprt(op) instead"))
3008  {
3009  }
3010 };
3011 
3012 template <>
3013 inline bool can_cast_expr<not_exprt>(const exprt &base)
3014 {
3015  return base.id() == ID_not;
3016 }
3017 
3018 inline void validate_expr(const not_exprt &value)
3019 {
3020  validate_operands(value, 1, "Not must have one operand");
3021 }
3022 
3029 inline const not_exprt &to_not_expr(const exprt &expr)
3030 {
3031  PRECONDITION(expr.id()==ID_not);
3032  const not_exprt &ret = static_cast<const not_exprt &>(expr);
3033  validate_expr(ret);
3034  return ret;
3035 }
3036 
3039 {
3040  PRECONDITION(expr.id()==ID_not);
3041  not_exprt &ret = static_cast<not_exprt &>(expr);
3042  validate_expr(ret);
3043  return ret;
3044 }
3045 
3046 
3049 {
3050 public:
3051  explicit dereference_exprt(const exprt &op):
3052  unary_exprt(ID_dereference, op, op.type().subtype())
3053  {
3054  PRECONDITION(op.type().id()==ID_pointer);
3055  }
3056 
3058  : unary_exprt(ID_dereference, std::move(op), std::move(type))
3059  {
3060  }
3061 
3063  {
3064  return op0();
3065  }
3066 
3067  const exprt &pointer() const
3068  {
3069  return op0();
3070  }
3071 
3072  static void check(
3073  const exprt &expr,
3075  {
3076  DATA_CHECK(
3077  vm,
3078  expr.operands().size() == 1,
3079  "dereference expression must have one operand");
3080  }
3081 
3082  static void validate(
3083  const exprt &expr,
3084  const namespacet &ns,
3086 };
3087 
3088 template <>
3089 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
3090 {
3091  return base.id() == ID_dereference;
3092 }
3093 
3094 inline void validate_expr(const dereference_exprt &value)
3095 {
3096  validate_operands(value, 1, "Dereference must have one operand");
3097 }
3098 
3105 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
3106 {
3107  PRECONDITION(expr.id()==ID_dereference);
3108  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
3109  validate_expr(ret);
3110  return ret;
3111 }
3112 
3115 {
3116  PRECONDITION(expr.id()==ID_dereference);
3117  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
3118  validate_expr(ret);
3119  return ret;
3120 }
3121 
3122 
3124 class if_exprt : public ternary_exprt
3125 {
3126 public:
3128  : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
3129  {
3130  }
3131 
3133  : ternary_exprt(
3134  ID_if,
3135  std::move(cond),
3136  std::move(t),
3137  std::move(f),
3138  std::move(type))
3139  {
3140  }
3141 
3143  {
3144  return op0();
3145  }
3146 
3147  const exprt &cond() const
3148  {
3149  return op0();
3150  }
3151 
3153  {
3154  return op1();
3155  }
3156 
3157  const exprt &true_case() const
3158  {
3159  return op1();
3160  }
3161 
3163  {
3164  return op2();
3165  }
3166 
3167  const exprt &false_case() const
3168  {
3169  return op2();
3170  }
3171 };
3172 
3173 template <>
3174 inline bool can_cast_expr<if_exprt>(const exprt &base)
3175 {
3176  return base.id() == ID_if;
3177 }
3178 
3179 inline void validate_expr(const if_exprt &value)
3180 {
3181  validate_operands(value, 3, "If-then-else must have three operands");
3182 }
3183 
3190 inline const if_exprt &to_if_expr(const exprt &expr)
3191 {
3192  PRECONDITION(expr.id()==ID_if);
3193  const if_exprt &ret = static_cast<const if_exprt &>(expr);
3194  validate_expr(ret);
3195  return ret;
3196 }
3197 
3199 inline if_exprt &to_if_expr(exprt &expr)
3200 {
3201  PRECONDITION(expr.id()==ID_if);
3202  if_exprt &ret = static_cast<if_exprt &>(expr);
3203  validate_expr(ret);
3204  return ret;
3205 }
3206 
3211 {
3212 public:
3213  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
3214  : expr_protectedt(
3215  ID_with,
3216  _old.type(),
3217  {_old, std::move(_where), std::move(_new_value)})
3218  {
3219  }
3220 
3222  {
3223  return op0();
3224  }
3225 
3226  const exprt &old() const
3227  {
3228  return op0();
3229  }
3230 
3232  {
3233  return op1();
3234  }
3235 
3236  const exprt &where() const
3237  {
3238  return op1();
3239  }
3240 
3242  {
3243  return op2();
3244  }
3245 
3246  const exprt &new_value() const
3247  {
3248  return op2();
3249  }
3250 };
3251 
3252 template <>
3253 inline bool can_cast_expr<with_exprt>(const exprt &base)
3254 {
3255  return base.id() == ID_with;
3256 }
3257 
3258 inline void validate_expr(const with_exprt &value)
3259 {
3261  value, 3, "array/structure update must have at least 3 operands", true);
3263  value.operands().size() % 2 == 1,
3264  "array/structure update must have an odd number of operands");
3265 }
3266 
3273 inline const with_exprt &to_with_expr(const exprt &expr)
3274 {
3275  PRECONDITION(expr.id()==ID_with);
3276  const with_exprt &ret = static_cast<const with_exprt &>(expr);
3277  validate_expr(ret);
3278  return ret;
3279 }
3280 
3283 {
3284  PRECONDITION(expr.id()==ID_with);
3285  with_exprt &ret = static_cast<with_exprt &>(expr);
3286  validate_expr(ret);
3287  return ret;
3288 }
3289 
3291 {
3292 public:
3293  explicit index_designatort(exprt _index)
3294  : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
3295  {
3296  }
3297 
3298  const exprt &index() const
3299  {
3300  return op0();
3301  }
3302 
3304  {
3305  return op0();
3306  }
3307 };
3308 
3309 template <>
3310 inline bool can_cast_expr<index_designatort>(const exprt &base)
3311 {
3312  return base.id() == ID_index_designator;
3313 }
3314 
3315 inline void validate_expr(const index_designatort &value)
3316 {
3317  validate_operands(value, 1, "Index designator must have one operand");
3318 }
3319 
3326 inline const index_designatort &to_index_designator(const exprt &expr)
3327 {
3328  PRECONDITION(expr.id()==ID_index_designator);
3329  const index_designatort &ret = static_cast<const index_designatort &>(expr);
3330  validate_expr(ret);
3331  return ret;
3332 }
3333 
3336 {
3337  PRECONDITION(expr.id()==ID_index_designator);
3338  index_designatort &ret = static_cast<index_designatort &>(expr);
3339  validate_expr(ret);
3340  return ret;
3341 }
3342 
3344 {
3345 public:
3346  explicit member_designatort(const irep_idt &_component_name)
3347  : expr_protectedt(ID_member_designator, typet())
3348  {
3349  set(ID_component_name, _component_name);
3350  }
3351 
3353  {
3354  return get(ID_component_name);
3355  }
3356 };
3357 
3358 template <>
3360 {
3361  return base.id() == ID_member_designator;
3362 }
3363 
3364 inline void validate_expr(const member_designatort &value)
3365 {
3366  validate_operands(value, 0, "Member designator must not have operands");
3367 }
3368 
3376 {
3377  PRECONDITION(expr.id()==ID_member_designator);
3378  const member_designatort &ret = static_cast<const member_designatort &>(expr);
3379  validate_expr(ret);
3380  return ret;
3381 }
3382 
3385 {
3386  PRECONDITION(expr.id()==ID_member_designator);
3387  member_designatort &ret = static_cast<member_designatort &>(expr);
3388  validate_expr(ret);
3389  return ret;
3390 }
3391 
3392 
3395 {
3396 public:
3397  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
3398  : ternary_exprt(
3399  ID_update,
3400  _old,
3401  std::move(_designator),
3402  std::move(_new_value),
3403  _old.type())
3404  {
3405  }
3406 
3408  {
3409  return op0();
3410  }
3411 
3412  const exprt &old() const
3413  {
3414  return op0();
3415  }
3416 
3417  // the designator operands are either
3418  // 1) member_designator or
3419  // 2) index_designator
3420  // as defined above
3422  {
3423  return op1().operands();
3424  }
3425 
3427  {
3428  return op1().operands();
3429  }
3430 
3432  {
3433  return op2();
3434  }
3435 
3436  const exprt &new_value() const
3437  {
3438  return op2();
3439  }
3440 };
3441 
3442 template <>
3443 inline bool can_cast_expr<update_exprt>(const exprt &base)
3444 {
3445  return base.id() == ID_update;
3446 }
3447 
3448 inline void validate_expr(const update_exprt &value)
3449 {
3451  value, 3, "Array/structure update must have three operands");
3452 }
3453 
3460 inline const update_exprt &to_update_expr(const exprt &expr)
3461 {
3462  PRECONDITION(expr.id()==ID_update);
3463  const update_exprt &ret = static_cast<const update_exprt &>(expr);
3464  validate_expr(ret);
3465  return ret;
3466 }
3467 
3470 {
3471  PRECONDITION(expr.id()==ID_update);
3472  update_exprt &ret = static_cast<update_exprt &>(expr);
3473  validate_expr(ret);
3474  return ret;
3475 }
3476 
3477 
3478 #if 0
3479 class array_update_exprt:public expr_protectedt
3481 {
3482 public:
3483  array_update_exprt(
3484  const exprt &_array,
3485  const exprt &_index,
3486  const exprt &_new_value):
3487  exprt(ID_array_update, _array.type())
3488  {
3489  add_to_operands(_array, _index, _new_value);
3490  }
3491 
3492  array_update_exprt():expr_protectedt(ID_array_update)
3493  {
3494  operands().resize(3);
3495  }
3496 
3497  exprt &array()
3498  {
3499  return op0();
3500  }
3501 
3502  const exprt &array() const
3503  {
3504  return op0();
3505  }
3506 
3507  exprt &index()
3508  {
3509  return op1();
3510  }
3511 
3512  const exprt &index() const
3513  {
3514  return op1();
3515  }
3516 
3517  exprt &new_value()
3518  {
3519  return op2();
3520  }
3521 
3522  const exprt &new_value() const
3523  {
3524  return op2();
3525  }
3526 };
3527 
3528 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
3529 {
3530  return base.id()==ID_array_update;
3531 }
3532 
3533 inline void validate_expr(const array_update_exprt &value)
3534 {
3535  validate_operands(value, 3, "Array update must have three operands");
3536 }
3537 
3544 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3545 {
3546  PRECONDITION(expr.id()==ID_array_update);
3547  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
3548  validate_expr(ret);
3549  return ret;
3550 }
3551 
3553 inline array_update_exprt &to_array_update_expr(exprt &expr)
3554 {
3555  PRECONDITION(expr.id()==ID_array_update);
3556  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
3557  validate_expr(ret);
3558  return ret;
3559 }
3560 
3561 #endif
3562 
3563 
3566 {
3567 public:
3568  member_exprt(exprt op, const irep_idt &component_name, typet _type)
3569  : unary_exprt(ID_member, std::move(op), std::move(_type))
3570  {
3571  set_component_name(component_name);
3572  }
3573 
3575  : unary_exprt(ID_member, std::move(op), c.type())
3576  {
3578  }
3579 
3581  {
3582  return get(ID_component_name);
3583  }
3584 
3585  void set_component_name(const irep_idt &component_name)
3586  {
3587  set(ID_component_name, component_name);
3588  }
3589 
3590  std::size_t get_component_number() const
3591  {
3592  return get_size_t(ID_component_number);
3593  }
3594 
3595  // will go away, use compound()
3596  const exprt &struct_op() const
3597  {
3598  return op0();
3599  }
3600 
3601  // will go away, use compound()
3603  {
3604  return op0();
3605  }
3606 
3607  const exprt &compound() const
3608  {
3609  return op0();
3610  }
3611 
3613  {
3614  return op0();
3615  }
3616 
3617  static void check(
3618  const exprt &expr,
3620  {
3621  DATA_CHECK(
3622  vm,
3623  expr.operands().size() == 1,
3624  "member expression must have one operand");
3625  }
3626 
3627  static void validate(
3628  const exprt &expr,
3629  const namespacet &ns,
3631 };
3632 
3633 template <>
3634 inline bool can_cast_expr<member_exprt>(const exprt &base)
3635 {
3636  return base.id() == ID_member;
3637 }
3638 
3639 inline void validate_expr(const member_exprt &value)
3640 {
3641  validate_operands(value, 1, "Extract member must have one operand");
3642 }
3643 
3650 inline const member_exprt &to_member_expr(const exprt &expr)
3651 {
3652  PRECONDITION(expr.id()==ID_member);
3653  const member_exprt &ret = static_cast<const member_exprt &>(expr);
3654  validate_expr(ret);
3655  return ret;
3656 }
3657 
3660 {
3661  PRECONDITION(expr.id()==ID_member);
3662  member_exprt &ret = static_cast<member_exprt &>(expr);
3663  validate_expr(ret);
3664  return ret;
3665 }
3666 
3667 
3670 {
3671 public:
3673  : unary_predicate_exprt(ID_isnan, std::move(op))
3674  {
3675  }
3676 
3677  DEPRECATED(SINCE(2018, 12, 2, "use isnan_exprt(op) instead"))
3679  {
3680  }
3681 };
3682 
3683 template <>
3684 inline bool can_cast_expr<isnan_exprt>(const exprt &base)
3685 {
3686  return base.id() == ID_isnan;
3687 }
3688 
3689 inline void validate_expr(const isnan_exprt &value)
3690 {
3691  validate_operands(value, 1, "Is NaN must have one operand");
3692 }
3693 
3700 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
3701 {
3702  PRECONDITION(expr.id()==ID_isnan);
3703  const isnan_exprt &ret = static_cast<const isnan_exprt &>(expr);
3704  validate_expr(ret);
3705  return ret;
3706 }
3707 
3710 {
3711  PRECONDITION(expr.id()==ID_isnan);
3712  isnan_exprt &ret = static_cast<isnan_exprt &>(expr);
3713  validate_expr(ret);
3714  return ret;
3715 }
3716 
3717 
3720 {
3721 public:
3723  : unary_predicate_exprt(ID_isinf, std::move(op))
3724  {
3725  }
3726 
3727  DEPRECATED(SINCE(2018, 12, 2, "use isinf_exprt(op) instead"))
3729  {
3730  }
3731 };
3732 
3733 template <>
3734 inline bool can_cast_expr<isinf_exprt>(const exprt &base)
3735 {
3736  return base.id() == ID_isinf;
3737 }
3738 
3739 inline void validate_expr(const isinf_exprt &value)
3740 {
3741  validate_operands(value, 1, "Is infinite must have one operand");
3742 }
3743 
3750 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
3751 {
3752  PRECONDITION(expr.id()==ID_isinf);
3753  const isinf_exprt &ret = static_cast<const isinf_exprt &>(expr);
3754  validate_expr(ret);
3755  return ret;
3756 }
3757 
3760 {
3761  PRECONDITION(expr.id()==ID_isinf);
3762  isinf_exprt &ret = static_cast<isinf_exprt &>(expr);
3763  validate_expr(ret);
3764  return ret;
3765 }
3766 
3767 
3770 {
3771 public:
3773  : unary_predicate_exprt(ID_isfinite, std::move(op))
3774  {
3775  }
3776 
3777  DEPRECATED(SINCE(2018, 12, 2, "use isfinite_exprt(op) instead"))
3779  {
3780  }
3781 };
3782 
3783 template <>
3784 inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
3785 {
3786  return base.id() == ID_isfinite;
3787 }
3788 
3789 inline void validate_expr(const isfinite_exprt &value)
3790 {
3791  validate_operands(value, 1, "Is finite must have one operand");
3792 }
3793 
3800 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
3801 {
3802  PRECONDITION(expr.id()==ID_isfinite);
3803  const isfinite_exprt &ret = static_cast<const isfinite_exprt &>(expr);
3804  validate_expr(ret);
3805  return ret;
3806 }
3807 
3810 {
3811  PRECONDITION(expr.id()==ID_isfinite);
3812  isfinite_exprt &ret = static_cast<isfinite_exprt &>(expr);
3813  validate_expr(ret);
3814  return ret;
3815 }
3816 
3817 
3820 {
3821 public:
3823  : unary_predicate_exprt(ID_isnormal, std::move(op))
3824  {
3825  }
3826 
3827  DEPRECATED(SINCE(2018, 12, 2, "use isnormal_exprt(op) instead"))
3829  {
3830  }
3831 };
3832 
3833 template <>
3834 inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
3835 {
3836  return base.id() == ID_isnormal;
3837 }
3838 
3839 inline void validate_expr(const isnormal_exprt &value)
3840 {
3841  validate_operands(value, 1, "Is normal must have one operand");
3842 }
3843 
3850 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
3851 {
3852  PRECONDITION(expr.id()==ID_isnormal);
3853  const isnormal_exprt &ret = static_cast<const isnormal_exprt &>(expr);
3854  validate_expr(ret);
3855  return ret;
3856 }
3857 
3860 {
3861  PRECONDITION(expr.id()==ID_isnormal);
3862  isnormal_exprt &ret = static_cast<isnormal_exprt &>(expr);
3863  validate_expr(ret);
3864  return ret;
3865 }
3866 
3867 
3870 {
3871 public:
3872  DEPRECATED(SINCE(2018, 12, 2, "use ieee_float_equal_exprt(lhs, rhs) instead"))
3874  {
3875  }
3876 
3879  std::move(_lhs),
3880  ID_ieee_float_equal,
3881  std::move(_rhs))
3882  {
3883  }
3884 };
3885 
3886 template <>
3888 {
3889  return base.id() == ID_ieee_float_equal;
3890 }
3891 
3892 inline void validate_expr(const ieee_float_equal_exprt &value)
3893 {
3894  validate_operands(value, 2, "IEEE equality must have two operands");
3895 }
3896 
3904 {
3905  PRECONDITION(expr.id()==ID_ieee_float_equal);
3906  const ieee_float_equal_exprt &ret =
3907  static_cast<const ieee_float_equal_exprt &>(expr);
3908  validate_expr(ret);
3909  return ret;
3910 }
3911 
3914 {
3915  PRECONDITION(expr.id()==ID_ieee_float_equal);
3916  ieee_float_equal_exprt &ret = static_cast<ieee_float_equal_exprt &>(expr);
3917  validate_expr(ret);
3918  return ret;
3919 }
3920 
3921 
3924 {
3925 public:
3926  DEPRECATED(
3927  SINCE(2018, 12, 2, "use ieee_float_notequal_exprt(lhs, rhs) instead"))
3929  binary_relation_exprt(ID_ieee_float_notequal)
3930  {
3931  }
3932 
3935  std::move(_lhs),
3936  ID_ieee_float_notequal,
3937  std::move(_rhs))
3938  {
3939  }
3940 };
3941 
3942 template <>
3944 {
3945  return base.id() == ID_ieee_float_notequal;
3946 }
3947 
3948 inline void validate_expr(const ieee_float_notequal_exprt &value)
3949 {
3950  validate_operands(value, 2, "IEEE inequality must have two operands");
3951 }
3952 
3960  const exprt &expr)
3961 {
3962  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3963  const ieee_float_notequal_exprt &ret =
3964  static_cast<const ieee_float_notequal_exprt &>(expr);
3965  validate_expr(ret);
3966  return ret;
3967 }
3968 
3971 {
3972  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3974  static_cast<ieee_float_notequal_exprt &>(expr);
3975  validate_expr(ret);
3976  return ret;
3977 }
3978 
3983 {
3984 public:
3986  const exprt &_lhs,
3987  const irep_idt &_id,
3988  exprt _rhs,
3989  exprt _rm)
3990  : ternary_exprt(_id, _lhs, std::move(_rhs), std::move(_rm), _lhs.type())
3991  {
3992  }
3993 
3995  {
3996  return op0();
3997  }
3998 
3999  const exprt &lhs() const
4000  {
4001  return op0();
4002  }
4003 
4005  {
4006  return op1();
4007  }
4008 
4009  const exprt &rhs() const
4010  {
4011  return op1();
4012  }
4013 
4015  {
4016  return op2();
4017  }
4018 
4019  const exprt &rounding_mode() const
4020  {
4021  return op2();
4022  }
4023 };
4024 
4025 template <>
4027 {
4028  return base.id() == ID_floatbv_plus || base.id() == ID_floatbv_minus ||
4029  base.id() == ID_floatbv_div || base.id() == ID_floatbv_mult;
4030 }
4031 
4032 inline void validate_expr(const ieee_float_op_exprt &value)
4033 {
4035  value, 3, "IEEE float operations must have three arguments");
4036 }
4037 
4045 {
4046  const ieee_float_op_exprt &ret =
4047  static_cast<const ieee_float_op_exprt &>(expr);
4048  validate_expr(ret);
4049  return ret;
4050 }
4051 
4054 {
4055  ieee_float_op_exprt &ret = static_cast<ieee_float_op_exprt &>(expr);
4056  validate_expr(ret);
4057  return ret;
4058 }
4059 
4060 
4063 {
4064 public:
4065  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
4066  {
4067  }
4068 };
4069 
4072 {
4073 public:
4074  constant_exprt(const irep_idt &_value, typet _type)
4075  : expr_protectedt(ID_constant, std::move(_type))
4076  {
4077  set_value(_value);
4078  }
4079 
4080  const irep_idt &get_value() const
4081  {
4082  return get(ID_value);
4083  }
4084 
4085  void set_value(const irep_idt &value)
4086  {
4087  set(ID_value, value);
4088  }
4089 
4090  bool value_is_zero_string() const;
4091 };
4092 
4093 template <>
4094 inline bool can_cast_expr<constant_exprt>(const exprt &base)
4095 {
4096  return base.id() == ID_constant;
4097 }
4098 
4105 inline const constant_exprt &to_constant_expr(const exprt &expr)
4106 {
4107  PRECONDITION(expr.id()==ID_constant);
4108  return static_cast<const constant_exprt &>(expr);
4109 }
4110 
4113 {
4114  PRECONDITION(expr.id()==ID_constant);
4115  return static_cast<constant_exprt &>(expr);
4116 }
4117 
4118 
4121 {
4122 public:
4124  {
4125  }
4126 };
4127 
4130 {
4131 public:
4133  {
4134  }
4135 };
4136 
4138 class nil_exprt : public nullary_exprt
4139 {
4140 public:
4142  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
4143  {
4144  }
4145 };
4146 
4147 template <>
4148 inline bool can_cast_expr<nil_exprt>(const exprt &base)
4149 {
4150  return base.id() == ID_nil;
4151 }
4152 
4155 {
4156 public:
4158  : constant_exprt(ID_NULL, std::move(type))
4159  {
4160  }
4161 };
4162 
4165 {
4166 public:
4167  replication_exprt(const constant_exprt &_times, const exprt &_src)
4168  : binary_exprt(_times, ID_replication, _src)
4169  {
4170  }
4171 
4173  {
4174  return static_cast<constant_exprt &>(op0());
4175  }
4176 
4177  const constant_exprt &times() const
4178  {
4179  return static_cast<const constant_exprt &>(op0());
4180  }
4181 
4183  {
4184  return op1();
4185  }
4186 
4187  const exprt &op() const
4188  {
4189  return op1();
4190  }
4191 };
4192 
4193 template <>
4194 inline bool can_cast_expr<replication_exprt>(const exprt &base)
4195 {
4196  return base.id() == ID_replication;
4197 }
4198 
4199 inline void validate_expr(const replication_exprt &value)
4200 {
4201  validate_operands(value, 2, "Bit-wise replication must have two operands");
4202 }
4203 
4210 inline const replication_exprt &to_replication_expr(const exprt &expr)
4211 {
4212  PRECONDITION(expr.id() == ID_replication);
4213  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
4214  validate_expr(ret);
4215  return ret;
4216 }
4217 
4220 {
4221  PRECONDITION(expr.id() == ID_replication);
4222  replication_exprt &ret = static_cast<replication_exprt &>(expr);
4223  validate_expr(ret);
4224  return ret;
4225 }
4226 
4233 {
4234 public:
4236  : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
4237  {
4238  }
4239 
4241  : multi_ary_exprt(
4242  ID_concatenation,
4243  {std::move(_op0), std::move(_op1)},
4244  std::move(_type))
4245  {
4246  }
4247 };
4248 
4249 template <>
4251 {
4252  return base.id() == ID_concatenation;
4253 }
4254 
4262 {
4263  PRECONDITION(expr.id()==ID_concatenation);
4264  return static_cast<const concatenation_exprt &>(expr);
4265 }
4266 
4269 {
4270  PRECONDITION(expr.id()==ID_concatenation);
4271  return static_cast<concatenation_exprt &>(expr);
4272 }
4273 
4274 
4277 {
4278 public:
4279  explicit infinity_exprt(typet _type)
4280  : nullary_exprt(ID_infinity, std::move(_type))
4281  {
4282  }
4283 };
4284 
4286 class let_exprt : public ternary_exprt
4287 {
4288 public:
4290  : ternary_exprt(
4291  ID_let,
4292  std::move(symbol),
4293  std::move(value),
4294  where,
4295  where.type())
4296  {
4297  }
4298 
4300  {
4301  return static_cast<symbol_exprt &>(op0());
4302  }
4303 
4304  const symbol_exprt &symbol() const
4305  {
4306  return static_cast<const symbol_exprt &>(op0());
4307  }
4308 
4310  {
4311  return op1();
4312  }
4313 
4314  const exprt &value() const
4315  {
4316  return op1();
4317  }
4318 
4320  {
4321  return op2();
4322  }
4323 
4324  const exprt &where() const
4325  {
4326  return op2();
4327  }
4328 };
4329 
4330 template <>
4331 inline bool can_cast_expr<let_exprt>(const exprt &base)
4332 {
4333  return base.id() == ID_let;
4334 }
4335 
4336 inline void validate_expr(const let_exprt &value)
4337 {
4338  validate_operands(value, 3, "Let must have three operands");
4339 }
4340 
4347 inline const let_exprt &to_let_expr(const exprt &expr)
4348 {
4349  PRECONDITION(expr.id()==ID_let);
4350  const let_exprt &ret = static_cast<const let_exprt &>(expr);
4351  validate_expr(ret);
4352  return ret;
4353 }
4354 
4357 {
4358  PRECONDITION(expr.id()==ID_let);
4359  let_exprt &ret = static_cast<let_exprt &>(expr);
4360  validate_expr(ret);
4361  return ret;
4362 }
4363 
4366 {
4367 public:
4369  : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
4370  {
4371  }
4372 
4373  explicit popcount_exprt(const exprt &_op)
4374  : unary_exprt(ID_popcount, _op, _op.type())
4375  {
4376  }
4377 };
4378 
4379 template <>
4380 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
4381 {
4382  return base.id() == ID_popcount;
4383 }
4384 
4385 inline void validate_expr(const popcount_exprt &value)
4386 {
4387  validate_operands(value, 1, "popcount must have one operand");
4388 }
4389 
4396 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
4397 {
4398  PRECONDITION(expr.id() == ID_popcount);
4399  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
4400  validate_expr(ret);
4401  return ret;
4402 }
4403 
4406 {
4407  PRECONDITION(expr.id() == ID_popcount);
4408  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
4409  validate_expr(ret);
4410  return ret;
4411 }
4412 
4417 {
4418 public:
4419  DEPRECATED(SINCE(2019, 1, 12, "use cond_exprt(operands, type) instead"))
4420  explicit cond_exprt(const typet &_type) : multi_ary_exprt(ID_cond, _type)
4421  {
4422  }
4423 
4424  cond_exprt(operandst _operands, typet _type)
4425  : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
4426  {
4427  }
4428 
4432  void add_case(const exprt &condition, const exprt &value)
4433  {
4434  PRECONDITION(condition.type().id() == ID_bool);
4435  operands().reserve(operands().size() + 2);
4436  operands().push_back(condition);
4437  operands().push_back(value);
4438  }
4439 };
4440 
4441 template <>
4442 inline bool can_cast_expr<cond_exprt>(const exprt &base)
4443 {
4444  return base.id() == ID_cond;
4445 }
4446 
4447 inline void validate_expr(const cond_exprt &value)
4448 {
4450  value.operands().size() % 2 == 0, "cond must have even number of operands");
4451 }
4452 
4459 inline const cond_exprt &to_cond_expr(const exprt &expr)
4460 {
4461  PRECONDITION(expr.id() == ID_cond);
4462  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
4463  validate_expr(ret);
4464  return ret;
4465 }
4466 
4469 {
4470  PRECONDITION(expr.id() == ID_cond);
4471  cond_exprt &ret = static_cast<cond_exprt &>(expr);
4472  validate_expr(ret);
4473  return ret;
4474 }
4475 
4487 {
4488 public:
4490  symbol_exprt arg,
4491  exprt body,
4492  array_typet _type)
4493  : binary_exprt(std::move(arg), ID_lambda, std::move(body), std::move(_type))
4494  {
4495  }
4496 
4497  const array_typet &type() const
4498  {
4499  return static_cast<const array_typet &>(binary_exprt::type());
4500  }
4501 
4503  {
4504  return static_cast<array_typet &>(binary_exprt::type());
4505  }
4506 
4507  const symbol_exprt &arg() const
4508  {
4509  return static_cast<const symbol_exprt &>(op0());
4510  }
4511 
4513  {
4514  return static_cast<symbol_exprt &>(op0());
4515  }
4516 
4517  const exprt &body() const
4518  {
4519  return op1();
4520  }
4521 
4523  {
4524  return op1();
4525  }
4526 };
4527 
4528 template <>
4530 {
4531  return base.id() == ID_lambda;
4532 }
4533 
4534 inline void validate_expr(const array_comprehension_exprt &value)
4535 {
4536  validate_operands(value, 2, "'Array comprehension' must have two operands");
4537 }
4538 
4545 inline const array_comprehension_exprt &
4547 {
4548  PRECONDITION(expr.id() == ID_lambda);
4549  const array_comprehension_exprt &ret =
4550  static_cast<const array_comprehension_exprt &>(expr);
4551  validate_expr(ret);
4552  return ret;
4553 }
4554 
4557 {
4558  PRECONDITION(expr.id() == ID_lambda);
4560  static_cast<array_comprehension_exprt &>(expr);
4561  validate_expr(ret);
4562  return ret;
4563 }
4564 
4565 #endif // CPROVER_UTIL_STD_EXPR_H
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3190
bool can_cast_expr< rem_exprt >(const exprt &base)
Definition: std_expr.h:1255
const irept & get_nil_irep()
Definition: irep.cpp:26
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:205
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:3903
const irep_idt & get_name() const
Definition: std_types.h:74
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:3443
bool can_cast_expr< bitxor_exprt >(const exprt &base)
Definition: std_expr.h:2589
The type of an expression, extends irept.
Definition: type.h:28
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2355
const array_typet & type() const
Definition: std_expr.h:4497
bool can_cast_expr< isnormal_exprt >(const exprt &base)
Definition: std_expr.h:3834
isnan_exprt(exprt op)
Definition: std_expr.h:3672
ashr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2762
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:406
Boolean negation.
Definition: std_expr.h:2998
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition: std_expr.h:752
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: std_expr.h:529
bitand_exprt(const exprt &_op0, exprt _op1)
Definition: std_expr.h:2618
const exprt & op1() const
Definition: std_expr.h:937
exprt & true_case()
Definition: std_expr.h:3152
symbol_exprt(typet type)
Definition: std_expr.h:92
Semantic type conversion.
Definition: std_expr.h:2153
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:671
and_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2290
const exprt & rhs() const
Definition: std_expr.h:4009
bitnot_exprt(exprt op)
Definition: std_expr.h:2502
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1096
rem_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1248
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:4486
An expression without operands.
Definition: std_expr.h:23
bool can_cast_expr< bitnot_exprt >(const exprt &base)
Definition: std_expr.h:2508
shl_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2719
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: std_expr.h:2134
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:579
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:779
const exprt & value() const
Definition: std_expr.h:4314
index_exprt(exprt _array, exprt _index, typet _type)
Definition: std_expr.h:1401
const exprt & lhs() const
Definition: std_expr.h:826
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
Definition: std_expr.h:2636
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1066
exprt & object()
Definition: std_expr.h:2951
array_list_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1593
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:227
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition: std_expr.h:4529
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:4546
bswap_exprt(exprt _op, std::size_t bits_per_byte)
Definition: std_expr.h:493
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2172
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1226
Boolean OR.
Definition: std_expr.h:2390
mult_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1089
exprt & op0()
Definition: expr.h:97
bitor_exprt(const exprt &_op0, exprt _op1)
Definition: std_expr.h:2546
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
exprt & op0()
Definition: std_expr.h:907
const exprt & src() const
Definition: std_expr.h:2805
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1181
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1021
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: std_expr.h:2100
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:686
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
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition: std_expr.h:3132
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:632
Operator to update elements in structs and arrays.
Definition: std_expr.h:3394
const exprt & op() const
Definition: std_expr.h:295
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:466
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: std_expr.h:4250
const exprt & pointer() const
Definition: std_expr.h:3067
Evaluates to true if the operand is infinite.
Definition: std_expr.h:3719
const exprt & op() const
Definition: std_expr.h:4187
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1569
bool can_cast_expr< shift_exprt >(const exprt &base)
Definition: std_expr.h:2683
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:184
const exprt & op2() const
Definition: std_expr.h:943
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3253
unsigned int get_instance() const
Definition: std_expr.cpp:45
exprt & struct_op()
Definition: std_expr.h:3602
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
Definition: std_expr.h:2600
concatenation_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4235
const exprt & real() const
Definition: std_expr.h:1819
const exprt & array() const
Definition: std_expr.h:1415
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: std_expr.h:2736
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1497
const irep_idt & get_identifier() const
Definition: std_expr.h:118
isfinite_exprt(exprt op)
Definition: std_expr.h:3772
exprt::operandst & designator()
Definition: std_expr.h:3421
exprt & lower()
Definition: std_expr.h:2884
const exprt & op3() const =delete
Base class for all expressions.
Definition: expr.h:358
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition: std_expr.h:3397
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:4432
exprt imag()
Definition: std_expr.h:1824
const irep_idt & get_value() const
Definition: std_expr.h:4080
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:2029
output_type narrow_cast(input_type value)
Alias for static_cast intended to be used for numeric casting Rationale: Easier to grep than static_c...
Definition: narrow.h:19
The null pointer constant.
Definition: std_expr.h:4154
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3072
An expression denoting a type.
Definition: std_expr.h:4062
array_of_exprt(exprt _what, array_typet _type)
Definition: std_expr.h:1470
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:3359
exprt & op3()
Definition: std_expr.h:925
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition: std_expr.h:290
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
Definition: std_expr.h:2564
const exprt & op1() const =delete
infinity_exprt(typet _type)
Definition: std_expr.h:4279
bool is_thread_local() const
Definition: std_expr.h:151
mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1203
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Definition: std_expr.h:2654
exprt real()
Definition: std_expr.h:1814
or_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2398
The trinary if-then-else operator.
Definition: std_expr.h:3124
exprt & cond()
Definition: std_expr.h:3142
std::size_t get_component_number() const
Definition: std_expr.h:3590
const exprt & body() const
Definition: std_expr.h:4517
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:3819
exprt & old()
Definition: std_expr.h:3221
unary_plus_exprt(exprt op)
Definition: std_expr.h:443
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1158
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1942
exprt & new_value()
Definition: std_expr.h:3241
typet & type()
Return the type of the expression.
Definition: expr.h:81
exprt & op2()
Definition: std_expr.h:919
bool can_cast_expr< extractbit_exprt >(const exprt &base)
Definition: std_expr.h:2817
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2443
bool can_cast_expr< bitand_exprt >(const exprt &base)
Definition: std_expr.h:2625
STL namespace.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2979
const exprt & op2() const =delete
dereference_exprt(exprt op, typet type)
Definition: std_expr.h:3057
The Boolean type.
Definition: std_types.h:36
address_of_exprt(exprt op, pointer_typet _type)
Definition: std_expr.h:2946
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1616
plus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:984
const exprt & where() const
Definition: std_expr.h:3236
A constant literal expression.
Definition: std_expr.h:4071
exprt & distance()
Definition: std_expr.h:2671
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1210
exprt & rounding_mode()
Definition: std_expr.h:4014
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1152
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2319
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1146
replication_exprt(const constant_exprt &_times, const exprt &_src)
Definition: std_expr.h:4167
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:3310
const exprt & index() const
Definition: std_expr.h:1425
const exprt & op3() const =delete
const exprt & lower() const
Definition: std_expr.h:2899
symbol_exprt & arg()
Definition: std_expr.h:4512
unary_minus_exprt(exprt _op)
Definition: std_expr.h:399
const exprt & where() const
Definition: std_expr.h:4324
irep_idt get_component_name() const
Definition: std_expr.h:3352
Boolean implication.
Definition: std_expr.h:2345
bool value_is_zero_string() const
Definition: std_expr.cpp:22
array_typet & type()
Definition: std_expr.h:1603
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1915
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:616
void set_bits_per_byte(std::size_t bits_per_byte)
Definition: std_expr.h:504
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:3959
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4347
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1709
array_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1541
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3105
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Definition: std_expr.h:3887
Extract member of struct or union.
Definition: std_expr.h:3565
const exprt & imag() const
Definition: std_expr.h:1829
const exprt & rounding_mode() const
Definition: std_expr.h:2234
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:3013
exprt & where()
Definition: std_expr.h:4319
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
Concatenation of bit-vector operands.
Definition: std_expr.h:4232
Equality.
Definition: std_expr.h:1290
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1374
bool can_cast_expr< bitor_exprt >(const exprt &base)
Definition: std_expr.h:2553
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:1005
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1165
const exprt & op() const
Definition: std_expr.h:2666
Templated functions to cast to specific exprt-derived classes.
void add(exprt index, exprt value)
add an index/value pair
Definition: std_expr.h:1609
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2371
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3585
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:4044
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
const exprt & compound() const
Definition: std_expr.h:3607
exprt & op()
Definition: std_expr.h:300
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:666
dynamic_object_exprt(typet type)
Definition: std_expr.h:2059
implies_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2348
const exprt & src() const
Definition: std_expr.h:2889
const irep_idt & id() const
Definition: irep.h:418
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2411
if_exprt(exprt cond, const exprt &t, exprt f)
Definition: std_expr.h:3127
popcount_exprt(const exprt &_op)
Definition: std_expr.h:4373
const exprt & op2() const =delete
index_designatort(exprt _index)
Definition: std_expr.h:3293
The unary plus expression.
Definition: std_expr.h:440
void set_value(const irep_idt &value)
Definition: std_expr.h:4085
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3669
Bit-wise OR.
Definition: std_expr.h:2543
bool can_cast_expr< isnan_exprt >(const exprt &base)
Definition: std_expr.h:3684
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:4459
ieee_float_notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:3933
An expression denoting infinity.
Definition: std_expr.h:4276
cond_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4424
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:1050
ashr_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2757
The Boolean constant true.
Definition: std_expr.h:4120
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition: std_expr.h:126
Division.
Definition: std_expr.h:1131
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: std_expr.h:4210
A base class for binary expressions.
Definition: std_expr.h:650
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4261
exprt & old()
Definition: std_expr.h:3407
const exprt & distance() const
Definition: std_expr.h:2676
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
Definition: std_expr.h:4289
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3460
const irep_idt & get_identifier() const
Definition: std_expr.h:232
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1670
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3617
The NIL expression.
Definition: std_expr.h:4138
Real part of the expression describing a complex number.
Definition: std_expr.h:1870
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
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition: std_expr.h:217
The pointer type These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1487
IEEE floating-point disequality.
Definition: std_expr.h:3923
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:3634
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:2833
and_exprt(exprt::operandst _operands)
Definition: std_expr.h:2306
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1305
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1659
div_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1134
const exprt & op3() const =delete
const exprt & op1() const =delete
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:1880
type_exprt(typet type)
Definition: std_expr.h:4065
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition: std_expr.h:989
Operator to dereference a pointer.
Definition: std_expr.h:3048
operandst & operands()=delete
remove all operand methods
exprt & rounding_mode()
Definition: std_expr.h:2229
The vector type.
Definition: std_types.h:1744
const exprt & op0() const =delete
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:239
exprt & src()
Definition: std_expr.h:2874
const array_typet & type() const
Definition: std_expr.h:1546
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1513
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:1836
const constant_exprt & times() const
Definition: std_expr.h:4177
Union constructor from single element.
Definition: std_expr.h:1685
std::size_t get_component_number() const
Definition: std_expr.h:1704
Boolean AND.
Definition: std_expr.h:2277
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2852
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:705
const exprt & new_value() const
Definition: std_expr.h:3436
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: std_expr.h:3750
exprt & op1()
Definition: expr.h:100
equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1293
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1626
const exprt & lhs() const
Definition: std_expr.h:3999
Generic base class for unary expressions.
Definition: std_expr.h:275
Disequality.
Definition: std_expr.h:1348
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:2013
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:450
array_typet & type()
Definition: std_expr.h:1480
An expression with three operands.
Definition: std_expr.h:54
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1716
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:108
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:2922
Left shift.
Definition: std_expr.h:2716
const exprt & what() const
Definition: std_expr.h:1490
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:859
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:278
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const exprt & false_case() const
Definition: std_expr.h:3167
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3650
floatbv_typecast_exprt(exprt op, exprt rounding, typet _type)
Definition: std_expr.h:2210
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: std_expr.h:2906
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition: std_expr.h:4442
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1962
nullary_exprt(const irep_idt &_id, typet _type)
Definition: std_expr.h:26
const exprt & cond() const
Definition: std_expr.h:3147
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition: std_expr.h:4489
is_dynamic_object_exprt(const exprt &op)
Definition: std_expr.h:2127
The plus expression Associativity is not specified.
Definition: std_expr.h:976
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
Definition: std_expr.h:2788
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:4094
const symbol_exprt & symbol() const
Definition: std_expr.h:4304
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
Definition: std_expr.h:2241
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:184
void set_static_lifetime()
Definition: std_expr.h:141
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition: std_expr.h:3213
Array constructor from single element.
Definition: std_expr.h:1467
array_typet & type()
Definition: std_expr.h:1551
exprt & upper()
Definition: std_expr.h:2879
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2473
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
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1298
const exprt & op0() const
Definition: std_expr.h:931
plus_exprt(operandst _operands, typet _type)
Definition: std_expr.h:998
and_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2285
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:356
Logical right shift.
Definition: std_expr.h:2769
exprt & compound()
Definition: std_expr.h:3612
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:3326
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:1925
Vector constructor from list of elements.
Definition: std_expr.h:1643
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:36
notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1351
const exprt & old() const
Definition: std_expr.h:3226
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
Definition: std_expr.h:2860
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: std_expr.h:3800
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:2432
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: std_expr.h:3089
Operator to return the address of an object.
Definition: std_expr.h:2941
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1787
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:895
The unary minus expression.
Definition: std_expr.h:391
exprt & false_case()
Definition: std_expr.h:3162
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: std_expr.h:2084
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4105
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:556
symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:98
const exprt & index() const
Definition: std_expr.h:3298
constant_exprt(const irep_idt &_value, typet _type)
Definition: std_expr.h:4074
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:2963
The Boolean constant false.
Definition: std_expr.h:4129
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:757
isinf_exprt(exprt op)
Definition: std_expr.h:3722
bool can_cast_expr< replication_exprt >(const exprt &base)
Definition: std_expr.h:4194
exprt & index()
Definition: std_expr.h:2800
const exprt & rhs() const
Definition: std_expr.h:836
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2257
void validate_expr(const symbol_exprt &value)
Definition: std_expr.h:173
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2162
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2484
const array_typet & type() const
Definition: std_expr.h:1598
std::vector< exprt > operandst
Definition: expr.h:55
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1086
const exprt::operandst & designator() const
Definition: std_expr.h:3426
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: std_expr.h:3943
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1358
typecast_exprt(exprt op, typet _type)
Definition: std_expr.h:2156
#define DEPRECATED(msg)
Definition: deprecate.h:23
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1112
const exprt & object() const
Definition: std_expr.h:1994
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition: std_expr.h:4148
Boolean XOR.
Definition: std_expr.h:2458
Complex numbers made of pair of given subtype.
Definition: std_types.h:1784
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4396
bitxor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2582
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3273
Bit-wise XOR.
Definition: std_expr.h:2579
const exprt & op3() const
Definition: std_expr.h:949
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:962
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:208
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1331
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:168
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:1918
xor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2466
Pre-defined types.
const exprt & op3() const =delete
popcount_exprt(exprt _op, typet _type)
Definition: std_expr.h:4368
const exprt & old() const
Definition: std_expr.h:3412
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs, exprt _rm)
Definition: std_expr.h:3985
const exprt & object() const
Definition: std_expr.h:2956
not_exprt(exprt _op)
Definition: std_expr.h:3001
unary_minus_exprt(exprt _op, typet _type)
Definition: std_expr.h:394
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: std_expr.h:3700
constant_exprt & times()
Definition: std_expr.h:4172
exprt & value()
Definition: std_expr.h:4309
Expression to hold a nondeterministic choice.
Definition: std_expr.h:203
lshr_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2772
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2699
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2330
or_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2403
exprt & index()
Definition: std_expr.h:1420
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4365
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
Definition: std_expr.h:1271
Evaluates to true if the operand is finite.
Definition: std_expr.h:3769
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2298
const exprt & index() const
Definition: std_expr.h:2810
exprt & op()
Definition: std_expr.h:2661
std::size_t get_bits_per_byte() const
Definition: std_expr.h:499
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2207
bool can_cast_expr< ieee_float_op_exprt >(const exprt &base)
Definition: std_expr.h:4026
Base class for all expressions.
Definition: expr.h:52
exprt & pointer()
Definition: std_expr.h:3062
Absolute value.
Definition: std_expr.h:347
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:601
const exprt & root_object() const
Definition: std_expr.cpp:217
const exprt & struct_op() const
Definition: std_expr.h:3596
const exprt & rounding_mode() const
Definition: std_expr.h:4019
const symbol_exprt & arg() const
Definition: std_expr.h:4507
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:843
dereference_exprt(const exprt &op)
Definition: std_expr.h:3051
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition: std_expr.h:65
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1852
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
Definition: std_expr.h:487
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
Definition: std_expr.h:4240
complex_real_exprt(const exprt &op)
Definition: std_expr.h:1873
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1732
const exprt & op2() const =delete
Operator to update elements in structs and arrays.
Definition: std_expr.h:3210
const exprt & upper() const
Definition: std_expr.h:2894
exprt & op1()
Definition: std_expr.h:913
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:800
member_exprt(exprt op, const struct_typet::componentt &c)
Definition: std_expr.h:3574
irep_idt get_component_name() const
Definition: std_expr.h:3580
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition: std_expr.h:3568
const exprt & offset() const
Definition: std_expr.h:2006
minus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1043
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2188
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:795
abs_exprt(exprt _op)
Definition: std_expr.h:350
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:4331
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3029
Remainder of division.
Definition: std_expr.h:1245
const exprt & valid() const
Definition: std_expr.h:2077
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1815
const exprt & true_case() const
Definition: std_expr.h:3157
exprt & index()
Definition: std_expr.h:3303
vector_exprt(operandst _operands, vector_typet _type)
Definition: std_expr.h:1652
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:113
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
Definition: validate.h:22
exprt & op()
Definition: std_expr.h:4182
irep_idt get_component_name() const
Definition: std_expr.h:1694
index_exprt(const exprt &_array, exprt _index)
Definition: std_expr.h:1396
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:314
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1699
source_locationt & add_source_location()
Definition: expr.h:256
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:372
sign_exprt(exprt _op)
Definition: std_expr.h:609
bool is_static_lifetime() const
Definition: std_expr.h:136
Arrays with given size.
Definition: std_types.h:964
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:131
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition: std_expr.h:593
bool can_cast_expr< bswap_exprt >(const exprt &base)
Definition: std_expr.h:511
Binary minus.
Definition: std_expr.h:1040
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:676
Bit-wise AND.
Definition: std_expr.h:2615
validation_modet
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition: std_expr.h:889
Expression to hold a symbol (variable)
Definition: std_expr.h:88
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: std_expr.h:3734
exprt & what()
Definition: std_expr.h:1485
exprt & op2()
Definition: expr.h:103
isnormal_exprt(exprt op)
Definition: std_expr.h:3822
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:764
bool can_cast_expr< isfinite_exprt >(const exprt &base)
Definition: std_expr.h:3784
exprt & new_value()
Definition: std_expr.h:3431
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1776
symbol_exprt & symbol()
Definition: std_expr.h:4299
object_descriptor_exprt(exprt _object)
Definition: std_expr.h:1974
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:721
shl_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2724
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:736
lshr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2777
Arithmetic right shift.
Definition: std_expr.h:2754
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition: std_expr.h:1805
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1432
exprt & where()
Definition: std_expr.h:3231
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: std_expr.h:2524
A let expression.
Definition: std_expr.h:4286
or_exprt(exprt::operandst _operands)
Definition: std_expr.h:2419
void clear_static_lifetime()
Definition: std_expr.h:146
struct_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1766
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:511
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1140
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: std_expr.h:3850
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
Representation of heap-allocated objects.
Definition: std_expr.h:2050
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:255
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:875
array_typet & type()
Definition: std_expr.h:4502
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:330
operandst & operands()
Definition: expr.h:91
void copy_to_operands(const exprt &expr)=delete
exprt & src()
Definition: std_expr.h:2795
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2499
Struct constructor from list of elements.
Definition: std_expr.h:1751
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: std_expr.h:2120
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:900
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:3174
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:74
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1897
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:3982
Bit-vector replication.
Definition: std_expr.h:4164
exprt & array()
Definition: std_expr.h:1410
void move_to_operands(exprt &)=delete
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1448
A base class for shift operators.
Definition: std_expr.h:2651
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt&#39;s operands.
Definition: expr.h:151
Array constructor from list of elements.
Definition: std_expr.h:1532
Complex constructor from a pair of numbers.
Definition: std_expr.h:1802
Modulo.
Definition: std_expr.h:1200
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1558
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
The byte swap expression.
Definition: std_expr.h:484
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:422
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:3346
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: std_expr.h:4380
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:807
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
Definition: std_expr.h:1584
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:3375
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:4416
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2784
ieee_float_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:3877
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:548
IEEE-floating-point equality.
Definition: std_expr.h:3869
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1315
null_pointer_exprt(pointer_typet type)
Definition: std_expr.h:4157
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition: std_expr.h:1688
Array index operator.
Definition: std_expr.h:1393
const array_typet & type() const
Definition: std_expr.h:1475
const exprt & new_value() const
Definition: std_expr.h:3246
const exprt & op() const
Definition: std_expr.h:2224