src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML

rationalized output for forthcoming slicing model

(*  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_prover : Proof.context -> string -> bool
  val run_smt_solver : mode -> string -> prover
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 is_smt_prover = 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, slice, timeout, ...} : params) state goal i facts =
  let
    val run_timeout = if slice = Time.zeroTime then timeout else slice
    val (higher_order, nat_as_int) =
      (case type_enc of
        SOME s =>  (String.isSubstring "native_higher" s, String.isSubstring "arith" s)
      | NONE => (false, false))
    fun repair_context ctxt = ctxt
      |> Context.proof_map (SMT_Config.select_solver name)
      |> Config.put SMT_Config.verbose debug
      |> Config.put SMT_Config.higher_order higher_order
      |> Config.put SMT_Config.nat_as_int nat_as_int
      |> (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, ...} =
      SMT_Solver.smt_filter ctxt goal facts i run_timeout
      handle exn =>
      if Exn.is_interrupt exn orelse debug then
        Exn.reraise exn
      else
        {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE,
         atp_proof = K []}

    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, ...})
    ({state, goal, subgoal, subgoal_count, facts, found_proof, ...} : prover_problem) =
  let
    val ctxt = Proof.context_of state

    val facts = snd facts

    val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
      smt_filter name params state goal subgoal facts
    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_proof name;
          val preferred =
            if smt_proofs then
              SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3)
            else
              Metis_Method (NONE, NONE);
          val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN;
        in
          ((preferred, methss),
           fn preplay =>
             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 one_line_params = (preplay (), 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;