9#ifndef CPROVER_UTIL_FLOATBV_EXPR_H
10#define CPROVER_UTIL_FLOATBV_EXPR_H
480 value, 3,
"IEEE float operations must have three arguments");
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
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.
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)
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.