src/HOL/Tools/SMT/z3_interface.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59632 5980e75a204e
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/z3_interface.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Interface to Z3 based on a relaxed version of SMT-LIB.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@58061
     7
signature Z3_INTERFACE =
blanchet@56078
     8
sig
blanchet@58061
     9
  val smtlib_z3C: SMT_Util.class
blanchet@56078
    10
blanchet@56078
    11
  datatype sym = Sym of string * sym list
blanchet@56078
    12
  type mk_builtins = {
blanchet@56078
    13
    mk_builtin_typ: sym -> typ option,
blanchet@56078
    14
    mk_builtin_num: theory -> int -> typ -> cterm option,
blanchet@56078
    15
    mk_builtin_fun: theory -> sym -> cterm list -> cterm option }
blanchet@56078
    16
  val add_mk_builtins: mk_builtins -> Context.generic -> Context.generic
blanchet@56078
    17
  val mk_builtin_typ: Proof.context -> sym -> typ option
blanchet@56078
    18
  val mk_builtin_num: Proof.context -> int -> typ -> cterm option
blanchet@56078
    19
  val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option
blanchet@56078
    20
blanchet@56078
    21
  val is_builtin_theory_term: Proof.context -> term -> bool
blanchet@57229
    22
end;
blanchet@56078
    23
blanchet@58061
    24
structure Z3_Interface: Z3_INTERFACE =
blanchet@56078
    25
struct
blanchet@56078
    26
blanchet@58061
    27
val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
blanchet@56078
    28
blanchet@56078
    29
blanchet@56078
    30
(* interface *)
blanchet@56078
    31
blanchet@56078
    32
local
blanchet@56078
    33
  fun translate_config ctxt =
blanchet@58360
    34
    {logic = K "", fp_kinds = [BNF_Util.Least_FP],
blanchet@58061
    35
     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
blanchet@56078
    36
blanchet@56078
    37
  fun is_div_mod @{const div (int)} = true
blanchet@56078
    38
    | is_div_mod @{const mod (int)} = true
blanchet@56078
    39
    | is_div_mod _ = false
blanchet@56078
    40
blanchet@56103
    41
  val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of)
blanchet@56078
    42
blanchet@56078
    43
  fun add_div_mod _ (thms, extra_thms) =
blanchet@56078
    44
    if have_int_div_mod thms orelse have_int_div_mod extra_thms then
blanchet@56101
    45
      (thms, @{thms div_as_z3div mod_as_z3mod} @ extra_thms)
blanchet@56078
    46
    else (thms, extra_thms)
blanchet@56078
    47
blanchet@56078
    48
  val setup_builtins =
blanchet@58061
    49
    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #>
blanchet@58061
    50
    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
blanchet@58061
    51
    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
blanchet@56078
    52
in
blanchet@56078
    53
blanchet@56078
    54
val _ = Theory.setup (Context.theory_map (
blanchet@56078
    55
  setup_builtins #>
blanchet@58061
    56
  SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #>
blanchet@58061
    57
  SMT_Translate.add_config (smtlib_z3C, translate_config)))
blanchet@56078
    58
blanchet@56078
    59
end
blanchet@56078
    60
blanchet@56078
    61
blanchet@56078
    62
(* constructors *)
blanchet@56078
    63
blanchet@56078
    64
datatype sym = Sym of string * sym list
blanchet@56078
    65
blanchet@56078
    66
blanchet@56078
    67
(** additional constructors **)
blanchet@56078
    68
blanchet@56078
    69
type mk_builtins = {
blanchet@56078
    70
  mk_builtin_typ: sym -> typ option,
blanchet@56078
    71
  mk_builtin_num: theory -> int -> typ -> cterm option,
blanchet@56078
    72
  mk_builtin_fun: theory -> sym -> cterm list -> cterm option }
blanchet@56078
    73
blanchet@56078
    74
fun chained _ [] = NONE
blanchet@56078
    75
  | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
blanchet@56078
    76
blanchet@56078
    77
fun chained_mk_builtin_typ bs sym =
blanchet@56078
    78
  chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs
blanchet@56078
    79
blanchet@56078
    80
fun chained_mk_builtin_num ctxt bs i T =
blanchet@56078
    81
  let val thy = Proof_Context.theory_of ctxt
blanchet@56078
    82
  in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end
blanchet@56078
    83
blanchet@56078
    84
fun chained_mk_builtin_fun ctxt bs s cts =
blanchet@56078
    85
  let val thy = Proof_Context.theory_of ctxt
blanchet@56078
    86
  in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end
blanchet@56078
    87
blanchet@56078
    88
fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
blanchet@56078
    89
blanchet@56078
    90
structure Mk_Builtins = Generic_Data
blanchet@56078
    91
(
blanchet@56078
    92
  type T = (int * mk_builtins) list
blanchet@56078
    93
  val empty = []
blanchet@56078
    94
  val extend = I
blanchet@56078
    95
  fun merge data = Ord_List.merge fst_int_ord data
blanchet@56078
    96
)
blanchet@56078
    97
blanchet@56103
    98
fun add_mk_builtins mk = Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
blanchet@56078
    99
blanchet@56078
   100
fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
blanchet@56078
   101
blanchet@56078
   102
blanchet@56078
   103
(** basic and additional constructors **)
blanchet@56078
   104
blanchet@56078
   105
fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool}
blanchet@56078
   106
  | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
blanchet@56078
   107
  | mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}  (*FIXME: legacy*)
blanchet@56078
   108
  | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}  (*FIXME: legacy*)
blanchet@56078
   109
  | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym
blanchet@56078
   110
blanchet@56078
   111
fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i)
blanchet@56078
   112
  | mk_builtin_num ctxt i T =
blanchet@56078
   113
      chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
blanchet@56078
   114
wenzelm@59621
   115
val mk_true = Thm.global_cterm_of @{theory} (@{const Not} $ @{const False})
wenzelm@59621
   116
val mk_false = Thm.global_cterm_of @{theory} @{const False}
wenzelm@59621
   117
val mk_not = Thm.apply (Thm.global_cterm_of @{theory} @{const Not})
wenzelm@59621
   118
val mk_implies = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.implies})
wenzelm@59621
   119
val mk_iff = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.eq (bool)})
wenzelm@59621
   120
val conj = Thm.global_cterm_of @{theory} @{const HOL.conj}
wenzelm@59621
   121
val disj = Thm.global_cterm_of @{theory} @{const HOL.disj}
blanchet@56078
   122
blanchet@56078
   123
fun mk_nary _ cu [] = cu
blanchet@56078
   124
  | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
blanchet@56078
   125
blanchet@58061
   126
val eq = SMT_Util.mk_const_pat @{theory} @{const_name HOL.eq} SMT_Util.destT1
blanchet@58061
   127
fun mk_eq ct cu = Thm.mk_binop (SMT_Util.instT' ct eq) ct cu
blanchet@56078
   128
blanchet@56078
   129
val if_term =
blanchet@58061
   130
  SMT_Util.mk_const_pat @{theory} @{const_name If} (SMT_Util.destT1 o SMT_Util.destT2)
blanchet@58061
   131
fun mk_if cc ct = Thm.mk_binop (Thm.apply (SMT_Util.instT' ct if_term) cc) ct
blanchet@56078
   132
blanchet@58061
   133
val access = SMT_Util.mk_const_pat @{theory} @{const_name fun_app} SMT_Util.destT1
blanchet@58061
   134
fun mk_access array = Thm.apply (SMT_Util.instT' array access) array
blanchet@56078
   135
blanchet@56090
   136
val update =
blanchet@58061
   137
  SMT_Util.mk_const_pat @{theory} @{const_name fun_upd} (Thm.dest_ctyp o SMT_Util.destT1)
blanchet@56078
   138
fun mk_update array index value =
wenzelm@59586
   139
  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
blanchet@58061
   140
  in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
blanchet@56078
   141
wenzelm@59621
   142
val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (int)})
wenzelm@59621
   143
val add = Thm.global_cterm_of @{theory} @{const plus (int)}
blanchet@56078
   144
val int0 = Numeral.mk_cnumber @{ctyp int} 0
wenzelm@59621
   145
val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (int)})
wenzelm@59621
   146
val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (int)})
wenzelm@59621
   147
val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3div})
wenzelm@59621
   148
val mk_mod = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3mod})
wenzelm@59621
   149
val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (int)})
wenzelm@59621
   150
val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (int)})
blanchet@56078
   151
blanchet@56078
   152
fun mk_builtin_fun ctxt sym cts =
blanchet@56078
   153
  (case (sym, cts) of
blanchet@56078
   154
    (Sym ("true", _), []) => SOME mk_true
blanchet@56078
   155
  | (Sym ("false", _), []) => SOME mk_false
blanchet@56078
   156
  | (Sym ("not", _), [ct]) => SOME (mk_not ct)
blanchet@56078
   157
  | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts)
blanchet@56078
   158
  | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts)
blanchet@56078
   159
  | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
blanchet@56078
   160
  | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
blanchet@56078
   161
  | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
blanchet@56078
   162
  | (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu))
blanchet@56078
   163
  | (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3)
blanchet@56078
   164
  | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *)
blanchet@56078
   165
  | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu)
blanchet@56078
   166
  | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
blanchet@56078
   167
  | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
blanchet@56078
   168
  | _ =>
wenzelm@59586
   169
    (case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of
blanchet@56078
   170
      (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
blanchet@56078
   171
    | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
blanchet@56078
   172
    | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
blanchet@56078
   173
    | (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu)
blanchet@56078
   174
    | (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu)
blanchet@56078
   175
    | (Sym ("mod", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mod ct cu)
blanchet@56078
   176
    | (Sym ("<", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt ct cu)
blanchet@56078
   177
    | (Sym ("<=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le ct cu)
blanchet@56078
   178
    | (Sym (">", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt cu ct)
blanchet@56078
   179
    | (Sym (">=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le cu ct)
blanchet@56078
   180
    | _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts))
blanchet@56078
   181
blanchet@56078
   182
blanchet@56078
   183
(* abstraction *)
blanchet@56078
   184
blanchet@56078
   185
fun is_builtin_theory_term ctxt t =
blanchet@58061
   186
  if SMT_Builtin.is_builtin_num ctxt t then true
blanchet@56078
   187
  else
blanchet@56078
   188
    (case Term.strip_comb t of
blanchet@58061
   189
      (Const c, ts) => SMT_Builtin.is_builtin_fun ctxt c ts
blanchet@56078
   190
    | _ => false)
blanchet@56078
   191
blanchet@57229
   192
end;