1#!/bin/csh
2
3#
4#  Run a set of otter jobs ($1/*.in) and compare the
5#  results existing outputs.
6#
7#  If $2 is given, it is assumed to be the Otter binary to use.
8#
9#  If $3 is given, it is the filename extension for output files.
10#
11
12set base=out
13
14if ($#argv == 0) then
15    echo "usage: Run_all directory [otter] [extension]"
16    exit 1
17endif
18
19if ($#argv >= 2) then
20   set OTTER=$2
21else
22   set OTTER=../../bin/otter
23endif
24
25if ($#argv >= 3) then
26   set OUT=$3
27else
28   set OUT=out$$
29endif
30
31cd $1
32set errors=0
33foreach i (*.in)
34  echo "Running $1/$i ..."
35  $OTTER < $i >& $i:r.$OUT
36  if (-e $i:r.$base) then
37    set genold=`grep "clauses generated" $i:r.$base | awk '{gen+=$3} END {print gen}'`
38    set gennew=`grep "clauses generated" $i:r.$OUT | awk '{gen+=$3} END {print gen}'`
39    if ($gennew != $genold) then
40      echo "There is a problem: your computer generated $gennew, $OUT generated $genold"
41      set errors=1
42    else
43      echo "Okay, it seems to have run correctly."
44    endif
45  else
46    echo "Okay, but there's no file for comparison."
47    set errors=1
48  endif
49end
50
51echo ""
52
53if (! $errors && $1 != split) then
54  set timeold=`grep "CPU time" *.$base | awk '{sum += $4} END {print sum}'`
55  set timenew=`grep "CPU time" *.$OUT | awk '{sum += $4} END {print sum}'`
56  set speedup=`awk "END {print $timeold / $timenew}" /dev/null`
57  echo "timenew=$timenew, timeold=$timeold."
58  echo "The new ($OUT) times are about $speedup times as fast as the old ($base) times."
59  set too_slow=`awk "END {if ($speedup < .1) print 1}" /dev/null`
60  if ($too_slow) then
61    echo "If this seems way too slow, edit source/Makefile,"
62    echo "including -DTP_NO_CLOCKS on the DFLAGS line,"
63    echo "then make clean; make otter."
64  endif
65endif
66
67echo "The output files have been left in $1/*.$OUT."
68echo ""
69
70cd ..
71