# HG changeset patch # User boehmes # Date 1270665642 -7200 # Node ID 37a5735783c55705644d142deb40a853c1dfc980 # Parent 8e5454761f2670efadf4cd19b0056f11525e71a4 buffered output (faster than direct output) diff -r 8e5454761f26 -r 37a5735783c5 src/HOL/SMT/Tools/smt_solver.ML --- a/src/HOL/SMT/Tools/smt_solver.ML Wed Apr 07 20:40:42 2010 +0200 +++ b/src/HOL/SMT/Tools/smt_solver.ML Wed Apr 07 20:40:42 2010 +0200 @@ -106,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 @@ -144,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 fixed_certificates - 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 = @@ -179,7 +174,8 @@ val thy = ProofContext.theory_of ctxt in SMT_Normalize.normalize ctxt prems - ||> run_solver ctxt command arguments o SMT_Translate.translate tc thy + ||> SMT_Translate.translate tc thy + ||> apfst (run_solver ctxt command arguments) ||> reconstruct o make_proof_data ctxt |-> fold SMT_Normalize.discharge_definition end diff -r 8e5454761f26 -r 37a5735783c5 src/HOL/SMT/Tools/smt_translate.ML --- a/src/HOL/SMT/Tools/smt_translate.ML Wed Apr 07 20:40:42 2010 +0200 +++ b/src/HOL/SMT/Tools/smt_translate.ML Wed Apr 07 20:40:42 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 8e5454761f26 -r 37a5735783c5 src/HOL/SMT/Tools/smtlib_interface.ML --- a/src/HOL/SMT/Tools/smtlib_interface.ML Wed Apr 07 20:40:42 2010 +0200 +++ b/src/HOL/SMT/Tools/smtlib_interface.ML Wed Apr 07 20:40:42 2010 +0200 @@ -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