# HG changeset patch # User desharna # Date 1638105301 -3600 # Node ID 8b1ab558e3eed2a7c996b535d959a89c885f7a9a # Parent f9908452b2824d1a80ef39cc9a4ed99c09dfb357 reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle diff -r f9908452b282 -r 8b1ab558e3ee src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sun Nov 21 11:21:16 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sun Nov 28 14:15:01 2021 +0100 @@ -3,7 +3,7 @@ Author: Sascha Boehme, TU Munich Author: Tobias Nipkow, TU Munich Author: Makarius - Author: Martin Desharnais, UniBw Munich + Author: Martin Desharnais, UniBw Munich, MPI-INF Saarbruecken Mirabelle action: "sledgehammer". *) @@ -21,48 +21,16 @@ val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) -val fact_filterK = "fact_filter" (*=STRING: fact filter*) val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) -val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*) val keepK = "keep" (*=BOOL: keep temporary files created by sledgehammer*) -val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*) -val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) -val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) -val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*) -val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*) -val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*) -val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*) val proverK = "prover" (*=STRING: name of the external prover to call*) -val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*) -val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*) -val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*) -val strictK = "strict" (*=BOOL: run in strict mode*) val term_orderK = "term_order" (*=STRING: term order (in E)*) -val type_encK = "type_enc" (*=STRING: type encoding scheme*) -val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*) -(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) (*defaults used in this Mirabelle action*) -val preplay_timeout_default = "1" -val lam_trans_default = "smart" -val uncurried_aliases_default = "smart" -val fact_filter_default = "smart" -val type_enc_default = "smart" -val strict_default = "false" -val max_facts_default = "smart" -val slice_default = "true" val check_trivial_default = false val keep_default = false -(*If a key is present in args then augment a list with its pair*) -(*This is used to avoid fixing default values at the Mirabelle level, and - instead use the default values of the tool (Sledgehammer in this case).*) -fun available_parameter args key label list = - let - val value = AList.lookup (op =) args key - in if is_some value then (label, the value) :: list else list end - datatype sh_data = ShData of { calls: int, success: int, @@ -336,10 +304,8 @@ SH_FAIL of int * int | SH_ERROR -fun run_sh prover_name fact_filter type_enc strict max_facts slice - lam_trans uncurried_aliases e_selection_heuristic term_order force_sos - hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST - minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = +fun run_sh (params as {max_facts, minimize, preplay_timeout, ...}) prover_name e_selection_heuristic + term_order force_sos hard_timeout dir pos st = let val thy = Proof.theory_of st val {context = ctxt, facts = chained_ths, goal} = Proof.goal st @@ -365,30 +331,13 @@ term_order |> the_default I) #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) force_sos |> the_default I)) - val params as {max_facts, minimize, preplay_timeout, ...} = - Sledgehammer_Commands.default_params thy - ([(* ("verbose", "true"), *) - ("fact_filter", fact_filter), - ("type_enc", type_enc), - ("strict", strict), - ("lam_trans", lam_trans |> the_default lam_trans_default), - ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default), - ("max_facts", max_facts), - ("slice", slice), - ("timeout", string_of_int timeout), - ("preplay_timeout", preplay_timeout)] - |> isar_proofsLST - |> smt_proofsLST - |> minimizeLST (*don't confuse the two minimization flags*) - |> max_new_mono_instancesLST - |> max_mono_itersLST) val default_max_facts = Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val time_limit = (case hard_timeout of NONE => I - | SOME secs => Timeout.apply (Time.fromSeconds secs)) + | SOME t => Timeout.apply t) fun failed failure = ({outcome = SOME failure, used_facts = [], used_from = [], preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime, @@ -432,33 +381,17 @@ in -fun run_sledgehammer change_data thy_index trivial output_dir args proof_method named_thms pos st = +fun run_sledgehammer change_data (params as {provers, timeout, ...}) output_dir + e_selection_heuristic term_order force_sos keep proof_method_from_msg thy_index trivial + proof_method named_thms pos st = let val thy = Proof.theory_of st val thy_name = Context.theory_name thy val triv_str = if trivial then "[T] " else "" val _ = change_data inc_sh_calls val _ = if trivial then () else change_data inc_sh_nontriv_calls - val prover_name = get_prover_name thy args - val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default - val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default - val strict = AList.lookup (op =) args strictK |> the_default strict_default - val max_facts = - (case AList.lookup (op =) args max_factsK of - SOME max => max - | NONE => - (case AList.lookup (op =) args max_relevantK of - SOME max => max - | NONE => max_facts_default)) - val slice = AList.lookup (op =) args sliceK |> the_default slice_default - val lam_trans = AList.lookup (op =) args lam_transK - val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK - val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK - val term_order = AList.lookup (op =) args term_orderK - val force_sos = AList.lookup (op =) args force_sosK - |> Option.map (curry (op <>) "false") val keep_dir = - if Mirabelle.get_bool_argument args (keepK, keep_default) then + if keep then let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in Path.append output_dir (Path.basic subdir) |> Isabelle_System.make_directory @@ -467,23 +400,13 @@ end else NONE - val timeout = Mirabelle.get_int_argument args (prover_timeoutK, 30) (* always use a hard timeout, but give some slack so that the automatic minimizer has a chance to do its magic *) - val preplay_timeout = AList.lookup (op =) args preplay_timeoutK - |> the_default preplay_timeout_default - val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" - val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs" - val minimizeLST = available_parameter args minimizeK "minimize" - val max_new_mono_instancesLST = - available_parameter args max_new_mono_instancesK max_new_mono_instancesK - val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK - val hard_timeout = SOME (4 * timeout) + val hard_timeout = SOME (Time.scale 4.0 timeout) + val prover_name = hd provers val (msg, result) = - run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans - uncurried_aliases e_selection_heuristic term_order force_sos - hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST - minimizeLST max_new_mono_instancesLST max_mono_itersLST keep_dir pos st + run_sh params prover_name e_selection_heuristic term_order force_sos hard_timeout keep_dir pos + st in (case result of SH_OK (time_isa, time_prover, names) => @@ -499,7 +422,7 @@ change_data (inc_sh_max_lems (length names)); change_data (inc_sh_time_isa time_isa); change_data (inc_sh_time_prover time_prover); - proof_method := proof_method_from_msg args msg; + proof_method := proof_method_from_msg msg; named_thms := SOME (map_filter get_thms names); triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg @@ -593,8 +516,22 @@ fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) = let + (* Parse Mirabelle-specific parameters *) val check_trivial = Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default) + val keep = Mirabelle.get_bool_argument arguments (keepK, keep_default) + val e_selection_heuristic = AList.lookup (op =) arguments e_selection_heuristicK + val term_order = AList.lookup (op =) arguments term_orderK + val force_sos = AList.lookup (op =) arguments force_sosK + |> Option.map (curry (op <>) "false") + val proof_method_from_msg = proof_method_from_msg arguments + + (* Parse Sledgehammer parameters *) + val params = Sledgehammer_Commands.default_params \<^theory> arguments + |> (fn (params as {provers, ...}) => + (case provers of + prover :: _ => Sledgehammer_Prover.set_params_provers params [prover] + | _ => error "sledgehammer action requires one prover")) val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data val change_data = Synchronized.change data @@ -612,8 +549,8 @@ check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre handle Timeout.TIMEOUT _ => false val log1 = - run_sledgehammer change_data theory_index trivial output_dir arguments meth named_thms - pos pre + run_sledgehammer change_data params output_dir e_selection_heuristic term_order + force_sos keep proof_method_from_msg theory_index trivial meth named_thms pos pre val log2 = (case !named_thms of SOME thms => @@ -628,4 +565,4 @@ val () = Mirabelle.register_action "sledgehammer" make_action -end +end \ No newline at end of file diff -r f9908452b282 -r 8b1ab558e3ee src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun Nov 21 11:21:16 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun Nov 28 14:15:01 2021 +0100 @@ -47,6 +47,8 @@ preplay_timeout : Time.time, expect : string} + val set_params_provers : params -> string list -> params + type prover_problem = {comment : string, state : Proof.state, @@ -141,6 +143,33 @@ preplay_timeout : Time.time, expect : string} +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, + slice = #slice params, + minimize = #minimize params, + timeout = #timeout params, + preplay_timeout = #preplay_timeout params, + expect = #expect params} + type prover_problem = {comment : string, state : Proof.state,