1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -372,10 +372,16 @@
     1.4          |> K ()
     1.5        end
     1.6      else if subcommand = minN then
     1.7 -      run_minimize (get_params Minimize ctxt
     1.8 -                               (("provers", [default_minimize_prover]) ::
     1.9 -                                override_params))
    1.10 -                   (K ()) (the_default 1 opt_i) (#add fact_override) state
    1.11 +      let
    1.12 +        val i = the_default 1 opt_i
    1.13 +        val params as {provers, ...} =
    1.14 +          get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
    1.15 +                                    override_params)
    1.16 +        val goal = prop_of (#goal (Proof.goal state))
    1.17 +        val facts = nearly_all_facts ctxt false fact_override Symtab.empty
    1.18 +                                     Termtab.empty [] [] goal
    1.19 +        val do_learn = mash_learn_proof ctxt params (hd provers) goal facts
    1.20 +      in run_minimize params do_learn i (#add fact_override) state end
    1.21      else if subcommand = messagesN then
    1.22        messages opt_i
    1.23      else if subcommand = supported_proversN then
    1.24 @@ -389,7 +395,7 @@
    1.25      else if subcommand = learnN orelse subcommand = relearnN then
    1.26        (if subcommand = relearnN then mash_unlearn ctxt else ();
    1.27         mash_learn ctxt (get_params Normal ctxt
    1.28 -                                   (("verbose", ["true"]) :: override_params)))
    1.29 +                                   (override_params @ [("verbose", ["true"])])))
    1.30      else if subcommand = kill_learnersN then
    1.31        kill_learners ()
    1.32      else if subcommand = running_learnersN then

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -54,7 +54,8 @@
     2.4      Proof.context -> params -> string -> int -> term list -> term
     2.5      -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
     2.6    val mash_learn_proof :
     2.7 -    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
     2.8 +    Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     2.9 +    -> unit
    2.10    val mash_learn_thy :
    2.11      Proof.context -> params -> theory -> Time.time -> fact list -> string
    2.12    val mash_learn : Proof.context -> params -> unit
    2.13 @@ -547,31 +548,46 @@
    2.14      val (deps, graph) = ([], graph) |> fold maybe_add_from deps
    2.15    in ((name, parents, feats, deps) :: upds, graph) end
    2.16  
    2.17 -val pass1_learn_timeout_factor = 0.5
    2.18 +val learn_timeout_slack = 2.0
    2.19  
    2.20 -fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
    2.21 +fun launch_thread timeout task =
    2.22    let
    2.23 -    val thy = Proof_Context.theory_of ctxt
    2.24 -    val prover = hd provers
    2.25 -    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
    2.26 -    val feats = features_of ctxt prover thy General [t]
    2.27 -    val deps = used_ths |> map nickname_of
    2.28 -  in
    2.29 -    mash_map ctxt (fn {thys, fact_graph} =>
    2.30 -        let
    2.31 -          val parents = parents_wrt_facts facts fact_graph
    2.32 -          val upds = [(name, parents, feats, deps)]
    2.33 -          val (upds, fact_graph) =
    2.34 -            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
    2.35 -        in
    2.36 -          mash_ADD ctxt overlord upds;
    2.37 -          {thys = thys, fact_graph = fact_graph}
    2.38 -        end)
    2.39 -  end
    2.40 +    val hard_timeout = time_mult learn_timeout_slack timeout
    2.41 +    val birth_time = Time.now ()
    2.42 +    val death_time = Time.+ (birth_time, hard_timeout)
    2.43 +    val desc = ("machine learner for Sledgehammer", "")
    2.44 +  in Async_Manager.launch MaShN birth_time death_time desc task end
    2.45 +
    2.46 +fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts
    2.47 +                     used_ths =
    2.48 +  if is_smt_prover ctxt prover then
    2.49 +    ()
    2.50 +  else
    2.51 +    launch_thread timeout
    2.52 +        (fn () =>
    2.53 +            let
    2.54 +              val thy = Proof_Context.theory_of ctxt
    2.55 +              val name = timestamp () ^ " " ^ serial_string () (* freshish *)
    2.56 +              val feats = features_of ctxt prover thy General [t]
    2.57 +              val deps = used_ths |> map nickname_of
    2.58 +            in
    2.59 +              mash_map ctxt (fn {thys, fact_graph} =>
    2.60 +                  let
    2.61 +                    val parents = parents_wrt_facts facts fact_graph
    2.62 +                    val upds = [(name, parents, feats, deps)]
    2.63 +                    val (upds, fact_graph) =
    2.64 +                      ([], fact_graph) |> fold (update_fact_graph ctxt) upds
    2.65 +                  in
    2.66 +                    mash_ADD ctxt overlord upds;
    2.67 +                    {thys = thys, fact_graph = fact_graph}
    2.68 +                  end);
    2.69 +              (true, "")
    2.70 +            end)
    2.71  
    2.72  (* Too many dependencies is a sign that a decision procedure is at work. There
    2.73     isn't much too learn from such proofs. *)
    2.74  val max_dependencies = 10
    2.75 +val pass1_learn_timeout_factor = 0.75
    2.76  
    2.77  (* The timeout is understood in a very slack fashion. *)
    2.78  fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
    2.79 @@ -647,7 +663,6 @@
    2.80  (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    2.81     Sledgehammer and Try. *)
    2.82  val min_secs_for_learning = 15
    2.83 -val learn_timeout_factor = 2.0
    2.84  
    2.85  fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
    2.86          max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
    2.87 @@ -661,19 +676,11 @@
    2.88      let
    2.89        val thy = Proof_Context.theory_of ctxt
    2.90        fun maybe_learn () =
    2.91 -        if not learn orelse Async_Manager.has_running_threads MaShN then
    2.92 -          ()
    2.93 -        else if Time.toSeconds timeout >= min_secs_for_learning then
    2.94 -          let
    2.95 -            val soft_timeout = time_mult learn_timeout_factor timeout
    2.96 -            val hard_timeout = time_mult 4.0 soft_timeout
    2.97 -            val birth_time = Time.now ()
    2.98 -            val death_time = Time.+ (birth_time, hard_timeout)
    2.99 -            val desc = ("machine learner for Sledgehammer", "")
   2.100 -          in
   2.101 -            Async_Manager.launch MaShN birth_time death_time desc
   2.102 -                (fn () =>
   2.103 -                    (true, mash_learn_thy ctxt params thy soft_timeout facts))
   2.104 +        if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
   2.105 +           Time.toSeconds timeout >= min_secs_for_learning then
   2.106 +          let val timeout = time_mult learn_timeout_slack timeout in
   2.107 +            launch_thread timeout
   2.108 +                (fn () => (true, mash_learn_thy ctxt params thy timeout facts))
   2.109            end
   2.110          else
   2.111            ()

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     3.3 @@ -255,11 +255,11 @@
     3.4       expect = expect}
     3.5    end
     3.6  
     3.7 -fun minimize ctxt mode do_learn name
     3.8 -             (params as {debug, verbose, isar_proof, minimize, ...})
     3.9 -             ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    3.10 -             (result as {outcome, used_facts, run_time, preplay, message,
    3.11 -                         message_tail} : prover_result) =
    3.12 +fun maybe_minimize ctxt mode do_learn name
    3.13 +        (params as {debug, verbose, isar_proof, minimize, ...})
    3.14 +        ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    3.15 +        (result as {outcome, used_facts, run_time, preplay, message,
    3.16 +                    message_tail} : prover_result) =
    3.17    if is_some outcome orelse null used_facts then
    3.18      result
    3.19    else
    3.20 @@ -328,7 +328,7 @@
    3.21  fun get_minimizing_prover ctxt mode do_learn name params minimize_command
    3.22                            problem =
    3.23    get_prover ctxt mode name params minimize_command problem
    3.24 -  |> minimize ctxt mode do_learn name params problem
    3.25 +  |> maybe_minimize ctxt mode do_learn name params problem
    3.26  
    3.27  fun run_minimize (params as {provers, ...}) do_learn i refs state =
    3.28    let

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
     4.3 @@ -87,7 +87,7 @@
     4.4      fun really_go () =
     4.5        problem
     4.6        |> get_minimizing_prover ctxt mode
     4.7 -             (mash_learn_proof ctxt params (prop_of goal)
     4.8 +             (mash_learn_proof ctxt params name (prop_of goal)
     4.9                                 (map untranslated_fact facts))
    4.10               name params minimize_command
    4.11        |> (fn {outcome, preplay, message, message_tail, ...} =>