# HG changeset patch # User blanchet # Date 1287748101 -7200 # Node ID 1e4c7185f3f99daea69c13c29408f586f0b58754 # Parent db8413d82c3b79353b7d441679f4c99a595d8944 remove more needless code ("run_smt_solvers"); tuning diff -r db8413d82c3b -r 1e4c7185f3f9 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r db8413d82c3b -r 1e4c7185f3f9 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 = diff -r db8413d82c3b -r 1e4c7185f3f9 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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