added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
3 * Added and implemented "binary_ints" and "bits" options
4 * Added "std" option and implemented support for nonstandard models
5 * Added and implemented "finitize" option to improve the precision of infinite
6 datatypes based on a monotonicity analysis
7 * Added support for quotient types
8 * Added support for "specification" and "ax_specification" constructs
9 * Added support for local definitions (for "function" and "termination"
11 * Added support for term postprocessors
12 * Optimized "Multiset.multiset" and "FinFun.finfun"
13 * Improved efficiency of "destroy_constrs" optimization
14 * Fixed soundness bugs related to "destroy_constrs" optimization and record
16 * Fixed soundness bug related to higher-order constructors
17 * Improved precision of set constructs
18 * Added cache to speed up repeated Kodkod invocations on the same problems
19 * Added "atoms" option
20 * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
21 "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
22 * Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
23 "sharing_depth", and "show_skolems" options
27 * Moved into Isabelle/HOL "Main"
28 * Renamed "nitpick_const_def" to "nitpick_def", "nitpick_const_simp" to
29 "nitpick_simp", "nitpick_const_psimp" to "nitpick_psimp", and
30 "nitpick_ind_intro" to "nitpick_intro"
31 * Replaced "special_depth" and "skolemize_depth" options by "specialize"
33 * Renamed "coalesce_type_vars" to "merge_type_vars"
34 * Optimized Kodkod encoding of datatypes whose constructors don't appear in
35 the formula to falsify
36 * Added support for codatatype view of datatypes
37 * Fixed soundness bug in the "uncurry" optimization
38 * Fixed soundness bugs related to sets, sets of sets, (co)inductive
39 predicates, typedefs, "finite", "rel_comp", and negative literals
40 * Fixed monotonicity check
41 * Fixed error when processing definitions
42 * Fixed error in "star_linear_preds" optimization
43 * Fixed error in Kodkod encoding of "The" and "Eps"
44 * Fixed error in display of uncurried constants
45 * Speeded up scope enumeration
47 Version 1.2.2 (16 Oct 2009)
49 * Added and implemented "star_linear_preds" option
50 * Added and implemented "format" option
51 * Added and implemented "coalesce_type_vars" option
52 * Added and implemented "max_genuine" option
53 * Fixed soundness issues related to "set", "distinct", "image", "Sigma",
54 "-1::nat", subset, constructors, sort axioms, and partially applied
56 * Fixed error in "show_consts" for boxed specialized constants
57 * Fixed errors in Kodkod encoding of "The", "Eps", and "ind"
58 * Fixed display of Skolem constants
59 * Fixed error in "check_potential" and "check_genuine"
60 * Added boxing support for higher-order constructor parameters
61 * Changed notation used for coinductive datatypes
62 * Optimized Kodkod encoding of "If", "card", and "setsum"
63 * Improved the monotonicity check
65 Version 1.2.1 (25 Sep 2009)
67 * Added explicit support for coinductive datatypes
68 * Added and implemented "box" option
69 * Added and implemented "fast_descrs" option
70 * Added and implemented "uncurry" option
71 * Renamed and generalized "sync_cards" and "inductive_mood" to "mono" and "wf"
72 * Fixed soundness issue related to nullary constructors
73 * Fixed soundness issue related to higher-order quantifiers
74 * Fixed soundness issue related to the "destroy_constrs" optimization
75 * Fixed soundness issues related to the "special_depth" optimization
76 * Added support for PicoSAT and incorporated it with the Nitpick package
77 * Added automatic detection of installed SAT solvers based on naming
79 * Optimized handling of quantifiers by moving them inward whenever possible
80 * Optimized and improved precision of "wf" and "wfrec"
81 * Improved handling of definitions made in locales
82 * Fixed checked scope count in message shown upon interruption and timeout
83 * Added minimalistic Nitpick-like tool called Minipick
85 Version 1.2.0 (27 Jul 2009)
87 * Optimized Kodkod encoding of datatypes and records
88 * Optimized coinductive definitions
89 * Fixed soundness issues related to pairs of functions
90 * Fixed soundness issue in the peephole optimizer
91 * Improved precision of non-well-founded predicates occurring positively in
92 the formula to falsify
93 * Added and implemented "destroy_constrs" option
94 * Changed semantics of "inductive_mood" option to ensure soundness
95 * Fixed semantics of "lockstep" option (broken in 1.1.1) and renamed it
97 * Improved precision of "trancl" and "rtrancl"
98 * Optimized Kodkod encoding of "tranclp" and "rtranclp"
99 * Made detection of inconsistent scope specifications more robust
100 * Fixed a few Kodkod generation bugs
102 Version 1.1.1 (24 Jun 2009)
104 * Added "show_all" option
105 * Fixed soundness issues related to type classes
106 * Improved precision of some set constructs
107 * Fiddled with the automatic monotonicity check
108 * Fixed performance issues related to scope enumeration
109 * Fixed a few Kodkod generation bugs
111 Version 1.1.0 (16 Jun 2009)
113 * Redesigned handling of datatypes to provide an interface baded on "card" and
114 "max", obsoleting "mult"
115 * Redesigned handling of typedefs, "rat", and "real"
116 * Made "lockstep" option a three-state option and added an automatic
118 * Made "batch_size" a (n + 1)-state option whose default depends on whether
120 * Made "debug" automatically enable "verbose"
121 * Added "destroy_equals" option
122 * Added "no_assms" option
123 * Fixed bug in computation of ground type
124 * Fixed performance issue related to datatype acyclicity constraint generation
125 * Fixed performance issue related to axiom selection
126 * Improved precision of some well-founded inductive predicates
127 * Added more checks to guard against very large cardinalities
128 * Improved hit rate of potential counterexamples
129 * Fixed several soundness issues
130 * Optimized the Kodkod encoding to benefit more from symmetry breaking
131 * Optimized relational composition, cartesian product, and converse
132 * Added support for HaifaSat
134 Version 1.0.3 (17 Mar 2009)
136 * Added "HOL-Nominal-Nitpick" as a target in addition to "HOL-Nitpick"
137 * Added "overlord" option to assist debugging
138 * Increased default value of "special_depth" option
139 * Fixed a bug that effectively disabled the "nitpick_const_def" attribute
140 * Ensured that no scopes are skipped when multithreading is enabled
141 * Fixed soundness issue in handling of "The", "Eps", and partial functions
142 defined using Isabelle's function package
143 * Fixed soundness issue in handling of non-definitional axioms
144 * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
145 "nat", "int", and "*"
146 * Fixed a few Kodkod generation bugs
147 * Optimized "div", "mod", and "dvd" on "nat" and "int"
149 Version 1.0.2 (12 Mar 2009)
151 * Added support for non-definitional axioms
152 * Improved Isar integration
153 * Added support for multiplicities of 0
154 * Added "max_threads" option and support for multithreaded Kodkodi
155 * Added "blocking" option to control whether Nitpick should be run
156 synchronously or asynchronously
157 * Merged "auto_timeout" and "wellfounded_timeout" into "tac_timeout"
158 * Added "auto" option to run Nitpick automatically (like Auto Quickcheck)
159 * Introduced "auto_timeout" to specify Auto Nitpick's time limit
160 * Renamed the possible values for the "expect" option
161 * Renamed the "peephole" option to "peephole_optim"
162 * Added negative versions of all Boolean options and made "= true" optional
163 * Altered order of automatic SAT solver selection
165 Version 1.0.1 (6 Mar 2009)
167 * Eliminated the need to import "Nitpick" to use "nitpick"
168 * Added "debug" option
169 * Replaced "specialize_funs" with the more general "special_depth" option
170 * Renamed "watch" option to "eval"
171 * Improved parsing of "card", "mult", and "iter" options
172 * Fixed a soundness bug in the "specialize_funs" optimization
173 * Increased the scope of the "specialize_funs" optimization
174 * Fixed a soundness bug in the treatment of "<" and "<=" on type "int"
175 * Fixed a soundness bug in the "subterm property" optimization for types of
177 * Improved the axiom selection for overloaded constants, which led to an
178 infinite loop for "Nominal.perm"
179 * Added support for multiple instantiations of non-well-founded inductive
180 predicates, which previously raised an exception
181 * Fixed a Kodkod generation bug
182 * Altered order of scope enumeration and automatic SAT solver selection
183 * Optimized "Eps", "nat_case", and "list_case"
184 * Improved output formatting
185 * Added checks to prevent infinite loops in axiom selector and constant
188 Version 1.0.0 (27 Feb 2009)