author  blanchet 
Fri, 27 Aug 2010 15:39:17 +0200  
changeset 38827  cf01645cbbce 
parent 38825  4ec3cbd95f25 
child 38828  91ad85f962c4 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_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 

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

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

8 
datatype locality = General  Theory  Local  Chained 
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 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

17 
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

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

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

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

21 
bool > real * real > int > bool > relevance_override 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

22 
> Proof.context * (thm list * 'a) > term list > term 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

23 
> ((string * locality) * thm) list 
15347  24 
end; 
25 

35826  26 
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = 
15347  27 
struct 
28 

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

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

30 

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

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

32 
fun trace_msg msg = if !trace then tracing (msg ()) else () 
35826  33 

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

34 
val term_patterns = Unsynchronized.ref true 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

35 

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

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

37 

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

38 
datatype locality = General  Theory  Local  Chained 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

39 

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

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

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

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

43 
only: bool} 
21070  44 

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

45 
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

46 

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

47 
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

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

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

50 

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

51 
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

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

53 
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

54 
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

55 
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

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

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

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

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

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

61 
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

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

64 

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

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

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

67 
(***************************************************************) 
19194  68 

24287  69 
(*** constants with types ***) 
70 

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

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

72 
datatype pattern = PVar  PApp of string * pattern list 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

73 

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

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

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

76 
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

77 
and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" 
24287  78 

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

38824  80 
fun match_pattern (PVar, _) = true 
81 
 match_pattern (PApp _, PVar) = false 

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

83 
s = t andalso match_patterns (ps, qs) 

84 
and match_patterns (_, []) = true 

85 
 match_patterns ([], _) = false 

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

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

24287  88 

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

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

90 
fun pconst_mem f consts (s, ps) = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

91 
exists (curry (match_patterns o f) ps) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

93 
fun pconst_hyper_mem f const_tab (s, ps) = 
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

94 
exists (curry (match_patterns 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

95 

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

96 
fun ptype (Type (s, Ts)) = PApp (s, map ptype Ts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

97 
 ptype (TFree (s, _)) = PApp (s, []) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

98 
 ptype (TVar _) = PVar 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

99 

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

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

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

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

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

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

105 
 _ => 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

106 
(* Pairs a constant with the list of its type instantiations. *) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

107 
and pconst_args thy const (s, T) ts = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

108 
(if const then map ptype (Sign.const_typargs thy (s, T)) else []) @ 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

109 
(if !term_patterns then map (pterm thy) ts else []) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

110 
and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts) 
24287  111 

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

112 
fun string_for_hyper_pconst (s, pss) = 
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

113 
s ^ "{" ^ commas (map string_for_patterns pss) ^ "}" 
24287  114 

38816  115 
val abs_name = "Sledgehammer.abs" 
38749  116 
val skolem_prefix = "Sledgehammer.sko" 
38747  117 

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

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

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

121 
[@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, 
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

122 
@{const_name "op ="}] 
37537  123 

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

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

125 
connective, which we ignore.*) 
38824  126 
fun add_pconst_to_table also_skolem (c, ps) = 
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

127 
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

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

129 
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

130 
else 
38824  131 
Symtab.map_default (c, [ps]) (insert (op =) ps) 
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

132 

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

133 
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

134 

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

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

136 
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

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

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

139 
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

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

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

142 
add_pconst_to_table also_skolems (pconst thy const (s, T) ts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

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

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

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

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

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

149 
null ts ? add_pconst_to_table true (abs_name, []) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

151 
 (_, ts) => fold do_term ts 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

152 
fun do_quantifier will_surely_be_skolemized body_t = 
37537  153 
do_formula pos body_t 
38747  154 
#> (if also_skolems andalso will_surely_be_skolemized then 
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

155 
add_pconst_to_table true (gensym skolem_prefix, []) 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

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

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

158 
and do_term_or_formula T = 
38692  159 
if is_formula_type T then do_formula NONE else do_term 
37537  160 
and do_formula pos t = 
161 
case t of 

162 
Const (@{const_name all}, _) $ Abs (_, _, body_t) => 

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

163 
do_quantifier (pos = SOME false) body_t 
37537  164 
 @{const "==>"} $ t1 $ t2 => 
165 
do_formula (flip pos) t1 #> do_formula pos t2 

166 
 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

167 
fold (do_term_or_formula T) [t1, t2] 
37537  168 
 @{const Trueprop} $ t1 => do_formula pos t1 
169 
 @{const Not} $ t1 => do_formula (flip pos) t1 

170 
 Const (@{const_name All}, _) $ Abs (_, _, body_t) => 

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

171 
do_quantifier (pos = SOME false) body_t 
37537  172 
 Const (@{const_name Ex}, _) $ Abs (_, _, body_t) => 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

173 
do_quantifier (pos = SOME true) body_t 
37537  174 
 @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2] 
175 
 @{const "op "} $ t1 $ t2 => fold (do_formula pos) [t1, t2] 

176 
 @{const "op >"} $ t1 $ t2 => 

177 
do_formula (flip pos) t1 #> do_formula pos t2 

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

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

179 
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

180 
 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

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

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

183 
 Const (@{const_name Ex1}, _) $ Abs (_, _, body_t) => 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

184 
do_quantifier (is_some pos) body_t 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

185 
 Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, body_t) => 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

186 
do_quantifier (pos = SOME false) 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

187 
(HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, body_t)) 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

188 
 Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, body_t) => 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

189 
do_quantifier (pos = SOME true) 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

190 
(HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, body_t)) 
37537  191 
 (t0 as Const (_, @{typ bool})) $ t1 => 
192 
do_term t0 #> do_formula pos t1 (* theory constant *) 

193 
 _ => 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

194 
in Symtab.empty > fold (do_formula pos) ts end 
24287  195 

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

197 
takes the given theory into account.*) 

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

198 
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

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

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

201 
val name = Context.theory_name (theory_of_thm th) 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

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

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

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

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

206 

24287  207 
(**** Constant / Type Frequencies ****) 
208 

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

211 
latter, we need a linear ordering on "pattern list". *) 
24287  212 

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

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

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

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

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

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

219 
prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2) 
24287  220 

38743  221 
structure CTtab = 
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

222 
Table(type key = pattern list val ord = dict_ord pattern_ord) 
24287  223 

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

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

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

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

227 
(* Twodimensional table update. Constant maps to types maps to count. *) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

228 
CTtab.map_default (pconst_args thy const (s, T) ts, 0) (Integer.add 1) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

229 
> Symtab.map_default (s, CTtab.empty) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

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

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

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

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

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

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

237 
in do_term o theory_const_prop_of theory_relevant o snd end 
24287  238 

239 

240 
(**** Actual Filtering Code ****) 

241 

242 
(*The frequency of a constant is the sum of those of all instances of its type.*) 

38824  243 
fun pconst_freq match const_tab (c, ps) = 
244 
CTtab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m) 

38686  245 
(the (Symtab.lookup const_tab c)) 0 
246 

24287  247 

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

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

249 
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

250 

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

251 
(* "log" seems best in practice. A constant function of one ignores the constant 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

252 
frequencies. *) 
38747  253 
fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0) 
254 
fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4 

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

255 

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

256 
(* FUDGE *) 
38821  257 
val abs_rel_weight = 0.5 
258 
val abs_irrel_weight = 2.0 

259 
val skolem_rel_weight = 2.0 (* impossible *) 

260 
val skolem_irrel_weight = 0.5 

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

261 

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

262 
(* Computes a constant's weight, as determined by its frequency. *) 
38821  263 
fun generic_weight abs_weight skolem_weight logx f const_tab (c as (s, _)) = 
38816  264 
if s = abs_name then abs_weight 
265 
else if String.isPrefix skolem_prefix s then skolem_weight 

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

266 
else logx (pconst_freq (match_patterns o f) const_tab c) 
38821  267 

268 
val rel_weight = generic_weight abs_rel_weight skolem_rel_weight rel_log I 

269 
val irrel_weight = generic_weight abs_irrel_weight skolem_irrel_weight irrel_log 

270 
swap 

24287  271 

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

272 
(* FUDGE *) 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

273 
fun locality_multiplier General = 1.0 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

274 
 locality_multiplier Theory = 1.1 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

275 
 locality_multiplier Local = 1.3 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

276 
 locality_multiplier Chained = 2.0 
38751
01c4d14b2a61
add a bonus for chained facts, since they are likely to be relevant;
blanchet
parents:
38749
diff
changeset

277 

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

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

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

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

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

282 
 (rel, irrel) => 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

283 
case irrel > filter_out (pconst_mem swap rel) of 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

285 
 irrel => 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

287 
val rel_weight = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

288 
fold (curry Real.+ o rel_weight const_tab) rel 0.0 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

289 
> curry Real.* (locality_multiplier loc) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

290 
val irrel_weight = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

291 
fold (curry Real.+ o irrel_weight const_tab) irrel 0.0 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

292 
val res = rel_weight / (rel_weight + irrel_weight) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

293 
in if Real.isFinite res then res else 0.0 end 
38747  294 

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

295 
fun pconsts_in_axiom thy t = 
38825  296 
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) 
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

297 
(get_pconsts 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

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

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

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

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

302 
 consts => SOME ((axiom, consts), NONE) 
24287  303 

38699  304 
type annotated_thm = 
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

305 
(((unit > string) * locality) * thm) * (string * pattern list) list 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

306 

38747  307 
fun take_most_relevant max_max_imperfect max_relevant remaining_max 
308 
(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

309 
let 
38747  310 
val max_imperfect = 
311 
Real.ceil (Math.pow (max_max_imperfect, 

312 
Real.fromInt remaining_max 

313 
/ Real.fromInt max_relevant)) 

314 
val (perfect, imperfect) = 

315 
candidates > List.partition (fn (_, w) => w > 0.99999) 

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

316 
> sort (Real.compare o swap o pairself snd) 
38747  317 
val ((accepts, more_rejects), rejects) = 
318 
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

319 
in 
38747  320 
trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^ 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

321 
" of " ^ Int.toString (length candidates) ^ "): " ^ (accepts 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

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

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

324 
> commas)); 
38747  325 
(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

326 
end 
24287  327 

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

328 
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

329 
if Symtab.is_empty tab then 
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

330 
get_pconsts 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

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

332 
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

333 
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

334 
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

335 

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

336 
(* FUDGE *) 
38683
23266607cb81
if no facts were selected on first iteration, try again with a lower threshold
blanchet
parents:
38682
diff
changeset

337 
val threshold_divisor = 2.0 
23266607cb81
if no facts were selected on first iteration, try again with a lower threshold
blanchet
parents:
38682
diff
changeset

338 
val ridiculous_threshold = 0.1 
38747  339 
val max_max_imperfect_fudge_factor = 0.66 
38683
23266607cb81
if no facts were selected on first iteration, try again with a lower threshold
blanchet
parents:
38682
diff
changeset

340 

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

341 
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

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

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

344 
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

345 
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

346 
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

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

348 
get_pconsts thy false (SOME false) goal_ts 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

349 
> fold (if_empty_replace_with_locality thy 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

350 
[Chained, Local, Theory] 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

352 
val del_thms = maps (ProofContext.get_fact ctxt) del 
38747  353 
val max_max_imperfect = 
354 
Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor) 

355 
fun iter j remaining_max threshold rel_const_tab hopeless hopeful = 

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

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

357 
fun game_over rejects = 
38747  358 
(* Add "add:" facts. *) 
359 
if null add_thms then 

360 
[] 

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

361 
else 
38747  362 
map_filter (fn ((p as (_, th), _), _) => 
363 
if member Thm.eq_thm add_thms th then SOME p 

364 
else NONE) rejects 

365 
fun relevant [] rejects hopeless [] = 

366 
(* Nothing has been added this iteration. *) 

367 
if j = 0 andalso threshold >= ridiculous_threshold then 

368 
(* First iteration? Try again. *) 

369 
iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab 

370 
hopeless hopeful 

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

371 
else 
38747  372 
game_over (rejects @ hopeless) 
373 
 relevant candidates rejects hopeless [] = 

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

374 
let 
38747  375 
val (accepts, more_rejects) = 
376 
take_most_relevant max_max_imperfect max_relevant remaining_max 

377 
candidates 

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

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

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

380 
> fold (add_pconst_to_table false) 
38747  381 
(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

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

383 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

400 
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

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

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

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

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

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

407 
else 
38747  408 
iter (j + 1) remaining_max threshold rel_const_tab' 
409 
hopeless_rejects hopeful_rejects) 

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

410 
end 
38747  411 
 relevant candidates rejects hopeless 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

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

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

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

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

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

418 
 NONE => axiom_weight loc const_tab rel_const_tab axiom_consts 
38747  419 
(* TODO: experiment 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

420 
val name = fst (fst (fst ax)) () 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

421 
val _ = if String.isPrefix "lift.simps(3" name then 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

422 
tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts)) 
38747  423 
else 
424 
() 

425 
*) 

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

426 
in 
38741  427 
if weight >= threshold then 
38747  428 
relevant ((ax, weight) :: candidates) rejects hopeless hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

429 
else 
38747  430 
relevant candidates ((ax, weight) :: rejects) hopeless hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

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

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

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

436 
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

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

438 
> map string_for_hyper_pconst)); 
38747  439 
relevant [] [] hopeless hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

442 
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

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

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

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

447 
end 
24287  448 

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

449 

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

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

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

453 

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

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

455 

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

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

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

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

459 
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

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

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

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

463 
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

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

465 

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

466 
fun make_fact_table xs = 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

467 
fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

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

469 

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

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

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

472 
["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", 
38682  473 
"split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", 
474 
"case_cong", "weak_case_cong"] 

475 
> map (prefix ".") 

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

476 

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

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

478 

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

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

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

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

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

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

484 

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

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

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

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

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

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

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

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

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

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

494 

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

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

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

498 

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

499 
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

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

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

502 

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

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

504 
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

505 

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

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

508 

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

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

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

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

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

514 

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

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

518 
 _ => false) (prop_of th) 

519 

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

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

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

522 

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

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

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

525 

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

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

527 
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

528 
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

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

530 

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

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

532 
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

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

534 
let 
38629  535 
fun is_bad_equal (Var z) t = 
536 
not (exists_subterm (fn Var z' => z = z'  _ => false) t) 

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

538 
 is_bad_equal _ _ = false 

539 
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

540 
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

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

542 
(_, @{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

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

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

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

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

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

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

549 
 (_, @{const "==>"} $ t1 $ t2) => 
38629  550 
do_formula (not pos) t1 andalso 
551 
(t2 = @{prop 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

552 
 (_, @{const "op >"} $ t1 $ t2) => 
38629  553 
do_formula (not pos) t1 andalso 
554 
(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

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

556 
 (true, @{const "op "} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

557 
 (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

558 
 (true, Const (@{const_name "op ="}, _) $ 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

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

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

561 
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

562 

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

563 
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

564 
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

565 
 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

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

567 

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

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

569 
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

570 
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

571 
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

572 
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

573 
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

574 

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

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

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

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

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

581 
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

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

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

584 

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

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

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

587 
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

588 
is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse 
38821  589 
is_metastrange_theorem thm orelse is_that_fact thm 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

591 

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

592 
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

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

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

595 
val thy_prefix = Context.theory_name thy ^ Long_Name.separator 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

596 
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

597 
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

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

599 
val is_chained = member Thm.eq_thm chained_ths 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38816
diff
changeset

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

601 
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

602 
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

603 
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

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

605 
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

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

607 
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

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

609 
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

610 
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

611 
fun add_facts global foldx facts = 
38699  612 
foldx (fn (name0, ths) => 
613 
if name0 <> "" andalso 

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

615 
(Facts.is_concealed facts name0 orelse 

616 
(respect_no_atp andalso is_package_def name0) orelse 

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

618 
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

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

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

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

622 
val base_loc = 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

623 
if not global then Local 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

624 
else if String.isPrefix thy_prefix name0 then Theory 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

625 
else General 
38699  626 
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

627 
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

628 
"`" ^ 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

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

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

631 
> simplify_spaces 
38699  632 
fun check_thms a = 
633 
case try (ProofContext.get_thms ctxt) a of 

634 
NONE => false 

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

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

636 
in 
38699  637 
pair 1 
638 
#> fold (fn th => fn (j, rest) => 

639 
(j + 1, 

640 
if is_theorem_bad_for_atps full_types th andalso 

641 
not (member Thm.eq_thm add_thms th) then 

642 
rest 

643 
else 

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

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

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

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

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

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

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

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

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

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

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

654 
 NONE => "" 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

655 
end), if is_chained th then Chained else base_loc), 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

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

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

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

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

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

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

663 

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

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

665 
names are preferred when both are available. *) 
38699  666 
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

667 
List.partition (fst o snd) #> op @ #> map (apsnd snd) 
38699  668 
#> 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

669 

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

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

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

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

673 

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

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

675 
theory_relevant (relevance_override as {add, del, only}) 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

676 
(ctxt, (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

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

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

679 
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

680 
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

681 
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

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

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

685 
o name_thm_pairs_from_ref ctxt reserved chained_ths) add 
38699  686 
else 
687 
all_name_thms_pairs ctxt reserved full_types add_thms chained_ths) 

38688  688 
> name_thm_pairs ctxt (respect_no_atp andalso not only) 
38595
bbb0982656eb
make sure that "add:" doesn't influence the relevance filter too much
blanchet
parents:
38594
diff
changeset

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

690 
in 
38688  691 
trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^ 
692 
" theorems"); 

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

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

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

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

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

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

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

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

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

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

702 

15347  703 
end; 