author | paulson |
Thu, 27 Apr 2006 12:11:05 +0200 | |
changeset 19480 | 868cf5051ff5 |
parent 19356 | 794802e95d35 |
child 19675 | a4894fb2a5f2 |
permissions | -rw-r--r-- |
16795 | 1 |
(* ID: $Id$ |
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
2 |
Author: Claire Quigley |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
3 |
Copyright 2004 University of Cambridge |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
4 |
*) |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
5 |
|
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
6 |
signature RES_CLASIMP = |
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
7 |
sig |
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
8 |
val blacklist : string list ref (*Theorems forbidden in the output*) |
19317
3d383e78b6f4
Introduction of "whitelist": theorems forced past the relevance filter
paulson
parents:
19209
diff
changeset
|
9 |
val whitelist : thm list ref (*Theorems required in the output*) |
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
10 |
val use_simpset: bool ref |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
11 |
val get_clasimp_atp_lemmas : |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
12 |
Proof.context -> |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
13 |
Term.term list -> |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
14 |
(string * Thm.thm) list -> |
19356
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
15 |
(bool * bool * bool) -> bool -> string Array.array * (thm * (string * int)) list |
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
16 |
end; |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
17 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
18 |
structure ResClasimp : RES_CLASIMP = |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
19 |
struct |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
20 |
val use_simpset = ref false; (*Performance is much better without simprules*) |
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
21 |
|
19317
3d383e78b6f4
Introduction of "whitelist": theorems forced past the relevance filter
paulson
parents:
19209
diff
changeset
|
22 |
(*The rule subsetI is frequently omitted by the relevance filter.*) |
3d383e78b6f4
Introduction of "whitelist": theorems forced past the relevance filter
paulson
parents:
19209
diff
changeset
|
23 |
val whitelist = ref [subsetI]; |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
24 |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
25 |
(*In general, these produce clauses that are prolific (match too many equality or |
18677 | 26 |
membership literals) and relate to seldom-used facts. Some duplicate other rules. |
27 |
FIXME: this blacklist needs to be maintained using theory data and added to using |
|
28 |
an attribute.*) |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
29 |
val blacklist = ref |
19480 | 30 |
["Datatype.prod.size", |
18677 | 31 |
"Divides.dvd_0_left_iff", |
32 |
"Finite_Set.card_0_eq", |
|
33 |
"Finite_Set.card_infinite", |
|
34 |
"Finite_Set.Max_ge", |
|
35 |
"Finite_Set.Max_in", |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
36 |
"Finite_Set.Max_le_iff", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
37 |
"Finite_Set.Max_less_iff", |
18677 | 38 |
"Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*) |
39 |
"Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*) |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
40 |
"Finite_Set.Min_ge_iff", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
41 |
"Finite_Set.Min_gr_iff", |
18677 | 42 |
"Finite_Set.Min_in", |
43 |
"Finite_Set.Min_le", |
|
44 |
"Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", |
|
45 |
"Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", |
|
46 |
"Finite_Set.min.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*) |
|
47 |
"Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*) |
|
48 |
"IntDef.Integ.Abs_Integ_inject", |
|
49 |
"IntDef.Integ.Abs_Integ_inverse", |
|
50 |
"IntDiv.zdvd_0_left", |
|
51 |
"List.append_eq_append_conv", |
|
18985 | 52 |
"List.hd_Cons_tl", (*Says everything is [] or Cons. Probably prolific.*) |
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
53 |
"List.in_listsD", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
54 |
"List.in_listsI", |
18677 | 55 |
"List.lists.Cons", |
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
56 |
"List.listsE", |
18677 | 57 |
"Nat.less_one", (*not directional? obscure*) |
58 |
"Nat.not_gr0", |
|
59 |
"Nat.one_eq_mult_iff", (*duplicate by symmetry*) |
|
60 |
"NatArith.of_nat_0_eq_iff", |
|
61 |
"NatArith.of_nat_eq_0_iff", |
|
62 |
"NatArith.of_nat_le_0_iff", |
|
63 |
"NatSimprocs.divide_le_0_iff_number_of", (*too many clauses*) |
|
64 |
"NatSimprocs.divide_less_0_iff_number_of", |
|
65 |
"NatSimprocs.equation_minus_iff_1", (*not directional*) |
|
66 |
"NatSimprocs.equation_minus_iff_number_of", (*not directional*) |
|
67 |
"NatSimprocs.le_minus_iff_1", (*not directional*) |
|
68 |
"NatSimprocs.le_minus_iff_number_of", (*not directional*) |
|
69 |
"NatSimprocs.less_minus_iff_1", (*not directional*) |
|
70 |
"NatSimprocs.less_minus_iff_number_of", (*not directional*) |
|
71 |
"NatSimprocs.minus_equation_iff_number_of", (*not directional*) |
|
72 |
"NatSimprocs.minus_le_iff_1", (*not directional*) |
|
73 |
"NatSimprocs.minus_le_iff_number_of", (*not directional*) |
|
74 |
"NatSimprocs.minus_less_iff_1", (*not directional*) |
|
75 |
"NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*) |
|
76 |
"NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*) |
|
77 |
"NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*) |
|
78 |
"NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*) |
|
79 |
"NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*) |
|
80 |
"NatSimprocs.zero_less_divide_iff_number_of", |
|
81 |
"OrderedGroup.abs_0_eq", (*duplicate by symmetry*) |
|
82 |
"OrderedGroup.diff_eq_0_iff_eq", (*prolific?*) |
|
83 |
"OrderedGroup.join_0_eq_0", |
|
84 |
"OrderedGroup.meet_0_eq_0", |
|
85 |
"OrderedGroup.pprt_eq_0", (*obscure*) |
|
86 |
"OrderedGroup.pprt_eq_id", (*obscure*) |
|
87 |
"OrderedGroup.pprt_mono", (*obscure*) |
|
88 |
"Parity.even_nat_power", (*obscure, somewhat prolilfic*) |
|
89 |
"Parity.power_eq_0_iff_number_of", |
|
90 |
"Parity.power_le_zero_eq_number_of", (*obscure and prolific*) |
|
91 |
"Parity.power_less_zero_eq_number_of", |
|
92 |
"Parity.zero_le_power_eq_number_of", (*obscure and prolific*) |
|
93 |
"Parity.zero_less_power_eq_number_of", (*obscure and prolific*) |
|
94 |
"Power.zero_less_power_abs_iff", |
|
95 |
"Relation.diagI", |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
96 |
"Relation.ImageI", |
18677 | 97 |
"Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*) |
98 |
"Ring_and_Field.divide_cancel_right", |
|
99 |
"Ring_and_Field.divide_divide_eq_left", |
|
100 |
"Ring_and_Field.divide_divide_eq_right", |
|
101 |
"Ring_and_Field.divide_eq_0_iff", |
|
102 |
"Ring_and_Field.divide_eq_1_iff", |
|
103 |
"Ring_and_Field.divide_eq_eq_1", |
|
104 |
"Ring_and_Field.divide_le_0_1_iff", |
|
105 |
"Ring_and_Field.divide_le_eq_1_neg", (*obscure and prolific*) |
|
106 |
"Ring_and_Field.divide_le_eq_1_pos", (*obscure and prolific*) |
|
107 |
"Ring_and_Field.divide_less_0_1_iff", |
|
108 |
"Ring_and_Field.divide_less_eq_1_neg", (*obscure and prolific*) |
|
109 |
"Ring_and_Field.divide_less_eq_1_pos", (*obscure and prolific*) |
|
110 |
"Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*) |
|
111 |
"Ring_and_Field.field_mult_cancel_left", |
|
112 |
"Ring_and_Field.field_mult_cancel_right", |
|
113 |
"Ring_and_Field.inverse_le_iff_le_neg", |
|
114 |
"Ring_and_Field.inverse_le_iff_le", |
|
115 |
"Ring_and_Field.inverse_less_iff_less_neg", |
|
116 |
"Ring_and_Field.inverse_less_iff_less", |
|
117 |
"Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*) |
|
118 |
"Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*) |
|
119 |
"Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*) |
|
120 |
"Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*) |
|
121 |
"Ring_and_Field.one_eq_divide_iff", (*duplicate by symmetry*) |
|
122 |
"Set.Diff_eq_empty_iff", (*redundant with paramodulation*) |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
123 |
"Set.Diff_insert0", |
18677 | 124 |
"Set.disjoint_insert_1", |
125 |
"Set.disjoint_insert_2", |
|
126 |
"Set.empty_Union_conv", (*redundant with paramodulation*) |
|
127 |
"Set.insert_disjoint_1", |
|
128 |
"Set.insert_disjoint_2", |
|
129 |
"Set.Int_UNIV", (*redundant with paramodulation*) |
|
130 |
"Set.Inter_iff", (*We already have InterI, InterE*) |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
131 |
"Set.Inter_UNIV_conv_1", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
132 |
"Set.Inter_UNIV_conv_2", |
18677 | 133 |
"Set.psubsetE", (*too prolific and obscure*) |
134 |
"Set.psubsetI", |
|
135 |
"Set.singleton_insert_inj_eq'", |
|
136 |
"Set.singleton_insert_inj_eq", |
|
137 |
"Set.singletonD", (*these two duplicate some "insert" lemmas*) |
|
138 |
"Set.singletonI", |
|
139 |
"Set.Un_empty", (*redundant with paramodulation*) |
|
140 |
"Set.Union_empty_conv", (*redundant with paramodulation*) |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
141 |
"Set.Union_iff", (*We already have UnionI, UnionE*) |
18677 | 142 |
"SetInterval.atLeastAtMost_iff", (*obscure and prolific*) |
143 |
"SetInterval.atLeastLessThan_iff", (*obscure and prolific*) |
|
144 |
"SetInterval.greaterThanAtMost_iff", (*obscure and prolific*) |
|
145 |
"SetInterval.greaterThanLessThan_iff", (*obscure and prolific*) |
|
19480 | 146 |
"SetInterval.ivl_subset"]; (*excessive case analysis*) |
147 |
||
18677 | 148 |
(*These might be prolific but are probably OK, and min and max are basic. |
149 |
"Orderings.max_less_iff_conj", |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
150 |
"Orderings.min_less_iff_conj", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
151 |
"Orderings.min_max.below_inf.below_inf_conv", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
152 |
"Orderings.min_max.below_sup.above_sup_conv", |
18677 | 153 |
Very prolific and somewhat obscure: |
154 |
"Set.InterD", |
|
155 |
"Set.UnionI", |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
156 |
*) |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
157 |
|
16956
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
158 |
(*The "name" of a theorem is its statement, if nothing else is available.*) |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
159 |
val plain_string_of_thm = |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
160 |
setmp show_question_marks false |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
161 |
(setmp print_mode [] |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
162 |
(Pretty.setmp_margin 999 string_of_thm)); |
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
163 |
|
17828 | 164 |
(*Returns the first substring enclosed in quotation marks, typically omitting |
165 |
the [.] of meta-level assumptions.*) |
|
166 |
val firstquoted = hd o (String.tokens (fn c => c = #"\"")) |
|
167 |
||
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
168 |
fun fake_thm_name th = |
17828 | 169 |
Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th); |
16061 | 170 |
|
17828 | 171 |
fun put_name_pair ("",th) = (fake_thm_name th, th) |
16956
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
172 |
| put_name_pair (a,th) = (a,th); |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
173 |
|
18677 | 174 |
(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*) |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
175 |
|
18449 | 176 |
exception HASH_CLAUSE and HASH_STRING; |
177 |
||
178 |
(*Catches (for deletion) theorems automatically generated from other theorems*) |
|
179 |
fun insert_suffixed_names ht x = |
|
180 |
(Polyhash.insert ht (x^"_iff1", ()); |
|
181 |
Polyhash.insert ht (x^"_iff2", ()); |
|
182 |
Polyhash.insert ht (x^"_dest", ())); |
|
183 |
||
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
184 |
fun make_banned_test xs = |
18449 | 185 |
let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) |
186 |
(6000, HASH_STRING) |
|
19156 | 187 |
fun banned s = isSome (Polyhash.peek ht s) |
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
188 |
in app (fn x => Polyhash.insert ht (x,())) (!blacklist); |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
189 |
app (insert_suffixed_names ht) (!blacklist @ xs); |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
190 |
banned |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
191 |
end; |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
192 |
|
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
193 |
|
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
194 |
(*** a hash function from Term.term to int, and also a hash table ***) |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
195 |
val xor_words = List.foldl Word.xorb 0w0; |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
196 |
|
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
197 |
fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w) |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
198 |
| hashw_term ((Free(_,_)), w) = w |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
199 |
| hashw_term ((Var(_,_)), w) = w |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
200 |
| hashw_term ((Bound _), w) = w |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
201 |
| hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w) |
19209 | 202 |
| hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w))); |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
203 |
|
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
204 |
fun hashw_pred (P,w) = |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
205 |
let val (p,args) = strip_comb P |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
206 |
in |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
207 |
List.foldl hashw_term w (p::args) |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
208 |
end; |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
209 |
|
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
210 |
fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0)) |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
211 |
| hash_literal P = hashw_pred(P,0w0); |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
212 |
|
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
213 |
|
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
214 |
fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits |
19209 | 215 |
| get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits) |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
216 |
| get_literals lit lits = (lit::lits); |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
217 |
|
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
218 |
|
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
219 |
fun hash_term term = Word.toIntX (xor_words (map hash_literal (get_literals term []))); |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
220 |
|
19356
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
221 |
fun hash_thm thm = hash_term (prop_of thm); |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
222 |
|
19356
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
223 |
fun eq_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2); |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
224 |
(*Create a hash table for clauses, of the given size*) |
18449 | 225 |
fun mk_clause_table n = |
19356
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
226 |
Polyhash.mkTable (hash_thm, eq_thm) |
18449 | 227 |
(n, HASH_CLAUSE); |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
228 |
|
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
229 |
(*Use a hash table to eliminate duplicates from xs*) |
18449 | 230 |
fun make_unique ht xs = |
231 |
(app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht); |
|
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
232 |
|
19356
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
233 |
fun mem_thm thm [] = false |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
234 |
| mem_thm thm ((thm',name)::thms_names) = eq_thm (thm,thm') orelse mem_thm thm thms_names; |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
235 |
|
19356
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
236 |
fun insert_thms [] thms_names = thms_names |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
237 |
| insert_thms ((thm,name)::thms_names) thms_names' = |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
238 |
if mem_thm thm thms_names' then insert_thms thms_names thms_names' |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
239 |
else insert_thms thms_names ((thm,name)::thms_names'); |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
240 |
|
19320
d3688974a063
Only display atpset theorems if Output.show_debug_msgs is true.
mengj
parents:
19317
diff
changeset
|
241 |
fun display_thms [] = () |
d3688974a063
Only display atpset theorems if Output.show_debug_msgs is true.
mengj
parents:
19317
diff
changeset
|
242 |
| display_thms ((name,thm)::nthms) = |
19209 | 243 |
let val nthm = name ^ ": " ^ (string_of_thm thm) |
19320
d3688974a063
Only display atpset theorems if Output.show_debug_msgs is true.
mengj
parents:
19317
diff
changeset
|
244 |
in Output.debug nthm; display_thms nthms end; |
19209 | 245 |
|
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
246 |
(*Write out the claset, simpset and atpset rules of the supplied theory.*) |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
247 |
(* also write supplied user rules, they are not relevance filtered *) |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
248 |
fun get_clasimp_atp_lemmas ctxt goals user_thms (use_claset, use_simpset', use_atpset) run_filter = |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
249 |
let val claset_thms = |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
250 |
if use_claset then |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
251 |
map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt) |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
252 |
else [] |
18449 | 253 |
val simpset_thms = |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
254 |
if (!use_simpset andalso use_simpset') then (* temporary, may merge two use_simpset later *) |
18792 | 255 |
map put_name_pair (ResAxioms.simpset_rules_of_ctxt ctxt) |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
256 |
else [] |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
257 |
val atpset_thms = |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
258 |
if use_atpset then |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
259 |
map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt) |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
260 |
else [] |
19320
d3688974a063
Only display atpset theorems if Output.show_debug_msgs is true.
mengj
parents:
19317
diff
changeset
|
261 |
val _ = if !Output.show_debug_msgs then (Output.debug "ATP theorems: "; display_thms atpset_thms) else () |
19317
3d383e78b6f4
Introduction of "whitelist": theorems forced past the relevance filter
paulson
parents:
19209
diff
changeset
|
262 |
val user_rules = |
3d383e78b6f4
Introduction of "whitelist": theorems forced past the relevance filter
paulson
parents:
19209
diff
changeset
|
263 |
case user_thms of (*use whitelist if there are no user-supplied rules*) |
3d383e78b6f4
Introduction of "whitelist": theorems forced past the relevance filter
paulson
parents:
19209
diff
changeset
|
264 |
[] => map (put_name_pair o ResAxioms.pairname) (!whitelist) |
3d383e78b6f4
Introduction of "whitelist": theorems forced past the relevance filter
paulson
parents:
19209
diff
changeset
|
265 |
| _ => map put_name_pair user_thms |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
266 |
val banned = make_banned_test (map #1 (user_rules@atpset_thms@claset_thms@simpset_thms)) |
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
267 |
fun ok (a,_) = not (banned a) |
19356
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
268 |
val claset_cls_thms = |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
269 |
if run_filter then ResAxioms.cnf_rules_pairs (filter ok claset_thms) |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
270 |
else ResAxioms.cnf_rules_pairs claset_thms |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
271 |
val simpset_cls_thms = |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
272 |
if run_filter then ResAxioms.cnf_rules_pairs (filter ok simpset_thms) |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
273 |
else ResAxioms.cnf_rules_pairs simpset_thms |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
274 |
val atpset_cls_thms = |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
275 |
if run_filter then ResAxioms.cnf_rules_pairs (filter ok atpset_thms) |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
276 |
else ResAxioms.cnf_rules_pairs atpset_thms |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
277 |
val user_cls_thms = ResAxioms.cnf_rules_pairs user_rules (* no filter here, because user supplied rules *) |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
278 |
val cls_thms_list = make_unique (mk_clause_table 2200) |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
279 |
(List.concat (user_cls_thms@atpset_cls_thms@simpset_cls_thms@claset_cls_thms)) |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
280 |
val relevant_cls_thms_list = |
19209 | 281 |
if run_filter |
19356
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
282 |
then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
283 |
else cls_thms_list |
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
284 |
val all_relevant_cls_thms_list = insert_thms (List.concat user_cls_thms) relevant_cls_thms_list (*ensure all user supplied rules are output*) |
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
285 |
in |
19356
794802e95d35
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj
parents:
19320
diff
changeset
|
286 |
(Array.fromList (map fst (map snd all_relevant_cls_thms_list)), all_relevant_cls_thms_list) |
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
287 |
end; |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
288 |
|
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
289 |
|
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
290 |
|
19201
294448903a66
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
mengj
parents:
19156
diff
changeset
|
291 |
end; |