keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)

--- a/src/HOL/Tools/SMT/smt_config.ML	Tue Nov 16 12:08:28 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Nov 17 08:14:55 2010 +0100
@@ -25,6 +25,7 @@
   val monomorph_limit: int Config.T
   val drop_bad_facts: bool Config.T
   val filter_only_facts: bool Config.T
+  val debug_files: string Config.T
 
   (*tools*)
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
@@ -131,6 +132,10 @@
 val (filter_only_facts, setup_filter_only_facts) =
   Attrib.config_bool filter_only_factsN (K false)
 
+val debug_filesN = "smt_debug_files"
+val (debug_files, setup_debug_files) =
+  Attrib.config_string debug_filesN (K "")
+
 val setup_options =
   setup_oracle #>
   setup_datatypes #>
@@ -141,7 +146,8 @@
   setup_monomorph_limit #>
   setup_drop_bad_facts #>
   setup_filter_only_facts #>
-  setup_trace_used_facts
+  setup_trace_used_facts #>
+  setup_debug_files
 
 
 (* diagnostics *)

--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 16 12:08:28 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Nov 17 08:14:55 2010 +0100
@@ -108,7 +108,17 @@
 
 fun run ctxt cmd args input =
   (case C.certificates_of ctxt of
-    NONE => Cache_IO.run (make_cmd (choose cmd) args) input
+    NONE =>
+      if Config.get ctxt C.debug_files = "" then
+        Cache_IO.run (make_cmd (choose cmd) args) input
+      else
+        let
+          val base_path = Path.explode (Config.get ctxt C.debug_files)
+          val in_path = Path.ext "smt_in" base_path
+          val out_path = Path.ext "smt_out" base_path
+        in
+          Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path 
+        end
   | SOME certs =>
       (case Cache_IO.lookup certs input of
         (NONE, key) =>

--- a/src/Tools/cache_io.ML	Tue Nov 16 12:08:28 2010 -0800
+++ b/src/Tools/cache_io.ML	Wed Nov 17 08:14:55 2010 +0100
@@ -13,6 +13,8 @@
     output: string list,
     redirected_output: string list,
     return_code: int}
+  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T ->
+    result
   val run: (Path.T -> Path.T -> string) -> string -> result
 
   (*cache*)
@@ -52,14 +54,16 @@
   redirected_output: string list,
   return_code: int}
 
+fun raw_run make_cmd str in_path out_path =
+  let
+    val _ = File.write in_path str
+    val (out2, rc) = bash_output (make_cmd in_path out_path)
+    val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
+  in {output=split_lines out2, redirected_output=out1, return_code=rc} end
+
 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, rc) = bash_output (make_cmd in_path out_path)
-      val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
-    in {output=split_lines out2, redirected_output=out1, return_code=rc} end))
+  with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
 
 
 (* cache *)