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,602 +1,603 @@ (* 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 type preplay_result = proof_method * (play_outcome * (string * stature) list) datatype sledgehammer_outcome = SH_Some of prover_result * preplay_result list | SH_Unknown | SH_TimeOut | SH_ResourcesOut | SH_None val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string 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_Problem 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_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh type preplay_result = proof_method * (play_outcome * (string * stature) list) datatype sledgehammer_outcome = SH_Some of prover_result * preplay_result list | SH_Unknown | SH_TimeOut | SH_ResourcesOut | 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_ResourcesOut = "resources_out" | 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 varify_nonfixed_terms_global nonfixeds tm = tm |> Same.commit (Term_Subst.map_aterms_same (fn Free (x, T) => if member (op =) nonfixeds x then Var ((x, 0), T) else raise Same.SAME | Var (xi, _) => raise TERM (Logic.bad_schematic xi, [tm]) | _ => raise Same.SAME)) fun max_outcome outcomes = let val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes val timeout = find_first (fn (SH_TimeOut, _) => true | _ => false) outcomes val resources_out = find_first (fn (SH_ResourcesOut, _) => true | _ => false) outcomes val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes val none = find_first (fn (SH_None, _) => true | _ => false) outcomes in some |> alternative snd unknown |> alternative snd timeout |> alternative snd resources_out |> alternative snd none |> the_default (SH_Unknown, "") end fun play_one_line_proofs minimize timeout used_facts state goal i methss = (if timeout = Time.zeroTime then [] else let val ctxt = Proof.context_of state val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts val fact_names = map fst used_facts val {facts = chained, ...} = Proof.goal state val goal_t = Logic.get_goal (Thm.prop_of goal) i fun try_methss ress [] = ress | try_methss ress (meths :: methss) = let fun mk_step meths = Prove { qualifiers = [], obtains = [], label = ("", 0), goal = goal_t, subproofs = [], facts = ([], fact_names), proof_methods = meths, comment = ""} val ress' = preplay_isar_step ctxt chained timeout [] (mk_step meths) |> map (fn (meth, play_outcome) => (case (minimize, play_outcome) of (true, Played time) => let val (time', used_names') = minimized_isar_step ctxt chained time (mk_step [meth]) ||> (facts_of_isar_step #> snd) val used_facts' = filter (member (op =) used_names' o fst) used_facts in (meth, Played time', used_facts') end | _ => (meth, play_outcome, used_facts))) val any_succeeded = exists (fn (_, Played _, _) => true | _ => false) ress' in try_methss (ress' @ ress) (if any_succeeded then [] else methss) end in try_methss [] methss end) |> map (fn (meth, play_outcome, used_facts) => (meth, (play_outcome, filter_out (fn (_, (sc, _)) => sc = Chained) used_facts))) |> sort (play_outcome_ord o apply2 (fn (_, (play_outcome, _)) => play_outcome)) fun select_one_line_proof used_facts preferred_meth preplay_results = (case preplay_results of (* Select best method if preplay succeeded *) (best_meth, (best_outcome as Played _, best_used_facts)) :: _ => (best_used_facts, (best_meth, best_outcome)) (* Otherwise select preferred method *) | _ => (used_facts, (preferred_meth, (case AList.lookup (op =) preplay_results preferred_meth of SOME (outcome, _) => outcome | NONE => Play_Timed_Out Time.zeroTime)))) |> apfst (filter_out (fn (_, (sc, _)) => sc = Chained)) fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn (problem as {state, subgoal, factss, ...} : prover_problem) - (slice as ((slice_size, abduce, check_consistent, num_facts, fact_filter), _)) name = + (slice as ((slice_size, abduce, check_inconsistent, num_facts, fact_filter), _)) name = let val ctxt = Proof.context_of state val _ = spying spy (fn () => (state, subgoal, name, "Launched" ^ (if abduce then " (abduce)" else "") ^ - (if check_consistent then " (check_consistent)" else ""))) + (if check_inconsistent then " (check_inconsistent)" else ""))) val _ = if verbose then writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^ (if abduce then " (abduce)" else "") ^ - (if check_consistent then " (check_consistent)" else "") ^ "...") + (if check_inconsistent then " (check_inconsistent)" else "") ^ "...") else () 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 ("Facts in " ^ name ^ " " ^ - (if check_consistent then "inconsistency" else "proof") ^ ": ") + (if check_inconsistent then "inconsistency" else "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 *) 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) :: factss) |> AList.group (op =) |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) in - "Success: Found " ^ (if check_consistent then "inconsistency" else "proof") ^ " with " ^ + "Success: Found " ^ (if check_inconsistent then "inconsistency" else "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 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 goal subgoal (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) = let val (output, chosen_preplay_outcome) = if outcome = SOME ATP_Proof.TimedOut then (SH_TimeOut, select_one_line_proof used_facts (fst preferred_methss) []) else if outcome = SOME ATP_Proof.OutOfResources then (SH_ResourcesOut, select_one_line_proof used_facts (fst preferred_methss) []) else if is_some outcome then (SH_None, select_one_line_proof used_facts (fst preferred_methss) []) else let val preplay_results = play_one_line_proofs minimize preplay_timeout used_facts state goal subgoal (snd preferred_methss) val chosen_preplay_outcome = select_one_line_proof used_facts (fst preferred_methss) preplay_results in (SH_Some (result, preplay_results), chosen_preplay_outcome) end fun output_message () = message (fn () => chosen_preplay_outcome) in (output, output_message) end -fun analyze_prover_result_for_consistency (result as {outcome, used_facts, ...} : prover_result) = +fun analyze_prover_result_for_inconsistency (result as {outcome, used_facts, ...} : prover_result) = if outcome = SOME ATP_Proof.TimedOut then (SH_TimeOut, K "") else if outcome = SOME ATP_Proof.OutOfResources then (SH_ResourcesOut, K "") else if is_some outcome then (SH_None, K "") else (SH_Some (result, []), fn () => (if member (op = o apsnd fst) used_facts sledgehammer_goal_as_fact then (case map fst (filter_out (equal sledgehammer_goal_as_fact o fst) used_facts) of [] => "The goal is inconsistent" | facts => "The goal is inconsistent with these facts: " ^ commas facts) else "The following facts are inconsistent: " ^ commas (map fst used_facts))) 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 "Metis_Examples" can be processed on any machine. *) if expect = "" orelse not (is_prover_installed ctxt prover_name) then () else (case (expect, outcome) of ("some", SH_Some _) => () | ("some_preplayed", SH_Some (_, preplay_results)) => if exists (fn (_, (Played _, _)) => true | _ => false) preplay_results then () else error ("Unexpected outcome: the external prover found a proof but preplay failed") | ("unknown", SH_Unknown) => () | ("timeout", SH_TimeOut) => () | ("resources_out", SH_ResourcesOut) => () | ("none", SH_None) => () | _ => error ("Unexpected outcome: " ^ quote outcome_code)) end fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode has_already_found_something found_something writeln_result learn - (problem as {state, subgoal, ...}) (slice as ((_, _, check_consistent, _, _), _)) prover_name = + (problem as {state, subgoal, ...}) (slice as ((_, _, check_inconsistent, _, _), _)) + prover_name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout fun flip_problem {comment, state, goal, subgoal, factss = factss, ...} = let val thy = Proof_Context.theory_of ctxt val assms = Assumption.all_assms_of ctxt val assm_ts = map Thm.term_of assms val subgoal_t = Logic.get_goal (Thm.prop_of goal) subgoal val polymorphic_subgoal_t = (Logic.list_implies (assm_ts, subgoal_t)) |> Logic.varify_global val nonfixeds = subtract (op =) (fold Term.add_free_names assm_ts []) (Term.add_free_names subgoal_t []) val monomorphic_subgoal_t = subgoal_t |> varify_nonfixed_terms_global nonfixeds val subgoal_thms = map (Skip_Proof.make_thm thy) [polymorphic_subgoal_t, monomorphic_subgoal_t] val new_facts = map (fn thm => (((sledgehammer_goal_as_fact, (Assum, General)), thm))) subgoal_thms in {comment = comment, state = state, goal = Thm.trivial @{cprop False}, subgoal = 1, subgoal_count = 1, factss = map (apsnd (append new_facts)) factss, has_already_found_something = has_already_found_something, found_something = found_something "an inconsistency"} end - val problem as {goal, ...} = problem |> check_consistent ? flip_problem + val problem as {goal, ...} = problem |> check_inconsistent ? flip_problem fun really_go () = launch_prover params mode learn problem slice prover_name - |> (if check_consistent then analyze_prover_result_for_consistency else + |> (if check_inconsistent then analyze_prover_result_for_inconsistency else preplay_prover_result params state goal subgoal) fun go () = if debug then really_go () else (really_go () handle ERROR msg => (SH_Unknown, fn () => "Warning: " ^ 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 () = if mode = Auto_Try then () else (case outcome of SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message) | _ => ()) in (outcome, message) end fun string_of_facts filter facts = "Selected " ^ string_of_int (length facts) ^ " " ^ (if filter = "" then "" else filter ^ " ") ^ "fact" ^ plural_s (length facts) ^ ": " ^ (space_implode " " (map (fst o fst) facts)) fun string_of_factss factss = if forall (null o snd) factss then "Found no relevant facts" else cat_lines (map (fn (filter, facts) => string_of_facts filter facts) factss) val default_slice_schedule = (* FUDGE (loosely inspired by Seventeen evaluation) *) [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, zipperpositionN, - cvc4N, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, eN, cvc4N, iproverN, zipperpositionN, + cvc4N, eN, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN, spassN, vampireN, zipperpositionN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, spassN, zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, zipperpositionN] fun schedule_of_provers provers num_slices = let val (known_provers, unknown_provers) = List.partition (member (op =) default_slice_schedule) provers val default_slice_schedule = filter (member (op =) known_provers) default_slice_schedule val num_default_slices = length default_slice_schedule fun round_robin _ [] = [] | round_robin 0 _ = [] | round_robin n (prover :: provers) = prover :: round_robin (n - 1) (provers @ [prover]) in if num_slices <= num_default_slices then take num_slices default_slice_schedule else default_slice_schedule @ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers) end fun prover_slices_of_schedule ctxt goal subgoal factss - ({abduce, check_consistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, + ({abduce, check_inconsistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, ...} : params) schedule = let fun triplicate_slices original = let val shift = - map (apfst (fn (slice_size, abduce, check_consistent, num_facts, fact_filter) => - (slice_size, abduce, check_consistent, num_facts, + map (apfst (fn (slice_size, abduce, check_inconsistent, num_facts, fact_filter) => + (slice_size, abduce, check_inconsistent, num_facts, if fact_filter = mashN then mepoN else if fact_filter = mepoN then meshN else mashN))) val shifted_once = shift original val shifted_twice = shift shifted_once in original @ shifted_once @ shifted_twice end fun adjust_extra (ATP_Slice (format0, type_enc0, lam_trans0, uncurried_aliases0, extra_extra0)) = ATP_Slice (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans, the_default uncurried_aliases0 uncurried_aliases, extra_extra0) | adjust_extra (extra as SMT_Slice _) = extra fun adjust_slice max_slice_size - ((slice_size0, abduce0, check_consistent0, num_facts0, fact_filter0), extra) = + ((slice_size0, abduce0, check_inconsistent0, num_facts0, fact_filter0), extra) = let val slice_size = Int.min (max_slice_size, slice_size0) val goal_not_False = not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) val abduce = (case abduce of NONE => abduce0 andalso goal_not_False | SOME max_candidates => max_candidates > 0) - val check_consistent = - (case check_consistent of - NONE => check_consistent0 andalso goal_not_False - | SOME check_consistent => check_consistent) + val check_inconsistent = + (case check_inconsistent of + NONE => check_inconsistent0 andalso goal_not_False + | SOME check_inconsistent => check_inconsistent) val fact_filter = fact_filter |> the_default fact_filter0 val max_facts = max_facts |> the_default num_facts0 val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss)) in - ((slice_size, abduce, check_consistent, num_facts, fact_filter), adjust_extra extra) + ((slice_size, abduce, check_inconsistent, num_facts, fact_filter), adjust_extra extra) end val provers = distinct (op =) schedule val prover_slices = map (fn prover => (prover, (is_none fact_filter ? triplicate_slices) (get_slices ctxt prover))) provers val max_threads = Multithreading.max_threads () fun translate_schedule _ 0 _ = [] | translate_schedule _ _ [] = [] | translate_schedule prover_slices slices_left (prover :: schedule) = (case AList.lookup (op =) prover_slices prover of SOME (slice0 :: slices) => let val prover_slices' = AList.update (op =) (prover, slices) prover_slices val slice as ((slice_size, _, _, _, _), _) = adjust_slice ((slices_left + max_threads - 1) div max_threads) slice0 in (prover, slice) :: translate_schedule prover_slices' (slices_left - slice_size) schedule end | _ => translate_schedule prover_slices slices_left schedule) in translate_schedule prover_slices (length schedule) schedule |> distinct (op =) end -fun run_sledgehammer (params as {verbose, spy, provers, check_consistent, induction_rules, +fun run_sledgehammer (params as {verbose, spy, provers, check_inconsistent, induction_rules, max_facts, max_proofs, slices, ...}) 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_proofs_and_inconsistencies = Synchronized.var "found_proofs_and_inconsistencies" 0 fun has_already_found_something () = if mode = Normal then Synchronized.value found_proofs_and_inconsistencies > 0 else false fun found_something a_proof_or_inconsistency prover_name = if mode = Normal then (Synchronized.change found_proofs_and_inconsistencies (fn n => n + 1); (the_default writeln writeln_result) (prover_name ^ " found " ^ a_proof_or_inconsistency ^ "...")) 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 => fold (fn prover => fold (fn ((_, _, _, max_facts, _), _) => Integer.max max_facts) (get_slices ctxt prover)) provers 0) * 51 div 50 (* some slack to account for filtering of induction facts below *) val ({elapsed, ...}, factss) = Timing.timing (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t) all_facts val induction_rules = the_default (if only then Include else Exclude) induction_rules val factss = map (apsnd (maybe_filter_out_induction_rules induction_rules)) factss 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 factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss, has_already_found_something = has_already_found_something, found_something = found_something "a proof"} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) val launch = launch_prover_and_preplay params mode has_already_found_something found_something writeln_result learn val schedule = if mode = Auto_Try then provers else schedule_of_provers provers slices val prover_slices = prover_slices_of_schedule ctxt goal i factss params schedule val _ = if verbose then writeln ("Running " ^ commas (map fst prover_slices) ^ "...") else () in if mode = Auto_Try then (SH_Unknown, "") |> fold (fn (prover, slice) => fn accum as (SH_Some _, _) => accum | _ => launch problem slice prover) prover_slices else (learn chained_thms; Par_List.map (fn (prover, slice) => if Synchronized.value found_proofs_and_inconsistencies < max_proofs then launch problem slice prover else (SH_None, "")) prover_slices |> max_outcome) end fun normal_failure () = (the_default writeln writeln_result - ("No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^ + ("No " ^ (if check_inconsistent = SOME true then "inconsistency" else "proof") ^ " found"); false) in (launch_provers () handle Timeout.TIMEOUT _ => (SH_TimeOut, "")) |> `(fn (outcome, message) => (case outcome of SH_Some _ => (the_default writeln writeln_result "Done"; true) | SH_Unknown => if message = "" then normal_failure () else (the_default writeln writeln_result ("Warning: " ^ message); false) | SH_TimeOut => normal_failure () | SH_ResourcesOut => normal_failure () | SH_None => if message = "" then normal_failure () else (the_default writeln writeln_result ("Warning: " ^ message); 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,614 +1,614 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Setup for supported ATPs. *) signature SLEDGEHAMMER_ATP_SYSTEMS = sig type atp_format = ATP_Problem.atp_format type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure type base_slice = int * bool * bool * int * string type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, arguments : bool -> bool -> string -> Time.time -> Path.T -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, generate_isabelle_info : bool, good_slices : Proof.context -> (base_slice * atp_slice) list, good_max_mono_iters : int, good_max_new_mono_instances : int} val default_max_mono_iters : int val default_max_new_mono_instances : int 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 -> bool -> (Proof.context -> base_slice * atp_slice) -> string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit val local_atps : string list val remote_atps : string list val dummy_atps : string list val non_dummy_atps : string list val all_atps : string list 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 *) -(* desired slice size, abduce, check_consistent, desired number of facts, fact filter *) +(* desired slice size, abduce, check_inconsistent, desired number of facts, fact filter *) type base_slice = int * bool * bool * int * string (* problem file format, type encoding, lambda translation scheme, uncurried aliases?, prover-specific extra information *) type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, arguments : bool -> bool -> string -> Time.time -> Path.T -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, generate_isabelle_info : bool, good_slices : Proof.context -> (base_slice * atp_slice) list, good_max_mono_iters : int, good_max_new_mono_instances : int} (* "good_slices" must be found empirically, ideally taking a holistic approach since the ATPs are run in parallel. *) 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" (* agsyHOL *) val agsyhol_config : atp_config = {exec = (["AGSYHOL_HOME"], ["agsyHOL"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => ["--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, generate_isabelle_info = false, good_slices = (* FUDGE *) K [((2, false, false, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_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 => ["--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, generate_isabelle_info = false, good_slices = (* FUDGE *) K [((1000 (* infinity *), false, false, 100, meshN), (TF1, "poly_native", liftingN, false, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} val alt_ergo = (alt_ergoN, fn () => alt_ergo_config) (* E *) val e_config : atp_config = {exec = (["E_HOME"], ["eprover-ho", "eprover"]), arguments = fn abduce => fn _ => fn extra_options => fn timeout => fn problem => ["--tstp-in --tstp-out --silent " ^ (if abduce then "--auto --print-saturated=ieIE --print-sat-info --soft-cpu-limit=" else extra_options ^ " --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, generate_isabelle_info = false, good_slices = let val (format, type_enc, lam_trans, extra_options) = if string_ord (getenv "E_VERSION", "2.7") <> LESS then (* '$ite' support appears to be buggy *) (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true") 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, "--auto-schedule") else (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule") in (* FUDGE *) K [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)), ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)), ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)), ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)), ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)), ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options))] end, good_max_mono_iters = default_max_mono_iters, good_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 => ["--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, generate_isabelle_info = false, good_slices = (* FUDGE *) K [((2, false, false, 32, meshN), (TF0, "mono_native", liftingN, false, "")), ((2, false, false, 512, meshN), (TX0, "mono_native", liftingN, false, "")), ((2, false, false, 128, mashN), (TF0, "mono_native", combsN, false, "")), ((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, "")), ((2, false, true, 256, mepoN), (TF0, "mono_native", combsN, false, ""))], good_max_mono_iters = default_max_mono_iters, good_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 => ["--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, generate_isabelle_info = false, good_slices = (* FUDGE *) K [((2, false, false, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_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 => [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, generate_isabelle_info = false, good_slices = (* FUDGE *) K [((6, false, false, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")), ((6, false, false, 512, meshN), (TF0, "mono_native", liftingN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_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 => [(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, generate_isabelle_info = false, good_slices = (* FUDGE *) K [((12, false, false, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_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 = {exec = (["SPASS_HOME"], ["SPASS"]), arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => ["-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, generate_isabelle_info = true, good_slices = (* FUDGE *) K [((2, false, false, 150, meshN), (DFG Monomorphic, "mono_native", combsN, true, "")), ((2, false, false, 500, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2SOS)), ((2, false, false, 50, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2LR0LT0)), ((2, false, false, 250, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2NuVS0)), ((2, false, false, 1000, mepoN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H1SOS)), ((2, false, true, 150, meshN), (DFG Monomorphic, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), ((2, false, false, 300, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2SOS)), ((2, false, false, 100, meshN), (DFG Monomorphic, "mono_native", combs_and_liftingN, true, spass_H2))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} 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 => [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, generate_isabelle_info = false, good_slices = (* FUDGE *) K [((2, false, false, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)), ((2, false, false, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)), ((2, false, false, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), ((2, false, true, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)), ((2, false, false, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), ((2, false, false, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)), ((2, false, false, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)), ((2, false, false, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} val vampire = (vampireN, fn () => vampire_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 => ["--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, generate_isabelle_info = true, good_slices = K [((1, false, false, 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")), (* sh5_sh1.sh *) ((1, false, false, 512, mepoN), (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")), (* sh10_c_ic.sh *) ((1, false, false, 1024, meshN), (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")), (* sh8_shallow_sine.sh *) ((1, false, false, 256, 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")), (* sh10_new_c.s3.sh *) ((1, false, true, 512, 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=lift --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")), (* sh8_b.comb.sh (modified) *) ((1, false, false, 1024, mashN), (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 --avatar=eager --split-only-ground=true")), (* sh5_add_var_l_av.sh *) ((1, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --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=2 --max-inferences=3 --boolean-reasoning=bool-hoist --bool-select=LO --ext-rules=off --kbo-weight-fun=lambda-def-invfreqrank --ho-prim-enum=none --ho-unif-level=pragmatic-framework -q \"1|prefer-sos|conjecture-relative-var(1.01,s,f)\" -q \"4|const|conjecture-relative-var(1.05,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1.02,l,f)\" -q \"4|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=true --select=e-selection2 --solve-formulas=true --lambdasup=0 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-max-derived=48 --e-encode-lambdas=lift --presaturate=true --prec-gen-fun=invfreq --e-call-point=0.2 --e-auto=true --sine-trim-implications=true")), (* sh10_e_lift.sh *) ((1, false, false, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-const --ho-prim-enum=neg --ho-prim-enum-early-bird=true --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework --ho-unif-max-depth=1 --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true -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 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=false --select=e-selection10 --solve-formulas=true --sup-at-vars=false --sup-at-var-headed=false --sup-from-var-headed=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=4 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-max-derived=32 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --e-call-point=0.16")), (* sh5_shallow_sine.sh *) ((1, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=bool-hoist --ext-rules=off --recognize-injectivity=true --ho-unif-level=full-framework -q \"4|prefer-goals|pnrefined(1,1,1,2,2,2,0.5)\" -q \"1|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-ho-steps|conjecture-relative-var(1.01,s,f)\" -q \"1|prefer-processed|fifo\" --select=bb+ho-selection --scan-clause-ac=false --kbo-weight-fun=invfreqrank --fluidsup=true --boolean-reasoning=bool-hoist --fluid-log-hoist=true --fluid-hoist=true --ite-axioms=true --lazy-cnf=true --ho-solid-decider=true --ho-fixpoint-decider=true --bool-select=\"sel1(pos_ctx)\" --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-call-point=0.35 --avatar=off --e-max-derived=50")), (* sh5_e_short1.sh *) ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --boolean-reasoning=simpl-only --select=e-selection12 --prec-gen-fun=invfreq_conj --ord=lambda_kbo --ho-unif-level=full-framework --ho-pattern-decider=true --ho-solid-decider=false --ho-fixpoint-decider=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=1 --sine=100 --sine-depth-min=1 --sine-depth-max=5 --sine-tolerance=1.5 -q \"1|prefer-sos|default\" -q \"8|prefer-processed|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --kbo-weight-fun=arity0")), (* sh5_32.sh *) ((1, false, false, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=2 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-elims=0 --ho-max-identifications=1 --max-inferences=3 --ext-rules=off --recognize-injectivity=true --ho-prim-enum=none --ho-choice-inst=true -q \"3|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"3|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"1|prefer-processed|fifo\" --select=MaxGoalNS --sine=60 --sine-tolerance=1.5 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=3 --kbo-weight-fun-from-precedence=true --kbo-weight-fun-from-precedence-rank=5 --trigger-bool-inst=1 --avatar=lazy --tptp-def-as-rewrite --rewrite-before-cnf=true --sup-from-var-headed=false --sup-at-vars=false")), (* sh5_sh4.sh *) ((1, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--tptp-def-as-rewrite --rewrite-before-cnf=true --mode=lambda-free-intensional --check-lambda-free=false --boolean-reasoning=simpl-only --post-cnf-lambda-lifting=true --ext-rules=off --ho-prim-enum=none --recognize-injectivity=true --no-max-vars --select=e-selection8 --prec-gen-fun=invfreq --kbo-weight-fun=invfreqrank --kbo-const-weight=2 --ord=lambdafree_kbo --ignore-orphans=true -q \"1|prefer-sos|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|conj_pref_weight(0.5,100,0.2,0.2,4)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.3,0.25,100,100,100,100,1.5,1.5,1)\" -q \"1|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --lazy-cnf=true --lazy-cnf-renaming-threshold=2")), (* sh5_lifting2.sh *) ((1, false, false, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --tptp-rewrite-formulas-only=true --mode=ho-pragmatic --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=neg --ho-prim-max=1 --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars -q \"1|prefer-sos|conjecture-relative-var(1.02,l,f)\" -q \"4|const|conjecture-relative-var(1,s,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --sine=50 --sine-tolerance=10 --sine-depth-max=5 --sine-depth-min=1 --e-max-derived=64 --e-encode-lambdas=lift --scan-clause-ac=false --prec-gen-fun=invfreq_conj --ord=lambda_kbo --solid-subsumption=true --ignore-orphans=true --e-call-point=0.2")), (* sh5_noforms.sh *) ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=4 --ho-unif-max-depth=3 --ho-max-elims=0 --ho-max-app-projections=1 --ho-max-identifications=0 --ho-max-rigid-imitations=2 --ho-unif-level=pragmatic-framework --boolean-reasoning=simpl-only --kbo-weight-fun=freqrank --ext-rules=ext-family --ext-rules-max-depth=2 --ho-prim-enum=eq --ho-prim-max=2 --interpret-bool-funs=false -q \"2|prefer-goals|default\" -q \"8|prefer-sos|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --recognize-injectivity=true --ho-selection-restriction=none --select=ho-selection2 --solve-formulas=true")), (* sh8_old_zip1.sh *) ((1, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --tptp-def-as-rewrite --rewrite-before-cnf=true --kbo-weight-fun=freqrank -q \"1|prefer-sos|default\" -q \"1|prefer-goals|conjecture-relative-var(1.03,s,f)\" -q \"1|prefer-non-goals|default\" -q \"5|const|conjecture-relative-var(1.01,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|const|conjecture-relative-var(1.05,l,f)\" -q \"1|defer-sos|conjecture-relative-var(1.1,s,f)\" --select=e-selection9 --recognize-injectivity=true --ho-choice-inst=false --ho-selection-restriction=none --sine=50 --sine-tolerance=3 --sine-depth-max=3 --sine-depth-min=1 --eq-encode=true --avatar=eager --sine-trim-implications=true"))], (* sh5_sh.eqenc.sh *) good_max_mono_iters = default_max_mono_iters, good_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 generate_isabelle_info good_slice = {exec = isabelle_scala_function, arguments = fn _ => fn _ => fn command => fn timeout => fn problem => [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, generate_isabelle_info = generate_isabelle_info, good_slices = fn ctxt => [good_slice ctxt], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} : atp_config fun remotify_config system_name system_versions good_slice ({proof_delims, known_failures, prem_role, generate_isabelle_info, ...} : atp_config) = remote_config system_name system_versions proof_delims known_failures prem_role generate_isabelle_info good_slice fun remote_atp name system_name system_versions proof_delims known_failures prem_role generate_isabelle_info good_slice = (remote_prefix ^ name, fn () => remote_config system_name system_versions proof_delims known_failures prem_role generate_isabelle_info good_slice) fun remotify_atp (name, config) system_name system_versions good_slice = (remote_prefix ^ name, remotify_config system_name system_versions good_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 false (K ((1000 (* infinity *), false, false, 50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *)) val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] (K ((1000 (* infinity *), false, false, 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 ((1000 (* infinity *), false, false, 250, meshN), (TF1, "poly_native", keep_lamsN, false, "")) (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] (K ((1000 (* infinity *), false, false, 750, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] (K ((1000 (* infinity *), false, false, 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 ((1000 (* infinity *), false, false, 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 ((1000 (* infinity *), false, false, 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 ((1000 (* infinity *), false, false, 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 [])))), proof_delims = [], known_failures = known_szs_status_failures, prem_role = prem_role, generate_isabelle_info = false, good_slices = K [((2, false, false, 256, "mepo"), (format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))], good_max_mono_iters = default_max_mono_iters, good_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) 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 ()) val local_atps = [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, zipperposition] val remote_atps = [remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, remote_waldmeister, remote_zipperposition] val dummy_atps = [dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced] val non_dummy_atps = local_atps @ remote_atps val all_atps = non_dummy_atps @ dummy_atps val _ = Theory.setup (fold add_atp all_atps) val local_atps = map fst local_atps val remote_atps = map fst remote_atps val dummy_atps = map fst dummy_atps val non_dummy_atps = map fst non_dummy_atps val all_atps = map fst all_atps end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML @@ -1,414 +1,414 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.ML Author: Jasmin Blanchette, TU Muenchen Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. *) signature SLEDGEHAMMER_COMMANDS = sig type params = Sledgehammer_Prover.params val provers : string Unsynchronized.ref val default_params : theory -> (string * string) list -> params val parse_params: (string * string) list parser end; structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = struct open ATP_Util open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_SMT open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer val runN = "run" val supported_proversN = "supported_provers" val refresh_tptpN = "refresh_tptp" (** Sledgehammer commands **) fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) (*** parameters ***) val provers = Unsynchronized.ref "" type raw_param = string * string list val default_default_params = [("debug", "false"), ("verbose", "false"), ("overlord", "false"), ("spy", "false"), ("abduce", "smart"), - ("check_consistent", "smart"), + ("check_inconsistent", "smart"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), ("uncurried_aliases", "smart"), ("learn", "true"), ("fact_filter", "smart"), ("induction_rules", "smart"), ("max_facts", "smart"), ("fact_thresholds", "0.45 0.85"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), ("max_proofs", "4"), ("isar_proofs", "smart"), ("compress", "smart"), ("try0", "true"), ("smt_proofs", "true"), ("minimize", "true"), ("slices", string_of_int (12 * Multithreading.max_threads ())), ("preplay_timeout", "1")] val alias_params = [("prover", ("provers", [])), (* undocumented *) ("dont_abduce", ("abduce", ["0"])), ("dont_preplay", ("preplay_timeout", ["0"])), ("dont_compress", ("compress", ["1"])), ("dont_slice", ("slices", ["1"])), ("isar_proof", ("isar_proofs", [])) (* legacy *)] val negated_alias_params = [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), - ("dont_check_consistent", "check_consistent"), + ("dont_check_inconsistent", "check_inconsistent"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), ("no_isar_proofs", "isar_proofs"), ("dont_minimize", "minimize"), ("dont_try0", "try0"), ("no_smt_proofs", "smt_proofs")] val property_dependent_params = ["provers", "timeout"] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) alias_params s orelse AList.defined (op =) negated_alias_params s orelse member (op =) property_dependent_params s orelse s = "expect" fun is_prover_list ctxt s = (case space_explode " " s of ss as _ :: _ => forall (is_prover_supported ctxt) ss | _ => false) fun unalias_raw_param (name, value) = (case AList.lookup (op =) alias_params name of SOME (name', []) => (name', value) | SOME (param' as (name', _)) => if value <> ["false"] then param' else error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")") | NONE => (case AList.lookup (op =) negated_alias_params name of SOME name' => (name', (case value of ["false"] => ["true"] | ["true"] => ["false"] | [] => ["false"] | _ => value)) | NONE => (name, value))) val any_type_enc = type_enc_of_string Strict "erased" (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" can be omitted. For the last four, this is a secret feature. *) fun normalize_raw_param ctxt = unalias_raw_param #> (fn (name, value) => if is_known_raw_param name then (name, value) else if null value then if is_prover_list ctxt name then ("provers", [name]) else if can (type_enc_of_string Strict) name then ("type_enc", [name]) else if can (trans_lams_of_string ctxt any_type_enc) name then ("lam_trans", [name]) else if member (op =) fact_filters name then ("fact_filter", [name]) else if is_some (Int.fromString name) then ("max_facts", [name]) else error ("Unknown parameter: " ^ quote name) else error ("Unknown parameter: " ^ quote name)) (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) val implode_param = strip_spaces_except_between_idents o space_implode " " (* FIXME: use "Generic_Data" *) structure Data = Theory_Data ( type T = raw_param list val empty = default_default_params |> map (apsnd single) fun merge data : T = AList.merge (op =) (K true) data ) (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value ctxt = \ \see also \<^system_option>\sledgehammer_provers\\ filter (is_prover_installed ctxt) (smts ctxt @ local_atps) |> implode_param fun set_default_raw_param param thy = let val ctxt = Proof_Context.init_global thy in thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) end fun default_raw_params thy = let val ctxt = Proof_Context.init_global thy in Data.get thy |> fold (AList.default (op =)) [("provers", [(case !provers of "" => default_provers_param_value ctxt | s => s)]), ("timeout", let val timeout = Options.default_int \<^system_option>\sledgehammer_timeout\ in [if timeout <= 0 then "none" else string_of_int timeout] end)] end fun extract_params mode default_params override_params = let val raw_params = rev override_params @ rev default_params val lookup = Option.map implode_param o AList.lookup (op =) raw_params val lookup_string = the_default "" o lookup fun general_lookup_bool option default_value name = (case lookup name of SOME s => parse_bool_option option name s | NONE => default_value) val lookup_bool = the o general_lookup_bool false (SOME false) fun lookup_time name = (case lookup name of SOME s => parse_time name s | NONE => Time.zeroTime) fun lookup_int name = (case lookup name of NONE => 0 | SOME s => (case Int.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))) fun lookup_real name = (case lookup name of NONE => 0.0 | SOME s => (case Real.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value"))) fun lookup_real_pair name = (case lookup name of NONE => (0.0, 0.0) | SOME s => (case s |> space_explode " " |> map Real.fromString of [SOME r1, SOME r2] => (r1, r2) | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ \values (e.g., \"0.6 0.95\")"))) fun lookup_option lookup' name = (case lookup name of SOME "smart" => NONE | _ => SOME (lookup' name)) val debug = mode <> Auto_Try andalso lookup_bool "debug" val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val abduce = if mode = Auto_Try then SOME 0 else lookup_option lookup_int "abduce" - val check_consistent = + val check_inconsistent = if mode = Auto_Try then SOME false - else lookup_option lookup_bool "check_consistent" + else lookup_option lookup_bool "check_inconsistent" val type_enc = if mode = Auto_Try then NONE else (case lookup_string "type_enc" of "smart" => NONE | s => (type_enc_of_string Strict s; SOME s)) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" val learn = lookup_bool "learn" val fact_filter = lookup_option lookup_string "fact_filter" |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf) val induction_rules = lookup_option (the o induction_rules_of_string o lookup_string) "induction_rules" val max_facts = lookup_option lookup_int "max_facts" val fact_thresholds = lookup_real_pair "fact_thresholds" val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" val max_proofs = lookup_int "max_proofs" val isar_proofs = lookup_option lookup_bool "isar_proofs" val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") val try0 = lookup_bool "try0" val smt_proofs = lookup_bool "smt_proofs" val minimize = mode <> Auto_Try andalso lookup_bool "minimize" val slices = if mode = Auto_Try then 1 else Int.max (1, lookup_int "slices") val timeout = lookup_time "timeout" val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, - abduce = abduce, check_consistent = check_consistent, type_enc = type_enc, strict = strict, + abduce = abduce, check_inconsistent = check_inconsistent, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, max_proofs = max_proofs, isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params fun default_params thy = get_params Normal thy o map (apsnd single) val silence_state = Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) (* Sledgehammer the given subgoal *) val default_learn_prover_timeout = 2.0 fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 = let (* We generally want chained facts to be picked up by the relevance filter, because it can then give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, verbose output, machine learning). However, if the fact is available by no other means (not even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice but to insert it into the state as an additional hypothesis. *) val {facts = chained0, ...} = Proof.goal state0 val (inserts, keep_chained) = if null chained0 orelse #only fact_override then (chained0, []) else let val ctxt0 = Proof.context_of state0 in List.partition (is_useful_unnamed_local_fact ctxt0) chained0 end val state = state0 |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained) |> silence_state val thy = Proof.theory_of state val ctxt = Proof.context_of state val override_params = override_params |> map (normalize_raw_param ctxt) in if subcommand = runN then let val i = the_default 1 opt_i in ignore (run_sledgehammer (get_params Normal thy override_params) Normal writeln_result i fact_override state) end else if subcommand = supported_proversN then supported_provers ctxt else if subcommand = unlearnN then mash_unlearn ctxt else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse subcommand = relearn_isarN orelse subcommand = relearn_proverN then (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt else (); mash_learn ctxt (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) (get_params Normal thy ([("timeout", [string_of_real default_learn_prover_timeout]), ("slice", ["false"])] @ override_params @ [("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_proverN orelse subcommand = relearn_proverN)) else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else error ("Unknown subcommand: " ^ quote subcommand) end fun string_of_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) val parse_query_bang = \<^keyword>\?\ || \<^keyword>\!\ || \<^keyword>\!!\ val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] val parse_params = parse_raw_params >> map (apsnd implode_param) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) || (Args.add |-- Args.colon |-- Scan.succeed [] >> add_fact_override) || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) || (Args.del |-- Args.colon |-- Scan.succeed [] >> del_fact_override) || (parse_fact_refs >> only_fact_override) val parse_fact_override = Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) no_fact_override val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer\ "search for first-order proof using automatic theorem provers" (Scan.optional Parse.name runN -- parse_raw_params -- parse_fact_override -- Scan.option Parse.nat >> (fn (((subcommand, params), fact_override), opt_i) => Toplevel.keep_proof (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of))) val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer_params\ "set and display the default parameters for Sledgehammer" (parse_raw_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ (case rev (default_raw_params thy) of [] => "none" | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) val _ = Try.tool_setup {name = sledgehammerN, weight = 40, auto_option = \<^system_option>\auto_sledgehammer\, body = fn auto => fn state => let val thy = Proof.theory_of state val mode = if auto then Auto_Try else Try val i = 1 in run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) |> apsnd (map_prod short_string_of_sledgehammer_outcome single) end} val _ = Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, writeln_result, ...} => (case try Toplevel.proof_of st of SOME state => let val [provers_arg, isar_proofs_arg, try0_arg] = args val override_params = ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), ("try0", [try0_arg]), ("debug", ["false"]), ("verbose", ["false"]), ("overlord", ["false"])]); in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end | NONE => error "Unknown proof context")) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML @@ -1,279 +1,279 @@ (* 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 base_slice = Sledgehammer_ATP_Systems.base_slice 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, abduce : int option, - check_consistent : bool option, + check_inconsistent : bool option, 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, max_proofs : int, 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 slice_timeout : int -> int -> Time.time -> Time.time type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, has_already_found_something : unit -> bool, found_something : string -> unit} datatype prover_slice_extra = ATP_Slice of atp_slice | SMT_Slice of string list type prover_slice = base_slice * prover_slice_extra 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_slice -> prover_result val SledgehammerN : string val default_abduce_max_candidates : int val str_of_mode : mode -> string val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string val is_atp : string -> bool val bunches_of_proof_methods : Proof.context -> bool -> bool -> string -> proof_method list list val facts_of_filter : string -> (string * fact list) list -> fact list val facts_of_basic_slice : base_slice -> (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" val default_abduce_max_candidates = 1 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 =) all_atps type params = {debug : bool, verbose : bool, overlord : bool, spy : bool, provers : string list, abduce : int option, - check_consistent : bool option, + check_inconsistent : bool option, 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, max_proofs : int, 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 slice_timeout slice_size slices timeout = let val max_threads = Multithreading.max_threads () val batches = (slices + max_threads - 1) div max_threads in seconds (Real.fromInt slice_size * Time.toReal timeout / Real.fromInt batches) end type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, has_already_found_something : unit -> bool, found_something : string -> unit} datatype prover_slice_extra = ATP_Slice of atp_slice | SMT_Slice of string list type prover_slice = base_slice * prover_slice_extra 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_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 smt_proofs needs_full_types desperate_lam_trans = let val misc_methodss = [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method, Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]] val metis_methodss = [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_Strategies.all_veriT_stgies (Context.Proof ctxt)), [SMT_Method SMT_Z3]] else [] in misc_methodss @ metis_methodss @ smt_methodss end fun facts_of_filter fact_filter factss = (case AList.lookup (op =) factss fact_filter of SOME facts => facts | NONE => snd (hd factss)) fun facts_of_basic_slice (_, _, _, num_facts, fact_filter) factss = let val facts = facts_of_filter fact_filter factss val (goal_facts, nongoal_facts) = List.partition (equal sledgehammer_goal_as_fact o fst o fst) facts in goal_facts @ take num_facts nongoal_facts end fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = filter ((member (eq_fst (op =)) used o fst) orf (if keep_chained then is_fact_chained else K false)) val max_fact_instances = 10 (* FUDGE *) val max_schematics = 20 (* 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 #> Config.put Monomorph.max_schematics max_schematics fun supported_provers ctxt = let val local_provers = sort_strings (local_atps @ SMT_Config.available_solvers_of ctxt) val remote_provers = sort_strings remote_atps in writeln ("Supported provers: " ^ commas (local_provers @ remote_provers)) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML @@ -1,267 +1,267 @@ (* 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 get_prover : Proof.context -> mode -> string -> prover val get_slices : Proof.context -> string -> prover_slice list val binary_min_facts : int Config.T val minimize_facts : (thm list -> unit) -> string -> params -> prover_slice -> 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 = is_atp orf is_smt_prover ctxt fun is_prover_installed ctxt prover_name = if is_atp prover_name then let val thy = Proof_Context.theory_of ctxt in is_atp_installed thy prover_name end else is_smt_prover_installed ctxt prover_name fun get_prover ctxt mode name = if is_atp 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) fun get_slices ctxt name = let val thy = Proof_Context.theory_of ctxt in if is_atp name then map (apsnd ATP_Slice) (#good_slices (get_atp thy name ()) ctxt) else if is_smt_prover ctxt name then map (apsnd SMT_Slice) (SMT_Solver.good_slices 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) - (slice as ((_, _, check_consistent, _, fact_filter), slice_extra)) silent + (slice as ((_, _, check_inconsistent, _, fact_filter), slice_extra)) 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, abduce = SOME 0, check_consistent = SOME false, strict = strict, + type_enc = type_enc, abduce = SOME 0, check_inconsistent = SOME false, 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, max_proofs = 1, 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, factss = [("", facts)], has_already_found_something = K false, found_something = K ()} val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, message} = prover params problem ((1, false, false, length facts, fact_filter), slice_extra) 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 " ^ (if check_consistent then "inconsistency" else "proof") ^ + "Found " ^ (if check_inconsistent then "inconsistency" else "proof") ^ (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ " (" ^ string_of_time run_time ^ ")")); result end (* 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, ...}) slice silent i n state goal facts = let val ctxt = Proof.context_of state val prover = get_prover ctxt Minimize prover_name val (chained, non_chained) = List.partition is_fact_chained facts fun test timeout non_chained = test_facts params 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 _ => "Warning: " ^ msg) end fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) ({state, goal, subgoal, subgoal_count, ...} : prover_problem) slice (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 slice (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 slice = get_prover ctxt mode name params problem slice |> maybe_minimize mode do_learn name params problem slice end;