diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML @@ -1,414 +1,414 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.ML Author: Jasmin Blanchette, TU Muenchen Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. *) signature SLEDGEHAMMER_COMMANDS = sig type params = Sledgehammer_Prover.params val provers : string Unsynchronized.ref val default_params : theory -> (string * string) list -> params val parse_params: (string * string) list parser end; structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = struct open ATP_Util open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer val cvc4N = "cvc4" val veritN = "verit" val z3N = "z3" val runN = "run" val supported_proversN = "supported_provers" val refresh_tptpN = "refresh_tptp" (** Sledgehammer commands **) fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) (*** parameters ***) val provers = Unsynchronized.ref "" type raw_param = string * string list val default_default_params = [("debug", "false"), ("verbose", "false"), ("overlord", "false"), ("spy", "false"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), ("uncurried_aliases", "smart"), ("learn", "true"), ("fact_filter", "smart"), ("induction_rules", "smart"), ("max_facts", "smart"), ("fact_thresholds", "0.45 0.85"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), ("isar_proofs", "smart"), ("compress", "smart"), ("try0", "true"), ("smt_proofs", "true"), ("minimize", "true"), - ("slice", "5"), + ("slices", string_of_int (6 * Multithreading.max_threads ())), ("preplay_timeout", "1")] val alias_params = [("prover", ("provers", [])), (* undocumented *) ("dont_preplay", ("preplay_timeout", ["0"])), ("dont_compress", ("compress", ["1"])), - ("dont_slice", ("slice", ["0"])), + ("dont_slice", ("slices", ["1"])), ("isar_proof", ("isar_proofs", [])) (* legacy *)] val negated_alias_params = [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), ("no_isar_proofs", "isar_proofs"), ("dont_minimize", "minimize"), ("dont_try0", "try0"), ("no_smt_proofs", "smt_proofs")] val property_dependent_params = ["provers", "timeout"] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) alias_params s orelse AList.defined (op =) negated_alias_params s orelse member (op =) property_dependent_params s orelse s = "expect" fun is_prover_list ctxt s = (case space_explode " " s of ss as _ :: _ => forall (is_prover_supported ctxt) ss | _ => false) fun unalias_raw_param (name, value) = (case AList.lookup (op =) alias_params name of SOME (name', []) => (name', value) | SOME (param' as (name', _)) => if value <> ["false"] then param' else error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")") | NONE => (case AList.lookup (op =) negated_alias_params name of SOME name' => (name', (case value of ["false"] => ["true"] | ["true"] => ["false"] | [] => ["false"] | _ => value)) | NONE => (name, value))) val any_type_enc = type_enc_of_string Strict "erased" (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" can be omitted. For the last four, this is a secret feature. *) fun normalize_raw_param ctxt = unalias_raw_param #> (fn (name, value) => if is_known_raw_param name then (name, value) else if null value then if is_prover_list ctxt name then ("provers", [name]) else if can (type_enc_of_string Strict) name then ("type_enc", [name]) else if can (trans_lams_of_string ctxt any_type_enc) name then ("lam_trans", [name]) else if member (op =) fact_filters name then ("fact_filter", [name]) else if is_some (Int.fromString name) then ("max_facts", [name]) else error ("Unknown parameter: " ^ quote name) else error ("Unknown parameter: " ^ quote name)) (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) val implode_param = strip_spaces_except_between_idents o space_implode " " (* FIXME: use "Generic_Data" *) structure Data = Theory_Data ( type T = raw_param list val empty = default_default_params |> map (apsnd single) fun merge data : T = AList.merge (op =) (K true) data ) fun remotify_prover_if_supported_and_not_already_remote ctxt name = if String.isPrefix remote_prefix name then SOME name else let val remote_name = remote_prefix ^ name in if is_prover_supported ctxt remote_name then SOME remote_name else NONE end fun remotify_prover_if_not_installed ctxt name = if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name else remotify_prover_if_supported_and_not_already_remote ctxt name (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value ctxt = [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN] \ \see also \<^system_option>\sledgehammer_provers\\ |> map_filter (remotify_prover_if_not_installed ctxt) |> implode_param fun set_default_raw_param param thy = let val ctxt = Proof_Context.init_global thy in thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) end fun default_raw_params thy = let val ctxt = Proof_Context.init_global thy in Data.get thy |> fold (AList.default (op =)) [("provers", [(case !provers of "" => default_provers_param_value ctxt | s => s)]), ("timeout", let val timeout = Options.default_int \<^system_option>\sledgehammer_timeout\ in [if timeout <= 0 then "none" else string_of_int timeout] end)] end fun extract_params mode default_params override_params = let val raw_params = rev override_params @ rev default_params val lookup = Option.map implode_param o AList.lookup (op =) raw_params val lookup_string = the_default "" o lookup fun general_lookup_bool option default_value name = (case lookup name of SOME s => parse_bool_option option name s | NONE => default_value) val lookup_bool = the o general_lookup_bool false (SOME false) fun lookup_time name = (case lookup name of SOME s => parse_time name s | NONE => Time.zeroTime) fun lookup_int name = (case lookup name of NONE => 0 | SOME s => (case Int.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))) fun lookup_real name = (case lookup name of NONE => 0.0 | SOME s => (case Real.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value"))) fun lookup_real_pair name = (case lookup name of NONE => (0.0, 0.0) | SOME s => (case s |> space_explode " " |> map Real.fromString of [SOME r1, SOME r2] => (r1, r2) | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ \values (e.g., \"0.6 0.95\")"))) fun lookup_option lookup' name = (case lookup name of SOME "smart" => NONE | _ => SOME (lookup' name)) val debug = mode <> Auto_Try andalso lookup_bool "debug" val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val type_enc = if mode = Auto_Try then NONE else (case lookup_string "type_enc" of "smart" => NONE | s => (type_enc_of_string Strict s; SOME s)) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" val learn = lookup_bool "learn" val fact_filter = lookup_option lookup_string "fact_filter" |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf) val induction_rules = lookup_option (the o induction_rules_of_string o lookup_string) "induction_rules" val max_facts = lookup_option lookup_int "max_facts" val fact_thresholds = lookup_real_pair "fact_thresholds" val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" val isar_proofs = lookup_option lookup_bool "isar_proofs" val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") val try0 = lookup_bool "try0" val smt_proofs = lookup_bool "smt_proofs" val minimize = lookup_bool "minimize" - val slice = if mode = Auto_Try then Time.zeroTime else lookup_time "slice" + val slices = if mode = Auto_Try then 1 else Int.max (1, lookup_int "slices") val timeout = lookup_time "timeout" val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, - minimize = minimize, slice = slice, timeout = timeout, preplay_timeout = preplay_timeout, + minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params fun default_params thy = get_params Normal thy o map (apsnd single) val silence_state = Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) (* Sledgehammer the given subgoal *) val default_learn_prover_timeout = 2.0 fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 = let (* We generally want chained facts to be picked up by the relevance filter, because it can then give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, verbose output, machine learning). However, if the fact is available by no other means (not even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice but to insert it into the state as an additional hypothesis. *) val {facts = chained0, ...} = Proof.goal state0 val (inserts, keep_chained) = if null chained0 orelse #only fact_override then (chained0, []) else let val ctxt0 = Proof.context_of state0 in List.partition (is_useful_unnamed_local_fact ctxt0) chained0 end val state = state0 |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained) |> silence_state val thy = Proof.theory_of state val ctxt = Proof.context_of state val override_params = override_params |> map (normalize_raw_param ctxt) in if subcommand = runN then let val i = the_default 1 opt_i in ignore (run_sledgehammer (get_params Normal thy override_params) Normal writeln_result i fact_override state) end else if subcommand = supported_proversN then supported_provers ctxt else if subcommand = unlearnN then mash_unlearn ctxt else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse subcommand = relearn_isarN orelse subcommand = relearn_proverN then (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt else (); mash_learn ctxt (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) (get_params Normal thy ([("timeout", [string_of_real default_learn_prover_timeout]), ("slice", ["false"])] @ override_params @ [("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_proverN orelse subcommand = relearn_proverN)) else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else error ("Unknown subcommand: " ^ quote subcommand) end fun string_of_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) val parse_query_bang = \<^keyword>\?\ || \<^keyword>\!\ || \<^keyword>\!!\ val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] val parse_params = parse_raw_params >> map (apsnd implode_param) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) || (parse_fact_refs >> only_fact_override) val parse_fact_override = Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) no_fact_override val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer\ "search for first-order proof using automatic theorem provers" (Scan.optional Parse.name runN -- parse_raw_params -- parse_fact_override -- Scan.option Parse.nat >> (fn (((subcommand, params), fact_override), opt_i) => Toplevel.keep_proof (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of))) val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer_params\ "set and display the default parameters for Sledgehammer" (parse_raw_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ (case rev (default_raw_params thy) of [] => "none" | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) val _ = Try.tool_setup {name = sledgehammerN, weight = 40, auto_option = \<^system_option>\auto_sledgehammer\, body = fn auto => fn state => let val thy = Proof.theory_of state val mode = if auto then Auto_Try else Try val i = 1 in run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) |> apsnd (map_prod short_string_of_sledgehammer_outcome single) end} val _ = Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, writeln_result, ...} => (case try Toplevel.proof_of st of SOME state => let val [provers_arg, isar_proofs_arg, try0_arg] = args val override_params = ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), ("try0", [try0_arg]), ("debug", ["false"]), ("verbose", ["false"]), ("overlord", ["false"])]); in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end | NONE => error "Unknown proof context")) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML @@ -1,262 +1,267 @@ (* 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, + slices : int, timeout : Time.time, preplay_timeout : Time.time, expect : string} val string_of_params : params -> string val set_params_provers : params -> string list -> params + val slice_timeout : int -> Time.time -> Time.time type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, facts : string * fact list, found_proof : string -> 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, + slices : int, 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, + slices = #slices params, timeout = #timeout params, preplay_timeout = #preplay_timeout params, expect = #expect params} +fun slice_timeout slices timeout = + Time.toReal timeout * Real.fromInt (Multithreading.max_threads ()) / Real.fromInt slices + |> seconds + type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, facts : string * fact list, found_proof : string -> 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 prover_name = (case mode of Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof" | Try => "Sledgehammer (" ^ prover_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; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML @@ -1,265 +1,265 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Author: Philipp Meyer, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Minimization of fact list for Metis using external provers. *) signature SLEDGEHAMMER_PROVER_MINIMIZE = sig type stature = ATP_Problem_Generate.stature type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params type prover = Sledgehammer_Prover.prover val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool val default_max_facts_of_prover : Proof.context -> string -> int val get_prover : Proof.context -> mode -> string -> prover val binary_min_facts : int Config.T val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state -> thm -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option * ((unit -> (string * stature) list * (proof_method * play_outcome)) -> string) val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover end; structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE = struct open ATP_Util open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_SMT fun is_prover_supported ctxt = let val thy = Proof_Context.theory_of ctxt in is_atp thy orf is_smt_prover ctxt end fun is_prover_installed ctxt = is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) fun default_max_facts_of_prover ctxt name = let val thy = Proof_Context.theory_of ctxt in if is_atp thy name then fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0 else if is_smt_prover ctxt name then SMT_Solver.default_max_relevant ctxt name else error ("No such prover: " ^ name) end fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in if is_atp thy name then run_atp mode name else if is_smt_prover ctxt name then run_smt_solver mode name else error ("No such prover: " ^ name) end (* wrapper for calling external prover *) fun n_facts names = let val n = length names in string_of_int n ^ " fact" ^ plural_s n ^ (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "") end fun print silent f = if silent then () else writeln (f ()) fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, induction_rules, ...} : params) silent (prover : prover) timeout i n state goal facts = let val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize, - slice = Time.zeroTime, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} + slices = 1, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, facts = ("", facts), found_proof = K ()} val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, message} = prover params problem val result as {outcome, ...} = if is_none outcome0 andalso forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then result0 else {outcome = SOME MaybeUnprovable, used_facts = [], used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} in print silent (fn () => (case outcome of SOME failure => string_of_atp_failure failure | NONE => "Found proof" ^ (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ " (" ^ string_of_time run_time ^ ")")); result end (* minimalization of facts *) (* Give the external prover some slack. The ATP gets further slack because the Sledgehammer preprocessing time is included in the estimate below but isn't part of the timeout. *) val slack_msecs = 200 fun new_timeout timeout run_time = Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs) |> Time.fromMilliseconds (* The linear algorithm usually outperforms the binary algorithm when over 60% of the facts are actually needed. The binary algorithm is much more appropriate for provers that cannot return the list of used facts and hence returns all facts as used. Since we cannot know in advance how many facts are actually needed, we heuristically set the threshold to 10 facts. *) val binary_min_facts = Attrib.setup_config_int \<^binding>\sledgehammer_minimize_binary_min_facts\ (K 20) fun linear_minimize test timeout result xs = let fun min _ [] p = p | min timeout (x :: xs) (seen, result) = (case test timeout (xs @ seen) of result as {outcome = NONE, used_facts, run_time, ...} : prover_result => min (new_timeout timeout run_time) (filter_used_facts true used_facts xs) (filter_used_facts false used_facts seen, result) | _ => min timeout xs (x :: seen, result)) in min timeout xs ([], result) end fun binary_minimize test timeout result xs = let fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) = let val (l0, r0) = chop (length xs div 2) xs (* val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup)) val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs)) val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0)) val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0)) *) val depth = depth + 1 val timeout = new_timeout timeout run_time in (case test timeout (sup @ l0) of result as {outcome = NONE, used_facts, ...} => min depth result (filter_used_facts true used_facts sup) (filter_used_facts true used_facts l0) | _ => (case test timeout (sup @ r0) of result as {outcome = NONE, used_facts, ...} => min depth result (filter_used_facts true used_facts sup) (filter_used_facts true used_facts r0) | _ => let val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 val (sup, r0) = (sup, r0) |> apply2 (filter_used_facts true (map fst sup_r0)) val (sup_l, (r, result)) = min depth result (sup @ l) r0 val sup = sup |> filter_used_facts true (map fst sup_l) in (sup, (l @ r, result)) end)) end (* |> tap (fn _ => warning (replicate_string depth " " ^ "}")) *) | min _ result sup xs = (sup, (xs, result)) in (case snd (min 0 result [] xs) of ([x], result as {run_time, ...}) => (case test (new_timeout timeout run_time) [] of result as {outcome = NONE, ...} => ([], result) | _ => ([x], result)) | p => p) end fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal facts = let val ctxt = Proof.context_of state val prover = get_prover ctxt Minimize prover_name val (chained, non_chained) = List.partition is_fact_chained facts fun test timeout non_chained = test_facts params silent prover timeout i n state goal (chained @ non_chained) in (print silent (fn () => "Sledgehammer minimizer: " ^ prover_name); (case test timeout non_chained of result as {outcome = NONE, used_facts, run_time, ...} => let val non_chained = filter_used_facts true used_facts non_chained val min = if length non_chained >= Config.get ctxt binary_min_facts then binary_minimize else linear_minimize val (min_facts, {message, ...}) = min test (new_timeout timeout run_time) result non_chained val min_facts_and_chained = chained @ min_facts in print silent (fn () => cat_lines ["Minimized to " ^ n_facts (map fst min_facts)] ^ (case length chained of 0 => "" | n => " (plus " ^ string_of_int n ^ " chained)")); (if learn then do_learn (maps snd min_facts_and_chained) else ()); (SOME min_facts_and_chained, message) end | {outcome = SOME TimedOut, ...} => (NONE, fn _ => "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")") | {message, ...} => (NONE, (prefix "Prover error: " o message)))) handle ERROR msg => (NONE, fn _ => "Error: " ^ msg) end fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) ({state, goal, subgoal, subgoal_count, ...} : prover_problem) (result as {outcome, used_facts, used_from, preferred_methss, run_time, message} : prover_result) = if is_some outcome then result else let val (used_facts, message) = if minimize then minimize_facts do_learn name params (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state goal (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) else (SOME used_facts, message) in (case used_facts of SOME used_facts => {outcome = NONE, used_facts = sort_by fst used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} | NONE => result) end fun get_minimizing_prover ctxt mode do_learn name params problem = get_prover ctxt mode name params problem |> maybe_minimize mode do_learn name params problem end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML @@ -1,161 +1,161 @@ (* 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>\sledgehammer_smt_builtins\ (K true) val smt_triggers = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_triggers\ (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>\nat\, \<^typ>\int\, HOLogic.realT]) fun smt_filter name ({debug, overlord, max_mono_iters, max_new_mono_instances, - type_enc, slice, timeout, ...} : params) state goal i facts = + type_enc, slices, timeout, ...} : params) state goal i facts = let - val run_timeout = if slice = Time.zeroTime then timeout else slice + val run_timeout = slice_timeout slices timeout 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;