--- a/doc-src/Sledgehammer/sledgehammer.tex Sun Feb 05 17:43:15 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Feb 06 23:01:01 2012 +0100
@@ -1059,25 +1059,26 @@
$\const{t}(\tau, t)$ becomes a unary function
$\const{t\_}\tau(t)$.
-\item[\labelitemi] \textbf{\textit{mono\_simple} (sound):} Exploits simple
+\item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native
first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
falls back on \textit{mono\_guards}. The problem is monomorphized.
-\item[\labelitemi] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
-higher-order types if the prover supports the THF0 syntax; otherwise, falls back
-on \textit{mono\_simple} or \textit{mono\_guards}. The problem is monomorphized.
+\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits
+native higher-order types if the prover supports the THF0 syntax; otherwise,
+falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is
+monomorphized.
\item[\labelitemi]
\textbf{%
\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
-\textit{mono\_simple}? (sound*):} \\
+\textit{mono\_native}? (sound*):} \\
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
-\textit{mono\_tags}, and \textit{mono\_simple} are fully
+\textit{mono\_tags}, and \textit{mono\_native} are fully
typed and sound. For each of these, Sledgehammer also provides a lighter,
virtually sound variant identified by a question mark (`\hbox{?}')\ that detects
-and erases monotonic types, notably infinite types. (For \textit{mono\_simple},
+and erases monotonic types, notably infinite types. (For \textit{mono\_native},
the types are not actually erased but rather replaced by a shared uniform type
of individuals.) As argument to the \textit{metis} proof method, the question
mark is replaced by a \hbox{``\textit{\_query\/}''} suffix.
@@ -1102,14 +1103,14 @@
\textbf{%
\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
-\textit{mono\_simple}!, \textit{mono\_simple\_higher}! (mildly unsound):} \\
+\textit{mono\_native}!, \textit{mono\_native\_higher}! (mildly unsound):} \\
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
-\textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}
+\textit{mono\_tags}, \textit{mono\_native}, and \textit{mono\_native\_higher}
also admit a mildly unsound (but very efficient) variant identified by an
exclamation mark (`\hbox{!}') that detects and erases erases all types except
-those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple}
-and \textit{mono\_simple\_higher}, the types are not actually erased but rather
+those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_native}
+and \textit{mono\_native\_higher}, the types are not actually erased but rather
replaced by a shared uniform type of individuals.) As argument to the
\textit{metis} proof method, the exclamation mark is replaced by the suffix
\hbox{``\textit{\_bang\/}''}.
@@ -1134,7 +1135,7 @@
the ATP and should be the most efficient virtually sound encoding for that ATP.
\end{enum}
-For SMT solvers, the type encoding is always \textit{mono\_simple}, irrespective
+For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective
of the value of this option.
\nopagebreak
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun Feb 05 17:43:15 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Feb 06 23:01:01 2012 +0100
@@ -279,9 +279,9 @@
prem_kind = Hypothesis,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN, false),
+ [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false),
sosN))),
- (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN, false),
+ (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false),
no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -306,7 +306,7 @@
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_native_higher", keep_lamsN,
false), "")))]}
val satallax = (satallaxN, satallax_config)
@@ -350,9 +350,9 @@
val spass = (spassN, spass_config)
-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)
+val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_native", combsN, true)
+val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_native", combsN, true)
+val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_native", liftingN, true)
(* Experimental *)
val spass_new_config : atp_config =
@@ -420,9 +420,9 @@
else
[(0.333, (false, ((150, vampire_tff0, "poly_guards??",
combs_or_liftingN, false), sosN))),
- (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN,
+ (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN,
false), sosN))),
- (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN,
+ (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN,
false), no_sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -445,10 +445,10 @@
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- 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), "")))]}
+ K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))),
+ (0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))),
+ (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))),
+ (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))]}
val z3_tptp = (z3_tptpN, z3_tptp_config)
@@ -469,11 +469,11 @@
else combsN, false), "")))]}
val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
-val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
+val dummy_tff1_config = dummy_config dummy_tff1_format "poly_native"
val dummy_tff1 = (dummy_tff1N, dummy_tff1_config)
val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
-val dummy_thf_config = dummy_config dummy_thf_format "poly_simple_higher"
+val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
val dummy_thf = (dummy_thfN, dummy_thf_config)
@@ -547,17 +547,17 @@
(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, false) (* FUDGE *))
+ (K (100, leo2_thf0, "mono_native_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, false)
+ (K (100, satallax_thf0, "mono_native_higher", keep_lamsN, false)
(* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["1.8"]
(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, false) (* FUDGE *))
+ (K (250, z3_tff0, "mono_native", 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, false) (* FUDGE *))
@@ -570,11 +570,11 @@
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
- (K (100, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
+ (K (100, explicit_tff0, "mono_native", 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, false) (* FUDGE *))
+ (K (150, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
[("#START OF PROOF", "Proved Goals:")]