#!/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
set PROG = /projects/slvg21/avg/Mchaff/ChaffMod/Chaff2
set CHAFFDIR = /projects/algo2/Chaff/Chaff2_20010323
set FLAGS = ( $CHAFFDIR/lime3hrs.smj )
set FLAGS = ( $CHAFFDIR/lime.smj )

set os = `uname`
set ws = `hostname`
if ($os == Linux) then
	set PROG = /projects/slvg21/avg/Mchaff/ChaffLinux/Chaff2
	set MEM = 800m
	endif

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

set OUTDIR = Out-chaff-${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 $inf $OUTDIR/$logf $FLAGS) \
	>& $OUTDIR/$outf
set exitSt = $status
set ans = `get-chaff-ans.csh $OUTDIR/$outf | awk '{print $NF;}' `
echo $inf ans = $ans exitSt = $exitSt

pushd $OUTDIR >& /dev/null
egrep 'instance|UserTimeForSearch' ${infr}*.out > DC-${infr}
cat DC-${infr} | \
	sed -e 's/.out:Satisfyable.*$/ 1/' | \
	sed -e 's/.out:Unsatisfiable.*$/ 0/' | \
	sed -e 's/^Satisfyable.*$/ 1/' | \
	sed -e 's/^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
