1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -204,14 +204,13 @@
     1.4    andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
     1.5                             | _ => false) (prop_of th)
     1.6  
     1.7 -fun is_theorem_bad_for_atps ho_atp exporter thm =
     1.8 +fun is_theorem_bad_for_atps ho_atp thm =
     1.9    is_metastrange_theorem thm orelse
    1.10 -  (not exporter andalso
    1.11 -   let val t = prop_of thm in
    1.12 -     is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
    1.13 -     exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    1.14 -     is_that_fact thm
    1.15 -   end)
    1.16 +  let val t = prop_of thm in
    1.17 +    is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
    1.18 +    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    1.19 +    is_that_fact thm
    1.20 +  end
    1.21  
    1.22  fun hackish_string_for_term ctxt t =
    1.23    Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    1.24 @@ -346,7 +345,7 @@
    1.25  fun maybe_filter_no_atps ctxt =
    1.26    not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
    1.27  
    1.28 -fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
    1.29 +fun all_facts ctxt ho_atp reserved add_ths chained_ths css_table =
    1.30    let
    1.31      val thy = Proof_Context.theory_of ctxt
    1.32      val global_facts = Global_Theory.facts_of thy
    1.33 @@ -363,9 +362,10 @@
    1.34        Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
    1.35      fun add_facts global foldx facts =
    1.36        foldx (fn (name0, ths) =>
    1.37 -        if not exporter andalso name0 <> "" andalso
    1.38 +        if name0 <> "" andalso
    1.39             forall (not o member Thm.eq_thm_prop add_ths) ths andalso
    1.40             (Facts.is_concealed facts name0 orelse
    1.41 +            not (can (Proof_Context.get_thms ctxt) name0) orelse
    1.42              (not (Config.get ctxt ignore_no_atp) andalso
    1.43               is_package_def name0) orelse
    1.44              exists (fn s => String.isSuffix s name0)
    1.45 @@ -385,24 +385,22 @@
    1.46              #> fold (fn th => fn (j, (multis, unis)) =>
    1.47                          (j + 1,
    1.48                           if not (member Thm.eq_thm_prop add_ths th) andalso
    1.49 -                            is_theorem_bad_for_atps ho_atp exporter th then
    1.50 +                            is_theorem_bad_for_atps ho_atp th then
    1.51                             (multis, unis)
    1.52                           else
    1.53                             let
    1.54                               val new =
    1.55                                 (((fn () =>
    1.56 -                                 if name0 = "" then
    1.57 -                                   th |> backquote_thm
    1.58 -                                 else
    1.59 -                                   [Facts.extern ctxt facts name0,
    1.60 -                                    Name_Space.extern ctxt full_space name0,
    1.61 -                                    name0]
    1.62 -                                   |> find_first check_thms
    1.63 -                                   |> (fn SOME name =>
    1.64 -                                          make_name reserved multi j name
    1.65 -                                        | NONE => "")),
    1.66 -                                stature_of_thm global assms chained_ths
    1.67 -                                               css_table name0 th), th)
    1.68 +                                     if name0 = "" then
    1.69 +                                       th |> backquote_thm
    1.70 +                                     else
    1.71 +                                       [Facts.extern ctxt facts name0,
    1.72 +                                        Name_Space.extern ctxt full_space name0]
    1.73 +                                       |> find_first check_thms
    1.74 +                                       |> the_default name0
    1.75 +                                       |> make_name reserved multi j),
    1.76 +                                  stature_of_thm global assms chained_ths
    1.77 +                                                 css_table name0 th), th)
    1.78                             in
    1.79                               if multi then (new :: multis, unis)
    1.80                               else (multis, new :: unis)
    1.81 @@ -419,7 +417,7 @@
    1.82  
    1.83  fun all_facts_of thy css_table =
    1.84    let val ctxt = Proof_Context.init_global thy in
    1.85 -    all_facts ctxt false Symtab.empty true [] [] css_table
    1.86 +    all_facts ctxt false Symtab.empty [] [] css_table
    1.87      |> rev (* try to restore the original order of facts, for MaSh *)
    1.88    end
    1.89  
    1.90 @@ -438,7 +436,7 @@
    1.91                 o fact_from_ref ctxt reserved chained_ths css_table) add
    1.92         else
    1.93           let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    1.94 -           all_facts ctxt ho_atp reserved false add chained_ths css_table
    1.95 +           all_facts ctxt ho_atp reserved add chained_ths css_table
    1.96             |> filter_out (member Thm.eq_thm_prop del o snd)
    1.97             |> maybe_filter_no_atps ctxt
    1.98           end)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     2.3 @@ -564,7 +564,7 @@
     2.4    let
     2.5      val thy = Proof_Context.theory_of ctxt
     2.6      val prover = hd provers
     2.7 -    val name = ATP_Util.timestamp () ^ serial_string () (* fresh enough *)
     2.8 +    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
     2.9      val feats = features_of ctxt prover thy General [t]
    2.10      val deps = used_ths |> map Thm.get_name_hint
    2.11    in
    2.12 @@ -583,8 +583,7 @@
    2.13  (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    2.14     Sledgehammer and Try. *)
    2.15  val min_secs_for_learning = 15
    2.16 -val short_learn_timeout_factor = 0.2
    2.17 -val long_learn_timeout_factor = 4.0
    2.18 +val learn_timeout_factor = 2.0
    2.19  
    2.20  fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
    2.21          max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
    2.22 @@ -597,16 +596,13 @@
    2.23    else
    2.24      let
    2.25        val thy = Proof_Context.theory_of ctxt
    2.26 -      fun maybe_learn can_suggest =
    2.27 +      fun maybe_learn () =
    2.28          if not learn orelse Async_Manager.has_running_threads MaShN then
    2.29            ()
    2.30          else if Time.toSeconds timeout >= min_secs_for_learning then
    2.31            let
    2.32 -            val factor =
    2.33 -              if can_suggest then short_learn_timeout_factor
    2.34 -              else long_learn_timeout_factor
    2.35 -            val soft_timeout = time_mult factor timeout
    2.36 -            val hard_timeout = time_mult 2.0 soft_timeout
    2.37 +            val soft_timeout = time_mult learn_timeout_factor timeout
    2.38 +            val hard_timeout = time_mult 4.0 soft_timeout
    2.39              val birth_time = Time.now ()
    2.40              val death_time = Time.+ (birth_time, hard_timeout)
    2.41              val desc = ("machine learner for Sledgehammer", "")
    2.42 @@ -619,12 +615,10 @@
    2.43            ()
    2.44        val fact_filter =
    2.45          case fact_filter of
    2.46 -          SOME ff =>
    2.47 -          (if ff <> iterN then maybe_learn (mash_can_suggest_facts ctxt)
    2.48 -           else (); ff)
    2.49 +          SOME ff => (() |> ff <> iterN ? maybe_learn; ff)
    2.50          | NONE =>
    2.51 -          if mash_can_suggest_facts ctxt then (maybe_learn true; meshN)
    2.52 -          else if mash_could_suggest_facts () then (maybe_learn false; iterN)
    2.53 +          if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
    2.54 +          else if mash_could_suggest_facts () then (maybe_learn (); iterN)
    2.55            else iterN
    2.56        val add_ths = Attrib.eval_thms ctxt add
    2.57        fun prepend_facts ths accepts =