src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
author blanchet
Sat, 19 Jan 2013 17:42:12 +0100
changeset 50985 23bb011a5832
parent 50608 5977de2993ac
child 51004 5f2788c38127
permissions -rw-r--r--
tuning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48380
d4b7c7be3116 renamed ML files
blanchet
parents: 48308
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
38027
505657ddb047 standardize "Author" tags
blanchet
parents: 37995
diff changeset
     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
88c9aa5666de tuned comments
blanchet
parents: 39946
diff changeset
     4
48380
d4b7c7be3116 renamed ML files
blanchet
parents: 48308
diff changeset
     5
Sledgehammer's iterative relevance filter (MePo = Meng-Paulson).
33309
5f67433e6dd8 proper header;
wenzelm
parents: 33306
diff changeset
     6
*)
15452
e2a721567f67 Jia Meng: delta simpsets and clasets
paulson
parents: 15347
diff changeset
     7
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
     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
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
    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
blanchet
parents: 47976
diff changeset
    16
  val pseudo_abs_name : string
blanchet
parents: 47976
diff changeset
    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
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48381
diff changeset
    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
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    24
end;
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    25
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
    26
structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    27
struct
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    28
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46217
diff changeset
    29
open ATP_Problem_Generate
50608
5977de2993ac better weight functions for MePo/MaSh etc.
blanchet
parents: 50383
diff changeset
    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 eta-expansion 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
89674e5a4d35 make tracing an option
blanchet
parents: 48296
diff changeset
    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
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    37
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    38
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
48219
blanchet
parents: 47976
diff changeset
    39
val pseudo_abs_name = sledgehammer_prefix ^ "abs"
blanchet
parents: 47976
diff changeset
    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
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    44
    Int.max (order_of_type T1 + 1, order_of_type T2)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    45
  | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    46
  | order_of_type _ = 0
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    47
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
    48
(* An abstraction of Isabelle types and first-order 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
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    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
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    56
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
    57
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
    58
(*Is the second type an instance of the first one?*)
38824
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
    59
fun match_pattern (PVar, _) = true
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
    60
  | match_pattern (PApp _, PVar) = false
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
    61
  | match_pattern (PApp (s, ps), PApp (t, qs)) =
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
    62
    s = t andalso match_patterns (ps, qs)
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
    63
and match_patterns (_, []) = true
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
    64
  | match_patterns ([], _) = false
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
    65
  | match_patterns (p :: ps, q :: qs) =
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
    66
    match_pattern (p, q) andalso match_patterns (ps, qs)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    67
fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
    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 first-order term matching
blanchet
parents: 38825
diff changeset
    70
fun pconst_mem f consts (s, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    71
  exists (curry (match_ptype o f) ps)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
    72
         (map snd (filter (curry (op =) s o fst) consts))
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
    73
fun pconst_hyper_mem f const_tab (s, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    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 (non-CNF) formulas
blanchet
parents: 37504
diff changeset
    75
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    76
fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    77
  | pattern_for_type (TFree (s, _)) = PApp (s, [])
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    78
  | pattern_for_type (TVar _) = PVar
38827
cf01645cbbce extended relevance filter with first-order 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
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    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
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
    87
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    88
fun string_for_hyper_pconst (s, ps) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    89
  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
    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 built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
    93
fun add_pconst_to_table also_skolem (s, p) =
48219
blanchet
parents: 47976
diff changeset
    94
  if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I
41066
3890ef4e02f9 pass constant arguments to the built-in 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 built-in 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 (non-CNF) 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
209546e0af2c comment tuning
blanchet
parents: 41204
diff changeset
   107
       each quantifiers that must necessarily be skolemized by the automatic
209546e0af2c comment tuning
blanchet
parents: 41204
diff changeset
   108
       prover, we introduce a fresh constant to simulate the effect of
209546e0af2c comment tuning
blanchet
parents: 41204
diff changeset
   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 first-order 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
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   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 right-hand 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
blanchet
parents: 47976
diff changeset
   128
         ? add_pconst_to_table true (pseudo_abs_name,
blanchet
parents: 47976
diff changeset
   129
                                     PType (order_of_type T + 1, [])))
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   130
        #> fold (do_term false) (t' :: ts)
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   131
      | (_, ts) => fold (do_term false) ts
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   132
    fun do_quantifier will_surely_be_skolemized abs_T body_t =
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   133
      do_formula pos body_t
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   134
      #> (if also_skolems andalso will_surely_be_skolemized then
48219
blanchet
parents: 47976
diff changeset
   135
            add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (),
blanchet
parents: 47976
diff changeset
   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
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   141
    and do_formula pos t =
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   142
      case t of
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   143
        Const (@{const_name all}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   144
        do_quantifier (pos = SOME false) T t'
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   145
      | @{const "==>"} $ t1 $ t2 =>
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   146
        do_formula (flip pos) t1 #> do_formula pos t2
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   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
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   149
      | @{const Trueprop} $ t1 => do_formula pos t1
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   150
      | @{const False} => I
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   151
      | @{const True} => I
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   152
      | @{const Not} $ t1 => do_formula (flip pos) t1
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   153
      | Const (@{const_name All}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   154
        do_quantifier (pos = SOME false) T t'
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   155
      | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   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
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   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 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   165
        do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   166
      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   167
        do_quantifier (is_some pos) T t'
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   168
      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   169
        do_quantifier (pos = SOME false) T
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   170
                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   171
      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   172
        do_quantifier (pos = SOME true) T
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   173
                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   174
      | (t0 as Const (_, @{typ bool})) $ t1 =>
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   175
        do_term false t0 #> do_formula pos t1  (* theory constant *)
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   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
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   178
48227
blanchet
parents: 48219
diff changeset
   179
fun pconsts_in_fact thy is_built_in_const t =
blanchet
parents: 48219
diff changeset
   180
  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
blanchet
parents: 48219
diff changeset
   181
              (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
blanchet
parents: 48219
diff changeset
   182
                                                   (SOME true) t) []
blanchet
parents: 48219
diff changeset
   183
blanchet
parents: 48219
diff changeset
   184
val const_names_in_fact = map fst ooo pconsts_in_fact
blanchet
parents: 48219
diff changeset
   185
blanchet
parents: 48219
diff changeset
   186
(* Inserts a dummy "constant" referring to the theory name, so that relevance
blanchet
parents: 48219
diff changeset
   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 (non-CNF) 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 (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   198
48227
blanchet
parents: 48219
diff changeset
   199
fun pair_consts_fact thy is_built_in_const fudge fact =
blanchet
parents: 48219
diff changeset
   200
  case fact |> snd |> theory_const_prop_of fudge
blanchet
parents: 48219
diff changeset
   201
            |> pconsts_in_fact thy is_built_in_const of
blanchet
parents: 48219
diff changeset
   202
    [] => NONE
blanchet
parents: 48219
diff changeset
   203
  | consts => SOME ((fact, consts), NONE)
blanchet
parents: 48219
diff changeset
   204
38743
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   205
(* A two-dimensional symbol table counts frequencies of constants. It's keyed
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   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
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   208
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   209
fun pattern_ord p =
38743
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   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
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   216
fun ptype_ord (PType p, PType q) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   217
  prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   218
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   219
structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   220
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   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 first-order term matching
blanchet
parents: 38825
diff changeset
   223
    fun do_const const (s, T) ts =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   224
      (* Two-dimensional table update. Constant maps to types maps to count. *)
41204
bd57cf5944cb get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents: 41202
diff changeset
   225
      PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   226
      |> Symtab.map_default (s, PType_Tab.empty)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   227
      #> fold do_term ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   228
    and do_term t =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   229
      case strip_comb t of
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   230
        (Const x, ts) => do_const true x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   231
      | (Free x, ts) => do_const false x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   232
      | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
cf01645cbbce extended relevance filter with first-order 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
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   235
39367
blanchet
parents: 39366
diff changeset
   236
fun pow_int _ 0 = 1.0
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   237
  | pow_int x 1 = x
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   238
  | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   239
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   240
(*The frequency of a constant is the sum of those of all instances of its type.*)
38824
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   241
fun pconst_freq match const_tab (c, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   242
  PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   243
                 (the (Symtab.lookup const_tab c)) 0
38686
45eeee8d6b12 modified relevance filter
blanchet
parents: 38684
diff changeset
   244
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   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
blanchet
parents: 39366
diff changeset
   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
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   261
    (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   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
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   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 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   271
                          theory_const_weight chained_const_weight weight_for f
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   272
                          const_tab chained_const_tab (c as (s, PType (m, _))) =
48219
blanchet
parents: 47976
diff changeset
   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
blanchet
parents: 47976
diff changeset
   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 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   282
    |> (if chained_const_weight < 1.0 andalso
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   283
           pconst_hyper_mem I chained_const_tab c then
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   284
          curry (op *) chained_const_weight
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   285
        else
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   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 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   292
                        theory_const_rel_weight 0.0 rel_weight_for I const_tab
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   293
                        Symtab.empty
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   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 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   297
                                   theory_const_irrel_weight,
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   298
                                   chained_const_irrel_weight, ...})
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   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 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   302
                        chained_const_irrel_weight (irrel_weight_for fudge) swap
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   303
                        const_tab chained_const_tab
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   304
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   305
fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   306
    intro_bonus
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   307
  | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   308
  | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   309
  | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   310
  | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   311
  | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   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
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   314
fun is_odd_const_name s =
48219
blanchet
parents: 47976
diff changeset
   315
  s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
40418
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   316
  String.isSuffix theory_const_suffix s
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   317
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   318
fun fact_weight fudge stature const_tab relevant_consts chained_consts
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   319
                fact_consts =
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   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 lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   321
                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
38827
cf01645cbbce extended relevance filter with first-order 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
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   324
    if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
40371
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   325
      0.0
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   326
    else
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   327
      let
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   328
        val irrel = irrel |> filter_out (pconst_mem swap rel)
40371
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   329
        val rel_weight =
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   330
          0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   331
        val irrel_weight =
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   332
          ~ (stature_bonus fudge stature)
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   333
          |> fold (curry (op +)
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   334
                   o irrel_pconst_weight fudge const_tab chained_consts) irrel
40371
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   335
        val res = rel_weight / (rel_weight + irrel_weight)
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   336
      in if Real.isFinite res then res else 0.0 end
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   337
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   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
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   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
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   344
                    Math.pow (Real.fromInt remaining_max
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   345
                              / Real.fromInt max_facts, max_imperfect_exp)))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   346
    val (perfect, imperfect) =
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   347
      candidates |> sort (Real.compare o swap o pairself snd)
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   348
                 |> take_prefix (fn (_, w) => w > 0.99999)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   349
    val ((accepts, more_rejects), rejects) =
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   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
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41336
diff changeset
   353
        "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41336
diff changeset
   354
        string_of_int (length candidates) ^ "): " ^
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   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
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   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
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   360
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   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
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   365
            (map_filter (fn ((_, (sc', _)), th) =>
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   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
blanchet
parents: 42680
diff changeset
   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
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   385
(* FIXME: This is currently only useful for polymorphic type encodings. *)
42702
blanchet
parents: 42680
diff changeset
   386
fun could_benefit_from_ext is_built_in_const facts =
blanchet
parents: 42680
diff changeset
   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
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   395
fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   396
        (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   397
        concl_t =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   398
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   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 lower-level "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
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   402
    val chained_ts =
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   403
      facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   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
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   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
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   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
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   417
              (* First iteration? Try again. *)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   418
              iter 0 max_facts (thres / threshold_divisor) rel_const_tab
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   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
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   422
          | relevant candidates rejects [] =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   423
            let
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   424
              val (accepts, more_rejects) =
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   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 built-in 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
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   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 first-order 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
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   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
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   456
                      hopeless_rejects hopeful_rejects)
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   457
            end
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   458
          | relevant candidates rejects
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   459
                     (((ax as (((_, stature), _), fact_consts)), cached_weight)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   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
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   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
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   469
                relevant ((ax, weight) :: candidates) rejects hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   470
              else
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   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 first-order term matching
blanchet
parents: 38825
diff changeset
   479
                      |> map string_for_hyper_pconst));
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   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
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   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 built-ins
blanchet
parents: 40251
diff changeset
   505
    facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   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
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41336
diff changeset
   509
                      "Total relevant: " ^ string_of_int (length accepts)))
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   510
  end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   511
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48381
diff changeset
   512
fun mepo_suggested_facts ctxt
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   513
        ({fact_thresholds = (thres0, thres1), ...} : params) prover
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   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
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   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
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   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 lower-level "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
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   533
       relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   534
           facts hyp_ts
44625
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
   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 relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30364
diff changeset
   537
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   538
end;