diff --git a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML @@ -1,475 +1,494 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Author: Jasmin Blanchette, TU Munich Author: Sascha Boehme, TU Munich Author: Tobias Nipkow, TU Munich Author: Makarius Author: Martin Desharnais, UniBw Munich, MPI-INF Saarbruecken Mirabelle action: "sledgehammer". *) structure Mirabelle_Sledgehammer: MIRABELLE_ACTION = struct (*To facilitate synching the description of Mirabelle Sledgehammer parameters (in ../lib/Tools/mirabelle) with the parameters actually used by this interface, the former extracts PARAMETER and DESCRIPTION from code below which has this pattern (provided it appears in a single line): val .*K = "PARAMETER" (*DESCRIPTION*) *) (* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) +val exhaustive_preplayK = "exhaustive_preplay" (*=BOOL: show exhaustive preplay data*) val keep_probsK = "keep_probs" (*=BOOL: keep temporary problem files created by sledgehammer*) val keep_proofsK = "keep_proofs" (*=BOOL: keep temporary proof files created by ATPs*) val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*) (*defaults used in this Mirabelle action*) val check_trivial_default = false +val exhaustive_preplay_default = false val keep_probs_default = false val keep_proofs_default = false datatype sh_data = ShData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, lemmas: int, max_lems: int, time_isa: int, time_prover: int} datatype re_data = ReData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, proofs: int, time: int, timeout: int, lemmas: int * int * int, posns: (Position.T * bool) list } fun make_sh_data (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, time_prover) = ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, time_isa=time_isa, time_prover=time_prover} fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, timeout,lemmas,posns) = ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns} val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0) val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover}) = (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns) datatype data = Data of { sh: sh_data, re_u: re_data (* proof method with unminimized set of lemmas *) } type change_data = (data -> data) -> unit fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} val empty_data = make_data (empty_sh_data, empty_re_data) fun map_sh_data f (Data {sh, re_u}) = let val sh' = make_sh_data (f (tuple_of_sh_data sh)) in make_data (sh', re_u) end fun map_re_data f (Data {sh, re_u}) = let val f' = make_re_data o f o tuple_of_re_data val re_u' = f' re_u in make_data (sh, re_u') end fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); val inc_sh_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover)) val inc_sh_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover)) val inc_sh_nontriv_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover)) val inc_sh_nontriv_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover)) fun inc_sh_lemmas n = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => (calls, success, nontriv_calls, nontriv_success, lemmas+n, max_lems, time_isa, time_prover)) fun inc_sh_max_lems n = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => (calls, success,nontriv_calls, nontriv_success, lemmas, Int.max (max_lems, n), time_isa, time_prover)) fun inc_sh_time_isa t = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa + t, time_prover)) fun inc_sh_time_prover t = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover + t)) val inc_proof_method_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) val inc_proof_method_proofs = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) fun inc_proof_method_time t = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) val inc_proof_method_timeout = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) fun inc_proof_method_lemmas n = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) fun inc_proof_method_posns pos = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) val str0 = string_of_int o the_default 0 local val str = string_of_int val str3 = Real.fmt (StringCvt.FIX (SOME 3)) fun percentage a b = string_of_int (a * 100 div b) fun ms t = Real.fromInt t / 1000.0 fun avg_time t n = if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 fun log_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover}) = "\nTotal number of sledgehammer calls: " ^ str calls ^ "\nNumber of successful sledgehammer calls: " ^ str success ^ "\nNumber of sledgehammer lemmas: " ^ str lemmas ^ "\nMax number of sledgehammer lemmas: " ^ str max_lems ^ "\nSuccess rate: " ^ percentage success calls ^ "%" ^ "\nTotal number of nontrivial sledgehammer calls: " ^ str nontriv_calls ^ "\nNumber of successful nontrivial sledgehammer calls: " ^ str nontriv_success ^ "\nTotal time for sledgehammer calls (Isabelle): " ^ str3 (ms time_isa) ^ "\nTotal time for successful sledgehammer calls (ATP): " ^ str3 (ms time_prover) ^ "\nAverage time for sledgehammer calls (Isabelle): " ^ str3 (avg_time time_isa calls) ^ "\nAverage time for successful sledgehammer calls (ATP): " ^ str3 (avg_time time_prover success) fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = let val proved = posns |> map (fn (pos, triv) => str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ (if triv then "[T]" else "")) in "\nTotal number of proof method calls: " ^ str calls ^ "\nNumber of successful proof method calls: " ^ str success ^ " (proof: " ^ str proofs ^ ")" ^ "\nNumber of proof method timeouts: " ^ str timeout ^ "\nSuccess rate: " ^ percentage success sh_calls ^ "%" ^ "\nTotal number of nontrivial proof method calls: " ^ str nontriv_calls ^ "\nNumber of successful nontrivial proof method calls: " ^ str nontriv_success ^ " (proof: " ^ str proofs ^ ")" ^ "\nNumber of successful proof method lemmas: " ^ str lemmas ^ "\nSOS of successful proof method lemmas: " ^ str lems_sos ^ "\nMax number of successful proof method lemmas: " ^ str lems_max ^ "\nTotal time for successful proof method calls: " ^ str3 (ms time) ^ "\nAverage time for successful proof method calls: " ^ str3 (avg_time time success) ^ "\nProved: " ^ space_implode " " proved end in fun log_data (Data {sh, re_u}) = let val ShData {calls=sh_calls, ...} = sh val ReData {calls=re_calls, ...} = re_u in if sh_calls > 0 then let val text1 = log_sh_data sh in if re_calls > 0 then text1 ^ "\n" ^ log_re_data sh_calls re_u else text1 end else "" end end type stature = ATP_Problem_Generate.stature fun is_good_line s = (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) andalso not (String.isSubstring "(> " s) andalso not (String.isSubstring ", > " s) andalso not (String.isSubstring "may fail" s) (* Fragile hack *) fun proof_method_from_msg args msg = (case AList.lookup (op =) args proof_methodK of SOME name => if name = "smart" then if exists is_good_line (split_lines msg) then "none" else "fail" else name | NONE => if exists is_good_line (split_lines msg) then "none" (* trust the preplayed proof *) else if String.isSubstring "metis (" msg then msg |> Substring.full |> Substring.position "metis (" |> snd |> Substring.position ")" |> fst |> Substring.string |> suffix ")" else if String.isSubstring "metis" msg then "metis" else "smt") local fun run_sh params keep pos state = let fun set_file_name (SOME (dir, keep_probs, keep_proofs)) = let val filename = "prob_" ^ StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^ StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos)) in Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__") #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir) #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir) #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ()) end | set_file_name NONE = I val state' = state |> Proof.map_context (set_file_name keep) val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () => Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1 Sledgehammer_Fact.no_fact_override state') () in (sledgehammer_outcome, msg, cpu_time) end handle ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0) | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0) in fun run_sledgehammer (params as {provers, ...}) output_dir keep_probs keep_proofs - proof_method_from_msg thy_index trivial pos st = + exhaustive_preplay proof_method_from_msg thy_index trivial pos st = let val thy = Proof.theory_of st val thy_name = Context.theory_name thy val triv_str = if trivial then "[T] " else "" val keep = if keep_probs orelse keep_proofs then let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in Path.append output_dir (Path.basic subdir) |> Isabelle_System.make_directory |> Path.implode |> (fn dir => SOME (dir, keep_probs, keep_proofs)) end else NONE val prover_name = hd provers val (sledgehamer_outcome, msg, cpu_time) = run_sh params keep pos st - val (time_prover, change_data, proof_method_and_used_thms) = + val (time_prover, change_data, proof_method_and_used_thms, exhaustive_preplay_msg) = (case sledgehamer_outcome of - Sledgehammer.SH_Some {used_facts, run_time, ...} => + Sledgehammer.SH_Some ({used_facts, run_time, ...}, preplay_results) => let val num_used_facts = length used_facts val time_prover = Time.toMilliseconds run_time fun get_thms (name, stature) = try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) name |> Option.map (pair (name, stature)) val change_data = inc_sh_success #> not trivial ? inc_sh_nontriv_success #> inc_sh_lemmas num_used_facts #> inc_sh_max_lems num_used_facts #> inc_sh_time_prover time_prover + + val exhaustive_preplay_msg = + if exhaustive_preplay then + preplay_results + |> map + (fn (meth, play_outcome, used_facts) => + "Preplay: " ^ + Sledgehammer_Proof_Methods.string_of_proof_method (map fst used_facts) meth ^ + " (" ^ Sledgehammer_Proof_Methods.string_of_play_outcome play_outcome ^ ")") + |> cat_lines + else + "" in (SOME time_prover, change_data, - SOME (proof_method_from_msg msg, map_filter get_thms used_facts)) + SOME (proof_method_from_msg msg, map_filter get_thms used_facts), + exhaustive_preplay_msg) end - | _ => (NONE, I, NONE)) + | _ => (NONE, I, NONE, "")) val outcome_msg = "(SH " ^ string_of_int cpu_time ^ "ms" ^ (case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^ ") [" ^ prover_name ^ "]: " in - (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg, change_data #> inc_sh_time_isa cpu_time, + (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg ^ + (if exhaustive_preplay_msg = "" then "" else ("\n" ^ exhaustive_preplay_msg)), + change_data #> inc_sh_time_isa cpu_time, proof_method_and_used_thms) end end fun override_params prover type_enc timeout = [("provers", prover), ("max_facts", "0"), ("type_enc", type_enc), ("strict", "true"), ("slice", "false"), ("timeout", timeout |> Time.toSeconds |> string_of_int)] fun run_proof_method trivial full name meth named_thms timeout pos st = let fun do_method named_thms ctxt = let val ref_of_str = (* FIXME proper wrapper for parser combinators *) suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none #> Parse.thm #> fst val thms = named_thms |> maps snd val facts = named_thms |> map (ref_of_str o fst o fst) val fact_override = {add = facts, del = [], only = true} fun my_timeout time_slice = timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal fun sledge_tac time_slice prover type_enc = Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt (override_params prover type_enc (my_timeout time_slice)) fact_override [] in if meth = "sledgehammer_tac" then sledge_tac 0.25 ATP_Proof.vampireN "mono_native" ORELSE' sledge_tac 0.25 ATP_Proof.eN "poly_guards??" ORELSE' sledge_tac 0.25 ATP_Proof.spassN "mono_native" ORELSE' SMT_Solver.smt_tac ctxt thms else if meth = "smt" then SMT_Solver.smt_tac ctxt thms else if full then Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if String.isPrefix "metis (" meth then let val (type_encs, lam_trans) = meth |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start |> filter Token.is_proper |> tl |> Metis_Tactic.parse_metis_options |> fst |>> the_default [ATP_Proof_Reconstruct.partial_typesN] ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end else if meth = "metis" then Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if meth = "none" then K all_tac else if meth = "fail" then K no_tac else (warning ("Unknown method " ^ quote meth); K no_tac) end fun apply_method named_thms = Mirabelle.can_apply timeout (do_method named_thms) st fun with_time (false, t) = ("failed (" ^ string_of_int t ^ ")", I) | with_time (true, t) = ("succeeded (" ^ string_of_int t ^ ")", inc_proof_method_success #> not trivial ? inc_proof_method_nontriv_success #> inc_proof_method_lemmas (length named_thms) #> inc_proof_method_time t #> inc_proof_method_posns (pos, trivial) #> name = "proof" ? inc_proof_method_proofs) fun timed_method named_thms = with_time (Mirabelle.cpu_time apply_method named_thms) handle Timeout.TIMEOUT _ => ("timeout", inc_proof_method_timeout) | ERROR msg => ("error: " ^ msg, I) in timed_method named_thms |> apsnd (fn change_data => change_data #> inc_proof_method_calls #> not trivial ? inc_proof_method_nontriv_calls) end val try0 = Try0.try0 (SOME (Time.fromSeconds 5)) ([], [], [], []) fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) = let (* Parse Mirabelle-specific parameters *) val check_trivial = Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default) val keep_probs = Mirabelle.get_bool_argument arguments (keep_probsK, keep_probs_default) val keep_proofs = Mirabelle.get_bool_argument arguments (keep_proofsK, keep_proofs_default) + val exhaustive_preplay = + Mirabelle.get_bool_argument arguments (exhaustive_preplayK, exhaustive_preplay_default) val proof_method_from_msg = proof_method_from_msg arguments val params = Sledgehammer_Commands.default_params \<^theory> arguments val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data val init_msg = "Params for sledgehammer: " ^ Sledgehammer_Prover.string_of_params params fun run ({theory_index, name, pos, pre, ...} : Mirabelle.command) = let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then "" else let val trivial = check_trivial andalso try0 pre handle Timeout.TIMEOUT _ => false val (outcome, log1, change_data1, proof_method_and_used_thms) = - run_sledgehammer params output_dir keep_probs keep_proofs proof_method_from_msg - theory_index trivial pos pre + run_sledgehammer params output_dir keep_probs keep_proofs exhaustive_preplay + proof_method_from_msg theory_index trivial pos pre val (log2, change_data2) = (case proof_method_and_used_thms of SOME (proof_method, used_thms) => run_proof_method trivial false name proof_method used_thms timeout pos pre |> apfst (prefix (proof_method ^ " (sledgehammer): ")) | NONE => ("", I)) val () = Synchronized.change data (change_data1 #> change_data2 #> inc_sh_calls #> not trivial ? inc_sh_nontriv_calls) in log1 ^ "\n" ^ log2 |> Symbol.trim_blanks |> prefix_lines (Sledgehammer.short_string_of_sledgehammer_outcome outcome ^ " ") end end fun finalize () = log_data (Synchronized.value data) in (init_msg, {run = run, finalize = finalize}) end val () = Mirabelle.register_action "sledgehammer" make_action end diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer.ML b/src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML @@ -1,479 +1,505 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Sledgehammer's heart. *) signature SLEDGEHAMMER = sig type stature = ATP_Problem_Generate.stature type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params type induction_rules = Sledgehammer_Prover.induction_rules type prover_problem = Sledgehammer_Prover.prover_problem type prover_result = Sledgehammer_Prover.prover_result + type preplay_result = proof_method * play_outcome * (string * stature) list + datatype sledgehammer_outcome = - SH_Some of prover_result + SH_Some of prover_result * preplay_result list | SH_Unknown | SH_Timeout | SH_None val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string - - val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int -> - proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome) val string_of_factss : (string * fact list) list -> string val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> Proof.state -> bool * (sledgehammer_outcome * string) end; structure Sledgehammer : SLEDGEHAMMER = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Minimize open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh +type preplay_result = proof_method * play_outcome * (string * stature) list + datatype sledgehammer_outcome = - SH_Some of prover_result + SH_Some of prover_result * preplay_result list | SH_Unknown | SH_Timeout | SH_None fun short_string_of_sledgehammer_outcome (SH_Some _) = "some" | short_string_of_sledgehammer_outcome SH_Unknown = "unknown" | short_string_of_sledgehammer_outcome SH_Timeout = "timeout" | short_string_of_sledgehammer_outcome SH_None = "none" fun alternative f (SOME x) (SOME y) = SOME (f (x, y)) | alternative _ (x as SOME _) NONE = x | alternative _ NONE (y as SOME _) = y | alternative _ NONE NONE = NONE fun max_outcome outcomes = let val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes val none = find_first (fn (SH_None, _) => true | _ => false) outcomes in some |> alternative snd unknown |> alternative snd timeout |> alternative snd none |> the_default (SH_Unknown, "") end -fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) = +fun play_one_line_proofs minimize timeout used_facts state i methss = (if timeout = Time.zeroTime then - (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) + [] else let val ctxt = Proof.context_of state - - val fact_names = used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained) |> map fst + val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts + val fact_names = map fst used_facts val {facts = chained, goal, ...} = Proof.goal state val goal_t = Logic.get_goal (Thm.prop_of goal) i - fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) - | try_methss ress [] = - (used_facts, - (case AList.lookup (op =) ress preferred_meth of - SOME play => (preferred_meth, play) - | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress)))) + fun try_methss ress [] = ress | try_methss ress (meths :: methss) = let - fun mk_step fact_names meths = + fun mk_step meths = Prove { qualifiers = [], obtains = [], label = ("", 0), goal = goal_t, subproofs = [], facts = ([], fact_names), proof_methods = meths, comment = ""} + val ress' = + preplay_isar_step ctxt chained timeout [] (mk_step meths) + |> map (fn result as (meth, play_outcome) => + (case (minimize, play_outcome) of + (true, Played time) => + let + val (time', used_names') = + minimized_isar_step ctxt chained time (mk_step [meth]) + ||> (facts_of_isar_step #> snd) + val used_facts' = filter (member (op =) used_names' o fst) used_facts + in + (meth, Played time', used_facts') + end + | _ => (meth, play_outcome, used_facts))) + val any_succeeded = exists (fn (_, Played _, _) => true | _ => false) ress' in - (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of - (res as (meth, Played time)) :: _ => - if not minimize then - (used_facts, res) - else - let - val (time', used_names') = - minimized_isar_step ctxt chained time (mk_step fact_names [meth]) - ||> (facts_of_isar_step #> snd) - val used_facts' = filter (member (op =) used_names' o fst) used_facts - in - (used_facts', (meth, Played time')) - end - | ress' => try_methss (ress' @ ress) methss) + try_methss (ress' @ ress) (if any_succeeded then [] else methss) end in try_methss [] methss end) - |> (fn (used_facts, (meth, play)) => - (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play))) + |> map (fn (meth, play_outcome, used_facts) => (meth, play_outcome, filter_out (fn (_, (sc, _)) => sc = Chained) used_facts)) + |> sort (play_outcome_ord o apply2 (fn (_, play_outcome, _) => play_outcome)) + +fun select_one_line_proof used_facts preferred_meth preplay_results = + (case preplay_results of + [] => (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) + | (best_meth, best_outcome, best_used_facts) :: results' => + let + val (prefered_outcome, prefered_used_facts) = + (case find_first (fn (meth, _, _) => meth = preferred_meth) preplay_results of + NONE => (Play_Timed_Out Time.zeroTime, used_facts) + | SOME (_, prefered_outcome, prefered_used_facts) => + (prefered_outcome, prefered_used_facts)) + in + (case (prefered_outcome, best_outcome) of + (* If prefered_meth succeeded, use it irrespective of other preplay results *) + (Played _, _) => (prefered_used_facts, (preferred_meth, prefered_outcome)) + (* If prefered_meth did not succeed but best method did, use best method *) + | (_, Played _) => (best_used_facts, (best_meth, best_outcome)) + (* If neither succeeded, use preferred_meth *) + | (_, _) => (prefered_used_facts, (preferred_meth, prefered_outcome))) + end) + |> apfst (filter_out (fn (_, (sc, _)) => sc = Chained)) fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn (problem as {state, subgoal, factss, ...} : prover_problem) (slice as ((slice_size, num_facts, fact_filter), _)) name = let val ctxt = Proof.context_of state val _ = spying spy (fn () => (state, subgoal, name, "Launched")) val _ = if verbose then writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^ "...") else () 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) |> commas |> prefix ("Facts in " ^ name ^ " proof: ") |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = let val num_used_facts = length used_facts fun find_indices facts = tag_list 1 facts |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> distinct (eq_fst (op =)) |> map (prefix "@" o string_of_int o snd) fun filter_info (fact_filter, facts) = let val indices = find_indices facts (* "Int.max" is there for robustness *) val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" in (commas (indices @ unknowns), fact_filter) end val filter_infos = map filter_info (("actual", used_from) :: factss) |> AList.group (op =) |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) in "Success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts ^ (if num_used_facts = 0 then "" else ": " ^ commas filter_infos) end | spying_str_of_res {outcome = SOME failure, ...} = "Failure: " ^ string_of_atp_failure failure in get_minimizing_prover ctxt mode learn name params problem slice |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => print_used_facts used_facts used_from | _ => ()) |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) end fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) = let - val output = + val (output, chosen_preplay_outcome) = if outcome = SOME ATP_Proof.TimedOut then - SH_Timeout + (SH_Timeout, select_one_line_proof used_facts (fst preferred_methss) []) else if is_some outcome then - SH_None + (SH_None, select_one_line_proof used_facts (fst preferred_methss) []) else - SH_Some result - fun output_message () = message (fn () => - play_one_line_proof minimize preplay_timeout used_facts state subgoal preferred_methss) + let + val preplay_results = + play_one_line_proofs minimize preplay_timeout used_facts state subgoal + (snd preferred_methss) + val chosen_preplay_outcome = + select_one_line_proof used_facts (fst preferred_methss) preplay_results + in + (SH_Some (result, preplay_results), chosen_preplay_outcome) + end + fun output_message () = message (fn () => chosen_preplay_outcome) in (output, output_message) end fun check_expected_outcome ctxt prover_name expect outcome = let val outcome_code = short_string_of_sledgehammer_outcome outcome in (* The "expect" argument is deliberately ignored if the prover is missing so that "Metis_Examples" can be processed on any machine. *) if expect = "" orelse outcome_code = expect orelse not (is_prover_installed ctxt prover_name) then () else error ("Unexpected outcome: " ^ quote outcome_code) end fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result learn (problem as {state, subgoal, ...}) slice prover_name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout fun really_go () = launch_prover params mode learn problem slice prover_name |> preplay_prover_result params state subgoal fun go () = if debug then really_go () else (really_go () handle ERROR msg => (SH_Unknown, fn () => "Error: " ^ msg ^ "\n") | exn => if Exn.is_interrupt exn then Exn.reraise exn else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) val (outcome, message) = Timeout.apply hard_timeout go () val () = check_expected_outcome ctxt prover_name expect outcome val message = message () val () = if mode = Auto_Try then () else (case outcome of SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message) | _ => ()) in (outcome, message) end fun string_of_facts filter facts = "Selected " ^ string_of_int (length facts) ^ " " ^ (if filter = "" then "" else filter ^ " ") ^ "fact" ^ plural_s (length facts) ^ ": " ^ (space_implode " " (map (fst o fst) facts)) fun string_of_factss factss = if forall (null o snd) factss then "Found no relevant facts" else cat_lines (map (fn (filter, facts) => string_of_facts filter facts) factss) val default_slice_schedule = (* FUDGE (inspired by Seventeen evaluation) *) [cvc4N, zipperpositionN, vampireN, veritN, eN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN, vampireN, vampireN, zipperpositionN, z3N, cvc4N, vampireN, iproverN, vampireN, zipperpositionN, z3N, z3N, cvc4N, cvc4N] fun schedule_of_provers provers num_slices = let val (known_provers, unknown_provers) = List.partition (member (op =) default_slice_schedule) provers val default_slice_schedule = filter (member (op =) known_provers) default_slice_schedule val num_default_slices = length default_slice_schedule fun round_robin _ [] = [] | round_robin 0 _ = [] | round_robin n (prover :: provers) = prover :: round_robin (n - 1) (provers @ [prover]) in if num_slices <= num_default_slices then take num_slices default_slice_schedule else default_slice_schedule @ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers) end fun prover_slices_of_schedule ctxt factss ({max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, ...} : params) schedule = let fun triplicate_slices original = let val shift = map (apfst (fn (slice_size, num_facts, fact_filter) => (slice_size, num_facts, if fact_filter = mashN then mepoN else if fact_filter = mepoN then meshN else mashN))) val shifted_once = shift original val shifted_twice = shift shifted_once in original @ shifted_once @ shifted_twice end fun adjust_extra (ATP_Slice (format0, type_enc0, lam_trans0, uncurried_aliases0, extra_extra0)) = ATP_Slice (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans, the_default uncurried_aliases0 uncurried_aliases, extra_extra0) | adjust_extra (extra as SMT_Slice _) = extra fun adjust_slice max_slice_size ((slice_size0, num_facts0, fact_filter0), extra) = let val slice_size = Int.min (max_slice_size, slice_size0) val fact_filter = fact_filter |> the_default fact_filter0 val max_facts = max_facts |> the_default num_facts0 val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss)) in ((slice_size, num_facts, fact_filter), adjust_extra extra) end val provers = distinct (op =) schedule val prover_slices = map (fn prover => (prover, (is_none fact_filter ? triplicate_slices) (get_slices ctxt prover))) provers val max_threads = Multithreading.max_threads () fun translate_schedule _ 0 _ = [] | translate_schedule _ _ [] = [] | translate_schedule prover_slices slices_left (prover :: schedule) = (case AList.lookup (op =) prover_slices prover of SOME (slice0 :: slices) => let val prover_slices' = AList.update (op =) (prover, slices) prover_slices val slice as ((slice_size, _, _), _) = adjust_slice ((slices_left + max_threads - 1) div max_threads) slice0 in (prover, slice) :: translate_schedule prover_slices' (slices_left - slice_size) schedule end | _ => translate_schedule prover_slices slices_left schedule) in translate_schedule prover_slices (length schedule) schedule |> distinct (op =) end fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state = if null provers then error "No prover is set" else (case subgoal_count state of 0 => (error "No subgoal!"; (false, (SH_None, ""))) | n => let val _ = Proof.assert_backward state val print = if mode = Normal andalso is_none writeln_result then writeln else K () val found_proofs = Synchronized.var "found_proofs" 0 fun found_proof prover_name = if mode = Normal then (Synchronized.change found_proofs (fn n => n + 1); (the_default writeln writeln_result) (prover_name ^ " found a proof...")) else () val ctxt = Proof.context_of state val inst_inducts = induction_rules = SOME Instantiate val {facts = chained_thms, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt val _ = (case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name) | NONE => ()) val _ = print "Sledgehammering..." val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode")) val ({elapsed, ...}, all_facts) = Timing.timing (nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts) concl_t val _ = spying spy (fn () => (state, i, "All", "Extracting " ^ string_of_int (length all_facts) ^ " facts from background theory in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) val spying_str_of_factss = commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) fun get_factss provers = let val max_max_facts = (case max_facts of SOME n => n | NONE => fold (fn prover => fold (fn ((_, n, _), _) => Integer.max n) (get_slices ctxt prover)) provers 0) * 51 div 50 (* some slack to account for filtering of induction facts below *) val ({elapsed, ...}, factss) = Timing.timing (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t) all_facts val induction_rules = the_default (if only then Include else Exclude) induction_rules val factss = map (apsnd (maybe_filter_out_induction_rules induction_rules)) factss val () = spying spy (fn () => (state, i, "All", "Filtering facts in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms (MaSh algorithm: " ^ str_of_mash_algorithm (the_mash_algorithm ()) ^ ")")); val () = if verbose then print (string_of_factss factss) else () val () = spying spy (fn () => (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)) in factss end fun launch_provers () = let val factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss, found_proof = found_proof} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) val launch = launch_prover_and_preplay params mode writeln_result learn val schedule = if mode = Auto_Try then provers else schedule_of_provers provers slices val prover_slices = prover_slices_of_schedule ctxt factss params schedule val _ = if verbose then writeln ("Running " ^ commas (map fst prover_slices) ^ "...") else () in if mode = Auto_Try then (SH_Unknown, "") |> fold (fn (prover, slice) => fn accum as (SH_Some _, _) => accum | _ => launch problem slice prover) prover_slices else (learn chained_thms; Par_List.map (fn (prover, slice) => if Synchronized.value found_proofs < max_proofs then launch problem slice prover else (SH_None, "")) prover_slices |> max_outcome) end in (launch_provers () handle Timeout.TIMEOUT _ => (SH_Timeout, "")) |> `(fn (outcome, message) => (case outcome of SH_Some _ => (the_default writeln writeln_result "QED"; true) | SH_Unknown => (the_default writeln writeln_result message; false) | SH_Timeout => (the_default writeln writeln_result "No proof found"; false) | SH_None => (the_default writeln writeln_result (if message = "" then "No proof found" else "Error: " ^ message); false))) end) end;