Sorry, there were a couple of typos in the last example. It should read: allSat $ \(x::SWord8) -> x `shiftL` 2 ./= x
Note that this will return all 255 values that satisfy this property; i.e., everything except 0. (Here, we're using "sat/allSat" as opposed to "prove," and hence the inversion of equality in the property.) -Levent. On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok <erk...@gmail.com> wrote: > 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