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 <erk...@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....@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@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> >> >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe