Am 15/02/2013 14:21, schrieb Jasmin Christian Blanchette: > Am 15.02.2013 um 13:37 schrieb Tobias Nipkow <[email protected]>: > >> 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.
Sure, something like that may well be s/h-very-light. Tobias > 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 > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
