# HG changeset patch # User quigley # Date 1115123241 -7200 # Node ID b30a35432f5a80ba4ea476c428711fd8b7289643 # Parent 6d6d3fabef02864dbd5872289041c9e9c8890f8c Replaced reference to SPASS with general one - set SPASS_HOME in settings file. Rewrote res_clasimpset.ML. Now produces an array of (thm, clause) in addition to writing out clasimpset as tptp strings. C.Q. diff -r 6d6d3fabef02 -r b30a35432f5a src/HOL/Tools/ATP/SpassCommunication.ML --- a/src/HOL/Tools/ATP/SpassCommunication.ML Tue May 03 10:33:31 2005 +0200 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML Tue May 03 14:27:21 2005 +0200 @@ -19,7 +19,6 @@ TextIO.output (fd, thisLine); logSpassInput (instr,fd)) end; - (**********************************************************************) (* Reconstruct the Spass proof w.r.t. thmstring (string version of *) (* Isabelle goal to be proved), then transfer the reconstruction *) @@ -38,16 +37,16 @@ end); -fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num = +fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr (num_of_clauses:int ) = 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 + METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString 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) = let +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" ) @@ -58,51 +57,18 @@ in TextIO.output(foo,(proofextract));TextIO.closeOut foo; - reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num thm + 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) + 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) = 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; - - 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 *) - Posix.Process.sleep(Time.fromSeconds 1); () - - end - - ) - else ( - - 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, *) @@ -110,7 +76,7 @@ (*********************************************************************************) -fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num) = +fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = (*let val _ = Posix.Process.wait () in*) @@ -127,20 +93,22 @@ 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); + 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) + 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) = + + +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.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, thm is: "^(string_of_thm thm)) @@ -159,7 +127,7 @@ val _ = TextIO.closeOut outfile in - startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num) + startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) end ) else if (thisLine= "SPASS beiseite: Completion found.\n" ) @@ -215,7 +183,7 @@ else (TextIO.output (spass_proof_file, (thisLine)); TextIO.flushOut spass_proof_file; - checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num)) + checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)) end ) @@ -229,36 +197,6 @@ (***********************************************************************) -(***********************************************************************) -(* Function used by the Isabelle process to read in a vampire proof *) -(***********************************************************************) - -(*fun getVampInput instr = let val thisLine = TextIO.inputLine instr - in - if (thisLine = "%============== End of proof. ==================\n" ) - then - ( - (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));() - ) - else if (thisLine = "% Unprovable.\n" ) - then - ( - (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));() - ) - else if (thisLine = "% Proof not found.\n") - then - ( - Pretty.writeln(Pretty.str (concat["vampire", thisLine]));() - ) - - - else - ( - Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr - ) - end; - -*) fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2))) then diff -r 6d6d3fabef02 -r b30a35432f5a src/HOL/Tools/ATP/recon_order_clauses.ML --- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 03 10:33:31 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 03 14:27:21 2005 +0200 @@ -242,7 +242,7 @@ (* resulting thm, clause-strs in spass order, vars *) fun rearrange_clause thm res_strlist allvars = - let val isa_strlist = get_meta_lits thm + let val isa_strlist = get_meta_lits thm (* change this to use Jia's code to get same looking thing as isastrlist? *) val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[]) val symmed = apply_rule sym symlist thm val not_symmed = apply_rule not_sym not_symlist symmed diff -r 6d6d3fabef02 -r b30a35432f5a src/HOL/Tools/ATP/recon_parse.ML --- a/src/HOL/Tools/ATP/recon_parse.ML Tue May 03 10:33:31 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_parse.ML Tue May 03 14:27:21 2005 +0200 @@ -405,10 +405,20 @@ val clause = term - val line = number ++ justification ++ a (Other "|") ++ + + + (*val line = number ++ justification ++ a (Other "|") ++ a (Other "|") ++ clause ++ a (Other ".") - >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c)) - + >> (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 diff -r 6d6d3fabef02 -r b30a35432f5a src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 03 10:33:31 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 03 14:27:21 2005 +0200 @@ -17,6 +17,39 @@ +(* +fun fill_cls_array array n [] = () +| fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x) + in + fill_cls_array array (n+1) (xs) + end; + + + +fun memo_add_clauses ((name:string, (cls:Thm.thm list)), symtable)= + symtable := Symtab.update((name , cls), !symtable); + + +fun memo_add_all ([], symtable) = () +| memo_add_all ((x::xs),symtable) = let val _ = memo_add_clauses (x, symtable) + in + memo_add_all (xs, symtable) + end + +fun memo_find_clause (name, (symtable: Thm.thm list Symtab.table ref)) = case Symtab.lookup (!symtable,name) of + NONE => [] + |SOME cls => cls ; + + +fun retrieve_clause array symtable clausenum = let + val (name, clnum) = Array.sub(array, clausenum) + val clauses = memo_find_clause (name, symtable) + val clause = get_nth clnum clauses + in + (name, clause) + end + *) + (* Versions that include type information *) fun string_of_thm thm = let val _ = set show_sorts @@ -146,8 +179,30 @@ fun thmstrings [] str = str | thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x)) +fun is_clasimp_ax clasimp_num n = n <=clasimp_num - fun get_axioms_used proof_steps thms = let + + +fun retrieve_axioms clause_arr [] = [] +| retrieve_axioms clause_arr (x::xs) = [Array.sub(clause_arr, x)]@ + (retrieve_axioms clause_arr xs) + + +(* retrieve the axioms that were obtained from the clasimpset *) + +fun get_clasimp_cls clause_arr clasimp_num step_nums = + let val clasimp_nums = List.filter (is_clasimp_ax clasimp_num) step_nums + in + retrieve_axioms clause_arr clasimp_nums + end + + + + +(* add array and table here, so can retrieve clasimp axioms *) + + fun get_axioms_used proof_steps thms clause_arr num_of_clauses = + let (*val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr"))) val _ = TextIO.output (outfile, thmstring) @@ -157,9 +212,21 @@ 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 clauses = make_clauses thms + + (***********************************************) + (* 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 outfile = TextIO.openAppend(File.sysify_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 @@ -215,7 +282,7 @@ val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*) in - (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas))) + (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas))) end fun numclstr (vars, []) str = str @@ -293,9 +360,12 @@ *) + + + val dummy_tac = PRIMITIVE(fn thm => thm ); -fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms= +fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = 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 @@ -307,7 +377,8 @@ val tokens = #1(lex proofstr) - + + (***********************************) (* parse spass proof into datatype *) (***********************************) @@ -327,7 +398,9 @@ (* get axioms as correctly numbered clauses w.r.t. the Spass proof *) (* 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 + (* should prob add array and table here, so that we can get axioms*) + (* produced from the clasimpset rather than the problem *) + val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses (*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") diff -r 6d6d3fabef02 -r b30a35432f5a src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 03 10:33:31 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 03 14:27:21 2005 +0200 @@ -67,9 +67,10 @@ fun reconstruction_failed fname = error (fname ^ ": reconstruction failed") -(****************************************) -(* Reconstruct an axiom resolution step *) -(****************************************) +(************************************************) +(* Reconstruct an axiom resolution step *) +(* clauses is a list of (clausenum,clause) pairs*) +(************************************************) fun follow_axiom clauses allvars (clausenum:int) thml clause_strs = let val this_axiom = valOf (assoc (clauses,clausenum)) diff -r 6d6d3fabef02 -r b30a35432f5a src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 03 10:33:31 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 03 14:27:21 2005 +0200 @@ -3,247 +3,76 @@ Copyright 2004 University of Cambridge *) -(* Get claset rules *) +signature RES_CLASIMP = + sig + val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int + end; + +structure ResClasimp : RES_CLASIMP = +struct fun has_name th = not((Thm.name_of_thm th)= "") fun has_name_pair (a,b) = not_equal a ""; -fun good_pair c (a,b) = not_equal b c; - - - -val num_of_clauses = ref 0; -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); - - -fun clause_numbering (name:string, cls) = let val num_of_cls = length cls - val numbers = 0 upto (num_of_cls -1) - val multi_name = multi name num_of_cls [] - in - ListPair.zip (multi_name,numbers) - end; fun stick [] = [] | stick (x::xs) = x@(stick xs ) - - -fun fill_cls_array array n [] = () -| fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x) - in - fill_cls_array array (n+1) (xs) - end; - - - -val nc = ref (Symtab.empty : (thm list) Symtab.table) - - - -fun memo_add_clauses (name:string, cls)= - nc := Symtab.update((name , cls), !nc); - - - -fun memo_find_clause name = case Symtab.lookup (!nc,name) of - NONE => [] - |SOME cls => cls ; - - -fun get_simp_metas [] = [[]] -| get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x - in - metas::(get_simp_metas xs) - end - handle THM _ => get_simp_metas xs +(* changed, now it also finds out the name of the theorem. *) +(* convert a theorem into CNF and then into Clause.clause format. *) +fun clausify_axiom_pairs thm = + let val isa_clauses = ResAxioms.cnf_axiom thm (*"isa_clauses" are already "standard"ed. *) + val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses + val thm_name = Thm.name_of_thm thm + val clauses_n = length isa_clauses + fun make_axiom_clauses _ [] []= [] + | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss' + in + make_axiom_clauses 0 isa_clauses' isa_clauses + end; -(* re-jig all these later as smaller functions for each bit *) - val num_of_clauses = ref 0; -val clause_arr = Array.array(3500, ("empty", 0)); - - -fun write_out_clasimp filename (clause_arr:(string * int) Array.array) = let - val _= warning "in writeoutclasimp" - (****************************************) - (* add claset rules to array and write out as strings *) - (****************************************) - val clausifiable_rules = ResAxioms.claset_rules_of_thy (the_context()) - val name_fol_cs = List.filter has_name clausifiable_rules; - (* length name_fol_cs is 93 *) - val good_names = map Thm.name_of_thm name_fol_cs; - - (*******************************************) - (* get (name, thm) pairs for claset rules *) - (*******************************************) +fun clausify_rules_pairs [] err_list = ([],err_list) + | clausify_rules_pairs (thm::thms) err_list = + let val (ts,es) = clausify_rules_pairs thms err_list + in + ((clausify_axiom_pairs thm)::ts,es) handle _ => (ts,(thm::es)) + end; - val names_rules = ListPair.zip (good_names,name_fol_cs); - - val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[]) - - val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls; +fun write_out_clasimp filename = let + val claset_rules = ResAxioms.claset_rules_of_thy (the_context()); + val named_claset = List.filter has_name claset_rules; + val claset_cls_thms = #1( clausify_rules_pairs named_claset []); - (* list of lists of tptp string clauses *) - val stick_clasrls = map stick claset_tptp_strs; - (* stick stick_clasrls length is 172*) - - val name_stick = ListPair.zip (good_names,stick_clasrls); + val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context()); + val named_simpset = map #2(List.filter has_name_pair simpset_rules); + val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []); - val cl_name_nums =map clause_numbering name_stick; - - val cl_long_name_nums = stick cl_name_nums; - (*******************************************) - (* create array and put clausename, number pairs into it *) - (*******************************************) + val cls_thms = (claset_cls_thms@simpset_cls_thms); + val cls_thms_list = stick cls_thms; - val _ = fill_cls_array clause_arr 1 cl_long_name_nums; - val _= num_of_clauses := (List.length cl_long_name_nums); - - (*************************************) - (* write claset out as tptp file *) - (*************************************) - - val claset_all_strs = stick stick_clasrls; - val out = TextIO.openOut filename; - val _= ResLib.writeln_strs out claset_all_strs; - val _= TextIO.flushOut out; - val _= TextIO.output (out,("\n \n")); - val _= TextIO.flushOut out; - (*val _= TextIO.closeOut out;*) - - (*********************) - (* Get simpset rules *) - (*********************) + (*********************************************************) + (* create array and put clausename, number pairs into it *) + (*********************************************************) + val num_of_clauses = 0; + val clause_arr = Array.fromList cls_thms_list; + + val num_of_clauses= (List.length cls_thms_list); - 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; - val simp_rules = map #2 named_simps; - - (* 1137 clausif simps *) - - (* need to get names of claset_cluases so we can make sure we've*) - (* got the same ones (ie. the named ones ) as the claset rules *) - (* length 1374*) - val new_simps = #1(ResAxioms.clausify_rules simp_rules []); - val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps; - - val stick_strs = map stick simpset_tptp_strs; - val name_stick = ListPair.zip (simp_names,stick_strs); - - val name_nums =map clause_numbering name_stick; - (* length 2409*) - val long_name_nums = stick name_nums; + (*************************************************) + (* Write out clauses as tptp strings to filename *) + (*************************************************) + val clauses = map #1(cls_thms_list); + val cls_tptp_strs = map ResClause.tptp_clause clauses; + (* list of lists of tptp string clauses *) + val stick_clasrls = stick cls_tptp_strs; + val out = TextIO.openOut filename; + val _= ResLib.writeln_strs out stick_clasrls; + val _= TextIO.flushOut out; + val _= TextIO.closeOut out + in + (clause_arr, num_of_clauses) + end; - val _ =fill_cls_array clause_arr (!num_of_clauses + 1) long_name_nums; - val _ =num_of_clauses := (!num_of_clauses) + (List.length long_name_nums); - - - - val tptplist = (stick stick_strs) - - in - ResLib.writeln_strs out tptplist; - TextIO.flushOut out; - TextIO.closeOut out; - clause_arr - end; - -(* - - Array.sub(clause_arr, 2310); -*) +end; diff -r 6d6d3fabef02 -r b30a35432f5a src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Tue May 03 10:33:31 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Tue May 03 14:27:21 2005 +0200 @@ -92,7 +92,7 @@ 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 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"));()) @@ -112,7 +112,8 @@ (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")); + sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n")); +(*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*) TextIO.flushOut toWatcherStr; Unix.reap exec_tptp2x; @@ -244,7 +245,7 @@ -fun setupWatcher (thm) = let +fun setupWatcher (thm,clause_arr, num_of_clauses) = let (** pipes for communication between parent and watcher **) val p1 = Posix.IO.pipe () val p2 = Posix.IO.pipe () @@ -275,6 +276,14 @@ 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.sysify_path(File.tmp_path (Path.basic "goal_in_watcher"))); val _ = TextIO.output (outfile,goalstr ) @@ -374,7 +383,7 @@ 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, thm, sg_num) ) ) + (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (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 *) @@ -475,7 +484,7 @@ ) else ( - if ((length procList)<2) (********************) + if ((length procList)<10) (********************) then (* Execute locally *) ( (********************) let @@ -587,7 +596,7 @@ (**********************************************************) fun killWatcher pid= killChild pid; -fun createWatcher (thm) = let val mychild = childInfo (setupWatcher(thm)) +fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses)) val streams =snd mychild val childin = fst streams val childout = snd streams diff -r 6d6d3fabef02 -r b30a35432f5a src/HOL/Tools/ATP/watcher.sig --- a/src/HOL/Tools/ATP/watcher.sig Tue May 03 10:33:31 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.sig Tue May 03 14:27:21 2005 +0200 @@ -36,7 +36,7 @@ (* Start a watcher and set up signal handlers *) (**********************************************************) -val createWatcher : Thm.thm -> TextIO.instream * TextIO.outstream * Posix.Process.pid +val createWatcher : Thm.thm*(ResClause.clause * Thm.thm) Array.array * int -> TextIO.instream * TextIO.outstream * Posix.Process.pid diff -r 6d6d3fabef02 -r b30a35432f5a src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue May 03 10:33:31 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Tue May 03 14:27:21 2005 +0200 @@ -180,22 +180,28 @@ val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring); val _ = TextIO.flushOut outfile; val _ = TextIO.closeOut outfile + val spass_home = getenv "SPASS_HOME" in (* without paramodulation *) (warning ("goalstring in call_res_tac is: "^goalstring)); (warning ("prob file in cal_res_tac is: "^probfile)); + Watcher.callResProvers(childout, + [("spass",thmstr,goalstring,spass_home, + "-DocProof", + clasimpfile, axfile, hypsfile, probfile)]); + Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", + [("spass",thmstr,goalstring,spass_home, "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", clasimpfile, axfile, hypsfile, probfile)]); (* with paramodulation *) (*Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", + [("spass",thmstr,goalstring,spass_home, "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", prob_path)]); *) (* Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", + [("spass",thmstr,goalstring,spass_home, "-DocProof", prob_path)]);*) dummy_tac end @@ -282,24 +288,32 @@ (******************************************************************) (*FIX changed to clasimp_file *) fun isar_atp' (thms, thm) = - let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) + let + val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) val _= (warning ("in isar_atp'")) val prems = prems_of thm val sign = sign_of_thm thm val thms_string = Meson.concat_with_and (map string_of_thm thms) val thmstring = string_of_thm thm 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 *) + + (* set up variables for writing out the clasimps to a tptp file *) + val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) + 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)) - val _ = (warning ("tenth axiom in array is: "^tenth_ax)) - val _ = (warning ("num_of_clauses is: "^(string_of_int (!num_of_clauses))) ) *) - - val (childin,childout,pid) = Watcher.createWatcher(thm) + (* cq:create watcher and pass to isar_atp_aux *) + (* tracing *) + (*val tenth_ax = fst( Array.sub(clause_arr, 1)) + val tenth_ax_thms = Recon_Transfer.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 is: "^tenth_ax)) + val _ = (warning ("tenth axiom in table is: "^clause_str)) + + val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) ) + *) + + val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses) val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid ))) in case prems of [] => ()