src/HOL/Tools/SMT/smt_builtin.ML
author blanchet
Mon Sep 30 17:47:50 2013 +0200 (2013-09-30)
changeset 54000 9cfff7f61d0d
parent 53999 ba9254f3111b
child 54489 03ff4d1e6784
permissions -rw-r--r--
added experimental configuration options to tune use of builtin symbols in SMT
boehmes@40277
     1
(*  Title:      HOL/Tools/SMT/smt_builtin.ML
boehmes@40277
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@40277
     3
boehmes@41059
     4
Tables of types and terms directly supported by SMT solvers.
boehmes@40277
     5
*)
boehmes@40277
     6
boehmes@40277
     7
signature SMT_BUILTIN =
boehmes@40277
     8
sig
blanchet@53999
     9
  (*for experiments*)
blanchet@54000
    10
  val filter_builtins: (typ -> bool) -> Proof.context -> Proof.context
blanchet@53999
    11
boehmes@41059
    12
  (*built-in types*)
boehmes@41124
    13
  val add_builtin_typ: SMT_Utils.class ->
boehmes@41072
    14
    typ * (typ -> string option) * (typ -> int -> string option) ->
boehmes@41072
    15
    Context.generic -> Context.generic
boehmes@41072
    16
  val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
boehmes@41072
    17
    Context.generic
boehmes@41281
    18
  val dest_builtin_typ: Proof.context -> typ -> string option
boehmes@41059
    19
  val is_builtin_typ_ext: Proof.context -> typ -> bool
boehmes@41059
    20
boehmes@41059
    21
  (*built-in numbers*)
boehmes@41281
    22
  val dest_builtin_num: Proof.context -> term -> (string * typ) option
boehmes@41059
    23
  val is_builtin_num: Proof.context -> term -> bool
boehmes@41059
    24
  val is_builtin_num_ext: Proof.context -> term -> bool
boehmes@41059
    25
boehmes@41059
    26
  (*built-in functions*)
boehmes@41059
    27
  type 'a bfun = Proof.context -> typ -> term list -> 'a
boehmes@41281
    28
  type bfunr = string * int * term list * (term list -> term)
boehmes@41124
    29
  val add_builtin_fun: SMT_Utils.class ->
boehmes@41281
    30
    (string * typ) * bfunr option bfun -> Context.generic -> Context.generic
boehmes@41124
    31
  val add_builtin_fun': SMT_Utils.class -> term * string -> Context.generic ->
boehmes@41072
    32
    Context.generic
boehmes@41354
    33
  val add_builtin_fun_ext: (string * typ) * term list bfun ->
boehmes@41354
    34
    Context.generic -> Context.generic
boehmes@41072
    35
  val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
boehmes@41072
    36
  val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
boehmes@41281
    37
  val dest_builtin_fun: Proof.context -> string * typ -> term list ->
boehmes@41281
    38
    bfunr option
boehmes@41281
    39
  val dest_builtin_eq: Proof.context -> term -> term -> bfunr option
boehmes@41281
    40
  val dest_builtin_pred: Proof.context -> string * typ -> term list ->
boehmes@41281
    41
    bfunr option
boehmes@41281
    42
  val dest_builtin_conn: Proof.context -> string * typ -> term list ->
boehmes@41281
    43
    bfunr option
boehmes@41281
    44
  val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
boehmes@41354
    45
  val dest_builtin_ext: Proof.context -> string * typ -> term list ->
boehmes@41354
    46
    term list option
boehmes@41059
    47
  val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
boehmes@41126
    48
  val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
boehmes@40277
    49
end
boehmes@40277
    50
boehmes@40277
    51
structure SMT_Builtin: SMT_BUILTIN =
boehmes@40277
    52
struct
boehmes@40277
    53
boehmes@41059
    54
boehmes@41059
    55
(* built-in tables *)
boehmes@41059
    56
boehmes@41059
    57
datatype ('a, 'b) kind = Ext of 'a | Int of 'b
boehmes@41059
    58
boehmes@41328
    59
type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT_Utils.dict 
blanchet@40677
    60
boehmes@41059
    61
fun typ_ord ((T, _), (U, _)) =
boehmes@41059
    62
  let
boehmes@41059
    63
    fun tord (TVar _, Type _) = GREATER
boehmes@41059
    64
      | tord (Type _, TVar _) = LESS
boehmes@41059
    65
      | tord (Type (n, Ts), Type (m, Us)) =
boehmes@41059
    66
          if n = m then list_ord tord (Ts, Us)
boehmes@41059
    67
          else Term_Ord.typ_ord (T, U)
boehmes@41059
    68
      | tord TU = Term_Ord.typ_ord TU
boehmes@41059
    69
  in tord (T, U) end
boehmes@40277
    70
boehmes@41059
    71
fun insert_ttab cs T f =
boehmes@41328
    72
  SMT_Utils.dict_map_default (cs, [])
boehmes@41059
    73
    (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
boehmes@41059
    74
boehmes@41059
    75
fun merge_ttab ttabp =
wenzelm@41473
    76
  SMT_Utils.dict_merge (Ord_List.merge typ_ord) ttabp
boehmes@40277
    77
boehmes@41059
    78
fun lookup_ttab ctxt ttab T =
wenzelm@42361
    79
  let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U)
boehmes@41124
    80
  in
boehmes@41328
    81
    get_first (find_first match)
boehmes@41328
    82
      (SMT_Utils.dict_lookup ttab (SMT_Config.solver_class_of ctxt))
boehmes@41124
    83
  end
boehmes@41059
    84
boehmes@41059
    85
type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
boehmes@41059
    86
boehmes@41059
    87
fun insert_btab cs n T f =
boehmes@41059
    88
  Symtab.map_default (n, []) (insert_ttab cs T f)
boehmes@41059
    89
boehmes@41059
    90
fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
boehmes@40277
    91
boehmes@41059
    92
fun lookup_btab ctxt btab (n, T) =
boehmes@41059
    93
  (case Symtab.lookup btab n of
boehmes@41059
    94
    NONE => NONE
boehmes@41059
    95
  | SOME ttab => lookup_ttab ctxt ttab T)
boehmes@40277
    96
blanchet@53998
    97
type 'a bfun = Proof.context -> typ -> term list -> 'a
blanchet@53998
    98
blanchet@53998
    99
type bfunr = string * int * term list * (term list -> term)
blanchet@53998
   100
blanchet@53998
   101
structure Builtins = Generic_Data
blanchet@53998
   102
(
blanchet@53998
   103
  type T =
blanchet@53998
   104
    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
blanchet@53998
   105
    (term list bfun, bfunr option bfun) btab
blanchet@53998
   106
  val empty = ([], Symtab.empty)
blanchet@53998
   107
  val extend = I
blanchet@53998
   108
  fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
blanchet@53998
   109
)
boehmes@41059
   110
blanchet@54000
   111
fun filter_ttab keep_T = map (apsnd (filter (keep_T o fst)))
blanchet@54000
   112
blanchet@54000
   113
fun filter_builtins keep_T =
blanchet@54000
   114
  Context.proof_map (Builtins.map (fn (ttab, btab) =>
blanchet@54000
   115
    (filter_ttab keep_T ttab, Symtab.map (K (filter_ttab keep_T)) btab)))
blanchet@53999
   116
blanchet@53999
   117
boehmes@41059
   118
(* built-in types *)
boehmes@40277
   119
boehmes@41059
   120
fun add_builtin_typ cs (T, f, g) =
blanchet@53998
   121
  Builtins.map (apfst (insert_ttab cs T (Int (f, g))))
boehmes@41059
   122
boehmes@41059
   123
fun add_builtin_typ_ext (T, f) =
blanchet@53998
   124
  Builtins.map (apfst (insert_ttab SMT_Utils.basicC T (Ext f)))
boehmes@40277
   125
boehmes@41059
   126
fun lookup_builtin_typ ctxt =
blanchet@53998
   127
  lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt)))
boehmes@40277
   128
boehmes@41281
   129
fun dest_builtin_typ ctxt T =
boehmes@41059
   130
  (case lookup_builtin_typ ctxt T of
boehmes@41059
   131
    SOME (_, Int (f, _)) => f T
boehmes@41059
   132
  | _ => NONE) 
boehmes@40277
   133
boehmes@41059
   134
fun is_builtin_typ_ext ctxt T =
boehmes@41059
   135
  (case lookup_builtin_typ ctxt T of
boehmes@41059
   136
    SOME (_, Int (f, _)) => is_some (f T)
boehmes@41059
   137
  | SOME (_, Ext f) => f T
boehmes@40277
   138
  | NONE => false)
boehmes@40277
   139
boehmes@41059
   140
boehmes@41059
   141
(* built-in numbers *)
boehmes@41059
   142
boehmes@41281
   143
fun dest_builtin_num ctxt t =
boehmes@41059
   144
  (case try HOLogic.dest_number t of
boehmes@41059
   145
    NONE => NONE
boehmes@41059
   146
  | SOME (T, i) =>
boehmes@41059
   147
      (case lookup_builtin_typ ctxt T of
boehmes@41127
   148
        SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
boehmes@41059
   149
      | _ => NONE))
boehmes@41059
   150
boehmes@41281
   151
val is_builtin_num = is_some oo dest_builtin_num
boehmes@41059
   152
boehmes@41059
   153
fun is_builtin_num_ext ctxt t =
boehmes@41059
   154
  (case try HOLogic.dest_number t of
boehmes@41059
   155
    NONE => false
boehmes@41059
   156
  | SOME (T, _) => is_builtin_typ_ext ctxt T)
boehmes@41059
   157
boehmes@41059
   158
boehmes@41059
   159
(* built-in functions *)
boehmes@41059
   160
boehmes@41059
   161
fun add_builtin_fun cs ((n, T), f) =
blanchet@53998
   162
  Builtins.map (apsnd (insert_btab cs n T (Int f)))
boehmes@40277
   163
boehmes@41059
   164
fun add_builtin_fun' cs (t, n) =
boehmes@41127
   165
  let
boehmes@41281
   166
    val c as (m, T) = Term.dest_Const t
boehmes@41281
   167
    fun app U ts = Term.list_comb (Const (m, U), ts)
boehmes@41281
   168
    fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U)
boehmes@41281
   169
  in add_builtin_fun cs (c, bfun) end
boehmes@41059
   170
boehmes@41059
   171
fun add_builtin_fun_ext ((n, T), f) =
blanchet@53998
   172
  Builtins.map (apsnd (insert_btab SMT_Utils.basicC n T (Ext f)))
boehmes@41059
   173
boehmes@41354
   174
fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I)
boehmes@41059
   175
boehmes@41072
   176
fun add_builtin_fun_ext'' n context =
boehmes@41072
   177
  let val thy = Context.theory_of context
boehmes@41072
   178
  in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end
boehmes@41059
   179
boehmes@41059
   180
fun lookup_builtin_fun ctxt =
blanchet@53998
   181
  lookup_btab ctxt (snd (Builtins.get (Context.Proof ctxt)))
boehmes@41059
   182
boehmes@41281
   183
fun dest_builtin_fun ctxt (c as (_, T)) ts =
boehmes@41059
   184
  (case lookup_builtin_fun ctxt c of
boehmes@41059
   185
    SOME (_, Int f) => f ctxt T ts
boehmes@41059
   186
  | _ => NONE)
boehmes@41059
   187
boehmes@41281
   188
fun dest_builtin_eq ctxt t u =
boehmes@41281
   189
  let
boehmes@41281
   190
    val aT = TFree (Name.aT, @{sort type})
boehmes@41281
   191
    val c = (@{const_name HOL.eq}, aT --> aT --> @{typ bool})
boehmes@41281
   192
    fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts)
boehmes@41281
   193
  in
boehmes@41281
   194
    dest_builtin_fun ctxt c []
boehmes@41281
   195
    |> Option.map (fn (n, i, _, _) => (n, i, [t, u], mk))
boehmes@41281
   196
  end
boehmes@41281
   197
boehmes@41281
   198
fun special_builtin_fun pred ctxt (c as (_, T)) ts =
boehmes@41281
   199
  if pred (Term.body_type T, Term.binder_types T) then
boehmes@41281
   200
    dest_builtin_fun ctxt c ts
boehmes@41281
   201
  else NONE
boehmes@41281
   202
boehmes@41281
   203
fun dest_builtin_pred ctxt = special_builtin_fun (equal @{typ bool} o fst) ctxt
boehmes@41281
   204
boehmes@41281
   205
fun dest_builtin_conn ctxt =
boehmes@41281
   206
  special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt
boehmes@41281
   207
boehmes@41281
   208
fun dest_builtin ctxt c ts =
blanchet@53999
   209
  let val t = Term.list_comb (Const c, ts)
boehmes@41281
   210
  in
boehmes@41281
   211
    (case dest_builtin_num ctxt t of
boehmes@41281
   212
      SOME (n, _) => SOME (n, 0, [], K t)
boehmes@41281
   213
    | NONE => dest_builtin_fun ctxt c ts)
boehmes@41281
   214
  end
boehmes@41281
   215
boehmes@41354
   216
fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =    
boehmes@41354
   217
  (case lookup_builtin_fun ctxt c of
boehmes@41354
   218
    SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
boehmes@41354
   219
  | SOME (_, Ext f) => SOME (f ctxt T ts)
boehmes@41354
   220
  | NONE => NONE)
boehmes@41354
   221
boehmes@41354
   222
fun dest_builtin_ext ctxt c ts =
boehmes@41354
   223
  if is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) then SOME []
boehmes@41354
   224
  else dest_builtin_fun_ext ctxt c ts
boehmes@41354
   225
boehmes@41281
   226
fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts)
boehmes@41059
   227
boehmes@41354
   228
fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
boehmes@41059
   229
boehmes@40277
   230
end