# HG changeset patch # User quigley # Date 1114012910 -7200 # Node ID a1863ea9052b525fb48ad9d4c132e19917d0a61c # Parent 70d559802ae397109d4f32737a49decb26db339e Corrected the problem with the ATP directory. diff -r 70d559802ae3 -r a1863ea9052b src/HOL/Tools/ATP/SpassCommunication.ML --- 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","","") diff -r 70d559802ae3 -r a1863ea9052b src/HOL/Tools/ATP/modUnix.ML --- 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, diff -r 70d559802ae3 -r a1863ea9052b src/HOL/Tools/ATP/recon_prelim.ML --- 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; diff -r 70d559802ae3 -r a1863ea9052b src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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) diff -r 70d559802ae3 -r a1863ea9052b src/HOL/Tools/ATP/res_clasimpset.ML --- 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; (* diff -r 70d559802ae3 -r a1863ea9052b src/HOL/Tools/ATP/watcher.ML --- 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) diff -r 70d559802ae3 -r a1863ea9052b src/HOL/Tools/ATP/watcher.sig --- 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 diff -r 70d559802ae3 -r a1863ea9052b src/HOL/Tools/res_atp.ML --- 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))