# HG changeset patch # User blanchet # Date 1277795137 -7200 # Node ID 295f3a9b44b6cd682b76d81d319c219e26dce46c # Parent b3f572839570d5d789ae39afd80568ce6660da5e move functions not needed by Metis out of "Metis_Clauses" diff -r b3f572839570 -r 295f3a9b44b6 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 18:47:07 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 09:05:37 2010 +0200 @@ -48,6 +48,7 @@ filtered_clauses: ((string * int) * thm) list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result + exception TRIVIAL of unit val kill_atps: unit -> unit val running_atps: unit -> unit @@ -119,6 +120,9 @@ type prover = params -> minimize_command -> Time.time -> problem -> prover_result +(* Trivial problem, which resolution cannot handle (empty clause) *) +exception TRIVIAL of unit + (* named provers *) structure Data = Theory_Data diff -r b3f572839570 -r 295f3a9b44b6 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 28 18:47:07 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 29 09:05:37 2010 +0200 @@ -7,13 +7,10 @@ signature ATP_SYSTEMS = sig - type prover = ATP_Manager.prover - - (* hooks for problem files *) + val trace : bool Unsynchronized.ref val dest_dir : string Config.T val problem_prefix : string Config.T val measure_runtime : bool Config.T - val refresh_systems_on_tptp : unit -> unit val default_atps_param_value : unit -> string val setup : theory -> theory @@ -30,6 +27,9 @@ open Sledgehammer_Proof_Reconstruct open ATP_Manager +val trace = Unsynchronized.ref false +fun trace_msg msg = if !trace then tracing (msg ()) else () + (** generic ATP **) (* external problem files *) @@ -121,6 +121,125 @@ (j :: hd shape) :: tl shape end + +(* Clause preparation *) + +fun make_clause_table xs = + fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty + +(* Remove existing axiom clauses from the conjecture clauses, as this can + dramatically boost an ATP's performance (for some reason). *) +fun subtract_cls ax_clauses = + filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) + +fun is_false_literal (Literal (pos, CombConst ((c, _), _, _))) = + (pos andalso c = "c_False") orelse (not pos andalso c = "c_True") + | is_false_literal _ = false +fun is_true_literal (Literal (pol, CombConst ((c, _), _, _))) = + (pol andalso c = "c_True") orelse + (not pol andalso c = "c_False") + | is_true_literal _ = false; +fun is_tautology (HOLClause {literals,...}) = exists is_true_literal literals + +(* making axiom and conjecture clauses *) +fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes = + let + val (skolem_somes, t) = + th |> prop_of |> conceal_skolem_somes clause_id skolem_somes + val (lits, ctypes_sorts) = literals_of_term thy t + in + if forall is_false_literal lits then + raise TRIVIAL () + else + (skolem_somes, + HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, + kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}) + end + +fun add_axiom_clause thy ((name, k), th) (skolem_somes, clss) = + let + val (skolem_somes, cls) = make_clause thy (k, name, Axiom, th) skolem_somes + in (skolem_somes, clss |> not (is_tautology cls) ? cons (name, cls)) end + +fun make_axiom_clauses thy clauses = + ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd + +fun make_conjecture_clauses thy = + let + fun aux _ _ [] = [] + | aux n skolem_somes (th :: ths) = + let + val (skolem_somes, cls) = + make_clause thy (n, "conjecture", Conjecture, th) skolem_somes + in cls :: aux (n + 1) skolem_somes ths end + in aux 0 [] end + +(** Helper clauses **) + +fun count_combterm (CombConst ((c, _), _, _)) = + Symtab.map_entry c (Integer.add 1) + | count_combterm (CombVar _) = I + | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2 +fun count_literal (Literal (_, t)) = count_combterm t +fun count_clause (HOLClause {literals, ...}) = fold count_literal literals + +fun cnf_helper_thms thy raw = + map (`Thm.get_name_hint) + #> (if raw then map (apfst (rpair 0)) else cnf_rules_pairs thy) + +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}))] +val optional_typed_helpers = + [(["c_True", "c_False"], (true, @{thms True_or_False})), + (["c_If"], (true, @{thms if_True if_False True_or_False}))] +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} + +val init_counters = + Symtab.make (maps (maps (map (rpair 0) o fst)) + [optional_helpers, optional_typed_helpers]) + +fun get_helper_clauses thy is_FO full_types conjectures axcls = + let + val axclauses = map snd (make_axiom_clauses thy axcls) + val ct = fold (fold count_clause) [conjectures, axclauses] init_counters + fun is_needed c = the (Symtab.lookup ct c) > 0 + 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) + in map snd (make_axiom_clauses thy cnfs) end + +(* prepare for passing to writer, + create additional clauses based on the information from extra_cls *) +fun prepare_clauses full_types goal_cls axcls extra_cls thy = + let + val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls + val ccls = subtract_cls extra_cls goal_cls + val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls + val ccltms = map prop_of ccls + and axtms = map (prop_of o snd) extra_cls + val subs = tfree_classes_of_terms ccltms + and supers = tvar_classes_of_terms axtms + and tycons = type_consts_of_terms thy (ccltms @ axtms) + (*TFrees in conjecture clauses; TVars in axiom clauses*) + val conjectures = make_conjecture_clauses thy ccls + 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 = + get_helper_clauses thy is_FO full_types conjectures extra_cls + val (supers', arity_clauses) = make_arity_clauses thy tycons supers + val classrel_clauses = make_classrel_clauses thy subs supers' + in + (Vector.fromList clnames, + (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses)) + end + + (* generic TPTP-based provers *) fun generic_tptp_prover diff -r b3f572839570 -r 295f3a9b44b6 src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jun 28 18:47:07 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 09:05:37 2010 +0200 @@ -33,9 +33,7 @@ datatype hol_clause = HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, literals: literal list, ctypes_sorts: typ list} - exception TRIVIAL of unit - val trace : bool Unsynchronized.ref val type_wrapper_name : string val schematic_var_prefix: string val fixed_var_prefix: string @@ -72,16 +70,9 @@ val literals_of_term : theory -> term -> literal list * typ list val conceal_skolem_somes : int -> (string * term) list -> term -> (string * term) list * term - val is_quasi_fol_theorem : theory -> thm -> bool val tfree_classes_of_terms : term list -> string list val tvar_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list - val prepare_clauses : - bool -> thm list -> ((string * int) * thm) list - -> ((string * int) * thm) list -> theory - -> string vector - * (hol_clause list * hol_clause list * hol_clause list * hol_clause list - * classrel_clause list * arity_clause list) end structure Metis_Clauses : METIS_CLAUSES = @@ -89,9 +80,6 @@ open Clausifier -val trace = Unsynchronized.ref false -fun trace_msg msg = if !trace then tracing (msg ()) else () - val type_wrapper_name = "ti" val schematic_var_prefix = "V_"; @@ -218,9 +206,6 @@ val skolem_prefix = "sko_" val skolem_infix = "$" -(*Keep the full complexity of the original name*) -fun flatten_name s = space_implode "_X" (Long_Name.explode s); - (* Hack: Could return false positives (e.g., a user happens to declare a constant called "SomeTheory.sko_means_shoe_in_$wedish". *) val is_skolem_const_name = @@ -457,17 +442,6 @@ | stripc x = x in stripc(u,[]) end -fun isFalse (Literal (pol, CombConst ((c, _), _, _))) = - (pol andalso c = "c_False") orelse (not pol andalso c = "c_True") - | isFalse _ = false; - -fun isTrue (Literal (pol, CombConst ((c, _), _, _))) = - (pol andalso c = "c_True") orelse - (not pol andalso c = "c_False") - | isTrue _ = false; - -fun isTaut (HOLClause {literals,...}) = exists isTrue literals; - fun type_of (Type (a, Ts)) = let val (folTypes,ts) = types_of Ts in (TyConstr (`make_fixed_type_const a, folTypes), ts) @@ -511,7 +485,7 @@ let val (P', tsP) = combterm_of thy P val (Q', tsQ) = combterm_of thy Q in (CombApp (P', Q'), union (op =) tsP tsQ) end - | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs" + | combterm_of _ (Abs _) = raise Fail "HOL clause: Abs" fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos) @@ -562,85 +536,6 @@ else (skolem_somes, t) -fun is_quasi_fol_theorem thy = - Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of - -(* Trivial problem, which resolution cannot handle (empty clause) *) -exception TRIVIAL of unit - -(* making axiom and conjecture clauses *) -fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes = - let - val (skolem_somes, t) = - th |> prop_of |> conceal_skolem_somes clause_id skolem_somes - val (lits, ctypes_sorts) = literals_of_term thy t - in - if forall isFalse lits then - raise TRIVIAL () - else - (skolem_somes, - HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, - kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}) - end - -fun add_axiom_clause thy ((name, k), th) (skolem_somes, clss) = - let - val (skolem_somes, cls) = make_clause thy (k, name, Axiom, th) skolem_somes - in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end - -fun make_axiom_clauses thy clauses = - ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd - -fun make_conjecture_clauses thy = - let - fun aux _ _ [] = [] - | aux n skolem_somes (th :: ths) = - let - val (skolem_somes, cls) = - make_clause thy (n, "conjecture", Conjecture, th) skolem_somes - in cls :: aux (n + 1) skolem_somes ths end - in aux 0 [] end - -(** Helper clauses **) - -fun count_combterm (CombConst ((c, _), _, _)) = - Symtab.map_entry c (Integer.add 1) - | count_combterm (CombVar _) = I - | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2 -fun count_literal (Literal (_, t)) = count_combterm t -fun count_clause (HOLClause {literals, ...}) = fold count_literal literals - -fun cnf_helper_thms thy raw = - map (`Thm.get_name_hint) - #> (if raw then map (apfst (rpair 0)) else cnf_rules_pairs thy) - -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}))] -val optional_typed_helpers = - [(["c_True", "c_False"], (true, @{thms True_or_False})), - (["c_If"], (true, @{thms if_True if_False True_or_False}))] -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} - -val init_counters = - Symtab.make (maps (maps (map (rpair 0) o fst)) - [optional_helpers, optional_typed_helpers]) - -fun get_helper_clauses thy is_FO full_types conjectures axcls = - let - val axclauses = map snd (make_axiom_clauses thy axcls) - val ct = fold (fold count_clause) [conjectures, axclauses] init_counters - fun is_needed c = the (Symtab.lookup ct c) > 0 - 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) - in map snd (make_axiom_clauses thy cnfs) end - (***************************************************************) (* Type Classes Present in the Axiom or Conjecture Clauses *) @@ -679,37 +574,4 @@ fun type_consts_of_terms thy ts = Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); -fun make_clause_table xs = - fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty - -(* Remove existing axiom clauses from the conjecture clauses, as this can - dramatically boost an ATP's performance (for some reason). *) -fun subtract_cls ax_clauses = - filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) - -(* prepare for passing to writer, - create additional clauses based on the information from extra_cls *) -fun prepare_clauses full_types goal_cls axcls extra_cls thy = - let - val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls - val ccls = subtract_cls extra_cls goal_cls - val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls - val ccltms = map prop_of ccls - and axtms = map (prop_of o snd) extra_cls - val subs = tfree_classes_of_terms ccltms - and supers = tvar_classes_of_terms axtms - and tycons = type_consts_of_terms thy (ccltms @ axtms) - (*TFrees in conjecture clauses; TVars in axiom clauses*) - val conjectures = make_conjecture_clauses thy ccls - 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 = - get_helper_clauses thy is_FO full_types conjectures extra_cls - val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val classrel_clauses = make_classrel_clauses thy subs supers' - in - (Vector.fromList clnames, - (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses)) - end - end; diff -r b3f572839570 -r 295f3a9b44b6 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 28 18:47:07 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 09:05:37 2010 +0200 @@ -670,13 +670,16 @@ ("c_False", (true, @{thms True_or_False})), ("c_If", (true, @{thms if_True if_False True_or_False}))] +fun is_quasi_fol_clause thy = + Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of + (* Function to generate metis clauses, including comb and type clauses *) fun build_map mode0 ctxt cls ths = let val thy = ProofContext.theory_of ctxt (*The modes FO and FT are sticky. HO can be downgraded to FO.*) fun set_mode FO = FO | set_mode HO = - if forall (is_quasi_fol_theorem thy) (cls @ ths) then FO else HO + if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO | set_mode FT = FT val mode = set_mode mode0 (*transform isabelle clause to metis clause *)