[Haskell-cafe] [Announcement] New release of SBV: SMT Based Verification, v3.0

[Levent Erkok]

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 <tikhon at jelv.is> 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 <mail at nh2.me> 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-Floating.html
>> >
>> > Happy theorem proving!
>> >
>> > -Levent.
>> >
>> >
>> > _______________________________________________
>> > Haskell-Cafe mailing list
>> > Haskell-Cafe at haskell.org
>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140216/09f87327/attachment.html>