src/HOL/Tools/Nitpick/nitpick_kodkod.ML
2011-03-15 ago support non-ground "need" values
2011-03-03 ago renamed "preconstr" option "need"
2011-02-21 ago more work on "fix_datatype_vals" optimization (renamed "preconstruct")
2011-02-21 ago more work on "fix_datatype_vals"
2011-02-21 ago first steps in implementing "fix_datatype_vals" optimization
2010-12-07 ago removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
2010-12-07 ago simplified special handling of set products
2010-12-07 ago use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
2010-10-01 ago tuning
2010-09-16 ago tuning
2010-09-14 ago eliminate more clutter related to "fast_descrs" optimization
2010-09-14 ago fixed bug in the "fast_descrs" optimization;
2010-09-13 ago remove unreferenced identifiers
2010-09-11 ago change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
2010-08-06 ago improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
2010-08-05 ago remove buggy and needless condition
2010-08-05 ago renamed internal function
2010-08-04 ago Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
2010-08-04 ago avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
2010-08-04 ago improve datatype symmetry breaking;
2010-08-04 ago make SML/NJ happy
2010-08-04 ago get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-08-03 ago more helpful message
2010-08-02 ago optimize generated Kodkod formula
2010-08-01 ago fix minor bug in sym breaking
2010-08-01 ago tweak datatype sym break code
2010-08-01 ago added manual symmetry breaking for datatypes
2010-07-31 ago started implementation of custom sym break
2010-07-30 ago gracefully handle the case where no integers occur in the formula and the "max" option is used
2010-06-21 ago optimized code generated for datatype cases + more;
2010-04-24 ago remove type annotations as comments;
2010-04-13 ago fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
2010-03-10 ago fixed soundness bug in Nitpick
2010-03-09 ago improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
2010-03-09 ago added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-02-27 ago use existing Typ_Graph;
2010-02-26 ago more work on the new monotonicity stuff in Nitpick
2010-02-25 ago improved precision of infinite "shallow" datatypes in Nitpick;
2010-02-23 ago improved precision of small sets in Nitpick
2010-02-22 ago fixed a few bugs in Nitpick and removed unreferenced variables
2010-02-18 ago added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
2010-02-17 ago make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
2010-02-17 ago added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
2010-02-13 ago redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
2010-02-12 ago minor fixes to Nitpick
2010-02-12 ago various cosmetic changes to Nitpick
2010-02-09 ago optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
2010-02-05 ago optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
2010-02-04 ago split "nitpick_hol.ML" into two files to make it more manageable;
2010-02-02 ago added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-01-20 ago some work on Nitpick's support for quotient types;
2010-01-07 ago reduced arity of Nitpick selectors associated with sets by 1, by using "Formula" instead of "Atom 2"
2009-12-18 ago polished Nitpick's binary integer support etc.;
2009-12-17 ago added support for binary nat/int representation to Nitpick
2009-12-14 ago get rid of polymorphic equality in Nitpick's code + a few minor cleanups
2009-12-04 ago fixed paths in Nitpick's ML file headers
2009-11-24 ago fixed arity of some empty relations in Nitpick's Kodkod generator;
2009-11-24 ago fix soundness bug in Nitpick's Kodkod generator for the relational composition case
2009-11-23 ago generate arguments of relational composition in the right order in Nitpick
2009-11-23 ago fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user