src/HOL/Tools/ATP_Manager/SPASS_TPTP
changeset 37962 d7dbe01f48d7
child 37990 586130f71c78
equal deleted inserted replaced
37961:6a48c85a211a 37962:d7dbe01f48d7
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
       
     4 # Isar proof reconstruction)
       
     5 #
       
     6 # Author: Jasmin Blanchette, TU Muenchen
       
     7 
       
     8 options=${@:1:$(($#-1))}
       
     9 name=${@:$(($#)):1}
       
    10 
       
    11 $SPASS_HOME/tptp2dfg $name $name.fof.dfg
       
    12 $SPASS_HOME/SPASS -Flotter $name.fof.dfg \
       
    13     | sed 's/description({$/description({*/' \
       
    14     > $name.cnf.dfg
       
    15 rm -f $name.fof.dfg
       
    16 cat $name.cnf.dfg
       
    17 $SPASS_HOME/SPASS $options $name.cnf.dfg
       
    18 rm -f $name.cnf.dfg