1.1 --- a/src/HOL/Tools/res_reconstruct.ML	Tue Jun 30 11:21:02 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Tue Jun 30 11:21:02 2009 +0200
     1.3 @@ -457,9 +457,28 @@
     1.4      in  trace msg; msg  end;
     1.5  
     1.6  
     1.7 -    
     1.8 -  (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
     1.9 -  
    1.10 +  (*=== EXTRACTING PROOF-TEXT === *)
    1.11 +
    1.12 +  val begin_proof_strings = ["# SZS output start CNFRefutation.",
    1.13 +      "=========== Refutation ==========",
    1.14 +  "Here is a proof"];
    1.15 +  val end_proof_strings = ["# SZS output end CNFRefutation",
    1.16 +      "======= End of refutation =======",
    1.17 +  "Formulae used in the proof"];
    1.18 +  fun get_proof_extract proof =
    1.19 +    let
    1.20 +    (*splits to_split by the first possible of a list of splitters*)
    1.21 +    val (begin_string, end_string) =
    1.22 +      (find_first (fn s => String.isSubstring s proof) begin_proof_strings,
    1.23 +      find_first (fn s => String.isSubstring s proof) end_proof_strings)
    1.24 +    in
    1.25 +      if is_none begin_string orelse is_none end_string
    1.26 +      then error "Could not extract proof (no substring indicating a proof)"
    1.27 +      else proof |> first_field (the begin_string) |> the |> snd
    1.28 +                 |> first_field (the end_string) |> the |> fst end;
    1.29 +
    1.30 +(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
    1.31 +
    1.32    val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
    1.33      "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
    1.34    val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
    1.35 @@ -469,31 +488,15 @@
    1.36    fun find_failure proof =
    1.37      let val failures =
    1.38        map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
    1.39 -         (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
    1.40 -    in if null failures then NONE else SOME (hd failures) end;
    1.41 -    
    1.42 -  (*=== EXTRACTING PROOF-TEXT === *)
    1.43 -  
    1.44 -  val begin_proof_strings = ["# SZS output start CNFRefutation.",
    1.45 -      "=========== Refutation ==========",
    1.46 -  "Here is a proof"];
    1.47 -  val end_proof_strings = ["# SZS output end CNFRefutation",
    1.48 -      "======= End of refutation =======",
    1.49 -  "Formulae used in the proof"];
    1.50 -  fun get_proof_extract proof =
    1.51 -    let
    1.52 -    (*splits to_split by the first possible of a list of splitters*)
    1.53 -    fun first_field_any [] to_split = NONE
    1.54 -      | first_field_any (splitter::splitters) to_split =
    1.55 -      let
    1.56 -      val result = (first_field splitter to_split)
    1.57 -      in
    1.58 -        if isSome result then result else first_field_any splitters to_split
    1.59 -      end
    1.60 -    val (a:string, b:string) = valOf (first_field_any begin_proof_strings proof)
    1.61 -    val (proofextract:string, c:string) = valOf (first_field_any end_proof_strings b)
    1.62 -    in proofextract end;
    1.63 -  
    1.64 +        (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
    1.65 +    val correct = null failures andalso
    1.66 +      exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
    1.67 +      exists (fn s => String.isSubstring s proof) end_proof_strings
    1.68 +    in
    1.69 +      if correct then NONE
    1.70 +      else if null failures then SOME "Output of ATP not in proper format"
    1.71 +      else SOME (hd failures) end;
    1.72 +
    1.73    (* === EXTRACTING LEMMAS === *)
    1.74    (* lines have the form "cnf(108, axiom, ...",
    1.75    the number (108) has to be extracted)*)