# HG changeset patch # User blanchet # Date 1332345204 -3600 # Node ID c73f7b0c7ebcb45d9422d448fa3c25ea84aa4669 # Parent 777549486d4421e8155864b4c0dbd3cbcfb35adc generate weights and precedences for predicates as well diff -r 777549486d44 -r c73f7b0c7ebc src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Mar 21 15:43:02 2012 +0000 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Mar 21 16:53:24 2012 +0100 @@ -85,6 +85,7 @@ val extract_isabelle_status : (string, 'a) ho_term list -> string option val extract_isabelle_rank : (string, 'a) ho_term list -> int val introN : string + val spec_introN : string val elimN : string val simpN : string val spec_eqN : string @@ -217,6 +218,7 @@ val isabelle_info_prefix = "isabelle_" val introN = "intro" +val spec_introN = "spec_intro" val elimN = "elim" val simpN = "simp" val spec_eqN = "spec_eq" @@ -551,8 +553,8 @@ (if gen_weights then ord_info else []) |> map spair |> commas |> maybe_enclose "weights [" "]." val syms = - [func_aries] @ (if sorted then [do_term_order_weights ()] else []) @ - [pred_aries] @ (if sorted then [sorts ()] else []) + [func_aries, pred_aries] @ + (if sorted then [do_term_order_weights (), sorts ()] else []) fun func_sigs () = filt (fn Decl (_, sym, ty) => if is_function_type ty then SOME (fun_typ sym ty) else NONE diff -r 777549486d44 -r c73f7b0c7ebc src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Mar 21 15:43:02 2012 +0000 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Mar 21 16:53:24 2012 +0100 @@ -16,7 +16,8 @@ type 'a problem = 'a ATP_Problem.problem datatype scope = Global | Local | Assum | Chained - datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq + datatype status = + General | Induct | Intro | Spec_Intro | Elim | Simp | Spec_Eq type stature = scope * status datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic @@ -547,7 +548,7 @@ in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end datatype scope = Global | Local | Assum | Chained -datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq +datatype status = General | Induct | Intro | Spec_Intro | Elim | Simp | Spec_Eq type stature = scope * status datatype order = First_Order | Higher_Order @@ -1413,7 +1414,11 @@ {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false}) -datatype app_op_level = Incomplete_Apply | Sufficient_Apply | Full_Apply +datatype app_op_level = + Min_App_Op | + Sufficient_App_Op | + Sufficient_App_Op_And_Predicator | + Full_App_Op_And_Predicator fun sym_table_for_facts ctxt type_enc app_op_level conjs facts = let @@ -1428,10 +1433,14 @@ iter (ary + 1) (range_type T) in iter 0 const_T end fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) = - if app_op_level = Sufficient_Apply andalso - (can dest_funT T orelse T = @{typ bool}) then + if (app_op_level = Sufficient_App_Op andalso can dest_funT T) orelse + (app_op_level = Sufficient_App_Op_And_Predicator andalso + (can dest_funT T orelse T = @{typ bool})) then let - val bool_vars' = bool_vars orelse body_type T = @{typ bool} + val bool_vars' = + bool_vars orelse + (app_op_level = Sufficient_App_Op_And_Predicator andalso + body_type T = @{typ bool}) fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} = {pred_sym = pred_sym andalso not bool_vars', min_ary = fold (fn T' => consider_var_ary T' T) types min_ary, @@ -1468,8 +1477,9 @@ val types' = types |> insert_type ctxt I T val in_conj = in_conj orelse conj_fact val min_ary = - if app_op_level = Sufficient_Apply andalso - not (pointer_eq (types', types)) then + if (app_op_level = Sufficient_App_Op orelse + app_op_level = Sufficient_App_Op_And_Predicator) + andalso not (pointer_eq (types', types)) then fold (consider_var_ary T) fun_var_Ts min_ary else min_ary @@ -1496,10 +1506,9 @@ | NONE => ary val min_ary = case app_op_level of - Incomplete_Apply => ary - | Sufficient_Apply => - fold (consider_var_ary T) fun_var_Ts ary - | Full_Apply => 0 + Min_App_Op => ary + | Full_App_Op_And_Predicator => 0 + | _ => fold (consider_var_ary T) fun_var_Ts ary in Symtab.update_new (s, {pred_sym = pred_sym, min_ary = min_ary, @@ -1984,6 +1993,7 @@ let val rank = rank j in case snd stature of Intro => isabelle_info introN rank + | Spec_Intro => isabelle_info spec_introN rank | Elim => isabelle_info elimN rank | Simp => isabelle_info simpN rank | Spec_Eq => isabelle_info spec_eqN rank @@ -2000,7 +2010,7 @@ type_class_formula type_enc superclass ty_arg]) |> mk_aquant AForall [(tvar_a_name, atype_of_type_vars type_enc)], - NONE, isabelle_info introN helper_rank) + NONE, isabelle_info spec_introN helper_rank) end fun formula_from_arity_atom type_enc (class, t, args) = @@ -2014,7 +2024,7 @@ (formula_from_arity_atom type_enc concl_atom) |> mk_aquant AForall (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)), - NONE, isabelle_info introN helper_rank) + NONE, isabelle_info spec_introN helper_rank) fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = @@ -2223,7 +2233,7 @@ always_guard_var_in_formula (SOME true) |> close_formula_universally |> bound_tvars type_enc true (atomic_types_of T), - NONE, isabelle_info introN helper_rank) + NONE, isabelle_info spec_introN helper_rank) fun formula_line_for_tags_mono_type ctxt format mono type_enc T = let val x_var = ATerm (`make_bound_var "X", []) in @@ -2303,7 +2313,7 @@ |> close_formula_universally |> bound_tvars type_enc (n > 1) (atomic_types_of T) |> maybe_negate, - NONE, isabelle_info introN helper_rank) + NONE, isabelle_info spec_introN helper_rank) end fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s @@ -2552,7 +2562,7 @@ |> List.partition is_poly_constr |> pairself (map fst) -val app_op_threshold = 50 +val app_op_and_predicator_threshold = 50 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter lam_trans uncurried_aliases readable_names preproc @@ -2565,11 +2575,13 @@ ruin everything. Hence we do it only if there are few facts (which is normally the case for "metis" and the minimizer). *) val app_op_level = - if polymorphism_of_type_enc type_enc = Polymorphic andalso - length facts >= app_op_threshold then - Incomplete_Apply + if length facts > app_op_and_predicator_threshold then + if polymorphism_of_type_enc type_enc = Polymorphic then + Min_App_Op + else + Sufficient_App_Op else - Sufficient_Apply + Sufficient_App_Op_And_Predicator val lam_trans = if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then @@ -2590,7 +2602,7 @@ firstorderize_fact thy monom_constrs format type_enc sym_tab0 (uncurried_aliases andalso not in_helper) val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false)) - val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts + val sym_tab = sym_table_for_facts ctxt type_enc Min_App_Op conjs facts val helpers = sym_tab |> helper_facts_for_sym_table ctxt format type_enc |> map (firstorderize true) @@ -2693,14 +2705,34 @@ |> sort (prod_ord Real.compare string_ord o pairself swap) end -fun make_head_roll (ATerm (s, args)) = - (* ugly hack: may make innocent victims (collateral damage) *) - if String.isPrefix app_op_name s andalso length args = 2 then - make_head_roll (hd args) ||> append (tl args) - else - (s, args) +(* Ugly hack: may make innocent victims (collateral damage) *) +fun may_be_app s args = String.isPrefix app_op_name s andalso length args = 2 +fun may_be_predicator s = + member (op =) [predicator_name, prefixed_predicator_name] s + +fun strip_predicator (tm as ATerm (s, [tm'])) = + if may_be_predicator s then tm' else tm + | strip_predicator tm = tm + +fun make_head_roll (ATerm (s, tms)) = + if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms) + else (s, tms) | make_head_roll _ = ("", []) +fun strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi + | strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis + | strip_up_to_predicator (AAtom tm) = [strip_predicator tm] + +fun strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi + | strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) = + strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1) + | strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi)) + +fun strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi + | strip_iff_etc (AConn (AIff, [phi1, phi2])) = + pairself strip_up_to_predicator (phi1, phi2) + | strip_iff_etc _ = ([], []) + val max_term_order_weight = 2147483647 fun atp_problem_term_order_info problem = @@ -2710,31 +2742,50 @@ #> Graph.default_node (s', ()) #> Graph.add_edge_acyclic (s, s') fun add_term_deps head (ATerm (s, args)) = - is_tptp_user_symbol s ? perhaps (try (add_edge s head)) - #> fold (add_term_deps head) args + if is_tptp_user_symbol head then + (if is_tptp_user_symbol s then perhaps (try (add_edge s head)) else I) + #> fold (add_term_deps head) args + else + I | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm - fun add_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) = + fun add_intro_deps pred (Formula (_, role, phi, _, info)) = + if pred (role, info) then + let val (hyps, concl) = strip_ahorn_etc phi in + case make_head_roll concl of + (head, args as _ :: _) => fold (add_term_deps head) (hyps @ args) + | _ => I + end + else + I + | add_intro_deps _ _ = I + fun add_atom_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) = if is_tptp_equal s then case make_head_roll lhs of - (head, rest as _ :: _) => - is_tptp_user_symbol head ? fold (add_term_deps head) (rhs :: rest) + (head, args as _ :: _) => fold (add_term_deps head) (rhs :: args) | _ => I else I - | add_eq_deps _ _ = I - fun add_deps pred (Formula (_, role, phi, _, info)) = + | add_atom_eq_deps _ _ = I + fun add_eq_deps pred (Formula (_, role, phi, _, info)) = if pred (role, info) then - formula_fold (SOME (role <> Conjecture)) add_eq_deps phi + case strip_iff_etc phi of + ([lhs], rhs) => + (case make_head_roll lhs of + (head, args as _ :: _) => fold (add_term_deps head) (rhs @ args) + | _ => I) + | _ => formula_fold (SOME (role <> Conjecture)) add_atom_eq_deps phi else I - | add_deps _ _ = I + | add_eq_deps _ _ = I fun has_status status (_, info) = extract_isabelle_status info = SOME status fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis) val graph = Graph.empty - |> fold (fold (add_deps (has_status spec_eqN)) o snd) problem - |> fold (fold (add_deps (has_status simpN orf is_conj)) o snd) problem + |> fold (fold (add_eq_deps (has_status spec_eqN)) o snd) problem + |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem + |> fold (fold (add_intro_deps (has_status spec_introN)) o snd) problem + |> fold (fold (add_intro_deps (has_status introN)) o snd) problem fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1 fun add_weights _ [] = I | add_weights weight syms = diff -r 777549486d44 -r c73f7b0c7ebc src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Mar 21 15:43:02 2012 +0000 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Mar 21 16:53:24 2012 +0100 @@ -169,7 +169,7 @@ val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false) val smartN = "smart" -val kboN = "kbo" +(* val kboN = "kbo" *) val lpoN = "lpo" val xweightsN = "_weights" val xprecN = "_prec" @@ -666,7 +666,7 @@ if ord = smartN then if atp = spass_newN orelse (atp = spassN andalso is_new_spass_version ()) then - {is_lpo = false, gen_weights = true, gen_prec = false, gen_simp = true} + {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false} else {is_lpo = false, gen_weights = false, gen_prec = false, gen_simp = false} diff -r 777549486d44 -r c73f7b0c7ebc src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Mar 21 15:43:02 2012 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Mar 21 16:53:24 2012 +0100 @@ -128,31 +128,32 @@ fold (fn normalize => Termtab.update (normalize t, stature)) (I :: normalizers) end) -(* - TODO: "intro" and "elim" rules are not exploited yet by SPASS (or any other - prover). Reintroduce this code when it becomes useful. It costs about 50 ms - per Sledgehammer invocation. - - val {safeIs, safeEs, hazIs, hazEs, ...} = + val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = ctxt |> claset_of |> Classical.rep_cs val intros = Item_Net.content safeIs @ Item_Net.content hazIs +(* Add once it is used: val elims = Item_Net.content safeEs @ Item_Net.content hazEs |> map Classical.classical_rule *) val simps = ctxt |> simpset_of |> dest_ss |> #simps + val specs = ctxt |> Spec_Rules.get val spec_eqs = - ctxt |> Spec_Rules.get - |> filter (curry (op =) Spec_Rules.Equational o fst) - |> maps (snd o snd) - |> filter_out (member Thm.eq_thm_prop risky_spec_eqs) + specs |> filter (curry (op =) Spec_Rules.Equational o fst) + |> maps (snd o snd) + |> filter_out (member Thm.eq_thm_prop risky_spec_eqs) + val spec_intros = + specs |> filter (member (op =) [Spec_Rules.Inductive, + Spec_Rules.Co_Inductive] o fst) + |> maps (snd o snd) in Termtab.empty |> add Simp [atomize] snd simps |> add Spec_Eq [] I spec_eqs -(* +(* Add once it is used: |> add Elim [] I elims +*) |> add Intro [] I intros -*) + |> add Spec_Intro [] I spec_intros end fun needs_quoting reserved s =