blanchet@58058: (* Title: HOL/Library/Old_SMT/old_z3_interface.ML boehmes@36898: Author: Sascha Boehme, TU Muenchen boehmes@36898: boehmes@36898: Interface to Z3 based on a relaxed version of SMT-LIB. boehmes@36898: *) boehmes@36898: blanchet@58058: signature OLD_Z3_INTERFACE = boehmes@36898: sig blanchet@58058: val smtlib_z3C: Old_SMT_Utils.class boehmes@41059: val setup: theory -> theory boehmes@36898: boehmes@36899: datatype sym = Sym of string * sym list boehmes@36899: type mk_builtins = { boehmes@36899: mk_builtin_typ: sym -> typ option, boehmes@36899: mk_builtin_num: theory -> int -> typ -> cterm option, boehmes@36899: mk_builtin_fun: theory -> sym -> cterm list -> cterm option } boehmes@36899: val add_mk_builtins: mk_builtins -> Context.generic -> Context.generic boehmes@36899: val mk_builtin_typ: Proof.context -> sym -> typ option boehmes@36899: val mk_builtin_num: Proof.context -> int -> typ -> cterm option boehmes@36899: val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option boehmes@36899: boehmes@36899: val is_builtin_theory_term: Proof.context -> term -> bool boehmes@36898: end boehmes@36898: blanchet@58058: structure Old_Z3_Interface: OLD_Z3_INTERFACE = boehmes@36898: struct boehmes@36898: blanchet@58058: val smtlib_z3C = Old_SMTLIB_Interface.smtlibC @ ["z3"] boehmes@36898: boehmes@36898: boehmes@36899: boehmes@41059: (* interface *) boehmes@36899: boehmes@36899: local boehmes@41127: fun translate_config ctxt = boehmes@41127: let boehmes@41127: val {prefixes, header, is_fol, serialize, ...} = blanchet@58058: Old_SMTLIB_Interface.translate_config ctxt boehmes@41127: in boehmes@41127: {prefixes=prefixes, header=header, is_fol=is_fol, serialize=serialize, boehmes@41127: has_datatypes=true} boehmes@41127: end boehmes@36899: boehmes@41302: fun is_div_mod @{const div (int)} = true boehmes@41302: | is_div_mod @{const mod (int)} = true boehmes@41280: | is_div_mod _ = false boehmes@41280: boehmes@41302: val div_by_z3div = @{lemma boehmes@41302: "ALL k l. k div l = ( boehmes@41280: if k = 0 | l = 0 then 0 boehmes@41280: else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l boehmes@41280: else z3div (-k) (-l))" blanchet@58057: by (simp add: z3div_def)} boehmes@37151: boehmes@41302: val mod_by_z3mod = @{lemma boehmes@41302: "ALL k l. k mod l = ( boehmes@41280: if l = 0 then k boehmes@41280: else if k = 0 then 0 boehmes@41280: else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l boehmes@41280: else - z3mod (-k) (-l))" boehmes@41280: by (simp add: z3mod_def)} boehmes@37151: boehmes@41302: val have_int_div_mod = boehmes@41302: exists (Term.exists_subterm is_div_mod o Thm.prop_of) boehmes@41280: boehmes@41302: fun add_div_mod _ (thms, extra_thms) = boehmes@41302: if have_int_div_mod thms orelse have_int_div_mod extra_thms then boehmes@41302: (thms, div_by_z3div :: mod_by_z3mod :: extra_thms) boehmes@41302: else (thms, extra_thms) boehmes@41072: boehmes@41072: val setup_builtins = blanchet@58058: Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #> blanchet@58058: Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #> blanchet@58058: Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod") boehmes@36899: in boehmes@36899: boehmes@41126: val setup = Context.theory_map ( boehmes@41126: setup_builtins #> blanchet@58058: Old_SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #> blanchet@58058: Old_SMT_Translate.add_config (smtlib_z3C, translate_config)) boehmes@41072: boehmes@36898: end boehmes@36899: boehmes@36899: boehmes@36899: boehmes@41059: (* constructors *) boehmes@36899: boehmes@36899: datatype sym = Sym of string * sym list boehmes@36899: boehmes@36899: boehmes@41059: (** additional constructors **) boehmes@36899: boehmes@36899: type mk_builtins = { boehmes@36899: mk_builtin_typ: sym -> typ option, boehmes@36899: mk_builtin_num: theory -> int -> typ -> cterm option, boehmes@36899: mk_builtin_fun: theory -> sym -> cterm list -> cterm option } boehmes@36899: boehmes@36899: fun chained _ [] = NONE boehmes@36899: | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs) boehmes@36899: boehmes@36899: fun chained_mk_builtin_typ bs sym = boehmes@36899: chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs boehmes@36899: boehmes@36899: fun chained_mk_builtin_num ctxt bs i T = wenzelm@42361: let val thy = Proof_Context.theory_of ctxt boehmes@36899: in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end boehmes@36899: boehmes@36899: fun chained_mk_builtin_fun ctxt bs s cts = wenzelm@42361: let val thy = Proof_Context.theory_of ctxt boehmes@36899: in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end boehmes@36899: boehmes@41059: fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) boehmes@41059: boehmes@36899: structure Mk_Builtins = Generic_Data boehmes@36899: ( boehmes@36899: type T = (int * mk_builtins) list boehmes@36899: val empty = [] boehmes@36899: val extend = I wenzelm@41473: fun merge data = Ord_List.merge fst_int_ord data boehmes@36899: ) boehmes@36899: boehmes@36899: fun add_mk_builtins mk = wenzelm@39687: Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) boehmes@36899: boehmes@36899: fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt)) boehmes@36899: boehmes@36899: boehmes@41059: (** basic and additional constructors **) boehmes@36899: blanchet@49720: fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool} boehmes@40516: | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int} blanchet@49720: | mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool} (*FIXME: legacy*) blanchet@49720: | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: legacy*) boehmes@36899: | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym boehmes@36899: boehmes@36899: fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i) boehmes@36899: | mk_builtin_num ctxt i T = boehmes@36899: chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T boehmes@36899: boehmes@40579: val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False}) boehmes@40579: val mk_false = Thm.cterm_of @{theory} @{const False} wenzelm@46497: val mk_not = Thm.apply (Thm.cterm_of @{theory} @{const Not}) boehmes@40579: val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies}) boehmes@40579: val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)}) boehmes@40579: val conj = Thm.cterm_of @{theory} @{const HOL.conj} boehmes@40579: val disj = Thm.cterm_of @{theory} @{const HOL.disj} boehmes@36899: boehmes@36899: fun mk_nary _ cu [] = cu boehmes@36899: | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) boehmes@36899: blanchet@58058: val eq = Old_SMT_Utils.mk_const_pat @{theory} @{const_name HOL.eq} Old_SMT_Utils.destT1 blanchet@58058: fun mk_eq ct cu = Thm.mk_binop (Old_SMT_Utils.instT' ct eq) ct cu boehmes@36899: boehmes@41691: val if_term = blanchet@58058: Old_SMT_Utils.mk_const_pat @{theory} @{const_name If} blanchet@58058: (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT2) boehmes@41691: fun mk_if cc ct cu = blanchet@58058: Thm.mk_binop (Thm.apply (Old_SMT_Utils.instT' ct if_term) cc) ct cu boehmes@36899: boehmes@41691: val nil_term = blanchet@58058: Old_SMT_Utils.mk_const_pat @{theory} @{const_name Nil} Old_SMT_Utils.destT1 boehmes@41691: val cons_term = blanchet@58058: Old_SMT_Utils.mk_const_pat @{theory} @{const_name Cons} Old_SMT_Utils.destT1 boehmes@36899: fun mk_list cT cts = blanchet@58058: fold_rev (Thm.mk_binop (Old_SMT_Utils.instT cT cons_term)) cts blanchet@58058: (Old_SMT_Utils.instT cT nil_term) boehmes@36899: blanchet@58058: val distinct = Old_SMT_Utils.mk_const_pat @{theory} @{const_name distinct} blanchet@58058: (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1) boehmes@36899: fun mk_distinct [] = mk_true boehmes@36899: | mk_distinct (cts as (ct :: _)) = blanchet@58058: Thm.apply (Old_SMT_Utils.instT' ct distinct) boehmes@41691: (mk_list (Thm.ctyp_of_term ct) cts) boehmes@36899: boehmes@41691: val access = blanchet@58058: Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} Old_SMT_Utils.destT1 blanchet@58058: fun mk_access array = Thm.apply (Old_SMT_Utils.instT' array access) array boehmes@36899: blanchet@58058: val update = Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd} blanchet@58058: (Thm.dest_ctyp o Old_SMT_Utils.destT1) boehmes@36899: fun mk_update array index value = boehmes@36899: let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array) boehmes@41691: in blanchet@58058: Thm.apply (Thm.mk_binop (Old_SMT_Utils.instTs cTs update) array index) value boehmes@41691: end boehmes@36899: wenzelm@46497: val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)}) boehmes@47965: val add = Thm.cterm_of @{theory} @{const plus (int)} boehmes@47965: val int0 = Numeral.mk_cnumber @{ctyp int} 0 boehmes@40579: val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)}) boehmes@40579: val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)}) boehmes@40579: val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div}) boehmes@40579: val mk_mod = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3mod}) boehmes@40579: val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (int)}) boehmes@40579: val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (int)}) boehmes@36899: boehmes@36899: fun mk_builtin_fun ctxt sym cts = boehmes@36899: (case (sym, cts) of boehmes@36899: (Sym ("true", _), []) => SOME mk_true boehmes@36899: | (Sym ("false", _), []) => SOME mk_false boehmes@36899: | (Sym ("not", _), [ct]) => SOME (mk_not ct) boehmes@40579: | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts) boehmes@40579: | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts) boehmes@36899: | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu) boehmes@36899: | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu) boehmes@36899: | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu) boehmes@36899: | (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu)) boehmes@41761: | (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) boehmes@41761: | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *) boehmes@36899: | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu) boehmes@36899: | (Sym ("distinct", _), _) => SOME (mk_distinct cts) wenzelm@46497: | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck) boehmes@36899: | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv) boehmes@36899: | _ => boehmes@36899: (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of boehmes@47965: (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts) boehmes@36899: | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct) boehmes@36899: | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu) boehmes@36899: | (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu) boehmes@37151: | (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu) boehmes@37151: | (Sym ("mod", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mod ct cu) boehmes@36899: | (Sym ("<", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt ct cu) boehmes@36899: | (Sym ("<=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le ct cu) boehmes@36899: | (Sym (">", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt cu ct) boehmes@36899: | (Sym (">=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le cu ct) boehmes@36899: | _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts)) boehmes@36899: boehmes@36899: boehmes@36899: boehmes@41059: (* abstraction *) boehmes@36899: boehmes@36899: fun is_builtin_theory_term ctxt t = blanchet@58058: if Old_SMT_Builtin.is_builtin_num ctxt t then true boehmes@41059: else boehmes@41059: (case Term.strip_comb t of blanchet@58058: (Const c, ts) => Old_SMT_Builtin.is_builtin_fun ctxt c ts boehmes@41059: | _ => false) boehmes@36899: boehmes@36899: end