# HG changeset patch # User blanchet # Date 1299147648 -3600 # Node ID e3cd0dce9b1a251fc3322f746b5a7837ea5e7b09 # Parent a3035d56171d0677b8f3ab7754bf141a97e969e5 renamed "preconstr" option "need" diff -r a3035d56171d -r e3cd0dce9b1a doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Thu Mar 03 10:55:41 2011 +0100 +++ b/doc-src/Nitpick/nitpick.tex Thu Mar 03 11:20:48 2011 +0100 @@ -2465,17 +2465,17 @@ {\small See also \textit{debug} (\S\ref{output-format}).} -\opargboolorsmart{preconstr}{term}{dont\_preconstr} -Specifies whether a datatype value should be preconstructed, meaning Nitpick +\opargboolorsmart{need}{term}{dont\_need} +Specifies whether a datatype value is required by the problem, meaning Nitpick will reserve a Kodkod atom for it. If a value must necessarily belong to the -subset of representable values that approximates a datatype, preconstructing -it can speed up the search significantly, especially for high cardinalities. By -default, Nitpick inspects the conjecture to infer terms that can be -preconstructed. - -\opsmart{preconstr}{dont\_preconstr} -Specifies the default preconstruction setting to use. This can be overridden on -a per-term basis using the \textit{preconstr}~\qty{term} option described above. +subset of representable values that approximates a datatype, specifying it can +speed up the search significantly, especially for high cardinalities. By +default, Nitpick inspects the conjecture to infer needed datatype values. + +\opsmart{need}{dont\_need} +Specifies the default needed datatype value setting to use. This can be +overridden on a per-term basis using the \textit{preconstr}~\qty{term} option +described above. \opsmart{total\_consts}{partial\_consts} Specifies whether constants occurring in the problem other than constructors can diff -r a3035d56171d -r e3cd0dce9b1a src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 10:55:41 2011 +0100 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 11:20:48 2011 +0100 @@ -39,7 +39,7 @@ stds = stds, wfs = [], user_axioms = NONE, debug = false, whacks = [], binary_ints = SOME false, destroy_constrs = true, specialize = false, star_linear_preds = false, total_consts = NONE, - preconstrs = [], tac_timeout = NONE, evals = [], case_names = case_names, + needs = [], tac_timeout = NONE, evals = [], case_names = case_names, def_tables = def_tables, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_table, choice_spec_table = choice_spec_table, diff -r a3035d56171d -r e3cd0dce9b1a src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 03 10:55:41 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 03 11:20:48 2011 +0100 @@ -35,7 +35,7 @@ specialize: bool, star_linear_preds: bool, total_consts: bool option, - preconstrs: (term option * bool option) list, + needs: (term option * bool option) list, peephole_optim: bool, datatype_sym_break: int, kodkod_sym_break: int, @@ -110,7 +110,7 @@ specialize: bool, star_linear_preds: bool, total_consts: bool option, - preconstrs: (term option * bool option) list, + needs: (term option * bool option) list, peephole_optim: bool, datatype_sym_break: int, kodkod_sym_break: int, @@ -199,7 +199,7 @@ fun check_constr_nut (Construct (_, _, _, us)) = List.app check_constr_nut us | check_constr_nut _ = - error "The \"preconstr\" option requires a constructor term." + error "The \"need\" option requires a constructor term." fun pick_them_nits_in_term deadline state (params : params) auto i n step subst assm_ts orig_t = @@ -217,7 +217,7 @@ boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord, user_axioms, assms, whacks, merge_type_vars, binary_ints, destroy_constrs, specialize, star_linear_preds, - total_consts, preconstrs, peephole_optim, datatype_sym_break, + total_consts, needs, peephole_optim, datatype_sym_break, kodkod_sym_break, tac_timeout, max_threads, show_datatypes, show_consts, evals, formats, atomss, max_potential, max_genuine, check_potential, check_genuine, batch_size, ...} = params @@ -258,7 +258,7 @@ o Date.fromTimeLocal o Time.now) val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) else orig_t - val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs + val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs val tfree_table = if merge_type_vars then merged_type_var_table_for_terms thy conj_ts else [] @@ -266,8 +266,8 @@ val neg_t = neg_t |> merge_tfrees val assm_ts = assm_ts |> map merge_tfrees val evals = evals |> map merge_tfrees - val preconstrs = preconstrs |> map (apfst (Option.map merge_tfrees)) - val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs + val needs = needs |> map (apfst (Option.map merge_tfrees)) + val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs val original_max_potential = max_potential val original_max_genuine = max_genuine val max_bisim_depth = fold Integer.max bisim_depths ~1 @@ -289,7 +289,7 @@ whacks = whacks, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, star_linear_preds = star_linear_preds, total_consts = total_consts, - preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals, + needs = needs, tac_timeout = tac_timeout, evals = evals, case_names = case_names, def_tables = def_tables, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_table, @@ -302,7 +302,7 @@ val real_frees = fold Term.add_frees conj_ts [] val _ = null (fold Term.add_tvars conj_ts []) orelse error "Nitpick cannot handle goals with schematic type variables." - val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms, + val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize) = preprocess_formulas hol_ctxt assm_ts neg_t val got_all_user_axioms = @@ -332,8 +332,8 @@ val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq) val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq) - val preconstr_us = preconstr_ts |> map (nut_from_term hol_ctxt Eq) - val _ = List.app check_constr_nut preconstr_us + val need_us = need_ts |> map (nut_from_term hol_ctxt Eq) + val _ = List.app check_constr_nut need_us val (free_names, const_names) = fold add_free_and_const_names (nondef_us @ def_us) ([], []) val (sel_names, nonsel_names) = @@ -526,8 +526,8 @@ def_us |> map (choose_reps_in_nut scope unsound rep_table true) val nondef_us = nondef_us |> map (choose_reps_in_nut scope unsound rep_table false) - val preconstr_us = - preconstr_us |> map (choose_reps_in_nut scope unsound rep_table false) + val need_us = + need_us |> map (choose_reps_in_nut scope unsound rep_table false) (* val _ = List.app (print_g o string_for_nut ctxt) (free_names @ sel_names @ nonsel_names @ @@ -541,8 +541,7 @@ rename_free_vars nonsel_names pool rel_table val nondef_us = nondef_us |> map (rename_vars_in_nut pool rel_table) val def_us = def_us |> map (rename_vars_in_nut pool rel_table) - val preconstr_us = - preconstr_us |> map (rename_vars_in_nut pool rel_table) + val need_us = need_us |> map (rename_vars_in_nut pool rel_table) val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us val def_fs = map (kodkod_formula_from_nut ofs kk) def_us val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True @@ -568,7 +567,7 @@ val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels val dtype_axioms = - declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us + declarative_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break bits ofs kk rel_table datatypes val declarative_axioms = plain_axioms @ dtype_axioms val univ_card = Int.max (univ_card nat_card int_card main_j0 diff -r a3035d56171d -r e3cd0dce9b1a src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 03 10:55:41 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 03 11:20:48 2011 +0100 @@ -28,7 +28,7 @@ specialize: bool, star_linear_preds: bool, total_consts: bool option, - preconstrs: (term option * bool option) list, + needs: (term option * bool option) list, tac_timeout: Time.time option, evals: term list, case_names: (string * int) list, @@ -261,7 +261,7 @@ specialize: bool, star_linear_preds: bool, total_consts: bool option, - preconstrs: (term option * bool option) list, + needs: (term option * bool option) list, tac_timeout: Time.time option, evals: term list, case_names: (string * int) list, diff -r a3035d56171d -r e3cd0dce9b1a src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 10:55:41 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 11:20:48 2011 +0100 @@ -59,7 +59,7 @@ ("specialize", "true"), ("star_linear_preds", "true"), ("total_consts", "smart"), - ("preconstr", "smart"), + ("need", "smart"), ("peephole_optim", "true"), ("datatype_sym_break", "5"), ("kodkod_sym_break", "15"), @@ -93,7 +93,7 @@ ("dont_specialize", "specialize"), ("dont_star_linear_preds", "star_linear_preds"), ("partial_consts", "total_consts"), - ("dont_preconstr", "preconstr"), + ("dont_need", "need"), ("no_peephole_optim", "peephole_optim"), ("no_debug", "debug"), ("quiet", "verbose"), @@ -109,8 +109,8 @@ member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse exists (fn p => String.isPrefix (p ^ " ") s) ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize", - "mono", "non_mono", "std", "non_std", "wf", "non_wf", "preconstr", - "dont_preconstr", "format", "atoms"] + "mono", "non_mono", "std", "non_std", "wf", "non_wf", "need", + "dont_need", "format", "atoms"] fun check_raw_param (s, _) = if is_known_raw_param s then () @@ -256,8 +256,7 @@ val specialize = lookup_bool "specialize" val star_linear_preds = lookup_bool "star_linear_preds" val total_consts = lookup_bool_option "total_consts" - val preconstrs = - lookup_bool_option_assigns read_term_polymorphic "preconstr" + val needs = lookup_bool_option_assigns read_term_polymorphic "need" val peephole_optim = lookup_bool "peephole_optim" val datatype_sym_break = lookup_int "datatype_sym_break" val kodkod_sym_break = lookup_int "kodkod_sym_break" @@ -289,7 +288,7 @@ merge_type_vars = merge_type_vars, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, star_linear_preds = star_linear_preds, total_consts = total_consts, - preconstrs = preconstrs, peephole_optim = peephole_optim, + needs = needs, peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break, kodkod_sym_break = kodkod_sym_break, timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads, diff -r a3035d56171d -r e3cd0dce9b1a src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 10:55:41 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 11:20:48 2011 +0100 @@ -1478,8 +1478,8 @@ "malformed Kodkod formula") end -fun preconstructed_value_axioms_for_datatype [] _ _ _ = [] - | preconstructed_value_axioms_for_datatype preconstr_us ofs kk +fun needed_value_axioms_for_datatype [] _ _ _ = [] + | needed_value_axioms_for_datatype need_us ofs kk ({typ, card, constrs, ...} : datatype_spec) = let fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) = @@ -1507,10 +1507,9 @@ else accum) | aux u = - raise NUT ("Nitpick_Kodkod.preconstructed_value_axioms_for_datatype\ - \.aux", [u]) + raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u]) in - case SOME (index_seq 0 card, []) |> fold aux preconstr_us of + case SOME (index_seq 0 card, []) |> fold aux need_us of SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk) | NONE => [KK.False] end @@ -1654,14 +1653,14 @@ nfas dtypes) end -fun is_datatype_in_preconstructed_value T (Construct (_, T', _, us)) = - T = T' orelse exists (is_datatype_in_preconstructed_value T) us - | is_datatype_in_preconstructed_value _ _ = false +fun is_datatype_in_needed_value T (Construct (_, T', _, us)) = + T = T' orelse exists (is_datatype_in_needed_value T) us + | is_datatype_in_needed_value _ _ = false val min_sym_break_card = 7 -fun sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us - datatype_sym_break kk rel_table nfas dtypes = +fun sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break + kk rel_table nfas dtypes = if datatype_sym_break = 0 then [] else @@ -1673,8 +1672,7 @@ o binder_types o snd o #const) constrs) |> filter_out (fn {typ, ...} => - exists (is_datatype_in_preconstructed_value typ) - preconstr_us) + exists (is_datatype_in_needed_value typ) need_us) |> (fn dtypes' => dtypes' |> length dtypes' > datatype_sym_break ? (sort (datatype_ord o swap) @@ -1779,7 +1777,7 @@ partition_axioms_for_datatype j0 kk rel_table dtype end -fun declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us +fun declarative_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break bits ofs kk rel_table dtypes = let val nfas = @@ -1788,9 +1786,9 @@ |> strongly_connected_sub_nfas in acyclicity_axioms_for_datatypes kk nfas @ - maps (preconstructed_value_axioms_for_datatype preconstr_us ofs kk) dtypes @ - sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us - datatype_sym_break kk rel_table nfas dtypes @ + maps (needed_value_axioms_for_datatype need_us ofs kk) dtypes @ + sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break + kk rel_table nfas dtypes @ maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table) dtypes end diff -r a3035d56171d -r e3cd0dce9b1a src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 03 10:55:41 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 03 11:20:48 2011 +0100 @@ -862,7 +862,7 @@ fun reconstruct_hol_model {show_datatypes, show_consts} ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms, debug, whacks, binary_ints, destroy_constrs, specialize, - star_linear_preds, total_consts, preconstrs, tac_timeout, + star_linear_preds, total_consts, needs, tac_timeout, evals, case_names, def_tables, nondef_table, user_nondefs, simp_table, psimp_table, choice_spec_table, intro_table, ground_thm_table, ersatz_table, skolems, special_funs, @@ -880,7 +880,7 @@ whacks = whacks, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, star_linear_preds = star_linear_preds, total_consts = total_consts, - preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals, + needs = needs, tac_timeout = tac_timeout, evals = evals, case_names = case_names, def_tables = def_tables, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_table, diff -r a3035d56171d -r e3cd0dce9b1a src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 10:55:41 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 11:20:48 2011 +0100 @@ -1244,7 +1244,7 @@ fun preprocess_formulas (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes, - preconstrs, ...}) assm_ts neg_t = + needs, ...}) assm_ts neg_t = let val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) = neg_t |> unfold_defs_in_term hol_ctxt @@ -1281,18 +1281,17 @@ #> close_form #> Term.map_abs_vars shortest_name val nondef_ts = nondef_ts |> map (do_middle false) - val preconstr_ts = - (* FIXME: Implement preconstruction inference. *) - preconstrs - |> map_filter (fn (SOME t, SOME true) => - SOME (t |> unfold_defs_in_term hol_ctxt - |> do_middle false) - | _ => NONE) + val need_ts = + (* FIXME: Implement inference. *) + needs |> map_filter (fn (SOME t, SOME true) => + SOME (t |> unfold_defs_in_term hol_ctxt + |> do_middle false) + | _ => NONE) val nondef_ts = nondef_ts |> map (do_tail false) val def_ts = def_ts |> map (do_middle true #> do_tail true) in - (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms, - no_poly_user_axioms, binarize) + (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, no_poly_user_axioms, + binarize) end end;