10 #ifndef CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H 11 #define CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H 16 #include "../flattening/bv_utils.h" 76 std::size_t dest_width,
81 std::size_t dest_width,
86 std::size_t dest_width,
126 void get(
const exprt &rm);
189 const std::size_t dest_bits,
191 const exprt &fraction,
213 #endif // CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
exprt isinf(const exprt &, const ieee_float_spect &)
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
bool is_signed(const typet &t)
Convenience function – is the type signed?
exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
ieee_float_spect get_spec(const exprt &)
exprt add_bias(const exprt &exponent, const ieee_float_spect &)
exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
exprt to_integer(const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)
exprt convert(const exprt &)
exprt pack(const biased_floatt &, const ieee_float_spect &)
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &)
exprt sign_bit(const exprt &)
exprt negation(const exprt &, const ieee_float_spect &)
void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
virtual exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &)
exprt isnormal(const exprt &, const ieee_float_spect &)
API to expression classes.
exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec)
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &)
exprt abs(const exprt &, const ieee_float_spect &)
The boolean constant false.
exprt float_bv(const exprt &src)
exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
exprt fraction_rounding_decision(const std::size_t dest_bits, const exprt sign, const exprt &fraction, const rounding_mode_bitst &)
rounding decision for fraction using sticky bit
exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
exprt is_zero(const exprt &, const ieee_float_spect &)
Base class for all expressions.
exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
exprt isfinite(const exprt &, const ieee_float_spect &)
exprt get_fraction(const exprt &, const ieee_float_spect &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
rounding_mode_bitst(const exprt &rm)
exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
void denormalization_shift(exprt &fraction, exprt &exponent, const ieee_float_spect &)
make sure exponent is not too small; the exponent is unbiased
exprt operator()(const exprt &src)
exprt isnan(const exprt &, const ieee_float_spect &)