src/HOL/Tools/ATP/scripts/spass

better handling of individual type for DFG format (SPASS)

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

options=${@:1:$(($#-1))}
name=${@:$(($#)):1}

"$SPASS_HOME/SPASS" -Flotter $name \
    | sed 's/description({$/description({*/' \
    | sed 's/set_ClauseFormulaRelation()\.//' \
    > $name.cnf
cat $name.cnf
"$SPASS_HOME/SPASS" $options $name.cnf \
    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
rm -f $name.cnf