1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -54,7 +54,8 @@
     1.4      Proof.context -> params -> string -> int -> term list -> term
     1.5      -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
     1.6    val mash_learn_proof :
     1.7 -    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
     1.8 +    Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     1.9 +    -> unit
    1.10    val mash_learn_thy :
    1.11      Proof.context -> params -> theory -> Time.time -> fact list -> string
    1.12    val mash_learn : Proof.context -> params -> unit
    1.13 @@ -547,31 +548,46 @@
    1.14      val (deps, graph) = ([], graph) |> fold maybe_add_from deps
    1.15    in ((name, parents, feats, deps) :: upds, graph) end
    1.16  
    1.17 -val pass1_learn_timeout_factor = 0.5
    1.18 +val learn_timeout_slack = 2.0
    1.19  
    1.20 -fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
    1.21 +fun launch_thread timeout task =
    1.22    let
    1.23 -    val thy = Proof_Context.theory_of ctxt
    1.24 -    val prover = hd provers
    1.25 -    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
    1.26 -    val feats = features_of ctxt prover thy General [t]
    1.27 -    val deps = used_ths |> map nickname_of
    1.28 -  in
    1.29 -    mash_map ctxt (fn {thys, fact_graph} =>
    1.30 -        let
    1.31 -          val parents = parents_wrt_facts facts fact_graph
    1.32 -          val upds = [(name, parents, feats, deps)]
    1.33 -          val (upds, fact_graph) =
    1.34 -            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
    1.35 -        in
    1.36 -          mash_ADD ctxt overlord upds;
    1.37 -          {thys = thys, fact_graph = fact_graph}
    1.38 -        end)
    1.39 -  end
    1.40 +    val hard_timeout = time_mult learn_timeout_slack timeout
    1.41 +    val birth_time = Time.now ()
    1.42 +    val death_time = Time.+ (birth_time, hard_timeout)
    1.43 +    val desc = ("machine learner for Sledgehammer", "")
    1.44 +  in Async_Manager.launch MaShN birth_time death_time desc task end
    1.45 +
    1.46 +fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts
    1.47 +                     used_ths =
    1.48 +  if is_smt_prover ctxt prover then
    1.49 +    ()
    1.50 +  else
    1.51 +    launch_thread timeout
    1.52 +        (fn () =>
    1.53 +            let
    1.54 +              val thy = Proof_Context.theory_of ctxt
    1.55 +              val name = timestamp () ^ " " ^ serial_string () (* freshish *)
    1.56 +              val feats = features_of ctxt prover thy General [t]
    1.57 +              val deps = used_ths |> map nickname_of
    1.58 +            in
    1.59 +              mash_map ctxt (fn {thys, fact_graph} =>
    1.60 +                  let
    1.61 +                    val parents = parents_wrt_facts facts fact_graph
    1.62 +                    val upds = [(name, parents, feats, deps)]
    1.63 +                    val (upds, fact_graph) =
    1.64 +                      ([], fact_graph) |> fold (update_fact_graph ctxt) upds
    1.65 +                  in
    1.66 +                    mash_ADD ctxt overlord upds;
    1.67 +                    {thys = thys, fact_graph = fact_graph}
    1.68 +                  end);
    1.69 +              (true, "")
    1.70 +            end)
    1.71  
    1.72  (* Too many dependencies is a sign that a decision procedure is at work. There
    1.73     isn't much too learn from such proofs. *)
    1.74  val max_dependencies = 10
    1.75 +val pass1_learn_timeout_factor = 0.75
    1.76  
    1.77  (* The timeout is understood in a very slack fashion. *)
    1.78  fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
    1.79 @@ -647,7 +663,6 @@
    1.80  (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    1.81     Sledgehammer and Try. *)
    1.82  val min_secs_for_learning = 15
    1.83 -val learn_timeout_factor = 2.0
    1.84  
    1.85  fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
    1.86          max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
    1.87 @@ -661,19 +676,11 @@
    1.88      let
    1.89        val thy = Proof_Context.theory_of ctxt
    1.90        fun maybe_learn () =
    1.91 -        if not learn orelse Async_Manager.has_running_threads MaShN then
    1.92 -          ()
    1.93 -        else if Time.toSeconds timeout >= min_secs_for_learning then
    1.94 -          let
    1.95 -            val soft_timeout = time_mult learn_timeout_factor timeout
    1.96 -            val hard_timeout = time_mult 4.0 soft_timeout
    1.97 -            val birth_time = Time.now ()
    1.98 -            val death_time = Time.+ (birth_time, hard_timeout)
    1.99 -            val desc = ("machine learner for Sledgehammer", "")
   1.100 -          in
   1.101 -            Async_Manager.launch MaShN birth_time death_time desc
   1.102 -                (fn () =>
   1.103 -                    (true, mash_learn_thy ctxt params thy soft_timeout facts))
   1.104 +        if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
   1.105 +           Time.toSeconds timeout >= min_secs_for_learning then
   1.106 +          let val timeout = time_mult learn_timeout_slack timeout in
   1.107 +            launch_thread timeout
   1.108 +                (fn () => (true, mash_learn_thy ctxt params thy timeout facts))
   1.109            end
   1.110          else
   1.111            ()