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