--- a/src/HOL/SMT/Tools/smt_translate.ML Wed May 12 23:53:55 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,541 +0,0 @@
-(* Title: HOL/SMT/Tools/smt_translate.ML
- Author: Sascha Boehme, TU Muenchen
-
-Translate theorems into an SMT intermediate format and serialize them,
-depending on an SMT interface.
-*)
-
-signature SMT_TRANSLATE =
-sig
- (* intermediate term structure *)
- datatype sym =
- SConst of string * typ |
- SFree of string * typ |
- SNum of int * typ
- datatype squant = SForall | SExists
- datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
- datatype ('a, 'b) sterm =
- SVar of int |
- SApp of 'a * ('a, 'b) sterm list |
- SLet of (string * 'b) * ('a, 'b) sterm * ('a, 'b) sterm |
- SQuant of squant * (string * 'b) list * ('a, 'b) sterm spattern list *
- ('a, 'b) sterm
-
- (* table for built-in symbols *)
- type builtin_fun = typ -> (sym, typ) sterm list ->
- (string * (sym, typ) sterm list) option
- type builtin_table = (typ * builtin_fun) list Symtab.table
- val builtin_make: (term * string) list -> builtin_table
- val builtin_add: term * builtin_fun -> builtin_table -> builtin_table
- val builtin_lookup: builtin_table -> theory -> string * typ ->
- (sym, typ) sterm list -> (string * (sym, typ) sterm list) option
- val bv_rotate: (int -> string) -> builtin_fun
- val bv_extend: (int -> string) -> builtin_fun
- val bv_extract: (int -> int -> string) -> builtin_fun
-
- (* configuration options *)
- type prefixes = {
- var_prefix: string,
- typ_prefix: string,
- fun_prefix: string,
- pred_prefix: string }
- type markers = {
- term_marker: string,
- formula_marker: string }
- type builtins = {
- builtin_typ: typ -> string option,
- builtin_num: int * typ -> string option,
- builtin_fun: bool -> builtin_table }
- type sign = {
- typs: string list,
- funs: (string * (string list * string)) list,
- preds: (string * string list) list }
- type config = {
- strict: bool,
- prefixes: prefixes,
- markers: markers,
- builtins: builtins,
- serialize: sign -> (string, string) sterm list -> string}
- type recon = {typs: typ Symtab.table, terms: term Symtab.table}
-
- val translate: config -> theory -> thm list -> string * (recon * thm list)
-
- val dest_binT: typ -> int
- val dest_funT: int -> typ -> typ list * typ
-end
-
-structure SMT_Translate: SMT_TRANSLATE =
-struct
-
-(* Intermediate term structure *)
-
-datatype sym =
- SConst of string * typ |
- SFree of string * typ |
- SNum of int * typ
-datatype squant = SForall | SExists
-datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
-datatype ('a, 'b) sterm =
- SVar of int |
- SApp of 'a * ('a, 'b) sterm list |
- SLet of (string * 'b) * ('a, 'b) sterm * ('a, 'b) sterm |
- SQuant of squant * (string * 'b) list * ('a, 'b) sterm spattern list *
- ('a, 'b) sterm
-
-fun app c ts = SApp (c, ts)
-
-fun map_pat f (SPat ps) = SPat (map f ps)
- | map_pat f (SNoPat ps) = SNoPat (map f ps)
-
-fun fold_map_pat f (SPat ps) = fold_map f ps #>> SPat
- | fold_map_pat f (SNoPat ps) = fold_map f ps #>> SNoPat
-
-val make_sconst = SConst o Term.dest_Const
-
-
-(* General type destructors. *)
-
-fun dest_binT T =
- (case T of
- Type (@{type_name "Numeral_Type.num0"}, _) => 0
- | Type (@{type_name "Numeral_Type.num1"}, _) => 1
- | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
- | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
- | _ => raise TYPE ("dest_binT", [T], []))
-
-val dest_wordT = (fn
- Type (@{type_name "word"}, [T]) => dest_binT T
- | T => raise TYPE ("dest_wordT", [T], []))
-
-val dest_funT =
- let
- fun dest Ts 0 T = (rev Ts, T)
- | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
- | dest _ _ T = raise TYPE ("dest_funT", [T], [])
- in dest [] end
-
-
-(* Table for built-in symbols *)
-
-type builtin_fun = typ -> (sym, typ) sterm list ->
- (string * (sym, typ) sterm list) option
-type builtin_table = (typ * builtin_fun) list Symtab.table
-
-fun builtin_make entries =
- let
- fun dest (t, bn) =
- let val (n, T) = Term.dest_Const t
- in (n, (Logic.varifyT_global T, K (SOME o pair bn))) end
- in Symtab.make (AList.group (op =) (map dest entries)) end
-
-fun builtin_add (t, f) tab =
- let val (n, T) = apsnd Logic.varifyT_global (Term.dest_Const t)
- in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
-
-fun builtin_lookup tab thy (n, T) ts =
- AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T
- |> (fn SOME f => f T ts | NONE => NONE)
-
-local
- val dest_nat = (fn
- SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
- | _ => NONE)
-in
-fun bv_rotate mk_name _ ts =
- dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
-
-fun bv_extend mk_name T ts =
- (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
- (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE
- | _ => NONE)
-
-fun bv_extract mk_name T ts =
- (case (try dest_wordT (body_type T), dest_nat (hd ts)) of
- (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts)
- | _ => NONE)
-end
-
-
-(* Configuration options *)
-
-type prefixes = {
- var_prefix: string,
- typ_prefix: string,
- fun_prefix: string,
- pred_prefix: string }
-type markers = {
- term_marker: string,
- formula_marker: string }
-type builtins = {
- builtin_typ: typ -> string option,
- builtin_num: int * typ -> string option,
- builtin_fun: bool -> builtin_table }
-type sign = {
- typs: string list,
- funs: (string * (string list * string)) list,
- preds: (string * string list) list }
-type config = {
- strict: bool,
- prefixes: prefixes,
- markers: markers,
- builtins: builtins,
- serialize: sign -> (string, string) sterm list -> string}
-type recon = {typs: typ Symtab.table, terms: term Symtab.table}
-
-
-(* Translate Isabelle/HOL terms into SMT intermediate terms.
- We assume that lambda-lifting has been performed before, i.e., lambda
- abstractions occur only at quantifiers and let expressions.
-*)
-local
- val quantifier = (fn
- @{const_name All} => SOME SForall
- | @{const_name Ex} => SOME SExists
- | _ => NONE)
-
- fun group_quant qname vs (t as Const (q, _) $ Abs (n, T, u)) =
- if q = qname then group_quant qname ((n, T) :: vs) u else (vs, t)
- | group_quant _ vs t = (vs, t)
-
- fun dest_trigger (@{term trigger} $ tl $ t) = (HOLogic.dest_list tl, t)
- | dest_trigger t = ([], t)
-
- fun pat f ts (Const (@{const_name pat}, _) $ t) = SPat (rev (f t :: ts))
- | pat f ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (f t :: ts))
- | pat f ts (Const (@{const_name andpat}, _) $ p $ t) = pat f (f t :: ts) p
- | pat _ _ t = raise TERM ("pat", [t])
-
- fun trans Ts t =
- (case Term.strip_comb t of
- (Const (qn, _), [Abs (n, T, t1)]) =>
- (case quantifier qn of
- SOME q =>
- let
- val (vs, u) = group_quant qn [(n, T)] t1
- val Us = map snd vs @ Ts
- val (ps, b) = dest_trigger u
- in SQuant (q, rev vs, map (pat (trans Us) []) ps, trans Us b) end
- | NONE => raise TERM ("intermediate", [t]))
- | (Const (@{const_name Let}, _), [t1, Abs (n, T, t2)]) =>
- SLet ((n, T), trans Ts t1, trans (T :: Ts) t2)
- | (Const (c as (@{const_name distinct}, _)), [t1]) =>
- (* this is not type-correct, but will be corrected at a later stage *)
- SApp (SConst c, map (trans Ts) (HOLogic.dest_list t1))
- | (Const c, ts) =>
- (case try HOLogic.dest_number t of
- SOME (T, i) => SApp (SNum (i, T), [])
- | NONE => SApp (SConst c, map (trans Ts) ts))
- | (Free c, ts) => SApp (SFree c, map (trans Ts) ts)
- | (Bound i, []) => SVar i
- | _ => raise TERM ("intermediate", [t]))
-in
-fun intermediate ts = map (trans [] o HOLogic.dest_Trueprop) ts
-end
-
-
-(* Separate formulas from terms by adding special marker symbols ("term",
- "formula"). Atoms "P" whose head symbol also occurs as function symbol are
- rewritten to "term P = term True". Connectives and built-in predicates
- occurring at term level are replaced by new constants, and theorems
- specifying their meaning are added.
-*)
-local
- local
- fun cons_nr (SConst _) = 0
- | cons_nr (SFree _) = 1
- | cons_nr (SNum _) = 2
-
- fun struct_ord (t, u) = int_ord (cons_nr t, cons_nr u)
-
- fun atoms_ord (SConst (n, _), SConst (m, _)) = fast_string_ord (n, m)
- | atoms_ord (SFree (n, _), SFree (m, _)) = fast_string_ord (n, m)
- | atoms_ord (SNum (i, _), SNum (j, _)) = int_ord (i, j)
- | atoms_ord _ = sys_error "atoms_ord"
-
- fun types_ord (SConst (_, T), SConst (_, U)) = Term_Ord.typ_ord (T, U)
- | types_ord (SFree (_, T), SFree (_, U)) = Term_Ord.typ_ord (T, U)
- | types_ord (SNum (_, T), SNum (_, U)) = Term_Ord.typ_ord (T, U)
- | types_ord _ = sys_error "types_ord"
-
- fun fast_sym_ord tu =
- (case struct_ord tu of
- EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
- | ord => ord)
- in
- structure Stab = Table(type key = sym val ord = fast_sym_ord)
- end
-
-
- (** Add the marker symbols "term" and "formula" to separate formulas and
- terms. **)
-
- val connectives = map make_sconst [@{term True}, @{term False},
- @{term Not}, @{term "op &"}, @{term "op |"}, @{term "op -->"},
- @{term "op = :: bool => _"}]
-
- fun insert_sym c = Stab.map_default (c, ()) I
- fun note false c (ps, fs) = (insert_sym c ps, fs)
- | note true c (ps, fs) = (ps, insert_sym c fs)
-
- val term_marker = SConst (@{const_name term}, Term.dummyT)
- val formula_marker = SConst (@{const_name formula}, Term.dummyT)
- fun mark f true t = f true t #>> app term_marker o single
- | mark f false t = f false t #>> app formula_marker o single
- fun mark' f false t = f true t #>> app term_marker o single
- | mark' f true t = f true t
- fun mark_term (t : (sym, typ) sterm) = app term_marker [t]
- fun lift_term_marker c ts =
- let val rem = (fn SApp (SConst (@{const_name term}, _), [t]) => t | t => t)
- in mark_term (SApp (c, map rem ts)) end
- fun is_term (SApp (SConst (@{const_name term}, _), _)) = true
- | is_term _ = false
-
- fun either x = (fn y as SOME _ => y | _ => x)
- fun get_loc loc i t =
- (case t of
- SVar j => if i = j then SOME loc else NONE
- | SApp (SConst (@{const_name term}, _), us) => get_locs true i us
- | SApp (SConst (@{const_name formula}, _), us) => get_locs false i us
- | SApp (_, us) => get_locs loc i us
- | SLet (_, u1, u2) => either (get_loc true i u1) (get_loc loc (i+1) u2)
- | SQuant (_, vs, _, u) => get_loc loc (i + length vs) u)
- and get_locs loc i ts = fold (either o get_loc loc i) ts NONE
-
- fun sep loc t =
- (case t of
- SVar _ => pair t
- | SApp (c as SConst (@{const_name If}, _), u :: us) =>
- mark sep false u ##>> fold_map (sep loc) us #>> app c o (op ::)
- | SApp (c, us) =>
- if not loc andalso member (op =) connectives c
- then fold_map (sep loc) us #>> app c
- else note loc c #> fold_map (mark' sep loc) us #>> app c
- | SLet (v, u1, u2) =>
- sep loc u2 #-> (fn u2' =>
- mark sep (the (get_loc loc 0 u2')) u1 #>> (fn u1' =>
- SLet (v, u1', u2')))
- | SQuant (q, vs, ps, u) =>
- fold_map (fold_map_pat (mark sep true)) ps ##>>
- sep loc u #>> (fn (ps', u') =>
- SQuant (q, vs, ps', u')))
-
- (** Rewrite atoms. **)
-
- val unterm_rule = @{lemma "term x == x" by (simp add: term_def)}
- val unterm_conv = More_Conv.top_sweep_conv (K (Conv.rewr_conv unterm_rule))
-
- val dest_word_type = (fn Type (@{type_name word}, [T]) => T | T => T)
- fun instantiate [] _ = I
- | instantiate (v :: _) T =
- Term.subst_TVars [(v, dest_word_type (Term.domain_type T))]
-
- fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
- | dest_alls t = t
- val dest_iff = (fn (Const (@{const_name iff}, _) $ t $ _ ) => t | t => t)
- val dest_eq = (fn (Const (@{const_name "op ="}, _) $ t $ _ ) => t | t => t)
- val dest_not = (fn (@{term Not} $ t) => t | t => t)
- val head_of = HOLogic.dest_Trueprop #> dest_alls #> dest_iff #> dest_not #>
- dest_eq #> Term.head_of
-
- fun prepare ctxt thm =
- let
- val rule = Conv.fconv_rule (unterm_conv ctxt) thm
- val prop = Thm.prop_of thm
- val inst = instantiate (Term.add_tvar_names prop [])
- fun inst_for T = (rule, singleton intermediate (inst T prop))
- in (make_sconst (head_of (Thm.prop_of rule)), inst_for) end
-
- val logicals = map (prepare @{context})
- @{lemma
- "~ holds False"
- "ALL p. holds (~ p) iff (~ holds p)"
- "ALL p q. holds (p & q) iff (holds p & holds q)"
- "ALL p q. holds (p | q) iff (holds p | holds q)"
- "ALL p q. holds (p --> q) iff (holds p --> holds q)"
- "ALL p q. holds (p iff q) iff (holds p iff holds q)"
- "ALL p q. holds (p = q) iff (p = q)"
- "ALL (a::int) b. holds (a < b) iff (a < b)"
- "ALL (a::int) b. holds (a <= b) iff (a <= b)"
- "ALL (a::real) b. holds (a < b) iff (a < b)"
- "ALL (a::real) b. holds (a <= b) iff (a <= b)"
- "ALL (a::'a::len0 word) b. holds (a < b) iff (a < b)"
- "ALL (a::'a::len0 word) b. holds (a <= b) iff (a <= b)"
- "ALL a b. holds (a <s b) iff (a <s b)"
- "ALL a b. holds (a <=s b) iff (a <=s b)"
- by (simp_all add: term_def iff_def)}
-
- fun is_instance thy (SConst (n, T), SConst (m, U)) =
- (n = m) andalso Sign.typ_instance thy (T, U)
- | is_instance _ _ = false
-
- fun rule_for thy c T =
- AList.lookup (is_instance thy) logicals c
- |> Option.map (fn inst_for => inst_for T)
-
- fun lookup_logical thy (c as SConst (_, T)) (thms, ts) =
- (case rule_for thy c T of
- SOME (thm, t) => (thm :: thms, t :: ts)
- | NONE => (thms, ts))
- | lookup_logical _ _ tss = tss
-
- val s_eq = make_sconst @{term "op = :: bool => _"}
- val s_True = mark_term (SApp (make_sconst @{term True}, []))
- fun holds (SApp (c, ts)) = SApp (s_eq, [lift_term_marker c ts, s_True])
- | holds t = SApp (s_eq, [mark_term t, s_True])
-
- val rewr_iff = (fn
- SConst (@{const_name "op ="}, T as @{typ "bool => bool => bool"}) =>
- SConst (@{const_name iff}, T)
- | c => c)
-
- fun rewrite ls =
- let
- fun rewr env loc t =
- (case t of
- SVar i => if not loc andalso nth env i then holds t else t
- | SApp (c as SConst (@{const_name term}, _), [u]) =>
- SApp (c, [rewr env true u])
- | SApp (c as SConst (@{const_name formula}, _), [u]) =>
- SApp (c, [rewr env false u])
- | SApp (c, us) =>
- let val f = if not loc andalso Stab.defined ls c then holds else I
- in f (SApp (rewr_iff c, map (rewr env loc) us)) end
- | SLet (v, u1, u2) =>
- SLet (v, rewr env loc u1, rewr (is_term u1 :: env) loc u2)
- | SQuant (q, vs, ps, u) =>
- let val e = replicate (length vs) true @ env
- in SQuant (q, vs, map (map_pat (rewr e loc)) ps, rewr e loc u) end)
- in map (rewr [] false) end
-in
-fun separate thy ts =
- let
- val (ts', (ps, fs)) = fold_map (sep false) ts (Stab.empty, Stab.empty)
- fun insert (px as (p, _)) = if Stab.defined fs p then Stab.update px else I
- in
- Stab.fold (lookup_logical thy o fst) fs ([], [])
- ||> append (rewrite (Stab.fold insert ps Stab.empty) ts')
- end
-end
-
-
-(* Collect the signature of intermediate terms, identify built-in symbols,
- rename uninterpreted symbols and types, make bound variables unique.
- We require @{term distinct} to be a built-in constant of the SMT solver.
-*)
-local
- fun empty_nctxt p = (p, 1)
- fun make_nctxt (pT, pf, pp) = (empty_nctxt pT, empty_nctxt (pf, pp))
- fun fresh_name (p, i) = (p ^ string_of_int i, (p, i+1))
- fun fresh_typ (nT, nfp) = fresh_name nT ||> (fn nT' => (nT', nfp))
- fun fresh_fun loc (nT, ((pf, pp), i)) =
- let val p = if loc then pf else pp
- in fresh_name (p, i) ||> (fn (_, i') => (nT, ((pf, pp), i'))) end
-
- val empty_sign = (Typtab.empty, Termtab.empty, Termtab.empty)
- fun lookup_typ (typs, _, _) = Option.map snd o Typtab.lookup typs
- fun lookup_fun true (_, funs, _) = Option.map snd o Termtab.lookup funs
- | lookup_fun false (_, _, preds) = Option.map snd o Termtab.lookup preds
- fun ext (k, v) = (k, (serial (), v))
- fun p_ord p = prod_ord int_ord (K EQUAL) p
- fun add_typ x (typs, funs, preds) =
- (Typtab.update (ext x) typs, funs, preds)
- fun add_fun true x (typs, funs, preds) =
- (typs, Termtab.update (ext x) funs, preds)
- | add_fun false x (typs, funs, preds) =
- (typs, funs, Termtab.update (ext x) preds)
- fun make_sign (typs, funs, preds) = {
- typs = map snd (sort p_ord (map snd (Typtab.dest typs))),
- funs = map snd (sort p_ord (map snd (Termtab.dest funs))),
- preds = map (apsnd fst o snd) (sort p_ord (map snd (Termtab.dest preds))) }
- fun make_rtab (typs, funs, preds) =
- let
- val rTs = Typtab.dest typs |> map (swap o apsnd snd) |> Symtab.make
- val rts = Termtab.dest funs @ Termtab.dest preds
- |> map (apfst fst o swap o apsnd snd) |> Symtab.make
- in {typs=rTs, terms=rts} end
-
- fun either f g x = (case f x of NONE => g x | y => y)
-
- fun rep_typ ({builtin_typ, ...} : builtins) T (st as (vars, ns, sgn)) =
- (case either builtin_typ (lookup_typ sgn) T of
- SOME n => (n, st)
- | NONE =>
- let val (n, ns') = fresh_typ ns
- in (n, (vars, ns', add_typ (T, n) sgn)) end)
-
- fun rep_var bs (_, T) (vars, ns, sgn) =
- let val (n', vars') = fresh_name vars
- in (vars', ns, sgn) |> rep_typ bs T |>> pair n' end
-
- fun rep_fun bs loc t T i (st as (_, _, sgn0)) =
- (case lookup_fun loc sgn0 t of
- SOME (n, _) => (n, st)
- | NONE =>
- let
- val (Us, U) = dest_funT i T
- val (uns, (vars, ns, sgn)) =
- st |> fold_map (rep_typ bs) Us ||>> rep_typ bs U
- val (n, ns') = fresh_fun loc ns
- in (n, (vars, ns', add_fun loc (t, (n, uns)) sgn)) end)
-
- fun rep_num (bs as {builtin_num, ...} : builtins) (i, T) st =
- (case builtin_num (i, T) of
- SOME n => (n, st)
- | NONE => rep_fun bs true (HOLogic.mk_number T i) T 0 st)
-in
-fun signature_of prefixes markers builtins thy ts =
- let
- val {var_prefix, typ_prefix, fun_prefix, pred_prefix} = prefixes
- val {formula_marker, term_marker} = markers
- val {builtin_fun, ...} = builtins
-
- fun sign loc t =
- (case t of
- SVar i => pair (SVar i)
- | SApp (SConst (@{const_name term}, _), [u]) =>
- sign true u #>> app term_marker o single
- | SApp (SConst (@{const_name formula}, _), [u]) =>
- sign false u #>> app formula_marker o single
- | SApp (SConst (c as (_, T)), ts) =>
- (case builtin_lookup (builtin_fun loc) thy c ts of
- SOME (n, ts') => fold_map (sign loc) ts' #>> app n
- | NONE =>
- rep_fun builtins loc (Const c) T (length ts) ##>>
- fold_map (sign loc) ts #>> SApp)
- | SApp (SFree (c as (_, T)), ts) =>
- rep_fun builtins loc (Free c) T (length ts) ##>>
- fold_map (sign loc) ts #>> SApp
- | SApp (SNum n, _) => rep_num builtins n #>> (fn n => SApp (n, []))
- | SLet (v, u1, u2) =>
- rep_var builtins v #-> (fn v' =>
- sign loc u1 ##>> sign loc u2 #>> (fn (u1', u2') =>
- SLet (v', u1', u2')))
- | SQuant (q, vs, ps, u) =>
- fold_map (rep_var builtins) vs ##>>
- fold_map (fold_map_pat (sign loc)) ps ##>>
- sign loc u #>> (fn ((vs', ps'), u') =>
- SQuant (q, vs', ps', u')))
- in
- (empty_nctxt var_prefix, make_nctxt (typ_prefix, fun_prefix, pred_prefix),
- empty_sign)
- |> fold_map (sign false) ts
- |> (fn (us, (_, _, sgn)) => (make_rtab sgn, (make_sign sgn, us)))
- end
-end
-
-
-(* Combination of all translation functions and invocation of serialization. *)
-
-fun translate config thy thms =
- let val {strict, prefixes, markers, builtins, serialize} = config
- in
- map Thm.prop_of thms
- |> SMT_Monomorph.monomorph thy
- |> intermediate
- |> (if strict then separate thy else pair [])
- ||>> signature_of prefixes markers builtins thy
- ||> (fn (sgn, ts) => serialize sgn ts)
- |> (fn ((thms', rtab), str) => (str, (rtab, thms' @ thms)))
- end
-
-end
--- a/src/HOL/SMT/Tools/smtlib_interface.ML Wed May 12 23:53:55 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(* Title: HOL/SMT/Tools/smtlib_interface.ML
- Author: Sascha Boehme, TU Muenchen
-
-Interface to SMT solvers based on the SMT-LIB format.
-*)
-
-signature SMTLIB_INTERFACE =
-sig
- val basic_builtins: SMT_Translate.builtins
- val default_attributes: string list
- val gen_interface: SMT_Translate.builtins -> string list -> string list ->
- SMT_Translate.config
- val interface: string list -> SMT_Translate.config
-end
-
-structure SMTLIB_Interface: SMTLIB_INTERFACE =
-struct
-
-structure T = SMT_Translate
-
-
-(* built-in types, functions and predicates *)
-
-val builtin_typ = (fn
- @{typ int} => SOME "Int"
- | @{typ real} => SOME "Real"
- | _ => NONE)
-
-val builtin_num = (fn
- (i, @{typ int}) => SOME (string_of_int i)
- | (i, @{typ real}) => SOME (string_of_int i ^ ".0")
- | _ => NONE)
-
-val builtin_funcs = T.builtin_make [
- (@{term If}, "ite"),
- (@{term "uminus :: int => _"}, "~"),
- (@{term "plus :: int => _"}, "+"),
- (@{term "minus :: int => _"}, "-"),
- (@{term "times :: int => _"}, "*"),
- (@{term "uminus :: real => _"}, "~"),
- (@{term "plus :: real => _"}, "+"),
- (@{term "minus :: real => _"}, "-"),
- (@{term "times :: real => _"}, "*") ]
-
-val builtin_preds = T.builtin_make [
- (@{term True}, "true"),
- (@{term False}, "false"),
- (@{term Not}, "not"),
- (@{term "op &"}, "and"),
- (@{term "op |"}, "or"),
- (@{term "op -->"}, "implies"),
- (@{term "op iff"}, "iff"),
- (@{term If}, "if_then_else"),
- (@{term distinct}, "distinct"),
- (@{term "op ="}, "="),
- (@{term "op < :: int => _"}, "<"),
- (@{term "op <= :: int => _"}, "<="),
- (@{term "op < :: real => _"}, "<"),
- (@{term "op <= :: real => _"}, "<=") ]
-
-
-(* serialization *)
-
-val wr = Buffer.add
-fun wr_line f = f #> wr "\n"
-
-fun sep f = wr " " #> f
-fun par f = sep (wr "(" #> f #> wr ")")
-
-fun wr1 s = sep (wr s)
-fun wrn f n = (fn [] => wr1 n | ts => par (wr n #> fold f ts))
-
-val term_marker = "__term"
-val formula_marker = "__form"
-fun dest_marker (T.SApp ("__term", [t])) = SOME (true, t)
- | dest_marker (T.SApp ("__form", [t])) = SOME (false, t)
- | dest_marker _ = NONE
-
-val tvar = prefix "?"
-val fvar = prefix "$"
-
-datatype lexpr =
- LVar of string |
- LTerm of lexpr list * (string, string) T.sterm
-
-fun wr_expr loc env t =
- (case t of
- T.SVar i =>
- (case nth env i of
- LVar name => wr1 name
- | LTerm (env', t') => wr_expr loc env' t')
- | T.SApp (n, ts) =>
- (case dest_marker t of
- SOME (loc', t') => wr_expr loc' env t'
- | NONE => wrn (wr_expr loc env) n ts)
- | T.SLet ((v, _), t1, t2) =>
- if loc
- then
- let val (_, t1') = the (dest_marker t1)
- in wr_expr loc (LTerm (env, t1') :: env) t2 end
- else
- let
- val (loc', t1') = the (dest_marker t1)
- val (kind, v') = if loc' then ("let", tvar v) else ("flet", fvar v)
- in
- par (wr kind #> par (wr v' #> wr_expr loc' env t1') #>
- wr_expr loc (LVar v' :: env) t2)
- end
- | T.SQuant (q, vs, ps, b) =>
- let
- val wr_quant = wr o (fn T.SForall => "forall" | T.SExists => "exists")
- fun wr_var (n, s) = par (wr (tvar n) #> wr1 s)
-
- val wre = wr_expr loc (map (LVar o tvar o fst) (rev vs) @ env)
-
- fun wrp s ts = wr1 (":" ^ s ^ " {") #> fold wre ts #> wr1 "}"
- fun wr_pat (T.SPat ts) = wrp "pat" ts
- | wr_pat (T.SNoPat ts) = wrp "nopat" ts
- in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
-
-fun serialize attributes comments ({typs, funs, preds} : T.sign) ts =
- let fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
- in
- Buffer.empty
- |> wr_line (wr "(benchmark Isabelle")
- |> wr_line (wr ":status unknown")
- |> fold (wr_line o wr) attributes
- |> length typs > 0 ?
- wr_line (wr ":extrasorts" #> par (fold wr1 typs))
- |> length funs > 0 ? (
- wr_line (wr ":extrafuns (") #>
- fold (wr_decl o apsnd (fn (Ts, T) => Ts @ [T])) funs #>
- wr_line (wr " )"))
- |> length preds > 0 ? (
- wr_line (wr ":extrapreds (") #>
- fold wr_decl preds #>
- wr_line (wr " )"))
- |> fold (fn t => wr ":assumption" #> wr_line (wr_expr false [] t)) ts
- |> wr_line (wr ":formula true")
- |> wr_line (wr ")")
- |> fold (fn comment => wr_line (wr ("; " ^ comment))) comments
- |> Buffer.content
- end
-
-
-(* SMT solver interface using the SMT-LIB input format *)
-
-val basic_builtins = {
- builtin_typ = builtin_typ,
- builtin_num = builtin_num,
- builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
-
-val default_attributes = [":logic AUFLIRA"]
-
-fun gen_interface builtins attributes comments = {
- strict = true,
- prefixes = {
- var_prefix = "x",
- typ_prefix = "T",
- fun_prefix = "uf_",
- pred_prefix = "up_" },
- markers = {
- term_marker = term_marker,
- formula_marker = formula_marker },
- builtins = builtins,
- serialize = serialize attributes comments }
-
-fun interface comments =
- gen_interface basic_builtins default_attributes comments
-
-end
--- a/src/HOL/SMT/Tools/z3_interface.ML Wed May 12 23:53:55 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-(* Title: HOL/SMT/Tools/z3_interface.ML
- Author: Sascha Boehme, TU Muenchen
-
-Interface to Z3 based on a relaxed version of SMT-LIB.
-*)
-
-signature Z3_INTERFACE =
-sig
- val interface: string list -> SMT_Translate.config
-end
-
-structure Z3_Interface: Z3_INTERFACE =
-struct
-
-structure T = SMT_Translate
-
-fun mk_name1 n i = n ^ "[" ^ string_of_int i ^ "]"
-fun mk_name2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
-
-val builtin_typ = (fn
- @{typ int} => SOME "Int"
- | @{typ real} => SOME "Real"
- | Type (@{type_name word}, [T]) =>
- Option.map (mk_name1 "BitVec") (try T.dest_binT T)
- | _ => NONE)
-
-val builtin_num = (fn
- (i, @{typ int}) => SOME (string_of_int i)
- | (i, @{typ real}) => SOME (string_of_int i ^ ".0")
- | (i, Type (@{type_name word}, [T])) =>
- Option.map (mk_name1 ("bv" ^ string_of_int i)) (try T.dest_binT T)
- | _ => NONE)
-
-val builtin_funcs = T.builtin_make [
- (@{term If}, "ite"),
- (@{term "uminus :: int => _"}, "~"),
- (@{term "plus :: int => _"}, "+"),
- (@{term "minus :: int => _"}, "-"),
- (@{term "times :: int => _"}, "*"),
- (@{term "op div :: int => _"}, "div"),
- (@{term "op mod :: int => _"}, "mod"),
- (@{term "op rem"}, "rem"),
- (@{term "uminus :: real => _"}, "~"),
- (@{term "plus :: real => _"}, "+"),
- (@{term "minus :: real => _"}, "-"),
- (@{term "times :: real => _"}, "*"),
- (@{term "op / :: real => _"}, "/"),
- (@{term "bitNOT :: 'a::len0 word => _"}, "bvnot"),
- (@{term "op AND :: 'a::len0 word => _"}, "bvand"),
- (@{term "op OR :: 'a::len0 word => _"}, "bvor"),
- (@{term "op XOR :: 'a::len0 word => _"}, "bvxor"),
- (@{term "uminus :: 'a::len0 word => _"}, "bvneg"),
- (@{term "op + :: 'a::len0 word => _"}, "bvadd"),
- (@{term "op - :: 'a::len0 word => _"}, "bvsub"),
- (@{term "op * :: 'a::len0 word => _"}, "bvmul"),
- (@{term "op div :: 'a::len0 word => _"}, "bvudiv"),
- (@{term "op mod :: 'a::len0 word => _"}, "bvurem"),
- (@{term "op sdiv"}, "bvsdiv"),
- (@{term "op smod"}, "bvsmod"),
- (@{term "op srem"}, "bvsrem"),
- (@{term word_cat}, "concat"),
- (@{term bv_shl}, "bvshl"),
- (@{term bv_lshr}, "bvlshr"),
- (@{term bv_ashr}, "bvashr")]
- |> T.builtin_add (@{term slice}, T.bv_extract (mk_name2 "extract"))
- |> T.builtin_add (@{term ucast}, T.bv_extend (mk_name1 "zero_extend"))
- |> T.builtin_add (@{term scast}, T.bv_extend (mk_name1 "sign_extend"))
- |> T.builtin_add (@{term word_rotl}, T.bv_rotate (mk_name1 "rotate_left"))
- |> T.builtin_add (@{term word_rotr}, T.bv_rotate (mk_name1 "rotate_right"))
-
-val builtin_preds = T.builtin_make [
- (@{term True}, "true"),
- (@{term False}, "false"),
- (@{term Not}, "not"),
- (@{term "op &"}, "and"),
- (@{term "op |"}, "or"),
- (@{term "op -->"}, "implies"),
- (@{term "op iff"}, "iff"),
- (@{term If}, "if_then_else"),
- (@{term distinct}, "distinct"),
- (@{term "op ="}, "="),
- (@{term "op < :: int => _"}, "<"),
- (@{term "op <= :: int => _"}, "<="),
- (@{term "op < :: real => _"}, "<"),
- (@{term "op <= :: real => _"}, "<="),
- (@{term "op < :: 'a::len0 word => _"}, "bvult"),
- (@{term "op <= :: 'a::len0 word => _"}, "bvule"),
- (@{term word_sless}, "bvslt"),
- (@{term word_sle}, "bvsle")]
-
-val builtins = {
- builtin_typ = builtin_typ,
- builtin_num = builtin_num,
- builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
-
-val interface = SMTLIB_Interface.gen_interface builtins []
-
-end