#!/bin/ksh93

SDIR=${.sh.file%/*}
typeset -r FPROG=${.sh.file}
typeset -r PROG=${FPROG##*/}
typeset -r VERSION='1.9'

PATH="${SDIR}:${PATH}"		# prefer the tools in the same path as this script
PROVER=${ whence eprover ; }
EXTRACT=${ whence epclextract ; }

function showUsage {
	typeset OPT
    [[ -z $1 ]] && X='--man' || X='-?'
    getopts -a ${PROG} "${ print ${USAGE} ; }" OPT $X
}

# temp. file to use
TMPFILE=
function cleanup {
	[[ -z ${TMPFILE} ]] && return
	cd || cd /
	rm -rf ${TMPFILE}
}

# print the last N entries of the given array, one per line.
function printLast {
	typeset -n A=$1
	integer N=$2 I K=${#A[@]}
	typeset OUT=

	(( ! N )) && return 0
	(( N < 0 )) && N=$K
	(( I=K - N ))
	(( I < 0 )) && I=0
	for (( ; I < K; I++ )); do
		OUT+="${A[I]}\n"
	done
	print "${OUT}"
}

function killBill {
	typeset TIME=$1 PID=$2 BLA=X
	read -t ${TIME} BLA					# timeout causes BLA to be set to ''
	[[ -z ${BLA} ]] && return 0			# input closed (EOF)
	kill -s KILL ${PID} 2>/dev/null
	print "# Time limit exceeded (${TIME} s)."
	return 1
}

function doMain {
	[[ -z ${PROVER} ]] && print -u2 'eprover not found - exiting.' && return 1
	[[ -z ${EXTRACT} ]] && print -u2 'eplextract not found - exiting.' && return 1

	if [[ ${PROG} == 'eproof_ram' ]]; then
		${PROVER} -l 4 -R -o - --pcl-terms-compressed --pcl-compact "$@" | \
			${EXTRACT} ${FORMAT} -f -C --competition-framing
		return $?
	fi

	TMPFILE=${ mktemp -t ${PROG}.XXXXXX ; }
	[[ -z ${TMPFILE} ]] && exit 2

	typeset TAIL STIME OUT
	[[ ${ uname -s ; } == 'SunOS' ]] && TAIL='/usr/xpg4/bin/tail' || TAIL='tail'

	# Effectively unlimited
	integer SEARCHLIMIT=2000000000 PROOFLIMIT=2000000000 N_TAIL=0 \
		PROOF=-1 WL_EMPTY=0 I P RES

	(( PRINT_STATS )) && N_TAIL=33 && PRINT_RES=1
	(( PRINT_RES )) && (( N_TAIL+= 6 ))

	${PROVER} -l 4 -R -o - --pcl-terms-compressed --pcl-compact "$@" \
		> "${TMPFILE}"
	RES=$?

	# parse results
	typeset -a LINES
	${TAIL} -n 70 "${TMPFILE}" | while read LINE ; do
		LINES+=( "${LINE}" )	# record (could be a huge file)
		[[ ${LINE:0:1} == '#' ]] || continue
		if [[ ${LINE:40:1} == ':' ]]; then
			[[ ${LINE:2:18} == 'Preprocessing time' ]] && print "${LINE}"
			continue
		fi
		[[ ${LINE:2:10} == 'Total time' ]] && \
			A=( ${LINE} ) && STIME=${A[4]%.*} && continue
		[[ ${LINE:2:15} == 'No proof found!' ]] && PROOF=0 && continue
		[[ ${LINE:2:12} == 'Proof found!' ]] && PROF=1 && continue
		[[ ${LINE:2:19} == 'Watchlist is empty!' ]] && WL_EMPTY=1 && continue
		[[ ${LINE:2:10} == 'SZS status' ]] && OUT+="${LINE}\n" && continue
		[[ ${LINE:2:7} == 'Failure' ]] && OUT+="${LINE}\n" && continue
	done

	if [[ -z ${STIME} ]]; then
	    print -u2 '# Cannot determine problem status within resource limit'
		return 1
	fi

	if (( ! PRROF )); then
		print '# Problem is satisfiable (or invalid), generating' \
			'saturation derivation'
	elif (( PROOF == 1 )); then
		print '# Problem is unsatisfiable (or provable), constructing' \
			'proof object'
	elif (( WL_EMPTY )); then
		print '# All watchlist clauses generated, constructing derivation'
	else
		print '# Cannot determine problem status'
		printLast LINES ${N_TAIL}
		return  ${RES}
	fi

	[[ -n ${OUFILE} ]] && exec 1> "${OUTFILE}"
	[[ -n ${OUT} ]] && print -n "${OUT}"
	grep '# SZS answer' "${TMPFILE}"

	if (( LIMITPROOFTIME )); then
		I=${STIME}
		(( PROOFLIMIT=TIMELIMIT - I ))
		(( PROOFLIMIT < 1 )) && \
			print -u2 "# Time limit exceeded (${PROOFLIMIT} s)." && return 99
		${EXTRACT} ${FORMAT} -f --competition-framing "${TMPFILE}" &
		I=$!
		killBill ${PROOFLIMIT} $I |&	# anyone remembers, what a copro is ;-)
		exec 8>&p			# assign fd8 to killBill's stdin
		exec 9<&p			# assign fd9 to killBill's stdout
		wait $I 2>/dev/null	# wait for extract to finish or be killed
		RES=$?
		read -u9 -t 0 X		# perhaps killBill has something to say
		[[ -n $X ]] && RES=99 && print -u2 "$X"
		exec 8>&-			# close killBill's stdin so it can terminate
		exec 9<&-			# similar
	else
		${EXTRACT} ${FORMAT} -f --competition-framing "${TMPFILE}"
		RES=$?
	fi
	printLast LINES ${N_TAIL}
	return ${RES}
}

USAGE='[-?'"${VERSION}"' ]
[-copyright?(C) 1998-2009  Stephan Schulz (schulz@eprover.org)]
[-portions copyright?(C) 2015 Jens Elkner (ksh93 port/cleanup)]
[-license?GPL 2+]
[-source?http://www.eprover.org]
[+NAME?'"${PROG}"' - a wrapper around eprover and epclextract]
[+DESCRIPTION?'"${PROG}"' is a wrapper around eprover and epclextract. It will run eprover with output level 4 (full output of all potentially proof-relevant inferences) and, in the case of success, automatically run epclextract to provide a proof derivation or a derivation of all clauses in the saturated proof state.]
[+?Please note that '"${PROG}"', unlike most E tools, does not support reading problems from stdin. It will silently assume an empty input from stdin.]
[+?Remember that all options and arguments which should be passed on to eprover or epclextract need to be given as operands to this script, i.e. use the "--" string to avoid, that this script chomps these (possibly unknown) options. E.g. "'"${PROG}"' -o \aoutfile\a \b--\b -W none --prune \afile\a" would result into "eprover -W none --prune \afile\a".]
[+?In particular, eproof will automatically do a close approximation of "the right thing" (tm) with the options describing input- and output formats.]
[h:help?Print this help and exit.]
[F:functions?Print a list of all functions available.]
[T:trace]:[fnList?A comma separated list of functions of this script to trace (convinience for troubleshooting).]
[+?]
[o:output-file]:[file?Redirect output into the given \afile\a.]
'
if [[ ${PROG} != 'eproof_ram' ]]; then
	USAGE+='[C:cpu-limit]:[num?Limit the time the prover is allowed to run to \anum\a seconds. \bNOTE\b for compatibility reasons and to avoid useless coredumps caused by signal XCPU this is \bnot cpu time\b but the elapsed (real) time - the long option name is kept for backward compatibility.]
[R:resources-info?Give some information about the resources used by the prover.]
[S:print-statistics?Print the inference statistics.]
'
fi
USAGE+='[V:version?Print the version numbers of \beprover\b(1) and \bepclextract\b(1) used by this script. Please include this with all bug reports (if any).]
[u:proof-time-unlimited?If eprover succeeds within the overall timelimit, do not stop \bepclextract\b(1) due to timeout.]
[84:tstp-in?Parse TPTP-3 format instead of E-LOP.]
[80:tstp-out?Print output clauses in TPTP-3 syntax.]
[81:tstp-format?Same as \b--tstp-in --tstp-out\b.]
[82:tptp3-out?Same as \b--tstp-out\b.]
[83:tptp3-format?Same as \b--tstp-format\b.]
[+SEE ALSO?\beprover\b(1), \bepclextract\b(1).]
\n\n\afile\a ...
'
integer TIMELIMIT=0 PRINT_RES=0 PRINT_STATS=0 LIMITPROOFTIME=1
typeset OUTFILE= FORMAT= IN_FORMAT= X="${ print ${USAGE} ; }"
while getopts "${X}" OPT ; do
	case ${OPT} in
		h) showUsage ; exit 0 ;;
		T)	if [[ ${OPTARG} == 'ALL' ]]; then
				typeset -ft ${ typeset +f ; }
			else
				typeset -ft ${OPTARG//,/ }
			fi
			;;
		F) typeset +f && exit 0 ;;
		
		C) TIMELIMIT="${OPTARG}" ;;
		o) OUTFILE="${OPTARG}" ; cp /dev/null "${OUTFILE}" ;;
		R) PRINT_RES=1 ;;
		S) PRINT_STATS=1 ;;
		u) LIMITPROOFTIME=0 ;;
		V)	[[ -z ${EPROVER} ]] && print -u2 'eprover not found' && exit 1
			A=( ${ ${PROVER} --version ; } )
			print "${A[1]}"
			exit  0
			;;
		80|82) FORMAT='--tstp-out' ;;
		81|83) FORMAT='--tstp-out' ; IN_FORMAT='--tstp-in' ;;
		84) IN_FORMAT='--tstp-in' ;;
		*) showUsage 1 && exit 1 ;;	
	esac
done
X=$((OPTIND-1))
shift $X && OPTIND=1
unset X

(( TIMELIMIT < 1 )) && TIMELIMIT=2000000000

trap cleanup EXIT
doMain ${IN_FORMAT} "$@"