Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gracefully handle empty SPASS problems
authorblanchet
Mon, 22 Aug 2011 15:02:45 +0200
changeset 44391 7b4104df2be6
parent 44390 99ef9fd7341b
child 44392 6750b4297691
gracefully handle empty SPASS problems
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/ATP/scripts/spass file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -290,6 +290,7 @@
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
+      (Unprovable, "No formulae and clauses found in input file"),
       (SpassTooOld, "tptp2dfg"),
       (InternalError, "Please report this error")],
    conj_sym_kind = Hypothesis,
--- a/src/HOL/Tools/ATP/scripts/spass	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/scripts/spass	Mon Aug 22 15:02:45 2011 +0200
@@ -11,6 +11,7 @@
 "$SPASS_HOME/tptp2dfg" $name $name.fof.dfg
 "$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
     | sed 's/description({$/description({*/' \
+    | sed 's/set_ClauseFormulaRelation()\.//' \
     > $name.cnf.dfg
 rm -f $name.fof.dfg
 cat $name.cnf.dfg
isabelle