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....@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 <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