16 val pseudo_abs_name : string |
16 val pseudo_abs_name : string |
17 val pseudo_skolem_prefix : string |
17 val pseudo_skolem_prefix : string |
18 val const_names_in_fact : |
18 val const_names_in_fact : |
19 theory -> (string * typ -> term list -> bool * term list) -> term |
19 theory -> (string * typ -> term list -> bool * term list) -> term |
20 -> string list |
20 -> string list |
21 val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list |
21 val weight_mepo_facts : 'a list -> ('a * real) list |
22 val mepo_suggested_facts : |
22 val mepo_suggested_facts : |
23 Proof.context -> params -> string -> int -> relevance_fudge option |
23 Proof.context -> params -> string -> int -> relevance_fudge option |
24 -> term list -> term -> fact list -> fact list |
24 -> term list -> term -> fact list -> fact list |
25 end; |
25 end; |
26 |
26 |
27 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO = |
27 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO = |
28 struct |
28 struct |
29 |
29 |
30 open ATP_Problem_Generate |
30 open ATP_Problem_Generate |
|
31 open Sledgehammer_Util |
31 open Sledgehammer_Fact |
32 open Sledgehammer_Fact |
32 open Sledgehammer_Provers |
33 open Sledgehammer_Provers |
33 |
34 |
34 val trace = |
35 val trace = |
35 Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false) |
36 Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false) |
507 |> insert_special_facts |
508 |> insert_special_facts |
508 |> tap (fn accepts => trace_msg ctxt (fn () => |
509 |> tap (fn accepts => trace_msg ctxt (fn () => |
509 "Total relevant: " ^ string_of_int (length accepts))) |
510 "Total relevant: " ^ string_of_int (length accepts))) |
510 end |
511 end |
511 |
512 |
512 (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *) |
|
513 (* FUDGE *) |
513 (* FUDGE *) |
514 fun weight_of_mepo_fact rank = |
514 fun weight_of_mepo_fact rank = |
515 Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0 |
515 Math.pow (0.62, log2 (Real.fromInt (rank + 1))) |
516 |
516 |
517 fun weight_mepo_facts facts = |
517 fun weight_mepo_facts facts = |
518 facts ~~ map weight_of_mepo_fact (0 upto length facts - 1) |
518 facts ~~ map weight_of_mepo_fact (0 upto length facts - 1) |
519 |
519 |
520 fun mepo_suggested_facts ctxt |
520 fun mepo_suggested_facts ctxt |