186 defs lhs rhs andalso |
186 defs lhs rhs andalso |
187 (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true) |
187 (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true) |
188 | _ => false |
188 | _ => false |
189 end; |
189 end; |
190 |
190 |
|
191 type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list); |
|
192 |
191 (*For a reverse sort, putting the largest values first.*) |
193 (*For a reverse sort, putting the largest values first.*) |
192 fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1); |
194 fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1); |
193 |
195 |
194 (*Limit the number of new clauses, to prevent runaway acceptance.*) |
196 (*Limit the number of new clauses, to prevent runaway acceptance.*) |
195 fun take_best newpairs = |
197 fun take_best (newpairs : (annotd_cls*real) list) = |
196 let val nnew = length newpairs |
198 let val nnew = length newpairs |
197 in |
199 in |
198 if nnew <= !max_new then (map #1 newpairs, []) |
200 if nnew <= !max_new then (map #1 newpairs, []) |
199 else |
201 else |
200 let val cls = map #1 (sort compare_pairs newpairs) |
202 let val cls = sort compare_pairs newpairs |
201 in Output.debug ("Number of candidates, " ^ Int.toString nnew ^ |
203 val accepted = List.take (cls, !max_new) |
|
204 in if !Output.show_debug_msgs then |
|
205 (Output.debug ("Number of candidates, " ^ Int.toString nnew ^ |
202 ", exceeds the limit of " ^ Int.toString (!max_new)); |
206 ", exceeds the limit of " ^ Int.toString (!max_new)); |
203 (List.take (cls, !max_new), List.drop (cls, !max_new)) |
207 Output.debug ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))); |
|
208 Output.debug ("Actually passed: " ^ |
|
209 space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted))) |
|
210 else (); |
|
211 (map #1 accepted, |
|
212 map #1 (List.drop (cls, !max_new))) |
204 end |
213 end |
205 end; |
214 end; |
206 |
215 |
207 fun relevant_clauses thy ctab p rel_consts = |
216 fun relevant_clauses thy ctab p rel_consts = |
208 let fun relevant ([],rejects) [] = [] (*Nothing added this iteration, so stop*) |
217 let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) |
209 | relevant (newpairs,rejects) [] = |
218 | relevant (newpairs,rejects) [] = |
210 let val (newrels,more_rejeccts) = take_best newpairs |
219 let val (newrels,more_rejects) = take_best newpairs |
211 val new_consts = List.concat (map #2 newrels) |
220 val new_consts = List.concat (map #2 newrels) |
212 val rel_consts' = foldl add_const_typ_table rel_consts new_consts |
221 val rel_consts' = foldl add_const_typ_table rel_consts new_consts |
213 val newp = p + (1.0-p) / !convergence |
222 val newp = p + (1.0-p) / !convergence |
214 in Output.debug ("relevant this iteration: " ^ Int.toString (length newrels)); |
223 in Output.debug ("relevant this iteration: " ^ Int.toString (length newrels)); |
215 (map #1 newrels) @ |
224 (map #1 newrels) @ |
216 (relevant_clauses thy ctab newp rel_consts' (more_rejeccts@rejects)) |
225 (relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects)) |
217 end |
226 end |
218 | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) = |
227 | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) = |
219 let val weight = clause_weight ctab rel_consts consts_typs |
228 let val weight = clause_weight ctab rel_consts consts_typs |
220 in |
229 in |
221 if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts) |
230 if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts) |
222 then (Output.debug name; |
231 then (Output.debug (name ^ " passes: " ^ Real.toString weight); |
223 relevant ((ax,weight)::newrels, rejects) axs) |
232 relevant ((ax,weight)::newrels, rejects) axs) |
224 else relevant (newrels, ax::rejects) axs |
233 else relevant (newrels, ax::rejects) axs |
225 end |
234 end |
226 in Output.debug ("relevant_clauses: " ^ Real.toString p); |
235 in Output.debug ("relevant_clauses, current pass mark = " ^ Real.toString p); |
227 relevant ([],[]) |
236 relevant ([],[]) |
228 end; |
237 end; |
229 |
238 |
230 fun relevance_filter thy axioms goals = |
239 fun relevance_filter thy axioms goals = |
231 if !run_relevance_filter andalso !pass_mark >= 0.1 |
240 if !run_relevance_filter andalso !pass_mark >= 0.1 |
232 then |
241 then |
233 let val _ = Output.debug "Start of relevance filtering"; |
242 let val _ = Output.debug "Start of relevance filtering"; |
234 val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms |
243 val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms |
|
244 val goal_const_tab = get_goal_consts_typs thy goals |
|
245 val _ = if !Output.show_debug_msgs |
|
246 then Output.debug ("Initial constants: " ^ |
|
247 space_implode ", " (Symtab.keys goal_const_tab)) |
|
248 else () |
235 val rels = relevant_clauses thy const_tab (!pass_mark) |
249 val rels = relevant_clauses thy const_tab (!pass_mark) |
236 (get_goal_consts_typs thy goals) |
250 goal_const_tab (map (pair_consts_typs_axiom thy) axioms) |
237 (map (pair_consts_typs_axiom thy) axioms) |
|
238 in |
251 in |
239 Output.debug ("Total relevant: " ^ Int.toString (length rels)); |
252 Output.debug ("Total relevant: " ^ Int.toString (length rels)); |
240 rels |
253 rels |
241 end |
254 end |
242 else axioms; |
255 else axioms; |