cprover
Loading...
Searching...
No Matches
float_utilst Class Reference

#include <float_utils.h>

Inheritance diagram for float_utilst:
Collaboration diagram for float_utilst:

Classes

struct  biased_floatt
struct  rounding_mode_bitst
struct  unbiased_floatt
struct  unpacked_floatt

Public Types

enum class  relt {
  LT , LE , EQ , GT ,
  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_float_valuet &)
bvt get_exponent (const bvt &)
 Gets the unbiased exponent in a floating-point bit-vector.
bvt get_fraction (const bvt &)
 Gets the fraction without hidden bit in a floating-point bit-vector src.
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)
bvt round_to_integral (const bvt &)
literalt relation (const bvt &src1, relt rel, const bvt &src2)
ieee_float_valuet 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
void denormalization_shift (bvt &fraction, bvt &exponent)
 make sure exponent is not too small; the exponent is unbiased
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.
unbiased_floatt unpack (const bvt &)
biased_floatt bias (const unbiased_floatt &)
 takes an unbiased float, and applies the bias
unbiased_floatt rounder (const unbiased_floatt &)
bvt round_and_pack (const unbiased_floatt &)
bvt pack (const biased_floatt &)
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
bvt subtract_exponents (const unbiased_floatt &src1, const unbiased_floatt &src2)
 Subtracts the exponents.
bvt sticky_right_shift (const bvt &op, const bvt &dist, literalt &sticky)

Protected Attributes

proptprop
bv_utilst bv_utils

Detailed Description

Definition at line 17 of file float_utils.h.

Member Enumeration Documentation

◆ relt

enum class float_utilst::relt
strong
Enumerator
LT 
LE 
EQ 
GT 
GE 

Definition at line 145 of file float_utils.h.

Constructor & Destructor Documentation

◆ float_utilst() [1/2]

float_utilst::float_utilst ( propt & _prop)
inlineexplicit

Definition at line 75 of file float_utils.h.

◆ float_utilst() [2/2]

float_utilst::float_utilst ( propt & _prop,
const floatbv_typet & type )
inline

Definition at line 81 of file float_utils.h.

◆ ~float_utilst()

virtual float_utilst::~float_utilst ( )
inlinevirtual

Definition at line 90 of file float_utils.h.

Member Function Documentation

◆ abs()

bvt float_utilst::abs ( const bvt & src)

Definition at line 603 of file float_utils.cpp.

◆ add()

bvt float_utilst::add ( const bvt & src1,
const bvt & src2 )
inline

Definition at line 117 of file float_utils.h.

◆ add_bias()

bvt float_utilst::add_bias ( const bvt & exponent)
protected

Definition at line 1237 of file float_utils.cpp.

◆ add_sub()

bvt float_utilst::add_sub ( const bvt & src1,
const bvt & src2,
bool subtract )
virtual

Definition at line 280 of file float_utils.cpp.

◆ bias()

float_utilst::biased_floatt float_utilst::bias ( const unbiased_floatt & src)
protected

takes an unbiased float, and applies the bias

Definition at line 1207 of file float_utils.cpp.

◆ build_constant()

bvt float_utilst::build_constant ( const ieee_float_valuet & src)

Definition at line 142 of file float_utils.cpp.

◆ conversion()

bvt float_utilst::conversion ( const bvt & src,
const ieee_float_spect & dest_spec )

Definition at line 185 of file float_utils.cpp.

◆ debug1()

bvt float_utilst::debug1 ( const bvt & op0,
const bvt & op1 )

Definition at line 1364 of file float_utils.cpp.

◆ debug2()

bvt float_utilst::debug2 ( const bvt & op0,
const bvt & op1 )

Definition at line 1371 of file float_utils.cpp.

◆ denormalization_shift()

void float_utilst::denormalization_shift ( bvt & fraction,
bvt & exponent )
protected

make sure exponent is not too small; the exponent is unbiased

Definition at line 869 of file float_utils.cpp.

◆ div()

bvt float_utilst::div ( const bvt & src1,
const bvt & src2 )
virtual

Definition at line 497 of file float_utils.cpp.

◆ exponent_all_ones()

literalt float_utilst::exponent_all_ones ( const bvt & src)

Definition at line 744 of file float_utils.cpp.

◆ exponent_all_zeros()

literalt float_utilst::exponent_all_zeros ( const bvt & src)

Definition at line 757 of file float_utils.cpp.

◆ fraction_all_zeros()

literalt float_utilst::fraction_all_zeros ( const bvt & src)

Definition at line 770 of file float_utils.cpp.

◆ fraction_rounding_decision()

literalt float_utilst::fraction_rounding_decision ( const std::size_t dest_bits,
const literalt sign,
const bvt & fraction )
protected

rounding decision for fraction using sticky bit

Definition at line 981 of file float_utils.cpp.

◆ from_signed_integer()

bvt float_utilst::from_signed_integer ( const bvt & src)

Definition at line 35 of file float_utils.cpp.

◆ from_unsigned_integer()

bvt float_utilst::from_unsigned_integer ( const bvt & src)

Definition at line 53 of file float_utils.cpp.

◆ get()

ieee_float_valuet float_utilst::get ( const bvt & src) const

Definition at line 1315 of file float_utils.cpp.

◆ get_exponent()

bvt float_utilst::get_exponent ( const bvt & src)

Gets the unbiased exponent in a floating-point bit-vector.

Definition at line 718 of file float_utils.cpp.

◆ get_fraction()

bvt float_utilst::get_fraction ( const bvt & src)

Gets the fraction without hidden bit in a floating-point bit-vector src.

Definition at line 724 of file float_utils.cpp.

◆ is_infinity()

literalt float_utilst::is_infinity ( const bvt & src)

Definition at line 710 of file float_utils.cpp.

◆ is_minus_inf()

literalt float_utilst::is_minus_inf ( const bvt & src)

Definition at line 729 of file float_utils.cpp.

◆ is_NaN()

literalt float_utilst::is_NaN ( const bvt & src)

Definition at line 738 of file float_utils.cpp.

◆ is_normal()

literalt float_utilst::is_normal ( const bvt & src)

Definition at line 256 of file float_utils.cpp.

◆ is_plus_inf()

literalt float_utilst::is_plus_inf ( const bvt & src)

Definition at line 701 of file float_utils.cpp.

◆ is_zero()

literalt float_utilst::is_zero ( const bvt & src)

Definition at line 692 of file float_utils.cpp.

◆ limit_distance()

bvt float_utilst::limit_distance ( const bvt & dist,
mp_integer limit )
protected

Limits the shift distance.

Definition at line 422 of file float_utils.cpp.

◆ mul()

bvt float_utilst::mul ( const bvt & src1,
const bvt & src2 )
virtual

Definition at line 445 of file float_utils.cpp.

◆ negate()

bvt float_utilst::negate ( const bvt & src)

Definition at line 594 of file float_utils.cpp.

◆ normalization_shift()

void float_utilst::normalization_shift ( bvt & fraction,
bvt & exponent )
protectedvirtual

normalize fraction/exponent pair returns 'zero' if fraction is zero

Reimplemented in float_approximationt.

Definition at line 780 of file float_utils.cpp.

◆ pack()

bvt float_utilst::pack ( const biased_floatt & src)
protected

Definition at line 1284 of file float_utils.cpp.

◆ relation()

literalt float_utilst::relation ( const bvt & src1,
relt rel,
const bvt & src2 )

Definition at line 611 of file float_utils.cpp.

◆ rem()

bvt float_utilst::rem ( const bvt & src1,
const bvt & src2 )
virtual

Definition at line 576 of file float_utils.cpp.

◆ round_and_pack()

bvt float_utilst::round_and_pack ( const unbiased_floatt & src)
protected

Definition at line 975 of file float_utils.cpp.

◆ round_exponent()

void float_utilst::round_exponent ( unbiased_floatt & result)
protected

Definition at line 1144 of file float_utils.cpp.

◆ round_fraction()

void float_utilst::round_fraction ( unbiased_floatt & result)
protected

Definition at line 1045 of file float_utils.cpp.

◆ round_to_integral()

bvt float_utilst::round_to_integral ( const bvt & src)

Definition at line 155 of file float_utils.cpp.

◆ rounder()

float_utilst::unbiased_floatt float_utilst::rounder ( const unbiased_floatt & src)
protected

Definition at line 937 of file float_utils.cpp.

◆ set_rounding_mode()

void float_utilst::set_rounding_mode ( const bvt & src)

Definition at line 15 of file float_utils.cpp.

◆ sign_bit()

literalt float_utilst::sign_bit ( const bvt & src)
inlinestatic

Definition at line 98 of file float_utils.h.

◆ sticky_right_shift()

bvt float_utilst::sticky_right_shift ( const bvt & op,
const bvt & dist,
literalt & sticky )
protected

Definition at line 1329 of file float_utils.cpp.

◆ sub()

bvt float_utilst::sub ( const bvt & src1,
const bvt & src2 )
inline

Definition at line 122 of file float_utils.h.

◆ sub_bias()

bvt float_utilst::sub_bias ( const bvt & exponent)
protected

Definition at line 1246 of file float_utils.cpp.

◆ subtract_exponents()

bvt float_utilst::subtract_exponents ( const unbiased_floatt & src1,
const unbiased_floatt & src2 )
protected

Subtracts the exponents.

Definition at line 264 of file float_utils.cpp.

◆ to_integer()

bvt float_utilst::to_integer ( const bvt & src,
std::size_t int_width,
bool is_signed )

Definition at line 84 of file float_utils.cpp.

◆ to_signed_integer()

bvt float_utilst::to_signed_integer ( const bvt & src,
std::size_t int_width )

Definition at line 70 of file float_utils.cpp.

◆ to_unsigned_integer()

bvt float_utilst::to_unsigned_integer ( const bvt & src,
std::size_t int_width )

Definition at line 77 of file float_utils.cpp.

◆ unpack()

float_utilst::unbiased_floatt float_utilst::unpack ( const bvt & src)
protected

Definition at line 1255 of file float_utils.cpp.

Member Data Documentation

◆ bv_utils

bv_utilst float_utilst::bv_utils
protected

Definition at line 162 of file float_utils.h.

◆ prop

propt& float_utilst::prop
protected

Definition at line 161 of file float_utils.h.

◆ rounding_mode_bits

rounding_mode_bitst float_utilst::rounding_mode_bits

Definition at line 73 of file float_utils.h.

◆ spec

ieee_float_spect float_utilst::spec

Definition at line 94 of file float_utils.h.


The documentation for this class was generated from the following files: