author | paulson |
Tue, 28 Feb 2006 11:10:51 +0100 | |
changeset 19156 | bdaa8a980431 |
parent 19010 | fef9e4881e83 |
child 19201 | 294448903a66 |
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*) |
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
9 |
val use_simpset: bool ref |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
10 |
val get_clasimp_lemmas : |
18753
aa82bd41555d
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
paulson
parents:
18677
diff
changeset
|
11 |
Proof.context -> term list -> |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
12 |
(ResClause.clause * thm) Array.array * ResClause.clause list |
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
13 |
end; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
14 |
|
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
15 |
structure ResClasimp : RES_CLASIMP = |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
16 |
struct |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
17 |
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
|
18 |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
19 |
(*In general, these produce clauses that are prolific (match too many equality or |
18677 | 20 |
membership literals) and relate to seldom-used facts. Some duplicate other rules. |
21 |
FIXME: this blacklist needs to be maintained using theory data and added to using |
|
22 |
an attribute.*) |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
23 |
val blacklist = ref |
18985 | 24 |
["Datatype.not_None_eq", (*Says everything is None or Some. Probably prolific.*) |
25 |
"Datatype.not_Some_eq_D", (*Says everything is None or Some. Probably prolific.*) |
|
26 |
"Datatype.not_Some_eq", (*Says everything is None or Some. Probably prolific.*) |
|
18677 | 27 |
"Datatype.option.size_1", |
28 |
"Datatype.option.size_2", |
|
29 |
"Datatype.prod.size", |
|
30 |
"Datatype.sum.size_1", |
|
31 |
"Datatype.sum.size_2", |
|
32 |
"Datatype.unit.size", |
|
33 |
"Divides.dvd_0_left_iff", |
|
34 |
"Finite_Set.card_0_eq", |
|
35 |
"Finite_Set.card_infinite", |
|
36 |
"Finite_Set.Max_ge", |
|
37 |
"Finite_Set.Max_in", |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
38 |
"Finite_Set.Max_le_iff", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
39 |
"Finite_Set.Max_less_iff", |
18677 | 40 |
"Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*) |
41 |
"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
|
42 |
"Finite_Set.Min_ge_iff", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
43 |
"Finite_Set.Min_gr_iff", |
18677 | 44 |
"Finite_Set.Min_in", |
45 |
"Finite_Set.Min_le", |
|
46 |
"Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", |
|
47 |
"Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", |
|
48 |
"Finite_Set.min.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*) |
|
49 |
"Finite_Set.min.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
|
50 |
"Infinite_Set.atmost_one_unique", |
18677 | 51 |
"IntArith.zabs_less_one_iff", |
52 |
"IntDef.Integ.Abs_Integ_inject", |
|
53 |
"IntDef.Integ.Abs_Integ_inverse", |
|
54 |
"IntDiv.zdvd_0_left", |
|
55 |
"IntDiv.zero_less_zpower_abs_iff", |
|
56 |
"List.append_eq_append_conv", |
|
57 |
"List.Cons_in_lex", |
|
18985 | 58 |
"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
|
59 |
"List.in_listsD", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
60 |
"List.in_listsI", |
18677 | 61 |
"List.lists.Cons", |
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
62 |
"List.listsE", |
18677 | 63 |
"List.take_eq_Nil", |
64 |
"Nat.less_one", |
|
65 |
"Nat.less_one", (*not directional? obscure*) |
|
66 |
"Nat.not_gr0", |
|
67 |
"Nat.one_eq_mult_iff", (*duplicate by symmetry*) |
|
68 |
"NatArith.of_nat_0_eq_iff", |
|
69 |
"NatArith.of_nat_eq_0_iff", |
|
70 |
"NatArith.of_nat_le_0_iff", |
|
71 |
"NatSimprocs.divide_le_0_iff_number_of", (*seldom used; often prolific*) |
|
72 |
"NatSimprocs.divide_le_0_iff_number_of", (*too many clauses*) |
|
73 |
"NatSimprocs.divide_less_0_iff_number_of", |
|
74 |
"NatSimprocs.divide_less_0_iff_number_of", (*too many clauses*) |
|
75 |
"NatSimprocs.equation_minus_iff_1", (*not directional*) |
|
76 |
"NatSimprocs.equation_minus_iff_number_of", (*not directional*) |
|
77 |
"NatSimprocs.le_minus_iff_1", (*not directional*) |
|
78 |
"NatSimprocs.le_minus_iff_number_of", (*not directional*) |
|
79 |
"NatSimprocs.less_minus_iff_1", (*not directional*) |
|
80 |
"NatSimprocs.less_minus_iff_number_of", (*not directional*) |
|
81 |
"NatSimprocs.minus_equation_iff_number_of", (*not directional*) |
|
82 |
"NatSimprocs.minus_le_iff_1", (*not directional*) |
|
83 |
"NatSimprocs.minus_le_iff_number_of", (*not directional*) |
|
84 |
"NatSimprocs.minus_less_iff_1", (*not directional*) |
|
85 |
"NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*) |
|
86 |
"NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*) |
|
87 |
"NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*) |
|
88 |
"NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*) |
|
89 |
"NatSimprocs.zero_le_divide_iff_number_of", |
|
90 |
"NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*) |
|
91 |
"NatSimprocs.zero_less_divide_iff_number_of", |
|
92 |
"NatSimprocs.zero_less_divide_iff_number_of", (*excessive case analysis*) |
|
93 |
"OrderedGroup.abs_0_eq", |
|
94 |
"OrderedGroup.abs_0_eq", (*duplicate by symmetry*) |
|
95 |
"OrderedGroup.diff_eq_0_iff_eq", (*prolific?*) |
|
96 |
"OrderedGroup.join_0_eq_0", |
|
97 |
"OrderedGroup.meet_0_eq_0", |
|
98 |
"OrderedGroup.pprt_eq_0", (*obscure*) |
|
99 |
"OrderedGroup.pprt_eq_id", (*obscure*) |
|
100 |
"OrderedGroup.pprt_mono", (*obscure*) |
|
101 |
"Parity.even_nat_power", (*obscure, somewhat prolilfic*) |
|
102 |
"Parity.power_eq_0_iff_number_of", |
|
103 |
"Parity.power_eq_0_iff_number_of", |
|
104 |
"Parity.power_le_zero_eq_number_of", |
|
105 |
"Parity.power_le_zero_eq_number_of", (*obscure and prolific*) |
|
106 |
"Parity.power_less_zero_eq_number_of", |
|
107 |
"Parity.zero_le_power_eq_number_of", (*obscure and prolific*) |
|
108 |
"Parity.zero_less_power_eq_number_of", (*obscure and prolific*) |
|
109 |
"Power.zero_less_power_abs_iff", |
|
110 |
"Relation.diagI", |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
111 |
"Relation.ImageI", |
18677 | 112 |
"Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*) |
113 |
"Ring_and_Field.divide_cancel_right", |
|
114 |
"Ring_and_Field.divide_divide_eq_left", |
|
115 |
"Ring_and_Field.divide_divide_eq_right", |
|
116 |
"Ring_and_Field.divide_eq_0_iff", |
|
117 |
"Ring_and_Field.divide_eq_1_iff", |
|
118 |
"Ring_and_Field.divide_eq_eq_1", |
|
119 |
"Ring_and_Field.divide_le_0_1_iff", |
|
120 |
"Ring_and_Field.divide_le_eq_1_neg", |
|
121 |
"Ring_and_Field.divide_le_eq_1_neg", (*obscure and prolific*) |
|
122 |
"Ring_and_Field.divide_le_eq_1_pos", |
|
123 |
"Ring_and_Field.divide_le_eq_1_pos", (*obscure and prolific*) |
|
124 |
"Ring_and_Field.divide_less_0_1_iff", |
|
125 |
"Ring_and_Field.divide_less_eq_1_neg", (*obscure and prolific*) |
|
126 |
"Ring_and_Field.divide_less_eq_1_pos", |
|
127 |
"Ring_and_Field.divide_less_eq_1_pos", (*obscure and prolific*) |
|
128 |
"Ring_and_Field.eq_divide_eq_1", |
|
129 |
"Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*) |
|
130 |
"Ring_and_Field.field_mult_cancel_left", |
|
131 |
"Ring_and_Field.field_mult_cancel_right", |
|
132 |
"Ring_and_Field.inverse_le_iff_le_neg", |
|
133 |
"Ring_and_Field.inverse_le_iff_le", |
|
134 |
"Ring_and_Field.inverse_less_iff_less_neg", |
|
135 |
"Ring_and_Field.inverse_less_iff_less", |
|
136 |
"Ring_and_Field.le_divide_eq_1_neg", |
|
137 |
"Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*) |
|
138 |
"Ring_and_Field.le_divide_eq_1_pos", |
|
139 |
"Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*) |
|
140 |
"Ring_and_Field.less_divide_eq_1_neg", |
|
141 |
"Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*) |
|
142 |
"Ring_and_Field.less_divide_eq_1_pos", |
|
143 |
"Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*) |
|
144 |
"Ring_and_Field.one_eq_divide_iff", (*duplicate by symmetry*) |
|
145 |
"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
|
146 |
"Set.Diff_insert0", |
18677 | 147 |
"Set.disjoint_insert_1", |
148 |
"Set.disjoint_insert_2", |
|
149 |
"Set.empty_Union_conv", (*redundant with paramodulation*) |
|
150 |
"Set.insert_disjoint_1", |
|
151 |
"Set.insert_disjoint_2", |
|
152 |
"Set.Int_UNIV", (*redundant with paramodulation*) |
|
153 |
"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
|
154 |
"Set.Inter_UNIV_conv_1", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
155 |
"Set.Inter_UNIV_conv_2", |
18677 | 156 |
"Set.psubsetE", (*too prolific and obscure*) |
157 |
"Set.psubsetI", |
|
158 |
"Set.singleton_insert_inj_eq'", |
|
159 |
"Set.singleton_insert_inj_eq", |
|
160 |
"Set.singletonD", (*these two duplicate some "insert" lemmas*) |
|
161 |
"Set.singletonI", |
|
162 |
"Set.Un_empty", (*redundant with paramodulation*) |
|
163 |
"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
|
164 |
"Set.Union_iff", (*We already have UnionI, UnionE*) |
18677 | 165 |
"SetInterval.atLeastAtMost_iff", (*obscure and prolific*) |
166 |
"SetInterval.atLeastLessThan_iff", (*obscure and prolific*) |
|
167 |
"SetInterval.greaterThanAtMost_iff", (*obscure and prolific*) |
|
168 |
"SetInterval.greaterThanLessThan_iff", (*obscure and prolific*) |
|
169 |
"SetInterval.ivl_subset", (*excessive case analysis*) |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
170 |
"Sum_Type.InlI", |
18677 | 171 |
"Sum_Type.InrI"]; |
172 |
||
173 |
(*These might be prolific but are probably OK, and min and max are basic. |
|
174 |
"Orderings.max_less_iff_conj", |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
175 |
"Orderings.min_less_iff_conj", |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
176 |
"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
|
177 |
"Orderings.min_max.below_sup.above_sup_conv", |
18677 | 178 |
Very prolific and somewhat obscure: |
179 |
"Set.InterD", |
|
180 |
"Set.UnionI", |
|
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
181 |
*) |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
182 |
|
16956
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
183 |
(*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
|
184 |
val plain_string_of_thm = |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
185 |
setmp show_question_marks false |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
186 |
(setmp print_mode [] |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
187 |
(Pretty.setmp_margin 999 string_of_thm)); |
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
188 |
|
17828 | 189 |
(*Returns the first substring enclosed in quotation marks, typically omitting |
190 |
the [.] of meta-level assumptions.*) |
|
191 |
val firstquoted = hd o (String.tokens (fn c => c = #"\"")) |
|
192 |
||
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
193 |
fun fake_thm_name th = |
17828 | 194 |
Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th); |
16061 | 195 |
|
17828 | 196 |
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
|
197 |
| 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
|
198 |
|
18677 | 199 |
(*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
|
200 |
|
18449 | 201 |
exception HASH_CLAUSE and HASH_STRING; |
202 |
||
203 |
(*Catches (for deletion) theorems automatically generated from other theorems*) |
|
204 |
fun insert_suffixed_names ht x = |
|
205 |
(Polyhash.insert ht (x^"_iff1", ()); |
|
206 |
Polyhash.insert ht (x^"_iff2", ()); |
|
207 |
Polyhash.insert ht (x^"_dest", ())); |
|
208 |
||
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
209 |
fun make_banned_test xs = |
18449 | 210 |
let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) |
211 |
(6000, HASH_STRING) |
|
19156 | 212 |
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
|
213 |
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
|
214 |
app (insert_suffixed_names ht) (!blacklist @ xs); |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
215 |
banned |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
216 |
end; |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
217 |
|
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
218 |
(*Create a hash table for clauses, of the given size*) |
18449 | 219 |
fun mk_clause_table n = |
220 |
Polyhash.mkTable (ResClause.hash_clause, ResClause.clause_eq) |
|
221 |
(n, HASH_CLAUSE); |
|
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
222 |
|
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
223 |
(*Use a hash table to eliminate duplicates from xs*) |
18449 | 224 |
fun make_unique ht xs = |
225 |
(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
|
226 |
|
19156 | 227 |
(*Write out the claset and simpset rules of the supplied theory.*) |
18753
aa82bd41555d
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
paulson
parents:
18677
diff
changeset
|
228 |
fun get_clasimp_lemmas ctxt goals = |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
229 |
let val claset_thms = |
18792 | 230 |
map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt) |
18449 | 231 |
val simpset_thms = |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
232 |
if !use_simpset then |
18792 | 233 |
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
|
234 |
else [] |
18509
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
235 |
val banned = make_banned_test (map #1 (claset_thms@simpset_thms)) |
d2d96f12a1fc
blacklist of prolific theorems (must be replaced by an attribute later
paulson
parents:
18449
diff
changeset
|
236 |
fun ok (a,_) = not (banned a) |
18449 | 237 |
val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms) |
238 |
val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms) |
|
18797 | 239 |
val cls_thms_list = make_unique (mk_clause_table 2200) |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
240 |
(List.concat (simpset_cls_thms@claset_cls_thms)) |
19156 | 241 |
val relevant_cls_thms_list = |
242 |
ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals |
|
17828 | 243 |
in (* create array of put clausename, number pairs into it *) |
18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18797
diff
changeset
|
244 |
(Array.fromList relevant_cls_thms_list, map #1 (relevant_cls_thms_list)) |
16061 | 245 |
end; |
15643 | 246 |
|
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
247 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
248 |
end; |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
249 |
|
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
250 |
|
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
251 |