#!/bin/bash

printf "bench\ttime\tnb_inv\n"
for i in lustre/*.lus; do 
  wc -l results/`basename $i .lus`.kind-ai.*.result | grep results > tmp;
  line=""; \
  while read line; do \
  printf "`basename $i .lus`\t"; 
   nb_inv=`echo "$line" | sed "s/[' ']*\([0-9]*\)[' ']*\(.*\).result/\1/"`;
   t=`echo "$line" | sed "s/[' ']*\([0-9]*\)[' ']*results\/\(.*\).result/\2/"`;
   time=`cat runtime/$t.time | grep elapsed | sed "s/^.*system //;s/elapsed.*//;s/0://;s/00\.\(..\)/\1/;s/\(..\)\.\(..\)/\1\2/;s/\^0\([1-9]\)/\1/"`;
#    name=`echo $i | sed "s/results\/\(.*\).kind-ai\(.*\)\.result/\1\2/`;  
#    echo `basename $name &`;
#    echo "`echo $tmp | sed "s/\.$//"`$idx";
     printf "${time}\t${nb_inv}\t";
#   tmp=`echo results/$t.result | sed "s/results\/\(.*\)kind-ai.*\.result/\1/"`;\
#   idx=`echo  results/$t.result | sed "s/.*kind-ai\(.*\)\.result/\1/;s/\.$//"`;\
#      first=1
#     for m in "ch79" "ch79v2" "lookahead" "aspic"; 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
# 	if [ $first -eq 0 ]; then
# 	    printf ","
# 	fi
# 	    printf "${m}="
# 	elif [ $t_impl_k = "sat" -a $k_impl_t = "unsat" ]; then
# 	if [ $first -eq 0 ]; then
# 	    printf ","
# 	fi
# 	    printf "${m}+"
# #	elif [ $t_impl_k = "sat" -a $k_impl_t = "sat" ]; then
# #	    echo ", ${m}neq"
# 	fi
# 	first=0;
#    done | xargs;
    printf "N";    
  done < tmp |xargs | sed "s/N /\n/g;s/N/\n/g" | sed "/^$/d";
done
