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