src/HOL/Tools/ATP/scripts/spass
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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
     1
#!/usr/bin/env bash
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
     2
#
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
     3
# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
     4
# Isar proof reconstruction)
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
     5
#
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
     6
# Author: Jasmin Blanchette, TU Muenchen
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
     7
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
     8
options=${@:1:$(($#-1))}
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
     9
name=${@:$(($#)):1}
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    10
45302
04c87dec70b8 gracefully do nothing if the SPASS input file is already in DFG format
blanchet
parents: 44391
diff changeset
    11
# Try converting the file from TPTP to DFG, but fail gracefully if it is already
04c87dec70b8 gracefully do nothing if the SPASS input file is already in DFG format
blanchet
parents: 44391
diff changeset
    12
# in DFG format.
04c87dec70b8 gracefully do nothing if the SPASS input file is already in DFG format
blanchet
parents: 44391
diff changeset
    13
"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg || cp $name $name.fof.dfg
41456
006d85ad56d3 allow spaces in $SPASS_HOME value;
wenzelm
parents: 38046
diff changeset
    14
"$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    15
    | sed 's/description({$/description({*/' \
44391
7b4104df2be6 gracefully handle empty SPASS problems
blanchet
parents: 41456
diff changeset
    16
    | sed 's/set_ClauseFormulaRelation()\.//' \
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    17
    > $name.cnf.dfg
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    18
rm -f $name.fof.dfg
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    19
cat $name.cnf.dfg
41456
006d85ad56d3 allow spaces in $SPASS_HOME value;
wenzelm
parents: 38046
diff changeset
    20
"$SPASS_HOME/SPASS" $options $name.cnf.dfg \
37990
586130f71c78 remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS)
blanchet
parents: 37962
diff changeset
    21
    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    22
rm -f $name.cnf.dfg