Jun Jie: A SymArray is an abstraction of an array that can contain symbolic values, as well as being indexed by a symbolic value. I'm not sure how the example you picked relates. There's a sample program in the SBV distribution that shows how to use SymArray's, maybe looking at that might help: http://hackage.haskell.org/packages/archive/sbv/2.10/doc/html/Data-SBV-Examples-Uninterpreted-AUF.html
Feel free to e-mail me privately for further questions on SBV; the mailing list might not be quite appropriate for detailed discussions. -Levent. On Sun, Mar 31, 2013 at 7:12 AM, J. J. W. <bsc.j....@gmail.com> wrote: > 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
