| author | blanchet |
| Fri, 23 Jul 2010 21:29:29 +0200 | |
| changeset 37962 | d7dbe01f48d7 |
| child 37990 | 586130f71c78 |
| permissions | -rwxr-xr-x |
|
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 |
|
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 |