74 if(type.
id()==ID_floatbv)
77 value.set_sign(
false);
81 else if(type.
id()==ID_signedbv ||
82 type.
id()==ID_unsignedbv)
114 const typet &type = expr.
op0().
type();
116 if(type.
id()==ID_floatbv)
122 else if(type.
id()==ID_signedbv ||
123 type.
id()==ID_unsignedbv)
141 auto &op = expr.
op();
145 if(op.is_constant() && rounding_mode.is_constant())
147 const auto rounding_mode_index =
169 if(dest_type==src_type)
172 const exprt &casted_expr = expr.
op();
179 if(casted_expr.
id()==ID_floatbv_div ||
180 casted_expr.
id()==ID_floatbv_mult ||
181 casted_expr.
id()==ID_floatbv_plus ||
182 casted_expr.
id()==ID_floatbv_minus)
184 if(casted_expr.
operands().size()==3 &&
185 casted_expr.
op0().
id()==ID_typecast &&
186 casted_expr.
op1().
id()==ID_typecast &&
189 casted_expr.
op0().
type()==dest_type &&
190 casted_expr.
op1().
type()==dest_type)
192 exprt result(casted_expr.
id(), floatbv_typecast_expr.type());
196 result.
op2()=rounding_mode;
209 if(rounding_mode_index.has_value())
211 if(src_type.
id()==ID_floatbv)
213 if(dest_type.
id()==ID_floatbv)
217 *rounding_mode_index);
223 else if(dest_type.
id()==ID_signedbv ||
224 dest_type.
id()==ID_unsignedbv)
230 *rounding_mode_index);
237 else if(src_type.
id()==ID_signedbv ||
238 src_type.
id()==ID_unsignedbv)
241 if(value.has_value())
243 if(dest_type.
id()==ID_floatbv)
247 *rounding_mode_index);
254 else if(src_type.
id() == ID_c_enum_tag)
263 new_floatbv_typecast_expr.
op() = simplified_typecast;
276 if(casted_expr.
id()==ID_if)
278 auto const &casted_if_expr =
to_if_expr(casted_expr);
285 auto simplified_if_expr =
simplify_expr(
if_exprt(casted_if_expr.cond(), casted_true_case, casted_false_case, dest_type),
ns);
286 expr = simplified_if_expr;
301 expr.
id() == ID_floatbv_plus || expr.
id() == ID_floatbv_minus ||
302 expr.
id() == ID_floatbv_mult || expr.
id() == ID_floatbv_div);
310 "expression type of operand must match type of expression");
313 "expression type of operand must match type of expression");
323 if(rounding_mode_opt.has_value())
325 const auto rounding_mode =
334 if(expr.
id()==ID_floatbv_plus)
336 else if(expr.
id()==ID_floatbv_minus)
338 else if(expr.
id()==ID_floatbv_mult)
340 else if(expr.
id()==ID_floatbv_div)
350 if(expr.
id()==ID_floatbv_div &&
363 expr.
id() == ID_ieee_float_equal || expr.
id() == ID_ieee_float_notequal);
379 if(expr.
id()==ID_ieee_float_notequal)
381 else if(expr.
id()==ID_ieee_float_equal)
389 if(lhs_sorted.
id() == ID_floatbv_plus || lhs_sorted.
id() == ID_floatbv_mult)
392 if(rhs_sorted.
id() == ID_floatbv_plus || rhs_sorted.
id() == ID_floatbv_mult)
395 if(lhs_sorted == rhs_sorted)
400 if(expr.
id()==ID_ieee_float_notequal)
403 else if(expr.
id()==ID_ieee_float_equal)
408 return std::move(isnan);
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
bool is_one() const
Return whether the expression is a constant representing 1.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
Round a floating-point number to an integral value considering the given rounding mode.
Semantic type conversion from/to floating-point formats.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
An IEEE 754 floating-point value, including specificiation.
bool ieee_equal(const ieee_float_valuet &) const
bool ieee_not_equal(const ieee_float_valuet &) const
constant_exprt to_expr() const
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
mp_integer to_integer() const
void from_integer(const mp_integer &i)
void change_spec(const ieee_float_spect &dest_spec)
ieee_floatt round_to_integral() const
The trinary if-then-else operator.
const irep_idt & id() const
Evaluates to true if the operand is NaN.
resultt simplify_isnan(const unary_exprt &)
resultt simplify_abs(const abs_exprt &)
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_node(const exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_isinf(const unary_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_sign(const sign_exprt &)
resultt simplify_floatbv_round_to_integral(const floatbv_round_to_integral_exprt &)
Semantic type conversion.
The type of an expression, extends irept.
Generic base class for unary expressions.
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
exprt simplify_expr(exprt src, const namespacet &ns)
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.