118 val command = |
118 val command = |
119 File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ |
119 File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ |
120 " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^ |
120 " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^ |
121 File.shell_path prob_file |
121 File.shell_path prob_file |
122 in |
122 in |
123 TimeLimit.timeLimit (seconds 0.15) bash_output command |
123 TimeLimit.timeLimit (seconds 0.3) bash_output command |
124 |> fst |
124 |> fst |
125 |> extract_tstplike_proof_and_outcome false true proof_delims |
125 |> extract_tstplike_proof_and_outcome false true proof_delims |
126 known_failures |
126 known_failures |
127 |> snd |
127 |> snd |
128 end |
128 end |
129 handle TimeLimit.TimeOut => SOME TimedOut |
129 handle TimeLimit.TimeOut => SOME TimedOut |
130 |
130 |
131 val likely_tautology_prefixes = |
131 val likely_tautology_prefixes = |
132 [@{theory HOL}, @{theory Meson}, @{theory Metis}] |
132 [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] |
133 |> map (fact_name_of o Context.theory_name) |
133 |> map (fact_name_of o Context.theory_name) |
134 |
134 |
135 fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) = |
135 fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) = |
136 exists (fn prefix => String.isPrefix prefix ident) |
136 exists (fn prefix => String.isPrefix prefix ident) |
137 likely_tautology_prefixes andalso |
137 likely_tautology_prefixes andalso |