1(*  Title:      HOL/Tools/SMT/smtlib_interface.ML
2    Author:     Sascha Boehme, TU Muenchen
3    Author:     Jasmin Blanchette, TU Muenchen
4
5Interface to SMT solvers based on the SMT-LIB 2 format.
6*)
7
8signature SMTLIB_INTERFACE =
9sig
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
17end;
18
19structure SMTLIB_Interface: SMTLIB_INTERFACE =
20struct
21
22val hoC = ["ho"]
23
24val smtlibC = ["smtlib"]   (* SMT-LIB 2 *)
25val hosmtlibC = smtlibC @ hoC   (* possibly SMT-LIB 3 *)
26
27
28(* builtins *)
29
30local
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
40in
41
42val setup_builtins =
43  SMT_Builtin.add_builtin_typ hosmtlibC
44    (\<^typ>\<open>'a => 'b\<close>, fn Type (\<^type_name>\<open>fun\<close>, Ts) => SOME ("->", Ts), K (K NONE)) #>
45  fold (SMT_Builtin.add_builtin_typ smtlibC) [
46    (\<^typ>\<open>bool\<close>, K (SOME ("Bool", [])), K (K NONE)),
47    (\<^typ>\<open>int\<close>, K (SOME ("Int", [])), int_num)] #>
48  fold (SMT_Builtin.add_builtin_fun' smtlibC) [
49    (\<^const>\<open>True\<close>, "true"),
50    (\<^const>\<open>False\<close>, "false"),
51    (\<^const>\<open>Not\<close>, "not"),
52    (\<^const>\<open>HOL.conj\<close>, "and"),
53    (\<^const>\<open>HOL.disj\<close>, "or"),
54    (\<^const>\<open>HOL.implies\<close>, "=>"),
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
65end
66
67
68(* serialization *)
69
70(** logic **)
71
72fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
73
74structure 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
82fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
83
84fun 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
97fun var i = "?v" ^ string_of_int i
98
99fun 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
130fun sctrarg (sel, typ) = "(" ^ sel ^ " " ^ typ ^ ")"
131fun sctr (name, args) = enclose "(" ")" (space_implode " " (name :: map sctrarg args))
132fun sdatatype (name, ctrs) = enclose "(" ")" (space_implode " " (name :: map sctr ctrs))
133
134fun string_of_fun (f, (ss, s)) = f ^ " (" ^ space_implode " " ss ^ ") " ^ s
135
136fun named_sterm s t = SMTLIB.S [SMTLIB.Sym "!", t, SMTLIB.Key "named", SMTLIB.Sym s]
137
138val assert_prefix = "a"
139
140fun assert_name_of_index i = assert_prefix ^ string_of_int i
141fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
142
143fun sdtyp (fp, dtyps) =
144  Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n"
145    (space_implode "\n  " (map sdatatype dtyps)))
146
147fun 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
168fun translate_config order ctxt = {
169  order = order,
170  logic = choose_logic ctxt,
171  fp_kinds = [],
172  serialize = serialize}
173
174val _ = 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
179end;
180