Version 2010
* Added and implemented "binary_ints" and "bits" options
* Added "std" option and implemented support for nonstandard models
* Added and implemented "finitize" option to improve the precision of infinite
datatypes based on a monotonicity analysis
* Added support for quotient types
* Added support for "specification" and "ax_specification" constructs
* Added support for local definitions (for "function" and "termination"
proofs)
* Added support for term postprocessors
* Optimized "Multiset.multiset" and "FinFun.finfun"
* Improved efficiency of "destroy_constrs" optimization
* Fixed soundness bugs related to "destroy_constrs" optimization and record
getters
* Fixed soundness bug related to higher-order constructors
* Added cache to speed up repeated Kodkod invocations on the same problems
* Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
"MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
Version 2009-1
* Moved into Isabelle/HOL "Main"
* Renamed "nitpick_const_def" to "nitpick_def", "nitpick_const_simp" to
"nitpick_simp", "nitpick_const_psimp" to "nitpick_psimp", and
"nitpick_ind_intro" to "nitpick_intro"
* Replaced "special_depth" and "skolemize_depth" options by "specialize"
and "skolemize"
* Renamed "coalesce_type_vars" to "merge_type_vars"
* Optimized Kodkod encoding of datatypes whose constructors don't appear in
the formula to falsify
* Added support for codatatype view of datatypes
* Fixed soundness bug in the "uncurry" optimization
* Fixed soundness bugs related to sets, sets of sets, (co)inductive
predicates, typedefs, "finite", "rel_comp", and negative literals
* Fixed monotonicity check
* Fixed error when processing definitions
* Fixed error in "star_linear_preds" optimization
* Fixed error in Kodkod encoding of "The" and "Eps"
* Fixed error in display of uncurried constants
* Speeded up scope enumeration
Version 1.2.2 (16 Oct 2009)
* Added and implemented "star_linear_preds" option
* Added and implemented "format" option
* Added and implemented "coalesce_type_vars" option
* Added and implemented "max_genuine" option
* Fixed soundness issues related to "set", "distinct", "image", "Sigma",
"-1::nat", subset, constructors, sort axioms, and partially applied
interpreted constants
* Fixed error in "show_consts" for boxed specialized constants
* Fixed errors in Kodkod encoding of "The", "Eps", and "ind"
* Fixed display of Skolem constants
* Fixed error in "check_potential" and "check_genuine"
* Added boxing support for higher-order constructor parameters
* Changed notation used for coinductive datatypes
* Optimized Kodkod encoding of "If", "card", and "setsum"
* Improved the monotonicity check
Version 1.2.1 (25 Sep 2009)
* Added explicit support for coinductive datatypes
* Added and implemented "box" option
* Added and implemented "fast_descrs" option
* Added and implemented "uncurry" option
* Renamed and generalized "sync_cards" and "inductive_mood" to "mono" and "wf"
* Fixed soundness issue related to nullary constructors
* Fixed soundness issue related to higher-order quantifiers
* Fixed soundness issue related to the "destroy_constrs" optimization
* Fixed soundness issues related to the "special_depth" optimization
* Added support for PicoSAT and incorporated it with the Nitpick package
* Added automatic detection of installed SAT solvers based on naming
convention
* Optimized handling of quantifiers by moving them inward whenever possible
* Optimized and improved precision of "wf" and "wfrec"
* Improved handling of definitions made in locales
* Fixed checked scope count in message shown upon interruption and timeout
* Added minimalistic Nitpick-like tool called Minipick
Version 1.2.0 (27 Jul 2009)
* Optimized Kodkod encoding of datatypes and records
* Optimized coinductive definitions
* Fixed soundness issues related to pairs of functions
* Fixed soundness issue in the peephole optimizer
* Improved precision of non-well-founded predicates occurring positively in
the formula to falsify
* Added and implemented "destroy_constrs" option
* Changed semantics of "inductive_mood" option to ensure soundness
* Fixed semantics of "lockstep" option (broken in 1.1.1) and renamed it
"sync_cards"
* Improved precision of "trancl" and "rtrancl"
* Optimized Kodkod encoding of "tranclp" and "rtranclp"
* Made detection of inconsistent scope specifications more robust
* Fixed a few Kodkod generation bugs
Version 1.1.1 (24 Jun 2009)
* Added "show_all" option
* Fixed soundness issues related to type classes
* Improved precision of some set constructs
* Fiddled with the automatic monotonicity check
* Fixed performance issues related to scope enumeration
* Fixed a few Kodkod generation bugs
Version 1.1.0 (16 Jun 2009)
* Redesigned handling of datatypes to provide an interface baded on "card" and
"max", obsoleting "mult"
* Redesigned handling of typedefs, "rat", and "real"
* Made "lockstep" option a three-state option and added an automatic
monotonicity check
* Made "batch_size" a (n + 1)-state option whose default depends on whether
"debug" is enabled
* Made "debug" automatically enable "verbose"
* Added "destroy_equals" option
* Added "no_assms" option
* Fixed bug in computation of ground type
* Fixed performance issue related to datatype acyclicity constraint generation
* Fixed performance issue related to axiom selection
* Improved precision of some well-founded inductive predicates
* Added more checks to guard against very large cardinalities
* Improved hit rate of potential counterexamples
* Fixed several soundness issues
* Optimized the Kodkod encoding to benefit more from symmetry breaking
* Optimized relational composition, cartesian product, and converse
* Added support for HaifaSat
Version 1.0.3 (17 Mar 2009)
* Added "HOL-Nominal-Nitpick" as a target in addition to "HOL-Nitpick"
* Added "overlord" option to assist debugging
* Increased default value of "special_depth" option
* Fixed a bug that effectively disabled the "nitpick_const_def" attribute
* Ensured that no scopes are skipped when multithreading is enabled
* Fixed soundness issue in handling of "The", "Eps", and partial functions
defined using Isabelle's function package
* Fixed soundness issue in handling of non-definitional axioms
* Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
"nat", "int", and "*"
* Fixed a few Kodkod generation bugs
* Optimized "div", "mod", and "dvd" on "nat" and "int"
Version 1.0.2 (12 Mar 2009)
* Added support for non-definitional axioms
* Improved Isar integration
* Added support for multiplicities of 0
* Added "max_threads" option and support for multithreaded Kodkodi
* Added "blocking" option to control whether Nitpick should be run
synchronously or asynchronously
* Merged "auto_timeout" and "wellfounded_timeout" into "tac_timeout"
* Added "auto" option to run Nitpick automatically (like Auto Quickcheck)
* Introduced "auto_timeout" to specify Auto Nitpick's time limit
* Renamed the possible values for the "expect" option
* Renamed the "peephole" option to "peephole_optim"
* Added negative versions of all Boolean options and made "= true" optional
* Altered order of automatic SAT solver selection
Version 1.0.1 (6 Mar 2009)
* Eliminated the need to import "Nitpick" to use "nitpick"
* Added "debug" option
* Replaced "specialize_funs" with the more general "special_depth" option
* Renamed "watch" option to "eval"
* Improved parsing of "card", "mult", and "iter" options
* Fixed a soundness bug in the "specialize_funs" optimization
* Increased the scope of the "specialize_funs" optimization
* Fixed a soundness bug in the treatment of "<" and "<=" on type "int"
* Fixed a soundness bug in the "subterm property" optimization for types of
cardinality 1
* Improved the axiom selection for overloaded constants, which led to an
infinite loop for "Nominal.perm"
* Added support for multiple instantiations of non-well-founded inductive
predicates, which previously raised an exception
* Fixed a Kodkod generation bug
* Altered order of scope enumeration and automatic SAT solver selection
* Optimized "Eps", "nat_case", and "list_case"
* Improved output formatting
* Added checks to prevent infinite loops in axiom selector and constant
unfolding
Version 1.0.0 (27 Feb 2009)
* First release