Added VampCommunication.ML.
Changed small set of Spass rules to Ordered version.
Fixed printing out of resolution proofs if parsing/translation fails.
--- 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 *)
--- /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;
--- 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
--- 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;
--- 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
--- 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