9 #ifndef CPROVER_UTIL_FLOATBV_EXPR_H
10 #define CPROVER_UTIL_FLOATBV_EXPR_H
54 return base.
id() == ID_floatbv_typecast;
99 return base.
id() == ID_isnan;
143 return base.
id() == ID_isinf;
187 return base.
id() == ID_isfinite;
231 return base.
id() == ID_isnormal;
278 return base.
id() == ID_ieee_float_equal;
317 ID_ieee_float_notequal,
326 return base.
id() == ID_ieee_float_notequal;
409 return base.
id() == ID_floatbv_plus || base.
id() == ID_floatbv_minus ||
410 base.
id() == ID_floatbv_div || base.
id() == ID_floatbv_mult;
416 value, 3,
"IEEE float operations must have three arguments");
A base class for binary expressions.
A base class for relations, i.e., binary predicates whose two operands have the same type.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
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 & rhs() const
const exprt & rounding_mode() 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.
An expression with three operands.
The type of an expression, extends irept.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
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)
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
bool can_cast_expr< isinf_exprt >(const exprt &base)
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.
bool can_cast_expr< isfinite_exprt >(const exprt &base)
bool can_cast_expr< isnormal_exprt >(const exprt &base)
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_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< ieee_float_op_exprt >(const exprt &base)
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
void validate_expr(const floatbv_typecast_exprt &value)
bool can_cast_expr< ieee_float_notequal_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.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
#define PRECONDITION(CONDITION)
API to expression classes.