--- a/src/HOL/Tools/ATP/modUnix.ML Thu May 26 10:05:28 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,280 +0,0 @@
-(* ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-(****************************************************************)
-(****** Slightly modified version of sml Unix structure *********)
-(****************************************************************)
-
-
-structure modUnix: MODUNIX =
- struct
-
-type signal = Posix.Signal.signal
-datatype exit_status = datatype Posix.Process.exit_status
-
-val fromStatus = Posix.Process.fromStatus
-
-
-fun reap(pid, instr, outstr) =
- let
- val u = TextIO.closeIn instr;
- val u = TextIO.closeOut outstr;
-
- val (_, status) =
- Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
- in
- status
- end
-
-fun fdReader (name : string, fd : Posix.IO.file_desc) =
- Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
-
-fun fdWriter (name, fd) =
- Posix.IO.mkTextWriter {
- appendMode = false,
- initBlkMode = true,
- name = name,
- chunkSize=4096,
- fd = fd
- };
-
-fun openOutFD (name, fd) =
- TextIO.mkOutstream (
- TextIO.StreamIO.mkOutstream (
- fdWriter (name, fd), IO.BLOCK_BUF));
-
-fun openInFD (name, fd) =
- TextIO.mkInstream (
- TextIO.StreamIO.mkInstream (
- fdReader (name, fd), ""));
-
-
-
-
-
-(*****************************************)
-(* The result of calling createWatcher *)
-(*****************************************)
-
-datatype proc = PROC of {
- pid : Posix.Process.pid,
- instr : TextIO.instream,
- outstr : TextIO.outstream
- };
-
-
-
-(*****************************************)
-(* The result of calling executeToList *)
-(*****************************************)
-
-datatype cmdproc = CMDPROC of {
- prover: string, (* Name of the resolution prover used, e.g. Vampire, SPASS *)
- cmd: string, (* The file containing the goal for res prover to prove *)
- thmstring: string, (* string representation of subgoal after negation, skolemization*)
- goalstring: string, (* string representation of subgoal*)
- pid : Posix.Process.pid,
- instr : TextIO.instream, (* Input stream to child process *)
- outstr : TextIO.outstream (* Output stream from child process *)
- };
-
-
-
-fun killChild pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
-
-fun childInfo (PROC{pid,instr,outstr}) = ((pid, (instr,outstr)));
-
-fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
-
-fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
-
-fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover,(cmd,(pid, (instr,outstr))));
-
-fun cmdchildPid (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (pid);
-
-fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover);
-
-fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (thmstring);
-
-fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (goalstring);
-(***************************************************************************)
-(* Takes a command - e.g. 'vampire', a list of arguments for the command, *)
-(* and a list of currently running processes. Creates a new process for *)
-(* cmd and argv and adds it to procList *)
-(***************************************************************************)
-
-
-
-
-fun mySshExecuteToList (cmd, argv, procList) = let
- val p1 = Posix.IO.pipe ()
- val p2 = Posix.IO.pipe ()
- val prover = hd argv
- val thmstring = hd(tl argv)
- val goalstring = hd(tl(tl argv))
- val argv = tl (tl argv)
-
- (* Turn the arguments into a single string. Perhaps we should quote the
- arguments. *)
- fun convArgs [] = []
- | convArgs [s] = [s]
- | convArgs (hd::tl) = hd :: " " :: convArgs tl
- val cmd_args = concat(convArgs(cmd :: argv))
-
- fun closep () = (
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p1);
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p2)
- )
- fun startChild () =(case Posix.Process.fork()
- of SOME pid => pid (* parent *)
- | NONE => let
- val oldchildin = #infd p1
- val newchildin = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val newchildout = Posix.FileSys.wordToFD 0w1
- (*val args = (["shep"]@([cmd]@argv))
- val newcmd = "/usr/bin/ssh"*)
-
- in
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = newchildin};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = newchildout};
- Posix.IO.close oldchildout;
- (* Run the command. *)
- (* Run this as a shell command. The command and arguments have
- to be a single argument. *)
- Posix.Process.exec("/bin/sh", ["sh", "-c", cmd_args])
- (*Posix.Process.exec(newcmd, args)*)
- end
- (* end case *))
- val _ = TextIO.flushOut TextIO.stdOut
- val pid = (startChild ()) handle ex => (closep(); raise ex)
- val instr = openInFD ("_exec_in", #infd p2)
- val outstr = openOutFD ("_exec_out", #outfd p1)
- val cmd = hd (rev argv)
- in
- (* close the child-side fds *)
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p1);
- (* set the fds close on exec *)
- Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- (((CMDPROC{
- prover = prover,
- cmd = cmd,
- thmstring = thmstring,
- goalstring = goalstring,
- pid = pid,
- instr = instr,
- outstr = outstr
- })::procList))
- end;
-
-
-fun myexecuteInEnv (cmd, argv, env) = let
- val p1 = Posix.IO.pipe ()
- val p2 = Posix.IO.pipe ()
- fun closep () = (
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p1);
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p2)
- )
- fun startChild () =(case Posix.Process.fork()
- of SOME pid => pid (* parent *)
- | NONE => let
- val oldchildin = #infd p1
- val newchildin = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val newchildout = Posix.FileSys.wordToFD 0w1
- in
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = newchildin};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = newchildout};
- Posix.IO.close oldchildout;
- Posix.Process.exece(cmd, argv, env)
- end
- (* end case *))
- val _ = TextIO.flushOut TextIO.stdOut
- val pid = (startChild ()) handle ex => (closep(); raise ex)
- val instr = openInFD ("_exec_in", #infd p2)
- val outstr = openOutFD ("_exec_out", #outfd p1)
- in
- (* close the child-side fds *)
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p1);
- (* set the fds close on exec *)
- Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- PROC{pid = pid,
- instr = instr,
- outstr = outstr
- }
- end;
-
-
-
-
-fun myexecuteToList (cmd, argv, procList) = let
- val p1 = Posix.IO.pipe ()
- val p2 = Posix.IO.pipe ()
- val prover = hd argv
- val thmstring = hd(tl argv)
- val goalstring = hd(tl(tl argv))
- val argv = tl (tl (tl(argv)))
-
- fun closep () = (
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p1);
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p2)
- )
- fun startChild () =(case Posix.Process.fork()
- of SOME pid => pid (* parent *)
- | NONE => let
- val oldchildin = #infd p1
- val newchildin = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val newchildout = Posix.FileSys.wordToFD 0w1
- in
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = newchildin};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = newchildout};
- Posix.IO.close oldchildout;
- Posix.Process.exec(cmd, argv)
- end
- (* end case *))
- val _ = TextIO.flushOut TextIO.stdOut
- val pid = (startChild ()) handle ex => (closep(); raise ex)
- val instr = openInFD ("_exec_in", #infd p2)
- val outstr = openOutFD ("_exec_out", #outfd p1)
- val cmd = hd (rev argv)
- in
- (* close the child-side fds *)
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p1);
- (* set the fds close on exec *)
- Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- (((CMDPROC{
- prover = prover,
- cmd = cmd,
- thmstring = thmstring,
- goalstring = goalstring,
- pid = pid,
- instr = instr,
- outstr = outstr
- })::procList))
- end;
-
-end;
--- a/src/HOL/Tools/ATP/spassshell Thu May 26 10:05:28 2005 +0200
+++ b/src/HOL/Tools/ATP/spassshell Thu May 26 16:50:07 2005 +0200
@@ -1,4 +1,4 @@
-`isatool getenv -b SPASS_HOME` $* |testoutput.py
+`isatool getenv -b SPASS_HOME`/SPASS $* |testoutput.py
#$SPASS_HOME $* |testoutput.py
--- a/src/HOL/Tools/ATP/testoutput.py Thu May 26 10:05:28 2005 +0200
+++ b/src/HOL/Tools/ATP/testoutput.py Thu May 26 16:50:07 2005 +0200
@@ -3,15 +3,6 @@
import string
import sys
-f = open ("/tmp/args", "w")
-for x in sys.argv:
- f.write("%s " % x)
-f.write("\n")
-f.close()
-
-#f = open ("/home/clq20/scratch/13354/dfg/spassprooflist", "r")
-#f = open ("/home/clq20/testoutput.py", "r")
-
mode = 0
try:
while 1:
@@ -29,25 +20,5 @@
pass
#f.close()
-
-
-
sys.exit()
-for i in range(0, 50):
- print "blah gibberish nonsense"
-
-print """Here is a proof with depth 1, length 9 :
-2[0:Inp] || v_P(tconst_fun(typ__Ha,tconst_bool),v_x)* -> v_P(tconst_fun(typ__Ha,tconst_bool),U)*.
-3[0:Inp] || v_P(tconst_fun(typ__Ha,tconst_bool),U)*+ -> v_P(tconst_fun(typ__Ha,tconst_bool),v_x)*.
-4[0:Inp] || -> v_P(tconst_fun(typ__Ha,tconst_bool),U)* v_P(tconst_fun(typ__Ha,tconst_bool),v_xa)*.
-5[0:Inp] || v_P(tconst_fun(typ__Ha,tconst_bool),v_xb)* v_P(tconst_fun(typ__Ha,tconst_bool),U)* -> .
-6[0:Con:4.0] || -> v_P(tconst_fun(typ__Ha,tconst_bool),v_xa)*.
-7[0:Con:5.1] || v_P(tconst_fun(typ__Ha,tconst_bool),v_xb)* -> .
-8[0:Res:6.0,3.0] || -> v_P(tconst_fun(typ__Ha,tconst_bool),v_x)*.
-9[0:MRR:2.0,8.0] || -> v_P(tconst_fun(typ__Ha,tconst_bool),U)*.
-10[0:UnC:9.0,7.0] || -> .
-Formulae used in the proof :
-
---------------------------SPASS-STOP------------------------------
-"""
--- a/src/HOL/Tools/ATP/watcher.ML Thu May 26 10:05:28 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Thu May 26 16:50:07 2005 +0200
@@ -15,8 +15,7 @@
(*use "Proof_Transfer";
use "VampireCommunication";
-use "SpassCommunication";
-use "modUnix";*)
+use "SpassCommunication";*)
(*use "/homes/clq20/Jia_Code/TransStartIsar";*)
@@ -137,12 +136,9 @@
fun getCmd cmdStr = let val backList = ((rev(explode cmdStr)))
in
-
if (String.isPrefix "\n" (implode backList ))
- then
- (implode (rev ((tl backList))))
- else
- (cmdStr)
+ then (implode (rev ((tl backList))))
+ else cmdStr
end
(********************************************************************************)
@@ -150,16 +146,12 @@
(********************************************************************************)
fun callResProver (toWatcherStr, arg) = (sendOutput (toWatcherStr, arg^"\n");
- TextIO.flushOut toWatcherStr
-
- )
+ TextIO.flushOut toWatcherStr)
(*****************************************************************************************)
(* Send request to Watcher for multiple provers to be called for filenames in arg *)
(*****************************************************************************************)
-
-
(* need to modify to send over hyps file too *)
fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n");
TextIO.flushOut toWatcherStr)
@@ -177,14 +169,14 @@
(*** 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.sysify_path wholefile)])
- val dfg_create =if File.exists dfg_dir
- then
- ((warning("dfg dir exists"));())
- else
- File.mkdir dfg_dir;
+ val dfg_create = if File.exists dfg_dir
+ then warning("dfg dir exists")
+ else File.mkdir dfg_dir;
val dfg_path = File.sysify_path dfg_dir;
- val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
+ val exec_tptp2x =
+ Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",
+ ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile])
(*val _ = Posix.Process.wait ()*)
(*val _ =Unix.reap exec_tptp2x*)
val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
@@ -192,16 +184,20 @@
in
goals_being_watched := (!goals_being_watched) + 1;
Posix.Process.sleep(Time.fromSeconds 1);
- (warning ("probfile is: "^probfile));
+ (warning ("probfile is: "^probfile));
(warning("dfg file is: "^newfile));
(warning ("wholefile is: "^(File.sysify_path wholefile)));
- sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
+ sendOutput (toWatcherStr,
+ prover ^ "*" ^ thmstring ^ "*" ^ goalstring ^ "*" ^ proverCmd ^
+ "*" ^ settings ^ "*" ^ newfile ^ "\n");
(*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
TextIO.flushOut toWatcherStr;
- Unix.reap exec_tptp2x;
-
- callResProvers (toWatcherStr,args)
-
+ Unix.reap exec_tptp2x;
+ if File.exists
+ (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
+ then callResProvers (toWatcherStr, args)
+ else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^
+ " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path)
end
(*
fun callResProversStr (toWatcherStr, []) = "End of calls\n"
--- a/src/HOL/Tools/res_atp.ML Thu May 26 10:05:28 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu May 26 16:50:07 2005 +0200
@@ -144,67 +144,66 @@
(* should be modified to allow other provers to be called *)
(*********************************************************************)
-fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let
- val thmstring = Meson.concat_with_and (map string_of_thm thms)
- val thm_no = length thms
- val _ = warning ("number of thms is : "^(string_of_int thm_no))
- val _ = warning ("thmstring in call_res is: "^thmstring)
-
- val goalstr = Sign.string_of_term sign sg_term
- val goalproofstring = proofstring goalstr
- val no_returns =List.filter not_newline ( goalproofstring)
- val goalstring = implode no_returns
- val _ = warning ("goalstring in call_res is: "^goalstring)
-
- (*val prob_file =File.tmp_path (Path.basic newprobfile); *)
- (*val _ =( warning ("calling make_clauses "))
- val clauses = make_clauses thms
- val _ =( warning ("called make_clauses "))*)
- (*val _ = tptp_inputs clauses prob_file*)
- val thmstring = Meson.concat_with_and (map string_of_thm thms)
-
- val goalstr = Sign.string_of_term sign sg_term
- val goalproofstring = proofstring goalstr
- val no_returns =List.filter not_newline ( goalproofstring)
- val goalstring = implode no_returns
-
- val thmproofstring = proofstring ( thmstring)
- val no_returns =List.filter not_newline ( thmproofstring)
- val thmstr = implode no_returns
-
- val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
- val axfile = (File.sysify_path axiom_file)
- val hypsfile = (File.sysify_path hyps_file)
- val clasimpfile = (File.sysify_path clasimp_file)
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile")))
- val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
- val _ = TextIO.flushOut outfile;
- val _ = TextIO.closeOut outfile
- val spass_home = getenv "SPASS_HOME"
- in
- (* without paramodulation *)
- (warning ("goalstring in call_res_tac is: "^goalstring));
- (warning ("prob file in cal_res_tac is: "^probfile));
- (* Watcher.callResProvers(childout,
- [("spass",thmstr,goalstring,(*spass_home*),
- "-DocProof",
- clasimpfile, axfile, hypsfile, probfile)]);*)
-
- Watcher.callResProvers(childout,
- [("spass",thmstr,goalstring(*,spass_home*),"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/spassshell",
- "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof",
- clasimpfile, axfile, hypsfile, probfile)]);
-
- (* with paramodulation *)
- (*Watcher.callResProvers(childout,
- [("spass",thmstr,goalstring,spass_home,
- "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof",
- prob_path)]); *)
- (* Watcher.callResProvers(childout,
- [("spass",thmstr,goalstring,spass_home,
- "-DocProof", prob_path)]);*)
- dummy_tac
- end
+fun call_resolve_tac sign thms sg_term (childin, childout,pid) n =
+ let val thmstring = Meson.concat_with_and (map string_of_thm thms)
+ val thm_no = length thms
+ val _ = warning ("number of thms is : "^(string_of_int thm_no))
+ val _ = warning ("thmstring in call_res is: "^thmstring)
+
+ val goalstr = Sign.string_of_term sign sg_term
+ val goalproofstring = proofstring goalstr
+ val no_returns =List.filter not_newline ( goalproofstring)
+ val goalstring = implode no_returns
+ val _ = warning ("goalstring in call_res is: "^goalstring)
+
+ (*val prob_file =File.tmp_path (Path.basic newprobfile); *)
+ (*val _ =( warning ("calling make_clauses "))
+ val clauses = make_clauses thms
+ val _ =( warning ("called make_clauses "))*)
+ (*val _ = tptp_inputs clauses prob_file*)
+ val thmstring = Meson.concat_with_and (map string_of_thm thms)
+
+ val goalstr = Sign.string_of_term sign sg_term
+ val goalproofstring = proofstring goalstr
+ val no_returns =List.filter not_newline ( goalproofstring)
+ val goalstring = implode no_returns
+
+ val thmproofstring = proofstring ( thmstring)
+ val no_returns =List.filter not_newline ( thmproofstring)
+ val thmstr = implode no_returns
+
+ val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
+ val axfile = (File.sysify_path axiom_file)
+ val hypsfile = (File.sysify_path hyps_file)
+ val clasimpfile = (File.sysify_path clasimp_file)
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile")))
+ val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
+ val _ = TextIO.flushOut outfile;
+ val _ = TextIO.closeOut outfile
+ in
+ (* without paramodulation *)
+ (warning ("goalstring in call_res_tac is: "^goalstring));
+ (warning ("prob file in cal_res_tac is: "^probfile));
+ (* Watcher.callResProvers(childout,
+ [("spass",thmstr,goalstring,*spass_home*,
+ "-DocProof",
+ clasimpfile, axfile, hypsfile, probfile)]);*)
+ Watcher.callResProvers(childout,
+ [("spass", thmstr, goalstring (*,spass_home*),
+ getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
+ "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof",
+ clasimpfile, axfile, hypsfile, probfile)]);
+
+ (* with paramodulation *)
+ (*Watcher.callResProvers(childout,
+ [("spass",thmstr,goalstring,spass_home,
+ "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof",
+ prob_path)]); *)
+ (* Watcher.callResProvers(childout,
+ [("spass",thmstr,goalstring,spass_home,
+ "-DocProof", prob_path)]);*)
+ dummy_tac
+ end
(**********************************************************)
(* write out the current subgoal as a tptp file, probN, *)