doc-src/Nitpick/nitpick.tex
2010-02-17 blanchet 2010-02-17 added gotcha to Nitpick manual regarding nonstandard models of "nat"
2010-02-17 blanchet 2010-02-17 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
2010-02-17 blanchet 2010-02-17 reintroduce structural induction hint in Nitpick
2010-02-13 blanchet 2010-02-13 more work on Nitpick's support for nonstandard models + fix in model reconstruction
2010-02-12 blanchet 2010-02-12 minor fixes to Nitpick
2010-02-09 blanchet 2010-02-09 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
2010-02-05 blanchet 2010-02-05 optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil"; this gains one cardinality in the AA tree examples in the Nitpick manual
2010-02-04 blanchet 2010-02-04 four changes to Nitpick: 1. avoid writing absolute paths in Kodkodi files for input/output files of external SAT solvers (e.g. MiniSat), to dodge Cygwin problems 2. do eta-contraction in the monotonicity check 3. improved quantifier massaging algorithms using ideas from Paradox 4. repaired "check_potential" and "check_genuine"
2010-02-02 blanchet 2010-02-02 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2009-12-18 blanchet 2009-12-18 polished Nitpick's binary integer support etc.; etc. = improve inconsistent scope correction + sort values nicely in output + handle "mod" using the characterization "x mod y = x - x div y * y" (instead of explicit code in Nitpick) + introduce KK = Kodkod as abbreviation
2009-12-17 blanchet 2009-12-17 added support for binary nat/int representation to Nitpick
2009-12-07 blanchet 2009-12-07 make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
2009-11-24 blanchet 2009-11-24 remove version number from Nitpick manual
2009-11-16 blanchet 2009-11-16 change the order in which Nitpick tries SAT solvers; so that the binary JNIs come further down the list and can easily be overridden
2009-11-05 blanchet 2009-11-05 added possibility to register datatypes as codatatypes in Nitpick; this is useful if the datatype is used only as a means to define the codatatype
2009-11-05 blanchet 2009-11-05 don't promise too much in the Nitpick manual
2009-10-29 blanchet 2009-10-29 fixed minor problems with Nitpick's documentation
2009-10-28 blanchet 2009-10-28 introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian
2009-10-27 blanchet 2009-10-27 fix typo in Nitpick manual
2009-10-27 blanchet 2009-10-27 clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak
2009-10-27 blanchet 2009-10-27 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
2009-10-27 blanchet 2009-10-27 internal renaming in Nitpick and fixed Kodkodi invokation on Linux; renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi
2009-10-26 blanchet 2009-10-26 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
2009-10-23 blanchet 2009-10-23 updated Nitpick documentation to remove weird default for "overlord"
2009-10-23 blanchet 2009-10-23 updated Nitpick manual to reflect the latest Stand der Dinge
2009-10-22 blanchet 2009-10-22 wrap line correctly in Nitpick documentation
2009-10-22 blanchet 2009-10-22 Added Nitpick manual.