115 val factsN : string |
115 val factsN : string |
116 val generate_atp_problem : Proof.context -> bool -> atp_format -> atp_formula_role -> type_enc -> |
116 val generate_atp_problem : Proof.context -> bool -> atp_format -> atp_formula_role -> type_enc -> |
117 mode -> string -> bool -> bool -> bool -> term list -> term -> |
117 mode -> string -> bool -> bool -> bool -> term list -> term -> |
118 ((string * stature) * term) list -> string atp_problem * string Symtab.table |
118 ((string * stature) * term) list -> string atp_problem * string Symtab.table |
119 * (string * term) list * int Symtab.table |
119 * (string * term) list * int Symtab.table |
120 val atp_problem_selection_weights : string atp_problem -> (string * real) list |
|
121 val atp_problem_term_order_info : string atp_problem -> (string * int) list |
120 val atp_problem_term_order_info : string atp_problem -> (string * int) list |
122 end; |
121 end; |
123 |
122 |
124 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE = |
123 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE = |
125 struct |
124 struct |
2921 val hyp_weight = 0.1 |
2920 val hyp_weight = 0.1 |
2922 val fact_min_weight = 0.2 |
2921 val fact_min_weight = 0.2 |
2923 val fact_max_weight = 1.0 |
2922 val fact_max_weight = 1.0 |
2924 val type_info_default_weight = 0.8 |
2923 val type_info_default_weight = 0.8 |
2925 |
2924 |
2926 (* Weights are from 0.0 (most important) to 1.0 (least important). *) |
|
2927 fun atp_problem_selection_weights problem = |
|
2928 let |
|
2929 fun add_term_weights weight (ATerm ((s, _), tms)) = |
|
2930 is_tptp_user_symbol s ? Symtab.default (s, weight) #> fold (add_term_weights weight) tms |
|
2931 | add_term_weights weight (AAbs ((_, tm), args)) = |
|
2932 add_term_weights weight tm #> fold (add_term_weights weight) args |
|
2933 fun add_line_weights weight (Formula (_, _, phi, _, _)) = |
|
2934 formula_fold NONE (K (add_term_weights weight)) phi |
|
2935 | add_line_weights _ _ = I |
|
2936 fun add_conjectures_weights [] = I |
|
2937 | add_conjectures_weights conjs = |
|
2938 let val (hyps, conj) = split_last conjs in |
|
2939 add_line_weights conj_weight conj |
|
2940 #> fold (add_line_weights hyp_weight) hyps |
|
2941 end |
|
2942 fun add_facts_weights facts = |
|
2943 let |
|
2944 val num_facts = length facts |
|
2945 fun weight_of j = |
|
2946 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j |
|
2947 / Real.fromInt num_facts |
|
2948 in |
|
2949 fold_index (fn (i, fact) => add_line_weights (weight_of i) fact) facts |
|
2950 end |
|
2951 val get = these o AList.lookup (op =) problem |
|
2952 in |
|
2953 Symtab.empty |
|
2954 |> add_conjectures_weights (get free_typesN @ get conjsN) |
|
2955 |> add_facts_weights (get factsN) |
|
2956 |> fold (fold (add_line_weights type_info_default_weight) o get) |
|
2957 [explicit_declsN, subclassesN, tconsN] |
|
2958 |> Symtab.dest |
|
2959 |> sort (prod_ord Real.compare string_ord o apply2 swap) |
|
2960 end |
|
2961 |
|
2962 (* Ugly hack: may make innocent victims (collateral damage) *) |
2925 (* Ugly hack: may make innocent victims (collateral damage) *) |
2963 fun may_be_app s args = String.isPrefix app_op_name s andalso length args = 2 |
2926 fun may_be_app s args = String.isPrefix app_op_name s andalso length args = 2 |
2964 fun may_be_predicator s = |
2927 fun may_be_predicator s = |
2965 member (op =) [predicator_name, prefixed_predicator_name] s |
2928 member (op =) [predicator_name, prefixed_predicator_name] s |
2966 |
2929 |