src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML

clarified colors, following d6a14ed060fb;

(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
    Author:     Fabian Immler, TU Muenchen
    Author:     Makarius
    Author:     Jasmin Blanchette, TU Muenchen

SMT solvers as Sledgehammer provers.
*)

signature SLEDGEHAMMER_PROVER_SMT =
sig
  type stature = ATP_Problem_Generate.stature
  type mode = Sledgehammer_Prover.mode
  type prover = Sledgehammer_Prover.prover

  val smt_builtins : bool Config.T
  val smt_triggers : bool Config.T

  val is_smt_solver : Proof.context -> string -> bool
  val is_smt_solver_installed : Proof.context -> string -> bool
  val run_smt_solver : mode -> string -> prover

  val smt_solvers : Proof.context -> string list
end;

structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
struct

open ATP_Util
open ATP_Proof
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Proof_Methods
open Sledgehammer_Isar
open Sledgehammer_ATP_Systems
open Sledgehammer_Prover

val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true)
val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true)

val smt_solvers = sort_strings o SMT_Config.all_solvers_of

val is_smt_solver = member (op =) o smt_solvers
val is_smt_solver_installed = member (op =) o SMT_Config.available_solvers_of

(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
   properly in the SMT module, we must interpret these here. *)
val z3_failures =
  [(101, OutOfResources),
   (103, MalformedInput),
   (110, MalformedInput),
   (112, TimedOut)]
val unix_failures =
  [(134, Crashed),
   (138, Crashed),
   (139, Crashed)]
val smt_failures = z3_failures @ unix_failures

fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) =
    if genuine then Unprovable else GaveUp
  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
    (case AList.lookup (op =) smt_failures code of
      SOME failure => failure
    | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code))
  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s

val is_boring_builtin_typ =
  not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT])

fun smt_filter name ({debug, overlord, max_mono_iters, max_new_mono_instances, type_enc, slices,
    timeout, ...} : params) memoize_fun_call state goal i slice_size facts options =
  let
    val run_timeout = slice_timeout slice_size slices timeout
    val (higher_order, nat_as_int) =
      (case type_enc of
        SOME s => (SOME (String.isSubstring "native_higher" s), SOME (String.isSubstring "arith" s))
      | NONE => (NONE, NONE))
    fun repair_context ctxt = ctxt
      |> Context.proof_map (SMT_Config.select_solver name)
      |> (case higher_order of
           SOME higher_order => Config.put SMT_Config.higher_order higher_order
         | NONE => I)
      |> (case nat_as_int of
           SOME nat_as_int => Config.put SMT_Config.nat_as_int nat_as_int
         | NONE => I)
      |> (if overlord then
            Config.put SMT_Config.debug_files
              (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
          else
            I)
       |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
       |> not (Config.get ctxt smt_builtins)
         ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
            #> Config.put SMT_Systems.z3_extensions false)
       |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
         default_max_new_mono_instances

    val state = Proof.map_context (repair_context) state
    val ctxt = Proof.context_of state

    val timer = Timer.startRealTimer ()
    val birth = Timer.checkRealTimer timer

    val filter_result as {outcome, ...} =
      \<^try>\<open>SMT_Solver.smt_filter ctxt goal facts i run_timeout memoize_fun_call options
        catch exn =>
          {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE,
           atp_proof = K []}\<close>

    val death = Timer.checkRealTimer timer
    val run_time = death - birth
  in
    {outcome = outcome, filter_result = filter_result, used_from = facts, run_time = run_time}
  end

fun run_smt_solver mode name
    (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout,
      ...} : params)
    ({state, goal, subgoal, subgoal_count, factss, found_something, memoize_fun_call,
      ...} : prover_problem)
    slice =
  let
    val (basic_slice as (slice_size, _, _, _, _), SMT_Slice options) = slice
    val facts = facts_of_basic_slice basic_slice factss
    val ctxt = Proof.context_of state

    val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
      smt_filter name params memoize_fun_call state goal subgoal slice_size facts options
    val used_facts =
      (case fact_ids of
        NONE => map fst used_from
      | SOME ids => sort_by fst (map (fst o snd) ids))
    val outcome = Option.map failure_of_smt_failure outcome

    val (preferred_methss, message) =
      (case outcome of
        NONE =>
        let
          val _ = found_something name;
          val preferred =
            if smt_proofs then
              SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default")
            else
              Metis_Method (NONE, NONE, []);
          val methss =
            if try0 then
              bunches_of_proof_methods ctxt smt_proofs false true
            else if smt_proofs then
              bunches_of_smt_methods ctxt
            else
              bunches_of_metis_methods ctxt false true
        in
          ((preferred, methss),
           fn preplay_outcome =>
             let
               val _ = if verbose then writeln "Generating proof text..." else ()

               fun isar_params () =
                 (verbose, (NONE, NONE, []), preplay_timeout, compress, try0, minimize,
                  atp_proof (), goal)

                val preplay_result = preplay_outcome
                  |> the_default
                    (map (apfst Pretty.str) used_facts,
                     (preferred, Play_Timed_Out Time.zeroTime))
               val one_line_params = (preplay_result, proof_banner mode name, subgoal, subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
             in
               proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
             end)
        end
      | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
  in
    {outcome = outcome, used_facts = used_facts, used_from = used_from,
     preferred_methss = preferred_methss, run_time = run_time, message = message}
  end

end;