gracefully handle empty SPASS problems
authorblanchet
Mon Aug 22 15:02:45 2011 +0200 (2011-08-22)
changeset 443917b4104df2be6
parent 44390 99ef9fd7341b
child 44392 6750b4297691
gracefully handle empty SPASS problems
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/scripts/spass
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -290,6 +290,7 @@
     1.4        (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
     1.5        (MalformedInput, "Undefined symbol"),
     1.6        (MalformedInput, "Free Variable"),
     1.7 +      (Unprovable, "No formulae and clauses found in input file"),
     1.8        (SpassTooOld, "tptp2dfg"),
     1.9        (InternalError, "Please report this error")],
    1.10     conj_sym_kind = Hypothesis,
     2.1 --- a/src/HOL/Tools/ATP/scripts/spass	Mon Aug 22 15:02:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/scripts/spass	Mon Aug 22 15:02:45 2011 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  "$SPASS_HOME/tptp2dfg" $name $name.fof.dfg
     2.5  "$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
     2.6      | sed 's/description({$/description({*/' \
     2.7 +    | sed 's/set_ClauseFormulaRelation()\.//' \
     2.8      > $name.cnf.dfg
     2.9  rm -f $name.fof.dfg
    2.10  cat $name.cnf.dfg