1.1 --- a/NEWS Sat Feb 04 07:40:02 2012 +0100
1.2 +++ b/NEWS Sat Feb 04 12:08:18 2012 +0100
1.3 @@ -305,7 +305,7 @@
1.4 affecting 'rat' and 'real'.
1.5
1.6 * Sledgehammer:
1.7 - - Added "lam_trans" and "minimize" options.
1.8 + - Added "lam_trans", "uncurry_aliases", and "minimize" options.
1.9 - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
1.10 - Renamed "sound" option to "strict".
1.11
2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Sat Feb 04 07:40:02 2012 +0100
2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Sat Feb 04 12:08:18 2012 +0100
2.3 @@ -722,6 +722,7 @@
2.4 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
2.5 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
2.6 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
2.7 +\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
2.8 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
2.9 \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
2.10 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
2.11 @@ -1005,6 +1006,10 @@
2.12 For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting},
2.13 irrespective of the value of this option.
2.14
2.15 +\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases}
2.16 +Specifies the $\lambda$ translation scheme to use in ATP problems. The supported
2.17 +translation schemes are listed below:
2.18 +
2.19 \opdefault{type\_enc}{string}{smart}
2.20 Specifies the type encoding to use in ATP problems. Some of the type encodings
2.21 are unsound, meaning that they can give rise to spurious proofs
3.1 --- a/src/HOL/TPTP/atp_theory_export.ML Sat Feb 04 07:40:02 2012 +0100
3.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Sat Feb 04 12:08:18 2012 +0100
3.3 @@ -181,7 +181,7 @@
3.4 ((Thm.get_name_hint th, loc),
3.5 th |> prop_of |> mono ? monomorphize_term ctxt))
3.6 |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false
3.7 - true [] @{prop False}
3.8 + false true [] @{prop False}
3.9 |> #1
3.10 val atp_problem =
3.11 atp_problem
4.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Feb 04 07:40:02 2012 +0100
4.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Feb 04 12:08:18 2012 +0100
4.3 @@ -103,7 +103,7 @@
4.4 val factsN : string
4.5 val prepare_atp_problem :
4.6 Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
4.7 - -> bool -> string -> bool -> bool -> term list -> term
4.8 + -> bool -> string -> bool -> bool -> bool -> term list -> term
4.9 -> ((string * stature) * term) list
4.10 -> string problem * string Symtab.table * (string * stature) list vector
4.11 * (string * term) list * int Symtab.table
4.12 @@ -166,7 +166,7 @@
4.13 val sym_decl_prefix = "sy_"
4.14 val guards_sym_formula_prefix = "gsy_"
4.15 val tags_sym_formula_prefix = "tsy_"
4.16 -val app_op_alias_eq_prefix = "aa_"
4.17 +val uncurried_alias_eq_prefix = "unc_"
4.18 val fact_prefix = "fact_"
4.19 val conjecture_prefix = "conj_"
4.20 val helper_prefix = "help_"
4.21 @@ -875,10 +875,10 @@
4.22 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
4.23
4.24 (* This shouldn't clash with anything else. *)
4.25 -val app_op_alias_sep = "\000"
4.26 +val uncurried_alias_sep = "\000"
4.27 val mangled_type_sep = "\001"
4.28
4.29 -val ascii_of_app_op_alias_sep = ascii_of app_op_alias_sep
4.30 +val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
4.31
4.32 fun generic_mangled_type_name f (ATerm (name, [])) = f name
4.33 | generic_mangled_type_name f (ATerm (name, tys)) =
4.34 @@ -919,10 +919,10 @@
4.35 ho_type_from_ho_term type_enc pred_sym ary
4.36 o ho_term_from_typ format type_enc
4.37
4.38 -fun aliased_app_op ary (s, s') =
4.39 - (s ^ ascii_of_app_op_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
4.40 -fun unaliased_app_op (s, s') =
4.41 - case space_explode app_op_alias_sep s of
4.42 +fun aliased_uncurried ary (s, s') =
4.43 + (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
4.44 +fun unaliased_uncurried (s, s') =
4.45 + case space_explode uncurried_alias_sep s of
4.46 [_] => (s, s')
4.47 | [s1, s2] => (s1, unsuffix s2 s')
4.48 | _ => raise Fail "ill-formed explicit application alias"
4.49 @@ -955,7 +955,7 @@
4.50 |> fst
4.51
4.52 fun unmangled_const_name s =
4.53 - (s, s) |> unaliased_app_op |> fst |> space_explode mangled_type_sep
4.54 + (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
4.55 fun unmangled_const s =
4.56 let val ss = unmangled_const_name s in
4.57 (hd ss, map unmangled_type (tl ss))
4.58 @@ -1533,7 +1533,7 @@
4.59 in list_app app [head, arg] end
4.60
4.61 fun firstorderize_fact thy monom_constrs format type_enc sym_tab
4.62 - app_op_aliases =
4.63 + uncurried_aliases =
4.64 let
4.65 fun do_app arg head = do_app_op format type_enc head arg
4.66 fun list_app_ops head args = fold do_app args head
4.67 @@ -1541,10 +1541,11 @@
4.68 let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
4.69 case head of
4.70 IConst (name as (s, _), T, T_args) =>
4.71 - if app_op_aliases andalso String.isPrefix const_prefix s then
4.72 + if uncurried_aliases andalso String.isPrefix const_prefix s then
4.73 let
4.74 val ary = length args
4.75 - val name = name |> ary > min_ary_of sym_tab s ? aliased_app_op ary
4.76 + val name = name |> ary > min_ary_of sym_tab s
4.77 + ? aliased_uncurried ary
4.78 in list_app (IConst (name, T, T_args)) args end
4.79 else
4.80 args |> chop (min_ary_of sym_tab s)
4.81 @@ -2393,8 +2394,8 @@
4.82
4.83 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
4.84
4.85 -fun do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
4.86 - type_enc sym_tab0 sym_tab base_s0 types in_conj =
4.87 +fun do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
4.88 + mono type_enc sym_tab0 sym_tab base_s0 types in_conj =
4.89 let
4.90 fun do_alias ary =
4.91 let
4.92 @@ -2412,8 +2413,8 @@
4.93 fun do_const name = IConst (name, T, T_args)
4.94 val do_term = ho_term_from_iterm ctxt format mono type_enc (SOME true)
4.95 val name1 as (s1, _) =
4.96 - base_name |> ary - 1 > base_ary ? aliased_app_op (ary - 1)
4.97 - val name2 as (s2, _) = base_name |> aliased_app_op ary
4.98 + base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
4.99 + val name2 as (s2, _) = base_name |> aliased_uncurried ary
4.100 val (arg_Ts, _) = chop_fun ary T
4.101 val bound_names =
4.102 1 upto ary |> map (`I o make_bound_var o string_of_int)
4.103 @@ -2431,35 +2432,35 @@
4.104 (do_term tm1) (do_term tm2)
4.105 in
4.106 ([tm1, tm2],
4.107 - [Formula (app_op_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, NONE,
4.108 - isabelle_info format spec_eqN helper_rank)])
4.109 + [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
4.110 + NONE, isabelle_info format spec_eqN helper_rank)])
4.111 |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
4.112 else pair_append (do_alias (ary - 1)))
4.113 end
4.114 in do_alias end
4.115 -fun app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
4.116 - type_enc sym_tab0 sym_tab
4.117 - (s, {min_ary, types, in_conj, ...} : sym_info) =
4.118 +fun uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
4.119 + type_enc sym_tab0 sym_tab
4.120 + (s, {min_ary, types, in_conj, ...} : sym_info) =
4.121 case unprefix_and_unascii const_prefix s of
4.122 SOME mangled_s =>
4.123 - if String.isSubstring app_op_alias_sep mangled_s then
4.124 + if String.isSubstring uncurried_alias_sep mangled_s then
4.125 let
4.126 val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
4.127 in
4.128 - do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
4.129 + do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
4.130 mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary
4.131 end
4.132 else
4.133 ([], [])
4.134 | NONE => ([], [])
4.135 -fun app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
4.136 - mono type_enc app_op_aliases sym_tab0 sym_tab =
4.137 +fun uncurried_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
4.138 + mono type_enc uncurried_aliases sym_tab0 sym_tab =
4.139 ([], [])
4.140 - |> app_op_aliases
4.141 + |> uncurried_aliases
4.142 ? Symtab.fold_rev
4.143 (pair_append
4.144 - o app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
4.145 - mono type_enc sym_tab0 sym_tab) sym_tab
4.146 + o uncurried_alias_lines_for_sym ctxt monom_constrs format
4.147 + conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab
4.148
4.149 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
4.150 Config.get ctxt type_tag_idempotence andalso
4.151 @@ -2469,7 +2470,7 @@
4.152
4.153 val implicit_declsN = "Should-be-implicit typings"
4.154 val explicit_declsN = "Explicit typings"
4.155 -val app_op_alias_eqsN = "Application aliases"
4.156 +val uncurried_alias_eqsN = "Uncurried aliases"
4.157 val factsN = "Relevant facts"
4.158 val class_relsN = "Class relationships"
4.159 val aritiesN = "Arities"
4.160 @@ -2554,7 +2555,8 @@
4.161 val app_op_threshold = 50
4.162
4.163 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
4.164 - lam_trans readable_names preproc hyp_ts concl_t facts =
4.165 + lam_trans uncurried_aliases readable_names preproc
4.166 + hyp_ts concl_t facts =
4.167 let
4.168 val thy = Proof_Context.theory_of ctxt
4.169 val type_enc = type_enc |> adjust_type_enc format
4.170 @@ -2568,7 +2570,6 @@
4.171 Incomplete_Apply
4.172 else
4.173 Sufficient_Apply
4.174 - val app_op_aliases = (format = DFG DFG_Sorted)
4.175 val lam_trans =
4.176 if lam_trans = keep_lamsN andalso
4.177 not (is_type_enc_higher_order type_enc) then
4.178 @@ -2587,7 +2588,7 @@
4.179 |>> map (make_fixed_const (SOME format))
4.180 fun firstorderize in_helper =
4.181 firstorderize_fact thy monom_constrs format type_enc sym_tab0
4.182 - (app_op_aliases andalso not in_helper)
4.183 + (uncurried_aliases andalso not in_helper)
4.184 val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
4.185 val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
4.186 val helpers =
4.187 @@ -2596,11 +2597,11 @@
4.188 val mono_Ts =
4.189 helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
4.190 val class_decl_lines = decl_lines_for_classes type_enc classes
4.191 - val (app_op_alias_eq_tms, app_op_alias_eq_lines) =
4.192 - app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
4.193 - mono type_enc app_op_aliases sym_tab0 sym_tab
4.194 + val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
4.195 + uncurried_alias_lines_for_sym_table ctxt monom_constrs format
4.196 + conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
4.197 val sym_decl_lines =
4.198 - (conjs, helpers @ facts, app_op_alias_eq_tms)
4.199 + (conjs, helpers @ facts, uncurried_alias_eq_tms)
4.200 |> sym_decl_table_for_facts ctxt format type_enc sym_tab
4.201 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
4.202 type_enc mono_Ts
4.203 @@ -2622,7 +2623,7 @@
4.204 FLOTTER hack. *)
4.205 val problem =
4.206 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
4.207 - (app_op_alias_eqsN, app_op_alias_eq_lines),
4.208 + (uncurried_alias_eqsN, uncurried_alias_eq_lines),
4.209 (factsN, fact_lines),
4.210 (class_relsN,
4.211 map (formula_line_for_class_rel_clause format type_enc)
5.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Sat Feb 04 07:40:02 2012 +0100
5.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Feb 04 12:08:18 2012 +0100
5.3 @@ -11,6 +11,7 @@
5.4 type formula_kind = ATP_Problem.formula_kind
5.5 type failure = ATP_Proof.failure
5.6
5.7 + type slice_spec = int * atp_format * string * string * bool
5.8 type atp_config =
5.9 {exec : string * string,
5.10 required_execs : (string * string) list,
5.11 @@ -22,9 +23,7 @@
5.12 conj_sym_kind : formula_kind,
5.13 prem_kind : formula_kind,
5.14 best_slices :
5.15 - Proof.context
5.16 - -> (real * (bool * ((int * atp_format * string * string) * string)))
5.17 - list}
5.18 + Proof.context -> (real * (bool * (slice_spec * string))) list}
5.19
5.20 val force_sos : bool Config.T
5.21 val e_smartN : string
5.22 @@ -58,8 +57,7 @@
5.23 val remote_atp :
5.24 string -> string -> string list -> (string * string) list
5.25 -> (failure * string) list -> formula_kind -> formula_kind
5.26 - -> (Proof.context -> int * atp_format * string * string)
5.27 - -> string * atp_config
5.28 + -> (Proof.context -> slice_spec) -> string * atp_config
5.29 val add_atp : string * atp_config -> theory -> theory
5.30 val get_atp : theory -> string -> atp_config
5.31 val supported_atps : theory -> string list
5.32 @@ -77,6 +75,8 @@
5.33
5.34 (* ATP configuration *)
5.35
5.36 +type slice_spec = int * atp_format * string * string * bool
5.37 +
5.38 type atp_config =
5.39 {exec : string * string,
5.40 required_execs : (string * string) list,
5.41 @@ -87,17 +87,16 @@
5.42 known_failures : (failure * string) list,
5.43 conj_sym_kind : formula_kind,
5.44 prem_kind : formula_kind,
5.45 - best_slices :
5.46 - Proof.context
5.47 - -> (real * (bool * ((int * atp_format * string * string) * string))) list}
5.48 + best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
5.49
5.50 (* "best_slices" must be found empirically, taking a wholistic approach since
5.51 the ATPs are run in parallel. The "real" component gives the faction of the
5.52 - time available given to the slice and should add up to 1.0. The "bool"
5.53 + time available given to the slice and should add up to 1.0. The first "bool"
5.54 component indicates whether the slice's strategy is complete; the "int", the
5.55 preferred number of facts to pass; the first "string", the preferred type
5.56 system (which should be sound or quasi-sound); the second "string", the
5.57 - preferred lambda translation scheme; the third "string", extra information to
5.58 + preferred lambda translation scheme; the second "bool", whether uncurried
5.59 + aliased should be generated; the third "string", extra information to
5.60 the prover (e.g., SOS or no SOS).
5.61
5.62 The last slice should be the most "normal" one, because it will get all the
5.63 @@ -248,12 +247,14 @@
5.64 let val method = effective_e_weight_method ctxt in
5.65 (* FUDGE *)
5.66 if method = e_smartN then
5.67 - [(0.333, (true, ((500, FOF, "mono_tags??", combsN), e_fun_weightN))),
5.68 - (0.334, (true, ((50, FOF, "mono_guards??", combsN), e_fun_weightN))),
5.69 - (0.333, (true, ((1000, FOF, "mono_tags??", combsN),
5.70 + [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false),
5.71 + e_fun_weightN))),
5.72 + (0.334, (true, ((50, FOF, "mono_guards??", combsN, false),
5.73 + e_fun_weightN))),
5.74 + (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false),
5.75 e_sym_offset_weightN)))]
5.76 else
5.77 - [(1.0, (true, ((500, FOF, "mono_tags??", combsN), method)))]
5.78 + [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))]
5.79 end}
5.80
5.81 val e = (eN, e_config)
5.82 @@ -278,9 +279,9 @@
5.83 prem_kind = Hypothesis,
5.84 best_slices = fn ctxt =>
5.85 (* FUDGE *)
5.86 - [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN),
5.87 + [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN, false),
5.88 sosN))),
5.89 - (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN),
5.90 + (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN, false),
5.91 no_sosN)))]
5.92 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
5.93 else I)}
5.94 @@ -305,8 +306,8 @@
5.95 prem_kind = Hypothesis,
5.96 best_slices =
5.97 (* FUDGE *)
5.98 - K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN),
5.99 - "")))]}
5.100 + K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN,
5.101 + false), "")))]}
5.102
5.103 val satallax = (satallaxN, satallax_config)
5.104
5.105 @@ -338,20 +339,20 @@
5.106 prem_kind = Conjecture,
5.107 best_slices = fn ctxt =>
5.108 (* FUDGE *)
5.109 - [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN),
5.110 + [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
5.111 sosN))),
5.112 - (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN),
5.113 + (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false),
5.114 sosN))),
5.115 - (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN),
5.116 + (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
5.117 no_sosN)))]
5.118 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
5.119 else I)}
5.120
5.121 val spass = (spassN, spass_config)
5.122
5.123 -val spass_new_macro_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN)
5.124 -val spass_new_macro_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN)
5.125 -val spass_new_macro_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN)
5.126 +val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN, true)
5.127 +val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN, true)
5.128 +val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN, true)
5.129
5.130 (* Experimental *)
5.131 val spass_new_config : atp_config =
5.132 @@ -368,9 +369,9 @@
5.133 prem_kind = #prem_kind spass_config,
5.134 best_slices = fn _ =>
5.135 (* FUDGE *)
5.136 - [(0.300, (true, (spass_new_macro_slice_1, ""))),
5.137 - (0.333, (true, (spass_new_macro_slice_2, ""))),
5.138 - (0.333, (true, (spass_new_macro_slice_3, "")))]}
5.139 + [(0.300, (true, (spass_new_slice_1, ""))),
5.140 + (0.333, (true, (spass_new_slice_2, ""))),
5.141 + (0.333, (true, (spass_new_slice_3, "")))]}
5.142
5.143 val spass_new = (spass_newN, spass_new_config)
5.144
5.145 @@ -410,18 +411,19 @@
5.146 best_slices = fn ctxt =>
5.147 (* FUDGE *)
5.148 (if is_old_vampire_version () then
5.149 - [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN),
5.150 - sosN))),
5.151 - (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN), sosN))),
5.152 - (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN),
5.153 + [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false),
5.154 + sosN))),
5.155 + (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false),
5.156 + sosN))),
5.157 + (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false),
5.158 no_sosN)))]
5.159 else
5.160 [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
5.161 - combs_or_liftingN), sosN))),
5.162 - (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN),
5.163 - sosN))),
5.164 - (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN),
5.165 - no_sosN)))])
5.166 + combs_or_liftingN, false), sosN))),
5.167 + (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN,
5.168 + false), sosN))),
5.169 + (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN,
5.170 + false), no_sosN)))])
5.171 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
5.172 else I)}
5.173
5.174 @@ -443,10 +445,10 @@
5.175 prem_kind = Hypothesis,
5.176 best_slices =
5.177 (* FUDGE *)
5.178 - K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN), ""))),
5.179 - (0.25, (false, ((125, z3_tff0, "mono_simple", combsN), ""))),
5.180 - (0.125, (false, ((62, z3_tff0, "mono_simple", combsN), ""))),
5.181 - (0.125, (false, ((31, z3_tff0, "mono_simple", combsN), "")))]}
5.182 + K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN, false), ""))),
5.183 + (0.25, (false, ((125, z3_tff0, "mono_simple", combsN, false), ""))),
5.184 + (0.125, (false, ((62, z3_tff0, "mono_simple", combsN, false), ""))),
5.185 + (0.125, (false, ((31, z3_tff0, "mono_simple", combsN, false), "")))]}
5.186
5.187 val z3_tptp = (z3_tptpN, z3_tptp_config)
5.188
5.189 @@ -464,7 +466,7 @@
5.190 best_slices =
5.191 K [(1.0, (false, ((200, format, type_enc,
5.192 if is_format_higher_order format then keep_lamsN
5.193 - else combsN), "")))]}
5.194 + else combsN, false), "")))]}
5.195
5.196 val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
5.197 val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
5.198 @@ -515,16 +517,13 @@
5.199 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
5.200 required_execs = [],
5.201 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
5.202 - "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
5.203 - ^ " -s " ^ the_system system_name system_versions,
5.204 + "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
5.205 + " -s " ^ the_system system_name system_versions,
5.206 proof_delims = union (op =) tstp_proof_delims proof_delims,
5.207 known_failures = known_failures @ known_perl_failures @ known_says_failures,
5.208 conj_sym_kind = conj_sym_kind,
5.209 prem_kind = prem_kind,
5.210 - best_slices = fn ctxt =>
5.211 - let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
5.212 - [(1.0, (false, ((max_relevant, format, type_enc, lam_trans), "")))]
5.213 - end}
5.214 + best_slices = fn ctxt => [(1.0, (false, (best_slice ctxt, "")))]}
5.215
5.216 fun remotify_config system_name system_versions best_slice
5.217 ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
5.218 @@ -545,43 +544,44 @@
5.219
5.220 val remote_e =
5.221 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
5.222 - (K (750, FOF, "mono_tags??", combsN) (* FUDGE *))
5.223 + (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *))
5.224 val remote_leo2 =
5.225 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
5.226 - (K (100, leo2_thf0, "mono_simple_higher", liftingN) (* FUDGE *))
5.227 + (K (100, leo2_thf0, "mono_simple_higher", liftingN, false) (* FUDGE *))
5.228 val remote_satallax =
5.229 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
5.230 - (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *))
5.231 + (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN, false)
5.232 + (* FUDGE *))
5.233 val remote_vampire =
5.234 remotify_atp vampire "Vampire" ["1.8"]
5.235 - (K (250, FOF, "mono_guards??", combs_or_liftingN) (* FUDGE *))
5.236 + (K (250, FOF, "mono_guards??", combs_or_liftingN, false) (* FUDGE *))
5.237 val remote_z3_tptp =
5.238 remotify_atp z3_tptp "Z3" ["3.0"]
5.239 - (K (250, z3_tff0, "mono_simple", combsN) (* FUDGE *))
5.240 + (K (250, z3_tff0, "mono_simple", combsN, false) (* FUDGE *))
5.241 val remote_e_sine =
5.242 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
5.243 - Conjecture (K (500, FOF, "mono_guards??", combsN) (* FUDGE *))
5.244 + Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *))
5.245 val remote_iprover =
5.246 remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
5.247 - (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
5.248 + (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
5.249 val remote_iprover_eq =
5.250 remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
5.251 - (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
5.252 + (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
5.253 val remote_snark =
5.254 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
5.255 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
5.256 - (K (100, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
5.257 + (K (100, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
5.258 val remote_e_tofof =
5.259 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
5.260 Hypothesis
5.261 - (K (150, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
5.262 + (K (150, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
5.263 val remote_waldmeister =
5.264 remote_atp waldmeisterN "Waldmeister" ["710"]
5.265 [("#START OF PROOF", "Proved Goals:")]
5.266 [(OutOfResources, "Too many function symbols"),
5.267 (Crashed, "Unrecoverable Segmentation Fault")]
5.268 Hypothesis Hypothesis
5.269 - (K (50, CNF_UEQ, "mono_tags??", combsN) (* FUDGE *))
5.270 + (K (50, CNF_UEQ, "mono_tags??", combsN, false) (* FUDGE *))
5.271
5.272 (* Setup *)
5.273
6.1 --- a/src/HOL/Tools/Metis/metis_generate.ML Sat Feb 04 07:40:02 2012 +0100
6.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML Sat Feb 04 12:08:18 2012 +0100
6.3 @@ -242,7 +242,7 @@
6.4 val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
6.5 val (atp_problem, _, _, lifted, sym_tab) =
6.6 prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
6.7 - false false [] @{prop False} props
6.8 + false false false [] @{prop False} props
6.9 (*
6.10 val _ = tracing ("ATP PROBLEM: " ^
6.11 cat_lines (lines_for_atp_problem CNF atp_problem))
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Feb 04 07:40:02 2012 +0100
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Feb 04 12:08:18 2012 +0100
7.3 @@ -89,6 +89,7 @@
7.4 ("type_enc", "smart"),
7.5 ("strict", "false"),
7.6 ("lam_trans", "smart"),
7.7 + ("uncurried_aliases", "smart"),
7.8 ("relevance_thresholds", "0.45 0.85"),
7.9 ("max_relevant", "smart"),
7.10 ("max_mono_iters", "3"),
7.11 @@ -107,14 +108,15 @@
7.12 ("no_overlord", "overlord"),
7.13 ("non_blocking", "blocking"),
7.14 ("non_strict", "strict"),
7.15 + ("no_uncurried_aliases", "uncurried_aliases"),
7.16 ("no_isar_proof", "isar_proof"),
7.17 ("dont_slice", "slice"),
7.18 ("dont_minimize", "minimize")]
7.19
7.20 val params_for_minimize =
7.21 ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
7.22 - "max_mono_iters", "max_new_mono_instances", "isar_proof",
7.23 - "isar_shrink_factor", "timeout", "preplay_timeout"]
7.24 + "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
7.25 + "isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"]
7.26
7.27 val property_dependent_params = ["provers", "timeout"]
7.28
7.29 @@ -286,6 +288,7 @@
7.30 | s => (type_enc_from_string Strict s; SOME s)
7.31 val strict = mode = Auto_Try orelse lookup_bool "strict"
7.32 val lam_trans = lookup_option lookup_string "lam_trans"
7.33 + val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
7.34 val relevance_thresholds = lookup_real_pair "relevance_thresholds"
7.35 val max_relevant = lookup_option lookup_int "max_relevant"
7.36 val max_mono_iters = lookup_int "max_mono_iters"
7.37 @@ -304,8 +307,9 @@
7.38 in
7.39 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
7.40 provers = provers, type_enc = type_enc, strict = strict,
7.41 - lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
7.42 - max_relevant = max_relevant, max_mono_iters = max_mono_iters,
7.43 + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
7.44 + relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
7.45 + max_mono_iters = max_mono_iters,
7.46 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
7.47 isar_shrink_factor = isar_shrink_factor, slice = slice,
7.48 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Feb 04 07:40:02 2012 +0100
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Feb 04 12:08:18 2012 +0100
8.3 @@ -48,7 +48,8 @@
8.4
8.5 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
8.6 max_new_mono_instances, type_enc, strict, lam_trans,
8.7 - isar_proof, isar_shrink_factor, preplay_timeout, ...} : params)
8.8 + uncurried_aliases, isar_proof, isar_shrink_factor,
8.9 + preplay_timeout, ...} : params)
8.10 silent (prover : prover) timeout i n state facts =
8.11 let
8.12 val _ =
8.13 @@ -62,8 +63,9 @@
8.14 val params =
8.15 {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
8.16 provers = provers, type_enc = type_enc, strict = strict,
8.17 - lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
8.18 - max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
8.19 + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
8.20 + relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
8.21 + max_mono_iters = max_mono_iters,
8.22 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
8.23 isar_shrink_factor = isar_shrink_factor, slice = false,
8.24 minimize = SOME false, timeout = timeout,
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Feb 04 07:40:02 2012 +0100
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Feb 04 12:08:18 2012 +0100
9.3 @@ -27,6 +27,7 @@
9.4 type_enc: string option,
9.5 strict: bool,
9.6 lam_trans: string option,
9.7 + uncurried_aliases: bool option,
9.8 relevance_thresholds: real * real,
9.9 max_relevant: int option,
9.10 max_mono_iters: int,
9.11 @@ -147,7 +148,7 @@
9.12 let val thy = Proof_Context.theory_of ctxt in
9.13 case try (get_atp thy) name of
9.14 SOME {best_slices, ...} =>
9.15 - exists (fn (_, (_, ((_, format, _, _), _))) => is_format format)
9.16 + exists (fn (_, (_, ((_, format, _, _, _), _))) => is_format format)
9.17 (best_slices ctxt)
9.18 | NONE => false
9.19 end
9.20 @@ -291,6 +292,7 @@
9.21 type_enc: string option,
9.22 strict: bool,
9.23 lam_trans: string option,
9.24 + uncurried_aliases: bool option,
9.25 relevance_thresholds: real * real,
9.26 max_relevant: int option,
9.27 max_mono_iters: int,
9.28 @@ -581,9 +583,9 @@
9.29 ({exec, required_execs, arguments, proof_delims, known_failures,
9.30 conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
9.31 (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
9.32 - max_relevant, max_mono_iters, max_new_mono_instances,
9.33 - isar_proof, isar_shrink_factor, slice, timeout,
9.34 - preplay_timeout, ...})
9.35 + uncurried_aliases, max_relevant, max_mono_iters,
9.36 + max_new_mono_instances, isar_proof, isar_shrink_factor,
9.37 + slice, timeout, preplay_timeout, ...})
9.38 minimize_command
9.39 ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
9.40 let
9.41 @@ -654,7 +656,8 @@
9.42 fun run_slice time_left (cache_key, cache_value)
9.43 (slice, (time_frac, (complete,
9.44 (key as (best_max_relevant, format, best_type_enc,
9.45 - best_lam_trans), extra)))) =
9.46 + best_lam_trans, best_uncurried_aliases),
9.47 + extra)))) =
9.48 let
9.49 val num_facts =
9.50 length facts |> is_none max_relevant
9.51 @@ -687,6 +690,10 @@
9.52 case lam_trans of
9.53 SOME s => s
9.54 | NONE => best_lam_trans
9.55 + val uncurried_aliases =
9.56 + case uncurried_aliases of
9.57 + SOME b => b
9.58 + | NONE => best_uncurried_aliases
9.59 val value as (atp_problem, _, fact_names, _, _) =
9.60 if cache_key = SOME key then
9.61 cache_value
9.62 @@ -700,8 +707,8 @@
9.63 ? monomorphize_facts
9.64 |> map (apsnd prop_of)
9.65 |> prepare_atp_problem ctxt format conj_sym_kind prem_kind
9.66 - type_enc false lam_trans readable_names true hyp_ts
9.67 - concl_t
9.68 + type_enc false lam_trans uncurried_aliases
9.69 + readable_names true hyp_ts concl_t
9.70 fun weights () = atp_problem_weights atp_problem
9.71 val full_proof = debug orelse isar_proof
9.72 val command =
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Feb 04 07:40:02 2012 +0100
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Feb 04 12:08:18 2012 +0100
10.3 @@ -74,9 +74,9 @@
10.4
10.5 fun adjust_reconstructor_params override_params
10.6 ({debug, verbose, overlord, blocking, provers, type_enc, strict,
10.7 - lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
10.8 - max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
10.9 - minimize, timeout, preplay_timeout, expect} : params) =
10.10 + lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
10.11 + max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
10.12 + slice, minimize, timeout, preplay_timeout, expect} : params) =
10.13 let
10.14 fun lookup_override name default_value =
10.15 case AList.lookup (op =) override_params name of
10.16 @@ -89,8 +89,8 @@
10.17 in
10.18 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
10.19 provers = provers, type_enc = type_enc, strict = strict,
10.20 - lam_trans = lam_trans, max_relevant = max_relevant,
10.21 - relevance_thresholds = relevance_thresholds,
10.22 + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
10.23 + max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
10.24 max_mono_iters = max_mono_iters,
10.25 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
10.26 isar_shrink_factor = isar_shrink_factor, slice = slice,