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