1.1 --- a/doc-src/Nitpick/nitpick.tex	Sat Apr 24 16:33:01 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Sat Apr 24 16:43:03 2010 +0200
     1.3 @@ -2498,25 +2498,6 @@
     1.4  Unless you are tracking down a bug in Nitpick or distrust the peephole
     1.5  optimizer, you should leave this option enabled.
     1.6  
     1.7 -\opdefault{sym\_break}{int}{20}
     1.8 -Specifies an upper bound on the number of relations for which Kodkod generates
     1.9 -symmetry breaking predicates. According to the Kodkod documentation
    1.10 -\cite{kodkod-2009-options}, ``in general, the higher this value, the more
    1.11 -symmetries will be broken, and the faster the formula will be solved. But,
    1.12 -setting the value too high may have the opposite effect and slow down the
    1.13 -solving.''
    1.14 -
    1.15 -\opdefault{sharing\_depth}{int}{3}
    1.16 -Specifies the depth to which Kodkod should check circuits for equivalence during
    1.17 -the translation to SAT. The default of 3 is the same as in Alloy. The minimum
    1.18 -allowed depth is 1. Increasing the sharing may result in a smaller SAT problem,
    1.19 -but can also slow down Kodkod.
    1.20 -
    1.21 -\opfalse{flatten\_props}{dont\_flatten\_props}
    1.22 -Specifies whether Kodkod should try to eliminate intermediate Boolean variables.
    1.23 -Although this might sound like a good idea, in practice it can drastically slow
    1.24 -down Kodkod.
    1.25 -
    1.26  \opdefault{max\_threads}{int}{0}
    1.27  Specifies the maximum number of threads to use in Kodkod. If this option is set
    1.28  to 0, Kodkod will compute an appropriate value based on the number of processor
    1.29 @@ -2569,7 +2550,7 @@
    1.30  Behind the scenes, Isabelle's built-in packages and theories rely on the
    1.31  following attributes to affect Nitpick's behavior:
    1.32  
    1.33 -\begin{itemize}
    1.34 +\begin{enum}
    1.35  \flushitem{\textit{nitpick\_def}}
    1.36  
    1.37  \nopagebreak
    1.38 @@ -2623,7 +2604,7 @@
    1.39  This attribute specifies the (free-form) specification of a constant defined
    1.40  using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
    1.41  
    1.42 -\end{itemize}
    1.43 +\end{enum}
    1.44  
    1.45  When faced with a constant, Nitpick proceeds as follows:
    1.46  

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 24 16:33:01 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 24 16:43:03 2010 +0200
     2.3 @@ -39,9 +39,6 @@
     2.4      peephole_optim: bool,
     2.5      timeout: Time.time option,
     2.6      tac_timeout: Time.time option,
     2.7 -    sym_break: int,
     2.8 -    sharing_depth: int,
     2.9 -    flatten_props: bool,
    2.10      max_threads: int,
    2.11      show_skolems: bool,
    2.12      show_datatypes: bool,
    2.13 @@ -115,9 +112,6 @@
    2.14    peephole_optim: bool,
    2.15    timeout: Time.time option,
    2.16    tac_timeout: Time.time option,
    2.17 -  sym_break: int,
    2.18 -  sharing_depth: int,
    2.19 -  flatten_props: bool,
    2.20    max_threads: int,
    2.21    show_skolems: bool,
    2.22    show_datatypes: bool,
    2.23 @@ -201,10 +195,9 @@
    2.24           boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    2.25           verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
    2.26           destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
    2.27 -         fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
    2.28 -         flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
    2.29 -         evals, formats, max_potential, max_genuine, check_potential,
    2.30 -         check_genuine, batch_size, ...} =
    2.31 +         fast_descrs, peephole_optim, tac_timeout, max_threads, show_skolems,
    2.32 +         show_datatypes, show_consts, evals, formats, max_potential,
    2.33 +         max_genuine, check_potential, check_genuine, batch_size, ...} =
    2.34        params
    2.35      val state_ref = Unsynchronized.ref state
    2.36      val pprint =
    2.37 @@ -511,9 +504,9 @@
    2.38          val settings = [("solver", commas_quote kodkod_sat_solver),
    2.39                          ("skolem_depth", "-1"),
    2.40                          ("bit_width", string_of_int bit_width),
    2.41 -                        ("symmetry_breaking", signed_string_of_int sym_break),
    2.42 -                        ("sharing", signed_string_of_int sharing_depth),
    2.43 -                        ("flatten", Bool.toString flatten_props),
    2.44 +                        ("symmetry_breaking", "20"),
    2.45 +                        ("sharing", "3"),
    2.46 +                        ("flatten", "false"),
    2.47                          ("delay", signed_string_of_int delay)]
    2.48          val plain_rels = free_rels @ other_rels
    2.49          val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
    2.50 @@ -922,8 +915,8 @@
    2.51          end
    2.52  
    2.53      val (skipped, the_scopes) =
    2.54 -      all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns
    2.55 -                 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    2.56 +      all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
    2.57 +                 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    2.58                   finitizable_dataTs
    2.59      val _ = if skipped > 0 then
    2.60                print_m (fn () => "Too many scopes. Skipping " ^

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Apr 24 16:33:01 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Apr 24 16:43:03 2010 +0200
     3.3 @@ -62,9 +62,6 @@
     3.4     ("peephole_optim", "true"),
     3.5     ("timeout", "30 s"),
     3.6     ("tac_timeout", "500 ms"),
     3.7 -   ("sym_break", "20"),
     3.8 -   ("sharing_depth", "3"),
     3.9 -   ("flatten_props", "false"),
    3.10     ("max_threads", "0"),
    3.11     ("debug", "false"),
    3.12     ("verbose", "false"),
    3.13 @@ -98,7 +95,6 @@
    3.14     ("dont_uncurry", "uncurry"),
    3.15     ("full_descrs", "fast_descrs"),
    3.16     ("no_peephole_optim", "peephole_optim"),
    3.17 -   ("dont_flatten_props", "flatten_props"),
    3.18     ("no_debug", "debug"),
    3.19     ("quiet", "verbose"),
    3.20     ("no_overlord", "overlord"),
    3.21 @@ -263,9 +259,6 @@
    3.22      val peephole_optim = lookup_bool "peephole_optim"
    3.23      val timeout = if auto then NONE else lookup_time "timeout"
    3.24      val tac_timeout = lookup_time "tac_timeout"
    3.25 -    val sym_break = Int.max (0, lookup_int "sym_break")
    3.26 -    val sharing_depth = Int.max (1, lookup_int "sharing_depth")
    3.27 -    val flatten_props = lookup_bool "flatten_props"
    3.28      val max_threads = Int.max (0, lookup_int "max_threads")
    3.29      val show_all = debug orelse lookup_bool "show_all"
    3.30      val show_skolems = show_all orelse lookup_bool "show_skolems"
    3.31 @@ -294,13 +287,12 @@
    3.32       skolemize = skolemize, star_linear_preds = star_linear_preds,
    3.33       uncurry = uncurry, fast_descrs = fast_descrs,
    3.34       peephole_optim = peephole_optim, timeout = timeout,
    3.35 -     tac_timeout = tac_timeout, sym_break = sym_break,
    3.36 -     sharing_depth = sharing_depth, flatten_props = flatten_props,
    3.37 -     max_threads = max_threads, show_skolems = show_skolems,
    3.38 -     show_datatypes = show_datatypes, show_consts = show_consts,
    3.39 -     formats = formats, evals = evals, max_potential = max_potential,
    3.40 -     max_genuine = max_genuine, check_potential = check_potential,
    3.41 -     check_genuine = check_genuine, batch_size = batch_size, expect = expect}
    3.42 +     tac_timeout = tac_timeout, max_threads = max_threads,
    3.43 +     show_skolems = show_skolems, show_datatypes = show_datatypes,
    3.44 +     show_consts = show_consts, formats = formats, evals = evals,
    3.45 +     max_potential = max_potential, max_genuine = max_genuine,
    3.46 +     check_potential = check_potential, check_genuine = check_genuine,
    3.47 +     batch_size = batch_size, expect = expect}
    3.48    end
    3.49  
    3.50  fun default_params thy =

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sat Apr 24 16:33:01 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sat Apr 24 16:43:03 2010 +0200
     4.3 @@ -49,7 +49,7 @@
     4.4    val scopes_equivalent : scope * scope -> bool
     4.5    val scope_less_eq : scope -> scope -> bool
     4.6    val all_scopes :
     4.7 -    hol_context -> bool -> int -> (typ option * int list) list
     4.8 +    hol_context -> bool -> (typ option * int list) list
     4.9      -> (styp option * int list) list -> (styp option * int list) list
    4.10      -> int list -> int list -> typ list -> typ list -> typ list -> typ list
    4.11      -> int * scope list
    4.12 @@ -458,9 +458,8 @@
    4.13       concrete = concrete, deep = deep, constrs = constrs}
    4.14    end
    4.15  
    4.16 -fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
    4.17 -                          deep_dataTs finitizable_dataTs
    4.18 -                          (desc as (card_assigns, _)) =
    4.19 +fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize deep_dataTs
    4.20 +                          finitizable_dataTs (desc as (card_assigns, _)) =
    4.21    let
    4.22      val datatypes =
    4.23        map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
    4.24 @@ -474,8 +473,7 @@
    4.25    in
    4.26      {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    4.27       datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
    4.28 -     ofs = if sym_break <= 0 then Typtab.empty
    4.29 -           else offset_table_for_card_assigns card_assigns datatypes}
    4.30 +     ofs = offset_table_for_card_assigns card_assigns datatypes}
    4.31    end
    4.32  
    4.33  fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []
    4.34 @@ -491,9 +489,9 @@
    4.35  val max_scopes = 4096
    4.36  val distinct_threshold = 512
    4.37  
    4.38 -fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns
    4.39 -               maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
    4.40 -               deep_dataTs finitizable_dataTs =
    4.41 +fun all_scopes (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
    4.42 +               iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    4.43 +               finitizable_dataTs =
    4.44    let
    4.45      val cards_assigns = repair_cards_assigns_wrt_boxing_etc thy mono_Ts
    4.46                                                              cards_assigns
    4.47 @@ -509,8 +507,8 @@
    4.48    in
    4.49      (length all - length head,
    4.50       descs |> length descs <= distinct_threshold ? distinct (op =)
    4.51 -           |> map (scope_from_descriptor hol_ctxt binarize sym_break
    4.52 -                                         deep_dataTs finitizable_dataTs))
    4.53 +           |> map (scope_from_descriptor hol_ctxt binarize deep_dataTs
    4.54 +                                         finitizable_dataTs))
    4.55    end
    4.56  
    4.57  end;