author  wenzelm 
Fri, 07 Jan 2011 23:10:33 +0100  
changeset 41456  006d85ad56d3 
parent 38046  6659c15e7421 
child 44391  7b4104df2be6 
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 

41456  11 
"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg 
12 
"$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

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 
41456  17 
"$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

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 