external_prover: "exec" the command line, in order to preserve the exact process context of the "system" invocation (this recovers interruptibility of E-1.0, which assumes to be the process group leader);
1 (* Title: HOL/Tools/atp_wrapper.ML
3 Author: Fabian Immler, TU Muenchen
5 Wrapper functions for external ATPs.
8 signature ATP_WRAPPER =
10 val destdir: string ref
11 val problem_name: string ref
13 (thm * (string * int)) list ->
14 (Path.T -> thm -> int -> (thm * (string * int)) list -> theory -> string vector) ->
15 Path.T * string -> (string -> string option) ->
16 (string * string vector * Proof.context * thm * int -> string) ->
18 val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
19 val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
20 val tptp_prover: Path.T * string -> AtpManager.prover
21 val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
22 val full_prover: Path.T * string -> AtpManager.prover
23 val vampire_opts: int -> bool -> AtpManager.prover
24 val vampire: AtpManager.prover
25 val vampire_opts_full: int -> bool -> AtpManager.prover
26 val vampire_full: AtpManager.prover
27 val eprover_opts: int -> bool -> AtpManager.prover
28 val eprover: AtpManager.prover
29 val eprover_opts_full: int -> bool -> AtpManager.prover
30 val eprover_full: AtpManager.prover
31 val spass_opts: int -> bool -> AtpManager.prover
32 val spass: AtpManager.prover
33 val remote_prover_opts: int -> bool -> string -> AtpManager.prover
34 val remote_prover: string -> AtpManager.prover
37 structure AtpWrapper: ATP_WRAPPER =
40 (** generic ATP wrapper **)
42 (* global hooks for writing problemfiles *)
44 val destdir = ref ""; (*Empty means write files to /tmp*)
45 val problem_name = ref "prob";
50 fun external_prover axiom_clauses write_problem_file (cmd, args) find_failure produce_answer timeout subgoalno goal =
52 (* path to unique problem file *)
53 val destdir' = ! destdir
54 val problem_name' = ! problem_name
55 fun prob_pathname nr =
56 let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
57 in if destdir' = "" then File.tmp_path probfile
58 else if File.exists (Path.explode (destdir'))
59 then Path.append (Path.explode (destdir')) probfile
60 else error ("No such directory: " ^ destdir')
63 (* write out problem file and call prover *)
64 val (ctxt, (chain_ths, th)) = goal
65 val thy = ProofContext.theory_of ctxt
66 val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
67 val probfile = prob_pathname subgoalno
68 val fname = File.platform_path probfile
69 val thm_names = write_problem_file probfile th subgoalno axiom_clauses thy
71 if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
72 else error ("Bad executable: " ^ Path.implode cmd)
73 val (proof, rc) = system_out (cmdline ^ " " ^ fname)
75 (* remove *temporary* files *)
76 val _ = if destdir' = "" then OS.FileSys.remove fname else ()
78 (* check for success and print out some information on failure *)
79 val failure = find_failure proof
80 val success = rc = 0 andalso is_none failure
82 if is_some failure then "External prover failed."
83 else if rc <> 0 then "External prover failed: " ^ proof
84 else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, th, subgoalno)
88 then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
92 then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
94 in (success, message) end;
98 (** common provers **)
100 (* generic TPTP-based provers *)
102 fun tptp_prover_opts_full max_new theory_const full command timeout n goal =
104 (ResAtp.get_relevant max_new theory_const goal n)
105 (ResAtp.write_problem_file false)
107 ResReconstruct.find_failure
108 (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
111 (*arbitrary ATP with TPTP input/output and problemfile as last argument*)
112 fun tptp_prover_opts max_new theory_const =
113 tptp_prover_opts_full max_new theory_const false;
115 val tptp_prover = tptp_prover_opts 60 true;
117 (*for structured proofs: prover must support TSTP*)
118 fun full_prover_opts max_new theory_const =
119 tptp_prover_opts_full max_new theory_const true;
121 val full_prover = full_prover_opts 60 true;
126 (*NB: Vampire does not work without explicit timelimit*)
128 fun vampire_opts max_new theory_const timeout = tptp_prover_opts
130 (Path.explode "$VAMPIRE_HOME/vampire",
131 ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
134 val vampire = vampire_opts 60 false;
136 fun vampire_opts_full max_new theory_const timeout = full_prover_opts
138 (Path.explode "$VAMPIRE_HOME/vampire",
139 ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
142 val vampire_full = vampire_opts 60 false;
147 fun eprover_opts max_new theory_const timeout = tptp_prover_opts
149 (Path.explode "$E_HOME/eproof",
150 "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
153 val eprover = eprover_opts 100 false;
155 fun eprover_opts_full max_new theory_const timeout = full_prover_opts
157 (Path.explode "$E_HOME/eproof",
158 "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
161 val eprover_full = eprover_opts_full 100 false;
166 fun spass_opts max_new theory_const timeout n goal = external_prover
167 (ResAtp.get_relevant max_new theory_const goal n)
168 (ResAtp.write_problem_file true)
169 (Path.explode "$SPASS_HOME/SPASS",
170 "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
171 ResReconstruct.find_failure
172 ResReconstruct.lemma_list_dfg
175 val spass = spass_opts 40 true;
178 (* remote prover invocation via SystemOnTPTP *)
180 fun remote_prover_opts max_new theory_const args timeout =
181 tptp_prover_opts max_new theory_const
182 (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int timeout)
185 val remote_prover = remote_prover_opts 60 false;