#!/bin/bash

# launch yices
echo "\\documentclass{article}"
echo "\\begin{document}"
echo "\\begin{tabular}{|l|ccccc|}"
echo "\\hline"
echo " &  ch79 & ch79v2  & lookahead & aspic& smt-ai\\\\"; 
echo "\\hline"
for i in results/*.kind-ai.result; do 
    name=`basename $i .kind-ai.result`;  
    echo `basename $name &`;
    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
	t_impl_k=`yices < generated_comp/${name}.${m}_kind-ai.yices | grep sat`;
#	echo ${name}.kind-ai_${m}.yices >&2
	k_impl_t=`yices < generated_comp/${name}.kind-ai_${m}.yices | 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/\([0-9]*\):/\1m/;s/\./s/;s/m00s00/m/;s/s00/s/;s/m00/m/;s/00s\(..\)/\1ms/;s/^0\([1-9]\)/\1/"
	
    done;
    echo "\\\\";    
done;
echo "\\hline \\end{tabular}\\\\"

echo "\\end{document}"
