--- a/NEWS Thu Dec 01 13:34:13 2011 +0100
+++ b/NEWS Thu Dec 01 13:34:14 2011 +0100
@@ -147,7 +147,7 @@
affecting 'rat' and 'real'.
* Sledgehammer:
- - Added "lam_trans" option.
+ - Added "lam_trans" and "minimize" options.
- Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
* Metis:
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 01 13:34:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 01 13:34:14 2011 +0100
@@ -96,6 +96,7 @@
("isar_proof", "false"),
("isar_shrink_factor", "1"),
("slice", "true"),
+ ("minimize", "smart"),
("preplay_timeout", "4")]
val alias_params =
@@ -107,7 +108,8 @@
("non_blocking", "blocking"),
("unsound", "sound"),
("no_isar_proof", "isar_proof"),
- ("dont_slice", "slice")]
+ ("dont_slice", "slice"),
+ ("dont_minimize", "minimize")]
val params_for_minimize =
["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
@@ -290,6 +292,8 @@
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val slice = mode <> Auto_Try andalso lookup_bool "slice"
+ val minimize =
+ if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
val timeout =
(if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
val preplay_timeout =
@@ -302,8 +306,9 @@
lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
max_relevant = max_relevant, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
- preplay_timeout = preplay_timeout, expect = expect}
+ isar_shrink_factor = isar_shrink_factor, slice = slice,
+ minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
+ expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 01 13:34:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 01 13:34:14 2011 +0100
@@ -66,7 +66,8 @@
max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slice = false,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
+ minimize = SOME false, timeout = timeout,
+ preplay_timeout = preplay_timeout, expect = ""}
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 01 13:34:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 01 13:34:14 2011 +0100
@@ -34,6 +34,7 @@
isar_proof: bool,
isar_shrink_factor: int,
slice: bool,
+ minimize: bool option,
timeout: Time.time,
preplay_timeout: Time.time,
expect: string}
@@ -297,6 +298,7 @@
isar_proof: bool,
isar_shrink_factor: int,
slice: bool,
+ minimize: bool option,
timeout: Time.time,
preplay_timeout: Time.time,
expect: string}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 01 13:34:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 01 13:34:14 2011 +0100
@@ -75,8 +75,8 @@
fun adjust_reconstructor_params override_params
({debug, verbose, overlord, blocking, provers, type_enc, sound,
lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
- max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout,
- preplay_timeout, expect} : params) =
+ max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
+ minimize, timeout, preplay_timeout, expect} : params) =
let
fun lookup_override name default_value =
case AList.lookup (op =) override_params name of
@@ -93,11 +93,13 @@
relevance_thresholds = relevance_thresholds,
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
- preplay_timeout = preplay_timeout, expect = expect}
+ isar_shrink_factor = isar_shrink_factor, slice = slice,
+ minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
+ expect = expect}
end
-fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
+fun minimize ctxt mode name
+ (params as {debug, verbose, isar_proof, minimize, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
(result as {outcome, used_facts, run_time, preplay, message,
message_tail} : prover_result) =
@@ -106,7 +108,7 @@
else
let
val num_facts = length used_facts
- val ((minimize, (minimize_name, params)), preplay) =
+ val ((perhaps_minimize, (minimize_name, params)), preplay) =
if mode = Normal then
if num_facts >= Config.get ctxt auto_minimize_min_facts then
((true, (name, params)), preplay)
@@ -116,10 +118,10 @@
0.001
* Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
<= Config.get ctxt auto_minimize_max_time
- val prover_fast_enough = can_min_fast_enough run_time
+ fun prover_fast_enough () = can_min_fast_enough run_time
in
if isar_proof then
- ((prover_fast_enough, (name, params)), preplay)
+ ((prover_fast_enough (), (name, params)), preplay)
else
let val preplay = preplay () in
(case preplay of
@@ -130,13 +132,14 @@
adjust_reconstructor_params
override_params params))
else
- (prover_fast_enough, (name, params))
- | _ => (prover_fast_enough, (name, params)),
+ (prover_fast_enough (), (name, params))
+ | _ => (prover_fast_enough (), (name, params)),
K preplay)
end
end
else
((false, (name, params)), preplay)
+ val minimize = minimize |> the_default perhaps_minimize
val (used_facts, (preplay, message, _)) =
if minimize then
minimize_facts minimize_name params (not verbose) subgoal