--- a/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
@@ -653,7 +653,8 @@
Specifies the automatic provers to use as a space-separated list (e.g.,
``\textit{cvc4}~\textit{e}~\textit{spass}~\textit{vampire\/}'').
Provers can be run locally or remotely; see \S\ref{installation} for
-installation instructions.
+installation instructions. By default, \textit{provers} is set to the list of
+all installed local provers.
The following local provers are supported:
--- a/src/HOL/Tools/SMT/smt_config.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon Jan 31 16:09:23 2022 +0100
@@ -14,6 +14,7 @@
options: Proof.context -> string list }
val add_solver: solver_info -> Context.generic -> Context.generic
val set_solver_options: string * string -> Context.generic -> Context.generic
+ val all_solvers_of: Proof.context -> string list
val is_available: Proof.context -> string -> bool
val available_solvers_of: Proof.context -> string list
val select_solver: string -> Context.generic -> Context.generic
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
@@ -420,10 +420,8 @@
val launch = launch_prover_and_preplay params mode writeln_result learn
val schedule =
- if mode = Auto_Try then
- provers
- else
- schedule_of_provers provers slices
+ if mode = Auto_Try then provers
+ else schedule_of_provers provers slices
val prover_slices = prover_slices_of_schedule ctxt params schedule
in
if mode = Auto_Try then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 31 16:09:23 2022 +0100
@@ -50,10 +50,12 @@
string * (unit -> atp_config)
val add_atp : string * (unit -> atp_config) -> theory -> theory
val get_atp : theory -> string -> (unit -> atp_config)
- val supported_atps : theory -> string list
val is_atp_installed : theory -> string -> bool
val refresh_systems_on_tptp : unit -> unit
val effective_term_order : Proof.context -> string -> term_order
+ val local_atps : string list
+ val remote_atps : string list
+ val atps : string list
end;
structure Sledgehammer_ATP_Systems : SLEDGEHAMMER_ATP_SYSTEMS =
@@ -681,8 +683,6 @@
fst (the (Symtab.lookup (Data.get thy) name))
handle Option.Option => error ("Unknown ATP: " ^ name)
-val supported_atps = Symtab.keys o Data.get
-
fun is_atp_installed thy name =
let val {exec, ...} = get_atp thy name () in
exists (fn var => getenv var <> "") (fst exec)
@@ -703,11 +703,17 @@
end
end
-val atps =
- [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
- remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
+val local_atps =
+ [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition]
+val remote_atps =
+ [remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced]
+val atps = local_atps @ remote_atps
val _ = Theory.setup (fold add_atp atps)
+val local_atps = map fst local_atps
+val remote_atps = map fst remote_atps
+val atps = map fst atps
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 16:09:23 2022 +0100
@@ -24,6 +24,7 @@
open Sledgehammer_Fact
open Sledgehammer_ATP_Systems
open Sledgehammer_Prover
+open Sledgehammer_Prover_SMT
open Sledgehammer_Prover_Minimize
open Sledgehammer_MaSh
open Sledgehammer
@@ -167,14 +168,9 @@
if is_prover_supported ctxt remote_name then SOME remote_name else NONE
end
-fun remotify_prover_if_not_installed ctxt name =
- if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
- else remotify_prover_if_supported_and_not_already_remote ctxt name
-
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value ctxt =
- [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN] \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
- |> map_filter (remotify_prover_if_not_installed ctxt)
+ filter (is_prover_installed ctxt) (atps @ smts ctxt) \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
|> implode_param
fun set_default_raw_param param thy =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100
@@ -79,7 +79,7 @@
val str_of_mode : mode -> string
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
- val is_atp : theory -> string -> bool
+ val is_atp : string -> bool
val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string ->
proof_method list list
val get_facts_of_filter : string -> (string * fact list) list -> fact list
@@ -122,7 +122,7 @@
| induction_rules_of_string "instantiate" = SOME Instantiate
| induction_rules_of_string _ = NONE
-val is_atp = member (op =) o supported_atps
+val is_atp = member (op =) atps
type params =
{debug : bool,
@@ -246,10 +246,8 @@
fun supported_provers ctxt =
let
- val thy = Proof_Context.theory_of ctxt
- val (remote_provers, local_provers) =
- sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt)
- |> List.partition (String.isPrefix remote_prefix)
+ val local_provers = sort_strings (local_atps @ SMT_Config.available_solvers_of ctxt)
+ val remote_provers = sort_strings remote_atps
in
writeln ("Supported provers: " ^ commas (local_provers @ remote_provers))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100
@@ -45,23 +45,24 @@
open Sledgehammer_Prover_SMT
fun is_prover_supported ctxt =
- let val thy = Proof_Context.theory_of ctxt in
- is_atp thy orf is_smt_prover ctxt
- end
+ is_atp orf is_smt_prover ctxt
-fun is_prover_installed ctxt =
- is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
+fun is_prover_installed ctxt prover_name =
+ if is_atp prover_name then
+ let val thy = Proof_Context.theory_of ctxt in
+ is_atp_installed thy prover_name
+ end
+ else
+ is_smt_prover_installed ctxt prover_name
fun get_prover ctxt mode name =
- let val thy = Proof_Context.theory_of ctxt in
- if is_atp thy name then run_atp mode name
- else if is_smt_prover ctxt name then run_smt_solver mode name
- else error ("No such prover: " ^ name)
- end
+ if is_atp name then run_atp mode name
+ else if is_smt_prover ctxt name then run_smt_solver mode name
+ else error ("No such prover: " ^ name)
fun get_slices ctxt name =
let val thy = Proof_Context.theory_of ctxt in
- if is_atp thy name then
+ if is_atp name then
map (apsnd SOME) (#good_slices (get_atp thy name ()) ctxt)
else if is_smt_prover ctxt name then
map (rpair NONE) (SMT_Solver.good_slices ctxt name)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100
@@ -16,7 +16,10 @@
val smt_triggers : bool Config.T
val is_smt_prover : Proof.context -> string -> bool
+ val is_smt_prover_installed : Proof.context -> string -> bool
val run_smt_solver : mode -> string -> prover
+
+ val smts : Proof.context -> string list
end;
structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
@@ -35,7 +38,10 @@
val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true)
val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true)
-val is_smt_prover = member (op =) o SMT_Config.available_solvers_of
+val smts = SMT_Config.all_solvers_of
+
+val is_smt_prover = member (op =) o smts
+val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
properly in the SMT module, we must interpret these here. *)