# HG changeset patch # User mengj # Date 1141700485 -3600 # Node ID b338c218cc6e125a1c0f762df2e52a6fc422f23f # Parent e6f1ff40ba99298cef25aded2b9ad88adeed2f14 Proof reconstruction now only takes names of theorems as input. diff -r e6f1ff40ba99 -r b338c218cc6e src/HOL/Tools/ATP/AtpCommunication.ML --- a/src/HOL/Tools/ATP/AtpCommunication.ML Tue Mar 07 03:59:48 2006 +0100 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML Tue Mar 07 04:01:25 2006 +0100 @@ -12,13 +12,13 @@ val reconstruct : bool ref val checkEProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * (ResClause.clause * thm) Array.array -> bool + string * string Array.array -> bool val checkVampProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * (ResClause.clause * thm) Array.array -> bool + string * string Array.array -> bool val checkSpassProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * thm * int * (ResClause.clause * thm) Array.array -> bool + string * thm * int * string Array.array -> bool val signal_parent: TextIO.outstream * Posix.Process.pid * string * string -> unit end; @@ -64,7 +64,7 @@ (* and if so, transfer output to the input pipe of the main Isabelle process *) (*********************************************************************************) -fun startTransfer (endS, fromChild, toParent, ppid, probfile, clause_arr) = +fun startTransfer (endS, fromChild, toParent, ppid, probfile, names_arr) = let fun transferInput currentString = let val thisLine = TextIO.inputLine fromChild in @@ -79,7 +79,7 @@ else Recon_Transfer.e_lemma_list in trace ("\nExtracted proof:\n" ^ proofextract); - lemma_list proofextract probfile toParent ppid clause_arr + lemma_list proofextract probfile toParent ppid names_arr end else transferInput (currentString^thisLine) end @@ -99,25 +99,25 @@ OS.Process.sleep (Time.fromMilliseconds 600)); (*Called from watcher. Returns true if the Vampire process has returned a verdict.*) -fun checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr) = +fun checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr) = let val thisLine = TextIO.inputLine fromChild in trace thisLine; if thisLine = "" then (trace "\nNo proof output seen"; false) else if String.isPrefix start_V8 thisLine - then startTransfer (end_V8, fromChild, toParent, ppid, probfile, clause_arr) + then startTransfer (end_V8, fromChild, toParent, ppid, probfile, names_arr) else if (String.isPrefix "Satisfiability detected" thisLine) orelse (String.isPrefix "Refutation not found" thisLine) then (signal_parent (toParent, ppid, "Failure\n", probfile); true) else - checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr) + checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr) end (*Called from watcher. Returns true if the E process has returned a verdict.*) -fun checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr) = +fun checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) = let val thisLine = TextIO.inputLine fromChild in trace thisLine; @@ -125,7 +125,7 @@ then (trace "\nNo proof output seen"; false) else if String.isPrefix start_E thisLine then - startTransfer (end_E, fromChild, toParent, ppid, probfile, clause_arr) + startTransfer (end_E, fromChild, toParent, ppid, probfile, names_arr) else if String.isPrefix "# Problem is satisfiable" thisLine then (signal_parent (toParent, ppid, "Invalid\n", probfile); true) @@ -133,7 +133,7 @@ then (signal_parent (toParent, ppid, "Failure\n", probfile); true) else - checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr) + checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) end @@ -143,16 +143,16 @@ (* steps as a string to the input pipe of the main Isabelle process *) (**********************************************************************) -fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num clause_arr = +fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num names_arr = SELECT_GOAL (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, METAHYPS(fn negs => Recon_Transfer.spass_reconstruct proofextract probfile - toParent ppid negs clause_arr)]) sg_num; + toParent ppid negs names_arr)]) sg_num; fun transferSpassInput (fromChild, toParent, ppid, probfile, - currentString, thm, sg_num, clause_arr) = + currentString, thm, sg_num, names_arr) = let val thisLine = TextIO.inputLine fromChild in trace thisLine; @@ -166,12 +166,12 @@ trace ("\nextracted spass proof: " ^ proofextract); if !reconstruct then (spass_reconstruct_tac proofextract toParent ppid probfile sg_num - clause_arr thm; ()) + names_arr thm; ()) else Recon_Transfer.spass_lemma_list proofextract probfile toParent - ppid clause_arr + ppid names_arr end else transferSpassInput (fromChild, toParent, ppid, probfile, - (currentString^thisLine), thm, sg_num, clause_arr) + (currentString^thisLine), thm, sg_num, names_arr) end; @@ -182,29 +182,29 @@ fun startSpassTransfer (fromChild, toParent, ppid, probfile, - thm, sg_num,clause_arr) = + thm, sg_num,names_arr) = let val thisLine = TextIO.inputLine fromChild in if thisLine = "" then false else if String.isPrefix "Here is a proof" thisLine then (trace ("\nabout to transfer SPASS proof:\n"); transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, - thm, sg_num,clause_arr); + thm, sg_num,names_arr); true) handle EOF => false - else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,clause_arr) + else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,names_arr) end (*Called from watcher. Returns true if the SPASS process has returned a verdict.*) fun checkSpassProofFound (fromChild, toParent, ppid, probfile, - thm, sg_num, clause_arr) = + thm, sg_num, names_arr) = let val thisLine = TextIO.inputLine fromChild in trace thisLine; if thisLine = "" then (trace "\nNo proof output seen"; false) else if thisLine = "SPASS beiseite: Proof found.\n" then - startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr) + startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr) else if thisLine = "SPASS beiseite: Completion found.\n" then (signal_parent (toParent, ppid, "Invalid\n", probfile); true) @@ -212,7 +212,7 @@ thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" then (signal_parent (toParent, ppid, "Failure\n", probfile); true) - else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr) + else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr) end end; diff -r e6f1ff40ba99 -r b338c218cc6e src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Mar 07 03:59:48 2006 +0100 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Mar 07 04:01:25 2006 +0100 @@ -149,17 +149,17 @@ (* retrieve the axioms that were obtained from the clasimpset *) -fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) step_nums = - let val clasimp_nums = List.filter (is_clasimp_ax (Array.length clause_arr - 1)) +fun get_clasimp_cls (names_arr: string array) step_nums = + let val clasimp_nums = List.filter (is_clasimp_ax (Array.length names_arr - 1)) (map subone step_nums) in - map (fn x => Array.sub(clause_arr, x)) clasimp_nums + map (fn x => Array.sub(names_arr, x)) clasimp_nums end (* get names of clasimp axioms used*) -fun get_axiom_names step_nums clause_arr = +fun get_axiom_names step_nums names_arr = sort_distinct string_ord - (map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums)); + (get_clasimp_cls names_arr step_nums); (*String contains multiple lines. We want those of the form "253[0:Inp] et cetera..." @@ -171,8 +171,8 @@ val lines = String.tokens (fn c => c = #"\n") proofstr in List.mapPartial (inputno o toks) lines end -fun get_axiom_names_spass proofstr clause_arr = - get_axiom_names (get_spass_linenums proofstr) clause_arr; +fun get_axiom_names_spass proofstr names_arr = + get_axiom_names (get_spass_linenums proofstr) names_arr; (*String contains multiple lines. A list consisting of the first number in each line is returned. *) @@ -183,8 +183,8 @@ val lines = String.tokens (fn c => c = #"\n") proofstr in List.mapPartial (firstno o numerics) lines end -fun get_axiom_names_e proofstr clause_arr = - get_axiom_names (get_linenums proofstr) clause_arr; +fun get_axiom_names_e proofstr names_arr = + get_axiom_names (get_linenums proofstr) names_arr; (*String contains multiple lines. We want those of the form "*********** [448, input] ***********". @@ -196,8 +196,8 @@ val lines = String.tokens (fn c => c = #"\n") proofstr in List.mapPartial (inputno o toks) lines end -fun get_axiom_names_vamp proofstr clause_arr = - get_axiom_names (get_vamp_linenums proofstr) clause_arr; +fun get_axiom_names_vamp proofstr names_arr = + get_axiom_names (get_vamp_linenums proofstr) names_arr; (***********************************************) @@ -212,7 +212,7 @@ fun addvars c (a,b) = (a,b,c) -fun get_axioms_used proof_steps thms clause_arr = +fun get_axioms_used proof_steps thms names_arr = let val axioms = (List.filter is_axiom) proof_steps val step_nums = get_step_nums axioms [] @@ -265,12 +265,12 @@ (*The signal handler in watcher.ML must be able to read the output of this.*) -fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr = +fun prover_lemma_list_aux getax proofstr probfile toParent ppid names_arr = let val _ = trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^ "\nprobfile is " ^ probfile ^ - " num of clauses is " ^ string_of_int (Array.length clause_arr)) - val axiom_names = getax proofstr clause_arr + " num of clauses is " ^ string_of_int (Array.length names_arr)) + val axiom_names = getax proofstr names_arr val ax_str = rules_to_string axiom_names in trace ("\nDone. Lemma list is " ^ ax_str); @@ -298,7 +298,7 @@ (**** Full proof reconstruction for SPASS (not really working) ****) -fun spass_reconstruct proofstr probfile toParent ppid thms clause_arr = +fun spass_reconstruct proofstr probfile toParent ppid thms names_arr = let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr) val tokens = #1(lex proofstr) @@ -315,7 +315,7 @@ (* 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 (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr + val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms names_arr (*val numcls_string = numclstr ( vars, numcls) ""*) val _ = trace "\ngot axioms" diff -r e6f1ff40ba99 -r b338c218cc6e src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Tue Mar 07 03:59:48 2006 +0100 +++ b/src/HOL/Tools/ATP/watcher.ML Tue Mar 07 04:01:25 2006 +0100 @@ -23,7 +23,7 @@ (* Start a watcher and set up signal handlers *) val createWatcher : - thm * (ResClause.clause * thm) Array.array -> + thm * string Array.array -> TextIO.instream * TextIO.outstream * Posix.Process.pid val killWatcher : Posix.Process.pid -> unit val setting_sep : char @@ -206,7 +206,7 @@ Date.toString(Date.fromTimeLocal(Time.now()))) in execCmds cmds newProcList end -fun checkChildren (th, clause_arr, toParentStr, children) = +fun checkChildren (th, names_arr, toParentStr, children) = let fun check [] = [] (* no children to check *) | check (child::children) = let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = @@ -220,11 +220,11 @@ let val _ = trace ("\nInput available from child: " ^ file) val childDone = (case prover of "vampire" => AtpCommunication.checkVampProofFound - (childIn, toParentStr, ppid, file, clause_arr) + (childIn, toParentStr, ppid, file, names_arr) | "E" => AtpCommunication.checkEProofFound - (childIn, toParentStr, ppid, file, clause_arr) + (childIn, toParentStr, ppid, file, names_arr) | "spass" => AtpCommunication.checkSpassProofFound - (childIn, toParentStr, ppid, file, th, sgno,clause_arr) + (childIn, toParentStr, ppid, file, th, sgno,names_arr) | _ => (trace ("\nBad prover! " ^ prover); true) ) in if childDone (*child has found a proof and transferred it*) @@ -240,7 +240,7 @@ end; -fun setupWatcher (th,clause_arr) = +fun setupWatcher (th,names_arr) = let val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*) val p2 = Posix.IO.pipe() @@ -277,16 +277,16 @@ if length procList < 40 then (* Execute locally *) let val _ = trace("\nCommands from parent: " ^ Int.toString(length cmds)) - val newProcList' = checkChildren(th, clause_arr, toParentStr, + val newProcList' = checkChildren(th, names_arr, toParentStr, execCmds cmds procList) in trace "\nCommands executed"; keepWatching newProcList' end else (* Execute remotely [FIXME: NOT REALLY] *) - let val newProcList' = checkChildren (th, clause_arr, toParentStr, + let val newProcList' = checkChildren (th, names_arr, toParentStr, execCmds cmds procList) in keepWatching newProcList' end | NONE => (* No new input from Isabelle *) (trace "\nNothing from parent..."; - keepWatching(checkChildren(th, clause_arr, toParentStr, procList)))) + keepWatching(checkChildren(th, names_arr, toParentStr, procList)))) handle exn => (*FIXME: exn handler is too general!*) (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn); keepWatching procList); @@ -344,8 +344,8 @@ fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th)) -fun createWatcher (th, clause_arr) = - let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,clause_arr) +fun createWatcher (th, names_arr) = + let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,names_arr) fun decr_watched() = (goals_being_watched := !goals_being_watched - 1; if !goals_being_watched = 0