20 bvt round_to_plus_inf=
22 bvt round_to_minus_inf=
70 std::size_t dest_width)
77 std::size_t dest_width)
84 std::size_t dest_width,
94 bvt fraction=unpacked.fraction;
96 if(dest_width>fraction.size())
99 fraction.insert(fraction.begin(),
100 lsb_extension.begin(),
101 lsb_extension.end());
106 unpacked.exponent.size());
112 bvt result=shift_result;
113 literalt exponent_sign=unpacked.exponent[unpacked.exponent.size()-1];
115 for(std::size_t i=0; i<result.size(); i++)
116 result[i]=
prop.
land(result[i], !exponent_sign);
119 if(result.size()>dest_width)
121 result.resize(dest_width);
124 assert(result.size()==dest_width);
138 throw "unsupported rounding mode";
171 int sourceSmallestNormalExponent=-((1 << (
spec.
e - 1)) - 1);
172 int sourceSmallestDenormalExponent =
173 sourceSmallestNormalExponent -
spec.
f;
177 int destSmallestNormalExponent=-((1 << (dest_spec.
e - 1)) - 1);
181 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
187 std::size_t padding=dest_spec.
f-
spec.
f;
204 result.
NaN=unpacked_src.
NaN;
234 bvt extended_exponent1=
236 bvt extended_exponent2=
239 assert(extended_exponent1.size()==extended_exponent2.size());
242 return bv_utils.
sub(extended_exponent1, extended_exponent2);
259 literalt src2_bigger=exponent_difference.back();
261 const bvt bigger_exponent=
265 const bvt new_fraction1=
268 const bvt new_fraction2=
278 const bvt fraction1_padded=
280 const bvt fraction2_padded=
285 const bvt fraction1_shifted=fraction1_padded;
287 fraction2_padded, limited_dist, sticky_bit);
290 bvt fraction2_stickied=fraction2_shifted;
291 fraction2_stickied[0]=
prop.
lor(fraction2_shifted[0], sticky_bit);
294 const bvt fraction1_ext=
296 const bvt fraction2_ext=
377 for(std::size_t i=0; i<result.
fraction.size(); i++)
378 result.
fraction[i]=new_fraction2[i];
394 upper_bits.erase(upper_bits.begin(), upper_bits.begin()+nb_bits);
398 lower_bits.resize(nb_bits);
401 result.resize(lower_bits.size());
404 for(std::size_t i=0; i<result.size(); i++)
405 result[i]=
prop.
lor(lower_bits[i], or_upper_bits);
449 NaN_cond.push_back(
is_NaN(src1));
450 NaN_cond.push_back(
is_NaN(src2));
468 std::size_t div_width=unpacked1.
fraction.size()*2+1;
472 fraction1.reserve(div_width);
473 while(fraction1.size()<div_width)
491 result.
fraction.begin(), have_remainder);
553 return sub(src1,
mul(
div(src1, src2), src2));
559 assert(!src.empty());
568 assert(!src.empty());
621 and_bv.push_back(less_than3);
622 and_bv.push_back(!bitwise_equal);
623 and_bv.push_back(!both_zero);
624 and_bv.push_back(!NaN);
631 or_bv.push_back(less_than3);
632 or_bv.push_back(both_zero);
633 or_bv.push_back(bitwise_equal);
645 prop.
lor(bitwise_equal, both_zero),
657 assert(!src.empty());
660 all_but_sign.resize(all_but_sign.size()-1);
712 exponent.erase(exponent.begin(), exponent.begin()+
spec.
f);
715 exponent.resize(
spec.
e);
725 exponent.erase(exponent.begin(), exponent.begin()+
spec.
f);
728 exponent.resize(
spec.
e);
752 for(std::size_t i=0; i<fraction.size(); i++)
757 for(std::size_t j=0; j<i; j++)
759 !fraction[fraction.size()-1-j]);
762 equal.push_back(fraction[fraction.size()-1-i]);
784 fraction=new_fraction;
785 exponent=new_exponent;
792 assert(!fraction.empty());
795 if(exponent.size()<depth)
800 for(
int d=depth-1; d>=0; d--)
802 std::size_t distance=(1<<d);
803 assert(fraction.size()>distance);
818 assert(d<(
signed)exponent_delta.size());
819 exponent_delta[d]=prefix_is_zero;
839 assert(exponent.size()>=
spec.
e);
861 if(fraction.size() < (
spec.
f + 3))
869 bvt denormalisedFraction=fraction;
872 denormalisedFraction =
874 denormalisedFraction[0]=
prop.
lor(denormalisedFraction[0], sticky_bit);
879 denormalisedFraction,
909 if(aligned_exponent.size()<exponent_bits)
936 const std::size_t dest_bits,
940 assert(dest_bits<fraction.size());
943 std::size_t extra_bits=fraction.size()-dest_bits;
959 assert(extra_bits>=1);
960 literalt rounding_bit=fraction[extra_bits-1];
963 literalt rounding_least=fraction[extra_bits];
968 prop.
lor(rounding_least, sticky_bit));
973 prop.
lor(rounding_bit, sticky_bit));
978 prop.
lor(rounding_bit, sticky_bit));
994 std::size_t fraction_size=
spec.
f+1;
997 if(result.
fraction.size()<fraction_size)
1000 std::size_t padding=fraction_size-result.
fraction.size();
1006 assert(result.
fraction.size()==fraction_size);
1008 else if(result.
fraction.size()==fraction_size)
1014 std::size_t extra_bits=result.
fraction.size()-fraction_size;
1015 assert(extra_bits>=1);
1025 assert(result.
fraction.size()==fraction_size);
1048 result.
fraction.back()=new_integer_part;
1074 prop.
lor(overflow, subnormal_to_normal));
1125 prop.
land(exponent_too_large, !overflow_to_inf);
1128 bvt largest_normal_exponent=
1172 for(std::size_t i=0; i<result.
exponent.size(); i++)
1181 assert(src.size()==
spec.
e);
1190 assert(src.size()==
spec.
e);
1206 result.fraction.push_back(
is_normal(src));
1209 assert(result.exponent.size()==
spec.
e);
1236 result[result.size()-1]=
1243 for(std::size_t i=0; i<
spec.
f; i++)
1249 for(std::size_t i=0; i<
spec.
e; i++)
1261 for(std::size_t i=0; i<src.size(); i++)
1266 result.
unpack(int_value);
1280 for(std::size_t stage=0; stage<dist.size(); stage++)
1288 if(d<=result.size())
bool is_signed(const typet &t)
Convenience function – is the type signed?
ieee_floatt get(const bvt &) const
bvt inverted(const bvt &op)
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
literalt is_minus_inf(const bvt &)
void round_exponent(unbiased_floatt &result)
literalt round_to_minus_inf
bvt cond_negate(const bvt &bv, const literalt cond)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
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)
virtual literalt lor(literalt a, literalt b)=0
bvt sub(const bvt &op0, const bvt &op1)
mp_integer max_exponent() const
literalt is_zero(const bvt &op)
const mp_integer & get_exponent() const
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 &)
virtual literalt land(literalt a, literalt b)=0
literalt is_all_ones(const bvt &op)
virtual literalt new_variable()=0
void unpack(const mp_integer &i)
bvt concatenate(const bvt &a, const bvt &b) const
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
bvt add_bias(const bvt &exponent)
virtual literalt lxor(literalt a, literalt b)=0
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)
literalt is_not_zero(const bvt &op)
static bvt extract_msb(const bvt &a, std::size_t n)
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)
bvt absolute_value(const bvt &op)
literalt is_plus_inf(const bvt &)
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
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.
bvt zero_extension(const bvt &bv, std::size_t new_size)
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
bvt debug2(const bvt &op0, const bvt &op1)
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
bvt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
bvt incrementer(const bvt &op, literalt carry_in)
literalt exponent_all_zeros(const bvt &)
void set_rounding_mode(const bvt &)
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
literalt is_infinity(const bvt &)
literalt const_literal(bool value)
literalt is_NaN(const bvt &)
bvt add(const bvt &op0, const bvt &op1)
literalt round_to_plus_inf
bvt from_unsigned_integer(const bvt &)
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
virtual tvt l_get(literalt a) const =0
bvt limit_distance(const bvt &dist, mp_integer limit)
Limits the shift distance.
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
bvt from_signed_integer(const bvt &)
bvt sign_extension(const bvt &bv, std::size_t new_size)
std::size_t width() const
bvt sub(const bvt &src1, const bvt &src2)
virtual literalt lselect(literalt a, literalt b, literalt c)=0
bvt sticky_right_shift(const bvt &op, const bvt &dist, literalt &sticky)
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
std::vector< literalt > bvt
bvt build_constant(const mp_integer &i, std::size_t width)
bvt zeros(std::size_t new_size) const
const mp_integer & get_fraction() const
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)