# HG changeset patch # User paulson # Date 1189091033 -7200 # Node ID 64c20ee76bc103b4c6e4e1bf6da82e8394d59c55 # Parent c90cee3163b76ee571b4ee4946a3e6d3d409a9a8 Vampire structured proofs. Better parsing; some bug fixes. diff -r c90cee3163b7 -r 64c20ee76bc1 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Thu Sep 06 17:03:32 2007 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Thu Sep 06 17:03:53 2007 +0200 @@ -70,7 +70,7 @@ and term x = (quoted >> atom || integer>>Int || truefalse || Symbol.scan_id -- Scan.optional ($$"(" |-- termlist --| $$")") [] >> Br || $$"(" |-- term --| $$")" || - $$"[" |-- termlist --| $$"]" >> listof) x; + $$"[" |-- Scan.optional termlist [] --| $$"]" >> listof) x; fun negate t = Br("c_Not", [t]); fun equate (t1,t2) = Br("c_equal", [t1,t2]); @@ -81,13 +81,13 @@ | syn_equal (t1, SOME (SOME _, t2)) = negate (equate (t1,t2)); (*Literals can involve negation, = and !=.*) -val literal = $$"~" |-- term >> negate || - (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal) ; +fun literal x = ($$"~" |-- literal >> negate || + (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal)) x; val literals = literal -- Scan.repeat ($$"|" |-- literal) >> op:: ; (*Clause: a list of literals separated by the disjunction sign*) -val clause = $$"(" |-- literals --| $$")"; +val clause = $$"(" |-- literals --| $$")" || Scan.single literal; val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist); @@ -435,7 +435,7 @@ stringify_deps thm_names ((lno,lname)::deps_map) lines end; -val proofstart = "\nproof (neg_clausify)\n"; +val proofstart = "proof (neg_clausify)\n"; fun isar_header [] = proofstart | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n"; @@ -452,7 +452,9 @@ app (fn th => Output.debug (fn () => string_of_thm th)) ccls; isar_header (map #1 fixes) ^ String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)) - end; + end + handle e => (*FIXME: exn handler is too general!*) + "Translation of TSTP raised an exception: " ^ Toplevel.exn_message e; (*Could use split_lines, but it can return blank lines...*) val lines = String.tokens (equal #"\n"); @@ -477,16 +479,16 @@ (**** retrieve the axioms that were used in the proof ****) +(*PureThy.get_name_hint returns "??.unknown" if no name is available.*) +fun goodhint x = (x <> "??.unknown"); + (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*) fun get_axiom_names (thm_names: string vector) step_nums = let fun is_axiom n = n <= Vector.length thm_names - fun index i = Vector.sub(thm_names, i-1) - val axnums = List.filter is_axiom step_nums - val axnames = sort_distinct string_ord (map index axnums) + fun getname i = Vector.sub(thm_names, i-1) in - if length axnums = length step_nums then "UNSOUND!!" :: axnames - else axnames - end + sort_distinct string_ord (filter goodhint (map getname (filter is_axiom step_nums))) + end; (*String contains multiple lines. We want those of the form "253[0:Inp] et cetera..." @@ -532,23 +534,21 @@ fun get_axiom_names_vamp proofextract thm_names = get_axiom_names thm_names (get_vamp_linenums proofextract); -fun get_axiom_names E = get_axiom_names_tstp - | get_axiom_names SPASS = get_axiom_names_spass - | get_axiom_names Vampire = get_axiom_names_vamp; +fun get_axiom_names_for E = get_axiom_names_tstp + | get_axiom_names_for SPASS = get_axiom_names_spass + | get_axiom_names_for Vampire = get_axiom_names_vamp; -fun rules_to_metis [] = "metis" - | rules_to_metis xs = "(metis " ^ space_implode " " xs ^ ")" - -fun metis_line atp proofextract thm_names = - "apply " ^ rules_to_metis (get_axiom_names atp proofextract thm_names); +fun metis_line [] = "apply metis" + | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" (*The signal handler in watcher.ML must be able to read the output of this.*) fun lemma_list atp proofextract thm_names probfile toParent ppid = - signal_success probfile toParent ppid (metis_line atp proofextract thm_names); + signal_success probfile toParent ppid + (metis_line (get_axiom_names_for atp proofextract thm_names)); -fun tstp_extract atp proofextract thm_names probfile toParent ppid ctxt th sgno = +fun tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno = let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract)) - val line1 = metis_line atp proofextract thm_names + val line1 = metis_line (get_axiom_names_tstp proofextract thm_names) in signal_success probfile toParent ppid (line1 ^ "\n" ^ decode_tstp_file cnfs ctxt th sgno thm_names) @@ -556,21 +556,17 @@ (**** Extracting proofs from an ATP's output ****) -(*Return everything in s that comes before the string t*) -fun cut_before t s = - let val (s1,s2) = Substring.position t (Substring.full s) - in if Substring.size s2 = 0 then error "cut_before: string not found" - else Substring.string s2 - end; - +val start_TSTP = "SZS output start CNFRefutation" +val end_TSTP = "SZS output end CNFRefutation" val start_E = "# Proof object starts here." val end_E = "# Proof object ends here." -val start_V6 = "%================== Proof: ======================" -val end_V6 = "%============== End of proof. ==================" val start_V8 = "=========== Refutation ==========" val end_V8 = "======= End of refutation =======" +val start_SPASS = "Here is a proof" val end_SPASS = "Formulae used in the proof" +fun any_substring ss ln = exists (fn s => String.isSubstring s ln) ss; + (*********************************************************************************) (* Inspect the output of an ATP process to see if it has found a proof, *) (* and if so, transfer output to the input pipe of the main Isabelle process *) @@ -579,32 +575,24 @@ (*Returns "true" if it successfully returns a lemma list, otherwise "false", but this return value is currently never used!*) fun startTransfer endS (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names) = - let fun transferInput currentString = - (case TextIO.inputLine fromChild of - NONE => (*end of file?*) - (trace ("\n extraction_failed. End bracket: " ^ endS ^ - "\naccumulated text: " ^ currentString); - false) - | SOME thisLine => - if String.isPrefix endS thisLine - then let val proofextract = currentString ^ cut_before endS thisLine - val atp = if endS = end_V8 then Vampire - else if endS = end_SPASS then SPASS - else E - in - trace ("\nExtracted proof:\n" ^ proofextract); + let val atp = if endS = end_V8 then Vampire + else if endS = end_SPASS then SPASS + else E + fun transferInput proofextract = + case TextIO.inputLine fromChild of + NONE => (*end of file?*) + (trace ("\n extraction_failed. End bracket: " ^ endS ^ + "\naccumulated text: " ^ proofextract); + false) + | SOME thisLine => + if any_substring [endS,end_TSTP] thisLine + then + (trace ("\nExtracted proof:\n" ^ proofextract); if String.isPrefix "cnf(" proofextract - then tstp_extract atp proofextract thm_names probfile toParent ppid ctxt th sgno + then tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno else lemma_list atp proofextract thm_names probfile toParent ppid; - true - end - handle e => (*FIXME: exn handler is too general!*) - (trace ("\nstartTransfer: In exception handler: " ^ Toplevel.exn_message e); - TextIO.output (toParent, "Translation failed\n" ^ probfile); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); true) - else transferInput (currentString^thisLine)) + else transferInput (proofextract ^ thisLine) in transferInput "" end @@ -627,10 +615,10 @@ (case TextIO.inputLine fromChild of NONE => (trace "\nNo proof output seen"; false) | SOME thisLine => - if String.isPrefix start_V8 thisLine + if any_substring [start_V8,start_TSTP] thisLine then startTransfer end_V8 arg - else if (String.isPrefix "Satisfiability detected" thisLine) orelse - (String.isPrefix "Refutation not found" thisLine) + else if (String.isSubstring "Satisfiability detected" thisLine) orelse + (String.isSubstring "Refutation not found" thisLine) then (signal_parent (toParent, ppid, "Failure\n", probfile); true) else checkVampProofFound arg); @@ -640,12 +628,12 @@ (case TextIO.inputLine fromChild of NONE => (trace "\nNo proof output seen"; false) | SOME thisLine => - if String.isPrefix start_E thisLine + if any_substring [start_E,start_TSTP] thisLine then startTransfer end_E arg - else if String.isPrefix "# Problem is satisfiable" thisLine + else if String.isSubstring "SZS status: Satisfiable" thisLine then (signal_parent (toParent, ppid, "Invalid\n", probfile); true) - else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine + else if String.isSubstring "SZS status: ResourceOut" thisLine then (signal_parent (toParent, ppid, "Failure\n", probfile); true) else checkEProofFound arg); @@ -655,7 +643,7 @@ (case TextIO.inputLine fromChild of NONE => (trace "\nNo proof output seen"; false) | SOME thisLine => - if String.isPrefix "Here is a proof" thisLine + if any_substring [start_SPASS,start_TSTP] thisLine then startTransfer end_SPASS arg else if thisLine = "SPASS beiseite: Completion found.\n" then (signal_parent (toParent, ppid, "Invalid\n", probfile);