#!/bin/csh -f
# run "check-rup.csh -keep" to append to $logname, else overwrites.

# Set your variables appropriately; if multiple sets, last one applies.

# Do "df -h . " (type the dot, not the quotes) to see how much disk
# is available in the current directory file system and decide on $filelimit.

# To produce your rup's on the fly, insert your solver command after
# the line "limit filesize $filelimit".  Note $inputcnf and $inputrup
# on lines just above the one mentioned.  DO NOT USE ">>& $inputlog"; instead
# use ">>& $logname" as you see on several other lines.

set rups = (fudge05-04.rup testeq.rup 5pipe.rup)

set RUPTORES = ./rupToRes_64_O3

set CHECKER3 = ./checker3_64_O3

set logname = rupToRes-all.log
set logname = rupToRes-64.log

set filelimit = 12288m
set filelimit = 16384m

#----------------------------------------------------------------------
if (-e $logname && x$1 != x-keep) /bin/rm $logname
touch $logname
foreach r ( $rups )
    set rr = $r:r
    set inputcnf = ${rr}.cnf
    set inputrup = ${rr}.rup
    set inputlog = ${rr}.log
    limit filesize $filelimit

    /usr/bin/time -p $RUPTORES $inputcnf >& $inputlog
    set ST = $status
    /bin/ls -l $inputrup ${rr}.proof >>& $inputlog
    cat $inputlog >>& $logname
    if ($ST == 25) echo WARNING: filesize exceeded $filelimit >>& $logname
    if ($ST != 20) then
        /bin/rm ${rr}.proof core*
        echo WARNING: rupToRes failed, verifier bypassed. >>& $logname
        continue
        endif

    set m = \
        `awk '/^c Original Num Clauses/{print $5;exit;}' $inputlog`
    set lastpf = \
        `awk '/^c Proof label of last phase2/{print $9;exit;}' $inputlog`
    @ npf = $lastpf - $m
    set fmlaints  = \
        `awk '/^[^cp]/{w+=NF;if($NF==0)w--;}END{print w;}' $inputcnf`
    set pfints  = \
        `awk '/^-rw.*\.proof$/{printf "%11.0f\n",($5+3.0)/4;}' $inputlog`
    set fmlapfints  = \
      `echo $fmlaints  $m| awk '{printf "%.0f\n",$1+0.0+6.0*$2;}'`
    set totpfints  = \
      `echo $fmlapfints $pfints | awk '{printf "%.0f\n",$1+0.0+$2;}'`
    echo FOUND $m $fmlapfints $lastpf $totpfints in $inputlog >>& $logname
    /bin/rm $inputlog

    /usr/bin/time -p $CHECKER3 $inputcnf ${rr}.proof >>& $logname
    set STCK = $status
    if ($STCK == 0) /bin/rm ${rr}.proof
    if ($STCK != 0) then
        echo ERROR: $0 exiting due to unverified proof ${rr}.proof
        exit $STCK
        endif
    end
