author | wenzelm |
Wed, 02 May 2012 11:47:45 +0200 | |
changeset 47847 | 7cddb6c8f93c |
parent 47730 | 15f4309bb9eb |
child 48250 | 1065c307fafe |
permissions | -rw-r--r-- |
47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML |
38892 | 2 |
Author: Jasmin Blanchette, TU Munich |
3 |
*) |
|
4 |
||
5 |
structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = |
|
6 |
struct |
|
7 |
||
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
8 |
fun get args name default_value = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
9 |
case AList.lookup (op =) args name of |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
10 |
SOME value => the (Real.fromString value) |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
11 |
| NONE => default_value |
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset
|
12 |
|
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
13 |
fun extract_relevance_fudge args |
42738 | 14 |
{local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, |
15 |
abs_rel_weight, abs_irrel_weight, skolem_irrel_weight, |
|
16 |
theory_const_rel_weight, theory_const_irrel_weight, |
|
42735
1d375de437e9
fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42642
diff
changeset
|
17 |
chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, |
42738 | 18 |
local_bonus, assum_bonus, chained_bonus, max_imperfect, max_imperfect_exp, |
19 |
threshold_divisor, ridiculous_threshold} = |
|
20 |
{local_const_multiplier = |
|
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41455
diff
changeset
|
21 |
get args "local_const_multiplier" local_const_multiplier, |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41138
diff
changeset
|
22 |
worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
23 |
higher_order_irrel_weight = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
24 |
get args "higher_order_irrel_weight" higher_order_irrel_weight, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
25 |
abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
26 |
abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
27 |
skolem_irrel_weight = get args "skolem_irrel_weight" skolem_irrel_weight, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
28 |
theory_const_rel_weight = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
29 |
get args "theory_const_rel_weight" theory_const_rel_weight, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
30 |
theory_const_irrel_weight = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
31 |
get args "theory_const_irrel_weight" theory_const_irrel_weight, |
42735
1d375de437e9
fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42642
diff
changeset
|
32 |
chained_const_irrel_weight = |
1d375de437e9
fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42642
diff
changeset
|
33 |
get args "chained_const_irrel_weight" chained_const_irrel_weight, |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
34 |
intro_bonus = get args "intro_bonus" intro_bonus, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
35 |
elim_bonus = get args "elim_bonus" elim_bonus, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
36 |
simp_bonus = get args "simp_bonus" simp_bonus, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
37 |
local_bonus = get args "local_bonus" local_bonus, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
38 |
assum_bonus = get args "assum_bonus" assum_bonus, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
39 |
chained_bonus = get args "chained_bonus" chained_bonus, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
40 |
max_imperfect = get args "max_imperfect" max_imperfect, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
41 |
max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
42 |
threshold_divisor = get args "threshold_divisor" threshold_divisor, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
43 |
ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold} |
38902 | 44 |
|
38892 | 45 |
structure Prooftab = |
41407 | 46 |
Table(type key = int * int val ord = prod_ord int_ord int_ord) |
38892 | 47 |
|
41407 | 48 |
val proof_table = Unsynchronized.ref (Prooftab.empty: string list list Prooftab.table) |
38892 | 49 |
|
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
50 |
val num_successes = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
51 |
val num_failures = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
52 |
val num_found_proofs = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
53 |
val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
54 |
val num_found_facts = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
55 |
val num_lost_facts = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
56 |
|
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
57 |
fun get id c = the_default 0 (AList.lookup (op =) (!c) id) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
58 |
fun add id c n = |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
59 |
c := (case AList.lookup (op =) (!c) id of |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
60 |
SOME m => AList.update (op =) (id, m + n) (!c) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
61 |
| NONE => (id, n) :: !c) |
38894 | 62 |
|
63 |
fun init proof_file _ thy = |
|
38892 | 64 |
let |
65 |
fun do_line line = |
|
66 |
case line |> space_explode ":" of |
|
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
43351
diff
changeset
|
67 |
[line_num, offset, proof] => |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
43351
diff
changeset
|
68 |
SOME (pairself (the o Int.fromString) (line_num, offset), |
38892 | 69 |
proof |> space_explode " " |> filter_out (curry (op =) "")) |
70 |
| _ => NONE |
|
38894 | 71 |
val proofs = File.read (Path.explode proof_file) |
38892 | 72 |
val proof_tab = |
73 |
proofs |> space_explode "\n" |
|
74 |
|> map_filter do_line |
|
75 |
|> AList.coalesce (op =) |
|
76 |
|> Prooftab.make |
|
77 |
in proof_table := proof_tab; thy end |
|
78 |
||
38894 | 79 |
fun percentage a b = if b = 0 then "N/A" else string_of_int (a * 100 div b) |
80 |
fun percentage_alt a b = percentage a (a + b) |
|
81 |
||
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
82 |
fun done id ({log, ...} : Mirabelle.done_args) = |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
83 |
if get id num_successes + get id num_failures > 0 then |
38897 | 84 |
(log ""; |
85 |
log ("Number of overall successes: " ^ |
|
86 |
string_of_int (get id num_successes)); |
|
87 |
log ("Number of overall failures: " ^ string_of_int (get id num_failures)); |
|
38894 | 88 |
log ("Overall success rate: " ^ |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
89 |
percentage_alt (get id num_successes) (get id num_failures) ^ "%"); |
38897 | 90 |
log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs)); |
91 |
log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs)); |
|
38894 | 92 |
log ("Proof found rate: " ^ |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
93 |
percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^ |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
94 |
"%"); |
38897 | 95 |
log ("Number of found facts: " ^ string_of_int (get id num_found_facts)); |
96 |
log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts)); |
|
38894 | 97 |
log ("Fact found rate: " ^ |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
98 |
percentage_alt (get id num_found_facts) (get id num_lost_facts) ^ |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
99 |
"%")) |
38894 | 100 |
else |
101 |
() |
|
38892 | 102 |
|
40220 | 103 |
val default_prover = ATP_Systems.eN (* arbitrary ATP *) |
38892 | 104 |
|
38897 | 105 |
fun with_index (i, s) = s ^ "@" ^ string_of_int i |
106 |
||
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
107 |
fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) = |
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
43351
diff
changeset
|
108 |
case (Position.line_of pos, Position.offset_of pos) of |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
43351
diff
changeset
|
109 |
(SOME line_num, SOME offset) => |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
43351
diff
changeset
|
110 |
(case Prooftab.lookup (!proof_table) (line_num, offset) of |
38892 | 111 |
SOME proofs => |
112 |
let |
|
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43088
diff
changeset
|
113 |
val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre |
40220 | 114 |
val prover = AList.lookup (op =) args "prover" |
115 |
|> the_default default_prover |
|
45706 | 116 |
val {relevance_thresholds, max_relevant, slice, ...} = |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
41790
diff
changeset
|
117 |
Sledgehammer_Isar.default_params ctxt args |
40220 | 118 |
val default_max_relevant = |
45706 | 119 |
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
41790
diff
changeset
|
120 |
prover |
42952
96f62b77748f
tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42944
diff
changeset
|
121 |
val is_appropriate_prop = |
96f62b77748f
tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42944
diff
changeset
|
122 |
Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt |
96f62b77748f
tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42944
diff
changeset
|
123 |
default_prover |
42589
9f7c48463645
restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42579
diff
changeset
|
124 |
val is_built_in_const = |
9f7c48463645
restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42579
diff
changeset
|
125 |
Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
126 |
val relevance_fudge = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
127 |
extract_relevance_fudge args |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40941
diff
changeset
|
128 |
(Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover) |
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
129 |
val relevance_override = {add = [], del = [], only = false} |
38892 | 130 |
val subgoal = 1 |
43088 | 131 |
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal |
44625 | 132 |
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover |
38892 | 133 |
val facts = |
44625 | 134 |
Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override |
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43088
diff
changeset
|
135 |
chained_ths hyp_ts concl_t |
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43088
diff
changeset
|
136 |
|> filter (is_appropriate_prop o prop_of o snd) |
44625 | 137 |
|> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds |
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43088
diff
changeset
|
138 |
(the_default default_max_relevant max_relevant) |
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43088
diff
changeset
|
139 |
is_built_in_const relevance_fudge relevance_override |
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43088
diff
changeset
|
140 |
chained_ths hyp_ts concl_t |
38892 | 141 |
|> map (fst o fst) |
38894 | 142 |
val (found_facts, lost_facts) = |
41455 | 143 |
flat proofs |> sort_distinct string_ord |
38897 | 144 |
|> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |
145 |
|> List.partition (curry (op <=) 0 o fst) |
|
146 |
|>> sort (prod_ord int_ord string_ord) ||> map snd |
|
38892 | 147 |
val found_proofs = filter (forall (member (op =) facts)) proofs |
38894 | 148 |
val n = length found_proofs |
38892 | 149 |
val _ = |
38894 | 150 |
if n = 0 then |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
151 |
(add id num_failures 1; log "Failure") |
38894 | 152 |
else |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
153 |
(add id num_successes 1; |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
154 |
add id num_found_proofs n; |
38897 | 155 |
log ("Success (" ^ string_of_int n ^ " of " ^ |
156 |
string_of_int (length proofs) ^ " proofs)")) |
|
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
157 |
val _ = add id num_lost_proofs (length proofs - n) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
158 |
val _ = add id num_found_facts (length found_facts) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
159 |
val _ = add id num_lost_facts (length lost_facts) |
38902 | 160 |
val _ = |
161 |
if null found_facts then |
|
162 |
() |
|
163 |
else |
|
164 |
let |
|
165 |
val found_weight = |
|
166 |
Real.fromInt (fold (fn (n, _) => |
|
167 |
Integer.add (n * n)) found_facts 0) |
|
168 |
/ Real.fromInt (length found_facts) |
|
169 |
|> Math.sqrt |> Real.ceil |
|
170 |
in |
|
171 |
log ("Found facts (among " ^ string_of_int (length facts) ^ |
|
172 |
", weight " ^ string_of_int found_weight ^ "): " ^ |
|
173 |
commas (map with_index found_facts)) |
|
174 |
end |
|
175 |
val _ = if null lost_facts then |
|
38897 | 176 |
() |
177 |
else |
|
38902 | 178 |
log ("Lost facts (among " ^ string_of_int (length facts) ^ |
179 |
"): " ^ commas lost_facts) |
|
38892 | 180 |
in () end |
38894 | 181 |
| NONE => log "No known proof") |
38892 | 182 |
| _ => () |
183 |
||
38894 | 184 |
val proof_fileK = "proof_file" |
185 |
||
186 |
fun invoke args = |
|
187 |
let |
|
188 |
val (pf_args, other_args) = |
|
189 |
args |> List.partition (curry (op =) proof_fileK o fst) |
|
190 |
val proof_file = case pf_args of |
|
191 |
[] => error "No \"proof_file\" specified" |
|
192 |
| (_, s) :: _ => s |
|
193 |
in Mirabelle.register (init proof_file, action other_args, done) end |
|
38892 | 194 |
|
195 |
end; |
|
38894 | 196 |
|
197 |
(* Workaround to keep the "mirabelle.pl" script happy *) |
|
198 |
structure Mirabelle_Sledgehammer_filter = Mirabelle_Sledgehammer_Filter; |