# HG changeset patch # User blanchet # Date 1272147030 -7200 # Node ID 8228b3a4a2baca7c53001488eb15109b1ceb5ef7 # Parent 30f7ce76712da877b078f207a22a9c8e7981a4d2 remove "skolemize" option from Nitpick, since Skolemization is always useful diff -r 30f7ce76712d -r 8228b3a4a2ba doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Sat Apr 24 17:48:21 2010 +0200 +++ b/doc-src/Nitpick/nitpick.tex Sun Apr 25 00:10:30 2010 +0200 @@ -428,9 +428,6 @@ $\mathit{sym}.y$ are simply the bound variables $x$ and $y$ from \textit{sym}'s definition. -Although skolemization is a useful optimization, you can disable it by invoking -Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details. - \subsection{Natural Numbers and Integers} \label{natural-numbers-and-integers} @@ -2199,9 +2196,6 @@ formula and usually help us to understand why the counterexample falsifies the formula. -\nopagebreak -{\small See also \textit{skolemize} (\S\ref{optimizations}).} - \opfalse{show\_datatypes}{hide\_datatypes} Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should be displayed as part of counterexamples. Such subsets are sometimes helpful when @@ -2451,15 +2445,6 @@ {\small See also \textit{debug} (\S\ref{output-format}) and \textit{show\_consts} (\S\ref{output-format}).} -\optrue{skolemize}{dont\_skolemize} -Specifies whether the formula should be skolemized. For performance reasons, -(positive) $\forall$-quanti\-fiers that occur in the scope of a higher-order -(positive) $\exists$-quanti\-fier are left unchanged. - -\nopagebreak -{\small See also \textit{debug} (\S\ref{output-format}) and -\textit{show\_skolems} (\S\ref{output-format}).} - \optrue{star\_linear\_preds}{dont\_star\_linear\_preds} Specifies whether Nitpick should use Kodkod's transitive closure operator to encode non-well-founded ``linear inductive predicates,'' i.e., inductive diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Sat Apr 24 17:48:21 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Sun Apr 25 00:10:30 2010 +0200 @@ -21,9 +21,9 @@ {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, binary_ints = SOME false, destroy_constrs = false, specialize = false, - skolemize = false, star_linear_preds = false, uncurry = false, - fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [], - def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [], + star_linear_preds = false, fast_descrs = false, tac_timeout = NONE, + evals = [], case_names = [], def_table = def_table, + nondef_table = Symtab.empty, user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty, choice_spec_table = Symtab.empty, intro_table = Symtab.empty, ground_thm_table = Inttab.empty, ersatz_table = [], diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Nitpick_Examples/Special_Nits.thy --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Sat Apr 24 17:48:21 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Sun Apr 25 00:10:30 2010 +0200 @@ -73,8 +73,6 @@ \ (\u. b = u \ f3 b b u b b = f3 u u b u u)" nitpick [expect = none] nitpick [dont_specialize, expect = none] -nitpick [dont_skolemize, expect = none] -nitpick [dont_specialize, dont_skolemize, expect = none] sorry function f4 :: "nat \ nat \ nat" where diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Sat Apr 24 17:48:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/HISTORY Sun Apr 25 00:10:30 2010 +0200 @@ -16,8 +16,9 @@ * Fixed soundness bug related to higher-order constructors * Added cache to speed up repeated Kodkod invocations on the same problems * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to - "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light" - * Removed "sym_break", "flatten_prop", "sharing_depth", and "uncurry" options + "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light" + * Removed "skolemize", "uncurry", "sym_break", "flatten_prop", and + "sharing_depth" options Version 2009-1 diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 17:48:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 25 00:10:30 2010 +0200 @@ -32,7 +32,6 @@ binary_ints: bool option, destroy_constrs: bool, specialize: bool, - skolemize: bool, star_linear_preds: bool, fast_descrs: bool, peephole_optim: bool, @@ -104,7 +103,6 @@ binary_ints: bool option, destroy_constrs: bool, specialize: bool, - skolemize: bool, star_linear_preds: bool, fast_descrs: bool, peephole_optim: bool, @@ -192,7 +190,7 @@ 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, skolemize, star_linear_preds, fast_descrs, + destroy_constrs, specialize, star_linear_preds, 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, ...} = @@ -262,15 +260,14 @@ {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, skolemize = skolemize, - 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 [], + 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 frees = Term.add_frees assms_t [] diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 24 17:48:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 25 00:10:30 2010 +0200 @@ -25,7 +25,6 @@ binary_ints: bool option, destroy_constrs: bool, specialize: bool, - skolemize: bool, star_linear_preds: bool, fast_descrs: bool, tac_timeout: Time.time option, @@ -235,7 +234,6 @@ binary_ints: bool option, destroy_constrs: bool, specialize: bool, - skolemize: bool, star_linear_preds: bool, fast_descrs: bool, tac_timeout: Time.time option, diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 17:48:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Apr 25 00:10:30 2010 +0200 @@ -55,7 +55,6 @@ ("binary_ints", "smart"), ("destroy_constrs", "true"), ("specialize", "true"), - ("skolemize", "true"), ("star_linear_preds", "true"), ("fast_descrs", "true"), ("peephole_optim", "true"), @@ -89,7 +88,6 @@ ("unary_ints", "binary_ints"), ("dont_destroy_constrs", "destroy_constrs"), ("dont_specialize", "specialize"), - ("dont_skolemize", "skolemize"), ("dont_star_linear_preds", "star_linear_preds"), ("full_descrs", "fast_descrs"), ("no_peephole_optim", "peephole_optim"), @@ -250,7 +248,6 @@ val binary_ints = lookup_bool_option "binary_ints" val destroy_constrs = lookup_bool "destroy_constrs" val specialize = lookup_bool "specialize" - val skolemize = lookup_bool "skolemize" val star_linear_preds = lookup_bool "star_linear_preds" val fast_descrs = lookup_bool "fast_descrs" val peephole_optim = lookup_bool "peephole_optim" @@ -281,9 +278,9 @@ user_axioms = user_axioms, assms = assms, merge_type_vars = merge_type_vars, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, - skolemize = skolemize, star_linear_preds = star_linear_preds, - fast_descrs = fast_descrs, peephole_optim = peephole_optim, - timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads, + star_linear_preds = star_linear_preds, fast_descrs = fast_descrs, + peephole_optim = peephole_optim, timeout = timeout, + 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, diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 17:48:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Apr 25 00:10:30 2010 +0200 @@ -843,8 +843,8 @@ fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts} ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms, debug, binary_ints, destroy_constrs, specialize, - skolemize, star_linear_preds, fast_descrs, tac_timeout, - evals, case_names, def_table, nondef_table, user_nondefs, + 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, ground_thm_table, ersatz_table, skolems, special_funs, unrolled_preds, wf_cache, constr_cache}, @@ -858,16 +858,16 @@ {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, skolemize = skolemize, - 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} + 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} diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 17:48:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sun Apr 25 00:10:30 2010 +0200 @@ -1226,14 +1226,15 @@ (** Preprocessor entry point **) +val max_skolem_depth = 4 + fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs, - boxes, skolemize, ...}) finitizes monos t = + boxes, ...}) finitizes monos t = let - val skolem_depth = if skolemize then 4 else ~1 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) = t |> unfold_defs_in_term hol_ctxt |> close_form - |> skolemize_term_and_more hol_ctxt skolem_depth + |> skolemize_term_and_more hol_ctxt max_skolem_depth |> specialize_consts_in_term hol_ctxt 0 |> axioms_for_term hol_ctxt val binarize =