--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 18 08:44:04 2012 +0200
@@ -367,7 +367,7 @@
handle List.Empty => error "No ATP available."
fun get_prover name =
(name, Sledgehammer_Minimize.get_minimizing_prover ctxt
- Sledgehammer_Provers.Normal name)
+ Sledgehammer_Provers.Normal (K ()) name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name
@@ -597,7 +597,7 @@
|> max_new_mono_instancesLST
|> max_mono_itersLST)
val minimize =
- Sledgehammer_Minimize.minimize_facts prover_name params
+ Sledgehammer_Minimize.minimize_facts (K ()) prover_name params
true 1 (Sledgehammer_Util.subgoal_count st)
val _ = log separator
val (used_facts, (preplay, message, message_tail)) =
--- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
@@ -90,7 +90,8 @@
facts
|> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
|> take (the max_facts)
- val res as {outcome, ...} = run_prover ctxt params prover facts goal
+ val res as {outcome, ...} =
+ run_prover_for_mash ctxt params prover facts goal
val _ = if is_none outcome then ok := !ok + 1 else ()
in str_of_res heading facts res end
val iter_s = prove iter_ok iterN iter_facts
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200
@@ -146,7 +146,7 @@
|> fold (add_isa_dep facts) isa_deps
|> map fix_name
in
- case run_prover ctxt params prover facts goal of
+ case run_prover_for_mash ctxt params prover facts goal of
{outcome = NONE, used_facts, ...} =>
used_facts |> map fst |> sort string_ord
| _ => isa_deps
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
@@ -25,8 +25,9 @@
val unescape_meta : string -> string
val unescape_metas : string -> string list
val extract_query : string -> string * string list
- val suggested_facts : string list -> fact list -> fact list
- val mesh_facts : int -> (fact list * fact list) list -> fact list
+ val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
+ val mesh_facts :
+ int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
val is_likely_tautology : Proof.context -> string -> thm -> bool
val is_too_meta : thm -> bool
val theory_ord : theory * theory -> order
@@ -35,7 +36,7 @@
Proof.context -> string -> theory -> status -> term list -> string list
val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
val goal_of_thm : theory -> thm -> thm
- val run_prover :
+ val run_prover_for_mash :
Proof.context -> params -> string -> fact list -> thm -> prover_result
val mash_RESET : Proof.context -> unit
val mash_INIT :
@@ -48,14 +49,14 @@
Proof.context -> bool -> int -> string list * string list -> string list
val mash_reset : Proof.context -> unit
val mash_could_suggest_facts : unit -> bool
- val mash_can_suggest_facts : unit -> bool
+ val mash_can_suggest_facts : Proof.context -> bool
val mash_suggest_facts :
- Proof.context -> params -> string -> int -> term list -> term -> fact list
- -> fact list * fact list
+ Proof.context -> params -> string -> int -> term list -> term
+ -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
val mash_learn_thy :
Proof.context -> params -> theory -> Time.time -> fact list -> string
val mash_learn_proof :
- Proof.context -> params -> term -> thm list -> fact list -> unit
+ Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
val relevant_facts :
Proof.context -> params -> string -> int -> fact_override -> term list
-> term -> fact list -> fact list
@@ -300,13 +301,13 @@
fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
-fun run_prover ctxt params prover facts goal =
+fun run_prover_for_mash ctxt params prover facts goal =
let
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
facts = facts |> map (apfst (apfst (fn name => name ())))
|> map Untranslated_Fact}
- val prover = get_minimizing_prover ctxt Normal prover
+ val prover = get_minimizing_prover ctxt Normal (K ()) prover
in prover params (K (K (K ""))) problem end
@@ -406,6 +407,15 @@
(*** High-level communication with MaSh ***)
+fun try_graph ctxt when def f =
+ f ()
+ handle Graph.CYCLES (cycle :: _) =>
+ (trace_msg ctxt (fn () =>
+ "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
+ | Graph.UNDEF name =>
+ (trace_msg ctxt (fn () =>
+ "Unknown fact " ^ quote name ^ " when " ^ when); def)
+
type mash_state =
{thys : bool Symtab.table,
fact_graph : unit Graph.T}
@@ -414,8 +424,8 @@
local
-fun mash_load (state as (true, _)) = state
- | mash_load _ =
+fun mash_load _ (state as (true, _)) = state
+ | mash_load ctxt _ =
let val path = mash_state_path () in
(true,
case try File.read_lines path of
@@ -431,7 +441,9 @@
val thys =
Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
|> fold (add_thy false) (unescape_metas incomp_thys)
- val fact_graph = Graph.empty |> fold add_fact_line fact_lines
+ val fact_graph =
+ try_graph ctxt "loading state file" Graph.empty (fn () =>
+ Graph.empty |> fold add_fact_line fact_lines)
in {thys = thys, fact_graph = fact_graph} end
| _ => empty_state)
end
@@ -456,10 +468,11 @@
in
-fun mash_map f =
- Synchronized.change global_state (mash_load ##> (f #> tap mash_save))
+fun mash_map ctxt f =
+ Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
-fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd)
+fun mash_get ctxt =
+ Synchronized.change_result global_state (mash_load ctxt #> `snd)
fun mash_reset ctxt =
Synchronized.change global_state (fn _ =>
@@ -469,17 +482,22 @@
end
fun mash_could_suggest_facts () = mash_home () <> ""
-fun mash_can_suggest_facts () = not (Graph.is_empty (#fact_graph (mash_get ())))
+fun mash_can_suggest_facts ctxt =
+ not (Graph.is_empty (#fact_graph (mash_get ctxt)))
-fun parents_wrt_facts facts fact_graph =
+fun parents_wrt_facts ctxt facts fact_graph =
let
val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph))
val facts =
- [] |> fold (cons o Thm.get_name_hint o snd) facts
- |> filter (Symtab.defined graph_facts)
- |> Graph.all_preds fact_graph
+ try_graph ctxt "when computing ancestor facts" [] (fn () =>
+ [] |> fold (cons o Thm.get_name_hint o snd) facts
+ |> filter (Symtab.defined graph_facts)
+ |> Graph.all_preds fact_graph)
val facts = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
- in fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals end
+ in
+ try_graph ctxt "when computing parent facts" [] (fn () =>
+ fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals)
+ end
(* Generate more suggestions than requested, because some might be thrown out
later for various reasons and "meshing" gives better results with some
@@ -493,8 +511,8 @@
concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
- val fact_graph = #fact_graph (mash_get ())
- val parents = parents_wrt_facts facts fact_graph
+ val fact_graph = #fact_graph (mash_get ctxt)
+ val parents = parents_wrt_facts ctxt facts fact_graph
val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
val suggs =
if Graph.is_empty fact_graph then []
@@ -511,13 +529,9 @@
fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
let
fun maybe_add_from from (accum as (parents, graph)) =
- (from :: parents, Graph.add_edge_acyclic (from, name) graph)
- handle Graph.CYCLES _ =>
- (trace_msg ctxt (fn () =>
- "Cycle between " ^ quote from ^ " and " ^ quote name); accum)
- | Graph.UNDEF _ =>
- (trace_msg ctxt (fn () => "Unknown node " ^ quote from); accum)
- val graph = graph |> Graph.new_node (name, ())
+ try_graph ctxt "updating graph" accum (fn () =>
+ (from :: parents, Graph.add_edge_acyclic (from, name) graph))
+ val graph = graph |> Graph.default_node (name, ())
val (parents, graph) = ([], graph) |> fold maybe_add_from parents
val (deps, graph) = ([], graph) |> fold maybe_add_from deps
in ((name, parents, feats, deps) :: upds, graph) end
@@ -532,7 +546,7 @@
val prover = hd provers
fun timed_out frac =
Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
- val {fact_graph, ...} = mash_get ()
+ val {fact_graph, ...} = mash_get ctxt
val new_facts =
facts |> filter_out (is_fact_in_graph fact_graph)
|> sort (thm_ord o pairself snd)
@@ -554,7 +568,7 @@
val deps = isabelle_dependencies_of all_names th
val upd = (name, parents, feats, deps)
in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
- val parents = parents_wrt_facts facts fact_graph
+ val parents = parents_wrt_facts ctxt facts fact_graph
val ((_, upds), _) =
((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
val n = length upds
@@ -570,7 +584,7 @@
fact_graph = fact_graph})
end
in
- mash_map trans;
+ mash_map ctxt trans;
if verbose then
"Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
(if verbose then
@@ -582,7 +596,7 @@
end
end
-fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t used_ths facts =
+fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
let
val thy = Proof_Context.theory_of ctxt
val prover = hd provers
@@ -590,9 +604,9 @@
val feats = features_of ctxt prover thy General [t]
val deps = used_ths |> map Thm.get_name_hint
in
- mash_map (fn {thys, fact_graph} =>
+ mash_map ctxt (fn {thys, fact_graph} =>
let
- val parents = parents_wrt_facts facts fact_graph
+ val parents = parents_wrt_facts ctxt facts fact_graph
val upds = [(name, parents, feats, deps)]
val (upds, fact_graph) =
([], fact_graph) |> fold (update_fact_graph ctxt) upds
@@ -608,19 +622,19 @@
val short_learn_timeout_factor = 0.2
val long_learn_timeout_factor = 4.0
-fun relevant_facts ctxt (params as {fact_filter, timeout, ...}) prover max_facts
- ({add, only, ...} : fact_override) hyp_ts concl_t facts =
+fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
+ max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
if not (subset (op =) (the_list fact_filter, fact_filters)) then
error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
else if only then
facts
- else if max_facts <= 0 then
+ else if max_facts <= 0 orelse null facts then
[]
else
let
val thy = Proof_Context.theory_of ctxt
fun maybe_learn can_suggest =
- if Async_Manager.has_running_threads MaShN orelse null facts then
+ if not learn orelse Async_Manager.has_running_threads MaShN then
()
else if Time.toSeconds timeout >= min_secs_for_learning then
let
@@ -642,10 +656,10 @@
val fact_filter =
case fact_filter of
SOME ff =>
- (if ff <> iterN then maybe_learn (mash_can_suggest_facts ()) else ();
- ff)
+ (if ff <> iterN then maybe_learn (mash_can_suggest_facts ctxt)
+ else (); ff)
| NONE =>
- if mash_can_suggest_facts () then (maybe_learn true; meshN)
+ if mash_can_suggest_facts ctxt then (maybe_learn true; meshN)
else if mash_could_suggest_facts () then (maybe_learn false; iterN)
else iterN
val add_ths = Attrib.eval_thms ctxt add
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:04 2012 +0200
@@ -86,6 +86,7 @@
("strict", "false"),
("lam_trans", "smart"),
("uncurried_aliases", "smart"),
+ ("learn", "true"),
("fact_filter", "smart"),
("max_facts", "smart"),
("fact_thresholds", "0.45 0.85"),
@@ -108,6 +109,7 @@
("non_blocking", "blocking"),
("non_strict", "strict"),
("no_uncurried_aliases", "uncurried_aliases"),
+ ("dont_learn", "learn"),
("no_isar_proof", "isar_proof"),
("dont_slice", "slice"),
("dont_minimize", "minimize")]
@@ -296,6 +298,7 @@
val strict = mode = Auto_Try orelse lookup_bool "strict"
val lam_trans = lookup_option lookup_string "lam_trans"
val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
+ val learn = lookup_bool "learn"
val fact_filter = lookup_option lookup_string "fact_filter"
val max_facts = lookup_option lookup_int "max_facts"
val fact_thresholds = lookup_real_pair "fact_thresholds"
@@ -317,7 +320,7 @@
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
provers = provers, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
- fact_filter = fact_filter, max_facts = max_facts,
+ 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_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slice = slice,
@@ -371,7 +374,7 @@
run_minimize (get_params Minimize ctxt
(("provers", [default_minimize_prover]) ::
override_params))
- (the_default 1 opt_i) (#add fact_override) state
+ (K ()) (the_default 1 opt_i) (#add fact_override) state
else if subcommand = messagesN then
messages opt_i
else if subcommand = supported_proversN then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:04 2012 +0200
@@ -17,13 +17,15 @@
val auto_minimize_min_facts : int Config.T
val auto_minimize_max_time : real Config.T
val minimize_facts :
- string -> params -> bool -> int -> int -> Proof.state
+ (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state
-> ((string * stature) * thm list) list
-> ((string * stature) * thm list) list option
* ((unit -> play) * (play -> string) * string)
- val get_minimizing_prover : Proof.context -> mode -> string -> prover
+ val get_minimizing_prover :
+ Proof.context -> mode -> (thm list -> unit) -> string -> prover
val run_minimize :
- params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
+ params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
+ -> Proof.state -> unit
end;
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
@@ -68,7 +70,7 @@
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
- fact_filter = NONE, max_facts = SOME (length facts),
+ learn = false, fact_filter = NONE, max_facts = SOME (length facts),
fact_thresholds = (1.01, 1.01), 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,
@@ -181,8 +183,8 @@
| p => p
end
-fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
- facts =
+fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
+ i n state facts =
let
val ctxt = Proof.context_of state
val prover =
@@ -202,13 +204,16 @@
linear_minimize
val (min_facts, {preplay, message, message_tail, ...}) =
min test (new_timeout timeout run_time) result facts
- val _ = print silent (fn () => cat_lines
- ["Minimized to " ^ n_facts (map fst min_facts)] ^
- (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
- |> length of
- 0 => ""
- | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
- in (SOME min_facts, (preplay, message, message_tail)) end
+ in
+ print silent (fn () => cat_lines
+ ["Minimized to " ^ n_facts (map fst min_facts)] ^
+ (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
+ |> length of
+ 0 => ""
+ | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
+ (if learn then do_learn (maps snd min_facts) else ());
+ (SOME min_facts, (preplay, message, message_tail))
+ end
| {outcome = SOME TimedOut, preplay, ...} =>
(NONE,
(preplay,
@@ -225,9 +230,10 @@
fun adjust_reconstructor_params override_params
({debug, verbose, overlord, blocking, provers, type_enc, strict,
- lam_trans, uncurried_aliases, fact_filter, max_facts, fact_thresholds,
- max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
- slice, minimize, timeout, preplay_timeout, expect} : params) =
+ lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
+ fact_thresholds, max_mono_iters, 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
@@ -241,7 +247,7 @@
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
provers = provers, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
- fact_filter = fact_filter, max_facts = max_facts,
+ 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_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slice = slice,
@@ -249,7 +255,7 @@
expect = expect}
end
-fun minimize ctxt mode name
+fun minimize ctxt mode do_learn name
(params as {debug, verbose, isar_proof, minimize, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
(result as {outcome, used_facts, run_time, preplay, message,
@@ -293,7 +299,7 @@
val minimize = minimize |> the_default perhaps_minimize
val (used_facts, (preplay, message, _)) =
if minimize then
- minimize_facts minimize_name params (not verbose) subgoal
+ minimize_facts do_learn minimize_name params (not verbose) subgoal
subgoal_count state
(filter_used_facts used_facts
(map (apsnd single o untranslated_fact) facts))
@@ -319,11 +325,12 @@
| NONE => result
end
-fun get_minimizing_prover ctxt mode name params minimize_command problem =
+fun get_minimizing_prover ctxt mode do_learn name params minimize_command
+ problem =
get_prover ctxt mode name params minimize_command problem
- |> minimize ctxt mode name params problem
+ |> minimize ctxt mode do_learn name params problem
-fun run_minimize (params as {provers, ...}) i refs state =
+fun run_minimize (params as {provers, ...}) do_learn i refs state =
let
val ctxt = Proof.context_of state
val reserved = reserved_isar_keyword_table ()
@@ -339,7 +346,7 @@
[] => error "No prover is set."
| prover :: _ =>
(kill_provers ();
- minimize_facts prover params false i n state facts
+ minimize_facts do_learn prover params false i n state facts
|> (fn (_, (preplay, message, message_tail)) =>
message (preplay ()) ^ message_tail
|> Output.urgent_message))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 18 08:44:04 2012 +0200
@@ -18,27 +18,28 @@
datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
type params =
- {debug: bool,
- verbose: bool,
- overlord: bool,
- blocking: bool,
- provers: string list,
- type_enc: string option,
- strict: bool,
- lam_trans: string option,
- uncurried_aliases: bool option,
- fact_filter: string option,
- max_facts: int option,
- fact_thresholds: real * real,
- max_mono_iters: int option,
- max_new_mono_instances: int option,
- isar_proof: bool,
- isar_shrink_factor: int,
- slice: bool,
- minimize: bool option,
- timeout: Time.time,
- preplay_timeout: Time.time,
- expect: string}
+ {debug : bool,
+ verbose : bool,
+ overlord : bool,
+ blocking : bool,
+ provers : string list,
+ type_enc : string option,
+ strict : bool,
+ lam_trans : string option,
+ uncurried_aliases : bool option,
+ learn : bool,
+ fact_filter : string option,
+ max_facts : int option,
+ fact_thresholds : real * real,
+ max_mono_iters : int option,
+ max_new_mono_instances : int option,
+ isar_proof : bool,
+ isar_shrink_factor : int,
+ slice : bool,
+ minimize : bool option,
+ timeout : Time.time,
+ preplay_timeout : Time.time,
+ expect : string}
type relevance_fudge =
{local_const_multiplier : real,
@@ -66,19 +67,19 @@
SMT_Weighted_Fact of (string * stature) * (int option * thm)
type prover_problem =
- {state: Proof.state,
- goal: thm,
- subgoal: int,
- subgoal_count: int,
- facts: prover_fact list}
+ {state : Proof.state,
+ goal : thm,
+ subgoal : int,
+ subgoal_count : int,
+ facts : prover_fact list}
type prover_result =
- {outcome: failure option,
- used_facts: (string * stature) list,
- run_time: Time.time,
- preplay: unit -> play,
- message: play -> string,
- message_tail: string}
+ {outcome : failure option,
+ used_facts : (string * stature) list,
+ run_time : Time.time,
+ preplay : unit -> play,
+ message : play -> string,
+ message_tail : string}
type prover =
params -> ((string * string list) list -> string -> minimize_command)
@@ -306,27 +307,28 @@
(** problems, results, ATPs, etc. **)
type params =
- {debug: bool,
- verbose: bool,
- overlord: bool,
- blocking: bool,
- provers: string list,
- type_enc: string option,
- strict: bool,
- lam_trans: string option,
- uncurried_aliases: bool option,
- fact_filter: string option,
- max_facts: int option,
- fact_thresholds: real * real,
- max_mono_iters: int option,
- max_new_mono_instances: int option,
- isar_proof: bool,
- isar_shrink_factor: int,
- slice: bool,
- minimize: bool option,
- timeout: Time.time,
- preplay_timeout: Time.time,
- expect: string}
+ {debug : bool,
+ verbose : bool,
+ overlord : bool,
+ blocking : bool,
+ provers : string list,
+ type_enc : string option,
+ strict : bool,
+ lam_trans : string option,
+ uncurried_aliases : bool option,
+ learn : bool,
+ fact_filter : string option,
+ max_facts : int option,
+ fact_thresholds : real * real,
+ max_mono_iters : int option,
+ max_new_mono_instances : int option,
+ isar_proof : bool,
+ isar_shrink_factor : int,
+ slice : bool,
+ minimize : bool option,
+ timeout : Time.time,
+ preplay_timeout : Time.time,
+ expect : string}
type relevance_fudge =
{local_const_multiplier : real,
@@ -354,19 +356,19 @@
SMT_Weighted_Fact of (string * stature) * (int option * thm)
type prover_problem =
- {state: Proof.state,
- goal: thm,
- subgoal: int,
- subgoal_count: int,
- facts: prover_fact list}
+ {state : Proof.state,
+ goal : thm,
+ subgoal : int,
+ subgoal_count : int,
+ facts : prover_fact list}
type prover_result =
- {outcome: failure option,
- used_facts: (string * stature) list,
- run_time: Time.time,
- preplay: unit -> play,
- message: play -> string,
- message_tail: string}
+ {outcome : failure option,
+ used_facts : (string * stature) list,
+ run_time : Time.time,
+ preplay : unit -> play,
+ message : play -> string,
+ message_tail : string}
type prover =
params -> ((string * string list) list -> string -> minimize_command)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:04 2012 +0200
@@ -86,7 +86,10 @@
|> take num_facts}
fun really_go () =
problem
- |> get_minimizing_prover ctxt mode name params minimize_command
+ |> get_minimizing_prover ctxt mode
+ (mash_learn_proof ctxt params (prop_of goal)
+ (map untranslated_fact facts))
+ name params minimize_command
|> (fn {outcome, preplay, message, message_tail, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN