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/preco...

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

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/preco...

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

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

...

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/preco...

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