# HG changeset patch # User blanchet # Date 1280175743 -7200 # Node ID 31705eccee23136b9fdafb86c167a20919d2329a # Parent a9b47b85ca24aca90f2bcc6977f5c089b18541b9 get rid of obsolete "axiom ID" component, since it's now always 0 diff -r a9b47b85ca24 -r 31705eccee23 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jul 26 20:07:31 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jul 26 22:22:23 2010 +0200 @@ -29,8 +29,8 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: ((string * int) * thm) list option, - filtered_clauses: ((string * int) * thm) list option} + axiom_clauses: (string * thm) list option, + filtered_clauses: (string * thm) list option} datatype failure = Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError @@ -44,7 +44,7 @@ proof: string, internal_thm_names: string Vector.vector, conjecture_shape: int list, - filtered_clauses: ((string * int) * thm) list} + filtered_clauses: (string * thm) list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result @@ -96,8 +96,8 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: ((string * int) * thm) list option, - filtered_clauses: ((string * int) * thm) list option} + axiom_clauses: (string * thm) list option, + filtered_clauses: (string * thm) list option} datatype failure = Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | @@ -113,7 +113,7 @@ proof: string, internal_thm_names: string Vector.vector, conjecture_shape: int list, - filtered_clauses: ((string * int) * thm) list} + filtered_clauses: (string * thm) list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result diff -r a9b47b85ca24 -r 31705eccee23 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 20:07:31 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 22:22:23 2010 +0200 @@ -220,8 +220,8 @@ (* making axiom and conjecture clauses *) fun make_clause thy (formula_id, formula_name, kind, t) = let - (* ### FIXME: introduce combinators and perform other transformations - previously done by Clausifier.to_nnf *) + (* ### FIXME: perform other transformations previously done by + "Clausifier.to_nnf", e.g. "HOL.If" *) val t = t |> transform_elim_term |> Object_Logic.atomize_term thy |> extensionalize_term @@ -233,8 +233,8 @@ ctypes_sorts = ctypes_sorts} end -fun add_axiom_clause thy ((name, k), th) = - cons (name, make_clause thy (k, name, Axiom, prop_of th)) +fun add_axiom_clause thy (name, th) = + cons (name, make_clause thy (0, name, Axiom, prop_of th)) fun make_axiom_clauses thy clauses = fold_rev (add_axiom_clause thy) clauses [] @@ -254,17 +254,13 @@ fun count_fol_formula (FOLFormula {combformula, ...}) = count_combformula combformula -fun cnf_helper_thms thy raw = - map (`Thm.get_name_hint) - #> (if raw then map (apfst (rpair 0)) else Clausifier.cnf_rules_pairs thy true) - val optional_helpers = - [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})), - (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})), - (["c_COMBS"], (false, @{thms COMBS_def}))] + [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}), + (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}), + (["c_COMBS"], @{thms COMBS_def})] val optional_typed_helpers = - [(["c_True", "c_False"], (true, @{thms True_or_False})), - (["c_If"], (true, @{thms if_True if_False True_or_False}))] + [(["c_True", "c_False"], @{thms True_or_False}), + (["c_If"], @{thms if_True if_False True_or_False})] val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} val init_counters = @@ -280,14 +276,14 @@ val cnfs = (optional_helpers |> full_types ? append optional_typed_helpers - |> maps (fn (ss, (raw, ths)) => - if exists is_needed ss then cnf_helper_thms thy raw ths - else [])) - @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers) + |> maps (fn (ss, ths) => + if exists is_needed ss then map (`Thm.get_name_hint) ths + else [])) @ + (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) in map snd (make_axiom_clauses thy cnfs) end -fun negate_term (@{const Not} $ t) = t - | negate_term t = @{const Not} $ t +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 *) @@ -300,9 +296,8 @@ 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) - (*TFrees in conjecture clauses; TVars in axiom clauses*) - val conjectures = - make_conjecture_clauses thy (map negate_term hyp_ts @ [concl_t]) + (* TFrees in conjecture clauses; TVars in axiom clauses *) + val conjectures = make_conjecture_clauses thy (map s_not hyp_ts @ [concl_t]) val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls) val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls) val helper_clauses = @@ -384,7 +379,6 @@ relevance_convergence defs_relevant max_axiom_clauses (the_default prefers_theory_relevant theory_relevant) relevance_override goal hyp_ts concl_t - |> Clausifier.cnf_rules_pairs thy true val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses val (internal_thm_names, clauses) = prepare_clauses full_types hyp_ts concl_t the_axiom_clauses diff -r a9b47b85ca24 -r 31705eccee23 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jul 26 20:07:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jul 26 22:22:23 2010 +0200 @@ -55,13 +55,12 @@ val _ = priority ("Testing " ^ string_of_int num_theorems ^ " theorem" ^ plural_s num_theorems ^ "...") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs - val axclauses = Clausifier.cnf_rules_pairs thy true name_thm_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = {subgoal = subgoal, goal = (ctxt, (facts, goal)), relevance_override = {add = [], del = [], only = false}, - axiom_clauses = SOME axclauses, - filtered_clauses = SOME (the_default axclauses filtered_clauses)} + axiom_clauses = SOME name_thm_pairs, + filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)} in prover params (K "") timeout problem |> tap (fn result : prover_result =>