# HG changeset patch # User blanchet # Date 1306068702 -7200 # Node ID 9e620869a576a4d24e47456702766459cea2934e # Parent 62a14c80d19498d2cebfc588dfcf7bc37073d3f5 improved Waldmeister support -- even run it by default on unit equational goals diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 22 14:51:42 2011 +0200 @@ -383,6 +383,8 @@ val default_max_relevant = Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing prover_name + val is_good_prop = + Sledgehammer_Provers.is_good_prop_for_prover ctxt prover_name val is_built_in_const = Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name val relevance_fudge = @@ -399,8 +401,9 @@ let val facts = Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds - (the_default default_max_relevant max_relevant) is_built_in_const - relevance_fudge relevance_override chained_ths hyp_ts concl_t + (the_default default_max_relevant max_relevant) is_good_prop + is_built_in_const relevance_fudge relevance_override chained_ths + hyp_ts concl_t val problem = {state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 22 14:51:42 2011 +0200 @@ -118,6 +118,8 @@ val default_max_relevant = Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing prover + val is_good_prop = + Sledgehammer_Provers.is_good_prop_for_prover ctxt default_prover val is_built_in_const = Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover val relevance_fudge = @@ -128,8 +130,9 @@ val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal val facts = Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds - (the_default default_max_relevant max_relevant) is_built_in_const - relevance_fudge relevance_override facts hyp_ts concl_t + (the_default default_max_relevant max_relevant) is_good_prop + is_built_in_const relevance_fudge relevance_override facts hyp_ts + concl_t |> map (fst o fst) val (found_facts, lost_facts) = flat proofs |> sort_distinct string_ord diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 22 14:51:42 2011 +0200 @@ -35,6 +35,7 @@ val mk_aconn : connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula + val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula val timestamp : unit -> string val hashw : word * word -> word val hashw_string : string * word -> word @@ -82,6 +83,10 @@ | mk_anot phi = AConn (ANot, [phi]) fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) +fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) + | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) + | formula_map f (AAtom tm) = AAtom (f tm) + val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now (* This hash function is recommended in Compilers: Principles, Techniques, and @@ -172,19 +177,22 @@ (Formula (_, _, AAtom (ATerm (("equal", _), _)), _, _)) = true | is_problem_line_cnf_ueq _ = false -fun open_formula (AQuant (AForall, _, phi)) = open_formula phi - | open_formula phi = phi -fun open_non_conjecture_line (line as Formula (_, Conjecture, _, _, _)) = line - | open_non_conjecture_line (Formula (ident, kind, phi, source, info)) = - Formula (ident, kind, open_formula phi, source, info) - | open_non_conjecture_line line = line +fun open_conjecture_term (ATerm ((s, s'), tms)) = + ATerm (s |> is_atp_variable s ? Name.desymbolize false |> `I, + tms |> map open_conjecture_term) +fun open_formula conj (AQuant (AForall, _, phi)) = open_formula conj phi + | open_formula true (AAtom t) = AAtom (open_conjecture_term t) + | open_formula _ phi = phi +fun open_formula_line (Formula (ident, kind, phi, source, info)) = + Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info) + | open_formula_line line = line fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) = Formula (ident, Hypothesis, mk_anot phi, source, info) | negate_conjecture_line line = line val filter_cnf_ueq_problem = - map (apsnd (map open_non_conjecture_line + map (apsnd (map open_formula_line #> filter is_problem_line_cnf_ueq #> map negate_conjecture_line)) #> (fn problem => diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:42 2011 +0200 @@ -419,8 +419,9 @@ [TFF, FOF] (K (250, ["simple"]) (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] - [("#START OF PROOF", "Proved Goals:")] [] Hypothesis Hypothesis - [CNF_UEQ] (K (500, ["poly_args"]) (* FUDGE *)) + [("#START OF PROOF", "Proved Goals:")] + [(OutOfResources, "Too many function symbols")] Hypothesis + Hypothesis [CNF_UEQ] (K (100, ["poly_args"]) (* FUDGE *)) (* Setup *) diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Sun May 22 14:51:42 2011 +0200 @@ -38,7 +38,7 @@ (* Converts an elim-rule into an equivalent theorem that does not have the predicate variable. Leaves other theorems unchanged. We simply instantiate - the conclusion variable to False. (Cf. "transform_elim_term" in + the conclusion variable to False. (Cf. "transform_elim_prop" in "Sledgehammer_Util".) *) fun transform_elim_theorem th = case concl_of th of (*conclusion variable*) diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 22 14:51:42 2011 +0200 @@ -176,10 +176,6 @@ is_type_level_virtually_sound level orelse level = Finite_Types val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys -fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) - | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) - | formula_map f (AAtom tm) = AAtom (f tm) - fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi | aconn_fold pos f (AImplies, [phi1, phi2]) = f (Option.map not pos) phi1 #> f pos phi2 @@ -452,7 +448,7 @@ let val thy = Proof_Context.theory_of ctxt val t = t |> Envir.beta_eta_contract - |> transform_elim_term + |> transform_elim_prop |> Object_Logic.atomize_term thy val need_trueprop = (fastype_of t = @{typ bool}) val t = t |> need_trueprop ? HOLogic.mk_Trueprop diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 22 14:51:42 2011 +0200 @@ -44,13 +44,13 @@ Proof.context -> unit Symtab.table -> thm list -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list val all_facts : - Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list - -> (((unit -> string) * locality) * (bool * thm)) list + Proof.context -> 'a Symtab.table -> bool -> (term -> bool) -> thm list + -> thm list -> (((unit -> string) * locality) * (bool * thm)) list val const_names_in_fact : theory -> (string * typ -> term list -> bool * term list) -> term -> string list val relevant_facts : - Proof.context -> real * real -> int + Proof.context -> real * real -> int -> (term -> bool) -> (string * typ -> term list -> bool * term list) -> relevance_fudge -> relevance_override -> thm list -> term list -> term -> ((string * locality) * thm) list @@ -785,11 +785,12 @@ (**** Predicates to detect unwanted facts (prolific or likely to cause unsoundness) ****) -fun is_theorem_bad_for_atps thm = +fun is_theorem_bad_for_atps is_good_prop thm = let val t = prop_of thm in - is_formula_too_complex t orelse exists_type type_has_top_sort t orelse - exists_sledgehammer_const t orelse exists_low_level_class_const t orelse - is_metastrange_theorem thm orelse is_that_fact thm + not (is_good_prop t) orelse is_formula_too_complex t orelse + exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse + exists_low_level_class_const t orelse is_metastrange_theorem thm orelse + is_that_fact thm end fun meta_equify (@{const Trueprop} @@ -814,7 +815,7 @@ mk_fact_table normalize_simp_prop snd simps) end -fun all_facts ctxt reserved really_all add_ths chained_ths = +fun all_facts ctxt reserved really_all is_good_prop add_ths chained_ths = let val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy @@ -868,7 +869,7 @@ pair 1 #> fold (fn th => fn (j, rest) => (j + 1, - if is_theorem_bad_for_atps th andalso + if is_theorem_bad_for_atps is_good_prop th andalso not (member Thm.eq_thm add_ths th) then rest else @@ -902,9 +903,9 @@ fun external_frees t = [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) -fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const - fudge (override as {add, only, ...}) chained_ths hyp_ts - concl_t = +fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_good_prop + is_built_in_const fudge (override as {add, only, ...}) + chained_ths hyp_ts concl_t = let val thy = Proof_Context.theory_of ctxt val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), @@ -920,7 +921,7 @@ maps (map (fn ((name, loc), th) => ((K name, loc), (true, th))) o fact_from_ref ctxt reserved chained_ths) add else - all_facts ctxt reserved false add_ths chained_ths) + all_facts ctxt reserved false is_good_prop add_ths chained_ths) |> Config.get ctxt instantiate_inducts ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) |> rearrange_facts ctxt only diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 22 14:51:42 2011 +0200 @@ -183,7 +183,7 @@ (* The first ATP of the list is used by Auto Sledgehammer. Because of the low timeout, it makes sense to put SPASS first. *) fun default_provers_param_value ctxt = - [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt] + [spassN, eN, vampireN, sine_eN, waldmeisterN, SMT_Solver.solver_name_of ctxt] |> map_filter (remotify_prover_if_not_installed ctxt) |> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ()) |> implode_param diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 22 14:51:42 2011 +0200 @@ -71,9 +71,12 @@ val das_Tool : string val select_smt_solver : string -> Proof.context -> Proof.context val is_smt_prover : Proof.context -> string -> bool + val is_unit_equational_atp : Proof.context -> string -> bool val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool val default_max_relevant_for_prover : Proof.context -> bool -> string -> int + val is_unit_equality : term -> bool + val is_good_prop_for_prover : Proof.context -> string -> term -> bool val is_built_in_const_for_prover : Proof.context -> string -> string * typ -> term list -> bool * term list val atp_relevance_fudge : relevance_fudge @@ -120,6 +123,13 @@ fun is_smt_prover ctxt name = member (op =) (SMT_Solver.available_solvers_of ctxt) name +fun is_unit_equational_atp ctxt name = + let val thy = Proof_Context.theory_of ctxt in + case try (get_atp thy) name of + SOME {formats, ...} => member (op =) formats CNF_UEQ + | NONE => false + end + fun is_prover_supported ctxt name = let val thy = Proof_Context.theory_of ctxt in is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name @@ -147,6 +157,20 @@ @{const_name conj}, @{const_name disj}, @{const_name implies}, @{const_name HOL.eq}, @{const_name If}, @{const_name Let}] +fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t + | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) = + is_unit_equality t + | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) = + is_unit_equality t + | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ _ $ _) = + T <> @{typ bool} + | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ _ $ _) = + T <> @{typ bool} + | is_unit_equality _ = false + +fun is_good_prop_for_prover ctxt name = + if is_unit_equational_atp ctxt name then is_unit_equality else K true + fun is_built_in_const_for_prover ctxt name = if is_smt_prover ctxt name then let val ctxt = ctxt |> select_smt_solver name in @@ -390,8 +414,8 @@ (* Facts containing variables of type "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types are omitted. *) -fun is_dangerous_term ctxt = - transform_elim_term +fun is_dangerous_prop ctxt = + transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) @@ -413,13 +437,13 @@ (* We could return (TFF, type_sys) in all cases but this would require the TFF provers to accept problems in which constants are implicitly declared. Today neither SNARK nor ToFoF-E satisfy this criterion. *) - if member (op =) formats FOF then - (FOF, type_sys) - else if member (op =) formats CNF_UEQ then + if member (op =) formats CNF_UEQ then (CNF_UEQ, case type_sys of Tags _ => type_sys | _ => Preds (polymorphism_of_type_sys type_sys, Const_Arg_Types, Light)) + else if member (op =) formats FOF then + (FOF, type_sys) else (TFF, Simple_Types All_Types) fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = @@ -514,7 +538,7 @@ val fairly_sound = is_type_sys_fairly_sound type_sys val facts = facts |> not fairly_sound - ? filter_out (is_dangerous_term ctxt o prop_of o snd + ? filter_out (is_dangerous_prop ctxt o prop_of o snd o untranslated_fact) |> take num_facts |> not (null blacklist) diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 22 14:51:42 2011 +0200 @@ -189,7 +189,9 @@ SOME name => error ("No such prover: " ^ name ^ ".") | NONE => () val _ = print "Sledgehammering..." - val (smts, atps) = provers |> List.partition (is_smt_prover ctxt) + val (smts, (ueq_atps, full_atps)) = + provers |> List.partition (is_smt_prover ctxt) + ||> List.partition (is_unit_equational_atp ctxt) fun launch_provers state get_facts translate maybe_smt_filter provers = let val facts = get_facts () @@ -212,7 +214,7 @@ |> (if blocking then smart_par_list_map else map) (launch problem) |> exists fst |> rpair state end - fun get_facts label relevance_fudge provers = + fun get_facts label is_good_prop relevance_fudge provers = let val max_max_relevant = case max_relevant of @@ -225,7 +227,7 @@ val is_built_in_const = is_built_in_const_for_prover ctxt (hd provers) in - relevant_facts ctxt relevance_thresholds max_max_relevant + relevant_facts ctxt relevance_thresholds max_max_relevant is_good_prop is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t |> tap (fn facts => @@ -241,18 +243,19 @@ else ()) end - fun launch_atps accum = - if null atps then + fun launch_atps label is_good_prop atps accum = + if null atps orelse not (is_good_prop concl_t) then accum else - launch_provers state (get_facts "ATP" atp_relevance_fudge o K atps) - (K (Untranslated_Fact o fst)) (K (K NONE)) atps + launch_provers state + (get_facts label is_good_prop atp_relevance_fudge o K atps) + (K (Untranslated_Fact o fst)) (K (K NONE)) atps fun launch_smts accum = if null smts then accum else let - val facts = get_facts "SMT solver" smt_relevance_fudge smts + val facts = get_facts "SMT solver" (K true) smt_relevance_fudge smts val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt fun smt_filter facts = (if debug then curry (op o) SOME @@ -264,14 +267,19 @@ |> map (launch_provers state (K facts) weight smt_filter o snd) |> exists fst |> rpair state end + val launch_full_atps = launch_atps "ATP" (K true) full_atps + val launch_ueq_atps = + launch_atps "Unit equational provers" is_unit_equality ueq_atps fun launch_atps_and_smt_solvers () = - [launch_atps, launch_smts] + [launch_full_atps, launch_ueq_atps, launch_smts] |> smart_par_list_map (fn f => f (false, state) |> K ()) handle ERROR msg => (print ("Error: " ^ msg); error msg) in (false, state) - |> (if blocking then launch_atps #> not auto ? launch_smts - else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p)) + |> (if blocking then + launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts) + else + (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p)) handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (false, state)) end diff -r 62a14c80d194 -r 9e620869a576 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun May 22 14:51:42 2011 +0200 @@ -25,7 +25,7 @@ val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool val monomorphic_term : Type.tyenv -> term -> term val eta_expand : typ list -> term -> int -> term - val transform_elim_term : term -> term + val transform_elim_prop : term -> term val specialize_type : theory -> (string * typ) -> term -> term val subgoal_count : Proof.state -> int val strip_subgoal : thm -> int -> (string * typ) list * term list * term @@ -210,7 +210,7 @@ predicate variable. Leaves other theorems unchanged. We simply instantiate the conclusion variable to False. (Cf. "transform_elim_theorem" in "Meson_Clausify".) *) -fun transform_elim_term t = +fun transform_elim_prop t = case Logic.strip_imp_concl t of @{const Trueprop} $ Var (z, @{typ bool}) => subst_Vars [(z, @{const False})] t diff -r 62a14c80d194 -r 9e620869a576 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Sun May 22 14:51:42 2011 +0200 @@ -34,8 +34,9 @@ val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i val facts = Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds - (the_default default_max_relevant max_relevant) is_built_in_const - relevance_fudge relevance_override chained_ths hyp_ts concl_t + (the_default default_max_relevant max_relevant) (K true) + is_built_in_const relevance_fudge relevance_override chained_ths + hyp_ts concl_t val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, facts = map Sledgehammer_Provers.Untranslated_Fact facts, diff -r 62a14c80d194 -r 9e620869a576 src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Sun May 22 14:51:41 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Sun May 22 14:51:42 2011 +0200 @@ -23,7 +23,7 @@ fun facts_of thy = Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty - true [] [] + true (K true) [] [] fun fold_body_thms f = let