Corrected the problem with the ATP directory.
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Wed Apr 20 17:19:42 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Wed Apr 20 18:01:50 2005 +0200
@@ -26,14 +26,57 @@
(**********************************************************************)
+val atomize_tac =
+ SUBGOAL
+ (fn (prop,_) =>
+ let val ts = Logic.strip_assums_hyp prop
+ in EVERY1
+ [METAHYPS
+ (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
+ REPEAT_DETERM_N (length ts) o (etac thin_rl)]
+ end);
-fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString) = let
+
+fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num =
+ let val foo = TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar3")));
+ in
+SELECT_GOAL
+ (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
+ METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs))]) sg_num
+ end ;
+
+
+fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let
val thisLine = TextIO.inputLine fromChild
in
if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
then (
let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
- val reconstr = Recon_Transfer.spassString_to_reconString (currentString^thisLine) thmstring
+ val foo = TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
+
+ in
+
+ TextIO.output(foo,(proofextract));TextIO.closeOut foo;
+ reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num thm
+
+ end
+ )
+ else (
+
+ transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
+ )
+ end;
+
+
+(*
+
+fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let
+ val thisLine = TextIO.inputLine fromChild
+ in
+ if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
+ then (
+ let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
+ val reconstr = Recon_Transfer.spassString_to_reconString (currentString^thisLine) thmstring thm sg_num
val foo = TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
in
TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
@@ -54,11 +97,11 @@
)
else (
- transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine))
+ transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
)
end;
-
+*)
(*********************************************************************************)
(* Inspect the output of a Spass process to see if it has found a proof, *)
@@ -66,9 +109,10 @@
(*********************************************************************************)
-fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) =
+fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num) =
(*let val _ = Posix.Process.wait ()
in*)
+
if (isSome (TextIO.canInput(fromChild, 5)))
then
(
@@ -77,24 +121,28 @@
if (String.isPrefix "Here is a proof" thisLine )
then
(
-
-
- transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine);
- true)
+ let
+ val outfile = TextIO.openAppend(File.sysify_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);
+ true
+ end)
else
(
- startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd)
+ startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num)
)
end
)
else (false)
(* end*)
-fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd) =
+fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num) =
let val spass_proof_file = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));
- val _ = TextIO.output (outfile, "checking proof found")
+ val _ = TextIO.output (outfile, "checking proof found, thm is: "^(string_of_thm thm))
val _ = TextIO.closeOut outfile
in
@@ -105,19 +153,19 @@
in if ( thisLine = "SPASS beiseite: Proof found.\n" )
then
(
- let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
in
- startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd)
+ startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num)
end
)
else if (thisLine= "SPASS beiseite: Completion found.\n" )
then
(
- let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
@@ -166,7 +214,7 @@
else
(TextIO.output (spass_proof_file, (thisLine));
TextIO.flushOut spass_proof_file;
- checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd))
+ checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num))
end
)
@@ -255,6 +303,6 @@
end
else
- ("No output from Spass.\n","","")
+ ("No output from reconstruction process.\n","","")
--- a/src/HOL/Tools/ATP/modUnix.ML Wed Apr 20 17:19:42 2005 +0200
+++ b/src/HOL/Tools/ATP/modUnix.ML Wed Apr 20 18:01:50 2005 +0200
@@ -8,8 +8,9 @@
val fromStatus = Posix.Process.fromStatus
+
fun reap(pid, instr, outstr) =
- let
+ let
val u = TextIO.closeIn instr;
val u = TextIO.closeOut outstr;
@@ -20,10 +21,10 @@
end
fun fdReader (name : string, fd : Posix.IO.file_desc) =
- Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
+ Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd };
fun fdWriter (name, fd) =
- Posix.IO.mkTextWriter {
+ Posix.IO.mkWriter {
appendMode = false,
initBlkMode = true,
name = name,
--- a/src/HOL/Tools/ATP/recon_prelim.ML Wed Apr 20 17:19:42 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_prelim.ML Wed Apr 20 18:01:50 2005 +0200
@@ -1,3 +1,4 @@
+
Goal "A -->A";
by Auto_tac;
@@ -194,7 +195,31 @@
fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
+exception powerError;
+fun power (x, n) = if x = 0 andalso n = 0
+ then raise powerError
+ else if n = 0
+ then 1
+ else x * power (x, n-1);
+
+
+fun get_tens n = power(10, (n-1))
+
+
+fun digits_to_int [] posn n = n
+| digits_to_int (x::xs) posn n = let
+ val digit_val = ((ord x) - 48)*(get_tens posn)
+ in
+ digits_to_int xs (posn -1 )(n + digit_val)
+ end;
+
+fun int_of_string str = let
+ val digits = explode str
+ val posn = length digits
+ in
+ digits_to_int digits posn 0
+ end
exception ASSERTION of string;
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Apr 20 17:19:42 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Apr 20 18:01:50 2005 +0200
@@ -151,17 +151,19 @@
| thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
- fun get_axioms_used proof_steps thmstring = let
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
+ fun get_axioms_used proof_steps thms = let
+ (*val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
val _ = TextIO.output (outfile, thmstring)
- val _ = TextIO.closeOut outfile
+ val _ = TextIO.closeOut outfile*)
(* 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 []
- val thm = thm_of_string thmstring
- val clauses = make_clauses [thm]
+
+
+ val clauses = make_clauses thms
val vars = map thm_vars clauses
@@ -298,14 +300,20 @@
*)
+val dummy_tac = PRIMITIVE(fn thm => thm );
-fun spassString_to_reconString proofstr thmstring =
- let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile"))); val _= warning("proofstr is: "^proofstr);
- val _ = warning ("thmstring is: "^thmstring);
- val _ = TextIO.output (outfile, (thmstring))
+fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms=
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));
+ (* val sign = sign_of_thm thm
+ val prems = prems_of thm
+ val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
+ val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
+ val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
+ (*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
val _ = TextIO.closeOut outfile
- val proofextract = extract_proof proofstr
- val tokens = #1(lex proofextract)
+
+ val tokens = #1(lex proofstr)
+
(***********************************)
(* parse spass proof into datatype *)
@@ -324,7 +332,9 @@
(************************************)
(* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
- val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thmstring
+ (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
+ (* subgoal this is, and turn it into meta_clauses *)
+ val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms
(*val numcls_string = numclstr ( vars, numcls) ""*)
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms")
@@ -357,15 +367,29 @@
val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
val _ = TextIO.closeOut outfile
+ val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
in
- (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
+ TextIO.output (toParent, reconstr^"\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 *)
+ OS.Process.sleep(Time.fromSeconds 1) ; dummy_tac
end
handle _ => (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
val _ = TextIO.output (outfile, ("In exception handler"));
val _ = TextIO.closeOut outfile
in
- "Proof found but translation failed!"
+ TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
+ TextIO.flushOut toParent;
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+ (* Attempt to prevent several signals from turning up simultaneously *)
+ OS.Process.sleep(Time.fromSeconds 1) ;dummy_tac
end)
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Wed Apr 20 17:19:42 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Wed Apr 20 18:01:50 2005 +0200
@@ -1,5 +1,7 @@
(* Get claset rules *)
+
+
fun remove_all [] rules = rules
| remove_all (x::xs) rules = let val rules' = List.filter (not_equal x) rules
in
@@ -23,6 +25,94 @@
val clause_arr = Array.array(3500, ("empty", 0));
+val foo_arr = Array.array(20, ("a",0));
+
+
+(*
+
+fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)];
+
+
+
+
+fun setupFork () = let
+ (** pipes for communication between parent and watcher **)
+ val p1 = Posix.IO.pipe ()
+ val p2 = Posix.IO.pipe ()
+ fun closep () = (
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p1);
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p2)
+ )
+ (***********************************************************)
+ (****** fork a watcher process and get it set up and going *)
+ (***********************************************************)
+ fun startFork () =
+ (case Posix.Process.fork() (***************************************)
+ of SOME pid => pid (* parent - i.e. main Isabelle process *)
+ (***************************************)
+
+ (*************************)
+ | NONE => let (* child - i.e. watcher *)
+ val oldchildin = #infd p1 (*************************)
+ val fromParent = Posix.FileSys.wordToFD 0w0
+ val oldchildout = #outfd p2
+ val toParent = Posix.FileSys.wordToFD 0w1
+ val fromParentIOD = Posix.FileSys.fdToIOD fromParent
+ val fromParentStr = openInFD ("_exec_in_parent", fromParent)
+ val toParentStr = openOutFD ("_exec_out_parent", toParent)
+ val fooax = fst(Array.sub(foo_arr, 3))
+ val outfile = TextIO.openOut("/homes/clq20/Jia_Code/fork");
+ val _ = TextIO.output (outfile, ("fooax 3 is: "^fooax))
+ val _ = TextIO.closeOut outfile
+ in
+ (***************************)
+ (*** Sort out pipes ********)
+ (***************************)
+
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p2);
+ Posix.IO.dup2{old = oldchildin, new = fromParent};
+ Posix.IO.close oldchildin;
+ Posix.IO.dup2{old = oldchildout, new = toParent};
+ Posix.IO.close oldchildout;
+
+ (***************************)
+ (* start the watcher loop *)
+ (***************************)
+
+ (****************************************************************************)
+ (* fake return value - actually want the watcher to loop until killed *)
+ (****************************************************************************)
+ Posix.Process.wordToPid 0w0
+
+ end)
+ val start = startFork()
+ in
+
+
+ (*******************************)
+ (* close the child-side fds *)
+ (*******************************)
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p1);
+ (* set the fds close on exec *)
+ Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+
+ (*******************************)
+ (* return value *)
+ (*******************************)
+ ()
+ end;
+
+
+
+*)
+
+
+
fun multi x 0 xlist = xlist
|multi x n xlist = multi x (n -1 ) (x::xlist);
@@ -91,7 +181,10 @@
val clause_arr = Array.array(3500, ("empty", 0));
-fun write_out_clasimp filename = let
+fun write_out_clasimp filename (clause_arr:(string * int) Array.array) = let
+ val outfile = TextIO.openOut("wibble"); val _ = TextIO.output (outfile, ("in write_out_clasimpset"))
+ val _ = TextIO.closeOut outfile
+ val _= (warning ("in writeoutclasimp"))
(****************************************)
(* add claset rules to array and write out as strings *)
(****************************************)
@@ -127,9 +220,7 @@
(* create array and put clausename, number pairs into it *)
(*******************************************)
- val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
-
-
+ val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
val _= num_of_clauses := (List.length cl_long_name_nums);
(*************************************)
@@ -147,7 +238,9 @@
(*********************)
(* Get simpset rules *)
(*********************)
+
val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
+
val named_simps = List.filter has_name_pair simpset_name_rules;
val simp_names = map #1 named_simps;
@@ -183,11 +276,11 @@
val tptplist = (stick stick_strs)
-
in
ResLib.writeln_strs out tptplist;
TextIO.flushOut out;
- TextIO.closeOut out
+ TextIO.closeOut out;
+ clause_arr
end;
(*
--- a/src/HOL/Tools/ATP/watcher.ML Wed Apr 20 17:19:42 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Wed Apr 20 18:01:50 2005 +0200
@@ -75,32 +75,43 @@
(* Send request to Watcher for multiple provers to be called for filenames in arg *)
(*****************************************************************************************)
+
+
(* need to modify to send over hyps file too *)
fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n");
TextIO.flushOut toWatcherStr)
-| callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,probfile)::args) =
- let
- val dfg_dir = File.tmp_path (Path.basic "dfg");
- (* need to check here if the directory exists and, if not, create it*)
- val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic"thmstring_in_watcher")));
- val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
+| callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
+ let val dfg_dir = File.tmp_path (Path.basic "dfg");
+ (*** need to check here if the directory exists and, if not, create it***)
+ val outfile = TextIO.openAppend(File.sysify_path
+ (File.tmp_path (Path.basic"thmstring_in_watcher"))); val _ = TextIO.output (outfile,
+ (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
val _ = TextIO.closeOut outfile
+ (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
+ val probID = last(explode probfile)
+ val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
+ (*** only include problem and clasimp for the moment, not sure how to refer to ***)
+ (*** hyps/local axioms just now ***)
+ val whole_prob_file = Unix.execute("/bin/cat", [(*clasimpfile, axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)])
val dfg_create =if File.exists dfg_dir
then
- ()
+ ((warning("dfg dir exists"));())
else
File.mkdir dfg_dir;
- val probID = last(explode probfile)
+
val dfg_path = File.sysify_path dfg_dir;
- val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v2.6.0/TPTP2X/tptp2X", ["-fdfg "^probfile^" -d "^dfg_path])
+ val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",
+ ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
(*val _ = Posix.Process.wait ()*)
(*val _ =Unix.reap exec_tptp2x*)
- val newfile = dfg_path^"/prob"^"_"^(probID)^".dfg"
+ val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
in
goals_being_watched := (!goals_being_watched) + 1;
OS.Process.sleep(Time.fromSeconds 1);
+ (warning ("probfile is: "^probfile));
(warning("dfg file is: "^newfile));
+ (warning ("wholefile is: "^(File.sysify_path wholefile)));
sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
TextIO.flushOut toWatcherStr;
Unix.reap exec_tptp2x;
@@ -108,13 +119,13 @@
callResProvers (toWatcherStr,args)
end
-
+(*
fun callResProversStr (toWatcherStr, []) = "End of calls\n"
-| callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings, file)::args) =
- ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^file^"\n")
+| callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) =
+ ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n")
- )
+ *)
(**************************************************************)
(* Send message to watcher to kill currently running vampires *)
@@ -233,7 +244,7 @@
-fun setupWatcher () = let
+fun setupWatcher (thm) = let
(** pipes for communication between parent and watcher **)
val p1 = Posix.IO.pipe ()
val p2 = Posix.IO.pipe ()
@@ -260,6 +271,10 @@
val fromParentIOD = Posix.FileSys.fdToIOD fromParent
val fromParentStr = openInFD ("_exec_in_parent", fromParent)
val toParentStr = openOutFD ("_exec_out_parent", toParent)
+ val sign = sign_of_thm thm
+ val prems = prems_of thm
+ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
+ val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
(*val goalstr = string_of_thm (the_goal)
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));
val _ = TextIO.output (outfile,goalstr )
@@ -333,12 +348,20 @@
| checkChildren ((childProc::otherChildren), toParentStr) =
let val (childInput,childOutput) = cmdstreamsOf childProc
val childPid = cmdchildPid childProc
+ (* childCmd is the .dfg file that the problem is in *)
val childCmd = fst(snd (cmdchildInfo childProc))
+ (* now get the number of the subgoal from the filename *)
+ val sg_num = int_of_string(get_nth 5 (rev(explode childCmd)))
val childIncoming = pollChildInput childInput
val parentID = Posix.ProcEnv.getppid()
val prover = cmdProver childProc
val thmstring = cmdThm childProc
+ val sign = sign_of_thm thm
+ val prems = prems_of thm
+ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
+ val _ = (warning ("subgoals forked to checkChildren: "^prems_string));
val goalstring = cmdGoal childProc
+
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));
val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
val _ = TextIO.closeOut outfile
@@ -348,10 +371,10 @@
(* check here for prover label on child*)
let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));
- val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
+ val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
val _ = TextIO.closeOut outfile
val childDone = (case prover of
- (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd) ) )
+ (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num) ) )
in
if childDone (**********************************************)
then (* child has found a proof and transferred it *)
@@ -386,6 +409,7 @@
(* takes list of (string, string, string list, string)list proclist *)
(********************************************************************)
+ (*** add subgoal id num to this *)
fun execCmds [] procList = procList
| execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList =
if (prover = "spass")
@@ -563,63 +587,19 @@
(**********************************************************)
fun killWatcher pid= killChild pid;
-fun createWatcher () = let val mychild = childInfo (setupWatcher())
+fun createWatcher (thm) = let val mychild = childInfo (setupWatcher(thm))
val streams =snd mychild
val childin = fst streams
val childout = snd streams
val childpid = fst mychild
-
+ 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));
fun vampire_proofHandler (n) =
(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() )
+ getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() )
- (* fun spass_proofHandler (n:int) = (
- let val (reconstr, thmstring, goalstring) = getSpassInput childin
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
-
- val _ = TextIO.output (outfile, ("In signal handler "^reconstr^" "^thmstring))
- val _ = TextIO.closeOut outfile
- in
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str reconstr) ;
- Pretty.writeln(Pretty.str (oct_char "361"));
- (*killWatcher childpid;*) ()
- end)*)
-
-
-(*
-
-fun spass_proofHandler (n:int) = (
- let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
-
- val _ = TextIO.output (outfile, ("In signal handler now\n"))
- val _ = TextIO.closeOut outfile
- val (reconstr, thmstring, goalstring) = getSpassInput childin
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
-
- val _ = TextIO.output (outfile, ("In signal handler "^reconstr^" "^thmstring^goalstring))
- val _ = TextIO.closeOut outfile
- in
- if ( (substring (reconstr, 0,1))= "[")
- then
-
- let val thm = thm_of_string thmstring
- val clauses = make_clauses [thm]
- val numcls = ListPair.zip (numlist (length clauses), map make_meta_clause clauses)
-
- in
- 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"));
- killWatcher childpid; ()
- end
- else
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str (goalstring^reconstr));
- Pretty.writeln(Pretty.str (oct_char "361"));
- (*killWatcher childpid; *) reap (childpid,childin, childout);()
- end )
-*)
fun spass_proofHandler (n) = (
let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
@@ -699,8 +679,7 @@
- in
- IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
+ in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
(childin, childout, childpid)
--- a/src/HOL/Tools/ATP/watcher.sig Wed Apr 20 17:19:42 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.sig Wed Apr 20 18:01:50 2005 +0200
@@ -21,7 +21,7 @@
(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
(*****************************************************************************************)
-val callResProvers : TextIO.outstream *(string* string*string *string*string*string) list -> unit
+val callResProvers : TextIO.outstream *(string* string*string *string*string*string*string*string*string) list -> unit
@@ -37,7 +37,7 @@
(* Start a watcher and set up signal handlers *)
(**********************************************************)
-val createWatcher : unit -> TextIO.instream * TextIO.outstream * Posix.Process.pid
+val createWatcher : Thm.thm -> TextIO.instream * TextIO.outstream * Posix.Process.pid
--- a/src/HOL/Tools/res_atp.ML Wed Apr 20 17:19:42 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Wed Apr 20 18:01:50 2005 +0200
@@ -291,8 +291,8 @@
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
(* set up variables for writing out the clasimps to a tptp file *)
- (* val clause_arr = write_out_clasimp (File.sysify_path clasimp_file) clause_arr*)
- (*val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) ) *)
+ val clause_arr = write_out_clasimp (File.sysify_path clasimp_file) clause_arr
+ val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )
(* cq: add write out clasimps to file *)
(* cq:create watcher and pass to isar_atp_aux *)
(*val tenth_ax = fst( Array.sub(clause_arr, 10))