src/HOL/Tools/Nitpick/nitpick_kodkod.ML
Fri, 18 Mar 2011 12:05:23 +0100 blanchet more optimizations of bounds for "need"
Fri, 18 Mar 2011 11:43:28 +0100 blanchet optimize Kodkod bounds when "need" is specified
Tue, 15 Mar 2011 15:49:42 +0100 blanchet support non-ground "need" values
Thu, 03 Mar 2011 11:20:48 +0100 blanchet renamed "preconstr" option "need"
Mon, 21 Feb 2011 17:36:32 +0100 blanchet more work on "fix_datatype_vals" optimization (renamed "preconstruct")
Mon, 21 Feb 2011 16:33:21 +0100 blanchet more work on "fix_datatype_vals"
Mon, 21 Feb 2011 15:45:44 +0100 blanchet first steps in implementing "fix_datatype_vals" optimization
Tue, 07 Dec 2010 11:56:01 +0100 blanchet removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
Tue, 07 Dec 2010 11:56:01 +0100 blanchet simplified special handling of set products
Tue, 07 Dec 2010 11:56:01 +0100 blanchet use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
Fri, 01 Oct 2010 10:58:01 +0200 blanchet tuning
Thu, 16 Sep 2010 14:24:03 +0200 blanchet tuning
Tue, 14 Sep 2010 13:44:43 +0200 blanchet eliminate more clutter related to "fast_descrs" optimization
Tue, 14 Sep 2010 12:52:50 +0200 blanchet fixed bug in the "fast_descrs" optimization;
Mon, 13 Sep 2010 20:21:40 +0200 blanchet remove unreferenced identifiers
Sat, 11 Sep 2010 10:20:25 +0200 blanchet change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
Fri, 06 Aug 2010 10:50:52 +0200 blanchet improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
Thu, 05 Aug 2010 01:12:12 +0200 blanchet remove buggy and needless condition
Thu, 05 Aug 2010 00:21:11 +0200 blanchet renamed internal function
Wed, 04 Aug 2010 23:27:27 +0200 blanchet Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
Wed, 04 Aug 2010 22:47:52 +0200 blanchet avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
Wed, 04 Aug 2010 21:56:17 +0200 blanchet improve datatype symmetry breaking;
Wed, 04 Aug 2010 10:51:04 +0200 blanchet make SML/NJ happy
Wed, 04 Aug 2010 10:39:35 +0200 blanchet get rid of all "optimizations" regarding "unit" and other cardinality-1 types
Tue, 03 Aug 2010 15:15:17 +0200 blanchet more helpful message
Mon, 02 Aug 2010 15:52:32 +0200 blanchet optimize generated Kodkod formula
Sun, 01 Aug 2010 23:15:26 +0200 blanchet fix minor bug in sym breaking
Sun, 01 Aug 2010 16:35:25 +0200 blanchet tweak datatype sym break code
Sun, 01 Aug 2010 15:51:25 +0200 blanchet added manual symmetry breaking for datatypes
Sat, 31 Jul 2010 16:39:32 +0200 blanchet started implementation of custom sym break
less more (0) -50 -30 tip