--- 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
--- 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 = [],
--- 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 @@
\<and> (\<forall>u. b = u \<longrightarrow> 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 \<Rightarrow> nat \<Rightarrow> nat" where
--- 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
--- 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 []
--- 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,
--- 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,
--- 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}
--- 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 =