# HG changeset patch
# User boehmes
# Date 1266333634 -3600
# Node ID 5e8935678ee4e37297a665ae5e3c3e1ec62ce4a3
# Parent  6007909a28bc29b3056a325cf2d8500d45922450
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)

diff -r 6007909a28bc -r 5e8935678ee4 src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Feb 16 15:26:24 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Feb 16 16:20:34 2010 +0100
@@ -57,4 +57,4 @@
 
 boogie_end
 
-end
\ No newline at end of file
+end
diff -r 6007909a28bc -r 5e8935678ee4 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 16 15:26:24 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 16 16:20:34 2010 +0100
@@ -20,7 +20,7 @@
   type solver_config = {
     command: {env_var: string, remote_name: string option},
     arguments: string list,
-    interface: interface,
+    interface: string list -> interface,
     reconstruct: proof_data -> thm }
 
   (*options*)
@@ -73,7 +73,7 @@
 type solver_config = {
   command: {env_var: string, remote_name: string option},
   arguments: string list,
-  interface: interface,
+  interface: string list -> interface,
   reconstruct: proof_data -> thm }
 
 
@@ -175,10 +175,13 @@
 fun make_proof_data ctxt ((recon, thms), ls) =
   {context=ctxt, output=ls, recon=recon, assms=SOME thms}
 
-fun gen_solver solver ctxt prems =
+fun gen_solver name solver ctxt prems =
   let
     val {command, arguments, interface, reconstruct} = solver ctxt
-    val {normalize=nc, translate=tc} = interface
+    val comments = ("solver: " ^ name) ::
+      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
+      "arguments:" :: arguments
+    val {normalize=nc, translate=tc} = interface comments
     val thy = ProofContext.theory_of ctxt
   in
     SMT_Normalize.normalize nc ctxt prems
@@ -221,17 +224,19 @@
 
 val solver_name_of = Selected_Solver.get
 
-fun select_solver name gen =
-  if is_none (lookup_solver (Context.theory_of gen) name)
+fun select_solver name context =
+  if is_none (lookup_solver (Context.theory_of context) name)
   then error ("SMT solver not registered: " ^ quote name)
-  else Selected_Solver.map (K name) gen
+  else Selected_Solver.map (K name) context
 
-fun raw_solver_of gen =
-  (case lookup_solver (Context.theory_of gen) (solver_name_of gen) of
+fun raw_solver_of context name =
+  (case lookup_solver (Context.theory_of context) name of
     NONE => error "No SMT solver selected"
   | SOME (s, _) => s)
 
-val solver_of = gen_solver o raw_solver_of
+fun solver_of context =
+  let val name = solver_name_of context
+  in gen_solver name (raw_solver_of context name) end
 
 
 (* SMT tactic *)
diff -r 6007909a28bc -r 5e8935678ee4 src/HOL/SMT/Tools/smtlib_interface.ML
--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Feb 16 15:26:24 2010 +0100
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Feb 16 16:20:34 2010 +0100
@@ -8,9 +8,9 @@
 sig
   val basic_builtins: SMT_Translate.builtins
   val default_attributes: string list
-  val gen_interface: SMT_Translate.builtins -> string list ->
+  val gen_interface: SMT_Translate.builtins -> string list -> string list ->
     SMT_Solver.interface
-  val interface: SMT_Solver.interface
+  val interface: string list -> SMT_Solver.interface
 end
 
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
@@ -118,12 +118,13 @@
           | 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 ({typs, funs, preds} : T.sign) ts stream =
+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)))
   in
     stream
     |> wr_line (wr "(benchmark Isabelle")
+    |> wr_line (wr ":status unknown")
     |> fold (wr_line o wr) attributes
     |> length typs > 0 ?
          wr_line (wr ":extrasorts" #> par (fold wr1 typs))
@@ -138,6 +139,7 @@
     |> fold (fn t => wr ":assumption" #> wr_line (wr_expr false [] t)) ts
     |> wr_line (wr ":formula true")
     |> wr_line (wr ")")
+    |> fold (fn comment => wr_line (wr ("; " ^ comment))) comments
     |> K ()
   end
 
@@ -149,9 +151,9 @@
   builtin_num = builtin_num,
   builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
 
-val default_attributes = [":logic AUFLIRA", ":status unknown"]
+val default_attributes = [":logic AUFLIRA"]
 
-fun gen_interface builtins attributes = {
+fun gen_interface builtins attributes comments = {
   normalize = [
     SMT_Normalize.RewriteTrivialLets,
     SMT_Normalize.RewriteNegativeNumerals,
@@ -170,8 +172,9 @@
       term_marker = term_marker,
       formula_marker = formula_marker },
     builtins = builtins,
-    serialize = serialize attributes }}
+    serialize = serialize attributes comments }}
 
-val interface = gen_interface basic_builtins default_attributes
+fun interface comments =
+  gen_interface basic_builtins default_attributes comments
 
 end
diff -r 6007909a28bc -r 5e8935678ee4 src/HOL/SMT/Tools/z3_interface.ML
--- a/src/HOL/SMT/Tools/z3_interface.ML	Tue Feb 16 15:26:24 2010 +0100
+++ b/src/HOL/SMT/Tools/z3_interface.ML	Tue Feb 16 16:20:34 2010 +0100
@@ -6,7 +6,7 @@
 
 signature Z3_INTERFACE =
 sig
-  val interface: SMT_Solver.interface
+  val interface: string list -> SMT_Solver.interface
 end
 
 structure Z3_Interface: Z3_INTERFACE =