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