1 /*-----------------------------------------------------------------------
2
3 File : e_ltb_runner.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Hack for the LTB category of CASC-2012 - parse an LTB spec file, and
10 run E on the various problems.
11
12 Copyright 2010-2012 by the author.
13 This code is released under the GNU General Public Licence and
14 the GNU Lesser General Public License.
15 See the file COPYING in the main E directory for details..
16 Run "eprover -h" for contact information.
17
18 Changes
19
20 <1> Mon Jun 28 02:15:05 CEST 2010
21 New
22
23 -----------------------------------------------------------------------*/
24
25 #include <clb_defines.h>
26 #include <cio_commandline.h>
27 #include <cio_output.h>
28 #include <ccl_relevance.h>
29 #include <cio_signals.h>
30 #include <ccl_formulafunc.h>
31 #include <cco_batch_spec.h>
32 #include <ccl_sine.h>
33 #include <e_version.h>
34
35
36 /*---------------------------------------------------------------------*/
37 /* Data types */
38 /*---------------------------------------------------------------------*/
39
40 #define NAME "e_ltb_runner"
41
42 typedef enum
43 {
44 OPT_NOOPT=0,
45 OPT_HELP,
46 OPT_VERSION,
47 OPT_VERBOSE,
48 OPT_OUTPUT,
49 OPT_OUTDIR,
50 OPT_INTERACTIVE,
51 OPT_PRINT_STATISTICS,
52 OPT_SILENT,
53 OPT_OUTPUTLEVEL,
54 OPT_GLOBAL_WTCLIMIT,
55 OPT_DUMMY
56 }OptionCodes;
57
58
59
60 /*---------------------------------------------------------------------*/
61 /* Global Variables */
62 /*---------------------------------------------------------------------*/
63
64
65 OptCell opts[] =
66 {
67 {OPT_HELP,
68 'h', "help",
69 NoArg, NULL,
70 "Print a short description of program usage and options."},
71
72 {OPT_VERSION,
73 'V', "version",
74 NoArg, NULL,
75 "Print the version number of the prover. Please include this"
76 " with all bug reports (if any)."},
77
78 {OPT_VERBOSE,
79 'v', "verbose",
80 OptArg, "1",
81 "Verbose comments on the progress of the program. This differs "
82 "from the output level (below) in that technical information is "
83 "printed to stderr, while the output level determines which "
84 "logical manipulations of the clauses are printed to stdout."},
85
86 {OPT_OUTPUT,
87 'o', "output-file",
88 ReqArg, NULL,
89 "Redirect output into the named file."},
90
91 {OPT_OUTDIR,
92 'd', "output-dir",
93 ReqArg, NULL,
94 "Directory for individual problem output files. Default is the current"
95 " working directory."},
96
97 {OPT_INTERACTIVE,
98 'i', "interactive",
99 NoArg, NULL,
100 "For each batch file, enter interactive mode after processing "
101 "batch the batch problems. Interactive mode allows the processing "
102 "of additional jobs with respect to the loaded axioms set. Jobs "
103 "are entered via stdin and print to stdout."},
104
105 {OPT_SILENT,
106 's', "silent",
107 NoArg, NULL,
108 "Equivalent to --output-level=0."},
109
110 {OPT_OUTPUTLEVEL,
111 'l', "output-level",
112 ReqArg, NULL,
113 "Select an output level, greater values imply more verbose "
114 "output. Level 0 produces "
115 "nearly no output, level 1 will output each clause as it is "
116 "processed, level 2 will output generating inferences, "
117 "level 3 will give a full protocol including rewrite steps and "
118 "level 4 will include some internal clause renamings. Levels >= 2"
119 " also imply PCL2 or TSTP formats (which can be post-processed"
120 " with suitable tools)."},
121
122 {OPT_GLOBAL_WTCLIMIT,
123 'w', "wtc-limit",
124 ReqArg, NULL,
125 "Set the global wall-clock limit for each batch (if any)."},
126
127 {OPT_NOOPT,
128 '\0', NULL,
129 NoArg, NULL,
130 NULL}
131 };
132
133 char *outname = NULL;
134 char *outdir = NULL;
135 long total_wtc_limit = 0;
136 bool interactive = false;
137
138 /*---------------------------------------------------------------------*/
139 /* Forward Declarations */
140 /*---------------------------------------------------------------------*/
141
142 CLState_p process_options(int argc, char* argv[]);
143 void print_help(FILE* out);
144
145 /*---------------------------------------------------------------------*/
146 /* Internal Functions */
147 /*---------------------------------------------------------------------*/
148
main(int argc,char * argv[])149 int main(int argc, char* argv[])
150 {
151 CLState_p state;
152 Scanner_p in;
153 BatchSpec_p spec;
154 StructFOFSpec_p ctrl;
155 char *prover = "eprover";
156 char *category = NULL;
157 char *train_dir = NULL;
158 long now, start, res;
159
160 assert(argv[0]);
161
162 InitIO(NAME);
163 DocOutputFormat = tstp_format;
164 OutputFormat = TSTPFormat;
165
166 state = process_options(argc, argv);
167
168 OpenGlobalOut(outname);
169
170 if((state->argc < 1) || (state->argc > 2))
171 {
172 Error("Usage: e_ltb_runner <spec> [<path-to-eprover>] \n",
173 USAGE_ERROR);
174 }
175 if(state->argc >= 2)
176 {
177 prover = state->argv[1];
178 }
179
180 in = CreateScanner(StreamTypeFile, state->argv[0], true, NULL);
181 ScannerSetFormat(in, TSTPFormat);
182
183 AcceptDottedId(in, "division.category");
184 category = ParseDottedId(in);
185
186 if(TestInpId(in, "division"))
187 {
188 AcceptDottedId(in, "division.category.training_directory");
189 train_dir = ParseContinous(in);
190 }
191
192 while(!TestInpTok(in, NoToken))
193 {
194 start = GetSecTime();
195 spec = BatchSpecParse(in, prover, category, train_dir, TSTPFormat);
196
197 /* BatchSpecPrint(GlobalOut, spec); */
198
199 if(total_wtc_limit && !spec->total_wtc_limit)
200 {
201 spec->total_wtc_limit = total_wtc_limit;
202 }
203 if(spec->per_prob_limit<=0 && total_wtc_limit<=0)
204 {
205 Error("Either the per-problem time limit or the global "
206 "time limit must be set to a value > 0", USAGE_ERROR);
207 }
208 /* BatchSpecPrint(stdout, spec); */
209 ctrl = StructFOFSpecAlloc();
210 BatchStructFOFSpecInit(spec, ctrl);
211 now = GetSecTime();
212 res = BatchProcessProblems(spec, ctrl,
213 MAX(0,total_wtc_limit-(now-start)),
214 outdir);
215 now = GetSecTime();
216 fprintf(GlobalOut, "\n\n# == WCT: %4lds, Solved: %4ld/%4ld ==\n",
217 now-start, res, BatchSpecProblemNo(spec));
218 fprintf(GlobalOut, "# =============== Batch done ===========\n\n");
219 if(interactive)
220 {
221 BatchProcessInteractive(spec, ctrl, stdout);
222 }
223 StructFOFSpecFree(ctrl);
224 BatchSpecFree(spec);
225 }
226 DestroyScanner(in);
227
228 if(category)
229 {
230 FREE(category);
231 }
232 if(train_dir)
233 {
234 FREE(train_dir);
235 }
236
237 CLStateFree(state);
238
239 OutClose(GlobalOut);
240 ExitIO();
241 #ifdef CLB_MEMORY_DEBUG
242 MemFlushFreeList();
243 MemDebugPrintStats(stdout);
244 #endif
245
246 return 0;
247 }
248
249
250 /*-----------------------------------------------------------------------
251 //
252 // Function: process_options()
253 //
254 // Read and process the command line option, return (the pointer to)
255 // a CLState object containing the remaining arguments.
256 //
257 // Global Variables: opts, Verbose, TBPrintInternalInfo
258 //
259 // Side Effects : Sets variables, may terminate with program
260 // description if option -h or --help was present
261 //
262 /----------------------------------------------------------------------*/
263
process_options(int argc,char * argv[])264 CLState_p process_options(int argc, char* argv[])
265 {
266 Opt_p handle;
267 CLState_p state;
268 char* arg;
269
270 state = CLStateAlloc(argc,argv);
271
272 while((handle = CLStateGetOpt(state, &arg, opts)))
273 {
274 switch(handle->option_code)
275 {
276 case OPT_VERBOSE:
277 Verbose = CLStateGetIntArg(handle, arg);
278 break;
279 case OPT_HELP:
280 print_help(stdout);
281 exit(NO_ERROR);
282 case OPT_VERSION:
283 fprintf(stdout, NAME " " VERSION " " E_NICKNAME "\n");
284 exit(NO_ERROR);
285 case OPT_OUTPUT:
286 outname = arg;
287 break;
288 case OPT_OUTDIR:
289 outdir = arg;
290 break;
291 case OPT_INTERACTIVE:
292 interactive = true;
293 break;
294 case OPT_SILENT:
295 OutputLevel = 0;
296 break;
297 case OPT_OUTPUTLEVEL:
298 OutputLevel = CLStateGetIntArg(handle, arg);
299 break;
300 case OPT_GLOBAL_WTCLIMIT:
301 total_wtc_limit = CLStateGetIntArg(handle, arg);
302 break;
303 default:
304 assert(false && "Unknown option");
305 break;
306 }
307 }
308 return state;
309 }
310
print_help(FILE * out)311 void print_help(FILE* out)
312 {
313 fprintf(out, "\n"
314 NAME " " VERSION " \"" E_NICKNAME "\"\n\
315 \n\
316 Usage: " NAME " [options] [files]\n\
317 \n\
318 Read a CASC 24 LTB batch specification file and process it.\n\
319 \n");
320 PrintOptions(stdout, opts, "Options:\n\n");
321 fprintf(out, "\n\n" E_FOOTER);
322 }
323
324
325 /*---------------------------------------------------------------------*/
326 /* End of File */
327 /*---------------------------------------------------------------------*/
328