# HG changeset patch # User blanchet # Date 1361365851 -3600 # Node ID 260cb10aac4bb2208a87901436adc60a994cacc3 # Parent e3447c380fe19604ac27c0ce03a527d17f987224 minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay diff -r e3447c380fe1 -r 260cb10aac4b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Feb 20 13:04:03 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Feb 20 14:10:51 2013 +0100 @@ -189,20 +189,6 @@ fun merge data : T = AList.merge (op =) (K true) data ) -fun remotify_prover_if_supported_and_not_already_remote ctxt name = - if String.isPrefix remote_prefix name then - SOME name - else - let val remote_name = remote_prefix ^ name in - if is_prover_supported ctxt remote_name then SOME remote_name else NONE - end - -fun remotify_prover_if_not_installed ctxt name = - if is_prover_supported ctxt name andalso is_prover_installed ctxt name then - SOME name - else - remotify_prover_if_supported_and_not_already_remote ctxt name - fun avoid_too_many_threads _ _ [] = [] | avoid_too_many_threads _ (0, 0) _ = [] | avoid_too_many_threads ctxt (0, max_remote) provers = diff -r e3447c380fe1 -r 260cb10aac4b src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 20 13:04:03 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 20 14:10:51 2013 +0100 @@ -35,6 +35,7 @@ open ATP_Util open ATP_Proof open ATP_Problem_Generate +open ATP_Systems open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Reconstruct @@ -296,9 +297,10 @@ (case Lazy.force preplay of Played (reconstr as Metis _, timeout) => if isar_proofs = SOME true then - (* Cheat: Assume the original prover is as fast as "metis" - for the goal it proved itself. *) - (can_min_fast_enough timeout, (name, params)) + (* Cheat: Assume the selected ATP is as fast as "metis" for + the goal it proved itself. *) + (can_min_fast_enough timeout, + (isar_proof_reconstructor ctxt name, params)) else if can_min_fast_enough timeout then (true, extract_reconstructor params reconstr ||> (fn override_params => @@ -334,14 +336,10 @@ | NONE => result end -(* TODO: implement *) -fun maybe_regenerate_isar_proof result = result - fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem = get_prover ctxt mode name params minimize_command problem |> maybe_minimize ctxt mode do_learn name params problem - |> maybe_regenerate_isar_proof fun run_minimize (params as {provers, ...}) do_learn i refs state = let diff -r e3447c380fe1 -r 260cb10aac4b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Feb 20 13:04:03 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Feb 20 14:10:51 2013 +0100 @@ -110,6 +110,10 @@ val is_unit_equational_atp : Proof.context -> string -> bool val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool + val remotify_prover_if_supported_and_not_already_remote : + Proof.context -> string -> string option + val remotify_prover_if_not_installed : + Proof.context -> string -> string option val default_max_facts_for_prover : Proof.context -> bool -> string -> int val is_unit_equality : term -> bool val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool @@ -129,6 +133,7 @@ val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list + val isar_proof_reconstructor : Proof.context -> string -> string val get_prover : Proof.context -> mode -> string -> prover end; @@ -186,6 +191,20 @@ is_reconstructor orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) +fun remotify_prover_if_supported_and_not_already_remote ctxt name = + if String.isPrefix remote_prefix name then + SOME name + else + let val remote_name = remote_prefix ^ name in + if is_prover_supported ctxt remote_name then SOME remote_name else NONE + end + +fun remotify_prover_if_not_installed ctxt name = + if is_prover_supported ctxt name andalso is_prover_installed ctxt name then + SOME name + else + remotify_prover_if_supported_and_not_already_remote ctxt name + fun get_slices slice slices = (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single) @@ -598,19 +617,26 @@ #> type_enc_from_string soundness #> adjust_type_enc format -val metis_minimize_max_time = seconds 2.0 +fun isar_proof_reconstructor ctxt name = + let val thy = Proof_Context.theory_of ctxt in + if is_atp thy name then name + else remotify_prover_if_not_installed ctxt eN |> the_default name + end -fun choose_minimize_command params minimize_command name preplay = +(* See the analogous logic in the function "maybe_minimize" in + "sledgehammer_minimize.ML". *) +fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command + name preplay = let - val (name, override_params) = + val maybe_isar_name = + name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt + val (min_name, override_params) = case preplay of - Played (reconstr, time) => - if Time.<= (time, metis_minimize_max_time) then - extract_reconstructor params reconstr - else - (name, []) - | _ => (name, []) - in minimize_command override_params name end + Played (reconstr, _) => + if isar_proofs = SOME true then (maybe_isar_name, []) + else extract_reconstructor params reconstr + | _ => (maybe_isar_name, []) + in minimize_command override_params min_name end fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = @@ -795,7 +821,8 @@ fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name - val full_proof = debug orelse isar_proofs = SOME true + val full_proof = + debug orelse (isar_proofs |> the_default (mode = Minimize)) val args = arguments ctxt full_proof extra (slice_timeout |> the_default one_day) @@ -917,7 +944,8 @@ pool, fact_names, sym_tab, atp_proof, goal) val one_line_params = (preplay, proof_banner mode name, used_facts, - choose_minimize_command params minimize_command name preplay, + choose_minimize_command ctxt params minimize_command name + preplay, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in @@ -1127,7 +1155,8 @@ let val one_line_params = (preplay, proof_banner mode name, used_facts, - choose_minimize_command params minimize_command name preplay, + choose_minimize_command ctxt params minimize_command name + preplay, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in one_line_proof_text num_chained one_line_params end, diff -r e3447c380fe1 -r 260cb10aac4b src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 13:04:03 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 14:10:51 2013 +0100 @@ -375,7 +375,6 @@ (_, []) => line :: lines | (pre, Inference_Step (name', _, _, _, _) :: post) => line :: pre @ map (replace_dependencies_in_line (name', [name])) post - | _ => raise Fail "unexpected inference" val waldmeister_conjecture_num = "1.0.0.0"