10 #ifndef CPROVER_SOLVERS_FLOATBV_FLOAT_UTILS_H 11 #define CPROVER_SOLVERS_FLOATBV_FLOAT_UTILS_H 39 round_to_even=round_to_zero=round_to_plus_inf=round_to_minus_inf=
60 default: assert(
false);
93 return src[src.size()-1];
111 return add_sub(src1, src2,
false);
116 return add_sub(src1, src2,
true);
202 const std::size_t dest_bits,
204 const bvt &fraction);
220 #endif // CPROVER_SOLVERS_FLOATBV_FLOAT_UTILS_H bool is_signed(const typet &t)
Convenience function – is the type signed?
literalt is_minus_inf(const bvt &)
void round_exponent(unbiased_floatt &result)
Fixed-width bit-vector with IEEE floating-point interpretation.
literalt round_to_minus_inf
bvt sub_bias(const bvt &exponent)
virtual void normalization_shift(bvt &fraction, bvt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
bvt to_signed_integer(const bvt &src, std::size_t int_width)
void denormalization_shift(bvt &fraction, bvt &exponent)
make sure exponent is not too small; the exponent is unbiased
virtual bvt rem(const bvt &src1, const bvt &src2)
literalt is_normal(const bvt &)
literalt exponent_all_ones(const bvt &)
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
bvt add_bias(const bvt &exponent)
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt debug1(const bvt &op0, const bvt &op1)
bvt conversion(const bvt &src, const ieee_float_spect &dest_spec)
bvt get_exponent(const bvt &)
Gets the unbiased exponent in a floating-point bit-vector.
literalt is_zero(const bvt &)
static literalt sign_bit(const bvt &src)
literalt is_plus_inf(const bvt &)
unbiased_floatt unpack(const bvt &)
virtual bvt div(const bvt &src1, const bvt &src2)
literalt fraction_rounding_decision(const std::size_t dest_bits, const literalt sign, const bvt &fraction)
rounding decision for fraction using sticky bit
bvt get_fraction(const bvt &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
bvt debug2(const bvt &op0, const bvt &op1)
bvt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
literalt exponent_all_zeros(const bvt &)
void set_rounding_mode(const bvt &)
literalt is_infinity(const bvt &)
literalt const_literal(bool value)
literalt is_NaN(const bvt &)
literalt round_to_plus_inf
bvt from_unsigned_integer(const bvt &)
bvt add(const bvt &src1, const bvt &src2)
rounding_mode_bitst rounding_mode_bits
bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed)
biased_floatt bias(const unbiased_floatt &)
takes an unbiased float, and applies the bias
float_utilst(propt &_prop)
bvt limit_distance(const bvt &dist, mp_integer limit)
Limits the shift distance.
bvt from_signed_integer(const bvt &)
bvt sub(const bvt &src1, const bvt &src2)
bvt sticky_right_shift(const bvt &op, const bvt &dist, literalt &sticky)
std::vector< literalt > bvt
float_utilst(propt &_prop, const floatbv_typet &type)
virtual bvt rounder(const unbiased_floatt &)
bvt pack(const biased_floatt &)
void round_fraction(unbiased_floatt &result)
bvt build_constant(const ieee_floatt &)
literalt fraction_all_zeros(const bvt &)
literalt relation(const bvt &src1, relt rel, const bvt &src2)