# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID 212e9ec706cf5bd9aef65968160817f5d4a7e092 # Parent ed510a3693e2cbe998de6f9f1f9731052ae30c53 run all installed provers by default diff -r ed510a3693e2 -r 212e9ec706cf src/Doc/Sledgehammer/document/root.tex --- 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: diff -r ed510a3693e2 -r 212e9ec706cf src/HOL/Tools/SMT/smt_config.ML --- 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 diff -r ed510a3693e2 -r 212e9ec706cf src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 diff -r ed510a3693e2 -r 212e9ec706cf src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- 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; diff -r ed510a3693e2 -r 212e9ec706cf src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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] \ \see also \<^system_option>\sledgehammer_provers\\ - |> map_filter (remotify_prover_if_not_installed ctxt) + filter (is_prover_installed ctxt) (atps @ smts ctxt) \ \see also \<^system_option>\sledgehammer_provers\\ |> implode_param fun set_default_raw_param param thy = diff -r ed510a3693e2 -r 212e9ec706cf src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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 diff -r ed510a3693e2 -r 212e9ec706cf src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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) diff -r ed510a3693e2 -r 212e9ec706cf src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- 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>\sledgehammer_smt_builtins\ (K true) val smt_triggers = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_triggers\ (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. *)