#!/bin/awk -f

# units = 1 for secs., 60 for mins., 3600 for hrs., etc.; default 1.
#
# Input format is:
#    first line is "SOLVER <mysolver> <othersolver>"
#    remaining lines are "<benchname> <mytime> <othertime>"
#        where <*time> = Inf for timeout or failure.
#
# Output format is:
#    first line is "<mysolver> <othersolver>"
#    remaining lines, except last, are "<myscore> <benchname>"
#        where <myscore> is  " 0" or " 1".
#    last line is "<my_cum_score> <num_benchs> <significance>"
#        where <significance> is one or more fields, to be explained.
# Only the last output line has three or more fields.

BEGIN {
	if (units == "") units = 1;
	if (noise == "") noise = 60 / units;
	}

NR == 1 {
	mysolver = $2;
	othersolver = $3;
	cumscore = 0;
	nbench = 0;
	nties = 0;
	print mysolver, othersolver;
	next;
	}

tolower($2) == "inf" {
	benchname = $1;
	myscore = 0;
	printf "%2d %s\n",  myscore, benchname;
	cumscore += myscore;
	nbench ++;
	next;
	}

{
	benchname = $1;
	myscore = 1;
	printf "%2d %s\n",  myscore, benchname;
	cumscore += myscore;
	nbench ++;
	next;
	}

END {
	print cumscore, nbench, 0, 0, 0, mysolver;
	}