renamed ML file
authorblanchet
Fri Jan 31 10:23:32 2014 +0100 (2014-01-31)
changeset 552011ee776da8da7
parent 55200 777328c9f1ea
child 55202 824c48a539c9
renamed ML file
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Sledgehammer.thy
src/HOL/TPTP/atp_problem_import.ML
src/HOL/TPTP/mash_eval.ML
src/HOL/TPTP/mash_export.ML
src/HOL/TPTP/sledgehammer_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 10:23:32 2014 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 10:23:32 2014 +0100
     1.3 @@ -376,7 +376,7 @@
     1.4    let
     1.5      val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (prop_of goal) all_facts
     1.6    in
     1.7 -    Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal
     1.8 +    Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal
     1.9        learn name
    1.10    end
    1.11  
    1.12 @@ -421,8 +421,8 @@
    1.13      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
    1.14      val i = 1
    1.15      fun set_file_name (SOME dir) =
    1.16 -        Config.put Sledgehammer_Provers.dest_dir dir
    1.17 -        #> Config.put Sledgehammer_Provers.problem_prefix
    1.18 +        Config.put Sledgehammer_Prover.dest_dir dir
    1.19 +        #> Config.put Sledgehammer_Prover.problem_prefix
    1.20            ("prob_" ^ str0 (Position.line_of pos) ^ "__")
    1.21          #> Config.put SMT_Config.debug_files
    1.22            (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
    1.23 @@ -453,9 +453,9 @@
    1.24            |> sh_minimizeLST (*don't confuse the two minimization flags*)
    1.25            |> max_new_mono_instancesLST
    1.26            |> max_mono_itersLST)
    1.27 -    val default_max_facts = Sledgehammer_Provers.default_max_facts_of_prover ctxt prover_name
    1.28 +    val default_max_facts = Sledgehammer_Prover.default_max_facts_of_prover ctxt prover_name
    1.29      val is_appropriate_prop =
    1.30 -      Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt prover_name
    1.31 +      Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt prover_name
    1.32      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
    1.33      val time_limit =
    1.34        (case hard_timeout of
    1.35 @@ -464,16 +464,16 @@
    1.36      fun failed failure =
    1.37        ({outcome = SOME failure, used_facts = [], used_from = [],
    1.38          run_time = Time.zeroTime,
    1.39 -        preplay = Lazy.value (Sledgehammer_Provers.plain_metis,
    1.40 +        preplay = Lazy.value (Sledgehammer_Prover.plain_metis,
    1.41            Sledgehammer_Reconstructor.Play_Failed),
    1.42          message = K "", message_tail = ""}, ~1)
    1.43      val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
    1.44 -         : Sledgehammer_Provers.prover_result,
    1.45 +         : Sledgehammer_Prover.prover_result,
    1.46           time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
    1.47        let
    1.48          val _ = if is_appropriate_prop concl_t then ()
    1.49                  else raise Fail "inappropriate"
    1.50 -        val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
    1.51 +        val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover_name
    1.52          val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
    1.53          val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.54          val facts =
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 10:23:32 2014 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 10:23:32 2014 +0100
     2.3 @@ -113,14 +113,14 @@
     2.4           val prover = AList.lookup (op =) args "prover" |> the_default default_prover
     2.5           val params as {max_facts, ...} =
     2.6             Sledgehammer_Commands.default_params ctxt args
     2.7 -         val default_max_facts = Sledgehammer_Provers.default_max_facts_of_prover ctxt prover
     2.8 +         val default_max_facts = Sledgehammer_Prover.default_max_facts_of_prover ctxt prover
     2.9           val is_appropriate_prop =
    2.10 -           Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt default_prover
    2.11 +           Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt default_prover
    2.12           val relevance_fudge =
    2.13             extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge
    2.14           val subgoal = 1
    2.15           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt
    2.16 -         val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
    2.17 +         val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
    2.18           val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
    2.19           val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    2.20           val facts =
     3.1 --- a/src/HOL/Sledgehammer.thy	Fri Jan 31 10:23:32 2014 +0100
     3.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jan 31 10:23:32 2014 +0100
     3.3 @@ -26,7 +26,7 @@
     3.4  ML_file "Tools/Sledgehammer/sledgehammer_try0.ML"
     3.5  ML_file "Tools/Sledgehammer/sledgehammer_minimize_isar.ML"
     3.6  ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
     3.7 -ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
     3.8 +ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
     3.9  ML_file "Tools/Sledgehammer/sledgehammer_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/atp_problem_import.ML	Fri Jan 31 10:23:32 2014 +0100
     4.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 10:23:32 2014 +0100
     4.3 @@ -182,7 +182,7 @@
     4.4  fun atp_tac ctxt completeness override_params timeout prover =
     4.5    let
     4.6      val ctxt =
     4.7 -      ctxt |> Config.put Sledgehammer_Provers.completish (completeness > 0)
     4.8 +      ctxt |> Config.put Sledgehammer_Prover.completish (completeness > 0)
     4.9      fun ref_of th = (Facts.named (Thm.derivation_name th), [])
    4.10    in
    4.11      Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
     5.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 10:23:32 2014 +0100
     5.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 10:23:32 2014 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  signature MASH_EVAL =
     5.6  sig
     5.7 -  type params = Sledgehammer_Provers.params
     5.8 +  type params = Sledgehammer_Prover.params
     5.9  
    5.10    val MePoN : string
    5.11    val MaSh_IsarN : string
    5.12 @@ -28,7 +28,7 @@
    5.13  open Sledgehammer_Fact
    5.14  open Sledgehammer_MePo
    5.15  open Sledgehammer_MaSh
    5.16 -open Sledgehammer_Provers
    5.17 +open Sledgehammer_Prover
    5.18  open Sledgehammer_Commands
    5.19  
    5.20  val prefix = Library.prefix
     6.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jan 31 10:23:32 2014 +0100
     6.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jan 31 10:23:32 2014 +0100
     6.3 @@ -7,7 +7,7 @@
     6.4  
     6.5  signature MASH_EXPORT =
     6.6  sig
     6.7 -  type params = Sledgehammer_Provers.params
     6.8 +  type params = Sledgehammer_Prover.params
     6.9  
    6.10    val generate_accessibility :
    6.11      Proof.context -> theory list -> bool -> string -> unit
    6.12 @@ -148,7 +148,7 @@
    6.13  fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
    6.14                                       linearize max_suggs file_name =
    6.15    let
    6.16 -    val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
    6.17 +    val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
    6.18      val path = file_name |> Path.explode
    6.19      val facts = all_facts ctxt
    6.20      val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
    6.21 @@ -229,7 +229,7 @@
    6.22  fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
    6.23                                (range, step) thys linearize max_suggs file_name =
    6.24    let
    6.25 -    val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
    6.26 +    val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
    6.27      val path = file_name |> Path.explode
    6.28      val facts = all_facts ctxt
    6.29      val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
     7.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 10:23:32 2014 +0100
     7.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 10:23:32 2014 +0100
     7.3 @@ -20,7 +20,7 @@
     7.4  
     7.5  open Sledgehammer_Util
     7.6  open Sledgehammer_Fact
     7.7 -open Sledgehammer_Provers
     7.8 +open Sledgehammer_Prover
     7.9  open Sledgehammer_MaSh
    7.10  open Sledgehammer_Commands
    7.11  
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Jan 31 10:23:32 2014 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Jan 31 10:23:32 2014 +0100
     8.3 @@ -6,7 +6,7 @@
     8.4  
     8.5  signature SLEDGEHAMMER_COMMANDS =
     8.6  sig
     8.7 -  type params = Sledgehammer_Provers.params
     8.8 +  type params = Sledgehammer_Prover.params
     8.9  
    8.10    val provers : string Unsynchronized.ref
    8.11    val default_params : Proof.context -> (string * string) list -> params
    8.12 @@ -21,7 +21,7 @@
    8.13  open ATP_Proof_Reconstruct
    8.14  open Sledgehammer_Util
    8.15  open Sledgehammer_Fact
    8.16 -open Sledgehammer_Provers
    8.17 +open Sledgehammer_Prover
    8.18  open Sledgehammer_Minimize
    8.19  open Sledgehammer_MaSh
    8.20  open Sledgehammer_Run
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 31 10:23:32 2014 +0100
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 31 10:23:32 2014 +0100
     9.3 @@ -10,8 +10,8 @@
     9.4    type raw_fact = Sledgehammer_Fact.raw_fact
     9.5    type fact = Sledgehammer_Fact.fact
     9.6    type fact_override = Sledgehammer_Fact.fact_override
     9.7 -  type params = Sledgehammer_Provers.params
     9.8 -  type prover_result = Sledgehammer_Provers.prover_result
     9.9 +  type params = Sledgehammer_Prover.params
    9.10 +  type prover_result = Sledgehammer_Prover.prover_result
    9.11  
    9.12    val trace : bool Config.T
    9.13    val MePoN : string
    9.14 @@ -106,7 +106,7 @@
    9.15  open ATP_Problem_Generate
    9.16  open Sledgehammer_Util
    9.17  open Sledgehammer_Fact
    9.18 -open Sledgehammer_Provers
    9.19 +open Sledgehammer_Prover
    9.20  open Sledgehammer_Minimize
    9.21  open Sledgehammer_MePo
    9.22  
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jan 31 10:23:32 2014 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jan 31 10:23:32 2014 +0100
    10.3 @@ -10,7 +10,7 @@
    10.4    type stature = ATP_Problem_Generate.stature
    10.5    type raw_fact = Sledgehammer_Fact.raw_fact
    10.6    type fact = Sledgehammer_Fact.fact
    10.7 -  type params = Sledgehammer_Provers.params
    10.8 +  type params = Sledgehammer_Prover.params
    10.9  
   10.10    type relevance_fudge =
   10.11      {local_const_multiplier : real,
   10.12 @@ -46,7 +46,7 @@
   10.13  open ATP_Problem_Generate
   10.14  open Sledgehammer_Util
   10.15  open Sledgehammer_Fact
   10.16 -open Sledgehammer_Provers
   10.17 +open Sledgehammer_Prover
   10.18  
   10.19  val trace =
   10.20    Attrib.setup_config_bool @{binding sledgehammer_mepo_trace} (K false)
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jan 31 10:23:32 2014 +0100
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jan 31 10:23:32 2014 +0100
    11.3 @@ -10,9 +10,9 @@
    11.4    type stature = ATP_Problem_Generate.stature
    11.5    type reconstructor = Sledgehammer_Reconstructor.reconstructor
    11.6    type play_outcome = Sledgehammer_Reconstructor.play_outcome
    11.7 -  type mode = Sledgehammer_Provers.mode
    11.8 -  type params = Sledgehammer_Provers.params
    11.9 -  type prover = Sledgehammer_Provers.prover
   11.10 +  type mode = Sledgehammer_Prover.mode
   11.11 +  type params = Sledgehammer_Prover.params
   11.12 +  type prover = Sledgehammer_Prover.prover
   11.13  
   11.14    val binary_min_facts : int Config.T
   11.15    val auto_minimize_min_facts : int Config.T
   11.16 @@ -39,7 +39,7 @@
   11.17  open Sledgehammer_Fact
   11.18  open Sledgehammer_Reconstructor
   11.19  open Sledgehammer_Reconstruct
   11.20 -open Sledgehammer_Provers
   11.21 +open Sledgehammer_Prover
   11.22  
   11.23  (* wrapper for calling external prover *)
   11.24  
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 10:23:32 2014 +0100
    12.3 @@ -0,0 +1,1063 @@
    12.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover.ML
    12.5 +    Author:     Fabian Immler, TU Muenchen
    12.6 +    Author:     Makarius
    12.7 +    Author:     Jasmin Blanchette, TU Muenchen
    12.8 +
    12.9 +Generic prover abstraction for Sledgehammer.
   12.10 +*)
   12.11 +
   12.12 +signature SLEDGEHAMMER_PROVER =
   12.13 +sig
   12.14 +  type atp_failure = ATP_Proof.atp_failure
   12.15 +  type stature = ATP_Problem_Generate.stature
   12.16 +  type type_enc = ATP_Problem_Generate.type_enc
   12.17 +  type fact = Sledgehammer_Fact.fact
   12.18 +  type reconstructor = Sledgehammer_Reconstructor.reconstructor
   12.19 +  type play_outcome = Sledgehammer_Reconstructor.play_outcome
   12.20 +  type minimize_command = Sledgehammer_Reconstructor.minimize_command
   12.21 +
   12.22 +  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
   12.23 +
   12.24 +  type params =
   12.25 +    {debug : bool,
   12.26 +     verbose : bool,
   12.27 +     overlord : bool,
   12.28 +     spy : bool,
   12.29 +     blocking : bool,
   12.30 +     provers : string list,
   12.31 +     type_enc : string option,
   12.32 +     strict : bool,
   12.33 +     lam_trans : string option,
   12.34 +     uncurried_aliases : bool option,
   12.35 +     learn : bool,
   12.36 +     fact_filter : string option,
   12.37 +     max_facts : int option,
   12.38 +     fact_thresholds : real * real,
   12.39 +     max_mono_iters : int option,
   12.40 +     max_new_mono_instances : int option,
   12.41 +     isar_proofs : bool option,
   12.42 +     compress_isar : real,
   12.43 +     try0_isar : bool,
   12.44 +     slice : bool,
   12.45 +     minimize : bool option,
   12.46 +     timeout : Time.time,
   12.47 +     preplay_timeout : Time.time,
   12.48 +     expect : string}
   12.49 +
   12.50 +  type prover_problem =
   12.51 +    {comment : string,
   12.52 +     state : Proof.state,
   12.53 +     goal : thm,
   12.54 +     subgoal : int,
   12.55 +     subgoal_count : int,
   12.56 +     factss : (string * fact list) list}
   12.57 +
   12.58 +  type prover_result =
   12.59 +    {outcome : atp_failure option,
   12.60 +     used_facts : (string * stature) list,
   12.61 +     used_from : fact list,
   12.62 +     run_time : Time.time,
   12.63 +     preplay : (reconstructor * play_outcome) Lazy.lazy,
   12.64 +     message : reconstructor * play_outcome -> string,
   12.65 +     message_tail : string}
   12.66 +
   12.67 +  type prover =
   12.68 +    params -> ((string * string list) list -> string -> minimize_command)
   12.69 +    -> prover_problem -> prover_result
   12.70 +
   12.71 +  val dest_dir : string Config.T
   12.72 +  val problem_prefix : string Config.T
   12.73 +  val completish : bool Config.T
   12.74 +  val atp_full_names : bool Config.T
   12.75 +  val smt_builtins : bool Config.T
   12.76 +  val smt_triggers : bool Config.T
   12.77 +  val smt_weights : bool Config.T
   12.78 +  val smt_weight_min_facts : int Config.T
   12.79 +  val smt_min_weight : int Config.T
   12.80 +  val smt_max_weight : int Config.T
   12.81 +  val smt_max_weight_index : int Config.T
   12.82 +  val smt_weight_curve : (int -> int) Unsynchronized.ref
   12.83 +  val smt_max_slices : int Config.T
   12.84 +  val smt_slice_fact_frac : real Config.T
   12.85 +  val smt_slice_time_frac : real Config.T
   12.86 +  val smt_slice_min_secs : int Config.T
   12.87 +  val SledgehammerN : string
   12.88 +  val plain_metis : reconstructor
   12.89 +  val select_smt_solver : string -> Proof.context -> Proof.context
   12.90 +  val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
   12.91 +  val is_reconstructor : string -> bool
   12.92 +  val is_atp : theory -> string -> bool
   12.93 +  val is_smt_prover : Proof.context -> string -> bool
   12.94 +  val is_ho_atp: Proof.context -> string -> bool
   12.95 +  val is_unit_equational_atp : Proof.context -> string -> bool
   12.96 +  val is_prover_supported : Proof.context -> string -> bool
   12.97 +  val is_prover_installed : Proof.context -> string -> bool
   12.98 +  val remotify_prover_if_supported_and_not_already_remote :
   12.99 +    Proof.context -> string -> string option
  12.100 +  val remotify_prover_if_not_installed :
  12.101 +    Proof.context -> string -> string option
  12.102 +  val default_max_facts_of_prover : Proof.context -> string -> int
  12.103 +  val is_unit_equality : term -> bool
  12.104 +  val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
  12.105 +  val weight_smt_fact :
  12.106 +    Proof.context -> int -> ((string * stature) * thm) * int
  12.107 +    -> (string * stature) * (int option * thm)
  12.108 +  val supported_provers : Proof.context -> unit
  12.109 +  val kill_provers : unit -> unit
  12.110 +  val running_provers : unit -> unit
  12.111 +  val messages : int option -> unit
  12.112 +  val is_fact_chained : (('a * stature) * 'b) -> bool
  12.113 +  val filter_used_facts :
  12.114 +    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
  12.115 +    ((''a * stature) * 'b) list
  12.116 +  val isar_proof_reconstructor : Proof.context -> string -> string
  12.117 +  val get_prover : Proof.context -> mode -> string -> prover
  12.118 +end;
  12.119 +
  12.120 +structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
  12.121 +struct
  12.122 +
  12.123 +open ATP_Util
  12.124 +open ATP_Problem
  12.125 +open ATP_Proof
  12.126 +open ATP_Systems
  12.127 +open ATP_Problem_Generate
  12.128 +open ATP_Proof_Reconstruct
  12.129 +open Metis_Tactic
  12.130 +open Sledgehammer_Util
  12.131 +open Sledgehammer_Fact
  12.132 +open Sledgehammer_Reconstructor
  12.133 +open Sledgehammer_Print
  12.134 +open Sledgehammer_Reconstruct
  12.135 +
  12.136 +
  12.137 +(** The Sledgehammer **)
  12.138 +
  12.139 +(* Empty string means create files in Isabelle's temporary files directory. *)
  12.140 +val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
  12.141 +val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
  12.142 +val completish = Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
  12.143 +
  12.144 +(* In addition to being easier to read, readable names are often much shorter,
  12.145 +   especially if types are mangled in names. This makes a difference for some
  12.146 +   provers (e.g., E). For these reason, short names are enabled by default. *)
  12.147 +val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
  12.148 +
  12.149 +val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
  12.150 +val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
  12.151 +val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
  12.152 +val smt_weight_min_facts =
  12.153 +  Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
  12.154 +
  12.155 +datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
  12.156 +
  12.157 +(* Identifier that distinguishes Sledgehammer from other tools that could use
  12.158 +   "Async_Manager". *)
  12.159 +val SledgehammerN = "Sledgehammer"
  12.160 +
  12.161 +val reconstructor_names = [metisN, smtN]
  12.162 +val plain_metis = Metis (hd partial_type_encs, combsN)
  12.163 +val is_reconstructor = member (op =) reconstructor_names
  12.164 +
  12.165 +val is_atp = member (op =) o supported_atps
  12.166 +
  12.167 +val select_smt_solver = Context.proof_map o SMT_Config.select_solver
  12.168 +
  12.169 +fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
  12.170 +
  12.171 +fun is_atp_of_format is_format ctxt name =
  12.172 +  let val thy = Proof_Context.theory_of ctxt in
  12.173 +    case try (get_atp thy) name of
  12.174 +      SOME config =>
  12.175 +      exists (fn (_, ((_, format, _, _, _), _)) => is_format format)
  12.176 +             (#best_slices (config ()) ctxt)
  12.177 +    | NONE => false
  12.178 +  end
  12.179 +
  12.180 +val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ)
  12.181 +val is_ho_atp = is_atp_of_format is_format_higher_order
  12.182 +
  12.183 +fun is_prover_supported ctxt =
  12.184 +  let val thy = Proof_Context.theory_of ctxt in
  12.185 +    is_reconstructor orf is_atp thy orf is_smt_prover ctxt
  12.186 +  end
  12.187 +
  12.188 +fun is_prover_installed ctxt =
  12.189 +  is_reconstructor orf is_smt_prover ctxt orf
  12.190 +  is_atp_installed (Proof_Context.theory_of ctxt)
  12.191 +
  12.192 +fun remotify_prover_if_supported_and_not_already_remote ctxt name =
  12.193 +  if String.isPrefix remote_prefix name then
  12.194 +    SOME name
  12.195 +  else
  12.196 +    let val remote_name = remote_prefix ^ name in
  12.197 +      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
  12.198 +    end
  12.199 +
  12.200 +fun remotify_prover_if_not_installed ctxt name =
  12.201 +  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
  12.202 +    SOME name
  12.203 +  else
  12.204 +    remotify_prover_if_supported_and_not_already_remote ctxt name
  12.205 +
  12.206 +fun get_slices slice slices =
  12.207 +  (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
  12.208 +
  12.209 +val reconstructor_default_max_facts = 20
  12.210 +
  12.211 +fun slice_max_facts (_, ( ((max_facts, _), _, _, _, _), _)) = max_facts
  12.212 +
  12.213 +fun default_max_facts_of_prover ctxt name =
  12.214 +  let val thy = Proof_Context.theory_of ctxt in
  12.215 +    if is_reconstructor name then
  12.216 +      reconstructor_default_max_facts
  12.217 +    else if is_atp thy name then
  12.218 +      fold (Integer.max o slice_max_facts) (#best_slices (get_atp thy name ()) ctxt) 0
  12.219 +    else (* is_smt_prover ctxt name *)
  12.220 +      SMT_Solver.default_max_relevant ctxt name
  12.221 +  end
  12.222 +
  12.223 +fun is_if (@{const_name If}, _) = true
  12.224 +  | is_if _ = false
  12.225 +
  12.226 +(* Beware of "if and only if" (which is translated as such) and "If" (which is
  12.227 +   translated to conditional equations). *)
  12.228 +fun is_good_unit_equality T t u =
  12.229 +  T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u])
  12.230 +
  12.231 +fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t
  12.232 +  | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) =
  12.233 +    is_unit_equality t
  12.234 +  | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) =
  12.235 +    is_unit_equality t
  12.236 +  | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) =
  12.237 +    is_good_unit_equality T t u
  12.238 +  | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) =
  12.239 +    is_good_unit_equality T t u
  12.240 +  | is_unit_equality _ = false
  12.241 +
  12.242 +fun is_appropriate_prop_of_prover ctxt name =
  12.243 +  if is_unit_equational_atp ctxt name then is_unit_equality else K true
  12.244 +
  12.245 +fun supported_provers ctxt =
  12.246 +  let
  12.247 +    val thy = Proof_Context.theory_of ctxt
  12.248 +    val (remote_provers, local_provers) =
  12.249 +      reconstructor_names @
  12.250 +      sort_strings (supported_atps thy) @
  12.251 +      sort_strings (SMT_Solver.available_solvers_of ctxt)
  12.252 +      |> List.partition (String.isPrefix remote_prefix)
  12.253 +  in
  12.254 +    Output.urgent_message ("Supported provers: " ^
  12.255 +                           commas (local_provers @ remote_provers) ^ ".")
  12.256 +  end
  12.257 +
  12.258 +fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
  12.259 +fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
  12.260 +val messages = Async_Manager.thread_messages SledgehammerN "prover"
  12.261 +
  12.262 +
  12.263 +(** problems, results, ATPs, etc. **)
  12.264 +
  12.265 +type params =
  12.266 +  {debug : bool,
  12.267 +   verbose : bool,
  12.268 +   overlord : bool,
  12.269 +   spy : bool,
  12.270 +   blocking : bool,
  12.271 +   provers : string list,
  12.272 +   type_enc : string option,
  12.273 +   strict : bool,
  12.274 +   lam_trans : string option,
  12.275 +   uncurried_aliases : bool option,
  12.276 +   learn : bool,
  12.277 +   fact_filter : string option,
  12.278 +   max_facts : int option,
  12.279 +   fact_thresholds : real * real,
  12.280 +   max_mono_iters : int option,
  12.281 +   max_new_mono_instances : int option,
  12.282 +   isar_proofs : bool option,
  12.283 +   compress_isar : real,
  12.284 +   try0_isar : bool,
  12.285 +   slice : bool,
  12.286 +   minimize : bool option,
  12.287 +   timeout : Time.time,
  12.288 +   preplay_timeout : Time.time,
  12.289 +   expect : string}
  12.290 +
  12.291 +type prover_problem =
  12.292 +  {comment : string,
  12.293 +   state : Proof.state,
  12.294 +   goal : thm,
  12.295 +   subgoal : int,
  12.296 +   subgoal_count : int,
  12.297 +   factss : (string * fact list) list}
  12.298 +
  12.299 +type prover_result =
  12.300 +  {outcome : atp_failure option,
  12.301 +   used_facts : (string * stature) list,
  12.302 +   used_from : fact list,
  12.303 +   run_time : Time.time,
  12.304 +   preplay : (reconstructor * play_outcome) Lazy.lazy,
  12.305 +   message : reconstructor * play_outcome -> string,
  12.306 +   message_tail : string}
  12.307 +
  12.308 +type prover =
  12.309 +  params -> ((string * string list) list -> string -> minimize_command)
  12.310 +  -> prover_problem -> prover_result
  12.311 +
  12.312 +(* FUDGE *)
  12.313 +val smt_min_weight =
  12.314 +  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
  12.315 +val smt_max_weight =
  12.316 +  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
  12.317 +val smt_max_weight_index =
  12.318 +  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
  12.319 +val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
  12.320 +
  12.321 +fun smt_fact_weight ctxt j num_facts =
  12.322 +  if Config.get ctxt smt_weights andalso
  12.323 +     num_facts >= Config.get ctxt smt_weight_min_facts then
  12.324 +    let
  12.325 +      val min = Config.get ctxt smt_min_weight
  12.326 +      val max = Config.get ctxt smt_max_weight
  12.327 +      val max_index = Config.get ctxt smt_max_weight_index
  12.328 +      val curve = !smt_weight_curve
  12.329 +    in
  12.330 +      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
  12.331 +            div curve max_index)
  12.332 +    end
  12.333 +  else
  12.334 +    NONE
  12.335 +
  12.336 +fun weight_smt_fact ctxt num_facts ((info, th), j) =
  12.337 +  let val thy = Proof_Context.theory_of ctxt in
  12.338 +    (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
  12.339 +  end
  12.340 +
  12.341 +fun overlord_file_location_of_prover prover =
  12.342 +  (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
  12.343 +
  12.344 +fun proof_banner mode name =
  12.345 +  case mode of
  12.346 +    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
  12.347 +  | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
  12.348 +  | _ => "Try this"
  12.349 +
  12.350 +fun bunch_of_reconstructors needs_full_types lam_trans =
  12.351 +  if needs_full_types then
  12.352 +    [Metis (full_type_enc, lam_trans false),
  12.353 +     Metis (really_full_type_enc, lam_trans false),
  12.354 +     Metis (full_type_enc, lam_trans true),
  12.355 +     Metis (really_full_type_enc, lam_trans true),
  12.356 +     SMT]
  12.357 +  else
  12.358 +    [Metis (partial_type_enc, lam_trans false),
  12.359 +     Metis (full_type_enc, lam_trans false),
  12.360 +     Metis (no_typesN, lam_trans true),
  12.361 +     Metis (really_full_type_enc, lam_trans true),
  12.362 +     SMT]
  12.363 +
  12.364 +fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
  12.365 +    let
  12.366 +      val override_params =
  12.367 +        (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
  12.368 +         else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
  12.369 +        (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
  12.370 +         else [("lam_trans", [lam_trans'])])
  12.371 +    in (metisN, override_params) end
  12.372 +  | extract_reconstructor _ SMT = (smtN, [])
  12.373 +
  12.374 +(* based on "Mirabelle.can_apply" and generalized *)
  12.375 +fun timed_apply timeout tac state i =
  12.376 +  let
  12.377 +    val {context = ctxt, facts, goal} = Proof.goal state
  12.378 +    val full_tac = Method.insert_tac facts i THEN tac ctxt i
  12.379 +  in
  12.380 +    TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
  12.381 +  end
  12.382 +
  12.383 +fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
  12.384 +  | tac_of_reconstructor SMT = SMT_Solver.smt_tac
  12.385 +
  12.386 +fun timed_reconstructor reconstr debug timeout ths =
  12.387 +  timed_apply timeout (silence_reconstructors debug
  12.388 +    #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
  12.389 +
  12.390 +fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
  12.391 +
  12.392 +fun filter_used_facts keep_chained used =
  12.393 +  filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
  12.394 +
  12.395 +fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
  12.396 +  let
  12.397 +    fun get_preferred reconstrs =
  12.398 +      if member (op =) reconstrs preferred then preferred
  12.399 +      else List.last reconstrs
  12.400 +  in
  12.401 +    if timeout = Time.zeroTime then
  12.402 +      (get_preferred reconstrs, Not_Played)
  12.403 +    else
  12.404 +      let
  12.405 +        val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
  12.406 +        val ths = pairs |> sort_wrt (fst o fst) |> map snd
  12.407 +        fun play [] [] = (get_preferred reconstrs, Play_Failed)
  12.408 +          | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
  12.409 +          | play timed_out (reconstr :: reconstrs) =
  12.410 +            let
  12.411 +              val _ =
  12.412 +                if verbose then
  12.413 +                  Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
  12.414 +                    "\" for " ^ string_of_time timeout ^ "...")
  12.415 +                else
  12.416 +                  ()
  12.417 +              val timer = Timer.startRealTimer ()
  12.418 +            in
  12.419 +              case timed_reconstructor reconstr debug timeout ths state i of
  12.420 +                SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
  12.421 +              | _ => play timed_out reconstrs
  12.422 +            end
  12.423 +            handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
  12.424 +      in
  12.425 +        play [] reconstrs
  12.426 +      end
  12.427 +  end
  12.428 +
  12.429 +
  12.430 +(* generic TPTP-based ATPs *)
  12.431 +
  12.432 +(* Too general means, positive equality literal with a variable X as one
  12.433 +   operand, when X does not occur properly in the other operand. This rules out
  12.434 +   clearly inconsistent facts such as X = a | X = b, though it by no means
  12.435 +   guarantees soundness. *)
  12.436 +
  12.437 +fun get_facts_of_filter _ [(_, facts)] = facts
  12.438 +  | get_facts_of_filter fact_filter factss =
  12.439 +    case AList.lookup (op =) factss fact_filter of
  12.440 +      SOME facts => facts
  12.441 +    | NONE => snd (hd factss)
  12.442 +
  12.443 +(* Unwanted equalities are those between a (bound or schematic) variable that
  12.444 +   does not properly occur in the second operand. *)
  12.445 +val is_exhaustive_finite =
  12.446 +  let
  12.447 +    fun is_bad_equal (Var z) t =
  12.448 +        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
  12.449 +      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
  12.450 +      | is_bad_equal _ _ = false
  12.451 +    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
  12.452 +    fun do_formula pos t =
  12.453 +      case (pos, t) of
  12.454 +        (_, @{const Trueprop} $ t1) => do_formula pos t1
  12.455 +      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
  12.456 +        do_formula pos t'
  12.457 +      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
  12.458 +        do_formula pos t'
  12.459 +      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
  12.460 +        do_formula pos t'
  12.461 +      | (_, @{const "==>"} $ t1 $ t2) =>
  12.462 +        do_formula (not pos) t1 andalso
  12.463 +        (t2 = @{prop False} orelse do_formula pos t2)
  12.464 +      | (_, @{const HOL.implies} $ t1 $ t2) =>
  12.465 +        do_formula (not pos) t1 andalso
  12.466 +        (t2 = @{const False} orelse do_formula pos t2)
  12.467 +      | (_, @{const Not} $ t1) => do_formula (not pos) t1
  12.468 +      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
  12.469 +      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
  12.470 +      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
  12.471 +      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
  12.472 +      | _ => false
  12.473 +  in do_formula true end
  12.474 +
  12.475 +fun has_bound_or_var_of_type pred =
  12.476 +  exists_subterm (fn Var (_, T as Type _) => pred T
  12.477 +                   | Abs (_, T as Type _, _) => pred T
  12.478 +                   | _ => false)
  12.479 +
  12.480 +(* Facts are forbidden to contain variables of these types. The typical reason
  12.481 +   is that they lead to unsoundness. Note that "unit" satisfies numerous
  12.482 +   equations like "?x = ()". The resulting clauses will have no type constraint,
  12.483 +   yielding false proofs. Even "bool" leads to many unsound proofs, though only
  12.484 +   for higher-order problems. *)
  12.485 +
  12.486 +(* Facts containing variables of type "unit" or "bool" or of the form
  12.487 +   "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
  12.488 +   are omitted. *)
  12.489 +fun is_dangerous_prop ctxt =
  12.490 +  transform_elim_prop
  12.491 +  #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
  12.492 +      is_exhaustive_finite)
  12.493 +
  12.494 +(* Important messages are important but not so important that users want to see
  12.495 +   them each time. *)
  12.496 +val atp_important_message_keep_quotient = 25
  12.497 +
  12.498 +fun choose_type_enc strictness best_type_enc format =
  12.499 +  the_default best_type_enc
  12.500 +  #> type_enc_of_string strictness
  12.501 +  #> adjust_type_enc format
  12.502 +
  12.503 +fun isar_proof_reconstructor ctxt name =
  12.504 +  let val thy = Proof_Context.theory_of ctxt in
  12.505 +    if is_atp thy name then name
  12.506 +    else remotify_prover_if_not_installed ctxt eN |> the_default name
  12.507 +  end
  12.508 +
  12.509 +(* See the analogous logic in the function "maybe_minimize" in
  12.510 +  "sledgehammer_minimize.ML". *)
  12.511 +fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command name preplay =
  12.512 +  let
  12.513 +    val maybe_isar_name = name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
  12.514 +    val (min_name, override_params) =
  12.515 +      (case preplay of
  12.516 +        (reconstr, Played _) =>
  12.517 +        if isar_proofs = SOME true then (maybe_isar_name, [])
  12.518 +        else extract_reconstructor params reconstr
  12.519 +      | _ => (maybe_isar_name, []))
  12.520 +  in minimize_command override_params min_name end
  12.521 +
  12.522 +val max_fact_instances = 10 (* FUDGE *)
  12.523 +
  12.524 +fun repair_monomorph_context max_iters best_max_iters max_new_instances
  12.525 +                             best_max_new_instances =
  12.526 +  Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
  12.527 +  #> Config.put Monomorph.max_new_instances
  12.528 +         (max_new_instances |> the_default best_max_new_instances)
  12.529 +  #> Config.put Monomorph.max_thm_instances max_fact_instances
  12.530 +
  12.531 +fun suffix_of_mode Auto_Try = "_try"
  12.532 +  | suffix_of_mode Try = "_try"
  12.533 +  | suffix_of_mode Normal = ""
  12.534 +  | suffix_of_mode MaSh = ""
  12.535 +  | suffix_of_mode Auto_Minimize = "_min"
  12.536 +  | suffix_of_mode Minimize = "_min"
  12.537 +
  12.538 +(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
  12.539 +   Linux appears to be the only ATP that does not honor its time limit. *)
  12.540 +val atp_timeout_slack = seconds 1.0
  12.541 +
  12.542 +val mono_max_privileged_facts = 10
  12.543 +
  12.544 +(* For low values of "max_facts", this fudge value ensures that most slices are
  12.545 +   invoked with a nontrivial amount of facts. *)
  12.546 +val max_fact_factor_fudge = 5
  12.547 +
  12.548 +fun run_atp mode name
  12.549 +    ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
  12.550 +      best_max_new_mono_instances, ...} : atp_config)
  12.551 +    (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
  12.552 +       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
  12.553 +       try0_isar, slice, timeout, preplay_timeout, ...})
  12.554 +    minimize_command
  12.555 +    ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
  12.556 +  let
  12.557 +    val thy = Proof.theory_of state
  12.558 +    val ctxt = Proof.context_of state
  12.559 +    val atp_mode =
  12.560 +      if Config.get ctxt completish then Sledgehammer_Completish
  12.561 +      else Sledgehammer
  12.562 +    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
  12.563 +    val (dest_dir, problem_prefix) =
  12.564 +      if overlord then overlord_file_location_of_prover name
  12.565 +      else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
  12.566 +    val problem_file_name =
  12.567 +      Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
  12.568 +                  suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
  12.569 +    val prob_path =
  12.570 +      if dest_dir = "" then
  12.571 +        File.tmp_path problem_file_name
  12.572 +      else if File.exists (Path.explode dest_dir) then
  12.573 +        Path.append (Path.explode dest_dir) problem_file_name
  12.574 +      else
  12.575 +        error ("No such directory: " ^ quote dest_dir ^ ".")
  12.576 +    val exec = exec ()
  12.577 +    val command0 =
  12.578 +      case find_first (fn var => getenv var <> "") (fst exec) of
  12.579 +        SOME var =>
  12.580 +        let
  12.581 +          val pref = getenv var ^ "/"
  12.582 +          val paths = map (Path.explode o prefix pref) (snd exec)
  12.583 +        in
  12.584 +          case find_first File.exists paths of
  12.585 +            SOME path => path
  12.586 +          | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
  12.587 +        end
  12.588 +      | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^
  12.589 +                       " is not set.")
  12.590 +    fun split_time s =
  12.591 +      let
  12.592 +        val split = String.tokens (fn c => str c = "\n")
  12.593 +        val (output, t) =
  12.594 +          s |> split |> (try split_last #> the_default ([], "0"))
  12.595 +            |>> cat_lines
  12.596 +        fun as_num f = f >> (fst o read_int)
  12.597 +        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
  12.598 +        val digit = Scan.one Symbol.is_ascii_digit
  12.599 +        val num3 = as_num (digit ::: digit ::: (digit >> single))
  12.600 +        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
  12.601 +        val as_time =
  12.602 +          raw_explode #> Scan.read Symbol.stopper time #> the_default 0
  12.603 +      in (output, as_time t |> Time.fromMilliseconds) end
  12.604 +    fun run () =
  12.605 +      let
  12.606 +        (* If slicing is disabled, we expand the last slice to fill the entire
  12.607 +           time available. *)
  12.608 +        val all_slices = best_slices ctxt
  12.609 +        val actual_slices = get_slices slice all_slices
  12.610 +        fun max_facts_of_slices f slices = fold (Integer.max o slice_max_facts o f) slices 0
  12.611 +        val num_actual_slices = length actual_slices
  12.612 +        val max_fact_factor =
  12.613 +          Real.fromInt (case max_facts of
  12.614 +              NONE => max_facts_of_slices I all_slices
  12.615 +            | SOME max => max)
  12.616 +          / Real.fromInt (max_facts_of_slices snd actual_slices)
  12.617 +        fun monomorphize_facts facts =
  12.618 +          let
  12.619 +            val ctxt =
  12.620 +              ctxt
  12.621 +              |> repair_monomorph_context max_mono_iters
  12.622 +                     best_max_mono_iters max_new_mono_instances
  12.623 +                     best_max_new_mono_instances
  12.624 +            (* pseudo-theorem involving the same constants as the subgoal *)
  12.625 +            val subgoal_th =
  12.626 +              Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
  12.627 +            val rths =
  12.628 +              facts |> chop mono_max_privileged_facts
  12.629 +                    |>> map (pair 1 o snd)
  12.630 +                    ||> map (pair 2 o snd)
  12.631 +                    |> op @
  12.632 +                    |> cons (0, subgoal_th)
  12.633 +          in
  12.634 +            Monomorph.monomorph atp_schematic_consts_of ctxt rths
  12.635 +            |> tl |> curry ListPair.zip (map fst facts)
  12.636 +            |> maps (fn (name, rths) =>
  12.637 +                        map (pair name o zero_var_indexes o snd) rths)
  12.638 +          end
  12.639 +        fun run_slice time_left (cache_key, cache_value)
  12.640 +                (slice, (time_frac,
  12.641 +                     (key as ((best_max_facts, best_fact_filter), format,
  12.642 +                              best_type_enc, best_lam_trans,
  12.643 +                              best_uncurried_aliases),
  12.644 +                      extra))) =
  12.645 +          let
  12.646 +            val effective_fact_filter =
  12.647 +              fact_filter |> the_default best_fact_filter
  12.648 +            val facts = get_facts_of_filter effective_fact_filter factss
  12.649 +            val num_facts =
  12.650 +              Real.ceil (max_fact_factor * Real.fromInt best_max_facts) +
  12.651 +              max_fact_factor_fudge
  12.652 +              |> Integer.min (length facts)
  12.653 +            val strictness = if strict then Strict else Non_Strict
  12.654 +            val type_enc =
  12.655 +              type_enc |> choose_type_enc strictness best_type_enc format
  12.656 +            val sound = is_type_enc_sound type_enc
  12.657 +            val real_ms = Real.fromInt o Time.toMilliseconds
  12.658 +            val slice_timeout =
  12.659 +              (real_ms time_left
  12.660 +               |> (if slice < num_actual_slices - 1 then
  12.661 +                     curry Real.min (time_frac * real_ms timeout)
  12.662 +                   else
  12.663 +                     I))
  12.664 +              * 0.001
  12.665 +              |> seconds
  12.666 +            val generous_slice_timeout =
  12.667 +              if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
  12.668 +            val _ =
  12.669 +              if debug then
  12.670 +                quote name ^ " slice #" ^ string_of_int (slice + 1) ^
  12.671 +                " with " ^ string_of_int num_facts ^ " fact" ^
  12.672 +                plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
  12.673 +                |> Output.urgent_message
  12.674 +              else
  12.675 +                ()
  12.676 +            val readable_names = not (Config.get ctxt atp_full_names)
  12.677 +            val lam_trans =
  12.678 +              case lam_trans of
  12.679 +                SOME s => s
  12.680 +              | NONE => best_lam_trans
  12.681 +            val uncurried_aliases =
  12.682 +              case uncurried_aliases of
  12.683 +                SOME b => b
  12.684 +              | NONE => best_uncurried_aliases
  12.685 +            val value as (atp_problem, _, fact_names, _, _) =
  12.686 +              if cache_key = SOME key then
  12.687 +                cache_value
  12.688 +              else
  12.689 +                facts
  12.690 +                |> not sound
  12.691 +                   ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
  12.692 +                |> take num_facts
  12.693 +                |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
  12.694 +                |> map (apsnd prop_of)
  12.695 +                |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
  12.696 +                                       lam_trans uncurried_aliases
  12.697 +                                       readable_names true hyp_ts concl_t
  12.698 +            fun sel_weights () = atp_problem_selection_weights atp_problem
  12.699 +            fun ord_info () = atp_problem_term_order_info atp_problem
  12.700 +            val ord = effective_term_order ctxt name
  12.701 +            val full_proof = isar_proofs |> the_default (mode = Minimize)
  12.702 +            val args =
  12.703 +              arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
  12.704 +                (ord, ord_info, sel_weights)
  12.705 +            val command =
  12.706 +              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
  12.707 +              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
  12.708 +            val _ =
  12.709 +              atp_problem
  12.710 +              |> lines_of_atp_problem format ord ord_info
  12.711 +              |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
  12.712 +              |> File.write_list prob_path
  12.713 +            val ((output, run_time), (atp_proof, outcome)) =
  12.714 +              TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
  12.715 +              |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
  12.716 +              |> fst |> split_time
  12.717 +              |> (fn accum as (output, _) =>
  12.718 +                     (accum,
  12.719 +                      extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
  12.720 +                      |>> atp_proof_of_tstplike_proof atp_problem
  12.721 +                      handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
  12.722 +              handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
  12.723 +            val outcome =
  12.724 +              (case outcome of
  12.725 +                NONE =>
  12.726 +                (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
  12.727 +                      |> Option.map (sort string_ord) of
  12.728 +                   SOME facts =>
  12.729 +                   let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
  12.730 +                     if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
  12.731 +                   end
  12.732 +                 | NONE => NONE)
  12.733 +              | _ => outcome)
  12.734 +          in
  12.735 +            ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
  12.736 +          end
  12.737 +        val timer = Timer.startRealTimer ()
  12.738 +        fun maybe_run_slice slice
  12.739 +                (result as (cache, (_, run_time0, _, _, SOME _))) =
  12.740 +            let
  12.741 +              val time_left = Time.- (timeout, Timer.checkRealTimer timer)
  12.742 +            in
  12.743 +              if Time.<= (time_left, Time.zeroTime) then
  12.744 +                result
  12.745 +              else
  12.746 +                run_slice time_left cache slice
  12.747 +                |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) =>
  12.748 +                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome)))
  12.749 +            end
  12.750 +          | maybe_run_slice _ result = result
  12.751 +      in
  12.752 +        ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
  12.753 +         ("", Time.zeroTime, [], [], SOME InternalError))
  12.754 +        |> fold maybe_run_slice actual_slices
  12.755 +      end
  12.756 +    (* If the problem file has not been exported, remove it; otherwise, export
  12.757 +       the proof file too. *)
  12.758 +    fun clean_up () =
  12.759 +      if dest_dir = "" then (try File.rm prob_path; ()) else ()
  12.760 +    fun export (_, (output, _, _, _, _)) =
  12.761 +      if dest_dir = "" then ()
  12.762 +      else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
  12.763 +    val ((_, (_, pool, fact_names, lifted, sym_tab)),
  12.764 +         (output, run_time, used_from, atp_proof, outcome)) =
  12.765 +      with_cleanup clean_up run () |> tap export
  12.766 +    val important_message =
  12.767 +      if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0
  12.768 +      then
  12.769 +        extract_important_message output
  12.770 +      else
  12.771 +        ""
  12.772 +    val (used_facts, preplay, message, message_tail) =
  12.773 +      (case outcome of
  12.774 +        NONE =>
  12.775 +        let
  12.776 +          val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
  12.777 +          val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
  12.778 +          val reconstrs =
  12.779 +            bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof
  12.780 +              o (fn desperate => if desperate then hide_lamsN else default_metis_lam_trans))
  12.781 +        in
  12.782 +          (used_facts,
  12.783 +           Lazy.lazy (fn () =>
  12.784 +             let val used_pairs = used_from |> filter_used_facts false used_facts in
  12.785 +               play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
  12.786 +                 (hd reconstrs) reconstrs
  12.787 +             end),
  12.788 +           fn preplay =>
  12.789 +              let
  12.790 +                val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
  12.791 +                fun isar_params () =
  12.792 +                  let
  12.793 +                    val metis_type_enc =
  12.794 +                      if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
  12.795 +                      else partial_typesN
  12.796 +                    val metis_lam_trans = lam_trans_of_atp_proof atp_proof default_metis_lam_trans
  12.797 +                    val atp_proof =
  12.798 +                      atp_proof
  12.799 +                      |> termify_atp_proof ctxt pool lifted sym_tab
  12.800 +                      |> introduce_spass_skolem
  12.801 +                      |> factify_atp_proof fact_names hyp_ts concl_t
  12.802 +                  in
  12.803 +                    (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
  12.804 +                     try0_isar, atp_proof, goal)
  12.805 +                  end
  12.806 +                val one_line_params =
  12.807 +                  (preplay, proof_banner mode name, used_facts,
  12.808 +                   choose_minimize_command ctxt params minimize_command name preplay,
  12.809 +                   subgoal, subgoal_count)
  12.810 +                val num_chained = length (#facts (Proof.goal state))
  12.811 +              in
  12.812 +                proof_text ctxt debug isar_proofs isar_params num_chained one_line_params
  12.813 +              end,
  12.814 +           (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
  12.815 +           (if important_message <> "" then
  12.816 +              "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
  12.817 +            else
  12.818 +              ""))
  12.819 +        end
  12.820 +      | SOME failure =>
  12.821 +        ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
  12.822 +  in
  12.823 +    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
  12.824 +     preplay = preplay, message = message, message_tail = message_tail}
  12.825 +  end
  12.826 +
  12.827 +(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
  12.828 +   these are sorted out properly in the SMT module, we have to interpret these
  12.829 +   ourselves. *)
  12.830 +val remote_smt_failures =
  12.831 +  [(2, NoLibwwwPerl),
  12.832 +   (22, CantConnect)]
  12.833 +val z3_failures =
  12.834 +  [(101, OutOfResources),
  12.835 +   (103, MalformedInput),
  12.836 +   (110, MalformedInput),
  12.837 +   (112, TimedOut)]
  12.838 +val unix_failures =
  12.839 +  [(138, Crashed),
  12.840 +   (139, Crashed)]
  12.841 +val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
  12.842 +
  12.843 +fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
  12.844 +    if is_real_cex then Unprovable else GaveUp
  12.845 +  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
  12.846 +  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
  12.847 +    (case AList.lookup (op =) smt_failures code of
  12.848 +       SOME failure => failure
  12.849 +     | NONE => UnknownError ("Abnormal termination with exit code " ^
  12.850 +                             string_of_int code ^ "."))
  12.851 +  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
  12.852 +  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
  12.853 +
  12.854 +(* FUDGE *)
  12.855 +val smt_max_slices =
  12.856 +  Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
  12.857 +val smt_slice_fact_frac =
  12.858 +  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac}
  12.859 +                           (K 0.667)
  12.860 +val smt_slice_time_frac =
  12.861 +  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
  12.862 +val smt_slice_min_secs =
  12.863 +  Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
  12.864 +
  12.865 +val is_boring_builtin_typ =
  12.866 +  not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
  12.867 +
  12.868 +fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
  12.869 +      ...} : params) state goal i =
  12.870 +  let
  12.871 +    fun repair_context ctxt =
  12.872 +      ctxt |> select_smt_solver name
  12.873 +           |> Config.put SMT_Config.verbose debug
  12.874 +           |> (if overlord then
  12.875 +                 Config.put SMT_Config.debug_files
  12.876 +                            (overlord_file_location_of_prover name
  12.877 +                             |> (fn (path, name) => path ^ "/" ^ name))
  12.878 +               else
  12.879 +                 I)
  12.880 +           |> Config.put SMT_Config.infer_triggers
  12.881 +                         (Config.get ctxt smt_triggers)
  12.882 +           |> not (Config.get ctxt smt_builtins)
  12.883 +              ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
  12.884 +                 #> Config.put SMT_Config.datatypes false)
  12.885 +           |> repair_monomorph_context max_mono_iters default_max_mono_iters
  12.886 +                  max_new_mono_instances default_max_new_mono_instances
  12.887 +    val state = Proof.map_context (repair_context) state
  12.888 +    val ctxt = Proof.context_of state
  12.889 +    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
  12.890 +    fun do_slice timeout slice outcome0 time_so_far
  12.891 +                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
  12.892 +      let
  12.893 +        val timer = Timer.startRealTimer ()
  12.894 +        val slice_timeout =
  12.895 +          if slice < max_slices then
  12.896 +            let val ms = Time.toMilliseconds timeout in
  12.897 +              Int.min (ms,
  12.898 +                  Int.max (1000 * Config.get ctxt smt_slice_min_secs,
  12.899 +                      Real.ceil (Config.get ctxt smt_slice_time_frac
  12.900 +                                 * Real.fromInt ms)))
  12.901 +              |> Time.fromMilliseconds
  12.902 +            end
  12.903 +          else
  12.904 +            timeout
  12.905 +        val num_facts = length weighted_facts
  12.906 +        val _ =
  12.907 +          if debug then
  12.908 +            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
  12.909 +            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
  12.910 +            |> Output.urgent_message
  12.911 +          else
  12.912 +            ()
  12.913 +        val birth = Timer.checkRealTimer timer
  12.914 +        val _ =
  12.915 +          if debug then Output.urgent_message "Invoking SMT solver..." else ()
  12.916 +        val (outcome, used_facts) =
  12.917 +          SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
  12.918 +          |> SMT_Solver.smt_filter_apply slice_timeout
  12.919 +          |> (fn {outcome, used_facts} => (outcome, used_facts))
  12.920 +          handle exn => if Exn.is_interrupt exn then
  12.921 +                          reraise exn
  12.922 +                        else
  12.923 +                          (ML_Compiler.exn_message exn
  12.924 +                           |> SMT_Failure.Other_Failure |> SOME, [])
  12.925 +        val death = Timer.checkRealTimer timer
  12.926 +        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
  12.927 +        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
  12.928 +        val too_many_facts_perhaps =
  12.929 +          case outcome of
  12.930 +            NONE => false
  12.931 +          | SOME (SMT_Failure.Counterexample _) => false
  12.932 +          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
  12.933 +          | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
  12.934 +          | SOME SMT_Failure.Out_Of_Memory => true
  12.935 +          | SOME (SMT_Failure.Other_Failure _) => true
  12.936 +        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
  12.937 +      in
  12.938 +        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
  12.939 +           Time.> (timeout, Time.zeroTime) then
  12.940 +          let
  12.941 +            val new_num_facts =
  12.942 +              Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
  12.943 +            val weighted_factss as (new_fact_filter, _) :: _ =
  12.944 +              weighted_factss
  12.945 +              |> (fn (x :: xs) => xs @ [x])
  12.946 +              |> app_hd (apsnd (take new_num_facts))
  12.947 +            val show_filter = fact_filter <> new_fact_filter
  12.948 +            fun num_of_facts fact_filter num_facts =
  12.949 +              string_of_int num_facts ^
  12.950 +              (if show_filter then " " ^ quote fact_filter else "") ^
  12.951 +              " fact" ^ plural_s num_facts
  12.952 +            val _ =
  12.953 +              if debug then
  12.954 +                quote name ^ " invoked with " ^
  12.955 +                num_of_facts fact_filter num_facts ^ ": " ^
  12.956 +                string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
  12.957 +                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
  12.958 +                "..."
  12.959 +                |> Output.urgent_message
  12.960 +              else
  12.961 +                ()
  12.962 +          in
  12.963 +            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
  12.964 +          end
  12.965 +        else
  12.966 +          {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
  12.967 +           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
  12.968 +      end
  12.969 +  in
  12.970 +    do_slice timeout 1 NONE Time.zeroTime
  12.971 +  end
  12.972 +
  12.973 +fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
  12.974 +    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
  12.975 +  let
  12.976 +    val ctxt = Proof.context_of state
  12.977 +    fun weight_facts facts =
  12.978 +      let val num_facts = length facts in
  12.979 +        facts ~~ (0 upto num_facts - 1)
  12.980 +        |> map (weight_smt_fact ctxt num_facts)
  12.981 +      end
  12.982 +    val weighted_factss = factss |> map (apsnd weight_facts)
  12.983 +    val {outcome, used_facts = used_pairs, used_from, run_time} =
  12.984 +      smt_filter_loop name params state goal subgoal weighted_factss
  12.985 +    val used_facts = used_pairs |> map fst
  12.986 +    val outcome = outcome |> Option.map failure_of_smt_failure
  12.987 +    val (preplay, message, message_tail) =
  12.988 +      case outcome of
  12.989 +        NONE =>
  12.990 +        (Lazy.lazy (fn () =>
  12.991 +           play_one_line_proof mode debug verbose preplay_timeout used_pairs
  12.992 +               state subgoal SMT
  12.993 +               (bunch_of_reconstructors false (fn desperate =>
  12.994 +                  if desperate then liftingN else default_metis_lam_trans))),
  12.995 +         fn preplay =>
  12.996 +            let
  12.997 +              val one_line_params =
  12.998 +                (preplay, proof_banner mode name, used_facts,
  12.999 +                 choose_minimize_command ctxt params minimize_command name preplay,
 12.1000 +                 subgoal, subgoal_count)
 12.1001 +              val num_chained = length (#facts (Proof.goal state))
 12.1002 +            in
 12.1003 +              one_line_proof_text num_chained one_line_params
 12.1004 +            end,
 12.1005 +         if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
 12.1006 +      | SOME failure =>
 12.1007 +        (Lazy.value (plain_metis, Play_Failed),
 12.1008 +         fn _ => string_of_atp_failure failure, "")
 12.1009 +  in
 12.1010 +    {outcome = outcome, used_facts = used_facts, used_from = used_from,
 12.1011 +     run_time = run_time, preplay = preplay, message = message,
 12.1012 +     message_tail = message_tail}
 12.1013 +  end
 12.1014 +
 12.1015 +fun run_reconstructor mode name
 12.1016 +        (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
 12.1017 +        minimize_command
 12.1018 +        ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...}
 12.1019 +         : prover_problem) =
 12.1020 +  let
 12.1021 +    val reconstr =
 12.1022 +      if name = metisN then
 12.1023 +        Metis (type_enc |> the_default (hd partial_type_encs),
 12.1024 +               lam_trans |> the_default default_metis_lam_trans)
 12.1025 +      else if name = smtN then
 12.1026 +        SMT
 12.1027 +      else
 12.1028 +        raise Fail ("unknown reconstructor: " ^ quote name)
 12.1029 +    val used_facts = facts |> map fst
 12.1030 +  in
 12.1031 +    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
 12.1032 +       state subgoal reconstr [reconstr] of
 12.1033 +      play as (_, Played time) =>
 12.1034 +      {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
 12.1035 +       preplay = Lazy.value play,
 12.1036 +       message =
 12.1037 +         fn play =>
 12.1038 +            let
 12.1039 +              val (_, override_params) = extract_reconstructor params reconstr
 12.1040 +              val one_line_params =
 12.1041 +                (play, proof_banner mode name, used_facts, minimize_command override_params name,
 12.1042 +                 subgoal, subgoal_count)
 12.1043 +              val num_chained = length (#facts (Proof.goal state))
 12.1044 +            in
 12.1045 +              one_line_proof_text num_chained one_line_params
 12.1046 +            end,
 12.1047 +       message_tail = ""}
 12.1048 +    | play =>
 12.1049 +      let
 12.1050 +        val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
 12.1051 +      in
 12.1052 +        {outcome = SOME failure, used_facts = [], used_from = [],
 12.1053 +         run_time = Time.zeroTime, preplay = Lazy.value play,
 12.1054 +         message = fn _ => string_of_atp_failure failure, message_tail = ""}
 12.1055 +      end)
 12.1056 +  end
 12.1057 +
 12.1058 +fun get_prover ctxt mode name =
 12.1059 +  let val thy = Proof_Context.theory_of ctxt in
 12.1060 +    if is_reconstructor name then run_reconstructor mode name
 12.1061 +    else if is_atp thy name then run_atp mode name (get_atp thy name ())
 12.1062 +    else if is_smt_prover ctxt name then run_smt_solver mode name
 12.1063 +    else error ("No such prover: " ^ name ^ ".")
 12.1064 +  end
 12.1065 +
 12.1066 +end;
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jan 31 10:23:32 2014 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,1063 +0,0 @@
    13.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_provers.ML
    13.5 -    Author:     Fabian Immler, TU Muenchen
    13.6 -    Author:     Makarius
    13.7 -    Author:     Jasmin Blanchette, TU Muenchen
    13.8 -
    13.9 -Generic prover abstraction for Sledgehammer.
   13.10 -*)
   13.11 -
   13.12 -signature SLEDGEHAMMER_PROVERS =
   13.13 -sig
   13.14 -  type atp_failure = ATP_Proof.atp_failure
   13.15 -  type stature = ATP_Problem_Generate.stature
   13.16 -  type type_enc = ATP_Problem_Generate.type_enc
   13.17 -  type fact = Sledgehammer_Fact.fact
   13.18 -  type reconstructor = Sledgehammer_Reconstructor.reconstructor
   13.19 -  type play_outcome = Sledgehammer_Reconstructor.play_outcome
   13.20 -  type minimize_command = Sledgehammer_Reconstructor.minimize_command
   13.21 -
   13.22 -  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
   13.23 -
   13.24 -  type params =
   13.25 -    {debug : bool,
   13.26 -     verbose : bool,
   13.27 -     overlord : bool,
   13.28 -     spy : bool,
   13.29 -     blocking : bool,
   13.30 -     provers : string list,
   13.31 -     type_enc : string option,
   13.32 -     strict : bool,
   13.33 -     lam_trans : string option,
   13.34 -     uncurried_aliases : bool option,
   13.35 -     learn : bool,
   13.36 -     fact_filter : string option,
   13.37 -     max_facts : int option,
   13.38 -     fact_thresholds : real * real,
   13.39 -     max_mono_iters : int option,
   13.40 -     max_new_mono_instances : int option,
   13.41 -     isar_proofs : bool option,
   13.42 -     compress_isar : real,
   13.43 -     try0_isar : bool,
   13.44 -     slice : bool,
   13.45 -     minimize : bool option,
   13.46 -     timeout : Time.time,
   13.47 -     preplay_timeout : Time.time,
   13.48 -     expect : string}
   13.49 -
   13.50 -  type prover_problem =
   13.51 -    {comment : string,
   13.52 -     state : Proof.state,
   13.53 -     goal : thm,
   13.54 -     subgoal : int,
   13.55 -     subgoal_count : int,
   13.56 -     factss : (string * fact list) list}
   13.57 -
   13.58 -  type prover_result =
   13.59 -    {outcome : atp_failure option,
   13.60 -     used_facts : (string * stature) list,
   13.61 -     used_from : fact list,
   13.62 -     run_time : Time.time,
   13.63 -     preplay : (reconstructor * play_outcome) Lazy.lazy,
   13.64 -     message : reconstructor * play_outcome -> string,
   13.65 -     message_tail : string}
   13.66 -
   13.67 -  type prover =
   13.68 -    params -> ((string * string list) list -> string -> minimize_command)
   13.69 -    -> prover_problem -> prover_result
   13.70 -
   13.71 -  val dest_dir : string Config.T
   13.72 -  val problem_prefix : string Config.T
   13.73 -  val completish : bool Config.T
   13.74 -  val atp_full_names : bool Config.T
   13.75 -  val smt_builtins : bool Config.T
   13.76 -  val smt_triggers : bool Config.T
   13.77 -  val smt_weights : bool Config.T
   13.78 -  val smt_weight_min_facts : int Config.T
   13.79 -  val smt_min_weight : int Config.T
   13.80 -  val smt_max_weight : int Config.T
   13.81 -  val smt_max_weight_index : int Config.T
   13.82 -  val smt_weight_curve : (int -> int) Unsynchronized.ref
   13.83 -  val smt_max_slices : int Config.T
   13.84 -  val smt_slice_fact_frac : real Config.T
   13.85 -  val smt_slice_time_frac : real Config.T
   13.86 -  val smt_slice_min_secs : int Config.T
   13.87 -  val SledgehammerN : string
   13.88 -  val plain_metis : reconstructor
   13.89 -  val select_smt_solver : string -> Proof.context -> Proof.context
   13.90 -  val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
   13.91 -  val is_reconstructor : string -> bool
   13.92 -  val is_atp : theory -> string -> bool
   13.93 -  val is_smt_prover : Proof.context -> string -> bool
   13.94 -  val is_ho_atp: Proof.context -> string -> bool
   13.95 -  val is_unit_equational_atp : Proof.context -> string -> bool
   13.96 -  val is_prover_supported : Proof.context -> string -> bool
   13.97 -  val is_prover_installed : Proof.context -> string -> bool
   13.98 -  val remotify_prover_if_supported_and_not_already_remote :
   13.99 -    Proof.context -> string -> string option
  13.100 -  val remotify_prover_if_not_installed :
  13.101 -    Proof.context -> string -> string option
  13.102 -  val default_max_facts_of_prover : Proof.context -> string -> int
  13.103 -  val is_unit_equality : term -> bool
  13.104 -  val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
  13.105 -  val weight_smt_fact :
  13.106 -    Proof.context -> int -> ((string * stature) * thm) * int
  13.107 -    -> (string * stature) * (int option * thm)
  13.108 -  val supported_provers : Proof.context -> unit
  13.109 -  val kill_provers : unit -> unit
  13.110 -  val running_provers : unit -> unit
  13.111 -  val messages : int option -> unit
  13.112 -  val is_fact_chained : (('a * stature) * 'b) -> bool
  13.113 -  val filter_used_facts :
  13.114 -    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
  13.115 -    ((''a * stature) * 'b) list
  13.116 -  val isar_proof_reconstructor : Proof.context -> string -> string
  13.117 -  val get_prover : Proof.context -> mode -> string -> prover
  13.118 -end;
  13.119 -
  13.120 -structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
  13.121 -struct
  13.122 -
  13.123 -open ATP_Util
  13.124 -open ATP_Problem
  13.125 -open ATP_Proof
  13.126 -open ATP_Systems
  13.127 -open ATP_Problem_Generate
  13.128 -open ATP_Proof_Reconstruct
  13.129 -open Metis_Tactic
  13.130 -open Sledgehammer_Util
  13.131 -open Sledgehammer_Fact
  13.132 -open Sledgehammer_Reconstructor
  13.133 -open Sledgehammer_Print
  13.134 -open Sledgehammer_Reconstruct
  13.135 -
  13.136 -
  13.137 -(** The Sledgehammer **)
  13.138 -
  13.139 -(* Empty string means create files in Isabelle's temporary files directory. *)
  13.140 -val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
  13.141 -val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
  13.142 -val completish = Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
  13.143 -
  13.144 -(* In addition to being easier to read, readable names are often much shorter,
  13.145 -   especially if types are mangled in names. This makes a difference for some
  13.146 -   provers (e.g., E). For these reason, short names are enabled by default. *)
  13.147 -val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
  13.148 -
  13.149 -val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
  13.150 -val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
  13.151 -val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
  13.152 -val smt_weight_min_facts =
  13.153 -  Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
  13.154 -
  13.155 -datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
  13.156 -
  13.157 -(* Identifier that distinguishes Sledgehammer from other tools that could use
  13.158 -   "Async_Manager". *)
  13.159 -val SledgehammerN = "Sledgehammer"
  13.160 -
  13.161 -val reconstructor_names = [metisN, smtN]
  13.162 -val plain_metis = Metis (hd partial_type_encs, combsN)
  13.163 -val is_reconstructor = member (op =) reconstructor_names
  13.164 -
  13.165 -val is_atp = member (op =) o supported_atps
  13.166 -
  13.167 -val select_smt_solver = Context.proof_map o SMT_Config.select_solver
  13.168 -
  13.169 -fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
  13.170 -
  13.171 -fun is_atp_of_format is_format ctxt name =
  13.172 -  let val thy = Proof_Context.theory_of ctxt in
  13.173 -    case try (get_atp thy) name of
  13.174 -      SOME config =>
  13.175 -      exists (fn (_, ((_, format, _, _, _), _)) => is_format format)
  13.176 -             (#best_slices (config ()) ctxt)
  13.177 -    | NONE => false
  13.178 -  end
  13.179 -
  13.180 -val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ)
  13.181 -val is_ho_atp = is_atp_of_format is_format_higher_order
  13.182 -
  13.183 -fun is_prover_supported ctxt =
  13.184 -  let val thy = Proof_Context.theory_of ctxt in
  13.185 -    is_reconstructor orf is_atp thy orf is_smt_prover ctxt
  13.186 -  end
  13.187 -
  13.188 -fun is_prover_installed ctxt =
  13.189 -  is_reconstructor orf is_smt_prover ctxt orf
  13.190 -  is_atp_installed (Proof_Context.theory_of ctxt)
  13.191 -
  13.192 -fun remotify_prover_if_supported_and_not_already_remote ctxt name =
  13.193 -  if String.isPrefix remote_prefix name then
  13.194 -    SOME name
  13.195 -  else
  13.196 -    let val remote_name = remote_prefix ^ name in
  13.197 -      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
  13.198 -    end
  13.199 -
  13.200 -fun remotify_prover_if_not_installed ctxt name =
  13.201 -  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
  13.202 -    SOME name
  13.203 -  else
  13.204 -    remotify_prover_if_supported_and_not_already_remote ctxt name
  13.205 -
  13.206 -fun get_slices slice slices =
  13.207 -  (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
  13.208 -
  13.209 -val reconstructor_default_max_facts = 20
  13.210 -
  13.211 -fun slice_max_facts (_, ( ((max_facts, _), _, _, _, _), _)) = max_facts
  13.212 -
  13.213 -fun default_max_facts_of_prover ctxt name =
  13.214 -  let val thy = Proof_Context.theory_of ctxt in
  13.215 -    if is_reconstructor name then
  13.216 -      reconstructor_default_max_facts
  13.217 -    else if is_atp thy name then
  13.218 -      fold (Integer.max o slice_max_facts) (#best_slices (get_atp thy name ()) ctxt) 0
  13.219 -    else (* is_smt_prover ctxt name *)
  13.220 -      SMT_Solver.default_max_relevant ctxt name
  13.221 -  end
  13.222 -
  13.223 -fun is_if (@{const_name If}, _) = true
  13.224 -  | is_if _ = false
  13.225 -
  13.226 -(* Beware of "if and only if" (which is translated as such) and "If" (which is
  13.227 -   translated to conditional equations). *)
  13.228 -fun is_good_unit_equality T t u =
  13.229 -  T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u])
  13.230 -
  13.231 -fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t
  13.232 -  | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) =
  13.233 -    is_unit_equality t
  13.234 -  | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) =
  13.235 -    is_unit_equality t
  13.236 -  | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) =
  13.237 -    is_good_unit_equality T t u
  13.238 -  | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) =
  13.239 -    is_good_unit_equality T t u
  13.240 -  | is_unit_equality _ = false
  13.241 -
  13.242 -fun is_appropriate_prop_of_prover ctxt name =
  13.243 -  if is_unit_equational_atp ctxt name then is_unit_equality else K true
  13.244 -
  13.245 -fun supported_provers ctxt =
  13.246 -  let
  13.247 -    val thy = Proof_Context.theory_of ctxt
  13.248 -    val (remote_provers, local_provers) =
  13.249 -      reconstructor_names @
  13.250 -      sort_strings (supported_atps thy) @
  13.251 -      sort_strings (SMT_Solver.available_solvers_of ctxt)
  13.252 -      |> List.partition (String.isPrefix remote_prefix)
  13.253 -  in
  13.254 -    Output.urgent_message ("Supported provers: " ^
  13.255 -                           commas (local_provers @ remote_provers) ^ ".")
  13.256 -  end
  13.257 -
  13.258 -fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
  13.259 -fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
  13.260 -val messages = Async_Manager.thread_messages SledgehammerN "prover"
  13.261 -
  13.262 -
  13.263 -(** problems, results, ATPs, etc. **)
  13.264 -
  13.265 -type params =
  13.266 -  {debug : bool,
  13.267 -   verbose : bool,
  13.268 -   overlord : bool,
  13.269 -   spy : bool,
  13.270 -   blocking : bool,
  13.271 -   provers : string list,
  13.272 -   type_enc : string option,
  13.273 -   strict : bool,
  13.274 -   lam_trans : string option,
  13.275 -   uncurried_aliases : bool option,
  13.276 -   learn : bool,
  13.277 -   fact_filter : string option,
  13.278 -   max_facts : int option,
  13.279 -   fact_thresholds : real * real,
  13.280 -   max_mono_iters : int option,
  13.281 -   max_new_mono_instances : int option,
  13.282 -   isar_proofs : bool option,
  13.283 -   compress_isar : real,
  13.284 -   try0_isar : bool,
  13.285 -   slice : bool,
  13.286 -   minimize : bool option,
  13.287 -   timeout : Time.time,
  13.288 -   preplay_timeout : Time.time,
  13.289 -   expect : string}
  13.290 -
  13.291 -type prover_problem =
  13.292 -  {comment : string,
  13.293 -   state : Proof.state,
  13.294 -   goal : thm,
  13.295 -   subgoal : int,
  13.296 -   subgoal_count : int,
  13.297 -   factss : (string * fact list) list}
  13.298 -
  13.299 -type prover_result =
  13.300 -  {outcome : atp_failure option,
  13.301 -   used_facts : (string * stature) list,
  13.302 -   used_from : fact list,
  13.303 -   run_time : Time.time,
  13.304 -   preplay : (reconstructor * play_outcome) Lazy.lazy,
  13.305 -   message : reconstructor * play_outcome -> string,
  13.306 -   message_tail : string}
  13.307 -
  13.308 -type prover =
  13.309 -  params -> ((string * string list) list -> string -> minimize_command)
  13.310 -  -> prover_problem -> prover_result
  13.311 -
  13.312 -(* FUDGE *)
  13.313 -val smt_min_weight =
  13.314 -  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
  13.315 -val smt_max_weight =
  13.316 -  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
  13.317 -val smt_max_weight_index =
  13.318 -  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
  13.319 -val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
  13.320 -
  13.321 -fun smt_fact_weight ctxt j num_facts =
  13.322 -  if Config.get ctxt smt_weights andalso
  13.323 -     num_facts >= Config.get ctxt smt_weight_min_facts then
  13.324 -    let
  13.325 -      val min = Config.get ctxt smt_min_weight
  13.326 -      val max = Config.get ctxt smt_max_weight
  13.327 -      val max_index = Config.get ctxt smt_max_weight_index
  13.328 -      val curve = !smt_weight_curve
  13.329 -    in
  13.330 -      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
  13.331 -            div curve max_index)
  13.332 -    end
  13.333 -  else
  13.334 -    NONE
  13.335 -
  13.336 -fun weight_smt_fact ctxt num_facts ((info, th), j) =
  13.337 -  let val thy = Proof_Context.theory_of ctxt in
  13.338 -    (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
  13.339 -  end
  13.340 -
  13.341 -fun overlord_file_location_of_prover prover =
  13.342 -  (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
  13.343 -
  13.344 -fun proof_banner mode name =
  13.345 -  case mode of
  13.346 -    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
  13.347 -  | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
  13.348 -  | _ => "Try this"
  13.349 -
  13.350 -fun bunch_of_reconstructors needs_full_types lam_trans =
  13.351 -  if needs_full_types then
  13.352 -    [Metis (full_type_enc, lam_trans false),
  13.353 -     Metis (really_full_type_enc, lam_trans false),
  13.354 -     Metis (full_type_enc, lam_trans true),
  13.355 -     Metis (really_full_type_enc, lam_trans true),
  13.356 -     SMT]
  13.357 -  else
  13.358 -    [Metis (partial_type_enc, lam_trans false),
  13.359 -     Metis (full_type_enc, lam_trans false),
  13.360 -     Metis (no_typesN, lam_trans true),
  13.361 -     Metis (really_full_type_enc, lam_trans true),
  13.362 -     SMT]
  13.363 -
  13.364 -fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
  13.365 -    let
  13.366 -      val override_params =
  13.367 -        (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
  13.368 -         else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
  13.369 -        (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
  13.370 -         else [("lam_trans", [lam_trans'])])
  13.371 -    in (metisN, override_params) end
  13.372 -  | extract_reconstructor _ SMT = (smtN, [])
  13.373 -
  13.374 -(* based on "Mirabelle.can_apply" and generalized *)
  13.375 -fun timed_apply timeout tac state i =
  13.376 -  let
  13.377 -    val {context = ctxt, facts, goal} = Proof.goal state
  13.378 -    val full_tac = Method.insert_tac facts i THEN tac ctxt i
  13.379 -  in
  13.380 -    TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
  13.381 -  end
  13.382 -
  13.383 -fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
  13.384 -  | tac_of_reconstructor SMT = SMT_Solver.smt_tac
  13.385 -
  13.386 -fun timed_reconstructor reconstr debug timeout ths =
  13.387 -  timed_apply timeout (silence_reconstructors debug
  13.388 -    #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
  13.389 -
  13.390 -fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
  13.391 -
  13.392 -fun filter_used_facts keep_chained used =
  13.393 -  filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
  13.394 -
  13.395 -fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
  13.396 -  let
  13.397 -    fun get_preferred reconstrs =
  13.398 -      if member (op =) reconstrs preferred then preferred
  13.399 -      else List.last reconstrs
  13.400 -  in
  13.401 -    if timeout = Time.zeroTime then
  13.402 -      (get_preferred reconstrs, Not_Played)
  13.403 -    else
  13.404 -      let
  13.405 -        val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
  13.406 -        val ths = pairs |> sort_wrt (fst o fst) |> map snd
  13.407 -        fun play [] [] = (get_preferred reconstrs, Play_Failed)
  13.408 -          | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
  13.409 -          | play timed_out (reconstr :: reconstrs) =
  13.410 -            let
  13.411 -              val _ =
  13.412 -                if verbose then
  13.413 -                  Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
  13.414 -                    "\" for " ^ string_of_time timeout ^ "...")
  13.415 -                else
  13.416 -                  ()
  13.417 -              val timer = Timer.startRealTimer ()
  13.418 -            in
  13.419 -              case timed_reconstructor reconstr debug timeout ths state i of
  13.420 -                SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
  13.421 -              | _ => play timed_out reconstrs
  13.422 -            end
  13.423 -            handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
  13.424 -      in
  13.425 -        play [] reconstrs
  13.426 -      end
  13.427 -  end
  13.428 -
  13.429 -
  13.430 -(* generic TPTP-based ATPs *)
  13.431 -
  13.432 -(* Too general means, positive equality literal with a variable X as one
  13.433 -   operand, when X does not occur properly in the other operand. This rules out
  13.434 -   clearly inconsistent facts such as X = a | X = b, though it by no means
  13.435 -   guarantees soundness. *)
  13.436 -
  13.437 -fun get_facts_of_filter _ [(_, facts)] = facts
  13.438 -  | get_facts_of_filter fact_filter factss =
  13.439 -    case AList.lookup (op =) factss fact_filter of
  13.440 -      SOME facts => facts
  13.441 -    | NONE => snd (hd factss)
  13.442 -
  13.443 -(* Unwanted equalities are those between a (bound or schematic) variable that
  13.444 -   does not properly occur in the second operand. *)
  13.445 -val is_exhaustive_finite =
  13.446 -  let
  13.447 -    fun is_bad_equal (Var z) t =
  13.448 -        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
  13.449 -      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
  13.450 -      | is_bad_equal _ _ = false
  13.451 -    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
  13.452 -    fun do_formula pos t =
  13.453 -      case (pos, t) of
  13.454 -        (_, @{const Trueprop} $ t1) => do_formula pos t1
  13.455 -      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
  13.456 -        do_formula pos t'
  13.457 -      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
  13.458 -        do_formula pos t'
  13.459 -      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
  13.460 -        do_formula pos t'
  13.461 -      | (_, @{const "==>"} $ t1 $ t2) =>
  13.462 -        do_formula (not pos) t1 andalso
  13.463 -        (t2 = @{prop False} orelse do_formula pos t2)
  13.464 -      | (_, @{const HOL.implies} $ t1 $ t2) =>
  13.465 -        do_formula (not pos) t1 andalso
  13.466 -        (t2 = @{const False} orelse do_formula pos t2)
  13.467 -      | (_, @{const Not} $ t1) => do_formula (not pos) t1
  13.468 -      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
  13.469 -      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
  13.470 -      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
  13.471 -      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
  13.472 -      | _ => false
  13.473 -  in do_formula true end
  13.474 -
  13.475 -fun has_bound_or_var_of_type pred =
  13.476 -  exists_subterm (fn Var (_, T as Type _) => pred T
  13.477 -                   | Abs (_, T as Type _, _) => pred T
  13.478 -                   | _ => false)
  13.479 -
  13.480 -(* Facts are forbidden to contain variables of these types. The typical reason
  13.481 -   is that they lead to unsoundness. Note that "unit" satisfies numerous
  13.482 -   equations like "?x = ()". The resulting clauses will have no type constraint,
  13.483 -   yielding false proofs. Even "bool" leads to many unsound proofs, though only
  13.484 -   for higher-order problems. *)
  13.485 -
  13.486 -(* Facts containing variables of type "unit" or "bool" or of the form
  13.487 -   "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
  13.488 -   are omitted. *)
  13.489 -fun is_dangerous_prop ctxt =
  13.490 -  transform_elim_prop
  13.491 -  #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
  13.492 -      is_exhaustive_finite)
  13.493 -
  13.494 -(* Important messages are important but not so important that users want to see
  13.495 -   them each time. *)
  13.496 -val atp_important_message_keep_quotient = 25
  13.497 -
  13.498 -fun choose_type_enc strictness best_type_enc format =
  13.499 -  the_default best_type_enc
  13.500 -  #> type_enc_of_string strictness
  13.501 -  #> adjust_type_enc format
  13.502 -
  13.503 -fun isar_proof_reconstructor ctxt name =
  13.504 -  let val thy = Proof_Context.theory_of ctxt in
  13.505 -    if is_atp thy name then name
  13.506 -    else remotify_prover_if_not_installed ctxt eN |> the_default name
  13.507 -  end
  13.508 -
  13.509 -(* See the analogous logic in the function "maybe_minimize" in
  13.510 -  "sledgehammer_minimize.ML". *)
  13.511 -fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command name preplay =
  13.512 -  let
  13.513 -    val maybe_isar_name = name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
  13.514 -    val (min_name, override_params) =
  13.515 -      (case preplay of
  13.516 -        (reconstr, Played _) =>
  13.517 -        if isar_proofs = SOME true then (maybe_isar_name, [])
  13.518 -        else extract_reconstructor params reconstr
  13.519 -      | _ => (maybe_isar_name, []))
  13.520 -  in minimize_command override_params min_name end
  13.521 -
  13.522 -val max_fact_instances = 10 (* FUDGE *)
  13.523 -
  13.524 -fun repair_monomorph_context max_iters best_max_iters max_new_instances
  13.525 -                             best_max_new_instances =
  13.526 -  Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
  13.527 -  #> Config.put Monomorph.max_new_instances
  13.528 -         (max_new_instances |> the_default best_max_new_instances)
  13.529 -  #> Config.put Monomorph.max_thm_instances max_fact_instances
  13.530 -
  13.531 -fun suffix_of_mode Auto_Try = "_try"
  13.532 -  | suffix_of_mode Try = "_try"
  13.533 -  | suffix_of_mode Normal = ""
  13.534 -  | suffix_of_mode MaSh = ""
  13.535 -  | suffix_of_mode Auto_Minimize = "_min"
  13.536 -  | suffix_of_mode Minimize = "_min"
  13.537 -
  13.538 -(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
  13.539 -   Linux appears to be the only ATP that does not honor its time limit. *)
  13.540 -val atp_timeout_slack = seconds 1.0
  13.541 -
  13.542 -val mono_max_privileged_facts = 10
  13.543 -
  13.544 -(* For low values of "max_facts", this fudge value ensures that most slices are
  13.545 -   invoked with a nontrivial amount of facts. *)
  13.546 -val max_fact_factor_fudge = 5
  13.547 -
  13.548 -fun run_atp mode name
  13.549 -    ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
  13.550 -      best_max_new_mono_instances, ...} : atp_config)
  13.551 -    (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
  13.552 -       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
  13.553 -       try0_isar, slice, timeout, preplay_timeout, ...})
  13.554 -    minimize_command
  13.555 -    ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
  13.556 -  let
  13.557 -    val thy = Proof.theory_of state
  13.558 -    val ctxt = Proof.context_of state
  13.559 -    val atp_mode =
  13.560 -      if Config.get ctxt completish then Sledgehammer_Completish
  13.561 -      else Sledgehammer
  13.562 -    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
  13.563 -    val (dest_dir, problem_prefix) =
  13.564 -      if overlord then overlord_file_location_of_prover name
  13.565 -      else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
  13.566 -    val problem_file_name =
  13.567 -      Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
  13.568 -                  suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
  13.569 -    val prob_path =
  13.570 -      if dest_dir = "" then
  13.571 -        File.tmp_path problem_file_name
  13.572 -      else if File.exists (Path.explode dest_dir) then
  13.573 -        Path.append (Path.explode dest_dir) problem_file_name
  13.574 -      else
  13.575 -        error ("No such directory: " ^ quote dest_dir ^ ".")
  13.576 -    val exec = exec ()
  13.577 -    val command0 =
  13.578 -      case find_first (fn var => getenv var <> "") (fst exec) of
  13.579 -        SOME var =>
  13.580 -        let
  13.581 -          val pref = getenv var ^ "/"
  13.582 -          val paths = map (Path.explode o prefix pref) (snd exec)
  13.583 -        in
  13.584 -          case find_first File.exists paths of
  13.585 -            SOME path => path
  13.586 -          | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
  13.587 -        end
  13.588 -      | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^
  13.589 -                       " is not set.")
  13.590 -    fun split_time s =
  13.591 -      let
  13.592 -        val split = String.tokens (fn c => str c = "\n")
  13.593 -        val (output, t) =
  13.594 -          s |> split |> (try split_last #> the_default ([], "0"))
  13.595 -            |>> cat_lines
  13.596 -        fun as_num f = f >> (fst o read_int)
  13.597 -        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
  13.598 -        val digit = Scan.one Symbol.is_ascii_digit
  13.599 -        val num3 = as_num (digit ::: digit ::: (digit >> single))
  13.600 -        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
  13.601 -        val as_time =
  13.602 -          raw_explode #> Scan.read Symbol.stopper time #> the_default 0
  13.603 -      in (output, as_time t |> Time.fromMilliseconds) end
  13.604 -    fun run () =
  13.605 -      let
  13.606 -        (* If slicing is disabled, we expand the last slice to fill the entire
  13.607 -           time available. *)
  13.608 -        val all_slices = best_slices ctxt
  13.609 -        val actual_slices = get_slices slice all_slices
  13.610 -        fun max_facts_of_slices f slices = fold (Integer.max o slice_max_facts o f) slices 0
  13.611 -        val num_actual_slices = length actual_slices
  13.612 -        val max_fact_factor =
  13.613 -          Real.fromInt (case max_facts of
  13.614 -              NONE => max_facts_of_slices I all_slices
  13.615 -            | SOME max => max)
  13.616 -          / Real.fromInt (max_facts_of_slices snd actual_slices)
  13.617 -        fun monomorphize_facts facts =
  13.618 -          let
  13.619 -            val ctxt =
  13.620 -              ctxt
  13.621 -              |> repair_monomorph_context max_mono_iters
  13.622 -                     best_max_mono_iters max_new_mono_instances
  13.623 -                     best_max_new_mono_instances
  13.624 -            (* pseudo-theorem involving the same constants as the subgoal *)
  13.625 -            val subgoal_th =
  13.626 -              Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
  13.627 -            val rths =
  13.628 -              facts |> chop mono_max_privileged_facts
  13.629 -                    |>> map (pair 1 o snd)
  13.630 -                    ||> map (pair 2 o snd)
  13.631 -                    |> op @
  13.632 -                    |> cons (0, subgoal_th)
  13.633 -          in
  13.634 -            Monomorph.monomorph atp_schematic_consts_of ctxt rths
  13.635 -            |> tl |> curry ListPair.zip (map fst facts)
  13.636 -            |> maps (fn (name, rths) =>
  13.637 -                        map (pair name o zero_var_indexes o snd) rths)
  13.638 -          end
  13.639 -        fun run_slice time_left (cache_key, cache_value)
  13.640 -                (slice, (time_frac,
  13.641 -                     (key as ((best_max_facts, best_fact_filter), format,
  13.642 -                              best_type_enc, best_lam_trans,
  13.643 -                              best_uncurried_aliases),
  13.644 -                      extra))) =
  13.645 -          let
  13.646 -            val effective_fact_filter =
  13.647 -              fact_filter |> the_default best_fact_filter
  13.648 -            val facts = get_facts_of_filter effective_fact_filter factss
  13.649 -            val num_facts =
  13.650 -              Real.ceil (max_fact_factor * Real.fromInt best_max_facts) +
  13.651 -              max_fact_factor_fudge
  13.652 -              |> Integer.min (length facts)
  13.653 -            val strictness = if strict then Strict else Non_Strict
  13.654 -            val type_enc =
  13.655 -              type_enc |> choose_type_enc strictness best_type_enc format
  13.656 -            val sound = is_type_enc_sound type_enc
  13.657 -            val real_ms = Real.fromInt o Time.toMilliseconds
  13.658 -            val slice_timeout =
  13.659 -              (real_ms time_left
  13.660 -               |> (if slice < num_actual_slices - 1 then
  13.661 -                     curry Real.min (time_frac * real_ms timeout)
  13.662 -                   else
  13.663 -                     I))
  13.664 -              * 0.001
  13.665 -              |> seconds
  13.666 -            val generous_slice_timeout =
  13.667 -              if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
  13.668 -            val _ =
  13.669 -              if debug then
  13.670 -                quote name ^ " slice #" ^ string_of_int (slice + 1) ^
  13.671 -                " with " ^ string_of_int num_facts ^ " fact" ^
  13.672 -                plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
  13.673 -                |> Output.urgent_message
  13.674 -              else
  13.675 -                ()
  13.676 -            val readable_names = not (Config.get ctxt atp_full_names)
  13.677 -            val lam_trans =
  13.678 -              case lam_trans of
  13.679 -                SOME s => s
  13.680 -              | NONE => best_lam_trans
  13.681 -            val uncurried_aliases =
  13.682 -              case uncurried_aliases of
  13.683 -                SOME b => b
  13.684 -              | NONE => best_uncurried_aliases
  13.685 -            val value as (atp_problem, _, fact_names, _, _) =
  13.686 -              if cache_key = SOME key then
  13.687 -                cache_value
  13.688 -              else
  13.689 -                facts
  13.690 -                |> not sound
  13.691 -                   ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
  13.692 -                |> take num_facts
  13.693 -                |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
  13.694 -                |> map (apsnd prop_of)
  13.695 -                |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
  13.696 -                                       lam_trans uncurried_aliases
  13.697 -                                       readable_names true hyp_ts concl_t
  13.698 -            fun sel_weights () = atp_problem_selection_weights atp_problem
  13.699 -            fun ord_info () = atp_problem_term_order_info atp_problem
  13.700 -            val ord = effective_term_order ctxt name
  13.701 -            val full_proof = isar_proofs |> the_default (mode = Minimize)
  13.702 -            val args =
  13.703 -              arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
  13.704 -                (ord, ord_info, sel_weights)
  13.705 -            val command =
  13.706 -              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
  13.707 -              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
  13.708 -            val _ =
  13.709 -              atp_problem
  13.710 -              |> lines_of_atp_problem format ord ord_info
  13.711 -              |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
  13.712 -              |> File.write_list prob_path
  13.713 -            val ((output, run_time), (atp_proof, outcome)) =
  13.714 -              TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
  13.715 -              |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
  13.716 -              |> fst |> split_time
  13.717 -              |> (fn accum as (output, _) =>
  13.718 -                     (accum,
  13.719 -                      extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
  13.720 -                      |>> atp_proof_of_tstplike_proof atp_problem
  13.721 -                      handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
  13.722 -              handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
  13.723 -            val outcome =
  13.724 -              (case outcome of
  13.725 -                NONE =>
  13.726 -                (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
  13.727 -                      |> Option.map (sort string_ord) of
  13.728 -                   SOME facts =>
  13.729 -                   let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
  13.730 -                     if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
  13.731 -                   end
  13.732 -                 | NONE => NONE)
  13.733 -              | _ => outcome)
  13.734 -          in
  13.735 -            ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
  13.736 -          end
  13.737 -        val timer = Timer.startRealTimer ()
  13.738 -        fun maybe_run_slice slice
  13.739 -                (result as (cache, (_, run_time0, _, _, SOME _))) =
  13.740 -            let
  13.741 -              val time_left = Time.- (timeout, Timer.checkRealTimer timer)
  13.742 -            in
  13.743 -              if Time.<= (time_left, Time.zeroTime) then
  13.744 -                result
  13.745 -              else
  13.746 -                run_slice time_left cache slice
  13.747 -                |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) =>
  13.748 -                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome)))
  13.749 -            end
  13.750 -          | maybe_run_slice _ result = result
  13.751 -      in
  13.752 -        ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
  13.753 -         ("", Time.zeroTime, [], [], SOME InternalError))
  13.754 -        |> fold maybe_run_slice actual_slices
  13.755 -      end
  13.756 -    (* If the problem file has not been exported, remove it; otherwise, export
  13.757 -       the proof file too. *)
  13.758 -    fun clean_up () =
  13.759 -      if dest_dir = "" then (try File.rm prob_path; ()) else ()
  13.760 -    fun export (_, (output, _, _, _, _)) =
  13.761 -      if dest_dir = "" then ()
  13.762 -      else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
  13.763 -    val ((_, (_, pool, fact_names, lifted, sym_tab)),
  13.764 -         (output, run_time, used_from, atp_proof, outcome)) =
  13.765 -      with_cleanup clean_up run () |> tap export
  13.766 -    val important_message =
  13.767 -      if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0
  13.768 -      then
  13.769 -        extract_important_message output
  13.770 -      else
  13.771 -        ""
  13.772 -    val (used_facts, preplay, message, message_tail) =
  13.773 -      (case outcome of
  13.774 -        NONE =>
  13.775 -        let
  13.776 -          val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
  13.777 -          val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
  13.778 -          val reconstrs =
  13.779 -            bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof
  13.780 -              o (fn desperate => if desperate then hide_lamsN else default_metis_lam_trans))
  13.781 -        in
  13.782 -          (used_facts,
  13.783 -           Lazy.lazy (fn () =>
  13.784 -             let val used_pairs = used_from |> filter_used_facts false used_facts in
  13.785 -               play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
  13.786 -                 (hd reconstrs) reconstrs
  13.787 -             end),
  13.788 -           fn preplay =>
  13.789 -              let
  13.790 -                val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
  13.791 -                fun isar_params () =
  13.792 -                  let
  13.793 -                    val metis_type_enc =
  13.794 -                      if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
  13.795 -                      else partial_typesN
  13.796 -                    val metis_lam_trans = lam_trans_of_atp_proof atp_proof default_metis_lam_trans
  13.797 -                    val atp_proof =
  13.798 -                      atp_proof
  13.799 -                      |> termify_atp_proof ctxt pool lifted sym_tab
  13.800 -                      |> introduce_spass_skolem
  13.801 -                      |> factify_atp_proof fact_names hyp_ts concl_t
  13.802 -                  in
  13.803 -                    (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
  13.804 -                     try0_isar, atp_proof, goal)
  13.805 -                  end
  13.806 -                val one_line_params =
  13.807 -                  (preplay, proof_banner mode name, used_facts,
  13.808 -                   choose_minimize_command ctxt params minimize_command name preplay,
  13.809 -                   subgoal, subgoal_count)
  13.810 -                val num_chained = length (#facts (Proof.goal state))
  13.811 -              in
  13.812 -                proof_text ctxt debug isar_proofs isar_params num_chained one_line_params
  13.813 -              end,
  13.814 -           (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
  13.815 -           (if important_message <> "" then
  13.816 -              "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
  13.817 -            else
  13.818 -              ""))
  13.819 -        end
  13.820 -      | SOME failure =>
  13.821 -        ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
  13.822 -  in
  13.823 -    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
  13.824 -     preplay = preplay, message = message, message_tail = message_tail}
  13.825 -  end
  13.826 -
  13.827 -(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
  13.828 -   these are sorted out properly in the SMT module, we have to interpret these
  13.829 -   ourselves. *)
  13.830 -val remote_smt_failures =
  13.831 -  [(2, NoLibwwwPerl),
  13.832 -   (22, CantConnect)]
  13.833 -val z3_failures =
  13.834 -  [(101, OutOfResources),
  13.835 -   (103, MalformedInput),
  13.836 -   (110, MalformedInput),
  13.837 -   (112, TimedOut)]
  13.838 -val unix_failures =
  13.839 -  [(138, Crashed),
  13.840 -   (139, Crashed)]
  13.841 -val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
  13.842 -
  13.843 -fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
  13.844 -    if is_real_cex then Unprovable else GaveUp
  13.845 -  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
  13.846 -  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
  13.847 -    (case AList.lookup (op =) smt_failures code of
  13.848 -       SOME failure => failure
  13.849 -     | NONE => UnknownError ("Abnormal termination with exit code " ^
  13.850 -                             string_of_int code ^ "."))
  13.851 -  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
  13.852 -  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
  13.853 -
  13.854 -(* FUDGE *)
  13.855 -val smt_max_slices =
  13.856 -  Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
  13.857 -val smt_slice_fact_frac =
  13.858 -  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac}
  13.859 -                           (K 0.667)
  13.860 -val smt_slice_time_frac =
  13.861 -  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
  13.862 -val smt_slice_min_secs =
  13.863 -  Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
  13.864 -
  13.865 -val is_boring_builtin_typ =
  13.866 -  not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
  13.867 -
  13.868 -fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
  13.869 -      ...} : params) state goal i =
  13.870 -  let
  13.871 -    fun repair_context ctxt =
  13.872 -      ctxt |> select_smt_solver name
  13.873 -           |> Config.put SMT_Config.verbose debug
  13.874 -           |> (if overlord then
  13.875 -                 Config.put SMT_Config.debug_files
  13.876 -                            (overlord_file_location_of_prover name
  13.877 -                             |> (fn (path, name) => path ^ "/" ^ name))
  13.878 -               else
  13.879 -                 I)
  13.880 -           |> Config.put SMT_Config.infer_triggers
  13.881 -                         (Config.get ctxt smt_triggers)
  13.882 -           |> not (Config.get ctxt smt_builtins)
  13.883 -              ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
  13.884 -                 #> Config.put SMT_Config.datatypes false)
  13.885 -           |> repair_monomorph_context max_mono_iters default_max_mono_iters
  13.886 -                  max_new_mono_instances default_max_new_mono_instances
  13.887 -    val state = Proof.map_context (repair_context) state
  13.888 -    val ctxt = Proof.context_of state
  13.889 -    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
  13.890 -    fun do_slice timeout slice outcome0 time_so_far
  13.891 -                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
  13.892 -      let
  13.893 -        val timer = Timer.startRealTimer ()
  13.894 -        val slice_timeout =
  13.895 -          if slice < max_slices then
  13.896 -            let val ms = Time.toMilliseconds timeout in
  13.897 -              Int.min (ms,
  13.898 -                  Int.max (1000 * Config.get ctxt smt_slice_min_secs,
  13.899 -                      Real.ceil (Config.get ctxt smt_slice_time_frac
  13.900 -                                 * Real.fromInt ms)))
  13.901 -              |> Time.fromMilliseconds
  13.902 -            end
  13.903 -          else
  13.904 -            timeout
  13.905 -        val num_facts = length weighted_facts
  13.906 -        val _ =
  13.907 -          if debug then
  13.908 -            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
  13.909 -            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
  13.910 -            |> Output.urgent_message
  13.911 -          else
  13.912 -            ()
  13.913 -        val birth = Timer.checkRealTimer timer
  13.914 -        val _ =
  13.915 -          if debug then Output.urgent_message "Invoking SMT solver..." else ()
  13.916 -        val (outcome, used_facts) =
  13.917 -          SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
  13.918 -          |> SMT_Solver.smt_filter_apply slice_timeout
  13.919 -          |> (fn {outcome, used_facts} => (outcome, used_facts))
  13.920 -          handle exn => if Exn.is_interrupt exn then
  13.921 -                          reraise exn
  13.922 -                        else
  13.923 -                          (ML_Compiler.exn_message exn
  13.924 -                           |> SMT_Failure.Other_Failure |> SOME, [])
  13.925 -        val death = Timer.checkRealTimer timer
  13.926 -        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
  13.927 -        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
  13.928 -        val too_many_facts_perhaps =
  13.929 -          case outcome of
  13.930 -            NONE => false
  13.931 -          | SOME (SMT_Failure.Counterexample _) => false
  13.932 -          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
  13.933 -          | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
  13.934 -          | SOME SMT_Failure.Out_Of_Memory => true
  13.935 -          | SOME (SMT_Failure.Other_Failure _) => true
  13.936 -        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
  13.937 -      in
  13.938 -        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
  13.939 -           Time.> (timeout, Time.zeroTime) then
  13.940 -          let
  13.941 -            val new_num_facts =
  13.942 -              Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
  13.943 -            val weighted_factss as (new_fact_filter, _) :: _ =
  13.944 -              weighted_factss
  13.945 -              |> (fn (x :: xs) => xs @ [x])
  13.946 -              |> app_hd (apsnd (take new_num_facts))
  13.947 -            val show_filter = fact_filter <> new_fact_filter
  13.948 -            fun num_of_facts fact_filter num_facts =
  13.949 -              string_of_int num_facts ^
  13.950 -              (if show_filter then " " ^ quote fact_filter else "") ^
  13.951 -              " fact" ^ plural_s num_facts
  13.952 -            val _ =
  13.953 -              if debug then
  13.954 -                quote name ^ " invoked with " ^
  13.955 -                num_of_facts fact_filter num_facts ^ ": " ^
  13.956 -                string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
  13.957 -                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
  13.958 -                "..."
  13.959 -                |> Output.urgent_message
  13.960 -              else
  13.961 -                ()
  13.962 -          in
  13.963 -            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
  13.964 -          end
  13.965 -        else
  13.966 -          {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
  13.967 -           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
  13.968 -      end
  13.969 -  in
  13.970 -    do_slice timeout 1 NONE Time.zeroTime
  13.971 -  end
  13.972 -
  13.973 -fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
  13.974 -    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
  13.975 -  let
  13.976 -    val ctxt = Proof.context_of state
  13.977 -    fun weight_facts facts =
  13.978 -      let val num_facts = length facts in
  13.979 -        facts ~~ (0 upto num_facts - 1)
  13.980 -        |> map (weight_smt_fact ctxt num_facts)
  13.981 -      end
  13.982 -    val weighted_factss = factss |> map (apsnd weight_facts)
  13.983 -    val {outcome, used_facts = used_pairs, used_from, run_time} =
  13.984 -      smt_filter_loop name params state goal subgoal weighted_factss
  13.985 -    val used_facts = used_pairs |> map fst
  13.986 -    val outcome = outcome |> Option.map failure_of_smt_failure
  13.987 -    val (preplay, message, message_tail) =
  13.988 -      case outcome of
  13.989 -        NONE =>
  13.990 -        (Lazy.lazy (fn () =>
  13.991 -           play_one_line_proof mode debug verbose preplay_timeout used_pairs
  13.992 -               state subgoal SMT
  13.993 -               (bunch_of_reconstructors false (fn desperate =>
  13.994 -                  if desperate then liftingN else default_metis_lam_trans))),
  13.995 -         fn preplay =>
  13.996 -            let
  13.997 -              val one_line_params =
  13.998 -                (preplay, proof_banner mode name, used_facts,
  13.999 -                 choose_minimize_command ctxt params minimize_command name preplay,
 13.1000 -                 subgoal, subgoal_count)
 13.1001 -              val num_chained = length (#facts (Proof.goal state))
 13.1002 -            in
 13.1003 -              one_line_proof_text num_chained one_line_params
 13.1004 -            end,
 13.1005 -         if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
 13.1006 -      | SOME failure =>
 13.1007 -        (Lazy.value (plain_metis, Play_Failed),
 13.1008 -         fn _ => string_of_atp_failure failure, "")
 13.1009 -  in
 13.1010 -    {outcome = outcome, used_facts = used_facts, used_from = used_from,
 13.1011 -     run_time = run_time, preplay = preplay, message = message,
 13.1012 -     message_tail = message_tail}
 13.1013 -  end
 13.1014 -
 13.1015 -fun run_reconstructor mode name
 13.1016 -        (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
 13.1017 -        minimize_command
 13.1018 -        ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...}
 13.1019 -         : prover_problem) =
 13.1020 -  let
 13.1021 -    val reconstr =
 13.1022 -      if name = metisN then
 13.1023 -        Metis (type_enc |> the_default (hd partial_type_encs),
 13.1024 -               lam_trans |> the_default default_metis_lam_trans)
 13.1025 -      else if name = smtN then
 13.1026 -        SMT
 13.1027 -      else
 13.1028 -        raise Fail ("unknown reconstructor: " ^ quote name)
 13.1029 -    val used_facts = facts |> map fst
 13.1030 -  in
 13.1031 -    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
 13.1032 -       state subgoal reconstr [reconstr] of
 13.1033 -      play as (_, Played time) =>
 13.1034 -      {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
 13.1035 -       preplay = Lazy.value play,
 13.1036 -       message =
 13.1037 -         fn play =>
 13.1038 -            let
 13.1039 -              val (_, override_params) = extract_reconstructor params reconstr
 13.1040 -              val one_line_params =
 13.1041 -                (play, proof_banner mode name, used_facts, minimize_command override_params name,
 13.1042 -                 subgoal, subgoal_count)
 13.1043 -              val num_chained = length (#facts (Proof.goal state))
 13.1044 -            in
 13.1045 -              one_line_proof_text num_chained one_line_params
 13.1046 -            end,
 13.1047 -       message_tail = ""}
 13.1048 -    | play =>
 13.1049 -      let
 13.1050 -        val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
 13.1051 -      in
 13.1052 -        {outcome = SOME failure, used_facts = [], used_from = [],
 13.1053 -         run_time = Time.zeroTime, preplay = Lazy.value play,
 13.1054 -         message = fn _ => string_of_atp_failure failure, message_tail = ""}
 13.1055 -      end)
 13.1056 -  end
 13.1057 -
 13.1058 -fun get_prover ctxt mode name =
 13.1059 -  let val thy = Proof_Context.theory_of ctxt in
 13.1060 -    if is_reconstructor name then run_reconstructor mode name
 13.1061 -    else if is_atp thy name then run_atp mode name (get_atp thy name ())
 13.1062 -    else if is_smt_prover ctxt name then run_smt_solver mode name
 13.1063 -    else error ("No such prover: " ^ name ^ ".")
 13.1064 -  end
 13.1065 -
 13.1066 -end;
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jan 31 10:23:32 2014 +0100
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jan 31 10:23:32 2014 +0100
    14.3 @@ -11,8 +11,8 @@
    14.4    type fact = Sledgehammer_Fact.fact
    14.5    type fact_override = Sledgehammer_Fact.fact_override
    14.6    type minimize_command = Sledgehammer_Reconstructor.minimize_command
    14.7 -  type mode = Sledgehammer_Provers.mode
    14.8 -  type params = Sledgehammer_Provers.params
    14.9 +  type mode = Sledgehammer_Prover.mode
   14.10 +  type params = Sledgehammer_Prover.params
   14.11  
   14.12    val someN : string
   14.13    val noneN : string
   14.14 @@ -33,7 +33,7 @@
   14.15  open ATP_Proof_Reconstruct
   14.16  open Sledgehammer_Util
   14.17  open Sledgehammer_Fact
   14.18 -open Sledgehammer_Provers
   14.19 +open Sledgehammer_Prover
   14.20  open Sledgehammer_Minimize
   14.21  open Sledgehammer_MaSh
   14.22