--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 14 15:10:50 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 14 16:17:20 2010 +0200
@@ -34,8 +34,8 @@
axiom_clauses: (thm * (string * int)) list option,
filtered_clauses: (thm * (string * int)) list option}
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
- MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
+ MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
message: string,
@@ -95,8 +95,8 @@
filtered_clauses: (thm * (string * int)) list option};
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
- MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
+ MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 14 15:10:50 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 14 16:17:20 2010 +0200
@@ -87,6 +87,8 @@
| (failure :: _) => ("", SOME failure)
fun string_for_failure Unprovable = "The ATP problem is unprovable."
+ | string_for_failure IncompleteUnprovable =
+ "The ATP cannot prove the problem."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The ATP ran out of resources."
| string_for_failure OldSpass =
@@ -337,10 +339,11 @@
\-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout),
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
- [(Unprovable, "SPASS beiseite: Completion found"),
+ [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
(TimedOut, "SPASS beiseite: Ran out of time"),
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
- (MalformedInput, "Undefined symbol")],
+ (MalformedInput, "Undefined symbol"),
+ (MalformedInput, "Free Variable")],
max_axiom_clauses = 40,
prefers_theory_relevant = true}
val spass = dfg_prover "spass" spass_config