src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
author blanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 42746 7e227e9de779
parent 42740 31334a7b109d
child 42755 4603154a3018
permissions -rw-r--r--
further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Generic prover abstraction for Sledgehammer.
     7 *)
     8 
     9 signature SLEDGEHAMMER_PROVERS =
    10 sig
    11   type failure = ATP_Proof.failure
    12   type locality = Sledgehammer_Filter.locality
    13   type relevance_fudge = Sledgehammer_Filter.relevance_fudge
    14   type translated_formula = Sledgehammer_ATP_Translate.translated_formula
    15   type type_system = Sledgehammer_ATP_Translate.type_system
    16   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
    17 
    18   datatype rich_type_system =
    19     Dumb_Type_Sys of type_system |
    20     Smart_Type_Sys of bool
    21 
    22   type params =
    23     {debug: bool,
    24      verbose: bool,
    25      overlord: bool,
    26      blocking: bool,
    27      provers: string list,
    28      type_sys: rich_type_system,
    29      relevance_thresholds: real * real,
    30      max_relevant: int option,
    31      max_mono_iters: int,
    32      max_new_mono_instances: int,
    33      explicit_apply: bool,
    34      isar_proof: bool,
    35      isar_shrink_factor: int,
    36      slicing: bool,
    37      timeout: Time.time,
    38      expect: string}
    39 
    40   datatype prover_fact =
    41     Untranslated_Fact of (string * locality) * thm |
    42     SMT_Weighted_Fact of (string * locality) * (int option * thm)
    43 
    44   type prover_problem =
    45     {state: Proof.state,
    46      goal: thm,
    47      subgoal: int,
    48      subgoal_count: int,
    49      facts: prover_fact list,
    50      smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
    51 
    52   type prover_result =
    53     {outcome: failure option,
    54      used_facts: (string * locality) list,
    55      run_time_in_msecs: int option,
    56      message: string}
    57 
    58   type prover = params -> minimize_command -> prover_problem -> prover_result
    59 
    60   val smt_triggers : bool Config.T
    61   val smt_weights : bool Config.T
    62   val smt_weight_min_facts : int Config.T
    63   val smt_min_weight : int Config.T
    64   val smt_max_weight : int Config.T
    65   val smt_max_weight_index : int Config.T
    66   val smt_weight_curve : (int -> int) Unsynchronized.ref
    67   val smt_max_slices : int Config.T
    68   val smt_slice_fact_frac : real Config.T
    69   val smt_slice_time_frac : real Config.T
    70   val smt_slice_min_secs : int Config.T
    71   val das_Tool : string
    72   val select_smt_solver : string -> Proof.context -> Proof.context
    73   val is_smt_prover : Proof.context -> string -> bool
    74   val is_prover_supported : Proof.context -> string -> bool
    75   val is_prover_installed : Proof.context -> string -> bool
    76   val default_max_relevant_for_prover : Proof.context -> bool -> string -> int
    77   val is_built_in_const_for_prover :
    78     Proof.context -> string -> string * typ -> term list -> bool * term list
    79   val atp_relevance_fudge : relevance_fudge
    80   val smt_relevance_fudge : relevance_fudge
    81   val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
    82   val dest_dir : string Config.T
    83   val problem_prefix : string Config.T
    84   val measure_run_time : bool Config.T
    85   val weight_smt_fact :
    86     Proof.context -> int -> ((string * locality) * thm) * int
    87     -> (string * locality) * (int option * thm)
    88   val untranslated_fact : prover_fact -> (string * locality) * thm
    89   val smt_weighted_fact :
    90     Proof.context -> int -> prover_fact * int
    91     -> (string * locality) * (int option * thm)
    92   val supported_provers : Proof.context -> unit
    93   val kill_provers : unit -> unit
    94   val running_provers : unit -> unit
    95   val messages : int option -> unit
    96   val get_prover : Proof.context -> bool -> string -> prover
    97 end;
    98 
    99 structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
   100 struct
   101 
   102 open ATP_Problem
   103 open ATP_Proof
   104 open ATP_Systems
   105 open Metis_Translate
   106 open Sledgehammer_Util
   107 open Sledgehammer_Filter
   108 open Sledgehammer_ATP_Translate
   109 open Sledgehammer_ATP_Reconstruct
   110 
   111 (** The Sledgehammer **)
   112 
   113 (* Identifier to distinguish Sledgehammer from other tools using
   114    "Async_Manager". *)
   115 val das_Tool = "Sledgehammer"
   116 
   117 val select_smt_solver =
   118   Context.proof_map o SMT_Config.select_solver
   119 
   120 fun is_smt_prover ctxt name =
   121   member (op =) (SMT_Solver.available_solvers_of ctxt) name
   122 
   123 fun is_prover_supported ctxt name =
   124   let val thy = Proof_Context.theory_of ctxt in
   125     is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name
   126   end
   127 
   128 fun is_prover_installed ctxt =
   129   is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
   130 
   131 fun get_slices slicing slices =
   132   (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
   133 
   134 fun default_max_relevant_for_prover ctxt slicing name =
   135   let val thy = Proof_Context.theory_of ctxt in
   136     if is_smt_prover ctxt name then
   137       SMT_Solver.default_max_relevant ctxt name
   138     else
   139       fold (Integer.max o fst o snd o snd o snd)
   140            (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
   141   end
   142 
   143 (* These are either simplified away by "Meson.presimplify" (most of the time) or
   144    handled specially via "fFalse", "fTrue", ..., "fequal". *)
   145 val atp_irrelevant_consts =
   146   [@{const_name False}, @{const_name True}, @{const_name Not},
   147    @{const_name conj}, @{const_name disj}, @{const_name implies},
   148    @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
   149 
   150 fun is_built_in_const_for_prover ctxt name =
   151   if is_smt_prover ctxt name then
   152     let val ctxt = ctxt |> select_smt_solver name in
   153       fn x => fn ts =>
   154          if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then
   155            (true, [])
   156          else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then
   157            (true, ts)
   158          else
   159            (false, ts)
   160     end
   161   else
   162     fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts s, ts)
   163 
   164 (* FUDGE *)
   165 val atp_relevance_fudge =
   166   {local_const_multiplier = 1.5,
   167    worse_irrel_freq = 100.0,
   168    higher_order_irrel_weight = 1.05,
   169    abs_rel_weight = 0.5,
   170    abs_irrel_weight = 2.0,
   171    skolem_irrel_weight = 0.25,
   172    theory_const_rel_weight = 0.5,
   173    theory_const_irrel_weight = 0.25,
   174    chained_const_irrel_weight = 0.25,
   175    intro_bonus = 0.15,
   176    elim_bonus = 0.15,
   177    simp_bonus = 0.15,
   178    local_bonus = 0.55,
   179    assum_bonus = 1.05,
   180    chained_bonus = 1.5,
   181    max_imperfect = 11.5,
   182    max_imperfect_exp = 1.0,
   183    threshold_divisor = 2.0,
   184    ridiculous_threshold = 0.01}
   185 
   186 (* FUDGE (FIXME) *)
   187 val smt_relevance_fudge =
   188   {local_const_multiplier = #local_const_multiplier atp_relevance_fudge,
   189    worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
   190    higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
   191    abs_rel_weight = #abs_rel_weight atp_relevance_fudge,
   192    abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,
   193    skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,
   194    theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,
   195    theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,
   196    chained_const_irrel_weight = #chained_const_irrel_weight atp_relevance_fudge,
   197    intro_bonus = #intro_bonus atp_relevance_fudge,
   198    elim_bonus = #elim_bonus atp_relevance_fudge,
   199    simp_bonus = #simp_bonus atp_relevance_fudge,
   200    local_bonus = #local_bonus atp_relevance_fudge,
   201    assum_bonus = #assum_bonus atp_relevance_fudge,
   202    chained_bonus = #chained_bonus atp_relevance_fudge,
   203    max_imperfect = #max_imperfect atp_relevance_fudge,
   204    max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge,
   205    threshold_divisor = #threshold_divisor atp_relevance_fudge,
   206    ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
   207 
   208 fun relevance_fudge_for_prover ctxt name =
   209   if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
   210 
   211 fun supported_provers ctxt =
   212   let
   213     val thy = Proof_Context.theory_of ctxt
   214     val (remote_provers, local_provers) =
   215       sort_strings (supported_atps thy) @
   216       sort_strings (SMT_Solver.available_solvers_of ctxt)
   217       |> List.partition (String.isPrefix remote_prefix)
   218   in
   219     Output.urgent_message ("Supported provers: " ^
   220                            commas (local_provers @ remote_provers) ^ ".")
   221   end
   222 
   223 fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
   224 fun running_provers () = Async_Manager.running_threads das_Tool "provers"
   225 val messages = Async_Manager.thread_messages das_Tool "prover"
   226 
   227 (** problems, results, ATPs, etc. **)
   228 
   229 datatype rich_type_system =
   230   Dumb_Type_Sys of type_system |
   231   Smart_Type_Sys of bool
   232 
   233 type params =
   234   {debug: bool,
   235    verbose: bool,
   236    overlord: bool,
   237    blocking: bool,
   238    provers: string list,
   239    type_sys: rich_type_system,
   240    relevance_thresholds: real * real,
   241    max_relevant: int option,
   242    max_mono_iters: int,
   243    max_new_mono_instances: int,
   244    explicit_apply: bool,
   245    isar_proof: bool,
   246    isar_shrink_factor: int,
   247    slicing: bool,
   248    timeout: Time.time,
   249    expect: string}
   250 
   251 datatype prover_fact =
   252   Untranslated_Fact of (string * locality) * thm |
   253   SMT_Weighted_Fact of (string * locality) * (int option * thm)
   254 
   255 type prover_problem =
   256   {state: Proof.state,
   257    goal: thm,
   258    subgoal: int,
   259    subgoal_count: int,
   260    facts: prover_fact list,
   261    smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
   262 
   263 type prover_result =
   264   {outcome: failure option,
   265    message: string,
   266    used_facts: (string * locality) list,
   267    run_time_in_msecs: int option}
   268 
   269 type prover = params -> minimize_command -> prover_problem -> prover_result
   270 
   271 (* configuration attributes *)
   272 
   273 val dest_dir =
   274   Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
   275   (* Empty string means create files in Isabelle's temporary files directory. *)
   276 
   277 val problem_prefix =
   278   Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
   279 
   280 val measure_run_time =
   281   Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
   282 
   283 fun with_path cleanup after f path =
   284   Exn.capture f path
   285   |> tap (fn _ => cleanup path)
   286   |> Exn.release
   287   |> tap (after path)
   288 
   289 fun proof_banner auto =
   290   if auto then "Auto Sledgehammer found a proof" else "Try this command"
   291 
   292 val smt_triggers =
   293   Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
   294 val smt_weights =
   295   Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
   296 val smt_weight_min_facts =
   297   Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
   298 
   299 (* FUDGE *)
   300 val smt_min_weight =
   301   Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
   302 val smt_max_weight =
   303   Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
   304 val smt_max_weight_index =
   305   Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
   306 val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
   307 
   308 fun smt_fact_weight ctxt j num_facts =
   309   if Config.get ctxt smt_weights andalso
   310      num_facts >= Config.get ctxt smt_weight_min_facts then
   311     let
   312       val min = Config.get ctxt smt_min_weight
   313       val max = Config.get ctxt smt_max_weight
   314       val max_index = Config.get ctxt smt_max_weight_index
   315       val curve = !smt_weight_curve
   316     in
   317       SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
   318             div curve max_index)
   319     end
   320   else
   321     NONE
   322 
   323 fun weight_smt_fact ctxt num_facts ((info, th), j) =
   324   let val thy = Proof_Context.theory_of ctxt in
   325     (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
   326   end
   327 
   328 fun untranslated_fact (Untranslated_Fact p) = p
   329   | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
   330 fun atp_translated_fact ctxt fact =
   331   translate_atp_fact ctxt false (untranslated_fact fact)
   332 fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
   333   | smt_weighted_fact ctxt num_facts (fact, j) =
   334     (untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts
   335 
   336 fun overlord_file_location_for_prover prover =
   337   (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   338 
   339 
   340 (* generic TPTP-based ATPs *)
   341 
   342 (* Too general means, positive equality literal with a variable X as one
   343    operand, when X does not occur properly in the other operand. This rules out
   344    clearly inconsistent facts such as X = a | X = b, though it by no means
   345    guarantees soundness. *)
   346 
   347 (* Unwanted equalities are those between a (bound or schematic) variable that
   348    does not properly occur in the second operand. *)
   349 val is_exhaustive_finite =
   350   let
   351     fun is_bad_equal (Var z) t =
   352         not (exists_subterm (fn Var z' => z = z' | _ => false) t)
   353       | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
   354       | is_bad_equal _ _ = false
   355     fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
   356     fun do_formula pos t =
   357       case (pos, t) of
   358         (_, @{const Trueprop} $ t1) => do_formula pos t1
   359       | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
   360         do_formula pos t'
   361       | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
   362         do_formula pos t'
   363       | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
   364         do_formula pos t'
   365       | (_, @{const "==>"} $ t1 $ t2) =>
   366         do_formula (not pos) t1 andalso
   367         (t2 = @{prop False} orelse do_formula pos t2)
   368       | (_, @{const HOL.implies} $ t1 $ t2) =>
   369         do_formula (not pos) t1 andalso
   370         (t2 = @{const False} orelse do_formula pos t2)
   371       | (_, @{const Not} $ t1) => do_formula (not pos) t1
   372       | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   373       | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   374       | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
   375       | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
   376       | _ => false
   377   in do_formula true end
   378 
   379 fun has_bound_or_var_of_type pred =
   380   exists_subterm (fn Var (_, T as Type _) => pred T
   381                    | Abs (_, T as Type _, _) => pred T
   382                    | _ => false)
   383 
   384 (* Facts are forbidden to contain variables of these types. The typical reason
   385    is that they lead to unsoundness. Note that "unit" satisfies numerous
   386    equations like "?x = ()". The resulting clauses will have no type constraint,
   387    yielding false proofs. Even "bool" leads to many unsound proofs, though only
   388    for higher-order problems. *)
   389 
   390 (* Facts containing variables of type "unit" or "bool" or of the form
   391    "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
   392    are omitted. *)
   393 fun is_dangerous_term ctxt =
   394   transform_elim_term
   395   #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
   396       is_exhaustive_finite)
   397 
   398 fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
   399   | int_opt_add _ _ = NONE
   400 
   401 val atp_blacklist_max_iters = 10
   402 (* Important messages are important but not so important that users want to see
   403    them each time. *)
   404 val atp_important_message_keep_quotient = 10
   405 
   406 val fallback_best_type_systems =
   407   [Preds (Polymorphic, Const_Arg_Types),
   408    Preds (Mangled_Monomorphic, Nonmonotonic_Types)]
   409 
   410 fun adjust_dumb_type_sys formats (Simple_Types level) =
   411     if member (op =) formats Tff then (Tff, Simple_Types level)
   412     else (Fof, Preds (Mangled_Monomorphic, level))
   413   | adjust_dumb_type_sys formats type_sys = (hd formats, type_sys)
   414 fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
   415     adjust_dumb_type_sys formats type_sys
   416   | determine_format_and_type_sys best_type_systems formats
   417                                   (Smart_Type_Sys full_types) =
   418     map type_sys_from_string best_type_systems @ fallback_best_type_systems
   419     |> find_first (if full_types then is_type_sys_virtually_sound else K true)
   420     |> the |> adjust_dumb_type_sys formats
   421 
   422 fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
   423   Config.put SMT_Config.verbose debug
   424   #> Config.put SMT_Config.monomorph_full false
   425   #> Config.put SMT_Config.monomorph_limit max_mono_iters
   426   #> Config.put SMT_Config.monomorph_instances max_mono_instances
   427 
   428 fun run_atp auto name
   429         ({exec, required_execs, arguments, proof_delims, known_failures,
   430           conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
   431         ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
   432           max_new_mono_instances, explicit_apply, isar_proof,
   433           isar_shrink_factor, slicing, timeout, ...} : params)
   434         minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   435   let
   436     val thy = Proof.theory_of state
   437     val ctxt = Proof.context_of state
   438     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
   439     val (dest_dir, problem_prefix) =
   440       if overlord then overlord_file_location_for_prover name
   441       else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
   442     val problem_file_name =
   443       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
   444                   "_" ^ string_of_int subgoal)
   445     val problem_path_name =
   446       if dest_dir = "" then
   447         File.tmp_path problem_file_name
   448       else if File.exists (Path.explode dest_dir) then
   449         Path.append (Path.explode dest_dir) problem_file_name
   450       else
   451         error ("No such directory: " ^ quote dest_dir ^ ".")
   452     val measure_run_time = verbose orelse Config.get ctxt measure_run_time
   453     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
   454     fun split_time s =
   455       let
   456         val split = String.tokens (fn c => str c = "\n")
   457         val (output, t) = s |> split |> split_last |> apfst cat_lines
   458         fun as_num f = f >> (fst o read_int)
   459         val num = as_num (Scan.many1 Symbol.is_ascii_digit)
   460         val digit = Scan.one Symbol.is_ascii_digit
   461         val num3 = as_num (digit ::: digit ::: (digit >> single))
   462         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
   463         val as_time = Scan.read Symbol.stopper time o raw_explode
   464       in (output, as_time t) end
   465     fun run_on prob_file =
   466       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
   467         (home_var, _) :: _ =>
   468         error ("The environment variable " ^ quote home_var ^ " is not set.")
   469       | [] =>
   470         if File.exists command then
   471           let
   472             (* If slicing is disabled, we expand the last slice to fill the
   473                entire time available. *)
   474             val actual_slices = get_slices slicing (best_slices ctxt)
   475             val num_actual_slices = length actual_slices
   476             fun monomorphize_facts facts =
   477               let
   478                 val facts = facts |> map untranslated_fact
   479                 (* pseudo-theorem involving the same constants as the subgoal *)
   480                 val subgoal_th =
   481                   Logic.list_implies (hyp_ts, concl_t)
   482                   |> Skip_Proof.make_thm thy
   483                 val indexed_facts =
   484                   (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
   485                 val max_mono_instances = max_new_mono_instances + length facts
   486               in
   487                 ctxt |> repair_smt_monomorph_context debug max_mono_iters
   488                                                      max_mono_instances
   489                      |> SMT_Monomorph.monomorph indexed_facts
   490                      |> fst |> sort (int_ord o pairself fst)
   491                      |> filter_out (curry (op =) ~1 o fst)
   492 (* FIXME:            |> take max_mono_instances (* just in case *) *)
   493                      |> map (Untranslated_Fact o apfst (fst o nth facts))
   494               end
   495             fun run_slice blacklist (slice, (time_frac, (complete,
   496                                        (best_max_relevant, best_type_systems))))
   497                           time_left =
   498               let
   499                 val num_facts =
   500                   length facts |> is_none max_relevant
   501                                   ? Integer.min best_max_relevant
   502                 val (format, type_sys) =
   503                   determine_format_and_type_sys best_type_systems formats type_sys
   504                 val fairly_sound = is_type_sys_fairly_sound type_sys
   505                 val facts =
   506                   facts |> not fairly_sound
   507                            ? filter_out (is_dangerous_term ctxt o prop_of o snd
   508                                          o untranslated_fact)
   509                         |> take num_facts
   510                         |> not (null blacklist)
   511                            ? filter_out (member (op =) blacklist o fst
   512                                          o untranslated_fact)
   513                         |> polymorphism_of_type_sys type_sys <> Polymorphic
   514                            ? monomorphize_facts
   515                         |> map (atp_translated_fact ctxt)
   516                 val real_ms = Real.fromInt o Time.toMilliseconds
   517                 val slice_timeout =
   518                   ((real_ms time_left
   519                     |> (if slice < num_actual_slices - 1 then
   520                           curry Real.min (time_frac * real_ms timeout)
   521                         else
   522                           I))
   523                    * 0.001) |> seconds
   524                 val _ =
   525                   if debug then
   526                     quote name ^ " slice #" ^ string_of_int (slice + 1) ^
   527                     " with " ^ string_of_int num_facts ^ " fact" ^
   528                     plural_s num_facts ^ " for " ^
   529                     string_from_time slice_timeout ^ "..."
   530                     |> Output.urgent_message
   531                   else
   532                     ()
   533                 val (atp_problem, pool, conjecture_offset, facts_offset,
   534                      fact_names) =
   535                   prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys
   536                                       explicit_apply hyp_ts concl_t facts
   537                 fun weights () = atp_problem_weights atp_problem
   538                 val core =
   539                   File.shell_path command ^ " " ^
   540                   arguments ctxt slice slice_timeout weights ^ " " ^
   541                   File.shell_path prob_file
   542                 val command =
   543                   (if measure_run_time then
   544                      "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
   545                    else
   546                      "exec " ^ core) ^ " 2>&1"
   547                 val _ =
   548                   atp_problem
   549                   |> tptp_strings_for_atp_problem format
   550                   |> cons ("% " ^ command ^ "\n")
   551                   |> File.write_list prob_file
   552                 val conjecture_shape =
   553                   conjecture_offset + 1
   554                     upto conjecture_offset + length hyp_ts + 1
   555                   |> map single
   556                 val ((output, msecs), res_code) =
   557                   bash_output command
   558                   |>> (if overlord then
   559                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   560                        else
   561                          I)
   562                   |>> (if measure_run_time then split_time else rpair NONE)
   563                 val (atp_proof, outcome) =
   564                   extract_tstplike_proof_and_outcome debug verbose complete
   565                       res_code proof_delims known_failures output
   566                   |>> atp_proof_from_tstplike_proof
   567                 val (conjecture_shape, facts_offset, fact_names) =
   568                   if is_none outcome then
   569                     repair_conjecture_shape_and_fact_names type_sys output
   570                         conjecture_shape facts_offset fact_names
   571                   else
   572                     (* don't bother repairing *)
   573                     (conjecture_shape, facts_offset, fact_names)
   574                 val outcome =
   575                   case outcome of
   576                     NONE =>
   577                     if is_unsound_proof type_sys conjecture_shape facts_offset
   578                                         fact_names atp_proof then
   579                       SOME (UnsoundProof (is_type_sys_virtually_sound type_sys))
   580                     else
   581                       NONE
   582                   | SOME Unprovable =>
   583                     if null blacklist then outcome
   584                     else SOME IncompleteUnprovable
   585                   | _ => outcome
   586               in
   587                 ((pool, conjecture_shape, facts_offset, fact_names),
   588                  (output, msecs, type_sys, atp_proof, outcome))
   589               end
   590             val timer = Timer.startRealTimer ()
   591             fun maybe_run_slice blacklist slice
   592                                 (result as (_, (_, msecs0, _, _, SOME _))) =
   593                 let
   594                   val time_left = Time.- (timeout, Timer.checkRealTimer timer)
   595                 in
   596                   if Time.<= (time_left, Time.zeroTime) then
   597                     result
   598                   else
   599                     (run_slice blacklist slice time_left
   600                      |> (fn (stuff, (output, msecs, type_sys, atp_proof,
   601                                      outcome)) =>
   602                             (stuff, (output, int_opt_add msecs0 msecs, type_sys,
   603                                      atp_proof, outcome))))
   604                 end
   605               | maybe_run_slice _ _ result = result
   606             fun maybe_blacklist_facts_and_retry iter blacklist
   607                     (result as ((_, _, facts_offset, fact_names),
   608                                 (_, _, type_sys, atp_proof,
   609                                  SOME (UnsoundProof false)))) =
   610                 (case used_facts_in_atp_proof type_sys facts_offset fact_names
   611                                               atp_proof of
   612                    [] => result
   613                  | new_baddies =>
   614                    let val blacklist = new_baddies @ blacklist in
   615                      result
   616                      |> maybe_run_slice blacklist (List.last actual_slices)
   617                      |> iter < atp_blacklist_max_iters
   618                         ? maybe_blacklist_facts_and_retry (iter + 1) blacklist
   619                    end)
   620               | maybe_blacklist_facts_and_retry _ _ result = result
   621           in
   622             ((Symtab.empty, [], 0, Vector.fromList []),
   623              ("", SOME 0, hd fallback_best_type_systems, [],
   624               SOME InternalError))
   625             |> fold (maybe_run_slice []) actual_slices
   626                (* The ATP found an unsound proof? Automatically try again
   627                   without the offending facts! *)
   628             |> maybe_blacklist_facts_and_retry 0 []
   629           end
   630         else
   631           error ("Bad executable: " ^ Path.print command ^ ".")
   632 
   633     (* If the problem file has not been exported, remove it; otherwise, export
   634        the proof file too. *)
   635     fun cleanup prob_file =
   636       if dest_dir = "" then try File.rm prob_file else NONE
   637     fun export prob_file (_, (output, _, _, _, _)) =
   638       if dest_dir = "" then
   639         ()
   640       else
   641         File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
   642     val ((pool, conjecture_shape, facts_offset, fact_names),
   643          (output, msecs, type_sys, atp_proof, outcome)) =
   644       with_path cleanup export run_on problem_path_name
   645     val important_message =
   646       if not auto andalso
   647          random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
   648         extract_important_message output
   649       else
   650         ""
   651     fun append_to_message message =
   652       message ^
   653       (if verbose then
   654          "\nATP real CPU time: " ^
   655          string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
   656        else
   657          "") ^
   658       (if important_message <> "" then
   659          "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
   660        else
   661          "")
   662     val isar_params = (ctxt, debug, isar_shrink_factor, pool, conjecture_shape)
   663     val metis_params =
   664       (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset,
   665        fact_names, goal, subgoal)
   666     val (outcome, (message, used_facts)) =
   667       case outcome of
   668         NONE =>
   669         (NONE, proof_text isar_proof isar_params metis_params
   670                |>> append_to_message)
   671       | SOME ProofMissing =>
   672         (NONE, metis_proof_text metis_params |>> append_to_message)
   673       | SOME failure => (outcome, (string_for_failure failure, []))
   674   in
   675     {outcome = outcome, message = message, used_facts = used_facts,
   676      run_time_in_msecs = msecs}
   677   end
   678 
   679 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
   680    these are sorted out properly in the SMT module, we have to interpret these
   681    ourselves. *)
   682 val remote_smt_failures =
   683   [(22, CantConnect),
   684    (2, NoLibwwwPerl)]
   685 val z3_wrapper_failures =
   686   [(10, NoRealZ3),
   687    (11, InternalError),
   688    (12, InternalError),
   689    (13, InternalError)]
   690 val z3_failures =
   691   [(101, OutOfResources),
   692    (103, MalformedInput),
   693    (110, MalformedInput)]
   694 val unix_failures =
   695   [(139, Crashed)]
   696 val smt_failures =
   697   remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
   698 
   699 fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
   700     if is_real_cex then Unprovable else IncompleteUnprovable
   701   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   702   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
   703     (case AList.lookup (op =) smt_failures code of
   704        SOME failure => failure
   705      | NONE => UnknownError ("Abnormal termination with exit code " ^
   706                              string_of_int code ^ "."))
   707   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   708   | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
   709     UnknownError msg
   710 
   711 (* FUDGE *)
   712 val smt_max_slices =
   713   Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
   714 val smt_slice_fact_frac =
   715   Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.5)
   716 val smt_slice_time_frac =
   717   Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.5)
   718 val smt_slice_min_secs =
   719   Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)
   720 
   721 fun smt_filter_loop ctxt name
   722                     ({debug, verbose, overlord, max_mono_iters,
   723                       max_new_mono_instances, timeout, slicing, ...} : params)
   724                     state i smt_filter =
   725   let
   726     val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
   727     val repair_context =
   728           select_smt_solver name
   729           #> (if overlord then
   730                 Config.put SMT_Config.debug_files
   731                            (overlord_file_location_for_prover name
   732                             |> (fn (path, name) => path ^ "/" ^ name))
   733               else
   734                 I)
   735           #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
   736     val state = state |> Proof.map_context repair_context
   737     fun do_slice timeout slice outcome0 time_so_far facts =
   738       let
   739         val timer = Timer.startRealTimer ()
   740         val state =
   741           state |> Proof.map_context
   742                        (repair_smt_monomorph_context debug max_mono_iters
   743                             (max_new_mono_instances + length facts))
   744         val ms = timeout |> Time.toMilliseconds
   745         val slice_timeout =
   746           if slice < max_slices then
   747             Int.min (ms,
   748                 Int.max (1000 * Config.get ctxt smt_slice_min_secs,
   749                     Real.ceil (Config.get ctxt smt_slice_time_frac
   750                                * Real.fromInt ms)))
   751             |> Time.fromMilliseconds
   752           else
   753             timeout
   754         val num_facts = length facts
   755         val _ =
   756           if debug then
   757             quote name ^ " slice " ^ string_of_int slice ^ " with " ^
   758             string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^
   759             string_from_time slice_timeout ^ "..."
   760             |> Output.urgent_message
   761           else
   762             ()
   763         val birth = Timer.checkRealTimer timer
   764         val _ =
   765           if debug then Output.urgent_message "Invoking SMT solver..." else ()
   766         val (outcome, used_facts) =
   767           (case (slice, smt_filter) of
   768              (1, SOME head) => head |> apsnd (apsnd repair_context)
   769            | _ => SMT_Solver.smt_filter_preprocess state facts i)
   770           |> SMT_Solver.smt_filter_apply slice_timeout
   771           |> (fn {outcome, used_facts} => (outcome, used_facts))
   772           handle exn => if Exn.is_interrupt exn then
   773                           reraise exn
   774                         else
   775                           (ML_Compiler.exn_message exn
   776                            |> SMT_Failure.Other_Failure |> SOME, [])
   777         val death = Timer.checkRealTimer timer
   778         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   779         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
   780         val too_many_facts_perhaps =
   781           case outcome of
   782             NONE => false
   783           | SOME (SMT_Failure.Counterexample _) => false
   784           | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
   785           | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
   786           | SOME SMT_Failure.Out_Of_Memory => true
   787           | SOME (SMT_Failure.Other_Failure _) => true
   788         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   789       in
   790         if too_many_facts_perhaps andalso slice < max_slices andalso
   791            num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
   792           let
   793             val new_num_facts =
   794               Real.ceil (Config.get ctxt smt_slice_fact_frac
   795                          * Real.fromInt num_facts)
   796             val _ =
   797               if verbose andalso is_some outcome then
   798                 quote name ^ " invoked with " ^ string_of_int num_facts ^
   799                 " fact" ^ plural_s num_facts ^ ": " ^
   800                 string_for_failure (failure_from_smt_failure (the outcome)) ^
   801                 " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^
   802                 plural_s new_num_facts ^ "..."
   803                 |> Output.urgent_message
   804               else
   805                 ()
   806           in
   807             facts |> take new_num_facts
   808                   |> do_slice timeout (slice + 1) outcome0 time_so_far
   809           end
   810         else
   811           {outcome = if is_none outcome then NONE else the outcome0,
   812            used_facts = used_facts,
   813            run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)}
   814       end
   815   in do_slice timeout 1 NONE Time.zeroTime end
   816 
   817 (* taken from "Mirabelle" and generalized *)
   818 fun can_apply timeout tac state i =
   819   let
   820     val {context = ctxt, facts, goal} = Proof.goal state
   821     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   822   in
   823     case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
   824       SOME (SOME _) => true
   825     | _ => false
   826   end
   827 
   828 val smt_metis_timeout = seconds 1.0
   829 
   830 fun can_apply_metis debug state i ths =
   831   can_apply smt_metis_timeout
   832             (Config.put Metis_Tactics.verbose debug
   833              #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
   834 
   835 fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command
   836                    ({state, subgoal, subgoal_count, facts, smt_filter, ...}
   837                     : prover_problem) =
   838   let
   839     val ctxt = Proof.context_of state
   840     val num_facts = length facts
   841     val facts = facts ~~ (0 upto num_facts - 1)
   842                 |> map (smt_weighted_fact ctxt num_facts)
   843     val {outcome, used_facts, run_time_in_msecs} =
   844       smt_filter_loop ctxt name params state subgoal smt_filter facts
   845     val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
   846     val outcome = outcome |> Option.map failure_from_smt_failure
   847     val message =
   848       case outcome of
   849         NONE =>
   850         let
   851           val (method, settings) =
   852             if can_apply_metis debug state subgoal (map snd used_facts) then
   853               ("metis", "")
   854             else
   855               ("smt", if name = SMT_Solver.solver_name_of ctxt then ""
   856                       else "smt_solver = " ^ maybe_quote name)
   857         in
   858           try_command_line (proof_banner auto)
   859               (apply_on_subgoal settings subgoal subgoal_count ^
   860                command_call method (map fst other_lemmas)) ^
   861           minimize_line minimize_command
   862                         (map fst (other_lemmas @ chained_lemmas)) ^
   863           (if verbose then
   864              "\nSMT solver real CPU time: " ^
   865              string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^
   866              "."
   867            else
   868              "")
   869         end
   870       | SOME failure => string_for_failure failure
   871   in
   872     {outcome = outcome, used_facts = map fst used_facts,
   873      run_time_in_msecs = run_time_in_msecs, message = message}
   874   end
   875 
   876 fun get_prover ctxt auto name =
   877   let val thy = Proof_Context.theory_of ctxt in
   878     if is_smt_prover ctxt name then
   879       run_smt_solver auto name
   880     else if member (op =) (supported_atps thy) name then
   881       run_atp auto name (get_atp thy name)
   882     else
   883       error ("No such prover: " ^ name ^ ".")
   884   end
   885 
   886 end;