cprover
|
#include <float_utils.h>
Public Member Functions | |
rounding_mode_bitst () | |
void | set (const ieee_floatt::rounding_modet mode) |
Public Attributes | |
literalt | round_to_even |
literalt | round_to_zero |
literalt | round_to_plus_inf |
literalt | round_to_minus_inf |
Definition at line 20 of file float_utils.h.
|
inline |
Definition at line 29 of file float_utils.h.
|
inline |
Definition at line 37 of file float_utils.h.
References const_literal(), round_to_even, ieee_floatt::ROUND_TO_EVEN, round_to_minus_inf, ieee_floatt::ROUND_TO_MINUS_INF, round_to_plus_inf, ieee_floatt::ROUND_TO_PLUS_INF, round_to_zero, and ieee_floatt::ROUND_TO_ZERO.
Referenced by bv_refinementt::check_SAT().
literalt float_utilst::rounding_mode_bitst::round_to_even |
Definition at line 24 of file float_utils.h.
Referenced by float_utilst::fraction_rounding_decision(), float_utilst::round_exponent(), set(), and float_utilst::set_rounding_mode().
literalt float_utilst::rounding_mode_bitst::round_to_minus_inf |
Definition at line 27 of file float_utils.h.
Referenced by float_utilst::add_sub(), float_utilst::fraction_rounding_decision(), float_utilst::round_exponent(), set(), and float_utilst::set_rounding_mode().
literalt float_utilst::rounding_mode_bitst::round_to_plus_inf |
Definition at line 26 of file float_utils.h.
Referenced by float_utilst::fraction_rounding_decision(), float_utilst::round_exponent(), set(), and float_utilst::set_rounding_mode().
literalt float_utilst::rounding_mode_bitst::round_to_zero |
Definition at line 25 of file float_utils.h.
Referenced by float_utilst::fraction_rounding_decision(), set(), float_utilst::set_rounding_mode(), and float_utilst::to_integer().