# HG changeset patch # User paulson # Date 1127135533 -7200 # Node ID f6a225f97f0a74e214c7d3810750f76c38d05697 # Parent c6005bfc1630eecc6ffad2f3b92e81a8c4ae6b75 simplification of the Isabelle-ATP code; hooks for batch generation of problems diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Sep 19 14:20:45 2005 +0200 +++ b/src/HOL/IsaMakefile Mon Sep 19 15:12:13 2005 +0200 @@ -93,8 +93,7 @@ Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy \ ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy \ Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML \ - Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML \ - Tools/ATP/VampCommunication.ML \ + Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML \ Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML \ Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML \ Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML \ diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Reconstruction.thy --- a/src/HOL/Reconstruction.thy Mon Sep 19 14:20:45 2005 +0200 +++ b/src/HOL/Reconstruction.thy Mon Sep 19 15:12:13 2005 +0200 @@ -20,8 +20,7 @@ "Tools/ATP/recon_translate_proof.ML" "Tools/ATP/recon_parse.ML" "Tools/ATP/recon_transfer_proof.ML" - "Tools/ATP/VampCommunication.ML" - "Tools/ATP/SpassCommunication.ML" + "Tools/ATP/AtpCommunication.ML" "Tools/ATP/watcher.ML" "Tools/ATP/res_clasimpset.ML" "Tools/res_atp.ML" diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Tools/ATP/AtpCommunication.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML Mon Sep 19 15:12:13 2005 +0200 @@ -0,0 +1,311 @@ +(* Title: VampCommunication.ml + ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) + +(***************************************************************************) +(* Code to deal with the transfer of proofs from a Vampire process *) +(***************************************************************************) +signature ATP_COMMUNICATION = + sig + val reconstruct : bool ref + val checkEProofFound: + TextIO.instream * TextIO.outstream * Posix.Process.pid * + string * string * thm * int * (ResClause.clause * thm) Array.array -> bool + val checkVampProofFound: + TextIO.instream * TextIO.outstream * Posix.Process.pid * + string * string * thm * int * (ResClause.clause * thm) Array.array -> bool + val checkSpassProofFound: + TextIO.instream * TextIO.outstream * Posix.Process.pid * + string * string * thm * int * (ResClause.clause * thm) Array.array -> bool + end; + +structure AtpCommunication : ATP_COMMUNICATION = +struct + +(* switch for whether to reconstruct a proof found, or just list the lemmas used *) +val reconstruct = ref false; + +exception EOF; + +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 =======" + +(*Identifies the start/end lines of an ATP's output*) +local open Recon_Parse in +fun extract_proof s = + if cut_exists "Here is a proof with" s then + (kill_lines 0 + 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 + (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; + +(**********************************************************************) +(* Reconstruct the Vampire/E proof w.r.t. thmstring (string version of *) +(* Isabelle goal to be proved), then transfer the reconstruction *) +(* steps as a string to the input pipe of the main Isabelle process *) +(**********************************************************************) + +fun reconstruct_tac proofextract goalstring toParent ppid sg_num clause_arr = + SELECT_GOAL + (EVERY1 + [rtac ccontr, ResLib.atomize_tac, skolemize_tac, + METAHYPS(fn negs => + (Recon_Transfer.prover_lemma_list proofextract + goalstring toParent ppid negs clause_arr))]) sg_num + + +(*********************************************************************************) +(* 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 *) +(*********************************************************************************) + +fun startTransfer (startS,endS) + (fromChild, toParent, ppid, goalstring, childCmd, thm, sg_num, clause_arr) = + let val thisLine = TextIO.inputLine fromChild + 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 ^ + "\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; + reconstruct_tac proofextract goalstring toParent ppid sg_num + clause_arr thm + 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, thm is: " ^ string_of_thm thm); + transferInput thisLine; + true) handle EOF => false + else + startTransfer (startS,endS) + (fromChild, toParent, ppid, goalstring, + childCmd, thm, sg_num,clause_arr) + end + +(*Called from watcher. Returns true if the Vampire process has returned a verdict.*) +fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, + thm, sg_num, 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, thm is: " ^ string_of_thm thm) + val thisLine = TextIO.inputLine fromChild + in + File.write (File.tmp_path (Path.basic "vampire_response")) thisLine; + if thisLine = "" + then (TextIO.output (proof_file, "No proof output seen \n"); + TextIO.closeOut proof_file; + false) + else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine + then + startTransfer (start_V8, end_V8) + (fromChild, toParent, ppid, goalstring, + childCmd, thm, sg_num, 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); + true) + else + (TextIO.output (proof_file, thisLine); + TextIO.flushOut proof_file; + checkVampProofFound (fromChild, toParent, ppid, + goalstring,childCmd, thm, sg_num, clause_arr)) + end + + +(*Called from watcher. Returns true if the E process has returned a verdict.*) +fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, + thm, sg_num, 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 ^ + "\nthm is: " ^ string_of_thm thm) + val thisLine = TextIO.inputLine fromChild + in + File.write (File.tmp_path (Path.basic "e_response")) 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 + startTransfer (start_E, end_E) + (fromChild, toParent, ppid, goalstring, + childCmd, thm, sg_num, 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); + 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); + true) + else + (TextIO.output (E_proof_file, thisLine); + TextIO.flushOut E_proof_file; + checkEProofFound (fromChild, toParent, ppid, goalstring, + childCmd, thm, sg_num, clause_arr)) + end + + +(**********************************************************************) +(* Reconstruct the Spass proof w.r.t. thmstring (string version of *) +(* Isabelle goal to be proved), then transfer the reconstruction *) +(* steps as a string to the input pipe of the main Isabelle process *) +(**********************************************************************) + +fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num + clause_arr = + let val f = if !reconstruct then Recon_Transfer.spass_reconstruct + else Recon_Transfer.spass_lemma_list + in + SELECT_GOAL + (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, + METAHYPS(fn negs => + f proofextract goalstring toParent ppid negs clause_arr)]) sg_num + end; + + +fun transferSpassInput (fromChild, toParent, ppid, goalstring, + currentString, thm, sg_num, clause_arr) = + let val thisLine = TextIO.inputLine fromChild + in + if thisLine = "" (*end of file?*) + then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString; + raise EOF) + else if thisLine = "--------------------------SPASS-STOP------------------------------\n" + then + let val proofextract = extract_proof (currentString^thisLine) + in + File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract; + spass_reconstruct_tac proofextract goalstring toParent ppid sg_num + clause_arr thm + end + else transferSpassInput (fromChild, toParent, ppid, goalstring, + (currentString^thisLine), thm, sg_num, clause_arr) + end; + + +(*********************************************************************************) +(* Inspect the output of a Spass process to see if it has found a proof, *) +(* and if so, transfer output to the input pipe of the main Isabelle process *) +(*********************************************************************************) + + +fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd, + thm, sg_num,clause_arr) = + let val thisLine = TextIO.inputLine fromChild + in + if thisLine = "" then false + else if String.isPrefix "Here is a proof" thisLine then + (File.append (File.tmp_path (Path.basic "spass_transfer")) + ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n"); + transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, + thm, sg_num,clause_arr); + true) handle EOF => false + else startSpassTransfer (fromChild, toParent, ppid, goalstring, + childCmd, thm, sg_num,clause_arr) + end + + +(*Called from watcher. Returns true if the E process has returned a verdict.*) +fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd, + 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; + if thisLine = "" + then (TextIO.output (spass_proof_file, ("No proof output seen \n")); + TextIO.closeOut spass_proof_file; + false) + else if thisLine = "SPASS beiseite: Proof found.\n" + then + startSpassTransfer (fromChild, toParent, ppid, goalstring, + childCmd, thm, sg_num, clause_arr) + else if thisLine = "SPASS beiseite: Completion found.\n" + 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); + 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); + 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); + TextIO.flushOut spass_proof_file; + checkSpassProofFound (fromChild, toParent, ppid, goalstring, + childCmd, thm, sg_num, clause_arr)) + end + +end; diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Tools/ATP/SpassCommunication.ML --- a/src/HOL/Tools/ATP/SpassCommunication.ML Mon Sep 19 14:20:45 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,176 +0,0 @@ -(* Title: SpassCommunication.ml - ID: $Id$ - Author: Claire Quigley - Copyright 2004 University of Cambridge -*) - -(***************************************************************************) -(* Code to deal with the transfer of proofs from a Spass process *) -(***************************************************************************) -signature SPASS_COMM = - sig - val reconstruct : bool ref - val getSpassInput : TextIO.instream -> string * string - val checkSpassProofFound: - TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool - end; - -structure SpassComm : SPASS_COMM = -struct - -(* switch for whether to reconstruct a proof found, or just list the lemmas used *) -val reconstruct = ref false; - -exception EOF; - -(**********************************************************************) -(* Reconstruct the Spass proof w.r.t. thmstring (string version of *) -(* Isabelle goal to be proved), then transfer the reconstruction *) -(* steps as a string to the input pipe of the main Isabelle process *) -(**********************************************************************) - -fun reconstruct_tac proofextract goalstring toParent ppid sg_num - clause_arr num_of_clauses = - let val f = if !reconstruct then Recon_Transfer.spassString_to_reconString - else Recon_Transfer.spassString_to_lemmaString - in - SELECT_GOAL - (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, - METAHYPS(fn negs => - f proofextract goalstring toParent ppid negs clause_arr num_of_clauses)]) sg_num - end; - - -fun transferSpassInput (fromChild, toParent, ppid, goalstring, - currentString, thm, sg_num,clause_arr, num_of_clauses) = - let val thisLine = TextIO.inputLine fromChild - in - if thisLine = "" (*end of file?*) - then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString; - raise EOF) - else if thisLine = "--------------------------SPASS-STOP------------------------------\n" - then - let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) - in - File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract; - reconstruct_tac proofextract goalstring toParent ppid sg_num - clause_arr num_of_clauses thm - end - else transferSpassInput (fromChild, toParent, ppid, goalstring, - (currentString^thisLine), thm, sg_num, clause_arr, - num_of_clauses) - end; - - -(*********************************************************************************) -(* Inspect the output of a Spass process to see if it has found a proof, *) -(* and if so, transfer output to the input pipe of the main Isabelle process *) -(*********************************************************************************) - - -fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd, - thm, sg_num,clause_arr, num_of_clauses) = - let val thisLine = TextIO.inputLine fromChild - in - if thisLine = "" then false - else if String.isPrefix "Here is a proof" thisLine then - (File.append (File.tmp_path (Path.basic "spass_transfer")) - ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n"); - transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, - thm, sg_num,clause_arr, num_of_clauses); - true) handle EOF => false - else startSpassTransfer (fromChild, toParent, ppid, goalstring, - childCmd, thm, sg_num,clause_arr, num_of_clauses) - end - - -fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd, - thm, sg_num, clause_arr, (num_of_clauses:int )) = - 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 - if thisLine = "" - then (TextIO.output (spass_proof_file, ("No proof output seen \n")); - TextIO.closeOut spass_proof_file; - false) - else if thisLine = "SPASS beiseite: Proof found.\n" - then - (File.write (File.tmp_path (Path.basic "spass_response")) thisLine; - startSpassTransfer (fromChild, toParent, ppid, goalstring, - childCmd, thm, sg_num, clause_arr, num_of_clauses)) - else if thisLine = "SPASS beiseite: Completion found.\n" - then - (File.write (File.tmp_path (Path.basic "spass_response")) thisLine; - TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent; - TextIO.output (spass_proof_file, thisLine); - TextIO.flushOut spass_proof_file; - TextIO.closeOut spass_proof_file; - - TextIO.output (toParent, thisLine^"\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); - true) - else if thisLine = "SPASS beiseite: Ran out of time.\n" - then - (File.write (File.tmp_path (Path.basic "spass_response")) thisLine; - TextIO.output (toParent, thisLine^"\n"); - TextIO.output (toParent, goalstring^"\n"); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - 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 if thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" - then - (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent; - TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; - true) - else - (TextIO.output (spass_proof_file, thisLine); - TextIO.flushOut spass_proof_file; - checkSpassProofFound (fromChild, toParent, ppid, goalstring, - childCmd, thm, sg_num, clause_arr, num_of_clauses)) - end - - -(***********************************************************************) -(* Function used by the Isabelle process to read in a spass proof *) -(***********************************************************************) - -fun getSpassInput instr = - let val thisLine = TextIO.inputLine instr - val _ = File.write (File.tmp_path (Path.basic "spass_line")) thisLine - in - if thisLine = "" then ("No output from reconstruction process.\n","") - else if String.sub (thisLine, 0) = #"[" orelse - String.isPrefix "SPASS beiseite:" thisLine orelse - String.isPrefix "Rules from" thisLine - then - let val goalstring = TextIO.inputLine instr - in (thisLine, goalstring) end - else if substring (thisLine,0,5) = "Proof" orelse - String.sub (thisLine, 0) = #"%" - then - let val goalstring = TextIO.inputLine instr - in - File.write (File.tmp_path (Path.basic "getSpassInput")) thisLine; - (thisLine, goalstring) - end - else getSpassInput instr - end - - -end; diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Tools/ATP/VampCommunication.ML --- a/src/HOL/Tools/ATP/VampCommunication.ML Mon Sep 19 14:20:45 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,236 +0,0 @@ -(* Title: VampCommunication.ml - ID: $Id$ - Author: Claire Quigley - Copyright 2004 University of Cambridge -*) - -(***************************************************************************) -(* Code to deal with the transfer of proofs from a Vampire process *) -(***************************************************************************) -signature VAMP_COMM = - sig - val getEInput : TextIO.instream -> string * string - val checkEProofFound: - TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool - - val getVampInput : TextIO.instream -> string * string - val checkVampProofFound: - TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool - end; - -structure VampComm : VAMP_COMM = -struct - -exception EOF; - -(**********************************************************************) -(* Reconstruct the Vampire/E proof w.r.t. thmstring (string version of *) -(* Isabelle goal to be proved), then transfer the reconstruction *) -(* steps as a string to the input pipe of the main Isabelle process *) -(**********************************************************************) - -fun reconstruct_tac proofextract goalstring toParent ppid sg_num - clause_arr num_of_clauses = - SELECT_GOAL - (EVERY1 - [rtac ccontr, ResLib.atomize_tac, skolemize_tac, - METAHYPS(fn negs => - (Recon_Transfer.proverString_to_lemmaString proofextract - goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num - - -(*********************************************************************************) -(* 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 *) -(*********************************************************************************) - -fun startTransfer (startS,endS) - (fromChild, toParent, ppid, goalstring,childCmd, - thm, sg_num,clause_arr, num_of_clauses) = - let val thisLine = TextIO.inputLine fromChild - 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 ^ - "\naccumulated text: " ^ currentString); - raise EOF) - else if String.isPrefix endS thisLine - then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) - in - File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; - reconstruct_tac proofextract goalstring toParent ppid sg_num - clause_arr num_of_clauses thm - 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, thm is: " ^ string_of_thm thm); - transferInput thisLine; - true) handle EOF => false - else - startTransfer (startS,endS) - (fromChild, toParent, ppid, goalstring, - childCmd, thm, sg_num,clause_arr, num_of_clauses) - end - - -fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, - thm, sg_num, clause_arr, num_of_clauses) = - let val proof_file = TextIO.openAppend - (File.platform_path(File.tmp_path (Path.basic "atp_proof"))) - val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf")) - ("checking if proof found, thm is: " ^ string_of_thm thm) - val thisLine = TextIO.inputLine fromChild - in - if thisLine = "" - then (TextIO.output (proof_file, "No proof output seen \n"); - TextIO.closeOut proof_file; - false) - else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine - then - (File.write (File.tmp_path (Path.basic "atp_response")) thisLine; - startTransfer (Recon_Parse.start_V8, Recon_Parse.end_V8) - (fromChild, toParent, ppid, goalstring, - childCmd, thm, sg_num, clause_arr, num_of_clauses)) - else if (String.isPrefix "Satisfiability detected" thisLine) orelse - (String.isPrefix "Refutation not found" thisLine) - then - (File.write (File.tmp_path (Path.basic "atp_response")) thisLine; - TextIO.output (toParent,childCmd^"\n"); - TextIO.flushOut toParent; - TextIO.output (proof_file, thisLine); - TextIO.closeOut proof_file; - - TextIO.output (toParent, thisLine^"\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); - true) - else - (TextIO.output (proof_file, thisLine); - TextIO.flushOut proof_file; - checkVampProofFound (fromChild, toParent, ppid, - goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)) - end - - -fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, - thm, sg_num, clause_arr, num_of_clauses) = - let val E_proof_file = TextIO.openAppend - (File.platform_path(File.tmp_path (Path.basic "atp_proof"))) - val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf")) - ("checking if proof found, thm is: " ^ string_of_thm thm) - val thisLine = TextIO.inputLine fromChild - in - 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.write (File.tmp_path (Path.basic "atp_response")) thisLine; - startTransfer (Recon_Parse.start_E, Recon_Parse.end_E) - (fromChild, toParent, ppid, goalstring, - childCmd, thm, sg_num, clause_arr, num_of_clauses)) - else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n" - then - (File.write (File.tmp_path (Path.basic "atp_response")) thisLine; - TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent; - TextIO.output (E_proof_file, thisLine); - TextIO.closeOut E_proof_file; - - TextIO.output (toParent, thisLine^"\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); - true) - else if thisLine = "# Failure: Resource limit exceeded (time)\n" - then - (File.write (File.tmp_path (Path.basic "atp_response")) thisLine; - TextIO.output (toParent, thisLine^"\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); - true) - else if thisLine = "# Failure: Resource limit exceeded (memory)\n" - then - (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - TextIO.output (toParent,childCmd^"\n" ); - TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; - true) - else - (TextIO.output (E_proof_file, thisLine); - TextIO.flushOut E_proof_file; - checkEProofFound (fromChild, toParent, ppid, goalstring, - childCmd, thm, sg_num, clause_arr, num_of_clauses)) - end - - -(***********************************************************************) -(* Function used by the Isabelle process to read in a Vampire proof *) -(***********************************************************************) - -fun getVampInput instr = - let val thisLine = TextIO.inputLine instr - val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine - in (* reconstructed proof string *) - if thisLine = "" then ("No output from reconstruction process.\n","") - else if String.sub (thisLine, 0) = #"[" orelse (*FIXME: for SPASS?*) - String.isPrefix "Satisfiability detected" thisLine orelse - String.isPrefix "Refutation not found" thisLine orelse - String.isPrefix "Rules from" thisLine - then - let val goalstring = TextIO.inputLine instr - in (thisLine, goalstring) end - else if thisLine = "Proof found but translation failed!" - then - let val goalstring = TextIO.inputLine instr - val _ = debug "getVampInput: translation of proof failed" - in (thisLine, goalstring) end - else getVampInput instr - end - - -(***********************************************************************) -(* Function used by the Isabelle process to read in an E proof *) -(***********************************************************************) - -fun getEInput instr = - let val thisLine = TextIO.inputLine instr - val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine - in (* reconstructed proof string *) - if thisLine = "" then ("No output from reconstruction process.\n","") - else if String.isPrefix "# Problem is satisfiable" thisLine orelse - String.isPrefix "# Cannot determine problem status" thisLine orelse - String.isPrefix "# Failure:" thisLine - then - let val goalstring = TextIO.inputLine instr - in (thisLine, goalstring) end - else if thisLine = "Proof found but translation failed!" - then - let val goalstring = TextIO.inputLine instr - val _ = debug "getEInput: translation of proof failed" - in (thisLine, goalstring) end - else getEInput instr - end - -end; diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Tools/ATP/recon_parse.ML --- a/src/HOL/Tools/ATP/recon_parse.ML Mon Sep 19 14:20:45 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_parse.ML Mon Sep 19 15:12:13 2005 +0200 @@ -66,9 +66,6 @@ fun finished input = if input = [] then (0, input) else raise Noparse; - - - (* Parsing the output from gandalf *) datatype token = Word of string | Number of int @@ -105,39 +102,6 @@ fun kill_lines 0 = Library.I | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n"; - (*fun extract_proof s - = if cut_exists "EMPTY CLAUSE DERIVED" s then - (kill_lines 6 - o snd o cut_after "EMPTY CLAUSE DERIVED" - o fst o cut_after "contradiction.\n") s - else - raise (GandalfError "Couldn't find a proof.") -*) - -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 =======" - - -(*Identifies the start/end lines of an ATP's output*) -fun extract_proof s = - if cut_exists "Here is a proof with" s then - (kill_lines 0 - 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 - (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*) fun several p = many (some p) fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "") @@ -163,17 +127,6 @@ fun lex s = alltokens (explode s) - -(*String contains multiple lines, terminated with newline characters. - 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) - fun firstno [] = NONE - | firstno (x::xs) = Int.fromString x - val lines = String.tokens (fn c => c = #"\n") proofstr - in List.mapPartial (firstno o numerics) lines end - - (************************************************************) (**************************************************) diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Sep 19 14:20:45 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Sep 19 15:12:13 2005 +0200 @@ -39,12 +39,10 @@ (*| proofstep_to_string (Rewrite((a,b),(c,d))) = "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*) -fun list_to_string [] liststr = liststr -| list_to_string (x::[]) liststr = liststr^(string_of_int x) -| list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",") - -fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]" +fun proof_to_string (num,(step,clause_strs, thmvars)) = + (string_of_int num)^(proofstep_to_string step)^ + "["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]" fun proofs_to_string [] str = str @@ -55,7 +53,9 @@ -fun init_proofstep_to_string (num, step, clause_strs) = (string_of_int num)^" "^(proofstep_to_string step)^" "^(clause_strs_to_string clause_strs "")^" " +fun init_proofstep_to_string (num, step, clause_strs) = + (string_of_int num)^" "^(proofstep_to_string step)^" "^ + (clause_strs_to_string clause_strs "")^" " fun init_proofsteps_to_string [] str = str | init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x @@ -144,12 +144,11 @@ (* retrieve the axioms that were obtained from the clasimpset *) -fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) clasimp_num step_nums = - let val realnums = map subone step_nums - val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums -(* val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums"))) - val _ = TextIO.output(axnums,(numstr clasimp_nums)) - val _ = TextIO.closeOut(axnums)*) +fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) step_nums = + let val clasimp_nums = List.filter (is_clasimp_ax (Array.length clause_arr - 1)) + (map subone step_nums) +(* val _ = File.write (File.tmp_path (Path.basic "axnums")) + (numstr clasimp_nums) *) in map (fn x => Array.sub(clause_arr, x)) clasimp_nums end @@ -159,7 +158,7 @@ (* get names of clasimp axioms used *) (*****************************************************) - fun get_axiom_names step_nums thms clause_arr num_of_clauses = + fun get_axiom_names step_nums thms clause_arr = let (* not sure why this is necessary again, but seems to be *) val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) @@ -168,7 +167,7 @@ (* here need to add the clauses from clause_arr*) (***********************************************) - val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums + val clasimp_names_cls = get_clasimp_cls clause_arr step_nums val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls val _ = File.write (File.tmp_path (Path.basic "clasimp_names")) (concat clasimp_names) @@ -178,20 +177,30 @@ end -fun get_axiom_names_spass proofstr thms clause_arr num_of_clauses = +fun get_axiom_names_spass proofstr thms clause_arr = let (* parse spass proof into datatype *) + val _ = File.write (File.tmp_path (Path.basic "parsing_progress")) + ("Started parsing:\n" ^ proofstr) val tokens = #1(lex proofstr) val proof_steps = parse tokens - val _ = File.write (File.tmp_path (Path.basic "parsing_done")) - ("Did parsing on "^proofstr) + val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!" (* get axioms as correctly numbered clauses w.r.t. the Spass proof *) in get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) - thms clause_arr num_of_clauses + thms clause_arr end; - fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses = - get_axiom_names (get_linenums proofstr) thms clause_arr num_of_clauses; + (*String contains multiple lines, terminated with newline characters. + 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) + fun firstno [] = NONE + | firstno (x::xs) = Int.fromString x + val lines = String.tokens (fn c => c = #"\n") proofstr + in List.mapPartial (firstno o numerics) lines end + +fun get_axiom_names_vamp_E proofstr thms clause_arr = + get_axiom_names (get_linenums proofstr) thms clause_arr; (***********************************************) @@ -206,13 +215,13 @@ fun addvars c (a,b) = (a,b,c) -fun get_axioms_used proof_steps thms clause_arr num_of_clauses = +fun get_axioms_used proof_steps thms clause_arr = let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) val axioms = (List.filter is_axiom) proof_steps val step_nums = get_step_nums axioms [] - val clauses =(*(clasimp_cls)@*)( make_clauses thms) + val clauses = make_clauses thms (*FIXME: must this be repeated??*) val vars = map thm_vars clauses @@ -265,19 +274,19 @@ val restore_linebreaks = subst_for #"\t" #"\n"; -fun proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms clause_arr num_of_clauses getax = - let val _ = File.append(File.tmp_path (Path.basic "spass_lemmastring")) +fun prover_lemma_list_aux proofstr goalstring toParent ppid thms clause_arr getax = + let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring")) ("proofstr is " ^ proofstr ^ "\ngoalstr is " ^ goalstring ^ - "\nnum of clauses is " ^ string_of_int num_of_clauses) + "\nnum of clauses is " ^ string_of_int (Array.length clause_arr)) - val axiom_names = getax proofstr thms clause_arr num_of_clauses - val ax_str = "Rules from clasimpset used in automatic proof: " ^ - rules_to_string axiom_names + val axiom_names = getax proofstr thms clause_arr + val ax_str = rules_to_string axiom_names in - File.append(File.tmp_path (Path.basic "spass_lemmastring")) - ("reconstring is: "^ax_str^" "^goalstring); - TextIO.output (toParent, ax_str^"\n"); + File.append(File.tmp_path (Path.basic "prover_lemmastring")) + ("\nlemma list is: " ^ ax_str); + TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^ + ax_str ^ "\n"); TextIO.output (toParent, "goalstring: "^goalstring^"\n"); TextIO.flushOut toParent; @@ -285,9 +294,10 @@ (* Attempt to prevent several signals from turning up simultaneously *) Posix.Process.sleep(Time.fromSeconds 1) ; all_tac end - handle _ => (*FIXME: exn handler is too general!*) - (File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler"; - TextIO.output (toParent, "Proof found but translation failed : " ^ + handle exn => (*FIXME: exn handler is too general!*) + (File.write(File.tmp_path (Path.basic "proverString_handler")) + ("In exception handler: " ^ Toplevel.exn_message exn); + TextIO.output (toParent, "Translation failed for the proof: " ^ remove_linebreaks proofstr ^ "\n"); TextIO.output (toParent, remove_linebreaks goalstring ^ "\n"); TextIO.flushOut toParent; @@ -295,21 +305,19 @@ (* Attempt to prevent several signals from turning up simultaneously *) Posix.Process.sleep(Time.fromSeconds 1); all_tac); -fun proverString_to_lemmaString proofstr goalstring toParent ppid thms - clause_arr num_of_clauses = - proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms - clause_arr num_of_clauses get_axiom_names_vamp_E; +fun prover_lemma_list proofstr goalstring toParent ppid thms clause_arr = + prover_lemma_list_aux proofstr goalstring toParent ppid thms + clause_arr get_axiom_names_vamp_E; -fun spassString_to_lemmaString proofstr goalstring toParent ppid thms - clause_arr num_of_clauses = - proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms - clause_arr num_of_clauses get_axiom_names_spass; +fun spass_lemma_list proofstr goalstring toParent ppid thms clause_arr = + prover_lemma_list_aux proofstr goalstring toParent ppid thms + clause_arr get_axiom_names_spass; (**** Full proof reconstruction for SPASS (not really working) ****) -fun spassString_to_reconString proofstr goalstring toParent ppid thms clause_arr num_of_clauses = - let val _ = File.write(File.tmp_path (Path.basic "spass_reconstruction")) +fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr = + let val _ = File.write(File.tmp_path (Path.basic "prover_reconstruction")) ("proofstr is: "^proofstr) val tokens = #1(lex proofstr) @@ -318,7 +326,7 @@ (***********************************) val proof_steps = parse tokens - val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) + val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) ("Did parsing on "^proofstr) (************************************) @@ -329,19 +337,19 @@ (* subgoal this is, and turn it into meta_clauses *) (* should prob add array and table here, so that we can get axioms*) (* produced from the clasimpset rather than the problem *) - val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses + val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr (*val numcls_string = numclstr ( vars, numcls) ""*) - val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) "got axioms" + val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) "got axioms" (************************************) (* translate proof *) (************************************) - val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) + val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) ("about to translate proof, steps: " ^(init_proofsteps_to_string proof_steps "")) val (newthm,proof) = translate_proof numcls proof_steps vars - val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) + val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")) (***************************************************) (* transfer necessary steps as strings to Isabelle *) @@ -371,9 +379,10 @@ (* Attempt to prevent several signals from turning up simultaneously *) Posix.Process.sleep(Time.fromSeconds 1) ; all_tac end - handle _ => - (File.append(File.tmp_path (Path.basic "spass_reconstruction")) "In exception handler"; - TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^ + handle exn => (*FIXME: exn handler is too general!*) + (File.append(File.tmp_path (Path.basic "prover_reconstruction")) + ("In exception handler: " ^ Toplevel.exn_message exn); + TextIO.output (toParent,"Translation failed for the proof:"^ (remove_linebreaks proofstr) ^"\n"); TextIO.output (toParent, goalstring^"\n"); TextIO.flushOut toParent; diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Mon Sep 19 14:20:45 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Mon Sep 19 15:12:13 2005 +0200 @@ -112,8 +112,8 @@ val use_simpset: bool ref val use_nameless: bool ref val get_clasimp_lemmas : - theory -> term -> - (ResClause.clause * thm) Array.array * int * ResClause.clause list + Proof.context -> term -> + (ResClause.clause * thm) Array.array * ResClause.clause list end; structure ResClasimp : RES_CLASIMP = @@ -155,16 +155,16 @@ (*Write out the claset and simpset rules of the supplied theory. FIXME: argument "goal" is a hack to allow relevance filtering. To reduce the number of clauses produced, set ResClasimp.relevant:=1*) -fun get_clasimp_lemmas thy goal = +fun get_clasimp_lemmas ctxt goal = let val claset_rules = map put_name_pair (ReduceAxiomsN.relevant_filter (!relevant) goal - (ResAxioms.claset_rules_of_thy thy)); + (ResAxioms.claset_rules_of_ctxt ctxt)); val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs claset_rules []); val simpset_rules = ReduceAxiomsN.relevant_filter (!relevant) goal - (ResAxioms.simpset_rules_of_thy thy); + (ResAxioms.simpset_rules_of_ctxt ctxt); val named_simpset = map put_name_pair simpset_rules val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []); @@ -184,7 +184,7 @@ (*********************************************************) val clause_arr = Array.fromList whole_list; in - (clause_arr, List.length whole_list, clauses) + (clause_arr, clauses) end; diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Mon Sep 19 14:20:45 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Mon Sep 19 15:12:13 2005 +0200 @@ -13,7 +13,6 @@ (* Hardwired version of where to pick up the tptp files for the moment *) (***************************************************************************) - signature WATCHER = sig @@ -36,7 +35,9 @@ (* Start a watcher and set up signal handlers *) (**********************************************************) -val createWatcher : thm*(ResClause.clause * thm) Array.array * int -> TextIO.instream * TextIO.outstream * Posix.Process.pid +val createWatcher : + thm * (ResClause.clause * thm) Array.array -> + TextIO.instream * TextIO.outstream * Posix.Process.pid (**********************************************************) (* Kill watcher process *) @@ -48,9 +49,8 @@ - structure Watcher: WATCHER = - struct +struct open ReconPrelim Recon_Transfer @@ -268,7 +268,10 @@ fun getProofCmd (a,c,d,e,f) = d -fun setupWatcher (thm,clause_arr, num_of_clauses) = +fun prems_string_of th = + Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th)) + +fun setupWatcher (thm,clause_arr) = let (** pipes for communication between parent and watcher **) val p1 = Posix.IO.pipe () @@ -295,10 +298,7 @@ val fromParentIOD = Posix.FileSys.fdToIOD fromParent val fromParentStr = openInFD ("_exec_in_parent", fromParent) val toParentStr = openOutFD ("_exec_out_parent", toParent) - val sign = sign_of_thm thm - val prems = prems_of thm - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) - val _ = debug ("subgoals forked to startWatcher: "^prems_string); + val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm); fun killChildren [] = () | killChildren (child_handle::children) = (killChild child_handle; killChildren children) @@ -367,46 +367,45 @@ | checkChildren ((childProc::otherChildren), toParentStr) = let val _ = File.append (File.tmp_path (Path.basic "child_check")) ("In check child, length of queue:"^ - (string_of_int (length (childProc::otherChildren)))^"\n") + string_of_int (length (childProc::otherChildren))) val (childInput,childOutput) = cmdstreamsOf childProc val child_handle= cmdchildHandle childProc (* childCmd is the .dfg file that the problem is in *) val childCmd = fst(snd (cmdchildInfo childProc)) - val _ = File.append (File.tmp_path (Path.basic "child_command")) - (childCmd^"\n") + val _ = File.append (File.tmp_path (Path.basic "child_check")) + ("\nchildCmd = " ^ childCmd) (* now get the number of the subgoal from the filename *) val path_parts = String.tokens(fn c => c = #"/") childCmd val digits = String.translate (fn c => if Char.isDigit c then str c else "") (List.last path_parts); - val sg_num = (case Int.fromString digits of SOME n => n - | NONE => error ("Watcher could not read subgoal nunber: " ^ childCmd)); - + val sg_num = + (case Int.fromString digits of SOME n => n + | NONE => (File.append (File.tmp_path (Path.basic "child_check")) + "\nWatcher could not read subgoal nunber!!"; + raise ERROR)); val childIncoming = pollChildInput childInput - val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) - ("finished polling child \n") + val _ = File.append (File.tmp_path (Path.basic "child_check")) + "\nfinished polling child" val parentID = Posix.ProcEnv.getppid() val prover = cmdProver childProc - val sign = sign_of_thm thm - val prems = prems_of thm - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) - val _ = debug("subgoals forked to checkChildren: "^prems_string) + val prems_string = prems_string_of thm val goalstring = cmdGoal childProc - val _ = File.append (File.tmp_path (Path.basic "child_comms")) - (prover^goalstring^childCmd^"\n") + val _ = File.append (File.tmp_path (Path.basic "child_check")) + ("\nsubgoals forked to checkChildren: " ^ + space_implode "\n" [prems_string,prover,goalstring]) in if isSome childIncoming then (* check here for prover label on child*) - let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) - ("subgoals forked to checkChildren:"^ - prems_string^prover^goalstring^childCmd) + let val _ = File.append (File.tmp_path (Path.basic "child_check")) + "\nInput available from childIncoming" val childDone = (case prover of - "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) - | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) - |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) + "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr) + | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr) + |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr) ) in - if childDone (**********************************************) + if childDone then (* child has found a proof and transferred it *) (* Remove this child and go on to check others*) (**********************************************) @@ -419,7 +418,8 @@ (childProc::(checkChildren (otherChildren, toParentStr))) end else - (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output "; + (File.append (File.tmp_path (Path.basic "child_check")) + "No child output"; childProc::(checkChildren (otherChildren, toParentStr))) end @@ -509,12 +509,12 @@ let val newProcList = execCmds (valOf cmdsFromIsa) procList val parentID = Posix.ProcEnv.getppid() - val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ") - val newProcList' =checkChildren (newProcList, toParentStr) - - val _ = debug("off to keep watching...") - val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ") + val _ = File.append (File.tmp_path (Path.basic "prekeep_watch")) + "Just execed a child\n" + val newProcList' = checkChildren (newProcList, toParentStr) in + File.append (File.tmp_path (Path.basic "keep_watch")) + "Off to keep watching...\n"; loop newProcList' end else (* Execute remotely *) @@ -529,7 +529,7 @@ else (* No new input from Isabelle *) let val newProcList = checkChildren (procList, toParentStr) in - (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n "); + (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...2\n "); loop newProcList end end @@ -602,20 +602,14 @@ (* Start a watcher and set up signal handlers *) (**********************************************************) -fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill); +fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill); fun reapWatcher(pid, instr, outstr) = - let val u = TextIO.closeIn instr; - val u = TextIO.closeOut outstr; - val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) - in - status - end + (TextIO.closeIn instr; TextIO.closeOut outstr; + Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ()) - -fun createWatcher (thm,clause_arr, num_of_clauses) = - let val (childpid,(childin,childout)) = - childInfo (setupWatcher(thm,clause_arr, num_of_clauses)) +fun createWatcher (thm, clause_arr) = + let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr)) fun decr_watched() = (goals_being_watched := (!goals_being_watched) - 1; if !goals_being_watched = 0 @@ -623,63 +617,54 @@ (File.append (File.tmp_path (Path.basic "reap_found")) ("Reaping a watcher, childpid = "^ LargeWord.toString (Posix.Process.pidToWord childpid)^"\n"); - killWatcher childpid; reapWatcher (childpid,childin, childout); ()) + killWatcher childpid; reapWatcher (childpid,childin, childout)) else ()) - val sign = sign_of_thm thm - val prems = prems_of thm - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) - val _ = debug ("subgoals forked to createWatcher: "^prems_string); -(*FIXME: do we need an E proofHandler??*) - fun vampire_proofHandler n = - (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"))) - fun spass_proofHandler n = ( - let val _ = File.append (File.tmp_path (Path.basic "spass_signal")) - "Starting SPASS signal handler\n" - val (reconstr, goalstring) = SpassComm.getSpassInput childin - val _ = File.append (File.tmp_path (Path.basic "spass_signal")) - ("In SPASS signal handler "^reconstr^goalstring^ - "goals_being_watched: "^ string_of_int (!goals_being_watched)) + val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm); + fun proofHandler n = + let val outcome = TextIO.inputLine childin + val goalstring = TextIO.inputLine childin + val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ + "\"\ngoalstring = " ^ goalstring ^ + "\ngoals_being_watched: "^ string_of_int (!goals_being_watched)) in (* if a proof has been found and sent back as a reconstruction proof *) - if substring (reconstr, 0,1) = "[" + if String.isPrefix "[" outcome then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Recon_Transfer.apply_res_thm reconstr goalstring; + Recon_Transfer.apply_res_thm outcome goalstring; Pretty.writeln(Pretty.str (oct_char "361")); decr_watched()) - (* if there's no proof, but a message from Spass *) - else if substring (reconstr, 0,5) = "SPASS" + (* if there's no proof, but a message from the signalling process*) + else if String.isPrefix "Invalid" outcome then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr)); + Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) + ^ "is not provable")); + Pretty.writeln(Pretty.str (oct_char "361")); + decr_watched()) + else if String.isPrefix "Failure" outcome + then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); + Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) + ^ "proof attempt failed")); Pretty.writeln(Pretty.str (oct_char "361")); decr_watched()) (* print out a list of rules used from clasimpset*) - else if substring (reconstr, 0,5) = "Rules" + else if String.isPrefix "Success" outcome then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^reconstr)); + Pretty.writeln(Pretty.str (goalstring^outcome)); Pretty.writeln(Pretty.str (oct_char "361")); decr_watched()) (* if proof translation failed *) - else if substring (reconstr, 0,5) = "Proof" + else if String.isPrefix "Translation failed" outcome then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); - Pretty.writeln(Pretty.str (oct_char "361")); - decr_watched()) - else if substring (reconstr, 0,1) = "%" - then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); + Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks outcome))); Pretty.writeln(Pretty.str (oct_char "361")); decr_watched()) - else (* add something here ?*) + else (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str ("Ran out of options in handler")); + Pretty.writeln(Pretty.str ("System error in proof handler")); Pretty.writeln(Pretty.str (oct_char "361")); decr_watched()) - end) - - in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler); - IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler); + end + in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler); (childin, childout, childpid) - end end (* structure Watcher *) diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Mon Sep 19 14:20:45 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Mon Sep 19 15:12:13 2005 +0200 @@ -9,24 +9,30 @@ sig val prover: string ref val custom_spass: string list ref + val destdir: string ref val hook_count: int ref + val problem_name: string ref end; structure ResAtp: RES_ATP = struct - val call_atp = ref false; val hook_count = ref 0; -fun debug_tac tac = (debug "testing"; tac); - val prover = ref "E"; (* use E as the default prover *) val custom_spass = (*specialized options for SPASS*) ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub", "-DocProof","-TimeLimit=60"]; -val prob_file = File.tmp_path (Path.basic "prob"); +val destdir = ref ""; (*Empty means write files to /tmp*) +val problem_name = ref "prob"; + +fun prob_pathname() = + if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name))) + else if File.exists (File.unpack_platform_path (!destdir)) + then !destdir ^ "/" ^ !problem_name + else error ("No such directory: " ^ !destdir); (**** for Isabelle/ML interface ****) @@ -68,7 +74,7 @@ val _ = debug ("in tptp_inputs_tfrees 2") val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss) val _ = debug ("in tptp_inputs_tfrees 3") - val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n + val probfile = prob_pathname() ^ "_" ^ string_of_int n val out = TextIO.openOut(probfile) in ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses)); @@ -85,7 +91,7 @@ fun dfg_inputs_tfrees thms n axclauses = let val clss = map (ResClause.make_conjecture_clause_thm) thms - val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) + val probfile = prob_pathname() ^ "_" ^ (string_of_int n) val _ = debug ("about to write out dfg prob file " ^ probfile) val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) axclauses [] [] [] @@ -108,7 +114,7 @@ val goalstring = proofstring (Sign.string_of_term sign sg_term) val _ = debug ("goalstring in make_atp_lists is " ^ goalstring) - val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n) + val probfile = prob_pathname() ^ "_" ^ string_of_int n val _ = debug ("prob file in watcher_call_provers is " ^ probfile) in (*Avoid command arguments containing spaces: Poly/ML and SML/NJ @@ -116,7 +122,7 @@ if !prover = "spass" then let val optionline = - if !SpassComm.reconstruct + if !AtpCommunication.reconstruct (*Proof reconstruction works for only a limited set of inference rules*) then "-" ^ space_implode "%-" (!custom_spass) @@ -170,30 +176,31 @@ ()); +(*FIXME: WHAT IS THMS FOR????*) + (******************************************************************) (* called in Isar automatically *) (* writes out the current clasimpset to a tptp file *) (* turns off xsymbol at start of function, restoring it at end *) (******************************************************************) (*FIX changed to clasimp_file *) -val isar_atp' = setmp print_mode [] +val isar_atp = setmp print_mode [] (fn (ctxt, thms, thm) => if Thm.no_prems thm then () else let - val _= debug ("in isar_atp'") + val _= debug ("in isar_atp") val thy = ProofContext.theory_of ctxt val prems = Thm.prems_of thm val thms_string = Meson.concat_with_and (map string_of_thm thms) val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems) (*set up variables for writing out the clasimps to a tptp file*) - val (clause_arr, num_of_clauses, axclauses) = - ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*) - val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^ - " clauses") - val (childin, childout, pid) = - Watcher.createWatcher (thm, clause_arr, num_of_clauses) + val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) + (*FIXME: hack!! need to consider relevance for all prems*) + val _ = debug ("claset and simprules total clauses = " ^ + string_of_int (Array.length clause_arr)) + val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr) val pid_string = string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid))) in @@ -205,43 +212,17 @@ end); val isar_atp_writeonly = setmp print_mode [] - (fn (ctxt, thms, thm) => + (fn (ctxt, thms: thm list, thm) => if Thm.no_prems thm then () else - let - val thy = ProofContext.theory_of ctxt - val prems = Thm.prems_of thm - - (*set up variables for writing out the clasimps to a tptp file*) - val (clause_arr, num_of_clauses, axclauses) = - ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*) + let val prems = Thm.prems_of thm + val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) in write_problem_files axclauses thm (length prems) end); -fun get_thms_cs claset = - let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset - in safeEs @ safeIs @ hazEs @ hazIs end; -fun append_name name [] _ = [] - | append_name name (thm :: thms) k = - Thm.name_thm ((name ^ "_" ^ string_of_int k), thm) :: append_name name thms (k + 1); - -fun append_names (name :: names) (thms :: thmss) = - append_name name thms 0 :: append_names names thmss; - -fun get_thms_ss [] = [] - | get_thms_ss thms = - let - val names = map Thm.name_of_thm thms - val thms' = map (mksimps mksimps_pairs) thms - val thms'' = append_names names thms' - in - ResLib.flat_noDup thms'' - end; - - -(* convert locally declared rules to axiom clauses *) +(* convert locally declared rules to axiom clauses: UNUSED *) fun subtract_simpset thy ctxt = let @@ -265,12 +246,7 @@ val proof = Toplevel.proof_of state val (ctxt, (_, goal)) = Proof.get_goal proof handle Proof.STATE _ => error "No goal present"; - val thy = ProofContext.theory_of ctxt; - - (* FIXME presently unused *) - val ss_thms = subtract_simpset thy ctxt; - val cs_thms = subtract_claset thy ctxt; in debug ("initial thm in isar_atp: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt goal)); @@ -278,10 +254,12 @@ Pretty.string_of (ProofContext.pretty_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)))); debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal)); + debug ("current theory: " ^ Context.theory_name thy); hook_count := !hook_count +1; debug ("in hook for time: " ^(string_of_int (!hook_count)) ); ResClause.init thy; - isar_atp' (ctxt, ProofContext.prems_of ctxt, goal) + if !destdir = "" then isar_atp (ctxt, ProofContext.prems_of ctxt, goal) + else isar_atp_writeonly (ctxt, ProofContext.prems_of ctxt, goal) end); val call_atpP = diff -r c6005bfc1630 -r f6a225f97f0a src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Mon Sep 19 14:20:45 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Mon Sep 19 15:12:13 2005 +0200 @@ -18,7 +18,10 @@ val rm_Eps : (term * term) list -> thm list -> term list val claset_rules_of_thy : theory -> (string * thm) list val simpset_rules_of_thy : theory -> (string * thm) list - val clausify_rules_pairs : (string*thm) list -> thm list -> (ResClause.clause*thm) list list * thm list + val claset_rules_of_ctxt: Proof.context -> (string * thm) list + val simpset_rules_of_ctxt : Proof.context -> (string * thm) list + val clausify_rules_pairs : + (string*thm) list -> thm list -> (ResClause.clause*thm) list list * thm list val clause_setup : (theory -> theory) list val meson_method_setup : (theory -> theory) list end; @@ -357,19 +360,31 @@ val tag_intro = preserve_name (fn th => th RS tagI); val tag_elim = preserve_name (fn th => tagD RS th); -fun claset_rules_of_thy thy = - let val cs = rep_cs (claset_of thy) - val intros = (#safeIs cs) @ (#hazIs cs) - val elims = (#safeEs cs) @ (#hazEs cs) +fun rules_of_claset cs = + let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs + val intros = safeIs @ hazIs + val elims = safeEs @ hazEs in + debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ + " elims: " ^ Int.toString(length elims)); if tagging_enabled then map pairname (map tag_intro intros @ map tag_elim elims) - else map pairname (intros @ elims) + else map pairname (intros @ elims) end; -fun simpset_rules_of_thy thy = - let val rules = #rules (fst (rep_ss (simpset_of thy))) - in map (fn r => (#name r, #thm r)) (Net.entries rules) end; +fun rules_of_simpset ss = + let val ({rules,...}, _) = rep_ss ss + val simps = Net.entries rules + in + debug ("rules_of_simpset: " ^ Int.toString(length simps)); + map (fn r => (#name r, #thm r)) simps + end; + +fun claset_rules_of_thy thy = rules_of_claset (claset_of thy); +fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy); + +fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt); +fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); (**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****)