split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
authorblanchet
Wed Dec 08 22:17:52 2010 +0100 (2010-12-08)
changeset 41087d7b5fd465198
parent 41086 b4cccce25d9a
child 41088 54eb8e7c7f9b
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
src/HOL/IsaMakefile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Dec 08 18:07:04 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Dec 08 22:17:52 2010 +0100
     1.3 @@ -344,12 +344,13 @@
     1.4    Tools/record.ML \
     1.5    Tools/semiring_normalizer.ML \
     1.6    Tools/Sledgehammer/async_manager.ML \
     1.7 -  Tools/Sledgehammer/sledgehammer.ML \
     1.8 +  Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
     1.9 +  Tools/Sledgehammer/sledgehammer_atp_translate.ML \
    1.10    Tools/Sledgehammer/sledgehammer_filter.ML \
    1.11    Tools/Sledgehammer/sledgehammer_minimize.ML \
    1.12    Tools/Sledgehammer/sledgehammer_isar.ML \
    1.13 -  Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
    1.14 -  Tools/Sledgehammer/sledgehammer_atp_translate.ML \
    1.15 +  Tools/Sledgehammer/sledgehammer_provers.ML \
    1.16 +  Tools/Sledgehammer/sledgehammer_run.ML \
    1.17    Tools/Sledgehammer/sledgehammer_util.ML \
    1.18    Tools/smallvalue_generators.ML \
    1.19    Tools/SMT/smtlib_interface.ML \
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 08 18:07:04 2010 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 08 22:17:52 2010 +0100
     2.3 @@ -319,7 +319,8 @@
     2.4      fun default_prover_name () =
     2.5        hd (#provers (Sledgehammer_Isar.default_params ctxt []))
     2.6        handle Empty => error "No ATP available."
     2.7 -    fun get_prover name = (name, Sledgehammer.get_prover ctxt false name)
     2.8 +    fun get_prover name =
     2.9 +      (name, Sledgehammer_Provers.get_prover ctxt false name)
    2.10    in
    2.11      (case AList.lookup (op =) args proverK of
    2.12        SOME name => get_prover name
    2.13 @@ -344,22 +345,22 @@
    2.14      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
    2.15      val thy = ProofContext.theory_of ctxt
    2.16      val i = 1
    2.17 -    fun change_dir (SOME dir) = Config.put Sledgehammer.dest_dir dir
    2.18 +    fun change_dir (SOME dir) = Config.put Sledgehammer_Provers.dest_dir dir
    2.19        | change_dir NONE = I
    2.20      val st' =
    2.21        st |> Proof.map_context
    2.22                  (change_dir dir
    2.23 -                 #> Config.put Sledgehammer.measure_run_time true)
    2.24 +                 #> Config.put Sledgehammer_Provers.measure_run_time true)
    2.25      val params as {full_types, relevance_thresholds, max_relevant, ...} =
    2.26        Sledgehammer_Isar.default_params ctxt
    2.27            [("verbose", "true"),
    2.28             ("timeout", Int.toString timeout)]
    2.29      val default_max_relevant =
    2.30 -      Sledgehammer.default_max_relevant_for_prover ctxt prover_name
    2.31 +      Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name
    2.32      val is_built_in_const =
    2.33 -      Sledgehammer.is_built_in_const_for_prover ctxt prover_name
    2.34 +      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
    2.35      val relevance_fudge =
    2.36 -      Sledgehammer.relevance_fudge_for_prover ctxt prover_name
    2.37 +      Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
    2.38      val relevance_override = {add = [], del = [], only = false}
    2.39      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    2.40      val facts =
    2.41 @@ -369,13 +370,13 @@
    2.42      val problem =
    2.43        {state = st', goal = goal, subgoal = i,
    2.44         subgoal_count = Sledgehammer_Util.subgoal_count st,
    2.45 -       facts = facts |> map Sledgehammer.Untranslated}
    2.46 +       facts = facts |> map Sledgehammer_Provers.Untranslated}
    2.47      val time_limit =
    2.48        (case hard_timeout of
    2.49          NONE => I
    2.50        | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
    2.51      val ({outcome, message, used_facts, run_time_in_msecs, ...}
    2.52 -         : Sledgehammer.prover_result,
    2.53 +         : Sledgehammer_Provers.prover_result,
    2.54          time_isa) = time_limit (Mirabelle.cpu_time
    2.55                        (prover params (K ""))) problem
    2.56      val time_prover = run_time_in_msecs |> the_default ~1
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Dec 08 18:07:04 2010 +0100
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Dec 08 22:17:52 2010 +0100
     3.3 @@ -109,12 +109,12 @@
     3.4           val prover = AList.lookup (op =) args "prover"
     3.5                        |> the_default default_prover
     3.6           val default_max_relevant =
     3.7 -           Sledgehammer.default_max_relevant_for_prover ctxt prover
     3.8 +           Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover
     3.9          val is_built_in_const =
    3.10 -          Sledgehammer.is_built_in_const_for_prover ctxt default_prover
    3.11 +          Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
    3.12           val relevance_fudge =
    3.13             extract_relevance_fudge args
    3.14 -               (Sledgehammer.relevance_fudge_for_prover ctxt prover)
    3.15 +               (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
    3.16           val relevance_override = {add = [], del = [], only = false}
    3.17           val {relevance_thresholds, full_types, max_relevant, ...} =
    3.18             Sledgehammer_Isar.default_params ctxt args
     4.1 --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Wed Dec 08 18:07:04 2010 +0100
     4.2 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Wed Dec 08 22:17:52 2010 +0100
     4.3 @@ -22,12 +22,13 @@
     4.4         @ [("timeout", Int.toString (Time.toSeconds timeout))])
     4.5         @ [("overlord", "true")]
     4.6        |> Sledgehammer_Isar.default_params ctxt
     4.7 -    val prover = Sledgehammer.get_prover ctxt false name
     4.8 +    val prover = Sledgehammer_Provers.get_prover ctxt false name
     4.9      val default_max_relevant =
    4.10 -      Sledgehammer.default_max_relevant_for_prover ctxt name
    4.11 +      Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
    4.12      val is_built_in_const =
    4.13 -      Sledgehammer.is_built_in_const_for_prover ctxt name
    4.14 -    val relevance_fudge = Sledgehammer.relevance_fudge_for_prover ctxt name
    4.15 +      Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    4.16 +    val relevance_fudge =
    4.17 +      Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    4.18      val relevance_override = {add = [], del = [], only = false}
    4.19      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    4.20      val facts =
    4.21 @@ -43,7 +44,7 @@
    4.22                          (prop_of goal))
    4.23      val problem =
    4.24        {state = Proof.init ctxt, goal = goal, subgoal = i,
    4.25 -       subgoal_count = n, facts = map Sledgehammer.Untranslated facts}
    4.26 +       subgoal_count = n, facts = map Sledgehammer_Provers.Untranslated facts}
    4.27    in
    4.28      (case prover params (K "") problem of
    4.29        {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
     5.1 --- a/src/HOL/Sledgehammer.thy	Wed Dec 08 18:07:04 2010 +0100
     5.2 +++ b/src/HOL/Sledgehammer.thy	Wed Dec 08 22:17:52 2010 +0100
     5.3 @@ -13,8 +13,9 @@
     5.4       "Tools/Sledgehammer/sledgehammer_filter.ML"
     5.5       "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
     5.6       "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML"
     5.7 -     "Tools/Sledgehammer/sledgehammer.ML"
     5.8 +     "Tools/Sledgehammer/sledgehammer_provers.ML"
     5.9       "Tools/Sledgehammer/sledgehammer_minimize.ML"
    5.10 +     "Tools/Sledgehammer/sledgehammer_run.ML"
    5.11       "Tools/Sledgehammer/sledgehammer_isar.ML"
    5.12  begin
    5.13  
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Dec 08 18:07:04 2010 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,730 +0,0 @@
     6.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer.ML
     6.5 -    Author:     Fabian Immler, TU Muenchen
     6.6 -    Author:     Makarius
     6.7 -    Author:     Jasmin Blanchette, TU Muenchen
     6.8 -
     6.9 -Sledgehammer's heart.
    6.10 -*)
    6.11 -
    6.12 -signature SLEDGEHAMMER =
    6.13 -sig
    6.14 -  type failure = ATP_Proof.failure
    6.15 -  type locality = Sledgehammer_Filter.locality
    6.16 -  type relevance_fudge = Sledgehammer_Filter.relevance_fudge
    6.17 -  type relevance_override = Sledgehammer_Filter.relevance_override
    6.18 -  type translated_formula = Sledgehammer_ATP_Translate.translated_formula
    6.19 -  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
    6.20 -
    6.21 -  type params =
    6.22 -    {blocking: bool,
    6.23 -     debug: bool,
    6.24 -     verbose: bool,
    6.25 -     overlord: bool,
    6.26 -     provers: string list,
    6.27 -     full_types: bool,
    6.28 -     explicit_apply: bool,
    6.29 -     relevance_thresholds: real * real,
    6.30 -     max_relevant: int option,
    6.31 -     isar_proof: bool,
    6.32 -     isar_shrink_factor: int,
    6.33 -     timeout: Time.time,
    6.34 -     expect: string}
    6.35 -
    6.36 -  datatype fact =
    6.37 -    Untranslated of (string * locality) * thm |
    6.38 -    Translated of term * ((string * locality) * translated_formula) option
    6.39 -
    6.40 -  type prover_problem =
    6.41 -    {state: Proof.state,
    6.42 -     goal: thm,
    6.43 -     subgoal: int,
    6.44 -     subgoal_count: int,
    6.45 -     facts: fact list}
    6.46 -
    6.47 -  type prover_result =
    6.48 -    {outcome: failure option,
    6.49 -     used_facts: (string * locality) list,
    6.50 -     run_time_in_msecs: int option,
    6.51 -     message: string}
    6.52 -
    6.53 -  type prover = params -> minimize_command -> prover_problem -> prover_result
    6.54 -
    6.55 -  val is_prover_available : Proof.context -> string -> bool
    6.56 -  val is_prover_installed : Proof.context -> string -> bool
    6.57 -  val default_max_relevant_for_prover : Proof.context -> string -> int
    6.58 -  val is_built_in_const_for_prover :
    6.59 -    Proof.context -> string -> string * typ -> term list -> bool
    6.60 -  val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
    6.61 -  val dest_dir : string Config.T
    6.62 -  val problem_prefix : string Config.T
    6.63 -  val measure_run_time : bool Config.T
    6.64 -  val available_provers : Proof.context -> unit
    6.65 -  val kill_provers : unit -> unit
    6.66 -  val running_provers : unit -> unit
    6.67 -  val messages : int option -> unit
    6.68 -  val get_prover : Proof.context -> bool -> string -> prover
    6.69 -  val run_sledgehammer :
    6.70 -    params -> bool -> int -> relevance_override -> (string -> minimize_command)
    6.71 -    -> Proof.state -> bool * Proof.state
    6.72 -  val setup : theory -> theory
    6.73 -end;
    6.74 -
    6.75 -structure Sledgehammer : SLEDGEHAMMER =
    6.76 -struct
    6.77 -
    6.78 -open ATP_Problem
    6.79 -open ATP_Proof
    6.80 -open ATP_Systems
    6.81 -open Metis_Translate
    6.82 -open Sledgehammer_Util
    6.83 -open Sledgehammer_Filter
    6.84 -open Sledgehammer_ATP_Translate
    6.85 -open Sledgehammer_ATP_Reconstruct
    6.86 -
    6.87 -
    6.88 -(** The Sledgehammer **)
    6.89 -
    6.90 -(* Identifier to distinguish Sledgehammer from other tools using
    6.91 -   "Async_Manager". *)
    6.92 -val das_Tool = "Sledgehammer"
    6.93 -
    6.94 -fun is_smt_prover ctxt name =
    6.95 -  let val smts = SMT_Solver.available_solvers_of ctxt in
    6.96 -    case try (unprefix remote_prefix) name of
    6.97 -      SOME suffix => member (op =) smts suffix andalso
    6.98 -                     SMT_Solver.is_remotely_available ctxt suffix
    6.99 -    | NONE => member (op =) smts name
   6.100 -  end
   6.101 -
   6.102 -fun is_prover_available ctxt name =
   6.103 -  let val thy = ProofContext.theory_of ctxt in
   6.104 -    is_smt_prover ctxt name orelse member (op =) (available_atps thy) name
   6.105 -  end
   6.106 -
   6.107 -fun is_prover_installed ctxt name =
   6.108 -  let val thy = ProofContext.theory_of ctxt in
   6.109 -    if is_smt_prover ctxt name then
   6.110 -      String.isPrefix remote_prefix name orelse
   6.111 -      SMT_Solver.is_locally_installed ctxt name
   6.112 -    else
   6.113 -      is_atp_installed thy name
   6.114 -  end
   6.115 -
   6.116 -fun available_smt_solvers ctxt =
   6.117 -  let val smts = SMT_Solver.available_solvers_of ctxt in
   6.118 -    smts @ map (prefix remote_prefix)
   6.119 -               (filter (SMT_Solver.is_remotely_available ctxt) smts)
   6.120 -  end
   6.121 -
   6.122 -(* FUDGE *)
   6.123 -val auto_max_relevant_divisor = 2
   6.124 -
   6.125 -fun default_max_relevant_for_prover ctxt name =
   6.126 -  let val thy = ProofContext.theory_of ctxt in
   6.127 -    if is_smt_prover ctxt name then
   6.128 -      SMT_Solver.default_max_relevant ctxt
   6.129 -          (perhaps (try (unprefix remote_prefix)) name)
   6.130 -    else
   6.131 -      #default_max_relevant (get_atp thy name)
   6.132 -  end
   6.133 -
   6.134 -(* These are typically simplified away by "Meson.presimplify". Equality is
   6.135 -   handled specially via "fequal". *)
   6.136 -val atp_irrelevant_consts =
   6.137 -  [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
   6.138 -   @{const_name HOL.eq}]
   6.139 -
   6.140 -fun is_built_in_const_for_prover ctxt name (s, T) args =
   6.141 -  if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args
   6.142 -  else member (op =) atp_irrelevant_consts s
   6.143 -
   6.144 -(* FUDGE *)
   6.145 -val atp_relevance_fudge =
   6.146 -  {worse_irrel_freq = 100.0,
   6.147 -   higher_order_irrel_weight = 1.05,
   6.148 -   abs_rel_weight = 0.5,
   6.149 -   abs_irrel_weight = 2.0,
   6.150 -   skolem_irrel_weight = 0.75,
   6.151 -   theory_const_rel_weight = 0.5,
   6.152 -   theory_const_irrel_weight = 0.25,
   6.153 -   intro_bonus = 0.15,
   6.154 -   elim_bonus = 0.15,
   6.155 -   simp_bonus = 0.15,
   6.156 -   local_bonus = 0.55,
   6.157 -   assum_bonus = 1.05,
   6.158 -   chained_bonus = 1.5,
   6.159 -   max_imperfect = 11.5,
   6.160 -   max_imperfect_exp = 1.0,
   6.161 -   threshold_divisor = 2.0,
   6.162 -   ridiculous_threshold = 0.1}
   6.163 -
   6.164 -(* FUDGE (FIXME) *)
   6.165 -val smt_relevance_fudge =
   6.166 -  {worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
   6.167 -   higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
   6.168 -   abs_rel_weight = #abs_rel_weight atp_relevance_fudge,
   6.169 -   abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,
   6.170 -   skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,
   6.171 -   theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,
   6.172 -   theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,
   6.173 -   intro_bonus = #intro_bonus atp_relevance_fudge,
   6.174 -   elim_bonus = #elim_bonus atp_relevance_fudge,
   6.175 -   simp_bonus = #simp_bonus atp_relevance_fudge,
   6.176 -   local_bonus = #local_bonus atp_relevance_fudge,
   6.177 -   assum_bonus = #assum_bonus atp_relevance_fudge,
   6.178 -   chained_bonus = #chained_bonus atp_relevance_fudge,
   6.179 -   max_imperfect = #max_imperfect atp_relevance_fudge,
   6.180 -   max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge,
   6.181 -   threshold_divisor = #threshold_divisor atp_relevance_fudge,
   6.182 -   ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
   6.183 -
   6.184 -fun relevance_fudge_for_prover ctxt name =
   6.185 -  if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
   6.186 -
   6.187 -fun available_provers ctxt =
   6.188 -  let
   6.189 -    val thy = ProofContext.theory_of ctxt
   6.190 -    val (remote_provers, local_provers) =
   6.191 -      sort_strings (available_atps thy) @
   6.192 -      sort_strings (available_smt_solvers ctxt)
   6.193 -      |> List.partition (String.isPrefix remote_prefix)
   6.194 -  in
   6.195 -    Output.urgent_message ("Available provers: " ^
   6.196 -                           commas (local_provers @ remote_provers) ^ ".")
   6.197 -  end
   6.198 -
   6.199 -fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
   6.200 -fun running_provers () = Async_Manager.running_threads das_Tool "provers"
   6.201 -val messages = Async_Manager.thread_messages das_Tool "prover"
   6.202 -
   6.203 -(** problems, results, ATPs, etc. **)
   6.204 -
   6.205 -type params =
   6.206 -  {blocking: bool,
   6.207 -   debug: bool,
   6.208 -   verbose: bool,
   6.209 -   overlord: bool,
   6.210 -   provers: string list,
   6.211 -   full_types: bool,
   6.212 -   explicit_apply: bool,
   6.213 -   relevance_thresholds: real * real,
   6.214 -   max_relevant: int option,
   6.215 -   isar_proof: bool,
   6.216 -   isar_shrink_factor: int,
   6.217 -   timeout: Time.time,
   6.218 -   expect: string}
   6.219 -
   6.220 -datatype fact =
   6.221 -  Untranslated of (string * locality) * thm |
   6.222 -  Translated of term * ((string * locality) * translated_formula) option
   6.223 -
   6.224 -type prover_problem =
   6.225 -  {state: Proof.state,
   6.226 -   goal: thm,
   6.227 -   subgoal: int,
   6.228 -   subgoal_count: int,
   6.229 -   facts: fact list}
   6.230 -
   6.231 -type prover_result =
   6.232 -  {outcome: failure option,
   6.233 -   message: string,
   6.234 -   used_facts: (string * locality) list,
   6.235 -   run_time_in_msecs: int option}
   6.236 -
   6.237 -type prover = params -> minimize_command -> prover_problem -> prover_result
   6.238 -
   6.239 -(* configuration attributes *)
   6.240 -
   6.241 -val (dest_dir, dest_dir_setup) =
   6.242 -  Attrib.config_string "sledgehammer_dest_dir" (K "")
   6.243 -  (* Empty string means create files in Isabelle's temporary files directory. *)
   6.244 -
   6.245 -val (problem_prefix, problem_prefix_setup) =
   6.246 -  Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
   6.247 -
   6.248 -val (measure_run_time, measure_run_time_setup) =
   6.249 -  Attrib.config_bool "sledgehammer_measure_run_time" (K false)
   6.250 -
   6.251 -fun with_path cleanup after f path =
   6.252 -  Exn.capture f path
   6.253 -  |> tap (fn _ => cleanup path)
   6.254 -  |> Exn.release
   6.255 -  |> tap (after path)
   6.256 -
   6.257 -fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
   6.258 -                       n goal =
   6.259 -  quote name ^
   6.260 -  (if verbose then
   6.261 -     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
   6.262 -   else
   6.263 -     "") ^
   6.264 -  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
   6.265 -  (if blocking then
   6.266 -     ""
   6.267 -   else
   6.268 -     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
   6.269 -
   6.270 -fun proof_banner auto =
   6.271 -  if auto then "Auto Sledgehammer found a proof" else "Try this command"
   6.272 -
   6.273 -(* generic TPTP-based ATPs *)
   6.274 -
   6.275 -fun dest_Untranslated (Untranslated p) = p
   6.276 -  | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
   6.277 -fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p
   6.278 -  | translated_fact _ (Translated p) = p
   6.279 -fun fact_name (Untranslated ((name, _), _)) = SOME name
   6.280 -  | fact_name (Translated (_, p)) = Option.map (fst o fst) p
   6.281 -
   6.282 -fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
   6.283 -  | int_opt_add _ _ = NONE
   6.284 -
   6.285 -(* Important messages are important but not so important that users want to see
   6.286 -   them each time. *)
   6.287 -val important_message_keep_factor = 0.1
   6.288 -
   6.289 -fun run_atp auto atp_name
   6.290 -        {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
   6.291 -         known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
   6.292 -        ({debug, verbose, overlord, full_types, explicit_apply, isar_proof,
   6.293 -          isar_shrink_factor, timeout, ...} : params)
   6.294 -        minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   6.295 -  let
   6.296 -    val ctxt = Proof.context_of state
   6.297 -    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
   6.298 -    val facts =
   6.299 -      facts |> map (translated_fact ctxt)
   6.300 -    val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   6.301 -                   else Config.get ctxt dest_dir
   6.302 -    val problem_prefix = Config.get ctxt problem_prefix
   6.303 -    val problem_file_name =
   6.304 -      Path.basic ((if overlord then "prob_" ^ atp_name
   6.305 -                   else problem_prefix ^ serial_string ())
   6.306 -                  ^ "_" ^ string_of_int subgoal)
   6.307 -    val problem_path_name =
   6.308 -      if dest_dir = "" then
   6.309 -        File.tmp_path problem_file_name
   6.310 -      else if File.exists (Path.explode dest_dir) then
   6.311 -        Path.append (Path.explode dest_dir) problem_file_name
   6.312 -      else
   6.313 -        error ("No such directory: " ^ quote dest_dir ^ ".")
   6.314 -    val measure_run_time = verbose orelse Config.get ctxt measure_run_time
   6.315 -    val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
   6.316 -    (* write out problem file and call ATP *)
   6.317 -    fun command_line complete timeout probfile =
   6.318 -      let
   6.319 -        val core = File.shell_path command ^ " " ^ arguments complete timeout ^
   6.320 -                   " " ^ File.shell_path probfile
   6.321 -      in
   6.322 -        (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
   6.323 -         else "exec " ^ core) ^ " 2>&1"
   6.324 -      end
   6.325 -    fun split_time s =
   6.326 -      let
   6.327 -        val split = String.tokens (fn c => str c = "\n");
   6.328 -        val (output, t) = s |> split |> split_last |> apfst cat_lines;
   6.329 -        fun as_num f = f >> (fst o read_int);
   6.330 -        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   6.331 -        val digit = Scan.one Symbol.is_ascii_digit;
   6.332 -        val num3 = as_num (digit ::: digit ::: (digit >> single));
   6.333 -        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   6.334 -        val as_time = Scan.read Symbol.stopper time o raw_explode
   6.335 -      in (output, as_time t) end;
   6.336 -    fun run_on probfile =
   6.337 -      case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
   6.338 -        (home_var, _) :: _ =>
   6.339 -        error ("The environment variable " ^ quote home_var ^ " is not set.")
   6.340 -      | [] =>
   6.341 -        if File.exists command then
   6.342 -          let
   6.343 -            fun run complete timeout =
   6.344 -              let
   6.345 -                val command = command_line complete timeout probfile
   6.346 -                val ((output, msecs), res_code) =
   6.347 -                  bash_output command
   6.348 -                  |>> (if overlord then
   6.349 -                         prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   6.350 -                       else
   6.351 -                         I)
   6.352 -                  |>> (if measure_run_time then split_time else rpair NONE)
   6.353 -                val (tstplike_proof, outcome) =
   6.354 -                  extract_tstplike_proof_and_outcome complete res_code
   6.355 -                      proof_delims known_failures output
   6.356 -              in (output, msecs, tstplike_proof, outcome) end
   6.357 -            val readable_names = debug andalso overlord
   6.358 -            val (atp_problem, pool, conjecture_offset, fact_names) =
   6.359 -              prepare_atp_problem ctxt readable_names explicit_forall full_types
   6.360 -                                  explicit_apply hyp_ts concl_t facts
   6.361 -            val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
   6.362 -                                                  atp_problem
   6.363 -            val _ = File.write_list probfile ss
   6.364 -            val conjecture_shape =
   6.365 -              conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   6.366 -              |> map single
   6.367 -            val run_twice = has_incomplete_mode andalso not auto
   6.368 -            val timer = Timer.startRealTimer ()
   6.369 -            val result =
   6.370 -              run false (if run_twice then
   6.371 -                           Time.fromMilliseconds
   6.372 -                                         (2 * Time.toMilliseconds timeout div 3)
   6.373 -                         else
   6.374 -                           timeout)
   6.375 -              |> run_twice
   6.376 -                 ? (fn (_, msecs0, _, SOME _) =>
   6.377 -                       run true (Time.- (timeout, Timer.checkRealTimer timer))
   6.378 -                       |> (fn (output, msecs, tstplike_proof, outcome) =>
   6.379 -                              (output, int_opt_add msecs0 msecs, tstplike_proof,
   6.380 -                               outcome))
   6.381 -                     | result => result)
   6.382 -          in ((pool, conjecture_shape, fact_names), result) end
   6.383 -        else
   6.384 -          error ("Bad executable: " ^ Path.implode command ^ ".")
   6.385 -
   6.386 -    (* If the problem file has not been exported, remove it; otherwise, export
   6.387 -       the proof file too. *)
   6.388 -    fun cleanup probfile =
   6.389 -      if dest_dir = "" then try File.rm probfile else NONE
   6.390 -    fun export probfile (_, (output, _, _, _)) =
   6.391 -      if dest_dir = "" then
   6.392 -        ()
   6.393 -      else
   6.394 -        File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   6.395 -    val ((pool, conjecture_shape, fact_names),
   6.396 -         (output, msecs, tstplike_proof, outcome)) =
   6.397 -      with_path cleanup export run_on problem_path_name
   6.398 -    val (conjecture_shape, fact_names) =
   6.399 -      repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
   6.400 -    val important_message =
   6.401 -      if not auto andalso random () <= important_message_keep_factor then
   6.402 -        extract_important_message output
   6.403 -      else
   6.404 -        ""
   6.405 -    val (message, used_facts) =
   6.406 -      case outcome of
   6.407 -        NONE =>
   6.408 -        proof_text isar_proof
   6.409 -            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   6.410 -            (proof_banner auto, full_types, minimize_command, tstplike_proof,
   6.411 -             fact_names, goal, subgoal)
   6.412 -        |>> (fn message =>
   6.413 -                message ^
   6.414 -                (if verbose then
   6.415 -                   "\nATP real CPU time: " ^
   6.416 -                   string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
   6.417 -                 else
   6.418 -                   "") ^
   6.419 -                (if important_message <> "" then
   6.420 -                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
   6.421 -                   important_message
   6.422 -                 else
   6.423 -                   ""))
   6.424 -      | SOME failure => (string_for_failure "ATP" failure, [])
   6.425 -  in
   6.426 -    {outcome = outcome, message = message, used_facts = used_facts,
   6.427 -     run_time_in_msecs = msecs}
   6.428 -  end
   6.429 -
   6.430 -(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
   6.431 -   these are sorted out properly in the SMT module, we have to interpret these
   6.432 -   ourselves. *)
   6.433 -val remote_smt_failures =
   6.434 -  [(22, CantConnect),
   6.435 -   (127, NoPerl),
   6.436 -   (2, NoLibwwwPerl)]
   6.437 -val z3_failures =
   6.438 -  [(103, MalformedInput),
   6.439 -   (110, MalformedInput)]
   6.440 -val unix_failures =
   6.441 -  [(139, Crashed)]
   6.442 -val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
   6.443 -
   6.444 -fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
   6.445 -  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   6.446 -  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
   6.447 -    (case AList.lookup (op =) smt_failures code of
   6.448 -       SOME failure => failure
   6.449 -     | NONE => UnknownError)
   6.450 -  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   6.451 -  | failure_from_smt_failure _ = UnknownError
   6.452 -
   6.453 -(* FUDGE *)
   6.454 -val smt_max_iter = 8
   6.455 -val smt_iter_fact_divisor = 2
   6.456 -val smt_iter_min_msecs = 5000
   6.457 -val smt_iter_timeout_divisor = 2
   6.458 -val smt_monomorph_limit = 4
   6.459 -
   6.460 -fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i =
   6.461 -  let
   6.462 -    val ctxt = Proof.context_of state
   6.463 -    fun iter timeout iter_num outcome0 msecs_so_far facts =
   6.464 -      let
   6.465 -        val timer = Timer.startRealTimer ()
   6.466 -        val ms = timeout |> Time.toMilliseconds
   6.467 -        val iter_timeout =
   6.468 -          if iter_num < smt_max_iter then
   6.469 -            Int.min (ms, Int.max (smt_iter_min_msecs,
   6.470 -                                  ms div smt_iter_timeout_divisor))
   6.471 -            |> Time.fromMilliseconds
   6.472 -          else
   6.473 -            timeout
   6.474 -        val num_facts = length facts
   6.475 -        val _ =
   6.476 -          if verbose then
   6.477 -            "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^
   6.478 -            plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..."
   6.479 -            |> Output.urgent_message
   6.480 -          else
   6.481 -            ()
   6.482 -        val {outcome, used_facts, run_time_in_msecs} =
   6.483 -          SMT_Solver.smt_filter remote iter_timeout state facts i
   6.484 -        val _ =
   6.485 -          if verbose andalso is_some outcome then
   6.486 -            "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
   6.487 -            |> Output.urgent_message
   6.488 -          else
   6.489 -            ()
   6.490 -        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   6.491 -        val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
   6.492 -        val too_many_facts_perhaps =
   6.493 -          case outcome of
   6.494 -            NONE => false
   6.495 -          | SOME (SMT_Failure.Counterexample _) => false
   6.496 -          | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
   6.497 -          | SOME (SMT_Failure.Abnormal_Termination code) =>
   6.498 -            (if verbose then
   6.499 -               "The SMT solver invoked with " ^ string_of_int num_facts ^
   6.500 -               " fact" ^ plural_s num_facts ^ " terminated abnormally with \
   6.501 -               \exit code " ^ string_of_int code ^ "."
   6.502 -               |> warning
   6.503 -             else
   6.504 -               ();
   6.505 -             true (* kind of *))
   6.506 -          | SOME SMT_Failure.Out_Of_Memory => true
   6.507 -          | SOME _ => true
   6.508 -        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   6.509 -      in
   6.510 -        if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso
   6.511 -           num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
   6.512 -          let val facts = take (num_facts div smt_iter_fact_divisor) facts in
   6.513 -            iter timeout (iter_num + 1) outcome0 msecs_so_far facts
   6.514 -          end
   6.515 -        else
   6.516 -          {outcome = if is_none outcome then NONE else the outcome0,
   6.517 -           used_facts = used_facts, run_time_in_msecs = msecs_so_far}
   6.518 -      end
   6.519 -  in iter timeout 1 NONE (SOME 0) end
   6.520 -
   6.521 -(* taken from "Mirabelle" and generalized *)
   6.522 -fun can_apply timeout tac state i =
   6.523 -  let
   6.524 -    val {context = ctxt, facts, goal} = Proof.goal state
   6.525 -    val full_tac = Method.insert_tac facts i THEN tac ctxt i
   6.526 -  in
   6.527 -    case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
   6.528 -      SOME (SOME _) => true
   6.529 -    | _ => false
   6.530 -  end
   6.531 -
   6.532 -val smt_metis_timeout = seconds 0.5
   6.533 -
   6.534 -fun can_apply_metis debug state i ths =
   6.535 -  can_apply smt_metis_timeout
   6.536 -            (Config.put Metis_Tactics.verbose debug
   6.537 -             #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
   6.538 -
   6.539 -fun run_smt_solver auto name (params as {debug, ...}) minimize_command
   6.540 -        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   6.541 -  let
   6.542 -    val (remote, suffix) =
   6.543 -      case try (unprefix remote_prefix) name of
   6.544 -        SOME suffix => (true, suffix)
   6.545 -      | NONE => (false, name)
   6.546 -    val repair_context =
   6.547 -      Context.proof_map (SMT_Config.select_solver suffix)
   6.548 -      #> Config.put SMT_Config.verbose debug
   6.549 -      #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
   6.550 -    val state = state |> Proof.map_context repair_context
   6.551 -    val thy = Proof.theory_of state
   6.552 -    val get_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
   6.553 -    val facts = facts |> map_filter get_fact
   6.554 -    val {outcome, used_facts, run_time_in_msecs} =
   6.555 -      smt_filter_loop params remote state subgoal facts
   6.556 -    val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
   6.557 -    val outcome = outcome |> Option.map failure_from_smt_failure
   6.558 -    val message =
   6.559 -      case outcome of
   6.560 -        NONE =>
   6.561 -        let
   6.562 -          val method =
   6.563 -            if can_apply_metis debug state subgoal (map snd used_facts) then
   6.564 -              "metis"
   6.565 -            else
   6.566 -              "smt"
   6.567 -        in
   6.568 -          try_command_line (proof_banner auto)
   6.569 -                           (apply_on_subgoal subgoal subgoal_count ^
   6.570 -                            command_call method (map fst other_lemmas)) ^
   6.571 -          minimize_line minimize_command
   6.572 -                        (map fst (other_lemmas @ chained_lemmas))
   6.573 -        end
   6.574 -      | SOME failure => string_for_failure "SMT solver" failure
   6.575 -  in
   6.576 -    {outcome = outcome, used_facts = map fst used_facts,
   6.577 -     run_time_in_msecs = run_time_in_msecs, message = message}
   6.578 -  end
   6.579 -
   6.580 -fun get_prover ctxt auto name =
   6.581 -  let val thy = ProofContext.theory_of ctxt in
   6.582 -    if is_smt_prover ctxt name then
   6.583 -      run_smt_solver auto name
   6.584 -    else if member (op =) (available_atps thy) name then
   6.585 -      run_atp auto name (get_atp thy name)
   6.586 -    else
   6.587 -      error ("No such prover: " ^ name ^ ".")
   6.588 -  end
   6.589 -
   6.590 -fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
   6.591 -               auto minimize_command only
   6.592 -               {state, goal, subgoal, subgoal_count, facts} name =
   6.593 -  let
   6.594 -    val ctxt = Proof.context_of state
   6.595 -    val birth_time = Time.now ()
   6.596 -    val death_time = Time.+ (birth_time, timeout)
   6.597 -    val max_relevant =
   6.598 -      the_default (default_max_relevant_for_prover ctxt name) max_relevant
   6.599 -    val num_facts = length facts |> not only ? Integer.min max_relevant
   6.600 -    val desc =
   6.601 -      prover_description ctxt params name num_facts subgoal subgoal_count goal
   6.602 -    val prover = get_prover ctxt auto name
   6.603 -    val problem =
   6.604 -      {state = state, goal = goal, subgoal = subgoal,
   6.605 -       subgoal_count = subgoal_count, facts = take num_facts facts}
   6.606 -    fun go () =
   6.607 -      let
   6.608 -        fun really_go () =
   6.609 -          prover params (minimize_command name) problem
   6.610 -          |> (fn {outcome, message, ...} =>
   6.611 -                 (if is_some outcome then "none" else "some", message))
   6.612 -        val (outcome_code, message) =
   6.613 -          if debug then
   6.614 -            really_go ()
   6.615 -          else
   6.616 -            (really_go ()
   6.617 -             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
   6.618 -                  | exn =>
   6.619 -                    if Exn.is_interrupt exn then
   6.620 -                      reraise exn
   6.621 -                    else
   6.622 -                      ("unknown", "Internal error:\n" ^
   6.623 -                                  ML_Compiler.exn_message exn ^ "\n"))
   6.624 -        val _ =
   6.625 -          if expect = "" orelse outcome_code = expect then
   6.626 -            ()
   6.627 -          else if blocking then
   6.628 -            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
   6.629 -          else
   6.630 -            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
   6.631 -      in (outcome_code = "some", message) end
   6.632 -  in
   6.633 -    if auto then
   6.634 -      let val (success, message) = TimeLimit.timeLimit timeout go () in
   6.635 -        (success, state |> success ? Proof.goal_message (fn () =>
   6.636 -             Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
   6.637 -                 (Pretty.str message)]))
   6.638 -      end
   6.639 -    else if blocking then
   6.640 -      let val (success, message) = TimeLimit.timeLimit timeout go () in
   6.641 -        List.app Output.urgent_message
   6.642 -                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
   6.643 -        (success, state)
   6.644 -      end
   6.645 -    else
   6.646 -      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
   6.647 -       (false, state))
   6.648 -  end
   6.649 -
   6.650 -fun run_sledgehammer (params as {blocking, debug, provers, full_types,
   6.651 -                                 relevance_thresholds, max_relevant, ...})
   6.652 -                     auto i (relevance_override as {only, ...}) minimize_command
   6.653 -                     state =
   6.654 -  if null provers then
   6.655 -    error "No prover is set."
   6.656 -  else case subgoal_count state of
   6.657 -    0 => (Output.urgent_message "No subgoal!"; (false, state))
   6.658 -  | n =>
   6.659 -    let
   6.660 -      val _ = Proof.assert_backward state
   6.661 -      val ctxt = Proof.context_of state
   6.662 -      val {facts = chained_ths, goal, ...} = Proof.goal state
   6.663 -      val (_, hyp_ts, concl_t) = strip_subgoal goal i
   6.664 -      val _ = () |> not blocking ? kill_provers
   6.665 -      val _ = case find_first (not o is_prover_available ctxt) provers of
   6.666 -                SOME name => error ("No such prover: " ^ name ^ ".")
   6.667 -              | NONE => ()
   6.668 -      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
   6.669 -      val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
   6.670 -      fun run_provers label full_types relevance_fudge maybe_translate provers
   6.671 -                      (res as (success, state)) =
   6.672 -        if success orelse null provers then
   6.673 -          res
   6.674 -        else
   6.675 -          let
   6.676 -            val max_max_relevant =
   6.677 -              case max_relevant of
   6.678 -                SOME n => n
   6.679 -              | NONE =>
   6.680 -                0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
   6.681 -                          provers
   6.682 -                  |> auto ? (fn n => n div auto_max_relevant_divisor)
   6.683 -            val is_built_in_const =
   6.684 -              is_built_in_const_for_prover ctxt (hd provers)
   6.685 -            val facts =
   6.686 -              relevant_facts ctxt full_types relevance_thresholds
   6.687 -                             max_max_relevant is_built_in_const relevance_fudge
   6.688 -                             relevance_override chained_ths hyp_ts concl_t
   6.689 -              |> map maybe_translate
   6.690 -            val problem =
   6.691 -              {state = state, goal = goal, subgoal = i, subgoal_count = n,
   6.692 -               facts = facts}
   6.693 -            val run_prover = run_prover params auto minimize_command only
   6.694 -          in
   6.695 -            if debug then
   6.696 -              Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
   6.697 -                  (if null facts then
   6.698 -                     "Found no relevant facts."
   6.699 -                   else
   6.700 -                     "Including (up to) " ^ string_of_int (length facts) ^
   6.701 -                     " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
   6.702 -                     (facts |> map_filter fact_name
   6.703 -                            |> space_implode " ") ^ "."))
   6.704 -            else
   6.705 -              ();
   6.706 -            if auto then
   6.707 -              fold (fn prover => fn (true, state) => (true, state)
   6.708 -                                  | (false, _) => run_prover problem prover)
   6.709 -                   provers (false, state)
   6.710 -            else
   6.711 -              provers |> (if blocking then Par_List.map else map)
   6.712 -                             (run_prover problem)
   6.713 -                      |> exists fst |> rpair state
   6.714 -          end
   6.715 -      val run_atps =
   6.716 -        run_provers "ATP" full_types atp_relevance_fudge
   6.717 -                    (Translated o translate_fact ctxt) atps
   6.718 -      val run_smts =
   6.719 -        run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
   6.720 -      fun run_atps_and_smt_solvers () =
   6.721 -        [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
   6.722 -    in
   6.723 -      (false, state)
   6.724 -      |> (if blocking then run_atps #> not auto ? run_smts
   6.725 -          else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
   6.726 -    end
   6.727 -
   6.728 -val setup =
   6.729 -  dest_dir_setup
   6.730 -  #> problem_prefix_setup
   6.731 -  #> measure_run_time_setup
   6.732 -
   6.733 -end;
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 08 18:07:04 2010 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 08 22:17:52 2010 +0100
     7.3 @@ -6,7 +6,7 @@
     7.4  
     7.5  signature SLEDGEHAMMER_ISAR =
     7.6  sig
     7.7 -  type params = Sledgehammer.params
     7.8 +  type params = Sledgehammer_Provers.params
     7.9  
    7.10    val auto : bool Unsynchronized.ref
    7.11    val provers : string Unsynchronized.ref
    7.12 @@ -21,8 +21,9 @@
    7.13  
    7.14  open ATP_Systems
    7.15  open Sledgehammer_Util
    7.16 -open Sledgehammer
    7.17 +open Sledgehammer_Provers
    7.18  open Sledgehammer_Minimize
    7.19 +open Sledgehammer_Run
    7.20  
    7.21  val auto = Unsynchronized.ref false
    7.22  
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Dec 08 18:07:04 2010 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Dec 08 22:17:52 2010 +0100
     8.3 @@ -8,7 +8,7 @@
     8.4  signature SLEDGEHAMMER_MINIMIZE =
     8.5  sig
     8.6    type locality = Sledgehammer_Filter.locality
     8.7 -  type params = Sledgehammer.params
     8.8 +  type params = Sledgehammer_Provers.params
     8.9  
    8.10    val minimize_facts :
    8.11      params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
    8.12 @@ -23,7 +23,7 @@
    8.13  open ATP_Proof
    8.14  open Sledgehammer_Util
    8.15  open Sledgehammer_Filter
    8.16 -open Sledgehammer
    8.17 +open Sledgehammer_Provers
    8.18  
    8.19  (* wrapper for calling external prover *)
    8.20  
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 08 22:17:52 2010 +0100
     9.3 @@ -0,0 +1,648 @@
     9.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     9.5 +    Author:     Fabian Immler, TU Muenchen
     9.6 +    Author:     Makarius
     9.7 +    Author:     Jasmin Blanchette, TU Muenchen
     9.8 +
     9.9 +Generic prover abstraction for Sledgehammer.
    9.10 +*)
    9.11 +
    9.12 +signature SLEDGEHAMMER_PROVERS =
    9.13 +sig
    9.14 +  type failure = ATP_Proof.failure
    9.15 +  type locality = Sledgehammer_Filter.locality
    9.16 +  type relevance_fudge = Sledgehammer_Filter.relevance_fudge
    9.17 +  type translated_formula = Sledgehammer_ATP_Translate.translated_formula
    9.18 +  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
    9.19 +
    9.20 +  type params =
    9.21 +    {blocking: bool,
    9.22 +     debug: bool,
    9.23 +     verbose: bool,
    9.24 +     overlord: bool,
    9.25 +     provers: string list,
    9.26 +     full_types: bool,
    9.27 +     explicit_apply: bool,
    9.28 +     relevance_thresholds: real * real,
    9.29 +     max_relevant: int option,
    9.30 +     isar_proof: bool,
    9.31 +     isar_shrink_factor: int,
    9.32 +     timeout: Time.time,
    9.33 +     expect: string}
    9.34 +
    9.35 +  datatype fact =
    9.36 +    Untranslated of (string * locality) * thm |
    9.37 +    Translated of term * ((string * locality) * translated_formula) option
    9.38 +
    9.39 +  type prover_problem =
    9.40 +    {state: Proof.state,
    9.41 +     goal: thm,
    9.42 +     subgoal: int,
    9.43 +     subgoal_count: int,
    9.44 +     facts: fact list}
    9.45 +
    9.46 +  type prover_result =
    9.47 +    {outcome: failure option,
    9.48 +     used_facts: (string * locality) list,
    9.49 +     run_time_in_msecs: int option,
    9.50 +     message: string}
    9.51 +
    9.52 +  type prover = params -> minimize_command -> prover_problem -> prover_result
    9.53 +
    9.54 +  val is_smt_prover : Proof.context -> string -> bool
    9.55 +  val is_prover_available : Proof.context -> string -> bool
    9.56 +  val is_prover_installed : Proof.context -> string -> bool
    9.57 +  val default_max_relevant_for_prover : Proof.context -> string -> int
    9.58 +  val is_built_in_const_for_prover :
    9.59 +    Proof.context -> string -> string * typ -> term list -> bool
    9.60 +  val atp_relevance_fudge : relevance_fudge
    9.61 +  val smt_relevance_fudge : relevance_fudge
    9.62 +  val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
    9.63 +  val dest_dir : string Config.T
    9.64 +  val problem_prefix : string Config.T
    9.65 +  val measure_run_time : bool Config.T
    9.66 +  val available_provers : Proof.context -> unit
    9.67 +  val kill_provers : unit -> unit
    9.68 +  val running_provers : unit -> unit
    9.69 +  val messages : int option -> unit
    9.70 +  val get_prover : Proof.context -> bool -> string -> prover
    9.71 +  val run_prover :
    9.72 +    params -> bool -> (string -> minimize_command) -> bool -> prover_problem
    9.73 +    -> string -> bool * Proof.state
    9.74 +  val setup : theory -> theory
    9.75 +end;
    9.76 +
    9.77 +structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
    9.78 +struct
    9.79 +
    9.80 +open ATP_Problem
    9.81 +open ATP_Proof
    9.82 +open ATP_Systems
    9.83 +open Metis_Translate
    9.84 +open Sledgehammer_Util
    9.85 +open Sledgehammer_Filter
    9.86 +open Sledgehammer_ATP_Translate
    9.87 +open Sledgehammer_ATP_Reconstruct
    9.88 +
    9.89 +(** The Sledgehammer **)
    9.90 +
    9.91 +(* Identifier to distinguish Sledgehammer from other tools using
    9.92 +   "Async_Manager". *)
    9.93 +val das_Tool = "Sledgehammer"
    9.94 +
    9.95 +fun is_smt_prover ctxt name =
    9.96 +  let val smts = SMT_Solver.available_solvers_of ctxt in
    9.97 +    case try (unprefix remote_prefix) name of
    9.98 +      SOME suffix => member (op =) smts suffix andalso
    9.99 +                     SMT_Solver.is_remotely_available ctxt suffix
   9.100 +    | NONE => member (op =) smts name
   9.101 +  end
   9.102 +
   9.103 +fun is_prover_available ctxt name =
   9.104 +  let val thy = ProofContext.theory_of ctxt in
   9.105 +    is_smt_prover ctxt name orelse member (op =) (available_atps thy) name
   9.106 +  end
   9.107 +
   9.108 +fun is_prover_installed ctxt name =
   9.109 +  let val thy = ProofContext.theory_of ctxt in
   9.110 +    if is_smt_prover ctxt name then
   9.111 +      String.isPrefix remote_prefix name orelse
   9.112 +      SMT_Solver.is_locally_installed ctxt name
   9.113 +    else
   9.114 +      is_atp_installed thy name
   9.115 +  end
   9.116 +
   9.117 +fun available_smt_solvers ctxt =
   9.118 +  let val smts = SMT_Solver.available_solvers_of ctxt in
   9.119 +    smts @ map (prefix remote_prefix)
   9.120 +               (filter (SMT_Solver.is_remotely_available ctxt) smts)
   9.121 +  end
   9.122 +
   9.123 +fun default_max_relevant_for_prover ctxt name =
   9.124 +  let val thy = ProofContext.theory_of ctxt in
   9.125 +    if is_smt_prover ctxt name then
   9.126 +      SMT_Solver.default_max_relevant ctxt
   9.127 +          (perhaps (try (unprefix remote_prefix)) name)
   9.128 +    else
   9.129 +      #default_max_relevant (get_atp thy name)
   9.130 +  end
   9.131 +
   9.132 +(* These are typically simplified away by "Meson.presimplify". Equality is
   9.133 +   handled specially via "fequal". *)
   9.134 +val atp_irrelevant_consts =
   9.135 +  [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
   9.136 +   @{const_name HOL.eq}]
   9.137 +
   9.138 +fun is_built_in_const_for_prover ctxt name (s, T) args =
   9.139 +  if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args
   9.140 +  else member (op =) atp_irrelevant_consts s
   9.141 +
   9.142 +(* FUDGE *)
   9.143 +val atp_relevance_fudge =
   9.144 +  {worse_irrel_freq = 100.0,
   9.145 +   higher_order_irrel_weight = 1.05,
   9.146 +   abs_rel_weight = 0.5,
   9.147 +   abs_irrel_weight = 2.0,
   9.148 +   skolem_irrel_weight = 0.75,
   9.149 +   theory_const_rel_weight = 0.5,
   9.150 +   theory_const_irrel_weight = 0.25,
   9.151 +   intro_bonus = 0.15,
   9.152 +   elim_bonus = 0.15,
   9.153 +   simp_bonus = 0.15,
   9.154 +   local_bonus = 0.55,
   9.155 +   assum_bonus = 1.05,
   9.156 +   chained_bonus = 1.5,
   9.157 +   max_imperfect = 11.5,
   9.158 +   max_imperfect_exp = 1.0,
   9.159 +   threshold_divisor = 2.0,
   9.160 +   ridiculous_threshold = 0.1}
   9.161 +
   9.162 +(* FUDGE (FIXME) *)
   9.163 +val smt_relevance_fudge =
   9.164 +  {worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
   9.165 +   higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
   9.166 +   abs_rel_weight = #abs_rel_weight atp_relevance_fudge,
   9.167 +   abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,
   9.168 +   skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,
   9.169 +   theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,
   9.170 +   theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,
   9.171 +   intro_bonus = #intro_bonus atp_relevance_fudge,
   9.172 +   elim_bonus = #elim_bonus atp_relevance_fudge,
   9.173 +   simp_bonus = #simp_bonus atp_relevance_fudge,
   9.174 +   local_bonus = #local_bonus atp_relevance_fudge,
   9.175 +   assum_bonus = #assum_bonus atp_relevance_fudge,
   9.176 +   chained_bonus = #chained_bonus atp_relevance_fudge,
   9.177 +   max_imperfect = #max_imperfect atp_relevance_fudge,
   9.178 +   max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge,
   9.179 +   threshold_divisor = #threshold_divisor atp_relevance_fudge,
   9.180 +   ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
   9.181 +
   9.182 +fun relevance_fudge_for_prover ctxt name =
   9.183 +  if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
   9.184 +
   9.185 +fun available_provers ctxt =
   9.186 +  let
   9.187 +    val thy = ProofContext.theory_of ctxt
   9.188 +    val (remote_provers, local_provers) =
   9.189 +      sort_strings (available_atps thy) @
   9.190 +      sort_strings (available_smt_solvers ctxt)
   9.191 +      |> List.partition (String.isPrefix remote_prefix)
   9.192 +  in
   9.193 +    Output.urgent_message ("Available provers: " ^
   9.194 +                           commas (local_provers @ remote_provers) ^ ".")
   9.195 +  end
   9.196 +
   9.197 +fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
   9.198 +fun running_provers () = Async_Manager.running_threads das_Tool "provers"
   9.199 +val messages = Async_Manager.thread_messages das_Tool "prover"
   9.200 +
   9.201 +(** problems, results, ATPs, etc. **)
   9.202 +
   9.203 +type params =
   9.204 +  {blocking: bool,
   9.205 +   debug: bool,
   9.206 +   verbose: bool,
   9.207 +   overlord: bool,
   9.208 +   provers: string list,
   9.209 +   full_types: bool,
   9.210 +   explicit_apply: bool,
   9.211 +   relevance_thresholds: real * real,
   9.212 +   max_relevant: int option,
   9.213 +   isar_proof: bool,
   9.214 +   isar_shrink_factor: int,
   9.215 +   timeout: Time.time,
   9.216 +   expect: string}
   9.217 +
   9.218 +datatype fact =
   9.219 +  Untranslated of (string * locality) * thm |
   9.220 +  Translated of term * ((string * locality) * translated_formula) option
   9.221 +
   9.222 +type prover_problem =
   9.223 +  {state: Proof.state,
   9.224 +   goal: thm,
   9.225 +   subgoal: int,
   9.226 +   subgoal_count: int,
   9.227 +   facts: fact list}
   9.228 +
   9.229 +type prover_result =
   9.230 +  {outcome: failure option,
   9.231 +   message: string,
   9.232 +   used_facts: (string * locality) list,
   9.233 +   run_time_in_msecs: int option}
   9.234 +
   9.235 +type prover = params -> minimize_command -> prover_problem -> prover_result
   9.236 +
   9.237 +(* configuration attributes *)
   9.238 +
   9.239 +val (dest_dir, dest_dir_setup) =
   9.240 +  Attrib.config_string "sledgehammer_dest_dir" (K "")
   9.241 +  (* Empty string means create files in Isabelle's temporary files directory. *)
   9.242 +
   9.243 +val (problem_prefix, problem_prefix_setup) =
   9.244 +  Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
   9.245 +
   9.246 +val (measure_run_time, measure_run_time_setup) =
   9.247 +  Attrib.config_bool "sledgehammer_measure_run_time" (K false)
   9.248 +
   9.249 +fun with_path cleanup after f path =
   9.250 +  Exn.capture f path
   9.251 +  |> tap (fn _ => cleanup path)
   9.252 +  |> Exn.release
   9.253 +  |> tap (after path)
   9.254 +
   9.255 +fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
   9.256 +                       n goal =
   9.257 +  quote name ^
   9.258 +  (if verbose then
   9.259 +     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
   9.260 +   else
   9.261 +     "") ^
   9.262 +  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
   9.263 +  (if blocking then
   9.264 +     ""
   9.265 +   else
   9.266 +     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
   9.267 +
   9.268 +fun proof_banner auto =
   9.269 +  if auto then "Auto Sledgehammer found a proof" else "Try this command"
   9.270 +
   9.271 +(* generic TPTP-based ATPs *)
   9.272 +
   9.273 +fun dest_Untranslated (Untranslated p) = p
   9.274 +  | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
   9.275 +fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p
   9.276 +  | translated_fact _ (Translated p) = p
   9.277 +
   9.278 +fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
   9.279 +  | int_opt_add _ _ = NONE
   9.280 +
   9.281 +(* Important messages are important but not so important that users want to see
   9.282 +   them each time. *)
   9.283 +val important_message_keep_factor = 0.1
   9.284 +
   9.285 +fun run_atp auto atp_name
   9.286 +        {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
   9.287 +         known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
   9.288 +        ({debug, verbose, overlord, full_types, explicit_apply, isar_proof,
   9.289 +          isar_shrink_factor, timeout, ...} : params)
   9.290 +        minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   9.291 +  let
   9.292 +    val ctxt = Proof.context_of state
   9.293 +    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
   9.294 +    val facts =
   9.295 +      facts |> map (translated_fact ctxt)
   9.296 +    val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   9.297 +                   else Config.get ctxt dest_dir
   9.298 +    val problem_prefix = Config.get ctxt problem_prefix
   9.299 +    val problem_file_name =
   9.300 +      Path.basic ((if overlord then "prob_" ^ atp_name
   9.301 +                   else problem_prefix ^ serial_string ())
   9.302 +                  ^ "_" ^ string_of_int subgoal)
   9.303 +    val problem_path_name =
   9.304 +      if dest_dir = "" then
   9.305 +        File.tmp_path problem_file_name
   9.306 +      else if File.exists (Path.explode dest_dir) then
   9.307 +        Path.append (Path.explode dest_dir) problem_file_name
   9.308 +      else
   9.309 +        error ("No such directory: " ^ quote dest_dir ^ ".")
   9.310 +    val measure_run_time = verbose orelse Config.get ctxt measure_run_time
   9.311 +    val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
   9.312 +    (* write out problem file and call ATP *)
   9.313 +    fun command_line complete timeout probfile =
   9.314 +      let
   9.315 +        val core = File.shell_path command ^ " " ^ arguments complete timeout ^
   9.316 +                   " " ^ File.shell_path probfile
   9.317 +      in
   9.318 +        (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
   9.319 +         else "exec " ^ core) ^ " 2>&1"
   9.320 +      end
   9.321 +    fun split_time s =
   9.322 +      let
   9.323 +        val split = String.tokens (fn c => str c = "\n");
   9.324 +        val (output, t) = s |> split |> split_last |> apfst cat_lines;
   9.325 +        fun as_num f = f >> (fst o read_int);
   9.326 +        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   9.327 +        val digit = Scan.one Symbol.is_ascii_digit;
   9.328 +        val num3 = as_num (digit ::: digit ::: (digit >> single));
   9.329 +        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   9.330 +        val as_time = Scan.read Symbol.stopper time o raw_explode
   9.331 +      in (output, as_time t) end;
   9.332 +    fun run_on probfile =
   9.333 +      case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
   9.334 +        (home_var, _) :: _ =>
   9.335 +        error ("The environment variable " ^ quote home_var ^ " is not set.")
   9.336 +      | [] =>
   9.337 +        if File.exists command then
   9.338 +          let
   9.339 +            fun run complete timeout =
   9.340 +              let
   9.341 +                val command = command_line complete timeout probfile
   9.342 +                val ((output, msecs), res_code) =
   9.343 +                  bash_output command
   9.344 +                  |>> (if overlord then
   9.345 +                         prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   9.346 +                       else
   9.347 +                         I)
   9.348 +                  |>> (if measure_run_time then split_time else rpair NONE)
   9.349 +                val (tstplike_proof, outcome) =
   9.350 +                  extract_tstplike_proof_and_outcome complete res_code
   9.351 +                      proof_delims known_failures output
   9.352 +              in (output, msecs, tstplike_proof, outcome) end
   9.353 +            val readable_names = debug andalso overlord
   9.354 +            val (atp_problem, pool, conjecture_offset, fact_names) =
   9.355 +              prepare_atp_problem ctxt readable_names explicit_forall full_types
   9.356 +                                  explicit_apply hyp_ts concl_t facts
   9.357 +            val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
   9.358 +                                                  atp_problem
   9.359 +            val _ = File.write_list probfile ss
   9.360 +            val conjecture_shape =
   9.361 +              conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   9.362 +              |> map single
   9.363 +            val run_twice = has_incomplete_mode andalso not auto
   9.364 +            val timer = Timer.startRealTimer ()
   9.365 +            val result =
   9.366 +              run false (if run_twice then
   9.367 +                           Time.fromMilliseconds
   9.368 +                                         (2 * Time.toMilliseconds timeout div 3)
   9.369 +                         else
   9.370 +                           timeout)
   9.371 +              |> run_twice
   9.372 +                 ? (fn (_, msecs0, _, SOME _) =>
   9.373 +                       run true (Time.- (timeout, Timer.checkRealTimer timer))
   9.374 +                       |> (fn (output, msecs, tstplike_proof, outcome) =>
   9.375 +                              (output, int_opt_add msecs0 msecs, tstplike_proof,
   9.376 +                               outcome))
   9.377 +                     | result => result)
   9.378 +          in ((pool, conjecture_shape, fact_names), result) end
   9.379 +        else
   9.380 +          error ("Bad executable: " ^ Path.implode command ^ ".")
   9.381 +
   9.382 +    (* If the problem file has not been exported, remove it; otherwise, export
   9.383 +       the proof file too. *)
   9.384 +    fun cleanup probfile =
   9.385 +      if dest_dir = "" then try File.rm probfile else NONE
   9.386 +    fun export probfile (_, (output, _, _, _)) =
   9.387 +      if dest_dir = "" then
   9.388 +        ()
   9.389 +      else
   9.390 +        File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   9.391 +    val ((pool, conjecture_shape, fact_names),
   9.392 +         (output, msecs, tstplike_proof, outcome)) =
   9.393 +      with_path cleanup export run_on problem_path_name
   9.394 +    val (conjecture_shape, fact_names) =
   9.395 +      repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
   9.396 +    val important_message =
   9.397 +      if not auto andalso random () <= important_message_keep_factor then
   9.398 +        extract_important_message output
   9.399 +      else
   9.400 +        ""
   9.401 +    val (message, used_facts) =
   9.402 +      case outcome of
   9.403 +        NONE =>
   9.404 +        proof_text isar_proof
   9.405 +            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   9.406 +            (proof_banner auto, full_types, minimize_command, tstplike_proof,
   9.407 +             fact_names, goal, subgoal)
   9.408 +        |>> (fn message =>
   9.409 +                message ^
   9.410 +                (if verbose then
   9.411 +                   "\nATP real CPU time: " ^
   9.412 +                   string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
   9.413 +                 else
   9.414 +                   "") ^
   9.415 +                (if important_message <> "" then
   9.416 +                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
   9.417 +                   important_message
   9.418 +                 else
   9.419 +                   ""))
   9.420 +      | SOME failure => (string_for_failure "ATP" failure, [])
   9.421 +  in
   9.422 +    {outcome = outcome, message = message, used_facts = used_facts,
   9.423 +     run_time_in_msecs = msecs}
   9.424 +  end
   9.425 +
   9.426 +(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
   9.427 +   these are sorted out properly in the SMT module, we have to interpret these
   9.428 +   ourselves. *)
   9.429 +val remote_smt_failures =
   9.430 +  [(22, CantConnect),
   9.431 +   (127, NoPerl),
   9.432 +   (2, NoLibwwwPerl)]
   9.433 +val z3_failures =
   9.434 +  [(103, MalformedInput),
   9.435 +   (110, MalformedInput)]
   9.436 +val unix_failures =
   9.437 +  [(139, Crashed)]
   9.438 +val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
   9.439 +
   9.440 +fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
   9.441 +  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   9.442 +  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
   9.443 +    (case AList.lookup (op =) smt_failures code of
   9.444 +       SOME failure => failure
   9.445 +     | NONE => UnknownError)
   9.446 +  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   9.447 +  | failure_from_smt_failure _ = UnknownError
   9.448 +
   9.449 +(* FUDGE *)
   9.450 +val smt_max_iter = 8
   9.451 +val smt_iter_fact_divisor = 2
   9.452 +val smt_iter_min_msecs = 5000
   9.453 +val smt_iter_timeout_divisor = 2
   9.454 +val smt_monomorph_limit = 4
   9.455 +
   9.456 +fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i =
   9.457 +  let
   9.458 +    val ctxt = Proof.context_of state
   9.459 +    fun iter timeout iter_num outcome0 msecs_so_far facts =
   9.460 +      let
   9.461 +        val timer = Timer.startRealTimer ()
   9.462 +        val ms = timeout |> Time.toMilliseconds
   9.463 +        val iter_timeout =
   9.464 +          if iter_num < smt_max_iter then
   9.465 +            Int.min (ms, Int.max (smt_iter_min_msecs,
   9.466 +                                  ms div smt_iter_timeout_divisor))
   9.467 +            |> Time.fromMilliseconds
   9.468 +          else
   9.469 +            timeout
   9.470 +        val num_facts = length facts
   9.471 +        val _ =
   9.472 +          if verbose then
   9.473 +            "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^
   9.474 +            plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..."
   9.475 +            |> Output.urgent_message
   9.476 +          else
   9.477 +            ()
   9.478 +        val {outcome, used_facts, run_time_in_msecs} =
   9.479 +          SMT_Solver.smt_filter remote iter_timeout state facts i
   9.480 +        val _ =
   9.481 +          if verbose andalso is_some outcome then
   9.482 +            "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
   9.483 +            |> Output.urgent_message
   9.484 +          else
   9.485 +            ()
   9.486 +        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   9.487 +        val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
   9.488 +        val too_many_facts_perhaps =
   9.489 +          case outcome of
   9.490 +            NONE => false
   9.491 +          | SOME (SMT_Failure.Counterexample _) => false
   9.492 +          | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
   9.493 +          | SOME (SMT_Failure.Abnormal_Termination code) =>
   9.494 +            (if verbose then
   9.495 +               "The SMT solver invoked with " ^ string_of_int num_facts ^
   9.496 +               " fact" ^ plural_s num_facts ^ " terminated abnormally with \
   9.497 +               \exit code " ^ string_of_int code ^ "."
   9.498 +               |> warning
   9.499 +             else
   9.500 +               ();
   9.501 +             true (* kind of *))
   9.502 +          | SOME SMT_Failure.Out_Of_Memory => true
   9.503 +          | SOME _ => true
   9.504 +        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   9.505 +      in
   9.506 +        if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso
   9.507 +           num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
   9.508 +          let val facts = take (num_facts div smt_iter_fact_divisor) facts in
   9.509 +            iter timeout (iter_num + 1) outcome0 msecs_so_far facts
   9.510 +          end
   9.511 +        else
   9.512 +          {outcome = if is_none outcome then NONE else the outcome0,
   9.513 +           used_facts = used_facts, run_time_in_msecs = msecs_so_far}
   9.514 +      end
   9.515 +  in iter timeout 1 NONE (SOME 0) end
   9.516 +
   9.517 +(* taken from "Mirabelle" and generalized *)
   9.518 +fun can_apply timeout tac state i =
   9.519 +  let
   9.520 +    val {context = ctxt, facts, goal} = Proof.goal state
   9.521 +    val full_tac = Method.insert_tac facts i THEN tac ctxt i
   9.522 +  in
   9.523 +    case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
   9.524 +      SOME (SOME _) => true
   9.525 +    | _ => false
   9.526 +  end
   9.527 +
   9.528 +val smt_metis_timeout = seconds 0.5
   9.529 +
   9.530 +fun can_apply_metis debug state i ths =
   9.531 +  can_apply smt_metis_timeout
   9.532 +            (Config.put Metis_Tactics.verbose debug
   9.533 +             #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
   9.534 +
   9.535 +fun run_smt_solver auto name (params as {debug, ...}) minimize_command
   9.536 +        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   9.537 +  let
   9.538 +    val (remote, suffix) =
   9.539 +      case try (unprefix remote_prefix) name of
   9.540 +        SOME suffix => (true, suffix)
   9.541 +      | NONE => (false, name)
   9.542 +    val repair_context =
   9.543 +      Context.proof_map (SMT_Config.select_solver suffix)
   9.544 +      #> Config.put SMT_Config.verbose debug
   9.545 +      #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
   9.546 +    val state = state |> Proof.map_context repair_context
   9.547 +    val thy = Proof.theory_of state
   9.548 +    val get_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
   9.549 +    val facts = facts |> map_filter get_fact
   9.550 +    val {outcome, used_facts, run_time_in_msecs} =
   9.551 +      smt_filter_loop params remote state subgoal facts
   9.552 +    val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
   9.553 +    val outcome = outcome |> Option.map failure_from_smt_failure
   9.554 +    val message =
   9.555 +      case outcome of
   9.556 +        NONE =>
   9.557 +        let
   9.558 +          val method =
   9.559 +            if can_apply_metis debug state subgoal (map snd used_facts) then
   9.560 +              "metis"
   9.561 +            else
   9.562 +              "smt"
   9.563 +        in
   9.564 +          try_command_line (proof_banner auto)
   9.565 +                           (apply_on_subgoal subgoal subgoal_count ^
   9.566 +                            command_call method (map fst other_lemmas)) ^
   9.567 +          minimize_line minimize_command
   9.568 +                        (map fst (other_lemmas @ chained_lemmas))
   9.569 +        end
   9.570 +      | SOME failure => string_for_failure "SMT solver" failure
   9.571 +  in
   9.572 +    {outcome = outcome, used_facts = map fst used_facts,
   9.573 +     run_time_in_msecs = run_time_in_msecs, message = message}
   9.574 +  end
   9.575 +
   9.576 +fun get_prover ctxt auto name =
   9.577 +  let val thy = ProofContext.theory_of ctxt in
   9.578 +    if is_smt_prover ctxt name then
   9.579 +      run_smt_solver auto name
   9.580 +    else if member (op =) (available_atps thy) name then
   9.581 +      run_atp auto name (get_atp thy name)
   9.582 +    else
   9.583 +      error ("No such prover: " ^ name ^ ".")
   9.584 +  end
   9.585 +
   9.586 +fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
   9.587 +               auto minimize_command only
   9.588 +               {state, goal, subgoal, subgoal_count, facts} name =
   9.589 +  let
   9.590 +    val ctxt = Proof.context_of state
   9.591 +    val birth_time = Time.now ()
   9.592 +    val death_time = Time.+ (birth_time, timeout)
   9.593 +    val max_relevant =
   9.594 +      the_default (default_max_relevant_for_prover ctxt name) max_relevant
   9.595 +    val num_facts = length facts |> not only ? Integer.min max_relevant
   9.596 +    val desc =
   9.597 +      prover_description ctxt params name num_facts subgoal subgoal_count goal
   9.598 +    val prover = get_prover ctxt auto name
   9.599 +    val problem =
   9.600 +      {state = state, goal = goal, subgoal = subgoal,
   9.601 +       subgoal_count = subgoal_count, facts = take num_facts facts}
   9.602 +    fun go () =
   9.603 +      let
   9.604 +        fun really_go () =
   9.605 +          prover params (minimize_command name) problem
   9.606 +          |> (fn {outcome, message, ...} =>
   9.607 +                 (if is_some outcome then "none" else "some", message))
   9.608 +        val (outcome_code, message) =
   9.609 +          if debug then
   9.610 +            really_go ()
   9.611 +          else
   9.612 +            (really_go ()
   9.613 +             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
   9.614 +                  | exn =>
   9.615 +                    if Exn.is_interrupt exn then
   9.616 +                      reraise exn
   9.617 +                    else
   9.618 +                      ("unknown", "Internal error:\n" ^
   9.619 +                                  ML_Compiler.exn_message exn ^ "\n"))
   9.620 +        val _ =
   9.621 +          if expect = "" orelse outcome_code = expect then
   9.622 +            ()
   9.623 +          else if blocking then
   9.624 +            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
   9.625 +          else
   9.626 +            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
   9.627 +      in (outcome_code = "some", message) end
   9.628 +  in
   9.629 +    if auto then
   9.630 +      let val (success, message) = TimeLimit.timeLimit timeout go () in
   9.631 +        (success, state |> success ? Proof.goal_message (fn () =>
   9.632 +             Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
   9.633 +                 (Pretty.str message)]))
   9.634 +      end
   9.635 +    else if blocking then
   9.636 +      let val (success, message) = TimeLimit.timeLimit timeout go () in
   9.637 +        List.app Output.urgent_message
   9.638 +                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
   9.639 +        (success, state)
   9.640 +      end
   9.641 +    else
   9.642 +      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
   9.643 +       (false, state))
   9.644 +  end
   9.645 +
   9.646 +val setup =
   9.647 +  dest_dir_setup
   9.648 +  #> problem_prefix_setup
   9.649 +  #> measure_run_time_setup
   9.650 +
   9.651 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 08 22:17:52 2010 +0100
    10.3 @@ -0,0 +1,112 @@
    10.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_run.ML
    10.5 +    Author:     Fabian Immler, TU Muenchen
    10.6 +    Author:     Makarius
    10.7 +    Author:     Jasmin Blanchette, TU Muenchen
    10.8 +
    10.9 +Sledgehammer's heart.
   10.10 +*)
   10.11 +
   10.12 +signature SLEDGEHAMMER_RUN =
   10.13 +sig
   10.14 +  type relevance_override = Sledgehammer_Filter.relevance_override
   10.15 +  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
   10.16 +  type params = Sledgehammer_Provers.params
   10.17 +
   10.18 +  val run_sledgehammer :
   10.19 +    params -> bool -> int -> relevance_override -> (string -> minimize_command)
   10.20 +    -> Proof.state -> bool * Proof.state
   10.21 +end;
   10.22 +
   10.23 +structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
   10.24 +struct
   10.25 +
   10.26 +open Sledgehammer_Util
   10.27 +open Sledgehammer_Filter
   10.28 +open Sledgehammer_ATP_Translate
   10.29 +open Sledgehammer_Provers
   10.30 +
   10.31 +(* FUDGE *)
   10.32 +val auto_max_relevant_divisor = 2
   10.33 +
   10.34 +fun fact_name (Untranslated ((name, _), _)) = SOME name
   10.35 +  | fact_name (Translated (_, p)) = Option.map (fst o fst) p
   10.36 +
   10.37 +fun run_sledgehammer (params as {blocking, debug, provers, full_types,
   10.38 +                                 relevance_thresholds, max_relevant, ...})
   10.39 +                     auto i (relevance_override as {only, ...}) minimize_command
   10.40 +                     state =
   10.41 +  if null provers then
   10.42 +    error "No prover is set."
   10.43 +  else case subgoal_count state of
   10.44 +    0 => (Output.urgent_message "No subgoal!"; (false, state))
   10.45 +  | n =>
   10.46 +    let
   10.47 +      val _ = Proof.assert_backward state
   10.48 +      val ctxt = Proof.context_of state
   10.49 +      val {facts = chained_ths, goal, ...} = Proof.goal state
   10.50 +      val (_, hyp_ts, concl_t) = strip_subgoal goal i
   10.51 +      val _ = () |> not blocking ? kill_provers
   10.52 +      val _ = case find_first (not o is_prover_available ctxt) provers of
   10.53 +                SOME name => error ("No such prover: " ^ name ^ ".")
   10.54 +              | NONE => ()
   10.55 +      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
   10.56 +      val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
   10.57 +      fun run_provers label full_types relevance_fudge maybe_translate provers
   10.58 +                      (res as (success, state)) =
   10.59 +        if success orelse null provers then
   10.60 +          res
   10.61 +        else
   10.62 +          let
   10.63 +            val max_max_relevant =
   10.64 +              case max_relevant of
   10.65 +                SOME n => n
   10.66 +              | NONE =>
   10.67 +                0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
   10.68 +                          provers
   10.69 +                  |> auto ? (fn n => n div auto_max_relevant_divisor)
   10.70 +            val is_built_in_const =
   10.71 +              is_built_in_const_for_prover ctxt (hd provers)
   10.72 +            val facts =
   10.73 +              relevant_facts ctxt full_types relevance_thresholds
   10.74 +                             max_max_relevant is_built_in_const relevance_fudge
   10.75 +                             relevance_override chained_ths hyp_ts concl_t
   10.76 +              |> map maybe_translate
   10.77 +            val problem =
   10.78 +              {state = state, goal = goal, subgoal = i, subgoal_count = n,
   10.79 +               facts = facts}
   10.80 +            val run_prover = run_prover params auto minimize_command only
   10.81 +          in
   10.82 +            if debug then
   10.83 +              Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
   10.84 +                  (if null facts then
   10.85 +                     "Found no relevant facts."
   10.86 +                   else
   10.87 +                     "Including (up to) " ^ string_of_int (length facts) ^
   10.88 +                     " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
   10.89 +                     (facts |> map_filter fact_name
   10.90 +                            |> space_implode " ") ^ "."))
   10.91 +            else
   10.92 +              ();
   10.93 +            if auto then
   10.94 +              fold (fn prover => fn (true, state) => (true, state)
   10.95 +                                  | (false, _) => run_prover problem prover)
   10.96 +                   provers (false, state)
   10.97 +            else
   10.98 +              provers |> (if blocking then Par_List.map else map)
   10.99 +                             (run_prover problem)
  10.100 +                      |> exists fst |> rpair state
  10.101 +          end
  10.102 +      val run_atps =
  10.103 +        run_provers "ATP" full_types atp_relevance_fudge
  10.104 +                    (Translated o translate_fact ctxt) atps
  10.105 +      val run_smts =
  10.106 +        run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
  10.107 +      fun run_atps_and_smt_solvers () =
  10.108 +        [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
  10.109 +    in
  10.110 +      (false, state)
  10.111 +      |> (if blocking then run_atps #> not auto ? run_smts
  10.112 +          else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
  10.113 +    end
  10.114 +
  10.115 +end;