#!/bin/bash

# launch yices
echo "\\documentclass{article}"
echo "\\begin{document}"
echo "\\begin{tabular}{|l|ccccc|}"
echo "\\hline"
echo " &  ch79 & ch79v2  & lookahead & aspici & smt-ai\\\\"; 
echo "\\hline"
for i in results/*.kind-ai*result; do 
  tmp=`echo $i | sed "s/results\/\(.*\)kind-ai.*\.result/\1/"`;\
  idx=`echo $i | sed "s/.*kind-ai\(.*\)\.result/\1/;s/\.$//"`;\
#    name=`echo $i | sed "s/results\/\(.*\).kind-ai\(.*\)\.result/\1\2/`;  
#    echo `basename $name &`;
    echo "`echo $tmp | sed "s/\.$//"`$idx";
    for m in "ch79" "ch79v2" "lookahead" "aspic" "smt-ai"; do
#        echo $name \"$t_impl_k\" \"$k_impl_t\" $m >&2
#	echo ${name}.${m}_kind-ai.yices >&2
      file1=$tmp$m\_kind-ai${idx}.yices;
      file2=${tmp}kind-ai${idx}\_$m.yices;
      t_impl_k=`yices < generated_comp/${file1} | grep sat`;
#	echo ${name}.kind-ai_${m}.yices >&2
	k_impl_t=`yices < generated_comp/${file2} | grep sat`;
	if [ $t_impl_k = "unsat" -a $k_impl_t = "unsat" ]; then
	    echo "& $=$"
	elif [ $t_impl_k = "sat" -a $k_impl_t = "unsat" ]; then
	    echo "& \$+\$"
	elif [ $t_impl_k = "unsat" -a $k_impl_t = "sat" ]; then
	    echo "& \$-$"
	elif [ $t_impl_k = "sat" -a $k_impl_t = "sat" ]; then
	    echo "& $\neq$"
	else
	    echo "& $\bot$"
	fi
    done;
    echo "\\\\";    
done;
echo "\\hline \\end{tabular}\\\\"
echo "$=$ means that the results of kind-ai and of the other tool are equivalent.\\\\"
echo "$\neq$ means that the results were not comparable. Kind-ai was not better than the other and vice versa.\\\\"
echo "$+$ means that kind-ai was better than the other tool\\\\"
echo "\$-$ means that the other tool properties implied the ones obtained by kind-ai\\\\"

echo "\\begin{tabular}{|l|cccccc|}"
echo "\\hline"
echo " & ch79 & ch79v2 & lookahead & aspic &  smt-ai & kind-ai \\\\"; 
echo "\\hline"
for i in runtime/*.kind-ai.time; do 
    name=`basename $i .kind-ai.time`;  
    echo $name;
    for m in "ch79" "ch79v2" "lookahead" "aspic" "smt-ai" "kind-ai"; do
	echo "&"
	cat  runtime/${name}.${m}.time | grep elapsed | sed "s/^.*system //;s/elapsed.*//;s/0://;s/00\.\(..\)/\1ms/;s/\(..\)\.\(..\)/\1.\2s/;s/^0\([1-9]\)/\1/"
	
    done;
    echo "\\\\";    
done;
echo "\\hline \\end{tabular}\\\\"

echo "\\end{document}"
