src/HOL/Tools/SMT/smt_builtin.ML

re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
added simple trigger inference mechanism;
added syntactic checks for triggers and quantifier weights;
factored out the normalization of special quantifiers (used to be in the eta-normalization part);
normalization now unfolds abs/min/max (not SMT-LIB-specific);
rules for pairs and function update are not anymore added automatically to the problem;
more aggressive rewriting of natural number operations into integer operations (minimizes the number of remaining nat-int coercions);
normalizations are now managed in a class-based manner (similar to built-in symbols)

(*  Title:      HOL/Tools/SMT/smt_builtin.ML
    Author:     Sascha Boehme, TU Muenchen

Tables of types and terms directly supported by SMT solvers.
*)

signature SMT_BUILTIN =
sig
  (*built-in types*)
  val add_builtin_typ: SMT_Utils.class ->
    typ * (typ -> string option) * (typ -> int -> string option) ->
    Context.generic -> Context.generic
  val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
    Context.generic
  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_Utils.class ->
    (string * typ) * (string * term list) option bfun -> Context.generic ->
    Context.generic
  val add_builtin_fun': SMT_Utils.class -> term * string -> Context.generic ->
    Context.generic
  val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic ->
    Context.generic
  val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
  val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
  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_fun_ext: 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

structure U = SMT_Utils
structure C = SMT_Config


(* built-in tables *)

datatype ('a, 'b) kind = Ext of 'a | Int of 'b

type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) U.dict 

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

fun insert_ttab cs T f =
  U.dict_map_default (cs, [])
    (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))

fun merge_ttab ttabp =
  U.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp

fun lookup_ttab ctxt ttab T =
  let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)
  in
    get_first (find_first match) (U.dict_lookup ttab (C.solver_class_of ctxt))
  end

type ('a, 'b) btab = ('a, 'b) ttab Symtab.table

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

fun lookup_btab ctxt btab (n, T) =
  (case Symtab.lookup btab n of
    NONE => NONE
  | SOME ttab => lookup_ttab ctxt ttab T)


(* built-in types *)

structure Builtin_Types = Generic_Data
(
  type T =
    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
  val empty = []
  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 U.basicC T (Ext f))

fun lookup_builtin_typ ctxt =
  lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt))

fun builtin_typ ctxt T =
  (case lookup_builtin_typ ctxt T of
    SOME (_, Int (f, _)) => f T
  | _ => NONE) 

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)


(* 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

structure Builtin_Funcs = Generic_Data
(
  type T = (bool bfun, (string * term list) option bfun) btab
  val empty = Symtab.empty
  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 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 U.basicC n T (Ext f))

fun add_builtin_fun_ext' c =
  add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true)

fun add_builtin_fun_ext'' n context =
  let val thy = Context.theory_of context
  in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end

fun lookup_builtin_fun ctxt =
  lookup_btab ctxt (Builtin_Funcs.get (Context.Proof 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_num_ext ctxt (Term.list_comb (Const c, ts)) orelse 
    is_builtin_fun_ext ctxt c ts

end