author  blanchet 
Sat, 19 Jan 2013 17:42:12 +0100  
changeset 50985  23bb011a5832 
parent 50608  5977de2993ac 
child 51004  5f2788c38127 
permissions  rwrr 
48380  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_mepo.ML 
38027  2 
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36227
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
39958  4 

48380  5 
Sledgehammer's iterative relevance filter (MePo = MengPaulson). 
33309  6 
*) 
15452  7 

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

9 
sig 
46340  10 
type stature = ATP_Problem_Generate.stature 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

11 
type fact = Sledgehammer_Fact.fact 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

12 
type params = Sledgehammer_Provers.params 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

13 
type relevance_fudge = Sledgehammer_Provers.relevance_fudge 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

14 

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

15 
val trace : bool Config.T 
48219  16 
val pseudo_abs_name : string 
17 
val pseudo_skolem_prefix : string 

43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43324
diff
changeset

18 
val const_names_in_fact : 
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43324
diff
changeset

19 
theory > (string * typ > term list > bool * term list) > term 
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43324
diff
changeset

20 
> string list 
48406  21 
val mepo_suggested_facts : 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

22 
Proof.context > params > string > int > relevance_fudge option 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

23 
> term list > term > fact list > fact list 
15347  24 
end; 
25 

48381  26 
structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO = 
15347  27 
struct 
28 

46320  29 
open ATP_Problem_Generate 
50608  30 
open Sledgehammer_Util 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

31 
open Sledgehammer_Fact 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

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

33 

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

34 
val trace = 
48308  35 
Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

36 
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () 
35826  37 

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

38 
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator 
48219  39 
val pseudo_abs_name = sledgehammer_prefix ^ "abs" 
40 
val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko" 

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

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

42 

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

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

46 
 order_of_type _ = 0 

47 

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

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

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

51 

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

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

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

54 
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

55 
and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" 
38939  56 
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps 
24287  57 

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

38824  59 
fun match_pattern (PVar, _) = true 
60 
 match_pattern (PApp _, PVar) = false 

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

62 
s = t andalso match_patterns (ps, qs) 

63 
and match_patterns (_, []) = true 

64 
 match_patterns ([], _) = false 

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

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

38939  67 
fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs) 
24287  68 

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

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

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

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

73 
fun pconst_hyper_mem f const_tab (s, ps) = 
38939  74 
exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s)) 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

75 

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

78 
 pattern_for_type (TVar _) = PVar 

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

79 

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

80 
(* Pairs a constant with the list of its type instantiations. *) 
41204
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

81 
fun ptype thy const x = 
38939  82 
(if const then map pattern_for_type (these (try (Sign.const_typargs thy) x)) 
41204
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

83 
else []) 
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

84 
fun rich_ptype thy const (s, T) = 
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

85 
PType (order_of_type T, ptype thy const (s, T)) 
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

86 
fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T)) 
24287  87 

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

24287  90 

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

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

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

93 
fun add_pconst_to_table also_skolem (s, p) = 
48219  94 
if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I 
41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

95 
else Symtab.map_default (s, [p]) (insert (op =) p) 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

96 

47933
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

97 
(* Set constants tend to pull in too many irrelevant facts. We limit the damage 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

98 
by treating them more or less as if they were builtin but add their 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

99 
axiomatization at the end. *) 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

100 
val set_consts = [@{const_name Collect}, @{const_name Set.member}] 
47939
9ff976a6c2cb
added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)
blanchet
parents:
47933
diff
changeset

101 
val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong} 
47933
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

102 

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

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

104 
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

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

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

109 
Skolemization. *) 

47933
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

110 
fun do_const const ext_arg (x as (s, _)) ts = 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

111 
let val (built_in, ts) = is_built_in_const x ts in 
47933
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

112 
if member (op =) set_consts s then 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

113 
fold (do_term ext_arg) ts 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

114 
else 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

115 
(not built_in 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

116 
? add_pconst_to_table also_skolems (rich_pconst thy const x)) 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

117 
#> fold (do_term false) ts 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

118 
end 
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset

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

120 
case strip_comb t of 
47933
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

121 
(Const x, ts) => do_const true ext_arg x ts 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

122 
 (Free x, ts) => do_const false ext_arg x ts 
38939  123 
 (Abs (_, T, t'), ts) => 
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset

124 
((null ts andalso not ext_arg) 
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset

125 
(* Since lambdas on the righthand side of equalities are usually 
47953
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47939
diff
changeset

126 
extensionalized later by "abs_extensionalize_term", we don't 
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47939
diff
changeset

127 
penalize them here. *) 
48219  128 
? add_pconst_to_table true (pseudo_abs_name, 
129 
PType (order_of_type T + 1, []))) 

42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

130 
#> fold (do_term false) (t' :: ts) 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

131 
 (_, ts) => fold (do_term false) ts 
38939  132 
fun do_quantifier will_surely_be_skolemized abs_T body_t = 
37537  133 
do_formula pos body_t 
38747  134 
#> (if also_skolems andalso will_surely_be_skolemized then 
48219  135 
add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (), 
136 
PType (order_of_type abs_T, [])) 

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

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

138 
I) 
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset

139 
and do_term_or_formula ext_arg T = 
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset

140 
if T = HOLogic.boolT then do_formula NONE else do_term ext_arg 
37537  141 
and do_formula pos t = 
142 
case t of 

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

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

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

42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset

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

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

151 
 @{const True} => I 
37537  152 
 @{const Not} $ t1 => do_formula (flip pos) t1 
38939  153 
 Const (@{const_name All}, _) $ Abs (_, T, t') => 
154 
do_quantifier (pos = SOME false) T t' 

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

156 
do_quantifier (pos = SOME true) T t' 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

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

158 
 @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2] 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

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

161 
 Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 => 
42741
546b0bda3cb8
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents:
42738
diff
changeset

162 
do_term_or_formula false T t1 #> do_term_or_formula true T t2 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

163 
 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

164 
$ t1 $ t2 $ t3 => 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

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

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

169 
do_quantifier (pos = SOME false) T 

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

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

172 
do_quantifier (pos = SOME true) T 

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

37537  174 
 (t0 as Const (_, @{typ bool})) $ t1 => 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

175 
do_term false t0 #> do_formula pos t1 (* theory constant *) 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

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

177 
in do_formula pos end 
24287  178 

48227  179 
fun pconsts_in_fact thy is_built_in_const t = 
180 
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) 

181 
(Symtab.empty > add_pconsts_in_term thy is_built_in_const true 

182 
(SOME true) t) [] 

183 

184 
val const_names_in_fact = map fst ooo pconsts_in_fact 

185 

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

187 
takes the given theory into account. *) 

41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

188 
fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...} 
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

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

190 
if exists (curry (op <) 0.0) [theory_const_rel_weight, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

191 
theory_const_irrel_weight] then 
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

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

193 
else 
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

194 
t 
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

195 

6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

196 
fun theory_const_prop_of fudge th = 
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

197 
theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th) 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

198 

48227  199 
fun pair_consts_fact thy is_built_in_const fudge fact = 
200 
case fact > snd > theory_const_prop_of fudge 

201 
> pconsts_in_fact thy is_built_in_const of 

202 
[] => NONE 

203 
 consts => SOME ((fact, consts), NONE) 

204 

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

207 
latter, we need a linear ordering on "pattern list". *) 
24287  208 

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

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

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

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

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

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

215 
prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2) 
38939  216 
fun ptype_ord (PType p, PType q) = 
217 
prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q) 

24287  218 

38939  219 
structure PType_Tab = Table(type key = ptype val ord = ptype_ord) 
24287  220 

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

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

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

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

224 
(* Twodimensional table update. Constant maps to types maps to count. *) 
41204
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

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

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

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

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

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

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

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

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

234 
in do_term o theory_const_prop_of fudge o snd end 
24287  235 

39367  236 
fun pow_int _ 0 = 1.0 
38939  237 
 pow_int x 1 = x 
238 
 pow_int x n = if n > 0 then x * pow_int x (n  1) else pow_int x (n + 1) / x 

239 

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

38686  244 

24287  245 

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

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

247 
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

248 

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

249 
(* "log" seems best in practice. A constant function of one ignores the constant 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

250 
frequencies. Rare constants give more points if they are relevant than less 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

251 
rare ones. *) 
39367  252 
fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0) 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

253 

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

254 
(* Irrelevant constants are treated differently. We associate lower penalties to 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

255 
very rare constants and very common ones  the former because they can't 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

256 
lead to the inclusion of too many new facts, and the latter because they are 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

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

258 
fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...} 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

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

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

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

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

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

265 

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

266 
fun multiplier_for_const_name local_const_multiplier s = 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

267 
if String.isSubstring "." s then 1.0 else local_const_multiplier 
38821  268 

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

269 
(* Computes a constant's weight, as determined by its frequency. *) 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

270 
fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

271 
theory_const_weight chained_const_weight weight_for f 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

272 
const_tab chained_const_tab (c as (s, PType (m, _))) = 
48219  273 
if s = pseudo_abs_name then 
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

274 
abs_weight 
48219  275 
else if String.isPrefix pseudo_skolem_prefix s then 
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

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

277 
else if String.isSuffix theory_const_suffix s then 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

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

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

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

281 
* weight_for m (pconst_freq (match_ptype o f) const_tab c) 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

282 
> (if chained_const_weight < 1.0 andalso 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

283 
pconst_hyper_mem I chained_const_tab c then 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

284 
curry (op *) chained_const_weight 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

285 
else 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

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

287 

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

288 
fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight, 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

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

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

291 
generic_pconst_weight local_const_multiplier abs_rel_weight 0.0 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

292 
theory_const_rel_weight 0.0 rel_weight_for I const_tab 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

293 
Symtab.empty 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

294 

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

295 
fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight, 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

296 
skolem_irrel_weight, 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

297 
theory_const_irrel_weight, 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

298 
chained_const_irrel_weight, ...}) 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

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

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

301 
skolem_irrel_weight theory_const_irrel_weight 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

302 
chained_const_irrel_weight (irrel_weight_for fudge) swap 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

303 
const_tab chained_const_tab 
24287  304 

46340  305 
fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) = 
306 
intro_bonus 

307 
 stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus 

308 
 stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus 

309 
 stature_bonus {local_bonus, ...} (Local, _) = local_bonus 

310 
 stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus 

311 
 stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus 

312 
 stature_bonus _ _ = 0.0 

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

313 

40418  314 
fun is_odd_const_name s = 
48219  315 
s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse 
40418  316 
String.isSuffix theory_const_suffix s 
317 

46340  318 
fun fact_weight fudge stature const_tab relevant_consts chained_consts 
319 
fact_consts = 

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

320 
case fact_consts > List.partition (pconst_hyper_mem I relevant_consts) 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

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

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

323 
 (rel, irrel) => 
40418  324 
if forall (forall (is_odd_const_name o fst)) [rel, irrel] then 
40371  325 
0.0 
326 
else 

327 
let 

42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

328 
val irrel = irrel > filter_out (pconst_mem swap rel) 
40371  329 
val rel_weight = 
330 
0.0 > fold (curry (op +) o rel_pconst_weight fudge const_tab) rel 

331 
val irrel_weight = 

46340  332 
~ (stature_bonus fudge stature) 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

333 
> fold (curry (op +) 
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42732
diff
changeset

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

38747  337 

48293  338 
fun take_most_relevant ctxt max_facts remaining_max 
42728
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset

339 
({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

340 
(candidates : ((fact * (string * ptype) list) * real) list) = 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

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

343 
Real.ceil (Math.pow (max_imperfect, 
38904  344 
Math.pow (Real.fromInt remaining_max 
48293  345 
/ Real.fromInt max_facts, max_imperfect_exp))) 
38747  346 
val (perfect, imperfect) = 
38889  347 
candidates > sort (Real.compare o swap o pairself snd) 
348 
> take_prefix (fn (_, w) => w > 0.99999) 

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

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

352 
trace_msg ctxt (fn () => 
41491  353 
"Actually passed (" ^ string_of_int (length accepts) ^ " of " ^ 
354 
string_of_int (length candidates) ^ "): " ^ 

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

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

357 
> commas)); 
38747  358 
(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

359 
end 
24287  360 

46340  361 
fun if_empty_replace_with_scope thy is_built_in_const facts sc tab = 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

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

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

364 
> fold (add_pconsts_in_term thy is_built_in_const false (SOME false)) 
46340  365 
(map_filter (fn ((_, (sc', _)), th) => 
366 
if sc' = sc then SOME (prop_of th) else NONE) facts) 

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

367 
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

368 
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

369 

42702  370 
fun consider_arities is_built_in_const th = 
41158
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

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

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

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

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

375 
t1 $ t2 => SOME tab > aux t1 (t2 :: args) > aux t2 [] 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

376 
 Const (x as (s, _)) => 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

377 
(if is_built_in_const x args > fst then 
41158
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

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

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

380 
NONE => SOME (Symtab.update (s, length args) tab) 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

381 
 SOME n => if n = length args then SOME tab else NONE) 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

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

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

384 

44785  385 
(* FIXME: This is currently only useful for polymorphic type encodings. *) 
42702  386 
fun could_benefit_from_ext is_built_in_const facts = 
387 
fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty) 

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

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

389 

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

390 
(* High enough so that it isn't wrongly considered as very relevant (e.g., for E 
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

391 
weights), but low enough so that it is unlikely to be truncated away if few 
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

392 
facts are included. *) 
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

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

394 

48293  395 
fun relevance_filter ctxt thres0 decay max_facts is_built_in_const 
48292  396 
(fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts 
397 
concl_t = 

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

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

400 
val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty 
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

401 
val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME 
48292  402 
val chained_ts = 
403 
facts > map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th) 

404 
 _ => NONE) 

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

405 
val chained_const_tab = Symtab.empty > fold (add_pconsts true) chained_ts 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

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

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

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

409 
> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab) 
46340  410 
> fold (if_empty_replace_with_scope thy is_built_in_const facts) 
38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

411 
[Chained, Assum, Local] 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

412 
fun iter j remaining_max thres rel_const_tab hopeless hopeful = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

413 
let 
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset

414 
fun relevant [] _ [] = 
38747  415 
(* Nothing has been added this iteration. *) 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

416 
if j = 0 andalso thres >= ridiculous_threshold then 
38747  417 
(* First iteration? Try again. *) 
48293  418 
iter 0 max_facts (thres / threshold_divisor) rel_const_tab 
38747  419 
hopeless hopeful 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

420 
else 
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset

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

423 
let 
38747  424 
val (accepts, more_rejects) = 
48293  425 
take_most_relevant ctxt max_facts remaining_max fudge candidates 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

428 
> fold (add_pconst_to_table false) (maps (snd o fst) accepts) 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

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

430 
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

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

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

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

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

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

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

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

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

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

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

441 
else SOME old_weight))) 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

442 
val thres = 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

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

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

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

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

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

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

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

451 
map (fst o fst) accepts @ 
38747  452 
(if remaining_max = 0 then 
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset

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

454 
else 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

455 
iter (j + 1) remaining_max thres rel_const_tab' 
38747  456 
hopeless_rejects hopeful_rejects) 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

457 
end 
38889  458 
 relevant candidates rejects 
46340  459 
(((ax as (((_, stature), _), fact_consts)), cached_weight) 
38747  460 
:: hopeful) = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

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

464 
SOME w => w 
46340  465 
 NONE => fact_weight fudge stature const_tab rel_const_tab 
42732
86683865278d
no penality for constants that appear in chained facts
blanchet
parents:
42730
diff
changeset

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

467 
in 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

468 
if weight >= thres then 
38889  469 
relevant ((ax, weight) :: candidates) rejects hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

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

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

475 
"ITERATION " ^ string_of_int j ^ ": current threshold: " ^ 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

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

477 
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

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

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

481 
end 
47933
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

482 
fun uses_const s t = 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

483 
fold_aterms (curry (fn (Const (s', _), false) => s' = s  (_, b) => b)) t 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

484 
false 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

485 
fun uses_const_anywhere accepts s = 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

486 
exists (uses_const s o prop_of o snd) accepts orelse 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

487 
exists (uses_const s) (concl_t :: hyp_ts) 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

488 
fun add_set_const_thms accepts = 
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

489 
exists (uses_const_anywhere accepts) set_consts ? append set_thms 
43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

490 
fun insert_into_facts accepts [] = accepts 
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

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

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

493 
val add = facts > filter (member Thm.eq_thm_prop ths o snd) 
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

494 
val (bef, after) = 
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

495 
accepts > filter_out (member Thm.eq_thm_prop ths o snd) 
48293  496 
> take (max_facts  length add) 
43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

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

498 
in bef @ add @ after end 
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

499 
fun insert_special_facts accepts = 
47939
9ff976a6c2cb
added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)
blanchet
parents:
47933
diff
changeset

500 
(* FIXME: get rid of "ext" here once it is treated as a helper *) 
43066
e0d4841c5b4a
fixed bug in appending special facts introduced in be0e66ccebfa  if several special facts were added, they overwrote each other
blanchet
parents:
42957
diff
changeset

501 
[] > could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext} 
47933
4e8e0245e8be
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
blanchet
parents:
47904
diff
changeset

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

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

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

505 
facts > map_filter (pair_consts_fact thy is_built_in_const fudge) 
48293  506 
> iter 0 max_facts thres0 goal_const_tab [] 
43492
43326cadc31a
insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents:
43477
diff
changeset

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

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

510 
end 
24287  511 

48406  512 
fun mepo_suggested_facts ctxt 
48293  513 
({fact_thresholds = (thres0, thres1), ...} : params) prover 
514 
max_facts fudge hyp_ts concl_t facts = 

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

515 
let 
42361  516 
val thy = Proof_Context.theory_of ctxt 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

517 
val is_built_in_const = 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

518 
Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

519 
val fudge = 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

520 
case fudge of 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

521 
SOME fudge => fudge 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

522 
 NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

523 
val decay = Math.pow ((1.0  thres1) / (1.0  thres0), 
48293  524 
1.0 / Real.fromInt (max_facts + 1)) 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

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

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

527 
" facts"); 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

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

529 
facts 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

530 
else if thres0 > 1.0 orelse thres0 > thres1 then 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

532 
else 
48293  533 
relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge 
534 
facts hyp_ts 

44625  535 
(concl_t > theory_constify fudge (Context.theory_name thy))) 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

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

537 

15347  538 
end; 