Email Gateway (Aug 18 2022 at 17:53): Email Gateway (Aug 18 2022 at 17:53):From: David Brumley <dbrumley@cmu.edu>
Hi,
I saw the discussion the other day about z3 on a mac. Coincidentally I
was setting up z3 on my mac too (10.6.8 on a 2008 mac pro)
I followed the recipe for z3 under wine. z3 seems to run fine from
the command line. I added the following to etc/settings (is there a
better place?):
Z3_COMPONENT="$COMPONENT"
Z3_HOME="$Z3_COMPONENT/$ISABELLE_PLATFORM"
Z3_NON_COMMERCIAL="yes"
Z3_SOLVER="$Z3_HOME/z3"
Z3_REMOTE_SOLVER="z3"
if [ -e "$Z3_HOME" ]
then
Z3_INSTALLED="yes"
fi
And put the z3 shell script from
http://www4.in.tum.de/~boehmes/z3.html under contrib/x86-darwin/z3.
z3 runs fine from the command line (at least z3 /h seems to work).
However, when I run it from isabelle I get
SMT outcome: Solver terminated abnormally with error code 109
The simplest example I've tried is:
lemma really_simple : "(a \and b) = (b \and a)"
sledgehammer [provers=z3,verbose=true,debug=true]
Complex lemmas have the same error.
Anyone run into this? I looked at the z3 documentation, but couldn't
find an error 109 on the list.
Thanks,
David
Email Gateway (Aug 18 2022 at 18:00):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi David,
I was able to get an error 109 on the Mac as well, even after following Sascha's online instructions. To investigate this, try adding
declare [[smt_trace]]
at the beginning of the .thy file, and send us the trace output.
SMT: Solver:
/Users/blanchet/isabelle/contrib/z3-2.15/x86-darwin/z3: line 11: winepath: command not found
fixme:heap:HeapSetInformation 0x0 1 0x0 0
Error: input file was not specified.
For usage information: z3 /h
If this is also your problem (and it probably is), either (1) make sure "/Applications/Wine.app/Contents/Resources/bin" is in your "PATH" before you launch Proof General or jEdit, or (2) update your "z3" script with the very latest version from Sascha's web page:
http://www4.in.tum.de/~boehmes/z3/mac/z3
I hope this helps. Please let us know if it doesn't, so we can iron out these issues once and for all.
Cheers,
Jasmin
Email Gateway (Aug 18 2022 at 18:00):From: David Brumley <dbrumley@cmu.edu>
Hello,
Thanks for all the help. The Isabelle community is amazing. The
updates worked with two small tweaks.
- 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.
- 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. It took me some
digging to initially find that option last week; perhaps an explicit
comment on the website would be helpful to others?
A couple of bizarre things happened when trying to get it to work
today. I note these in case someone else experiences them.
When I started up wine today it asked to self-update. I said yes.
/Applications/Wine.appContents/MacOS/startwine went away. Reinstalling
wine from the dpkg fixed. .
The [[smt_trace]] option is really cool. I didn't know about that widget.
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.
Take care,
-David
Email Gateway (Aug 18 2022 at 18:00):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
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
Email Gateway (Aug 18 2022 at 18:04):From: Sascha Boehme <boehmes@in.tum.de>
Hi David,
I just updated the description of how to run Z3 on a Mac:
http://www4.in.tum.de/~boehmes/z3.html
Especially, I added a section about how to run Z3 with Isabelle.
Please replace your setup (modification of etc/settings) with what is
described in section 4 of that webpage.
Cheers,
Sascha
David Brumley wrote:
Email Gateway (Aug 18 2022 at 18:08):From: David Brumley <dbrumley@cmu.edu>
Hi,
Sorry for the delay; I was traveling.
I did not get this error message anywhere obvious. I'm an isabelle
noob, so perhaps it was somewhere I wasn't looking? I just got an
error related to Z3 remote, but not an indication what to change.
Thanks again for your help.
Take care,
David
Email Gateway (Aug 18 2022 at 18:08):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi David,
Indeed -- I can reproduce this. Isabelle2011 was released at a point where the Sledgehammer/SMT business was a bit flaky, unfortunately. More precisely, some changes were done to the integration of off-the-shelf solvers in January, and Sledgehammer was not tested against these. With the repository version of Isabelle (or the next release), you would get the aforementioned message.
Regards,
Jasmin
Last updated: Apr 19 2024 at 01:05 UTC