--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Aug 01 14:43:57 2014 +0200
@@ -318,8 +318,6 @@
(* Sledgehammer the given subgoal *)
-val default_minimize_prover = metisN
-
fun is_raw_param_relevant_for_minimize (name, _) = not (member (op =) params_not_for_minimize name)
fun string_of_raw_param (key, values) =
@@ -338,7 +336,7 @@
more_override_params
|> filter is_raw_param_relevant_for_minimize
|> map nice_string_of_raw_param
- |> (if prover_name = default_minimize_prover then I else cons prover_name)
+ |> cons prover_name
|> space_implode ", "
in
sledgehammerN ^ " " ^ minN ^ (if params = "" then "" else enclose " [" "]" params) ^
@@ -365,8 +363,7 @@
let
val ctxt = ctxt |> Config.put instantiate_inducts false
val i = the_default 1 opt_i
- val params =
- get_params Minimize thy (("provers", [default_minimize_prover]) :: override_params)
+ val params = get_params Minimize thy override_params
val goal = prop_of (#goal (Proof.goal state))
val facts = nearly_all_facts ctxt false fact_override Symtab.empty Termtab.empty [] [] goal
val learn = mash_learn_proof ctxt params goal facts
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Aug 01 14:43:57 2014 +0200
@@ -12,6 +12,7 @@
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step
+ val minimized_isar_step : Proof.context -> Time.time -> isar_step -> Time.time * isar_step
val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
isar_step -> isar_step
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200
@@ -68,11 +68,8 @@
val SledgehammerN : string
val str_of_mode : mode -> string
- val smtN : string
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
- val extract_proof_method : params -> proof_method -> string * (string * string list) list
- val is_proof_method : string -> bool
val is_atp : theory -> string -> bool
val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
val is_fact_chained : (('a * stature) * 'b) -> bool
@@ -80,9 +77,6 @@
((''a * stature) * 'b) list
val play_one_line_proof : mode -> Time.time -> ((string * 'a) * thm) list -> Proof.state -> int ->
proof_method -> proof_method list -> proof_method * play_outcome
- val isar_supported_prover_of : theory -> string -> string
- val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
- string -> proof_method * play_outcome -> 'a
val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
Proof.context
@@ -120,11 +114,6 @@
| str_of_mode Auto_Minimize = "Auto_Minimize"
| str_of_mode Minimize = "Minimize"
-val smtN = "smt"
-
-val proof_method_names = [metisN, smtN]
-val is_proof_method = member (op =) proof_method_names
-
val is_atp = member (op =) o supported_atps
type params =
@@ -197,17 +186,6 @@
Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
(if smt_proofs then [SMT2_Method] else [])
-fun extract_proof_method ({type_enc, lam_trans, ...} : params)
- (Metis_Method (type_enc', lam_trans')) =
- let
- val override_params =
- (if is_none type_enc' andalso is_none type_enc then []
- else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
- (if is_none lam_trans' andalso is_none lam_trans then []
- else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
- in (metisN, override_params) end
- | extract_proof_method _ SMT2_Method = (smtN, [])
-
fun preplay_methods timeout facts meths state i =
let
val {context = ctxt, facts = chained, goal} = Proof.goal state
@@ -242,26 +220,6 @@
end
end
-val canonical_isar_supported_prover = eN
-val z3N = "z3"
-
-fun isar_supported_prover_of thy name =
- if is_atp thy name orelse name = z3N then name
- else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover
- else name
-
-(* FIXME: See the analogous logic in the function "maybe_minimize" in
- "sledgehammer_prover_minimize.ML". *)
-fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay =
- let
- val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
- val (min_name, override_params) =
- (case preplay of
- (meth as Metis_Method _, Played _) =>
- if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
- | _ => (maybe_isar_name, []))
- in minimize_command override_params min_name end
-
val max_fact_instances = 10 (* FUDGE *)
fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
@@ -274,7 +232,6 @@
let
val thy = Proof_Context.theory_of ctxt
val (remote_provers, local_provers) =
- proof_method_names @
sort_strings (supported_atps thy) @
sort_strings (SMT2_Config.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200
@@ -132,9 +132,9 @@
val atp_important_message_keep_quotient = 25
fun run_atp mode name
- (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
- fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0,
- smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
+ ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
+ max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
+ slice, minimize, timeout, preplay_timeout, ...} : params)
minimize_command
({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -391,8 +391,7 @@
end
val one_line_params =
- (preplay, proof_banner mode name, used_facts,
- choose_minimize_command thy params minimize_command name preplay, subgoal,
+ (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal,
subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200
@@ -48,59 +48,17 @@
open Sledgehammer_Prover_ATP
open Sledgehammer_Prover_SMT2
-fun run_proof_method mode name (params as {timeout, type_enc, lam_trans, ...})
- minimize_command
- ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
- let
- val meth =
- if name = metisN then Metis_Method (type_enc, lam_trans)
- else if name = smtN then SMT2_Method
- else raise Fail ("unknown proof_method: " ^ quote name)
- val used_facts = facts |> map fst
- in
- (case play_one_line_proof (if mode = Minimize then Normal else mode) timeout facts state subgoal
- meth [meth] of
- play as (_, Played time) =>
- {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
- preplay = Lazy.value play,
- message = fn play =>
- let
- val ctxt = Proof.context_of state
- val (_, override_params) = extract_proof_method params meth
- val one_line_params =
- (play, proof_banner mode name, used_facts, minimize_command override_params name,
- subgoal, subgoal_count)
- val num_chained = length (#facts (Proof.goal state))
- in
- one_line_proof_text ctxt num_chained one_line_params
- end,
- message_tail = ""}
- | play =>
- let
- val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
- in
- {outcome = SOME failure, used_facts = [], used_from = [],
- run_time = Time.zeroTime, preplay = Lazy.value play,
- message = fn _ => string_of_atp_failure failure, message_tail = ""}
- end)
- end
-
fun is_prover_supported ctxt =
let val thy = Proof_Context.theory_of ctxt in
- is_proof_method orf is_atp thy orf is_smt2_prover ctxt
+ is_atp thy orf is_smt2_prover ctxt
end
fun is_prover_installed ctxt =
- is_proof_method orf is_smt2_prover ctxt orf
- is_atp_installed (Proof_Context.theory_of ctxt)
-
-val proof_method_default_max_facts = 20
+ is_smt2_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
fun default_max_facts_of_prover ctxt name =
let val thy = Proof_Context.theory_of ctxt in
- if is_proof_method name then
- proof_method_default_max_facts
- else if is_atp thy name then
+ if is_atp thy name then
fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
else if is_smt2_prover ctxt name then
SMT2_Solver.default_max_relevant ctxt name
@@ -110,8 +68,7 @@
fun get_prover ctxt mode name =
let val thy = Proof_Context.theory_of ctxt in
- if is_proof_method name then run_proof_method mode name
- else if is_atp thy name then run_atp mode name
+ if is_atp thy name then run_atp mode name
else if is_smt2_prover ctxt name then run_smt2_solver mode name
else error ("No such prover: " ^ name ^ ".")
end
@@ -278,30 +235,7 @@
(NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, ""))
end
-fun adjust_proof_method_params override_params
- ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
- uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
- max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, minimize, timeout,
- preplay_timeout, expect} : params) =
- let
- fun lookup_override name default_value =
- (case AList.lookup (op =) override_params name of
- SOME [s] => SOME s
- | _ => default_value)
- (* Only those options that proof_methods are interested in are considered here. *)
- val type_enc = lookup_override "type_enc" type_enc
- val lam_trans = lookup_override "lam_trans" lam_trans
- in
- {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
- provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
- uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
- max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
- max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
- end
-
-fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
+fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...})
({state, goal, subgoal, subgoal_count, ...} : prover_problem)
(result as {outcome, used_facts, used_from, run_time, preplay, message, message_tail} :
prover_result) =
@@ -309,26 +243,9 @@
result
else
let
- val thy = Proof_Context.theory_of ctxt
-
- val (minimize_name, params) =
- if mode = Normal then
- (case Lazy.force preplay of
- (meth as Metis_Method _, Played _) =>
- if isar_proofs = SOME true then
- (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
- itself. *)
- (isar_supported_prover_of thy name, params)
- else
- extract_proof_method params meth
- ||> (fn override_params => adjust_proof_method_params override_params params)
- | _ => (name, params))
- else
- (name, params)
-
val (used_facts, (preplay, message, _)) =
if minimize then
- minimize_facts do_learn minimize_name params
+ minimize_facts do_learn name params
(not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
goal (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from))
|>> Option.map (map fst)
@@ -344,7 +261,7 @@
fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem =
get_prover ctxt mode name params minimize_command problem
- |> maybe_minimize ctxt mode do_learn name params problem
+ |> maybe_minimize mode do_learn name params problem
fun run_minimize (params as {provers, ...}) do_learn i refs state =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200
@@ -207,8 +207,7 @@
goal)
val one_line_params =
- (preplay, proof_banner mode name, used_facts,
- choose_minimize_command thy params minimize_command name preplay, subgoal,
+ (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal,
subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in