1 (* Title: HOL/Tools/atp_wrapper.ML |
|
2 Author: Fabian Immler, TU Muenchen |
|
3 |
|
4 Wrapper functions for external ATPs. |
|
5 *) |
|
6 |
|
7 signature ATP_WRAPPER = |
|
8 sig |
|
9 val destdir: string ref |
|
10 val problem_name: string ref |
|
11 val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover |
|
12 val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover |
|
13 val tptp_prover: Path.T * string -> AtpManager.prover |
|
14 val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover |
|
15 val full_prover: Path.T * string -> AtpManager.prover |
|
16 val vampire_opts: int -> bool -> AtpManager.prover |
|
17 val vampire: AtpManager.prover |
|
18 val vampire_opts_full: int -> bool -> AtpManager.prover |
|
19 val vampire_full: AtpManager.prover |
|
20 val eprover_opts: int -> bool -> AtpManager.prover |
|
21 val eprover: AtpManager.prover |
|
22 val eprover_opts_full: int -> bool -> AtpManager.prover |
|
23 val eprover_full: AtpManager.prover |
|
24 val spass_opts: int -> bool -> AtpManager.prover |
|
25 val spass: AtpManager.prover |
|
26 val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover |
|
27 val remote_prover: string -> string -> AtpManager.prover |
|
28 val refresh_systems: unit -> unit |
|
29 end; |
|
30 |
|
31 structure AtpWrapper: ATP_WRAPPER = |
|
32 struct |
|
33 |
|
34 (** generic ATP wrapper **) |
|
35 |
|
36 (* global hooks for writing problemfiles *) |
|
37 |
|
38 val destdir = ref ""; (*Empty means write files to /tmp*) |
|
39 val problem_name = ref "prob"; |
|
40 |
|
41 |
|
42 (* basic template *) |
|
43 |
|
44 fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer |
|
45 timeout axiom_clauses filtered_clauses name subgoalno goal = |
|
46 let |
|
47 (* path to unique problem file *) |
|
48 val destdir' = ! destdir |
|
49 val problem_name' = ! problem_name |
|
50 fun prob_pathname nr = |
|
51 let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr) |
|
52 in if destdir' = "" then File.tmp_path probfile |
|
53 else if File.exists (Path.explode (destdir')) |
|
54 then Path.append (Path.explode (destdir')) probfile |
|
55 else error ("No such directory: " ^ destdir') |
|
56 end |
|
57 |
|
58 (* get clauses and prepare them for writing *) |
|
59 val (ctxt, (chain_ths, th)) = goal |
|
60 val thy = ProofContext.theory_of ctxt |
|
61 val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths |
|
62 val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno) |
|
63 val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls |
|
64 val the_filtered_clauses = |
|
65 case filtered_clauses of |
|
66 NONE => relevance_filter goal goal_cls |
|
67 | SOME fcls => fcls |
|
68 val the_axiom_clauses = |
|
69 case axiom_clauses of |
|
70 NONE => the_filtered_clauses |
|
71 | SOME axcls => axcls |
|
72 val (thm_names, clauses) = |
|
73 preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy |
|
74 |
|
75 (* write out problem file and call prover *) |
|
76 val probfile = prob_pathname subgoalno |
|
77 val conj_pos = writer probfile clauses |
|
78 val (proof, rc) = system_out ( |
|
79 if File.exists cmd then |
|
80 space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile] |
|
81 else error ("Bad executable: " ^ Path.implode cmd)) |
|
82 |
|
83 (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *) |
|
84 val _ = |
|
85 if destdir' = "" then File.rm probfile |
|
86 else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof |
|
87 |
|
88 (* check for success and print out some information on failure *) |
|
89 val failure = find_failure proof |
|
90 val success = rc = 0 andalso is_none failure |
|
91 val message = |
|
92 if is_some failure then "External prover failed." |
|
93 else if rc <> 0 then "External prover failed: " ^ proof |
|
94 else "Try this command: " ^ |
|
95 produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno) |
|
96 val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof) |
|
97 in (success, message, proof, thm_names, the_filtered_clauses) end; |
|
98 |
|
99 |
|
100 |
|
101 (** common provers **) |
|
102 |
|
103 (* generic TPTP-based provers *) |
|
104 |
|
105 fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal = |
|
106 external_prover |
|
107 (ResAtp.get_relevant max_new theory_const) |
|
108 (ResAtp.prepare_clauses false) |
|
109 (ResHolClause.tptp_write_file (AtpManager.get_full_types())) |
|
110 command |
|
111 ResReconstruct.find_failure |
|
112 (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false) |
|
113 timeout ax_clauses fcls name n goal; |
|
114 |
|
115 (*arbitrary ATP with TPTP input/output and problemfile as last argument*) |
|
116 fun tptp_prover_opts max_new theory_const = |
|
117 tptp_prover_opts_full max_new theory_const false; |
|
118 |
|
119 fun tptp_prover x = tptp_prover_opts 60 true x; |
|
120 |
|
121 (*for structured proofs: prover must support TSTP*) |
|
122 fun full_prover_opts max_new theory_const = |
|
123 tptp_prover_opts_full max_new theory_const true; |
|
124 |
|
125 fun full_prover x = full_prover_opts 60 true x; |
|
126 |
|
127 |
|
128 (* Vampire *) |
|
129 |
|
130 (*NB: Vampire does not work without explicit timelimit*) |
|
131 |
|
132 fun vampire_opts max_new theory_const timeout = tptp_prover_opts |
|
133 max_new theory_const |
|
134 (Path.explode "$VAMPIRE_HOME/vampire", |
|
135 ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout)) |
|
136 timeout; |
|
137 |
|
138 val vampire = vampire_opts 60 false; |
|
139 |
|
140 fun vampire_opts_full max_new theory_const timeout = full_prover_opts |
|
141 max_new theory_const |
|
142 (Path.explode "$VAMPIRE_HOME/vampire", |
|
143 ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout)) |
|
144 timeout; |
|
145 |
|
146 val vampire_full = vampire_opts_full 60 false; |
|
147 |
|
148 |
|
149 (* E prover *) |
|
150 |
|
151 fun eprover_opts max_new theory_const timeout = tptp_prover_opts |
|
152 max_new theory_const |
|
153 (Path.explode "$E_HOME/eproof", |
|
154 "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout) |
|
155 timeout; |
|
156 |
|
157 val eprover = eprover_opts 100 false; |
|
158 |
|
159 fun eprover_opts_full max_new theory_const timeout = full_prover_opts |
|
160 max_new theory_const |
|
161 (Path.explode "$E_HOME/eproof", |
|
162 "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout) |
|
163 timeout; |
|
164 |
|
165 val eprover_full = eprover_opts_full 100 false; |
|
166 |
|
167 |
|
168 (* SPASS *) |
|
169 |
|
170 fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover |
|
171 (ResAtp.get_relevant max_new theory_const) |
|
172 (ResAtp.prepare_clauses true) |
|
173 (ResHolClause.dfg_write_file (AtpManager.get_full_types())) |
|
174 (Path.explode "$SPASS_HOME/SPASS", |
|
175 "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ |
|
176 string_of_int timeout) |
|
177 ResReconstruct.find_failure |
|
178 (ResReconstruct.lemma_list true) |
|
179 timeout ax_clauses fcls name n goal; |
|
180 |
|
181 val spass = spass_opts 40 true; |
|
182 |
|
183 |
|
184 (* remote prover invocation via SystemOnTPTP *) |
|
185 |
|
186 val systems = |
|
187 Synchronized.var "atp_wrapper_systems" ([]: string list); |
|
188 |
|
189 fun get_systems () = |
|
190 let |
|
191 val (answer, rc) = system_out (("$ISABELLE_HOME/lib/scripts/SystemOnTPTP" |> |
|
192 Path.explode |> File.shell_path) ^ " -w") |
|
193 in |
|
194 if rc <> 0 then error ("Get available systems from SystemOnTPTP:\n" ^ answer) |
|
195 else split_lines answer |
|
196 end; |
|
197 |
|
198 fun refresh_systems () = Synchronized.change systems (fn _ => |
|
199 get_systems ()); |
|
200 |
|
201 fun get_system prefix = Synchronized.change_result systems (fn systems => |
|
202 let val systems = if null systems then get_systems() else systems |
|
203 in (find_first (String.isPrefix prefix) systems, systems) end); |
|
204 |
|
205 fun remote_prover_opts max_new theory_const args prover_prefix timeout = |
|
206 let val sys = |
|
207 case get_system prover_prefix of |
|
208 NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP") |
|
209 | SOME sys => sys |
|
210 in tptp_prover_opts max_new theory_const |
|
211 (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", |
|
212 args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout |
|
213 end; |
|
214 |
|
215 val remote_prover = remote_prover_opts 60 false; |
|
216 |
|
217 end; |
|
218 |
|