# HG changeset patch # User smolkas # Date 1358420194 -3600 # Node ID beb95bf66b21f4fa800eb07b41753699fcc7ce6e # Parent 141d8f575f6ff408deba475a279737e1239b92a1 changed type of preplay time; tuned preplaying diff -r 141d8f575f6f -r beb95bf66b21 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 17 11:55:40 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 17 11:56:34 2013 +0100 @@ -2,16 +2,21 @@ Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen -Preplaying of reconstructed isar proofs. +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 -> Time.time option + 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 -> Time.time option + Time.time -> (isar_step option * isar_step) -> unit -> preplay_time end structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY = @@ -20,13 +25,25 @@ 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 |> SOME) - handle TimeLimit.TimeOut => NONE + (TimeLimit.timeLimit timeout tac arg; + Timing.result timing |> #cpu |> pair false) + handle TimeLimit.TimeOut => (true, timeout) end (* lookup facts in context *) @@ -71,9 +88,9 @@ Assume (_, t) => make_thm t | Obtain (_, _, _, t, _) => make_thm t | Prove (_, _, t, _) => make_thm t - | _ => error "Preplay error: unexpected succedent of case split") + | _ => error "preplay error: unexpected succedent of case split") :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) - | _ => error "Preplay error: malformed case split") + | _ => error "preplay error: malformed case split") #> make_thm) cases) val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug @@ -83,12 +100,13 @@ fun tac {context = ctxt, prems = _} = Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 in - take_time timeout (fn () => goal tac) + take_time timeout + (fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg)) end - handle ZEROTIME => K (SOME Time.zeroTime) + handle ZEROTIME => K zero_preplay_time -(* this version does not throw exceptions but returns NONE instead *) -fun try_metis_quietly debug type_enc lam_trans ctxt = - the_default NONE oo try oo try_metis debug type_enc lam_trans ctxt +(* 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 141d8f575f6f -r beb95bf66b21 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 17 11:55:40 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 17 11:56:34 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 141d8f575f6f -r beb95bf66b21 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Jan 17 11:55:40 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Jan 17 11:56:34 2013 +0100 @@ -8,9 +8,10 @@ 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 = @@ -45,10 +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) - (* Main function for shrinking proofs *) fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout isar_shrink proof = @@ -64,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 @@ -115,10 +114,10 @@ (* cache metis preplay times in lazy time vector *) val metis_time = v_map_index - (if not preplay then K (SOME Time.zeroTime) #> Lazy.value + (if not preplay then K (zero_preplay_time) #> Lazy.value else - apsnd the - #> apfst (fn i => try (get (i-1) #> the) proof_vect) + 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) @@ -126,47 +125,46 @@ 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 debug type_enc lam_trans ctxt 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 @@ -225,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