[Haskell-cafe] Haskell SBV Package with Z3

[Levent Erkok]

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/20130328/80559f00/attachment.htm>