]> matita.cs.unibo.it Git - helm.git/blob - matita/tests/TPTP/try.sh
Added the computation of max_weight.
[helm.git] / matita / tests / TPTP / try.sh
1 #!/bin/sh
2
3 MATITAC=../../matitac.opt
4 #MATITAC=../../matitac
5
6 if [ -z "$1" ]; then
7   TODO=Unsatisfiable/[A-Z]*.ma
8 else
9   TODO=`cat $1`
10 fi
11
12 mkdir -p logs
13
14 i=1
15 for X in $TODO; do
16   echo -n "$X ... "
17   LOGNAME=logs/log.`basename $X`
18   $MATITAC -nodb $X > $LOGNAME 2>&1
19   RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'`
20   if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then
21     TIME=`grep "TIME NEEDED" $LOGNAME`
22     MAXWEIGHT=`grep "max weight:" $LOGNAME`
23     echo OK $TIME $RATING $MAXWEIGHT $i
24   else
25     echo FAIL $RATING $i
26   fi
27   i=`expr $i + 1`
28   gzip -f $LOGNAME
29 done