--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 12:15:31 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 13:48:21 2010 +0200
@@ -359,6 +359,7 @@
relevance_override chained_ths hyp_ts concl_t
val problem =
{state = st', goal = goal, subgoal = i,
+ subgoal_count = Sledgehammer_Util.subgoal_count st,
axioms = axioms |> map Sledgehammer.Unprepared, only = true}
val time_limit =
(case hard_timeout of
@@ -430,9 +431,6 @@
end
-
-val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
-
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
open Metis_Translate
@@ -446,7 +444,8 @@
val params = Sledgehammer_Isar.default_params thy
[("provers", prover_name), ("timeout", Int.toString timeout ^ " s")]
val minimize =
- Sledgehammer_Minimize.minimize_facts params 1 (subgoal_count st)
+ Sledgehammer_Minimize.minimize_facts params 1
+ (Sledgehammer_Util.subgoal_count st)
val _ = log separator
in
case minimize st (these (!named_thms)) of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 12:15:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 13:48:21 2010 +0200
@@ -37,6 +37,7 @@
{state: Proof.state,
goal: thm,
subgoal: int,
+ subgoal_count: int,
axioms: axiom list,
only: bool}
@@ -132,6 +133,7 @@
{state: Proof.state,
goal: thm,
subgoal: int,
+ subgoal_count: int,
axioms: axiom list,
only: bool}
@@ -198,7 +200,7 @@
({debug, verbose, overlord, full_types, explicit_apply,
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
minimize_command
- ({state, goal, subgoal, axioms, only} : prover_problem) =
+ ({state, goal, subgoal, axioms, only, ...} : prover_problem) =
let
val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
@@ -342,7 +344,8 @@
run_time_in_msecs = NONE})
fun run_smt_solver remote ({timeout, ...} : params) minimize_command
- ({state, subgoal, axioms, ...} : prover_problem) =
+ ({state, subgoal, subgoal_count, axioms, ...}
+ : prover_problem) =
let
val {outcome, used_axioms, run_time_in_msecs} =
saschas_run_smt_solver remote timeout state
@@ -350,7 +353,7 @@
val message =
if outcome = NONE then
try_command_line (proof_banner false)
- (apply_on_subgoal subgoal (subgoal_count state) ^
+ (apply_on_subgoal subgoal subgoal_count ^
command_call smtN (map fst used_axioms)) ^
minimize_line minimize_command (map fst used_axioms)
else
@@ -367,7 +370,8 @@
run_atp auto name (get_atp thy name)
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
- auto i n minimize_command (problem as {state, goal, axioms, ...})
+ auto minimize_command
+ (problem as {state, goal, subgoal, subgoal_count, axioms, ...})
name =
let
val thy = Proof.theory_of state
@@ -377,7 +381,8 @@
val max_relevant =
the_default (default_max_relevant_for_prover thy name) max_relevant
val num_axioms = Int.min (length axioms, max_relevant)
- val desc = prover_description ctxt params name num_axioms i n goal
+ val desc =
+ prover_description ctxt params name num_axioms subgoal subgoal_count goal
fun go () =
let
fun really_go () =
@@ -435,15 +440,10 @@
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val _ = () |> not blocking ? kill_provers
val _ = if auto then () else priority "Sledgehammering..."
- fun relevant full_types max_relevant =
- relevant_facts ctxt full_types relevance_thresholds max_relevant
- relevance_override chained_ths hyp_ts concl_t
- val run_prover = run_prover params auto i n minimize_command
val (smts, atps) =
provers |> List.partition (member (op =) smt_prover_names)
- |>> take 1 (* no point in running both "smt" and "remote_smt" *)
- fun run_atps (res as (success, state)) =
- if success orelse null atps then
+ fun run_provers full_types maybe_prepare provers (res as (success, state)) =
+ if success orelse null provers then
res
else
let
@@ -452,43 +452,35 @@
SOME n => n
| NONE =>
0 |> fold (Integer.max o default_max_relevant_for_prover thy)
- atps
+ provers
|> auto ? (fn n => n div auto_max_relevant_divisor)
- val axioms = relevant full_types max_max_relevant
- |> map (Prepared o prepare_axiom ctxt)
+ val axioms =
+ relevant_facts ctxt full_types relevance_thresholds
+ max_max_relevant relevance_override chained_ths
+ hyp_ts concl_t
+ |> map maybe_prepare
val problem =
- {state = state, goal = goal, subgoal = i, axioms = axioms,
- only = only}
+ {state = state, goal = goal, subgoal = i, subgoal_count = n,
+ axioms = axioms, only = only}
+ val run_prover = run_prover params auto minimize_command
in
if auto then
fold (fn prover => fn (true, state) => (true, state)
| (false, _) => run_prover problem prover)
- atps (false, state)
+ provers (false, state)
else
- atps |> (if blocking then Par_List.map else map)
- (run_prover problem)
- |> exists fst |> rpair state
+ provers |> (if blocking then Par_List.map else map)
+ (run_prover problem)
+ |> exists fst |> rpair state
end
- fun run_smt_solvers (res as (success, state)) =
- if success orelse null smts then
- res
- else
- let
- val max_relevant =
- max_relevant |> the_default smt_default_max_relevant
- val axioms = relevant true max_relevant |> map Unprepared
- val problem =
- {state = state, goal = goal, subgoal = i, axioms = axioms,
- only = only}
- in smts |> map (run_prover problem) |> exists fst |> rpair state end
+ val run_atps = run_provers full_types (Prepared o prepare_axiom ctxt) atps
+ val run_smts = run_provers true Unprepared smts
fun run_atps_and_smt_solvers () =
- [run_atps, run_smt_solvers]
- |> Par_List.map (fn f => f (false, state) |> K ())
+ [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
in
- if blocking then
- (false, state) |> run_atps |> not auto ? run_smt_solvers
- else
- Future.fork (tap run_atps_and_smt_solvers) |> K (false, state)
+ (false, state)
+ |> (if blocking then run_atps #> not auto ? run_smts
+ else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
end
val setup =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 12:15:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 13:48:21 2010 +0200
@@ -45,7 +45,7 @@
fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof,
isar_shrink_factor, ...} : params) (prover : prover)
- explicit_apply timeout subgoal state axioms =
+ explicit_apply timeout i n state axioms =
let
val _ =
priority ("Testing " ^ n_facts (map fst axioms) ^ "...")
@@ -58,11 +58,10 @@
val axioms =
axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n))
val {context = ctxt, goal, ...} = Proof.goal state
- val prover_problem =
- {state = state, goal = goal, subgoal = subgoal, axioms = axioms,
- only = true}
- val result as {outcome, used_axioms, ...} =
- prover params (K "") prover_problem
+ val problem =
+ {state = state, goal = goal, subgoal = i, subgoal_count = n,
+ axioms = axioms, only = true}
+ val result as {outcome, used_axioms, ...} = prover params (K "") problem
in
priority (case outcome of
SOME failure => string_for_failure failure
@@ -90,8 +89,8 @@
val fudge_msecs = 1000
fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."
- | minimize_facts (params as {provers = prover_name :: _, timeout, ...})
- i (_ : int) state axioms =
+ | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n
+ state axioms =
let
val thy = Proof.theory_of state
val prover = get_prover thy false prover_name
@@ -103,7 +102,7 @@
not (forall (Meson.is_fol_term thy)
(concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
fun do_test timeout =
- test_facts params prover explicit_apply timeout i state
+ test_facts params prover explicit_apply timeout i n state
val timer = Timer.startRealTimer ()
in
(case do_test timeout axioms of