1#!/sw/bin/gawk -f
2
3# Usage: sequential_eground.awk <spec_file>
4#
5# Copyright 1998,2001 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 grounder 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_eground.awk: Cannot get PID ?!?" > "/dev/stderr";
36      exit 1;
37   }
38   return tmp;
39}
40
41function expand_file(name,            pipe, tmp)
42{
43   pipe = "echo " name;
44   pipe | getline tmp;
45   close(pipe);
46   if(!tmp)
47   {
48      print "sequential_eground.awk: Cannot expand filename" > "/dev/stderr";
49      exit 1;
50   }
51   return tmp;
52}
53
54
55function file_exists(file,    test, tmp)
56{
57  test = getline tmp < file;
58  close(file);
59  if(test == -1)
60    {
61      return 0;
62    }
63  return 1;
64}
65
66
67function check_and_initialize(    tmp, job)
68{
69  if(first_job)
70    {
71      if(!executable)
72	{
73	  print "sequential_eground.awk: No executable found" > "/dev/stderr";
74	  exit 1;
75	}
76      if(!logfile)
77	{
78	  print "sequential_eground.awk: No logfile found" > "/dev/stderr";
79	  exit 1;
80	}
81      if(!problemdir)
82	{
83	  print "sequential_eground.awk: No problemdir found" > "/dev/stderr";
84	  exit 1;
85	}
86      if(!file_exists(logfile))
87	{
88	  print "Creating log file " logfile
89	  print "# " args " " auto_args > logfile;
90	  tmp = "which " executable;
91	  tmp | getline execpath;
92	  close(tmp);
93	  tmp = "ls -l " execpath;
94	  tmp | getline execdate;
95	  close(tmp);
96	  print "# " substr(execdate, 42) > logfile;
97	}
98      else
99	{
100	  print "Logfile " logfile " exists, using old results";
101
102	  processed_count = 0;
103	  while ((getline tmp < logfile) > 0)
104	  {
105	     if(match(tmp, /^[A-Za-z].*\.lop/)||
106		match(tmp, /^[A-Za-z].*\.p/)||
107		match(tmp, /^[A-Za-z].*\.e/)||
108		match(tmp, /^[A-Za-z].*\.tptp/))
109	     {
110		job = substr(tmp, RSTART, RLENGTH);
111		processed_jobs[job] = 1;
112		processed_count++;
113	     }
114	  }
115	  close(logfile);
116	  print "Found " processed_count " old results";
117	}
118      first_job = 0;
119    }
120}
121
122
123
124function process_result(job,    file, tmp,  time, status, reason, name)
125{
126   time = time_limit;
127   status = "F";
128   reason = "unknown";
129   clauses = 0;
130   literals = 0;
131   file = cwd "/__prvout__" procid "_" global_hostname "__";
132   name = job;
133
134   while((getline tmp < file)>0)
135   {
136      if(index(tmp, "# Success!"))
137      {
138	 status = "S";
139	 reason = "success";
140      }
141      else if(index(tmp, "# Failure: Resource limit exceeded (memory)"))
142      {
143	 reason = "maxmem ";
144      }
145      else if(index(tmp, "# Failure: Resource limit exceeded (time)"))
146      {
147	 reason = "maxtime ";
148      }
149      else if(index(tmp, "# Total time"))
150      {
151	 time = substr(tmp, 30);
152      }
153      else if(index(tmp, "# Generated clauses                    :"))
154      {
155	 clauses = substr(tmp, 42);
156      }
157      else if(index(tmp, "# Generated literals                   :"))
158      {
159	 literals = substr(tmp, 42);
160      }
161
162   }
163   close(file);
164   printf("%-29s %s %8.3f %8s %10d %10d\n", name, status, 0+time,
165	  reason, clauses, literals) >> logfile;
166   printf("%-29s %s %8.3f %8s %10d %10d\n", name, status, 0+time,
167	  reason, clauses, literals);
168   system("rm " file);
169}
170
171function find_max_index(array,     i)
172{
173   for(i=1; array[i]; i++)
174   {
175   }
176   return i-1;
177}
178
179
180function shift_num_array(array, position,              limit,i)
181{
182   limit = find_max_index(array);
183
184   for(i = limit; i>=position; i--)
185   {
186      array[i+1] = array[i];
187   }
188   array[position] = "";
189
190   return limit+1;
191}
192
193
194
195function job_is_not_processed(job    ,tmp)
196{
197   match(job, /^[A-Za-z]+.*\.lop/) || match(job, /^[A-Za-z]+.*\.p/)|| match(job, /^[A-Za-z]+.*\.e/)  || match(job, /^[A-Za-z].*\.tptp/);
198   tmp = substr(job, RSTART, RLENGTH);
199   if(tmp in processed_jobs)
200   {
201      return 0;
202   }
203   return 1;
204}
205
206function host_is_reserved(         pipe, tmp)
207{
208   if(global_checkreservation)
209   {
210      return file_exists(global_checkreservation);
211   }
212   return 0;
213}
214
215BEGIN{
216   print "Initializing...";
217   time_limit = 10; # Default, may be overridden
218   auto_args = "--suppress-result --print-statistics -R"
219   first_job = 1;
220   cwd = ENVIRON["PWD"];
221   print "Working directory is " cwd ".";
222   procid = get_pid();
223   global_hostname = get_hostname();
224
225   reserved_hosts["sunjessen56"] = "schulz";
226   reserved_hosts["sunjessen48"] = "letz";
227   reserved_hosts["sunjessen51"] = "stenzg";
228   reserved_hosts["sunjessen57"] = "jobmann";
229   if(global_hostname in reserved_hosts)
230   {
231      global_checkreservation = "/home/" \
232	 reserved_hosts[global_hostname] \
233	 "/HOST_RESERVED_" global_hostname;
234   }
235
236   print "PID is " procid " on host " global_hostname ".";
237}
238
239
240/^Executable:/{
241   executable = expand_file($2);
242   next;
243}
244
245/^Logfile:/{
246   logfile = expand_file($2);
247   next;
248}
249
250/^Problemdir:/{
251   problemdir = expand_file($2);
252   next;
253}
254
255/^Arguments:/{
256   args = "";
257   for(i=2; i<=NF; i++)
258   {
259      args = args " " $(i);
260   }
261  next;
262}
263
264/^Time limit:/{
265   time_limit = $3;
266   next;
267}
268
269/^Include:/{
270   split(expand_file($2), local_files);
271   local_count = ARGIND+1;
272   for(i=1; local_files[i]; i++)
273   {
274      print "Adding file " local_files[i];
275      shift_num_array(ARGV, local_count);
276      ARGV[local_count] = local_files[i];
277      local_count++;
278      ARGC++;
279   }
280   next;
281}
282
283
284# Everything else not starting with # and not empty is a job!
285/^#/{
286  print "Skipping comment";
287  next;
288}
289
290/[A-Za-z0-9]+/{
291   while(host_is_reserved())
292   {
293      print "Waiting for reservation to expire!";
294      system("sleep 600")
295   }
296   job = $0;
297   check_and_initialize();
298   if(job_is_not_processed(job))
299   {
300      outfile = cwd "/__prvout__" procid "_" global_hostname "__";
301      command = executable " " auto_args " --cpu-limit=" time_limit " " args " " problemdir "/" job " > " outfile;
302
303      prefix = "/usr/bin/nice -10 ";
304      # print prefix command
305      system(prefix command);
306      process_result(job);
307   }
308}
309
310
311END{
312   print "Sorting Result file";
313   srtfile = logfile ".srt";
314   system("sort " logfile " | myuniq.awk > " srtfile "; mv " srtfile " " logfile);
315   print "Test run complete";
316}
317
318