src/HOL/Tools/SMT/smt_builtin.ML
author boehmes
Wed Dec 15 08:39:24 2010 +0100 (2010-12-15)
changeset 41126 e0bd443c0fdd
parent 41124 1de17a2de5ad
child 41127 2ea84c8535c6
permissions -rw-r--r--
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)
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
boehmes@41059
     9
  (*built-in types*)
boehmes@41124
    10
  val add_builtin_typ: SMT_Utils.class ->
boehmes@41072
    11
    typ * (typ -> string option) * (typ -> int -> string option) ->
boehmes@41072
    12
    Context.generic -> Context.generic
boehmes@41072
    13
  val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
boehmes@41072
    14
    Context.generic
boehmes@41059
    15
  val builtin_typ: Proof.context -> typ -> string option
boehmes@41059
    16
  val is_builtin_typ: Proof.context -> typ -> bool
boehmes@41059
    17
  val is_builtin_typ_ext: Proof.context -> typ -> bool
boehmes@41059
    18
boehmes@41059
    19
  (*built-in numbers*)
boehmes@41059
    20
  val builtin_num: Proof.context -> term -> string option
boehmes@41059
    21
  val is_builtin_num: Proof.context -> term -> bool
boehmes@41059
    22
  val is_builtin_num_ext: Proof.context -> term -> bool
boehmes@41059
    23
boehmes@41059
    24
  (*built-in functions*)
boehmes@41059
    25
  type 'a bfun = Proof.context -> typ -> term list -> 'a
boehmes@41124
    26
  val add_builtin_fun: SMT_Utils.class ->
boehmes@41072
    27
    (string * typ) * (string * term list) option bfun -> Context.generic ->
boehmes@41072
    28
    Context.generic
boehmes@41124
    29
  val add_builtin_fun': SMT_Utils.class -> term * string -> Context.generic ->
boehmes@41072
    30
    Context.generic
boehmes@41072
    31
  val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic ->
boehmes@41072
    32
    Context.generic
boehmes@41072
    33
  val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
boehmes@41072
    34
  val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
boehmes@41059
    35
  val builtin_fun: Proof.context -> string * typ -> term list ->
boehmes@41059
    36
    (string * term list) option
boehmes@41059
    37
  val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
boehmes@41059
    38
  val is_builtin_pred: Proof.context -> string * typ -> term list -> bool
boehmes@41059
    39
  val is_builtin_conn: Proof.context -> string * typ -> term list -> bool
boehmes@41126
    40
  val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
boehmes@41059
    41
  val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
boehmes@40277
    42
end
boehmes@40277
    43
boehmes@40277
    44
structure SMT_Builtin: SMT_BUILTIN =
boehmes@40277
    45
struct
boehmes@40277
    46
boehmes@41124
    47
structure U = SMT_Utils
boehmes@41059
    48
structure C = SMT_Config
boehmes@41059
    49
boehmes@41059
    50
boehmes@41059
    51
(* built-in tables *)
boehmes@41059
    52
boehmes@41059
    53
datatype ('a, 'b) kind = Ext of 'a | Int of 'b
boehmes@41059
    54
boehmes@41124
    55
type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) U.dict 
blanchet@40677
    56
boehmes@41059
    57
fun typ_ord ((T, _), (U, _)) =
boehmes@41059
    58
  let
boehmes@41059
    59
    fun tord (TVar _, Type _) = GREATER
boehmes@41059
    60
      | tord (Type _, TVar _) = LESS
boehmes@41059
    61
      | tord (Type (n, Ts), Type (m, Us)) =
boehmes@41059
    62
          if n = m then list_ord tord (Ts, Us)
boehmes@41059
    63
          else Term_Ord.typ_ord (T, U)
boehmes@41059
    64
      | tord TU = Term_Ord.typ_ord TU
boehmes@41059
    65
  in tord (T, U) end
boehmes@40277
    66
boehmes@41059
    67
fun insert_ttab cs T f =
boehmes@41124
    68
  U.dict_map_default (cs, [])
boehmes@41059
    69
    (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
boehmes@41059
    70
boehmes@41059
    71
fun merge_ttab ttabp =
boehmes@41124
    72
  U.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp
boehmes@40277
    73
boehmes@41059
    74
fun lookup_ttab ctxt ttab T =
boehmes@41124
    75
  let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)
boehmes@41124
    76
  in
boehmes@41124
    77
    get_first (find_first match) (U.dict_lookup ttab (C.solver_class_of ctxt))
boehmes@41124
    78
  end
boehmes@41059
    79
boehmes@41059
    80
type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
boehmes@41059
    81
boehmes@41059
    82
fun insert_btab cs n T f =
boehmes@41059
    83
  Symtab.map_default (n, []) (insert_ttab cs T f)
boehmes@41059
    84
boehmes@41059
    85
fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
boehmes@40277
    86
boehmes@41059
    87
fun lookup_btab ctxt btab (n, T) =
boehmes@41059
    88
  (case Symtab.lookup btab n of
boehmes@41059
    89
    NONE => NONE
boehmes@41059
    90
  | SOME ttab => lookup_ttab ctxt ttab T)
boehmes@40277
    91
boehmes@41059
    92
boehmes@41059
    93
(* built-in types *)
boehmes@40277
    94
boehmes@41072
    95
structure Builtin_Types = Generic_Data
boehmes@41059
    96
(
boehmes@41059
    97
  type T =
boehmes@41059
    98
    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
boehmes@41072
    99
  val empty = []
boehmes@41059
   100
  val extend = I
boehmes@41059
   101
  val merge = merge_ttab
boehmes@41059
   102
)
boehmes@41059
   103
boehmes@41059
   104
fun add_builtin_typ cs (T, f, g) =
boehmes@41059
   105
  Builtin_Types.map (insert_ttab cs T (Int (f, g)))
boehmes@41059
   106
boehmes@41059
   107
fun add_builtin_typ_ext (T, f) =
boehmes@41124
   108
  Builtin_Types.map (insert_ttab U.basicC T (Ext f))
boehmes@40277
   109
boehmes@41059
   110
fun lookup_builtin_typ ctxt =
boehmes@41072
   111
  lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt))
boehmes@40277
   112
boehmes@41059
   113
fun builtin_typ ctxt T =
boehmes@41059
   114
  (case lookup_builtin_typ ctxt T of
boehmes@41059
   115
    SOME (_, Int (f, _)) => f T
boehmes@41059
   116
  | _ => NONE) 
boehmes@40277
   117
boehmes@41059
   118
fun is_builtin_typ ctxt T = is_some (builtin_typ ctxt T)
boehmes@41059
   119
boehmes@41059
   120
fun is_builtin_typ_ext ctxt T =
boehmes@41059
   121
  (case lookup_builtin_typ ctxt T of
boehmes@41059
   122
    SOME (_, Int (f, _)) => is_some (f T)
boehmes@41059
   123
  | SOME (_, Ext f) => f T
boehmes@40277
   124
  | NONE => false)
boehmes@40277
   125
boehmes@41059
   126
boehmes@41059
   127
(* built-in numbers *)
boehmes@41059
   128
boehmes@41059
   129
fun builtin_num ctxt t =
boehmes@41059
   130
  (case try HOLogic.dest_number t of
boehmes@41059
   131
    NONE => NONE
boehmes@41059
   132
  | SOME (T, i) =>
boehmes@41059
   133
      (case lookup_builtin_typ ctxt T of
boehmes@41059
   134
        SOME (_, Int (_, g)) => g T i
boehmes@41059
   135
      | _ => NONE))
boehmes@41059
   136
boehmes@41059
   137
val is_builtin_num = is_some oo builtin_num
boehmes@41059
   138
boehmes@41059
   139
fun is_builtin_num_ext ctxt t =
boehmes@41059
   140
  (case try HOLogic.dest_number t of
boehmes@41059
   141
    NONE => false
boehmes@41059
   142
  | SOME (T, _) => is_builtin_typ_ext ctxt T)
boehmes@41059
   143
boehmes@41059
   144
boehmes@41059
   145
(* built-in functions *)
boehmes@41059
   146
boehmes@41059
   147
type 'a bfun = Proof.context -> typ -> term list -> 'a
boehmes@41059
   148
boehmes@41072
   149
structure Builtin_Funcs = Generic_Data
boehmes@41059
   150
(
boehmes@41126
   151
  type T = (bool bfun, (string * term list) option bfun) btab
boehmes@41126
   152
  val empty = Symtab.empty
boehmes@41059
   153
  val extend = I
boehmes@41059
   154
  val merge = merge_btab
boehmes@41059
   155
)
boehmes@41059
   156
boehmes@41059
   157
fun add_builtin_fun cs ((n, T), f) =
boehmes@41059
   158
  Builtin_Funcs.map (insert_btab cs n T (Int f))
boehmes@40277
   159
boehmes@41059
   160
fun add_builtin_fun' cs (t, n) =
boehmes@41059
   161
  add_builtin_fun cs (Term.dest_Const t, fn _ => fn _ => SOME o pair n)
boehmes@41059
   162
boehmes@41059
   163
fun add_builtin_fun_ext ((n, T), f) =
boehmes@41124
   164
  Builtin_Funcs.map (insert_btab U.basicC n T (Ext f))
boehmes@41059
   165
boehmes@41126
   166
fun add_builtin_fun_ext' c =
boehmes@41126
   167
  add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true)
boehmes@41059
   168
boehmes@41072
   169
fun add_builtin_fun_ext'' n context =
boehmes@41072
   170
  let val thy = Context.theory_of context
boehmes@41072
   171
  in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end
boehmes@41059
   172
boehmes@41059
   173
fun lookup_builtin_fun ctxt =
boehmes@41072
   174
  lookup_btab ctxt (Builtin_Funcs.get (Context.Proof ctxt))
boehmes@41059
   175
boehmes@41059
   176
fun builtin_fun ctxt (c as (_, T)) ts =
boehmes@41059
   177
  (case lookup_builtin_fun ctxt c of
boehmes@41059
   178
    SOME (_, Int f) => f ctxt T ts
boehmes@41059
   179
  | _ => NONE)
boehmes@41059
   180
boehmes@41059
   181
fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts)
boehmes@41059
   182
boehmes@41059
   183
fun is_special_builtin_fun pred ctxt (c as (_, T)) ts =
boehmes@41059
   184
  (case lookup_builtin_fun ctxt c of
boehmes@41059
   185
    SOME (U, Int f) => pred U andalso is_some (f ctxt T ts)
boehmes@41059
   186
  | _ => false)
boehmes@41059
   187
boehmes@41059
   188
fun is_pred_type T = Term.body_type T = @{typ bool}
boehmes@41059
   189
fun is_conn_type T =
boehmes@41059
   190
  forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
boehmes@41059
   191
boehmes@41059
   192
fun is_builtin_pred ctxt = is_special_builtin_fun is_pred_type ctxt
boehmes@41059
   193
fun is_builtin_conn ctxt = is_special_builtin_fun is_conn_type ctxt
boehmes@41059
   194
boehmes@41059
   195
fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
boehmes@41059
   196
  (case lookup_builtin_fun ctxt c of
boehmes@41059
   197
    SOME (_, Int f) => is_some (f ctxt T ts)
boehmes@41059
   198
  | SOME (_, Ext f) => f ctxt T ts
boehmes@41059
   199
  | NONE => false)
boehmes@41059
   200
boehmes@41059
   201
(* FIXME: move this information to the interfaces *)
boehmes@41059
   202
val only_partially_supported = [
boehmes@41059
   203
  @{const_name times},
boehmes@41059
   204
  @{const_name div_class.div},
boehmes@41059
   205
  @{const_name div_class.mod},
boehmes@41059
   206
  @{const_name inverse_class.divide} ]
boehmes@41059
   207
boehmes@41059
   208
fun is_builtin_ext ctxt (c as (n, _)) ts =
boehmes@41059
   209
  if member (op =) only_partially_supported n then false
boehmes@41073
   210
  else
boehmes@41073
   211
    is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) orelse 
boehmes@41073
   212
    is_builtin_fun_ext ctxt c ts
boehmes@40277
   213
boehmes@40277
   214
end