--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Aug 01 15:51:25 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Aug 01 16:35:25 2010 +0200
@@ -56,8 +56,8 @@
("star_linear_preds", "true"),
("fast_descrs", "true"),
("peephole_optim", "true"),
- ("datatype_sym_break", "20"),
- ("kodkod_sym_break", "20"),
+ ("datatype_sym_break", "5"),
+ ("kodkod_sym_break", "15"),
("timeout", "30 s"),
("tac_timeout", "500 ms"),
("max_threads", "0"),
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sun Aug 01 15:51:25 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sun Aug 01 16:35:25 2010 +0200
@@ -786,6 +786,7 @@
break cycles; otherwise, we may end up with two incompatible symmetry
breaking orders, leading to spurious models. *)
fun should_tabulate_suc_for_type dtypes T =
+ is_asymmetric_nondatatype T orelse
case datatype_spec dtypes T of
SOME {self_rec, ...} => self_rec
| NONE => false
@@ -908,7 +909,10 @@
dtypes)
(dtypes |> filter is_datatype_good_and_old
|> filter (fn {constrs = [_], ...} => false
- | {card, ...} => card >= min_sym_break_card)
+ | {card, constrs, ...} =>
+ card >= min_sym_break_card andalso
+ forall (forall (not o is_higher_order_type)
+ o binder_types o snd o #const) constrs)
|> (fn dtypes' =>
dtypes'
|> length dtypes' > datatype_sym_break
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Sun Aug 01 15:51:25 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sun Aug 01 16:35:25 2010 +0200
@@ -38,6 +38,7 @@
datatypes: datatype_spec list,
ofs: int Typtab.table}
+ val is_asymmetric_nondatatype : typ -> bool
val datatype_spec : datatype_spec list -> typ -> datatype_spec option
val constr_spec : datatype_spec list -> styp -> constr_spec
val is_complete_type : datatype_spec list -> bool -> typ -> bool
@@ -96,6 +97,9 @@
type row = row_kind * int list
type block = row list
+val is_asymmetric_nondatatype =
+ is_iterator_type orf is_integer_type orf is_bit_type
+
fun datatype_spec (dtypes : datatype_spec list) T =
List.find (curry (op =) T o #typ) dtypes
@@ -368,8 +372,7 @@
let
fun aux next _ [] = Typtab.update_new (dummyT, next)
| aux next reusable ((T, k) :: assigns) =
- if k = 1 orelse is_iterator_type T orelse is_integer_type T
- orelse is_bit_type T then
+ if k = 1 orelse is_asymmetric_nondatatype T then
aux next reusable assigns
else if length (these (Option.map #constrs (datatype_spec dtypes T)))
> 1 then