9#ifndef CPROVER_UTIL_FLOATBV_EXPR_H
10#define CPROVER_UTIL_FLOATBV_EXPR_H
54 return base.
id() == ID_floatbv_typecast;
94 ID_floatbv_round_to_integral,
124 return base.
id() == ID_floatbv_round_to_integral;
163 return base.
id() == ID_isnan;
207 return base.
id() == ID_isinf;
251 return base.
id() == ID_isfinite;
295 return base.
id() == ID_isnormal;
342 return base.
id() == ID_ieee_float_equal;
381 ID_ieee_float_notequal,
390 return base.
id() == ID_ieee_float_notequal;
473 return base.
id() == ID_floatbv_plus || base.
id() == ID_floatbv_minus ||
474 base.
id() == ID_floatbv_div || base.
id() == ID_floatbv_mult;
480 value, 3,
"IEEE float operations must have three arguments");
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
A constant literal expression.
Base class for all expressions.
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 ...
typet & type()
Return the type of the expression.
floatbv_mod_exprt(exprt _lhs, exprt _rhs)
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 & 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
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
The type of an expression, extends irept.
unary_predicate_exprt(const irep_idt &_id, exprt _op)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
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.
#define PRECONDITION(CONDITION)
API to expression classes.