# HG changeset patch # User blanchet # Date 1272120183 -7200 # Node ID 2132f15b366f69f803305fadc342e1d699583c5c # Parent ff5f88702590cabf8c47f474e02301abd9a81fc5 Fruhjahrsputz: remove three mostly useless Nitpick options diff -r ff5f88702590 -r 2132f15b366f doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Sat Apr 24 16:33:01 2010 +0200 +++ b/doc-src/Nitpick/nitpick.tex Sat Apr 24 16:43:03 2010 +0200 @@ -2498,25 +2498,6 @@ Unless you are tracking down a bug in Nitpick or distrust the peephole optimizer, you should leave this option enabled. -\opdefault{sym\_break}{int}{20} -Specifies an upper bound on the number of relations for which Kodkod generates -symmetry breaking predicates. According to the Kodkod documentation -\cite{kodkod-2009-options}, ``in general, the higher this value, the more -symmetries will be broken, and the faster the formula will be solved. But, -setting the value too high may have the opposite effect and slow down the -solving.'' - -\opdefault{sharing\_depth}{int}{3} -Specifies the depth to which Kodkod should check circuits for equivalence during -the translation to SAT. The default of 3 is the same as in Alloy. The minimum -allowed depth is 1. Increasing the sharing may result in a smaller SAT problem, -but can also slow down Kodkod. - -\opfalse{flatten\_props}{dont\_flatten\_props} -Specifies whether Kodkod should try to eliminate intermediate Boolean variables. -Although this might sound like a good idea, in practice it can drastically slow -down Kodkod. - \opdefault{max\_threads}{int}{0} Specifies the maximum number of threads to use in Kodkod. If this option is set to 0, Kodkod will compute an appropriate value based on the number of processor @@ -2569,7 +2550,7 @@ Behind the scenes, Isabelle's built-in packages and theories rely on the following attributes to affect Nitpick's behavior: -\begin{itemize} +\begin{enum} \flushitem{\textit{nitpick\_def}} \nopagebreak @@ -2623,7 +2604,7 @@ This attribute specifies the (free-form) specification of a constant defined using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command. -\end{itemize} +\end{enum} When faced with a constant, Nitpick proceeds as follows: diff -r ff5f88702590 -r 2132f15b366f src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 16:33:01 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 16:43:03 2010 +0200 @@ -39,9 +39,6 @@ peephole_optim: bool, timeout: Time.time option, tac_timeout: Time.time option, - sym_break: int, - sharing_depth: int, - flatten_props: bool, max_threads: int, show_skolems: bool, show_datatypes: bool, @@ -115,9 +112,6 @@ peephole_optim: bool, timeout: Time.time option, tac_timeout: Time.time option, - sym_break: int, - sharing_depth: int, - flatten_props: bool, max_threads: int, show_skolems: bool, show_datatypes: bool, @@ -201,10 +195,9 @@ boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints, destroy_constrs, specialize, skolemize, star_linear_preds, uncurry, - fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth, - flatten_props, max_threads, show_skolems, show_datatypes, show_consts, - evals, formats, max_potential, max_genuine, check_potential, - check_genuine, batch_size, ...} = + fast_descrs, peephole_optim, tac_timeout, max_threads, show_skolems, + show_datatypes, show_consts, evals, formats, max_potential, + max_genuine, check_potential, check_genuine, batch_size, ...} = params val state_ref = Unsynchronized.ref state val pprint = @@ -511,9 +504,9 @@ val settings = [("solver", commas_quote kodkod_sat_solver), ("skolem_depth", "-1"), ("bit_width", string_of_int bit_width), - ("symmetry_breaking", signed_string_of_int sym_break), - ("sharing", signed_string_of_int sharing_depth), - ("flatten", Bool.toString flatten_props), + ("symmetry_breaking", "20"), + ("sharing", "3"), + ("flatten", "false"), ("delay", signed_string_of_int delay)] val plain_rels = free_rels @ other_rels val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels @@ -922,8 +915,8 @@ end val (skipped, the_scopes) = - all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns - iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs + all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns + bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs finitizable_dataTs val _ = if skipped > 0 then print_m (fn () => "Too many scopes. Skipping " ^ diff -r ff5f88702590 -r 2132f15b366f src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 16:33:01 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 16:43:03 2010 +0200 @@ -62,9 +62,6 @@ ("peephole_optim", "true"), ("timeout", "30 s"), ("tac_timeout", "500 ms"), - ("sym_break", "20"), - ("sharing_depth", "3"), - ("flatten_props", "false"), ("max_threads", "0"), ("debug", "false"), ("verbose", "false"), @@ -98,7 +95,6 @@ ("dont_uncurry", "uncurry"), ("full_descrs", "fast_descrs"), ("no_peephole_optim", "peephole_optim"), - ("dont_flatten_props", "flatten_props"), ("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), @@ -263,9 +259,6 @@ val peephole_optim = lookup_bool "peephole_optim" val timeout = if auto then NONE else lookup_time "timeout" val tac_timeout = lookup_time "tac_timeout" - val sym_break = Int.max (0, lookup_int "sym_break") - val sharing_depth = Int.max (1, lookup_int "sharing_depth") - val flatten_props = lookup_bool "flatten_props" val max_threads = Int.max (0, lookup_int "max_threads") val show_all = debug orelse lookup_bool "show_all" val show_skolems = show_all orelse lookup_bool "show_skolems" @@ -294,13 +287,12 @@ skolemize = skolemize, star_linear_preds = star_linear_preds, uncurry = uncurry, fast_descrs = fast_descrs, peephole_optim = peephole_optim, timeout = timeout, - tac_timeout = tac_timeout, sym_break = sym_break, - sharing_depth = sharing_depth, flatten_props = flatten_props, - max_threads = max_threads, show_skolems = show_skolems, - show_datatypes = show_datatypes, show_consts = show_consts, - formats = formats, evals = evals, max_potential = max_potential, - max_genuine = max_genuine, check_potential = check_potential, - check_genuine = check_genuine, batch_size = batch_size, expect = expect} + tac_timeout = tac_timeout, max_threads = max_threads, + show_skolems = show_skolems, show_datatypes = show_datatypes, + show_consts = show_consts, formats = formats, evals = evals, + max_potential = max_potential, max_genuine = max_genuine, + check_potential = check_potential, check_genuine = check_genuine, + batch_size = batch_size, expect = expect} end fun default_params thy = diff -r ff5f88702590 -r 2132f15b366f src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Apr 24 16:33:01 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Apr 24 16:43:03 2010 +0200 @@ -49,7 +49,7 @@ val scopes_equivalent : scope * scope -> bool val scope_less_eq : scope -> scope -> bool val all_scopes : - hol_context -> bool -> int -> (typ option * int list) list + hol_context -> bool -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list -> int list -> int list -> typ list -> typ list -> typ list -> typ list -> int * scope list @@ -458,9 +458,8 @@ concrete = concrete, deep = deep, constrs = constrs} end -fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break - deep_dataTs finitizable_dataTs - (desc as (card_assigns, _)) = +fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize deep_dataTs + finitizable_dataTs (desc as (card_assigns, _)) = let val datatypes = map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs @@ -474,8 +473,7 @@ in {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns, datatypes = datatypes, bits = bits, bisim_depth = bisim_depth, - ofs = if sym_break <= 0 then Typtab.empty - else offset_table_for_card_assigns card_assigns datatypes} + ofs = offset_table_for_card_assigns card_assigns datatypes} end fun repair_cards_assigns_wrt_boxing_etc _ _ [] = [] @@ -491,9 +489,9 @@ val max_scopes = 4096 val distinct_threshold = 512 -fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns - maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts - deep_dataTs finitizable_dataTs = +fun all_scopes (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns + iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs + finitizable_dataTs = let val cards_assigns = repair_cards_assigns_wrt_boxing_etc thy mono_Ts cards_assigns @@ -509,8 +507,8 @@ in (length all - length head, descs |> length descs <= distinct_threshold ? distinct (op =) - |> map (scope_from_descriptor hol_ctxt binarize sym_break - deep_dataTs finitizable_dataTs)) + |> map (scope_from_descriptor hol_ctxt binarize deep_dataTs + finitizable_dataTs)) end end;