Go to the documentation of this file.
77 if(type.
id()==ID_floatbv)
80 value.set_sign(
false);
84 else if(type.
id()==ID_signedbv ||
85 type.
id()==ID_unsignedbv)
119 if(type.
id()==ID_floatbv)
125 else if(type.
id()==ID_signedbv ||
126 type.
id()==ID_unsignedbv)
147 const typet &dest_type =
ns.
follow(floatbv_typecast_expr.type());
148 const typet &src_type =
ns.
follow(floatbv_typecast_expr.op().type());
151 if(dest_type==src_type)
153 expr = floatbv_typecast_expr.op();
157 const exprt &casted_expr = floatbv_typecast_expr.op();
158 const exprt &rounding_mode = floatbv_typecast_expr.rounding_mode();
164 if(casted_expr.
id()==ID_floatbv_div ||
165 casted_expr.
id()==ID_floatbv_mult ||
166 casted_expr.
id()==ID_floatbv_plus ||
167 casted_expr.
id()==ID_floatbv_minus)
169 if(casted_expr.
operands().size()==3 &&
170 casted_expr.
op0().
id()==ID_typecast &&
171 casted_expr.
op1().
id()==ID_typecast &&
177 exprt result(casted_expr.
id(), floatbv_typecast_expr.type());
179 result.op0()=casted_expr.
op0().
op0();
181 result.
op2()=rounding_mode;
194 if(!
to_integer(rounding_mode, rounding_mode_index))
196 if(src_type.
id()==ID_floatbv)
198 if(dest_type.
id()==ID_floatbv)
203 rounding_mode_index);
209 else if(dest_type.
id()==ID_signedbv ||
210 dest_type.
id()==ID_unsignedbv)
217 rounding_mode_index);
224 else if(src_type.
id()==ID_signedbv ||
225 src_type.
id()==ID_unsignedbv)
230 if(dest_type.
id()==ID_floatbv)
235 rounding_mode_index);
242 else if(src_type.
id() == ID_c_enum_tag)
251 floatbv_typecast_expr;
252 new_floatbv_typecast_expr.
op() = simplified_typecast;
255 expr = new_floatbv_typecast_expr;
265 if(casted_expr.
id()==ID_if)
267 auto const &casted_if_expr =
to_if_expr(casted_expr);
274 auto simplified_if_expr =
simplify_expr(
if_exprt(casted_if_expr.cond(), casted_true_case, casted_false_case, dest_type),
ns);
275 expr = simplified_if_expr;
289 expr.
id() == ID_floatbv_plus || expr.
id() == ID_floatbv_minus ||
290 expr.
id() == ID_floatbv_mult || expr.
id() == ID_floatbv_div);
293 "binary operations have two operands, here an addtional parameter "
294 "is for the rounding mode");
302 "expression type of operand must match type of expression");
305 "expression type of operand must match type of expression");
325 if(expr.
id()==ID_floatbv_plus)
327 else if(expr.
id()==ID_floatbv_minus)
329 else if(expr.
id()==ID_floatbv_mult)
331 else if(expr.
id()==ID_floatbv_div)
342 if(expr.
id()==ID_floatbv_div &&
357 expr.
id() == ID_ieee_float_equal || expr.
id() == ID_ieee_float_notequal);
361 if(expr.
type().
id()!=ID_bool)
364 if(operands.size()!=2)
382 if(expr.
id()==ID_ieee_float_notequal)
384 else if(expr.
id()==ID_ieee_float_equal)
392 if(expr.
op0()==expr.
op1())
397 if(expr.
id()==ID_ieee_float_notequal)
400 else if(expr.
id()==ID_ieee_float_equal)
bool simplify_node(exprt &expr)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
#define PRECONDITION(CONDITION)
bool simplify_isnormal(exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
The type of an expression, extends irept.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
The trinary if-then-else operator.
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
void change_spec(const ieee_float_spect &dest_spec)
Base class for all expressions.
mp_integer to_integer() const
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool simplify_abs(exprt &expr)
#define UNREACHABLE
This should be used to mark dead code.
typet & type()
Return the type of the expression.
Semantic type conversion from/to floating-point formats.
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
bool ieee_equal(const ieee_floatt &other) const
bool simplify_sign(exprt &expr)
const irep_idt & id() const
std::vector< exprt > operandst
void from_integer(const mp_integer &i)
bool simplify_floatbv_op(exprt &expr)
rounding_modet rounding_mode
bool simplify_ieee_float_relation(exprt &expr)
bool simplify_isinf(exprt &expr)
bool ieee_not_equal(const ieee_floatt &other) const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
bool is_constant() const
Return whether the expression is a constant.
bool simplify_isnan(exprt &expr)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
bool is_one() const
Return whether the expression is a constant representing 1.
constant_exprt to_expr() const
Semantic type conversion.
bool simplify_floatbv_typecast(exprt &expr)
Evaluates to true if the operand is NaN.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.