process.template

#!/bin/bash
# This is for BenchExec

# innermost, outermost, or nothing (for full rewriting)
strategy=STRATEGY
# SN, RC, or DC
property=PROPERTY

stdoutfile=`mktemp`

# first sed-ivocation removes the last line of the file, which is EOF
# second sed-invocation removes the time stamps
sed '$ d' $1 | sed 's/^[^\t]*\t//g' > "$stdoutfile"

result=`sed 1q "$stdoutfile"`

regex="YES|NO|AST|SAST|PAST|WORST_CASE\((\?|NON_POLY|Omega\(n\^([0-9]+)\)),(\?|POLY|O\((1|n\^([0-9]+))\))\)"

echo starexec-result=$result

if [[ "$result" =~ $regex ]]; then
	cpfinputfile=`mktemp`
	cpf2file=`mktemp`
	cpf3file=`mktemp`
	inputconversionerrfile=`mktemp`
	proofconversionerrfile=`mktemp`
	certerrfile=`mktemp`
	timefile=`mktemp`
	sed '1d' $stdoutfile > $cpf2file
	./cpf2_to_3.sh $cpf2file > $cpf3file 2> $proofconversionerrfile
	if [ -n "$strategy" ]; then
	    ./trs-conversion --from ari --to cpf3 --strategy "$strategy" --mode termcomp "$2" > $cpfinputfile 2> $inputconversionerrfile
	else
	    ./trs-conversion --from ari --to cpf3 --mode termcomp "$2" > $cpfinputfile 2> $inputconversionerrfile
	fi
	cert=`/usr/bin/time -o "$timefile" -f %U ./ceta --inputf "$cpfinputfile" --answer "$result" --property "$property" "$cpf3file" 2> "$certerrfile"`
	echo certification-result=$cert
	echo inputconversion-err=`cat "$inputconversionerrfile"`
	echo proofconversion-err=`cat "$proofconversionerrfile"`
	echo certification-err=`cat "$certerrfile"`
	echo certification-time=`cat "$timefile"`
	rm "$stdoutfile" "$cpfinputfile" "$cpf2file" "$cpf3file" "$certerrfile" "$inputconversionerrfile" "$proofconversionerrfile" "$timefile"
fi