(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover.ML
Author: Fabian Immler, TU Muenchen
Author: Makarius
Author: Jasmin Blanchette, TU Muenchen
Generic prover abstraction for Sledgehammer.
*)
signature SLEDGEHAMMER_PROVER =
sig
type atp_failure = ATP_Proof.atp_failure
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
type fact = Sledgehammer_Fact.fact
type proof_method = Sledgehammer_Proof_Methods.proof_method
type play_outcome = Sledgehammer_Proof_Methods.play_outcome
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
datatype induction_rules = Include | Exclude | Instantiate
val induction_rules_of_string : string -> induction_rules option
val maybe_filter_out_induction_rules : induction_rules -> fact list -> fact list
type params =
{debug : bool,
verbose : bool,
overlord : bool,
spy : bool,
provers : string list,
type_enc : string option,
strict : bool,
lam_trans : string option,
uncurried_aliases : bool option,
learn : bool,
fact_filter : string option,
induction_rules : induction_rules option,
max_facts : int option,
fact_thresholds : real * real,
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool option,
compress : real option,
try0 : bool,
smt_proofs : bool,
minimize : bool,
slice : Time.time,
timeout : Time.time,
preplay_timeout : Time.time,
expect : string}
val string_of_params : params -> string
val set_params_provers : params -> string list -> params
type prover_problem =
{comment : string,
state : Proof.state,
goal : thm,
subgoal : int,
subgoal_count : int,
facts : string * fact list,
found_proof : unit -> unit}
type prover_result =
{outcome : atp_failure option,
used_facts : (string * stature) list,
used_from : fact list,
preferred_methss : proof_method * proof_method list list,
run_time : Time.time,
message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
type prover = params -> prover_problem -> prover_result
val SledgehammerN : string
val str_of_mode : mode -> string
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
val is_atp : theory -> string -> bool
val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string ->
proof_method list list
val is_fact_chained : (('a * stature) * 'b) -> bool
val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
Proof.context
val supported_provers : Proof.context -> unit
end;
structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
struct
open ATP_Proof
open ATP_Util
open ATP_Problem
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Metis_Tactic
open Sledgehammer_Fact
open Sledgehammer_Proof_Methods
open Sledgehammer_ATP_Systems
(* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *)
val SledgehammerN = "Sledgehammer"
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
fun str_of_mode Auto_Try = "Auto Try"
| str_of_mode Try = "Try"
| str_of_mode Normal = "Normal"
| str_of_mode Minimize = "Minimize"
| str_of_mode MaSh = "MaSh"
datatype induction_rules = Include | Exclude | Instantiate
fun induction_rules_of_string "include" = SOME Include
| induction_rules_of_string "exclude" = SOME Exclude
| induction_rules_of_string "instantiate" = SOME Instantiate
| induction_rules_of_string _ = NONE
val is_atp = member (op =) o supported_atps
type params =
{debug : bool,
verbose : bool,
overlord : bool,
spy : bool,
provers : string list,
type_enc : string option,
strict : bool,
lam_trans : string option,
uncurried_aliases : bool option,
learn : bool,
fact_filter : string option,
induction_rules : induction_rules option,
max_facts : int option,
fact_thresholds : real * real,
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool option,
compress : real option,
try0 : bool,
smt_proofs : bool,
minimize : bool,
slice : Time.time,
timeout : Time.time,
preplay_timeout : Time.time,
expect : string}
fun string_of_params (params : params) =
YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100)))
fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
induction_rules = Exclude ?
filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
fun set_params_provers params provers =
{debug = #debug params,
verbose = #verbose params,
overlord = #overlord params,
spy = #spy params,
provers = provers,
type_enc = #type_enc params,
strict = #strict params,
lam_trans = #lam_trans params,
uncurried_aliases = #uncurried_aliases params,
learn = #learn params,
fact_filter = #fact_filter params,
induction_rules = #induction_rules params,
max_facts = #max_facts params,
fact_thresholds = #fact_thresholds params,
max_mono_iters = #max_mono_iters params,
max_new_mono_instances = #max_new_mono_instances params,
isar_proofs = #isar_proofs params,
compress = #compress params,
try0 = #try0 params,
smt_proofs = #smt_proofs params,
minimize = #minimize params,
slice = #slice params,
timeout = #timeout params,
preplay_timeout = #preplay_timeout params,
expect = #expect params}
type prover_problem =
{comment : string,
state : Proof.state,
goal : thm,
subgoal : int,
subgoal_count : int,
facts : string * fact list,
found_proof : unit -> unit}
type prover_result =
{outcome : atp_failure option,
used_facts : (string * stature) list,
used_from : fact list,
preferred_methss : proof_method * proof_method list list,
run_time : Time.time,
message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
type prover = params -> prover_problem -> prover_result
fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
fun proof_banner mode name =
(case mode of
Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
| _ => "Try this")
fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans =
let
val try0_methodss =
if try0 then
[[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]]
else
[]
val metis_methods =
(if try0 then [] else [Metis_Method (NONE, NONE)]) @
Metis_Method (SOME full_typesN, NONE) ::
Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) ::
(if needs_full_types then
[Metis_Method (SOME really_full_type_enc, NONE),
Metis_Method (SOME full_typesN, SOME desperate_lam_trans)]
else
[Metis_Method (SOME no_typesN, SOME desperate_lam_trans)])
val smt_methodss =
if smt_proofs then
[map (SMT_Method o SMT_Verit) (Verit_Proof.all_veriT_stgies (Context.Proof ctxt)),
[SMT_Method SMT_Z3]]
else
[]
in
try0_methodss @ [metis_methods] @ smt_methodss
end
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
fun filter_used_facts keep_chained used =
filter ((member (eq_fst (op =)) used o fst) orf
(if keep_chained then is_fact_chained else K false))
val max_fact_instances = 10 (* FUDGE *)
fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
#> Config.put Monomorph.max_new_instances
(max_new_instances |> the_default best_max_new_instances)
#> Config.put Monomorph.max_thm_instances max_fact_instances
fun supported_provers ctxt =
let
val thy = Proof_Context.theory_of ctxt
val (remote_provers, local_provers) =
sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
writeln ("Supported provers: " ^ commas (local_provers @ remote_provers))
end
end;