diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer.ML b/src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML @@ -1,374 +1,361 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Sledgehammer's heart. *) signature SLEDGEHAMMER = sig type stature = ATP_Problem_Generate.stature type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override 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 induction_rules = Sledgehammer_Prover.induction_rules type prover_problem = Sledgehammer_Prover.prover_problem type prover_result = Sledgehammer_Prover.prover_result datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int -> proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome) val string_of_factss : (string * fact list) list -> string val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> Proof.state -> bool * (sledgehammer_outcome * string) end; structure Sledgehammer : SLEDGEHAMMER = struct open ATP_Util open ATP_Proof open ATP_Problem_Generate open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Minimize open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None fun short_string_of_sledgehammer_outcome (SH_Some _) = "some" | short_string_of_sledgehammer_outcome SH_Unknown = "unknown" | short_string_of_sledgehammer_outcome SH_Timeout = "timeout" | short_string_of_sledgehammer_outcome SH_None = "none" fun alternative f (SOME x) (SOME y) = SOME (f (x, y)) | alternative _ (x as SOME _) NONE = x | alternative _ NONE (y as SOME _) = y | alternative _ NONE NONE = NONE fun max_outcome outcomes = let val result = find_first (fn (SH_Some _, _) => true | _ => false) outcomes val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes val none = find_first (fn (SH_None, _) => true | _ => false) outcomes in result |> alternative snd unknown |> alternative snd timeout |> alternative snd none |> the_default (SH_Unknown, "") end fun is_metis_method (Metis_Method _) = true | is_metis_method _ = false fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) = (if timeout = Time.zeroTime then (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) else let val ctxt = Proof.context_of state val fact_names = used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained) |> map fst val {facts = chained, goal, ...} = Proof.goal state val goal_t = Logic.get_goal (Thm.prop_of goal) i fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) | try_methss ress [] = (used_facts, (case AList.lookup (op =) ress preferred_meth of SOME play => (preferred_meth, play) | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress)))) | try_methss ress (meths :: methss) = let fun mk_step fact_names meths = Prove { qualifiers = [], obtains = [], label = ("", 0), goal = goal_t, subproofs = [], facts = ([], fact_names), proof_methods = meths, comment = ""} in (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of (res as (meth, Played time)) :: _ => (* if a fact is needed by an ATP, it will be needed by "metis" *) if not minimize orelse is_metis_method meth then (used_facts, res) else let val (time', used_names') = minimized_isar_step ctxt chained time (mk_step fact_names [meth]) ||> (facts_of_isar_step #> snd) val used_facts' = filter (member (op =) used_names' o fst) used_facts in (used_facts', (meth, Played time')) end | ress' => try_methss (ress' @ ress) methss) end in try_methss [] methss end) |> (fn (used_facts, (meth, play)) => (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play))) fun launch_prover (params as {verbose, spy, max_facts, induction_rules, ...}) mode only learn - ({comment, state, goal, subgoal, subgoal_count, facts, found_proof} : prover_problem) name = + (problem as {state, subgoal, factss, ...} : prover_problem) slice name = let val ctxt = Proof.context_of state val _ = spying spy (fn () => (state, subgoal, name, "Launched")) - val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) - val num_facts = length (snd facts) |> not only ? Integer.min max_facts val induction_rules = the_default Exclude induction_rules - val problem = - {comment = comment, state = state, goal = goal, subgoal = subgoal, - subgoal_count = subgoal_count, - facts = facts - (* We take "num_facts" because "facts" contains the maximum of all called provers. *) - |> apsnd (take num_facts o maybe_filter_out_induction_rules induction_rules), - found_proof = found_proof} - fun print_used_facts used_facts used_from = tag_list 1 used_from |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas - |> prefix ("Fact" ^ plural_s num_facts ^ " in " ^ name ^ - " proof (of " ^ string_of_int num_facts ^ "): ") + |> prefix ("Facts in " ^ name ^ " proof: ") |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = let val num_used_facts = length used_facts fun find_indices facts = tag_list 1 facts |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> distinct (eq_fst (op =)) |> map (prefix "@" o string_of_int o snd) fun filter_info (fact_filter, facts) = let val indices = find_indices facts (* "Int.max" is there for robustness -- it shouldn't be necessary *) val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" in (commas (indices @ unknowns), fact_filter) end val filter_infos = - map filter_info [("actual", used_from), facts] + map filter_info (("actual", used_from) :: factss) |> AList.group (op =) |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) in - "Success: Found proof with " ^ string_of_int num_used_facts ^ " of " ^ - string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ + "Success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^ + plural_s num_used_facts ^ (if num_used_facts = 0 then "" else ": " ^ commas filter_infos) end | spying_str_of_res {outcome = SOME failure, ...} = "Failure: " ^ string_of_atp_failure failure in - problem - |> get_minimizing_prover ctxt mode learn name params + get_minimizing_prover ctxt mode learn name params problem slice |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => print_used_facts used_facts used_from | _ => ()) |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) end fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) = let val output = if outcome = SOME ATP_Proof.TimedOut then SH_Timeout else if is_some outcome then SH_None else SH_Some result fun output_message () = message (fn () => play_one_line_proof minimize preplay_timeout used_facts state subgoal preferred_methss) in (output, output_message) end fun check_expected_outcome ctxt prover_name expect outcome = let val outcome_code = short_string_of_sledgehammer_outcome outcome in (* The "expect" argument is deliberately ignored if the prover is missing so that the "Metis_Examples" can be processed on any machine. *) if expect = "" orelse outcome_code = expect orelse not (is_prover_installed ctxt prover_name) then () else error ("Unexpected outcome: " ^ quote outcome_code) end fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result only - learn (problem as {state, subgoal, ...}) prover_name = + learn (problem as {state, subgoal, ...}) slice prover_name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout fun really_go () = - launch_prover params mode only learn problem prover_name + launch_prover params mode only learn problem slice prover_name |> preplay_prover_result params state subgoal fun go () = if debug then really_go () else (really_go () handle ERROR msg => (SH_Unknown, fn () => "Error: " ^ msg ^ "\n") | exn => if Exn.is_interrupt exn then Exn.reraise exn else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) val (outcome, message) = Timeout.apply hard_timeout go () val () = check_expected_outcome ctxt prover_name expect outcome val message = message () val () = (case outcome of SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message) | _ => ()) in (outcome, message) end val auto_try_max_facts_divisor = 2 (* FUDGE *) fun string_of_facts facts = "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^ (facts |> map (fst o fst) |> space_implode " ") fun string_of_factss factss = if forall (null o snd) factss then "Found no relevant facts" else cat_lines (map (fn (filter, facts) => (if filter = "" then "" else filter ^ ": ") ^ string_of_facts facts) factss) fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, ...}) mode writeln_result i (fact_override as {only, ...}) state = if null provers then error "No prover is set" else (case subgoal_count state of 0 => (error "No subgoal!"; (false, (SH_None, ""))) | n => let val _ = Proof.assert_backward state val print = if mode = Normal andalso is_none writeln_result then writeln else K () val found_proof = fn prover_name => if mode = Normal then (writeln_result |> the_default writeln) (prover_name ^ " found a proof...") else () val ctxt = Proof.context_of state val inst_inducts = induction_rules = SOME Instantiate val {facts = chained_thms, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt val _ = (case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name) | NONE => ()) val _ = print "Sledgehammering..." val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode")) val ({elapsed, ...}, all_facts) = Timing.timing (nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts) concl_t val _ = spying spy (fn () => (state, i, "All", "Extracting " ^ string_of_int (length all_facts) ^ " facts from background theory in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) val spying_str_of_factss = commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) fun get_factss provers = let val max_max_facts = (case max_facts of SOME n => n | NONE => 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)) val ({elapsed, ...}, factss) = Timing.timing (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t) all_facts val () = spying spy (fn () => (state, i, "All", "Filtering facts in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms (MaSh algorithm: " ^ str_of_mash_algorithm (the_mash_algorithm ()) ^ ")")); val () = if verbose then print (string_of_factss factss) else () val () = spying spy (fn () => (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)) in factss end fun launch_provers () = let - val facts = hd (get_factss provers) (* temporary *) val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = facts, found_proof = found_proof} + factss = get_factss provers, found_proof = found_proof} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) val launch = launch_prover_and_preplay params mode writeln_result only learn in if mode = Auto_Try then (SH_Unknown, "") |> fold (fn prover => - fn accum as (SH_Some _, _) => accum - | _ => launch problem prover) + fn accum as (SH_Some _, _) => accum + | _ => launch problem (get_default_slice ctxt prover) prover) provers else (learn chained_thms; provers - |> Par_List.map (launch problem) + |> Par_List.map (fn prover => launch problem (get_default_slice ctxt prover) prover) |> max_outcome) end in (launch_provers () handle Timeout.TIMEOUT _ => (SH_Timeout, "")) |> `(fn (outcome, _) => (case outcome of SH_Some _ => (print "QED"; true) | SH_Timeout => (print "Timed out"; false) | _ => (print "Done"; false))) end) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML @@ -1,708 +1,708 @@ (* Title: HOL/Tools/ATP/atp_systems.ML Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Setup for supported ATPs. *) signature SLEDGEHAMMER_ATP_SYSTEMS = sig type term_order = ATP_Problem.term_order type atp_format = ATP_Problem.atp_format type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure - type atp_slice_spec = (int * string) * atp_format * string * string * bool * string + type atp_slice = (int * string) * atp_format * string * string * bool * string type atp_config = {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, - best_slices : Proof.context -> atp_slice_spec list, + best_slices : Proof.context -> atp_slice list, best_max_mono_iters : int, best_max_new_mono_instances : int} val default_max_mono_iters : int val default_max_new_mono_instances : int val term_order : string Config.T val e_smartN : string val e_autoN : string val e_fun_weightN : string val e_sym_offset_weightN : string val e_selection_heuristic : string Config.T val e_default_fun_weight : real Config.T val e_fun_weight_base : real Config.T val e_fun_weight_span : real Config.T val e_default_sym_offs_weight : real Config.T val e_sym_offs_weight_base : real Config.T val e_sym_offs_weight_span : real Config.T val spass_H1SOS : string val spass_H2 : string val spass_H2LR0LT0 : string val spass_H2NuVS0 : string val spass_H2NuVS0Red2 : string val spass_H2SOS : string val isabelle_scala_function: string list * string list val remote_atp : string -> string -> string list -> (string * string) list -> - (atp_failure * string) list -> atp_formula_role -> (Proof.context -> atp_slice_spec) -> + (atp_failure * string) list -> atp_formula_role -> (Proof.context -> atp_slice) -> string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) val supported_atps : theory -> string list val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit val effective_term_order : Proof.context -> string -> term_order end; structure Sledgehammer_ATP_Systems : SLEDGEHAMMER_ATP_SYSTEMS = struct open ATP_Problem open ATP_Proof open ATP_Problem_Generate (* ATP configuration *) val TF0 = TFF (Monomorphic, Without_FOOL) val TF1 = TFF (Polymorphic, Without_FOOL) val TX0 = TFF (Monomorphic, With_FOOL {with_ite = true, with_let = true}) val TX1 = TFF (Polymorphic, With_FOOL {with_ite = true, with_let = true}) val TH0 = THF (Monomorphic, {with_ite = true, with_let = true}, THF_With_Choice) val TH1 = THF (Polymorphic, {with_ite = true, with_let = true}, THF_With_Choice) val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 100 (* FUDGE *) -type atp_slice_spec = (int * string) * atp_format * string * string * bool * string +type atp_slice = (int * string) * atp_format * string * string * bool * string type atp_config = {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, - best_slices : Proof.context -> atp_slice_spec list, + best_slices : Proof.context -> atp_slice list, best_max_mono_iters : int, best_max_new_mono_instances : int} (* "best_slices" must be found empirically, taking a holistic approach since the ATPs are run in parallel. Each slice has the format (time_frac, ((max_facts, fact_filter), format, type_enc, lam_trans, uncurried_aliases), extra) where time_frac = faction of the time available given to the slice (which should add up to 1.0) extra = extra information to the prover (e.g., SOS or no SOS). The last slice should be the most "normal" one, because it will get all the time available if the other slices fail early and also because it is used if slicing is disabled (e.g., by the minimizer). *) val mepoN = "mepo" val mashN = "mash" val meshN = "mesh" val tstp_proof_delims = [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"), ("% SZS output start Refutation", "% SZS output end Refutation"), ("% SZS output start Proof", "% SZS output end Proof")] fun known_szs_failures wrap = [(Unprovable, wrap "CounterSatisfiable"), (Unprovable, wrap "Satisfiable"), (GaveUp, wrap "GaveUp"), (GaveUp, wrap "Unknown"), (GaveUp, wrap "Incomplete"), (ProofMissing, wrap "Theorem"), (ProofMissing, wrap "Unsatisfiable"), (TimedOut, wrap "Timeout"), (Inappropriate, wrap "Inappropriate"), (OutOfResources, wrap "ResourceOut"), (OutOfResources, wrap "MemoryOut"), (Interrupted, wrap "Forced"), (Interrupted, wrap "User")] val known_szs_status_failures = known_szs_failures (prefix "SZS status ") val known_says_failures = known_szs_failures (prefix " says ") structure Data = Theory_Data ( type T = ((unit -> atp_config) * stamp) Symtab.table val empty = Symtab.empty fun merge data : T = Symtab.merge (eq_snd (op =)) data handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) ) fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000) val sosN = "sos" val no_sosN = "no_sos" val smartN = "smart" (* val kboN = "kbo" *) val lpoN = "lpo" val xweightsN = "_weights" val xprecN = "_prec" val xsimpN = "_simp" (* SPASS-specific *) (* Possible values for "atp_term_order": "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *) val term_order = Attrib.setup_config_string \<^binding>\atp_term_order\ (K smartN) (* agsyHOL *) val agsyhol_config : atp_config = {exec = (["AGSYHOL_HOME"], ["agsyHOL"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => ["--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [((60, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val agsyhol = (agsyholN, fn () => agsyhol_config) (* Alt-Ergo *) val alt_ergo_config : atp_config = {exec = (["WHY3_HOME"], ["why3"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => ["--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], proof_delims = [], known_failures = [(ProofMissing, ": Valid"), (TimedOut, ": Timeout"), (GaveUp, ": Unknown")], prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) [((100, meshN), TF1, "poly_native", liftingN, false, "")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val alt_ergo = (alt_ergoN, fn () => alt_ergo_config) (* E *) val e_smartN = "smart" val e_autoN = "auto" val e_fun_weightN = "fun_weight" val e_sym_offset_weightN = "sym_offset_weight" val e_selection_heuristic = Attrib.setup_config_string \<^binding>\atp_e_selection_heuristic\ (K e_smartN) (* FUDGE *) val e_default_fun_weight = Attrib.setup_config_real \<^binding>\atp_e_default_fun_weight\ (K 20.0) val e_fun_weight_base = Attrib.setup_config_real \<^binding>\atp_e_fun_weight_base\ (K 0.0) val e_fun_weight_span = Attrib.setup_config_real \<^binding>\atp_e_fun_weight_span\ (K 40.0) val e_default_sym_offs_weight = Attrib.setup_config_real \<^binding>\atp_e_default_sym_offs_weight\ (K 1.0) val e_sym_offs_weight_base = Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_base\ (K ~20.0) val e_sym_offs_weight_span = Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_span\ (K 60.0) fun e_selection_heuristic_case heuristic fw sow = if heuristic = e_fun_weightN then fw else if heuristic = e_sym_offset_weightN then sow else raise Fail ("unexpected " ^ quote heuristic) fun scaled_e_selection_weight ctxt heuristic w = w * Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_span e_sym_offs_weight_span) + Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_base e_sym_offs_weight_base) |> Real.ceil |> signed_string_of_int fun e_selection_weight_arguments ctxt heuristic sel_weights = if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then (* supplied by Stephan Schulz *) "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ \--destructive-er-aggressive --destructive-er --presat-simplify \ \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^ e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^ "(SimulateSOS," ^ (e_selection_heuristic_case heuristic e_default_fun_weight e_default_sym_offs_weight |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^ ",20,1.5,1.5,1" ^ (sel_weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_selection_weight ctxt heuristic w) |> implode) ^ "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ \FIFOWeight(PreferProcessed))' " else "-xAuto " val e_ord_weights = map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode "," fun e_ord_precedence [_] = "" | e_ord_precedence info = info |> map fst |> space_implode "<" fun e_term_order_info_arguments false false _ = "" | e_term_order_info_arguments gen_weights gen_prec ord_info = let val ord_info = ord_info () in (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^ (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "") end val e_config : atp_config = {exec = (["E_HOME"], ["eprover-ho", "eprover"]), arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => ["--auto-schedule --tstp-in --tstp-out --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path problem], proof_delims = [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ tstp_proof_delims, known_failures = [(TimedOut, "Failure: Resource limit exceeded (time)"), (TimedOut, "time limit exceeded")] @ known_szs_status_failures, prem_role = Conjecture, best_slices = fn ctxt => let val heuristic = Config.get ctxt e_selection_heuristic val (format, enc, main_lam_trans) = if string_ord (getenv "E_VERSION", "2.7") <> LESS then (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) else if string_ord (getenv "E_VERSION", "2.6") <> LESS then (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) else (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN) in (* FUDGE *) if heuristic = e_smartN then [((128, meshN), format, enc, main_lam_trans, false, e_fun_weightN), ((128, mashN), format, enc, main_lam_trans, false, e_sym_offset_weightN), ((91, mepoN), format, enc, main_lam_trans, false, e_autoN), ((1000, meshN), format, "poly_guards??", main_lam_trans, false, e_sym_offset_weightN), ((256, mepoN), format, enc, liftingN, false, e_fun_weightN), ((64, mashN), format, enc, combsN, false, e_fun_weightN)] else [((500, meshN), format, enc, combsN, false, heuristic)] end, best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val e = (eN, fn () => e_config) (* iProver *) val iprover_config : atp_config = {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^ "--clausifier_options \"--mode clausify\" " ^ "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem], proof_delims = tstp_proof_delims, known_failures = [(ProofIncomplete, "% SZS output start CNFRefutation")] @ known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [((150, meshN), FOF, "mono_guards??", liftingN, false, "")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val iprover = (iproverN, fn () => iprover_config) (* LEO-II *) val leo2_config : atp_config = {exec = (["LEO2_HOME"], ["leo.opt", "leo"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ => ["--foatp e --atp e=\"$E_HOME\"/eprover \ \--atp epclextract=\"$E_HOME\"/epclextract \ \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^ File.bash_path problem], proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "CPU time limit exceeded, terminating"), (GaveUp, "No.of.Axioms")] @ known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [((40, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val leo2 = (leo2N, fn () => leo2_config) (* Leo-III *) (* Include choice? Disabled now since it's disabled for Satallax as well. *) val leo3_config : atp_config = {exec = (["LEO3_HOME"], ["leo3"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ => [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \ \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ (if full_proofs then "--nleq --naeq " else "")], proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [((512, meshN), TH1, "mono_native_higher", keep_lamsN, false, "")], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val leo3 = (leo3N, fn () => leo3_config) (* Satallax *) (* Choice is disabled until there is proper reconstruction for it. *) val satallax_config : atp_config = {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => [(case getenv "E_HOME" of "" => "" | home => "-E " ^ home ^ "/eprover ") ^ "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], proof_delims = [("% SZS output start Proof", "% SZS output end Proof")], known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [((150, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val satallax = (satallaxN, fn () => satallax_config) (* SPASS *) val spass_H1SOS = "-Heuristic=1 -SOS" val spass_H2 = "-Heuristic=2" val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0" val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0" val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" val spass_H2SOS = "-Heuristic=2 -SOS" val spass_config : atp_config = let val format = DFG Monomorphic in {exec = (["SPASS_HOME"], ["SPASS"]), arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => fn _ => ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem |> extra_options <> "" ? prefix (extra_options ^ " ")], proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(GaveUp, "SPASS beiseite: Completion found"), (TimedOut, "SPASS beiseite: Ran out of time"), (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), (Unprovable, "No formulae and clauses found in input file"), (InternalError, "Please report this error")], prem_role = Conjecture, best_slices = fn _ => (* FUDGE *) [((150, meshN), format, "mono_native", combsN, true, ""), ((500, meshN), format, "mono_native", liftingN, true, spass_H2SOS), ((50, meshN), format, "mono_native", liftingN, true, spass_H2LR0LT0), ((250, meshN), format, "mono_native", combsN, true, spass_H2NuVS0), ((1000, mepoN), format, "mono_native", liftingN, true, spass_H1SOS), ((150, meshN), format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2), ((300, meshN), format, "mono_native", combsN, true, spass_H2SOS), ((100, meshN), format, "mono_native", combs_and_liftingN, true, spass_H2)], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} end val spass = (spassN, fn () => spass_config) (* Vampire *) val vampire_basic_options = "--proof tptp --output_axiom_names on" ^ (if ML_System.platform_is_windows then "" (*time slicing is not support in the Windows version of Vampire*) else " --mode casc") val vampire_full_proof_options = " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0" val vampire_config : atp_config = {exec = (["VAMPIRE_HOME"], ["vampire"]), arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ => [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^ " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem |> sos = sosN ? prefix "--sos on "], proof_delims = [("=========== Refutation ==========", "======= End of refutation =======")] @ tstp_proof_delims, known_failures = [(GaveUp, "UNPROVABLE"), (GaveUp, "CANNOT PROVE"), (Unprovable, "Satisfiability detected"), (Unprovable, "Termination reason: Satisfiable"), (Interrupted, "Aborted by signal SIGINT")] @ known_szs_status_failures, prem_role = Hypothesis, best_slices = fn ctxt => (* FUDGE *) [((500, meshN), TX1, "mono_native_fool", combs_or_liftingN, false, sosN), ((150, meshN), TX1, "poly_native_fool", combs_or_liftingN, false, sosN), ((50, meshN), TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} val vampire = (vampireN, fn () => vampire_config) (* Z3 with TPTP syntax (half experimental, half legacy) *) val z3_tptp_config : atp_config = {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem], proof_delims = [("SZS status Theorem", "")], known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [((250, meshN), TF0, "mono_native", combsN, false, ""), ((125, mepoN), TF0, "mono_native", combsN, false, ""), ((62, mashN), TF0, "mono_native", combsN, false, ""), ((31, meshN), TF0, "mono_native", combsN, false, "")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} val z3_tptp = (z3_tptpN, fn () => z3_tptp_config) (* Zipperposition *) val zipperposition_config : atp_config = let val format = THF (Polymorphic, {with_ite = true, with_let = false}, THF_Without_Choice) in {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]), arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ => ["--input tptp", "--output tptp", "--timeout " ^ Time.toString timeout, extra_options, File.bash_path problem], proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "SZS status ResourceOut")] @ (* odd way of timing out *) known_szs_status_failures, prem_role = Hypothesis, best_slices = fn _ => [((512, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1"), ((256, mashN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1"), ((128, mepoN), format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj"), ((1024, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1"), ((64, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=ignore --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15"), ((512, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true -o tptp --avatar=eager --split-only-ground=true")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} end val zipperposition = (zipperpositionN, fn () => zipperposition_config) (* Remote ATP invocation via SystemOnTPTP *) val no_remote_systems = {url = "", systems = [] : string list} val remote_systems = Synchronized.var "atp_remote_systems" no_remote_systems fun get_remote_systems () = Timeout.apply (seconds 10.0) SystemOnTPTP.list_systems () handle ERROR msg => (warning msg; no_remote_systems) | Timeout.TIMEOUT _ => no_remote_systems fun find_remote_system name [] systems = find_first (String.isPrefix (name ^ "---")) systems | find_remote_system name (version :: versions) systems = case find_first (String.isPrefix (name ^ "---" ^ version)) systems of NONE => find_remote_system name versions systems | res => res fun get_remote_system name versions = Synchronized.change_result remote_systems (fn remote => (if #url remote <> SystemOnTPTP.get_url () orelse null (#systems remote) then get_remote_systems () else remote) |> ` #systems) |> `(find_remote_system name versions) fun the_remote_system name versions = (case get_remote_system name versions of (SOME sys, _) => sys | (NONE, []) => error "SystemOnTPTP is currently not available" | (NONE, syss) => (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of [] => error "SystemOnTPTP is currently not available" | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg) | syss => error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^ commas_quote syss ^ ".)"))) val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"]) fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice = {exec = isabelle_scala_function, arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ => [the_remote_system system_name system_versions, Isabelle_System.absolute_path problem, command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)], proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_says_failures, prem_role = prem_role, best_slices = fn ctxt => [best_slice ctxt], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} : atp_config fun remotify_config system_name system_versions best_slice ({proof_delims, known_failures, prem_role, ...} : atp_config) = remote_config system_name system_versions proof_delims known_failures prem_role best_slice fun remote_atp name system_name system_versions proof_delims known_failures prem_role best_slice = (remote_prefix ^ name, fn () => remote_config system_name system_versions proof_delims known_failures prem_role best_slice) fun remotify_atp (name, config) system_name system_versions best_slice = (remote_prefix ^ name, remotify_config system_name system_versions best_slice o config) fun gen_remote_waldmeister name type_enc = remote_atp name "Waldmeister" ["710"] tstp_proof_delims ([(OutOfResources, "Too many function symbols"), (Inappropriate, "**** Unexpected end of file."), (Crashed, "Unrecoverable Segmentation Fault")] @ known_szs_status_failures) Hypothesis (K ((50, meshN), CNF_UEQ, type_enc, combsN, false, "") (* FUDGE *)) val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] (K ((60, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "") (* FUDGE *)) val remote_alt_ergo = remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] (K ((250, meshN), TF1, "poly_native", keep_lamsN, false, "") (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] (K ((750, meshN), TF0, "mono_native", combsN, false, "") (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] (K ((150, meshN), FOF, "mono_guards??", liftingN, false, "") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] (K ((40, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "") (* FUDGE *)) val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] (K ((150, meshN), THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "") (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" val remote_zipperposition = remotify_atp zipperposition "Zipperpin" ["2.1", "2.0"] (K ((512, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "") (* FUDGE *)) (* Dummy prover *) fun dummy_config prem_role format type_enc uncurried_aliases : atp_config = {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), arguments = K (K (K (K (K (K []))))), proof_delims = [], known_failures = known_szs_status_failures, prem_role = prem_role, best_slices = K [((200, "mepo"), format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, "")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val dummy_fof = (dummy_fofN, fn () => dummy_config Hypothesis FOF "mono_guards??" false) val dummy_tfx = (dummy_tfxN, fn () => dummy_config Hypothesis TX1 "poly_native_fool" false) val dummy_thf = (dummy_thfN, fn () => dummy_config Hypothesis TH1 "poly_native_higher" false) val dummy_thf_reduced = let val format = THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice) val config = dummy_config Hypothesis format "poly_native_higher" false in (dummy_thfN ^ "_reduced", fn () => config) end (* Setup *) fun add_atp (name, config) thy = Data.map (Symtab.update_new (name, (config, stamp ()))) thy handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) fun get_atp thy name = fst (the (Symtab.lookup (Data.get thy) name)) handle Option.Option => error ("Unknown ATP: " ^ name) val supported_atps = Symtab.keys o Data.get fun is_atp_installed thy name = let val {exec, ...} = get_atp thy name () in exists (fn var => getenv var <> "") (fst exec) end fun refresh_systems_on_tptp () = Synchronized.change remote_systems (fn _ => get_remote_systems ()) fun effective_term_order ctxt atp = let val ord = Config.get ctxt term_order in if ord = smartN then {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN), gen_simp = false} else let val is_lpo = String.isSubstring lpoN ord in {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord} end end val atps = [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced] val _ = Theory.setup (fold add_atp atps) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML @@ -1,1637 +1,1638 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_mash.ML Author: Jasmin Blanchette, TU Muenchen Author: Cezary Kaliszyk, University of Innsbruck Sledgehammer's machine-learning-based relevance filter (MaSh). *) signature SLEDGEHAMMER_MASH = sig type stature = ATP_Problem_Generate.stature type lazy_fact = Sledgehammer_Fact.lazy_fact type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override type params = Sledgehammer_Prover.params type prover_result = Sledgehammer_Prover.prover_result val trace : bool Config.T val duplicates : bool Config.T val MePoN : string val MaShN : string val MeShN : string val mepoN : string val mashN : string val meshN : string val unlearnN : string val learn_isarN : string val learn_proverN : string val relearn_isarN : string val relearn_proverN : string val fact_filters : string list val encode_str : string -> string val encode_strs : string list -> string val decode_str : string -> string val decode_strs : string -> string list datatype mash_algorithm = MaSh_NB | MaSh_kNN | MaSh_NB_kNN | MaSh_NB_Ext | MaSh_kNN_Ext val is_mash_enabled : unit -> bool val the_mash_algorithm : unit -> mash_algorithm val str_of_mash_algorithm : mash_algorithm -> string val mesh_facts : ('a list -> 'a list) -> ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list val nickname_of_thm : thm -> string val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list val crude_thm_ord : Proof.context -> thm ord val thm_less : thm * thm -> bool val goal_of_thm : theory -> thm -> thm val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm -> prover_result val features_of : Proof.context -> string -> stature -> term list -> string list val trim_dependencies : string list -> string list option val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option val prover_dependencies_of : Proof.context -> params -> string -> int -> lazy_fact list -> string Symtab.table * string Symtab.table -> thm -> bool * string list val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list val num_extra_feature_facts : int val extra_feature_factor : real val weight_facts_smoothly : 'a list -> ('a * real) list val weight_facts_steeply : 'a list -> ('a * real) list val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list -> ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term -> lazy_fact list -> fact list * fact list val mash_unlearn : Proof.context -> unit val mash_learn_proof : Proof.context -> params -> term -> thm list -> unit val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time -> lazy_fact list -> string val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit val mash_can_suggest_facts : Proof.context -> bool val mash_can_suggest_facts_fast : Proof.context -> bool val generous_max_suggestions : int -> int val mepo_weight : real val mash_weight : real val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> lazy_fact list -> (string * fact list) list end; structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = struct open ATP_Util open ATP_Problem_Generate open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Prover open Sledgehammer_Prover_Minimize open Sledgehammer_MePo val anonymous_proof_prefix = "." val trace = Attrib.setup_config_bool \<^binding>\sledgehammer_mash_trace\ (K false) val duplicates = Attrib.setup_config_bool \<^binding>\sledgehammer_fact_duplicates\ (K false) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () fun gen_eq_thm ctxt = if Config.get ctxt duplicates then Thm.eq_thm_strict else Thm.eq_thm_prop val MePoN = "MePo" val MaShN = "MaSh" val MeShN = "MeSh" val mepoN = "mepo" val mashN = "mash" val meshN = "mesh" val fact_filters = [meshN, mepoN, mashN] val unlearnN = "unlearn" val learn_isarN = "learn_isar" val learn_proverN = "learn_prover" val relearn_isarN = "relearn_isar" val relearn_proverN = "relearn_prover" fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i))) type xtab = int * int Symtab.table val empty_xtab = (0, Symtab.empty) fun add_to_xtab key (next, tab) = (next + 1, Symtab.update_new (key, next) tab) fun maybe_add_to_xtab key = perhaps (try (add_to_xtab key)) fun state_file () = Path.expand (Path.explode "$ISABELLE_HOME_USER/mash_state") val remove_state_file = try File.rm o state_file datatype mash_algorithm = MaSh_NB | MaSh_kNN | MaSh_NB_kNN | MaSh_NB_Ext | MaSh_kNN_Ext fun mash_algorithm () = (case Options.default_string \<^system_option>\MaSh\ of "yes" => SOME MaSh_NB_kNN | "sml" => SOME MaSh_NB_kNN | "nb" => SOME MaSh_NB | "knn" => SOME MaSh_kNN | "nb_knn" => SOME MaSh_NB_kNN | "nb_ext" => SOME MaSh_NB_Ext | "knn_ext" => SOME MaSh_kNN_Ext | "none" => NONE | "" => NONE | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm); NONE)) val is_mash_enabled = is_some o mash_algorithm val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm fun str_of_mash_algorithm MaSh_NB = "nb" | str_of_mash_algorithm MaSh_kNN = "knn" | str_of_mash_algorithm MaSh_NB_kNN = "nb_knn" | str_of_mash_algorithm MaSh_NB_Ext = "nb_ext" | str_of_mash_algorithm MaSh_kNN_Ext = "knn_ext" fun scaled_avg [] = 0 | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs fun avg [] = 0.0 | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs) fun normalize_scores _ [] = [] | normalize_scores max_facts xs = map (apsnd (curry (op *) (1.0 / avg (map snd (take max_facts xs))))) xs fun mesh_facts maybe_distinct _ max_facts [(_, (sels, unks))] = map fst (take max_facts sels) @ take (max_facts - length sels) unks |> maybe_distinct | mesh_facts _ fact_eq max_facts mess = let val mess = mess |> map (apsnd (apfst (normalize_scores max_facts))) fun score_in fact (global_weight, (sels, unks)) = let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in (case find_index (curry fact_eq fact o fst) sels of ~1 => if member fact_eq unks fact then NONE else SOME 0.0 | rank => score_at rank) end fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg in fold (union fact_eq o map fst o take max_facts o fst o snd) mess [] |> map (`weight_of) |> sort (int_ord o apply2 fst o swap) |> map snd |> take max_facts end fun smooth_weight_of_fact rank = Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0 (* FUDGE *) fun steep_weight_of_fact rank = Math.pow (0.62, log2 (Real.fromInt (rank + 1))) (* FUDGE *) fun weight_facts_smoothly facts = map_index (swap o apfst smooth_weight_of_fact) facts fun weight_facts_steeply facts = map_index (swap o apfst steep_weight_of_fact) facts fun sort_array_suffix cmp needed a = let exception BOTTOM of int val al = Array.length a fun maxson l i = let val i31 = i + i + i + 1 in if i31 + 2 < l then let val x = Unsynchronized.ref i31 in if is_less (cmp (Array.sub (a, i31), Array.sub (a, i31 + 1))) then x := i31 + 1 else (); if is_less (cmp (Array.sub (a, !x), Array.sub (a, i31 + 2))) then x := i31 + 2 else (); !x end else if i31 + 1 < l andalso is_less (cmp (Array.sub (a, i31), Array.sub (a, i31 + 1))) then i31 + 1 else if i31 < l then i31 else raise BOTTOM i end fun trickledown l i e = let val j = maxson l i in if is_greater (cmp (Array.sub (a, j), e)) then (Array.update (a, i, Array.sub (a, j)); trickledown l j e) else Array.update (a, i, e) end fun trickle l i e = trickledown l i e handle BOTTOM i => Array.update (a, i, e) fun bubbledown l i = let val j = maxson l i in Array.update (a, i, Array.sub (a, j)); bubbledown l j end fun bubble l i = bubbledown l i handle BOTTOM i => i fun trickleup i e = let val father = (i - 1) div 3 in if is_less (cmp (Array.sub (a, father), e)) then (Array.update (a, i, Array.sub (a, father)); if father > 0 then trickleup father e else Array.update (a, 0, e)) else Array.update (a, i, e) end fun for i = if i < 0 then () else (trickle al i (Array.sub (a, i)); for (i - 1)) fun for2 i = if i < Integer.max 2 (al - needed) then () else let val e = Array.sub (a, i) in Array.update (a, i, Array.sub (a, 0)); trickleup (bubble i 0) e; for2 (i - 1) end in for (((al + 1) div 3) - 1); for2 (al - 1); if al > 1 then let val e = Array.sub (a, 1) in Array.update (a, 1, Array.sub (a, 0)); Array.update (a, 0, e) end else () end fun rev_sort_list_prefix cmp needed xs = let val ary = Array.fromList xs in sort_array_suffix cmp needed ary; Array.foldl (op ::) [] ary end (*** Convenience functions for synchronized access ***) fun synchronized_timed_value var time_limit = Synchronized.timed_access var time_limit (fn value => SOME (value, value)) fun synchronized_timed_change_result var time_limit f = Synchronized.timed_access var time_limit (SOME o f) fun synchronized_timed_change var time_limit f = synchronized_timed_change_result var time_limit (fn x => ((), f x)) fun mash_time_limit _ = SOME (seconds 0.1) (*** Isabelle-agnostic machine learning ***) structure MaSh = struct fun select_fact_idxs (big_number : real) recommends = List.app (fn at => let val (j, ov) = Array.sub (recommends, at) in Array.update (recommends, at, (j, big_number + ov)) end) fun wider_array_of_vector init vec = let val ary = Array.array init in Array.copyVec {src = vec, dst = ary, di = 0}; ary end val nb_def_prior_weight = 1000 (* FUDGE *) fun learn_facts (tfreq0, sfreq0, dffreq0) num_facts0 num_facts num_feats depss featss = let val tfreq = wider_array_of_vector (num_facts, 0) tfreq0 val sfreq = wider_array_of_vector (num_facts, Inttab.empty) sfreq0 val dffreq = wider_array_of_vector (num_feats, 0) dffreq0 fun learn_one th feats deps = let fun add_th weight t = let val im = Array.sub (sfreq, t) fun fold_fn s = Inttab.map_default (s, 0) (Integer.add weight) in map_array_at tfreq (Integer.add weight) t; Array.update (sfreq, t, fold fold_fn feats im) end val add_sym = map_array_at dffreq (Integer.add 1) in add_th nb_def_prior_weight th; List.app (add_th 1) deps; List.app add_sym feats end fun for i = if i = num_facts then () else (learn_one i (Vector.sub (featss, i)) (Vector.sub (depss, i)); for (i + 1)) in for num_facts0; (Array.vector tfreq, Array.vector sfreq, Array.vector dffreq) end fun naive_bayes (tfreq, sfreq, dffreq) num_facts max_suggs fact_idxs goal_feats = let val tau = 0.2 (* FUDGE *) val pos_weight = 5.0 (* FUDGE *) val def_val = ~18.0 (* FUDGE *) val init_val = 30.0 (* FUDGE *) val ln_afreq = Math.ln (Real.fromInt num_facts) val idf = Vector.map (fn i => ln_afreq - Math.ln (Real.fromInt i)) dffreq fun tfidf feat = Vector.sub (idf, feat) fun log_posterior i = let val tfreq = Real.fromInt (Vector.sub (tfreq, i)) fun add_feat (f, fw0) (res, sfh) = (case Inttab.lookup sfh f of SOME sf => (res + fw0 * tfidf f * Math.ln (pos_weight * Real.fromInt sf / tfreq), Inttab.delete f sfh) | NONE => (res + fw0 * tfidf f * def_val, sfh)) val (res, sfh) = fold add_feat goal_feats (init_val * Math.ln tfreq, Vector.sub (sfreq, i)) fun fold_sfh (f, sf) sow = sow + tfidf f * Math.ln (1.0 - Real.fromInt (sf - 1) / tfreq) val sum_of_weights = Inttab.fold fold_sfh sfh 0.0 in res + tau * sum_of_weights end val posterior = Array.tabulate (num_facts, (fn j => (j, log_posterior j))) fun ret at acc = if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc) in select_fact_idxs 100000.0 posterior fact_idxs; sort_array_suffix (Real.compare o apply2 snd) max_suggs posterior; ret (Integer.max 0 (num_facts - max_suggs)) [] end val initial_k = 0 fun k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs fact_idxs goal_feats = let exception EXIT of unit val ln_afreq = Math.ln (Real.fromInt num_facts) fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat))) val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0) val feat_facts = Array.array (num_feats, []) val _ = Vector.foldl (fn (feats, fact) => (List.app (map_array_at feat_facts (cons fact)) feats; fact + 1)) 0 featss fun do_feat (s, sw0) = let val sw = sw0 * tfidf s val w6 = Math.pow (sw, 6.0 (* FUDGE *)) fun inc_overlap j = let val (_, ov) = Array.sub (overlaps_sqr, j) in Array.update (overlaps_sqr, j, (j, w6 + ov)) end in List.app inc_overlap (Array.sub (feat_facts, s)) end val _ = List.app do_feat goal_feats val _ = sort_array_suffix (Real.compare o apply2 snd) num_facts overlaps_sqr val no_recommends = Unsynchronized.ref 0 val recommends = Array.tabulate (num_facts, rpair 0.0) val age = Unsynchronized.ref 500000000.0 fun inc_recommend v j = let val (_, ov) = Array.sub (recommends, j) in if ov <= 0.0 then (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov))) else Array.update (recommends, j, (j, v + ov)) end val k = Unsynchronized.ref 0 fun do_k k = if k >= num_facts then raise EXIT () else let val deps_factor = 2.7 (* FUDGE *) val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1) val _ = inc_recommend o2 j val ds = Vector.sub (depss, j) val l = Real.fromInt (length ds) in List.app (inc_recommend (deps_factor * o2 / l)) ds end fun while1 () = if !k = initial_k + 1 then () else (do_k (!k); k := !k + 1; while1 ()) handle EXIT () => () fun while2 () = if !no_recommends >= max_suggs then () else (do_k (!k); k := !k + 1; age := !age - 10000.0; while2 ()) handle EXIT () => () fun ret acc at = if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1) in while1 (); while2 (); select_fact_idxs 1000000000.0 recommends fact_idxs; sort_array_suffix (Real.compare o apply2 snd) max_suggs recommends; ret [] (Integer.max 0 (num_facts - max_suggs)) end (* experimental *) fun external_tool tool max_suggs learns goal_feats = let val ser = string_of_int (serial ()) (* poor person's attempt at thread-safety *) val ocs = TextIO.openOut ("adv_syms" ^ ser) val ocd = TextIO.openOut ("adv_deps" ^ ser) val ocq = TextIO.openOut ("adv_seq" ^ ser) val occ = TextIO.openOut ("adv_conj" ^ ser) fun os oc s = TextIO.output (oc, s) fun ol _ _ _ [] = () | ol _ f _ [e] = f e | ol oc f sep (h :: t) = (f h; os oc sep; ol oc f sep t) fun do_learn (name, feats, deps) = (os ocs name; os ocs ":"; ol ocs (os ocs o quote) ", " feats; os ocs "\n"; os ocd name; os ocd ":"; ol ocd (os ocd) " " deps; os ocd "\n"; os ocq name; os ocq "\n") fun forkexec no = let val cmd = "~/misc/" ^ tool ^ " adv_syms" ^ ser ^ " adv_deps" ^ ser ^ " " ^ string_of_int no ^ " adv_seq" ^ ser ^ " < adv_conj" ^ ser in fst (Isabelle_System.bash_output cmd) |> space_explode " " |> filter_out (curry (op =) "") end in (List.app do_learn learns; ol occ (os occ o quote) ", " (map fst goal_feats); TextIO.closeOut ocs; TextIO.closeOut ocd; TextIO.closeOut ocq; TextIO.closeOut occ; forkexec max_suggs) end fun k_nearest_neighbors_ext max_suggs = external_tool ("newknn/knn" ^ " " ^ string_of_int initial_k) max_suggs fun naive_bayes_ext max_suggs = external_tool "predict/nbayes" max_suggs fun query_external ctxt algorithm max_suggs learns goal_feats = (trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats)); (case algorithm of MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats | MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats)) fun query_internal ctxt algorithm num_facts num_feats (fact_names, featss, depss) (freqs as (_, _, dffreq)) fact_idxs max_suggs goal_feats int_goal_feats = let fun nb () = naive_bayes freqs num_facts max_suggs fact_idxs int_goal_feats |> map fst fun knn () = k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs fact_idxs int_goal_feats |> map fst in (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^ elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}"); (case algorithm of MaSh_NB => nb () | MaSh_kNN => knn () | MaSh_NB_kNN => mesh_facts I (op =) max_suggs [(0.5 (* FUDGE *), (weight_facts_steeply (nb ()), [])), (0.5 (* FUDGE *), (weight_facts_steeply (knn ()), []))]) |> map (curry Vector.sub fact_names)) end end; (*** Persistent, stringly-typed state ***) fun meta_char c = if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse c = #"," orelse c = #"'" then String.str c else (* fixed width, in case more digits follow *) "%" ^ stringN_of_int 3 (Char.ord c) fun unmeta_chars accum [] = String.implode (rev accum) | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) = (case Int.fromString (String.implode [d1, d2, d3]) of SOME n => unmeta_chars (Char.chr n :: accum) cs | NONE => "" (* error *)) | unmeta_chars _ (#"%" :: _) = "" (* error *) | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs val encode_str = String.translate meta_char val encode_strs = map encode_str #> space_implode " " fun decode_str s = if String.isSubstring "%" s then unmeta_chars [] (String.explode s) else s; fun decode_strs s = space_explode " " s |> String.isSubstring "%" s ? map decode_str; datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop fun str_of_proof_kind Isar_Proof = "i" | str_of_proof_kind Automatic_Proof = "a" | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x" fun proof_kind_of_str "a" = Automatic_Proof | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop | proof_kind_of_str _ (* "i" *) = Isar_Proof fun add_edge_to name parent = Graph.default_node (parent, (Isar_Proof, [], [])) #> Graph.add_edge (parent, name) fun add_node kind name parents feats deps (accum as (access_G, (fact_xtab, feat_xtab), learns)) = let val fact_xtab' = add_to_xtab name fact_xtab in ((Graph.new_node (name, (kind, feats, deps)) access_G handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G) |> fold (add_edge_to name) parents, (fact_xtab', fold maybe_add_to_xtab feats feat_xtab), (name, feats, deps) :: learns) end handle Symtab.DUP _ => accum (* robustness (in case the state file violates the invariant) *) fun try_graph ctxt when def f = f () handle Graph.CYCLES (cycle :: _) => (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def) | Graph.DUP name => (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def) | Graph.UNDEF name => (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def) | exn => if Exn.is_interrupt exn then Exn.reraise exn else (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn); def) fun graph_info G = string_of_int (length (Graph.keys G)) ^ " node(s), " ^ string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ " edge(s), " ^ string_of_int (length (Graph.maximals G)) ^ " maximal" type ffds = string vector * int list vector * int list vector type freqs = int vector * int Inttab.table vector * int vector type mash_state = {access_G : (proof_kind * string list * string list) Graph.T, xtabs : xtab * xtab, ffds : ffds, freqs : freqs, dirty_facts : string list option} val empty_xtabs = (empty_xtab, empty_xtab) val empty_ffds = (Vector.fromList [], Vector.fromList [], Vector.fromList []) : ffds val empty_freqs = (Vector.fromList [], Vector.fromList [], Vector.fromList []) : freqs val empty_state = {access_G = Graph.empty, xtabs = empty_xtabs, ffds = empty_ffds, freqs = empty_freqs, dirty_facts = SOME []} : mash_state fun recompute_ffds_freqs_from_learns (learns : (string * string list * string list) list) ((num_facts, fact_tab), (num_feats, feat_tab)) num_facts0 (fact_names0, featss0, depss0) freqs0 = let val fact_names = Vector.concat [fact_names0, Vector.fromList (map #1 learns)] val featss = Vector.concat [featss0, Vector.fromList (map (map_filter (Symtab.lookup feat_tab) o #2) learns)] val depss = Vector.concat [depss0, Vector.fromList (map (map_filter (Symtab.lookup fact_tab) o #3) learns)] in ((fact_names, featss, depss), MaSh.learn_facts freqs0 num_facts0 num_facts num_feats depss featss) end fun reorder_learns (num_facts, fact_tab) learns = let val ary = Array.array (num_facts, ("", [], [])) in List.app (fn learn as (fact, _, _) => Array.update (ary, the (Symtab.lookup fact_tab fact), learn)) learns; Array.foldr (op ::) [] ary end fun recompute_ffds_freqs_from_access_G access_G (xtabs as (fact_xtab, _)) = let val learns = Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G |> reorder_learns fact_xtab in recompute_ffds_freqs_from_learns learns xtabs 0 empty_ffds empty_freqs end local val version = "*** MaSh version 20190121 ***" exception FILE_VERSION_TOO_NEW of unit fun extract_node line = (case space_explode ":" line of [head, tail] => (case (space_explode " " head, map (unprefix " ") (space_explode ";" tail)) of ([kind, name], [parents, feats, deps]) => SOME (proof_kind_of_str kind, decode_str name, decode_strs parents, decode_strs feats, decode_strs deps) | _ => NONE) | _ => NONE) fun would_load_state (memory_time, _) = let val path = state_file () in (case try OS.FileSys.modTime (File.platform_path path) of NONE => false | SOME disk_time => memory_time < disk_time) end; fun load_state ctxt (time_state as (memory_time, _)) = let val path = state_file () in (case try OS.FileSys.modTime (File.platform_path path) of NONE => time_state | SOME disk_time => if memory_time >= disk_time then time_state else (disk_time, (case try File.read_lines path of SOME (version' :: node_lines) => let fun extract_line_and_add_node line = (case extract_node line of NONE => I (* should not happen *) | SOME (kind, name, parents, feats, deps) => add_node kind name parents feats deps) val empty_G_etc = (Graph.empty, empty_xtabs, []) val (access_G, xtabs, rev_learns) = (case string_ord (version', version) of EQUAL => try_graph ctxt "loading state" empty_G_etc (fn () => fold extract_line_and_add_node node_lines empty_G_etc) | LESS => (remove_state_file (); empty_G_etc) (* cannot parse old file *) | GREATER => raise FILE_VERSION_TOO_NEW ()) val (ffds, freqs) = recompute_ffds_freqs_from_learns (rev rev_learns) xtabs 0 empty_ffds empty_freqs in trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")"); {access_G = access_G, xtabs = xtabs, ffds = ffds, freqs = freqs, dirty_facts = SOME []} end | _ => empty_state))) end fun str_of_entry (kind, name, parents, feats, deps) = str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs feats ^ "; " ^ encode_strs deps ^ "\n" fun save_state _ (time_state as (_, {dirty_facts = SOME [], ...})) = time_state | save_state ctxt (memory_time, {access_G, xtabs, ffds, freqs, dirty_facts}) = let fun append_entry (name, ((kind, feats, deps), (parents, _))) = cons (kind, name, Graph.Keys.dest parents, feats, deps) val path = state_file () val dirty_facts' = (case try OS.FileSys.modTime (File.platform_path path) of NONE => NONE | SOME disk_time => if disk_time <= memory_time then dirty_facts else NONE) val (banner, entries) = (case dirty_facts' of SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names []) | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])) in (case banner of SOME s => File.write path s | NONE => (); entries |> chunk_list 500 |> List.app (File.append path o implode o map str_of_entry)) handle IO.Io _ => (); trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info access_G ^ (case dirty_facts of SOME dirty_facts => "; " ^ string_of_int (length dirty_facts) ^ " dirty fact(s)" | _ => "") ^ ")"); (Time.now (), {access_G = access_G, xtabs = xtabs, ffds = ffds, freqs = freqs, dirty_facts = SOME []}) end val global_state = Synchronized.var "Sledgehammer_MaSh.global_state" (Time.zeroTime, empty_state) in fun map_state ctxt f = (trace_msg ctxt (fn () => "Changing MaSh state"); synchronized_timed_change global_state mash_time_limit (load_state ctxt ##> f #> save_state ctxt)) |> ignore handle FILE_VERSION_TOO_NEW () => () fun peek_state ctxt = (trace_msg ctxt (fn () => "Peeking at MaSh state"); (case synchronized_timed_value global_state mash_time_limit of NONE => NONE | SOME state => if would_load_state state then NONE else SOME state)) fun get_state ctxt = (trace_msg ctxt (fn () => "Retrieving MaSh state"); synchronized_timed_change_result global_state mash_time_limit (perhaps (try (load_state ctxt)) #> `snd)) fun clear_state ctxt = (trace_msg ctxt (fn () => "Clearing MaSh state"); Synchronized.change global_state (fn _ => (remove_state_file (); (Time.zeroTime, empty_state)))) end (*** Isabelle helpers ***) fun crude_printed_term size t = let fun term _ (res, 0) = (res, 0) | term (t $ u) (res, size) = let val (res, size) = term t (res ^ "(", size) val (res, size) = term u (res ^ " ", size) in (res ^ ")", size) end | term (Abs (s, _, t)) (res, size) = term t (res ^ "%" ^ s ^ ".", size - 1) | term (Bound n) (res, size) = (res ^ "#" ^ string_of_int n, size - 1) | term (Const (s, _)) (res, size) = (res ^ Long_Name.base_name s, size - 1) | term (Free (s, _)) (res, size) = (res ^ s, size - 1) | term (Var ((s, _), _)) (res, size) = (res ^ s, size - 1) in fst (term t ("", size)) end fun nickname_of_thm th = if Thm.has_name_hint th then let val hint = Thm.get_name_hint th in (* There must be a better way to detect local facts. *) (case Long_Name.dest_local hint of SOME suf => Long_Name.implode [Thm.theory_name th, suf, crude_printed_term 25 (Thm.prop_of th)] | NONE => hint) end else crude_printed_term 50 (Thm.prop_of th) fun find_suggested_facts ctxt facts = let fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) val tab = fold add facts Symtab.empty fun lookup nick = Symtab.lookup tab nick |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) | _ => ()) in map_filter lookup end fun free_feature_of s = "f" ^ s fun thy_feature_of s = "y" ^ s fun type_feature_of s = "t" ^ s fun class_feature_of s = "s" ^ s val local_feature = "local" fun crude_thm_ord ctxt = let val ancestor_lengths = fold (fn thy => Symtab.update (Context.theory_name thy, length (Context.ancestors_of thy))) (Theory.nodes_of (Proof_Context.theory_of ctxt)) Symtab.empty val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name fun crude_theory_ord p = if Context.eq_thy_id p then EQUAL else if Context.proper_subthy_id p then LESS else if Context.proper_subthy_id (swap p) then GREATER else (case apply2 ancestor_length p of (SOME m, SOME n) => (case int_ord (m, n) of EQUAL => string_ord (apply2 Context.theory_id_name p) | ord => ord) | _ => string_ord (apply2 Context.theory_id_name p)) in fn p => (case crude_theory_ord (apply2 Thm.theory_id p) of EQUAL => (* The hack below is necessary because of odd dependencies that are not reflected in the theory comparison. *) let val q = apply2 nickname_of_thm p in (* Hack to put "xxx_def" before "xxxI" and "xxxE" *) (case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of EQUAL => string_ord q | ord => ord) end | ord => ord) end; val thm_less_eq = Context.subthy_id o apply2 Thm.theory_id fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p)) val freezeT = Type.legacy_freeze_type fun freeze (t $ u) = freeze t $ freeze u | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) | freeze (Var ((s, _), T)) = Free (s, freezeT T) | freeze (Const (s, T)) = Const (s, freezeT T) | freeze (Free (s, T)) = Free (s, freezeT T) | freeze t = t fun goal_of_thm thy = Thm.prop_of #> freeze #> Thm.global_cterm_of thy #> Goal.init fun run_prover_for_mash ctxt params prover goal_name facts goal = let val problem = {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, - subgoal_count = 1, facts = ("", facts), found_proof = K ()} + subgoal_count = 1, factss = [("", facts)], found_proof = K ()} + val slice = get_default_slice ctxt prover in - get_minimizing_prover ctxt MaSh (K ()) prover params problem + get_minimizing_prover ctxt MaSh (K ()) prover params problem slice end val bad_types = [\<^type_name>\prop\, \<^type_name>\bool\, \<^type_name>\fun\] val crude_str_of_sort = space_implode "," o map Long_Name.base_name o subtract (op =) \<^sort>\type\ fun crude_str_of_typ (Type (s, [])) = Long_Name.base_name s | crude_str_of_typ (Type (s, Ts)) = Long_Name.base_name s ^ implode (map crude_str_of_typ Ts) | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S fun maybe_singleton_str "" = [] | maybe_singleton_str s = [s] val max_pat_breadth = 5 (* FUDGE *) fun term_features_of ctxt thy_name term_max_depth type_max_depth ts = let val thy = Proof_Context.theory_of ctxt val fixes = map snd (Variable.dest_fixes ctxt) val classes = Sign.classes_of thy fun add_classes \<^sort>\type\ = I | add_classes S = fold (`(Sorts.super_classes classes) #> swap #> op :: #> subtract (op =) \<^sort>\type\ #> map class_feature_of #> union (op =)) S fun pattify_type 0 _ = [] | pattify_type _ (Type (s, [])) = if member (op =) bad_types s then [] else [s] | pattify_type depth (Type (s, U :: Ts)) = let val T = Type (s, Ts) val ps = take max_pat_breadth (pattify_type depth T) val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U) in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end | pattify_type _ (TFree (_, S)) = maybe_singleton_str (crude_str_of_sort S) | pattify_type _ (TVar (_, S)) = maybe_singleton_str (crude_str_of_sort S) fun add_type_pat depth T = union (op =) (map type_feature_of (pattify_type depth T)) fun add_type_pats 0 _ = I | add_type_pats depth t = add_type_pat depth t #> add_type_pats (depth - 1) t fun add_type T = add_type_pats type_max_depth T #> fold_atyps_sorts (add_classes o snd) T fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts | add_subtypes T = add_type T fun pattify_term _ 0 _ = [] | pattify_term _ _ (Const (s, _)) = if is_widely_irrelevant_const s then [] else [s] | pattify_term _ _ (Free (s, T)) = maybe_singleton_str (crude_str_of_typ T) |> (if member (op =) fixes s then cons (free_feature_of (Long_Name.append thy_name s)) else I) | pattify_term _ _ (Var (_, T)) = maybe_singleton_str (crude_str_of_typ T) | pattify_term Ts _ (Bound j) = maybe_singleton_str (crude_str_of_typ (nth Ts j)) | pattify_term Ts depth (t $ u) = let val ps = take max_pat_breadth (pattify_term Ts depth t) val qs = take max_pat_breadth ("" :: pattify_term Ts (depth - 1) u) in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end | pattify_term _ _ _ = [] fun add_term_pat Ts = union (op =) oo pattify_term Ts fun add_term_pats _ 0 _ = I | add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t fun add_term Ts = add_term_pats Ts term_max_depth fun add_subterms Ts t = (case strip_comb t of (Const (s, T), args) => (not (is_widely_irrelevant_const s) ? add_term Ts t) #> add_subtypes T #> fold (add_subterms Ts) args | (head, args) => (case head of Free (_, T) => add_term Ts t #> add_subtypes T | Var (_, T) => add_subtypes T | Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body | _ => I) #> fold (add_subterms Ts) args) in fold (add_subterms []) ts [] end val term_max_depth = 2 val type_max_depth = 1 (* TODO: Generate type classes for types? *) fun features_of ctxt thy_name (scope, _) ts = thy_feature_of thy_name :: term_features_of ctxt thy_name term_max_depth type_max_depth ts |> scope <> Global ? cons local_feature (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn from such proofs. *) val max_dependencies = 20 (* FUDGE *) val prover_default_max_facts = 25 (* FUDGE *) (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) val typedef_dep = nickname_of_thm @{thm CollectI} (* Mysterious parts of the class machinery create lots of proofs that refer exclusively to "someI_ex" (and to some internal constructions). *) val class_some_dep = nickname_of_thm @{thm someI_ex} val fundef_ths = @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff fundef_default_value} |> map nickname_of_thm (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) val typedef_ths = @{thms type_definition.Abs_inverse type_definition.Rep_inverse type_definition.Rep type_definition.Rep_inject type_definition.Abs_inject type_definition.Rep_cases type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct type_definition.Rep_range type_definition.Abs_image} |> map nickname_of_thm fun is_size_def [dep] th = (case first_field ".rec" dep of SOME (pref, _) => (case first_field ".size" (nickname_of_thm th) of SOME (pref', _) => pref = pref' | NONE => false) | NONE => false) | is_size_def _ _ = false fun trim_dependencies deps = if length deps > max_dependencies then NONE else SOME deps fun isar_dependencies_of name_tabs th = thms_in_proof max_dependencies (SOME name_tabs) th |> Option.map (fn deps => if deps = [typedef_dep] orelse deps = [class_some_dep] orelse exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse is_size_def deps th then [] else deps) fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts name_tabs th = (case isar_dependencies_of name_tabs th of SOME [] => (false, []) | isar_deps0 => let val isar_deps = these isar_deps0 val thy = Proof_Context.theory_of ctxt val goal = goal_of_thm thy th val name = nickname_of_thm th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val facts = facts |> filter (fn (_, th') => thm_less (th', th)) fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) fun is_dep dep (_, th) = (nickname_of_thm th = dep) fun add_isar_dep facts dep accum = if exists (is_dep dep) accum then accum else (case find_first (is_dep dep) facts of SOME ((_, status), th) => accum @ [(("", status), th)] | NONE => accum (* should not happen *)) val mepo_facts = facts |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE hyp_ts concl_t val facts = mepo_facts |> fold (add_isar_dep facts) isar_deps |> map nickify val num_isar_deps = length isar_deps in if verbose andalso auto_level = 0 then writeln ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^ string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^ " facts") else (); (case run_prover_for_mash ctxt params prover name facts goal of {outcome = NONE, used_facts, ...} => (if verbose andalso auto_level = 0 then let val num_facts = length used_facts in writeln ("Found proof with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts) end else (); (true, map fst used_facts)) | _ => (false, isar_deps)) end) (*** High-level communication with MaSh ***) (* In the following functions, chunks are risers w.r.t. "thm_less_eq". *) fun chunks_and_parents_for chunks th = let fun insert_parent new parents = let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in parents |> forall (fn p => not (thm_less_eq (new, p))) parents ? cons new end fun rechunk seen (rest as th' :: ths) = if thm_less_eq (th', th) then (rev seen, rest) else rechunk (th' :: seen) ths fun do_chunk [] accum = accum | do_chunk (chunk as hd_chunk :: _) (chunks, parents) = if thm_less_eq (hd_chunk, th) then (chunk :: chunks, insert_parent hd_chunk parents) else if thm_less_eq (List.last chunk, th) then let val (front, back as hd_back :: _) = rechunk [] chunk in (front :: back :: chunks, insert_parent hd_back parents) end else (chunk :: chunks, parents) in fold_rev do_chunk chunks ([], []) |>> cons [] ||> map nickname_of_thm end fun attach_parents_to_facts _ [] = [] | attach_parents_to_facts old_facts (facts as (_, th) :: _) = let fun do_facts _ [] = [] | do_facts (_, parents) [fact] = [(parents, fact)] | do_facts (chunks, parents) ((fact as (_, th)) :: (facts as (_, th') :: _)) = let val chunks = app_hd (cons th) chunks val chunks_and_parents' = if thm_less_eq (th, th') andalso Thm.theory_name th = Thm.theory_name th' then (chunks, [nickname_of_thm th]) else chunks_and_parents_for chunks th' in (parents, fact) :: do_facts chunks_and_parents' facts end in old_facts @ facts |> do_facts (chunks_and_parents_for [[]] th) |> drop (length old_facts) end fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm val chained_feature_factor = 0.5 (* FUDGE *) val extra_feature_factor = 0.1 (* FUDGE *) val num_extra_feature_facts = 10 (* FUDGE *) val max_proximity_facts = 100 (* FUDGE *) fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown = let val inter_fact = inter (eq_snd Thm.eq_thm_prop) val raw_mash = find_suggested_facts ctxt facts suggs val proximate = take max_proximity_facts facts val unknown_chained = inter_fact raw_unknown chained val unknown_proximate = inter_fact raw_unknown proximate val mess = [(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])), (0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])), (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))] val unknown = raw_unknown |> fold (subtract (eq_snd Thm.eq_thm_prop)) [unknown_chained, unknown_proximate] in (mesh_facts (fact_distinct (op aconv)) (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown) end fun mash_suggested_facts ctxt thy_name ({debug, ...} : params) max_suggs hyp_ts concl_t facts = let val algorithm = the_mash_algorithm () val facts = facts |> rev_sort_list_prefix (crude_thm_ord ctxt o apply2 snd) (Int.max (num_extra_feature_facts, max_proximity_facts)) val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name th fun chained_or_extra_features_of factor (((_, stature), th), weight) = [Thm.prop_of th] |> features_of ctxt (Thm.theory_name th) stature |> map (rpair (weight * factor)) in (case get_state ctxt of NONE => ([], []) | SOME {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} => let val goal_feats0 = features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts) val chained_feats = chained |> map (rpair 1.0) |> map (chained_or_extra_features_of chained_feature_factor) |> rpair [] |-> fold (union (eq_fst (op =))) val extra_feats = facts |> take (Int.max (0, num_extra_feature_facts - length chained)) |> filter fact_has_right_theory |> weight_facts_steeply |> map (chained_or_extra_features_of extra_feature_factor) |> rpair [] |-> fold (union (eq_fst (op =))) val goal_feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0) |> debug ? sort (Real.compare o swap o apply2 snd) val fact_idxs = map_filter (Symtab.lookup fact_tab o nickname_of_thm o snd) facts val suggs = if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then let val learns = Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G in MaSh.query_external ctxt algorithm max_suggs learns goal_feats end else let val int_goal_feats = map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats in MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs fact_idxs max_suggs goal_feats int_goal_feats end val unknown = filter_out (is_fact_in_graph access_G o snd) facts in find_mash_suggestions ctxt max_suggs suggs facts chained unknown |> apply2 (map fact_of_lazy_fact) end) end fun mash_unlearn ctxt = (clear_state ctxt; writeln "Reset MaSh") fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (accum as (access_G, (fact_xtab, feat_xtab))) = let fun maybe_learn_from from (accum as (parents, access_G)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) access_G)) val access_G = access_G |> Graph.default_node (name, (Isar_Proof, feats, deps)) val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents val (deps, _) = ([], access_G) |> fold maybe_learn_from deps val fact_xtab = add_to_xtab name fact_xtab val feat_xtab = fold maybe_add_to_xtab feats feat_xtab in (SOME (name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab))) end handle Symtab.DUP _ => (NONE, accum) (* facts sometimes have the same name, confusingly *) fun relearn_wrt_access_graph ctxt (name, deps) access_G = let fun maybe_relearn_from from (accum as (parents, access_G)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) access_G)) val access_G = access_G |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps)) val (deps, _) = ([], access_G) |> fold maybe_relearn_from deps in ((name, deps), access_G) end fun flop_wrt_access_graph name = Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps)) val learn_timeout_slack = 20.0 fun launch_thread timeout task = let val hard_timeout = Time.scale learn_timeout_slack timeout val birth_time = Time.now () val death_time = birth_time + Timeout.scale_time hard_timeout val desc = ("Machine learner for Sledgehammer", "") in Async_Manager_Legacy.thread MaShN birth_time death_time desc task end fun anonymous_proof_name () = Date.fmt (anonymous_proof_prefix ^ "%Y%m%d.%H%M%S.") (Date.fromTimeLocal (Time.now ())) ^ serial_string () fun mash_learn_proof ctxt ({timeout, ...} : params) t used_ths = if not (null used_ths) andalso is_mash_enabled () then launch_thread timeout (fn () => let val thy = Proof_Context.theory_of ctxt val feats = features_of ctxt (Context.theory_name thy) (Local, General) [t] in map_state ctxt (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} => let val deps = used_ths |> filter (is_fact_in_graph access_G) |> map nickname_of_thm val name = anonymous_proof_name () val (access_G', xtabs', rev_learns) = add_node Automatic_Proof name [] (* ignore parents *) feats deps (access_G, xtabs, []) val (ffds', freqs') = recompute_ffds_freqs_from_learns (rev rev_learns) xtabs' num_facts0 ffds freqs in {access_G = access_G', xtabs = xtabs', ffds = ffds', freqs = freqs', dirty_facts = Option.map (cons name) dirty_facts} end); (true, "") end) else () fun sendback sub = Active.sendback_markup_command (sledgehammerN ^ " " ^ sub) val commit_timeout = seconds 30.0 (* The timeout is understood in a very relaxed fashion. *) fun mash_learn_facts ctxt (params as {debug, verbose, ...}) prover auto_level run_prover learn_timeout facts = let val timer = Timer.startRealTimer () fun next_commit_time () = Timer.checkRealTimer timer + commit_timeout in (case get_state ctxt of NONE => "MaSh is busy\nPlease try again later" | SOME {access_G, ...} => let val is_in_access_G = is_fact_in_graph access_G o snd val no_new_facts = forall is_in_access_G facts in if no_new_facts andalso not run_prover then if auto_level < 2 then "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^ (if auto_level = 0 andalso not run_prover then "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover" else "") else "" else let val name_tabs = build_name_tables nickname_of_thm facts fun deps_of status th = if status = Non_Rec_Def orelse status = Rec_Def then SOME [] else if run_prover then prover_dependencies_of ctxt params prover auto_level facts name_tabs th |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps) else isar_dependencies_of name_tabs th fun do_commit [] [] [] state = state | do_commit learns relearns flops {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} = let val was_empty = Graph.is_empty access_G val (learns, (access_G', xtabs')) = fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs) |>> map_filter I val (relearns, access_G'') = fold_map (relearn_wrt_access_graph ctxt) relearns access_G' val access_G''' = access_G'' |> fold flop_wrt_access_graph flops val dirty_facts' = (case (was_empty, dirty_facts) of (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names) | _ => NONE) val (ffds', freqs') = if null relearns then recompute_ffds_freqs_from_learns (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs' num_facts0 ffds freqs else recompute_ffds_freqs_from_access_G access_G''' xtabs' in {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs', dirty_facts = dirty_facts'} end fun commit last learns relearns flops = (if debug andalso auto_level = 0 then writeln "Committing..." else (); map_state ctxt (do_commit (rev learns) relearns flops); if not last andalso auto_level = 0 then let val num_proofs = length learns + length relearns in writeln ("Learned " ^ string_of_int num_proofs ^ " " ^ (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout) end else ()) fun learn_new_fact _ (accum as (_, (_, _, true))) = accum | learn_new_fact (parents, ((_, stature as (_, status)), th)) (learns, (num_nontrivial, next_commit, _)) = let val name = nickname_of_thm th val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] val deps = these (deps_of status th) val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1 val learns = (name, parents, feats, deps) :: learns val (learns, next_commit) = if Timer.checkRealTimer timer > next_commit then (commit false learns [] []; ([], next_commit_time ())) else (learns, next_commit) val timed_out = Timer.checkRealTimer timer > learn_timeout in (learns, (num_nontrivial, next_commit, timed_out)) end val (num_new_facts, num_nontrivial) = if no_new_facts then (0, 0) else let val new_facts = facts |> sort (crude_thm_ord ctxt o apply2 snd) |> map (pair []) (* ignore parents *) |> filter_out (is_in_access_G o snd) val (learns, (num_nontrivial, _, _)) = ([], (0, next_commit_time (), false)) |> fold learn_new_fact new_facts in commit true learns [] []; (length new_facts, num_nontrivial) end fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum | relearn_old_fact ((_, (_, status)), th) ((relearns, flops), (num_nontrivial, next_commit, _)) = let val name = nickname_of_thm th val (num_nontrivial, relearns, flops) = (case deps_of status th of SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops) | NONE => (num_nontrivial, relearns, name :: flops)) val (relearns, flops, next_commit) = if Timer.checkRealTimer timer > next_commit then (commit false [] relearns flops; ([], [], next_commit_time ())) else (relearns, flops, next_commit) val timed_out = Timer.checkRealTimer timer > learn_timeout in ((relearns, flops), (num_nontrivial, next_commit, timed_out)) end val num_nontrivial = if not run_prover then num_nontrivial else let val max_isar = 1000 * max_dependencies fun priority_of th = Random.random_range 0 max_isar + (case try (Graph.get_node access_G) (nickname_of_thm th) of SOME (Isar_Proof, _, deps) => ~100 * length deps | SOME (Automatic_Proof, _, _) => 2 * max_isar | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar | NONE => 0) val old_facts = facts |> filter is_in_access_G |> map (`(priority_of o snd)) |> sort (int_ord o apply2 fst) |> map snd val ((relearns, flops), (num_nontrivial, _, _)) = (([], []), (num_nontrivial, next_commit_time (), false)) |> fold relearn_old_fact old_facts in commit true [] relearns flops; num_nontrivial end in if verbose orelse auto_level < 2 then "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^ " and " ^ string_of_int num_nontrivial ^ " nontrivial " ^ (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s num_nontrivial ^ (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") else "" end end) end fun mash_learn ctxt (params as {provers, timeout, induction_rules, ...}) fact_override chained run_prover = let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = nearly_all_facts ctxt (induction_rules = SOME Instantiate) fact_override Keyword.empty_keywords css chained [] \<^prop>\True\ |> sort (crude_thm_ord ctxt o apply2 snd o swap) val num_facts = length facts val prover = hd provers fun learn auto_level run_prover = mash_learn_facts ctxt params prover auto_level run_prover one_year facts |> writeln in if run_prover then (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^ string_of_time timeout ^ ").\n\nCollecting Isar proofs first..."); learn 1 false; writeln "Now collecting automatic proofs\n\ \This may take several hours; you can safely stop the learning process at any point"; learn 0 true) else (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for Isar proofs..."); learn 0 false) end fun mash_can_suggest_facts ctxt = (case get_state ctxt of NONE => false | SOME {access_G, ...} => not (Graph.is_empty access_G)) fun mash_can_suggest_facts_fast ctxt = (case peek_state ctxt of NONE => false | SOME (_, {access_G, ...}) => not (Graph.is_empty access_G)) (* Generate more suggestions than requested, because some might be thrown out later for various reasons (e.g., duplicates). *) fun generous_max_suggestions max_facts = 2 * max_facts + 25 (* FUDGE *) val mepo_weight = 0.5 (* FUDGE *) val mash_weight = 0.5 (* FUDGE *) val max_facts_to_learn_before_query = 100 (* FUDGE *) (* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer. *) val min_secs_for_learning = 10 fun relevant_facts ctxt (params as {verbose, learn, fact_filter, timeout, ...}) prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = if not (subset (op =) (the_list fact_filter, fact_filters)) then error ("Unknown fact filter: " ^ quote (the fact_filter)) else if only then [("", map fact_of_lazy_fact facts)] else if max_facts <= 0 orelse null facts then [("", [])] else let val thy_name = Context.theory_name (Proof_Context.theory_of ctxt) fun maybe_launch_thread exact min_num_facts_to_learn = if not (Async_Manager_Legacy.has_running_threads MaShN) andalso Time.toSeconds timeout >= min_secs_for_learning then let val timeout = Time.scale learn_timeout_slack timeout in (if verbose then writeln ("Started MaShing through " ^ (if exact then "" else "up to ") ^ string_of_int min_num_facts_to_learn ^ " fact" ^ plural_s min_num_facts_to_learn ^ " in the background") else ()); launch_thread timeout (fn () => (true, mash_learn_facts ctxt params prover 2 false timeout facts)) end else () val mash_enabled = is_mash_enabled () val mash_fast = mash_can_suggest_facts_fast ctxt fun please_learn () = if mash_fast then (case get_state ctxt of NONE => maybe_launch_thread false (length facts) | SOME {access_G, xtabs = ((num_facts0, _), _), ...} => let val is_in_access_G = is_fact_in_graph access_G o snd val min_num_facts_to_learn = length facts - num_facts0 in if min_num_facts_to_learn <= max_facts_to_learn_before_query then (case length (filter_out is_in_access_G facts) of 0 => () | num_facts_to_learn => if num_facts_to_learn <= max_facts_to_learn_before_query then mash_learn_facts ctxt params prover 2 false timeout facts |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s)) else maybe_launch_thread true num_facts_to_learn) else maybe_launch_thread false min_num_facts_to_learn end) else maybe_launch_thread false (length facts) val _ = if learn andalso mash_enabled andalso fact_filter <> SOME mepoN then please_learn () else () val effective_fact_filter = (case fact_filter of SOME ff => ff | NONE => if mash_enabled andalso mash_fast then meshN else mepoN) val unique_facts = drop_duplicate_facts facts val add_ths = Attrib.eval_thms ctxt add fun in_add (_, th) = member Thm.eq_thm_prop add_ths th fun add_and_take accepts = (case add_ths of [] => accepts | _ => (unique_facts |> filter in_add |> map fact_of_lazy_fact) @ (accepts |> filter_out in_add)) |> take max_facts fun mepo () = (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts |> weight_facts_steeply, []) fun mash () = mash_suggested_facts ctxt thy_name params (generous_max_suggestions max_facts) hyp_ts concl_t facts |>> weight_facts_steeply val mess = (* the order is important for the "case" expression below *) [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash) |> effective_fact_filter <> mashN ? cons (mepo_weight, mepo) |> Par_List.map (apsnd (fn f => f ())) val mesh = mesh_facts (fact_distinct (op aconv)) (eq_snd (gen_eq_thm ctxt)) max_facts mess |> add_and_take in (case (fact_filter, mess) of (NONE, [(_, (mepo, _)), (_, (mash, _))]) => [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take), (mashN, mash |> map fst |> add_and_take)] | _ => [(effective_fact_filter, mesh)]) end 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,267 +1,282 @@ (* 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 + type atp_slice = Sledgehammer_ATP_Systems.atp_slice 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, 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, + factss : (string * fact list) list, found_proof : string -> unit} + datatype prover_slice = + ATP_Slice of atp_slice + | SMT_Slice of int * string + 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 + type prover = params -> prover_problem -> prover_slice -> 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 get_facts_of_filter : string -> (string * fact list) list -> fact 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, 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, 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, + factss : (string * fact list) list, found_proof : string -> unit} +datatype prover_slice = + ATP_Slice of atp_slice +| SMT_Slice of int * string + 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 +type prover = params -> prover_problem -> prover_slice -> 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 get_facts_of_filter fact_filter factss = + (case AList.lookup (op =) factss fact_filter of + SOME facts => facts + | NONE => snd (hd factss)) + 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_atp.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML @@ -1,351 +1,352 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen ATPs as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_ATP = sig type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val atp_problem_dest_dir : string Config.T val atp_proof_dest_dir : string Config.T val atp_problem_prefix : string Config.T val atp_completish : int Config.T val atp_full_names : bool Config.T val run_atp : mode -> string -> prover end; structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = struct open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *) val atp_problem_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_dest_dir\ (K "") val atp_proof_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_proof_dest_dir\ (K "") val atp_problem_prefix = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_prefix\ (K "prob") val atp_completish = Attrib.setup_config_int \<^binding>\sledgehammer_atp_completish\ (K 0) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) val atp_full_names = Attrib.setup_config_bool \<^binding>\sledgehammer_atp_full_names\ (K false) fun choose_type_enc strictness best_type_enc format = the_default best_type_enc #> type_enc_of_string strictness #> adjust_type_enc format fun has_bound_or_var_of_type pred = exists_subterm (fn Var (_, T as Type _) => pred T | Abs (_, T as Type _, _) => pred T | _ => false) (* Unwanted equalities are those between a (bound or schematic) variable that does not properly occur in the second operand. *) val is_exhaustive_finite = let fun is_bad_equal (Var z) t = not (exists_subterm (fn Var z' => z = z' | _ => false) t) | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) | is_bad_equal _ _ = false fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 fun do_formula pos t = (case (pos, t) of (_, \<^Const_>\Trueprop for t1\) => do_formula pos t1 | (true, Const (\<^const_name>\Pure.all\, _) $ Abs (_, _, t')) => do_formula pos t' | (true, Const (\<^const_name>\All\, _) $ Abs (_, _, t')) => do_formula pos t' | (false, Const (\<^const_name>\Ex\, _) $ Abs (_, _, t')) => do_formula pos t' | (_, \<^Const_>\Pure.imp for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^prop>\False\ orelse do_formula pos t2) | (_, \<^Const_>\implies for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^Const>\False\ orelse do_formula pos t2) | (_, \<^Const_>\Not for t1\) => do_formula (not pos) t1 | (true, \<^Const_>\disj for t1 t2\) => forall (do_formula pos) [t1, t2] | (false, \<^Const_>\conj for t1 t2\) => forall (do_formula pos) [t1, t2] | (true, Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) => do_equals t1 t2 | (true, Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2) => do_equals t1 t2 | _ => false) in do_formula true end (* Facts containing variables of finite types such as "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type encodings. *) fun is_dangerous_prop ctxt = transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) val mono_max_privileged_facts = 10 fun suffix_of_mode Auto_Try = "_try" | suffix_of_mode Try = "_try" | suffix_of_mode Normal = "" | suffix_of_mode MaSh = "" | suffix_of_mode Minimize = "_min" (* Important messages are important but not so important that users want to see them each time. *) val atp_important_message_keep_quotient = 25 fun run_atp mode name - ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_facts, - max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, - slices, timeout, preplay_timeout, spy, ...} : params) - ({comment, state, goal, subgoal, subgoal_count, facts, found_proof} : prover_problem) = + ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter, + max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, + minimize, slices, timeout, preplay_timeout, spy, ...} : params) + ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem) + slice = let val thy = Proof.theory_of state val ctxt = Proof.context_of state - val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, + val ATP_Slice ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans, + best_uncurried_aliases, extra) = slice + + val {exec, arguments, proof_delims, known_failures, prem_role, best_max_mono_iters, best_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name val completish = Config.get ctxt atp_completish val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (problem_dest_dir, proof_dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name |> (fn (dir, prefix) => (dir, dir, prefix)) else (Config.get ctxt atp_problem_dest_dir, Config.get ctxt atp_proof_dest_dir, Config.get ctxt atp_problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |> Path.ext "p" val prob_path = if problem_dest_dir = "" then File.tmp_path problem_file_name else if File.exists (Path.explode problem_dest_dir) then Path.explode problem_dest_dir + problem_file_name else error ("No such directory: " ^ quote problem_dest_dir) val executable = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let val pref = getenv var ^ "/" val paths = map (Path.explode o prefix pref) (if ML_System.platform_is_windows then map (suffix ".exe") (snd exec) @ snd exec else snd exec); in (case find_first File.exists paths of SOME path => path | NONE => error ("Bad executable: " ^ Path.print (hd paths))) end | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) fun run () = let - val ((best_max_facts, _), format, best_type_enc, best_lam_trans, best_uncurried_aliases, - extra) = - List.last (best_slices ctxt) - fun monomorphize_facts facts = let val ctxt = ctxt |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances best_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) val subgoal_th = Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy val rths = facts |> chop mono_max_privileged_facts |>> map (pair 1 o snd) ||> map (pair 2 o snd) |> op @ |> cons (0, subgoal_th) in Monomorph.monomorph atp_schematic_consts_of ctxt rths |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end - val facts = snd facts + val effective_fact_filter = fact_filter |> the_default best_fact_filter + val facts = get_facts_of_filter effective_fact_filter factss val num_facts = (case max_facts of NONE => best_max_facts | SOME max_facts => max_facts) |> Integer.min (length facts) val strictness = if strict then Strict else Non_Strict val type_enc = type_enc |> choose_type_enc strictness best_type_enc format val run_timeout = slice_timeout slices timeout val generous_run_timeout = if mode = MaSh then one_day else run_timeout val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let val sound = is_type_enc_sound type_enc val generate_info = (case format of DFG _ => true | _ => false) val readable_names = not (Config.get ctxt atp_full_names) val lam_trans = lam_trans |> the_default best_lam_trans val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases in facts |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> take num_facts |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode lam_trans uncurried_aliases readable_names true hyp_ts concl_t end) () val () = spying spy (fn () => (state, subgoal, name, "Generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name val args = arguments ctxt full_proofs extra run_timeout prob_path (ord, ord_info, sel_weights) val command = space_implode " " (File.bash_path executable :: args) fun run_command () = if exec = isabelle_scala_function then let val {output, timing} = SystemOnTPTP.run_system_encoded args in (output, timing) end else let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) in (Process_Result.out res, Process_Result.timing_elapsed res) end val _ = atp_problem |> lines_of_atp_problem format ord ord_info |> (exec <> isabelle_scala_function) ? cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val ((output, run_time), (atp_proof, outcome)) = Timeout.apply generous_run_timeout run_command () |>> overlord ? (fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output) |> (fn accum as (output, _) => (accum, extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) atp_problem handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) handle Timeout.TIMEOUT _ => (("", run_timeout), ([], SOME TimedOut)) | ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg))) val () = spying spy (fn () => (state, subgoal, name, "Running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms")) val outcome = (case outcome of NONE => (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of SOME facts => let val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) in if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure end | NONE => (found_proof name; NONE)) | _ => outcome) in (atp_problem_data, (output, run_time, facts, atp_proof, outcome), (format, type_enc)) end (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () fun export (_, (output, _, _, _, _), _) = let val proof_dest_dir_path = Path.explode proof_dest_dir val make_export_file_name = Path.split_ext #> apfst (Path.explode o suffix "_proof" o Path.implode) #> swap #> uncurry Path.ext in if proof_dest_dir = "" then Output.system_message "don't export proof" else if File.exists proof_dest_dir_path then File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output else error ("No such directory: " ^ quote proof_dest_dir) end val ((_, pool, lifted, sym_tab), (output, run_time, used_from, atp_proof, outcome), (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message = if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0 then extract_important_message output else "" val (used_facts, preferred_methss, message) = (case outcome of NONE => let val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val preferred_methss = (Metis_Method (NONE, NONE), bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN)) in (used_facts, preferred_methss, fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = let val metis_type_enc = if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE val metis_lam_trans = if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE val atp_proof = atp_proof |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> local_name = spassN ? introduce_spass_skolems |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, minimize, atp_proof, goal) end 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 ^ (if important_message <> "" then "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message else "") 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; 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,278 @@ (* 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 + type prover_slice = Sledgehammer_Prover.prover_slice 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 get_default_slice : Proof.context -> string -> prover_slice 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) (#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 +fun get_default_slice ctxt name = + let val thy = Proof_Context.theory_of ctxt in + if is_atp thy name then + ATP_Slice (List.last (#best_slices (get_atp thy name ()) ctxt)) + else if is_smt_prover ctxt name then + SMT_Slice (SMT_Solver.default_max_relevant ctxt 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 = + slice 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, 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 ()} + factss = [("", facts)], found_proof = K ()} val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, message} = - prover params problem + prover params problem slice 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 slice = get_default_slice ctxt 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) + test_facts params slice 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 +fun get_minimizing_prover ctxt mode do_learn name params problem slice = + get_prover ctxt mode name params problem slice |> 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,165 @@ (* 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, slices, timeout, ...} : params) state goal i facts = let 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, +fun run_smt_solver mode name (params as {debug, verbose, fact_filter, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, ...}) - ({state, goal, subgoal, subgoal_count, facts, found_proof, ...} : prover_problem) = + ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) + slice = let val ctxt = Proof.context_of state - val facts = snd facts + val SMT_Slice (best_max_facts, best_fact_filter) = slice + + val effective_fact_filter = fact_filter |> the_default best_fact_filter + val facts = get_facts_of_filter effective_fact_filter factss 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; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML @@ -1,76 +1,77 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2010, 2011 Sledgehammer as a tactic. *) signature SLEDGEHAMMER_TACTICS = sig type fact_override = Sledgehammer_Fact.fact_override val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override -> thm list -> int -> tactic val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override -> thm list -> int -> tactic end; structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = struct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer_Commands fun run_prover override_params fact_override chained i n ctxt goal = let val thy = Proof_Context.theory_of ctxt val mode = Normal val params as {provers, induction_rules, max_facts, ...} = default_params thy override_params val name = hd provers val prover = get_prover ctxt mode name val default_max_facts = default_max_facts_of_prover ctxt name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val keywords = Thy_Header.get_keywords' ctxt val css_table = clasimpset_rule_table_of ctxt val inst_inducts = induction_rules = SOME Instantiate val facts = nearly_all_facts ctxt inst_inducts fact_override keywords css_table chained hyp_ts concl_t |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override hyp_ts concl_t |> hd |> snd val problem = {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - facts = ("", facts), found_proof = K ()} + factss = [("", facts)], found_proof = K ()} + val slice = get_default_slice ctxt name in - (case prover params problem of + (case prover params problem slice of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME | _ => NONE) handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) end fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th = let val override_params = override_params @ [("preplay_timeout", "0")] in (case run_prover override_params fact_override chained i i ctxt th of SOME facts => Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt (maps (thms_of_name ctxt) facts) i th | NONE => Seq.empty) end fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th = let val override_params = override_params @ [("preplay_timeout", "0"), ("minimize", "false")] val xs = run_prover override_params fact_override chained i i ctxt th in if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty end end;