Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
recon_transfer_proof.ML to deal with the E theorem prover.
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Sep 02 17:55:24 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Sep 02 21:29:33 2005 +0200
@@ -217,6 +217,26 @@
end
+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
+
(***********************************************)
(* get axioms for reconstruction *)
(***********************************************)
@@ -419,6 +439,46 @@
end;
+fun EString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses =
+ let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
+ (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
+ "goalstr is: "^goalstring^" num of clauses is: "^
+ (string_of_int num_of_clauses))
+
+ (***********************************)
+ (* get vampire axiom names *)
+ (***********************************)
+
+ val (axiom_names) = get_axiom_names_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
+ 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
+ end;
+
(* val proofstr = "1582[0:Inp] || -> v_P*.\
\1583[0:Inp] || v_P* -> .\
\1584[0:MRR:1583.0,1582.0] || -> ."; *)
--- a/src/HOL/Tools/ATP/watcher.ML Fri Sep 02 17:55:24 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Fri Sep 02 21:29:33 2005 +0200
@@ -502,7 +502,8 @@
("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) )
+ "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 (**********************************************)
--- a/src/HOL/Tools/res_atp.ML Fri Sep 02 17:55:24 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Sep 02 21:29:33 2005 +0200
@@ -189,13 +189,22 @@
optionline, clasimpfile, axfile, hypsfile, probfile)] @
(make_atp_list xs sign (n+1)))
end
- else
+ else if !vampire
+ then
let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
in
([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
clasimpfile, 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",
+ clasimpfile, axfile, hypsfile, probfile)] @
+ (make_atp_list xs sign (n+1)))
+ end
+
end
val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1