#!/bin/sh

case "x$1" in
  xextra*)
    logs=extralogs; times=extratimes
    ;;
  *)
    logs=logs; times=times
esac

names=`awk '{print $2}' $times/summary`
echo '{%'
echo '\\def\\S{\\hspace{.5em}}'
echo -n '\\begin{tabular}{|@{\\S}r'

for name in $names
do
  echo -n '@{\\S}|@{\\S}r'
done
echo '@{\\S}|}'

echo '\\hline'

printf "%17s" ""
for name in $names
do
  case $name in
    sc14*) name="sc14-ayv";;
    minisat) name="mini-sat";;
    glucose*) name="glu-cose-2.3";;
    swd*) name="swd-ia5by-a26";;
  esac
  if [ x"`echo $name|grep -- -`" = x ]
  then
    printf "&%14s" $name
  else
    echo -n '&\\shortstack{'"`echo $name|sed -e 's,-,@@@@,g'|tr @ '\\\\'`"'}'
  fi
done
echo '\\\\'
echo '\\hline'
echo '\\hline'

printf "%17s" solved
for name in $names
do
  printf "&%14d" `grep 'SATISFIABLE$' $logs/$name/*.log|wc -l`
done
echo '\\\\'

printf "%17s" unsatisfiable
for name in $names
do
  printf "&%14d" `grep '\<UNSATISFIABLE$' $logs/$name/*.log|wc -l`
done
echo '\\\\'

printf "%17s" satisfiable
for name in $names
do
  printf "&%14d" `grep '\<SATISFIABLE$' $logs/$name/*.log|wc -l`
done
echo '\\\\'

echo '\\hline'
echo '\\hline'

printf "%17s" 'reductions (1e3 \#)'
for name in $names
do
  case $name in
    glucose*|swd*)
      n=`awk '/^c nb ReduceDB.*:/{s+=$5}END{printf "%.0f", s/1e3}' $logs/$name/*.log`
      printf "&%14d" $n
      ;;
    minisat*)
      printf "&%14s" "---"
      ;;
    sc14*)
      n=`awk '/^c reds:.*count,/{s+=$3}END{printf "%.0f", s/1e3}' $logs/$name/*.log`
      printf "&%14d" $n
      ;;
    *)
      n=`grep reductions, $logs/$name/*.log|awk '{s+=$2}END{printf "%.0f", s/1e3}'`
      printf "&%14d" $n
      ;;
  esac
done
echo '\\\\'

printf "%17s" 'restarts (1e3 \#)'
for name in $names
do
  case $name in
    glucose*|swd*)
      n=`awk '/^c restarts.*:/{s+=$4}END{printf "%.0f", s/1e3}' $logs/$name/*.log`
      ;;
    minisat*)
      n=`awk '/^restarts.*:/{s+=$3}END{printf "%.0f", s/1e3}' $logs/$name/*.log`
      ;;
    sc14*)
      n=`awk '/^c rsts:.*restarts/{s+=$3}END{printf "%.0f", s/1e3}' $logs/$name/*.log`
      ;;
    *)
      n=`grep restarts, $logs/$name/*.log|awk '{s+=$2}END{printf "%.0f", s/1e3}'`
      ;;
    esac
    printf "&%14d" $n
done
echo '\\\\'

printf "%17s" 'rescored (1e3 \#)'
for name in $names
do
  case $name in
    glucose*|swd*|minisat*)
      printf "&%14s" "---"
      ;;
    *)
      n=`grep '^c coll:' $logs/$name/*.log|awk '{s+=$8}END{printf "%.0f", s/1e3}'`
      printf "&%14d" $n
      ;;
  esac
done
echo '\\\\'

echo '\\hline'

for stats in conflicts decisions
do
  printf "%17s" "$stats "'(1e6 \#)'
  for name in $names
  do
    case $name in
      glucose*|swd*)
	n=`awk '/^c '$stats'.*:/{s+=$4}END{printf "%.0f", s/1e6}' $logs/$name/*.log`
	;;
      minisat*)
	n=`awk '/^'$stats'.*:/{s+=$3}END{printf "%.0f", s/1e6}' $logs/$name/*.log`
        ;;
      *)
	n=`grep $stats, $logs/$name/*.log|awk '{s+=$2}END{printf "%.0f", s/1e6}'`
	;;
    esac
    printf "&%14d" $n
  done
  echo '\\\\'
done

echo '\\hline'
echo '\\hline'

printf "%17s" 'simp (1e3 sec)'
for name in $names
do
  case $name in
    glucose*|swd*)
      n=`grep "Simplification time:" $logs/$name/*.log|awk '{s+=$5}END{printf "%.1f", s/1e3}'`
      ;;
    minisat*)
      n=`grep "Simplification time:" $logs/$name/*.log|awk '{s+=$4}END{printf "%.1f", s/1e3}'`
      ;;
    *)
      n=`grep "simplifying\\$" $logs/$name/*.log|awk '{s+=$2}END{printf "%.1f", s/1e3}'`
      ;;
  esac
  printf "&%14.1f" $n
done
echo '\\\\'

printf "%17s" "search (1e3 sec)"
for name in $names
do
  case $name in
    glucose*|swd*)
      n=`awk '/Simplification time:/{p=$5}/CPU time/{s+=$5-p}END{printf "%.1f", s/1e3}' $logs/$name/*.log`
      ;;
    minisat*)
      n=`awk '/Simplification time:/{p=$4}/CPU time/{s+=$4-p}END{printf "%.1f", s/1e3}' $logs/$name/*.log`
      ;;
    *)
      n=`grep "search\\$" $logs/$name/*.log|awk '{s+=$2}END{printf "%.1f", s/1e3}'`
      ;;
  esac
  printf "&%14.1f" $n
done
echo '\\\\'

echo '\\hline'

for time in bump decide rescore
do
  printf "%17s" "$time (1e3 sec)"
  for name in $names
  do
    case $name in
      glucose*|swd*|minisat*)
	printf "&%14s" "---"
        ;;
      sc14*)
        case time in
	  rescore)
	    printf "&%14s" "---"
	    ;;
	  *)
	    n=`grep "$time\\$" $logs/$name/*.log|awk '{s+=$2}END{printf "%.1f", s/1e3}'`
	    printf "&%14.1f" $n
	    ;;
	esac
	;;
      *)
	n=`grep "$time\\$" $logs/$name/*.log|awk '{s+=$2}END{printf "%.1f", s/1e3}'`
	printf "&%14.1f" $n
	;;
    esac
  done
  echo '\\\\'
done

echo '\\hline'
echo '\\end{tabular}}'
