--- a/NEWS Mon Jun 27 22:23:44 2011 +0200
+++ b/NEWS Mon Jun 27 22:44:44 2011 +0200
@@ -85,14 +85,20 @@
INCOMPATIBILITY.
- Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
TPTP problems (TFF).
- - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options.
+ - Added "type_sys", "sound", "max_mono_iters", and "max_new_mono_instances"
+ options.
+ - Removed "full_types" option and corresponding Proof General menu item.
+ INCOMPATIBILITY.
* Metis:
- - Removed "metisF" -- use "metis" instead.
- - Obsoleted "metisFT" -- use "metis (full_types)" instead.
+ - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
+ - Obsoleted "metisFT" -- use "metis (full_types)" instead. INCOMPATIBILITY.
* "try":
- - Added "simp:", "intro:", and "elim:" options.
+ - Renamed "try_methods" and added "simp:", "intro:", "dest:", and "elim:"
+ options. INCOMPATIBILITY.
+ - Introduced "try" that not only runs "try_methods" but also "solve_direct",
+ "sledgehammer", "quickcheck", and "nitpick".
* Quickcheck:
- Added "eval" option to evaluate terms for the found counterexample
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 27 22:23:44 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 27 22:44:44 2011 +0200
@@ -1287,6 +1287,33 @@
number of rule premises will be taken into account here.
*}
+section {* Model Elimination and Resolution *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{method_def (HOL) "meson"} & : & @{text method} \\
+ @{method_def (HOL) "metis"} & : & @{text method} \\
+ \end{matharray}
+
+ @{rail "
+ @@{method (HOL) meson} @{syntax thmrefs}?
+ ;
+
+ @@{method (HOL) metis} ( '(' ('partial_types' | 'full_types' | 'no_types'
+ | @{syntax name}) ')' )? @{syntax thmrefs}?
+ "}
+
+ The @{method (HOL) meson} method implements Loveland's model elimination
+ procedure \cite{loveland-78}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for
+ examples.
+
+ The @{method (HOL) metis} method combines ordered resolution and ordered
+ paramodulation to find first-order (or mildly higher-order) proofs. The first
+ optional argument specifies a type encoding; see the Sledgehammer manual
+ \cite{isabelle-sledgehammer} for details. The @{file
+ "~~/src/HOL/Metis_Examples"} directory contains several small theories
+ developed to a large extent using Metis.
+*}
section {* Coherent Logic *}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 27 22:23:44 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 27 22:44:44 2011 +0200
@@ -1816,6 +1816,60 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Model Elimination and Resolution%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{HOL}{method}{meson}\hypertarget{method.HOL.meson}{\hyperlink{method.HOL.meson}{\mbox{\isa{meson}}}} & : & \isa{method} \\
+ \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
+ \end{matharray}
+
+ \begin{railoutput}
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.HOL.meson}{\mbox{\isa{meson}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
+\rail@begin{5}{}
+\rail@term{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@bar
+\rail@term{\isa{partial{\isaliteral{5F}{\isacharunderscore}}types}}[]
+\rail@nextbar{2}
+\rail@term{\isa{full{\isaliteral{5F}{\isacharunderscore}}types}}[]
+\rail@nextbar{3}
+\rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}types}}[]
+\rail@nextbar{4}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@endbar
+\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+ The \hyperlink{method.HOL.meson}{\mbox{\isa{meson}}} method implements Loveland's model elimination
+ procedure \cite{loveland-78}. See \verb|~~/src/HOL/ex/Meson_Test.thy| for
+ examples.
+
+ The \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}} method combines ordered resolution and ordered
+ paramodulation to find first-order (or mildly higher-order) proofs. The first
+ optional argument specifies a type encoding; see the Sledgehammer manual
+ \cite{isabelle-sledgehammer} for details. The \verb|~~/src/HOL/Metis_Examples| directory contains several small theories
+ developed to a large extent using Metis.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Coherent Logic%
}
\isamarkuptrue%
--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 27 22:23:44 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 27 22:44:44 2011 +0200
@@ -337,12 +337,6 @@
and simply write the prover names as a space-separated list (e.g., ``\textit{e
spass remote\_vampire}'').
-\item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding})
-specifies whether type-sound encodings should be used. By default, Sledgehammer
-employs a mixture of type-sound and type-unsound encodings, occasionally
-yielding unsound ATP proofs. In contrast, SMT solver proofs should always be
-sound.
-
\item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
specifies the maximum number of facts that should be passed to the provers. By
default, the value is prover-dependent but varies between about 150 and 1000. If
@@ -404,37 +398,26 @@
Proof reconstruction failed.
\postw
-This usually indicates that Sledgehammer found a type-incorrect proof.
-Sledgehammer erases some type information to speed up the search. Try
-Sledgehammer again with full type information: \textit{full\_types}
-(\S\ref{problem-encoding}), or choose a specific type encoding with
-\textit{type\_sys} (\S\ref{problem-encoding}). Older versions of Sledgehammer
-were frequent victims of this problem. Now this should very seldom be an issue,
-but if you notice many unsound proofs, contact the author at \authoremail.
+This message usually indicates that Sledgehammer found a type-incorrect proof.
+This was a frequent issue with older versions of Sledgehammer, which did not
+supply enough typing information to the ATPs by default. If you notice many
+unsound proofs and are not using \textit{type\_sys} (\S\ref{problem-encoding}),
+contact the author at \authoremail.
\point{How can I tell whether a generated proof is sound?}
-First, if Metis can reconstruct it, the proof is sound (modulo soundness of
-Isabelle's inference kernel). If it fails or runs seemingly forever, you can try
+First, if Metis can reconstruct it, the proof is sound (assuming Isabelle's
+inference kernel is sound). If it fails or runs seemingly forever, you can try
\prew
\textbf{apply}~\textbf{--} \\
-\textbf{sledgehammer} [\textit{type\_sys} = \textit{poly\_tags}] (\textit{metis\_facts})
+\textbf{sledgehammer} [\textit{sound}] (\textit{metis\_facts})
\postw
where \textit{metis\_facts} is the list of facts appearing in the suggested
-Metis call. The automatic provers should be able to re-find the proof very
-quickly if it is sound, and the \textit{type\_sys} $=$ \textit{poly\_tags}
-option (\S\ref{problem-encoding}) ensures that no unsound proofs are found.
-
-The \textit{full\_types} option (\S\ref{problem-encoding}) can also be used
-here, but it is unsound in extremely rare degenerate cases such as the
-following:
-
-\prew
-\textbf{lemma} ``$\forall x\> y\Colon{'}\!a.\ x = y \,\Longrightarrow \exists f\> g\Colon\mathit{nat} \Rightarrow {'}\!a.\ f \not= g$'' \\
-\textbf{sledgehammer} [\textit{full\_types}] (\textit{nat.distinct\/}(1))
-\postw
+Metis call. The automatic provers should be able to re-find the proof quickly if
+it is sound, and the \textit{sound} option (\S\ref{problem-encoding}) ensures
+that no unsound proofs are found.
\point{Which facts are passed to the automatic provers?}
@@ -456,7 +439,7 @@
Sledgehammer is good at finding short proofs combining a handful of existing
lemmas. If you are looking for longer proofs, you must typically restrict the
number of facts, by setting the \textit{max\_relevant} option
-(\S\ref{relevance-filter}) to, say, 50 or 100.
+(\S\ref{relevance-filter}) to, say, 25 or 50.
You can also influence which facts are actually selected in a number of ways. If
you simply want to ensure that a fact is included, you can specify it using the
@@ -654,7 +637,7 @@
enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
General. For automatic runs, only the first prover set using \textit{provers}
(\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
-\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{full\_types}
+\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{sound}
(\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})
and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout}
(\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof
@@ -890,14 +873,6 @@
\label{problem-encoding}
\begin{enum}
-\opfalse{full\_types}{partial\_types}
-Specifies whether a type-sound encoding should be used when translating
-higher-order types to untyped first-order logic. Enabling this option virtually
-prevents the discovery of type-incorrect proofs, but it can slow down the ATP
-slightly. This option is implicitly enabled for automatic runs. For historical
-reasons, the default value of this option can be overridden using the option
-``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General.
-
\opdefault{type\_sys}{string}{smart}
Specifies the type system to use in ATP problems. Some of the type systems are
unsound, meaning that they can give rise to spurious proofs (unreconstructible
@@ -960,7 +935,8 @@
notably infinite types. (For \textit{simple}, 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
-``\textit{\_query}'' suffix.
+``\textit{\_query}'' suffix. If the \emph{sound} option is enabled, these
+encodings are fully sound.
\item[$\bullet$]
\textbf{%
@@ -977,9 +953,8 @@
\textit{metis} proof method, the exclamation mark is replaced by a
``\textit{\_bang}'' suffix.
-\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
-uses a sound or virtually sound encoding; otherwise, uses any encoding. The actual
-encoding used depends on the ATP and should be the most efficient for that ATP.
+\item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
+the ATP and should be the most efficient virtually sound encoding for that ATP.
\end{enum}
In addition, all the \textit{preds} and \textit{tags} type systems are available
@@ -994,6 +969,11 @@
\nopagebreak
{\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
+
+\opfalse{sound}{unsound}
+Specifies whether Sledgehammer should run in its fully sound mode. In that mode,
+quasi-sound type encodings are made fully sound, at the cost of some (usually
+needless) clutter.
\end{enum}
\subsection{Relevance Filter}
--- a/doc-src/manual.bib Mon Jun 27 22:23:44 2011 +0200
+++ b/doc-src/manual.bib Mon Jun 27 22:44:44 2011 +0200
@@ -822,6 +822,12 @@
month = "Feb.",
year = 2010}
+@book{loveland-78,
+ author = "D. W. Loveland",
+ title = "Automated Theorem Proving: A Logical Basis",
+ year = 1978,
+ publisher = "North-Holland Publishing Co."}
+
@InProceedings{lowe-fdr,
author = {Gavin Lowe},
title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
--- a/src/HOL/Inductive.thy Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Inductive.thy Mon Jun 27 22:44:44 2011 +0200
@@ -297,7 +297,7 @@
let
(* FIXME proper name context!? *)
val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
- val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
+ val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr_permissive ctxt [x, cs];
in lambda x ft end
in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
*}
--- a/src/HOL/List.thy Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/List.thy Mon Jun 27 22:44:44 2011 +0200
@@ -391,7 +391,7 @@
Syntax.const @{syntax_const "_case1"} $
Syntax.const @{const_syntax dummy_pattern} $ NilC;
val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
- val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
+ val ft = Datatype_Case.case_tr false Datatype.info_of_constr_permissive ctxt [x, cs];
in lambda x ft end;
fun abs_tr ctxt (p as Free (s, T)) e opti =
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 27 22:44:44 2011 +0200
@@ -8,7 +8,6 @@
val proverK = "prover"
val prover_timeoutK = "prover_timeout"
val keepK = "keep"
-val full_typesK = "full_types"
val type_sysK = "type_sys"
val slicingK = "slicing"
val e_weight_methodK = "e_weight_method"
@@ -630,8 +629,6 @@
end
fun invoke args =
- let
- val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK
- in Mirabelle.register (init, sledgehammer_action args, done) end
+ Mirabelle.register (init, sledgehammer_action args, done)
end
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 27 22:44:44 2011 +0200
@@ -23,8 +23,12 @@
prem_kind : formula_kind,
formats : format list,
best_slices :
- Proof.context -> (real * (bool * (int * string list * string))) list}
+ Proof.context -> (real * (bool * (int * string * string))) list}
+ val e_smartN : string
+ val e_autoN : string
+ val e_fun_weightN : string
+ val e_sym_offset_weightN : string
val e_weight_method : string Config.T
val e_default_fun_weight : real Config.T
val e_fun_weight_base : real Config.T
@@ -48,7 +52,7 @@
val remote_atp :
string -> string -> string list -> (string * string) list
-> (failure * string) list -> formula_kind -> formula_kind -> format list
- -> (Proof.context -> int * string list) -> string * atp_config
+ -> (Proof.context -> int * string) -> 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,19 +81,19 @@
prem_kind : formula_kind,
formats : format list,
best_slices :
- Proof.context -> (real * (bool * (int * string list * string))) list}
+ Proof.context -> (real * (bool * (int * string * string))) list}
(* "best_slices" must be found empirically, taking a wholistic approach since
the ATPs are run in parallel. The "real" components give the faction of the
- time available given to the slice; these should add up to 1.0. The "bool"
+ time available given to the slice and should add up to 1.0. The "bool"
component indicates whether the slice's strategy is complete; the "int", the
- preferred number of facts to pass; the "string list", the preferred type
- systems, which should be of the form [sound] or [unsound, sound], where
- "sound" is a sound type system and "unsound" is an unsound one.
+ preferred number of facts to pass; the first "string", the preferred type
+ system (which should be sound or quasi-sound); the second "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
- time available if the other slices fail early and also because it is used for
- remote provers and if slicing is disabled. *)
+ time available if the other slices fail early and also because it is used if
+ slicing is disabled (e.g., by the minimizer). *)
val known_perl_failures =
[(CantConnect, "HTTP error"),
@@ -193,10 +197,9 @@
{exec = ("E_HOME", "eproof"),
required_execs = [],
arguments =
- fn ctxt => fn full_proof => fn method => fn timeout => fn weights =>
+ fn ctxt => fn _ => fn method => fn timeout => fn weights =>
"--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
- " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout) ^
- (if full_proof orelse is_old_e_version () then "" else " --trim"),
+ " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout),
proof_delims = tstp_proof_delims,
known_failures =
[(Unprovable, "SZS status: CounterSatisfiable"),
@@ -214,11 +217,11 @@
let val method = effective_e_weight_method ctxt in
(* FUDGE *)
if method = e_smartN then
- [(0.333, (true, (500, ["mangled_tags?"], e_fun_weightN))),
- (0.334, (true, (50, ["mangled_preds?"], e_fun_weightN))),
- (0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN)))]
+ [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))),
+ (0.334, (true, (50, "mangled_preds?", e_fun_weightN))),
+ (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
else
- [(1.0, (true, (500, ["mangled_tags?"], method)))]
+ [(1.0, (true, (500, "mangled_tags?", method)))]
end}
val e = (eN, e_config)
@@ -234,7 +237,7 @@
val spass_config : atp_config =
{exec = ("ISABELLE_ATP", "scripts/spass"),
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
- arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
+ arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
\-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
|> sos = sosN ? prefix "-SOS=1 ",
@@ -253,9 +256,9 @@
formats = [FOF],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, ["mangled_tags"], sosN))),
- (0.333, (false, (300, ["poly_tags?"], sosN))),
- (0.334, (true, (50, ["mangled_tags?"], no_sosN)))]
+ [(0.333, (false, (150, "mangled_tags", sosN))),
+ (0.333, (false, (300, "poly_tags?", sosN))),
+ (0.334, (true, (50, "mangled_tags?", no_sosN)))]
|> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -270,7 +273,7 @@
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
- arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
+ arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
"--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
" --thanks \"Andrei and Krystof\" --input_file"
|> sos = sosN ? prefix "--sos on ",
@@ -294,9 +297,9 @@
formats = [FOF],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, ["poly_preds"], sosN))),
- (0.334, (true, (50, ["mangled_preds?"], no_sosN))),
- (0.333, (false, (500, ["mangled_tags?"], sosN)))]
+ [(0.333, (false, (150, "poly_preds", sosN))),
+ (0.334, (true, (50, "mangled_preds?", no_sosN))),
+ (0.333, (false, (500, "mangled_tags?", sosN)))]
|> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -322,7 +325,7 @@
formats = [FOF],
best_slices =
(* FUDGE (FIXME) *)
- K [(1.0, (false, (250, [], "")))]}
+ K [(1.0, (false, (250, "mangled_preds?", "")))]}
val z3_atp = (z3_atpN, z3_atp_config)
@@ -382,8 +385,8 @@
prem_kind = prem_kind,
formats = formats,
best_slices = fn ctxt =>
- let val (max_relevant, type_syss) = best_slice ctxt in
- [(1.0, (false, (max_relevant, type_syss, "")))]
+ let val (max_relevant, type_sys) = best_slice ctxt in
+ [(1.0, (false, (max_relevant, type_sys, "")))]
end}
fun remotify_config system_name system_versions best_slice
@@ -403,36 +406,35 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
- (K (750, ["mangled_tags?"]) (* FUDGE *))
+ (K (750, "mangled_tags?") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
- (K (200, ["mangled_preds?"]) (* FUDGE *))
+ (K (200, "mangled_preds?") (* FUDGE *))
val remote_z3_atp =
- remotify_atp z3_atp "Z3" ["2.18"] (K (250, ["mangled_preds?"]) (* FUDGE *))
+ remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *))
val remote_leo2 =
remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
- (K (100, ["simple"]) (* FUDGE *))
+ (K (100, "simple") (* FUDGE *))
val remote_satallax =
remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
- (K (64, ["simple"]) (* FUDGE *))
+ (K (64, "simple") (* FUDGE *))
val remote_sine_e =
- remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
- Axiom Conjecture [FOF]
- (K (500, ["mangled_preds?"]) (* FUDGE *))
+ remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
+ Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
- [TFF, FOF] (K (100, ["simple"]) (* FUDGE *))
+ [TFF, FOF] (K (100, "simple") (* FUDGE *))
val remote_tofof_e =
remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
- Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *))
+ Axiom Hypothesis [TFF] (K (150, "simple") (* 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 [CNF_UEQ]
- (K (50, ["mangled_tags?"]) (* FUDGE *))
+ (K (50, "mangled_tags?") (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 27 22:44:44 2011 +0200
@@ -87,7 +87,7 @@
val helper_table : ((string * bool) * thm list) list
val factsN : string
val prepare_atp_problem :
- Proof.context -> format -> formula_kind -> formula_kind -> type_sys
+ Proof.context -> format -> formula_kind -> formula_kind -> type_sys -> bool
-> bool -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
@@ -991,7 +991,8 @@
fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
| should_encode_type _ _ All_Types _ = true
- | should_encode_type ctxt _ Fin_Nonmono_Types T = is_type_surely_finite ctxt T
+ | should_encode_type ctxt _ Fin_Nonmono_Types T =
+ is_type_surely_finite ctxt false T
| should_encode_type _ _ _ _ = false
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
@@ -1617,26 +1618,27 @@
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
out with monotonicity" paper presented at CADE 2011. *)
-fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
- | add_combterm_nonmonotonic_types ctxt level locality _
+fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
+ | add_combterm_nonmonotonic_types ctxt level sound locality _
(CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
tm2)) =
(is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
(case level of
Noninf_Nonmono_Types =>
not (is_locality_global locality) orelse
- not (is_type_surely_infinite ctxt T)
- | Fin_Nonmono_Types => is_type_surely_finite ctxt T
+ not (is_type_surely_infinite ctxt sound T)
+ | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
| _ => true)) ? insert_type ctxt I (deep_freeze_type T)
- | add_combterm_nonmonotonic_types _ _ _ _ _ = I
-fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...}
- : translated_formula) =
+ | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I
+fun add_fact_nonmonotonic_types ctxt level sound
+ ({kind, locality, combformula, ...} : translated_formula) =
formula_fold (SOME (kind <> Conjecture))
- (add_combterm_nonmonotonic_types ctxt level locality) combformula
-fun nonmonotonic_types_for_facts ctxt type_sys facts =
+ (add_combterm_nonmonotonic_types ctxt level sound locality)
+ combformula
+fun nonmonotonic_types_for_facts ctxt type_sys sound facts =
let val level = level_of_type_sys type_sys in
if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
- [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
+ [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
(* We must add "bool" in case the helper "True_or_False" is added
later. In addition, several places in the code rely on the list of
nonmonotonic types not being empty. *)
@@ -1817,7 +1819,7 @@
val explicit_apply = NONE (* for experimental purposes *)
-fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
+fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys sound
exporter readable_names preproc hyp_ts concl_t facts =
let
val (format, type_sys) = choose_format [format] type_sys
@@ -1825,7 +1827,8 @@
translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
facts
val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
- val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
+ val nonmono_Ts =
+ conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys sound
val repair = repair_fact ctxt format type_sys sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
val repaired_sym_tab =
--- a/src/HOL/Tools/ATP/atp_util.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Mon Jun 27 22:44:44 2011 +0200
@@ -21,8 +21,8 @@
val typ_of_dtyp :
Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
-> typ
- val is_type_surely_finite : Proof.context -> typ -> bool
- val is_type_surely_infinite : Proof.context -> typ -> bool
+ val is_type_surely_finite : Proof.context -> bool -> typ -> bool
+ val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
val transform_elim_prop : term -> term
@@ -136,7 +136,7 @@
0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
cardinality 2 or more. The specified default cardinality is returned if the
cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt default_card T =
+fun tiny_card_of_type ctxt sound default_card T =
let
val thy = Proof_Context.theory_of ctxt
val max = 2 (* 1 would be too small for the "fun" case *)
@@ -181,19 +181,20 @@
(Logic.varifyT_global abs_type) T
(Logic.varifyT_global rep_type)
|> aux true avoid of
- 0 => 0
+ 0 => if sound then default_card else 0
| 1 => 1
| _ => default_card)
| [] => default_card)
(* Very slightly unsound: Type variables are assumed not to be
constrained to cardinality 1. (In practice, the user would most
likely have used "unit" directly anyway.) *)
- | TFree _ => if default_card = 1 then 2 else default_card
+ | TFree _ =>
+ if default_card = 1 andalso not sound then 2 else default_card
| TVar _ => default_card
in Int.min (max, aux false [] T) end
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
-fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
+fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
+fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
fun monomorphic_term subst =
map_types (map_type_tvar (fn v =>
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Jun 27 22:44:44 2011 +0200
@@ -23,6 +23,7 @@
val get_constrs : theory -> string -> (string * typ) list option
val get_all : theory -> info Symtab.table
val info_of_constr : theory -> string * typ -> info option
+ val info_of_constr_permissive : theory -> string * typ -> info option
val info_of_case : theory -> string -> info option
val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
val make_case : Proof.context -> Datatype_Case.config -> string list -> term ->
@@ -70,6 +71,15 @@
fun info_of_constr thy (c, T) =
let
val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
+ in
+ case body_type T of
+ Type (tyco, _) => AList.lookup (op =) tab tyco
+ | _ => NONE
+ end;
+
+fun info_of_constr_permissive thy (c, T) =
+ let
+ val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
val default =
if null tab then NONE
@@ -216,7 +226,7 @@
(* translation rules for case *)
fun make_case ctxt = Datatype_Case.make_case
- (info_of_constr (Proof_Context.theory_of ctxt)) ctxt;
+ (info_of_constr_permissive (Proof_Context.theory_of ctxt)) ctxt;
fun strip_case ctxt = Datatype_Case.strip_case
(info_of_case (Proof_Context.theory_of ctxt));
@@ -230,7 +240,7 @@
val trfun_setup =
Sign.add_advanced_trfuns ([],
- [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr)],
+ [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr_permissive)],
[], []);
--- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 27 22:44:44 2011 +0200
@@ -196,8 +196,8 @@
tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false false
- [] @{prop False} props
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false
+ false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jun 27 22:44:44 2011 +0200
@@ -776,9 +776,9 @@
fun is_metastrange_theorem th =
case head_of (concl_of th) of
- Const (a, _) => (a <> @{const_name Trueprop} andalso
- a <> @{const_name "=="})
- | _ => false
+ Const (s, _) => (s <> @{const_name Trueprop} andalso
+ s <> @{const_name "=="})
+ | _ => false
fun is_that_fact th =
String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
@@ -791,12 +791,14 @@
(**** Predicates to detect unwanted facts (prolific or likely to cause
unsoundness) ****)
-fun is_theorem_bad_for_atps thm =
- let val t = prop_of thm in
- is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
- exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
- is_metastrange_theorem thm orelse is_that_fact thm
- end
+fun is_theorem_bad_for_atps exporter thm =
+ is_metastrange_theorem thm orelse
+ (not exporter andalso
+ let val t = prop_of thm in
+ is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
+ exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
+ is_that_fact thm
+ end)
fun meta_equify (@{const Trueprop}
$ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) =
@@ -822,7 +824,7 @@
|> add Simp normalize_simp_prop snd simps
end
-fun all_facts ctxt reserved really_all add_ths chained_ths =
+fun all_facts ctxt reserved exporter add_ths chained_ths =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -852,7 +854,7 @@
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
fun add_facts global foldx facts =
foldx (fn (name0, ths) =>
- if not really_all andalso name0 <> "" andalso
+ if not exporter andalso name0 <> "" andalso
forall (not o member Thm.eq_thm_prop add_ths) ths andalso
(Facts.is_concealed facts name0 orelse
(not (Config.get ctxt ignore_no_atp) andalso
@@ -874,9 +876,8 @@
pair 1
#> fold (fn th => fn (j, (multis, unis)) =>
(j + 1,
- if not really_all andalso
- not (member Thm.eq_thm_prop add_ths th) andalso
- is_theorem_bad_for_atps th then
+ if not (member Thm.eq_thm_prop add_ths th) andalso
+ is_theorem_bad_for_atps exporter th then
(multis, unis)
else
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 27 22:44:44 2011 +0200
@@ -12,7 +12,6 @@
val auto : bool Unsynchronized.ref
val provers : string Unsynchronized.ref
val timeout : int Unsynchronized.ref
- val full_types : bool Unsynchronized.ref
val default_params : Proof.context -> (string * string) list -> params
val setup : theory -> theory
end;
@@ -65,7 +64,6 @@
val provers = Unsynchronized.ref ""
val timeout = Unsynchronized.ref 30
-val full_types = Unsynchronized.ref false
val _ =
ProofGeneralPgip.add_preference Preferences.category_proof
@@ -79,11 +77,6 @@
"Sledgehammer: Time Limit"
"ATPs will be interrupted after this time (in seconds)")
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.bool_pref full_types
- "Sledgehammer: Full Types" "ATPs will use full type information")
-
type raw_param = string * string list
val default_default_params =
@@ -92,6 +85,7 @@
("overlord", "false"),
("blocking", "false"),
("type_sys", "smart"),
+ ("sound", "false"),
("relevance_thresholds", "0.45 0.85"),
("max_relevant", "smart"),
("max_mono_iters", "3"),
@@ -108,16 +102,16 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("non_blocking", "blocking"),
- ("partial_types", "full_types"),
+ ("unsound", "sound"),
("no_isar_proof", "isar_proof"),
("no_slicing", "slicing")]
val params_for_minimize =
- ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
+ ["debug", "verbose", "overlord", "type_sys", "sound", "max_mono_iters",
"max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
"preplay_timeout"]
-val property_dependent_params = ["provers", "full_types", "timeout"]
+val property_dependent_params = ["provers", "timeout"]
fun is_known_raw_param s =
AList.defined (op =) default_default_params s orelse
@@ -130,7 +124,8 @@
ss as _ :: _ => forall (is_prover_supported ctxt) ss
| _ => false
-(* Secret feature: "provers =" and "type_sys =" can be left out. *)
+(* "provers =" and "type_sys =" can be left out. The latter is a secret
+ feature. *)
fun check_and_repair_raw_param ctxt (name, value) =
if is_known_raw_param name then
(name, value)
@@ -218,7 +213,6 @@
[("provers", [case !provers of
"" => default_provers_param_value ctxt
| s => s]),
- ("full_types", [if !full_types then "true" else "false"]),
("timeout", let val timeout = !timeout in
[if timeout <= 0 then "none"
else string_of_int timeout]
@@ -272,10 +266,11 @@
|> mode = Auto_Try ? single o hd
val type_sys =
if mode = Auto_Try then
- Smart_Type_Sys true
+ NONE
else case lookup_string "type_sys" of
- "smart" => Smart_Type_Sys (mode = Try orelse lookup_bool "full_types")
- | s => Dumb_Type_Sys (type_sys_from_string s)
+ "smart" => NONE
+ | s => SOME (type_sys_from_string s)
+ val sound = mode = Auto_Try orelse lookup_bool "sound"
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"
@@ -294,9 +289,9 @@
provers = provers, relevance_thresholds = relevance_thresholds,
max_relevant = max_relevant, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = expect}
+ sound = sound, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, slicing = slicing,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jun 27 22:44:44 2011 +0200
@@ -59,7 +59,7 @@
val {goal, ...} = Proof.goal state
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
- provers = provers, type_sys = type_sys,
+ provers = provers, type_sys = type_sys, sound = true,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
@@ -167,18 +167,17 @@
Int.min (msecs, Time.toMilliseconds time + slack_msecs)
|> Time.fromMilliseconds
val facts = filter_used_facts used_facts facts
- val (min_thms, {preplay, message, message_tail, ...}) =
+ val (min_facts, {preplay, message, message_tail, ...}) =
if length facts >= Config.get ctxt binary_min_facts then
binary_minimize (do_test new_timeout) facts
else
sublinear_minimize (do_test new_timeout) facts ([], result)
- val n = length min_thms
val _ = print silent (fn () => cat_lines
- ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
- (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
+ ["Minimized to " ^ n_facts used_facts] ^
+ (case length (filter (curry (op =) Chained o snd o fst) min_facts) of
0 => ""
- | n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
- in (SOME min_thms, (preplay, message, message_tail)) end
+ | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
+ in (SOME min_facts, (preplay, message, message_tail)) end
| {outcome = SOME TimedOut, preplay, ...} =>
(NONE,
(preplay,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 27 22:44:44 2011 +0200
@@ -18,17 +18,14 @@
datatype mode = Auto_Try | Try | Normal | Minimize
- datatype rich_type_sys =
- Dumb_Type_Sys of type_sys |
- Smart_Type_Sys of bool
-
type params =
{debug: bool,
verbose: bool,
overlord: bool,
blocking: bool,
provers: string list,
- type_sys: rich_type_sys,
+ type_sys: type_sys option,
+ sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -286,17 +283,14 @@
(** problems, results, ATPs, etc. **)
-datatype rich_type_sys =
- Dumb_Type_Sys of type_sys |
- Smart_Type_Sys of bool
-
type params =
{debug: bool,
verbose: bool,
overlord: bool,
blocking: bool,
provers: string list,
- type_sys: rich_type_sys,
+ type_sys: type_sys option,
+ sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -500,7 +494,7 @@
are omitted. *)
fun is_dangerous_prop ctxt =
transform_elim_prop
- #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
+ #> (has_bound_or_var_of_type (is_type_surely_finite ctxt false) orf
is_exhaustive_finite)
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
@@ -510,16 +504,11 @@
them each time. *)
val atp_important_message_keep_quotient = 10
-val fallback_best_type_syss =
- [Preds (Mangled_Monomorphic, Noninf_Nonmono_Types, Lightweight)]
-
-fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
- choose_format formats type_sys
- | choose_format_and_type_sys best_type_syss formats
- (Smart_Type_Sys full_types) =
- map type_sys_from_string best_type_syss @ fallback_best_type_syss
- |> find_first (if full_types then is_type_sys_virtually_sound else K true)
- |> the |> choose_format formats
+fun choose_format_and_type_sys best_type_sys formats type_sys_opt =
+ (case type_sys_opt of
+ SOME ts => ts
+ | NONE => type_sys_from_string best_type_sys)
+ |> choose_format formats
val metis_minimize_max_time = seconds 2.0
@@ -541,9 +530,9 @@
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
- ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
- max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
- timeout, preplay_timeout, ...} : params)
+ ({debug, verbose, overlord, type_sys, sound, max_relevant,
+ max_mono_iters, max_new_mono_instances, isar_proof,
+ isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
minimize_command
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
@@ -609,14 +598,14 @@
|> maps (fn (name, rths) => map (pair name o snd) rths)
end
fun run_slice (slice, (time_frac, (complete,
- (best_max_relevant, best_type_syss, extra))))
+ (best_max_relevant, best_type_sys, extra))))
time_left =
let
val num_facts =
length facts |> is_none max_relevant
? Integer.min best_max_relevant
val (format, type_sys) =
- choose_format_and_type_sys best_type_syss formats type_sys
+ choose_format_and_type_sys best_type_sys formats type_sys
val fairly_sound = is_type_sys_fairly_sound type_sys
val facts =
facts |> map untranslated_fact
@@ -646,8 +635,8 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_sys false (Config.get ctxt atp_readable_names) true
- hyp_ts concl_t facts
+ type_sys sound false (Config.get ctxt atp_readable_names)
+ true hyp_ts concl_t facts
fun weights () = atp_problem_weights atp_problem
val full_proof = debug orelse isar_proof
val core =
@@ -749,6 +738,10 @@
facts |> map untranslated_fact |> filter_used_facts used_facts
|> map snd
in
+ (if mode = Minimize then
+ Output.urgent_message "Preplaying proof..."
+ else
+ ());
play_one_line_proof debug preplay_timeout used_ths state subgoal
metis_reconstructors
end,
--- a/src/HOL/ex/atp_export.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Mon Jun 27 22:44:44 2011 +0200
@@ -21,12 +21,16 @@
open ATP_Problem
open ATP_Translate
+open ATP_Proof
+open ATP_Systems
val fact_name_of = prefix fact_prefix o ascii_of
fun facts_of thy =
Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
true [] []
+ |> filter (curry (op =) @{typ bool} o fastype_of
+ o Object_Logic.atomize_term thy o prop_of o snd)
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
fixes that seem to be missing over there; or maybe the two code portions are
@@ -63,7 +67,7 @@
fun interesting_const_names ctxt =
let val thy = Proof_Context.theory_of ctxt in
Sledgehammer_Filter.const_names_in_fact thy
- (Sledgehammer_Provers.is_built_in_const_for_prover ctxt ATP_Systems.eN)
+ (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN)
end
fun generate_tptp_graph_file_for_theory ctxt thy file_name =
@@ -105,6 +109,38 @@
fun ident_of_problem_line (Decl (ident, _, _)) = ident
| ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
+fun run_some_atp ctxt problem =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val prob_file = Path.explode "/tmp/prob.tptp"
+ val {exec, arguments, proof_delims, known_failures, ...} =
+ get_atp thy spassN
+ val _ = problem |> tptp_lines_for_atp_problem FOF
+ |> File.write_list prob_file
+ val command =
+ File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
+ " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
+ File.shell_path prob_file
+ in
+ TimeLimit.timeLimit (seconds 0.3) bash_output command
+ |> fst
+ |> extract_tstplike_proof_and_outcome false true proof_delims
+ known_failures
+ |> snd
+ end
+ handle TimeLimit.TimeOut => SOME TimedOut
+
+val likely_tautology_prefixes =
+ [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}]
+ |> map (fact_name_of o Context.theory_name)
+
+fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) =
+ exists (fn prefix => String.isPrefix prefix ident)
+ likely_tautology_prefixes andalso
+ is_none (run_some_atp ctxt
+ [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])])
+ | is_problem_line_tautology _ _ = false
+
structure String_Graph = Graph(type key = string val ord = string_ord);
fun order_facts ord = sort (ord o pairself ident_of_problem_line)
@@ -119,18 +155,20 @@
val type_sys = type_sys |> type_sys_from_string
val path = file_name |> Path.explode
val _ = File.write path ""
- val facts0 = facts_of thy
- val facts =
- facts0 |> map (fn ((_, loc), th) =>
- ((Thm.get_name_hint th, loc), prop_of th))
+ val facts = facts_of thy
val (atp_problem, _, _, _, _, _, _) =
- prepare_atp_problem ctxt format Axiom Axiom type_sys true false true []
- @{prop False} facts
- val all_names = facts0 |> map (Thm.get_name_hint o snd)
+ facts
+ |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
+ |> prepare_atp_problem ctxt format Axiom Axiom type_sys true true false
+ true [] @{prop False}
+ val atp_problem =
+ atp_problem
+ |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
+ val all_names = facts |> map (Thm.get_name_hint o snd)
val infers =
- facts0 |> map (fn (_, th) =>
- (fact_name_of (Thm.get_name_hint th),
- theorems_mentioned_in_proof_term (SOME all_names) th))
+ facts |> map (fn (_, th) =>
+ (fact_name_of (Thm.get_name_hint th),
+ theorems_mentioned_in_proof_term (SOME all_names) th))
val all_atp_problem_names =
atp_problem |> maps (map ident_of_problem_line o snd)
val infers =
@@ -140,7 +178,8 @@
String_Graph.empty
|> fold (String_Graph.new_node o rpair ()) all_atp_problem_names
|> fold (fn (to, froms) =>
- fold (fn from => String_Graph.add_edge (from, to)) froms) infers
+ fold (fn from => String_Graph.add_edge (from, to)) froms)
+ infers
|> String_Graph.topological_order
val order_tab =
Symtab.empty
--- a/src/Provers/Arith/fast_lin_arith.ML Mon Jun 27 22:23:44 2011 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Jun 27 22:44:44 2011 +0200
@@ -633,7 +633,7 @@
handle NoEx => NONE
in
case ex of
- SOME s => (warning "Linear arithmetic failed - see trace for a counterexample."; tracing s)
+ SOME s => (warning "Linear arithmetic failed - see trace for a (potentially spurious) counterexample."; tracing s)
| NONE => warning "Linear arithmetic failed"
end;