1#!/sw/bin/gawk -f 2 3# Usage: filter_results.awk <filter_file> [<from_file>] 4# 5# Copyright 1998, 2016 Stephan Schulz, schulz@eprover.org 6# 7# Read file of TPTP problem names and a second file, return all lines 8# from the second file in which a name from the first file 9# occurs. Also pass through comments. 10# 11 12BEGIN{ 13 if(!ARGV[1]) 14 { 15 print "Usage: filter_results.awk <filter_file> [<from_file>]"; 16 exit 1; 17 } 18 if(!ARGV[2]) 19 { 20 ARGV[2] = "-"; 21 ARGC++; 22 } 23} 24 25function get_basename(name, tmp) 26{ 27 if(!match(name, /\.[a-z]*( |$)/)) 28 { 29 print "filter_results.awk: Cannot find problem basename in '" name "'"; 30 } 31 return substr(name, 0 , RSTART-1); 32} 33 34 35# Skipping comments 36 37/^#/{ 38 if(ARGIND==2) 39 { 40 print 41 } 42 next; 43} 44 45# Process all non-empty lines 46 47/[A-Za-z0-9]+/{ 48 if(ARGIND == 1) 49 { 50 names[$1] = 1; 51 } 52 else 53 { 54 if(names[$1]) 55 { 56 print; 57 # delete names[get_basename($0)]; 58 } 59 } 60} 61 62#END{ 63# print "Remaining:"; 64# for(i in names) 65# { 66# print i; 67# } 68#} 69