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 "base_type.h"
17 #include "expr_cast.h"
18 #include "invariant.h"
19 #include "mathematical_types.h"
20 #include "std_types.h"
21 
23 class nullary_exprt : public exprt
24 {
25 public:
26  // constructors
27  DEPRECATED("use nullary_exprt(id, type) instead")
28  explicit nullary_exprt(const irep_idt &_id) : exprt(_id)
29  {
30  }
31 
32  nullary_exprt(const irep_idt &_id, const typet &_type) : exprt(_id, _type)
33  {
34  }
35 
37  operandst &operands() = delete;
38  const operandst &operands() const = delete;
39 
40  const exprt &op0() const = delete;
41  exprt &op0() = delete;
42  const exprt &op1() const = delete;
43  exprt &op1() = delete;
44  const exprt &op2() const = delete;
45  exprt &op2() = delete;
46  const exprt &op3() const = delete;
47  exprt &op3() = delete;
48 
49  void move_to_operands(exprt &) = delete;
50  void move_to_operands(exprt &, exprt &) = delete;
51  void move_to_operands(exprt &, exprt &, exprt &) = delete;
52 
53  void copy_to_operands(const exprt &expr) = delete;
54  void copy_to_operands(const exprt &, const exprt &) = delete;
55  void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
56 };
57 
59 class ternary_exprt : public exprt
60 {
61 public:
62  // constructors
63  DEPRECATED("use ternary_exprt(id, op0, op1, op2, type) instead")
64  explicit ternary_exprt(const irep_idt &_id) : exprt(_id)
65  {
66  operands().resize(3);
67  }
68 
69  DEPRECATED("use ternary_exprt(id, op0, op1, op2, type) instead")
70  explicit ternary_exprt(const irep_idt &_id, const typet &_type)
71  : exprt(_id, _type)
72  {
73  operands().resize(3);
74  }
75 
77  const irep_idt &_id,
78  const exprt &_op0,
79  const exprt &_op1,
80  const exprt &_op2,
81  const typet &_type)
82  : exprt(_id, _type)
83  {
84  add_to_operands(_op0, _op1, _op2);
85  }
86 
87  const exprt &op3() const = delete;
88  exprt &op3() = delete;
89 };
90 
93 class transt : public ternary_exprt
94 {
95 public:
96  DEPRECATED("use transt(op0, op1, op2) instead")
97  transt() : ternary_exprt(ID_trans)
98  {
99  }
100 
102  const irep_idt &_id,
103  const exprt &_op0,
104  const exprt &_op1,
105  const exprt &_op2,
106  const typet &_type)
107  : ternary_exprt(_id, _op0, _op1, _op2, _type)
108  {
109  }
110 
111  exprt &invar() { return op0(); }
112  exprt &init() { return op1(); }
113  exprt &trans() { return op2(); }
114 
115  const exprt &invar() const { return op0(); }
116  const exprt &init() const { return op1(); }
117  const exprt &trans() const { return op2(); }
118 };
119 
124 inline const transt &to_trans_expr(const exprt &expr)
125 {
126  PRECONDITION(expr.id()==ID_trans);
128  expr.operands().size()==3,
129  "Transition systems must have three operands");
130  return static_cast<const transt &>(expr);
131 }
132 
134 inline transt &to_trans_expr(exprt &expr)
135 {
136  PRECONDITION(expr.id()==ID_trans);
138  expr.operands().size()==3,
139  "Transition systems must have three operands");
140  return static_cast<transt &>(expr);
141 }
142 
143 template<> inline bool can_cast_expr<transt>(const exprt &base)
144 {
145  return base.id()==ID_trans;
146 }
147 inline void validate_expr(const transt &value)
148 {
149  validate_operands(value, 3, "Transition systems must have three operands");
150 }
151 
152 
155 {
156 public:
157  DEPRECATED("use symbol_exprt(identifier, type) instead")
159  {
160  }
161 
163  DEPRECATED("use symbol_exprt(identifier, type) instead")
164  explicit symbol_exprt(const irep_idt &identifier) : nullary_exprt(ID_symbol)
165  {
166  set_identifier(identifier);
167  }
168 
170  explicit symbol_exprt(const typet &type) : nullary_exprt(ID_symbol, type)
171  {
172  }
173 
176  symbol_exprt(const irep_idt &identifier, const typet &type)
177  : nullary_exprt(ID_symbol, type)
178  {
179  set_identifier(identifier);
180  }
181 
182  void set_identifier(const irep_idt &identifier)
183  {
184  set(ID_identifier, identifier);
185  }
186 
187  const irep_idt &get_identifier() const
188  {
189  return get(ID_identifier);
190  }
191 };
192 
196 {
197 public:
198  DEPRECATED("use decorated_symbol_exprt(identifier, type) instead")
200  {
201  }
202 
204  DEPRECATED("use decorated_symbol_exprt(identifier, type) instead")
205  explicit decorated_symbol_exprt(const irep_idt &identifier):
206  symbol_exprt(identifier)
207  {
208  }
209 
211  DEPRECATED("use decorated_symbol_exprt(identifier, type) instead")
214  {
215  }
216 
220  const irep_idt &identifier,
221  const typet &type):symbol_exprt(identifier, type)
222  {
223  }
224 
225  bool is_static_lifetime() const
226  {
227  return get_bool(ID_C_static_lifetime);
228  }
229 
231  {
232  return set(ID_C_static_lifetime, true);
233  }
234 
236  {
237  remove(ID_C_static_lifetime);
238  }
239 
240  bool is_thread_local() const
241  {
242  return get_bool(ID_C_thread_local);
243  }
244 
246  {
247  return set(ID_C_thread_local, true);
248  }
249 
251  {
252  remove(ID_C_thread_local);
253  }
254 };
255 
262 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
263 {
264  PRECONDITION(expr.id()==ID_symbol);
265  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
266  return static_cast<const symbol_exprt &>(expr);
267 }
268 
271 {
272  PRECONDITION(expr.id()==ID_symbol);
273  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
274  return static_cast<symbol_exprt &>(expr);
275 }
276 
277 template<> inline bool can_cast_expr<symbol_exprt>(const exprt &base)
278 {
279  return base.id()==ID_symbol;
280 }
281 inline void validate_expr(const symbol_exprt &value)
282 {
283  validate_operands(value, 0, "Symbols must not have operands");
284 }
285 
286 
289 {
290 public:
293  nondet_symbol_exprt(const irep_idt &identifier, const typet &type)
294  : nullary_exprt(ID_nondet_symbol, type)
295  {
296  set_identifier(identifier);
297  }
298 
299  void set_identifier(const irep_idt &identifier)
300  {
301  set(ID_identifier, identifier);
302  }
303 
304  const irep_idt &get_identifier() const
305  {
306  return get(ID_identifier);
307  }
308 };
309 
317 {
318  PRECONDITION(expr.id()==ID_nondet_symbol);
319  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
320  return static_cast<const nondet_symbol_exprt &>(expr);
321 }
322 
325 {
326  PRECONDITION(expr.id()==ID_symbol);
327  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
328  return static_cast<nondet_symbol_exprt &>(expr);
329 }
330 
331 template<> inline bool can_cast_expr<nondet_symbol_exprt>(const exprt &base)
332 {
333  return base.id()==ID_nondet_symbol;
334 }
335 inline void validate_expr(const nondet_symbol_exprt &value)
336 {
337  validate_operands(value, 0, "Symbols must not have operands");
338 }
339 
340 
342 class unary_exprt:public exprt
343 {
344 public:
345  DEPRECATED("use unary_exprt(id, op) instead")
347  {
348  operands().resize(1);
349  }
350 
351  DEPRECATED("use unary_exprt(id, op) instead")
352  explicit unary_exprt(const irep_idt &_id):exprt(_id)
353  {
354  operands().resize(1);
355  }
356 
358  const irep_idt &_id,
359  const exprt &_op):
360  exprt(_id, _op.type())
361  {
362  add_to_operands(_op);
363  }
364 
365  DEPRECATED("use unary_exprt(id, op, type) instead")
367  const irep_idt &_id,
368  const typet &_type):exprt(_id, _type)
369  {
370  operands().resize(1);
371  }
372 
374  const irep_idt &_id,
375  const exprt &_op,
376  const typet &_type):
377  exprt(_id, _type)
378  {
379  add_to_operands(_op);
380  }
381 
382  const exprt &op() const
383  {
384  return op0();
385  }
386 
388  {
389  return op0();
390  }
391 
392  const exprt &op1() const = delete;
393  exprt &op1() = delete;
394  const exprt &op2() const = delete;
395  exprt &op2() = delete;
396  const exprt &op3() const = delete;
397  exprt &op3() = delete;
398 };
399 
406 inline const unary_exprt &to_unary_expr(const exprt &expr)
407 {
409  expr.operands().size()==1,
410  "Unary expressions must have one operand");
411  return static_cast<const unary_exprt &>(expr);
412 }
413 
416 {
418  expr.operands().size()==1,
419  "Unary expressions must have one operand");
420  return static_cast<unary_exprt &>(expr);
421 }
422 
423 template<> inline bool can_cast_expr<unary_exprt>(const exprt &base)
424 {
425  return base.operands().size()==1;
426 }
427 
428 
430 class abs_exprt:public unary_exprt
431 {
432 public:
433  DEPRECATED("use abs_exprt(op) instead")
435  {
436  }
437 
438  explicit abs_exprt(const exprt &_op):
439  unary_exprt(ID_abs, _op, _op.type())
440  {
441  }
442 };
443 
450 inline const abs_exprt &to_abs_expr(const exprt &expr)
451 {
452  PRECONDITION(expr.id()==ID_abs);
454  expr.operands().size()==1,
455  "Absolute value must have one operand");
456  return static_cast<const abs_exprt &>(expr);
457 }
458 
461 {
462  PRECONDITION(expr.id()==ID_abs);
464  expr.operands().size()==1,
465  "Absolute value must have one operand");
466  return static_cast<abs_exprt &>(expr);
467 }
468 
469 template<> inline bool can_cast_expr<abs_exprt>(const exprt &base)
470 {
471  return base.id()==ID_abs;
472 }
473 inline void validate_expr(const abs_exprt &value)
474 {
475  validate_operands(value, 1, "Absolute value must have one operand");
476 }
477 
478 
481 {
482 public:
483  DEPRECATED("use unary_minus_exprt(op) instead")
484  unary_minus_exprt():unary_exprt(ID_unary_minus)
485  {
486  }
487 
489  const exprt &_op,
490  const typet &_type):
491  unary_exprt(ID_unary_minus, _op, _type)
492  {
493  }
494 
495  explicit unary_minus_exprt(const exprt &_op):
496  unary_exprt(ID_unary_minus, _op, _op.type())
497  {
498  }
499 };
500 
507 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
508 {
509  PRECONDITION(expr.id()==ID_unary_minus);
511  expr.operands().size()==1,
512  "Unary minus must have one operand");
513  return static_cast<const unary_minus_exprt &>(expr);
514 }
515 
518 {
519  PRECONDITION(expr.id()==ID_unary_minus);
521  expr.operands().size()==1,
522  "Unary minus must have one operand");
523  return static_cast<unary_minus_exprt &>(expr);
524 }
525 
526 template<> inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
527 {
528  return base.id()==ID_unary_minus;
529 }
530 inline void validate_expr(const unary_minus_exprt &value)
531 {
532  validate_operands(value, 1, "Unary minus must have one operand");
533 }
534 
537 {
538 public:
539  explicit unary_plus_exprt(const exprt &op)
540  : unary_exprt(ID_unary_plus, op, op.type())
541  {
542  }
543 };
544 
551 inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
552 {
553  PRECONDITION(expr.id() == ID_unary_plus);
555  expr.operands().size() == 1, "unary plus must have one operand");
556  return static_cast<const unary_plus_exprt &>(expr);
557 }
558 
561 {
562  PRECONDITION(expr.id() == ID_unary_plus);
564  expr.operands().size() == 1, "unary plus must have one operand");
565  return static_cast<unary_plus_exprt &>(expr);
566 }
567 
568 template <>
569 inline bool can_cast_expr<unary_plus_exprt>(const exprt &base)
570 {
571  return base.id() == ID_unary_plus;
572 }
573 inline void validate_expr(const unary_plus_exprt &value)
574 {
575  validate_operands(value, 1, "unary plus must have one operand");
576 }
577 
580 {
581 public:
582  bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
583  : unary_exprt(ID_bswap, _op, _type)
584  {
585  set_bits_per_byte(bits_per_byte);
586  }
587 
588  bswap_exprt(const exprt &_op, std::size_t bits_per_byte)
589  : unary_exprt(ID_bswap, _op, _op.type())
590  {
591  set_bits_per_byte(bits_per_byte);
592  }
593 
594  std::size_t get_bits_per_byte() const
595  {
596  return get_size_t(ID_bits_per_byte);
597  }
598 
599  void set_bits_per_byte(std::size_t bits_per_byte)
600  {
601  set(ID_bits_per_byte, bits_per_byte);
602  }
603 };
604 
611 inline const bswap_exprt &to_bswap_expr(const exprt &expr)
612 {
613  PRECONDITION(expr.id() == ID_bswap);
614  DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand");
616  expr.op0().type() == expr.type(), "bswap type must match operand type");
617  return static_cast<const bswap_exprt &>(expr);
618 }
619 
622 {
623  PRECONDITION(expr.id() == ID_bswap);
624  DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand");
626  expr.op0().type() == expr.type(), "bswap type must match operand type");
627  return static_cast<bswap_exprt &>(expr);
628 }
629 
630 template <>
631 inline bool can_cast_expr<bswap_exprt>(const exprt &base)
632 {
633  return base.id() == ID_bswap;
634 }
635 inline void validate_expr(const bswap_exprt &value)
636 {
637  validate_operands(value, 1, "bswap must have one operand");
639  value.op().type() == value.type(), "bswap type must match operand type");
640 }
641 
644 class predicate_exprt:public exprt
645 {
646 public:
647  DEPRECATED("use predicate_exprt(id) instead")
649  {
650  }
651 
652  explicit predicate_exprt(const irep_idt &_id):
653  exprt(_id, bool_typet())
654  {
655  }
656 
657  DEPRECATED("use unary_predicate_exprt(id, op) instead")
659  const irep_idt &_id,
660  const exprt &_op):exprt(_id, bool_typet())
661  {
662  add_to_operands(_op);
663  }
664 
665  DEPRECATED("use binary_predicate_exprt(op1, id, op2) instead")
667  const irep_idt &_id,
668  const exprt &_op0,
669  const exprt &_op1):exprt(_id, bool_typet())
670  {
671  add_to_operands(_op0, _op1);
672  }
673 };
674 
678 {
679 public:
680  DEPRECATED("use unary_predicate_exprt(id, op) instead")
682  {
683  }
684 
685  DEPRECATED("use unary_predicate_exprt(id, op) instead")
686  explicit unary_predicate_exprt(const irep_idt &_id):
687  unary_exprt(_id, bool_typet())
688  {
689  }
690 
692  const irep_idt &_id,
693  const exprt &_op):unary_exprt(_id, _op, bool_typet())
694  {
695  }
696 
697 };
698 
702 {
703 public:
704  DEPRECATED("use sign_exprt(op) instead")
706  {
707  }
708 
709  explicit sign_exprt(const exprt &_op):
710  unary_predicate_exprt(ID_sign, _op)
711  {
712  }
713 };
714 
721 inline const sign_exprt &to_sign_expr(const exprt &expr)
722 {
723  PRECONDITION(expr.id() == ID_sign);
725  expr.operands().size() == 1, "sign expression must have one operand");
726  return static_cast<const sign_exprt &>(expr);
727 }
728 
731 {
732  PRECONDITION(expr.id() == ID_sign);
734  expr.operands().size() == 1, "sign expression must have one operand");
735  return static_cast<sign_exprt &>(expr);
736 }
737 
738 template <>
739 inline bool can_cast_expr<sign_exprt>(const exprt &base)
740 {
741  return base.id() == ID_sign;
742 }
743 inline void validate_expr(const sign_exprt &expr)
744 {
745  validate_operands(expr, 1, "sign expression must have one operand");
746 }
747 
749 class binary_exprt:public exprt
750 {
751 public:
752  DEPRECATED("use binary_exprt(lhs, id, rhs) instead")
754  {
755  operands().resize(2);
756  }
757 
758  DEPRECATED("use binary_exprt(lhs, id, rhs) instead")
759  explicit binary_exprt(const irep_idt &_id):exprt(_id)
760  {
761  operands().resize(2);
762  }
763 
764  DEPRECATED("use binary_exprt(lhs, id, rhs, type) instead")
766  const irep_idt &_id,
767  const typet &_type):exprt(_id, _type)
768  {
769  operands().resize(2);
770  }
771 
773  const exprt &_lhs,
774  const irep_idt &_id,
775  const exprt &_rhs):
776  exprt(_id, _lhs.type())
777  {
778  add_to_operands(_lhs, _rhs);
779  }
780 
782  const exprt &_lhs,
783  const irep_idt &_id,
784  const exprt &_rhs,
785  const typet &_type):
786  exprt(_id, _type)
787  {
788  add_to_operands(_lhs, _rhs);
789  }
790 
791  static void check(
792  const exprt &expr,
794  {
795  DATA_CHECK(
796  vm,
797  expr.operands().size() == 2,
798  "binary expression must have two operands");
799  }
800 
801  static void validate(
802  const exprt &expr,
803  const namespacet &,
805  {
806  check(expr, vm);
807  }
808 
809  const exprt &op2() const = delete;
810  exprt &op2() = delete;
811  const exprt &op3() const = delete;
812  exprt &op3() = delete;
813 };
814 
821 inline const binary_exprt &to_binary_expr(const exprt &expr)
822 {
824  expr.operands().size()==2,
825  "Binary expressions must have two operands");
826  return static_cast<const binary_exprt &>(expr);
827 }
828 
831 {
833  expr.operands().size()==2,
834  "Binary expressions must have two operands");
835  return static_cast<binary_exprt &>(expr);
836 }
837 
838 template<> inline bool can_cast_expr<binary_exprt>(const exprt &base)
839 {
840  return base.operands().size()==2;
841 }
842 
846 {
847 public:
848  DEPRECATED("use binary_predicate_exprt(lhs, id, rhs) instead")
850  {
851  }
852 
853  DEPRECATED("use binary_predicate_exprt(lhs, id, rhs) instead")
854  explicit binary_predicate_exprt(const irep_idt &_id):
855  binary_exprt(_id, bool_typet())
856  {
857  }
858 
860  const exprt &_op0,
861  const irep_idt &_id,
862  const exprt &_op1):binary_exprt(_op0, _id, _op1, bool_typet())
863  {
864  }
865 
866  static void check(
867  const exprt &expr,
869  {
870  binary_exprt::check(expr, vm);
871  }
872 
873  static void validate(
874  const exprt &expr,
875  const namespacet &ns,
877  {
878  binary_exprt::validate(expr, ns, vm);
879 
880  DATA_CHECK(
881  vm,
882  expr.type().id() == ID_bool,
883  "result of binary predicate expression should be of type bool");
884  }
885 };
886 
889 {
890 public:
891  DEPRECATED("use binary_relation_exprt(lhs, id, rhs) instead")
893  {
894  }
895 
896  DEPRECATED("use binary_relation_exprt(lhs, id, rhs) instead")
897  explicit binary_relation_exprt(const irep_idt &id):
899  {
900  }
901 
903  const exprt &_lhs,
904  const irep_idt &_id,
905  const exprt &_rhs):
906  binary_predicate_exprt(_lhs, _id, _rhs)
907  {
908  }
909 
910  static void check(
911  const exprt &expr,
913  {
915  }
916 
917  static void validate(
918  const exprt &expr,
919  const namespacet &ns,
921  {
922  binary_predicate_exprt::validate(expr, ns, vm);
923 
924  // check types
925  DATA_CHECK(
926  vm,
927  base_type_eq(expr.op0().type(), expr.op1().type(), ns),
928  "lhs and rhs of binary relation expression should have same type");
929  }
930 
932  {
933  return op0();
934  }
935 
936  const exprt &lhs() const
937  {
938  return op0();
939  }
940 
942  {
943  return op1();
944  }
945 
946  const exprt &rhs() const
947  {
948  return op1();
949  }
950 };
951 
959 {
961  expr.operands().size()==2,
962  "Binary relations must have two operands");
963  return static_cast<const binary_relation_exprt &>(expr);
964 }
965 
968 {
970  expr.operands().size()==2,
971  "Binary relations must have two operands");
972  return static_cast<binary_relation_exprt &>(expr);
973 }
974 
975 template<> inline bool can_cast_expr<binary_relation_exprt>(const exprt &base)
976 {
977  return can_cast_expr<binary_exprt>(base);
978 }
979 
980 
983 class multi_ary_exprt:public exprt
984 {
985 public:
986  DEPRECATED("use multi_ary_exprt(id, op, type) instead")
988  {
989  }
990 
991  DEPRECATED("use multi_ary_exprt(id, op, type) instead")
992  explicit multi_ary_exprt(const irep_idt &_id):exprt(_id)
993  {
994  }
995 
996  DEPRECATED("use multi_ary_exprt(id, op, type) instead")
998  const irep_idt &_id,
999  const typet &_type):exprt(_id, _type)
1000  {
1001  }
1002 
1004  const irep_idt &_id,
1005  operandst &&_operands,
1006  const typet &_type)
1007  : exprt(_id, _type)
1008  {
1009  operands() = std::move(_operands);
1010  }
1011 
1013  const exprt &_lhs,
1014  const irep_idt &_id,
1015  const exprt &_rhs):
1016  exprt(_id, _lhs.type())
1017  {
1018  add_to_operands(_lhs, _rhs);
1019  }
1020 
1022  const exprt &_lhs,
1023  const irep_idt &_id,
1024  const exprt &_rhs,
1025  const typet &_type):
1026  exprt(_id, _type)
1027  {
1028  add_to_operands(_lhs, _rhs);
1029  }
1030 };
1031 
1038 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
1039 {
1040  return static_cast<const multi_ary_exprt &>(expr);
1041 }
1042 
1045 {
1046  return static_cast<multi_ary_exprt &>(expr);
1047 }
1048 
1049 
1053 {
1054 public:
1055  DEPRECATED("use plus_exprt(lhs, rhs) instead")
1057  {
1058  }
1059 
1060  DEPRECATED("use plus_exprt(lhs, rhs, type) instead")
1062  {
1063  }
1064 
1066  const exprt &_lhs,
1067  const exprt &_rhs):
1068  multi_ary_exprt(_lhs, ID_plus, _rhs)
1069  {
1070  }
1071 
1073  const exprt &_lhs,
1074  const exprt &_rhs,
1075  const typet &_type):
1076  multi_ary_exprt(_lhs, ID_plus, _rhs, _type)
1077  {
1078  }
1079 
1080  plus_exprt(operandst &&_operands, const typet &_type)
1081  : multi_ary_exprt(ID_plus, std::move(_operands), _type)
1082  {
1083  }
1084 };
1085 
1092 inline const plus_exprt &to_plus_expr(const exprt &expr)
1093 {
1094  PRECONDITION(expr.id()==ID_plus);
1096  expr.operands().size()>=2,
1097  "Plus must have two or more operands");
1098  return static_cast<const plus_exprt &>(expr);
1099 }
1100 
1103 {
1104  PRECONDITION(expr.id()==ID_plus);
1106  expr.operands().size()>=2,
1107  "Plus must have two or more operands");
1108  return static_cast<plus_exprt &>(expr);
1109 }
1110 
1111 template<> inline bool can_cast_expr<plus_exprt>(const exprt &base)
1112 {
1113  return base.id()==ID_plus;
1114 }
1115 inline void validate_expr(const plus_exprt &value)
1116 {
1117  validate_operands(value, 2, "Plus must have two or more operands", true);
1118 }
1119 
1120 
1123 {
1124 public:
1125  DEPRECATED("use minus_exprt(lhs, rhs) instead")
1127  {
1128  }
1129 
1131  const exprt &_lhs,
1132  const exprt &_rhs):
1133  binary_exprt(_lhs, ID_minus, _rhs)
1134  {
1135  }
1136 };
1137 
1144 inline const minus_exprt &to_minus_expr(const exprt &expr)
1145 {
1146  PRECONDITION(expr.id()==ID_minus);
1148  expr.operands().size()>=2,
1149  "Minus must have two or more operands");
1150  return static_cast<const minus_exprt &>(expr);
1151 }
1152 
1155 {
1156  PRECONDITION(expr.id()==ID_minus);
1158  expr.operands().size()>=2,
1159  "Minus must have two or more operands");
1160  return static_cast<minus_exprt &>(expr);
1161 }
1162 
1163 template<> inline bool can_cast_expr<minus_exprt>(const exprt &base)
1164 {
1165  return base.id()==ID_minus;
1166 }
1167 inline void validate_expr(const minus_exprt &value)
1168 {
1169  validate_operands(value, 2, "Minus must have two or more operands", true);
1170 }
1171 
1172 
1176 {
1177 public:
1178  DEPRECATED("use mult_exprt(lhs, rhs) instead")
1180  {
1181  }
1182 
1184  const exprt &_lhs,
1185  const exprt &_rhs):
1186  multi_ary_exprt(_lhs, ID_mult, _rhs)
1187  {
1188  }
1189 };
1190 
1197 inline const mult_exprt &to_mult_expr(const exprt &expr)
1198 {
1199  PRECONDITION(expr.id()==ID_mult);
1201  expr.operands().size()>=2,
1202  "Multiply must have two or more operands");
1203  return static_cast<const mult_exprt &>(expr);
1204 }
1205 
1208 {
1209  PRECONDITION(expr.id()==ID_mult);
1211  expr.operands().size()>=2,
1212  "Multiply must have two or more operands");
1213  return static_cast<mult_exprt &>(expr);
1214 }
1215 
1216 template<> inline bool can_cast_expr<mult_exprt>(const exprt &base)
1217 {
1218  return base.id()==ID_mult;
1219 }
1220 inline void validate_expr(const mult_exprt &value)
1221 {
1222  validate_operands(value, 2, "Multiply must have two or more operands", true);
1223 }
1224 
1225 
1228 {
1229 public:
1230  DEPRECATED("use div_exprt(lhs, rhs) instead")
1232  {
1233  }
1234 
1236  const exprt &_lhs,
1237  const exprt &_rhs):
1238  binary_exprt(_lhs, ID_div, _rhs)
1239  {
1240  }
1241 
1244  {
1245  return op0();
1246  }
1247 
1249  const exprt &dividend() const
1250  {
1251  return op0();
1252  }
1253 
1256  {
1257  return op1();
1258  }
1259 
1261  const exprt &divisor() const
1262  {
1263  return op1();
1264  }
1265 };
1266 
1273 inline const div_exprt &to_div_expr(const exprt &expr)
1274 {
1275  PRECONDITION(expr.id()==ID_div);
1277  expr.operands().size()==2,
1278  "Divide must have two operands");
1279  return static_cast<const div_exprt &>(expr);
1280 }
1281 
1284 {
1285  PRECONDITION(expr.id()==ID_div);
1287  expr.operands().size()==2,
1288  "Divide must have two operands");
1289  return static_cast<div_exprt &>(expr);
1290 }
1291 
1292 template<> inline bool can_cast_expr<div_exprt>(const exprt &base)
1293 {
1294  return base.id()==ID_div;
1295 }
1296 inline void validate_expr(const div_exprt &value)
1297 {
1298  validate_operands(value, 2, "Divide must have two operands");
1299 }
1300 
1301 
1304 {
1305 public:
1306  DEPRECATED("use mod_exprt(lhs, rhs) instead")
1308  {
1309  }
1310 
1312  const exprt &_lhs,
1313  const exprt &_rhs):
1314  binary_exprt(_lhs, ID_mod, _rhs)
1315  {
1316  }
1317 };
1318 
1325 inline const mod_exprt &to_mod_expr(const exprt &expr)
1326 {
1327  PRECONDITION(expr.id()==ID_mod);
1328  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
1329  return static_cast<const mod_exprt &>(expr);
1330 }
1331 
1334 {
1335  PRECONDITION(expr.id()==ID_mod);
1336  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
1337  return static_cast<mod_exprt &>(expr);
1338 }
1339 
1340 template<> inline bool can_cast_expr<mod_exprt>(const exprt &base)
1341 {
1342  return base.id()==ID_mod;
1343 }
1344 inline void validate_expr(const mod_exprt &value)
1345 {
1346  validate_operands(value, 2, "Modulo must have two operands");
1347 }
1348 
1349 
1352 {
1353 public:
1354  DEPRECATED("use rem_exprt(lhs, rhs) instead")
1356  {
1357  }
1358 
1360  const exprt &_lhs,
1361  const exprt &_rhs):
1362  binary_exprt(_lhs, ID_rem, _rhs)
1363  {
1364  }
1365 };
1366 
1373 inline const rem_exprt &to_rem_expr(const exprt &expr)
1374 {
1375  PRECONDITION(expr.id()==ID_rem);
1376  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
1377  return static_cast<const rem_exprt &>(expr);
1378 }
1379 
1382 {
1383  PRECONDITION(expr.id()==ID_rem);
1384  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
1385  return static_cast<rem_exprt &>(expr);
1386 }
1387 
1388 template<> inline bool can_cast_expr<rem_exprt>(const exprt &base)
1389 {
1390  return base.id()==ID_rem;
1391 }
1392 inline void validate_expr(const rem_exprt &value)
1393 {
1394  validate_operands(value, 2, "Remainder must have two operands");
1395 }
1396 
1397 
1400 {
1401 public:
1402  DEPRECATED("use power_exprt(lhs, rhs) instead")
1404  {
1405  }
1406 
1408  const exprt &_base,
1409  const exprt &_exp):
1410  binary_exprt(_base, ID_power, _exp)
1411  {
1412  }
1413 };
1414 
1421 inline const power_exprt &to_power_expr(const exprt &expr)
1422 {
1423  PRECONDITION(expr.id()==ID_power);
1424  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
1425  return static_cast<const power_exprt &>(expr);
1426 }
1427 
1430 {
1431  PRECONDITION(expr.id()==ID_power);
1432  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
1433  return static_cast<power_exprt &>(expr);
1434 }
1435 
1436 template<> inline bool can_cast_expr<power_exprt>(const exprt &base)
1437 {
1438  return base.id()==ID_power;
1439 }
1440 inline void validate_expr(const power_exprt &value)
1441 {
1442  validate_operands(value, 2, "Power must have two operands");
1443 }
1444 
1445 
1448 {
1449 public:
1450  DEPRECATED("use factorial_power_exprt(lhs, rhs) instead")
1451  factorial_power_exprt():binary_exprt(ID_factorial_power)
1452  {
1453  }
1454 
1456  const exprt &_base,
1457  const exprt &_exp):
1458  binary_exprt(_base, ID_factorial_power, _exp)
1459  {
1460  }
1461 };
1462 
1470 {
1471  PRECONDITION(expr.id()==ID_factorial_power);
1473  expr.operands().size()==2,
1474  "Factorial power must have two operands");
1475  return static_cast<const factorial_power_exprt &>(expr);
1476 }
1477 
1480 {
1481  PRECONDITION(expr.id()==ID_factorial_power);
1483  expr.operands().size()==2,
1484  "Factorial power must have two operands");
1485  return static_cast<factorial_power_exprt &>(expr);
1486 }
1487 
1489  const exprt &base)
1490 {
1491  return base.id()==ID_factorial_power;
1492 }
1493 inline void validate_expr(const factorial_power_exprt &value)
1494 {
1495  validate_operands(value, 2, "Factorial power must have two operands");
1496 }
1497 
1498 
1501 {
1502 public:
1503  DEPRECATED("use equal_exprt(lhs, rhs) instead")
1505  {
1506  }
1507 
1508  equal_exprt(const exprt &_lhs, const exprt &_rhs):
1509  binary_relation_exprt(_lhs, ID_equal, _rhs)
1510  {
1511  }
1512 
1513  static void check(
1514  const exprt &expr,
1516  {
1517  binary_relation_exprt::check(expr, vm);
1518  }
1519 
1520  static void validate(
1521  const exprt &expr,
1522  const namespacet &ns,
1524  {
1525  binary_relation_exprt::validate(expr, ns, vm);
1526  }
1527 };
1528 
1535 inline const equal_exprt &to_equal_expr(const exprt &expr)
1536 {
1537  PRECONDITION(expr.id()==ID_equal);
1538  equal_exprt::check(expr);
1539  return static_cast<const equal_exprt &>(expr);
1540 }
1541 
1544 {
1545  PRECONDITION(expr.id()==ID_equal);
1546  equal_exprt::check(expr);
1547  return static_cast<equal_exprt &>(expr);
1548 }
1549 
1550 template<> inline bool can_cast_expr<equal_exprt>(const exprt &base)
1551 {
1552  return base.id()==ID_equal;
1553 }
1554 inline void validate_expr(const equal_exprt &value)
1555 {
1556  validate_operands(value, 2, "Equality must have two operands");
1557 }
1558 
1559 
1562 {
1563 public:
1564  DEPRECATED("use notequal_exprt(lhs, rhs) instead")
1566  {
1567  }
1568 
1569  notequal_exprt(const exprt &_lhs, const exprt &_rhs):
1570  binary_relation_exprt(_lhs, ID_notequal, _rhs)
1571  {
1572  }
1573 };
1574 
1581 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1582 {
1583  PRECONDITION(expr.id()==ID_notequal);
1585  expr.operands().size()==2,
1586  "Inequality must have two operands");
1587  return static_cast<const notequal_exprt &>(expr);
1588 }
1589 
1592 {
1593  PRECONDITION(expr.id()==ID_notequal);
1595  expr.operands().size()==2,
1596  "Inequality must have two operands");
1597  return static_cast<notequal_exprt &>(expr);
1598 }
1599 
1600 template<> inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1601 {
1602  return base.id()==ID_notequal;
1603 }
1604 inline void validate_expr(const notequal_exprt &value)
1605 {
1606  validate_operands(value, 2, "Inequality must have two operands");
1607 }
1608 
1609 
1612 {
1613 public:
1614  DEPRECATED("use index_exprt(array, index) instead")
1616  {
1617  }
1618 
1619  DEPRECATED("use index_exprt(array, index) instead")
1620  explicit index_exprt(const typet &_type):binary_exprt(ID_index, _type)
1621  {
1622  }
1623 
1624  index_exprt(const exprt &_array, const exprt &_index):
1625  binary_exprt(_array, ID_index, _index, _array.type().subtype())
1626  {
1627  }
1628 
1630  const exprt &_array,
1631  const exprt &_index,
1632  const typet &_type):
1633  binary_exprt(_array, ID_index, _index, _type)
1634  {
1635  }
1636 
1638  {
1639  return op0();
1640  }
1641 
1642  const exprt &array() const
1643  {
1644  return op0();
1645  }
1646 
1648  {
1649  return op1();
1650  }
1651 
1652  const exprt &index() const
1653  {
1654  return op1();
1655  }
1656 };
1657 
1664 inline const index_exprt &to_index_expr(const exprt &expr)
1665 {
1666  PRECONDITION(expr.id()==ID_index);
1668  expr.operands().size()==2,
1669  "Array index must have two operands");
1670  return static_cast<const index_exprt &>(expr);
1671 }
1672 
1675 {
1676  PRECONDITION(expr.id()==ID_index);
1678  expr.operands().size()==2,
1679  "Array index must have two operands");
1680  return static_cast<index_exprt &>(expr);
1681 }
1682 
1683 template<> inline bool can_cast_expr<index_exprt>(const exprt &base)
1684 {
1685  return base.id()==ID_index;
1686 }
1687 inline void validate_expr(const index_exprt &value)
1688 {
1689  validate_operands(value, 2, "Array index must have two operands");
1690 }
1691 
1692 
1695 {
1696 public:
1697  DEPRECATED("use array_of_exprt(what, type) instead")
1699  {
1700  }
1701 
1702  explicit array_of_exprt(
1703  const exprt &_what, const array_typet &_type):
1704  unary_exprt(ID_array_of, _what, _type)
1705  {
1706  }
1707 
1709  {
1710  return op0();
1711  }
1712 
1713  const exprt &what() const
1714  {
1715  return op0();
1716  }
1717 };
1718 
1725 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1726 {
1727  PRECONDITION(expr.id()==ID_array_of);
1729  expr.operands().size()==1,
1730  "'Array of' must have one operand");
1731  return static_cast<const array_of_exprt &>(expr);
1732 }
1733 
1736 {
1737  PRECONDITION(expr.id()==ID_array_of);
1739  expr.operands().size()==1,
1740  "'Array of' must have one operand");
1741  return static_cast<array_of_exprt &>(expr);
1742 }
1743 
1744 template<> inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1745 {
1746  return base.id()==ID_array_of;
1747 }
1748 inline void validate_expr(const array_of_exprt &value)
1749 {
1750  validate_operands(value, 1, "'Array of' must have one operand");
1751 }
1752 
1753 
1756 {
1757 public:
1758  DEPRECATED("use array_exprt(type) instead")
1760  {
1761  }
1762 
1763  DEPRECATED("use array_exprt(operands, type) instead")
1764  explicit array_exprt(const array_typet &_type)
1765  : multi_ary_exprt(ID_array, _type)
1766  {
1767  }
1768 };
1769 
1776 inline const array_exprt &to_array_expr(const exprt &expr)
1777 {
1778  PRECONDITION(expr.id()==ID_array);
1779  return static_cast<const array_exprt &>(expr);
1780 }
1781 
1784 {
1785  PRECONDITION(expr.id()==ID_array);
1786  return static_cast<array_exprt &>(expr);
1787 }
1788 
1789 template<> inline bool can_cast_expr<array_exprt>(const exprt &base)
1790 {
1791  return base.id()==ID_array;
1792 }
1793 
1797 {
1798 public:
1799  DEPRECATED("use array_list_exprt(operands, type) instead")
1800  explicit array_list_exprt(const array_typet &_type)
1801  : multi_ary_exprt(ID_array_list, _type)
1802  {
1803  }
1804 
1805  array_list_exprt(operandst &&_operands, const array_typet &_type)
1806  : multi_ary_exprt(ID_array_list, std::move(_operands), _type)
1807  {
1808  }
1809 };
1810 
1811 template <>
1812 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1813 {
1814  return base.id() == ID_array_list;
1815 }
1816 
1817 inline void validate_expr(const array_list_exprt &value)
1818 {
1819  PRECONDITION(value.operands().size() % 2 == 0);
1820 }
1821 
1824 {
1825 public:
1826  DEPRECATED("use vector_exprt(type) instead")
1828  {
1829  }
1830 
1831  DEPRECATED("use vector_exprt(operands, type) instead")
1832  explicit vector_exprt(const vector_typet &_type)
1833  : multi_ary_exprt(ID_vector, _type)
1834  {
1835  }
1836 
1837  vector_exprt(operandst &&_operands, const vector_typet &_type)
1838  : multi_ary_exprt(ID_vector, std::move(_operands), _type)
1839  {
1840  }
1841 };
1842 
1849 inline const vector_exprt &to_vector_expr(const exprt &expr)
1850 {
1851  PRECONDITION(expr.id()==ID_vector);
1852  return static_cast<const vector_exprt &>(expr);
1853 }
1854 
1857 {
1858  PRECONDITION(expr.id()==ID_vector);
1859  return static_cast<vector_exprt &>(expr);
1860 }
1861 
1862 template<> inline bool can_cast_expr<vector_exprt>(const exprt &base)
1863 {
1864  return base.id()==ID_vector;
1865 }
1866 
1867 
1870 {
1871 public:
1872  DEPRECATED("use union_exprt(component_name, value, type) instead")
1874  {
1875  }
1876 
1877  DEPRECATED("use union_exprt(component_name, value, type) instead")
1878  explicit union_exprt(const typet &_type):
1879  unary_exprt(ID_union, _type)
1880  {
1881  }
1882 
1884  const irep_idt &_component_name,
1885  const exprt &_value,
1886  const typet &_type)
1887  : unary_exprt(ID_union, _value, _type)
1888  {
1889  set_component_name(_component_name);
1890  }
1891 
1893  {
1894  return get(ID_component_name);
1895  }
1896 
1897  void set_component_name(const irep_idt &component_name)
1898  {
1899  set(ID_component_name, component_name);
1900  }
1901 
1902  std::size_t get_component_number() const
1903  {
1904  return get_size_t(ID_component_number);
1905  }
1906 
1907  void set_component_number(std::size_t component_number)
1908  {
1909  set(ID_component_number, component_number);
1910  }
1911 };
1912 
1919 inline const union_exprt &to_union_expr(const exprt &expr)
1920 {
1921  PRECONDITION(expr.id()==ID_union);
1923  expr.operands().size()==1,
1924  "Union constructor must have one operand");
1925  return static_cast<const union_exprt &>(expr);
1926 }
1927 
1930 {
1931  PRECONDITION(expr.id()==ID_union);
1933  expr.operands().size()==1,
1934  "Union constructor must have one operand");
1935  return static_cast<union_exprt &>(expr);
1936 }
1937 
1938 template<> inline bool can_cast_expr<union_exprt>(const exprt &base)
1939 {
1940  return base.id()==ID_union;
1941 }
1942 inline void validate_expr(const union_exprt &value)
1943 {
1944  validate_operands(value, 1, "Union constructor must have one operand");
1945 }
1946 
1947 
1950 {
1951 public:
1952  DEPRECATED("use struct_exprt(component_name, value, type) instead")
1954  {
1955  }
1956 
1957  DEPRECATED("use struct_exprt(component_name, value, type) instead")
1958  explicit struct_exprt(const typet &_type) : multi_ary_exprt(ID_struct, _type)
1959  {
1960  }
1961 
1962  struct_exprt(operandst &&_operands, const typet &_type)
1963  : multi_ary_exprt(ID_struct, std::move(_operands), _type)
1964  {
1965  }
1966 
1967  exprt &component(const irep_idt &name, const namespacet &ns);
1968  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1969 };
1970 
1977 inline const struct_exprt &to_struct_expr(const exprt &expr)
1978 {
1979  PRECONDITION(expr.id()==ID_struct);
1980  return static_cast<const struct_exprt &>(expr);
1981 }
1982 
1985 {
1986  PRECONDITION(expr.id()==ID_struct);
1987  return static_cast<struct_exprt &>(expr);
1988 }
1989 
1990 template<> inline bool can_cast_expr<struct_exprt>(const exprt &base)
1991 {
1992  return base.id()==ID_struct;
1993 }
1994 
1995 
1998 {
1999 public:
2000  DEPRECATED("use complex_exprt(r, i, type) instead")
2002  {
2003  }
2004 
2005  DEPRECATED("use complex_exprt(r, i, type) instead")
2006  explicit complex_exprt(const complex_typet &_type):
2007  binary_exprt(ID_complex, _type)
2008  {
2009  }
2010 
2012  const exprt &_real,
2013  const exprt &_imag,
2014  const complex_typet &_type)
2015  : binary_exprt(_real, ID_complex, _imag, _type)
2016  {
2017  }
2018 
2020  {
2021  return op0();
2022  }
2023 
2024  const exprt &real() const
2025  {
2026  return op0();
2027  }
2028 
2030  {
2031  return op1();
2032  }
2033 
2034  const exprt &imag() const
2035  {
2036  return op1();
2037  }
2038 };
2039 
2046 inline const complex_exprt &to_complex_expr(const exprt &expr)
2047 {
2048  PRECONDITION(expr.id()==ID_complex);
2050  expr.operands().size()==2,
2051  "Complex constructor must have two operands");
2052  return static_cast<const complex_exprt &>(expr);
2053 }
2054 
2057 {
2058  PRECONDITION(expr.id()==ID_complex);
2060  expr.operands().size()==2,
2061  "Complex constructor must have two operands");
2062  return static_cast<complex_exprt &>(expr);
2063 }
2064 
2065 template<> inline bool can_cast_expr<complex_exprt>(const exprt &base)
2066 {
2067  return base.id()==ID_complex;
2068 }
2069 inline void validate_expr(const complex_exprt &value)
2070 {
2071  validate_operands(value, 2, "Complex constructor must have two operands");
2072 }
2073 
2076 {
2077 public:
2078  explicit complex_real_exprt(const exprt &op)
2079  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
2080  {
2081  }
2082 };
2083 
2091 {
2092  PRECONDITION(expr.id() == ID_complex_real);
2094  expr.operands().size() == 1,
2095  "real part retrieval operation must have one operand");
2096  return static_cast<const complex_real_exprt &>(expr);
2097 }
2098 
2101 {
2102  PRECONDITION(expr.id() == ID_complex_real);
2104  expr.operands().size() == 1,
2105  "real part retrieval operation must have one operand");
2106  return static_cast<complex_real_exprt &>(expr);
2107 }
2108 
2109 template <>
2111 {
2112  return base.id() == ID_complex_real;
2113 }
2114 
2115 inline void validate_expr(const complex_real_exprt &expr)
2116 {
2118  expr, 1, "real part retrieval operation must have one operand");
2119 }
2120 
2123 {
2124 public:
2125  explicit complex_imag_exprt(const exprt &op)
2126  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
2127  {
2128  }
2129 };
2130 
2138 {
2139  PRECONDITION(expr.id() == ID_complex_imag);
2141  expr.operands().size() == 1,
2142  "imaginary part retrieval operation must have one operand");
2143  return static_cast<const complex_imag_exprt &>(expr);
2144 }
2145 
2148 {
2149  PRECONDITION(expr.id() == ID_complex_imag);
2151  expr.operands().size() == 1,
2152  "imaginary part retrieval operation must have one operand");
2153  return static_cast<complex_imag_exprt &>(expr);
2154 }
2155 
2156 template <>
2158 {
2159  return base.id() == ID_complex_imag;
2160 }
2161 
2162 inline void validate_expr(const complex_imag_exprt &expr)
2163 {
2165  expr, 1, "imaginary part retrieval operation must have one operand");
2166 }
2167 
2168 class namespacet;
2169 
2172 {
2173 public:
2175  : binary_exprt(exprt(ID_unknown), ID_object_descriptor, exprt(ID_unknown))
2176  {
2177  }
2178 
2179  void build(const exprt &expr, const namespacet &ns);
2180 
2182  {
2183  return op0();
2184  }
2185 
2186  const exprt &object() const
2187  {
2188  return op0();
2189  }
2190 
2191  const exprt &root_object() const;
2192 
2194  {
2195  return op1();
2196  }
2197 
2198  const exprt &offset() const
2199  {
2200  return op1();
2201  }
2202 };
2203 
2211  const exprt &expr)
2212 {
2213  PRECONDITION(expr.id()==ID_object_descriptor);
2215  expr.operands().size()==2,
2216  "Object descriptor must have two operands");
2217  return static_cast<const object_descriptor_exprt &>(expr);
2218 }
2219 
2222 {
2223  PRECONDITION(expr.id()==ID_object_descriptor);
2225  expr.operands().size()==2,
2226  "Object descriptor must have two operands");
2227  return static_cast<object_descriptor_exprt &>(expr);
2228 }
2229 
2230 template<>
2232 {
2233  return base.id()==ID_object_descriptor;
2234 }
2235 inline void validate_expr(const object_descriptor_exprt &value)
2236 {
2237  validate_operands(value, 2, "Object descriptor must have two operands");
2238 }
2239 
2240 
2243 {
2244 public:
2246  : binary_exprt(exprt(ID_unknown), ID_dynamic_object, exprt(ID_unknown))
2247  {
2248  }
2249 
2251  : binary_exprt(
2252  exprt(ID_unknown),
2253  ID_dynamic_object,
2254  exprt(ID_unknown),
2255  type)
2256  {
2257  }
2258 
2259  void set_instance(unsigned int instance);
2260 
2261  unsigned int get_instance() const;
2262 
2264  {
2265  return op1();
2266  }
2267 
2268  const exprt &valid() const
2269  {
2270  return op1();
2271  }
2272 };
2273 
2281  const exprt &expr)
2282 {
2283  PRECONDITION(expr.id()==ID_dynamic_object);
2285  expr.operands().size()==2,
2286  "Dynamic object must have two operands");
2287  return static_cast<const dynamic_object_exprt &>(expr);
2288 }
2289 
2292 {
2293  PRECONDITION(expr.id()==ID_dynamic_object);
2295  expr.operands().size()==2,
2296  "Dynamic object must have two operands");
2297  return static_cast<dynamic_object_exprt &>(expr);
2298 }
2299 
2300 template<> inline bool can_cast_expr<dynamic_object_exprt>(const exprt &base)
2301 {
2302  return base.id()==ID_dynamic_object;
2303 }
2304 
2305 inline void validate_expr(const dynamic_object_exprt &value)
2306 {
2307  validate_operands(value, 2, "Dynamic object must have two operands");
2308 }
2309 
2310 
2313 {
2314 public:
2315  DEPRECATED("use typecast_exprt(op, type) instead")
2316  explicit typecast_exprt(const typet &_type):unary_exprt(ID_typecast, _type)
2317  {
2318  }
2319 
2320  typecast_exprt(const exprt &op, const typet &_type):
2321  unary_exprt(ID_typecast, op, _type)
2322  {
2323  }
2324 
2325  // returns a typecast if the type doesn't already match
2326  static exprt conditional_cast(const exprt &expr, const typet &type)
2327  {
2328  if(expr.type() == type)
2329  return expr;
2330  else
2331  return typecast_exprt(expr, type);
2332  }
2333 };
2334 
2341 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2342 {
2343  PRECONDITION(expr.id()==ID_typecast);
2345  expr.operands().size()==1,
2346  "Typecast must have one operand");
2347  return static_cast<const typecast_exprt &>(expr);
2348 }
2349 
2352 {
2353  PRECONDITION(expr.id()==ID_typecast);
2355  expr.operands().size()==1,
2356  "Typecast must have one operand");
2357  return static_cast<typecast_exprt &>(expr);
2358 }
2359 
2360 template<> inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2361 {
2362  return base.id()==ID_typecast;
2363 }
2364 inline void validate_expr(const typecast_exprt &value)
2365 {
2366  validate_operands(value, 1, "Typecast must have one operand");
2367 }
2368 
2369 
2372 {
2373 public:
2374  DEPRECATED("use floatbv_typecast_exprt(op, r, type) instead")
2375  floatbv_typecast_exprt():binary_exprt(ID_floatbv_typecast)
2376  {
2377  }
2378 
2380  const exprt &op,
2381  const exprt &rounding,
2382  const typet &_type):binary_exprt(op, ID_floatbv_typecast, rounding, _type)
2383  {
2384  }
2385 
2387  {
2388  return op0();
2389  }
2390 
2391  const exprt &op() const
2392  {
2393  return op0();
2394  }
2395 
2397  {
2398  return op1();
2399  }
2400 
2401  const exprt &rounding_mode() const
2402  {
2403  return op1();
2404  }
2405 };
2406 
2414 {
2415  PRECONDITION(expr.id()==ID_floatbv_typecast);
2417  expr.operands().size()==2,
2418  "Float typecast must have two operands");
2419  return static_cast<const floatbv_typecast_exprt &>(expr);
2420 }
2421 
2424 {
2425  PRECONDITION(expr.id()==ID_floatbv_typecast);
2427  expr.operands().size()==2,
2428  "Float typecast must have two operands");
2429  return static_cast<floatbv_typecast_exprt &>(expr);
2430 }
2431 
2432 template<>
2434 {
2435  return base.id()==ID_floatbv_typecast;
2436 }
2437 inline void validate_expr(const floatbv_typecast_exprt &value)
2438 {
2439  validate_operands(value, 2, "Float typecast must have two operands");
2440 }
2441 
2442 
2445 {
2446 public:
2447  DEPRECATED("use and_exprt(op, op) instead")
2449  {
2450  }
2451 
2452  and_exprt(const exprt &op0, const exprt &op1):
2453  multi_ary_exprt(op0, ID_and, op1, bool_typet())
2454  {
2455  }
2456 
2457  and_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
2458  : multi_ary_exprt(ID_and, {op0, op1, op2}, bool_typet())
2459  {
2460  }
2461 
2463  const exprt &op0,
2464  const exprt &op1,
2465  const exprt &op2,
2466  const exprt &op3)
2467  : multi_ary_exprt(ID_and, {op0, op1, op2, op3}, bool_typet())
2468  {
2469  }
2470 
2471  explicit and_exprt(exprt::operandst &&_operands)
2472  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2473  {
2474  }
2475 };
2476 
2480 
2482 
2489 inline const and_exprt &to_and_expr(const exprt &expr)
2490 {
2491  PRECONDITION(expr.id()==ID_and);
2492  // DATA_INVARIANT(
2493  // expr.operands().size()>=2,
2494  // "And must have two or more operands");
2495  return static_cast<const and_exprt &>(expr);
2496 }
2497 
2500 {
2501  PRECONDITION(expr.id()==ID_and);
2502  // DATA_INVARIANT(
2503  // expr.operands().size()>=2,
2504  // "And must have two or more operands");
2505  return static_cast<and_exprt &>(expr);
2506 }
2507 
2508 template<> inline bool can_cast_expr<and_exprt>(const exprt &base)
2509 {
2510  return base.id()==ID_and;
2511 }
2512 // inline void validate_expr(const and_exprt &value)
2513 // {
2514 // validate_operands(value, 2, "And must have two or more operands", true);
2515 // }
2516 
2517 
2520 {
2521 public:
2522  DEPRECATED("use implies_exprt(a, b) instead")
2524  {
2525  }
2526 
2527  implies_exprt(const exprt &op0, const exprt &op1):
2528  binary_exprt(op0, ID_implies, op1, bool_typet())
2529  {
2530  }
2531 };
2532 
2539 inline const implies_exprt &to_implies_expr(const exprt &expr)
2540 {
2541  PRECONDITION(expr.id()==ID_implies);
2542  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
2543  return static_cast<const implies_exprt &>(expr);
2544 }
2545 
2548 {
2549  PRECONDITION(expr.id()==ID_implies);
2550  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
2551  return static_cast<implies_exprt &>(expr);
2552 }
2553 
2554 template<> inline bool can_cast_expr<implies_exprt>(const exprt &base)
2555 {
2556  return base.id()==ID_implies;
2557 }
2558 inline void validate_expr(const implies_exprt &value)
2559 {
2560  validate_operands(value, 2, "Implies must have two operands");
2561 }
2562 
2563 
2566 {
2567 public:
2568  DEPRECATED("use or_exprt(op, op) instead")
2570  {
2571  }
2572 
2573  or_exprt(const exprt &op0, const exprt &op1):
2574  multi_ary_exprt(op0, ID_or, op1, bool_typet())
2575  {
2576  }
2577 
2578  or_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
2579  : multi_ary_exprt(ID_or, {op0, op1, op2}, bool_typet())
2580  {
2581  }
2582 
2584  const exprt &op0,
2585  const exprt &op1,
2586  const exprt &op2,
2587  const exprt &op3)
2588  : multi_ary_exprt(ID_or, {op0, op1, op2, op3}, bool_typet())
2589  {
2590  }
2591 
2592  explicit or_exprt(exprt::operandst &&_operands)
2593  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2594  {
2595  }
2596 };
2597 
2601 
2603 
2610 inline const or_exprt &to_or_expr(const exprt &expr)
2611 {
2612  PRECONDITION(expr.id()==ID_or);
2613  // DATA_INVARIANT(
2614  // expr.operands().size()>=2,
2615  // "Or must have two or more operands");
2616  return static_cast<const or_exprt &>(expr);
2617 }
2618 
2620 inline or_exprt &to_or_expr(exprt &expr)
2621 {
2622  PRECONDITION(expr.id()==ID_or);
2623  // DATA_INVARIANT(
2624  // expr.operands().size()>=2,
2625  // "Or must have two or more operands");
2626  return static_cast<or_exprt &>(expr);
2627 }
2628 
2629 template<> inline bool can_cast_expr<or_exprt>(const exprt &base)
2630 {
2631  return base.id()==ID_or;
2632 }
2633 // inline void validate_expr(const or_exprt &value)
2634 // {
2635 // validate_operands(value, 2, "Or must have two or more operands", true);
2636 // }
2637 
2638 
2641 {
2642 public:
2643  DEPRECATED("use xor_exprt(op, op) instead")
2645  {
2646  }
2647 
2648  xor_exprt(const exprt &_op0, const exprt &_op1):
2649  multi_ary_exprt(_op0, ID_xor, _op1, bool_typet())
2650  {
2651  }
2652 };
2653 
2660 inline const xor_exprt &to_xor_expr(const exprt &expr)
2661 {
2662  PRECONDITION(expr.id()==ID_xor);
2663  return static_cast<const xor_exprt &>(expr);
2664 }
2665 
2668 {
2669  PRECONDITION(expr.id()==ID_xor);
2670  return static_cast<xor_exprt &>(expr);
2671 }
2672 
2673 template<> inline bool can_cast_expr<xor_exprt>(const exprt &base)
2674 {
2675  return base.id()==ID_xor;
2676 }
2677 // inline void validate_expr(const bitxor_exprt &value)
2678 // {
2679 // validate_operands(
2680 // value,
2681 // 2,
2682 // "Bit-wise xor must have two or more operands",
2683 // true);
2684 // }
2685 
2686 
2689 {
2690 public:
2691  DEPRECATED("use bitnot_exprt(op) instead")
2693  {
2694  }
2695 
2696  explicit bitnot_exprt(const exprt &op):
2697  unary_exprt(ID_bitnot, op)
2698  {
2699  }
2700 };
2701 
2708 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
2709 {
2710  PRECONDITION(expr.id()==ID_bitnot);
2711  // DATA_INVARIANT(expr.operands().size()==1,
2712  // "Bit-wise not must have one operand");
2713  return static_cast<const bitnot_exprt &>(expr);
2714 }
2715 
2718 {
2719  PRECONDITION(expr.id()==ID_bitnot);
2720  // DATA_INVARIANT(expr.operands().size()==1,
2721  // "Bit-wise not must have one operand");
2722  return static_cast<bitnot_exprt &>(expr);
2723 }
2724 
2725 template<> inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
2726 {
2727  return base.id()==ID_bitnot;
2728 }
2729 // inline void validate_expr(const bitnot_exprt &value)
2730 // {
2731 // validate_operands(value, 1, "Bit-wise not must have one operand");
2732 // }
2733 
2734 
2737 {
2738 public:
2739  DEPRECATED("use bitor_exprt(op0, op1) instead")
2741  {
2742  }
2743 
2744  bitor_exprt(const exprt &_op0, const exprt &_op1)
2745  : multi_ary_exprt(_op0, ID_bitor, _op1, _op0.type())
2746  {
2747  }
2748 };
2749 
2756 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
2757 {
2758  PRECONDITION(expr.id()==ID_bitor);
2759  // DATA_INVARIANT(
2760  // expr.operands().size()>=2,
2761  // "Bit-wise or must have two or more operands");
2762  return static_cast<const bitor_exprt &>(expr);
2763 }
2764 
2767 {
2768  PRECONDITION(expr.id()==ID_bitor);
2769  // DATA_INVARIANT(
2770  // expr.operands().size()>=2,
2771  // "Bit-wise or must have two or more operands");
2772  return static_cast<bitor_exprt &>(expr);
2773 }
2774 
2775 template<> inline bool can_cast_expr<bitor_exprt>(const exprt &base)
2776 {
2777  return base.id()==ID_bitor;
2778 }
2779 // inline void validate_expr(const bitor_exprt &value)
2780 // {
2781 // validate_operands(
2782 // value,
2783 // 2,
2784 // "Bit-wise or must have two or more operands",
2785 // true);
2786 // }
2787 
2788 
2791 {
2792 public:
2793  DEPRECATED("use bitxor_exprt(op0, op1) instead")
2795  {
2796  }
2797 
2798  bitxor_exprt(const exprt &_op0, const exprt &_op1):
2799  multi_ary_exprt(_op0, ID_bitxor, _op1, _op0.type())
2800  {
2801  }
2802 };
2803 
2810 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
2811 {
2812  PRECONDITION(expr.id()==ID_bitxor);
2813  // DATA_INVARIANT(
2814  // expr.operands().size()>=2,
2815  // "Bit-wise xor must have two or more operands");
2816  return static_cast<const bitxor_exprt &>(expr);
2817 }
2818 
2821 {
2822  PRECONDITION(expr.id()==ID_bitxor);
2823  // DATA_INVARIANT(
2824  // expr.operands().size()>=2,
2825  // "Bit-wise xor must have two or more operands");
2826  return static_cast<bitxor_exprt &>(expr);
2827 }
2828 
2829 template<> inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
2830 {
2831  return base.id()==ID_bitxor;
2832 }
2833 // inline void validate_expr(const bitxor_exprt &value)
2834 // {
2835 // validate_operands(
2836 // value,
2837 // 2,
2838 // "Bit-wise xor must have two or more operands",
2839 // true);
2840 // }
2841 
2842 
2845 {
2846 public:
2847  DEPRECATED("use bitand_exprt(op0, op1) instead")
2849  {
2850  }
2851 
2852  bitand_exprt(const exprt &_op0, const exprt &_op1)
2853  : multi_ary_exprt(_op0, ID_bitand, _op1, _op0.type())
2854  {
2855  }
2856 };
2857 
2864 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
2865 {
2866  PRECONDITION(expr.id()==ID_bitand);
2867  // DATA_INVARIANT(
2868  // expr.operands().size()>=2,
2869  // "Bit-wise and must have two or more operands");
2870  return static_cast<const bitand_exprt &>(expr);
2871 }
2872 
2875 {
2876  PRECONDITION(expr.id()==ID_bitand);
2877  // DATA_INVARIANT(
2878  // expr.operands().size()>=2,
2879  // "Bit-wise and must have two or more operands");
2880  return static_cast<bitand_exprt &>(expr);
2881 }
2882 
2883 template<> inline bool can_cast_expr<bitand_exprt>(const exprt &base)
2884 {
2885  return base.id()==ID_bitand;
2886 }
2887 // inline void validate_expr(const bitand_exprt &value)
2888 // {
2889 // validate_operands(
2890 // value,
2891 // 2,
2892 // "Bit-wise and must have two or more operands",
2893 // true);
2894 // }
2895 
2896 
2899 {
2900 public:
2901  DEPRECATED("use shift_exprt(value, id, distance) instead")
2902  explicit shift_exprt(const irep_idt &_id):binary_exprt(_id)
2903  {
2904  }
2905 
2906  DEPRECATED("use shift_exprt(value, id, distance) instead")
2907  shift_exprt(const irep_idt &_id, const typet &_type):
2908  binary_exprt(_id, _type)
2909  {
2910  }
2911 
2912  shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance):
2913  binary_exprt(_src, _id, _distance)
2914  {
2915  }
2916 
2917  shift_exprt(
2918  const exprt &_src,
2919  const irep_idt &_id,
2920  const std::size_t _distance);
2921 
2923  {
2924  return op0();
2925  }
2926 
2927  const exprt &op() const
2928  {
2929  return op0();
2930  }
2931 
2933  {
2934  return op1();
2935  }
2936 
2937  const exprt &distance() const
2938  {
2939  return op1();
2940  }
2941 };
2942 
2949 inline const shift_exprt &to_shift_expr(const exprt &expr)
2950 {
2952  expr.operands().size()==2,
2953  "Shifts must have two operands");
2954  return static_cast<const shift_exprt &>(expr);
2955 }
2956 
2959 {
2961  expr.operands().size()==2,
2962  "Shifts must have two operands");
2963  return static_cast<shift_exprt &>(expr);
2964 }
2965 
2966 // The to_*_expr function for this type doesn't do any checks before casting,
2967 // therefore the implementation is essentially a static_cast.
2968 // Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
2969 // inline void validate_expr(const shift_exprt &value)
2970 // {
2971 // validate_operands(value, 2, "Shifts must have two operands");
2972 // }
2973 
2974 
2977 {
2978 public:
2979  DEPRECATED("use shl_exprt(value, distance) instead")
2981  {
2982  }
2983 
2984  shl_exprt(const exprt &_src, const exprt &_distance):
2985  shift_exprt(_src, ID_shl, _distance)
2986  {
2987  }
2988 
2989  shl_exprt(const exprt &_src, const std::size_t _distance):
2990  shift_exprt(_src, ID_shl, _distance)
2991  {
2992  }
2993 };
2994 
3001 inline const shl_exprt &to_shl_expr(const exprt &expr)
3002 {
3003  PRECONDITION(expr.id() == ID_shl);
3005  expr.operands().size() == 2, "Bit-wise shl must have two operands");
3006  return static_cast<const shl_exprt &>(expr);
3007 }
3008 
3011 {
3012  PRECONDITION(expr.id() == ID_shl);
3014  expr.operands().size() == 2, "Bit-wise shl must have two operands");
3015  return static_cast<shl_exprt &>(expr);
3016 }
3017 
3020 {
3021 public:
3022  DEPRECATED("use ashl_exprt(value, distance) instead")
3024  {
3025  }
3026 
3027  ashr_exprt(const exprt &_src, const exprt &_distance):
3028  shift_exprt(_src, ID_ashr, _distance)
3029  {
3030  }
3031 
3032  ashr_exprt(const exprt &_src, const std::size_t _distance):
3033  shift_exprt(_src, ID_ashr, _distance)
3034  {
3035  }
3036 };
3037 
3040 {
3041 public:
3042  DEPRECATED("use lshl_exprt(value, distance) instead")
3044  {
3045  }
3046 
3047  lshr_exprt(const exprt &_src, const exprt &_distance):
3048  shift_exprt(_src, ID_lshr, _distance)
3049  {
3050  }
3051 
3052  lshr_exprt(const exprt &_src, const std::size_t _distance):
3053  shift_exprt(_src, ID_lshr, _distance)
3054  {
3055  }
3056 };
3057 
3060 {
3061 public:
3062  DEPRECATED("use replication_exprt(times, value) instead")
3064  {
3065  }
3066 
3067  DEPRECATED("use replication_exprt(times, value) instead")
3068  explicit replication_exprt(const typet &_type):
3069  binary_exprt(ID_replication, _type)
3070  {
3071  }
3072 
3073  replication_exprt(const exprt &_times, const exprt &_src):
3074  binary_exprt(_times, ID_replication, _src)
3075  {
3076  }
3077 
3079  {
3080  return op0();
3081  }
3082 
3083  const exprt &times() const
3084  {
3085  return op0();
3086  }
3087 
3089  {
3090  return op1();
3091  }
3092 
3093  const exprt &op() const
3094  {
3095  return op1();
3096  }
3097 };
3098 
3105 inline const replication_exprt &to_replication_expr(const exprt &expr)
3106 {
3107  PRECONDITION(expr.id()==ID_replication);
3109  expr.operands().size()==2,
3110  "Bit-wise replication must have two operands");
3111  return static_cast<const replication_exprt &>(expr);
3112 }
3113 
3116 {
3117  PRECONDITION(expr.id()==ID_replication);
3119  expr.operands().size()==2,
3120  "Bit-wise replication must have two operands");
3121  return static_cast<replication_exprt &>(expr);
3122 }
3123 
3124 template<> inline bool can_cast_expr<replication_exprt>(const exprt &base)
3125 {
3126  return base.id()==ID_replication;
3127 }
3128 inline void validate_expr(const replication_exprt &value)
3129 {
3130  validate_operands(value, 2, "Bit-wise replication must have two operands");
3131 }
3132 
3133 
3136 {
3137 public:
3138  DEPRECATED("use extractbit_exprt(value, index) instead")
3140  {
3141  }
3142 
3145  const exprt &_src,
3146  const exprt &_index):binary_predicate_exprt(_src, ID_extractbit, _index)
3147  {
3148  }
3149 
3152  const exprt &_src,
3153  const std::size_t _index);
3154 
3156  {
3157  return op0();
3158  }
3159 
3161  {
3162  return op1();
3163  }
3164 
3165  const exprt &src() const
3166  {
3167  return op0();
3168  }
3169 
3170  const exprt &index() const
3171  {
3172  return op1();
3173  }
3174 };
3175 
3182 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
3183 {
3184  PRECONDITION(expr.id()==ID_extractbit);
3186  expr.operands().size()==2,
3187  "Extract bit must have two operands");
3188  return static_cast<const extractbit_exprt &>(expr);
3189 }
3190 
3193 {
3194  PRECONDITION(expr.id()==ID_extractbit);
3196  expr.operands().size()==2,
3197  "Extract bit must have two operands");
3198  return static_cast<extractbit_exprt &>(expr);
3199 }
3200 
3201 template<> inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
3202 {
3203  return base.id()==ID_extractbit;
3204 }
3205 inline void validate_expr(const extractbit_exprt &value)
3206 {
3207  validate_operands(value, 2, "Extract bit must have two operands");
3208 }
3209 
3210 
3213 {
3214 public:
3215  DEPRECATED("use extractbits_exprt(value, upper, lower) instead")
3216  extractbits_exprt():exprt(ID_extractbits)
3217  {
3218  operands().resize(3);
3219  }
3220 
3227  const exprt &_src,
3228  const exprt &_upper,
3229  const exprt &_lower,
3230  const typet &_type):exprt(ID_extractbits, _type)
3231  {
3232  add_to_operands(_src, _upper, _lower);
3233  }
3234 
3235  // NOLINTNEXTLINE(whitespace/line_length)
3238  const exprt &_src,
3239  const std::size_t _upper,
3240  const std::size_t _lower,
3241  const typet &_type);
3242 
3244  {
3245  return op0();
3246  }
3247 
3249  {
3250  return op1();
3251  }
3252 
3254  {
3255  return op2();
3256  }
3257 
3258  const exprt &src() const
3259  {
3260  return op0();
3261  }
3262 
3263  const exprt &upper() const
3264  {
3265  return op1();
3266  }
3267 
3268  const exprt &lower() const
3269  {
3270  return op2();
3271  }
3272 };
3273 
3280 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
3281 {
3282  PRECONDITION(expr.id()==ID_extractbits);
3284  expr.operands().size()==3,
3285  "Extract bits must have three operands");
3286  return static_cast<const extractbits_exprt &>(expr);
3287 }
3288 
3291 {
3292  PRECONDITION(expr.id()==ID_extractbits);
3294  expr.operands().size()==3,
3295  "Extract bits must have three operands");
3296  return static_cast<extractbits_exprt &>(expr);
3297 }
3298 
3299 template<> inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
3300 {
3301  return base.id()==ID_extractbits;
3302 }
3303 inline void validate_expr(const extractbits_exprt &value)
3304 {
3305  validate_operands(value, 3, "Extract bits must have three operands");
3306 }
3307 
3308 
3311 {
3312 public:
3313  explicit address_of_exprt(const exprt &op);
3314 
3315  address_of_exprt(const exprt &op, const pointer_typet &_type):
3316  unary_exprt(ID_address_of, op, _type)
3317  {
3318  }
3319 
3321  {
3322  return op0();
3323  }
3324 
3325  const exprt &object() const
3326  {
3327  return op0();
3328  }
3329 };
3330 
3337 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
3338 {
3339  PRECONDITION(expr.id()==ID_address_of);
3340  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
3341  return static_cast<const address_of_exprt &>(expr);
3342 }
3343 
3346 {
3347  PRECONDITION(expr.id()==ID_address_of);
3348  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
3349  return static_cast<address_of_exprt &>(expr);
3350 }
3351 
3352 template<> inline bool can_cast_expr<address_of_exprt>(const exprt &base)
3353 {
3354  return base.id()==ID_address_of;
3355 }
3356 inline void validate_expr(const address_of_exprt &value)
3357 {
3358  validate_operands(value, 1, "Address of must have one operand");
3359 }
3360 
3361 
3364 {
3365 public:
3366  explicit not_exprt(const exprt &op):
3367  unary_exprt(ID_not, op) // type from op.type()
3368  {
3369  PRECONDITION(op.type().id()==ID_bool);
3370  }
3371 
3372  DEPRECATED("use not_exprt(op) instead")
3374  {
3375  }
3376 };
3377 
3384 inline const not_exprt &to_not_expr(const exprt &expr)
3385 {
3386  PRECONDITION(expr.id()==ID_not);
3387  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
3388  return static_cast<const not_exprt &>(expr);
3389 }
3390 
3393 {
3394  PRECONDITION(expr.id()==ID_not);
3395  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
3396  return static_cast<not_exprt &>(expr);
3397 }
3398 
3399 template<> inline bool can_cast_expr<not_exprt>(const exprt &base)
3400 {
3401  return base.id()==ID_not;
3402 }
3403 
3404 inline void validate_expr(const not_exprt &value)
3405 {
3406  validate_operands(value, 1, "Not must have one operand");
3407 }
3408 
3409 
3412 {
3413 public:
3414  DEPRECATED("use dereference_exprt(pointer) instead")
3415  dereference_exprt():unary_exprt(ID_dereference)
3416  {
3417  }
3418 
3419  DEPRECATED("use dereference_exprt(pointer) instead")
3420  explicit dereference_exprt(const typet &type):
3421  unary_exprt(ID_dereference, type)
3422  {
3423  }
3424 
3425  explicit dereference_exprt(const exprt &op):
3426  unary_exprt(ID_dereference, op, op.type().subtype())
3427  {
3428  PRECONDITION(op.type().id()==ID_pointer);
3429  }
3430 
3432  unary_exprt(ID_dereference, op, type)
3433  {
3434  }
3435 
3437  {
3438  return op0();
3439  }
3440 
3441  const exprt &pointer() const
3442  {
3443  return op0();
3444  }
3445 };
3446 
3453 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
3454 {
3455  PRECONDITION(expr.id()==ID_dereference);
3457  expr.operands().size()==1,
3458  "Dereference must have one operand");
3459  return static_cast<const dereference_exprt &>(expr);
3460 }
3461 
3464 {
3465  PRECONDITION(expr.id()==ID_dereference);
3467  expr.operands().size()==1,
3468  "Dereference must have one operand");
3469  return static_cast<dereference_exprt &>(expr);
3470 }
3471 
3472 template<> inline bool can_cast_expr<dereference_exprt>(const exprt &base)
3473 {
3474  return base.id()==ID_dereference;
3475 }
3476 inline void validate_expr(const dereference_exprt &value)
3477 {
3478  validate_operands(value, 1, "Dereference must have one operand");
3479 }
3480 
3481 
3483 class if_exprt : public ternary_exprt
3484 {
3485 public:
3486  if_exprt(const exprt &cond, const exprt &t, const exprt &f)
3487  : ternary_exprt(ID_if, cond, t, f, t.type())
3488  {
3489  }
3490 
3491  if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
3492  : ternary_exprt(ID_if, cond, t, f, type)
3493  {
3494  }
3495 
3496  DEPRECATED("use if_exprt(cond, t, f) instead")
3498  {
3499  }
3500 
3502  {
3503  return op0();
3504  }
3505 
3506  const exprt &cond() const
3507  {
3508  return op0();
3509  }
3510 
3512  {
3513  return op1();
3514  }
3515 
3516  const exprt &true_case() const
3517  {
3518  return op1();
3519  }
3520 
3522  {
3523  return op2();
3524  }
3525 
3526  const exprt &false_case() const
3527  {
3528  return op2();
3529  }
3530 };
3531 
3538 inline const if_exprt &to_if_expr(const exprt &expr)
3539 {
3540  PRECONDITION(expr.id()==ID_if);
3542  expr.operands().size()==3,
3543  "If-then-else must have three operands");
3544  return static_cast<const if_exprt &>(expr);
3545 }
3546 
3548 inline if_exprt &to_if_expr(exprt &expr)
3549 {
3550  PRECONDITION(expr.id()==ID_if);
3552  expr.operands().size()==3,
3553  "If-then-else must have three operands");
3554  return static_cast<if_exprt &>(expr);
3555 }
3556 
3557 template<> inline bool can_cast_expr<if_exprt>(const exprt &base)
3558 {
3559  return base.id()==ID_if;
3560 }
3561 inline void validate_expr(const if_exprt &value)
3562 {
3563  validate_operands(value, 3, "If-then-else must have three operands");
3564 }
3565 
3569 class with_exprt:public exprt
3570 {
3571 public:
3573  const exprt &_old,
3574  const exprt &_where,
3575  const exprt &_new_value):
3576  exprt(ID_with, _old.type())
3577  {
3578  add_to_operands(_old, _where, _new_value);
3579  }
3580 
3581  DEPRECATED("use with_exprt(old, where, new_value) instead")
3582  with_exprt():exprt(ID_with)
3583  {
3584  operands().resize(3);
3585  }
3586 
3588  {
3589  return op0();
3590  }
3591 
3592  const exprt &old() const
3593  {
3594  return op0();
3595  }
3596 
3598  {
3599  return op1();
3600  }
3601 
3602  const exprt &where() const
3603  {
3604  return op1();
3605  }
3606 
3608  {
3609  return op2();
3610  }
3611 
3612  const exprt &new_value() const
3613  {
3614  return op2();
3615  }
3616 };
3617 
3624 inline const with_exprt &to_with_expr(const exprt &expr)
3625 {
3626  PRECONDITION(expr.id()==ID_with);
3628  expr.operands().size()==3,
3629  "Array/structure update must have three operands");
3630  return static_cast<const with_exprt &>(expr);
3631 }
3632 
3635 {
3636  PRECONDITION(expr.id()==ID_with);
3638  expr.operands().size()==3,
3639  "Array/structure update must have three operands");
3640  return static_cast<with_exprt &>(expr);
3641 }
3642 
3643 template<> inline bool can_cast_expr<with_exprt>(const exprt &base)
3644 {
3645  return base.id()==ID_with;
3646 }
3647 inline void validate_expr(const with_exprt &value)
3648 {
3650  value,
3651  3,
3652  "Array/structure update must have three operands");
3653 }
3654 
3655 
3657 {
3658 public:
3659  explicit index_designatort(const exprt &_index):
3660  exprt(ID_index_designator)
3661  {
3662  add_to_operands(_index);
3663  }
3664 
3665  const exprt &index() const
3666  {
3667  return op0();
3668  }
3669 
3671  {
3672  return op0();
3673  }
3674 };
3675 
3682 inline const index_designatort &to_index_designator(const exprt &expr)
3683 {
3684  PRECONDITION(expr.id()==ID_index_designator);
3686  expr.operands().size()==1,
3687  "Index designator must have one operand");
3688  return static_cast<const index_designatort &>(expr);
3689 }
3690 
3693 {
3694  PRECONDITION(expr.id()==ID_index_designator);
3696  expr.operands().size()==1,
3697  "Index designator must have one operand");
3698  return static_cast<index_designatort &>(expr);
3699 }
3700 
3701 template<> inline bool can_cast_expr<index_designatort>(const exprt &base)
3702 {
3703  return base.id()==ID_index_designator;
3704 }
3705 inline void validate_expr(const index_designatort &value)
3706 {
3707  validate_operands(value, 1, "Index designator must have one operand");
3708 }
3709 
3710 
3712 {
3713 public:
3714  explicit member_designatort(const irep_idt &_component_name):
3715  exprt(ID_member_designator)
3716  {
3717  set(ID_component_name, _component_name);
3718  }
3719 
3721  {
3722  return get(ID_component_name);
3723  }
3724 };
3725 
3733 {
3734  PRECONDITION(expr.id()==ID_member_designator);
3736  !expr.has_operands(),
3737  "Member designator must not have operands");
3738  return static_cast<const member_designatort &>(expr);
3739 }
3740 
3743 {
3744  PRECONDITION(expr.id()==ID_member_designator);
3746  !expr.has_operands(),
3747  "Member designator must not have operands");
3748  return static_cast<member_designatort &>(expr);
3749 }
3750 
3751 template<> inline bool can_cast_expr<member_designatort>(const exprt &base)
3752 {
3753  return base.id()==ID_member_designator;
3754 }
3755 inline void validate_expr(const member_designatort &value)
3756 {
3757  validate_operands(value, 0, "Member designator must not have operands");
3758 }
3759 
3760 
3763 {
3764 public:
3766  const exprt &_old,
3767  const exprt &_designator,
3768  const exprt &_new_value)
3769  : ternary_exprt(ID_update, _old, _designator, _new_value, _old.type())
3770  {
3771  }
3772 
3773  DEPRECATED("use update_exprt(old, where, new_value) instead")
3774  explicit update_exprt(const typet &_type) : ternary_exprt(ID_update, _type)
3775  {
3776  }
3777 
3778  DEPRECATED("use update_exprt(old, where, new_value) instead")
3780  {
3781  op1().id(ID_designator);
3782  }
3783 
3785  {
3786  return op0();
3787  }
3788 
3789  const exprt &old() const
3790  {
3791  return op0();
3792  }
3793 
3794  // the designator operands are either
3795  // 1) member_designator or
3796  // 2) index_designator
3797  // as defined above
3799  {
3800  return op1().operands();
3801  }
3802 
3804  {
3805  return op1().operands();
3806  }
3807 
3809  {
3810  return op2();
3811  }
3812 
3813  const exprt &new_value() const
3814  {
3815  return op2();
3816  }
3817 };
3818 
3825 inline const update_exprt &to_update_expr(const exprt &expr)
3826 {
3827  PRECONDITION(expr.id()==ID_update);
3829  expr.operands().size()==3,
3830  "Array/structure update must have three operands");
3831  return static_cast<const update_exprt &>(expr);
3832 }
3833 
3836 {
3837  PRECONDITION(expr.id()==ID_update);
3839  expr.operands().size()==3,
3840  "Array/structure update must have three operands");
3841  return static_cast<update_exprt &>(expr);
3842 }
3843 
3844 template<> inline bool can_cast_expr<update_exprt>(const exprt &base)
3845 {
3846  return base.id()==ID_update;
3847 }
3848 inline void validate_expr(const update_exprt &value)
3849 {
3851  value,
3852  3,
3853  "Array/structure update must have three operands");
3854 }
3855 
3856 
3857 #if 0
3858 class array_update_exprt:public exprt
3860 {
3861 public:
3862  array_update_exprt(
3863  const exprt &_array,
3864  const exprt &_index,
3865  const exprt &_new_value):
3866  exprt(ID_array_update, _array.type())
3867  {
3868  add_to_operands(_array, _index, _new_value);
3869  }
3870 
3871  array_update_exprt():exprt(ID_array_update)
3872  {
3873  operands().resize(3);
3874  }
3875 
3876  exprt &array()
3877  {
3878  return op0();
3879  }
3880 
3881  const exprt &array() const
3882  {
3883  return op0();
3884  }
3885 
3886  exprt &index()
3887  {
3888  return op1();
3889  }
3890 
3891  const exprt &index() const
3892  {
3893  return op1();
3894  }
3895 
3896  exprt &new_value()
3897  {
3898  return op2();
3899  }
3900 
3901  const exprt &new_value() const
3902  {
3903  return op2();
3904  }
3905 };
3906 
3913 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3914 {
3915  PRECONDITION(expr.id()==ID_array_update);
3917  expr.operands().size()==3,
3918  "Array update must have three operands");
3919  return static_cast<const array_update_exprt &>(expr);
3920 }
3921 
3923 inline array_update_exprt &to_array_update_expr(exprt &expr)
3924 {
3925  PRECONDITION(expr.id()==ID_array_update);
3927  expr.operands().size()==3,
3928  "Array update must have three operands");
3929  return static_cast<array_update_exprt &>(expr);
3930 }
3931 
3932 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
3933 {
3934  return base.id()==ID_array_update;
3935 }
3936 inline void validate_expr(const array_update_exprt &value)
3937 {
3938  validate_operands(value, 3, "Array update must have three operands");
3939 }
3940 
3941 #endif
3942 
3943 
3946 {
3947 public:
3949  const exprt &op,
3950  const irep_idt &component_name,
3951  const typet &_type):
3952  unary_exprt(ID_member, op, _type)
3953  {
3954  set_component_name(component_name);
3955  }
3956 
3958  const exprt &op,
3959  const struct_typet::componentt &c):
3960  unary_exprt(ID_member, op, c.type())
3961  {
3963  }
3964 
3965  DEPRECATED("use member_exprt(op, c) instead")
3967  {
3968  }
3969 
3971  {
3972  return get(ID_component_name);
3973  }
3974 
3975  void set_component_name(const irep_idt &component_name)
3976  {
3977  set(ID_component_name, component_name);
3978  }
3979 
3980  std::size_t get_component_number() const
3981  {
3982  return get_size_t(ID_component_number);
3983  }
3984 
3985  // will go away, use compound()
3986  const exprt &struct_op() const
3987  {
3988  return op0();
3989  }
3990 
3991  // will go away, use compound()
3993  {
3994  return op0();
3995  }
3996 
3997  const exprt &compound() const
3998  {
3999  return op0();
4000  }
4001 
4003  {
4004  return op0();
4005  }
4006 };
4007 
4014 inline const member_exprt &to_member_expr(const exprt &expr)
4015 {
4016  PRECONDITION(expr.id()==ID_member);
4018  expr.operands().size()==1,
4019  "Extract member must have one operand");
4020  return static_cast<const member_exprt &>(expr);
4021 }
4022 
4025 {
4026  PRECONDITION(expr.id()==ID_member);
4028  expr.operands().size()==1,
4029  "Extract member must have one operand");
4030  return static_cast<member_exprt &>(expr);
4031 }
4032 
4033 template<> inline bool can_cast_expr<member_exprt>(const exprt &base)
4034 {
4035  return base.id()==ID_member;
4036 }
4037 inline void validate_expr(const member_exprt &value)
4038 {
4039  validate_operands(value, 1, "Extract member must have one operand");
4040 }
4041 
4042 
4045 {
4046 public:
4047  explicit isnan_exprt(const exprt &op):
4048  unary_predicate_exprt(ID_isnan, op)
4049  {
4050  }
4051 
4052  DEPRECATED("use isnan_exprt(op) instead")
4054  {
4055  }
4056 };
4057 
4064 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
4065 {
4066  PRECONDITION(expr.id()==ID_isnan);
4067  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
4068  return static_cast<const isnan_exprt &>(expr);
4069 }
4070 
4073 {
4074  PRECONDITION(expr.id()==ID_isnan);
4075  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
4076  return static_cast<isnan_exprt &>(expr);
4077 }
4078 
4079 template<> inline bool can_cast_expr<isnan_exprt>(const exprt &base)
4080 {
4081  return base.id()==ID_isnan;
4082 }
4083 inline void validate_expr(const isnan_exprt &value)
4084 {
4085  validate_operands(value, 1, "Is NaN must have one operand");
4086 }
4087 
4088 
4091 {
4092 public:
4093  explicit isinf_exprt(const exprt &op):
4094  unary_predicate_exprt(ID_isinf, op)
4095  {
4096  }
4097 
4098  DEPRECATED("use isinf_exprt(op) instead")
4100  {
4101  }
4102 };
4103 
4110 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
4111 {
4112  PRECONDITION(expr.id()==ID_isinf);
4114  expr.operands().size()==1,
4115  "Is infinite must have one operand");
4116  return static_cast<const isinf_exprt &>(expr);
4117 }
4118 
4121 {
4122  PRECONDITION(expr.id()==ID_isinf);
4124  expr.operands().size()==1,
4125  "Is infinite must have one operand");
4126  return static_cast<isinf_exprt &>(expr);
4127 }
4128 
4129 template<> inline bool can_cast_expr<isinf_exprt>(const exprt &base)
4130 {
4131  return base.id()==ID_isinf;
4132 }
4133 inline void validate_expr(const isinf_exprt &value)
4134 {
4135  validate_operands(value, 1, "Is infinite must have one operand");
4136 }
4137 
4138 
4141 {
4142 public:
4143  explicit isfinite_exprt(const exprt &op):
4144  unary_predicate_exprt(ID_isfinite, op)
4145  {
4146  }
4147 
4148  DEPRECATED("use isfinite_exprt(op) instead")
4150  {
4151  }
4152 };
4153 
4160 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
4161 {
4162  PRECONDITION(expr.id()==ID_isfinite);
4163  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
4164  return static_cast<const isfinite_exprt &>(expr);
4165 }
4166 
4169 {
4170  PRECONDITION(expr.id()==ID_isfinite);
4171  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
4172  return static_cast<isfinite_exprt &>(expr);
4173 }
4174 
4175 template<> inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
4176 {
4177  return base.id()==ID_isfinite;
4178 }
4179 inline void validate_expr(const isfinite_exprt &value)
4180 {
4181  validate_operands(value, 1, "Is finite must have one operand");
4182 }
4183 
4184 
4187 {
4188 public:
4189  explicit isnormal_exprt(const exprt &op):
4190  unary_predicate_exprt(ID_isnormal, op)
4191  {
4192  }
4193 
4194  DEPRECATED("use isnormal_exprt(op) instead")
4196  {
4197  }
4198 };
4199 
4206 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
4207 {
4208  PRECONDITION(expr.id()==ID_isnormal);
4209  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
4210  return static_cast<const isnormal_exprt &>(expr);
4211 }
4212 
4215 {
4216  PRECONDITION(expr.id()==ID_isnormal);
4217  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
4218  return static_cast<isnormal_exprt &>(expr);
4219 }
4220 
4221 template<> inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
4222 {
4223  return base.id()==ID_isnormal;
4224 }
4225 inline void validate_expr(const isnormal_exprt &value)
4226 {
4227  validate_operands(value, 1, "Is normal must have one operand");
4228 }
4229 
4230 
4233 {
4234 public:
4235  DEPRECATED("use ieee_float_equal_exprt(lhs, rhs) instead")
4237  {
4238  }
4239 
4240  ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs):
4241  binary_relation_exprt(_lhs, ID_ieee_float_equal, _rhs)
4242  {
4243  }
4244 };
4245 
4253 {
4254  PRECONDITION(expr.id()==ID_ieee_float_equal);
4256  expr.operands().size()==2,
4257  "IEEE equality must have two operands");
4258  return static_cast<const ieee_float_equal_exprt &>(expr);
4259 }
4260 
4263 {
4264  PRECONDITION(expr.id()==ID_ieee_float_equal);
4266  expr.operands().size()==2,
4267  "IEEE equality must have two operands");
4268  return static_cast<ieee_float_equal_exprt &>(expr);
4269 }
4270 
4271 template<>
4273 {
4274  return base.id()==ID_ieee_float_equal;
4275 }
4276 inline void validate_expr(const ieee_float_equal_exprt &value)
4277 {
4278  validate_operands(value, 2, "IEEE equality must have two operands");
4279 }
4280 
4281 
4284 {
4285 public:
4286  DEPRECATED("use ieee_float_notequal_exprt(lhs, rhs) instead")
4288  binary_relation_exprt(ID_ieee_float_notequal)
4289  {
4290  }
4291 
4292  ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs):
4293  binary_relation_exprt(_lhs, ID_ieee_float_notequal, _rhs)
4294  {
4295  }
4296 };
4297 
4305  const exprt &expr)
4306 {
4307  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4309  expr.operands().size()==2,
4310  "IEEE inequality must have two operands");
4311  return static_cast<const ieee_float_notequal_exprt &>(expr);
4312 }
4313 
4316 {
4317  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4319  expr.operands().size()==2,
4320  "IEEE inequality must have two operands");
4321  return static_cast<ieee_float_notequal_exprt &>(expr);
4322 }
4323 
4324 template<>
4326 {
4327  return base.id()==ID_ieee_float_notequal;
4328 }
4329 inline void validate_expr(const ieee_float_notequal_exprt &value)
4330 {
4331  validate_operands(value, 2, "IEEE inequality must have two operands");
4332 }
4333 
4338 {
4339 public:
4341  const exprt &_lhs,
4342  const irep_idt &_id,
4343  const exprt &_rhs,
4344  const exprt &_rm)
4345  : ternary_exprt(_id, _lhs, _rhs, _rm, _lhs.type())
4346  {
4347  }
4348 
4350  {
4351  return op0();
4352  }
4353 
4354  const exprt &lhs() const
4355  {
4356  return op0();
4357  }
4358 
4360  {
4361  return op1();
4362  }
4363 
4364  const exprt &rhs() const
4365  {
4366  return op1();
4367  }
4368 
4370  {
4371  return op2();
4372  }
4373 
4374  const exprt &rounding_mode() const
4375  {
4376  return op2();
4377  }
4378 };
4379 
4387 {
4389  expr.operands().size()==3,
4390  "IEEE float operations must have three arguments");
4391  return static_cast<const ieee_float_op_exprt &>(expr);
4392 }
4393 
4396 {
4398  expr.operands().size()==3,
4399  "IEEE float operations must have three arguments");
4400  return static_cast<ieee_float_op_exprt &>(expr);
4401 }
4402 
4403 // The to_*_expr function for this type doesn't do any checks before casting,
4404 // therefore the implementation is essentially a static_cast.
4405 // Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
4406 // template<>
4407 // inline void validate_expr<ieee_float_op_exprt>(
4408 // const ieee_float_op_exprt &value)
4409 // {
4410 // validate_operands(
4411 // value,
4412 // 3,
4413 // "IEEE float operations must have three arguments");
4414 // }
4415 
4416 
4419 {
4420 public:
4421  DEPRECATED("use type_exprt(type) instead")
4423  {
4424  }
4425 
4426  explicit type_exprt(const typet &type) : nullary_exprt(ID_type, type)
4427  {
4428  }
4429 };
4430 
4432 class constant_exprt:public exprt
4433 {
4434 public:
4435  DEPRECATED("use constant_exprt(value, type) instead")
4436  constant_exprt():exprt(ID_constant)
4437  {
4438  }
4439 
4440  DEPRECATED("use constant_exprt(value, type) instead")
4441  explicit constant_exprt(const typet &type):exprt(ID_constant, type)
4442  {
4443  }
4444 
4445  constant_exprt(const irep_idt &_value, const typet &_type):
4446  exprt(ID_constant, _type)
4447  {
4448  set_value(_value);
4449  }
4450 
4451  const irep_idt &get_value() const
4452  {
4453  return get(ID_value);
4454  }
4455 
4456  void set_value(const irep_idt &value)
4457  {
4458  set(ID_value, value);
4459  }
4460 
4461  bool value_is_zero_string() const;
4462 };
4463 
4464 
4471 inline const constant_exprt &to_constant_expr(const exprt &expr)
4472 {
4473  PRECONDITION(expr.id()==ID_constant);
4474  return static_cast<const constant_exprt &>(expr);
4475 }
4476 
4479 {
4480  PRECONDITION(expr.id()==ID_constant);
4481  return static_cast<constant_exprt &>(expr);
4482 }
4483 
4484 template<> inline bool can_cast_expr<constant_exprt>(const exprt &base)
4485 {
4486  return base.id()==ID_constant;
4487 }
4488 
4489 
4492 {
4493 public:
4495  {
4496  }
4497 };
4498 
4501 {
4502 public:
4504  {
4505  }
4506 };
4507 
4509 class nil_exprt : public nullary_exprt
4510 {
4511 public:
4513  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
4514  {
4515  }
4516 };
4517 
4520 {
4521 public:
4523  : constant_exprt(ID_NULL, type)
4524  {
4525  }
4526 };
4527 
4530 {
4531 public:
4533 
4535  const symbol_exprt &_function,
4536  const argumentst &_arguments,
4537  const typet &_type)
4538  : binary_exprt(_function, ID_function_application, exprt(), _type)
4539  {
4540  arguments() = _arguments;
4541  }
4542 
4543  symbol_exprt &function()
4544  {
4545  return static_cast<symbol_exprt &>(op0());
4546  }
4547 
4548  const symbol_exprt &function() const
4549  {
4550  return static_cast<const symbol_exprt &>(op0());
4551  }
4552 
4554  {
4555  return op1().operands();
4556  }
4557 
4558  const argumentst &arguments() const
4559  {
4560  return op1().operands();
4561  }
4562 };
4563 
4571  const exprt &expr)
4572 {
4573  PRECONDITION(expr.id()==ID_function_application);
4575  expr.operands().size()==2,
4576  "Function application must have two operands");
4577  return static_cast<const function_application_exprt &>(expr);
4578 }
4579 
4582 {
4583  PRECONDITION(expr.id()==ID_function_application);
4585  expr.operands().size()==2,
4586  "Function application must have two operands");
4587  return static_cast<function_application_exprt &>(expr);
4588 }
4589 
4590 template<>
4592 {
4593  return base.id()==ID_function_application;
4594 }
4596 {
4597  validate_operands(value, 2, "Function application must have two operands");
4598 }
4599 
4606 {
4607 public:
4608  DEPRECATED("use concatenation_exprt(op, type) instead")
4609  concatenation_exprt() : multi_ary_exprt(ID_concatenation)
4610  {
4611  }
4612 
4613  DEPRECATED("use concatenation_exprt(op, type) instead")
4614  explicit concatenation_exprt(const typet &_type)
4615  : multi_ary_exprt(ID_concatenation, _type)
4616  {
4617  }
4618 
4619  concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
4620  : multi_ary_exprt(_op0, ID_concatenation, _op1, _type)
4621  {
4622  }
4623 
4624  concatenation_exprt(operandst &&_operands, const typet &_type)
4625  : multi_ary_exprt(ID_concatenation, std::move(_operands), _type)
4626  {
4627  }
4628 };
4629 
4637 {
4638  PRECONDITION(expr.id()==ID_concatenation);
4639  // DATA_INVARIANT(
4640  // expr.operands().size()>=2,
4641  // "Concatenation must have two or more operands");
4642  return static_cast<const concatenation_exprt &>(expr);
4643 }
4644 
4647 {
4648  PRECONDITION(expr.id()==ID_concatenation);
4649  // DATA_INVARIANT(
4650  // expr.operands().size()>=2,
4651  // "Concatenation must have two or more operands");
4652  return static_cast<concatenation_exprt &>(expr);
4653 }
4654 
4655 template<> inline bool can_cast_expr<concatenation_exprt>(const exprt &base)
4656 {
4657  return base.id()==ID_concatenation;
4658 }
4659 // template<>
4660 // inline void validate_expr<concatenation_exprt>(
4661 // const concatenation_exprt &value)
4662 // {
4663 // validate_operands(
4664 // value,
4665 // 2,
4666 // "Concatenation must have two or more operands",
4667 // true);
4668 // }
4669 
4670 
4673 {
4674 public:
4675  explicit infinity_exprt(const typet &_type)
4676  : nullary_exprt(ID_infinity, _type)
4677  {
4678  }
4679 };
4680 
4682 class let_exprt : public ternary_exprt
4683 {
4684 public:
4686  const symbol_exprt &symbol,
4687  const exprt &value,
4688  const exprt &where)
4689  : ternary_exprt(ID_let, symbol, value, where, where.type())
4690  {
4691  }
4692 
4694  {
4695  return static_cast<symbol_exprt &>(op0());
4696  }
4697 
4698  const symbol_exprt &symbol() const
4699  {
4700  return static_cast<const symbol_exprt &>(op0());
4701  }
4702 
4704  {
4705  return op1();
4706  }
4707 
4708  const exprt &value() const
4709  {
4710  return op1();
4711  }
4712 
4714  {
4715  return op2();
4716  }
4717 
4718  const exprt &where() const
4719  {
4720  return op2();
4721  }
4722 };
4723 
4730 inline const let_exprt &to_let_expr(const exprt &expr)
4731 {
4732  PRECONDITION(expr.id()==ID_let);
4733  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
4734  return static_cast<const let_exprt &>(expr);
4735 }
4736 
4739 {
4740  PRECONDITION(expr.id()==ID_let);
4741  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
4742  return static_cast<let_exprt &>(expr);
4743 }
4744 
4745 template<> inline bool can_cast_expr<let_exprt>(const exprt &base)
4746 {
4747  return base.id()==ID_let;
4748 }
4749 inline void validate_expr(const let_exprt &value)
4750 {
4751  validate_operands(value, 3, "Let must have three operands");
4752 }
4753 
4756 {
4757 public:
4759  const irep_idt &_id,
4760  const symbol_exprt &_symbol,
4761  const exprt &_where)
4762  : binary_predicate_exprt(_symbol, _id, _where)
4763  {
4764  }
4765 
4767  {
4768  return static_cast<symbol_exprt &>(op0());
4769  }
4770 
4771  const symbol_exprt &symbol() const
4772  {
4773  return static_cast<const symbol_exprt &>(op0());
4774  }
4775 
4777  {
4778  return op1();
4779  }
4780 
4781  const exprt &where() const
4782  {
4783  return op1();
4784  }
4785 };
4786 
4793 inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
4794 {
4795  DATA_INVARIANT(expr.operands().size()==2,
4796  "quantifier expressions must have two operands");
4798  expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
4799  return static_cast<const quantifier_exprt &>(expr);
4800 }
4801 
4804 {
4805  DATA_INVARIANT(expr.operands().size()==2,
4806  "quantifier expressions must have two operands");
4808  expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
4809  return static_cast<quantifier_exprt &>(expr);
4810 }
4811 
4812 template<> inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
4813 {
4814  return base.id() == ID_forall || base.id() == ID_exists;
4815 }
4816 
4817 inline void validate_expr(const quantifier_exprt &value)
4818 {
4819  validate_operands(value, 2,
4820  "quantifier expressions must have two operands");
4821 }
4822 
4825 {
4826 public:
4827  forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
4828  : quantifier_exprt(ID_forall, _symbol, _where)
4829  {
4830  }
4831 };
4832 
4835 {
4836 public:
4837  exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
4838  : quantifier_exprt(ID_exists, _symbol, _where)
4839  {
4840  }
4841 };
4842 
4843 inline const exists_exprt &to_exists_expr(const exprt &expr)
4844 {
4845  PRECONDITION(expr.id() == ID_exists);
4847  expr.operands().size() == 2,
4848  "exists expressions have exactly two operands");
4849  return static_cast<const exists_exprt &>(expr);
4850 }
4851 
4853 {
4854  PRECONDITION(expr.id() == ID_exists);
4856  expr.operands().size() == 2,
4857  "exists expressions have exactly two operands");
4858  return static_cast<exists_exprt &>(expr);
4859 }
4860 
4863 {
4864 public:
4865  DEPRECATED("use popcount_exprt(op, type) instead")
4866  popcount_exprt(): unary_exprt(ID_popcount)
4867  {
4868  }
4869 
4870  popcount_exprt(const exprt &_op, const typet &_type)
4871  : unary_exprt(ID_popcount, _op, _type)
4872  {
4873  }
4874 
4875  explicit popcount_exprt(const exprt &_op)
4876  : unary_exprt(ID_popcount, _op, _op.type())
4877  {
4878  }
4879 };
4880 
4887 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
4888 {
4889  PRECONDITION(expr.id() == ID_popcount);
4890  DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand");
4891  return static_cast<const popcount_exprt &>(expr);
4892 }
4893 
4896 {
4897  PRECONDITION(expr.id() == ID_popcount);
4898  DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand");
4899  return static_cast<popcount_exprt &>(expr);
4900 }
4901 
4902 template <>
4903 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
4904 {
4905  return base.id() == ID_popcount;
4906 }
4907 inline void validate_expr(const popcount_exprt &value)
4908 {
4909  validate_operands(value, 1, "popcount must have one operand");
4910 }
4911 
4916 {
4917 public:
4918  DEPRECATED("use cond_exprt(operands, type) instead")
4919  explicit cond_exprt(const typet &_type) : multi_ary_exprt(ID_cond, _type)
4920  {
4921  }
4922 
4923  cond_exprt(operandst &&_operands, const typet &_type)
4924  : multi_ary_exprt(ID_cond, std::move(_operands), _type)
4925  {
4926  }
4927 
4931  void add_case(const exprt &condition, const exprt &value)
4932  {
4933  PRECONDITION(condition.type().id() == ID_bool);
4934  operands().reserve(operands().size() + 2);
4935  operands().push_back(condition);
4936  operands().push_back(value);
4937  }
4938 };
4939 
4946 inline const cond_exprt &to_cond_expr(const exprt &expr)
4947 {
4948  PRECONDITION(expr.id() == ID_cond);
4950  expr.operands().size() % 2 == 0, "cond must have even number of operands");
4951  return static_cast<const cond_exprt &>(expr);
4952 }
4953 
4956 {
4957  PRECONDITION(expr.id() == ID_cond);
4959  expr.operands().size() % 2 != 0, "cond must have even number of operands");
4960  return static_cast<cond_exprt &>(expr);
4961 }
4962 
4963 #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:3538
bool can_cast_expr< rem_exprt >(const exprt &base)
Definition: std_expr.h:1388
const irept & get_nil_irep()
Definition: irep.cpp:55
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:183
const transt & to_trans_expr(const exprt &expr)
Cast an exprt to a transt expr must be known to be transt.
Definition: std_expr.h:124
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:4252
const irep_idt & get_name() const
Definition: std_types.h:132
bitnot_exprt(const exprt &op)
Definition: std_expr.h:2696
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:3844
bool can_cast_expr< bitxor_exprt >(const exprt &base)
Definition: std_expr.h:2829
The type of an expression, extends irept.
Definition: type.h:27
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2554
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:1021
exprt & invar()
Definition: std_expr.h:111
bool can_cast_expr< isnormal_exprt >(const exprt &base)
Definition: std_expr.h:4221
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast an exprt to a factorial_power_exprt.
Definition: std_expr.h:1469
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:526
Boolean negation.
Definition: std_expr.h:3363
unary_minus_exprt(const exprt &_op, const typet &_type)
Definition: std_expr.h:488
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: std_expr.h:611
exprt & true_case()
Definition: std_expr.h:3511
Semantic type conversion.
Definition: std_expr.h:2312
or_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:2573
const exprt & rhs() const
Definition: std_expr.h:4364
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1216
bool can_cast_expr< quantifier_exprt >(const exprt &base)
Definition: std_expr.h:4812
An expression without operands.
Definition: std_expr.h:23
bool can_cast_expr< bitnot_exprt >(const exprt &base)
Definition: std_expr.h:2725
function_application_exprt(const symbol_exprt &_function, const argumentst &_arguments, const typet &_type)
Definition: std_expr.h:4534
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:677
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:888
const exprt & value() const
Definition: std_expr.h:4708
if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
Definition: std_expr.h:3491
const exprt & lhs() const
Definition: std_expr.h:936
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
Definition: std_expr.h:2864
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1144
Application of (mathematical) function.
Definition: std_expr.h:4529
exprt & object()
Definition: std_expr.h:3320
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:299
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4827
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2360
index_exprt(const exprt &_array, const exprt &_index)
Definition: std_expr.h:1624
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1325
ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:4292
Boolean OR.
Definition: std_expr.h:2565
bool can_cast_expr< transt >(const exprt &base)
Definition: std_expr.h:143
exprt & op0()
Definition: expr.h:84
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:781
const exprt & src() const
Definition: std_expr.h:3165
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1273
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1092
let_exprt(const symbol_exprt &symbol, const exprt &value, const exprt &where)
Definition: std_expr.h:4685
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: std_expr.h:2280
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:801
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:721
Operator to update elements in structs and arrays.
Definition: std_expr.h:3762
const exprt & op() const
Definition: std_expr.h:382
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:318
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:551
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: std_expr.h:4655
const exprt & pointer() const
Definition: std_expr.h:3441
Evaluates to true if the operand is infinite.
Definition: std_expr.h:4090
const exprt & op() const
Definition: std_expr.h:3093
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1776
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:162
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3643
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
Definition: std_expr.h:2457
unsigned int get_instance() const
Definition: std_expr.cpp:43
exprt & struct_op()
Definition: std_expr.h:3992
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
Definition: std_expr.h:2810
Mathematical types.
const exprt & real() const
Definition: std_expr.h:2024
const exprt & array() const
Definition: std_expr.h:1642
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: std_expr.h:3001
bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
Definition: std_expr.h:582
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1744
const irep_idt & get_identifier() const
Definition: std_expr.h:187
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
Definition: std_expr.h:2578
exprt::operandst & designator()
Definition: std_expr.h:3798
exprt & lower()
Definition: std_expr.h:3253
shift_exprt(const irep_idt &_id)
Definition: std_expr.h:2902
const exprt & op3() const =delete
ternary_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
Definition: std_expr.h:76
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:4931
exprt imag()
Definition: std_expr.h:2029
const irep_idt & get_value() const
Definition: std_expr.h:4451
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:2210
The null pointer constant.
Definition: std_expr.h:4519
argumentst & arguments()
Definition: std_expr.h:4553
An expression denoting a type.
Definition: std_expr.h:4418
abs_exprt(const exprt &_op)
Definition: std_expr.h:438
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:3751
type_exprt(const typet &type)
Definition: std_expr.h:4426
concatenation_exprt(operandst &&_operands, const typet &_type)
Definition: std_expr.h:4624
plus_exprt(const exprt &_lhs, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:1072
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
Definition: std_expr.h:2756
const exprt & op1() const =delete
Transition system, consisting of state invariant, initial state predicate, and transition predicate...
Definition: std_expr.h:93
bool is_thread_local() const
Definition: std_expr.h:240
exprt real()
Definition: std_expr.h:2019
transt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
Definition: std_expr.h:101
The trinary if-then-else operator.
Definition: std_expr.h:3483
exprt & cond()
Definition: std_expr.h:3501
std::size_t get_component_number() const
Definition: std_expr.h:3980
const exists_exprt & to_exists_expr(const exprt &expr)
Definition: std_expr.h:4843
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:4186
exprt & old()
Definition: std_expr.h:3587
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1261
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:2137
exprt & new_value()
Definition: std_expr.h:3607
multi_ary_exprt(const irep_idt &_id, operandst &&_operands, const typet &_type)
Definition: std_expr.h:1003
typet & type()
Return the type of the expression.
Definition: expr.h:68
const symbol_exprt & symbol() const
Definition: std_expr.h:4771
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
Definition: std_expr.h:1488
bool can_cast_expr< extractbit_exprt >(const exprt &base)
Definition: std_expr.h:3201
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2610
bool can_cast_expr< bitand_exprt >(const exprt &base)
Definition: std_expr.h:2883
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:3337
const exprt & op2() const =delete
const exprt & where() const
Definition: std_expr.h:4781
The Boolean type.
Definition: std_types.h:28
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1812
const exprt & where() const
Definition: std_expr.h:3602
A constant literal expression.
Definition: std_expr.h:4432
exprt & distance()
Definition: std_expr.h:2932
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1340
exprt & rounding_mode()
Definition: std_expr.h:4369
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1255
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2508
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1249
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:228
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:3701
const exprt & index() const
Definition: std_expr.h:1652
const exprt & op3() const =delete
symbol_exprt(const typet &type)
Definition: std_expr.h:170
const exprt & lower() const
Definition: std_expr.h:3268
const exprt & where() const
Definition: std_expr.h:4718
irep_idt get_component_name() const
Definition: std_expr.h:3720
Boolean implication.
Definition: std_expr.h:2519
bool value_is_zero_string() const
Definition: std_expr.cpp:20
Exponentiation.
Definition: std_expr.h:1399
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2122
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:739
void set_bits_per_byte(std::size_t bits_per_byte)
Definition: std_expr.h:599
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:4304
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4730
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:209
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1907
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const exprt &_rm)
Definition: std_expr.h:4340
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3453
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
Definition: std_expr.h:2583
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Definition: std_expr.h:4272
Extract member of struct or union.
Definition: std_expr.h:3945
const exprt & imag() const
Definition: std_expr.h:2034
const exprt & rounding_mode() const
Definition: std_expr.h:2401
extractbits_exprt(const exprt &_src, const exprt &_upper, const exprt &_lower, const typet &_type)
Extract the bits [_lower .
Definition: std_expr.h:3226
cond_exprt(operandst &&_operands, const typet &_type)
Definition: std_expr.h:4923
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:3399
exprt & where()
Definition: std_expr.h:4713
void set_instance(unsigned int instance)
Definition: std_expr.cpp:38
Concatenation of bit-vector operands.
Definition: std_expr.h:4605
Equality.
Definition: std_expr.h:1500
symbol_exprt & symbol()
Definition: std_expr.h:4766
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1581
bool can_cast_expr< bitor_exprt >(const exprt &base)
Definition: std_expr.h:2775
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:1111
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1292
const exprt & op() const
Definition: std_expr.h:2927
Templated functions to cast to specific exprt-derived classes.
constant_exprt(const irep_idt &_value, const typet &_type)
Definition: std_expr.h:4445
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2539
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3975
bool can_cast_expr< function_application_exprt >(const exprt &base)
Definition: std_expr.h:4591
binary_predicate_exprt(const exprt &_op0, const irep_idt &_id, const exprt &_op1)
Definition: std_expr.h:859
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:4386
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:48
const exprt & compound() const
Definition: std_expr.h:3997
exprt & op()
Definition: std_expr.h:387
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:772
bswap_exprt(const exprt &_op, std::size_t bits_per_byte)
Definition: std_expr.h:588
if_exprt(const exprt &cond, const exprt &t, const exprt &f)
Definition: std_expr.h:3486
const exprt & src() const
Definition: std_expr.h:3258
const irep_idt & id() const
Definition: irep.h:256
dereference_exprt(const exprt &op, const typet &type)
Definition: std_expr.h:3431
popcount_exprt(const exprt &_op)
Definition: std_expr.h:4875
const exprt & op2() const =delete
The unary plus expression.
Definition: std_expr.h:536
void set_value(const irep_idt &value)
Definition: std_expr.h:4456
const exprt & times() const
Definition: std_expr.h:3083
Evaluates to true if the operand is NaN.
Definition: std_expr.h:4044
Bit-wise OR.
Definition: std_expr.h:2736
bool can_cast_expr< isnan_exprt >(const exprt &base)
Definition: std_expr.h:4079
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:4946
An expression denoting infinity.
Definition: std_expr.h:4672
shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance)
Definition: std_expr.h:2912
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:1163
The Boolean constant true.
Definition: std_expr.h:4491
unary_exprt(const irep_idt &_id, const exprt &_op, const typet &_type)
Definition: std_expr.h:373
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition: std_expr.h:195
Division.
Definition: std_expr.h:1227
binary_relation_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:902
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: std_expr.h:3105
A base class for binary expressions.
Definition: std_expr.h:749
const exprt & invar() const
Definition: std_expr.h:115
decorated_symbol_exprt(const irep_idt &identifier, const typet &type)
Definition: std_expr.h:219
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4636
exprt & init()
Definition: std_expr.h:112
exprt & old()
Definition: std_expr.h:3784
const exprt & distance() const
Definition: std_expr.h:2937
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3825
exprt & times()
Definition: std_expr.h:3078
const irep_idt & get_identifier() const
Definition: std_expr.h:304
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1849
The NIL expression.
Definition: std_expr.h:4509
Real part of the expression describing a complex number.
Definition: std_expr.h:2075
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:119
unary_minus_exprt(const exprt &_op)
Definition: std_expr.h:495
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:1492
IEEE floating-point disequality.
Definition: std_expr.h:4283
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:4033
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:3182
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1520
member_exprt(const exprt &op, const struct_typet::componentt &c)
Definition: std_expr.h:3957
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1862
const exprt & op3() const =delete
const exprt & op1() const =delete
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:2110
Operator to dereference a pointer.
Definition: std_expr.h:3411
operandst & operands()=delete
remove all operand methods
exprt & rounding_mode()
Definition: std_expr.h:2396
The vector type.
Definition: std_types.h:1740
const exprt & op0() const =delete
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:331
exprt & src()
Definition: std_expr.h:3243
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1725
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:2065
Union constructor from single element.
Definition: std_expr.h:1869
std::size_t get_component_number() const
Definition: std_expr.h:1902
Boolean AND.
Definition: std_expr.h:2444
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3212
factorial_power_exprt(const exprt &_base, const exprt &_exp)
Definition: std_expr.h:1455
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:838
const exprt & new_value() const
Definition: std_expr.h:3813
popcount_exprt(const exprt &_op, const typet &_type)
Definition: std_expr.h:4870
not_exprt(const exprt &op)
Definition: std_expr.h:3366
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: std_expr.h:4110
exprt & op1()
Definition: expr.h:87
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: std_expr.h:4570
const exprt & lhs() const
Definition: std_expr.h:4354
and_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:2452
Generic base class for unary expressions.
Definition: std_expr.h:342
Disequality.
Definition: std_expr.h:1561
exprt::operandst argumentst
Definition: std_expr.h:4532
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:1012
infinity_exprt(const typet &_type)
Definition: std_expr.h:4675
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:2231
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:569
An expression with three operands.
Definition: std_expr.h:59
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1938
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:3280
Left shift.
Definition: std_expr.h:2976
const exprt & what() const
Definition: std_expr.h:1713
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:958
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:357
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const exprt & false_case() const
Definition: std_expr.h:3526
typecast_exprt(const typet &_type)
Definition: std_expr.h:2316
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:4014
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: std_expr.h:3299
lshr_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:3052
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2171
const exprt & cond() const
Definition: std_expr.h:3506
A forall expression.
Definition: std_expr.h:4824
with_exprt(const exprt &_old, const exprt &_where, const exprt &_new_value)
Definition: std_expr.h:3572
The plus expression Associativity is not specified.
Definition: std_expr.h:1052
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:4484
symbol_exprt(const irep_idt &identifier, const typet &type)
Definition: std_expr.h:176
const symbol_exprt & symbol() const
Definition: std_expr.h:4698
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
Definition: std_expr.h:2433
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:262
null_pointer_exprt(const pointer_typet &type)
Definition: std_expr.h:4522
ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:4240
exprt & where()
Definition: std_expr.h:4776
void set_static_lifetime()
Definition: std_expr.h:230
Array constructor from single element.
Definition: std_expr.h:1694
exprt & upper()
Definition: std_expr.h:3248
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: std_expr.h:4793
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2673
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:26
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1513
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:469
power_exprt(const exprt &_base, const exprt &_exp)
Definition: std_expr.h:1407
isfinite_exprt(const exprt &op)
Definition: std_expr.h:4143
Logical right shift.
Definition: std_expr.h:3039
exprt & compound()
Definition: std_expr.h:4002
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:3682
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:2157
Vector constructor from list of elements.
Definition: std_expr.h:1823
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const exprt & old() const
Definition: std_expr.h:3592
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: std_expr.h:4160
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:2629
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: std_expr.h:3472
Operator to return the address of an object.
Definition: std_expr.h:3310
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1977
The unary minus expression.
Definition: std_expr.h:480
exprt & false_case()
Definition: std_expr.h:3521
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: std_expr.h:2300
concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
Definition: std_expr.h:4619
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4471
implies_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:2527
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:652
union_exprt(const irep_idt &_component_name, const exprt &_value, const typet &_type)
Definition: std_expr.h:1883
member_exprt(const exprt &op, const irep_idt &component_name, const typet &_type)
Definition: std_expr.h:3948
quantifier_exprt(const irep_idt &_id, const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4758
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
const exprt & index() const
Definition: std_expr.h:3665
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:3352
The Boolean constant false.
Definition: std_expr.h:4500
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:866
const exprt & init() const
Definition: std_expr.h:116
bool can_cast_expr< replication_exprt >(const exprt &base)
Definition: std_expr.h:3124
exprt & index()
Definition: std_expr.h:3160
const exprt & rhs() const
Definition: std_expr.h:946
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2413
exprt & trans()
Definition: std_expr.h:113
equal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1508
void validate_expr(const transt &value)
Definition: std_expr.h:147
struct_exprt(operandst &&_operands, const typet &_type)
Definition: std_expr.h:1962
const exprt & trans() const
Definition: std_expr.h:117
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2326
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2660
std::vector< exprt > operandst
Definition: expr.h:57
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1175
const exprt::operandst & designator() const
Definition: std_expr.h:3803
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: std_expr.h:4325
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1600
#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:1197
or_exprt(exprt::operandst &&_operands)
Definition: std_expr.h:2592
const exprt & object() const
Definition: std_expr.h:2186
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
Definition: std_expr.h:1421
minus_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1130
Boolean XOR.
Definition: std_expr.h:2640
index_designatort(const exprt &_index)
Definition: std_expr.h:3659
Complex numbers made of pair of given subtype.
Definition: std_types.h:1792
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4887
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3624
Bit-wise XOR.
Definition: std_expr.h:2790
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:1038
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1535
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:277
dynamic_object_exprt(const typet &type)
Definition: std_expr.h:2250
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:2125
Pre-defined types.
const exprt & op3() const =delete
array_list_exprt(operandst &&_operands, const array_typet &_type)
Definition: std_expr.h:1805
typecast_exprt(const exprt &op, const typet &_type)
Definition: std_expr.h:2320
const exprt & old() const
Definition: std_expr.h:3789
const exprt & object() const
Definition: std_expr.h:3325
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: std_expr.h:4064
plus_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1065
update_exprt(const exprt &_old, const exprt &_designator, const exprt &_new_value)
Definition: std_expr.h:3765
exprt & value()
Definition: std_expr.h:4703
Expression to hold a nondeterministic choice.
Definition: std_expr.h:288
bitand_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2852
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2949
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2489
exprt & index()
Definition: std_expr.h:1647
shl_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2984
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4862
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
Definition: std_expr.h:1373
Evaluates to true if the operand is finite.
Definition: std_expr.h:4140
const exprt & index() const
Definition: std_expr.h:3170
ashr_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:3027
exprt & op()
Definition: std_expr.h:2922
std::size_t get_bits_per_byte() const
Definition: std_expr.h:594
xor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2648
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2371
div_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1235
shl_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2989
Base class for all expressions.
Definition: expr.h:54
exprt & pointer()
Definition: std_expr.h:3436
Absolute value.
Definition: std_expr.h:430
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:701
const exprt & root_object() const
Definition: std_expr.cpp:195
floatbv_typecast_exprt(const exprt &op, const exprt &rounding, const typet &_type)
Definition: std_expr.h:2379
const exprt & struct_op() const
Definition: std_expr.h:3986
const exprt & rounding_mode() const
Definition: std_expr.h:4374
isnormal_exprt(const exprt &op)
Definition: std_expr.h:4189
nondet_symbol_exprt(const irep_idt &identifier, const typet &type)
Definition: std_expr.h:293
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:975
dereference_exprt(const exprt &op)
Definition: std_expr.h:3425
and_exprt(exprt::operandst &&_operands)
Definition: std_expr.h:2471
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:2046
complex_real_exprt(const exprt &op)
Definition: std_expr.h:2078
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1919
vector_exprt(operandst &&_operands, const vector_typet &_type)
Definition: std_expr.h:1837
const exprt & op2() const =delete
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast an exprt to a factorial_power_exprt.
Definition: std_expr.h:1479
Operator to update elements in structs and arrays.
Definition: std_expr.h:3569
const exprt & upper() const
Definition: std_expr.h:3263
sign_exprt(const exprt &_op)
Definition: std_expr.h:709
A base class for quantifier expressions.
Definition: std_expr.h:4755
lshr_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:3047
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:910
unary_predicate_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:691
irep_idt get_component_name() const
Definition: std_expr.h:3970
const exprt & offset() const
Definition: std_expr.h:2198
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2341
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:4745
rem_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1359
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3384
Remainder of division.
Definition: std_expr.h:1351
const exprt & valid() const
Definition: std_expr.h:2268
bitor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2744
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1823
const exprt & true_case() const
Definition: std_expr.h:3516
exprt & index()
Definition: std_expr.h:3670
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:182
#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:3088
irep_idt get_component_name() const
Definition: std_expr.h:1892
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:423
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1897
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:450
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
Definition: std_expr.h:2462
bool is_static_lifetime() const
Definition: std_expr.h:225
isinf_exprt(const exprt &op)
Definition: std_expr.h:4093
Arrays with given size.
Definition: std_types.h:1024
bool can_cast_expr< bswap_exprt >(const exprt &base)
Definition: std_expr.h:631
Binary minus.
Definition: std_expr.h:1122
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:791
Bit-wise AND.
Definition: std_expr.h:2844
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4837
validation_modet
isnan_exprt(const exprt &op)
Definition: std_expr.h:4047
Expression to hold a symbol (variable)
Definition: std_expr.h:154
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: std_expr.h:4129
exprt & what()
Definition: std_expr.h:1708
exprt & op2()
Definition: expr.h:90
bool can_cast_expr< power_exprt >(const exprt &base)
Definition: std_expr.h:1436
ashr_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:3032
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:873
bool can_cast_expr< isfinite_exprt >(const exprt &base)
Definition: std_expr.h:4175
exprt & new_value()
Definition: std_expr.h:3808
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1990
replication_exprt(const exprt &_times, const exprt &_src)
Definition: std_expr.h:3073
symbol_exprt & symbol()
Definition: std_expr.h:4693
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:821
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:845
plus_exprt(operandst &&_operands, const typet &_type)
Definition: std_expr.h:1080
Arithmetic right shift.
Definition: std_expr.h:3019
An exists expression.
Definition: std_expr.h:4834
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1683
exprt & where()
Definition: std_expr.h:3597
Base Type Computation.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: std_expr.h:2708
A let expression.
Definition: std_expr.h:4682
void clear_static_lifetime()
Definition: std_expr.h:235
#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:485
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1243
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: std_expr.h:4206
Representation of heap-allocated objects.
Definition: std_expr.h:2242
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:316
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:983
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:406
operandst & operands()
Definition: expr.h:78
mult_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1183
mod_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1311
void copy_to_operands(const exprt &expr)=delete
exprt & src()
Definition: std_expr.h:3155
bitxor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2798
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2688
index_exprt(const exprt &_array, const exprt &_index, const typet &_type)
Definition: std_expr.h:1629
Struct constructor from list of elements.
Definition: std_expr.h:1949
unary_plus_exprt(const exprt &op)
Definition: std_expr.h:539
extractbit_exprt(const exprt &_src, const exprt &_index)
Extract the _index-th least significant bit from _src.
Definition: std_expr.h:3144
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:3557
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:243
Falling factorial power.
Definition: std_expr.h:1447
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:2090
notequal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1569
complex_exprt(const exprt &_real, const exprt &_imag, const complex_typet &_type)
Definition: std_expr.h:2011
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:4337
Bit-vector replication.
Definition: std_expr.h:3059
exprt & array()
Definition: std_expr.h:1637
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:1664
A base class for shift operators.
Definition: std_expr.h:2898
const argumentst & arguments() const
Definition: std_expr.h:4558
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt&#39;s operands.
Definition: expr.h:130
Array constructor from list of elements.
Definition: std_expr.h:1755
nullary_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:32
Complex constructor from a pair of numbers.
Definition: std_expr.h:1997
Modulo.
Definition: std_expr.h:1303
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1789
The byte swap expression.
Definition: std_expr.h:579
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:507
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:3714
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: std_expr.h:4903
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:917
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
Definition: std_expr.h:1796
array_of_exprt(const exprt &_what, const array_typet &_type)
Definition: std_expr.h:1702
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:3732
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:4915
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:3135
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:644
IEEE-floating-point equality.
Definition: std_expr.h:4232
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1550
Array index operator.
Definition: std_expr.h:1611
exprt & op3()
Definition: expr.h:93
address_of_exprt(const exprt &op, const pointer_typet &_type)
Definition: std_expr.h:3315
const exprt & new_value() const
Definition: std_expr.h:3612
const exprt & op() const
Definition: std_expr.h:2391