To add to what Tikhon mentioned; most SMT solvers deploy a number of heuristics in the theories they support, and a slight modification of the problem ("benchmark" in SMTLib terminology) can exhibit itself as a performance degradation. I don't think it's possible to generalize and say that bit-vectors are faster than unbounded integers. It is entirely problem specific, and whatever optimizations/tricks might be available in the underlying solver; which will also depend of the version of the solver you have, options, the random seed they use, etc. One thing is for sure though: SMT solvers have improved significantly in the last decade, and they'll only get better in time. It's quite an active research area with many very highly-skilled people working on them. Re: Rebindable syntax: I'm not a big fan of it; but patches are always welcome! SBV is hosted on github, so it should be easy to branch if anybody is interested in exploring: http://github.com/LeventErkok/sbv -Levent. On Sun, Feb 16, 2014 at 6:33 PM, Tikhon Jelvis wrote:

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 wrote:

...

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