Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
Rewrote res_clasimpset.ML. Now produces an array of (thm, clause) in addition to writing out clasimpset as tptp strings. C.Q.
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Tue May 03 14:27:21 2005 +0200
@@ -19,7 +19,6 @@
TextIO.output (fd, thisLine); logSpassInput (instr,fd))
end;
-
(**********************************************************************)
(* Reconstruct the Spass proof w.r.t. thmstring (string version of *)
(* Isabelle goal to be proved), then transfer the reconstruction *)
@@ -38,16 +37,16 @@
end);
-fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num =
+fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr (num_of_clauses:int ) =
let val foo = TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar3")));
in
SELECT_GOAL
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
- METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs))]) sg_num
+ METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs clause_arr num_of_clauses ))]) sg_num
end ;
-fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let
+fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = let
val thisLine = TextIO.inputLine fromChild
in
if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
@@ -58,51 +57,18 @@
in
TextIO.output(foo,(proofextract));TextIO.closeOut foo;
- reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num thm
+ reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr num_of_clauses thm
end
)
else (
- transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
+ transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr, num_of_clauses)
)
end;
-(*
-fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let
- val thisLine = TextIO.inputLine fromChild
- in
- if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
- then (
- let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
- val reconstr = Recon_Transfer.spassString_to_reconString (currentString^thisLine) thmstring thm sg_num
- val foo = TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
- in
- TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
-
- TextIO.output (toParent, reconstr^"\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); ()
-
- end
-
- )
- else (
-
- transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
- )
- end;
-
-*)
(*********************************************************************************)
(* Inspect the output of a Spass process to see if it has found a proof, *)
@@ -110,7 +76,7 @@
(*********************************************************************************)
-fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num) =
+fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) =
(*let val _ = Posix.Process.wait ()
in*)
@@ -127,20 +93,22 @@
val _= TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
val _ = TextIO.closeOut outfile;
in
- transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num);
+ transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr, num_of_clauses);
true
end)
else
(
- startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num)
+ startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses)
)
end
)
else (false)
(* end*)
-fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num) =
+
+
+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))
@@ -159,7 +127,7 @@
val _ = TextIO.closeOut outfile
in
- startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num)
+ startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)
end
)
else if (thisLine= "SPASS beiseite: Completion found.\n" )
@@ -215,7 +183,7 @@
else
(TextIO.output (spass_proof_file, (thisLine));
TextIO.flushOut spass_proof_file;
- checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num))
+ checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
end
)
@@ -229,36 +197,6 @@
(***********************************************************************)
-(***********************************************************************)
-(* Function used by the Isabelle process to read in a vampire proof *)
-(***********************************************************************)
-
-(*fun getVampInput instr = let val thisLine = TextIO.inputLine instr
- in
- if (thisLine = "%============== End of proof. ==================\n" )
- then
- (
- (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
- )
- else if (thisLine = "% Unprovable.\n" )
- then
- (
- (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
- )
- else if (thisLine = "% Proof not found.\n")
- then
- (
- Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
- )
-
-
- else
- (
- Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
- )
- end;
-
-*)
fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
then
--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 03 14:27:21 2005 +0200
@@ -242,7 +242,7 @@
(* resulting thm, clause-strs in spass order, vars *)
fun rearrange_clause thm res_strlist allvars =
- let val isa_strlist = get_meta_lits thm
+ let val isa_strlist = get_meta_lits thm (* change this to use Jia's code to get same looking thing as isastrlist? *)
val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
val symmed = apply_rule sym symlist thm
val not_symmed = apply_rule not_sym not_symlist symmed
--- a/src/HOL/Tools/ATP/recon_parse.ML Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML Tue May 03 14:27:21 2005 +0200
@@ -405,10 +405,20 @@
val clause = term
- val line = number ++ justification ++ a (Other "|") ++
+
+
+ (*val line = number ++ justification ++ a (Other "|") ++
a (Other "|") ++ clause ++ a (Other ".")
- >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))
-
+ >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))*)
+
+
+(* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *)
+ val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++
+ a (Other "|") ++ clause ++ a (Other ".")
+ >> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c)))
+
+
+
val lines = many line
val alllines = (lines ++ finished) >> fst
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 03 14:27:21 2005 +0200
@@ -17,6 +17,39 @@
+(*
+fun fill_cls_array array n [] = ()
+| fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
+ in
+ fill_cls_array array (n+1) (xs)
+ end;
+
+
+
+fun memo_add_clauses ((name:string, (cls:Thm.thm list)), symtable)=
+ symtable := Symtab.update((name , cls), !symtable);
+
+
+fun memo_add_all ([], symtable) = ()
+| memo_add_all ((x::xs),symtable) = let val _ = memo_add_clauses (x, symtable)
+ in
+ memo_add_all (xs, symtable)
+ end
+
+fun memo_find_clause (name, (symtable: Thm.thm list Symtab.table ref)) = case Symtab.lookup (!symtable,name) of
+ NONE => []
+ |SOME cls => cls ;
+
+
+fun retrieve_clause array symtable clausenum = let
+ val (name, clnum) = Array.sub(array, clausenum)
+ val clauses = memo_find_clause (name, symtable)
+ val clause = get_nth clnum clauses
+ in
+ (name, clause)
+ end
+ *)
+
(* Versions that include type information *)
fun string_of_thm thm = let val _ = set show_sorts
@@ -146,8 +179,30 @@
fun thmstrings [] str = str
| thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
+fun is_clasimp_ax clasimp_num n = n <=clasimp_num
- fun get_axioms_used proof_steps thms = let
+
+
+fun retrieve_axioms clause_arr [] = []
+| retrieve_axioms clause_arr (x::xs) = [Array.sub(clause_arr, x)]@
+ (retrieve_axioms clause_arr 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
+ in
+ retrieve_axioms clause_arr clasimp_nums
+ end
+
+
+
+
+(* add array and table here, so can retrieve clasimp axioms *)
+
+ fun get_axioms_used proof_steps thms clause_arr num_of_clauses =
+ let
(*val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
val _ = TextIO.output (outfile, thmstring)
@@ -157,9 +212,21 @@
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 clauses = make_clauses thms
+
+ (***********************************************)
+ (* here need to add the clauses from clause_arr*)
+ (***********************************************)
+
+ (* val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums
+ val clasimp_names = map #1 clasimp_names_cls
+ val clasimp_cls = map #2 clasimp_names_cls
+ val outfile = TextIO.openAppend(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 clauses =(*(clasimp_cls)@*)( make_clauses thms)
val vars = map thm_vars clauses
@@ -215,7 +282,7 @@
val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
in
- (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
+ (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
end
fun numclstr (vars, []) str = str
@@ -293,9 +360,12 @@
*)
+
+
+
val dummy_tac = PRIMITIVE(fn thm => thm );
-fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms=
+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")));
(* val sign = sign_of_thm thm
val prems = prems_of thm
@@ -307,7 +377,8 @@
val tokens = #1(lex proofstr)
-
+
+
(***********************************)
(* parse spass proof into datatype *)
(***********************************)
@@ -327,7 +398,9 @@
(* 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 *)
- val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms
+ (* should prob add array and table here, so that we can get axioms*)
+ (* produced from the clasimpset rather than the problem *)
+ val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses
(*val numcls_string = numclstr ( vars, numcls) ""*)
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms")
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 03 14:27:21 2005 +0200
@@ -67,9 +67,10 @@
fun reconstruction_failed fname = error (fname ^ ": reconstruction failed")
-(****************************************)
-(* Reconstruct an axiom resolution step *)
-(****************************************)
+(************************************************)
+(* Reconstruct an axiom resolution step *)
+(* clauses is a list of (clausenum,clause) pairs*)
+(************************************************)
fun follow_axiom clauses allvars (clausenum:int) thml clause_strs =
let val this_axiom = valOf (assoc (clauses,clausenum))
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 03 14:27:21 2005 +0200
@@ -3,247 +3,76 @@
Copyright 2004 University of Cambridge
*)
-(* Get claset rules *)
+signature RES_CLASIMP =
+ sig
+ val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int
+ end;
+
+structure ResClasimp : RES_CLASIMP =
+struct
fun has_name th = not((Thm.name_of_thm th)= "")
fun has_name_pair (a,b) = not_equal a "";
-fun good_pair c (a,b) = not_equal b c;
-
-
-
-val num_of_clauses = ref 0;
-val clause_arr = Array.array(3500, ("empty", 0));
-
-
-(*
-val foo_arr = Array.array(20, ("a",0));
-
-fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)];
-
-
-
-
-fun setupFork () = let
- (** pipes for communication between parent and watcher **)
- 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)
- )
- (***********************************************************)
- (****** fork a watcher process and get it set up and going *)
- (***********************************************************)
- fun startFork () =
- (case Posix.Process.fork() (***************************************)
- of SOME pid => pid (* parent - i.e. main Isabelle process *)
- (***************************************)
-
- (*************************)
- | NONE => let (* child - i.e. watcher *)
- val oldchildin = #infd p1 (*************************)
- val fromParent = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val toParent = Posix.FileSys.wordToFD 0w1
- val fromParentIOD = Posix.FileSys.fdToIOD fromParent
- val fromParentStr = openInFD ("_exec_in_parent", fromParent)
- val toParentStr = openOutFD ("_exec_out_parent", toParent)
- val fooax = fst(Array.sub(foo_arr, 3))
- val outfile = TextIO.openOut("/homes/clq20/Jia_Code/fork");
- val _ = TextIO.output (outfile, ("fooax 3 is: "^fooax))
- val _ = TextIO.closeOut outfile
- in
- (***************************)
- (*** Sort out pipes ********)
- (***************************)
-
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = fromParent};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = toParent};
- Posix.IO.close oldchildout;
-
- (***************************)
- (* start the watcher loop *)
- (***************************)
-
- (****************************************************************************)
- (* fake return value - actually want the watcher to loop until killed *)
- (****************************************************************************)
- Posix.Process.wordToPid 0w0
-
- end)
- val start = startFork()
- 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]);
-
- (*******************************)
- (* return value *)
- (*******************************)
- ()
- end;
-
-
-
-*)
-
-
-
-
-fun multi x 0 xlist = xlist
- |multi x n xlist = multi x (n -1 ) (x::xlist);
-
-
-fun clause_numbering (name:string, cls) = let val num_of_cls = length cls
- val numbers = 0 upto (num_of_cls -1)
- val multi_name = multi name num_of_cls []
- in
- ListPair.zip (multi_name,numbers)
- end;
fun stick [] = []
| stick (x::xs) = x@(stick xs )
-
-
-fun fill_cls_array array n [] = ()
-| fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
- in
- fill_cls_array array (n+1) (xs)
- end;
-
-
-
-val nc = ref (Symtab.empty : (thm list) Symtab.table)
-
-
-
-fun memo_add_clauses (name:string, cls)=
- nc := Symtab.update((name , cls), !nc);
-
-
-
-fun memo_find_clause name = case Symtab.lookup (!nc,name) of
- NONE => []
- |SOME cls => cls ;
-
-
-fun get_simp_metas [] = [[]]
-| get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x
- in
- metas::(get_simp_metas xs)
- end
- handle THM _ => get_simp_metas xs
+(* changed, now it also finds out the name of the theorem. *)
+(* convert a theorem into CNF and then into Clause.clause format. *)
+fun clausify_axiom_pairs thm =
+ let val isa_clauses = ResAxioms.cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
+ val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses
+ val thm_name = Thm.name_of_thm thm
+ 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') :: make_axiom_clauses (i+1) clss clss'
+ in
+ make_axiom_clauses 0 isa_clauses' isa_clauses
+ end;
-(* re-jig all these later as smaller functions for each bit *)
- val num_of_clauses = ref 0;
-val clause_arr = Array.array(3500, ("empty", 0));
-
-
-fun write_out_clasimp filename (clause_arr:(string * int) Array.array) = let
- val _= warning "in writeoutclasimp"
- (****************************************)
- (* add claset rules to array and write out as strings *)
- (****************************************)
- val clausifiable_rules = ResAxioms.claset_rules_of_thy (the_context())
- val name_fol_cs = List.filter has_name clausifiable_rules;
- (* length name_fol_cs is 93 *)
- val good_names = map Thm.name_of_thm name_fol_cs;
-
- (*******************************************)
- (* get (name, thm) pairs for claset rules *)
- (*******************************************)
+fun clausify_rules_pairs [] err_list = ([],err_list)
+ | clausify_rules_pairs (thm::thms) err_list =
+ let val (ts,es) = clausify_rules_pairs thms err_list
+ in
+ ((clausify_axiom_pairs thm)::ts,es) handle _ => (ts,(thm::es))
+ end;
- val names_rules = ListPair.zip (good_names,name_fol_cs);
-
- val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[])
-
- val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
+fun write_out_clasimp filename = let
+ val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
+ val named_claset = List.filter has_name claset_rules;
+ val claset_cls_thms = #1( clausify_rules_pairs named_claset []);
- (* list of lists of tptp string clauses *)
- val stick_clasrls = map stick claset_tptp_strs;
- (* stick stick_clasrls length is 172*)
-
- val name_stick = ListPair.zip (good_names,stick_clasrls);
+ val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
+ val named_simpset = map #2(List.filter has_name_pair simpset_rules);
+ val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []);
- val cl_name_nums =map clause_numbering name_stick;
-
- val cl_long_name_nums = stick cl_name_nums;
- (*******************************************)
- (* create array and put clausename, number pairs into it *)
- (*******************************************)
+ val cls_thms = (claset_cls_thms@simpset_cls_thms);
+ val cls_thms_list = stick cls_thms;
- val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
- val _= num_of_clauses := (List.length cl_long_name_nums);
-
- (*************************************)
- (* write claset out as tptp file *)
- (*************************************)
-
- val claset_all_strs = stick stick_clasrls;
- val out = TextIO.openOut filename;
- val _= ResLib.writeln_strs out claset_all_strs;
- val _= TextIO.flushOut out;
- val _= TextIO.output (out,("\n \n"));
- val _= TextIO.flushOut out;
- (*val _= TextIO.closeOut out;*)
-
- (*********************)
- (* Get simpset rules *)
- (*********************)
+ (*********************************************************)
+ (* 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);
- val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
-
- val named_simps = List.filter has_name_pair simpset_name_rules;
-
- val simp_names = map #1 named_simps;
- val simp_rules = map #2 named_simps;
-
- (* 1137 clausif simps *)
-
- (* need to get names of claset_cluases so we can make sure we've*)
- (* got the same ones (ie. the named ones ) as the claset rules *)
- (* length 1374*)
- val new_simps = #1(ResAxioms.clausify_rules simp_rules []);
- val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
-
- val stick_strs = map stick simpset_tptp_strs;
- val name_stick = ListPair.zip (simp_names,stick_strs);
-
- val name_nums =map clause_numbering name_stick;
- (* length 2409*)
- val long_name_nums = stick name_nums;
+ (*************************************************)
+ (* Write out clauses as tptp strings to filename *)
+ (*************************************************)
+ val clauses = map #1(cls_thms_list);
+ val cls_tptp_strs = map ResClause.tptp_clause clauses;
+ (* list of lists of tptp string clauses *)
+ val stick_clasrls = stick cls_tptp_strs;
+ val out = TextIO.openOut filename;
+ val _= ResLib.writeln_strs out stick_clasrls;
+ val _= TextIO.flushOut out;
+ val _= TextIO.closeOut out
+ in
+ (clause_arr, num_of_clauses)
+ end;
- val _ =fill_cls_array clause_arr (!num_of_clauses + 1) long_name_nums;
- val _ =num_of_clauses := (!num_of_clauses) + (List.length long_name_nums);
-
-
-
- val tptplist = (stick stick_strs)
-
- in
- ResLib.writeln_strs out tptplist;
- TextIO.flushOut out;
- TextIO.closeOut out;
- clause_arr
- end;
-
-(*
-
- Array.sub(clause_arr, 2310);
-*)
+end;
--- a/src/HOL/Tools/ATP/watcher.ML Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Tue May 03 14:27:21 2005 +0200
@@ -92,7 +92,7 @@
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.sysify_path wholefile)])
+ 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"));())
@@ -112,7 +112,8 @@
(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;
@@ -244,7 +245,7 @@
-fun setupWatcher (thm) = let
+fun setupWatcher (thm,clause_arr, num_of_clauses) = let
(** pipes for communication between parent and watcher **)
val p1 = Posix.IO.pipe ()
val p2 = Posix.IO.pipe ()
@@ -275,6 +276,14 @@
val prems = prems_of thm
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
+ (* tracing *)
+ (*val tenth_ax = fst( Array.sub(clause_arr, 1))
+ val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
+ val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
+ val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))
+ val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))
+ val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )
+ *)
(*val goalstr = string_of_thm (the_goal)
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));
val _ = TextIO.output (outfile,goalstr )
@@ -374,7 +383,7 @@
val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
val _ = TextIO.closeOut outfile
val childDone = (case prover of
- (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num) ) )
+ (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (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 *)
@@ -475,7 +484,7 @@
)
else
(
- if ((length procList)<2) (********************)
+ if ((length procList)<10) (********************)
then (* Execute locally *)
( (********************)
let
@@ -587,7 +596,7 @@
(**********************************************************)
fun killWatcher pid= killChild pid;
-fun createWatcher (thm) = let val mychild = childInfo (setupWatcher(thm))
+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
--- a/src/HOL/Tools/ATP/watcher.sig Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.sig Tue May 03 14:27:21 2005 +0200
@@ -36,7 +36,7 @@
(* Start a watcher and set up signal handlers *)
(**********************************************************)
-val createWatcher : Thm.thm -> TextIO.instream * TextIO.outstream * Posix.Process.pid
+val createWatcher : Thm.thm*(ResClause.clause * Thm.thm) Array.array * int -> TextIO.instream * TextIO.outstream * Posix.Process.pid
--- a/src/HOL/Tools/res_atp.ML Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue May 03 14:27:21 2005 +0200
@@ -180,22 +180,28 @@
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,"/homes/clq20/bin/SPASS",
+ [("spass",thmstr,goalstring,spass_home,
"-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof",
clasimpfile, axfile, hypsfile, probfile)]);
(* with paramodulation *)
(*Watcher.callResProvers(childout,
- [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",
+ [("spass",thmstr,goalstring,spass_home,
"-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof",
prob_path)]); *)
(* Watcher.callResProvers(childout,
- [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",
+ [("spass",thmstr,goalstring,spass_home,
"-DocProof", prob_path)]);*)
dummy_tac
end
@@ -282,24 +288,32 @@
(******************************************************************)
(*FIX changed to clasimp_file *)
fun isar_atp' (thms, thm) =
- let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
+ let
+ val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
val _= (warning ("in isar_atp'"))
val prems = prems_of thm
val sign = sign_of_thm thm
val thms_string = Meson.concat_with_and (map string_of_thm thms)
val thmstring = string_of_thm thm
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
- (* set up variables for writing out the clasimps to a tptp file *)
+
+ (* set up variables for writing out the clasimps to a tptp file *)
+ val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp (File.sysify_path clasimp_file)
+ val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )
- val clause_arr = write_out_clasimp (File.sysify_path clasimp_file) clause_arr
- val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )
(* cq: add write out clasimps to file *)
- (* cq:create watcher and pass to isar_atp_aux *)
- (*val tenth_ax = fst( Array.sub(clause_arr, 10))
- val _ = (warning ("tenth axiom in array is: "^tenth_ax))
- val _ = (warning ("num_of_clauses is: "^(string_of_int (!num_of_clauses))) ) *)
-
- val (childin,childout,pid) = Watcher.createWatcher(thm)
+ (* cq:create watcher and pass to isar_atp_aux *)
+ (* tracing *)
+ (*val tenth_ax = fst( Array.sub(clause_arr, 1))
+ val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab)
+ val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
+ val _ = (warning ("tenth axiom in array is: "^tenth_ax))
+ val _ = (warning ("tenth axiom in table is: "^clause_str))
+
+ val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) )
+ *)
+
+ val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
in
case prems of [] => ()