41 slice : bool, |
41 slice : bool, |
42 minimize : bool option, |
42 minimize : bool option, |
43 timeout : Time.time option, |
43 timeout : Time.time option, |
44 preplay_timeout : Time.time option, |
44 preplay_timeout : Time.time option, |
45 expect : string} |
45 expect : string} |
46 |
|
47 type relevance_fudge = |
|
48 {local_const_multiplier : real, |
|
49 worse_irrel_freq : real, |
|
50 higher_order_irrel_weight : real, |
|
51 abs_rel_weight : real, |
|
52 abs_irrel_weight : real, |
|
53 theory_const_rel_weight : real, |
|
54 theory_const_irrel_weight : real, |
|
55 chained_const_irrel_weight : real, |
|
56 intro_bonus : real, |
|
57 elim_bonus : real, |
|
58 simp_bonus : real, |
|
59 local_bonus : real, |
|
60 assum_bonus : real, |
|
61 chained_bonus : real, |
|
62 max_imperfect : real, |
|
63 max_imperfect_exp : real, |
|
64 threshold_divisor : real, |
|
65 ridiculous_threshold : real} |
|
66 |
46 |
67 type prover_problem = |
47 type prover_problem = |
68 {state : Proof.state, |
48 {state : Proof.state, |
69 goal : thm, |
49 goal : thm, |
70 subgoal : int, |
50 subgoal : int, |
117 val remotify_prover_if_not_installed : |
97 val remotify_prover_if_not_installed : |
118 Proof.context -> string -> string option |
98 Proof.context -> string -> string option |
119 val default_max_facts_of_prover : Proof.context -> bool -> string -> int |
99 val default_max_facts_of_prover : Proof.context -> bool -> string -> int |
120 val is_unit_equality : term -> bool |
100 val is_unit_equality : term -> bool |
121 val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool |
101 val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool |
122 val atp_relevance_fudge : relevance_fudge |
|
123 val smt_relevance_fudge : relevance_fudge |
|
124 val relevance_fudge_of_prover : Proof.context -> string -> relevance_fudge |
|
125 val weight_smt_fact : |
102 val weight_smt_fact : |
126 Proof.context -> int -> ((string * stature) * thm) * int |
103 Proof.context -> int -> ((string * stature) * thm) * int |
127 -> (string * stature) * (int option * thm) |
104 -> (string * stature) * (int option * thm) |
128 val supported_provers : Proof.context -> unit |
105 val supported_provers : Proof.context -> unit |
129 val kill_provers : unit -> unit |
106 val kill_provers : unit -> unit |
260 is_good_unit_equality T t u |
237 is_good_unit_equality T t u |
261 | is_unit_equality _ = false |
238 | is_unit_equality _ = false |
262 |
239 |
263 fun is_appropriate_prop_of_prover ctxt name = |
240 fun is_appropriate_prop_of_prover ctxt name = |
264 if is_unit_equational_atp ctxt name then is_unit_equality else K true |
241 if is_unit_equational_atp ctxt name then is_unit_equality else K true |
265 |
|
266 (* FUDGE *) |
|
267 val atp_relevance_fudge = |
|
268 {local_const_multiplier = 1.5, |
|
269 worse_irrel_freq = 100.0, |
|
270 higher_order_irrel_weight = 1.05, |
|
271 abs_rel_weight = 0.5, |
|
272 abs_irrel_weight = 2.0, |
|
273 theory_const_rel_weight = 0.5, |
|
274 theory_const_irrel_weight = 0.25, |
|
275 chained_const_irrel_weight = 0.25, |
|
276 intro_bonus = 0.15, |
|
277 elim_bonus = 0.15, |
|
278 simp_bonus = 0.15, |
|
279 local_bonus = 0.55, |
|
280 assum_bonus = 1.05, |
|
281 chained_bonus = 1.5, |
|
282 max_imperfect = 11.5, |
|
283 max_imperfect_exp = 1.0, |
|
284 threshold_divisor = 2.0, |
|
285 ridiculous_threshold = 0.1} |
|
286 |
|
287 (* FUDGE (FIXME) *) |
|
288 val smt_relevance_fudge = |
|
289 {local_const_multiplier = #local_const_multiplier atp_relevance_fudge, |
|
290 worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge, |
|
291 higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge, |
|
292 abs_rel_weight = #abs_rel_weight atp_relevance_fudge, |
|
293 abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge, |
|
294 theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge, |
|
295 theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge, |
|
296 chained_const_irrel_weight = #chained_const_irrel_weight atp_relevance_fudge, |
|
297 intro_bonus = #intro_bonus atp_relevance_fudge, |
|
298 elim_bonus = #elim_bonus atp_relevance_fudge, |
|
299 simp_bonus = #simp_bonus atp_relevance_fudge, |
|
300 local_bonus = #local_bonus atp_relevance_fudge, |
|
301 assum_bonus = #assum_bonus atp_relevance_fudge, |
|
302 chained_bonus = #chained_bonus atp_relevance_fudge, |
|
303 max_imperfect = #max_imperfect atp_relevance_fudge, |
|
304 max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge, |
|
305 threshold_divisor = #threshold_divisor atp_relevance_fudge, |
|
306 ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} |
|
307 |
|
308 fun relevance_fudge_of_prover ctxt name = |
|
309 if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge |
|
310 |
242 |
311 fun supported_provers ctxt = |
243 fun supported_provers ctxt = |
312 let |
244 let |
313 val thy = Proof_Context.theory_of ctxt |
245 val thy = Proof_Context.theory_of ctxt |
314 val (remote_provers, local_provers) = |
246 val (remote_provers, local_provers) = |
351 slice : bool, |
283 slice : bool, |
352 minimize : bool option, |
284 minimize : bool option, |
353 timeout : Time.time option, |
285 timeout : Time.time option, |
354 preplay_timeout : Time.time option, |
286 preplay_timeout : Time.time option, |
355 expect : string} |
287 expect : string} |
356 |
|
357 type relevance_fudge = |
|
358 {local_const_multiplier : real, |
|
359 worse_irrel_freq : real, |
|
360 higher_order_irrel_weight : real, |
|
361 abs_rel_weight : real, |
|
362 abs_irrel_weight : real, |
|
363 theory_const_rel_weight : real, |
|
364 theory_const_irrel_weight : real, |
|
365 chained_const_irrel_weight : real, |
|
366 intro_bonus : real, |
|
367 elim_bonus : real, |
|
368 simp_bonus : real, |
|
369 local_bonus : real, |
|
370 assum_bonus : real, |
|
371 chained_bonus : real, |
|
372 max_imperfect : real, |
|
373 max_imperfect_exp : real, |
|
374 threshold_divisor : real, |
|
375 ridiculous_threshold : real} |
|
376 |
288 |
377 type prover_problem = |
289 type prover_problem = |
378 {state : Proof.state, |
290 {state : Proof.state, |
379 goal : thm, |
291 goal : thm, |
380 subgoal : int, |
292 subgoal : int, |