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