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