# HG changeset patch # User blanchet # Date 1310588179 -7200 # Node ID eb9be23db2b72116d28a3aa1e6b21ea1376805bc # Parent 06094d789512cdb1daa0adf7d49c0d1494fcffdb cleanly separate TPTP related files from other examples diff -r 06094d789512 -r eb9be23db2b7 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jul 13 21:59:54 2011 +0200 +++ b/src/HOL/IsaMakefile Wed Jul 13 22:16:19 2011 +0200 @@ -74,6 +74,7 @@ TLA-Buffer \ TLA-Inc \ TLA-Memory \ + HOL-TPTP \ HOL-UNITY \ HOL-Unix \ HOL-Word-Examples \ @@ -1047,9 +1048,9 @@ $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \ Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \ - ex/ATP_Export.thy ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \ + ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \ ex/BT.thy ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \ - ex/CASC_Setup.thy ex/CTL.thy ex/Case_Product.thy \ + ex/CTL.thy ex/Case_Product.thy \ ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \ ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \ ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \ @@ -1164,6 +1165,19 @@ @cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory +## HOL-TPTP + +HOL-TPTP: HOL $(LOG)/HOL-TPTP.gz + +$(LOG)/HOL-TPTP.gz: \ + $(OUT)/HOL \ + TPTP/ROOT.ML \ + TPTP/ATP_Export.thy \ + TPTP/CASC_Setup.thy \ + TPTP/atp_export.ML + @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP + + ## HOL-Multivariate_Analysis HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis diff -r 06094d789512 -r eb9be23db2b7 src/HOL/TPTP/ATP_Export.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/ATP_Export.thy Wed Jul 13 22:16:19 2011 +0200 @@ -0,0 +1,44 @@ +theory ATP_Export +imports Complex_Main +uses "atp_export.ML" +begin + +ML {* +val do_it = false; (* switch to "true" to generate the files *) +val thy = @{theory Complex_Main}; +val ctxt = @{context} +*} + +ML {* +if do_it then + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds" + "/tmp/infs_poly_preds.tptp" +else + () +*} + +ML {* +if do_it then + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags" + "/tmp/infs_poly_tags.tptp" +else + () +*} + +ML {* +if do_it then + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy" + "/tmp/infs_poly_tags_heavy.tptp" +else + () +*} + +ML {* +if do_it then + ATP_Export.generate_tptp_graph_file_for_theory ctxt thy + "/tmp/graph.out" +else + () +*} + +end diff -r 06094d789512 -r eb9be23db2b7 src/HOL/TPTP/CASC_Setup.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/CASC_Setup.thy Wed Jul 13 22:16:19 2011 +0200 @@ -0,0 +1,71 @@ +(* Title: HOL/ex/CASC_Setup.thy + Author: Jasmin Blanchette + Copyright 2011 + +Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and +TNT divisions. This theory file should be loaded by the Isabelle theory files +generated by Geoff Sutcliffe's TPTP2X tool from the original THF0 files. +*) + +theory CASC_Setup +imports Main +uses "sledgehammer_tactics.ML" +begin + +declare mem_def [simp add] + +declare [[smt_oracle]] + +refute_params [maxtime = 10000, no_assms, expect = genuine] +nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms, + batch_size = 1, expect = genuine] + +ML {* Proofterm.proofs := 0 *} + +ML {* +fun SOLVE_TIMEOUT seconds name tac st = + let + val result = + TimeLimit.timeLimit (Time.fromSeconds seconds) + (fn () => SINGLE (SOLVE tac) st) () + handle TimeLimit.TimeOut => NONE + | ERROR _ => NONE + in + (case result of + NONE => (warning ("FAILURE: " ^ name); Seq.empty) + | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st')) + end +*} + +ML {* +fun isabellep_tac ctxt max_secs = + SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) + ORELSE + SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" + (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) + ORELSE + SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt + THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "metis" + (ALLGOALS (Metis_Tactics.metis_tac [] ctxt [])) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt)) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt)) + ORELSE + SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt)) +*} + +method_setup isabellep = {* + Scan.lift (Scan.optional Parse.nat 1) >> + (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m)) +*} "combination of Isabelle provers and oracles for CASC" + +end diff -r 06094d789512 -r eb9be23db2b7 src/HOL/TPTP/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/ROOT.ML Wed Jul 13 22:16:19 2011 +0200 @@ -0,0 +1,14 @@ +(* Title: HOL/TPTP/ROOT.ML + Author: Jasmin Blanchette, TU Muenchen + Author: Nik Sultana, University of Cambridge + Copyright 2011 + +TPTP-related extensions. +*) + +use_thys [ + "ATP_Export" +]; + +Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs) + use_thy "CASC_Setup"; diff -r 06094d789512 -r eb9be23db2b7 src/HOL/TPTP/atp_export.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/atp_export.ML Wed Jul 13 22:16:19 2011 +0200 @@ -0,0 +1,196 @@ +(* Title: HOL/ex/atp_export.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2011 + +Export Isabelle theories as first-order TPTP inferences, exploiting +Sledgehammer's translation. +*) + +signature ATP_EXPORT = +sig + val theorems_mentioned_in_proof_term : + string list option -> thm -> string list + val generate_tptp_graph_file_for_theory : + Proof.context -> theory -> string -> unit + val generate_tptp_inference_file_for_theory : + Proof.context -> theory -> string -> string -> unit +end; + +structure ATP_Export : ATP_EXPORT = +struct + +open ATP_Problem +open ATP_Translate +open ATP_Proof +open ATP_Systems + +val fact_name_of = prefix fact_prefix o ascii_of + +fun facts_of thy = + Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty + true [] [] + |> filter (curry (op =) @{typ bool} o fastype_of + o Object_Logic.atomize_term thy o prop_of o snd) + +(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few + fixes that seem to be missing over there; or maybe the two code portions are + not doing the same? *) +fun fold_body_thms thm_name all_names f = + let + fun app n (PBody {thms, ...}) = + thms |> fold (fn (_, (name, prop, body)) => fn x => + let + val body' = Future.join body + val n' = + n + (if name = "" orelse + (is_some all_names andalso + not (member (op =) (the all_names) name)) orelse + (* uncommon case where the proved theorem occurs twice + (e.g., "Transitive_Closure.trancl_into_trancl") *) + n = 1 andalso name = thm_name then + 0 + else + 1) + val x' = x |> n' <= 1 ? app n' body' + in (x' |> n = 1 ? f (name, prop, body')) end) + in fold (app 0) end + +fun theorems_mentioned_in_proof_term all_names thm = + let + fun collect (s, _, _) = if s <> "" then insert (op =) s else I + val names = + [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect + [Thm.proof_body_of thm] + |> map fact_name_of + in names end + +fun interesting_const_names ctxt = + let val thy = Proof_Context.theory_of ctxt in + Sledgehammer_Filter.const_names_in_fact thy + (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN) + end + +fun generate_tptp_graph_file_for_theory ctxt thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val axioms = Theory.all_axioms_of thy |> map fst + fun do_thm thm = + let + val name = Thm.get_name_hint thm + val s = + "[" ^ Thm.legacy_get_kind thm ^ "] " ^ + (if member (op =) axioms name then "A" else "T") ^ " " ^ + prefix fact_prefix (ascii_of name) ^ ": " ^ + commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^ + commas (map (prefix const_prefix o ascii_of) + (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" + in File.append path s end + val thms = facts_of thy |> map snd + val _ = map do_thm thms + in () end + +fun inference_term [] = NONE + | inference_term ss = + ATerm ("inference", + [ATerm ("isabelle", []), + ATerm (tptp_empty_list, []), + ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)]) + |> SOME +fun inference infers ident = + these (AList.lookup (op =) infers ident) |> inference_term +fun add_inferences_to_problem_line infers + (Formula (ident, Axiom, phi, NONE, NONE)) = + Formula (ident, Lemma, phi, inference infers ident, NONE) + | add_inferences_to_problem_line _ line = line +val add_inferences_to_problem = + map o apsnd o map o add_inferences_to_problem_line + +fun ident_of_problem_line (Decl (ident, _, _)) = ident + | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident + +fun run_some_atp ctxt problem = + let + val thy = Proof_Context.theory_of ctxt + val prob_file = Path.explode "/tmp/prob.tptp" (* FIXME File.tmp_path (?) *) + val {exec, arguments, proof_delims, known_failures, ...} = + get_atp thy spassN + val _ = problem |> tptp_lines_for_atp_problem FOF + |> File.write_list prob_file + val command = + File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ + " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^ + File.shell_path prob_file + in + TimeLimit.timeLimit (seconds 0.3) bash_output command + |> fst + |> extract_tstplike_proof_and_outcome false true proof_delims + known_failures + |> snd + end + handle TimeLimit.TimeOut => SOME TimedOut + +val likely_tautology_prefixes = + [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] + |> map (fact_name_of o Context.theory_name) + +fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) = + exists (fn prefix => String.isPrefix prefix ident) + likely_tautology_prefixes andalso + is_none (run_some_atp ctxt + [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])]) + | is_problem_line_tautology _ _ = false + +structure String_Graph = Graph(type key = string val ord = string_ord); + +fun order_facts ord = sort (ord o pairself 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 + +fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name = + let + val format = FOF + val type_enc = type_enc |> type_enc_from_string + val path = file_name |> Path.explode + val _ = File.write path "" + val facts = facts_of thy + val (atp_problem, _, _, _, _, _, _) = + facts + |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) + |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false + true [] @{prop False} + val atp_problem = + atp_problem + |> map (apsnd (filter_out (is_problem_line_tautology ctxt))) + val all_names = facts |> map (Thm.get_name_hint o snd) + val infers = + facts |> map (fn (_, th) => + (fact_name_of (Thm.get_name_hint th), + theorems_mentioned_in_proof_term (SOME all_names) th)) + val all_atp_problem_names = + atp_problem |> maps (map ident_of_problem_line o snd) + val infers = + infers |> filter (member (op =) all_atp_problem_names o fst) + |> map (apsnd (filter (member (op =) all_atp_problem_names))) + val ordered_names = + String_Graph.empty + |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names + |> fold (fn (to, froms) => + fold (fn from => String_Graph.add_edge (from, to)) froms) + infers + |> 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 pairself (the o Symtab.lookup order_tab) + val atp_problem = + atp_problem |> add_inferences_to_problem infers + |> order_problem_facts name_ord + val ss = tptp_lines_for_atp_problem FOF atp_problem + val _ = app (File.append path) ss + in () end + +end; diff -r 06094d789512 -r eb9be23db2b7 src/HOL/ex/ATP_Export.thy --- a/src/HOL/ex/ATP_Export.thy Wed Jul 13 21:59:54 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,44 +0,0 @@ -theory ATP_Export -imports Complex_Main -uses "atp_export.ML" -begin - -ML {* -val do_it = false; (* switch to "true" to generate the files *) -val thy = @{theory Complex_Main}; -val ctxt = @{context} -*} - -ML {* -if do_it then - ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds" - "/tmp/infs_poly_preds.tptp" -else - () -*} - -ML {* -if do_it then - ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags" - "/tmp/infs_poly_tags.tptp" -else - () -*} - -ML {* -if do_it then - ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy" - "/tmp/infs_poly_tags_heavy.tptp" -else - () -*} - -ML {* -if do_it then - ATP_Export.generate_tptp_graph_file_for_theory ctxt thy - "/tmp/graph.out" -else - () -*} - -end diff -r 06094d789512 -r eb9be23db2b7 src/HOL/ex/CASC_Setup.thy --- a/src/HOL/ex/CASC_Setup.thy Wed Jul 13 21:59:54 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,71 +0,0 @@ -(* Title: HOL/ex/CASC_Setup.thy - Author: Jasmin Blanchette - Copyright 2011 - -Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and -TNT divisions. This theory file should be loaded by the Isabelle theory files -generated by Geoff Sutcliffe's TPTP2X tool from the original THF0 files. -*) - -theory CASC_Setup -imports Main -uses "sledgehammer_tactics.ML" -begin - -declare mem_def [simp add] - -declare [[smt_oracle]] - -refute_params [maxtime = 10000, no_assms, expect = genuine] -nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms, - batch_size = 1, expect = genuine] - -ML {* Proofterm.proofs := 0 *} - -ML {* -fun SOLVE_TIMEOUT seconds name tac st = - let - val result = - TimeLimit.timeLimit (Time.fromSeconds seconds) - (fn () => SINGLE (SOLVE tac) st) () - handle TimeLimit.TimeOut => NONE - | ERROR _ => NONE - in - (case result of - NONE => (warning ("FAILURE: " ^ name); Seq.empty) - | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st')) - end -*} - -ML {* -fun isabellep_tac ctxt max_secs = - SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) - ORELSE - SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" - (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) - ORELSE - SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt - THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "metis" - (ALLGOALS (Metis_Tactics.metis_tac [] ctxt [])) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt)) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt)) - ORELSE - SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt)) -*} - -method_setup isabellep = {* - Scan.lift (Scan.optional Parse.nat 1) >> - (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m)) -*} "combination of Isabelle provers and oracles for CASC" - -end diff -r 06094d789512 -r eb9be23db2b7 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Wed Jul 13 21:59:54 2011 +0200 +++ b/src/HOL/ex/ROOT.ML Wed Jul 13 22:16:19 2011 +0200 @@ -11,8 +11,7 @@ "Normalization_by_Evaluation", "Hebrew", "Chinese", - "Serbian", - "ATP_Export" + "Serbian" ]; use_thys [ @@ -78,9 +77,6 @@ "Set_Algebras" ]; -Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs) - use_thy "CASC_Setup"; - if getenv "ISABELLE_GHC" = "" then () else use_thy "Quickcheck_Narrowing_Examples"; diff -r 06094d789512 -r eb9be23db2b7 src/HOL/ex/atp_export.ML --- a/src/HOL/ex/atp_export.ML Wed Jul 13 21:59:54 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,196 +0,0 @@ -(* Title: HOL/ex/atp_export.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2011 - -Export Isabelle theories as first-order TPTP inferences, exploiting -Sledgehammer's translation. -*) - -signature ATP_EXPORT = -sig - val theorems_mentioned_in_proof_term : - string list option -> thm -> string list - val generate_tptp_graph_file_for_theory : - Proof.context -> theory -> string -> unit - val generate_tptp_inference_file_for_theory : - Proof.context -> theory -> string -> string -> unit -end; - -structure ATP_Export : ATP_EXPORT = -struct - -open ATP_Problem -open ATP_Translate -open ATP_Proof -open ATP_Systems - -val fact_name_of = prefix fact_prefix o ascii_of - -fun facts_of thy = - Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty - true [] [] - |> filter (curry (op =) @{typ bool} o fastype_of - o Object_Logic.atomize_term thy o prop_of o snd) - -(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few - fixes that seem to be missing over there; or maybe the two code portions are - not doing the same? *) -fun fold_body_thms thm_name all_names f = - let - fun app n (PBody {thms, ...}) = - thms |> fold (fn (_, (name, prop, body)) => fn x => - let - val body' = Future.join body - val n' = - n + (if name = "" orelse - (is_some all_names andalso - not (member (op =) (the all_names) name)) orelse - (* uncommon case where the proved theorem occurs twice - (e.g., "Transitive_Closure.trancl_into_trancl") *) - n = 1 andalso name = thm_name then - 0 - else - 1) - val x' = x |> n' <= 1 ? app n' body' - in (x' |> n = 1 ? f (name, prop, body')) end) - in fold (app 0) end - -fun theorems_mentioned_in_proof_term all_names thm = - let - fun collect (s, _, _) = if s <> "" then insert (op =) s else I - val names = - [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect - [Thm.proof_body_of thm] - |> map fact_name_of - in names end - -fun interesting_const_names ctxt = - let val thy = Proof_Context.theory_of ctxt in - Sledgehammer_Filter.const_names_in_fact thy - (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN) - end - -fun generate_tptp_graph_file_for_theory ctxt thy file_name = - let - val path = file_name |> Path.explode - val _ = File.write path "" - val axioms = Theory.all_axioms_of thy |> map fst - fun do_thm thm = - let - val name = Thm.get_name_hint thm - val s = - "[" ^ Thm.legacy_get_kind thm ^ "] " ^ - (if member (op =) axioms name then "A" else "T") ^ " " ^ - prefix fact_prefix (ascii_of name) ^ ": " ^ - commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^ - commas (map (prefix const_prefix o ascii_of) - (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" - in File.append path s end - val thms = facts_of thy |> map snd - val _ = map do_thm thms - in () end - -fun inference_term [] = NONE - | inference_term ss = - ATerm ("inference", - [ATerm ("isabelle", []), - ATerm (tptp_empty_list, []), - ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)]) - |> SOME -fun inference infers ident = - these (AList.lookup (op =) infers ident) |> inference_term -fun add_inferences_to_problem_line infers - (Formula (ident, Axiom, phi, NONE, NONE)) = - Formula (ident, Lemma, phi, inference infers ident, NONE) - | add_inferences_to_problem_line _ line = line -val add_inferences_to_problem = - map o apsnd o map o add_inferences_to_problem_line - -fun ident_of_problem_line (Decl (ident, _, _)) = ident - | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident - -fun run_some_atp ctxt problem = - let - val thy = Proof_Context.theory_of ctxt - val prob_file = Path.explode "/tmp/prob.tptp" (* FIXME File.tmp_path (?) *) - val {exec, arguments, proof_delims, known_failures, ...} = - get_atp thy spassN - val _ = problem |> tptp_lines_for_atp_problem FOF - |> File.write_list prob_file - val command = - File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ - " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^ - File.shell_path prob_file - in - TimeLimit.timeLimit (seconds 0.3) bash_output command - |> fst - |> extract_tstplike_proof_and_outcome false true proof_delims - known_failures - |> snd - end - handle TimeLimit.TimeOut => SOME TimedOut - -val likely_tautology_prefixes = - [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] - |> map (fact_name_of o Context.theory_name) - -fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) = - exists (fn prefix => String.isPrefix prefix ident) - likely_tautology_prefixes andalso - is_none (run_some_atp ctxt - [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])]) - | is_problem_line_tautology _ _ = false - -structure String_Graph = Graph(type key = string val ord = string_ord); - -fun order_facts ord = sort (ord o pairself 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 - -fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name = - let - val format = FOF - val type_enc = type_enc |> type_enc_from_string - val path = file_name |> Path.explode - val _ = File.write path "" - val facts = facts_of thy - val (atp_problem, _, _, _, _, _, _) = - facts - |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) - |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false - true [] @{prop False} - val atp_problem = - atp_problem - |> map (apsnd (filter_out (is_problem_line_tautology ctxt))) - val all_names = facts |> map (Thm.get_name_hint o snd) - val infers = - facts |> map (fn (_, th) => - (fact_name_of (Thm.get_name_hint th), - theorems_mentioned_in_proof_term (SOME all_names) th)) - val all_atp_problem_names = - atp_problem |> maps (map ident_of_problem_line o snd) - val infers = - infers |> filter (member (op =) all_atp_problem_names o fst) - |> map (apsnd (filter (member (op =) all_atp_problem_names))) - val ordered_names = - String_Graph.empty - |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names - |> fold (fn (to, froms) => - fold (fn from => String_Graph.add_edge (from, to)) froms) - infers - |> 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 pairself (the o Symtab.lookup order_tab) - val atp_problem = - atp_problem |> add_inferences_to_problem infers - |> order_problem_facts name_ord - val ss = tptp_lines_for_atp_problem FOF atp_problem - val _ = app (File.append path) ss - in () end - -end;