19 bvt round_to_plus_inf=
21 bvt round_to_minus_inf=
69 std::size_t dest_width)
76 std::size_t dest_width)
83 std::size_t dest_width,
95 if(dest_width > fraction.size())
98 bv_utils.build_constant(0U, dest_width - fraction.size());
100 fraction.begin(), lsb_extension.begin(), lsb_extension.end());
111 bvt result = shift_result;
114 for(std::size_t i = 0; i < result.size(); i++)
115 result[i] =
prop.land(result[i], !exponent_sign);
118 if(result.size() > dest_width)
120 result.resize(dest_width);
124 result.size() == dest_width,
125 "result bitvector width should equal the destination bitvector width");
169 int sourceSmallestNormalExponent=-((1 << (
spec.e - 1)) - 1);
170 int sourceSmallestDenormalExponent =
171 sourceSmallestNormalExponent -
spec.f;
175 int destSmallestNormalExponent=-((1 << (dest_spec.
e - 1)) - 1);
177 if(dest_spec.
e>=
spec.e &&
178 dest_spec.
f>=
spec.f &&
179 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
185 std::size_t padding=dest_spec.
f-
spec.f;
195 if(dest_spec.
e >
spec.e)
206 result.
NaN=unpacked_src.
NaN;
236 bvt extended_exponent1=
238 bvt extended_exponent2=
241 PRECONDITION(extended_exponent1.size() == extended_exponent2.size());
244 return bv_utils.sub(extended_exponent1, extended_exponent2);
261 literalt src2_bigger=exponent_difference.back();
263 const bvt bigger_exponent=
267 const bvt new_fraction1=
270 const bvt new_fraction2=
274 const bvt distance=
bv_utils.absolute_value(exponent_difference);
280 const bvt fraction1_padded=
282 const bvt fraction2_padded=
287 const bvt fraction1_shifted=fraction1_padded;
289 fraction2_padded, limited_dist, sticky_bit);
292 bvt fraction2_stickied=fraction2_shifted;
293 fraction2_stickied[0]=
prop.lor(fraction2_shifted[0], sticky_bit);
296 const bvt fraction1_ext=
297 bv_utils.zero_extension(fraction1_shifted, fraction1_shifted.size()+2);
298 const bvt fraction2_ext=
299 bv_utils.zero_extension(fraction2_stickied, fraction2_stickied.size()+2);
306 bv_utils.add_sub(fraction1_ext, fraction2_ext, subtract_lit);
379 for(std::size_t i=0; i<result.
fraction.size(); i++)
380 result.
fraction[i]=new_fraction2[i];
396 upper_bits.erase(upper_bits.begin(), upper_bits.begin()+nb_bits);
400 lower_bits.resize(nb_bits);
403 result.resize(lower_bits.size());
406 for(std::size_t i=0; i<result.size(); i++)
407 result[i]=
prop.lor(lower_bits[i], or_upper_bits);
435 bvt added_exponent=
bv_utils.add(exponent1, exponent2);
451 NaN_cond.push_back(
is_NaN(src1));
452 NaN_cond.push_back(
is_NaN(src2));
470 std::size_t div_width=unpacked1.
fraction.size()*2+1;
474 fraction1.reserve(div_width);
475 while(fraction1.size()<div_width)
493 result.
fraction.begin(), have_remainder);
504 bvt added_exponent=
bv_utils.sub(exponent1, exponent2);
509 bv_utils.build_constant(
spec.f, added_exponent.size()));
619 prop.lselect(signs_different,
626 and_bv.push_back(less_than3);
627 and_bv.push_back(!bitwise_equal);
628 and_bv.push_back(!both_zero);
629 and_bv.push_back(!NaN);
631 return prop.land(and_bv);
636 or_bv.push_back(less_than3);
637 or_bv.push_back(both_zero);
638 or_bv.push_back(bitwise_equal);
640 return prop.land(
prop.lor(or_bv), !NaN);
650 prop.lor(bitwise_equal, both_zero),
664 all_but_sign.resize(all_but_sign.size()-1);
665 return bv_utils.is_zero(all_but_sign);
674 return prop.land(and_bv);
702 return prop.land(and_bv);
716 exponent.erase(exponent.begin(), exponent.begin()+
spec.f);
719 exponent.resize(
spec.e);
721 return bv_utils.is_all_ones(exponent);
729 exponent.erase(exponent.begin(), exponent.begin()+
spec.f);
732 exponent.resize(
spec.e);
752 bvt new_fraction=
prop.new_variables(fraction.size());
753 bvt new_exponent=
prop.new_variables(exponent.size());
756 for(std::size_t i=0; i<fraction.size(); i++)
761 for(std::size_t j=0; j<i; j++)
763 !fraction[fraction.size()-1-j]);
766 equal.push_back(fraction[fraction.size()-1-i]);
772 bvt shifted_fraction=
bv_utils.shift(fraction, bv_utilst::LEFT, i);
773 bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
776 bvt adjustment=
bv_utils.build_constant(-i, exponent.size());
777 bvt added_exponent=
bv_utils.add(exponent, adjustment);
778 bv_utils.cond_implies_equal(shift, added_exponent, new_exponent);
786 bv_utils.cond_implies_equal(fraction_all_zero, zero_fraction, new_fraction);
788 fraction=new_fraction;
789 exponent=new_exponent;
801 bv_utils.sign_extension(exponent, std::max(depth, exponent.size() + 1));
803 bvt exponent_delta=
bv_utils.zeros(exponent.size());
805 for(
int d=depth-1; d>=0; d--)
807 std::size_t distance=(1<<d);
809 fraction.size() > distance,
"fraction must be larger than distance");
812 const bvt prefix=
bv_utils.extract_msb(fraction, distance);
821 bv_utils.select(prefix_is_zero, shifted, fraction);
825 d < (
signed)exponent_delta.size(),
826 "depth must be smaller than exponent size");
827 exponent_delta[d]=prefix_is_zero;
830 exponent=
bv_utils.sub(exponent, exponent_delta);
855 exponent=
bv_utils.sign_extension(exponent, exponent.size() + 1);
859 bv_utils.build_constant(-
bias+1, exponent.size()), exponent);
869 if(fraction.size() < (
spec.f + 3))
877 bvt denormalisedFraction=fraction;
880 denormalisedFraction =
882 denormalisedFraction[0]=
prop.lor(denormalisedFraction[0], sticky_bit);
887 denormalisedFraction,
894 bv_utils.shift(fraction, bv_utilst::LRIGHT, distance),
917 if(aligned_exponent.size()<exponent_bits)
921 bv_utils.sign_extension(aligned_exponent, exponent_bits);
944 const std::size_t dest_bits,
951 std::size_t extra_bits=fraction.size()-dest_bits;
962 bvt tail=
bv_utils.extract(fraction, 0, extra_bits-2);
963 sticky_bit=
prop.lor(tail);
968 extra_bits >= 1,
"the extra bits include at least the rounding bit");
969 literalt rounding_bit=fraction[extra_bits-1];
972 literalt rounding_least=fraction[extra_bits];
976 prop.land(rounding_bit,
977 prop.lor(rounding_least, sticky_bit));
982 prop.lor(rounding_bit, sticky_bit));
987 prop.lor(rounding_bit, sticky_bit));
998 prop.new_variable()))));
1003 std::size_t fraction_size=
spec.f+1;
1006 if(result.
fraction.size()<fraction_size)
1009 std::size_t padding=fraction_size-result.
fraction.size();
1016 result.
fraction.size() == fraction_size,
1017 "sizes should be equal as result.fraction was zero-padded");
1019 else if(result.
fraction.size()==fraction_size)
1025 std::size_t extra_bits=result.
fraction.size()-fraction_size;
1028 "the extra bits should at least include the rounding bit");
1039 result.
fraction.size() == fraction_size,
1040 "sizes should be equal as extra bits were chopped off from "
1061 literalt new_integer_part=
prop.lor(integer_part1, integer_part0);
1064 result.
fraction.back()=new_integer_part;
1090 prop.lor(overflow, subnormal_to_normal));
1118 spec.max_exponent()-
spec.bias(), old_exponent.size());
1124 !
bv_utils.signed_less_than(old_exponent, max_exponent),
1138 prop.land(exponent_too_large, !overflow_to_inf);
1141 bvt largest_normal_exponent=
1154 prop.land(exponent_too_large,
1186 for(std::size_t i=0; i<result.
exponent.size(); i++)
1246 result.resize(
spec.width());
1250 result[result.size()-1]=
1257 for(std::size_t i=0; i<
spec.f; i++)
1258 result[i]=
prop.land(src.
fraction[i], !infinity_or_NaN);
1260 result[0]=
prop.lor(result[0], src.
NaN);
1263 for(std::size_t i=0; i<
spec.e; i++)
1275 for(std::size_t i=0; i<src.size(); i++)
1276 int_value+=
power(2, i)*
prop.l_get(src[i]).is_true();
1280 result.
unpack(int_value);
1294 for(std::size_t stage=0; stage<dist.size(); stage++)
1302 if(d<=result.size())
1303 lost_bits=
bv_utils.extract(result, 0, d-1);
1308 prop.land(dist[stage],
prop.lor(lost_bits)),
1311 result=
bv_utils.select(dist[stage], tmp, result);
bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed)
literalt is_NaN(const bvt &)
virtual void normalization_shift(bvt &fraction, bvt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
bvt build_constant(const ieee_floatt &)
bvt debug2(const bvt &op0, const bvt &op1)
virtual bvt rem(const bvt &src1, const bvt &src2)
literalt is_plus_inf(const bvt &)
literalt is_infinity(const bvt &)
void set_rounding_mode(const bvt &)
void round_exponent(unbiased_floatt &result)
void round_fraction(unbiased_floatt &result)
bvt sticky_right_shift(const bvt &op, const bvt &dist, literalt &sticky)
virtual bvt rounder(const unbiased_floatt &)
unbiased_floatt unpack(const bvt &)
bvt from_unsigned_integer(const bvt &)
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt debug1(const bvt &op0, const bvt &op1)
bvt add_bias(const bvt &exponent)
bvt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
bvt get_fraction(const bvt &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
literalt is_minus_inf(const bvt &)
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_exponent(const bvt &)
Gets the unbiased exponent in a floating-point bit-vector.
void denormalization_shift(bvt &fraction, bvt &exponent)
make sure exponent is not too small; the exponent is unbiased
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
virtual bvt div(const bvt &src1, const bvt &src2)
ieee_floatt get(const bvt &) const
literalt exponent_all_zeros(const bvt &)
literalt fraction_all_zeros(const bvt &)
bvt from_signed_integer(const bvt &)
literalt is_zero(const bvt &)
bvt sub(const bvt &src1, const bvt &src2)
bvt sub_bias(const bvt &exponent)
bvt limit_distance(const bvt &dist, mp_integer limit)
Limits the shift distance.
bvt conversion(const bvt &src, const ieee_float_spect &dest_spec)
bvt pack(const biased_floatt &)
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
static literalt sign_bit(const bvt &src)
literalt exponent_all_ones(const bvt &)
bvt to_signed_integer(const bvt &src, std::size_t int_width)
literalt is_normal(const bvt &)
literalt relation(const bvt &src1, relt rel, const bvt &src2)
rounding_mode_bitst rounding_mode_bits
biased_floatt bias(const unbiased_floatt &)
takes an unbiased float, and applies the bias
const mp_integer & get_exponent() const
const mp_integer & get_fraction() const
void unpack(const mp_integer &i)
std::vector< literalt > bvt
literalt const_literal(bool value)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool is_signed(const typet &t)
Convenience function – is the type signed?