--- a/NEWS Fri Jul 20 23:37:54 2012 +0200
+++ b/NEWS Fri Jul 20 23:38:15 2012 +0200
@@ -46,6 +46,8 @@
* Sledgehammer:
+ - Added MaSh relevance filter based on machine-learning; see the
+ Sledgehammer manual for details.
- Rationalized type encodings ("type_enc" option).
- Renamed options:
max_relevant ~> max_facts
--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Jul 20 23:37:54 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Jul 20 23:38:15 2012 +0200
@@ -106,10 +106,10 @@
SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire
\cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are
run either locally or remotely via the System\-On\-TPTP web service
-\cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is
-used by default, and you can tell Sledgehammer to try Alt-Ergo \cite{alt-ergo},
-CVC3 \cite{cvc3}, and Yices \cite{yices} as well; these are run either locally
-or (for CVC3 and Z3) on a server at the TU M\"unchen.
+\cite{sutcliffe-2000}. In addition to the ATPs, a selection of the SMT solvers
+CVC3 \cite{cvc3}, Yices \cite{yices}, and Z3 \cite{z3} are run by default, and
+you can tell Sledgehammer to try Alt-Ergo \cite{alt-ergo} as well; these are run
+either locally or (for CVC3 and Z3) on a server at the TU M\"unchen.
The problem passed to the automatic provers consists of your current goal
together with a heuristic selection of hundreds of facts (theorems) from the
@@ -152,7 +152,7 @@
\section{Installation}
\label{installation}
-Sledgehammer is part of Isabelle, so you don't need to install it. However, it
+Sledgehammer is part of Isabelle, so you do not need to install it. However, it
relies on third-party automatic provers (ATPs and SMT solvers).
Among the ATPs, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
@@ -161,11 +161,10 @@
\cite{sutcliffe-2000}. If you want better performance, you should at least
install E and SPASS locally.
-Among the SMT solvers, Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and
-CVC3 and Z3 can be run remotely on a TU M\"unchen server. If you want better
-performance and get the ability to replay proofs that rely on the \emph{smt}
-proof method without an Internet connection, you should at least install Z3
-locally.
+The SMT solvers Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and CVC3 and
+Z3 can be run remotely on a TU M\"unchen server. If you want better performance
+and get the ability to replay proofs that rely on the \emph{smt} proof method
+without an Internet connection, you should at least have Z3 locally installed.
There are three main ways to install automatic provers on your machine:
@@ -220,12 +219,16 @@
\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
\texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
-the executable, \emph{including the file name}. Sledgehammer has been tested
-with Alt-Ergo 0.93, CVC3 2.2 and 2.4.1, Yices 1.0.28 and 1.0.33, and Z3 3.0,
-3.1, 3.2, and 4.0. Since the SMT solvers' output formats are somewhat unstable,
-other versions of the solvers might not work well with Sledgehammer. Ideally,
-also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or
-\texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.0'').
+the executable, \emph{including the file name};
+for Alt-Ergo, set the
+environment variable \texttt{WHY3\_HOME} to the directory that contains the
+\texttt{why3} executable.
+Sledgehammer has been tested with Alt-Ergo 0.93 and 0.94, CVC3 2.2 and 2.4.1,
+Yices 1.0.28 and 1.0.33, and Z3 3.0 to 4.0. Since the SMT solvers' output
+formats are somewhat unstable, other versions of the solvers might not work well
+with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION},
+\texttt{YICES\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number
+(e.g., ``4.0'').
\end{enum}
\end{sloppy}
@@ -301,10 +304,9 @@
\textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
where the goal's conclusion is a (universally quantified) equation.
-For each successful prover, Sledgehammer gives a one-liner proof that uses
-the \textit{metis} or \textit{smt} proof method. Approximate timings are shown
-in parentheses, indicating how fast the call is. You can click the proof to
-insert it into the theory text.
+For each successful prover, Sledgehammer gives a one-liner \textit{metis} or
+\textit{smt} method call. Rough timings are shown in parentheses, indicating how
+fast the call is. You can click the proof to insert it into the theory text.
In addition, you can ask Sledgehammer for an Isar text proof by passing the
\textit{isar\_proof} option (\S\ref{output-format}):
@@ -386,21 +388,41 @@
\label{frequently-asked-questions}
This sections answers frequently (and infrequently) asked questions about
-Sledgehammer. It is a good idea to skim over it now even if you don't have any
+Sledgehammer. It is a good idea to skim over it now even if you do not have any
questions at this stage. And if you have any further questions not listed here,
send them to the author at \authoremail.
\point{Which facts are passed to the automatic provers?}
-The relevance filter assigns a score to every available fact (lemma, theorem,
-definition, or axiom) based upon how many constants that fact shares with the
-conjecture. This process iterates to include facts relevant to those just
-accepted, but with a decay factor to ensure termination. The constants are
-weighted to give unusual ones greater significance. The relevance filter copes
-best when the conjecture contains some unusual constants; if all the constants
-are common, it is unable to discriminate among the hundreds of facts that are
-picked up. The relevance filter is also memoryless: It has no information about
-how many times a particular fact has been used in a proof, and it cannot learn.
+Sledgehammer heuristically selects a few hundred relevant lemmas from the
+currently loaded libraries. The component that performs this selection is
+called \emph{relevance filter}.
+
+\begin{enum}
+\item[\labelitemi]
+The traditional relevance filter, called \emph{MePo}
+(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact
+(lemma, theorem, definition, or axiom) based upon how many constants that fact
+shares with the conjecture. This process iterates to include facts relevant to
+those just accepted. The constants are weighted to give unusual ones greater
+significance. MePo copes best when the conjecture contains some unusual
+constants; if all the constants are common, it is unable to discriminate among
+the hundreds of facts that are picked up. The filter is also memoryless: It has
+no information about how many times a particular fact has been used in a proof,
+and it cannot learn.
+
+\item[\labelitemi]
+An experimental, memoryful alternative to MePo is \emph{MaSh}
+(\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It
+relies on an external tool called \texttt{mash} that applies machine learning to
+the problem of finding relevant facts.
+
+\item[\labelitemi] The \emph{Mesh} filter combines MePo and MaSh.
+\end{enum}
+
+The default is either MePo or Mesh, depending on whether \texttt{mash} is
+installed and what class of provers the target prover belongs to
+(\S\ref{relevance-filter}).
The number of facts included in a problem varies from prover to prover, since
some provers get overwhelmed more easily than others. You can show the number of
@@ -453,8 +475,8 @@
Since the steps are fairly small, \textit{metis} is more likely to be able to
replay them.
-\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It
-is usually stronger, but you need to either have Z3 available to replay the
+\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}.
+It is usually stronger, but you need to either have Z3 available to replay the
proofs, trust the SMT solver, or use certificates. See the documentation in the
\emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.
@@ -599,9 +621,10 @@
\point{Auto can solve it---why not Sledgehammer?}
Problems can be easy for \textit{auto} and difficult for automatic provers, but
-the reverse is also true, so don't be discouraged if your first attempts fail.
+the reverse is also true, so do not be discouraged if your first attempts fail.
Because the system refers to all theorems known to Isabelle, it is particularly
-suitable when your goal has a short proof from lemmas that you don't know about.
+suitable when your goal has a short proof from lemmas that you do not know
+about.
\point{Why are there so many options?}
@@ -659,6 +682,40 @@
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
\end{enum}
+In addition, the following subcommands provide fine control over machine
+learning with MaSh:
+
+\begin{enum}
+\item[\labelitemi] \textbf{\textit{unlearn}:} Resets MaSh, erasing any
+persistent state.
+
+\item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current
+theory to process all the available facts, learning from their Isabelle/Isar
+proofs. This happens automatically at Sledgehammer invocations if the
+\textit{learn} option (\S\ref{relevance-filter}) is enabled.
+
+\item[\labelitemi] \textbf{\textit{learn\_atp}:} Invokes MaSh on the current
+theory to process all the available facts, learning from ATP-generated proofs.
+The ATP to use and its timeout can be set using the
+\textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout}
+(\S\ref{timeouts}) options. It is recommended to perform learning using an
+efficient first-order ATP (such as E, SPASS, and Vampire) as opposed to a
+higher-order ATP or an SMT solver.
+
+\item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn}
+followed by \textit{learn\_isar}.
+
+\item[\labelitemi] \textbf{\textit{relearn\_atp}:} Same as \textit{unlearn}
+followed by \textit{learn\_atp}.
+
+\item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about
+currently running machine learners, including elapsed runtime and remaining
+time until timeout.
+
+\item[\labelitemi] \textbf{\textit{kill\_learners}:} Terminates all running
+machine learners.
+\end{enum}
+
Sledgehammer's behavior can be influenced by various \qty{options}, which can be
specified in brackets after the \textbf{sledgehammer} command. The
\qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
@@ -718,9 +775,9 @@
All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
For convenience, the following aliases are provided:
\begin{enum}
-\item[\labelitemi] \textbf{\textit{full\_types}:} Synonym for \textit{poly\_guards\_query}.
-\item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}.
-\item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}.
+\item[\labelitemi] \textbf{\textit{full\_types}:} Alias for \textit{poly\_guards\_query}.
+\item[\labelitemi] \textbf{\textit{partial\_types}:} Alias for \textit{poly\_args}.
+\item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}.
\end{enum}
\section{Option Reference}
@@ -916,12 +973,11 @@
with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
-the SMT module's \textit{smt\_solver} configuration option is set to), and (if
-appropriate) Waldmeister in parallel---either locally or remotely, depending on
-the number of processor cores available. For historical reasons, the default
-value of this option can be overridden using the option ``Sledgehammer:
-Provers'' in Proof General's ``Isabelle'' menu.
+By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
+Yices, Z3, and (if appropriate) Waldmeister in parallel---either locally or
+remotely, depending on the number of processor cores available. For historical
+reasons, the default value of this option can be overridden using the option
+``Sledgehammer: Provers'' in Proof General's ``Isabelle'' menu.
It is generally a good idea to run several provers in parallel. Running E,
SPASS, and Vampire for 5~seconds yields a similar success rate to running the
@@ -971,13 +1027,79 @@
Specifies whether Sledgehammer should put its temporary files in
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
debugging Sledgehammer but also unsafe if several instances of the tool are run
-simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
-safely remove them after Sledgehammer has run.
+simultaneously. The files are identified by the prefixes \texttt{prob\_} and
+\texttt{mash\_}; you may safely remove them after Sledgehammer has run.
\nopagebreak
{\small See also \textit{debug} (\S\ref{output-format}).}
\end{enum}
+\subsection{Relevance Filter}
+\label{relevance-filter}
+
+\begin{enum}
+\opdefault{fact\_filter}{string}{smart}
+Specifies the relevance filter to use. The following filters are available:
+
+\begin{enum}
+\item[\labelitemi] \textbf{\textit{mepo}:}
+The traditional memoryless MePo relevance filter.
+
+\item[\labelitemi] \textbf{\textit{mash}:}
+The memoryful MaSh machine learner. MaSh relies on the external program
+\texttt{mash}, which can be obtained from the author at \authoremail. To install
+it, set the environment variable \texttt{MASH\_HOME} to the directory that
+contains the \texttt{mash} executable.
+Persistent data is stored in the \texttt{\$ISABELLE\_HOME\_USER/mash} directory.
+
+\item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh.
+
+\item[\labelitemi] \textbf{\textit{smart}:} Use Mesh if \texttt{mash} is
+installed and the target prover is an ATP; otherwise, use MePo.
+\end{enum}
+
+\opdefault{max\_facts}{smart\_int}{smart}
+Specifies the maximum number of facts that may be returned by the relevance
+filter. If the option is set to \textit{smart}, it is set to a value that was
+empirically found to be appropriate for the prover. Typical values range between
+50 and 1000.
+
+\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85}
+Specifies the thresholds above which facts are considered relevant by the
+relevance filter. The first threshold is used for the first iteration of the
+relevance filter and the second threshold is used for the last iteration (if it
+is reached). The effective threshold is quadratically interpolated for the other
+iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
+are relevant and 1 only theorems that refer to previously seen constants.
+
+\optrue{learn}{dont\_learn}
+Specifies whether MaSh should be run automatically by Sledgehammer to learn the
+available theories (and hence provide more accurate results). Learning only
+takes place if \texttt{mash} is installed.
+
+\opdefault{max\_new\_mono\_instances}{int}{smart}
+Specifies the maximum number of monomorphic instances to generate beyond
+\textit{max\_facts}. The higher this limit is, the more monomorphic instances
+are potentially generated. Whether monomorphization takes place depends on the
+type encoding used. If the option is set to \textit{smart}, it is set to a value
+that was empirically found to be appropriate for the prover. For most provers,
+this value is 200.
+
+\nopagebreak
+{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
+
+\opdefault{max\_mono\_iters}{int}{smart}
+Specifies the maximum number of iterations for the monomorphization fixpoint
+construction. The higher this limit is, the more monomorphic instances are
+potentially generated. Whether monomorphization takes place depends on the
+type encoding used. If the option is set to \textit{smart}, it is set to a value
+that was empirically found to be appropriate for the prover. For most provers,
+this value is 3.
+
+\nopagebreak
+{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
+\end{enum}
+
\subsection{Problem Encoding}
\label{problem-encoding}
@@ -1143,47 +1265,6 @@
deliberately set to an unsound encoding.
\end{enum}
-\subsection{Relevance Filter}
-\label{relevance-filter}
-
-\begin{enum}
-\opdefault{max\_facts}{smart\_int}{smart}
-Specifies the maximum number of facts that may be returned by the relevance
-filter. If the option is set to \textit{smart}, it is set to a value that was
-empirically found to be appropriate for the prover. Typical values range between
-50 and 1000.
-
-\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85}
-Specifies the thresholds above which facts are considered relevant by the
-relevance filter. The first threshold is used for the first iteration of the
-relevance filter and the second threshold is used for the last iteration (if it
-is reached). The effective threshold is quadratically interpolated for the other
-iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
-are relevant and 1 only theorems that refer to previously seen constants.
-
-\opdefault{max\_new\_mono\_instances}{int}{smart}
-Specifies the maximum number of monomorphic instances to generate beyond
-\textit{max\_facts}. The higher this limit is, the more monomorphic instances
-are potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it is set to a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 200.
-
-\nopagebreak
-{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
-
-\opdefault{max\_mono\_iters}{int}{smart}
-Specifies the maximum number of iterations for the monomorphization fixpoint
-construction. The higher this limit is, the more monomorphic instances are
-potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it is set to a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 3.
-
-\nopagebreak
-{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
-\end{enum}
-
\subsection{Output Format}
\label{output-format}
--- a/src/HOL/IsaMakefile Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/IsaMakefile Fri Jul 20 23:38:15 2012 +0200
@@ -371,8 +371,8 @@
Tools/semiring_normalizer.ML \
Tools/Sledgehammer/async_manager.ML \
Tools/Sledgehammer/sledgehammer_fact.ML \
- Tools/Sledgehammer/sledgehammer_filter_iter.ML \
- Tools/Sledgehammer/sledgehammer_filter_mash.ML \
+ Tools/Sledgehammer/sledgehammer_mash.ML \
+ Tools/Sledgehammer/sledgehammer_mepo.ML \
Tools/Sledgehammer/sledgehammer_minimize.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_provers.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 20 23:38:15 2012 +0200
@@ -367,7 +367,7 @@
handle List.Empty => error "No ATP available."
fun get_prover name =
(name, Sledgehammer_Minimize.get_minimizing_prover ctxt
- Sledgehammer_Provers.Normal (K ()) name)
+ Sledgehammer_Provers.Normal (K (K ())) name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name
@@ -466,7 +466,7 @@
Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
+ |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
(the_default default_max_facts max_facts)
Sledgehammer_Fact.no_fact_override hyp_ts concl_t
val problem =
@@ -597,7 +597,7 @@
|> max_new_mono_instancesLST
|> max_mono_itersLST)
val minimize =
- Sledgehammer_Minimize.minimize_facts (K ()) prover_name params
+ Sledgehammer_Minimize.minimize_facts (K (K ())) prover_name params
true 1 (Sledgehammer_Util.subgoal_count st)
val _ = log separator
val (used_facts, (preplay, message, message_tail)) =
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jul 20 23:38:15 2012 +0200
@@ -133,7 +133,7 @@
Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
+ |> Sledgehammer_MePo.mepo_suggested_facts ctxt params
default_prover (the_default default_max_facts max_facts)
(SOME relevance_fudge) hyp_ts concl_t
|> map ((fn name => name ()) o fst o fst)
--- a/src/HOL/Sledgehammer.thy Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Jul 20 23:38:15 2012 +0200
@@ -14,8 +14,8 @@
"Tools/Sledgehammer/sledgehammer_fact.ML"
"Tools/Sledgehammer/sledgehammer_provers.ML"
"Tools/Sledgehammer/sledgehammer_minimize.ML"
- "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
- "Tools/Sledgehammer/sledgehammer_filter_mash.ML"
+ "Tools/Sledgehammer/sledgehammer_mepo.ML"
+ "Tools/Sledgehammer/sledgehammer_mash.ML"
"Tools/Sledgehammer/sledgehammer_run.ML"
"Tools/Sledgehammer/sledgehammer_isar.ML"
begin
--- a/src/HOL/TPTP/ATP_Theory_Export.thy Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy Fri Jul 20 23:38:15 2012 +0200
@@ -10,13 +10,13 @@
begin
ML {*
-open ATP_Problem;
-open ATP_Theory_Export;
+open ATP_Problem
+open ATP_Theory_Export
*}
ML {*
-val do_it = false; (* switch to "true" to generate the files *)
-val thy = @{theory List};
+val do_it = false (* switch to "true" to generate the files *)
+val thy = @{theory List}
val ctxt = @{context}
*}
--- a/src/HOL/TPTP/MaSh_Export.thy Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Fri Jul 20 23:38:15 2012 +0200
@@ -54,7 +54,7 @@
ML {*
if do_it then
- generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
+ generate_mepo_suggestions @{context} params thy 500 "/tmp/mash_mepo_suggestions"
else
()
*}
--- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 23:38:15 2012 +0200
@@ -66,7 +66,7 @@
val ord = effective_term_order ctxt atp
val _ = problem |> lines_for_atp_problem format ord (K [])
|> File.write_list prob_file
- val path = getenv (List.last (fst exec)) ^ "/" ^ snd exec
+ val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
File.shell_path (Path.explode path) ^
" " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^
@@ -114,8 +114,8 @@
end
fun all_non_tautological_facts_of thy css_table =
- Sledgehammer_Fact.all_facts_of thy css_table
- |> filter_out (Sledgehammer_Filter_MaSh.is_likely_tautology_or_too_meta o snd)
+ Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
+ |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
let
--- a/src/HOL/TPTP/mash_eval.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 20 23:38:15 2012 +0200
@@ -17,18 +17,18 @@
struct
open Sledgehammer_Fact
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
-val isarN = "Isar"
-val iterN = "Iter"
-val mashN = "MaSh"
-val meshN = "Mesh"
+val MePoN = "MePo"
+val MaShN = "MaSh"
+val MeshN = "Mesh"
+val IsarN = "Isar"
val max_facts_slack = 2
val all_names =
filter_out is_likely_tautology_or_too_meta
- #> map (rpair () o Thm.get_name_hint) #> Symtab.make
+ #> map (rpair () o nickname_of) #> Symtab.make
fun evaluate_mash_suggestions ctxt params thy file_name =
let
@@ -39,9 +39,9 @@
val path = file_name |> Path.explode
val lines = path |> File.read_lines
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of thy css_table
+ val facts = all_facts_of (Proof_Context.init_global thy) css_table
val all_names = all_names (facts |> map snd)
- val iter_ok = Unsynchronized.ref 0
+ val mepo_ok = Unsynchronized.ref 0
val mash_ok = Unsynchronized.ref 0
val mesh_ok = Unsynchronized.ref 0
val isar_ok = Unsynchronized.ref 0
@@ -70,41 +70,43 @@
let
val (name, suggs) = extract_query line
val th =
- case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of
+ case find_first (fn (_, th) => nickname_of th = name) facts of
SOME (_, th) => th
| NONE => error ("No fact called \"" ^ name ^ "\"")
val goal = goal_of_thm thy th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
- val isar_deps = isabelle_dependencies_of all_names th
+ val isar_deps = isar_dependencies_of all_names th |> these
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- val isar_facts = suggested_facts isar_deps facts
- val iter_facts =
- Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
- prover slack_max_facts NONE hyp_ts concl_t facts
- val mash_facts = facts |> suggested_facts suggs
- val mess = [(iter_facts, []), (mash_facts, [])]
+ val mepo_facts =
+ Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
+ slack_max_facts NONE hyp_ts concl_t facts
+ |> Sledgehammer_MePo.weight_mepo_facts
+ val mash_facts = suggested_facts suggs facts
+ val mess = [(mepo_facts, []), (mash_facts, [])]
val mesh_facts = mesh_facts slack_max_facts mess
- fun prove ok heading facts =
+ val isar_facts = suggested_facts (map (rpair 1.0) isar_deps) facts
+ fun prove ok heading get facts =
let
val facts =
- facts
- |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
- |> take (the max_facts)
+ facts |> map get
+ |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts
+ concl_t
+ |> take (the max_facts)
val res as {outcome, ...} =
run_prover_for_mash ctxt params prover facts goal
val _ = if is_none outcome then ok := !ok + 1 else ()
in str_of_res heading facts res end
- val iter_s = prove iter_ok iterN iter_facts
- val mash_s = prove mash_ok mashN mash_facts
- val mesh_s = prove mesh_ok meshN mesh_facts
- val isar_s = prove isar_ok isarN isar_facts
+ val mepo_s = prove mepo_ok MePoN fst mepo_facts
+ val mash_s = prove mash_ok MaShN fst mash_facts
+ val mesh_s = prove mesh_ok MeshN I mesh_facts
+ val isar_s = prove isar_ok IsarN fst isar_facts
in
- ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, mesh_s,
+ ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
isar_s]
|> cat_lines |> tracing
end
fun total_of heading ok n =
- " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
+ " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
Real.fmt (StringCvt.FIX (SOME 1))
(100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
@@ -119,10 +121,10 @@
tracing ("Options: " ^ commas options);
List.app solve_goal (tag_list 1 lines);
["Successes (of " ^ string_of_int n ^ " goals)",
- total_of iterN iter_ok n,
- total_of mashN mash_ok n,
- total_of meshN mesh_ok n,
- total_of isarN isar_ok n]
+ total_of MePoN mepo_ok n,
+ total_of MaShN mash_ok n,
+ total_of MeshN mesh_ok n,
+ total_of IsarN isar_ok n]
|> cat_lines |> tracing
end
--- a/src/HOL/TPTP/mash_export.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jul 20 23:38:15 2012 +0200
@@ -17,7 +17,7 @@
val generate_atp_dependencies :
Proof.context -> params -> theory -> bool -> string -> unit
val generate_commands : Proof.context -> string -> theory -> string -> unit
- val generate_iter_suggestions :
+ val generate_mepo_suggestions :
Proof.context -> params -> theory -> int -> string -> unit
end;
@@ -25,14 +25,14 @@
struct
open Sledgehammer_Fact
-open Sledgehammer_Filter_Iter
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MePo
+open Sledgehammer_MaSh
fun thy_map_from_facts ths =
ths |> sort (thm_ord o swap o pairself snd)
|> map (snd #> `(theory_of_thm #> Context.theory_name))
|> AList.coalesce (op =)
- |> map (apsnd (map Thm.get_name_hint))
+ |> map (apsnd (map nickname_of))
fun has_thy thy th =
Context.theory_name thy = Context.theory_name (theory_of_thm th)
@@ -51,7 +51,7 @@
val all_names =
filter_out is_likely_tautology_or_too_meta
- #> map (rpair () o Thm.get_name_hint) #> Symtab.make
+ #> map (rpair () o nickname_of) #> Symtab.make
fun generate_accessibility thy include_thy file_name =
let
@@ -63,7 +63,7 @@
val _ = File.append path s
in [fact] end
val thy_map =
- all_facts_of thy Termtab.empty
+ all_facts_of (Proof_Context.init_global thy) Termtab.empty
|> not include_thy ? filter_out (has_thy thy o snd)
|> thy_map_from_facts
fun do_thy facts =
@@ -79,13 +79,13 @@
val _ = File.write path ""
val css_table = clasimpset_rule_table_of ctxt
val facts =
- all_facts_of thy css_table
+ all_facts_of (Proof_Context.init_global thy) css_table
|> not include_thy ? filter_out (has_thy thy o snd)
- fun do_fact ((_, (_, status)), th) =
+ fun do_fact ((_, stature), th) =
let
- val name = Thm.get_name_hint th
+ val name = nickname_of th
val feats =
- features_of ctxt prover (theory_of_thm th) status [prop_of th]
+ features_of ctxt prover (theory_of_thm th) stature [prop_of th]
val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
in File.append path s end
in List.app do_fact facts end
@@ -95,62 +95,36 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val ths =
- all_facts_of thy Termtab.empty
+ all_facts_of (Proof_Context.init_global thy) Termtab.empty
|> not include_thy ? filter_out (has_thy thy o snd)
|> map snd
val all_names = all_names ths
fun do_thm th =
let
- val name = Thm.get_name_hint th
- val deps = isabelle_dependencies_of all_names th
+ val name = nickname_of th
+ val deps = isar_dependencies_of all_names th |> these
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
in File.append path s end
in List.app do_thm ths end
-fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
- include_thy file_name =
+fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy
+ file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
val facts =
- all_facts_of thy Termtab.empty
+ all_facts_of (Proof_Context.init_global thy) Termtab.empty
|> not include_thy ? filter_out (has_thy thy o snd)
val ths = facts |> map snd
val all_names = all_names ths
- fun is_dep dep (_, th) = Thm.get_name_hint th = dep
- fun add_isar_dep facts dep accum =
- if exists (is_dep dep) accum then
- accum
- else case find_first (is_dep dep) facts of
- SOME ((name, status), th) => accum @ [((name, status), th)]
- | NONE => accum (* shouldn't happen *)
- fun fix_name ((_, stature), th) =
- ((fn () => th |> Thm.get_name_hint, stature), th)
fun do_thm th =
let
- val name = Thm.get_name_hint th
- val goal = goal_of_thm thy th
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
+ val name = nickname_of th
val deps =
- case isabelle_dependencies_of all_names th of
- [] => []
- | isar_dep as [_] => isar_dep (* can hardly beat that *)
- | isar_deps =>
- let
- val facts =
- facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- val facts =
- facts |> iterative_relevant_facts ctxt params prover
- (the max_facts) NONE hyp_ts concl_t
- |> fold (add_isar_dep facts) isar_deps
- |> map fix_name
- in
- case run_prover_for_mash ctxt params prover facts goal of
- {outcome = NONE, used_facts, ...} =>
- used_facts |> map fst |> sort string_ord
- | _ => isar_deps
- end
+ case atp_dependencies_of ctxt params prover 0 facts all_names th of
+ SOME deps => deps
+ | NONE => isar_dependencies_of all_names th |> these
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
in File.append path s end
in List.app do_thm ths end
@@ -160,17 +134,17 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of thy css_table
+ val facts = all_facts_of (Proof_Context.init_global thy) css_table
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
val ths = facts |> map snd
val all_names = all_names ths
- fun do_fact ((_, (_, status)), th) prevs =
+ fun do_fact ((_, stature), th) prevs =
let
- val name = Thm.get_name_hint th
- val feats = features_of ctxt prover thy status [prop_of th]
- val deps = isabelle_dependencies_of all_names th
+ val name = nickname_of th
+ val feats = features_of ctxt prover thy stature [prop_of th]
+ val deps = isar_dependencies_of all_names th |> these
val kind = Thm.legacy_get_kind th
val core = escape_metas prevs ^ "; " ^ escape_metas feats
val query = if kind <> "" then "? " ^ core ^ "\n" else ""
@@ -183,20 +157,20 @@
val parents = parent_facts thy thy_map
in fold do_fact new_facts parents; () end
-fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
+fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant
file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of thy css_table
+ val facts = all_facts_of (Proof_Context.init_global thy) css_table
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
fun do_fact (fact as (_, th)) old_facts =
let
- val name = Thm.get_name_hint th
+ val name = nickname_of th
val goal = goal_of_thm thy th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val kind = Thm.legacy_get_kind th
@@ -205,10 +179,9 @@
let
val suggs =
old_facts
- |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
- prover max_relevant NONE hyp_ts concl_t
+ |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
+ max_relevant NONE hyp_ts concl_t
|> map (fn ((name, _), _) => name ())
- |> sort string_ord
val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
in File.append path s end
else
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Fri Jul 20 23:38:15 2012 +0200
@@ -21,7 +21,7 @@
open Sledgehammer_Util
open Sledgehammer_Fact
open Sledgehammer_Provers
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
open Sledgehammer_Isar
fun run_prover override_params fact_override i n ctxt goal =
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 20 23:38:15 2012 +0200
@@ -14,8 +14,7 @@
type slice_spec = int * atp_format * string * string * bool
type atp_config =
- {exec : string list * string,
- required_vars : string list list,
+ {exec : string list * string list,
arguments :
Proof.context -> bool -> string -> Time.time
-> term_order * (unit -> (string * int) list)
@@ -87,8 +86,7 @@
type slice_spec = int * atp_format * string * string * bool
type atp_config =
- {exec : string list * string,
- required_vars : string list list,
+ {exec : string list * string list,
arguments :
Proof.context -> bool -> string -> Time.time
-> term_order * (unit -> (string * int) list)
@@ -190,8 +188,7 @@
val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
val alt_ergo_config : atp_config =
- {exec = (["WHY3_HOME"], "why3"),
- required_vars = [],
+ {exec = (["WHY3_HOME"], ["why3"]),
arguments =
fn _ => fn _ => fn _ => fn timeout => fn _ =>
"--format tff1 --prover alt-ergo --timelimit " ^
@@ -263,7 +260,7 @@
\--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
\--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
- "(SimulateSOS, " ^
+ "(SimulateSOS," ^
(e_selection_heuristic_case heuristic
e_default_fun_weight e_default_sym_offs_weight
|> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
@@ -303,8 +300,7 @@
fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO"
val e_config : atp_config =
- {exec = (["E_HOME"], "eproof"),
- required_vars = [],
+ {exec = (["E_HOME"], ["eproof_ram", "eproof"]),
arguments =
fn ctxt => fn full_proof => fn heuristic => fn timeout =>
fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
@@ -314,11 +310,7 @@
"--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
"--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
e_shell_level_argument full_proof,
- proof_delims =
- (* work-around for bug in "epclextract" version 1.6 *)
- ("# SZS status Theorem\n# SZS output start Saturation.",
- "# SZS output end Saturation.") ::
- tstp_proof_delims,
+ proof_delims = tstp_proof_delims,
known_failures =
[(TimedOut, "Failure: Resource limit exceeded (time)"),
(TimedOut, "time limit exceeded")] @
@@ -348,8 +340,7 @@
THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
val leo2_config : atp_config =
- {exec = (["LEO2_HOME"], "leo"),
- required_vars = [],
+ {exec = (["LEO2_HOME"], ["leo"]),
arguments =
fn _ => fn _ => fn _ => fn timeout => fn _ =>
"--foatp e --atp e=\"$E_HOME\"/eprover \
@@ -377,8 +368,7 @@
THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
val satallax_config : atp_config =
- {exec = (["SATALLAX_HOME"], "satallax"),
- required_vars = [],
+ {exec = (["SATALLAX_HOME"], ["satallax"]),
arguments =
fn _ => fn _ => fn _ => fn timeout => fn _ =>
"-p hocore -t " ^ string_of_int (to_secs 1 timeout),
@@ -405,8 +395,7 @@
(* FIXME: Make "SPASS_NEW_HOME" legacy. *)
val spass_config : atp_config =
- {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"),
- required_vars = [],
+ {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
|> extra_options <> "" ? prefix (extra_options ^ " "),
@@ -447,8 +436,7 @@
val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
val vampire_config : atp_config =
- {exec = (["VAMPIRE_HOME"], "vampire"),
- required_vars = [],
+ {exec = (["VAMPIRE_HOME"], ["vampire"]),
arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
"--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
" --proof tptp --output_axiom_names on\
@@ -491,8 +479,7 @@
val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
val z3_tptp_config : atp_config =
- {exec = (["Z3_HOME"], "z3"),
- required_vars = [],
+ {exec = (["Z3_HOME"], ["z3"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
"MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
proof_delims = [],
@@ -513,8 +500,7 @@
(* Not really a prover: Experimental Polymorphic THF and DFG output *)
fun dummy_config format type_enc : atp_config =
- {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"),
- required_vars = [],
+ {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
arguments = K (K (K (K (K "")))),
proof_delims = [],
known_failures = known_szs_status_failures,
@@ -577,8 +563,7 @@
fun remote_config system_name system_versions proof_delims known_failures
prem_role best_slice : atp_config =
- {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
- required_vars = [],
+ {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
(if command <> "" then "-c " ^ quote command ^ " " else "") ^
"-s " ^ the_system system_name system_versions ^ " " ^
@@ -660,8 +645,8 @@
val supported_atps = Symtab.keys o Data.get
fun is_atp_installed thy name =
- let val {exec, required_vars, ...} = get_atp thy name () in
- forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars)
+ let val {exec, ...} = get_atp thy name () in
+ exists (fn var => getenv var <> "") (fst exec)
end
fun refresh_systems_on_tptp () =
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Fri Jul 20 23:38:15 2012 +0200
@@ -23,7 +23,7 @@
val remote_prefix = "remote_"
fun make_name is_remote name = name |> is_remote ? prefix remote_prefix
-fun make_local_avail name () = getenv (name ^ "_INSTALLED") = "yes"
+fun make_local_avail name () = getenv (name ^ "_SOLVER") <> ""
fun make_remote_avail name () = getenv (name ^ "_REMOTE_SOLVER") <> ""
fun make_avail is_remote name =
if is_remote then make_remote_avail name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 23:38:15 2012 +0200
@@ -23,12 +23,14 @@
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
-> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
+ val is_likely_tautology_or_too_meta : thm -> bool
+ val backquote_thm : thm -> string
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
val maybe_instantiate_inducts :
Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
-> (((unit -> string) * 'a) * thm) list
val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
- val all_facts_of : theory -> status Termtab.table -> fact list
+ val all_facts_of : Proof.context -> status Termtab.table -> fact list
val nearly_all_facts :
Proof.context -> bool -> fact_override -> unit Symtab.table
-> status Termtab.table -> thm list -> term list -> term -> fact list
@@ -84,10 +86,10 @@
| is_rec_def _ = false
fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
-fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
+fun is_chained chained = member Thm.eq_thm_prop chained
-fun scope_of_thm global assms chained_ths th =
- if is_chained chained_ths th then Chained
+fun scope_of_thm global assms chained th =
+ if is_chained chained th then Chained
else if global then Global
else if is_assum assms th then Assum
else Local
@@ -97,20 +99,20 @@
body_type T = @{typ bool}
| _ => false)
-fun status_of_thm css_table name th =
+fun status_of_thm css name th =
(* FIXME: use structured name *)
if (String.isSubstring ".induct" name orelse
String.isSubstring ".inducts" name) andalso
may_be_induction (prop_of th) then
Induction
- else case Termtab.lookup css_table (prop_of th) of
+ else case Termtab.lookup css (prop_of th) of
SOME status => status
| NONE => General
-fun stature_of_thm global assms chained_ths css_table name th =
- (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
+fun stature_of_thm global assms chained css name th =
+ (scope_of_thm global assms chained th, status_of_thm css name th)
-fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
+fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
val bracket =
@@ -126,15 +128,12 @@
make_name reserved true
(nth (maps (explode_interval (length ths)) intervals) j) name ^
bracket
- in
- (ths, (0, []))
- |-> fold (fn th => fn (j, rest) =>
- let val name = nth_name j in
- (j + 1, ((name, stature_of_thm false [] chained_ths
- css_table name th), th) :: rest)
- end)
- |> snd
- end
+ fun add_nth th (j, rest) =
+ let val name = nth_name j in
+ (j + 1, ((name, stature_of_thm false [] chained css name th), th)
+ :: rest)
+ end
+ in (0, []) |> fold add_nth ths |> snd end
(* Reject theorems with names like "List.filter.filter_list_def" or
"Accessible_Part.acc.defs", as these are definitions arising from packages. *)
@@ -212,9 +211,27 @@
is_that_fact thm
end
-fun hackish_string_for_term ctxt t =
+fun is_likely_tautology_or_too_meta th =
+ let
+ val is_boring_const = member (op =) atp_widely_irrelevant_consts
+ fun is_boring_bool t =
+ not (exists_Const (not o is_boring_const o fst) t) orelse
+ exists_type (exists_subtype (curry (op =) @{typ prop})) t
+ fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
+ | is_boring_prop (@{const "==>"} $ t $ u) =
+ is_boring_prop t andalso is_boring_prop u
+ | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
+ is_boring_prop t andalso is_boring_prop u
+ | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
+ is_boring_bool t andalso is_boring_bool u
+ | is_boring_prop _ = true
+ in
+ is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
+ end
+
+fun hackish_string_for_term thy t =
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) (Syntax.string_of_term ctxt) t
+ (print_mode_value ())) (Syntax.string_of_term_global thy) t
|> String.translate (fn c => if Char.isPrint c then str c else "")
|> simplify_spaces
@@ -240,6 +257,13 @@
(Term.add_vars t [] |> sort_wrt (fst o fst))
|> fst
+fun backquote_term thy t =
+ t |> close_form
+ |> hackish_string_for_term thy
+ |> backquote
+
+fun backquote_thm th = backquote_term (theory_of_thm th) (prop_of th)
+
fun clasimpset_rule_table_of ctxt =
let
val thy = Proof_Context.theory_of ctxt
@@ -302,13 +326,14 @@
fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
let
+ val thy = Proof_Context.theory_of ctxt
fun varify_noninducts (t as Free (s, T)) =
if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
| varify_noninducts t = t
val p_inst =
concl_prop |> map_aterms varify_noninducts |> close_form
|> lambda (Free ind_x)
- |> hackish_string_for_term ctxt
+ |> hackish_string_for_term thy
in
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
@@ -345,7 +370,7 @@
fun maybe_filter_no_atps ctxt =
not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
-fun all_facts ctxt ho_atp reserved add_ths chained_ths css_table =
+fun all_facts ctxt ho_atp reserved add_ths chained css =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -356,7 +381,7 @@
not (Thm.has_name_hint th) andalso
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
val unnamed_locals =
- union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
+ union Thm.eq_thm_prop (Facts.props local_facts) chained
|> filter is_good_unnamed_local |> map (pair "" o single)
val full_space =
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
@@ -374,8 +399,6 @@
else
let
val multi = length ths > 1
- val backquote_thm =
- backquote o hackish_string_for_term ctxt o close_form o prop_of
fun check_thms a =
case try (Proof_Context.get_thms ctxt) a of
NONE => false
@@ -392,15 +415,15 @@
val new =
(((fn () =>
if name0 = "" then
- th |> backquote_thm
+ backquote_thm th
else
[Facts.extern ctxt facts name0,
Name_Space.extern ctxt full_space name0]
|> find_first check_thms
|> the_default name0
|> make_name reserved multi j),
- stature_of_thm global assms chained_ths
- css_table name0 th), th)
+ stature_of_thm global assms chained css name0
+ th), th)
in
if multi then (new :: multis, unis)
else (multis, new :: unis)
@@ -415,28 +438,27 @@
|> op @
end
-fun all_facts_of thy css_table =
- let val ctxt = Proof_Context.init_global thy in
- all_facts ctxt false Symtab.empty [] [] css_table
- |> rev (* try to restore the original order of facts, for MaSh *)
- end
+fun all_facts_of ctxt css =
+ all_facts ctxt false Symtab.empty [] [] css
+ |> rev (* partly restore the original order of facts, for MaSh *)
-fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths
- hyp_ts concl_t =
+fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
+ concl_t =
if only andalso null add then
[]
else
let
- val chained_ths =
- chained_ths
+ val chained =
+ chained
|> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
in
(if only then
maps (map (fn ((name, stature), th) => ((K name, stature), th))
- o fact_from_ref ctxt reserved chained_ths css_table) add
+ o fact_from_ref ctxt reserved chained css) add
else
let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
- all_facts ctxt ho_atp reserved add chained_ths css_table
+ all_facts ctxt ho_atp reserved add chained css
+ |> filter_out (is_likely_tautology_or_too_meta o snd)
|> filter_out (member Thm.eq_thm_prop del o snd)
|> maybe_filter_no_atps ctxt
|> uniquify
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Fri Jul 20 23:37:54 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,537 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
- Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-Sledgehammer's iterative relevance filter.
-*)
-
-signature SLEDGEHAMMER_FILTER_ITER =
-sig
- type stature = ATP_Problem_Generate.stature
- type fact = Sledgehammer_Fact.fact
- type params = Sledgehammer_Provers.params
- type relevance_fudge = Sledgehammer_Provers.relevance_fudge
-
- val trace : bool Config.T
- val pseudo_abs_name : string
- val pseudo_skolem_prefix : string
- val const_names_in_fact :
- theory -> (string * typ -> term list -> bool * term list) -> term
- -> string list
- val iterative_relevant_facts :
- Proof.context -> params -> string -> int -> relevance_fudge option
- -> term list -> term -> fact list -> fact list
-end;
-
-structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
-struct
-
-open ATP_Problem_Generate
-open Sledgehammer_Fact
-open Sledgehammer_Provers
-
-val trace =
- Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false)
-fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
-
-val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-val pseudo_abs_name = sledgehammer_prefix ^ "abs"
-val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
-val theory_const_suffix = Long_Name.separator ^ " 1"
-
-fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
- Int.max (order_of_type T1 + 1, order_of_type T2)
- | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
- | order_of_type _ = 0
-
-(* An abstraction of Isabelle types and first-order terms *)
-datatype pattern = PVar | PApp of string * pattern list
-datatype ptype = PType of int * pattern list
-
-fun string_for_pattern PVar = "_"
- | string_for_pattern (PApp (s, ps)) =
- if null ps then s else s ^ string_for_patterns ps
-and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
-fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
-
-(*Is the second type an instance of the first one?*)
-fun match_pattern (PVar, _) = true
- | match_pattern (PApp _, PVar) = false
- | match_pattern (PApp (s, ps), PApp (t, qs)) =
- s = t andalso match_patterns (ps, qs)
-and match_patterns (_, []) = true
- | match_patterns ([], _) = false
- | match_patterns (p :: ps, q :: qs) =
- match_pattern (p, q) andalso match_patterns (ps, qs)
-fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
-
-(* Is there a unifiable constant? *)
-fun pconst_mem f consts (s, ps) =
- exists (curry (match_ptype o f) ps)
- (map snd (filter (curry (op =) s o fst) consts))
-fun pconst_hyper_mem f const_tab (s, ps) =
- exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
-
-fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
- | pattern_for_type (TFree (s, _)) = PApp (s, [])
- | pattern_for_type (TVar _) = PVar
-
-(* Pairs a constant with the list of its type instantiations. *)
-fun ptype thy const x =
- (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
- else [])
-fun rich_ptype thy const (s, T) =
- PType (order_of_type T, ptype thy const (s, T))
-fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
-
-fun string_for_hyper_pconst (s, ps) =
- s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
-
-(* Add a pconstant to the table, but a [] entry means a standard
- connective, which we ignore.*)
-fun add_pconst_to_table also_skolem (s, p) =
- if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I
- else Symtab.map_default (s, [p]) (insert (op =) p)
-
-(* Set constants tend to pull in too many irrelevant facts. We limit the damage
- by treating them more or less as if they were built-in but add their
- axiomatization at the end. *)
-val set_consts = [@{const_name Collect}, @{const_name Set.member}]
-val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
-
-fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
- let
- val flip = Option.map not
- (* We include free variables, as well as constants, to handle locales. For
- each quantifiers that must necessarily be skolemized by the automatic
- prover, we introduce a fresh constant to simulate the effect of
- Skolemization. *)
- fun do_const const ext_arg (x as (s, _)) ts =
- let val (built_in, ts) = is_built_in_const x ts in
- if member (op =) set_consts s then
- fold (do_term ext_arg) ts
- else
- (not built_in
- ? add_pconst_to_table also_skolems (rich_pconst thy const x))
- #> fold (do_term false) ts
- end
- and do_term ext_arg t =
- case strip_comb t of
- (Const x, ts) => do_const true ext_arg x ts
- | (Free x, ts) => do_const false ext_arg x ts
- | (Abs (_, T, t'), ts) =>
- ((null ts andalso not ext_arg)
- (* Since lambdas on the right-hand side of equalities are usually
- extensionalized later by "abs_extensionalize_term", we don't
- penalize them here. *)
- ? add_pconst_to_table true (pseudo_abs_name,
- PType (order_of_type T + 1, [])))
- #> fold (do_term false) (t' :: ts)
- | (_, ts) => fold (do_term false) ts
- fun do_quantifier will_surely_be_skolemized abs_T body_t =
- do_formula pos body_t
- #> (if also_skolems andalso will_surely_be_skolemized then
- add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (),
- PType (order_of_type abs_T, []))
- else
- I)
- and do_term_or_formula ext_arg T =
- if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
- and do_formula pos t =
- case t of
- Const (@{const_name all}, _) $ Abs (_, T, t') =>
- do_quantifier (pos = SOME false) T t'
- | @{const "==>"} $ t1 $ t2 =>
- do_formula (flip pos) t1 #> do_formula pos t2
- | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
- do_term_or_formula false T t1 #> do_term_or_formula true T t2
- | @{const Trueprop} $ t1 => do_formula pos t1
- | @{const False} => I
- | @{const True} => I
- | @{const Not} $ t1 => do_formula (flip pos) t1
- | Const (@{const_name All}, _) $ Abs (_, T, t') =>
- do_quantifier (pos = SOME false) T t'
- | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
- do_quantifier (pos = SOME true) T t'
- | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
- | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
- | @{const HOL.implies} $ t1 $ t2 =>
- do_formula (flip pos) t1 #> do_formula pos t2
- | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
- do_term_or_formula false T t1 #> do_term_or_formula true T t2
- | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
- $ t1 $ t2 $ t3 =>
- do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
- | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
- do_quantifier (is_some pos) T t'
- | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
- do_quantifier (pos = SOME false) T
- (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
- | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
- do_quantifier (pos = SOME true) T
- (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
- | (t0 as Const (_, @{typ bool})) $ t1 =>
- do_term false t0 #> do_formula pos t1 (* theory constant *)
- | _ => do_term false t
- in do_formula pos end
-
-fun pconsts_in_fact thy is_built_in_const t =
- Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
- (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
- (SOME true) t) []
-
-val const_names_in_fact = map fst ooo pconsts_in_fact
-
-(* Inserts a dummy "constant" referring to the theory name, so that relevance
- takes the given theory into account. *)
-fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
- : relevance_fudge) thy_name t =
- if exists (curry (op <) 0.0) [theory_const_rel_weight,
- theory_const_irrel_weight] then
- Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
- else
- t
-
-fun theory_const_prop_of fudge th =
- theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
-
-fun pair_consts_fact thy is_built_in_const fudge fact =
- case fact |> snd |> theory_const_prop_of fudge
- |> pconsts_in_fact thy is_built_in_const of
- [] => NONE
- | consts => SOME ((fact, consts), NONE)
-
-(* A two-dimensional symbol table counts frequencies of constants. It's keyed
- first by constant name and second by its list of type instantiations. For the
- latter, we need a linear ordering on "pattern list". *)
-
-fun pattern_ord p =
- case p of
- (PVar, PVar) => EQUAL
- | (PVar, PApp _) => LESS
- | (PApp _, PVar) => GREATER
- | (PApp q1, PApp q2) =>
- prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
-fun ptype_ord (PType p, PType q) =
- prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
-
-structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
-
-fun count_fact_consts thy fudge =
- let
- fun do_const const (s, T) ts =
- (* Two-dimensional table update. Constant maps to types maps to count. *)
- PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
- |> Symtab.map_default (s, PType_Tab.empty)
- #> fold do_term ts
- and do_term t =
- case strip_comb t of
- (Const x, ts) => do_const true x ts
- | (Free x, ts) => do_const false x ts
- | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
- | (_, ts) => fold do_term ts
- in do_term o theory_const_prop_of fudge o snd end
-
-fun pow_int _ 0 = 1.0
- | pow_int x 1 = x
- | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
-
-(*The frequency of a constant is the sum of those of all instances of its type.*)
-fun pconst_freq match const_tab (c, ps) =
- PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
- (the (Symtab.lookup const_tab c)) 0
-
-
-(* A surprising number of theorems contain only a few significant constants.
- These include all induction rules, and other general theorems. *)
-
-(* "log" seems best in practice. A constant function of one ignores the constant
- frequencies. Rare constants give more points if they are relevant than less
- rare ones. *)
-fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
-
-(* Irrelevant constants are treated differently. We associate lower penalties to
- very rare constants and very common ones -- the former because they can't
- lead to the inclusion of too many new facts, and the latter because they are
- so common as to be of little interest. *)
-fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
- : relevance_fudge) order freq =
- let val (k, x) = worse_irrel_freq |> `Real.ceil in
- (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
- else rel_weight_for order freq / rel_weight_for order k)
- * pow_int higher_order_irrel_weight (order - 1)
- end
-
-fun multiplier_for_const_name local_const_multiplier s =
- if String.isSubstring "." s then 1.0 else local_const_multiplier
-
-(* Computes a constant's weight, as determined by its frequency. *)
-fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
- theory_const_weight chained_const_weight weight_for f
- const_tab chained_const_tab (c as (s, PType (m, _))) =
- if s = pseudo_abs_name then
- abs_weight
- else if String.isPrefix pseudo_skolem_prefix s then
- skolem_weight
- else if String.isSuffix theory_const_suffix s then
- theory_const_weight
- else
- multiplier_for_const_name local_const_multiplier s
- * weight_for m (pconst_freq (match_ptype o f) const_tab c)
- |> (if chained_const_weight < 1.0 andalso
- pconst_hyper_mem I chained_const_tab c then
- curry (op *) chained_const_weight
- else
- I)
-
-fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
- theory_const_rel_weight, ...} : relevance_fudge)
- const_tab =
- generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
- theory_const_rel_weight 0.0 rel_weight_for I const_tab
- Symtab.empty
-
-fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
- skolem_irrel_weight,
- theory_const_irrel_weight,
- chained_const_irrel_weight, ...})
- const_tab chained_const_tab =
- generic_pconst_weight local_const_multiplier abs_irrel_weight
- skolem_irrel_weight theory_const_irrel_weight
- chained_const_irrel_weight (irrel_weight_for fudge) swap
- const_tab chained_const_tab
-
-fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
- intro_bonus
- | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
- | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
- | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
- | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
- | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
- | stature_bonus _ _ = 0.0
-
-fun is_odd_const_name s =
- s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
- String.isSuffix theory_const_suffix s
-
-fun fact_weight fudge stature const_tab relevant_consts chained_consts
- fact_consts =
- case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
- ||> filter_out (pconst_hyper_mem swap relevant_consts) of
- ([], _) => 0.0
- | (rel, irrel) =>
- if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
- 0.0
- else
- let
- val irrel = irrel |> filter_out (pconst_mem swap rel)
- val rel_weight =
- 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
- val irrel_weight =
- ~ (stature_bonus fudge stature)
- |> fold (curry (op +)
- o irrel_pconst_weight fudge const_tab chained_consts) irrel
- val res = rel_weight / (rel_weight + irrel_weight)
- in if Real.isFinite res then res else 0.0 end
-
-fun take_most_relevant ctxt max_facts remaining_max
- ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
- (candidates : ((fact * (string * ptype) list) * real) list) =
- let
- val max_imperfect =
- Real.ceil (Math.pow (max_imperfect,
- Math.pow (Real.fromInt remaining_max
- / Real.fromInt max_facts, max_imperfect_exp)))
- val (perfect, imperfect) =
- candidates |> sort (Real.compare o swap o pairself snd)
- |> take_prefix (fn (_, w) => w > 0.99999)
- val ((accepts, more_rejects), rejects) =
- chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
- in
- trace_msg ctxt (fn () =>
- "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
- string_of_int (length candidates) ^ "): " ^
- (accepts |> map (fn ((((name, _), _), _), weight) =>
- name () ^ " [" ^ Real.toString weight ^ "]")
- |> commas));
- (accepts, more_rejects @ rejects)
- end
-
-fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
- if Symtab.is_empty tab then
- Symtab.empty
- |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
- (map_filter (fn ((_, (sc', _)), th) =>
- if sc' = sc then SOME (prop_of th) else NONE) facts)
- else
- tab
-
-fun consider_arities is_built_in_const th =
- let
- fun aux _ _ NONE = NONE
- | aux t args (SOME tab) =
- case t of
- t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
- | Const (x as (s, _)) =>
- (if is_built_in_const x args |> fst then
- SOME tab
- else case Symtab.lookup tab s of
- NONE => SOME (Symtab.update (s, length args) tab)
- | SOME n => if n = length args then SOME tab else NONE)
- | _ => SOME tab
- in aux (prop_of th) [] end
-
-(* FIXME: This is currently only useful for polymorphic type encodings. *)
-fun could_benefit_from_ext is_built_in_const facts =
- fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
- |> is_none
-
-(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
- weights), but low enough so that it is unlikely to be truncated away if few
- facts are included. *)
-val special_fact_index = 75
-
-fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
- (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
- concl_t =
- let
- val thy = Proof_Context.theory_of ctxt
- val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
- val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
- val chained_ts =
- facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
- | _ => NONE)
- val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
- val goal_const_tab =
- Symtab.empty |> fold (add_pconsts true) hyp_ts
- |> add_pconsts false concl_t
- |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
- |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
- [Chained, Assum, Local]
- fun iter j remaining_max thres rel_const_tab hopeless hopeful =
- let
- fun relevant [] _ [] =
- (* Nothing has been added this iteration. *)
- if j = 0 andalso thres >= ridiculous_threshold then
- (* First iteration? Try again. *)
- iter 0 max_facts (thres / threshold_divisor) rel_const_tab
- hopeless hopeful
- else
- []
- | relevant candidates rejects [] =
- let
- val (accepts, more_rejects) =
- take_most_relevant ctxt max_facts remaining_max fudge candidates
- val rel_const_tab' =
- rel_const_tab
- |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
- fun is_dirty (c, _) =
- Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
- val (hopeful_rejects, hopeless_rejects) =
- (rejects @ hopeless, ([], []))
- |-> fold (fn (ax as (_, consts), old_weight) =>
- if exists is_dirty consts then
- apfst (cons (ax, NONE))
- else
- apsnd (cons (ax, old_weight)))
- |>> append (more_rejects
- |> map (fn (ax as (_, consts), old_weight) =>
- (ax, if exists is_dirty consts then NONE
- else SOME old_weight)))
- val thres =
- 1.0 - (1.0 - thres)
- * Math.pow (decay, Real.fromInt (length accepts))
- val remaining_max = remaining_max - length accepts
- in
- trace_msg ctxt (fn () => "New or updated constants: " ^
- commas (rel_const_tab' |> Symtab.dest
- |> subtract (op =) (rel_const_tab |> Symtab.dest)
- |> map string_for_hyper_pconst));
- map (fst o fst) accepts @
- (if remaining_max = 0 then
- []
- else
- iter (j + 1) remaining_max thres rel_const_tab'
- hopeless_rejects hopeful_rejects)
- end
- | relevant candidates rejects
- (((ax as (((_, stature), _), fact_consts)), cached_weight)
- :: hopeful) =
- let
- val weight =
- case cached_weight of
- SOME w => w
- | NONE => fact_weight fudge stature const_tab rel_const_tab
- chained_const_tab fact_consts
- in
- if weight >= thres then
- relevant ((ax, weight) :: candidates) rejects hopeful
- else
- relevant candidates ((ax, weight) :: rejects) hopeful
- end
- in
- trace_msg ctxt (fn () =>
- "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
- Real.toString thres ^ ", constants: " ^
- commas (rel_const_tab |> Symtab.dest
- |> filter (curry (op <>) [] o snd)
- |> map string_for_hyper_pconst));
- relevant [] [] hopeful
- end
- fun uses_const s t =
- fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
- false
- fun uses_const_anywhere accepts s =
- exists (uses_const s o prop_of o snd) accepts orelse
- exists (uses_const s) (concl_t :: hyp_ts)
- fun add_set_const_thms accepts =
- exists (uses_const_anywhere accepts) set_consts ? append set_thms
- fun insert_into_facts accepts [] = accepts
- | insert_into_facts accepts ths =
- let
- val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
- val (bef, after) =
- accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
- |> take (max_facts - length add)
- |> chop special_fact_index
- in bef @ add @ after end
- fun insert_special_facts accepts =
- (* FIXME: get rid of "ext" here once it is treated as a helper *)
- [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
- |> add_set_const_thms accepts
- |> insert_into_facts accepts
- in
- facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
- |> iter 0 max_facts thres0 goal_const_tab []
- |> insert_special_facts
- |> tap (fn accepts => trace_msg ctxt (fn () =>
- "Total relevant: " ^ string_of_int (length accepts)))
- end
-
-fun iterative_relevant_facts ctxt
- ({fact_thresholds = (thres0, thres1), ...} : params) prover
- max_facts fudge hyp_ts concl_t facts =
- let
- val thy = Proof_Context.theory_of ctxt
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover
- val fudge =
- case fudge of
- SOME fudge => fudge
- | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover
- val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
- 1.0 / Real.fromInt (max_facts + 1))
- in
- trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
- " facts");
- (if thres1 < 0.0 then
- facts
- else if thres0 > 1.0 orelse thres0 > thres1 then
- []
- else
- relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
- facts hyp_ts
- (concl_t |> theory_constify fudge (Context.theory_name thy)))
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Fri Jul 20 23:37:54 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,668 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
- Author: Jasmin Blanchette, TU Muenchen
-
-Sledgehammer's machine-learning-based relevance filter (MaSh).
-*)
-
-signature SLEDGEHAMMER_FILTER_MASH =
-sig
- type status = ATP_Problem_Generate.status
- type stature = ATP_Problem_Generate.stature
- type fact = Sledgehammer_Fact.fact
- type fact_override = Sledgehammer_Fact.fact_override
- type params = Sledgehammer_Provers.params
- type relevance_fudge = Sledgehammer_Provers.relevance_fudge
- type prover_result = Sledgehammer_Provers.prover_result
-
- val trace : bool Config.T
- val MaShN : string
- val meshN : string
- val iterN : string
- val mashN : string
- val fact_filters : string list
- val escape_meta : string -> string
- val escape_metas : string list -> string
- val unescape_meta : string -> string
- val unescape_metas : string -> string list
- val extract_query : string -> string * string list
- val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
- val mesh_facts :
- int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
- val is_likely_tautology_or_too_meta : thm -> bool
- val theory_ord : theory * theory -> order
- val thm_ord : thm * thm -> order
- val features_of :
- Proof.context -> string -> theory -> status -> term list -> string list
- val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
- val goal_of_thm : theory -> thm -> thm
- val run_prover_for_mash :
- Proof.context -> params -> string -> fact list -> thm -> prover_result
- val mash_CLEAR : Proof.context -> unit
- val mash_INIT :
- Proof.context -> bool
- -> (string * string list * string list * string list) list -> unit
- val mash_ADD :
- Proof.context -> bool
- -> (string * string list * string list * string list) list -> unit
- val mash_QUERY :
- Proof.context -> bool -> int -> string list * string list -> string list
- val mash_unlearn : Proof.context -> unit
- val mash_could_suggest_facts : unit -> bool
- val mash_can_suggest_facts : Proof.context -> bool
- val mash_suggest_facts :
- Proof.context -> params -> string -> int -> term list -> term
- -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
- val mash_learn_thy :
- Proof.context -> params -> theory -> Time.time -> fact list -> string
- val mash_learn_proof :
- Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
- val relevant_facts :
- Proof.context -> params -> string -> int -> fact_override -> term list
- -> term -> fact list -> fact list
- val kill_learners : unit -> unit
- val running_learners : unit -> unit
-end;
-
-structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
-struct
-
-open ATP_Util
-open ATP_Problem_Generate
-open Sledgehammer_Util
-open Sledgehammer_Fact
-open Sledgehammer_Filter_Iter
-open Sledgehammer_Provers
-open Sledgehammer_Minimize
-
-val trace =
- Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)
-fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
-
-val MaShN = "MaSh"
-
-val meshN = "mesh"
-val iterN = "iter"
-val mashN = "mash"
-
-val fact_filters = [meshN, iterN, mashN]
-
-fun mash_home () = getenv "MASH_HOME"
-fun mash_state_dir () =
- getenv "ISABELLE_HOME_USER" ^ "/mash"
- |> tap (Isabelle_System.mkdir o Path.explode)
-fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
-
-
-(*** Isabelle helpers ***)
-
-fun meta_char c =
- if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
- c = #")" orelse c = #"," then
- String.str c
- else
- (* fixed width, in case more digits follow *)
- "\\" ^ stringN_of_int 3 (Char.ord c)
-
-fun unmeta_chars accum [] = String.implode (rev accum)
- | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
- (case Int.fromString (String.implode [d1, d2, d3]) of
- SOME n => unmeta_chars (Char.chr n :: accum) cs
- | NONE => "" (* error *))
- | unmeta_chars _ (#"\\" :: _) = "" (* error *)
- | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
-
-val escape_meta = String.translate meta_char
-val escape_metas = map escape_meta #> space_implode " "
-val unescape_meta = String.explode #> unmeta_chars []
-val unescape_metas =
- space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
-
-fun extract_query line =
- case space_explode ":" line of
- [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
- | _ => ("", [])
-
-fun suggested_facts suggs facts =
- let
- fun add_fact (fact as (_, th)) = Symtab.default (Thm.get_name_hint th, fact)
- val tab = Symtab.empty |> fold add_fact facts
- in map_filter (Symtab.lookup tab) suggs end
-
-(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
-fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0
-
-fun sum_sq_avg [] = 0
- | sum_sq_avg xs =
- Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs
-
-fun mesh_facts max_facts [(selected, unknown)] =
- take max_facts selected @ take (max_facts - length selected) unknown
- | mesh_facts max_facts mess =
- let
- val mess = mess |> map (apfst (`length))
- val fact_eq = Thm.eq_thm o pairself snd
- fun score_in fact ((sel_len, sels), unks) =
- case find_index (curry fact_eq fact) sels of
- ~1 => (case find_index (curry fact_eq fact) unks of
- ~1 => SOME sel_len
- | _ => NONE)
- | j => SOME j
- fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg
- val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
- in
- facts |> map (`score_of) |> sort (int_ord o swap o pairself fst)
- |> map snd |> take max_facts
- end
-
-val thy_feature_prefix = "y_"
-
-val thy_feature_name_of = prefix thy_feature_prefix
-val const_name_of = prefix const_prefix
-val type_name_of = prefix type_const_prefix
-val class_name_of = prefix class_prefix
-
-fun is_likely_tautology_or_too_meta th =
- let
- val is_boring_const = member (op =) atp_widely_irrelevant_consts
- fun is_boring_bool t =
- not (exists_Const (not o is_boring_const o fst) t) orelse
- exists_type (exists_subtype (curry (op =) @{typ prop})) t
- fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
- | is_boring_prop (@{const "==>"} $ t $ u) =
- is_boring_prop t andalso is_boring_prop u
- | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
- is_boring_prop t andalso is_boring_prop u
- | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
- is_boring_bool t andalso is_boring_bool u
- | is_boring_prop _ = true
- in
- is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
- end
-
-fun theory_ord p =
- if Theory.eq_thy p then
- EQUAL
- else if Theory.subthy p then
- LESS
- else if Theory.subthy (swap p) then
- GREATER
- else case int_ord (pairself (length o Theory.ancestors_of) p) of
- EQUAL => string_ord (pairself Context.theory_name p)
- | order => order
-
-val thm_ord = theory_ord o pairself theory_of_thm
-
-val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
-
-fun interesting_terms_types_and_classes ctxt prover term_max_depth
- type_max_depth ts =
- let
- fun is_bad_const (x as (s, _)) args =
- member (op =) atp_logical_consts s orelse
- fst (is_built_in_const_for_prover ctxt prover x args)
- fun add_classes @{sort type} = I
- | add_classes S = union (op =) (map class_name_of S)
- fun do_add_type (Type (s, Ts)) =
- (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
- #> fold do_add_type Ts
- | do_add_type (TFree (_, S)) = add_classes S
- | do_add_type (TVar (_, S)) = add_classes S
- fun add_type T = type_max_depth >= 0 ? do_add_type T
- fun mk_app s args =
- if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
- else s
- fun patternify ~1 _ = ""
- | patternify depth t =
- case strip_comb t of
- (Const (s, _), args) =>
- mk_app (const_name_of s) (map (patternify (depth - 1)) args)
- | _ => ""
- fun add_term_patterns ~1 _ = I
- | add_term_patterns depth t =
- insert (op =) (patternify depth t)
- #> add_term_patterns (depth - 1) t
- val add_term = add_term_patterns term_max_depth
- fun add_patterns t =
- let val (head, args) = strip_comb t in
- (case head of
- Const (x as (_, T)) =>
- not (is_bad_const x args) ? (add_term t #> add_type T)
- | Free (_, T) => add_type T
- | Var (_, T) => add_type T
- | Abs (_, T, body) => add_type T #> add_patterns body
- | _ => I)
- #> fold add_patterns args
- end
- in [] |> fold add_patterns ts end
-
-fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
-
-val term_max_depth = 1
-val type_max_depth = 1
-
-(* TODO: Generate type classes for types? *)
-fun features_of ctxt prover thy status ts =
- thy_feature_name_of (Context.theory_name thy) ::
- interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
- ts
- |> forall is_lambda_free ts ? cons "no_lams"
- |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
- |> (case status of
- General => I
- | Induction => cons "induction"
- | Intro => cons "intro"
- | Inductive => cons "inductive"
- | Elim => cons "elim"
- | Simp => cons "simp"
- | Def => cons "def")
-
-fun isabelle_dependencies_of all_facts = thms_in_proof (SOME all_facts)
-
-val freezeT = Type.legacy_freeze_type
-
-fun freeze (t $ u) = freeze t $ freeze u
- | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
- | freeze (Var ((s, _), T)) = Free (s, freezeT T)
- | freeze (Const (s, T)) = Const (s, freezeT T)
- | freeze (Free (s, T)) = Free (s, freezeT T)
- | freeze t = t
-
-fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
-
-fun run_prover_for_mash ctxt params prover facts goal =
- let
- val problem =
- {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
- facts = facts |> map (apfst (apfst (fn name => name ())))
- |> map Untranslated_Fact}
- val prover = get_minimizing_prover ctxt Normal (K ()) prover
- in prover params (K (K (K ""))) problem end
-
-
-(*** Low-level communication with MaSh ***)
-
-fun write_file (xs, f) file =
- let val path = Path.explode file in
- File.write path "";
- xs |> chunk_list 500
- |> List.app (File.append path o space_implode "" o map f)
- end
-
-fun mash_info overlord =
- if overlord then (getenv "ISABELLE_HOME_USER", "")
- else (getenv "ISABELLE_TMP", serial_string ())
-
-fun run_mash ctxt overlord (temp_dir, serial) core =
- let
- val log_file = temp_dir ^ "/mash_log" ^ serial
- val err_file = temp_dir ^ "/mash_err" ^ serial
- val command =
- mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^
- " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file
- in
- trace_msg ctxt (fn () => "Running " ^ command);
- write_file ([], K "") log_file;
- write_file ([], K "") err_file;
- Isabelle_System.bash command;
- if overlord then ()
- else (map (File.rm o Path.explode) [log_file, err_file]; ());
- trace_msg ctxt (K "Done")
- end
-
-(* TODO: Eliminate code once "mash.py" handles sequences of ADD commands as fast
- as a single INIT. *)
-fun run_mash_init ctxt overlord write_access write_feats write_deps =
- let
- val info as (temp_dir, serial) = mash_info overlord
- val in_dir = temp_dir ^ "/mash_init" ^ serial
- val in_dir_path = in_dir |> Path.explode |> tap Isabelle_System.mkdir
- in
- write_file write_access (in_dir ^ "/mash_accessibility");
- write_file write_feats (in_dir ^ "/mash_features");
- write_file write_deps (in_dir ^ "/mash_dependencies");
- run_mash ctxt overlord info ("--init --inputDir " ^ in_dir);
- (* FIXME: temporary hack *)
- if overlord then ()
- else (Isabelle_System.bash ("rm -r -f " ^ File.shell_path in_dir_path); ())
- end
-
-fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
- let
- val info as (temp_dir, serial) = mash_info overlord
- val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
- val cmd_file = temp_dir ^ "/mash_commands" ^ serial
- in
- write_file ([], K "") sugg_file;
- write_file write_cmds cmd_file;
- run_mash ctxt overlord info
- ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
- " --numberOfPredictions " ^ string_of_int max_suggs ^
- (if save then " --saveModel" else ""));
- read_suggs (fn () => File.read_lines (Path.explode sugg_file))
- |> tap (fn _ =>
- if overlord then ()
- else (map (File.rm o Path.explode) [sugg_file, cmd_file]; ()))
- end
-
-fun str_of_update (name, parents, feats, deps) =
- "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
- escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
-
-fun str_of_query (parents, feats) =
- "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
-
-fun init_str_of_update get (upd as (name, _, _, _)) =
- escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n"
-
-fun mash_CLEAR ctxt =
- let val path = mash_state_dir () |> Path.explode in
- trace_msg ctxt (K "MaSh CLEAR");
- File.fold_dir (fn file => fn () =>
- File.rm (Path.append path (Path.basic file)))
- path ()
- end
-
-fun mash_INIT ctxt _ [] = mash_CLEAR ctxt
- | mash_INIT ctxt overlord upds =
- (trace_msg ctxt (fn () => "MaSh INIT " ^
- elide_string 1000 (space_implode " " (map #1 upds)));
- run_mash_init ctxt overlord (upds, init_str_of_update #2)
- (upds, init_str_of_update #3) (upds, init_str_of_update #4))
-
-fun mash_ADD _ _ [] = ()
- | mash_ADD ctxt overlord upds =
- (trace_msg ctxt (fn () => "MaSh ADD " ^
- elide_string 1000 (space_implode " " (map #1 upds)));
- run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
-
-fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
- (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
- run_mash_commands ctxt overlord false max_suggs
- ([query], str_of_query)
- (fn suggs => snd (extract_query (List.last (suggs ()))))
- handle List.Empty => [])
-
-
-(*** High-level communication with MaSh ***)
-
-fun try_graph ctxt when def f =
- f ()
- handle Graph.CYCLES (cycle :: _) =>
- (trace_msg ctxt (fn () =>
- "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
- | Graph.UNDEF name =>
- (trace_msg ctxt (fn () =>
- "Unknown fact " ^ quote name ^ " when " ^ when); def)
-
-type mash_state =
- {thys : bool Symtab.table,
- fact_graph : unit Graph.T}
-
-val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty}
-
-local
-
-fun mash_load _ (state as (true, _)) = state
- | mash_load ctxt _ =
- let val path = mash_state_path () in
- (true,
- case try File.read_lines path of
- SOME (comp_thys :: incomp_thys :: fact_lines) =>
- let
- fun add_thy comp thy = Symtab.update (thy, comp)
- fun add_edge_to name parent =
- Graph.default_node (parent, ())
- #> Graph.add_edge (parent, name)
- fun add_fact_line line =
- case extract_query line of
- ("", _) => I (* shouldn't happen *)
- | (name, parents) =>
- Graph.default_node (name, ())
- #> fold (add_edge_to name) parents
- val thys =
- Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
- |> fold (add_thy false) (unescape_metas incomp_thys)
- val fact_graph =
- try_graph ctxt "loading state" Graph.empty (fn () =>
- Graph.empty |> fold add_fact_line fact_lines)
- in {thys = thys, fact_graph = fact_graph} end
- | _ => empty_state)
- end
-
-fun mash_save ({thys, fact_graph, ...} : mash_state) =
- let
- val path = mash_state_path ()
- val thys = Symtab.dest thys
- val line_for_thys = escape_metas o AList.find (op =) thys
- fun fact_line_for name parents =
- escape_meta name ^ ": " ^ escape_metas parents
- val append_fact = File.append path o suffix "\n" oo fact_line_for
- in
- File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");
- Graph.fold (fn (name, ((), (parents, _))) => fn () =>
- append_fact name (Graph.Keys.dest parents))
- fact_graph ()
- end
-
-val global_state =
- Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
-
-in
-
-fun mash_map ctxt f =
- Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
-
-fun mash_get ctxt =
- Synchronized.change_result global_state (mash_load ctxt #> `snd)
-
-fun mash_unlearn ctxt =
- Synchronized.change global_state (fn _ =>
- (mash_CLEAR ctxt; File.write (mash_state_path ()) "";
- (true, empty_state)))
-
-end
-
-fun mash_could_suggest_facts () = mash_home () <> ""
-fun mash_can_suggest_facts ctxt =
- not (Graph.is_empty (#fact_graph (mash_get ctxt)))
-
-fun parents_wrt_facts facts fact_graph =
- let
- val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
- val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
- fun insert_not_parent parents name =
- not (member (op =) parents name) ? insert (op =) name
- fun parents_of parents [] = parents
- | parents_of parents (name :: names) =
- if Symtab.defined tab name then
- parents_of (name :: parents) names
- else
- parents_of parents (Graph.Keys.fold (insert_not_parent parents)
- (Graph.imm_preds fact_graph name) names)
- in parents_of [] (Graph.maximals fact_graph) end
-
-(* Generate more suggestions than requested, because some might be thrown out
- later for various reasons and "meshing" gives better results with some
- slack. *)
-fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
-
-fun is_fact_in_graph fact_graph (_, th) =
- can (Graph.get_node fact_graph) (Thm.get_name_hint th)
-
-fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
- concl_t facts =
- let
- val thy = Proof_Context.theory_of ctxt
- val fact_graph = #fact_graph (mash_get ctxt)
- val parents = parents_wrt_facts facts fact_graph
- val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
- val suggs =
- if Graph.is_empty fact_graph then []
- else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
- val selected = facts |> suggested_facts suggs
- val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
- in (selected, unknown) end
-
-fun add_thys_for thy =
- let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in
- add false thy #> fold (add true) (Theory.ancestors_of thy)
- end
-
-fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
- let
- fun maybe_add_from from (accum as (parents, graph)) =
- try_graph ctxt "updating graph" accum (fn () =>
- (from :: parents, Graph.add_edge_acyclic (from, name) graph))
- val graph = graph |> Graph.default_node (name, ())
- val (parents, graph) = ([], graph) |> fold maybe_add_from parents
- val (deps, graph) = ([], graph) |> fold maybe_add_from deps
- in ((name, parents, feats, deps) :: upds, graph) end
-
-val pass1_learn_timeout_factor = 0.5
-
-(* Too many dependencies is a sign that a decision procedure is at work. There
- isn't much too learn from such proofs. *)
-val max_dependencies = 10
-
-(* The timeout is understood in a very slack fashion. *)
-fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
- facts =
- let
- val timer = Timer.startRealTimer ()
- val prover = hd provers
- fun timed_out frac =
- Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
- val {fact_graph, ...} = mash_get ctxt
- val new_facts =
- facts |> filter_out (is_fact_in_graph fact_graph)
- |> sort (thm_ord o pairself snd)
- in
- if null new_facts then
- ""
- else
- let
- val ths = facts |> map snd
- val all_names =
- ths |> filter_out is_likely_tautology_or_too_meta
- |> map (rpair () o Thm.get_name_hint)
- |> Symtab.make
- fun trim_deps deps = if length deps > max_dependencies then [] else deps
- fun do_fact _ (accum as (_, true)) = accum
- | do_fact ((_, (_, status)), th) ((parents, upds), false) =
- let
- val name = Thm.get_name_hint th
- val feats =
- features_of ctxt prover (theory_of_thm th) status [prop_of th]
- val deps = isabelle_dependencies_of all_names th |> trim_deps
- val upd = (name, parents, feats, deps)
- in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
- val parents = parents_wrt_facts facts fact_graph
- val ((_, upds), _) =
- ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
- val n = length upds
- fun trans {thys, fact_graph} =
- let
- val mash_INIT_or_ADD =
- if Graph.is_empty fact_graph then mash_INIT else mash_ADD
- val (upds, fact_graph) =
- ([], fact_graph) |> fold (update_fact_graph ctxt) upds
- in
- (mash_INIT_or_ADD ctxt overlord (rev upds);
- {thys = thys |> add_thys_for thy,
- fact_graph = fact_graph})
- end
- in
- mash_map ctxt trans;
- if verbose then
- "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
- (if verbose then
- " in " ^ string_from_time (Timer.checkRealTimer timer)
- else
- "") ^ "."
- else
- ""
- end
- end
-
-fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
- let
- val thy = Proof_Context.theory_of ctxt
- val prover = hd provers
- val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
- val feats = features_of ctxt prover thy General [t]
- val deps = used_ths |> map Thm.get_name_hint
- in
- mash_map ctxt (fn {thys, fact_graph} =>
- let
- val parents = parents_wrt_facts facts fact_graph
- val upds = [(name, parents, feats, deps)]
- val (upds, fact_graph) =
- ([], fact_graph) |> fold (update_fact_graph ctxt) upds
- in
- mash_ADD ctxt overlord upds;
- {thys = thys, fact_graph = fact_graph}
- end)
- end
-
-(* The threshold should be large enough so that MaSh doesn't kick in for Auto
- Sledgehammer and Try. *)
-val min_secs_for_learning = 15
-val learn_timeout_factor = 2.0
-
-fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
- max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
- if not (subset (op =) (the_list fact_filter, fact_filters)) then
- error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
- else if only then
- facts
- else if max_facts <= 0 orelse null facts then
- []
- else
- let
- val thy = Proof_Context.theory_of ctxt
- fun maybe_learn () =
- if not learn orelse Async_Manager.has_running_threads MaShN then
- ()
- else if Time.toSeconds timeout >= min_secs_for_learning then
- let
- val soft_timeout = time_mult learn_timeout_factor timeout
- val hard_timeout = time_mult 4.0 soft_timeout
- val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, hard_timeout)
- val desc = ("machine learner for Sledgehammer", "")
- in
- Async_Manager.launch MaShN birth_time death_time desc
- (fn () =>
- (true, mash_learn_thy ctxt params thy soft_timeout facts))
- end
- else
- ()
- val fact_filter =
- case fact_filter of
- SOME ff => (() |> ff <> iterN ? maybe_learn; ff)
- | NONE =>
- if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
- else if mash_could_suggest_facts () then (maybe_learn (); iterN)
- else iterN
- val add_ths = Attrib.eval_thms ctxt add
- fun prepend_facts ths accepts =
- ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
- (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
- |> take max_facts
- fun iter () =
- iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
- concl_t facts
- fun mash () =
- mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
- val mess =
- [] |> (if fact_filter <> mashN then cons (iter (), []) else I)
- |> (if fact_filter <> iterN then cons (mash ()) else I)
- in
- mesh_facts max_facts mess
- |> not (null add_ths) ? prepend_facts add_ths
- end
-
-fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
-fun running_learners () = Async_Manager.running_threads MaShN "learner"
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 23:38:15 2012 +0200
@@ -26,9 +26,13 @@
open Sledgehammer_Fact
open Sledgehammer_Provers
open Sledgehammer_Minimize
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
open Sledgehammer_Run
+val cvc3N = "cvc3"
+val yicesN = "yices"
+val z3N = "z3"
+
val runN = "run"
val minN = "min"
val messagesN = "messages"
@@ -37,7 +41,6 @@
val running_proversN = "running_provers"
val kill_learnersN = "kill_learners"
val running_learnersN = "running_learners"
-val unlearnN = "unlearn"
val refresh_tptpN = "refresh_tptp"
val auto = Unsynchronized.ref false
@@ -152,8 +155,8 @@
val any_type_enc = type_enc_from_string Strict "erased"
-(* "provers =", "type_enc =", "lam_trans =", and "fact_filter =" can be omitted.
- For the last three, this is a secret feature. *)
+(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
+ can be omitted. For the last four, this is a secret feature. *)
fun normalize_raw_param ctxt =
unalias_raw_param
#> (fn (name, value) =>
@@ -168,6 +171,8 @@
("lam_trans", [name])
else if member (op =) fact_filters name then
("fact_filter", [name])
+ else if can Int.fromString name then
+ ("max_facts", [name])
else
error ("Unknown parameter: " ^ quote name ^ "."))
@@ -213,16 +218,15 @@
val max_local_and_remote =
max_local_and_remote
|> (if String.isPrefix remote_prefix prover then apsnd else apfst)
- (Integer.add ~1)
+ (Integer.add ~1)
in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end
val max_default_remote_threads = 4
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
- timeout, it makes sense to put SPASS first. *)
+ timeout, it makes sense to put E first. *)
fun default_provers_param_value ctxt =
- [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN,
- waldmeisterN]
+ [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
max_default_remote_threads)
@@ -245,8 +249,7 @@
end)]
end
-val infinity_time_in_secs = 60 * 60 * 24 * 365
-val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
+val the_timeout = the_default infinite_timeout
fun extract_params mode default_params override_params =
let
@@ -322,7 +325,7 @@
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
learn = learn, fact_filter = fact_filter, max_facts = max_facts,
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
- max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
+ 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,
expect = expect}
@@ -352,12 +355,14 @@
|> (if prover_name = default_minimize_prover then I else cons prover_name)
|> space_implode ", "
in
- "sledgehammer" ^ " " ^ minN ^
+ sledgehammerN ^ " " ^ minN ^
(if params = "" then "" else enclose " [" "]" params) ^
" (" ^ space_implode " " fact_names ^ ")" ^
(if i = 1 then "" else " " ^ string_of_int i)
end
+val default_learn_atp_timeout = 0.5
+
fun hammer_away override_params subcommand opt_i fact_override state =
let
val ctxt = Proof.context_of state
@@ -371,10 +376,17 @@
|> K ()
end
else if subcommand = minN then
- run_minimize (get_params Minimize ctxt
- (("provers", [default_minimize_prover]) ::
- override_params))
- (K ()) (the_default 1 opt_i) (#add fact_override) state
+ let
+ val ctxt = ctxt |> Config.put instantiate_inducts false
+ val i = the_default 1 opt_i
+ val params =
+ get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
+ override_params)
+ val goal = prop_of (#goal (Proof.goal state))
+ val facts = nearly_all_facts ctxt false fact_override Symtab.empty
+ Termtab.empty [] [] goal
+ fun learn prover = mash_learn_proof ctxt params prover goal facts
+ in run_minimize params learn i (#add fact_override) state end
else if subcommand = messagesN then
messages opt_i
else if subcommand = supported_proversN then
@@ -383,12 +395,27 @@
kill_provers ()
else if subcommand = running_proversN then
running_provers ()
+ else if subcommand = unlearnN then
+ mash_unlearn ctxt
+ else if subcommand = learn_isarN orelse subcommand = learn_atpN orelse
+ subcommand = relearn_isarN orelse subcommand = relearn_atpN then
+ (if subcommand = relearn_isarN orelse subcommand = relearn_atpN then
+ mash_unlearn ctxt
+ else
+ ();
+ mash_learn ctxt (get_params Normal ctxt
+ (("timeout",
+ [string_of_real default_learn_atp_timeout]) ::
+ override_params @
+ [("slice", ["false"]),
+ ("minimize", ["true"]),
+ ("preplay_timeout", ["0"])]))
+ fact_override (#facts (Proof.goal state))
+ (subcommand = learn_atpN orelse subcommand = relearn_atpN))
else if subcommand = kill_learnersN then
kill_learners ()
else if subcommand = running_learnersN then
running_learners ()
- else if subcommand = unlearnN then
- mash_unlearn ctxt
else if subcommand = refresh_tptpN then
refresh_systems_on_tptp ()
else
@@ -452,6 +479,6 @@
(minimize_command [] i) state
end
-val setup = Try.register_tool ("sledgehammer", (40, auto, try_sledgehammer))
+val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 23:38:15 2012 +0200
@@ -0,0 +1,895 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_mash.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+Sledgehammer's machine-learning-based relevance filter (MaSh).
+*)
+
+signature SLEDGEHAMMER_MASH =
+sig
+ type stature = ATP_Problem_Generate.stature
+ type fact = Sledgehammer_Fact.fact
+ type fact_override = Sledgehammer_Fact.fact_override
+ type params = Sledgehammer_Provers.params
+ type relevance_fudge = Sledgehammer_Provers.relevance_fudge
+ type prover_result = Sledgehammer_Provers.prover_result
+
+ val trace : bool Config.T
+ val MaShN : string
+ val mepoN : string
+ val mashN : string
+ val meshN : string
+ val unlearnN : string
+ val learn_isarN : string
+ val learn_atpN : string
+ val relearn_isarN : string
+ val relearn_atpN : string
+ val fact_filters : string list
+ val escape_meta : string -> string
+ val escape_metas : string list -> string
+ val unescape_meta : string -> string
+ val unescape_metas : string -> string list
+ val extract_query : string -> string * (string * real) list
+ val nickname_of : thm -> string
+ val suggested_facts :
+ (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
+ val mesh_facts :
+ int -> ((('a * thm) * real) list * ('a * thm) list) list -> ('a * thm) list
+ val theory_ord : theory * theory -> order
+ val thm_ord : thm * thm -> order
+ val goal_of_thm : theory -> thm -> thm
+ val run_prover_for_mash :
+ Proof.context -> params -> string -> fact list -> thm -> prover_result
+ val features_of :
+ Proof.context -> string -> theory -> stature -> term list -> string list
+ val isar_dependencies_of : unit Symtab.table -> thm -> string list option
+ val atp_dependencies_of :
+ Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
+ -> thm -> string list option
+ val mash_CLEAR : Proof.context -> unit
+ val mash_ADD :
+ Proof.context -> bool
+ -> (string * string list * string list * string list) list -> unit
+ val mash_REPROVE :
+ Proof.context -> bool -> (string * string list) list -> unit
+ val mash_QUERY :
+ Proof.context -> bool -> int -> string list * string list
+ -> (string * real) list
+ val mash_unlearn : Proof.context -> unit
+ val mash_could_suggest_facts : unit -> bool
+ val mash_can_suggest_facts : Proof.context -> bool
+ val mash_suggested_facts :
+ Proof.context -> params -> string -> int -> term list -> term
+ -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list
+ val mash_learn_proof :
+ Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
+ -> unit
+ val mash_learn :
+ Proof.context -> params -> fact_override -> thm list -> bool -> unit
+ val relevant_facts :
+ Proof.context -> params -> string -> int -> fact_override -> term list
+ -> term -> fact list -> fact list
+ val kill_learners : unit -> unit
+ val running_learners : unit -> unit
+end;
+
+structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
+struct
+
+open ATP_Util
+open ATP_Problem_Generate
+open Sledgehammer_Util
+open Sledgehammer_Fact
+open Sledgehammer_Provers
+open Sledgehammer_Minimize
+open Sledgehammer_MePo
+
+val trace =
+ Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
+fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
+
+val MaShN = "MaSh"
+
+val mepoN = "mepo"
+val mashN = "mash"
+val meshN = "mesh"
+
+val fact_filters = [meshN, mepoN, mashN]
+
+val unlearnN = "unlearn"
+val learn_isarN = "learn_isar"
+val learn_atpN = "learn_atp"
+val relearn_isarN = "relearn_isar"
+val relearn_atpN = "relearn_atp"
+
+fun mash_home () = getenv "MASH_HOME"
+fun mash_model_dir () =
+ getenv "ISABELLE_HOME_USER" ^ "/mash"
+ |> tap (Isabelle_System.mkdir o Path.explode)
+val mash_state_dir = mash_model_dir
+fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
+
+
+(*** Isabelle helpers ***)
+
+fun meta_char c =
+ if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
+ c = #")" orelse c = #"," then
+ String.str c
+ else
+ (* fixed width, in case more digits follow *)
+ "%" ^ stringN_of_int 3 (Char.ord c)
+
+fun unmeta_chars accum [] = String.implode (rev accum)
+ | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
+ (case Int.fromString (String.implode [d1, d2, d3]) of
+ SOME n => unmeta_chars (Char.chr n :: accum) cs
+ | NONE => "" (* error *))
+ | unmeta_chars _ (#"%" :: _) = "" (* error *)
+ | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
+
+val escape_meta = String.translate meta_char
+val escape_metas = map escape_meta #> space_implode " "
+val unescape_meta = String.explode #> unmeta_chars []
+val unescape_metas =
+ space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
+
+fun extract_node line =
+ case space_explode ":" line of
+ [name, parents] => (unescape_meta name, unescape_metas parents)
+ | _ => ("", [])
+
+fun extract_suggestion sugg =
+ case space_explode "=" sugg of
+ [name, weight] =>
+ SOME (unescape_meta name, Real.fromString weight |> the_default 0.0)
+ | _ => NONE
+
+fun extract_query line =
+ case space_explode ":" line of
+ [goal, suggs] =>
+ (unescape_meta goal,
+ map_filter extract_suggestion (space_explode " " suggs))
+ | _ => ("", [])
+
+fun parent_of_local_thm th =
+ let
+ val thy = th |> Thm.theory_of_thm
+ val facts = thy |> Global_Theory.facts_of
+ val space = facts |> Facts.space_of
+ fun id_of s = #id (Name_Space.the_entry space s)
+ fun max_id (s', _) (s, id) =
+ let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
+ in ("", ~1) |> Facts.fold_static max_id facts |> fst end
+
+val local_prefix = "local" ^ Long_Name.separator
+
+fun nickname_of th =
+ if Thm.has_name_hint th then
+ let val hint = Thm.get_name_hint th in
+ (* FIXME: There must be a better way to detect local facts. *)
+ case try (unprefix local_prefix) hint of
+ SOME suf =>
+ parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf
+ | NONE => hint
+ end
+ else
+ backquote_thm th
+
+fun suggested_facts suggs facts =
+ let
+ fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
+ val tab = Symtab.empty |> fold add_fact facts
+ fun find_sugg (name, weight) =
+ Symtab.lookup tab name |> Option.map (rpair weight)
+ in map_filter find_sugg suggs end
+
+fun sum_avg [] = 0
+ | sum_avg xs =
+ Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
+
+fun normalize_scores [] = []
+ | normalize_scores ((fact, score) :: tail) =
+ (fact, 1.0) :: map (apsnd (curry Real.* (1.0 / score))) tail
+
+fun mesh_facts max_facts [(sels, unks)] =
+ map fst (take max_facts sels) @ take (max_facts - length sels) unks
+ | mesh_facts max_facts mess =
+ let
+ val mess = mess |> map (apfst (normalize_scores #> `length))
+ val fact_eq = Thm.eq_thm o pairself snd
+ fun score_at sels = try (nth sels) #> Option.map snd
+ fun score_in fact ((sel_len, sels), unks) =
+ case find_index (curry fact_eq fact o fst) sels of
+ ~1 => (case find_index (curry fact_eq fact) unks of
+ ~1 => score_at sels sel_len
+ | _ => NONE)
+ | rank => score_at sels rank
+ fun weight_of fact = mess |> map_filter (score_in fact) |> sum_avg
+ val facts =
+ fold (union fact_eq o map fst o take max_facts o snd o fst) mess []
+ in
+ facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
+ |> map snd |> take max_facts
+ end
+
+val thy_feature_name_of = prefix "y"
+val const_name_of = prefix "c"
+val type_name_of = prefix "t"
+val class_name_of = prefix "s"
+
+fun theory_ord p =
+ if Theory.eq_thy p then
+ EQUAL
+ else if Theory.subthy p then
+ LESS
+ else if Theory.subthy (swap p) then
+ GREATER
+ else case int_ord (pairself (length o Theory.ancestors_of) p) of
+ EQUAL => string_ord (pairself Context.theory_name p)
+ | order => order
+
+val thm_ord = theory_ord o pairself theory_of_thm
+
+val freezeT = Type.legacy_freeze_type
+
+fun freeze (t $ u) = freeze t $ freeze u
+ | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
+ | freeze (Var ((s, _), T)) = Free (s, freezeT T)
+ | freeze (Const (s, T)) = Const (s, freezeT T)
+ | freeze (Free (s, T)) = Free (s, freezeT T)
+ | freeze t = t
+
+fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
+
+fun run_prover_for_mash ctxt params prover facts goal =
+ let
+ val problem =
+ {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
+ facts = facts |> map (apfst (apfst (fn name => name ())))
+ |> map Untranslated_Fact}
+ in
+ get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
+ problem
+ end
+
+val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
+
+val logical_consts =
+ [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
+
+fun interesting_terms_types_and_classes ctxt prover term_max_depth
+ type_max_depth ts =
+ let
+ fun is_bad_const (x as (s, _)) args =
+ member (op =) logical_consts s orelse
+ fst (is_built_in_const_for_prover ctxt prover x args)
+ fun add_classes @{sort type} = I
+ | add_classes S = union (op =) (map class_name_of S)
+ fun do_add_type (Type (s, Ts)) =
+ (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
+ #> fold do_add_type Ts
+ | do_add_type (TFree (_, S)) = add_classes S
+ | do_add_type (TVar (_, S)) = add_classes S
+ fun add_type T = type_max_depth >= 0 ? do_add_type T
+ fun mk_app s args =
+ if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
+ else s
+ fun patternify ~1 _ = ""
+ | patternify depth t =
+ case strip_comb t of
+ (Const (x as (s, _)), args) =>
+ if is_bad_const x args then ""
+ else mk_app (const_name_of s) (map (patternify (depth - 1)) args)
+ | _ => ""
+ fun add_pattern depth t =
+ case patternify depth t of "" => I | s => insert (op =) s
+ fun add_term_patterns ~1 _ = I
+ | add_term_patterns depth t =
+ add_pattern depth t #> add_term_patterns (depth - 1) t
+ val add_term = add_term_patterns term_max_depth
+ fun add_patterns t =
+ let val (head, args) = strip_comb t in
+ (case head of
+ Const (_, T) => add_term t #> add_type T
+ | Free (_, T) => add_type T
+ | Var (_, T) => add_type T
+ | Abs (_, T, body) => add_type T #> add_patterns body
+ | _ => I)
+ #> fold add_patterns args
+ end
+ in [] |> fold add_patterns ts end
+
+fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
+
+val term_max_depth = 1
+val type_max_depth = 1
+
+(* TODO: Generate type classes for types? *)
+fun features_of ctxt prover thy (scope, status) ts =
+ thy_feature_name_of (Context.theory_name thy) ::
+ interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
+ ts
+ |> forall is_lambda_free ts ? cons "no_lams"
+ |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
+ |> scope <> Global ? cons "local"
+ |> (case status of
+ General => I
+ | Induction => cons "induction"
+ | Intro => cons "intro"
+ | Inductive => cons "inductive"
+ | Elim => cons "elim"
+ | Simp => cons "simp"
+ | Def => cons "def")
+
+(* Too many dependencies is a sign that a decision procedure is at work. There
+ isn't much too learn from such proofs. *)
+val max_dependencies = 10
+val atp_dependency_default_max_fact = 50
+
+fun trim_dependencies deps =
+ if length deps <= max_dependencies then SOME deps else NONE
+
+fun isar_dependencies_of all_names =
+ thms_in_proof (SOME all_names) #> trim_dependencies
+
+fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
+ auto_level facts all_names th =
+ case isar_dependencies_of all_names th of
+ SOME [] => NONE
+ | isar_deps =>
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val goal = goal_of_thm thy th
+ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
+ val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+ fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
+ fun is_dep dep (_, th) = nickname_of th = dep
+ fun add_isar_dep facts dep accum =
+ if exists (is_dep dep) accum then
+ accum
+ else case find_first (is_dep dep) facts of
+ SOME ((name, status), th) => accum @ [((name, status), th)]
+ | NONE => accum (* shouldn't happen *)
+ val facts =
+ facts |> mepo_suggested_facts ctxt params prover
+ (max_facts |> the_default atp_dependency_default_max_fact)
+ NONE hyp_ts concl_t
+ |> fold (add_isar_dep facts) (these isar_deps)
+ |> map fix_name
+ in
+ if verbose andalso auto_level = 0 then
+ let val num_facts = length facts in
+ "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^
+ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
+ "."
+ |> Output.urgent_message
+ end
+ else
+ ();
+ case run_prover_for_mash ctxt params prover facts goal of
+ {outcome = NONE, used_facts, ...} =>
+ (if verbose andalso auto_level = 0 then
+ let val num_facts = length used_facts in
+ "Found proof with " ^ string_of_int num_facts ^ " fact" ^
+ plural_s num_facts ^ "."
+ |> Output.urgent_message
+ end
+ else
+ ();
+ used_facts |> map fst |> trim_dependencies)
+ | _ => NONE
+ end
+
+
+(*** Low-level communication with MaSh ***)
+
+(* more friendly than "try o File.rm" for those who keep the files open in their
+ text editor *)
+fun wipe_out file = File.write file ""
+
+fun write_file (xs, f) file =
+ let val path = Path.explode file in
+ wipe_out path;
+ xs |> chunk_list 500
+ |> List.app (File.append path o space_implode "" o map f)
+ end
+
+fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
+ let
+ val (temp_dir, serial) =
+ if overlord then (getenv "ISABELLE_HOME_USER", "")
+ else (getenv "ISABELLE_TMP", serial_string ())
+ val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null"
+ val err_file = temp_dir ^ "/mash_err" ^ serial
+ val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
+ val cmd_file = temp_dir ^ "/mash_commands" ^ serial
+ val core =
+ "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
+ " --numberOfPredictions " ^ string_of_int max_suggs ^
+ (if save then " --saveModel" else "")
+ val command =
+ mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
+ " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
+ in
+ write_file ([], K "") sugg_file;
+ write_file write_cmds cmd_file;
+ trace_msg ctxt (fn () => "Running " ^ command);
+ Isabelle_System.bash command;
+ read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
+ |> tap (fn _ => trace_msg ctxt (fn () =>
+ case try File.read (Path.explode err_file) of
+ NONE => "Done"
+ | SOME "" => "Done"
+ | SOME s => "Error: " ^ elide_string 1000 s))
+ |> not overlord
+ ? tap (fn _ => List.app (wipe_out o Path.explode)
+ [err_file, sugg_file, cmd_file])
+ end
+
+fun str_of_add (name, parents, feats, deps) =
+ "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
+ escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
+
+fun str_of_reprove (name, deps) =
+ "p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
+
+fun str_of_query (parents, feats) =
+ "? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n"
+
+fun mash_CLEAR ctxt =
+ let val path = mash_model_dir () |> Path.explode in
+ trace_msg ctxt (K "MaSh CLEAR");
+ File.fold_dir (fn file => fn _ =>
+ try File.rm (Path.append path (Path.basic file)))
+ path NONE;
+ ()
+ end
+
+fun mash_ADD _ _ [] = ()
+ | mash_ADD ctxt overlord adds =
+ (trace_msg ctxt (fn () => "MaSh ADD " ^
+ elide_string 1000 (space_implode " " (map #1 adds)));
+ run_mash_tool ctxt overlord true 0 (adds, str_of_add) (K ()))
+
+fun mash_REPROVE _ _ [] = ()
+ | mash_REPROVE ctxt overlord reps =
+ (trace_msg ctxt (fn () => "MaSh REPROVE " ^
+ elide_string 1000 (space_implode " " (map #1 reps)));
+ run_mash_tool ctxt overlord true 0 (reps, str_of_reprove) (K ()))
+
+fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
+ (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
+ run_mash_tool ctxt overlord false max_suggs
+ ([query], str_of_query)
+ (fn suggs =>
+ case suggs () of
+ [] => []
+ | suggs => snd (extract_query (List.last suggs)))
+ handle List.Empty => [])
+
+
+(*** High-level communication with MaSh ***)
+
+fun try_graph ctxt when def f =
+ f ()
+ handle Graph.CYCLES (cycle :: _) =>
+ (trace_msg ctxt (fn () =>
+ "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
+ | Graph.DUP name =>
+ (trace_msg ctxt (fn () =>
+ "Duplicate fact " ^ quote name ^ " when " ^ when); def)
+ | Graph.UNDEF name =>
+ (trace_msg ctxt (fn () =>
+ "Unknown fact " ^ quote name ^ " when " ^ when); def)
+ | exn =>
+ if Exn.is_interrupt exn then
+ reraise exn
+ else
+ (trace_msg ctxt (fn () =>
+ "Internal error when " ^ when ^ ":\n" ^
+ ML_Compiler.exn_message exn); def)
+
+fun graph_info G =
+ string_of_int (length (Graph.keys G)) ^ " node(s), " ^
+ string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^
+ " edge(s), " ^
+ string_of_int (length (Graph.minimals G)) ^ " minimal, " ^
+ string_of_int (length (Graph.maximals G)) ^ " maximal"
+
+type mash_state = {fact_G : unit Graph.T}
+
+val empty_state = {fact_G = Graph.empty}
+
+local
+
+val version = "*** MaSh 0.0 ***"
+
+fun load _ (state as (true, _)) = state
+ | load ctxt _ =
+ let val path = mash_state_path () in
+ (true,
+ case try File.read_lines path of
+ SOME (version' :: node_lines) =>
+ let
+ fun add_edge_to name parent =
+ Graph.default_node (parent, ()) #> Graph.add_edge (parent, name)
+ fun add_node line =
+ case extract_node line of
+ ("", _) => I (* shouldn't happen *)
+ | (name, parents) =>
+ Graph.default_node (name, ()) #> fold (add_edge_to name) parents
+ val fact_G =
+ try_graph ctxt "loading state" Graph.empty (fn () =>
+ Graph.empty |> version' = version ? fold add_node node_lines)
+ in
+ trace_msg ctxt (fn () =>
+ "Loaded fact graph (" ^ graph_info fact_G ^ ")");
+ {fact_G = fact_G}
+ end
+ | _ => empty_state)
+ end
+
+fun save ctxt {fact_G} =
+ let
+ val path = mash_state_path ()
+ fun fact_line_for name parents =
+ escape_meta name ^ ": " ^ escape_metas parents
+ val append_fact = File.append path o suffix "\n" oo fact_line_for
+ fun append_entry (name, ((), (parents, _))) () =
+ append_fact name (Graph.Keys.dest parents)
+ in
+ File.write path (version ^ "\n");
+ Graph.fold append_entry fact_G ();
+ trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")")
+ end
+
+val global_state =
+ Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
+
+in
+
+fun mash_map ctxt f =
+ Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt)))
+
+fun mash_get ctxt =
+ Synchronized.change_result global_state (load ctxt #> `snd)
+
+fun mash_unlearn ctxt =
+ Synchronized.change global_state (fn _ =>
+ (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
+
+end
+
+fun mash_could_suggest_facts () = mash_home () <> ""
+fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
+
+fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
+
+fun maximal_in_graph fact_G facts =
+ let
+ val facts = [] |> fold (cons o nickname_of o snd) facts
+ val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
+ fun insert_new seen name =
+ not (Symtab.defined seen name) ? insert (op =) name
+ fun find_maxes _ (maxs, []) = map snd maxs
+ | find_maxes seen (maxs, new :: news) =
+ find_maxes
+ (seen |> num_keys (Graph.imm_succs fact_G new) > 1
+ ? Symtab.default (new, ()))
+ (if Symtab.defined tab new then
+ let
+ val newp = Graph.all_preds fact_G [new]
+ fun is_ancestor x yp = member (op =) yp x
+ val maxs =
+ maxs |> filter (fn (_, max) => not (is_ancestor max newp))
+ in
+ if exists (is_ancestor new o fst) maxs then
+ (maxs, news)
+ else
+ ((newp, new)
+ :: filter_out (fn (_, max) => is_ancestor max newp) maxs,
+ news)
+ end
+ else
+ (maxs, Graph.Keys.fold (insert_new seen)
+ (Graph.imm_preds fact_G new) news))
+ in find_maxes Symtab.empty ([], Graph.maximals fact_G) end
+
+(* Generate more suggestions than requested, because some might be thrown out
+ later for various reasons and "meshing" gives better results with some
+ slack. *)
+fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
+
+fun is_fact_in_graph fact_G (_, th) =
+ can (Graph.get_node fact_G) (nickname_of th)
+
+fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
+ concl_t facts =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val fact_G = #fact_G (mash_get ctxt)
+ val parents = maximal_in_graph fact_G facts
+ val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
+ val suggs =
+ if Graph.is_empty fact_G then []
+ else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
+ val selected =
+ facts |> suggested_facts suggs
+ (* The weights currently returned by "mash.py" are too extreme to
+ make any sense. *)
+ |> map fst |> weight_mepo_facts
+ val unknown = facts |> filter_out (is_fact_in_graph fact_G)
+ in (selected, unknown) end
+
+fun add_to_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
+ let
+ fun maybe_add_from from (accum as (parents, graph)) =
+ try_graph ctxt "updating graph" accum (fn () =>
+ (from :: parents, Graph.add_edge_acyclic (from, name) graph))
+ val graph = graph |> Graph.default_node (name, ())
+ val (parents, graph) = ([], graph) |> fold maybe_add_from parents
+ val (deps, _) = ([], graph) |> fold maybe_add_from deps
+ in ((name, parents, feats, deps) :: adds, graph) end
+
+val learn_timeout_slack = 2.0
+
+fun launch_thread timeout task =
+ let
+ val hard_timeout = time_mult learn_timeout_slack timeout
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, hard_timeout)
+ val desc = ("machine learner for Sledgehammer", "")
+ in Async_Manager.launch MaShN birth_time death_time desc task end
+
+fun freshish_name () =
+ Date.fmt ".%Y_%m_%d_%H_%M_%S__" (Date.fromTimeLocal (Time.now ())) ^
+ serial_string ()
+
+fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts
+ used_ths =
+ if is_smt_prover ctxt prover then
+ ()
+ else
+ launch_thread timeout (fn () =>
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val name = freshish_name ()
+ val feats = features_of ctxt prover thy (Local, General) [t]
+ val deps = used_ths |> map nickname_of
+ val {fact_G} = mash_get ctxt
+ val parents = maximal_in_graph fact_G facts
+ in
+ mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
+ end)
+
+fun sendback sub =
+ Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
+
+val commit_timeout = seconds 30.0
+
+(* The timeout is understood in a very slack fashion. *)
+fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
+ auto_level atp learn_timeout facts =
+ let
+ val timer = Timer.startRealTimer ()
+ fun next_commit_time () =
+ Time.+ (Timer.checkRealTimer timer, commit_timeout)
+ val {fact_G} = mash_get ctxt
+ val (old_facts, new_facts) =
+ facts |> List.partition (is_fact_in_graph fact_G)
+ ||> sort (thm_ord o pairself snd)
+ in
+ if null new_facts andalso (not atp orelse null old_facts) then
+ if auto_level < 2 then
+ "No new " ^ (if atp then "ATP" else "Isar") ^ " proofs to learn." ^
+ (if auto_level = 0 andalso not atp then
+ "\n\nHint: Try " ^ sendback learn_atpN ^ " to learn from ATP proofs."
+ else
+ "")
+ else
+ ""
+ else
+ let
+ val all_names =
+ facts |> map snd
+ |> filter_out is_likely_tautology_or_too_meta
+ |> map (rpair () o nickname_of)
+ |> Symtab.make
+ val deps_of =
+ if atp then
+ atp_dependencies_of ctxt params prover auto_level facts all_names
+ else
+ isar_dependencies_of all_names
+ fun do_commit [] [] state = state
+ | do_commit adds reps {fact_G} =
+ let
+ val (adds, fact_G) =
+ ([], fact_G) |> fold (add_to_fact_graph ctxt) adds
+ in
+ mash_ADD ctxt overlord (rev adds);
+ mash_REPROVE ctxt overlord reps;
+ {fact_G = fact_G}
+ end
+ fun commit last adds reps =
+ (if debug andalso auto_level = 0 then
+ Output.urgent_message "Committing..."
+ else
+ ();
+ mash_map ctxt (do_commit (rev adds) reps);
+ if not last andalso auto_level = 0 then
+ let val num_proofs = length adds + length reps in
+ "Learned " ^ string_of_int num_proofs ^ " " ^
+ (if atp then "ATP" else "Isar") ^ " proof" ^
+ plural_s num_proofs ^ " in the last " ^
+ string_from_time commit_timeout ^ "."
+ |> Output.urgent_message
+ end
+ else
+ ())
+ fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
+ | learn_new_fact ((_, stature), th)
+ (adds, (parents, n, next_commit, _)) =
+ let
+ val name = nickname_of th
+ val feats =
+ features_of ctxt prover (theory_of_thm th) stature [prop_of th]
+ val deps = deps_of th |> these
+ val n = n |> not (null deps) ? Integer.add 1
+ val adds = (name, parents, feats, deps) :: adds
+ val (adds, next_commit) =
+ if Time.> (Timer.checkRealTimer timer, next_commit) then
+ (commit false adds []; ([], next_commit_time ()))
+ else
+ (adds, next_commit)
+ val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+ in (adds, ([name], n, next_commit, timed_out)) end
+ val n =
+ if null new_facts then
+ 0
+ else
+ let
+ val last_th = new_facts |> List.last |> snd
+ (* crude approximation *)
+ val ancestors =
+ old_facts
+ |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER)
+ val parents = maximal_in_graph fact_G ancestors
+ val (adds, (_, n, _, _)) =
+ ([], (parents, 0, next_commit_time (), false))
+ |> fold learn_new_fact new_facts
+ in commit true adds []; n end
+ fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
+ | relearn_old_fact (_, th) (reps, (n, next_commit, _)) =
+ let
+ val name = nickname_of th
+ val (n, reps) =
+ case deps_of th of
+ SOME deps => (n + 1, (name, deps) :: reps)
+ | NONE => (n, reps)
+ val (reps, next_commit) =
+ if Time.> (Timer.checkRealTimer timer, next_commit) then
+ (commit false [] reps; ([], next_commit_time ()))
+ else
+ (reps, next_commit)
+ val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+ in (reps, (n, next_commit, timed_out)) end
+ val n =
+ if null old_facts then
+ n
+ else
+ let
+ fun priority_of (_, th) =
+ random_range 0 (1000 * max_dependencies)
+ - 500 * (th |> isar_dependencies_of all_names
+ |> Option.map length
+ |> the_default max_dependencies)
+ val old_facts =
+ old_facts |> map (`priority_of)
+ |> sort (int_ord o pairself fst)
+ |> map snd
+ val (reps, (n, _, _)) =
+ ([], (n, next_commit_time (), false))
+ |> fold relearn_old_fact old_facts
+ in commit true [] reps; n end
+ in
+ if verbose orelse auto_level < 2 then
+ "Learned " ^ string_of_int n ^ " nontrivial " ^
+ (if atp then "ATP" else "Isar") ^ " proof" ^ plural_s n ^
+ (if verbose then
+ " in " ^ string_from_time (Timer.checkRealTimer timer)
+ else
+ "") ^ "."
+ else
+ ""
+ end
+ end
+
+fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained
+ atp =
+ let
+ val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+ val ctxt = ctxt |> Config.put instantiate_inducts false
+ val facts =
+ nearly_all_facts ctxt false fact_override Symtab.empty css chained []
+ @{prop True}
+ val num_facts = length facts
+ val prover = hd provers
+ fun learn auto_level atp =
+ mash_learn_facts ctxt params prover auto_level atp infinite_timeout facts
+ |> Output.urgent_message
+ in
+ (if atp then
+ ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
+ plural_s num_facts ^ " for ATP proofs (" ^ quote prover ^ " timeout: " ^
+ string_from_time timeout ^ ").\n\nCollecting Isar proofs first..."
+ |> Output.urgent_message;
+ learn 1 false;
+ "Now collecting ATP proofs. This may take several hours. You can \
+ \safely stop the learning process at any point."
+ |> Output.urgent_message;
+ learn 0 true)
+ else
+ ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
+ plural_s num_facts ^ " for Isar proofs..."
+ |> Output.urgent_message;
+ learn 0 false))
+ end
+
+(* The threshold should be large enough so that MaSh doesn't kick in for Auto
+ Sledgehammer and Try. *)
+val min_secs_for_learning = 15
+
+fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
+ max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
+ if not (subset (op =) (the_list fact_filter, fact_filters)) then
+ error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
+ else if only then
+ facts
+ else if max_facts <= 0 orelse null facts then
+ []
+ else
+ let
+ fun maybe_learn () =
+ if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
+ Time.toSeconds timeout >= min_secs_for_learning then
+ let val timeout = time_mult learn_timeout_slack timeout in
+ launch_thread timeout
+ (fn () => (true, mash_learn_facts ctxt params prover 2 false
+ timeout facts))
+ end
+ else
+ ()
+ val fact_filter =
+ case fact_filter of
+ SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
+ | NONE =>
+ if is_smt_prover ctxt prover then
+ mepoN
+ else if mash_could_suggest_facts () then
+ (maybe_learn ();
+ if mash_can_suggest_facts ctxt then meshN else mepoN)
+ else
+ mepoN
+ val add_ths = Attrib.eval_thms ctxt add
+ fun prepend_facts ths accepts =
+ ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
+ (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
+ |> take max_facts
+ fun mepo () =
+ facts |> mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts
+ concl_t
+ |> weight_mepo_facts
+ fun mash () =
+ mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts
+ val mess =
+ [] |> (if fact_filter <> mashN then cons (mepo (), []) else I)
+ |> (if fact_filter <> mepoN then cons (mash ()) else I)
+ in
+ mesh_facts max_facts mess
+ |> not (null add_ths) ? prepend_facts add_ths
+ end
+
+fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
+fun running_learners () = Async_Manager.running_threads MaShN "learner"
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Jul 20 23:38:15 2012 +0200
@@ -0,0 +1,545 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
+ Author: Jasmin Blanchette, TU Muenchen
+
+Sledgehammer's iterative relevance filter (MePo = Meng-Paulson).
+*)
+
+signature SLEDGEHAMMER_MEPO =
+sig
+ type stature = ATP_Problem_Generate.stature
+ type fact = Sledgehammer_Fact.fact
+ type params = Sledgehammer_Provers.params
+ type relevance_fudge = Sledgehammer_Provers.relevance_fudge
+
+ val trace : bool Config.T
+ val pseudo_abs_name : string
+ val pseudo_skolem_prefix : string
+ val const_names_in_fact :
+ theory -> (string * typ -> term list -> bool * term list) -> term
+ -> string list
+ val mepo_suggested_facts :
+ Proof.context -> params -> string -> int -> relevance_fudge option
+ -> term list -> term -> fact list -> fact list
+ val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
+end;
+
+structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
+struct
+
+open ATP_Problem_Generate
+open Sledgehammer_Fact
+open Sledgehammer_Provers
+
+val trace =
+ Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false)
+fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
+
+val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+val pseudo_abs_name = sledgehammer_prefix ^ "abs"
+val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
+val theory_const_suffix = Long_Name.separator ^ " 1"
+
+fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
+ Int.max (order_of_type T1 + 1, order_of_type T2)
+ | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
+ | order_of_type _ = 0
+
+(* An abstraction of Isabelle types and first-order terms *)
+datatype pattern = PVar | PApp of string * pattern list
+datatype ptype = PType of int * pattern list
+
+fun string_for_pattern PVar = "_"
+ | string_for_pattern (PApp (s, ps)) =
+ if null ps then s else s ^ string_for_patterns ps
+and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
+fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
+
+(*Is the second type an instance of the first one?*)
+fun match_pattern (PVar, _) = true
+ | match_pattern (PApp _, PVar) = false
+ | match_pattern (PApp (s, ps), PApp (t, qs)) =
+ s = t andalso match_patterns (ps, qs)
+and match_patterns (_, []) = true
+ | match_patterns ([], _) = false
+ | match_patterns (p :: ps, q :: qs) =
+ match_pattern (p, q) andalso match_patterns (ps, qs)
+fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
+
+(* Is there a unifiable constant? *)
+fun pconst_mem f consts (s, ps) =
+ exists (curry (match_ptype o f) ps)
+ (map snd (filter (curry (op =) s o fst) consts))
+fun pconst_hyper_mem f const_tab (s, ps) =
+ exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
+
+fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
+ | pattern_for_type (TFree (s, _)) = PApp (s, [])
+ | pattern_for_type (TVar _) = PVar
+
+(* Pairs a constant with the list of its type instantiations. *)
+fun ptype thy const x =
+ (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
+ else [])
+fun rich_ptype thy const (s, T) =
+ PType (order_of_type T, ptype thy const (s, T))
+fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
+
+fun string_for_hyper_pconst (s, ps) =
+ s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
+
+(* Add a pconstant to the table, but a [] entry means a standard
+ connective, which we ignore.*)
+fun add_pconst_to_table also_skolem (s, p) =
+ if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I
+ else Symtab.map_default (s, [p]) (insert (op =) p)
+
+(* Set constants tend to pull in too many irrelevant facts. We limit the damage
+ by treating them more or less as if they were built-in but add their
+ axiomatization at the end. *)
+val set_consts = [@{const_name Collect}, @{const_name Set.member}]
+val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
+
+fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
+ let
+ val flip = Option.map not
+ (* We include free variables, as well as constants, to handle locales. For
+ each quantifiers that must necessarily be skolemized by the automatic
+ prover, we introduce a fresh constant to simulate the effect of
+ Skolemization. *)
+ fun do_const const ext_arg (x as (s, _)) ts =
+ let val (built_in, ts) = is_built_in_const x ts in
+ if member (op =) set_consts s then
+ fold (do_term ext_arg) ts
+ else
+ (not built_in
+ ? add_pconst_to_table also_skolems (rich_pconst thy const x))
+ #> fold (do_term false) ts
+ end
+ and do_term ext_arg t =
+ case strip_comb t of
+ (Const x, ts) => do_const true ext_arg x ts
+ | (Free x, ts) => do_const false ext_arg x ts
+ | (Abs (_, T, t'), ts) =>
+ ((null ts andalso not ext_arg)
+ (* Since lambdas on the right-hand side of equalities are usually
+ extensionalized later by "abs_extensionalize_term", we don't
+ penalize them here. *)
+ ? add_pconst_to_table true (pseudo_abs_name,
+ PType (order_of_type T + 1, [])))
+ #> fold (do_term false) (t' :: ts)
+ | (_, ts) => fold (do_term false) ts
+ fun do_quantifier will_surely_be_skolemized abs_T body_t =
+ do_formula pos body_t
+ #> (if also_skolems andalso will_surely_be_skolemized then
+ add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (),
+ PType (order_of_type abs_T, []))
+ else
+ I)
+ and do_term_or_formula ext_arg T =
+ if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
+ and do_formula pos t =
+ case t of
+ Const (@{const_name all}, _) $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME false) T t'
+ | @{const "==>"} $ t1 $ t2 =>
+ do_formula (flip pos) t1 #> do_formula pos t2
+ | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
+ do_term_or_formula false T t1 #> do_term_or_formula true T t2
+ | @{const Trueprop} $ t1 => do_formula pos t1
+ | @{const False} => I
+ | @{const True} => I
+ | @{const Not} $ t1 => do_formula (flip pos) t1
+ | Const (@{const_name All}, _) $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME false) T t'
+ | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME true) T t'
+ | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const HOL.implies} $ t1 $ t2 =>
+ do_formula (flip pos) t1 #> do_formula pos t2
+ | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
+ do_term_or_formula false T t1 #> do_term_or_formula true T t2
+ | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
+ $ t1 $ t2 $ t3 =>
+ do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
+ | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
+ do_quantifier (is_some pos) T t'
+ | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME false) T
+ (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
+ | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME true) T
+ (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
+ | (t0 as Const (_, @{typ bool})) $ t1 =>
+ do_term false t0 #> do_formula pos t1 (* theory constant *)
+ | _ => do_term false t
+ in do_formula pos end
+
+fun pconsts_in_fact thy is_built_in_const t =
+ Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
+ (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
+ (SOME true) t) []
+
+val const_names_in_fact = map fst ooo pconsts_in_fact
+
+(* Inserts a dummy "constant" referring to the theory name, so that relevance
+ takes the given theory into account. *)
+fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
+ : relevance_fudge) thy_name t =
+ if exists (curry (op <) 0.0) [theory_const_rel_weight,
+ theory_const_irrel_weight] then
+ Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
+ else
+ t
+
+fun theory_const_prop_of fudge th =
+ theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
+
+fun pair_consts_fact thy is_built_in_const fudge fact =
+ case fact |> snd |> theory_const_prop_of fudge
+ |> pconsts_in_fact thy is_built_in_const of
+ [] => NONE
+ | consts => SOME ((fact, consts), NONE)
+
+(* A two-dimensional symbol table counts frequencies of constants. It's keyed
+ first by constant name and second by its list of type instantiations. For the
+ latter, we need a linear ordering on "pattern list". *)
+
+fun pattern_ord p =
+ case p of
+ (PVar, PVar) => EQUAL
+ | (PVar, PApp _) => LESS
+ | (PApp _, PVar) => GREATER
+ | (PApp q1, PApp q2) =>
+ prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
+fun ptype_ord (PType p, PType q) =
+ prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
+
+structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
+
+fun count_fact_consts thy fudge =
+ let
+ fun do_const const (s, T) ts =
+ (* Two-dimensional table update. Constant maps to types maps to count. *)
+ PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
+ |> Symtab.map_default (s, PType_Tab.empty)
+ #> fold do_term ts
+ and do_term t =
+ case strip_comb t of
+ (Const x, ts) => do_const true x ts
+ | (Free x, ts) => do_const false x ts
+ | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
+ | (_, ts) => fold do_term ts
+ in do_term o theory_const_prop_of fudge o snd end
+
+fun pow_int _ 0 = 1.0
+ | pow_int x 1 = x
+ | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
+
+(*The frequency of a constant is the sum of those of all instances of its type.*)
+fun pconst_freq match const_tab (c, ps) =
+ PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
+ (the (Symtab.lookup const_tab c)) 0
+
+
+(* A surprising number of theorems contain only a few significant constants.
+ These include all induction rules, and other general theorems. *)
+
+(* "log" seems best in practice. A constant function of one ignores the constant
+ frequencies. Rare constants give more points if they are relevant than less
+ rare ones. *)
+fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
+
+(* Irrelevant constants are treated differently. We associate lower penalties to
+ very rare constants and very common ones -- the former because they can't
+ lead to the inclusion of too many new facts, and the latter because they are
+ so common as to be of little interest. *)
+fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
+ : relevance_fudge) order freq =
+ let val (k, x) = worse_irrel_freq |> `Real.ceil in
+ (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
+ else rel_weight_for order freq / rel_weight_for order k)
+ * pow_int higher_order_irrel_weight (order - 1)
+ end
+
+fun multiplier_for_const_name local_const_multiplier s =
+ if String.isSubstring "." s then 1.0 else local_const_multiplier
+
+(* Computes a constant's weight, as determined by its frequency. *)
+fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
+ theory_const_weight chained_const_weight weight_for f
+ const_tab chained_const_tab (c as (s, PType (m, _))) =
+ if s = pseudo_abs_name then
+ abs_weight
+ else if String.isPrefix pseudo_skolem_prefix s then
+ skolem_weight
+ else if String.isSuffix theory_const_suffix s then
+ theory_const_weight
+ else
+ multiplier_for_const_name local_const_multiplier s
+ * weight_for m (pconst_freq (match_ptype o f) const_tab c)
+ |> (if chained_const_weight < 1.0 andalso
+ pconst_hyper_mem I chained_const_tab c then
+ curry (op *) chained_const_weight
+ else
+ I)
+
+fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
+ theory_const_rel_weight, ...} : relevance_fudge)
+ const_tab =
+ generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
+ theory_const_rel_weight 0.0 rel_weight_for I const_tab
+ Symtab.empty
+
+fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
+ skolem_irrel_weight,
+ theory_const_irrel_weight,
+ chained_const_irrel_weight, ...})
+ const_tab chained_const_tab =
+ generic_pconst_weight local_const_multiplier abs_irrel_weight
+ skolem_irrel_weight theory_const_irrel_weight
+ chained_const_irrel_weight (irrel_weight_for fudge) swap
+ const_tab chained_const_tab
+
+fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
+ intro_bonus
+ | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
+ | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
+ | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
+ | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
+ | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
+ | stature_bonus _ _ = 0.0
+
+fun is_odd_const_name s =
+ s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
+ String.isSuffix theory_const_suffix s
+
+fun fact_weight fudge stature const_tab relevant_consts chained_consts
+ fact_consts =
+ case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
+ ||> filter_out (pconst_hyper_mem swap relevant_consts) of
+ ([], _) => 0.0
+ | (rel, irrel) =>
+ if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
+ 0.0
+ else
+ let
+ val irrel = irrel |> filter_out (pconst_mem swap rel)
+ val rel_weight =
+ 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
+ val irrel_weight =
+ ~ (stature_bonus fudge stature)
+ |> fold (curry (op +)
+ o irrel_pconst_weight fudge const_tab chained_consts) irrel
+ val res = rel_weight / (rel_weight + irrel_weight)
+ in if Real.isFinite res then res else 0.0 end
+
+fun take_most_relevant ctxt max_facts remaining_max
+ ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
+ (candidates : ((fact * (string * ptype) list) * real) list) =
+ let
+ val max_imperfect =
+ Real.ceil (Math.pow (max_imperfect,
+ Math.pow (Real.fromInt remaining_max
+ / Real.fromInt max_facts, max_imperfect_exp)))
+ val (perfect, imperfect) =
+ candidates |> sort (Real.compare o swap o pairself snd)
+ |> take_prefix (fn (_, w) => w > 0.99999)
+ val ((accepts, more_rejects), rejects) =
+ chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
+ in
+ trace_msg ctxt (fn () =>
+ "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
+ string_of_int (length candidates) ^ "): " ^
+ (accepts |> map (fn ((((name, _), _), _), weight) =>
+ name () ^ " [" ^ Real.toString weight ^ "]")
+ |> commas));
+ (accepts, more_rejects @ rejects)
+ end
+
+fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
+ if Symtab.is_empty tab then
+ Symtab.empty
+ |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
+ (map_filter (fn ((_, (sc', _)), th) =>
+ if sc' = sc then SOME (prop_of th) else NONE) facts)
+ else
+ tab
+
+fun consider_arities is_built_in_const th =
+ let
+ fun aux _ _ NONE = NONE
+ | aux t args (SOME tab) =
+ case t of
+ t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
+ | Const (x as (s, _)) =>
+ (if is_built_in_const x args |> fst then
+ SOME tab
+ else case Symtab.lookup tab s of
+ NONE => SOME (Symtab.update (s, length args) tab)
+ | SOME n => if n = length args then SOME tab else NONE)
+ | _ => SOME tab
+ in aux (prop_of th) [] end
+
+(* FIXME: This is currently only useful for polymorphic type encodings. *)
+fun could_benefit_from_ext is_built_in_const facts =
+ fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
+ |> is_none
+
+(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
+ weights), but low enough so that it is unlikely to be truncated away if few
+ facts are included. *)
+val special_fact_index = 75
+
+fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
+ (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
+ concl_t =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
+ val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
+ val chained_ts =
+ facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
+ | _ => NONE)
+ val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
+ val goal_const_tab =
+ Symtab.empty |> fold (add_pconsts true) hyp_ts
+ |> add_pconsts false concl_t
+ |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
+ |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
+ [Chained, Assum, Local]
+ fun iter j remaining_max thres rel_const_tab hopeless hopeful =
+ let
+ fun relevant [] _ [] =
+ (* Nothing has been added this iteration. *)
+ if j = 0 andalso thres >= ridiculous_threshold then
+ (* First iteration? Try again. *)
+ iter 0 max_facts (thres / threshold_divisor) rel_const_tab
+ hopeless hopeful
+ else
+ []
+ | relevant candidates rejects [] =
+ let
+ val (accepts, more_rejects) =
+ take_most_relevant ctxt max_facts remaining_max fudge candidates
+ val rel_const_tab' =
+ rel_const_tab
+ |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
+ fun is_dirty (c, _) =
+ Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
+ val (hopeful_rejects, hopeless_rejects) =
+ (rejects @ hopeless, ([], []))
+ |-> fold (fn (ax as (_, consts), old_weight) =>
+ if exists is_dirty consts then
+ apfst (cons (ax, NONE))
+ else
+ apsnd (cons (ax, old_weight)))
+ |>> append (more_rejects
+ |> map (fn (ax as (_, consts), old_weight) =>
+ (ax, if exists is_dirty consts then NONE
+ else SOME old_weight)))
+ val thres =
+ 1.0 - (1.0 - thres)
+ * Math.pow (decay, Real.fromInt (length accepts))
+ val remaining_max = remaining_max - length accepts
+ in
+ trace_msg ctxt (fn () => "New or updated constants: " ^
+ commas (rel_const_tab' |> Symtab.dest
+ |> subtract (op =) (rel_const_tab |> Symtab.dest)
+ |> map string_for_hyper_pconst));
+ map (fst o fst) accepts @
+ (if remaining_max = 0 then
+ []
+ else
+ iter (j + 1) remaining_max thres rel_const_tab'
+ hopeless_rejects hopeful_rejects)
+ end
+ | relevant candidates rejects
+ (((ax as (((_, stature), _), fact_consts)), cached_weight)
+ :: hopeful) =
+ let
+ val weight =
+ case cached_weight of
+ SOME w => w
+ | NONE => fact_weight fudge stature const_tab rel_const_tab
+ chained_const_tab fact_consts
+ in
+ if weight >= thres then
+ relevant ((ax, weight) :: candidates) rejects hopeful
+ else
+ relevant candidates ((ax, weight) :: rejects) hopeful
+ end
+ in
+ trace_msg ctxt (fn () =>
+ "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
+ Real.toString thres ^ ", constants: " ^
+ commas (rel_const_tab |> Symtab.dest
+ |> filter (curry (op <>) [] o snd)
+ |> map string_for_hyper_pconst));
+ relevant [] [] hopeful
+ end
+ fun uses_const s t =
+ fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
+ false
+ fun uses_const_anywhere accepts s =
+ exists (uses_const s o prop_of o snd) accepts orelse
+ exists (uses_const s) (concl_t :: hyp_ts)
+ fun add_set_const_thms accepts =
+ exists (uses_const_anywhere accepts) set_consts ? append set_thms
+ fun insert_into_facts accepts [] = accepts
+ | insert_into_facts accepts ths =
+ let
+ val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
+ val (bef, after) =
+ accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
+ |> take (max_facts - length add)
+ |> chop special_fact_index
+ in bef @ add @ after end
+ fun insert_special_facts accepts =
+ (* FIXME: get rid of "ext" here once it is treated as a helper *)
+ [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
+ |> add_set_const_thms accepts
+ |> insert_into_facts accepts
+ in
+ facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
+ |> iter 0 max_facts thres0 goal_const_tab []
+ |> insert_special_facts
+ |> tap (fn accepts => trace_msg ctxt (fn () =>
+ "Total relevant: " ^ string_of_int (length accepts)))
+ end
+
+fun mepo_suggested_facts ctxt
+ ({fact_thresholds = (thres0, thres1), ...} : params) prover
+ max_facts fudge hyp_ts concl_t facts =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val is_built_in_const =
+ Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover
+ val fudge =
+ case fudge of
+ SOME fudge => fudge
+ | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover
+ val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
+ 1.0 / Real.fromInt (max_facts + 1))
+ in
+ trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
+ " facts");
+ (if thres1 < 0.0 then
+ facts
+ else if thres0 > 1.0 orelse thres0 > thres1 then
+ []
+ else
+ relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
+ facts hyp_ts
+ (concl_t |> theory_constify fudge (Context.theory_name thy)))
+ end
+
+(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
+fun weight_of_fact rank =
+ Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
+
+fun weight_mepo_facts facts =
+ facts ~~ map weight_of_fact (0 upto length facts - 1)
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 23:38:15 2012 +0200
@@ -17,15 +17,15 @@
val auto_minimize_min_facts : int Config.T
val auto_minimize_max_time : real Config.T
val minimize_facts :
- (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state
- -> ((string * stature) * thm list) list
+ (string -> thm list -> unit) -> string -> params -> bool -> int -> int
+ -> Proof.state -> ((string * stature) * thm list) list
-> ((string * stature) * thm list) list option
* ((unit -> play) * (play -> string) * string)
val get_minimizing_prover :
- Proof.context -> mode -> (thm list -> unit) -> string -> prover
+ Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
val run_minimize :
- params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
- -> Proof.state -> unit
+ params -> (string -> thm list -> unit) -> int
+ -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
end;
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
@@ -211,7 +211,7 @@
|> length of
0 => ""
| n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
- (if learn then do_learn (maps snd min_facts) else ());
+ (if learn then do_learn prover_name (maps snd min_facts) else ());
(SOME min_facts, (preplay, message, message_tail))
end
| {outcome = SOME TimedOut, preplay, ...} =>
@@ -255,11 +255,11 @@
expect = expect}
end
-fun minimize ctxt mode do_learn name
- (params as {debug, verbose, isar_proof, minimize, ...})
- ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
- (result as {outcome, used_facts, run_time, preplay, message,
- message_tail} : prover_result) =
+fun maybe_minimize ctxt mode do_learn name
+ (params as {verbose, isar_proof, minimize, ...})
+ ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
+ (result as {outcome, used_facts, run_time, preplay, message,
+ message_tail} : prover_result) =
if is_some outcome orelse null used_facts then
result
else
@@ -299,7 +299,8 @@
val minimize = minimize |> the_default perhaps_minimize
val (used_facts, (preplay, message, _)) =
if minimize then
- minimize_facts do_learn minimize_name params (not verbose) subgoal
+ minimize_facts do_learn minimize_name params
+ (mode <> Normal orelse not verbose) subgoal
subgoal_count state
(filter_used_facts used_facts
(map (apsnd single o untranslated_fact) facts))
@@ -309,36 +310,25 @@
in
case used_facts of
SOME used_facts =>
- (if debug andalso not (null used_facts) then
- tag_list 1 facts
- |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
- |> filter_used_facts used_facts
- |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
- |> commas
- |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
- " proof (of " ^ string_of_int (length facts) ^ "): ") "."
- |> Output.urgent_message
- else
- ();
- {outcome = NONE, used_facts = used_facts, run_time = run_time,
- preplay = preplay, message = message, message_tail = message_tail})
+ {outcome = NONE, used_facts = used_facts, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail}
| NONE => result
end
fun get_minimizing_prover ctxt mode do_learn name params minimize_command
problem =
get_prover ctxt mode name params minimize_command problem
- |> minimize ctxt mode do_learn name params problem
+ |> maybe_minimize ctxt mode do_learn name params problem
fun run_minimize (params as {provers, ...}) do_learn i refs state =
let
val ctxt = Proof.context_of state
val reserved = reserved_isar_keyword_table ()
val chained_ths = #facts (Proof.goal state)
- val css_table = clasimpset_rule_table_of ctxt
+ val css = clasimpset_rule_table_of ctxt
val facts =
refs |> maps (map (apsnd single)
- o fact_from_ref ctxt reserved chained_ths css_table)
+ o fact_from_ref ctxt reserved chained_ths css)
in
case subgoal_count state of
0 => Output.urgent_message "No subgoal!"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 20 23:38:15 2012 +0200
@@ -15,7 +15,7 @@
type play = ATP_Proof_Reconstruct.play
type minimize_command = ATP_Proof_Reconstruct.minimize_command
- datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
+ datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
type params =
{debug : bool,
@@ -150,7 +150,7 @@
(** The Sledgehammer **)
-datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
+datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
(* Identifier that distinguishes Sledgehammer from other tools that could use
"Async_Manager". *)
@@ -621,6 +621,7 @@
fun suffix_for_mode Auto_Try = "_auto_try"
| suffix_for_mode Try = "_try"
| suffix_for_mode Normal = ""
+ | suffix_for_mode MaSh = "_mash"
| suffix_for_mode Auto_Minimize = "_auto_min"
| suffix_for_mode Minimize = "_min"
@@ -631,9 +632,8 @@
val mono_max_privileged_facts = 10
fun run_atp mode name
- ({exec, required_vars, arguments, proof_delims, known_failures,
- prem_role, best_slices, best_max_mono_iters,
- best_max_new_mono_instances, ...} : atp_config)
+ ({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
+ best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
(params as {debug, verbose, overlord, type_enc, strict, lam_trans,
uncurried_aliases, max_facts, max_mono_iters,
max_new_mono_instances, isar_proof, isar_shrink_factor,
@@ -660,9 +660,17 @@
Path.append (Path.explode dest_dir) problem_file_name
else
error ("No such directory: " ^ quote dest_dir ^ ".")
- val command =
+ val command0 =
case find_first (fn var => getenv var <> "") (fst exec) of
- SOME var => Path.explode (getenv var ^ "/" ^ snd exec)
+ SOME var =>
+ let
+ val pref = getenv var ^ "/"
+ val paths = map (Path.explode o prefix pref) (snd exec)
+ in
+ case find_first File.exists paths of
+ SOME path => path
+ | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
+ end
| NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^
" is not set.")
fun split_time s =
@@ -680,179 +688,162 @@
raw_explode #> Scan.read Symbol.stopper time #> the_default 0
in (output, as_time t |> Time.fromMilliseconds) end
fun run_on prob_file =
- case find_first (forall (fn var => getenv var = ""))
- (fst exec :: required_vars) of
- SOME home_vars =>
- error ("The environment variable " ^ quote (hd home_vars) ^
- " is not set.")
- | NONE =>
- if File.exists command then
+ let
+ (* If slicing is disabled, we expand the last slice to fill the entire
+ time available. *)
+ val actual_slices = get_slices slice (best_slices ctxt)
+ val num_actual_slices = length actual_slices
+ fun monomorphize_facts facts =
+ let
+ val ctxt =
+ ctxt
+ |> repair_monomorph_context max_mono_iters best_max_mono_iters
+ max_new_mono_instances best_max_new_mono_instances
+ (* pseudo-theorem involving the same constants as the subgoal *)
+ val subgoal_th =
+ Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
+ val rths =
+ facts |> chop mono_max_privileged_facts
+ |>> map (pair 1 o snd)
+ ||> map (pair 2 o snd)
+ |> op @
+ |> cons (0, subgoal_th)
+ in
+ Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl
+ |> curry ListPair.zip (map fst facts)
+ |> maps (fn (name, rths) =>
+ map (pair name o zero_var_indexes o snd) rths)
+ end
+ fun run_slice time_left (cache_key, cache_value)
+ (slice, (time_frac, (complete,
+ (key as (best_max_facts, format, best_type_enc,
+ best_lam_trans, best_uncurried_aliases),
+ extra)))) =
let
- (* If slicing is disabled, we expand the last slice to fill the
- entire time available. *)
- val actual_slices = get_slices slice (best_slices ctxt)
- val num_actual_slices = length actual_slices
- fun monomorphize_facts facts =
- let
- val ctxt =
- ctxt
- |> repair_monomorph_context max_mono_iters best_max_mono_iters
- max_new_mono_instances best_max_new_mono_instances
- (* pseudo-theorem involving the same constants as the subgoal *)
- val subgoal_th =
- Logic.list_implies (hyp_ts, concl_t)
- |> Skip_Proof.make_thm thy
- val rths =
- facts |> chop mono_max_privileged_facts
- |>> map (pair 1 o snd)
- ||> map (pair 2 o snd)
- |> op @
- |> cons (0, subgoal_th)
- in
- Monomorph.monomorph atp_schematic_consts_of rths ctxt
- |> fst |> tl
- |> curry ListPair.zip (map fst facts)
- |> maps (fn (name, rths) =>
- map (pair name o zero_var_indexes o snd) rths)
- end
- fun run_slice time_left (cache_key, cache_value)
- (slice, (time_frac, (complete,
- (key as (best_max_facts, format, best_type_enc,
- best_lam_trans, best_uncurried_aliases),
- extra)))) =
- let
- val num_facts =
- length facts |> is_none max_facts ? Integer.min best_max_facts
- val soundness = if strict then Strict else Non_Strict
- val type_enc =
- type_enc |> choose_type_enc soundness best_type_enc format
- val sound = is_type_enc_sound type_enc
- val real_ms = Real.fromInt o Time.toMilliseconds
- val slice_timeout =
- ((real_ms time_left
- |> (if slice < num_actual_slices - 1 then
- curry Real.min (time_frac * real_ms timeout)
- else
- I))
- * 0.001) |> seconds
- val generous_slice_timeout =
- Time.+ (slice_timeout, atp_timeout_slack)
- val _ =
- if debug then
- quote name ^ " slice #" ^ string_of_int (slice + 1) ^
- " with " ^ string_of_int num_facts ^ " fact" ^
- plural_s num_facts ^ " for " ^
- string_from_time slice_timeout ^ "..."
- |> Output.urgent_message
- else
- ()
- val readable_names = not (Config.get ctxt atp_full_names)
- val lam_trans =
- 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
- else
- facts
- |> map untranslated_fact
- |> not sound
- ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
- |> take num_facts
- |> not (is_type_enc_polymorphic type_enc)
- ? monomorphize_facts
- |> map (apsnd prop_of)
- |> prepare_atp_problem ctxt format prem_role type_enc
- atp_mode lam_trans uncurried_aliases
- readable_names true hyp_ts concl_t
- fun sel_weights () = atp_problem_selection_weights atp_problem
- fun ord_info () = atp_problem_term_order_info atp_problem
- val ord = effective_term_order ctxt name
- val full_proof = debug orelse isar_proof
- val args = arguments ctxt full_proof extra slice_timeout
- (ord, ord_info, sel_weights)
- val command =
- File.shell_path command ^ " " ^ args ^ " " ^
- File.shell_path prob_file
- |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
- val _ =
- atp_problem
- |> lines_for_atp_problem format ord ord_info
- |> cons ("% " ^ command ^ "\n")
- |> File.write_list prob_file
- val ((output, run_time), (atp_proof, outcome)) =
- TimeLimit.timeLimit generous_slice_timeout
- Isabelle_System.bash_output command
- |>> (if overlord then
- prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
- else
- I)
- |> fst |> split_time
- |> (fn accum as (output, _) =>
- (accum,
- extract_tstplike_proof_and_outcome verbose complete
- proof_delims known_failures output
- |>> atp_proof_from_tstplike_proof atp_problem
- handle UNRECOGNIZED_ATP_PROOF () =>
- ([], SOME ProofIncomplete)))
- handle TimeLimit.TimeOut =>
- (("", slice_timeout), ([], SOME TimedOut))
- val outcome =
- case outcome of
- NONE =>
- (case used_facts_in_unsound_atp_proof ctxt fact_names
- atp_proof
- |> Option.map (sort string_ord) of
- SOME facts =>
- let
- val failure =
- UnsoundProof (is_type_enc_sound type_enc, facts)
- in
- if debug then
- (warning (string_for_failure failure); NONE)
- else
- SOME failure
- end
- | NONE => NONE)
- | _ => outcome
- in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
- val timer = Timer.startRealTimer ()
- fun maybe_run_slice slice
- (result as (cache, (_, run_time0, _, SOME _))) =
- let
- val time_left = Time.- (timeout, Timer.checkRealTimer timer)
- in
- if Time.<= (time_left, Time.zeroTime) then
- result
- else
- run_slice time_left cache slice
- |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
- (cache, (output, Time.+ (run_time0, run_time),
- atp_proof, outcome)))
- end
- | maybe_run_slice _ result = result
- in
- ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
- ("", Time.zeroTime, [], SOME InternalError))
- |> fold maybe_run_slice actual_slices
- end
- else
- error ("Bad executable: " ^ Path.print command)
+ val num_facts =
+ length facts |> is_none max_facts ? Integer.min best_max_facts
+ val soundness = if strict then Strict else Non_Strict
+ val type_enc =
+ type_enc |> choose_type_enc soundness best_type_enc format
+ val sound = is_type_enc_sound type_enc
+ val real_ms = Real.fromInt o Time.toMilliseconds
+ val slice_timeout =
+ ((real_ms time_left
+ |> (if slice < num_actual_slices - 1 then
+ curry Real.min (time_frac * real_ms timeout)
+ else
+ I))
+ * 0.001) |> seconds
+ val generous_slice_timeout =
+ Time.+ (slice_timeout, atp_timeout_slack)
+ val _ =
+ if debug then
+ quote name ^ " slice #" ^ string_of_int (slice + 1) ^
+ " with " ^ string_of_int num_facts ^ " fact" ^
+ plural_s num_facts ^ " for " ^
+ string_from_time slice_timeout ^ "..."
+ |> Output.urgent_message
+ else
+ ()
+ val readable_names = not (Config.get ctxt atp_full_names)
+ val lam_trans =
+ 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
+ else
+ facts
+ |> map untranslated_fact
+ |> not sound
+ ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
+ |> take num_facts
+ |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
+ |> map (apsnd prop_of)
+ |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
+ lam_trans uncurried_aliases
+ readable_names true hyp_ts concl_t
+ fun sel_weights () = atp_problem_selection_weights atp_problem
+ fun ord_info () = atp_problem_term_order_info atp_problem
+ val ord = effective_term_order ctxt name
+ val full_proof = debug orelse isar_proof
+ val args = arguments ctxt full_proof extra slice_timeout
+ (ord, ord_info, sel_weights)
+ val command =
+ File.shell_path command0 ^ " " ^ args ^ " " ^
+ File.shell_path prob_file
+ |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
+ val _ =
+ atp_problem
+ |> lines_for_atp_problem format ord ord_info
+ |> cons ("% " ^ command ^ "\n")
+ |> File.write_list prob_file
+ val ((output, run_time), (atp_proof, outcome)) =
+ TimeLimit.timeLimit generous_slice_timeout
+ Isabelle_System.bash_output command
+ |>> (if overlord then
+ prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
+ else
+ I)
+ |> fst |> split_time
+ |> (fn accum as (output, _) =>
+ (accum,
+ extract_tstplike_proof_and_outcome verbose complete
+ proof_delims known_failures output
+ |>> atp_proof_from_tstplike_proof atp_problem
+ handle UNRECOGNIZED_ATP_PROOF () =>
+ ([], SOME ProofIncomplete)))
+ handle TimeLimit.TimeOut =>
+ (("", slice_timeout), ([], SOME TimedOut))
+ val outcome =
+ case outcome of
+ NONE =>
+ (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
+ |> Option.map (sort string_ord) of
+ SOME facts =>
+ let
+ val failure =
+ UnsoundProof (is_type_enc_sound type_enc, facts)
+ in
+ if debug then (warning (string_for_failure failure); NONE)
+ else SOME failure
+ end
+ | NONE => NONE)
+ | _ => outcome
+ in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
+ val timer = Timer.startRealTimer ()
+ fun maybe_run_slice slice
+ (result as (cache, (_, run_time0, _, SOME _))) =
+ let
+ val time_left = Time.- (timeout, Timer.checkRealTimer timer)
+ in
+ if Time.<= (time_left, Time.zeroTime) then
+ result
+ else
+ run_slice time_left cache slice
+ |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
+ (cache, (output, Time.+ (run_time0, run_time),
+ atp_proof, outcome)))
+ end
+ | maybe_run_slice _ result = result
+ in
+ ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
+ ("", Time.zeroTime, [], SOME InternalError))
+ |> fold maybe_run_slice actual_slices
+ end
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
fun cleanup prob_file =
if dest_dir = "" then try File.rm prob_file else NONE
fun export prob_file (_, (output, _, _, _)) =
- if dest_dir = "" then
- ()
- else
- File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
+ if dest_dir = "" then ()
+ else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
val ((_, (_, pool, fact_names, _, sym_tab)),
(output, run_time, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 23:38:15 2012 +0200
@@ -33,7 +33,7 @@
open Sledgehammer_Fact
open Sledgehammer_Provers
open Sledgehammer_Minimize
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
val someN = "some"
val noneN = "none"
@@ -64,8 +64,8 @@
fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
timeout, expect, ...})
- mode minimize_command only {state, goal, subgoal, subgoal_count, facts}
- name =
+ mode minimize_command only learn
+ {state, goal, subgoal, subgoal_count, facts} name =
let
val ctxt = Proof.context_of state
val hard_timeout = Time.+ (timeout, timeout)
@@ -84,12 +84,21 @@
? filter_out (curry (op =) Induction o snd o snd o fst
o untranslated_fact)
|> take num_facts}
+ fun print_used_facts used_facts =
+ tag_list 1 facts
+ |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
+ |> filter_used_facts used_facts
+ |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
+ |> commas
+ |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
+ " proof (of " ^ string_of_int (length facts) ^ "): ") "."
+ |> Output.urgent_message
fun really_go () =
problem
- |> get_minimizing_prover ctxt mode
- (mash_learn_proof ctxt params (prop_of goal)
- (map untranslated_fact facts))
- name params minimize_command
+ |> get_minimizing_prover ctxt mode learn name params minimize_command
+ |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} =>
+ print_used_facts used_facts
+ | _ => ())
|> (fn {outcome, preplay, message, message_tail, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
@@ -171,14 +180,14 @@
val state =
state |> Proof.map_context (Config.put SMT_Config.verbose debug)
val ctxt = Proof.context_of state
- val {facts = chained_ths, goal, ...} = Proof.goal state
+ val {facts = chained, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
val reserved = reserved_isar_keyword_table ()
- val css_table = clasimpset_rule_table_of ctxt
- val facts =
- nearly_all_facts ctxt ho_atp fact_override reserved css_table
- chained_ths hyp_ts concl_t
+ val css = clasimpset_rule_table_of ctxt
+ val all_facts =
+ nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
+ concl_t
val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
@@ -196,7 +205,9 @@
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts}
- val launch = launch_prover params mode minimize_command only
+ fun learn prover =
+ mash_learn_proof ctxt params prover (prop_of goal) all_facts
+ val launch = launch_prover params mode minimize_command only learn
in
if mode = Auto_Try orelse mode = Try then
(unknownN, state)
@@ -220,7 +231,7 @@
provers
|> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
in
- facts
+ all_facts
|> (case is_appropriate_prop of
SOME is_app => filter (is_app o prop_of o snd)
| NONE => I)
@@ -228,7 +239,7 @@
hyp_ts concl_t
|> map (apfst (apfst (fn name => name ())))
|> tap (fn facts =>
- if debug then
+ if verbose then
label ^ plural_s (length provers) ^ ": " ^
(if null facts then
"Found no relevant facts."
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 20 23:37:54 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 20 23:38:15 2012 +0200
@@ -6,9 +6,11 @@
signature SLEDGEHAMMER_UTIL =
sig
+ val sledgehammerN : string
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
+ val infinite_timeout : Time.time
val time_mult : real -> Time.time -> Time.time
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
@@ -22,11 +24,15 @@
open ATP_Util
+val sledgehammerN = "sledgehammer"
+
fun plural_s n = if n = 1 then "" else "s"
val serial_commas = Try.serial_commas
val simplify_spaces = strip_spaces false (K true)
+val infinite_timeout = seconds 31536000.0 (* one year *)
+
fun time_mult k t =
Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))