|
1 (* ========================================================================= *) |
|
2 (* METIS FIRST ORDER PROVER *) |
|
3 (* *) |
|
4 (* Copyright (c) 2001-2007 Joe Hurd *) |
|
5 (* *) |
|
6 (* Metis is free software; you can redistribute it and/or modify *) |
|
7 (* it under the terms of the GNU General Public License as published by *) |
|
8 (* the Free Software Foundation; either version 2 of the License, or *) |
|
9 (* (at your option) any later version. *) |
|
10 (* *) |
|
11 (* Metis is distributed in the hope that it will be useful, *) |
|
12 (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) |
|
13 (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) |
|
14 (* GNU General Public License for more details. *) |
|
15 (* *) |
|
16 (* You should have received a copy of the GNU General Public License *) |
|
17 (* along with Metis; if not, write to the Free Software *) |
|
18 (* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) |
|
19 (* ========================================================================= *) |
|
20 |
|
21 open Useful; |
|
22 |
|
23 (* ------------------------------------------------------------------------- *) |
|
24 (* The program name. *) |
|
25 (* ------------------------------------------------------------------------- *) |
|
26 |
|
27 val PROGRAM = "metis"; |
|
28 |
|
29 (* ------------------------------------------------------------------------- *) |
|
30 (* Program options. *) |
|
31 (* ------------------------------------------------------------------------- *) |
|
32 |
|
33 val QUIET = ref false; |
|
34 |
|
35 val TEST = ref false; |
|
36 |
|
37 val ITEMS = ["name","goal","clauses","size","category","proof","saturated"]; |
|
38 |
|
39 val show_items = map (fn s => (s, ref false)) ITEMS; |
|
40 |
|
41 fun show_ref s = |
|
42 case List.find (equal s o fst) show_items of |
|
43 NONE => raise Bug ("item " ^ s ^ " not found") |
|
44 | SOME (_,r) => r; |
|
45 |
|
46 fun showing s = not (!QUIET) andalso (s = "status" orelse !(show_ref s)); |
|
47 |
|
48 fun notshowing s = not (showing s); |
|
49 |
|
50 fun showing_any () = List.exists showing ITEMS; |
|
51 |
|
52 fun notshowing_any () = not (showing_any ()); |
|
53 |
|
54 fun show s = case show_ref s of r => r := true; |
|
55 |
|
56 fun hide s = case show_ref s of r => r := false; |
|
57 |
|
58 local |
|
59 open Useful Options; |
|
60 in |
|
61 val specialOptions = |
|
62 [{switches = ["--show"], arguments = ["ITEM"], |
|
63 description = "show ITEM (see below for list)", |
|
64 processor = |
|
65 beginOpt (enumOpt ITEMS endOpt) (fn _ => fn s => show s)}, |
|
66 {switches = ["--hide"], arguments = ["ITEM"], |
|
67 description = "hide ITEM (see below for list)", |
|
68 processor = |
|
69 beginOpt (enumOpt ITEMS endOpt) (fn _ => fn s => hide s)}, |
|
70 {switches = ["-q","--quiet"], arguments = [], |
|
71 description = "Run quietly; indicate provability with return value", |
|
72 processor = beginOpt endOpt (fn _ => QUIET := true)}, |
|
73 {switches = ["--test"], arguments = [], |
|
74 description = "Skip the proof search for the input problems", |
|
75 processor = beginOpt endOpt (fn _ => TEST := true)}]; |
|
76 end; |
|
77 |
|
78 val VERSION = "2.0"; |
|
79 |
|
80 val versionString = PROGRAM^" version "^VERSION^" (release 20070609)"^"\n"; |
|
81 |
|
82 val programOptions = |
|
83 {name = PROGRAM, |
|
84 version = versionString, |
|
85 header = "usage: "^PROGRAM^" [option ...] problem.tptp ...\n" ^ |
|
86 "Proves the input TPTP problem files.\n", |
|
87 footer = "Possible ITEMs are {" ^ join "," ITEMS ^ "}.\n" ^ |
|
88 "Problems can be read from standard input using the " ^ |
|
89 "special - filename.\n", |
|
90 options = specialOptions @ Options.basicOptions}; |
|
91 |
|
92 fun exit x : unit = Options.exit programOptions x; |
|
93 fun succeed () = Options.succeed programOptions; |
|
94 fun fail mesg = Options.fail programOptions mesg; |
|
95 fun usage mesg = Options.usage programOptions mesg; |
|
96 |
|
97 val (opts,work) = |
|
98 Options.processOptions programOptions (CommandLine.arguments ()); |
|
99 |
|
100 val () = if null work then usage "no input problem files" else (); |
|
101 |
|
102 (* ------------------------------------------------------------------------- *) |
|
103 (* The core application. *) |
|
104 (* ------------------------------------------------------------------------- *) |
|
105 |
|
106 local |
|
107 fun display_sep () = |
|
108 if notshowing_any () then () |
|
109 else print (nChars #"-" (!Parser.lineLength) ^ "\n"); |
|
110 |
|
111 fun display_name filename = |
|
112 if notshowing "name" then () |
|
113 else print ("Problem: " ^ filename ^ "\n\n"); |
|
114 |
|
115 fun display_goal goal = |
|
116 if notshowing "goal" then () |
|
117 else print ("Goal:\n" ^ Formula.toString goal ^ "\n\n"); |
|
118 |
|
119 fun display_clauses cls = |
|
120 if notshowing "clauses" then () |
|
121 else print ("Clauses:\n" ^ Problem.toString cls ^ "\n\n"); |
|
122 |
|
123 fun display_size cls = |
|
124 if notshowing "size" then () |
|
125 else |
|
126 let |
|
127 fun plural 1 s = "1 " ^ s |
|
128 | plural n s = Int.toString n ^ " " ^ s ^ "s" |
|
129 |
|
130 val {clauses,literals,symbols,typedSymbols} = Problem.size cls |
|
131 in |
|
132 print |
|
133 ("Size: " ^ |
|
134 plural clauses "clause" ^ ", " ^ |
|
135 plural literals "literal" ^ ", " ^ |
|
136 plural symbols "symbol" ^ ", " ^ |
|
137 plural typedSymbols "typed symbol" ^ ".\n\n") |
|
138 end; |
|
139 |
|
140 fun display_category cls = |
|
141 if notshowing "category" then () |
|
142 else |
|
143 let |
|
144 val cat = Problem.categorize cls |
|
145 in |
|
146 print ("Category: " ^ Problem.categoryToString cat ^ ".\n\n") |
|
147 end; |
|
148 |
|
149 fun display_proof filename th = |
|
150 if notshowing "proof" then () |
|
151 else |
|
152 (print ("SZS output start CNFRefutation for " ^ filename ^ "\n"); |
|
153 print (Proof.toString (Proof.proof th)); |
|
154 print ("SZS output end CNFRefutation for " ^ filename ^ "\n\n")); |
|
155 |
|
156 fun display_saturated filename ths = |
|
157 if notshowing "saturated" then () |
|
158 else |
|
159 (print ("SZS output start Saturated for " ^ filename ^ "\n"); |
|
160 app (fn th => print (Thm.toString th ^ "\n")) ths; |
|
161 print ("SZS output end Saturated for " ^ filename ^ "\n\n")); |
|
162 |
|
163 fun display_result filename result = |
|
164 case result of |
|
165 Resolution.Contradiction th => display_proof filename th |
|
166 | Resolution.Satisfiable ths => display_saturated filename ths; |
|
167 |
|
168 fun display_status filename status = |
|
169 if notshowing "status" then () |
|
170 else print ("SZS status " ^ status ^ " for " ^ filename ^ "\n"); |
|
171 |
|
172 fun display_problem filename cls = |
|
173 let |
|
174 (*DEBUG |
|
175 val () = Tptp.write {filename = "cnf.tptp"} (Tptp.fromProblem cls) |
|
176 *) |
|
177 val () = display_clauses cls |
|
178 val () = display_size cls |
|
179 val () = display_category cls |
|
180 in |
|
181 () |
|
182 end; |
|
183 |
|
184 fun display_problems filename problems = |
|
185 List.app (display_problem filename) problems; |
|
186 |
|
187 fun refute cls = |
|
188 Resolution.loop (Resolution.new Resolution.default (map Thm.axiom cls)); |
|
189 |
|
190 fun refutable filename cls = |
|
191 let |
|
192 val () = display_problem filename cls |
|
193 in |
|
194 case refute cls of |
|
195 Resolution.Contradiction th => (display_proof filename th; true) |
|
196 | Resolution.Satisfiable ths => (display_saturated filename ths; false) |
|
197 end; |
|
198 in |
|
199 fun prove filename = |
|
200 let |
|
201 val () = display_sep () |
|
202 val () = display_name filename |
|
203 val tptp = Tptp.read {filename = filename} |
|
204 in |
|
205 case Tptp.toGoal tptp of |
|
206 Tptp.Cnf prob => |
|
207 let |
|
208 val () = display_problem filename prob |
|
209 in |
|
210 if !TEST then |
|
211 (display_status filename "Unknown"; |
|
212 true) |
|
213 else |
|
214 case refute prob of |
|
215 Resolution.Contradiction th => |
|
216 (display_status filename "Unsatisfiable"; |
|
217 if showing "proof" then print "\n" else (); |
|
218 display_proof filename th; |
|
219 true) |
|
220 | Resolution.Satisfiable ths => |
|
221 (display_status filename "Satisfiable"; |
|
222 if showing "saturated" then print "\n" else (); |
|
223 display_saturated filename ths; |
|
224 false) |
|
225 end |
|
226 | Tptp.Fof goal => |
|
227 let |
|
228 val () = display_goal goal |
|
229 val problems = Problem.fromGoal goal |
|
230 val result = |
|
231 if !TEST then (display_problems filename problems; true) |
|
232 else List.all (refutable filename) problems |
|
233 val status = |
|
234 if !TEST then "Unknown" |
|
235 else if Tptp.hasConjecture tptp then |
|
236 if result then "Theorem" else "CounterSatisfiable" |
|
237 else |
|
238 if result then "Unsatisfiable" else "Satisfiable" |
|
239 val () = display_status filename status |
|
240 in |
|
241 result |
|
242 end |
|
243 end; |
|
244 end; |
|
245 |
|
246 (* ------------------------------------------------------------------------- *) |
|
247 (* Top level. *) |
|
248 (* ------------------------------------------------------------------------- *) |
|
249 |
|
250 val () = |
|
251 let |
|
252 (*DEBUG |
|
253 val () = print "Running in DEBUG mode.\n" |
|
254 *) |
|
255 val success = List.all prove work |
|
256 val return = not (!QUIET) orelse success |
|
257 in |
|
258 exit {message = NONE, usage = false, success = return} |
|
259 end |
|
260 handle Error s => die (PROGRAM^" failed:\n" ^ s) |
|
261 | Bug s => die ("BUG found in "^PROGRAM^" program:\n" ^ s); |