remove "skolemize" option from Nitpick, since Skolemization is always useful
authorblanchet
Sun Apr 25 00:10:30 2010 +0200 (2010-04-25)
changeset 363898228b3a4a2ba
parent 36388 30f7ce76712d
child 36390 eee4ee6a5cbe
remove "skolemize" option from Nitpick, since Skolemization is always useful
doc-src/Nitpick/nitpick.tex
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Nitpick_Examples/Special_Nits.thy
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     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 =