(* 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 ();
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;