Email Gateway (Aug 18 2022 at 17:13): Email Gateway (Aug 18 2022 at 17:13):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi all,
Isabelle2011's Sledgehammer invokes Z3 by default in addition to Vampire & Co., which is nice because it often finds proofs that are outside the ATPs' reach. Unfortunately, we just found that for some theories, the Z3 problem preparation last "forever" and uses a lot of CPU.
So if you notice that after calling Sledgehammer you get no report from "z3" or "remote_z3" and the "poly" process takes 100% CPU, you might be a victim of this problem. Workaround: Decrease the monomorphization limit by adding
declare [[smt_monomorph_limit = 2]]
or even "= 1" at the beginning of your theory (or in an included theory), or disable Z3 by adding
sledgehammer_params [provers = e spass remote_vampire remote_sine_e]
(or whatever values make sense to you). Invoking Sledgehammer in synchronous mode, using
sledgehammer [blocking]
or (to change the default)
sledgehammer_params [blocking]
should also do the trick.
I'm sorry for the trouble caused by this issue. Strangely enough, we never had any problems with the 1500 goals from nine theories we used for testing, including the largish Jinja.
If you work with the repository version, expect a fix in the coming days.
Cheers,
Jasmin
Last updated: Apr 20 2024 at 12:26 UTC