author | blanchet |
Thu, 15 Sep 2011 10:57:40 +0200 | |
changeset 44934 | 2302faa4ae0e |
parent 44785 | f4975fa4a2f8 |
child 45034 | b0f61dec677a |
permissions | -rw-r--r-- |
38988 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter.ML |
38027 | 2 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36227
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
39958 | 4 |
|
5 |
Sledgehammer's relevance filter. |
|
33309 | 6 |
*) |
15452 | 7 |
|
38988 | 8 |
signature SLEDGEHAMMER_FILTER = |
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset
|
9 |
sig |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43066
diff
changeset
|
10 |
type locality = ATP_Translate.locality |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset
|
11 |
|
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
12 |
type relevance_fudge = |
42738 | 13 |
{local_const_multiplier : real, |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41158
diff
changeset
|
14 |
worse_irrel_freq : real, |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
15 |
higher_order_irrel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
16 |
abs_rel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
17 |
abs_irrel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
18 |
skolem_irrel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
19 |
theory_const_rel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
20 |
theory_const_irrel_weight : real, |
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:
42732
diff
changeset
|
21 |
chained_const_irrel_weight : real, |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
22 |
intro_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
23 |
elim_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
24 |
simp_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
25 |
local_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
26 |
assum_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
27 |
chained_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
28 |
max_imperfect : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
29 |
max_imperfect_exp : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
30 |
threshold_divisor : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
31 |
ridiculous_threshold : real} |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
32 |
|
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset
|
33 |
type relevance_override = |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
34 |
{add : (Facts.ref * Attrib.src list) list, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
35 |
del : (Facts.ref * Attrib.src list) list, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
36 |
only : bool} |
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset
|
37 |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
38 |
val trace : bool Config.T |
42728
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
39 |
val ignore_no_atp : bool Config.T |
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
40 |
val instantiate_inducts : bool Config.T |
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44400
diff
changeset
|
41 |
val no_relevance_override : 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:
43324
diff
changeset
|
42 |
val const_names_in_fact : |
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:
43324
diff
changeset
|
43 |
theory -> (string * typ -> term list -> bool * term list) -> term |
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:
43324
diff
changeset
|
44 |
-> string list |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
45 |
val fact_from_ref : |
38996 | 46 |
Proof.context -> unit Symtab.table -> thm list |
47 |
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list |
|
41767
44b2a0385001
export useful function (needed in a Sledgehammer-related experiment)
blanchet
parents:
41491
diff
changeset
|
48 |
val all_facts : |
44585 | 49 |
Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list |
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:
43324
diff
changeset
|
50 |
-> (((unit -> string) * locality) * thm) list |
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:
43324
diff
changeset
|
51 |
val nearly_all_facts : |
44585 | 52 |
Proof.context -> bool -> relevance_override -> thm list -> term list -> term |
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:
43324
diff
changeset
|
53 |
-> (((unit -> string) * locality) * thm) list |
37347
635425a442e8
show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset
|
54 |
val relevant_facts : |
44625 | 55 |
Proof.context -> real * real -> int |
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset
|
56 |
-> (string * typ -> term list -> bool * term list) -> relevance_fudge |
41066
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset
|
57 |
-> relevance_override -> thm list -> term list -> term |
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:
43324
diff
changeset
|
58 |
-> (((unit -> string) * locality) * thm) list |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
59 |
-> ((string * locality) * thm) list |
15347 | 60 |
end; |
61 |
||
38988 | 62 |
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = |
15347 | 63 |
struct |
64 |
||
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43066
diff
changeset
|
65 |
open ATP_Translate |
44934 | 66 |
open Metis_Tactic |
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38644
diff
changeset
|
67 |
open Sledgehammer_Util |
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38644
diff
changeset
|
68 |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
69 |
val trace = |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
70 |
Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false) |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
71 |
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
35826 | 72 |
|
41273
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset
|
73 |
(* experimental features *) |
42728
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
74 |
val ignore_no_atp = |
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
75 |
Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false) |
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
76 |
val instantiate_inducts = |
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
77 |
Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
78 |
|
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
79 |
type relevance_fudge = |
42738 | 80 |
{local_const_multiplier : real, |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41158
diff
changeset
|
81 |
worse_irrel_freq : real, |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
82 |
higher_order_irrel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
83 |
abs_rel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
84 |
abs_irrel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
85 |
skolem_irrel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
86 |
theory_const_rel_weight : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
87 |
theory_const_irrel_weight : real, |
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:
42732
diff
changeset
|
88 |
chained_const_irrel_weight : real, |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
89 |
intro_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
90 |
elim_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
91 |
simp_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
92 |
local_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
93 |
assum_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
94 |
chained_bonus : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
95 |
max_imperfect : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
96 |
max_imperfect_exp : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
97 |
threshold_divisor : real, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
98 |
ridiculous_threshold : real} |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
99 |
|
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset
|
100 |
type relevance_override = |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
101 |
{add : (Facts.ref * Attrib.src list) list, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
102 |
del : (Facts.ref * Attrib.src list) list, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
103 |
only : bool} |
21070 | 104 |
|
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44400
diff
changeset
|
105 |
val no_relevance_override = {add = [], del = [], only = false} |
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44400
diff
changeset
|
106 |
|
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset
|
107 |
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator |
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39718
diff
changeset
|
108 |
val abs_name = sledgehammer_prefix ^ "abs" |
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39718
diff
changeset
|
109 |
val skolem_prefix = sledgehammer_prefix ^ "sko" |
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset
|
110 |
val theory_const_suffix = Long_Name.separator ^ " 1" |
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset
|
111 |
|
40227
e31e3f0071d4
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents:
40205
diff
changeset
|
112 |
fun needs_quoting reserved s = |
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
113 |
Symtab.defined reserved s orelse |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
41999
diff
changeset
|
114 |
exists (not o Lexicon.is_identifier) (Long_Name.explode s) |
40227
e31e3f0071d4
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents:
40205
diff
changeset
|
115 |
|
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
116 |
fun make_name reserved multi j name = |
40227
e31e3f0071d4
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents:
40205
diff
changeset
|
117 |
(name |> needs_quoting reserved name ? quote) ^ |
41491 | 118 |
(if multi then "(" ^ string_of_int j ^ ")" else "") |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
119 |
|
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
120 |
fun explode_interval _ (Facts.FromTo (i, j)) = i upto j |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
121 |
| explode_interval max (Facts.From i) = i upto i + max - 1 |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
122 |
| explode_interval _ (Facts.Single i) = [i] |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
123 |
|
41279 | 124 |
val backquote = |
125 |
raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`" |
|
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
126 |
fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) = |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
127 |
let |
38996 | 128 |
val ths = Attrib.eval_thms ctxt [xthm] |
129 |
val bracket = |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41989
diff
changeset
|
130 |
map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41989
diff
changeset
|
131 |
|> implode |
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
132 |
fun nth_name j = |
38996 | 133 |
case xref of |
41279 | 134 |
Facts.Fact s => backquote s ^ bracket |
38996 | 135 |
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]" |
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
136 |
| Facts.Named ((name, _), NONE) => |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
137 |
make_name reserved (length ths > 1) (j + 1) name ^ bracket |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
138 |
| Facts.Named ((name, _), SOME intervals) => |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
139 |
make_name reserved true |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
140 |
(nth (maps (explode_interval (length ths)) intervals) j) name ^ |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
141 |
bracket |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
142 |
in |
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
143 |
(ths, (0, [])) |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset
|
144 |
|-> fold (fn th => fn (j, rest) => |
43421 | 145 |
(j + 1, |
146 |
((nth_name j, |
|
147 |
if member Thm.eq_thm_prop chained_ths th then Chained |
|
148 |
else General), th) :: rest)) |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
149 |
|> snd |
38699 | 150 |
end |
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset
|
151 |
|
41199 | 152 |
(* This is a terrible hack. Free variables are sometimes code as "M__" when they |
153 |
are displayed as "M" and we want to avoid clashes with these. But sometimes |
|
154 |
it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all |
|
155 |
free variables. In the worse case scenario, where the fact won't be resolved |
|
156 |
correctly, the user can fix it manually, e.g., by naming the fact in |
|
157 |
question. Ideally we would need nothing of it, but backticks just don't work |
|
158 |
with schematic variables. *) |
|
159 |
fun all_prefixes_of s = |
|
160 |
map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) |
|
161 |
fun close_form t = |
|
162 |
(t, [] |> Term.add_free_names t |> maps all_prefixes_of) |
|
163 |
|> fold (fn ((s, i), T) => fn (t', taken) => |
|
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
43245
diff
changeset
|
164 |
let val s' = singleton (Name.variant_list taken) s in |
41199 | 165 |
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const |
166 |
else Term.all) T |
|
167 |
$ Abs (s', T, abstract_over (Var ((s, i), T), t')), |
|
168 |
s' :: taken) |
|
169 |
end) |
|
170 |
(Term.add_vars t [] |> sort_wrt (fst o fst)) |
|
171 |
|> fst |
|
172 |
||
173 |
fun string_for_term ctxt t = |
|
174 |
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
|
175 |
(print_mode_value ())) (Syntax.string_of_term ctxt) t |
|
176 |
|> String.translate (fn c => if Char.isPrint c then str c else "") |
|
177 |
|> simplify_spaces |
|
178 |
||
179 |
(** Structural induction rules **) |
|
180 |
||
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset
|
181 |
fun struct_induct_rule_on th = |
41199 | 182 |
case Logic.strip_horn (prop_of th) of |
183 |
(prems, @{const Trueprop} |
|
184 |
$ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => |
|
185 |
if not (is_TVar ind_T) andalso length prems > 1 andalso |
|
186 |
exists (exists_subterm (curry (op aconv) p)) prems andalso |
|
187 |
not (exists (exists_subterm (curry (op aconv) a)) prems) then |
|
188 |
SOME (p_name, ind_T) |
|
189 |
else |
|
190 |
NONE |
|
191 |
| _ => NONE |
|
192 |
||
43245 | 193 |
fun instantiate_induct_rule ctxt concl_prop p_name ((name, loc), th) ind_x = |
41199 | 194 |
let |
195 |
fun varify_noninducts (t as Free (s, T)) = |
|
196 |
if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) |
|
197 |
| varify_noninducts t = t |
|
198 |
val p_inst = |
|
199 |
concl_prop |> map_aterms varify_noninducts |> close_form |
|
200 |
|> lambda (Free ind_x) |
|
201 |
|> string_for_term ctxt |
|
202 |
in |
|
41207 | 203 |
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", loc), |
43245 | 204 |
th |> read_instantiate ctxt [((p_name, 0), p_inst)]) |
41199 | 205 |
end |
206 |
||
207 |
fun type_match thy (T1, T2) = |
|
208 |
(Sign.typ_match thy (T2, T1) Vartab.empty; true) |
|
209 |
handle Type.TYPE_MATCH => false |
|
210 |
||
43245 | 211 |
fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = |
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset
|
212 |
case struct_induct_rule_on th of |
41199 | 213 |
SOME (p_name, ind_T) => |
42361 | 214 |
let val thy = Proof_Context.theory_of ctxt in |
41199 | 215 |
stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) |
216 |
|> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax)) |
|
217 |
end |
|
218 |
| NONE => [ax] |
|
219 |
||
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset
|
220 |
(***************************************************************) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset
|
221 |
(* Relevance Filtering *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset
|
222 |
(***************************************************************) |
19194 | 223 |
|
24287 | 224 |
(*** constants with types ***) |
225 |
||
38939 | 226 |
fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) = |
227 |
order_of_type T1 (* cheat: pretend sets are first-order *) |
|
228 |
| order_of_type (Type (@{type_name fun}, [T1, T2])) = |
|
229 |
Int.max (order_of_type T1 + 1, order_of_type T2) |
|
230 |
| order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0 |
|
231 |
| order_of_type _ = 0 |
|
232 |
||
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
233 |
(* An abstraction of Isabelle types and first-order terms *) |
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
234 |
datatype pattern = PVar | PApp of string * pattern list |
38939 | 235 |
datatype ptype = PType of int * pattern list |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
236 |
|
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
237 |
fun string_for_pattern PVar = "_" |
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
238 |
| string_for_pattern (PApp (s, ps)) = |
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
239 |
if null ps then s else s ^ string_for_patterns ps |
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
240 |
and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" |
38939 | 241 |
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps |
24287 | 242 |
|
243 |
(*Is the second type an instance of the first one?*) |
|
38824 | 244 |
fun match_pattern (PVar, _) = true |
245 |
| match_pattern (PApp _, PVar) = false |
|
246 |
| match_pattern (PApp (s, ps), PApp (t, qs)) = |
|
247 |
s = t andalso match_patterns (ps, qs) |
|
248 |
and match_patterns (_, []) = true |
|
249 |
| match_patterns ([], _) = false |
|
250 |
| match_patterns (p :: ps, q :: qs) = |
|
251 |
match_pattern (p, q) andalso match_patterns (ps, qs) |
|
38939 | 252 |
fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs) |
24287 | 253 |
|
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
254 |
(* Is there a unifiable constant? *) |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
255 |
fun pconst_mem f consts (s, ps) = |
38939 | 256 |
exists (curry (match_ptype o f) ps) |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
257 |
(map snd (filter (curry (op =) s o fst) consts)) |
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
258 |
fun pconst_hyper_mem f const_tab (s, ps) = |
38939 | 259 |
exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s)) |
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents:
37504
diff
changeset
|
260 |
|
38939 | 261 |
fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts) |
262 |
| pattern_for_type (TFree (s, _)) = PApp (s, []) |
|
263 |
| pattern_for_type (TVar _) = PVar |
|
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
264 |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
265 |
(* Pairs a constant with the list of its type instantiations. *) |
41204
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset
|
266 |
fun ptype thy const x = |
38939 | 267 |
(if const then map pattern_for_type (these (try (Sign.const_typargs thy) x)) |
41204
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset
|
268 |
else []) |
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset
|
269 |
fun rich_ptype thy const (s, T) = |
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset
|
270 |
PType (order_of_type T, ptype thy const (s, T)) |
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset
|
271 |
fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T)) |
24287 | 272 |
|
38939 | 273 |
fun string_for_hyper_pconst (s, ps) = |
274 |
s ^ "{" ^ commas (map string_for_ptype ps) ^ "}" |
|
24287 | 275 |
|
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
276 |
(* Add a pconstant to the table, but a [] entry means a standard |
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset
|
277 |
connective, which we ignore.*) |
41066
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset
|
278 |
fun add_pconst_to_table also_skolem (s, p) = |
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset
|
279 |
if (not also_skolem andalso String.isPrefix skolem_prefix s) then I |
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset
|
280 |
else Symtab.map_default (s, [p]) (insert (op =) p) |
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset
|
281 |
|
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
282 |
(* Set constants tend to pull in too many irrelevant facts. We limit the damage |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
283 |
by treating them more or less as if they were built-in but add their |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
284 |
definition at the end. *) |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
285 |
val set_consts = |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
286 |
[(@{const_name Collect}, @{thms Collect_def}), |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
287 |
(@{const_name Set.member}, @{thms mem_def})] |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
288 |
|
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
289 |
val is_set_const = AList.defined (op =) set_consts |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
290 |
|
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
291 |
fun add_pconsts_in_term thy is_built_in_const also_skolems pos = |
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents:
37504
diff
changeset
|
292 |
let |
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset
|
293 |
val flip = Option.map not |
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset
|
294 |
(* We include free variables, as well as constants, to handle locales. For |
41205 | 295 |
each quantifiers that must necessarily be skolemized by the automatic |
296 |
prover, we introduce a fresh constant to simulate the effect of |
|
297 |
Skolemization. *) |
|
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
298 |
fun do_const const ext_arg (x as (s, _)) ts = |
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset
|
299 |
let val (built_in, ts) = is_built_in_const x ts in |
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
300 |
if is_set_const s then |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
301 |
fold (do_term ext_arg) ts |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
302 |
else |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
303 |
(not built_in |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
304 |
? add_pconst_to_table also_skolems (rich_pconst thy const x)) |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
305 |
#> fold (do_term false) ts |
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset
|
306 |
end |
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
307 |
and do_term ext_arg t = |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
308 |
case strip_comb t of |
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
309 |
(Const x, ts) => do_const true ext_arg x ts |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
310 |
| (Free x, ts) => do_const false ext_arg x ts |
38939 | 311 |
| (Abs (_, T, t'), ts) => |
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
312 |
((null ts andalso not ext_arg) |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
313 |
(* Since lambdas on the right-hand side of equalities are usually |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
314 |
extensionalized later by "extensionalize_term", we don't penalize |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
315 |
them here. *) |
41066
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset
|
316 |
? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, []))) |
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:
42732
diff
changeset
|
317 |
#> fold (do_term false) (t' :: ts) |
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:
42732
diff
changeset
|
318 |
| (_, ts) => fold (do_term false) ts |
38939 | 319 |
fun do_quantifier will_surely_be_skolemized abs_T body_t = |
37537 | 320 |
do_formula pos body_t |
38747 | 321 |
#> (if also_skolems andalso will_surely_be_skolemized then |
41066
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset
|
322 |
add_pconst_to_table true |
43559
c1966f322105
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
wenzelm
parents:
43492
diff
changeset
|
323 |
(legacy_gensym skolem_prefix, PType (order_of_type abs_T, [])) |
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset
|
324 |
else |
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset
|
325 |
I) |
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
326 |
and do_term_or_formula ext_arg T = |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
327 |
if T = HOLogic.boolT then do_formula NONE else do_term ext_arg |
37537 | 328 |
and do_formula pos t = |
329 |
case t of |
|
38939 | 330 |
Const (@{const_name all}, _) $ Abs (_, T, t') => |
331 |
do_quantifier (pos = SOME false) T t' |
|
37537 | 332 |
| @{const "==>"} $ t1 $ t2 => |
333 |
do_formula (flip pos) t1 #> do_formula pos t2 |
|
334 |
| Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => |
|
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
335 |
do_term_or_formula false T t1 #> do_term_or_formula true T t2 |
37537 | 336 |
| @{const Trueprop} $ t1 => do_formula pos t1 |
41140
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
337 |
| @{const False} => I |
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
338 |
| @{const True} => I |
37537 | 339 |
| @{const Not} $ t1 => do_formula (flip pos) t1 |
38939 | 340 |
| Const (@{const_name All}, _) $ Abs (_, T, t') => |
341 |
do_quantifier (pos = SOME false) T t' |
|
342 |
| Const (@{const_name Ex}, _) $ Abs (_, T, t') => |
|
343 |
do_quantifier (pos = SOME true) T t' |
|
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
344 |
| @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2] |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
345 |
| @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2] |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset
|
346 |
| @{const HOL.implies} $ t1 $ t2 => |
37537 | 347 |
do_formula (flip pos) t1 #> do_formula pos t2 |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset
|
348 |
| Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 => |
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
349 |
do_term_or_formula false T t1 #> do_term_or_formula true T t2 |
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset
|
350 |
| Const (@{const_name If}, Type (_, [_, Type (_, [T, _])])) |
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset
|
351 |
$ t1 $ t2 $ t3 => |
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:
42732
diff
changeset
|
352 |
do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3] |
38939 | 353 |
| Const (@{const_name Ex1}, _) $ Abs (_, T, t') => |
354 |
do_quantifier (is_some pos) T t' |
|
355 |
| Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') => |
|
356 |
do_quantifier (pos = SOME false) T |
|
357 |
(HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t')) |
|
358 |
| Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') => |
|
359 |
do_quantifier (pos = SOME true) T |
|
360 |
(HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t')) |
|
37537 | 361 |
| (t0 as Const (_, @{typ bool})) $ t1 => |
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:
42732
diff
changeset
|
362 |
do_term false t0 #> do_formula pos t1 (* theory constant *) |
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:
42732
diff
changeset
|
363 |
| _ => do_term false t |
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
364 |
in do_formula pos end |
24287 | 365 |
|
366 |
(*Inserts a dummy "constant" referring to the theory name, so that relevance |
|
367 |
takes the given theory into account.*) |
|
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset
|
368 |
fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...} |
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset
|
369 |
: relevance_fudge) thy_name t = |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
370 |
if exists (curry (op <) 0.0) [theory_const_rel_weight, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
371 |
theory_const_irrel_weight] then |
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset
|
372 |
Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t |
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents:
37504
diff
changeset
|
373 |
else |
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset
|
374 |
t |
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset
|
375 |
|
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset
|
376 |
fun theory_const_prop_of fudge th = |
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset
|
377 |
theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th) |
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents:
37504
diff
changeset
|
378 |
|
24287 | 379 |
(**** Constant / Type Frequencies ****) |
380 |
||
38743 | 381 |
(* A two-dimensional symbol table counts frequencies of constants. It's keyed |
382 |
first by constant name and second by its list of type instantiations. For the |
|
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
383 |
latter, we need a linear ordering on "pattern list". *) |
24287 | 384 |
|
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
385 |
fun pattern_ord p = |
38743 | 386 |
case p of |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
387 |
(PVar, PVar) => EQUAL |
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
388 |
| (PVar, PApp _) => LESS |
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
389 |
| (PApp _, PVar) => GREATER |
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
390 |
| (PApp q1, PApp q2) => |
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset
|
391 |
prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2) |
38939 | 392 |
fun ptype_ord (PType p, PType q) = |
393 |
prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q) |
|
24287 | 394 |
|
38939 | 395 |
structure PType_Tab = Table(type key = ptype val ord = ptype_ord) |
24287 | 396 |
|
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
397 |
fun count_fact_consts thy fudge = |
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset
|
398 |
let |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
399 |
fun do_const const (s, T) ts = |
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
400 |
(* Two-dimensional table update. Constant maps to types maps to count. *) |
41204
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset
|
401 |
PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1) |
38939 | 402 |
|> Symtab.map_default (s, PType_Tab.empty) |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
403 |
#> fold do_term ts |
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
404 |
and do_term t = |
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
405 |
case strip_comb t of |
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
406 |
(Const x, ts) => do_const true x ts |
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
407 |
| (Free x, ts) => do_const false x ts |
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
408 |
| (Abs (_, _, t'), ts) => fold do_term (t' :: ts) |
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
409 |
| (_, ts) => fold do_term ts |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
410 |
in do_term o theory_const_prop_of fudge o snd end |
24287 | 411 |
|
412 |
||
413 |
(**** Actual Filtering Code ****) |
|
414 |
||
39367 | 415 |
fun pow_int _ 0 = 1.0 |
38939 | 416 |
| pow_int x 1 = x |
417 |
| pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x |
|
418 |
||
24287 | 419 |
(*The frequency of a constant is the sum of those of all instances of its type.*) |
38824 | 420 |
fun pconst_freq match const_tab (c, ps) = |
38939 | 421 |
PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m) |
422 |
(the (Symtab.lookup const_tab c)) 0 |
|
38686 | 423 |
|
24287 | 424 |
|
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset
|
425 |
(* A surprising number of theorems contain only a few significant constants. |
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset
|
426 |
These include all induction rules, and other general theorems. *) |
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset
|
427 |
|
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset
|
428 |
(* "log" seems best in practice. A constant function of one ignores the constant |
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset
|
429 |
frequencies. Rare constants give more points if they are relevant than less |
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset
|
430 |
rare ones. *) |
39367 | 431 |
fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0) |
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset
|
432 |
|
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset
|
433 |
(* Irrelevant constants are treated differently. We associate lower penalties to |
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset
|
434 |
very rare constants and very common ones -- the former because they can't |
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset
|
435 |
lead to the inclusion of too many new facts, and the latter because they are |
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset
|
436 |
so common as to be of little interest. *) |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
437 |
fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...} |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
438 |
: relevance_fudge) order freq = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
439 |
let val (k, x) = worse_irrel_freq |> `Real.ceil in |
38939 | 440 |
(if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x |
441 |
else rel_weight_for order freq / rel_weight_for order k) |
|
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
442 |
* pow_int higher_order_irrel_weight (order - 1) |
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset
|
443 |
end |
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset
|
444 |
|
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
445 |
fun multiplier_for_const_name local_const_multiplier s = |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
446 |
if String.isSubstring "." s then 1.0 else local_const_multiplier |
38821 | 447 |
|
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
448 |
(* Computes a constant's weight, as determined by its frequency. *) |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
449 |
fun generic_pconst_weight local_const_multiplier abs_weight skolem_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:
42732
diff
changeset
|
450 |
theory_const_weight chained_const_weight weight_for f |
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:
42732
diff
changeset
|
451 |
const_tab chained_const_tab (c as (s, PType (m, _))) = |
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
452 |
if s = abs_name then |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
453 |
abs_weight |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
454 |
else if String.isPrefix skolem_prefix s then |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
455 |
skolem_weight |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
456 |
else if String.isSuffix theory_const_suffix s then |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
457 |
theory_const_weight |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
458 |
else |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
459 |
multiplier_for_const_name local_const_multiplier s |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
460 |
* weight_for m (pconst_freq (match_ptype o f) const_tab c) |
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:
42732
diff
changeset
|
461 |
|> (if chained_const_weight < 1.0 andalso |
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:
42732
diff
changeset
|
462 |
pconst_hyper_mem I chained_const_tab c then |
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:
42732
diff
changeset
|
463 |
curry (op *) chained_const_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:
42732
diff
changeset
|
464 |
else |
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:
42732
diff
changeset
|
465 |
I) |
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
466 |
|
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
467 |
fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight, |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
468 |
theory_const_rel_weight, ...} : relevance_fudge) |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
469 |
const_tab = |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
470 |
generic_pconst_weight local_const_multiplier abs_rel_weight 0.0 |
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:
42732
diff
changeset
|
471 |
theory_const_rel_weight 0.0 rel_weight_for I const_tab |
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:
42732
diff
changeset
|
472 |
Symtab.empty |
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:
42732
diff
changeset
|
473 |
|
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
474 |
fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight, |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
475 |
skolem_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:
42732
diff
changeset
|
476 |
theory_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:
42732
diff
changeset
|
477 |
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:
42732
diff
changeset
|
478 |
const_tab chained_const_tab = |
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
479 |
generic_pconst_weight local_const_multiplier abs_irrel_weight |
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset
|
480 |
skolem_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:
42732
diff
changeset
|
481 |
chained_const_irrel_weight (irrel_weight_for fudge) swap |
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:
42732
diff
changeset
|
482 |
const_tab chained_const_tab |
24287 | 483 |
|
43421 | 484 |
fun locality_bonus ({intro_bonus, ...} : relevance_fudge) Intro = intro_bonus |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
485 |
| locality_bonus {elim_bonus, ...} Elim = elim_bonus |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
486 |
| locality_bonus {simp_bonus, ...} Simp = simp_bonus |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
487 |
| locality_bonus {local_bonus, ...} Local = local_bonus |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
488 |
| locality_bonus {assum_bonus, ...} Assum = assum_bonus |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
489 |
| locality_bonus {chained_bonus, ...} Chained = chained_bonus |
43421 | 490 |
| locality_bonus _ _ = 0.0 |
38751
01c4d14b2a61
add a bonus for chained facts, since they are likely to be relevant;
blanchet
parents:
38749
diff
changeset
|
491 |
|
40418 | 492 |
fun is_odd_const_name s = |
493 |
s = abs_name orelse String.isPrefix skolem_prefix s orelse |
|
494 |
String.isSuffix theory_const_suffix s |
|
495 |
||
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
496 |
fun fact_weight fudge loc const_tab relevant_consts chained_consts fact_consts = |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
497 |
case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts) |
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
498 |
||> filter_out (pconst_hyper_mem swap relevant_consts) of |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
499 |
([], _) => 0.0 |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
500 |
| (rel, irrel) => |
40418 | 501 |
if forall (forall (is_odd_const_name o fst)) [rel, irrel] then |
40371 | 502 |
0.0 |
503 |
else |
|
504 |
let |
|
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:
42732
diff
changeset
|
505 |
val irrel = irrel |> filter_out (pconst_mem swap rel) |
40371 | 506 |
val rel_weight = |
507 |
0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel |
|
508 |
val irrel_weight = |
|
509 |
~ (locality_bonus fudge loc) |
|
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:
42732
diff
changeset
|
510 |
|> fold (curry (op +) |
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:
42732
diff
changeset
|
511 |
o irrel_pconst_weight fudge const_tab chained_consts) irrel |
40371 | 512 |
val res = rel_weight / (rel_weight + irrel_weight) |
513 |
in if Real.isFinite res then res else 0.0 end |
|
38747 | 514 |
|
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40251
diff
changeset
|
515 |
fun pconsts_in_fact thy is_built_in_const t = |
38825 | 516 |
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) |
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
517 |
(Symtab.empty |> add_pconsts_in_term thy is_built_in_const true |
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
518 |
(SOME true) t) [] |
42729 | 519 |
|
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40251
diff
changeset
|
520 |
fun pair_consts_fact thy is_built_in_const fudge fact = |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
521 |
case fact |> snd |> theory_const_prop_of fudge |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40251
diff
changeset
|
522 |
|> pconsts_in_fact thy is_built_in_const of |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
523 |
[] => NONE |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
524 |
| consts => SOME ((fact, consts), NONE) |
24287 | 525 |
|
41768
dd2125fb75f9
export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents:
41767
diff
changeset
|
526 |
val const_names_in_fact = map fst ooo pconsts_in_fact |
dd2125fb75f9
export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents:
41767
diff
changeset
|
527 |
|
38699 | 528 |
type annotated_thm = |
38939 | 529 |
(((unit -> string) * locality) * thm) * (string * ptype) list |
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents:
37504
diff
changeset
|
530 |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
531 |
fun take_most_relevant ctxt max_relevant remaining_max |
42728
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
532 |
({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
533 |
(candidates : (annotated_thm * real) list) = |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
534 |
let |
38747 | 535 |
val max_imperfect = |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
536 |
Real.ceil (Math.pow (max_imperfect, |
38904 | 537 |
Math.pow (Real.fromInt remaining_max |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
538 |
/ Real.fromInt max_relevant, max_imperfect_exp))) |
38747 | 539 |
val (perfect, imperfect) = |
38889 | 540 |
candidates |> sort (Real.compare o swap o pairself snd) |
541 |
|> take_prefix (fn (_, w) => w > 0.99999) |
|
38747 | 542 |
val ((accepts, more_rejects), rejects) = |
543 |
chop max_imperfect imperfect |>> append perfect |>> chop remaining_max |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
544 |
in |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
545 |
trace_msg ctxt (fn () => |
41491 | 546 |
"Actually passed (" ^ string_of_int (length accepts) ^ " of " ^ |
547 |
string_of_int (length candidates) ^ "): " ^ |
|
38889 | 548 |
(accepts |> map (fn ((((name, _), _), _), weight) => |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset
|
549 |
name () ^ " [" ^ Real.toString weight ^ "]") |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
550 |
|> commas)); |
38747 | 551 |
(accepts, more_rejects @ rejects) |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
552 |
end |
24287 | 553 |
|
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40251
diff
changeset
|
554 |
fun if_empty_replace_with_locality thy is_built_in_const facts loc tab = |
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset
|
555 |
if Symtab.is_empty tab then |
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
556 |
Symtab.empty |
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
557 |
|> fold (add_pconsts_in_term thy is_built_in_const false (SOME false)) |
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
558 |
(map_filter (fn ((_, loc'), th) => |
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
559 |
if loc' = loc then SOME (prop_of th) else NONE) |
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
560 |
facts) |
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset
|
561 |
else |
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset
|
562 |
tab |
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset
|
563 |
|
42702 | 564 |
fun consider_arities is_built_in_const th = |
41158
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
565 |
let |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
566 |
fun aux _ _ NONE = NONE |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
567 |
| aux t args (SOME tab) = |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
568 |
case t of |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
569 |
t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 [] |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
570 |
| Const (x as (s, _)) => |
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset
|
571 |
(if is_built_in_const x args |> fst then |
41158
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
572 |
SOME tab |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
573 |
else case Symtab.lookup tab s of |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
574 |
NONE => SOME (Symtab.update (s, length args) tab) |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
575 |
| SOME n => if n = length args then SOME tab else NONE) |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
576 |
| _ => SOME tab |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
577 |
in aux (prop_of th) [] end |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
578 |
|
44785 | 579 |
(* FIXME: This is currently only useful for polymorphic type encodings. *) |
42702 | 580 |
fun could_benefit_from_ext is_built_in_const facts = |
581 |
fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty) |
|
41158
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
582 |
|> is_none |
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset
|
583 |
|
43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
584 |
(* High enough so that it isn't wrongly considered as very relevant (e.g., for E |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
585 |
weights), but low enough so that it is unlikely to be truncated away if few |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
586 |
facts are included. *) |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
587 |
val special_fact_index = 75 |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
588 |
|
44625 | 589 |
fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
590 |
(fudge as {threshold_divisor, ridiculous_threshold, ...}) |
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
591 |
({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t = |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
592 |
let |
42361 | 593 |
val thy = Proof_Context.theory_of ctxt |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
594 |
val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty |
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
595 |
val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME |
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
596 |
val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts |
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset
|
597 |
val goal_const_tab = |
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
598 |
Symtab.empty |> fold (add_pconsts true) hyp_ts |
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
599 |
|> add_pconsts false concl_t |
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
600 |
|> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab) |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40251
diff
changeset
|
601 |
|> fold (if_empty_replace_with_locality thy is_built_in_const facts) |
38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset
|
602 |
[Chained, Assum, Local] |
39012 | 603 |
val add_ths = Attrib.eval_thms ctxt add |
604 |
val del_ths = Attrib.eval_thms ctxt del |
|
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
605 |
val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd) |
38747 | 606 |
fun iter j remaining_max threshold rel_const_tab hopeless hopeful = |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
607 |
let |
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset
|
608 |
fun relevant [] _ [] = |
38747 | 609 |
(* Nothing has been added this iteration. *) |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
610 |
if j = 0 andalso threshold >= ridiculous_threshold then |
38747 | 611 |
(* First iteration? Try again. *) |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset
|
612 |
iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab |
38747 | 613 |
hopeless hopeful |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
614 |
else |
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset
|
615 |
[] |
38889 | 616 |
| relevant candidates rejects [] = |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
617 |
let |
38747 | 618 |
val (accepts, more_rejects) = |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
619 |
take_most_relevant ctxt max_relevant remaining_max fudge |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
620 |
candidates |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
621 |
val rel_const_tab' = |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
622 |
rel_const_tab |
41066
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset
|
623 |
|> fold (add_pconst_to_table false) (maps (snd o fst) accepts) |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
624 |
fun is_dirty (c, _) = |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
625 |
Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
626 |
val (hopeful_rejects, hopeless_rejects) = |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
627 |
(rejects @ hopeless, ([], [])) |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
628 |
|-> fold (fn (ax as (_, consts), old_weight) => |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
629 |
if exists is_dirty consts then |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
630 |
apfst (cons (ax, NONE)) |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
631 |
else |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
632 |
apsnd (cons (ax, old_weight))) |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
633 |
|>> append (more_rejects |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
634 |
|> map (fn (ax as (_, consts), old_weight) => |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
635 |
(ax, if exists is_dirty consts then NONE |
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
636 |
else SOME old_weight))) |
38747 | 637 |
val threshold = |
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset
|
638 |
1.0 - (1.0 - threshold) |
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset
|
639 |
* Math.pow (decay, Real.fromInt (length accepts)) |
38747 | 640 |
val remaining_max = remaining_max - length accepts |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
641 |
in |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
642 |
trace_msg ctxt (fn () => "New or updated constants: " ^ |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
643 |
commas (rel_const_tab' |> Symtab.dest |
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset
|
644 |
|> subtract (op =) (rel_const_tab |> Symtab.dest) |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
645 |
|> map string_for_hyper_pconst)); |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
646 |
map (fst o fst) accepts @ |
38747 | 647 |
(if remaining_max = 0 then |
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset
|
648 |
[] |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
649 |
else |
38747 | 650 |
iter (j + 1) remaining_max threshold rel_const_tab' |
651 |
hopeless_rejects hopeful_rejects) |
|
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
652 |
end |
38889 | 653 |
| relevant candidates rejects |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
654 |
(((ax as (((_, loc), _), fact_consts)), cached_weight) |
38747 | 655 |
:: hopeful) = |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
656 |
let |
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
657 |
val weight = |
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
658 |
case cached_weight of |
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
659 |
SOME w => w |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
660 |
| NONE => fact_weight fudge loc const_tab rel_const_tab |
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset
|
661 |
chained_const_tab fact_consts |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
662 |
in |
38741 | 663 |
if weight >= threshold then |
38889 | 664 |
relevant ((ax, weight) :: candidates) rejects hopeful |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
665 |
else |
38889 | 666 |
relevant candidates ((ax, weight) :: rejects) hopeful |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
667 |
end |
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
668 |
in |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
669 |
trace_msg ctxt (fn () => |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
670 |
"ITERATION " ^ string_of_int j ^ ": current threshold: " ^ |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
671 |
Real.toString threshold ^ ", constants: " ^ |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
672 |
commas (rel_const_tab |> Symtab.dest |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
673 |
|> filter (curry (op <>) [] o snd) |
38827
cf01645cbbce
extended relevance filter with first-order term matching
blanchet
parents:
38825
diff
changeset
|
674 |
|> map string_for_hyper_pconst)); |
38889 | 675 |
relevant [] [] hopeful |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
676 |
end |
42826
be0e66ccebfa
append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
blanchet
parents:
42812
diff
changeset
|
677 |
fun prepend_facts ths accepts = |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
678 |
((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ |
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
679 |
(accepts |> filter_out (member Thm.eq_thm_prop ths o snd))) |
40408 | 680 |
|> take max_relevant |
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
681 |
fun uses_const s t = |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
682 |
fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t |
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset
|
683 |
false |
43066
e0d4841c5b4a
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents:
42957
diff
changeset
|
684 |
fun add_set_const_thms accepts (s, ths) = |
e0d4841c5b4a
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents:
42957
diff
changeset
|
685 |
if exists (uses_const s o prop_of o snd) accepts orelse |
e0d4841c5b4a
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents:
42957
diff
changeset
|
686 |
exists (uses_const s) (concl_t :: hyp_ts) then |
e0d4841c5b4a
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents:
42957
diff
changeset
|
687 |
append ths |
e0d4841c5b4a
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents:
42957
diff
changeset
|
688 |
else |
e0d4841c5b4a
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents:
42957
diff
changeset
|
689 |
I |
43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
690 |
fun insert_into_facts accepts [] = accepts |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
691 |
| insert_into_facts accepts ths = |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
692 |
let |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
693 |
val add = facts |> filter (member Thm.eq_thm_prop ths o snd) |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
694 |
val (bef, after) = |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
695 |
accepts |> filter_out (member Thm.eq_thm_prop ths o snd) |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
696 |
|> take (max_relevant - length add) |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
697 |
|> chop special_fact_index |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
698 |
in bef @ add @ after end |
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
699 |
fun insert_special_facts accepts = |
43066
e0d4841c5b4a
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents:
42957
diff
changeset
|
700 |
[] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext} |
e0d4841c5b4a
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents:
42957
diff
changeset
|
701 |
|> fold (add_set_const_thms accepts) set_consts |
43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
702 |
|> insert_into_facts accepts |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
703 |
in |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40251
diff
changeset
|
704 |
facts |> map_filter (pair_consts_fact thy is_built_in_const fudge) |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
705 |
|> iter 0 max_relevant threshold0 goal_const_tab [] |
42826
be0e66ccebfa
append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
blanchet
parents:
42812
diff
changeset
|
706 |
|> not (null add_ths) ? prepend_facts add_ths |
43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset
|
707 |
|> insert_special_facts |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
708 |
|> tap (fn accepts => trace_msg ctxt (fn () => |
41491 | 709 |
"Total relevant: " ^ string_of_int (length accepts))) |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
710 |
end |
24287 | 711 |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
712 |
|
24287 | 713 |
(***************************************************************) |
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset
|
714 |
(* Retrieving and filtering lemmas *) |
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset
|
715 |
(***************************************************************) |
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset
|
716 |
|
33022
c95102496490
Removal of the unused atpset concept, the atp attribute and some related code.
paulson
parents:
32994
diff
changeset
|
717 |
(*** retrieve lemmas and filter them ***) |
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset
|
718 |
|
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset
|
719 |
(*Reject theorems with names like "List.filter.filter_list_def" or |
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset
|
720 |
"Accessible_Part.acc.defs", as these are definitions arising from packages.*) |
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset
|
721 |
fun is_package_def a = |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
722 |
let val names = Long_Name.explode a in |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
723 |
(length names > 2 andalso not (hd names = "local") andalso |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
724 |
String.isSuffix "_def" a) orelse String.isSuffix "_defs" a |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
725 |
end |
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset
|
726 |
|
43245 | 727 |
fun uniquify xs = |
728 |
Termtab.fold (cons o snd) |
|
729 |
(fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) [] |
|
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset
|
730 |
|
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
731 |
(* FIXME: put other record thms here, or declare as "no_atp" *) |
44585 | 732 |
fun multi_base_blacklist ctxt ho_atp = |
41199 | 733 |
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", |
734 |
"cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", |
|
735 |
"weak_case_cong"] |
|
44585 | 736 |
|> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? |
737 |
append ["induct", "inducts"] |
|
38682 | 738 |
|> map (prefix ".") |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
739 |
|
44585 | 740 |
val max_lambda_nesting = 3 (*only applies if not ho_atp*) |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
741 |
|
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
742 |
fun term_has_too_many_lambdas max (t1 $ t2) = |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
743 |
exists (term_has_too_many_lambdas max) [t1, t2] |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
744 |
| term_has_too_many_lambdas max (Abs (_, _, t)) = |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
745 |
max = 0 orelse term_has_too_many_lambdas (max - 1) t |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
746 |
| term_has_too_many_lambdas _ _ = false |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
747 |
|
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
748 |
(* Don't count nested lambdas at the level of formulas, since they are |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
749 |
quantifiers. *) |
44585 | 750 |
fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*) |
751 |
| formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) = |
|
752 |
formula_has_too_many_lambdas false (T :: Ts) t |
|
753 |
| formula_has_too_many_lambdas _ Ts t = |
|
41273
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset
|
754 |
if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then |
44585 | 755 |
exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t)) |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
756 |
else |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
757 |
term_has_too_many_lambdas max_lambda_nesting t |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
758 |
|
38692 | 759 |
(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31) |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
760 |
was 11. *) |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
761 |
val max_apply_depth = 15 |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
762 |
|
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
763 |
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
764 |
| apply_depth (Abs (_, _, t)) = apply_depth t |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
765 |
| apply_depth _ = 0 |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
766 |
|
44585 | 767 |
fun is_formula_too_complex ho_atp t = |
768 |
apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t |
|
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
769 |
|
39946 | 770 |
(* FIXME: Extend to "Meson" and "Metis" *) |
37543 | 771 |
val exists_sledgehammer_const = |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
772 |
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
773 |
|
38904 | 774 |
(* FIXME: make more reliable *) |
775 |
val exists_low_level_class_const = |
|
776 |
exists_Const (fn (s, _) => |
|
777 |
String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) |
|
778 |
||
38821 | 779 |
fun is_metastrange_theorem th = |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
780 |
case head_of (concl_of th) of |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
781 |
Const (s, _) => (s <> @{const_name Trueprop} andalso |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
782 |
s <> @{const_name "=="}) |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
783 |
| _ => false |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
784 |
|
38821 | 785 |
fun is_that_fact th = |
786 |
String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) |
|
787 |
andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN |
|
788 |
| _ => false) (prop_of th) |
|
789 |
||
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset
|
790 |
(**** Predicates to detect unwanted facts (prolific or likely to cause |
37347
635425a442e8
show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset
|
791 |
unsoundness) ****) |
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset
|
792 |
|
44585 | 793 |
fun is_theorem_bad_for_atps ho_atp exporter thm = |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
794 |
is_metastrange_theorem thm orelse |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
795 |
(not exporter andalso |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
796 |
let val t = prop_of thm in |
44585 | 797 |
is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
798 |
exists_sledgehammer_const t orelse exists_low_level_class_const t orelse |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
799 |
is_that_fact thm |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
800 |
end) |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
801 |
|
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
802 |
fun meta_equify (@{const Trueprop} |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
803 |
$ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) = |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
804 |
Const (@{const_name "=="}, T --> T --> @{typ prop}) $ t1 $ t2 |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
805 |
| meta_equify t = t |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
806 |
|
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
807 |
val normalize_simp_prop = |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
808 |
meta_equify |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
809 |
#> map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t) |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
810 |
#> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S))) |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
811 |
|
43245 | 812 |
fun clasimpset_rule_table_of ctxt = |
38937
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset
|
813 |
let |
43245 | 814 |
fun add loc g f = fold (Termtab.update o rpair loc o g o prop_of o f) |
42812 | 815 |
val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs |
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42741
diff
changeset
|
816 |
val intros = Item_Net.content safeIs @ Item_Net.content hazIs |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42741
diff
changeset
|
817 |
val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs) |
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
818 |
val simps = ctxt |> simpset_of |> dest_ss |> #simps |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
819 |
in |
43245 | 820 |
Termtab.empty |> add Intro I I intros |
821 |
|> add Elim I I elims |
|
822 |
|> add Simp I snd simps |
|
823 |
|> add Simp normalize_simp_prop snd simps |
|
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
824 |
end |
38937
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset
|
825 |
|
44585 | 826 |
fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths = |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
827 |
let |
42361 | 828 |
val thy = Proof_Context.theory_of ctxt |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39367
diff
changeset
|
829 |
val global_facts = Global_Theory.facts_of thy |
42361 | 830 |
val local_facts = Proof_Context.facts_of ctxt |
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents:
38629
diff
changeset
|
831 |
val named_locals = local_facts |> Facts.dest_static [] |
38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset
|
832 |
val assms = Assumption.all_assms_of ctxt |
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset
|
833 |
fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
834 |
val is_chained = member Thm.eq_thm_prop chained_ths |
43245 | 835 |
val clasimpset_table = clasimpset_rule_table_of ctxt |
44585 | 836 |
fun locality_of_theorem global (name: string) th = |
44586 | 837 |
if String.isSubstring ".induct" name orelse(*FIXME: use structured name*) |
838 |
String.isSubstring ".inducts" name then |
|
44585 | 839 |
Induction |
840 |
else if is_chained th then |
|
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
841 |
Chained |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
842 |
else if global then |
43421 | 843 |
case Termtab.lookup clasimpset_table (prop_of th) of |
844 |
SOME loc => loc |
|
44783 | 845 |
| NONE => General |
44585 | 846 |
else if is_assum th then Assum else Local |
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents:
38699
diff
changeset
|
847 |
fun is_good_unnamed_local th = |
38820
d0f98bd81a85
add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents:
38819
diff
changeset
|
848 |
not (Thm.has_name_hint th) andalso |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
849 |
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals |
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents:
38629
diff
changeset
|
850 |
val unnamed_locals = |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
851 |
union Thm.eq_thm_prop (Facts.props local_facts) chained_ths |
38820
d0f98bd81a85
add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents:
38819
diff
changeset
|
852 |
|> filter is_good_unnamed_local |> map (pair "" o single) |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
853 |
val full_space = |
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents:
38699
diff
changeset
|
854 |
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset
|
855 |
fun add_facts global foldx facts = |
38699 | 856 |
foldx (fn (name0, ths) => |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
857 |
if not exporter andalso name0 <> "" andalso |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
858 |
forall (not o member Thm.eq_thm_prop add_ths) ths andalso |
38699 | 859 |
(Facts.is_concealed facts name0 orelse |
42728
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
860 |
(not (Config.get ctxt ignore_no_atp) andalso |
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
861 |
is_package_def name0) orelse |
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
862 |
exists (fn s => String.isSuffix s name0) |
44585 | 863 |
(multi_base_blacklist ctxt ho_atp) orelse |
38699 | 864 |
String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
865 |
I |
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
866 |
else |
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
867 |
let |
38699 | 868 |
val multi = length ths > 1 |
41279 | 869 |
val backquote_thm = |
870 |
backquote o string_for_term ctxt o close_form o prop_of |
|
38699 | 871 |
fun check_thms a = |
42361 | 872 |
case try (Proof_Context.get_thms ctxt) a of |
38699 | 873 |
NONE => false |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
874 |
| SOME ths' => eq_list Thm.eq_thm_prop (ths, ths') |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
875 |
in |
38699 | 876 |
pair 1 |
43245 | 877 |
#> fold (fn th => fn (j, (multis, unis)) => |
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
878 |
(j + 1, |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
879 |
if not (member Thm.eq_thm_prop add_ths th) andalso |
44585 | 880 |
is_theorem_bad_for_atps ho_atp exporter th then |
43245 | 881 |
(multis, unis) |
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
882 |
else |
43245 | 883 |
let |
884 |
val new = |
|
885 |
(((fn () => |
|
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
886 |
if name0 = "" then |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
887 |
th |> backquote_thm |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
888 |
else |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
889 |
[Facts.extern ctxt facts name0, |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
890 |
Name_Space.extern ctxt full_space name0, |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
891 |
name0] |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
892 |
|> find_first check_thms |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
893 |
|> (fn SOME name => |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
894 |
make_name reserved multi j name |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
895 |
| NONE => "")), |
44585 | 896 |
locality_of_theorem global name0 th), th) |
43245 | 897 |
in |
898 |
if multi then (new :: multis, unis) |
|
899 |
else (multis, new :: unis) |
|
900 |
end)) ths |
|
38699 | 901 |
#> snd |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
902 |
end) |
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents:
38629
diff
changeset
|
903 |
in |
43245 | 904 |
(* The single-name theorems go after the multiple-name ones, so that single |
905 |
names are preferred when both are available. *) |
|
906 |
([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals) |
|
907 |
|> add_facts true Facts.fold_static global_facts global_facts |
|
908 |
|> op @ |
|
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents:
38629
diff
changeset
|
909 |
end |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
910 |
|
41199 | 911 |
fun external_frees t = |
912 |
[] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) |
|
913 |
||
44585 | 914 |
fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override) |
915 |
chained_ths hyp_ts concl_t = |
|
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:
43324
diff
changeset
|
916 |
let |
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:
43324
diff
changeset
|
917 |
val thy = Proof_Context.theory_of ctxt |
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:
43324
diff
changeset
|
918 |
val reserved = reserved_isar_keyword_table () |
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:
43324
diff
changeset
|
919 |
val add_ths = Attrib.eval_thms ctxt add |
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:
43324
diff
changeset
|
920 |
val ind_stmt = |
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:
43324
diff
changeset
|
921 |
Logic.list_implies (hyp_ts |> filter_out (null o external_frees), 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:
43324
diff
changeset
|
922 |
|> Object_Logic.atomize_term thy |
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:
43324
diff
changeset
|
923 |
val ind_stmt_xs = external_frees ind_stmt |
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:
43324
diff
changeset
|
924 |
in |
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:
43324
diff
changeset
|
925 |
(if only then |
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:
43324
diff
changeset
|
926 |
maps (map (fn ((name, loc), th) => ((K name, loc), th)) |
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:
43324
diff
changeset
|
927 |
o fact_from_ref ctxt reserved chained_ths) add |
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:
43324
diff
changeset
|
928 |
else |
44585 | 929 |
all_facts ctxt ho_atp reserved false add_ths chained_ths) |
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:
43324
diff
changeset
|
930 |
|> Config.get ctxt instantiate_inducts |
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:
43324
diff
changeset
|
931 |
? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) |
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:
43324
diff
changeset
|
932 |
|> (not (Config.get ctxt ignore_no_atp) andalso not only) |
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:
43324
diff
changeset
|
933 |
? filter_out (No_ATPs.member ctxt o snd) |
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:
43324
diff
changeset
|
934 |
|> uniquify |
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:
43324
diff
changeset
|
935 |
end |
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:
43324
diff
changeset
|
936 |
|
44625 | 937 |
fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const |
938 |
fudge (override as {only, ...}) chained_ths hyp_ts concl_t |
|
939 |
facts = |
|
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset
|
940 |
let |
42361 | 941 |
val thy = Proof_Context.theory_of ctxt |
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset
|
942 |
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), |
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset
|
943 |
1.0 / Real.fromInt (max_relevant + 1)) |
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset
|
944 |
in |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
945 |
trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset
|
946 |
" facts"); |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39265
diff
changeset
|
947 |
(if only orelse threshold1 < 0.0 then |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40191
diff
changeset
|
948 |
facts |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39265
diff
changeset
|
949 |
else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse |
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39265
diff
changeset
|
950 |
max_relevant = 0 then |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
951 |
[] |
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
952 |
else |
44625 | 953 |
relevance_filter ctxt threshold0 decay max_relevant is_built_in_const |
954 |
fudge override facts (chained_ths |> map prop_of) hyp_ts |
|
955 |
(concl_t |> theory_constify fudge (Context.theory_name thy))) |
|
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset
|
956 |
|> map (apfst (apfst (fn f => f ()))) |
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset
|
957 |
end |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30364
diff
changeset
|
958 |
|
15347 | 959 |
end; |