#!/bin/csh -f

if ($#argv != 4) then
	echo Usage: $0 in.cnf ncolors cpumins '-c | -cn | -tr'
	exit $#argv
	endif

if (x$4 != x-c && x$4 != x-cn && x$4 != x-tr) then
	echo Usage: $0 in.cnf ncolors cpumins '-c | -cn | -tr'
	exit $#argv
	endif


set MEM = 800m
# one day = 86400.  $CPUTO controls limit, so this is set higher.
set FLAGS = (-t 3000000 -h 4 )
set PROG = 2clseq


set os = `uname`
set ws = `hostname`
if ($os == Linux) then
	set PROG = Linux/2clseq
	set MEM = 1600m
	endif

if ($ws == pegasus) then
	set MEM = 3600m
	endif

set OUTDIR = Out-2clseq-${ws}$4
if (! -e $OUTDIR) mkdir $OUTDIR

set NCOL = $2
if ($NCOL < 10) set NCOL = 0$NCOL
# We'll assume ncolors (almost) always < 100 and use 2 digits minimum.

set CPU = $3
@ CPUTO = $CPU * 101 / 100

set inf = $1
set inft = $inf:t
set infr = $inft:r
set infncol = $infr-$NCOL
set outf = $infncol.out
set logf = $infncol.log

echo -n Starting on $inf for $NCOL colors ' '
date
head -4 $inf | sed 's/^/	/'

(limit cputime ${CPUTO}m; \
	limit coredumpsize 100k; \
	limit stacksize 256m; \
	limit datasize $MEM; \
	/usr/bin/time -p $PROG $FLAGS $inf ) \
	>& $OUTDIR/$outf
set exitSt = $status
tr ',' ' ' < timetable.dat > $OUTDIR/$logf
/bin/rm timetable.dat
set ans = `get-2clseq-ans.csh $OUTDIR/$outf | awk '{print $NF;}' `
echo $inf ans = $ans exitSt = $exitSt

pushd $OUTDIR >& /dev/null
egrep 'SATISFIABLE|UNKNOWN|cpu sec' ${infr}*.out | \
	tr -d '()' | sed 's/\([0-9]\)\([a-z]\)/\1 \2/g' > DC-${infr}
cat DC-${infr} | \
	sed -e 's/.out:SATISFIABLE.*$/ 1/' | \
	sed -e 's/.out:UNSATISFIABLE.*$/ 0/' | \
	cat > ans-${infr}

popd >& /dev/null

echo -n Done ' '
date

set MAXSIG = 45 # check /usr/include/sys/signal.h
if ($os == Linux) set MAXSIG = 63

@ XMAXSIG = 128 + $MAXSIG
if ($ans < 0 && $exitSt >= 128 && $exitSt <= $XMAXSIG) then
	exit $exitSt
	endif

if ($os == Linux && $ans < 0 && $exitSt > 1 && $exitSt <= $MAXSIG) then
	@ exsh = 128 + $exitSt
	exit $exsh
	endif

exit $ans

