64 TimeLimit.timeLimit atp_timeout Isabelle_System.bash_output command |
64 TimeLimit.timeLimit atp_timeout Isabelle_System.bash_output command |
65 |> fst |
65 |> fst |
66 |> extract_tstplike_proof_and_outcome false proof_delims known_failures |
66 |> extract_tstplike_proof_and_outcome false proof_delims known_failures |
67 |> snd |
67 |> snd |
68 handle TimeLimit.TimeOut => SOME TimedOut |
68 handle TimeLimit.TimeOut => SOME TimedOut |
69 val _ = tracing ("Ran ATP: " ^ PolyML.makestring outcome) (*###*) |
69 val _ = |
|
70 tracing ("Ran ATP: " ^ |
|
71 case outcome of |
|
72 NONE => "Success" |
|
73 | SOME failure => string_for_failure failure) |
70 in outcome end |
74 in outcome end |
71 |
|
72 val tautology_prefixes = |
|
73 [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] |
|
74 |> map (fact_name_of o Context.theory_name) |
|
75 |
|
76 fun is_problem_line_tautology ctxt format |
|
77 (Formula ((ident, alt), role, phi, _, _)) = |
|
78 (role = Conjecture andalso |
|
79 phi = AAtom (ATerm ((tptp_false, []), []))) orelse |
|
80 (exists (fn prefix => String.isPrefix prefix ident) |
|
81 tautology_prefixes andalso |
|
82 is_none (run_atp ctxt format |
|
83 [(factsN, [Formula ((ident, alt), Conjecture, phi, NONE, [])])])) |
|
84 | is_problem_line_tautology _ _ _ = false |
|
85 |
75 |
86 fun is_problem_line_reprovable ctxt format prelude axioms deps |
76 fun is_problem_line_reprovable ctxt format prelude axioms deps |
87 (Formula (ident', _, phi, _, _)) = |
77 (Formula (ident', _, phi, _, _)) = |
88 is_none (run_atp ctxt format |
78 is_none (run_atp ctxt format |
89 ((factsN, Formula (ident', Conjecture, phi, NONE, []) :: |
79 ((factsN, Formula (ident', Conjecture, phi, NONE, []) :: |
179 |> map (fn ((_, loc), th) => |
169 |> map (fn ((_, loc), th) => |
180 ((Thm.get_name_hint th, loc), |
170 ((Thm.get_name_hint th, loc), |
181 th |> prop_of |> mono ? monomorphize_term ctxt)) |
171 th |> prop_of |> mono ? monomorphize_term ctxt)) |
182 |> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false |
172 |> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false |
183 false true [] @{prop False} |
173 false true [] @{prop False} |
184 |> #1 |
174 |> #1 |> sort_wrt (heading_sort_key o fst) |
185 val problem = |
|
186 problem |
|
187 |> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) |
|
188 |> sort_wrt (heading_sort_key o fst) |
|
189 val prelude = fst (split_last problem) |
175 val prelude = fst (split_last problem) |
190 val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts |
176 val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts |
191 val infers = |
177 val infers = |
192 if infer_policy = No_Inferences then |
178 if infer_policy = No_Inferences then |
193 [] |
179 [] |