[isabelle-dev] Status of HOL/SMT

[Jasmin Christian Blanchette]

Hi Makarius,

Sascha and I are responsible for SMT. Sascha still occasionally works on it, but I bear the ultimate responsibility for it now.

> 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.

Yes, I have been aware of these issues since early November (cf. 3b7ad6153322). I had moved to Z3 4.0 because the success rate in Sledgehammer was slightly higher than for 3.2, but in the light of replayability of old proofs / regeneration of existing certificates, we should include 3.2 with the next release, not 4.0. I'll update the components accordingly in a moment.

The real issue, at the end of the day, seems to be not so much Z3 4.0 in itself but rather the fact that our code often can't parse them. I've looked into this and saw no quick fix [*].

> What is also strange is that there seems to be no isatest/mira run that actually invokes Z3 again on these example theories.

... nor can there be, with the way in which the certification is hard-coded in them. I don't have a quick solutions for this; problems that Sascha hasn't addressed in four years aren't going to vanish automagically by my putting one lost hour here and there.

Because of a toxic combination of paper deadlines and teaching-related tasks, chances are very low that any of this will change before the next release (unless somebody else jumps in), but I hope to have more time to focus on Sledgehammer again next year -- and SMT is now a critical component of not only of Isabelle but also of Sledgehammer.

Jasmin

[*] In short, the proof seems to be referring to actual model elements, using some strange syntax. These are not parsed correctly and I have no clue how they should be handled. I was hoping to bring this up once Sascha's done with other problems I've reported to him (in the monomorphizer).