# HG changeset patch
# User boehmes
# Date 1273701237 -7200
# Node ID 48cf03469dc646878ee1d40bd56d809f75100a87
# Parent  ea94c03ad567ca0fae56e8f64ae9f75f443b44bd
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms

diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/IsaMakefile	Wed May 12 23:53:57 2010 +0200
@@ -1245,11 +1245,11 @@
 $(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/ROOT.ML SMT/SMT_Base.thy SMT/Z3.thy \
   SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML	\
   SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML              \
+  SMT/Tools/z3_interface.ML SMT/Tools/smt_additional_facts.ML		\
   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_solver.ML $(SRC)/Tools/cache_io.ML	\
-  SMT/Tools/smt_additional_facts.ML
+  SMT/Tools/z3_model.ML SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML
 	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
 
 
diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/SMT/SMT_Base.thy
--- a/src/HOL/SMT/SMT_Base.thy	Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/SMT_Base.thy	Wed May 12 23:53:57 2010 +0200
@@ -106,26 +106,13 @@
 
 text {*
 Some SMT solver formats require a strict separation between formulas and terms.
-The following marker symbols are used internally to separate those categories:
+During normalization, all uninterpreted constants are treated as function
+symbols, and atoms (with uninterpreted head symbol) are turned into terms by
+equating them with true using the following term-level equation symbol:
 *}
 
-definition formula :: "bool \<Rightarrow> bool" where "formula x = x"
-definition "term" where "term x = x"
-
-text {*
-Predicate symbols also occurring as function symbols are turned into function
-symbols by translating atomic formulas into terms:
-*}
-
-abbreviation holds :: "bool \<Rightarrow> bool" where "holds \<equiv> (\<lambda>P. term P = term True)"
-
-text {*
-The following constant represents equivalence, to be treated differently than
-the (polymorphic) equality predicate:
-*}
-
-definition iff :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "iff" 50) where
-  "(x iff y) = (x = y)"
+definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50)
+  where "(x term_eq y) = (x = y)"
 
 
 
diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:57 2010 +0200
@@ -9,9 +9,9 @@
     numerals),
   * embed natural numbers into integers,
   * add extra rules specifying types and constants which occur frequently,
+  * fully translate into object logic, add universal closure,
   * lift lambda terms,
-  * make applications explicit for functions with varying number of arguments,
-  * fully translate into object logic, add universal closure. 
+  * make applications explicit for functions with varying number of arguments.
 *)
 
 signature SMT_NORMALIZE =
@@ -45,28 +45,6 @@
 
 
 
-(* simplification of trivial let expressions (whose bound variables occur at
-   most once) *)
-
-local
-  fun count i (Bound j) = if j = i then 1 else 0
-    | count i (t $ u) = count i t + count i u
-    | count i (Abs (_, _, t)) = count (i + 1) t
-    | count _ _ = 0
-
-  fun is_trivial_let (Const (@{const_name Let}, _) $ _ $ Abs (_, _, t)) =
-        (count 0 t <= 1)
-    | is_trivial_let _ = false
-
-  fun let_conv _ = if_true_conv is_trivial_let (Conv.rewr_conv @{thm Let_def})
-in
-fun trivial_let ctxt =
-  map ((Term.exists_subterm is_trivial_let o Thm.prop_of) ??
-    Conv.fconv_rule (More_Conv.top_conv let_conv ctxt))
-end
-
-
-
 (* simplification of trivial distincts (distinct should have at least
    three elements in the argument list) *)
 
@@ -507,7 +485,6 @@
 
 fun normalize ctxt thms =
   thms
-  |> trivial_let ctxt
   |> trivial_distinct ctxt
   |> rewrite_bool_cases ctxt
   |> normalize_numerals ctxt
diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Wed May 12 23:53:57 2010 +0200
@@ -12,8 +12,7 @@
   type proof_data = {
     context: Proof.context,
     output: string list,
-    recon: SMT_Translate.recon,
-    assms: thm list option }
+    recon: SMT_Translate.recon }
   type solver_config = {
     command: {env_var: string, remote_name: string option},
     arguments: string list,
@@ -60,8 +59,7 @@
 type proof_data = {
   context: Proof.context,
   output: string list,
-  recon: SMT_Translate.recon,
-  assms: thm list option }
+  recon: SMT_Translate.recon }
 
 type solver_config = {
   command: {env_var: string, remote_name: string option},
@@ -164,8 +162,11 @@
 
 end
 
-fun make_proof_data ctxt (ls, (recon, thms)) =
-  {context=ctxt, output=ls, recon=recon, assms=SOME thms}
+fun invoke translate_config command arguments ctxt thms =
+  thms
+  |> SMT_Translate.translate translate_config ctxt
+  |>> run_solver ctxt command arguments
+  |> (fn (ls, recon) => {context=ctxt, output=ls, recon=recon})
 
 fun gen_solver name solver ctxt prems =
   let
@@ -173,14 +174,11 @@
     val comments = ("solver: " ^ name) ::
       ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
       "arguments:" :: arguments
-    val tc = interface comments
-    val thy = ProofContext.theory_of ctxt
   in
     SMT_Additional_Facts.add_facts prems
     |> SMT_Normalize.normalize ctxt 
-    ||> SMT_Translate.translate tc thy
-    ||> apfst (run_solver ctxt command arguments)
-    ||> reconstruct o make_proof_data ctxt
+    ||> invoke (interface comments) command arguments ctxt
+    ||> reconstruct
     |-> fold SMT_Normalize.discharge_definition
   end
 
diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/SMT/Tools/smt_translate.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Wed May 12 23:53:57 2010 +0200
@@ -0,0 +1,355 @@
+(*  Title:      HOL/SMT/Tools/smt_translate.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Translate theorems into an SMT intermediate format and serialize them.
+*)
+
+signature SMT_TRANSLATE =
+sig
+  (* intermediate term structure *)
+  datatype squant = SForall | SExists
+  datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
+  datatype sterm =
+    SVar of int |
+    SApp of string * sterm list |
+    SLet of string * sterm * sterm |
+    SQua of squant * string list * sterm spattern list * sterm
+
+  (* configuration options *)
+  type prefixes = {sort_prefix: string, func_prefix: string}
+  type strict = {
+    is_builtin_conn: string * typ -> bool,
+    is_builtin_pred: string * typ -> bool,
+    is_builtin_distinct: bool}
+  type builtins = {
+    builtin_typ: typ -> string option,
+    builtin_num: typ -> int -> string option,
+    builtin_fun: string * typ -> term list -> (string * term list) option }
+  datatype smt_theory = Integer | Real | Bitvector
+  type sign = {
+    theories: smt_theory list,
+    sorts: string list,
+    funcs: (string * (string list * string)) list }
+  type config = {
+    prefixes: prefixes,
+    strict: strict option,
+    builtins: builtins,
+    serialize: sign -> sterm list -> string }
+  type recon = {
+    typs: typ Symtab.table,
+    terms: term Symtab.table,
+    unfolds: thm list,
+    assms: thm list option }
+
+  val translate: config -> Proof.context -> thm list -> string * recon
+end
+
+structure SMT_Translate: SMT_TRANSLATE =
+struct
+
+(* intermediate term structure *)
+
+datatype squant = SForall | SExists
+
+datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
+
+datatype sterm =
+  SVar of int |
+  SApp of string * sterm list |
+  SLet of string * sterm * sterm |
+  SQua of squant * string list * sterm spattern list * sterm
+
+
+
+(* configuration options *)
+
+type prefixes = {sort_prefix: string, func_prefix: string}
+
+type strict = {
+  is_builtin_conn: string * typ -> bool,
+  is_builtin_pred: string * typ -> bool,
+  is_builtin_distinct: bool}
+
+type builtins = {
+  builtin_typ: typ -> string option,
+  builtin_num: typ -> int -> string option,
+  builtin_fun: string * typ -> term list -> (string * term list) option }
+
+datatype smt_theory = Integer | Real | Bitvector
+
+type sign = {
+  theories: smt_theory list,
+  sorts: string list,
+  funcs: (string * (string list * string)) list }
+
+type config = {
+  prefixes: prefixes,
+  strict: strict option,
+  builtins: builtins,
+  serialize: sign -> sterm list -> string }
+
+type recon = {
+  typs: typ Symtab.table,
+  terms: term Symtab.table,
+  unfolds: thm list,
+  assms: thm list option }
+
+
+
+(* utility functions *)
+
+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
+
+val quantifier = (fn
+    @{const_name All} => SOME SForall
+  | @{const_name Ex} => SOME SExists
+  | _ => NONE)
+
+fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) =
+      if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
+  | group_quant _ Ts t = (Ts, t)
+
+fun dest_pat ts (Const (@{const_name pat}, _) $ t) = SPat (rev (t :: ts))
+  | dest_pat ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (t :: ts))
+  | dest_pat ts (Const (@{const_name andpat}, _) $ p $ t) = dest_pat (t::ts) p
+  | dest_pat _ t = raise TERM ("dest_pat", [t])
+
+fun dest_trigger (@{term trigger} $ tl $ t) =
+      (map (dest_pat []) (HOLogic.dest_list tl), t)
+  | dest_trigger t = ([], t)
+
+fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
+  let
+    val (Ts, u) = group_quant qn [T] t
+    val (ps, b) = dest_trigger u
+  in (q, rev Ts, ps, b) end)
+
+fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
+  | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
+
+fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm)
+
+
+
+(* enforce a strict separation between formulas and terms *)
+
+val term_eq_rewr = @{lemma "x term_eq y == x = y" by (simp add: term_eq_def)}
+
+val term_bool = @{lemma "~(True term_eq False)" by (simp add: term_eq_def)}
+val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
+
+
+val is_let = (fn Const (@{const_name Let}, _) $ _ $ Abs _ => true | _ => false)
+
+val is_true_eq = (fn
+    @{term "op = :: bool => _"} $ _ $ @{term True} => true
+  | _ => false)
+
+val true_eq_rewr = @{lemma "P = True == P" by simp}
+
+val is_trivial_if = (fn
+    Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
+  | _ => false)
+
+val trivial_if_rewr = @{lemma "(if P then True else False) == P"
+  by (atomize(full)) simp}
+
+fun rewrite _ ct =
+  if is_trivial_if (Thm.term_of ct) then Conv.rewr_conv trivial_if_rewr ct
+  else if is_true_eq (Thm.term_of ct) then Conv.rewr_conv true_eq_rewr ct
+  else if is_let (Thm.term_of ct) then Conv.rewr_conv @{thm Let_def} ct
+  else Conv.all_conv ct
+
+val needs_rewrite =
+  Term.exists_subterm (is_trivial_if orf is_true_eq orf is_let)
+
+fun normalize ctxt thm =
+  if needs_rewrite (Thm.prop_of thm)
+  then Conv.fconv_rule (More_Conv.top_conv rewrite ctxt) thm
+  else thm
+
+val unfold_rules = [term_eq_rewr, Let_def, trivial_if_rewr, true_eq_rewr]
+
+
+val revert_types =
+  let
+    fun revert @{typ prop} = @{typ bool}
+      | revert (Type (n, Ts)) = Type (n, map revert Ts)
+      | revert T = T
+  in Term.map_types revert end
+
+
+fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
+  let
+
+    fun is_builtin_conn' (@{const_name True}, _) = false
+      | is_builtin_conn' (@{const_name False}, _) = false
+      | is_builtin_conn' c = is_builtin_conn c
+
+    val propT = @{typ prop} and boolT = @{typ bool}
+    val as_propT = (fn @{typ bool} => propT | T => T)
+    fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
+    fun conn (n, T) = (n, mapTs as_propT as_propT T)
+    fun pred (n, T) = (n, mapTs I as_propT T)
+
+    val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred
+    fun as_term t = Const term_eq $ t $ @{term True}
+
+    val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
+    fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False}
+
+    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
+
+    fun in_term t =
+      (case Term.strip_comb t of
+        (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
+          c $ in_form t1 $ in_term t2 $ in_term t3
+      | (h as Const c, ts) =>
+          if is_builtin_conn' (conn c) orelse is_builtin_pred (pred c)
+          then wrap_in_if (in_form t)
+          else Term.list_comb (h, map in_term ts)
+      | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
+      | _ => t)
+
+    and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
+      | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
+      | in_pat ((c as Const (@{const_name andpat}, _)) $ p $ t) =
+          c $ in_pat p $ in_term t
+      | in_pat t = raise TERM ("in_pat", [t])
+
+    and in_pats p = in_list @{typ pattern} in_pat p
+
+    and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
+      | in_trig t = in_form t
+
+    and in_form t =
+      (case Term.strip_comb t of
+        (q as Const (qn, _), [Abs (n, T, t')]) =>
+          if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
+          else as_term (in_term t)
+      | (Const (c as (@{const_name distinct}, T)), [t']) =>
+          if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
+          else as_term (in_term t)
+      | (Const c, ts) =>
+          if is_builtin_conn (conn c)
+          then Term.list_comb (Const (conn c), map in_form ts)
+          else if is_builtin_pred (pred c)
+          then Term.list_comb (Const (pred c), map in_term ts)
+          else as_term (in_term t)
+      | _ => as_term (in_term t))
+  in
+    map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms),
+    map (in_form o prop_of) (term_bool :: thms)))
+  end
+
+
+
+(* translation from Isabelle terms into SMT intermediate terms *)
+
+val empty_context = (1, Typtab.empty, 1, Termtab.empty, [])
+
+fun make_sign (_, typs, _, terms, thys) = {
+  theories = thys,
+  sorts = Typtab.fold (cons o snd) typs [],
+  funcs = Termtab.fold (cons o snd) terms [] }
+
+fun make_recon (unfolds, assms) (_, typs, _, terms, _) = {
+  typs = Symtab.make (map swap (Typtab.dest typs)),
+  terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)),
+  unfolds = unfolds,
+  assms = SOME assms }
+
+fun string_of_index pre i = pre ^ string_of_int i
+
+fun add_theory T (Tidx, typs, idx, terms, thys) =
+  let
+    fun add @{typ int} = insert (op =) Integer
+      | add @{typ real} = insert (op =) Real
+      | add (Type (@{type_name word}, _)) = insert (op =) Bitvector
+      | add (Type (_, Ts)) = fold add Ts
+      | add _ = I
+  in (Tidx, typs, idx, terms, add T thys) end
+
+fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms, thys)) =
+  (case Typtab.lookup typs T of
+    SOME s => (s, cx)
+  | NONE =>
+      let
+        val s = string_of_index sort_prefix Tidx
+        val typs' = Typtab.update (T, s) typs
+      in (s, (Tidx+1, typs', idx, terms, thys)) end)
+
+fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms, thys)) =
+  (case Termtab.lookup terms t of
+    SOME (f, _) => (f, cx)
+  | NONE =>
+      let
+        val f = string_of_index func_prefix idx
+        val terms' = Termtab.update (revert_types t, (f, ss)) terms
+      in (f, (Tidx, typs, idx+1, terms', thys)) end)
+
+fun relaxed thms = (([], thms), map prop_of thms)
+
+fun with_context f (ths, ts) =
+  let val (us, context) = fold_map f ts empty_context
+  in ((make_sign context, us), make_recon ths context) end
+
+
+fun translate {prefixes, strict, builtins, serialize} ctxt =
+  let
+    val {sort_prefix, func_prefix} = prefixes
+    val {builtin_typ, builtin_num, builtin_fun} = builtins
+
+    fun transT T = add_theory T #>
+      (case builtin_typ T of
+        SOME n => pair n
+      | NONE => fresh_typ sort_prefix T)
+
+    fun app n ts = SApp (n, ts)
+
+    fun trans t =
+      (case Term.strip_comb t of
+        (Const (qn, _), [Abs (_, T, t1)]) =>
+          (case dest_quant qn T t1 of
+            SOME (q, Ts, ps, b) =>
+              fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
+              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
+          | NONE => raise TERM ("intermediate", [t]))
+      | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
+          transT T ##>> trans t1 ##>> trans t2 #>>
+          (fn ((U, u1), u2) => SLet (U, u1, u2))
+      | (h as Const (c as (@{const_name distinct}, T)), [t1]) =>
+          (case builtin_fun c (HOLogic.dest_list t1) of
+            SOME (n, ts) => add_theory T #> fold_map trans ts #>> app n
+          | NONE => transs h T [t1])
+      | (h as Const (c as (_, T)), ts) =>
+          (case try HOLogic.dest_number t of
+            SOME (T, i) =>
+              (case builtin_num T i of
+                SOME n => add_theory T #> pair (SApp (n, []))
+              | NONE => transs t T [])
+          | NONE =>
+              (case builtin_fun c ts of
+                SOME (n, ts') => add_theory T #> fold_map trans ts' #>> app n
+              | NONE => transs h T ts))
+      | (h as Free (_, T), ts) => transs h T ts
+      | (Bound i, []) => pair (SVar i)
+      | _ => raise TERM ("intermediate", [t]))
+
+    and transs t T ts =
+      let val (Us, U) = dest_funT (length ts) T
+      in
+        fold_map transT Us ##>> transT U #-> (fn Up =>
+        fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp)
+      end
+  in
+    (if is_some strict then strictify (the strict) ctxt else relaxed) #>
+    with_context trans #>> uncurry serialize
+  end
+
+end
diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/SMT/Tools/smtlib_interface.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Wed May 12 23:53:57 2010 +0200
@@ -0,0 +1,214 @@
+(*  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 interface: string list -> SMT_Translate.config
+end
+
+structure SMTLIB_Interface: SMTLIB_INTERFACE =
+struct
+
+structure T = SMT_Translate
+
+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], []))
+
+fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
+  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
+
+
+
+(* builtins *)
+
+fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
+fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
+
+fun builtin_typ @{typ int} = SOME "Int"
+  | builtin_typ @{typ real} = SOME "Real"
+  | builtin_typ (Type (@{type_name word}, [T])) =
+      Option.map (index1 "BitVec") (try dest_binT T)
+  | builtin_typ _ = NONE
+
+fun builtin_num @{typ int} i = SOME (string_of_int i)
+  | builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
+  | builtin_num (Type (@{type_name word}, [T])) i =
+      Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
+  | builtin_num _ _ = NONE
+
+val is_propT = (fn @{typ prop} => true | _ => false)
+fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
+fun is_predT T = is_propT (Term.body_type T)
+
+fun just c ts = SOME (c, ts)
+
+val is_arith_type = member (op =) [@{typ int}, @{typ real}] o Term.domain_type
+
+fun fixed_bvT (Ts, T) x =
+  if forall (can dest_wordT) (T :: Ts) then SOME x else NONE
+
+fun if_fixed_bvT' T = fixed_bvT ([], Term.domain_type T)
+fun if_fixed_bvT T = curry (fixed_bvT ([], Term.domain_type T))
+fun if_full_fixed_bvT T = curry (fixed_bvT (Term.strip_type T))
+
+fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
+  | dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
+fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
+  | dest_nat ts = raise TERM ("dest_nat", ts)
+fun dest_nat_word_funT (T, ts) =
+  (dest_word_funT (Term.range_type T), dest_nat ts)
+
+fun bv_extend n T ts =
+  (case try dest_word_funT T of
+    SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE
+  | _ => NONE)
+
+fun bv_rotate n T ts =
+  try dest_nat ts
+  |> Option.map (fn (i, ts') => (index1 n i, ts'))
+
+fun bv_extract n T ts =
+  try dest_nat_word_funT (T, ts)
+  |> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, ts'))
+
+
+fun conn @{const_name True} = SOME "true"
+  | conn @{const_name False} = SOME "false"
+  | conn @{const_name Not} = SOME "not"
+  | conn @{const_name "op &"} = SOME "and"
+  | conn @{const_name "op |"} = SOME "or"
+  | conn @{const_name "op -->"} = SOME "implies"
+  | conn @{const_name "op ="} = SOME "iff"
+  | conn @{const_name If} = SOME "if_then_else"
+  | conn _ = NONE
+
+fun pred @{const_name distinct} _ = SOME "distinct"
+  | pred @{const_name "op ="} _ = SOME "="
+  | pred @{const_name term_eq} _ = SOME "="
+  | pred @{const_name less} T =
+      if is_arith_type T then SOME "<"
+      else if_fixed_bvT' T "bvult"
+  | pred @{const_name less_eq} T =
+      if is_arith_type T then SOME "<="
+      else if_fixed_bvT' T "bvule"
+  | pred @{const_name word_sless} T = if_fixed_bvT' T "bvslt"
+  | pred @{const_name word_sle} T = if_fixed_bvT' T "bvsle"
+  | pred _ _ = NONE
+
+fun func @{const_name If} _ = just "ite"
+  | func @{const_name uminus} T =
+      if is_arith_type T then just "~"
+      else if_fixed_bvT T "bvneg"
+  | func @{const_name plus} T = 
+      if is_arith_type T then just "+"
+      else if_fixed_bvT T "bvadd"
+  | func @{const_name minus} T =
+      if is_arith_type T then just "-"
+      else if_fixed_bvT T "bvsub"
+  | func @{const_name times} T = 
+      if is_arith_type T then just "*"
+      else if_fixed_bvT T "bvmul"
+  | func @{const_name bitNOT} T = if_fixed_bvT T "bvnot"
+  | func @{const_name bitAND} T = if_fixed_bvT T "bvand"
+  | func @{const_name bitOR} T = if_fixed_bvT T "bvor"
+  | func @{const_name bitXOR} T = if_fixed_bvT T "bvxor"
+  | func @{const_name div} T = if_fixed_bvT T "bvudiv"
+  | func @{const_name mod} T = if_fixed_bvT T "bvurem"
+  | func @{const_name sdiv} T = if_fixed_bvT T "bvsdiv"
+  | func @{const_name smod} T = if_fixed_bvT T "bvsmod"
+  | func @{const_name srem} T = if_fixed_bvT T "bvsrem"
+  | func @{const_name word_cat} T = if_full_fixed_bvT T "concat"
+  | func @{const_name bv_shl} T = if_full_fixed_bvT T "bvshl"
+  | func @{const_name bv_lshr} T = if_full_fixed_bvT T "bvlshr"
+  | func @{const_name bv_ashr} T = if_full_fixed_bvT T "bvashr"
+  | func @{const_name slice} T = bv_extract "extract" T
+  | func @{const_name ucast} T = bv_extend "zero_extend" T
+  | func @{const_name scast} T = bv_extend "sign_extend" T
+  | func @{const_name word_rotl} T = bv_rotate "rotate_left" T
+  | func @{const_name word_rotr} T = bv_rotate "rotate_right" T
+  | func _ _ = K NONE
+
+fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
+fun is_builtin_pred (n, T) = is_predT T andalso is_some (pred n T)
+
+fun builtin_fun (n, T) ts =
+  if is_connT T then conn n |> Option.map (rpair ts)
+  else if is_predT T then pred n T |> Option.map (rpair ts)
+  else func n T ts
+
+
+
+(* serialization *)
+
+val add = Buffer.add
+fun sep f = add " " #> f
+fun enclose l r f = sep (add l #> f #> add r)
+val par = enclose "(" ")"
+fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
+fun line f = f #> add "\n"
+
+fun var i = add "?v" #> add (string_of_int i)
+
+fun sterm l (T.SVar i) = sep (var (l - i - 1))
+  | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
+  | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
+  | sterm l (T.SQua (q, ss, ps, t)) =
+      let
+        val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
+        val vs = map_index (apfst (Integer.add l)) ss
+        fun var_decl (i, s) = par (var i #> sep (add s))
+        val sub = sterm (l + length ss)
+        fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
+        fun pats (T.SPat ts) = pat ":pat" ts
+          | pats (T.SNoPat ts) = pat ":nopat" ts
+      in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end
+
+fun choose_logic theories =
+  if member (op =) theories T.Bitvector then "QF_AUFBV"
+  else if member (op =) theories T.Real then "AUFLIRA"
+  else "AUFLIA"
+
+fun serialize comments {theories, sorts, funcs} ts =
+  Buffer.empty
+  |> line (add "(benchmark Isabelle")
+  |> line (add ":status unknown")
+  |> line (add ":logic " #> add (choose_logic theories))
+  |> length sorts > 0 ?
+       line (add ":extrasorts" #> par (fold (sep o add) sorts))
+  |> length funcs > 0 ? (
+       line (add ":extrafuns" #> add " (") #>
+       fold (fn (f, (ss, s)) =>
+         line (sep (app f (sep o add) (ss @ [s])))) funcs #>
+       line (add ")"))
+  |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
+  |> line (add ":formula true)")
+  |> fold (fn str => line (add "; " #> add str)) comments
+  |> Buffer.content
+
+
+
+(* interface *)
+
+fun interface comments = {
+  prefixes = {
+    sort_prefix = "S",
+    func_prefix = "f"},
+  strict = SOME {
+    is_builtin_conn = is_builtin_conn,
+    is_builtin_pred = is_builtin_pred,
+    is_builtin_distinct = true},
+  builtins = {
+    builtin_typ = builtin_typ,
+    builtin_num = builtin_num,
+    builtin_fun = builtin_fun},
+  serialize = serialize comments}
+
+end
diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/SMT/Tools/z3_interface.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/z3_interface.ML	Wed May 12 23:53:57 2010 +0200
@@ -0,0 +1,35 @@
+(*  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
+
+fun z3_builtin_fun bf c ts =
+  (case Const c of
+    @{term "op / :: real => _"} => SOME ("/", ts)
+  | _ => bf c ts)
+
+fun interface comments =
+  let
+    val {prefixes, strict, builtins, serialize} =
+      SMTLIB_Interface.interface comments
+    val {builtin_typ, builtin_num, builtin_fun} = builtins
+  in
+   {prefixes = prefixes,
+    strict = strict,
+    builtins = {
+      builtin_typ = builtin_typ,
+      builtin_num = builtin_num,
+      builtin_fun = z3_builtin_fun builtin_fun},
+    serialize = serialize}
+  end
+
+end
diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/SMT/Tools/z3_proof.ML
--- a/src/HOL/SMT/Tools/z3_proof.ML	Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_proof.ML	Wed May 12 23:53:57 2010 +0200
@@ -6,8 +6,7 @@
 
 signature Z3_PROOF =
 sig
-  val reconstruct: Proof.context -> thm list option -> SMT_Translate.recon ->
-    string list -> thm
+  val reconstruct: Proof.context -> SMT_Translate.recon -> string list -> thm
 end
 
 structure Z3_Proof: Z3_PROOF =
@@ -56,13 +55,13 @@
 fun make_context (Ttab, ttab, etab, ptab, nctxt) =
   Context {Ttab=Ttab, ttab=ttab, etab=etab, ptab=ptab, nctxt=nctxt}
 
-fun empty_context thy ({typs, terms=ttab} : SMT_Translate.recon) =
+fun empty_context thy ({typs, terms, ...} : SMT_Translate.recon) =
   let
-    val ttab' = Symtab.map (fn @{term True} => @{term "~False"} | t => t) ttab
-    val ns = Symtab.fold (Term.add_free_names o snd) ttab' []
+    val ttab = Symtab.map (fn @{term True} => @{term "~False"} | t => t) terms
+    val ns = Symtab.fold (Term.add_free_names o snd) ttab []
     val nctxt = Name.make_context ns
-    val tt = Symtab.map (Thm.cterm_of thy) ttab'
-  in make_context (typs, tt, Inttab.empty, Inttab.empty, nctxt) end
+    val ttab' = Symtab.map (Thm.cterm_of thy) ttab
+  in make_context (typs, ttab', Inttab.empty, Inttab.empty, nctxt) end
 
 fun map_context f (Context {Ttab, ttab, etab, ptab, nctxt}) =
   make_context (f (Ttab, ttab, etab, ptab, nctxt))
@@ -237,14 +236,15 @@
     |> handle_errors line_no (Scan.finite' Symbol.stopper (node thy))
     |> (fn (stop', (cx', _)) => (stop', line_no + 1, cx'))
 
-fun reconstruct ctxt assms recon output =
+fun reconstruct ctxt recon output =
   let
     val _ = T.var_prefix <> free_prefix orelse error "Same prefixes"
 
     val thy = ProofContext.theory_of ctxt
+    val {unfolds, assms, ...} = recon
   in
     (case fold (parse_line thy) output (NONE, 1, empty_context thy recon) of
-      (SOME p, _, Context {ptab, ...}) => R.prove ctxt assms ptab p
+      (SOME p, _, Context {ptab, ...}) => R.prove ctxt unfolds assms ptab p
     | _ => z3_exn "bad proof")
   end
 
diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/SMT/Tools/z3_proof_rules.ML
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Wed May 12 23:53:57 2010 +0200
@@ -14,8 +14,8 @@
   (*proof reconstruction*)
   type proof
   val make_proof: rule -> int list -> cterm * cterm list -> proof
-  val prove: Proof.context -> thm list option -> proof Inttab.table -> int ->
-    thm
+  val prove: Proof.context -> thm list -> thm list option ->
+    proof Inttab.table -> int -> thm
 
   (*setup*)
   val trace_assms: bool Config.T
@@ -479,19 +479,16 @@
   Attrib.config_bool "z3_trace_assms" (K false)
 
 local
-  val TT_eq = @{lemma "(P = (~False)) == P" by simp}
   val remove_trigger = @{lemma "trigger t p == p"
     by (rule eq_reflection, rule trigger_def)}
-  val remove_iff = @{lemma "p iff q == p = q"
-    by (rule eq_reflection, rule iff_def)}
 
   fun with_context simpset ctxt = Simplifier.context ctxt simpset
 
   val prep_ss = with_context (Simplifier.empty_ss addsimps
-    [@{thm Let_def}, remove_trigger, remove_iff, true_false, TT_eq])
+    [@{thm Let_def}, remove_trigger, true_false])
 
-  val TT_eq_conv = Conv.rewr_conv TT_eq
-  val norm_conv = More_Conv.bottom_conv (K (Conv.try_conv TT_eq_conv))
+  fun norm_conv ctxt unfolds = More_Conv.top_conv
+    (K (Conv.try_conv (More_Conv.rewrs_conv unfolds))) ctxt
 
   val threshold = 10
   
@@ -513,9 +510,10 @@
     val thms = map rewrite assms
   in if length assms < threshold then Some thms else Many (thm_net_of thms) end
 
-fun asserted _ NONE ct = Thm (Thm.assume (T.mk_prop ct))
-  | asserted ctxt (SOME assms) ct =
-      Thm (with_conv (norm_conv ctxt) (lookup_assm ctxt assms) (T.mk_prop ct))
+fun asserted _ _ NONE ct = Thm (Thm.assume (T.mk_prop ct))
+  | asserted ctxt unfolds (SOME assms) ct =
+      Thm (with_conv (norm_conv ctxt unfolds) (lookup_assm ctxt assms)
+        (T.mk_prop ct))
 end
 
 
@@ -1326,7 +1324,7 @@
 fun not_supported r =
   z3_exn ("proof rule not implemented: " ^ quote (string_of_rule r))
 
-fun prove ctxt assms =
+fun prove ctxt unfolds assms =
   let
     val prems = Option.map (prepare_assms ctxt) assms
 
@@ -1334,8 +1332,8 @@
       (case (r, ps) of
         (* core rules *)
         (TrueAxiom, _) => (([], Thm true_thm), ptab)
-      | (Asserted, _) => (([], asserted ctxt prems ct), ptab)
-      | (Goal, _) => (([], asserted ctxt prems ct), ptab)
+      | (Asserted, _) => (([], asserted ctxt unfolds prems ct), ptab)
+      | (Goal, _) => (([], asserted ctxt unfolds prems ct), ptab)
       | (ModusPonens, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
       | (ModusPonensOeq, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
       | (AndElim, [(p, (_, i))]) => apfst (pair []) (and_elim (p, i) ct ptab)
diff -r ea94c03ad567 -r 48cf03469dc6 src/HOL/SMT/Tools/z3_solver.ML
--- a/src/HOL/SMT/Tools/z3_solver.ML	Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_solver.ML	Wed May 12 23:53:57 2010 +0200
@@ -61,9 +61,9 @@
   check_unsat recon output
   |> K @{cprop False}
 
-fun prover ({context, output, recon, assms} : SMT_Solver.proof_data) =
+fun prover ({context, output, recon} : SMT_Solver.proof_data) =
   check_unsat recon output
-  |> Z3_Proof.reconstruct context assms recon
+  |> Z3_Proof.reconstruct context recon
 
 fun solver oracle ctxt =
   let val with_proof = Config.get ctxt proofs