diff --git a/src/HOL/TPTP/atp_problem_import.ML b/src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML +++ b/src/HOL/TPTP/atp_problem_import.ML @@ -1,323 +1,321 @@ (* Title: HOL/TPTP/atp_problem_import.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2012 Import TPTP problems as Isabelle terms or goals. *) signature ATP_PROBLEM_IMPORT = sig val read_tptp_file : theory -> (string * term -> 'a) -> string -> 'a list * ('a list * 'a list) * local_theory val nitpick_tptp_file : theory -> int -> string -> unit val refute_tptp_file : theory -> int -> string -> unit val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool val SOLVE_TIMEOUT : int -> string -> tactic -> tactic val atp_tac : local_theory -> int -> (string * string) list -> int -> term list -> string -> int -> tactic val smt_solver_tac : string -> local_theory -> int -> tactic val make_conj : term list * term list -> term list -> term val sledgehammer_tptp_file : theory -> int -> string -> unit val isabelle_tptp_file : theory -> int -> string -> unit val isabelle_hot_tptp_file : theory -> int -> string -> unit val translate_tptp_file : theory -> string -> string -> unit end; structure ATP_Problem_Import : ATP_PROBLEM_IMPORT = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate val debug = false val overlord = false (** TPTP parsing **) fun exploded_absolute_path file_name = Path.explode file_name |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD")) fun read_tptp_file thy postproc file_name = let fun has_role role (_, role', _, _) = (role' = role) fun get_prop f (name, _, P, _) = P |> f |> close_form |> pair name |> postproc val path = exploded_absolute_path file_name val ((_, _, problem), thy) = TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy val (conjs, defs_and_nondefs) = problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture) ||> List.partition (has_role TPTP_Syntax.Role_Definition) in (map (get_prop I) conjs, apply2 (map (get_prop Logic.varify_global)) defs_and_nondefs, Named_Target.theory_init thy) end (** Nitpick **) fun aptrueprop f ((t0 as \<^Const_>\Trueprop\) $ t1) = t0 $ f t1 | aptrueprop f t = f t fun is_legitimate_tptp_def \<^Const_>\Trueprop for t\ = is_legitimate_tptp_def t | is_legitimate_tptp_def \<^Const_>\HOL.eq _ for t u\ = (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u) | is_legitimate_tptp_def _ = false fun nitpick_tptp_file thy timeout file_name = let val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name val thy = Proof_Context.theory_of lthy val (defs, pseudo_defs) = defs |> map (ATP_Util.abs_extensionalize_term lthy #> aptrueprop (hol_open_form I)) |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop) o ATP_Util.unextensionalize_def) val nondefs = pseudo_defs @ nondefs val state = Proof.init lthy val params = [("card", "1-100"), ("box", "false"), ("max_threads", "1"), ("batch_size", "5"), ("falsify", if null conjs then "false" else "true"), ("verbose", "true"), ("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("show_consts", "true"), ("format", "1"), ("max_potential", "0"), ("timeout", string_of_int timeout), ("tac_timeout", string_of_int ((timeout + 49) div 50))] |> Nitpick_Commands.default_params thy val i = 1 val n = 1 val step = 0 val subst = [] in Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst defs nondefs (case conjs of conj :: _ => conj | [] => \<^prop>\True\); () end (** Refute **) fun refute_tptp_file thy timeout file_name = let fun print_szs_of_outcome falsify s = "% SZS status " ^ (if s = "genuine" then if falsify then "CounterSatisfiable" else "Satisfiable" else "GaveUp") |> writeln val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name val params = [("maxtime", string_of_int timeout), ("maxvars", "100000")] in Refute.refute_term lthy params (defs @ nondefs) (case conjs of conj :: _ => conj | [] => \<^prop>\True\) |> print_szs_of_outcome (not (null conjs)) end (** Sledgehammer and Isabelle (combination of provers) **) fun can_tac ctxt tactic conj = can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt) fun SOLVE_TIMEOUT seconds name tac st = let val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s") val result = Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) () handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE in (case result of NONE => (writeln ("FAILURE: " ^ name); Seq.empty) | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st')) end fun nitpick_finite_oracle_tac lthy timeout i th = let fun is_safe (Type (\<^type_name>\fun\, Ts)) = forall is_safe Ts | is_safe \<^typ>\prop\ = true | is_safe \<^typ>\bool\ = true | is_safe _ = false val conj = Thm.term_of (Thm.cprem_of th i) in if exists_type (not o is_safe) conj then Seq.empty else let val thy = Proof_Context.theory_of lthy val state = Proof.init lthy val params = [("box", "false"), ("max_threads", "1"), ("verbose", "true"), ("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("max_potential", "0"), ("timeout", string_of_int timeout)] |> Nitpick_Commands.default_params thy val i = 1 val n = 1 val step = 0 val subst = [] val (outcome, _) = Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj in if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac lthy) th else Seq.empty end end fun atp_tac lthy completeness override_params timeout assms prover = let val thy = Proof_Context.theory_of lthy val assm_ths0 = map (Skip_Proof.make_thm thy) assms val ((assm_name, _), lthy) = lthy |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0) |> Local_Theory.note ((\<^binding>\thms\, []), assm_ths0) fun ref_of th = (Facts.named (Thm.derivation_name th), []) val ref_of_assms = (Facts.named assm_name, []) in Sledgehammer_Tactics.sledgehammer_as_oracle_tac lthy ([("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("provers", prover), ("timeout", string_of_int timeout)] @ (if completeness > 0 then [("type_enc", if completeness = 1 then "mono_native" else "poly_tags")] else []) @ override_params) {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} [] end fun sledgehammer_tac demo lthy timeout assms i = let val frac = if demo then 16 else 12 fun slice mult completeness prover = SOLVE_TIMEOUT (mult * timeout div frac) (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else "")) (atp_tac lthy completeness [] (mult * timeout div frac) assms prover i) in slice 2 0 ATP_Proof.spassN ORELSE slice 2 0 ATP_Proof.vampireN ORELSE slice 2 0 ATP_Proof.eN ORELSE slice 1 1 ATP_Proof.spassN ORELSE slice 1 2 ATP_Proof.eN ORELSE slice 1 1 ATP_Proof.vampireN ORELSE slice 1 2 ATP_Proof.vampireN ORELSE (if demo then slice 2 0 ATP_Proof.satallaxN ORELSE slice 2 0 ATP_Proof.leo2N else no_tac) end fun smt_solver_tac solver lthy = let val lthy = lthy |> Context.proof_map (SMT_Config.select_solver solver) in SMT_Solver.smt_tac lthy [] end fun auto_etc_tac lthy timeout assms i = SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac lthy (timeout div 20) i) ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass" (auto_tac lthy THEN ALLGOALS (atp_tac lthy 0 [] (timeout div 5) assms ATP_Proof.spassN)) ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" lthy i) ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" lthy i) ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i) ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac lthy i) fun make_conj (defs, nondefs) conjs = Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => \<^prop>\False\) fun print_szs_of_success conjs success = writeln ("% SZS status " ^ (if success then if null conjs then "Unsatisfiable" else "Theorem" else "GaveUp")) fun sledgehammer_tptp_file thy timeout file_name = let val (conjs, assms, lthy) = read_tptp_file thy snd file_name val conj = make_conj ([], []) conjs val assms = op @ assms in can_tac lthy (fn lthy => sledgehammer_tac true lthy timeout assms 1) conj |> print_szs_of_success conjs end fun generic_isabelle_tptp_file demo thy timeout file_name = let val (conjs, assms, lthy) = read_tptp_file thy snd file_name val conj = make_conj ([], []) conjs val full_conj = make_conj assms conjs val assms = op @ assms val (last_hope_atp, last_hope_completeness) = if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2) in (can_tac lthy (fn lthy => auto_etc_tac lthy (timeout div 2) assms 1) full_conj orelse can_tac lthy (fn lthy => sledgehammer_tac demo lthy (timeout div 2) assms 1) conj orelse can_tac lthy (fn lthy => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)") (atp_tac lthy last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj) |> print_szs_of_success conjs end val isabelle_tptp_file = generic_isabelle_tptp_file false val isabelle_hot_tptp_file = generic_isabelle_tptp_file true (** Translator between TPTP(-like) file formats **) fun translate_tptp_file thy format_str file_name = let val (conjs, (defs, nondefs), lthy) = read_tptp_file thy I file_name val conj = make_conj ([], []) (map snd conjs) val (format, type_enc, lam_trans) = (case format_str of "FOF" => (FOF, "mono_guards??", liftingN) | "TF0" => (TFF (Monomorphic, Without_FOOL), "mono_native", liftingN) | "TH0" => (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) | "DFG" => (DFG Monomorphic, "mono_native", liftingN) | _ => error ("Unknown format " ^ quote format_str ^ " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")")) val generate_info = false val uncurried_aliases = false val readable_names = true val presimp = true val facts = map (apfst (rpair (Global, Non_Rec_Def))) defs @ map (apfst (rpair (Global, General))) nondefs val (atp_problem, _, _, _) = generate_atp_problem lthy generate_info format Hypothesis (type_enc_of_string Strict type_enc) Translator lam_trans uncurried_aliases readable_names presimp [] conj facts - val ord = Sledgehammer_ATP_Systems.effective_term_order lthy spassN - val ord_info = K [] - val lines = lines_of_atp_problem format ord ord_info atp_problem + val lines = lines_of_atp_problem format (K []) atp_problem in List.app Output.physical_stdout lines end end; diff --git a/src/HOL/TPTP/atp_theory_export.ML b/src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML +++ b/src/HOL/TPTP/atp_theory_export.ML @@ -1,364 +1,360 @@ (* Title: HOL/TPTP/atp_theory_export.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2011 Export Isabelle theories as first-order TPTP inferences. *) signature ATP_THEORY_EXPORT = sig type atp_format = ATP_Problem.atp_format datatype inference_policy = No_Inferences | Unchecked_Inferences | Checked_Inferences val generate_atp_inference_file_for_theory : Proof.context -> theory -> atp_format -> inference_policy -> string -> string -> unit val generate_casc_lbt_isa_files_for_theory : Proof.context -> theory -> atp_format -> inference_policy -> string -> string -> unit end; structure ATP_Theory_Export : ATP_THEORY_EXPORT = struct open ATP_Problem open ATP_Proof open ATP_Problem_Generate open Sledgehammer_ATP_Systems val max_dependencies = 100 val max_facts = 512 val atp_timeout = seconds 0.5 datatype inference_policy = No_Inferences | Unchecked_Inferences | Checked_Inferences val prefix = Library.prefix val fact_name_of = prefix fact_prefix o ascii_of fun atp_of_format (THF (Polymorphic, _, _)) = leo3N | atp_of_format (THF (Monomorphic, _, _)) = satallaxN | atp_of_format (DFG Monomorphic) = spassN | atp_of_format (TFF (Polymorphic, _)) = alt_ergoN | atp_of_format (TFF (Monomorphic, _)) = vampireN | atp_of_format FOF = eN (* FIXME? *) | atp_of_format CNF_UEQ = waldmeisterN | atp_of_format CNF = eN (* FIXME? *) fun run_atp ctxt format problem = let val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob") val atp = atp_of_format format val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () - val ord = effective_term_order ctxt atp val _ = problem - |> lines_of_atp_problem format ord (K []) + |> lines_of_atp_problem format (K []) |> File.write_list prob_file val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = space_implode " " (File.bash_path (Path.explode path) :: - arguments ctxt false "" atp_timeout prob_file (ord, K [], K [])) + arguments ctxt false "" atp_timeout prob_file) val outcome = Timeout.apply atp_timeout Isabelle_System.bash_output command |> fst |> extract_tstplike_proof_and_outcome false proof_delims known_failures |> snd handle Timeout.TIMEOUT _ => SOME TimedOut val _ = tracing ("Ran ATP: " ^ (case outcome of NONE => "Success" | SOME failure => string_of_atp_failure failure)) in outcome end fun is_problem_line_reprovable ctxt format prelude axioms deps (Formula (ident', _, phi, _, _)) = is_none (run_atp ctxt format ((factsN, Formula (ident', Conjecture, phi, NONE, []) :: map_filter (Symtab.lookup axioms) deps) :: prelude)) | is_problem_line_reprovable _ _ _ _ _ _ = false fun inference_term _ [] = NONE | inference_term check_infs ss = ATerm (("inference", []), [ATerm (("checked_isabelle" |> not check_infs ? prefix "un", []), []), ATerm ((tptp_empty_list, []), []), ATerm ((tptp_empty_list, []), map (fn s => ATerm ((s, []), [])) ss)]) |> SOME fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers (line as Formula ((ident, alt), Axiom, phi, NONE, info)) = let val deps = case these (AList.lookup (op =) infers ident) of [] => [] | deps => if check_infs andalso not (is_problem_line_reprovable ctxt format prelude axioms deps line) then [] else deps in Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, info) end | add_inferences_to_problem_line _ _ _ _ _ _ line = line fun add_inferences_to_problem ctxt format check_infs prelude infers problem = let fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) = Symtab.default (ident, axiom) | add_if_axiom _ = I val add_axioms_of_problem = fold (fold add_if_axiom o snd) val axioms = Symtab.empty |> check_infs ? add_axioms_of_problem problem in map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs prelude axioms infers))) problem end fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident | ident_of_problem_line (Type_Decl (ident, _, _)) = ident | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident fun order_facts ord = sort (ord o apply2 ident_of_problem_line) fun order_problem_facts _ [] = [] | order_problem_facts ord ((heading, lines) :: problem) = if heading = factsN then (heading, order_facts ord lines) :: problem else (heading, lines) :: order_problem_facts ord problem (* A fairly random selection of types used for monomorphizing. *) val ground_types = [\<^typ>\nat\, HOLogic.intT, HOLogic.realT, \<^typ>\nat => bool\, \<^typ>\bool\, \<^typ>\unit\] fun ground_type_of_tvar _ [] tvar = raise TYPE ("ground_type_of_tvar", [TVar tvar], []) | ground_type_of_tvar thy (T :: Ts) tvar = if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T else ground_type_of_tvar thy Ts tvar fun monomorphize_term ctxt t = let val thy = Proof_Context.theory_of ctxt in t |> map_types (map_type_tvar (ground_type_of_tvar thy ground_types)) handle TYPE _ => \<^prop>\True\ end fun heading_sort_key heading = if String.isPrefix factsN heading then "_" ^ heading else heading fun problem_of_theory ctxt thy format infer_policy type_enc = let val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val type_enc = type_enc |> type_enc_of_string Non_Strict |> adjust_type_enc format val mono = not (is_type_enc_polymorphic type_enc) val facts = Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true Keyword.empty_keywords [] [] css_table |> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd) val problem = facts |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt)) |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true [] \<^prop>\False\ |> #1 |> sort_by (heading_sort_key o fst) val prelude = fst (split_last problem) val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts val infers = if infer_policy = No_Inferences then [] else facts |> map (fn (_, th) => (fact_name_of (Thm.get_name_hint th), th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs) |> these |> map fact_name_of)) val all_problem_names = problem |> maps (map ident_of_problem_line o snd) |> distinct (op =) val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names) val infers = infers |> filter (Symtab.defined all_problem_name_set o fst) |> map (apsnd (filter (Symtab.defined all_problem_name_set))) val maybe_add_edge = perhaps o try o String_Graph.add_edge_acyclic val ordered_names = String_Graph.empty |> fold (String_Graph.new_node o rpair ()) all_problem_names |> fold (fn (to, froms) => fold (fn from => maybe_add_edge (from, to)) froms) infers |> fold (fn (to, from) => maybe_add_edge (from, to)) (tl all_problem_names ~~ fst (split_last all_problem_names)) |> String_Graph.topological_order val order_tab = Symtab.empty |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names)) val name_ord = int_ord o apply2 (the o Symtab.lookup order_tab) in (facts, problem |> (case format of DFG _ => I | _ => add_inferences_to_problem ctxt format (infer_policy = Checked_Inferences) prelude infers) |> order_problem_facts name_ord) end -fun lines_of_problem ctxt format = - lines_of_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K []) - fun write_lines path ss = let val _ = File.write path "" val _ = app (File.append path) ss in () end fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc file_name = let val (_, problem) = problem_of_theory ctxt thy format infer_policy type_enc - val ss = lines_of_problem ctxt format problem + val ss = lines_of_atp_problem format (K []) problem in write_lines (Path.explode file_name) ss end fun ap dir = Path.append dir o Path.explode fun chop_maximal_groups eq xs = let val rev_xs = rev xs fun chop_group _ [] = [] | chop_group n (xs as x :: _) = let val n' = find_index (curry eq x) rev_xs val (ws', xs') = chop (n - n') xs in ws' :: chop_group n' xs' end in chop_group (length xs) xs end fun theory_name_of_fact (Formula ((_, alt), _, _, _, _)) = (case first_field Long_Name.separator alt of NONE => alt | SOME (thy, _) => thy) | theory_name_of_fact _ = "" val problem_suffix = ".p" val suggestion_suffix = ".sugg" val include_suffix = ".ax" val file_order_name = "FilesInProcessingOrder" val problem_order_name = "ProblemsInProcessingOrder" val problem_name = "problems" val suggestion_name = "suggestions" val include_name = "incl" val prelude_base_name = "prelude" val prelude_name = prelude_base_name ^ include_suffix val encode_meta = Sledgehammer_MaSh.encode_str fun include_base_name_of_fact x = encode_meta (theory_name_of_fact x) fun include_line base_name = "include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n" val hol_base_name = encode_meta "HOL" fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) = (case try (Global_Theory.get_thm thy) alt of SOME th => (* This is a crude hack to detect theorems stated and proved by the user (as opposed to those derived by various packages). In addition, we leave out everything in "HOL" as too basic to be interesting. *) Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name | NONE => false) (* Convention: theoryname__goalname *) fun problem_name_of base_name n alt = base_name ^ "__" ^ string_of_int n ^ "_" ^ perhaps (try (unprefix (base_name ^ "_"))) alt ^ problem_suffix fun suggestion_name_of base_name n alt = base_name ^ "__" ^ string_of_int n ^ "_" ^ perhaps (try (unprefix (base_name ^ "_"))) alt ^ suggestion_suffix fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc dir_name = let val dir = Isabelle_System.make_directory (Path.explode dir_name) val file_order_path = ap dir file_order_name val _ = File.write file_order_path "" val problem_order_path = ap dir problem_order_name val _ = File.write problem_order_path "" val problem_dir = Isabelle_System.make_directory (ap dir problem_name) val suggestion_dir = Isabelle_System.make_directory (ap dir suggestion_name) val include_dir = Isabelle_System.make_directory (ap problem_dir include_name) val (facts, (prelude, groups)) = problem_of_theory ctxt thy format infer_policy type_enc ||> split_last ||> apsnd (snd #> chop_maximal_groups (op = o apply2 theory_name_of_fact) #> map (`(include_base_name_of_fact o hd))) val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts) fun write_prelude () = - let val ss = lines_of_problem ctxt format prelude in + let val ss = lines_of_atp_problem format (K []) prelude in File.append file_order_path (prelude_base_name ^ "\n"); write_lines (ap include_dir prelude_name) ss end fun write_include_file (base_name, fact_lines) = let val name = base_name ^ include_suffix - val ss = lines_of_problem ctxt format [(factsN, fact_lines)] + val ss = lines_of_atp_problem format (K []) [(factsN, fact_lines)] in File.append file_order_path (base_name ^ "\n"); write_lines (ap include_dir name) ss end fun select_facts_for_fact facts fact = let val (hyp_ts, conj_t) = Logic.strip_horn (Thm.prop_of (snd fact)) val mepo = Sledgehammer_MePo.mepo_suggested_facts ctxt (Sledgehammer_Commands.default_params thy []) max_facts NONE hyp_ts conj_t facts in map (suffix "\n" o fact_name_of o Thm.get_name_hint o snd) mepo end fun write_problem_files _ _ _ _ [] = () | write_problem_files _ seen_facts includes [] groups = write_problem_files 1 seen_facts includes includes groups | write_problem_files n seen_facts includes _ ((base_name, []) :: groups) = write_problem_files n seen_facts (includes @ [include_line base_name]) [] groups | write_problem_files n seen_facts includes seen_ss ((base_name, fact_line :: fact_lines) :: groups) = let val (alt, pname, sname, conj) = (case fact_line of Formula ((ident, alt), _, phi, _, _) => (alt, problem_name_of base_name n (encode_meta alt), suggestion_name_of base_name n (encode_meta alt), Formula ((ident, alt), Conjecture, phi, NONE, []))) val fact = the (Symtab.lookup fact_tab alt) val fact_s = tptp_string_of_line format fact_line in (if should_generate_problem thy base_name fact_line then let val conj_s = tptp_string_of_line format conj in File.append problem_order_path (pname ^ "\n"); write_lines (ap problem_dir pname) (seen_ss @ [conj_s]); write_lines (ap suggestion_dir sname) (select_facts_for_fact facts fact) end else (); write_problem_files (n + 1) (fact :: seen_facts) includes (seen_ss @ [fact_s]) ((base_name, fact_lines) :: groups)) end val _ = write_prelude () val _ = app write_include_file groups val _ = write_problem_files 1 [] [include_line prelude_base_name] [] groups in () end end;