author  blanchet 
Mon, 02 Jan 2012 14:32:20 +0100  
changeset 46073  b2594cc862d7 
parent 45982  989b1eede03c 
child 46217  7b19666f0e3d 
permissions  rwrr 
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
finetuned 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 Sledgehammerrelated 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 userspecified 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 builtin 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 etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38644
diff
changeset

67 
open Sledgehammer_Util 
e063be321438
perform etaexpansion 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 firstorder 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
finetuned 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 nonidentifierlike 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 nonidentifierlike 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 nonidentifierlike 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 

45034  152 
(* This is a terrible hack. Free variables are sometimes coded as "M__" when 
153 
they are displayed as "M" and we want to avoid clashes with these. But 

154 
sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all 

155 
prefixes of all free variables. In the worse case scenario, where the fact 

156 
won't be resolved correctly, the user can fix it manually, e.g., by naming 

157 
the fact in question. Ideally we would need nothing of it, but backticks 

158 
simply don't work with schematic variables. *) 

41199  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 oldstyle / 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 

46073
b2594cc862d7
removed special handling for set constants in relevance filter
blanchet
parents:
45982
diff
changeset

226 
fun order_of_type (Type (@{type_name fun}, [T1, T2])) = 
38939  227 
Int.max (order_of_type T1 + 1, order_of_type T2) 
228 
 order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0 

229 
 order_of_type _ = 0 

230 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

231 
(* An abstraction of Isabelle types and firstorder terms *) 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

232 
datatype pattern = PVar  PApp of string * pattern list 
38939  233 
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

234 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

235 
fun string_for_pattern PVar = "_" 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

236 
 string_for_pattern (PApp (s, ps)) = 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

237 
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

238 
and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" 
38939  239 
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps 
24287  240 

241 
(*Is the second type an instance of the first one?*) 

38824  242 
fun match_pattern (PVar, _) = true 
243 
 match_pattern (PApp _, PVar) = false 

244 
 match_pattern (PApp (s, ps), PApp (t, qs)) = 

245 
s = t andalso match_patterns (ps, qs) 

246 
and match_patterns (_, []) = true 

247 
 match_patterns ([], _) = false 

248 
 match_patterns (p :: ps, q :: qs) = 

249 
match_pattern (p, q) andalso match_patterns (ps, qs) 

38939  250 
fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs) 
24287  251 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

252 
(* Is there a unifiable constant? *) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

253 
fun pconst_mem f consts (s, ps) = 
38939  254 
exists (curry (match_ptype o f) ps) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

255 
(map snd (filter (curry (op =) s o fst) consts)) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

256 
fun pconst_hyper_mem f const_tab (s, ps) = 
38939  257 
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 (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

258 

38939  259 
fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts) 
260 
 pattern_for_type (TFree (s, _)) = PApp (s, []) 

261 
 pattern_for_type (TVar _) = PVar 

38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

262 

38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

263 
(* 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

264 
fun ptype thy const x = 
38939  265 
(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

266 
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

267 
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

268 
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

269 
fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T)) 
24287  270 

38939  271 
fun string_for_hyper_pconst (s, ps) = 
272 
s ^ "{" ^ commas (map string_for_ptype ps) ^ "}" 

24287  273 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

274 
(* 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

275 
connective, which we ignore.*) 
41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

276 
fun add_pconst_to_table also_skolem (s, p) = 
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

277 
if (not also_skolem andalso String.isPrefix skolem_prefix s) then I 
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

278 
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

279 

42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

280 
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 (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

281 
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

282 
val flip = Option.map not 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

283 
(* We include free variables, as well as constants, to handle locales. For 
41205  284 
each quantifiers that must necessarily be skolemized by the automatic 
285 
prover, we introduce a fresh constant to simulate the effect of 

286 
Skolemization. *) 

46073
b2594cc862d7
removed special handling for set constants in relevance filter
blanchet
parents:
45982
diff
changeset

287 
fun do_const const x 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

288 
let val (built_in, ts) = is_built_in_const x ts in 
46073
b2594cc862d7
removed special handling for set constants in relevance filter
blanchet
parents:
45982
diff
changeset

289 
(not built_in 
b2594cc862d7
removed special handling for set constants in relevance filter
blanchet
parents:
45982
diff
changeset

290 
? add_pconst_to_table also_skolems (rich_pconst thy const x)) 
b2594cc862d7
removed special handling for set constants in relevance filter
blanchet
parents:
45982
diff
changeset

291 
#> 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

292 
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

293 
and do_term ext_arg t = 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

294 
case strip_comb t of 
46073
b2594cc862d7
removed special handling for set constants in relevance filter
blanchet
parents:
45982
diff
changeset

295 
(Const x, ts) => do_const true x ts 
b2594cc862d7
removed special handling for set constants in relevance filter
blanchet
parents:
45982
diff
changeset

296 
 (Free x, ts) => do_const false x ts 
38939  297 
 (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

298 
((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

299 
(* Since lambdas on the righthand 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

300 
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

301 
them here. *) 
41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

302 
? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, []))) 
42735
1d375de437e9
finetuned 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

303 
#> fold (do_term false) (t' :: ts) 
1d375de437e9
finetuned 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

304 
 (_, ts) => fold (do_term false) ts 
38939  305 
fun do_quantifier will_surely_be_skolemized abs_T body_t = 
37537  306 
do_formula pos body_t 
38747  307 
#> (if also_skolems andalso will_surely_be_skolemized then 
41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

308 
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

309 
(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

310 
else 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

311 
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

312 
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

313 
if T = HOLogic.boolT then do_formula NONE else do_term ext_arg 
37537  314 
and do_formula pos t = 
315 
case t of 

38939  316 
Const (@{const_name all}, _) $ Abs (_, T, t') => 
317 
do_quantifier (pos = SOME false) T t' 

37537  318 
 @{const "==>"} $ t1 $ t2 => 
319 
do_formula (flip pos) t1 #> do_formula pos t2 

320 
 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

321 
do_term_or_formula false T t1 #> do_term_or_formula true T t2 
37537  322 
 @{const Trueprop} $ t1 => do_formula pos t1 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

323 
 @{const False} => I 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

324 
 @{const True} => I 
37537  325 
 @{const Not} $ t1 => do_formula (flip pos) t1 
38939  326 
 Const (@{const_name All}, _) $ Abs (_, T, t') => 
327 
do_quantifier (pos = SOME false) T t' 

328 
 Const (@{const_name Ex}, _) $ Abs (_, T, t') => 

329 
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

330 
 @{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

331 
 @{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

332 
 @{const HOL.implies} $ t1 $ t2 => 
37537  333 
do_formula (flip pos) t1 #> do_formula pos t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

334 
 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

335 
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

336 
 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

337 
$ t1 $ t2 $ t3 => 
42735
1d375de437e9
finetuned 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

338 
do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3] 
38939  339 
 Const (@{const_name Ex1}, _) $ Abs (_, T, t') => 
340 
do_quantifier (is_some pos) T t' 

341 
 Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') => 

342 
do_quantifier (pos = SOME false) T 

343 
(HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t')) 

344 
 Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') => 

345 
do_quantifier (pos = SOME true) T 

346 
(HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t')) 

37537  347 
 (t0 as Const (_, @{typ bool})) $ t1 => 
42735
1d375de437e9
finetuned 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

348 
do_term false t0 #> do_formula pos t1 (* theory constant *) 
1d375de437e9
finetuned 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

349 
 _ => do_term false t 
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

350 
in do_formula pos end 
24287  351 

352 
(*Inserts a dummy "constant" referring to the theory name, so that relevance 

353 
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

354 
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

355 
: relevance_fudge) thy_name t = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

356 
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

357 
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

358 
Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

359 
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

360 
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

361 

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

362 
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

363 
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 (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

364 

24287  365 
(**** Constant / Type Frequencies ****) 
366 

38743  367 
(* A twodimensional symbol table counts frequencies of constants. It's keyed 
368 
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

369 
latter, we need a linear ordering on "pattern list". *) 
24287  370 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

371 
fun pattern_ord p = 
38743  372 
case p of 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

373 
(PVar, PVar) => EQUAL 
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

374 
 (PVar, PApp _) => LESS 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

375 
 (PApp _, PVar) => GREATER 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

376 
 (PApp q1, PApp q2) => 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

377 
prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2) 
38939  378 
fun ptype_ord (PType p, PType q) = 
379 
prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q) 

24287  380 

38939  381 
structure PType_Tab = Table(type key = ptype val ord = ptype_ord) 
24287  382 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

383 
fun count_fact_consts thy fudge = 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

384 
let 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

385 
fun do_const const (s, T) ts = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

386 
(* Twodimensional 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

387 
PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1) 
38939  388 
> Symtab.map_default (s, PType_Tab.empty) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

389 
#> fold do_term ts 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

390 
and do_term t = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

391 
case strip_comb t of 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

392 
(Const x, ts) => do_const true x ts 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

393 
 (Free x, ts) => do_const false x ts 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

394 
 (Abs (_, _, t'), ts) => fold do_term (t' :: ts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

395 
 (_, ts) => fold do_term ts 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

396 
in do_term o theory_const_prop_of fudge o snd end 
24287  397 

398 

399 
(**** Actual Filtering Code ****) 

400 

39367  401 
fun pow_int _ 0 = 1.0 
38939  402 
 pow_int x 1 = x 
403 
 pow_int x n = if n > 0 then x * pow_int x (n  1) else pow_int x (n + 1) / x 

404 

24287  405 
(*The frequency of a constant is the sum of those of all instances of its type.*) 
38824  406 
fun pconst_freq match const_tab (c, ps) = 
38939  407 
PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m) 
408 
(the (Symtab.lookup const_tab c)) 0 

38686  409 

24287  410 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

411 
(* 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

412 
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

413 

c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

414 
(* "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

415 
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

416 
rare ones. *) 
39367  417 
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

418 

2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

419 
(* 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

420 
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

421 
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

422 
so common as to be of little interest. *) 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

423 
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

424 
: relevance_fudge) order freq = 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

425 
let val (k, x) = worse_irrel_freq > `Real.ceil in 
38939  426 
(if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x 
427 
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

428 
* pow_int higher_order_irrel_weight (order  1) 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

429 
end 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

430 

41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

431 
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

432 
if String.isSubstring "." s then 1.0 else local_const_multiplier 
38821  433 

41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

434 
(* 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

435 
fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight 
42735
1d375de437e9
finetuned 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

436 
theory_const_weight chained_const_weight weight_for f 
1d375de437e9
finetuned 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

437 
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

438 
if s = abs_name then 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

439 
abs_weight 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

440 
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

441 
skolem_weight 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

442 
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

443 
theory_const_weight 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

444 
else 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

445 
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 
* weight_for m (pconst_freq (match_ptype o f) const_tab c) 
42735
1d375de437e9
finetuned 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

447 
> (if chained_const_weight < 1.0 andalso 
1d375de437e9
finetuned 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

448 
pconst_hyper_mem I chained_const_tab c then 
1d375de437e9
finetuned 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

449 
curry (op *) chained_const_weight 
1d375de437e9
finetuned 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 
else 
1d375de437e9
finetuned 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 
I) 
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

452 

56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

453 
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

454 
theory_const_rel_weight, ...} : relevance_fudge) 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

455 
const_tab = 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

456 
generic_pconst_weight local_const_multiplier abs_rel_weight 0.0 
42735
1d375de437e9
finetuned 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

457 
theory_const_rel_weight 0.0 rel_weight_for I const_tab 
1d375de437e9
finetuned 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

458 
Symtab.empty 
1d375de437e9
finetuned 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

459 

41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

460 
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

461 
skolem_irrel_weight, 
42735
1d375de437e9
finetuned 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 
theory_const_irrel_weight, 
1d375de437e9
finetuned 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 
chained_const_irrel_weight, ...}) 
1d375de437e9
finetuned 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 
const_tab chained_const_tab = 
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

465 
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

466 
skolem_irrel_weight theory_const_irrel_weight 
42735
1d375de437e9
finetuned 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

467 
chained_const_irrel_weight (irrel_weight_for fudge) swap 
1d375de437e9
finetuned 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

468 
const_tab chained_const_tab 
24287  469 

43421  470 
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

471 
 locality_bonus {elim_bonus, ...} Elim = elim_bonus 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

472 
 locality_bonus {simp_bonus, ...} Simp = simp_bonus 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

473 
 locality_bonus {local_bonus, ...} Local = local_bonus 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

474 
 locality_bonus {assum_bonus, ...} Assum = assum_bonus 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

475 
 locality_bonus {chained_bonus, ...} Chained = chained_bonus 
43421  476 
 locality_bonus _ _ = 0.0 
38751
01c4d14b2a61
add a bonus for chained facts, since they are likely to be relevant;
blanchet
parents:
38749
diff
changeset

477 

40418  478 
fun is_odd_const_name s = 
479 
s = abs_name orelse String.isPrefix skolem_prefix s orelse 

480 
String.isSuffix theory_const_suffix s 

481 

42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

482 
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 lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

483 
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 lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

484 
> filter_out (pconst_hyper_mem swap relevant_consts) of 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

485 
([], _) => 0.0 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

486 
 (rel, irrel) => 
40418  487 
if forall (forall (is_odd_const_name o fst)) [rel, irrel] then 
40371  488 
0.0 
489 
else 

490 
let 

42735
1d375de437e9
finetuned 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

491 
val irrel = irrel > filter_out (pconst_mem swap rel) 
40371  492 
val rel_weight = 
493 
0.0 > fold (curry (op +) o rel_pconst_weight fudge const_tab) rel 

494 
val irrel_weight = 

495 
~ (locality_bonus fudge loc) 

42735
1d375de437e9
finetuned 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

496 
> fold (curry (op +) 
1d375de437e9
finetuned 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

497 
o irrel_pconst_weight fudge const_tab chained_consts) irrel 
40371  498 
val res = rel_weight / (rel_weight + irrel_weight) 
499 
in if Real.isFinite res then res else 0.0 end 

38747  500 

40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

501 
fun pconsts_in_fact thy is_built_in_const t = 
38825  502 
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

503 
(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

504 
(SOME true) t) [] 
42729  505 

40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

506 
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 lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

507 
case fact > snd > theory_const_prop_of fudge 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

508 
> pconsts_in_fact thy is_built_in_const of 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

509 
[] => NONE 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

510 
 consts => SOME ((fact, consts), NONE) 
24287  511 

41768
dd2125fb75f9
export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents:
41767
diff
changeset

512 
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

513 

38699  514 
type annotated_thm = 
38939  515 
(((unit > string) * locality) * thm) * (string * ptype) list 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

516 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

517 
fun take_most_relevant ctxt max_relevant remaining_max 
42728
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset

518 
({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

519 
(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

520 
let 
38747  521 
val max_imperfect = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

522 
Real.ceil (Math.pow (max_imperfect, 
38904  523 
Math.pow (Real.fromInt remaining_max 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

524 
/ Real.fromInt max_relevant, max_imperfect_exp))) 
38747  525 
val (perfect, imperfect) = 
38889  526 
candidates > sort (Real.compare o swap o pairself snd) 
527 
> take_prefix (fn (_, w) => w > 0.99999) 

38747  528 
val ((accepts, more_rejects), rejects) = 
529 
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

530 
in 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

531 
trace_msg ctxt (fn () => 
41491  532 
"Actually passed (" ^ string_of_int (length accepts) ^ " of " ^ 
533 
string_of_int (length candidates) ^ "): " ^ 

38889  534 
(accepts > map (fn ((((name, _), _), _), weight) => 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

535 
name () ^ " [" ^ Real.toString weight ^ "]") 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

536 
> commas)); 
38747  537 
(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

538 
end 
24287  539 

40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

540 
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

541 
if Symtab.is_empty tab then 
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

542 
Symtab.empty 
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

543 
> 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

544 
(map_filter (fn ((_, loc'), th) => 
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

545 
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

546 
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

547 
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

548 
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

549 

42702  550 
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

551 
let 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

552 
fun aux _ _ NONE = NONE 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

553 
 aux t args (SOME tab) = 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

554 
case t of 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

555 
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

556 
 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

557 
(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

558 
SOME tab 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

559 
else case Symtab.lookup tab s of 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

560 
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

561 
 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

562 
 _ => SOME tab 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

563 
in aux (prop_of th) [] end 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

564 

44785  565 
(* FIXME: This is currently only useful for polymorphic type encodings. *) 
42702  566 
fun could_benefit_from_ext is_built_in_const facts = 
567 
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

568 
> is_none 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

569 

43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

570 
(* 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

571 
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

572 
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

573 
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

574 

44625  575 
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

576 
(fudge as {threshold_divisor, ridiculous_threshold, ...}) 
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

577 
({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

578 
let 
42361  579 
val thy = Proof_Context.theory_of ctxt 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

580 
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

581 
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

582 
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

583 
val goal_const_tab = 
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

584 
Symtab.empty > fold (add_pconsts true) hyp_ts 
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

585 
> add_pconsts false concl_t 
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

586 
> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab) 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

587 
> 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

588 
[Chained, Assum, Local] 
39012  589 
val add_ths = Attrib.eval_thms ctxt add 
590 
val del_ths = Attrib.eval_thms ctxt del 

42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison  ensures that backtickquoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset

591 
val facts = facts > filter_out (member Thm.eq_thm_prop del_ths o snd) 
38747  592 
fun iter j remaining_max threshold rel_const_tab hopeless hopeful = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

593 
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

594 
fun relevant [] _ [] = 
38747  595 
(* Nothing has been added this iteration. *) 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

596 
if j = 0 andalso threshold >= ridiculous_threshold then 
38747  597 
(* First iteration? Try again. *) 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

598 
iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab 
38747  599 
hopeless hopeful 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

600 
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

601 
[] 
38889  602 
 relevant candidates rejects [] = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

603 
let 
38747  604 
val (accepts, more_rejects) = 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

605 
take_most_relevant ctxt max_relevant remaining_max fudge 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

606 
candidates 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

607 
val rel_const_tab' = 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

608 
rel_const_tab 
41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

609 
> 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

610 
fun is_dirty (c, _) = 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

611 
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

612 
val (hopeful_rejects, hopeless_rejects) = 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

613 
(rejects @ hopeless, ([], [])) 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

614 
> fold (fn (ax as (_, consts), old_weight) => 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

615 
if exists is_dirty consts then 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

616 
apfst (cons (ax, NONE)) 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

617 
else 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

618 
apsnd (cons (ax, old_weight))) 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

619 
>> append (more_rejects 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

620 
> map (fn (ax as (_, consts), old_weight) => 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

621 
(ax, if exists is_dirty consts then NONE 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

622 
else SOME old_weight))) 
38747  623 
val threshold = 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

624 
1.0  (1.0  threshold) 
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

625 
* Math.pow (decay, Real.fromInt (length accepts)) 
38747  626 
val remaining_max = remaining_max  length accepts 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

627 
in 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

628 
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

629 
commas (rel_const_tab' > Symtab.dest 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

630 
> subtract (op =) (rel_const_tab > Symtab.dest) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

631 
> map string_for_hyper_pconst)); 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

632 
map (fst o fst) accepts @ 
38747  633 
(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

634 
[] 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

635 
else 
38747  636 
iter (j + 1) remaining_max threshold rel_const_tab' 
637 
hopeless_rejects hopeful_rejects) 

38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

638 
end 
38889  639 
 relevant candidates rejects 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

640 
(((ax as (((_, loc), _), fact_consts)), cached_weight) 
38747  641 
:: hopeful) = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

642 
let 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

643 
val weight = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

644 
case cached_weight of 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

645 
SOME w => w 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

646 
 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

647 
chained_const_tab fact_consts 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

648 
in 
38741  649 
if weight >= threshold then 
38889  650 
relevant ((ax, weight) :: candidates) rejects hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

651 
else 
38889  652 
relevant candidates ((ax, weight) :: rejects) hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

653 
end 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

654 
in 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

655 
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

656 
"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

657 
Real.toString threshold ^ ", constants: " ^ 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

658 
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

659 
> filter (curry (op <>) [] o snd) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

660 
> map string_for_hyper_pconst)); 
38889  661 
relevant [] [] hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

662 
end 
42826
be0e66ccebfa
append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
blanchet
parents:
42812
diff
changeset

663 
fun prepend_facts ths accepts = 
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison  ensures that backtickquoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset

664 
((facts > filter (member Thm.eq_thm_prop ths o snd)) @ 
c693f9b7674a
use "eq_thm_prop" for slacker comparison  ensures that backtickquoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset

665 
(accepts > filter_out (member Thm.eq_thm_prop ths o snd))) 
40408  666 
> take max_relevant 
43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

667 
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

668 
 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

669 
let 
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

670 
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

671 
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

672 
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

673 
> 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

674 
> 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

675 
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

676 
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

677 
[] > could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext} 
43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

678 
> insert_into_facts accepts 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

679 
in 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

680 
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 lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

681 
> 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

682 
> 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

683 
> insert_special_facts 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

684 
> tap (fn accepts => trace_msg ctxt (fn () => 
41491  685 
"Total relevant: " ^ string_of_int (length accepts))) 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

686 
end 
24287  687 

38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

688 

24287  689 
(***************************************************************) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

690 
(* Retrieving and filtering lemmas *) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

691 
(***************************************************************) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

692 

33022
c95102496490
Removal of the unused atpset concept, the atp attribute and some related code.
paulson
parents:
32994
diff
changeset

693 
(*** retrieve lemmas and filter them ***) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

694 

20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

695 
(*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

696 
"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

697 
fun is_package_def a = 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

698 
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

699 
(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

700 
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

701 
end 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

702 

43245  703 
fun uniquify xs = 
704 
Termtab.fold (cons o snd) 

705 
(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

706 

37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

707 
(* FIXME: put other record thms here, or declare as "no_atp" *) 
44585  708 
fun multi_base_blacklist ctxt ho_atp = 
41199  709 
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", 
710 
"cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", 

711 
"weak_case_cong"] 

44585  712 
> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? 
713 
append ["induct", "inducts"] 

38682  714 
> map (prefix ".") 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

715 

44585  716 
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

717 

1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

718 
fun term_has_too_many_lambdas max (t1 $ t2) = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

719 
exists (term_has_too_many_lambdas max) [t1, t2] 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

720 
 term_has_too_many_lambdas max (Abs (_, _, t)) = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

721 
max = 0 orelse term_has_too_many_lambdas (max  1) t 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

722 
 term_has_too_many_lambdas _ _ = false 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

723 

1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

724 
(* 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

725 
quantifiers. *) 
44585  726 
fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*) 
727 
 formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) = 

728 
formula_has_too_many_lambdas false (T :: Ts) t 

729 
 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

730 
if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then 
44585  731 
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

732 
else 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

733 
term_has_too_many_lambdas max_lambda_nesting t 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

734 

38692  735 
(* The max apply depth of any "metis" call in "Metis_Examples" (on 20071031) 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

736 
was 11. *) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

737 
val max_apply_depth = 15 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

738 

1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

739 
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

740 
 apply_depth (Abs (_, _, t)) = apply_depth t 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

741 
 apply_depth _ = 0 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

742 

44585  743 
fun is_formula_too_complex ho_atp t = 
744 
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

745 

39946  746 
(* FIXME: Extend to "Meson" and "Metis" *) 
37543  747 
val exists_sledgehammer_const = 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

748 
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

749 

38904  750 
(* FIXME: make more reliable *) 
751 
val exists_low_level_class_const = 

752 
exists_Const (fn (s, _) => 

753 
String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) 

754 

38821  755 
fun is_metastrange_theorem th = 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

756 
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

757 
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

758 
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

759 
 _ => false 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

760 

38821  761 
fun is_that_fact th = 
762 
String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) 

763 
andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN 

764 
 _ => false) (prop_of th) 

765 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

766 
(**** Predicates to detect unwanted facts (prolific or likely to cause 
37347
635425a442e8
show more respect for userspecified 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

767 
unsoundness) ****) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

768 

44585  769 
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

770 
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

771 
(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

772 
let val t = prop_of thm in 
44585  773 
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

774 
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

775 
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

776 
end) 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

777 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

778 
val crude_zero_vars = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

779 
map_aterms (fn Var ((s, _), T) => Var ((s, 0), T)  t => t) 
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

780 
#> 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

781 

43245  782 
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

783 
let 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

784 
val thy = Proof_Context.theory_of ctxt 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

785 
val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

786 
fun add loc g f = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

787 
fold (Termtab.update o rpair loc o g o crude_zero_vars o prop_of o f) 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

788 
val {safeIs, safeEs, hazIs, hazEs, ...} = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

789 
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

790 
val intros = Item_Net.content safeIs @ Item_Net.content hazIs 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

791 
val elims = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

792 
Item_Net.content safeEs @ Item_Net.content hazEs 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

793 
> map Classical.classical_rule 
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

794 
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

795 
in 
43245  796 
Termtab.empty > add Intro I I intros 
797 
> add Elim I I elims 

798 
> add Simp I snd simps 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

799 
> add Simp atomize 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

800 
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

801 

44585  802 
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

803 
let 
42361  804 
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 globalonly;
wenzelm
parents:
39367
diff
changeset

805 
val global_facts = Global_Theory.facts_of thy 
42361  806 
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

807 
val named_locals = local_facts > Facts.dest_static [] 
38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

808 
val assms = Assumption.all_assms_of ctxt 
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

809 
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 backtickquoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset

810 
val is_chained = member Thm.eq_thm_prop chained_ths 
43245  811 
val clasimpset_table = clasimpset_rule_table_of ctxt 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

812 
fun locality_of_theorem global name th = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

813 
if String.isSubstring ".induct" name orelse (*FIXME: use structured name*) 
44586  814 
String.isSubstring ".inducts" name then 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

815 
Induction 
44585  816 
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

817 
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

818 
else if global then 
43421  819 
case Termtab.lookup clasimpset_table (prop_of th) of 
820 
SOME loc => loc 

44783  821 
 NONE => General 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

822 
else if is_assum th then 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

823 
Assum 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

824 
else 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45034
diff
changeset

825 
Local 
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38699
diff
changeset

826 
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

827 
not (Thm.has_name_hint th) andalso 
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison  ensures that backtickquoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset

828 
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

829 
val unnamed_locals = 
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison  ensures that backtickquoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset

830 
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

831 
> 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

832 
val full_space = 
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38699
diff
changeset

833 
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

834 
fun add_facts global foldx facts = 
38699  835 
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

836 
if not exporter andalso name0 <> "" andalso 
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison  ensures that backtickquoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset

837 
forall (not o member Thm.eq_thm_prop add_ths) ths andalso 
38699  838 
(Facts.is_concealed facts name0 orelse 
42728
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset

839 
(not (Config.get ctxt ignore_no_atp) andalso 
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset

840 
is_package_def name0) orelse 
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset

841 
exists (fn s => String.isSuffix s name0) 
44585  842 
(multi_base_blacklist ctxt ho_atp) orelse 
38699  843 
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

844 
I 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

845 
else 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

846 
let 
38699  847 
val multi = length ths > 1 
41279  848 
val backquote_thm = 
849 
backquote o string_for_term ctxt o close_form o prop_of 

38699  850 
fun check_thms a = 
42361  851 
case try (Proof_Context.get_thms ctxt) a of 
38699  852 
NONE => false 
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison  ensures that backtickquoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset

853 
 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

854 
in 
38699  855 
pair 1 
43245  856 
#> 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

857 
(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

858 
if not (member Thm.eq_thm_prop add_ths th) andalso 
44585  859 
is_theorem_bad_for_atps ho_atp exporter th then 
43245  860 
(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

861 
else 
43245  862 
let 
863 
val new = 

864 
(((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

865 
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

866 
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

867 
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

868 
[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

869 
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

870 
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

871 
> 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

872 
> (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

873 
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

874 
 NONE => "")), 
44585  875 
locality_of_theorem global name0 th), th) 
43245  876 
in 
877 
if multi then (new :: multis, unis) 

878 
else (multis, new :: unis) 

879 
end)) ths 

38699  880 
#> snd 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

881 
end) 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

882 
in 
43245  883 
(* The singlename theorems go after the multiplename ones, so that single 
884 
names are preferred when both are available. *) 

885 
([], []) > add_facts false fold local_facts (unnamed_locals @ named_locals) 

886 
> add_facts true Facts.fold_static global_facts global_facts 

887 
> op @ 

38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

888 
end 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

889 

41199  890 
fun external_frees t = 
891 
[] > Term.add_frees t > filter_out (can Name.dest_internal o fst) 

892 

44585  893 
fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override) 
894 
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

895 
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

896 
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

897 
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

898 
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

899 
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

900 
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

901 
> 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

902 
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

903 
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

904 
(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

905 
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

906 
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

907 
else 
44585  908 
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

909 
> 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

910 
? 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

911 
> (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

912 
? 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

913 
> 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

914 
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

915 

44625  916 
fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const 
917 
fudge (override as {only, ...}) chained_ths hyp_ts concl_t 

918 
facts = 

37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

919 
let 
42361  920 
val thy = Proof_Context.theory_of ctxt 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

921 
val decay = Math.pow ((1.0  threshold1) / (1.0  threshold0), 
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

922 
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

923 
in 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

924 
trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

925 
" facts"); 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39265
diff
changeset

926 
(if only orelse threshold1 < 0.0 then 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

927 
facts 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39265
diff
changeset

928 
else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse 
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39265
diff
changeset

929 
max_relevant = 0 then 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

930 
[] 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

931 
else 
44625  932 
relevance_filter ctxt threshold0 decay max_relevant is_built_in_const 
933 
fudge override facts (chained_ths > map prop_of) hyp_ts 

934 
(concl_t > theory_constify fudge (Context.theory_name thy))) 

38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

935 
> 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

936 
end 
30536
07b4f050e4df
split relevancefilter and writing of problemfiles;
immler@in.tum.de
parents:
30364
diff
changeset

937 

15347  938 
end; 