Here's a fairly extreme nerd snipe: what does this do and why? Apologies to those who just can't wrap their head around it. ((x + 0.24999994) + 0.25000006).floor()
Ahhhh right, sure. That's what I would expect. It's not the exact constants, it's their relationship with epsilon. Whew.
-
-
beautiful floats! :-) and beautiful implementation of float support in CVC4 by Florian Schanda and
@ciphernyx, as Z3 does not seem to be able to prove these properties. -
Looking at the implementation of the float-to-integer conversion in GNAT (in Ada, this conversion does the same round-nearest-tie-to-away), it seems that simply adding the predecessor of 0.5 and then taking floor does the same. Slightly simpler. CVC4 also proves it for 32/64 bits
- 1 more reply
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.