equal
deleted
inserted
replaced
49 fun run_atp ctxt format problem = |
49 fun run_atp ctxt format problem = |
50 let |
50 let |
51 val thy = Proof_Context.theory_of ctxt |
51 val thy = Proof_Context.theory_of ctxt |
52 val prob_file = File.tmp_path (Path.explode "prob") |
52 val prob_file = File.tmp_path (Path.explode "prob") |
53 val atp = atp_of_format format |
53 val atp = atp_of_format format |
54 val {exec, arguments, proof_delims, known_failures, ...} = |
54 val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () |
55 get_atp thy atp () |
|
56 val ord = effective_term_order ctxt atp |
55 val ord = effective_term_order ctxt atp |
57 val _ = problem |> lines_of_atp_problem format ord (K []) |
56 val _ = problem |> lines_of_atp_problem format ord (K []) |
58 |> File.write_list prob_file |
57 |> File.write_list prob_file |
59 val exec = exec () |
58 val exec = exec false |
60 val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) |
59 val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) |
61 val command = |
60 val command = |
62 File.shell_path (Path.explode path) ^ " " ^ |
61 File.shell_path (Path.explode path) ^ " " ^ |
63 arguments ctxt false "" atp_timeout (File.shell_path prob_file) |
62 arguments ctxt false "" atp_timeout (File.shell_path prob_file) |
64 (ord, K [], K []) |
63 (ord, K [], K []) |