From 4d6dfee39ca102851b1f10738598166b15c052da Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 29 May 2006 20:40:35 +0000
Subject: [PATCH] committed the base utils for TPTP processing

---
 helm/software/matita/tests/TPTP/README      | 30 +++++++++++++++++++++
 helm/software/matita/tests/TPTP/classify.sh | 23 ++++++++++++++++
 helm/software/matita/tests/TPTP/try.sh      | 22 +++++++++++++++
 3 files changed, 75 insertions(+)
 create mode 100644 helm/software/matita/tests/TPTP/README
 create mode 100755 helm/software/matita/tests/TPTP/classify.sh
 create mode 100755 helm/software/matita/tests/TPTP/try.sh

diff --git a/helm/software/matita/tests/TPTP/README b/helm/software/matita/tests/TPTP/README
new file mode 100644
index 000000000..eba61fd0e
--- /dev/null
+++ b/helm/software/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/helm/software/matita/tests/TPTP/classify.sh b/helm/software/matita/tests/TPTP/classify.sh
new file mode 100755
index 000000000..2fc71e093
--- /dev/null
+++ b/helm/software/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/helm/software/matita/tests/TPTP/try.sh b/helm/software/matita/tests/TPTP/try.sh
new file mode 100755
index 000000000..eb1c3f9d1
--- /dev/null
+++ b/helm/software/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
-- 
2.39.2