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,522 +1,522 @@ (* 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 skolemize_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] @ 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_skolemize_rule = member (op =) skolemize_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 = 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_skolemizing_line (_, _, _, rule', deps') = is_skolemize_rule rule' andalso member (op =) deps' name fun is_before_skolemize_rule () = exists is_skolemizing_line lines in if is_duplicate orelse (role = Plain andalso not (is_skolemize_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_skolemize_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_Default :: meths + else if smt_proofs then 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 skolems_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) |> (fn x => fold_rev add_line_pass1 x []) |> 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 (skos, proof_methods) = (if is_skolemize_rule rule then (skolems_of ctxt goal, skolem_methods) else if is_arith_rule rule then ([], arith_methods) else ([], rewrite_methods)) ||> massage_methods val prove = Prove { qualifiers = [], obtains = skos, label = label, goal = goal, subproofs = [], facts = ([], []), proof_methods = proof_methods, comment = ""} in (prove, ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd)) end val (lems, _) = fold_map add_lemma (map_filter (get_role (curry (op =) 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 skolem = is_skolemize_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 skolem 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 skolem andalso is_clause_tainted g then let val skos = skolems_of ctxt (prop_of_clause g) val subproof = Proof {fixes = skos, 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 skolem then (case skolems_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 (keep_fastest_method_of_isar_step (!preplay_data) #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |> tap (trace_isar_proof "Minimized") |> `(preplay_outcome_of_isar_proof (!preplay_data)) ||> (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_proof_methods.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML @@ -1,206 +1,206 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen Reconstructors. *) signature SLEDGEHAMMER_PROOF_METHODS = sig type stature = ATP_Problem_Generate.stature datatype SMT_backend = - SMT_Default | + SMT_Z3 | SMT_Verit of string datatype proof_method = Metis_Method of string option * string option | Meson_Method | SMT_Method of SMT_backend | SATx_Method | Blast_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Moura_Method | Linarith_Method | Presburger_Method | Algebra_Method datatype play_outcome = Played of Time.time | Play_Timed_Out of Time.time | Play_Failed type one_line_params = ((string * stature) list * (proof_method * play_outcome)) * string * int * int val is_proof_method_direct : proof_method -> bool val proof_method_distinguishes_chained_and_direct : proof_method -> bool val string_of_proof_method : string list -> proof_method -> string val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic val string_of_play_outcome : play_outcome -> string val play_outcome_ord : play_outcome ord val one_line_proof_text : Proof.context -> int -> one_line_params -> string end; structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS = struct open ATP_Util open ATP_Problem_Generate open ATP_Proof_Reconstruct datatype SMT_backend = - SMT_Default | + SMT_Z3 | SMT_Verit of string datatype proof_method = Metis_Method of string option * string option | Meson_Method | SMT_Method of SMT_backend | SATx_Method | Blast_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Moura_Method | Linarith_Method | Presburger_Method | Algebra_Method datatype play_outcome = Played of Time.time | Play_Timed_Out of Time.time | Play_Failed type one_line_params = ((string * stature) list * (proof_method * play_outcome)) * string * int * int fun is_proof_method_direct (Metis_Method _) = true | is_proof_method_direct Meson_Method = true | is_proof_method_direct (SMT_Method _) = true | is_proof_method_direct Simp_Method = true | is_proof_method_direct _ = false fun proof_method_distinguishes_chained_and_direct Simp_Method = true | proof_method_distinguishes_chained_and_direct _ = false fun is_proof_method_multi_goal Auto_Method = true | is_proof_method_multi_goal _ = false fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")" fun string_of_proof_method ss meth = let val meth_s = (case meth of Metis_Method (NONE, NONE) => "metis" | Metis_Method (type_enc_opt, lam_trans_opt) => "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" | Meson_Method => "meson" - | SMT_Method SMT_Default => "smt" + | SMT_Method SMT_Z3 => "smt (z3)" | SMT_Method (SMT_Verit strategy) => "smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")" | SATx_Method => "satx" | Blast_Method => "blast" | Simp_Method => if null ss then "simp" else "simp add:" | Auto_Method => "auto" | Fastforce_Method => "fastforce" | Force_Method => "force" | Moura_Method => "moura" | Linarith_Method => "linarith" | Presburger_Method => "presburger" | Algebra_Method => "algebra") in maybe_paren (space_implode " " (meth_s :: ss)) end fun tac_of_proof_method ctxt (local_facts, global_facts) meth = let fun tac_of_metis (type_enc_opt, lam_trans_opt) = let val ctxt = ctxt |> Config.put Metis_Tactic.verbose false |> Config.put Metis_Tactic.trace false in SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt), global_facts) ctxt local_facts) end - fun tac_of_smt SMT_Default = SMT_Solver.smt_tac + fun tac_of_smt SMT_Z3 = SMT_Solver.smt_tac | tac_of_smt (SMT_Verit strategy) = Verit_Proof.verit_tac_stgy strategy in (case meth of Metis_Method options => tac_of_metis options | SMT_Method backend => tac_of_smt backend ctxt (local_facts @ global_facts) | _ => Method.insert_tac ctxt local_facts THEN' (case meth of Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) | _ => Method.insert_tac ctxt global_facts THEN' (case meth of SATx_Method => SAT.satx_tac ctxt | Blast_Method => blast_tac ctxt | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt) | Fastforce_Method => Clasimp.fast_force_tac ctxt | Force_Method => Clasimp.force_tac ctxt | Moura_Method => moura_tac ctxt | Linarith_Method => Lin_Arith.tac ctxt | Presburger_Method => Cooper.tac true [] [] ctxt | Algebra_Method => Groebner.algebra_tac [] [] ctxt))) end fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) | string_of_play_outcome (Play_Timed_Out time) = if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out" | string_of_play_outcome Play_Failed = "failed" fun play_outcome_ord (Played time1, Played time2) = int_ord (apply2 Time.toMilliseconds (time1, time2)) | play_outcome_ord (Played _, _) = LESS | play_outcome_ord (_, Played _) = GREATER | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = int_ord (apply2 Time.toMilliseconds (time1, time2)) | play_outcome_ord (Play_Timed_Out _, _) = LESS | play_outcome_ord (_, Play_Timed_Out _) = GREATER | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL fun apply_on_subgoal _ 1 = "by " | apply_on_subgoal 1 _ = "apply " | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n (* FIXME *) fun proof_method_command meth i n used_chaineds _(*num_chained*) extras = let val (indirect_ss, direct_ss) = if is_proof_method_direct meth then ([], extras |> proof_method_distinguishes_chained_and_direct meth ? append used_chaineds) else (extras, []) in (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^ apply_on_subgoal i n ^ string_of_proof_method direct_ss meth ^ (if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "") end fun try_command_line banner play command = let val s = string_of_play_outcome play in banner ^ ": " ^ Active.sendback_markup_command command ^ (s |> s <> "" ? enclose " (" ")") end fun one_line_proof_text _ num_chained ((used_facts, (meth, play)), banner, subgoal, subgoal_count) = let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in map fst extra |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained |> (if play = Play_Failed then prefix "One-line proof reconstruction failed: " else try_command_line banner play) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML @@ -1,213 +1,213 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Generic prover abstraction for Sledgehammer. *) signature SLEDGEHAMMER_PROVER = sig type atp_failure = ATP_Proof.atp_failure type stature = ATP_Problem_Generate.stature type type_enc = ATP_Problem_Generate.type_enc type fact = Sledgehammer_Fact.fact type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome datatype mode = Auto_Try | Try | Normal | Minimize | MaSh 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, max_facts : int option, fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, isar_proofs : bool option, compress : real option, try0 : bool, smt_proofs : bool, slice : bool, minimize : bool, timeout : Time.time, preplay_timeout : Time.time, expect : string} type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, found_proof : unit -> unit} type prover_result = {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} type prover = params -> prover_problem -> prover_result val SledgehammerN : string val str_of_mode : mode -> string val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string val is_atp : theory -> string -> bool val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string -> proof_method list list val is_fact_chained : (('a * stature) * 'b) -> bool val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context val supported_provers : Proof.context -> unit end; structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = struct open ATP_Proof open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof_Reconstruct open Metis_Tactic open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_ATP_Systems (* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *) val SledgehammerN = "Sledgehammer" datatype mode = Auto_Try | Try | Normal | Minimize | MaSh fun str_of_mode Auto_Try = "Auto Try" | str_of_mode Try = "Try" | str_of_mode Normal = "Normal" | str_of_mode Minimize = "Minimize" | str_of_mode MaSh = "MaSh" val is_atp = member (op =) o supported_atps type params = {debug : bool, verbose : bool, overlord : bool, spy : bool, provers : string list, type_enc : string option, strict : bool, lam_trans : string option, uncurried_aliases : bool option, learn : bool, fact_filter : string option, max_facts : int option, fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, isar_proofs : bool option, compress : real option, try0 : bool, smt_proofs : bool, slice : bool, minimize : bool, timeout : Time.time, preplay_timeout : Time.time, expect : string} type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, found_proof : unit -> unit} type prover_result = {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} type prover = params -> prover_problem -> prover_result fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) fun proof_banner mode name = (case mode of Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this") fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans = let val try0_methodss = if try0 then [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method, Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]] else [] val metis_methods = (if try0 then [] else [Metis_Method (NONE, NONE)]) @ Metis_Method (SOME full_typesN, NONE) :: Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) :: (if needs_full_types then [Metis_Method (SOME really_full_type_enc, NONE), Metis_Method (SOME full_typesN, SOME desperate_lam_trans)] else [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) val smt_methodss = if smt_proofs then - [SMT_Method SMT_Default :: + [SMT_Method SMT_Z3 :: map (fn strategy => SMT_Method (SMT_Verit strategy)) (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))] else [] in try0_methodss @ [metis_methods] @ smt_methodss end fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = filter ((member (eq_fst (op =)) used o fst) orf (if keep_chained then is_fact_chained else K false)) val max_fact_instances = 10 (* FUDGE *) fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters) #> Config.put Monomorph.max_new_instances (max_new_instances |> the_default best_max_new_instances) #> Config.put Monomorph.max_thm_instances max_fact_instances fun supported_provers ctxt = let val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) in writeln ("Supported provers: " ^ commas (local_provers @ remote_provers)) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_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,231 +1,231 @@ (* 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 smt_max_slices : int Config.T val smt_slice_fact_frac : real Config.T val smt_slice_time_frac : real Config.T val smt_slice_min_secs : int Config.T val is_smt_prover : Proof.context -> string -> bool val run_smt_solver : mode -> string -> prover end; structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT = struct open ATP_Util open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover val smt_builtins = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_builtins\ (K true) val smt_triggers = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_triggers\ (K true) val is_smt_prover = member (op =) o SMT_Config.available_solvers_of (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out properly in the SMT module, we must interpret these here. *) val z3_failures = [(101, OutOfResources), (103, MalformedInput), (110, MalformedInput), (112, TimedOut)] val unix_failures = [(134, Crashed), (138, Crashed), (139, Crashed)] val smt_failures = z3_failures @ unix_failures fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) = if genuine then Unprovable else GaveUp | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) = (case AList.lookup (op =) smt_failures code of SOME failure => failure | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code)) | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s (* FUDGE *) val smt_max_slices = Attrib.setup_config_int \<^binding>\sledgehammer_smt_max_slices\ (K 8) val smt_slice_fact_frac = Attrib.setup_config_real \<^binding>\sledgehammer_smt_slice_fact_frac\ (K 0.667) val smt_slice_time_frac = Attrib.setup_config_real \<^binding>\sledgehammer_smt_slice_time_frac\ (K 0.333) val smt_slice_min_secs = Attrib.setup_config_int \<^binding>\sledgehammer_smt_slice_min_secs\ (K 3) val is_boring_builtin_typ = not o exists_subtype (member (op =) [\<^typ>\nat\, \<^typ>\int\, HOLogic.realT]) fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice, ...} : params) state goal i = let fun repair_context ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver name) |> Config.put SMT_Config.verbose debug |> (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 max_slices = if slice then Config.get ctxt smt_max_slices else 1 fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) = let val timer = Timer.startRealTimer () val slice_timeout = if slice < max_slices then let val ms = Time.toMilliseconds timeout in Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs, Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms))) |> Time.fromMilliseconds end else timeout val num_facts = length facts val _ = if debug then quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout |> writeln else () val birth = Timer.checkRealTimer timer val filter_result as {outcome, ...} = SMT_Solver.smt_filter ctxt goal facts i slice_timeout handle exn => if Exn.is_interrupt exn orelse debug then Exn.reraise exn else {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE, atp_proof = K []} val death = Timer.checkRealTimer timer val outcome0 = if is_none outcome0 then SOME outcome else outcome0 val time_so_far = time_so_far + (death - birth) val timeout = timeout - Timer.checkRealTimer timer val too_many_facts_perhaps = (case outcome of NONE => false | SOME (SMT_Failure.Counterexample _) => false | SOME SMT_Failure.Time_Out => slice_timeout <> timeout | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *) | SOME SMT_Failure.Out_Of_Memory => true | SOME (SMT_Failure.Other_Failure _) => true) in if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso timeout > Time.zeroTime then let val new_num_facts = Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts) val factss as (new_fact_filter, _) :: _ = factss |> (fn (x :: xs) => xs @ [x]) |> app_hd (apsnd (take new_num_facts)) val show_filter = fact_filter <> new_fact_filter fun num_of_facts fact_filter num_facts = string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^ " fact" ^ plural_s num_facts val _ = if debug then quote name ^ " invoked with " ^ num_of_facts fact_filter num_facts ^ ": " ^ string_of_atp_failure (failure_of_smt_failure (the outcome)) ^ " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^ "..." |> writeln else () in do_slice timeout (slice + 1) outcome0 time_so_far factss end else {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result, used_from = facts, run_time = time_so_far} end in do_slice timeout 1 NONE Time.zeroTime 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) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = smt_filter_loop name params state goal subgoal factss 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 (); val preferred = if smt_proofs then - SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Default) + SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3) else Metis_Method (NONE, NONE); val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN; in ((preferred, methss), fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), goal) val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params end) end | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end;