#!/bin/bash

sedtimerule="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/"

# launch yices
echo "{\scriptsize"
echo "\begin{center}"
echo "\begin{tabular}{l|@{\;}c@{\;}c@{\ }c@{\ }c@{\ }c|@{\ }c@{\ }c}"
echo "\\hline"
echo "{\bf Benchmarks} & {\bf Ch79} & {\bf Ch79V2}  & {\bf Lookahead} & {\bf Aspic } & {\bf Smt-ai} & {\bf Smt-ai runtime} & {\bf Kind-ai runtime}\\\\"; 
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
	valid_idx=`ls -r results/${name}.kind-ai*.result | sed "s/results\/${name}\.kind-ai//g;s/\.result//g"`
	t_impl_k=`yices < generated_comp/${name}.${m}_kind-ai.yices | grep sat`;
	k_impl_t=`yices < generated_comp/${name}.kind-ai_${m}.yices | grep sat`;
	runtime=`cat runtime/${name}.kind-ai.time | grep elapsed | sed "${sedtimerule}"`
	if [ $t_impl_k = "unsat" -a $k_impl_t = "unsat" ]; then
	    previous="="
	elif [ $t_impl_k = "sat" -a $k_impl_t = "unsat" ]; then
	    previous="+"
	elif [ $t_impl_k = "unsat" -a $k_impl_t = "sat" ]; then
	    previous="-"
	elif [ $t_impl_k = "sat" -a $k_impl_t = "sat" ]; then
	    previous="||"
	else
	    previous="bot"
	fi
	for idx in ${valid_idx}; do
 	   echo "generated_comp/${name}.${m}_kind-ai${idx}.yices" >&2
	    t_impl_k=`yices < generated_comp/${name}.${m}_kind-ai${idx}.yices | grep sat`;
	    k_impl_t=`yices < generated_comp/${name}.kind-ai${idx}_${m}.yices | grep sat`;	    
	    if [ $t_impl_k = "unsat" -a $k_impl_t = "unsat" ]; then
		current="="
	    elif [ $t_impl_k = "sat" -a $k_impl_t = "unsat" ]; then
		current="+"
	    elif [ $t_impl_k = "unsat" -a $k_impl_t = "sat" ]; then
		current="-"
	    elif [ $t_impl_k = "sat" -a $k_impl_t = "sat" ]; then
		current="||"
	    else
		current="bot"
	    fi;
	    if [ $current = "-" -o $current = "||" -o \( $current = "=" -a $previous = "+" \) ]; then
		break
	    else
		echo "$idx is not invalid, we look earlier results" >&2
		previous=$current;
		runtime=`cat runtime/${name}.kind-ai${idx}.time | grep elapsed | sed "${sedtimerule}"`
	    fi;	    
 	done;
# #        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 "& $||$"
# 	# else
# 	#     echo "& $\bot$"
# 	# fi
	if [ $previous = "-" -o $previous = "||" ]; then
	    echo "& \$${previous}\$"
	else
	    echo "& \$${previous}\$ ${runtime}"
	fi;

    done;
    echo "& `cat  runtime/${name}.smt-ai.time | grep elapsed | sed "${sedtimerule}"` &"
    cat  runtime/${name}.kind-ai.time | grep elapsed | sed "${sedtimerule}"
    echo "\\\\";    
done;
echo "\\hline \\end{tabular}\\end{center}}";
