--- 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;
--- 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;
--- 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;
--- 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;
--- 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 ")")
--- 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 *)
--- 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;