19 bvt round_to_plus_inf=
21 bvt round_to_minus_inf=
72 std::size_t dest_width)
79 std::size_t dest_width)
86 std::size_t dest_width,
98 if(dest_width > fraction.size())
101 bv_utils.build_constant(0U, dest_width - fraction.size());
103 fraction.begin(), lsb_extension.begin(), lsb_extension.end());
114 bvt result = shift_result;
117 for(std::size_t i = 0; i < result.size(); i++)
118 result[i] =
prop.land(result[i], !exponent_sign);
121 if(result.size() > dest_width)
123 result.resize(dest_width);
127 result.size() == dest_width,
128 "result bitvector width should equal the destination bitvector width");
160 auto unpacked =
unpack(src);
161 auto is_special =
prop.lor({unpacked.zero, unpacked.NaN, unpacked.infinity});
173 magic_number_bv.back() = src.back();
175 auto tmp1 =
add_sub(src, magic_number_bv,
false);
177 auto tmp2 =
add_sub(tmp1, magic_number_bv,
true);
180 tmp2.back() = src.back();
182 return bv_utils.select(
prop.lor(is_special, ge_magic_number), src, tmp2);
202 int sourceSmallestNormalExponent=-((1 << (
spec.e - 1)) - 1);
203 int sourceSmallestDenormalExponent =
204 sourceSmallestNormalExponent -
spec.f;
208 int destSmallestNormalExponent=-((1 << (dest_spec.
e - 1)) - 1);
210 if(dest_spec.
e>=
spec.e &&
211 dest_spec.
f>=
spec.f &&
212 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
218 std::size_t padding=dest_spec.
f-
spec.f;
228 if(dest_spec.
e >
spec.e)
239 result.
NaN=unpacked_src.
NaN;
269 bvt extended_exponent1=
271 bvt extended_exponent2=
274 PRECONDITION(extended_exponent1.size() == extended_exponent2.size());
277 return bv_utils.sub(extended_exponent1, extended_exponent2);
294 literalt src2_bigger=exponent_difference.back();
296 const bvt bigger_exponent=
300 const bvt new_fraction1=
303 const bvt new_fraction2=
307 const bvt distance=
bv_utils.absolute_value(exponent_difference);
313 const bvt fraction1_padded=
315 const bvt fraction2_padded=
320 const bvt fraction1_shifted=fraction1_padded;
322 fraction2_padded, limited_dist, sticky_bit);
325 bvt fraction2_stickied=fraction2_shifted;
326 fraction2_stickied[0]=
prop.lor(fraction2_shifted[0], sticky_bit);
329 const bvt fraction1_ext=
330 bv_utils.zero_extension(fraction1_shifted, fraction1_shifted.size()+2);
331 const bvt fraction2_ext=
332 bv_utils.zero_extension(fraction2_stickied, fraction2_stickied.size()+2);
339 bv_utils.add_sub(fraction1_ext, fraction2_ext, subtract_lit);
412 for(std::size_t i=0; i<result.
fraction.size(); i++)
413 result.
fraction[i]=new_fraction2[i];
429 upper_bits.erase(upper_bits.begin(), upper_bits.begin()+nb_bits);
433 lower_bits.resize(nb_bits);
436 result.resize(lower_bits.size());
439 for(std::size_t i=0; i<result.size(); i++)
440 result[i]=
prop.lor(lower_bits[i], or_upper_bits);
468 bvt added_exponent=
bv_utils.add(exponent1, exponent2);
484 NaN_cond.push_back(
is_NaN(src1));
485 NaN_cond.push_back(
is_NaN(src2));
503 std::size_t div_width=unpacked1.
fraction.size()*2+1;
507 fraction1.reserve(div_width);
508 while(fraction1.size()<div_width)
526 result.
fraction.begin(), have_remainder);
537 bvt added_exponent=
bv_utils.sub(exponent1, exponent2);
542 bv_utils.build_constant(
spec.f, added_exponent.size()));
652 prop.lselect(signs_different,
659 and_bv.push_back(less_than3);
660 and_bv.push_back(!bitwise_equal);
661 and_bv.push_back(!both_zero);
662 and_bv.push_back(!NaN);
664 return prop.land(and_bv);
669 or_bv.push_back(less_than3);
670 or_bv.push_back(both_zero);
671 or_bv.push_back(bitwise_equal);
673 return prop.land(
prop.lor(or_bv), !NaN);
683 prop.lor(bitwise_equal, both_zero),
697 all_but_sign.resize(all_but_sign.size()-1);
698 return bv_utils.is_zero(all_but_sign);
707 return prop.land(and_bv);
735 return prop.land(and_bv);
749 exponent.erase(exponent.begin(), exponent.begin()+
spec.f);
752 exponent.resize(
spec.e);
754 return bv_utils.is_all_ones(exponent);
762 exponent.erase(exponent.begin(), exponent.begin()+
spec.f);
765 exponent.resize(
spec.e);
785 bvt new_fraction=
prop.new_variables(fraction.size());
786 bvt new_exponent=
prop.new_variables(exponent.size());
789 for(std::size_t i=0; i<fraction.size(); i++)
794 for(std::size_t j=0; j<i; j++)
796 !fraction[fraction.size()-1-j]);
799 equal.push_back(fraction[fraction.size()-1-i]);
805 bvt shifted_fraction=
bv_utils.shift(fraction, bv_utilst::LEFT, i);
806 bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
809 bvt adjustment=
bv_utils.build_constant(-i, exponent.size());
810 bvt added_exponent=
bv_utils.add(exponent, adjustment);
811 bv_utils.cond_implies_equal(shift, added_exponent, new_exponent);
819 bv_utils.cond_implies_equal(fraction_all_zero, zero_fraction, new_fraction);
821 fraction=new_fraction;
822 exponent=new_exponent;
834 bv_utils.sign_extension(exponent, std::max(depth, exponent.size() + 1));
836 bvt exponent_delta=
bv_utils.zeros(exponent.size());
838 for(
int d=depth-1; d>=0; d--)
840 std::size_t distance=(1<<d);
842 fraction.size() > distance,
"fraction must be larger than distance");
845 const bvt prefix=
bv_utils.extract_msb(fraction, distance);
854 bv_utils.select(prefix_is_zero, shifted, fraction);
858 d < (
signed)exponent_delta.size(),
859 "depth must be smaller than exponent size");
860 exponent_delta[d]=prefix_is_zero;
863 exponent=
bv_utils.sub(exponent, exponent_delta);
888 exponent=
bv_utils.sign_extension(exponent, exponent.size() + 1);
892 bv_utils.build_constant(-
bias+1, exponent.size()), exponent);
902 if(fraction.size() < (
spec.f + 3))
910 bvt denormalisedFraction=fraction;
913 denormalisedFraction =
915 denormalisedFraction[0]=
prop.lor(denormalisedFraction[0], sticky_bit);
920 denormalisedFraction,
927 bv_utils.shift(fraction, bv_utilst::LRIGHT, distance),
950 if(aligned_exponent.size()<exponent_bits)
954 bv_utils.sign_extension(aligned_exponent, exponent_bits);
982 const std::size_t dest_bits,
989 std::size_t extra_bits=fraction.size()-dest_bits;
1000 bvt tail=
bv_utils.extract(fraction, 0, extra_bits-2);
1001 sticky_bit=
prop.lor(tail);
1006 extra_bits >= 1,
"the extra bits include at least the rounding bit");
1007 literalt rounding_bit=fraction[extra_bits-1];
1010 literalt rounding_least=fraction[extra_bits];
1014 prop.land(rounding_bit,
1015 prop.lor(rounding_least, sticky_bit));
1020 prop.lor(rounding_bit, sticky_bit));
1025 prop.lor(rounding_bit, sticky_bit));
1032 literalt round_to_away = rounding_bit;
1041 prop.new_variable())))));
1047 std::size_t fraction_size=
spec.f+1;
1050 if(result.
fraction.size()<fraction_size)
1053 std::size_t padding=fraction_size-result.
fraction.size();
1060 result.
fraction.size() == fraction_size,
1061 "sizes should be equal as result.fraction was zero-padded");
1063 else if(result.
fraction.size()==fraction_size)
1069 std::size_t extra_bits=result.
fraction.size()-fraction_size;
1072 "the extra bits should at least include the rounding bit");
1083 result.
fraction.size() == fraction_size,
1084 "sizes should be equal as extra bits were chopped off from "
1105 literalt new_integer_part=
prop.lor(integer_part1, integer_part0);
1108 result.
fraction.back()=new_integer_part;
1134 prop.lor(overflow, subnormal_to_normal));
1162 spec.max_exponent()-
spec.bias(), old_exponent.size());
1168 !
bv_utils.signed_less_than(old_exponent, max_exponent),
1182 prop.land(exponent_too_large, !overflow_to_inf);
1185 bvt largest_normal_exponent=
1198 prop.land(exponent_too_large,
1230 for(std::size_t i=0; i<result.
exponent.size(); i++)
1290 result.resize(
spec.width());
1294 result[result.size()-1]=
1301 for(std::size_t i=0; i<
spec.f; i++)
1302 result[i]=
prop.land(src.
fraction[i], !infinity_or_NaN);
1304 result[0]=
prop.lor(result[0], src.
NaN);
1307 for(std::size_t i=0; i<
spec.e; i++)
1319 for(std::size_t i=0; i<src.size(); i++)
1320 int_value+=
power(2, i)*
prop.l_get(src[i]).is_true();
1324 result.
unpack(int_value);
1338 for(std::size_t stage=0; stage<dist.size(); stage++)
1346 if(d<=result.size())
1347 lost_bits=
bv_utils.extract(result, 0, d-1);
1352 prop.land(dist[stage],
prop.lor(lost_bits)),
1355 result=
bv_utils.select(dist[stage], tmp, result);
unbiased_floatt rounder(const unbiased_floatt &)
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 debug2(const bvt &op0, const bvt &op1)
virtual bvt rem(const bvt &src1, const bvt &src2)
bvt round_to_integral(const bvt &)
literalt is_plus_inf(const bvt &)
ieee_float_valuet get(const bvt &) const
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)
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 round_and_pack(const unbiased_floatt &)
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)
bvt build_constant(const ieee_float_valuet &)
virtual bvt div(const bvt &src1, const bvt &src2)
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
An IEEE 754 floating-point value, including specificiation.
const mp_integer & get_fraction() const
void unpack(const mp_integer &)
const mp_integer & get_exponent() const
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
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?