src/HOL/Tools/SMT/z3_interface.ML
author boehmes
Wed May 23 16:03:38 2012 +0200 (2012-05-23)
changeset 47965 8ba6438557bc
parent 46497 89ccf66aa73d
child 49720 6279490e0438
permissions -rw-r--r--
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes@36898
     1
(*  Title:      HOL/Tools/SMT/z3_interface.ML
boehmes@36898
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36898
     3
boehmes@36898
     4
Interface to Z3 based on a relaxed version of SMT-LIB.
boehmes@36898
     5
*)
boehmes@36898
     6
boehmes@36898
     7
signature Z3_INTERFACE =
boehmes@36898
     8
sig
boehmes@41124
     9
  val smtlib_z3C: SMT_Utils.class
boehmes@41059
    10
  val setup: theory -> theory
boehmes@36898
    11
boehmes@36899
    12
  datatype sym = Sym of string * sym list
boehmes@36899
    13
  type mk_builtins = {
boehmes@36899
    14
    mk_builtin_typ: sym -> typ option,
boehmes@36899
    15
    mk_builtin_num: theory -> int -> typ -> cterm option,
boehmes@36899
    16
    mk_builtin_fun: theory -> sym -> cterm list -> cterm option }
boehmes@36899
    17
  val add_mk_builtins: mk_builtins -> Context.generic -> Context.generic
boehmes@36899
    18
  val mk_builtin_typ: Proof.context -> sym -> typ option
boehmes@36899
    19
  val mk_builtin_num: Proof.context -> int -> typ -> cterm option
boehmes@36899
    20
  val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option
boehmes@36899
    21
boehmes@36899
    22
  val is_builtin_theory_term: Proof.context -> term -> bool
boehmes@36898
    23
end
boehmes@36898
    24
boehmes@36898
    25
structure Z3_Interface: Z3_INTERFACE =
boehmes@36898
    26
struct
boehmes@36898
    27
boehmes@41059
    28
val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
boehmes@36898
    29
boehmes@36898
    30
boehmes@36899
    31
boehmes@41059
    32
(* interface *)
boehmes@36899
    33
boehmes@36899
    34
local
boehmes@41127
    35
  fun translate_config ctxt =
boehmes@41127
    36
    let
boehmes@41127
    37
      val {prefixes, header, is_fol, serialize, ...} =
boehmes@41127
    38
        SMTLIB_Interface.translate_config ctxt
boehmes@41127
    39
    in
boehmes@41127
    40
      {prefixes=prefixes, header=header, is_fol=is_fol, serialize=serialize,
boehmes@41127
    41
        has_datatypes=true}
boehmes@41127
    42
    end
boehmes@36899
    43
boehmes@41302
    44
  fun is_div_mod @{const div (int)} = true
boehmes@41302
    45
    | is_div_mod @{const mod (int)} = true
boehmes@41280
    46
    | is_div_mod _ = false
boehmes@41280
    47
boehmes@41302
    48
  val div_by_z3div = @{lemma
boehmes@41302
    49
    "ALL k l. k div l = (
boehmes@41280
    50
      if k = 0 | l = 0 then 0
boehmes@41280
    51
      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l
boehmes@41280
    52
      else z3div (-k) (-l))"
boehmes@41280
    53
    by (simp add: SMT.z3div_def)}
boehmes@37151
    54
boehmes@41302
    55
  val mod_by_z3mod = @{lemma
boehmes@41302
    56
    "ALL k l. k mod l = (
boehmes@41280
    57
      if l = 0 then k
boehmes@41280
    58
      else if k = 0 then 0
boehmes@41280
    59
      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l
boehmes@41280
    60
      else - z3mod (-k) (-l))"
boehmes@41280
    61
    by (simp add: z3mod_def)}
boehmes@37151
    62
boehmes@41302
    63
  val have_int_div_mod =
boehmes@41302
    64
    exists (Term.exists_subterm is_div_mod o Thm.prop_of)
boehmes@41280
    65
boehmes@41302
    66
  fun add_div_mod _ (thms, extra_thms) =
boehmes@41302
    67
    if have_int_div_mod thms orelse have_int_div_mod extra_thms then
boehmes@41302
    68
      (thms, div_by_z3div :: mod_by_z3mod :: extra_thms)
boehmes@41302
    69
    else (thms, extra_thms)
boehmes@41072
    70
boehmes@41072
    71
  val setup_builtins =
boehmes@41691
    72
    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #>
boehmes@41691
    73
    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
boehmes@41691
    74
    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
boehmes@36899
    75
in
boehmes@36899
    76
boehmes@41126
    77
val setup = Context.theory_map (
boehmes@41126
    78
  setup_builtins #>
boehmes@41302
    79
  SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #>
boehmes@41127
    80
  SMT_Translate.add_config (smtlib_z3C, translate_config))
boehmes@41072
    81
boehmes@36898
    82
end
boehmes@36899
    83
boehmes@36899
    84
boehmes@36899
    85
boehmes@41059
    86
(* constructors *)
boehmes@36899
    87
boehmes@36899
    88
datatype sym = Sym of string * sym list
boehmes@36899
    89
boehmes@36899
    90
boehmes@41059
    91
(** additional constructors **)
boehmes@36899
    92
boehmes@36899
    93
type mk_builtins = {
boehmes@36899
    94
  mk_builtin_typ: sym -> typ option,
boehmes@36899
    95
  mk_builtin_num: theory -> int -> typ -> cterm option,
boehmes@36899
    96
  mk_builtin_fun: theory -> sym -> cterm list -> cterm option }
boehmes@36899
    97
boehmes@36899
    98
fun chained _ [] = NONE
boehmes@36899
    99
  | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
boehmes@36899
   100
boehmes@36899
   101
fun chained_mk_builtin_typ bs sym =
boehmes@36899
   102
  chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs
boehmes@36899
   103
boehmes@36899
   104
fun chained_mk_builtin_num ctxt bs i T =
wenzelm@42361
   105
  let val thy = Proof_Context.theory_of ctxt
boehmes@36899
   106
  in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end
boehmes@36899
   107
boehmes@36899
   108
fun chained_mk_builtin_fun ctxt bs s cts =
wenzelm@42361
   109
  let val thy = Proof_Context.theory_of ctxt
boehmes@36899
   110
  in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end
boehmes@36899
   111
boehmes@41059
   112
fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
boehmes@41059
   113
boehmes@36899
   114
structure Mk_Builtins = Generic_Data
boehmes@36899
   115
(
boehmes@36899
   116
  type T = (int * mk_builtins) list
boehmes@36899
   117
  val empty = []
boehmes@36899
   118
  val extend = I
wenzelm@41473
   119
  fun merge data = Ord_List.merge fst_int_ord data
boehmes@36899
   120
)
boehmes@36899
   121
boehmes@36899
   122
fun add_mk_builtins mk =
wenzelm@39687
   123
  Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
boehmes@36899
   124
boehmes@36899
   125
fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
boehmes@36899
   126
boehmes@36899
   127
boehmes@41059
   128
(** basic and additional constructors **)
boehmes@36899
   129
boehmes@36899
   130
fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
boehmes@40516
   131
  | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
boehmes@40516
   132
  | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}  (*FIXME: delete*)
boehmes@36899
   133
  | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym
boehmes@36899
   134
boehmes@36899
   135
fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i)
boehmes@36899
   136
  | mk_builtin_num ctxt i T =
boehmes@36899
   137
      chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
boehmes@36899
   138
boehmes@40579
   139
val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
boehmes@40579
   140
val mk_false = Thm.cterm_of @{theory} @{const False}
wenzelm@46497
   141
val mk_not = Thm.apply (Thm.cterm_of @{theory} @{const Not})
boehmes@40579
   142
val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies})
boehmes@40579
   143
val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)})
boehmes@40579
   144
val conj = Thm.cterm_of @{theory} @{const HOL.conj}
boehmes@40579
   145
val disj = Thm.cterm_of @{theory} @{const HOL.disj}
boehmes@36899
   146
boehmes@36899
   147
fun mk_nary _ cu [] = cu
boehmes@36899
   148
  | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
boehmes@36899
   149
boehmes@41691
   150
val eq = SMT_Utils.mk_const_pat @{theory} @{const_name HOL.eq} SMT_Utils.destT1
boehmes@41691
   151
fun mk_eq ct cu = Thm.mk_binop (SMT_Utils.instT' ct eq) ct cu
boehmes@36899
   152
boehmes@41691
   153
val if_term =
boehmes@41691
   154
  SMT_Utils.mk_const_pat @{theory} @{const_name If}
boehmes@41691
   155
    (SMT_Utils.destT1 o SMT_Utils.destT2)
boehmes@41691
   156
fun mk_if cc ct cu =
wenzelm@46497
   157
  Thm.mk_binop (Thm.apply (SMT_Utils.instT' ct if_term) cc) ct cu
boehmes@36899
   158
boehmes@41691
   159
val nil_term =
boehmes@41691
   160
  SMT_Utils.mk_const_pat @{theory} @{const_name Nil} SMT_Utils.destT1
boehmes@41691
   161
val cons_term =
boehmes@41691
   162
  SMT_Utils.mk_const_pat @{theory} @{const_name Cons} SMT_Utils.destT1
boehmes@36899
   163
fun mk_list cT cts =
boehmes@41691
   164
  fold_rev (Thm.mk_binop (SMT_Utils.instT cT cons_term)) cts
boehmes@41691
   165
    (SMT_Utils.instT cT nil_term)
boehmes@36899
   166
boehmes@41691
   167
val distinct = SMT_Utils.mk_const_pat @{theory} @{const_name distinct}
boehmes@41691
   168
  (SMT_Utils.destT1 o SMT_Utils.destT1)
boehmes@36899
   169
fun mk_distinct [] = mk_true
boehmes@36899
   170
  | mk_distinct (cts as (ct :: _)) =
wenzelm@46497
   171
      Thm.apply (SMT_Utils.instT' ct distinct)
boehmes@41691
   172
        (mk_list (Thm.ctyp_of_term ct) cts)
boehmes@36899
   173
boehmes@41691
   174
val access =
boehmes@41691
   175
  SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} SMT_Utils.destT1
wenzelm@46497
   176
fun mk_access array = Thm.apply (SMT_Utils.instT' array access) array
boehmes@36899
   177
boehmes@41691
   178
val update = SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd}
boehmes@41691
   179
  (Thm.dest_ctyp o SMT_Utils.destT1)
boehmes@36899
   180
fun mk_update array index value =
boehmes@36899
   181
  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
boehmes@41691
   182
  in
wenzelm@46497
   183
    Thm.apply (Thm.mk_binop (SMT_Utils.instTs cTs update) array index) value
boehmes@41691
   184
  end
boehmes@36899
   185
wenzelm@46497
   186
val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
boehmes@47965
   187
val add = Thm.cterm_of @{theory} @{const plus (int)}
boehmes@47965
   188
val int0 = Numeral.mk_cnumber @{ctyp int} 0
boehmes@40579
   189
val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
boehmes@40579
   190
val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
boehmes@40579
   191
val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div})
boehmes@40579
   192
val mk_mod = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3mod})
boehmes@40579
   193
val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (int)})
boehmes@40579
   194
val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (int)})
boehmes@36899
   195
boehmes@36899
   196
fun mk_builtin_fun ctxt sym cts =
boehmes@36899
   197
  (case (sym, cts) of
boehmes@36899
   198
    (Sym ("true", _), []) => SOME mk_true
boehmes@36899
   199
  | (Sym ("false", _), []) => SOME mk_false
boehmes@36899
   200
  | (Sym ("not", _), [ct]) => SOME (mk_not ct)
boehmes@40579
   201
  | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts)
boehmes@40579
   202
  | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts)
boehmes@36899
   203
  | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
boehmes@36899
   204
  | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
boehmes@36899
   205
  | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
boehmes@36899
   206
  | (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu))
boehmes@41761
   207
  | (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3)
boehmes@41761
   208
  | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *)
boehmes@36899
   209
  | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu)
boehmes@36899
   210
  | (Sym ("distinct", _), _) => SOME (mk_distinct cts)
wenzelm@46497
   211
  | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
boehmes@36899
   212
  | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
boehmes@36899
   213
  | _ =>
boehmes@36899
   214
    (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
boehmes@47965
   215
      (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
boehmes@36899
   216
    | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
boehmes@36899
   217
    | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
boehmes@36899
   218
    | (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu)
boehmes@37151
   219
    | (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu)
boehmes@37151
   220
    | (Sym ("mod", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mod ct cu)
boehmes@36899
   221
    | (Sym ("<", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt ct cu)
boehmes@36899
   222
    | (Sym ("<=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le ct cu)
boehmes@36899
   223
    | (Sym (">", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt cu ct)
boehmes@36899
   224
    | (Sym (">=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le cu ct)
boehmes@36899
   225
    | _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts))
boehmes@36899
   226
boehmes@36899
   227
boehmes@36899
   228
boehmes@41059
   229
(* abstraction *)
boehmes@36899
   230
boehmes@36899
   231
fun is_builtin_theory_term ctxt t =
boehmes@41691
   232
  if SMT_Builtin.is_builtin_num ctxt t then true
boehmes@41059
   233
  else
boehmes@41059
   234
    (case Term.strip_comb t of
boehmes@41691
   235
      (Const c, ts) => SMT_Builtin.is_builtin_fun ctxt c ts
boehmes@41059
   236
    | _ => false)
boehmes@36899
   237
boehmes@36899
   238
end