--- 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:
--- 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 " ^
--- 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 =
--- 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;