[isabelle-dev] smt2

[Jasmin Blanchette]

Hi Andreas,

Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:

> On 14/03/14 14:18, Jasmin Blanchette wrote:
>> Another candidate is "Quickcheck_Narrowing.thy". Nothing in "HOL" seems to depend on it, and (please correct me if I'm mistaken) hardly anybody go into the trouble of setting up Quickcheck (and GHC) so that it uses the narrowing strategy.
> I guess I am the exception to the rule. I have GHC set up and sometimes try quickcheck[narrowing]. Sometimes, it does give better results than the random and exhaustive generators.

How big an issue is it to you if we move narrowing to Library? From what I understand, you already pull in quite a bit from Library, to the extent that "Coinductive" is based on the "HOL-Library" session. And Quickcheck has a nice generic interface for registering "testers" at any point, so technically the move should be nearly trivial.

Jasmin