cprover
Loading...
Searching...
No Matches
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),
24 ID_floatbv_typecast,
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{
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{
89public:
91 : unary_predicate_exprt(ID_isnan, std::move(op))
92 {
93 }
94};
95
96template <>
97inline bool can_cast_expr<isnan_exprt>(const exprt &base)
98{
99 return base.id() == ID_isnan;
100}
101
102inline void validate_expr(const isnan_exprt &value)
103{
104 validate_operands(value, 1, "Is NaN must have one operand");
105}
106
113inline 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{
133public:
135 : unary_predicate_exprt(ID_isinf, std::move(op))
136 {
137 }
138};
139
140template <>
141inline bool can_cast_expr<isinf_exprt>(const exprt &base)
142{
143 return base.id() == ID_isinf;
144}
145
146inline void validate_expr(const isinf_exprt &value)
147{
148 validate_operands(value, 1, "Is infinite must have one operand");
149}
150
157inline 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{
177public:
179 : unary_predicate_exprt(ID_isfinite, std::move(op))
180 {
181 }
182};
183
184template <>
185inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
186{
187 return base.id() == ID_isfinite;
188}
189
190inline void validate_expr(const isfinite_exprt &value)
191{
192 validate_operands(value, 1, "Is finite must have one operand");
193}
194
201inline 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{
221public:
223 : unary_predicate_exprt(ID_isnormal, std::move(op))
224 {
225 }
226};
227
228template <>
229inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
230{
231 return base.id() == ID_isnormal;
232}
233
234inline void validate_expr(const isnormal_exprt &value)
235{
236 validate_operands(value, 1, "Is normal must have one operand");
237}
238
245inline 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{
265public:
268 std::move(_lhs),
269 ID_ieee_float_equal,
270 std::move(_rhs))
271 {
272 }
273};
274
275template <>
277{
278 return base.id() == ID_ieee_float_equal;
279}
280
281inline 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{
313public:
316 std::move(_lhs),
317 ID_ieee_float_notequal,
318 std::move(_rhs))
319 {
320 }
321};
322
323template <>
325{
326 return base.id() == ID_ieee_float_notequal;
327}
328
330{
331 validate_operands(value, 2, "IEEE inequality must have two operands");
332}
333
340inline 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{
365public:
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
406template <>
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
413inline 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:583
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
A constant literal expression.
Definition std_expr.h:2942
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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.
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:396
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:49
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
exprt & op2()
Definition expr.h:131
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:326
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:528
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 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 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< ieee_float_op_exprt >(const exprt &base)
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.