<div dir="ltr"><div style>Dear L. Erkok,</div><div style><br></div><div style>First I would like to wish you happy easter and I would like to thank you for your help.</div><div style><br></div><div>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?)</div>
<div><br></div><div style>prove $ \(a :: SWord8) b c -> a .> b &&& b .> c ==> a .> c<br>Q.E.D.</div><div style><br></div><div style>how should I express this using SymArray? </div><div style><br>
</div><div style>Thanks in advance!</div><div style><br></div><div style>Yours sincerely,</div><div style><br></div><div style>Jun Jie</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">2013/3/29 Levent Erkok <span dir="ltr"><<a href="mailto:erkokl@gmail.com" target="_blank">erkokl@gmail.com</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Sorry, there were a couple of typos in the last example. It should read: <div><br></div><div> allSat $ \(x::SWord8) -> x `shiftL` 2 ./= x<br>
</div><div><br></div><div>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.)</div>
<span class="HOEnZb"><font color="#888888">
<div><br></div><div>-Levent.</div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok <span dir="ltr"><<a href="mailto:erkokl@gmail.com" target="_blank">erkokl@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><div>You're welcome Jun Jie. </div><div><br></div><div>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:</div>
<div><br></div><div> allSat $ \x -><span> \(x::SWord8) -> x `shiftL` 2 .!= x</span><span><font color="#888888"><br><br>-Levent. </font></span></div><div><div><div><br>On Mar 29, 2013, at 1:42 AM, "J. J. W." <<a href="mailto:bsc.j.j.w@gmail.com" target="_blank">bsc.j.j.w@gmail.com</a>> wrote:<br>
<br></div><blockquote type="cite"><div><div dir="ltr">Dear Levent,<div><br></div><div>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.</div>
<div><br></div><div>Code that is on Hackage:</div><div><br></div><div><div> Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x</div><div> Falsifiable. Counter-example:</div>
<div> x = 128 :: SWord8</div><div><br></div><div>My current GHCi output:</div><div><br></div><div><div>Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x</div><div>
Falsifiable. Counter-example:</div><div> x = 51 :: SWord8</div><div>(0.02 secs, 1196468 bytes)</div><div><br></div><div>Thank you for your help!</div><div><br></div><div>Yours sincerely,</div><div>
<br></div><div>Jun Jie</div></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">2013/3/29 Levent Erkok <span dir="ltr"><<a href="mailto:erkokl@gmail.com" target="_blank">erkokl@gmail.com</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi Jun Jie:<div><br></div><div>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.</div>
<div><br></div>
<div>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: <a href="http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html" target="_blank">http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html</a></div>
<div><br></div><div>Let me know if you find any issues after you get the latest-development version of Z3 installed.</div><div><br></div><div>-Levent. </div></div><div class="gmail_extra"><br><br>
<div class="gmail_quote"><div><div>On Thu, Mar 28, 2013 at 10:22 PM, J. J. W. <span dir="ltr"><<a href="mailto:bsc.j.j.w@gmail.com" target="_blank">bsc.j.j.w@gmail.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div><div>
<div dir="ltr">Dear all,<div><br></div><div>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:</div><div><br></div><div>
cabal install sbv</div><div><br></div><div>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).</div>
<div><br></div><div>I ran the program: <span style="color:rgb(51,51,51);font-family:Consolas,'Liberation Mono',Courier,monospace;font-size:12px;line-height:16px;white-space:pre-wrap">SBVUnitTests. </span>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:</div>
<div><br></div><div><div>ghci -XScopedTypeVariables</div><div>ghci> :m Data.SBV</div><div>ghci> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x</div><div><br></div><div>Now this should return Q.E.D., however it returned the following:</div>
<div><br></div><div>An error occured.</div><div>Failed to complete the call to z3</div><div>Executable: "C:\\Program Files\\z3-4.3.0-x64\\bin\\z3.exe</div><div>Options: /in /smt2</div><div>
Exit code: 0</div><div>Solver output:</div><div>===========================================================</div><div>; :smt.mbqi</div><div>; :pp.decimal_precision</div><div>===========================================================</div>
<div><br></div><div>Giving up..</div><div><br></div><div>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?</div>
<div><br></div><div>I am using Z3 version 4.3.0, SBV 2.10 and GHCi 7.4.2</div><div><br></div><div>Thank you for your help!</div><div><br></div><div>Yours sincerely,</div><div><br>
</div><div>Jun Jie</div><div><br></div></div></div>
<br></div></div>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>
</div></blockquote></div></div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>