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 
10 #ifndef CPROVER_UTIL_EXPR_H
11 #define CPROVER_UTIL_EXPR_H
12 
13 #define OPERANDS_IN_GETSUB
14 
15 #include "type.h"
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 #define forall_expr_list(it, expr) \
37  for(expr_listt::const_iterator it=(expr).begin(); \
38  it!=(expr).end(); ++it)
39 
40 #define Forall_expr_list(it, expr) \
41  for(expr_listt::iterator it=(expr).begin(); \
42  it!=(expr).end(); ++it)
43 
46 class exprt:public irept
47 {
48 public:
49  typedef std::vector<exprt> operandst;
50 
51  // constructors
52  exprt() { }
53  explicit exprt(const irep_idt &_id):irept(_id) { }
54  exprt(const irep_idt &_id, const typet &_type):irept(_id)
55  {
56  add(ID_type, _type);
57  }
58 
59  // returns the type of the expression
60  typet &type() { return static_cast<typet &>(add(ID_type)); }
61  const typet &type() const
62  {
63  return static_cast<const typet &>(find(ID_type));
64  }
65 
66  // returns true if there is at least one operand
67  bool has_operands() const
68  { return !operands().empty(); }
69 
70  operandst &operands()
71  #ifdef OPERANDS_IN_GETSUB
72  { return (operandst &)get_sub(); }
73  #else
74  { return (operandst &)(add(ID_operands).get_sub()); }
75  #endif
76 
77  const operandst &operands() const
78  #ifdef OPERANDS_IN_GETSUB
79  { return (const operandst &)get_sub(); }
80  #else
81  { return (const operandst &)(find(ID_operands).get_sub()); }
82  #endif
83 
85  { return operands().front(); }
86 
88  { return operands()[1]; }
89 
91  { return operands()[2]; }
92 
94  { return operands()[3]; }
95 
96  const exprt &op0() const
97  { return operands().front(); }
98 
99  const exprt &op1() const
100  { return operands()[1]; }
101 
102  const exprt &op2() const
103  { return operands()[2]; }
104 
105  const exprt &op3() const
106  { return operands()[3]; }
107 
109  { operands().reserve(n) ; }
110 
111  // destroys expr, e1, e2, e3
112  void move_to_operands(exprt &expr);
113  void move_to_operands(exprt &e1, exprt &e2);
114  void move_to_operands(exprt &e1, exprt &e2, exprt &e3);
115  // does not destroy expr, e1, e2, e3
116  void copy_to_operands(const exprt &expr);
117  void copy_to_operands(const exprt &e1, const exprt &e2);
118  void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3);
119 
120  // the following are deprecated -- use constructors instead
121  void make_typecast(const typet &_type);
122  void make_not();
123 
124  void make_true();
125  void make_false();
126  void make_bool(bool value);
127  void negate();
128 
129  bool sum(const exprt &expr);
130  bool mul(const exprt &expr);
131  bool subtract(const exprt &expr);
132 
133  bool is_constant() const;
134  bool is_true() const;
135  bool is_false() const;
136  bool is_zero() const;
137  bool is_one() const;
138  bool is_boolean() const;
139 
140  const source_locationt &find_source_location() const;
141 
143  {
144  return static_cast<const source_locationt &>(find(ID_C_source_location));
145  }
146 
148  {
149  return static_cast<source_locationt &>(add(ID_C_source_location));
150  }
151 
152  exprt &add_expr(const irep_idt &name)
153  {
154  return static_cast<exprt &>(add(name));
155  }
156 
157  const exprt &find_expr(const irep_idt &name) const
158  {
159  return static_cast<const exprt &>(find(name));
160  }
161 
162  void visit(class expr_visitort &visitor);
163  void visit(class const_expr_visitort &visitor) const;
164 };
165 
166 typedef std::list<exprt> expr_listt;
167 
169 {
170 public:
171  virtual ~expr_visitort() { }
172  virtual void operator()(exprt &expr) { }
173 };
174 
176 {
177 public:
178  virtual ~const_expr_visitort() { }
179  virtual void operator()(const exprt &expr) { }
180 };
181 
182 #endif // CPROVER_UTIL_EXPR_H
virtual void operator()(exprt &expr)
Definition: expr.h:172
The type of an expression.
Definition: type.h:20
bool is_boolean() const
Definition: expr.cpp:231
exprt & op0()
Definition: expr.h:84
const exprt & op3() const
Definition: expr.h:105
const exprt & op2() const
Definition: expr.h:102
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
bool is_false() const
Definition: expr.cpp:140
exprt()
Definition: expr.h:52
exprt(const irep_idt &_id)
Definition: expr.h:53
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:157
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
virtual ~expr_visitort()
Definition: expr.h:171
unsignedbv_typet size_type()
Definition: c_types.cpp:57
void make_bool(bool value)
Definition: expr.cpp:147
subt & get_sub()
Definition: irep.h:245
void make_true()
Definition: expr.cpp:153
void visit(class expr_visitort &visitor)
Definition: expr.cpp:483
const source_locationt & find_source_location() const
Definition: expr.cpp:466
exprt & op1()
Definition: expr.h:87
exprt(const irep_idt &_id, const typet &_type)
Definition: expr.h:54
const operandst & operands() const
Definition: expr.h:77
Base class for tree-like data structures with sharing.
Definition: irep.h:87
const typet & type() const
Definition: expr.h:61
std::list< exprt > expr_listt
Definition: expr.h:166
bool has_operands() const
Definition: expr.h:67
bool is_constant() const
Definition: expr.cpp:128
std::vector< exprt > operandst
Definition: expr.h:49
bool mul(const exprt &expr)
Definition: expr.cpp:374
const exprt & op1() const
Definition: expr.h:99
const exprt & op0() const
Definition: expr.h:96
void make_not()
Definition: expr.cpp:100
Base class for all expressions.
Definition: expr.h:46
virtual void operator()(const exprt &expr)
Definition: expr.h:179
void make_false()
Definition: expr.cpp:159
const source_locationt & source_location() const
Definition: expr.h:142
void negate()
Definition: expr.cpp:165
irept & add(const irep_namet &name)
Definition: irep.cpp:306
bool subtract(const exprt &expr)
Definition: expr.cpp:427
bool is_zero() const
Definition: expr.cpp:236
source_locationt & add_source_location()
Definition: expr.h:147
exprt & op2()
Definition: expr.h:90
exprt & add_expr(const irep_idt &name)
Definition: expr.h:152
virtual ~const_expr_visitort()
Definition: expr.h:178
bool sum(const exprt &expr)
Definition: expr.cpp:321
operandst & operands()
Definition: expr.h:70
void make_typecast(const typet &_type)
Definition: expr.cpp:90
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
bool is_one() const
Definition: expr.cpp:280
exprt & op3()
Definition: expr.h:93