# HG changeset patch # User blanchet # Date 1280407183 -7200 # Node ID c4b57f68ddb3ff6f1e2dfd135ffc7cd726f43505 # Parent 81ead4aaba2d3876309803086737e39584b093a0 remove the "extra_clauses" business introduced in 19a5f1c8a844; it isn't working reliably because of: * relevance_override * it is ignored anyway by TPTP generator A better solution would/will be to ensure monotonicity: extra axioms not used in an ATP proof shouldn't make the rest of the problem provable diff -r 81ead4aaba2d -r c4b57f68ddb3 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 12:07:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:39:43 2010 +0200 @@ -30,8 +30,7 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (string * thm) list option, - filtered_clauses: (string * thm) list option} + axiom_clauses: (string * thm) list option} type prover_result = {outcome: failure option, message: string, @@ -41,8 +40,7 @@ output: string, proof: string, internal_thm_names: string Vector.vector, - conjecture_shape: int list list, - filtered_clauses: (string * thm) list} + conjecture_shape: int list list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result @@ -100,8 +98,7 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (string * thm) list option, - filtered_clauses: (string * thm) list option} + axiom_clauses: (string * thm) list option} type prover_result = {outcome: failure option, @@ -112,8 +109,7 @@ output: string, proof: string, internal_thm_names: string Vector.vector, - conjecture_shape: int list list, - filtered_clauses: (string * thm) list} + conjecture_shape: int list list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result @@ -345,14 +341,12 @@ fun s_not (@{const Not} $ t) = t | s_not t = @{const Not} $ t -(* prepare for passing to writer, - create additional clauses based on the information from extra_cls *) -fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls = +fun prepare_clauses ctxt full_types hyp_ts concl_t axcls = let val thy = ProofContext.theory_of ctxt val goal_t = Logic.list_implies (hyp_ts, concl_t) val is_FO = Meson.is_fol_term thy goal_t - val axtms = map (prop_of o snd) extra_cls + val axtms = map (prop_of o snd) axcls val subs = tfree_classes_of_terms [goal_t] val supers = tvar_classes_of_terms axtms val tycons = type_consts_of_terms thy (goal_t :: axtms) @@ -361,19 +355,16 @@ map (s_not o HOLogic.dest_Trueprop) hyp_ts @ [HOLogic.dest_Trueprop concl_t] |> make_conjecture_clauses ctxt - val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls val (clnames, axiom_clauses) = ListPair.unzip (map (make_axiom_clause ctxt) axcls) - (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the - "get_helper_clauses" call? *) val helper_clauses = - get_helper_clauses ctxt is_FO full_types conjectures extra_clauses + get_helper_clauses ctxt is_FO full_types conjectures axiom_clauses val (supers', arity_clauses) = make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' in (Vector.fromList clnames, - (conjectures, axiom_clauses, extra_clauses, helper_clauses, - class_rel_clauses, arity_clauses)) + (conjectures, axiom_clauses, helper_clauses, class_rel_clauses, + arity_clauses)) end fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) @@ -596,8 +587,8 @@ (const_table_for_problem explicit_apply problem) problem fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply - file (conjectures, axiom_clauses, extra_clauses, - helper_clauses, class_rel_clauses, arity_clauses) = + file (conjectures, axiom_clauses, helper_clauses, + class_rel_clauses, arity_clauses) = let val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses val class_rel_lines = @@ -684,26 +675,23 @@ relevance_convergence, theory_relevant, defs_relevant, isar_proof, isar_shrink_factor, ...} : params) minimize_command timeout - ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} - : problem) = + ({subgoal, goal, relevance_override, axiom_clauses} : problem) = let (* get clauses and prepare them for writing *) val (ctxt, (_, th)) = goal; val thy = ProofContext.theory_of ctxt (* ### FIXME: (1) preprocessing for "if" etc. *) val (params, hyp_ts, concl_t) = strip_subgoal th subgoal - val the_filtered_clauses = - case filtered_clauses of - SOME fcls => fcls + val the_axiom_clauses = + case axiom_clauses of + SOME axioms => axioms | NONE => relevant_facts full_types relevance_threshold relevance_convergence defs_relevant max_new_relevant_facts_per_iter (the_default prefers_theory_relevant theory_relevant) relevance_override goal hyp_ts concl_t - val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses val (internal_thm_names, clauses) = prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses - the_filtered_clauses (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" @@ -814,8 +802,7 @@ {outcome = outcome, message = message, pool = pool, used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, output = output, proof = proof, internal_thm_names = internal_thm_names, - conjecture_shape = conjecture_shape, - filtered_clauses = the_filtered_clauses} + conjecture_shape = conjecture_shape} end fun get_prover_fun thy name = prover_fun name (get_prover thy name) @@ -837,8 +824,7 @@ let val problem = {subgoal = i, goal = (ctxt, (facts, goal)), - relevance_override = relevance_override, axiom_clauses = NONE, - filtered_clauses = NONE} + relevance_override = relevance_override, axiom_clauses = NONE} in prover params (minimize_command name) timeout problem |> #message handle ERROR message => "Error: " ^ message ^ "\n" diff -r 81ead4aaba2d -r c4b57f68ddb3 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 12:07:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 14:39:43 2010 +0200 @@ -18,7 +18,6 @@ structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER = struct -open Metis_Clauses open Sledgehammer_Util open Sledgehammer_Fact_Filter open Sledgehammer_Proof_Reconstruct @@ -37,7 +36,7 @@ | string_for_outcome (SOME failure) = string_for_failure failure fun sledgehammer_test_theorems (params : params) prover timeout subgoal state - filtered_clauses name_thms_pairs = + name_thms_pairs = let val num_theorems = length name_thms_pairs val _ = @@ -54,8 +53,7 @@ val problem = {subgoal = subgoal, goal = (ctxt, (facts, goal)), relevance_override = {add = [], del = [], only = false}, - axiom_clauses = SOME name_thm_pairs, - filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)} + axiom_clauses = SOME name_thm_pairs} in prover params (K "") timeout problem |> tap (fn result : prover_result => @@ -91,15 +89,14 @@ sledgehammer_test_theorems params prover minimize_timeout i state val {context = ctxt, goal, ...} = Proof.goal state; in - (* try prove first to check result and get used theorems *) - (case test_facts NONE name_thms_pairs of - result as {outcome = NONE, pool, proof, used_thm_names, - conjecture_shape, filtered_clauses, ...} => + (* FIXME: merge both "test_facts" calls *) + (case test_facts name_thms_pairs of + result as {outcome = NONE, pool, used_thm_names, + conjecture_shape, ...} => let val (min_thms, {proof, internal_thm_names, ...}) = - sublinear_minimize (test_facts (SOME filtered_clauses)) - (filter_used_facts used_thm_names name_thms_pairs) - ([], result) + sublinear_minimize test_facts + (filter_used_facts used_thm_names name_thms_pairs) ([], result) val m = length min_thms val _ = priority (cat_lines ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")