# HG changeset patch # User blanchet # Date 1328353698 -3600 # Node ID d4754183ccce7a6794fff3e679f8f6a37c8ca7c8 # Parent 2520cd337056975eeb352a411976f2ac2d93f4bd made option available to users (mostly for experiments) diff -r 2520cd337056 -r d4754183ccce NEWS --- a/NEWS Sat Feb 04 07:40:02 2012 +0100 +++ b/NEWS Sat Feb 04 12:08:18 2012 +0100 @@ -305,7 +305,7 @@ affecting 'rat' and 'real'. * Sledgehammer: - - Added "lam_trans" and "minimize" options. + - Added "lam_trans", "uncurry_aliases", and "minimize" options. - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice"). - Renamed "sound" option to "strict". diff -r 2520cd337056 -r d4754183ccce doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Sat Feb 04 07:40:02 2012 +0100 +++ b/doc-src/Sledgehammer/sledgehammer.tex Sat Feb 04 12:08:18 2012 +0100 @@ -722,6 +722,7 @@ \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} +\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]} \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]} @@ -1005,6 +1006,10 @@ For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting}, irrespective of the value of this option. +\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases} +Specifies the $\lambda$ translation scheme to use in ATP problems. The supported +translation schemes are listed below: + \opdefault{type\_enc}{string}{smart} Specifies the type encoding to use in ATP problems. Some of the type encodings are unsound, meaning that they can give rise to spurious proofs diff -r 2520cd337056 -r d4754183ccce src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Sat Feb 04 07:40:02 2012 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Sat Feb 04 12:08:18 2012 +0100 @@ -181,7 +181,7 @@ ((Thm.get_name_hint th, loc), th |> prop_of |> mono ? monomorphize_term ctxt)) |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false - true [] @{prop False} + false true [] @{prop False} |> #1 val atp_problem = atp_problem diff -r 2520cd337056 -r d4754183ccce src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Feb 04 07:40:02 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Feb 04 12:08:18 2012 +0100 @@ -103,7 +103,7 @@ val factsN : string val prepare_atp_problem : Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc - -> bool -> string -> bool -> bool -> term list -> term + -> bool -> string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list -> string problem * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table @@ -166,7 +166,7 @@ val sym_decl_prefix = "sy_" val guards_sym_formula_prefix = "gsy_" val tags_sym_formula_prefix = "tsy_" -val app_op_alias_eq_prefix = "aa_" +val uncurried_alias_eq_prefix = "unc_" val fact_prefix = "fact_" val conjecture_prefix = "conj_" val helper_prefix = "help_" @@ -875,10 +875,10 @@ if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T) (* This shouldn't clash with anything else. *) -val app_op_alias_sep = "\000" +val uncurried_alias_sep = "\000" val mangled_type_sep = "\001" -val ascii_of_app_op_alias_sep = ascii_of app_op_alias_sep +val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep fun generic_mangled_type_name f (ATerm (name, [])) = f name | generic_mangled_type_name f (ATerm (name, tys)) = @@ -919,10 +919,10 @@ ho_type_from_ho_term type_enc pred_sym ary o ho_term_from_typ format type_enc -fun aliased_app_op ary (s, s') = - (s ^ ascii_of_app_op_alias_sep ^ string_of_int ary, s' ^ string_of_int ary) -fun unaliased_app_op (s, s') = - case space_explode app_op_alias_sep s of +fun aliased_uncurried ary (s, s') = + (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary) +fun unaliased_uncurried (s, s') = + case space_explode uncurried_alias_sep s of [_] => (s, s') | [s1, s2] => (s1, unsuffix s2 s') | _ => raise Fail "ill-formed explicit application alias" @@ -955,7 +955,7 @@ |> fst fun unmangled_const_name s = - (s, s) |> unaliased_app_op |> fst |> space_explode mangled_type_sep + (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep fun unmangled_const s = let val ss = unmangled_const_name s in (hd ss, map unmangled_type (tl ss)) @@ -1533,7 +1533,7 @@ in list_app app [head, arg] end fun firstorderize_fact thy monom_constrs format type_enc sym_tab - app_op_aliases = + uncurried_aliases = let fun do_app arg head = do_app_op format type_enc head arg fun list_app_ops head args = fold do_app args head @@ -1541,10 +1541,11 @@ let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in case head of IConst (name as (s, _), T, T_args) => - if app_op_aliases andalso String.isPrefix const_prefix s then + if uncurried_aliases andalso String.isPrefix const_prefix s then let val ary = length args - val name = name |> ary > min_ary_of sym_tab s ? aliased_app_op ary + val name = name |> ary > min_ary_of sym_tab s + ? aliased_uncurried ary in list_app (IConst (name, T, T_args)) args end else args |> chop (min_ary_of sym_tab s) @@ -2393,8 +2394,8 @@ fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) -fun do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono - type_enc sym_tab0 sym_tab base_s0 types in_conj = +fun do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind + mono type_enc sym_tab0 sym_tab base_s0 types in_conj = let fun do_alias ary = let @@ -2412,8 +2413,8 @@ fun do_const name = IConst (name, T, T_args) val do_term = ho_term_from_iterm ctxt format mono type_enc (SOME true) val name1 as (s1, _) = - base_name |> ary - 1 > base_ary ? aliased_app_op (ary - 1) - val name2 as (s2, _) = base_name |> aliased_app_op ary + base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1) + val name2 as (s2, _) = base_name |> aliased_uncurried ary val (arg_Ts, _) = chop_fun ary T val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int) @@ -2431,35 +2432,35 @@ (do_term tm1) (do_term tm2) in ([tm1, tm2], - [Formula (app_op_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, NONE, - isabelle_info format spec_eqN helper_rank)]) + [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, + NONE, isabelle_info format spec_eqN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end in do_alias end -fun app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono - type_enc sym_tab0 sym_tab - (s, {min_ary, types, in_conj, ...} : sym_info) = +fun uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono + type_enc sym_tab0 sym_tab + (s, {min_ary, types, in_conj, ...} : sym_info) = case unprefix_and_unascii const_prefix s of SOME mangled_s => - if String.isSubstring app_op_alias_sep mangled_s then + if String.isSubstring uncurried_alias_sep mangled_s then let val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const in - do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind + do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary end else ([], []) | NONE => ([], []) -fun app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind - mono type_enc app_op_aliases sym_tab0 sym_tab = +fun uncurried_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind + mono type_enc uncurried_aliases sym_tab0 sym_tab = ([], []) - |> app_op_aliases + |> uncurried_aliases ? Symtab.fold_rev (pair_append - o app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind - mono type_enc sym_tab0 sym_tab) sym_tab + o uncurried_alias_lines_for_sym ctxt monom_constrs format + conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab fun needs_type_tag_idempotence ctxt (Tags (poly, level)) = Config.get ctxt type_tag_idempotence andalso @@ -2469,7 +2470,7 @@ val implicit_declsN = "Should-be-implicit typings" val explicit_declsN = "Explicit typings" -val app_op_alias_eqsN = "Application aliases" +val uncurried_alias_eqsN = "Uncurried aliases" val factsN = "Relevant facts" val class_relsN = "Class relationships" val aritiesN = "Arities" @@ -2554,7 +2555,8 @@ val app_op_threshold = 50 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter - lam_trans readable_names preproc hyp_ts concl_t facts = + lam_trans uncurried_aliases readable_names preproc + hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt val type_enc = type_enc |> adjust_type_enc format @@ -2568,7 +2570,6 @@ Incomplete_Apply else Sufficient_Apply - val app_op_aliases = (format = DFG DFG_Sorted) val lam_trans = if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then @@ -2587,7 +2588,7 @@ |>> map (make_fixed_const (SOME format)) fun firstorderize in_helper = firstorderize_fact thy monom_constrs format type_enc sym_tab0 - (app_op_aliases andalso not in_helper) + (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 helpers = @@ -2596,11 +2597,11 @@ val mono_Ts = helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc val class_decl_lines = decl_lines_for_classes type_enc classes - val (app_op_alias_eq_tms, app_op_alias_eq_lines) = - app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind - mono type_enc app_op_aliases sym_tab0 sym_tab + val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) = + uncurried_alias_lines_for_sym_table ctxt monom_constrs format + conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab val sym_decl_lines = - (conjs, helpers @ facts, app_op_alias_eq_tms) + (conjs, helpers @ facts, uncurried_alias_eq_tms) |> sym_decl_table_for_facts ctxt format type_enc sym_tab |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc mono_Ts @@ -2622,7 +2623,7 @@ FLOTTER hack. *) val problem = [(explicit_declsN, class_decl_lines @ sym_decl_lines), - (app_op_alias_eqsN, app_op_alias_eq_lines), + (uncurried_alias_eqsN, uncurried_alias_eq_lines), (factsN, fact_lines), (class_relsN, map (formula_line_for_class_rel_clause format type_enc) diff -r 2520cd337056 -r d4754183ccce src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sat Feb 04 07:40:02 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Feb 04 12:08:18 2012 +0100 @@ -11,6 +11,7 @@ type formula_kind = ATP_Problem.formula_kind type failure = ATP_Proof.failure + type slice_spec = int * atp_format * string * string * bool type atp_config = {exec : string * string, required_execs : (string * string) list, @@ -22,9 +23,7 @@ conj_sym_kind : formula_kind, prem_kind : formula_kind, best_slices : - Proof.context - -> (real * (bool * ((int * atp_format * string * string) * string))) - list} + Proof.context -> (real * (bool * (slice_spec * string))) list} val force_sos : bool Config.T val e_smartN : string @@ -58,8 +57,7 @@ val remote_atp : string -> string -> string list -> (string * string) list -> (failure * string) list -> formula_kind -> formula_kind - -> (Proof.context -> int * atp_format * string * string) - -> string * atp_config + -> (Proof.context -> slice_spec) -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list @@ -77,6 +75,8 @@ (* ATP configuration *) +type slice_spec = int * atp_format * string * string * bool + type atp_config = {exec : string * string, required_execs : (string * string) list, @@ -87,17 +87,16 @@ known_failures : (failure * string) list, conj_sym_kind : formula_kind, prem_kind : formula_kind, - best_slices : - Proof.context - -> (real * (bool * ((int * atp_format * string * string) * string))) list} + best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list} (* "best_slices" must be found empirically, taking a wholistic approach since the ATPs are run in parallel. The "real" component gives the faction of the - time available given to the slice and should add up to 1.0. The "bool" + time available given to the slice and should add up to 1.0. The first "bool" component indicates whether the slice's strategy is complete; the "int", the preferred number of facts to pass; the first "string", the preferred type system (which should be sound or quasi-sound); the second "string", the - preferred lambda translation scheme; the third "string", extra information to + preferred lambda translation scheme; the second "bool", whether uncurried + aliased should be generated; the third "string", extra information to the prover (e.g., SOS or no SOS). The last slice should be the most "normal" one, because it will get all the @@ -248,12 +247,14 @@ let val method = effective_e_weight_method ctxt in (* FUDGE *) if method = e_smartN then - [(0.333, (true, ((500, FOF, "mono_tags??", combsN), e_fun_weightN))), - (0.334, (true, ((50, FOF, "mono_guards??", combsN), e_fun_weightN))), - (0.333, (true, ((1000, FOF, "mono_tags??", combsN), + [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), + e_fun_weightN))), + (0.334, (true, ((50, FOF, "mono_guards??", combsN, false), + e_fun_weightN))), + (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))] else - [(1.0, (true, ((500, FOF, "mono_tags??", combsN), method)))] + [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))] end} val e = (eN, e_config) @@ -278,9 +279,9 @@ prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN), + [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN, false), sosN))), - (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN), + (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN, false), no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -305,8 +306,8 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN), - "")))]} + K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN, + false), "")))]} val satallax = (satallaxN, satallax_config) @@ -338,20 +339,20 @@ prem_kind = Conjecture, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN), + [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false), sosN))), - (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN), + (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false), sosN))), - (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN), + (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} val spass = (spassN, spass_config) -val spass_new_macro_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN) -val spass_new_macro_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN) -val spass_new_macro_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN) +val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN, true) +val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN, true) +val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN, true) (* Experimental *) val spass_new_config : atp_config = @@ -368,9 +369,9 @@ prem_kind = #prem_kind spass_config, best_slices = fn _ => (* FUDGE *) - [(0.300, (true, (spass_new_macro_slice_1, ""))), - (0.333, (true, (spass_new_macro_slice_2, ""))), - (0.333, (true, (spass_new_macro_slice_3, "")))]} + [(0.300, (true, (spass_new_slice_1, ""))), + (0.333, (true, (spass_new_slice_2, ""))), + (0.333, (true, (spass_new_slice_3, "")))]} val spass_new = (spass_newN, spass_new_config) @@ -410,18 +411,19 @@ best_slices = fn ctxt => (* FUDGE *) (if is_old_vampire_version () then - [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN), - sosN))), - (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN), sosN))), - (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN), + [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), + sosN))), + (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), + sosN))), + (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))] else [(0.333, (false, ((150, vampire_tff0, "poly_guards??", - combs_or_liftingN), sosN))), - (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN), - sosN))), - (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN), - no_sosN)))]) + combs_or_liftingN, false), sosN))), + (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN, + false), sosN))), + (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN, + false), no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -443,10 +445,10 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN), ""))), - (0.25, (false, ((125, z3_tff0, "mono_simple", combsN), ""))), - (0.125, (false, ((62, z3_tff0, "mono_simple", combsN), ""))), - (0.125, (false, ((31, z3_tff0, "mono_simple", combsN), "")))]} + K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN, false), ""))), + (0.25, (false, ((125, z3_tff0, "mono_simple", combsN, false), ""))), + (0.125, (false, ((62, z3_tff0, "mono_simple", combsN, false), ""))), + (0.125, (false, ((31, z3_tff0, "mono_simple", combsN, false), "")))]} val z3_tptp = (z3_tptpN, z3_tptp_config) @@ -464,7 +466,7 @@ best_slices = K [(1.0, (false, ((200, format, type_enc, if is_format_higher_order format then keep_lamsN - else combsN), "")))]} + else combsN, false), "")))]} val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit) val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple" @@ -515,16 +517,13 @@ {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => - "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) - ^ " -s " ^ the_system system_name system_versions, + "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^ + " -s " ^ the_system system_name system_versions, proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ known_says_failures, conj_sym_kind = conj_sym_kind, prem_kind = prem_kind, - best_slices = fn ctxt => - let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in - [(1.0, (false, ((max_relevant, format, type_enc, lam_trans), "")))] - end} + best_slices = fn ctxt => [(1.0, (false, (best_slice ctxt, "")))]} fun remotify_config system_name system_versions best_slice ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...} @@ -545,43 +544,44 @@ val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] - (K (750, FOF, "mono_tags??", combsN) (* FUDGE *)) + (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"] - (K (100, leo2_thf0, "mono_simple_higher", liftingN) (* FUDGE *)) + (K (100, leo2_thf0, "mono_simple_higher", liftingN, false) (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.1", "2.0", "2"] - (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *)) + (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN, false) + (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["1.8"] - (K (250, FOF, "mono_guards??", combs_or_liftingN) (* FUDGE *)) + (K (250, FOF, "mono_guards??", combs_or_liftingN, false) (* FUDGE *)) val remote_z3_tptp = remotify_atp z3_tptp "Z3" ["3.0"] - (K (250, z3_tff0, "mono_simple", combsN) (* FUDGE *)) + (K (250, z3_tff0, "mono_simple", combsN, false) (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom - Conjecture (K (500, FOF, "mono_guards??", combsN) (* FUDGE *)) + Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *)) val remote_iprover = remote_atp iproverN "iProver" [] [] [] Axiom Conjecture - (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *)) + (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *)) val remote_iprover_eq = remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture - (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *)) + (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis - (K (100, explicit_tff0, "mono_simple", liftingN) (* FUDGE *)) + (K (100, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *)) val remote_e_tofof = remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom Hypothesis - (K (150, explicit_tff0, "mono_simple", liftingN) (* FUDGE *)) + (K (150, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] [(OutOfResources, "Too many function symbols"), (Crashed, "Unrecoverable Segmentation Fault")] Hypothesis Hypothesis - (K (50, CNF_UEQ, "mono_tags??", combsN) (* FUDGE *)) + (K (50, CNF_UEQ, "mono_tags??", combsN, false) (* FUDGE *)) (* Setup *) diff -r 2520cd337056 -r d4754183ccce src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Sat Feb 04 07:40:02 2012 +0100 +++ b/src/HOL/Tools/Metis/metis_generate.ML Sat Feb 04 12:08:18 2012 +0100 @@ -242,7 +242,7 @@ val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans val (atp_problem, _, _, lifted, sym_tab) = prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans - false false [] @{prop False} props + false false false [] @{prop False} props (* val _ = tracing ("ATP PROBLEM: " ^ cat_lines (lines_for_atp_problem CNF atp_problem)) diff -r 2520cd337056 -r d4754183ccce src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Feb 04 07:40:02 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Feb 04 12:08:18 2012 +0100 @@ -89,6 +89,7 @@ ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), + ("uncurried_aliases", "smart"), ("relevance_thresholds", "0.45 0.85"), ("max_relevant", "smart"), ("max_mono_iters", "3"), @@ -107,14 +108,15 @@ ("no_overlord", "overlord"), ("non_blocking", "blocking"), ("non_strict", "strict"), + ("no_uncurried_aliases", "uncurried_aliases"), ("no_isar_proof", "isar_proof"), ("dont_slice", "slice"), ("dont_minimize", "minimize")] val params_for_minimize = ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans", - "max_mono_iters", "max_new_mono_instances", "isar_proof", - "isar_shrink_factor", "timeout", "preplay_timeout"] + "uncurried_aliases", "max_mono_iters", "max_new_mono_instances", + "isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"] val property_dependent_params = ["provers", "timeout"] @@ -286,6 +288,7 @@ | s => (type_enc_from_string Strict s; SOME s) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" + val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_option lookup_int "max_relevant" val max_mono_iters = lookup_int "max_mono_iters" @@ -304,8 +307,9 @@ in {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, provers = provers, type_enc = type_enc, strict = strict, - lam_trans = lam_trans, relevance_thresholds = relevance_thresholds, - max_relevant = max_relevant, max_mono_iters = max_mono_iters, + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, + relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, + max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, diff -r 2520cd337056 -r d4754183ccce src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Feb 04 07:40:02 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Feb 04 12:08:18 2012 +0100 @@ -48,7 +48,8 @@ fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, - isar_proof, isar_shrink_factor, preplay_timeout, ...} : params) + uncurried_aliases, isar_proof, isar_shrink_factor, + preplay_timeout, ...} : params) silent (prover : prover) timeout i n state facts = let val _ = @@ -62,8 +63,9 @@ val params = {debug = debug, verbose = verbose, overlord = overlord, blocking = true, provers = provers, type_enc = type_enc, strict = strict, - lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01), - max_relevant = SOME (length facts), max_mono_iters = max_mono_iters, + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, + relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts), + max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slice = false, minimize = SOME false, timeout = timeout, diff -r 2520cd337056 -r d4754183ccce src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Feb 04 07:40:02 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Feb 04 12:08:18 2012 +0100 @@ -27,6 +27,7 @@ type_enc: string option, strict: bool, lam_trans: string option, + uncurried_aliases: bool option, relevance_thresholds: real * real, max_relevant: int option, max_mono_iters: int, @@ -147,7 +148,7 @@ let val thy = Proof_Context.theory_of ctxt in case try (get_atp thy) name of SOME {best_slices, ...} => - exists (fn (_, (_, ((_, format, _, _), _))) => is_format format) + exists (fn (_, (_, ((_, format, _, _, _), _))) => is_format format) (best_slices ctxt) | NONE => false end @@ -291,6 +292,7 @@ type_enc: string option, strict: bool, lam_trans: string option, + uncurried_aliases: bool option, relevance_thresholds: real * real, max_relevant: int option, max_mono_iters: int, @@ -581,9 +583,9 @@ ({exec, required_execs, arguments, proof_delims, known_failures, conj_sym_kind, prem_kind, best_slices, ...} : atp_config) (params as {debug, verbose, overlord, type_enc, strict, lam_trans, - max_relevant, max_mono_iters, max_new_mono_instances, - isar_proof, isar_shrink_factor, slice, timeout, - preplay_timeout, ...}) + uncurried_aliases, max_relevant, max_mono_iters, + max_new_mono_instances, isar_proof, isar_shrink_factor, + slice, timeout, preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = let @@ -654,7 +656,8 @@ fun run_slice time_left (cache_key, cache_value) (slice, (time_frac, (complete, (key as (best_max_relevant, format, best_type_enc, - best_lam_trans), extra)))) = + best_lam_trans, best_uncurried_aliases), + extra)))) = let val num_facts = length facts |> is_none max_relevant @@ -687,6 +690,10 @@ case lam_trans of SOME s => s | NONE => best_lam_trans + val uncurried_aliases = + case uncurried_aliases of + SOME b => b + | NONE => best_uncurried_aliases val value as (atp_problem, _, fact_names, _, _) = if cache_key = SOME key then cache_value @@ -700,8 +707,8 @@ ? monomorphize_facts |> map (apsnd prop_of) |> prepare_atp_problem ctxt format conj_sym_kind prem_kind - type_enc false lam_trans readable_names true hyp_ts - concl_t + type_enc false lam_trans uncurried_aliases + readable_names true hyp_ts concl_t fun weights () = atp_problem_weights atp_problem val full_proof = debug orelse isar_proof val command = diff -r 2520cd337056 -r d4754183ccce src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Feb 04 07:40:02 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Feb 04 12:08:18 2012 +0100 @@ -74,9 +74,9 @@ fun adjust_reconstructor_params override_params ({debug, verbose, overlord, blocking, provers, type_enc, strict, - lam_trans, relevance_thresholds, max_relevant, max_mono_iters, - max_new_mono_instances, isar_proof, isar_shrink_factor, slice, - minimize, timeout, preplay_timeout, expect} : params) = + lam_trans, uncurried_aliases, relevance_thresholds, max_relevant, + max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, + slice, minimize, timeout, preplay_timeout, expect} : params) = let fun lookup_override name default_value = case AList.lookup (op =) override_params name of @@ -89,8 +89,8 @@ in {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, provers = provers, type_enc = type_enc, strict = strict, - lam_trans = lam_trans, max_relevant = max_relevant, - relevance_thresholds = relevance_thresholds, + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, + max_relevant = max_relevant, relevance_thresholds = relevance_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slice = slice,