# HG changeset patch # User quigley # Date 1125689395 -7200 # Node ID 6edb84c661dd51b7ebc75f30d79160f6c1ebee6b # Parent 8e55ad29b690e130e87a526891e5119b2eee1f09 Added ECommunication.ML diff -r 8e55ad29b690 -r 6edb84c661dd src/HOL/Reconstruction.thy --- a/src/HOL/Reconstruction.thy Fri Sep 02 21:29:33 2005 +0200 +++ b/src/HOL/Reconstruction.thy Fri Sep 02 21:29:55 2005 +0200 @@ -9,6 +9,7 @@ theory Reconstruction imports Hilbert_Choice Map Infinite_Set Extraction uses "Tools/res_lib.ML" + "Tools/res_clause.ML" "Tools/res_skolem_function.ML" "Tools/res_axioms.ML" @@ -21,6 +22,7 @@ "Tools/ATP/recon_transfer_proof.ML" "Tools/ATP/VampCommunication.ML" "Tools/ATP/SpassCommunication.ML" + "Tools/ATP/ECommunication.ML" "Tools/ATP/watcher.sig" "Tools/ATP/watcher.ML" "Tools/ATP/res_clasimpset.ML" diff -r 8e55ad29b690 -r 6edb84c661dd src/HOL/Tools/ATP/ECommunication.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/ECommunication.ML Fri Sep 02 21:29:55 2005 +0200 @@ -0,0 +1,279 @@ +(* Title: SpassCommunication.ml + ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) + +(***************************************************************************) +(* Code to deal with the transfer of proofs from a E process *) +(***************************************************************************) +signature E_COMM = + sig + val reconstruct : bool ref + val E: bool ref + val getEInput : TextIO.instream -> string * string * string + val checkEProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * string * + string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array * int -> bool + + end; + +structure EComm :E_COMM = +struct + +(* switch for whether to reconstruct a proof found, or just list the lemmas used *) +val reconstruct = ref true; +val E = ref false; + +(***********************************) +(* Write E output to a file *) +(***********************************) + +fun logEInput (instr, fd) = + let val thisLine = TextIO.inputLine instr + in if thisLine = "# Proof object ends here.\n" + then TextIO.output (fd, thisLine) + else (TextIO.output (fd, thisLine); logEInput (instr,fd)) + end; + +(**********************************************************************) +(* Reconstruct the 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 *) +(**********************************************************************) + +val atomize_tac = SUBGOAL + (fn (prop,_) => + let val ts = Logic.strip_assums_hyp prop + in EVERY1 + [METAHYPS + (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), + REPEAT_DETERM_N (length ts) o (etac thin_rl)] + end); + + +fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num + clause_arr (num_of_clauses:int ) = + (*FIXME: foo is never used!*) + let val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3"))); + in + SELECT_GOAL + (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, + METAHYPS(fn negs => + ( Recon_Transfer.EString_to_lemmaString proofextract thmstring goalstring + toParent ppid negs clause_arr num_of_clauses ))]) sg_num + end ; + + +fun transferEInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = + let val thisLine = TextIO.inputLine fromChild + in + if thisLine = "# Proof object ends here.\n" + then + let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) + in + File.write (File.tmp_path (Path.basic"foobar2")) proofextract; + reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num + clause_arr num_of_clauses thm + end + else transferEInput (fromChild, toParent, ppid,thmstring, goalstring, + (currentString^thisLine), thm, sg_num, clause_arr, + num_of_clauses) + end; + + +(*********************************************************************************) +(* Inspect the output of a E process to see if it has found a proof, *) +(* and if so, transfer output to the input pipe of the main Isabelle process *) +(*********************************************************************************) + + +fun startETransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = +(*let val _ = Posix.Process.wait () +in*) + + if (isSome (TextIO.canInput(fromChild, 5))) + then + let val thisLine = TextIO.inputLine fromChild + in + if String.isPrefix "# Proof object starts" thisLine then + let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer"))) + val _= TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm)) + val _ = TextIO.closeOut outfile + in + transferEInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, + thm, sg_num,clause_arr, num_of_clauses); + true + end + else startETransfer (fromChild, toParent, ppid, thmstring, goalstring, + childCmd, thm, sg_num,clause_arr, num_of_clauses) + end + else false + (* end*) + + +fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) = + 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 "foo_checkE")) + ("checking if proof found, thm is: "^(string_of_thm thm)) + in + if (isSome (TextIO.canInput(fromChild, 5))) + then + let val thisLine = TextIO.inputLine fromChild + in if (*thisLine = "# Problem is unsatisfiable (or provable), constructing proof object\n"*) + thisLine = "# # TSTP exit status: Unsatisfiable\n" + then + let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + val _ = TextIO.output (outfile, thisLine) + + val _ = TextIO.closeOut outfile + in + startETransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) + end + else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n" + then + let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + val _ = TextIO.output (outfile, thisLine) + + val _ = TextIO.closeOut outfile + in + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (E_proof_file, thisLine); + TextIO.flushOut E_proof_file; + TextIO.closeOut E_proof_file; + (*TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; + TextIO.output (toParent, "bar\n"); + TextIO.flushOut toParent;*) + + TextIO.output (toParent, thisLine^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, thmstring^"\n"); + TextIO.flushOut toParent; + 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 + end + else if thisLine = "# Failure: Resource limit exceeded (time)\n" + then + let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + val _ = TextIO.output (outfile, thisLine) + in TextIO.output (toParent, thisLine^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, thmstring^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, goalstring^"\n"); + TextIO.flushOut toParent; + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + TextIO.output (outfile, ("signalled parent\n"));TextIO.closeOut outfile; + (* Attempt to prevent several signals from turning up simultaneously *) + Posix.Process.sleep(Time.fromSeconds 1); + true + end + 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.flushOut toParent; + TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; + true) + else + (TextIO.output (E_proof_file, thisLine); + TextIO.flushOut E_proof_file; + checkEProofFound (fromChild, toParent, ppid, thmstring,goalstring, + childCmd, thm, sg_num, clause_arr, num_of_clauses)) + end + else + (TextIO.output (E_proof_file, ("No proof output seen \n")); + TextIO.closeOut E_proof_file; + false) + end + + + +(***********************************************************************) +(* Function used by the Isabelle process to read in a E proof *) +(***********************************************************************) + +fun getEInput instr = + if isSome (TextIO.canInput(instr, 2)) + then + let val thisLine = TextIO.inputLine instr + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); + val _ = TextIO.output (outfile, thisLine) + val _ = TextIO.closeOut outfile + in + if substring (thisLine, 0,1) = "[" + then + (*Pretty.writeln(Pretty.str thisLine)*) + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + else if String.isPrefix "SPASS beiseite:" thisLine + then + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + + else if String.isPrefix "# No proof" thisLine + then + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + + else if String.isPrefix "# Failure" thisLine + then + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + + + + else if String.isPrefix "Rules from" thisLine + then + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + else if substring (thisLine, 0,5) = "Proof" + then + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine; + (reconstr, thmstring, goalstring) + end + else if substring (thisLine, 0,1) = "%" + then + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine; + (reconstr, thmstring, goalstring) + end + else getEInput instr + end + else + ("No output from reconstruction process.\n","","") + +end;