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