src/HOL/Tools/ATP/scripts/spass
changeset 47055 16e2633f3b4b
parent 46403 3069344da626
equal deleted inserted replaced
47054:b86864a2b16e 47055:16e2633f3b4b
     5 #
     5 #
     6 # Author: Jasmin Blanchette, TU Muenchen
     6 # Author: Jasmin Blanchette, TU Muenchen
     7 
     7 
     8 options=${@:1:$(($#-1))}
     8 options=${@:1:$(($#-1))}
     9 name=${@:$(($#)):1}
     9 name=${@:$(($#)):1}
       
    10 home=${SPASS_OLD_HOME:-$SPASS_HOME}
    10 
    11 
    11 "$SPASS_HOME/SPASS" -Flotter "$name" \
    12 "$home/SPASS" -Flotter "$name" \
    12     | sed 's/description({$/description({*/' \
    13     | sed 's/description({$/description({*/' \
    13     | sed 's/set_ClauseFormulaRelation()\.//' \
    14     | sed 's/set_ClauseFormulaRelation()\.//' \
    14     > $name.cnf
    15     > $name.cnf
    15 cat $name.cnf
    16 cat $name.cnf
    16 "$SPASS_HOME/SPASS" $options "$name.cnf" \
    17 "$home/SPASS" $options "$name.cnf" \
    17     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
    18     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
    18 rm -f "$name.cnf"
    19 rm -f "$name.cnf"