Re: [Haskell-cafe] Haskell SBV Package with Z3
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 > 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 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." 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 >> >>> 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. 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 $
[Haskell-cafe] Optimizing Fold Expressions
Dear all, I was wondering whether it was possible to write fold expressions more elegantly. Suppose I have the following datastructure: data Expr = Add Expr Expr | Sub Expr Expr | Mul Expr Expr | Eq Expr Expr | B Bool | I Int deriving Show type ExprAlgebra r = (r -> r -> r, -- Add r -> r -> r, -- Sub r -> r -> r, -- Mul r -> r -> r, -- Eq Bool -> r, -- Bool Int -> r -- Int ) foldAlgebra :: ExprAlgebra r -> Expr -> r foldAlgebra alg@(a, b, c ,d, e, f) (Add x y) = a (foldAlgebra alg x) (foldAlgebra alg y) foldAlgebra alg@(a, b, c ,d, e, f) (Sub x y) = b (foldAlgebra alg x) (foldAlgebra alg y) foldAlgebra alg@(a, b, c ,d, e, f) (Mul x y) = c (foldAlgebra alg x) (foldAlgebra alg y) foldAlgebra alg@(a, b, c ,d, e, f) (Eq x y) = d (foldAlgebra alg x) (foldAlgebra alg y) foldAlgebra alg@(a, b, c ,d, e, f) (B b')= e b' foldAlgebra alg@(a, b, c ,d, e, f) (I i) = f i If I am correct, this works, however if we for example would like to replace all Int's by booleans (note: this is to illustrate my problem): replaceIntByBool = foldAlgebra (Add, Sub, Mul, Eq, B, \x -> if x == 0 then B False else B True) As you can see, a lot of "useless" identity code. Can I somehow optimize this? Can someone give me some pointers how I can write this more clearly (or with less code?) So I constantly don't have to write Add, Sub, Mul, for those things that I just want an "identity function"? Thanks in advance! Jun Jie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell SBV Package with Z3
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 > 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. 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
[Haskell-cafe] Haskell SBV Package with Z3
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
