Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
authorquigley
Thu Jul 28 16:26:59 2005 +0200 (2005-07-28)
changeset 16950e7f0f41d513a
parent 16949 ea65d75e0ce1
child 16951 6d21767178e6
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Jul 28 15:20:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Jul 28 16:26:59 2005 +0200
     1.3 @@ -107,14 +107,17 @@
     1.4  
     1.5  signature RES_CLASIMP = 
     1.6    sig
     1.7 +
     1.8    val relevant : int ref
     1.9 +  val use_simpset: bool ref
    1.10    val write_out_clasimp : string -> theory -> term -> 
    1.11 -                             (ResClause.clause * thm) Array.array * int
    1.12 +                             (ResClause.clause * thm) Array.array * int * ResClause.clause list
    1.13 +
    1.14    end;
    1.15  
    1.16  structure ResClasimp : RES_CLASIMP =
    1.17  struct
    1.18 -
    1.19 +val use_simpset = ref true;
    1.20  (*Relevance filtering is off by default*)
    1.21  val relevant = ref 0;  
    1.22  
    1.23 @@ -176,6 +179,12 @@
    1.24  	(multi_name)
    1.25      end;
    1.26  
    1.27 +
    1.28 +fun concat_with sep []  = ""
    1.29 +  | concat_with sep [x] = "(" ^ x ^ ")"
    1.30 +  | concat_with sep (x::xs) = "(" ^ x ^ ")" ^  sep ^ (concat_with sep xs);
    1.31 +
    1.32 +
    1.33  (*Write out the claset and simpset rules of the supplied theory.
    1.34    FIXME: argument "goal" is a hack to allow relevance filtering.
    1.35    To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    1.36 @@ -184,6 +193,7 @@
    1.37                ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.38                  (ResAxioms.claset_rules_of_thy thy);
    1.39  	val named_claset = List.filter has_name_pair claset_rules;
    1.40 +
    1.41  	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
    1.42  
    1.43  	val simpset_rules =
    1.44 @@ -191,9 +201,13 @@
    1.45                  (ResAxioms.simpset_rules_of_thy thy);
    1.46  	val named_simpset = 
    1.47  	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
    1.48 +        val justnames = map #1 named_simpset
    1.49 +        val namestring = concat_with "\n" justnames
    1.50 +        val _ = File.append (File.tmp_path (Path.basic "clasimp_names"))
    1.51 +			  (namestring)
    1.52  	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    1.53  
    1.54 -	val cls_thms = (claset_cls_thms@simpset_cls_thms);
    1.55 +	val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) else claset_cls_thms;
    1.56  	val cls_thms_list = List.concat cls_thms;
    1.57          (* length 1429 *)
    1.58  	(*************************************************)
    1.59 @@ -219,9 +233,10 @@
    1.60  	val _= TextIO.flushOut out;
    1.61  	val _= TextIO.closeOut out
    1.62    in
    1.63 -	(clause_arr, num_of_clauses)
    1.64 +	(clause_arr, num_of_clauses, clauses)
    1.65    end;
    1.66  
    1.67 +
    1.68  end;
    1.69  
    1.70