--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 18:39:22 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 18:39:22 2011 +0200
@@ -317,13 +317,13 @@
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
-fun get_prover ctxt slicing args =
+fun get_prover ctxt args =
let
fun default_prover_name () =
hd (#provers (Sledgehammer_Isar.default_params ctxt []))
handle Empty => error "No ATP available."
fun get_prover name =
- (name, Sledgehammer_Run.get_minimizing_prover ctxt false slicing name)
+ (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name
@@ -429,7 +429,7 @@
val triv_str = if trivial then "[T] " else ""
val _ = change_data id inc_sh_calls
val _ = if trivial then () else change_data id inc_sh_nontriv_calls
- val (prover_name, prover) = get_prover (Proof.context_of st) true args
+ val (prover_name, prover) = get_prover (Proof.context_of st) args
val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val dir = AList.lookup (op =) args keepK
@@ -473,7 +473,7 @@
let
val ctxt = Proof.context_of st
val n0 = length (these (!named_thms))
- val (prover_name, _) = get_prover ctxt false args
+ val (prover_name, _) = get_prover ctxt args
val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
val timeout =
AList.lookup (op =) args minimize_timeoutK
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Apr 21 18:39:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Apr 21 18:39:22 2011 +0200
@@ -254,7 +254,7 @@
val explicit_apply = lookup_bool "explicit_apply"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
- val slicing = lookup_bool "slicing"
+ val slicing = not auto andalso lookup_bool "slicing"
val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
val expect = lookup_string "expect"
in
@@ -303,7 +303,7 @@
in
if subcommand = runN then
let val i = the_default 1 opt_i in
- run_sledgehammer (get_params false ctxt override_params) false true i
+ run_sledgehammer (get_params false ctxt override_params) false i
relevance_override (minimize_command override_params i)
state
|> K ()
@@ -376,7 +376,7 @@
fun auto_sledgehammer state =
let val ctxt = Proof.context_of state in
- run_sledgehammer (get_params true ctxt []) true false 1
+ run_sledgehammer (get_params true ctxt []) true 1
no_relevance_override (minimize_command [] 1) state
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Apr 21 18:39:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Apr 21 18:39:22 2011 +0200
@@ -147,7 +147,7 @@
silent i n state facts =
let
val ctxt = Proof.context_of state
- val prover = get_prover ctxt false false prover_name
+ val prover = get_prover ctxt false prover_name
val msecs = Time.toMilliseconds timeout
val _ = print silent (fn () => "Sledgehammer minimize: " ^
quote prover_name ^ ".")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 18:39:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 18:39:22 2011 +0200
@@ -93,7 +93,7 @@
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
- val get_prover : Proof.context -> bool -> bool -> string -> prover
+ val get_prover : Proof.context -> bool -> string -> prover
val setup : theory -> theory
end;
@@ -334,7 +334,7 @@
them each time. *)
val atp_important_message_keep_factor = 0.1
-fun run_atp auto may_slice name
+fun run_atp auto name
({exec, required_execs, arguments, slices, proof_delims, known_failures,
explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config)
({debug, verbose, overlord, max_relevant, monomorphize,
@@ -345,7 +345,6 @@
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
- val slicing = may_slice andalso slicing
fun monomorphize_facts facts =
let
val repair_context =
@@ -566,13 +565,11 @@
val smt_slice_time_frac = Unsynchronized.ref 0.5
val smt_slice_min_secs = Unsynchronized.ref 5
-fun smt_filter_loop may_slice name
- ({debug, verbose, overlord, monomorphize_limit, timeout,
- slicing, ...} : params)
+fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit,
+ timeout, slicing, ...} : params)
state i smt_filter =
let
val ctxt = Proof.context_of state
- val slicing = may_slice andalso slicing
val max_slices = if slicing then !smt_max_slices else 1
val repair_context =
select_smt_solver name
@@ -684,8 +681,7 @@
(Config.put Metis_Tactics.verbose debug
#> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
-fun run_smt_solver auto may_slice name (params as {debug, verbose, ...})
- minimize_command
+fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command
({state, subgoal, subgoal_count, facts, smt_filter, ...}
: prover_problem) =
let
@@ -695,7 +691,7 @@
val facts = facts ~~ (0 upto num_facts - 1)
|> map (smt_weighted_fact thy num_facts)
val {outcome, used_facts, run_time_in_msecs} =
- smt_filter_loop may_slice name params state subgoal smt_filter facts
+ smt_filter_loop name params state subgoal smt_filter facts
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
val outcome = outcome |> Option.map failure_from_smt_failure
val message =
@@ -727,12 +723,12 @@
run_time_in_msecs = run_time_in_msecs, message = message}
end
-fun get_prover ctxt auto may_slice name =
+fun get_prover ctxt auto name =
let val thy = Proof_Context.theory_of ctxt in
if is_smt_prover ctxt name then
- run_smt_solver auto may_slice name
+ run_smt_solver auto name
else if member (op =) (supported_atps thy) name then
- run_atp auto may_slice name (get_atp thy name)
+ run_atp auto name (get_atp thy name)
else
error ("No such prover: " ^ name ^ ".")
end
--- 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)
--- a/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 18:39:22 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 18:39:22 2011 +0200
@@ -23,7 +23,7 @@
@ [("timeout", string_of_int (Time.toSeconds timeout))])
(* @ [("overlord", "true")] *)
|> Sledgehammer_Isar.default_params ctxt
- val prover = Sledgehammer_Provers.get_prover ctxt false true name
+ val prover = Sledgehammer_Provers.get_prover ctxt false name
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
val is_built_in_const =