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