--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 01 17:27:10 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 01 18:41:23 2010 +0200
@@ -299,20 +299,27 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover hard_timeout timeout dir st =
+fun run_sh prover_name prover hard_timeout timeout dir st =
let
- val {context = ctxt, facts, goal} = Proof.goal st
+ val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val thy = ProofContext.theory_of ctxt
+ val i = 1
val change_dir = (fn SOME d => Config.put Sledgehammer.dest_dir d | _ => I)
val ctxt' =
ctxt
|> change_dir dir
|> Config.put Sledgehammer.measure_runtime true
- val params = Sledgehammer_Isar.default_params thy
- [("timeout", Int.toString timeout ^ " s")]
- val problem =
- {subgoal = 1, goal = (ctxt', (facts, goal)),
- relevance_override = {add = [], del = [], only = false}, axioms = NONE}
+ val params as {full_types, relevance_thresholds, max_relevant, ...} =
+ Sledgehammer_Isar.default_params thy
+ [("timeout", Int.toString timeout ^ " s")]
+ val relevance_override = {add = [], del = [], only = false}
+ val {default_max_relevant, ...} = ATP_Systems.get_prover thy prover_name
+ val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
+ val axioms =
+ Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
+ (the_default default_max_relevant max_relevant)
+ relevance_override chained_ths hyp_ts concl_t
+ val problem = {ctxt = ctxt', goal = goal, subgoal = i, axioms = axioms}
val time_limit =
(case hard_timeout of
NONE => I
@@ -352,7 +359,7 @@
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
|> Option.map (fst o read_int o explode)
- val (msg, result) = run_sh prover hard_timeout timeout dir st
+ val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
in
case result of
SH_OK (time_isa, time_atp, names) =>