[isabelle-dev] Status of HOL/SMT

[Makarius]

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")