src/HOL/Tools/SMT/smtlib_interface.ML
author boehmes
Sun Dec 19 17:55:56 2010 +0100 (2010-12-19)
changeset 41280 a7de9d36f4f2
parent 41127 2ea84c8535c6
child 41281 679118e35378
permissions -rw-r--r--
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
hide internal constants z3div and z3mod;
rewrite div/mod to z3div/z3mod instead of adding extra rules characterizing div/mod in terms of z3div/z3mod
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@41124
     9
  val smtlibC: SMT_Utils.class
boehmes@41059
    10
  val add_logic: int * (term list -> string option) -> Context.generic ->
boehmes@36899
    11
    Context.generic
boehmes@41127
    12
  val translate_config: Proof.context -> SMT_Translate.config
boehmes@41059
    13
  val setup: theory -> theory
boehmes@36898
    14
end
boehmes@36898
    15
boehmes@36898
    16
structure SMTLIB_Interface: SMTLIB_INTERFACE =
boehmes@36898
    17
struct
boehmes@36898
    18
boehmes@41280
    19
structure U = SMT_Utils
boehmes@41059
    20
structure B = SMT_Builtin
boehmes@36898
    21
structure N = SMT_Normalize
boehmes@36898
    22
structure T = SMT_Translate
boehmes@36898
    23
boehmes@41059
    24
val smtlibC = ["smtlib"]
boehmes@36898
    25
boehmes@36898
    26
boehmes@41059
    27
(* builtins *)
boehmes@36898
    28
boehmes@41059
    29
local
boehmes@41059
    30
  fun int_num _ i = SOME (string_of_int i)
boehmes@36899
    31
boehmes@41280
    32
  fun is_linear [t] = U.is_number t
boehmes@41280
    33
    | is_linear [t, u] = U.is_number t orelse U.is_number u
boehmes@41280
    34
    | is_linear _ = false
boehmes@41280
    35
boehmes@41280
    36
  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
boehmes@41280
    37
boehmes@41127
    38
  fun distinct _ (Type (_, [Type (_, [T]), _])) [t] =
boehmes@41059
    39
        (case try HOLogic.dest_list t of
boehmes@41127
    40
          SOME (ts as _ :: _) =>
boehmes@41127
    41
            let
boehmes@41127
    42
              fun mkT U = replicate (length ts) U ---> @{typ bool}
boehmes@41127
    43
              val U = mkT T and U' = mkT (TVar (("'a", 0), @{sort type}))
boehmes@41127
    44
            in SOME ((("distinct", length ts), U), ts, U') end
boehmes@41059
    45
        | _ => NONE)
boehmes@41059
    46
    | distinct _ _ _ = NONE
boehmes@41059
    47
in
boehmes@36898
    48
boehmes@41072
    49
val setup_builtins =
boehmes@41059
    50
  B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
boehmes@41059
    51
  fold (B.add_builtin_fun' smtlibC) [
boehmes@41059
    52
    (@{const True}, "true"),
boehmes@41059
    53
    (@{const False}, "false"),
boehmes@41059
    54
    (@{const Not}, "not"),
boehmes@41059
    55
    (@{const HOL.conj}, "and"),
boehmes@41059
    56
    (@{const HOL.disj}, "or"),
boehmes@41059
    57
    (@{const HOL.implies}, "implies"),
boehmes@41059
    58
    (@{const HOL.eq (bool)}, "iff"),
boehmes@41059
    59
    (@{const HOL.eq ('a)}, "="),
boehmes@41059
    60
    (@{const If (bool)}, "if_then_else"),
boehmes@41059
    61
    (@{const If ('a)}, "ite"),
boehmes@41059
    62
    (@{const less (int)}, "<"),
boehmes@41059
    63
    (@{const less_eq (int)}, "<="),
boehmes@41059
    64
    (@{const uminus (int)}, "~"),
boehmes@41059
    65
    (@{const plus (int)}, "+"),
boehmes@41280
    66
    (@{const minus (int)}, "-") ] #>
boehmes@41280
    67
  B.add_builtin_fun smtlibC (Term.dest_Const @{const times (int)}, times) #>
boehmes@41059
    68
  B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
boehmes@36898
    69
boehmes@41059
    70
end
boehmes@36898
    71
boehmes@36898
    72
boehmes@41059
    73
(* serialization *)
boehmes@36898
    74
boehmes@41059
    75
(** header **)
boehmes@41059
    76
boehmes@41059
    77
fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
boehmes@36899
    78
boehmes@36899
    79
structure Logics = Generic_Data
boehmes@36899
    80
(
boehmes@36899
    81
  type T = (int * (term list -> string option)) list
boehmes@36899
    82
  val empty = []
boehmes@36899
    83
  val extend = I
wenzelm@39687
    84
  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
boehmes@36899
    85
)
boehmes@36899
    86
boehmes@41059
    87
fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
boehmes@36899
    88
boehmes@36899
    89
fun choose_logic ctxt ts =
boehmes@36899
    90
  let
boehmes@36899
    91
    fun choose [] = "AUFLIA"
boehmes@41059
    92
      | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
boehmes@41059
    93
  in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
boehmes@36899
    94
boehmes@36899
    95
boehmes@41072
    96
(** serialization **)
boehmes@36899
    97
boehmes@36898
    98
val add = Buffer.add
boehmes@36898
    99
fun sep f = add " " #> f
boehmes@36898
   100
fun enclose l r f = sep (add l #> f #> add r)
boehmes@36898
   101
val par = enclose "(" ")"
boehmes@36898
   102
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
boehmes@36898
   103
fun line f = f #> add "\n"
boehmes@36898
   104
boehmes@36898
   105
fun var i = add "?v" #> add (string_of_int i)
boehmes@36898
   106
boehmes@36898
   107
fun sterm l (T.SVar i) = sep (var (l - i - 1))
boehmes@36898
   108
  | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
boehmes@36898
   109
  | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
boehmes@40664
   110
  | sterm l (T.SQua (q, ss, ps, w, t)) =
boehmes@36898
   111
      let
boehmes@36898
   112
        val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
boehmes@36898
   113
        val vs = map_index (apfst (Integer.add l)) ss
boehmes@36898
   114
        fun var_decl (i, s) = par (var i #> sep (add s))
boehmes@36898
   115
        val sub = sterm (l + length ss)
boehmes@36898
   116
        fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
boehmes@36898
   117
        fun pats (T.SPat ts) = pat ":pat" ts
boehmes@36898
   118
          | pats (T.SNoPat ts) = pat ":nopat" ts
boehmes@40664
   119
        fun weight NONE = I
boehmes@40664
   120
          | weight (SOME i) =
boehmes@40664
   121
              sep (add ":weight { " #> add (string_of_int i) #> add " }")
boehmes@40664
   122
      in
boehmes@40664
   123
        par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
boehmes@40664
   124
      end
boehmes@36898
   125
boehmes@37155
   126
fun ssort sorts = sort fast_string_ord sorts
boehmes@37155
   127
fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
boehmes@37155
   128
boehmes@39298
   129
fun sdatatypes decls =
boehmes@39298
   130
  let
boehmes@39298
   131
    fun con (n, []) = add n
boehmes@39298
   132
      | con (n, sels) = par (add n #>
boehmes@39298
   133
          fold (fn (n, s) => sep (par (add n #> sep (add s)))) sels)
boehmes@39298
   134
    fun dtyp (n, decl) = add n #> fold (sep o con) decl
boehmes@39298
   135
  in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
boehmes@39298
   136
boehmes@39298
   137
fun serialize comments {header, sorts, dtyps, funcs} ts =
boehmes@36898
   138
  Buffer.empty
boehmes@36898
   139
  |> line (add "(benchmark Isabelle")
boehmes@36898
   140
  |> line (add ":status unknown")
boehmes@36899
   141
  |> fold (line o add) header
boehmes@36898
   142
  |> length sorts > 0 ?
boehmes@37155
   143
       line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts)))
boehmes@39298
   144
  |> fold sdatatypes dtyps
boehmes@36898
   145
  |> length funcs > 0 ? (
boehmes@36898
   146
       line (add ":extrafuns" #> add " (") #>
boehmes@36898
   147
       fold (fn (f, (ss, s)) =>
boehmes@37155
   148
         line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #>
boehmes@36898
   149
       line (add ")"))
boehmes@36898
   150
  |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
boehmes@36898
   151
  |> line (add ":formula true)")
boehmes@36898
   152
  |> fold (fn str => line (add "; " #> add str)) comments
boehmes@36898
   153
  |> Buffer.content
boehmes@36898
   154
boehmes@36898
   155
boehmes@41072
   156
(* interface *)
boehmes@36898
   157
boehmes@41127
   158
fun translate_config ctxt = {
boehmes@41127
   159
  prefixes = {
boehmes@41127
   160
    sort_prefix = "S",
boehmes@41127
   161
    func_prefix = "f"},
boehmes@41127
   162
  header = choose_logic ctxt,
boehmes@41127
   163
  is_fol = true,
boehmes@41127
   164
  has_datatypes = false,
boehmes@41127
   165
  serialize = serialize}
boehmes@36898
   166
boehmes@41127
   167
val setup = Context.theory_map (
boehmes@41127
   168
  setup_builtins #>
boehmes@41127
   169
  T.add_config (smtlibC, translate_config))
boehmes@41072
   170
boehmes@36898
   171
end