cprover
std_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_STD_EXPR_H
11 #define CPROVER_UTIL_STD_EXPR_H
12 
15 
16 #include "as_const.h"
17 #include "expr_cast.h"
18 #include "invariant.h"
19 #include "narrow.h"
20 #include "std_types.h"
21 
24 {
25 public:
26  // constructors
27  DEPRECATED(SINCE(2018, 9, 21, "use nullary_exprt(id, type) instead"))
28  explicit nullary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet())
29  {
30  }
31 
32  nullary_exprt(const irep_idt &_id, typet _type)
33  : expr_protectedt(_id, std::move(_type))
34  {
35  }
36 
38  operandst &operands() = delete;
39  const operandst &operands() const = delete;
40 
41  const exprt &op0() const = delete;
42  exprt &op0() = delete;
43  const exprt &op1() const = delete;
44  exprt &op1() = delete;
45  const exprt &op2() const = delete;
46  exprt &op2() = delete;
47  const exprt &op3() const = delete;
48  exprt &op3() = delete;
49 
50  void move_to_operands(exprt &) = delete;
51  void move_to_operands(exprt &, exprt &) = delete;
52  void move_to_operands(exprt &, exprt &, exprt &) = delete;
53 
54  void copy_to_operands(const exprt &expr) = delete;
55  void copy_to_operands(const exprt &, const exprt &) = delete;
56  void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
57 };
58 
61 {
62 public:
63  // constructors
64  DEPRECATED(
65  SINCE(2018, 9, 21, "use ternary_exprt(id, op0, op1, op2, type) instead"))
66  explicit ternary_exprt(const irep_idt &_id) : expr_protectedt(_id, type())
67  {
68  operands().resize(3);
69  }
70 
71  DEPRECATED(
72  SINCE(2018, 9, 21, "use ternary_exprt(id, op0, op1, op2, type) instead"))
73  explicit ternary_exprt(const irep_idt &_id, const typet &_type)
74  : expr_protectedt(_id, _type)
75  {
76  operands().resize(3);
77  }
78 
80  const irep_idt &_id,
81  exprt _op0,
82  exprt _op1,
83  exprt _op2,
84  typet _type)
86  _id,
87  std::move(_type),
88  {std::move(_op0), std::move(_op1), std::move(_op2)})
89  {
90  }
91 
92  // make op0 to op2 public
93  using exprt::op0;
94  using exprt::op1;
95  using exprt::op2;
96 
97  const exprt &op3() const = delete;
98  exprt &op3() = delete;
99 };
100 
103 {
104 public:
105  DEPRECATED(SINCE(2018, 9, 21, "use symbol_exprt(identifier, type) instead"))
107  {
108  }
109 
111  DEPRECATED(SINCE(2018, 9, 21, "use symbol_exprt(identifier, type) instead"))
112  explicit symbol_exprt(const irep_idt &identifier) : nullary_exprt(ID_symbol)
113  {
114  set_identifier(identifier);
115  }
116 
118  explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type))
119  {
120  }
121 
124  symbol_exprt(const irep_idt &identifier, typet type)
125  : nullary_exprt(ID_symbol, std::move(type))
126  {
127  set_identifier(identifier);
128  }
129 
134  static symbol_exprt typeless(const irep_idt &id)
135  {
136  return symbol_exprt(id, typet());
137  }
138 
139  void set_identifier(const irep_idt &identifier)
140  {
141  set(ID_identifier, identifier);
142  }
143 
144  const irep_idt &get_identifier() const
145  {
146  return get(ID_identifier);
147  }
148 };
149 
153 {
154 public:
155  DEPRECATED(
156  SINCE(2018, 9, 21, "use decorated_symbol_exprt(identifier, type) instead"))
158  {
159  }
160 
162  DEPRECATED(
163  SINCE(2018, 9, 21, "use decorated_symbol_exprt(identifier, type) instead"))
164  explicit decorated_symbol_exprt(const irep_idt &identifier):
165  symbol_exprt(identifier)
166  {
167  }
168 
170  DEPRECATED(
171  SINCE(2018, 9, 21, "use decorated_symbol_exprt(identifier, type) instead"))
174  {
175  }
176 
180  : symbol_exprt(identifier, std::move(type))
181  {
182  }
183 
184  bool is_static_lifetime() const
185  {
186  return get_bool(ID_C_static_lifetime);
187  }
188 
190  {
191  return set(ID_C_static_lifetime, true);
192  }
193 
195  {
196  remove(ID_C_static_lifetime);
197  }
198 
199  bool is_thread_local() const
200  {
201  return get_bool(ID_C_thread_local);
202  }
203 
205  {
206  return set(ID_C_thread_local, true);
207  }
208 
210  {
211  remove(ID_C_thread_local);
212  }
213 };
214 
215 template <>
216 inline bool can_cast_expr<symbol_exprt>(const exprt &base)
217 {
218  return base.id() == ID_symbol;
219 }
220 
221 inline void validate_expr(const symbol_exprt &value)
222 {
223  validate_operands(value, 0, "Symbols must not have operands");
224 }
225 
232 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
233 {
234  PRECONDITION(expr.id()==ID_symbol);
235  const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
236  validate_expr(ret);
237  return ret;
238 }
239 
242 {
243  PRECONDITION(expr.id()==ID_symbol);
244  symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
245  validate_expr(ret);
246  return ret;
247 }
248 
249 
252 {
253 public:
257  : nullary_exprt(ID_nondet_symbol, std::move(type))
258  {
259  set_identifier(identifier);
260  }
261 
262  void set_identifier(const irep_idt &identifier)
263  {
264  set(ID_identifier, identifier);
265  }
266 
267  const irep_idt &get_identifier() const
268  {
269  return get(ID_identifier);
270  }
271 };
272 
273 template <>
275 {
276  return base.id() == ID_nondet_symbol;
277 }
278 
279 inline void validate_expr(const nondet_symbol_exprt &value)
280 {
281  validate_operands(value, 0, "Symbols must not have operands");
282 }
283 
291 {
292  PRECONDITION(expr.id()==ID_nondet_symbol);
293  const nondet_symbol_exprt &ret =
294  static_cast<const nondet_symbol_exprt &>(expr);
295  validate_expr(ret);
296  return ret;
297 }
298 
301 {
302  PRECONDITION(expr.id()==ID_symbol);
303  nondet_symbol_exprt &ret = static_cast<nondet_symbol_exprt &>(expr);
304  validate_expr(ret);
305  return ret;
306 }
307 
308 
311 {
312 public:
313  DEPRECATED(SINCE(2018, 9, 21, "use unary_exprt(id, op) instead"))
315  {
316  operands().resize(1);
317  }
318 
319  DEPRECATED(SINCE(2018, 9, 21, "use unary_exprt(id, op) instead"))
320  explicit unary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet())
321  {
322  operands().resize(1);
323  }
324 
325  unary_exprt(const irep_idt &_id, const exprt &_op)
326  : expr_protectedt(_id, _op.type(), {_op})
327  {
328  }
329 
330  DEPRECATED(SINCE(2018, 12, 2, "use unary_exprt(id, op, type) instead"))
331  unary_exprt(const irep_idt &_id, const typet &_type)
332  : expr_protectedt(_id, _type)
333  {
334  operands().resize(1);
335  }
336 
337  unary_exprt(const irep_idt &_id, exprt _op, typet _type)
338  : expr_protectedt(_id, std::move(_type), {std::move(_op)})
339  {
340  }
341 
342  const exprt &op() const
343  {
344  return op0();
345  }
346 
348  {
349  return op0();
350  }
351 
352  const exprt &op1() const = delete;
353  exprt &op1() = delete;
354  const exprt &op2() const = delete;
355  exprt &op2() = delete;
356  const exprt &op3() const = delete;
357  exprt &op3() = delete;
358 };
359 
360 template <>
361 inline bool can_cast_expr<unary_exprt>(const exprt &base)
362 {
363  return base.operands().size() == 1;
364 }
365 
366 inline void validate_expr(const unary_exprt &value)
367 {
368  validate_operands(value, 1, "Unary expressions must have one operand");
369 }
370 
377 inline const unary_exprt &to_unary_expr(const exprt &expr)
378 {
379  const unary_exprt &ret = static_cast<const unary_exprt &>(expr);
380  validate_expr(ret);
381  return ret;
382 }
383 
386 {
387  unary_exprt &ret = static_cast<unary_exprt &>(expr);
388  validate_expr(ret);
389  return ret;
390 }
391 
392 
394 class abs_exprt:public unary_exprt
395 {
396 public:
397  DEPRECATED(SINCE(2018, 9, 21, "use abs_exprt(op) instead"))
399  {
400  }
401 
402  explicit abs_exprt(exprt _op) : unary_exprt(ID_abs, std::move(_op))
403  {
404  }
405 };
406 
407 template <>
408 inline bool can_cast_expr<abs_exprt>(const exprt &base)
409 {
410  return base.id() == ID_abs;
411 }
412 
413 inline void validate_expr(const abs_exprt &value)
414 {
415  validate_operands(value, 1, "Absolute value must have one operand");
416 }
417 
424 inline const abs_exprt &to_abs_expr(const exprt &expr)
425 {
426  PRECONDITION(expr.id()==ID_abs);
427  const abs_exprt &ret = static_cast<const abs_exprt &>(expr);
428  validate_expr(ret);
429  return ret;
430 }
431 
434 {
435  PRECONDITION(expr.id()==ID_abs);
436  abs_exprt &ret = static_cast<abs_exprt &>(expr);
437  validate_expr(ret);
438  return ret;
439 }
440 
441 
444 {
445 public:
446  DEPRECATED(SINCE(2018, 9, 21, "use unary_minus_exprt(op) instead"))
447  unary_minus_exprt():unary_exprt(ID_unary_minus)
448  {
449  }
450 
452  : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
453  {
454  }
455 
456  explicit unary_minus_exprt(exprt _op)
457  : unary_exprt(ID_unary_minus, std::move(_op))
458  {
459  }
460 };
461 
462 template <>
463 inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
464 {
465  return base.id() == ID_unary_minus;
466 }
467 
468 inline void validate_expr(const unary_minus_exprt &value)
469 {
470  validate_operands(value, 1, "Unary minus must have one operand");
471 }
472 
479 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
480 {
481  PRECONDITION(expr.id()==ID_unary_minus);
482  const unary_minus_exprt &ret = static_cast<const unary_minus_exprt &>(expr);
483  validate_expr(ret);
484  return ret;
485 }
486 
489 {
490  PRECONDITION(expr.id()==ID_unary_minus);
491  unary_minus_exprt &ret = static_cast<unary_minus_exprt &>(expr);
492  validate_expr(ret);
493  return ret;
494 }
495 
498 {
499 public:
501  : unary_exprt(ID_unary_plus, std::move(op))
502  {
503  }
504 };
505 
506 template <>
507 inline bool can_cast_expr<unary_plus_exprt>(const exprt &base)
508 {
509  return base.id() == ID_unary_plus;
510 }
511 
512 inline void validate_expr(const unary_plus_exprt &value)
513 {
514  validate_operands(value, 1, "unary plus must have one operand");
515 }
516 
523 inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
524 {
525  PRECONDITION(expr.id() == ID_unary_plus);
526  const unary_plus_exprt &ret = static_cast<const unary_plus_exprt &>(expr);
527  validate_expr(ret);
528  return ret;
529 }
530 
533 {
534  PRECONDITION(expr.id() == ID_unary_plus);
535  unary_plus_exprt &ret = static_cast<unary_plus_exprt &>(expr);
536  validate_expr(ret);
537  return ret;
538 }
539 
542 {
543 public:
544  bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
545  : unary_exprt(ID_bswap, std::move(_op), std::move(_type))
546  {
547  set_bits_per_byte(bits_per_byte);
548  }
549 
550  bswap_exprt(exprt _op, std::size_t bits_per_byte)
551  : unary_exprt(ID_bswap, std::move(_op))
552  {
553  set_bits_per_byte(bits_per_byte);
554  }
555 
556  std::size_t get_bits_per_byte() const
557  {
558  return get_size_t(ID_bits_per_byte);
559  }
560 
561  void set_bits_per_byte(std::size_t bits_per_byte)
562  {
563  set(ID_bits_per_byte, narrow_cast<long long>(bits_per_byte));
564  }
565 };
566 
567 template <>
568 inline bool can_cast_expr<bswap_exprt>(const exprt &base)
569 {
570  return base.id() == ID_bswap;
571 }
572 
573 inline void validate_expr(const bswap_exprt &value)
574 {
575  validate_operands(value, 1, "bswap must have one operand");
577  value.op().type() == value.type(), "bswap type must match operand type");
578 }
579 
586 inline const bswap_exprt &to_bswap_expr(const exprt &expr)
587 {
588  PRECONDITION(expr.id() == ID_bswap);
589  const bswap_exprt &ret = static_cast<const bswap_exprt &>(expr);
590  validate_expr(ret);
591  return ret;
592 }
593 
596 {
597  PRECONDITION(expr.id() == ID_bswap);
598  bswap_exprt &ret = static_cast<bswap_exprt &>(expr);
599  validate_expr(ret);
600  return ret;
601 }
602 
606 {
607 public:
608  DEPRECATED(SINCE(2018, 12, 2, "use predicate_exprt(id) instead"))
610  {
611  }
612 
613  explicit predicate_exprt(const irep_idt &_id)
614  : expr_protectedt(_id, bool_typet())
615  {
616  }
617 
618  DEPRECATED(SINCE(2018, 12, 2, "use unary_predicate_exprt(id, op) instead"))
619  predicate_exprt(const irep_idt &_id, const exprt &_op)
620  : expr_protectedt(_id, bool_typet())
621  {
622  add_to_operands(_op);
623  }
624 
625  DEPRECATED(
626  SINCE(2018, 12, 2, "use binary_predicate_exprt(op1, id, op2) instead"))
627  predicate_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1)
628  : expr_protectedt(_id, bool_typet())
629  {
630  add_to_operands(_op0, _op1);
631  }
632 };
633 
637 {
638 public:
639  DEPRECATED(SINCE(2018, 12, 2, "use unary_predicate_exprt(id, op) instead"))
641  {
642  }
643 
644  DEPRECATED(SINCE(2018, 12, 2, "use unary_predicate_exprt(id, op) instead"))
645  explicit unary_predicate_exprt(const irep_idt &_id):
646  unary_exprt(_id, bool_typet())
647  {
648  }
649 
651  : unary_exprt(_id, std::move(_op), bool_typet())
652  {
653  }
654 };
655 
659 {
660 public:
661  DEPRECATED(SINCE(2018, 12, 2, "use sign_exprt(op) instead"))
663  {
664  }
665 
666  explicit sign_exprt(exprt _op)
667  : unary_predicate_exprt(ID_sign, std::move(_op))
668  {
669  }
670 };
671 
672 template <>
673 inline bool can_cast_expr<sign_exprt>(const exprt &base)
674 {
675  return base.id() == ID_sign;
676 }
677 
678 inline void validate_expr(const sign_exprt &expr)
679 {
680  validate_operands(expr, 1, "sign expression must have one operand");
681 }
682 
689 inline const sign_exprt &to_sign_expr(const exprt &expr)
690 {
691  PRECONDITION(expr.id() == ID_sign);
692  const sign_exprt &ret = static_cast<const sign_exprt &>(expr);
693  validate_expr(ret);
694  return ret;
695 }
696 
699 {
700  PRECONDITION(expr.id() == ID_sign);
701  sign_exprt &ret = static_cast<sign_exprt &>(expr);
702  validate_expr(ret);
703  return ret;
704 }
705 
708 {
709 public:
710  DEPRECATED(SINCE(2018, 9, 21, "use binary_exprt(lhs, id, rhs) instead"))
712  {
713  operands().resize(2);
714  }
715 
716  DEPRECATED(SINCE(2018, 9, 21, "use binary_exprt(lhs, id, rhs) instead"))
717  explicit binary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet())
718  {
719  operands().resize(2);
720  }
721 
722  DEPRECATED(SINCE(2018, 12, 2, "use binary_exprt(lhs, id, rhs, type) instead"))
723  binary_exprt(const irep_idt &_id, const typet &_type)
724  : expr_protectedt(_id, _type)
725  {
726  operands().resize(2);
727  }
728 
729  binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
730  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
731  {
732  }
733 
734  binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
735  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
736  {
737  }
738 
739  static void check(
740  const exprt &expr,
742  {
743  DATA_CHECK(
744  vm,
745  expr.operands().size() == 2,
746  "binary expression must have two operands");
747  }
748 
749  static void validate(
750  const exprt &expr,
751  const namespacet &,
753  {
754  check(expr, vm);
755  }
756 
757  // make op0 and op1 public
758  using exprt::op0;
759  using exprt::op1;
760 
761  const exprt &op2() const = delete;
762  exprt &op2() = delete;
763  const exprt &op3() const = delete;
764  exprt &op3() = delete;
765 };
766 
767 template <>
768 inline bool can_cast_expr<binary_exprt>(const exprt &base)
769 {
770  return base.operands().size() == 2;
771 }
772 
773 inline void validate_expr(const binary_exprt &value)
774 {
775  binary_exprt::check(value);
776 }
777 
784 inline const binary_exprt &to_binary_expr(const exprt &expr)
785 {
786  binary_exprt::check(expr);
787  return static_cast<const binary_exprt &>(expr);
788 }
789 
792 {
793  binary_exprt::check(expr);
794  return static_cast<binary_exprt &>(expr);
795 }
796 
800 {
801 public:
802  DEPRECATED(
803  SINCE(2018, 12, 2, "use binary_predicate_exprt(lhs, id, rhs) instead"))
805  {
806  }
807 
808  DEPRECATED(
809  SINCE(2018, 12, 2, "use binary_predicate_exprt(lhs, id, rhs) instead"))
810  explicit binary_predicate_exprt(const irep_idt &_id):
811  binary_exprt(_id, bool_typet())
812  {
813  }
814 
815  binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
816  : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
817  {
818  }
819 
820  static void check(
821  const exprt &expr,
823  {
824  binary_exprt::check(expr, vm);
825  }
826 
827  static void validate(
828  const exprt &expr,
829  const namespacet &ns,
831  {
832  binary_exprt::validate(expr, ns, vm);
833 
834  DATA_CHECK(
835  vm,
836  expr.type().id() == ID_bool,
837  "result of binary predicate expression should be of type bool");
838  }
839 };
840 
843 {
844 public:
845  DEPRECATED(
846  SINCE(2018, 12, 2, "use binary_relation_exprt(lhs, id, rhs) instead"))
848  {
849  }
850 
851  DEPRECATED(
852  SINCE(2018, 12, 2, "use binary_relation_exprt(lhs, id, rhs) instead"))
853  explicit binary_relation_exprt(const irep_idt &id):
855  {
856  }
857 
858  binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
859  : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
860  {
861  }
862 
863  static void check(
864  const exprt &expr,
866  {
868  }
869 
870  static void validate(
871  const exprt &expr,
872  const namespacet &ns,
874  {
875  binary_predicate_exprt::validate(expr, ns, vm);
876 
877  // check types
878  DATA_CHECK(
879  vm,
880  expr.op0().type() == expr.op1().type(),
881  "lhs and rhs of binary relation expression should have same type");
882  }
883 
885  {
886  return op0();
887  }
888 
889  const exprt &lhs() const
890  {
891  return op0();
892  }
893 
895  {
896  return op1();
897  }
898 
899  const exprt &rhs() const
900  {
901  return op1();
902  }
903 };
904 
905 template <>
907 {
908  return can_cast_expr<binary_exprt>(base);
909 }
910 
911 inline void validate_expr(const binary_relation_exprt &value)
912 {
914 }
915 
923 {
925  return static_cast<const binary_relation_exprt &>(expr);
926 }
927 
930 {
932  return static_cast<binary_relation_exprt &>(expr);
933 }
934 
935 
939 {
940 public:
941  DEPRECATED(SINCE(2018, 9, 21, "use multi_ary_exprt(id, op, type) instead"))
943  {
944  }
945 
946  DEPRECATED(SINCE(2018, 9, 21, "use multi_ary_exprt(id, op, type) instead"))
947  explicit multi_ary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet())
948  {
949  }
950 
951  DEPRECATED(SINCE(2018, 12, 7, "use multi_ary_exprt(id, op, type) instead"))
952  multi_ary_exprt(const irep_idt &_id, const typet &_type)
953  : expr_protectedt(_id, _type)
954  {
955  }
956 
957  multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
958  : expr_protectedt(_id, std::move(_type))
959  {
960  operands() = std::move(_operands);
961  }
962 
963  multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
964  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
965  {
966  }
967 
968  multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
969  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
970  {
971  }
972 
973  // In contrast to exprt::opX, the methods
974  // below check the size.
976  {
977  PRECONDITION(operands().size() >= 1);
978  return operands().front();
979  }
980 
982  {
983  PRECONDITION(operands().size() >= 2);
984  return operands()[1];
985  }
986 
988  {
989  PRECONDITION(operands().size() >= 3);
990  return operands()[2];
991  }
992 
994  {
995  PRECONDITION(operands().size() >= 4);
996  return operands()[3];
997  }
998 
999  const exprt &op0() const
1000  {
1001  PRECONDITION(operands().size() >= 1);
1002  return operands().front();
1003  }
1004 
1005  const exprt &op1() const
1006  {
1007  PRECONDITION(operands().size() >= 2);
1008  return operands()[1];
1009  }
1010 
1011  const exprt &op2() const
1012  {
1013  PRECONDITION(operands().size() >= 3);
1014  return operands()[2];
1015  }
1016 
1017  const exprt &op3() const
1018  {
1019  PRECONDITION(operands().size() >= 4);
1020  return operands()[3];
1021  }
1022 };
1023 
1030 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
1031 {
1032  return static_cast<const multi_ary_exprt &>(expr);
1033 }
1034 
1037 {
1038  return static_cast<multi_ary_exprt &>(expr);
1039 }
1040 
1041 
1045 {
1046 public:
1047  DEPRECATED(SINCE(2018, 9, 21, "use plus_exprt(lhs, rhs) instead"))
1049  {
1050  }
1051 
1052  DEPRECATED(SINCE(2019, 1, 12, "use plus_exprt(lhs, rhs, type) instead"))
1054  {
1055  }
1056 
1057  plus_exprt(exprt _lhs, exprt _rhs)
1058  : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
1059  {
1060  }
1061 
1062  plus_exprt(exprt _lhs, exprt _rhs, typet _type)
1063  : multi_ary_exprt(
1064  std::move(_lhs),
1065  ID_plus,
1066  std::move(_rhs),
1067  std::move(_type))
1068  {
1069  }
1070 
1071  plus_exprt(operandst _operands, typet _type)
1072  : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
1073  {
1074  }
1075 };
1076 
1077 template <>
1078 inline bool can_cast_expr<plus_exprt>(const exprt &base)
1079 {
1080  return base.id() == ID_plus;
1081 }
1082 
1083 inline void validate_expr(const plus_exprt &value)
1084 {
1085  validate_operands(value, 2, "Plus must have two or more operands", true);
1086 }
1087 
1094 inline const plus_exprt &to_plus_expr(const exprt &expr)
1095 {
1096  PRECONDITION(expr.id()==ID_plus);
1097  const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
1098  validate_expr(ret);
1099  return ret;
1100 }
1101 
1104 {
1105  PRECONDITION(expr.id()==ID_plus);
1106  plus_exprt &ret = static_cast<plus_exprt &>(expr);
1107  validate_expr(ret);
1108  return ret;
1109 }
1110 
1111 
1114 {
1115 public:
1116  DEPRECATED(SINCE(2018, 9, 21, "use minus_exprt(lhs, rhs) instead"))
1118  {
1119  }
1120 
1122  : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
1123  {
1124  }
1125 };
1126 
1127 template <>
1128 inline bool can_cast_expr<minus_exprt>(const exprt &base)
1129 {
1130  return base.id() == ID_minus;
1131 }
1132 
1133 inline void validate_expr(const minus_exprt &value)
1134 {
1135  validate_operands(value, 2, "Minus must have two or more operands", true);
1136 }
1137 
1144 inline const minus_exprt &to_minus_expr(const exprt &expr)
1145 {
1146  PRECONDITION(expr.id()==ID_minus);
1147  const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
1148  validate_expr(ret);
1149  return ret;
1150 }
1151 
1154 {
1155  PRECONDITION(expr.id()==ID_minus);
1156  minus_exprt &ret = static_cast<minus_exprt &>(expr);
1157  validate_expr(ret);
1158  return ret;
1159 }
1160 
1161 
1165 {
1166 public:
1167  DEPRECATED(SINCE(2018, 9, 21, "use mult_exprt(lhs, rhs) instead"))
1169  {
1170  }
1171 
1172  mult_exprt(exprt _lhs, exprt _rhs)
1173  : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
1174  {
1175  }
1176 };
1177 
1178 template <>
1179 inline bool can_cast_expr<mult_exprt>(const exprt &base)
1180 {
1181  return base.id() == ID_mult;
1182 }
1183 
1184 inline void validate_expr(const mult_exprt &value)
1185 {
1186  validate_operands(value, 2, "Multiply must have two or more operands", true);
1187 }
1188 
1195 inline const mult_exprt &to_mult_expr(const exprt &expr)
1196 {
1197  PRECONDITION(expr.id()==ID_mult);
1198  const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1199  validate_expr(ret);
1200  return ret;
1201 }
1202 
1205 {
1206  PRECONDITION(expr.id()==ID_mult);
1207  mult_exprt &ret = static_cast<mult_exprt &>(expr);
1208  validate_expr(ret);
1209  return ret;
1210 }
1211 
1212 
1215 {
1216 public:
1217  DEPRECATED(SINCE(2018, 9, 21, "use div_exprt(lhs, rhs) instead"))
1219  {
1220  }
1221 
1222  div_exprt(exprt _lhs, exprt _rhs)
1223  : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1224  {
1225  }
1226 
1229  {
1230  return op0();
1231  }
1232 
1234  const exprt &dividend() const
1235  {
1236  return op0();
1237  }
1238 
1241  {
1242  return op1();
1243  }
1244 
1246  const exprt &divisor() const
1247  {
1248  return op1();
1249  }
1250 };
1251 
1252 template <>
1253 inline bool can_cast_expr<div_exprt>(const exprt &base)
1254 {
1255  return base.id() == ID_div;
1256 }
1257 
1258 inline void validate_expr(const div_exprt &value)
1259 {
1260  validate_operands(value, 2, "Divide must have two operands");
1261 }
1262 
1269 inline const div_exprt &to_div_expr(const exprt &expr)
1270 {
1271  PRECONDITION(expr.id()==ID_div);
1272  const div_exprt &ret = static_cast<const div_exprt &>(expr);
1273  validate_expr(ret);
1274  return ret;
1275 }
1276 
1279 {
1280  PRECONDITION(expr.id()==ID_div);
1281  div_exprt &ret = static_cast<div_exprt &>(expr);
1282  validate_expr(ret);
1283  return ret;
1284 }
1285 
1286 
1289 {
1290 public:
1291  DEPRECATED(SINCE(2018, 9, 21, "use mod_exprt(lhs, rhs) instead"))
1293  {
1294  }
1295 
1296  mod_exprt(exprt _lhs, exprt _rhs)
1297  : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1298  {
1299  }
1300 };
1301 
1302 template <>
1303 inline bool can_cast_expr<mod_exprt>(const exprt &base)
1304 {
1305  return base.id() == ID_mod;
1306 }
1307 
1308 inline void validate_expr(const mod_exprt &value)
1309 {
1310  validate_operands(value, 2, "Modulo must have two operands");
1311 }
1312 
1319 inline const mod_exprt &to_mod_expr(const exprt &expr)
1320 {
1321  PRECONDITION(expr.id()==ID_mod);
1322  const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1323  validate_expr(ret);
1324  return ret;
1325 }
1326 
1329 {
1330  PRECONDITION(expr.id()==ID_mod);
1331  mod_exprt &ret = static_cast<mod_exprt &>(expr);
1332  validate_expr(ret);
1333  return ret;
1334 }
1335 
1336 
1339 {
1340 public:
1341  DEPRECATED(SINCE(2018, 9, 21, "use rem_exprt(lhs, rhs) instead"))
1343  {
1344  }
1345 
1346  rem_exprt(exprt _lhs, exprt _rhs)
1347  : binary_exprt(std::move(_lhs), ID_rem, std::move(_rhs))
1348  {
1349  }
1350 };
1351 
1352 template <>
1353 inline bool can_cast_expr<rem_exprt>(const exprt &base)
1354 {
1355  return base.id() == ID_rem;
1356 }
1357 
1358 inline void validate_expr(const rem_exprt &value)
1359 {
1360  validate_operands(value, 2, "Remainder must have two operands");
1361 }
1362 
1369 inline const rem_exprt &to_rem_expr(const exprt &expr)
1370 {
1371  PRECONDITION(expr.id()==ID_rem);
1372  const rem_exprt &ret = static_cast<const rem_exprt &>(expr);
1373  validate_expr(ret);
1374  return ret;
1375 }
1376 
1379 {
1380  PRECONDITION(expr.id()==ID_rem);
1381  rem_exprt &ret = static_cast<rem_exprt &>(expr);
1382  validate_expr(ret);
1383  return ret;
1384 }
1385 
1386 
1389 {
1390 public:
1391  DEPRECATED(SINCE(2018, 9, 21, "use equal_exprt(lhs, rhs) instead"))
1393  {
1394  }
1395 
1397  : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1398  {
1399  }
1400 
1401  static void check(
1402  const exprt &expr,
1404  {
1405  binary_relation_exprt::check(expr, vm);
1406  }
1407 
1408  static void validate(
1409  const exprt &expr,
1410  const namespacet &ns,
1412  {
1413  binary_relation_exprt::validate(expr, ns, vm);
1414  }
1415 };
1416 
1417 template <>
1418 inline bool can_cast_expr<equal_exprt>(const exprt &base)
1419 {
1420  return base.id() == ID_equal;
1421 }
1422 
1423 inline void validate_expr(const equal_exprt &value)
1424 {
1425  equal_exprt::check(value);
1426 }
1427 
1434 inline const equal_exprt &to_equal_expr(const exprt &expr)
1435 {
1436  PRECONDITION(expr.id()==ID_equal);
1437  equal_exprt::check(expr);
1438  return static_cast<const equal_exprt &>(expr);
1439 }
1440 
1443 {
1444  PRECONDITION(expr.id()==ID_equal);
1445  equal_exprt::check(expr);
1446  return static_cast<equal_exprt &>(expr);
1447 }
1448 
1449 
1452 {
1453 public:
1454  DEPRECATED(SINCE(2018, 9, 21, "use notequal_exprt(lhs, rhs) instead"))
1456  {
1457  }
1458 
1460  : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1461  {
1462  }
1463 };
1464 
1465 template <>
1466 inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1467 {
1468  return base.id() == ID_notequal;
1469 }
1470 
1471 inline void validate_expr(const notequal_exprt &value)
1472 {
1473  validate_operands(value, 2, "Inequality must have two operands");
1474 }
1475 
1482 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1483 {
1484  PRECONDITION(expr.id()==ID_notequal);
1485  const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1486  validate_expr(ret);
1487  return ret;
1488 }
1489 
1492 {
1493  PRECONDITION(expr.id()==ID_notequal);
1494  notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1495  validate_expr(ret);
1496  return ret;
1497 }
1498 
1499 
1502 {
1503 public:
1504  DEPRECATED(SINCE(2018, 9, 21, "use index_exprt(array, index) instead"))
1506  {
1507  }
1508 
1509  DEPRECATED(SINCE(2018, 9, 21, "use index_exprt(array, index) instead"))
1510  explicit index_exprt(const typet &_type):binary_exprt(ID_index, _type)
1511  {
1512  }
1513 
1514  index_exprt(const exprt &_array, exprt _index)
1515  : binary_exprt(_array, ID_index, std::move(_index), _array.type().subtype())
1516  {
1517  }
1518 
1519  index_exprt(exprt _array, exprt _index, typet _type)
1520  : binary_exprt(
1521  std::move(_array),
1522  ID_index,
1523  std::move(_index),
1524  std::move(_type))
1525  {
1526  }
1527 
1529  {
1530  return op0();
1531  }
1532 
1533  const exprt &array() const
1534  {
1535  return op0();
1536  }
1537 
1539  {
1540  return op1();
1541  }
1542 
1543  const exprt &index() const
1544  {
1545  return op1();
1546  }
1547 };
1548 
1549 template <>
1550 inline bool can_cast_expr<index_exprt>(const exprt &base)
1551 {
1552  return base.id() == ID_index;
1553 }
1554 
1555 inline void validate_expr(const index_exprt &value)
1556 {
1557  validate_operands(value, 2, "Array index must have two operands");
1558 }
1559 
1566 inline const index_exprt &to_index_expr(const exprt &expr)
1567 {
1568  PRECONDITION(expr.id()==ID_index);
1569  const index_exprt &ret = static_cast<const index_exprt &>(expr);
1570  validate_expr(ret);
1571  return ret;
1572 }
1573 
1576 {
1577  PRECONDITION(expr.id()==ID_index);
1578  index_exprt &ret = static_cast<index_exprt &>(expr);
1579  validate_expr(ret);
1580  return ret;
1581 }
1582 
1583 
1586 {
1587 public:
1588  explicit array_of_exprt(exprt _what, array_typet _type)
1589  : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1590  {
1591  }
1592 
1593  const array_typet &type() const
1594  {
1595  return static_cast<const array_typet &>(unary_exprt::type());
1596  }
1597 
1599  {
1600  return static_cast<array_typet &>(unary_exprt::type());
1601  }
1602 
1604  {
1605  return op0();
1606  }
1607 
1608  const exprt &what() const
1609  {
1610  return op0();
1611  }
1612 };
1613 
1614 template <>
1615 inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1616 {
1617  return base.id() == ID_array_of;
1618 }
1619 
1620 inline void validate_expr(const array_of_exprt &value)
1621 {
1622  validate_operands(value, 1, "'Array of' must have one operand");
1623 }
1624 
1631 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1632 {
1633  PRECONDITION(expr.id()==ID_array_of);
1634  const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1635  validate_expr(ret);
1636  return ret;
1637 }
1638 
1641 {
1642  PRECONDITION(expr.id()==ID_array_of);
1643  array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1644  validate_expr(ret);
1645  return ret;
1646 }
1647 
1648 
1651 {
1652 public:
1653  DEPRECATED(SINCE(2019, 1, 12, "use array_exprt(operands, type) instead"))
1654  explicit array_exprt(const array_typet &_type)
1655  : multi_ary_exprt(ID_array, _type)
1656  {
1657  }
1658 
1660  : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1661  {
1662  }
1663 
1664  const array_typet &type() const
1665  {
1666  return static_cast<const array_typet &>(multi_ary_exprt::type());
1667  }
1668 
1670  {
1671  return static_cast<array_typet &>(multi_ary_exprt::type());
1672  }
1673 };
1674 
1675 template <>
1676 inline bool can_cast_expr<array_exprt>(const exprt &base)
1677 {
1678  return base.id() == ID_array;
1679 }
1680 
1687 inline const array_exprt &to_array_expr(const exprt &expr)
1688 {
1689  PRECONDITION(expr.id()==ID_array);
1690  return static_cast<const array_exprt &>(expr);
1691 }
1692 
1695 {
1696  PRECONDITION(expr.id()==ID_array);
1697  return static_cast<array_exprt &>(expr);
1698 }
1699 
1703 {
1704 public:
1705  DEPRECATED(SINCE(2019, 1, 12, "use array_list_exprt(operands, type) instead"))
1706  explicit array_list_exprt(const array_typet &_type)
1707  : multi_ary_exprt(ID_array_list, _type)
1708  {
1709  }
1710 
1712  : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1713  {
1714  }
1715 
1716  const array_typet &type() const
1717  {
1718  return static_cast<const array_typet &>(multi_ary_exprt::type());
1719  }
1720 
1722  {
1723  return static_cast<array_typet &>(multi_ary_exprt::type());
1724  }
1725 
1727  void add(exprt index, exprt value)
1728  {
1729  add_to_operands(std::move(index), std::move(value));
1730  }
1731 };
1732 
1733 template <>
1734 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1735 {
1736  return base.id() == ID_array_list;
1737 }
1738 
1739 inline void validate_expr(const array_list_exprt &value)
1740 {
1741  PRECONDITION(value.operands().size() % 2 == 0);
1742 }
1743 
1744 inline const array_list_exprt &to_array_list_expr(const exprt &expr)
1745 {
1747  auto &ret = static_cast<const array_list_exprt &>(expr);
1748  validate_expr(ret);
1749  return ret;
1750 }
1751 
1753 {
1755  auto &ret = static_cast<array_list_exprt &>(expr);
1756  validate_expr(ret);
1757  return ret;
1758 }
1759 
1762 {
1763 public:
1764  DEPRECATED(SINCE(2018, 9, 21, "use vector_exprt(type) instead"))
1766  {
1767  }
1768 
1769  DEPRECATED(SINCE(2019, 1, 12, "use vector_exprt(operands, type) instead"))
1770  explicit vector_exprt(const vector_typet &_type)
1771  : multi_ary_exprt(ID_vector, _type)
1772  {
1773  }
1774 
1776  : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1777  {
1778  }
1779 };
1780 
1781 template <>
1782 inline bool can_cast_expr<vector_exprt>(const exprt &base)
1783 {
1784  return base.id() == ID_vector;
1785 }
1786 
1793 inline const vector_exprt &to_vector_expr(const exprt &expr)
1794 {
1795  PRECONDITION(expr.id()==ID_vector);
1796  return static_cast<const vector_exprt &>(expr);
1797 }
1798 
1801 {
1802  PRECONDITION(expr.id()==ID_vector);
1803  return static_cast<vector_exprt &>(expr);
1804 }
1805 
1806 
1809 {
1810 public:
1811  DEPRECATED(
1812  SINCE(2018, 9, 21, "use union_exprt(component_name, value, type) instead"))
1814  {
1815  }
1816 
1817  DEPRECATED(
1818  SINCE(2018, 9, 21, "use union_exprt(component_name, value, type) instead"))
1819  explicit union_exprt(const typet &_type):
1820  unary_exprt(ID_union, _type)
1821  {
1822  }
1823 
1824  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1825  : unary_exprt(ID_union, std::move(_value), std::move(_type))
1826  {
1827  set_component_name(_component_name);
1828  }
1829 
1831  {
1832  return get(ID_component_name);
1833  }
1834 
1835  void set_component_name(const irep_idt &component_name)
1836  {
1837  set(ID_component_name, component_name);
1838  }
1839 
1840  std::size_t get_component_number() const
1841  {
1842  return get_size_t(ID_component_number);
1843  }
1844 
1845  void set_component_number(std::size_t component_number)
1846  {
1847  set(ID_component_number, narrow_cast<long long>(component_number));
1848  }
1849 };
1850 
1851 template <>
1852 inline bool can_cast_expr<union_exprt>(const exprt &base)
1853 {
1854  return base.id() == ID_union;
1855 }
1856 
1857 inline void validate_expr(const union_exprt &value)
1858 {
1859  validate_operands(value, 1, "Union constructor must have one operand");
1860 }
1861 
1868 inline const union_exprt &to_union_expr(const exprt &expr)
1869 {
1870  PRECONDITION(expr.id()==ID_union);
1871  const union_exprt &ret = static_cast<const union_exprt &>(expr);
1872  validate_expr(ret);
1873  return ret;
1874 }
1875 
1878 {
1879  PRECONDITION(expr.id()==ID_union);
1880  union_exprt &ret = static_cast<union_exprt &>(expr);
1881  validate_expr(ret);
1882  return ret;
1883 }
1884 
1885 
1888 {
1889 public:
1890  DEPRECATED(
1891  SINCE(2018, 9, 21, "use struct_exprt(component_name, value, type) instead"))
1893  {
1894  }
1895 
1896  DEPRECATED(
1897  SINCE(2019, 1, 12, "use struct_exprt(component_name, value, type) instead"))
1898  explicit struct_exprt(const typet &_type) : multi_ary_exprt(ID_struct, _type)
1899  {
1900  }
1901 
1902  struct_exprt(operandst _operands, typet _type)
1903  : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1904  {
1905  }
1906 
1907  exprt &component(const irep_idt &name, const namespacet &ns);
1908  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1909 };
1910 
1911 template <>
1912 inline bool can_cast_expr<struct_exprt>(const exprt &base)
1913 {
1914  return base.id() == ID_struct;
1915 }
1916 
1923 inline const struct_exprt &to_struct_expr(const exprt &expr)
1924 {
1925  PRECONDITION(expr.id()==ID_struct);
1926  return static_cast<const struct_exprt &>(expr);
1927 }
1928 
1931 {
1932  PRECONDITION(expr.id()==ID_struct);
1933  return static_cast<struct_exprt &>(expr);
1934 }
1935 
1936 
1939 {
1940 public:
1941  DEPRECATED(SINCE(2018, 9, 21, "use complex_exprt(r, i, type) instead"))
1943  {
1944  }
1945 
1946  DEPRECATED(SINCE(2018, 9, 21, "use complex_exprt(r, i, type) instead"))
1947  explicit complex_exprt(const complex_typet &_type):
1948  binary_exprt(ID_complex, _type)
1949  {
1950  }
1951 
1953  : binary_exprt(
1954  std::move(_real),
1955  ID_complex,
1956  std::move(_imag),
1957  std::move(_type))
1958  {
1959  }
1960 
1962  {
1963  return op0();
1964  }
1965 
1966  const exprt &real() const
1967  {
1968  return op0();
1969  }
1970 
1972  {
1973  return op1();
1974  }
1975 
1976  const exprt &imag() const
1977  {
1978  return op1();
1979  }
1980 };
1981 
1982 template <>
1983 inline bool can_cast_expr<complex_exprt>(const exprt &base)
1984 {
1985  return base.id() == ID_complex;
1986 }
1987 
1988 inline void validate_expr(const complex_exprt &value)
1989 {
1990  validate_operands(value, 2, "Complex constructor must have two operands");
1991 }
1992 
1999 inline const complex_exprt &to_complex_expr(const exprt &expr)
2000 {
2001  PRECONDITION(expr.id()==ID_complex);
2002  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
2003  validate_expr(ret);
2004  return ret;
2005 }
2006 
2009 {
2010  PRECONDITION(expr.id()==ID_complex);
2011  complex_exprt &ret = static_cast<complex_exprt &>(expr);
2012  validate_expr(ret);
2013  return ret;
2014 }
2015 
2018 {
2019 public:
2020  explicit complex_real_exprt(const exprt &op)
2021  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
2022  {
2023  }
2024 };
2025 
2026 template <>
2028 {
2029  return base.id() == ID_complex_real;
2030 }
2031 
2032 inline void validate_expr(const complex_real_exprt &expr)
2033 {
2035  expr, 1, "real part retrieval operation must have one operand");
2036 }
2037 
2045 {
2046  PRECONDITION(expr.id() == ID_complex_real);
2047  const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
2048  validate_expr(ret);
2049  return ret;
2050 }
2051 
2054 {
2055  PRECONDITION(expr.id() == ID_complex_real);
2056  complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
2057  validate_expr(ret);
2058  return ret;
2059 }
2060 
2063 {
2064 public:
2065  explicit complex_imag_exprt(const exprt &op)
2066  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
2067  {
2068  }
2069 };
2070 
2071 template <>
2073 {
2074  return base.id() == ID_complex_imag;
2075 }
2076 
2077 inline void validate_expr(const complex_imag_exprt &expr)
2078 {
2080  expr, 1, "imaginary part retrieval operation must have one operand");
2081 }
2082 
2090 {
2091  PRECONDITION(expr.id() == ID_complex_imag);
2092  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
2093  validate_expr(ret);
2094  return ret;
2095 }
2096 
2099 {
2100  PRECONDITION(expr.id() == ID_complex_imag);
2101  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
2102  validate_expr(ret);
2103  return ret;
2104 }
2105 
2106 class namespacet;
2107 
2110 {
2111 public:
2113  : binary_exprt(
2114  exprt(ID_unknown),
2115  ID_object_descriptor,
2116  exprt(ID_unknown),
2117  typet())
2118  {
2119  }
2120 
2121  explicit object_descriptor_exprt(exprt _object)
2122  : binary_exprt(
2123  std::move(_object),
2124  ID_object_descriptor,
2125  exprt(ID_unknown),
2126  typet())
2127  {
2128  }
2129 
2134  void build(const exprt &expr, const namespacet &ns);
2135 
2137  {
2138  return op0();
2139  }
2140 
2141  const exprt &object() const
2142  {
2143  return op0();
2144  }
2145 
2146  const exprt &root_object() const;
2147 
2149  {
2150  return op1();
2151  }
2152 
2153  const exprt &offset() const
2154  {
2155  return op1();
2156  }
2157 };
2158 
2159 template <>
2161 {
2162  return base.id() == ID_object_descriptor;
2163 }
2164 
2165 inline void validate_expr(const object_descriptor_exprt &value)
2166 {
2167  validate_operands(value, 2, "Object descriptor must have two operands");
2168 }
2169 
2177  const exprt &expr)
2178 {
2179  PRECONDITION(expr.id()==ID_object_descriptor);
2180  const object_descriptor_exprt &ret =
2181  static_cast<const object_descriptor_exprt &>(expr);
2182  validate_expr(ret);
2183  return ret;
2184 }
2185 
2188 {
2189  PRECONDITION(expr.id()==ID_object_descriptor);
2190  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
2191  validate_expr(ret);
2192  return ret;
2193 }
2194 
2195 
2198 {
2199 public:
2200  DEPRECATED(SINCE(2019, 2, 11, "use dynamic_object_exprt(type) instead"))
2202  : binary_exprt(exprt(ID_unknown), ID_dynamic_object, exprt(ID_unknown))
2203  {
2204  }
2205 
2207  : binary_exprt(
2208  exprt(ID_unknown),
2209  ID_dynamic_object,
2210  exprt(ID_unknown),
2211  std::move(type))
2212  {
2213  }
2214 
2215  void set_instance(unsigned int instance);
2216 
2217  unsigned int get_instance() const;
2218 
2220  {
2221  return op1();
2222  }
2223 
2224  const exprt &valid() const
2225  {
2226  return op1();
2227  }
2228 };
2229 
2230 template <>
2232 {
2233  return base.id() == ID_dynamic_object;
2234 }
2235 
2236 inline void validate_expr(const dynamic_object_exprt &value)
2237 {
2238  validate_operands(value, 2, "Dynamic object must have two operands");
2239 }
2240 
2248  const exprt &expr)
2249 {
2250  PRECONDITION(expr.id()==ID_dynamic_object);
2251  const dynamic_object_exprt &ret =
2252  static_cast<const dynamic_object_exprt &>(expr);
2253  validate_expr(ret);
2254  return ret;
2255 }
2256 
2259 {
2260  PRECONDITION(expr.id()==ID_dynamic_object);
2261  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
2262  validate_expr(ret);
2263  return ret;
2264 }
2265 
2266 
2269 {
2270 public:
2271  DEPRECATED(SINCE(2018, 9, 21, "use typecast_exprt(op, type) instead"))
2272  explicit typecast_exprt(const typet &_type):unary_exprt(ID_typecast, _type)
2273  {
2274  }
2275 
2277  : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2278  {
2279  }
2280 
2281  // returns a typecast if the type doesn't already match
2282  static exprt conditional_cast(const exprt &expr, const typet &type)
2283  {
2284  if(expr.type() == type)
2285  return expr;
2286  else
2287  return typecast_exprt(expr, type);
2288  }
2289 };
2290 
2291 template <>
2292 inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2293 {
2294  return base.id() == ID_typecast;
2295 }
2296 
2297 inline void validate_expr(const typecast_exprt &value)
2298 {
2299  validate_operands(value, 1, "Typecast must have one operand");
2300 }
2301 
2308 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2309 {
2310  PRECONDITION(expr.id()==ID_typecast);
2311  const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
2312  validate_expr(ret);
2313  return ret;
2314 }
2315 
2318 {
2319  PRECONDITION(expr.id()==ID_typecast);
2320  typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
2321  validate_expr(ret);
2322  return ret;
2323 }
2324 
2325 
2328 {
2329 public:
2330  DEPRECATED(
2331  SINCE(2018, 9, 21, "use floatbv_typecast_exprt(op, r, type) instead"))
2332  floatbv_typecast_exprt():binary_exprt(ID_floatbv_typecast)
2333  {
2334  }
2335 
2337  : binary_exprt(
2338  std::move(op),
2339  ID_floatbv_typecast,
2340  std::move(rounding),
2341  std::move(_type))
2342  {
2343  }
2344 
2346  {
2347  return op0();
2348  }
2349 
2350  const exprt &op() const
2351  {
2352  return op0();
2353  }
2354 
2356  {
2357  return op1();
2358  }
2359 
2360  const exprt &rounding_mode() const
2361  {
2362  return op1();
2363  }
2364 };
2365 
2366 template <>
2368 {
2369  return base.id() == ID_floatbv_typecast;
2370 }
2371 
2372 inline void validate_expr(const floatbv_typecast_exprt &value)
2373 {
2374  validate_operands(value, 2, "Float typecast must have two operands");
2375 }
2376 
2384 {
2385  PRECONDITION(expr.id()==ID_floatbv_typecast);
2386  const floatbv_typecast_exprt &ret =
2387  static_cast<const floatbv_typecast_exprt &>(expr);
2388  validate_expr(ret);
2389  return ret;
2390 }
2391 
2394 {
2395  PRECONDITION(expr.id()==ID_floatbv_typecast);
2396  floatbv_typecast_exprt &ret = static_cast<floatbv_typecast_exprt &>(expr);
2397  validate_expr(ret);
2398  return ret;
2399 }
2400 
2401 
2404 {
2405 public:
2406  DEPRECATED(SINCE(2019, 1, 12, "use and_exprt(op, op) instead"))
2408  {
2409  }
2410 
2412  : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2413  {
2414  }
2415 
2417  : multi_ary_exprt(
2418  ID_and,
2419  {std::move(op0), std::move(op1), std::move(op2)},
2420  bool_typet())
2421  {
2422  }
2423 
2425  : multi_ary_exprt(
2426  ID_and,
2427  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2428  bool_typet())
2429  {
2430  }
2431 
2432  explicit and_exprt(exprt::operandst _operands)
2433  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2434  {
2435  }
2436 };
2437 
2441 
2443 
2444 template <>
2445 inline bool can_cast_expr<and_exprt>(const exprt &base)
2446 {
2447  return base.id() == ID_and;
2448 }
2449 
2456 inline const and_exprt &to_and_expr(const exprt &expr)
2457 {
2458  PRECONDITION(expr.id()==ID_and);
2459  return static_cast<const and_exprt &>(expr);
2460 }
2461 
2464 {
2465  PRECONDITION(expr.id()==ID_and);
2466  return static_cast<and_exprt &>(expr);
2467 }
2468 
2469 
2472 {
2473 public:
2474  DEPRECATED(SINCE(2018, 9, 21, "use implies_exprt(a, b) instead"))
2476  {
2477  }
2478 
2480  : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2481  {
2482  }
2483 };
2484 
2485 template <>
2486 inline bool can_cast_expr<implies_exprt>(const exprt &base)
2487 {
2488  return base.id() == ID_implies;
2489 }
2490 
2491 inline void validate_expr(const implies_exprt &value)
2492 {
2493  validate_operands(value, 2, "Implies must have two operands");
2494 }
2495 
2502 inline const implies_exprt &to_implies_expr(const exprt &expr)
2503 {
2504  PRECONDITION(expr.id()==ID_implies);
2505  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2506  validate_expr(ret);
2507  return ret;
2508 }
2509 
2512 {
2513  PRECONDITION(expr.id()==ID_implies);
2514  implies_exprt &ret = static_cast<implies_exprt &>(expr);
2515  validate_expr(ret);
2516  return ret;
2517 }
2518 
2519 
2522 {
2523 public:
2524  DEPRECATED(SINCE(2019, 1, 12, "use or_exprt(op, op) instead"))
2526  {
2527  }
2528 
2530  : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2531  {
2532  }
2533 
2535  : multi_ary_exprt(
2536  ID_or,
2537  {std::move(op0), std::move(op1), std::move(op2)},
2538  bool_typet())
2539  {
2540  }
2541 
2543  : multi_ary_exprt(
2544  ID_or,
2545  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2546  bool_typet())
2547  {
2548  }
2549 
2550  explicit or_exprt(exprt::operandst _operands)
2551  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2552  {
2553  }
2554 };
2555 
2559 
2561 
2562 template <>
2563 inline bool can_cast_expr<or_exprt>(const exprt &base)
2564 {
2565  return base.id() == ID_or;
2566 }
2567 
2574 inline const or_exprt &to_or_expr(const exprt &expr)
2575 {
2576  PRECONDITION(expr.id()==ID_or);
2577  return static_cast<const or_exprt &>(expr);
2578 }
2579 
2581 inline or_exprt &to_or_expr(exprt &expr)
2582 {
2583  PRECONDITION(expr.id()==ID_or);
2584  return static_cast<or_exprt &>(expr);
2585 }
2586 
2587 
2590 {
2591 public:
2592  DEPRECATED(SINCE(2019, 1, 12, "use xor_exprt(op, op) instead"))
2594  {
2595  }
2596 
2597  xor_exprt(exprt _op0, exprt _op1)
2598  : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2599  {
2600  }
2601 };
2602 
2603 template <>
2604 inline bool can_cast_expr<xor_exprt>(const exprt &base)
2605 {
2606  return base.id() == ID_xor;
2607 }
2608 
2615 inline const xor_exprt &to_xor_expr(const exprt &expr)
2616 {
2617  PRECONDITION(expr.id()==ID_xor);
2618  return static_cast<const xor_exprt &>(expr);
2619 }
2620 
2623 {
2624  PRECONDITION(expr.id()==ID_xor);
2625  return static_cast<xor_exprt &>(expr);
2626 }
2627 
2628 
2631 {
2632 public:
2633  DEPRECATED(SINCE(2018, 9, 21, "use bitnot_exprt(op) instead"))
2635  {
2636  }
2637 
2638  explicit bitnot_exprt(exprt op) : unary_exprt(ID_bitnot, std::move(op))
2639  {
2640  }
2641 };
2642 
2643 template <>
2644 inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
2645 {
2646  return base.id() == ID_bitnot;
2647 }
2648 
2649 inline void validate_expr(const bitnot_exprt &value)
2650 {
2651  validate_operands(value, 1, "Bit-wise not must have one operand");
2652 }
2653 
2660 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
2661 {
2662  PRECONDITION(expr.id()==ID_bitnot);
2663  const bitnot_exprt &ret = static_cast<const bitnot_exprt &>(expr);
2664  validate_expr(ret);
2665  return ret;
2666 }
2667 
2670 {
2671  PRECONDITION(expr.id()==ID_bitnot);
2672  bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
2673  validate_expr(ret);
2674  return ret;
2675 }
2676 
2677 
2680 {
2681 public:
2682  DEPRECATED(SINCE(2018, 9, 21, "use bitor_exprt(op0, op1) instead"))
2684  {
2685  }
2686 
2687  bitor_exprt(const exprt &_op0, exprt _op1)
2688  : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
2689  {
2690  }
2691 };
2692 
2693 template <>
2694 inline bool can_cast_expr<bitor_exprt>(const exprt &base)
2695 {
2696  return base.id() == ID_bitor;
2697 }
2698 
2705 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
2706 {
2707  PRECONDITION(expr.id()==ID_bitor);
2708  return static_cast<const bitor_exprt &>(expr);
2709 }
2710 
2713 {
2714  PRECONDITION(expr.id()==ID_bitor);
2715  return static_cast<bitor_exprt &>(expr);
2716 }
2717 
2718 
2721 {
2722 public:
2723  DEPRECATED(SINCE(2018, 9, 21, "use bitxor_exprt(op0, op1) instead"))
2725  {
2726  }
2727 
2729  : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
2730  {
2731  }
2732 };
2733 
2734 template <>
2735 inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
2736 {
2737  return base.id() == ID_bitxor;
2738 }
2739 
2746 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
2747 {
2748  PRECONDITION(expr.id()==ID_bitxor);
2749  return static_cast<const bitxor_exprt &>(expr);
2750 }
2751 
2754 {
2755  PRECONDITION(expr.id()==ID_bitxor);
2756  return static_cast<bitxor_exprt &>(expr);
2757 }
2758 
2759 
2762 {
2763 public:
2764  DEPRECATED(SINCE(2018, 9, 21, "use bitand_exprt(op0, op1) instead"))
2766  {
2767  }
2768 
2769  bitand_exprt(const exprt &_op0, exprt _op1)
2770  : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
2771  {
2772  }
2773 };
2774 
2775 template <>
2776 inline bool can_cast_expr<bitand_exprt>(const exprt &base)
2777 {
2778  return base.id() == ID_bitand;
2779 }
2780 
2787 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
2788 {
2789  PRECONDITION(expr.id()==ID_bitand);
2790  return static_cast<const bitand_exprt &>(expr);
2791 }
2792 
2795 {
2796  PRECONDITION(expr.id()==ID_bitand);
2797  return static_cast<bitand_exprt &>(expr);
2798 }
2799 
2800 
2803 {
2804 public:
2805  DEPRECATED(SINCE(2018, 9, 21, "use shift_exprt(value, id, distance) instead"))
2806  explicit shift_exprt(const irep_idt &_id):binary_exprt(_id)
2807  {
2808  }
2809 
2810  DEPRECATED(SINCE(2018, 9, 21, "use shift_exprt(value, id, distance) instead"))
2811  shift_exprt(const irep_idt &_id, const typet &_type):
2812  binary_exprt(_id, _type)
2813  {
2814  }
2815 
2816  shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
2817  : binary_exprt(std::move(_src), _id, std::move(_distance))
2818  {
2819  }
2820 
2821  shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
2822 
2824  {
2825  return op0();
2826  }
2827 
2828  const exprt &op() const
2829  {
2830  return op0();
2831  }
2832 
2834  {
2835  return op1();
2836  }
2837 
2838  const exprt &distance() const
2839  {
2840  return op1();
2841  }
2842 };
2843 
2844 template <>
2845 inline bool can_cast_expr<shift_exprt>(const exprt &base)
2846 {
2847  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr;
2848 }
2849 
2850 inline void validate_expr(const shift_exprt &value)
2851 {
2852  validate_operands(value, 2, "Shifts must have two operands");
2853 }
2854 
2861 inline const shift_exprt &to_shift_expr(const exprt &expr)
2862 {
2863  const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
2864  validate_expr(ret);
2865  return ret;
2866 }
2867 
2870 {
2871  shift_exprt &ret = static_cast<shift_exprt &>(expr);
2872  validate_expr(ret);
2873  return ret;
2874 }
2875 
2876 
2879 {
2880 public:
2881  DEPRECATED(SINCE(2018, 9, 21, "use shl_exprt(value, distance) instead"))
2883  {
2884  }
2885 
2886  shl_exprt(exprt _src, exprt _distance)
2887  : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
2888  {
2889  }
2890 
2891  shl_exprt(exprt _src, const std::size_t _distance)
2892  : shift_exprt(std::move(_src), ID_shl, _distance)
2893  {
2894  }
2895 };
2896 
2903 inline const shl_exprt &to_shl_expr(const exprt &expr)
2904 {
2905  PRECONDITION(expr.id() == ID_shl);
2906  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
2907  validate_expr(ret);
2908  return ret;
2909 }
2910 
2913 {
2914  PRECONDITION(expr.id() == ID_shl);
2915  shl_exprt &ret = static_cast<shl_exprt &>(expr);
2916  validate_expr(ret);
2917  return ret;
2918 }
2919 
2922 {
2923 public:
2924  DEPRECATED(SINCE(2018, 9, 21, "use ashl_exprt(value, distance) instead"))
2926  {
2927  }
2928 
2929  ashr_exprt(exprt _src, exprt _distance)
2930  : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
2931  {
2932  }
2933 
2934  ashr_exprt(exprt _src, const std::size_t _distance)
2935  : shift_exprt(std::move(_src), ID_ashr, _distance)
2936  {
2937  }
2938 };
2939 
2942 {
2943 public:
2944  DEPRECATED(SINCE(2018, 9, 21, "use lshl_exprt(value, distance) instead"))
2946  {
2947  }
2948 
2949  lshr_exprt(exprt _src, exprt _distance)
2950  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2951  {
2952  }
2953 
2954  lshr_exprt(exprt _src, const std::size_t _distance)
2955  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2956  {
2957  }
2958 };
2959 
2962 {
2963 public:
2964  DEPRECATED(SINCE(2018, 9, 21, "use extractbit_exprt(value, index) instead"))
2966  {
2967  }
2968 
2971  : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
2972  {
2973  }
2974 
2975  extractbit_exprt(exprt _src, const std::size_t _index);
2976 
2978  {
2979  return op0();
2980  }
2981 
2983  {
2984  return op1();
2985  }
2986 
2987  const exprt &src() const
2988  {
2989  return op0();
2990  }
2991 
2992  const exprt &index() const
2993  {
2994  return op1();
2995  }
2996 };
2997 
2998 template <>
2999 inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
3000 {
3001  return base.id() == ID_extractbit;
3002 }
3003 
3004 inline void validate_expr(const extractbit_exprt &value)
3005 {
3006  validate_operands(value, 2, "Extract bit must have two operands");
3007 }
3008 
3015 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
3016 {
3017  PRECONDITION(expr.id()==ID_extractbit);
3018  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
3019  validate_expr(ret);
3020  return ret;
3021 }
3022 
3025 {
3026  PRECONDITION(expr.id()==ID_extractbit);
3027  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
3028  validate_expr(ret);
3029  return ret;
3030 }
3031 
3032 
3035 {
3036 public:
3037  DEPRECATED(
3038  SINCE(2018, 9, 21, "use extractbits_exprt(value, upper, lower) instead"))
3039  extractbits_exprt() : expr_protectedt(ID_extractbits, typet())
3040  {
3041  operands().resize(3);
3042  }
3043 
3049  extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
3050  : expr_protectedt(
3051  ID_extractbits,
3052  std::move(_type),
3053  {std::move(_src), std::move(_upper), std::move(_lower)})
3054  {
3055  }
3056 
3058  exprt _src,
3059  const std::size_t _upper,
3060  const std::size_t _lower,
3061  typet _type);
3062 
3064  {
3065  return op0();
3066  }
3067 
3069  {
3070  return op1();
3071  }
3072 
3074  {
3075  return op2();
3076  }
3077 
3078  const exprt &src() const
3079  {
3080  return op0();
3081  }
3082 
3083  const exprt &upper() const
3084  {
3085  return op1();
3086  }
3087 
3088  const exprt &lower() const
3089  {
3090  return op2();
3091  }
3092 };
3093 
3094 template <>
3095 inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
3096 {
3097  return base.id() == ID_extractbits;
3098 }
3099 
3100 inline void validate_expr(const extractbits_exprt &value)
3101 {
3102  validate_operands(value, 3, "Extract bits must have three operands");
3103 }
3104 
3111 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
3112 {
3113  PRECONDITION(expr.id()==ID_extractbits);
3114  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
3115  validate_expr(ret);
3116  return ret;
3117 }
3118 
3121 {
3122  PRECONDITION(expr.id()==ID_extractbits);
3123  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
3124  validate_expr(ret);
3125  return ret;
3126 }
3127 
3128 
3131 {
3132 public:
3133  explicit address_of_exprt(const exprt &op);
3134 
3136  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
3137  {
3138  }
3139 
3141  {
3142  return op0();
3143  }
3144 
3145  const exprt &object() const
3146  {
3147  return op0();
3148  }
3149 };
3150 
3151 template <>
3152 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
3153 {
3154  return base.id() == ID_address_of;
3155 }
3156 
3157 inline void validate_expr(const address_of_exprt &value)
3158 {
3159  validate_operands(value, 1, "Address of must have one operand");
3160 }
3161 
3168 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
3169 {
3170  PRECONDITION(expr.id()==ID_address_of);
3171  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
3172  validate_expr(ret);
3173  return ret;
3174 }
3175 
3178 {
3179  PRECONDITION(expr.id()==ID_address_of);
3180  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
3181  validate_expr(ret);
3182  return ret;
3183 }
3184 
3185 
3188 {
3189 public:
3190  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
3191  {
3192  PRECONDITION(as_const(*this).op().type().id() == ID_bool);
3193  }
3194 
3195  DEPRECATED(SINCE(2019, 1, 12, "use not_exprt(op) instead"))
3197  {
3198  }
3199 };
3200 
3201 template <>
3202 inline bool can_cast_expr<not_exprt>(const exprt &base)
3203 {
3204  return base.id() == ID_not;
3205 }
3206 
3207 inline void validate_expr(const not_exprt &value)
3208 {
3209  validate_operands(value, 1, "Not must have one operand");
3210 }
3211 
3218 inline const not_exprt &to_not_expr(const exprt &expr)
3219 {
3220  PRECONDITION(expr.id()==ID_not);
3221  const not_exprt &ret = static_cast<const not_exprt &>(expr);
3222  validate_expr(ret);
3223  return ret;
3224 }
3225 
3228 {
3229  PRECONDITION(expr.id()==ID_not);
3230  not_exprt &ret = static_cast<not_exprt &>(expr);
3231  validate_expr(ret);
3232  return ret;
3233 }
3234 
3235 
3238 {
3239 public:
3240  DEPRECATED(SINCE(2018, 9, 21, "use dereference_exprt(pointer) instead"))
3241  dereference_exprt():unary_exprt(ID_dereference)
3242  {
3243  }
3244 
3245  DEPRECATED(SINCE(2018, 9, 21, "use dereference_exprt(pointer) instead"))
3246  explicit dereference_exprt(const typet &type):
3247  unary_exprt(ID_dereference, type)
3248  {
3249  }
3250 
3251  explicit dereference_exprt(const exprt &op):
3252  unary_exprt(ID_dereference, op, op.type().subtype())
3253  {
3254  PRECONDITION(op.type().id()==ID_pointer);
3255  }
3256 
3258  : unary_exprt(ID_dereference, std::move(op), std::move(type))
3259  {
3260  }
3261 
3263  {
3264  return op0();
3265  }
3266 
3267  const exprt &pointer() const
3268  {
3269  return op0();
3270  }
3271 
3272  static void check(
3273  const exprt &expr,
3275  {
3276  DATA_CHECK(
3277  vm,
3278  expr.operands().size() == 1,
3279  "dereference expression must have one operand");
3280  }
3281 
3282  static void validate(
3283  const exprt &expr,
3284  const namespacet &ns,
3286 };
3287 
3288 template <>
3289 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
3290 {
3291  return base.id() == ID_dereference;
3292 }
3293 
3294 inline void validate_expr(const dereference_exprt &value)
3295 {
3296  validate_operands(value, 1, "Dereference must have one operand");
3297 }
3298 
3305 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
3306 {
3307  PRECONDITION(expr.id()==ID_dereference);
3308  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
3309  validate_expr(ret);
3310  return ret;
3311 }
3312 
3315 {
3316  PRECONDITION(expr.id()==ID_dereference);
3317  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
3318  validate_expr(ret);
3319  return ret;
3320 }
3321 
3322 
3324 class if_exprt : public ternary_exprt
3325 {
3326 public:
3328  : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
3329  {
3330  }
3331 
3333  : ternary_exprt(
3334  ID_if,
3335  std::move(cond),
3336  std::move(t),
3337  std::move(f),
3338  std::move(type))
3339  {
3340  }
3341 
3342  DEPRECATED(SINCE(2018, 9, 21, "use if_exprt(cond, t, f) instead"))
3344  {
3345  }
3346 
3348  {
3349  return op0();
3350  }
3351 
3352  const exprt &cond() const
3353  {
3354  return op0();
3355  }
3356 
3358  {
3359  return op1();
3360  }
3361 
3362  const exprt &true_case() const
3363  {
3364  return op1();
3365  }
3366 
3368  {
3369  return op2();
3370  }
3371 
3372  const exprt &false_case() const
3373  {
3374  return op2();
3375  }
3376 };
3377 
3378 template <>
3379 inline bool can_cast_expr<if_exprt>(const exprt &base)
3380 {
3381  return base.id() == ID_if;
3382 }
3383 
3384 inline void validate_expr(const if_exprt &value)
3385 {
3386  validate_operands(value, 3, "If-then-else must have three operands");
3387 }
3388 
3395 inline const if_exprt &to_if_expr(const exprt &expr)
3396 {
3397  PRECONDITION(expr.id()==ID_if);
3398  const if_exprt &ret = static_cast<const if_exprt &>(expr);
3399  validate_expr(ret);
3400  return ret;
3401 }
3402 
3404 inline if_exprt &to_if_expr(exprt &expr)
3405 {
3406  PRECONDITION(expr.id()==ID_if);
3407  if_exprt &ret = static_cast<if_exprt &>(expr);
3408  validate_expr(ret);
3409  return ret;
3410 }
3411 
3416 {
3417 public:
3418  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
3419  : expr_protectedt(
3420  ID_with,
3421  _old.type(),
3422  {_old, std::move(_where), std::move(_new_value)})
3423  {
3424  }
3425 
3426  DEPRECATED(
3427  SINCE(2018, 9, 21, "use with_exprt(old, where, new_value) instead"))
3429  {
3430  operands().resize(3);
3431  }
3432 
3434  {
3435  return op0();
3436  }
3437 
3438  const exprt &old() const
3439  {
3440  return op0();
3441  }
3442 
3444  {
3445  return op1();
3446  }
3447 
3448  const exprt &where() const
3449  {
3450  return op1();
3451  }
3452 
3454  {
3455  return op2();
3456  }
3457 
3458  const exprt &new_value() const
3459  {
3460  return op2();
3461  }
3462 };
3463 
3464 template <>
3465 inline bool can_cast_expr<with_exprt>(const exprt &base)
3466 {
3467  return base.id() == ID_with;
3468 }
3469 
3470 inline void validate_expr(const with_exprt &value)
3471 {
3473  value, 3, "array/structure update must have at least 3 operands", true);
3475  value.operands().size() % 2 == 1,
3476  "array/structure update must have an odd number of operands");
3477 }
3478 
3485 inline const with_exprt &to_with_expr(const exprt &expr)
3486 {
3487  PRECONDITION(expr.id()==ID_with);
3488  const with_exprt &ret = static_cast<const with_exprt &>(expr);
3489  validate_expr(ret);
3490  return ret;
3491 }
3492 
3495 {
3496  PRECONDITION(expr.id()==ID_with);
3497  with_exprt &ret = static_cast<with_exprt &>(expr);
3498  validate_expr(ret);
3499  return ret;
3500 }
3501 
3503 {
3504 public:
3505  explicit index_designatort(exprt _index)
3506  : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
3507  {
3508  }
3509 
3510  const exprt &index() const
3511  {
3512  return op0();
3513  }
3514 
3516  {
3517  return op0();
3518  }
3519 };
3520 
3521 template <>
3522 inline bool can_cast_expr<index_designatort>(const exprt &base)
3523 {
3524  return base.id() == ID_index_designator;
3525 }
3526 
3527 inline void validate_expr(const index_designatort &value)
3528 {
3529  validate_operands(value, 1, "Index designator must have one operand");
3530 }
3531 
3538 inline const index_designatort &to_index_designator(const exprt &expr)
3539 {
3540  PRECONDITION(expr.id()==ID_index_designator);
3541  const index_designatort &ret = static_cast<const index_designatort &>(expr);
3542  validate_expr(ret);
3543  return ret;
3544 }
3545 
3548 {
3549  PRECONDITION(expr.id()==ID_index_designator);
3550  index_designatort &ret = static_cast<index_designatort &>(expr);
3551  validate_expr(ret);
3552  return ret;
3553 }
3554 
3556 {
3557 public:
3558  explicit member_designatort(const irep_idt &_component_name)
3559  : expr_protectedt(ID_member_designator, typet())
3560  {
3561  set(ID_component_name, _component_name);
3562  }
3563 
3565  {
3566  return get(ID_component_name);
3567  }
3568 };
3569 
3570 template <>
3572 {
3573  return base.id() == ID_member_designator;
3574 }
3575 
3576 inline void validate_expr(const member_designatort &value)
3577 {
3578  validate_operands(value, 0, "Member designator must not have operands");
3579 }
3580 
3588 {
3589  PRECONDITION(expr.id()==ID_member_designator);
3590  const member_designatort &ret = static_cast<const member_designatort &>(expr);
3591  validate_expr(ret);
3592  return ret;
3593 }
3594 
3597 {
3598  PRECONDITION(expr.id()==ID_member_designator);
3599  member_designatort &ret = static_cast<member_designatort &>(expr);
3600  validate_expr(ret);
3601  return ret;
3602 }
3603 
3604 
3607 {
3608 public:
3609  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
3610  : ternary_exprt(
3611  ID_update,
3612  _old,
3613  std::move(_designator),
3614  std::move(_new_value),
3615  _old.type())
3616  {
3617  }
3618 
3619  DEPRECATED(
3620  SINCE(2018, 9, 21, "use update_exprt(old, where, new_value) instead"))
3621  explicit update_exprt(const typet &_type) : ternary_exprt(ID_update, _type)
3622  {
3623  }
3624 
3625  DEPRECATED(
3626  SINCE(2018, 9, 21, "use update_exprt(old, where, new_value) instead"))
3628  {
3629  op1().id(ID_designator);
3630  }
3631 
3633  {
3634  return op0();
3635  }
3636 
3637  const exprt &old() const
3638  {
3639  return op0();
3640  }
3641 
3642  // the designator operands are either
3643  // 1) member_designator or
3644  // 2) index_designator
3645  // as defined above
3647  {
3648  return op1().operands();
3649  }
3650 
3652  {
3653  return op1().operands();
3654  }
3655 
3657  {
3658  return op2();
3659  }
3660 
3661  const exprt &new_value() const
3662  {
3663  return op2();
3664  }
3665 };
3666 
3667 template <>
3668 inline bool can_cast_expr<update_exprt>(const exprt &base)
3669 {
3670  return base.id() == ID_update;
3671 }
3672 
3673 inline void validate_expr(const update_exprt &value)
3674 {
3676  value, 3, "Array/structure update must have three operands");
3677 }
3678 
3685 inline const update_exprt &to_update_expr(const exprt &expr)
3686 {
3687  PRECONDITION(expr.id()==ID_update);
3688  const update_exprt &ret = static_cast<const update_exprt &>(expr);
3689  validate_expr(ret);
3690  return ret;
3691 }
3692 
3695 {
3696  PRECONDITION(expr.id()==ID_update);
3697  update_exprt &ret = static_cast<update_exprt &>(expr);
3698  validate_expr(ret);
3699  return ret;
3700 }
3701 
3702 
3703 #if 0
3704 class array_update_exprt:public expr_protectedt
3706 {
3707 public:
3708  array_update_exprt(
3709  const exprt &_array,
3710  const exprt &_index,
3711  const exprt &_new_value):
3712  exprt(ID_array_update, _array.type())
3713  {
3714  add_to_operands(_array, _index, _new_value);
3715  }
3716 
3717  array_update_exprt():expr_protectedt(ID_array_update)
3718  {
3719  operands().resize(3);
3720  }
3721 
3722  exprt &array()
3723  {
3724  return op0();
3725  }
3726 
3727  const exprt &array() const
3728  {
3729  return op0();
3730  }
3731 
3732  exprt &index()
3733  {
3734  return op1();
3735  }
3736 
3737  const exprt &index() const
3738  {
3739  return op1();
3740  }
3741 
3742  exprt &new_value()
3743  {
3744  return op2();
3745  }
3746 
3747  const exprt &new_value() const
3748  {
3749  return op2();
3750  }
3751 };
3752 
3753 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
3754 {
3755  return base.id()==ID_array_update;
3756 }
3757 
3758 inline void validate_expr(const array_update_exprt &value)
3759 {
3760  validate_operands(value, 3, "Array update must have three operands");
3761 }
3762 
3769 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3770 {
3771  PRECONDITION(expr.id()==ID_array_update);
3772  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
3773  validate_expr(ret);
3774  return ret;
3775 }
3776 
3778 inline array_update_exprt &to_array_update_expr(exprt &expr)
3779 {
3780  PRECONDITION(expr.id()==ID_array_update);
3781  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
3782  validate_expr(ret);
3783  return ret;
3784 }
3785 
3786 #endif
3787 
3788 
3791 {
3792 public:
3793  member_exprt(exprt op, const irep_idt &component_name, typet _type)
3794  : unary_exprt(ID_member, std::move(op), std::move(_type))
3795  {
3796  set_component_name(component_name);
3797  }
3798 
3800  : unary_exprt(ID_member, std::move(op), c.type())
3801  {
3803  }
3804 
3805  DEPRECATED(SINCE(2018, 9, 21, "use member_exprt(op, c) instead"))
3807  {
3808  }
3809 
3811  {
3812  return get(ID_component_name);
3813  }
3814 
3815  void set_component_name(const irep_idt &component_name)
3816  {
3817  set(ID_component_name, component_name);
3818  }
3819 
3820  std::size_t get_component_number() const
3821  {
3822  return get_size_t(ID_component_number);
3823  }
3824 
3825  // will go away, use compound()
3826  const exprt &struct_op() const
3827  {
3828  return op0();
3829  }
3830 
3831  // will go away, use compound()
3833  {
3834  return op0();
3835  }
3836 
3837  const exprt &compound() const
3838  {
3839  return op0();
3840  }
3841 
3843  {
3844  return op0();
3845  }
3846 
3847  static void check(
3848  const exprt &expr,
3850  {
3851  DATA_CHECK(
3852  vm,
3853  expr.operands().size() == 1,
3854  "member expression must have one operand");
3855  }
3856 
3857  static void validate(
3858  const exprt &expr,
3859  const namespacet &ns,
3861 };
3862 
3863 template <>
3864 inline bool can_cast_expr<member_exprt>(const exprt &base)
3865 {
3866  return base.id() == ID_member;
3867 }
3868 
3869 inline void validate_expr(const member_exprt &value)
3870 {
3871  validate_operands(value, 1, "Extract member must have one operand");
3872 }
3873 
3880 inline const member_exprt &to_member_expr(const exprt &expr)
3881 {
3882  PRECONDITION(expr.id()==ID_member);
3883  const member_exprt &ret = static_cast<const member_exprt &>(expr);
3884  validate_expr(ret);
3885  return ret;
3886 }
3887 
3890 {
3891  PRECONDITION(expr.id()==ID_member);
3892  member_exprt &ret = static_cast<member_exprt &>(expr);
3893  validate_expr(ret);
3894  return ret;
3895 }
3896 
3897 
3900 {
3901 public:
3903  : unary_predicate_exprt(ID_isnan, std::move(op))
3904  {
3905  }
3906 
3907  DEPRECATED(SINCE(2018, 12, 2, "use isnan_exprt(op) instead"))
3909  {
3910  }
3911 };
3912 
3913 template <>
3914 inline bool can_cast_expr<isnan_exprt>(const exprt &base)
3915 {
3916  return base.id() == ID_isnan;
3917 }
3918 
3919 inline void validate_expr(const isnan_exprt &value)
3920 {
3921  validate_operands(value, 1, "Is NaN must have one operand");
3922 }
3923 
3930 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
3931 {
3932  PRECONDITION(expr.id()==ID_isnan);
3933  const isnan_exprt &ret = static_cast<const isnan_exprt &>(expr);
3934  validate_expr(ret);
3935  return ret;
3936 }
3937 
3940 {
3941  PRECONDITION(expr.id()==ID_isnan);
3942  isnan_exprt &ret = static_cast<isnan_exprt &>(expr);
3943  validate_expr(ret);
3944  return ret;
3945 }
3946 
3947 
3950 {
3951 public:
3953  : unary_predicate_exprt(ID_isinf, std::move(op))
3954  {
3955  }
3956 
3957  DEPRECATED(SINCE(2018, 12, 2, "use isinf_exprt(op) instead"))
3959  {
3960  }
3961 };
3962 
3963 template <>
3964 inline bool can_cast_expr<isinf_exprt>(const exprt &base)
3965 {
3966  return base.id() == ID_isinf;
3967 }
3968 
3969 inline void validate_expr(const isinf_exprt &value)
3970 {
3971  validate_operands(value, 1, "Is infinite must have one operand");
3972 }
3973 
3980 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
3981 {
3982  PRECONDITION(expr.id()==ID_isinf);
3983  const isinf_exprt &ret = static_cast<const isinf_exprt &>(expr);
3984  validate_expr(ret);
3985  return ret;
3986 }
3987 
3990 {
3991  PRECONDITION(expr.id()==ID_isinf);
3992  isinf_exprt &ret = static_cast<isinf_exprt &>(expr);
3993  validate_expr(ret);
3994  return ret;
3995 }
3996 
3997 
4000 {
4001 public:
4003  : unary_predicate_exprt(ID_isfinite, std::move(op))
4004  {
4005  }
4006 
4007  DEPRECATED(SINCE(2018, 12, 2, "use isfinite_exprt(op) instead"))
4009  {
4010  }
4011 };
4012 
4013 template <>
4014 inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
4015 {
4016  return base.id() == ID_isfinite;
4017 }
4018 
4019 inline void validate_expr(const isfinite_exprt &value)
4020 {
4021  validate_operands(value, 1, "Is finite must have one operand");
4022 }
4023 
4030 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
4031 {
4032  PRECONDITION(expr.id()==ID_isfinite);
4033  const isfinite_exprt &ret = static_cast<const isfinite_exprt &>(expr);
4034  validate_expr(ret);
4035  return ret;
4036 }
4037 
4040 {
4041  PRECONDITION(expr.id()==ID_isfinite);
4042  isfinite_exprt &ret = static_cast<isfinite_exprt &>(expr);
4043  validate_expr(ret);
4044  return ret;
4045 }
4046 
4047 
4050 {
4051 public:
4053  : unary_predicate_exprt(ID_isnormal, std::move(op))
4054  {
4055  }
4056 
4057  DEPRECATED(SINCE(2018, 12, 2, "use isnormal_exprt(op) instead"))
4059  {
4060  }
4061 };
4062 
4063 template <>
4064 inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
4065 {
4066  return base.id() == ID_isnormal;
4067 }
4068 
4069 inline void validate_expr(const isnormal_exprt &value)
4070 {
4071  validate_operands(value, 1, "Is normal must have one operand");
4072 }
4073 
4080 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
4081 {
4082  PRECONDITION(expr.id()==ID_isnormal);
4083  const isnormal_exprt &ret = static_cast<const isnormal_exprt &>(expr);
4084  validate_expr(ret);
4085  return ret;
4086 }
4087 
4090 {
4091  PRECONDITION(expr.id()==ID_isnormal);
4092  isnormal_exprt &ret = static_cast<isnormal_exprt &>(expr);
4093  validate_expr(ret);
4094  return ret;
4095 }
4096 
4097 
4100 {
4101 public:
4102  DEPRECATED(SINCE(2018, 12, 2, "use ieee_float_equal_exprt(lhs, rhs) instead"))
4104  {
4105  }
4106 
4109  std::move(_lhs),
4110  ID_ieee_float_equal,
4111  std::move(_rhs))
4112  {
4113  }
4114 };
4115 
4116 template <>
4118 {
4119  return base.id() == ID_ieee_float_equal;
4120 }
4121 
4122 inline void validate_expr(const ieee_float_equal_exprt &value)
4123 {
4124  validate_operands(value, 2, "IEEE equality must have two operands");
4125 }
4126 
4134 {
4135  PRECONDITION(expr.id()==ID_ieee_float_equal);
4136  const ieee_float_equal_exprt &ret =
4137  static_cast<const ieee_float_equal_exprt &>(expr);
4138  validate_expr(ret);
4139  return ret;
4140 }
4141 
4144 {
4145  PRECONDITION(expr.id()==ID_ieee_float_equal);
4146  ieee_float_equal_exprt &ret = static_cast<ieee_float_equal_exprt &>(expr);
4147  validate_expr(ret);
4148  return ret;
4149 }
4150 
4151 
4154 {
4155 public:
4156  DEPRECATED(
4157  SINCE(2018, 12, 2, "use ieee_float_notequal_exprt(lhs, rhs) instead"))
4159  binary_relation_exprt(ID_ieee_float_notequal)
4160  {
4161  }
4162 
4165  std::move(_lhs),
4166  ID_ieee_float_notequal,
4167  std::move(_rhs))
4168  {
4169  }
4170 };
4171 
4172 template <>
4174 {
4175  return base.id() == ID_ieee_float_notequal;
4176 }
4177 
4178 inline void validate_expr(const ieee_float_notequal_exprt &value)
4179 {
4180  validate_operands(value, 2, "IEEE inequality must have two operands");
4181 }
4182 
4190  const exprt &expr)
4191 {
4192  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4193  const ieee_float_notequal_exprt &ret =
4194  static_cast<const ieee_float_notequal_exprt &>(expr);
4195  validate_expr(ret);
4196  return ret;
4197 }
4198 
4201 {
4202  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4204  static_cast<ieee_float_notequal_exprt &>(expr);
4205  validate_expr(ret);
4206  return ret;
4207 }
4208 
4213 {
4214 public:
4216  const exprt &_lhs,
4217  const irep_idt &_id,
4218  exprt _rhs,
4219  exprt _rm)
4220  : ternary_exprt(_id, _lhs, std::move(_rhs), std::move(_rm), _lhs.type())
4221  {
4222  }
4223 
4225  {
4226  return op0();
4227  }
4228 
4229  const exprt &lhs() const
4230  {
4231  return op0();
4232  }
4233 
4235  {
4236  return op1();
4237  }
4238 
4239  const exprt &rhs() const
4240  {
4241  return op1();
4242  }
4243 
4245  {
4246  return op2();
4247  }
4248 
4249  const exprt &rounding_mode() const
4250  {
4251  return op2();
4252  }
4253 };
4254 
4255 template <>
4257 {
4258  return base.id() == ID_floatbv_plus || base.id() == ID_floatbv_minus ||
4259  base.id() == ID_floatbv_div || base.id() == ID_floatbv_mult;
4260 }
4261 
4262 inline void validate_expr(const ieee_float_op_exprt &value)
4263 {
4265  value, 3, "IEEE float operations must have three arguments");
4266 }
4267 
4275 {
4276  const ieee_float_op_exprt &ret =
4277  static_cast<const ieee_float_op_exprt &>(expr);
4278  validate_expr(ret);
4279  return ret;
4280 }
4281 
4284 {
4285  ieee_float_op_exprt &ret = static_cast<ieee_float_op_exprt &>(expr);
4286  validate_expr(ret);
4287  return ret;
4288 }
4289 
4290 
4293 {
4294 public:
4295  DEPRECATED(SINCE(2018, 9, 21, "use type_exprt(type) instead"))
4297  {
4298  }
4299 
4300  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
4301  {
4302  }
4303 };
4304 
4307 {
4308 public:
4309  DEPRECATED(SINCE(2018, 9, 21, "use constant_exprt(value, type) instead"))
4311  {
4312  }
4313 
4314  DEPRECATED(SINCE(2018, 9, 21, "use constant_exprt(value, type) instead"))
4315  explicit constant_exprt(const typet &type)
4316  : expr_protectedt(ID_constant, type)
4317  {
4318  }
4319 
4320  constant_exprt(const irep_idt &_value, typet _type)
4321  : expr_protectedt(ID_constant, std::move(_type))
4322  {
4323  set_value(_value);
4324  }
4325 
4326  const irep_idt &get_value() const
4327  {
4328  return get(ID_value);
4329  }
4330 
4331  void set_value(const irep_idt &value)
4332  {
4333  set(ID_value, value);
4334  }
4335 
4336  bool value_is_zero_string() const;
4337 };
4338 
4339 template <>
4340 inline bool can_cast_expr<constant_exprt>(const exprt &base)
4341 {
4342  return base.id() == ID_constant;
4343 }
4344 
4351 inline const constant_exprt &to_constant_expr(const exprt &expr)
4352 {
4353  PRECONDITION(expr.id()==ID_constant);
4354  return static_cast<const constant_exprt &>(expr);
4355 }
4356 
4359 {
4360  PRECONDITION(expr.id()==ID_constant);
4361  return static_cast<constant_exprt &>(expr);
4362 }
4363 
4364 
4367 {
4368 public:
4370  {
4371  }
4372 };
4373 
4376 {
4377 public:
4379  {
4380  }
4381 };
4382 
4384 class nil_exprt : public nullary_exprt
4385 {
4386 public:
4388  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
4389  {
4390  }
4391 };
4392 
4395 {
4396 public:
4398  : constant_exprt(ID_NULL, std::move(type))
4399  {
4400  }
4401 };
4402 
4405 {
4406 public:
4407  DEPRECATED(SINCE(2018, 9, 21, "use replication_exprt(times, value) instead"))
4408  replication_exprt() : binary_exprt(ID_replication)
4409  {
4410  }
4411 
4412  DEPRECATED(SINCE(2018, 9, 21, "use replication_exprt(times, value) instead"))
4413  explicit replication_exprt(const typet &_type)
4414  : binary_exprt(ID_replication, _type)
4415  {
4416  }
4417 
4418  replication_exprt(const constant_exprt &_times, const exprt &_src)
4419  : binary_exprt(_times, ID_replication, _src)
4420  {
4421  }
4422 
4424  {
4425  return static_cast<constant_exprt &>(op0());
4426  }
4427 
4428  const constant_exprt &times() const
4429  {
4430  return static_cast<const constant_exprt &>(op0());
4431  }
4432 
4434  {
4435  return op1();
4436  }
4437 
4438  const exprt &op() const
4439  {
4440  return op1();
4441  }
4442 };
4443 
4444 template <>
4445 inline bool can_cast_expr<replication_exprt>(const exprt &base)
4446 {
4447  return base.id() == ID_replication;
4448 }
4449 
4450 inline void validate_expr(const replication_exprt &value)
4451 {
4452  validate_operands(value, 2, "Bit-wise replication must have two operands");
4453 }
4454 
4461 inline const replication_exprt &to_replication_expr(const exprt &expr)
4462 {
4463  PRECONDITION(expr.id() == ID_replication);
4464  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
4465  validate_expr(ret);
4466  return ret;
4467 }
4468 
4471 {
4472  PRECONDITION(expr.id() == ID_replication);
4473  replication_exprt &ret = static_cast<replication_exprt &>(expr);
4474  validate_expr(ret);
4475  return ret;
4476 }
4477 
4484 {
4485 public:
4486  DEPRECATED(SINCE(2018, 9, 21, "use concatenation_exprt(op, type) instead"))
4487  concatenation_exprt() : multi_ary_exprt(ID_concatenation)
4488  {
4489  }
4490 
4491  DEPRECATED(SINCE(2018, 9, 21, "use concatenation_exprt(op, type) instead"))
4492  explicit concatenation_exprt(const typet &_type)
4493  : multi_ary_exprt(ID_concatenation, _type)
4494  {
4495  }
4496 
4498  : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
4499  {
4500  }
4501 
4503  : multi_ary_exprt(
4504  ID_concatenation,
4505  {std::move(_op0), std::move(_op1)},
4506  std::move(_type))
4507  {
4508  }
4509 };
4510 
4511 template <>
4513 {
4514  return base.id() == ID_concatenation;
4515 }
4516 
4524 {
4525  PRECONDITION(expr.id()==ID_concatenation);
4526  return static_cast<const concatenation_exprt &>(expr);
4527 }
4528 
4531 {
4532  PRECONDITION(expr.id()==ID_concatenation);
4533  return static_cast<concatenation_exprt &>(expr);
4534 }
4535 
4536 
4539 {
4540 public:
4541  explicit infinity_exprt(typet _type)
4542  : nullary_exprt(ID_infinity, std::move(_type))
4543  {
4544  }
4545 };
4546 
4548 class let_exprt : public ternary_exprt
4549 {
4550 public:
4552  : ternary_exprt(
4553  ID_let,
4554  std::move(symbol),
4555  std::move(value),
4556  where,
4557  where.type())
4558  {
4559  }
4560 
4562  {
4563  return static_cast<symbol_exprt &>(op0());
4564  }
4565 
4566  const symbol_exprt &symbol() const
4567  {
4568  return static_cast<const symbol_exprt &>(op0());
4569  }
4570 
4572  {
4573  return op1();
4574  }
4575 
4576  const exprt &value() const
4577  {
4578  return op1();
4579  }
4580 
4582  {
4583  return op2();
4584  }
4585 
4586  const exprt &where() const
4587  {
4588  return op2();
4589  }
4590 };
4591 
4592 template <>
4593 inline bool can_cast_expr<let_exprt>(const exprt &base)
4594 {
4595  return base.id() == ID_let;
4596 }
4597 
4598 inline void validate_expr(const let_exprt &value)
4599 {
4600  validate_operands(value, 3, "Let must have three operands");
4601 }
4602 
4609 inline const let_exprt &to_let_expr(const exprt &expr)
4610 {
4611  PRECONDITION(expr.id()==ID_let);
4612  const let_exprt &ret = static_cast<const let_exprt &>(expr);
4613  validate_expr(ret);
4614  return ret;
4615 }
4616 
4619 {
4620  PRECONDITION(expr.id()==ID_let);
4621  let_exprt &ret = static_cast<let_exprt &>(expr);
4622  validate_expr(ret);
4623  return ret;
4624 }
4625 
4628 {
4629 public:
4630  DEPRECATED(SINCE(2018, 9, 21, "use popcount_exprt(op, type) instead"))
4631  popcount_exprt(): unary_exprt(ID_popcount)
4632  {
4633  }
4634 
4636  : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
4637  {
4638  }
4639 
4640  explicit popcount_exprt(const exprt &_op)
4641  : unary_exprt(ID_popcount, _op, _op.type())
4642  {
4643  }
4644 };
4645 
4646 template <>
4647 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
4648 {
4649  return base.id() == ID_popcount;
4650 }
4651 
4652 inline void validate_expr(const popcount_exprt &value)
4653 {
4654  validate_operands(value, 1, "popcount must have one operand");
4655 }
4656 
4663 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
4664 {
4665  PRECONDITION(expr.id() == ID_popcount);
4666  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
4667  validate_expr(ret);
4668  return ret;
4669 }
4670 
4673 {
4674  PRECONDITION(expr.id() == ID_popcount);
4675  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
4676  validate_expr(ret);
4677  return ret;
4678 }
4679 
4684 {
4685 public:
4686  DEPRECATED(SINCE(2019, 1, 12, "use cond_exprt(operands, type) instead"))
4687  explicit cond_exprt(const typet &_type) : multi_ary_exprt(ID_cond, _type)
4688  {
4689  }
4690 
4691  cond_exprt(operandst _operands, typet _type)
4692  : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
4693  {
4694  }
4695 
4699  void add_case(const exprt &condition, const exprt &value)
4700  {
4701  PRECONDITION(condition.type().id() == ID_bool);
4702  operands().reserve(operands().size() + 2);
4703  operands().push_back(condition);
4704  operands().push_back(value);
4705  }
4706 };
4707 
4708 template <>
4709 inline bool can_cast_expr<cond_exprt>(const exprt &base)
4710 {
4711  return base.id() == ID_cond;
4712 }
4713 
4714 inline void validate_expr(const cond_exprt &value)
4715 {
4717  value.operands().size() % 2 == 0, "cond must have even number of operands");
4718 }
4719 
4726 inline const cond_exprt &to_cond_expr(const exprt &expr)
4727 {
4728  PRECONDITION(expr.id() == ID_cond);
4729  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
4730  validate_expr(ret);
4731  return ret;
4732 }
4733 
4736 {
4737  PRECONDITION(expr.id() == ID_cond);
4738  cond_exprt &ret = static_cast<cond_exprt &>(expr);
4739  validate_expr(ret);
4740  return ret;
4741 }
4742 
4743 #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:3395
bool can_cast_expr< rem_exprt >(const exprt &base)
Definition: std_expr.h:1353
const irept & get_nil_irep()
Definition: irep.cpp:51
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:205
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
Definition: std_expr.h:4133
const irep_idt & get_name() const
Definition: std_types.h:79
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:3668
bool can_cast_expr< bitxor_exprt >(const exprt &base)
Definition: std_expr.h:2735
The type of an expression, extends irept.
Definition: type.h:28
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2486
bool can_cast_expr< isnormal_exprt >(const exprt &base)
Definition: std_expr.h:4064
isnan_exprt(exprt op)
Definition: std_expr.h:3902
ashr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2934
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:463
Boolean negation.
Definition: std_expr.h:3187
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition: std_expr.h:815
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: std_expr.h:586
bitand_exprt(const exprt &_op0, exprt _op1)
Definition: std_expr.h:2769
const exprt & op1() const
Definition: std_expr.h:1005
exprt & true_case()
Definition: std_expr.h:3357
symbol_exprt(typet type)
Definition: std_expr.h:118
Semantic type conversion.
Definition: std_expr.h:2268
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:734
and_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2416
const exprt & rhs() const
Definition: std_expr.h:4239
bitnot_exprt(exprt op)
Definition: std_expr.h:2638
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1179
rem_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1346
An expression without operands.
Definition: std_expr.h:23
bool can_cast_expr< bitnot_exprt >(const exprt &base)
Definition: std_expr.h:2644
shl_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2886
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:636
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:842
const exprt & value() const
Definition: std_expr.h:4576
index_exprt(exprt _array, exprt _index, typet _type)
Definition: std_expr.h:1519
const exprt & lhs() const
Definition: std_expr.h:889
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
Definition: std_expr.h:2787
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1144
exprt & object()
Definition: std_expr.h:3140
array_list_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1711
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:262
bswap_exprt(exprt _op, std::size_t bits_per_byte)
Definition: std_expr.h:550
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2292
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1319
Boolean OR.
Definition: std_expr.h:2521
mult_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1172
exprt & op0()
Definition: expr.h:97
bitor_exprt(const exprt &_op0, exprt _op1)
Definition: std_expr.h:2687
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
exprt & op0()
Definition: std_expr.h:975
const exprt & src() const
Definition: std_expr.h:2987
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1269
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1094
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: std_expr.h:2247
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:749
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
Definition: std_expr.cpp:238
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition: std_expr.h:3332
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:689
Operator to update elements in structs and arrays.
Definition: std_expr.h:3606
const exprt & op() const
Definition: std_expr.h:342
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:523
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: std_expr.h:4512
const exprt & pointer() const
Definition: std_expr.h:3267
Evaluates to true if the operand is infinite.
Definition: std_expr.h:3949
const exprt & op() const
Definition: std_expr.h:4438
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1687
bool can_cast_expr< shift_exprt >(const exprt &base)
Definition: std_expr.h:2845
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:184
const exprt & op2() const
Definition: std_expr.h:1011
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3465
unsigned int get_instance() const
Definition: std_expr.cpp:45
exprt & struct_op()
Definition: std_expr.h:3832
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
Definition: std_expr.h:2746
concatenation_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4497
const exprt & real() const
Definition: std_expr.h:1966
const exprt & array() const
Definition: std_expr.h:1533
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: std_expr.h:2903
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1615
const irep_idt & get_identifier() const
Definition: std_expr.h:144
isfinite_exprt(exprt op)
Definition: std_expr.h:4002
exprt::operandst & designator()
Definition: std_expr.h:3646
exprt & lower()
Definition: std_expr.h:3073
shift_exprt(const irep_idt &_id)
Definition: std_expr.h:2806
const exprt & op3() const =delete
Base class for all expressions.
Definition: expr.h:348
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition: std_expr.h:3609
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:4699
exprt imag()
Definition: std_expr.h:1971
const irep_idt & get_value() const
Definition: std_expr.h:4326
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:2176
output_type narrow_cast(input_type value)
Alias for static_cast intended to be used for numeric casting Rationale: Easier to grep than static_c...
Definition: narrow.h:19
The null pointer constant.
Definition: std_expr.h:4394
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3272
An expression denoting a type.
Definition: std_expr.h:4292
array_of_exprt(exprt _what, array_typet _type)
Definition: std_expr.h:1588
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:3571
exprt & op3()
Definition: std_expr.h:993
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition: std_expr.h:337
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
Definition: std_expr.h:2705
const exprt & op1() const =delete
infinity_exprt(typet _type)
Definition: std_expr.h:4541
bool is_thread_local() const
Definition: std_expr.h:199
mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1296
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Definition: std_expr.h:2816
exprt real()
Definition: std_expr.h:1961
or_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2529
The trinary if-then-else operator.
Definition: std_expr.h:3324
exprt & cond()
Definition: std_expr.h:3347
std::size_t get_component_number() const
Definition: std_expr.h:3820
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:4049
exprt & old()
Definition: std_expr.h:3433
unary_plus_exprt(exprt op)
Definition: std_expr.h:500
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1246
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:2089
exprt & new_value()
Definition: std_expr.h:3453
typet & type()
Return the type of the expression.
Definition: expr.h:81
exprt & op2()
Definition: std_expr.h:987
bool can_cast_expr< extractbit_exprt >(const exprt &base)
Definition: std_expr.h:2999
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2574
bool can_cast_expr< bitand_exprt >(const exprt &base)
Definition: std_expr.h:2776
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:3168
const exprt & op2() const =delete
dereference_exprt(exprt op, typet type)
Definition: std_expr.h:3257
The Boolean type.
Definition: std_types.h:29
address_of_exprt(exprt op, pointer_typet _type)
Definition: std_expr.h:3135
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1734
plus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1057
const exprt & where() const
Definition: std_expr.h:3448
A constant literal expression.
Definition: std_expr.h:4306
exprt & distance()
Definition: std_expr.h:2833
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1303
exprt & rounding_mode()
Definition: std_expr.h:4244
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1240
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2445
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1234
replication_exprt(const constant_exprt &_times, const exprt &_src)
Definition: std_expr.h:4418
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:102
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:3522
const exprt & index() const
Definition: std_expr.h:1543
const exprt & op3() const =delete
const exprt & lower() const
Definition: std_expr.h:3088
unary_minus_exprt(exprt _op)
Definition: std_expr.h:456
const exprt & where() const
Definition: std_expr.h:4586
irep_idt get_component_name() const
Definition: std_expr.h:3564
Boolean implication.
Definition: std_expr.h:2471
bool value_is_zero_string() const
Definition: std_expr.cpp:22
array_typet & type()
Definition: std_expr.h:1721
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2062
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:673
void set_bits_per_byte(std::size_t bits_per_byte)
Definition: std_expr.h:561
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:4189
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4609
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1845
array_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1659
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3305
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Definition: std_expr.h:4117
Extract member of struct or union.
Definition: std_expr.h:3790
const exprt & imag() const
Definition: std_expr.h:1976
const exprt & rounding_mode() const
Definition: std_expr.h:2360
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:3202
exprt & where()
Definition: std_expr.h:4581
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
Concatenation of bit-vector operands.
Definition: std_expr.h:4483
Equality.
Definition: std_expr.h:1388
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1482
bool can_cast_expr< bitor_exprt >(const exprt &base)
Definition: std_expr.h:2694
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:1078
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1253
const exprt & op() const
Definition: std_expr.h:2828
Templated functions to cast to specific exprt-derived classes.
void add(exprt index, exprt value)
add an index/value pair
Definition: std_expr.h:1727
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2502
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3815
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:4274
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:50
const exprt & compound() const
Definition: std_expr.h:3837
exprt & op()
Definition: std_expr.h:347
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:729
dynamic_object_exprt(typet type)
Definition: std_expr.h:2206
implies_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2479
const exprt & src() const
Definition: std_expr.h:3078
const irep_idt & id() const
Definition: irep.h:413
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2542
if_exprt(exprt cond, const exprt &t, exprt f)
Definition: std_expr.h:3327
popcount_exprt(const exprt &_op)
Definition: std_expr.h:4640
const exprt & op2() const =delete
index_designatort(exprt _index)
Definition: std_expr.h:3505
The unary plus expression.
Definition: std_expr.h:497
void set_value(const irep_idt &value)
Definition: std_expr.h:4331
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3899
Bit-wise OR.
Definition: std_expr.h:2679
bool can_cast_expr< isnan_exprt >(const exprt &base)
Definition: std_expr.h:3914
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:4726
ieee_float_notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:4163
An expression denoting infinity.
Definition: std_expr.h:4538
cond_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4691
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:1128
ashr_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2929
The Boolean constant true.
Definition: std_expr.h:4366
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition: std_expr.h:152
Division.
Definition: std_expr.h:1214
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: std_expr.h:4461
A base class for binary expressions.
Definition: std_expr.h:707
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4523
exprt & old()
Definition: std_expr.h:3632
const exprt & distance() const
Definition: std_expr.h:2838
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
Definition: std_expr.h:4551
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3685
const irep_idt & get_identifier() const
Definition: std_expr.h:267
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1793
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3847
The NIL expression.
Definition: std_expr.h:4384
Real part of the expression describing a complex number.
Definition: std_expr.h:2017
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: std_expr.cpp:140
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:4153
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:3864
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:3015
and_exprt(exprt::operandst _operands)
Definition: std_expr.h:2432
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1408
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1782
div_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1222
const exprt & op3() const =delete
const exprt & op1() const =delete
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:2027
type_exprt(typet type)
Definition: std_expr.h:4300
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition: std_expr.h:1062
Operator to dereference a pointer.
Definition: std_expr.h:3237
operandst & operands()=delete
remove all operand methods
exprt & rounding_mode()
Definition: std_expr.h:2355
The vector type.
Definition: std_types.h:1742
const exprt & op0() const =delete
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:274
exprt & src()
Definition: std_expr.h:3063
const array_typet & type() const
Definition: std_expr.h:1664
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1631
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:1983
const constant_exprt & times() const
Definition: std_expr.h:4428
Union constructor from single element.
Definition: std_expr.h:1808
std::size_t get_component_number() const
Definition: std_expr.h:1840
Boolean AND.
Definition: std_expr.h:2403
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3034
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:768
const exprt & new_value() const
Definition: std_expr.h:3661
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: std_expr.h:3980
exprt & op1()
Definition: expr.h:100
equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1396
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1744
const exprt & lhs() const
Definition: std_expr.h:4229
Generic base class for unary expressions.
Definition: std_expr.h:310
Disequality.
Definition: std_expr.h:1451
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:2160
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:507
array_typet & type()
Definition: std_expr.h:1598
An expression with three operands.
Definition: std_expr.h:60
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1852
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:134
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:3111
Left shift.
Definition: std_expr.h:2878
const exprt & what() const
Definition: std_expr.h:1608
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:922
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:325
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const exprt & false_case() const
Definition: std_expr.h:3372
typecast_exprt(const typet &_type)
Definition: std_expr.h:2272
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3880
floatbv_typecast_exprt(exprt op, exprt rounding, typet _type)
Definition: std_expr.h:2336
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: std_expr.h:3095
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition: std_expr.h:4709
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2109
nullary_exprt(const irep_idt &_id, typet _type)
Definition: std_expr.h:32
const exprt & cond() const
Definition: std_expr.h:3352
The plus expression Associativity is not specified.
Definition: std_expr.h:1044
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
Definition: std_expr.h:2970
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:4340
const symbol_exprt & symbol() const
Definition: std_expr.h:4566
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
Definition: std_expr.h:2367
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:232
void set_static_lifetime()
Definition: std_expr.h:189
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition: std_expr.h:3418
Array constructor from single element.
Definition: std_expr.h:1585
array_typet & type()
Definition: std_expr.h:1669
exprt & upper()
Definition: std_expr.h:3068
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2604
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:28
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1401
const exprt & op0() const
Definition: std_expr.h:999
plus_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1071
and_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2411
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:408
Logical right shift.
Definition: std_expr.h:2941
exprt & compound()
Definition: std_expr.h:3842
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:3538
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:2072
Vector constructor from list of elements.
Definition: std_expr.h:1761
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:36
notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1459
const exprt & old() const
Definition: std_expr.h:3438
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
Definition: std_expr.h:3049
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: std_expr.h:4030
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:2563
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: std_expr.h:3289
Operator to return the address of an object.
Definition: std_expr.h:3130
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1923
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:963
The unary minus expression.
Definition: std_expr.h:443
exprt & false_case()
Definition: std_expr.h:3367
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: std_expr.h:2231
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4351
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:613
symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:124
const exprt & index() const
Definition: std_expr.h:3510
constant_exprt(const irep_idt &_value, typet _type)
Definition: std_expr.h:4320
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:3152
The Boolean constant false.
Definition: std_expr.h:4375
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:820
isinf_exprt(exprt op)
Definition: std_expr.h:3952
bool can_cast_expr< replication_exprt >(const exprt &base)
Definition: std_expr.h:4445
exprt & index()
Definition: std_expr.h:2982
const exprt & rhs() const
Definition: std_expr.h:899
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2383
void validate_expr(const symbol_exprt &value)
Definition: std_expr.h:221
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2282
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2615
const array_typet & type() const
Definition: std_expr.h:1716
std::vector< exprt > operandst
Definition: expr.h:55
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1164
const exprt::operandst & designator() const
Definition: std_expr.h:3651
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: std_expr.h:4173
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1466
typecast_exprt(exprt op, typet _type)
Definition: std_expr.h:2276
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1195
const exprt & object() const
Definition: std_expr.h:2141
Boolean XOR.
Definition: std_expr.h:2589
Complex numbers made of pair of given subtype.
Definition: std_types.h:1782
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4663
bitxor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2728
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3485
Bit-wise XOR.
Definition: std_expr.h:2720
const exprt & op3() const
Definition: std_expr.h:1017
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:1030
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:256
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1434
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:216
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:2065
xor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2597
Pre-defined types.
const exprt & op3() const =delete
popcount_exprt(exprt _op, typet _type)
Definition: std_expr.h:4635
const exprt & old() const
Definition: std_expr.h:3637
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs, exprt _rm)
Definition: std_expr.h:4215
const exprt & object() const
Definition: std_expr.h:3145
not_exprt(exprt _op)
Definition: std_expr.h:3190
unary_minus_exprt(exprt _op, typet _type)
Definition: std_expr.h:451
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: std_expr.h:3930
constant_exprt & times()
Definition: std_expr.h:4423
exprt & value()
Definition: std_expr.h:4571
Expression to hold a nondeterministic choice.
Definition: std_expr.h:251
lshr_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2949
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2861
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2456
or_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2534
exprt & index()
Definition: std_expr.h:1538
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4627
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
Definition: std_expr.h:1369
Evaluates to true if the operand is finite.
Definition: std_expr.h:3999
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2424
const exprt & index() const
Definition: std_expr.h:2992
exprt & op()
Definition: std_expr.h:2823
std::size_t get_bits_per_byte() const
Definition: std_expr.h:556
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2327
bool can_cast_expr< ieee_float_op_exprt >(const exprt &base)
Definition: std_expr.h:4256
Base class for all expressions.
Definition: expr.h:52
exprt & pointer()
Definition: std_expr.h:3262
Absolute value.
Definition: std_expr.h:394
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:658
const exprt & root_object() const
Definition: std_expr.cpp:217
const exprt & struct_op() const
Definition: std_expr.h:3826
const exprt & rounding_mode() const
Definition: std_expr.h:4249
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:906
dereference_exprt(const exprt &op)
Definition: std_expr.h:3251
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition: std_expr.h:79
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1999
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
Definition: std_expr.h:544
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
Definition: std_expr.h:4502
complex_real_exprt(const exprt &op)
Definition: std_expr.h:2020
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1868
const exprt & op2() const =delete
Operator to update elements in structs and arrays.
Definition: std_expr.h:3415
const exprt & upper() const
Definition: std_expr.h:3083
exprt & op1()
Definition: std_expr.h:981
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:863
member_exprt(exprt op, const struct_typet::componentt &c)
Definition: std_expr.h:3799
irep_idt get_component_name() const
Definition: std_expr.h:3810
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition: std_expr.h:3793
const exprt & offset() const
Definition: std_expr.h:2153
minus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1121
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2308
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:858
abs_exprt(exprt _op)
Definition: std_expr.h:402
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:4593
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3218
Remainder of division.
Definition: std_expr.h:1338
const exprt & valid() const
Definition: std_expr.h:2224
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1813
const exprt & true_case() const
Definition: std_expr.h:3362
exprt & index()
Definition: std_expr.h:3515
vector_exprt(operandst _operands, vector_typet _type)
Definition: std_expr.h:1775
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:139
#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:4433
irep_idt get_component_name() const
Definition: std_expr.h:1830
index_exprt(const exprt &_array, exprt _index)
Definition: std_expr.h:1514
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:361
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1835
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:424
sign_exprt(exprt _op)
Definition: std_expr.h:666
bool is_static_lifetime() const
Definition: std_expr.h:184
Arrays with given size.
Definition: std_types.h:976
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:179
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition: std_expr.h:650
bool can_cast_expr< bswap_exprt >(const exprt &base)
Definition: std_expr.h:568
Binary minus.
Definition: std_expr.h:1113
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:739
Bit-wise AND.
Definition: std_expr.h:2761
validation_modet
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition: std_expr.h:957
Expression to hold a symbol (variable)
Definition: std_expr.h:102
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: std_expr.h:3964
exprt & what()
Definition: std_expr.h:1603
exprt & op2()
Definition: expr.h:103
isnormal_exprt(exprt op)
Definition: std_expr.h:4052
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:827
bool can_cast_expr< isfinite_exprt >(const exprt &base)
Definition: std_expr.h:4014
exprt & new_value()
Definition: std_expr.h:3656
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1912
symbol_exprt & symbol()
Definition: std_expr.h:4561
object_descriptor_exprt(exprt _object)
Definition: std_expr.h:2121
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:784
shl_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2891
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:799
lshr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2954
Arithmetic right shift.
Definition: std_expr.h:2921
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition: std_expr.h:1952
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1550
exprt & where()
Definition: std_expr.h:3443
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: std_expr.h:2660
A let expression.
Definition: std_expr.h:4548
or_exprt(exprt::operandst _operands)
Definition: std_expr.h:2550
void clear_static_lifetime()
Definition: std_expr.h:194
struct_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1902
#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:1228
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: std_expr.h:4080
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
Definition: std_expr.cpp:278
Representation of heap-allocated objects.
Definition: std_expr.h:2197
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:290
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:938
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:377
operandst & operands()
Definition: expr.h:91
void copy_to_operands(const exprt &expr)=delete
exprt & src()
Definition: std_expr.h:2977
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2630
Struct constructor from list of elements.
Definition: std_expr.h:1887
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:968
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:3379
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:112
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:2044
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:4212
Bit-vector replication.
Definition: std_expr.h:4404
exprt & array()
Definition: std_expr.h:1528
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:1566
A base class for shift operators.
Definition: std_expr.h:2802
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt&#39;s operands.
Definition: expr.h:151
Array constructor from list of elements.
Definition: std_expr.h:1650
Complex constructor from a pair of numbers.
Definition: std_expr.h:1938
Modulo.
Definition: std_expr.h:1288
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1676
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
The byte swap expression.
Definition: std_expr.h:541
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:479
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:3558
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: std_expr.h:4647
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:870
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
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:3587
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:4683
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2961
ieee_float_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:4107
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:605
IEEE-floating-point equality.
Definition: std_expr.h:4099
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1418
null_pointer_exprt(pointer_typet type)
Definition: std_expr.h:4397
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition: std_expr.h:1824
Array index operator.
Definition: std_expr.h:1501
const array_typet & type() const
Definition: std_expr.h:1593
const exprt & new_value() const
Definition: std_expr.h:3458
const exprt & op() const
Definition: std_expr.h:2350