#!/usr/bin/perl

%d1 = ();
%d2 = ();

$min = 10000;
$max = 0;

$no_plot = 0;
$png = 0;
$eps = 0;
$unsat = 0;
if ($ARGV[0] eq "-u") {
  shift @ARGV;
  $unsat = 1;
}

if ($ARGV[0] eq "-p") {
  shift @ARGV;
  $png = 1;
}

if ($ARGV[0] eq "-n") {
  shift @ARGV;
  $no_plot = 1;
}

if ($ARGV[0] eq "-e") {
  shift @ARGV;
  $eps = 1;
}

sub filename($) {
  $f = shift;
  -f $f and return $f;
  -f "logs/$f" and return "logs/$f";
  if ($f eq ".") {
    $f = `ls -1 logs/200* 200* | tail -1`;
    chomp $f;
    return "$f";
  }
  return $f;
}

sub read_file {
  $f1 = filename(shift);
  open(F,"< $f1") || die "cannot open $f1";
  my %d1 = ();
  $ok = 1;
  while(<F>) {
    if ($unsat) {
    /SAT=True/ and $ok = 0;
    }
    /SAT=False/ and $ok = 1;
    /TIMEOUT/ and $ok = 1;
    
    my ($file,$time);
    if (/running time \[(.*)]: ([\d\.]+)/ and $ok) {
      $file = $1;
      $time = $2;
    } elsif (/([^,]+),[^,]+,([\d.]+),[\d.]*(.*)/) {
      $file = $1;
      $time = $2;
      $rest = $3;
      $rest =~ /OK:/ or $time = -2;
      $rest =~ /TIMEOUT/ and $time = -1;
      /[ ,]-o:(\S+)/ and $d1{'opts'} = $1;
    } else { next; }

    
    $d1{$file} = $time;
    if ($time > $max) { $max = $time; }
    if ($time > 0 && $time < $min) { $min = $time; }

    # $_ = <F>;
    # /inst: (\d+)/ or die;
    # /\(\+ (\d+)/ or die;
    #$d1{$file} = $1 / 100.0;
  }
  return %d1;
}

%d1 = read_file($ARGV[0]);
%d2 = read_file($ARGV[1]);

$o1 = $d1{'opts'};
$o2 = $d2{'opts'};
$d1{'opts'} = undef;
$d2{'opts'} = undef;

$timeout = $max * 1.5;
$wrong = $max * 1.8;

sub gettime($)
{
  my $t = shift;
  return $wrong if ($t == -2);
  return $timeout if ($t == -1);
  return $t;
}

sub xfmt($)
{
  my $t = shift;

  if ($t == -2) {
    return "  WRONG";
  }

  if($t == -1) {
    return "   TIME"
  }

  return sprintf("%7.2f", $t);
}

$f1 = $ARGV[0];
$f2 = $ARGV[1];

open(F,"> plotdata");
open(H,"| cat");
$s1 = 0;
$s2 = 0;

sub xcmp($$)
{
  my $k1 = shift;
  my $k2 = shift;
  $k1 = gettime($d1{$k1}) + gettime($d2{$k1});
  $k2 = gettime($d1{$k2}) + gettime($d2{$k2});
  return $k1 <=> $k2;
}

sub min($$)
{
  my ($a,$b) = @_; if ($a < $b) { return $a ; } else { return $b; }
}

$to1 = 0;
$to2 = 0;
$wrong1 = 0;
$wrong2 = 0;
$tr1 = 0;
$tr2 = 0;

foreach my $k (sort xcmp (keys %d1)) {
  if ($d2{$k}) {
    my $t1 = gettime($d1{$k});
    my $t2 = gettime($d2{$k});

    $to1++ if ($d1{$k} == -1);
    $to2++ if ($d2{$k} == -1);
    $wrong1++ if ($d1{$k} == -2);
    $wrong2++ if ($d2{$k} == -2);
    if ($d1{$k} > 0 && $d2{$k} > 0) {
      $tr1 += $t1;
      $tr2 += $t2;
    }

    print F $t1 . " " . $t2 . "\n";
    $mark = "";
    $t1 = min($t1,$timeout);
    $t2 = min($t2,$timeout);
    $mark = "0;0";
    if (abs($t1 - $t2) > 0.5) {
      if ($t1 * 1.4 < $t2) {
        $mark = "31;1";
      }
      elsif ($t1 * 1.1 < $t2) {
        $mark = "0;31";
      }
      elsif ($t1 / 1.4 > $t2) {
        $mark = "32;1";
      }
      elsif ($t1 / 1.1 > $t2) {
        $mark = "0;32";
      }
    }
    $beg = "\e[${mark}m";
    $end = "\e[0m";
    $s1 += $t1;
    $s2 += $t2;
    $t2++ if($t2==0);
    printf H "$beg%s %s %5.2f   %s$end\n", xfmt($d1{$k}), xfmt($d2{$k}), $t1/$t2, $k;
  }
}
close(H);
$s2++ if($s2==0);
printf  "%7d %7d %5.2f   TIMEOUTS\n", $to1, $to2, $to1*1.0/($to2==0?1:$to2);
printf  "%7d %7d %5.2f   WRONGS\n", $wrong1, $wrong2, $wrong1*1.0/($wrong2==0?1:$wrong2);
printf  "%s %s %5.2f   TOTAL w/o TO/WR\n", xfmt($tr1), xfmt($tr2), $tr1/($tr2==0?1:$tr2);
printf  "%s %s %5.2f   TOTAL\n", xfmt($s1), xfmt($s2), $s1/$s2;
printf  "%s vs %s\n", $o1, $o2;


if (!$no_plot) {
$gain = sprintf ("(speedup %.2f)", $s1 / $s2);
open(F,"| gnuplot -geometry 750x700");
$points = "with points pt 0";
if (!$png && !$eps) {
print F "
set terminal x11 enhanced persist title '$f1 -- $f2';
set lmargin 6;
set bmargin 2;
set ylabel '$f2';
";
} elsif ($png) {
print F "
set terminal png size 900, 900;
set output 'plot.png';
set ylabel '$f2';
";
} elsif ($eps) {
print F "
set terminal postscript eps 24;
set output 'plot.eps';
set size 0.75, 1.0;
";
$points="";
}
$max *= 2.0;
$min /= 1.5;
#$max=100;$min=0.2;
print F "
set logscale;
set xlabel '$f1 $gain';
plot [$min:$max] [$min:$max] 'plotdata' notitle, \\
	x notitle, \\
	2*x notitle $points, \\
	0.5*x notitle $points, \\
	4*x notitle $points, \\
	0.25*x notitle $points, \\
	8*x notitle with points pt 0, \\
	0.125*x notitle with points pt 0;
" ;
close(F);
sleep(1) unless ($png);
}
unlink("plotdata");