John Regehrfun superoptimizer result from @hyperoptimizer, this occurs in ImageMagick
I Can't Believe It's Not Zero!... hold up. This is checking |a - b| < 0.0, which is always false. Is there a typo or a bug in the checker, or did I misread something?
@steve @hyperoptimizer I don't think typo-- I'm cutting and pasting.
but we've seen Alive2 and Z3 bugs wrt FP....
Alexander Monakov@regehr @steve @hyperoptimizer but the godbolt link has
%cmp = fcmp olt double %ext, 1.000000e-15
which is reasonable, so 0.0000 shown in the screenshot is the result of printing with %f?
@amonakov @steve @hyperoptimizer ah.... the screenshot is Alive2's output, which may not be sufficiently careful about floats.
indeed the godbolt link is the correct code
void friend@regehr with C-style formatters, IIRC, either of %.16e or %.17g will print differently two doubles that are different, whereas obviously %f does not.
(assuming a modicum of quality of the libc doing the printing)
@void_friend yeah I'll patch Alive2 for this thanks
@void_friend @regehr these days I would try to use zmij (https://github.com/vitaut/zmij/) or similar for a self-contained portable very fast option that prints exactly as many digits as necessary to differentiate doubles, and not depend on libc.
@steve @void_friend not sure I can get Nuno to buy into a new dependency, hoping I can do this with just LLVM's APFloat utils
@regehr @void_friend APFloat should probably have a toShortestString with no parameters, then you wouldn't need it (obviously, this is a larger project, though).
But note that zmij and swiftDtoa and a few of the others are basically zero-dependency single-file implementations, so you can just copy them and not introduce any new dependencies for your project.
@steve @void_friend nice thanks, I've not used any of those yet
@regehr If you are willing to accept base-2 exponents being printed instead of base-10 (the significand can be in base 10, e.g. 1.57p2 for π), you can make a function sufficient for regression tests with a call to frexp, a multiplication and a conversion to uint64_t. Always prints differently doubles that are different and the n-1 first digits are even correct!
If you want base-10 exponents, it's better to add a dependency than to try to reinvent it. Either you'll have to reinvent multiprecision integers or to reinvent extremely sophisticated shortcuts invented along the decades by extremely bright people. It is really difficult and the algorithms known today have refined the job of doing this conversion efficiently to a tour de force.
@void_friend it looks like LLVM's APFloat library has everything I might want here, except not printing the shortest lossless string. but I don't know that we care specifically about that.
Joe Groff (1M Context)