# HG changeset patch # User blanchet # Date 1280839782 -7200 # Node ID 7a88032f9265047149b5e555212f6fe6f979a968 # Parent 7207321df8afb87972e82b593287610a94204058 bump up the max cardinalities, to use up more of the time given to us by the user diff -r 7207321df8af -r 7a88032f9265 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 03 14:49:02 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 03 14:49:42 2010 +0200 @@ -1374,7 +1374,8 @@ case t |> strip_abs_body |> strip_comb of (Const x, ts as (_ :: _)) => (case def_of_const thy table x of - SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts + SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso + forall is_good_arg ts | NONE => false) | _ => false end diff -r 7207321df8af -r 7a88032f9265 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Aug 03 14:49:02 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Aug 03 14:49:42 2010 +0200 @@ -34,10 +34,10 @@ type raw_param = string * string list val default_default_params = - [("card", "1\8"), - ("iter", "0,1,2,4,8,12,16,24"), - ("bits", "1,2,3,4,6,8,10,12"), - ("bisim_depth", "7"), + [("card", "1\10"), + ("iter", "0,1,2,4,8,12,16,20,24,28"), + ("bits", "1,2,3,4,6,8,10,12,14,16"), + ("bisim_depth", "9"), ("box", "smart"), ("finitize", "smart"), ("mono", "smart"), @@ -265,7 +265,7 @@ val batch_size = case lookup_int_option "batch_size" of SOME n => Int.max (1, n) - | NONE => if debug then 1 else 64 + | NONE => if debug then 1 else 50 val expect = lookup_string "expect" in {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, diff -r 7207321df8af -r 7a88032f9265 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Aug 03 14:49:02 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Aug 03 14:49:42 2010 +0200 @@ -493,8 +493,8 @@ | repair_cards_assigns_wrt_boxing_etc thy Ts ((NONE, ks) :: cards_assigns) = (NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns -val max_scopes = 4096 -val distinct_threshold = 512 +val max_scopes = 5000 +val distinct_threshold = 1000 fun all_scopes (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs