[Haskell-cafe] Haskell SBV Package with Z3

[Levent Erkok]

Jun Jie: A SymArray is an abstraction of an array that can contain symbolic
values, as well as being indexed by a symbolic value. I'm not sure how the
example you picked relates. There's a sample program in the SBV
distribution that shows how to use SymArray's, maybe looking at that might
help:
http://hackage.haskell.org/packages/archive/sbv/2.10/doc/html/Data-SBV-Examples-Uninterpreted-AUF.html

Feel free to e-mail me privately for further questions on SBV; the mailing
list might not be quite appropriate for detailed discussions.

-Levent.


On Sun, Mar 31, 2013 at 7:12 AM, J. J. W. <bsc.j.j.w at gmail.com> wrote:

> 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/61aeedca/attachment-0001.htm>