It's a difference in the Z3 theorem prover rather than the library.
SInteger maps to the theory of integers while SWord32 maps to theory of
bitvectors. The two are implemented completely differently.
Of course, this just punts the question to why Z3 can be faster for
Integers than for BitVectors. BitVectors are just fixed-length patterns of
bits--32 bits in this case. Integers, on the other hand, cannot be reasoned
about as bits because Z3 has to prove things about *all* integers in the
mathematical sense. I *think* the difference comes up because the theory of
bitvectors is optimized for exhaustively searching over all possible bit
patterns given a wide range of constraints while integers, by their very
nature, have to be dealt with symbolically.
In fact, working with bitvectors is pretty much the same as doing normal
SAT solving. I don't know about Z3 in particular, but this is actually how
some solvers implement bitvectors: they just compile the bitvector
constraints to normal SAT constraints (called "bit blasting").
For simpler queries, symbolically working with integers can prove faster,
but for complex ones it might just not return an answer at all. (In SBV, it
would just return `Unknown'.) Since the domain of bitvectors of a given
size is finite we can, in principle, check everything which means that any
set of constraints is solvable although it might take a really long time.
Also, the solver uses different strategies for the same types depending on
the actual constraints you have. I've noticed slow-downs in a very similar
vein just using SInteger. I had a problem that would quickly return
`Unknown' with unbounded integers; when I added some bounds (ie x .> 0 &&&
x .< 10000000000) the process started eating up a lot more CPU and not
returning in a reasonable time-frame.
I should add that while I've worked *with* a few SMT solvers, I still only
have a vague idea of how they are implemented. If you really want to
understand what's going on, you'll have to ask somebody knowledgeable or
just read their publications :).
On Sun, Feb 16, 2014 at 6:04 PM, Niklas Hambüchen
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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe