[Haskell-cafe] Haskell SBV Package with Z3

[J. J. W.]

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/6506b4a5/attachment-0001.htm>