#!/bin/ksh

DIR="$1"
PROBLEM="$2"
TIME="$3"

for FILE in `ls ${DIR}/p-${PROBLEM}*` ;
do

cat /dev/null > result

Kt < $FILE > result | true &

PID=$!

let SPENT=0

while test \( ! -s result \) -a \( ${SPENT} -lt ${TIME} \) ;
do
sleep 30
let SPENT=+30
done

kill -9 ${PID} >/dev/null 2>&1

INSTANCE=`echo ${FILE} | sed "s#${DIR}/##"` 

if test -s result ;
then
UNSAT=`grep -c "^.Formula is valid." result | sed "s#[^0-9]##g`
SAT=`grep -c "^.Formula is NOT valid." result | sed "s#[^0-9]##g`


WHEN=`grep "$time taken:" result | sed  "s#^.time taken: ##" | sed "s#seconds\.##"`

if test $UNSAT -eq 0 -a $SAT -eq 0 ;
then
TIME=360000
else
SEC=`echo $WHEN | sed "s#\([0-9]*\)\.\([0-9]*\)#\1#"  | sed "s#[^0-9]##g"`
MSEC=`echo $WHEN | sed "s#\([0-9]*\)\.\([0-9]*\)#\2#"  | sed "s#[^0-9]##g"`
                           
let TIME=$(($SEC+$(($MSEC/10000))))
fi

if test $UNSAT -eq 1 ;
then
	echo "r ${INSTANCE} ${TIME} U"
elif test $SAT -eq 1 ;
then
	echo "r ${INSTANCE} ${TIME} S"
else
	echo "r ${INSTANCE} ${TIME} T"
fi
else
	echo "r ${INSTANCE} 360000 T"
fi
done