--- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu Jun 09 23:33:28 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Fri Jun 10 16:15:36 2005 +0200
@@ -8,6 +8,7 @@
signature RES_CLASIMP =
sig
val write_out_clasimp :string -> theory -> (ResClause.clause * thm) Array.array * int
+val write_out_clasimp_small :string -> theory -> (ResClause.clause * thm) Array.array * int
end;
structure ResClasimp : RES_CLASIMP =
@@ -112,6 +113,53 @@
(clause_arr, num_of_clauses)
end;
+
+
+
+
+(*Write out the claset and simpset rules of the supplied theory. Only include the first 50 rules*)
+fun write_out_clasimp_small filename thy =
+ let val claset_rules = ResAxioms.claset_rules_of_thy thy;
+ val named_claset = List.filter has_name_pair claset_rules;
+ val claset_names = map remove_spaces_pair (named_claset)
+ val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
+
+ val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
+ val named_simpset =
+ map remove_spaces_pair (List.filter has_name_pair simpset_rules)
+ val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
+
+ val cls_thms = (claset_cls_thms@simpset_cls_thms);
+ val cls_thms_list = List.concat cls_thms;
+ (* 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);
+ val mini_list = List.take ( whole_list,50)
+ (*********************************************************)
+ (* create array and put clausename, number pairs into it *)
+ (*********************************************************)
+ val num_of_clauses = 0;
+ val clause_arr = Array.fromList mini_list;
+ val num_of_clauses = List.length mini_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 (List.take (stick_clasrls,50));
+ val _= TextIO.flushOut out;
+ val _= TextIO.closeOut out
+ in
+ (clause_arr, num_of_clauses)
+ end;
+
+
+
end;