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