]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/tests/TPTP/try.sh
Improved tests (for left parameters and mutual recursive definitions).
[helm.git] / helm / software / matita / tests / TPTP / try.sh
1 #!/bin/sh
2
3 prover=y
4
5 MATITAC=../../matitac.opt
6 #MATITAC=../../matitac
7 MATITAPROVER=../../matitaprover.opt
8 TPTPPATH=/home/tassi/TPTP-v3.1.1/
9
10 if [ -z "$1" ]; then
11   if [ $prover = 'y' ]; then
12     TODO=`cat elenco_unsatisfiable.txt`   
13   else
14     TODO=Unsatisfiable/[A-Z]*.ma
15   fi
16 else
17   TODO=`cat $1`
18 fi
19
20 mkdir -p logs
21
22 i=1
23 for X in $TODO; do
24   echo -n "$X ... "
25   LOGNAME=logs/log.`basename $X`
26   if [ $prover = 'y' ]; then
27     $MATITAPROVER -tptppath $TPTPPATH $X > $LOGNAME 2>&1
28   else
29     $MATITAC -nodb $X > $LOGNAME 2>&1
30   fi
31   if [ $prover = 'y' ]; then
32     BASE=`echo $X | cut -c 1-3`   
33     RATING=`grep "Rating" $TPTPPATH/Problems/$BASE/$X | sed 's/v.*//' | sed 's/%//'`      
34   else
35     RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'`
36   fi
37   if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then
38     TIME=`grep "TIME" $LOGNAME`
39     MAXWEIGHT=`grep "max weight:" $LOGNAME`
40     echo OK $TIME $RATING $MAXWEIGHT $i
41   else
42     echo FAIL $RATING $i
43   fi
44   i=`expr $i + 1`
45   gzip -f $LOGNAME
46 done