src/HOL/Tools/SMT/smtlib_interface.ML
author boehmes
Mon Dec 06 15:38:02 2010 +0100 (2010-12-06)
changeset 41057 8dbc951a291c
parent 40681 872b08416fb4
child 41059 d2b1fc1b8e19
permissions -rw-r--r--
tuned
boehmes@36898
     1
(*  Title:      HOL/Tools/SMT/smtlib_interface.ML
boehmes@36898
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36898
     3
boehmes@36898
     4
Interface to SMT solvers based on the SMT-LIB format.
boehmes@36898
     5
*)
boehmes@36898
     6
boehmes@36898
     7
signature SMTLIB_INTERFACE =
boehmes@36898
     8
sig
boehmes@36899
     9
  type builtins = {
boehmes@36899
    10
    builtin_typ: typ -> string option,
boehmes@36899
    11
    builtin_num: typ -> int -> string option,
boehmes@36899
    12
    builtin_func: string * typ -> term list -> (string * term list) option,
boehmes@36899
    13
    builtin_pred: string * typ -> term list -> (string * term list) option,
boehmes@36899
    14
    is_builtin_pred: string -> typ -> bool }
boehmes@36899
    15
  val add_builtins: builtins -> Context.generic -> Context.generic
boehmes@36899
    16
  val add_logic: (term list -> string option) -> Context.generic ->
boehmes@36899
    17
    Context.generic
boehmes@40162
    18
  val extra_norm: SMT_Normalize.extra_norm
boehmes@36898
    19
  val interface: SMT_Solver.interface
boehmes@36898
    20
end
boehmes@36898
    21
boehmes@36898
    22
structure SMTLIB_Interface: SMTLIB_INTERFACE =
boehmes@36898
    23
struct
boehmes@36898
    24
boehmes@36898
    25
structure N = SMT_Normalize
boehmes@36898
    26
structure T = SMT_Translate
boehmes@36898
    27
boehmes@36898
    28
boehmes@36898
    29
boehmes@36898
    30
(** facts about uninterpreted constants **)
boehmes@36898
    31
boehmes@36898
    32
infix 2 ??
boehmes@40161
    33
fun (ex ?? f) irules = irules |> exists (ex o Thm.prop_of o snd) irules ? f
boehmes@36898
    34
boehmes@36898
    35
boehmes@36898
    36
(* pairs *)
boehmes@36898
    37
boehmes@36898
    38
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
boehmes@36898
    39
haftmann@37678
    40
val pair_type = (fn Type (@{type_name Product_Type.prod}, _) => true | _ => false)
boehmes@36898
    41
val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
boehmes@36898
    42
boehmes@40161
    43
val add_pair_rules = exists_pair_type ?? append (map (pair ~1) pair_rules)
boehmes@36898
    44
boehmes@36898
    45
boehmes@36898
    46
(* function update *)
boehmes@36898
    47
boehmes@36898
    48
val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
boehmes@36898
    49
boehmes@36898
    50
val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
boehmes@36898
    51
val exists_fun_upd = Term.exists_subterm is_fun_upd
boehmes@36898
    52
boehmes@40161
    53
val add_fun_upd_rules = exists_fun_upd ?? append (map (pair ~1) fun_upd_rules)
boehmes@36898
    54
boehmes@36898
    55
boehmes@36898
    56
(* abs/min/max *)
boehmes@36898
    57
boehmes@36898
    58
val exists_abs_min_max = Term.exists_subterm (fn
boehmes@36898
    59
    Const (@{const_name abs}, _) => true
boehmes@36898
    60
  | Const (@{const_name min}, _) => true
boehmes@36898
    61
  | Const (@{const_name max}, _) => true
boehmes@36898
    62
  | _ => false)
boehmes@36898
    63
boehmes@37786
    64
val unfold_abs_conv = Conv.rewr_conv (mk_meta_eq @{thm abs_if})
boehmes@37786
    65
val unfold_min_conv = Conv.rewr_conv (mk_meta_eq @{thm min_def})
boehmes@37786
    66
val unfold_max_conv = Conv.rewr_conv (mk_meta_eq @{thm max_def})
boehmes@36898
    67
boehmes@36898
    68
fun expand_conv cv = N.eta_expand_conv (K cv)
boehmes@36898
    69
fun expand2_conv cv = N.eta_expand_conv (N.eta_expand_conv (K cv))
boehmes@36898
    70
boehmes@36898
    71
fun unfold_def_conv ctxt ct =
boehmes@36898
    72
  (case Thm.term_of ct of
boehmes@36898
    73
    Const (@{const_name abs}, _) $ _ => unfold_abs_conv
boehmes@36898
    74
  | Const (@{const_name abs}, _) => expand_conv unfold_abs_conv ctxt
boehmes@36898
    75
  | Const (@{const_name min}, _) $ _ $ _ => unfold_min_conv
boehmes@36898
    76
  | Const (@{const_name min}, _) $ _ => expand_conv unfold_min_conv ctxt
boehmes@36898
    77
  | Const (@{const_name min}, _) => expand2_conv unfold_min_conv ctxt
boehmes@36898
    78
  | Const (@{const_name max}, _) $ _ $ _ => unfold_max_conv
boehmes@36898
    79
  | Const (@{const_name max}, _) $ _ => expand_conv unfold_max_conv ctxt
boehmes@36898
    80
  | Const (@{const_name max}, _) => expand2_conv unfold_max_conv ctxt
boehmes@36898
    81
  | _ => Conv.all_conv) ct
boehmes@36898
    82
boehmes@36898
    83
fun unfold_abs_min_max_defs ctxt thm =
boehmes@36898
    84
  if exists_abs_min_max (Thm.prop_of thm)
wenzelm@36936
    85
  then Conv.fconv_rule (Conv.top_conv unfold_def_conv ctxt) thm
boehmes@36898
    86
  else thm
boehmes@36898
    87
boehmes@36898
    88
boehmes@36898
    89
(* include additional facts *)
boehmes@36898
    90
boehmes@40161
    91
fun extra_norm has_datatypes irules ctxt =
boehmes@40161
    92
  irules
boehmes@39298
    93
  |> not has_datatypes ? add_pair_rules
boehmes@36898
    94
  |> add_fun_upd_rules
boehmes@40161
    95
  |> map (apsnd (unfold_abs_min_max_defs ctxt))
boehmes@36898
    96
  |> rpair ctxt
boehmes@36898
    97
boehmes@36898
    98
boehmes@36898
    99
boehmes@36898
   100
(** builtins **)
boehmes@36898
   101
boehmes@36899
   102
(* additional builtins *)
boehmes@36898
   103
boehmes@36899
   104
type builtins = {
boehmes@36899
   105
  builtin_typ: typ -> string option,
boehmes@36899
   106
  builtin_num: typ -> int -> string option,
boehmes@36899
   107
  builtin_func: string * typ -> term list -> (string * term list) option,
boehmes@36899
   108
  builtin_pred: string * typ -> term list -> (string * term list) option,
boehmes@36899
   109
  is_builtin_pred: string -> typ -> bool }
boehmes@36898
   110
boehmes@36899
   111
fun chained _ [] = NONE
boehmes@36899
   112
  | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
boehmes@36898
   113
boehmes@36899
   114
fun chained' _ [] = false
boehmes@36899
   115
  | chained' f (b :: bs) = f b orelse chained' f bs
boehmes@36899
   116
boehmes@36899
   117
fun chained_builtin_typ bs T =
boehmes@36899
   118
  chained (fn {builtin_typ, ...} : builtins => builtin_typ T) bs
boehmes@36898
   119
boehmes@36899
   120
fun chained_builtin_num bs T i =
boehmes@36899
   121
  chained (fn {builtin_num, ...} : builtins => builtin_num T i) bs
boehmes@36898
   122
boehmes@36899
   123
fun chained_builtin_func bs c ts =
boehmes@36899
   124
  chained (fn {builtin_func, ...} : builtins => builtin_func c ts) bs
boehmes@36899
   125
boehmes@36899
   126
fun chained_builtin_pred bs c ts =
boehmes@36899
   127
  chained (fn {builtin_pred, ...} : builtins => builtin_pred c ts) bs
boehmes@36898
   128
boehmes@36899
   129
fun chained_is_builtin_pred bs n T =
boehmes@36899
   130
  chained' (fn {is_builtin_pred, ...} : builtins => is_builtin_pred n T) bs
boehmes@36898
   131
boehmes@36899
   132
fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
boehmes@36898
   133
boehmes@36899
   134
structure Builtins = Generic_Data
boehmes@36899
   135
(
boehmes@36899
   136
  type T = (int * builtins) list
boehmes@36899
   137
  val empty = []
boehmes@36899
   138
  val extend = I
wenzelm@39687
   139
  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
boehmes@36899
   140
)
boehmes@36898
   141
wenzelm@39687
   142
fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs))
boehmes@36898
   143
boehmes@36899
   144
fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
boehmes@36899
   145
boehmes@36899
   146
boehmes@36899
   147
(* basic builtins combined with additional builtins *)
boehmes@36899
   148
boehmes@36899
   149
fun builtin_typ _ @{typ int} = SOME "Int"
boehmes@36899
   150
  | builtin_typ ctxt T = chained_builtin_typ (get_builtins ctxt) T
boehmes@36898
   151
boehmes@36899
   152
fun builtin_num _ @{typ int} i = SOME (string_of_int i)
boehmes@36899
   153
  | builtin_num ctxt T i = chained_builtin_num (get_builtins ctxt) T i
boehmes@36898
   154
boehmes@36899
   155
fun if_int_type T n =
boehmes@36899
   156
  (case try Term.domain_type T of
boehmes@36899
   157
    SOME @{typ int} => SOME n
boehmes@36899
   158
  | _ => NONE)
boehmes@36898
   159
boehmes@36898
   160
fun conn @{const_name True} = SOME "true"
boehmes@36898
   161
  | conn @{const_name False} = SOME "false"
boehmes@36898
   162
  | conn @{const_name Not} = SOME "not"
haftmann@38795
   163
  | conn @{const_name HOL.conj} = SOME "and"
haftmann@38795
   164
  | conn @{const_name HOL.disj} = SOME "or"
haftmann@38786
   165
  | conn @{const_name HOL.implies} = SOME "implies"
haftmann@38864
   166
  | conn @{const_name HOL.eq} = SOME "iff"
boehmes@36898
   167
  | conn @{const_name If} = SOME "if_then_else"
boehmes@36898
   168
  | conn _ = NONE
boehmes@36898
   169
boehmes@40681
   170
fun distinct_pred (@{const_name distinct}, _) [t] =
boehmes@40681
   171
      try HOLogic.dest_list t |> Option.map (pair "distinct")
boehmes@40681
   172
  | distinct_pred _ _ = NONE
boehmes@40681
   173
boehmes@40681
   174
fun pred @{const_name HOL.eq} _ = SOME "="
boehmes@36898
   175
  | pred @{const_name term_eq} _ = SOME "="
boehmes@36899
   176
  | pred @{const_name less} T = if_int_type T "<"
boehmes@36899
   177
  | pred @{const_name less_eq} T = if_int_type T "<="
boehmes@36898
   178
  | pred _ _ = NONE
boehmes@36898
   179
boehmes@36899
   180
fun func @{const_name If} _ = SOME "ite"
boehmes@36899
   181
  | func @{const_name uminus} T = if_int_type T "~"
boehmes@36899
   182
  | func @{const_name plus} T = if_int_type T "+"
boehmes@36899
   183
  | func @{const_name minus} T = if_int_type T "-"
boehmes@36899
   184
  | func @{const_name times} T = if_int_type T "*"
boehmes@36899
   185
  | func _ _ = NONE
boehmes@36899
   186
boehmes@36899
   187
val is_propT = (fn @{typ prop} => true | _ => false)
boehmes@36899
   188
fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
boehmes@36899
   189
fun is_predT T = is_propT (Term.body_type T)
boehmes@36898
   190
boehmes@36898
   191
fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
boehmes@36899
   192
fun is_builtin_pred ctxt (n, T) = is_predT T andalso
boehmes@36899
   193
  (is_some (pred n T) orelse chained_is_builtin_pred (get_builtins ctxt) n T)
boehmes@36898
   194
boehmes@36899
   195
fun builtin_fun ctxt (c as (n, T)) ts =
boehmes@36899
   196
  let
boehmes@36899
   197
    val builtin_func' = chained_builtin_func (get_builtins ctxt)
boehmes@41057
   198
    fun builtin_pred' c ts =
boehmes@40681
   199
      (case distinct_pred c ts of
boehmes@40681
   200
        SOME b => SOME b
boehmes@40681
   201
      | NONE => chained_builtin_pred (get_builtins ctxt) c ts)
boehmes@36899
   202
  in
boehmes@36899
   203
    if is_connT T then conn n |> Option.map (rpair ts)
boehmes@36899
   204
    else if is_predT T then
boehmes@36899
   205
      (case pred n T of SOME c' => SOME (c', ts) | NONE => builtin_pred' c ts)
boehmes@36899
   206
    else 
boehmes@36899
   207
      (case func n T of SOME c' => SOME (c', ts) | NONE => builtin_func' c ts)
boehmes@36899
   208
  end
boehmes@36898
   209
boehmes@36898
   210
boehmes@36898
   211
boehmes@36898
   212
(** serialization **)
boehmes@36898
   213
boehmes@36899
   214
(* header *)
boehmes@36899
   215
boehmes@36899
   216
structure Logics = Generic_Data
boehmes@36899
   217
(
boehmes@36899
   218
  type T = (int * (term list -> string option)) list
boehmes@36899
   219
  val empty = []
boehmes@36899
   220
  val extend = I
wenzelm@39687
   221
  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
boehmes@36899
   222
)
boehmes@36899
   223
wenzelm@39687
   224
fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l))
boehmes@36899
   225
boehmes@36899
   226
fun choose_logic ctxt ts =
boehmes@36899
   227
  let
boehmes@36899
   228
    fun choose [] = "AUFLIA"
boehmes@36899
   229
      | choose ((_, l) :: ls) = (case l ts of SOME s => s | NONE => choose ls)
boehmes@36899
   230
  in [":logic " ^ choose (rev (Logics.get (Context.Proof ctxt)))] end
boehmes@36899
   231
boehmes@36899
   232
boehmes@36899
   233
(* serialization *)
boehmes@36899
   234
boehmes@36898
   235
val add = Buffer.add
boehmes@36898
   236
fun sep f = add " " #> f
boehmes@36898
   237
fun enclose l r f = sep (add l #> f #> add r)
boehmes@36898
   238
val par = enclose "(" ")"
boehmes@36898
   239
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
boehmes@36898
   240
fun line f = f #> add "\n"
boehmes@36898
   241
boehmes@36898
   242
fun var i = add "?v" #> add (string_of_int i)
boehmes@36898
   243
boehmes@36898
   244
fun sterm l (T.SVar i) = sep (var (l - i - 1))
boehmes@36898
   245
  | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
boehmes@36898
   246
  | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
boehmes@40664
   247
  | sterm l (T.SQua (q, ss, ps, w, t)) =
boehmes@36898
   248
      let
boehmes@36898
   249
        val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
boehmes@36898
   250
        val vs = map_index (apfst (Integer.add l)) ss
boehmes@36898
   251
        fun var_decl (i, s) = par (var i #> sep (add s))
boehmes@36898
   252
        val sub = sterm (l + length ss)
boehmes@36898
   253
        fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
boehmes@36898
   254
        fun pats (T.SPat ts) = pat ":pat" ts
boehmes@36898
   255
          | pats (T.SNoPat ts) = pat ":nopat" ts
boehmes@40664
   256
        fun weight NONE = I
boehmes@40664
   257
          | weight (SOME i) =
boehmes@40664
   258
              sep (add ":weight { " #> add (string_of_int i) #> add " }")
boehmes@40664
   259
      in
boehmes@40664
   260
        par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
boehmes@40664
   261
      end
boehmes@36898
   262
boehmes@37155
   263
fun ssort sorts = sort fast_string_ord sorts
boehmes@37155
   264
fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
boehmes@37155
   265
boehmes@39298
   266
fun sdatatypes decls =
boehmes@39298
   267
  let
boehmes@39298
   268
    fun con (n, []) = add n
boehmes@39298
   269
      | con (n, sels) = par (add n #>
boehmes@39298
   270
          fold (fn (n, s) => sep (par (add n #> sep (add s)))) sels)
boehmes@39298
   271
    fun dtyp (n, decl) = add n #> fold (sep o con) decl
boehmes@39298
   272
  in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
boehmes@39298
   273
boehmes@39298
   274
fun serialize comments {header, sorts, dtyps, funcs} ts =
boehmes@36898
   275
  Buffer.empty
boehmes@36898
   276
  |> line (add "(benchmark Isabelle")
boehmes@36898
   277
  |> line (add ":status unknown")
boehmes@36899
   278
  |> fold (line o add) header
boehmes@36898
   279
  |> length sorts > 0 ?
boehmes@37155
   280
       line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts)))
boehmes@39298
   281
  |> fold sdatatypes dtyps
boehmes@36898
   282
  |> length funcs > 0 ? (
boehmes@36898
   283
       line (add ":extrafuns" #> add " (") #>
boehmes@36898
   284
       fold (fn (f, (ss, s)) =>
boehmes@37155
   285
         line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #>
boehmes@36898
   286
       line (add ")"))
boehmes@36898
   287
  |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
boehmes@36898
   288
  |> line (add ":formula true)")
boehmes@36898
   289
  |> fold (fn str => line (add "; " #> add str)) comments
boehmes@36898
   290
  |> Buffer.content
boehmes@36898
   291
boehmes@36898
   292
boehmes@36898
   293
boehmes@36899
   294
(** interfaces **)
boehmes@36898
   295
boehmes@36898
   296
val interface = {
boehmes@40162
   297
  extra_norm = extra_norm,
boehmes@36898
   298
  translate = {
boehmes@36898
   299
    prefixes = {
boehmes@36898
   300
      sort_prefix = "S",
boehmes@36898
   301
      func_prefix = "f"},
boehmes@36899
   302
    header = choose_logic,
boehmes@36898
   303
    strict = SOME {
boehmes@36898
   304
      is_builtin_conn = is_builtin_conn,
boehmes@36898
   305
      is_builtin_pred = is_builtin_pred,
boehmes@36898
   306
      is_builtin_distinct = true},
boehmes@36898
   307
    builtins = {
boehmes@36898
   308
      builtin_typ = builtin_typ,
boehmes@36898
   309
      builtin_num = builtin_num,
boehmes@39298
   310
      builtin_fun = builtin_fun,
boehmes@39298
   311
      has_datatypes = false},
boehmes@36898
   312
    serialize = serialize}}
boehmes@36898
   313
boehmes@36898
   314
end