search

herbie-fp / herbie

Optimize floating-point expressions for accuracy
https://herbie.uwplse.org
Other
766 stars 32 forks source link

suggest ldexp() for x*2^y #328

Open berthubert opened 4 years ago

berthubert commented 4 years ago

Hi,

Thank you for Herbie, I think this will be very useful, if only to educate people that even double precision floating point is not magic!

In many contexts of Global Navigation Satellite Systems (GNSS), it is common to get parameters as integers which then need to be multiplied by 2^-47, for example. It turns out that IEEE 754 can do such multiplications natively on the exponent, and for this reason, POSIX provides a primitive called ldexp(x, y) where the result is x * 2^y, both for positive and negative y.

Using it enhances precision and speed, so it might be worthwhile to add it to Herbie.

pavpanchekha commented 4 years ago

Good suggestion. We don't have ldexp right now because it takes an integer argument—that doesn't work for complicated and uninteresting reasons—but we should be able to do it soon.