--- a/src/HOL/Tools/SMT/smt_config.ML Tue Feb 28 21:58:59 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Wed Feb 29 17:43:41 2012 +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 is_available: Proof.context -> string -> bool
val available_solvers_of: Proof.context -> string list
val select_solver: string -> Context.generic -> Context.generic
val solver_of: Proof.context -> string
--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Feb 28 21:58:59 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Feb 29 17:43:41 2012 +0100
@@ -237,10 +237,13 @@
fun gen_apply (ithms, ctxt) =
let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt
in
- (ithms, ctxt)
- |-> invoke name command
- |> reconstruct ctxt
- |>> distinct (op =)
+ if not (SMT_Config.is_available ctxt name) then
+ error ("The SMT solver " ^ quote name ^ " is not installed.")
+ else
+ (ithms, ctxt)
+ |-> invoke name command
+ |> reconstruct ctxt
+ |>> distinct (op =)
end
fun apply_solver ctxt = gen_apply o gen_preprocess ctxt