[isabelle-dev] Status of HOL/SMT
Makarius
makarius at sketis.net
Tue Dec 4 14:19:16 CET 2012
Dear all,
since SMT and Z3 has been mentioned several times recently, I was curious
to see how it works at the moment -- also in preparation of the release.
This immediately lead to a problem with the external cache-access not
being thread-safe. It is addressed in Isabelle/4d1590544b91.
Then running some examples with the current z3-4.0 version produced a lot
of errors, see the included change for SMT_Examples.thy and the resulting
errors. It works with z3-3.2 from Isabelle2012.
So what is the status of HOL/SMT? Is it maintained, and who feels
responsible for it? This fine work by Sascha Boehme deserves to be kept
in shape.
What is also strange is that there seems to be no isatest/mira run that
actually invokes Z3 again on these example theories.
Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1354613695 -3600
# Node ID ee8b83e9b571d286e38d4d527e309da589df04fa
# Parent 4b6dc5077e98868379aafcbc8db45567fe105f75
test;
diff -r 4b6dc5077e98 -r ee8b83e9b571 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Mon Dec 03 18:19:12 2012 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Tue Dec 04 10:34:55 2012 +0100
@@ -9,8 +9,6 @@
begin
declare [[smt_oracle = false]]
-declare [[smt_certificates = "SMT_Examples.certs"]]
-declare [[smt_read_only_certificates = true]]
-------------- next part --------------
Loading theory "SMT_Examples"
*** exception CTERM ("apply: types don't agree", ["op =", "(if 0 <= x + y then x + y else -1 * x + -1 * y) + (-1 * (if 0 <= x then x else -1 * x) + -1 * (if 0 <= y then y else -1 * y))"]) raised (line 271 of "thm.ML")
*** At command "by" (line 272 of "~~/src/HOL/SMT_Examples/SMT_Examples.thy")
*** Z3 found a proof, but proof reconstruction failed at the following subgoal:
*** assumptions:
*** ~ x <= 3 / 2
*** 0 <= a
*** ~ 4 <= 3 * x + 7 * a
*** proposition: False
*** Adding a rule to the lemma group "z3_rule" might solve this problem.
*** At command "by" (line 289 of "~~/src/HOL/SMT_Examples/SMT_Examples.thy")
*** exception Option raised (line 81 of "General/basics.ML")
*** At command "by" (line 301 of "~~/src/HOL/SMT_Examples/SMT_Examples.thy")
*** exception CTERM ("apply: types don't agree", ["op =", "x3 + (x5 + -1 * (if 0 <= x4 then x4 else -1 * x4))"]) raised (line 271 of "thm.ML")
*** At command "by" (line 323 of "~~/src/HOL/SMT_Examples/SMT_Examples.thy")
*** exception THM 1 raised (line 373 of "drule.ML"):
*** COMP
*** 0 +
*** (2 * b + (2 * e + (2 * (p * b) + 2 * (p * e))) +
*** (d + p * d +
*** (-1 * b +
*** (-1 * e + (-1 * d + (-1 * (p * d) + (-1 * (p * b) + -1 * (p * e)))))))) =
*** b + (e + (p * b + p * e))
*** 0 +
*** ((b + e) * (2 + 2 * p) + (d * (1 + p) + -1 * ((1 + p) * (b + (d + e))))) =
*** ?u
*** ==> 0 +
*** ((b + e) * (2 + 2 * p) +
*** (d * (1 + p) + -1 * ((1 + p) * (b + (d + e))))) ==
*** ?u
*** At command "by" (line 413 of "~~/src/HOL/SMT_Examples/SMT_Examples.thy")
*** Z3 found a proof, but proof reconstruction failed at the following subgoal:
*** assumptions:
*** x * y <= 0
*** ~ x <= 0
*** ~ y <= 0
*** proposition: False
*** Adding a rule to the lemma group "z3_rule" might solve this problem.
*** At command "by" (line 423 of "~~/src/HOL/SMT_Examples/SMT_Examples.thy")
More information about the isabelle-dev
mailing list