author | blanchet |
Thu, 24 Mar 2011 17:49:27 +0100 | |
changeset 42102 | fcfd07f122d4 |
parent 39502 | cffceed8e7fa |
child 43269 | 3535f16d9714 |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* METIS FIRST ORDER PROVER *) |
|
39502 | 3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
open Useful; |
|
7 |
||
8 |
(* ------------------------------------------------------------------------- *) |
|
9 |
(* The program name and version. *) |
|
10 |
(* ------------------------------------------------------------------------- *) |
|
11 |
||
12 |
val PROGRAM = "metis"; |
|
13 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
14 |
val VERSION = "2.3"; |
39348 | 15 |
|
42102 | 16 |
val versionString = PROGRAM^" "^VERSION^" (release 20101229)"^"\n"; |
39348 | 17 |
|
18 |
(* ------------------------------------------------------------------------- *) |
|
19 |
(* Program options. *) |
|
20 |
(* ------------------------------------------------------------------------- *) |
|
21 |
||
42102 | 22 |
val ITEMS = ["name","goal","clauses","size","category","proof","saturation"]; |
23 |
||
24 |
val TIMEOUT : int option ref = ref NONE; |
|
25 |
||
26 |
val TPTP : string option ref = ref NONE; |
|
27 |
||
39348 | 28 |
val QUIET = ref false; |
29 |
||
30 |
val TEST = ref false; |
|
31 |
||
32 |
val extended_items = "all" :: ITEMS; |
|
33 |
||
42102 | 34 |
val show_items = List.map (fn s => (s, ref false)) ITEMS; |
39348 | 35 |
|
36 |
fun show_ref s = |
|
37 |
case List.find (equal s o fst) show_items of |
|
38 |
NONE => raise Bug ("item " ^ s ^ " not found") |
|
39 |
| SOME (_,r) => r; |
|
40 |
||
41 |
fun show_set b = app (fn (_,r) => r := b) show_items; |
|
42 |
||
43 |
fun showing s = not (!QUIET) andalso (s = "status" orelse !(show_ref s)); |
|
44 |
||
45 |
fun notshowing s = not (showing s); |
|
46 |
||
47 |
fun showing_any () = List.exists showing ITEMS; |
|
48 |
||
49 |
fun notshowing_any () = not (showing_any ()); |
|
50 |
||
51 |
fun show "all" = show_set true |
|
52 |
| show s = case show_ref s of r => r := true; |
|
53 |
||
54 |
fun hide "all" = show_set false |
|
55 |
| hide s = case show_ref s of r => r := false; |
|
56 |
||
57 |
(* ------------------------------------------------------------------------- *) |
|
58 |
(* Process command line arguments and environment variables. *) |
|
59 |
(* ------------------------------------------------------------------------- *) |
|
60 |
||
61 |
local |
|
62 |
open Useful Options; |
|
63 |
in |
|
64 |
val specialOptions = |
|
65 |
[{switches = ["--show"], arguments = ["ITEM"], |
|
66 |
description = "show ITEM (see below for list)", |
|
67 |
processor = |
|
68 |
beginOpt (enumOpt extended_items endOpt) (fn _ => fn s => show s)}, |
|
69 |
{switches = ["--hide"], arguments = ["ITEM"], |
|
70 |
description = "hide ITEM (see below for list)", |
|
71 |
processor = |
|
72 |
beginOpt (enumOpt extended_items endOpt) (fn _ => fn s => hide s)}, |
|
42102 | 73 |
{switches = ["--time-limit"], arguments = ["N"], |
74 |
description = "give up after N seconds", |
|
75 |
processor = |
|
76 |
beginOpt (optionOpt ("-", intOpt (SOME 0, NONE)) endOpt) |
|
77 |
(fn _ => fn n => TIMEOUT := n)}, |
|
39348 | 78 |
{switches = ["--tptp"], arguments = ["DIR"], |
79 |
description = "specify the TPTP installation directory", |
|
80 |
processor = |
|
81 |
beginOpt (stringOpt endOpt) (fn _ => fn s => TPTP := SOME s)}, |
|
82 |
{switches = ["-q","--quiet"], arguments = [], |
|
83 |
description = "Run quietly; indicate provability with return value", |
|
84 |
processor = beginOpt endOpt (fn _ => QUIET := true)}, |
|
85 |
{switches = ["--test"], arguments = [], |
|
86 |
description = "Skip the proof search for the input problems", |
|
87 |
processor = beginOpt endOpt (fn _ => TEST := true)}]; |
|
88 |
end; |
|
89 |
||
90 |
val programOptions = |
|
91 |
{name = PROGRAM, |
|
92 |
version = versionString, |
|
93 |
header = "usage: "^PROGRAM^" [option ...] problem.tptp ...\n" ^ |
|
94 |
"Proves the input TPTP problem files.\n", |
|
95 |
footer = "Possible ITEMs are {" ^ join "," extended_items ^ "}.\n" ^ |
|
96 |
"Problems can be read from standard input using the " ^ |
|
97 |
"special - filename.\n", |
|
98 |
options = specialOptions @ Options.basicOptions}; |
|
99 |
||
100 |
fun exit x : unit = Options.exit programOptions x; |
|
101 |
fun succeed () = Options.succeed programOptions; |
|
102 |
fun fail mesg = Options.fail programOptions mesg; |
|
103 |
fun usage mesg = Options.usage programOptions mesg; |
|
104 |
||
105 |
fun processOptions () = |
|
106 |
let |
|
107 |
val args = CommandLine.arguments () |
|
108 |
||
109 |
val (_,work) = Options.processOptions programOptions args |
|
110 |
||
111 |
val () = |
|
112 |
case !TPTP of |
|
113 |
SOME _ => () |
|
114 |
| NONE => TPTP := OS.Process.getEnv "TPTP" |
|
115 |
in |
|
116 |
work |
|
117 |
end; |
|
118 |
||
119 |
(* ------------------------------------------------------------------------- *) |
|
120 |
(* The core application. *) |
|
121 |
(* ------------------------------------------------------------------------- *) |
|
122 |
||
42102 | 123 |
fun newLimit () = |
124 |
case !TIMEOUT of |
|
125 |
NONE => K true |
|
126 |
| SOME lim => |
|
127 |
let |
|
128 |
val timer = Timer.startRealTimer () |
|
129 |
||
130 |
val lim = Time.fromReal (Real.fromInt lim) |
|
131 |
||
132 |
fun check () = |
|
133 |
let |
|
134 |
val time = Timer.checkRealTimer timer |
|
135 |
in |
|
136 |
Time.<= (time,lim) |
|
137 |
end |
|
138 |
in |
|
139 |
check |
|
140 |
end; |
|
141 |
||
39348 | 142 |
(*MetisDebug |
143 |
val next_cnf = |
|
144 |
let |
|
145 |
val cnf_counter = ref 0 |
|
146 |
in |
|
147 |
fn () => |
|
148 |
let |
|
149 |
val ref cnf_count = cnf_counter |
|
150 |
val () = cnf_counter := cnf_count + 1 |
|
151 |
in |
|
152 |
cnf_count |
|
153 |
end |
|
154 |
end; |
|
155 |
*) |
|
156 |
||
157 |
local |
|
158 |
fun display_sep () = |
|
159 |
if notshowing_any () then () |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
160 |
else TextIO.print (nChars #"-" (!Print.lineLength) ^ "\n"); |
39348 | 161 |
|
162 |
fun display_name filename = |
|
163 |
if notshowing "name" then () |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
164 |
else TextIO.print ("Problem: " ^ filename ^ "\n\n"); |
39348 | 165 |
|
166 |
fun display_goal tptp = |
|
167 |
if notshowing "goal" then () |
|
168 |
else |
|
169 |
let |
|
170 |
val goal = Tptp.goal tptp |
|
171 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
172 |
TextIO.print ("Goal:\n" ^ Formula.toString goal ^ "\n\n") |
39348 | 173 |
end; |
174 |
||
175 |
fun display_clauses cls = |
|
176 |
if notshowing "clauses" then () |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
177 |
else TextIO.print ("Clauses:\n" ^ Problem.toString cls ^ "\n\n"); |
39348 | 178 |
|
179 |
fun display_size cls = |
|
180 |
if notshowing "size" then () |
|
181 |
else |
|
182 |
let |
|
183 |
fun plural 1 s = "1 " ^ s |
|
184 |
| plural n s = Int.toString n ^ " " ^ s ^ "s" |
|
185 |
||
186 |
val {clauses,literals,symbols,typedSymbols} = Problem.size cls |
|
187 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
188 |
TextIO.print |
39348 | 189 |
("Size: " ^ |
190 |
plural clauses "clause" ^ ", " ^ |
|
191 |
plural literals "literal" ^ ", " ^ |
|
192 |
plural symbols "symbol" ^ ", " ^ |
|
193 |
plural typedSymbols "typed symbol" ^ ".\n\n") |
|
194 |
end; |
|
195 |
||
196 |
fun display_category cls = |
|
197 |
if notshowing "category" then () |
|
198 |
else |
|
199 |
let |
|
200 |
val cat = Problem.categorize cls |
|
201 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
202 |
TextIO.print ("Category: " ^ Problem.categoryToString cat ^ ".\n\n") |
39348 | 203 |
end; |
204 |
||
205 |
local |
|
206 |
fun display_proof_start filename = |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
207 |
TextIO.print ("\nSZS output start CNFRefutation for " ^ filename ^ "\n"); |
39348 | 208 |
|
209 |
fun display_proof_body problem proofs = |
|
210 |
let |
|
211 |
val comments = [] |
|
212 |
||
213 |
val includes = [] |
|
214 |
||
215 |
val formulas = |
|
216 |
Tptp.fromProof |
|
217 |
{problem = problem, |
|
218 |
proofs = proofs} |
|
219 |
||
220 |
val proof = |
|
221 |
Tptp.Problem |
|
222 |
{comments = comments, |
|
223 |
includes = includes, |
|
224 |
formulas = formulas} |
|
225 |
||
226 |
val mapping = Tptp.defaultMapping |
|
227 |
val mapping = Tptp.addVarSetMapping mapping (Tptp.freeVars proof) |
|
228 |
||
229 |
val filename = "-" |
|
230 |
in |
|
231 |
Tptp.write |
|
232 |
{problem = proof, |
|
233 |
mapping = mapping, |
|
234 |
filename = filename} |
|
235 |
end; |
|
236 |
||
237 |
fun display_proof_end filename = |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
238 |
TextIO.print ("SZS output end CNFRefutation for " ^ filename ^ "\n\n"); |
39348 | 239 |
in |
240 |
fun display_proof filename problem proofs = |
|
241 |
if notshowing "proof" then () |
|
242 |
else |
|
243 |
let |
|
244 |
val () = display_proof_start filename |
|
245 |
val () = display_proof_body problem proofs |
|
246 |
val () = display_proof_end filename |
|
247 |
in |
|
248 |
() |
|
249 |
end; |
|
250 |
end; |
|
251 |
||
252 |
fun display_saturation filename ths = |
|
253 |
if notshowing "saturation" then () |
|
254 |
else |
|
255 |
let |
|
256 |
(*MetisDebug |
|
257 |
val () = |
|
258 |
let |
|
259 |
val problem = |
|
260 |
Tptp.mkProblem |
|
261 |
{comments = ["Saturation clause set for " ^ filename], |
|
262 |
includes = [], |
|
263 |
names = Tptp.noClauseNames, |
|
264 |
roles = Tptp.noClauseRoles, |
|
265 |
problem = {axioms = [], |
|
42102 | 266 |
conjecture = List.map Thm.clause ths}} |
39348 | 267 |
|
268 |
val mapping = |
|
269 |
Tptp.addVarSetMapping Tptp.defaultMapping |
|
270 |
(Tptp.freeVars problem) |
|
271 |
in |
|
272 |
Tptp.write |
|
273 |
{problem = problem, |
|
274 |
mapping = mapping, |
|
275 |
filename = "saturation.tptp"} |
|
276 |
end |
|
277 |
*) |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
278 |
val () = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
279 |
TextIO.print |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
280 |
("\nSZS output start Saturation for " ^ filename ^ "\n") |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
281 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
282 |
val () = app (fn th => TextIO.print (Thm.toString th ^ "\n")) ths |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
283 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
284 |
val () = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
285 |
TextIO.print |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
286 |
("SZS output end Saturation for " ^ filename ^ "\n\n") |
39348 | 287 |
in |
288 |
() |
|
289 |
end; |
|
290 |
||
291 |
fun display_status filename status = |
|
292 |
if notshowing "status" then () |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
293 |
else |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
294 |
TextIO.print ("SZS status " ^ Tptp.toStringStatus status ^ |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
295 |
" for " ^ filename ^ "\n"); |
39348 | 296 |
|
297 |
fun display_problem filename cls = |
|
298 |
let |
|
299 |
(*MetisDebug |
|
300 |
val () = |
|
301 |
let |
|
302 |
val problem = |
|
303 |
Tptp.mkProblem |
|
304 |
{comments = ["CNF clauses for " ^ filename], |
|
305 |
includes = [], |
|
306 |
names = Tptp.noClauseNames, |
|
307 |
roles = Tptp.noClauseRoles, |
|
308 |
problem = cls} |
|
309 |
||
310 |
val mapping = |
|
311 |
Tptp.addVarSetMapping Tptp.defaultMapping |
|
312 |
(Tptp.freeVars problem) |
|
313 |
||
314 |
val filename = "cnf_" ^ Int.toString (next_cnf ()) ^ ".tptp" |
|
315 |
in |
|
316 |
Tptp.write |
|
317 |
{problem = problem, |
|
318 |
mapping = mapping, |
|
319 |
filename = filename} |
|
320 |
end |
|
321 |
*) |
|
322 |
val () = display_clauses cls |
|
42102 | 323 |
|
39348 | 324 |
val () = display_size cls |
42102 | 325 |
|
39348 | 326 |
val () = display_category cls |
327 |
in |
|
328 |
() |
|
329 |
end; |
|
330 |
||
331 |
fun mkTptpFilename filename = |
|
42102 | 332 |
if isPrefix "/" filename then filename |
333 |
else |
|
334 |
case !TPTP of |
|
335 |
NONE => filename |
|
336 |
| SOME tptp => |
|
337 |
let |
|
338 |
val tptp = stripSuffix (equal #"/") tptp |
|
339 |
in |
|
340 |
tptp ^ "/" ^ filename |
|
341 |
end; |
|
39348 | 342 |
|
343 |
fun readIncludes mapping seen formulas includes = |
|
344 |
case includes of |
|
345 |
[] => formulas |
|
346 |
| inc :: includes => |
|
347 |
if StringSet.member inc seen then |
|
348 |
readIncludes mapping seen formulas includes |
|
349 |
else |
|
350 |
let |
|
351 |
val seen = StringSet.add seen inc |
|
352 |
||
353 |
val filename = mkTptpFilename inc |
|
354 |
||
355 |
val Tptp.Problem {includes = i, formulas = f, ...} = |
|
356 |
Tptp.read {filename = filename, mapping = mapping} |
|
357 |
||
358 |
val formulas = f @ formulas |
|
359 |
||
360 |
val includes = List.revAppend (i,includes) |
|
361 |
in |
|
362 |
readIncludes mapping seen formulas includes |
|
363 |
end; |
|
364 |
||
365 |
fun read mapping filename = |
|
366 |
let |
|
367 |
val problem = Tptp.read {filename = filename, mapping = mapping} |
|
368 |
||
369 |
val Tptp.Problem {comments,includes,formulas} = problem |
|
370 |
in |
|
42102 | 371 |
if List.null includes then problem |
39348 | 372 |
else |
373 |
let |
|
374 |
val seen = StringSet.empty |
|
375 |
||
376 |
val includes = rev includes |
|
377 |
||
378 |
val formulas = readIncludes mapping seen formulas includes |
|
379 |
in |
|
380 |
Tptp.Problem |
|
381 |
{comments = comments, |
|
382 |
includes = [], |
|
383 |
formulas = formulas} |
|
384 |
end |
|
385 |
end; |
|
386 |
||
387 |
val resolutionParameters = |
|
388 |
let |
|
42102 | 389 |
val {active,waiting} = Resolution.default |
39348 | 390 |
|
391 |
val waiting = |
|
392 |
let |
|
393 |
val {symbolsWeight, |
|
394 |
variablesWeight, |
|
395 |
literalsWeight, |
|
396 |
models} = waiting |
|
397 |
||
398 |
val models = |
|
399 |
case models of |
|
400 |
[{model = _, |
|
401 |
initialPerturbations, |
|
402 |
maxChecks, |
|
403 |
perturbations, |
|
404 |
weight}] => |
|
405 |
let |
|
406 |
val model = Tptp.defaultModel |
|
407 |
in |
|
408 |
[{model = model, |
|
409 |
initialPerturbations = initialPerturbations, |
|
410 |
maxChecks = maxChecks, |
|
411 |
perturbations = perturbations, |
|
412 |
weight = weight}] |
|
413 |
end |
|
414 |
| _ => raise Bug "resolutionParameters.waiting.models" |
|
415 |
in |
|
416 |
{symbolsWeight = symbolsWeight, |
|
417 |
variablesWeight = variablesWeight, |
|
418 |
literalsWeight = literalsWeight, |
|
419 |
models = models} |
|
420 |
end |
|
421 |
in |
|
422 |
{active = active, |
|
423 |
waiting = waiting} |
|
424 |
end; |
|
425 |
||
42102 | 426 |
fun resolutionLoop limit res = |
427 |
case Resolution.iterate res of |
|
428 |
Resolution.Decided dec => SOME dec |
|
429 |
| Resolution.Undecided res => |
|
430 |
if limit () then resolutionLoop limit res else NONE; |
|
431 |
||
432 |
fun refute limit {axioms,conjecture} = |
|
39348 | 433 |
let |
42102 | 434 |
val axioms = List.map Thm.axiom axioms |
435 |
and conjecture = List.map Thm.axiom conjecture |
|
436 |
||
39348 | 437 |
val problem = {axioms = axioms, conjecture = conjecture} |
42102 | 438 |
|
439 |
val res = Resolution.new resolutionParameters problem |
|
39348 | 440 |
in |
42102 | 441 |
resolutionLoop limit res |
39348 | 442 |
end; |
443 |
||
42102 | 444 |
fun refuteAll limit filename tptp probs acc = |
39348 | 445 |
case probs of |
446 |
[] => |
|
447 |
let |
|
448 |
val status = |
|
449 |
if !TEST then Tptp.UnknownStatus |
|
450 |
else if Tptp.hasFofConjecture tptp then Tptp.TheoremStatus |
|
451 |
else Tptp.UnsatisfiableStatus |
|
452 |
||
453 |
val () = display_status filename status |
|
454 |
||
455 |
val () = |
|
456 |
if !TEST then () |
|
457 |
else display_proof filename tptp (rev acc) |
|
458 |
in |
|
459 |
true |
|
460 |
end |
|
461 |
| prob :: probs => |
|
462 |
let |
|
463 |
val {subgoal,problem,sources} = prob |
|
464 |
||
465 |
val () = display_problem filename problem |
|
466 |
in |
|
42102 | 467 |
if !TEST then refuteAll limit filename tptp probs acc |
39348 | 468 |
else |
42102 | 469 |
case refute limit problem of |
470 |
SOME (Resolution.Contradiction th) => |
|
39348 | 471 |
let |
472 |
val subgoalProof = |
|
473 |
{subgoal = subgoal, |
|
474 |
sources = sources, |
|
475 |
refutation = th} |
|
476 |
||
477 |
val acc = subgoalProof :: acc |
|
478 |
in |
|
42102 | 479 |
refuteAll limit filename tptp probs acc |
39348 | 480 |
end |
42102 | 481 |
| SOME (Resolution.Satisfiable ths) => |
39348 | 482 |
let |
483 |
val status = |
|
484 |
if Tptp.hasFofConjecture tptp then |
|
485 |
Tptp.CounterSatisfiableStatus |
|
486 |
else |
|
487 |
Tptp.SatisfiableStatus |
|
488 |
||
489 |
val () = display_status filename status |
|
42102 | 490 |
|
39348 | 491 |
val () = display_saturation filename ths |
492 |
in |
|
493 |
false |
|
494 |
end |
|
42102 | 495 |
| NONE => |
496 |
let |
|
497 |
val status = Tptp.UnknownStatus |
|
498 |
||
499 |
val () = display_status filename status |
|
500 |
in |
|
501 |
false |
|
502 |
end |
|
39348 | 503 |
end; |
504 |
in |
|
42102 | 505 |
fun prove limit mapping filename = |
39348 | 506 |
let |
507 |
val () = display_sep () |
|
42102 | 508 |
|
39348 | 509 |
val () = display_name filename |
42102 | 510 |
|
39348 | 511 |
val tptp = read mapping filename |
42102 | 512 |
|
39348 | 513 |
val () = display_goal tptp |
42102 | 514 |
|
39348 | 515 |
val problems = Tptp.normalize tptp |
516 |
in |
|
42102 | 517 |
refuteAll limit filename tptp problems [] |
39348 | 518 |
end; |
42102 | 519 |
end; |
39348 | 520 |
|
42102 | 521 |
fun proveAll limit mapping filenames = |
522 |
List.all |
|
523 |
(if !QUIET then prove limit mapping |
|
524 |
else fn filename => prove limit mapping filename orelse true) |
|
525 |
filenames; |
|
39348 | 526 |
|
527 |
(* ------------------------------------------------------------------------- *) |
|
528 |
(* Top level. *) |
|
529 |
(* ------------------------------------------------------------------------- *) |
|
530 |
||
531 |
val () = |
|
532 |
let |
|
533 |
val work = processOptions () |
|
534 |
||
42102 | 535 |
val () = if List.null work then usage "no input problem files" else () |
536 |
||
537 |
val limit = newLimit () |
|
39348 | 538 |
|
539 |
val mapping = Tptp.defaultMapping |
|
540 |
||
42102 | 541 |
val success = proveAll limit mapping work |
39348 | 542 |
in |
543 |
exit {message = NONE, usage = false, success = success} |
|
544 |
end |
|
545 |
handle Error s => die (PROGRAM^" failed:\n" ^ s) |
|
546 |
| Bug s => die ("BUG found in "^PROGRAM^" program:\n" ^ s); |