CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
floatbv_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes for floating-point arithmetic
4
5Author: 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{
20public:
23 std::move(op),
25 std::move(rounding),
26 std::move(_type))
27 {
28 }
29
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
51template <>
53{
54 return base.id() == ID_floatbv_typecast;
55}
56
57inline void validate_expr(const floatbv_typecast_exprt &value)
58{
59 validate_operands(value, 2, "Float typecast must have two operands");
60}
61
69{
72 static_cast<const floatbv_typecast_exprt &>(expr);
74 return ret;
75}
76
85
89{
90public:
99
101 {
102 return op0();
103 }
104
105 const exprt &op() const
106 {
107 return op0();
108 }
109
111 {
112 return op1();
113 }
114
115 const exprt &rounding_mode() const
116 {
117 return op1();
118 }
119};
120
121template <>
123{
124 return base.id() == ID_floatbv_round_to_integral;
125}
126
140
149
152{
153public:
156 {
157 }
158};
159
160template <>
161inline bool can_cast_expr<isnan_exprt>(const exprt &base)
162{
163 return base.id() == ID_isnan;
164}
165
166inline void validate_expr(const isnan_exprt &value)
167{
168 validate_operands(value, 1, "Is NaN must have one operand");
169}
170
177inline const isnan_exprt &to_isnan_expr(const exprt &expr)
178{
179 PRECONDITION(expr.id() == ID_isnan);
180 const isnan_exprt &ret = static_cast<const isnan_exprt &>(expr);
182 return ret;
183}
184
187{
188 PRECONDITION(expr.id() == ID_isnan);
189 isnan_exprt &ret = static_cast<isnan_exprt &>(expr);
191 return ret;
192}
193
196{
197public:
200 {
201 }
202};
203
204template <>
205inline bool can_cast_expr<isinf_exprt>(const exprt &base)
206{
207 return base.id() == ID_isinf;
208}
209
210inline void validate_expr(const isinf_exprt &value)
211{
212 validate_operands(value, 1, "Is infinite must have one operand");
213}
214
221inline const isinf_exprt &to_isinf_expr(const exprt &expr)
222{
223 PRECONDITION(expr.id() == ID_isinf);
224 const isinf_exprt &ret = static_cast<const isinf_exprt &>(expr);
226 return ret;
227}
228
231{
232 PRECONDITION(expr.id() == ID_isinf);
233 isinf_exprt &ret = static_cast<isinf_exprt &>(expr);
235 return ret;
236}
237
240{
241public:
244 {
245 }
246};
247
248template <>
249inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
250{
251 return base.id() == ID_isfinite;
252}
253
254inline void validate_expr(const isfinite_exprt &value)
255{
256 validate_operands(value, 1, "Is finite must have one operand");
257}
258
265inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
266{
267 PRECONDITION(expr.id() == ID_isfinite);
268 const isfinite_exprt &ret = static_cast<const isfinite_exprt &>(expr);
270 return ret;
271}
272
275{
276 PRECONDITION(expr.id() == ID_isfinite);
277 isfinite_exprt &ret = static_cast<isfinite_exprt &>(expr);
279 return ret;
280}
281
284{
285public:
288 {
289 }
290};
291
292template <>
293inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
294{
295 return base.id() == ID_isnormal;
296}
297
298inline void validate_expr(const isnormal_exprt &value)
299{
300 validate_operands(value, 1, "Is normal must have one operand");
301}
302
309inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
310{
311 PRECONDITION(expr.id() == ID_isnormal);
312 const isnormal_exprt &ret = static_cast<const isnormal_exprt &>(expr);
314 return ret;
315}
316
319{
320 PRECONDITION(expr.id() == ID_isnormal);
321 isnormal_exprt &ret = static_cast<isnormal_exprt &>(expr);
323 return ret;
324}
325
338
339template <>
341{
342 return base.id() == ID_ieee_float_equal;
343}
344
345inline void validate_expr(const ieee_float_equal_exprt &value)
346{
347 validate_operands(value, 2, "IEEE equality must have two operands");
348}
349
357{
360 static_cast<const ieee_float_equal_exprt &>(expr);
362 return ret;
363}
364
373
386
387template <>
389{
390 return base.id() == ID_ieee_float_notequal;
391}
392
394{
395 validate_operands(value, 2, "IEEE inequality must have two operands");
396}
397
404inline const ieee_float_notequal_exprt &
406{
409 static_cast<const ieee_float_notequal_exprt &>(expr);
411 return ret;
412}
413
423
428{
429public:
431 const exprt &_lhs,
432 const irep_idt &_id,
433 exprt _rhs,
434 exprt _rm)
435 : ternary_exprt(_id, _lhs, std::move(_rhs), std::move(_rm), _lhs.type())
436 {
437 }
438
440 {
441 return op0();
442 }
443
444 const exprt &lhs() const
445 {
446 return op0();
447 }
448
450 {
451 return op1();
452 }
453
454 const exprt &rhs() const
455 {
456 return op1();
457 }
458
460 {
461 return op2();
462 }
463
464 const exprt &rounding_mode() const
465 {
466 return op2();
467 }
468};
469
470template <>
472{
473 return base.id() == ID_floatbv_plus || base.id() == ID_floatbv_minus ||
474 base.id() == ID_floatbv_div || base.id() == ID_floatbv_mult;
475}
476
477inline void validate_expr(const ieee_float_op_exprt &value)
478{
480 value, 3, "IEEE float operations must have three arguments");
481}
482
490{
491 const ieee_float_op_exprt &ret =
492 static_cast<const ieee_float_op_exprt &>(expr);
494 return ret;
495}
496
499{
500 ieee_float_op_exprt &ret = static_cast<ieee_float_op_exprt &>(expr);
502 return ret;
503}
504
516
524{
525 PRECONDITION(expr.id() == ID_floatbv_mod);
527 return static_cast<const floatbv_mod_exprt &>(expr);
528}
529
532{
533 PRECONDITION(expr.id() == ID_floatbv_mod);
535 return static_cast<floatbv_mod_exprt &>(expr);
536}
537
549
557{
558 PRECONDITION(expr.id() == ID_floatbv_rem);
560 return static_cast<const floatbv_rem_exprt &>(expr);
561}
562
565{
566 PRECONDITION(expr.id() == ID_floatbv_rem);
568 return static_cast<floatbv_rem_exprt &>(expr);
569}
570
575
576#endif // CPROVER_UTIL_FLOATBV_EXPR_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A base class for binary expressions.
Definition std_expr.h:638
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
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:3117
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
static void check(const exprt &, const validation_modet)
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...
Definition expr.h:254
typet & type()
Return the type of the expression.
Definition expr.h:84
IEEE floating-point mod.
floatbv_mod_exprt(exprt _lhs, exprt _rhs)
IEEE floating-point rem.
floatbv_rem_exprt(exprt _lhs, exprt _rhs)
Round a floating-point number to an integral value considering the given rounding mode.
const exprt & rounding_mode() const
floatbv_round_to_integral_exprt(exprt op, exprt rounding)
Semantic type conversion from/to floating-point formats.
const exprt & op() const
const exprt & rounding_mode() const
floatbv_typecast_exprt(exprt op, exprt rounding, typet _type)
IEEE-floating-point equality.
ieee_float_equal_exprt(exprt _lhs, exprt _rhs)
IEEE floating-point disequality.
ieee_float_notequal_exprt(exprt _lhs, exprt _rhs)
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs, exprt _rm)
const exprt & rounding_mode() const
const exprt & rhs() const
const exprt & lhs() const
const irep_idt & id() const
Definition irep.h:388
Evaluates to true if the operand is finite.
isfinite_exprt(exprt op)
Evaluates to true if the operand is infinite.
isinf_exprt(exprt op)
Evaluates to true if the operand is NaN.
isnan_exprt(exprt op)
Evaluates to true if the operand is a normal number.
isnormal_exprt(exprt op)
An expression with three operands.
Definition std_expr.h:67
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
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)
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
bool can_cast_expr< isinf_exprt >(const exprt &base)
const floatbv_round_to_integral_exprt & to_floatbv_round_to_integral_expr(const exprt &expr)
Cast an exprt to a floatbv_round_to_integral_exprt.
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
constant_exprt floatbv_rounding_mode(unsigned)
returns the a rounding mode expression for a given IEEE rounding mode, encoded using the recommendati...
bool can_cast_expr< isfinite_exprt >(const exprt &base)
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
const floatbv_mod_exprt & to_floatbv_mod_expr(const exprt &expr)
Cast an exprt to a floatbv_mod_exprt.
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
bool can_cast_expr< isnormal_exprt >(const exprt &base)
bool can_cast_expr< floatbv_round_to_integral_exprt >(const exprt &base)
bool can_cast_expr< ieee_float_op_exprt >(const exprt &base)
const floatbv_rem_exprt & to_floatbv_rem_expr(const exprt &expr)
Cast an exprt to a floatbv_rem_exprt.
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
void validate_expr(const floatbv_typecast_exprt &value)
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
STL namespace.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.