# HG changeset patch
# User blanchet
# Date 1291397241 -3600
# Node ID ff805bb109d89fa8db5b10e9985835d0007626fa
# Parent  2c150063cd4d7cd73471fc66aec29a4640421228
export more information about available SMT solvers

diff -r 2c150063cd4d -r ff805bb109d8 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Dec 03 17:59:13 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Dec 03 18:27:21 2010 +0100
@@ -27,8 +27,11 @@
   type solver = bool option -> Proof.context -> (int * thm) list ->
     int list * thm
   val add_solver: solver_config -> theory -> theory
+  val solver_name_of: Proof.context -> string
   val solver_of: Proof.context -> solver
-  val is_locally_installed: Proof.context -> bool
+  val available_solvers_of: Proof.context -> string list
+  val is_locally_installed: Proof.context -> string -> bool
+  val is_remotely_available: Proof.context -> string -> bool
 
   (*filter*)
   val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
@@ -295,14 +298,19 @@
   let val name = C.solver_of ctxt
   in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end
 
+val solver_name_of = fst o name_and_solver_of
 fun solver_of ctxt =
   let val (name, raw_solver) = name_and_solver_of ctxt
   in gen_solver name raw_solver end
 
-fun is_locally_installed ctxt =
-  let val (_, {env_var, ...}) = name_and_solver_of ctxt
+val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof
+
+fun is_locally_installed ctxt name =
+  let val {env_var, ...} = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
   in is_some (get_local_solver env_var) end
 
+fun is_remotely_available ctxt name =
+  #is_remote (the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name))
 
 
 (* filter *)