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,502 +1,505 @@ (* 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_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_None fun short_string_of_sledgehammer_outcome (SH_Some _) = "some" | short_string_of_sledgehammer_outcome SH_Unknown = "unknown" | short_string_of_sledgehammer_outcome SH_Timeout = "timeout" | short_string_of_sledgehammer_outcome SH_None = "none" fun alternative f (SOME x) (SOME y) = SOME (f (x, y)) | alternative _ (x as SOME _) NONE = x | alternative _ NONE (y as SOME _) = y | alternative _ NONE NONE = NONE fun max_outcome outcomes = let val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes val none = find_first (fn (SH_None, _) => true | _ => false) outcomes in some |> alternative snd unknown |> alternative snd timeout |> alternative snd none |> the_default (SH_Unknown, "") end fun play_one_line_proofs minimize timeout used_facts state 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, goal, ...} = 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 result as (meth, play_outcome) => + |> 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 with dummy timeout *) - | _ => (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))) + (* Otherwise select preferred method *) + | (fst_meth, fst_outcome, _) :: _ => + (used_facts, (preferred_meth, + if fst_meth = preferred_meth then fst_outcome else Play_Timed_Out Time.zeroTime)) + | [] => (used_facts, (preferred_meth, 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, num_facts, fact_filter), _)) name = let val ctxt = Proof.context_of state val _ = spying spy (fn () => (state, subgoal, name, "Launched")) 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) ^ "...") 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 ^ " 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 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 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 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 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 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 some proof but preplay failed") | ("unknown", SH_Unknown) => () | ("timeout", SH_Timeout) => () | ("none", SH_None) => () | _ => error ("Unexpected outcome: " ^ quote outcome_code)) end fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result learn (problem as {state, subgoal, ...}) slice prover_name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout fun really_go () = launch_prover params mode learn problem slice prover_name |> preplay_prover_result params state subgoal fun go () = if debug then really_go () else (really_go () handle ERROR msg => (SH_Unknown, fn () => "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 (inspired by Seventeen evaluation) *) [cvc4N, zipperpositionN, vampireN, veritN, eN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN, vampireN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, vampireN, cvc4N, z3N, z3N, cvc4N, cvc4N] 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 factss ({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, num_facts, fact_filter) => (slice_size, 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, num_facts0, fact_filter0), extra) = let val slice_size = Int.min (max_slice_size, slice_size0) 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, 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, 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 = Synchronized.var "found_proofs" 0 fun found_proof prover_name = if mode = Normal then (Synchronized.change found_proofs (fn n => n + 1); (the_default writeln writeln_result) (prover_name ^ " found a proof...")) else () val ctxt = Proof.context_of state val inst_inducts = induction_rules = SOME Instantiate val {facts = chained_thms, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt val _ = (case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name) | NONE => ()) val _ = print "Sledgehammering..." val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode")) val ({elapsed, ...}, all_facts) = Timing.timing (nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts) concl_t val _ = spying spy (fn () => (state, i, "All", "Extracting " ^ string_of_int (length all_facts) ^ " facts from background theory in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) val spying_str_of_factss = commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) fun get_factss provers = let val max_max_facts = (case max_facts of SOME n => n | NONE => fold (fn prover => fold (fn ((_, n, _), _) => Integer.max n) (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, found_proof = found_proof} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) val launch = launch_prover_and_preplay params mode writeln_result learn val schedule = if mode = Auto_Try then provers else schedule_of_provers provers slices val prover_slices = prover_slices_of_schedule ctxt 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 < max_proofs then launch problem slice prover else (SH_None, "")) prover_slices |> max_outcome) end in (launch_provers () handle Timeout.TIMEOUT _ => (SH_Timeout, "")) |> `(fn (outcome, message) => (case outcome of SH_Some _ => (the_default writeln writeln_result "QED"; true) | SH_Unknown => (the_default writeln writeln_result message; false) | SH_Timeout => (the_default writeln writeln_result "No proof found"; false) | SH_None => (the_default writeln writeln_result (if message = "" then "No proof found" else "Warning: " ^ message); false))) end) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML @@ -1,528 +1,528 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen Isar proof reconstruction from ATP proofs. *) signature SLEDGEHAMMER_ISAR = sig type atp_step_name = ATP_Proof.atp_step_name type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof type stature = ATP_Problem_Generate.stature type one_line_params = Sledgehammer_Proof_Methods.one_line_params val trace : bool Config.T type isar_params = bool * (string option * string option) * Time.time * real option * bool * bool * (term, string) atp_step list * thm val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int -> one_line_params -> string end; structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = struct open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Compress open Sledgehammer_Isar_Minimize structure String_Redirect = ATP_Proof_Redirect( type key = atp_step_name val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') val string_of = fst) open String_Redirect val trace = Attrib.setup_config_bool \<^binding>\sledgehammer_isar_trace\ (K false) val e_definition_rule = "definition" val e_skolemize_rule = "skolemize" val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" val satallax_skolemize_rule = "tab_ex" val vampire_skolemisation_rule = "skolemisation" val veriT_la_generic_rule = "la_generic" val veriT_simp_arith_rule = "simp_arith" val veriT_skolemize_rules = Verit_Proof.skolemization_steps val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") val zipperposition_cnf_rule = "cnf" val symbol_introduction_rules = [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule, zipperposition_cnf_rule, zipperposition_define_rule] @ veriT_skolemize_rules fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix val is_symbol_introduction_rule = member (op =) symbol_introduction_rules fun is_arith_rule rule = String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse rule = veriT_la_generic_rule fun raw_label_of_num num = (num, 0) fun label_of_clause [(num, _)] = raw_label_of_num num | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) fun add_global_fact ss = apsnd (union (op =) ss) fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss | add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names)) fun add_line_pass1 (line as (name, role, t, rule, [])) lines = (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or definitions. *) if role = Conjecture orelse role = Negated_Conjecture then line :: lines else if t aconv \<^prop>\True\ then map (replace_dependencies_in_line (name, [])) lines else if role = Definition orelse role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines else if role = Axiom then lines (* axioms (facts) need no proof lines *) else map (replace_dependencies_in_line (name, [])) lines | add_line_pass1 line lines = line :: lines fun add_lines_pass2 res [] = rev res | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) = let fun normalize role = role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop) val norm_t = normalize role t val is_duplicate = exists (fn (prev_name, prev_role, prev_t, _, _) => (prev_role = Hypothesis andalso prev_t aconv t) orelse (member (op =) deps prev_name andalso Term.aconv_untyped (normalize prev_role prev_t, norm_t))) res fun looks_boring () = t aconv \<^prop>\False\ orelse length deps < 2 fun is_symbol_introduction_line (_, _, _, rule', deps') = is_symbol_introduction_rule rule' andalso member (op =) deps' name fun is_before_symbol_introduction_rule () = exists is_symbol_introduction_line lines in if is_duplicate orelse (role = Plain andalso not (is_symbol_introduction_rule rule) andalso not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso not (null lines) andalso looks_boring () andalso not (is_before_symbol_introduction_rule ())) then add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines) else add_lines_pass2 (line :: res) lines end type isar_params = bool * (string option * string option) * Time.time * real option * bool * bool * (term, string) atp_step list * thm val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method] val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods val systematic_methods = basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods val skolem_methods = Moura_Method :: systematic_methods fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = let val _ = if debug then writeln "Constructing Isar proof..." else () fun generate_proof_text () = let val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = isar_params () in if null atp_proof0 then one_line_proof_text ctxt 0 one_line_params else let val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods fun massage_methods (meths as meth :: _) = if not try0 then [meth] - else if smt_proofs then SMT_Method SMT_Z3 :: meths + else if smt_proofs then insert (op =) (SMT_Method SMT_Z3) meths else meths val (params, _, concl_t) = strip_subgoal goal subgoal ctxt val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd val do_preplay = preplay_timeout <> Time.zeroTime val compress = (case compress of NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0 | SOME n => n) fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem fun introduced_symbols_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev fun get_role keep_role ((num, _), role, t, rule, _) = if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE val trace = Config.get ctxt trace val string_of_atp_steps = let val to_string = ATP_Proof.string_of_atp_step (Syntax.string_of_term ctxt) I in enclose "[\n" "\n]" o cat_lines o map (enclose " " "," o to_string) end val atp_proof = atp_proof0 |> trace ? tap (tracing o prefix "atp_proof0 = " o string_of_atp_steps) |> distinct (op =) (* Zipperposition generates duplicate lines *) |> (fn lines => fold_rev add_line_pass1 lines []) |> add_lines_pass2 [] |> trace ? tap (tracing o prefix "atp_proof = " o string_of_atp_steps) val conjs = map_filter (fn (name, role, _, _, _) => if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) atp_proof val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof fun add_lemma ((label, goal), rule) ctxt = let val (obtains, proof_methods) = (if is_symbol_introduction_rule rule then (introduced_symbols_of ctxt goal, skolem_methods) else if is_arith_rule rule then ([], arith_methods) else ([], rewrite_methods)) ||> massage_methods val prove = Prove { qualifiers = [], obtains = obtains, label = label, goal = goal, subproofs = [], facts = ([], []), proof_methods = proof_methods, comment = ""} in (prove, ctxt |> not (null obtains) ? (Variable.add_fixes (map fst obtains) #> snd)) end val (lems, _) = fold_map add_lemma (map_filter (get_role (member (op =) [Definition, Lemma])) atp_proof) ctxt val bot = #1 (List.last atp_proof) val refute_graph = atp_proof |> map (fn (name, _, _, _, from) => (from, name)) |> make_refute_graph bot |> fold (Atom_Graph.default_node o rpair ()) conjs val axioms = axioms_of_refute_graph refute_graph conjs val tainted = tainted_atoms_of_refute_graph refute_graph conjs val is_clause_tainted = exists (member (op =) tainted) val steps = Symtab.empty |> fold (fn (name as (s, _), role, t, rule, _) => Symtab.update_new (s, (rule, t |> (if is_clause_tainted [name] then HOLogic.dest_Trueprop #> role <> Conjecture ? s_not #> fold exists_of (map Var (Term.add_vars t [])) #> HOLogic.mk_Trueprop else I)))) atp_proof fun is_referenced_in_step _ (Let _) = false | is_referenced_in_step l (Prove {subproofs, facts = (ls, _), ...}) = member (op =) ls l orelse exists (is_referenced_in_proof l) subproofs and is_referenced_in_proof l (Proof {steps, ...}) = exists (is_referenced_in_step l) steps fun insert_lemma_in_step lem (step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs), proof_methods, comment}) = let val l' = the (label_of_isar_step lem) in if member (op =) ls l' then [lem, step] else let val refs = map (is_referenced_in_proof l') subproofs in if length (filter I refs) = 1 then [Prove { qualifiers = qualifiers, obtains = obtains, label = label, goal = goal, subproofs = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subproofs, facts = (ls, gs), proof_methods = proof_methods, comment = comment}] else [lem, step] end end and insert_lemma_in_steps lem [] = [lem] | insert_lemma_in_steps lem (step :: steps) = if is_referenced_in_step (the (label_of_isar_step lem)) step then insert_lemma_in_step lem step @ steps else step :: insert_lemma_in_steps lem steps and insert_lemma_in_proof lem (proof as Proof {steps, ...}) = isar_proof_with_steps proof (insert_lemma_in_steps lem steps) val rule_of_clause_id = fst o the o Symtab.lookup steps o fst val finish_off = close_form #> rename_bound_vars fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off | prop_of_clause names = let val lits = map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) in (case List.partition (can HOLogic.dest_not) lits of (negs as _ :: _, pos as _ :: _) => s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) | _ => fold (curry s_disj) lits \<^term>\False\) end |> HOLogic.mk_Trueprop |> finish_off fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] fun isar_steps outer predecessor accum [] = accum |> (if tainted = [] then (* e.g., trivial, empty proof by Z3 *) cons (Prove { qualifiers = if outer then [Show] else [], obtains = [], label = no_label, goal = concl_t, subproofs = [], facts = sort_facts (the_list predecessor, []), proof_methods = massage_methods systematic_methods', comment = ""}) else I) |> rev | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = let val l = label_of_clause c val t = prop_of_clause c val rule = rule_of_clause_id id val introduces_symbols = is_symbol_introduction_rule rule val deps = ([], []) |> fold add_fact_of_dependency gamma |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext] |> sort_facts val meths = (if introduces_symbols then skolem_methods else if is_arith_rule rule then arith_methods else systematic_methods') |> massage_methods fun prove subproofs facts = Prove { qualifiers = maybe_show outer c, obtains = [], label = l, goal = t, subproofs = subproofs, facts = facts, proof_methods = meths, comment = ""} fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs in if is_clause_tainted c then (case gamma of [g] => if introduces_symbols andalso is_clause_tainted g andalso not (null accum) then let val fixes = introduced_symbols_of ctxt (prop_of_clause g) val subproof = Proof {fixes = fixes, assumptions = [], steps = rev accum} in isar_steps outer (SOME l) [prove [subproof] ([], [])] infs end else steps_of_rest (prove [] deps) | _ => steps_of_rest (prove [] deps)) else steps_of_rest (if introduces_symbols then (case introduced_symbols_of ctxt t of [] => prove [] deps | skos => Prove { qualifiers = [], obtains = skos, label = l, goal = t, subproofs = [], facts = deps, proof_methods = meths, comment = ""}) else prove [] deps) end | isar_steps outer predecessor accum (Cases cases :: infs) = let fun isar_case (c, subinfs) = isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs val c = succedent_of_cases cases val l = label_of_clause c val t = prop_of_clause c val step = Prove { qualifiers = maybe_show outer c, obtains = [], label = l, goal = t, subproofs = map isar_case (filter_out (null o snd) cases), facts = sort_facts (the_list predecessor, []), proof_methods = massage_methods systematic_methods', comment = ""} in isar_steps outer (SOME l) (step :: accum) infs end and isar_proof outer fixes assumptions lems infs = let val steps = fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs) in Proof {fixes = fixes, assumptions = assumptions, steps = steps} end val canonical_isar_proof = refute_graph |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph) |> redirect_graph axioms tainted bot |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof) |> isar_proof true params assms lems |> postprocess_isar_proof_remove_show_stuttering |> postprocess_isar_proof_remove_unreferenced_steps I |> relabel_isar_proof_canonically val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty val _ = fold_isar_steps (fn meth => K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) (steps_of_isar_proof canonical_isar_proof) () fun str_of_preplay_outcome outcome = if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" fun str_of_meth l meth = string_of_proof_method [] meth ^ " " ^ str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) fun comment_of l = map (str_of_meth l) #> commas fun trace_isar_proof label proof = if trace then tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof ctxt subgoal subgoal_count (comment_isar_proof comment_of proof) ^ "\n") else () fun comment_of l (meth :: _) = (case (verbose, Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of (false, Played _) => "" | (_, outcome) => string_of_play_outcome outcome) val (play_outcome, isar_proof) = canonical_isar_proof |> tap (trace_isar_proof "Original") |> compress_isar_proof ctxt compress preplay_timeout preplay_data |> tap (trace_isar_proof "Compressed") |> postprocess_isar_proof_remove_unreferenced_steps (do_preplay ? keep_fastest_method_of_isar_step (!preplay_data) #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |> tap (trace_isar_proof "Minimized") |> `(if do_preplay then preplay_outcome_of_isar_proof (!preplay_data) else K (Play_Timed_Out Time.zeroTime)) ||> (comment_isar_proof comment_of #> chain_isar_proof #> kill_useless_labels_in_isar_proof #> relabel_isar_proof_nicely #> rationalize_obtains_in_isar_proofs ctxt) in (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of (0, 1) => one_line_proof_text ctxt 0 (if is_less (play_outcome_ord (play_outcome, one_line_play)) then (case isar_proof of Proof {steps = [Prove {facts = (_, gfs), proof_methods = meth :: _, ...}], ...} => let val used_facts' = map_filter (fn s => if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained) used_facts then NONE else SOME (s, (Global, General))) gfs in ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) end) else one_line_params) ^ (if isar_proofs = SOME true then "\n(No Isar proof available)" else "") | (_, num_steps) => let val msg = (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @ (if do_preplay then [string_of_play_outcome play_outcome] else []) in one_line_proof_text ctxt 0 one_line_params ^ "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ Active.sendback_markup_command (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) end) end end in if debug then generate_proof_text () else (case try generate_proof_text () of SOME s => s | NONE => one_line_proof_text ctxt 0 one_line_params ^ (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) end fun isar_proof_would_be_a_good_idea (_, play) = (case play of Played _ => false | Play_Timed_Out time => time > Time.zeroTime | Play_Failed => true) fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained (one_line_params as ((_, preplay), _, _, _)) = (if isar_proofs = SOME true orelse (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params else one_line_proof_text ctxt num_chained) one_line_params 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,268 +1,263 @@ (* 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, 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, found_proof : 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 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 -> bool -> string -> - proof_method list list + 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" 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, 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, found_proof : 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 try0 smt_proofs needs_full_types desperate_lam_trans = +fun bunches_of_proof_methods ctxt smt_proofs needs_full_types desperate_lam_trans = let - val try0_methodss = - if try0 then - [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method, - Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]] - else - [] + val misc_methodss = + [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method, + Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]] - val metis_methods = - (if try0 then [] else [Metis_Method (NONE, NONE)]) @ - Metis_Method (SOME full_typesN, NONE) :: - Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) :: - (if needs_full_types then - [Metis_Method (SOME really_full_type_enc, NONE), - Metis_Method (SOME full_typesN, SOME desperate_lam_trans)] - else - [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) + val 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_Proof.all_veriT_stgies (Context.Proof ctxt)), [SMT_Method SMT_Z3]] else [] in - try0_methodss @ [metis_methods] @ smt_methodss + 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 = facts_of_filter fact_filter factss |> take num_facts fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = filter ((member (eq_fst (op =)) used o fst) orf (if keep_chained then is_fact_chained else K false)) val max_fact_instances = 10 (* FUDGE *) fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters) #> Config.put Monomorph.max_new_instances (max_new_instances |> the_default best_max_new_instances) #> Config.put Monomorph.max_thm_instances max_fact_instances fun supported_provers ctxt = let val 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_atp.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML @@ -1,344 +1,348 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen ATPs as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_ATP = sig type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val atp_problem_dest_dir : string Config.T val atp_proof_dest_dir : string Config.T val atp_problem_prefix : string Config.T val atp_completish : int Config.T val atp_full_names : bool Config.T val run_atp : mode -> string -> prover end; structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = struct open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *) val atp_problem_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_dest_dir\ (K "") val atp_proof_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_proof_dest_dir\ (K "") val atp_problem_prefix = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_prefix\ (K "prob") val atp_completish = Attrib.setup_config_int \<^binding>\sledgehammer_atp_completish\ (K 0) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) val atp_full_names = Attrib.setup_config_bool \<^binding>\sledgehammer_atp_full_names\ (K false) fun choose_type_enc strictness format good_type_enc = type_enc_of_string strictness good_type_enc |> adjust_type_enc format fun has_bound_or_var_of_type pred = exists_subterm (fn Var (_, T as Type _) => pred T | Abs (_, T as Type _, _) => pred T | _ => false) (* Unwanted equalities are those between a (bound or schematic) variable that does not properly occur in the second operand. *) val is_exhaustive_finite = let fun is_bad_equal (Var z) t = not (exists_subterm (fn Var z' => z = z' | _ => false) t) | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) | is_bad_equal _ _ = false fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 fun do_formula pos t = (case (pos, t) of (_, \<^Const_>\Trueprop for t1\) => do_formula pos t1 | (true, Const (\<^const_name>\Pure.all\, _) $ Abs (_, _, t')) => do_formula pos t' | (true, Const (\<^const_name>\All\, _) $ Abs (_, _, t')) => do_formula pos t' | (false, Const (\<^const_name>\Ex\, _) $ Abs (_, _, t')) => do_formula pos t' | (_, \<^Const_>\Pure.imp for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^prop>\False\ orelse do_formula pos t2) | (_, \<^Const_>\implies for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^Const>\False\ orelse do_formula pos t2) | (_, \<^Const_>\Not for t1\) => do_formula (not pos) t1 | (true, \<^Const_>\disj for t1 t2\) => forall (do_formula pos) [t1, t2] | (false, \<^Const_>\conj for t1 t2\) => forall (do_formula pos) [t1, t2] | (true, Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) => do_equals t1 t2 | (true, Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2) => do_equals t1 t2 | _ => false) in do_formula true end (* Facts containing variables of finite types such as "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type encodings. *) fun is_dangerous_prop ctxt = transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) val mono_max_privileged_facts = 10 fun suffix_of_mode Auto_Try = "_try" | suffix_of_mode Try = "_try" | suffix_of_mode Normal = "" | suffix_of_mode MaSh = "" | suffix_of_mode Minimize = "_min" (* Important messages are important but not so important that users want to see them each time. *) val atp_important_message_keep_quotient = 25 fun run_atp mode name ({debug, verbose, overlord, strict, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout, preplay_timeout, spy, ...} : params) ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem) slice = let val (basic_slice as (slice_size, _, _), ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) = slice val facts = facts_of_basic_slice basic_slice factss val thy = Proof.theory_of state val ctxt = Proof.context_of state val {exec, arguments, proof_delims, known_failures, prem_role, good_max_mono_iters, good_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name val completish = Config.get ctxt atp_completish val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (problem_dest_dir, proof_dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name |> (fn (dir, prefix) => (dir, dir, prefix)) else (Config.get ctxt atp_problem_dest_dir, Config.get ctxt atp_proof_dest_dir, Config.get ctxt atp_problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |> Path.ext "p" val prob_path = if problem_dest_dir = "" then File.tmp_path problem_file_name else if File.exists (Path.explode problem_dest_dir) then Path.explode problem_dest_dir + problem_file_name else error ("No such directory: " ^ quote problem_dest_dir) val executable = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let val pref = getenv var ^ "/" val paths = map (Path.explode o prefix pref) (if ML_System.platform_is_windows then map (suffix ".exe") (snd exec) @ snd exec else snd exec); in (case find_first File.exists paths of SOME path => path | NONE => error ("Bad executable: " ^ Path.print (hd paths))) end | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) fun run () = let fun monomorphize_facts facts = let val ctxt = ctxt |> repair_monomorph_context max_mono_iters good_max_mono_iters max_new_mono_instances good_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) val subgoal_th = Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy val rths = facts |> chop mono_max_privileged_facts |>> map (pair 1 o snd) ||> map (pair 2 o snd) |> op @ |> cons (0, subgoal_th) in Monomorph.monomorph atp_schematic_consts_of ctxt rths |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end val strictness = if strict then Strict else Non_Strict val type_enc = choose_type_enc strictness good_format good_type_enc val run_timeout = slice_timeout slice_size slices timeout val generous_run_timeout = if mode = MaSh then one_day else run_timeout val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let val generate_info = (case good_format of DFG _ => true | _ => false) val readable_names = not (Config.get ctxt atp_full_names) in facts |> not (is_type_enc_sound type_enc) ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) |> generate_atp_problem ctxt generate_info good_format prem_role type_enc atp_mode good_lam_trans good_uncurried_aliases readable_names true hyp_ts concl_t end) () val () = spying spy (fn () => (state, subgoal, name, "Generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) val args = arguments ctxt full_proofs extra run_timeout prob_path val command = space_implode " " (File.bash_path executable :: args) fun run_command () = if exec = isabelle_scala_function then let val {output, timing} = SystemOnTPTP.run_system_encoded args in (output, timing) end else let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) in (Process_Result.out res, Process_Result.timing_elapsed res) end val _ = atp_problem |> lines_of_atp_problem good_format (fn () => atp_problem_term_order_info atp_problem) |> (exec <> isabelle_scala_function) ? cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val ((output, run_time), ((atp_proof, tstplike_proof), outcome)) = Timeout.apply generous_run_timeout run_command () |>> overlord ? (fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output) |> (fn accum as (output, _) => (accum, extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |>> `(atp_proof_of_tstplike_proof false (perhaps (try (unprefix remote_prefix)) name) atp_problem) handle UNRECOGNIZED_ATP_PROOF () => (([], ""), SOME ProofUnparsable))) handle Timeout.TIMEOUT _ => (("", run_timeout), (([], ""), SOME TimedOut)) | ERROR msg => (("", Time.zeroTime), (([], ""), SOME (UnknownError msg))) val () = spying spy (fn () => (state, subgoal, name, "Running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms")) val outcome = (case outcome of NONE => (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of SOME facts => let val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) in if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure end | NONE => (found_proof name; NONE)) | _ => outcome) in (atp_problem_data, (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, outcome), (good_format, type_enc)) end (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () fun export (_, (output, _, _, _, _, _, _), _) = let val proof_dest_dir_path = Path.explode proof_dest_dir val make_export_file_name = Path.split_ext #> apfst (Path.explode o suffix "_proof" o Path.implode) #> swap #> uncurry Path.ext in if proof_dest_dir = "" then Output.system_message "don't export proof" else if File.exists proof_dest_dir_path then File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output else error ("No such directory: " ^ quote proof_dest_dir) end val ((_, pool, lifted, sym_tab), (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof, outcome), (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message = if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0 then extract_important_message output else "" val (used_facts, preferred_methss, message) = (case outcome of NONE => let val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof + val preferred = Metis_Method (NONE, NONE) val preferred_methss = - (Metis_Method (NONE, NONE), - bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types - (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN)) + (preferred, + if try0 then + bunches_of_proof_methods ctxt smt_proofs needs_full_types + (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN) + else + [[preferred]]) in (used_facts, preferred_methss, fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = let val full_atp_proof = atp_proof_of_tstplike_proof true (perhaps (try (unprefix remote_prefix)) name) atp_problem tstplike_proof val metis_type_enc = if is_typed_helper_used_in_atp_proof full_atp_proof then SOME full_typesN else NONE val metis_lam_trans = if atp_proof_prefers_lifting full_atp_proof then SOME liftingN else NONE val full_atp_proof = full_atp_proof |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> local_name = spassN ? introduce_spass_skolems |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, minimize, full_atp_proof, goal) end val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params ^ (if important_message <> "" then "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message else "") end) end | SOME failure => ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML @@ -1,171 +1,175 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen SMT solvers as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_SMT = sig type stature = ATP_Problem_Generate.stature type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val smt_builtins : bool Config.T val smt_triggers : bool Config.T val is_smt_prover : Proof.context -> string -> bool val is_smt_prover_installed : Proof.context -> string -> bool val run_smt_solver : mode -> string -> prover val smts : Proof.context -> string list end; structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT = struct open ATP_Util open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover val smt_builtins = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_builtins\ (K true) val smt_triggers = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_triggers\ (K true) val smts = sort_strings o SMT_Config.all_solvers_of val is_smt_prover = member (op =) o smts val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out properly in the SMT module, we must interpret these here. *) val z3_failures = [(101, OutOfResources), (103, MalformedInput), (110, MalformedInput), (112, TimedOut)] val unix_failures = [(134, Crashed), (138, Crashed), (139, Crashed)] val smt_failures = z3_failures @ unix_failures fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) = if genuine then Unprovable else GaveUp | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) = (case AList.lookup (op =) smt_failures code of SOME failure => failure | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code)) | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s val is_boring_builtin_typ = not o exists_subtype (member (op =) [\<^typ>\nat\, \<^typ>\int\, HOLogic.realT]) fun smt_filter name ({debug, overlord, max_mono_iters, max_new_mono_instances, type_enc, slices, timeout, ...} : params) state goal i slice_size facts options = let val run_timeout = slice_timeout slice_size slices timeout val (higher_order, nat_as_int) = (case type_enc of SOME s => (SOME (String.isSubstring "native_higher" s), SOME (String.isSubstring "arith" s)) | NONE => (NONE, NONE)) fun repair_context ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver name) |> (case higher_order of SOME higher_order => Config.put SMT_Config.higher_order higher_order | NONE => I) |> (case nat_as_int of SOME nat_as_int => Config.put SMT_Config.nat_as_int nat_as_int | NONE => I) |> (if overlord then Config.put SMT_Config.debug_files (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) else I) |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers) |> not (Config.get ctxt smt_builtins) ? (SMT_Builtin.filter_builtins is_boring_builtin_typ #> Config.put SMT_Systems.z3_extensions false) |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances default_max_new_mono_instances val state = Proof.map_context (repair_context) state val ctxt = Proof.context_of state val timer = Timer.startRealTimer () val birth = Timer.checkRealTimer timer val filter_result as {outcome, ...} = SMT_Solver.smt_filter ctxt goal facts i run_timeout options handle exn => if Exn.is_interrupt exn orelse debug then Exn.reraise exn else {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE, atp_proof = K []} val death = Timer.checkRealTimer timer val run_time = death - birth in {outcome = outcome, filter_result = filter_result, used_from = facts, run_time = run_time} end fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, ...}) ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) slice = let val (basic_slice as (slice_size, _, _), SMT_Slice options) = slice val facts = facts_of_basic_slice basic_slice factss val ctxt = Proof.context_of state val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = smt_filter name params state goal subgoal slice_size facts options val used_facts = (case fact_ids of NONE => map fst used_from | SOME ids => sort_by fst (map (fst o snd) ids)) val outcome = Option.map failure_of_smt_failure outcome val (preferred_methss, message) = (case outcome of NONE => let val _ = found_proof name; val preferred = if smt_proofs then SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default") else Metis_Method (NONE, NONE); - val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN; + val methss = + if try0 then + bunches_of_proof_methods ctxt smt_proofs false liftingN + else + [[preferred]] in ((preferred, methss), fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), goal) val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params end) end | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end;