# HG changeset patch # User boehmes # Date 1273701238 -7200 # Node ID 2f172cf4fb52cdd27d5cb20441080d0dc8707d6c # Parent 48cf03469dc646878ee1d40bd56d809f75100a87 added tracing of reconstruction data diff -r 48cf03469dc6 -r 2f172cf4fb52 src/HOL/SMT/Tools/smt_solver.ML --- a/src/HOL/SMT/Tools/smt_solver.ML Wed May 12 23:53:57 2010 +0200 +++ b/src/HOL/SMT/Tools/smt_solver.ML Wed May 12 23:53:58 2010 +0200 @@ -162,9 +162,21 @@ end +fun trace_recon_data ctxt {typs, terms, ...} = + let + fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] + fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) + fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) + in + trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [ + Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)), + Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) () + end + fun invoke translate_config command arguments ctxt thms = thms |> SMT_Translate.translate translate_config ctxt + ||> tap (trace_recon_data ctxt) |>> run_solver ctxt command arguments |> (fn (ls, recon) => {context=ctxt, output=ls, recon=recon})