#!/usr/bin/perl


sub parse($)
{
  my $line = shift;
  my @res = ();
  $line =~ s/[\r\n]//g;
  while ($line ne "") {
    if ($line =~ s/^"(([^"]|"")*)",?//) {
      push @res, $1;
    } elsif ($line =~ s/([^,]*),?//) {
      push @res, $1;
    } 
  }
  return @res;
}

sub estimate()
{
  my $na = $last[$namedict{'num_asserts'}];
  my $nm = $last[$namedict{'num_matchings'}];
  my $nc = $last[$namedict{'num_clauses'}];

return 0.000139969988185198 * $na + 4.65006829002747E-05 * $nc + -0.00079894625041762 * $nm +
	-9.3366304251058E-11 * $na * $na + 3.10424425731029E-10 * $nc * $nc +
	6.73898783232225E-08 * $nm * $nm + 4.2429615168996;
}

$only_ok = 0;
while (1) {
  if ($ARGV[0] eq "-ok") {
    $only_ok = 1;
    shift;
  } else { last }
}


foreach my $filename (@ARGV) {
open(F,"<$filename");
@names = parse(<F>);
push @names, "estimated time";
for($i=0;$i<@names;$i++) {
  $namedict{$names[$i]} = $i;
}

@last = parse(<F>);

push @last, estimate();
my @min = @last;
my @sum = @last;
my @max = @last;
my $count = 1;

my $problems = 0;

my $other_problems = 0;
my $other = 0;

while (<F>) {
  if (/^#/) {
    /OK:/ or $other_problems++;
    $other++;
    next;
  }

  next if $only_ok && ! /OK:/;

  $count++;
  @last = parse($_);
  push @last, estimate();

  /OK:/ or $problems++;
  for($i=0;$i<@last;$i++) {
    $max[$i] = $last[$i] if ($max[$i] < $last[$i]);
    $min[$i] = $last[$i] if ($min[$i] > $last[$i]);
    $sum[$i] += $last[$i];
  }
}


for($i=0;$i<@last;$i++) {
  if ($max[$i] > 0) {
    printf "%25s: %12.2f - %12.2f - %12.2f  sum: %12.2f\n", 
    	$names[$i], $min[$i], $sum[$i]/$count, $max[$i], $sum[$i];
  } else {
    $last[$i] =~ s@/home/malekith/fx7/fx7.exe -t 300 -ax:tests/KillTc -valid -s -mqi:20@@; 
    $last[$i] =~ s@/home/malekith/fx7/fx7.exe -t 300@@; 
    $last[$i] =~ s@.*work/fx7.exe -npb -t:300 -mqi:30 -(in|)valid -s -ax:KillTc@@;
    $last[$i] =~ s@boogie/.*@@;
    $last[$i] =~ s@AUFLIA/.*@@;
    $last[$i] =~ s@ t/.*@@;

    $names[$i] =~ s/Cmd line/Cmd line ::/;

    printf "%25s: %s\n", $names[$i], $last[$i];
  }
}

printf "%25s:: %d (%d failed) + $other other ($other_problems failed)\n", "entries", $count, $problems;


$est = $sum[$namedict{'estimated time'}];
$real = $sum[$namedict{'user/sys time'}]+0.0001;
printf "Est-error: est: %d, real: %d, diff: %d, err: %.3f\n", $est, $real, $est-$real, $est/$real;
printf "SUMMARY: %6d est +%-4d/%-4d errs " . $last[$namedict{'Cmd line'}] . "\n", $est, $other_problems, $problems;
print "-------------------------------::-------------------------------\n";

}