# HG changeset patch # User blanchet # Date 1340702080 -7200 # Node ID 0186df5074c8b3f4ea7d8defd851582750454610 # Parent efaff8206967d45c30aa13ce7cca988ca2d6b322 renamed experimental option diff -r efaff8206967 -r 0186df5074c8 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Tue Jun 26 11:14:40 2012 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Tue Jun 26 11:14:40 2012 +0200 @@ -183,19 +183,19 @@ in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end end -fun atp_tac ctxt aggressivity override_params timeout prover = +fun atp_tac ctxt completeness override_params timeout prover = let val ctxt = - ctxt |> Config.put Sledgehammer_Provers.aggressive (aggressivity > 0) + ctxt |> Config.put Sledgehammer_Provers.completish (completeness > 0) in Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt ([("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("provers", prover), ("timeout", string_of_int timeout)] @ - (if aggressivity > 0 then + (if completeness > 0 then [("type_enc", - if aggressivity = 1 then "mono_native" else "poly_guards??"), + if completeness = 1 then "mono_native" else "poly_guards??"), ("slicing", "false")] else []) @ @@ -207,12 +207,12 @@ fun sledgehammer_tac demo ctxt timeout i = let val frac = if demo then 16 else 12 - fun slice mult aggressivity prover = + fun slice mult completeness prover = SOLVE_TIMEOUT (mult * timeout div frac) (prover ^ - (if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")" + (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else "")) - (atp_tac ctxt aggressivity [] (mult * timeout div frac) prover i) + (atp_tac ctxt completeness [] (mult * timeout div frac) prover i) in slice 2 0 ATP_Systems.spassN ORELSE slice 2 0 ATP_Systems.vampireN @@ -290,13 +290,13 @@ val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy) file_name val conj = make_conj assms conjs - val (last_hope_atp, last_hope_aggressive) = + val (last_hope_atp, last_hope_completeness) = if demo then (ATP_Systems.satallaxN, 0) else (ATP_Systems.vampireN, 2) in (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)") - (atp_tac ctxt last_hope_aggressive [] timeout last_hope_atp 1)) conj) + (atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj) |> print_szs_from_success conjs end diff -r efaff8206967 -r 0186df5074c8 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200 @@ -492,11 +492,14 @@ fun string_of_arity (0, n) = string_of_int n | string_of_arity (m, n) = string_of_int m ^ "+" ^ string_of_int n +val dfg_class_inter = space_implode " & " + fun dfg_string_for_formula poly gen_simp info = let val str_for_typ = string_for_type (DFG poly) fun str_for_bound_typ (ty, []) = str_for_typ ty - | str_for_bound_typ (ty, cls) = str_for_typ ty ^ " : " ^ commas cls + | str_for_bound_typ (ty, cls) = + str_for_typ ty ^ " : " ^ dfg_class_inter cls fun suffix_tag top_level s = if top_level then case extract_isabelle_status info of @@ -554,7 +557,7 @@ |>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"]) in "predicate(" ^ commas (sym :: ty_vars @ map str_for_typ tys) ^ ")." end fun str_for_bound_tvar (ty, []) = ty - | str_for_bound_tvar (ty, cls) = ty ^ " : " ^ commas cls + | str_for_bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls fun sort_decl xs ty cl = "sort(" ^ (if null xs then "" diff -r efaff8206967 -r 0186df5074c8 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200 @@ -15,7 +15,7 @@ type formula_role = ATP_Problem.formula_role type 'a problem = 'a ATP_Problem.problem - datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter + datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter datatype scope = Global | Local | Assum | Chained datatype status = @@ -116,7 +116,7 @@ open ATP_Util open ATP_Problem -datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter +datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter datatype scope = Global | Local | Assum | Chained datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def @@ -1594,8 +1594,8 @@ val predicator_iconst = IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, []) -fun predicatify aggressive tm = - if aggressive then +fun predicatify completish tm = + if completish then IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm), fTrue_iconst) else @@ -1615,7 +1615,7 @@ in list_app app [head, arg] end fun firstorderize_fact thy constrs type_enc sym_tab uncurried_aliases - aggressive = + completish = let fun do_app arg head = mk_app_op type_enc head arg fun list_app_ops head args = fold do_app args head @@ -1637,8 +1637,8 @@ fun introduce_predicators tm = case strip_iterm_comb tm of (IConst ((s, _), _, _), _) => - if is_pred_sym sym_tab s then tm else predicatify aggressive tm - | _ => predicatify aggressive tm + if is_pred_sym sym_tab s then tm else predicatify completish tm + | _ => predicatify completish tm val do_iterm = not (is_type_enc_higher_order type_enc) ? (introduce_app_ops #> introduce_predicators) @@ -1699,7 +1699,7 @@ [(General, @{lemma "~ P x | fEx P" by (auto simp: fEx_def)})])] |> map (apsnd (map (apsnd zero_var_indexes))) -val aggressive_helper_table = +val completish_helper_table = base_helper_table @ [((predicator_name, true), @{thms True_or_False fTrue_ne_fFalse} |> map (pair General)), @@ -1761,7 +1761,7 @@ could_specialize_helpers type_enc andalso not (null (Term.hidden_polymorphism t)) -fun add_helper_facts_for_sym ctxt format type_enc aggressive +fun add_helper_facts_for_sym ctxt format type_enc completish (s, {types, ...} : sym_info) = case unprefix_and_unascii const_prefix s of SOME mangled_s => @@ -1794,18 +1794,18 @@ fold (fn ((helper_s, needs_sound), ths) => if (needs_sound andalso not sound) orelse (helper_s <> unmangled_s andalso - (not aggressive orelse could_specialize)) then + (not completish orelse could_specialize)) then I else ths ~~ (1 upto length ths) |> maps (dub_and_inst needs_sound o apfst (apsnd prop_of)) |> make_facts |> union (op = o pairself #iformula)) - (if aggressive then aggressive_helper_table else helper_table) + (if completish then completish_helper_table else helper_table) end | NONE => I -fun helper_facts_for_sym_table ctxt format type_enc aggressive sym_tab = - Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc aggressive) +fun helper_facts_for_sym_table ctxt format type_enc completish sym_tab = + Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc completish) sym_tab [] (***************************************************************) @@ -2253,13 +2253,13 @@ end (* We add "bool" in case the helper "True_or_False" is included later. *) -fun default_mono level aggressive = +fun default_mono level completish = {maybe_finite_Ts = [@{typ bool}], surely_infinite_Ts = case level of Nonmono_Types (Strict, _) => [] | _ => known_infinite_types, - maybe_nonmono_Ts = [if aggressive then tvar_a else @{typ bool}]} + maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]} (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it out with monotonicity" paper presented at CADE 2011. *) @@ -2291,9 +2291,9 @@ fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) = formula_fold (SOME (role <> Conjecture)) (add_iterm_mononotonicity_info ctxt level) iformula -fun mononotonicity_info_for_facts ctxt type_enc aggressive facts = +fun mononotonicity_info_for_facts ctxt type_enc completish facts = let val level = level_of_type_enc type_enc in - default_mono level aggressive + default_mono level completish |> is_type_level_monotonicity_based level ? fold (add_fact_mononotonicity_info ctxt level) facts end @@ -2655,7 +2655,7 @@ 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 mode = Sledgehammer_Aggressive then + if mode = Sledgehammer_Completish then Full_App_Op_And_Predicator else if length facts + length hyp_ts > app_op_and_predicator_threshold then @@ -2664,7 +2664,7 @@ else Sufficient_App_Op_And_Predicator val exporter = (mode = Exporter) - val aggressive = (mode = Sledgehammer_Aggressive) + val completish = (mode = Sledgehammer_Completish) val lam_trans = if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then @@ -2678,11 +2678,11 @@ val (_, sym_tab0) = sym_table_for_facts ctxt type_enc app_op_level conjs facts val mono = - conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc aggressive + conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc completish val constrs = all_constrs_of_polymorphic_datatypes thy fun firstorderize in_helper = firstorderize_fact thy constrs type_enc sym_tab0 - (uncurried_aliases andalso not in_helper) aggressive + (uncurried_aliases andalso not in_helper) completish val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false)) val (ho_stuff, sym_tab) = sym_table_for_facts ctxt type_enc Min_App_Op conjs facts @@ -2694,7 +2694,7 @@ |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false) uncurried_alias_eq_tms val helpers = - sym_tab |> helper_facts_for_sym_table ctxt format type_enc aggressive + sym_tab |> helper_facts_for_sym_table ctxt format type_enc completish |> map (firstorderize true) val mono_Ts = helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc diff -r efaff8206967 -r 0186df5074c8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:40 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:40 2012 +0200 @@ -65,7 +65,7 @@ val dest_dir : string Config.T val problem_prefix : string Config.T - val aggressive : bool Config.T + val completish : bool Config.T val atp_full_names : bool Config.T val smt_triggers : bool Config.T val smt_weights : bool Config.T @@ -335,8 +335,8 @@ Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "") val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob") -val aggressive = - Attrib.setup_config_bool @{binding sledgehammer_aggressive} (K false) +val completish = + Attrib.setup_config_bool @{binding sledgehammer_completish} (K false) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some @@ -596,7 +596,7 @@ val thy = Proof.theory_of state val ctxt = Proof.context_of state val atp_mode = - if Config.get ctxt aggressive then Sledgehammer_Aggressive + if Config.get ctxt completish then Sledgehammer_Completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal val (dest_dir, problem_prefix) =