cprover
float_utilst Class Reference

#include <float_utils.h>

Inheritance diagram for float_utilst:
[legend]
Collaboration diagram for float_utilst:
[legend]

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

proptprop
 
bv_utilst bv_utils
 

Detailed Description

Definition at line 17 of file float_utils.h.

Member Enumeration Documentation

◆ relt

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

Definition at line 136 of file float_utils.h.

Constructor & Destructor Documentation

◆ float_utilst() [1/2]

float_utilst::float_utilst ( propt _prop)
inlineexplicit

Definition at line 67 of file float_utils.h.

◆ float_utilst() [2/2]

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

Definition at line 73 of file float_utils.h.

◆ ~float_utilst()

virtual float_utilst::~float_utilst ( )
inlinevirtual

Definition at line 82 of file float_utils.h.

Member Function Documentation

◆ abs()

bvt float_utilst::abs ( const bvt src)

Definition at line 565 of file float_utils.cpp.

References const_literal().

Referenced by boolbvt::convert_abs().

◆ add()

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

Definition at line 109 of file float_utils.h.

References add_sub().

Referenced by bv_refinementt::check_SAT().

◆ add_bias()

bvt float_utilst::add_bias ( const bvt exponent)
protected

◆ add_sub()

◆ bias()

◆ build_constant()

◆ conversion()

◆ debug1()

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

Definition at line 1308 of file float_utils.cpp.

◆ debug2()

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

Definition at line 1315 of file float_utils.cpp.

◆ denormalization_shift()

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

◆ div()

◆ exponent_all_ones()

literalt float_utilst::exponent_all_ones ( const bvt src)

◆ exponent_all_zeros()

literalt float_utilst::exponent_all_zeros ( const bvt src)

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().

◆ fraction_all_zeros()

literalt float_utilst::fraction_all_zeros ( const bvt src)

◆ fraction_rounding_decision()

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

◆ from_signed_integer()

◆ from_unsigned_integer()

◆ get()

ieee_floatt float_utilst::get ( const bvt src) const

◆ get_exponent()

bvt float_utilst::get_exponent ( const bvt src)

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 unpack().

◆ 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 687 of file float_utils.cpp.

References bv_utils, bv_utilst::extract(), ieee_float_spect::f, and spec.

Referenced by bv_refinementt::check_UNSAT(), and unpack().

◆ is_infinity()

literalt float_utilst::is_infinity ( const bvt src)

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(), and unpack().

◆ is_minus_inf()

literalt float_utilst::is_minus_inf ( const bvt src)

Definition at line 692 of file float_utils.cpp.

References exponent_all_ones(), fraction_all_zeros(), propt::land(), prop, and sign_bit().

◆ is_NaN()

literalt float_utilst::is_NaN ( const bvt src)

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(), and unpack().

◆ is_normal()

literalt float_utilst::is_normal ( const bvt src)

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(), and unpack().

◆ is_plus_inf()

literalt float_utilst::is_plus_inf ( const bvt src)

Definition at line 664 of file float_utils.cpp.

References exponent_all_ones(), fraction_all_zeros(), propt::land(), prop, and sign_bit().

◆ is_zero()

literalt float_utilst::is_zero ( const bvt src)

Definition at line 655 of file float_utils.cpp.

References bv_utils, and bv_utilst::is_zero().

Referenced by relation(), boolbvt::type_conversion(), and unpack().

◆ limit_distance()

bvt float_utilst::limit_distance ( const bvt dist,
mp_integer  limit 
)
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().

◆ mul()

◆ negate()

bvt float_utilst::negate ( const bvt src)

Definition at line 556 of file float_utils.cpp.

References sign_bit().

Referenced by boolbvt::convert_unary_minus().

◆ normalization_shift()

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

◆ pack()

◆ relation()

◆ rem()

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

Definition at line 541 of file float_utils.cpp.

References div(), mul(), and sub().

Referenced by boolbvt::convert_floatbv_op(), and div().

◆ round_exponent()

◆ round_fraction()

◆ rounder()

◆ set_rounding_mode()

◆ sign_bit()

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

Definition at line 90 of file float_utils.h.

Referenced by from_signed_integer(), is_minus_inf(), is_plus_inf(), negate(), relation(), and unpack().

◆ sticky_right_shift()

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

◆ sub()

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

Definition at line 114 of file float_utils.h.

References add_sub().

Referenced by bv_refinementt::check_SAT(), and rem().

◆ sub_bias()

bvt float_utilst::sub_bias ( const bvt exponent)
protected

◆ subtract_exponents()

bvt float_utilst::subtract_exponents ( const unbiased_floatt src1,
const unbiased_floatt src2 
)
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().

◆ to_integer()

◆ to_signed_integer()

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

Definition at line 68 of file float_utils.cpp.

References to_integer().

Referenced by boolbvt::convert_floatbv_typecast().

◆ to_unsigned_integer()

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

Definition at line 75 of file float_utils.cpp.

References to_integer().

Referenced by boolbvt::convert_floatbv_typecast().

◆ unpack()

Member Data Documentation

◆ bv_utils

◆ prop

◆ rounding_mode_bits

◆ spec


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