Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
ruleset.
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Tue May 31 12:36:01 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Tue May 31 12:42:36 2005 +0200
@@ -7,6 +7,20 @@
(***************************************************************************)
(* Code to deal with the transfer of proofs from a Spass process *)
(***************************************************************************)
+signature SPASS_COMM =
+ sig
+ val reconstruct : 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 =
+struct
+
+(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
+val reconstruct = ref true;
(***********************************)
(* Write Spass output to a file *)
@@ -42,7 +56,13 @@
in
SELECT_GOAL
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
- METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs clause_arr num_of_clauses ))]) sg_num
+ METAHYPS(fn negs => (if !reconstruct
+ then
+ Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring
+ toParent ppid negs clause_arr num_of_clauses
+ else
+ Recon_Transfer.spassString_to_lemmaString proofextract thmstring goalstring
+ toParent ppid negs clause_arr num_of_clauses ))]) sg_num
end ;
@@ -111,7 +131,7 @@
fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) =
let val spass_proof_file = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));
- val _ = TextIO.output (outfile, "checking proof found, thm is: "^(string_of_thm thm))
+ val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm))
val _ = TextIO.closeOut outfile
in
@@ -140,8 +160,8 @@
val _ = TextIO.closeOut outfile
in
- (*TextIO.output (toParent,childCmd^"\n" );
- TextIO.flushOut toParent;*)
+ TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
TextIO.output (spass_proof_file, (thisLine));
TextIO.flushOut spass_proof_file;
TextIO.closeOut spass_proof_file;
@@ -224,6 +244,18 @@
(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
(
@@ -245,3 +277,4 @@
("No output from reconstruction process.\n","","")
+end;
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 31 12:36:01 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 31 12:42:36 2005 +0200
@@ -1,6 +1,7 @@
+
(* ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
*)
(******************)
@@ -195,19 +196,66 @@
| retrieve_axioms clause_arr (x::xs) = [Array.sub(clause_arr, x)]@
(retrieve_axioms clause_arr xs)
+fun subone x = x - 1
+
+fun numstr [] = ""
+| numstr (x::xs) = (string_of_int x)^"%"^(numstr xs)
+
(* retrieve the axioms that were obtained from the clasimpset *)
fun get_clasimp_cls clause_arr clasimp_num step_nums =
- let val clasimp_nums = List.filter (is_clasimp_ax 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.sysify_path(File.tmp_path (Path.basic "axnums")))
+ val _ = TextIO.output(axnums,(numstr clasimp_nums))
+ val _ = TextIO.closeOut(axnums)
in
retrieve_axioms clause_arr clasimp_nums
end
+fun get_cls [] = []
+| get_cls (x::xs) = ((#1 x)::(get_cls xs))
+
+(* add array and table here, so can retrieve clasimp axioms *)
+
+ fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * Thm.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 []
+
+ (***********************************************)
+ (* here need to add the clauses from clause_arr*)
+ (***********************************************)
+
+ val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums
+ val clauses=(get_cls clasimp_names_cls)
+ val (names_clsnums) = map ResClause.clause_info clauses
+ val clasimp_names = map fst names_clsnums
+
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names
+ val _ = TextIO.output (outfile,clasimp_namestr)
+ val _ = TextIO.closeOut outfile
+ val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
+
+ in
+ (clasimp_names)
+ end
+
+fun numclstr (vars, []) str = str
+| numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
+in
+numclstr (vars,rest) newstr
+end
+fun addvars c (a,b) = (a,b,c)
-(* add array and table here, so can retrieve clasimp axioms *)
fun get_axioms_used proof_steps thms clause_arr num_of_clauses =
let
@@ -293,32 +341,8 @@
(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
end
-fun numclstr (vars, []) str = str
-| numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
-in
-numclstr (vars,rest) newstr
-end
-(*
-
-val proofstr = "Did parsing on Here is a proof with depth 4, length 9 :\
-\1[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\
-\3[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\
-\5[0:Inp] || -> v_P(tconst_fun(typ__da_a,tconst_bool),U)* v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\
-\7[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\
-\9[0:Fac:5.0,5.1] || -> v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\
-\10[0:Res:9.0,3.0] || -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\
-\11[0:Res:10.0,1.0] || -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\
-\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\
-\14[0:Res:11.0,12.0] || -> .\
-\Formulae used in the proof :"
-
-*)
-
-
-fun addvars c (a,b) = (a,b,c)
-
-
+
(*********************************************************************)
(* Pass in spass string of proof and string version of isabelle goal *)
@@ -326,52 +350,74 @@
(*********************************************************************)
-(*
-
+fun rules_to_string [] str = str
+| rules_to_string [x] str = str^x
+| rules_to_string (x::xs) str = rules_to_string xs (str^x^" ")
+
-val proofstr = "Here is a proof with depth 2, length 5 :\
-\1[0:Inp] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
-\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\
-\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa).\
-\7[0:Res:1.0,5.0] || -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
-\9[0:Res:7.0,3.0] || -> .\
-\Formulae used in the proof :"
+val dummy_tac = PRIMITIVE(fn thm => thm );
-val proofstr = "Here is a proof with depth 4, length 9 :\
-\1[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
-\3[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\
-\5[0:Inp] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)* v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
-\7[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\
-\9[0:Fac:5.0,5.1] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
-\10[0:Res:9.0,3.0] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\
-\11[0:Res:10.0,1.0] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
-\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\
-\14[0:Res:11.0,12.0] || -> .\
-\Formulae used in the proof :";
+fun spassString_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_steps1 = 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 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;
+ 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!" ^"\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 thmstring = " (~ (P::'a::type => bool) (x::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | P (x::'a::type)) & ((P::'a::type => bool) (xa::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | ~ P (xb::'a::type))";
-
-val thmstring = "(ALL xb::'a::type. (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) | (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) & P xb & ~ Q xb)"
-
-
-val thmstring ="(ALL xb::'a::type. (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) | (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) & P xb & ~ Q xb)"
-
-val proofstr = "Did parsing on Here is a proof with depth 2, length 5 :\
-\1[0:Inp] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
-\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\
-\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x(tconst_fun(typ__asc39_a,typ__asc39_a),U))* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U)).\
-\7[0:Res:1.0,5.0] || -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U))*.\
-\9[0:Res:7.0,3.0] || -> .\
-\Formulae used in the proof :";
-
-*)
-
-
-
-
-val dummy_tac = PRIMITIVE(fn thm => thm );
fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses =
let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));
@@ -474,10 +520,6 @@
-
-
-
-
(**********************************************************************************)
(* At other end, want to turn back into datatype so can apply reconstruct_proof. *)
(* This will be done by the signal handler *)
@@ -808,4 +850,6 @@
end
+
+
end;
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 31 12:36:01 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 31 12:42:36 2005 +0200
@@ -5,7 +5,7 @@
Copyright 2004 University of Cambridge
*)
-signature RES_CLASIMP =
+signature RES_CLASIMP =
sig
val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int
end;
@@ -50,6 +50,30 @@
(*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 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)
+ val multi_name = multi (clause, theorem) num_of_cls []
+ in
+ (multi_name)
+ end;
+
+
+
+
fun write_out_clasimp filename =
let val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
@@ -64,22 +88,25 @@
val cls_thms = (claset_cls_thms@simpset_cls_thms);
val cls_thms_list = List.concat cls_thms;
-
- (*********************************************************)
- (* create array and put clausename, number pairs into it *)
- (*********************************************************)
- val num_of_clauses = 0;
- val clause_arr = Array.fromList cls_thms_list;
-
- val num_of_clauses = List.length cls_thms_list;
-
+ (* length 1429 *)
(*************************************************)
(* Write out clauses as tptp strings to filename *)
(*************************************************)
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);
+
+ (*********************************************************)
+ (* 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;
+ (* length 1581*)
val out = TextIO.openOut filename;
val _= ResLib.writeln_strs out stick_clasrls;
val _= TextIO.flushOut out;
@@ -88,6 +115,7 @@
(clause_arr, num_of_clauses)
end;
-
end;
+
+
--- a/src/HOL/Tools/ATP/watcher.ML Tue May 31 12:36:01 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Tue May 31 12:42:36 2005 +0200
@@ -1,4 +1,5 @@
(* Title: Watcher.ML
+
ID: $Id$
Author: Claire Quigley
Copyright 2004 University of Cambridge
@@ -162,27 +163,28 @@
val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
(thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")
(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
- val probID = ReconOrderClauses.last(explode probfile)
+ val probID = ReconOrderClauses.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 ***)
- (*FIXME: find a way that works for SML/NJ too: it regards > as a filename!*)
- val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)])
+
+ (*** hyps/local axioms just now (*,axfile, hypsfile,*) ***)
+ val whole_prob_file = system ("/bin/cat " ^ clasimpfile ^" "^ 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_path = File.sysify_path dfg_dir;
- val tptp2x_args = ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]
val exec_tptp2x =
- Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", tptp2x_args)
+ 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"
in
goals_being_watched := (!goals_being_watched) + 1;
- Posix.Process.sleep(Time.fromSeconds 4);
+ Posix.Process.sleep(Time.fromSeconds 1);
(warning ("probfile is: "^probfile));
(warning("dfg file is: "^newfile));
(warning ("wholefile is: "^(File.sysify_path wholefile)));
@@ -195,8 +197,8 @@
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 " ^
- space_implode " " tptp2x_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"
@@ -381,7 +383,7 @@
in
if (isSome pd ) then
let val pd' = OS.IO.pollIn (valOf pd)
- val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100))
+ val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000))
in
if null pdl
then
@@ -407,7 +409,7 @@
in
if (isSome pd ) then
let val pd' = OS.IO.pollIn (valOf pd)
- val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100))
+ val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000))
in
if null pdl
then
@@ -456,7 +458,7 @@
(* 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" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) )
+ (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"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 *)
@@ -700,81 +702,123 @@
status
end
-fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
- let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
- val streams =snd mychild
- val childin = fst streams
- val childout = snd streams
- val childpid = fst mychild
- val sign = sign_of_thm thm
- val prems = prems_of thm
- val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
- 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"));() )
-
+
+fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
+ val streams =snd mychild
+ val childin = fst streams
+ val childout = snd streams
+ val childpid = fst mychild
+ val sign = sign_of_thm thm
+ val prems = prems_of thm
+ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
+ 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"));() )
+
+
+fun spass_proofHandler (n) = (
+ let val outfile = TextIO.openOut(File.sysify_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 outfile = TextIO.openAppend(File.sysify_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))))
+ val _ = TextIO.closeOut outfile
+ in (* if a proof has been found and sent back as a reconstruction proof *)
+ if ( (substring (reconstr, 0,1))= "[")
+ then
- fun spass_proofHandler (n) = (
- let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n"
- val (reconstr, thmstring, goalstring) = getSpassInput childin
- val _ = File.append (File.tmp_path (Path.basic "foo_signal"))
- ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))
- in (* if a proof has been found and sent back as a reconstruction proof *)
- if ( (substring (reconstr, 0,1))= "[")
- then
- (
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Recon_Transfer.apply_res_thm reconstr goalstring;
- Pretty.writeln(Pretty.str (oct_char "361"));
-
- goals_being_watched := ((!goals_being_watched) - 1);
-
- if ((!goals_being_watched) = 0)
- then
- (let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
- ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")
- in
- reapWatcher (childpid,childin, childout); ()
- end)
- else ()
- )
- (* if there's no proof, but a message from Spass *)
- else if ((substring (reconstr, 0,5))= "SPASS")
- then
- (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 (oct_char "361"));
- if (!goals_being_watched = 0)
- then
- (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
- ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
- reapWatcher (childpid,childin, childout); ())
- else
- ()
- )
- (* if proof translation failed *)
- else if ((substring (reconstr, 0,5)) = "Proof")
- then
- (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 (oct_char "361"));
- if (!goals_being_watched = 0)
- then
- (File.write(File.tmp_path (Path.basic "foo_reap_comp"))
- ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
- reapWatcher (childpid,childin, childout); ())
- else ())
- else () (* add something here ?*)
- end)
+ (
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Recon_Transfer.apply_res_thm reconstr goalstring;
+ Pretty.writeln(Pretty.str (oct_char "361"));
+
+ goals_being_watched := ((!goals_being_watched) - 1);
+
+ if ((!goals_being_watched) = 0)
+ then
+ (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
+ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
+ val _ = TextIO.closeOut outfile
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
+ end)
+ else
+ ()
+ )
+ (* if there's no proof, but a message from Spass *)
+ else if ((substring (reconstr, 0,5))= "SPASS")
+ then
+ (
+ 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 (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
+ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
+ val _ = TextIO.closeOut outfile
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
+ end )
+ else
+ ()
+ )
+ (* print out a list of rules used from clasimpset*)
+ else if ((substring (reconstr, 0,5))= "Rules")
+ then
+ (
+ 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 (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
+ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
+ val _ = TextIO.closeOut outfile
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout);()
+ end )
+ else
+ ()
+ )
+
+ (* if proof translation failed *)
+ else if ((substring (reconstr, 0,5)) = "Proof")
+ then
+ (
+ 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 (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
+ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
+ val _ = TextIO.closeOut outfile
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
+ end )
+ else
+ ()
+ )
-
- in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
- IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
- (childin, childout, childpid)
+ else (* add something here ?*)
+ ()
+
+ end)
+
+
+
+ in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
+ IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
+ (childin, childout, childpid)
+
end
--- a/src/HOL/Tools/res_atp.ML Tue May 31 12:36:01 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue May 31 12:42:36 2005 +0200
@@ -21,7 +21,7 @@
(*val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic*)
(*val atp_tac : int -> Tactical.tactic*)
val debug: bool ref
-
+val full_spass: bool ref
end;
structure ResAtp : RES_ATP =
@@ -38,6 +38,7 @@
(* default value is false *)
val trace_res = ref false;
+val full_spass = ref false;
val skolem_tac = skolemize_tac;
@@ -188,11 +189,19 @@
[("spass",thmstr,goalstring,*spass_home*,
"-DocProof",
clasimpfile, axfile, hypsfile, probfile)]);*)
- Watcher.callResProvers(childout,
+ if !full_spass
+ then
+ (Watcher.callResProvers(childout,
+ [("spass", thmstr, goalstring (*,spass_home*),
+ getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
+ "-DocProof",
+ clasimpfile, axfile, hypsfile, probfile)]))
+ else
+ (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)]);
+ clasimpfile, axfile, hypsfile, probfile)]));
(* with paramodulation *)
(*Watcher.callResProvers(childout,
--- a/src/HOL/Tools/res_axioms.ML Tue May 31 12:36:01 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Tue May 31 12:42:36 2005 +0200
@@ -396,7 +396,19 @@
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
-(* outputs a list of (thm,clause) pairs *)
+(* outputs a list of (clause,thm) pairs *)
+(*fun clausify_axiom_pairs (thm_name,thm) =
+ let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
+ val isa_clauses' = rm_Eps [] isa_clauses
+ val clauses_n = length isa_clauses
+ fun make_axiom_clauses _ [] []= []
+ | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls', thm_name, i) :: make_axiom_clauses (i+1) clss clss'
+ in
+ make_axiom_clauses 0 isa_clauses' isa_clauses
+ end;
+*)
+
+
fun clausify_axiom_pairs (thm_name,thm) =
let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
val isa_clauses' = rm_Eps [] isa_clauses
@@ -407,7 +419,6 @@
make_axiom_clauses 0 isa_clauses' isa_clauses
end;
-
fun clausify_rules_pairs [] err_list = ([],err_list)
| clausify_rules_pairs ((name,thm)::thms) err_list =
let val (ts,es) = clausify_rules_pairs thms err_list