# HG changeset patch # User blanchet # Date 1287665709 -7200 # Node ID 6ad9081665db3dc59f427761172ad625412c2240 # Parent b4f62d0660e0d56f4473b3307341b61dc1e3770e use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..." diff -r b4f62d0660e0 -r 6ad9081665db NEWS --- 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 *** diff -r b4f62d0660e0 -r 6ad9081665db doc-src/Sledgehammer/sledgehammer.tex --- 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} diff -r b4f62d0660e0 -r 6ad9081665db src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r b4f62d0660e0 -r 6ad9081665db src/HOL/Tools/ATP/atp_systems.ML --- 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; diff -r b4f62d0660e0 -r 6ad9081665db src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 diff -r b4f62d0660e0 -r 6ad9081665db src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r b4f62d0660e0 -r 6ad9081665db src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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; diff -r b4f62d0660e0 -r 6ad9081665db src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- 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,