# HG changeset patch # User paulson # Date 1126109666 -7200 # Node ID 5cde710a8a2381c14f0ca98310979abb9a8dda5c # Parent 6cef3aedd6610d61ead8fe0b50ce58213e98d9fb Progress on eprover linkup, also massive tidying diff -r 6cef3aedd661 -r 5cde710a8a23 src/HOL/Tools/ATP/ECommunication.ML --- a/src/HOL/Tools/ATP/ECommunication.ML Wed Sep 07 09:54:31 2005 +0200 +++ b/src/HOL/Tools/ATP/ECommunication.ML Wed Sep 07 18:14:26 2005 +0200 @@ -21,16 +21,7 @@ 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; +exception EOF; (**********************************************************************) (* Reconstruct the E proof w.r.t. thmstring (string version of *) @@ -47,153 +38,134 @@ toParent ppid negs clause_arr num_of_clauses ))]) sg_num -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"extracted-prf-E")) 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; +fun transferEInput (fromChild, toParent, ppid,thmstring,goalstring, + currentString, thm, sg_num,clause_arr, num_of_clauses) = + let val thisLine = TextIO.inputLine fromChild + in + File.append (File.tmp_path (Path.basic "eprover_transfer")) + ("transferEInput input line: " ^ thisLine); + if thisLine = "" (*end of file?*) + then (File.write (File.tmp_path (Path.basic"eprover_extraction_failed")) currentString; + raise EOF) + else 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"eprover_extracted_prf")) 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 an E process to see if it has found a proof, *) +(* Inspect the output of an 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) = - if isSome (TextIO.canInput(fromChild, 5)) - then let val thisLine = TextIO.inputLine fromChild in - if String.isPrefix "# Proof object starts" thisLine + if thisLine = "" then false + else if String.isPrefix "# Proof object starts" thisLine then - (File.append (File.tmp_path (Path.basic "transfer-E")) - ("about to transfer proof, thm is: " ^ string_of_thm thm); + (File.append (File.tmp_path (Path.basic "eprover_transfer")) + ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n"); transferEInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, - thm, sg_num,clause_arr, num_of_clauses); - true) + thm, sg_num,clause_arr, num_of_clauses); + true) handle EOF => false else startETransfer (fromChild, toParent, ppid, thmstring, goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) end - else false -fun checkEProofFound (fromChild, toParent, ppid,thmstring,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 "E_proof"))) - val _ = File.write (File.tmp_path (Path.basic "checking-prf-E")) - ("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 _ = 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;*) +fun checkEProofFound (fromChild, toParent, ppid,thmstring,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 "eprover_proof"))) + val _ = File.write (File.tmp_path (Path.basic "eprover_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 = "# Problem is unsatisfiable (or provable), constructing proof object\n"*) + thisLine = "# TSTP exit status: Unsatisfiable\n" + then + (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine; + startETransfer (fromChild, toParent, ppid, thmstring,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 "eprover_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.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) + TextIO.output (toParent, thisLine^"\n"); + TextIO.output (toParent, thmstring^"\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 "eprover_response")) thisLine; + TextIO.output (toParent, thisLine^"\n"); + TextIO.output (toParent, thmstring^"\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.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 (***********************************************************************) -(* Function used by the Isabelle process to read in a E proof *) +(* Function used by the Isabelle process to read in an 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 + val _ = File.write (File.tmp_path (Path.basic "eprover_line")) thisLine in - if substring (thisLine, 0,1) = "[" + if thisLine = "" then ("No output from reconstruction process.\n","","") + else if String.sub (thisLine, 0) = #"[" 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 + else if String.isPrefix "SPASS beiseite:" thisLine (*FIXME: wrong!!*) then let val reconstr = thisLine val thmstring = TextIO.inputLine instr @@ -219,9 +191,6 @@ in (reconstr, thmstring, goalstring) end - - - else if String.isPrefix "Rules from" thisLine then let val reconstr = thisLine @@ -250,7 +219,4 @@ end else getEInput instr end - else - ("No output from reconstruction process.\n","","") - end; diff -r 6cef3aedd661 -r 5cde710a8a23 src/HOL/Tools/ATP/SpassCommunication.ML --- a/src/HOL/Tools/ATP/SpassCommunication.ML Wed Sep 07 09:54:31 2005 +0200 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML Wed Sep 07 18:14:26 2005 +0200 @@ -11,27 +11,18 @@ sig val reconstruct : bool ref val getSpassInput : TextIO.instream -> string * string * string - val checkSpassProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * string * - string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array * int -> bool - + val checkSpassProofFound: + TextIO.instream * TextIO.outstream * Posix.Process.pid * string * + 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 true; - -(***********************************) -(* Write Spass output to a file *) -(***********************************) +val reconstruct = ref false; -fun logSpassInput (instr, fd) = - let val thisLine = TextIO.inputLine instr - in if thisLine = "--------------------------SPASS-STOP------------------------------\n" - then TextIO.output (fd, thisLine) - else (TextIO.output (fd, thisLine); logSpassInput (instr,fd)) - end; +exception EOF; (**********************************************************************) (* Reconstruct the Spass proof w.r.t. thmstring (string version of *) @@ -40,148 +31,121 @@ (**********************************************************************) 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 + 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 => - (if !reconstruct - then Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring - toParent ppid negs clause_arr num_of_clauses - else Recon_Transfer.spassString_to_lemmaString proofextract thmstring goalstring - toParent ppid negs clause_arr num_of_clauses ))]) sg_num - end ; + f proofextract thmstring goalstring + toParent ppid negs clause_arr num_of_clauses)]) sg_num + end; -fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = - let val thisLine = TextIO.inputLine fromChild - in - if thisLine = "--------------------------SPASS-STOP------------------------------\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 transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring, - (currentString^thisLine), thm, sg_num, clause_arr, - num_of_clauses) - end; +fun transferSpassInput (fromChild, toParent, ppid,thmstring,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"eprover_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 thmstring goalstring toParent ppid sg_num + clause_arr num_of_clauses thm + end + else transferSpassInput (fromChild, toParent, ppid,thmstring, 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, *) +(* 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, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = -(*let val _ = Posix.Process.wait () -in*) - - if (isSome (TextIO.canInput(fromChild, 5))) - then +fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, + thm, sg_num,clause_arr, num_of_clauses) = let val thisLine = TextIO.inputLine fromChild in - if String.isPrefix "Here is a proof" 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 - transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, - thm, sg_num,clause_arr, num_of_clauses); - true - end - else startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring, - childCmd, thm, sg_num,clause_arr, num_of_clauses) + 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,thmstring, goalstring,thisLine, + thm, sg_num,clause_arr, num_of_clauses); + true) handle EOF => false + else startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring, + childCmd, thm, sg_num,clause_arr, num_of_clauses) end - else false - (* end*) - -fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,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 "foo_checkspass")) - ("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 = "SPASS beiseite: Proof found.\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 - startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) - end - else if thisLine= "SPASS beiseite: Completion found.\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 (spass_proof_file, thisLine); - TextIO.flushOut spass_proof_file; - TextIO.closeOut spass_proof_file; - (*TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; - TextIO.output (toParent, "bar\n"); - TextIO.flushOut toParent;*) +fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,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, thmstring,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.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 = "SPASS beiseite: Ran out of 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 = "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, thmstring,goalstring, - childCmd, thm, sg_num, clause_arr, num_of_clauses)) - end - else - (TextIO.output (spass_proof_file, ("No proof output seen \n")); - TextIO.closeOut spass_proof_file; - false) + TextIO.output (toParent, thisLine^"\n"); + TextIO.output (toParent, thmstring^"\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, thmstring^"\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, thmstring,goalstring, + childCmd, thm, sg_num, clause_arr, num_of_clauses)) end @@ -190,60 +154,28 @@ (***********************************************************************) fun getSpassInput 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 + val _ = File.write (File.tmp_path (Path.basic "spass_line")) thisLine 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 + 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 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" + let val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in (thisLine, thmstring, goalstring) end + else if substring (thisLine,0,5) = "Proof" orelse + String.sub (thisLine, 0) = #"%" then - let val reconstr = thisLine - val thmstring = TextIO.inputLine instr + let val thmstring = TextIO.inputLine instr val goalstring = TextIO.inputLine instr in - File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine; - (reconstr, thmstring, goalstring) + File.write (File.tmp_path (Path.basic "getSpassInput")) thisLine; + (thisLine, 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 getSpassInput instr end - else - ("No output from reconstruction process.\n","","") end; diff -r 6cef3aedd661 -r 5cde710a8a23 src/HOL/Tools/ATP/VampCommunication.ML --- a/src/HOL/Tools/ATP/VampCommunication.ML Wed Sep 07 09:54:31 2005 +0200 +++ b/src/HOL/Tools/ATP/VampCommunication.ML Wed Sep 07 18:14:26 2005 +0200 @@ -18,16 +18,7 @@ structure VampComm : VAMP_COMM = struct -(***********************************) -(* Write Vampire output to a file *) -(***********************************) - -fun logVampInput (instr, fd) = - let val thisLine = TextIO.inputLine instr - in if (thisLine = "%============== End of proof. ==================\n" ) - then TextIO.output (fd, thisLine) - else (TextIO.output (fd, thisLine); logVampInput (instr,fd)) - end; +exception EOF; (**********************************************************************) (* Reconstruct the Vampire proof w.r.t. thmstring (string version of *) @@ -45,13 +36,17 @@ goalstring toParent ppid negs clause_arr num_of_clauses ))]) sg_num -fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = +fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, + currentString, thm, sg_num,clause_arr, num_of_clauses) = let val thisLine = TextIO.inputLine fromChild in - if (thisLine = "%============== End of proof. ==================\n" ) + if thisLine = "" (*end of file?*) + then (File.write (File.tmp_path (Path.basic"vampire_extraction_failed")) currentString; + raise EOF) + else if (thisLine = "%============== End of proof. ==================\n" ) then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) in - File.write (File.tmp_path (Path.basic"extracted-prf-vamp")) proofextract; + File.write (File.tmp_path (Path.basic"vampire_extracted_prf")) proofextract; reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr num_of_clauses thm end @@ -61,190 +56,114 @@ (*********************************************************************************) -(* Inspect the output of a Vampire process to see if it has found a proof, *) +(* Inspect the output of a Vampire process to see if it has found a proof, *) (* and if so, transfer output to the input pipe of the main Isabelle process *) (*********************************************************************************) fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses) = - if isSome (TextIO.canInput(fromChild, 5)) - then - let val thisLine = TextIO.inputLine fromChild - in - if (thisLine = "%================== Proof: ======================\n") - then - (File.append (File.tmp_path (Path.basic "transfer-vamp")) - ("about to transfer proof, thm is: " ^ string_of_thm thm); - transferVampInput (fromChild, toParent, ppid,thmstring, goalstring, - thisLine, thm, sg_num,clause_arr, num_of_clauses); - true) - else - startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring, - childCmd, thm, sg_num,clause_arr, num_of_clauses) - end - else false - - -fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, num_of_clauses) = - let val vamp_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof"))) - val _ = File.write (File.tmp_path (Path.basic "checking-prf-vamp")) - ("checking if proof found, thm is: " ^ string_of_thm thm) + let val thisLine = TextIO.inputLine fromChild in - if (isSome (TextIO.canInput(fromChild, 5))) + if thisLine = "" then false + else if (thisLine = "%================== Proof: ======================\n") then - ( - let val thisLine = TextIO.inputLine fromChild - in if (thisLine = "% Proof found. Thanks to Tanya!\n" ) - then - let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); - val _ = TextIO.output (outfile, (thisLine)) - - val _ = TextIO.closeOut outfile - in - startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) - end - else if (thisLine = "% Unprovable.\n" ) - then - let val outfile = TextIO.openOut(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 (vamp_proof_file, (thisLine)); - TextIO.flushOut vamp_proof_file; - TextIO.closeOut vamp_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 = "% Proof not found. Time limit expired.\n") - then - (let val outfile = TextIO.openOut(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 (vamp_proof_file, (thisLine)); - TextIO.flushOut vamp_proof_file; - TextIO.closeOut vamp_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 - (TextIO.output (vamp_proof_file, (thisLine)); - TextIO.flushOut vamp_proof_file; - checkVampProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)) - - end - ) + (File.append (File.tmp_path (Path.basic "vampire_transfer")) + ("about to transfer proof, thm is: " ^ string_of_thm thm); + transferVampInput (fromChild, toParent, ppid,thmstring, goalstring, + thisLine, thm, sg_num,clause_arr, num_of_clauses); + true) handle EOF => false else - (TextIO.output (vamp_proof_file, ("No proof output seen \n"));TextIO.closeOut vamp_proof_file;false) + startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring, + childCmd, thm, sg_num,clause_arr, num_of_clauses) end +fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, + thm, sg_num, clause_arr, num_of_clauses) = + let val vamp_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 + if thisLine = "" + then (TextIO.output (vamp_proof_file, ("No proof output seen \n")); + TextIO.closeOut vamp_proof_file; + false) + else if thisLine = "% Proof found. Thanks to Tanya!\n" + then + (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine; + startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring, + childCmd, thm, sg_num, clause_arr, num_of_clauses)) + else if (thisLine = "% Unprovable.\n" ) + then + (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine; + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (vamp_proof_file, thisLine); + TextIO.closeOut vamp_proof_file; + (*TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; + TextIO.output (toParent, "bar\n"); + TextIO.flushOut toParent;*) + + TextIO.output (toParent, thisLine^"\n"); + TextIO.output (toParent, thmstring^"\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 = "% Proof not found. Time limit expired.\n") + then + (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine; + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (vamp_proof_file, thisLine); + TextIO.closeOut vamp_proof_file; + + TextIO.output (toParent, thisLine^"\n"); + TextIO.output (toParent, thmstring^"\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 (vamp_proof_file, thisLine); + TextIO.flushOut vamp_proof_file; + checkVampProofFound (fromChild, toParent, ppid, thmstring, + goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)) + end + + (***********************************************************************) -(* Function used by the Isabelle process to read in a vamp proof *) +(* Function used by the Isabelle process to read in a Vampire proof *) (***********************************************************************) fun getVampInput instr = - if (isSome (TextIO.canInput(instr, 2))) - then - let val thisLine = TextIO.inputLine instr - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine)) + let val thisLine = TextIO.inputLine instr + val _ = File.write (File.tmp_path (Path.basic "vampire_line")) thisLine + in (* reconstructed proof string *) + if thisLine = "" then ("No output from reconstruction process.\n","","") + else if String.sub (thisLine, 0) = #"[" orelse + thisLine = "% Unprovable.\n" orelse + thisLine ="% Proof not found. Time limit expired.\n" orelse + String.isPrefix "Rules from" thisLine + then + let val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in (thisLine, thmstring, goalstring) end + else if thisLine = "Proof found but translation failed!" + then + let val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + val _ = debug "getVampInput: translation of proof failed" + in (thisLine, thmstring, goalstring) end + else getVampInput instr + end - val _ = TextIO.closeOut outfile - in (* reconstructed proof string *) - 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 (thisLine = "% Unprovable.\n" ) - then - ( - let val reconstr = thisLine - val thmstring = TextIO.inputLine instr - val goalstring = TextIO.inputLine instr - in - (reconstr, thmstring, goalstring) - end - ) - else if (thisLine = "% Proof not found. Time limit expired.\n") - 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 (thisLine = "Proof found but translation failed!") - then - ( - let val reconstr = thisLine - val thmstring = TextIO.inputLine instr - val goalstring = TextIO.inputLine instr - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getVamp"))); - val _ = TextIO.output (outfile, (thisLine)) - val _ = TextIO.closeOut outfile - in - (reconstr, thmstring, goalstring) - end - ) - else - getVampInput instr - - end - else - ("No output from reconstruction process.\n","","") end; diff -r 6cef3aedd661 -r 5cde710a8a23 src/HOL/Tools/ATP/recon_parse.ML --- a/src/HOL/Tools/ATP/recon_parse.ML Wed Sep 07 09:54:31 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_parse.ML Wed Sep 07 18:14:26 2005 +0200 @@ -25,7 +25,6 @@ (* Parser combinators *) exception Noparse; -exception SPASSError of string; exception VampError of string; @@ -118,47 +117,22 @@ raise (GandalfError "Couldn't find a proof.") *) -val proofstring = -"0:00:00.00 for the reduction.\ -\\ -\Here is a proof with depth 3, length 7 :\ -\1[0:Inp] || -> P(xa)*.\ -\2[0:Inp] || -> Q(xb)*.\ -\3[0:Inp] || R(U)* -> .\ -\4[0:Inp] || Q(U) P(V) -> R(x(V,U))*.\ -\9[0:Res:4.2,3.0] || Q(U)*+ P(V)* -> .\ -\11[0:Res:2.0,9.0] || P(U)* -> .\ -\12[0:Res:1.0,11.0] || -> .\ -\Formulae used in the proof :\ -\\ -\--------------------------SPASS-STOP------------------------------" - -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 "%================== Proof: ======================" s then - (kill_lines 0 - o snd o cut_after "%================== Proof: ======================" - o fst o cut_before "============== End of proof. ==================") s - else - raise SPASSError "Couldn't find a proof." - -(*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 - raise SPASSError "Couldn't find a proof." -*) - - - - +(*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 "%================== Proof: ======================" s then + (kill_lines 0 (*Vampire 5.0*) + o snd o cut_after "%================== Proof: ======================" + o fst o cut_before "============== End of proof. ==================") s + else if cut_exists "# Proof object ends here." s then + (kill_lines 0 (*eproof*) + o snd o cut_after "# Proof object starts here." + o fst o cut_before "# Proof object ends here.") 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 "") @@ -358,12 +332,6 @@ exception NOTERM - -fun implode_with_space [] = implode [] -| implode_with_space [x] = implode [x] -| implode_with_space (x::[y]) = x^" "^y -| implode_with_space (x::xs) = (x^" "^(implode_with_space xs)) - (* FIX - should change the stars and pluses to many rather than explicit patterns *) fun trim_prefix a b = @@ -499,87 +467,22 @@ (*and arglist input = ( nterm >> (fn (a) => (a)) || nterm ++ many (a (Other ",") ++ nterm >> snd) - >> (fn (a, b) => (a^" "^(implode_with_space b)))) input*) + >> (fn (a, b) => (a^" "^(space_implode " " b)))) input*) and arglist input = ( nterm ++ many (a (Other ",") ++ nterm >> snd) - >> (fn (a, b) => (a^" "^(implode_with_space b))) + >> (fn (a, b) => (a^" "^(space_implode " " b))) || nterm >> (fn (a) => (a)))input val clause = term - - - (*val line = number ++ justification ++ a (Other "|") ++ - a (Other "|") ++ clause ++ a (Other ".") - >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))*) - - (* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *) val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++ a (Other "|") ++ clause ++ a (Other ".") >> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c))) - - val lines = many line val alllines = (lines ++ finished) >> fst val parse = fst o alllines - val s = proofstring; - - - - -fun dropUntilNot ch [] = ( []) - | dropUntilNot ch (x::xs) = if not(x = ch ) - then - (x::xs) - else - dropUntilNot ch xs - - -fun remove_spaces str [] = str -| remove_spaces str (x::[]) = if x = " " - then - str - else - (str^x) -| remove_spaces str (x::xs) = - let val (first, rest) = ReconOrderClauses.takeUntil " " (x::xs) [] - val (next) = dropUntilNot " " rest - in - if next = [] - then - (str^(implode first)) - else remove_spaces (str^(implode first)^" ") next - end - - -fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs) - - -fun all_spaces xs = List.filter (not_equal " " ) xs - -fun just_change_space [] = [] -| just_change_space ((clausenum, step, strs)::xs) = - let val newstrs = remove_space_strs strs - in - if (all_spaces newstrs = [] ) (* all type_info *) - then - (clausenum, step, newstrs)::(just_change_space xs) - else - (clausenum, step, newstrs)::(just_change_space xs) - end; - -fun change_space [] = [] -| change_space ((clausenum, step, strs)::xs) = - let val newstrs = remove_space_strs strs - in - if (all_spaces newstrs = [] ) (* all type_info *) - then - (clausenum, step, T_info, newstrs)::(change_space xs) - else - (clausenum, step, P_info, newstrs)::(change_space xs) - end end; diff -r 6cef3aedd661 -r 5cde710a8a23 src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Sep 07 09:54:31 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Sep 07 18:14:26 2005 +0200 @@ -175,12 +175,10 @@ (* get names of clasimp axioms used *) (*****************************************************) - fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses = + fun get_axiom_names step_nums thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses = let (* not sure why this is necessary again, but seems to be *) val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) - val axioms = get_init_axioms proof_steps - val step_nums = get_step_nums axioms [] (***********************************************) (* here need to add the clauses from clause_arr*) @@ -195,47 +193,14 @@ in clasimp_names end - - fun get_axiom_names_vamp proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses = - let - (* not sure why this is necessary again, but seems to be *) - val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) - val step_nums =get_linenums proofstr - - (***********************************************) - (* 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 = map (#1 o ResClause.clause_info o #1) clasimp_names_cls - - val _ = File.write (File.tmp_path (Path.basic "clasimp_names")) - (concat clasimp_names) - val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode)) - in - clasimp_names - end + + fun get_axiom_names_spass proof_steps thms clause_arr num_of_clauses = + get_axiom_names (get_step_nums (get_init_axioms proof_steps) []) + thms clause_arr num_of_clauses; - -fun get_axiom_names_E proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses = - let - (* not sure why this is necessary again, but seems to be *) - val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) - val step_nums =get_linenums proofstr - - (***********************************************) - (* 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 = map (#1 o ResClause.clause_info o #1) clasimp_names_cls - - val _ = File.write (File.tmp_path (Path.basic "clasimp_names")) - (concat clasimp_names) - val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode)) - in - clasimp_names - 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; + (***********************************************) (* get axioms for reconstruction *) @@ -255,19 +220,6 @@ val axioms = get_init_axioms proof_steps val step_nums = get_step_nums axioms [] - (***********************************************) - (* 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 = map #1 clasimp_names_cls - val clasimp_cls = map #2 clasimp_names_cls - val _ = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names - val _ = TextIO.output (outfile,clasimp_namestr) - - val _ = TextIO.closeOut outfile -*) - val clauses =(*(clasimp_cls)@*)( make_clauses thms) val vars = map thm_vars clauses @@ -302,20 +254,8 @@ val extra_with_vars = if (not (extra_metas = []) ) then ListPair.zip (extra_metas,extra_vars) else [] - (* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) - val _ = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas"))) - - val _ = TextIO.output (outfile, ((thmstrings ax_metas ""))) - val _ = TextIO.closeOut outfile - val foo_metas = File.platform_path(File.tmp_path (Path.basic "foo_metas")) - val foo_metas2 = File.platform_path(File.tmp_path (Path.basic "foo_metas2")) - val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", " <", foo_metas, " >", foo_metas2]) - val infile = TextIO.openIn(File.platform_path(File.tmp_path (Path.basic "foo_metas2"))) - val ax_metas_str = TextIO.inputLine (infile) - val _ = TextIO.closeIn infile - val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*) in - (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas))) + (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas))) end; @@ -329,9 +269,6 @@ | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]" -val dummy_tac = PRIMITIVE(fn thm => thm ); - - (*val proofstr = "1242[0:Inp] || -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\ \1279[0:Inp] || -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\ \1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\ @@ -351,10 +288,10 @@ (* parse spass proof into datatype *) (***********************************) val tokens = #1(lex proofstr) - val proof_steps1 = parse tokens - val proof_steps = just_change_space proof_steps1 - val _ = File.write (File.tmp_path (Path.basic "foo_parse")) ("Did parsing on "^proofstr) - val _ = File.write(File.tmp_path (Path.basic "foo_thmstring_at_parse")) + val proof_steps = parse tokens + val _ = File.write (File.tmp_path (Path.basic "parsing_done")) + ("Did parsing on "^proofstr) + val _ = File.write(File.tmp_path (Path.basic "parsing_thmstring")) ("Parsing for thmstring: "^thmstring) (************************************) (* recreate original subgoal as thm *) @@ -366,22 +303,20 @@ (* should prob add array and table here, so that we can get axioms*) (* produced from the clasimpset rather than the problem *) - val (axiom_names) = get_axiom_names proof_steps thms clause_arr num_of_clauses + val axiom_names = get_axiom_names_spass proof_steps thms clause_arr num_of_clauses val ax_str = "Rules from clasimpset used in proof found by SPASS: " ^ rules_to_string axiom_names val _ = File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^" "^goalstring) in TextIO.output (toParent, ax_str^"\n"); - TextIO.flushOut toParent; TextIO.output (toParent, "goalstring: "^goalstring^"\n"); - TextIO.flushOut toParent; TextIO.output (toParent, "thmstring: "^thmstring^"\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) ; dummy_tac + Posix.Process.sleep(Time.fromSeconds 1) ; all_tac end handle _ => let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler" @@ -394,7 +329,7 @@ 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) ;dummy_tac + Posix.Process.sleep(Time.fromSeconds 1); all_tac end @@ -408,34 +343,29 @@ (* get vampire axiom names *) (***********************************) - val (axiom_names) = get_axiom_names_vamp proofstr thms clause_arr num_of_clauses + val axiom_names = get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^ rules_to_string axiom_names in File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^" "^goalstring); TextIO.output (toParent, ax_str^"\n"); - TextIO.flushOut toParent; TextIO.output (toParent, "goalstring: "^goalstring^"\n"); - TextIO.flushOut toParent; TextIO.output (toParent, "thmstring: "^thmstring^"\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) ; dummy_tac + Posix.Process.sleep(Time.fromSeconds 1) ; all_tac end handle _ => let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler" in TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) ); - 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) ;dummy_tac + Posix.Process.sleep(Time.fromSeconds 1); all_tac end; @@ -446,42 +376,35 @@ (string_of_int num_of_clauses)) (***********************************) - (* get vampire axiom names *) + (* get E axiom names *) (***********************************) - val (axiom_names) = get_axiom_names_E proofstr thms clause_arr num_of_clauses + val axiom_names = get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses val ax_str = "Rules from clasimpset used in proof found by E: " ^ rules_to_string axiom_names in File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^" "^goalstring); TextIO.output (toParent, ax_str^"\n"); TextIO.flushOut toParent; - TextIO.output (toParent, "goalstring: "^goalstring^"\n"); - TextIO.flushOut toParent; TextIO.output (toParent, "thmstring: "^thmstring^"\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) ; dummy_tac + Posix.Process.sleep(Time.fromSeconds 1) ; all_tac end handle _ => let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler" in - TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) ); - TextIO.flushOut toParent; + TextIO.output (toParent,"Proof found by E but translation failed for resolution proof: "^(remove_linebreaks proofstr) ); 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) ;dummy_tac + Posix.Process.sleep(Time.fromSeconds 1); all_tac end; -(* val proofstr = "1582[0:Inp] || -> v_P*.\ - \1583[0:Inp] || v_P* -> .\ - \1584[0:MRR:1583.0,1582.0] || -> ."; *) fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = let val _ = File.write(File.tmp_path (Path.basic "thmstringfile")) @@ -491,8 +414,7 @@ (***********************************) (* parse spass proof into datatype *) (***********************************) - val proof_steps1 = parse tokens - val proof_steps = just_change_space proof_steps1 + val proof_steps = parse tokens val _ = File.write (File.tmp_path (Path.basic "foo_parse")) ("Did parsing on "^proofstr) @@ -550,7 +472,7 @@ 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) ; dummy_tac + Posix.Process.sleep(Time.fromSeconds 1) ; all_tac end handle _ => let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler" @@ -563,7 +485,7 @@ 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) ;dummy_tac + Posix.Process.sleep(Time.fromSeconds 1); all_tac end @@ -643,8 +565,9 @@ (** change this to allow P (x U) *) - fun arglist_step input = ( word ++ many word >> (fn (a, b) => (a^" "^(implode_with_space b))) - ||word >> (fn (a) => (a)))input + fun arglist_step input = + ( word ++ many word >> (fn (a, b) => (a^" "^(space_implode " " b))) + ||word >> (fn (a) => (a)))input fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++ a (Other ")") diff -r 6cef3aedd661 -r 5cde710a8a23 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Wed Sep 07 09:54:31 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Wed Sep 07 18:14:26 2005 +0200 @@ -328,76 +328,63 @@ 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 _ = (warning ("subgoals forked to startWatcher: "^prems_string)); - (* tracing *) - (*val tenth_ax = fst( Array.sub(clause_arr, 1)) - val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab) - val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) - val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax)) - val _ = (warning ("tenth axiom in table in watcher is: "^clause_str)) - val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) ) - *) - (*val goalstr = string_of_thm (the_goal) - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher"))); - val _ = TextIO.output (outfile,goalstr ) - val _ = TextIO.closeOut outfile*) + val _ = debug ("subgoals forked to startWatcher: "^prems_string); fun killChildren [] = () - | killChildren (child_handle::children) = (killChild child_handle; killChildren children) + | killChildren (child_handle::children) = + (killChild child_handle; killChildren children) (*************************************************************) (* take an instream and poll its underlying reader for input *) (*************************************************************) fun pollParentInput () = - let val pd = OS.IO.pollDesc (fromParentIOD) - in - if (isSome pd ) then - let val pd' = OS.IO.pollIn (valOf pd) - val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) - val _ = File.append (File.tmp_path (Path.basic "parent_poll")) - ("In parent_poll\n") - in - if null pdl - then - NONE - else if (OS.IO.isIn (hd pdl)) - then SOME (getCmds (toParentStr, fromParentStr, [])) - else NONE - end - else NONE - end + let val pd = OS.IO.pollDesc (fromParentIOD) + in + if isSome pd then + let val pd' = OS.IO.pollIn (valOf pd) + val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) + val _ = File.append (File.tmp_path (Path.basic "parent_poll")) + ("In parent_poll\n") + in + if null pdl + then + NONE + else if (OS.IO.isIn (hd pdl)) + then SOME (getCmds (toParentStr, fromParentStr, [])) + else NONE + end + else NONE + end fun pollChildInput (fromStr) = - let val _ = File.append (File.tmp_path (Path.basic "child_poll")) - ("In child_poll\n") - val iod = getInIoDesc fromStr - in - if isSome iod - then - let val pd = OS.IO.pollDesc (valOf iod) - in - if (isSome pd ) then - let val pd' = OS.IO.pollIn (valOf pd) - val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) - in - if null pdl - then - ( File.append (File.tmp_path (Path.basic "child_poll_res")) - ("Null pdl \n");NONE) - else if (OS.IO.isIn (hd pdl)) - then - (let val inval = (TextIO.inputLine fromStr) - val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n") - in - SOME inval - end) - else - ( File.append (File.tmp_path (Path.basic "child_poll_res")) - ("Null pdl \n");NONE) - end - else NONE - end - else NONE + let val _ = File.append (File.tmp_path (Path.basic "child_poll")) + ("In child_poll\n") + val iod = getInIoDesc fromStr + in + if isSome iod + then + let val pd = OS.IO.pollDesc (valOf iod) + in + if isSome pd then + let val pd' = OS.IO.pollIn (valOf pd) + val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) + in + if null pdl + then + (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl\n"; + NONE) + else if OS.IO.isIn (hd pdl) + then + let val inval = (TextIO.inputLine fromStr) + val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n") + in SOME inval end + else + (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl \n"; + NONE) + end + else NONE + end + else NONE end @@ -434,37 +421,37 @@ 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 _ = warning("subgoals forked to checkChildren: "^prems_string) + val _ = debug("subgoals forked to checkChildren: "^prems_string) val goalstring = cmdGoal childProc val _ = File.append (File.tmp_path (Path.basic "child_comms")) (prover^thmstring^goalstring^childCmd^"\n") in - if (isSome childIncoming) + 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^thmstring^goalstring^childCmd) - val childDone = (case prover of - "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) - | "E" => (EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) - |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) - in - if childDone (**********************************************) - then (* child has found a proof and transferred it *) - (* Remove this child and go on to check others*) - (**********************************************) - (Unix.reap child_handle; - checkChildren(otherChildren, toParentStr)) - else - (**********************************************) - (* Keep this child and go on to check others *) - (**********************************************) - (childProc::(checkChildren (otherChildren, toParentStr))) - end - else - (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output "; - childProc::(checkChildren (otherChildren, toParentStr))) + (* 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^thmstring^goalstring^childCmd) + val childDone = (case prover of + "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) + | "E" => EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) + |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) + in + if childDone (**********************************************) + then (* child has found a proof and transferred it *) + (* Remove this child and go on to check others*) + (**********************************************) + (Unix.reap child_handle; + checkChildren(otherChildren, toParentStr)) + else + (**********************************************) + (* Keep this child and go on to check others *) + (**********************************************) + (childProc::(checkChildren (otherChildren, toParentStr))) + end + else + (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output "; + childProc::(checkChildren (otherChildren, toParentStr))) end @@ -480,7 +467,7 @@ fun execCmds [] procList = procList | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child")) ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) in - if (prover = "spass") + if prover = "spass" then let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) @@ -495,7 +482,8 @@ outstr = outstr })::procList)) val _ = File.append (File.tmp_path (Path.basic "exec_child")) ("\nexecuting command for goal:\n"^ - goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) + goalstring^proverCmd^(concat settings)^file^ + " at "^(Date.toString(Date.fromTimeLocal(Time.now())))) in Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList @@ -546,31 +534,33 @@ (**********************************************) (* Watcher Loop *) (**********************************************) + val iterations_left = ref 1000; (*200 seconds, 5 iterations per sec*) fun keepWatching (toParentStr, fromParentStr,procList) = let fun loop (procList) = let val _ = Posix.Process.sleep (Time.fromMilliseconds 200) val cmdsFromIsa = pollParentInput () - fun killchildHandler (n:int) = - (TextIO.output(toParentStr, "Killing child proof processes!\n"); + fun killchildHandler () = + (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); TextIO.flushOut toParentStr; killChildren (map (cmdchildHandle) procList); ()) in (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) - (**********************************) - if (isSome cmdsFromIsa) + iterations_left := !iterations_left - 1; + if !iterations_left = 0 then killchildHandler () + else if isSome cmdsFromIsa then (* deal with input from Isabelle *) - if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" ) + if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" then let val child_handles = map cmdchildHandle procList in killChildren child_handles; (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) - loop ([]) + loop [] end else - if ((length procList)<10) (********************) + if length procList < 5 (********************) then (* Execute locally *) let val newProcList = execCmds (valOf cmdsFromIsa) procList @@ -578,10 +568,10 @@ val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ") val newProcList' =checkChildren (newProcList, toParentStr) - val _ = warning("off to keep watching...") + val _ = debug("off to keep watching...") val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ") in - loop (newProcList') + loop newProcList' end else (* Execute remotely *) (* (actually not remote for now )*) @@ -590,17 +580,17 @@ val parentID = Posix.ProcEnv.getppid() val newProcList' =checkChildren (newProcList, toParentStr) in - loop (newProcList') + loop newProcList' end 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 "); - loop (newProcList) + loop newProcList end end in - loop (procList) + loop procList end @@ -678,7 +668,8 @@ status end -fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = + +fun createWatcher (thm,clause_arr, num_of_clauses) = let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses)) val streams = snd mychild val childin = fst streams @@ -687,34 +678,33 @@ 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 _ = (warning ("subgoals forked to createWatcher: "^prems_string)); + 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 outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1"))); - val _ = TextIO.output (outfile, ("In signal handler now\n")) - val _ = TextIO.closeOut outfile + let val _ = File.append (File.tmp_path (Path.basic "spass_signal_in")) + "Starting SPASS signal handler\n" val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin - val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal"))); - - val _ = TextIO.output (outfile, ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))) - val _ = TextIO.closeOut outfile + val _ = File.append (File.tmp_path (Path.basic "spass_signal_out")) + ("In SPASS signal handler "^reconstr^thmstring^goalstring^ + "goals_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) = "[" then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); Recon_Transfer.apply_res_thm reconstr goalstring; Pretty.writeln(Pretty.str (oct_char "361")); - goals_being_watched := ((!goals_being_watched) - 1); + goals_being_watched := (!goals_being_watched) - 1; - if (!goals_being_watched) = 0 + if !goals_being_watched = 0 then - let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found")) - ("Reaping a watcher, goals watched is: "^ - (string_of_int (!goals_being_watched))^"\n") + let val _ = File.write (File.tmp_path (Path.basic "reap_found")) + ("Reaping a watcher, goals watched now "^ + string_of_int (!goals_being_watched)^"\n") in - killWatcher (childpid); reapWatcher (childpid,childin, childout); () + killWatcher childpid; reapWatcher (childpid,childin, childout); () end else () ) (* if there's no proof, but a message from Spass *) diff -r 6cef3aedd661 -r 5cde710a8a23 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Sep 07 09:54:31 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Wed Sep 07 18:14:26 2005 +0200 @@ -8,9 +8,7 @@ signature RES_ATP = sig val axiom_file : Path.T - val full_spass: bool ref - val spass: bool ref - val vampire: bool ref + val prover: string ref val custom_spass: string list ref val hook_count: int ref end; @@ -24,9 +22,7 @@ fun debug_tac tac = (debug "testing"; tac); -val vampire = ref false; (* use Vampire as default prover? *) -val spass = ref true; (* use spass as default prover *) -val full_spass = ref true; (*specifies Auto mode: SPASS can use all inference rules*) +val prover = ref "spass"; (* use spass as default prover *) val custom_spass = (*specialized options for SPASS*) ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub", "-DocProof","-TimeLimit=60"]; @@ -130,8 +126,7 @@ (*********************************************************************) -(* call SPASS with settings and problem file for the current subgoal *) -(* should be modified to allow other provers to be called *) +(* call prover with settings and problem file for the current subgoal *) (*********************************************************************) (* now passing in list of skolemized thms and list of sgterms to go with them *) fun call_resolve_tac (thms: thm list list) sign (sg_terms: term list) (childin, childout,pid) n = @@ -152,12 +147,14 @@ val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n) val _ = debug ("prob file in call_resolve_tac is " ^ probfile) in - if !spass + if !prover = "spass" then - let val optionline = (*Custom SPASS options, or default?*) - if !full_spass (*Auto mode: all SPASS inference rules*) - then "-DocProof%-TimeLimit=60%-SOS" - else "-" ^ space_implode "%-" (!custom_spass) + let val optionline = + if !SpassComm.reconstruct + (*Proof reconstruction works for only a limited set of + inference rules*) + then "-" ^ space_implode "%-" (!custom_spass) + else "-DocProof%-TimeLimit=60%-SOS" (*Auto mode*) val _ = debug ("SPASS option string is " ^ optionline) val _ = ResLib.helper_path "SPASS_HOME" "SPASS" (*We've checked that SPASS is there for ATP/spassshell to run.*) @@ -167,7 +164,7 @@ optionline, axfile, hypsfile, probfile)] @ (make_atp_list xs sign (n+1))) end - else if !vampire + else if !prover = "vampire" then let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel" in @@ -175,14 +172,16 @@ axfile, hypsfile, probfile)] @ (make_atp_list xs sign (n+1))) end - else - let val Eprover = ResLib.helper_path "E_HOME" "eproof" - in - ([("E", thmstr, goalstring, Eprover, "--tptp-in -l5", - axfile, hypsfile, probfile)] @ - (make_atp_list xs sign (n+1))) - end - + else if !prover = "E" + then + let val Eprover = ResLib.helper_path "E_HOME" "eproof" + in + ([("E", thmstr, goalstring, Eprover, + "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60", + axfile, hypsfile, probfile)] @ + (make_atp_list xs sign (n+1))) + end + else error ("Invalid prover name: " ^ !prover) end val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1 @@ -205,15 +204,15 @@ all_tac thm) else - ( SELECT_GOAL + (SELECT_GOAL (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, METAHYPS(fn negs => - (if !spass + (if !prover = "spass" then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses; get_sko_thms tfrees sign sg_terms (childin, childout, pid) - thm (n -1) (negs::sko_thms) axclauses; - all_tac))]) n thm ) + thm (n-1) (negs::sko_thms) axclauses; + all_tac))]) n thm) @@ -223,36 +222,20 @@ (* in proof reconstruction *) (**********************************************) -fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) axclauses = - let - val prems = Thm.prems_of thm - (*val sg_term = get_nth k prems*) - val sign = sign_of_thm thm - val thmstring = string_of_thm thm +fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) axclauses = + let val tfree_lits = isar_atp_h thms + val prems = Thm.prems_of thm + val sign = sign_of_thm thm + val thmstring = string_of_thm thm in - debug("in isar_atp_goal'"); + debug ("in isar_atp_aux"); debug("thmstring in isar_atp_goal': " ^ thmstring); (* go and call callResProvers with this subgoal *) (* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *) (* recursive call to pick up the remaining subgoals *) (* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *) - get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n [] axclauses - end; - - -(**************************************************) -(* convert clauses from "assume" to conjecture. *) -(* i.e. apply make_clauses and then get tptp for *) -(* any hypotheses in the goal produced by assume *) -(* statements; *) -(* write to file "hyps" *) -(**************************************************) - -fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) axclauses = - let val tfree_lits = isar_atp_h thms - in - debug ("in isar_atp_aux"); - isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) axclauses + get_sko_thms tfree_lits sign prems (childin, childout, pid) + thm n_subgoals [] axclauses end; (******************************************************************) @@ -270,7 +253,6 @@ 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 thm_string = string_of_thm thm 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*) @@ -282,7 +264,6 @@ string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid))) in debug ("initial thms: " ^ thms_string); - debug ("initial thm: " ^ thm_string); debug ("subgoals: " ^ prems_string); debug ("pid: "^ pid_string); isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;