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