centralized handling of built-in types and constants;
authorboehmes
Tue Dec 07 14:53:12 2010 +0100 (2010-12-07)
changeset 41059d2b1fc1b8e19
parent 41058 42e0a0bfef73
child 41060 4199fdcfa3c0
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)
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
     1.1 --- a/src/HOL/SMT.thy	Mon Dec 06 16:54:22 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Tue Dec 07 14:53:12 2010 +0100
     1.3 @@ -105,16 +105,18 @@
     1.4  subsection {* First-order logic *}
     1.5  
     1.6  text {*
     1.7 -Some SMT solvers require a strict separation between formulas and
     1.8 -terms.  When translating higher-order into first-order problems,
     1.9 -all uninterpreted constants (those not builtin in the target solver)
    1.10 +Some SMT solvers only accept problems in first-order logic, i.e.,
    1.11 +where formulas and terms are syntactically separated. When
    1.12 +translating higher-order into first-order problems, all
    1.13 +uninterpreted constants (those not built-in in the target solver)
    1.14  are treated as function symbols in the first-order sense.  Their
    1.15 -occurrences as head symbols in atoms (i.e., as predicate symbols) is
    1.16 -turned into terms by equating such atoms with @{term True} using the
    1.17 -following term-level equation symbol.
    1.18 +occurrences as head symbols in atoms (i.e., as predicate symbols) are
    1.19 +turned into terms by equating such atoms with @{term True}.
    1.20 +Whenever the boolean type occurs in first-order terms, it is replaced
    1.21 +by the following type.
    1.22  *}
    1.23  
    1.24 -definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
    1.25 +typedecl term_bool
    1.26  
    1.27  
    1.28  
    1.29 @@ -159,7 +161,10 @@
    1.30  
    1.31  setup {*
    1.32    SMT_Config.setup #>
    1.33 +  SMT_Normalize.setup #>
    1.34    SMT_Solver.setup #>
    1.35 +  SMTLIB_Interface.setup #>
    1.36 +  Z3_Interface.setup #>
    1.37    Z3_Proof_Reconstruction.setup #>
    1.38    SMT_Setup_Solvers.setup
    1.39  *}
    1.40 @@ -354,9 +359,10 @@
    1.41  
    1.42  
    1.43  
    1.44 +hide_type term_bool
    1.45  hide_type (open) pattern
    1.46 -hide_const Pattern term_eq
    1.47 -hide_const (open) trigger pat nopat weight fun_app z3div z3mod
    1.48 +hide_const Pattern fun_app
    1.49 +hide_const (open) trigger pat nopat weight z3div z3mod
    1.50  
    1.51  
    1.52  
     2.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Mon Dec 06 16:54:22 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Dec 07 14:53:12 2010 +0100
     2.3 @@ -1,116 +1,226 @@
     2.4  (*  Title:      HOL/Tools/SMT/smt_builtin.ML
     2.5      Author:     Sascha Boehme, TU Muenchen
     2.6  
     2.7 -Crafted collection of SMT built-in symbols.
     2.8 -
     2.9 -FIXME: This list is currently not automatically kept synchronized with the
    2.10 -remaining implementation.
    2.11 +Tables of types and terms directly supported by SMT solvers.
    2.12  *)
    2.13  
    2.14  signature SMT_BUILTIN =
    2.15  sig
    2.16 -  val is_builtin: Proof.context -> string * typ -> bool
    2.17 -  val is_partially_builtin: Proof.context -> string * typ -> bool
    2.18 +  (*built-in types*)
    2.19 +  val add_builtin_typ: SMT_Config.class ->
    2.20 +    typ * (typ -> string option) * (typ -> int -> string option) -> theory ->
    2.21 +    theory
    2.22 +  val add_builtin_typ_ext: typ * (typ -> bool) -> theory -> theory
    2.23 +  val builtin_typ: Proof.context -> typ -> string option
    2.24 +  val is_builtin_typ: Proof.context -> typ -> bool
    2.25 +  val is_builtin_typ_ext: Proof.context -> typ -> bool
    2.26 +
    2.27 +  (*built-in numbers*)
    2.28 +  val builtin_num: Proof.context -> term -> string option
    2.29 +  val is_builtin_num: Proof.context -> term -> bool
    2.30 +  val is_builtin_num_ext: Proof.context -> term -> bool
    2.31 +
    2.32 +  (*built-in functions*)
    2.33 +  type 'a bfun = Proof.context -> typ -> term list -> 'a
    2.34 +  val add_builtin_fun: SMT_Config.class ->
    2.35 +    (string * typ) * (string * term list) option bfun -> theory -> theory
    2.36 +  val add_builtin_fun': SMT_Config.class -> term * string -> theory -> theory
    2.37 +  val add_builtin_fun_ext: (string * typ) * bool bfun -> theory -> theory
    2.38 +  val add_builtin_fun_ext': string * typ -> theory -> theory
    2.39 +  val add_builtin_fun_ext'': string -> theory -> theory
    2.40 +  val builtin_fun: Proof.context -> string * typ -> term list ->
    2.41 +    (string * term list) option
    2.42 +  val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
    2.43 +  val is_builtin_pred: Proof.context -> string * typ -> term list -> bool
    2.44 +  val is_builtin_conn: Proof.context -> string * typ -> term list -> bool
    2.45 +  val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
    2.46  end
    2.47  
    2.48  structure SMT_Builtin: SMT_BUILTIN =
    2.49  struct
    2.50  
    2.51 -fun is_arithT T =
    2.52 -  (case T of
    2.53 -     @{typ int} => true
    2.54 -   | @{typ nat} => true
    2.55 -   | Type ("RealDef.real", []) => true
    2.56 -   | _ => false)
    2.57 +structure C = SMT_Config
    2.58 +
    2.59 +
    2.60 +(* built-in tables *)
    2.61 +
    2.62 +datatype ('a, 'b) kind = Ext of 'a | Int of 'b
    2.63 +
    2.64 +type ('a, 'b) ttab = (C.class * (typ * ('a, 'b) kind) Ord_List.T) list 
    2.65  
    2.66 -fun is_arithT_dom (Type (@{type_name fun}, [T, _])) = is_arithT T
    2.67 -  | is_arithT_dom _ = false
    2.68 -fun is_arithT_ran (Type (@{type_name fun}, [_, T])) = is_arithT T
    2.69 -  | is_arithT_ran _ = false
    2.70 +fun empty_ttab () = []
    2.71  
    2.72 -val builtins = Symtab.make [
    2.73 -
    2.74 -  (* Pure constants *)
    2.75 -  (@{const_name all}, K true),
    2.76 -  (@{const_name "=="}, K true),
    2.77 -  (@{const_name "==>"}, K true),
    2.78 -  (@{const_name Trueprop}, K true),
    2.79 +fun typ_ord ((T, _), (U, _)) =
    2.80 +  let
    2.81 +    fun tord (TVar _, Type _) = GREATER
    2.82 +      | tord (Type _, TVar _) = LESS
    2.83 +      | tord (Type (n, Ts), Type (m, Us)) =
    2.84 +          if n = m then list_ord tord (Ts, Us)
    2.85 +          else Term_Ord.typ_ord (T, U)
    2.86 +      | tord TU = Term_Ord.typ_ord TU
    2.87 +  in tord (T, U) end
    2.88  
    2.89 -  (* logical constants *)
    2.90 -  (@{const_name All}, K true),
    2.91 -  (@{const_name Ex}, K true),
    2.92 -  (@{const_name Ball}, K true),
    2.93 -  (@{const_name Bex}, K true),
    2.94 -  (@{const_name Ex1}, K true),
    2.95 -  (@{const_name True}, K true),
    2.96 -  (@{const_name False}, K true),
    2.97 -  (@{const_name Not}, K true),
    2.98 -  (@{const_name HOL.conj}, K true),
    2.99 -  (@{const_name HOL.disj}, K true),
   2.100 -  (@{const_name HOL.implies}, K true),
   2.101 +fun insert_ttab cs T f =
   2.102 +  AList.map_default (op =) (cs, [])
   2.103 +    (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
   2.104 +
   2.105 +fun merge_ttab ttabp =
   2.106 +  AList.join (op =) (K (uncurry (Ord_List.union typ_ord) o swap)) ttabp
   2.107  
   2.108 -  (* term abbreviations *)
   2.109 -  (@{const_name If}, K true),
   2.110 -  (@{const_name bool.bool_case}, K true),
   2.111 -  (@{const_name Let}, K true),
   2.112 -  (* (@{const_name distinct}, K true),  -- not a real builtin, only when
   2.113 -                                           applied to an explicit list *)
   2.114 +fun lookup_ttab ctxt ttab T =
   2.115 +  let
   2.116 +    val cs = C.solver_class_of ctxt
   2.117 +    fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)
   2.118 +
   2.119 +    fun matching (cs', Txs) =
   2.120 +      if is_prefix (op =) cs' cs then find_first match Txs
   2.121 +      else NONE
   2.122 +  in get_first matching ttab end
   2.123 +
   2.124 +type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
   2.125 +
   2.126 +fun empty_btab () = Symtab.empty
   2.127  
   2.128 -  (* technicalities *)
   2.129 -  (@{const_name SMT.pat}, K true),
   2.130 -  (@{const_name SMT.nopat}, K true),
   2.131 -  (@{const_name SMT.trigger}, K true),
   2.132 -  (@{const_name SMT.weight}, K true),
   2.133 -  (@{const_name SMT.fun_app}, K true),
   2.134 -  (@{const_name SMT.z3div}, K true),
   2.135 -  (@{const_name SMT.z3mod}, K true),
   2.136 +fun insert_btab cs n T f =
   2.137 +  Symtab.map_default (n, []) (insert_ttab cs T f)
   2.138 +
   2.139 +fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
   2.140  
   2.141 -  (* equality *)
   2.142 -  (@{const_name HOL.eq}, K true),
   2.143 +fun lookup_btab ctxt btab (n, T) =
   2.144 +  (case Symtab.lookup btab n of
   2.145 +    NONE => NONE
   2.146 +  | SOME ttab => lookup_ttab ctxt ttab T)
   2.147  
   2.148 -  (* numerals *)
   2.149 -  (@{const_name zero_class.zero}, is_arithT),
   2.150 -  (@{const_name one_class.one}, is_arithT),
   2.151 -  (@{const_name Int.Pls}, K true),
   2.152 -  (@{const_name Int.Min}, K true),
   2.153 -  (@{const_name Int.Bit0}, K true),
   2.154 -  (@{const_name Int.Bit1}, K true),
   2.155 -  (@{const_name number_of}, is_arithT_ran),
   2.156 +
   2.157 +(* built-in types *)
   2.158  
   2.159 -  (* arithmetic *)
   2.160 -  (@{const_name nat}, K true),
   2.161 -  (@{const_name of_nat}, K true),
   2.162 -  (@{const_name Suc}, K true),
   2.163 -  (@{const_name plus}, is_arithT_dom),
   2.164 -  (@{const_name uminus}, is_arithT_dom),
   2.165 -  (@{const_name minus}, is_arithT_dom),
   2.166 -  (@{const_name abs}, is_arithT_dom),
   2.167 -  (@{const_name min}, is_arithT_dom),
   2.168 -  (@{const_name max}, is_arithT_dom),
   2.169 -  (@{const_name less}, is_arithT_dom),
   2.170 -  (@{const_name less_eq}, is_arithT_dom),
   2.171 -  
   2.172 -  (* pairs *)
   2.173 -  (@{const_name fst}, K true),
   2.174 -  (@{const_name snd}, K true),
   2.175 -  (@{const_name Pair}, K true)
   2.176 +structure Builtin_Types = Theory_Data
   2.177 +(
   2.178 +  type T =
   2.179 +    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
   2.180 +  val empty = empty_ttab ()
   2.181 +  val extend = I
   2.182 +  val merge = merge_ttab
   2.183 +)
   2.184 +
   2.185 +fun add_builtin_typ cs (T, f, g) =
   2.186 +  Builtin_Types.map (insert_ttab cs T (Int (f, g)))
   2.187 +
   2.188 +fun add_builtin_typ_ext (T, f) =
   2.189 +  Builtin_Types.map (insert_ttab C.basicC T (Ext f))
   2.190  
   2.191 -  ]
   2.192 +fun lookup_builtin_typ ctxt =
   2.193 +  lookup_ttab ctxt (Builtin_Types.get (ProofContext.theory_of ctxt))
   2.194  
   2.195 -val all_builtins =
   2.196 -  builtins
   2.197 -  |> Symtab.update (@{const_name times}, is_arithT_dom)
   2.198 -  |> Symtab.update (@{const_name div_class.div}, is_arithT_dom)
   2.199 -  |> Symtab.update (@{const_name div_class.mod}, is_arithT_dom)
   2.200 -  |> Symtab.update ("Rings.inverse_class.divide", is_arithT_dom)
   2.201 +fun builtin_typ ctxt T =
   2.202 +  (case lookup_builtin_typ ctxt T of
   2.203 +    SOME (_, Int (f, _)) => f T
   2.204 +  | _ => NONE) 
   2.205  
   2.206 -fun lookup_builtin bs (name, T) =
   2.207 -  (case Symtab.lookup bs name of
   2.208 -    SOME proper_type => proper_type T
   2.209 +fun is_builtin_typ ctxt T = is_some (builtin_typ ctxt T)
   2.210 +
   2.211 +fun is_builtin_typ_ext ctxt T =
   2.212 +  (case lookup_builtin_typ ctxt T of
   2.213 +    SOME (_, Int (f, _)) => is_some (f T)
   2.214 +  | SOME (_, Ext f) => f T
   2.215    | NONE => false)
   2.216  
   2.217 -fun is_builtin _ = lookup_builtin builtins
   2.218 +
   2.219 +(* built-in numbers *)
   2.220 +
   2.221 +fun builtin_num ctxt t =
   2.222 +  (case try HOLogic.dest_number t of
   2.223 +    NONE => NONE
   2.224 +  | SOME (T, i) =>
   2.225 +      (case lookup_builtin_typ ctxt T of
   2.226 +        SOME (_, Int (_, g)) => g T i
   2.227 +      | _ => NONE))
   2.228 +
   2.229 +val is_builtin_num = is_some oo builtin_num
   2.230 +
   2.231 +fun is_builtin_num_ext ctxt t =
   2.232 +  (case try HOLogic.dest_number t of
   2.233 +    NONE => false
   2.234 +  | SOME (T, _) => is_builtin_typ_ext ctxt T)
   2.235 +
   2.236 +
   2.237 +(* built-in functions *)
   2.238 +
   2.239 +type 'a bfun = Proof.context -> typ -> term list -> 'a
   2.240 +
   2.241 +fun true3 _ _ _ = true
   2.242 +
   2.243 +fun raw_add_builtin_fun_ext thy cs n =
   2.244 +  insert_btab cs n (Sign.the_const_type thy n) (Ext true3)
   2.245 +
   2.246 +val basic_builtin_fun_names = [
   2.247 +  @{const_name SMT.pat}, @{const_name SMT.nopat},
   2.248 +  @{const_name SMT.trigger}, @{const_name SMT.weight}]
   2.249 +
   2.250 +fun basic_builtin_funcs () =
   2.251 +  empty_btab ()
   2.252 +  |> fold (raw_add_builtin_fun_ext @{theory} C.basicC) basic_builtin_fun_names
   2.253 +       (* FIXME: SMT_Normalize should check that they are properly used *)
   2.254 +
   2.255 +structure Builtin_Funcs = Theory_Data
   2.256 +(
   2.257 +  type T = (bool bfun, (string * term list) option bfun) btab
   2.258 +  val empty = basic_builtin_funcs ()
   2.259 +  val extend = I
   2.260 +  val merge = merge_btab
   2.261 +)
   2.262 +
   2.263 +fun add_builtin_fun cs ((n, T), f) =
   2.264 +  Builtin_Funcs.map (insert_btab cs n T (Int f))
   2.265  
   2.266 -fun is_partially_builtin _ = lookup_builtin all_builtins
   2.267 +fun add_builtin_fun' cs (t, n) =
   2.268 +  add_builtin_fun cs (Term.dest_Const t, fn _ => fn _ => SOME o pair n)
   2.269 +
   2.270 +fun add_builtin_fun_ext ((n, T), f) =
   2.271 +  Builtin_Funcs.map (insert_btab C.basicC n T (Ext f))
   2.272 +
   2.273 +fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, true3)
   2.274 +
   2.275 +fun add_builtin_fun_ext'' n thy =
   2.276 +  add_builtin_fun_ext' (n, Sign.the_const_type thy n) thy
   2.277 +
   2.278 +fun lookup_builtin_fun ctxt =
   2.279 +  lookup_btab ctxt (Builtin_Funcs.get (ProofContext.theory_of ctxt))
   2.280 +
   2.281 +fun builtin_fun ctxt (c as (_, T)) ts =
   2.282 +  (case lookup_builtin_fun ctxt c of
   2.283 +    SOME (_, Int f) => f ctxt T ts
   2.284 +  | _ => NONE)
   2.285 +
   2.286 +fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts)
   2.287 +
   2.288 +fun is_special_builtin_fun pred ctxt (c as (_, T)) ts =
   2.289 +  (case lookup_builtin_fun ctxt c of
   2.290 +    SOME (U, Int f) => pred U andalso is_some (f ctxt T ts)
   2.291 +  | _ => false)
   2.292 +
   2.293 +fun is_pred_type T = Term.body_type T = @{typ bool}
   2.294 +fun is_conn_type T =
   2.295 +  forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
   2.296 +
   2.297 +fun is_builtin_pred ctxt = is_special_builtin_fun is_pred_type ctxt
   2.298 +fun is_builtin_conn ctxt = is_special_builtin_fun is_conn_type ctxt
   2.299 +
   2.300 +fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
   2.301 +  (case lookup_builtin_fun ctxt c of
   2.302 +    SOME (_, Int f) => is_some (f ctxt T ts)
   2.303 +  | SOME (_, Ext f) => f ctxt T ts
   2.304 +  | NONE => false)
   2.305 +
   2.306 +(* FIXME: move this information to the interfaces *)
   2.307 +val only_partially_supported = [
   2.308 +  @{const_name times},
   2.309 +  @{const_name div_class.div},
   2.310 +  @{const_name div_class.mod},
   2.311 +  @{const_name inverse_class.divide} ]
   2.312 +
   2.313 +fun is_builtin_ext ctxt (c as (n, _)) ts =
   2.314 +  if member (op =) only_partially_supported n then false
   2.315 +  else is_builtin_fun_ext ctxt c ts
   2.316  
   2.317  end
     3.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Mon Dec 06 16:54:22 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Dec 07 14:53:12 2010 +0100
     3.3 @@ -6,11 +6,16 @@
     3.4  
     3.5  signature SMT_CONFIG =
     3.6  sig
     3.7 +  (*class*)
     3.8 +  type class = string list
     3.9 +  val basicC: class
    3.10 +
    3.11    (*solver*)
    3.12 -  val add_solver: string -> Context.generic -> Context.generic
    3.13 +  val add_solver: string * class -> Context.generic -> Context.generic
    3.14    val set_solver_options: string * string -> Context.generic -> Context.generic
    3.15    val select_solver: string -> Context.generic -> Context.generic
    3.16    val solver_of: Proof.context -> string
    3.17 +  val solver_class_of: Proof.context -> class
    3.18    val solver_options_of: Proof.context -> string list
    3.19  
    3.20    (*options*)
    3.21 @@ -46,11 +51,18 @@
    3.22  structure SMT_Config: SMT_CONFIG =
    3.23  struct
    3.24  
    3.25 +(* class *)
    3.26 +
    3.27 +type class = string list
    3.28 +
    3.29 +val basicC = []
    3.30 +
    3.31 +
    3.32  (* solver *)
    3.33  
    3.34  structure Solvers = Generic_Data
    3.35  (
    3.36 -  type T = string list Symtab.table * string option
    3.37 +  type T = (class * string list) Symtab.table * string option
    3.38    val empty = (Symtab.empty, NONE)
    3.39    val extend = I
    3.40    fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
    3.41 @@ -58,14 +70,14 @@
    3.42  
    3.43  fun set_solver_options (name, options) =
    3.44    let val opts = String.tokens (Symbol.is_ascii_blank o str) options
    3.45 -  in Solvers.map (apfst (Symtab.map_entry name (K opts))) end
    3.46 +  in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
    3.47  
    3.48 -fun add_solver name context =
    3.49 +fun add_solver (name, class) context =
    3.50    if Symtab.defined (fst (Solvers.get context)) name then
    3.51      error ("Solver already registered: " ^ quote name)
    3.52    else
    3.53      context
    3.54 -    |> Solvers.map (apfst (Symtab.update (name, [])))
    3.55 +    |> Solvers.map (apfst (Symtab.update (name, (class, []))))
    3.56      |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
    3.57          (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
    3.58            (Thm.declaration_attribute o K o set_solver_options o pair name))
    3.59 @@ -76,18 +88,23 @@
    3.60      Solvers.map (apsnd (K (SOME name))) context
    3.61    else error ("Trying to select unknown solver: " ^ quote name)
    3.62  
    3.63 -val lookup_solver = snd o Solvers.get o Context.Proof
    3.64 +fun no_solver_err () = error "No SMT solver selected"
    3.65  
    3.66  fun solver_of ctxt =
    3.67 -  (case lookup_solver ctxt of
    3.68 -    SOME name => name
    3.69 -  | NONE => error "No SMT solver selected")
    3.70 +  (case Solvers.get (Context.Proof ctxt) of
    3.71 +    (_, SOME name) => name
    3.72 +  | (_, NONE) => no_solver_err ())
    3.73 +
    3.74 +fun solver_class_of ctxt =
    3.75 +  (case Solvers.get (Context.Proof ctxt) of
    3.76 +    (solvers, SOME name) => fst (the (Symtab.lookup solvers name))
    3.77 +  | (_, NONE) => no_solver_err())
    3.78  
    3.79  fun solver_options_of ctxt =
    3.80 -  (case lookup_solver ctxt of
    3.81 -    NONE => []
    3.82 -  | SOME name =>
    3.83 -      Symtab.lookup_list (fst (Solvers.get (Context.Proof ctxt))) name)
    3.84 +  (case Solvers.get (Context.Proof ctxt) of
    3.85 +    (solvers, SOME name) =>
    3.86 +      (case Symtab.lookup solvers name of SOME (_, opts) => opts | NONE => [])
    3.87 +  | (_, NONE) => [])
    3.88  
    3.89  val setup_solver =
    3.90    Attrib.setup @{binding smt_solver}
     4.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Dec 06 16:54:22 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 07 14:53:12 2010 +0100
     4.3 @@ -23,12 +23,14 @@
     4.4      (int * thm) list * Proof.context
     4.5    val atomize_conv: Proof.context -> conv
     4.6    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
     4.7 +  val setup: theory -> theory
     4.8  end
     4.9  
    4.10  structure SMT_Normalize: SMT_NORMALIZE =
    4.11  struct
    4.12  
    4.13  structure U = SMT_Utils
    4.14 +structure B = SMT_Builtin
    4.15  
    4.16  infix 2 ??
    4.17  fun (test ?? f) x = if test x then f x else x
    4.18 @@ -95,6 +97,9 @@
    4.19  fun rewrite_bool_cases ctxt =
    4.20    map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    4.21      Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt)))
    4.22 +
    4.23 +val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
    4.24 +
    4.25  end
    4.26  
    4.27  
    4.28 @@ -203,10 +208,20 @@
    4.29    val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
    4.30    val uses_nat_int = Term.exists_subterm (member (op aconv)
    4.31      [@{const of_nat (int)}, @{const nat}])
    4.32 +
    4.33 +  val nat_ops = [
    4.34 +    @{const less (nat)}, @{const less_eq (nat)},
    4.35 +    @{const Suc}, @{const plus (nat)}, @{const minus (nat)},
    4.36 +    @{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
    4.37 +  val nat_ops' = @{const of_nat (int)} :: @{const nat} :: nat_ops
    4.38  in
    4.39  fun nat_as_int ctxt =
    4.40    map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
    4.41    exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding
    4.42 +
    4.43 +val setup_nat_as_int =
    4.44 +  B.add_builtin_typ_ext (@{typ nat}, K true) #>
    4.45 +  fold (B.add_builtin_fun_ext' o Term.dest_Const) nat_ops'
    4.46  end
    4.47  
    4.48  
    4.49 @@ -263,7 +278,7 @@
    4.50      | _ =>
    4.51          (case Term.strip_comb (Thm.term_of ct) of
    4.52            (Const (c as (_, T)), ts) =>
    4.53 -            if SMT_Builtin.is_partially_builtin ctxt c
    4.54 +            if SMT_Builtin.is_builtin_fun ctxt c ts
    4.55              then eta_args_conv norm_conv
    4.56                (length (Term.binder_types T) - length ts)
    4.57              else args_conv o norm_conv
    4.58 @@ -294,7 +309,7 @@
    4.59      | _ =>
    4.60          (case Term.strip_comb t of
    4.61            (Const (c as (_, T)), ts) =>
    4.62 -            if SMT_Builtin.is_builtin ctxt c
    4.63 +            if SMT_Builtin.is_builtin_fun ctxt c ts
    4.64              then length (Term.binder_types T) = length ts andalso
    4.65                forall (is_normed ctxt) ts
    4.66              else forall (is_normed ctxt) ts
    4.67 @@ -302,6 +317,11 @@
    4.68  in
    4.69  fun norm_binder_conv ctxt =
    4.70    U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
    4.71 +
    4.72 +val setup_unfolded_quants =
    4.73 +  fold B.add_builtin_fun_ext'' [@{const_name Ball}, @{const_name Bex},
    4.74 +    @{const_name Ex1}]
    4.75 +
    4.76  end
    4.77  
    4.78  fun norm_def ctxt thm =
    4.79 @@ -325,6 +345,10 @@
    4.80        Conv.rewr_conv @{thm atomize_all}
    4.81    | _ => Conv.all_conv) ct
    4.82  
    4.83 +val setup_atomize =
    4.84 +  fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
    4.85 +    @{const_name all}, @{const_name Trueprop}]
    4.86 +
    4.87  fun normalize_rule ctxt =
    4.88    Conv.fconv_rule (
    4.89      (* reduce lambda abstractions, except at known binders: *)
    4.90 @@ -554,4 +578,14 @@
    4.91      |-> (if with_datatypes then datatype_selectors else pair)
    4.92    end
    4.93  
    4.94 +
    4.95 +
    4.96 +(* setup *)
    4.97 +
    4.98 +val setup =
    4.99 +  setup_bool_case #>
   4.100 +  setup_nat_as_int #>
   4.101 +  setup_unfolded_quants #>
   4.102 +  setup_atomize
   4.103 +
   4.104  end
     5.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Mon Dec 06 16:54:22 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Tue Dec 07 14:53:12 2010 +0100
     5.3 @@ -12,6 +12,8 @@
     5.4  structure SMT_Real: SMT_REAL =
     5.5  struct
     5.6  
     5.7 +structure B = SMT_Builtin
     5.8 +
     5.9  
    5.10  (* SMT-LIB logic *)
    5.11  
    5.12 @@ -21,58 +23,28 @@
    5.13    else NONE
    5.14  
    5.15  
    5.16 -
    5.17 -(* SMT-LIB builtins *)
    5.18 +(* SMT-LIB and Z3 built-ins *)
    5.19  
    5.20  local
    5.21 -  fun smtlib_builtin_typ @{typ real} = SOME "Real"
    5.22 -    | smtlib_builtin_typ _ = NONE
    5.23 -
    5.24 -  fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
    5.25 -    | smtlib_builtin_num _ _ = NONE
    5.26 +  val smtlibC = SMTLIB_Interface.smtlibC
    5.27  
    5.28 -  fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts)
    5.29 -    | smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts)
    5.30 -    | smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts)
    5.31 -    | smtlib_builtin_func @{const_name times} ts = SOME ("*", ts)
    5.32 -    | smtlib_builtin_func _ _ = NONE
    5.33 -
    5.34 -  fun smtlib_builtin_pred @{const_name less} = SOME "<"
    5.35 -    | smtlib_builtin_pred @{const_name less_eq} = SOME "<="
    5.36 -    | smtlib_builtin_pred _ = NONE
    5.37 -
    5.38 -  fun real_fun T y f x = 
    5.39 -    (case try Term.domain_type T of
    5.40 -      SOME @{typ real} => f x
    5.41 -    | _ => y)
    5.42 +  fun real_num _ i = SOME (string_of_int i ^ ".0")
    5.43  in
    5.44  
    5.45 -val smtlib_builtins = {
    5.46 -  builtin_typ = smtlib_builtin_typ,
    5.47 -  builtin_num = smtlib_builtin_num,
    5.48 -  builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)),
    5.49 -  builtin_pred = (fn (n, T) => fn ts =>
    5.50 -    real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)),
    5.51 -  is_builtin_pred = (fn n => fn T =>
    5.52 -    real_fun T false (is_some o smtlib_builtin_pred) n) }
    5.53 +val setup_builtins =
    5.54 +  B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
    5.55 +  fold (B.add_builtin_fun' smtlibC) [
    5.56 +    (@{const uminus (real)}, "~"),
    5.57 +    (@{const plus (real)}, "+"),
    5.58 +    (@{const minus (real)}, "-"),
    5.59 +    (@{const times (real)}, "*"),
    5.60 +    (@{const less (real)}, "<"),
    5.61 +    (@{const less_eq (real)}, "<=") ] #>
    5.62 +  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
    5.63  
    5.64  end
    5.65  
    5.66  
    5.67 -
    5.68 -(* Z3 builtins *)
    5.69 -
    5.70 -local
    5.71 -  fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
    5.72 -    | z3_builtin_fun _ _ = NONE
    5.73 -in
    5.74 -
    5.75 -val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts)
    5.76 -
    5.77 -end
    5.78 -
    5.79 -
    5.80 -
    5.81  (* Z3 constructors *)
    5.82  
    5.83  local
    5.84 @@ -117,7 +89,6 @@
    5.85  end
    5.86  
    5.87  
    5.88 -
    5.89  (* Z3 proof reconstruction *)
    5.90  
    5.91  val real_rules = @{lemma
    5.92 @@ -132,14 +103,12 @@
    5.93    "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
    5.94  
    5.95  
    5.96 -
    5.97  (* setup *)
    5.98  
    5.99  val setup =
   5.100 +  setup_builtins #>
   5.101    Context.theory_map (
   5.102 -    SMTLIB_Interface.add_logic smtlib_logic #>
   5.103 -    SMTLIB_Interface.add_builtins smtlib_builtins #>
   5.104 -    Z3_Interface.add_builtin_funs z3_builtins #>
   5.105 +    SMTLIB_Interface.add_logic (10, smtlib_logic) #>
   5.106      Z3_Interface.add_mk_builtins z3_mk_builtins #>
   5.107      fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
   5.108      Z3_Proof_Tools.add_simproc real_linarith_proc)
     6.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Dec 06 16:54:22 2010 +0100
     6.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Dec 07 14:53:12 2010 +0100
     6.3 @@ -8,6 +8,7 @@
     6.4  sig
     6.5    (*configuration*)
     6.6    type interface = {
     6.7 +    class: SMT_Config.class,
     6.8      extra_norm: SMT_Normalize.extra_norm,
     6.9      translate: SMT_Translate.config }
    6.10    datatype outcome = Unsat | Sat | Unknown
    6.11 @@ -57,6 +58,7 @@
    6.12  (* configuration *)
    6.13  
    6.14  type interface = {
    6.15 +  class: SMT_Config.class,
    6.16    extra_norm: SMT_Normalize.extra_norm,
    6.17    translate: SMT_Translate.config }
    6.18  
    6.19 @@ -195,13 +197,10 @@
    6.20  
    6.21  fun set_has_datatypes with_datatypes translate =
    6.22    let
    6.23 -    val {prefixes, header, strict, builtins, serialize} = translate
    6.24 -    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
    6.25 +    val {prefixes, header, is_fol, has_datatypes, serialize} = translate
    6.26      val with_datatypes' = has_datatypes andalso with_datatypes
    6.27 -    val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num,
    6.28 -      builtin_fun=builtin_fun, has_datatypes=with_datatypes}
    6.29 -    val translate' = {prefixes=prefixes, header=header, strict=strict,
    6.30 -      builtins=builtins', serialize=serialize}
    6.31 +    val translate' = {prefixes=prefixes, header=header, is_fol=is_fol,
    6.32 +      has_datatypes=with_datatypes', serialize=serialize}
    6.33    in (with_datatypes', translate') end
    6.34  
    6.35  fun trace_assumptions ctxt irules idxs =
    6.36 @@ -219,7 +218,7 @@
    6.37  fun gen_solver name info rm ctxt irules =
    6.38    let
    6.39      val {env_var, is_remote, options, interface, reconstruct, ...} = info
    6.40 -    val {extra_norm, translate} = interface
    6.41 +    val {extra_norm, translate, ...} = interface
    6.42      val (with_datatypes, translate') =
    6.43        set_has_datatypes (Config.get ctxt C.datatypes) translate
    6.44      val cmd = (rm, env_var, is_remote, name)
    6.45 @@ -284,6 +283,7 @@
    6.46    let
    6.47      val {name, env_var, is_remote, options, interface, outcome, cex_parser,
    6.48        reconstruct, default_max_relevant} = cfg
    6.49 +    val {class, ...} = interface
    6.50  
    6.51      fun core_oracle () = cfalse
    6.52  
    6.53 @@ -294,7 +294,7 @@
    6.54    in
    6.55      Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
    6.56      Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
    6.57 -    Context.theory_map (C.add_solver name)
    6.58 +    Context.theory_map (C.add_solver (name, class))
    6.59    end
    6.60  
    6.61  end
     7.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Dec 06 16:54:22 2010 +0100
     7.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Dec 07 14:53:12 2010 +0100
     7.3 @@ -17,17 +17,6 @@
     7.4  
     7.5    (* configuration options *)
     7.6    type prefixes = {sort_prefix: string, func_prefix: string}
     7.7 -  type header = Proof.context -> term list -> string list
     7.8 -  type strict = {
     7.9 -    is_builtin_conn: string * typ -> bool,
    7.10 -    is_builtin_pred: Proof.context -> string * typ -> bool,
    7.11 -    is_builtin_distinct: bool}
    7.12 -  type builtins = {
    7.13 -    builtin_typ: Proof.context -> typ -> string option,
    7.14 -    builtin_num: Proof.context -> typ -> int -> string option,
    7.15 -    builtin_fun: Proof.context -> string * typ -> term list ->
    7.16 -      (string * term list) option,
    7.17 -    has_datatypes: bool }
    7.18    type sign = {
    7.19      header: string list,
    7.20      sorts: string list,
    7.21 @@ -35,9 +24,9 @@
    7.22      funcs: (string * (string list * string)) list }
    7.23    type config = {
    7.24      prefixes: prefixes,
    7.25 -    header: header,
    7.26 -    strict: strict option,
    7.27 -    builtins: builtins,
    7.28 +    header: Proof.context -> term list -> string list,
    7.29 +    is_fol: bool,
    7.30 +    has_datatypes: bool,
    7.31      serialize: string list -> sign -> sterm list -> string }
    7.32    type recon = {
    7.33      typs: typ Symtab.table,
    7.34 @@ -53,6 +42,7 @@
    7.35  struct
    7.36  
    7.37  structure U = SMT_Utils
    7.38 +structure B = SMT_Builtin
    7.39  
    7.40  
    7.41  (* intermediate term structure *)
    7.42 @@ -73,20 +63,6 @@
    7.43  
    7.44  type prefixes = {sort_prefix: string, func_prefix: string}
    7.45  
    7.46 -type header = Proof.context -> term list -> string list
    7.47 -
    7.48 -type strict = {
    7.49 -  is_builtin_conn: string * typ -> bool,
    7.50 -  is_builtin_pred: Proof.context -> string * typ -> bool,
    7.51 -  is_builtin_distinct: bool}
    7.52 -
    7.53 -type builtins = {
    7.54 -  builtin_typ: Proof.context -> typ -> string option,
    7.55 -  builtin_num: Proof.context -> typ -> int -> string option,
    7.56 -  builtin_fun: Proof.context -> string * typ -> term list ->
    7.57 -    (string * term list) option,
    7.58 -  has_datatypes: bool }
    7.59 -
    7.60  type sign = {
    7.61    header: string list,
    7.62    sorts: string list,
    7.63 @@ -95,9 +71,9 @@
    7.64  
    7.65  type config = {
    7.66    prefixes: prefixes,
    7.67 -  header: header,
    7.68 -  strict: strict option,
    7.69 -  builtins: builtins,
    7.70 +  header: Proof.context -> term list -> string list,
    7.71 +  is_fol: bool,
    7.72 +  has_datatypes: bool,
    7.73    serialize: string list -> sign -> sterm list -> string }
    7.74  
    7.75  type recon = {
    7.76 @@ -152,13 +128,20 @@
    7.77  
    7.78  
    7.79  
    7.80 -(* enforce a strict separation between formulas and terms *)
    7.81 +(* map HOL formulas to FOL formulas (i.e., separate formulas froms terms) *)
    7.82  
    7.83 -val term_eq_rewr = @{lemma "term_eq x y == x = y" by (simp add: term_eq_def)}
    7.84 +val tboolT = @{typ SMT.term_bool}
    7.85 +val term_true = Const (@{const_name True}, tboolT)
    7.86 +val term_false = Const (@{const_name False}, tboolT)
    7.87  
    7.88 -val term_bool = @{lemma "~(term_eq True False)" by (simp add: term_eq_def)}
    7.89 -val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
    7.90 -
    7.91 +val term_bool = @{lemma "True ~= False" by simp}
    7.92 +val term_bool_prop =
    7.93 +  let
    7.94 +    fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)}
    7.95 +      | replace @{const True} = term_true
    7.96 +      | replace @{const False} = term_false
    7.97 +      | replace t = t
    7.98 +  in Term.map_aterms replace (prop_of term_bool) end
    7.99  
   7.100  val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
   7.101      Const (@{const_name Let}, _) => true
   7.102 @@ -171,63 +154,57 @@
   7.103    @{lemma "P = True == P" by (rule eq_reflection) simp},
   7.104    @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
   7.105  
   7.106 -fun rewrite ctxt = Simplifier.full_rewrite
   7.107 -  (Simplifier.context ctxt empty_ss addsimps rewrite_rules)
   7.108 +fun rewrite ctxt ct =
   7.109 +  Conv.top_sweep_conv (fn ctxt' =>
   7.110 +    Conv.rewrs_conv rewrite_rules then_conv rewrite ctxt') ctxt ct
   7.111  
   7.112  fun normalize ctxt thm =
   7.113    if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
   7.114  
   7.115 -val unfold_rules = term_eq_rewr :: rewrite_rules
   7.116 -
   7.117 +fun revert_typ @{typ SMT.term_bool} = @{typ bool}
   7.118 +  | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts)
   7.119 +  | revert_typ T = T
   7.120  
   7.121 -val revert_types =
   7.122 -  let
   7.123 -    fun revert @{typ prop} = @{typ bool}
   7.124 -      | revert (Type (n, Ts)) = Type (n, map revert Ts)
   7.125 -      | revert T = T
   7.126 -  in Term.map_types revert end
   7.127 +val revert_types = Term.map_types revert_typ
   7.128  
   7.129 -
   7.130 -fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
   7.131 +fun folify ctxt =
   7.132    let
   7.133 -    fun is_builtin_conn' (@{const_name True}, _) = false
   7.134 -      | is_builtin_conn' (@{const_name False}, _) = false
   7.135 -      | is_builtin_conn' c = is_builtin_conn c
   7.136 +    fun is_builtin_conn (@{const_name True}, _) _ = false
   7.137 +      | is_builtin_conn (@{const_name False}, _) _ = false
   7.138 +      | is_builtin_conn c ts = B.is_builtin_conn ctxt c ts
   7.139  
   7.140 -    fun is_builtin_pred' _ (@{const_name distinct}, _) [t] =
   7.141 -          is_builtin_distinct andalso can HOLogic.dest_list t
   7.142 -      | is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
   7.143 +    fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true
   7.144  
   7.145 -    val propT = @{typ prop} and boolT = @{typ bool}
   7.146 -    val as_propT = (fn @{typ bool} => propT | T => T)
   7.147 +    fun as_tbool @{typ bool} = tboolT
   7.148 +      | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts)
   7.149 +      | as_tbool T = T
   7.150      fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
   7.151 -    fun conn (n, T) = (n, mapTs as_propT as_propT T)
   7.152 -    fun pred (n, T) = (n, mapTs I as_propT T)
   7.153 +    fun predT T = mapTs as_tbool I T
   7.154 +    fun funcT T = mapTs as_tbool as_tbool T
   7.155 +    fun func (n, T) = Const (n, funcT T)
   7.156  
   7.157 -    val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
   7.158 -    fun as_term t = Const term_eq $ t $ @{const True}
   7.159 -
   7.160 -    val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
   7.161 -    fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
   7.162 +    fun map_ifT T = T |> Term.dest_funT ||> funcT |> (op -->)
   7.163 +    val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const
   7.164 +    fun wrap_in_if t = if_term $ t $ term_true $ term_false
   7.165  
   7.166      fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
   7.167  
   7.168      fun in_term t =
   7.169        (case Term.strip_comb t of
   7.170 -        (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
   7.171 -          c $ in_form t1 $ in_term t2 $ in_term t3
   7.172 -      | (h as Const c, ts) =>
   7.173 -          if is_builtin_conn' (conn c) orelse is_builtin_pred' ctxt (pred c) ts
   7.174 +        (Const (c as @{const_name If}, T), [t1, t2, t3]) =>
   7.175 +          Const (c, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3
   7.176 +      | (Const c, ts) =>
   7.177 +          if is_builtin_conn c ts orelse B.is_builtin_pred ctxt c ts
   7.178            then wrap_in_if (in_form t)
   7.179 -          else Term.list_comb (h, map in_term ts)
   7.180 -      | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
   7.181 +          else Term.list_comb (func c, map in_term ts)
   7.182 +      | (Free (n, T), ts) => Term.list_comb (Free (n, funcT T), map in_term ts)
   7.183        | _ => t)
   7.184  
   7.185      and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
   7.186        | in_weight t = in_form t 
   7.187  
   7.188 -    and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
   7.189 -      | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
   7.190 +    and in_pat (Const (c as (@{const_name pat}, _)) $ t) = func c $ in_term t
   7.191 +      | in_pat (Const (c as (@{const_name nopat}, _)) $ t) = func c $ in_term t
   7.192        | in_pat t = raise TERM ("in_pat", [t])
   7.193  
   7.194      and in_pats ps =
   7.195 @@ -239,23 +216,23 @@
   7.196      and in_form t =
   7.197        (case Term.strip_comb t of
   7.198          (q as Const (qn, _), [Abs (n, T, t')]) =>
   7.199 -          if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
   7.200 +          if is_some (quantifier qn) then q $ Abs (n, as_tbool T, in_trig t')
   7.201            else as_term (in_term t)
   7.202 -      | (Const (c as (@{const_name distinct}, T)), [t']) =>
   7.203 -          if is_builtin_distinct andalso can HOLogic.dest_list t' then
   7.204 -            Const (pred c) $ in_list T in_term t'
   7.205 +      | (Const (c as (n as @{const_name distinct}, T)), [t']) =>
   7.206 +          if B.is_builtin_fun ctxt c [t'] then
   7.207 +            Const (n, predT T) $ in_list T in_term t'
   7.208            else as_term (in_term t)
   7.209 -      | (Const c, ts) =>
   7.210 -          if is_builtin_conn (conn c)
   7.211 -          then Term.list_comb (Const (conn c), map in_form ts)
   7.212 -          else if is_builtin_pred ctxt (pred c)
   7.213 -          then Term.list_comb (Const (pred c), map in_term ts)
   7.214 +      | (Const (c as (n, T)), ts) =>
   7.215 +          if B.is_builtin_conn ctxt c ts
   7.216 +          then Term.list_comb (Const c, map in_form ts)
   7.217 +          else if B.is_builtin_pred ctxt c ts
   7.218 +          then Term.list_comb (Const (n, predT T), map in_term ts)
   7.219            else as_term (in_term t)
   7.220        | _ => as_term (in_term t))
   7.221    in
   7.222      map (apsnd (normalize ctxt)) #> (fn irules =>
   7.223 -    ((unfold_rules, (~1, term_bool') :: irules),
   7.224 -     map (in_form o prop_of o snd) ((~1, term_bool) :: irules)))
   7.225 +    ((rewrite_rules, (~1, term_bool) :: irules),
   7.226 +     term_bool_prop :: map (in_form o prop_of o snd) irules))
   7.227    end
   7.228  
   7.229  
   7.230 @@ -280,10 +257,12 @@
   7.231  fun string_of_index pre i = pre ^ string_of_int i
   7.232  
   7.233  fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) =
   7.234 -  let val s = string_of_index sort_prefix Tidx
   7.235 -  in (s, (Tidx+1, Typtab.update (T, (s, proper)) typs, dtyps, idx, terms)) end
   7.236 +  let
   7.237 +    val s = string_of_index sort_prefix Tidx
   7.238 +    val U = revert_typ T
   7.239 +  in (s, (Tidx+1, Typtab.update (U, (s, proper)) typs, dtyps, idx, terms)) end
   7.240  
   7.241 -fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs
   7.242 +fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs o revert_typ
   7.243  
   7.244  fun fresh_typ T f cx =
   7.245    (case lookup_typ cx T of
   7.246 @@ -297,7 +276,7 @@
   7.247    in (f, (Tidx, typs, dtyps, idx+1, terms')) end
   7.248  
   7.249  fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) =
   7.250 -  (case Termtab.lookup terms t of
   7.251 +  (case Termtab.lookup terms (revert_types t) of
   7.252      SOME (f, _) => (f, cx)
   7.253    | NONE => new_fun func_prefix t ss cx)
   7.254  
   7.255 @@ -335,15 +314,15 @@
   7.256    in ((make_sign (header ts) context, us), make_recon ths context) end
   7.257  
   7.258  
   7.259 -fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
   7.260 +fun translate config ctxt comments =
   7.261    let
   7.262 +    val {prefixes, is_fol, header, has_datatypes, serialize} = config
   7.263      val {sort_prefix, func_prefix} = prefixes
   7.264 -    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
   7.265  
   7.266      fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true)
   7.267        | transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], []))
   7.268        | transT (T as Type (n, Ts)) =
   7.269 -          (case builtin_typ ctxt T of
   7.270 +          (case B.builtin_typ ctxt T of
   7.271              SOME n => pair n
   7.272            | NONE => fresh_typ T (fn _ => fn cx =>
   7.273                if not has_datatypes then new_typ sort_prefix true T cx
   7.274 @@ -387,17 +366,14 @@
   7.275            transT T ##>> trans t1 ##>> trans t2 #>>
   7.276            (fn ((U, u1), u2) => SLet (U, u1, u2))
   7.277        | (h as Const (c as (@{const_name distinct}, T)), ts) =>
   7.278 -          (case builtin_fun ctxt c ts of
   7.279 +          (case B.builtin_fun ctxt c ts of
   7.280              SOME (n, ts) => fold_map trans ts #>> app n
   7.281            | NONE => transs h T ts)
   7.282        | (h as Const (c as (_, T)), ts) =>
   7.283 -          (case try HOLogic.dest_number t of
   7.284 -            SOME (T, i) =>
   7.285 -              (case builtin_num ctxt T i of
   7.286 -                SOME n => pair (SApp (n, []))
   7.287 -              | NONE => transs t T [])
   7.288 +          (case B.builtin_num ctxt t of
   7.289 +            SOME n => pair (SApp (n, []))
   7.290            | NONE =>
   7.291 -              (case builtin_fun ctxt c ts of
   7.292 +              (case B.builtin_fun ctxt c ts of
   7.293                  SOME (n, ts') => fold_map trans ts' #>> app n
   7.294                | NONE => transs h T ts))
   7.295        | (h as Free (_, T), ts) => transs h T ts
   7.296 @@ -414,7 +390,7 @@
   7.297          fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
   7.298        end
   7.299    in
   7.300 -    (case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>
   7.301 +    (if is_fol then folify ctxt else relaxed) #>
   7.302      with_context (header ctxt) trans #>> uncurry (serialize comments)
   7.303    end
   7.304  
     8.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Dec 06 16:54:22 2010 +0100
     8.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Dec 07 14:53:12 2010 +0100
     8.3 @@ -6,34 +6,31 @@
     8.4  
     8.5  signature SMTLIB_INTERFACE =
     8.6  sig
     8.7 -  type builtins = {
     8.8 -    builtin_typ: typ -> string option,
     8.9 -    builtin_num: typ -> int -> string option,
    8.10 -    builtin_func: string * typ -> term list -> (string * term list) option,
    8.11 -    builtin_pred: string * typ -> term list -> (string * term list) option,
    8.12 -    is_builtin_pred: string -> typ -> bool }
    8.13 -  val add_builtins: builtins -> Context.generic -> Context.generic
    8.14 -  val add_logic: (term list -> string option) -> Context.generic ->
    8.15 +  val smtlibC: SMT_Config.class
    8.16 +  val add_logic: int * (term list -> string option) -> Context.generic ->
    8.17      Context.generic
    8.18 -  val extra_norm: SMT_Normalize.extra_norm
    8.19 +  val setup: theory -> theory
    8.20    val interface: SMT_Solver.interface
    8.21  end
    8.22  
    8.23  structure SMTLIB_Interface: SMTLIB_INTERFACE =
    8.24  struct
    8.25  
    8.26 +structure B = SMT_Builtin
    8.27  structure N = SMT_Normalize
    8.28  structure T = SMT_Translate
    8.29  
    8.30 +val smtlibC = ["smtlib"]
    8.31  
    8.32  
    8.33 -(** facts about uninterpreted constants **)
    8.34 +
    8.35 +(* facts about uninterpreted constants *)
    8.36  
    8.37  infix 2 ??
    8.38  fun (ex ?? f) irules = irules |> exists (ex o Thm.prop_of o snd) irules ? f
    8.39  
    8.40  
    8.41 -(* pairs *)
    8.42 +(** pairs **)
    8.43  
    8.44  val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
    8.45  
    8.46 @@ -43,7 +40,7 @@
    8.47  val add_pair_rules = exists_pair_type ?? append (map (pair ~1) pair_rules)
    8.48  
    8.49  
    8.50 -(* function update *)
    8.51 +(** function update **)
    8.52  
    8.53  val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
    8.54  
    8.55 @@ -53,7 +50,7 @@
    8.56  val add_fun_upd_rules = exists_fun_upd ?? append (map (pair ~1) fun_upd_rules)
    8.57  
    8.58  
    8.59 -(* abs/min/max *)
    8.60 +(** abs/min/max **)
    8.61  
    8.62  val exists_abs_min_max = Term.exists_subterm (fn
    8.63      Const (@{const_name abs}, _) => true
    8.64 @@ -86,7 +83,7 @@
    8.65    else thm
    8.66  
    8.67  
    8.68 -(* include additional facts *)
    8.69 +(** include additional facts **)
    8.70  
    8.71  fun extra_norm has_datatypes irules ctxt =
    8.72    irules
    8.73 @@ -97,121 +94,49 @@
    8.74  
    8.75  
    8.76  
    8.77 -(** builtins **)
    8.78 -
    8.79 -(* additional builtins *)
    8.80 -
    8.81 -type builtins = {
    8.82 -  builtin_typ: typ -> string option,
    8.83 -  builtin_num: typ -> int -> string option,
    8.84 -  builtin_func: string * typ -> term list -> (string * term list) option,
    8.85 -  builtin_pred: string * typ -> term list -> (string * term list) option,
    8.86 -  is_builtin_pred: string -> typ -> bool }
    8.87 +(* builtins *)
    8.88  
    8.89 -fun chained _ [] = NONE
    8.90 -  | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
    8.91 -
    8.92 -fun chained' _ [] = false
    8.93 -  | chained' f (b :: bs) = f b orelse chained' f bs
    8.94 -
    8.95 -fun chained_builtin_typ bs T =
    8.96 -  chained (fn {builtin_typ, ...} : builtins => builtin_typ T) bs
    8.97 -
    8.98 -fun chained_builtin_num bs T i =
    8.99 -  chained (fn {builtin_num, ...} : builtins => builtin_num T i) bs
   8.100 -
   8.101 -fun chained_builtin_func bs c ts =
   8.102 -  chained (fn {builtin_func, ...} : builtins => builtin_func c ts) bs
   8.103 +local
   8.104 +  fun int_num _ i = SOME (string_of_int i)
   8.105  
   8.106 -fun chained_builtin_pred bs c ts =
   8.107 -  chained (fn {builtin_pred, ...} : builtins => builtin_pred c ts) bs
   8.108 -
   8.109 -fun chained_is_builtin_pred bs n T =
   8.110 -  chained' (fn {is_builtin_pred, ...} : builtins => is_builtin_pred n T) bs
   8.111 -
   8.112 -fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
   8.113 -
   8.114 -structure Builtins = Generic_Data
   8.115 -(
   8.116 -  type T = (int * builtins) list
   8.117 -  val empty = []
   8.118 -  val extend = I
   8.119 -  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
   8.120 -)
   8.121 -
   8.122 -fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs))
   8.123 -
   8.124 -fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
   8.125 -
   8.126 -
   8.127 -(* basic builtins combined with additional builtins *)
   8.128 -
   8.129 -fun builtin_typ _ @{typ int} = SOME "Int"
   8.130 -  | builtin_typ ctxt T = chained_builtin_typ (get_builtins ctxt) T
   8.131 -
   8.132 -fun builtin_num _ @{typ int} i = SOME (string_of_int i)
   8.133 -  | builtin_num ctxt T i = chained_builtin_num (get_builtins ctxt) T i
   8.134 +  fun distinct _ _ [t] =
   8.135 +        (case try HOLogic.dest_list t of
   8.136 +          SOME (ts as _ :: _) => SOME ("distinct", ts)
   8.137 +        | _ => NONE)
   8.138 +    | distinct _ _ _ = NONE
   8.139 +in
   8.140  
   8.141 -fun if_int_type T n =
   8.142 -  (case try Term.domain_type T of
   8.143 -    SOME @{typ int} => SOME n
   8.144 -  | _ => NONE)
   8.145 -
   8.146 -fun conn @{const_name True} = SOME "true"
   8.147 -  | conn @{const_name False} = SOME "false"
   8.148 -  | conn @{const_name Not} = SOME "not"
   8.149 -  | conn @{const_name HOL.conj} = SOME "and"
   8.150 -  | conn @{const_name HOL.disj} = SOME "or"
   8.151 -  | conn @{const_name HOL.implies} = SOME "implies"
   8.152 -  | conn @{const_name HOL.eq} = SOME "iff"
   8.153 -  | conn @{const_name If} = SOME "if_then_else"
   8.154 -  | conn _ = NONE
   8.155 -
   8.156 -fun distinct_pred (@{const_name distinct}, _) [t] =
   8.157 -      try HOLogic.dest_list t |> Option.map (pair "distinct")
   8.158 -  | distinct_pred _ _ = NONE
   8.159 -
   8.160 -fun pred @{const_name HOL.eq} _ = SOME "="
   8.161 -  | pred @{const_name term_eq} _ = SOME "="
   8.162 -  | pred @{const_name less} T = if_int_type T "<"
   8.163 -  | pred @{const_name less_eq} T = if_int_type T "<="
   8.164 -  | pred _ _ = NONE
   8.165 +val setup =
   8.166 +  B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
   8.167 +  fold (B.add_builtin_fun' smtlibC) [
   8.168 +    (@{const True}, "true"),
   8.169 +    (@{const False}, "false"),
   8.170 + (* FIXME: we do not test if these constants are fully applied! *)
   8.171 +    (@{const Not}, "not"),
   8.172 +    (@{const HOL.conj}, "and"),
   8.173 +    (@{const HOL.disj}, "or"),
   8.174 +    (@{const HOL.implies}, "implies"),
   8.175 +    (@{const HOL.eq (bool)}, "iff"),
   8.176 +    (@{const HOL.eq ('a)}, "="),
   8.177 +    (@{const If (bool)}, "if_then_else"),
   8.178 +    (@{const If ('a)}, "ite"),
   8.179 +    (@{const less (int)}, "<"),
   8.180 +    (@{const less_eq (int)}, "<="),
   8.181 +    (@{const uminus (int)}, "~"),
   8.182 +    (@{const plus (int)}, "+"),
   8.183 +    (@{const minus (int)}, "-"),
   8.184 +    (@{const times (int)}, "*") ] #>
   8.185 +  B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
   8.186  
   8.187 -fun func @{const_name If} _ = SOME "ite"
   8.188 -  | func @{const_name uminus} T = if_int_type T "~"
   8.189 -  | func @{const_name plus} T = if_int_type T "+"
   8.190 -  | func @{const_name minus} T = if_int_type T "-"
   8.191 -  | func @{const_name times} T = if_int_type T "*"
   8.192 -  | func _ _ = NONE
   8.193 -
   8.194 -val is_propT = (fn @{typ prop} => true | _ => false)
   8.195 -fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
   8.196 -fun is_predT T = is_propT (Term.body_type T)
   8.197 -
   8.198 -fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
   8.199 -fun is_builtin_pred ctxt (n, T) = is_predT T andalso
   8.200 -  (is_some (pred n T) orelse chained_is_builtin_pred (get_builtins ctxt) n T)
   8.201 -
   8.202 -fun builtin_fun ctxt (c as (n, T)) ts =
   8.203 -  let
   8.204 -    val builtin_func' = chained_builtin_func (get_builtins ctxt)
   8.205 -    fun builtin_pred' c ts =
   8.206 -      (case distinct_pred c ts of
   8.207 -        SOME b => SOME b
   8.208 -      | NONE => chained_builtin_pred (get_builtins ctxt) c ts)
   8.209 -  in
   8.210 -    if is_connT T then conn n |> Option.map (rpair ts)
   8.211 -    else if is_predT T then
   8.212 -      (case pred n T of SOME c' => SOME (c', ts) | NONE => builtin_pred' c ts)
   8.213 -    else 
   8.214 -      (case func n T of SOME c' => SOME (c', ts) | NONE => builtin_func' c ts)
   8.215 -  end
   8.216 +end
   8.217  
   8.218  
   8.219  
   8.220 -(** serialization **)
   8.221 +(* serialization *)
   8.222  
   8.223 -(* header *)
   8.224 +(** header **)
   8.225 +
   8.226 +fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
   8.227  
   8.228  structure Logics = Generic_Data
   8.229  (
   8.230 @@ -221,13 +146,13 @@
   8.231    fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
   8.232  )
   8.233  
   8.234 -fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l))
   8.235 +fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
   8.236  
   8.237  fun choose_logic ctxt ts =
   8.238    let
   8.239      fun choose [] = "AUFLIA"
   8.240 -      | choose ((_, l) :: ls) = (case l ts of SOME s => s | NONE => choose ls)
   8.241 -  in [":logic " ^ choose (rev (Logics.get (Context.Proof ctxt)))] end
   8.242 +      | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
   8.243 +  in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
   8.244  
   8.245  
   8.246  (* serialization *)
   8.247 @@ -294,21 +219,15 @@
   8.248  (** interfaces **)
   8.249  
   8.250  val interface = {
   8.251 +  class = smtlibC,
   8.252    extra_norm = extra_norm,
   8.253    translate = {
   8.254      prefixes = {
   8.255        sort_prefix = "S",
   8.256        func_prefix = "f"},
   8.257      header = choose_logic,
   8.258 -    strict = SOME {
   8.259 -      is_builtin_conn = is_builtin_conn,
   8.260 -      is_builtin_pred = is_builtin_pred,
   8.261 -      is_builtin_distinct = true},
   8.262 -    builtins = {
   8.263 -      builtin_typ = builtin_typ,
   8.264 -      builtin_num = builtin_num,
   8.265 -      builtin_fun = builtin_fun,
   8.266 -      has_datatypes = false},
   8.267 +    is_fol = true,
   8.268 +    has_datatypes = false,
   8.269      serialize = serialize}}
   8.270  
   8.271  end
     9.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Mon Dec 06 16:54:22 2010 +0100
     9.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Dec 07 14:53:12 2010 +0100
     9.3 @@ -6,8 +6,8 @@
     9.4  
     9.5  signature Z3_INTERFACE =
     9.6  sig
     9.7 -  type builtin_fun = string * typ -> term list -> (string * term list) option
     9.8 -  val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic
     9.9 +  val smtlib_z3C: SMT_Config.class
    9.10 +  val setup: theory -> theory
    9.11    val interface: SMT_Solver.interface
    9.12  
    9.13    datatype sym = Sym of string * sym list
    9.14 @@ -27,45 +27,17 @@
    9.15  struct
    9.16  
    9.17  structure U = SMT_Utils
    9.18 -
    9.19 -
    9.20 -(** Z3-specific builtins **)
    9.21 -
    9.22 -type builtin_fun = string * typ -> term list -> (string * term list) option
    9.23 -
    9.24 -fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
    9.25 +structure B = SMT_Builtin
    9.26  
    9.27 -structure Builtins = Generic_Data
    9.28 -(
    9.29 -  type T = (int * builtin_fun) list
    9.30 -  val empty = []
    9.31 -  val extend = I
    9.32 -  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
    9.33 -)
    9.34 -
    9.35 -fun add_builtin_funs b =
    9.36 -  Builtins.map (Ord_List.insert fst_int_ord (serial (), b))
    9.37 -
    9.38 -fun get_builtin_funs ctxt c ts =
    9.39 -  let
    9.40 -    fun chained [] = NONE
    9.41 -      | chained (b :: bs) = (case b c ts of SOME x => SOME x | _ => chained bs)
    9.42 -  in chained (map snd (Builtins.get (Context.Proof ctxt))) end
    9.43 -
    9.44 -fun z3_builtin_fun builtin_fun ctxt c ts =
    9.45 -  (case builtin_fun ctxt c ts of
    9.46 -    SOME x => SOME x
    9.47 -  | _ => get_builtin_funs ctxt c ts)
    9.48 +val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
    9.49  
    9.50  
    9.51  
    9.52 -(** interface **)
    9.53 +(* interface *)
    9.54  
    9.55  local
    9.56 -  val {translate, ...} = SMTLIB_Interface.interface
    9.57 -  val {prefixes, strict, header, builtins, serialize} = translate
    9.58 -  val {is_builtin_pred, ...}= the strict
    9.59 -  val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
    9.60 +  val {translate, extra_norm, ...} = SMTLIB_Interface.interface
    9.61 +  val {prefixes, is_fol, header, serialize, ...} = translate
    9.62  
    9.63    fun is_int_div_mod @{const div (int)} = true
    9.64      | is_int_div_mod @{const mod (int)} = true
    9.65 @@ -76,45 +48,33 @@
    9.66      then [(~1, @{thm div_by_z3div}), (~1, @{thm mod_by_z3mod})] @ irules
    9.67      else irules
    9.68  
    9.69 -  fun extra_norm' has_datatypes =
    9.70 -    SMTLIB_Interface.extra_norm has_datatypes o add_div_mod
    9.71 -
    9.72 -  fun z3_builtin_fun' _ (@{const_name z3div}, _) ts = SOME ("div", ts)
    9.73 -    | z3_builtin_fun' _ (@{const_name z3mod}, _) ts = SOME ("mod", ts)
    9.74 -    | z3_builtin_fun' ctxt c ts = z3_builtin_fun builtin_fun ctxt c ts
    9.75 -
    9.76 -  val as_propT = (fn @{typ bool} => @{typ prop} | T => T)
    9.77 +  fun extra_norm' has_datatypes = extra_norm has_datatypes o add_div_mod
    9.78  in
    9.79  
    9.80 -fun is_builtin_num ctxt (T, i) = is_some (builtin_num ctxt T i)
    9.81 -
    9.82 -fun is_builtin_fun ctxt (c as (n, T)) ts =
    9.83 -  is_some (z3_builtin_fun' ctxt c ts) orelse 
    9.84 -  is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->))
    9.85 +val setup =
    9.86 +  B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
    9.87 +  B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
    9.88  
    9.89  val interface = {
    9.90 +  class = smtlib_z3C,
    9.91    extra_norm = extra_norm',
    9.92    translate = {
    9.93      prefixes = prefixes,
    9.94 -    strict = strict,
    9.95 +    is_fol = is_fol,
    9.96      header = header,
    9.97 -    builtins = {
    9.98 -      builtin_typ = builtin_typ,
    9.99 -      builtin_num = builtin_num,
   9.100 -      builtin_fun = z3_builtin_fun',
   9.101 -      has_datatypes = true},
   9.102 +    has_datatypes = true,
   9.103      serialize = serialize}}
   9.104  
   9.105  end
   9.106  
   9.107  
   9.108  
   9.109 -(** constructors **)
   9.110 +(* constructors *)
   9.111  
   9.112  datatype sym = Sym of string * sym list
   9.113  
   9.114  
   9.115 -(* additional constructors *)
   9.116 +(** additional constructors **)
   9.117  
   9.118  type mk_builtins = {
   9.119    mk_builtin_typ: sym -> typ option,
   9.120 @@ -135,6 +95,8 @@
   9.121    let val thy = ProofContext.theory_of ctxt
   9.122    in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end
   9.123  
   9.124 +fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
   9.125 +
   9.126  structure Mk_Builtins = Generic_Data
   9.127  (
   9.128    type T = (int * mk_builtins) list
   9.129 @@ -149,7 +111,7 @@
   9.130  fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
   9.131  
   9.132  
   9.133 -(* basic and additional constructors *)
   9.134 +(** basic and additional constructors **)
   9.135  
   9.136  fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
   9.137    | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
   9.138 @@ -241,14 +203,13 @@
   9.139  
   9.140  
   9.141  
   9.142 -(** abstraction **)
   9.143 +(* abstraction *)
   9.144  
   9.145  fun is_builtin_theory_term ctxt t =
   9.146 -  (case try HOLogic.dest_number t of
   9.147 -    SOME n => is_builtin_num ctxt n
   9.148 -  | NONE =>
   9.149 -      (case Term.strip_comb t of
   9.150 -        (Const c, ts) => is_builtin_fun ctxt c ts
   9.151 -      | _ => false))
   9.152 +  if B.is_builtin_num ctxt t then true
   9.153 +  else
   9.154 +    (case Term.strip_comb t of
   9.155 +      (Const c, ts) => B.is_builtin_fun ctxt c ts
   9.156 +    | _ => false)
   9.157  
   9.158  end
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Dec 06 16:54:22 2010 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Dec 07 14:53:12 2010 +0100
    10.3 @@ -135,7 +135,7 @@
    10.4     @{const_name HOL.eq}]
    10.5  
    10.6  fun is_built_in_const_for_prover ctxt name (s, T) =
    10.7 -  if is_smt_prover ctxt name then SMT_Builtin.is_builtin ctxt (s, T)
    10.8 +  if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) [] (*FIXME*)
    10.9    else member (op =) atp_irrelevant_consts s
   10.10  
   10.11  (* FUDGE *)