--- a/NEWS Thu Oct 21 14:54:39 2010 +0200
+++ b/NEWS Thu Oct 21 14:55:09 2010 +0200
@@ -276,18 +276,28 @@
meson_disj_FalseD2 ~> Meson.disj_FalseD2
INCOMPATIBILITY.
-* Sledgehammer: Renamed lemmas:
- COMBI_def ~> Meson.COMBI_def
- COMBK_def ~> Meson.COMBK_def
- COMBB_def ~> Meson.COMBB_def
- COMBC_def ~> Meson.COMBC_def
- COMBS_def ~> Meson.COMBS_def
- abs_I ~> Meson.abs_I
- abs_K ~> Meson.abs_K
- abs_B ~> Meson.abs_B
- abs_C ~> Meson.abs_C
- abs_S ~> Meson.abs_S
-INCOMPATIBILITY.
+* Sledgehammer:
+ - Renamed lemmas:
+ COMBI_def ~> Meson.COMBI_def
+ COMBK_def ~> Meson.COMBK_def
+ COMBB_def ~> Meson.COMBB_def
+ COMBC_def ~> Meson.COMBC_def
+ COMBS_def ~> Meson.COMBS_def
+ abs_I ~> Meson.abs_I
+ abs_K ~> Meson.abs_K
+ abs_B ~> Meson.abs_B
+ abs_C ~> Meson.abs_C
+ abs_S ~> Meson.abs_S
+ INCOMPATIBILITY.
+ - Renamed commands:
+ sledgehammer atp_info ~> sledgehammer running_provers
+ sledgehammer atp_kill ~> sledgehammer kill_provers
+ sledgehammer available_atps ~> sledgehammer available_provers
+ INCOMPATIBILITY.
+ - Renamed options:
+ sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
+ sledgehammer [atp = ...] ~> sledgehammer [provers = ...]
+ INCOMPATIBILITY.
*** FOL ***
--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Oct 21 14:54:39 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Oct 21 14:55:09 2010 +0200
@@ -79,9 +79,9 @@
Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS
-\cite{weidenbach-et-al-2009}, and Vampire \cite{riazanov-voronkov-2002}, which
-can be run locally or remotely via the SystemOnTPTP web service
-\cite{sutcliffe-2000}.
+\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002},
+SInE-E \cite{sine}, and SNARK \cite{snark}. The ATPs are run either locally or
+remotely via the SystemOnTPTP web service \cite{sutcliffe-2000}.
The problem passed to ATPs consists of your current goal together with a
heuristic selection of hundreds of facts (theorems) from the current theory
@@ -124,9 +124,9 @@
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
relies on third-party automatic theorem provers (ATPs). Currently, E, SPASS, and
-Vampire are supported. All of these are available remotely via SystemOnTPTP
-\cite{sutcliffe-2000}, but if you want better performance you will need to
-install at least E and SPASS locally.
+Vampire can be run locally; in addition, E, Vampire, SInE-E, and SNARK
+are available remotely via SystemOnTPTP \cite{sutcliffe-2000}. If you want
+better performance, you should install at least E and SPASS locally.
There are three main ways to install ATPs on your machine:
@@ -199,24 +199,24 @@
\prew
\slshape
-Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
+Sledgehammer: Prover ``\textit{e}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
%
-Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
+Sledgehammer: Prover ``\textit{spass}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
%
-Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
+Sledgehammer: Prover ``\textit{remote\_vampire}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
\phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_vampire}] \\
\phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
\phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
\postw
@@ -291,14 +291,16 @@
to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
limit on the number of messages to display (5 by default).
-\item[$\bullet$] \textbf{\textit{available\_atps}:} Prints the list of installed ATPs.
+\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of installed provers.
See \S\ref{installation} and \S\ref{mode-of-operation} for more information on
-how to install ATPs.
+how to install automatic provers.
-\item[$\bullet$] \textbf{\textit{running\_atps}:} Prints information about currently
-running ATPs, including elapsed runtime and remaining time until timeout.
+\item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about
+currently running automatic provers, including elapsed runtime and remaining
+time until timeout.
-\item[$\bullet$] \textbf{\textit{kill\_atps}:} Terminates all running ATPs.
+\item[$\bullet$] \textbf{\textit{kill\_provers}:} Terminates all running
+automatic provers.
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
@@ -334,10 +336,10 @@
You can instruct Sledgehammer to run automatically on newly entered theorems by
enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
-General. For automatic runs, only the first ATP set using \textit{atps}
+General. For automatic runs, only the first prover set using \textit{provers}
(\S\ref{mode-of-operation}) is considered, \textit{verbose}
(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled,
-fewer facts are passed to the ATP, and \textit{timeout} (\S\ref{timeouts}) is
+fewer facts are passed to the prover, and \textit{timeout} (\S\ref{timeouts}) is
superseded by the ``Auto Tools Time Limit'' in Proof General's ``Isabelle''
menu. Sledgehammer's output is also more concise.
@@ -382,9 +384,9 @@
\label{mode-of-operation}
\begin{enum}
-\opnodefault{atps}{string}
-Specifies the ATPs (automated theorem provers) to use as a space-separated list
-(e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported:
+\opnodefault{provers}{string}
+Specifies the automatic provers to use as a space-separated list (e.g.,
+``\textit{e}~\textit{spass}''). The following provers are supported:
\begin{enum}
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
@@ -423,22 +425,28 @@
By default, Sledgehammer will run E, SPASS, Vampire, and SInE-E in parallel.
For at most two of E, SPASS, and Vampire, it will use any locally installed
version if available. For historical reasons, the default value of this option
-can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
-menu in Proof General.
+can be overridden using the option ``Sledgehammer: Provers'' from the
+``Isabelle'' menu in Proof General.
-It is a good idea to run several ATPs in parallel, although it could slow down
-your machine. Running E, SPASS, and Vampire together for 5 seconds yields about
-the same success rate as running the most effective of these (Vampire) for 120
-seconds \cite{boehme-nipkow-2010}.
+It is a good idea to run several provers in parallel, although it could slow
+down your machine. Running E, SPASS, and Vampire together for 5 seconds yields
+about the same success rate as running the most effective of these (Vampire) for
+120 seconds \cite{boehme-nipkow-2010}.
+
+\opnodefault{prover}{string}
+Alias for \textit{provers}.
+
+\opnodefault{atps}{string}
+Legacy alias for \textit{provers}.
\opnodefault{atp}{string}
-Alias for \textit{atps}.
+Legacy alias for \textit{provers}.
\opdefault{timeout}{time}{$\mathbf{30}$ s}
-Specifies the maximum amount of time that the ATPs should spend searching for a
-proof. For historical reasons, the default value of this option can be
-overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
-menu in Proof General.
+Specifies the maximum amount of time that the automatic provers should spend
+searching for a proof. For historical reasons, the default value of this option
+can be overridden using the option ``Sledgehammer: Time Limit'' from the
+``Isabelle'' menu in Proof General.
\opfalse{blocking}{non\_blocking}
Specifies whether the \textbf{sledgehammer} command should operate
@@ -471,8 +479,8 @@
Specifies whether full-type information is exported. Enabling this option can
prevent the discovery of type-incorrect proofs, but it also tends to slow down
the ATPs significantly. For historical reasons, the default value of this option
-can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
-menu in Proof General.
+can be overridden using the option ``Sledgehammer: Full Types'' from the
+``Isabelle'' menu in Proof General.
\end{enum}
\subsection{Relevance Filter}
@@ -490,18 +498,8 @@
\opdefault{max\_relevant}{int\_or\_smart}{\textit{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 ATP. A typical value would be 300.
-
-%\opsmartx{theory\_relevant}{theory\_irrelevant}
-%Specifies whether the theory from which a fact comes should be taken into
-%consideration by the relevance filter. If the option is set to \textit{smart},
-%it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
-%empirical results suggest that these are the best settings.
-
-%\opfalse{defs\_relevant}{defs\_irrelevant}
-%Specifies whether the definition of constants occurring in the formula to prove
-%should be considered particularly relevant. Enabling this option tends to lead
-%to larger problems and typically slows down the ATPs.
+empirically found to be appropriate for the prover. A typical value would be
+300.
\end{enum}
\subsection{Output Format}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 21 14:54:39 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 21 14:55:09 2010 +0200
@@ -316,13 +316,13 @@
fun get_atp thy args =
let
fun default_atp_name () =
- hd (#atps (Sledgehammer_Isar.default_params thy []))
+ hd (#provers (Sledgehammer_Isar.default_params thy []))
handle Empty => error "No ATP available."
- fun get_prover name = (name, Sledgehammer.get_prover_fun thy name)
+ fun get_atp name = (name, Sledgehammer.get_atp_fun thy name)
in
(case AList.lookup (op =) args proverK of
- SOME name => get_prover name
- | NONE => get_prover (default_atp_name ()))
+ SOME name => get_atp name
+ | NONE => get_atp (default_atp_name ()))
end
type locality = Sledgehammer_Filter.locality
@@ -349,7 +349,7 @@
Sledgehammer_Isar.default_params thy
[("timeout", Int.toString timeout ^ " s")]
val relevance_override = {add = [], del = [], only = false}
- val {default_max_relevant, ...} = ATP_Systems.get_prover thy prover_name
+ val {default_max_relevant, ...} = ATP_Systems.get_atp thy prover_name
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val axioms =
Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
@@ -364,7 +364,7 @@
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
val ({outcome, message, used_thm_names,
- atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result,
+ atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.atp_result,
time_isa) = time_limit (Mirabelle.cpu_time
(prover params (K ""))) problem
in
@@ -443,7 +443,7 @@
|> Option.map (fst o read_int o explode)
|> the_default 5
val params = Sledgehammer_Isar.default_params thy
- [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")]
+ [("provers", prover_name), ("timeout", Int.toString timeout ^ " s")]
val minimize =
Sledgehammer_Minimize.minimize_theorems params 1 (subgoal_count st)
val _ = log separator
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Oct 21 14:54:39 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Oct 21 14:55:09 2010 +0200
@@ -9,7 +9,7 @@
sig
type failure = ATP_Proof.failure
- type prover_config =
+ type atp_config =
{exec: string * string,
required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
@@ -20,11 +20,17 @@
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
- val add_prover: string * prover_config -> theory -> theory
- val get_prover: theory -> string -> prover_config
- val available_atps: theory -> unit
+ val eN : string
+ val spassN : string
+ val vampireN : string
+ val sine_eN : string
+ val snarkN : string
+ val remote_atp_prefix : string
+ val add_atp : string * atp_config -> theory -> theory
+ val get_atp : theory -> string -> atp_config
+ val available_atps : theory -> string list
+ val is_atp_installed : theory -> string -> bool
val refresh_systems_on_tptp : unit -> unit
- val default_atps_param_value : unit -> string
val setup : theory -> theory
end;
@@ -33,9 +39,9 @@
open ATP_Proof
-(* prover configuration *)
+(* ATP configuration *)
-type prover_config =
+type atp_config =
{exec: string * string,
required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
@@ -51,33 +57,28 @@
(NoPerl, "env: perl"),
(NoLibwwwPerl, "Can't locate HTTP")]
-(* named provers *)
+(* named ATPs *)
+
+val eN = "e"
+val spassN = "spass"
+val vampireN = "vampire"
+val sine_eN = "sine_e"
+val snarkN = "snark"
+val remote_atp_prefix = "remote_"
structure Data = Theory_Data
(
- type T = (prover_config * stamp) Symtab.table
+ type T = (atp_config * stamp) Symtab.table
val empty = Symtab.empty
val extend = I
fun merge data : T = Symtab.merge (eq_snd op =) data
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
)
-fun add_prover (name, config) thy =
- Data.map (Symtab.update_new (name, (config, stamp ()))) thy
- handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
-
-fun get_prover thy name =
- the (Symtab.lookup (Data.get thy) name) |> fst
- handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
-
-fun available_atps thy =
- priority ("Available ATPs: " ^
- commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
-
fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
-(* E prover *)
+(* E *)
(* Give older versions of E an extra second, because the "eproof" script wrongly
subtracted an entire second to account for the overhead of the script
@@ -92,7 +93,7 @@
val tstp_proof_delims =
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
-val e_config : prover_config =
+val e_config : atp_config =
{exec = ("E_HOME", "eproof"),
required_execs = [],
arguments = fn _ => fn timeout =>
@@ -113,14 +114,14 @@
explicit_forall = false,
use_conjecture_for_hypotheses = true}
-val e = ("e", e_config)
+val e = (eN, e_config)
(* SPASS *)
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
-val spass_config : prover_config =
+val spass_config : atp_config =
{exec = ("ISABELLE_ATP", "scripts/spass"),
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
arguments = fn complete => fn timeout =>
@@ -142,12 +143,12 @@
explicit_forall = true,
use_conjecture_for_hypotheses = true}
-val spass = ("spass", spass_config)
+val spass = (spassN, spass_config)
(* Vampire *)
-val vampire_config : prover_config =
+val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
arguments = fn complete => fn timeout =>
@@ -172,10 +173,10 @@
explicit_forall = false,
use_conjecture_for_hypotheses = true}
-val vampire = ("vampire", vampire_config)
+val vampire = (vampireN, vampire_config)
-(* Remote prover invocation via SystemOnTPTP *)
+(* Remote ATP invocation via SystemOnTPTP *)
val systems = Synchronized.var "atp_systems" ([] : string list)
@@ -187,9 +188,6 @@
SOME failure => string_for_failure failure
| NONE => perhaps (try (unsuffix "\n")) output ^ ".")
-fun refresh_systems_on_tptp () =
- Synchronized.change systems (fn _ => get_systems ())
-
fun find_system name [] systems = find_first (String.isPrefix name) systems
| find_system name (version :: versions) systems =
case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
@@ -208,7 +206,7 @@
fun remote_config system_name system_versions proof_delims known_failures
default_max_relevant use_conjecture_for_hypotheses
- : prover_config =
+ : atp_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn timeout =>
@@ -225,48 +223,49 @@
fun remotify_config system_name system_versions
({proof_delims, known_failures, default_max_relevant,
- use_conjecture_for_hypotheses, ...} : prover_config) : prover_config =
+ use_conjecture_for_hypotheses, ...} : atp_config) : atp_config =
remote_config system_name system_versions proof_delims known_failures
default_max_relevant use_conjecture_for_hypotheses
-val remotify_name = prefix "remote_"
-fun remote_prover name system_name system_versions proof_delims known_failures
- default_max_relevant use_conjecture_for_hypotheses =
- (remotify_name name,
+fun remote_atp name system_name system_versions proof_delims known_failures
+ default_max_relevant use_conjecture_for_hypotheses =
+ (remote_atp_prefix ^ name,
remote_config system_name system_versions proof_delims known_failures
default_max_relevant use_conjecture_for_hypotheses)
-fun remotify_prover (name, config) system_name system_versions =
- (remotify_name name, remotify_config system_name system_versions config)
+fun remotify_atp (name, config) system_name system_versions =
+ (remote_atp_prefix ^ name, remotify_config system_name system_versions config)
-val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
-val remote_vampire = remotify_prover vampire "Vampire" ["0.6", "9.0", "1.0"]
+val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
+val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
val remote_sine_e =
- remote_prover "sine_e" "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
+ remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
800 (* FUDGE *) true
val remote_snark =
- remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
- 250 (* FUDGE *) true
+ remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] []
+ 250 (* FUDGE *) true
(* Setup *)
-fun is_installed ({exec, required_execs, ...} : prover_config) =
- forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
-fun maybe_remote (name, config) =
- name |> not (is_installed config) ? remotify_name
+fun add_atp (name, config) thy =
+ Data.map (Symtab.update_new (name, (config, stamp ()))) thy
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
+
+fun get_atp thy name =
+ the (Symtab.lookup (Data.get thy) name) |> fst
+ handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
+
+val available_atps = Symtab.keys o Data.get
-(* The first prover of the list is used by Auto Sledgehammer. Because of the low
- timeout, it makes sense to put SPASS first. *)
-fun default_atps_param_value () =
- space_implode " " ((if is_installed (snd spass) then [fst spass] else []) @
- [maybe_remote e] @
- [if forall (is_installed o snd) [e, spass] then
- remotify_name (fst vampire)
- else
- maybe_remote vampire,
- fst remote_sine_e])
+fun is_atp_installed thy name =
+ let val {exec, required_execs, ...} = get_atp thy name in
+ forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
+ end
-val provers = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
- remote_snark]
-val setup = fold add_prover provers
+fun refresh_systems_on_tptp () =
+ Synchronized.change systems (fn _ => get_systems ())
+
+val atps = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
+ remote_snark]
+val setup = fold add_atp atps
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Oct 21 14:54:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Oct 21 14:55:09 2010 +0200
@@ -19,7 +19,7 @@
debug: bool,
verbose: bool,
overlord: bool,
- atps: string list,
+ provers: string list,
full_types: bool,
explicit_apply: bool,
relevance_thresholds: real * real,
@@ -29,14 +29,14 @@
timeout: Time.time,
expect: string}
- type problem =
+ type atp_problem =
{state: Proof.state,
goal: thm,
subgoal: int,
axioms: (term * ((string * locality) * fol_formula) option) list,
only: bool}
- type prover_result =
+ type atp_result =
{outcome: failure option,
message: string,
pool: string Symtab.table,
@@ -47,15 +47,16 @@
axiom_names: (string * locality) list vector,
conjecture_shape: int list list}
- type prover = params -> minimize_command -> problem -> prover_result
+ type atp = params -> minimize_command -> atp_problem -> atp_result
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
- val kill_atps: unit -> unit
- val running_atps: unit -> unit
- val messages: int option -> unit
- val get_prover_fun : theory -> string -> prover
+ val available_provers : theory -> unit
+ val kill_provers : unit -> unit
+ val running_provers : unit -> unit
+ val messages : int option -> unit
+ val get_atp_fun : theory -> string -> atp
val run_sledgehammer :
params -> bool -> int -> relevance_override -> (string -> minimize_command)
-> Proof.state -> bool * Proof.state
@@ -81,18 +82,22 @@
"Async_Manager". *)
val das_Tool = "Sledgehammer"
-fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
-fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
-val messages = Async_Manager.thread_messages das_Tool "ATP"
+fun available_provers thy =
+ priority ("Available provers: " ^
+ commas (sort_strings (available_atps thy)) ^ ".")
-(** problems, results, provers, etc. **)
+fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
+fun running_provers () = Async_Manager.running_threads das_Tool "provers"
+val messages = Async_Manager.thread_messages das_Tool "prover"
+
+(** problems, results, ATPs, etc. **)
type params =
{blocking: bool,
debug: bool,
verbose: bool,
overlord: bool,
- atps: string list,
+ provers: string list,
full_types: bool,
explicit_apply: bool,
relevance_thresholds: real * real,
@@ -102,14 +107,14 @@
timeout: Time.time,
expect: string}
-type problem =
+type atp_problem =
{state: Proof.state,
goal: thm,
subgoal: int,
axioms: (term * ((string * locality) * fol_formula) option) list,
only: bool}
-type prover_result =
+type atp_result =
{outcome: failure option,
message: string,
pool: string Symtab.table,
@@ -120,7 +125,7 @@
axiom_names: (string * locality) list vector,
conjecture_shape: int list list}
-type prover = params -> minimize_command -> problem -> prover_result
+type atp = params -> minimize_command -> atp_problem -> atp_result
(* configuration attributes *)
@@ -140,41 +145,41 @@
|> Exn.release
|> tap (after path)
-(* generic TPTP-based provers *)
+(* generic TPTP-based ATPs *)
(* Important messages are important but not so important that users want to see
them each time. *)
val important_message_keep_factor = 0.1
-fun prover_fun auto atp_name
+fun atp_fun auto atp_name
{exec, required_execs, arguments, has_incomplete_mode, proof_delims,
known_failures, default_max_relevant, explicit_forall,
use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
- minimize_command ({state, goal, subgoal, axioms, only} : problem) =
+ minimize_command ({state, goal, subgoal, axioms, only} : atp_problem) =
let
val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
val axioms = axioms |> not only
? take (the_default default_max_relevant max_relevant)
- val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
- else Config.get ctxt dest_dir
- val the_problem_prefix = Config.get ctxt problem_prefix
- val problem_file_name =
+ val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
+ else Config.get ctxt dest_dir
+ val problem_prefix = Config.get ctxt problem_prefix
+ val atp_problem_file_name =
Path.basic ((if overlord then "prob_" ^ atp_name
- else the_problem_prefix ^ serial_string ())
+ else problem_prefix ^ serial_string ())
^ "_" ^ string_of_int subgoal)
- val problem_path_name =
- if the_dest_dir = "" then
- File.tmp_path problem_file_name
- else if File.exists (Path.explode the_dest_dir) then
- Path.append (Path.explode the_dest_dir) problem_file_name
+ val atp_problem_path_name =
+ if dest_dir = "" then
+ File.tmp_path atp_problem_file_name
+ else if File.exists (Path.explode dest_dir) then
+ Path.append (Path.explode dest_dir) atp_problem_file_name
else
- error ("No such directory: " ^ quote the_dest_dir ^ ".")
+ error ("No such directory: " ^ quote dest_dir ^ ".")
val measure_run_time = verbose orelse Config.get ctxt measure_run_time
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
- (* write out problem file and call prover *)
+ (* write out problem file and call ATP *)
fun command_line complete timeout probfile =
let
val core = File.shell_path command ^ " " ^ arguments complete timeout ^
@@ -216,11 +221,11 @@
proof_delims known_failures output
in (output, msecs, tstplike_proof, outcome) end
val readable_names = debug andalso overlord
- val (problem, pool, conjecture_offset, axiom_names) =
- prepare_problem ctxt readable_names explicit_forall full_types
- explicit_apply hyp_ts concl_t axioms
+ val (atp_problem, pool, conjecture_offset, axiom_names) =
+ prepare_atp_problem ctxt readable_names explicit_forall full_types
+ explicit_apply hyp_ts concl_t axioms
val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
- problem
+ atp_problem
val _ = File.write_list probfile ss
val conjecture_shape =
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
@@ -246,15 +251,15 @@
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
fun cleanup probfile =
- if the_dest_dir = "" then try File.rm probfile else NONE
+ if dest_dir = "" then try File.rm probfile else NONE
fun export probfile (_, (output, _, _, _)) =
- if the_dest_dir = "" then
+ if dest_dir = "" then
()
else
File.write (Path.explode (Path.implode probfile ^ "_proof")) output
val ((pool, conjecture_shape, axiom_names),
(output, msecs, tstplike_proof, outcome)) =
- with_path cleanup export run_on problem_path_name
+ with_path cleanup export run_on atp_problem_path_name
val (conjecture_shape, axiom_names) =
repair_conjecture_shape_and_axiom_names output conjecture_shape
axiom_names
@@ -291,12 +296,13 @@
axiom_names = axiom_names, conjecture_shape = conjecture_shape}
end
-fun get_prover_fun thy name = prover_fun false name (get_prover thy name)
+fun get_atp_fun thy name = atp_fun false name (get_atp thy name)
-fun run_prover (params as {blocking, debug, verbose, max_relevant, timeout,
- expect, ...})
- auto i n minimize_command (problem as {state, goal, axioms, ...})
- (prover as {default_max_relevant, ...}, atp_name) =
+fun run_atp (params as {blocking, debug, verbose, max_relevant, timeout, expect,
+ ...})
+ auto i n minimize_command
+ (atp_problem as {state, goal, axioms, ...})
+ (atp as {default_max_relevant, ...}, atp_name) =
let
val ctxt = Proof.context_of state
val birth_time = Time.now ()
@@ -317,8 +323,8 @@
fun go () =
let
fun really_go () =
- prover_fun auto atp_name prover params (minimize_command atp_name)
- problem
+ atp_fun auto atp_name atp params (minimize_command atp_name)
+ atp_problem
|> (fn {outcome, message, ...} =>
(if is_some outcome then "none" else "some", message))
val (outcome_code, message) =
@@ -357,21 +363,21 @@
val auto_max_relevant_divisor = 2
-fun run_sledgehammer (params as {blocking, atps, full_types,
+fun run_sledgehammer (params as {blocking, provers, full_types,
relevance_thresholds, max_relevant, ...})
auto i (relevance_override as {only, ...}) minimize_command
state =
- if null atps then
- error "No ATP is set."
+ if null provers then
+ error "No prover is set."
else case subgoal_count state of
0 => (priority "No subgoal!"; (false, state))
| n =>
let
val _ = Proof.assert_backward state
val thy = Proof.theory_of state
- val _ = () |> not blocking ? kill_atps
+ val _ = () |> not blocking ? kill_provers
val _ = if auto then () else priority "Sledgehammering..."
- val provers = map (`(get_prover thy)) atps
+ val atps = map (`(get_atp thy)) provers
fun go () =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
@@ -380,23 +386,23 @@
case max_relevant of
SOME n => n
| NONE =>
- 0 |> fold (Integer.max o #default_max_relevant o fst) provers
+ 0 |> fold (Integer.max o #default_max_relevant o fst) atps
|> auto ? (fn n => n div auto_max_relevant_divisor)
val axioms =
relevant_facts ctxt full_types relevance_thresholds
max_max_relevant relevance_override chained_ths
hyp_ts concl_t
- val problem =
+ val atp_problem =
{state = state, goal = goal, subgoal = i,
axioms = map (prepare_axiom ctxt) axioms, only = only}
- val run_prover = run_prover params auto i n minimize_command problem
+ val run_atp = run_atp params auto i n minimize_command atp_problem
in
if auto then
- fold (fn prover => fn (true, state) => (true, state)
- | (false, _) => run_prover prover)
- provers (false, state)
+ fold (fn atp => fn (true, state) => (true, state)
+ | (false, _) => run_atp atp)
+ atps (false, state)
else
- (if blocking then Par_List.map else map) run_prover provers
+ (if blocking then Par_List.map else map) run_atp atps
|> exists fst |> rpair state
end
in if blocking then go () else Future.fork (tap go) |> K (false, state) end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 21 14:54:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 21 14:55:09 2010 +0200
@@ -9,7 +9,7 @@
type params = Sledgehammer.params
val auto : bool Unsynchronized.ref
- val atps : string Unsynchronized.ref
+ val provers : string Unsynchronized.ref
val timeout : int Unsynchronized.ref
val full_types : bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
@@ -49,14 +49,14 @@
(*** parameters ***)
-val atps = Unsynchronized.ref ""
+val provers = Unsynchronized.ref ""
val timeout = Unsynchronized.ref 30
val full_types = Unsynchronized.ref false
val _ =
ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.string_pref atps
- "Sledgehammer: ATPs"
+ (Preferences.string_pref provers
+ "Sledgehammer: Provers"
"Default automatic provers (separated by whitespace)")
val _ =
@@ -84,7 +84,9 @@
("isar_shrink_factor", "1")]
val alias_params =
- [("atp", "atps")]
+ [("prover", "provers"),
+ ("atps", "provers"), (* FIXME: legacy *)
+ ("atp", "provers")] (* FIXME: legacy *)
val negated_alias_params =
[("non_blocking", "blocking"),
("no_debug", "debug"),
@@ -98,7 +100,7 @@
["debug", "verbose", "overlord", "full_types", "isar_proof",
"isar_shrink_factor", "timeout"]
-val property_dependent_params = ["atps", "full_types", "timeout"]
+val property_dependent_params = ["provers", "full_types", "timeout"]
fun is_known_raw_param s =
AList.defined (op =) default_default_params s orelse
@@ -128,11 +130,28 @@
val extend = I
fun merge p : T = AList.merge (op =) (K true) p)
+fun maybe_remote_atp thy name =
+ name |> not (is_atp_installed thy name) ? prefix remote_atp_prefix
+
+(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
+ timeout, it makes sense to put SPASS first. *)
+fun default_provers_param_value thy =
+ (filter (is_atp_installed thy) [spassN] @
+ [maybe_remote_atp thy eN,
+ if forall (is_atp_installed thy) [spassN, eN] then
+ remote_atp_prefix ^ vampireN
+ else
+ maybe_remote_atp thy vampireN,
+ remote_atp_prefix ^ sine_eN])
+ |> space_implode " "
+
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
fun default_raw_params thy =
Data.get thy
|> fold (AList.default (op =))
- [("atps", [case !atps of "" => default_atps_param_value () | s => s]),
+ [("provers", [case !provers of
+ "" => default_provers_param_value thy
+ | s => s]),
("full_types", [if !full_types then "true" else "false"]),
("timeout", let val timeout = !timeout in
[if timeout <= 0 then "none"
@@ -180,7 +199,8 @@
val debug = not auto andalso lookup_bool "debug"
val verbose = debug orelse (not auto andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
- val atps = lookup_string "atps" |> space_explode " " |> auto ? single o hd
+ val provers = lookup_string "provers" |> space_explode " "
+ |> auto ? single o hd
val full_types = lookup_bool "full_types"
val explicit_apply = lookup_bool "explicit_apply"
val relevance_thresholds =
@@ -193,7 +213,8 @@
val expect = lookup_string "expect"
in
{blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
- atps = atps, full_types = full_types, explicit_apply = explicit_apply,
+ provers = provers, full_types = full_types,
+ explicit_apply = explicit_apply,
relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
timeout = timeout, expect = expect}
@@ -210,9 +231,9 @@
val runN = "run"
val minimizeN = "minimize"
val messagesN = "messages"
-val available_atpsN = "available_atps"
-val running_atpsN = "running_atps"
-val kill_atpsN = "kill_atps"
+val available_proversN = "available_provers"
+val running_proversN = "running_provers"
+val kill_proversN = "kill_provers"
val refresh_tptpN = "refresh_tptp"
val is_raw_param_relevant_for_minimize =
@@ -220,8 +241,8 @@
fun string_for_raw_param (key, values) =
key ^ (case space_implode " " values of "" => "" | value => " = " ^ value)
-fun minimize_command override_params i atp_name fact_names =
- sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
+fun minimize_command override_params i prover_name fact_names =
+ sledgehammerN ^ " " ^ minimizeN ^ " [prover = " ^ prover_name ^
(override_params |> filter is_raw_param_relevant_for_minimize
|> implode o map (prefix ", " o string_for_raw_param)) ^
"] (" ^ space_implode " " fact_names ^ ")" ^
@@ -244,12 +265,12 @@
(#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
- else if subcommand = available_atpsN then
- available_atps thy
- else if subcommand = running_atpsN then
- running_atps ()
- else if subcommand = kill_atpsN then
- kill_atps ()
+ else if subcommand = available_proversN then
+ available_provers thy
+ else if subcommand = running_proversN then
+ running_provers ()
+ else if subcommand = kill_proversN then
+ kill_provers ()
else if subcommand = refresh_tptpN then
refresh_systems_on_tptp ()
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 21 14:54:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 21 14:55:09 2010 +0200
@@ -44,25 +44,24 @@
"")
end
-fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof,
+fun test_theorems ({debug, verbose, overlord, provers, full_types, isar_proof,
isar_shrink_factor, ...} : params)
- (prover : prover) explicit_apply timeout subgoal state
- axioms =
+ (atp : atp) explicit_apply timeout subgoal state axioms =
let
val _ =
priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
val params =
{blocking = true, debug = debug, verbose = verbose, overlord = overlord,
- atps = atps, full_types = full_types, explicit_apply = explicit_apply,
- relevance_thresholds = (1.01, 1.01),
+ provers = provers, full_types = full_types,
+ explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01),
max_relevant = SOME 65536 (* a large number *), isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
val {context = ctxt, goal, ...} = Proof.goal state
- val problem =
+ val atp_problem =
{state = state, goal = goal, subgoal = subgoal,
axioms = map (prepare_axiom ctxt) axioms, only = true}
- val result as {outcome, used_thm_names, ...} = prover params (K "") problem
+ val result as {outcome, used_thm_names, ...} = atp params (K "") atp_problem
in
priority (case outcome of
NONE =>
@@ -81,7 +80,7 @@
fun sublinear_minimize _ [] p = p
| sublinear_minimize test (x :: xs) (seen, result) =
case test (xs @ seen) of
- result as {outcome = NONE, used_thm_names, ...} : prover_result =>
+ result as {outcome = NONE, used_thm_names, ...} : atp_result =>
sublinear_minimize test (filter_used_facts used_thm_names xs)
(filter_used_facts used_thm_names seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)
@@ -91,22 +90,22 @@
timeout. *)
val fudge_msecs = 1000
-fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
- | minimize_theorems (params as {debug, atps = atp :: _, full_types,
+fun minimize_theorems {provers = [], ...} _ _ _ _ = error "No prover is set."
+ | minimize_theorems (params as {debug, provers = prover :: _, full_types,
isar_proof, isar_shrink_factor, timeout, ...})
i (_ : int) state axioms =
let
val thy = Proof.theory_of state
- val prover = get_prover_fun thy atp
+ val atp = get_atp_fun thy prover
val msecs = Time.toMilliseconds timeout
- val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".")
+ val _ = priority ("Sledgehammer minimize: prover " ^ quote prover ^ ".")
val {context = ctxt, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val explicit_apply =
not (forall (Meson.is_fol_term thy)
(concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
fun do_test timeout =
- test_theorems params prover explicit_apply timeout i state
+ test_theorems params atp explicit_apply timeout i state
val timer = Timer.startRealTimer ()
in
(case do_test timeout axioms of
@@ -159,7 +158,8 @@
case subgoal_count state of
0 => priority "No subgoal!"
| n =>
- (kill_atps (); priority (#2 (minimize_theorems params i n state axioms)))
+ (kill_provers ();
+ priority (#2 (minimize_theorems params i n state axioms)))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Oct 21 14:54:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Oct 21 14:55:09 2010 +0200
@@ -16,7 +16,7 @@
val prepare_axiom :
Proof.context -> (string * 'a) * thm
-> term * ((string * 'a) * fol_formula) option
- val prepare_problem :
+ val prepare_atp_problem :
Proof.context -> bool -> bool -> bool -> bool -> term list -> term
-> (term * ((string * 'a) * fol_formula) option) list
-> string problem * string Symtab.table * int * (string * 'a) list vector
@@ -494,8 +494,8 @@
repair_problem_with_const_table thy explicit_forall full_types
(const_table_for_problem explicit_apply problem) problem
-fun prepare_problem ctxt readable_names explicit_forall full_types
- explicit_apply hyp_ts concl_t axioms =
+fun prepare_atp_problem ctxt readable_names explicit_forall full_types
+ explicit_apply hyp_ts concl_t axioms =
let
val thy = ProofContext.theory_of ctxt
val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,