Go to the documentation of this file.
23 if(expr.
op().
type().
id() != ID_floatbv)
69 if(type.
id()==ID_floatbv)
72 value.set_sign(
false);
76 else if(type.
id()==ID_signedbv ||
77 type.
id()==ID_unsignedbv)
111 if(type.
id()==ID_floatbv)
117 else if(type.
id()==ID_signedbv ||
118 type.
id()==ID_unsignedbv)
142 if(dest_type==src_type)
145 const exprt &casted_expr = expr.
op();
152 if(casted_expr.
id()==ID_floatbv_div ||
153 casted_expr.
id()==ID_floatbv_mult ||
154 casted_expr.
id()==ID_floatbv_plus ||
155 casted_expr.
id()==ID_floatbv_minus)
157 if(casted_expr.
operands().size()==3 &&
158 casted_expr.
op0().
id()==ID_typecast &&
159 casted_expr.
op1().
id()==ID_typecast &&
162 casted_expr.
op0().
type()==dest_type &&
163 casted_expr.
op1().
type()==dest_type)
165 exprt result(casted_expr.
id(), floatbv_typecast_expr.type());
169 result.
op2()=rounding_mode;
181 const auto rounding_mode_index = numeric_cast<mp_integer>(rounding_mode);
182 if(rounding_mode_index.has_value())
184 if(src_type.
id()==ID_floatbv)
186 if(dest_type.
id()==ID_floatbv)
191 *rounding_mode_index);
196 else if(dest_type.
id()==ID_signedbv ||
197 dest_type.
id()==ID_unsignedbv)
204 *rounding_mode_index);
210 else if(src_type.
id()==ID_signedbv ||
211 src_type.
id()==ID_unsignedbv)
213 const auto value = numeric_cast<mp_integer>(casted_expr);
214 if(value.has_value())
216 if(dest_type.
id()==ID_floatbv)
221 *rounding_mode_index);
227 else if(src_type.
id() == ID_c_enum_tag)
231 exprt simplified_typecast =
236 new_floatbv_typecast_expr.
op() = simplified_typecast;
249 if(casted_expr.
id()==ID_if)
251 auto const &casted_if_expr =
to_if_expr(casted_expr);
258 auto simplified_if_expr =
simplify_expr(
if_exprt(casted_if_expr.cond(), casted_true_case, casted_false_case, dest_type),
ns);
259 expr = simplified_if_expr;
274 expr.
id() == ID_floatbv_plus || expr.
id() == ID_floatbv_minus ||
275 expr.
id() == ID_floatbv_mult || expr.
id() == ID_floatbv_div);
283 "expression type of operand must match type of expression");
286 "expression type of operand must match type of expression");
297 const auto rounding_mode = numeric_cast<mp_integer>(op2);
298 if(rounding_mode.has_value())
307 if(expr.
id()==ID_floatbv_plus)
309 else if(expr.
id()==ID_floatbv_minus)
311 else if(expr.
id()==ID_floatbv_mult)
313 else if(expr.
id()==ID_floatbv_div)
323 if(expr.
id()==ID_floatbv_div &&
336 expr.
id() == ID_ieee_float_equal || expr.
id() == ID_ieee_float_notequal);
352 if(expr.
id()==ID_ieee_float_notequal)
354 else if(expr.
id()==ID_ieee_float_equal)
360 if(expr.
lhs() == expr.
rhs())
365 if(expr.
id()==ID_ieee_float_notequal)
368 else if(expr.
id()==ID_ieee_float_equal)
373 return std::move(isnan);
#define UNREACHABLE
This should be used to mark dead code.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
resultt simplify_isnormal(const unary_exprt &)
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 change_spec(const ieee_float_spect &dest_spec)
Base class for all expressions.
Generic base class for unary expressions.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
mp_integer to_integer() const
static resultt unchanged(exprt expr)
resultt simplify_node(exprt)
typet & type()
Return the type of the expression.
Semantic type conversion from/to floating-point formats.
resultt simplify_isnan(const unary_exprt &)
#define PRECONDITION(CONDITION)
bool ieee_equal(const ieee_floatt &other) const
exprt simplify_expr(exprt src, const namespacet &ns)
const irep_idt & id() const
void from_integer(const mp_integer &i)
rounding_modet rounding_mode
Deprecated expression utility functions.
bool ieee_not_equal(const ieee_floatt &other) const
resultt simplify_sign(const sign_exprt &)
bool is_constant() const
Return whether the expression is a constant.
A base class for relations, i.e., binary predicates whose two operands have the same type.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
bool is_one() const
Return whether the expression is a constant representing 1.
constant_exprt to_expr() const
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Semantic type conversion.
resultt simplify_abs(const abs_exprt &)
API to expression classes.
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
Evaluates to true if the operand is NaN.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
resultt simplify_isinf(const unary_exprt &)