joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface

--- a/NEWS	Tue Oct 26 11:39:26 2010 +0200
+++ b/NEWS	Tue Oct 26 11:45:12 2010 +0200
@@ -306,6 +306,15 @@
     sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
     INCOMPATIBILITY.
 
+* Changed SMT configuration options:
+  - Renamed:
+    z3_proofs ~> smt_oracle (with swapped semantics)
+    z3_trace_assms ~> smt_trace_used_facts
+    INCOMPATIBILITY.
+  - Added:
+    cvc3_options
+    yices_options
+    smt_datatypes
 
 *** FOL ***
 

--- a/src/HOL/IsaMakefile	Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 26 11:45:12 2010 +0200
@@ -336,20 +336,18 @@
   Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
   Tools/Sledgehammer/sledgehammer_atp_translate.ML \
   Tools/Sledgehammer/sledgehammer_util.ML \
-  Tools/SMT/cvc3_solver.ML \
   Tools/SMT/smtlib_interface.ML \
   Tools/SMT/smt_monomorph.ML \
   Tools/SMT/smt_normalize.ML \
+  Tools/SMT/smt_setup_solvers.ML \
   Tools/SMT/smt_solver.ML \
   Tools/SMT/smt_translate.ML \
-  Tools/SMT/yices_solver.ML \
   Tools/SMT/z3_interface.ML \
   Tools/SMT/z3_model.ML \
   Tools/SMT/z3_proof_literals.ML \
   Tools/SMT/z3_proof_parser.ML \
   Tools/SMT/z3_proof_reconstruction.ML \
   Tools/SMT/z3_proof_tools.ML \
-  Tools/SMT/z3_solver.ML \
   Tools/string_code.ML \
   Tools/string_syntax.ML \
   Tools/transfer.ML \

--- a/src/HOL/SMT.thy	Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/SMT.thy	Tue Oct 26 11:45:12 2010 +0200
@@ -19,9 +19,7 @@
   ("Tools/SMT/z3_proof_reconstruction.ML")
   ("Tools/SMT/z3_model.ML")
   ("Tools/SMT/z3_interface.ML")
-  ("Tools/SMT/z3_solver.ML")
-  ("Tools/SMT/cvc3_solver.ML")
-  ("Tools/SMT/yices_solver.ML")
+  ("Tools/SMT/smt_setup_solvers.ML")
 begin
 
 
@@ -124,16 +122,12 @@
 use "Tools/SMT/z3_proof_literals.ML"
 use "Tools/SMT/z3_proof_reconstruction.ML"
 use "Tools/SMT/z3_model.ML"
-use "Tools/SMT/z3_solver.ML"
-use "Tools/SMT/cvc3_solver.ML"
-use "Tools/SMT/yices_solver.ML"
+use "Tools/SMT/smt_setup_solvers.ML"
 
 setup {*
   SMT_Solver.setup #>
   Z3_Proof_Reconstruction.setup #>
-  Z3_Solver.setup #>
-  CVC3_Solver.setup #>
-  Yices_Solver.setup
+  SMT_Setup_Solvers.setup
 *}
 
 
@@ -171,6 +165,31 @@
 
 declare [[ smt_timeout = 20 ]]
 
+text {*
+In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
+solvers are fully trusted without additional checks.  The following
+option can cause the SMT solver to run in proof-producing mode, giving
+a checkable certificate.  This is currently only implemented for Z3.
+*}
+
+declare [[ smt_oracle = false ]]
+
+text {*
+Each SMT solver provides several commandline options to tweak its
+behaviour.  They can be passed to the solver by setting the following
+options.
+*}
+
+declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]
+
+text {*
+Enable the following option to use built-in support for datatypes and
+records.  Currently, this is only implemented for Z3 running in oracle
+mode.
+*}
+
+declare [[ smt_datatypes = false ]]
+
 
 
 subsection {* Certificates *}
@@ -213,41 +232,14 @@
 
 declare [[ smt_trace = false ]]
 
-
-
-subsection {* Z3-specific options *}
-
 text {*
-Z3 is the only SMT solver whose proofs are checked (or reconstructed)
-in Isabelle (all other solvers are implemented as oracles).  Enabling
-or disabling proof reconstruction for Z3 is controlled by the option
-@{text z3_proofs}. 
+From the set of assumptions given to the SMT solver, those assumptions
+used in the proof are traced when the following option is set to
+@{term true}.  This only works for Z3 when it runs in non-oracle mode
+(see options @{text smt_solver} and @{text smt_oracle} above).
 *}
 
-declare [[ z3_proofs = true ]]
-
-text {*
-From the set of assumptions given to Z3, those assumptions used in
-the proof are traced when the option @{text z3_trace_assms} is set to
-@{term true}.
-*}
-
-declare [[ z3_trace_assms = false ]]
-
-text {*
-Z3 provides several commandline options to tweak its behaviour.  They
-can be configured by writing them literally as value for the option
-@{text z3_options}.
-*}
-
-declare [[ z3_options = "" ]]
-
-text {*
-The following configuration option may be used to enable mapping of
-HOL datatypes and records to native datatypes provided by Z3.
-*}
-
-declare [[ z3_datatypes = false ]]
+declare [[ smt_trace_used_facts = false ]]
 
 
 

--- a/src/HOL/Tools/SMT/cvc3_solver.ML	Tue Oct 26 11:39:26 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*  Title:      HOL/Tools/SMT/cvc3_solver.ML
-    Author:     Sascha Boehme, TU Muenchen
-
-Interface of the SMT solver CVC3.
-*)
-
-signature CVC3_SOLVER =
-sig
-  val setup: theory -> theory
-end
-
-structure CVC3_Solver: CVC3_SOLVER =
-struct
-
-val solver_name = "cvc3"
-val env_var = "CVC3_SOLVER"
-
-val options = ["-lang", "smtlib", "-output-lang", "presentation"]
-
-val is_sat = String.isPrefix "Satisfiable."
-val is_unsat = String.isPrefix "Unsatisfiable."
-val is_unknown = String.isPrefix "Unknown."
-
-fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])
-
-fun core_oracle (output, _) =
-  let
-    val empty_line = (fn "" => true | _ => false)
-    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
-    val (l, _) = split_first (snd (chop_while empty_line output))
-  in
-    if is_unsat l then @{cprop False}
-    else if is_sat l then raise_cex true
-    else if is_unknown l then raise_cex false
-    else raise SMT_Solver.SMT (solver_name ^ " failed")
-  end
-
-fun solver oracle _ = {
-  command = {env_var=env_var, remote_name=SOME solver_name},
-  arguments = options,
-  interface = SMTLIB_Interface.interface,
-  reconstruct = pair o pair [] o oracle }
-
-val setup =
-  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
-  Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle)))
-
-end

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:45:12 2010 +0200
@@ -17,7 +17,7 @@
 
 signature SMT_NORMALIZE =
 sig
-  type extra_norm = (int * thm) list -> Proof.context ->
+  type extra_norm = bool -> (int * thm) list -> Proof.context ->
     (int * thm) list * Proof.context
   val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
     (int * thm) list * Proof.context
@@ -480,7 +480,7 @@
 
 (* combined normalization *)
 
-type extra_norm = (int * thm) list -> Proof.context ->
+type extra_norm = bool -> (int * thm) list -> Proof.context ->
   (int * thm) list * Proof.context
 
 fun with_context f irules ctxt = (f ctxt irules, ctxt)
@@ -492,7 +492,7 @@
   |> normalize_numerals ctxt
   |> nat_as_int ctxt
   |> rpair ctxt
-  |-> extra_norm
+  |-> extra_norm with_datatypes
   |-> with_context (fn cx => map (apsnd (normalize_rule cx)))
   |-> SMT_Monomorph.monomorph
   |-> lift_lambdas

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Oct 26 11:45:12 2010 +0200
@@ -0,0 +1,93 @@
+(*  Title:      HOL/Tools/SMT/smt_setup_solvers.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Setup SMT solvers.
+*)
+
+signature SMT_SETUP_SOLVERS =
+sig
+  val setup: theory -> theory
+end
+
+structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS =
+struct
+
+fun outcome_of unsat sat unknown solver_name line =
+  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 " ^
+    quote solver_name ^ " failed, " ^ "see trace for details."))
+
+fun on_first_line test_outcome solver_name lines =
+  let
+    val empty_line = (fn "" => true | _ => false)
+    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
+    val (l, ls) = split_first (snd (chop_while empty_line lines))
+  in (test_outcome solver_name l, ls) end
+
+
+(* CVC3 *)
+
+val cvc3 = {
+  name = "cvc3",
+  env_var = "CVC3_SOLVER",
+  is_remote = true,
+  options = K ["-lang", "smtlib", "-output-lang", "presentation"],
+  interface = SMTLIB_Interface.interface,
+  outcome =
+    on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+  cex_parser = NONE,
+  reconstruct = NONE }
+
+
+(* Yices *)
+
+val yices = {
+  name = "yices",
+  env_var = "YICES_SOLVER",
+  is_remote = false,
+  options = K ["--smtlib"],
+  interface = SMTLIB_Interface.interface,
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+  cex_parser = NONE,
+  reconstruct = NONE }
+
+
+(* Z3 *)
+
+fun z3_options ctxt =
+  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
+  |> not (Config.get ctxt SMT_Solver.oracle) ?
+       append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
+
+fun z3_on_last_line solver_name lines =
+  let
+    fun junk l =
+      String.isPrefix "WARNING" l orelse
+      String.isPrefix "ERROR" l orelse
+      forall Symbol.is_ascii_blank (Symbol.explode l)
+  in
+    the_default ("", []) (try (swap o split_last) (filter_out junk lines))
+    |>> outcome_of "unsat" "sat" "unknown" solver_name
+  end
+
+val z3 = {
+  name = "z3",
+  env_var = "Z3_SOLVER",
+  is_remote = true,
+  options = z3_options,
+  interface = Z3_Interface.interface,
+  outcome = z3_on_last_line,
+  cex_parser = SOME Z3_Model.parse_counterex,
+  reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
+
+
+(* overall setup *)
+
+val setup =
+  SMT_Solver.add_solver cvc3 #>
+  SMT_Solver.add_solver yices #>
+  SMT_Solver.add_solver z3
+
+end

--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:45:12 2010 +0200
@@ -6,24 +6,37 @@
 
 signature SMT_SOLVER =
 sig
-  exception SMT of string
-  exception SMT_COUNTEREXAMPLE of bool * term list
+  datatype failure =
+    Counterexample of bool * term list |
+    Time_Out |
+    Other_Failure of string
+  val string_of_failure: Proof.context -> failure -> string
+  exception SMT of failure
 
   type interface = {
     extra_norm: SMT_Normalize.extra_norm,
     translate: SMT_Translate.config }
+  datatype outcome = Unsat | Sat | Unknown
   type solver_config = {
-    command: {env_var: string, remote_name: string option},
-    arguments: string list,
+    name: string,
+    env_var: string,
+    is_remote: bool,
+    options: Proof.context -> string list,
     interface: interface,
-    reconstruct: (string list * SMT_Translate.recon) -> Proof.context ->
-      (int list * thm) * Proof.context }
+    outcome: string -> string list -> outcome * string list,
+    cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
+      term list) option,
+    reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
+      (int list * thm) * Proof.context) option }
 
   (*options*)
+  val oracle: bool Config.T
+  val datatypes: bool Config.T
   val timeout: int Config.T
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
   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
@@ -31,19 +44,17 @@
 
   (*solvers*)
   type solver = Proof.context -> (int * thm) list -> int list * thm
-  type solver_info = Context.generic -> Pretty.T list
-  val add_solver: string * (Proof.context -> solver_config) ->
-    Context.generic -> Context.generic
+  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 add_solver_info: string * solver_info -> Context.generic ->
-    Context.generic
   val solver_name_of: Context.generic -> string
   val select_solver: string -> Context.generic -> Context.generic
   val solver_of: Context.generic -> solver
 
-  (*solver*)
-  val smt_solver: Proof.context -> ('a * thm) list -> 'a list * thm
-  val smt_filter: Proof.context -> ('a * thm) list -> 'a list * string
+  (*filter*)
+  val smt_filter: Proof.state -> int -> ('a * thm) list ->
+    'a list * failure option
 
   (*tactic*)
   val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
@@ -57,36 +68,64 @@
 structure SMT_Solver: SMT_SOLVER =
 struct
 
-exception SMT of string
-exception SMT_COUNTEREXAMPLE of bool * term list
+datatype failure =
+  Counterexample of bool * term list |
+  Time_Out |
+  Other_Failure of string
 
+fun string_of_failure ctxt (Counterexample (real, ex)) =
+      let
+        val msg = if real then "Counterexample found"
+          else "Potential counterexample 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 = "Time out."
+  | string_of_failure _ (Other_Failure msg) = msg
+
+exception SMT of failure
 
 type interface = {
   extra_norm: SMT_Normalize.extra_norm,
   translate: SMT_Translate.config }
 
+datatype outcome = Unsat | Sat | Unknown
+
 type solver_config = {
-  command: {env_var: string, remote_name: string option},
-  arguments: string list,
+  name: string,
+  env_var: string,
+  is_remote: bool,
+  options: Proof.context -> string list,
   interface: interface,
-  reconstruct: (string list * SMT_Translate.recon) -> Proof.context ->
-    (int list * thm) * Proof.context }
+  outcome: string -> string list -> outcome * string list,
+  cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
+    term list) option,
+  reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
+    (int list * thm) * Proof.context) option }
 
 
 
 (* SMT options *)
 
+val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true)
+
+val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
+
 val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
 
 fun with_timeout ctxt f x =
   TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
-  handle TimeLimit.TimeOut => raise SMT "timeout"
+  handle TimeLimit.TimeOut => raise SMT Time_Out
 
 val (trace, setup_trace) = Attrib.config_bool "smt_trace" (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 *)
@@ -115,21 +154,20 @@
 
 local
 
-fun choose {env_var, remote_name} =
+fun choose (env_var, is_remote, remote_name) =
   let
     val local_solver = getenv env_var
-    val remote_solver = the_default "" remote_name
     val remote_url = getenv "REMOTE_SMT_URL"
   in
     if local_solver <> ""
     then 
      (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ...");
       [local_solver])
-    else if remote_solver <> ""
+    else if is_remote
     then
-     (tracing ("Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
+     (tracing ("Invoking remote SMT solver " ^ quote remote_name ^ " at " ^
         quote remote_url ^ " ...");
-      [getenv "REMOTE_SMT", remote_solver])
+      [getenv "REMOTE_SMT", remote_name])
     else error ("Undefined Isabelle environment variable: " ^ quote env_var)
   end
 
@@ -181,30 +219,46 @@
       Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) ()
   end
 
-fun invoke translate_config comments command arguments irules ctxt =
-  irules
-  |> SMT_Translate.translate translate_config ctxt comments
-  ||> tap (trace_recon_data ctxt)
-  |>> run_solver ctxt command arguments
-  |> rpair ctxt
+fun invoke translate_config name cmd more_opts options irules ctxt =
+  let
+    val args = more_opts @ options ctxt
+    val comments = ("solver: " ^ name) ::
+      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
+      "arguments:" :: args
+  in
+    irules
+    |> SMT_Translate.translate translate_config ctxt comments
+    ||> tap (trace_recon_data ctxt)
+    |>> run_solver ctxt cmd args
+    |> rpair ctxt
+  end
 
 fun discharge_definitions thm =
   if Thm.nprems_of thm = 0 then thm
   else discharge_definitions (@{thm reflexive} RS thm)
 
-fun gen_solver name solver ctxt prems =
+fun set_has_datatypes with_datatypes translate =
   let
-    val {command, arguments, interface, reconstruct} = solver ctxt
-    val comments = ("solver: " ^ name) ::
-      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
-      "arguments:" :: arguments
+    val {prefixes, header, strict, builtins, serialize} = translate
+    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
+    val with_datatypes' = has_datatypes andalso with_datatypes
+    val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num,
+      builtin_fun=builtin_fun, has_datatypes=with_datatypes}
+    val translate' = {prefixes=prefixes, header=header, strict=strict,
+      builtins=builtins', serialize=serialize}
+  in (with_datatypes', translate') end
+
+fun gen_solver name info ctxt irules =
+  let
+    val {env_var, is_remote, options, more_options, interface, reconstruct} =
+      info
     val {extra_norm, translate} = interface
-    val {builtins, ...} = translate
-    val {has_datatypes, ...} = builtins
+    val (with_datatypes, translate') =
+      set_has_datatypes (Config.get ctxt datatypes) translate
   in
-    (prems, ctxt)
-    |-> SMT_Normalize.normalize extra_norm has_datatypes
-    |-> invoke translate comments command arguments
+    (irules, ctxt)
+    |-> SMT_Normalize.normalize extra_norm with_datatypes
+    |-> invoke translate' name (env_var, is_remote, name) more_options options
     |-> reconstruct
     |-> (fn (idxs, thm) => fn ctxt' => thm
     |> singleton (ProofContext.export ctxt' ctxt)
@@ -217,11 +271,19 @@
 (* solver store *)
 
 type solver = Proof.context -> (int * thm) list -> int list * thm
-type solver_info = Context.generic -> Pretty.T list
+
+type solver_info = {
+  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 }
 
 structure Solvers = Generic_Data
 (
-  type T = ((Proof.context -> solver_config) * solver_info) Symtab.table
+  type T = solver_info Symtab.table
   val empty = Symtab.empty
   val extend = I
   fun merge data = Symtab.merge (K true) data
@@ -229,10 +291,48 @@
 )
 
 val no_solver = "(none)"
-val add_solver = Solvers.map o Symtab.update_new o apsnd (rpair (K []))
+
+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
+        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
+
+fun add_solver cfg =
+  let
+    val {name, env_var, is_remote, options, interface, outcome, cex_parser,
+      reconstruct} = cfg
+
+    fun core_oracle () = @{cprop False}
+
+    fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
+      more_options=[], 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)
+  end
+
+end
+
 val all_solver_names_of = Symtab.keys o Solvers.get
 val lookup_solver = Symtab.lookup o Solvers.get
-fun add_solver_info (n, i) = Solvers.map (Symtab.map_entry n (apsnd (K i)))
 
 
 
@@ -256,7 +356,7 @@
 fun raw_solver_of context name =
   (case lookup_solver context name of
     NONE => error "No SMT solver selected"
-  | SOME (s, _) => s)
+  | SOME s => s)
 
 fun solver_of context =
   let val name = solver_name_of context
@@ -264,58 +364,57 @@
 
 
 
-(* SMT solver *)
+(* SMT filter *)
 
 val has_topsort = Term.exists_type (Term.exists_subtype (fn
     TFree (_, []) => true
   | TVar (_, []) => true
   | _ => false))
 
-fun smt_solver ctxt xrules =
+fun smt_solver ctxt irules =
   (* without this test, we would run into problems when atomizing the rules: *)
-  if exists (has_topsort o Thm.prop_of o snd) xrules
-  then raise SMT "proof state contains the universal sort {}"
-  else
+  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) ctxt irules
+
+fun smt_filter st i xrules =
+  let
+    val {context, facts, goal} = Proof.goal st
+    val cprop =
+      Thm.cprem_of goal i
+      |> Thm.rhs_of o SMT_Normalize.atomize_conv context
+      |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
+    val irs = map (pair ~1) (Thm.assume cprop :: facts)
+  in
     split_list xrules
-    ||>> solver_of (Context.Proof ctxt) ctxt o map_index I
+    ||>> solver_of (Context.Proof context) context o append irs o map_index I
     |>> uncurry (map_filter o try o nth) o apsnd (distinct (op =))
-
-fun smt_filter ctxt xrules =
-  (fst (smt_solver ctxt xrules), "")
-  handle SMT msg => ([], "SMT: " ^ msg)
-       | SMT_COUNTEREXAMPLE _ => ([], "SMT: potential counterexample")
+    |> rpair NONE o fst
+  end
+  handle SMT fail => ([], SOME fail)
 
 
 
 (* SMT tactic *)
 
 local
-  fun pretty_cex ctxt (real, ex) =
-    let
-      val msg = if real then "SMT: counterexample found"
-        else "SMT: potential counterexample found"
-    in
-      if null ex then msg ^ "."
-      else Pretty.string_of (Pretty.big_list (msg ^ ":")
-        (map (Syntax.pretty_term ctxt) ex))
-    end
-
   fun fail_tac f msg st = (f msg; Tactical.no_tac st)
 
   fun SAFE pass_exns tac ctxt i st =
     if pass_exns then tac ctxt i st
-    else (tac ctxt i st
-      handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st
-           | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st)
+    else (tac ctxt i st handle SMT fail => fail_tac
+      (trace_msg ctxt (prefix "SMT: ") o string_of_failure ctxt) fail st)
 in
+
 fun smt_tac' pass_exns ctxt rules =
   CONVERSION (SMT_Normalize.atomize_conv ctxt)
   THEN' Tactic.rtac @{thm ccontr}
   THEN' SUBPROOF (fn {context, prems, ...} =>
-    let fun solve cx = snd (smt_solver cx (map (pair ()) (rules @ prems)))
+    let fun solve cx = snd (smt_solver cx (map (pair ~1) (rules @ prems)))
     in SAFE pass_exns (Tactic.rtac o solve) context 1 end) ctxt
 
 val smt_tac = smt_tac' false
+
 end
 
 val smt_method =
@@ -332,8 +431,11 @@
     (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration" #>
+  setup_oracle #>
+  setup_datatypes #>
   setup_timeout #>
   setup_trace #>
+  setup_trace_used_facts #>
   setup_fixed_certificates #>
   Attrib.setup @{binding smt_certificates}
     (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
@@ -348,13 +450,12 @@
     val t = string_of_int (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 take_info = (fn (_, []) => NONE | info => SOME info)
-    val infos =
-      Solvers.get context
-      |> Symtab.dest
-      |> map_filter (fn (n, (_, info)) => take_info (n, info context))
-      |> sort (prod_ord string_ord (K EQUAL))
-      |> map (fn (n, ps) => Pretty.big_list (n ^ ":") ps)
+    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
@@ -363,12 +464,14 @@
       else "false"
   in
     Pretty.writeln (Pretty.big_list "SMT setup:" [
-      Pretty.str ("Current SMT solver: " ^ solver_name_of context),
+      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),
-      Pretty.big_list "Solver-specific settings:" infos])
+      Pretty.str ("Fixed certificates: " ^ fixed)])
   end
 
 val _ =

--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Oct 26 11:45:12 2010 +0200
@@ -15,7 +15,7 @@
   val add_builtins: builtins -> Context.generic -> Context.generic
   val add_logic: (term list -> string option) -> Context.generic ->
     Context.generic
-  val extra_norm: bool -> SMT_Normalize.extra_norm
+  val extra_norm: SMT_Normalize.extra_norm
   val interface: SMT_Solver.interface
 end
 
@@ -283,7 +283,7 @@
 (** interfaces **)
 
 val interface = {
-  extra_norm = extra_norm false,
+  extra_norm = extra_norm,
   translate = {
     prefixes = {
       sort_prefix = "S",

--- a/src/HOL/Tools/SMT/yices_solver.ML	Tue Oct 26 11:39:26 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(*  Title:      HOL/Tools/SMT/yices_solver.ML
-    Author:     Sascha Boehme, TU Muenchen
-
-Interface of the SMT solver Yices.
-*)
-
-signature YICES_SOLVER =
-sig
-  val setup: theory -> theory
-end
-
-structure Yices_Solver: YICES_SOLVER =
-struct
-
-val solver_name = "yices"
-val env_var = "YICES_SOLVER"
-
-val options = ["--smtlib"]
-
-fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])
-
-fun core_oracle (output, _) =
-  let
-    val empty_line = (fn "" => true | _ => false)
-    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
-    val (l, _) = split_first (snd (chop_while empty_line output))
-  in
-    if String.isPrefix "unsat" l then @{cprop False}
-    else if String.isPrefix "sat" l then raise_cex true
-    else if String.isPrefix "unknown" l then raise_cex false
-    else raise SMT_Solver.SMT (solver_name ^ " failed")
-  end
-
-fun solver oracle _ = {
-  command = {env_var=env_var, remote_name=NONE},
-  arguments = options,
-  interface = SMTLIB_Interface.interface,
-  reconstruct = pair o pair [] o oracle }
-
-val setup =
-  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
-  Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle)))
-
-end

--- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Oct 26 11:45:12 2010 +0200
@@ -8,7 +8,7 @@
 sig
   type builtin_fun = string * typ -> term list -> (string * term list) option
   val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic
-  val interface: bool -> SMT_Solver.interface
+  val interface: SMT_Solver.interface
 
   datatype sym = Sym of string * sym list
   type mk_builtins = {
@@ -95,8 +95,8 @@
   is_some (z3_builtin_fun' ctxt c ts) orelse 
   is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->))
 
-fun interface has_datatypes = {
-  extra_norm = extra_norm' has_datatypes,
+val interface = {
+  extra_norm = extra_norm',
   translate = {
     prefixes = prefixes,
     strict = strict,
@@ -105,7 +105,7 @@
       builtin_typ = builtin_typ,
       builtin_num = builtin_num,
       builtin_fun = z3_builtin_fun',
-      has_datatypes = has_datatypes},
+      has_datatypes = true},
     serialize = serialize}}
 
 end

--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Tue Oct 26 11:45:12 2010 +0200
@@ -240,8 +240,8 @@
 
 (* core parser *)
 
-fun parse_exn line_no msg = raise SMT_Solver.SMT ("Z3 proof parser (line " ^
-  string_of_int line_no ^ "): " ^ msg)
+fun parse_exn line_no msg = raise SMT_Solver.SMT (SMT_Solver.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	Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Oct 26 11:45:12 2010 +0200
@@ -8,7 +8,7 @@
 sig
   val add_z3_rule: thm -> Context.generic -> Context.generic
   val trace_assms: bool Config.T
-  val reconstruct: string list * SMT_Translate.recon -> Proof.context ->
+  val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
     (int list * thm) * Proof.context
   val setup: theory -> theory
 end
@@ -20,7 +20,8 @@
 structure T = Z3_Proof_Tools
 structure L = Z3_Proof_Literals
 
-fun z3_exn msg = raise SMT_Solver.SMT ("Z3 proof reconstruction: " ^ msg)
+fun z3_exn msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
+  ("Z3 proof reconstruction: " ^ msg))
 
 
 
@@ -826,7 +827,7 @@
     (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab)))
   end
 
-fun reconstruct (output, {typs, terms, unfolds, assms}) ctxt =
+fun reconstruct ctxt {typs, terms, unfolds, assms} output =
   P.parse ctxt typs terms output
   |> (fn (idx, (ptab, vars, cx)) => prove cx unfolds assms vars (idx, ptab))
 

--- a/src/HOL/Tools/SMT/z3_solver.ML	Tue Oct 26 11:39:26 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-(*  Title:      HOL/Tools/SMT/z3_solver.ML
-    Author:     Sascha Boehme, TU Muenchen
-
-Interface of the SMT solver Z3.
-*)
-
-signature Z3_SOLVER =
-sig
-  val proofs: bool Config.T
-  val options: string Config.T
-  val datatypes: bool Config.T
-  val setup: theory -> theory
-end
-
-structure Z3_Solver: Z3_SOLVER =
-struct
-
-val solver_name = "z3"
-val env_var = "Z3_SOLVER"
-
-val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false)
-val (options, options_setup) = Attrib.config_string "z3_options" (K "")
-val (datatypes, datatypes_setup) = Attrib.config_bool "z3_datatypes" (K false)
-
-fun add xs ys = ys @ xs
-
-fun explode_options s = String.tokens (Symbol.is_ascii_blank o str) s
-
-fun get_options ctxt =
-  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"]
-  |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
-  |> add (explode_options (Config.get ctxt options))
-
-fun pretty_config context = [
-  Pretty.str ("With proofs: " ^
-    (if Config.get_generic context proofs then "true" else "false")),
-  Pretty.str ("Options: " ^
-    space_implode " " (get_options (Context.proof_of context))) ]
-
-fun cmdline_options ctxt =
-  get_options ctxt
-  |> add ["-smt"]
-
-fun raise_cex ctxt real recon ls =
-  let val cex = Z3_Model.parse_counterex ctxt recon ls
-  in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end
-
-fun if_unsat f (output, recon) ctxt =
-  let
-    fun jnk l =
-      String.isPrefix "WARNING" l orelse
-      String.isPrefix "ERROR" l orelse
-      forall Symbol.is_ascii_blank (Symbol.explode l)
-    val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output))
-  in
-    if String.isPrefix "unsat" l then f (ls, recon) ctxt
-    else if String.isPrefix "sat" l then raise_cex ctxt true recon ls
-    else if String.isPrefix "unknown" l then raise_cex ctxt false recon ls
-    else raise SMT_Solver.SMT (solver_name ^ " failed")
-  end
-
-val core_oracle = uncurry (if_unsat (K (K @{cprop False})))
-
-val prover = if_unsat Z3_Proof_Reconstruction.reconstruct
-
-fun solver oracle ctxt =
-  let
-    val with_datatypes = Config.get ctxt datatypes
-    val with_proof = not with_datatypes andalso Config.get ctxt proofs
-                     (* FIXME: implement proof reconstruction for datatypes *)
-  in
-   {command = {env_var=env_var, remote_name=SOME solver_name},
-    arguments = cmdline_options ctxt,
-    interface = Z3_Interface.interface with_datatypes,
-    reconstruct =
-      if with_proof then prover else (fn r => `(pair [] o oracle o pair r))}
-  end
-
-val setup =
-  proofs_setup #>
-  options_setup #>
-  datatypes_setup #>
-  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
-  Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) #>
-  Context.theory_map (SMT_Solver.add_solver_info (solver_name, pretty_config))
-
-end