equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
|
2 # |
|
3 # Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for |
|
4 # Isar proof reconstruction) |
|
5 # |
|
6 # Author: Jasmin Blanchette, TU Muenchen |
|
7 |
|
8 options=${@:1:$(($#-1))} |
|
9 name=${@:$(($#)):1} |
|
10 home=${SPASS_OLD_HOME:-$SPASS_HOME} |
|
11 |
|
12 "$home/SPASS" -Flotter "$name" \ |
|
13 | sed 's/description({$/description({*/' \ |
|
14 | sed 's/set_ClauseFormulaRelation()\.//' \ |
|
15 > $name.cnf |
|
16 cat $name.cnf |
|
17 "$home/SPASS" $options "$name.cnf" \ |
|
18 | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' |
|
19 rm -f "$name.cnf" |
|