cprover
Loading...
Searching...
No Matches
float_bv.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_BV_H
11#define CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H
12
13#include <util/ieee_float.h>
14#include <util/std_expr.h>
15
17{
18public:
19 exprt operator()(const exprt &src) const
20 {
21 return convert(src);
22 }
23
24 exprt convert(const exprt &) const;
25
26 static exprt negation(const exprt &, const ieee_float_spect &);
27 static exprt abs(const exprt &, const ieee_float_spect &);
28 static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &);
29 static exprt is_zero(const exprt &);
30 static exprt isnan(const exprt &, const ieee_float_spect &);
31 static exprt isinf(const exprt &, const ieee_float_spect &);
32 static exprt isnormal(const exprt &, const ieee_float_spect &);
33 static exprt isfinite(const exprt &, const ieee_float_spect &);
34
35 // add/sub
37 bool subtract,
38 const exprt &,
39 const exprt &,
40 const exprt &rm,
41 const ieee_float_spect &) const;
42
43 // mul/div
44 exprt
45 mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
46 const;
47 exprt
48 div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
49 const;
50
51 // conversion
53 const exprt &,
54 const exprt &rm,
55 const ieee_float_spect &) const;
57 const exprt &,
58 const exprt &rm,
59 const ieee_float_spect &) const;
61 const exprt &src,
62 std::size_t dest_width,
63 const exprt &rm,
64 const ieee_float_spect &);
66 const exprt &src,
67 std::size_t dest_width,
68 const exprt &rm,
69 const ieee_float_spect &);
70 static exprt to_integer(
71 const exprt &src,
72 std::size_t dest_width,
73 bool is_signed,
74 const exprt &rm,
75 const ieee_float_spect &);
77 const exprt &src,
78 const exprt &rm,
79 const ieee_float_spect &src_spec,
80 const ieee_float_spect &dest_spec) const;
81
82 // relations
83 enum class relt { LT, LE, EQ, GT, GE };
84 static exprt
85 relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &);
86
87private:
88 // helpers
89 static ieee_float_spect get_spec(const exprt &);
90 // still biased
91 static exprt get_exponent(const exprt &, const ieee_float_spect &);
92 // without hidden bit
93 static exprt get_fraction(const exprt &, const ieee_float_spect &);
94 static exprt sign_bit(const exprt &);
95
96 static exprt exponent_all_ones(const exprt &, const ieee_float_spect &);
97 static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &);
98 static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &);
99
101 {
102 // these are mutually exclusive, obviously
107
108 void get(const exprt &rm);
109 explicit rounding_mode_bitst(const exprt &rm) { get(rm); }
110 };
111
112 // unpacked
113 static void normalization_shift(exprt &fraction, exprt &exponent);
114 static void denormalization_shift(
115 exprt &fraction,
116 exprt &exponent,
117 const ieee_float_spect &);
118
119 static exprt add_bias(const exprt &exponent, const ieee_float_spect &);
120 static exprt sub_bias(const exprt &exponent, const ieee_float_spect &);
121
122 static exprt limit_distance(const exprt &dist, mp_integer limit);
123
137
138 // This has a biased exponent (unsigned)
139 // and an _implicit_ hidden bit.
141 {
142 };
143
144 // The hidden bit is explicit,
145 // and the exponent is not biased (signed)
147 {
148 };
149
150 static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &);
151
152 // this takes unpacked format, and returns packed
154 const unbiased_floatt &,
155 const exprt &rm,
156 const ieee_float_spect &) const;
157 static exprt pack(const biased_floatt &, const ieee_float_spect &);
158 static unbiased_floatt unpack(const exprt &, const ieee_float_spect &);
159
160 static void round_fraction(
161 unbiased_floatt &result,
162 const rounding_mode_bitst &,
163 const ieee_float_spect &);
164 static void round_exponent(
165 unbiased_floatt &result,
166 const rounding_mode_bitst &,
167 const ieee_float_spect &);
168
169 // rounding decision for fraction
171 const std::size_t dest_bits,
172 const exprt sign,
173 const exprt &fraction,
174 const rounding_mode_bitst &);
175
176 // helpers for adder
177
178 // computes src1.exponent-src2.exponent with extension
179 static exprt
180 subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2);
181
182 // computes the "sticky-bit"
183 static exprt
184 sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky);
185};
186
187inline exprt float_bv(const exprt &src)
188{
189 return float_bvt()(src);
190}
191
192#endif // CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H
Base class for all expressions.
Definition expr.h:56
The Boolean constant false.
Definition std_expr.h:3017
static unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
static void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
Definition float_bv.cpp:951
static exprt get_fraction(const exprt &, const ieee_float_spect &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition float_bv.cpp:933
static exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
static exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:250
static exprt to_integer(const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:364
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:324
static exprt isfinite(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:915
static exprt isnormal(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:486
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:300
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:515
static exprt is_zero(const exprt &)
Definition float_bv.cpp:234
exprt operator()(const exprt &src) const
Definition float_bv.h:19
static exprt abs(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:192
static void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
static exprt fraction_rounding_decision(const std::size_t dest_bits, const exprt sign, const exprt &fraction, const rounding_mode_bitst &)
rounding decision for fraction using sticky bit
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec) const
Definition float_bv.cpp:412
static exprt isnan(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:942
static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
static exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
Definition float_bv.cpp:923
static void denormalization_shift(exprt &fraction, exprt &exponent, const ieee_float_spect &)
make sure exponent is not too small; the exponent is unbiased
static exprt add_bias(const exprt &exponent, const ieee_float_spect &)
static exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const
static exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
Definition float_bv.cpp:496
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:734
exprt convert(const exprt &) const
Definition float_bv.cpp:19
static ieee_float_spect get_spec(const exprt &)
Definition float_bv.cpp:186
static exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:355
static exprt negation(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:202
static exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:823
static exprt isinf(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:906
static exprt sign_bit(const exprt &)
Definition float_bv.cpp:293
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:685
static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:268
static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:259
static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:212
static exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:346
static exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition float_bv.cpp:661
static exprt pack(const biased_floatt &, const ieee_float_spect &)
static void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
exprt float_bv(const exprt &src)
Definition float_bv.h:187
BigInt mp_integer
Definition smt_terms.h:18
API to expression classes.
rounding_mode_bitst(const exprt &rm)
Definition float_bv.h:109
void get(const exprt &rm)
Definition float_bv.cpp:278
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45