better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)

--- a/NEWS	Mon Nov 08 11:49:28 2010 +0100
+++ b/NEWS	Mon Nov 08 12:13:44 2010 +0100
@@ -350,9 +350,10 @@
     z3_trace_assms ~> smt_trace_used_facts
     INCOMPATIBILITY.
   - Added:
+    smt_verbose
+    smt_datatypes
     cvc3_options
     yices_options
-    smt_datatypes
 
 * Removed [split_format ... and ... and ...] version of
 [split_format].  Potential INCOMPATIBILITY.

--- a/src/HOL/IsaMakefile	Mon Nov 08 11:49:28 2010 +0100
+++ b/src/HOL/IsaMakefile	Mon Nov 08 12:13:44 2010 +0100
@@ -340,6 +340,8 @@
   Tools/smallvalue_generators.ML \
   Tools/SMT/smtlib_interface.ML \
   Tools/SMT/smt_builtin.ML \
+  Tools/SMT/smt_config.ML \
+  Tools/SMT/smt_failure.ML \
   Tools/SMT/smt_monomorph.ML \
   Tools/SMT/smt_normalize.ML \
   Tools/SMT/smt_setup_solvers.ML \

--- a/src/HOL/SMT.thy	Mon Nov 08 11:49:28 2010 +0100
+++ b/src/HOL/SMT.thy	Mon Nov 08 12:13:44 2010 +0100
@@ -8,7 +8,9 @@
 imports List
 uses
   "Tools/Datatype/datatype_selectors.ML"
-  ("Tools/SMT/smt_monomorph.ML")
+  "Tools/SMT/smt_failure.ML"
+  "Tools/SMT/smt_config.ML"
+  "Tools/SMT/smt_monomorph.ML"
   ("Tools/SMT/smt_builtin.ML")
   ("Tools/SMT/smt_normalize.ML")
   ("Tools/SMT/smt_translate.ML")
@@ -126,7 +128,6 @@
 
 subsection {* Setup *}
 
-use "Tools/SMT/smt_monomorph.ML"
 use "Tools/SMT/smt_builtin.ML"
 use "Tools/SMT/smt_normalize.ML"
 use "Tools/SMT/smt_translate.ML"
@@ -141,6 +142,7 @@
 use "Tools/SMT/smt_setup_solvers.ML"
 
 setup {*
+  SMT_Config.setup #>
   SMT_Solver.setup #>
   Z3_Proof_Reconstruction.setup #>
   SMT_Setup_Solvers.setup
@@ -241,6 +243,13 @@
 subsection {* Tracing *}
 
 text {*
+The SMT method, when applied, traces important information.  To
+make it entirely silent, set the following option to @{text false}.
+*}
+
+declare [[ smt_verbose = true ]]
+
+text {*
 For tracing the generated problem file given to the SMT solver as
 well as the returned result of the solver, the option
 @{text smt_trace} should be set to @{text true}.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Nov 08 12:13:44 2010 +0100
@@ -0,0 +1,232 @@
+(*  Title:      HOL/Tools/SMT/smt_config.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Configuration options and diagnostic tools for SMT.
+*)
+
+signature SMT_CONFIG =
+sig
+  (*solver*)
+  val add_solver: string -> Context.generic -> Context.generic
+  val set_solver_options: string * string -> Context.generic -> Context.generic
+  val select_solver: string -> Context.generic -> Context.generic
+  val solver_of: Proof.context -> string
+  val solver_options_of: Proof.context -> string list
+
+  (*options*)
+  val oracle: bool Config.T
+  val datatypes: bool Config.T
+  val timeout: real Config.T
+  val fixed: bool Config.T
+  val verbose: bool Config.T
+  val traceN: string
+  val trace: bool Config.T
+  val trace_used_facts: bool Config.T
+  val monomorph_limit: int Config.T
+  val drop_bad_facts: bool Config.T
+  val filter_only_facts: bool Config.T
+
+  (*tools*)
+  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
+
+  (*diagnostics*)
+  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
+  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
+
+  (*certificates*)
+  val select_certificates: string -> Context.generic -> Context.generic
+  val certificates_of: Proof.context -> Cache_IO.cache option
+
+  (*setup*)
+  val setup: theory -> theory
+  val print_setup: Proof.context -> unit
+end
+
+structure SMT_Config: SMT_CONFIG =
+struct
+
+(* solver *)
+
+structure Solvers = Generic_Data
+(
+  type T = string list Symtab.table * string option
+  val empty = (Symtab.empty, NONE)
+  val extend = I
+  fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
+)
+
+fun set_solver_options (name, options) =
+  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
+  in Solvers.map (apfst (Symtab.map_entry name (K opts))) end
+
+fun add_solver name context =
+  if Symtab.defined (fst (Solvers.get context)) name then
+    error ("Solver already registered: " ^ quote name)
+  else
+    context
+    |> Solvers.map (apfst (Symtab.update (name, [])))
+    |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
+        (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+          (Thm.declaration_attribute o K o set_solver_options o pair name))
+        ("Additional command line options for SMT solver " ^ quote name))
+
+fun select_solver name context =
+  if Symtab.defined (fst (Solvers.get context)) name then
+    Solvers.map (apsnd (K (SOME name))) context
+  else error ("Trying to select unknown solver: " ^ quote name)
+
+val lookup_solver = snd o Solvers.get o Context.Proof
+
+fun solver_of ctxt =
+  (case lookup_solver ctxt of
+    SOME name => name
+  | NONE => error "No SMT solver selected")
+
+fun solver_options_of ctxt =
+  (case lookup_solver ctxt of
+    NONE => []
+  | SOME name =>
+      Symtab.lookup_list (fst (Solvers.get (Context.Proof ctxt))) name)
+
+val setup_solver =
+  Attrib.setup @{binding smt_solver}
+    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+      (Thm.declaration_attribute o K o select_solver))
+    "SMT solver configuration"
+
+
+(* options *)
+
+val oracleN = "smt_oracle"
+val (oracle, setup_oracle) = Attrib.config_bool oracleN (K true)
+
+val datatypesN = "smt_datatypes"
+val (datatypes, setup_datatypes) = Attrib.config_bool datatypesN (K false)
+
+val timeoutN = "smt_timeout"
+val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
+
+val fixedN = "smt_fixed"
+val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
+
+val verboseN = "smt_verbose"
+val (verbose, setup_verbose) = Attrib.config_bool verboseN (K true)
+
+val traceN = "smt_trace"
+val (trace, setup_trace) = Attrib.config_bool traceN (K false)
+
+val trace_used_factsN = "smt_trace_used_facts"
+val (trace_used_facts, setup_trace_used_facts) =
+  Attrib.config_bool trace_used_factsN (K false)
+
+val monomorph_limitN = "smt_monomorph_limit"
+val (monomorph_limit, setup_monomorph_limit) =
+  Attrib.config_int monomorph_limitN (K 10)
+
+val drop_bad_factsN = "smt_drop_bad_facts"
+val (drop_bad_facts, setup_drop_bad_facts) =
+  Attrib.config_bool drop_bad_factsN (K false)
+
+val filter_only_factsN = "smt_filter_only_facts"
+val (filter_only_facts, setup_filter_only_facts) =
+  Attrib.config_bool filter_only_factsN (K false)
+
+val setup_options =
+  setup_oracle #>
+  setup_datatypes #>
+  setup_timeout #>
+  setup_fixed #>
+  setup_trace #>
+  setup_verbose #>
+  setup_monomorph_limit #>
+  setup_drop_bad_facts #>
+  setup_filter_only_facts #>
+  setup_trace_used_facts
+
+
+(* diagnostics *)
+
+fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
+
+fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
+
+fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
+
+
+(* tools *)
+
+fun with_timeout ctxt f x =
+  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
+  handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+
+
+(* certificates *)
+
+structure Certificates = Generic_Data
+(
+  type T = Cache_IO.cache option
+  val empty = NONE
+  val extend = I
+  fun merge (s, _) = s
+)
+
+val get_certificates_path =
+  Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
+
+fun select_certificates name = Certificates.put (
+  if name = "" then NONE
+  else SOME (Cache_IO.make (Path.explode name)))
+
+val certificates_of = Certificates.get o Context.Proof
+
+val setup_certificates =
+  Attrib.setup @{binding smt_certificates}
+    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+      (Thm.declaration_attribute o K o select_certificates))
+    "SMT certificates configuration"
+
+
+(* setup *)
+
+val setup =
+  setup_solver #>
+  setup_options #>
+  setup_certificates
+
+fun print_setup ctxt =
+  let
+    fun string_of_bool b = if b then "true" else "false"
+
+    val (names, sel) = Solvers.get (Context.Proof ctxt) |> apfst Symtab.keys
+    val ns = if null names then ["(none)"] else sort_strings names
+    val n = the_default "(none)" sel
+    val opts = solver_options_of ctxt
+    
+    val t = string_of_real (Config.get ctxt timeout)
+
+    val certs_filename =
+      (case get_certificates_path ctxt of
+        SOME path => Path.implode path
+      | NONE => "(disabled)")
+  in
+    Pretty.writeln (Pretty.big_list "SMT setup:" [
+      Pretty.str ("Current SMT solver: " ^ n),
+      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
+      Pretty.str_list "Available SMT solvers: "  "" ns,
+      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
+      Pretty.str ("With proofs: " ^
+        string_of_bool (not (Config.get ctxt oracle))),
+      Pretty.str ("Certificates cache: " ^ certs_filename),
+      Pretty.str ("Fixed certificates: " ^
+        string_of_bool (Config.get ctxt fixed))])
+  end
+
+val _ =
+  Outer_Syntax.improper_command "smt_status"
+    ("show the available SMT solvers, the currently selected SMT solver, " ^
+      "and the values of SMT configuration options")
+    Keyword.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
+      print_setup (Toplevel.context_of state))))
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_failure.ML	Mon Nov 08 12:13:44 2010 +0100
@@ -0,0 +1,41 @@
+(*  Title:      HOL/Tools/SMT/smt_failure.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Failures and exception of SMT.
+*)
+
+signature SMT_FAILURE =
+sig
+  datatype failure =
+    Counterexample of bool * term list |
+    Time_Out |
+    Out_Of_Memory |
+    Other_Failure of string
+  val string_of_failure: Proof.context -> failure -> string
+  exception SMT of failure
+end
+
+structure SMT_Failure: SMT_FAILURE =
+struct
+
+datatype failure =
+  Counterexample of bool * term list |
+  Time_Out |
+  Out_Of_Memory |
+  Other_Failure of string
+
+fun string_of_failure ctxt (Counterexample (real, ex)) =
+      let
+        val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
+      in
+        if null ex then msg
+        else Pretty.string_of (Pretty.big_list (msg ^ ":")
+          (map (Syntax.pretty_term ctxt) ex))
+      end
+  | string_of_failure _ Time_Out = "Timed out"
+  | string_of_failure _ Out_Of_Memory = "Ran out of memory"
+  | string_of_failure _ (Other_Failure msg) = msg
+
+exception SMT of failure
+
+end

--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Nov 08 11:49:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Nov 08 12:13:44 2010 +0100
@@ -92,16 +92,19 @@
    computation uses only the constants occurring with schematic type
    variables in the propositions. To ease comparisons, such sets of
    costants are always kept in their initial order. *)
-fun incremental_monomorph thy limit all_grounds new_grounds irules =
+fun incremental_monomorph ctxt limit all_grounds new_grounds irules =
   let
+    val thy = ProofContext.theory_of ctxt
     val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
     val spec = specialize thy all_grounds' new_grounds
     val (irs, new_grounds') = fold_map spec irules Symtab.empty
   in
     if Symtab.is_empty new_grounds' then irs
     else if limit > 0
-    then incremental_monomorph thy (limit-1) all_grounds' new_grounds' irs
-    else (warning "SMT: monomorphization limit reached"; irs)
+    then incremental_monomorph ctxt (limit-1) all_grounds' new_grounds' irs
+    else
+     (SMT_Config.verbose_msg ctxt (K "Warning: Monomorphization limit reached")
+      (); irs)
   end
 
 
@@ -175,7 +178,7 @@
       in
         polys
         |> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)]))
-        |> incremental_monomorph thy limit Symtab.empty grounds
+        |> incremental_monomorph ctxt' limit Symtab.empty grounds
         |> map (apsnd (filter_most_specific thy))
         |> flat o map2 (instantiate thy) Tenvs
         |> append monos
@@ -183,9 +186,6 @@
       end
 
 
-val monomorph_limit = 10
-
-
 (* Instantiate all polymorphic constants (i.e., constants occurring
    both with ground types and type variables) with all (necessary)
    ground types; thereby create copies of theorems containing those
@@ -199,6 +199,6 @@
   irules
   |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
   |>> incr_indexes
-  |-> mono_all ctxt monomorph_limit
+  |-> mono_all ctxt (Config.get ctxt SMT_Config.monomorph_limit)
 
 end

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 08 11:49:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 08 12:13:44 2010 +0100
@@ -19,8 +19,7 @@
 sig
   type extra_norm = bool -> (int * thm) list -> Proof.context ->
     (int * thm) list * Proof.context
-  val normalize: (Proof.context -> (thm -> string) -> thm -> unit) -> bool ->
-    extra_norm -> bool -> (int * thm) list -> Proof.context ->
+  val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
     (int * thm) list * Proof.context
   val atomize_conv: Proof.context -> conv
   val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
@@ -247,7 +246,7 @@
             then eta_args_conv norm_conv
               (length (Term.binder_types T) - length ts)
             else args_conv o norm_conv
-        | (_, ts) => args_conv o norm_conv)) ctxt ct
+        | _ => args_conv o norm_conv)) ctxt ct
 
   fun is_normed ctxt t =
     (case t of
@@ -516,15 +515,15 @@
 
 fun with_context f irules ctxt = (f ctxt irules, ctxt)
 
-fun normalize trace keep_assms extra_norm with_datatypes irules ctxt =
+fun normalize extra_norm with_datatypes irules ctxt =
   let
     fun norm f ctxt' (i, thm) =
-      if keep_assms then SOME (i, f ctxt' thm)
-      else
+      if Config.get ctxt' SMT_Config.drop_bad_facts then
         (case try (f ctxt') thm of
           SOME thm' => SOME (i, thm')
-        | NONE => (trace ctxt' (prefix ("SMT warning: " ^
+        | NONE => (SMT_Config.verbose_msg ctxt' (prefix ("Warning: " ^
             "dropping assumption: ") o Display.string_of_thm ctxt') thm; NONE))
+      else SOME (i, f ctxt' thm)
   in
     irules
     |> trivial_distinct ctxt

--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Nov 08 11:49:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Nov 08 12:13:44 2010 +0100
@@ -16,9 +16,9 @@
   if String.isPrefix unsat line then SMT_Solver.Unsat
   else if String.isPrefix sat line then SMT_Solver.Sat
   else if String.isPrefix unknown line then SMT_Solver.Unknown
-  else raise SMT_Solver.SMT (SMT_Solver.Other_Failure ("Solver " ^
+  else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
     quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
-    "configuration option " ^ quote SMT_Solver.traceN ^ " and " ^
+    "configuration option " ^ quote SMT_Config.traceN ^ " and " ^
     " see the trace for details."))
 
 fun on_first_line test_outcome solver_name lines =
@@ -60,14 +60,14 @@
 
 fun z3_options ctxt =
   ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
-  |> not (Config.get ctxt SMT_Solver.oracle) ?
+  |> not (Config.get ctxt SMT_Config.oracle) ?
        append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
 
 fun z3_on_last_line solver_name lines =
   let
     fun junk l =
       if String.isPrefix "WARNING: Out of allocated virtual memory" l
-      then raise SMT_Solver.SMT SMT_Solver.Out_Of_Memory
+      then raise SMT_Failure.SMT SMT_Failure.Out_Of_Memory
       else
         String.isPrefix "WARNING" l orelse
         String.isPrefix "ERROR" l orelse

--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 08 11:49:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 08 12:13:44 2010 +0100
@@ -6,14 +6,7 @@
 
 signature SMT_SOLVER =
 sig
-  datatype failure =
-    Counterexample of bool * term list |
-    Time_Out |
-    Out_Of_Memory |
-    Other_Failure of string
-  val string_of_failure: Proof.context -> string -> failure -> string
-  exception SMT of failure
-
+  (*configuration*)
   type interface = {
     extra_norm: SMT_Normalize.extra_norm,
     translate: SMT_Translate.config }
@@ -30,37 +23,16 @@
     reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
       (int list * thm) * Proof.context) option }
 
-  (*options*)
-  val oracle: bool Config.T
-  val filter_only: bool Config.T
-  val datatypes: bool Config.T
-  val keep_assms: bool Config.T
-  val timeout: real Config.T
-  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
-  val traceN: string
-  val trace: bool Config.T
-  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
-  val trace_used_facts: bool Config.T
-
-  (*certificates*)
-  val fixed_certificates: bool Config.T
-  val select_certificates: string -> Context.generic -> Context.generic
-
-  (*solvers*)
+  (*registry*)
   type solver = bool option -> Proof.context -> (int * thm) list ->
     int list * thm
   val add_solver: solver_config -> theory -> theory
-  val set_solver_options: string -> string -> Context.generic ->
-    Context.generic
-  val all_solver_names_of: Context.generic -> string list
-  val solver_name_of: Context.generic -> string
-  val select_solver: string -> Context.generic -> Context.generic
-  val solver_of: Context.generic -> solver
+  val solver_of: Proof.context -> solver
   val is_locally_installed: Proof.context -> bool
 
   (*filter*)
   val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
-    {outcome: failure option, used_facts: 'a list,
+    {outcome: SMT_Failure.failure option, used_facts: 'a list,
     run_time_in_msecs: int option}
 
   (*tactic*)
@@ -69,31 +41,15 @@
 
   (*setup*)
   val setup: theory -> theory
-  val print_setup: Context.generic -> unit
 end
 
 structure SMT_Solver: SMT_SOLVER =
 struct
 
-datatype failure =
-  Counterexample of bool * term list |
-  Time_Out |
-  Out_Of_Memory |
-  Other_Failure of string
+structure C = SMT_Config
 
-fun string_of_failure ctxt _ (Counterexample (real, ex)) =
-      let
-        val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
-      in
-        if null ex then msg ^ "."
-        else Pretty.string_of (Pretty.big_list (msg ^ ":")
-          (map (Syntax.pretty_term ctxt) ex))
-      end
-  | string_of_failure _ name Time_Out = name ^ " timed out."
-  | string_of_failure _ name Out_Of_Memory = name ^ " ran out of memory."
-  | string_of_failure _ _ (Other_Failure msg) = msg
 
-exception SMT of failure
+(* configuration *)
 
 type interface = {
   extra_norm: SMT_Normalize.extra_norm,
@@ -114,57 +70,6 @@
     (int list * thm) * Proof.context) option }
 
 
-
-(* SMT options *)
-
-val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true)
-
-val (filter_only, setup_filter_only) =
-  Attrib.config_bool "smt_filter_only" (K false)
-
-val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
-
-val (keep_assms, setup_keep_assms) =
-  Attrib.config_bool "smt_keep_assms" (K true)
-
-val (timeout, setup_timeout) = Attrib.config_real "smt_timeout" (K 30.0)
-
-fun with_timeout ctxt f x =
-  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
-  handle TimeLimit.TimeOut => raise SMT Time_Out
-
-val traceN = "smt_trace"
-val (trace, setup_trace) = Attrib.config_bool traceN (K false)
-
-fun trace_msg ctxt f x =
-  if Config.get ctxt trace then tracing (f x) else ()
-
-val (trace_used_facts, setup_trace_used_facts) =
-  Attrib.config_bool "smt_trace_used_facts" (K false)
-
-
-(* SMT certificates *)
-
-val (fixed_certificates, setup_fixed_certificates) =
-  Attrib.config_bool "smt_fixed" (K false)
-
-structure Certificates = Generic_Data
-(
-  type T = Cache_IO.cache option
-  val empty = NONE
-  val extend = I
-  fun merge (s, _) = s
-)
-
-val get_certificates_path =
-  Option.map (Cache_IO.cache_path_of) o Certificates.get
-
-fun select_certificates name = Certificates.put (
-  if name = "" then NONE
-  else SOME (Cache_IO.make (Path.explode name)))
-
-
-
 (* interface to external solvers *)
 
 fun get_local_solver env_var =
@@ -202,12 +107,12 @@
   [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
 
 fun run ctxt cmd args input =
-  (case Certificates.get (Context.Proof ctxt) of
+  (case C.certificates_of ctxt of
     NONE => Cache_IO.run (make_cmd (choose cmd) args) input
   | SOME certs =>
       (case Cache_IO.lookup certs input of
         (NONE, key) =>
-          if Config.get ctxt fixed_certificates
+          if Config.get ctxt C.fixed
           then error ("Bad certificates cache: missing certificate")
           else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
             input
@@ -223,36 +128,37 @@
     fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
       (map Pretty.str ls))
 
-    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input
+    val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
 
-    val (res, err) = with_timeout ctxt (run ctxt cmd args) input
-    val _ = trace_msg ctxt (pretty "SMT solver:") err
+    val (res, err) = C.with_timeout ctxt (run ctxt cmd args) input
+    val _ = C.trace_msg ctxt (pretty "Solver:") err
 
     val ls = rev (snd (chop_while (equal "") (rev res)))
-    val _ = trace_msg ctxt (pretty "SMT result:") ls
+    val _ = C.trace_msg ctxt (pretty "Result:") ls
   in ls end
 
 end
 
-fun trace_assms ctxt = trace_msg ctxt (Pretty.string_of o
-  Pretty.big_list "SMT assertions:" o map (Display.pretty_thm ctxt o snd))
+fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
+  Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
 
 fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
   let
     fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
-    fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
-    fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
+    fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
+    fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
   in
-    trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [
-      Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)),
-      Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) ()
+    C.trace_msg ctxt (fn () =>
+      Pretty.string_of (Pretty.big_list "Names:" [
+        Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
+        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
   end
 
-fun invoke translate_config name cmd more_opts options irules ctxt =
+fun invoke translate_config name cmd options irules ctxt =
   let
-    val args = more_opts @ options ctxt
+    val args = C.solver_options_of ctxt @ options ctxt
     val comments = ("solver: " ^ name) ::
-      ("timeout: " ^ Time.toString (seconds (Config.get ctxt timeout))) ::
+      ("timeout: " ^ Time.toString (seconds (Config.get ctxt C.timeout))) ::
       "arguments:" :: args
   in
     irules
@@ -283,7 +189,7 @@
     val thms = filter (fn i => i >= 0) idxs
       |> map_filter (AList.lookup (op =) irules)
   in
-    if Config.get ctxt trace_used_facts andalso length thms > 0
+    if Config.get ctxt C.trace_used_facts andalso length thms > 0
     then
       tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
         (map (Display.pretty_thm ctxt) thms)))
@@ -292,17 +198,15 @@
 
 fun gen_solver name info rm ctxt irules =
   let
-    val {env_var, is_remote, options, more_options, interface, reconstruct} =
-      info
+    val {env_var, is_remote, options, interface, reconstruct} = info
     val {extra_norm, translate} = interface
     val (with_datatypes, translate') =
-      set_has_datatypes (Config.get ctxt datatypes) translate
+      set_has_datatypes (Config.get ctxt C.datatypes) translate
     val cmd = (rm, env_var, is_remote, name)
-    val keep = Config.get ctxt keep_assms
   in
     (irules, ctxt)
-    |-> SMT_Normalize.normalize trace_msg keep extra_norm with_datatypes
-    |-> invoke translate' name cmd more_options options
+    |-> SMT_Normalize.normalize extra_norm with_datatypes
+    |-> invoke translate' name cmd options
     |-> reconstruct
     |-> (fn (idxs, thm) => fn ctxt' => thm
     |> singleton (ProofContext.export ctxt' ctxt)
@@ -313,7 +217,7 @@
 
 
 
-(* solver store *)
+(* registry *)
 
 type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
 
@@ -321,7 +225,6 @@
   env_var: string,
   is_remote: bool,
   options: Proof.context -> string list,
-  more_options: string list,
   interface: interface,
   reconstruct: string list * SMT_Translate.recon -> Proof.context ->
     (int list * thm) * Proof.context }
@@ -335,24 +238,18 @@
     handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
 )
 
-val no_solver = "(none)"
-
-fun set_solver_options name opts = Solvers.map (Symtab.map_entry name (fn
-  {env_var, is_remote, options, interface, reconstruct, ...} =>
-  {env_var=env_var, is_remote=is_remote, options=options,
-   more_options=String.tokens (Symbol.is_ascii_blank o str) opts,
-   interface=interface, reconstruct=reconstruct}))
-
 local
   fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt =
     (case outcome output of
       (Unsat, ls) =>
-        if not (Config.get ctxt oracle) andalso is_some reconstruct
+        if not (Config.get ctxt C.oracle) andalso is_some reconstruct
         then the reconstruct ctxt recon ls
         else (([], ocl ()), ctxt)
     | (result, ls) =>
         let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
-        in raise SMT (Counterexample (result = Sat, ts)) end)
+        in
+          raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
+        end)
 in
 
 fun add_solver cfg =
@@ -363,59 +260,31 @@
     fun core_oracle () = @{cprop False}
 
     fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
-      more_options=[], interface=interface,
+      interface=interface,
       reconstruct=finish (outcome name) cex_parser reconstruct ocl }
   in
     Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
     Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
-    Attrib.setup (Binding.name (name ^ "_options"))
-      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
-        (Thm.declaration_attribute o K o set_solver_options name))
-      ("Additional command line options for SMT solver " ^ quote name)
+    Context.theory_map (C.add_solver name)
   end
 
 end
 
-val all_solver_names_of = Symtab.keys o Solvers.get
-val lookup_solver = Symtab.lookup o Solvers.get
-
-
-
-(* selected solver *)
-
-structure Selected_Solver = Generic_Data
-(
-  type T = string
-  val empty = no_solver
-  val extend = I
-  fun merge (s, _) = s
-)
+fun name_and_solver_of ctxt =
+  let val name = C.solver_of ctxt
+  in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end
 
-val solver_name_of = Selected_Solver.get
-
-fun select_solver name context =
-  if is_none (lookup_solver context name)
-  then error ("SMT solver not registered: " ^ quote name)
-  else Selected_Solver.map (K name) context
-
-fun raw_solver_of context name =
-  (case lookup_solver context name of
-    NONE => error "No SMT solver selected"
-  | SOME s => s)
-
-fun solver_of context =
-  let val name = solver_name_of context
-  in gen_solver name (raw_solver_of context name) end
+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 name = solver_name_of (Context.Proof ctxt)
-    val {env_var, ...} = raw_solver_of (Context.Proof ctxt) name
+  let val (_, {env_var, ...}) = name_and_solver_of ctxt
   in is_some (get_local_solver env_var) end
 
 
 
-(* SMT filter *)
+(* filter *)
 
 val has_topsort = Term.exists_type (Term.exists_subtype (fn
     TFree (_, []) => true
@@ -424,19 +293,20 @@
 
 fun smt_solver rm ctxt irules =
   (* without this test, we would run into problems when atomizing the rules: *)
-  if exists (has_topsort o Thm.prop_of o snd) irules
-  then raise SMT (Other_Failure "proof state contains the universal sort {}")
-  else solver_of (Context.Proof ctxt) rm ctxt irules
+  if exists (has_topsort o Thm.prop_of o snd) irules then
+    raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
+      "contains the universal sort {}"))
+  else solver_of ctxt rm ctxt irules
 
 fun smt_filter run_remote time_limit st xrules i =
   let
     val {facts, goal, ...} = Proof.goal st
     val ctxt =
       Proof.context_of st
-      |> Config.put timeout (Real.fromInt (Time.toSeconds time_limit))
-      |> Config.put oracle false
-      |> Config.put filter_only true
-      |> Config.put keep_assms false
+      |> Config.put C.oracle false
+      |> Config.put C.timeout (Real.fromInt (Time.toSeconds time_limit))
+      |> Config.put C.drop_bad_facts true
+      |> Config.put C.filter_only_facts true
     val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     val cprop =
       concl
@@ -450,7 +320,8 @@
     |-> map_filter o try o nth
     |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
   end
-  handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs=NONE}
+  handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[],
+    run_time_in_msecs=NONE}
   (* FIXME: measure runtime *)
 
 
@@ -460,14 +331,17 @@
 fun smt_tac' pass_exns ctxt rules =
   CONVERSION (SMT_Normalize.atomize_conv ctxt)
   THEN' Tactic.rtac @{thm ccontr}
-  THEN' SUBPROOF (fn {context=cx, prems, ...} =>
+  THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
     let
-      fun solve () = snd (smt_solver NONE cx (map (pair ~1) (rules @ prems)))
-      val name = solver_name_of (Context.Proof cx)
-      val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx name)
+      fun solve irules = snd (smt_solver NONE ctxt' irules)
+      val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
+      val str_of = SMT_Failure.string_of_failure ctxt'
+      fun safe_solve irules =
+        if pass_exns then SOME (solve irules)
+        else (SOME (solve irules) handle SMT_Failure.SMT fail =>
+          (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
     in
-      (if pass_exns then SOME (solve ())
-       else (SOME (solve ()) handle SMT fail => (trace fail; NONE)))
+      safe_solve (map (pair ~1) (rules @ prems))
       |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
     end) ctxt
 
@@ -483,60 +357,7 @@
 (* setup *)
 
 val setup =
-  Attrib.setup @{binding smt_solver}
-    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
-      (Thm.declaration_attribute o K o select_solver))
-    "SMT solver configuration" #>
-  setup_oracle #>
-  setup_filter_only #>
-  setup_datatypes #>
-  setup_keep_assms #>
-  setup_timeout #>
-  setup_trace #>
-  setup_trace_used_facts #>
-  setup_fixed_certificates #>
-  Attrib.setup @{binding smt_certificates}
-    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
-      (Thm.declaration_attribute o K o select_certificates))
-    "SMT certificates" #>
   Method.setup @{binding smt} smt_method
     "Applies an SMT solver to the current goal."
 
-
-fun print_setup context =
-  let
-    val t = Time.toString (seconds (Config.get_generic context timeout))
-    val names = sort_strings (all_solver_names_of context)
-    val ns = if null names then [no_solver] else names
-    val n = solver_name_of context
-    val opts =
-      (case Symtab.lookup (Solvers.get context) n of
-        NONE => []
-      | SOME {more_options, options, ...} =>
-          more_options @ options (Context.proof_of context))
-    val certs_filename =
-      (case get_certificates_path context of
-        SOME path => Path.implode path
-      | NONE => "(disabled)")
-    val fixed = if Config.get_generic context fixed_certificates then "true"
-      else "false"
-  in
-    Pretty.writeln (Pretty.big_list "SMT setup:" [
-      Pretty.str ("Current SMT solver: " ^ n),
-      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
-      Pretty.str_list "Available SMT solvers: "  "" ns,
-      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
-      Pretty.str ("With proofs: " ^
-        (if Config.get_generic context oracle then "false" else "true")),
-      Pretty.str ("Certificates cache: " ^ certs_filename),
-      Pretty.str ("Fixed certificates: " ^ fixed)])
-  end
-
-val _ =
-  Outer_Syntax.improper_command "smt_status"
-    "show the available SMT solvers and the currently selected solver"
-    Keyword.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
-      print_setup (Context.Proof (Toplevel.context_of state)))))
-
 end

--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 08 11:49:28 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 08 12:13:44 2010 +0100
@@ -240,7 +240,7 @@
 
 (* core parser *)
 
-fun parse_exn line_no msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
+fun parse_exn line_no msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
   ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg))
 
 fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg

--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 08 11:49:28 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 08 12:13:44 2010 +0100
@@ -19,7 +19,7 @@
 structure T = Z3_Proof_Tools
 structure L = Z3_Proof_Literals
 
-fun z3_exn msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
+fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
   ("Z3 proof reconstruction: " ^ msg))
 
 
@@ -66,11 +66,11 @@
 (** proof tools **)
 
 fun named ctxt name prover ct =
-  let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
+  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
   in prover ct end
 
 fun NAMED ctxt name tac i st =
-  let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
+  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
   in tac i st end
 
 fun pretty_goal ctxt thms t =
@@ -90,7 +90,7 @@
     fun apply [] ct = error (try_apply_err ct)
       | apply (prover :: provers) ct =
           (case try prover ct of
-            SOME thm => (SMT_Solver.trace_msg ctxt I "Z3: succeeded"; thm)
+            SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
           | NONE => apply provers ct)
 
   in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end
@@ -732,9 +732,9 @@
 in
 fun trace_rule idx prove r ps ct (cxp as (ctxt, ptab)) =
   let
-    val _ = SMT_Solver.trace_msg ctxt (header idx r o count_rules) ptab
+    val _ = SMT_Config.trace_msg ctxt (header idx r o count_rules) ptab
     val result as (p, (ctxt', _)) = prove r ps ct cxp
-    val _ = if not (Config.get ctxt' SMT_Solver.trace) then ()
+    val _ = if not (Config.get ctxt' SMT_Config.trace) then ()
       else check ctxt' idx r ps ct p
   in result end
 end
@@ -844,7 +844,7 @@
     val (idx, (ptab, vars, cx)) = P.parse ctxt typs terms output
     val assms' = prepare_assms cx unfolds assms
   in
-    if Config.get cx SMT_Solver.filter_only
+    if Config.get cx SMT_Config.filter_only_facts
     then ((filter_assms cx assms' ptab idx [], @{thm TrueI}), cx)
     else apfst (pair []) (prove cx assms' vars idx ptab)
   end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 11:49:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 12:13:44 2010 +0100
@@ -409,9 +409,9 @@
      run_time_in_msecs = msecs}
   end
 
-fun failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
-  | failure_from_smt_failure SMT_Solver.Time_Out = TimedOut
-  | failure_from_smt_failure SMT_Solver.Out_Of_Memory = OutOfResources
+fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
+  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
+  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
 
 val smt_max_iter = 5
@@ -473,10 +473,10 @@
                          (apply_on_subgoal subgoal subgoal_count ^
                           command_call smtN (map fst used_facts)) ^
         minimize_line minimize_command (map fst used_facts)
-      | SOME SMT_Solver.Time_Out => "Timed out."
-      | SOME (SMT_Solver.Counterexample _) => "The SMT problem is unprovable."
+      | SOME SMT_Failure.Time_Out => "Timed out."
+      | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
       | SOME failure =>
-        SMT_Solver.string_of_failure ctxt "The SMT solver" failure
+        SMT_Failure.string_of_failure ctxt failure
     val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
   in
     {outcome = outcome, used_facts = used_facts,