# HG changeset patch # User boehmes # Date 1273701236 -7200 # Node ID ea94c03ad567ca0fae56e8f64ae9f75f443b44bd # Parent e0d295cb8bfdfffff43f268df9a5bbf52a9a27fe deleted SMT translation files (to be replaced by a simplified version) diff -r e0d295cb8bfd -r ea94c03ad567 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed May 12 23:53:55 2010 +0200 +++ b/src/HOL/IsaMakefile Wed May 12 23:53:56 2010 +0200 @@ -1248,8 +1248,7 @@ SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \ SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \ SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \ - SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML \ - SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML \ + SMT/Tools/z3_model.ML SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML \ SMT/Tools/smt_additional_facts.ML @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT diff -r e0d295cb8bfd -r ea94c03ad567 src/HOL/SMT/Tools/smt_translate.ML --- 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 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 diff -r e0d295cb8bfd -r ea94c03ad567 src/HOL/SMT/Tools/smtlib_interface.ML --- 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 diff -r e0d295cb8bfd -r ea94c03ad567 src/HOL/SMT/Tools/z3_interface.ML --- 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