--- 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" );
--- 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
--- 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 );*)
--- 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;
--- 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;
--- 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"))
--- 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
--- 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";
--- 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
--- 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);