[Haskell-cafe] Haskell SBV Package with Z3

[J. J. W.]

Dear L. Erkok,

First I would like to wish you happy easter and I would like to thank you
for your help.

I have a couple of more questions. I am now playing with SBV package,
however I am not sure if I understand the use of arrays, maybe you can give
me some pointers. For example I want to prove the following (note: this
example is only used to illustrate my question, I thought I've read
somewhere in Haddock that this method only support functions with 7
parameters?)

prove $ \(a :: SWord8) b c -> a .> b &&& b .> c ==> a .> c
Q.E.D.

how should I express this using SymArray?

Thanks in advance!

Yours sincerely,

Jun Jie


2013/3/29 Levent Erkok <erkokl at gmail.com>

> 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/20130331/428ae132/attachment.htm>