# HG changeset patch
# User boehmes
# Date 1291729992 -3600
# Node ID d2b1fc1b8e19273b7a11187c0c4b8554156a1e1d
# Parent  42e0a0bfef736247c1d78c9685f500a3c4a4abec
centralized handling of built-in types and constants;
also store types and constants which are rewritten during preprocessing;
interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols);
removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)

diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/SMT.thy	Tue Dec 07 14:53:12 2010 +0100
@@ -105,16 +105,18 @@
 subsection {* First-order logic *}
 
 text {*
-Some SMT solvers require a strict separation between formulas and
-terms.  When translating higher-order into first-order problems,
-all uninterpreted constants (those not builtin in the target solver)
+Some SMT solvers only accept problems in first-order logic, i.e.,
+where formulas and terms are syntactically separated. When
+translating higher-order into first-order problems, all
+uninterpreted constants (those not built-in in the target solver)
 are treated as function symbols in the first-order sense.  Their
-occurrences as head symbols in atoms (i.e., as predicate symbols) is
-turned into terms by equating such atoms with @{term True} using the
-following term-level equation symbol.
+occurrences as head symbols in atoms (i.e., as predicate symbols) are
+turned into terms by equating such atoms with @{term True}.
+Whenever the boolean type occurs in first-order terms, it is replaced
+by the following type.
 *}
 
-definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
+typedecl term_bool
 
 
 
@@ -159,7 +161,10 @@
 
 setup {*
   SMT_Config.setup #>
+  SMT_Normalize.setup #>
   SMT_Solver.setup #>
+  SMTLIB_Interface.setup #>
+  Z3_Interface.setup #>
   Z3_Proof_Reconstruction.setup #>
   SMT_Setup_Solvers.setup
 *}
@@ -354,9 +359,10 @@
 
 
 
+hide_type term_bool
 hide_type (open) pattern
-hide_const Pattern term_eq
-hide_const (open) trigger pat nopat weight fun_app z3div z3mod
+hide_const Pattern fun_app
+hide_const (open) trigger pat nopat weight z3div z3mod
 
 
 
diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Dec 07 14:53:12 2010 +0100
@@ -1,116 +1,226 @@
 (*  Title:      HOL/Tools/SMT/smt_builtin.ML
     Author:     Sascha Boehme, TU Muenchen
 
-Crafted collection of SMT built-in symbols.
-
-FIXME: This list is currently not automatically kept synchronized with the
-remaining implementation.
+Tables of types and terms directly supported by SMT solvers.
 *)
 
 signature SMT_BUILTIN =
 sig
-  val is_builtin: Proof.context -> string * typ -> bool
-  val is_partially_builtin: Proof.context -> string * typ -> bool
+  (*built-in types*)
+  val add_builtin_typ: SMT_Config.class ->
+    typ * (typ -> string option) * (typ -> int -> string option) -> theory ->
+    theory
+  val add_builtin_typ_ext: typ * (typ -> bool) -> theory -> theory
+  val builtin_typ: Proof.context -> typ -> string option
+  val is_builtin_typ: Proof.context -> typ -> bool
+  val is_builtin_typ_ext: Proof.context -> typ -> bool
+
+  (*built-in numbers*)
+  val builtin_num: Proof.context -> term -> string option
+  val is_builtin_num: Proof.context -> term -> bool
+  val is_builtin_num_ext: Proof.context -> term -> bool
+
+  (*built-in functions*)
+  type 'a bfun = Proof.context -> typ -> term list -> 'a
+  val add_builtin_fun: SMT_Config.class ->
+    (string * typ) * (string * term list) option bfun -> theory -> theory
+  val add_builtin_fun': SMT_Config.class -> term * string -> theory -> theory
+  val add_builtin_fun_ext: (string * typ) * bool bfun -> theory -> theory
+  val add_builtin_fun_ext': string * typ -> theory -> theory
+  val add_builtin_fun_ext'': string -> theory -> theory
+  val builtin_fun: Proof.context -> string * typ -> term list ->
+    (string * term list) option
+  val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
+  val is_builtin_pred: Proof.context -> string * typ -> term list -> bool
+  val is_builtin_conn: Proof.context -> string * typ -> term list -> bool
+  val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
 end
 
 structure SMT_Builtin: SMT_BUILTIN =
 struct
 
-fun is_arithT T =
-  (case T of
-     @{typ int} => true
-   | @{typ nat} => true
-   | Type ("RealDef.real", []) => true
-   | _ => false)
+structure C = SMT_Config
+
+
+(* built-in tables *)
+
+datatype ('a, 'b) kind = Ext of 'a | Int of 'b
+
+type ('a, 'b) ttab = (C.class * (typ * ('a, 'b) kind) Ord_List.T) list 
 
-fun is_arithT_dom (Type (@{type_name fun}, [T, _])) = is_arithT T
-  | is_arithT_dom _ = false
-fun is_arithT_ran (Type (@{type_name fun}, [_, T])) = is_arithT T
-  | is_arithT_ran _ = false
+fun empty_ttab () = []
 
-val builtins = Symtab.make [
-
-  (* Pure constants *)
-  (@{const_name all}, K true),
-  (@{const_name "=="}, K true),
-  (@{const_name "==>"}, K true),
-  (@{const_name Trueprop}, K true),
+fun typ_ord ((T, _), (U, _)) =
+  let
+    fun tord (TVar _, Type _) = GREATER
+      | tord (Type _, TVar _) = LESS
+      | tord (Type (n, Ts), Type (m, Us)) =
+          if n = m then list_ord tord (Ts, Us)
+          else Term_Ord.typ_ord (T, U)
+      | tord TU = Term_Ord.typ_ord TU
+  in tord (T, U) end
 
-  (* logical constants *)
-  (@{const_name All}, K true),
-  (@{const_name Ex}, K true),
-  (@{const_name Ball}, K true),
-  (@{const_name Bex}, K true),
-  (@{const_name Ex1}, K true),
-  (@{const_name True}, K true),
-  (@{const_name False}, K true),
-  (@{const_name Not}, K true),
-  (@{const_name HOL.conj}, K true),
-  (@{const_name HOL.disj}, K true),
-  (@{const_name HOL.implies}, K true),
+fun insert_ttab cs T f =
+  AList.map_default (op =) (cs, [])
+    (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
+
+fun merge_ttab ttabp =
+  AList.join (op =) (K (uncurry (Ord_List.union typ_ord) o swap)) ttabp
 
-  (* term abbreviations *)
-  (@{const_name If}, K true),
-  (@{const_name bool.bool_case}, K true),
-  (@{const_name Let}, K true),
-  (* (@{const_name distinct}, K true),  -- not a real builtin, only when
-                                           applied to an explicit list *)
+fun lookup_ttab ctxt ttab T =
+  let
+    val cs = C.solver_class_of ctxt
+    fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)
+
+    fun matching (cs', Txs) =
+      if is_prefix (op =) cs' cs then find_first match Txs
+      else NONE
+  in get_first matching ttab end
+
+type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
+
+fun empty_btab () = Symtab.empty
 
-  (* technicalities *)
-  (@{const_name SMT.pat}, K true),
-  (@{const_name SMT.nopat}, K true),
-  (@{const_name SMT.trigger}, K true),
-  (@{const_name SMT.weight}, K true),
-  (@{const_name SMT.fun_app}, K true),
-  (@{const_name SMT.z3div}, K true),
-  (@{const_name SMT.z3mod}, K true),
+fun insert_btab cs n T f =
+  Symtab.map_default (n, []) (insert_ttab cs T f)
+
+fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
 
-  (* equality *)
-  (@{const_name HOL.eq}, K true),
+fun lookup_btab ctxt btab (n, T) =
+  (case Symtab.lookup btab n of
+    NONE => NONE
+  | SOME ttab => lookup_ttab ctxt ttab T)
 
-  (* numerals *)
-  (@{const_name zero_class.zero}, is_arithT),
-  (@{const_name one_class.one}, is_arithT),
-  (@{const_name Int.Pls}, K true),
-  (@{const_name Int.Min}, K true),
-  (@{const_name Int.Bit0}, K true),
-  (@{const_name Int.Bit1}, K true),
-  (@{const_name number_of}, is_arithT_ran),
+
+(* built-in types *)
 
-  (* arithmetic *)
-  (@{const_name nat}, K true),
-  (@{const_name of_nat}, K true),
-  (@{const_name Suc}, K true),
-  (@{const_name plus}, is_arithT_dom),
-  (@{const_name uminus}, is_arithT_dom),
-  (@{const_name minus}, is_arithT_dom),
-  (@{const_name abs}, is_arithT_dom),
-  (@{const_name min}, is_arithT_dom),
-  (@{const_name max}, is_arithT_dom),
-  (@{const_name less}, is_arithT_dom),
-  (@{const_name less_eq}, is_arithT_dom),
-  
-  (* pairs *)
-  (@{const_name fst}, K true),
-  (@{const_name snd}, K true),
-  (@{const_name Pair}, K true)
+structure Builtin_Types = Theory_Data
+(
+  type T =
+    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
+  val empty = empty_ttab ()
+  val extend = I
+  val merge = merge_ttab
+)
+
+fun add_builtin_typ cs (T, f, g) =
+  Builtin_Types.map (insert_ttab cs T (Int (f, g)))
+
+fun add_builtin_typ_ext (T, f) =
+  Builtin_Types.map (insert_ttab C.basicC T (Ext f))
 
-  ]
+fun lookup_builtin_typ ctxt =
+  lookup_ttab ctxt (Builtin_Types.get (ProofContext.theory_of ctxt))
 
-val all_builtins =
-  builtins
-  |> Symtab.update (@{const_name times}, is_arithT_dom)
-  |> Symtab.update (@{const_name div_class.div}, is_arithT_dom)
-  |> Symtab.update (@{const_name div_class.mod}, is_arithT_dom)
-  |> Symtab.update ("Rings.inverse_class.divide", is_arithT_dom)
+fun builtin_typ ctxt T =
+  (case lookup_builtin_typ ctxt T of
+    SOME (_, Int (f, _)) => f T
+  | _ => NONE) 
 
-fun lookup_builtin bs (name, T) =
-  (case Symtab.lookup bs name of
-    SOME proper_type => proper_type T
+fun is_builtin_typ ctxt T = is_some (builtin_typ ctxt T)
+
+fun is_builtin_typ_ext ctxt T =
+  (case lookup_builtin_typ ctxt T of
+    SOME (_, Int (f, _)) => is_some (f T)
+  | SOME (_, Ext f) => f T
   | NONE => false)
 
-fun is_builtin _ = lookup_builtin builtins
+
+(* built-in numbers *)
+
+fun builtin_num ctxt t =
+  (case try HOLogic.dest_number t of
+    NONE => NONE
+  | SOME (T, i) =>
+      (case lookup_builtin_typ ctxt T of
+        SOME (_, Int (_, g)) => g T i
+      | _ => NONE))
+
+val is_builtin_num = is_some oo builtin_num
+
+fun is_builtin_num_ext ctxt t =
+  (case try HOLogic.dest_number t of
+    NONE => false
+  | SOME (T, _) => is_builtin_typ_ext ctxt T)
+
+
+(* built-in functions *)
+
+type 'a bfun = Proof.context -> typ -> term list -> 'a
+
+fun true3 _ _ _ = true
+
+fun raw_add_builtin_fun_ext thy cs n =
+  insert_btab cs n (Sign.the_const_type thy n) (Ext true3)
+
+val basic_builtin_fun_names = [
+  @{const_name SMT.pat}, @{const_name SMT.nopat},
+  @{const_name SMT.trigger}, @{const_name SMT.weight}]
+
+fun basic_builtin_funcs () =
+  empty_btab ()
+  |> fold (raw_add_builtin_fun_ext @{theory} C.basicC) basic_builtin_fun_names
+       (* FIXME: SMT_Normalize should check that they are properly used *)
+
+structure Builtin_Funcs = Theory_Data
+(
+  type T = (bool bfun, (string * term list) option bfun) btab
+  val empty = basic_builtin_funcs ()
+  val extend = I
+  val merge = merge_btab
+)
+
+fun add_builtin_fun cs ((n, T), f) =
+  Builtin_Funcs.map (insert_btab cs n T (Int f))
 
-fun is_partially_builtin _ = lookup_builtin all_builtins
+fun add_builtin_fun' cs (t, n) =
+  add_builtin_fun cs (Term.dest_Const t, fn _ => fn _ => SOME o pair n)
+
+fun add_builtin_fun_ext ((n, T), f) =
+  Builtin_Funcs.map (insert_btab C.basicC n T (Ext f))
+
+fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, true3)
+
+fun add_builtin_fun_ext'' n thy =
+  add_builtin_fun_ext' (n, Sign.the_const_type thy n) thy
+
+fun lookup_builtin_fun ctxt =
+  lookup_btab ctxt (Builtin_Funcs.get (ProofContext.theory_of ctxt))
+
+fun builtin_fun ctxt (c as (_, T)) ts =
+  (case lookup_builtin_fun ctxt c of
+    SOME (_, Int f) => f ctxt T ts
+  | _ => NONE)
+
+fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts)
+
+fun is_special_builtin_fun pred ctxt (c as (_, T)) ts =
+  (case lookup_builtin_fun ctxt c of
+    SOME (U, Int f) => pred U andalso is_some (f ctxt T ts)
+  | _ => false)
+
+fun is_pred_type T = Term.body_type T = @{typ bool}
+fun is_conn_type T =
+  forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
+
+fun is_builtin_pred ctxt = is_special_builtin_fun is_pred_type ctxt
+fun is_builtin_conn ctxt = is_special_builtin_fun is_conn_type ctxt
+
+fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
+  (case lookup_builtin_fun ctxt c of
+    SOME (_, Int f) => is_some (f ctxt T ts)
+  | SOME (_, Ext f) => f ctxt T ts
+  | NONE => false)
+
+(* FIXME: move this information to the interfaces *)
+val only_partially_supported = [
+  @{const_name times},
+  @{const_name div_class.div},
+  @{const_name div_class.mod},
+  @{const_name inverse_class.divide} ]
+
+fun is_builtin_ext ctxt (c as (n, _)) ts =
+  if member (op =) only_partially_supported n then false
+  else is_builtin_fun_ext ctxt c ts
 
 end
diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Dec 07 14:53:12 2010 +0100
@@ -6,11 +6,16 @@
 
 signature SMT_CONFIG =
 sig
+  (*class*)
+  type class = string list
+  val basicC: class
+
   (*solver*)
-  val add_solver: string -> Context.generic -> Context.generic
+  val add_solver: string * class -> 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_class_of: Proof.context -> class
   val solver_options_of: Proof.context -> string list
 
   (*options*)
@@ -46,11 +51,18 @@
 structure SMT_Config: SMT_CONFIG =
 struct
 
+(* class *)
+
+type class = string list
+
+val basicC = []
+
+
 (* solver *)
 
 structure Solvers = Generic_Data
 (
-  type T = string list Symtab.table * string option
+  type T = (class * 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)
@@ -58,14 +70,14 @@
 
 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
+  in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
 
-fun add_solver name context =
+fun add_solver (name, class) context =
   if Symtab.defined (fst (Solvers.get context)) name then
     error ("Solver already registered: " ^ quote name)
   else
     context
-    |> Solvers.map (apfst (Symtab.update (name, [])))
+    |> Solvers.map (apfst (Symtab.update (name, (class, []))))
     |> 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))
@@ -76,18 +88,23 @@
     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 no_solver_err () = error "No SMT solver selected"
 
 fun solver_of ctxt =
-  (case lookup_solver ctxt of
-    SOME name => name
-  | NONE => error "No SMT solver selected")
+  (case Solvers.get (Context.Proof ctxt) of
+    (_, SOME name) => name
+  | (_, NONE) => no_solver_err ())
+
+fun solver_class_of ctxt =
+  (case Solvers.get (Context.Proof ctxt) of
+    (solvers, SOME name) => fst (the (Symtab.lookup solvers name))
+  | (_, NONE) => no_solver_err())
 
 fun solver_options_of ctxt =
-  (case lookup_solver ctxt of
-    NONE => []
-  | SOME name =>
-      Symtab.lookup_list (fst (Solvers.get (Context.Proof ctxt))) name)
+  (case Solvers.get (Context.Proof ctxt) of
+    (solvers, SOME name) =>
+      (case Symtab.lookup solvers name of SOME (_, opts) => opts | NONE => [])
+  | (_, NONE) => [])
 
 val setup_solver =
   Attrib.setup @{binding smt_solver}
diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 07 14:53:12 2010 +0100
@@ -23,12 +23,14 @@
     (int * thm) list * Proof.context
   val atomize_conv: Proof.context -> conv
   val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
+  val setup: theory -> theory
 end
 
 structure SMT_Normalize: SMT_NORMALIZE =
 struct
 
 structure U = SMT_Utils
+structure B = SMT_Builtin
 
 infix 2 ??
 fun (test ?? f) x = if test x then f x else x
@@ -95,6 +97,9 @@
 fun rewrite_bool_cases ctxt =
   map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
     Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt)))
+
+val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
+
 end
 
 
@@ -203,10 +208,20 @@
   val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
   val uses_nat_int = Term.exists_subterm (member (op aconv)
     [@{const of_nat (int)}, @{const nat}])
+
+  val nat_ops = [
+    @{const less (nat)}, @{const less_eq (nat)},
+    @{const Suc}, @{const plus (nat)}, @{const minus (nat)},
+    @{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
+  val nat_ops' = @{const of_nat (int)} :: @{const nat} :: nat_ops
 in
 fun nat_as_int ctxt =
   map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
   exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding
+
+val setup_nat_as_int =
+  B.add_builtin_typ_ext (@{typ nat}, K true) #>
+  fold (B.add_builtin_fun_ext' o Term.dest_Const) nat_ops'
 end
 
 
@@ -263,7 +278,7 @@
     | _ =>
         (case Term.strip_comb (Thm.term_of ct) of
           (Const (c as (_, T)), ts) =>
-            if SMT_Builtin.is_partially_builtin ctxt c
+            if SMT_Builtin.is_builtin_fun ctxt c ts
             then eta_args_conv norm_conv
               (length (Term.binder_types T) - length ts)
             else args_conv o norm_conv
@@ -294,7 +309,7 @@
     | _ =>
         (case Term.strip_comb t of
           (Const (c as (_, T)), ts) =>
-            if SMT_Builtin.is_builtin ctxt c
+            if SMT_Builtin.is_builtin_fun ctxt c ts
             then length (Term.binder_types T) = length ts andalso
               forall (is_normed ctxt) ts
             else forall (is_normed ctxt) ts
@@ -302,6 +317,11 @@
 in
 fun norm_binder_conv ctxt =
   U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
+
+val setup_unfolded_quants =
+  fold B.add_builtin_fun_ext'' [@{const_name Ball}, @{const_name Bex},
+    @{const_name Ex1}]
+
 end
 
 fun norm_def ctxt thm =
@@ -325,6 +345,10 @@
       Conv.rewr_conv @{thm atomize_all}
   | _ => Conv.all_conv) ct
 
+val setup_atomize =
+  fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
+    @{const_name all}, @{const_name Trueprop}]
+
 fun normalize_rule ctxt =
   Conv.fconv_rule (
     (* reduce lambda abstractions, except at known binders: *)
@@ -554,4 +578,14 @@
     |-> (if with_datatypes then datatype_selectors else pair)
   end
 
+
+
+(* setup *)
+
+val setup =
+  setup_bool_case #>
+  setup_nat_as_int #>
+  setup_unfolded_quants #>
+  setup_atomize
+
 end
diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML	Tue Dec 07 14:53:12 2010 +0100
@@ -12,6 +12,8 @@
 structure SMT_Real: SMT_REAL =
 struct
 
+structure B = SMT_Builtin
+
 
 (* SMT-LIB logic *)
 
@@ -21,58 +23,28 @@
   else NONE
 
 
-
-(* SMT-LIB builtins *)
+(* SMT-LIB and Z3 built-ins *)
 
 local
-  fun smtlib_builtin_typ @{typ real} = SOME "Real"
-    | smtlib_builtin_typ _ = NONE
-
-  fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
-    | smtlib_builtin_num _ _ = NONE
+  val smtlibC = SMTLIB_Interface.smtlibC
 
-  fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts)
-    | smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts)
-    | smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts)
-    | smtlib_builtin_func @{const_name times} ts = SOME ("*", ts)
-    | smtlib_builtin_func _ _ = NONE
-
-  fun smtlib_builtin_pred @{const_name less} = SOME "<"
-    | smtlib_builtin_pred @{const_name less_eq} = SOME "<="
-    | smtlib_builtin_pred _ = NONE
-
-  fun real_fun T y f x = 
-    (case try Term.domain_type T of
-      SOME @{typ real} => f x
-    | _ => y)
+  fun real_num _ i = SOME (string_of_int i ^ ".0")
 in
 
-val smtlib_builtins = {
-  builtin_typ = smtlib_builtin_typ,
-  builtin_num = smtlib_builtin_num,
-  builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)),
-  builtin_pred = (fn (n, T) => fn ts =>
-    real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)),
-  is_builtin_pred = (fn n => fn T =>
-    real_fun T false (is_some o smtlib_builtin_pred) n) }
+val setup_builtins =
+  B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
+  fold (B.add_builtin_fun' smtlibC) [
+    (@{const uminus (real)}, "~"),
+    (@{const plus (real)}, "+"),
+    (@{const minus (real)}, "-"),
+    (@{const times (real)}, "*"),
+    (@{const less (real)}, "<"),
+    (@{const less_eq (real)}, "<=") ] #>
+  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
 
 end
 
 
-
-(* Z3 builtins *)
-
-local
-  fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
-    | z3_builtin_fun _ _ = NONE
-in
-
-val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts)
-
-end
-
-
-
 (* Z3 constructors *)
 
 local
@@ -117,7 +89,6 @@
 end
 
 
-
 (* Z3 proof reconstruction *)
 
 val real_rules = @{lemma
@@ -132,14 +103,12 @@
   "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
 
 
-
 (* setup *)
 
 val setup =
+  setup_builtins #>
   Context.theory_map (
-    SMTLIB_Interface.add_logic smtlib_logic #>
-    SMTLIB_Interface.add_builtins smtlib_builtins #>
-    Z3_Interface.add_builtin_funs z3_builtins #>
+    SMTLIB_Interface.add_logic (10, smtlib_logic) #>
     Z3_Interface.add_mk_builtins z3_mk_builtins #>
     fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
     Z3_Proof_Tools.add_simproc real_linarith_proc)
diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Dec 07 14:53:12 2010 +0100
@@ -8,6 +8,7 @@
 sig
   (*configuration*)
   type interface = {
+    class: SMT_Config.class,
     extra_norm: SMT_Normalize.extra_norm,
     translate: SMT_Translate.config }
   datatype outcome = Unsat | Sat | Unknown
@@ -57,6 +58,7 @@
 (* configuration *)
 
 type interface = {
+  class: SMT_Config.class,
   extra_norm: SMT_Normalize.extra_norm,
   translate: SMT_Translate.config }
 
@@ -195,13 +197,10 @@
 
 fun set_has_datatypes with_datatypes translate =
   let
-    val {prefixes, header, strict, builtins, serialize} = translate
-    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
+    val {prefixes, header, is_fol, has_datatypes, serialize} = translate
     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}
+    val translate' = {prefixes=prefixes, header=header, is_fol=is_fol,
+      has_datatypes=with_datatypes', serialize=serialize}
   in (with_datatypes', translate') end
 
 fun trace_assumptions ctxt irules idxs =
@@ -219,7 +218,7 @@
 fun gen_solver name info rm ctxt irules =
   let
     val {env_var, is_remote, options, interface, reconstruct, ...} = info
-    val {extra_norm, translate} = interface
+    val {extra_norm, translate, ...} = interface
     val (with_datatypes, translate') =
       set_has_datatypes (Config.get ctxt C.datatypes) translate
     val cmd = (rm, env_var, is_remote, name)
@@ -284,6 +283,7 @@
   let
     val {name, env_var, is_remote, options, interface, outcome, cex_parser,
       reconstruct, default_max_relevant} = cfg
+    val {class, ...} = interface
 
     fun core_oracle () = cfalse
 
@@ -294,7 +294,7 @@
   in
     Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
     Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
-    Context.theory_map (C.add_solver name)
+    Context.theory_map (C.add_solver (name, class))
   end
 
 end
diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Dec 07 14:53:12 2010 +0100
@@ -17,17 +17,6 @@
 
   (* configuration options *)
   type prefixes = {sort_prefix: string, func_prefix: string}
-  type header = Proof.context -> term list -> string list
-  type strict = {
-    is_builtin_conn: string * typ -> bool,
-    is_builtin_pred: Proof.context -> string * typ -> bool,
-    is_builtin_distinct: bool}
-  type builtins = {
-    builtin_typ: Proof.context -> typ -> string option,
-    builtin_num: Proof.context -> typ -> int -> string option,
-    builtin_fun: Proof.context -> string * typ -> term list ->
-      (string * term list) option,
-    has_datatypes: bool }
   type sign = {
     header: string list,
     sorts: string list,
@@ -35,9 +24,9 @@
     funcs: (string * (string list * string)) list }
   type config = {
     prefixes: prefixes,
-    header: header,
-    strict: strict option,
-    builtins: builtins,
+    header: Proof.context -> term list -> string list,
+    is_fol: bool,
+    has_datatypes: bool,
     serialize: string list -> sign -> sterm list -> string }
   type recon = {
     typs: typ Symtab.table,
@@ -53,6 +42,7 @@
 struct
 
 structure U = SMT_Utils
+structure B = SMT_Builtin
 
 
 (* intermediate term structure *)
@@ -73,20 +63,6 @@
 
 type prefixes = {sort_prefix: string, func_prefix: string}
 
-type header = Proof.context -> term list -> string list
-
-type strict = {
-  is_builtin_conn: string * typ -> bool,
-  is_builtin_pred: Proof.context -> string * typ -> bool,
-  is_builtin_distinct: bool}
-
-type builtins = {
-  builtin_typ: Proof.context -> typ -> string option,
-  builtin_num: Proof.context -> typ -> int -> string option,
-  builtin_fun: Proof.context -> string * typ -> term list ->
-    (string * term list) option,
-  has_datatypes: bool }
-
 type sign = {
   header: string list,
   sorts: string list,
@@ -95,9 +71,9 @@
 
 type config = {
   prefixes: prefixes,
-  header: header,
-  strict: strict option,
-  builtins: builtins,
+  header: Proof.context -> term list -> string list,
+  is_fol: bool,
+  has_datatypes: bool,
   serialize: string list -> sign -> sterm list -> string }
 
 type recon = {
@@ -152,13 +128,20 @@
 
 
 
-(* enforce a strict separation between formulas and terms *)
+(* map HOL formulas to FOL formulas (i.e., separate formulas froms terms) *)
 
-val term_eq_rewr = @{lemma "term_eq x y == x = y" by (simp add: term_eq_def)}
+val tboolT = @{typ SMT.term_bool}
+val term_true = Const (@{const_name True}, tboolT)
+val term_false = Const (@{const_name False}, tboolT)
 
-val term_bool = @{lemma "~(term_eq True False)" by (simp add: term_eq_def)}
-val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
-
+val term_bool = @{lemma "True ~= False" by simp}
+val term_bool_prop =
+  let
+    fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)}
+      | replace @{const True} = term_true
+      | replace @{const False} = term_false
+      | replace t = t
+  in Term.map_aterms replace (prop_of term_bool) end
 
 val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
     Const (@{const_name Let}, _) => true
@@ -171,63 +154,57 @@
   @{lemma "P = True == P" by (rule eq_reflection) simp},
   @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
 
-fun rewrite ctxt = Simplifier.full_rewrite
-  (Simplifier.context ctxt empty_ss addsimps rewrite_rules)
+fun rewrite ctxt ct =
+  Conv.top_sweep_conv (fn ctxt' =>
+    Conv.rewrs_conv rewrite_rules then_conv rewrite ctxt') ctxt ct
 
 fun normalize ctxt thm =
   if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
 
-val unfold_rules = term_eq_rewr :: rewrite_rules
-
+fun revert_typ @{typ SMT.term_bool} = @{typ bool}
+  | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts)
+  | revert_typ T = T
 
-val revert_types =
-  let
-    fun revert @{typ prop} = @{typ bool}
-      | revert (Type (n, Ts)) = Type (n, map revert Ts)
-      | revert T = T
-  in Term.map_types revert end
+val revert_types = Term.map_types revert_typ
 
-
-fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
+fun folify ctxt =
   let
-    fun is_builtin_conn' (@{const_name True}, _) = false
-      | is_builtin_conn' (@{const_name False}, _) = false
-      | is_builtin_conn' c = is_builtin_conn c
+    fun is_builtin_conn (@{const_name True}, _) _ = false
+      | is_builtin_conn (@{const_name False}, _) _ = false
+      | is_builtin_conn c ts = B.is_builtin_conn ctxt c ts
 
-    fun is_builtin_pred' _ (@{const_name distinct}, _) [t] =
-          is_builtin_distinct andalso can HOLogic.dest_list t
-      | is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
+    fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true
 
-    val propT = @{typ prop} and boolT = @{typ bool}
-    val as_propT = (fn @{typ bool} => propT | T => T)
+    fun as_tbool @{typ bool} = tboolT
+      | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts)
+      | as_tbool T = T
     fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
-    fun conn (n, T) = (n, mapTs as_propT as_propT T)
-    fun pred (n, T) = (n, mapTs I as_propT T)
+    fun predT T = mapTs as_tbool I T
+    fun funcT T = mapTs as_tbool as_tbool T
+    fun func (n, T) = Const (n, funcT T)
 
-    val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
-    fun as_term t = Const term_eq $ t $ @{const True}
-
-    val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
-    fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
+    fun map_ifT T = T |> Term.dest_funT ||> funcT |> (op -->)
+    val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const
+    fun wrap_in_if t = if_term $ t $ term_true $ term_false
 
     fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
 
     fun in_term t =
       (case Term.strip_comb t of
-        (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
-          c $ in_form t1 $ in_term t2 $ in_term t3
-      | (h as Const c, ts) =>
-          if is_builtin_conn' (conn c) orelse is_builtin_pred' ctxt (pred c) ts
+        (Const (c as @{const_name If}, T), [t1, t2, t3]) =>
+          Const (c, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3
+      | (Const c, ts) =>
+          if is_builtin_conn c ts orelse B.is_builtin_pred ctxt c ts
           then wrap_in_if (in_form t)
-          else Term.list_comb (h, map in_term ts)
-      | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
+          else Term.list_comb (func c, map in_term ts)
+      | (Free (n, T), ts) => Term.list_comb (Free (n, funcT T), map in_term ts)
       | _ => t)
 
     and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
       | in_weight t = in_form t 
 
-    and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
-      | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
+    and in_pat (Const (c as (@{const_name pat}, _)) $ t) = func c $ in_term t
+      | in_pat (Const (c as (@{const_name nopat}, _)) $ t) = func c $ in_term t
       | in_pat t = raise TERM ("in_pat", [t])
 
     and in_pats ps =
@@ -239,23 +216,23 @@
     and in_form t =
       (case Term.strip_comb t of
         (q as Const (qn, _), [Abs (n, T, t')]) =>
-          if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
+          if is_some (quantifier qn) then q $ Abs (n, as_tbool T, in_trig t')
           else as_term (in_term t)
-      | (Const (c as (@{const_name distinct}, T)), [t']) =>
-          if is_builtin_distinct andalso can HOLogic.dest_list t' then
-            Const (pred c) $ in_list T in_term t'
+      | (Const (c as (n as @{const_name distinct}, T)), [t']) =>
+          if B.is_builtin_fun ctxt c [t'] then
+            Const (n, predT T) $ in_list T in_term t'
           else as_term (in_term t)
-      | (Const c, ts) =>
-          if is_builtin_conn (conn c)
-          then Term.list_comb (Const (conn c), map in_form ts)
-          else if is_builtin_pred ctxt (pred c)
-          then Term.list_comb (Const (pred c), map in_term ts)
+      | (Const (c as (n, T)), ts) =>
+          if B.is_builtin_conn ctxt c ts
+          then Term.list_comb (Const c, map in_form ts)
+          else if B.is_builtin_pred ctxt c ts
+          then Term.list_comb (Const (n, predT T), map in_term ts)
           else as_term (in_term t)
       | _ => as_term (in_term t))
   in
     map (apsnd (normalize ctxt)) #> (fn irules =>
-    ((unfold_rules, (~1, term_bool') :: irules),
-     map (in_form o prop_of o snd) ((~1, term_bool) :: irules)))
+    ((rewrite_rules, (~1, term_bool) :: irules),
+     term_bool_prop :: map (in_form o prop_of o snd) irules))
   end
 
 
@@ -280,10 +257,12 @@
 fun string_of_index pre i = pre ^ string_of_int i
 
 fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) =
-  let val s = string_of_index sort_prefix Tidx
-  in (s, (Tidx+1, Typtab.update (T, (s, proper)) typs, dtyps, idx, terms)) end
+  let
+    val s = string_of_index sort_prefix Tidx
+    val U = revert_typ T
+  in (s, (Tidx+1, Typtab.update (U, (s, proper)) typs, dtyps, idx, terms)) end
 
-fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs
+fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs o revert_typ
 
 fun fresh_typ T f cx =
   (case lookup_typ cx T of
@@ -297,7 +276,7 @@
   in (f, (Tidx, typs, dtyps, idx+1, terms')) end
 
 fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) =
-  (case Termtab.lookup terms t of
+  (case Termtab.lookup terms (revert_types t) of
     SOME (f, _) => (f, cx)
   | NONE => new_fun func_prefix t ss cx)
 
@@ -335,15 +314,15 @@
   in ((make_sign (header ts) context, us), make_recon ths context) end
 
 
-fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
+fun translate config ctxt comments =
   let
+    val {prefixes, is_fol, header, has_datatypes, serialize} = config
     val {sort_prefix, func_prefix} = prefixes
-    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
 
     fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true)
       | transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], []))
       | transT (T as Type (n, Ts)) =
-          (case builtin_typ ctxt T of
+          (case B.builtin_typ ctxt T of
             SOME n => pair n
           | NONE => fresh_typ T (fn _ => fn cx =>
               if not has_datatypes then new_typ sort_prefix true T cx
@@ -387,17 +366,14 @@
           transT T ##>> trans t1 ##>> trans t2 #>>
           (fn ((U, u1), u2) => SLet (U, u1, u2))
       | (h as Const (c as (@{const_name distinct}, T)), ts) =>
-          (case builtin_fun ctxt c ts of
+          (case B.builtin_fun ctxt c ts of
             SOME (n, ts) => fold_map trans ts #>> app n
           | NONE => transs h T ts)
       | (h as Const (c as (_, T)), ts) =>
-          (case try HOLogic.dest_number t of
-            SOME (T, i) =>
-              (case builtin_num ctxt T i of
-                SOME n => pair (SApp (n, []))
-              | NONE => transs t T [])
+          (case B.builtin_num ctxt t of
+            SOME n => pair (SApp (n, []))
           | NONE =>
-              (case builtin_fun ctxt c ts of
+              (case B.builtin_fun ctxt c ts of
                 SOME (n, ts') => fold_map trans ts' #>> app n
               | NONE => transs h T ts))
       | (h as Free (_, T), ts) => transs h T ts
@@ -414,7 +390,7 @@
         fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
       end
   in
-    (case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>
+    (if is_fol then folify ctxt else relaxed) #>
     with_context (header ctxt) trans #>> uncurry (serialize comments)
   end
 
diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Dec 07 14:53:12 2010 +0100
@@ -6,34 +6,31 @@
 
 signature SMTLIB_INTERFACE =
 sig
-  type builtins = {
-    builtin_typ: typ -> string option,
-    builtin_num: typ -> int -> string option,
-    builtin_func: string * typ -> term list -> (string * term list) option,
-    builtin_pred: string * typ -> term list -> (string * term list) option,
-    is_builtin_pred: string -> typ -> bool }
-  val add_builtins: builtins -> Context.generic -> Context.generic
-  val add_logic: (term list -> string option) -> Context.generic ->
+  val smtlibC: SMT_Config.class
+  val add_logic: int * (term list -> string option) -> Context.generic ->
     Context.generic
-  val extra_norm: SMT_Normalize.extra_norm
+  val setup: theory -> theory
   val interface: SMT_Solver.interface
 end
 
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
 struct
 
+structure B = SMT_Builtin
 structure N = SMT_Normalize
 structure T = SMT_Translate
 
+val smtlibC = ["smtlib"]
 
 
-(** facts about uninterpreted constants **)
+
+(* facts about uninterpreted constants *)
 
 infix 2 ??
 fun (ex ?? f) irules = irules |> exists (ex o Thm.prop_of o snd) irules ? f
 
 
-(* pairs *)
+(** pairs **)
 
 val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
 
@@ -43,7 +40,7 @@
 val add_pair_rules = exists_pair_type ?? append (map (pair ~1) pair_rules)
 
 
-(* function update *)
+(** function update **)
 
 val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
 
@@ -53,7 +50,7 @@
 val add_fun_upd_rules = exists_fun_upd ?? append (map (pair ~1) fun_upd_rules)
 
 
-(* abs/min/max *)
+(** abs/min/max **)
 
 val exists_abs_min_max = Term.exists_subterm (fn
     Const (@{const_name abs}, _) => true
@@ -86,7 +83,7 @@
   else thm
 
 
-(* include additional facts *)
+(** include additional facts **)
 
 fun extra_norm has_datatypes irules ctxt =
   irules
@@ -97,121 +94,49 @@
 
 
 
-(** builtins **)
-
-(* additional builtins *)
-
-type builtins = {
-  builtin_typ: typ -> string option,
-  builtin_num: typ -> int -> string option,
-  builtin_func: string * typ -> term list -> (string * term list) option,
-  builtin_pred: string * typ -> term list -> (string * term list) option,
-  is_builtin_pred: string -> typ -> bool }
+(* builtins *)
 
-fun chained _ [] = NONE
-  | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
-
-fun chained' _ [] = false
-  | chained' f (b :: bs) = f b orelse chained' f bs
-
-fun chained_builtin_typ bs T =
-  chained (fn {builtin_typ, ...} : builtins => builtin_typ T) bs
-
-fun chained_builtin_num bs T i =
-  chained (fn {builtin_num, ...} : builtins => builtin_num T i) bs
-
-fun chained_builtin_func bs c ts =
-  chained (fn {builtin_func, ...} : builtins => builtin_func c ts) bs
+local
+  fun int_num _ i = SOME (string_of_int i)
 
-fun chained_builtin_pred bs c ts =
-  chained (fn {builtin_pred, ...} : builtins => builtin_pred c ts) bs
-
-fun chained_is_builtin_pred bs n T =
-  chained' (fn {is_builtin_pred, ...} : builtins => is_builtin_pred n T) bs
-
-fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
-
-structure Builtins = Generic_Data
-(
-  type T = (int * builtins) list
-  val empty = []
-  val extend = I
-  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
-)
-
-fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs))
-
-fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
-
-
-(* basic builtins combined with additional builtins *)
-
-fun builtin_typ _ @{typ int} = SOME "Int"
-  | builtin_typ ctxt T = chained_builtin_typ (get_builtins ctxt) T
-
-fun builtin_num _ @{typ int} i = SOME (string_of_int i)
-  | builtin_num ctxt T i = chained_builtin_num (get_builtins ctxt) T i
+  fun distinct _ _ [t] =
+        (case try HOLogic.dest_list t of
+          SOME (ts as _ :: _) => SOME ("distinct", ts)
+        | _ => NONE)
+    | distinct _ _ _ = NONE
+in
 
-fun if_int_type T n =
-  (case try Term.domain_type T of
-    SOME @{typ int} => SOME n
-  | _ => NONE)
-
-fun conn @{const_name True} = SOME "true"
-  | conn @{const_name False} = SOME "false"
-  | conn @{const_name Not} = SOME "not"
-  | conn @{const_name HOL.conj} = SOME "and"
-  | conn @{const_name HOL.disj} = SOME "or"
-  | conn @{const_name HOL.implies} = SOME "implies"
-  | conn @{const_name HOL.eq} = SOME "iff"
-  | conn @{const_name If} = SOME "if_then_else"
-  | conn _ = NONE
-
-fun distinct_pred (@{const_name distinct}, _) [t] =
-      try HOLogic.dest_list t |> Option.map (pair "distinct")
-  | distinct_pred _ _ = NONE
-
-fun pred @{const_name HOL.eq} _ = SOME "="
-  | pred @{const_name term_eq} _ = SOME "="
-  | pred @{const_name less} T = if_int_type T "<"
-  | pred @{const_name less_eq} T = if_int_type T "<="
-  | pred _ _ = NONE
+val setup =
+  B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
+  fold (B.add_builtin_fun' smtlibC) [
+    (@{const True}, "true"),
+    (@{const False}, "false"),
+ (* FIXME: we do not test if these constants are fully applied! *)
+    (@{const Not}, "not"),
+    (@{const HOL.conj}, "and"),
+    (@{const HOL.disj}, "or"),
+    (@{const HOL.implies}, "implies"),
+    (@{const HOL.eq (bool)}, "iff"),
+    (@{const HOL.eq ('a)}, "="),
+    (@{const If (bool)}, "if_then_else"),
+    (@{const If ('a)}, "ite"),
+    (@{const less (int)}, "<"),
+    (@{const less_eq (int)}, "<="),
+    (@{const uminus (int)}, "~"),
+    (@{const plus (int)}, "+"),
+    (@{const minus (int)}, "-"),
+    (@{const times (int)}, "*") ] #>
+  B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
 
-fun func @{const_name If} _ = SOME "ite"
-  | func @{const_name uminus} T = if_int_type T "~"
-  | func @{const_name plus} T = if_int_type T "+"
-  | func @{const_name minus} T = if_int_type T "-"
-  | func @{const_name times} T = if_int_type T "*"
-  | func _ _ = NONE
-
-val is_propT = (fn @{typ prop} => true | _ => false)
-fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
-fun is_predT T = is_propT (Term.body_type T)
-
-fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
-fun is_builtin_pred ctxt (n, T) = is_predT T andalso
-  (is_some (pred n T) orelse chained_is_builtin_pred (get_builtins ctxt) n T)
-
-fun builtin_fun ctxt (c as (n, T)) ts =
-  let
-    val builtin_func' = chained_builtin_func (get_builtins ctxt)
-    fun builtin_pred' c ts =
-      (case distinct_pred c ts of
-        SOME b => SOME b
-      | NONE => chained_builtin_pred (get_builtins ctxt) c ts)
-  in
-    if is_connT T then conn n |> Option.map (rpair ts)
-    else if is_predT T then
-      (case pred n T of SOME c' => SOME (c', ts) | NONE => builtin_pred' c ts)
-    else 
-      (case func n T of SOME c' => SOME (c', ts) | NONE => builtin_func' c ts)
-  end
+end
 
 
 
-(** serialization **)
+(* serialization *)
 
-(* header *)
+(** header **)
+
+fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
 
 structure Logics = Generic_Data
 (
@@ -221,13 +146,13 @@
   fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
 )
 
-fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l))
+fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
 
 fun choose_logic ctxt ts =
   let
     fun choose [] = "AUFLIA"
-      | choose ((_, l) :: ls) = (case l ts of SOME s => s | NONE => choose ls)
-  in [":logic " ^ choose (rev (Logics.get (Context.Proof ctxt)))] end
+      | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
+  in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
 
 
 (* serialization *)
@@ -294,21 +219,15 @@
 (** interfaces **)
 
 val interface = {
+  class = smtlibC,
   extra_norm = extra_norm,
   translate = {
     prefixes = {
       sort_prefix = "S",
       func_prefix = "f"},
     header = choose_logic,
-    strict = SOME {
-      is_builtin_conn = is_builtin_conn,
-      is_builtin_pred = is_builtin_pred,
-      is_builtin_distinct = true},
-    builtins = {
-      builtin_typ = builtin_typ,
-      builtin_num = builtin_num,
-      builtin_fun = builtin_fun,
-      has_datatypes = false},
+    is_fol = true,
+    has_datatypes = false,
     serialize = serialize}}
 
 end
diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Dec 07 14:53:12 2010 +0100
@@ -6,8 +6,8 @@
 
 signature Z3_INTERFACE =
 sig
-  type builtin_fun = string * typ -> term list -> (string * term list) option
-  val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic
+  val smtlib_z3C: SMT_Config.class
+  val setup: theory -> theory
   val interface: SMT_Solver.interface
 
   datatype sym = Sym of string * sym list
@@ -27,45 +27,17 @@
 struct
 
 structure U = SMT_Utils
-
-
-(** Z3-specific builtins **)
-
-type builtin_fun = string * typ -> term list -> (string * term list) option
-
-fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
+structure B = SMT_Builtin
 
-structure Builtins = Generic_Data
-(
-  type T = (int * builtin_fun) list
-  val empty = []
-  val extend = I
-  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
-)
-
-fun add_builtin_funs b =
-  Builtins.map (Ord_List.insert fst_int_ord (serial (), b))
-
-fun get_builtin_funs ctxt c ts =
-  let
-    fun chained [] = NONE
-      | chained (b :: bs) = (case b c ts of SOME x => SOME x | _ => chained bs)
-  in chained (map snd (Builtins.get (Context.Proof ctxt))) end
-
-fun z3_builtin_fun builtin_fun ctxt c ts =
-  (case builtin_fun ctxt c ts of
-    SOME x => SOME x
-  | _ => get_builtin_funs ctxt c ts)
+val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
 
 
 
-(** interface **)
+(* interface *)
 
 local
-  val {translate, ...} = SMTLIB_Interface.interface
-  val {prefixes, strict, header, builtins, serialize} = translate
-  val {is_builtin_pred, ...}= the strict
-  val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
+  val {translate, extra_norm, ...} = SMTLIB_Interface.interface
+  val {prefixes, is_fol, header, serialize, ...} = translate
 
   fun is_int_div_mod @{const div (int)} = true
     | is_int_div_mod @{const mod (int)} = true
@@ -76,45 +48,33 @@
     then [(~1, @{thm div_by_z3div}), (~1, @{thm mod_by_z3mod})] @ irules
     else irules
 
-  fun extra_norm' has_datatypes =
-    SMTLIB_Interface.extra_norm has_datatypes o add_div_mod
-
-  fun z3_builtin_fun' _ (@{const_name z3div}, _) ts = SOME ("div", ts)
-    | z3_builtin_fun' _ (@{const_name z3mod}, _) ts = SOME ("mod", ts)
-    | z3_builtin_fun' ctxt c ts = z3_builtin_fun builtin_fun ctxt c ts
-
-  val as_propT = (fn @{typ bool} => @{typ prop} | T => T)
+  fun extra_norm' has_datatypes = extra_norm has_datatypes o add_div_mod
 in
 
-fun is_builtin_num ctxt (T, i) = is_some (builtin_num ctxt T i)
-
-fun is_builtin_fun ctxt (c as (n, T)) ts =
-  is_some (z3_builtin_fun' ctxt c ts) orelse 
-  is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->))
+val setup =
+  B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
+  B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
 
 val interface = {
+  class = smtlib_z3C,
   extra_norm = extra_norm',
   translate = {
     prefixes = prefixes,
-    strict = strict,
+    is_fol = is_fol,
     header = header,
-    builtins = {
-      builtin_typ = builtin_typ,
-      builtin_num = builtin_num,
-      builtin_fun = z3_builtin_fun',
-      has_datatypes = true},
+    has_datatypes = true,
     serialize = serialize}}
 
 end
 
 
 
-(** constructors **)
+(* constructors *)
 
 datatype sym = Sym of string * sym list
 
 
-(* additional constructors *)
+(** additional constructors **)
 
 type mk_builtins = {
   mk_builtin_typ: sym -> typ option,
@@ -135,6 +95,8 @@
   let val thy = ProofContext.theory_of ctxt
   in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end
 
+fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
+
 structure Mk_Builtins = Generic_Data
 (
   type T = (int * mk_builtins) list
@@ -149,7 +111,7 @@
 fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
 
 
-(* basic and additional constructors *)
+(** basic and additional constructors **)
 
 fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
   | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
@@ -241,14 +203,13 @@
 
 
 
-(** abstraction **)
+(* abstraction *)
 
 fun is_builtin_theory_term ctxt t =
-  (case try HOLogic.dest_number t of
-    SOME n => is_builtin_num ctxt n
-  | NONE =>
-      (case Term.strip_comb t of
-        (Const c, ts) => is_builtin_fun ctxt c ts
-      | _ => false))
+  if B.is_builtin_num ctxt t then true
+  else
+    (case Term.strip_comb t of
+      (Const c, ts) => B.is_builtin_fun ctxt c ts
+    | _ => false)
 
 end
diff -r 42e0a0bfef73 -r d2b1fc1b8e19 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Dec 07 14:53:12 2010 +0100
@@ -135,7 +135,7 @@
    @{const_name HOL.eq}]
 
 fun is_built_in_const_for_prover ctxt name (s, T) =
-  if is_smt_prover ctxt name then SMT_Builtin.is_builtin ctxt (s, T)
+  if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) [] (*FIXME*)
   else member (op =) atp_irrelevant_consts s
 
 (* FUDGE *)