[isabelle-dev] [isabelle] the sound of a sledgehammer

[Jasmin Christian Blanchette]

Am 15.02.2013 um 13:37 schrieb Tobias Nipkow <nipkow at in.tum.de>:

> Triggering s/h via "sorry" (or some other explicit means) is perfectly
> reasonable, but having the IDE invoke s/h based on time outs and guesses should
> be avoided: the success rate is low and it consumes a lot of resources.
> 
> This is in contrast to auto-solve and quickcheck, both of which have a low
> overhead. Conceivably one could configure a s/h-very-light, which would be
> launched spontaneously.

With 2 s of 1 CPU, it's possible to do quite a bit with Sledgehammer already (with one prover -- probably the lightning-fast Z3). Of course, that's still at least one order of magnitude slower than Quickcheck or solve_direct.

Incidentally, most of the noncompressible overhead comes from picking up all the 10 000 or so facts from the context before filtering them, repeatedly for each Sledgehammer invocation. It's hard to do better there without using hacks or enriching the theories with Sledgehammer-specific data (think "Skolem cache"…).

Jasmin