--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 18:39:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 18:39:22 2011 +0200
@@ -14,10 +14,10 @@
type prover = Sledgehammer_Provers.prover
val auto_minimize_min_facts : int Unsynchronized.ref
- val get_minimizing_prover : Proof.context -> bool -> bool -> string -> prover
+ val get_minimizing_prover : Proof.context -> bool -> string -> prover
val run_sledgehammer :
- params -> bool -> bool -> int -> relevance_override
- -> (string -> minimize_command) -> Proof.state -> bool * Proof.state
+ params -> bool -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> bool * Proof.state
end;
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
@@ -44,10 +44,10 @@
val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
-fun get_minimizing_prover ctxt auto may_slice name
+fun get_minimizing_prover ctxt auto name
(params as {debug, verbose, explicit_apply, ...}) minimize_command
(problem as {state, subgoal, subgoal_count, facts, ...}) =
- get_prover ctxt auto may_slice name params minimize_command problem
+ get_prover ctxt auto name params minimize_command problem
|> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
if is_some outcome then
result
@@ -85,11 +85,10 @@
fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
expect, ...})
- auto may_slice minimize_command only
+ auto minimize_command only
{state, goal, subgoal, subgoal_count, facts, smt_filter} name =
let
val ctxt = Proof.context_of state
- val slicing = may_slice andalso slicing
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
val max_relevant =
@@ -104,8 +103,7 @@
smt_filter = smt_filter}
fun really_go () =
problem
- |> get_minimizing_prover ctxt auto may_slice name params
- (minimize_command name)
+ |> get_minimizing_prover ctxt auto name params (minimize_command name)
|> (fn {outcome, message, ...} =>
(if is_some outcome then "none" else "some" (* sic *), message))
fun go () =
@@ -170,8 +168,7 @@
fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
type_sys, relevance_thresholds, max_relevant,
slicing, timeout, ...})
- auto may_slice i (relevance_override as {only, ...})
- minimize_command state =
+ auto i (relevance_override as {only, ...}) minimize_command state =
if null provers then
error "No prover is set."
else case subgoal_count state of
@@ -184,7 +181,6 @@
state |> Proof.map_context (Config.put SMT_Config.verbose debug)
val ctxt = Proof.context_of state
val thy = Proof_Context.theory_of ctxt
- val slicing = may_slice andalso slicing
val {facts = chained_ths, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val no_dangerous_types = types_dangerous_types type_sys
@@ -205,7 +201,7 @@
facts = facts,
smt_filter = maybe_smt_filter
(fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
- val launch = launch_prover params auto may_slice minimize_command only
+ val launch = launch_prover params auto minimize_command only
in
if auto then
fold (fn prover => fn (true, state) => (true, state)