author blanchet
Sat, 29 Oct 2011 13:15:58 +0200
changeset 45302 04c87dec70b8
parent 44391 7b4104df2be6
child 45304 e6901aa86a9e
permissions -rwxr-xr-x
gracefully do nothing if the SPASS input file is already in DFG format

#!/usr/bin/env bash
# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
# Isar proof reconstruction)
# Author: Jasmin Blanchette, TU Muenchen


# Try converting the file from TPTP to DFG, but fail gracefully if it is already
# in DFG format.
"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg || cp $name $name.fof.dfg
"$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
    | sed 's/description({$/description({*/' \
    | sed 's/set_ClauseFormulaRelation()\.//' \
    > $name.cnf.dfg
rm -f $name.fof.dfg
cat $name.cnf.dfg
"$SPASS_HOME/SPASS" $options $name.cnf.dfg \
    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
rm -f $name.cnf.dfg