suggest ldexp() for x*2^y

[berthubert]

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]

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.