(* 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 -> stringlist val default_smt_solvers : Proof.context -> stringlist end;
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 default_smt_solvers = sort_strings o SMT_Config.all_nondummy_sledgehammer_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 let val (path, name) = overlord_file_location_of_prover name val file_base = path ^ "/" ^ name in
Config.put SMT_Config.problem_dest_file file_base #>
Config.put SMT_Config.proof_dest_file file_base end 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 (SMT_Verit "default") else
Metis_Method (NONE, NONE, []); val methss = if try0 then
bunches_of_proof_methods ctxt smt_proofs falsetrue elseif smt_proofs then
bunches_of_smt_methods ctxt else
bunches_of_metis_methods ctxt falsetrue in
((preferred, methss),
fn preplay_outcome => let val _ = if verbose then writeln "Generating proof text..."else ()
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
