# HG changeset patch # User paulson # Date 1127320531 -7200 # Node ID c1143a96f6d7e29ab7824023594339338294390e # Parent e93f7510e1e1da0abafd478e5d55564abf0d3c9f improved proof parsing diff -r e93f7510e1e1 -r c1143a96f6d7 src/HOL/Tools/ATP/AtpCommunication.ML --- a/src/HOL/Tools/ATP/AtpCommunication.ML Wed Sep 21 18:35:19 2005 +0200 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML Wed Sep 21 18:35:31 2005 +0200 @@ -44,13 +44,11 @@ o snd o cut_after ":" o snd o cut_after "Here is a proof with" o fst o cut_after " || -> .") s - else if cut_exists start_V8 s then + else if cut_exists end_V8 s then (kill_lines 0 (*Vampire 8.0*) - o snd o cut_after start_V8 o fst o cut_before end_V8) s else if cut_exists end_E s then (kill_lines 0 (*eproof*) - o snd o cut_after start_E o fst o cut_before end_E) s else "??extract_proof failed" (*Couldn't find a proof*) end; @@ -61,124 +59,82 @@ (* and if so, transfer output to the input pipe of the main Isabelle process *) (*********************************************************************************) -fun startTransfer (startS,endS) - (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) = - let val thisLine = TextIO.inputLine fromChild - fun transferInput currentString = +fun startTransfer (endS, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) = + let fun transferInput currentString = let val thisLine = TextIO.inputLine fromChild in if thisLine = "" (*end of file?*) then (File.write (File.tmp_path (Path.basic"extraction_failed")) - ("start bracket: " ^ startS ^ - "\nend bracket: " ^ endS ^ + ("end bracket: " ^ endS ^ "\naccumulated text: " ^ currentString); raise EOF) else if String.isPrefix endS thisLine then let val proofextract = extract_proof (currentString^thisLine) in File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; - Recon_Transfer.prover_lemma_list proofextract goalstring toParent ppid clause_arr + (if endS = end_V8 (*vampire?*) + then Recon_Transfer.vamp_lemma_list + else Recon_Transfer.e_lemma_list) + proofextract goalstring toParent ppid clause_arr end else transferInput (currentString^thisLine) end in - if thisLine = "" then false - else if String.isPrefix startS thisLine - then - (File.append (File.tmp_path (Path.basic "transfer_start")) - ("about to transfer proof, first line is: " ^ thisLine); - transferInput thisLine; - true) handle EOF => false - else - startTransfer (startS,endS) - (fromChild, toParent, ppid, goalstring, - childCmd, clause_arr) - end + transferInput ""; true + end handle EOF => false + +fun signal_parent (toParent, ppid, msg, goalstring) = + (TextIO.output (toParent, msg); + TextIO.output (toParent, goalstring^"\n"); + TextIO.flushOut toParent; + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + (*Space apart signals arising from multiple subgoals*) + Posix.Process.sleep(Time.fromMilliseconds 200)); (*Called from watcher. Returns true if the Vampire process has returned a verdict.*) fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) = - let val proof_file = TextIO.openAppend - (File.platform_path(File.tmp_path (Path.basic "vampire_proof"))) - val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf")) - ("checking if proof found. childCmd is " ^ childCmd ^ - "\ngoalstring is: " ^ goalstring) - val thisLine = TextIO.inputLine fromChild + let val thisLine = TextIO.inputLine fromChild in - File.write (File.tmp_path (Path.basic "vampire_response")) thisLine; + File.append (File.tmp_path (Path.basic "proof")) thisLine; if thisLine = "" - then (TextIO.output (proof_file, "No proof output seen \n"); - TextIO.closeOut proof_file; + then (File.append (File.tmp_path (Path.basic "proof")) + "No proof output seen \n"; false) - else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine + else if String.isPrefix start_V8 thisLine then - startTransfer (start_V8, end_V8) - (fromChild, toParent, ppid, goalstring, - childCmd, clause_arr) + startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) else if (String.isPrefix "Satisfiability detected" thisLine) orelse (String.isPrefix "Refutation not found" thisLine) then - (TextIO.output (toParent, "Failure\n"); - TextIO.output (toParent, goalstring^"\n"); - TextIO.flushOut toParent; - TextIO.output (proof_file, thisLine); - TextIO.closeOut proof_file; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); + (signal_parent (toParent, ppid, "Failure\n", goalstring); true) else - (TextIO.output (proof_file, thisLine); - TextIO.flushOut proof_file; - checkVampProofFound (fromChild, toParent, ppid, - goalstring,childCmd, clause_arr)) + checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) end (*Called from watcher. Returns true if the E process has returned a verdict.*) fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) = - let val E_proof_file = TextIO.openAppend - (File.platform_path(File.tmp_path (Path.basic "e_proof"))) - val _ = File.write (File.tmp_path (Path.basic "e_checking_prf")) - ("checking if proof found. childCmd is " ^ childCmd ^ - "\ngoalstring is: " ^ goalstring) - val thisLine = TextIO.inputLine fromChild + let val thisLine = TextIO.inputLine fromChild in - File.write (File.tmp_path (Path.basic "e_response")) thisLine; + File.append (File.tmp_path (Path.basic "proof")) thisLine; if thisLine = "" - then (TextIO.output (E_proof_file, "No proof output seen \n"); - TextIO.closeOut E_proof_file; - false) - else if thisLine = "# TSTP exit status: Unsatisfiable\n" + then (File.append (File.tmp_path (Path.basic "proof")) + "No proof output seen \n"; + false) + else if String.isPrefix start_E thisLine then - startTransfer (start_E, end_E) - (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) + startTransfer (end_E, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) else if String.isPrefix "# Problem is satisfiable" thisLine then - (TextIO.output (toParent, "Invalid\n"); - TextIO.output (toParent, goalstring^"\n"); - TextIO.flushOut toParent; - TextIO.output (E_proof_file, thisLine); - TextIO.closeOut E_proof_file; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); + (signal_parent (toParent, ppid, "Invalid\n", goalstring); true) else if String.isPrefix "# Failure: Resource limit exceeded" thisLine then (*In fact, E distingishes "out of time" and "out of memory"*) - (File.write (File.tmp_path (Path.basic "e_response")) thisLine; - TextIO.output (toParent, "Failure\n"); - TextIO.output (toParent, goalstring^"\n"); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - TextIO.output (E_proof_file, "signalled parent\n"); - TextIO.closeOut E_proof_file; - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); + (signal_parent (toParent, ppid, "Failure\n", goalstring); true) else - (TextIO.output (E_proof_file, thisLine); - TextIO.flushOut E_proof_file; - checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)) + checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) end @@ -207,7 +163,7 @@ then let val proofextract = extract_proof (currentString^thisLine) in - File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract; + File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; if !reconstruct then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num clause_arr thm; ()) @@ -246,8 +202,6 @@ thm, sg_num, clause_arr) = let val spass_proof_file = TextIO.openAppend (File.platform_path(File.tmp_path (Path.basic "spass_proof"))) - val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf")) - ("checking if proof found, thm is: "^(string_of_thm thm)) val thisLine = TextIO.inputLine fromChild in File.write (File.tmp_path (Path.basic "spass_response")) thisLine; @@ -263,24 +217,14 @@ then (TextIO.output (spass_proof_file, thisLine); TextIO.closeOut spass_proof_file; - TextIO.output (toParent, "Invalid\n"); - TextIO.output (toParent, goalstring^"\n"); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); + signal_parent (toParent, ppid, "Invalid\n", goalstring); true) else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" then - (TextIO.output (toParent, "Failure\n"); - TextIO.output (toParent, goalstring^"\n"); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + (signal_parent (toParent, ppid, "Failure\n", goalstring); TextIO.output (spass_proof_file, "signalled parent\n"); TextIO.closeOut spass_proof_file; - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); true) else (TextIO.output (spass_proof_file, thisLine); diff -r e93f7510e1e1 -r c1143a96f6d7 src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Sep 21 18:35:19 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Sep 21 18:35:31 2005 +0200 @@ -189,7 +189,7 @@ get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr end; - (*String contains multiple lines, terminated with newline characters. + (*String contains multiple lines. A list consisting of the first number in each line is returned. *) fun get_linenums proofstr = let val numerics = String.tokens (not o Char.isDigit) @@ -198,9 +198,22 @@ val lines = String.tokens (fn c => c = #"\n") proofstr in List.mapPartial (firstno o numerics) lines end -fun get_axiom_names_vamp_E proofstr clause_arr = +fun get_axiom_names_e proofstr clause_arr = get_axiom_names (get_linenums proofstr) clause_arr; + (*String contains multiple lines. We want those of the form + "*********** [448, input] ***********". + A list consisting of the first number in each line is returned. *) +fun get_vamp_linenums proofstr = + let val toks = String.tokens (not o Char.isAlphaNum) + fun inputno [n,"input"] = Int.fromString n + | inputno _ = NONE + val lines = String.tokens (fn c => c = #"\n") proofstr + in List.mapPartial (inputno o toks) lines end + +fun get_axiom_names_vamp proofstr clause_arr = + get_axiom_names (get_vamp_linenums proofstr) clause_arr; + (***********************************************) (* get axioms for reconstruction *) @@ -303,7 +316,9 @@ (* Attempt to prevent several signals from turning up simultaneously *) Posix.Process.sleep(Time.fromSeconds 1); ()); -val prover_lemma_list = prover_lemma_list_aux get_axiom_names_vamp_E; +val e_lemma_list = prover_lemma_list_aux get_axiom_names_e; + +val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp; val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;