# HG changeset patch # User blanchet # Date 1359651245 -3600 # Node ID e8ff34a1fa9a1ddd3c4c4adb86f847a4bfa79fb5 # Parent e096c0dc538b6a1f723798e448549aa33851cda8 thread through fact triple component from which used facts come, for accurate index output diff -r e096c0dc538b -r e8ff34a1fa9a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100 @@ -456,13 +456,14 @@ NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) fun failed failure = - ({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime, + ({outcome = SOME failure, used_facts = [], used_from = [], + run_time = Time.zeroTime, preplay = Lazy.value (Sledgehammer_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis), message = K "", message_tail = ""}, ~1) - val ({outcome, used_facts, run_time, preplay, message, message_tail} + val ({outcome, used_facts, run_time, preplay, message, message_tail, ...} : Sledgehammer_Provers.prover_result, - time_isa) = time_limit (Mirabelle.cpu_time (fn () => + time_isa) = time_limit (Mirabelle.cpu_time (fn () => let val _ = if is_appropriate_prop concl_t then () else raise Fail "inappropriate" diff -r e096c0dc538b -r e8ff34a1fa9a src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 31 17:54:05 2013 +0100 @@ -269,7 +269,7 @@ (params as {verbose, isar_proofs, minimize, ...}) ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...} : prover_problem) - (result as {outcome, used_facts, run_time, preplay, message, + (result as {outcome, used_facts, used_from, run_time, preplay, message, message_tail} : prover_result) = if is_some outcome orelse null used_facts then result @@ -317,8 +317,9 @@ in case used_facts of SOME used_facts => - {outcome = NONE, used_facts = used_facts, run_time = run_time, - preplay = preplay, message = message, message_tail = message_tail} + {outcome = NONE, used_facts = used_facts, used_from = used_from, + run_time = run_time, preplay = preplay, message = message, + message_tail = message_tail} | NONE => result end diff -r e096c0dc538b -r e8ff34a1fa9a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100 @@ -72,7 +72,8 @@ type prover_result = {outcome : failure option, - used_facts : (string * stature) list, (* FIXME: store triple component *) + used_facts : (string * stature) list, + used_from : fact list, run_time : Time.time, preplay : play Lazy.lazy, message : play -> string, @@ -359,6 +360,7 @@ type prover_result = {outcome : failure option, used_facts : (string * stature) list, + used_from : fact list, run_time : Time.time, preplay : play Lazy.lazy, message : play -> string, @@ -909,8 +911,9 @@ ([], Lazy.value (Failed_to_Play plain_metis), fn _ => string_for_failure failure, "") in - {outcome = outcome, used_facts = used_facts, run_time = run_time, - preplay = preplay, message = message, message_tail = message_tail} + {outcome = outcome, used_facts = used_facts, used_from = facts (* ### *), + run_time = run_time, preplay = preplay, message = message, + message_tail = message_tail} end (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until @@ -970,7 +973,7 @@ val ctxt = Proof.context_of state |> repair_context val state = state |> Proof.map_context (K ctxt) val max_slices = if slice then Config.get ctxt smt_max_slices else 1 - fun do_slice timeout slice outcome0 time_so_far facts = + fun do_slice timeout slice outcome0 time_so_far weighted_facts = let val timer = Timer.startRealTimer () val state = @@ -989,7 +992,7 @@ end else timeout - val num_facts = length facts + val num_facts = length weighted_facts val _ = if debug then quote name ^ " slice " ^ string_of_int slice ^ " with " ^ @@ -1005,7 +1008,8 @@ if debug then Output.urgent_message "Invoking SMT solver..." else () val state_facts = these (try (#facts o Proof.goal) state) val (outcome, used_facts) = - SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i + SMT_Solver.smt_filter_preprocess ctxt state_facts goal weighted_facts + i |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day) |> (fn {outcome, used_facts} => (outcome, used_facts)) handle exn => if Exn.is_interrupt exn then @@ -1047,12 +1051,14 @@ else () in - facts |> take new_num_facts - |> do_slice timeout (slice + 1) outcome0 time_so_far + weighted_facts + |> take new_num_facts + |> do_slice timeout (slice + 1) outcome0 time_so_far end else {outcome = if is_none outcome then NONE else the outcome0, - used_facts = used_facts, run_time = time_so_far} + used_facts = used_facts, used_from = map (apsnd snd) weighted_facts, + run_time = time_so_far} end in do_slice timeout 1 NONE Time.zeroTime end @@ -1066,7 +1072,7 @@ val facts = facts ~~ (0 upto num_facts - 1) |> map (weight_smt_fact ctxt num_facts) - val {outcome, used_facts = used_pairs, run_time} = + val {outcome, used_facts = used_pairs, used_from, run_time} = smt_filter_loop name params state goal subgoal facts val used_facts = used_pairs |> map fst val outcome = outcome |> Option.map failure_from_smt_failure @@ -1094,8 +1100,9 @@ (Lazy.value (Failed_to_Play plain_metis), fn _ => string_for_failure failure, "") in - {outcome = outcome, used_facts = used_facts, run_time = run_time, - preplay = preplay, message = message, message_tail = message_tail} + {outcome = outcome, used_facts = used_facts, used_from = used_from, + run_time = run_time, preplay = preplay, message = message, + message_tail = message_tail} end fun run_reconstructor mode name @@ -1118,8 +1125,8 @@ verbose timeout facts state subgoal reconstr [reconstr] of play as Played (_, time) => - {outcome = NONE, used_facts = used_facts, run_time = time, - preplay = Lazy.value play, + {outcome = NONE, used_facts = used_facts, used_from = facts, + run_time = time, preplay = Lazy.value play, message = fn play => let @@ -1135,8 +1142,8 @@ let val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut in - {outcome = SOME failure, used_facts = [], run_time = Time.zeroTime, - preplay = Lazy.value play, + {outcome = SOME failure, used_facts = [], used_from = [], + run_time = Time.zeroTime, preplay = Lazy.value play, message = fn _ => string_for_failure failure, message_tail = ""} end end diff -r e096c0dc538b -r e8ff34a1fa9a src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100 @@ -88,8 +88,8 @@ ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false)) #> take num_facts)} - fun print_used_facts used_facts = - tag_list 1 facts + fun print_used_facts used_facts used_from = + tag_list 1 used_from |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) @@ -100,9 +100,10 @@ fun really_go () = problem |> get_minimizing_isar_prover ctxt mode learn name params minimize_command - |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} => - print_used_facts used_facts - | _ => ()) + |> verbose + ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => + print_used_facts used_facts used_from + | _ => ()) |> (fn {outcome, preplay, message, message_tail, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN