From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 29 May 2006 20:40:35 +0000 (+0000)
Subject: committed the base utils for TPTP processing
X-Git-Tag: 0.4.95@7852~1398
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d1f8a9b86dbd0466f02c7d0ad945a08903b672a;p=helm.git

committed the base utils for TPTP processing
---

diff --git a/matita/tests/TPTP/README b/matita/tests/TPTP/README
new file mode 100644
index 000000000..eba61fd0e
--- /dev/null
+++ b/matita/tests/TPTP/README
@@ -0,0 +1,30 @@
+to generate the problems:
+
+  cd ../../../components/binaries/tptp2grafite/
+  make generate
+  cd ../../../matita/tests/TPTP
+  ./classify.sh
+
+to start a run:
+
+  be sure to have matitac.opt in ../../
+  ./try | tee logname
+
+if you have a file containing the list of files to execute, like 
+
+  ...
+  Unsatisfiable/BOO001-1.ma
+  Unsatisfiable/BOO002-1.ma
+  Unsatisfiable/BOO004-2.ma
+  Unsatisfiable/LCL113-2.ma
+  ...
+
+  you can run 
+  
+  ./try filewithproblemlist | tee logname
+
+logname format
+
+  log.SECONDS.DAY-MONTH.MESSAGE
+
+
diff --git a/matita/tests/TPTP/classify.sh b/matita/tests/TPTP/classify.sh
new file mode 100755
index 000000000..2fc71e093
--- /dev/null
+++ b/matita/tests/TPTP/classify.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+
+mkdir Open
+mkdir Unknown
+mkdir Satisfiable
+mkdir Unsatisfiable
+
+for X in [A-Z]*.ma; do
+  echo $X
+  STATUS=`grep "^(\* *Status *:" $X`
+  if [ `echo $STATUS | grep Open | wc -l` -eq 1 ]; then
+    mv $X Open/
+  fi
+  if [ `echo $STATUS | grep Unknown | wc -l` -eq 1 ]; then
+    mv $X Unknown/
+  fi
+  if [ `echo $STATUS | grep Satisfiable | wc -l` -eq 1 ]; then
+    mv $X Satisfiable/
+  fi
+  if [ `echo $STATUS | grep Unsatisfiable | wc -l` -eq 1 ]; then
+    mv $X Unsatisfiable/
+  fi
+done
diff --git a/matita/tests/TPTP/try.sh b/matita/tests/TPTP/try.sh
new file mode 100755
index 000000000..eb1c3f9d1
--- /dev/null
+++ b/matita/tests/TPTP/try.sh
@@ -0,0 +1,22 @@
+#!/bin/sh
+
+if [ -z "$1" ]; then
+  TODO=Unsatisfiable/[A-Z]*.ma
+else
+  TODO=`cat $1`
+fi
+
+mkdir -p logs
+
+for X in $TODO; do
+  echo -n "$X ... "
+  LOGNAME=logs/log.`basename $X`
+  ../../matitac.opt $X > $LOGNAME 2>&1
+  if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then
+    TIME=`grep "TIME NEEDED" $LOGNAME`
+    RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'`
+    echo OK $TIME $RATING
+  else
+    echo FAIL
+  fi
+done