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