1 |
|
/* |
2 |
|
** Copyright (C) 2018 Martin Brain |
3 |
|
** |
4 |
|
** See the file LICENSE for licensing information. |
5 |
|
*/ |
6 |
|
|
7 |
|
/* |
8 |
|
** compare.h |
9 |
|
** |
10 |
|
** Martin Brain |
11 |
|
** martin.brain@cs.ox.ac.uk |
12 |
|
** 25/08/14 |
13 |
|
** |
14 |
|
** Comparison between floating-point numbers |
15 |
|
** |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "symfpu/core/unpackedFloat.h" |
19 |
|
#include "symfpu/core/ite.h" |
20 |
|
|
21 |
|
#ifndef SYMFPU_COMPARE |
22 |
|
#define SYMFPU_COMPARE |
23 |
|
|
24 |
|
namespace symfpu { |
25 |
|
|
26 |
|
// SMT-LIB equality |
27 |
|
template <class t> |
28 |
2646 |
typename t::prop smtlibEqual (const typename t::fpt &format, |
29 |
|
const unpackedFloat<t> &left, |
30 |
|
const unpackedFloat<t> &right) { |
31 |
|
typedef typename t::prop prop; |
32 |
|
|
33 |
2646 |
PRECONDITION(left.valid(format)); |
34 |
2646 |
PRECONDITION(right.valid(format)); |
35 |
|
|
36 |
|
// Relies on a number of properties of the unpacked format |
37 |
|
// particularly the use of default exponents, significands and signs |
38 |
|
|
39 |
8254 |
prop flagsEqual((left.getNaN() == right.getNaN()) && |
40 |
4915 |
(left.getInf() == right.getInf()) && |
41 |
7207 |
(left.getZero() == right.getZero()) && |
42 |
2608 |
(left.getSign() == right.getSign())); |
43 |
|
|
44 |
2981 |
prop flagsAndExponent(flagsEqual && left.getExponent() == right.getExponent()); |
45 |
|
|
46 |
|
// Avoid comparing (and thus instantiating) the significand unless necessary |
47 |
2646 |
probabilityAnnotation<t,prop>(flagsAndExponent, UNLIKELY); |
48 |
|
|
49 |
7603 |
prop res(ITE(flagsAndExponent, |
50 |
4957 |
left.getSignificand() == right.getSignificand(), |
51 |
|
prop(false))); |
52 |
|
|
53 |
2981 |
return res; |
54 |
|
} |
55 |
|
|
56 |
|
// IEEE-754 Equality (not actually an equivalence relation but ...) |
57 |
|
template <class t> |
58 |
|
typename t::prop ieee754Equal (const typename t::fpt &format, |
59 |
|
const unpackedFloat<t> &left, |
60 |
|
const unpackedFloat<t> &right) { |
61 |
|
|
62 |
|
typedef typename t::prop prop; |
63 |
|
|
64 |
|
PRECONDITION(left.valid(format)); |
65 |
|
PRECONDITION(right.valid(format)); |
66 |
|
|
67 |
|
prop neitherNan(!left.getNaN() && !right.getNaN()); // All comparison with NaN are false |
68 |
|
prop bothZero(left.getZero() && right.getZero()); // Both zeros are equal |
69 |
|
prop neitherZero(!left.getZero() && !right.getZero()); |
70 |
|
|
71 |
|
prop flagsAndExponent(neitherNan && |
72 |
|
(bothZero || (neitherZero && |
73 |
|
(left.getInf() == right.getInf() && |
74 |
|
left.getSign() == right.getSign() && |
75 |
|
left.getExponent() == right.getExponent())))); |
76 |
|
|
77 |
|
// Avoid comparing (and thus instantiating) the significand unless necessary |
78 |
|
probabilityAnnotation<t,prop>(flagsAndExponent, UNLIKELY); |
79 |
|
|
80 |
|
prop res(ITE(flagsAndExponent, left.getSignificand() == right.getSignificand(), prop(false))); |
81 |
|
|
82 |
|
return res; |
83 |
|
} |
84 |
|
|
85 |
|
|
86 |
|
// Share the common comparison code between functions |
87 |
|
// equality == true if the equal case returns true |
88 |
|
// IEEE-754 semantics for ordering with NaN |
89 |
|
// (i.e. unordered with everything, not even equal to itself) |
90 |
|
template <class t> |
91 |
300 |
typename t::prop ordering (const typename t::fpt &format, |
92 |
|
const unpackedFloat<t> &left, |
93 |
|
const unpackedFloat<t> &right, |
94 |
|
const typename t::prop equality) { |
95 |
|
|
96 |
|
typedef typename t::prop prop; |
97 |
|
|
98 |
300 |
PRECONDITION(left.valid(format)); |
99 |
300 |
PRECONDITION(right.valid(format)); |
100 |
|
|
101 |
|
// All comparison with NaN are false |
102 |
356 |
prop neitherNaN(!left.getNaN() && !right.getNaN()); |
103 |
|
|
104 |
|
// Either is an infinity (wrong in the case of NaN but will be corrected) |
105 |
1200 |
prop infCase( (left.isNegativeInf() && ITE(equality, prop(true), !right.isNegativeInf()) ) || |
106 |
968 |
(right.isPositiveInf() && ITE(equality, prop(true), !left.isPositiveInf()) ) || |
107 |
591 |
(ITE(equality, left.getInf() && right.getInf() && left.getSign() == right.getSign(), prop(false))) ); |
108 |
|
|
109 |
|
|
110 |
|
// Either is a zero (wrong in the case of NaN but will be corrected) |
111 |
1036 |
prop zeroCase( ( left.getZero() && !right.getZero() && !right.getSign()) || |
112 |
804 |
(right.getZero() && !left.getZero() && left.getSign()) || |
113 |
473 |
(ITE(equality, left.getZero() && right.getZero(), prop(false))) ); |
114 |
|
|
115 |
|
|
116 |
|
// Normal and subnormal case |
117 |
1256 |
prop normalOrSubnormal(!left.getNaN() && !right.getNaN() && |
118 |
819 |
!left.getInf() && !right.getInf() && |
119 |
747 |
!left.getZero() && !right.getZero()); |
120 |
|
|
121 |
356 |
prop negativeLessThanPositive(normalOrSubnormal && left.getSign() && !right.getSign()); |
122 |
|
|
123 |
356 |
prop exponentNeeded(normalOrSubnormal && left.getSign() == right.getSign()); |
124 |
300 |
probabilityAnnotation<t>(exponentNeeded, UNLIKELY); |
125 |
|
|
126 |
439 |
prop positiveCase(!left.getSign() && !right.getSign() && |
127 |
139 |
left.getExponent() < right.getExponent()); |
128 |
376 |
prop negativeCase( left.getSign() && right.getSign() && |
129 |
76 |
left.getExponent() > right.getExponent()); |
130 |
|
|
131 |
|
|
132 |
356 |
prop exponentEqual(left.getExponent() == right.getExponent()); |
133 |
|
|
134 |
356 |
prop significandNeeded(exponentNeeded && exponentEqual); |
135 |
300 |
probabilityAnnotation<t>(significandNeeded, VERYUNLIKELY); |
136 |
|
|
137 |
439 |
prop positiveExEqCase(!left.getSign() && !right.getSign() && |
138 |
139 |
left.getSignificand() < right.getSignificand()); |
139 |
376 |
prop negativeExEqCase( left.getSign() && right.getSign() && |
140 |
76 |
left.getSignificand() > right.getSignificand()); |
141 |
|
|
142 |
439 |
prop positiveExEqCaseEq(!left.getSign() && !right.getSign() && |
143 |
139 |
left.getSignificand() <= right.getSignificand()); |
144 |
376 |
prop negativeExEqCaseEq( left.getSign() && right.getSign() && |
145 |
76 |
left.getSignificand() >= right.getSignificand()); |
146 |
|
|
147 |
488 |
return ITE(!normalOrSubnormal, |
148 |
488 |
neitherNaN && (infCase || zeroCase), |
149 |
488 |
ITE(!exponentNeeded, |
150 |
|
negativeLessThanPositive, |
151 |
488 |
ITE(!significandNeeded, |
152 |
488 |
positiveCase || negativeCase, |
153 |
488 |
ITE(equality, |
154 |
488 |
positiveExEqCaseEq || negativeExEqCaseEq, |
155 |
844 |
positiveExEqCase || negativeExEqCase)))); |
156 |
|
} |
157 |
|
|
158 |
|
|
159 |
|
template <class t> |
160 |
6 |
typename t::prop lessThan (const typename t::fpt &format, |
161 |
|
const unpackedFloat<t> &left, |
162 |
|
const unpackedFloat<t> &right) { |
163 |
6 |
PRECONDITION(left.valid(format)); |
164 |
6 |
PRECONDITION(right.valid(format)); |
165 |
|
|
166 |
|
typedef typename t::prop prop; |
167 |
|
|
168 |
6 |
return ordering(format, left, right, prop(false)); |
169 |
|
} |
170 |
|
|
171 |
|
|
172 |
|
template <class t> |
173 |
78 |
typename t::prop lessThanOrEqual (const typename t::fpt &format, |
174 |
|
const unpackedFloat<t> &left, |
175 |
|
const unpackedFloat<t> &right) { |
176 |
78 |
PRECONDITION(left.valid(format)); |
177 |
78 |
PRECONDITION(right.valid(format)); |
178 |
|
|
179 |
|
typedef typename t::prop prop; |
180 |
|
|
181 |
78 |
return ordering(format, left, right, prop(true)); |
182 |
|
} |
183 |
|
|
184 |
|
|
185 |
|
// Note that IEEE-754 says that max(+0,-0) = +/-0 and max(-0,+0) = +/- 0 |
186 |
|
template <class t> |
187 |
216 |
unpackedFloat<t> max (const typename t::fpt &format, |
188 |
|
const unpackedFloat<t> &left, |
189 |
|
const unpackedFloat<t> &right, |
190 |
|
const typename t::prop &zeroCase) { |
191 |
432 |
return ITE(left.getNaN() || ordering(format, left, right, zeroCase), |
192 |
|
right, |
193 |
432 |
left); |
194 |
|
} |
195 |
|
|
196 |
|
// Note that IEEE-754 says that min(+0,-0) = +/-0 and min(-0,+0) = +/- 0 |
197 |
|
// this will always return the left one. |
198 |
|
template <class t> |
199 |
|
unpackedFloat<t> min (const typename t::fpt &format, |
200 |
|
const unpackedFloat<t> &left, |
201 |
|
const unpackedFloat<t> &right, |
202 |
|
const typename t::prop &zeroCase) { |
203 |
|
return ITE(right.getNaN() || ordering(format, left, right, zeroCase), |
204 |
|
left, |
205 |
|
right); |
206 |
|
} |
207 |
|
|
208 |
|
|
209 |
|
|
210 |
|
template <class t> |
211 |
|
typename t::prop originalLessThan (const typename t::fpt &format, |
212 |
|
const unpackedFloat<t> &left, |
213 |
|
const unpackedFloat<t> &right) { |
214 |
|
|
215 |
|
typedef typename t::prop prop; |
216 |
|
|
217 |
|
PRECONDITION(left.valid(format)); |
218 |
|
PRECONDITION(right.valid(format)); |
219 |
|
|
220 |
|
// Optimisation : merge < and == |
221 |
|
|
222 |
|
|
223 |
|
// All comparison with NaN are false |
224 |
|
prop neitherNan(!left.getNaN() && !right.getNaN()); |
225 |
|
|
226 |
|
// Infinities are bigger than everything but themself |
227 |
|
prop eitherInf(left.getInf() || right.getInf()); |
228 |
|
prop infCase(( left.isNegativeInf() && !right.isNegativeInf()) || |
229 |
|
(!left.isPositiveInf() && right.isPositiveInf())); |
230 |
|
|
231 |
|
|
232 |
|
// Both zero are equal |
233 |
|
prop eitherZero(left.getZero() || right.getZero()); |
234 |
|
prop zeroCase(( left.getZero() && !right.getZero() && !right.getSign()) || |
235 |
|
(!left.getZero() && left.getSign() && right.getZero())); |
236 |
|
|
237 |
|
|
238 |
|
// Normal and subnormal |
239 |
|
|
240 |
|
prop negativeLessThanPositive(left.getSign() && !right.getSign()); // - < + |
241 |
|
prop positiveCase(!left.getSign() && !right.getSign() && |
242 |
|
((left.getExponent() < right.getExponent()) || |
243 |
|
(left.getExponent() == right.getExponent() && |
244 |
|
left.getSignificand() < right.getSignificand()))); |
245 |
|
|
246 |
|
prop negativeCase(left.getSign() && right.getSign() && |
247 |
|
((left.getExponent() > right.getExponent()) || |
248 |
|
(left.getExponent() == right.getExponent() && |
249 |
|
left.getSignificand() > right.getSignificand()))); |
250 |
|
|
251 |
|
|
252 |
|
return neitherNan && |
253 |
|
ITE(eitherInf, |
254 |
|
infCase, |
255 |
|
ITE(eitherZero, |
256 |
|
zeroCase, |
257 |
|
negativeLessThanPositive || positiveCase || negativeCase)); |
258 |
|
} |
259 |
|
|
260 |
|
// Optimised combination of the two |
261 |
|
template <class t> |
262 |
|
typename t::prop originalLessThanOrEqual (const typename t::fpt &format, |
263 |
|
const unpackedFloat<t> &left, |
264 |
|
const unpackedFloat<t> &right) { |
265 |
|
|
266 |
|
typedef typename t::prop prop; |
267 |
|
|
268 |
|
PRECONDITION(left.valid(format)); |
269 |
|
PRECONDITION(right.valid(format)); |
270 |
|
|
271 |
|
// Optimisation : merge < and == |
272 |
|
|
273 |
|
|
274 |
|
// All comparison with NaN are false |
275 |
|
prop neitherNan(!left.getNaN() && !right.getNaN()); |
276 |
|
|
277 |
|
// Infinities are bigger than everything but themself |
278 |
|
prop eitherInf(left.getInf() || right.getInf()); |
279 |
|
prop infCase( (left.getInf() && right.getInf() && left.getSign() == right.getSign()) || |
280 |
|
left.isNegativeInf() || |
281 |
|
right.isPositiveInf()); |
282 |
|
|
283 |
|
|
284 |
|
// Both zero are equal |
285 |
|
prop eitherZero(left.getZero() || right.getZero()); |
286 |
|
prop zeroCase((left.getZero() && right.getZero()) || |
287 |
|
( left.getZero() && !right.getSign()) || |
288 |
|
( left.getSign() && right.getZero())); |
289 |
|
|
290 |
|
|
291 |
|
// Normal and subnormal |
292 |
|
|
293 |
|
prop negativeLessThanPositive(left.getSign() && !right.getSign()); // - < + |
294 |
|
prop positiveCase(!left.getSign() && !right.getSign() && |
295 |
|
((left.getExponent() < right.getExponent()) || |
296 |
|
(left.getExponent() == right.getExponent() && |
297 |
|
left.getSignificand() <= right.getSignificand()))); |
298 |
|
|
299 |
|
prop negativeCase(left.getSign() && right.getSign() && |
300 |
|
((left.getExponent() > right.getExponent()) || |
301 |
|
(left.getExponent() == right.getExponent() && |
302 |
|
left.getSignificand() >= right.getSignificand()))); |
303 |
|
|
304 |
|
|
305 |
|
return neitherNan && |
306 |
|
ITE(eitherInf, |
307 |
|
infCase, |
308 |
|
ITE(eitherZero, |
309 |
|
zeroCase, |
310 |
|
negativeLessThanPositive || positiveCase || negativeCase)); |
311 |
|
} |
312 |
|
|
313 |
|
} |
314 |
|
|
315 |
|
#endif |