cprover
Loading...
Searching...
No Matches
float_utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_SOLVERS_FLOATBV_FLOAT_UTILS_H
11#define CPROVER_SOLVERS_FLOATBV_FLOAT_UTILS_H
12
13#include <util/ieee_float.h>
14
16
18{
19public:
66
68
69 explicit float_utilst(propt &_prop):
70 prop(_prop),
71 bv_utils(_prop)
72 {
73 }
74
75 float_utilst(propt &_prop, const floatbv_typet &type):
77 prop(_prop),
78 bv_utils(_prop)
79 {
80 }
81
82 void set_rounding_mode(const bvt &);
83
84 virtual ~float_utilst()
85 {
86 }
87
89
91
92 static inline literalt sign_bit(const bvt &src)
93 {
94 // this is the top bit
95 return src[src.size()-1];
96 }
97
98 // extraction
99 bvt get_exponent(const bvt &); // still biased
100 bvt get_fraction(const bvt &); // without hidden bit
101 literalt is_normal(const bvt &);
102 literalt is_zero(const bvt &); // this returns true on both 0 and -0
103 literalt is_infinity(const bvt &);
104 literalt is_plus_inf(const bvt &);
105 literalt is_minus_inf(const bvt &);
106 literalt is_NaN(const bvt &);
107
108 // add/sub
109 virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract);
110
111 bvt add(const bvt &src1, const bvt &src2)
112 {
113 return add_sub(src1, src2, false);
114 }
115
116 bvt sub(const bvt &src1, const bvt &src2)
117 {
118 return add_sub(src1, src2, true);
119 }
120
121 // mul/div/rem
122 virtual bvt mul(const bvt &src1, const bvt &src2);
123 virtual bvt div(const bvt &src1, const bvt &src2);
124 virtual bvt rem(const bvt &src1, const bvt &src2);
125
126 bvt abs(const bvt &);
127 bvt negate(const bvt &);
128
129 // conversion
131 bvt from_signed_integer(const bvt &);
132 bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed);
133 bvt to_signed_integer(const bvt &src, std::size_t int_width);
134 bvt to_unsigned_integer(const bvt &src, std::size_t int_width);
135 bvt conversion(const bvt &src, const ieee_float_spect &dest_spec);
136
137 // relations
138 enum class relt { LT, LE, EQ, GT, GE };
139 literalt relation(const bvt &src1, relt rel, const bvt &src2);
140
141 // constants
142 ieee_floatt get(const bvt &) const;
143
144 // helpers
148
149 // debugging hooks
150 bvt debug1(const bvt &op0, const bvt &op1);
151 bvt debug2(const bvt &op0, const bvt &op1);
152
153protected:
156
157 // unpacked
158 virtual void normalization_shift(bvt &fraction, bvt &exponent);
159 void denormalization_shift(bvt &fraction, bvt &exponent);
160
161 bvt add_bias(const bvt &exponent);
162 bvt sub_bias(const bvt &exponent);
163
164 bvt limit_distance(const bvt &dist, mp_integer limit);
165
167 {
170
172 sign(const_literal(false)),
173 infinity(const_literal(false)),
174 zero(const_literal(false)),
175 NaN(const_literal(false))
176 {
177 }
178 };
179
180 // this has a biased exponent
181 // and an _implicit_ hidden bit
183 {
184 };
185
186 // the hidden bit is explicit,
187 // and the exponent is not biased
189 {
190 };
191
193
194 // this takes unpacked format, and returns packed
195 virtual bvt rounder(const unbiased_floatt &);
196 bvt pack(const biased_floatt &);
197 unbiased_floatt unpack(const bvt &);
198
199 void round_fraction(unbiased_floatt &result);
200 void round_exponent(unbiased_floatt &result);
201
202 // rounding decision for fraction
204 const std::size_t dest_bits,
205 const literalt sign,
206 const bvt &fraction);
207
208 // helpers for adder
209
210 // computes src1.exponent-src2.exponent with extension
212 const unbiased_floatt &src1,
213 const unbiased_floatt &src2);
214
215 // computes the "sticky-bit"
217 const bvt &op,
218 const bvt &dist,
219 literalt &sticky);
220};
221
222#endif // CPROVER_SOLVERS_FLOATBV_FLOAT_UTILS_H
float_utilst(propt &_prop, const floatbv_typet &type)
Definition float_utils.h:75
bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed)
virtual ~float_utilst()
Definition float_utils.h:84
literalt is_NaN(const bvt &)
virtual void normalization_shift(bvt &fraction, bvt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
bvt build_constant(const ieee_floatt &)
bv_utilst bv_utils
bvt debug2(const bvt &op0, const bvt &op1)
virtual bvt rem(const bvt &src1, const bvt &src2)
literalt is_plus_inf(const bvt &)
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)
virtual bvt rounder(const unbiased_floatt &)
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 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)
virtual bvt div(const bvt &src1, const bvt &src2)
bvt negate(const bvt &)
ieee_floatt get(const bvt &) const
bvt add(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)
bvt abs(const bvt &)
static literalt sign_bit(const bvt &src)
Definition float_utils.h:92
float_utilst(propt &_prop)
Definition float_utils.h:69
ieee_float_spect spec
Definition float_utils.h:88
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
Definition float_utils.h:67
biased_floatt bias(const unbiased_floatt &)
takes an unbiased float, and applies the bias
Fixed-width bit-vector with IEEE floating-point interpretation.
TO_BE_DOCUMENTED.
Definition prop.h:25
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
BigInt mp_integer
Definition smt_terms.h:17
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
void set(const ieee_floatt::rounding_modet mode)
Definition float_utils.h:37
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45