Email Gateway (Aug 18 2022 at 14:41): Email Gateway (Aug 18 2022 at 14:41):From: John Matthews <matthews@galois.com>
Hello,
I'm trying to use the new "smt" proof method in Isabelle2009-1. Here's
my theory header:
theory test
imports Main "~~/SMT/SMT"
begin
However, Isabelle reports the following error when trying to load the
SMT theory:
*** Theory loader: failed to load "SMT" (unresolved "Z3", "SMT_Base")
*** Theory loader: failed to load "Z3" (unresolved "SMT_Base")
*** Undeclared class: "len"
*** At command "definition" (line 67 of "/Applications/Isabelle/
Isabelle/src/HOL/SMT/SMT_Base.thy").
*** At command "theory".
Should I be loading SMT.thy some other way?
Thanks,
-john
smime.p7s
Email Gateway (Aug 18 2022 at 14:41):From: John Matthews <matthews@galois.com>
Actually, I'm trying to use this import statement:
imports Main "~~/src/HOL/SMT/SMT"
Thanks,
-john
smime.p7s
Email Gateway (Aug 18 2022 at 14:42):From: Sascha Boehme <boehmes@in.tum.de>
Hello John,
Thanks for reporting this bug; it will be fixed in newer versions of
Isabelle. As for Isabelle2009-1, there are two possible workarounds
(the first one is the recommended way):
1) Build the HOL-SMT image by (at the Isabelle2009-1 directory):
./build -m HOL-SMT HOL
and load this when using SMT instead of the default HOL image.
With this method, you may drop the path to the SMT theory; the
import line may thus read "imports SMT".
2) Manually modify the file "~~/src/HOL/SMT/SMT_Base.thy", i.e.,
change the line starting with "imports" into
imports Real "~~/src/HOL/Word/Word"
"~~/src/HOL/Decision_Procs/Dense_Linear_Order"
Note that in any case "Main" does not need to be imported, because it
is already contained in SMT.
Regards,
Sascha
John Matthews wrote:
Email Gateway (Aug 18 2022 at 14:42):From: John Matthews <matthews@galois.com>
Thanks Sascha. Since I'm working in HOLCF I tried your approach (2),
which worked fine.
Another question: Does the smt proof method support uninterpreted
functions? I tried to prove the following three lemmas using smt, but
only the first one succeeded:
lemma "(x::int) = y+1 --> abs (x - 1) = abs y"
by smt
consts f :: "int => int"
lemma "(x::int) = y+1 --> f (x - 1) = f y"
oops
lemma "(x::int) = y+1 --> g (x - 1) = g y"
oops
Thanks,
-john
smime.p7s
Email Gateway (Aug 18 2022 at 14:42):From: Sascha Boehme <boehmes@in.tum.de>
Hello John,
Uninterpreted functions are supported by the smt method. In your case,
there are two ways to prove the lemma:
1) Use a different SMT solver, i.e.,
lemma "(x::int) = y+1 --> f (x - 1) = f y"
using [[smt_solver=cvc3]]
by smt
2) Apply some magic. In this case, tweak the default SMT solver Z3 as
follows:
lemma "(x::int) = y+1 --> f (x - 1) = f y"
using [[z3_options="AUTO_CONFIG=false"]]
by smt
Both ways also work for your third example.
Thanks for bringing up this issue. In newer versions of Isabelle,
providing this odd Z3 option will not be necessary anymore in such
situations.
Regards,
Sascha
John Matthews wrote:
Last updated: Apr 18 2024 at 08:19 UTC