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