# HG changeset patch # User quigley # Date 1122560819 -7200 # Node ID e7f0f41d513afefb251f2dba1d1e2c9923440eff # Parent ea65d75e0ce1e7d6a278f46c7e4264a89e028cb2 Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files diff -r ea65d75e0ce1 -r e7f0f41d513a src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu Jul 28 15:20:06 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Thu Jul 28 16:26:59 2005 +0200 @@ -107,14 +107,17 @@ signature RES_CLASIMP = sig + val relevant : int ref + val use_simpset: bool ref val write_out_clasimp : string -> theory -> term -> - (ResClause.clause * thm) Array.array * int + (ResClause.clause * thm) Array.array * int * ResClause.clause list + end; structure ResClasimp : RES_CLASIMP = struct - +val use_simpset = ref true; (*Relevance filtering is off by default*) val relevant = ref 0; @@ -176,6 +179,12 @@ (multi_name) end; + +fun concat_with sep [] = "" + | concat_with sep [x] = "(" ^ x ^ ")" + | concat_with sep (x::xs) = "(" ^ x ^ ")" ^ sep ^ (concat_with sep xs); + + (*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*) @@ -184,6 +193,7 @@ ReduceAxiomsN.relevant_filter (!relevant) goal (ResAxioms.claset_rules_of_thy thy); val named_claset = List.filter has_name_pair claset_rules; + val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []); val simpset_rules = @@ -191,9 +201,13 @@ (ResAxioms.simpset_rules_of_thy thy); val named_simpset = map remove_spaces_pair (List.filter has_name_pair simpset_rules) + val justnames = map #1 named_simpset + val namestring = concat_with "\n" justnames + val _ = File.append (File.tmp_path (Path.basic "clasimp_names")) + (namestring) val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []); - val cls_thms = (claset_cls_thms@simpset_cls_thms); + val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) else claset_cls_thms; val cls_thms_list = List.concat cls_thms; (* length 1429 *) (*************************************************) @@ -219,9 +233,10 @@ val _= TextIO.flushOut out; val _= TextIO.closeOut out in - (clause_arr, num_of_clauses) + (clause_arr, num_of_clauses, clauses) end; + end;