blanchet@38293
|
1 |
(* Title: HOL/Tools/ATP/atp_systems.ML
|
wenzelm@28592
|
2 |
Author: Fabian Immler, TU Muenchen
|
blanchet@36371
|
3 |
Author: Jasmin Blanchette, TU Muenchen
|
wenzelm@28592
|
4 |
|
blanchet@36376
|
5 |
Setup for supported ATPs.
|
wenzelm@28592
|
6 |
*)
|
wenzelm@28592
|
7 |
|
blanchet@36376
|
8 |
signature ATP_SYSTEMS =
|
wenzelm@28592
|
9 |
sig
|
blanchet@46172
|
10 |
type atp_format = ATP_Problem.atp_format
|
blanchet@43448
|
11 |
type formula_kind = ATP_Problem.formula_kind
|
blanchet@39731
|
12 |
type failure = ATP_Proof.failure
|
blanchet@38257
|
13 |
|
blanchet@40240
|
14 |
type atp_config =
|
blanchet@43449
|
15 |
{exec : string * string,
|
blanchet@43449
|
16 |
required_execs : (string * string) list,
|
blanchet@43517
|
17 |
arguments :
|
blanchet@44344
|
18 |
Proof.context -> bool -> string -> Time.time
|
blanchet@44220
|
19 |
-> (unit -> (string * real) list) -> string,
|
blanchet@43449
|
20 |
proof_delims : (string * string) list,
|
blanchet@43449
|
21 |
known_failures : (failure * string) list,
|
blanchet@43580
|
22 |
conj_sym_kind : formula_kind,
|
blanchet@43580
|
23 |
prem_kind : formula_kind,
|
blanchet@44344
|
24 |
best_slices :
|
blanchet@45618
|
25 |
Proof.context
|
blanchet@46392
|
26 |
-> (real * (bool * (int * atp_format * string * string * string))) list}
|
blanchet@38257
|
27 |
|
blanchet@44970
|
28 |
val force_sos : bool Config.T
|
blanchet@44428
|
29 |
val e_smartN : string
|
blanchet@44428
|
30 |
val e_autoN : string
|
blanchet@44428
|
31 |
val e_fun_weightN : string
|
blanchet@44428
|
32 |
val e_sym_offset_weightN : string
|
blanchet@43517
|
33 |
val e_weight_method : string Config.T
|
blanchet@43517
|
34 |
val e_default_fun_weight : real Config.T
|
blanchet@43517
|
35 |
val e_fun_weight_base : real Config.T
|
blanchet@43517
|
36 |
val e_fun_weight_span : real Config.T
|
blanchet@43517
|
37 |
val e_default_sym_offs_weight : real Config.T
|
blanchet@43517
|
38 |
val e_sym_offs_weight_base : real Config.T
|
blanchet@43517
|
39 |
val e_sym_offs_weight_span : real Config.T
|
blanchet@40240
|
40 |
val eN : string
|
blanchet@45454
|
41 |
val e_sineN : string
|
blanchet@45454
|
42 |
val e_tofofN : string
|
blanchet@46209
|
43 |
val iproverN : string
|
blanchet@46209
|
44 |
val iprover_eqN : string
|
blanchet@45454
|
45 |
val leo2N : string
|
blanchet@46226
|
46 |
val dummy_tff1N : string
|
blanchet@46226
|
47 |
val dummy_thfN : string
|
blanchet@45454
|
48 |
val satallaxN : string
|
blanchet@45454
|
49 |
val snarkN : string
|
blanchet@40240
|
50 |
val spassN : string
|
blanchet@46172
|
51 |
val spass_newN : string
|
blanchet@40240
|
52 |
val vampireN : string
|
blanchet@43779
|
53 |
val waldmeisterN : string
|
blanchet@45282
|
54 |
val z3_tptpN : string
|
blanchet@40241
|
55 |
val remote_prefix : string
|
blanchet@42609
|
56 |
val remote_atp :
|
blanchet@42609
|
57 |
string -> string -> string list -> (string * string) list
|
blanchet@45275
|
58 |
-> (failure * string) list -> formula_kind -> formula_kind
|
blanchet@46392
|
59 |
-> (Proof.context -> int * atp_format * string * string)
|
blanchet@46392
|
60 |
-> string * atp_config
|
blanchet@40240
|
61 |
val add_atp : string * atp_config -> theory -> theory
|
blanchet@40240
|
62 |
val get_atp : theory -> string -> atp_config
|
blanchet@42591
|
63 |
val supported_atps : theory -> string list
|
blanchet@40240
|
64 |
val is_atp_installed : theory -> string -> bool
|
blanchet@35867
|
65 |
val refresh_systems_on_tptp : unit -> unit
|
blanchet@35867
|
66 |
val setup : theory -> theory
|
wenzelm@28592
|
67 |
end;
|
wenzelm@28592
|
68 |
|
blanchet@36376
|
69 |
structure ATP_Systems : ATP_SYSTEMS =
|
wenzelm@28592
|
70 |
struct
|
wenzelm@28596
|
71 |
|
blanchet@43448
|
72 |
open ATP_Problem
|
blanchet@39731
|
73 |
open ATP_Proof
|
blanchet@47148
|
74 |
open ATP_Problem_Generate
|
blanchet@39731
|
75 |
|
blanchet@40240
|
76 |
(* ATP configuration *)
|
blanchet@35826
|
77 |
|
blanchet@40240
|
78 |
type atp_config =
|
blanchet@43449
|
79 |
{exec : string * string,
|
blanchet@43449
|
80 |
required_execs : (string * string) list,
|
blanchet@43517
|
81 |
arguments :
|
blanchet@44344
|
82 |
Proof.context -> bool -> string -> Time.time
|
blanchet@44344
|
83 |
-> (unit -> (string * real) list) -> string,
|
blanchet@43449
|
84 |
proof_delims : (string * string) list,
|
blanchet@43449
|
85 |
known_failures : (failure * string) list,
|
blanchet@43580
|
86 |
conj_sym_kind : formula_kind,
|
blanchet@43580
|
87 |
prem_kind : formula_kind,
|
blanchet@44344
|
88 |
best_slices :
|
blanchet@45618
|
89 |
Proof.context
|
blanchet@46392
|
90 |
-> (real * (bool * (int * atp_format * string * string * string))) list}
|
boehmes@32864
|
91 |
|
blanchet@43588
|
92 |
(* "best_slices" must be found empirically, taking a wholistic approach since
|
blanchet@43588
|
93 |
the ATPs are run in parallel. The "real" components give the faction of the
|
blanchet@44431
|
94 |
time available given to the slice and should add up to 1.0. The "bool"
|
blanchet@43588
|
95 |
component indicates whether the slice's strategy is complete; the "int", the
|
blanchet@44431
|
96 |
preferred number of facts to pass; the first "string", the preferred type
|
blanchet@46392
|
97 |
system (which should be sound or quasi-sound); the second "string", the
|
blanchet@46392
|
98 |
preferred lambda translation scheme; the third "string", extra information to
|
blanchet@46392
|
99 |
the prover (e.g., SOS or no SOS).
|
blanchet@43588
|
100 |
|
blanchet@43588
|
101 |
The last slice should be the most "normal" one, because it will get all the
|
blanchet@44431
|
102 |
time available if the other slices fail early and also because it is used if
|
blanchet@44431
|
103 |
slicing is disabled (e.g., by the minimizer). *)
|
blanchet@43581
|
104 |
|
blanchet@38307
|
105 |
val known_perl_failures =
|
blanchet@38340
|
106 |
[(CantConnect, "HTTP error"),
|
blanchet@38340
|
107 |
(NoPerl, "env: perl"),
|
blanchet@38311
|
108 |
(NoLibwwwPerl, "Can't locate HTTP")]
|
wenzelm@28596
|
109 |
|
blanchet@46071
|
110 |
fun known_szs_failures wrap =
|
blanchet@46071
|
111 |
[(Unprovable, wrap "CounterSatisfiable"),
|
blanchet@46071
|
112 |
(Unprovable, wrap "Satisfiable"),
|
blanchet@46071
|
113 |
(GaveUp, wrap "GaveUp"),
|
blanchet@46071
|
114 |
(GaveUp, wrap "Unknown"),
|
blanchet@46071
|
115 |
(GaveUp, wrap "Incomplete"),
|
blanchet@46071
|
116 |
(ProofMissing, wrap "Theorem"),
|
blanchet@46071
|
117 |
(ProofMissing, wrap "Unsatisfiable"),
|
blanchet@46071
|
118 |
(TimedOut, wrap "Timeout"),
|
blanchet@46071
|
119 |
(Inappropriate, wrap "Inappropriate"),
|
blanchet@46071
|
120 |
(OutOfResources, wrap "ResourceOut"),
|
blanchet@46071
|
121 |
(OutOfResources, wrap "MemoryOut"),
|
blanchet@46071
|
122 |
(Interrupted, wrap "Forced"),
|
blanchet@46071
|
123 |
(Interrupted, wrap "User")]
|
blanchet@46071
|
124 |
|
blanchet@46071
|
125 |
val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
|
blanchet@46071
|
126 |
val known_says_failures = known_szs_failures (prefix " says ")
|
blanchet@46071
|
127 |
|
blanchet@40240
|
128 |
(* named ATPs *)
|
blanchet@40240
|
129 |
|
blanchet@40240
|
130 |
val eN = "e"
|
blanchet@45454
|
131 |
val e_sineN = "e_sine"
|
blanchet@45454
|
132 |
val e_tofofN = "e_tofof"
|
blanchet@46209
|
133 |
val iproverN = "iprover"
|
blanchet@46209
|
134 |
val iprover_eqN = "iprover_eq"
|
blanchet@44970
|
135 |
val leo2N = "leo2"
|
blanchet@46226
|
136 |
val dummy_tff1N = "dummy_tff1" (* experimental *)
|
blanchet@46226
|
137 |
val dummy_thfN = "dummy_thf" (* experimental *)
|
blanchet@44970
|
138 |
val satallaxN = "satallax"
|
blanchet@45454
|
139 |
val snarkN = "snark"
|
blanchet@40240
|
140 |
val spassN = "spass"
|
blanchet@46226
|
141 |
val spass_newN = "spass_new" (* experimental *)
|
blanchet@40240
|
142 |
val vampireN = "vampire"
|
blanchet@45454
|
143 |
val waldmeisterN = "waldmeister"
|
blanchet@45282
|
144 |
val z3_tptpN = "z3_tptp"
|
blanchet@40241
|
145 |
val remote_prefix = "remote_"
|
wenzelm@28596
|
146 |
|
blanchet@38257
|
147 |
structure Data = Theory_Data
|
blanchet@38257
|
148 |
(
|
blanchet@40240
|
149 |
type T = (atp_config * stamp) Symtab.table
|
blanchet@38257
|
150 |
val empty = Symtab.empty
|
blanchet@38257
|
151 |
val extend = I
|
blanchet@38257
|
152 |
fun merge data : T = Symtab.merge (eq_snd op =) data
|
blanchet@38257
|
153 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
|
blanchet@38257
|
154 |
)
|
blanchet@36370
|
155 |
|
blanchet@44852
|
156 |
fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
|
blanchet@36140
|
157 |
|
blanchet@44344
|
158 |
val sosN = "sos"
|
blanchet@44344
|
159 |
val no_sosN = "no_sos"
|
blanchet@44344
|
160 |
|
blanchet@44970
|
161 |
val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
|
blanchet@44970
|
162 |
|
blanchet@39731
|
163 |
|
blanchet@40240
|
164 |
(* E *)
|
wenzelm@28596
|
165 |
|
blanchet@45279
|
166 |
fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
|
blanchet@45279
|
167 |
|
blanchet@36369
|
168 |
val tstp_proof_delims =
|
blanchet@43803
|
169 |
[("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
|
blanchet@43803
|
170 |
("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
|
blanchet@36369
|
171 |
|
blanchet@44344
|
172 |
val e_smartN = "smart"
|
blanchet@43517
|
173 |
val e_autoN = "auto"
|
blanchet@43517
|
174 |
val e_fun_weightN = "fun_weight"
|
blanchet@43517
|
175 |
val e_sym_offset_weightN = "sym_offset_weight"
|
blanchet@42589
|
176 |
|
blanchet@43517
|
177 |
val e_weight_method =
|
blanchet@44344
|
178 |
Attrib.setup_config_string @{binding atp_e_weight_method} (K e_smartN)
|
blanchet@42641
|
179 |
(* FUDGE *)
|
blanchet@43517
|
180 |
val e_default_fun_weight =
|
blanchet@43517
|
181 |
Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
|
blanchet@43517
|
182 |
val e_fun_weight_base =
|
blanchet@43517
|
183 |
Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
|
blanchet@43517
|
184 |
val e_fun_weight_span =
|
blanchet@43517
|
185 |
Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
|
blanchet@43517
|
186 |
val e_default_sym_offs_weight =
|
blanchet@43517
|
187 |
Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
|
blanchet@43517
|
188 |
val e_sym_offs_weight_base =
|
blanchet@43517
|
189 |
Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
|
blanchet@43517
|
190 |
val e_sym_offs_weight_span =
|
blanchet@43517
|
191 |
Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
|
blanchet@42589
|
192 |
|
blanchet@43314
|
193 |
fun e_weight_method_case method fw sow =
|
blanchet@43517
|
194 |
if method = e_fun_weightN then fw
|
blanchet@43517
|
195 |
else if method = e_sym_offset_weightN then sow
|
blanchet@44349
|
196 |
else raise Fail ("unexpected " ^ quote method)
|
blanchet@42589
|
197 |
|
blanchet@43517
|
198 |
fun scaled_e_weight ctxt method w =
|
blanchet@43517
|
199 |
w * Config.get ctxt
|
blanchet@43517
|
200 |
(e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
|
blanchet@43517
|
201 |
+ Config.get ctxt
|
blanchet@43517
|
202 |
(e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
|
blanchet@42589
|
203 |
|> Real.ceil |> signed_string_of_int
|
blanchet@41561
|
204 |
|
blanchet@43517
|
205 |
fun e_weight_arguments ctxt method weights =
|
blanchet@43517
|
206 |
if method = e_autoN then
|
blanchet@42589
|
207 |
"-xAutoDev"
|
blanchet@42589
|
208 |
else
|
blanchet@44489
|
209 |
(* supplied by Stephan Schulz *)
|
blanchet@41562
|
210 |
"--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
|
blanchet@41562
|
211 |
\--destructive-er-aggressive --destructive-er --presat-simplify \
|
blanchet@41562
|
212 |
\--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
|
blanchet@41562
|
213 |
\--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
|
blanchet@43314
|
214 |
\-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
|
blanchet@42589
|
215 |
"(SimulateSOS, " ^
|
blanchet@43517
|
216 |
(e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
|
blanchet@43517
|
217 |
|> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
|
blanchet@41562
|
218 |
",20,1.5,1.5,1" ^
|
blanchet@43517
|
219 |
(weights ()
|
blanchet@43517
|
220 |
|> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
|
blanchet@43517
|
221 |
|> implode) ^
|
blanchet@41562
|
222 |
"),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
|
blanchet@41562
|
223 |
\1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
|
blanchet@41562
|
224 |
\FIFOWeight(PreferProcessed))'"
|
blanchet@41561
|
225 |
|
blanchet@43517
|
226 |
fun effective_e_weight_method ctxt =
|
blanchet@43517
|
227 |
if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
|
blanchet@43314
|
228 |
|
blanchet@40240
|
229 |
val e_config : atp_config =
|
blanchet@38338
|
230 |
{exec = ("E_HOME", "eproof"),
|
blanchet@38338
|
231 |
required_execs = [],
|
blanchet@44220
|
232 |
arguments =
|
blanchet@44429
|
233 |
fn ctxt => fn _ => fn method => fn timeout => fn weights =>
|
blanchet@44344
|
234 |
"--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
|
blanchet@44852
|
235 |
" -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
|
blanchet@43803
|
236 |
proof_delims = tstp_proof_delims,
|
blanchet@36265
|
237 |
known_failures =
|
blanchet@46071
|
238 |
known_szs_status_failures @
|
blanchet@46071
|
239 |
[(TimedOut, "Failure: Resource limit exceeded (time)"),
|
blanchet@36370
|
240 |
(TimedOut, "time limit exceeded"),
|
blanchet@46071
|
241 |
(OutOfResources, "# Cannot determine problem status")],
|
blanchet@44327
|
242 |
conj_sym_kind = Hypothesis,
|
blanchet@43580
|
243 |
prem_kind = Conjecture,
|
blanchet@43517
|
244 |
best_slices = fn ctxt =>
|
blanchet@44344
|
245 |
let val method = effective_e_weight_method ctxt in
|
blanchet@44345
|
246 |
(* FUDGE *)
|
blanchet@44344
|
247 |
if method = e_smartN then
|
blanchet@46392
|
248 |
[(0.333, (true, (500, FOF, "mono_tags??", combinatorsN,
|
blanchet@46392
|
249 |
e_fun_weightN))),
|
blanchet@46392
|
250 |
(0.334, (true, (50, FOF, "mono_guards??", combinatorsN,
|
blanchet@46392
|
251 |
e_fun_weightN))),
|
blanchet@46392
|
252 |
(0.333, (true, (1000, FOF, "mono_tags??", combinatorsN,
|
blanchet@46392
|
253 |
e_sym_offset_weightN)))]
|
blanchet@44344
|
254 |
else
|
blanchet@46392
|
255 |
[(1.0, (true, (500, FOF, "mono_tags??", combinatorsN, method)))]
|
blanchet@44344
|
256 |
end}
|
blanchet@38698
|
257 |
|
blanchet@40240
|
258 |
val e = (eN, e_config)
|
wenzelm@28596
|
259 |
|
wenzelm@28596
|
260 |
|
blanchet@44970
|
261 |
(* LEO-II *)
|
blanchet@44970
|
262 |
|
blanchet@45618
|
263 |
val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
|
blanchet@45618
|
264 |
|
blanchet@44970
|
265 |
val leo2_config : atp_config =
|
blanchet@44970
|
266 |
{exec = ("LEO2_HOME", "leo"),
|
blanchet@44970
|
267 |
required_execs = [],
|
blanchet@44970
|
268 |
arguments =
|
blanchet@44970
|
269 |
fn _ => fn _ => fn sos => fn timeout => fn _ =>
|
blanchet@46171
|
270 |
"--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
|
blanchet@44970
|
271 |
|> sos = sosN ? prefix "--sos ",
|
blanchet@44970
|
272 |
proof_delims = tstp_proof_delims,
|
blanchet@46078
|
273 |
known_failures =
|
blanchet@46078
|
274 |
known_szs_status_failures @
|
blanchet@46078
|
275 |
[(TimedOut, "CPU time limit exceeded, terminating")],
|
blanchet@44970
|
276 |
conj_sym_kind = Axiom,
|
blanchet@44970
|
277 |
prem_kind = Hypothesis,
|
blanchet@44970
|
278 |
best_slices = fn ctxt =>
|
blanchet@44970
|
279 |
(* FUDGE *)
|
blanchet@46392
|
280 |
[(0.667, (false, (150, leo2_thf0, "mono_simple_higher", lam_liftingN,
|
blanchet@46392
|
281 |
sosN))),
|
blanchet@46392
|
282 |
(0.333, (true, (50, leo2_thf0, "mono_simple_higher", lam_liftingN,
|
blanchet@46392
|
283 |
no_sosN)))]
|
blanchet@44970
|
284 |
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
|
blanchet@44970
|
285 |
else I)}
|
blanchet@44970
|
286 |
|
blanchet@44970
|
287 |
val leo2 = (leo2N, leo2_config)
|
blanchet@44970
|
288 |
|
blanchet@44970
|
289 |
|
blanchet@44970
|
290 |
(* Satallax *)
|
blanchet@44970
|
291 |
|
blanchet@45618
|
292 |
val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
|
blanchet@45618
|
293 |
|
blanchet@44970
|
294 |
val satallax_config : atp_config =
|
blanchet@44970
|
295 |
{exec = ("SATALLAX_HOME", "satallax"),
|
blanchet@44970
|
296 |
required_execs = [],
|
blanchet@44970
|
297 |
arguments =
|
blanchet@44970
|
298 |
fn _ => fn _ => fn _ => fn timeout => fn _ =>
|
blanchet@46033
|
299 |
"-p hocore -t " ^ string_of_int (to_secs 1 timeout),
|
blanchet@46033
|
300 |
proof_delims =
|
blanchet@46033
|
301 |
[("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
|
blanchet@46071
|
302 |
known_failures = known_szs_status_failures,
|
blanchet@44970
|
303 |
conj_sym_kind = Axiom,
|
blanchet@44970
|
304 |
prem_kind = Hypothesis,
|
blanchet@45275
|
305 |
best_slices =
|
blanchet@45618
|
306 |
(* FUDGE *)
|
blanchet@46392
|
307 |
K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", keep_lamsN,
|
blanchet@46392
|
308 |
"")))]}
|
blanchet@44970
|
309 |
|
blanchet@44970
|
310 |
val satallax = (satallaxN, satallax_config)
|
blanchet@44970
|
311 |
|
blanchet@44970
|
312 |
|
blanchet@39731
|
313 |
(* SPASS *)
|
blanchet@39731
|
314 |
|
blanchet@36219
|
315 |
(* The "-VarWeight=3" option helps the higher-order problems, probably by
|
blanchet@45307
|
316 |
counteracting the presence of explicit application operators. *)
|
blanchet@40240
|
317 |
val spass_config : atp_config =
|
blanchet@38338
|
318 |
{exec = ("ISABELLE_ATP", "scripts/spass"),
|
blanchet@39246
|
319 |
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
|
blanchet@44431
|
320 |
arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
|
blanchet@38199
|
321 |
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
|
blanchet@44852
|
322 |
\-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
|
blanchet@44344
|
323 |
|> sos = sosN ? prefix "-SOS=1 ",
|
blanchet@36369
|
324 |
proof_delims = [("Here is a proof", "Formulae used in the proof")],
|
blanchet@36289
|
325 |
known_failures =
|
blanchet@38307
|
326 |
known_perl_failures @
|
blanchet@43891
|
327 |
[(GaveUp, "SPASS beiseite: Completion found"),
|
blanchet@36370
|
328 |
(TimedOut, "SPASS beiseite: Ran out of time"),
|
blanchet@36958
|
329 |
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
|
blanchet@37388
|
330 |
(MalformedInput, "Undefined symbol"),
|
blanchet@37389
|
331 |
(MalformedInput, "Free Variable"),
|
blanchet@45250
|
332 |
(Unprovable, "No formulae and clauses found in input file"),
|
blanchet@39490
|
333 |
(InternalError, "Please report this error")],
|
blanchet@44327
|
334 |
conj_sym_kind = Hypothesis,
|
blanchet@43580
|
335 |
prem_kind = Conjecture,
|
blanchet@43590
|
336 |
best_slices = fn ctxt =>
|
blanchet@43588
|
337 |
(* FUDGE *)
|
blanchet@46392
|
338 |
[(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", lam_liftingN,
|
blanchet@46392
|
339 |
sosN))),
|
blanchet@46392
|
340 |
(0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", lam_liftingN,
|
blanchet@46392
|
341 |
sosN))),
|
blanchet@46747
|
342 |
(0.334, (false, (50, DFG DFG_Unsorted, "mono_tags??", lam_liftingN,
|
blanchet@46747
|
343 |
no_sosN)))]
|
blanchet@44970
|
344 |
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
|
blanchet@43590
|
345 |
else I)}
|
blanchet@38698
|
346 |
|
blanchet@40240
|
347 |
val spass = (spassN, spass_config)
|
wenzelm@28596
|
348 |
|
blanchet@46172
|
349 |
(* Experimental *)
|
blanchet@46172
|
350 |
val spass_new_config : atp_config =
|
blanchet@46172
|
351 |
{exec = ("SPASS_HOME", "SPASS"),
|
blanchet@46172
|
352 |
required_execs = [],
|
blanchet@46172
|
353 |
arguments = #arguments spass_config,
|
blanchet@46172
|
354 |
proof_delims = #proof_delims spass_config,
|
blanchet@46172
|
355 |
known_failures = #known_failures spass_config,
|
blanchet@46172
|
356 |
conj_sym_kind = #conj_sym_kind spass_config,
|
blanchet@46172
|
357 |
prem_kind = #prem_kind spass_config,
|
blanchet@46172
|
358 |
best_slices = fn ctxt =>
|
blanchet@46172
|
359 |
(* FUDGE *)
|
blanchet@46392
|
360 |
[(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", lam_liftingN,
|
blanchet@46392
|
361 |
sosN))) (*,
|
blanchet@46392
|
362 |
(0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", lam_liftingN,
|
blanchet@46392
|
363 |
sosN))),
|
blanchet@46392
|
364 |
(0.334, (true, (50, DFG DFG_Sorted, "mono_simple", lam_liftingN,
|
blanchet@46392
|
365 |
no_sosN)))*)]
|
blanchet@46172
|
366 |
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
|
blanchet@46172
|
367 |
else I)}
|
blanchet@46172
|
368 |
|
blanchet@46172
|
369 |
val spass_new = (spass_newN, spass_new_config)
|
blanchet@46172
|
370 |
|
blanchet@38698
|
371 |
|
blanchet@37509
|
372 |
(* Vampire *)
|
blanchet@37509
|
373 |
|
blanchet@45362
|
374 |
(* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
|
blanchet@45362
|
375 |
SystemOnTPTP. *)
|
blanchet@45279
|
376 |
fun is_old_vampire_version () =
|
blanchet@45362
|
377 |
string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
|
blanchet@45279
|
378 |
|
blanchet@45618
|
379 |
val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
|
blanchet@45453
|
380 |
|
blanchet@40240
|
381 |
val vampire_config : atp_config =
|
blanchet@38338
|
382 |
{exec = ("VAMPIRE_HOME", "vampire"),
|
blanchet@38338
|
383 |
required_execs = [],
|
blanchet@44431
|
384 |
arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
|
blanchet@45276
|
385 |
"--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
|
blanchet@46103
|
386 |
" --proof tptp --output_axiom_names on\
|
blanchet@46103
|
387 |
\ --forced_options propositional_to_bdd=off\
|
blanchet@45276
|
388 |
\ --thanks \"Andrei and Krystof\" --input_file"
|
blanchet@44344
|
389 |
|> sos = sosN ? prefix "--sos on ",
|
blanchet@37509
|
390 |
proof_delims =
|
blanchet@37509
|
391 |
[("=========== Refutation ==========",
|
blanchet@37509
|
392 |
"======= End of refutation ======="),
|
blanchet@38279
|
393 |
("% SZS output start Refutation", "% SZS output end Refutation"),
|
blanchet@38279
|
394 |
("% SZS output start Proof", "% SZS output end Proof")],
|
blanchet@37509
|
395 |
known_failures =
|
blanchet@46071
|
396 |
known_szs_status_failures @
|
blanchet@43891
|
397 |
[(GaveUp, "UNPROVABLE"),
|
blanchet@43891
|
398 |
(GaveUp, "CANNOT PROVE"),
|
blanchet@37509
|
399 |
(Unprovable, "Satisfiability detected"),
|
blanchet@38885
|
400 |
(Unprovable, "Termination reason: Satisfiable"),
|
blanchet@39490
|
401 |
(Interrupted, "Aborted by signal SIGINT")],
|
blanchet@44327
|
402 |
conj_sym_kind = Conjecture,
|
blanchet@43580
|
403 |
prem_kind = Conjecture,
|
blanchet@43590
|
404 |
best_slices = fn ctxt =>
|
blanchet@43588
|
405 |
(* FUDGE *)
|
blanchet@45279
|
406 |
(if is_old_vampire_version () then
|
blanchet@46392
|
407 |
[(0.333, (false, (150, FOF, "poly_guards??", hybrid_lamsN, sosN))),
|
blanchet@46392
|
408 |
(0.333, (false, (500, FOF, "mono_tags??", hybrid_lamsN, sosN))),
|
blanchet@46392
|
409 |
(0.334, (true, (50, FOF, "mono_guards??", hybrid_lamsN, no_sosN)))]
|
blanchet@45279
|
410 |
else
|
blanchet@46392
|
411 |
[(0.333, (false, (150, vampire_tff0, "poly_guards??", hybrid_lamsN,
|
blanchet@46392
|
412 |
sosN))),
|
blanchet@46392
|
413 |
(0.333, (false, (500, vampire_tff0, "mono_simple", hybrid_lamsN,
|
blanchet@46392
|
414 |
sosN))),
|
blanchet@46392
|
415 |
(0.334, (true, (50, vampire_tff0, "mono_simple", hybrid_lamsN,
|
blanchet@46392
|
416 |
no_sosN)))])
|
blanchet@44970
|
417 |
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
|
blanchet@43590
|
418 |
else I)}
|
blanchet@38698
|
419 |
|
blanchet@40240
|
420 |
val vampire = (vampireN, vampire_config)
|
blanchet@37509
|
421 |
|
blanchet@38698
|
422 |
|
blanchet@42611
|
423 |
(* Z3 with TPTP syntax *)
|
blanchet@42611
|
424 |
|
blanchet@45618
|
425 |
val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
|
blanchet@45453
|
426 |
|
blanchet@45282
|
427 |
val z3_tptp_config : atp_config =
|
blanchet@42611
|
428 |
{exec = ("Z3_HOME", "z3"),
|
blanchet@42611
|
429 |
required_execs = [],
|
blanchet@44220
|
430 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
|
blanchet@45279
|
431 |
"MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
|
blanchet@42611
|
432 |
proof_delims = [],
|
blanchet@46071
|
433 |
known_failures = known_szs_status_failures,
|
blanchet@43580
|
434 |
conj_sym_kind = Hypothesis,
|
blanchet@43580
|
435 |
prem_kind = Hypothesis,
|
blanchet@43588
|
436 |
best_slices =
|
blanchet@45282
|
437 |
(* FUDGE *)
|
blanchet@46392
|
438 |
K [(0.5, (false, (250, z3_tff0, "mono_simple", combinatorsN, ""))),
|
blanchet@46392
|
439 |
(0.25, (false, (125, z3_tff0, "mono_simple", combinatorsN, ""))),
|
blanchet@46392
|
440 |
(0.125, (false, (62, z3_tff0, "mono_simple", combinatorsN, ""))),
|
blanchet@46392
|
441 |
(0.125, (false, (31, z3_tff0, "mono_simple", combinatorsN, "")))]}
|
blanchet@42611
|
442 |
|
blanchet@45282
|
443 |
val z3_tptp = (z3_tptpN, z3_tptp_config)
|
blanchet@42611
|
444 |
|
blanchet@45454
|
445 |
|
blanchet@45618
|
446 |
(* Not really a prover: Experimental Polymorphic TFF and THF output *)
|
blanchet@45454
|
447 |
|
blanchet@45618
|
448 |
fun dummy_config format type_enc : atp_config =
|
blanchet@45460
|
449 |
{exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
|
blanchet@45454
|
450 |
required_execs = [],
|
blanchet@45454
|
451 |
arguments = K (K (K (K (K "")))),
|
blanchet@45454
|
452 |
proof_delims = [],
|
blanchet@46071
|
453 |
known_failures = known_szs_status_failures,
|
blanchet@45454
|
454 |
conj_sym_kind = Hypothesis,
|
blanchet@45454
|
455 |
prem_kind = Hypothesis,
|
blanchet@46392
|
456 |
best_slices =
|
blanchet@46392
|
457 |
K [(1.0, (false, (200, format, type_enc,
|
blanchet@46392
|
458 |
if is_format_higher_order format then keep_lamsN
|
blanchet@46392
|
459 |
else combinatorsN, "")))]}
|
blanchet@45454
|
460 |
|
blanchet@46226
|
461 |
val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
|
blanchet@46226
|
462 |
val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
|
blanchet@46226
|
463 |
val dummy_tff1 = (dummy_tff1N, dummy_tff1_config)
|
blanchet@45454
|
464 |
|
blanchet@46226
|
465 |
val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
|
blanchet@46226
|
466 |
val dummy_thf_config = dummy_config dummy_thf_format "poly_simple_higher"
|
blanchet@46226
|
467 |
val dummy_thf = (dummy_thfN, dummy_thf_config)
|
blanchet@45618
|
468 |
|
blanchet@42611
|
469 |
|
blanchet@40240
|
470 |
(* Remote ATP invocation via SystemOnTPTP *)
|
wenzelm@28596
|
471 |
|
blanchet@38307
|
472 |
val systems = Synchronized.var "atp_systems" ([] : string list)
|
immler@31828
|
473 |
|
immler@31828
|
474 |
fun get_systems () =
|
blanchet@45453
|
475 |
case Isabelle_System.bash_output
|
blanchet@45453
|
476 |
"\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
|
blanchet@39731
|
477 |
(output, 0) => split_lines output
|
blanchet@39731
|
478 |
| (output, _) =>
|
blanchet@39731
|
479 |
error (case extract_known_failure known_perl_failures output of
|
blanchet@42615
|
480 |
SOME failure => string_for_failure failure
|
blanchet@39731
|
481 |
| NONE => perhaps (try (unsuffix "\n")) output ^ ".")
|
immler@31828
|
482 |
|
blanchet@43408
|
483 |
fun find_system name [] systems =
|
blanchet@43408
|
484 |
find_first (String.isPrefix (name ^ "---")) systems
|
blanchet@38929
|
485 |
| find_system name (version :: versions) systems =
|
blanchet@38929
|
486 |
case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
|
blanchet@38929
|
487 |
NONE => find_system name versions systems
|
blanchet@38929
|
488 |
| res => res
|
blanchet@38929
|
489 |
|
blanchet@38929
|
490 |
fun get_system name versions =
|
blanchet@38812
|
491 |
Synchronized.change_result systems
|
blanchet@38812
|
492 |
(fn systems => (if null systems then get_systems () else systems)
|
blanchet@43796
|
493 |
|> `(`(find_system name versions)))
|
immler@31828
|
494 |
|
blanchet@38929
|
495 |
fun the_system name versions =
|
blanchet@38929
|
496 |
case get_system name versions of
|
blanchet@43796
|
497 |
(SOME sys, _) => sys
|
blanchet@43796
|
498 |
| (NONE, []) => error ("SystemOnTPTP is currently not available.")
|
blanchet@43796
|
499 |
| (NONE, syss) =>
|
blanchet@43796
|
500 |
error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
|
blanchet@43796
|
501 |
"(Available systems: " ^ commas_quote syss ^ ".)")
|
wenzelm@28596
|
502 |
|
blanchet@41396
|
503 |
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
|
blanchet@41396
|
504 |
|
blanchet@38929
|
505 |
fun remote_config system_name system_versions proof_delims known_failures
|
blanchet@45275
|
506 |
conj_sym_kind prem_kind best_slice : atp_config =
|
blanchet@38338
|
507 |
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
|
blanchet@38338
|
508 |
required_execs = [],
|
blanchet@44220
|
509 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
|
blanchet@44852
|
510 |
"-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
|
blanchet@41396
|
511 |
^ " -s " ^ the_system system_name system_versions,
|
blanchet@43803
|
512 |
proof_delims = union (op =) tstp_proof_delims proof_delims,
|
blanchet@46071
|
513 |
known_failures = known_failures @ known_perl_failures @ known_says_failures,
|
blanchet@43580
|
514 |
conj_sym_kind = conj_sym_kind,
|
blanchet@43580
|
515 |
prem_kind = prem_kind,
|
blanchet@44344
|
516 |
best_slices = fn ctxt =>
|
blanchet@46392
|
517 |
let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
|
blanchet@46392
|
518 |
[(1.0, (false, (max_relevant, format, type_enc, lam_trans, "")))]
|
blanchet@44344
|
519 |
end}
|
blanchet@43314
|
520 |
|
blanchet@44371
|
521 |
fun remotify_config system_name system_versions best_slice
|
blanchet@45275
|
522 |
({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
|
blanchet@44371
|
523 |
: atp_config) : atp_config =
|
blanchet@38929
|
524 |
remote_config system_name system_versions proof_delims known_failures
|
blanchet@45275
|
525 |
conj_sym_kind prem_kind best_slice
|
blanchet@38257
|
526 |
|
blanchet@40240
|
527 |
fun remote_atp name system_name system_versions proof_delims known_failures
|
blanchet@45275
|
528 |
conj_sym_kind prem_kind best_slice =
|
blanchet@40241
|
529 |
(remote_prefix ^ name,
|
blanchet@38929
|
530 |
remote_config system_name system_versions proof_delims known_failures
|
blanchet@45275
|
531 |
conj_sym_kind prem_kind best_slice)
|
blanchet@44371
|
532 |
fun remotify_atp (name, config) system_name system_versions best_slice =
|
blanchet@44371
|
533 |
(remote_prefix ^ name,
|
blanchet@44371
|
534 |
remotify_config system_name system_versions best_slice config)
|
wenzelm@28592
|
535 |
|
blanchet@45618
|
536 |
val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
|
blanchet@45453
|
537 |
|
blanchet@44371
|
538 |
val remote_e =
|
blanchet@44371
|
539 |
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
|
blanchet@46392
|
540 |
(K (750, FOF, "mono_tags??", combinatorsN) (* FUDGE *))
|
blanchet@44970
|
541 |
val remote_leo2 =
|
blanchet@44970
|
542 |
remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
|
blanchet@46392
|
543 |
(K (100, leo2_thf0, "mono_simple_higher", lam_liftingN) (* FUDGE *))
|
blanchet@44970
|
544 |
val remote_satallax =
|
blanchet@44970
|
545 |
remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
|
blanchet@46392
|
546 |
(K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *))
|
blanchet@44371
|
547 |
val remote_vampire =
|
blanchet@45354
|
548 |
remotify_atp vampire "Vampire" ["1.8"]
|
blanchet@46392
|
549 |
(K (250, FOF, "mono_guards??", hybrid_lamsN) (* FUDGE *))
|
blanchet@45282
|
550 |
val remote_z3_tptp =
|
blanchet@45618
|
551 |
remotify_atp z3_tptp "Z3" ["3.0"]
|
blanchet@46392
|
552 |
(K (250, z3_tff0, "mono_simple", combinatorsN) (* FUDGE *))
|
blanchet@44963
|
553 |
val remote_e_sine =
|
blanchet@44963
|
554 |
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
|
blanchet@46392
|
555 |
Conjecture (K (500, FOF, "mono_guards??", combinatorsN) (* FUDGE *))
|
blanchet@46209
|
556 |
val remote_iprover =
|
blanchet@46209
|
557 |
remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
|
blanchet@46392
|
558 |
(K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *))
|
blanchet@46209
|
559 |
val remote_iprover_eq =
|
blanchet@46209
|
560 |
remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
|
blanchet@46392
|
561 |
(K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *))
|
blanchet@42611
|
562 |
val remote_snark =
|
blanchet@43780
|
563 |
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
|
blanchet@46392
|
564 |
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
|
blanchet@46392
|
565 |
(K (100, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *))
|
blanchet@44963
|
566 |
val remote_e_tofof =
|
blanchet@45453
|
567 |
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
|
blanchet@46392
|
568 |
Hypothesis
|
blanchet@46392
|
569 |
(K (150, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *))
|
blanchet@43779
|
570 |
val remote_waldmeister =
|
blanchet@43779
|
571 |
remote_atp waldmeisterN "Waldmeister" ["710"]
|
blanchet@46392
|
572 |
[("#START OF PROOF", "Proved Goals:")]
|
blanchet@46392
|
573 |
[(OutOfResources, "Too many function symbols"),
|
blanchet@46392
|
574 |
(Crashed, "Unrecoverable Segmentation Fault")]
|
blanchet@46392
|
575 |
Hypothesis Hypothesis
|
blanchet@46392
|
576 |
(K (50, CNF_UEQ, "mono_tags??", combinatorsN) (* FUDGE *))
|
blanchet@38698
|
577 |
|
blanchet@38698
|
578 |
(* Setup *)
|
blanchet@38698
|
579 |
|
blanchet@40240
|
580 |
fun add_atp (name, config) thy =
|
blanchet@40240
|
581 |
Data.map (Symtab.update_new (name, (config, stamp ()))) thy
|
blanchet@40240
|
582 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
|
blanchet@36371
|
583 |
|
blanchet@40240
|
584 |
fun get_atp thy name =
|
blanchet@40240
|
585 |
the (Symtab.lookup (Data.get thy) name) |> fst
|
blanchet@40240
|
586 |
handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
|
blanchet@36371
|
587 |
|
blanchet@42591
|
588 |
val supported_atps = Symtab.keys o Data.get
|
blanchet@40240
|
589 |
|
blanchet@40240
|
590 |
fun is_atp_installed thy name =
|
blanchet@40240
|
591 |
let val {exec, required_execs, ...} = get_atp thy name in
|
blanchet@40240
|
592 |
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
|
blanchet@40240
|
593 |
end
|
blanchet@40240
|
594 |
|
blanchet@40240
|
595 |
fun refresh_systems_on_tptp () =
|
blanchet@40240
|
596 |
Synchronized.change systems (fn _ => get_systems ())
|
blanchet@40240
|
597 |
|
blanchet@43803
|
598 |
val atps =
|
blanchet@46226
|
599 |
[e, leo2, dummy_tff1, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp,
|
blanchet@46226
|
600 |
remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
|
blanchet@46210
|
601 |
remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
|
blanchet@46210
|
602 |
remote_waldmeister]
|
blanchet@40240
|
603 |
val setup = fold add_atp atps
|
blanchet@35867
|
604 |
|
wenzelm@28592
|
605 |
end;
|