author  blanchet 
Wed, 01 Sep 2010 10:26:54 +0200  
changeset 38992  542474156c66 
parent 38988  483879af0643 
child 38993  504b9e1efd33 
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 
33309  4 
*) 
15452  5 

38988  6 
signature SLEDGEHAMMER_FILTER = 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

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

8 
datatype locality = General  Intro  Elim  Simp  Local  Chained 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

9 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

10 
type relevance_override = 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

11 
{add: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

12 
del: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

13 
only: bool} 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

14 

37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

15 
val trace : bool Unsynchronized.ref 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

16 
val worse_irrel_freq : real Unsynchronized.ref 
38939  17 
val higher_order_irrel_weight : real Unsynchronized.ref 
38899
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

18 
val abs_rel_weight : real Unsynchronized.ref 
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

19 
val abs_irrel_weight : real Unsynchronized.ref 
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

20 
val skolem_irrel_weight : real Unsynchronized.ref 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

21 
val theory_const_rel_weight : real Unsynchronized.ref 
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

22 
val theory_const_irrel_weight : real Unsynchronized.ref 
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

23 
val intro_bonus : real Unsynchronized.ref 
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

24 
val elim_bonus : real Unsynchronized.ref 
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

25 
val simp_bonus : real Unsynchronized.ref 
38899
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

26 
val local_bonus : real Unsynchronized.ref 
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

27 
val chained_bonus : real Unsynchronized.ref 
38904  28 
val max_imperfect : real Unsynchronized.ref 
29 
val max_imperfect_exp : real Unsynchronized.ref 

38899
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

30 
val threshold_divisor : real Unsynchronized.ref 
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

31 
val ridiculous_threshold : real Unsynchronized.ref 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

32 
val name_thm_pairs_from_ref : 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

33 
Proof.context > unit Symtab.table > thm list > Facts.ref 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

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

35 
val relevant_facts : 
38891  36 
Proof.context > bool > real * real > int > bool > relevance_override 
37 
> thm list > term list > term > ((string * locality) * thm) list 

15347  38 
end; 
39 

38988  40 
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = 
15347  41 
struct 
42 

38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38644
diff
changeset

43 
open Sledgehammer_Util 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38644
diff
changeset

44 

37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

45 
val trace = Unsynchronized.ref false 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

46 
fun trace_msg msg = if !trace then tracing (msg ()) else () 
35826  47 

38828
91ad85f962c4
turn off experimental feature per default + avoid exception on "theory constant"
blanchet
parents:
38827
diff
changeset

48 
(* experimental feature *) 
38889  49 
val term_patterns = false 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

50 

37580
c2c1caff5dea
got rid of "respect_no_atp" option, which even I don't use
blanchet
parents:
37578
diff
changeset

51 
val respect_no_atp = true 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

52 

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

53 
datatype locality = General  Intro  Elim  Simp  Local  Chained 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

54 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

55 
type relevance_override = 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

56 
{add: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

57 
del: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

58 
only: bool} 
21070  59 

37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

60 
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

61 
val abs_name = "Sledgehammer.abs" 
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

62 
val skolem_prefix = "Sledgehammer.sko" 
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

63 
val theory_const_suffix = Long_Name.separator ^ " 1" 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

64 

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

65 
fun repair_name reserved multi j name = 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

66 
(name > Symtab.defined reserved name ? quote) ^ 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

67 
(if multi then "(" ^ Int.toString j ^ ")" else "") 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

68 

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

69 
fun name_thm_pairs_from_ref ctxt reserved chained_ths xref = 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

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

71 
val ths = ProofContext.get_fact ctxt xref 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

72 
val name = Facts.string_of_ref xref 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

73 
val multi = length ths > 1 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

74 
in 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

75 
(ths, (1, [])) 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

76 
> fold (fn th => fn (j, rest) => 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

77 
(j + 1, ((repair_name reserved multi j name, 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

78 
if member Thm.eq_thm chained_ths th then Chained 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

79 
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

80 
> snd 
38699  81 
end 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

82 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

83 
(***************************************************************) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

84 
(* Relevance Filtering *) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

85 
(***************************************************************) 
19194  86 

24287  87 
(*** constants with types ***) 
88 

38939  89 
fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) = 
90 
order_of_type T1 (* cheat: pretend sets are firstorder *) 

91 
 order_of_type (Type (@{type_name fun}, [T1, T2])) = 

92 
Int.max (order_of_type T1 + 1, order_of_type T2) 

93 
 order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0 

94 
 order_of_type _ = 0 

95 

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

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

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

99 

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

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

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

102 
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

103 
and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" 
38939  104 
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps 
24287  105 

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

38824  107 
fun match_pattern (PVar, _) = true 
108 
 match_pattern (PApp _, PVar) = false 

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

110 
s = t andalso match_patterns (ps, qs) 

111 
and match_patterns (_, []) = true 

112 
 match_patterns ([], _) = false 

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

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

38939  115 
fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs) 
24287  116 

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

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

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

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

121 
fun pconst_hyper_mem f const_tab (s, ps) = 
38939  122 
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

123 

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

126 
 pattern_for_type (TVar _) = PVar 

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

127 

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

128 
fun pterm thy t = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

130 
(Const x, ts) => PApp (pconst thy true x ts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

131 
 (Free x, ts) => PApp (pconst thy false x ts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

132 
 (Var x, []) => PVar 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

133 
 _ => PApp ("?", []) (* equivalence class of higherorder constructs *) 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

134 
(* Pairs a constant with the list of its type instantiations. *) 
38939  135 
and ptype thy const x ts = 
136 
(if const then map pattern_for_type (these (try (Sign.const_typargs thy) x)) 

38828
91ad85f962c4
turn off experimental feature per default + avoid exception on "theory constant"
blanchet
parents:
38827
diff
changeset

137 
else []) @ 
38889  138 
(if term_patterns then map (pterm thy) ts else []) 
38939  139 
and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts) 
140 
and rich_ptype thy const (s, T) ts = 

141 
PType (order_of_type T, ptype thy const (s, T) ts) 

142 
and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts) 

24287  143 

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

24287  146 

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

147 
(* These are typically simplified away by "Meson.presimplify". Equality is 
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

148 
handled specially via "fequal". *) 
38682  149 
val boring_consts = 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

150 
[@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

151 
@{const_name HOL.eq}] 
37537  152 

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

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

154 
connective, which we ignore.*) 
38939  155 
fun add_pconst_to_table also_skolem (c, 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

156 
if member (op =) boring_consts c orelse 
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

157 
(not also_skolem andalso String.isPrefix skolem_prefix c) then 
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

158 
I 
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

159 
else 
38939  160 
Symtab.map_default (c, [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

161 

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

162 
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) 
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

163 

38906  164 
fun pconsts_in_terms thy also_skolems pos ts = 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

165 
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

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

167 
(* We include free variables, as well as constants, to handle locales. For 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

168 
each quantifiers that must necessarily be skolemized by the ATP, we 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

169 
introduce a fresh constant to simulate the effect of Skolemization. *) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

170 
fun do_const const (s, T) ts = 
38939  171 
add_pconst_to_table also_skolems (rich_pconst thy const (s, T) ts) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

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

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

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

176 
 (Free x, ts) => do_const false x ts 
38939  177 
 (Abs (_, T, t'), ts) => 
178 
(null ts 

179 
? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, []))) 

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

180 
#> fold do_term (t' :: ts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

181 
 (_, ts) => fold do_term ts 
38939  182 
fun do_quantifier will_surely_be_skolemized abs_T body_t = 
37537  183 
do_formula pos body_t 
38747  184 
#> (if also_skolems andalso will_surely_be_skolemized then 
38939  185 
add_pconst_to_table true 
186 
(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

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

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

189 
and do_term_or_formula T = 
38692  190 
if is_formula_type T then do_formula NONE else do_term 
37537  191 
and do_formula pos t = 
192 
case t of 

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

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

197 
 Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => 

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

198 
fold (do_term_or_formula T) [t1, t2] 
37537  199 
 @{const Trueprop} $ t1 => do_formula pos t1 
200 
 @{const Not} $ t1 => do_formula (flip pos) t1 

38939  201 
 Const (@{const_name All}, _) $ Abs (_, T, t') => 
202 
do_quantifier (pos = SOME false) T t' 

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

204 
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

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

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

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

209 
 Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 => 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

210 
fold (do_term_or_formula T) [t1, t2] 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

211 
 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

212 
$ t1 $ t2 $ t3 => 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

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

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

217 
do_quantifier (pos = SOME false) T 

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

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

220 
do_quantifier (pos = SOME true) T 

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

37537  222 
 (t0 as Const (_, @{typ bool})) $ t1 => 
223 
do_term t0 #> do_formula pos t1 (* theory constant *) 

224 
 _ => do_term t 

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

225 
in Symtab.empty > fold (do_formula pos) ts end 
24287  226 

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

228 
takes the given theory into account.*) 

37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

229 
fun theory_const_prop_of theory_relevant th = 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

230 
if theory_relevant then 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

231 
let 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

232 
val name = Context.theory_name (theory_of_thm th) 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

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

234 
in t $ prop_of th end 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

235 
else 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

236 
prop_of th 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

237 

24287  238 
(**** Constant / Type Frequencies ****) 
239 

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

242 
latter, we need a linear ordering on "pattern list". *) 
24287  243 

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

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

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

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

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

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

250 
prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2) 
38939  251 
fun ptype_ord (PType p, PType q) = 
252 
prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q) 

24287  253 

38939  254 
structure PType_Tab = Table(type key = ptype val ord = ptype_ord) 
24287  255 

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

256 
fun count_axiom_consts theory_relevant thy = 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

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

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

259 
(* Twodimensional table update. Constant maps to types maps to count. *) 
38939  260 
PType_Tab.map_default (rich_ptype thy const (s, T) ts, 0) (Integer.add 1) 
261 
> Symtab.map_default (s, PType_Tab.empty) 

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

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

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

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

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

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

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

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

269 
in do_term o theory_const_prop_of theory_relevant o snd end 
24287  270 

271 

272 
(**** Actual Filtering Code ****) 

273 

38939  274 
fun pow_int x 0 = 1.0 
275 
 pow_int x 1 = x 

276 
 pow_int x n = if n > 0 then x * pow_int x (n  1) else pow_int x (n + 1) / x 

277 

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

38686  282 

24287  283 

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

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

285 
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

286 

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

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

288 
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

289 
rare ones. *) 
38939  290 
fun rel_weight_for order 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

291 

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

292 
(* FUDGE *) 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

293 
val worse_irrel_freq = Unsynchronized.ref 100.0 
38939  294 
val higher_order_irrel_weight = Unsynchronized.ref 1.05 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

295 

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

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

297 
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

298 
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

299 
so common as to be of little interest. *) 
38939  300 
fun irrel_weight_for order freq = 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

301 
let val (k, x) = !worse_irrel_freq > `Real.ceil in 
38939  302 
(if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x 
303 
else rel_weight_for order freq / rel_weight_for order k) 

304 
* pow_int (!higher_order_irrel_weight) (order  1) 

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

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

306 

38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

307 
(* FUDGE *) 
38899
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

308 
val abs_rel_weight = Unsynchronized.ref 0.5 
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

309 
val abs_irrel_weight = Unsynchronized.ref 2.0 
38904  310 
val skolem_irrel_weight = Unsynchronized.ref 0.75 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

311 
val theory_const_rel_weight = Unsynchronized.ref 0.5 
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

312 
val theory_const_irrel_weight = Unsynchronized.ref 0.25 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

313 

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

314 
(* Computes a constant's weight, as determined by its frequency. *) 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

315 
fun generic_pconst_weight abs_weight skolem_weight theory_const_weight 
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

316 
weight_for f const_tab (c as (s, PType (m, _))) = 
38816  317 
if s = abs_name then abs_weight 
318 
else if String.isPrefix skolem_prefix s then skolem_weight 

38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

319 
else if String.isSuffix theory_const_suffix s then theory_const_weight 
38939  320 
else weight_for m (pconst_freq (match_ptype o f) const_tab c) 
38821  321 

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

322 
fun rel_pconst_weight const_tab = 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

323 
generic_pconst_weight (!abs_rel_weight) 0.0 (!theory_const_rel_weight) 
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

324 
rel_weight_for I const_tab 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

325 
fun irrel_pconst_weight const_tab = 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

326 
generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight) 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

327 
(!theory_const_irrel_weight) irrel_weight_for swap const_tab 
24287  328 

38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

329 
(* FUDGE *) 
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

330 
val intro_bonus = Unsynchronized.ref 0.15 
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

331 
val elim_bonus = Unsynchronized.ref 0.15 
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

332 
val simp_bonus = Unsynchronized.ref 0.15 
38906  333 
val local_bonus = Unsynchronized.ref 0.55 
38901
ee36b983ca22
fiddle with fact filter based on Mirabelle experiments
blanchet
parents:
38899
diff
changeset

334 
val chained_bonus = Unsynchronized.ref 1.5 
38899
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

335 

38889  336 
fun locality_bonus General = 0.0 
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

337 
 locality_bonus Intro = !intro_bonus 
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

338 
 locality_bonus Elim = !elim_bonus 
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

339 
 locality_bonus Simp = !simp_bonus 
38899
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

340 
 locality_bonus Local = !local_bonus 
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

341 
 locality_bonus Chained = !chained_bonus 
38751
01c4d14b2a61
add a bonus for chained facts, since they are likely to be relevant;
blanchet
parents:
38749
diff
changeset

342 

38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

343 
fun axiom_weight loc const_tab relevant_consts axiom_consts = 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

344 
case axiom_consts > List.partition (pconst_hyper_mem I relevant_consts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

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

347 
 (rel, irrel) => 
38889  348 
let 
349 
val irrel = irrel > filter_out (pconst_mem swap rel) 

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

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

351 
0.0 > fold (curry (op +) o rel_pconst_weight const_tab) rel 
38889  352 
val irrel_weight = 
353 
~ (locality_bonus loc) 

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

354 
> fold (curry (op +) o irrel_pconst_weight const_tab) irrel 
38889  355 
val res = rel_weight / (rel_weight + irrel_weight) 
356 
in if Real.isFinite res then res else 0.0 end 

38747  357 

38904  358 
(* FIXME: experiment 
359 
fun debug_axiom_weight loc const_tab relevant_consts axiom_consts = 

360 
case axiom_consts > List.partition (pconst_hyper_mem I relevant_consts) 

361 
> filter_out (pconst_hyper_mem swap relevant_consts) of 

362 
([], _) => 0.0 

363 
 (rel, irrel) => 

364 
let 

365 
val irrel = irrel > filter_out (pconst_mem swap rel) 

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

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

367 
0.0 > fold (curry (op +) o rel_pconst_weight const_tab) rel 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

368 
val irrels_weight = 
38904  369 
~ (locality_bonus loc) 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

370 
> fold (curry (op +) o irrel_pconst_weight const_tab) irrel 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

371 
val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel)) 
38939  372 
val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel)) 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

373 
val res = rels_weight / (rels_weight + irrels_weight) 
38904  374 
in if Real.isFinite res then res else 0.0 end 
375 
*) 

376 

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

377 
fun pconsts_in_axiom thy t = 
38825  378 
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) 
38906  379 
(pconsts_in_terms thy true (SOME true) [t]) [] 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

380 
fun pair_consts_axiom theory_relevant thy axiom = 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

381 
case axiom > snd > theory_const_prop_of theory_relevant 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

382 
> pconsts_in_axiom thy of 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

383 
[] => NONE 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

384 
 consts => SOME ((axiom, consts), NONE) 
24287  385 

38699  386 
type annotated_thm = 
38939  387 
(((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

388 

38904  389 
(* FUDGE *) 
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

390 
val max_imperfect = Unsynchronized.ref 11.5 
38904  391 
val max_imperfect_exp = Unsynchronized.ref 1.0 
38889  392 

38904  393 
fun take_most_relevant max_relevant remaining_max 
38747  394 
(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

395 
let 
38747  396 
val max_imperfect = 
38904  397 
Real.ceil (Math.pow (!max_imperfect, 
398 
Math.pow (Real.fromInt remaining_max 

399 
/ Real.fromInt max_relevant, !max_imperfect_exp))) 

38747  400 
val (perfect, imperfect) = 
38889  401 
candidates > sort (Real.compare o swap o pairself snd) 
402 
> take_prefix (fn (_, w) => w > 0.99999) 

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

405 
in 
38889  406 
trace_msg (fn () => 
407 
"Actually passed (" ^ Int.toString (length accepts) ^ " of " ^ 

408 
Int.toString (length candidates) ^ "): " ^ 

409 
(accepts > map (fn ((((name, _), _), _), weight) => 

38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

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

411 
> commas)); 
38747  412 
(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

413 
end 
24287  414 

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

415 
fun if_empty_replace_with_locality thy axioms loc 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

416 
if Symtab.is_empty tab then 
38906  417 
pconsts_in_terms thy false (SOME false) 
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

418 
(map_filter (fn ((_, loc'), th) => 
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

419 
if loc' = loc then SOME (prop_of th) else NONE) axioms) 
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

420 
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

421 
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

422 

38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

423 
(* FUDGE *) 
38899
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

424 
val threshold_divisor = Unsynchronized.ref 2.0 
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

425 
val ridiculous_threshold = Unsynchronized.ref 0.1 
38683
23266607cb81
if no facts were selected on first iteration, try again with a lower threshold
blanchet
parents:
38682
diff
changeset

426 

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

427 
fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

428 
({add, del, ...} : relevance_override) axioms goal_ts = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

430 
val thy = ProofContext.theory_of ctxt 
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

431 
val const_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

432 
fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty 
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

433 
val goal_const_tab = 
38906  434 
pconsts_in_terms thy false (SOME false) goal_ts 
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

435 
> fold (if_empty_replace_with_locality thy axioms) [Chained, Local] 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

436 
val add_thms = maps (ProofContext.get_fact ctxt) add 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

437 
val del_thms = maps (ProofContext.get_fact ctxt) del 
38747  438 
fun iter j remaining_max threshold rel_const_tab hopeless hopeful = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

440 
fun game_over rejects = 
38747  441 
(* Add "add:" facts. *) 
442 
if null add_thms then 

443 
[] 

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

444 
else 
38747  445 
map_filter (fn ((p as (_, th), _), _) => 
446 
if member Thm.eq_thm add_thms th then SOME p 

447 
else NONE) rejects 

38889  448 
fun relevant [] rejects [] = 
38747  449 
(* Nothing has been added this iteration. *) 
38899
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

450 
if j = 0 andalso threshold >= !ridiculous_threshold then 
38747  451 
(* First iteration? Try again. *) 
38899
55391ee96614
made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents:
38891
diff
changeset

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

454 
else 
38747  455 
game_over (rejects @ hopeless) 
38889  456 
 relevant candidates rejects [] = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

457 
let 
38747  458 
val (accepts, more_rejects) = 
38904  459 
take_most_relevant max_relevant remaining_max candidates 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

461 
rel_const_tab 
38901
ee36b983ca22
fiddle with fact filter based on Mirabelle experiments
blanchet
parents:
38899
diff
changeset

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

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

464 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

481 
trace_msg (fn () => "New or updated constants: " ^ 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

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

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

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

485 
map (fst o fst) accepts @ 
38747  486 
(if remaining_max = 0 then 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

487 
game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects) 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

488 
else 
38747  489 
iter (j + 1) remaining_max threshold rel_const_tab' 
490 
hopeless_rejects hopeful_rejects) 

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

491 
end 
38889  492 
 relevant candidates rejects 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

493 
(((ax as (((_, loc), th), axiom_consts)), cached_weight) 
38747  494 
:: hopeful) = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

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

498 
SOME w => w 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

499 
 NONE => axiom_weight loc const_tab rel_const_tab axiom_consts 
38904  500 
(* FIXME: experiment 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

501 
val name = fst (fst (fst ax)) () 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

502 
val _ = if String.isSubstring "positive_minus" name orelse String.isSubstring "not_exp_le_zero" name then 
38901
ee36b983ca22
fiddle with fact filter based on Mirabelle experiments
blanchet
parents:
38899
diff
changeset

503 
tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts)) 
38747  504 
else 
505 
() 

506 
*) 

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

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

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

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

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

514 
trace_msg (fn () => 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

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

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

517 
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

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

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

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

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

523 
axioms > filter_out (member Thm.eq_thm del_thms o snd) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

524 
> map_filter (pair_consts_axiom theory_relevant thy) 
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

525 
> iter 0 max_relevant threshold0 goal_const_tab [] 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

526 
> tap (fn res => trace_msg (fn () => 
38686  527 
"Total relevant: " ^ Int.toString (length res))) 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

528 
end 
24287  529 

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

530 

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

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

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

534 

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

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

536 

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

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

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

539 
fun is_package_def a = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30291
diff
changeset

540 
let val names = Long_Name.explode a 
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

541 
in 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

542 
length names > 2 andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

543 
not (hd names = "local") andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

544 
String.isSuffix "_def" a orelse String.isSuffix "_defs" a 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

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

546 

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

547 
fun mk_fact_table f xs = 
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

548 
fold (Termtab.update o `(prop_of o f)) xs Termtab.empty 
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

549 
fun uniquify xs = Termtab.fold (cons o snd) (mk_fact_table snd xs) [] 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

550 

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

551 
(* FIXME: put other record thms here, or declare as "no_atp" *) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

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

553 
["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", 
38682  554 
"split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", 
555 
"case_cong", "weak_case_cong"] 

556 
> map (prefix ".") 

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

557 

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

558 
val max_lambda_nesting = 3 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

559 

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

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

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

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

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

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

565 

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

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

567 
quantifiers. *) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

568 
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

569 
formula_has_too_many_lambdas (T :: Ts) t 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

570 
 formula_has_too_many_lambdas Ts t = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

571 
if is_formula_type (fastype_of1 (Ts, t)) then 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

572 
exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t)) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

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

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

575 

38692  576 
(* 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

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

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

579 

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

580 
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

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

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

583 

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

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

585 
apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

586 

37543  587 
val exists_sledgehammer_const = 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

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

589 

38904  590 
(* FIXME: make more reliable *) 
591 
val exists_low_level_class_const = 

592 
exists_Const (fn (s, _) => 

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

594 

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

596 
case head_of (concl_of th) of 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

597 
Const (a, _) => (a <> @{const_name Trueprop} andalso 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

598 
a <> @{const_name "=="}) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

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

600 

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

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

604 
 _ => false) (prop_of th) 

605 

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

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

607 
exists_subtype (fn TFree (_, []) => true  TVar (_, []) => true  _ => false) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

608 

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

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

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

611 

38289
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

612 
(* Too general means, positive equality literal with a variable X as one 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

613 
operand, when X does not occur properly in the other operand. This rules out 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

614 
clearly inconsistent facts such as X = a  X = b, though it by no means 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

615 
guarantees soundness. *) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

616 

38289
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

617 
(* Unwanted equalities are those between a (bound or schematic) variable that 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

618 
does not properly occur in the second operand. *) 
38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

619 
val is_exhaustive_finite = 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

620 
let 
38629  621 
fun is_bad_equal (Var z) t = 
622 
not (exists_subterm (fn Var z' => z = z'  _ => false) t) 

623 
 is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) 

624 
 is_bad_equal _ _ = false 

625 
fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 

38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

626 
fun do_formula pos t = 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

627 
case (pos, t) of 
38615
4e1d828ee514
improve "x = A  x = B  x = C"style axiom detection
blanchet
parents:
38611
diff
changeset

628 
(_, @{const Trueprop} $ t1) => do_formula pos t1 
38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

629 
 (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

630 
do_formula pos t' 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

631 
 (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

632 
do_formula pos t' 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

633 
 (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

634 
do_formula pos t' 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

635 
 (_, @{const "==>"} $ t1 $ t2) => 
38629  636 
do_formula (not pos) t1 andalso 
637 
(t2 = @{prop False} orelse do_formula pos t2) 

38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

638 
 (_, @{const HOL.implies} $ t1 $ t2) => 
38629  639 
do_formula (not pos) t1 andalso 
640 
(t2 = @{const False} orelse do_formula pos t2) 

38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

641 
 (_, @{const Not} $ t1) => do_formula (not pos) t1 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

642 
 (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

643 
 (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

644 
 (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2 
38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

645 
 (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

646 
 _ => false 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

647 
in do_formula true end 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

648 

38592
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

649 
fun has_bound_or_var_of_type tycons = 
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

650 
exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s 
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

651 
 Abs (_, Type (s, _), _) => member (op =) tycons s 
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

652 
 _ => false) 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

653 

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

654 
(* Facts are forbidden to contain variables of these types. The typical reason 
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

655 
is that they lead to unsoundness. Note that "unit" satisfies numerous 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

656 
equations like "?x = ()". The resulting clauses will have no type constraint, 
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

657 
yielding false proofs. Even "bool" leads to many unsound proofs, though only 
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

658 
for higherorder problems. *) 
38592
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

659 
val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}]; 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

660 

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

661 
(* Facts containing variables of type "unit" or "bool" or of the form 
38290
581a402a80f0
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents:
38289
diff
changeset

662 
"ALL x. x = A  x = B  x = C" are likely to lead to unsound proofs if types 
581a402a80f0
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents:
38289
diff
changeset

663 
are omitted. *) 
38593  664 
fun is_dangerous_term full_types t = 
38609  665 
not full_types andalso 
38679
2cfd0777580f
destroy elim rules before checking for finite exhaustive facts
blanchet
parents:
38652
diff
changeset

666 
let val t = transform_elim_term t in 
2cfd0777580f
destroy elim rules before checking for finite exhaustive facts
blanchet
parents:
38652
diff
changeset

667 
has_bound_or_var_of_type dangerous_types t orelse 
2cfd0777580f
destroy elim rules before checking for finite exhaustive facts
blanchet
parents:
38652
diff
changeset

668 
is_exhaustive_finite t 
2cfd0777580f
destroy elim rules before checking for finite exhaustive facts
blanchet
parents:
38652
diff
changeset

669 
end 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

670 

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

671 
fun is_theorem_bad_for_atps full_types thm = 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

672 
let val t = prop_of thm in 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

673 
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

674 
is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse 
38904  675 
exists_low_level_class_const t orelse is_metastrange_theorem thm orelse 
676 
is_that_fact thm 

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

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

678 

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

679 
fun clasimpset_rules_of ctxt = 
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

680 
let 
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

681 
val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt > claset_of > rep_cs 
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

682 
val intros = safeIs @ hazIs 
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

683 
val elims = map Classical.classical_rule (safeEs @ hazEs) 
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

684 
val simps = ctxt > simpset_of > dest_ss > #simps > map snd 
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

685 
in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end 
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

686 

38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

687 
fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths = 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

688 
let 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

689 
val thy = ProofContext.theory_of ctxt 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

690 
val global_facts = PureThy.facts_of thy 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

691 
val local_facts = ProofContext.facts_of ctxt 
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

692 
val named_locals = local_facts > Facts.dest_static [] 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

693 
val is_chained = member Thm.eq_thm chained_ths 
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

694 
val (intros, elims, simps) = 
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

695 
if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then 
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

696 
clasimpset_rules_of ctxt 
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

697 
else 
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

698 
(Termtab.empty, Termtab.empty, Termtab.empty) 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38816
diff
changeset

699 
(* Unnamed nonchained formulas with schematic variables are omitted, because 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38816
diff
changeset

700 
they are rejected by the backticks (`...`) parser for some reason. *) 
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

701 
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

702 
not (Thm.has_name_hint th) andalso 
d0f98bd81a85
add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents:
38819
diff
changeset

703 
(not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) andalso 
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

704 
forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

705 
val unnamed_locals = 
38820
d0f98bd81a85
add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents:
38819
diff
changeset

706 
union Thm.eq_thm (Facts.props local_facts) chained_ths 
d0f98bd81a85
add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents:
38819
diff
changeset

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

708 
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

709 
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

710 
fun add_facts global foldx facts = 
38699  711 
foldx (fn (name0, ths) => 
712 
if name0 <> "" andalso 

713 
forall (not o member Thm.eq_thm add_thms) ths andalso 

714 
(Facts.is_concealed facts name0 orelse 

715 
(respect_no_atp andalso is_package_def name0) orelse 

716 
exists (fn s => String.isSuffix s name0) multi_base_blacklist orelse 

717 
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

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

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

720 
let 
38699  721 
val multi = length ths > 1 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

722 
fun backquotify th = 
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

723 
"`" ^ Print_Mode.setmp [Print_Mode.input] 
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

724 
(Syntax.string_of_term ctxt) (prop_of th) ^ "`" 
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

725 
> String.translate (fn c => if Char.isPrint c then str c else "") 
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

726 
> simplify_spaces 
38699  727 
fun check_thms a = 
728 
case try (ProofContext.get_thms ctxt) a of 

729 
NONE => false 

730 
 SOME ths' => Thm.eq_thms (ths, ths') 

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

731 
in 
38699  732 
pair 1 
733 
#> fold (fn th => fn (j, rest) => 

734 
(j + 1, 

735 
if is_theorem_bad_for_atps full_types th andalso 

736 
not (member Thm.eq_thm add_thms th) then 

737 
rest 

738 
else 

38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

739 
(((fn () => 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

740 
if name0 = "" then 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

741 
th > backquotify 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

742 
else 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

743 
let 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

744 
val name1 = Facts.extern facts name0 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

745 
val name2 = Name_Space.extern full_space name0 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

746 
in 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

747 
case find_first check_thms [name1, name2, name0] of 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

748 
SOME name => repair_name reserved multi j name 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

749 
 NONE => "" 
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

750 
end), 
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

751 
let val t = prop_of th in 
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

752 
if is_chained th then Chained 
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

753 
else if not global then Local 
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

754 
else if Termtab.defined intros t then Intro 
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

755 
else if Termtab.defined elims t then Elim 
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

756 
else if Termtab.defined simps t then Simp 
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

757 
else General 
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

758 
end), 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

759 
(multi, th)) :: rest)) ths 
38699  760 
#> snd 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

762 
in 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

763 
[] > add_facts false fold local_facts (unnamed_locals @ named_locals) 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

764 
> add_facts true Facts.fold_static global_facts global_facts 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

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

766 

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

767 
(* The singlename theorems go after the multiplename ones, so that single 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

768 
names are preferred when both are available. *) 
38699  769 
fun name_thm_pairs ctxt respect_no_atp = 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

770 
List.partition (fst o snd) #> op @ #> map (apsnd snd) 
38699  771 
#> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

772 

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

773 
(***************************************************************) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

774 
(* ATP invocation methods setup *) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

775 
(***************************************************************) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

776 

38891  777 
fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

778 
theory_relevant (relevance_override as {add, del, only}) 
38891  779 
chained_ths hyp_ts concl_t = 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

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

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

782 
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

783 
val add_thms = maps (ProofContext.get_fact ctxt) add 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

784 
val reserved = reserved_isar_keyword_table () 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

785 
val axioms = 
38699  786 
(if only then 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

787 
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th))) 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

788 
o name_thm_pairs_from_ref ctxt reserved chained_ths) add 
38699  789 
else 
790 
all_name_thms_pairs ctxt reserved full_types add_thms chained_ths) 

38688  791 
> name_thm_pairs ctxt (respect_no_atp andalso not only) 
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

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

793 
in 
38688  794 
trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^ 
795 
" theorems"); 

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

796 
(if threshold0 > 1.0 orelse threshold0 > threshold1 then 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

798 
else if threshold0 < 0.0 then 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

801 
relevance_filter ctxt threshold0 decay max_relevant theory_relevant 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

802 
relevance_override axioms (concl_t :: hyp_ts)) 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

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

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

805 

15347  806 
end; 