src/HOL/Tools/Quickcheck/exhaustive_generators.ML
Tue, 17 Jul 2012 10:39:39 +0200 bulwahn improved equality optimisation in Quickcheck
Mon, 02 Jul 2012 11:45:19 +0200 bulwahn exporting important function for the "many conjecture refutation" compilation of quickcheck
Tue, 29 May 2012 13:46:50 +0200 bulwahn added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
Tue, 21 Feb 2012 12:20:33 +0100 bulwahn subtype preprocessing in Quickcheck;
Wed, 25 Jan 2012 15:19:04 +0100 bulwahn generalizing check if size matters because it is different for random and exhaustive testing
Fri, 20 Jan 2012 09:28:51 +0100 bulwahn tuned
Thu, 29 Dec 2011 15:54:37 +0100 wenzelm comments;
Tue, 20 Dec 2011 17:22:31 +0100 bulwahn exporting instantiation functions in quickcheck for their usage in abstract generators
Tue, 20 Dec 2011 17:22:31 +0100 bulwahn generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
Mon, 05 Dec 2011 12:36:20 +0100 bulwahn random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
Mon, 05 Dec 2011 12:36:06 +0100 bulwahn exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
Mon, 05 Dec 2011 12:35:05 +0100 bulwahn dynamic genuine_flag in compilation of random and exhaustive
Mon, 05 Dec 2011 12:35:04 +0100 bulwahn indicating where the restart should occur; making safe_if dynamic
Thu, 01 Dec 2011 22:16:23 +0100 bulwahn removing catch_match' now that catch_match is polymorphic
Thu, 01 Dec 2011 22:14:35 +0100 bulwahn compilations return genuine flag to quickcheck framework
Thu, 01 Dec 2011 22:14:35 +0100 bulwahn the simple exhaustive compilation also indicates if counterexample is potentially spurious;
Thu, 01 Dec 2011 22:14:35 +0100 bulwahn changing the exhaustive generator signatures;
Thu, 01 Dec 2011 22:14:35 +0100 bulwahn quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
Thu, 01 Dec 2011 22:14:35 +0100 bulwahn quickcheck random can also find potential counterexamples;
Wed, 30 Nov 2011 09:35:58 +0100 bulwahn also potential counterexamples in the simple exhaustive testing in quickcheck
Wed, 30 Nov 2011 09:21:09 +0100 bulwahn adding a exception-safe term reification step in quickcheck; adding examples
Wed, 30 Nov 2011 09:21:07 +0100 bulwahn quickcheck returns counterexamples that are potentially spurious due to underspecified code equations and match exceptions
Mon, 14 Nov 2011 11:14:06 +0100 bulwahn setting up exhaustive generators which are used for the smart generators
Wed, 09 Nov 2011 11:35:09 +0100 bulwahn more precise messages with the tester's name in quickcheck; tuned
Mon, 17 Oct 2011 10:19:01 +0200 bulwahn moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn removing generator registration
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn parametrized test_term functions in quickcheck
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn adding random, exhaustive and SML quickcheck as testers
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Mon, 18 Apr 2011 09:10:23 +0200 bulwahn adding bounded_forall tester
Mon, 18 Apr 2011 09:10:23 +0200 bulwahn creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 09 Apr 2011 15:00:23 +0200 wenzelm made SML/NJ happy;
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn correcting constant name in exhaustive_generators
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn switching fast compilation off by default for now in exhaustive quickcheck
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn ensuring datatype limitations before the instantiation in quickcheck_exhaustive
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn splitting exhaustive and full_exhaustive into separate type classes
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn removing duplicate code
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn revisiting mk_equation functions and refactoring them in exhaustive quickcheck
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn creating a general mk_equation_terms for the different compilations
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn adding an even faster compilation scheme
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn new compilation for exhaustive quickcheck
Thu, 07 Apr 2011 14:51:25 +0200 bulwahn correcting bounded_forall construction; tuned
Tue, 05 Apr 2011 09:38:23 +0200 bulwahn deriving bounded_forall instances in quickcheck_exhaustive
Tue, 05 Apr 2011 08:53:52 +0200 bulwahn generalizing ensure_sort_datatype for bounded_forall instances
Mon, 04 Apr 2011 14:44:11 +0200 bulwahn refactoring generator definition in quickcheck and removing clone
Fri, 01 Apr 2011 13:49:38 +0200 bulwahn adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
Wed, 30 Mar 2011 19:09:57 +0200 bulwahn removing dead code in exhaustive_generators
Wed, 30 Mar 2011 09:44:16 +0200 bulwahn generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn extending the test data generators to take the evaluation terms as arguments
Mon, 14 Mar 2011 12:34:12 +0100 bulwahn tuned exhaustive_generators
Mon, 14 Mar 2011 12:34:10 +0100 bulwahn tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn adaptions in generators using the common functions
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn renaming signatures and structures; correcting header
less more (0) tip