author  blanchet 
Mon, 26 Jul 2010 11:19:57 +0200  
changeset 37990  586130f71c78 
parent 37962  d7dbe01f48d7 
permissions  rwxrxrx 
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 Flottergenerated 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 