X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Ftests%2FTPTP%2Ftry.sh;fp=matita%2Ftests%2FTPTP%2Ftry.sh;h=685484d93ffe01e55d7b66d60d45f779044c4153;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/tests/TPTP/try.sh b/matita/tests/TPTP/try.sh
new file mode 100755
index 000000000..685484d93
--- /dev/null
+++ b/matita/tests/TPTP/try.sh
@@ -0,0 +1,46 @@
+#!/bin/sh
+
+prover=y
+
+MATITAC=../../matitac.opt
+#MATITAC=../../matitac
+MATITAPROVER=../../matitaprover.opt
+TPTPPATH=/home/tassi/TPTP-v3.1.1/
+
+if [ -z "$1" ]; then
+  if [ $prover = 'y' ]; then
+    TODO=`cat elenco_unsatisfiable.txt`	  
+  else
+    TODO=Unsatisfiable/[A-Z]*.ma
+  fi
+else
+  TODO=`cat $1`
+fi
+
+mkdir -p logs
+
+i=1
+for X in $TODO; do
+  echo -n "$X ... "
+  LOGNAME=logs/log.`basename $X`
+  if [ $prover = 'y' ]; then
+    $MATITAPROVER -tptppath $TPTPPATH $X > $LOGNAME 2>&1
+  else
+    $MATITAC -nodb $X > $LOGNAME 2>&1
+  fi
+  if [ $prover = 'y' ]; then
+    BASE=`echo $X | cut -c 1-3`	  
+    RATING=`grep "Rating" $TPTPPATH/Problems/$BASE/$X | sed 's/v.*//' | sed 's/%//'`	  
+  else
+    RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'`
+  fi
+  if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then
+    TIME=`grep "TIME" $LOGNAME`
+    MAXWEIGHT=`grep "max weight:" $LOGNAME`
+    echo OK $TIME $RATING $MAXWEIGHT $i
+  else
+    echo FAIL $RATING $i
+  fi
+  i=`expr $i + 1`
+  gzip -f $LOGNAME
+done