# HG changeset patch # User boehmes # Date 1274972946 -7200 # Node ID e3f18cfc98299f7d6a73f4bb4579aff420bb657b # Parent f6ae8db23352caa100890997921800d1417bdae8 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks) diff -r f6ae8db23352 -r e3f18cfc9829 src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML Thu May 27 16:30:26 2010 +0200 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Thu May 27 17:09:06 2010 +0200 @@ -248,17 +248,20 @@ | pats (T.SNoPat ts) = pat ":nopat" ts in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end +fun ssort sorts = sort fast_string_ord sorts +fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs + fun serialize comments {header, sorts, funcs} ts = Buffer.empty |> line (add "(benchmark Isabelle") |> line (add ":status unknown") |> fold (line o add) header |> length sorts > 0 ? - line (add ":extrasorts" #> par (fold (sep o add) sorts)) + line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts))) |> length funcs > 0 ? ( line (add ":extrafuns" #> add " (") #> fold (fn (f, (ss, s)) => - line (sep (app f (sep o add) (ss @ [s])))) funcs #> + line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #> line (add ")")) |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts |> line (add ":formula true)")