[Haskell-cafe] Haskell SBV Package with Z3

[Levent Erkok]

Sorry, there were a couple of typos in the last example. It should read:

              allSat $ \(x::SWord8) -> x `shiftL` 2 ./= x

Note that this will return all 255 values that satisfy this property; i.e.,
everything except 0. (Here, we're using "sat/allSat" as opposed to "prove,"
 and hence the inversion of equality in the property.)

-Levent.


On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok <erkokl at gmail.com> wrote:

> You're welcome Jun Jie.
>
> Regarding getting a different counter example: That's perfectly normal.
> When SMT solvers build models they use random seeds. Furthermore, different
> versions of the same solver can use different algorithms/heuristics to
> arrive at the falsifying model. So, it's entirely expected that you get a
> different counter-example. You can turn the question around, and ask the
> solver to give you all counter-examples like this:
>
>          allSat $ \x -> \(x::SWord8) -> x `shiftL` 2 .!= x
>
> -Levent.
>
> On Mar 29, 2013, at 1:42 AM, "J. J. W." <bsc.j.j.w at gmail.com> wrote:
>
> Dear Levent,
>
> Thank you for your support. I am very honoured to have the developer of
> the SBV package to solve my elementary problem. I noticed that the
> counter-example given by my Z3 differs from the one said on HackageDB:
> sbv-2.10.
>
> Code that is on Hackage:
>
>  Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .==
> x
>    Falsifiable. Counter-example:
>      x = 128 :: SWord8
>
> My current GHCi output:
>
> Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x
> Falsifiable. Counter-example:
>   x = 51 :: SWord8
> (0.02 secs, 1196468 bytes)
>
> Thank you for your help!
>
> Yours sincerely,
>
> Jun Jie
>
>
> 2013/3/29 Levent Erkok <erkokl at gmail.com>
>
>> Hi Jun Jie:
>>
>> SBV uses some of the not-yet-officially-released features in Z3. The
>> version you have, while it's the latest official Z3 release, will not work.
>>
>> To resolve, you need to install the "development" version of Z3
>> (something that is at least 4.3.2 or better). Here're instructions from the
>> Microsoft folks explaining how to get these builds:
>> http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html
>>
>> Let me know if you find any issues after you get the latest-development
>> version of Z3 installed.
>>
>> -Levent.
>>
>>
>> On Thu, Mar 28, 2013 at 10:22 PM, J. J. W. <bsc.j.j.w at gmail.com> wrote:
>>
>>>  Dear all,
>>>
>>> I have a small question regarding the installation of the SBV package. I
>>> first installed the SBV 2.10 package with cabal with the following
>>> instructions:
>>>
>>> cabal install sbv
>>>
>>> Next I installed the Z3 theorem prover and adding the path to my system
>>> variables (Windows 7 x64). Next I tested whether I could find it by opening
>>> cmd.exe and then typing z3, I get an error message of Z3, so I can safely
>>> assume the system can find it. (I added the path to the bin of Z3, I have
>>> not included the include directory, I see no reason why I should add a path
>>> to this directory, but maybe I am wrong).
>>>
>>> I ran the program: SBVUnitTests. However it had some errors in the
>>> beginning and afterwards a few failures. Having no idea how to fix this, I
>>> continued to check whether I can get the SBV to work. So I started to
>>> execute the SBV package:
>>>
>>> ghci -XScopedTypeVariables
>>> ghci> :m Data.SBV
>>> ghci> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
>>>
>>> Now this should return Q.E.D., however it returned the following:
>>>
>>> An error occured.
>>> Failed to complete the call to z3
>>> Executable: "C:\\Program Files\\z3-4.3.0-x64\\bin\\z3.exe
>>> Options: /in /smt2
>>> Exit code: 0
>>> Solver output:
>>> ===========================================================
>>> ; :smt.mbqi
>>> ; :pp.decimal_precision
>>> ===========================================================
>>>
>>> Giving up..
>>>
>>> It does seems like that the Z3 has a normal output, however not a
>>> result. Can someone help me to figure out what I actually did wrong?
>>>
>>> I am using Z3 version 4.3.0, SBV 2.10 and GHCi 7.4.2
>>>
>>> Thank you for your help!
>>>
>>> Yours sincerely,
>>>
>>> Jun Jie
>>>
>>>
>>> _______________________________________________
>>> 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/20130329/bc6530e0/attachment.htm>