| author | wenzelm |
| Wed, 02 May 2012 21:23:14 +0200 | |
| changeset 47861 | c7144da6abfb |
| parent 47055 | 16e2633f3b4b |
| 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}
|
|
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
46403
diff
changeset
|
10 |
home=${SPASS_OLD_HOME:-$SPASS_HOME}
|
|
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
diff
changeset
|
11 |
|
|
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
46403
diff
changeset
|
12 |
"$home/SPASS" -Flotter "$name" \ |
|
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({*/' \
|
| 44391 | 14 |
| sed 's/set_ClauseFormulaRelation()\.//' \ |
|
45304
e6901aa86a9e
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
blanchet
parents:
45302
diff
changeset
|
15 |
> $name.cnf |
|
e6901aa86a9e
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
blanchet
parents:
45302
diff
changeset
|
16 |
cat $name.cnf |
|
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
46403
diff
changeset
|
17 |
"$home/SPASS" $options "$name.cnf" \ |
|
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/' |
| 46403 | 19 |
rm -f "$name.cnf" |