author blanchet
Fri, 23 Jul 2010 21:29:29 +0200
changeset 37962 d7dbe01f48d7
child 37990 586130f71c78
permissions -rwxr-xr-x
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; this is rather involved because the Flotter FOF-to-CNF translator is normally implicit. We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.

#!/usr/bin/env bash
# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
# Isar proof reconstruction)
# Author: Jasmin Blanchette, TU Muenchen


$SPASS_HOME/tptp2dfg $name $name.fof.dfg
$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
    | sed 's/description({$/description({*/' \
    > $name.cnf.dfg
rm -f $name.fof.dfg
cat $name.cnf.dfg
$SPASS_HOME/SPASS $options $name.cnf.dfg
rm -f $name.cnf.dfg