src/HOL/Tools/SMT/smtlib_interface.ML
author blanchet
Wed Sep 17 16:53:39 2014 +0200 (2014-09-17)
changeset 58360 dee1fd1cc631
parent 58061 3d060f43accb
child 58361 7f2b3b6f6ad1
permissions -rw-r--r--
added interface for CVC4 extensions
     1 (*  Title:      HOL/Tools/SMT/smtlib_interface.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Interface to SMT solvers based on the SMT-LIB 2 format.
     6 *)
     7 
     8 signature SMTLIB_INTERFACE =
     9 sig
    10   val smtlibC: SMT_Util.class
    11   val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
    12   val translate_config: Proof.context -> SMT_Translate.config
    13   val assert_index_of_name: string -> int
    14   val assert_prefix : string
    15 end;
    16 
    17 structure SMTLIB_Interface: SMTLIB_INTERFACE =
    18 struct
    19 
    20 val smtlibC = ["smtlib"]
    21 
    22 
    23 (* builtins *)
    24 
    25 local
    26   fun int_num _ i = SOME (string_of_int i)
    27 
    28   fun is_linear [t] = SMT_Util.is_number t
    29     | is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u
    30     | is_linear _ = false
    31 
    32   fun times _ _ ts =
    33     let val mk = Term.list_comb o pair @{const times (int)}
    34     in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
    35 in
    36 
    37 val setup_builtins =
    38   fold (SMT_Builtin.add_builtin_typ smtlibC) [
    39     (@{typ bool}, K (SOME "Bool"), K (K NONE)),
    40     (@{typ int}, K (SOME "Int"), int_num)] #>
    41   fold (SMT_Builtin.add_builtin_fun' smtlibC) [
    42     (@{const True}, "true"),
    43     (@{const False}, "false"),
    44     (@{const Not}, "not"),
    45     (@{const HOL.conj}, "and"),
    46     (@{const HOL.disj}, "or"),
    47     (@{const HOL.implies}, "=>"),
    48     (@{const HOL.eq ('a)}, "="),
    49     (@{const If ('a)}, "ite"),
    50     (@{const less (int)}, "<"),
    51     (@{const less_eq (int)}, "<="),
    52     (@{const uminus (int)}, "-"),
    53     (@{const plus (int)}, "+"),
    54     (@{const minus (int)}, "-")] #>
    55   SMT_Builtin.add_builtin_fun smtlibC
    56     (Term.dest_Const @{const times (int)}, times)
    57 
    58 end
    59 
    60 
    61 (* serialization *)
    62 
    63 (** logic **)
    64 
    65 fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
    66 
    67 structure Logics = Generic_Data
    68 (
    69   type T = (int * (term list -> string option)) list
    70   val empty = []
    71   val extend = I
    72   fun merge data = Ord_List.merge fst_int_ord data
    73 )
    74 
    75 fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
    76 
    77 fun choose_logic ctxt ts =
    78   let
    79     fun choose [] = "AUFLIA"
    80       | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
    81   in
    82     (case choose (Logics.get (Context.Proof ctxt)) of
    83       "" => "" (* for default Z3 logic, a subset of everything *)
    84     | logic => "(set-logic " ^ logic ^ ")\n")
    85   end
    86 
    87 
    88 (** serialization **)
    89 
    90 fun var i = "?v" ^ string_of_int i
    91 
    92 fun tree_of_sterm l (SMT_Translate.SVar i) = SMTLIB.Sym (var (l - i - 1))
    93   | tree_of_sterm _ (SMT_Translate.SApp (n, [])) = SMTLIB.Sym n
    94   | tree_of_sterm l (SMT_Translate.SApp (n, ts)) =
    95       SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
    96   | tree_of_sterm _ (SMT_Translate.SLet _) =
    97       raise Fail "SMT-LIB: unsupported let expression"
    98   | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
    99       let
   100         val l' = l + length ss
   101 
   102         fun quant_name SMT_Translate.SForall = "forall"
   103           | quant_name SMT_Translate.SExists = "exists"
   104 
   105         fun gen_trees_of_pat keyword ps =
   106           [SMTLIB.Key keyword, (case map (tree_of_sterm l') ps of [t] => t | ts => SMTLIB.S ts)]
   107         fun trees_of_pat (SMT_Translate.SPat ps) = gen_trees_of_pat "pattern" ps
   108           | trees_of_pat (SMT_Translate.SNoPat ps) = gen_trees_of_pat "no-pattern" ps
   109         fun tree_of_pats [] t = t
   110           | tree_of_pats pats t = SMTLIB.S (SMTLIB.Sym "!" :: t :: maps trees_of_pat pats)
   111 
   112         val vs = map_index (fn (i, ty) =>
   113           SMTLIB.S [SMTLIB.Sym (var (l + i)), SMTLIB.Sym ty]) ss
   114 
   115         val body = t
   116           |> tree_of_sterm l'
   117           |> tree_of_pats pats
   118       in
   119         SMTLIB.S [SMTLIB.Sym (quant_name q), SMTLIB.S vs, body]
   120       end
   121 
   122 
   123 fun sctrarg (sel, typ) = "(" ^ sel ^ " " ^ typ ^ ")"
   124 fun sctr (name, args) = enclose "(" ")" (space_implode " " (name :: map sctrarg args))
   125 fun sdatatype (name, ctrs) = enclose "(" ")" (space_implode " " (name :: map sctr ctrs))
   126 
   127 fun string_of_fun (f, (ss, s)) = f ^ " (" ^ space_implode " " ss ^ ") " ^ s
   128 
   129 fun named_sterm s t = SMTLIB.S [SMTLIB.Sym "!", t, SMTLIB.Key "named", SMTLIB.Sym s]
   130 
   131 val assert_prefix = "a"
   132 
   133 fun assert_name_of_index i = assert_prefix ^ string_of_int i
   134 fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
   135 
   136 fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
   137   Buffer.empty
   138   |> fold (Buffer.add o enclose "; " "\n") comments
   139   |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
   140   |> Buffer.add logic
   141   |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
   142   |> (if null dtyps then I
   143     else Buffer.add (enclose "(declare-datatypes () (" "))\n"
   144       (space_implode "\n  " (maps (map sdatatype) dtyps))))
   145   |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
   146       (sort (fast_string_ord o pairself fst) funcs)
   147   |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"
   148       (SMTLIB.str_of (named_sterm (assert_name_of_index i) (tree_of_sterm 0 t))))) (map_index I ts)
   149   |> Buffer.add "(check-sat)\n(get-proof)\n"
   150   |> Buffer.content
   151 
   152 (* interface *)
   153 
   154 fun translate_config ctxt = {
   155   logic = choose_logic ctxt,
   156   fp_kinds = [],
   157   serialize = serialize}
   158 
   159 val _ = Theory.setup (Context.theory_map
   160   (setup_builtins #>
   161    SMT_Translate.add_config (smtlibC, translate_config)))
   162 
   163 end;