# HG changeset patch # User quigley # Date 1117536156 -7200 # Node ID 2f6fc19aba1ec3b25f53e450f895c748c287e1f6 # Parent a6403c6c533952814c9494f4ba97eab21faa5b0e Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass ruleset. diff -r a6403c6c5339 -r 2f6fc19aba1e src/HOL/Tools/ATP/SpassCommunication.ML --- a/src/HOL/Tools/ATP/SpassCommunication.ML Tue May 31 12:36:01 2005 +0200 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML Tue May 31 12:42:36 2005 +0200 @@ -7,6 +7,20 @@ (***************************************************************************) (* Code to deal with the transfer of proofs from a Spass process *) (***************************************************************************) +signature SPASS_COMM = + 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 + + 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 *) @@ -42,7 +56,13 @@ in SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, - METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs clause_arr num_of_clauses ))]) sg_num + 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 ; @@ -111,7 +131,7 @@ 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)) + val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm)) val _ = TextIO.closeOut outfile in @@ -140,8 +160,8 @@ val _ = TextIO.closeOut outfile in - (*TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent;*) + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; TextIO.output (spass_proof_file, (thisLine)); TextIO.flushOut spass_proof_file; TextIO.closeOut spass_proof_file; @@ -224,6 +244,18 @@ (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 ( @@ -245,3 +277,4 @@ ("No output from reconstruction process.\n","","") +end; diff -r a6403c6c5339 -r 2f6fc19aba1e src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 31 12:36:01 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 31 12:42:36 2005 +0200 @@ -1,6 +1,7 @@ + (* ID: $Id$ - Author: Claire Quigley - Copyright 2004 University of Cambridge + Author: Claire Quigley + Copyright 2004 University of Cambridge *) (******************) @@ -195,19 +196,66 @@ | retrieve_axioms clause_arr (x::xs) = [Array.sub(clause_arr, x)]@ (retrieve_axioms clause_arr xs) +fun subone x = x - 1 + +fun numstr [] = "" +| numstr (x::xs) = (string_of_int x)^"%"^(numstr 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 + let + val realnums = map subone step_nums + + + val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums + val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums"))) + val _ = TextIO.output(axnums,(numstr clasimp_nums)) + val _ = TextIO.closeOut(axnums) in retrieve_axioms clause_arr clasimp_nums end +fun get_cls [] = [] +| get_cls (x::xs) = ((#1 x)::(get_cls xs)) + +(* add array and table here, so can retrieve clasimp axioms *) + + fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * Thm.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*) + (***********************************************) + + val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums + val clauses=(get_cls clasimp_names_cls) + val (names_clsnums) = map ResClause.clause_info clauses + val clasimp_names = map fst names_clsnums + + val outfile = TextIO.openOut(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 _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode)) + + in + (clasimp_names) + end + +fun numclstr (vars, []) str = str +| numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" " +in +numclstr (vars,rest) newstr +end +fun addvars c (a,b) = (a,b,c) -(* add array and table here, so can retrieve clasimp axioms *) fun get_axioms_used proof_steps thms clause_arr num_of_clauses = let @@ -293,32 +341,8 @@ (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas))) end -fun numclstr (vars, []) str = str -| numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" " -in -numclstr (vars,rest) newstr -end -(* - -val proofstr = "Did parsing on Here is a proof with depth 4, length 9 :\ -\1[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\ -\3[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\ -\5[0:Inp] || -> v_P(tconst_fun(typ__da_a,tconst_bool),U)* v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\ -\7[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\ -\9[0:Fac:5.0,5.1] || -> v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\ -\10[0:Res:9.0,3.0] || -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\ -\11[0:Res:10.0,1.0] || -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\ -\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\ -\14[0:Res:11.0,12.0] || -> .\ -\Formulae used in the proof :" - -*) - - -fun addvars c (a,b) = (a,b,c) - - + (*********************************************************************) (* Pass in spass string of proof and string version of isabelle goal *) @@ -326,52 +350,74 @@ (*********************************************************************) -(* - +fun rules_to_string [] str = str +| rules_to_string [x] str = str^x +| rules_to_string (x::xs) str = rules_to_string xs (str^x^" ") + -val proofstr = "Here is a proof with depth 2, length 5 :\ -\1[0:Inp] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\ -\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\ -\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa).\ -\7[0:Res:1.0,5.0] || -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\ -\9[0:Res:7.0,3.0] || -> .\ -\Formulae used in the proof :" +val dummy_tac = PRIMITIVE(fn thm => thm ); -val proofstr = "Here is a proof with depth 4, length 9 :\ -\1[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\ -\3[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\ -\5[0:Inp] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)* v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\ -\7[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\ -\9[0:Fac:5.0,5.1] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\ -\10[0:Res:9.0,3.0] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\ -\11[0:Res:10.0,1.0] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\ -\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\ -\14[0:Res:11.0,12.0] || -> .\ -\Formulae used in the proof :"; +fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = + let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "thmstringfile"))); val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses))) + val _ = TextIO.closeOut outfile + + (***********************************) + (* parse spass proof into datatype *) + (***********************************) + + val tokens = #1(lex proofstr) + val proof_steps1 = parse tokens + val proof_steps = just_change_space proof_steps1 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr)) + val _ = TextIO.closeOut outfile + + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring)) + val _ = TextIO.closeOut outfile + (************************************) + (* recreate original subgoal as thm *) + (************************************) + + (* 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 *) + (* 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 ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "") + val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile"))); val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^" "^goalstring)) + val _ = TextIO.closeOut outfile + + 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 + 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 + TextIO.output (toParent,"Proof found but translation failed!" ^"\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) ;dummy_tac + end) -val thmstring = " (~ (P::'a::type => bool) (x::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | P (x::'a::type)) & ((P::'a::type => bool) (xa::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | ~ P (xb::'a::type))"; - -val thmstring = "(ALL xb::'a::type. (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) | (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) & P xb & ~ Q xb)" - - -val thmstring ="(ALL xb::'a::type. (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) | (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) & P xb & ~ Q xb)" - -val proofstr = "Did parsing on Here is a proof with depth 2, length 5 :\ -\1[0:Inp] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\ -\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\ -\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x(tconst_fun(typ__asc39_a,typ__asc39_a),U))* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U)).\ -\7[0:Res:1.0,5.0] || -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U))*.\ -\9[0:Res:7.0,3.0] || -> .\ -\Formulae used in the proof :"; - -*) - - - - -val dummy_tac = PRIMITIVE(fn thm => thm ); 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"))); @@ -474,10 +520,6 @@ - - - - (**********************************************************************************) (* At other end, want to turn back into datatype so can apply reconstruct_proof. *) (* This will be done by the signal handler *) @@ -808,4 +850,6 @@ end + + end; diff -r a6403c6c5339 -r 2f6fc19aba1e src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 31 12:36:01 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 31 12:42:36 2005 +0200 @@ -5,7 +5,7 @@ Copyright 2004 University of Cambridge *) -signature RES_CLASIMP = +signature RES_CLASIMP = sig val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int end; @@ -50,6 +50,30 @@ (*Insert th into the result provided the name is not "".*) fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths; +fun posinlist x [] n = "not in list" +| posinlist x (y::ys) n = if (x=y) + then + string_of_int n + else posinlist x (ys) (n+1) + + +fun pairup [] [] = [] +| pairup (x::xs) (y::ys) = (x,y)::(pairup xs ys) + +fun multi x 0 xlist = xlist + |multi x n xlist = multi x (n -1 ) (x::xlist); + + +fun clause_numbering ((clause, theorem), cls) = let val num_of_cls = length cls + val numbers = 0 upto (num_of_cls -1) + val multi_name = multi (clause, theorem) num_of_cls [] + in + (multi_name) + end; + + + + fun write_out_clasimp filename = let val claset_rules = ResAxioms.claset_rules_of_thy (the_context()); @@ -64,22 +88,25 @@ val cls_thms = (claset_cls_thms@simpset_cls_thms); val cls_thms_list = List.concat cls_thms; - - (*********************************************************) - (* 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; - + (* length 1429 *) (*************************************************) (* Write out clauses as tptp strings to filename *) (*************************************************) val clauses = map #1(cls_thms_list); val cls_tptp_strs = map ResClause.tptp_clause clauses; + val alllist = pairup cls_thms_list cls_tptp_strs + val whole_list = List.concat (map clause_numbering alllist); + + (*********************************************************) + (* create array and put clausename, number pairs into it *) + (*********************************************************) + val num_of_clauses = 0; + val clause_arr = Array.fromList whole_list; + val num_of_clauses = List.length whole_list; + (* list of lists of tptp string clauses *) val stick_clasrls = List.concat cls_tptp_strs; + (* length 1581*) val out = TextIO.openOut filename; val _= ResLib.writeln_strs out stick_clasrls; val _= TextIO.flushOut out; @@ -88,6 +115,7 @@ (clause_arr, num_of_clauses) end; - end; + + diff -r a6403c6c5339 -r 2f6fc19aba1e src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Tue May 31 12:36:01 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Tue May 31 12:42:36 2005 +0200 @@ -1,4 +1,5 @@ (* Title: Watcher.ML + ID: $Id$ Author: Claire Quigley Copyright 2004 University of Cambridge @@ -162,27 +163,28 @@ val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher")) (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n") (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) - val probID = ReconOrderClauses.last(explode probfile) + val probID = ReconOrderClauses.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 ***) - (*FIXME: find a way that works for SML/NJ too: it regards > as a filename!*) - val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)]) + + (*** hyps/local axioms just now (*,axfile, hypsfile,*) ***) + val whole_prob_file = system ("/bin/cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ (File.sysify_path wholefile)) + val dfg_create = if File.exists dfg_dir then warning("dfg dir exists") else File.mkdir dfg_dir; val dfg_path = File.sysify_path dfg_dir; - val tptp2x_args = ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile] val exec_tptp2x = - Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", tptp2x_args) + Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", + ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]) (*val _ = Posix.Process.wait ()*) (*val _ =Unix.reap exec_tptp2x*) val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg" in goals_being_watched := (!goals_being_watched) + 1; - Posix.Process.sleep(Time.fromSeconds 4); + Posix.Process.sleep(Time.fromSeconds 1); (warning ("probfile is: "^probfile)); (warning("dfg file is: "^newfile)); (warning ("wholefile is: "^(File.sysify_path wholefile))); @@ -195,8 +197,8 @@ if File.exists (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg"))) then callResProvers (toWatcherStr, args) - else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X " ^ - space_implode " " tptp2x_args) + else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^ + " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path) end (* fun callResProversStr (toWatcherStr, []) = "End of calls\n" @@ -381,7 +383,7 @@ in if (isSome pd ) then let val pd' = OS.IO.pollIn (valOf pd) - val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) + val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) in if null pdl then @@ -407,7 +409,7 @@ in if (isSome pd ) then let val pd' = OS.IO.pollIn (valOf pd) - val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) + val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) in if null pdl then @@ -456,7 +458,7 @@ (* 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" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) + (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"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 *) @@ -700,81 +702,123 @@ status end -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 - 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"));() ) - + +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 + 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"));() ) + + +fun spass_proofHandler (n) = ( + 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) = SpassComm.getSpassInput childin + val outfile = TextIO.openAppend(File.sysify_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 + in (* if a proof has been found and sent back as a reconstruction proof *) + if ( (substring (reconstr, 0,1))= "[") + then - fun spass_proofHandler (n) = ( - let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n" - val (reconstr, thmstring, goalstring) = getSpassInput childin - val _ = File.append (File.tmp_path (Path.basic "foo_signal")) - ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(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); - - 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") - in - reapWatcher (childpid,childin, childout); () - end) - else () - ) - (* if there's no proof, but a message from Spass *) - else if ((substring (reconstr, 0,5))= "SPASS") - then - (goals_being_watched := (!goals_being_watched) -1; - Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^reconstr)); - Pretty.writeln(Pretty.str (oct_char "361")); - if (!goals_being_watched = 0) - then - (File.write (File.tmp_path (Path.basic "foo_reap_comp")) - ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"); - reapWatcher (childpid,childin, childout); ()) - else - () - ) - (* if proof translation failed *) - else if ((substring (reconstr, 0,5)) = "Proof") - then - (goals_being_watched := (!goals_being_watched) -1; - Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^reconstr)); - Pretty.writeln(Pretty.str (oct_char "361")); - if (!goals_being_watched = 0) - then - (File.write(File.tmp_path (Path.basic "foo_reap_comp")) - ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"); - reapWatcher (childpid,childin, childout); ()) - else ()) - else () (* add something here ?*) - end) + ( + 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); + + if ((!goals_being_watched) = 0) + then + (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found"))); + val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) + val _ = TextIO.closeOut outfile + in + killWatcher (childpid); reapWatcher (childpid,childin, childout); () + end) + else + () + ) + (* if there's no proof, but a message from Spass *) + else if ((substring (reconstr, 0,5))= "SPASS") + then + ( + goals_being_watched := (!goals_being_watched) -1; + Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); + Pretty.writeln(Pretty.str (goalstring^reconstr)); + Pretty.writeln(Pretty.str (oct_char "361")); + if (!goals_being_watched = 0) + then + (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp"))); + val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) + val _ = TextIO.closeOut outfile + in + killWatcher (childpid); reapWatcher (childpid,childin, childout); () + end ) + else + () + ) + (* print out a list of rules used from clasimpset*) + else if ((substring (reconstr, 0,5))= "Rules") + then + ( + goals_being_watched := (!goals_being_watched) -1; + Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); + Pretty.writeln(Pretty.str (goalstring^reconstr)); + Pretty.writeln(Pretty.str (oct_char "361")); + if (!goals_being_watched = 0) + then + (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp"))); + val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) + val _ = TextIO.closeOut outfile + in + killWatcher (childpid); reapWatcher (childpid,childin, childout);() + end ) + else + () + ) + + (* if proof translation failed *) + else if ((substring (reconstr, 0,5)) = "Proof") + then + ( + goals_being_watched := (!goals_being_watched) -1; + Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); + Pretty.writeln(Pretty.str (goalstring^reconstr)); + Pretty.writeln(Pretty.str (oct_char "361")); + if (!goals_being_watched = 0) + then + (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp"))); + val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) + val _ = TextIO.closeOut outfile + in + killWatcher (childpid); reapWatcher (childpid,childin, childout); () + end ) + else + () + ) - - in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler); - IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler); - (childin, childout, childpid) + else (* add something here ?*) + () + + end) + + + + in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler); + IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler); + (childin, childout, childpid) + end diff -r a6403c6c5339 -r 2f6fc19aba1e src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue May 31 12:36:01 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Tue May 31 12:42:36 2005 +0200 @@ -21,7 +21,7 @@ (*val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic*) (*val atp_tac : int -> Tactical.tactic*) val debug: bool ref - +val full_spass: bool ref end; structure ResAtp : RES_ATP = @@ -38,6 +38,7 @@ (* default value is false *) val trace_res = ref false; +val full_spass = ref false; val skolem_tac = skolemize_tac; @@ -188,11 +189,19 @@ [("spass",thmstr,goalstring,*spass_home*, "-DocProof", clasimpfile, axfile, hypsfile, probfile)]);*) - Watcher.callResProvers(childout, + if !full_spass + then + (Watcher.callResProvers(childout, + [("spass", thmstr, goalstring (*,spass_home*), + getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", + "-DocProof", + clasimpfile, axfile, hypsfile, probfile)])) + else + (Watcher.callResProvers(childout, [("spass", thmstr, goalstring (*,spass_home*), getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", - clasimpfile, axfile, hypsfile, probfile)]); + clasimpfile, axfile, hypsfile, probfile)])); (* with paramodulation *) (*Watcher.callResProvers(childout, diff -r a6403c6c5339 -r 2f6fc19aba1e src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Tue May 31 12:36:01 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Tue May 31 12:42:36 2005 +0200 @@ -396,7 +396,19 @@ (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****) -(* outputs a list of (thm,clause) pairs *) +(* outputs a list of (clause,thm) pairs *) +(*fun clausify_axiom_pairs (thm_name,thm) = + let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *) + val isa_clauses' = rm_Eps [] isa_clauses + 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', thm_name, i) :: make_axiom_clauses (i+1) clss clss' + in + make_axiom_clauses 0 isa_clauses' isa_clauses + end; +*) + + fun clausify_axiom_pairs (thm_name,thm) = let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *) val isa_clauses' = rm_Eps [] isa_clauses @@ -407,7 +419,6 @@ make_axiom_clauses 0 isa_clauses' isa_clauses end; - fun clausify_rules_pairs [] err_list = ([],err_list) | clausify_rules_pairs ((name,thm)::thms) err_list = let val (ts,es) = clausify_rules_pairs thms err_list