cprover
std_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_STD_EXPR_H
11 #define CPROVER_UTIL_STD_EXPR_H
12 
15 
16 #include "base_type.h"
17 #include "expr_cast.h"
18 #include "invariant.h"
19 #include "mathematical_types.h"
20 #include "std_types.h"
21 
23 class nullary_exprt : public exprt
24 {
25 public:
26  // constructors
27  DEPRECATED("use nullary_exprt(id, type) instead")
28  explicit nullary_exprt(const irep_idt &_id) : exprt(_id)
29  {
30  }
31 
32  nullary_exprt(const irep_idt &_id, const typet &_type) : exprt(_id, _type)
33  {
34  }
35 
37  operandst &operands() = delete;
38  const operandst &operands() const = delete;
39 
40  const exprt &op0() const = delete;
41  exprt &op0() = delete;
42  const exprt &op1() const = delete;
43  exprt &op1() = delete;
44  const exprt &op2() const = delete;
45  exprt &op2() = delete;
46  const exprt &op3() const = delete;
47  exprt &op3() = delete;
48 
49  void move_to_operands(exprt &) = delete;
50  void move_to_operands(exprt &, exprt &) = delete;
51  void move_to_operands(exprt &, exprt &, exprt &) = delete;
52 
53  void copy_to_operands(const exprt &expr) = delete;
54  void copy_to_operands(const exprt &, const exprt &) = delete;
55  void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
56 };
57 
59 class ternary_exprt : public exprt
60 {
61 public:
62  // constructors
63  DEPRECATED("use ternary_exprt(id, op0, op1, op2, type) instead")
64  explicit ternary_exprt(const irep_idt &_id) : exprt(_id)
65  {
66  operands().resize(3);
67  }
68 
69  DEPRECATED("use ternary_exprt(id, op0, op1, op2, type) instead")
70  explicit ternary_exprt(const irep_idt &_id, const typet &_type)
71  : exprt(_id, _type)
72  {
73  operands().resize(3);
74  }
75 
77  const irep_idt &_id,
78  const exprt &_op0,
79  const exprt &_op1,
80  const exprt &_op2,
81  const typet &_type)
82  : exprt(_id, _type)
83  {
84  add_to_operands(_op0, _op1, _op2);
85  }
86 
87  const exprt &op3() const = delete;
88  exprt &op3() = delete;
89 };
90 
93 class transt : public ternary_exprt
94 {
95 public:
96  transt() : ternary_exprt(ID_trans)
97  {
98  }
99 
100  exprt &invar() { return op0(); }
101  exprt &init() { return op1(); }
102  exprt &trans() { return op2(); }
103 
104  const exprt &invar() const { return op0(); }
105  const exprt &init() const { return op1(); }
106  const exprt &trans() const { return op2(); }
107 };
108 
113 inline const transt &to_trans_expr(const exprt &expr)
114 {
115  PRECONDITION(expr.id()==ID_trans);
117  expr.operands().size()==3,
118  "Transition systems must have three operands");
119  return static_cast<const transt &>(expr);
120 }
121 
123 inline transt &to_trans_expr(exprt &expr)
124 {
125  PRECONDITION(expr.id()==ID_trans);
127  expr.operands().size()==3,
128  "Transition systems must have three operands");
129  return static_cast<transt &>(expr);
130 }
131 
132 template<> inline bool can_cast_expr<transt>(const exprt &base)
133 {
134  return base.id()==ID_trans;
135 }
136 inline void validate_expr(const transt &value)
137 {
138  validate_operands(value, 3, "Transition systems must have three operands");
139 }
140 
141 
144 {
145 public:
146  DEPRECATED("use symbol_exprt(identifier, type) instead")
148  {
149  }
150 
152  DEPRECATED("use symbol_exprt(identifier, type) instead")
153  explicit symbol_exprt(const irep_idt &identifier) : nullary_exprt(ID_symbol)
154  {
155  set_identifier(identifier);
156  }
157 
159  explicit symbol_exprt(const typet &type) : nullary_exprt(ID_symbol, type)
160  {
161  }
162 
165  symbol_exprt(const irep_idt &identifier, const typet &type)
166  : nullary_exprt(ID_symbol, type)
167  {
168  set_identifier(identifier);
169  }
170 
171  void set_identifier(const irep_idt &identifier)
172  {
173  set(ID_identifier, identifier);
174  }
175 
176  const irep_idt &get_identifier() const
177  {
178  return get(ID_identifier);
179  }
180 };
181 
185 {
186 public:
187  DEPRECATED("use decorated_symbol_exprt(identifier, type) instead")
189  {
190  }
191 
193  DEPRECATED("use decorated_symbol_exprt(identifier, type) instead")
194  explicit decorated_symbol_exprt(const irep_idt &identifier):
195  symbol_exprt(identifier)
196  {
197  }
198 
200  DEPRECATED("use decorated_symbol_exprt(identifier, type) instead")
203  {
204  }
205 
209  const irep_idt &identifier,
210  const typet &type):symbol_exprt(identifier, type)
211  {
212  }
213 
214  bool is_static_lifetime() const
215  {
216  return get_bool(ID_C_static_lifetime);
217  }
218 
220  {
221  return set(ID_C_static_lifetime, true);
222  }
223 
225  {
226  remove(ID_C_static_lifetime);
227  }
228 
229  bool is_thread_local() const
230  {
231  return get_bool(ID_C_thread_local);
232  }
233 
235  {
236  return set(ID_C_thread_local, true);
237  }
238 
240  {
241  remove(ID_C_thread_local);
242  }
243 };
244 
251 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
252 {
253  PRECONDITION(expr.id()==ID_symbol);
254  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
255  return static_cast<const symbol_exprt &>(expr);
256 }
257 
260 {
261  PRECONDITION(expr.id()==ID_symbol);
262  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
263  return static_cast<symbol_exprt &>(expr);
264 }
265 
266 template<> inline bool can_cast_expr<symbol_exprt>(const exprt &base)
267 {
268  return base.id()==ID_symbol;
269 }
270 inline void validate_expr(const symbol_exprt &value)
271 {
272  validate_operands(value, 0, "Symbols must not have operands");
273 }
274 
275 
278 {
279 public:
282  nondet_symbol_exprt(const irep_idt &identifier, const typet &type)
283  : nullary_exprt(ID_nondet_symbol, type)
284  {
285  set_identifier(identifier);
286  }
287 
288  void set_identifier(const irep_idt &identifier)
289  {
290  set(ID_identifier, identifier);
291  }
292 
293  const irep_idt &get_identifier() const
294  {
295  return get(ID_identifier);
296  }
297 };
298 
306 {
307  PRECONDITION(expr.id()==ID_nondet_symbol);
308  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
309  return static_cast<const nondet_symbol_exprt &>(expr);
310 }
311 
314 {
315  PRECONDITION(expr.id()==ID_symbol);
316  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
317  return static_cast<nondet_symbol_exprt &>(expr);
318 }
319 
320 template<> inline bool can_cast_expr<nondet_symbol_exprt>(const exprt &base)
321 {
322  return base.id()==ID_nondet_symbol;
323 }
324 inline void validate_expr(const nondet_symbol_exprt &value)
325 {
326  validate_operands(value, 0, "Symbols must not have operands");
327 }
328 
329 
331 class unary_exprt:public exprt
332 {
333 public:
334  DEPRECATED("use unary_exprt(id, op) instead")
336  {
337  operands().resize(1);
338  }
339 
340  DEPRECATED("use unary_exprt(id, op) instead")
341  explicit unary_exprt(const irep_idt &_id):exprt(_id)
342  {
343  operands().resize(1);
344  }
345 
347  const irep_idt &_id,
348  const exprt &_op):
349  exprt(_id, _op.type())
350  {
351  add_to_operands(_op);
352  }
353 
354  DEPRECATED("use unary_exprt(id, op, type) instead")
356  const irep_idt &_id,
357  const typet &_type):exprt(_id, _type)
358  {
359  operands().resize(1);
360  }
361 
363  const irep_idt &_id,
364  const exprt &_op,
365  const typet &_type):
366  exprt(_id, _type)
367  {
368  add_to_operands(_op);
369  }
370 
371  const exprt &op() const
372  {
373  return op0();
374  }
375 
377  {
378  return op0();
379  }
380 
381  const exprt &op1() const = delete;
382  exprt &op1() = delete;
383  const exprt &op2() const = delete;
384  exprt &op2() = delete;
385  const exprt &op3() const = delete;
386  exprt &op3() = delete;
387 };
388 
395 inline const unary_exprt &to_unary_expr(const exprt &expr)
396 {
398  expr.operands().size()==1,
399  "Unary expressions must have one operand");
400  return static_cast<const unary_exprt &>(expr);
401 }
402 
405 {
407  expr.operands().size()==1,
408  "Unary expressions must have one operand");
409  return static_cast<unary_exprt &>(expr);
410 }
411 
412 template<> inline bool can_cast_expr<unary_exprt>(const exprt &base)
413 {
414  return base.operands().size()==1;
415 }
416 
417 
419 class abs_exprt:public unary_exprt
420 {
421 public:
422  DEPRECATED("use abs_exprt(op) instead")
424  {
425  }
426 
427  explicit abs_exprt(const exprt &_op):
428  unary_exprt(ID_abs, _op, _op.type())
429  {
430  }
431 };
432 
439 inline const abs_exprt &to_abs_expr(const exprt &expr)
440 {
441  PRECONDITION(expr.id()==ID_abs);
443  expr.operands().size()==1,
444  "Absolute value must have one operand");
445  return static_cast<const abs_exprt &>(expr);
446 }
447 
450 {
451  PRECONDITION(expr.id()==ID_abs);
453  expr.operands().size()==1,
454  "Absolute value must have one operand");
455  return static_cast<abs_exprt &>(expr);
456 }
457 
458 template<> inline bool can_cast_expr<abs_exprt>(const exprt &base)
459 {
460  return base.id()==ID_abs;
461 }
462 inline void validate_expr(const abs_exprt &value)
463 {
464  validate_operands(value, 1, "Absolute value must have one operand");
465 }
466 
467 
470 {
471 public:
472  DEPRECATED("use unary_minus_exprt(op) instead")
473  unary_minus_exprt():unary_exprt(ID_unary_minus)
474  {
475  }
476 
478  const exprt &_op,
479  const typet &_type):
480  unary_exprt(ID_unary_minus, _op, _type)
481  {
482  }
483 
484  explicit unary_minus_exprt(const exprt &_op):
485  unary_exprt(ID_unary_minus, _op, _op.type())
486  {
487  }
488 };
489 
496 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
497 {
498  PRECONDITION(expr.id()==ID_unary_minus);
500  expr.operands().size()==1,
501  "Unary minus must have one operand");
502  return static_cast<const unary_minus_exprt &>(expr);
503 }
504 
507 {
508  PRECONDITION(expr.id()==ID_unary_minus);
510  expr.operands().size()==1,
511  "Unary minus must have one operand");
512  return static_cast<unary_minus_exprt &>(expr);
513 }
514 
515 template<> inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
516 {
517  return base.id()==ID_unary_minus;
518 }
519 inline void validate_expr(const unary_minus_exprt &value)
520 {
521  validate_operands(value, 1, "Unary minus must have one operand");
522 }
523 
526 {
527 public:
528  explicit unary_plus_exprt(const exprt &op)
529  : unary_exprt(ID_unary_plus, op, op.type())
530  {
531  }
532 };
533 
540 inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
541 {
542  PRECONDITION(expr.id() == ID_unary_plus);
544  expr.operands().size() == 1, "unary plus must have one operand");
545  return static_cast<const unary_plus_exprt &>(expr);
546 }
547 
550 {
551  PRECONDITION(expr.id() == ID_unary_plus);
553  expr.operands().size() == 1, "unary plus must have one operand");
554  return static_cast<unary_plus_exprt &>(expr);
555 }
556 
557 template <>
558 inline bool can_cast_expr<unary_plus_exprt>(const exprt &base)
559 {
560  return base.id() == ID_unary_plus;
561 }
562 inline void validate_expr(const unary_plus_exprt &value)
563 {
564  validate_operands(value, 1, "unary plus must have one operand");
565 }
566 
569 {
570 public:
571  bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
572  : unary_exprt(ID_bswap, _op, _type)
573  {
574  set_bits_per_byte(bits_per_byte);
575  }
576 
577  bswap_exprt(const exprt &_op, std::size_t bits_per_byte)
578  : unary_exprt(ID_bswap, _op, _op.type())
579  {
580  set_bits_per_byte(bits_per_byte);
581  }
582 
583  std::size_t get_bits_per_byte() const
584  {
585  return get_size_t(ID_bits_per_byte);
586  }
587 
588  void set_bits_per_byte(std::size_t bits_per_byte)
589  {
590  set(ID_bits_per_byte, bits_per_byte);
591  }
592 };
593 
600 inline const bswap_exprt &to_bswap_expr(const exprt &expr)
601 {
602  PRECONDITION(expr.id() == ID_bswap);
603  DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand");
605  expr.op0().type() == expr.type(), "bswap type must match operand type");
606  return static_cast<const bswap_exprt &>(expr);
607 }
608 
611 {
612  PRECONDITION(expr.id() == ID_bswap);
613  DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand");
615  expr.op0().type() == expr.type(), "bswap type must match operand type");
616  return static_cast<bswap_exprt &>(expr);
617 }
618 
619 template <>
620 inline bool can_cast_expr<bswap_exprt>(const exprt &base)
621 {
622  return base.id() == ID_bswap;
623 }
624 inline void validate_expr(const bswap_exprt &value)
625 {
626  validate_operands(value, 1, "bswap must have one operand");
628  value.op().type() == value.type(), "bswap type must match operand type");
629 }
630 
633 class predicate_exprt:public exprt
634 {
635 public:
636  DEPRECATED("use predicate_exprt(id) instead")
638  {
639  }
640 
641  explicit predicate_exprt(const irep_idt &_id):
642  exprt(_id, bool_typet())
643  {
644  }
645 
646  DEPRECATED("use unary_predicate_exprt(id, op) instead")
648  const irep_idt &_id,
649  const exprt &_op):exprt(_id, bool_typet())
650  {
651  add_to_operands(_op);
652  }
653 
654  DEPRECATED("use binary_predicate_exprt(op1, id, op2) instead")
656  const irep_idt &_id,
657  const exprt &_op0,
658  const exprt &_op1):exprt(_id, bool_typet())
659  {
660  add_to_operands(_op0, _op1);
661  }
662 };
663 
667 {
668 public:
669  DEPRECATED("use unary_predicate_exprt(id, op) instead")
671  {
672  }
673 
674  DEPRECATED("use unary_predicate_exprt(id, op) instead")
675  explicit unary_predicate_exprt(const irep_idt &_id):
676  unary_exprt(_id, bool_typet())
677  {
678  }
679 
681  const irep_idt &_id,
682  const exprt &_op):unary_exprt(_id, _op, bool_typet())
683  {
684  }
685 
686 };
687 
691 {
692 public:
693  DEPRECATED("use sign_exprt(op) instead")
695  {
696  }
697 
698  explicit sign_exprt(const exprt &_op):
699  unary_predicate_exprt(ID_sign, _op)
700  {
701  }
702 };
703 
710 inline const sign_exprt &to_sign_expr(const exprt &expr)
711 {
712  PRECONDITION(expr.id() == ID_sign);
714  expr.operands().size() == 1, "sign expression must have one operand");
715  return static_cast<const sign_exprt &>(expr);
716 }
717 
720 {
721  PRECONDITION(expr.id() == ID_sign);
723  expr.operands().size() == 1, "sign expression must have one operand");
724  return static_cast<sign_exprt &>(expr);
725 }
726 
727 template <>
728 inline bool can_cast_expr<sign_exprt>(const exprt &base)
729 {
730  return base.id() == ID_sign;
731 }
732 inline void validate_expr(const sign_exprt &expr)
733 {
734  validate_operands(expr, 1, "sign expression must have one operand");
735 }
736 
738 class binary_exprt:public exprt
739 {
740 public:
741  DEPRECATED("use binary_exprt(lhs, id, rhs) instead")
743  {
744  operands().resize(2);
745  }
746 
747  DEPRECATED("use binary_exprt(lhs, id, rhs) instead")
748  explicit binary_exprt(const irep_idt &_id):exprt(_id)
749  {
750  operands().resize(2);
751  }
752 
753  DEPRECATED("use binary_exprt(lhs, id, rhs, type) instead")
755  const irep_idt &_id,
756  const typet &_type):exprt(_id, _type)
757  {
758  operands().resize(2);
759  }
760 
762  const exprt &_lhs,
763  const irep_idt &_id,
764  const exprt &_rhs):
765  exprt(_id, _lhs.type())
766  {
767  add_to_operands(_lhs, _rhs);
768  }
769 
771  const exprt &_lhs,
772  const irep_idt &_id,
773  const exprt &_rhs,
774  const typet &_type):
775  exprt(_id, _type)
776  {
777  add_to_operands(_lhs, _rhs);
778  }
779 
780  static void check(
781  const exprt &expr,
783  {
784  DATA_CHECK(
785  vm,
786  expr.operands().size() == 2,
787  "binary expression must have two operands");
788  }
789 
790  static void validate(
791  const exprt &expr,
792  const namespacet &,
794  {
795  check(expr, vm);
796  }
797 
798  const exprt &op2() const = delete;
799  exprt &op2() = delete;
800  const exprt &op3() const = delete;
801  exprt &op3() = delete;
802 };
803 
810 inline const binary_exprt &to_binary_expr(const exprt &expr)
811 {
813  expr.operands().size()==2,
814  "Binary expressions must have two operands");
815  return static_cast<const binary_exprt &>(expr);
816 }
817 
820 {
822  expr.operands().size()==2,
823  "Binary expressions must have two operands");
824  return static_cast<binary_exprt &>(expr);
825 }
826 
827 template<> inline bool can_cast_expr<binary_exprt>(const exprt &base)
828 {
829  return base.operands().size()==2;
830 }
831 
832 
836 {
837 public:
838  DEPRECATED("use binary_predicate_exprt(lhs, id, rhs) instead")
840  {
841  }
842 
843  DEPRECATED("use binary_predicate_exprt(lhs, id, rhs) instead")
844  explicit binary_predicate_exprt(const irep_idt &_id):
845  binary_exprt(_id, bool_typet())
846  {
847  }
848 
850  const exprt &_op0,
851  const irep_idt &_id,
852  const exprt &_op1):binary_exprt(_op0, _id, _op1, bool_typet())
853  {
854  }
855 
856  static void check(
857  const exprt &expr,
859  {
860  binary_exprt::check(expr, vm);
861  }
862 
863  static void validate(
864  const exprt &expr,
865  const namespacet &ns,
867  {
868  binary_exprt::validate(expr, ns, vm);
869 
870  DATA_CHECK(
871  vm,
872  expr.type().id() == ID_bool,
873  "result of binary predicate expression should be of type bool");
874  }
875 };
876 
879 {
880 public:
881  DEPRECATED("use binary_relation_exprt(lhs, id, rhs) instead")
883  {
884  }
885 
886  DEPRECATED("use binary_relation_exprt(lhs, id, rhs) instead")
887  explicit binary_relation_exprt(const irep_idt &id):
889  {
890  }
891 
893  const exprt &_lhs,
894  const irep_idt &_id,
895  const exprt &_rhs):
896  binary_predicate_exprt(_lhs, _id, _rhs)
897  {
898  }
899 
900  static void check(
901  const exprt &expr,
903  {
905  }
906 
907  static void validate(
908  const exprt &expr,
909  const namespacet &ns,
911  {
912  binary_predicate_exprt::validate(expr, ns, vm);
913 
914  // check types
915  DATA_CHECK(
916  vm,
917  base_type_eq(expr.op0().type(), expr.op1().type(), ns),
918  "lhs and rhs of binary relation expression should have same type");
919  }
920 
922  {
923  return op0();
924  }
925 
926  const exprt &lhs() const
927  {
928  return op0();
929  }
930 
932  {
933  return op1();
934  }
935 
936  const exprt &rhs() const
937  {
938  return op1();
939  }
940 };
941 
949 {
951  expr.operands().size()==2,
952  "Binary relations must have two operands");
953  return static_cast<const binary_relation_exprt &>(expr);
954 }
955 
958 {
960  expr.operands().size()==2,
961  "Binary relations must have two operands");
962  return static_cast<binary_relation_exprt &>(expr);
963 }
964 
965 template<> inline bool can_cast_expr<binary_relation_exprt>(const exprt &base)
966 {
967  return can_cast_expr<binary_exprt>(base);
968 }
969 
970 
973 class multi_ary_exprt:public exprt
974 {
975 public:
976  DEPRECATED("use multi_ary_exprt(id, op, type) instead")
978  {
979  }
980 
981  DEPRECATED("use multi_ary_exprt(id, op, type) instead")
982  explicit multi_ary_exprt(const irep_idt &_id):exprt(_id)
983  {
984  }
985 
986  DEPRECATED("use multi_ary_exprt(id, op, type) instead")
988  const irep_idt &_id,
989  const typet &_type):exprt(_id, _type)
990  {
991  }
992 
994  const irep_idt &_id,
995  operandst &&_operands,
996  const typet &_type)
997  : exprt(_id, _type)
998  {
999  operands() = std::move(_operands);
1000  }
1001 
1003  const exprt &_lhs,
1004  const irep_idt &_id,
1005  const exprt &_rhs):
1006  exprt(_id, _lhs.type())
1007  {
1008  add_to_operands(_lhs, _rhs);
1009  }
1010 
1012  const exprt &_lhs,
1013  const irep_idt &_id,
1014  const exprt &_rhs,
1015  const typet &_type):
1016  exprt(_id, _type)
1017  {
1018  add_to_operands(_lhs, _rhs);
1019  }
1020 };
1021 
1028 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
1029 {
1030  return static_cast<const multi_ary_exprt &>(expr);
1031 }
1032 
1035 {
1036  return static_cast<multi_ary_exprt &>(expr);
1037 }
1038 
1039 
1043 {
1044 public:
1045  DEPRECATED("use plus_exprt(lhs, rhs) instead")
1047  {
1048  }
1049 
1051  {
1052  }
1053 
1055  const exprt &_lhs,
1056  const exprt &_rhs):
1057  multi_ary_exprt(_lhs, ID_plus, _rhs)
1058  {
1059  }
1060 
1062  const exprt &_lhs,
1063  const exprt &_rhs,
1064  const typet &_type):
1065  multi_ary_exprt(_lhs, ID_plus, _rhs, _type)
1066  {
1067  }
1068 };
1069 
1076 inline const plus_exprt &to_plus_expr(const exprt &expr)
1077 {
1078  PRECONDITION(expr.id()==ID_plus);
1080  expr.operands().size()>=2,
1081  "Plus must have two or more operands");
1082  return static_cast<const plus_exprt &>(expr);
1083 }
1084 
1087 {
1088  PRECONDITION(expr.id()==ID_plus);
1090  expr.operands().size()>=2,
1091  "Plus must have two or more operands");
1092  return static_cast<plus_exprt &>(expr);
1093 }
1094 
1095 template<> inline bool can_cast_expr<plus_exprt>(const exprt &base)
1096 {
1097  return base.id()==ID_plus;
1098 }
1099 inline void validate_expr(const plus_exprt &value)
1100 {
1101  validate_operands(value, 2, "Plus must have two or more operands", true);
1102 }
1103 
1104 
1107 {
1108 public:
1109  DEPRECATED("use minus_exprt(lhs, rhs) instead")
1111  {
1112  }
1113 
1115  const exprt &_lhs,
1116  const exprt &_rhs):
1117  binary_exprt(_lhs, ID_minus, _rhs)
1118  {
1119  }
1120 };
1121 
1128 inline const minus_exprt &to_minus_expr(const exprt &expr)
1129 {
1130  PRECONDITION(expr.id()==ID_minus);
1132  expr.operands().size()>=2,
1133  "Minus must have two or more operands");
1134  return static_cast<const minus_exprt &>(expr);
1135 }
1136 
1139 {
1140  PRECONDITION(expr.id()==ID_minus);
1142  expr.operands().size()>=2,
1143  "Minus must have two or more operands");
1144  return static_cast<minus_exprt &>(expr);
1145 }
1146 
1147 template<> inline bool can_cast_expr<minus_exprt>(const exprt &base)
1148 {
1149  return base.id()==ID_minus;
1150 }
1151 inline void validate_expr(const minus_exprt &value)
1152 {
1153  validate_operands(value, 2, "Minus must have two or more operands", true);
1154 }
1155 
1156 
1160 {
1161 public:
1162  DEPRECATED("use mult_exprt(lhs, rhs) instead")
1164  {
1165  }
1166 
1168  const exprt &_lhs,
1169  const exprt &_rhs):
1170  multi_ary_exprt(_lhs, ID_mult, _rhs)
1171  {
1172  }
1173 };
1174 
1181 inline const mult_exprt &to_mult_expr(const exprt &expr)
1182 {
1183  PRECONDITION(expr.id()==ID_mult);
1185  expr.operands().size()>=2,
1186  "Multiply must have two or more operands");
1187  return static_cast<const mult_exprt &>(expr);
1188 }
1189 
1192 {
1193  PRECONDITION(expr.id()==ID_mult);
1195  expr.operands().size()>=2,
1196  "Multiply must have two or more operands");
1197  return static_cast<mult_exprt &>(expr);
1198 }
1199 
1200 template<> inline bool can_cast_expr<mult_exprt>(const exprt &base)
1201 {
1202  return base.id()==ID_mult;
1203 }
1204 inline void validate_expr(const mult_exprt &value)
1205 {
1206  validate_operands(value, 2, "Multiply must have two or more operands", true);
1207 }
1208 
1209 
1212 {
1213 public:
1214  DEPRECATED("use div_exprt(lhs, rhs) instead")
1216  {
1217  }
1218 
1220  const exprt &_lhs,
1221  const exprt &_rhs):
1222  binary_exprt(_lhs, ID_div, _rhs)
1223  {
1224  }
1225 
1228  {
1229  return op0();
1230  }
1231 
1233  const exprt &dividend() const
1234  {
1235  return op0();
1236  }
1237 
1240  {
1241  return op1();
1242  }
1243 
1245  const exprt &divisor() const
1246  {
1247  return op1();
1248  }
1249 };
1250 
1257 inline const div_exprt &to_div_expr(const exprt &expr)
1258 {
1259  PRECONDITION(expr.id()==ID_div);
1261  expr.operands().size()==2,
1262  "Divide must have two operands");
1263  return static_cast<const div_exprt &>(expr);
1264 }
1265 
1268 {
1269  PRECONDITION(expr.id()==ID_div);
1271  expr.operands().size()==2,
1272  "Divide must have two operands");
1273  return static_cast<div_exprt &>(expr);
1274 }
1275 
1276 template<> inline bool can_cast_expr<div_exprt>(const exprt &base)
1277 {
1278  return base.id()==ID_div;
1279 }
1280 inline void validate_expr(const div_exprt &value)
1281 {
1282  validate_operands(value, 2, "Divide must have two operands");
1283 }
1284 
1285 
1288 {
1289 public:
1290  DEPRECATED("use mod_exprt(lhs, rhs) instead")
1292  {
1293  }
1294 
1296  const exprt &_lhs,
1297  const exprt &_rhs):
1298  binary_exprt(_lhs, ID_mod, _rhs)
1299  {
1300  }
1301 };
1302 
1309 inline const mod_exprt &to_mod_expr(const exprt &expr)
1310 {
1311  PRECONDITION(expr.id()==ID_mod);
1312  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
1313  return static_cast<const mod_exprt &>(expr);
1314 }
1315 
1318 {
1319  PRECONDITION(expr.id()==ID_mod);
1320  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
1321  return static_cast<mod_exprt &>(expr);
1322 }
1323 
1324 template<> inline bool can_cast_expr<mod_exprt>(const exprt &base)
1325 {
1326  return base.id()==ID_mod;
1327 }
1328 inline void validate_expr(const mod_exprt &value)
1329 {
1330  validate_operands(value, 2, "Modulo must have two operands");
1331 }
1332 
1333 
1336 {
1337 public:
1338  DEPRECATED("use rem_exprt(lhs, rhs) instead")
1340  {
1341  }
1342 
1344  const exprt &_lhs,
1345  const exprt &_rhs):
1346  binary_exprt(_lhs, ID_rem, _rhs)
1347  {
1348  }
1349 };
1350 
1357 inline const rem_exprt &to_rem_expr(const exprt &expr)
1358 {
1359  PRECONDITION(expr.id()==ID_rem);
1360  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
1361  return static_cast<const rem_exprt &>(expr);
1362 }
1363 
1366 {
1367  PRECONDITION(expr.id()==ID_rem);
1368  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
1369  return static_cast<rem_exprt &>(expr);
1370 }
1371 
1372 template<> inline bool can_cast_expr<rem_exprt>(const exprt &base)
1373 {
1374  return base.id()==ID_rem;
1375 }
1376 inline void validate_expr(const rem_exprt &value)
1377 {
1378  validate_operands(value, 2, "Remainder must have two operands");
1379 }
1380 
1381 
1384 {
1385 public:
1386  DEPRECATED("use power_exprt(lhs, rhs) instead")
1388  {
1389  }
1390 
1392  const exprt &_base,
1393  const exprt &_exp):
1394  binary_exprt(_base, ID_power, _exp)
1395  {
1396  }
1397 };
1398 
1405 inline const power_exprt &to_power_expr(const exprt &expr)
1406 {
1407  PRECONDITION(expr.id()==ID_power);
1408  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
1409  return static_cast<const power_exprt &>(expr);
1410 }
1411 
1414 {
1415  PRECONDITION(expr.id()==ID_power);
1416  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
1417  return static_cast<power_exprt &>(expr);
1418 }
1419 
1420 template<> inline bool can_cast_expr<power_exprt>(const exprt &base)
1421 {
1422  return base.id()==ID_power;
1423 }
1424 inline void validate_expr(const power_exprt &value)
1425 {
1426  validate_operands(value, 2, "Power must have two operands");
1427 }
1428 
1429 
1432 {
1433 public:
1434  DEPRECATED("use factorial_power_exprt(lhs, rhs) instead")
1435  factorial_power_exprt():binary_exprt(ID_factorial_power)
1436  {
1437  }
1438 
1440  const exprt &_base,
1441  const exprt &_exp):
1442  binary_exprt(_base, ID_factorial_power, _exp)
1443  {
1444  }
1445 };
1446 
1454 {
1455  PRECONDITION(expr.id()==ID_factorial_power);
1457  expr.operands().size()==2,
1458  "Factorial power must have two operands");
1459  return static_cast<const factorial_power_exprt &>(expr);
1460 }
1461 
1464 {
1465  PRECONDITION(expr.id()==ID_factorial_power);
1467  expr.operands().size()==2,
1468  "Factorial power must have two operands");
1469  return static_cast<factorial_power_exprt &>(expr);
1470 }
1471 
1473  const exprt &base)
1474 {
1475  return base.id()==ID_factorial_power;
1476 }
1477 inline void validate_expr(const factorial_power_exprt &value)
1478 {
1479  validate_operands(value, 2, "Factorial power must have two operands");
1480 }
1481 
1482 
1485 {
1486 public:
1487  DEPRECATED("use equal_exprt(lhs, rhs) instead")
1489  {
1490  }
1491 
1492  equal_exprt(const exprt &_lhs, const exprt &_rhs):
1493  binary_relation_exprt(_lhs, ID_equal, _rhs)
1494  {
1495  }
1496 
1497  static void check(
1498  const exprt &expr,
1500  {
1501  binary_relation_exprt::check(expr, vm);
1502  }
1503 
1504  static void validate(
1505  const exprt &expr,
1506  const namespacet &ns,
1508  {
1509  binary_relation_exprt::validate(expr, ns, vm);
1510  }
1511 };
1512 
1519 inline const equal_exprt &to_equal_expr(const exprt &expr)
1520 {
1521  PRECONDITION(expr.id()==ID_equal);
1522  equal_exprt::check(expr);
1523  return static_cast<const equal_exprt &>(expr);
1524 }
1525 
1528 {
1529  PRECONDITION(expr.id()==ID_equal);
1530  equal_exprt::check(expr);
1531  return static_cast<equal_exprt &>(expr);
1532 }
1533 
1534 template<> inline bool can_cast_expr<equal_exprt>(const exprt &base)
1535 {
1536  return base.id()==ID_equal;
1537 }
1538 inline void validate_expr(const equal_exprt &value)
1539 {
1540  validate_operands(value, 2, "Equality must have two operands");
1541 }
1542 
1543 
1546 {
1547 public:
1548  DEPRECATED("use notequal_exprt(lhs, rhs) instead")
1550  {
1551  }
1552 
1553  notequal_exprt(const exprt &_lhs, const exprt &_rhs):
1554  binary_relation_exprt(_lhs, ID_notequal, _rhs)
1555  {
1556  }
1557 };
1558 
1565 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1566 {
1567  PRECONDITION(expr.id()==ID_notequal);
1569  expr.operands().size()==2,
1570  "Inequality must have two operands");
1571  return static_cast<const notequal_exprt &>(expr);
1572 }
1573 
1576 {
1577  PRECONDITION(expr.id()==ID_notequal);
1579  expr.operands().size()==2,
1580  "Inequality must have two operands");
1581  return static_cast<notequal_exprt &>(expr);
1582 }
1583 
1584 template<> inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1585 {
1586  return base.id()==ID_notequal;
1587 }
1588 inline void validate_expr(const notequal_exprt &value)
1589 {
1590  validate_operands(value, 2, "Inequality must have two operands");
1591 }
1592 
1593 
1596 {
1597 public:
1598  DEPRECATED("use index_exprt(array, index) instead")
1600  {
1601  }
1602 
1603  DEPRECATED("use index_exprt(array, index) instead")
1604  explicit index_exprt(const typet &_type):binary_exprt(ID_index, _type)
1605  {
1606  }
1607 
1608  index_exprt(const exprt &_array, const exprt &_index):
1609  binary_exprt(_array, ID_index, _index, _array.type().subtype())
1610  {
1611  }
1612 
1614  const exprt &_array,
1615  const exprt &_index,
1616  const typet &_type):
1617  binary_exprt(_array, ID_index, _index, _type)
1618  {
1619  }
1620 
1622  {
1623  return op0();
1624  }
1625 
1626  const exprt &array() const
1627  {
1628  return op0();
1629  }
1630 
1632  {
1633  return op1();
1634  }
1635 
1636  const exprt &index() const
1637  {
1638  return op1();
1639  }
1640 };
1641 
1648 inline const index_exprt &to_index_expr(const exprt &expr)
1649 {
1650  PRECONDITION(expr.id()==ID_index);
1652  expr.operands().size()==2,
1653  "Array index must have two operands");
1654  return static_cast<const index_exprt &>(expr);
1655 }
1656 
1659 {
1660  PRECONDITION(expr.id()==ID_index);
1662  expr.operands().size()==2,
1663  "Array index must have two operands");
1664  return static_cast<index_exprt &>(expr);
1665 }
1666 
1667 template<> inline bool can_cast_expr<index_exprt>(const exprt &base)
1668 {
1669  return base.id()==ID_index;
1670 }
1671 inline void validate_expr(const index_exprt &value)
1672 {
1673  validate_operands(value, 2, "Array index must have two operands");
1674 }
1675 
1676 
1679 {
1680 public:
1681  DEPRECATED("use array_of_exprt(what, type) instead")
1683  {
1684  }
1685 
1686  explicit array_of_exprt(
1687  const exprt &_what, const array_typet &_type):
1688  unary_exprt(ID_array_of, _what, _type)
1689  {
1690  }
1691 
1693  {
1694  return op0();
1695  }
1696 
1697  const exprt &what() const
1698  {
1699  return op0();
1700  }
1701 };
1702 
1709 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1710 {
1711  PRECONDITION(expr.id()==ID_array_of);
1713  expr.operands().size()==1,
1714  "'Array of' must have one operand");
1715  return static_cast<const array_of_exprt &>(expr);
1716 }
1717 
1720 {
1721  PRECONDITION(expr.id()==ID_array_of);
1723  expr.operands().size()==1,
1724  "'Array of' must have one operand");
1725  return static_cast<array_of_exprt &>(expr);
1726 }
1727 
1728 template<> inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1729 {
1730  return base.id()==ID_array_of;
1731 }
1732 inline void validate_expr(const array_of_exprt &value)
1733 {
1734  validate_operands(value, 1, "'Array of' must have one operand");
1735 }
1736 
1737 
1740 {
1741 public:
1742  DEPRECATED("use array_exprt(type) instead")
1744  {
1745  }
1746 
1747  explicit array_exprt(const array_typet &_type)
1748  : multi_ary_exprt(ID_array, _type)
1749  {
1750  }
1751 };
1752 
1759 inline const array_exprt &to_array_expr(const exprt &expr)
1760 {
1761  PRECONDITION(expr.id()==ID_array);
1762  return static_cast<const array_exprt &>(expr);
1763 }
1764 
1767 {
1768  PRECONDITION(expr.id()==ID_array);
1769  return static_cast<array_exprt &>(expr);
1770 }
1771 
1772 template<> inline bool can_cast_expr<array_exprt>(const exprt &base)
1773 {
1774  return base.id()==ID_array;
1775 }
1776 
1780 {
1781 public:
1782  explicit array_list_exprt(const array_typet &_type)
1783  : multi_ary_exprt(ID_array_list, _type)
1784  {
1785  }
1786 };
1787 
1788 template <>
1789 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1790 {
1791  return base.id() == ID_array_list;
1792 }
1793 
1794 inline void validate_expr(const array_list_exprt &value)
1795 {
1796  PRECONDITION(value.operands().size() % 2 == 0);
1797 }
1798 
1801 {
1802 public:
1803  DEPRECATED("use vector_exprt(type) instead")
1805  {
1806  }
1807 
1808  explicit vector_exprt(const vector_typet &_type)
1809  : multi_ary_exprt(ID_vector, _type)
1810  {
1811  }
1812 };
1813 
1820 inline const vector_exprt &to_vector_expr(const exprt &expr)
1821 {
1822  PRECONDITION(expr.id()==ID_vector);
1823  return static_cast<const vector_exprt &>(expr);
1824 }
1825 
1828 {
1829  PRECONDITION(expr.id()==ID_vector);
1830  return static_cast<vector_exprt &>(expr);
1831 }
1832 
1833 template<> inline bool can_cast_expr<vector_exprt>(const exprt &base)
1834 {
1835  return base.id()==ID_vector;
1836 }
1837 
1838 
1841 {
1842 public:
1843  DEPRECATED("use union_exprt(component_name, value, type) instead")
1845  {
1846  }
1847 
1848  DEPRECATED("use union_exprt(component_name, value, type) instead")
1849  explicit union_exprt(const typet &_type):
1850  unary_exprt(ID_union, _type)
1851  {
1852  }
1853 
1855  const irep_idt &_component_name,
1856  const exprt &_value,
1857  const typet &_type)
1858  : unary_exprt(ID_union, _value, _type)
1859  {
1860  set_component_name(_component_name);
1861  }
1862 
1864  {
1865  return get(ID_component_name);
1866  }
1867 
1868  void set_component_name(const irep_idt &component_name)
1869  {
1870  set(ID_component_name, component_name);
1871  }
1872 
1873  std::size_t get_component_number() const
1874  {
1875  return get_size_t(ID_component_number);
1876  }
1877 
1878  void set_component_number(std::size_t component_number)
1879  {
1880  set(ID_component_number, component_number);
1881  }
1882 };
1883 
1890 inline const union_exprt &to_union_expr(const exprt &expr)
1891 {
1892  PRECONDITION(expr.id()==ID_union);
1894  expr.operands().size()==1,
1895  "Union constructor must have one operand");
1896  return static_cast<const union_exprt &>(expr);
1897 }
1898 
1901 {
1902  PRECONDITION(expr.id()==ID_union);
1904  expr.operands().size()==1,
1905  "Union constructor must have one operand");
1906  return static_cast<union_exprt &>(expr);
1907 }
1908 
1909 template<> inline bool can_cast_expr<union_exprt>(const exprt &base)
1910 {
1911  return base.id()==ID_union;
1912 }
1913 inline void validate_expr(const union_exprt &value)
1914 {
1915  validate_operands(value, 1, "Union constructor must have one operand");
1916 }
1917 
1918 
1921 {
1922 public:
1923  DEPRECATED("use struct_exprt(component_name, value, type) instead")
1925  {
1926  }
1927 
1928  explicit struct_exprt(const typet &_type) : multi_ary_exprt(ID_struct, _type)
1929  {
1930  }
1931 
1932  exprt &component(const irep_idt &name, const namespacet &ns);
1933  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1934 };
1935 
1942 inline const struct_exprt &to_struct_expr(const exprt &expr)
1943 {
1944  PRECONDITION(expr.id()==ID_struct);
1945  return static_cast<const struct_exprt &>(expr);
1946 }
1947 
1950 {
1951  PRECONDITION(expr.id()==ID_struct);
1952  return static_cast<struct_exprt &>(expr);
1953 }
1954 
1955 template<> inline bool can_cast_expr<struct_exprt>(const exprt &base)
1956 {
1957  return base.id()==ID_struct;
1958 }
1959 
1960 
1963 {
1964 public:
1965  DEPRECATED("use complex_exprt(r, i, type) instead")
1967  {
1968  }
1969 
1970  DEPRECATED("use complex_exprt(r, i, type) instead")
1971  explicit complex_exprt(const complex_typet &_type):
1972  binary_exprt(ID_complex, _type)
1973  {
1974  }
1975 
1977  const exprt &_real,
1978  const exprt &_imag,
1979  const complex_typet &_type)
1980  : binary_exprt(_real, ID_complex, _imag, _type)
1981  {
1982  }
1983 
1985  {
1986  return op0();
1987  }
1988 
1989  const exprt &real() const
1990  {
1991  return op0();
1992  }
1993 
1995  {
1996  return op1();
1997  }
1998 
1999  const exprt &imag() const
2000  {
2001  return op1();
2002  }
2003 };
2004 
2011 inline const complex_exprt &to_complex_expr(const exprt &expr)
2012 {
2013  PRECONDITION(expr.id()==ID_complex);
2015  expr.operands().size()==2,
2016  "Complex constructor must have two operands");
2017  return static_cast<const complex_exprt &>(expr);
2018 }
2019 
2022 {
2023  PRECONDITION(expr.id()==ID_complex);
2025  expr.operands().size()==2,
2026  "Complex constructor must have two operands");
2027  return static_cast<complex_exprt &>(expr);
2028 }
2029 
2030 template<> inline bool can_cast_expr<complex_exprt>(const exprt &base)
2031 {
2032  return base.id()==ID_complex;
2033 }
2034 inline void validate_expr(const complex_exprt &value)
2035 {
2036  validate_operands(value, 2, "Complex constructor must have two operands");
2037 }
2038 
2041 {
2042 public:
2043  explicit complex_real_exprt(const exprt &op)
2044  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
2045  {
2046  }
2047 };
2048 
2056 {
2057  PRECONDITION(expr.id() == ID_complex_real);
2059  expr.operands().size() == 1,
2060  "real part retrieval operation must have one operand");
2061  return static_cast<const complex_real_exprt &>(expr);
2062 }
2063 
2066 {
2067  PRECONDITION(expr.id() == ID_complex_real);
2069  expr.operands().size() == 1,
2070  "real part retrieval operation must have one operand");
2071  return static_cast<complex_real_exprt &>(expr);
2072 }
2073 
2074 template <>
2076 {
2077  return base.id() == ID_complex_real;
2078 }
2079 
2080 inline void validate_expr(const complex_real_exprt &expr)
2081 {
2083  expr, 1, "real part retrieval operation must have one operand");
2084 }
2085 
2088 {
2089 public:
2090  explicit complex_imag_exprt(const exprt &op)
2091  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
2092  {
2093  }
2094 };
2095 
2103 {
2104  PRECONDITION(expr.id() == ID_complex_imag);
2106  expr.operands().size() == 1,
2107  "imaginary part retrieval operation must have one operand");
2108  return static_cast<const complex_imag_exprt &>(expr);
2109 }
2110 
2113 {
2114  PRECONDITION(expr.id() == ID_complex_imag);
2116  expr.operands().size() == 1,
2117  "imaginary part retrieval operation must have one operand");
2118  return static_cast<complex_imag_exprt &>(expr);
2119 }
2120 
2121 template <>
2123 {
2124  return base.id() == ID_complex_imag;
2125 }
2126 
2127 inline void validate_expr(const complex_imag_exprt &expr)
2128 {
2130  expr, 1, "imaginary part retrieval operation must have one operand");
2131 }
2132 
2133 class namespacet;
2134 
2137 {
2138 public:
2139  object_descriptor_exprt():binary_exprt(ID_object_descriptor)
2140  {
2141  op0().id(ID_unknown);
2142  op1().id(ID_unknown);
2143  }
2144 
2145  void build(const exprt &expr, const namespacet &ns);
2146 
2148  {
2149  return op0();
2150  }
2151 
2152  const exprt &object() const
2153  {
2154  return op0();
2155  }
2156 
2157  const exprt &root_object() const;
2158 
2160  {
2161  return op1();
2162  }
2163 
2164  const exprt &offset() const
2165  {
2166  return op1();
2167  }
2168 };
2169 
2177  const exprt &expr)
2178 {
2179  PRECONDITION(expr.id()==ID_object_descriptor);
2181  expr.operands().size()==2,
2182  "Object descriptor must have two operands");
2183  return static_cast<const object_descriptor_exprt &>(expr);
2184 }
2185 
2188 {
2189  PRECONDITION(expr.id()==ID_object_descriptor);
2191  expr.operands().size()==2,
2192  "Object descriptor must have two operands");
2193  return static_cast<object_descriptor_exprt &>(expr);
2194 }
2195 
2196 template<>
2198 {
2199  return base.id()==ID_object_descriptor;
2200 }
2201 inline void validate_expr(const object_descriptor_exprt &value)
2202 {
2203  validate_operands(value, 2, "Object descriptor must have two operands");
2204 }
2205 
2206 
2209 {
2210 public:
2211  dynamic_object_exprt():binary_exprt(ID_dynamic_object)
2212  {
2213  op0().id(ID_unknown);
2214  op1().id(ID_unknown);
2215  }
2216 
2217  explicit dynamic_object_exprt(const typet &type):
2218  binary_exprt(ID_dynamic_object, type)
2219  {
2220  op0().id(ID_unknown);
2221  op1().id(ID_unknown);
2222  }
2223 
2224  void set_instance(unsigned int instance);
2225 
2226  unsigned int get_instance() const;
2227 
2229  {
2230  return op1();
2231  }
2232 
2233  const exprt &valid() const
2234  {
2235  return op1();
2236  }
2237 };
2238 
2246  const exprt &expr)
2247 {
2248  PRECONDITION(expr.id()==ID_dynamic_object);
2250  expr.operands().size()==2,
2251  "Dynamic object must have two operands");
2252  return static_cast<const dynamic_object_exprt &>(expr);
2253 }
2254 
2257 {
2258  PRECONDITION(expr.id()==ID_dynamic_object);
2260  expr.operands().size()==2,
2261  "Dynamic object must have two operands");
2262  return static_cast<dynamic_object_exprt &>(expr);
2263 }
2264 
2265 template<> inline bool can_cast_expr<dynamic_object_exprt>(const exprt &base)
2266 {
2267  return base.id()==ID_dynamic_object;
2268 }
2269 
2270 inline void validate_expr(const dynamic_object_exprt &value)
2271 {
2272  validate_operands(value, 2, "Dynamic object must have two operands");
2273 }
2274 
2275 
2278 {
2279 public:
2280  DEPRECATED("use typecast_exprt(op, type) instead")
2281  explicit typecast_exprt(const typet &_type):unary_exprt(ID_typecast, _type)
2282  {
2283  }
2284 
2285  typecast_exprt(const exprt &op, const typet &_type):
2286  unary_exprt(ID_typecast, op, _type)
2287  {
2288  }
2289 
2290  // returns a typecast if the type doesn't already match
2291  static exprt conditional_cast(const exprt &expr, const typet &type)
2292  {
2293  if(expr.type() == type)
2294  return expr;
2295  else
2296  return typecast_exprt(expr, type);
2297  }
2298 };
2299 
2306 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2307 {
2308  PRECONDITION(expr.id()==ID_typecast);
2310  expr.operands().size()==1,
2311  "Typecast must have one operand");
2312  return static_cast<const typecast_exprt &>(expr);
2313 }
2314 
2317 {
2318  PRECONDITION(expr.id()==ID_typecast);
2320  expr.operands().size()==1,
2321  "Typecast must have one operand");
2322  return static_cast<typecast_exprt &>(expr);
2323 }
2324 
2325 template<> inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2326 {
2327  return base.id()==ID_typecast;
2328 }
2329 inline void validate_expr(const typecast_exprt &value)
2330 {
2331  validate_operands(value, 1, "Typecast must have one operand");
2332 }
2333 
2334 
2337 {
2338 public:
2339  DEPRECATED("use floatbv_typecast_exprt(op, r, type) instead")
2340  floatbv_typecast_exprt():binary_exprt(ID_floatbv_typecast)
2341  {
2342  }
2343 
2345  const exprt &op,
2346  const exprt &rounding,
2347  const typet &_type):binary_exprt(op, ID_floatbv_typecast, rounding, _type)
2348  {
2349  }
2350 
2352  {
2353  return op0();
2354  }
2355 
2356  const exprt &op() const
2357  {
2358  return op0();
2359  }
2360 
2362  {
2363  return op1();
2364  }
2365 
2366  const exprt &rounding_mode() const
2367  {
2368  return op1();
2369  }
2370 };
2371 
2379 {
2380  PRECONDITION(expr.id()==ID_floatbv_typecast);
2382  expr.operands().size()==2,
2383  "Float typecast must have two operands");
2384  return static_cast<const floatbv_typecast_exprt &>(expr);
2385 }
2386 
2389 {
2390  PRECONDITION(expr.id()==ID_floatbv_typecast);
2392  expr.operands().size()==2,
2393  "Float typecast must have two operands");
2394  return static_cast<floatbv_typecast_exprt &>(expr);
2395 }
2396 
2397 template<>
2399 {
2400  return base.id()==ID_floatbv_typecast;
2401 }
2402 inline void validate_expr(const floatbv_typecast_exprt &value)
2403 {
2404  validate_operands(value, 2, "Float typecast must have two operands");
2405 }
2406 
2407 
2410 {
2411 public:
2413  {
2414  }
2415 
2416  and_exprt(const exprt &op0, const exprt &op1):
2417  multi_ary_exprt(op0, ID_and, op1, bool_typet())
2418  {
2419  }
2420 
2421  and_exprt(const exprt &op0, const exprt &op1, const exprt &op2):
2422  multi_ary_exprt(ID_and, bool_typet())
2423  {
2425  }
2426 
2428  const exprt &op0,
2429  const exprt &op1,
2430  const exprt &op2,
2431  const exprt &op3):
2432  multi_ary_exprt(ID_and, bool_typet())
2433  {
2434  exprt::operandst &op=operands();
2435  op.resize(4);
2436  op[0]=op0;
2437  op[1]=op1;
2438  op[2]=op2;
2439  op[3]=op3;
2440  }
2441 };
2442 
2446 
2448 
2455 inline const and_exprt &to_and_expr(const exprt &expr)
2456 {
2457  PRECONDITION(expr.id()==ID_and);
2458  // DATA_INVARIANT(
2459  // expr.operands().size()>=2,
2460  // "And must have two or more operands");
2461  return static_cast<const and_exprt &>(expr);
2462 }
2463 
2466 {
2467  PRECONDITION(expr.id()==ID_and);
2468  // DATA_INVARIANT(
2469  // expr.operands().size()>=2,
2470  // "And must have two or more operands");
2471  return static_cast<and_exprt &>(expr);
2472 }
2473 
2474 template<> inline bool can_cast_expr<and_exprt>(const exprt &base)
2475 {
2476  return base.id()==ID_and;
2477 }
2478 // inline void validate_expr(const and_exprt &value)
2479 // {
2480 // validate_operands(value, 2, "And must have two or more operands", true);
2481 // }
2482 
2483 
2486 {
2487 public:
2488  DEPRECATED("use implies_exprt(a, b) instead")
2490  {
2491  }
2492 
2493  implies_exprt(const exprt &op0, const exprt &op1):
2494  binary_exprt(op0, ID_implies, op1, bool_typet())
2495  {
2496  }
2497 };
2498 
2505 inline const implies_exprt &to_implies_expr(const exprt &expr)
2506 {
2507  PRECONDITION(expr.id()==ID_implies);
2508  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
2509  return static_cast<const implies_exprt &>(expr);
2510 }
2511 
2514 {
2515  PRECONDITION(expr.id()==ID_implies);
2516  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
2517  return static_cast<implies_exprt &>(expr);
2518 }
2519 
2520 template<> inline bool can_cast_expr<implies_exprt>(const exprt &base)
2521 {
2522  return base.id()==ID_implies;
2523 }
2524 inline void validate_expr(const implies_exprt &value)
2525 {
2526  validate_operands(value, 2, "Implies must have two operands");
2527 }
2528 
2529 
2532 {
2533 public:
2535  {
2536  }
2537 
2538  or_exprt(const exprt &op0, const exprt &op1):
2539  multi_ary_exprt(op0, ID_or, op1, bool_typet())
2540  {
2541  }
2542 
2543  or_exprt(const exprt &op0, const exprt &op1, const exprt &op2):
2544  multi_ary_exprt(ID_or, bool_typet())
2545  {
2547  }
2548 
2550  const exprt &op0,
2551  const exprt &op1,
2552  const exprt &op2,
2553  const exprt &op3):
2554  multi_ary_exprt(ID_or, bool_typet())
2555  {
2556  exprt::operandst &op=operands();
2557  op.resize(4);
2558  op[0]=op0;
2559  op[1]=op1;
2560  op[2]=op2;
2561  op[3]=op3;
2562  }
2563 };
2564 
2568 
2570 
2577 inline const or_exprt &to_or_expr(const exprt &expr)
2578 {
2579  PRECONDITION(expr.id()==ID_or);
2580  // DATA_INVARIANT(
2581  // expr.operands().size()>=2,
2582  // "Or must have two or more operands");
2583  return static_cast<const or_exprt &>(expr);
2584 }
2585 
2587 inline or_exprt &to_or_expr(exprt &expr)
2588 {
2589  PRECONDITION(expr.id()==ID_or);
2590  // DATA_INVARIANT(
2591  // expr.operands().size()>=2,
2592  // "Or must have two or more operands");
2593  return static_cast<or_exprt &>(expr);
2594 }
2595 
2596 template<> inline bool can_cast_expr<or_exprt>(const exprt &base)
2597 {
2598  return base.id()==ID_or;
2599 }
2600 // inline void validate_expr(const or_exprt &value)
2601 // {
2602 // validate_operands(value, 2, "Or must have two or more operands", true);
2603 // }
2604 
2605 
2608 {
2609 public:
2611  {
2612  }
2613 
2614  xor_exprt(const exprt &_op0, const exprt &_op1):
2615  multi_ary_exprt(_op0, ID_xor, _op1, bool_typet())
2616  {
2617  }
2618 };
2619 
2626 inline const xor_exprt &to_xor_expr(const exprt &expr)
2627 {
2628  PRECONDITION(expr.id()==ID_xor);
2629  return static_cast<const xor_exprt &>(expr);
2630 }
2631 
2634 {
2635  PRECONDITION(expr.id()==ID_xor);
2636  return static_cast<xor_exprt &>(expr);
2637 }
2638 
2639 template<> inline bool can_cast_expr<xor_exprt>(const exprt &base)
2640 {
2641  return base.id()==ID_xor;
2642 }
2643 // inline void validate_expr(const bitxor_exprt &value)
2644 // {
2645 // validate_operands(
2646 // value,
2647 // 2,
2648 // "Bit-wise xor must have two or more operands",
2649 // true);
2650 // }
2651 
2652 
2655 {
2656 public:
2657  DEPRECATED("use bitnot_exprt(op) instead")
2659  {
2660  }
2661 
2662  explicit bitnot_exprt(const exprt &op):
2663  unary_exprt(ID_bitnot, op)
2664  {
2665  }
2666 };
2667 
2674 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
2675 {
2676  PRECONDITION(expr.id()==ID_bitnot);
2677  // DATA_INVARIANT(expr.operands().size()==1,
2678  // "Bit-wise not must have one operand");
2679  return static_cast<const bitnot_exprt &>(expr);
2680 }
2681 
2684 {
2685  PRECONDITION(expr.id()==ID_bitnot);
2686  // DATA_INVARIANT(expr.operands().size()==1,
2687  // "Bit-wise not must have one operand");
2688  return static_cast<bitnot_exprt &>(expr);
2689 }
2690 
2691 template<> inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
2692 {
2693  return base.id()==ID_bitnot;
2694 }
2695 // inline void validate_expr(const bitnot_exprt &value)
2696 // {
2697 // validate_operands(value, 1, "Bit-wise not must have one operand");
2698 // }
2699 
2700 
2703 {
2704 public:
2705  DEPRECATED("use bitor_exprt(op0, op1) instead")
2707  {
2708  }
2709 
2710  bitor_exprt(const exprt &_op0, const exprt &_op1):
2711  multi_ary_exprt(ID_bitor, _op0.type())
2712  {
2713  add_to_operands(_op0, _op1);
2714  }
2715 };
2716 
2723 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
2724 {
2725  PRECONDITION(expr.id()==ID_bitor);
2726  // DATA_INVARIANT(
2727  // expr.operands().size()>=2,
2728  // "Bit-wise or must have two or more operands");
2729  return static_cast<const bitor_exprt &>(expr);
2730 }
2731 
2734 {
2735  PRECONDITION(expr.id()==ID_bitor);
2736  // DATA_INVARIANT(
2737  // expr.operands().size()>=2,
2738  // "Bit-wise or must have two or more operands");
2739  return static_cast<bitor_exprt &>(expr);
2740 }
2741 
2742 template<> inline bool can_cast_expr<bitor_exprt>(const exprt &base)
2743 {
2744  return base.id()==ID_bitor;
2745 }
2746 // inline void validate_expr(const bitor_exprt &value)
2747 // {
2748 // validate_operands(
2749 // value,
2750 // 2,
2751 // "Bit-wise or must have two or more operands",
2752 // true);
2753 // }
2754 
2755 
2758 {
2759 public:
2760  DEPRECATED("use bitxor_exprt(op0, op1) instead")
2762  {
2763  }
2764 
2765  bitxor_exprt(const exprt &_op0, const exprt &_op1):
2766  multi_ary_exprt(_op0, ID_bitxor, _op1, _op0.type())
2767  {
2768  }
2769 };
2770 
2777 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
2778 {
2779  PRECONDITION(expr.id()==ID_bitxor);
2780  // DATA_INVARIANT(
2781  // expr.operands().size()>=2,
2782  // "Bit-wise xor must have two or more operands");
2783  return static_cast<const bitxor_exprt &>(expr);
2784 }
2785 
2788 {
2789  PRECONDITION(expr.id()==ID_bitxor);
2790  // DATA_INVARIANT(
2791  // expr.operands().size()>=2,
2792  // "Bit-wise xor must have two or more operands");
2793  return static_cast<bitxor_exprt &>(expr);
2794 }
2795 
2796 template<> inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
2797 {
2798  return base.id()==ID_bitxor;
2799 }
2800 // inline void validate_expr(const bitxor_exprt &value)
2801 // {
2802 // validate_operands(
2803 // value,
2804 // 2,
2805 // "Bit-wise xor must have two or more operands",
2806 // true);
2807 // }
2808 
2809 
2812 {
2813 public:
2814  DEPRECATED("use bitand_exprt(op0, op1) instead")
2816  {
2817  }
2818 
2819  bitand_exprt(const exprt &_op0, const exprt &_op1):
2820  multi_ary_exprt(ID_bitand, _op0.type())
2821  {
2822  add_to_operands(_op0, _op1);
2823  }
2824 };
2825 
2832 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
2833 {
2834  PRECONDITION(expr.id()==ID_bitand);
2835  // DATA_INVARIANT(
2836  // expr.operands().size()>=2,
2837  // "Bit-wise and must have two or more operands");
2838  return static_cast<const bitand_exprt &>(expr);
2839 }
2840 
2843 {
2844  PRECONDITION(expr.id()==ID_bitand);
2845  // DATA_INVARIANT(
2846  // expr.operands().size()>=2,
2847  // "Bit-wise and must have two or more operands");
2848  return static_cast<bitand_exprt &>(expr);
2849 }
2850 
2851 template<> inline bool can_cast_expr<bitand_exprt>(const exprt &base)
2852 {
2853  return base.id()==ID_bitand;
2854 }
2855 // inline void validate_expr(const bitand_exprt &value)
2856 // {
2857 // validate_operands(
2858 // value,
2859 // 2,
2860 // "Bit-wise and must have two or more operands",
2861 // true);
2862 // }
2863 
2864 
2867 {
2868 public:
2869  DEPRECATED("use shift_exprt(value, id, distance) instead")
2870  explicit shift_exprt(const irep_idt &_id):binary_exprt(_id)
2871  {
2872  }
2873 
2874  DEPRECATED("use shift_exprt(value, id, distance) instead")
2875  shift_exprt(const irep_idt &_id, const typet &_type):
2876  binary_exprt(_id, _type)
2877  {
2878  }
2879 
2880  shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance):
2881  binary_exprt(_src, _id, _distance)
2882  {
2883  }
2884 
2885  shift_exprt(
2886  const exprt &_src,
2887  const irep_idt &_id,
2888  const std::size_t _distance);
2889 
2891  {
2892  return op0();
2893  }
2894 
2895  const exprt &op() const
2896  {
2897  return op0();
2898  }
2899 
2901  {
2902  return op1();
2903  }
2904 
2905  const exprt &distance() const
2906  {
2907  return op1();
2908  }
2909 };
2910 
2917 inline const shift_exprt &to_shift_expr(const exprt &expr)
2918 {
2920  expr.operands().size()==2,
2921  "Shifts must have two operands");
2922  return static_cast<const shift_exprt &>(expr);
2923 }
2924 
2927 {
2929  expr.operands().size()==2,
2930  "Shifts must have two operands");
2931  return static_cast<shift_exprt &>(expr);
2932 }
2933 
2934 // The to_*_expr function for this type doesn't do any checks before casting,
2935 // therefore the implementation is essentially a static_cast.
2936 // Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
2937 // inline void validate_expr(const shift_exprt &value)
2938 // {
2939 // validate_operands(value, 2, "Shifts must have two operands");
2940 // }
2941 
2942 
2945 {
2946 public:
2947  DEPRECATED("use shl_exprt(value, distance) instead")
2949  {
2950  }
2951 
2952  shl_exprt(const exprt &_src, const exprt &_distance):
2953  shift_exprt(_src, ID_shl, _distance)
2954  {
2955  }
2956 
2957  shl_exprt(const exprt &_src, const std::size_t _distance):
2958  shift_exprt(_src, ID_shl, _distance)
2959  {
2960  }
2961 };
2962 
2965 {
2966 public:
2967  DEPRECATED("use ashl_exprt(value, distance) instead")
2969  {
2970  }
2971 
2972  ashr_exprt(const exprt &_src, const exprt &_distance):
2973  shift_exprt(_src, ID_ashr, _distance)
2974  {
2975  }
2976 
2977  ashr_exprt(const exprt &_src, const std::size_t _distance):
2978  shift_exprt(_src, ID_ashr, _distance)
2979  {
2980  }
2981 };
2982 
2985 {
2986 public:
2987  DEPRECATED("use lshl_exprt(value, distance) instead")
2989  {
2990  }
2991 
2992  lshr_exprt(const exprt &_src, const exprt &_distance):
2993  shift_exprt(_src, ID_lshr, _distance)
2994  {
2995  }
2996 
2997  lshr_exprt(const exprt &_src, const std::size_t _distance):
2998  shift_exprt(_src, ID_lshr, _distance)
2999  {
3000  }
3001 };
3002 
3005 {
3006 public:
3007  DEPRECATED("use replication_exprt(times, value) instead")
3009  {
3010  }
3011 
3012  DEPRECATED("use replication_exprt(times, value) instead")
3013  explicit replication_exprt(const typet &_type):
3014  binary_exprt(ID_replication, _type)
3015  {
3016  }
3017 
3018  replication_exprt(const exprt &_times, const exprt &_src):
3019  binary_exprt(_times, ID_replication, _src)
3020  {
3021  }
3022 
3024  {
3025  return op0();
3026  }
3027 
3028  const exprt &times() const
3029  {
3030  return op0();
3031  }
3032 
3034  {
3035  return op1();
3036  }
3037 
3038  const exprt &op() const
3039  {
3040  return op1();
3041  }
3042 };
3043 
3050 inline const replication_exprt &to_replication_expr(const exprt &expr)
3051 {
3052  PRECONDITION(expr.id()==ID_replication);
3054  expr.operands().size()==2,
3055  "Bit-wise replication must have two operands");
3056  return static_cast<const replication_exprt &>(expr);
3057 }
3058 
3061 {
3062  PRECONDITION(expr.id()==ID_replication);
3064  expr.operands().size()==2,
3065  "Bit-wise replication must have two operands");
3066  return static_cast<replication_exprt &>(expr);
3067 }
3068 
3069 template<> inline bool can_cast_expr<replication_exprt>(const exprt &base)
3070 {
3071  return base.id()==ID_replication;
3072 }
3073 inline void validate_expr(const replication_exprt &value)
3074 {
3075  validate_operands(value, 2, "Bit-wise replication must have two operands");
3076 }
3077 
3078 
3081 {
3082 public:
3083  DEPRECATED("use extractbit_exprt(value, index) instead")
3085  {
3086  }
3087 
3090  const exprt &_src,
3091  const exprt &_index):binary_predicate_exprt(_src, ID_extractbit, _index)
3092  {
3093  }
3094 
3097  const exprt &_src,
3098  const std::size_t _index);
3099 
3101  {
3102  return op0();
3103  }
3104 
3106  {
3107  return op1();
3108  }
3109 
3110  const exprt &src() const
3111  {
3112  return op0();
3113  }
3114 
3115  const exprt &index() const
3116  {
3117  return op1();
3118  }
3119 };
3120 
3127 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
3128 {
3129  PRECONDITION(expr.id()==ID_extractbit);
3131  expr.operands().size()==2,
3132  "Extract bit must have two operands");
3133  return static_cast<const extractbit_exprt &>(expr);
3134 }
3135 
3138 {
3139  PRECONDITION(expr.id()==ID_extractbit);
3141  expr.operands().size()==2,
3142  "Extract bit must have two operands");
3143  return static_cast<extractbit_exprt &>(expr);
3144 }
3145 
3146 template<> inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
3147 {
3148  return base.id()==ID_extractbit;
3149 }
3150 inline void validate_expr(const extractbit_exprt &value)
3151 {
3152  validate_operands(value, 2, "Extract bit must have two operands");
3153 }
3154 
3155 
3158 {
3159 public:
3160  DEPRECATED("use extractbits_exprt(value, upper, lower) instead")
3161  extractbits_exprt():exprt(ID_extractbits)
3162  {
3163  operands().resize(3);
3164  }
3165 
3172  const exprt &_src,
3173  const exprt &_upper,
3174  const exprt &_lower,
3175  const typet &_type):exprt(ID_extractbits, _type)
3176  {
3177  add_to_operands(_src, _upper, _lower);
3178  }
3179 
3180  // NOLINTNEXTLINE(whitespace/line_length)
3183  const exprt &_src,
3184  const std::size_t _upper,
3185  const std::size_t _lower,
3186  const typet &_type);
3187 
3189  {
3190  return op0();
3191  }
3192 
3194  {
3195  return op1();
3196  }
3197 
3199  {
3200  return op2();
3201  }
3202 
3203  const exprt &src() const
3204  {
3205  return op0();
3206  }
3207 
3208  const exprt &upper() const
3209  {
3210  return op1();
3211  }
3212 
3213  const exprt &lower() const
3214  {
3215  return op2();
3216  }
3217 };
3218 
3225 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
3226 {
3227  PRECONDITION(expr.id()==ID_extractbits);
3229  expr.operands().size()==3,
3230  "Extract bits must have three operands");
3231  return static_cast<const extractbits_exprt &>(expr);
3232 }
3233 
3236 {
3237  PRECONDITION(expr.id()==ID_extractbits);
3239  expr.operands().size()==3,
3240  "Extract bits must have three operands");
3241  return static_cast<extractbits_exprt &>(expr);
3242 }
3243 
3244 template<> inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
3245 {
3246  return base.id()==ID_extractbits;
3247 }
3248 inline void validate_expr(const extractbits_exprt &value)
3249 {
3250  validate_operands(value, 3, "Extract bits must have three operands");
3251 }
3252 
3253 
3256 {
3257 public:
3258  explicit address_of_exprt(const exprt &op);
3259 
3260  address_of_exprt(const exprt &op, const pointer_typet &_type):
3261  unary_exprt(ID_address_of, op, _type)
3262  {
3263  }
3264 
3266  {
3267  return op0();
3268  }
3269 
3270  const exprt &object() const
3271  {
3272  return op0();
3273  }
3274 };
3275 
3282 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
3283 {
3284  PRECONDITION(expr.id()==ID_address_of);
3285  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
3286  return static_cast<const address_of_exprt &>(expr);
3287 }
3288 
3291 {
3292  PRECONDITION(expr.id()==ID_address_of);
3293  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
3294  return static_cast<address_of_exprt &>(expr);
3295 }
3296 
3297 template<> inline bool can_cast_expr<address_of_exprt>(const exprt &base)
3298 {
3299  return base.id()==ID_address_of;
3300 }
3301 inline void validate_expr(const address_of_exprt &value)
3302 {
3303  validate_operands(value, 1, "Address of must have one operand");
3304 }
3305 
3306 
3309 {
3310 public:
3311  explicit not_exprt(const exprt &op):
3312  unary_exprt(ID_not, op) // type from op.type()
3313  {
3314  PRECONDITION(op.type().id()==ID_bool);
3315  }
3316 
3318  {
3319  }
3320 };
3321 
3328 inline const not_exprt &to_not_expr(const exprt &expr)
3329 {
3330  PRECONDITION(expr.id()==ID_not);
3331  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
3332  return static_cast<const not_exprt &>(expr);
3333 }
3334 
3337 {
3338  PRECONDITION(expr.id()==ID_not);
3339  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
3340  return static_cast<not_exprt &>(expr);
3341 }
3342 
3343 template<> inline bool can_cast_expr<not_exprt>(const exprt &base)
3344 {
3345  return base.id()==ID_not;
3346 }
3347 
3348 inline void validate_expr(const not_exprt &value)
3349 {
3350  validate_operands(value, 1, "Not must have one operand");
3351 }
3352 
3353 
3356 {
3357 public:
3358  DEPRECATED("use dereference_exprt(pointer) instead")
3359  dereference_exprt():unary_exprt(ID_dereference)
3360  {
3361  }
3362 
3363  DEPRECATED("use dereference_exprt(pointer) instead")
3364  explicit dereference_exprt(const typet &type):
3365  unary_exprt(ID_dereference, type)
3366  {
3367  }
3368 
3369  explicit dereference_exprt(const exprt &op):
3370  unary_exprt(ID_dereference, op, op.type().subtype())
3371  {
3372  PRECONDITION(op.type().id()==ID_pointer);
3373  }
3374 
3376  unary_exprt(ID_dereference, op, type)
3377  {
3378  }
3379 
3381  {
3382  return op0();
3383  }
3384 
3385  const exprt &pointer() const
3386  {
3387  return op0();
3388  }
3389 };
3390 
3397 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
3398 {
3399  PRECONDITION(expr.id()==ID_dereference);
3401  expr.operands().size()==1,
3402  "Dereference must have one operand");
3403  return static_cast<const dereference_exprt &>(expr);
3404 }
3405 
3408 {
3409  PRECONDITION(expr.id()==ID_dereference);
3411  expr.operands().size()==1,
3412  "Dereference must have one operand");
3413  return static_cast<dereference_exprt &>(expr);
3414 }
3415 
3416 template<> inline bool can_cast_expr<dereference_exprt>(const exprt &base)
3417 {
3418  return base.id()==ID_dereference;
3419 }
3420 inline void validate_expr(const dereference_exprt &value)
3421 {
3422  validate_operands(value, 1, "Dereference must have one operand");
3423 }
3424 
3425 
3427 class if_exprt : public ternary_exprt
3428 {
3429 public:
3430  if_exprt(const exprt &cond, const exprt &t, const exprt &f)
3431  : ternary_exprt(ID_if, cond, t, f, t.type())
3432  {
3433  }
3434 
3435  if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
3436  : ternary_exprt(ID_if, cond, t, f, type)
3437  {
3438  }
3439 
3440  DEPRECATED("use if_exprt(cond, t, f) instead")
3442  {
3443  }
3444 
3446  {
3447  return op0();
3448  }
3449 
3450  const exprt &cond() const
3451  {
3452  return op0();
3453  }
3454 
3456  {
3457  return op1();
3458  }
3459 
3460  const exprt &true_case() const
3461  {
3462  return op1();
3463  }
3464 
3466  {
3467  return op2();
3468  }
3469 
3470  const exprt &false_case() const
3471  {
3472  return op2();
3473  }
3474 };
3475 
3482 inline const if_exprt &to_if_expr(const exprt &expr)
3483 {
3484  PRECONDITION(expr.id()==ID_if);
3486  expr.operands().size()==3,
3487  "If-then-else must have three operands");
3488  return static_cast<const if_exprt &>(expr);
3489 }
3490 
3492 inline if_exprt &to_if_expr(exprt &expr)
3493 {
3494  PRECONDITION(expr.id()==ID_if);
3496  expr.operands().size()==3,
3497  "If-then-else must have three operands");
3498  return static_cast<if_exprt &>(expr);
3499 }
3500 
3501 template<> inline bool can_cast_expr<if_exprt>(const exprt &base)
3502 {
3503  return base.id()==ID_if;
3504 }
3505 inline void validate_expr(const if_exprt &value)
3506 {
3507  validate_operands(value, 3, "If-then-else must have three operands");
3508 }
3509 
3510 
3514 class with_exprt:public exprt
3515 {
3516 public:
3518  const exprt &_old,
3519  const exprt &_where,
3520  const exprt &_new_value):
3521  exprt(ID_with, _old.type())
3522  {
3523  add_to_operands(_old, _where, _new_value);
3524  }
3525 
3526  DEPRECATED("use with_exprt(old, where, new_value) instead")
3527  with_exprt():exprt(ID_with)
3528  {
3529  operands().resize(3);
3530  }
3531 
3533  {
3534  return op0();
3535  }
3536 
3537  const exprt &old() const
3538  {
3539  return op0();
3540  }
3541 
3543  {
3544  return op1();
3545  }
3546 
3547  const exprt &where() const
3548  {
3549  return op1();
3550  }
3551 
3553  {
3554  return op2();
3555  }
3556 
3557  const exprt &new_value() const
3558  {
3559  return op2();
3560  }
3561 };
3562 
3569 inline const with_exprt &to_with_expr(const exprt &expr)
3570 {
3571  PRECONDITION(expr.id()==ID_with);
3573  expr.operands().size()==3,
3574  "Array/structure update must have three operands");
3575  return static_cast<const with_exprt &>(expr);
3576 }
3577 
3580 {
3581  PRECONDITION(expr.id()==ID_with);
3583  expr.operands().size()==3,
3584  "Array/structure update must have three operands");
3585  return static_cast<with_exprt &>(expr);
3586 }
3587 
3588 template<> inline bool can_cast_expr<with_exprt>(const exprt &base)
3589 {
3590  return base.id()==ID_with;
3591 }
3592 inline void validate_expr(const with_exprt &value)
3593 {
3595  value,
3596  3,
3597  "Array/structure update must have three operands");
3598 }
3599 
3600 
3602 {
3603 public:
3604  explicit index_designatort(const exprt &_index):
3605  exprt(ID_index_designator)
3606  {
3607  add_to_operands(_index);
3608  }
3609 
3610  const exprt &index() const
3611  {
3612  return op0();
3613  }
3614 
3616  {
3617  return op0();
3618  }
3619 };
3620 
3627 inline const index_designatort &to_index_designator(const exprt &expr)
3628 {
3629  PRECONDITION(expr.id()==ID_index_designator);
3631  expr.operands().size()==1,
3632  "Index designator must have one operand");
3633  return static_cast<const index_designatort &>(expr);
3634 }
3635 
3638 {
3639  PRECONDITION(expr.id()==ID_index_designator);
3641  expr.operands().size()==1,
3642  "Index designator must have one operand");
3643  return static_cast<index_designatort &>(expr);
3644 }
3645 
3646 template<> inline bool can_cast_expr<index_designatort>(const exprt &base)
3647 {
3648  return base.id()==ID_index_designator;
3649 }
3650 inline void validate_expr(const index_designatort &value)
3651 {
3652  validate_operands(value, 1, "Index designator must have one operand");
3653 }
3654 
3655 
3657 {
3658 public:
3659  explicit member_designatort(const irep_idt &_component_name):
3660  exprt(ID_member_designator)
3661  {
3662  set(ID_component_name, _component_name);
3663  }
3664 
3666  {
3667  return get(ID_component_name);
3668  }
3669 };
3670 
3678 {
3679  PRECONDITION(expr.id()==ID_member_designator);
3681  !expr.has_operands(),
3682  "Member designator must not have operands");
3683  return static_cast<const member_designatort &>(expr);
3684 }
3685 
3688 {
3689  PRECONDITION(expr.id()==ID_member_designator);
3691  !expr.has_operands(),
3692  "Member designator must not have operands");
3693  return static_cast<member_designatort &>(expr);
3694 }
3695 
3696 template<> inline bool can_cast_expr<member_designatort>(const exprt &base)
3697 {
3698  return base.id()==ID_member_designator;
3699 }
3700 inline void validate_expr(const member_designatort &value)
3701 {
3702  validate_operands(value, 0, "Member designator must not have operands");
3703 }
3704 
3705 
3708 {
3709 public:
3711  const exprt &_old,
3712  const exprt &_designator,
3713  const exprt &_new_value)
3714  : ternary_exprt(ID_update, _old, _designator, _new_value, _old.type())
3715  {
3716  }
3717 
3718  DEPRECATED("use update_exprt(old, where, new_value) instead")
3719  explicit update_exprt(const typet &_type) : ternary_exprt(ID_update, _type)
3720  {
3721  }
3722 
3723  DEPRECATED("use update_exprt(old, where, new_value) instead")
3725  {
3726  op1().id(ID_designator);
3727  }
3728 
3730  {
3731  return op0();
3732  }
3733 
3734  const exprt &old() const
3735  {
3736  return op0();
3737  }
3738 
3739  // the designator operands are either
3740  // 1) member_designator or
3741  // 2) index_designator
3742  // as defined above
3744  {
3745  return op1().operands();
3746  }
3747 
3749  {
3750  return op1().operands();
3751  }
3752 
3754  {
3755  return op2();
3756  }
3757 
3758  const exprt &new_value() const
3759  {
3760  return op2();
3761  }
3762 };
3763 
3770 inline const update_exprt &to_update_expr(const exprt &expr)
3771 {
3772  PRECONDITION(expr.id()==ID_update);
3774  expr.operands().size()==3,
3775  "Array/structure update must have three operands");
3776  return static_cast<const update_exprt &>(expr);
3777 }
3778 
3781 {
3782  PRECONDITION(expr.id()==ID_update);
3784  expr.operands().size()==3,
3785  "Array/structure update must have three operands");
3786  return static_cast<update_exprt &>(expr);
3787 }
3788 
3789 template<> inline bool can_cast_expr<update_exprt>(const exprt &base)
3790 {
3791  return base.id()==ID_update;
3792 }
3793 inline void validate_expr(const update_exprt &value)
3794 {
3796  value,
3797  3,
3798  "Array/structure update must have three operands");
3799 }
3800 
3801 
3802 #if 0
3803 class array_update_exprt:public exprt
3805 {
3806 public:
3807  array_update_exprt(
3808  const exprt &_array,
3809  const exprt &_index,
3810  const exprt &_new_value):
3811  exprt(ID_array_update, _array.type())
3812  {
3813  add_to_operands(_array, _index, _new_value);
3814  }
3815 
3816  array_update_exprt():exprt(ID_array_update)
3817  {
3818  operands().resize(3);
3819  }
3820 
3821  exprt &array()
3822  {
3823  return op0();
3824  }
3825 
3826  const exprt &array() const
3827  {
3828  return op0();
3829  }
3830 
3831  exprt &index()
3832  {
3833  return op1();
3834  }
3835 
3836  const exprt &index() const
3837  {
3838  return op1();
3839  }
3840 
3841  exprt &new_value()
3842  {
3843  return op2();
3844  }
3845 
3846  const exprt &new_value() const
3847  {
3848  return op2();
3849  }
3850 };
3851 
3858 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3859 {
3860  PRECONDITION(expr.id()==ID_array_update);
3862  expr.operands().size()==3,
3863  "Array update must have three operands");
3864  return static_cast<const array_update_exprt &>(expr);
3865 }
3866 
3868 inline array_update_exprt &to_array_update_expr(exprt &expr)
3869 {
3870  PRECONDITION(expr.id()==ID_array_update);
3872  expr.operands().size()==3,
3873  "Array update must have three operands");
3874  return static_cast<array_update_exprt &>(expr);
3875 }
3876 
3877 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
3878 {
3879  return base.id()==ID_array_update;
3880 }
3881 inline void validate_expr(const array_update_exprt &value)
3882 {
3883  validate_operands(value, 3, "Array update must have three operands");
3884 }
3885 
3886 #endif
3887 
3888 
3891 {
3892 public:
3894  const exprt &op,
3895  const irep_idt &component_name,
3896  const typet &_type):
3897  unary_exprt(ID_member, op, _type)
3898  {
3899  set_component_name(component_name);
3900  }
3901 
3903  const exprt &op,
3904  const struct_typet::componentt &c):
3905  unary_exprt(ID_member, op, c.type())
3906  {
3908  }
3909 
3910  DEPRECATED("use member_exprt(op, c) instead")
3912  {
3913  }
3914 
3916  {
3917  return get(ID_component_name);
3918  }
3919 
3920  void set_component_name(const irep_idt &component_name)
3921  {
3922  set(ID_component_name, component_name);
3923  }
3924 
3925  std::size_t get_component_number() const
3926  {
3927  return get_size_t(ID_component_number);
3928  }
3929 
3930  // will go away, use compound()
3931  const exprt &struct_op() const
3932  {
3933  return op0();
3934  }
3935 
3936  // will go away, use compound()
3938  {
3939  return op0();
3940  }
3941 
3942  const exprt &compound() const
3943  {
3944  return op0();
3945  }
3946 
3948  {
3949  return op0();
3950  }
3951 };
3952 
3959 inline const member_exprt &to_member_expr(const exprt &expr)
3960 {
3961  PRECONDITION(expr.id()==ID_member);
3963  expr.operands().size()==1,
3964  "Extract member must have one operand");
3965  return static_cast<const member_exprt &>(expr);
3966 }
3967 
3970 {
3971  PRECONDITION(expr.id()==ID_member);
3973  expr.operands().size()==1,
3974  "Extract member must have one operand");
3975  return static_cast<member_exprt &>(expr);
3976 }
3977 
3978 template<> inline bool can_cast_expr<member_exprt>(const exprt &base)
3979 {
3980  return base.id()==ID_member;
3981 }
3982 inline void validate_expr(const member_exprt &value)
3983 {
3984  validate_operands(value, 1, "Extract member must have one operand");
3985 }
3986 
3987 
3990 {
3991 public:
3992  explicit isnan_exprt(const exprt &op):
3993  unary_predicate_exprt(ID_isnan, op)
3994  {
3995  }
3996 
3997  DEPRECATED("use isnan_exprt(op) instead")
3999  {
4000  }
4001 };
4002 
4009 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
4010 {
4011  PRECONDITION(expr.id()==ID_isnan);
4012  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
4013  return static_cast<const isnan_exprt &>(expr);
4014 }
4015 
4018 {
4019  PRECONDITION(expr.id()==ID_isnan);
4020  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
4021  return static_cast<isnan_exprt &>(expr);
4022 }
4023 
4024 template<> inline bool can_cast_expr<isnan_exprt>(const exprt &base)
4025 {
4026  return base.id()==ID_isnan;
4027 }
4028 inline void validate_expr(const isnan_exprt &value)
4029 {
4030  validate_operands(value, 1, "Is NaN must have one operand");
4031 }
4032 
4033 
4036 {
4037 public:
4038  explicit isinf_exprt(const exprt &op):
4039  unary_predicate_exprt(ID_isinf, op)
4040  {
4041  }
4042 
4043  DEPRECATED("use isinf_exprt(op) instead")
4045  {
4046  }
4047 };
4048 
4055 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
4056 {
4057  PRECONDITION(expr.id()==ID_isinf);
4059  expr.operands().size()==1,
4060  "Is infinite must have one operand");
4061  return static_cast<const isinf_exprt &>(expr);
4062 }
4063 
4066 {
4067  PRECONDITION(expr.id()==ID_isinf);
4069  expr.operands().size()==1,
4070  "Is infinite must have one operand");
4071  return static_cast<isinf_exprt &>(expr);
4072 }
4073 
4074 template<> inline bool can_cast_expr<isinf_exprt>(const exprt &base)
4075 {
4076  return base.id()==ID_isinf;
4077 }
4078 inline void validate_expr(const isinf_exprt &value)
4079 {
4080  validate_operands(value, 1, "Is infinite must have one operand");
4081 }
4082 
4083 
4086 {
4087 public:
4088  explicit isfinite_exprt(const exprt &op):
4089  unary_predicate_exprt(ID_isfinite, op)
4090  {
4091  }
4092 
4093  DEPRECATED("use isfinite_exprt(op) instead")
4095  {
4096  }
4097 };
4098 
4105 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
4106 {
4107  PRECONDITION(expr.id()==ID_isfinite);
4108  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
4109  return static_cast<const isfinite_exprt &>(expr);
4110 }
4111 
4114 {
4115  PRECONDITION(expr.id()==ID_isfinite);
4116  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
4117  return static_cast<isfinite_exprt &>(expr);
4118 }
4119 
4120 template<> inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
4121 {
4122  return base.id()==ID_isfinite;
4123 }
4124 inline void validate_expr(const isfinite_exprt &value)
4125 {
4126  validate_operands(value, 1, "Is finite must have one operand");
4127 }
4128 
4129 
4132 {
4133 public:
4134  explicit isnormal_exprt(const exprt &op):
4135  unary_predicate_exprt(ID_isnormal, op)
4136  {
4137  }
4138 
4139  DEPRECATED("use isnormal_exprt(op) instead")
4141  {
4142  }
4143 };
4144 
4151 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
4152 {
4153  PRECONDITION(expr.id()==ID_isnormal);
4154  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
4155  return static_cast<const isnormal_exprt &>(expr);
4156 }
4157 
4160 {
4161  PRECONDITION(expr.id()==ID_isnormal);
4162  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
4163  return static_cast<isnormal_exprt &>(expr);
4164 }
4165 
4166 template<> inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
4167 {
4168  return base.id()==ID_isnormal;
4169 }
4170 inline void validate_expr(const isnormal_exprt &value)
4171 {
4172  validate_operands(value, 1, "Is normal must have one operand");
4173 }
4174 
4175 
4178 {
4179 public:
4180  DEPRECATED("use ieee_float_equal_exprt(lhs, rhs) instead")
4182  {
4183  }
4184 
4185  ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs):
4186  binary_relation_exprt(_lhs, ID_ieee_float_equal, _rhs)
4187  {
4188  }
4189 };
4190 
4198 {
4199  PRECONDITION(expr.id()==ID_ieee_float_equal);
4201  expr.operands().size()==2,
4202  "IEEE equality must have two operands");
4203  return static_cast<const ieee_float_equal_exprt &>(expr);
4204 }
4205 
4208 {
4209  PRECONDITION(expr.id()==ID_ieee_float_equal);
4211  expr.operands().size()==2,
4212  "IEEE equality must have two operands");
4213  return static_cast<ieee_float_equal_exprt &>(expr);
4214 }
4215 
4216 template<>
4218 {
4219  return base.id()==ID_ieee_float_equal;
4220 }
4221 inline void validate_expr(const ieee_float_equal_exprt &value)
4222 {
4223  validate_operands(value, 2, "IEEE equality must have two operands");
4224 }
4225 
4226 
4229 {
4230 public:
4231  DEPRECATED("use ieee_float_notequal_exprt(lhs, rhs) instead")
4233  binary_relation_exprt(ID_ieee_float_notequal)
4234  {
4235  }
4236 
4237  ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs):
4238  binary_relation_exprt(_lhs, ID_ieee_float_notequal, _rhs)
4239  {
4240  }
4241 };
4242 
4250  const exprt &expr)
4251 {
4252  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4254  expr.operands().size()==2,
4255  "IEEE inequality must have two operands");
4256  return static_cast<const ieee_float_notequal_exprt &>(expr);
4257 }
4258 
4261 {
4262  PRECONDITION(expr.id()==ID_ieee_float_notequal);
4264  expr.operands().size()==2,
4265  "IEEE inequality must have two operands");
4266  return static_cast<ieee_float_notequal_exprt &>(expr);
4267 }
4268 
4269 template<>
4271 {
4272  return base.id()==ID_ieee_float_notequal;
4273 }
4274 inline void validate_expr(const ieee_float_notequal_exprt &value)
4275 {
4276  validate_operands(value, 2, "IEEE inequality must have two operands");
4277 }
4278 
4283 {
4284 public:
4285  DEPRECATED("use ieee_float_op_exprt(lhs, id, rhs, rm) instead")
4287  {
4288  operands().resize(3);
4289  }
4290 
4292  const exprt &_lhs,
4293  const irep_idt &_id,
4294  const exprt &_rhs,
4295  const exprt &_rm)
4296  : exprt(_id, _lhs.type())
4297  {
4298  add_to_operands(_lhs, _rhs, _rm);
4299  }
4300 
4302  {
4303  return op0();
4304  }
4305 
4306  const exprt &lhs() const
4307  {
4308  return op0();
4309  }
4310 
4312  {
4313  return op1();
4314  }
4315 
4316  const exprt &rhs() const
4317  {
4318  return op1();
4319  }
4320 
4322  {
4323  return op2();
4324  }
4325 
4326  const exprt &rounding_mode() const
4327  {
4328  return op2();
4329  }
4330 };
4331 
4339 {
4341  expr.operands().size()==3,
4342  "IEEE float operations must have three arguments");
4343  return static_cast<const ieee_float_op_exprt &>(expr);
4344 }
4345 
4348 {
4350  expr.operands().size()==3,
4351  "IEEE float operations must have three arguments");
4352  return static_cast<ieee_float_op_exprt &>(expr);
4353 }
4354 
4355 // The to_*_expr function for this type doesn't do any checks before casting,
4356 // therefore the implementation is essentially a static_cast.
4357 // Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
4358 // template<>
4359 // inline void validate_expr<ieee_float_op_exprt>(
4360 // const ieee_float_op_exprt &value)
4361 // {
4362 // validate_operands(
4363 // value,
4364 // 3,
4365 // "IEEE float operations must have three arguments");
4366 // }
4367 
4368 
4371 {
4372 public:
4373  DEPRECATED("use type_exprt(type) instead")
4375  {
4376  }
4377 
4378  explicit type_exprt(const typet &type) : nullary_exprt(ID_type, type)
4379  {
4380  }
4381 };
4382 
4384 class constant_exprt:public exprt
4385 {
4386 public:
4387  DEPRECATED("use constant_exprt(value, type) instead")
4388  constant_exprt():exprt(ID_constant)
4389  {
4390  }
4391 
4392  DEPRECATED("use constant_exprt(value, type) instead")
4393  explicit constant_exprt(const typet &type):exprt(ID_constant, type)
4394  {
4395  }
4396 
4397  constant_exprt(const irep_idt &_value, const typet &_type):
4398  exprt(ID_constant, _type)
4399  {
4400  set_value(_value);
4401  }
4402 
4403  const irep_idt &get_value() const
4404  {
4405  return get(ID_value);
4406  }
4407 
4408  void set_value(const irep_idt &value)
4409  {
4410  set(ID_value, value);
4411  }
4412 
4413  bool value_is_zero_string() const;
4414 };
4415 
4416 
4423 inline const constant_exprt &to_constant_expr(const exprt &expr)
4424 {
4425  PRECONDITION(expr.id()==ID_constant);
4426  return static_cast<const constant_exprt &>(expr);
4427 }
4428 
4431 {
4432  PRECONDITION(expr.id()==ID_constant);
4433  return static_cast<constant_exprt &>(expr);
4434 }
4435 
4436 template<> inline bool can_cast_expr<constant_exprt>(const exprt &base)
4437 {
4438  return base.id()==ID_constant;
4439 }
4440 
4441 
4444 {
4445 public:
4447  {
4448  }
4449 };
4450 
4453 {
4454 public:
4456  {
4457  }
4458 };
4459 
4461 class nil_exprt : public nullary_exprt
4462 {
4463 public:
4465  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
4466  {
4467  }
4468 };
4469 
4472 {
4473 public:
4475  : constant_exprt(ID_NULL, type)
4476  {
4477  }
4478 };
4479 
4482 {
4483 public:
4485 
4487  const symbol_exprt &_function,
4488  const argumentst &_arguments,
4489  const typet &_type)
4490  : binary_exprt(ID_function_application, _type)
4491  {
4492  function()=_function;
4493  arguments() = _arguments;
4494  }
4495 
4496  symbol_exprt &function()
4497  {
4498  return static_cast<symbol_exprt &>(op0());
4499  }
4500 
4501  const symbol_exprt &function() const
4502  {
4503  return static_cast<const symbol_exprt &>(op0());
4504  }
4505 
4507  {
4508  return op1().operands();
4509  }
4510 
4511  const argumentst &arguments() const
4512  {
4513  return op1().operands();
4514  }
4515 };
4516 
4524  const exprt &expr)
4525 {
4526  PRECONDITION(expr.id()==ID_function_application);
4528  expr.operands().size()==2,
4529  "Function application must have two operands");
4530  return static_cast<const function_application_exprt &>(expr);
4531 }
4532 
4535 {
4536  PRECONDITION(expr.id()==ID_function_application);
4538  expr.operands().size()==2,
4539  "Function application must have two operands");
4540  return static_cast<function_application_exprt &>(expr);
4541 }
4542 
4543 template<>
4545 {
4546  return base.id()==ID_function_application;
4547 }
4549 {
4550  validate_operands(value, 2, "Function application must have two operands");
4551 }
4552 
4559 {
4560 public:
4561  DEPRECATED("use concatenation_exprt(op, type) instead")
4562  concatenation_exprt() : multi_ary_exprt(ID_concatenation)
4563  {
4564  }
4565 
4566  DEPRECATED("use concatenation_exprt(op, type) instead")
4567  explicit concatenation_exprt(const typet &_type)
4568  : multi_ary_exprt(ID_concatenation, _type)
4569  {
4570  }
4571 
4572  concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
4573  : multi_ary_exprt(_op0, ID_concatenation, _op1, _type)
4574  {
4575  }
4576 
4577  concatenation_exprt(operandst &&_operands, const typet &_type)
4578  : multi_ary_exprt(ID_concatenation, std::move(_operands), _type)
4579  {
4580  }
4581 };
4582 
4590 {
4591  PRECONDITION(expr.id()==ID_concatenation);
4592  // DATA_INVARIANT(
4593  // expr.operands().size()>=2,
4594  // "Concatenation must have two or more operands");
4595  return static_cast<const concatenation_exprt &>(expr);
4596 }
4597 
4600 {
4601  PRECONDITION(expr.id()==ID_concatenation);
4602  // DATA_INVARIANT(
4603  // expr.operands().size()>=2,
4604  // "Concatenation must have two or more operands");
4605  return static_cast<concatenation_exprt &>(expr);
4606 }
4607 
4608 template<> inline bool can_cast_expr<concatenation_exprt>(const exprt &base)
4609 {
4610  return base.id()==ID_concatenation;
4611 }
4612 // template<>
4613 // inline void validate_expr<concatenation_exprt>(
4614 // const concatenation_exprt &value)
4615 // {
4616 // validate_operands(
4617 // value,
4618 // 2,
4619 // "Concatenation must have two or more operands",
4620 // true);
4621 // }
4622 
4623 
4626 {
4627 public:
4628  explicit infinity_exprt(const typet &_type)
4629  : nullary_exprt(ID_infinity, _type)
4630  {
4631  }
4632 };
4633 
4635 class let_exprt : public ternary_exprt
4636 {
4637 public:
4639  const symbol_exprt &symbol,
4640  const exprt &value,
4641  const exprt &where)
4642  : ternary_exprt(ID_let, symbol, value, where, where.type())
4643  {
4644  }
4645 
4647  {
4648  return static_cast<symbol_exprt &>(op0());
4649  }
4650 
4651  const symbol_exprt &symbol() const
4652  {
4653  return static_cast<const symbol_exprt &>(op0());
4654  }
4655 
4657  {
4658  return op1();
4659  }
4660 
4661  const exprt &value() const
4662  {
4663  return op1();
4664  }
4665 
4667  {
4668  return op2();
4669  }
4670 
4671  const exprt &where() const
4672  {
4673  return op2();
4674  }
4675 };
4676 
4683 inline const let_exprt &to_let_expr(const exprt &expr)
4684 {
4685  PRECONDITION(expr.id()==ID_let);
4686  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
4687  return static_cast<const let_exprt &>(expr);
4688 }
4689 
4692 {
4693  PRECONDITION(expr.id()==ID_let);
4694  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
4695  return static_cast<let_exprt &>(expr);
4696 }
4697 
4698 template<> inline bool can_cast_expr<let_exprt>(const exprt &base)
4699 {
4700  return base.id()==ID_let;
4701 }
4702 inline void validate_expr(const let_exprt &value)
4703 {
4704  validate_operands(value, 3, "Let must have three operands");
4705 }
4706 
4709 {
4710 public:
4712  const irep_idt &_id,
4713  const symbol_exprt &_symbol,
4714  const exprt &_where)
4715  : binary_predicate_exprt(_symbol, _id, _where)
4716  {
4717  }
4718 
4720  {
4721  return static_cast<symbol_exprt &>(op0());
4722  }
4723 
4724  const symbol_exprt &symbol() const
4725  {
4726  return static_cast<const symbol_exprt &>(op0());
4727  }
4728 
4730  {
4731  return op1();
4732  }
4733 
4734  const exprt &where() const
4735  {
4736  return op1();
4737  }
4738 };
4739 
4746 inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
4747 {
4748  DATA_INVARIANT(expr.operands().size()==2,
4749  "quantifier expressions must have two operands");
4751  expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
4752  return static_cast<const quantifier_exprt &>(expr);
4753 }
4754 
4757 {
4758  DATA_INVARIANT(expr.operands().size()==2,
4759  "quantifier expressions must have two operands");
4761  expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
4762  return static_cast<quantifier_exprt &>(expr);
4763 }
4764 
4765 template<> inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
4766 {
4767  return base.id() == ID_forall || base.id() == ID_exists;
4768 }
4769 
4770 inline void validate_expr(const quantifier_exprt &value)
4771 {
4772  validate_operands(value, 2,
4773  "quantifier expressions must have two operands");
4774 }
4775 
4778 {
4779 public:
4780  forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
4781  : quantifier_exprt(ID_forall, _symbol, _where)
4782  {
4783  }
4784 };
4785 
4788 {
4789 public:
4790  exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
4791  : quantifier_exprt(ID_exists, _symbol, _where)
4792  {
4793  }
4794 };
4795 
4796 inline const exists_exprt &to_exists_expr(const exprt &expr)
4797 {
4798  PRECONDITION(expr.id() == ID_exists);
4800  expr.operands().size() == 2,
4801  "exists expressions have exactly two operands");
4802  return static_cast<const exists_exprt &>(expr);
4803 }
4804 
4806 {
4807  PRECONDITION(expr.id() == ID_exists);
4809  expr.operands().size() == 2,
4810  "exists expressions have exactly two operands");
4811  return static_cast<exists_exprt &>(expr);
4812 }
4813 
4816 {
4817 public:
4818  DEPRECATED("use popcount_exprt(op, type) instead")
4819  popcount_exprt(): unary_exprt(ID_popcount)
4820  {
4821  }
4822 
4823  popcount_exprt(const exprt &_op, const typet &_type)
4824  : unary_exprt(ID_popcount, _op, _type)
4825  {
4826  }
4827 
4828  explicit popcount_exprt(const exprt &_op)
4829  : unary_exprt(ID_popcount, _op, _op.type())
4830  {
4831  }
4832 };
4833 
4840 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
4841 {
4842  PRECONDITION(expr.id() == ID_popcount);
4843  DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand");
4844  return static_cast<const popcount_exprt &>(expr);
4845 }
4846 
4849 {
4850  PRECONDITION(expr.id() == ID_popcount);
4851  DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand");
4852  return static_cast<popcount_exprt &>(expr);
4853 }
4854 
4855 template <>
4856 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
4857 {
4858  return base.id() == ID_popcount;
4859 }
4860 inline void validate_expr(const popcount_exprt &value)
4861 {
4862  validate_operands(value, 1, "popcount must have one operand");
4863 }
4864 
4869 {
4870 public:
4871  explicit cond_exprt(const typet &_type) : multi_ary_exprt(ID_cond, _type)
4872  {
4873  }
4874 
4878  void add_case(const exprt &condition, const exprt &value)
4879  {
4880  PRECONDITION(condition.type().id() == ID_bool);
4881  operands().reserve(operands().size() + 2);
4882  operands().push_back(condition);
4883  operands().push_back(value);
4884  }
4885 };
4886 
4893 inline const cond_exprt &to_cond_expr(const exprt &expr)
4894 {
4895  PRECONDITION(expr.id() == ID_cond);
4897  expr.operands().size() % 2 != 0, "cond must have even number of operands");
4898  return static_cast<const cond_exprt &>(expr);
4899 }
4900 
4903 {
4904  PRECONDITION(expr.id() == ID_cond);
4906  expr.operands().size() % 2 != 0, "cond must have even number of operands");
4907  return static_cast<cond_exprt &>(expr);
4908 }
4909 
4910 #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:3482
bool can_cast_expr< rem_exprt >(const exprt &base)
Definition: std_expr.h:1372
const irept & get_nil_irep()
Definition: irep.cpp:55
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:187
const transt & to_trans_expr(const exprt &expr)
Cast an exprt to a transt expr must be known to be transt.
Definition: std_expr.h:113
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:4197
const irep_idt & get_name() const
Definition: std_types.h:132
bitnot_exprt(const exprt &op)
Definition: std_expr.h:2662
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:3789
bool can_cast_expr< bitxor_exprt >(const exprt &base)
Definition: std_expr.h:2796
The type of an expression, extends irept.
Definition: type.h:27
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2520
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:1011
exprt & invar()
Definition: std_expr.h:100
bool can_cast_expr< isnormal_exprt >(const exprt &base)
Definition: std_expr.h:4166
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast an exprt to a factorial_power_exprt.
Definition: std_expr.h:1453
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:515
Boolean negation.
Definition: std_expr.h:3308
unary_minus_exprt(const exprt &_op, const typet &_type)
Definition: std_expr.h:477
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: std_expr.h:600
exprt & true_case()
Definition: std_expr.h:3455
Semantic type conversion.
Definition: std_expr.h:2277
or_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:2538
const exprt & rhs() const
Definition: std_expr.h:4316
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1200
bool can_cast_expr< quantifier_exprt >(const exprt &base)
Definition: std_expr.h:4765
An expression without operands.
Definition: std_expr.h:23
bool can_cast_expr< bitnot_exprt >(const exprt &base)
Definition: std_expr.h:2691
function_application_exprt(const symbol_exprt &_function, const argumentst &_arguments, const typet &_type)
Definition: std_expr.h:4486
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:666
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
cond_exprt(const typet &_type)
Definition: std_expr.h:4871
const exprt & value() const
Definition: std_expr.h:4661
if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
Definition: std_expr.h:3435
const exprt & lhs() const
Definition: std_expr.h:926
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
Definition: std_expr.h:2832
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1128
Application of (mathematical) function.
Definition: std_expr.h:4481
exprt & object()
Definition: std_expr.h:3265
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:288
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4780
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2325
index_exprt(const exprt &_array, const exprt &_index)
Definition: std_expr.h:1608
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1309
ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:4237
Boolean OR.
Definition: std_expr.h:2531
bool can_cast_expr< transt >(const exprt &base)
Definition: std_expr.h:132
exprt & op0()
Definition: expr.h:84
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:770
const exprt & src() const
Definition: std_expr.h:3110
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1257
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1076
let_exprt(const symbol_exprt &symbol, const exprt &value, const exprt &where)
Definition: std_expr.h:4638
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: std_expr.h:2245
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:790
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:710
Operator to update elements in structs and arrays.
Definition: std_expr.h:3707
const exprt & op() const
Definition: std_expr.h:371
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:540
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: std_expr.h:4608
const exprt & pointer() const
Definition: std_expr.h:3385
Evaluates to true if the operand is infinite.
Definition: std_expr.h:4035
const exprt & op() const
Definition: std_expr.h:3038
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1759
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:166
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3588
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
Definition: std_expr.h:2421
unsigned int get_instance() const
Definition: std_expr.cpp:45
exprt & struct_op()
Definition: std_expr.h:3937
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
Definition: std_expr.h:2777
Mathematical types.
const exprt & real() const
Definition: std_expr.h:1989
const exprt & array() const
Definition: std_expr.h:1626
bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
Definition: std_expr.h:571
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1728
const irep_idt & get_identifier() const
Definition: std_expr.h:176
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
Definition: std_expr.h:2543
exprt::operandst & designator()
Definition: std_expr.h:3743
exprt & lower()
Definition: std_expr.h:3198
shift_exprt(const irep_idt &_id)
Definition: std_expr.h:2870
const exprt & op3() const =delete
ternary_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
Definition: std_expr.h:76
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:4878
exprt imag()
Definition: std_expr.h:1994
const irep_idt & get_value() const
Definition: std_expr.h:4403
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:2176
The null pointer constant.
Definition: std_expr.h:4471
argumentst & arguments()
Definition: std_expr.h:4506
An expression denoting a type.
Definition: std_expr.h:4370
abs_exprt(const exprt &_op)
Definition: std_expr.h:427
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:3696
type_exprt(const typet &type)
Definition: std_expr.h:4378
concatenation_exprt(operandst &&_operands, const typet &_type)
Definition: std_expr.h:4577
plus_exprt(const exprt &_lhs, const exprt &_rhs, const typet &_type)
Definition: std_expr.h:1061
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
Definition: std_expr.h:2723
const exprt & op1() const =delete
Transition system, consisting of state invariant, initial state predicate, and transition predicate...
Definition: std_expr.h:93
bool is_thread_local() const
Definition: std_expr.h:229
exprt real()
Definition: std_expr.h:1984
The trinary if-then-else operator.
Definition: std_expr.h:3427
exprt & cond()
Definition: std_expr.h:3445
std::size_t get_component_number() const
Definition: std_expr.h:3925
const exists_exprt & to_exists_expr(const exprt &expr)
Definition: std_expr.h:4796
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:4131
exprt & old()
Definition: std_expr.h:3532
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1245
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:2102
exprt & new_value()
Definition: std_expr.h:3552
multi_ary_exprt(const irep_idt &_id, operandst &&_operands, const typet &_type)
Definition: std_expr.h:993
typet & type()
Return the type of the expression.
Definition: expr.h:68
const symbol_exprt & symbol() const
Definition: std_expr.h:4724
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
Definition: std_expr.h:1472
bool can_cast_expr< extractbit_exprt >(const exprt &base)
Definition: std_expr.h:3146
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2577
bool can_cast_expr< bitand_exprt >(const exprt &base)
Definition: std_expr.h:2851
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:3282
const exprt & op2() const =delete
const exprt & where() const
Definition: std_expr.h:4734
The Boolean type.
Definition: std_types.h:28
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1789
const exprt & where() const
Definition: std_expr.h:3547
A constant literal expression.
Definition: std_expr.h:4384
exprt & distance()
Definition: std_expr.h:2900
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1324
exprt & rounding_mode()
Definition: std_expr.h:4321
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1239
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2474
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1233
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:3646
const exprt & index() const
Definition: std_expr.h:1636
const exprt & op3() const =delete
symbol_exprt(const typet &type)
Definition: std_expr.h:159
const exprt & lower() const
Definition: std_expr.h:3213
const exprt & where() const
Definition: std_expr.h:4671
irep_idt get_component_name() const
Definition: std_expr.h:3665
Boolean implication.
Definition: std_expr.h:2485
bool value_is_zero_string() const
Definition: std_expr.cpp:20
Exponentiation.
Definition: std_expr.h:1383
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2087
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:728
void set_bits_per_byte(std::size_t bits_per_byte)
Definition: std_expr.h:588
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:4249
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4683
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:206
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1878
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const exprt &_rm)
Definition: std_expr.h:4291
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
Definition: std_expr.h:2549
vector_exprt(const vector_typet &_type)
Definition: std_expr.h:1808
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Definition: std_expr.h:4217
Extract member of struct or union.
Definition: std_expr.h:3890
const exprt & imag() const
Definition: std_expr.h:1999
const exprt & rounding_mode() const
Definition: std_expr.h:2366
extractbits_exprt(const exprt &_src, const exprt &_upper, const exprt &_lower, const typet &_type)
Extract the bits [_lower .
Definition: std_expr.h:3171
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:3343
exprt & where()
Definition: std_expr.h:4666
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
Concatenation of bit-vector operands.
Definition: std_expr.h:4558
Equality.
Definition: std_expr.h:1484
symbol_exprt & symbol()
Definition: std_expr.h:4719
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1565
bool can_cast_expr< bitor_exprt >(const exprt &base)
Definition: std_expr.h:2742
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:1095
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1276
const exprt & op() const
Definition: std_expr.h:2895
Templated functions to cast to specific exprt-derived classes.
constant_exprt(const irep_idt &_value, const typet &_type)
Definition: std_expr.h:4397
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2505
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3920
bool can_cast_expr< function_application_exprt >(const exprt &base)
Definition: std_expr.h:4544
binary_predicate_exprt(const exprt &_op0, const irep_idt &_id, const exprt &_op1)
Definition: std_expr.h:849
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:4338
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:3942
exprt & op()
Definition: std_expr.h:376
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:761
bswap_exprt(const exprt &_op, std::size_t bits_per_byte)
Definition: std_expr.h:577
if_exprt(const exprt &cond, const exprt &t, const exprt &f)
Definition: std_expr.h:3430
const exprt & src() const
Definition: std_expr.h:3203
const irep_idt & id() const
Definition: irep.h:259
dereference_exprt(const exprt &op, const typet &type)
Definition: std_expr.h:3375
popcount_exprt(const exprt &_op)
Definition: std_expr.h:4828
const exprt & op2() const =delete
The unary plus expression.
Definition: std_expr.h:525
void set_value(const irep_idt &value)
Definition: std_expr.h:4408
const exprt & times() const
Definition: std_expr.h:3028
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3989
Bit-wise OR.
Definition: std_expr.h:2702
bool can_cast_expr< isnan_exprt >(const exprt &base)
Definition: std_expr.h:4024
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:4893
An expression denoting infinity.
Definition: std_expr.h:4625
shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance)
Definition: std_expr.h:2880
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:1147
The Boolean constant true.
Definition: std_expr.h:4443
unary_exprt(const irep_idt &_id, const exprt &_op, const typet &_type)
Definition: std_expr.h:362
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition: std_expr.h:184
Division.
Definition: std_expr.h:1211
binary_relation_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:892
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: std_expr.h:3050
A base class for binary expressions.
Definition: std_expr.h:738
const exprt & invar() const
Definition: std_expr.h:104
decorated_symbol_exprt(const irep_idt &identifier, const typet &type)
Definition: std_expr.h:208
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4589
exprt & init()
Definition: std_expr.h:101
exprt & old()
Definition: std_expr.h:3729
const exprt & distance() const
Definition: std_expr.h:2905
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3770
exprt & times()
Definition: std_expr.h:3023
const irep_idt & get_identifier() const
Definition: std_expr.h:293
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1820
The NIL expression.
Definition: std_expr.h:4461
Real part of the expression describing a complex number.
Definition: std_expr.h:2040
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:123
unary_minus_exprt(const exprt &_op)
Definition: std_expr.h:484
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:1507
IEEE floating-point disequality.
Definition: std_expr.h:4228
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:3978
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:3127
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1504
member_exprt(const exprt &op, const struct_typet::componentt &c)
Definition: std_expr.h:3902
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1833
const exprt & op3() const =delete
const exprt & op1() const =delete
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:2075
Operator to dereference a pointer.
Definition: std_expr.h:3355
operandst & operands()=delete
remove all operand methods
exprt & rounding_mode()
Definition: std_expr.h:2361
The vector type.
Definition: std_types.h:1755
const exprt & op0() const =delete
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:320
exprt & src()
Definition: std_expr.h:3188
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1709
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:2030
Union constructor from single element.
Definition: std_expr.h:1840
std::size_t get_component_number() const
Definition: std_expr.h:1873
Boolean AND.
Definition: std_expr.h:2409
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3157
factorial_power_exprt(const exprt &_base, const exprt &_exp)
Definition: std_expr.h:1439
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:827
const exprt & new_value() const
Definition: std_expr.h:3758
popcount_exprt(const exprt &_op, const typet &_type)
Definition: std_expr.h:4823
not_exprt(const exprt &op)
Definition: std_expr.h:3311
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: std_expr.h:4055
exprt & op1()
Definition: expr.h:87
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: std_expr.h:4523
const exprt & lhs() const
Definition: std_expr.h:4306
and_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:2416
Generic base class for unary expressions.
Definition: std_expr.h:331
Disequality.
Definition: std_expr.h:1545
exprt::operandst argumentst
Definition: std_expr.h:4484
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
Definition: std_expr.h:1002
infinity_exprt(const typet &_type)
Definition: std_expr.h:4628
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:2197
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:558
An expression with three operands.
Definition: std_expr.h:59
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1909
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:3225
Left shift.
Definition: std_expr.h:2944
const exprt & what() const
Definition: std_expr.h:1697
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:948
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:346
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const exprt & false_case() const
Definition: std_expr.h:3470
typecast_exprt(const typet &_type)
Definition: std_expr.h:2281
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: std_expr.h:3244
lshr_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2997
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
const exprt & cond() const
Definition: std_expr.h:3450
A forall expression.
Definition: std_expr.h:4777
with_exprt(const exprt &_old, const exprt &_where, const exprt &_new_value)
Definition: std_expr.h:3517
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:4436
symbol_exprt(const irep_idt &identifier, const typet &type)
Definition: std_expr.h:165
const symbol_exprt & symbol() const
Definition: std_expr.h:4651
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
Definition: std_expr.h:2398
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
null_pointer_exprt(const pointer_typet &type)
Definition: std_expr.h:4474
ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:4185
exprt & where()
Definition: std_expr.h:4729
void set_static_lifetime()
Definition: std_expr.h:219
Array constructor from single element.
Definition: std_expr.h:1678
exprt & upper()
Definition: std_expr.h:3193
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: std_expr.h:4746
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2639
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:26
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1497
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:458
power_exprt(const exprt &_base, const exprt &_exp)
Definition: std_expr.h:1391
isfinite_exprt(const exprt &op)
Definition: std_expr.h:4088
Logical right shift.
Definition: std_expr.h:2984
exprt & compound()
Definition: std_expr.h:3947
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:3627
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:2122
Vector constructor from list of elements.
Definition: std_expr.h:1800
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const exprt & old() const
Definition: std_expr.h:3537
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: std_expr.h:4105
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:2596
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: std_expr.h:3416
Operator to return the address of an object.
Definition: std_expr.h:3255
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1942
The unary minus expression.
Definition: std_expr.h:469
transt()
Definition: std_expr.h:96
exprt & false_case()
Definition: std_expr.h:3465
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: std_expr.h:2265
concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
Definition: std_expr.h:4572
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
implies_exprt(const exprt &op0, const exprt &op1)
Definition: std_expr.h:2493
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:641
union_exprt(const irep_idt &_component_name, const exprt &_value, const typet &_type)
Definition: std_expr.h:1854
member_exprt(const exprt &op, const irep_idt &component_name, const typet &_type)
Definition: std_expr.h:3893
quantifier_exprt(const irep_idt &_id, const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4711
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
const exprt & index() const
Definition: std_expr.h:3610
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:3297
The Boolean constant false.
Definition: std_expr.h:4452
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:856
or_exprt()
Definition: std_expr.h:2534
const exprt & init() const
Definition: std_expr.h:105
bool can_cast_expr< replication_exprt >(const exprt &base)
Definition: std_expr.h:3069
exprt & index()
Definition: std_expr.h:3105
const exprt & rhs() const
Definition: std_expr.h:936
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2378
exprt & trans()
Definition: std_expr.h:102
equal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1492
void validate_expr(const transt &value)
Definition: std_expr.h:136
const exprt & trans() const
Definition: std_expr.h:106
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2291
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2626
std::vector< exprt > operandst
Definition: expr.h:57
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
const exprt::operandst & designator() const
Definition: std_expr.h:3748
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: std_expr.h:4270
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1584
#define DEPRECATED(msg)
Definition: deprecate.h:23
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1181
const exprt & object() const
Definition: std_expr.h:2152
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
Definition: std_expr.h:1405
minus_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1114
Boolean XOR.
Definition: std_expr.h:2607
index_designatort(const exprt &_index)
Definition: std_expr.h:3604
Complex numbers made of pair of given subtype.
Definition: std_types.h:1807
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4840
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3569
Bit-wise XOR.
Definition: std_expr.h:2757
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:1028
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1519
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:266
dynamic_object_exprt(const typet &type)
Definition: std_expr.h:2217
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:2090
Pre-defined types.
const exprt & op3() const =delete
typecast_exprt(const exprt &op, const typet &_type)
Definition: std_expr.h:2285
const exprt & old() const
Definition: std_expr.h:3734
const exprt & object() const
Definition: std_expr.h:3270
plus_exprt(const typet &type)
Definition: std_expr.h:1050
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: std_expr.h:4009
plus_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1054
update_exprt(const exprt &_old, const exprt &_designator, const exprt &_new_value)
Definition: std_expr.h:3710
exprt & value()
Definition: std_expr.h:4656
Expression to hold a nondeterministic choice.
Definition: std_expr.h:277
bitand_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2819
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2917
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2455
exprt & index()
Definition: std_expr.h:1631
shl_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2952
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4815
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
Definition: std_expr.h:1357
Evaluates to true if the operand is finite.
Definition: std_expr.h:4085
const exprt & index() const
Definition: std_expr.h:3115
ashr_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2972
exprt & op()
Definition: std_expr.h:2890
std::size_t get_bits_per_byte() const
Definition: std_expr.h:583
xor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2614
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2336
div_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1219
shl_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2957
Base class for all expressions.
Definition: expr.h:54
exprt & pointer()
Definition: std_expr.h:3380
Absolute value.
Definition: std_expr.h:419
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:690
const exprt & root_object() const
Definition: std_expr.cpp:199
floatbv_typecast_exprt(const exprt &op, const exprt &rounding, const typet &_type)
Definition: std_expr.h:2344
const exprt & struct_op() const
Definition: std_expr.h:3931
const exprt & rounding_mode() const
Definition: std_expr.h:4326
isnormal_exprt(const exprt &op)
Definition: std_expr.h:4134
nondet_symbol_exprt(const irep_idt &identifier, const typet &type)
Definition: std_expr.h:282
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:965
dereference_exprt(const exprt &op)
Definition: std_expr.h:3369
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:2011
complex_real_exprt(const exprt &op)
Definition: std_expr.h:2043
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1890
const exprt & op2() const =delete
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast an exprt to a factorial_power_exprt.
Definition: std_expr.h:1463
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
const exprt & upper() const
Definition: std_expr.h:3208
sign_exprt(const exprt &_op)
Definition: std_expr.h:698
A base class for quantifier expressions.
Definition: std_expr.h:4708
lshr_exprt(const exprt &_src, const exprt &_distance)
Definition: std_expr.h:2992
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:900
unary_predicate_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:680
irep_idt get_component_name() const
Definition: std_expr.h:3915
const exprt & offset() const
Definition: std_expr.h:2164
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:4698
rem_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1343
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3328
Remainder of division.
Definition: std_expr.h:1335
const exprt & valid() const
Definition: std_expr.h:2233
bitor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2710
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1838
const exprt & true_case() const
Definition: std_expr.h:3460
exprt & index()
Definition: std_expr.h:3615
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
#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
array_exprt(const array_typet &_type)
Definition: std_expr.h:1747
exprt & op()
Definition: std_expr.h:3033
irep_idt get_component_name() const
Definition: std_expr.h:1863
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:412
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1868
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:439
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
Definition: std_expr.h:2427
bool is_static_lifetime() const
Definition: std_expr.h:214
isinf_exprt(const exprt &op)
Definition: std_expr.h:4038
Arrays with given size.
Definition: std_types.h:1000
bool can_cast_expr< bswap_exprt >(const exprt &base)
Definition: std_expr.h:620
Binary minus.
Definition: std_expr.h:1106
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:780
Bit-wise AND.
Definition: std_expr.h:2811
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: std_expr.h:4790
validation_modet
isnan_exprt(const exprt &op)
Definition: std_expr.h:3992
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: std_expr.h:4074
exprt & what()
Definition: std_expr.h:1692
exprt & op2()
Definition: expr.h:90
bool can_cast_expr< power_exprt >(const exprt &base)
Definition: std_expr.h:1420
ashr_exprt(const exprt &_src, const std::size_t _distance)
Definition: std_expr.h:2977
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:863
bool can_cast_expr< isfinite_exprt >(const exprt &base)
Definition: std_expr.h:4120
exprt & new_value()
Definition: std_expr.h:3753
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1955
replication_exprt(const exprt &_times, const exprt &_src)
Definition: std_expr.h:3018
symbol_exprt & symbol()
Definition: std_expr.h:4646
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:810
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:835
Arithmetic right shift.
Definition: std_expr.h:2964
struct_exprt(const typet &_type)
Definition: std_expr.h:1928
An exists expression.
Definition: std_expr.h:4787
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1667
exprt & where()
Definition: std_expr.h:3542
Base Type Computation.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: std_expr.h:2674
A let expression.
Definition: std_expr.h:4635
void clear_static_lifetime()
Definition: std_expr.h:224
#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:1227
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: std_expr.h:4151
Representation of heap-allocated objects.
Definition: std_expr.h:2208
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:305
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:973
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:395
operandst & operands()
Definition: expr.h:78
mult_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1167
mod_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1295
void copy_to_operands(const exprt &expr)=delete
exprt & src()
Definition: std_expr.h:3100
bitxor_exprt(const exprt &_op0, const exprt &_op1)
Definition: std_expr.h:2765
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2654
index_exprt(const exprt &_array, const exprt &_index, const typet &_type)
Definition: std_expr.h:1613
Struct constructor from list of elements.
Definition: std_expr.h:1920
unary_plus_exprt(const exprt &op)
Definition: std_expr.h:528
extractbit_exprt(const exprt &_src, const exprt &_index)
Extract the _index-th least significant bit from _src.
Definition: std_expr.h:3089
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:3501
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
Falling factorial power.
Definition: std_expr.h:1431
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:2055
notequal_exprt(const exprt &_lhs, const exprt &_rhs)
Definition: std_expr.h:1553
complex_exprt(const exprt &_real, const exprt &_imag, const complex_typet &_type)
Definition: std_expr.h:1976
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:4282
Bit-vector replication.
Definition: std_expr.h:3004
exprt & array()
Definition: std_expr.h:1621
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:1648
array_list_exprt(const array_typet &_type)
Definition: std_expr.h:1782
A base class for shift operators.
Definition: std_expr.h:2866
const argumentst & arguments() const
Definition: std_expr.h:4511
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt&#39;s operands.
Definition: expr.h:130
Array constructor from list of elements.
Definition: std_expr.h:1739
nullary_exprt(const irep_idt &_id, const typet &_type)
Definition: std_expr.h:32
Complex constructor from a pair of numbers.
Definition: std_expr.h:1962
Modulo.
Definition: std_expr.h:1287
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1772
The byte swap expression.
Definition: std_expr.h:568
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:496
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:3659
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: std_expr.h:4856
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:907
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
Definition: std_expr.h:1779
array_of_exprt(const exprt &_what, const array_typet &_type)
Definition: std_expr.h:1686
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:3677
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:4868
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:3080
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:633
IEEE-floating-point equality.
Definition: std_expr.h:4177
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1534
Array index operator.
Definition: std_expr.h:1595
exprt & op3()
Definition: expr.h:93
address_of_exprt(const exprt &op, const pointer_typet &_type)
Definition: std_expr.h:3260
const exprt & new_value() const
Definition: std_expr.h:3557
const exprt & op() const
Definition: std_expr.h:2356