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)
authorboehmes
Mon Nov 08 12:13:44 2010 +0100 (2010-11-08)
changeset 404247550b2cba1cb
parent 40423 6923b39ad91f
child 40425 c9b5e0fcee31
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)
NEWS
src/HOL/IsaMakefile
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_failure.ML
src/HOL/Tools/SMT/smt_monomorph.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/z3_proof_parser.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
     1.1 --- a/NEWS	Mon Nov 08 11:49:28 2010 +0100
     1.2 +++ b/NEWS	Mon Nov 08 12:13:44 2010 +0100
     1.3 @@ -350,9 +350,10 @@
     1.4      z3_trace_assms ~> smt_trace_used_facts
     1.5      INCOMPATIBILITY.
     1.6    - Added:
     1.7 +    smt_verbose
     1.8 +    smt_datatypes
     1.9      cvc3_options
    1.10      yices_options
    1.11 -    smt_datatypes
    1.12  
    1.13  * Removed [split_format ... and ... and ...] version of
    1.14  [split_format].  Potential INCOMPATIBILITY.
     2.1 --- a/src/HOL/IsaMakefile	Mon Nov 08 11:49:28 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Mon Nov 08 12:13:44 2010 +0100
     2.3 @@ -340,6 +340,8 @@
     2.4    Tools/smallvalue_generators.ML \
     2.5    Tools/SMT/smtlib_interface.ML \
     2.6    Tools/SMT/smt_builtin.ML \
     2.7 +  Tools/SMT/smt_config.ML \
     2.8 +  Tools/SMT/smt_failure.ML \
     2.9    Tools/SMT/smt_monomorph.ML \
    2.10    Tools/SMT/smt_normalize.ML \
    2.11    Tools/SMT/smt_setup_solvers.ML \
     3.1 --- a/src/HOL/SMT.thy	Mon Nov 08 11:49:28 2010 +0100
     3.2 +++ b/src/HOL/SMT.thy	Mon Nov 08 12:13:44 2010 +0100
     3.3 @@ -8,7 +8,9 @@
     3.4  imports List
     3.5  uses
     3.6    "Tools/Datatype/datatype_selectors.ML"
     3.7 -  ("Tools/SMT/smt_monomorph.ML")
     3.8 +  "Tools/SMT/smt_failure.ML"
     3.9 +  "Tools/SMT/smt_config.ML"
    3.10 +  "Tools/SMT/smt_monomorph.ML"
    3.11    ("Tools/SMT/smt_builtin.ML")
    3.12    ("Tools/SMT/smt_normalize.ML")
    3.13    ("Tools/SMT/smt_translate.ML")
    3.14 @@ -126,7 +128,6 @@
    3.15  
    3.16  subsection {* Setup *}
    3.17  
    3.18 -use "Tools/SMT/smt_monomorph.ML"
    3.19  use "Tools/SMT/smt_builtin.ML"
    3.20  use "Tools/SMT/smt_normalize.ML"
    3.21  use "Tools/SMT/smt_translate.ML"
    3.22 @@ -141,6 +142,7 @@
    3.23  use "Tools/SMT/smt_setup_solvers.ML"
    3.24  
    3.25  setup {*
    3.26 +  SMT_Config.setup #>
    3.27    SMT_Solver.setup #>
    3.28    Z3_Proof_Reconstruction.setup #>
    3.29    SMT_Setup_Solvers.setup
    3.30 @@ -241,6 +243,13 @@
    3.31  subsection {* Tracing *}
    3.32  
    3.33  text {*
    3.34 +The SMT method, when applied, traces important information.  To
    3.35 +make it entirely silent, set the following option to @{text false}.
    3.36 +*}
    3.37 +
    3.38 +declare [[ smt_verbose = true ]]
    3.39 +
    3.40 +text {*
    3.41  For tracing the generated problem file given to the SMT solver as
    3.42  well as the returned result of the solver, the option
    3.43  @{text smt_trace} should be set to @{text true}.
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Nov 08 12:13:44 2010 +0100
     4.3 @@ -0,0 +1,232 @@
     4.4 +(*  Title:      HOL/Tools/SMT/smt_config.ML
     4.5 +    Author:     Sascha Boehme, TU Muenchen
     4.6 +
     4.7 +Configuration options and diagnostic tools for SMT.
     4.8 +*)
     4.9 +
    4.10 +signature SMT_CONFIG =
    4.11 +sig
    4.12 +  (*solver*)
    4.13 +  val add_solver: string -> Context.generic -> Context.generic
    4.14 +  val set_solver_options: string * string -> Context.generic -> Context.generic
    4.15 +  val select_solver: string -> Context.generic -> Context.generic
    4.16 +  val solver_of: Proof.context -> string
    4.17 +  val solver_options_of: Proof.context -> string list
    4.18 +
    4.19 +  (*options*)
    4.20 +  val oracle: bool Config.T
    4.21 +  val datatypes: bool Config.T
    4.22 +  val timeout: real Config.T
    4.23 +  val fixed: bool Config.T
    4.24 +  val verbose: bool Config.T
    4.25 +  val traceN: string
    4.26 +  val trace: bool Config.T
    4.27 +  val trace_used_facts: bool Config.T
    4.28 +  val monomorph_limit: int Config.T
    4.29 +  val drop_bad_facts: bool Config.T
    4.30 +  val filter_only_facts: bool Config.T
    4.31 +
    4.32 +  (*tools*)
    4.33 +  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
    4.34 +
    4.35 +  (*diagnostics*)
    4.36 +  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
    4.37 +  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
    4.38 +
    4.39 +  (*certificates*)
    4.40 +  val select_certificates: string -> Context.generic -> Context.generic
    4.41 +  val certificates_of: Proof.context -> Cache_IO.cache option
    4.42 +
    4.43 +  (*setup*)
    4.44 +  val setup: theory -> theory
    4.45 +  val print_setup: Proof.context -> unit
    4.46 +end
    4.47 +
    4.48 +structure SMT_Config: SMT_CONFIG =
    4.49 +struct
    4.50 +
    4.51 +(* solver *)
    4.52 +
    4.53 +structure Solvers = Generic_Data
    4.54 +(
    4.55 +  type T = string list Symtab.table * string option
    4.56 +  val empty = (Symtab.empty, NONE)
    4.57 +  val extend = I
    4.58 +  fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
    4.59 +)
    4.60 +
    4.61 +fun set_solver_options (name, options) =
    4.62 +  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
    4.63 +  in Solvers.map (apfst (Symtab.map_entry name (K opts))) end
    4.64 +
    4.65 +fun add_solver name context =
    4.66 +  if Symtab.defined (fst (Solvers.get context)) name then
    4.67 +    error ("Solver already registered: " ^ quote name)
    4.68 +  else
    4.69 +    context
    4.70 +    |> Solvers.map (apfst (Symtab.update (name, [])))
    4.71 +    |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
    4.72 +        (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
    4.73 +          (Thm.declaration_attribute o K o set_solver_options o pair name))
    4.74 +        ("Additional command line options for SMT solver " ^ quote name))
    4.75 +
    4.76 +fun select_solver name context =
    4.77 +  if Symtab.defined (fst (Solvers.get context)) name then
    4.78 +    Solvers.map (apsnd (K (SOME name))) context
    4.79 +  else error ("Trying to select unknown solver: " ^ quote name)
    4.80 +
    4.81 +val lookup_solver = snd o Solvers.get o Context.Proof
    4.82 +
    4.83 +fun solver_of ctxt =
    4.84 +  (case lookup_solver ctxt of
    4.85 +    SOME name => name
    4.86 +  | NONE => error "No SMT solver selected")
    4.87 +
    4.88 +fun solver_options_of ctxt =
    4.89 +  (case lookup_solver ctxt of
    4.90 +    NONE => []
    4.91 +  | SOME name =>
    4.92 +      Symtab.lookup_list (fst (Solvers.get (Context.Proof ctxt))) name)
    4.93 +
    4.94 +val setup_solver =
    4.95 +  Attrib.setup @{binding smt_solver}
    4.96 +    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
    4.97 +      (Thm.declaration_attribute o K o select_solver))
    4.98 +    "SMT solver configuration"
    4.99 +
   4.100 +
   4.101 +(* options *)
   4.102 +
   4.103 +val oracleN = "smt_oracle"
   4.104 +val (oracle, setup_oracle) = Attrib.config_bool oracleN (K true)
   4.105 +
   4.106 +val datatypesN = "smt_datatypes"
   4.107 +val (datatypes, setup_datatypes) = Attrib.config_bool datatypesN (K false)
   4.108 +
   4.109 +val timeoutN = "smt_timeout"
   4.110 +val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
   4.111 +
   4.112 +val fixedN = "smt_fixed"
   4.113 +val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
   4.114 +
   4.115 +val verboseN = "smt_verbose"
   4.116 +val (verbose, setup_verbose) = Attrib.config_bool verboseN (K true)
   4.117 +
   4.118 +val traceN = "smt_trace"
   4.119 +val (trace, setup_trace) = Attrib.config_bool traceN (K false)
   4.120 +
   4.121 +val trace_used_factsN = "smt_trace_used_facts"
   4.122 +val (trace_used_facts, setup_trace_used_facts) =
   4.123 +  Attrib.config_bool trace_used_factsN (K false)
   4.124 +
   4.125 +val monomorph_limitN = "smt_monomorph_limit"
   4.126 +val (monomorph_limit, setup_monomorph_limit) =
   4.127 +  Attrib.config_int monomorph_limitN (K 10)
   4.128 +
   4.129 +val drop_bad_factsN = "smt_drop_bad_facts"
   4.130 +val (drop_bad_facts, setup_drop_bad_facts) =
   4.131 +  Attrib.config_bool drop_bad_factsN (K false)
   4.132 +
   4.133 +val filter_only_factsN = "smt_filter_only_facts"
   4.134 +val (filter_only_facts, setup_filter_only_facts) =
   4.135 +  Attrib.config_bool filter_only_factsN (K false)
   4.136 +
   4.137 +val setup_options =
   4.138 +  setup_oracle #>
   4.139 +  setup_datatypes #>
   4.140 +  setup_timeout #>
   4.141 +  setup_fixed #>
   4.142 +  setup_trace #>
   4.143 +  setup_verbose #>
   4.144 +  setup_monomorph_limit #>
   4.145 +  setup_drop_bad_facts #>
   4.146 +  setup_filter_only_facts #>
   4.147 +  setup_trace_used_facts
   4.148 +
   4.149 +
   4.150 +(* diagnostics *)
   4.151 +
   4.152 +fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
   4.153 +
   4.154 +fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
   4.155 +
   4.156 +fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
   4.157 +
   4.158 +
   4.159 +(* tools *)
   4.160 +
   4.161 +fun with_timeout ctxt f x =
   4.162 +  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
   4.163 +  handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
   4.164 +
   4.165 +
   4.166 +(* certificates *)
   4.167 +
   4.168 +structure Certificates = Generic_Data
   4.169 +(
   4.170 +  type T = Cache_IO.cache option
   4.171 +  val empty = NONE
   4.172 +  val extend = I
   4.173 +  fun merge (s, _) = s
   4.174 +)
   4.175 +
   4.176 +val get_certificates_path =
   4.177 +  Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
   4.178 +
   4.179 +fun select_certificates name = Certificates.put (
   4.180 +  if name = "" then NONE
   4.181 +  else SOME (Cache_IO.make (Path.explode name)))
   4.182 +
   4.183 +val certificates_of = Certificates.get o Context.Proof
   4.184 +
   4.185 +val setup_certificates =
   4.186 +  Attrib.setup @{binding smt_certificates}
   4.187 +    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   4.188 +      (Thm.declaration_attribute o K o select_certificates))
   4.189 +    "SMT certificates configuration"
   4.190 +
   4.191 +
   4.192 +(* setup *)
   4.193 +
   4.194 +val setup =
   4.195 +  setup_solver #>
   4.196 +  setup_options #>
   4.197 +  setup_certificates
   4.198 +
   4.199 +fun print_setup ctxt =
   4.200 +  let
   4.201 +    fun string_of_bool b = if b then "true" else "false"
   4.202 +
   4.203 +    val (names, sel) = Solvers.get (Context.Proof ctxt) |> apfst Symtab.keys
   4.204 +    val ns = if null names then ["(none)"] else sort_strings names
   4.205 +    val n = the_default "(none)" sel
   4.206 +    val opts = solver_options_of ctxt
   4.207 +    
   4.208 +    val t = string_of_real (Config.get ctxt timeout)
   4.209 +
   4.210 +    val certs_filename =
   4.211 +      (case get_certificates_path ctxt of
   4.212 +        SOME path => Path.implode path
   4.213 +      | NONE => "(disabled)")
   4.214 +  in
   4.215 +    Pretty.writeln (Pretty.big_list "SMT setup:" [
   4.216 +      Pretty.str ("Current SMT solver: " ^ n),
   4.217 +      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
   4.218 +      Pretty.str_list "Available SMT solvers: "  "" ns,
   4.219 +      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
   4.220 +      Pretty.str ("With proofs: " ^
   4.221 +        string_of_bool (not (Config.get ctxt oracle))),
   4.222 +      Pretty.str ("Certificates cache: " ^ certs_filename),
   4.223 +      Pretty.str ("Fixed certificates: " ^
   4.224 +        string_of_bool (Config.get ctxt fixed))])
   4.225 +  end
   4.226 +
   4.227 +val _ =
   4.228 +  Outer_Syntax.improper_command "smt_status"
   4.229 +    ("show the available SMT solvers, the currently selected SMT solver, " ^
   4.230 +      "and the values of SMT configuration options")
   4.231 +    Keyword.diag
   4.232 +    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
   4.233 +      print_setup (Toplevel.context_of state))))
   4.234 +
   4.235 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/SMT/smt_failure.ML	Mon Nov 08 12:13:44 2010 +0100
     5.3 @@ -0,0 +1,41 @@
     5.4 +(*  Title:      HOL/Tools/SMT/smt_failure.ML
     5.5 +    Author:     Sascha Boehme, TU Muenchen
     5.6 +
     5.7 +Failures and exception of SMT.
     5.8 +*)
     5.9 +
    5.10 +signature SMT_FAILURE =
    5.11 +sig
    5.12 +  datatype failure =
    5.13 +    Counterexample of bool * term list |
    5.14 +    Time_Out |
    5.15 +    Out_Of_Memory |
    5.16 +    Other_Failure of string
    5.17 +  val string_of_failure: Proof.context -> failure -> string
    5.18 +  exception SMT of failure
    5.19 +end
    5.20 +
    5.21 +structure SMT_Failure: SMT_FAILURE =
    5.22 +struct
    5.23 +
    5.24 +datatype failure =
    5.25 +  Counterexample of bool * term list |
    5.26 +  Time_Out |
    5.27 +  Out_Of_Memory |
    5.28 +  Other_Failure of string
    5.29 +
    5.30 +fun string_of_failure ctxt (Counterexample (real, ex)) =
    5.31 +      let
    5.32 +        val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
    5.33 +      in
    5.34 +        if null ex then msg
    5.35 +        else Pretty.string_of (Pretty.big_list (msg ^ ":")
    5.36 +          (map (Syntax.pretty_term ctxt) ex))
    5.37 +      end
    5.38 +  | string_of_failure _ Time_Out = "Timed out"
    5.39 +  | string_of_failure _ Out_Of_Memory = "Ran out of memory"
    5.40 +  | string_of_failure _ (Other_Failure msg) = msg
    5.41 +
    5.42 +exception SMT of failure
    5.43 +
    5.44 +end
     6.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Nov 08 11:49:28 2010 +0100
     6.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Nov 08 12:13:44 2010 +0100
     6.3 @@ -92,16 +92,19 @@
     6.4     computation uses only the constants occurring with schematic type
     6.5     variables in the propositions. To ease comparisons, such sets of
     6.6     costants are always kept in their initial order. *)
     6.7 -fun incremental_monomorph thy limit all_grounds new_grounds irules =
     6.8 +fun incremental_monomorph ctxt limit all_grounds new_grounds irules =
     6.9    let
    6.10 +    val thy = ProofContext.theory_of ctxt
    6.11      val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
    6.12      val spec = specialize thy all_grounds' new_grounds
    6.13      val (irs, new_grounds') = fold_map spec irules Symtab.empty
    6.14    in
    6.15      if Symtab.is_empty new_grounds' then irs
    6.16      else if limit > 0
    6.17 -    then incremental_monomorph thy (limit-1) all_grounds' new_grounds' irs
    6.18 -    else (warning "SMT: monomorphization limit reached"; irs)
    6.19 +    then incremental_monomorph ctxt (limit-1) all_grounds' new_grounds' irs
    6.20 +    else
    6.21 +     (SMT_Config.verbose_msg ctxt (K "Warning: Monomorphization limit reached")
    6.22 +      (); irs)
    6.23    end
    6.24  
    6.25  
    6.26 @@ -175,7 +178,7 @@
    6.27        in
    6.28          polys
    6.29          |> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)]))
    6.30 -        |> incremental_monomorph thy limit Symtab.empty grounds
    6.31 +        |> incremental_monomorph ctxt' limit Symtab.empty grounds
    6.32          |> map (apsnd (filter_most_specific thy))
    6.33          |> flat o map2 (instantiate thy) Tenvs
    6.34          |> append monos
    6.35 @@ -183,9 +186,6 @@
    6.36        end
    6.37  
    6.38  
    6.39 -val monomorph_limit = 10
    6.40 -
    6.41 -
    6.42  (* Instantiate all polymorphic constants (i.e., constants occurring
    6.43     both with ground types and type variables) with all (necessary)
    6.44     ground types; thereby create copies of theorems containing those
    6.45 @@ -199,6 +199,6 @@
    6.46    irules
    6.47    |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
    6.48    |>> incr_indexes
    6.49 -  |-> mono_all ctxt monomorph_limit
    6.50 +  |-> mono_all ctxt (Config.get ctxt SMT_Config.monomorph_limit)
    6.51  
    6.52  end
     7.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 08 11:49:28 2010 +0100
     7.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 08 12:13:44 2010 +0100
     7.3 @@ -19,8 +19,7 @@
     7.4  sig
     7.5    type extra_norm = bool -> (int * thm) list -> Proof.context ->
     7.6      (int * thm) list * Proof.context
     7.7 -  val normalize: (Proof.context -> (thm -> string) -> thm -> unit) -> bool ->
     7.8 -    extra_norm -> bool -> (int * thm) list -> Proof.context ->
     7.9 +  val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
    7.10      (int * thm) list * Proof.context
    7.11    val atomize_conv: Proof.context -> conv
    7.12    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
    7.13 @@ -247,7 +246,7 @@
    7.14              then eta_args_conv norm_conv
    7.15                (length (Term.binder_types T) - length ts)
    7.16              else args_conv o norm_conv
    7.17 -        | (_, ts) => args_conv o norm_conv)) ctxt ct
    7.18 +        | _ => args_conv o norm_conv)) ctxt ct
    7.19  
    7.20    fun is_normed ctxt t =
    7.21      (case t of
    7.22 @@ -516,15 +515,15 @@
    7.23  
    7.24  fun with_context f irules ctxt = (f ctxt irules, ctxt)
    7.25  
    7.26 -fun normalize trace keep_assms extra_norm with_datatypes irules ctxt =
    7.27 +fun normalize extra_norm with_datatypes irules ctxt =
    7.28    let
    7.29      fun norm f ctxt' (i, thm) =
    7.30 -      if keep_assms then SOME (i, f ctxt' thm)
    7.31 -      else
    7.32 +      if Config.get ctxt' SMT_Config.drop_bad_facts then
    7.33          (case try (f ctxt') thm of
    7.34            SOME thm' => SOME (i, thm')
    7.35 -        | NONE => (trace ctxt' (prefix ("SMT warning: " ^
    7.36 +        | NONE => (SMT_Config.verbose_msg ctxt' (prefix ("Warning: " ^
    7.37              "dropping assumption: ") o Display.string_of_thm ctxt') thm; NONE))
    7.38 +      else SOME (i, f ctxt' thm)
    7.39    in
    7.40      irules
    7.41      |> trivial_distinct ctxt
     8.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Nov 08 11:49:28 2010 +0100
     8.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Nov 08 12:13:44 2010 +0100
     8.3 @@ -16,9 +16,9 @@
     8.4    if String.isPrefix unsat line then SMT_Solver.Unsat
     8.5    else if String.isPrefix sat line then SMT_Solver.Sat
     8.6    else if String.isPrefix unknown line then SMT_Solver.Unknown
     8.7 -  else raise SMT_Solver.SMT (SMT_Solver.Other_Failure ("Solver " ^
     8.8 +  else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
     8.9      quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
    8.10 -    "configuration option " ^ quote SMT_Solver.traceN ^ " and " ^
    8.11 +    "configuration option " ^ quote SMT_Config.traceN ^ " and " ^
    8.12      " see the trace for details."))
    8.13  
    8.14  fun on_first_line test_outcome solver_name lines =
    8.15 @@ -60,14 +60,14 @@
    8.16  
    8.17  fun z3_options ctxt =
    8.18    ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
    8.19 -  |> not (Config.get ctxt SMT_Solver.oracle) ?
    8.20 +  |> not (Config.get ctxt SMT_Config.oracle) ?
    8.21         append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
    8.22  
    8.23  fun z3_on_last_line solver_name lines =
    8.24    let
    8.25      fun junk l =
    8.26        if String.isPrefix "WARNING: Out of allocated virtual memory" l
    8.27 -      then raise SMT_Solver.SMT SMT_Solver.Out_Of_Memory
    8.28 +      then raise SMT_Failure.SMT SMT_Failure.Out_Of_Memory
    8.29        else
    8.30          String.isPrefix "WARNING" l orelse
    8.31          String.isPrefix "ERROR" l orelse
     9.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 08 11:49:28 2010 +0100
     9.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 08 12:13:44 2010 +0100
     9.3 @@ -6,14 +6,7 @@
     9.4  
     9.5  signature SMT_SOLVER =
     9.6  sig
     9.7 -  datatype failure =
     9.8 -    Counterexample of bool * term list |
     9.9 -    Time_Out |
    9.10 -    Out_Of_Memory |
    9.11 -    Other_Failure of string
    9.12 -  val string_of_failure: Proof.context -> string -> failure -> string
    9.13 -  exception SMT of failure
    9.14 -
    9.15 +  (*configuration*)
    9.16    type interface = {
    9.17      extra_norm: SMT_Normalize.extra_norm,
    9.18      translate: SMT_Translate.config }
    9.19 @@ -30,37 +23,16 @@
    9.20      reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    9.21        (int list * thm) * Proof.context) option }
    9.22  
    9.23 -  (*options*)
    9.24 -  val oracle: bool Config.T
    9.25 -  val filter_only: bool Config.T
    9.26 -  val datatypes: bool Config.T
    9.27 -  val keep_assms: bool Config.T
    9.28 -  val timeout: real Config.T
    9.29 -  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
    9.30 -  val traceN: string
    9.31 -  val trace: bool Config.T
    9.32 -  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
    9.33 -  val trace_used_facts: bool Config.T
    9.34 -
    9.35 -  (*certificates*)
    9.36 -  val fixed_certificates: bool Config.T
    9.37 -  val select_certificates: string -> Context.generic -> Context.generic
    9.38 -
    9.39 -  (*solvers*)
    9.40 +  (*registry*)
    9.41    type solver = bool option -> Proof.context -> (int * thm) list ->
    9.42      int list * thm
    9.43    val add_solver: solver_config -> theory -> theory
    9.44 -  val set_solver_options: string -> string -> Context.generic ->
    9.45 -    Context.generic
    9.46 -  val all_solver_names_of: Context.generic -> string list
    9.47 -  val solver_name_of: Context.generic -> string
    9.48 -  val select_solver: string -> Context.generic -> Context.generic
    9.49 -  val solver_of: Context.generic -> solver
    9.50 +  val solver_of: Proof.context -> solver
    9.51    val is_locally_installed: Proof.context -> bool
    9.52  
    9.53    (*filter*)
    9.54    val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
    9.55 -    {outcome: failure option, used_facts: 'a list,
    9.56 +    {outcome: SMT_Failure.failure option, used_facts: 'a list,
    9.57      run_time_in_msecs: int option}
    9.58  
    9.59    (*tactic*)
    9.60 @@ -69,31 +41,15 @@
    9.61  
    9.62    (*setup*)
    9.63    val setup: theory -> theory
    9.64 -  val print_setup: Context.generic -> unit
    9.65  end
    9.66  
    9.67  structure SMT_Solver: SMT_SOLVER =
    9.68  struct
    9.69  
    9.70 -datatype failure =
    9.71 -  Counterexample of bool * term list |
    9.72 -  Time_Out |
    9.73 -  Out_Of_Memory |
    9.74 -  Other_Failure of string
    9.75 +structure C = SMT_Config
    9.76  
    9.77 -fun string_of_failure ctxt _ (Counterexample (real, ex)) =
    9.78 -      let
    9.79 -        val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
    9.80 -      in
    9.81 -        if null ex then msg ^ "."
    9.82 -        else Pretty.string_of (Pretty.big_list (msg ^ ":")
    9.83 -          (map (Syntax.pretty_term ctxt) ex))
    9.84 -      end
    9.85 -  | string_of_failure _ name Time_Out = name ^ " timed out."
    9.86 -  | string_of_failure _ name Out_Of_Memory = name ^ " ran out of memory."
    9.87 -  | string_of_failure _ _ (Other_Failure msg) = msg
    9.88  
    9.89 -exception SMT of failure
    9.90 +(* configuration *)
    9.91  
    9.92  type interface = {
    9.93    extra_norm: SMT_Normalize.extra_norm,
    9.94 @@ -114,57 +70,6 @@
    9.95      (int list * thm) * Proof.context) option }
    9.96  
    9.97  
    9.98 -
    9.99 -(* SMT options *)
   9.100 -
   9.101 -val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true)
   9.102 -
   9.103 -val (filter_only, setup_filter_only) =
   9.104 -  Attrib.config_bool "smt_filter_only" (K false)
   9.105 -
   9.106 -val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
   9.107 -
   9.108 -val (keep_assms, setup_keep_assms) =
   9.109 -  Attrib.config_bool "smt_keep_assms" (K true)
   9.110 -
   9.111 -val (timeout, setup_timeout) = Attrib.config_real "smt_timeout" (K 30.0)
   9.112 -
   9.113 -fun with_timeout ctxt f x =
   9.114 -  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
   9.115 -  handle TimeLimit.TimeOut => raise SMT Time_Out
   9.116 -
   9.117 -val traceN = "smt_trace"
   9.118 -val (trace, setup_trace) = Attrib.config_bool traceN (K false)
   9.119 -
   9.120 -fun trace_msg ctxt f x =
   9.121 -  if Config.get ctxt trace then tracing (f x) else ()
   9.122 -
   9.123 -val (trace_used_facts, setup_trace_used_facts) =
   9.124 -  Attrib.config_bool "smt_trace_used_facts" (K false)
   9.125 -
   9.126 -
   9.127 -(* SMT certificates *)
   9.128 -
   9.129 -val (fixed_certificates, setup_fixed_certificates) =
   9.130 -  Attrib.config_bool "smt_fixed" (K false)
   9.131 -
   9.132 -structure Certificates = Generic_Data
   9.133 -(
   9.134 -  type T = Cache_IO.cache option
   9.135 -  val empty = NONE
   9.136 -  val extend = I
   9.137 -  fun merge (s, _) = s
   9.138 -)
   9.139 -
   9.140 -val get_certificates_path =
   9.141 -  Option.map (Cache_IO.cache_path_of) o Certificates.get
   9.142 -
   9.143 -fun select_certificates name = Certificates.put (
   9.144 -  if name = "" then NONE
   9.145 -  else SOME (Cache_IO.make (Path.explode name)))
   9.146 -
   9.147 -
   9.148 -
   9.149  (* interface to external solvers *)
   9.150  
   9.151  fun get_local_solver env_var =
   9.152 @@ -202,12 +107,12 @@
   9.153    [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
   9.154  
   9.155  fun run ctxt cmd args input =
   9.156 -  (case Certificates.get (Context.Proof ctxt) of
   9.157 +  (case C.certificates_of ctxt of
   9.158      NONE => Cache_IO.run (make_cmd (choose cmd) args) input
   9.159    | SOME certs =>
   9.160        (case Cache_IO.lookup certs input of
   9.161          (NONE, key) =>
   9.162 -          if Config.get ctxt fixed_certificates
   9.163 +          if Config.get ctxt C.fixed
   9.164            then error ("Bad certificates cache: missing certificate")
   9.165            else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
   9.166              input
   9.167 @@ -223,36 +128,37 @@
   9.168      fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
   9.169        (map Pretty.str ls))
   9.170  
   9.171 -    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input
   9.172 +    val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
   9.173  
   9.174 -    val (res, err) = with_timeout ctxt (run ctxt cmd args) input
   9.175 -    val _ = trace_msg ctxt (pretty "SMT solver:") err
   9.176 +    val (res, err) = C.with_timeout ctxt (run ctxt cmd args) input
   9.177 +    val _ = C.trace_msg ctxt (pretty "Solver:") err
   9.178  
   9.179      val ls = rev (snd (chop_while (equal "") (rev res)))
   9.180 -    val _ = trace_msg ctxt (pretty "SMT result:") ls
   9.181 +    val _ = C.trace_msg ctxt (pretty "Result:") ls
   9.182    in ls end
   9.183  
   9.184  end
   9.185  
   9.186 -fun trace_assms ctxt = trace_msg ctxt (Pretty.string_of o
   9.187 -  Pretty.big_list "SMT assertions:" o map (Display.pretty_thm ctxt o snd))
   9.188 +fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
   9.189 +  Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
   9.190  
   9.191  fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
   9.192    let
   9.193      fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
   9.194 -    fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
   9.195 -    fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
   9.196 +    fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
   9.197 +    fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
   9.198    in
   9.199 -    trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [
   9.200 -      Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)),
   9.201 -      Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) ()
   9.202 +    C.trace_msg ctxt (fn () =>
   9.203 +      Pretty.string_of (Pretty.big_list "Names:" [
   9.204 +        Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
   9.205 +        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
   9.206    end
   9.207  
   9.208 -fun invoke translate_config name cmd more_opts options irules ctxt =
   9.209 +fun invoke translate_config name cmd options irules ctxt =
   9.210    let
   9.211 -    val args = more_opts @ options ctxt
   9.212 +    val args = C.solver_options_of ctxt @ options ctxt
   9.213      val comments = ("solver: " ^ name) ::
   9.214 -      ("timeout: " ^ Time.toString (seconds (Config.get ctxt timeout))) ::
   9.215 +      ("timeout: " ^ Time.toString (seconds (Config.get ctxt C.timeout))) ::
   9.216        "arguments:" :: args
   9.217    in
   9.218      irules
   9.219 @@ -283,7 +189,7 @@
   9.220      val thms = filter (fn i => i >= 0) idxs
   9.221        |> map_filter (AList.lookup (op =) irules)
   9.222    in
   9.223 -    if Config.get ctxt trace_used_facts andalso length thms > 0
   9.224 +    if Config.get ctxt C.trace_used_facts andalso length thms > 0
   9.225      then
   9.226        tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
   9.227          (map (Display.pretty_thm ctxt) thms)))
   9.228 @@ -292,17 +198,15 @@
   9.229  
   9.230  fun gen_solver name info rm ctxt irules =
   9.231    let
   9.232 -    val {env_var, is_remote, options, more_options, interface, reconstruct} =
   9.233 -      info
   9.234 +    val {env_var, is_remote, options, interface, reconstruct} = info
   9.235      val {extra_norm, translate} = interface
   9.236      val (with_datatypes, translate') =
   9.237 -      set_has_datatypes (Config.get ctxt datatypes) translate
   9.238 +      set_has_datatypes (Config.get ctxt C.datatypes) translate
   9.239      val cmd = (rm, env_var, is_remote, name)
   9.240 -    val keep = Config.get ctxt keep_assms
   9.241    in
   9.242      (irules, ctxt)
   9.243 -    |-> SMT_Normalize.normalize trace_msg keep extra_norm with_datatypes
   9.244 -    |-> invoke translate' name cmd more_options options
   9.245 +    |-> SMT_Normalize.normalize extra_norm with_datatypes
   9.246 +    |-> invoke translate' name cmd options
   9.247      |-> reconstruct
   9.248      |-> (fn (idxs, thm) => fn ctxt' => thm
   9.249      |> singleton (ProofContext.export ctxt' ctxt)
   9.250 @@ -313,7 +217,7 @@
   9.251  
   9.252  
   9.253  
   9.254 -(* solver store *)
   9.255 +(* registry *)
   9.256  
   9.257  type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
   9.258  
   9.259 @@ -321,7 +225,6 @@
   9.260    env_var: string,
   9.261    is_remote: bool,
   9.262    options: Proof.context -> string list,
   9.263 -  more_options: string list,
   9.264    interface: interface,
   9.265    reconstruct: string list * SMT_Translate.recon -> Proof.context ->
   9.266      (int list * thm) * Proof.context }
   9.267 @@ -335,24 +238,18 @@
   9.268      handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
   9.269  )
   9.270  
   9.271 -val no_solver = "(none)"
   9.272 -
   9.273 -fun set_solver_options name opts = Solvers.map (Symtab.map_entry name (fn
   9.274 -  {env_var, is_remote, options, interface, reconstruct, ...} =>
   9.275 -  {env_var=env_var, is_remote=is_remote, options=options,
   9.276 -   more_options=String.tokens (Symbol.is_ascii_blank o str) opts,
   9.277 -   interface=interface, reconstruct=reconstruct}))
   9.278 -
   9.279  local
   9.280    fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt =
   9.281      (case outcome output of
   9.282        (Unsat, ls) =>
   9.283 -        if not (Config.get ctxt oracle) andalso is_some reconstruct
   9.284 +        if not (Config.get ctxt C.oracle) andalso is_some reconstruct
   9.285          then the reconstruct ctxt recon ls
   9.286          else (([], ocl ()), ctxt)
   9.287      | (result, ls) =>
   9.288          let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
   9.289 -        in raise SMT (Counterexample (result = Sat, ts)) end)
   9.290 +        in
   9.291 +          raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
   9.292 +        end)
   9.293  in
   9.294  
   9.295  fun add_solver cfg =
   9.296 @@ -363,59 +260,31 @@
   9.297      fun core_oracle () = @{cprop False}
   9.298  
   9.299      fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
   9.300 -      more_options=[], interface=interface,
   9.301 +      interface=interface,
   9.302        reconstruct=finish (outcome name) cex_parser reconstruct ocl }
   9.303    in
   9.304      Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
   9.305      Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
   9.306 -    Attrib.setup (Binding.name (name ^ "_options"))
   9.307 -      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   9.308 -        (Thm.declaration_attribute o K o set_solver_options name))
   9.309 -      ("Additional command line options for SMT solver " ^ quote name)
   9.310 +    Context.theory_map (C.add_solver name)
   9.311    end
   9.312  
   9.313  end
   9.314  
   9.315 -val all_solver_names_of = Symtab.keys o Solvers.get
   9.316 -val lookup_solver = Symtab.lookup o Solvers.get
   9.317 -
   9.318 -
   9.319 -
   9.320 -(* selected solver *)
   9.321 -
   9.322 -structure Selected_Solver = Generic_Data
   9.323 -(
   9.324 -  type T = string
   9.325 -  val empty = no_solver
   9.326 -  val extend = I
   9.327 -  fun merge (s, _) = s
   9.328 -)
   9.329 +fun name_and_solver_of ctxt =
   9.330 +  let val name = C.solver_of ctxt
   9.331 +  in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end
   9.332  
   9.333 -val solver_name_of = Selected_Solver.get
   9.334 -
   9.335 -fun select_solver name context =
   9.336 -  if is_none (lookup_solver context name)
   9.337 -  then error ("SMT solver not registered: " ^ quote name)
   9.338 -  else Selected_Solver.map (K name) context
   9.339 -
   9.340 -fun raw_solver_of context name =
   9.341 -  (case lookup_solver context name of
   9.342 -    NONE => error "No SMT solver selected"
   9.343 -  | SOME s => s)
   9.344 -
   9.345 -fun solver_of context =
   9.346 -  let val name = solver_name_of context
   9.347 -  in gen_solver name (raw_solver_of context name) end
   9.348 +fun solver_of ctxt =
   9.349 +  let val (name, raw_solver) = name_and_solver_of ctxt
   9.350 +  in gen_solver name raw_solver end
   9.351  
   9.352  fun is_locally_installed ctxt =
   9.353 -  let
   9.354 -    val name = solver_name_of (Context.Proof ctxt)
   9.355 -    val {env_var, ...} = raw_solver_of (Context.Proof ctxt) name
   9.356 +  let val (_, {env_var, ...}) = name_and_solver_of ctxt
   9.357    in is_some (get_local_solver env_var) end
   9.358  
   9.359  
   9.360  
   9.361 -(* SMT filter *)
   9.362 +(* filter *)
   9.363  
   9.364  val has_topsort = Term.exists_type (Term.exists_subtype (fn
   9.365      TFree (_, []) => true
   9.366 @@ -424,19 +293,20 @@
   9.367  
   9.368  fun smt_solver rm ctxt irules =
   9.369    (* without this test, we would run into problems when atomizing the rules: *)
   9.370 -  if exists (has_topsort o Thm.prop_of o snd) irules
   9.371 -  then raise SMT (Other_Failure "proof state contains the universal sort {}")
   9.372 -  else solver_of (Context.Proof ctxt) rm ctxt irules
   9.373 +  if exists (has_topsort o Thm.prop_of o snd) irules then
   9.374 +    raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
   9.375 +      "contains the universal sort {}"))
   9.376 +  else solver_of ctxt rm ctxt irules
   9.377  
   9.378  fun smt_filter run_remote time_limit st xrules i =
   9.379    let
   9.380      val {facts, goal, ...} = Proof.goal st
   9.381      val ctxt =
   9.382        Proof.context_of st
   9.383 -      |> Config.put timeout (Real.fromInt (Time.toSeconds time_limit))
   9.384 -      |> Config.put oracle false
   9.385 -      |> Config.put filter_only true
   9.386 -      |> Config.put keep_assms false
   9.387 +      |> Config.put C.oracle false
   9.388 +      |> Config.put C.timeout (Real.fromInt (Time.toSeconds time_limit))
   9.389 +      |> Config.put C.drop_bad_facts true
   9.390 +      |> Config.put C.filter_only_facts true
   9.391      val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
   9.392      val cprop =
   9.393        concl
   9.394 @@ -450,7 +320,8 @@
   9.395      |-> map_filter o try o nth
   9.396      |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
   9.397    end
   9.398 -  handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs=NONE}
   9.399 +  handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[],
   9.400 +    run_time_in_msecs=NONE}
   9.401    (* FIXME: measure runtime *)
   9.402  
   9.403  
   9.404 @@ -460,14 +331,17 @@
   9.405  fun smt_tac' pass_exns ctxt rules =
   9.406    CONVERSION (SMT_Normalize.atomize_conv ctxt)
   9.407    THEN' Tactic.rtac @{thm ccontr}
   9.408 -  THEN' SUBPROOF (fn {context=cx, prems, ...} =>
   9.409 +  THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
   9.410      let
   9.411 -      fun solve () = snd (smt_solver NONE cx (map (pair ~1) (rules @ prems)))
   9.412 -      val name = solver_name_of (Context.Proof cx)
   9.413 -      val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx name)
   9.414 +      fun solve irules = snd (smt_solver NONE ctxt' irules)
   9.415 +      val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
   9.416 +      val str_of = SMT_Failure.string_of_failure ctxt'
   9.417 +      fun safe_solve irules =
   9.418 +        if pass_exns then SOME (solve irules)
   9.419 +        else (SOME (solve irules) handle SMT_Failure.SMT fail =>
   9.420 +          (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
   9.421      in
   9.422 -      (if pass_exns then SOME (solve ())
   9.423 -       else (SOME (solve ()) handle SMT fail => (trace fail; NONE)))
   9.424 +      safe_solve (map (pair ~1) (rules @ prems))
   9.425        |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
   9.426      end) ctxt
   9.427  
   9.428 @@ -483,60 +357,7 @@
   9.429  (* setup *)
   9.430  
   9.431  val setup =
   9.432 -  Attrib.setup @{binding smt_solver}
   9.433 -    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   9.434 -      (Thm.declaration_attribute o K o select_solver))
   9.435 -    "SMT solver configuration" #>
   9.436 -  setup_oracle #>
   9.437 -  setup_filter_only #>
   9.438 -  setup_datatypes #>
   9.439 -  setup_keep_assms #>
   9.440 -  setup_timeout #>
   9.441 -  setup_trace #>
   9.442 -  setup_trace_used_facts #>
   9.443 -  setup_fixed_certificates #>
   9.444 -  Attrib.setup @{binding smt_certificates}
   9.445 -    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   9.446 -      (Thm.declaration_attribute o K o select_certificates))
   9.447 -    "SMT certificates" #>
   9.448    Method.setup @{binding smt} smt_method
   9.449      "Applies an SMT solver to the current goal."
   9.450  
   9.451 -
   9.452 -fun print_setup context =
   9.453 -  let
   9.454 -    val t = Time.toString (seconds (Config.get_generic context timeout))
   9.455 -    val names = sort_strings (all_solver_names_of context)
   9.456 -    val ns = if null names then [no_solver] else names
   9.457 -    val n = solver_name_of context
   9.458 -    val opts =
   9.459 -      (case Symtab.lookup (Solvers.get context) n of
   9.460 -        NONE => []
   9.461 -      | SOME {more_options, options, ...} =>
   9.462 -          more_options @ options (Context.proof_of context))
   9.463 -    val certs_filename =
   9.464 -      (case get_certificates_path context of
   9.465 -        SOME path => Path.implode path
   9.466 -      | NONE => "(disabled)")
   9.467 -    val fixed = if Config.get_generic context fixed_certificates then "true"
   9.468 -      else "false"
   9.469 -  in
   9.470 -    Pretty.writeln (Pretty.big_list "SMT setup:" [
   9.471 -      Pretty.str ("Current SMT solver: " ^ n),
   9.472 -      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
   9.473 -      Pretty.str_list "Available SMT solvers: "  "" ns,
   9.474 -      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
   9.475 -      Pretty.str ("With proofs: " ^
   9.476 -        (if Config.get_generic context oracle then "false" else "true")),
   9.477 -      Pretty.str ("Certificates cache: " ^ certs_filename),
   9.478 -      Pretty.str ("Fixed certificates: " ^ fixed)])
   9.479 -  end
   9.480 -
   9.481 -val _ =
   9.482 -  Outer_Syntax.improper_command "smt_status"
   9.483 -    "show the available SMT solvers and the currently selected solver"
   9.484 -    Keyword.diag
   9.485 -    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
   9.486 -      print_setup (Context.Proof (Toplevel.context_of state)))))
   9.487 -
   9.488  end
    10.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 08 11:49:28 2010 +0100
    10.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 08 12:13:44 2010 +0100
    10.3 @@ -240,7 +240,7 @@
    10.4  
    10.5  (* core parser *)
    10.6  
    10.7 -fun parse_exn line_no msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
    10.8 +fun parse_exn line_no msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
    10.9    ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg))
   10.10  
   10.11  fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg
    11.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 08 11:49:28 2010 +0100
    11.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 08 12:13:44 2010 +0100
    11.3 @@ -19,7 +19,7 @@
    11.4  structure T = Z3_Proof_Tools
    11.5  structure L = Z3_Proof_Literals
    11.6  
    11.7 -fun z3_exn msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
    11.8 +fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
    11.9    ("Z3 proof reconstruction: " ^ msg))
   11.10  
   11.11  
   11.12 @@ -66,11 +66,11 @@
   11.13  (** proof tools **)
   11.14  
   11.15  fun named ctxt name prover ct =
   11.16 -  let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
   11.17 +  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
   11.18    in prover ct end
   11.19  
   11.20  fun NAMED ctxt name tac i st =
   11.21 -  let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
   11.22 +  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
   11.23    in tac i st end
   11.24  
   11.25  fun pretty_goal ctxt thms t =
   11.26 @@ -90,7 +90,7 @@
   11.27      fun apply [] ct = error (try_apply_err ct)
   11.28        | apply (prover :: provers) ct =
   11.29            (case try prover ct of
   11.30 -            SOME thm => (SMT_Solver.trace_msg ctxt I "Z3: succeeded"; thm)
   11.31 +            SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
   11.32            | NONE => apply provers ct)
   11.33  
   11.34    in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end
   11.35 @@ -732,9 +732,9 @@
   11.36  in
   11.37  fun trace_rule idx prove r ps ct (cxp as (ctxt, ptab)) =
   11.38    let
   11.39 -    val _ = SMT_Solver.trace_msg ctxt (header idx r o count_rules) ptab
   11.40 +    val _ = SMT_Config.trace_msg ctxt (header idx r o count_rules) ptab
   11.41      val result as (p, (ctxt', _)) = prove r ps ct cxp
   11.42 -    val _ = if not (Config.get ctxt' SMT_Solver.trace) then ()
   11.43 +    val _ = if not (Config.get ctxt' SMT_Config.trace) then ()
   11.44        else check ctxt' idx r ps ct p
   11.45    in result end
   11.46  end
   11.47 @@ -844,7 +844,7 @@
   11.48      val (idx, (ptab, vars, cx)) = P.parse ctxt typs terms output
   11.49      val assms' = prepare_assms cx unfolds assms
   11.50    in
   11.51 -    if Config.get cx SMT_Solver.filter_only
   11.52 +    if Config.get cx SMT_Config.filter_only_facts
   11.53      then ((filter_assms cx assms' ptab idx [], @{thm TrueI}), cx)
   11.54      else apfst (pair []) (prove cx assms' vars idx ptab)
   11.55    end
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 11:49:28 2010 +0100
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 12:13:44 2010 +0100
    12.3 @@ -409,9 +409,9 @@
    12.4       run_time_in_msecs = msecs}
    12.5    end
    12.6  
    12.7 -fun failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
    12.8 -  | failure_from_smt_failure SMT_Solver.Time_Out = TimedOut
    12.9 -  | failure_from_smt_failure SMT_Solver.Out_Of_Memory = OutOfResources
   12.10 +fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
   12.11 +  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   12.12 +  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   12.13    | failure_from_smt_failure _ = UnknownError
   12.14  
   12.15  val smt_max_iter = 5
   12.16 @@ -473,10 +473,10 @@
   12.17                           (apply_on_subgoal subgoal subgoal_count ^
   12.18                            command_call smtN (map fst used_facts)) ^
   12.19          minimize_line minimize_command (map fst used_facts)
   12.20 -      | SOME SMT_Solver.Time_Out => "Timed out."
   12.21 -      | SOME (SMT_Solver.Counterexample _) => "The SMT problem is unprovable."
   12.22 +      | SOME SMT_Failure.Time_Out => "Timed out."
   12.23 +      | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
   12.24        | SOME failure =>
   12.25 -        SMT_Solver.string_of_failure ctxt "The SMT solver" failure
   12.26 +        SMT_Failure.string_of_failure ctxt failure
   12.27      val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
   12.28    in
   12.29      {outcome = outcome, used_facts = used_facts,