# HG changeset patch # User quigley # Date 1119285564 -7200 # Node ID d0a1f6231e2fc17d556ef107c34283ed10726439 # Parent e1a36498a30f1c0e757318c4da01f2070ec18552 Added VampCommunication.ML. Changed small set of Spass rules to Ordered version. Fixed printing out of resolution proofs if parsing/translation fails. diff -r e1a36498a30f -r d0a1f6231e2f src/HOL/Tools/ATP/SpassCommunication.ML --- a/src/HOL/Tools/ATP/SpassCommunication.ML Mon Jun 20 16:41:47 2005 +0200 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML Mon Jun 20 18:39:24 2005 +0200 @@ -10,6 +10,7 @@ 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 @@ -21,6 +22,7 @@ (* 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 *) diff -r e1a36498a30f -r d0a1f6231e2f src/HOL/Tools/ATP/VampCommunication.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/VampCommunication.ML Mon Jun 20 18:39:24 2005 +0200 @@ -0,0 +1,281 @@ +(* Title: VampCommunication.ml + ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) + +(***************************************************************************) +(* Code to deal with the transfer of proofs from a Vamp 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 + + end; + +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 *) +(***********************************) + +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)) + end; + +(**********************************************************************) +(* Reconstruct the Vamp 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 +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 ; + + +fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = 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) + ) + end; + + + + +(*********************************************************************************) +(* Inspect the output of a Vamp 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))) + 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) + + else + ( + startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses) + ) + end + ) + else (false) + (* end*) + + + +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 + in + if (isSome (TextIO.canInput(fromChild, 5))) + then + ( + 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 );*) + 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)) + + val _ = TextIO.closeOut outfile + in + + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (vamp_proof_file, (thisLine)); + TextIO.flushOut vamp_proof_file; + TextIO.closeOut vamp_proof_file; + (*TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; + TextIO.output (toParent, "bar\n"); + TextIO.flushOut toParent;*) + + TextIO.output (toParent, thisLine^"\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); + true + end) + else if (thisLine = "% Proof not found.\n") + then + ( + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; + + true) + + else + (TextIO.output (vamp_proof_file, (thisLine)); + TextIO.flushOut vamp_proof_file; + checkVampProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)) + + end + ) + else + (TextIO.output (vamp_proof_file, ("No proof output seen \n"));TextIO.closeOut vamp_proof_file;false) + end + + +(***********************************************************************) +(* Function used by the Isabelle process to read in a vamp proof *) +(***********************************************************************) + + + +fun getVampInput instr = if (isSome (TextIO.canInput(instr, 2))) + then + let val thisLine = TextIO.inputLine instr + val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine)) + + val _ = TextIO.closeOut outfile + in (* reconstructed proof string *) + if ( (substring (thisLine, 0,1))= "[") + then + (*Pretty.writeln(Pretty.str (thisLine))*) + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + else if (thisLine = "% Unprovable.\n" ) + then + ( + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + ) + else if (thisLine = "% Proof not found.\n") + then + ( + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (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 + ( + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getVamp"))); + val _ = TextIO.output (outfile, (thisLine)) + val _ = TextIO.closeOut outfile + in + (reconstr, thmstring, goalstring) + end + ) + else + getVampInput instr + + end + else + ("No output from reconstruction process.\n","","") + + +end; diff -r e1a36498a30f -r d0a1f6231e2f src/HOL/Tools/ATP/recon_parse.ML --- a/src/HOL/Tools/ATP/recon_parse.ML Mon Jun 20 16:41:47 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_parse.ML Mon Jun 20 18:39:24 2005 +0200 @@ -30,6 +30,8 @@ exception Noparse; exception SPASSError of string; +exception VampError of string; + fun (parser1 ++ parser2) input = let @@ -159,6 +161,9 @@ *) + + + fun several p = many (some p) fun collect (h, t) = h ^ (Utils.itlist (fn s1 => fn s2 => s1 ^ s2) t "") @@ -182,11 +187,54 @@ (* val lex = fst ( alltokens ( (map str) explode))*) fun lex s = alltokens (explode s) + +(*********************************************************) +(* Temporary code to "parse" Vampire proofs *) +(*********************************************************) + +fun num_int (Number n) = n +| num_int _ = raise VampError "Not a number" + + fun takeUntil ch [] res = (res, []) + | takeUntil ch (x::xs) res = if x = ch + then + (res, xs) + else + takeUntil ch xs (res@[x]) + +fun linenums [] nums = nums +| linenums (x::xs) nums = let val (fst, rest ) = takeUntil (Other "%") (x::xs) [] + in + if rest = [] + then + nums + else + let val num = hd rest + val int_of = num_int num + + in + linenums rest (int_of::nums) + end + end + +fun get_linenums proofstr = let val s = extract_proof proofstr + val tokens = #1(lex s) + + in + rev (linenums tokens []) + end + +(************************************************************) +(************************************************************) + + +(**************************************************) +(* Code to parse SPASS proofs *) +(**************************************************) + datatype Tree = Leaf of string | Branch of Tree * Tree - - fun number ((Number n)::rest) = (n, rest) | number _ = raise NOPARSE_NUM diff -r e1a36498a30f -r d0a1f6231e2f src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Jun 20 16:41:47 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Jun 20 18:39:24 2005 +0200 @@ -201,9 +201,9 @@ fun get_clasimp_cls clause_arr 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.platform_path(File.tmp_path (Path.basic "axnums"))) +(* val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums"))) val _ = TextIO.output(axnums,(numstr clasimp_nums)) - val _ = TextIO.closeOut(axnums) + val _ = TextIO.closeOut(axnums)*) in retrieve_axioms clause_arr clasimp_nums end @@ -235,12 +235,11 @@ clasimp_names end - fun get_axiom_names_vamp proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses = + fun get_axiom_names_vamp proofstr thms (clause_arr:(ResClause.clause * 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 [] + val step_nums =get_linenums proofstr (***********************************************) (* here need to add the clauses from clause_arr*) @@ -455,7 +454,49 @@ val _ = TextIO.output (outfile, ("In exception handler")); val _ = TextIO.closeOut outfile in - TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr) ^"\n"); + TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" ); + TextIO.flushOut toParent; + TextIO.output (toParent, (remove_linebreaks thmstring)^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, ( (remove_linebreaks 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) + + +fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = + let val outfile = TextIO.openAppend(File.platform_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 + + (***********************************) + (* get vampire axiom names *) + (***********************************) + + val (axiom_names) = get_axiom_names_vamp proofstr 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.platform_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.platform_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 for resolution proof: "^(remove_linebreaks proofstr) ); TextIO.flushOut toParent; TextIO.output (toParent, thmstring^"\n"); TextIO.flushOut toParent; @@ -467,66 +508,6 @@ end) -(*fun vampString_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_steps = VampParse.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_vamp 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;fdsa - 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 for resolution proof: \n"^(remove_linebreaks proofstr) ^"\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 proofstr = "1582[0:Inp] || -> v_P*.\ @@ -619,7 +600,7 @@ val _ = TextIO.output (outfile, ("In exception handler")); val _ = TextIO.closeOut outfile in - TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^proofstr ^"\n"); + TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\n"); TextIO.flushOut toParent; TextIO.output (toParent, thmstring^"\n"); TextIO.flushOut toParent; diff -r e1a36498a30f -r d0a1f6231e2f src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Mon Jun 20 16:41:47 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Mon Jun 20 18:39:24 2005 +0200 @@ -135,12 +135,12 @@ (* Remove the \n character from the end of each filename *) (********************************************************************************) -fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) +(*fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) in if (String.isPrefix "\n" (implode backList )) then (implode (rev ((tl backList)))) else cmdStr - end + end*) (********************************************************************************) (* Send request to Watcher for a vampire to be called for filename in arg *) @@ -270,25 +270,57 @@ val tptp2X = getenv "TPTP2X_HOME" ^ "/tptp2X" - val _ = if File.exists (File.unpack_platform_path tptp2X) then () - else error ("Could not find the file " ^ tptp2X) - - val bar = (fn s => (File.write (File.tmp_path (Path.basic "tptp2X-call")) s; system s)) - (tptp2X ^ " -fdfg -d " ^ dfg_path ^ " " ^ File.platform_path wholefile) - val newfile = dfg_path ^ "/ax_prob" ^ "_" ^ probID ^ ".dfg" - val _ = File.append (File.tmp_path (Path.basic "thmstring_in_watcher")) - (thmstring ^ "\n goals_watched" ^ - string_of_int(!goals_being_watched) ^ newfile ^ "\n") - - in - (prover,thmstring,goalstring, proverCmd, settings,newfile) - end; + + (*** need to check here if the directory exists and, if not, create it***) + + + (*** 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,(*axfile, hypsfile,*)probfile, ">", (File.platform_path wholefile)]) + val dfg_create = + if !SpassComm.spass + then + if File.exists dfg_dir + then + ((warning("dfg dir exists"));()) + else + File.mkdir dfg_dir + else + (warning("not converting to dfg");()) + val dfg_path = File.platform_path dfg_dir; + + val bar = if !SpassComm.spass then system ("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X -fdfg "^ + (File.platform_path wholefile)^" -d "^dfg_path) + else + 7 + + val newfile = if !SpassComm.spass + then + dfg_path^"/ax_prob"^"_"^(probID)^".dfg" + else + (File.platform_path wholefile) + + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"thmstring_in_watcher"))); + val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")) + val _ = TextIO.closeOut outfile + + in + (prover,thmstring,goalstring, proverCmd, settings,newfile) + 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 = "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? *) @@ -441,8 +473,14 @@ end fun pollChildInput (fromStr) = - let val iod = getInIoDesc fromStr - in + + let val _ = File.append (File.tmp_path (Path.basic "child_poll")) + ("In child_poll\n") + val iod = getInIoDesc fromStr + in + + + if isSome iod then let val pd = OS.IO.pollDesc (valOf iod) @@ -450,17 +488,22 @@ if (isSome pd ) then let val pd' = OS.IO.pollIn (valOf pd) val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) - val _ = File.append (File.tmp_path (Path.basic "child_poll")) - ("In child_poll\n") + in if null pdl then - NONE + ( File.append (File.tmp_path (Path.basic "child_poll_res")) + ("Null pdl \n");NONE) else if (OS.IO.isIn (hd pdl)) then - SOME ((*getCmd*) (TextIO.inputLine fromStr)) + (let val inval = (TextIO.inputLine fromStr) + val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n") + in + SOME inval + end) else - NONE + ( File.append (File.tmp_path (Path.basic "child_poll_res")) + ("Null pdl \n");NONE) end else NONE @@ -505,8 +548,9 @@ then (* 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" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) + val childDone = (case prover of + "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) + |"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 *) @@ -561,6 +605,7 @@ else let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (settings@[file]))) val (instr, outstr)=Unix.streamsOf childhandle + val newProcList = (((CMDPROC{ prover = prover, cmd = file, @@ -569,6 +614,8 @@ proc_handle = childhandle, instr = instr, outstr = outstr })::procList)) + + val _ = File.append (File.tmp_path (Path.basic "exec_child")) ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^(TextIO.input instr)^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) in Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList end @@ -768,14 +815,14 @@ 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"));() ) + VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() ) fun spass_proofHandler (n) = ( let val outfile = TextIO.openOut(File.platform_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 (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin val outfile = TextIO.openAppend(File.platform_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)))) @@ -808,7 +855,7 @@ ( 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 ((Recon_Transfer.restore_linebreaks goalstring)^reconstr)); Pretty.writeln(Pretty.str (oct_char "361")); if (!goals_being_watched = 0) then diff -r e1a36498a30f -r d0a1f6231e2f src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Mon Jun 20 16:41:47 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Mon Jun 20 18:39:24 2005 +0200 @@ -10,7 +10,7 @@ signature RES_ATP = -sig +sig val trace_res : bool ref val subgoals: Thm.thm list val traceflag : bool ref @@ -22,6 +22,8 @@ (*val atp_tac : int -> Tactical.tactic*) val debug: bool ref val full_spass: bool ref +(*val spass: bool ref*) +val vampire: bool ref end; structure ResAtp : RES_ATP = @@ -36,7 +38,14 @@ fun debug_tac tac = (warning "testing";tac); (* default value is false *) + val full_spass = ref false; + +(* use spass as default prover *) +(*val spass = ref true;*) + +val vampire = ref false; + val trace_res = ref false; val skolem_tac = skolemize_tac; @@ -171,16 +180,22 @@ val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) val _ = (warning ("prob file in cal_res_tac is: "^probfile)) in - if !full_spass - then + if !SpassComm.spass + then if !full_spass + then ([("spass", thmstr, goalstring (*,spass_home*), getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*), "-DocProof%-TimeLimit=60", clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) - else + else ([("spass", thmstr, goalstring (*,spass_home*), getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*), - "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", + "-Auto=0%-IORe%-IOFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", + clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) + else + ([("vampire", thmstr, goalstring (*,spass_home*), + "/homes/jm318/Vampire8/vkernel"(*( getenv "SPASS_HOME")^"/SPASS"*), + "-t 300%-m 100000", clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) end