1.1 --- a/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Feb 16 15:26:24 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Feb 16 16:20:34 2010 +0100
     1.3 @@ -57,4 +57,4 @@
     1.4  
     1.5  boogie_end
     1.6  
     1.7 -end
     1.8 \ No newline at end of file
     1.9 +end

     2.1 --- a/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 16 15:26:24 2010 +0100
     2.2 +++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 16 16:20:34 2010 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4    type solver_config = {
     2.5      command: {env_var: string, remote_name: string option},
     2.6      arguments: string list,
     2.7 -    interface: interface,
     2.8 +    interface: string list -> interface,
     2.9      reconstruct: proof_data -> thm }
    2.10  
    2.11    (*options*)
    2.12 @@ -73,7 +73,7 @@
    2.13  type solver_config = {
    2.14    command: {env_var: string, remote_name: string option},
    2.15    arguments: string list,
    2.16 -  interface: interface,
    2.17 +  interface: string list -> interface,
    2.18    reconstruct: proof_data -> thm }
    2.19  
    2.20  
    2.21 @@ -175,10 +175,13 @@
    2.22  fun make_proof_data ctxt ((recon, thms), ls) =
    2.23    {context=ctxt, output=ls, recon=recon, assms=SOME thms}
    2.24  
    2.25 -fun gen_solver solver ctxt prems =
    2.26 +fun gen_solver name solver ctxt prems =
    2.27    let
    2.28      val {command, arguments, interface, reconstruct} = solver ctxt
    2.29 -    val {normalize=nc, translate=tc} = interface
    2.30 +    val comments = ("solver: " ^ name) ::
    2.31 +      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
    2.32 +      "arguments:" :: arguments
    2.33 +    val {normalize=nc, translate=tc} = interface comments
    2.34      val thy = ProofContext.theory_of ctxt
    2.35    in
    2.36      SMT_Normalize.normalize nc ctxt prems
    2.37 @@ -221,17 +224,19 @@
    2.38  
    2.39  val solver_name_of = Selected_Solver.get
    2.40  
    2.41 -fun select_solver name gen =
    2.42 -  if is_none (lookup_solver (Context.theory_of gen) name)
    2.43 +fun select_solver name context =
    2.44 +  if is_none (lookup_solver (Context.theory_of context) name)
    2.45    then error ("SMT solver not registered: " ^ quote name)
    2.46 -  else Selected_Solver.map (K name) gen
    2.47 +  else Selected_Solver.map (K name) context
    2.48  
    2.49 -fun raw_solver_of gen =
    2.50 -  (case lookup_solver (Context.theory_of gen) (solver_name_of gen) of
    2.51 +fun raw_solver_of context name =
    2.52 +  (case lookup_solver (Context.theory_of context) name of
    2.53      NONE => error "No SMT solver selected"
    2.54    | SOME (s, _) => s)
    2.55  
    2.56 -val solver_of = gen_solver o raw_solver_of
    2.57 +fun solver_of context =
    2.58 +  let val name = solver_name_of context
    2.59 +  in gen_solver name (raw_solver_of context name) end
    2.60  
    2.61  
    2.62  (* SMT tactic *)

     3.1 --- a/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Feb 16 15:26:24 2010 +0100
     3.2 +++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Feb 16 16:20:34 2010 +0100
     3.3 @@ -8,9 +8,9 @@
     3.4  sig
     3.5    val basic_builtins: SMT_Translate.builtins
     3.6    val default_attributes: string list
     3.7 -  val gen_interface: SMT_Translate.builtins -> string list ->
     3.8 +  val gen_interface: SMT_Translate.builtins -> string list -> string list ->
     3.9      SMT_Solver.interface
    3.10 -  val interface: SMT_Solver.interface
    3.11 +  val interface: string list -> SMT_Solver.interface
    3.12  end
    3.13  
    3.14  structure SMTLIB_Interface: SMTLIB_INTERFACE =
    3.15 @@ -118,12 +118,13 @@
    3.16            | wr_pat (T.SNoPat ts) = wrp "nopat" ts
    3.17        in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
    3.18  
    3.19 -fun serialize attributes ({typs, funs, preds} : T.sign) ts stream =
    3.20 +fun serialize attributes comments ({typs, funs, preds} : T.sign) ts stream =
    3.21    let
    3.22      fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
    3.23    in
    3.24      stream
    3.25      |> wr_line (wr "(benchmark Isabelle")
    3.26 +    |> wr_line (wr ":status unknown")
    3.27      |> fold (wr_line o wr) attributes
    3.28      |> length typs > 0 ?
    3.29           wr_line (wr ":extrasorts" #> par (fold wr1 typs))
    3.30 @@ -138,6 +139,7 @@
    3.31      |> fold (fn t => wr ":assumption" #> wr_line (wr_expr false [] t)) ts
    3.32      |> wr_line (wr ":formula true")
    3.33      |> wr_line (wr ")")
    3.34 +    |> fold (fn comment => wr_line (wr ("; " ^ comment))) comments
    3.35      |> K ()
    3.36    end
    3.37  
    3.38 @@ -149,9 +151,9 @@
    3.39    builtin_num = builtin_num,
    3.40    builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
    3.41  
    3.42 -val default_attributes = [":logic AUFLIRA", ":status unknown"]
    3.43 +val default_attributes = [":logic AUFLIRA"]
    3.44  
    3.45 -fun gen_interface builtins attributes = {
    3.46 +fun gen_interface builtins attributes comments = {
    3.47    normalize = [
    3.48      SMT_Normalize.RewriteTrivialLets,
    3.49      SMT_Normalize.RewriteNegativeNumerals,
    3.50 @@ -170,8 +172,9 @@
    3.51        term_marker = term_marker,
    3.52        formula_marker = formula_marker },
    3.53      builtins = builtins,
    3.54 -    serialize = serialize attributes }}
    3.55 +    serialize = serialize attributes comments }}
    3.56  
    3.57 -val interface = gen_interface basic_builtins default_attributes
    3.58 +fun interface comments =
    3.59 +  gen_interface basic_builtins default_attributes comments
    3.60  
    3.61  end

     4.1 --- a/src/HOL/SMT/Tools/z3_interface.ML	Tue Feb 16 15:26:24 2010 +0100
     4.2 +++ b/src/HOL/SMT/Tools/z3_interface.ML	Tue Feb 16 16:20:34 2010 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  signature Z3_INTERFACE =
     4.6  sig
     4.7 -  val interface: SMT_Solver.interface
     4.8 +  val interface: string list -> SMT_Solver.interface
     4.9  end
    4.10  
    4.11  structure Z3_Interface: Z3_INTERFACE =