CBMC
floatbv_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for floating-point arithmetic
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_FLOATBV_EXPR_H
10 #define CPROVER_UTIL_FLOATBV_EXPR_H
11 
14 
15 #include "std_expr.h"
16 
19 {
20 public:
22  : binary_exprt(
23  std::move(op),
24  ID_floatbv_typecast,
25  std::move(rounding),
26  std::move(_type))
27  {
28  }
29 
30  exprt &op()
31  {
32  return op0();
33  }
34 
35  const exprt &op() const
36  {
37  return op0();
38  }
39 
41  {
42  return op1();
43  }
44 
45  const exprt &rounding_mode() const
46  {
47  return op1();
48  }
49 };
50 
51 template <>
53 {
54  return base.id() == ID_floatbv_typecast;
55 }
56 
57 inline void validate_expr(const floatbv_typecast_exprt &value)
58 {
59  validate_operands(value, 2, "Float typecast must have two operands");
60 }
61 
69 {
70  PRECONDITION(expr.id() == ID_floatbv_typecast);
71  const floatbv_typecast_exprt &ret =
72  static_cast<const floatbv_typecast_exprt &>(expr);
73  validate_expr(ret);
74  return ret;
75 }
76 
79 {
80  PRECONDITION(expr.id() == ID_floatbv_typecast);
81  floatbv_typecast_exprt &ret = static_cast<floatbv_typecast_exprt &>(expr);
82  validate_expr(ret);
83  return ret;
84 }
85 
88 {
89 public:
90  explicit isnan_exprt(exprt op)
91  : unary_predicate_exprt(ID_isnan, std::move(op))
92  {
93  }
94 };
95 
96 template <>
97 inline bool can_cast_expr<isnan_exprt>(const exprt &base)
98 {
99  return base.id() == ID_isnan;
100 }
101 
102 inline void validate_expr(const isnan_exprt &value)
103 {
104  validate_operands(value, 1, "Is NaN must have one operand");
105 }
106 
113 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
114 {
115  PRECONDITION(expr.id() == ID_isnan);
116  const isnan_exprt &ret = static_cast<const isnan_exprt &>(expr);
117  validate_expr(ret);
118  return ret;
119 }
120 
123 {
124  PRECONDITION(expr.id() == ID_isnan);
125  isnan_exprt &ret = static_cast<isnan_exprt &>(expr);
126  validate_expr(ret);
127  return ret;
128 }
129 
132 {
133 public:
134  explicit isinf_exprt(exprt op)
135  : unary_predicate_exprt(ID_isinf, std::move(op))
136  {
137  }
138 };
139 
140 template <>
141 inline bool can_cast_expr<isinf_exprt>(const exprt &base)
142 {
143  return base.id() == ID_isinf;
144 }
145 
146 inline void validate_expr(const isinf_exprt &value)
147 {
148  validate_operands(value, 1, "Is infinite must have one operand");
149 }
150 
157 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
158 {
159  PRECONDITION(expr.id() == ID_isinf);
160  const isinf_exprt &ret = static_cast<const isinf_exprt &>(expr);
161  validate_expr(ret);
162  return ret;
163 }
164 
167 {
168  PRECONDITION(expr.id() == ID_isinf);
169  isinf_exprt &ret = static_cast<isinf_exprt &>(expr);
170  validate_expr(ret);
171  return ret;
172 }
173 
176 {
177 public:
179  : unary_predicate_exprt(ID_isfinite, std::move(op))
180  {
181  }
182 };
183 
184 template <>
185 inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
186 {
187  return base.id() == ID_isfinite;
188 }
189 
190 inline void validate_expr(const isfinite_exprt &value)
191 {
192  validate_operands(value, 1, "Is finite must have one operand");
193 }
194 
201 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
202 {
203  PRECONDITION(expr.id() == ID_isfinite);
204  const isfinite_exprt &ret = static_cast<const isfinite_exprt &>(expr);
205  validate_expr(ret);
206  return ret;
207 }
208 
211 {
212  PRECONDITION(expr.id() == ID_isfinite);
213  isfinite_exprt &ret = static_cast<isfinite_exprt &>(expr);
214  validate_expr(ret);
215  return ret;
216 }
217 
220 {
221 public:
223  : unary_predicate_exprt(ID_isnormal, std::move(op))
224  {
225  }
226 };
227 
228 template <>
229 inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
230 {
231  return base.id() == ID_isnormal;
232 }
233 
234 inline void validate_expr(const isnormal_exprt &value)
235 {
236  validate_operands(value, 1, "Is normal must have one operand");
237 }
238 
245 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
246 {
247  PRECONDITION(expr.id() == ID_isnormal);
248  const isnormal_exprt &ret = static_cast<const isnormal_exprt &>(expr);
249  validate_expr(ret);
250  return ret;
251 }
252 
255 {
256  PRECONDITION(expr.id() == ID_isnormal);
257  isnormal_exprt &ret = static_cast<isnormal_exprt &>(expr);
258  validate_expr(ret);
259  return ret;
260 }
261 
264 {
265 public:
268  std::move(_lhs),
269  ID_ieee_float_equal,
270  std::move(_rhs))
271  {
272  }
273 };
274 
275 template <>
277 {
278  return base.id() == ID_ieee_float_equal;
279 }
280 
281 inline void validate_expr(const ieee_float_equal_exprt &value)
282 {
283  validate_operands(value, 2, "IEEE equality must have two operands");
284 }
285 
293 {
294  PRECONDITION(expr.id() == ID_ieee_float_equal);
295  const ieee_float_equal_exprt &ret =
296  static_cast<const ieee_float_equal_exprt &>(expr);
297  validate_expr(ret);
298  return ret;
299 }
300 
303 {
304  PRECONDITION(expr.id() == ID_ieee_float_equal);
305  ieee_float_equal_exprt &ret = static_cast<ieee_float_equal_exprt &>(expr);
306  validate_expr(ret);
307  return ret;
308 }
309 
312 {
313 public:
316  std::move(_lhs),
317  ID_ieee_float_notequal,
318  std::move(_rhs))
319  {
320  }
321 };
322 
323 template <>
325 {
326  return base.id() == ID_ieee_float_notequal;
327 }
328 
329 inline void validate_expr(const ieee_float_notequal_exprt &value)
330 {
331  validate_operands(value, 2, "IEEE inequality must have two operands");
332 }
333 
340 inline const ieee_float_notequal_exprt &
342 {
343  PRECONDITION(expr.id() == ID_ieee_float_notequal);
344  const ieee_float_notequal_exprt &ret =
345  static_cast<const ieee_float_notequal_exprt &>(expr);
346  validate_expr(ret);
347  return ret;
348 }
349 
352 {
353  PRECONDITION(expr.id() == ID_ieee_float_notequal);
355  static_cast<ieee_float_notequal_exprt &>(expr);
356  validate_expr(ret);
357  return ret;
358 }
359 
364 {
365 public:
367  const exprt &_lhs,
368  const irep_idt &_id,
369  exprt _rhs,
370  exprt _rm)
371  : ternary_exprt(_id, _lhs, std::move(_rhs), std::move(_rm), _lhs.type())
372  {
373  }
374 
376  {
377  return op0();
378  }
379 
380  const exprt &lhs() const
381  {
382  return op0();
383  }
384 
386  {
387  return op1();
388  }
389 
390  const exprt &rhs() const
391  {
392  return op1();
393  }
394 
396  {
397  return op2();
398  }
399 
400  const exprt &rounding_mode() const
401  {
402  return op2();
403  }
404 };
405 
406 template <>
408 {
409  return base.id() == ID_floatbv_plus || base.id() == ID_floatbv_minus ||
410  base.id() == ID_floatbv_div || base.id() == ID_floatbv_mult;
411 }
412 
413 inline void validate_expr(const ieee_float_op_exprt &value)
414 {
416  value, 3, "IEEE float operations must have three arguments");
417 }
418 
426 {
427  const ieee_float_op_exprt &ret =
428  static_cast<const ieee_float_op_exprt &>(expr);
429  validate_expr(ret);
430  return ret;
431 }
432 
435 {
436  ieee_float_op_exprt &ret = static_cast<ieee_float_op_exprt &>(expr);
437  validate_expr(ret);
438  return ret;
439 }
440 
445 
446 #endif // CPROVER_UTIL_FLOATBV_EXPR_H
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
A constant literal expression.
Definition: std_expr.h:2990
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
const exprt & rounding_mode() const
Definition: floatbv_expr.h:45
const exprt & op() const
Definition: floatbv_expr.h:35
floatbv_typecast_exprt(exprt op, exprt rounding, typet _type)
Definition: floatbv_expr.h:21
IEEE-floating-point equality.
Definition: floatbv_expr.h:264
ieee_float_equal_exprt(exprt _lhs, exprt _rhs)
Definition: floatbv_expr.h:266
IEEE floating-point disequality.
Definition: floatbv_expr.h:312
ieee_float_notequal_exprt(exprt _lhs, exprt _rhs)
Definition: floatbv_expr.h:314
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs, exprt _rm)
Definition: floatbv_expr.h:366
const exprt & rhs() const
Definition: floatbv_expr.h:390
exprt & rounding_mode()
Definition: floatbv_expr.h:395
const exprt & rounding_mode() const
Definition: floatbv_expr.h:400
const exprt & lhs() const
Definition: floatbv_expr.h:380
const irep_idt & id() const
Definition: irep.h:388
Evaluates to true if the operand is finite.
Definition: floatbv_expr.h:176
isfinite_exprt(exprt op)
Definition: floatbv_expr.h:178
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
isinf_exprt(exprt op)
Definition: floatbv_expr.h:134
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
isnan_exprt(exprt op)
Definition: floatbv_expr.h:90
Evaluates to true if the operand is a normal number.
Definition: floatbv_expr.h:220
isnormal_exprt(exprt op)
Definition: floatbv_expr.h:222
An expression with three operands.
Definition: std_expr.h:67
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:391
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:585
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
bool can_cast_expr< isnan_exprt >(const exprt &base)
Definition: floatbv_expr.h:97
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: floatbv_expr.h:245
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
Definition: floatbv_expr.h:52
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: floatbv_expr.h:113
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: floatbv_expr.h:141
constant_exprt floatbv_rounding_mode(unsigned)
returns the a rounding mode expression for a given IEEE rounding mode, encoded using the recommendati...
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
bool can_cast_expr< isfinite_exprt >(const exprt &base)
Definition: floatbv_expr.h:185
bool can_cast_expr< isnormal_exprt >(const exprt &base)
Definition: floatbv_expr.h:229
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: floatbv_expr.h:201
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
Definition: floatbv_expr.h:341
bool can_cast_expr< ieee_float_op_exprt >(const exprt &base)
Definition: floatbv_expr.h:407
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Definition: floatbv_expr.h:276
void validate_expr(const floatbv_typecast_exprt &value)
Definition: floatbv_expr.h:57
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: floatbv_expr.h:324
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
Definition: floatbv_expr.h:292
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: floatbv_expr.h:157
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.