src/HOL/Tools/ATP/scripts/spass
author blanchet
Wed, 28 Jul 2010 19:01:34 +0200
changeset 38046 6659c15e7421
parent 38041 src/HOL/Tools/ATP_Manager/scripts/spass@3b80d6082131
child 41456 006d85ad56d3
permissions -rwxr-xr-x
rename directory
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
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    11
$SPASS_HOME/tptp2dfg $name $name.fof.dfg
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    12
$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    13
    | sed 's/description({$/description({*/' \
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    14
    > $name.cnf.dfg
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff changeset
    15
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
    16
cat $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
    17
$SPASS_HOME/SPASS $options $name.cnf.dfg \
586130f71c78 remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS)
blanchet
parents: 37962
diff changeset
    18
    | 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
    19
rm -f $name.cnf.dfg