1#!/sw/bin/gawk -f
2
3# Usage: sequential_eprover.awk <spec_file>
4#
5# Copyright 1998--2002 Stephan Schulz, schulz@informatik.tu-muenchen.de
6#
7# Read a specification file describing a set of parameters and a list
8# of problems, and run a sequential test of the prover over the
9# problems.
10
11
12function min(a,b)
13{
14  if(a>b)
15    {
16      return b;
17    }
18  return a;
19}
20
21function get_hostname(   pipe, tmp)
22{
23   pipe = "hostname";
24   pipe | getline tmp;
25   close(pipe);
26   return tmp;
27}
28
29function get_pid(     tmp)
30{
31#   getline tmp < "/dev/pid";
32#   close("/dev/pid");
33#   if(!tmp)
34#  {
35#     print "sequential_eprover_raw.awk: Cannot get PID ?!?" > "/dev/stderr";
36#      exit 1;
37#   }
38#   return tmp;
39   return "abba"
40}
41
42
43function expand_file(name,            pipe, tmp)
44{
45   pipe = "echo " name;
46   pipe | getline tmp;
47   close(pipe);
48   if(!tmp)
49   {
50      print "sequential_eprover_raw.awk: Cannot expand filename" > "/dev/stderr";
51      exit 1;
52   }
53   return tmp;
54}
55
56
57function file_exists(file,    test, tmp)
58{
59  test = getline tmp < file;
60  close(file);
61  if(test == -1)
62    {
63      return 0;
64    }
65  return 1;
66}
67
68
69function check_and_initialize(    tmp, job)
70{
71  if(first_job)
72    {
73      if(!executable)
74	{
75	  print "sequential_eprover_raw.awk: No executable found" > "/dev/stderr";
76	  exit 1;
77	}
78      if(!logfile)
79	{
80	  print "sequential_eprover_raw.awk: No logfile found" > "/dev/stderr";
81	  exit 1;
82	}
83      if(!problemdir)
84	{
85	  print "sequential_eprover_raw.awk: No problemdir found" > "/dev/stderr";
86	  exit 1;
87	}
88      if(!file_exists(logfile))
89	{
90	  print "Creating log file " logfile
91	  print "# " args " " auto_args > logfile;
92	  tmp = "which " executable;
93	  tmp | getline execpath;
94	  close(tmp);
95	  tmp = "ls -l " execpath;
96	  tmp | getline execdate;
97	  close(tmp);
98	  print "# " substr(execdate, 42) > logfile;
99	}
100      else
101	{
102	  print "Logfile " logfile " exists, using old results";
103
104	  processed_count = 0;
105	  while ((getline tmp < logfile) > 0)
106	  {
107	     if(match(tmp, /^[0-9A-Za-z].*\.lop/) ||
108                match(tmp, /^[0-9A-Za-z].*\.p/)||
109                match(tmp, /^[0-9A-Za-z].*\.e/)  ||
110                match(tmp, /^[0-9A-Za-z].*\.tpt/)  ||
111                match(tmp, /^[0-9A-Za-z].*\.tptp/))
112	     {
113		job = substr(tmp, RSTART, RLENGTH);
114		processed_jobs[job] = 1;
115		processed_count++;
116	     }
117	  }
118	  close(logfile);
119	  print "Found " processed_count " old results";
120	}
121      first_job = 0;
122    }
123}
124
125function host_cpu_limit_opt(limit)
126{
127   res = sprintf("--cpu-limit=%d", limit);
128
129   return res;
130}
131
132
133
134function process_result(job,    file, name, tmp,  time, status,
135			reason, generated, processed, shared_terms,
136			raw_terms, rewrite_steps, r_matches, e_matches, literals)
137{
138   file = cwd "/__prvout__" procid "_" global_hostname "__";
139   name = job;
140   time = time_limit;
141   status = "F";
142   reason = "unknown";
143   generated = 0;
144   processed = 0;
145   shared_terms = 0;
146   raw_terms = 0;
147   rewrite_steps = 0;
148   r_matches = 0;
149   e_matches = 0;
150   literals = 0;
151
152   while((getline tmp < file)>0)
153   {
154      if(index(tmp, "# No proof found!"))
155      {
156	 status = "N";
157	 reason = "success";
158      }
159      else if(index(tmp, "# Proof found!"))
160      {
161	 status = "T";
162	 reason = "success";
163      }
164      else if(index(tmp, "# Failure: Out of unprocessed clauses!"))
165      {
166	 status = "F";
167	 reason = "incomplete";
168      }
169      else if(index(tmp, "# Failure: Resource limit exceeded (memory)"))
170      {
171	 reason = "maxmem ";
172      }
173      else if(index(tmp, "# Failure: Resource limit exceeded (time)"))
174      {
175	 reason = "maxtime ";
176      }
177      else if(index(tmp, "# Failure: User resource limit exceeded"))
178      {
179	 reason = "maxres";
180      }
181      else if(index(tmp, "# Processed clauses                    :"))
182      {
183	 processed = substr(tmp, 42);
184      }
185      else if(index(tmp, "# Generated clauses                    :"))
186      {
187	 generated = substr(tmp, 42);
188      }
189      else if(index(tmp, "# Shared term nodes                    :"))
190      {
191	 shared_terms = substr(tmp, 42);
192      }
193      else if(index(tmp, "# ...corresponding unshared nodes      :"))
194      {
195	 raw_terms = substr(tmp, 42);
196      }
197      else if(index(tmp, "# Shared rewrite steps                 :"))
198      {
199	 rewrite_steps = substr(tmp, 42);
200         }
201      else if(index(tmp, "# Match attempts with oriented units   :"))
202      {
203	 r_matches = substr(tmp, 42);
204      }
205      else if(index(tmp, "# Match attempts with unoriented units :"))
206      {
207	 e_matches = substr(tmp, 42);
208      }
209      else if(index(tmp, "# Total literals in generated clauses  :"))
210      {
211	 literals = substr(tmp, 42);
212      }
213      else if(index(tmp, "# Total time"))
214      {
215	 time = substr(tmp, 30);
216      }
217   }
218   close(file);
219
220   printf("%-29s " status " %8.3f  %-10s %10d %10d %10d %10d %10d %10d %10d %10d\n",
221	  name, 0+time, reason, generated, processed, shared_terms,
222	  raw_terms, rewrite_steps, r_matches, e_matches, literals) >> logfile;
223   printf("%-29s " status " %8.3f  " reason "\n", name, 0+time);
224   system("rm " file);
225}
226
227function find_max_index(array,     i)
228{
229   for(i=1; array[i]; i++)
230   {
231   }
232   return i-1;
233}
234
235
236function shift_num_array(array, position,              limit,i)
237{
238   limit = find_max_index(array);
239
240   for(i = limit; i>=position; i--)
241   {
242      array[i+1] = array[i];
243   }
244   array[position] = "";
245
246   return limit+1;
247}
248
249
250
251function job_is_not_processed(job    ,tmp)
252{
253   match(job, /^[0-9A-Za-z].*\.lop/) || \
254   match(job, /^[0-9A-Za-z].*\.p/)||    \
255   match(job, /^[0-9A-Za-z].*\.e/)  ||  \
256   match(job, /^[0-9A-Za-z].*\.tpt/)  ||  \
257   match(job, /^[0-9A-Za-z].*\.tptp/);
258   tmp = substr(job, RSTART, RLENGTH);
259   if(tmp in processed_jobs)
260   {
261      return 0;
262   }
263   return 1;
264}
265
266BEGIN{
267   print "Initializing...";
268   print ARGV[1];
269   soft_cpu_limit = 0;
270   time_limit = 10; # Default, may be overridden
271   auto_args = "-s --print-pid --resources-info --print-statistics --tptp3-in";
272   first_job = 1;
273   executable="~/bin/eprover"
274   tmpname=ARGV[1]
275   sub(/tptp_/, "protokoll_", tmpname);
276   logfile = tmpname
277   problemdir="~/EPROVER/ONTOPROBS"
278   cwd = ENVIRON["PWD"];
279   print "Working directory is " cwd ".";
280   procid = get_pid();
281   global_hostname = get_hostname();
282   jobs = ""
283   print "PID is " procid " on host " global_hostname ".";
284}
285
286
287/^Executable:/{
288   executable = expand_file($2);
289   next;
290}
291
292/^Logfile:/{
293   logfile = expand_file($2);
294   next;
295}
296
297/^Problemdir:/{
298   problemdir = expand_file($2);
299   next;
300}
301
302/^Arguments:/{
303   args = "";
304   for(i=2; i<=NF; i++)
305   {
306      args = args " " $(i);
307   }
308   next;
309}
310
311/^Time limit:/{
312   time_limit = $3;
313   next;
314}
315
316/^Include:/{
317   split(expand_file($2), local_files);
318   local_count = ARGIND+1;
319   for(i=1; local_files[i]; i++)
320   {
321      print "Adding file " local_files[i];
322      shift_num_array(ARGV, local_count);
323      ARGV[local_count] = local_files[i];
324      local_count++;
325      ARGC++;
326   }
327   next;
328}
329
330
331# Everything else not starting with # and not empty is a job!
332/^#/{
333  print "Skipping comment";
334  next;
335}
336
337/[A-Za-z0-9]+/{
338   job = $0;
339   check_and_initialize();
340   if(job_is_not_processed(job))
341   {
342      cpu_opt = host_cpu_limit_opt(time_limit);
343      outfile = cwd "/__prvout__" procid "_" global_hostname "__";
344      command = executable " " auto_args " " cpu_opt " " args " " problemdir "/" job " > " outfile;
345
346      prefix = "/usr/bin/nice -10 ";
347      system(prefix command);
348      process_result(job);
349   }
350}
351
352
353END{
354   print "Sorting Result file";
355   srtfile = logfile ".srt";
356   system("sort " logfile " | myuniq.awk > " srtfile "; mv " srtfile " " logfile);
357   print "Test run complete";
358}
359