[isabelle-dev] smt2

[Jasmin Christian Blanchette]

Hi all,

> So far the development has taken place in a private repository. I will move it to Isabelle next week (in "src/HOL/Tools/SMT2", in session "HOL-SMT2"). To be able to connect it with Sledgehammer's Isar proof generator, the best would be to make it part of the "HOL" session, but that's for a bit later.

Actually, I did the transition in one go, directly to the "HOL" session, to avoid moving files around needlessly (which makes Mercurial logs harder to read). So I'm sorry if Makarius's recent optimizations and drop in "HOL" processing time is now eaten by "SMT2". Rest assured that I will move the old "SMT" out of "HOL" and to "Library" immediately after the Isabelle2014 release (planned for this summer), before we phase it out completely after the presumptive Isabelle2015 release.

There's also a new "z3-4.3.0" component that's used by new new module. When you write "by smt2", you get Z3 4.3.0, whereas "by smt" gives you the old 3.2. For Sledgehammer, you can invoke the new Z3 by passing "z3_new" as the prover. And it supports Isar proof construction, albeit in a somewhat rudimentary fashion (even more so than for E, SPASS, Vampire). I hope to enable "z3_new" by default with Sledgehammer before the next release.

Jasmin