--- a/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 00:01:33 2011 +0200
@@ -12,6 +12,8 @@
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
type 'a problem = 'a ATP_Problem.problem
+ exception UNRECOGNIZED_ATP_PROOF of unit
+
datatype failure =
Unprovable |
IncompleteUnprovable |
@@ -66,6 +68,8 @@
open ATP_Problem
+exception UNRECOGNIZED_ATP_PROOF of unit
+
datatype failure =
Unprovable |
IncompleteUnprovable |
@@ -445,7 +449,7 @@
s |> strip_spaces_except_between_ident_chars
|> raw_explode
|> Scan.finite Symbol.stopper
- (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
+ (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
(Scan.repeat1 (parse_line problem))))
|> fst
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue May 24 00:01:33 2011 +0200
@@ -385,9 +385,9 @@
" -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
^ " -s " ^ the_system system_name system_versions,
proof_delims = union (op =) tstp_proof_delims proof_delims,
- known_failures =
- known_failures @ known_perl_failures @
+ known_failures = known_failures @ known_perl_failures @
[(Unprovable, "says Satisfiable"),
+ (ProofMissing, "says Theorem"),
(IncompleteUnprovable, "says Unknown"),
(IncompleteUnprovable, "says GaveUp"),
(TimedOut, "says Timeout"),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 00:01:33 2011 +0200
@@ -610,6 +610,7 @@
extract_tstplike_proof_and_outcome verbose complete res_code
proof_delims known_failures output
|>> atp_proof_from_tstplike_proof atp_problem
+ handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)
val (conjecture_shape, facts_offset, fact_names,
typed_helpers) =
if is_none outcome then