cprover
|
#include <float_utils.h>
Classes | |
struct | biased_floatt |
struct | rounding_mode_bitst |
struct | unbiased_floatt |
struct | unpacked_floatt |
Public Types | |
enum | relt { relt::LT, relt::LE, relt::EQ, relt::GT, relt::GE } |
Public Member Functions | |
float_utilst (propt &_prop) | |
float_utilst (propt &_prop, const floatbv_typet &type) | |
void | set_rounding_mode (const bvt &) |
virtual | ~float_utilst () |
bvt | build_constant (const ieee_floatt &) |
bvt | get_exponent (const bvt &) |
Gets the unbiased exponent in a floating-point bit-vector. More... | |
bvt | get_fraction (const bvt &) |
Gets the fraction without hidden bit in a floating-point bit-vector src. More... | |
literalt | is_normal (const bvt &) |
literalt | is_zero (const bvt &) |
literalt | is_infinity (const bvt &) |
literalt | is_plus_inf (const bvt &) |
literalt | is_minus_inf (const bvt &) |
literalt | is_NaN (const bvt &) |
virtual bvt | add_sub (const bvt &src1, const bvt &src2, bool subtract) |
bvt | add (const bvt &src1, const bvt &src2) |
bvt | sub (const bvt &src1, const bvt &src2) |
virtual bvt | mul (const bvt &src1, const bvt &src2) |
virtual bvt | div (const bvt &src1, const bvt &src2) |
virtual bvt | rem (const bvt &src1, const bvt &src2) |
bvt | abs (const bvt &) |
bvt | negate (const bvt &) |
bvt | from_unsigned_integer (const bvt &) |
bvt | from_signed_integer (const bvt &) |
bvt | to_integer (const bvt &src, std::size_t int_width, bool is_signed) |
bvt | to_signed_integer (const bvt &src, std::size_t int_width) |
bvt | to_unsigned_integer (const bvt &src, std::size_t int_width) |
bvt | conversion (const bvt &src, const ieee_float_spect &dest_spec) |
literalt | relation (const bvt &src1, relt rel, const bvt &src2) |
ieee_floatt | get (const bvt &) const |
literalt | exponent_all_ones (const bvt &) |
literalt | exponent_all_zeros (const bvt &) |
literalt | fraction_all_zeros (const bvt &) |
bvt | debug1 (const bvt &op0, const bvt &op1) |
bvt | debug2 (const bvt &op0, const bvt &op1) |
Static Public Member Functions | |
static literalt | sign_bit (const bvt &src) |
Public Attributes | |
rounding_mode_bitst | rounding_mode_bits |
ieee_float_spect | spec |
Protected Member Functions | |
virtual void | normalization_shift (bvt &fraction, bvt &exponent) |
normalize fraction/exponent pair returns 'zero' if fraction is zero More... | |
void | denormalization_shift (bvt &fraction, bvt &exponent) |
make sure exponent is not too small; the exponent is unbiased More... | |
bvt | add_bias (const bvt &exponent) |
bvt | sub_bias (const bvt &exponent) |
bvt | limit_distance (const bvt &dist, mp_integer limit) |
Limits the shift distance. More... | |
biased_floatt | bias (const unbiased_floatt &) |
takes an unbiased float, and applies the bias More... | |
virtual bvt | rounder (const unbiased_floatt &) |
bvt | pack (const biased_floatt &) |
unbiased_floatt | unpack (const bvt &) |
void | round_fraction (unbiased_floatt &result) |
void | round_exponent (unbiased_floatt &result) |
literalt | fraction_rounding_decision (const std::size_t dest_bits, const literalt sign, const bvt &fraction) |
rounding decision for fraction using sticky bit More... | |
bvt | subtract_exponents (const unbiased_floatt &src1, const unbiased_floatt &src2) |
Subtracts the exponents. More... | |
bvt | sticky_right_shift (const bvt &op, const bvt &dist, literalt &sticky) |
Protected Attributes | |
propt & | prop |
bv_utilst | bv_utils |
Definition at line 17 of file float_utils.h.
|
strong |
Enumerator | |
---|---|
LT | |
LE | |
EQ | |
GT | |
GE |
Definition at line 136 of file float_utils.h.
|
inlineexplicit |
Definition at line 67 of file float_utils.h.
|
inline |
Definition at line 73 of file float_utils.h.
References set_rounding_mode().
|
inlinevirtual |
Definition at line 82 of file float_utils.h.
Definition at line 565 of file float_utils.cpp.
References const_literal().
Referenced by boolbvt::convert_abs(), and sub().
Definition at line 109 of file float_utils.h.
References add_sub().
Referenced by bv_refinementt::check_SAT().
Definition at line 1181 of file float_utils.cpp.
References bv_utilst::add(), ieee_float_spect::bias(), bv_utilst::build_constant(), bv_utils, ieee_float_spect::e, and spec.
Referenced by bias().
Definition at line 245 of file float_utils.cpp.
References bv_utilst::absolute_value(), bv_utilst::add(), bv_utilst::add_sub(), bias(), bv_utilst::build_constant(), bv_utils, bv_utilst::concatenate(), const_literal(), ieee_float_spect::e, float_utilst::unpacked_floatt::exponent, ieee_float_spect::f, float_utilst::unpacked_floatt::fraction, float_utilst::unpacked_floatt::infinity, propt::land(), limit_distance(), propt::lor(), propt::lselect(), propt::lxor(), float_utilst::unpacked_floatt::NaN, pack(), prop, float_utilst::rounding_mode_bitst::round_to_minus_inf, rounder(), rounding_mode_bits, bv_utilst::select(), float_utilst::unpacked_floatt::sign, bv_utilst::sign_extension(), spec, sticky_right_shift(), subtract_exponents(), unpack(), float_utilst::unpacked_floatt::zero, bv_utilst::zero_extension(), and bv_utilst::zeros().
Referenced by add(), boolbvt::convert_add_sub(), boolbvt::convert_floatbv_op(), sign_bit(), and sub().
|
protected |
takes an unbiased float, and applies the bias
Definition at line 1152 of file float_utils.cpp.
References add_bias(), float_utilst::unpacked_floatt::exponent, ieee_float_spect::f, float_utilst::unpacked_floatt::fraction, float_utilst::unpacked_floatt::infinity, propt::land(), float_utilst::unpacked_floatt::NaN, prop, float_utilst::unpacked_floatt::sign, and spec.
Referenced by add_sub(), build_constant(), conversion(), denormalization_shift(), and rounder().
bvt float_utilst::build_constant | ( | const ieee_floatt & | src | ) |
Definition at line 141 of file float_utils.cpp.
References bias(), bv_utilst::build_constant(), bv_utils, const_literal(), ieee_float_spect::e, float_utilst::unpacked_floatt::exponent, ieee_float_spect::f, float_utilst::unpacked_floatt::fraction, ieee_floatt::get_exponent(), ieee_floatt::get_fraction(), ieee_floatt::get_sign(), float_utilst::unpacked_floatt::infinity, ieee_floatt::is_infinity(), ieee_floatt::is_NaN(), float_utilst::unpacked_floatt::NaN, pack(), float_utilst::unpacked_floatt::sign, and spec.
Referenced by bv_refinementt::check_SAT().
bvt float_utilst::conversion | ( | const bvt & | src, |
const ieee_float_spect & | dest_spec | ||
) |
Definition at line 154 of file float_utils.cpp.
References bias(), bv_utils, bv_utilst::concatenate(), ieee_float_spect::e, float_utilst::unpacked_floatt::exponent, ieee_float_spect::f, float_utilst::unpacked_floatt::fraction, float_utilst::unpacked_floatt::infinity, float_utilst::unpacked_floatt::NaN, normalization_shift(), pack(), rounder(), float_utilst::unpacked_floatt::sign, bv_utilst::sign_extension(), spec, unpack(), ieee_float_spect::width(), and bv_utilst::zeros().
Referenced by boolbvt::convert_floatbv_typecast(), and sub().
Definition at line 1308 of file float_utils.cpp.
Definition at line 1315 of file float_utils.cpp.
make sure exponent is not too small; the exponent is unbiased
Definition at line 828 of file float_utils.cpp.
References ieee_float_spect::bias(), bias(), bv_utilst::build_constant(), bv_utils, bv_utilst::concatenate(), const_literal(), ieee_float_spect::e, ieee_float_spect::f, bv_utilst::is_zero(), propt::land(), propt::lor(), prop, bv_utilst::select(), bv_utilst::shift(), bv_utilst::sign_extension(), spec, sticky_right_shift(), bv_utilst::sub(), and bv_utilst::zeros().
Referenced by rounder().
Definition at line 462 of file float_utils.cpp.
References bv_utilst::add(), bv_utilst::build_constant(), bv_utils, const_literal(), float_utilst::unpacked_floatt::exponent, ieee_float_spect::f, float_utilst::unpacked_floatt::fraction, float_utilst::unpacked_floatt::infinity, bv_utilst::is_not_zero(), propt::land(), propt::lor(), propt::lxor(), float_utilst::unpacked_floatt::NaN, prop, rem(), rounder(), bv_utilst::select(), float_utilst::unpacked_floatt::sign, bv_utilst::sign_extension(), spec, bv_utilst::sub(), unpack(), bv_utilst::unsigned_divider(), float_utilst::unpacked_floatt::zero, bv_utilst::zero_extension(), and bv_utilst::zeros().
Referenced by bv_refinementt::check_SAT(), boolbvt::convert_floatbv_op(), rem(), and sub().
Definition at line 707 of file float_utils.cpp.
References bv_utils, ieee_float_spect::e, ieee_float_spect::f, bv_utilst::is_all_ones(), and spec.
Referenced by is_infinity(), is_minus_inf(), is_NaN(), is_normal(), and is_plus_inf().
Definition at line 720 of file float_utils.cpp.
References bv_utils, ieee_float_spect::e, ieee_float_spect::f, bv_utilst::is_zero(), and spec.
Referenced by is_normal().
Definition at line 733 of file float_utils.cpp.
References bv_utils, ieee_float_spect::f, bv_utilst::is_zero(), spec, and ieee_float_spect::width().
Referenced by is_infinity(), is_minus_inf(), is_NaN(), and is_plus_inf().
|
protected |
rounding decision for fraction using sticky bit
Definition at line 937 of file float_utils.cpp.
References bv_utils, const_literal(), bv_utilst::extract(), propt::land(), propt::lor(), propt::lselect(), propt::new_variable(), prop, float_utilst::rounding_mode_bitst::round_to_even, float_utilst::rounding_mode_bitst::round_to_minus_inf, float_utilst::rounding_mode_bitst::round_to_plus_inf, float_utilst::rounding_mode_bitst::round_to_zero, and rounding_mode_bits.
Referenced by round_fraction().
Definition at line 33 of file float_utils.cpp.
References bv_utilst::absolute_value(), address_bits(), bv_utilst::build_constant(), bv_utils, float_utilst::unpacked_floatt::exponent, float_utilst::unpacked_floatt::fraction, rounder(), float_utilst::unpacked_floatt::sign, and sign_bit().
Referenced by boolbvt::convert_floatbv_typecast(), sub(), and boolbvt::type_conversion().
Definition at line 51 of file float_utils.cpp.
References address_bits(), bv_utilst::build_constant(), bv_utils, const_literal(), float_utilst::unpacked_floatt::exponent, float_utilst::unpacked_floatt::fraction, rounder(), and float_utilst::unpacked_floatt::sign.
Referenced by boolbvt::convert_floatbv_typecast(), sub(), and boolbvt::type_conversion().
ieee_floatt float_utilst::get | ( | const bvt & | src | ) | const |
Definition at line 1259 of file float_utils.cpp.
References tvt::is_true(), propt::l_get(), power(), prop, spec, ieee_floatt::spec, and ieee_floatt::unpack().
Gets the unbiased exponent in a floating-point bit-vector.
Definition at line 681 of file float_utils.cpp.
References bv_utils, ieee_float_spect::e, bv_utilst::extract(), ieee_float_spect::f, and spec.
Referenced by sign_bit(), and unpack().
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition at line 687 of file float_utils.cpp.
References bv_utils, bv_utilst::extract(), ieee_float_spect::f, and spec.
Referenced by bv_refinementt::check_UNSAT(), sign_bit(), and unpack().
Definition at line 673 of file float_utils.cpp.
References exponent_all_ones(), fraction_all_zeros(), propt::land(), and prop.
Referenced by boolbvt::convert_rest(), sign_bit(), and unpack().
Definition at line 692 of file float_utils.cpp.
References exponent_all_ones(), fraction_all_zeros(), propt::land(), prop, and sign_bit().
Referenced by sign_bit().
Definition at line 701 of file float_utils.cpp.
References exponent_all_ones(), fraction_all_zeros(), propt::land(), and prop.
Referenced by boolbvt::convert_rest(), mul(), relation(), sign_bit(), and unpack().
Definition at line 221 of file float_utils.cpp.
References exponent_all_ones(), exponent_all_zeros(), propt::land(), and prop.
Referenced by boolbvt::convert_rest(), sign_bit(), and unpack().
Definition at line 664 of file float_utils.cpp.
References exponent_all_ones(), fraction_all_zeros(), propt::land(), prop, and sign_bit().
Referenced by sign_bit().
Definition at line 655 of file float_utils.cpp.
References bv_utils, and bv_utilst::is_zero().
Referenced by relation(), sign_bit(), boolbvt::type_conversion(), and unpack().
|
protected |
Limits the shift distance.
Definition at line 387 of file float_utils.cpp.
References address_bits(), integer2unsigned(), propt::lor(), and prop.
Referenced by add_sub().
Definition at line 410 of file float_utils.cpp.
References bv_utilst::add(), bv_utils, float_utilst::unpacked_floatt::exponent, float_utilst::unpacked_floatt::fraction, bv_utilst::inc(), float_utilst::unpacked_floatt::infinity, is_NaN(), propt::land(), propt::lor(), propt::lxor(), float_utilst::unpacked_floatt::NaN, prop, rounder(), float_utilst::unpacked_floatt::sign, bv_utilst::sign_extension(), unpack(), bv_utilst::unsigned_multiplier(), float_utilst::unpacked_floatt::zero, and bv_utilst::zero_extension().
Referenced by bv_refinementt::check_SAT(), boolbvt::convert_floatbv_op(), rem(), and sub().
Definition at line 556 of file float_utils.cpp.
References sign_bit().
Referenced by boolbvt::convert_unary_minus(), and sub().
normalize fraction/exponent pair returns 'zero' if fraction is zero
Reimplemented in float_approximationt.
Definition at line 743 of file float_utils.cpp.
References bv_utilst::add(), address_bits(), bv_utilst::build_constant(), bv_utils, bv_utilst::cond_implies_equal(), const_literal(), bv_utilst::extract_msb(), integer2unsigned(), bv_utilst::is_zero(), propt::land(), bv_utilst::LEFT, propt::new_variables(), prop, bv_utilst::select(), bv_utilst::shift(), bv_utilst::sign_extension(), bv_utilst::sub(), and bv_utilst::zeros().
Referenced by conversion(), and rounder().
|
protected |
Definition at line 1228 of file float_utils.cpp.
References const_literal(), ieee_float_spect::e, float_utilst::unpacked_floatt::exponent, ieee_float_spect::f, float_utilst::unpacked_floatt::fraction, float_utilst::unpacked_floatt::infinity, propt::land(), propt::lor(), propt::lselect(), float_utilst::unpacked_floatt::NaN, prop, float_utilst::unpacked_floatt::sign, spec, and ieee_float_spect::width().
Referenced by add_sub(), build_constant(), conversion(), and rounder().
Definition at line 573 of file float_utils.cpp.
References bv_utils, const_literal(), EQ, bv_utilst::equal(), GE, GT, is_NaN(), is_zero(), propt::land(), LE, propt::lor(), propt::lselect(), LT, propt::lxor(), prop, sign_bit(), and bv_utilst::unsigned_less_than().
Referenced by boolbvt::convert_bv_rel(), and boolbvt::convert_ieee_float_rel().
Definition at line 541 of file float_utils.cpp.
References div(), mul(), and sub().
Referenced by boolbvt::convert_floatbv_op(), div(), and sub().
|
protected |
Definition at line 1086 of file float_utils.cpp.
References ieee_float_spect::bias(), bv_utilst::build_constant(), bv_utils, ieee_float_spect::e, float_utilst::unpacked_floatt::exponent, float_utilst::unpacked_floatt::fraction, float_utilst::unpacked_floatt::infinity, bv_utilst::inverted(), bv_utilst::is_zero(), propt::land(), propt::lor(), ieee_float_spect::max_exponent(), prop, float_utilst::rounding_mode_bitst::round_to_even, float_utilst::rounding_mode_bitst::round_to_minus_inf, float_utilst::rounding_mode_bitst::round_to_plus_inf, rounding_mode_bits, bv_utilst::select(), float_utilst::unpacked_floatt::sign, bv_utilst::signed_less_than(), spec, and bv_utilst::zeros().
Referenced by rounder().
|
protected |
Definition at line 994 of file float_utils.cpp.
References bv_utils, bv_utilst::concatenate(), float_utilst::unpacked_floatt::exponent, bv_utilst::extract(), ieee_float_spect::f, float_utilst::unpacked_floatt::fraction, fraction_rounding_decision(), bv_utilst::incrementer(), propt::land(), propt::lor(), neg(), prop, float_utilst::unpacked_floatt::sign, spec, bv_utilst::zero_extension(), and bv_utilst::zeros().
Referenced by rounder().
|
protectedvirtual |
Definition at line 896 of file float_utils.cpp.
References address_bits(), bias(), bv_utils, denormalization_shift(), ieee_float_spect::e, float_utilst::unpacked_floatt::exponent, ieee_float_spect::f, float_utilst::unpacked_floatt::fraction, float_utilst::unpacked_floatt::infinity, integer2size_t(), float_utilst::unpacked_floatt::NaN, normalization_shift(), pack(), round_exponent(), round_fraction(), float_utilst::unpacked_floatt::sign, bv_utilst::sign_extension(), and spec.
Referenced by add_sub(), conversion(), div(), from_signed_integer(), from_unsigned_integer(), and mul().
void float_utilst::set_rounding_mode | ( | const bvt & | src | ) |
Definition at line 16 of file float_utils.cpp.
References bv_utilst::build_constant(), bv_utils, bv_utilst::equal(), float_utilst::rounding_mode_bitst::round_to_even, ieee_floatt::ROUND_TO_EVEN, float_utilst::rounding_mode_bitst::round_to_minus_inf, ieee_floatt::ROUND_TO_MINUS_INF, float_utilst::rounding_mode_bitst::round_to_plus_inf, ieee_floatt::ROUND_TO_PLUS_INF, float_utilst::rounding_mode_bitst::round_to_zero, ieee_floatt::ROUND_TO_ZERO, and rounding_mode_bits.
Referenced by boolbvt::convert_floatbv_op(), boolbvt::convert_floatbv_typecast(), and float_utilst().
Definition at line 90 of file float_utils.h.
References add_sub(), get_exponent(), get_fraction(), is_infinity(), is_minus_inf(), is_NaN(), is_normal(), is_plus_inf(), and is_zero().
Referenced by from_signed_integer(), is_minus_inf(), is_plus_inf(), negate(), relation(), and unpack().
|
protected |
Definition at line 1273 of file float_utils.cpp.
References bv_utils, const_literal(), bv_utilst::extract(), propt::land(), propt::lor(), bv_utilst::LRIGHT, prop, bv_utilst::select(), and bv_utilst::shift().
Referenced by add_sub(), and denormalization_shift().
Definition at line 114 of file float_utils.h.
References abs(), add_sub(), conversion(), div(), from_signed_integer(), from_unsigned_integer(), is_signed(), mul(), negate(), rem(), to_integer(), to_signed_integer(), and to_unsigned_integer().
Referenced by bv_refinementt::check_SAT(), and rem().
Definition at line 1190 of file float_utils.cpp.
References ieee_float_spect::bias(), bv_utilst::build_constant(), bv_utils, ieee_float_spect::e, spec, and bv_utilst::sub().
Referenced by unpack().
|
protected |
Subtracts the exponents.
Definition at line 229 of file float_utils.cpp.
References bv_utils, float_utilst::unpacked_floatt::exponent, bv_utilst::sign_extension(), and bv_utilst::sub().
Referenced by add_sub().
Definition at line 82 of file float_utils.cpp.
References bv_utilst::build_constant(), bv_utils, bv_utilst::cond_negate(), literalt::is_true(), propt::land(), bv_utilst::LRIGHT, prop, float_utilst::rounding_mode_bitst::round_to_zero, rounding_mode_bits, bv_utilst::shift(), spec, bv_utilst::sub(), unpack(), and ieee_float_spect::width().
Referenced by sub(), to_signed_integer(), and to_unsigned_integer().
Definition at line 68 of file float_utils.cpp.
References to_integer().
Referenced by boolbvt::convert_floatbv_typecast(), and sub().
Definition at line 75 of file float_utils.cpp.
References to_integer().
Referenced by boolbvt::convert_floatbv_typecast(), and sub().
|
protected |
Definition at line 1199 of file float_utils.cpp.
References ieee_float_spect::bias(), bv_utilst::build_constant(), bv_utils, ieee_float_spect::e, get_exponent(), get_fraction(), is_infinity(), is_NaN(), is_normal(), is_zero(), bv_utilst::is_zero(), bv_utilst::select(), float_utilst::unpacked_floatt::sign, sign_bit(), spec, sub_bias(), and ieee_float_spect::width().
Referenced by add_sub(), conversion(), div(), mul(), and to_integer().
|
protected |
Definition at line 153 of file float_utils.h.
Referenced by add_bias(), add_sub(), build_constant(), conversion(), denormalization_shift(), div(), exponent_all_ones(), exponent_all_zeros(), fraction_all_zeros(), fraction_rounding_decision(), from_signed_integer(), from_unsigned_integer(), get_exponent(), get_fraction(), is_zero(), mul(), float_approximationt::normalization_shift(), normalization_shift(), relation(), round_exponent(), round_fraction(), rounder(), set_rounding_mode(), sticky_right_shift(), sub_bias(), subtract_exponents(), to_integer(), and unpack().
|
protected |
Definition at line 152 of file float_utils.h.
Referenced by add_sub(), bias(), denormalization_shift(), div(), fraction_rounding_decision(), get(), is_infinity(), is_minus_inf(), is_NaN(), is_normal(), is_plus_inf(), limit_distance(), mul(), float_approximationt::normalization_shift(), normalization_shift(), float_approximationt::overapproximating_left_shift(), pack(), relation(), round_exponent(), round_fraction(), sticky_right_shift(), and to_integer().
rounding_mode_bitst float_utilst::rounding_mode_bits |
Definition at line 65 of file float_utils.h.
Referenced by add_sub(), bv_refinementt::check_SAT(), fraction_rounding_decision(), round_exponent(), set_rounding_mode(), and to_integer().
ieee_float_spect float_utilst::spec |
Definition at line 86 of file float_utils.h.
Referenced by add_bias(), add_sub(), bias(), build_constant(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), conversion(), boolbvt::convert_floatbv_op(), boolbvt::convert_floatbv_typecast(), denormalization_shift(), div(), exponent_all_ones(), exponent_all_zeros(), fraction_all_zeros(), get(), get_exponent(), get_fraction(), pack(), round_exponent(), round_fraction(), rounder(), sub_bias(), to_integer(), boolbvt::type_conversion(), and unpack().