cprover
expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_EXPR_H
10 #define CPROVER_UTIL_EXPR_H
11 
12 #include "type.h"
13 
14 #include <functional>
15 #include <list>
16 
17 #define forall_operands(it, expr) \
18  if((expr).has_operands()) /* NOLINT(readability/braces) */ \
19  for(exprt::operandst::const_iterator it=(expr).operands().begin(), \
20  it##_end=(expr).operands().end(); \
21  it!=it##_end; ++it)
22 
23 #define Forall_operands(it, expr) \
24  if((expr).has_operands()) /* NOLINT(readability/braces) */ \
25  for(exprt::operandst::iterator it=(expr).operands().begin(); \
26  it!=(expr).operands().end(); ++it)
27 
28 #define forall_expr(it, expr) \
29  for(exprt::operandst::const_iterator it=(expr).begin(); \
30  it!=(expr).end(); ++it)
31 
32 #define Forall_expr(it, expr) \
33  for(exprt::operandst::iterator it=(expr).begin(); \
34  it!=(expr).end(); ++it)
35 
36 class depth_iteratort;
39 
42 class exprt:public irept
43 {
44 public:
45  typedef std::vector<exprt> operandst;
46 
47  // constructors
48  exprt() { }
49  explicit exprt(const irep_idt &_id):irept(_id) { }
50  exprt(const irep_idt &_id, const typet &_type):irept(_id)
51  {
52  add(ID_type, _type);
53  }
54 
55  // returns the type of the expression
56  typet &type() { return static_cast<typet &>(add(ID_type)); }
57  const typet &type() const
58  {
59  return static_cast<const typet &>(find(ID_type));
60  }
61 
62  // returns true if there is at least one operand
63  bool has_operands() const
64  { return !operands().empty(); }
65 
67  { return (operandst &)get_sub(); }
68 
69  const operandst &operands() const
70  { return (const operandst &)get_sub(); }
71 
73  { return operands().front(); }
74 
76  { return operands()[1]; }
77 
79  { return operands()[2]; }
80 
82  { return operands()[3]; }
83 
84  const exprt &op0() const
85  { return operands().front(); }
86 
87  const exprt &op1() const
88  { return operands()[1]; }
89 
90  const exprt &op2() const
91  { return operands()[2]; }
92 
93  const exprt &op3() const
94  { return operands()[3]; }
95 
97  { operands().reserve(n) ; }
98 
99  // destroys expr, e1, e2, e3
100  void move_to_operands(exprt &expr);
101  void move_to_operands(exprt &e1, exprt &e2);
102  void move_to_operands(exprt &e1, exprt &e2, exprt &e3);
103  // does not destroy expr, e1, e2, e3
104  void copy_to_operands(const exprt &expr);
105  void copy_to_operands(const exprt &e1, const exprt &e2);
106  void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3);
107 
108  // the following are deprecated -- use constructors instead
109  void make_typecast(const typet &_type);
110  void make_not();
111 
112  void make_true();
113  void make_false();
114  void make_bool(bool value);
115 
116  bool is_constant() const;
117  bool is_true() const;
118  bool is_false() const;
119  bool is_zero() const;
120  bool is_one() const;
121  bool is_boolean() const;
122 
123  const source_locationt &find_source_location() const;
124 
126  {
127  return static_cast<const source_locationt &>(find(ID_C_source_location));
128  }
129 
131  {
132  return static_cast<source_locationt &>(add(ID_C_source_location));
133  }
134 
135  exprt &add_expr(const irep_idt &name)
136  {
137  return static_cast<exprt &>(add(name));
138  }
139 
140  const exprt &find_expr(const irep_idt &name) const
141  {
142  return static_cast<const exprt &>(find(name));
143  }
144 
145  void visit(class expr_visitort &visitor);
146  void visit(class const_expr_visitort &visitor) const;
147 
154  depth_iteratort depth_begin(std::function<exprt &()> mutate_root) const;
159 };
160 
162 {
163 public:
164  virtual ~expr_visitort() { }
165  virtual void operator()(exprt &expr) { }
166 };
167 
169 {
170 public:
171  virtual ~const_expr_visitort() { }
172  virtual void operator()(const exprt &expr) { }
173 };
174 
175 #endif // CPROVER_UTIL_EXPR_H
virtual void operator()(exprt &expr)
Definition: expr.h:165
The type of an expression.
Definition: type.h:22
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:320
bool is_boolean() const
Definition: expr.cpp:156
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:307
exprt & op0()
Definition: expr.h:72
const exprt & op3() const
Definition: expr.h:93
const exprt & op2() const
Definition: expr.h:90
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
bool is_false() const
Definition: expr.cpp:131
exprt()
Definition: expr.h:48
exprt(const irep_idt &_id)
Definition: expr.h:49
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:140
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
virtual ~expr_visitort()
Definition: expr.h:164
unsignedbv_typet size_type()
Definition: c_types.cpp:58
depth_iteratort depth_begin()
Definition: expr.cpp:299
void make_bool(bool value)
Definition: expr.cpp:138
subt & get_sub()
Definition: irep.h:245
void make_true()
Definition: expr.cpp:144
void visit(class expr_visitort &visitor)
Definition: expr.cpp:263
const source_locationt & find_source_location() const
Definition: expr.cpp:246
exprt & op1()
Definition: expr.h:75
exprt(const irep_idt &_id, const typet &_type)
Definition: expr.h:50
const operandst & operands() const
Definition: expr.h:69
Base class for tree-like data structures with sharing.
Definition: irep.h:86
const typet & type() const
Definition: expr.h:57
bool has_operands() const
Definition: expr.h:63
bool is_constant() const
Definition: expr.cpp:119
std::vector< exprt > operandst
Definition: expr.h:45
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:322
const exprt & op1() const
Definition: expr.h:87
const exprt & op0() const
Definition: expr.h:84
void make_not()
Definition: expr.cpp:91
Base class for all expressions.
Definition: expr.h:42
virtual void operator()(const exprt &expr)
Definition: expr.h:172
void make_false()
Definition: expr.cpp:150
const source_locationt & source_location() const
Definition: expr.h:125
const_depth_iteratort depth_cend() const
Definition: expr.cpp:309
irept & add(const irep_namet &name)
Definition: irep.cpp:306
bool is_zero() const
Definition: expr.cpp:161
source_locationt & add_source_location()
Definition: expr.h:130
exprt & op2()
Definition: expr.h:78
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:316
depth_iteratort depth_end()
Definition: expr.cpp:301
exprt & add_expr(const irep_idt &name)
Definition: expr.h:135
virtual ~const_expr_visitort()
Definition: expr.h:171
operandst & operands()
Definition: expr.h:66
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:318
void reserve_operands(operandst::size_type n)
Definition: expr.h:96
bool is_one() const
Definition: expr.cpp:205
exprt & op3()
Definition: expr.h:81