1.1 --- a/doc-src/Nitpick/nitpick.tex Sat Apr 24 17:48:21 2010 +0200
1.2 +++ b/doc-src/Nitpick/nitpick.tex Sun Apr 25 00:10:30 2010 +0200
1.3 @@ -428,9 +428,6 @@
1.4 $\mathit{sym}.y$ are simply the bound variables $x$ and $y$
1.5 from \textit{sym}'s definition.
1.6
1.7 -Although skolemization is a useful optimization, you can disable it by invoking
1.8 -Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details.
1.9 -
1.10 \subsection{Natural Numbers and Integers}
1.11 \label{natural-numbers-and-integers}
1.12
1.13 @@ -2199,9 +2196,6 @@
1.14 formula and usually help us to understand why the counterexample falsifies the
1.15 formula.
1.16
1.17 -\nopagebreak
1.18 -{\small See also \textit{skolemize} (\S\ref{optimizations}).}
1.19 -
1.20 \opfalse{show\_datatypes}{hide\_datatypes}
1.21 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
1.22 be displayed as part of counterexamples. Such subsets are sometimes helpful when
1.23 @@ -2451,15 +2445,6 @@
1.24 {\small See also \textit{debug} (\S\ref{output-format}) and
1.25 \textit{show\_consts} (\S\ref{output-format}).}
1.26
1.27 -\optrue{skolemize}{dont\_skolemize}
1.28 -Specifies whether the formula should be skolemized. For performance reasons,
1.29 -(positive) $\forall$-quanti\-fiers that occur in the scope of a higher-order
1.30 -(positive) $\exists$-quanti\-fier are left unchanged.
1.31 -
1.32 -\nopagebreak
1.33 -{\small See also \textit{debug} (\S\ref{output-format}) and
1.34 -\textit{show\_skolems} (\S\ref{output-format}).}
1.35 -
1.36 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
1.37 Specifies whether Nitpick should use Kodkod's transitive closure operator to
1.38 encode non-well-founded ``linear inductive predicates,'' i.e., inductive
2.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Sat Apr 24 17:48:21 2010 +0200
2.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Sun Apr 25 00:10:30 2010 +0200
2.3 @@ -21,9 +21,9 @@
2.4 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
2.5 stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
2.6 binary_ints = SOME false, destroy_constrs = false, specialize = false,
2.7 - skolemize = false, star_linear_preds = false, uncurry = false,
2.8 - fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [],
2.9 - def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [],
2.10 + star_linear_preds = false, fast_descrs = false, tac_timeout = NONE,
2.11 + evals = [], case_names = [], def_table = def_table,
2.12 + nondef_table = Symtab.empty, user_nondefs = [],
2.13 simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
2.14 choice_spec_table = Symtab.empty, intro_table = Symtab.empty,
2.15 ground_thm_table = Inttab.empty, ersatz_table = [],
3.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Sat Apr 24 17:48:21 2010 +0200
3.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Sun Apr 25 00:10:30 2010 +0200
3.3 @@ -73,8 +73,6 @@
3.4 \<and> (\<forall>u. b = u \<longrightarrow> f3 b b u b b = f3 u u b u u)"
3.5 nitpick [expect = none]
3.6 nitpick [dont_specialize, expect = none]
3.7 -nitpick [dont_skolemize, expect = none]
3.8 -nitpick [dont_specialize, dont_skolemize, expect = none]
3.9 sorry
3.10
3.11 function f4 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
4.1 --- a/src/HOL/Tools/Nitpick/HISTORY Sat Apr 24 17:48:21 2010 +0200
4.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Sun Apr 25 00:10:30 2010 +0200
4.3 @@ -16,8 +16,9 @@
4.4 * Fixed soundness bug related to higher-order constructors
4.5 * Added cache to speed up repeated Kodkod invocations on the same problems
4.6 * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
4.7 - "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
4.8 - * Removed "sym_break", "flatten_prop", "sharing_depth", and "uncurry" options
4.9 + "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
4.10 + * Removed "skolemize", "uncurry", "sym_break", "flatten_prop", and
4.11 + "sharing_depth" options
4.12
4.13 Version 2009-1
4.14
5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 17:48:21 2010 +0200
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 25 00:10:30 2010 +0200
5.3 @@ -32,7 +32,6 @@
5.4 binary_ints: bool option,
5.5 destroy_constrs: bool,
5.6 specialize: bool,
5.7 - skolemize: bool,
5.8 star_linear_preds: bool,
5.9 fast_descrs: bool,
5.10 peephole_optim: bool,
5.11 @@ -104,7 +103,6 @@
5.12 binary_ints: bool option,
5.13 destroy_constrs: bool,
5.14 specialize: bool,
5.15 - skolemize: bool,
5.16 star_linear_preds: bool,
5.17 fast_descrs: bool,
5.18 peephole_optim: bool,
5.19 @@ -192,7 +190,7 @@
5.20 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
5.21 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
5.22 verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
5.23 - destroy_constrs, specialize, skolemize, star_linear_preds, fast_descrs,
5.24 + destroy_constrs, specialize, star_linear_preds, fast_descrs,
5.25 peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes,
5.26 show_consts, evals, formats, max_potential, max_genuine,
5.27 check_potential, check_genuine, batch_size, ...} =
5.28 @@ -262,15 +260,14 @@
5.29 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
5.30 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
5.31 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
5.32 - specialize = specialize, skolemize = skolemize,
5.33 - star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
5.34 - tac_timeout = tac_timeout, evals = evals, case_names = case_names,
5.35 - def_table = def_table, nondef_table = nondef_table,
5.36 - user_nondefs = user_nondefs, simp_table = simp_table,
5.37 - psimp_table = psimp_table, choice_spec_table = choice_spec_table,
5.38 - intro_table = intro_table, ground_thm_table = ground_thm_table,
5.39 - ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
5.40 - special_funs = Unsynchronized.ref [],
5.41 + specialize = specialize, star_linear_preds = star_linear_preds,
5.42 + fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
5.43 + case_names = case_names, def_table = def_table,
5.44 + nondef_table = nondef_table, user_nondefs = user_nondefs,
5.45 + simp_table = simp_table, psimp_table = psimp_table,
5.46 + choice_spec_table = choice_spec_table, intro_table = intro_table,
5.47 + ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
5.48 + skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
5.49 unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
5.50 constr_cache = Unsynchronized.ref []}
5.51 val frees = Term.add_frees assms_t []
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 24 17:48:21 2010 +0200
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 25 00:10:30 2010 +0200
6.3 @@ -25,7 +25,6 @@
6.4 binary_ints: bool option,
6.5 destroy_constrs: bool,
6.6 specialize: bool,
6.7 - skolemize: bool,
6.8 star_linear_preds: bool,
6.9 fast_descrs: bool,
6.10 tac_timeout: Time.time option,
6.11 @@ -235,7 +234,6 @@
6.12 binary_ints: bool option,
6.13 destroy_constrs: bool,
6.14 specialize: bool,
6.15 - skolemize: bool,
6.16 star_linear_preds: bool,
6.17 fast_descrs: bool,
6.18 tac_timeout: Time.time option,
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 17:48:21 2010 +0200
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Apr 25 00:10:30 2010 +0200
7.3 @@ -55,7 +55,6 @@
7.4 ("binary_ints", "smart"),
7.5 ("destroy_constrs", "true"),
7.6 ("specialize", "true"),
7.7 - ("skolemize", "true"),
7.8 ("star_linear_preds", "true"),
7.9 ("fast_descrs", "true"),
7.10 ("peephole_optim", "true"),
7.11 @@ -89,7 +88,6 @@
7.12 ("unary_ints", "binary_ints"),
7.13 ("dont_destroy_constrs", "destroy_constrs"),
7.14 ("dont_specialize", "specialize"),
7.15 - ("dont_skolemize", "skolemize"),
7.16 ("dont_star_linear_preds", "star_linear_preds"),
7.17 ("full_descrs", "fast_descrs"),
7.18 ("no_peephole_optim", "peephole_optim"),
7.19 @@ -250,7 +248,6 @@
7.20 val binary_ints = lookup_bool_option "binary_ints"
7.21 val destroy_constrs = lookup_bool "destroy_constrs"
7.22 val specialize = lookup_bool "specialize"
7.23 - val skolemize = lookup_bool "skolemize"
7.24 val star_linear_preds = lookup_bool "star_linear_preds"
7.25 val fast_descrs = lookup_bool "fast_descrs"
7.26 val peephole_optim = lookup_bool "peephole_optim"
7.27 @@ -281,9 +278,9 @@
7.28 user_axioms = user_axioms, assms = assms,
7.29 merge_type_vars = merge_type_vars, binary_ints = binary_ints,
7.30 destroy_constrs = destroy_constrs, specialize = specialize,
7.31 - skolemize = skolemize, star_linear_preds = star_linear_preds,
7.32 - fast_descrs = fast_descrs, peephole_optim = peephole_optim,
7.33 - timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads,
7.34 + star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
7.35 + peephole_optim = peephole_optim, timeout = timeout,
7.36 + tac_timeout = tac_timeout, max_threads = max_threads,
7.37 show_skolems = show_skolems, show_datatypes = show_datatypes,
7.38 show_consts = show_consts, formats = formats, evals = evals,
7.39 max_potential = max_potential, max_genuine = max_genuine,
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 17:48:21 2010 +0200
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Apr 25 00:10:30 2010 +0200
8.3 @@ -843,8 +843,8 @@
8.4 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
8.5 ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
8.6 debug, binary_ints, destroy_constrs, specialize,
8.7 - skolemize, star_linear_preds, fast_descrs, tac_timeout,
8.8 - evals, case_names, def_table, nondef_table, user_nondefs,
8.9 + star_linear_preds, fast_descrs, tac_timeout, evals,
8.10 + case_names, def_table, nondef_table, user_nondefs,
8.11 simp_table, psimp_table, choice_spec_table, intro_table,
8.12 ground_thm_table, ersatz_table, skolems, special_funs,
8.13 unrolled_preds, wf_cache, constr_cache},
8.14 @@ -858,16 +858,16 @@
8.15 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
8.16 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
8.17 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
8.18 - specialize = specialize, skolemize = skolemize,
8.19 - star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
8.20 - tac_timeout = tac_timeout, evals = evals, case_names = case_names,
8.21 - def_table = def_table, nondef_table = nondef_table,
8.22 - user_nondefs = user_nondefs, simp_table = simp_table,
8.23 - psimp_table = psimp_table, choice_spec_table = choice_spec_table,
8.24 - intro_table = intro_table, ground_thm_table = ground_thm_table,
8.25 - ersatz_table = ersatz_table, skolems = skolems,
8.26 - special_funs = special_funs, unrolled_preds = unrolled_preds,
8.27 - wf_cache = wf_cache, constr_cache = constr_cache}
8.28 + specialize = specialize, star_linear_preds = star_linear_preds,
8.29 + fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
8.30 + case_names = case_names, def_table = def_table,
8.31 + nondef_table = nondef_table, user_nondefs = user_nondefs,
8.32 + simp_table = simp_table, psimp_table = psimp_table,
8.33 + choice_spec_table = choice_spec_table, intro_table = intro_table,
8.34 + ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
8.35 + skolems = skolems, special_funs = special_funs,
8.36 + unrolled_preds = unrolled_preds, wf_cache = wf_cache,
8.37 + constr_cache = constr_cache}
8.38 val scope =
8.39 {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
8.40 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 17:48:21 2010 +0200
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sun Apr 25 00:10:30 2010 +0200
9.3 @@ -1226,14 +1226,15 @@
9.4
9.5 (** Preprocessor entry point **)
9.6
9.7 +val max_skolem_depth = 4
9.8 +
9.9 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
9.10 - boxes, skolemize, ...}) finitizes monos t =
9.11 + boxes, ...}) finitizes monos t =
9.12 let
9.13 - val skolem_depth = if skolemize then 4 else ~1
9.14 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
9.15 t |> unfold_defs_in_term hol_ctxt
9.16 |> close_form
9.17 - |> skolemize_term_and_more hol_ctxt skolem_depth
9.18 + |> skolemize_term_and_more hol_ctxt max_skolem_depth
9.19 |> specialize_consts_in_term hol_ctxt 0
9.20 |> axioms_for_term hol_ctxt
9.21 val binarize =