author  blanchet 
Fri, 23 Jul 2010 21:29:29 +0200  
changeset 37962  d7dbe01f48d7 
child 37990  586130f71c78 
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 
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff
changeset

17 
$SPASS_HOME/SPASS $options $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.cnf.dfg 