Re: [Haskell-cafe] Haskell SBV Package with Z3

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

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/preco...

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. 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe