1.1 --- a/src/HOL/Tools/Nitpick/HISTORY Tue Jun 01 14:54:35 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,190 +0,0 @@
1.4 -Version 2010
1.5 -
1.6 - * Added and implemented "binary_ints" and "bits" options
1.7 - * Added "std" option and implemented support for nonstandard models
1.8 - * Added and implemented "finitize" option to improve the precision of infinite
1.9 - datatypes based on a monotonicity analysis
1.10 - * Added support for quotient types
1.11 - * Added support for "specification" and "ax_specification" constructs
1.12 - * Added support for local definitions (for "function" and "termination"
1.13 - proofs)
1.14 - * Added support for term postprocessors
1.15 - * Optimized "Multiset.multiset" and "FinFun.finfun"
1.16 - * Improved efficiency of "destroy_constrs" optimization
1.17 - * Fixed soundness bugs related to "destroy_constrs" optimization and record
1.18 - getters
1.19 - * Fixed soundness bug related to higher-order constructors
1.20 - * Improved precision of set constructs
1.21 - * Added cache to speed up repeated Kodkod invocations on the same problems
1.22 - * Added "atoms" option
1.23 - * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
1.24 - "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
1.25 - * Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
1.26 - "sharing_depth", and "show_skolems" options
1.27 -
1.28 -Version 2009-1
1.29 -
1.30 - * Moved into Isabelle/HOL "Main"
1.31 - * Renamed "nitpick_const_def" to "nitpick_def", "nitpick_const_simp" to
1.32 - "nitpick_simp", "nitpick_const_psimp" to "nitpick_psimp", and
1.33 - "nitpick_ind_intro" to "nitpick_intro"
1.34 - * Replaced "special_depth" and "skolemize_depth" options by "specialize"
1.35 - and "skolemize"
1.36 - * Renamed "coalesce_type_vars" to "merge_type_vars"
1.37 - * Optimized Kodkod encoding of datatypes whose constructors don't appear in
1.38 - the formula to falsify
1.39 - * Added support for codatatype view of datatypes
1.40 - * Fixed soundness bug in the "uncurry" optimization
1.41 - * Fixed soundness bugs related to sets, sets of sets, (co)inductive
1.42 - predicates, typedefs, "finite", "rel_comp", and negative literals
1.43 - * Fixed monotonicity check
1.44 - * Fixed error when processing definitions
1.45 - * Fixed error in "star_linear_preds" optimization
1.46 - * Fixed error in Kodkod encoding of "The" and "Eps"
1.47 - * Fixed error in display of uncurried constants
1.48 - * Speeded up scope enumeration
1.49 -
1.50 -Version 1.2.2 (16 Oct 2009)
1.51 -
1.52 - * Added and implemented "star_linear_preds" option
1.53 - * Added and implemented "format" option
1.54 - * Added and implemented "coalesce_type_vars" option
1.55 - * Added and implemented "max_genuine" option
1.56 - * Fixed soundness issues related to "set", "distinct", "image", "Sigma",
1.57 - "-1::nat", subset, constructors, sort axioms, and partially applied
1.58 - interpreted constants
1.59 - * Fixed error in "show_consts" for boxed specialized constants
1.60 - * Fixed errors in Kodkod encoding of "The", "Eps", and "ind"
1.61 - * Fixed display of Skolem constants
1.62 - * Fixed error in "check_potential" and "check_genuine"
1.63 - * Added boxing support for higher-order constructor parameters
1.64 - * Changed notation used for coinductive datatypes
1.65 - * Optimized Kodkod encoding of "If", "card", and "setsum"
1.66 - * Improved the monotonicity check
1.67 -
1.68 -Version 1.2.1 (25 Sep 2009)
1.69 -
1.70 - * Added explicit support for coinductive datatypes
1.71 - * Added and implemented "box" option
1.72 - * Added and implemented "fast_descrs" option
1.73 - * Added and implemented "uncurry" option
1.74 - * Renamed and generalized "sync_cards" and "inductive_mood" to "mono" and "wf"
1.75 - * Fixed soundness issue related to nullary constructors
1.76 - * Fixed soundness issue related to higher-order quantifiers
1.77 - * Fixed soundness issue related to the "destroy_constrs" optimization
1.78 - * Fixed soundness issues related to the "special_depth" optimization
1.79 - * Added support for PicoSAT and incorporated it with the Nitpick package
1.80 - * Added automatic detection of installed SAT solvers based on naming
1.81 - convention
1.82 - * Optimized handling of quantifiers by moving them inward whenever possible
1.83 - * Optimized and improved precision of "wf" and "wfrec"
1.84 - * Improved handling of definitions made in locales
1.85 - * Fixed checked scope count in message shown upon interruption and timeout
1.86 - * Added minimalistic Nitpick-like tool called Minipick
1.87 -
1.88 -Version 1.2.0 (27 Jul 2009)
1.89 -
1.90 - * Optimized Kodkod encoding of datatypes and records
1.91 - * Optimized coinductive definitions
1.92 - * Fixed soundness issues related to pairs of functions
1.93 - * Fixed soundness issue in the peephole optimizer
1.94 - * Improved precision of non-well-founded predicates occurring positively in
1.95 - the formula to falsify
1.96 - * Added and implemented "destroy_constrs" option
1.97 - * Changed semantics of "inductive_mood" option to ensure soundness
1.98 - * Fixed semantics of "lockstep" option (broken in 1.1.1) and renamed it
1.99 - "sync_cards"
1.100 - * Improved precision of "trancl" and "rtrancl"
1.101 - * Optimized Kodkod encoding of "tranclp" and "rtranclp"
1.102 - * Made detection of inconsistent scope specifications more robust
1.103 - * Fixed a few Kodkod generation bugs
1.104 -
1.105 -Version 1.1.1 (24 Jun 2009)
1.106 -
1.107 - * Added "show_all" option
1.108 - * Fixed soundness issues related to type classes
1.109 - * Improved precision of some set constructs
1.110 - * Fiddled with the automatic monotonicity check
1.111 - * Fixed performance issues related to scope enumeration
1.112 - * Fixed a few Kodkod generation bugs
1.113 -
1.114 -Version 1.1.0 (16 Jun 2009)
1.115 -
1.116 - * Redesigned handling of datatypes to provide an interface baded on "card" and
1.117 - "max", obsoleting "mult"
1.118 - * Redesigned handling of typedefs, "rat", and "real"
1.119 - * Made "lockstep" option a three-state option and added an automatic
1.120 - monotonicity check
1.121 - * Made "batch_size" a (n + 1)-state option whose default depends on whether
1.122 - "debug" is enabled
1.123 - * Made "debug" automatically enable "verbose"
1.124 - * Added "destroy_equals" option
1.125 - * Added "no_assms" option
1.126 - * Fixed bug in computation of ground type
1.127 - * Fixed performance issue related to datatype acyclicity constraint generation
1.128 - * Fixed performance issue related to axiom selection
1.129 - * Improved precision of some well-founded inductive predicates
1.130 - * Added more checks to guard against very large cardinalities
1.131 - * Improved hit rate of potential counterexamples
1.132 - * Fixed several soundness issues
1.133 - * Optimized the Kodkod encoding to benefit more from symmetry breaking
1.134 - * Optimized relational composition, cartesian product, and converse
1.135 - * Added support for HaifaSat
1.136 -
1.137 -Version 1.0.3 (17 Mar 2009)
1.138 -
1.139 - * Added "HOL-Nominal-Nitpick" as a target in addition to "HOL-Nitpick"
1.140 - * Added "overlord" option to assist debugging
1.141 - * Increased default value of "special_depth" option
1.142 - * Fixed a bug that effectively disabled the "nitpick_const_def" attribute
1.143 - * Ensured that no scopes are skipped when multithreading is enabled
1.144 - * Fixed soundness issue in handling of "The", "Eps", and partial functions
1.145 - defined using Isabelle's function package
1.146 - * Fixed soundness issue in handling of non-definitional axioms
1.147 - * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
1.148 - "nat", "int", and "*"
1.149 - * Fixed a few Kodkod generation bugs
1.150 - * Optimized "div", "mod", and "dvd" on "nat" and "int"
1.151 -
1.152 -Version 1.0.2 (12 Mar 2009)
1.153 -
1.154 - * Added support for non-definitional axioms
1.155 - * Improved Isar integration
1.156 - * Added support for multiplicities of 0
1.157 - * Added "max_threads" option and support for multithreaded Kodkodi
1.158 - * Added "blocking" option to control whether Nitpick should be run
1.159 - synchronously or asynchronously
1.160 - * Merged "auto_timeout" and "wellfounded_timeout" into "tac_timeout"
1.161 - * Added "auto" option to run Nitpick automatically (like Auto Quickcheck)
1.162 - * Introduced "auto_timeout" to specify Auto Nitpick's time limit
1.163 - * Renamed the possible values for the "expect" option
1.164 - * Renamed the "peephole" option to "peephole_optim"
1.165 - * Added negative versions of all Boolean options and made "= true" optional
1.166 - * Altered order of automatic SAT solver selection
1.167 -
1.168 -Version 1.0.1 (6 Mar 2009)
1.169 -
1.170 - * Eliminated the need to import "Nitpick" to use "nitpick"
1.171 - * Added "debug" option
1.172 - * Replaced "specialize_funs" with the more general "special_depth" option
1.173 - * Renamed "watch" option to "eval"
1.174 - * Improved parsing of "card", "mult", and "iter" options
1.175 - * Fixed a soundness bug in the "specialize_funs" optimization
1.176 - * Increased the scope of the "specialize_funs" optimization
1.177 - * Fixed a soundness bug in the treatment of "<" and "<=" on type "int"
1.178 - * Fixed a soundness bug in the "subterm property" optimization for types of
1.179 - cardinality 1
1.180 - * Improved the axiom selection for overloaded constants, which led to an
1.181 - infinite loop for "Nominal.perm"
1.182 - * Added support for multiple instantiations of non-well-founded inductive
1.183 - predicates, which previously raised an exception
1.184 - * Fixed a Kodkod generation bug
1.185 - * Altered order of scope enumeration and automatic SAT solver selection
1.186 - * Optimized "Eps", "nat_case", and "list_case"
1.187 - * Improved output formatting
1.188 - * Added checks to prevent infinite loops in axiom selector and constant
1.189 - unfolding
1.190 -
1.191 -Version 1.0.0 (27 Feb 2009)
1.192 -
1.193 - * First release