28 if(src_type==dest_type)
31 if(src_type.
id() == ID_c_bit_field)
44 if(src_type.
id()==ID_floatbv &&
45 dest_type.
id()==ID_floatbv)
53 else if(src_type.
id()==ID_signedbv &&
54 dest_type.
id()==ID_floatbv)
59 else if(src_type.
id()==ID_unsignedbv &&
60 dest_type.
id()==ID_floatbv)
65 else if(src_type.
id()==ID_floatbv &&
66 dest_type.
id()==ID_signedbv)
72 else if(src_type.
id()==ID_floatbv &&
73 dest_type.
id()==ID_unsignedbv)
86 if(expr.
op().
type().
id() == ID_floatbv)
113 "both operands of a floating point operator must match the expression type",
120 if(expr.
type().
id() == ID_floatbv)
124 if(expr.
id()==ID_floatbv_plus)
125 return float_utils.
add_sub(lhs_as_bv, rhs_as_bv,
false);
126 else if(expr.
id()==ID_floatbv_minus)
127 return float_utils.
add_sub(lhs_as_bv, rhs_as_bv,
true);
128 else if(expr.
id()==ID_floatbv_mult)
129 return float_utils.
mul(lhs_as_bv, rhs_as_bv);
130 else if(expr.
id()==ID_floatbv_div)
131 return float_utils.
div(lhs_as_bv, rhs_as_bv);
135 else if(expr.
type().
id() == ID_complex)
139 if(subtype.
id()==ID_floatbv)
147 sub_width > 0 && width % sub_width == 0,
148 "width of a complex subtype must be positive and evenly divide the "
149 "width of the complex expression");
151 sub_width * 2 == width,
"a complex type consists of exactly two parts");
153 bvt lhs_real{lhs_as_bv.begin(), lhs_as_bv.begin() + sub_width};
154 bvt rhs_real{rhs_as_bv.begin(), rhs_as_bv.begin() + sub_width};
156 bvt lhs_imag{lhs_as_bv.begin() + sub_width, lhs_as_bv.end()};
157 bvt rhs_imag{rhs_as_bv.begin() + sub_width, rhs_as_bv.end()};
159 bvt result_real, result_imag;
161 if(expr.
id() == ID_floatbv_plus || expr.
id() == ID_floatbv_minus)
163 result_real = float_utils.
add_sub(
164 lhs_real, rhs_real, expr.
id() == ID_floatbv_minus);
165 result_imag = float_utils.
add_sub(
166 lhs_imag, rhs_imag, expr.
id() == ID_floatbv_minus);
168 else if(expr.
id() == ID_floatbv_mult)
173 result_real = float_utils.
add_sub(
174 float_utils.
mul(lhs_real, rhs_real),
175 float_utils.
mul(lhs_imag, rhs_imag),
177 result_imag = float_utils.
add_sub(
178 float_utils.
mul(lhs_real, rhs_imag),
179 float_utils.
mul(lhs_imag, rhs_real),
182 else if(expr.
id() == ID_floatbv_div)
185 float_utils.
mul(lhs_real, rhs_real),
186 float_utils.
mul(lhs_imag, rhs_imag),
189 float_utils.
mul(lhs_imag, rhs_real),
190 float_utils.
mul(lhs_real, rhs_imag),
194 float_utils.
mul(rhs_real, rhs_real),
195 float_utils.
mul(rhs_imag, rhs_imag),
198 result_real = float_utils.
div(numerator_real, denominator);
199 result_imag = float_utils.
div(numerator_imag, denominator);
204 bvt result_bv = std::move(result_real);
205 result_bv.reserve(width);
208 std::make_move_iterator(result_imag.begin()),
209 std::make_move_iterator(result_imag.end()));
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
std::size_t get_width() const
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual std::size_t boolbv_width(const typet &type) const
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
virtual bvt convert_floatbv_round_to_integral(const floatbv_round_to_integral_exprt &)
Base class for all expressions.
typet & type()
Return the type of the expression.
bvt round_to_integral(const bvt &)
void set_rounding_mode(const bvt &)
bvt from_unsigned_integer(const bvt &)
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
virtual bvt div(const bvt &src1, const bvt &src2)
bvt from_signed_integer(const bvt &)
bvt conversion(const bvt &src, const ieee_float_spect &dest_spec)
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
bvt to_signed_integer(const bvt &src, std::size_t int_width)
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)...
const irep_idt & id() const
const typet & subtype() const
Semantic type conversion.
The type of an expression, extends irept.
API to expression classes for floating-point arithmetic.
std::vector< literalt > bvt
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
const type_with_subtypet & to_type_with_subtype(const typet &type)