refactor large ML file
authorblanchet
Fri Jan 31 12:30:54 2014 +0100 (2014-01-31 ago)
changeset 552058450622db0c5
parent 55203 e872d196a73b
child 55206 f7358e55018f
refactor large ML file
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Sledgehammer.thy
src/HOL/TPTP/mash_eval.ML
src/HOL/TPTP/sledgehammer_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 10:34:20 2014 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 12:30:54 2014 +0100
     1.3 @@ -361,10 +361,10 @@
     1.4  
     1.5  fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
     1.6  
     1.7 -fun get_prover_name ctxt args =
     1.8 +fun get_prover_name thy args =
     1.9    let
    1.10      fun default_prover_name () =
    1.11 -      hd (#provers (Sledgehammer_Commands.default_params ctxt []))
    1.12 +      hd (#provers (Sledgehammer_Commands.default_params thy []))
    1.13        handle List.Empty => error "No ATP available."
    1.14    in
    1.15      (case AList.lookup (op =) args proverK of
    1.16 @@ -417,6 +417,7 @@
    1.17        hard_timeout timeout preplay_timeout sh_minimizeLST
    1.18        max_new_mono_instancesLST max_mono_itersLST dir pos st =
    1.19    let
    1.20 +    val thy = Proof.theory_of st
    1.21      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
    1.22      val i = 1
    1.23      fun set_file_name (SOME dir) =
    1.24 @@ -438,7 +439,7 @@
    1.25              #> (Option.map (Config.put ATP_Systems.force_sos)
    1.26                    force_sos |> the_default I))
    1.27      val params as {max_facts, ...} =
    1.28 -      Sledgehammer_Commands.default_params ctxt
    1.29 +      Sledgehammer_Commands.default_params thy
    1.30           ([("verbose", "true"),
    1.31             ("fact_filter", fact_filter),
    1.32             ("type_enc", type_enc),
    1.33 @@ -452,7 +453,8 @@
    1.34            |> sh_minimizeLST (*don't confuse the two minimization flags*)
    1.35            |> max_new_mono_instancesLST
    1.36            |> max_mono_itersLST)
    1.37 -    val default_max_facts = Sledgehammer_Prover.default_max_facts_of_prover ctxt prover_name
    1.38 +    val default_max_facts =
    1.39 +      Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name
    1.40      val is_appropriate_prop =
    1.41        Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt prover_name
    1.42      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
    1.43 @@ -510,11 +512,12 @@
    1.44  fun run_sledgehammer trivial args reconstructor named_thms id
    1.45        ({pre=st, log, pos, ...}: Mirabelle.run_args) =
    1.46    let
    1.47 +    val thy = Proof.theory_of st
    1.48      val ctxt = Proof.context_of st
    1.49      val triv_str = if trivial then "[T] " else ""
    1.50      val _ = change_data id inc_sh_calls
    1.51      val _ = if trivial then () else change_data id inc_sh_nontriv_calls
    1.52 -    val prover_name = get_prover_name ctxt args
    1.53 +    val prover_name = get_prover_name thy args
    1.54      val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default
    1.55      val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
    1.56      val strict = AList.lookup (op =) args strictK |> the_default strict_default
    1.57 @@ -580,10 +583,11 @@
    1.58  fun run_minimize args reconstructor named_thms id
    1.59          ({pre=st, log, ...}: Mirabelle.run_args) =
    1.60    let
    1.61 +    val thy = Proof.theory_of st
    1.62      val ctxt = Proof.context_of st
    1.63      val {goal, ...} = Proof.goal st
    1.64      val n0 = length (these (!named_thms))
    1.65 -    val prover_name = get_prover_name ctxt args
    1.66 +    val prover_name = get_prover_name thy args
    1.67      val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
    1.68      val strict = AList.lookup (op =) args strictK |> the_default strict_default
    1.69      val timeout =
    1.70 @@ -596,7 +600,7 @@
    1.71      val max_new_mono_instancesLST =
    1.72        available_parameter args max_new_mono_instancesK max_new_mono_instancesK
    1.73      val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
    1.74 -    val params = Sledgehammer_Commands.default_params ctxt
    1.75 +    val params = Sledgehammer_Commands.default_params thy
    1.76       ([("provers", prover_name),
    1.77         ("verbose", "true"),
    1.78         ("type_enc", type_enc),
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 10:34:20 2014 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 12:30:54 2014 +0100
     2.3 @@ -11,25 +11,18 @@
     2.4    | NONE => default_value
     2.5  
     2.6  fun extract_relevance_fudge args
     2.7 -      {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight,
     2.8 -       abs_rel_weight, abs_irrel_weight, theory_const_rel_weight,
     2.9 -       theory_const_irrel_weight, chained_const_irrel_weight, intro_bonus,
    2.10 -       elim_bonus, simp_bonus, local_bonus, assum_bonus, chained_bonus,
    2.11 -       max_imperfect, max_imperfect_exp, threshold_divisor,
    2.12 -       ridiculous_threshold} =
    2.13 -  {local_const_multiplier =
    2.14 -       get args "local_const_multiplier" local_const_multiplier,
    2.15 +      {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight,
    2.16 +       abs_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight,
    2.17 +       chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus,
    2.18 +       chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
    2.19 +  {local_const_multiplier = get args "local_const_multiplier" local_const_multiplier,
    2.20     worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
    2.21 -   higher_order_irrel_weight =
    2.22 -       get args "higher_order_irrel_weight" higher_order_irrel_weight,
    2.23 +   higher_order_irrel_weight = get args "higher_order_irrel_weight" higher_order_irrel_weight,
    2.24     abs_rel_weight = get args "abs_rel_weight" abs_rel_weight,
    2.25     abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight,
    2.26 -   theory_const_rel_weight =
    2.27 -       get args "theory_const_rel_weight" theory_const_rel_weight,
    2.28 -   theory_const_irrel_weight =
    2.29 -       get args "theory_const_irrel_weight" theory_const_irrel_weight,
    2.30 -   chained_const_irrel_weight =
    2.31 -       get args "chained_const_irrel_weight" chained_const_irrel_weight,
    2.32 +   theory_const_rel_weight = get args "theory_const_rel_weight" theory_const_rel_weight,
    2.33 +   theory_const_irrel_weight = get args "theory_const_irrel_weight" theory_const_irrel_weight,
    2.34 +   chained_const_irrel_weight = get args "chained_const_irrel_weight" chained_const_irrel_weight,
    2.35     intro_bonus = get args "intro_bonus" intro_bonus,
    2.36     elim_bonus = get args "elim_bonus" elim_bonus,
    2.37     simp_bonus = get args "simp_bonus" simp_bonus,
    2.38 @@ -56,17 +49,17 @@
    2.39  fun get id c = the_default 0 (AList.lookup (op =) (!c) id)
    2.40  fun add id c n =
    2.41    c := (case AList.lookup (op =) (!c) id of
    2.42 -          SOME m => AList.update (op =) (id, m + n) (!c)
    2.43 -        | NONE => (id, n) :: !c)
    2.44 +         SOME m => AList.update (op =) (id, m + n) (!c)
    2.45 +       | NONE => (id, n) :: !c)
    2.46  
    2.47  fun init proof_file _ thy =
    2.48    let
    2.49      fun do_line line =
    2.50 -      case line |> space_explode ":" of
    2.51 +      (case line |> space_explode ":" of
    2.52          [line_num, offset, proof] =>
    2.53          SOME (pairself (the o Int.fromString) (line_num, offset),
    2.54                proof |> space_explode " " |> filter_out (curry (op =) ""))
    2.55 -       | _ => NONE
    2.56 +       | _ => NONE)
    2.57      val proofs = File.read (Path.explode proof_file)
    2.58      val proof_tab =
    2.59        proofs |> space_explode "\n"
    2.60 @@ -81,21 +74,18 @@
    2.61  fun done id ({log, ...} : Mirabelle.done_args) =
    2.62    if get id num_successes + get id num_failures > 0 then
    2.63      (log "";
    2.64 -     log ("Number of overall successes: " ^
    2.65 -          string_of_int (get id num_successes));
    2.66 +     log ("Number of overall successes: " ^ string_of_int (get id num_successes));
    2.67       log ("Number of overall failures: " ^ string_of_int (get id num_failures));
    2.68       log ("Overall success rate: " ^
    2.69            percentage_alt (get id num_successes) (get id num_failures) ^ "%");
    2.70       log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs));
    2.71       log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs));
    2.72       log ("Proof found rate: " ^
    2.73 -          percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^
    2.74 -          "%");
    2.75 +          percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^ "%");
    2.76       log ("Number of found facts: " ^ string_of_int (get id num_found_facts));
    2.77       log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts));
    2.78       log ("Fact found rate: " ^
    2.79 -          percentage_alt (get id num_found_facts) (get id num_lost_facts) ^
    2.80 -          "%"))
    2.81 +          percentage_alt (get id num_found_facts) (get id num_lost_facts) ^ "%"))
    2.82    else
    2.83      ()
    2.84  
    2.85 @@ -109,13 +99,12 @@
    2.86      (case Prooftab.lookup (!proof_table) (line_num, offset) of
    2.87         SOME proofs =>
    2.88         let
    2.89 +         val thy = Proof.theory_of pre
    2.90           val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
    2.91           val prover = AList.lookup (op =) args "prover" |> the_default default_prover
    2.92 -         val params as {max_facts, ...} =
    2.93 -           Sledgehammer_Commands.default_params ctxt args
    2.94 -         val default_max_facts = Sledgehammer_Prover.default_max_facts_of_prover ctxt prover
    2.95 -         val is_appropriate_prop =
    2.96 -           Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt default_prover
    2.97 +         val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args
    2.98 +         val default_max_facts =
    2.99 +           Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover
   2.100           val relevance_fudge =
   2.101             extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge
   2.102           val subgoal = 1
   2.103 @@ -127,7 +116,6 @@
   2.104             Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
   2.105                 Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
   2.106                 hyp_ts concl_t
   2.107 -           |> filter (is_appropriate_prop o prop_of o snd)
   2.108             |> Sledgehammer_Fact.drop_duplicate_facts
   2.109             |> Sledgehammer_MePo.mepo_suggested_facts ctxt params
   2.110                    (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t
   2.111 @@ -156,8 +144,7 @@
   2.112             else
   2.113               let
   2.114                 val found_weight =
   2.115 -                 Real.fromInt (fold (fn (n, _) =>
   2.116 -                                        Integer.add (n * n)) found_facts 0)
   2.117 +                 Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0)
   2.118                     / Real.fromInt (length found_facts)
   2.119                   |> Math.sqrt |> Real.ceil
   2.120               in
   2.121 @@ -178,11 +165,11 @@
   2.122  
   2.123  fun invoke args =
   2.124    let
   2.125 -    val (pf_args, other_args) =
   2.126 -      args |> List.partition (curry (op =) proof_fileK o fst)
   2.127 -    val proof_file = case pf_args of
   2.128 -                       [] => error "No \"proof_file\" specified"
   2.129 -                     | (_, s) :: _ => s
   2.130 +    val (pf_args, other_args) = args |> List.partition (curry (op =) proof_fileK o fst)
   2.131 +    val proof_file =
   2.132 +      (case pf_args of
   2.133 +        [] => error "No \"proof_file\" specified"
   2.134 +      | (_, s) :: _ => s)
   2.135    in Mirabelle.register (init proof_file, action other_args, done) end
   2.136  
   2.137  end;
     3.1 --- a/src/HOL/Sledgehammer.thy	Fri Jan 31 10:34:20 2014 +0100
     3.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jan 31 12:30:54 2014 +0100
     3.3 @@ -27,6 +27,8 @@
     3.4  ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
     3.5  ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
     3.6  ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
     3.7 +ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
     3.8 +ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
     3.9  ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
    3.10  ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
    3.11  ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
     4.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 10:34:20 2014 +0100
     4.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 12:30:54 2014 +0100
     4.3 @@ -46,12 +46,12 @@
     4.4          mepo_file_name mash_isar_file_name mash_prover_file_name
     4.5          mesh_isar_file_name mesh_prover_file_name report_file_name =
     4.6    let
     4.7 +    val thy = Proof_Context.theory_of ctxt
     4.8      val zeros = [0, 0, 0, 0, 0, 0]
     4.9      val report_path = report_file_name |> Path.explode
    4.10      val _ = File.write report_path ""
    4.11      fun print s = File.append report_path (s ^ "\n")
    4.12 -    val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
    4.13 -      default_params ctxt []
    4.14 +    val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
    4.15      val prover = hd provers
    4.16      val slack_max_facts = generous_max_facts (the max_facts)
    4.17      val lines_of = Path.explode #> try File.read_lines #> these
     5.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 10:34:20 2014 +0100
     5.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 12:30:54 2014 +0100
     5.3 @@ -21,13 +21,15 @@
     5.4  open Sledgehammer_Util
     5.5  open Sledgehammer_Fact
     5.6  open Sledgehammer_Prover
     5.7 +open Sledgehammer_Prover_Minimize
     5.8  open Sledgehammer_MaSh
     5.9  open Sledgehammer_Commands
    5.10  
    5.11  fun run_prover override_params fact_override i n ctxt goal =
    5.12    let
    5.13 +    val thy = Proof_Context.theory_of ctxt
    5.14      val mode = Normal
    5.15 -    val params as {provers, max_facts, ...} = default_params ctxt override_params
    5.16 +    val params as {provers, max_facts, ...} = default_params thy override_params
    5.17      val name = hd provers
    5.18      val prover = get_prover ctxt mode name
    5.19      val default_max_facts = default_max_facts_of_prover ctxt name
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Jan 31 10:34:20 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Jan 31 12:30:54 2014 +0100
     6.3 @@ -9,7 +9,7 @@
     6.4    type params = Sledgehammer_Prover.params
     6.5  
     6.6    val provers : string Unsynchronized.ref
     6.7 -  val default_params : Proof.context -> (string * string) list -> params
     6.8 +  val default_params : theory -> (string * string) list -> params
     6.9  end;
    6.10  
    6.11  structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS =
    6.12 @@ -193,9 +193,9 @@
    6.13  
    6.14  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    6.15     timeout, it makes sense to put E first. *)
    6.16 -fun default_provers_param_value mode ctxt =
    6.17 +fun default_provers_param_value mode thy =
    6.18    [eN, spassN, z3N, vampireN, e_sineN, yicesN]
    6.19 -  |> map_filter (remotify_prover_if_not_installed ctxt)
    6.20 +  |> map_filter (remotify_atp_if_not_installed thy)
    6.21    (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
    6.22    |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
    6.23    |> implode_param
    6.24 @@ -205,18 +205,14 @@
    6.25      thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
    6.26    end
    6.27  
    6.28 -fun default_raw_params mode ctxt =
    6.29 -  let val thy = Proof_Context.theory_of ctxt in
    6.30 -    Data.get thy
    6.31 -    |> fold (AList.default (op =))
    6.32 -            [("provers", [case !provers of
    6.33 -                            "" => default_provers_param_value mode ctxt
    6.34 -                          | s => s]),
    6.35 -             ("timeout", let val timeout = Options.default_int @{option sledgehammer_timeout} in
    6.36 -                           [if timeout <= 0 then "none"
    6.37 -                            else string_of_int timeout]
    6.38 -                         end)]
    6.39 -  end
    6.40 +fun default_raw_params mode thy =
    6.41 +  Data.get thy
    6.42 +  |> fold (AList.default (op =))
    6.43 +       [("provers", [(case !provers of "" => default_provers_param_value mode thy | s => s)]),
    6.44 +        ("timeout",
    6.45 +         let val timeout = Options.default_int @{option sledgehammer_timeout} in
    6.46 +           [if timeout <= 0 then "none" else string_of_int timeout]
    6.47 +         end)]
    6.48  
    6.49  fun extract_params mode default_params override_params =
    6.50    let
    6.51 @@ -342,15 +338,16 @@
    6.52  
    6.53  fun hammer_away override_params subcommand opt_i fact_override state =
    6.54    let
    6.55 +    val thy = Proof.theory_of state
    6.56      val ctxt = Proof.context_of state
    6.57 +
    6.58      val override_params = override_params |> map (normalize_raw_param ctxt)
    6.59      val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
    6.60    in
    6.61      if subcommand = runN then
    6.62        let val i = the_default 1 opt_i in
    6.63 -        run_sledgehammer (get_params Normal ctxt override_params) Normal NONE i
    6.64 -                         fact_override (minimize_command override_params i)
    6.65 -                         state
    6.66 +        run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override
    6.67 +          (minimize_command override_params i) state
    6.68          |> K ()
    6.69        end
    6.70      else if subcommand = minN then
    6.71 @@ -358,8 +355,7 @@
    6.72          val ctxt = ctxt |> Config.put instantiate_inducts false
    6.73          val i = the_default 1 opt_i
    6.74          val params =
    6.75 -          get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
    6.76 -                                    override_params)
    6.77 +          get_params Minimize thy (("provers", [default_minimize_prover]) :: override_params)
    6.78          val goal = prop_of (#goal (Proof.goal state))
    6.79          val facts = nearly_all_facts ctxt false fact_override Symtab.empty
    6.80                                       Termtab.empty [] [] goal
    6.81 @@ -371,22 +367,21 @@
    6.82        supported_provers ctxt
    6.83      else if subcommand = kill_allN then
    6.84        (kill_provers ();
    6.85 -       kill_learners ctxt (get_params Normal ctxt override_params))
    6.86 +       kill_learners ctxt (get_params Normal thy override_params))
    6.87      else if subcommand = running_proversN then
    6.88        running_provers ()
    6.89      else if subcommand = unlearnN then
    6.90 -      mash_unlearn ctxt (get_params Normal ctxt override_params)
    6.91 +      mash_unlearn ctxt (get_params Normal thy override_params)
    6.92      else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
    6.93              subcommand = relearn_isarN orelse subcommand = relearn_proverN then
    6.94        (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then
    6.95 -         mash_unlearn ctxt (get_params Normal ctxt override_params)
    6.96 +         mash_unlearn ctxt (get_params Normal thy override_params)
    6.97         else
    6.98           ();
    6.99         mash_learn ctxt
   6.100             (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
   6.101 -           (get_params Normal ctxt
   6.102 -                ([("timeout",
   6.103 -                   [string_of_real default_learn_prover_timeout]),
   6.104 +           (get_params Normal thy
   6.105 +                ([("timeout", [string_of_real default_learn_prover_timeout]),
   6.106                    ("slice", ["false"])] @
   6.107                   override_params @
   6.108                   [("minimize", ["true"]),
   6.109 @@ -410,16 +405,12 @@
   6.110  
   6.111  fun sledgehammer_params_trans params =
   6.112    Toplevel.theory
   6.113 -      (fold set_default_raw_param params
   6.114 -       #> tap (fn thy =>
   6.115 -                  let val ctxt = Proof_Context.init_global thy in
   6.116 -                    writeln ("Default parameters for Sledgehammer:\n" ^
   6.117 -                             (case rev (default_raw_params Normal ctxt) of
   6.118 -                                [] => "none"
   6.119 -                              | params =>
   6.120 -                                params |> map string_of_raw_param
   6.121 -                                       |> sort_strings |> cat_lines))
   6.122 -                  end))
   6.123 +    (fold set_default_raw_param params
   6.124 +     #> tap (fn thy =>
   6.125 +          writeln ("Default parameters for Sledgehammer:\n" ^
   6.126 +            (case rev (default_raw_params Normal thy) of
   6.127 +              [] => "none"
   6.128 +            | params => params |> map string_of_raw_param |> sort_strings |> cat_lines))))
   6.129  
   6.130  val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
   6.131  val parse_key =
   6.132 @@ -451,12 +442,12 @@
   6.133  
   6.134  fun try_sledgehammer auto state =
   6.135    let
   6.136 -    val ctxt = Proof.context_of state
   6.137 +    val thy = Proof.theory_of state
   6.138      val mode = if auto then Auto_Try else Try
   6.139      val i = 1
   6.140    in
   6.141 -    run_sledgehammer (get_params mode ctxt []) mode NONE i no_fact_override
   6.142 -                     (minimize_command [] i) state
   6.143 +    run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (minimize_command [] i)
   6.144 +      state
   6.145    end
   6.146  
   6.147  val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
   6.148 @@ -466,8 +457,9 @@
   6.149      (case try Toplevel.proof_of st of
   6.150        SOME state =>
   6.151          let
   6.152 -          val [provers_arg, isar_proofs_arg] = args;
   6.153 +          val thy = Proof.theory_of state
   6.154            val ctxt = Proof.context_of state
   6.155 +          val [provers_arg, isar_proofs_arg] = args
   6.156  
   6.157            val override_params =
   6.158              ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
   6.159 @@ -478,9 +470,9 @@
   6.160                 ("verbose", ["false"]),
   6.161                 ("overlord", ["false"])])
   6.162              |> map (normalize_raw_param ctxt)
   6.163 -          val _ =
   6.164 -            run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
   6.165 -              no_fact_override (minimize_command override_params 1) state
   6.166 +
   6.167 +          val _ = run_sledgehammer (get_params Normal thy override_params) Normal
   6.168 +            (SOME output_result) 1 no_fact_override (minimize_command override_params 1) state
   6.169          in () end
   6.170      | NONE => error "Unknown proof context"))
   6.171  
   6.172 @@ -489,8 +481,8 @@
   6.173  val _ = Isabelle_Process.protocol_command "Sledgehammer.provers"
   6.174    (fn [] =>
   6.175      let
   6.176 -      val this_ctxt = @{context}
   6.177 -      val provers = space_implode " " (#provers (default_params this_ctxt []))
   6.178 +      val this_thy = @{theory}
   6.179 +      val provers = space_implode " " (#provers (default_params this_thy []))
   6.180      in Output.protocol_message Markup.sledgehammer_provers provers end)
   6.181  
   6.182  end;
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 10:34:20 2014 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 12:30:54 2014 +0100
     7.3 @@ -130,7 +130,6 @@
     7.4      (t', subst)
     7.5    end
     7.6  
     7.7 -
     7.8  (* (4) Typing-spot table *)
     7.9  local
    7.10  fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 10:34:20 2014 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 12:30:54 2014 +0100
     8.3 @@ -69,49 +69,35 @@
     8.4    val problem_prefix : string Config.T
     8.5    val completish : bool Config.T
     8.6    val atp_full_names : bool Config.T
     8.7 -  val smt_builtins : bool Config.T
     8.8 -  val smt_triggers : bool Config.T
     8.9 -  val smt_weights : bool Config.T
    8.10 -  val smt_weight_min_facts : int Config.T
    8.11 -  val smt_min_weight : int Config.T
    8.12 -  val smt_max_weight : int Config.T
    8.13 -  val smt_max_weight_index : int Config.T
    8.14 -  val smt_weight_curve : (int -> int) Unsynchronized.ref
    8.15 -  val smt_max_slices : int Config.T
    8.16 -  val smt_slice_fact_frac : real Config.T
    8.17 -  val smt_slice_time_frac : real Config.T
    8.18 -  val smt_slice_min_secs : int Config.T
    8.19    val SledgehammerN : string
    8.20    val plain_metis : reconstructor
    8.21 -  val select_smt_solver : string -> Proof.context -> Proof.context
    8.22 +  val overlord_file_location_of_prover : string -> string * string
    8.23 +  val proof_banner : mode -> string -> string
    8.24    val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
    8.25    val is_reconstructor : string -> bool
    8.26    val is_atp : theory -> string -> bool
    8.27 -  val is_smt_prover : Proof.context -> string -> bool
    8.28    val is_ho_atp: Proof.context -> string -> bool
    8.29    val is_unit_equational_atp : Proof.context -> string -> bool
    8.30 -  val is_prover_supported : Proof.context -> string -> bool
    8.31 -  val is_prover_installed : Proof.context -> string -> bool
    8.32 -  val remotify_prover_if_supported_and_not_already_remote :
    8.33 -    Proof.context -> string -> string option
    8.34 -  val remotify_prover_if_not_installed :
    8.35 -    Proof.context -> string -> string option
    8.36 -  val default_max_facts_of_prover : Proof.context -> string -> int
    8.37    val is_unit_equality : term -> bool
    8.38    val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
    8.39 -  val weight_smt_fact :
    8.40 -    Proof.context -> int -> ((string * stature) * thm) * int
    8.41 -    -> (string * stature) * (int option * thm)
    8.42    val supported_provers : Proof.context -> unit
    8.43    val kill_provers : unit -> unit
    8.44    val running_provers : unit -> unit
    8.45    val messages : int option -> unit
    8.46    val is_fact_chained : (('a * stature) * 'b) -> bool
    8.47 +  val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
    8.48    val filter_used_facts :
    8.49      bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    8.50      ((''a * stature) * 'b) list
    8.51 -  val isar_proof_reconstructor : Proof.context -> string -> string
    8.52 -  val get_prover : Proof.context -> mode -> string -> prover
    8.53 +  val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
    8.54 +    Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome
    8.55 +  val remotify_atp_if_not_installed : theory -> string -> string option
    8.56 +  val isar_supported_prover_of : theory -> string -> string
    8.57 +  val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
    8.58 +    string -> reconstructor * play_outcome -> 'a
    8.59 +  val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
    8.60 +    Proof.context
    8.61 +  val run_reconstructor : mode -> string -> prover
    8.62  end;
    8.63  
    8.64  structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
    8.65 @@ -130,9 +116,6 @@
    8.66  open Sledgehammer_Isar_Print
    8.67  open Sledgehammer_Isar
    8.68  
    8.69 -
    8.70 -(** The Sledgehammer **)
    8.71 -
    8.72  (* Empty string means create files in Isabelle's temporary files directory. *)
    8.73  val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
    8.74  val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
    8.75 @@ -143,12 +126,6 @@
    8.76     provers (e.g., E). For these reason, short names are enabled by default. *)
    8.77  val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
    8.78  
    8.79 -val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
    8.80 -val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
    8.81 -val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
    8.82 -val smt_weight_min_facts =
    8.83 -  Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
    8.84 -
    8.85  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    8.86  
    8.87  (* Identifier that distinguishes Sledgehammer from other tools that could use
    8.88 @@ -161,61 +138,28 @@
    8.89  
    8.90  val is_atp = member (op =) o supported_atps
    8.91  
    8.92 -val select_smt_solver = Context.proof_map o SMT_Config.select_solver
    8.93 -
    8.94 -fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
    8.95 -
    8.96  fun is_atp_of_format is_format ctxt name =
    8.97    let val thy = Proof_Context.theory_of ctxt in
    8.98 -    case try (get_atp thy) name of
    8.99 +    (case try (get_atp thy) name of
   8.100        SOME config =>
   8.101 -      exists (fn (_, ((_, format, _, _, _), _)) => is_format format)
   8.102 -             (#best_slices (config ()) ctxt)
   8.103 -    | NONE => false
   8.104 +      exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
   8.105 +    | NONE => false)
   8.106    end
   8.107  
   8.108  val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ)
   8.109  val is_ho_atp = is_atp_of_format is_format_higher_order
   8.110  
   8.111 -fun is_prover_supported ctxt =
   8.112 -  let val thy = Proof_Context.theory_of ctxt in
   8.113 -    is_reconstructor orf is_atp thy orf is_smt_prover ctxt
   8.114 -  end
   8.115 -
   8.116 -fun is_prover_installed ctxt =
   8.117 -  is_reconstructor orf is_smt_prover ctxt orf
   8.118 -  is_atp_installed (Proof_Context.theory_of ctxt)
   8.119 -
   8.120 -fun remotify_prover_if_supported_and_not_already_remote ctxt name =
   8.121 +fun remotify_atp_if_supported_and_not_already_remote thy name =
   8.122    if String.isPrefix remote_prefix name then
   8.123      SOME name
   8.124    else
   8.125      let val remote_name = remote_prefix ^ name in
   8.126 -      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
   8.127 +      if is_atp thy remote_name then SOME remote_name else NONE
   8.128      end
   8.129  
   8.130 -fun remotify_prover_if_not_installed ctxt name =
   8.131 -  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
   8.132 -    SOME name
   8.133 -  else
   8.134 -    remotify_prover_if_supported_and_not_already_remote ctxt name
   8.135 -
   8.136 -fun get_slices slice slices =
   8.137 -  (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
   8.138 -
   8.139 -val reconstructor_default_max_facts = 20
   8.140 -
   8.141 -fun slice_max_facts (_, ( ((max_facts, _), _, _, _, _), _)) = max_facts
   8.142 -
   8.143 -fun default_max_facts_of_prover ctxt name =
   8.144 -  let val thy = Proof_Context.theory_of ctxt in
   8.145 -    if is_reconstructor name then
   8.146 -      reconstructor_default_max_facts
   8.147 -    else if is_atp thy name then
   8.148 -      fold (Integer.max o slice_max_facts) (#best_slices (get_atp thy name ()) ctxt) 0
   8.149 -    else (* is_smt_prover ctxt name *)
   8.150 -      SMT_Solver.default_max_relevant ctxt name
   8.151 -  end
   8.152 +fun remotify_atp_if_not_installed thy name =
   8.153 +  if is_atp_installed thy name then SOME name
   8.154 +  else remotify_atp_if_supported_and_not_already_remote thy name
   8.155  
   8.156  fun is_if (@{const_name If}, _) = true
   8.157    | is_if _ = false
   8.158 @@ -256,9 +200,6 @@
   8.159  fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
   8.160  val messages = Async_Manager.thread_messages SledgehammerN "prover"
   8.161  
   8.162 -
   8.163 -(** problems, results, ATPs, etc. **)
   8.164 -
   8.165  type params =
   8.166    {debug : bool,
   8.167     verbose : bool,
   8.168 @@ -306,43 +247,13 @@
   8.169    params -> ((string * string list) list -> string -> minimize_command)
   8.170    -> prover_problem -> prover_result
   8.171  
   8.172 -(* FUDGE *)
   8.173 -val smt_min_weight =
   8.174 -  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
   8.175 -val smt_max_weight =
   8.176 -  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
   8.177 -val smt_max_weight_index =
   8.178 -  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
   8.179 -val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
   8.180 -
   8.181 -fun smt_fact_weight ctxt j num_facts =
   8.182 -  if Config.get ctxt smt_weights andalso
   8.183 -     num_facts >= Config.get ctxt smt_weight_min_facts then
   8.184 -    let
   8.185 -      val min = Config.get ctxt smt_min_weight
   8.186 -      val max = Config.get ctxt smt_max_weight
   8.187 -      val max_index = Config.get ctxt smt_max_weight_index
   8.188 -      val curve = !smt_weight_curve
   8.189 -    in
   8.190 -      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
   8.191 -            div curve max_index)
   8.192 -    end
   8.193 -  else
   8.194 -    NONE
   8.195 -
   8.196 -fun weight_smt_fact ctxt num_facts ((info, th), j) =
   8.197 -  let val thy = Proof_Context.theory_of ctxt in
   8.198 -    (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
   8.199 -  end
   8.200 -
   8.201 -fun overlord_file_location_of_prover prover =
   8.202 -  (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   8.203 +fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   8.204  
   8.205  fun proof_banner mode name =
   8.206 -  case mode of
   8.207 +  (case mode of
   8.208      Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   8.209    | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   8.210 -  | _ => "Try this"
   8.211 +  | _ => "Try this")
   8.212  
   8.213  fun bunch_of_reconstructors needs_full_types lam_trans =
   8.214    if needs_full_types then
   8.215 @@ -423,91 +334,17 @@
   8.216        end
   8.217    end
   8.218  
   8.219 -
   8.220 -(* generic TPTP-based ATPs *)
   8.221 -
   8.222 -(* Too general means, positive equality literal with a variable X as one
   8.223 -   operand, when X does not occur properly in the other operand. This rules out
   8.224 -   clearly inconsistent facts such as X = a | X = b, though it by no means
   8.225 -   guarantees soundness. *)
   8.226 -
   8.227 -fun get_facts_of_filter _ [(_, facts)] = facts
   8.228 -  | get_facts_of_filter fact_filter factss =
   8.229 -    case AList.lookup (op =) factss fact_filter of
   8.230 -      SOME facts => facts
   8.231 -    | NONE => snd (hd factss)
   8.232 +val canonical_isar_supported_prover = eN
   8.233  
   8.234 -(* Unwanted equalities are those between a (bound or schematic) variable that
   8.235 -   does not properly occur in the second operand. *)
   8.236 -val is_exhaustive_finite =
   8.237 -  let
   8.238 -    fun is_bad_equal (Var z) t =
   8.239 -        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
   8.240 -      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
   8.241 -      | is_bad_equal _ _ = false
   8.242 -    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
   8.243 -    fun do_formula pos t =
   8.244 -      case (pos, t) of
   8.245 -        (_, @{const Trueprop} $ t1) => do_formula pos t1
   8.246 -      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
   8.247 -        do_formula pos t'
   8.248 -      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
   8.249 -        do_formula pos t'
   8.250 -      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
   8.251 -        do_formula pos t'
   8.252 -      | (_, @{const "==>"} $ t1 $ t2) =>
   8.253 -        do_formula (not pos) t1 andalso
   8.254 -        (t2 = @{prop False} orelse do_formula pos t2)
   8.255 -      | (_, @{const HOL.implies} $ t1 $ t2) =>
   8.256 -        do_formula (not pos) t1 andalso
   8.257 -        (t2 = @{const False} orelse do_formula pos t2)
   8.258 -      | (_, @{const Not} $ t1) => do_formula (not pos) t1
   8.259 -      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   8.260 -      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   8.261 -      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
   8.262 -      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
   8.263 -      | _ => false
   8.264 -  in do_formula true end
   8.265 -
   8.266 -fun has_bound_or_var_of_type pred =
   8.267 -  exists_subterm (fn Var (_, T as Type _) => pred T
   8.268 -                   | Abs (_, T as Type _, _) => pred T
   8.269 -                   | _ => false)
   8.270 -
   8.271 -(* Facts are forbidden to contain variables of these types. The typical reason
   8.272 -   is that they lead to unsoundness. Note that "unit" satisfies numerous
   8.273 -   equations like "?x = ()". The resulting clauses will have no type constraint,
   8.274 -   yielding false proofs. Even "bool" leads to many unsound proofs, though only
   8.275 -   for higher-order problems. *)
   8.276 -
   8.277 -(* Facts containing variables of type "unit" or "bool" or of the form
   8.278 -   "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
   8.279 -   are omitted. *)
   8.280 -fun is_dangerous_prop ctxt =
   8.281 -  transform_elim_prop
   8.282 -  #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
   8.283 -      is_exhaustive_finite)
   8.284 -
   8.285 -(* Important messages are important but not so important that users want to see
   8.286 -   them each time. *)
   8.287 -val atp_important_message_keep_quotient = 25
   8.288 -
   8.289 -fun choose_type_enc strictness best_type_enc format =
   8.290 -  the_default best_type_enc
   8.291 -  #> type_enc_of_string strictness
   8.292 -  #> adjust_type_enc format
   8.293 -
   8.294 -fun isar_proof_reconstructor ctxt name =
   8.295 -  let val thy = Proof_Context.theory_of ctxt in
   8.296 -    if is_atp thy name then name
   8.297 -    else remotify_prover_if_not_installed ctxt eN |> the_default name
   8.298 -  end
   8.299 +fun isar_supported_prover_of thy name =
   8.300 +  if is_atp thy name then name
   8.301 +  else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover)
   8.302  
   8.303  (* FIXME: See the analogous logic in the function "maybe_minimize" in
   8.304     "sledgehammer_prover_minimize.ML". *)
   8.305 -fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command name preplay =
   8.306 +fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay =
   8.307    let
   8.308 -    val maybe_isar_name = name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
   8.309 +    val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
   8.310      val (min_name, override_params) =
   8.311        (case preplay of
   8.312          (reconstr, Played _) =>
   8.313 @@ -518,502 +355,15 @@
   8.314  
   8.315  val max_fact_instances = 10 (* FUDGE *)
   8.316  
   8.317 -fun repair_monomorph_context max_iters best_max_iters max_new_instances
   8.318 -                             best_max_new_instances =
   8.319 +fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
   8.320    Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
   8.321    #> Config.put Monomorph.max_new_instances
   8.322 -         (max_new_instances |> the_default best_max_new_instances)
   8.323 +       (max_new_instances |> the_default best_max_new_instances)
   8.324    #> Config.put Monomorph.max_thm_instances max_fact_instances
   8.325  
   8.326 -fun suffix_of_mode Auto_Try = "_try"
   8.327 -  | suffix_of_mode Try = "_try"
   8.328 -  | suffix_of_mode Normal = ""
   8.329 -  | suffix_of_mode MaSh = ""
   8.330 -  | suffix_of_mode Auto_Minimize = "_min"
   8.331 -  | suffix_of_mode Minimize = "_min"
   8.332 -
   8.333 -(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
   8.334 -   Linux appears to be the only ATP that does not honor its time limit. *)
   8.335 -val atp_timeout_slack = seconds 1.0
   8.336 -
   8.337 -val mono_max_privileged_facts = 10
   8.338 -
   8.339 -(* For low values of "max_facts", this fudge value ensures that most slices are
   8.340 -   invoked with a nontrivial amount of facts. *)
   8.341 -val max_fact_factor_fudge = 5
   8.342 -
   8.343 -fun run_atp mode name
   8.344 -    ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
   8.345 -      best_max_new_mono_instances, ...} : atp_config)
   8.346 -    (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
   8.347 -       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
   8.348 -       try0_isar, slice, timeout, preplay_timeout, ...})
   8.349 +fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
   8.350      minimize_command
   8.351 -    ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   8.352 -  let
   8.353 -    val thy = Proof.theory_of state
   8.354 -    val ctxt = Proof.context_of state
   8.355 -    val atp_mode =
   8.356 -      if Config.get ctxt completish then Sledgehammer_Completish
   8.357 -      else Sledgehammer
   8.358 -    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
   8.359 -    val (dest_dir, problem_prefix) =
   8.360 -      if overlord then overlord_file_location_of_prover name
   8.361 -      else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
   8.362 -    val problem_file_name =
   8.363 -      Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
   8.364 -                  suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
   8.365 -    val prob_path =
   8.366 -      if dest_dir = "" then
   8.367 -        File.tmp_path problem_file_name
   8.368 -      else if File.exists (Path.explode dest_dir) then
   8.369 -        Path.append (Path.explode dest_dir) problem_file_name
   8.370 -      else
   8.371 -        error ("No such directory: " ^ quote dest_dir ^ ".")
   8.372 -    val exec = exec ()
   8.373 -    val command0 =
   8.374 -      case find_first (fn var => getenv var <> "") (fst exec) of
   8.375 -        SOME var =>
   8.376 -        let
   8.377 -          val pref = getenv var ^ "/"
   8.378 -          val paths = map (Path.explode o prefix pref) (snd exec)
   8.379 -        in
   8.380 -          case find_first File.exists paths of
   8.381 -            SOME path => path
   8.382 -          | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
   8.383 -        end
   8.384 -      | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^
   8.385 -                       " is not set.")
   8.386 -    fun split_time s =
   8.387 -      let
   8.388 -        val split = String.tokens (fn c => str c = "\n")
   8.389 -        val (output, t) =
   8.390 -          s |> split |> (try split_last #> the_default ([], "0"))
   8.391 -            |>> cat_lines
   8.392 -        fun as_num f = f >> (fst o read_int)
   8.393 -        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
   8.394 -        val digit = Scan.one Symbol.is_ascii_digit
   8.395 -        val num3 = as_num (digit ::: digit ::: (digit >> single))
   8.396 -        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
   8.397 -        val as_time =
   8.398 -          raw_explode #> Scan.read Symbol.stopper time #> the_default 0
   8.399 -      in (output, as_time t |> Time.fromMilliseconds) end
   8.400 -    fun run () =
   8.401 -      let
   8.402 -        (* If slicing is disabled, we expand the last slice to fill the entire
   8.403 -           time available. *)
   8.404 -        val all_slices = best_slices ctxt
   8.405 -        val actual_slices = get_slices slice all_slices
   8.406 -        fun max_facts_of_slices f slices = fold (Integer.max o slice_max_facts o f) slices 0
   8.407 -        val num_actual_slices = length actual_slices
   8.408 -        val max_fact_factor =
   8.409 -          Real.fromInt (case max_facts of
   8.410 -              NONE => max_facts_of_slices I all_slices
   8.411 -            | SOME max => max)
   8.412 -          / Real.fromInt (max_facts_of_slices snd actual_slices)
   8.413 -        fun monomorphize_facts facts =
   8.414 -          let
   8.415 -            val ctxt =
   8.416 -              ctxt
   8.417 -              |> repair_monomorph_context max_mono_iters
   8.418 -                     best_max_mono_iters max_new_mono_instances
   8.419 -                     best_max_new_mono_instances
   8.420 -            (* pseudo-theorem involving the same constants as the subgoal *)
   8.421 -            val subgoal_th =
   8.422 -              Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
   8.423 -            val rths =
   8.424 -              facts |> chop mono_max_privileged_facts
   8.425 -                    |>> map (pair 1 o snd)
   8.426 -                    ||> map (pair 2 o snd)
   8.427 -                    |> op @
   8.428 -                    |> cons (0, subgoal_th)
   8.429 -          in
   8.430 -            Monomorph.monomorph atp_schematic_consts_of ctxt rths
   8.431 -            |> tl |> curry ListPair.zip (map fst facts)
   8.432 -            |> maps (fn (name, rths) =>
   8.433 -                        map (pair name o zero_var_indexes o snd) rths)
   8.434 -          end
   8.435 -        fun run_slice time_left (cache_key, cache_value)
   8.436 -                (slice, (time_frac,
   8.437 -                     (key as ((best_max_facts, best_fact_filter), format,
   8.438 -                              best_type_enc, best_lam_trans,
   8.439 -                              best_uncurried_aliases),
   8.440 -                      extra))) =
   8.441 -          let
   8.442 -            val effective_fact_filter =
   8.443 -              fact_filter |> the_default best_fact_filter
   8.444 -            val facts = get_facts_of_filter effective_fact_filter factss
   8.445 -            val num_facts =
   8.446 -              Real.ceil (max_fact_factor * Real.fromInt best_max_facts) +
   8.447 -              max_fact_factor_fudge
   8.448 -              |> Integer.min (length facts)
   8.449 -            val strictness = if strict then Strict else Non_Strict
   8.450 -            val type_enc =
   8.451 -              type_enc |> choose_type_enc strictness best_type_enc format
   8.452 -            val sound = is_type_enc_sound type_enc
   8.453 -            val real_ms = Real.fromInt o Time.toMilliseconds
   8.454 -            val slice_timeout =
   8.455 -              (real_ms time_left
   8.456 -               |> (if slice < num_actual_slices - 1 then
   8.457 -                     curry Real.min (time_frac * real_ms timeout)
   8.458 -                   else
   8.459 -                     I))
   8.460 -              * 0.001
   8.461 -              |> seconds
   8.462 -            val generous_slice_timeout =
   8.463 -              if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
   8.464 -            val _ =
   8.465 -              if debug then
   8.466 -                quote name ^ " slice #" ^ string_of_int (slice + 1) ^
   8.467 -                " with " ^ string_of_int num_facts ^ " fact" ^
   8.468 -                plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
   8.469 -                |> Output.urgent_message
   8.470 -              else
   8.471 -                ()
   8.472 -            val readable_names = not (Config.get ctxt atp_full_names)
   8.473 -            val lam_trans =
   8.474 -              case lam_trans of
   8.475 -                SOME s => s
   8.476 -              | NONE => best_lam_trans
   8.477 -            val uncurried_aliases =
   8.478 -              case uncurried_aliases of
   8.479 -                SOME b => b
   8.480 -              | NONE => best_uncurried_aliases
   8.481 -            val value as (atp_problem, _, fact_names, _, _) =
   8.482 -              if cache_key = SOME key then
   8.483 -                cache_value
   8.484 -              else
   8.485 -                facts
   8.486 -                |> not sound
   8.487 -                   ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
   8.488 -                |> take num_facts
   8.489 -                |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
   8.490 -                |> map (apsnd prop_of)
   8.491 -                |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
   8.492 -                                       lam_trans uncurried_aliases
   8.493 -                                       readable_names true hyp_ts concl_t
   8.494 -            fun sel_weights () = atp_problem_selection_weights atp_problem
   8.495 -            fun ord_info () = atp_problem_term_order_info atp_problem
   8.496 -            val ord = effective_term_order ctxt name
   8.497 -            val full_proof = isar_proofs |> the_default (mode = Minimize)
   8.498 -            val args =
   8.499 -              arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
   8.500 -                (ord, ord_info, sel_weights)
   8.501 -            val command =
   8.502 -              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
   8.503 -              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
   8.504 -            val _ =
   8.505 -              atp_problem
   8.506 -              |> lines_of_atp_problem format ord ord_info
   8.507 -              |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
   8.508 -              |> File.write_list prob_path
   8.509 -            val ((output, run_time), (atp_proof, outcome)) =
   8.510 -              TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
   8.511 -              |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
   8.512 -              |> fst |> split_time
   8.513 -              |> (fn accum as (output, _) =>
   8.514 -                     (accum,
   8.515 -                      extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
   8.516 -                      |>> atp_proof_of_tstplike_proof atp_problem
   8.517 -                      handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
   8.518 -              handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
   8.519 -            val outcome =
   8.520 -              (case outcome of
   8.521 -                NONE =>
   8.522 -                (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
   8.523 -                      |> Option.map (sort string_ord) of
   8.524 -                   SOME facts =>
   8.525 -                   let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
   8.526 -                     if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
   8.527 -                   end
   8.528 -                 | NONE => NONE)
   8.529 -              | _ => outcome)
   8.530 -          in
   8.531 -            ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
   8.532 -          end
   8.533 -        val timer = Timer.startRealTimer ()
   8.534 -        fun maybe_run_slice slice
   8.535 -                (result as (cache, (_, run_time0, _, _, SOME _))) =
   8.536 -            let
   8.537 -              val time_left = Time.- (timeout, Timer.checkRealTimer timer)
   8.538 -            in
   8.539 -              if Time.<= (time_left, Time.zeroTime) then
   8.540 -                result
   8.541 -              else
   8.542 -                run_slice time_left cache slice
   8.543 -                |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) =>
   8.544 -                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome)))
   8.545 -            end
   8.546 -          | maybe_run_slice _ result = result
   8.547 -      in
   8.548 -        ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
   8.549 -         ("", Time.zeroTime, [], [], SOME InternalError))
   8.550 -        |> fold maybe_run_slice actual_slices
   8.551 -      end
   8.552 -    (* If the problem file has not been exported, remove it; otherwise, export
   8.553 -       the proof file too. *)
   8.554 -    fun clean_up () =
   8.555 -      if dest_dir = "" then (try File.rm prob_path; ()) else ()
   8.556 -    fun export (_, (output, _, _, _, _)) =
   8.557 -      if dest_dir = "" then ()
   8.558 -      else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
   8.559 -    val ((_, (_, pool, fact_names, lifted, sym_tab)),
   8.560 -         (output, run_time, used_from, atp_proof, outcome)) =
   8.561 -      with_cleanup clean_up run () |> tap export
   8.562 -    val important_message =
   8.563 -      if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0
   8.564 -      then
   8.565 -        extract_important_message output
   8.566 -      else
   8.567 -        ""
   8.568 -    val (used_facts, preplay, message, message_tail) =
   8.569 -      (case outcome of
   8.570 -        NONE =>
   8.571 -        let
   8.572 -          val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
   8.573 -          val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
   8.574 -          val reconstrs =
   8.575 -            bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof
   8.576 -              o (fn desperate => if desperate then hide_lamsN else default_metis_lam_trans))
   8.577 -        in
   8.578 -          (used_facts,
   8.579 -           Lazy.lazy (fn () =>
   8.580 -             let val used_pairs = used_from |> filter_used_facts false used_facts in
   8.581 -               play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
   8.582 -                 (hd reconstrs) reconstrs
   8.583 -             end),
   8.584 -           fn preplay =>
   8.585 -              let
   8.586 -                val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
   8.587 -                fun isar_params () =
   8.588 -                  let
   8.589 -                    val metis_type_enc =
   8.590 -                      if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
   8.591 -                      else partial_typesN
   8.592 -                    val metis_lam_trans = lam_trans_of_atp_proof atp_proof default_metis_lam_trans
   8.593 -                    val atp_proof =
   8.594 -                      atp_proof
   8.595 -                      |> termify_atp_proof ctxt pool lifted sym_tab
   8.596 -                      |> introduce_spass_skolem
   8.597 -                      |> factify_atp_proof fact_names hyp_ts concl_t
   8.598 -                  in
   8.599 -                    (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
   8.600 -                     try0_isar, atp_proof, goal)
   8.601 -                  end
   8.602 -                val one_line_params =
   8.603 -                  (preplay, proof_banner mode name, used_facts,
   8.604 -                   choose_minimize_command ctxt params minimize_command name preplay,
   8.605 -                   subgoal, subgoal_count)
   8.606 -                val num_chained = length (#facts (Proof.goal state))
   8.607 -              in
   8.608 -                proof_text ctxt debug isar_proofs isar_params num_chained one_line_params
   8.609 -              end,
   8.610 -           (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
   8.611 -           (if important_message <> "" then
   8.612 -              "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
   8.613 -            else
   8.614 -              ""))
   8.615 -        end
   8.616 -      | SOME failure =>
   8.617 -        ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
   8.618 -  in
   8.619 -    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
   8.620 -     preplay = preplay, message = message, message_tail = message_tail}
   8.621 -  end
   8.622 -
   8.623 -(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
   8.624 -   these are sorted out properly in the SMT module, we have to interpret these
   8.625 -   ourselves. *)
   8.626 -val remote_smt_failures =
   8.627 -  [(2, NoLibwwwPerl),
   8.628 -   (22, CantConnect)]
   8.629 -val z3_failures =
   8.630 -  [(101, OutOfResources),
   8.631 -   (103, MalformedInput),
   8.632 -   (110, MalformedInput),
   8.633 -   (112, TimedOut)]
   8.634 -val unix_failures =
   8.635 -  [(138, Crashed),
   8.636 -   (139, Crashed)]
   8.637 -val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
   8.638 -
   8.639 -fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
   8.640 -    if is_real_cex then Unprovable else GaveUp
   8.641 -  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
   8.642 -  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
   8.643 -    (case AList.lookup (op =) smt_failures code of
   8.644 -       SOME failure => failure
   8.645 -     | NONE => UnknownError ("Abnormal termination with exit code " ^
   8.646 -                             string_of_int code ^ "."))
   8.647 -  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   8.648 -  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
   8.649 -
   8.650 -(* FUDGE *)
   8.651 -val smt_max_slices =
   8.652 -  Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
   8.653 -val smt_slice_fact_frac =
   8.654 -  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac}
   8.655 -                           (K 0.667)
   8.656 -val smt_slice_time_frac =
   8.657 -  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
   8.658 -val smt_slice_min_secs =
   8.659 -  Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
   8.660 -
   8.661 -val is_boring_builtin_typ =
   8.662 -  not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
   8.663 -
   8.664 -fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
   8.665 -      ...} : params) state goal i =
   8.666 -  let
   8.667 -    fun repair_context ctxt =
   8.668 -      ctxt |> select_smt_solver name
   8.669 -           |> Config.put SMT_Config.verbose debug
   8.670 -           |> (if overlord then
   8.671 -                 Config.put SMT_Config.debug_files
   8.672 -                            (overlord_file_location_of_prover name
   8.673 -                             |> (fn (path, name) => path ^ "/" ^ name))
   8.674 -               else
   8.675 -                 I)
   8.676 -           |> Config.put SMT_Config.infer_triggers
   8.677 -                         (Config.get ctxt smt_triggers)
   8.678 -           |> not (Config.get ctxt smt_builtins)
   8.679 -              ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
   8.680 -                 #> Config.put SMT_Config.datatypes false)
   8.681 -           |> repair_monomorph_context max_mono_iters default_max_mono_iters
   8.682 -                  max_new_mono_instances default_max_new_mono_instances
   8.683 -    val state = Proof.map_context (repair_context) state
   8.684 -    val ctxt = Proof.context_of state
   8.685 -    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
   8.686 -    fun do_slice timeout slice outcome0 time_so_far
   8.687 -                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
   8.688 -      let
   8.689 -        val timer = Timer.startRealTimer ()
   8.690 -        val slice_timeout =
   8.691 -          if slice < max_slices then
   8.692 -            let val ms = Time.toMilliseconds timeout in
   8.693 -              Int.min (ms,
   8.694 -                  Int.max (1000 * Config.get ctxt smt_slice_min_secs,
   8.695 -                      Real.ceil (Config.get ctxt smt_slice_time_frac
   8.696 -                                 * Real.fromInt ms)))
   8.697 -              |> Time.fromMilliseconds
   8.698 -            end
   8.699 -          else
   8.700 -            timeout
   8.701 -        val num_facts = length weighted_facts
   8.702 -        val _ =
   8.703 -          if debug then
   8.704 -            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
   8.705 -            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
   8.706 -            |> Output.urgent_message
   8.707 -          else
   8.708 -            ()
   8.709 -        val birth = Timer.checkRealTimer timer
   8.710 -        val _ =
   8.711 -          if debug then Output.urgent_message "Invoking SMT solver..." else ()
   8.712 -        val (outcome, used_facts) =
   8.713 -          SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
   8.714 -          |> SMT_Solver.smt_filter_apply slice_timeout
   8.715 -          |> (fn {outcome, used_facts} => (outcome, used_facts))
   8.716 -          handle exn => if Exn.is_interrupt exn then
   8.717 -                          reraise exn
   8.718 -                        else
   8.719 -                          (ML_Compiler.exn_message exn
   8.720 -                           |> SMT_Failure.Other_Failure |> SOME, [])
   8.721 -        val death = Timer.checkRealTimer timer
   8.722 -        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   8.723 -        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
   8.724 -        val too_many_facts_perhaps =
   8.725 -          case outcome of
   8.726 -            NONE => false
   8.727 -          | SOME (SMT_Failure.Counterexample _) => false
   8.728 -          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
   8.729 -          | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
   8.730 -          | SOME SMT_Failure.Out_Of_Memory => true
   8.731 -          | SOME (SMT_Failure.Other_Failure _) => true
   8.732 -        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   8.733 -      in
   8.734 -        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
   8.735 -           Time.> (timeout, Time.zeroTime) then
   8.736 -          let
   8.737 -            val new_num_facts =
   8.738 -              Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
   8.739 -            val weighted_factss as (new_fact_filter, _) :: _ =
   8.740 -              weighted_factss
   8.741 -              |> (fn (x :: xs) => xs @ [x])
   8.742 -              |> app_hd (apsnd (take new_num_facts))
   8.743 -            val show_filter = fact_filter <> new_fact_filter
   8.744 -            fun num_of_facts fact_filter num_facts =
   8.745 -              string_of_int num_facts ^
   8.746 -              (if show_filter then " " ^ quote fact_filter else "") ^
   8.747 -              " fact" ^ plural_s num_facts
   8.748 -            val _ =
   8.749 -              if debug then
   8.750 -                quote name ^ " invoked with " ^
   8.751 -                num_of_facts fact_filter num_facts ^ ": " ^
   8.752 -                string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
   8.753 -                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
   8.754 -                "..."
   8.755 -                |> Output.urgent_message
   8.756 -              else
   8.757 -                ()
   8.758 -          in
   8.759 -            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
   8.760 -          end
   8.761 -        else
   8.762 -          {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
   8.763 -           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
   8.764 -      end
   8.765 -  in
   8.766 -    do_slice timeout 1 NONE Time.zeroTime
   8.767 -  end
   8.768 -
   8.769 -fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
   8.770 -    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   8.771 -  let
   8.772 -    val ctxt = Proof.context_of state
   8.773 -    fun weight_facts facts =
   8.774 -      let val num_facts = length facts in
   8.775 -        facts ~~ (0 upto num_facts - 1)
   8.776 -        |> map (weight_smt_fact ctxt num_facts)
   8.777 -      end
   8.778 -    val weighted_factss = factss |> map (apsnd weight_facts)
   8.779 -    val {outcome, used_facts = used_pairs, used_from, run_time} =
   8.780 -      smt_filter_loop name params state goal subgoal weighted_factss
   8.781 -    val used_facts = used_pairs |> map fst
   8.782 -    val outcome = outcome |> Option.map failure_of_smt_failure
   8.783 -    val (preplay, message, message_tail) =
   8.784 -      case outcome of
   8.785 -        NONE =>
   8.786 -        (Lazy.lazy (fn () =>
   8.787 -           play_one_line_proof mode debug verbose preplay_timeout used_pairs
   8.788 -               state subgoal SMT
   8.789 -               (bunch_of_reconstructors false (fn desperate =>
   8.790 -                  if desperate then liftingN else default_metis_lam_trans))),
   8.791 -         fn preplay =>
   8.792 -            let
   8.793 -              val one_line_params =
   8.794 -                (preplay, proof_banner mode name, used_facts,
   8.795 -                 choose_minimize_command ctxt params minimize_command name preplay,
   8.796 -                 subgoal, subgoal_count)
   8.797 -              val num_chained = length (#facts (Proof.goal state))
   8.798 -            in
   8.799 -              one_line_proof_text num_chained one_line_params
   8.800 -            end,
   8.801 -         if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
   8.802 -      | SOME failure =>
   8.803 -        (Lazy.value (plain_metis, Play_Failed),
   8.804 -         fn _ => string_of_atp_failure failure, "")
   8.805 -  in
   8.806 -    {outcome = outcome, used_facts = used_facts, used_from = used_from,
   8.807 -     run_time = run_time, preplay = preplay, message = message,
   8.808 -     message_tail = message_tail}
   8.809 -  end
   8.810 -
   8.811 -fun run_reconstructor mode name
   8.812 -        (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
   8.813 -        minimize_command
   8.814 -        ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...}
   8.815 -         : prover_problem) =
   8.816 +    ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
   8.817    let
   8.818      val reconstr =
   8.819        if name = metisN then
   8.820 @@ -1052,12 +402,4 @@
   8.821        end)
   8.822    end
   8.823  
   8.824 -fun get_prover ctxt mode name =
   8.825 -  let val thy = Proof_Context.theory_of ctxt in
   8.826 -    if is_reconstructor name then run_reconstructor mode name
   8.827 -    else if is_atp thy name then run_atp mode name (get_atp thy name ())
   8.828 -    else if is_smt_prover ctxt name then run_smt_solver mode name
   8.829 -    else error ("No such prover: " ^ name ^ ".")
   8.830 -  end
   8.831 -
   8.832  end;
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Jan 31 12:30:54 2014 +0100
     9.3 @@ -0,0 +1,394 @@
     9.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
     9.5 +    Author:     Fabian Immler, TU Muenchen
     9.6 +    Author:     Makarius
     9.7 +    Author:     Jasmin Blanchette, TU Muenchen
     9.8 +
     9.9 +ATPs as Sledgehammer provers.
    9.10 +*)
    9.11 +
    9.12 +signature SLEDGEHAMMER_PROVER_ATP =
    9.13 +sig
    9.14 +  type mode = Sledgehammer_Prover.mode
    9.15 +  type prover = Sledgehammer_Prover.prover
    9.16 +
    9.17 +  val run_atp : mode -> string -> prover
    9.18 +end;
    9.19 +
    9.20 +structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP =
    9.21 +struct
    9.22 +
    9.23 +open ATP_Util
    9.24 +open ATP_Problem
    9.25 +open ATP_Proof
    9.26 +open ATP_Problem_Generate
    9.27 +open ATP_Proof_Reconstruct
    9.28 +open ATP_Systems
    9.29 +open Sledgehammer_Util
    9.30 +open Sledgehammer_Reconstructor
    9.31 +open Sledgehammer_Isar
    9.32 +open Sledgehammer_Prover
    9.33 +
    9.34 +fun choose_type_enc strictness best_type_enc format =
    9.35 +  the_default best_type_enc
    9.36 +  #> type_enc_of_string strictness
    9.37 +  #> adjust_type_enc format
    9.38 +
    9.39 +fun has_bound_or_var_of_type pred =
    9.40 +  exists_subterm (fn Var (_, T as Type _) => pred T
    9.41 +                   | Abs (_, T as Type _, _) => pred T
    9.42 +                   | _ => false)
    9.43 +
    9.44 +(* Unwanted equalities are those between a (bound or schematic) variable that does not properly
    9.45 +   occur in the second operand. *)
    9.46 +val is_exhaustive_finite =
    9.47 +  let
    9.48 +    fun is_bad_equal (Var z) t =
    9.49 +        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
    9.50 +      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
    9.51 +      | is_bad_equal _ _ = false
    9.52 +    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
    9.53 +    fun do_formula pos t =
    9.54 +      case (pos, t) of
    9.55 +        (_, @{const Trueprop} $ t1) => do_formula pos t1
    9.56 +      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
    9.57 +        do_formula pos t'
    9.58 +      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
    9.59 +        do_formula pos t'
    9.60 +      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
    9.61 +        do_formula pos t'
    9.62 +      | (_, @{const "==>"} $ t1 $ t2) =>
    9.63 +        do_formula (not pos) t1 andalso
    9.64 +        (t2 = @{prop False} orelse do_formula pos t2)
    9.65 +      | (_, @{const HOL.implies} $ t1 $ t2) =>
    9.66 +        do_formula (not pos) t1 andalso
    9.67 +        (t2 = @{const False} orelse do_formula pos t2)
    9.68 +      | (_, @{const Not} $ t1) => do_formula (not pos) t1
    9.69 +      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
    9.70 +      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
    9.71 +      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
    9.72 +      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
    9.73 +      | _ => false
    9.74 +  in do_formula true end
    9.75 +
    9.76 +(* Facts containing variables of finite types such as "unit" or "bool" or of the form
    9.77 +   "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type
    9.78 +   encodings. *)
    9.79 +fun is_dangerous_prop ctxt =
    9.80 +  transform_elim_prop
    9.81 +  #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite)
    9.82 +
    9.83 +fun get_slices slice slices =
    9.84 +  (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
    9.85 +
    9.86 +fun get_facts_of_filter _ [(_, facts)] = facts
    9.87 +  | get_facts_of_filter fact_filter factss =
    9.88 +    (case AList.lookup (op =) factss fact_filter of
    9.89 +      SOME facts => facts
    9.90 +    | NONE => snd (hd factss))
    9.91 +
    9.92 +(* For low values of "max_facts", this fudge value ensures that most slices are invoked with a
    9.93 +   nontrivial amount of facts. *)
    9.94 +val max_fact_factor_fudge = 5
    9.95 +
    9.96 +val mono_max_privileged_facts = 10
    9.97 +
    9.98 +fun suffix_of_mode Auto_Try = "_try"
    9.99 +  | suffix_of_mode Try = "_try"
   9.100 +  | suffix_of_mode Normal = ""
   9.101 +  | suffix_of_mode MaSh = ""
   9.102 +  | suffix_of_mode Auto_Minimize = "_min"
   9.103 +  | suffix_of_mode Minimize = "_min"
   9.104 +
   9.105 +(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be
   9.106 +   the only ATP that does not honor its time limit. *)
   9.107 +val atp_timeout_slack = seconds 1.0
   9.108 +
   9.109 +(* Important messages are important but not so important that users want to see
   9.110 +   them each time. *)
   9.111 +val atp_important_message_keep_quotient = 25
   9.112 +
   9.113 +fun run_atp mode name
   9.114 +    (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
   9.115 +       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
   9.116 +       try0_isar, slice, timeout, preplay_timeout, ...})
   9.117 +    minimize_command
   9.118 +    ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   9.119 +  let
   9.120 +    val thy = Proof.theory_of state
   9.121 +    val ctxt = Proof.context_of state
   9.122 +
   9.123 +    val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
   9.124 +      best_max_new_mono_instances, ...} = get_atp thy name ()
   9.125 +
   9.126 +    val atp_mode = if Config.get ctxt completish then Sledgehammer_Completish else Sledgehammer
   9.127 +    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
   9.128 +    val (dest_dir, problem_prefix) =
   9.129 +      if overlord then overlord_file_location_of_prover name
   9.130 +      else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
   9.131 +    val problem_file_name =
   9.132 +      Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
   9.133 +                  suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
   9.134 +    val prob_path =
   9.135 +      if dest_dir = "" then
   9.136 +        File.tmp_path problem_file_name
   9.137 +      else if File.exists (Path.explode dest_dir) then
   9.138 +        Path.append (Path.explode dest_dir) problem_file_name
   9.139 +      else
   9.140 +        error ("No such directory: " ^ quote dest_dir ^ ".")
   9.141 +    val exec = exec ()
   9.142 +    val command0 =
   9.143 +      case find_first (fn var => getenv var <> "") (fst exec) of
   9.144 +        SOME var =>
   9.145 +        let
   9.146 +          val pref = getenv var ^ "/"
   9.147 +          val paths = map (Path.explode o prefix pref) (snd exec)
   9.148 +        in
   9.149 +          case find_first File.exists paths of
   9.150 +            SOME path => path
   9.151 +          | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
   9.152 +        end
   9.153 +      | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^
   9.154 +                       " is not set.")
   9.155 +
   9.156 +    fun split_time s =
   9.157 +      let
   9.158 +        val split = String.tokens (fn c => str c = "\n")
   9.159 +        val (output, t) =
   9.160 +          s |> split |> (try split_last #> the_default ([], "0"))
   9.161 +            |>> cat_lines
   9.162 +        fun as_num f = f >> (fst o read_int)
   9.163 +        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
   9.164 +        val digit = Scan.one Symbol.is_ascii_digit
   9.165 +        val num3 = as_num (digit ::: digit ::: (digit >> single))
   9.166 +        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
   9.167 +        val as_time =
   9.168 +          raw_explode #> Scan.read Symbol.stopper time #> the_default 0
   9.169 +      in (output, as_time t |> Time.fromMilliseconds) end
   9.170 +
   9.171 +    fun run () =
   9.172 +      let
   9.173 +        (* If slicing is disabled, we expand the last slice to fill the entire
   9.174 +           time available. *)
   9.175 +        val all_slices = best_slices ctxt
   9.176 +        val actual_slices = get_slices slice all_slices
   9.177 +        fun max_facts_of_slices f slices = fold (Integer.max o fst o #1 o fst o snd o f) slices 0
   9.178 +        val num_actual_slices = length actual_slices
   9.179 +        val max_fact_factor =
   9.180 +          Real.fromInt (case max_facts of
   9.181 +              NONE => max_facts_of_slices I all_slices
   9.182 +            | SOME max => max)
   9.183 +          / Real.fromInt (max_facts_of_slices snd actual_slices)
   9.184 +        fun monomorphize_facts facts =
   9.185 +          let
   9.186 +            val ctxt =
   9.187 +              ctxt
   9.188 +              |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances
   9.189 +                   best_max_new_mono_instances
   9.190 +            (* pseudo-theorem involving the same constants as the subgoal *)
   9.191 +            val subgoal_th =
   9.192 +              Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
   9.193 +            val rths =
   9.194 +              facts |> chop mono_max_privileged_facts
   9.195 +                    |>> map (pair 1 o snd)
   9.196 +                    ||> map (pair 2 o snd)
   9.197 +                    |> op @
   9.198 +                    |> cons (0, subgoal_th)
   9.199 +          in
   9.200 +            Monomorph.monomorph atp_schematic_consts_of ctxt rths
   9.201 +            |> tl |> curry ListPair.zip (map fst facts)
   9.202 +            |> maps (fn (name, rths) =>
   9.203 +                        map (pair name o zero_var_indexes o snd) rths)
   9.204 +          end
   9.205 +
   9.206 +        fun run_slice time_left (cache_key, cache_value)
   9.207 +                (slice, (time_frac,
   9.208 +                     (key as ((best_max_facts, best_fact_filter), format,
   9.209 +                              best_type_enc, best_lam_trans,
   9.210 +                              best_uncurried_aliases),
   9.211 +                      extra))) =
   9.212 +          let
   9.213 +            val effective_fact_filter =
   9.214 +              fact_filter |> the_default best_fact_filter
   9.215 +            val facts = get_facts_of_filter effective_fact_filter factss
   9.216 +            val num_facts =
   9.217 +              Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge
   9.218 +              |> Integer.min (length facts)
   9.219 +            val strictness = if strict then Strict else Non_Strict
   9.220 +            val type_enc = type_enc |> choose_type_enc strictness best_type_enc format
   9.221 +            val sound = is_type_enc_sound type_enc
   9.222 +            val real_ms = Real.fromInt o Time.toMilliseconds
   9.223 +            val slice_timeout =
   9.224 +              (real_ms time_left
   9.225 +               |> (if slice < num_actual_slices - 1 then
   9.226 +                     curry Real.min (time_frac * real_ms timeout)
   9.227 +                   else
   9.228 +                     I))
   9.229 +              * 0.001
   9.230 +              |> seconds
   9.231 +            val generous_slice_timeout =
   9.232 +              if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
   9.233 +            val _ =
   9.234 +              if debug then
   9.235 +                quote name ^ " slice #" ^ string_of_int (slice + 1) ^
   9.236 +                " with " ^ string_of_int num_facts ^ " fact" ^
   9.237 +                plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
   9.238 +                |> Output.urgent_message
   9.239 +              else
   9.240 +                ()
   9.241 +            val readable_names = not (Config.get ctxt atp_full_names)
   9.242 +            val lam_trans =
   9.243 +              case lam_trans of
   9.244 +                SOME s => s
   9.245 +              | NONE => best_lam_trans
   9.246 +            val uncurried_aliases =
   9.247 +              case uncurried_aliases of
   9.248 +                SOME b => b
   9.249 +              | NONE => best_uncurried_aliases
   9.250 +            val value as (atp_problem, _, fact_names, _, _) =
   9.251 +              if cache_key = SOME key then
   9.252 +                cache_value
   9.253 +              else
   9.254 +                facts
   9.255 +                |> not sound ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
   9.256 +                |> take num_facts
   9.257 +                |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
   9.258 +                |> map (apsnd prop_of)
   9.259 +                |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
   9.260 +                                       lam_trans uncurried_aliases
   9.261 +                                       readable_names true hyp_ts concl_t
   9.262 +
   9.263 +            fun sel_weights () = atp_problem_selection_weights atp_problem
   9.264 +            fun ord_info () = atp_problem_term_order_info atp_problem
   9.265 +
   9.266 +            val ord = effective_term_order ctxt name
   9.267 +            val full_proof = isar_proofs |> the_default (mode = Minimize)
   9.268 +            val args =
   9.269 +              arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
   9.270 +                (ord, ord_info, sel_weights)
   9.271 +            val command =
   9.272 +              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
   9.273 +              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
   9.274 +            val _ =
   9.275 +              atp_problem
   9.276 +              |> lines_of_atp_problem format ord ord_info
   9.277 +              |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
   9.278 +              |> File.write_list prob_path
   9.279 +            val ((output, run_time), (atp_proof, outcome)) =
   9.280 +              TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
   9.281 +              |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
   9.282 +              |> fst |> split_time
   9.283 +              |> (fn accum as (output, _) =>
   9.284 +                     (accum,
   9.285 +                      extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
   9.286 +                      |>> atp_proof_of_tstplike_proof atp_problem
   9.287 +                      handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
   9.288 +              handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
   9.289 +            val outcome =
   9.290 +              (case outcome of
   9.291 +                NONE =>
   9.292 +                (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
   9.293 +                      |> Option.map (sort string_ord) of
   9.294 +                   SOME facts =>
   9.295 +                   let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
   9.296 +                     if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
   9.297 +                   end
   9.298 +                 | NONE => NONE)
   9.299 +              | _ => outcome)
   9.300 +          in
   9.301 +            ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
   9.302 +          end
   9.303 +
   9.304 +        val timer = Timer.startRealTimer ()
   9.305 +
   9.306 +        fun maybe_run_slice slice
   9.307 +                (result as (cache, (_, run_time0, _, _, SOME _))) =
   9.308 +            let
   9.309 +              val time_left = Time.- (timeout, Timer.checkRealTimer timer)
   9.310 +            in
   9.311 +              if Time.<= (time_left, Time.zeroTime) then
   9.312 +                result
   9.313 +              else
   9.314 +                run_slice time_left cache slice
   9.315 +                |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) =>
   9.316 +                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome)))
   9.317 +            end
   9.318 +          | maybe_run_slice _ result = result
   9.319 +      in
   9.320 +        ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
   9.321 +         ("", Time.zeroTime, [], [], SOME InternalError))
   9.322 +        |> fold maybe_run_slice actual_slices
   9.323 +      end
   9.324 +
   9.325 +    (* If the problem file has not been exported, remove it; otherwise, export
   9.326 +       the proof file too. *)
   9.327 +    fun clean_up () =
   9.328 +      if dest_dir = "" then (try File.rm prob_path; ()) else ()
   9.329 +    fun export (_, (output, _, _, _, _)) =
   9.330 +      if dest_dir = "" then ()
   9.331 +      else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
   9.332 +    val ((_, (_, pool, fact_names, lifted, sym_tab)),
   9.333 +         (output, run_time, used_from, atp_proof, outcome)) =
   9.334 +      with_cleanup clean_up run () |> tap export
   9.335 +    val important_message =
   9.336 +      if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0
   9.337 +      then
   9.338 +        extract_important_message output
   9.339 +      else
   9.340 +        ""
   9.341 +
   9.342 +    val (used_facts, preplay, message, message_tail) =
   9.343 +      (case outcome of
   9.344 +        NONE =>
   9.345 +        let
   9.346 +          val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
   9.347 +          val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
   9.348 +          val reconstrs =
   9.349 +            bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof
   9.350 +              o (fn desperate => if desperate then hide_lamsN else default_metis_lam_trans))
   9.351 +        in
   9.352 +          (used_facts,
   9.353 +           Lazy.lazy (fn () =>
   9.354 +             let val used_pairs = used_from |> filter_used_facts false used_facts in
   9.355 +               play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
   9.356 +                 (hd reconstrs) reconstrs
   9.357 +             end),
   9.358 +           fn preplay =>
   9.359 +              let
   9.360 +                val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
   9.361 +                fun isar_params () =
   9.362 +                  let
   9.363 +                    val metis_type_enc =
   9.364 +                      if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
   9.365 +                      else partial_typesN
   9.366 +                    val metis_lam_trans = lam_trans_of_atp_proof atp_proof default_metis_lam_trans
   9.367 +                    val atp_proof =
   9.368 +                      atp_proof
   9.369 +                      |> termify_atp_proof ctxt pool lifted sym_tab
   9.370 +                      |> introduce_spass_skolem
   9.371 +                      |> factify_atp_proof fact_names hyp_ts concl_t
   9.372 +                  in
   9.373 +                    (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
   9.374 +                     try0_isar, atp_proof, goal)
   9.375 +                  end
   9.376 +                val one_line_params =
   9.377 +                  (preplay, proof_banner mode name, used_facts,
   9.378 +                   choose_minimize_command thy params minimize_command name preplay, subgoal,
   9.379 +                   subgoal_count)
   9.380 +                val num_chained = length (#facts (Proof.goal state))
   9.381 +              in
   9.382 +                proof_text ctxt debug isar_proofs isar_params num_chained one_line_params
   9.383 +              end,
   9.384 +           (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
   9.385 +           (if important_message <> "" then
   9.386 +              "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
   9.387 +            else
   9.388 +              ""))
   9.389 +        end
   9.390 +      | SOME failure =>
   9.391 +        ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
   9.392 +  in
   9.393 +    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
   9.394 +     preplay = preplay, message = message, message_tail = message_tail}
   9.395 +  end
   9.396 +
   9.397 +end;
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jan 31 10:34:20 2014 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jan 31 12:30:54 2014 +0100
    10.3 @@ -14,6 +14,11 @@
    10.4    type params = Sledgehammer_Prover.params
    10.5    type prover = Sledgehammer_Prover.prover
    10.6  
    10.7 +  val is_prover_supported : Proof.context -> string -> bool
    10.8 +  val is_prover_installed : Proof.context -> string -> bool
    10.9 +  val default_max_facts_of_prover : Proof.context -> string -> int
   10.10 +  val get_prover : Proof.context -> mode -> string -> prover
   10.11 +
   10.12    val binary_min_facts : int Config.T
   10.13    val auto_minimize_min_facts : int Config.T
   10.14    val auto_minimize_max_time : real Config.T
   10.15 @@ -24,6 +29,7 @@
   10.16      * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string)
   10.17         * string)
   10.18    val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
   10.19 +
   10.20    val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
   10.21      Proof.state -> unit
   10.22  end;
   10.23 @@ -40,6 +46,36 @@
   10.24  open Sledgehammer_Reconstructor
   10.25  open Sledgehammer_Isar
   10.26  open Sledgehammer_Prover
   10.27 +open Sledgehammer_Prover_ATP
   10.28 +open Sledgehammer_Prover_SMT
   10.29 +
   10.30 +fun is_prover_supported ctxt =
   10.31 +  let val thy = Proof_Context.theory_of ctxt in
   10.32 +    is_reconstructor orf is_atp thy orf is_smt_prover ctxt
   10.33 +  end
   10.34 +
   10.35 +fun is_prover_installed ctxt =
   10.36 +  is_reconstructor orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
   10.37 +
   10.38 +val reconstructor_default_max_facts = 20
   10.39 +
   10.40 +fun default_max_facts_of_prover ctxt name =
   10.41 +  let val thy = Proof_Context.theory_of ctxt in
   10.42 +    if is_reconstructor name then
   10.43 +      reconstructor_default_max_facts
   10.44 +    else if is_atp thy name then
   10.45 +      fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
   10.46 +    else (* is_smt_prover ctxt name *)
   10.47 +      SMT_Solver.default_max_relevant ctxt name
   10.48 +  end
   10.49 +
   10.50 +fun get_prover ctxt mode name =
   10.51 +  let val thy = Proof_Context.theory_of ctxt in
   10.52 +    if is_reconstructor name then run_reconstructor mode name
   10.53 +    else if is_atp thy name then run_atp mode name
   10.54 +    else if is_smt_prover ctxt name then run_smt_solver mode name
   10.55 +    else error ("No such prover: " ^ name ^ ".")
   10.56 +  end
   10.57  
   10.58  (* wrapper for calling external prover *)
   10.59  
   10.60 @@ -234,16 +270,17 @@
   10.61       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   10.62    end
   10.63  
   10.64 -fun maybe_minimize ctxt mode do_learn name
   10.65 -        (params as {verbose, isar_proofs, minimize, ...})
   10.66 -        ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
   10.67 -        (result as {outcome, used_facts, used_from, run_time, preplay, message,
   10.68 -                    message_tail} : prover_result) =
   10.69 +fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
   10.70 +    ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
   10.71 +    (result as {outcome, used_facts, used_from, run_time, preplay, message, message_tail} :
   10.72 +     prover_result) =
   10.73    if is_some outcome orelse null used_facts then
   10.74      result
   10.75    else
   10.76      let
   10.77 +      val thy = Proof_Context.theory_of ctxt
   10.78        val num_facts = length used_facts
   10.79 +
   10.80        val ((perhaps_minimize, (minimize_name, params)), preplay) =
   10.81          if mode = Normal then
   10.82            if num_facts >= Config.get ctxt auto_minimize_min_facts then
   10.83 @@ -261,7 +298,7 @@
   10.84                   if isar_proofs = SOME true then
   10.85                     (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
   10.86                        itself. *)
   10.87 -                   (can_min_fast_enough timeout, (isar_proof_reconstructor ctxt name, params))
   10.88 +                   (can_min_fast_enough timeout, (isar_supported_prover_of thy name, params))
   10.89                   else if can_min_fast_enough timeout then
   10.90                     (true, extract_reconstructor params reconstr
   10.91                            ||> (fn override_params =>
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Jan 31 12:30:54 2014 +0100
    11.3 @@ -0,0 +1,268 @@
    11.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
    11.5 +    Author:     Fabian Immler, TU Muenchen
    11.6 +    Author:     Makarius
    11.7 +    Author:     Jasmin Blanchette, TU Muenchen
    11.8 +
    11.9 +SMT solvers as Sledgehammer provers.
   11.10 +*)
   11.11 +
   11.12 +signature SLEDGEHAMMER_PROVER_SMT =
   11.13 +sig
   11.14 +  type stature = ATP_Problem_Generate.stature
   11.15 +  type mode = Sledgehammer_Prover.mode
   11.16 +  type prover = Sledgehammer_Prover.prover
   11.17 +
   11.18 +  val smt_builtins : bool Config.T
   11.19 +  val smt_triggers : bool Config.T
   11.20 +  val smt_weights : bool Config.T
   11.21 +  val smt_weight_min_facts : int Config.T
   11.22 +  val smt_min_weight : int Config.T
   11.23 +  val smt_max_weight : int Config.T
   11.24 +  val smt_max_weight_index : int Config.T
   11.25 +  val smt_weight_curve : (int -> int) Unsynchronized.ref
   11.26 +  val smt_max_slices : int Config.T
   11.27 +  val smt_slice_fact_frac : real Config.T
   11.28 +  val smt_slice_time_frac : real Config.T
   11.29 +  val smt_slice_min_secs : int Config.T
   11.30 +
   11.31 +  val select_smt_solver : string -> Proof.context -> Proof.context
   11.32 +  val is_smt_prover : Proof.context -> string -> bool
   11.33 +  val weight_smt_fact : Proof.context -> int -> ((string * stature) * thm) * int
   11.34 +    -> (string * stature) * (int option * thm)
   11.35 +  val run_smt_solver : mode -> string -> prover
   11.36 +end;
   11.37 +
   11.38 +structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
   11.39 +struct
   11.40 +
   11.41 +open ATP_Proof
   11.42 +open ATP_Util
   11.43 +open ATP_Systems
   11.44 +open ATP_Problem_Generate
   11.45 +open ATP_Proof_Reconstruct
   11.46 +open Sledgehammer_Util
   11.47 +open Sledgehammer_Reconstructor
   11.48 +open Sledgehammer_Isar_Print
   11.49 +open Sledgehammer_Prover
   11.50 +
   11.51 +val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
   11.52 +val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
   11.53 +val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
   11.54 +val smt_weight_min_facts =
   11.55 +  Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
   11.56 +
   11.57 +val select_smt_solver = Context.proof_map o SMT_Config.select_solver
   11.58 +
   11.59 +fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
   11.60 +
   11.61 +(* FUDGE *)
   11.62 +val smt_min_weight =
   11.63 +  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
   11.64 +val smt_max_weight =
   11.65 +  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
   11.66 +val smt_max_weight_index =
   11.67 +  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
   11.68 +val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
   11.69 +
   11.70 +fun smt_fact_weight ctxt j num_facts =
   11.71 +  if Config.get ctxt smt_weights andalso
   11.72 +     num_facts >= Config.get ctxt smt_weight_min_facts then
   11.73 +    let
   11.74 +      val min = Config.get ctxt smt_min_weight
   11.75 +      val max = Config.get ctxt smt_max_weight
   11.76 +      val max_index = Config.get ctxt smt_max_weight_index
   11.77 +      val curve = !smt_weight_curve
   11.78 +    in
   11.79 +      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
   11.80 +            div curve max_index)
   11.81 +    end
   11.82 +  else
   11.83 +    NONE
   11.84 +
   11.85 +fun weight_smt_fact ctxt num_facts ((info, th), j) =
   11.86 +  let val thy = Proof_Context.theory_of ctxt in
   11.87 +    (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
   11.88 +  end
   11.89 +
   11.90 +(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
   11.91 +   properly in the SMT module, we must interpret these here. *)
   11.92 +val z3_failures =
   11.93 +  [(101, OutOfResources),
   11.94 +   (103, MalformedInput),
   11.95 +   (110, MalformedInput),
   11.96 +   (112, TimedOut)]
   11.97 +val unix_failures =
   11.98 +  [(138, Crashed),
   11.99 +   (139, Crashed)]
  11.100 +val smt_failures = z3_failures @ unix_failures
  11.101 +
  11.102 +fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
  11.103 +    if is_real_cex then Unprovable else GaveUp
  11.104 +  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
  11.105 +  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
  11.106 +    (case AList.lookup (op =) smt_failures code of
  11.107 +      SOME failure => failure
  11.108 +    | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
  11.109 +  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
  11.110 +  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
  11.111 +
  11.112 +(* FUDGE *)
  11.113 +val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
  11.114 +val smt_slice_fact_frac =
  11.115 +  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667)
  11.116 +val smt_slice_time_frac =
  11.117 +  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
  11.118 +val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
  11.119 +
  11.120 +val is_boring_builtin_typ =
  11.121 +  not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
  11.122 +
  11.123 +fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
  11.124 +      ...} : params) state goal i =
  11.125 +  let
  11.126 +    fun repair_context ctxt =
  11.127 +      ctxt |> select_smt_solver name
  11.128 +           |> Config.put SMT_Config.verbose debug
  11.129 +           |> (if overlord then
  11.130 +                 Config.put SMT_Config.debug_files
  11.131 +                   (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
  11.132 +               else
  11.133 +                 I)
  11.134 +           |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
  11.135 +           |> not (Config.get ctxt smt_builtins)
  11.136 +              ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
  11.137 +                 #> Config.put SMT_Config.datatypes false)
  11.138 +           |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
  11.139 +                default_max_new_mono_instances
  11.140 +
  11.141 +    val state = Proof.map_context (repair_context) state
  11.142 +    val ctxt = Proof.context_of state
  11.143 +    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
  11.144 +
  11.145 +    fun do_slice timeout slice outcome0 time_so_far
  11.146 +                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
  11.147 +      let
  11.148 +        val timer = Timer.startRealTimer ()
  11.149 +        val slice_timeout =
  11.150 +          if slice < max_slices then
  11.151 +            let val ms = Time.toMilliseconds timeout in
  11.152 +              Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs,
  11.153 +                Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms)))
  11.154 +              |> Time.fromMilliseconds
  11.155 +            end
  11.156 +          else
  11.157 +            timeout
  11.158 +        val num_facts = length weighted_facts
  11.159 +        val _ =
  11.160 +          if debug then
  11.161 +            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
  11.162 +            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
  11.163 +            |> Output.urgent_message
  11.164 +          else
  11.165 +            ()
  11.166 +        val birth = Timer.checkRealTimer timer
  11.167 +        val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
  11.168 +
  11.169 +        val (outcome, used_facts) =
  11.170 +          SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
  11.171 +          |> SMT_Solver.smt_filter_apply slice_timeout
  11.172 +          |> (fn {outcome, used_facts} => (outcome, used_facts))
  11.173 +          handle exn =>
  11.174 +            if Exn.is_interrupt exn then reraise exn
  11.175 +            else (ML_Compiler.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
  11.176 +
  11.177 +        val death = Timer.checkRealTimer timer
  11.178 +        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
  11.179 +        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
  11.180 +
  11.181 +        val too_many_facts_perhaps =
  11.182 +          (case outcome of
  11.183 +            NONE => false
  11.184 +          | SOME (SMT_Failure.Counterexample _) => false
  11.185 +          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
  11.186 +          | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
  11.187 +          | SOME SMT_Failure.Out_Of_Memory => true
  11.188 +          | SOME (SMT_Failure.Other_Failure _) => true)
  11.189 +
  11.190 +        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
  11.191 +      in
  11.192 +        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
  11.193 +           Time.> (timeout, Time.zeroTime) then
  11.194 +          let
  11.195 +            val new_num_facts =
  11.196 +              Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
  11.197 +            val weighted_factss as (new_fact_filter, _) :: _ =
  11.198 +              weighted_factss
  11.199 +              |> (fn (x :: xs) => xs @ [x])
  11.200 +              |> app_hd (apsnd (take new_num_facts))
  11.201 +            val show_filter = fact_filter <> new_fact_filter
  11.202 +
  11.203 +            fun num_of_facts fact_filter num_facts =
  11.204 +              string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
  11.205 +              " fact" ^ plural_s num_facts
  11.206 +
  11.207 +            val _ =
  11.208 +              if debug then
  11.209 +                quote name ^ " invoked with " ^
  11.210 +                num_of_facts fact_filter num_facts ^ ": " ^
  11.211 +                string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
  11.212 +                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
  11.213 +                "..."
  11.214 +                |> Output.urgent_message
  11.215 +              else
  11.216 +                ()
  11.217 +          in
  11.218 +            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
  11.219 +          end
  11.220 +        else
  11.221 +          {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
  11.222 +           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
  11.223 +      end
  11.224 +  in
  11.225 +    do_slice timeout 1 NONE Time.zeroTime
  11.226 +  end
  11.227 +
  11.228 +fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
  11.229 +    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
  11.230 +  let
  11.231 +    val thy = Proof.theory_of state
  11.232 +    val ctxt = Proof.context_of state
  11.233 +
  11.234 +    fun weight_facts facts =
  11.235 +      let val num_facts = length facts in
  11.236 +        map (weight_smt_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
  11.237 +      end
  11.238 +
  11.239 +    val weighted_factss = factss |> map (apsnd weight_facts)
  11.240 +    val {outcome, used_facts = used_pairs, used_from, run_time} =
  11.241 +      smt_filter_loop name params state goal subgoal weighted_factss
  11.242 +    val used_facts = used_pairs |> map fst
  11.243 +    val outcome = outcome |> Option.map failure_of_smt_failure
  11.244 +
  11.245 +    val (preplay, message, message_tail) =
  11.246 +      (case outcome of
  11.247 +        NONE =>
  11.248 +        (Lazy.lazy (fn () =>
  11.249 +           play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT
  11.250 +             (bunch_of_reconstructors false (fn desperate =>
  11.251 +                if desperate then liftingN else default_metis_lam_trans))),
  11.252 +         fn preplay =>
  11.253 +            let
  11.254 +              val one_line_params =
  11.255 +                (preplay, proof_banner mode name, used_facts,
  11.256 +                 choose_minimize_command thy params minimize_command name preplay, subgoal,
  11.257 +                 subgoal_count)
  11.258 +              val num_chained = length (#facts (Proof.goal state))
  11.259 +            in
  11.260 +              one_line_proof_text num_chained one_line_params
  11.261 +            end,
  11.262 +         if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
  11.263 +      | SOME failure =>
  11.264 +        (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
  11.265 +  in
  11.266 +    {outcome = outcome, used_facts = used_facts, used_from = used_from,
  11.267 +     run_time = run_time, preplay = preplay, message = message,
  11.268 +     message_tail = message_tail}
  11.269 +  end
  11.270 +
  11.271 +end;