# HG changeset patch
# User ballarin
# Date 1270671769 -7200
# Node ID 32383448c01b5df85d1df3d6a340a60bd0ba1cbc
# Parent  abc6a2ea4b889e11965f0a5291ec531a77a1cf05# Parent  37a5735783c55705644d142deb40a853c1dfc980
Merged.

diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Wed Apr 07 22:22:49 2010 +0200
@@ -82,7 +82,7 @@
 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
 
 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 
 boogie_vc Dijkstra
   using [[z3_proofs=true]]
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/Boogie/Examples/Boogie_Max.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Wed Apr 07 22:22:49 2010 +0200
@@ -39,7 +39,7 @@
 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
 
 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Max.certs"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 
 boogie_vc max
   using [[z3_proofs=true]]
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Wed Apr 07 22:22:49 2010 +0200
@@ -47,7 +47,7 @@
 boogie_open (quiet) "~~/src/HOL/Boogie/Examples/VCC_Max"
 
 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/VCC_Max.certs"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 
 boogie_status
 
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 07 22:22:49 2010 +0200
@@ -8,7 +8,7 @@
 begin
 
 declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 declare [[z3_proofs=true]]
 
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/SMT/Examples/SMT_Examples.thy
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Wed Apr 07 22:22:49 2010 +0200
@@ -17,7 +17,7 @@
 the following option is set to "false":
 *}
 
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 
 
 
@@ -539,7 +539,8 @@
 
 lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> (f (i1 := v1, i2 := v2)) i = f i" by smt
 
-lemma "(f g x = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)" by smt
+lemma "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
+  by smt
 
 lemma "id 3 = 3 \<and> id True = True" by (smt id_def)
 
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/SMT/SMT.thy
--- a/src/HOL/SMT/SMT.thy	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/SMT.thy	Wed Apr 07 22:22:49 2010 +0200
@@ -62,11 +62,11 @@
 
 declare [[ smt_certificates = "" ]]
 
-text {* Enables or disables the addition of new certificates to
-the current certificates file (when disabled, only existing
-certificates are used and no SMT solver is invoked): *}
+text {* Allows or disallows the addition of new certificates to
+the current certificates file (when set to @{text false}, only
+existing certificates are used and no SMT solver is invoked): *}
 
-declare [[ smt_record = true ]]
+declare [[ smt_fixed = false ]]
 
 
 subsection {* Special configuration options *}
@@ -76,8 +76,4 @@
 
 declare [[ smt_trace = false ]]
 
-text {* Unfold (some) definitions passed to the SMT solver: *}
-
-declare [[ smt_unfold_defs = true ]]
-
 end
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/SMT/SMT_Base.thy
--- a/src/HOL/SMT/SMT_Base.thy	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/SMT_Base.thy	Wed Apr 07 22:22:49 2010 +0200
@@ -138,6 +138,6 @@
 use "Tools/smt_solver.ML"
 use "Tools/smtlib_interface.ML"
 
-setup {* SMT_Normalize.setup #> SMT_Solver.setup *}
+setup {* SMT_Solver.setup *}
 
 end
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed Apr 07 22:22:49 2010 +0200
@@ -13,35 +13,19 @@
 
 signature SMT_NORMALIZE =
 sig
-  val normalize_rule: Proof.context -> thm -> thm
   val instantiate_free: cterm * cterm -> thm -> thm
   val discharge_definition: cterm -> thm -> thm
 
-  val trivial_let: Proof.context -> thm list -> thm list
-  val positive_numerals: Proof.context -> thm list -> thm list
-  val nat_as_int: Proof.context -> thm list -> thm list
-  val unfold_defs: bool Config.T
-  val add_pair_rules: Proof.context -> thm list -> thm list
-  val add_fun_upd_rules: Proof.context -> thm list -> thm list
-  val add_abs_min_max_rules: Proof.context -> thm list -> thm list
-
-  datatype config =
-    RewriteTrivialLets |
-    RewriteNegativeNumerals |
-    RewriteNaturalNumbers |
-    AddPairRules |
-    AddFunUpdRules |
-    AddAbsMinMaxRules
-
-  val normalize: config list -> Proof.context -> thm list ->
-    cterm list * thm list
-
-  val setup: theory -> theory
+  val normalize: Proof.context -> thm list -> cterm list * thm list
 end
 
 structure SMT_Normalize: SMT_NORMALIZE =
 struct
 
+infix 2 ??
+fun (test ?? f) x = if test x then f x else x
+
+
 local
   val all1 = @{lemma "All P == ALL x. P x" by (rule reflexive)}
   val all2 = @{lemma "All == (%P. ALL x. P x)" by (rule reflexive)}
@@ -133,7 +117,6 @@
 
 fun normalize_rule ctxt =
   Conv.fconv_rule (
-    unfold_quants_conv ctxt then_conv
     Thm.beta_conversion true then_conv
     Thm.eta_conversion then_conv
     norm_binder_conv ctxt) #>
@@ -141,10 +124,9 @@
   Drule.forall_intr_vars #>
   Conv.fconv_rule (atomize_conv ctxt)
 
-fun instantiate_free (cv, ct) thm =
-  if Term.exists_subterm (equal (Thm.term_of cv)) (Thm.prop_of thm)
-  then Thm.forall_elim ct (Thm.forall_intr cv thm)
-  else thm
+fun instantiate_free (cv, ct) =
+  (Term.exists_subterm (equal (Thm.term_of cv)) o Thm.prop_of) ??
+  (Thm.forall_elim ct o Thm.forall_intr cv)
 
 fun discharge_definition ct thm =
   let val (cv, cu) = Thm.dest_equals ct
@@ -172,11 +154,10 @@
     | is_trivial_let _ = false
 
   fun let_conv _ = if_true_conv is_trivial_let (Conv.rewr_conv @{thm Let_def})
-
-  fun cond_let_conv ctxt = if_true_conv (Term.exists_subterm is_trivial_let)
-    (More_Conv.top_conv let_conv ctxt)
 in
-fun trivial_let ctxt = map (Conv.fconv_rule (cond_let_conv ctxt))
+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
 
 
@@ -190,7 +171,6 @@
         Term.exists_subterm neg_numeral t andalso
         is_number_sort (ProofContext.theory_of ctxt) (Term.body_type T)
     | is_neg_number _ _ = false
-  fun has_neg_number ctxt = Term.exists_subterm (is_neg_number ctxt)
 
   val pos_numeral_ss = HOL_ss
     addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}]
@@ -207,11 +187,10 @@
   fun pos_conv ctxt = if_conv (is_neg_number ctxt)
     (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
     Conv.no_conv
-
-  fun cond_pos_conv ctxt = if_true_conv (has_neg_number ctxt)
-    (More_Conv.top_sweep_conv pos_conv ctxt)
 in
-fun positive_numerals ctxt = map (Conv.fconv_rule (cond_pos_conv ctxt))
+fun positive_numerals ctxt =
+  map ((Term.exists_subterm (is_neg_number ctxt) o Thm.prop_of) ??
+    Conv.fconv_rule (More_Conv.top_sweep_conv pos_conv ctxt))
 end
 
 
@@ -275,23 +254,14 @@
   val uses_nat_int =
     Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
 in
-fun nat_as_int ctxt thms =
-  let
-    fun norm thm = thm
-      |> uses_nat_type (Thm.prop_of thm) ? Conv.fconv_rule (conv ctxt)
-    val thms' = map norm thms
-  in
-    if exists (uses_nat_int o Thm.prop_of) thms' then nat_embedding @ thms'
-    else thms'
-  end
+fun nat_as_int ctxt =
+  map ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt)) #>
+  exists (uses_nat_int o Thm.prop_of) ?? append nat_embedding
 end
 
 
 (* include additional rules *)
 
-val (unfold_defs, unfold_defs_setup) =
-  Attrib.config_bool "smt_unfold_defs" (K true)
-
 local
   val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
 
@@ -302,46 +272,50 @@
   val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
   val exists_fun_upd = Term.exists_subterm is_fun_upd
 in
-fun add_pair_rules _ thms =
-  thms
-  |> exists (exists_pair_type o Thm.prop_of) thms ? append pair_rules
+fun add_pair_rules _ =
+  exists (exists_pair_type o Thm.prop_of) ?? append pair_rules
 
-fun add_fun_upd_rules _ thms =
-  thms
-  |> exists (exists_fun_upd o Thm.prop_of) thms ? append fun_upd_rules
+fun add_fun_upd_rules _ =
+  exists (exists_fun_upd o Thm.prop_of) ?? append fun_upd_rules
 end
 
 
+(* unfold definitions of specific constants *)
+
 local
-  fun mk_entry t thm = (Term.head_of t, (thm, thm RS @{thm eq_reflection}))
+  fun mk_entry (t as Const (n, _)) thm = ((n, t), thm)
+    | mk_entry t _ = raise TERM ("mk_entry", [t])
   fun prepare_def thm =
-    (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
-      Const (@{const_name "op ="}, _) $ t $ _ => mk_entry t thm
+    (case Thm.prop_of thm of
+      Const (@{const_name "=="}, _) $ t $ _ => mk_entry (Term.head_of t) thm
     | t => raise TERM ("prepare_def", [t]))
 
   val defs = map prepare_def [
-    @{thm abs_if[where 'a = int]}, @{thm abs_if[where 'a = real]},
-    @{thm min_def[where 'a = int]}, @{thm min_def[where 'a = real]},
-    @{thm max_def[where 'a = int]}, @{thm max_def[where 'a = real]}]
+    @{thm abs_if[where 'a = int, THEN eq_reflection]},
+    @{thm abs_if[where 'a = real, THEN eq_reflection]},
+    @{thm min_def[where 'a = int, THEN eq_reflection]},
+    @{thm min_def[where 'a = real, THEN eq_reflection]},
+    @{thm max_def[where 'a = int, THEN eq_reflection]},
+    @{thm max_def[where 'a = real, THEN eq_reflection]},
+    @{thm Ex1_def}, @{thm Ball_def}, @{thm Bex_def}]
 
-  fun add_sym t = if AList.defined (op =) defs t then insert (op =) t else I
-  fun add_syms thms = fold (Term.fold_aterms add_sym o Thm.prop_of) thms []
+  fun matches thy ((t as Const (n, _)), (m, p)) =
+        n = m andalso Pattern.matches thy (p, t)
+    | matches _ _ = false
 
-  fun unfold_def_conv ds ct =
-    (case AList.lookup (op =) ds (Term.head_of (Thm.term_of ct)) of
-      SOME (_, eq) => Conv.rewr_conv eq
+  fun lookup_def thy = AList.lookup (matches thy) defs
+  fun lookup_def_head thy = lookup_def thy o Term.head_of
+
+  fun occurs_def thy = Term.exists_subterm (is_some o lookup_def thy)
+
+  fun unfold_def_conv ctxt ct =
+    (case lookup_def_head (ProofContext.theory_of ctxt) (Thm.term_of ct) of
+      SOME thm => Conv.rewr_conv thm
     | NONE => Conv.all_conv) ct
-
-  fun unfold_conv ctxt thm =
-    (case filter (member (op =) (add_syms [thm]) o fst) defs of
-      [] => thm
-    | ds => thm |> Conv.fconv_rule
-        (More_Conv.bottom_conv (K (unfold_def_conv ds)) ctxt))
 in
-fun add_abs_min_max_rules ctxt thms =
-  if Config.get ctxt unfold_defs
-  then map (unfold_conv ctxt) thms
-  else map fst (map_filter (AList.lookup (op =) defs) (add_syms thms)) @ thms
+fun unfold_defs ctxt =
+  (occurs_def (ProofContext.theory_of ctxt) o Thm.prop_of) ??
+  Conv.fconv_rule (More_Conv.top_conv unfold_def_conv ctxt)
 end
 
 
@@ -496,29 +470,15 @@
 
 (* combined normalization *)
 
-datatype config =
-  RewriteTrivialLets |
-  RewriteNegativeNumerals |
-  RewriteNaturalNumbers |
-  AddPairRules |
-  AddFunUpdRules |
-  AddAbsMinMaxRules
-
-fun normalize config ctxt thms =
-  let fun if_enabled c f = member (op =) config c ? f ctxt
-  in
-    thms
-    |> if_enabled RewriteTrivialLets trivial_let
-    |> if_enabled RewriteNegativeNumerals positive_numerals
-    |> if_enabled RewriteNaturalNumbers nat_as_int
-    |> if_enabled AddPairRules add_pair_rules
-    |> if_enabled AddFunUpdRules add_fun_upd_rules
-    |> if_enabled AddAbsMinMaxRules add_abs_min_max_rules
-    |> map (normalize_rule ctxt)
-    |> lift_lambdas ctxt
-    |> apsnd (explicit_application ctxt)
-  end
-
-val setup = unfold_defs_setup
+fun normalize ctxt thms =
+  thms
+  |> trivial_let ctxt
+  |> positive_numerals ctxt
+  |> nat_as_int ctxt
+  |> add_pair_rules ctxt
+  |> add_fun_upd_rules ctxt
+  |> map (unfold_defs ctxt #> normalize_rule ctxt)
+  |> lift_lambdas ctxt
+  |> apsnd (explicit_application ctxt)
 
 end
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 22:22:49 2010 +0200
@@ -9,9 +9,6 @@
   exception SMT of string
   exception SMT_COUNTEREXAMPLE of bool * term list
 
-  type interface = {
-    normalize: SMT_Normalize.config list,
-    translate: SMT_Translate.config }
   type proof_data = {
     context: Proof.context,
     output: string list,
@@ -20,7 +17,7 @@
   type solver_config = {
     command: {env_var: string, remote_name: string option},
     arguments: string list,
-    interface: string list -> interface,
+    interface: string list -> SMT_Translate.config,
     reconstruct: proof_data -> thm }
 
   (*options*)
@@ -30,7 +27,7 @@
   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
 
   (*certificates*)
-  val record: bool Config.T
+  val fixed_certificates: bool Config.T
   val select_certificates: string -> Context.generic -> Context.generic
 
   (*solvers*)
@@ -60,10 +57,6 @@
 exception SMT_COUNTEREXAMPLE of bool * term list
 
 
-type interface = {
-  normalize: SMT_Normalize.config list,
-  translate: SMT_Translate.config }
-
 type proof_data = {
   context: Proof.context,
   output: string list,
@@ -73,7 +66,7 @@
 type solver_config = {
   command: {env_var: string, remote_name: string option},
   arguments: string list,
-  interface: string list -> interface,
+  interface: string list -> SMT_Translate.config,
   reconstruct: proof_data -> thm }
 
 
@@ -93,7 +86,8 @@
 
 (* SMT certificates *)
 
-val (record, setup_record) = Attrib.config_bool "smt_record" (K true)
+val (fixed_certificates, setup_fixed_certificates) =
+  Attrib.config_bool "smt_fixed" (K false)
 
 structure Certificates = Generic_Data
 (
@@ -112,22 +106,6 @@
 
 local
 
-fun invoke ctxt output f problem_path =
-  let
-    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
-      (map Pretty.str ls))
-
-    val x = File.open_output output problem_path
-    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
-      problem_path
-
-    val (res, err) = with_timeout ctxt f problem_path
-    val _ = trace_msg ctxt (pretty "SMT solver:") err
-
-    val ls = rev (dropwhile (equal "") (rev res))
-    val _ = trace_msg ctxt (pretty "SMT result:") ls
-  in (x, ls) end
-
 fun choose {env_var, remote_name} =
   let
     val local_solver = getenv env_var
@@ -150,29 +128,40 @@
   map File.shell_quote (solver @ args) @
   [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
 
-fun no_cmd _ _ = error ("Bad certificates cache: missing certificate")
-
-fun run ctxt cmd args problem_path =
-  let val certs = Certificates.get (Context.Proof ctxt)
-  in
-    if is_none certs 
-    then Cache_IO.run' (make_cmd (choose cmd) args) problem_path
-    else if Config.get ctxt record
-    then Cache_IO.cached' (the certs) (make_cmd (choose cmd) args) problem_path
-    else
-     (tracing ("Using cached certificate from " ^
-        File.shell_path (Cache_IO.cache_path_of (the certs)) ^ " ...");
-      Cache_IO.cached' (the certs) no_cmd problem_path)
-  end
+fun run ctxt cmd args input =
+  (case Certificates.get (Context.Proof ctxt) of
+    NONE => Cache_IO.run (make_cmd (choose cmd) args) input
+  | SOME certs =>
+      (case Cache_IO.lookup certs input of
+        (NONE, key) =>
+          if Config.get ctxt fixed_certificates
+          then error ("Bad certificates cache: missing certificate")
+          else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
+            input
+      | (SOME output, _) =>
+         (tracing ("Using cached certificate from " ^
+            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
+          output)))
 
 in
 
-fun run_solver ctxt cmd args output =
-  Cache_IO.with_tmp_file "smt-" (invoke ctxt output (run ctxt cmd args))
+fun run_solver ctxt cmd args input =
+  let
+    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
+      (map Pretty.str ls))
+
+    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input
+
+    val (res, err) = with_timeout ctxt (run ctxt cmd args) input
+    val _ = trace_msg ctxt (pretty "SMT solver:") err
+
+    val ls = rev (dropwhile (equal "") (rev res))
+    val _ = trace_msg ctxt (pretty "SMT result:") ls
+  in ls end
 
 end
 
-fun make_proof_data ctxt ((recon, thms), ls) =
+fun make_proof_data ctxt (ls, (recon, thms)) =
   {context=ctxt, output=ls, recon=recon, assms=SOME thms}
 
 fun gen_solver name solver ctxt prems =
@@ -181,11 +170,12 @@
     val comments = ("solver: " ^ name) ::
       ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
       "arguments:" :: arguments
-    val {normalize=nc, translate=tc} = interface comments
+    val tc = interface comments
     val thy = ProofContext.theory_of ctxt
   in
-    SMT_Normalize.normalize nc ctxt prems
-    ||> run_solver ctxt command arguments o SMT_Translate.translate tc thy
+    SMT_Normalize.normalize ctxt prems
+    ||> SMT_Translate.translate tc thy
+    ||> apfst (run_solver ctxt command arguments)
     ||> reconstruct o make_proof_data ctxt
     |-> fold SMT_Normalize.discharge_definition
   end
@@ -261,11 +251,22 @@
            | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st)
 
   fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules
+
+  val has_topsort = Term.exists_type (Term.exists_subtype (fn
+      TFree (_, []) => true
+    | TVar (_, []) => true
+    | _ => false))
 in
 fun smt_tac' pass_exns ctxt rules =
   Tactic.rtac @{thm ccontr} THEN'
   SUBPROOF (fn {context, prems, ...} =>
-    SAFE pass_exns (Tactic.rtac o smt_solver (rules @ prems)) context 1) ctxt
+    let val thms = rules @ prems
+    in
+      if exists (has_topsort o Thm.prop_of) thms
+      then fail_tac (trace_msg context I)
+        "SMT: proof state contains the universal sort {}"
+      else SAFE pass_exns (Tactic.rtac o smt_solver thms) context 1
+    end) ctxt
 
 val smt_tac = smt_tac' false
 end
@@ -285,7 +286,7 @@
     "SMT solver configuration" #>
   setup_timeout #>
   setup_trace #>
-  setup_record #>
+  setup_fixed_certificates #>
   Attrib.setup (Binding.name "smt_certificates")
     (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/SMT/Tools/smt_translate.ML
--- a/src/HOL/SMT/Tools/smt_translate.ML	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Wed Apr 07 22:22:49 2010 +0200
@@ -55,11 +55,10 @@
     prefixes: prefixes,
     markers: markers,
     builtins: builtins,
-    serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
+    serialize: sign -> (string, string) sterm list -> string}
   type recon = {typs: typ Symtab.table, terms: term Symtab.table}
 
-  val translate: config -> theory -> thm list -> TextIO.outstream ->
-    recon * thm list
+  val translate: config -> theory -> thm list -> string * (recon * thm list)
 
   val dest_binT: typ -> int
   val dest_funT: int -> typ -> typ list * typ
@@ -180,7 +179,7 @@
   prefixes: prefixes,
   markers: markers,
   builtins: builtins,
-  serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
+  serialize: sign -> (string, string) sterm list -> string}
 type recon = {typs: typ Symtab.table, terms: term Symtab.table}
 
 
@@ -527,7 +526,7 @@
 
 (* Combination of all translation functions and invocation of serialization. *)
 
-fun translate config thy thms stream =
+fun translate config thy thms =
   let val {strict, prefixes, markers, builtins, serialize} = config
   in
     map Thm.prop_of thms
@@ -535,8 +534,8 @@
     |> intermediate
     |> (if strict then separate thy else pair [])
     ||>> signature_of prefixes markers builtins thy
-    ||> (fn (sgn, ts) => serialize sgn ts stream)
-    |> (fn ((thms', rtab), _) => (rtab, thms' @ thms))
+    ||> (fn (sgn, ts) => serialize sgn ts)
+    |> (fn ((thms', rtab), str) => (str, (rtab, thms' @ thms)))
   end
 
 end
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/SMT/Tools/smtlib_interface.ML
--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Wed Apr 07 22:22:49 2010 +0200
@@ -9,8 +9,8 @@
   val basic_builtins: SMT_Translate.builtins
   val default_attributes: string list
   val gen_interface: SMT_Translate.builtins -> string list -> string list ->
-    SMT_Solver.interface
-  val interface: string list -> SMT_Solver.interface
+    SMT_Translate.config
+  val interface: string list -> SMT_Translate.config
 end
 
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
@@ -61,7 +61,7 @@
 
 (* serialization *)
 
-fun wr s stream = (TextIO.output (stream, s); stream)
+val wr = Buffer.add
 fun wr_line f = f #> wr "\n"
 
 fun sep f = wr " " #> f
@@ -118,11 +118,10 @@
           | 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 stream =
-  let
-    fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
+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
-    stream
+    Buffer.empty
     |> wr_line (wr "(benchmark Isabelle")
     |> wr_line (wr ":status unknown")
     |> fold (wr_line o wr) attributes
@@ -140,7 +139,7 @@
     |> wr_line (wr ":formula true")
     |> wr_line (wr ")")
     |> fold (fn comment => wr_line (wr ("; " ^ comment))) comments
-    |> K ()
+    |> Buffer.content
   end
 
 
@@ -154,25 +153,17 @@
 val default_attributes = [":logic AUFLIRA"]
 
 fun gen_interface builtins attributes comments = {
-  normalize = [
-    SMT_Normalize.RewriteTrivialLets,
-    SMT_Normalize.RewriteNegativeNumerals,
-    SMT_Normalize.RewriteNaturalNumbers,
-    SMT_Normalize.AddAbsMinMaxRules,
-    SMT_Normalize.AddPairRules,
-    SMT_Normalize.AddFunUpdRules ],
-  translate = {
-    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 }}
+  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
diff -r abc6a2ea4b88 -r 32383448c01b src/HOL/SMT/Tools/z3_interface.ML
--- a/src/HOL/SMT/Tools/z3_interface.ML	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_interface.ML	Wed Apr 07 22:22:49 2010 +0200
@@ -6,7 +6,7 @@
 
 signature Z3_INTERFACE =
 sig
-  val interface: string list -> SMT_Solver.interface
+  val interface: string list -> SMT_Translate.config
 end
 
 structure Z3_Interface: Z3_INTERFACE =
diff -r abc6a2ea4b88 -r 32383448c01b src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Wed Apr 07 19:17:10 2010 +0200
+++ b/src/Tools/cache_io.ML	Wed Apr 07 22:22:49 2010 +0200
@@ -7,20 +7,23 @@
 signature CACHE_IO =
 sig
   val with_tmp_file: string -> (Path.T -> 'a) -> 'a
-  val run: (Path.T -> string) -> Path.T -> string list
-  val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list
+  val run: (Path.T -> Path.T -> string) -> string -> string list * string list
 
   type cache
   val make: Path.T -> cache
   val cache_path_of: cache -> Path.T
-  val cached: cache -> (Path.T -> string) -> Path.T -> string list
-  val cached': cache -> (Path.T -> Path.T -> string) -> Path.T ->
+  val lookup: cache -> string -> (string list * string list) option * string
+  val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
+    string -> string list * string list
+  val run_cached: cache -> (Path.T -> Path.T -> string) -> string ->
     string list * string list
 end
 
 structure Cache_IO : CACHE_IO =
 struct
 
+val cache_io_prefix = "cache-io-"
+
 fun with_tmp_file name f =
   let
     val path = File.tmp_path (Path.explode (name ^ serial_string ()))
@@ -28,14 +31,14 @@
     val _ = try File.rm path
   in Exn.release x end
 
-fun run' make_cmd in_path =
-  with_tmp_file "cache-io-" (fn out_path =>
+fun run make_cmd str =
+  with_tmp_file cache_io_prefix (fn in_path =>
+  with_tmp_file cache_io_prefix (fn out_path =>
     let
+      val _ = File.write in_path str
       val (out2, _) = bash_output (make_cmd in_path out_path)
       val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
-    in (out1, split_lines out2) end)
-
-fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path)
+    in (out1, split_lines out2) end))
 
 
 
@@ -85,28 +88,35 @@
       else (i, xsp)
   in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
 
-fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
-  let val key = SHA1.digest (File.read in_path)
+
+fun lookup (Cache {path=cache_path, table}) str =
+  let val key = SHA1.digest str
   in
     (case Symtab.lookup (snd (Synchronized.value table)) key of
-      SOME pos => load_cached_result cache_path pos
-    | NONE =>
-        let
-          val res as (out, err) = run' make_cmd in_path
-          val (l1, l2) = pairself length res
-          val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
-          val lines = map (suffix "\n") (header :: out @ err)
-
-          val _ = Synchronized.change table (fn (p, tab) =>
-            if Symtab.defined tab key then (p, tab)
-            else
-              let val _ = File.append_list cache_path lines
-              in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
-        in res end)
+      NONE => (NONE, key)
+    | SOME pos => (SOME (load_cached_result cache_path pos), key))
   end
 
-fun cached cache make_cmd =
-  snd o cached' cache (fn in_path => fn _ => make_cmd in_path)
+
+fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
+  let
+    val res as (out, err) = run make_cmd str
+    val (l1, l2) = pairself length res
+    val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
+    val lines = map (suffix "\n") (header :: out @ err)
+
+    val _ = Synchronized.change table (fn (p, tab) =>
+      if Symtab.defined tab key then (p, tab)
+      else
+        let val _ = File.append_list cache_path lines
+        in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
+  in res end
+
+
+fun run_cached cache make_cmd str =
+  (case lookup cache str of
+    (NONE, key) => run_and_cache cache key make_cmd str
+  | (SOME output, _) => output)
 
 end
 end