Dear L. Erkok, First I would like to wish you happy easter and I would like to thank you for your help.
I have a couple of more questions. I am now playing with SBV package, however I am not sure if I understand the use of arrays, maybe you can give me some pointers. For example I want to prove the following (note: this example is only used to illustrate my question, I thought I've read somewhere in Haddock that this method only support functions with 7 parameters?) prove $ \(a :: SWord8) b c -> a .> b &&& b .> c ==> a .> c Q.E.D. how should I express this using SymArray? Thanks in advance! Yours sincerely, Jun Jie 2013/3/29 Levent Erkok <erk...@gmail.com> > 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
