src/HOL/Tools/SMT/smtlib_interface.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 66551 4df6b0ae900d
child 67399 eab6ce8368fa
permissions -rw-r--r--
more symbols;
     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 hosmtlibC: SMT_Util.class
    12   val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
    13   val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
    14   val assert_name_of_index: int -> string
    15   val assert_index_of_name: string -> int
    16   val assert_prefix : string
    17 end;
    18 
    19 structure SMTLIB_Interface: SMTLIB_INTERFACE =
    20 struct
    21 
    22 val hoC = ["ho"]
    23 
    24 val smtlibC = ["smtlib"]   (* SMT-LIB 2 *)
    25 val hosmtlibC = smtlibC @ hoC   (* possibly SMT-LIB 3 *)
    26 
    27 
    28 (* builtins *)
    29 
    30 local
    31   fun int_num _ i = SOME (string_of_int i)
    32 
    33   fun is_linear [t] = SMT_Util.is_number t
    34     | is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u
    35     | is_linear _ = false
    36 
    37   fun times _ _ ts =
    38     let val mk = Term.list_comb o pair @{const times (int)}
    39     in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
    40 in
    41 
    42 val setup_builtins =
    43   SMT_Builtin.add_builtin_typ hosmtlibC
    44     (@{typ "'a => 'b"}, fn Type (@{type_name fun}, Ts) => SOME ("->", Ts), K (K NONE)) #>
    45   fold (SMT_Builtin.add_builtin_typ smtlibC) [
    46     (@{typ bool}, K (SOME ("Bool", [])), K (K NONE)),
    47     (@{typ int}, K (SOME ("Int", [])), int_num)] #>
    48   fold (SMT_Builtin.add_builtin_fun' smtlibC) [
    49     (@{const True}, "true"),
    50     (@{const False}, "false"),
    51     (@{const Not}, "not"),
    52     (@{const HOL.conj}, "and"),
    53     (@{const HOL.disj}, "or"),
    54     (@{const HOL.implies}, "=>"),
    55     (@{const HOL.eq ('a)}, "="),
    56     (@{const If ('a)}, "ite"),
    57     (@{const less (int)}, "<"),
    58     (@{const less_eq (int)}, "<="),
    59     (@{const uminus (int)}, "-"),
    60     (@{const plus (int)}, "+"),
    61     (@{const minus (int)}, "-")] #>
    62   SMT_Builtin.add_builtin_fun smtlibC
    63     (Term.dest_Const @{const times (int)}, times)
    64 
    65 end
    66 
    67 
    68 (* serialization *)
    69 
    70 (** logic **)
    71 
    72 fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
    73 
    74 structure Logics = Generic_Data
    75 (
    76   type T = (int * (term list -> string option)) list
    77   val empty = []
    78   val extend = I
    79   fun merge data = Ord_List.merge fst_int_ord data
    80 )
    81 
    82 fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
    83 
    84 fun choose_logic ctxt ts =
    85   let
    86     fun choose [] = "AUFLIA"
    87       | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
    88   in
    89     (case choose (Logics.get (Context.Proof ctxt)) of
    90       "" => "" (* for default Z3 logic, a subset of everything *)
    91     | logic => "(set-logic " ^ logic ^ ")\n")
    92   end
    93 
    94 
    95 (** serialization **)
    96 
    97 fun var i = "?v" ^ string_of_int i
    98 
    99 fun tree_of_sterm l (SMT_Translate.SVar (i, [])) = SMTLIB.Sym (var (l - i - 1))
   100   | tree_of_sterm l (SMT_Translate.SVar (i, ts)) =
   101       SMTLIB.S (SMTLIB.Sym (var (l - i - 1)) :: map (tree_of_sterm l) ts)
   102   | tree_of_sterm _ (SMT_Translate.SConst (n, [])) = SMTLIB.Sym n
   103   | tree_of_sterm l (SMT_Translate.SConst (n, ts)) =
   104       SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
   105   | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
   106       let
   107         val l' = l + length ss
   108 
   109         fun quant_name SMT_Translate.SForall = "forall"
   110           | quant_name SMT_Translate.SExists = "exists"
   111 
   112         fun gen_trees_of_pat keyword ps =
   113           [SMTLIB.Key keyword, SMTLIB.S (map (tree_of_sterm l') ps)]
   114         fun trees_of_pat (SMT_Translate.SPat ps) = gen_trees_of_pat "pattern" ps
   115           | trees_of_pat (SMT_Translate.SNoPat ps) = gen_trees_of_pat "no-pattern" ps
   116         fun tree_of_pats [] t = t
   117           | tree_of_pats pats t = SMTLIB.S (SMTLIB.Sym "!" :: t :: maps trees_of_pat pats)
   118 
   119         val vs = map_index (fn (i, ty) =>
   120           SMTLIB.S [SMTLIB.Sym (var (l + i)), SMTLIB.Sym ty]) ss
   121 
   122         val body = t
   123           |> tree_of_sterm l'
   124           |> tree_of_pats pats
   125       in
   126         SMTLIB.S [SMTLIB.Sym (quant_name q), SMTLIB.S vs, body]
   127       end
   128 
   129 
   130 fun sctrarg (sel, typ) = "(" ^ sel ^ " " ^ typ ^ ")"
   131 fun sctr (name, args) = enclose "(" ")" (space_implode " " (name :: map sctrarg args))
   132 fun sdatatype (name, ctrs) = enclose "(" ")" (space_implode " " (name :: map sctr ctrs))
   133 
   134 fun string_of_fun (f, (ss, s)) = f ^ " (" ^ space_implode " " ss ^ ") " ^ s
   135 
   136 fun named_sterm s t = SMTLIB.S [SMTLIB.Sym "!", t, SMTLIB.Key "named", SMTLIB.Sym s]
   137 
   138 val assert_prefix = "a"
   139 
   140 fun assert_name_of_index i = assert_prefix ^ string_of_int i
   141 fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
   142 
   143 fun sdtyp (fp, dtyps) =
   144   Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n"
   145     (space_implode "\n  " (map sdatatype dtyps)))
   146 
   147 fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
   148   let
   149     val unsat_core = member (op =) smt_options (":produce-unsat-cores", "true")
   150   in
   151     Buffer.empty
   152     |> fold (Buffer.add o enclose "; " "\n") comments
   153     |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
   154     |> Buffer.add logic
   155     |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
   156     |> fold sdtyp (AList.coalesce (op =) dtyps)
   157     |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
   158         (sort (fast_string_ord o apply2 fst) funcs)
   159     |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"
   160         (SMTLIB.str_of (named_sterm (assert_name_of_index i) (tree_of_sterm 0 t))))) (map_index I ts)
   161     |> Buffer.add "(check-sat)\n"
   162     |> Buffer.add (if unsat_core then "(get-unsat-core)\n" else "(get-proof)\n")
   163     |> Buffer.content
   164   end
   165 
   166 (* interface *)
   167 
   168 fun translate_config order ctxt = {
   169   order = order,
   170   logic = choose_logic ctxt,
   171   fp_kinds = [],
   172   serialize = serialize}
   173 
   174 val _ = Theory.setup (Context.theory_map
   175   (setup_builtins #>
   176    SMT_Translate.add_config (smtlibC, translate_config SMT_Util.First_Order) #>
   177    SMT_Translate.add_config (hosmtlibC, translate_config SMT_Util.Higher_Order)))
   178 
   179 end;