# HG changeset patch # User blanchet # Date 1459159547 -7200 # Node ID 27333dc58e28a3bb4fb750620d1feea7a7822da1 # Parent 8adf274f5988747a645d82abe149dfe29d46dda6 refined experimental option of Sledgehammer diff -r 8adf274f5988 -r 27333dc58e28 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Sat Mar 26 18:51:58 2016 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Mon Mar 28 12:05:47 2016 +0200 @@ -185,7 +185,7 @@ val thy = Proof_Context.theory_of ctxt val assm_ths0 = map (Skip_Proof.make_thm thy) assms val ((assm_name, _), ctxt) = ctxt - |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0) + |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 2 else 0) |> Local_Theory.note ((@{binding thms}, []), assm_ths0) fun ref_of th = (Facts.named (Thm.derivation_name th), []) diff -r 8adf274f5988 -r 27333dc58e28 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Mar 26 18:51:58 2016 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Mar 28 12:05:47 2016 +0200 @@ -15,7 +15,7 @@ type atp_formula_role = ATP_Problem.atp_formula_role type 'a atp_problem = 'a ATP_Problem.atp_problem - datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator + datatype mode = Metis | Sledgehammer | Sledgehammer_Completish of int | Exporter | Translator datatype scope = Global | Local | Assum | Chained datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def @@ -126,7 +126,7 @@ open ATP_Util open ATP_Problem -datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator +datatype mode = Metis | Sledgehammer | Sledgehammer_Completish of int | Exporter | Translator datatype scope = Global | Local | Assum | Chained datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def @@ -1530,7 +1530,7 @@ val predicator_iconst = IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, []) fun predicatify completish tm = - if completish then + if completish > 0 then IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm), fTrue_iconst) else IApp (predicator_iconst, tm) @@ -1734,14 +1734,14 @@ fold (fn ((helper_s, needs_sound), ths) => if (needs_sound andalso not sound) orelse (helper_s <> unmangled_s andalso - (not completish orelse could_specialize)) then + (completish < 2 orelse could_specialize)) then I else ths ~~ (1 upto length ths) |> maps (dub_and_inst needs_sound o apfst (apsnd Thm.prop_of)) |> make_facts |> union (op = o apply2 #iformula)) - (if completish then completish_helper_table else helper_table) + (if completish >= 2 then completish_helper_table else helper_table) end | NONE => I) fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab = @@ -2169,7 +2169,7 @@ 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 completish then tvar_a else @{typ bool}]} + maybe_nonmono_Ts = [if completish >= 2 then tvar_a else @{typ bool}]} (* This inference is described in section 4 of Blanchette et al., "Encoding monomorphic and polymorphic types", TACAS 2013. *) @@ -2572,13 +2572,13 @@ let val thy = Proof_Context.theory_of ctxt val type_enc = type_enc |> adjust_type_enc format - val completish = (mode = Sledgehammer_Completish) + val completish = (case mode of Sledgehammer_Completish k => k | _ => 0) (* Forcing explicit applications is expensive for polymorphic encodings, because it takes only one existential variable ranging over "'a => 'b" to 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 completish then + if completish > 0 then Full_App_Op_And_Predicator else if length facts + length hyp_ts >= app_op_and_predicator_threshold then if is_type_enc_polymorphic type_enc then Min_App_Op else Sufficient_App_Op diff -r 8adf274f5988 -r 27333dc58e28 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Mar 26 18:51:58 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Mar 28 12:05:47 2016 +0200 @@ -13,7 +13,7 @@ val atp_dest_dir : string Config.T val atp_problem_prefix : string Config.T - val atp_completish : bool Config.T + val atp_completish : int Config.T val atp_full_names : bool Config.T val is_ho_atp : Proof.context -> string -> bool @@ -41,7 +41,7 @@ val atp_dest_dir = Attrib.setup_config_string @{binding sledgehammer_atp_dest_dir} (K "") val atp_problem_prefix = Attrib.setup_config_string @{binding sledgehammer_atp_problem_prefix} (K "prob") -val atp_completish = Attrib.setup_config_bool @{binding sledgehammer_atp_completish} (K false) +val atp_completish = Attrib.setup_config_int @{binding sledgehammer_atp_completish} (K 0) (* 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 provers (e.g., E). For these reason, short names are enabled by default. *) @@ -146,7 +146,8 @@ val waldmeister_new = (local_name = waldmeister_newN) val spassy = (local_name = pirateN orelse local_name = spassN) - val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer + val completish = Config.get ctxt atp_completish + val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name