--- a/src/HOL/Tools/SMT/smt_config.ML Fri Mar 05 17:29:49 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Fri Mar 05 20:38:55 2021 +0100
@@ -41,6 +41,7 @@
val compress_verit_proofs: Proof.context -> bool
(*tools*)
+ val get_timeout: Proof.context -> Time.time option
val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b
val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
@@ -218,6 +219,10 @@
(* tools *)
+fun get_timeout ctxt =
+ let val t = seconds (Config.get ctxt timeout);
+ in if Timeout.ignored t then NONE else SOME (Timeout.scale_time t) end;
+
fun with_time_limit ctxt timeout_config f x =
Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out