1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Aug 23 16:02:32 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Aug 23 16:14:26 2013 +0200
     1.3 @@ -311,10 +311,10 @@
     1.4    s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
     1.5    String.isSuffix theory_const_suffix s
     1.6  
     1.7 -fun fact_weight fudge stature const_tab relevant_consts chained_consts
     1.8 -                fact_consts =
     1.9 -  case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
    1.10 -                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
    1.11 +fun fact_weight fudge stature const_tab rel_const_tab rel_const_iter_tab
    1.12 +                chained_const_tab fact_consts =
    1.13 +  case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab)
    1.14 +                   ||> filter_out (pconst_hyper_mem swap rel_const_tab) of
    1.15      ([], _) => 0.0
    1.16    | (rel, irrel) =>
    1.17      if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
    1.18 @@ -327,7 +327,8 @@
    1.19          val irrel_weight =
    1.20            ~ (stature_bonus fudge stature)
    1.21            |> fold (curry (op +)
    1.22 -                   o irrel_pconst_weight fudge const_tab chained_consts) irrel
    1.23 +                   o irrel_pconst_weight fudge const_tab chained_const_tab)
    1.24 +                  irrel
    1.25          val res = rel_weight / (rel_weight + irrel_weight)
    1.26        in if Real.isFinite res then res else 0.0 end
    1.27  
    1.28 @@ -400,30 +401,36 @@
    1.29                              | _ => NONE)
    1.30      val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
    1.31      val goal_const_tab =
    1.32 -      Symtab.empty |> fold (add_pconsts true) hyp_ts
    1.33 -                   |> add_pconsts false concl_t
    1.34 +      Symtab.empty
    1.35 +      |> fold (add_pconsts true) hyp_ts
    1.36 +      |> add_pconsts false concl_t
    1.37        |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
    1.38        |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
    1.39                [Chained, Assum, Local]
    1.40 -    fun iter j remaining_max thres rel_const_tab hopeless hopeful =
    1.41 +    val goal_const_iter_tab = goal_const_tab |> Symtab.map (K (K ~1))
    1.42 +    fun iter j remaining_max thres rel_const_tab rel_const_iter_tab hopeless
    1.43 +             hopeful =
    1.44        let
    1.45          fun relevant [] _ [] =
    1.46              (* Nothing has been added this iteration. *)
    1.47              if j = 0 andalso thres >= ridiculous_threshold then
    1.48                (* First iteration? Try again. *)
    1.49                iter 0 max_facts (thres / threshold_divisor) rel_const_tab
    1.50 -                   hopeless hopeful
    1.51 +                   rel_const_iter_tab hopeless hopeful
    1.52              else
    1.53                []
    1.54            | relevant candidates rejects [] =
    1.55              let
    1.56                val (accepts, more_rejects) =
    1.57                  take_most_relevant ctxt max_facts remaining_max fudge candidates
    1.58 +              val sps = maps (snd o fst) accepts;
    1.59                val rel_const_tab' =
    1.60 -                rel_const_tab
    1.61 -                |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
    1.62 -              fun is_dirty (c, _) =
    1.63 -                Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
    1.64 +                rel_const_tab |> fold (add_pconst_to_table false) sps
    1.65 +              val rel_const_iter_tab' =
    1.66 +                rel_const_iter_tab
    1.67 +                |> fold (fn (s, _) => Symtab.default (s, j)) sps
    1.68 +              fun is_dirty (s, _) =
    1.69 +                Symtab.lookup rel_const_tab' s <> Symtab.lookup rel_const_tab s
    1.70                val (hopeful_rejects, hopeless_rejects) =
    1.71                   (rejects @ hopeless, ([], []))
    1.72                   |-> fold (fn (ax as (_, consts), old_weight) =>
    1.73 @@ -441,7 +448,8 @@
    1.74                val remaining_max = remaining_max - length accepts
    1.75              in
    1.76                trace_msg ctxt (fn () => "New or updated constants: " ^
    1.77 -                  commas (rel_const_tab' |> Symtab.dest
    1.78 +                  commas (rel_const_tab'
    1.79 +                          |> Symtab.dest
    1.80                            |> subtract (op =) (rel_const_tab |> Symtab.dest)
    1.81                            |> map string_of_hyper_pconst));
    1.82                map (fst o fst) accepts @
    1.83 @@ -449,7 +457,7 @@
    1.84                   []
    1.85                 else
    1.86                   iter (j + 1) remaining_max thres rel_const_tab'
    1.87 -                      hopeless_rejects hopeful_rejects)
    1.88 +                      rel_const_iter_tab' hopeless_rejects hopeful_rejects)
    1.89              end
    1.90            | relevant candidates rejects
    1.91                       (((ax as (((_, stature), _), fact_consts)), cached_weight)
    1.92 @@ -458,8 +466,9 @@
    1.93                val weight =
    1.94                  case cached_weight of
    1.95                    SOME w => w
    1.96 -                | NONE => fact_weight fudge stature const_tab rel_const_tab
    1.97 -                                      chained_const_tab fact_consts
    1.98 +                | NONE =>
    1.99 +                  fact_weight fudge stature const_tab rel_const_tab
   1.100 +                              rel_const_iter_tab chained_const_tab fact_consts
   1.101              in
   1.102                if weight >= thres then
   1.103                  relevant ((ax, weight) :: candidates) rejects hopeful
   1.104 @@ -470,7 +479,8 @@
   1.105            trace_msg ctxt (fn () =>
   1.106                "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
   1.107                Real.toString thres ^ ", constants: " ^
   1.108 -              commas (rel_const_tab |> Symtab.dest
   1.109 +              commas (rel_const_tab
   1.110 +                      |> Symtab.dest
   1.111                        |> filter (curry (op <>) [] o snd)
   1.112                        |> map string_of_hyper_pconst));
   1.113            relevant [] [] hopeful
   1.114 @@ -499,7 +509,7 @@
   1.115           |> insert_into_facts accepts
   1.116    in
   1.117      facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
   1.118 -          |> iter 0 max_facts thres0 goal_const_tab []
   1.119 +          |> iter 0 max_facts thres0 goal_const_tab goal_const_iter_tab []
   1.120            |> insert_special_facts
   1.121            |> tap (fn accepts => trace_msg ctxt (fn () =>
   1.122                        "Total relevant: " ^ string_of_int (length accepts)))