# Re: [isabelle] z3 on a mac

Hi David,

>  - The script on the webpage uses 'Wine Files/drive_c/Program
> Files/Microsoft Research/Z3/bin/z3.exe'.  On my machine z3 installs
> with the same path except Z3-2.19 instead of just Z3.

This is mentioned under step 3 at http://www4.in.tum.de/~boehmes/z3.html. I think Sascha is unwilling to hardcode and then have to maintain version numbers.

>  - I still needed to edit contrib/z3/etc/settings and uncomment
> Z3_NON_COMMERCIAL="yes" for it to work. I don't know if it is
> intentionally left uncommented in your tar file.

Yes, it's intentional; by uncommenting it out, you acknowledge that you are a noncommercial user. (Some of our users are commercial or semicommercial and hence not allowed to use the noncommercial version of Z3.)

> It took me some
> digging to initially find that option last week; perhaps  an explicit
> comment on the website would be helpful to others?

Not sure this is the right place. That web page is only for Mac users, whereas the problem you describe is platform-agnostic. Normally (i.e. with Isabelle2011 or better), if you neglect to set "Z3_NON_COMMERCIAL" to "yes", you will get an error when using the "smt" method or Sledgehammer:

The SMT solver Z3 is not activated. To activate it, set the environment variable Z3_NON_COMMERCIAL to "yes".

Didn't you get such a message?

> - When I started up wine today it asked to self-update. I said yes.
> /Applications/Wine.app/Contents/MacOS/startwine went away. Reinstalling
> wine from the dpkg fixed.

Strange. It also self-updated for me today, but the "startwine" file is still there.

> - The [[smt_trace]] option is really cool. I didn't know about that widget.

A similar effect can be achieved using Sledgehammer's "overlord" option (see "sledgehammer.pdf" for details). I find it more convenient to study SMT/ATP inputs and outputs in the comfort of my favorite editor than in Emacs's amazingly slow trace buffer.

> - z3 seems to be successfully invoked. The first time I ran it to prove:
>
> lemma reallysimple : "(a \<and> b)= (b \<and> a)"
> using [[smt_trace]]
> sledgehammer [provers=z3,verbose=true,debug=true]
>
> z3 didn't produce a solution. However, it has reliably since then.
> I'm not sure why, but it's worked reliably since then. I'm chalking it
> up to first time initialization tasks.

Weird. If you run into other oddities that you can reproduce or for which you at least have a trace, please let Sascha or me know.

Cheers,

Jasmin



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.