src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
author blanchet
Fri Dec 17 00:27:40 2010 +0100 (2010-12-17 ago)
changeset 41222 f9783376d9b1
parent 41220 4d11b0de7dd8
child 41236 def0a3013554
permissions -rw-r--r--
more precise/correct SMT error handling
     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   type params =
    19     {debug: bool,
    20      verbose: bool,
    21      overlord: bool,
    22      blocking: bool,
    23      provers: string list,
    24      type_sys: type_system,
    25      explicit_apply: bool,
    26      relevance_thresholds: real * real,
    27      max_relevant: int option,
    28      isar_proof: bool,
    29      isar_shrink_factor: int,
    30      timeout: Time.time,
    31      expect: string}
    32 
    33   datatype prover_fact =
    34     Untranslated_Fact of (string * locality) * thm |
    35     ATP_Translated_Fact of
    36       translated_formula option * ((string * locality) * thm)
    37 
    38   type prover_problem =
    39     {state: Proof.state,
    40      goal: thm,
    41      subgoal: int,
    42      subgoal_count: int,
    43      facts: prover_fact list}
    44 
    45   type prover_result =
    46     {outcome: failure option,
    47      used_facts: (string * locality) list,
    48      run_time_in_msecs: int option,
    49      message: string}
    50 
    51   type prover = params -> minimize_command -> prover_problem -> prover_result
    52 
    53   (* for experimentation purposes -- do not use in production code *)
    54   val smt_max_iters : int Unsynchronized.ref
    55   val smt_iter_fact_frac : real Unsynchronized.ref
    56   val smt_iter_time_frac : real Unsynchronized.ref
    57   val smt_iter_min_msecs : int Unsynchronized.ref
    58   val smt_monomorph_limit : int Unsynchronized.ref
    59   val smt_weights : bool Unsynchronized.ref
    60   val smt_min_weight : int Unsynchronized.ref
    61   val smt_max_weight : int Unsynchronized.ref
    62   val smt_max_index : int Unsynchronized.ref
    63   val smt_weight_curve : (int -> int) Unsynchronized.ref
    64 
    65   val das_Tool : string
    66   val is_smt_prover : Proof.context -> string -> bool
    67   val is_prover_available : Proof.context -> string -> bool
    68   val is_prover_installed : Proof.context -> string -> bool
    69   val default_max_relevant_for_prover : Proof.context -> string -> int
    70   val is_built_in_const_for_prover :
    71     Proof.context -> string -> string * typ -> term list -> bool
    72   val atp_relevance_fudge : relevance_fudge
    73   val smt_relevance_fudge : relevance_fudge
    74   val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
    75   val dest_dir : string Config.T
    76   val problem_prefix : string Config.T
    77   val measure_run_time : bool Config.T
    78   val untranslated_fact : prover_fact -> (string * locality) * thm
    79   val available_provers : Proof.context -> unit
    80   val kill_provers : unit -> unit
    81   val running_provers : unit -> unit
    82   val messages : int option -> unit
    83   val get_prover : Proof.context -> bool -> string -> prover
    84   val setup : theory -> theory
    85 end;
    86 
    87 structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
    88 struct
    89 
    90 open ATP_Problem
    91 open ATP_Proof
    92 open ATP_Systems
    93 open Metis_Translate
    94 open Sledgehammer_Util
    95 open Sledgehammer_Filter
    96 open Sledgehammer_ATP_Translate
    97 open Sledgehammer_ATP_Reconstruct
    98 
    99 (** The Sledgehammer **)
   100 
   101 (* Identifier to distinguish Sledgehammer from other tools using
   102    "Async_Manager". *)
   103 val das_Tool = "Sledgehammer"
   104 
   105 fun is_smt_prover ctxt name =
   106   let val smts = SMT_Solver.available_solvers_of ctxt in
   107     case try (unprefix remote_prefix) name of
   108       SOME suffix => member (op =) smts suffix andalso
   109                      SMT_Solver.is_remotely_available ctxt suffix
   110     | NONE => member (op =) smts name
   111   end
   112 
   113 fun is_prover_available ctxt name =
   114   let val thy = ProofContext.theory_of ctxt in
   115     is_smt_prover ctxt name orelse member (op =) (available_atps thy) name
   116   end
   117 
   118 fun is_prover_installed ctxt name =
   119   let val thy = ProofContext.theory_of ctxt in
   120     if is_smt_prover ctxt name then
   121       String.isPrefix remote_prefix name orelse
   122       SMT_Solver.is_locally_installed ctxt name
   123     else
   124       is_atp_installed thy name
   125   end
   126 
   127 fun available_smt_solvers ctxt =
   128   let val smts = SMT_Solver.available_solvers_of ctxt in
   129     smts @ map (prefix remote_prefix)
   130                (filter (SMT_Solver.is_remotely_available ctxt) smts)
   131   end
   132 
   133 fun default_max_relevant_for_prover ctxt name =
   134   let val thy = ProofContext.theory_of ctxt in
   135     if is_smt_prover ctxt name then
   136       SMT_Solver.default_max_relevant ctxt
   137           (perhaps (try (unprefix remote_prefix)) name)
   138     else
   139       #default_max_relevant (get_atp thy name)
   140   end
   141 
   142 (* These are either simplified away by "Meson.presimplify" (most of the time) or
   143    handled specially via "fFalse", "fTrue", ..., "fequal". *)
   144 val atp_irrelevant_consts =
   145   [@{const_name False}, @{const_name True}, @{const_name Not},
   146    @{const_name conj}, @{const_name disj}, @{const_name implies},
   147    @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
   148 
   149 fun is_built_in_const_for_prover ctxt name (s, T) args =
   150   if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args
   151   else member (op =) atp_irrelevant_consts s
   152 
   153 (* FUDGE *)
   154 val atp_relevance_fudge =
   155   {allow_ext = true,
   156    worse_irrel_freq = 100.0,
   157    higher_order_irrel_weight = 1.05,
   158    abs_rel_weight = 0.5,
   159    abs_irrel_weight = 2.0,
   160    skolem_irrel_weight = 0.75,
   161    theory_const_rel_weight = 0.5,
   162    theory_const_irrel_weight = 0.25,
   163    intro_bonus = 0.15,
   164    elim_bonus = 0.15,
   165    simp_bonus = 0.15,
   166    local_bonus = 0.55,
   167    assum_bonus = 1.05,
   168    chained_bonus = 1.5,
   169    max_imperfect = 11.5,
   170    max_imperfect_exp = 1.0,
   171    threshold_divisor = 2.0,
   172    ridiculous_threshold = 0.01}
   173 
   174 (* FUDGE (FIXME) *)
   175 val smt_relevance_fudge =
   176   {allow_ext = false,
   177    worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
   178    higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
   179    abs_rel_weight = #abs_rel_weight atp_relevance_fudge,
   180    abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,
   181    skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,
   182    theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,
   183    theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,
   184    intro_bonus = #intro_bonus atp_relevance_fudge,
   185    elim_bonus = #elim_bonus atp_relevance_fudge,
   186    simp_bonus = #simp_bonus atp_relevance_fudge,
   187    local_bonus = #local_bonus atp_relevance_fudge,
   188    assum_bonus = #assum_bonus atp_relevance_fudge,
   189    chained_bonus = #chained_bonus atp_relevance_fudge,
   190    max_imperfect = #max_imperfect atp_relevance_fudge,
   191    max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge,
   192    threshold_divisor = #threshold_divisor atp_relevance_fudge,
   193    ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
   194 
   195 fun relevance_fudge_for_prover ctxt name =
   196   if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
   197 
   198 fun available_provers ctxt =
   199   let
   200     val thy = ProofContext.theory_of ctxt
   201     val (remote_provers, local_provers) =
   202       sort_strings (available_atps thy) @
   203       sort_strings (available_smt_solvers ctxt)
   204       |> List.partition (String.isPrefix remote_prefix)
   205   in
   206     Output.urgent_message ("Available provers: " ^
   207                            commas (local_provers @ remote_provers) ^ ".")
   208   end
   209 
   210 fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
   211 fun running_provers () = Async_Manager.running_threads das_Tool "provers"
   212 val messages = Async_Manager.thread_messages das_Tool "prover"
   213 
   214 (** problems, results, ATPs, etc. **)
   215 
   216 type params =
   217   {debug: bool,
   218    verbose: bool,
   219    overlord: bool,
   220    blocking: bool,
   221    provers: string list,
   222    type_sys: type_system,
   223    explicit_apply: bool,
   224    relevance_thresholds: real * real,
   225    max_relevant: int option,
   226    isar_proof: bool,
   227    isar_shrink_factor: int,
   228    timeout: Time.time,
   229    expect: string}
   230 
   231 datatype prover_fact =
   232   Untranslated_Fact of (string * locality) * thm |
   233   ATP_Translated_Fact of translated_formula option * ((string * locality) * thm)
   234 
   235 type prover_problem =
   236   {state: Proof.state,
   237    goal: thm,
   238    subgoal: int,
   239    subgoal_count: int,
   240    facts: prover_fact list}
   241 
   242 type prover_result =
   243   {outcome: failure option,
   244    message: string,
   245    used_facts: (string * locality) list,
   246    run_time_in_msecs: int option}
   247 
   248 type prover = params -> minimize_command -> prover_problem -> prover_result
   249 
   250 (* configuration attributes *)
   251 
   252 val (dest_dir, dest_dir_setup) =
   253   Attrib.config_string "sledgehammer_dest_dir" (K "")
   254   (* Empty string means create files in Isabelle's temporary files directory. *)
   255 
   256 val (problem_prefix, problem_prefix_setup) =
   257   Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
   258 
   259 val (measure_run_time, measure_run_time_setup) =
   260   Attrib.config_bool "sledgehammer_measure_run_time" (K false)
   261 
   262 fun with_path cleanup after f path =
   263   Exn.capture f path
   264   |> tap (fn _ => cleanup path)
   265   |> Exn.release
   266   |> tap (after path)
   267 
   268 fun proof_banner auto =
   269   if auto then "Auto Sledgehammer found a proof" else "Try this command"
   270 
   271 (* generic TPTP-based ATPs *)
   272 
   273 fun untranslated_fact (Untranslated_Fact p) = p
   274   | untranslated_fact (ATP_Translated_Fact (_, p)) = p
   275 fun atp_translated_fact ctxt (Untranslated_Fact p) = translate_atp_fact ctxt p
   276   | atp_translated_fact _ (ATP_Translated_Fact q) = q
   277 
   278 fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
   279   | int_opt_add _ _ = NONE
   280 
   281 fun overlord_file_location_for_prover prover =
   282   (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   283 
   284 val atp_first_iter_time_frac = 0.67
   285 
   286 (* Important messages are important but not so important that users want to see
   287    them each time. *)
   288 val important_message_keep_factor = 0.1
   289 
   290 fun run_atp auto name
   291         ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
   292           known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
   293           : atp_config)
   294         ({debug, verbose, overlord, type_sys, explicit_apply, isar_proof,
   295           isar_shrink_factor, timeout, ...} : params)
   296         minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   297   let
   298     val ctxt = Proof.context_of state
   299     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
   300     val facts = facts |> map (atp_translated_fact ctxt)
   301     val (dest_dir, problem_prefix) =
   302       if overlord then overlord_file_location_for_prover name
   303       else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
   304     val problem_file_name =
   305       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
   306                   "_" ^ string_of_int subgoal)
   307     val problem_path_name =
   308       if dest_dir = "" then
   309         File.tmp_path problem_file_name
   310       else if File.exists (Path.explode dest_dir) then
   311         Path.append (Path.explode dest_dir) problem_file_name
   312       else
   313         error ("No such directory: " ^ quote dest_dir ^ ".")
   314     val measure_run_time = verbose orelse Config.get ctxt measure_run_time
   315     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
   316     (* write out problem file and call ATP *)
   317     fun command_line complete timeout probfile =
   318       let
   319         val core = File.shell_path command ^ " " ^ arguments complete timeout ^
   320                    " " ^ File.shell_path probfile
   321       in
   322         (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
   323          else "exec " ^ core) ^ " 2>&1"
   324       end
   325     fun split_time s =
   326       let
   327         val split = String.tokens (fn c => str c = "\n");
   328         val (output, t) = s |> split |> split_last |> apfst cat_lines;
   329         fun as_num f = f >> (fst o read_int);
   330         val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   331         val digit = Scan.one Symbol.is_ascii_digit;
   332         val num3 = as_num (digit ::: digit ::: (digit >> single));
   333         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   334         val as_time = Scan.read Symbol.stopper time o raw_explode
   335       in (output, as_time t) end;
   336     fun run_on probfile =
   337       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
   338         (home_var, _) :: _ =>
   339         error ("The environment variable " ^ quote home_var ^ " is not set.")
   340       | [] =>
   341         if File.exists command then
   342           let
   343             fun run complete timeout =
   344               let
   345                 val command = command_line complete timeout probfile
   346                 val ((output, msecs), res_code) =
   347                   bash_output command
   348                   |>> (if overlord then
   349                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   350                        else
   351                          I)
   352                   |>> (if measure_run_time then split_time else rpair NONE)
   353                 val (tstplike_proof, outcome) =
   354                   extract_tstplike_proof_and_outcome complete res_code
   355                       proof_delims known_failures output
   356               in (output, msecs, tstplike_proof, outcome) end
   357             val readable_names = debug andalso overlord
   358             val (atp_problem, pool, conjecture_offset, fact_names) =
   359               prepare_atp_problem ctxt readable_names explicit_forall type_sys
   360                                   explicit_apply hyp_ts concl_t facts
   361             val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
   362                                                   atp_problem
   363             val _ = File.write_list probfile ss
   364             val conjecture_shape =
   365               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   366               |> map single
   367             val run_twice = has_incomplete_mode andalso not auto
   368             val timer = Timer.startRealTimer ()
   369             val result =
   370               run false
   371                  (if run_twice then
   372                     seconds (0.001 * atp_first_iter_time_frac
   373                              * Real.fromInt (Time.toMilliseconds timeout))
   374                   else
   375                     timeout)
   376               |> run_twice
   377                  ? (fn (_, msecs0, _, SOME _) =>
   378                        run true (Time.- (timeout, Timer.checkRealTimer timer))
   379                        |> (fn (output, msecs, tstplike_proof, outcome) =>
   380                               (output, int_opt_add msecs0 msecs, tstplike_proof,
   381                                outcome))
   382                      | result => result)
   383           in ((pool, conjecture_shape, fact_names), result) end
   384         else
   385           error ("Bad executable: " ^ Path.implode command ^ ".")
   386 
   387     (* If the problem file has not been exported, remove it; otherwise, export
   388        the proof file too. *)
   389     fun cleanup probfile =
   390       if dest_dir = "" then try File.rm probfile else NONE
   391     fun export probfile (_, (output, _, _, _)) =
   392       if dest_dir = "" then
   393         ()
   394       else
   395         File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   396     val ((pool, conjecture_shape, fact_names),
   397          (output, msecs, tstplike_proof, outcome)) =
   398       with_path cleanup export run_on problem_path_name
   399     val (conjecture_shape, fact_names) =
   400       repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
   401     val important_message =
   402       if not auto andalso random () <= important_message_keep_factor then
   403         extract_important_message output
   404       else
   405         ""
   406     val (message, used_facts) =
   407       case outcome of
   408         NONE =>
   409         proof_text isar_proof
   410             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   411             (proof_banner auto, type_sys, minimize_command, tstplike_proof,
   412              fact_names, goal, subgoal)
   413         |>> (fn message =>
   414                 message ^
   415                 (if verbose then
   416                    "\nATP real CPU time: " ^
   417                    string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
   418                  else
   419                    "") ^
   420                 (if important_message <> "" then
   421                    "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
   422                    important_message
   423                  else
   424                    ""))
   425       | SOME failure => (string_for_failure "ATP" failure, [])
   426   in
   427     {outcome = outcome, message = message, used_facts = used_facts,
   428      run_time_in_msecs = msecs}
   429   end
   430 
   431 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
   432    these are sorted out properly in the SMT module, we have to interpret these
   433    ourselves. *)
   434 val perl_failures =
   435   [(127, NoPerl)]
   436 val remote_smt_failures =
   437   [(22, CantConnect),
   438    (2, NoLibwwwPerl)]
   439 val z3_wrapper_failures =
   440   [(10, NoRealZ3),
   441    (11, InternalError),
   442    (12, InternalError),
   443    (13, InternalError)]
   444 val z3_failures =
   445   [(103, MalformedInput),
   446    (110, MalformedInput)]
   447 val unix_failures =
   448   [(139, Crashed)]
   449 val smt_failures =
   450   perl_failures @ remote_smt_failures @ z3_wrapper_failures @ z3_failures @
   451   unix_failures
   452 
   453 val internal_error_prefix = "Internal error: "
   454 
   455 fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
   456   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   457   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
   458     (case AList.lookup (op =) smt_failures code of
   459        SOME failure => failure
   460      | NONE => UnknownError)
   461   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   462   | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
   463     if String.isPrefix internal_error_prefix msg then InternalError
   464     else UnknownError
   465 
   466 (* FUDGE *)
   467 val smt_max_iters = Unsynchronized.ref 8
   468 val smt_iter_fact_frac = Unsynchronized.ref 0.5
   469 val smt_iter_time_frac = Unsynchronized.ref 0.5
   470 val smt_iter_min_msecs = Unsynchronized.ref 5000
   471 val smt_monomorph_limit = Unsynchronized.ref 4
   472 
   473 fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
   474   let
   475     val ctxt = Proof.context_of state
   476     fun iter timeout iter_num outcome0 time_so_far facts =
   477       let
   478         val timer = Timer.startRealTimer ()
   479         val ms = timeout |> Time.toMilliseconds
   480         val iter_timeout =
   481           if iter_num < !smt_max_iters then
   482             Int.min (ms,
   483                 Int.max (!smt_iter_min_msecs,
   484                     Real.ceil (!smt_iter_time_frac * Real.fromInt ms)))
   485             |> Time.fromMilliseconds
   486           else
   487             timeout
   488         val num_facts = length facts
   489         val _ =
   490           if verbose then
   491             "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^
   492             plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..."
   493             |> Output.urgent_message
   494           else
   495             ()
   496         val birth = Timer.checkRealTimer timer
   497         val _ =
   498           if debug then Output.urgent_message "Invoking SMT solver..." else ()
   499         val (outcome, used_facts) =
   500           SMT_Solver.smt_filter remote iter_timeout state facts i
   501           |> (fn {outcome, used_facts, ...} => (outcome, used_facts))
   502           handle exn => if Exn.is_interrupt exn then
   503                           reraise exn
   504                         else
   505                           (internal_error_prefix ^ ML_Compiler.exn_message exn
   506                            |> SMT_Failure.Other_Failure |> SOME, [])
   507         val death = Timer.checkRealTimer timer
   508         val _ =
   509           if verbose andalso is_some outcome then
   510             "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
   511             |> Output.urgent_message
   512           else if debug then
   513             Output.urgent_message "SMT solver returned."
   514           else
   515             ()
   516         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   517         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
   518         val too_many_facts_perhaps =
   519           case outcome of
   520             NONE => false
   521           | SOME (SMT_Failure.Counterexample _) => false
   522           | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
   523           | SOME (SMT_Failure.Abnormal_Termination code) =>
   524             (if verbose then
   525                "The SMT solver invoked with " ^ string_of_int num_facts ^
   526                " fact" ^ plural_s num_facts ^ " terminated abnormally with \
   527                \exit code " ^ string_of_int code ^ "."
   528                |> warning
   529              else
   530                ();
   531              true (* kind of *))
   532           | SOME SMT_Failure.Out_Of_Memory => true
   533           | SOME (SMT_Failure.Other_Failure _) => true
   534         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   535       in
   536         if too_many_facts_perhaps andalso iter_num < !smt_max_iters andalso
   537            num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
   538           let
   539             val n = Real.ceil (!smt_iter_fact_frac * Real.fromInt num_facts)
   540           in iter timeout (iter_num + 1) outcome0 time_so_far (take n facts) end
   541         else
   542           {outcome = if is_none outcome then NONE else the outcome0,
   543            used_facts = used_facts,
   544            run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)}
   545       end
   546   in iter timeout 1 NONE Time.zeroTime end
   547 
   548 (* taken from "Mirabelle" and generalized *)
   549 fun can_apply timeout tac state i =
   550   let
   551     val {context = ctxt, facts, goal} = Proof.goal state
   552     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   553   in
   554     case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
   555       SOME (SOME _) => true
   556     | _ => false
   557   end
   558 
   559 val smt_metis_timeout = seconds 1.0
   560 
   561 fun can_apply_metis debug state i ths =
   562   can_apply smt_metis_timeout
   563             (Config.put Metis_Tactics.verbose debug
   564              #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
   565 
   566 val smt_weights = Unsynchronized.ref true
   567 val smt_weight_min_facts = 20
   568 
   569 (* FUDGE *)
   570 val smt_min_weight = Unsynchronized.ref 0
   571 val smt_max_weight = Unsynchronized.ref 10
   572 val smt_max_index = Unsynchronized.ref 200
   573 val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
   574 
   575 fun smt_fact_weight j num_facts =
   576   if !smt_weights andalso num_facts >= smt_weight_min_facts then
   577     SOME (!smt_max_weight
   578           - (!smt_max_weight - !smt_min_weight + 1)
   579             * !smt_weight_curve (Int.max (0, !smt_max_index - j - 1))
   580             div !smt_weight_curve (!smt_max_index))
   581   else
   582     NONE
   583 
   584 fun run_smt_solver auto name (params as {debug, verbose, overlord, ...})
   585         minimize_command
   586         ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   587   let
   588     val (remote, suffix) =
   589       case try (unprefix remote_prefix) name of
   590         SOME suffix => (true, suffix)
   591       | NONE => (false, name)
   592     val repair_context =
   593       Context.proof_map (SMT_Config.select_solver suffix)
   594       #> Config.put SMT_Config.verbose debug
   595       #> (if overlord then
   596             Config.put SMT_Config.debug_files
   597                        (overlord_file_location_for_prover name
   598                         |> (fn (path, base) => path ^ "/" ^ base))
   599           else
   600             I)
   601       #> Config.put SMT_Config.monomorph_limit (!smt_monomorph_limit)
   602     val state = state |> Proof.map_context repair_context
   603     val thy = Proof.theory_of state
   604     val num_facts = length facts
   605     val facts =
   606       facts ~~ (0 upto num_facts - 1)
   607       |> map (fn (fact, j) =>
   608                  fact |> untranslated_fact
   609                       |> apsnd (pair (smt_fact_weight j num_facts)
   610                                 o Thm.transfer thy))
   611     val {outcome, used_facts, run_time_in_msecs} =
   612       smt_filter_loop params remote state subgoal facts
   613     val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
   614     val outcome = outcome |> Option.map failure_from_smt_failure
   615     val message =
   616       case outcome of
   617         NONE =>
   618         let
   619           val (method, settings) =
   620             if can_apply_metis debug state subgoal (map snd used_facts) then
   621               ("metis", "")
   622             else
   623               ("smt", if suffix = SMT_Config.solver_of @{context} then ""
   624                       else "smt_solver = " ^ maybe_quote suffix)
   625         in
   626           try_command_line (proof_banner auto)
   627               (apply_on_subgoal settings subgoal subgoal_count ^
   628                command_call method (map fst other_lemmas)) ^
   629           minimize_line minimize_command
   630                         (map fst (other_lemmas @ chained_lemmas)) ^
   631           (if verbose then
   632              "\nSMT solver real CPU time: " ^
   633              string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^
   634              "."
   635            else
   636              "")
   637         end
   638       | SOME failure => string_for_failure "SMT solver" failure
   639   in
   640     {outcome = outcome, used_facts = map fst used_facts,
   641      run_time_in_msecs = run_time_in_msecs, message = message}
   642   end
   643 
   644 fun get_prover ctxt auto name =
   645   let val thy = ProofContext.theory_of ctxt in
   646     if is_smt_prover ctxt name then
   647       run_smt_solver auto name
   648     else if member (op =) (available_atps thy) name then
   649       run_atp auto name (get_atp thy name)
   650     else
   651       error ("No such prover: " ^ name ^ ".")
   652   end
   653 
   654 val setup =
   655   dest_dir_setup
   656   #> problem_prefix_setup
   657   #> measure_run_time_setup
   658 
   659 end;