Hi, this is pretty darn cool. Short technical question: Why functions on SInteger so much faster to check than functions on SWord32? Is it because they don't overflow? Also I think RebindableSyntax would be really useful for this. I have seen your counter arguments in https://github.com/LeventErkok/sbv/issues/79, but RebindableSyntax would make checking many functions really easy. I think your idea with making it a separate module is the right way, e.g. Data.SBV.RebindableSyntax. Niklas On 16/02/14 23:50, Levent Erkok wrote:
Home page: http://leventerkok.github.io/sbv/ ChangeLog: http://github.com/LeventErkok/sbv/blob/master/CHANGES.md
I'm happy to announce a new release of SBV, v3.0.
The most important addition is support for reasoning about IEEE-74 floating point numbers, i.e., programs using the Float and Double types. See the change-log for full details.
Reasoning with floating-point is a tricky task, and SMT solvers are slowly starting to provide support for true machine arithmetic as prescribed by the IEEE-754 standard. In particular, the semantics of NaN and Infinity are both properly captured, along with proper rounding. Also supported is fused-multiply-add, and square-root functions at the logic level.
Currently, only Z3 (the developer version release) has official support for this logic, and the implementation in SBV builds on top of Z3's implementation. It's likely that both Z3's and SBV might have some rough edges, so any bug reports are most welcome.
There's also a new example file demonstrating the floating-point arithmetic: Formally establishing that floating point addition is not associative (finding a concrete counter-example), multiplicative inverses do not necessarily exist, etc. See: http://hackage.haskell.org/package/sbv-3.0/docs/Data-SBV-Examples-Misc-Float...
Happy theorem proving!
-Levent.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe