#!/bin/csh

if ($#argv != 2) then
    echo "Need 2 arguments: input file, time limit in seconds. "
    exit 1
endif

set input=$1
set time_limit=$2

# set TPTPHome = /home/tptp

set OTTER=/home/mccune/ctp/source/otter
set MACE_LOOP=mace-loop

set unique_id=`hostname`-$$
set OUTFILE=/tmp/otter-mace-out-$unique_id
set TIMEFILE=/tmp/time-$unique_id

set time=10000

if (! -e $input) then
    echo $input not found.
    exit 1
endif

######################## Try Otter for a short time.

limit cputime 5
cat $input | $OTTER >& $OUTFILE
set stat=$status
if ($stat == 103) goto proof

######################## Try MACE for a short time.

limit cputime 5
$MACE_LOOP $input 10000 10000 -m1 -p > $OUTFILE
set stat=$status
if ($stat == 15 || $stat == 16) goto model

######################## Try Otter for the remaining time.

time > $TIMEFILE
set seconds_spent=`cat $TIMEFILE | sed 's/\..*//'`
/bin/rm $TIMEFILE

@ cpu_limit= $time_limit - $seconds_spent
limit cputime $cpu_limit

# echo $seconds_spent seconds_spent
# echo $time_limit time_limit
# echo $cpu_limit cpu_limit

cat $input | $OTTER >& $OUTFILE
set stat=$status
if ($stat == 103) goto proof

############################################## (failure)

set pm='fail'
set siz='-'
set lev='-'
# set cpu=`grep 'user CPU time' $OUTFILE | awk '{print $4}'`
set gen=`grep 'clauses generated' $OUTFILE | awk '{print $3}'`
set mem=`grep 'Kbytes malloced' $OUTFILE | awk '{print $3}'`K

goto print

############################################## proof:

proof:

set pm=PROOF
set siz=`grep 'Length of proof' $OUTFILE | awk '{print $5}' | sed 's/\.//'`
set lev=`grep 'Length of proof' $OUTFILE | awk '{print $10}' | sed 's/\.//'`
# set cpu=`egrep 'UNIT|EMPTY' $OUTFILE | awk '{print $5}'`
set gen=`grep 'clauses generated' $OUTFILE | awk '{print $3}'`
set mem=`grep 'Kbytes malloced' $OUTFILE | awk '{print $3}'`K

goto print

############################################## model:

model:

cat $OUTFILE

set pm=MODEL
set mem='-'
set lev='-'
set gen='-'
# set cpu=`grep 'Model #1' $OUTFILE | awk '{print $5}'`
set siz=`grep 'The set is satisfiable' $OUTFILE | awk '{print $10}'`

goto print

############################################## print:

print:

time > $TIMEFILE
set seconds_spent=`cat $TIMEFILE | sed 's/\..*//'`
/bin/rm $TIMEFILE

echo "$input $pm $stat $seconds_spent $mem $gen $siz $lev"
time

/bin/rm $OUTFILE
exit 0