# HG changeset patch # User blanchet # Date 1281032270 -7200 # Node ID 3d1d928dce503f81d87619c44b84e44b82de6775 # Parent 10417cd47448c0940133dcd6d9e904e9daa57b33 added "whack" diff -r 10417cd47448 -r 3d1d928dce50 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Thu Aug 05 18:33:07 2010 +0200 +++ b/doc-src/Nitpick/nitpick.tex Thu Aug 05 20:17:50 2010 +0200 @@ -2494,6 +2494,14 @@ {\small See also \textit{debug} (\S\ref{output-format}).} +\opnodefault{whack}{term\_list} +Specifies a list of atomic terms (usually constants, but also free and schematic +variables) that should be taken as being $\unk$ (unknown). This can be useful to +reduce the size of the Kodkod problem if you can guess in advance that a +constant might not be needed to find a countermodel. + +{\small See also \textit{debug} (\S\ref{output-format}).} + \optrue{peephole\_optim}{no\_peephole\_optim} Specifies whether Nitpick should simplify the generated Kodkod formulas using a peephole optimizer. These optimizations can make a significant difference. diff -r 10417cd47448 -r 3d1d928dce50 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Aug 05 18:33:07 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Aug 05 20:17:50 2010 +0200 @@ -28,6 +28,7 @@ overlord: bool, user_axioms: bool option, assms: bool, + whacks: term list, merge_type_vars: bool, binary_ints: bool option, destroy_constrs: bool, @@ -101,6 +102,7 @@ overlord: bool, user_axioms: bool option, assms: bool, + whacks: term list, merge_type_vars: bool, binary_ints: bool option, destroy_constrs: bool, @@ -193,12 +195,12 @@ *) val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, - verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints, - destroy_constrs, specialize, star_linear_preds, fast_descrs, - 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 + verbose, overlord, user_axioms, assms, whacks, merge_type_vars, + binary_ints, destroy_constrs, specialize, star_linear_preds, + fast_descrs, 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 val state_ref = Unsynchronized.ref state val pprint = if auto then @@ -263,15 +265,16 @@ val (hol_ctxt as {wf_cache, ...}) = {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, - binary_ints = binary_ints, destroy_constrs = destroy_constrs, - specialize = specialize, star_linear_preds = star_linear_preds, - fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, - case_names = case_names, def_table = def_table, - nondef_table = nondef_table, user_nondefs = user_nondefs, - simp_table = simp_table, psimp_table = psimp_table, - choice_spec_table = choice_spec_table, intro_table = intro_table, - ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, - skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], + whacks = whacks, binary_ints = binary_ints, + destroy_constrs = destroy_constrs, specialize = specialize, + star_linear_preds = star_linear_preds, fast_descrs = fast_descrs, + tac_timeout = tac_timeout, evals = evals, case_names = case_names, + def_table = def_table, nondef_table = nondef_table, + user_nondefs = user_nondefs, simp_table = simp_table, + psimp_table = psimp_table, choice_spec_table = choice_spec_table, + intro_table = intro_table, ground_thm_table = ground_thm_table, + ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], + special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} val pseudo_frees = fold Term.add_frees assm_ts [] diff -r 10417cd47448 -r 3d1d928dce50 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 18:33:07 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 20:17:50 2010 +0200 @@ -22,6 +22,7 @@ wfs: (styp option * bool option) list, user_axioms: bool option, debug: bool, + whacks: term list, binary_ints: bool option, destroy_constrs: bool, specialize: bool, @@ -236,6 +237,7 @@ wfs: (styp option * bool option) list, user_axioms: bool option, debug: bool, + whacks: term list, binary_ints: bool option, destroy_constrs: bool, specialize: bool, @@ -1578,9 +1580,9 @@ val def_inline_threshold_for_booleans = 50 val def_inline_threshold_for_non_booleans = 20 -fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names, - def_table, ground_thm_table, ersatz_table, - ...}) = +fun unfold_defs_in_term + (hol_ctxt as {thy, ctxt, stds, whacks, fast_descrs, case_names, + def_table, ground_thm_table, ersatz_table, ...}) = let fun do_term depth Ts t = case t of @@ -1628,10 +1630,12 @@ (case strip_comb t of (Const x, ts) => do_const depth Ts t x ts | _ => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)) - | Free _ => t - | Var _ => t | Bound _ => t | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body) + | _ => if member (term_match thy) whacks t then + Const (@{const_name unknown}, fastype_of1 (Ts, t)) + else + t and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T = (Abs (Name.uu, body_type T, select_nth_constr_arg ctxt stds x (Bound 0) n res_T), []) @@ -1641,7 +1645,9 @@ select_nth_constr_arg_with_args depth Ts (@{const_name Quot}, rep_T --> abs_T) ts 0 rep_T and do_const depth Ts t (x as (s, T)) ts = - case AList.lookup (op =) ersatz_table s of + if member (term_match thy) whacks (Const x) then + Const (@{const_name unknown}, fastype_of1 (Ts, t)) + else case AList.lookup (op =) ersatz_table s of SOME s' => do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts | NONE => diff -r 10417cd47448 -r 3d1d928dce50 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Aug 05 18:33:07 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Aug 05 20:17:50 2010 +0200 @@ -101,7 +101,7 @@ fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) negated_params s orelse - member (op =) ["max", "show_all", "eval", "expect"] s orelse + member (op =) ["max", "show_all", "whack", "eval", "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", "format", @@ -214,13 +214,13 @@ case lookup name of NONE => NONE | SOME s => parse_time_option name s - val lookup_term_list = - AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt val read_type_polymorphic = Syntax.read_typ ctxt #> Logic.mk_type #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type val read_term_polymorphic = Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt) + val lookup_term_list_polymorphic = + AList.lookup (op =) raw_params #> these #> map read_term_polymorphic val read_const_polymorphic = read_term_polymorphic #> dest_Const val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1 val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1 @@ -240,6 +240,7 @@ val overlord = lookup_bool "overlord" val user_axioms = lookup_bool_option "user_axioms" val assms = lookup_bool "assms" + val whacks = lookup_term_list_polymorphic "whack" val merge_type_vars = lookup_bool "merge_type_vars" val binary_ints = lookup_bool_option "binary_ints" val destroy_constrs = lookup_bool "destroy_constrs" @@ -256,7 +257,7 @@ val show_consts = debug orelse lookup_bool "show_consts" val formats = lookup_ints_assigns read_term_polymorphic "format" 0 val atomss = lookup_strings_assigns read_type_polymorphic "atoms" - val evals = lookup_term_list "eval" + val evals = lookup_term_list_polymorphic "eval" val max_potential = if auto then 0 else Int.max (0, lookup_int "max_potential") val max_genuine = Int.max (0, lookup_int "max_genuine") @@ -273,7 +274,7 @@ boxes = boxes, finitizes = finitizes, monos = monos, stds = stds, wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify, debug = debug, verbose = verbose, overlord = overlord, - user_axioms = user_axioms, assms = assms, + user_axioms = user_axioms, assms = assms, whacks = whacks, merge_type_vars = merge_type_vars, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, star_linear_preds = star_linear_preds, fast_descrs = fast_descrs, diff -r 10417cd47448 -r 3d1d928dce50 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Aug 05 18:33:07 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Aug 05 20:17:50 2010 +0200 @@ -852,7 +852,7 @@ fun reconstruct_hol_model {show_datatypes, show_consts} ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms, - debug, binary_ints, destroy_constrs, specialize, + debug, whacks, binary_ints, destroy_constrs, specialize, star_linear_preds, fast_descrs, tac_timeout, evals, case_names, def_table, nondef_table, user_nondefs, simp_table, psimp_table, choice_spec_table, intro_table, @@ -868,17 +868,17 @@ val hol_ctxt = {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, - binary_ints = binary_ints, destroy_constrs = destroy_constrs, - specialize = specialize, star_linear_preds = star_linear_preds, - fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, - case_names = case_names, def_table = def_table, - nondef_table = nondef_table, user_nondefs = user_nondefs, - simp_table = simp_table, psimp_table = psimp_table, - choice_spec_table = choice_spec_table, intro_table = intro_table, - ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, - skolems = skolems, special_funs = special_funs, - unrolled_preds = unrolled_preds, wf_cache = wf_cache, - constr_cache = constr_cache} + whacks = whacks, binary_ints = binary_ints, + destroy_constrs = destroy_constrs, specialize = specialize, + star_linear_preds = star_linear_preds, fast_descrs = fast_descrs, + tac_timeout = tac_timeout, evals = evals, case_names = case_names, + def_table = def_table, nondef_table = nondef_table, + user_nondefs = user_nondefs, simp_table = simp_table, + psimp_table = psimp_table, choice_spec_table = choice_spec_table, + intro_table = intro_table, ground_thm_table = ground_thm_table, + ersatz_table = ersatz_table, skolems = skolems, + special_funs = special_funs, unrolled_preds = unrolled_preds, + wf_cache = wf_cache, constr_cache = constr_cache} val scope = {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns, bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}