251 (map #1 accepted, map #1 (List.drop (cls, max_new))) |
251 (map #1 accepted, map #1 (List.drop (cls, max_new))) |
252 end |
252 end |
253 end; |
253 end; |
254 |
254 |
255 fun relevant_clauses ctxt convergence follow_defs max_new |
255 fun relevant_clauses ctxt convergence follow_defs max_new |
256 (relevance_override as {add, del, only}) thy ctab p |
256 (relevance_override as {add, del, only}) thy ctab = |
257 rel_consts = |
257 let |
258 let val add_thms = maps (ProofContext.get_fact ctxt) add |
258 val add_thms = maps (ProofContext.get_fact ctxt) add |
259 val del_thms = maps (ProofContext.get_fact ctxt) del |
259 val del_thms = maps (ProofContext.get_fact ctxt) del |
260 fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) |
260 fun iter p rel_consts = |
261 | relevant (newpairs,rejects) [] = |
261 let |
262 let val (newrels,more_rejects) = take_best max_new newpairs |
262 fun relevant ([], _) [] = [] (* Nothing added this iteration *) |
263 val new_consts = maps #2 newrels |
263 | relevant (newpairs,rejects) [] = |
264 val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts |
264 let |
265 val newp = p + (1.0-p) / convergence |
265 val (newrels, more_rejects) = take_best max_new newpairs |
|
266 val new_consts = maps #2 newrels |
|
267 val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts |
|
268 val newp = p + (1.0-p) / convergence |
266 in |
269 in |
267 trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); |
270 trace_msg (fn () => "relevant this iteration: " ^ |
268 map #1 newrels @ |
271 Int.toString (length newrels)); |
269 relevant_clauses ctxt convergence follow_defs max_new |
272 map #1 newrels @ iter newp rel_consts' (more_rejects @ rejects) |
270 relevance_override thy ctab newp rel_consts' |
|
271 (more_rejects @ rejects) |
|
272 end |
273 end |
273 | relevant (newrels, rejects) |
274 | relevant (newrels, rejects) |
274 ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = |
275 ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = |
275 let |
276 let |
276 val weight = if member Thm.eq_thm del_thms thm then 0.0 |
277 val weight = if member Thm.eq_thm del_thms thm then 0.0 |
277 else if member Thm.eq_thm add_thms thm then 1.0 |
278 else if member Thm.eq_thm add_thms thm then 1.0 |
278 else if only then 0.0 |
279 else if only then 0.0 |
279 else clause_weight ctab rel_consts consts_typs |
280 else clause_weight ctab rel_consts consts_typs |
280 in |
281 in |
281 if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts) |
282 if p <= weight orelse |
282 then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ |
283 (follow_defs andalso defines thy (#1 clsthm) rel_consts) then |
283 " passes: " ^ Real.toString weight)); |
284 (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ |
284 relevant ((ax,weight)::newrels, rejects) axs) |
285 " passes: " ^ Real.toString weight); |
285 else relevant (newrels, ax::rejects) axs |
286 relevant ((ax, weight) :: newrels, rejects) axs) |
|
287 else |
|
288 relevant (newrels, ax :: rejects) axs |
286 end |
289 end |
287 in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); |
290 in |
288 relevant ([],[]) |
291 trace_msg (fn () => "relevant_clauses, current pass mark: " ^ |
289 end; |
292 Real.toString p); |
|
293 relevant ([], []) |
|
294 end |
|
295 in iter end |
290 |
296 |
291 fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new |
297 fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new |
292 theory_const relevance_override thy axioms goals = |
298 theory_const relevance_override thy axioms goals = |
293 if relevance_threshold > 0.0 then |
299 if relevance_threshold > 0.0 then |
294 let |
300 let |