# HG changeset patch # User wenzelm # Date 1358428355 -3600 # Node ID e424e17ee42048e7f505ba09c5d29efc91982a14 # Parent 7f0bc95af61c30f8f410076450ef9a1f74dddeb5# Parent ca071373b695ae266a6c7f6b8d62bd2a0b50018d merged diff -r ca071373b695 -r e424e17ee420 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Jan 17 14:11:26 2013 +0100 +++ b/Admin/components/components.sha1 Thu Jan 17 14:12:35 2013 +0100 @@ -6,6 +6,8 @@ cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz 0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz +2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz +e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz 6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz 8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz diff -r ca071373b695 -r e424e17ee420 Admin/components/main --- a/Admin/components/main Thu Jan 17 14:11:26 2013 +0100 +++ b/Admin/components/main Thu Jan 17 14:12:35 2013 +0100 @@ -1,6 +1,6 @@ #main components for everyday use, without big impact on overall build time cvc3-2.4.1 -e-1.6 +e-1.6-2 exec_process-1.0.3 Haskabelle-2013 jdk-7u11 diff -r ca071373b695 -r e424e17ee420 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Jan 17 14:11:26 2013 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Jan 17 14:12:35 2013 +0100 @@ -12,7 +12,7 @@ %\usepackage[scaled=.85]{beramono} \usepackage{isabelle,iman,pdfsetup} -\newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}} +\newcommand\download{\url{http://isabelle.in.tum.de/components/}} \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} @@ -865,6 +865,12 @@ that contains the \texttt{emales.py} script. Sledgehammer has been tested with version 1.1. +\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is a metaprover developed +by Josef Urban that implements strategy scheduling on top of E. To use +E-Par, set the environment variable \texttt{E\_HOME} to the directory +that contains the \texttt{runepar.pl} script and the \texttt{eprover} and +\texttt{epclextract} executables, or use the prebuilt E package from \download. + \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the diff -r ca071373b695 -r e424e17ee420 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Jan 17 14:11:26 2013 +0100 +++ b/src/HOL/Sledgehammer.thy Thu Jan 17 14:12:35 2013 +0100 @@ -16,6 +16,7 @@ ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" ML_file "Tools/Sledgehammer/sledgehammer_proof.ML" ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML" +ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML" ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML" ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" ML_file "Tools/Sledgehammer/sledgehammer_provers.ML" diff -r ca071373b695 -r e424e17ee420 src/HOL/TPTP/MaSh_Eval.thy --- a/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 14:11:26 2013 +0100 +++ b/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 14:12:35 2013 +0100 @@ -12,9 +12,9 @@ sledgehammer_params [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native, - lam_trans = combs_and_lifting, timeout = 15, dont_preplay, minimize] + lam_trans = lifting, timeout = 15, dont_preplay, minimize] -declare [[sledgehammer_instantiate_inducts]] +declare [[sledgehammer_instantiate_inducts = false]] ML {* !Multithreading.max_threads diff -r ca071373b695 -r e424e17ee420 src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 14:11:26 2013 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 14:12:35 2013 +0100 @@ -12,9 +12,9 @@ sledgehammer_params [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native, - lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize] + lam_trans = lifting, timeout = 2, dont_preplay, minimize] -declare [[sledgehammer_instantiate_inducts]] +declare [[sledgehammer_instantiate_inducts = false]] ML {* !Multithreading.max_threads @@ -29,7 +29,7 @@ val thys = [@{theory List}] val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] val prover = hd provers -val max_suggestions = 1024 +val max_suggestions = 1536 val dir = "List" val prefix = "/tmp/" ^ dir ^ "/" *} diff -r ca071373b695 -r e424e17ee420 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Thu Jan 17 14:11:26 2013 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Thu Jan 17 14:12:35 2013 +0100 @@ -68,9 +68,9 @@ |> File.write_list prob_file val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = - File.shell_path (Path.explode path) ^ - " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^ - File.shell_path prob_file + File.shell_path (Path.explode path) ^ " " ^ + arguments ctxt false "" (seconds 1.0) (File.shell_path prob_file) + (ord, K [], K []) in TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command |> fst diff -r ca071373b695 -r e424e17ee420 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jan 17 14:11:26 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Jan 17 14:12:35 2013 +0100 @@ -16,7 +16,7 @@ type atp_config = {exec : string list * string list, arguments : - Proof.context -> bool -> string -> Time.time + Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, @@ -45,6 +45,7 @@ val dummy_thfN : string val eN : string val e_malesN : string + val e_parN : string val e_sineN : string val e_tofofN : string val iproverN : string @@ -88,7 +89,7 @@ type atp_config = {exec : string list * string list, arguments : - Proof.context -> bool -> string -> Time.time + Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, @@ -140,6 +141,7 @@ val dummy_thfN = "dummy_thf" (* for experiments *) val eN = "e" val e_malesN = "e_males" +val e_parN = "e_par" val e_sineN = "e_sine" val e_tofofN = "e_tofof" val iproverN = "iprover" @@ -189,9 +191,9 @@ val alt_ergo_config : atp_config = {exec = (["WHY3_HOME"], ["why3"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--format tff1 --prover alt-ergo --timelimit " ^ - string_of_int (to_secs 1 timeout), + string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [], known_failures = [(ProofMissing, ": Valid"), @@ -301,13 +303,14 @@ val e_config : atp_config = {exec = (["E_HOME"], ["eproof_ram", "eproof"]), arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => + fn file_name => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => "--tstp-in --tstp-out --output-level=5 --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^ "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ - e_shell_level_argument full_proof, + e_shell_level_argument full_proof ^ " " ^ file_name, proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "Failure: Resource limit exceeded (time)"), @@ -334,27 +337,45 @@ val e_males_config : atp_config = {exec = (["E_MALES_HOME"], ["emales.py"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => - "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p", + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => + "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name, proof_delims = tstp_proof_delims, known_failures = #known_failures e_config, prem_role = Conjecture, best_slices = (* FUDGE *) - K [(1.0, ((1000, FOF, "mono_tags??", combsN, false), ""))], + K [(0.5, ((1000, FOF, "mono_tags??", combsN, false), "")), + (0.5, ((1000, FOF, "mono_guards??", combsN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val e_males = (e_malesN, fn () => e_males_config) +(* E-Par *) + +val e_par_config : atp_config = + {exec = (["E_HOME"], ["runepar.pl"]), + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => + string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^ + " 2" (* proofs *), + proof_delims = tstp_proof_delims, + known_failures = #known_failures e_config, + prem_role = Conjecture, + best_slices = #best_slices e_males_config, + best_max_mono_iters = default_max_mono_iters, + best_max_new_mono_instances = default_max_new_mono_instances} + +val e_par = (e_parN, fn () => e_par_config) + + (* iProver *) val iprover_config : atp_config = {exec = (["IPROVER_HOME"], ["iprover"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^ - string_of_real (Time.toReal timeout), + string_of_real (Time.toReal timeout) ^ " " ^ file_name, proof_delims = tstp_proof_delims, known_failures = [(ProofIncomplete, "% SZS output start CNFRefutation")] @ @@ -393,10 +414,11 @@ val leo2_config : atp_config = {exec = (["LEO2_HOME"], ["leo"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--foatp e --atp e=\"$E_HOME\"/eprover \ \--atp epclextract=\"$E_HOME\"/epclextract \ - \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout), + \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ + file_name, proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "CPU time limit exceeded, terminating"), @@ -419,8 +441,8 @@ val satallax_config : atp_config = {exec = (["SATALLAX_HOME"], ["satallax"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => - "-p hocore -t " ^ string_of_int (to_secs 1 timeout), + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => + "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")], known_failures = known_szs_status_failures, @@ -446,9 +468,11 @@ (* FIXME: Make "SPASS_NEW_HOME" legacy. *) val spass_config : atp_config = {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]), - arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ => - ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) - |> extra_options <> "" ? prefix (extra_options ^ " "), + arguments = + fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ => + "-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ + file_name + |> extra_options <> "" ? prefix (extra_options ^ " "), proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(OldSPASS, "Unrecognized option Isabelle"), @@ -489,14 +513,14 @@ val vampire_config : atp_config = {exec = (["VAMPIRE_HOME"], ["vampire"]), - arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => + arguments = fn _ => fn _ => fn sos => fn timeout => fn file_name => fn _ => "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^ " --proof tptp --output_axiom_names on" ^ (if is_vampire_at_least_1_8 () then " --forced_options propositional_to_bdd=off" else "") ^ - " --thanks \"Andrei and Krystof\" --input_file" + " --thanks \"Andrei and Krystof\" --input_file " ^ file_name |> sos = sosN ? prefix "--sos on ", proof_delims = [("=========== Refutation ==========", @@ -535,9 +559,9 @@ val z3_tptp_config : atp_config = {exec = (["Z3_HOME"], ["z3"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^ - string_of_int (to_secs 1 timeout), + string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [("\ncore(", ").")], known_failures = known_szs_status_failures, prem_role = Hypothesis, @@ -557,7 +581,7 @@ fun dummy_config format type_enc : atp_config = {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), - arguments = K (K (K (K (K "")))), + arguments = K (K (K (K (K (K ""))))), proof_delims = [], known_failures = known_szs_status_failures, prem_role = Hypothesis, @@ -623,10 +647,12 @@ fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice : atp_config = {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]), - arguments = fn _ => fn _ => fn command => fn timeout => fn _ => - (if command <> "" then "-c " ^ quote command ^ " " else "") ^ - "-s " ^ the_remote_system system_name system_versions ^ " " ^ - "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)), + arguments = + fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ => + (if command <> "" then "-c " ^ quote command ^ " " else "") ^ + "-s " ^ the_remote_system system_name system_versions ^ " " ^ + "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^ + " " ^ file_name, proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ known_says_failures, prem_role = prem_role, @@ -726,10 +752,10 @@ end val atps= - [alt_ergo, e, e_males, iprover, iprover_eq, leo2, satallax, spass, spass_poly, - vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, remote_e_tofof, - remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, - remote_vampire, remote_snark, remote_waldmeister] + [alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, + spass_poly, vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, + remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, + remote_satallax, remote_vampire, remote_snark, remote_waldmeister] val setup = fold add_atp atps diff -r ca071373b695 -r e424e17ee420 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 17 14:12:35 2013 +0100 @@ -0,0 +1,112 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML + Author: Jasmin Blanchette, TU Muenchen + Author: Steffen Juilf Smolka, TU Muenchen + +Preplaying of isar proofs. +*) + +signature SLEDGEHAMMER_PREPLAY = +sig + type isar_step = Sledgehammer_Proof.isar_step + eqtype preplay_time + val zero_preplay_time : preplay_time + val some_preplay_time : preplay_time + val add_preplay_time : preplay_time -> preplay_time -> preplay_time + val string_of_preplay_time : preplay_time -> string + val try_metis : bool -> string -> string -> Proof.context -> + Time.time -> (isar_step option * isar_step) -> unit -> preplay_time + val try_metis_quietly : bool -> string -> string -> Proof.context -> + Time.time -> (isar_step option * isar_step) -> unit -> preplay_time +end + +structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY = +struct + +open Sledgehammer_Util +open Sledgehammer_Proof + +(* The boolean flag encodes whether the time is exact (false) or an lower bound + (true) *) +type preplay_time = bool * Time.time + +val zero_preplay_time = (false, Time.zeroTime) +val some_preplay_time = (true, Time.zeroTime) + +fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) + +val string_of_preplay_time = ATP_Util.string_from_ext_time + +(* timing *) +fun take_time timeout tac arg = + let + val timing = Timing.start () + in + (TimeLimit.timeLimit timeout tac arg; + Timing.result timing |> #cpu |> pair false) + handle TimeLimit.TimeOut => (true, timeout) + end + +(* lookup facts in context *) +fun resolve_fact_names ctxt names = + names + |>> map string_for_label + |> op @ + |> maps (thms_of_name ctxt) + +exception ZEROTIME +fun try_metis debug type_enc lam_trans ctxt timeout (succedent, step) = + let + val (t, byline, obtain) = + (case step of + Prove (_, _, t, byline) => (t, byline, false) + | Obtain (_, xs, _, t, byline) => + (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis + (see ~~/src/Pure/Isar/obtain.ML) *) + let + val thesis = Term.Free ("thesis", HOLogic.boolT) + val thesis_prop = thesis |> HOLogic.mk_Trueprop + val frees = map Term.Free xs + + (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) + val inner_prop = + fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) + + (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) + val prop = + Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) + in + (prop, byline, true) + end + | _ => raise ZEROTIME) + val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) + val facts = + (case byline of + By_Metis fact_names => resolve_fact_names ctxt fact_names + | Case_Split (cases, fact_names) => + resolve_fact_names ctxt fact_names + @ (case the succedent of + Assume (_, t) => make_thm t + | Obtain (_, _, _, t, _) => make_thm t + | Prove (_, _, t, _) => make_thm t + | _ => error "preplay error: unexpected succedent of case split") + :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) + | _ => error "preplay error: malformed case split") + #> make_thm) + cases) + val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug + |> obtain ? Config.put Metis_Tactic.new_skolem true + val goal = + Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t + fun tac {context = ctxt, prems = _} = + Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 + in + take_time timeout + (fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg)) + end + handle ZEROTIME => K zero_preplay_time + +(* this version treats exceptions like timeouts *) +fun try_metis_quietly debug type_enc lam_trans ctxt timeout = + the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout + +end diff -r ca071373b695 -r e424e17ee420 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 17 14:11:26 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 17 14:12:35 2013 +0100 @@ -786,12 +786,12 @@ fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name val full_proof = debug orelse isar_proofs - val args = arguments ctxt full_proof extra - (slice_timeout |> the_default one_day) - (ord, ord_info, sel_weights) + val args = + arguments ctxt full_proof extra + (slice_timeout |> the_default one_day) + (File.shell_path prob_path) (ord, ord_info, sel_weights) val command = - "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ - File.shell_path prob_path ^ ")" + "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")" |> enclose "TIMEFORMAT='%3R'; { time " " ; }" val _ = atp_problem diff -r ca071373b695 -r e424e17ee420 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 17 14:11:26 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 17 14:12:35 2013 +0100 @@ -741,7 +741,7 @@ and do_case outer (c, infs) = Assume (label_of_clause c, prop_of_clause c) :: map (isar_step_of_direct_inf outer) infs - val (isar_proof, (preplay_fail, ext_time)) = + val (isar_proof, (preplay_fail, preplay_time)) = ref_graph |> redirect_graph axioms tainted |> map (isar_step_of_direct_inf true) @@ -771,8 +771,8 @@ let val msg = (if preplay then - [if preplay_fail then "may fail" - else string_from_ext_time ext_time] + [(if preplay_fail then "may fail, " else "") ^ + Sledgehammer_Preplay.string_of_preplay_time preplay_time] else []) @ (if verbose then diff -r ca071373b695 -r e424e17ee420 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Jan 17 14:11:26 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Jan 17 14:12:35 2013 +0100 @@ -2,15 +2,16 @@ Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen -Shrinking and preplaying of reconstructed isar proofs. +Shrinking of reconstructed isar proofs. *) signature SLEDGEHAMMER_SHRINK = sig type isar_step = Sledgehammer_Proof.isar_step + type preplay_time = Sledgehammer_Preplay.preplay_time val shrink_proof : bool -> Proof.context -> string -> string -> bool -> Time.time option - -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time)) + -> real -> isar_step list -> isar_step list * (bool * preplay_time) end structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK = @@ -18,6 +19,7 @@ open Sledgehammer_Util open Sledgehammer_Proof +open Sledgehammer_Preplay (* Parameters *) val merge_timeout_slack = 1.2 @@ -44,17 +46,6 @@ fun pop_max tab = pop tab (the (Inttab.max_key tab)) fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab -(* Timing *) -fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) -val no_time = (false, Time.zeroTime) -fun take_time timeout tac arg = - let val timing = Timing.start () in - (TimeLimit.timeLimit timeout tac arg; - Timing.result timing |> #cpu |> SOME) - handle TimeLimit.TimeOut => NONE - end - - (* Main function for shrinking proofs *) fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout isar_shrink proof = @@ -70,9 +61,11 @@ fun handle_metis_fail try_metis () = try_metis () handle exn => (if Exn.is_interrupt exn orelse debug then reraise exn - else metis_fail := true; SOME Time.zeroTime) + else metis_fail := true; some_preplay_time) fun get_time lazy_time = - if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time + if !metis_fail andalso not (Lazy.is_finished lazy_time) + then some_preplay_time + else Lazy.force lazy_time val metis_fail = fn () => !metis_fail end @@ -118,116 +111,60 @@ v_fold_index (add_if_cand proof_vect) refed_by_vect [] |> Inttab.make_list - (* Metis Preplaying *) - fun resolve_fact_names names = - names - |>> map string_for_label - |> op @ - |> maps (thms_of_name ctxt) - - (* TODO: add "Obtain" case *) - exception ZEROTIME - fun try_metis timeout (succedent, step) = - (if not preplay then K (SOME Time.zeroTime) else - let - val (t, byline, obtain) = - (case step of - Prove (_, _, t, byline) => (t, byline, false) - | Obtain (_, xs, _, t, byline) => - (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis - (see ~~/src/Pure/Isar/obtain.ML) *) - let - val thesis = Term.Free ("thesis", HOLogic.boolT) - val thesis_prop = thesis |> HOLogic.mk_Trueprop - val frees = map Term.Free xs - - (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) - val inner_prop = - fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) - - (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) - val prop = - Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) - in - (prop, byline, true) - end - | _ => raise ZEROTIME) - val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) - val facts = - (case byline of - By_Metis fact_names => resolve_fact_names fact_names - | Case_Split (cases, fact_names) => - resolve_fact_names fact_names - @ (case the succedent of - Assume (_, t) => make_thm t - | Obtain (_, _, _, t, _) => make_thm t - | Prove (_, _, t, _) => make_thm t - | _ => error "Internal error: unexpected succedent of case split") - :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) - | _ => error "Internal error: malformed case split") - #> make_thm) - cases) - val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug - |> obtain ? Config.put Metis_Tactic.new_skolem true - val goal = - Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t - fun tac {context = ctxt, prems = _} = - Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 - in - take_time timeout (fn () => goal tac) - end) - handle ZEROTIME => K (SOME Time.zeroTime) - - val try_metis_quietly = the_default NONE oo try oo try_metis - (* cache metis preplay times in lazy time vector *) val metis_time = v_map_index - (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout - o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the) + (if not preplay then K (zero_preplay_time) #> Lazy.value + else + apsnd the (* step *) + #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *) + #> try_metis debug type_enc lam_trans ctxt preplay_timeout + #> handle_metis_fail + #> Lazy.lazy) proof_vect + fun sum_up_time lazy_time_vector = Vector.foldl - ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts)) - | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout))) - o apfst get_time) - no_time lazy_time_vector + (apfst get_time #> uncurry add_preplay_time) + zero_preplay_time lazy_time_vector (* Merging *) - (* TODO: consider adding "Obtain" cases *) fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 = let val (step_constructor, lfs2, gfs2) = (case step2 of (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) => (fn by => Prove (qs2, label2, t, by), lfs2, gfs2) - | (Obtain(qs2, xs, label2, t, By_Metis (lfs2, gfs2))) => + | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) => (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) - | _ => error "Internal error: unmergeable Isar steps" ) + | _ => error "sledgehammer_shrink: unmergeable Isar steps" ) val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 val gfs = union (op =) gfs1 gfs2 in step_constructor (By_Metis (lfs, gfs)) end - | merge _ _ = error "Internal error: unmergeable Isar steps" + | merge _ _ = error "sledgehammer_shrink: unmergeable Isar steps" fun try_merge metis_time (s1, i) (s2, j) = - (case get i metis_time |> Lazy.force of - NONE => (NONE, metis_time) - | SOME t1 => - (case get j metis_time |> Lazy.force of - NONE => (NONE, metis_time) - | SOME t2 => - let - val s12 = merge s1 s2 - val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) - in - case try_metis_quietly timeout (NONE, s12) () of - NONE => (NONE, metis_time) - | some_t12 => - (SOME s12, metis_time - |> replace (Time.zeroTime |> SOME |> Lazy.value) i - |> replace (Lazy.value some_t12) j) + if not preplay then (merge s1 s2 |> SOME, metis_time) + else + (case get i metis_time |> Lazy.force of + (true, _) => (NONE, metis_time) + | (_, t1) => + (case get j metis_time |> Lazy.force of + (true, _) => (NONE, metis_time) + | (_, t2) => + let + val s12 = merge s1 s2 + val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) + in + case try_metis_quietly debug type_enc lam_trans ctxt timeout + (NONE, s12) () of + (true, _) => (NONE, metis_time) + | exact_time => + (SOME s12, metis_time + |> replace (zero_preplay_time |> Lazy.value) i + |> replace (Lazy.value exact_time) j) - end)) + end)) fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' = if Inttab.is_empty cand_tab @@ -286,20 +223,20 @@ proof |> do_case_splits rich_ctxt |>> shrink_top_level on_top_level rich_ctxt in - (proof, ext_time_add lower_level_time top_level_time) + (proof, add_preplay_time lower_level_time top_level_time) end and do_case_splits ctxt proof = let fun shrink_each_and_collect_time shrink candidates = - let fun f_m cand time = shrink cand ||> ext_time_add time - in fold_map f_m candidates no_time end + let fun f_m cand time = shrink cand ||> add_preplay_time time + in fold_map f_m candidates zero_preplay_time end val shrink_case_split = shrink_each_and_collect_time (do_proof false ctxt) fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) = let val (cases, time) = shrink_case_split cases in (Prove (qs, l, t, Case_Split (cases, facts)), time) end - | shrink step = (step, no_time) + | shrink step = (step, zero_preplay_time) in shrink_each_and_collect_time shrink proof end