src/HOL/Tools/SMT/smtlib_interface.ML
author boehmes
Tue Dec 07 14:53:12 2010 +0100 (2010-12-07)
changeset 41059 d2b1fc1b8e19
parent 41057 8dbc951a291c
child 41072 9f9bc1bdacef
permissions -rw-r--r--
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)
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@41059
     9
  val smtlibC: SMT_Config.class
boehmes@41059
    10
  val add_logic: int * (term list -> string option) -> Context.generic ->
boehmes@36899
    11
    Context.generic
boehmes@41059
    12
  val setup: theory -> theory
boehmes@36898
    13
  val interface: SMT_Solver.interface
boehmes@36898
    14
end
boehmes@36898
    15
boehmes@36898
    16
structure SMTLIB_Interface: SMTLIB_INTERFACE =
boehmes@36898
    17
struct
boehmes@36898
    18
boehmes@41059
    19
structure B = SMT_Builtin
boehmes@36898
    20
structure N = SMT_Normalize
boehmes@36898
    21
structure T = SMT_Translate
boehmes@36898
    22
boehmes@41059
    23
val smtlibC = ["smtlib"]
boehmes@36898
    24
boehmes@36898
    25
boehmes@41059
    26
boehmes@41059
    27
(* facts about uninterpreted constants *)
boehmes@36898
    28
boehmes@36898
    29
infix 2 ??
boehmes@40161
    30
fun (ex ?? f) irules = irules |> exists (ex o Thm.prop_of o snd) irules ? f
boehmes@36898
    31
boehmes@36898
    32
boehmes@41059
    33
(** pairs **)
boehmes@36898
    34
boehmes@36898
    35
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
boehmes@36898
    36
haftmann@37678
    37
val pair_type = (fn Type (@{type_name Product_Type.prod}, _) => true | _ => false)
boehmes@36898
    38
val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
boehmes@36898
    39
boehmes@40161
    40
val add_pair_rules = exists_pair_type ?? append (map (pair ~1) pair_rules)
boehmes@36898
    41
boehmes@36898
    42
boehmes@41059
    43
(** function update **)
boehmes@36898
    44
boehmes@36898
    45
val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
boehmes@36898
    46
boehmes@36898
    47
val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
boehmes@36898
    48
val exists_fun_upd = Term.exists_subterm is_fun_upd
boehmes@36898
    49
boehmes@40161
    50
val add_fun_upd_rules = exists_fun_upd ?? append (map (pair ~1) fun_upd_rules)
boehmes@36898
    51
boehmes@36898
    52
boehmes@41059
    53
(** abs/min/max **)
boehmes@36898
    54
boehmes@36898
    55
val exists_abs_min_max = Term.exists_subterm (fn
boehmes@36898
    56
    Const (@{const_name abs}, _) => true
boehmes@36898
    57
  | Const (@{const_name min}, _) => true
boehmes@36898
    58
  | Const (@{const_name max}, _) => true
boehmes@36898
    59
  | _ => false)
boehmes@36898
    60
boehmes@37786
    61
val unfold_abs_conv = Conv.rewr_conv (mk_meta_eq @{thm abs_if})
boehmes@37786
    62
val unfold_min_conv = Conv.rewr_conv (mk_meta_eq @{thm min_def})
boehmes@37786
    63
val unfold_max_conv = Conv.rewr_conv (mk_meta_eq @{thm max_def})
boehmes@36898
    64
boehmes@36898
    65
fun expand_conv cv = N.eta_expand_conv (K cv)
boehmes@36898
    66
fun expand2_conv cv = N.eta_expand_conv (N.eta_expand_conv (K cv))
boehmes@36898
    67
boehmes@36898
    68
fun unfold_def_conv ctxt ct =
boehmes@36898
    69
  (case Thm.term_of ct of
boehmes@36898
    70
    Const (@{const_name abs}, _) $ _ => unfold_abs_conv
boehmes@36898
    71
  | Const (@{const_name abs}, _) => expand_conv unfold_abs_conv ctxt
boehmes@36898
    72
  | Const (@{const_name min}, _) $ _ $ _ => unfold_min_conv
boehmes@36898
    73
  | Const (@{const_name min}, _) $ _ => expand_conv unfold_min_conv ctxt
boehmes@36898
    74
  | Const (@{const_name min}, _) => expand2_conv unfold_min_conv ctxt
boehmes@36898
    75
  | Const (@{const_name max}, _) $ _ $ _ => unfold_max_conv
boehmes@36898
    76
  | Const (@{const_name max}, _) $ _ => expand_conv unfold_max_conv ctxt
boehmes@36898
    77
  | Const (@{const_name max}, _) => expand2_conv unfold_max_conv ctxt
boehmes@36898
    78
  | _ => Conv.all_conv) ct
boehmes@36898
    79
boehmes@36898
    80
fun unfold_abs_min_max_defs ctxt thm =
boehmes@36898
    81
  if exists_abs_min_max (Thm.prop_of thm)
wenzelm@36936
    82
  then Conv.fconv_rule (Conv.top_conv unfold_def_conv ctxt) thm
boehmes@36898
    83
  else thm
boehmes@36898
    84
boehmes@36898
    85
boehmes@41059
    86
(** include additional facts **)
boehmes@36898
    87
boehmes@40161
    88
fun extra_norm has_datatypes irules ctxt =
boehmes@40161
    89
  irules
boehmes@39298
    90
  |> not has_datatypes ? add_pair_rules
boehmes@36898
    91
  |> add_fun_upd_rules
boehmes@40161
    92
  |> map (apsnd (unfold_abs_min_max_defs ctxt))
boehmes@36898
    93
  |> rpair ctxt
boehmes@36898
    94
boehmes@36898
    95
boehmes@36898
    96
boehmes@41059
    97
(* builtins *)
boehmes@36898
    98
boehmes@41059
    99
local
boehmes@41059
   100
  fun int_num _ i = SOME (string_of_int i)
boehmes@36899
   101
boehmes@41059
   102
  fun distinct _ _ [t] =
boehmes@41059
   103
        (case try HOLogic.dest_list t of
boehmes@41059
   104
          SOME (ts as _ :: _) => SOME ("distinct", ts)
boehmes@41059
   105
        | _ => NONE)
boehmes@41059
   106
    | distinct _ _ _ = NONE
boehmes@41059
   107
in
boehmes@36898
   108
boehmes@41059
   109
val setup =
boehmes@41059
   110
  B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
boehmes@41059
   111
  fold (B.add_builtin_fun' smtlibC) [
boehmes@41059
   112
    (@{const True}, "true"),
boehmes@41059
   113
    (@{const False}, "false"),
boehmes@41059
   114
 (* FIXME: we do not test if these constants are fully applied! *)
boehmes@41059
   115
    (@{const Not}, "not"),
boehmes@41059
   116
    (@{const HOL.conj}, "and"),
boehmes@41059
   117
    (@{const HOL.disj}, "or"),
boehmes@41059
   118
    (@{const HOL.implies}, "implies"),
boehmes@41059
   119
    (@{const HOL.eq (bool)}, "iff"),
boehmes@41059
   120
    (@{const HOL.eq ('a)}, "="),
boehmes@41059
   121
    (@{const If (bool)}, "if_then_else"),
boehmes@41059
   122
    (@{const If ('a)}, "ite"),
boehmes@41059
   123
    (@{const less (int)}, "<"),
boehmes@41059
   124
    (@{const less_eq (int)}, "<="),
boehmes@41059
   125
    (@{const uminus (int)}, "~"),
boehmes@41059
   126
    (@{const plus (int)}, "+"),
boehmes@41059
   127
    (@{const minus (int)}, "-"),
boehmes@41059
   128
    (@{const times (int)}, "*") ] #>
boehmes@41059
   129
  B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
boehmes@36898
   130
boehmes@41059
   131
end
boehmes@36898
   132
boehmes@36898
   133
boehmes@36898
   134
boehmes@41059
   135
(* serialization *)
boehmes@36898
   136
boehmes@41059
   137
(** header **)
boehmes@41059
   138
boehmes@41059
   139
fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
boehmes@36899
   140
boehmes@36899
   141
structure Logics = Generic_Data
boehmes@36899
   142
(
boehmes@36899
   143
  type T = (int * (term list -> string option)) list
boehmes@36899
   144
  val empty = []
boehmes@36899
   145
  val extend = I
wenzelm@39687
   146
  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
boehmes@36899
   147
)
boehmes@36899
   148
boehmes@41059
   149
fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
boehmes@36899
   150
boehmes@36899
   151
fun choose_logic ctxt ts =
boehmes@36899
   152
  let
boehmes@36899
   153
    fun choose [] = "AUFLIA"
boehmes@41059
   154
      | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
boehmes@41059
   155
  in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
boehmes@36899
   156
boehmes@36899
   157
boehmes@36899
   158
(* serialization *)
boehmes@36899
   159
boehmes@36898
   160
val add = Buffer.add
boehmes@36898
   161
fun sep f = add " " #> f
boehmes@36898
   162
fun enclose l r f = sep (add l #> f #> add r)
boehmes@36898
   163
val par = enclose "(" ")"
boehmes@36898
   164
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
boehmes@36898
   165
fun line f = f #> add "\n"
boehmes@36898
   166
boehmes@36898
   167
fun var i = add "?v" #> add (string_of_int i)
boehmes@36898
   168
boehmes@36898
   169
fun sterm l (T.SVar i) = sep (var (l - i - 1))
boehmes@36898
   170
  | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
boehmes@36898
   171
  | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
boehmes@40664
   172
  | sterm l (T.SQua (q, ss, ps, w, t)) =
boehmes@36898
   173
      let
boehmes@36898
   174
        val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
boehmes@36898
   175
        val vs = map_index (apfst (Integer.add l)) ss
boehmes@36898
   176
        fun var_decl (i, s) = par (var i #> sep (add s))
boehmes@36898
   177
        val sub = sterm (l + length ss)
boehmes@36898
   178
        fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
boehmes@36898
   179
        fun pats (T.SPat ts) = pat ":pat" ts
boehmes@36898
   180
          | pats (T.SNoPat ts) = pat ":nopat" ts
boehmes@40664
   181
        fun weight NONE = I
boehmes@40664
   182
          | weight (SOME i) =
boehmes@40664
   183
              sep (add ":weight { " #> add (string_of_int i) #> add " }")
boehmes@40664
   184
      in
boehmes@40664
   185
        par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
boehmes@40664
   186
      end
boehmes@36898
   187
boehmes@37155
   188
fun ssort sorts = sort fast_string_ord sorts
boehmes@37155
   189
fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
boehmes@37155
   190
boehmes@39298
   191
fun sdatatypes decls =
boehmes@39298
   192
  let
boehmes@39298
   193
    fun con (n, []) = add n
boehmes@39298
   194
      | con (n, sels) = par (add n #>
boehmes@39298
   195
          fold (fn (n, s) => sep (par (add n #> sep (add s)))) sels)
boehmes@39298
   196
    fun dtyp (n, decl) = add n #> fold (sep o con) decl
boehmes@39298
   197
  in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
boehmes@39298
   198
boehmes@39298
   199
fun serialize comments {header, sorts, dtyps, funcs} ts =
boehmes@36898
   200
  Buffer.empty
boehmes@36898
   201
  |> line (add "(benchmark Isabelle")
boehmes@36898
   202
  |> line (add ":status unknown")
boehmes@36899
   203
  |> fold (line o add) header
boehmes@36898
   204
  |> length sorts > 0 ?
boehmes@37155
   205
       line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts)))
boehmes@39298
   206
  |> fold sdatatypes dtyps
boehmes@36898
   207
  |> length funcs > 0 ? (
boehmes@36898
   208
       line (add ":extrafuns" #> add " (") #>
boehmes@36898
   209
       fold (fn (f, (ss, s)) =>
boehmes@37155
   210
         line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #>
boehmes@36898
   211
       line (add ")"))
boehmes@36898
   212
  |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
boehmes@36898
   213
  |> line (add ":formula true)")
boehmes@36898
   214
  |> fold (fn str => line (add "; " #> add str)) comments
boehmes@36898
   215
  |> Buffer.content
boehmes@36898
   216
boehmes@36898
   217
boehmes@36898
   218
boehmes@36899
   219
(** interfaces **)
boehmes@36898
   220
boehmes@36898
   221
val interface = {
boehmes@41059
   222
  class = smtlibC,
boehmes@40162
   223
  extra_norm = extra_norm,
boehmes@36898
   224
  translate = {
boehmes@36898
   225
    prefixes = {
boehmes@36898
   226
      sort_prefix = "S",
boehmes@36898
   227
      func_prefix = "f"},
boehmes@36899
   228
    header = choose_logic,
boehmes@41059
   229
    is_fol = true,
boehmes@41059
   230
    has_datatypes = false,
boehmes@36898
   231
    serialize = serialize}}
boehmes@36898
   232
boehmes@36898
   233
end