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()
-
-
CVC4 agrees with you that it's correct for 32bits floats, but generates a counterexample for 64bits double: (fp
#b0#b01111111101#b1111111111111111111111111111111111111111111111111110) IIUC that's the predecessor of the predecessor of 0.5 and indeed I wrote a test and it fails. -
Wow, that's interesting and mysterious. I would have thought that f64 has the same rounding behavior as f32, just more precision, but I guess not. Worth looking into more deeply. Also yay SMT.
- 5 more replies
New conversation -
-
-
Here's how Java does it (with the caveat that Java has a few unique float semantics that may or may be reflected here). Definitely more complicated than (int)(x + 0.5f): http://hg.openjdk.java.net/jdk/jdk11/file/1ddf9a99e4ad/src/java.base/share/classes/java/lang/Math.java#l690 …
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.