author  blanchet 
Sat, 05 Jun 2010 16:39:23 +0200  
changeset 37347  635425a442e8 
parent 37345  4402a2bfa204 
child 37348  3ad1bfd2de46 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML 
33309  2 
Author: Jia Meng, Cambridge University Computer Laboratory, NICTA 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36227
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
33309  4 
*) 
15452  5 

35826  6 
signature SLEDGEHAMMER_FACT_FILTER = 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

7 
sig 
35865  8 
type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause 
9 
type arity_clause = Sledgehammer_FOL_Clause.arity_clause 

35826  10 
type axiom_name = Sledgehammer_HOL_Clause.axiom_name 
35865  11 
type hol_clause = Sledgehammer_HOL_Clause.hol_clause 
12 
type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id 

36473
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

13 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

14 
type relevance_override = 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

15 
{add: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

16 
del: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

17 
only: bool} 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

18 

37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

19 
val name_thms_pair_from_ref : 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

20 
Proof.context > thm list > Facts.ref > string * thm list 
22989  21 
val tvar_classes_of_terms : term list > string list 
22 
val tfree_classes_of_terms : term list > string list 

23 
val type_consts_of_terms : theory > term list > string list 

37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

24 
val relevant_facts : 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

25 
bool > bool > real > real > bool > int > bool > relevance_override 
36473
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

26 
> Proof.context * (thm list * 'a) > thm list 
35963  27 
> (thm * (string * int)) list 
36473
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

28 
val prepare_clauses : 
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

29 
bool > thm list > thm list > (thm * (axiom_name * hol_clause_id)) list 
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

30 
> (thm * (axiom_name * hol_clause_id)) list > theory 
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

31 
> axiom_name vector 
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

32 
* (hol_clause list * hol_clause list * hol_clause list * 
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

33 
hol_clause list * classrel_clause list * arity_clause list) 
15347  34 
end; 
35 

35826  36 
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = 
15347  37 
struct 
38 

35865  39 
open Sledgehammer_FOL_Clause 
40 
open Sledgehammer_Fact_Preprocessor 

41 
open Sledgehammer_HOL_Clause 

35826  42 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

43 
type relevance_override = 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

44 
{add: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

45 
del: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

46 
only: bool} 
21070  47 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

48 
(***************************************************************) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

49 
(* Relevance Filtering *) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

50 
(***************************************************************) 
19194  51 

35865  52 
fun strip_Trueprop (@{const Trueprop} $ t) = t 
24958  53 
 strip_Trueprop t = t; 
19194  54 

24287  55 
(*A surprising number of theorems contain only a few significant constants. 
56 
These include all induction rules, and other general theorems. Filtering 

57 
theorems in clause form reveals these complexities in the form of Skolem 

58 
functions. If we were instead to filter theorems in their natural form, 

59 
some other method of measuring theorem complexity would become necessary.*) 

60 

61 
fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0); 

62 

63 
(*The default seems best in practice. A constant function of one ignores 

64 
the constant frequencies.*) 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

65 
val weight_fn = log_weight2; 
24287  66 

67 

68 
(*Including equality in this list might be expected to stop rules like subset_antisym from 

69 
being chosen, but for some reason filtering works better with them listed. The 

70 
logical signs All, Ex, &, and > are omitted because any remaining occurrrences 

71 
must be within comprehensions.*) 

35865  72 
val standard_consts = 
73 
[@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, 

74 
@{const_name "=="}, @{const_name "op "}, @{const_name Not}, 

75 
@{const_name "op ="}]; 

24287  76 

77 

78 
(*** constants with types ***) 

79 

80 
(*An abstraction of Isabelle types*) 

81 
datatype const_typ = CTVar  CType of string * const_typ list 

82 

83 
(*Is the second type an instance of the first one?*) 

84 
fun match_type (CType(con1,args1)) (CType(con2,args2)) = 

85 
con1=con2 andalso match_types args1 args2 

86 
 match_type CTVar _ = true 

87 
 match_type _ CTVar = false 

88 
and match_types [] [] = true 

89 
 match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2; 

90 

91 
(*Is there a unifiable constant?*) 

92 
fun uni_mem gctab (c,c_typ) = 

93 
case Symtab.lookup gctab c of 

94 
NONE => false 

95 
 SOME ctyps_list => exists (match_types c_typ) ctyps_list; 

96 

97 
(*Maps a "real" type to a const_typ*) 

98 
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 

99 
 const_typ_of (TFree _) = CTVar 

100 
 const_typ_of (TVar _) = CTVar 

101 

102 
(*Pairs a constant with the list of its type instantiations (using const_typ)*) 

103 
fun const_with_typ thy (c,typ) = 

104 
let val tvars = Sign.const_typargs thy (c,typ) 

105 
in (c, map const_typ_of tvars) end 

106 
handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) 

107 

108 
(*Add a const/type pair to the table, but a [] entry means a standard connective, 

109 
which we ignore.*) 

110 
fun add_const_typ_table ((c,ctyps), tab) = 

111 
Symtab.map_default (c, [ctyps]) (fn [] => []  ctyps_list => insert (op =) ctyps ctyps_list) 

112 
tab; 

113 

114 
(*Free variables are included, as well as constants, to handle locales*) 

115 
fun add_term_consts_typs_rm thy (Const(c, typ), tab) = 

116 
add_const_typ_table (const_with_typ thy (c,typ), tab) 

117 
 add_term_consts_typs_rm thy (Free(c, typ), tab) = 

118 
add_const_typ_table (const_with_typ thy (c,typ), tab) 

119 
 add_term_consts_typs_rm thy (t $ u, tab) = 

120 
add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab)) 

121 
 add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab) 

32994  122 
 add_term_consts_typs_rm _ (_, tab) = tab; 
24287  123 

124 
(*The empty list here indicates that the constant is being ignored*) 

125 
fun add_standard_const (s,tab) = Symtab.update (s,[]) tab; 

126 

127 
val null_const_tab : const_typ list list Symtab.table = 

30190  128 
List.foldl add_standard_const Symtab.empty standard_consts; 
24287  129 

30190  130 
fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab; 
24287  131 

132 
(*Inserts a dummy "constant" referring to the theory name, so that relevance 

133 
takes the given theory into account.*) 

36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

134 
fun const_prop_of theory_relevant th = 
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

135 
if theory_relevant then 
24287  136 
let val name = Context.theory_name (theory_of_thm th) 
137 
val t = Const (name ^ ". 1", HOLogic.boolT) 

138 
in t $ prop_of th end 

139 
else prop_of th; 

140 

141 
(**** Constant / Type Frequencies ****) 

142 

143 
(*A twodimensional symbol table counts frequencies of constants. It's keyed first by 

144 
constant name and second by its list of type instantiations. For the latter, we need 

145 
a linear ordering on type const_typ list.*) 

146 

147 
local 

148 

149 
fun cons_nr CTVar = 0 

150 
 cons_nr (CType _) = 1; 

151 

152 
in 

153 

154 
fun const_typ_ord TU = 

155 
case TU of 

156 
(CType (a, Ts), CType (b, Us)) => 

157 
(case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us)  ord => ord) 

158 
 (T, U) => int_ord (cons_nr T, cons_nr U); 

159 

160 
end; 

161 

31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31910
diff
changeset

162 
structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord); 
24287  163 

36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

164 
fun count_axiom_consts theory_relevant thy ((thm,_), tab) = 
24287  165 
let fun count_const (a, T, tab) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

166 
let val (c, cts) = const_with_typ thy (a,T) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

167 
in (*Twodimensional table update. Constant maps to types maps to count.*) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

168 
Symtab.map_default (c, CTtab.empty) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

169 
(CTtab.map_default (cts,0) (fn n => n+1)) tab 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

170 
end 
24287  171 
fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

172 
 count_term_consts (Free(a,T), tab) = count_const(a,T,tab) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

173 
 count_term_consts (t $ u, tab) = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

174 
count_term_consts (t, count_term_consts (u, tab)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

175 
 count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

176 
 count_term_consts (_, tab) = tab 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

177 
in count_term_consts (const_prop_of theory_relevant thm, tab) end; 
24287  178 

179 

180 
(**** Actual Filtering Code ****) 

181 

182 
(*The frequency of a constant is the sum of those of all instances of its type.*) 

183 
fun const_frequency ctab (c, cts) = 

36185
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

184 
CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m) 
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

185 
(the (Symtab.lookup ctab c)) 0 
24287  186 

187 
(*Add in a constant's weight, as determined by its frequency.*) 

188 
fun add_ct_weight ctab ((c,T), w) = 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

189 
w + weight_fn (real (const_frequency ctab (c,T))); 
24287  190 

191 
(*Relevant constants are weighted according to frequency, 

192 
but irrelevant constants are simply counted. Otherwise, Skolem functions, 

193 
which are rare, would harm a clause's chances of being picked.*) 

194 
fun clause_weight ctab gctyps consts_typs = 

195 
let val rel = filter (uni_mem gctyps) consts_typs 

196 
val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel 

197 
in 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

198 
rel_weight / (rel_weight + real (length consts_typs  length rel)) 
24287  199 
end; 
200 

201 
(*Multiplies out to a list of pairs: 'a * 'b list > ('a * 'b) list > ('a * 'b) list*) 

30190  202 
fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys; 
24287  203 

204 
fun consts_typs_of_term thy t = 

205 
let val tab = add_term_consts_typs_rm thy (t, null_const_tab) 

206 
in Symtab.fold add_expand_pairs tab [] end; 

207 

36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

208 
fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) = 
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

209 
(p, (consts_typs_of_term thy (const_prop_of theory_relevant thm))); 
24287  210 

211 
exception ConstFree; 

212 
fun dest_ConstFree (Const aT) = aT 

213 
 dest_ConstFree (Free aT) = aT 

214 
 dest_ConstFree _ = raise ConstFree; 

215 

216 
(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*) 

32994  217 
fun defines thy thm gctypes = 
24287  218 
let val tm = prop_of thm 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

219 
fun defs lhs rhs = 
24287  220 
let val (rator,args) = strip_comb lhs 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

221 
val ct = const_with_typ thy (dest_ConstFree rator) 
33037
b22e44496dc2
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
haftmann
parents:
32994
diff
changeset

222 
in 
b22e44496dc2
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
haftmann
parents:
32994
diff
changeset

223 
forall is_Var args andalso uni_mem gctypes ct andalso 
33038  224 
subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) 
24287  225 
end 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

226 
handle ConstFree => false 
24287  227 
in 
35963  228 
case tm of 
229 
@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => 

230 
defs lhs rhs 

231 
 _ => false 

24287  232 
end; 
233 

234 
type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list); 

235 

236 
(*For a reverse sort, putting the largest values first.*) 

237 
fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1); 

238 

239 
(*Limit the number of new clauses, to prevent runaway acceptance.*) 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

240 
fun take_best max_new (newpairs : (annotd_cls*real) list) = 
24287  241 
let val nnew = length newpairs 
242 
in 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

243 
if nnew <= max_new then (map #1 newpairs, []) 
24287  244 
else 
245 
let val cls = sort compare_pairs newpairs 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

246 
val accepted = List.take (cls, max_new) 
24287  247 
in 
35865  248 
trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

249 
", exceeds the limit of " ^ Int.toString (max_new))); 
35865  250 
trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); 
251 
trace_msg (fn () => "Actually passed: " ^ 

24287  252 
space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted)); 
253 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

254 
(map #1 accepted, map #1 (List.drop (cls, max_new))) 
24287  255 
end 
256 
end; 

257 

37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

258 
fun cnf_for_facts ctxt = 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

259 
let val thy = ProofContext.theory_of ctxt in 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

260 
maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt) 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

261 
end 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

262 

36922  263 
fun relevant_clauses ctxt relevance_convergence defs_relevant max_new 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

264 
(relevance_override as {add, del, ...}) ctab = 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

265 
let 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

266 
val thy = ProofContext.theory_of ctxt 
37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

267 
val add_thms = cnf_for_facts ctxt add 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

268 
val del_thms = cnf_for_facts ctxt del 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

269 
fun iter threshold rel_consts = 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

270 
let 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

271 
fun relevant ([], _) [] = [] (* Nothing added this iteration *) 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

272 
 relevant (newpairs, rejects) [] = 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

273 
let 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

274 
val (newrels, more_rejects) = take_best max_new newpairs 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

275 
val new_consts = maps #2 newrels 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

276 
val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

277 
val threshold = 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

278 
threshold + (1.0  threshold) / relevance_convergence 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

279 
in 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

280 
trace_msg (fn () => "relevant this iteration: " ^ 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

281 
Int.toString (length newrels)); 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

282 
map #1 newrels @ iter threshold rel_consts' 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

283 
(more_rejects @ rejects) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

284 
end 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

285 
 relevant (newrels, rejects) 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

286 
((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

287 
let 
37345
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

288 
val weight = if member Thm.eq_thm add_thms thm then 1.0 
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

289 
else if member Thm.eq_thm del_thms thm then 0.0 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

290 
else clause_weight ctab rel_consts consts_typs 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

291 
in 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

292 
if weight >= threshold orelse 
36922  293 
(defs_relevant andalso defines thy (#1 clsthm) rel_consts) then 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

294 
(trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

295 
" passes: " ^ Real.toString weight); 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

296 
relevant ((ax, weight) :: newrels, rejects) axs) 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

297 
else 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

298 
relevant (newrels, ax :: rejects) axs 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

299 
end 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

300 
in 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

301 
trace_msg (fn () => "relevant_clauses, current threshold: " ^ 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

302 
Real.toString threshold); 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

303 
relevant ([], []) 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

304 
end 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

305 
in iter end 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

306 

36922  307 
fun relevance_filter ctxt relevance_threshold relevance_convergence 
308 
defs_relevant max_new theory_relevant relevance_override 

309 
thy axioms goals = 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

310 
if relevance_threshold > 0.0 then 
35963  311 
let 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

312 
val const_tab = List.foldl (count_axiom_consts theory_relevant thy) 
35963  313 
Symtab.empty axioms 
24287  314 
val goal_const_tab = get_goal_consts_typs thy goals 
35963  315 
val _ = 
316 
trace_msg (fn () => "Initial constants: " ^ 

317 
commas (Symtab.keys goal_const_tab)) 

318 
val relevant = 

36922  319 
relevant_clauses ctxt relevance_convergence defs_relevant max_new 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

320 
relevance_override const_tab relevance_threshold 
36922  321 
goal_const_tab 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

322 
(map (pair_consts_typs_axiom theory_relevant thy) 
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

323 
axioms) 
35963  324 
in 
325 
trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); 

326 
relevant 

327 
end 

328 
else 

329 
axioms; 

24287  330 

331 
(***************************************************************) 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

332 
(* Retrieving and filtering lemmas *) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

333 
(***************************************************************) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

334 

33022
c95102496490
Removal of the unused atpset concept, the atp attribute and some related code.
paulson
parents:
32994
diff
changeset

335 
(*** retrieve lemmas and filter them ***) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

336 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

337 
(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

338 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

339 
fun setinsert (x,s) = Symtab.update (x,()) s; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

340 

20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

341 
(*Reject theorems with names like "List.filter.filter_list_def" or 
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

342 
"Accessible_Part.acc.defs", as these are definitions arising from packages.*) 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

343 
fun is_package_def a = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30291
diff
changeset

344 
let val names = Long_Name.explode a 
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

345 
in 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

346 
length names > 2 andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

347 
not (hd names = "local") andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

348 
String.isSuffix "_def" a orelse String.isSuffix "_defs" a 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

349 
end; 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

350 

36061  351 
fun mk_clause_table xs = 
352 
fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

353 

36061  354 
fun make_unique xs = 
355 
Termtab.fold (cons o snd) (mk_clause_table xs) [] 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

356 

36061  357 
(* Remove existing axiom clauses from the conjecture clauses, as this can 
358 
dramatically boost an ATP's performance (for some reason). *) 

359 
fun subtract_cls ax_clauses = 

360 
filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of) 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

361 

37345
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

362 
fun all_name_thms_pairs respect_no_atp ctxt chained_ths = 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

363 
let 
26675  364 
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); 
26278  365 
val local_facts = ProofContext.facts_of ctxt; 
33641
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

366 
val full_space = 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

367 
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts); 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

368 

af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

369 
fun valid_facts facts = 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

370 
(facts, []) > Facts.fold_static (fn (name, ths0) => 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

371 
let 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

372 
fun check_thms a = 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

373 
(case try (ProofContext.get_thms ctxt) a of 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

374 
NONE => false 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

375 
 SOME ths1 => Thm.eq_thms (ths0, ths1)); 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

376 

af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

377 
val name1 = Facts.extern facts name; 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

378 
val name2 = Name_Space.extern full_space name; 
37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

379 
val ths = filter_out is_bad_for_atp ths0; 
33641
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

380 
in 
36968
62e29faa3718
make sure chained facts don't pop up in the metis proof
blanchet
parents:
36922
diff
changeset

381 
if Facts.is_concealed facts name orelse 
36227
8987f7a9afef
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
blanchet
parents:
36220
diff
changeset

382 
(respect_no_atp andalso is_package_def name) then 
8987f7a9afef
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
blanchet
parents:
36220
diff
changeset

383 
I 
8987f7a9afef
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
blanchet
parents:
36220
diff
changeset

384 
else case find_first check_thms [name1, name2, name] of 
8987f7a9afef
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
blanchet
parents:
36220
diff
changeset

385 
NONE => I 
37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

386 
 SOME name' => 
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

387 
cons (name' > forall (member Thm.eq_thm chained_ths) ths 
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

388 
? prefix chained_prefix, ths) 
33641
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

389 
end); 
26675  390 
in valid_facts global_facts @ valid_facts local_facts end; 
21224  391 

33309  392 
fun multi_name a th (n, pairs) = 
393 
(n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs); 

21224  394 

33309  395 
fun add_single_names (a, []) pairs = pairs 
396 
 add_single_names (a, [th]) pairs = (a, th) :: pairs 

397 
 add_single_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)); 

21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

398 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

399 
(*Ignore blacklisted basenames*) 
33309  400 
fun add_multi_names (a, ths) pairs = 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36550
diff
changeset

401 
if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs 
33309  402 
else add_single_names (a, ths) pairs; 
21224  403 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

404 
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

405 

36550
f8da913b6c3a
make sure short theorem names are preferred to composite ones in Sledgehammer;
blanchet
parents:
36473
diff
changeset

406 
(* The singlename theorems go after the multiplename ones, so that single 
f8da913b6c3a
make sure short theorem names are preferred to composite ones in Sledgehammer;
blanchet
parents:
36473
diff
changeset

407 
names are preferred when both are available. *) 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

408 
fun name_thm_pairs respect_no_atp ctxt name_thms_pairs = 
33309  409 
let 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

410 
val (mults, singles) = List.partition is_multi name_thms_pairs 
36550
f8da913b6c3a
make sure short theorem names are preferred to composite ones in Sledgehammer;
blanchet
parents:
36473
diff
changeset

411 
val ps = [] > fold add_single_names singles 
f8da913b6c3a
make sure short theorem names are preferred to composite ones in Sledgehammer;
blanchet
parents:
36473
diff
changeset

412 
> fold add_multi_names mults 
36060
4d27652ffb40
reintroduce efficient set structure to collect "no_atp" theorems
blanchet
parents:
36059
diff
changeset

413 
in ps > respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; 
21224  414 

37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

415 
fun is_named ("", th) = 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

416 
(warning ("No name for theorem " ^ 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

417 
Display.string_of_thm_without_context th); false) 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

418 
 is_named _ = true 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

419 
fun checked_name_thm_pairs respect_no_atp ctxt = 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

420 
name_thm_pairs respect_no_atp ctxt 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

421 
#> tap (fn ps => trace_msg 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

422 
(fn () => ("Considering " ^ Int.toString (length ps) ^ 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

423 
" theorems"))) 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

424 
#> filter is_named 
19894  425 

37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

426 
fun name_thms_pair_from_ref ctxt chained_ths xref = 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

427 
let 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

428 
val ths = ProofContext.get_fact ctxt xref 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

429 
val name = Facts.string_of_ref xref 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

430 
> forall (member Thm.eq_thm chained_ths) ths 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

431 
? prefix chained_prefix 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

432 
in (name, ths) end 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

433 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

434 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

435 
(***************************************************************) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

436 
(* Type Classes Present in the Axiom or Conjecture Clauses *) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

437 
(***************************************************************) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

438 

32952  439 
fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts); 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

440 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

441 
(*Remove this trivial type class*) 
35865  442 
fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

443 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

444 
fun tvar_classes_of_terms ts = 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29267
diff
changeset

445 
let val sorts_list = map (map #2 o OldTerm.term_tvars) ts 
30190  446 
in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

447 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

448 
fun tfree_classes_of_terms ts = 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29267
diff
changeset

449 
let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts 
30190  450 
in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

451 

21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

452 
(*fold type constructors*) 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

453 
fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) 
32994  454 
 fold_type_consts _ _ x = x; 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

455 

18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

456 
val add_type_consts_in_type = fold_type_consts setinsert; 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

457 

21397
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

458 
(*Type constructors used to instantiate overloaded constants are the only ones needed.*) 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

459 
fun add_type_consts_in_term thy = 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

460 
let val const_typargs = Sign.const_typargs thy 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

461 
fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x 
32994  462 
 add_tcs (Abs (_, _, u)) x = add_tcs u x 
21397
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

463 
 add_tcs (t $ u) x = add_tcs t (add_tcs u x) 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

464 
 add_tcs _ x = x 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

465 
in add_tcs end 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

466 

21397
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

467 
fun type_consts_of_terms thy ts = 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

468 
Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

469 

18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

470 

19194  471 
(***************************************************************) 
472 
(* ATP invocation methods setup *) 

473 
(***************************************************************) 

474 

20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

475 
(*Ensures that no higherorder theorems "leak out"*) 
24958  476 
fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls 
477 
 restrict_to_logic thy false cls = cls; 

20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

478 

37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

479 
(**** Predicates to detect unwanted clauses (prolific or likely to cause 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

480 
unsoundness) ****) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

481 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

482 
(** Too general means, positive equality literal with a variable X as one operand, 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

483 
when X does not occur properly in the other operand. This rules out clearly 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

484 
inconsistent clauses such as V=aV=b, though it by no means guarantees soundness. **) 
21588  485 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

486 
fun occurs ix = 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

487 
let fun occ(Var (jx,_)) = (ix=jx) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

488 
 occ(t1$t2) = occ t1 orelse occ t2 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

489 
 occ(Abs(_,_,t)) = occ t 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

490 
 occ _ = false 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

491 
in occ end; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

492 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31410
diff
changeset

493 
fun is_recordtype T = not (null (Record.dest_recTs T)); 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

494 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

495 
(*Unwanted equalities include 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

496 
(1) those between a variable that does not properly occur in the second operand, 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

497 
(2) those between a variable and a record, since these seem to be prolific "cases" thms 
21588  498 
*) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

499 
fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

500 
 too_general_eqterms _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

501 

35865  502 
fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) = 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

503 
too_general_eqterms (x,y) orelse too_general_eqterms(y,x) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

504 
 too_general_equality _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

505 

29267  506 
fun has_typed_var tycons = exists_subterm 
507 
(fn Var (_, Type (a, _)) => member (op =) tycons a  _ => false); 

21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

508 

37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

509 
(* Clauses are forbidden to contain variables of these types. The typical reason 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

510 
is that they lead to unsoundness. Note that "unit" satisfies numerous 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

511 
equations like "?x = ()". The resulting clause will have no type constraint, 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

512 
yielding false proofs. Even "bool" leads to many unsound proofs, though only 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

513 
for higherorder problems. *) 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

514 
val dangerous_types = [@{type_name unit}, @{type_name bool}]; 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

515 

37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

516 
(* Clauses containing variables of type "unit" or "bool" or of the form 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

517 
"?x = A  ?x = B  ?x = C" are likely to lead to unsound proofs if types are 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

518 
omitted. *) 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

519 
fun is_dangerous_term _ @{prop True} = true 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

520 
 is_dangerous_term full_types t = 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

521 
not full_types andalso 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

522 
(has_typed_var dangerous_types t orelse 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

523 
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t))) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

524 

37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

525 
fun is_dangerous_theorem full_types add_thms thm = 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

526 
not (member Thm.eq_thm add_thms thm) andalso 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

527 
is_dangerous_term full_types (prop_of thm) 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

528 

635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

529 
fun remove_dangerous_clauses full_types add_thms = 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

530 
filter_out (is_dangerous_theorem full_types add_thms o fst) 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

531 

36473
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

532 
fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of 
30536
07b4f050e4df
split relevancefilter and writing of problemfiles;
immler@in.tum.de
parents:
30364
diff
changeset

533 

37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

534 
fun relevant_facts full_types respect_no_atp relevance_threshold 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

535 
relevance_convergence defs_relevant max_new theory_relevant 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

536 
(relevance_override as {add, del, only}) 
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

537 
(ctxt, (chained_ths, _)) goal_cls = 
36185
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

538 
if (only andalso null add) orelse relevance_threshold > 1.0 then 
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

539 
[] 
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

540 
else 
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

541 
let 
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

542 
val thy = ProofContext.theory_of ctxt 
37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

543 
val add_thms = cnf_for_facts ctxt add 
37345
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

544 
val has_override = not (null add) orelse not (null del) 
36473
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

545 
val is_FO = is_first_order thy goal_cls 
37345
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

546 
val axioms = 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

547 
checked_name_thm_pairs respect_no_atp ctxt 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

548 
(if only then map (name_thms_pair_from_ref ctxt chained_ths) add 
37345
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

549 
else all_name_thms_pairs respect_no_atp ctxt chained_ths) 
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

550 
> cnf_rules_pairs thy 
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

551 
> not has_override ? make_unique 
36185
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

552 
> restrict_to_logic thy is_FO 
37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

553 
> not only ? remove_dangerous_clauses full_types add_thms 
36185
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

554 
in 
36922  555 
relevance_filter ctxt relevance_threshold relevance_convergence 
556 
defs_relevant max_new theory_relevant relevance_override 

37345
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

557 
thy axioms (map prop_of goal_cls) 
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37344
diff
changeset

558 
> has_override ? make_unique 
36185
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

559 
end 
30536
07b4f050e4df
split relevancefilter and writing of problemfiles;
immler@in.tum.de
parents:
30364
diff
changeset

560 

31752
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31749
diff
changeset

561 
(* prepare for passing to writer, 
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31749
diff
changeset

562 
create additional clauses based on the information from extra_cls *) 
37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

563 
fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy = 
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
30536
diff
changeset

564 
let 
36473
8a5c99a1c965
remove "higher_order" option from Sledgehammer  the "smart" default is good enough
blanchet
parents:
36393
diff
changeset

565 
val is_FO = is_first_order thy goal_cls 
36061  566 
val ccls = subtract_cls extra_cls goal_cls 
35865  567 
val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls 
30536
07b4f050e4df
split relevancefilter and writing of problemfiles;
immler@in.tum.de
parents:
30364
diff
changeset

568 
val ccltms = map prop_of ccls 
31752
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31749
diff
changeset

569 
and axtms = map (prop_of o #1) extra_cls 
30536
07b4f050e4df
split relevancefilter and writing of problemfiles;
immler@in.tum.de
parents:
30364
diff
changeset

570 
val subs = tfree_classes_of_terms ccltms 
07b4f050e4df
split relevancefilter and writing of problemfiles;
immler@in.tum.de
parents:
30364
diff
changeset

571 
and supers = tvar_classes_of_terms axtms 
35865  572 
and tycons = type_consts_of_terms thy (ccltms @ axtms) 
30536
07b4f050e4df
split relevancefilter and writing of problemfiles;
immler@in.tum.de
parents:
30364
diff
changeset

573 
(*TFrees in conjecture clauses; TVars in axiom clauses*) 
35865  574 
val conjectures = make_conjecture_clauses dfg thy ccls 
575 
val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls) 

576 
val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls) 

577 
val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, []) 

578 
val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers 

579 
val classrel_clauses = make_classrel_clauses thy subs supers' 

30536
07b4f050e4df
split relevancefilter and writing of problemfiles;
immler@in.tum.de
parents:
30364
diff
changeset

580 
in 
31752
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31749
diff
changeset

581 
(Vector.fromList clnames, 
31865
5e97c4abd18e
fixed: count constants with supplementary lemmas
immler@in.tum.de
parents:
31837
diff
changeset

582 
(conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses)) 
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
30536
diff
changeset

583 
end 
15644  584 

15347  585 
end; 