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