# HG changeset patch # User paulson # Date 1126079671 -7200 # Node ID 6cef3aedd6610d61ead8fe0b50ce58213e98d9fb # Parent c33c9e9df4f82b623196fc7e387561b7f9ec08e3 axioms now included in tptp files, no /bin/cat and various tidying diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/ATP/ECommunication.ML --- a/src/HOL/Tools/ATP/ECommunication.ML Wed Sep 07 09:53:50 2005 +0200 +++ b/src/HOL/Tools/ATP/ECommunication.ML Wed Sep 07 09:54:31 2005 +0200 @@ -9,19 +9,16 @@ (***************************************************************************) signature E_COMM = sig - val reconstruct : bool ref val E: bool ref val getEInput : TextIO.instream -> string * string * string - val checkEProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * string * - string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array * int -> bool - + val checkEProofFound: + TextIO.instream * TextIO.outstream * Posix.Process.pid * string * + string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool end; -structure EComm :E_COMM = +structure EComm : E_COMM = struct -(* switch for whether to reconstruct a proof found, or just list the lemmas used *) -val reconstruct = ref true; val E = ref false; (***********************************) @@ -41,27 +38,13 @@ (* steps as a string to the input pipe of the main Isabelle process *) (**********************************************************************) -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 reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num - clause_arr (num_of_clauses:int ) = - (*FIXME: foo is never used!*) - let val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3"))); - in + clause_arr num_of_clauses = SELECT_GOAL - (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, + (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, METAHYPS(fn negs => - ( Recon_Transfer.EString_to_lemmaString proofextract thmstring goalstring + (Recon_Transfer.EString_to_lemmaString proofextract thmstring goalstring toParent ppid negs clause_arr num_of_clauses ))]) sg_num - end ; fun transferEInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = @@ -71,7 +54,7 @@ then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) in - File.write (File.tmp_path (Path.basic"foobar2")) proofextract; + File.write (File.tmp_path (Path.basic"extracted-prf-E")) proofextract; reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr num_of_clauses thm end @@ -82,45 +65,40 @@ (*********************************************************************************) -(* Inspect the output of a E process to see if it has found a proof, *) +(* Inspect the output of an E process to see if it has found a proof, *) (* and if so, transfer output to the input pipe of the main Isabelle process *) (*********************************************************************************) -fun startETransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = -(*let val _ = Posix.Process.wait () -in*) - - if (isSome (TextIO.canInput(fromChild, 5))) - then - let val thisLine = TextIO.inputLine fromChild - in - if String.isPrefix "# Proof object starts" thisLine then - let val outfile = TextIO.openAppend(File.platform_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 - transferEInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, - thm, sg_num,clause_arr, num_of_clauses); - true - end - else startETransfer (fromChild, toParent, ppid, thmstring, goalstring, - childCmd, thm, sg_num,clause_arr, num_of_clauses) - end - else false - (* end*) +fun startETransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, + thm, sg_num,clause_arr, num_of_clauses) = + if isSome (TextIO.canInput(fromChild, 5)) + then + let val thisLine = TextIO.inputLine fromChild + in + if String.isPrefix "# Proof object starts" thisLine + then + (File.append (File.tmp_path (Path.basic "transfer-E")) + ("about to transfer proof, thm is: " ^ string_of_thm thm); + transferEInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, + thm, sg_num,clause_arr, num_of_clauses); + true) + else startETransfer (fromChild, toParent, ppid, thmstring, goalstring, + childCmd, thm, sg_num,clause_arr, num_of_clauses) + end + else false -fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) = +fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, num_of_clauses) = let val E_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "E_proof"))) - val _ = File.write(File.tmp_path (Path.basic "foo_checkE")) - ("checking if proof found, thm is: "^(string_of_thm thm)) + val _ = File.write (File.tmp_path (Path.basic "checking-prf-E")) + ("checking if proof found, thm is: " ^ string_of_thm thm) in if (isSome (TextIO.canInput(fromChild, 5))) then let val thisLine = TextIO.inputLine fromChild in if (*thisLine = "# Problem is unsatisfiable (or provable), constructing proof object\n"*) - thisLine = "# # TSTP exit status: Unsatisfiable\n" + thisLine = "# TSTP exit status: Unsatisfiable\n" then let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) val _ = TextIO.output (outfile, thisLine) @@ -131,9 +109,8 @@ end else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n" then - let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); val _ = TextIO.output (outfile, thisLine) - val _ = TextIO.closeOut outfile in TextIO.output (toParent,childCmd^"\n" ); diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/ATP/SpassCommunication.ML --- a/src/HOL/Tools/ATP/SpassCommunication.ML Wed Sep 07 09:53:50 2005 +0200 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML Wed Sep 07 09:54:31 2005 +0200 @@ -10,19 +10,17 @@ signature SPASS_COMM = sig val reconstruct : bool ref - val spass: 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 = +structure SpassComm : SPASS_COMM = struct (* switch for whether to reconstruct a proof found, or just list the lemmas used *) val reconstruct = ref true; -val spass = ref true; (***********************************) (* Write Spass output to a file *) @@ -41,23 +39,13 @@ (* steps as a string to the input pipe of the main Isabelle process *) (**********************************************************************) -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 reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr (num_of_clauses:int ) = (*FIXME: foo is never used!*) let val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3"))); in SELECT_GOAL - (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, + (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, METAHYPS(fn negs => (if !reconstruct then Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/ATP/VampCommunication.ML --- a/src/HOL/Tools/ATP/VampCommunication.ML Wed Sep 07 09:53:50 2005 +0200 +++ b/src/HOL/Tools/ATP/VampCommunication.ML Wed Sep 07 09:54:31 2005 +0200 @@ -5,138 +5,91 @@ *) (***************************************************************************) -(* Code to deal with the transfer of proofs from a Vamp process *) +(* Code to deal with the transfer of proofs from a Vampire process *) (***************************************************************************) signature VAMP_COMM = sig - val reconstruct : bool ref val getVampInput : TextIO.instream -> string * string * string - val checkVampProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * string * - string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array * int -> bool - + val checkVampProofFound: + TextIO.instream * TextIO.outstream * Posix.Process.pid * string * + string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool end; -structure VampComm :VAMP_COMM = +structure VampComm : VAMP_COMM = struct -(* switch for whether to reconstruct a proof found, or just list the lemmas used *) -val reconstruct = ref true; - (***********************************) -(* Write Vamp output to a file *) +(* Write Vampire output to a file *) (***********************************) fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr in if (thisLine = "%============== End of proof. ==================\n" ) then TextIO.output (fd, thisLine) - else ( - TextIO.output (fd, thisLine); logVampInput (instr,fd)) + else (TextIO.output (fd, thisLine); logVampInput (instr,fd)) end; (**********************************************************************) -(* Reconstruct the Vamp proof w.r.t. thmstring (string version of *) +(* Reconstruct the Vampire proof w.r.t. thmstring (string version of *) (* Isabelle goal to be proved), then transfer the reconstruction *) (* steps as a string to the input pipe of the main Isabelle process *) (**********************************************************************) - -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 reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr (num_of_clauses:int ) = - let val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3"))); - in +fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num + clause_arr num_of_clauses = SELECT_GOAL - (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, - METAHYPS(fn negs => - ((*if !reconstruct - then - Recon_Transfer.vampString_to_reconString proofextract thmstring goalstring - toParent ppid negs clause_arr num_of_clauses - else*) - Recon_Transfer.vampString_to_lemmaString proofextract thmstring goalstring - toParent ppid negs clause_arr num_of_clauses ))]) sg_num - end ; + (EVERY1 + [rtac ccontr, ResLib.atomize_tac, skolemize_tac, + METAHYPS(fn negs => + (Recon_Transfer.vampString_to_lemmaString proofextract thmstring + goalstring toParent ppid negs clause_arr num_of_clauses ))]) sg_num fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = - let - val thisLine = TextIO.inputLine fromChild + let val thisLine = TextIO.inputLine fromChild in if (thisLine = "%============== End of proof. ==================\n" ) - then ( - let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) - val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2"))); - - in - - TextIO.output(foo,(proofextract));TextIO.closeOut foo; - reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr num_of_clauses thm - - end - ) - else ( - - transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr, num_of_clauses) - ) + then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) + in + File.write (File.tmp_path (Path.basic"extracted-prf-vamp")) proofextract; + reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num + clause_arr num_of_clauses thm + end + else transferVampInput (fromChild, toParent, ppid,thmstring, goalstring, + currentString^thisLine, thm, sg_num, clause_arr, num_of_clauses) end; - - (*********************************************************************************) -(* Inspect the output of a Vamp process to see if it has found a proof, *) +(* Inspect the output of a Vampire process to see if it has found a proof, *) (* and if so, transfer output to the input pipe of the main Isabelle process *) (*********************************************************************************) -fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = - (*let val _ = Posix.Process.wait () - in*) - - if (isSome (TextIO.canInput(fromChild, 5))) +fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, + thm, sg_num,clause_arr, num_of_clauses) = + if isSome (TextIO.canInput(fromChild, 5)) then - ( let val thisLine = TextIO.inputLine fromChild in if (thisLine = "%================== Proof: ======================\n") then - ( - let - val outfile = TextIO.openAppend(File.platform_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 - transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr, num_of_clauses); - true - end) - + (File.append (File.tmp_path (Path.basic "transfer-vamp")) + ("about to transfer proof, thm is: " ^ string_of_thm thm); + transferVampInput (fromChild, toParent, ppid,thmstring, goalstring, + thisLine, thm, sg_num,clause_arr, num_of_clauses); + true) else - ( - startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses) - ) + startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring, + childCmd, thm, sg_num,clause_arr, num_of_clauses) end - ) - else (false) -(* end*) + else false - -fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) = - let val vamp_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof"))) - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkvamp"))); - val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm)) - - val _ = TextIO.closeOut outfile +fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, num_of_clauses) = + let val vamp_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof"))) + val _ = File.write (File.tmp_path (Path.basic "checking-prf-vamp")) + ("checking if proof found, thm is: " ^ string_of_thm thm) in if (isSome (TextIO.canInput(fromChild, 5))) then @@ -144,19 +97,15 @@ let val thisLine = TextIO.inputLine fromChild in if (thisLine = "% Proof found. Thanks to Tanya!\n" ) then - ( - let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); val _ = TextIO.output (outfile, (thisLine)) val _ = TextIO.closeOut outfile in startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) end - ) else if (thisLine = "% Unprovable.\n" ) then - - ( let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) val _ = TextIO.output (outfile, (thisLine)) @@ -183,7 +132,7 @@ (* Attempt to prevent several signals from turning up simultaneously *) Posix.Process.sleep(Time.fromSeconds 1); true - end) + end else if (thisLine = "% Proof not found. Time limit expired.\n") then (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/ATP/recon_prelim.ML --- a/src/HOL/Tools/ATP/recon_prelim.ML Wed Sep 07 09:53:50 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_prelim.ML Wed Sep 07 09:54:31 2005 +0200 @@ -121,10 +121,6 @@ fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]); -fun int_of_string str = - (case Int.fromString str of SOME n => n - | NONE => error ("int_of_string: " ^ str)); - val no_lines = filter_out (equal "\n"); exception ASSERTION of string; diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Wed Sep 07 09:53:50 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Wed Sep 07 09:54:31 2005 +0200 @@ -108,18 +108,17 @@ signature RES_CLASIMP = sig - val relevant : int ref val use_simpset: bool ref val use_nameless: bool ref - val write_out_clasimp : string -> theory -> term -> - (ResClause.clause * thm) Array.array * int * ResClause.clause list - + val get_clasimp_lemmas : + theory -> term -> + (ResClause.clause * thm) Array.array * int * ResClause.clause list end; structure ResClasimp : RES_CLASIMP = struct -val use_simpset = ref true; +val use_simpset = ref false; (*Performance is much better without simprules*) val use_nameless = ref false; (*Because most are useless [iff] rules*) val relevant = ref 0; (*Relevance filtering is off by default*) @@ -143,35 +142,20 @@ (* outputs a list of (thm,clause) pairs *) - -(*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 multi x 0 xlist = xlist + |multi x n xlist = multi x (n-1) (x::xlist); -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) +fun clause_numbering ((clause, theorem), num_of_cls) = + let val numbers = 0 upto (num_of_cls - 1) in - multi (clause, theorem) num_of_cls [] + multi (clause, theorem) num_of_cls [] end; (*Write out the claset and simpset rules of the supplied theory. FIXME: argument "goal" is a hack to allow relevance filtering. To reduce the number of clauses produced, set ResClasimp.relevant:=1*) -fun write_out_clasimp filename thy goal = +fun get_clasimp_lemmas thy goal = let val claset_rules = map put_name_pair (ReduceAxiomsN.relevant_filter (!relevant) goal @@ -188,27 +172,19 @@ else claset_cls_thms; val cls_thms_list = List.concat cls_thms; (*************************************************) - (* Write out clauses as tptp strings to filename *) + (* Identify the set of clauses to be written out *) (*************************************************) 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); + val cls_nums = map ResClause.num_of_clauses clauses; + val whole_list = List.concat + (map clause_numbering (ListPair.zip (cls_thms_list, cls_nums))); (*********************************************************) (* 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; - val out = TextIO.openOut filename; - val _= ResLib.writeln_strs out stick_clasrls; - val _= TextIO.closeOut out in - (clause_arr, num_of_clauses, clauses) + (clause_arr, List.length whole_list, clauses) end; diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Wed Sep 07 09:53:50 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Wed Sep 07 09:54:31 2005 +0200 @@ -13,10 +13,40 @@ (* Hardwired version of where to pick up the tptp files for the moment *) (***************************************************************************) -(*use "Proof_Transfer"; -use "VampireCommunication"; -use "SpassCommunication";*) -(*use "/homes/clq20/Jia_Code/TransStartIsar";*) + +signature WATCHER = +sig + +(*****************************************************************************************) +(* Send request to Watcher for multiple spasses to be called for filenames in arg *) +(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *) +(*****************************************************************************************) + +val callResProvers : + TextIO.outstream * (string*string*string*string*string*string*string*string) list + -> unit + +(************************************************************************) +(* Send message to watcher to kill currently running resolution provers *) +(************************************************************************) + +val callSlayer : TextIO.outstream -> unit + +(**********************************************************) +(* Start a watcher and set up signal handlers *) +(**********************************************************) + +val createWatcher : thm*(ResClause.clause * thm) Array.array * int -> TextIO.instream * TextIO.outstream * Posix.Process.pid + +(**********************************************************) +(* Kill watcher process *) +(**********************************************************) + +val killWatcher : Posix.Process.pid -> unit + +end + + structure Watcher: WATCHER = @@ -128,16 +158,6 @@ ((ys@[thisLine])) end -(********************************************************************************) -(* Remove the \n character from the end of each filename *) -(********************************************************************************) - -(*fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) - in - if (String.isPrefix "\n" (implode backList )) - then (implode (rev ((tl backList)))) - else cmdStr - end*) (********************************************************************************) (* Send request to Watcher for a vampire to be called for filename in arg *) @@ -153,31 +173,24 @@ (*****************************************************************************************) -(* need to modify to send over hyps file too *) +(*Uses the $-character to separate items sent to watcher*) fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) | callResProvers (toWatcherStr, - (prover,thmstring,goalstring, proverCmd,settings,clasimpfile, + (prover,thmstring,goalstring, proverCmd,settings, axfile, hypsfile,probfile) :: args) = let val _ = File.write (File.tmp_path (Path.basic "tog_comms")) (prover^thmstring^goalstring^proverCmd^settings^ - clasimpfile^hypsfile^probfile) + hypsfile^probfile) in sendOutput (toWatcherStr, (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^ - settings^"$"^clasimpfile^"$"^hypsfile^"$"^probfile^"\n")); + settings^"$"^hypsfile^"$"^probfile^"\n")); goals_being_watched := (!goals_being_watched) + 1; TextIO.flushOut toWatcherStr; callResProvers (toWatcherStr,args) end - -(* -fun callResProversStr (toWatcherStr, []) = "End of calls\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 *) @@ -193,111 +206,40 @@ (* prover, proverCmd, settings and file from input string *) (**************************************************************) - - fun takeUntil ch [] res = (res, []) - | takeUntil ch (x::xs) res = - if x = ch then (res, xs) - else takeUntil ch xs (res@[x]) - - fun getSettings [] settings = settings -| getSettings (xs) settings = - let val (set, rest ) = takeUntil "%" xs [] - in - getSettings rest (settings@[(implode set)]) - end - fun separateFields str = - let val outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field"))) - val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") ) - val _ = TextIO.closeOut outfile - val (prover, rest) = takeUntil "$" str [] - val prover = implode prover - - val (thmstring, rest) = takeUntil "$" rest [] - val thmstring = implode thmstring - - val (goalstring, rest) = takeUntil "$" rest [] - val goalstring = implode goalstring - - val (proverCmd, rest ) = takeUntil "$" rest [] - val proverCmd = implode proverCmd - - val (settings, rest) = takeUntil "$" rest [] - val settings = getSettings settings [] - - val (clasimpfile, rest ) = takeUntil "$" rest [] - val clasimpfile = implode clasimpfile - - val (hypsfile, rest ) = takeUntil "$" rest [] - val hypsfile = implode hypsfile - - val (file, rest) = takeUntil "$" rest [] - val file = implode file - + let val _ = File.append (File.tmp_path (Path.basic "sep_field")) + ("In separateFields, str is: " ^ str ^ "\n\n") + val [prover,thmstring,goalstring,proverCmd,settingstr,hypsfile,probfile] = + String.tokens (fn c => c = #"$") str + val settings = String.tokens (fn c => c = #"%") settingstr val _ = File.append (File.tmp_path (Path.basic "sep_comms")) - ("Sep comms are: "^(implode str)^"**"^ + ("Sep comms are: "^ str ^"**"^ prover^" thmstring: "^thmstring^"\n goalstr: "^goalstring^ - " \n provercmd: "^proverCmd^" \n clasimp "^clasimpfile^ - " \n hyps "^hypsfile^"\n prob "^file^"\n\n") + " \n provercmd: "^proverCmd^ + " \n hyps "^hypsfile^"\n prob "^probfile^"\n\n") in - (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file) + (prover,thmstring,goalstring, proverCmd, settings, hypsfile, probfile) end -(***********************************************************************************) -(* do tptp2x and cat to turn clasimpfile, hypsfile and probfile into one .dfg file *) -(***********************************************************************************) - -fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile ,probfile) = +fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, hypsfile ,probfile) = let - (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) - val probID = List.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,probfile, ">", - File.platform_path wholefile]) - - (* if using spass prob_n already contains whole DFG file, otherwise need to mash axioms*) - (* from clasimpset onto problem file *) - val newfile = if !SpassComm.spass - then probfile - else (File.platform_path wholefile) - val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher")) - (thmstring^"\n goals_watched"^ - (string_of_int(!goals_being_watched))^newfile^"\n") + (thmstring ^ "\n goals_watched" ^ + (string_of_int(!goals_being_watched)) ^ probfile^"\n") in - (prover,thmstring,goalstring, proverCmd, settings,newfile) + (prover, thmstring, goalstring, proverCmd, settings, probfile) end; - - -(* remove \n from end of command and put back into tuple format *) - - -(* val cmdStr = "spass*((ALL xa. (~ P x | P xa) & (~ P xa | P x)) & (P xa | (ALL x. P x)) & ((ALL x. ~ P x) | ~ P xb) [.])*(EX x. ALL y. P x = P y) --> (EX x. P x) = (ALL y. P y)*/homes/clq20/bin/SPASS*-DocProof*/local/scratch/clq20/27023/clasimp*/local/scratch/clq20/27023/hyps*/local/scratch/clq20/27023/prob_1\n" - -val cmdStr = "vampire*(length (rev xs) = length xs [.]) & (length (rev (a # xs)) ~= length (a # xs) [.])*length (rev []) = length []*/homes/jm318/Vampire8/vkernel*-t 300%-m 100000*/local/scratch/clq20/23523/clasimp*/local/scratch/clq20/23523/hyps*/local/scratch/clq20/23523/prob_1\n" - *) - -(*FIX: are the two getCmd procs getting confused? Why do I have two anyway? *) +val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c); - fun getCmd cmdStr = - let val backList = rev(explode cmdStr) - val _ = File.append (File.tmp_path (Path.basic"cmdStr")) cmdStr - in - if (String.isPrefix "\n" (implode backList )) - then - let val newCmdStr = (rev(tl backList)) - in File.write (File.tmp_path (Path.basic"backlist")) - ("about to call sepfields with "^(implode newCmdStr)); - formatCmd (separateFields newCmdStr) - end - else formatCmd (separateFields (explode cmdStr)) - end +fun getCmd cmdStr = + let val cmdStr' = remove_newlines cmdStr + in + File.write (File.tmp_path (Path.basic"sepfields_call")) + ("about to call sepfields with " ^ cmdStr'); + formatCmd (separateFields cmdStr') + end; fun getProofCmd (a,b,c,d,e,f) = d @@ -467,7 +409,8 @@ (*********************************) | checkChildren ((childProc::otherChildren), toParentStr) = let val _ = File.append (File.tmp_path (Path.basic "child_check")) - ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n") + ("In check child, length of queue:"^ + (string_of_int (length (childProc::otherChildren)))^"\n") val (childInput,childOutput) = cmdstreamsOf childProc val child_handle= cmdchildHandle childProc (* childCmd is the .dfg file that the problem is in *) @@ -475,11 +418,12 @@ val _ = File.append (File.tmp_path (Path.basic "child_command")) (childCmd^"\n") (* now get the number of the subgoal from the filename *) - val sg_num = (*if (!SpassComm.spass ) - then - int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd))) - else*) - int_of_string(hd (rev(explode childCmd))) + val path_parts = String.tokens(fn c => c = #"/") childCmd + val digits = String.translate + (fn c => if Char.isDigit c then str c else "") + (List.last path_parts); + val sg_num = (case Int.fromString digits of SOME n => n + | NONE => error ("Watcher could not read subgoal nunber: " ^ childCmd)); val childIncoming = pollChildInput childInput val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/ATP/watcher.sig --- a/src/HOL/Tools/ATP/watcher.sig Wed Sep 07 09:53:50 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -(* ID: $Id$ - Author: Claire Quigley - Copyright 2004 University of Cambridge -*) - -(***************************************************************************) -(* The watcher process starts a Spass process when it receives a *) -(* message from Isabelle *) -(* Signals Isabelle, puts output of child into pipe to Isabelle, *) -(* and removes dead processes. Also possible to kill all the vampire *) -(* processes currently running. *) -(***************************************************************************) - - -signature WATCHER = -sig - -(*****************************************************************************************) -(* Send request to Watcher for multiple spasses to be called for filenames in arg *) -(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *) -(*****************************************************************************************) - -val callResProvers : TextIO.outstream *(string* string*string *string*string*string*string*string*string) list -> unit - - - -(************************************************************************) -(* Send message to watcher to kill currently running resolution provers *) -(************************************************************************) - -val callSlayer : TextIO.outstream -> unit - - - -(**********************************************************) -(* Start a watcher and set up signal handlers *) -(**********************************************************) - -val createWatcher : Thm.thm*(ResClause.clause * Thm.thm) Array.array * int -> TextIO.instream * TextIO.outstream * Posix.Process.pid - - - -(**********************************************************) -(* Kill watcher process *) -(**********************************************************) - -val killWatcher : (Posix.Process.pid) -> unit - - -end diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Sep 07 09:53:50 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Wed Sep 07 09:54:31 2005 +0200 @@ -8,14 +8,11 @@ signature RES_ATP = sig val axiom_file : Path.T -(*val atp_ax_tac : thm list -> int -> Tactical.tactic*) -(*val atp_tac : int -> Tactical.tactic*) val full_spass: bool ref -(*val spass: bool ref*) + val spass: bool ref val vampire: bool ref val custom_spass: string list ref val hook_count: int ref -(* val invoke_atp: Toplevel.transition -> Toplevel.transition*) end; structure ResAtp: RES_ATP = @@ -27,32 +24,14 @@ fun debug_tac tac = (debug "testing"; tac); -val full_spass = ref false; - -(* use spass as default prover *) -(*val spass = ref true;*) - -val custom_spass = ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub","-DocProof","-TimeLimit=60"]; -val vampire = ref false; - -val skolem_tac = skolemize_tac; - -val num_of_clauses = ref 0; -val clause_arr = Array.array (3500, ("empty", 0)); - - -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); +val vampire = ref false; (* use Vampire as default prover? *) +val spass = ref true; (* use spass as default prover *) +val full_spass = ref true; (*specifies Auto mode: SPASS can use all inference rules*) +val custom_spass = (*specialized options for SPASS*) + ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub", + "-DocProof","-TimeLimit=60"]; val axiom_file = File.tmp_path (Path.basic "axioms"); -val clasimp_file = File.tmp_path (Path.basic "clasimp"); val hyps_file = File.tmp_path (Path.basic "hyps"); val prob_file = File.tmp_path (Path.basic "prob"); @@ -82,12 +61,11 @@ fun repeat_someI_ex thm = repeat_RS thm someI_ex; -(*FIXME: is function isar_atp_h used? If not, delete!*) (*********************************************************************) (* convert clauses from "assume" to conjecture. write to file "hyps" *) (* hypotheses of the goal currently being proved *) (*********************************************************************) -(*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *) +(*perhaps have 2 different versions of this, depending on whether or not spass is set *) fun isar_atp_h thms = let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms val prems' = map repeat_someI_ex prems @@ -112,7 +90,7 @@ (* where N is the number of this subgoal *) (*********************************************************************) -fun tptp_inputs_tfrees thms n tfrees = +fun tptp_inputs_tfrees thms n tfrees axclauses = let val _ = debug ("in tptp_inputs_tfrees 0") val clss = map (ResClause.make_conjecture_clause_thm) thms @@ -124,6 +102,7 @@ val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n val out = TextIO.openOut(probfile) in + ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses)); ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; debug probfile @@ -160,7 +139,6 @@ val axfile = (File.platform_path axiom_file) val hypsfile = (File.platform_path hyps_file) - val clasimpfile = (File.platform_path clasimp_file) fun make_atp_list [] sign n = [] | make_atp_list ((sko_thm, sg_term)::xs) sign n = @@ -174,7 +152,7 @@ val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n) val _ = debug ("prob file in call_resolve_tac is " ^ probfile) in - if !SpassComm.spass + if !spass then let val optionline = (*Custom SPASS options, or default?*) if !full_spass (*Auto mode: all SPASS inference rules*) @@ -186,7 +164,7 @@ in ([("spass", thmstr, goalstring, getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", - optionline, clasimpfile, axfile, hypsfile, probfile)] @ + optionline, axfile, hypsfile, probfile)] @ (make_atp_list xs sign (n+1))) end else if !vampire @@ -194,14 +172,14 @@ let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel" in ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000", - clasimpfile, axfile, hypsfile, probfile)] @ + axfile, hypsfile, probfile)] @ (make_atp_list xs sign (n+1))) end else let val Eprover = ResLib.helper_path "E_HOME" "eproof" in ([("E", thmstr, goalstring, Eprover, "--tptp-in -l5", - clasimpfile, axfile, hypsfile, probfile)] @ + axfile, hypsfile, probfile)] @ (make_atp_list xs sign (n+1))) end @@ -228,11 +206,11 @@ else ( SELECT_GOAL - (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, + (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, METAHYPS(fn negs => - (if !SpassComm.spass + (if !spass then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses - else tptp_inputs_tfrees (make_clauses negs) n tfrees; + else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses; get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n -1) (negs::sko_thms) axclauses; all_tac))]) n thm ) @@ -297,9 +275,8 @@ (*set up variables for writing out the clasimps to a tptp file*) val (clause_arr, num_of_clauses, axclauses) = - ResClasimp.write_out_clasimp (File.platform_path clasimp_file) thy - (hd prems) (*FIXME: hack!! need to do all prems*) - val _ = debug ("clasimp_file is " ^ File.platform_path clasimp_file ^ " with " ^ (string_of_int num_of_clauses)^ " clauses") + ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*) + val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^ " clauses") val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses) val pid_string = string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid))) @@ -355,9 +332,7 @@ (** the Isar toplevel hook **) val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state => - let - val proof = Toplevel.proof_of state val (ctxt, (_, goal)) = Proof.get_goal proof handle Proof.STATE _ => error "No goal present"; diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Sep 07 09:53:50 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Wed Sep 07 09:54:31 2005 +0200 @@ -30,6 +30,7 @@ val clause_info : clause -> string * string val typed : unit -> unit val untyped : unit -> unit + val num_of_clauses : clause -> int val dfg_clauses2str : string list -> string val clause2dfg : clause -> string * string list @@ -626,6 +627,12 @@ make_arity_clause (cls_id,Axiom,conclLit,premLits) end; +(*The number of clauses generated from cls, including type clauses*) +fun num_of_clauses (Clause cls) = + let val num_tfree_lits = + if !keep_types then length (#tfree_type_literals cls) + else 0 + in 1 + num_tfree_lits end; (**** Isabelle class relations ****) @@ -818,8 +825,6 @@ end; - - fun concat_with sep [] = "" | concat_with sep [x] = "(" ^ x ^ ")" | concat_with sep (x::xs) = "(" ^ x ^ ")" ^ sep ^ (concat_with sep xs); @@ -954,20 +959,14 @@ ResLib.writeln_strs out str; TextIO.closeOut out end; -(*val filestr = clauses2dfg newcls "flump" [] [] [] []; -*) -(* fileout "flump.dfg" [filestr];*) -(*FIX: ask Jia what this is for *) - - -fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls); - +fun string_of_arClauseID (ArityClause arcls) = + arclause_prefix ^ string_of_int(#clause_id arcls); fun string_of_arLit (TConsLit(b,(c,t,args))) = let val pol = if b then "++" else "--" - val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args) + val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args) in pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" end @@ -1027,8 +1026,6 @@ (* code to produce TPTP files *) (********************************) - - fun tptp_literal (Literal(pol,pred,tag)) = let val pred_string = string_of_predicate pred val tagged_pol = @@ -1054,7 +1051,6 @@ "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "])."; - fun tptp_clause_aux (Clause cls) = let val lits = map tptp_literal (#literals cls) val tvar_lits_strs = @@ -1066,26 +1062,27 @@ then (map tptp_of_typeLit (#tfree_type_literals cls)) else [] in - (tvar_lits_strs @ lits,tfree_lits) + (tvar_lits_strs @ lits, tfree_lits) end; - fun tptp_clause cls = - let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) + let val (lits,tfree_lits) = tptp_clause_aux cls + (*"lits" includes the typing assumptions (TVars)*) val cls_id = string_of_clauseID cls val ax_name = string_of_axiomName cls val knd = string_of_kind cls val lits_str = ResLib.list_to_string' lits - val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) fun typ_clss k [] = [] + val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) + fun typ_clss k [] = [] | typ_clss k (tfree :: tfrees) = - (gen_tptp_type_cls(cls_id,knd,tfree,k)) :: (typ_clss (k+1) tfrees) + (gen_tptp_type_cls(cls_id,knd,tfree,k)) :: typ_clss (k+1) tfrees in cls_str :: (typ_clss 0 tfree_lits) end; - fun clause2tptp cls = - let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) + let val (lits,tfree_lits) = tptp_clause_aux cls + (*"lits" includes the typing assumptions (TVars)*) val cls_id = string_of_clauseID cls val ax_name = string_of_axiomName cls val knd = string_of_kind cls diff -r c33c9e9df4f8 -r 6cef3aedd661 src/HOL/Tools/res_lib.ML --- a/src/HOL/Tools/res_lib.ML Wed Sep 07 09:53:50 2005 +0200 +++ b/src/HOL/Tools/res_lib.ML Wed Sep 07 09:54:31 2005 +0200 @@ -8,6 +8,7 @@ signature RES_LIB = sig +val atomize_tac : int -> tactic val flat_noDup : ''a list list -> ''a list val helper_path : string -> string -> string val list2str_sep : string -> string list -> string @@ -16,7 +17,6 @@ val no_rep_add : ''a -> ''a list -> ''a list val no_rep_app : ''a list -> ''a list -> ''a list val pair_ins : 'a -> 'b list -> ('a * 'b) list -val rm_rep : ''a list -> ''a list val trim_ends : string -> string val write_strs : TextIO.outstream -> TextIO.vector list -> unit val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit @@ -26,6 +26,17 @@ structure ResLib : RES_LIB = struct +val atomize_tac = + SUBGOAL + (fn (prop,_) => + let val ts = Logic.strip_assums_hyp prop + val atom = ObjectLogic.atomize_thm o forall_intr_vars + in EVERY1 + [METAHYPS + (fn hyps => cut_facts_tac (map atom hyps) 1), + REPEAT_DETERM_N (length ts) o (etac thin_rl)] + end); + (*Remove both ends from the string (presumably quotation marks?)*) fun trim_ends s = String.substring(s,1,String.size s - 2); @@ -57,9 +68,6 @@ fun no_rep_app l1 [] = l1 | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y; -fun rm_rep [] = [] - | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y); - fun flat_noDup [] = [] | flat_noDup (x::y) = no_rep_app x (flat_noDup y);