src/HOL/Tools/ATP/scripts/spass
author huffman
Sat, 21 Apr 2012 10:59:52 +0200
changeset 47647 ec29cc09599d
parent 47055 16e2633f3b4b
permissions -rwxr-xr-x
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator

#!/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}
home=${SPASS_OLD_HOME:-$SPASS_HOME}

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