equal
deleted
inserted
replaced
110 | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident |
110 | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident |
111 |
111 |
112 fun run_some_atp ctxt problem = |
112 fun run_some_atp ctxt problem = |
113 let |
113 let |
114 val thy = Proof_Context.theory_of ctxt |
114 val thy = Proof_Context.theory_of ctxt |
115 val prob_file = Path.explode "/tmp/prob.tptp" (* FIXME File.tmp_path (?) *) |
115 val prob_file = File.tmp_path (Path.explode "prob.tptp") |
116 val {exec, arguments, proof_delims, known_failures, ...} = |
116 val {exec, arguments, proof_delims, known_failures, ...} = |
117 get_atp thy spassN |
117 get_atp thy spassN |
118 val _ = problem |> tptp_lines_for_atp_problem FOF |
118 val _ = problem |> tptp_lines_for_atp_problem FOF |
119 |> File.write_list prob_file |
119 |> File.write_list prob_file |
120 val command = |
120 val command = |