--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 03 16:44:38 2010 +0100
@@ -35,7 +35,7 @@
val filter_only: bool Config.T
val datatypes: bool Config.T
val keep_assms: bool Config.T
- val timeout: int Config.T
+ val timeout: real Config.T
val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
val traceN: string
val trace: bool Config.T
@@ -127,10 +127,10 @@
val (keep_assms, setup_keep_assms) =
Attrib.config_bool "smt_keep_assms" (K true)
-val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
+val (timeout, setup_timeout) = Attrib.config_real "smt_timeout" (K 30.0)
fun with_timeout ctxt f x =
- TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
+ TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
handle TimeLimit.TimeOut => raise SMT Time_Out
val traceN = "smt_trace"
@@ -252,7 +252,7 @@
let
val args = more_opts @ options ctxt
val comments = ("solver: " ^ name) ::
- ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
+ ("timeout: " ^ Time.toString (seconds (Config.get ctxt timeout))) ::
"arguments:" :: args
in
irules
@@ -433,7 +433,7 @@
val {facts, goal, ...} = Proof.goal st
val ctxt =
Proof.context_of st
- |> Config.put timeout (Time.toSeconds time_limit)
+ |> Config.put timeout (Real.fromInt (Time.toSeconds time_limit))
|> Config.put oracle false
|> Config.put filter_only true
|> Config.put keep_assms false
@@ -504,7 +504,7 @@
fun print_setup context =
let
- val t = string_of_int (Config.get_generic context timeout)
+ val t = Time.toString (seconds (Config.get_generic context timeout))
val names = sort_strings (all_solver_names_of context)
val ns = if null names then [no_solver] else names
val n = solver_name_of context