# HG changeset patch
# User wenzelm
# Date 1614973135 -3600
# Node ID a40e69fde2b45c69694f0ed3450929aa58bf9ef8
# Parent  3b5196dac4c8d43ee6d76bda045919573110dfca
clarified smt: support Timeout.ignored and Timeout.scale_time;

diff -r 3b5196dac4c8 -r a40e69fde2b4 src/HOL/Tools/SMT/smt_config.ML
--- 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
diff -r 3b5196dac4c8 -r a40e69fde2b4 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Fri Mar 05 17:29:49 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Fri Mar 05 20:38:55 2021 +0100
@@ -57,10 +57,12 @@
 (* CVC3 *)
 
 local
-  fun cvc3_options ctxt = [
-    "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
-    "-lang", "smt2",
-    "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]
+  fun cvc3_options ctxt =
+    ["-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
+     "-lang", "smt2"] @
+    (case SMT_Config.get_timeout ctxt of
+      NONE => []
+    | SOME t => ["-timeout", string_of_int (Real.ceil (Time.toReal t))])
 in
 
 val cvc3: SMT_Solver.solver_config = {
@@ -83,11 +85,13 @@
 val cvc4_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc4_extensions\<close> (K false)
 
 local
-  fun cvc4_options ctxt = [
-    "--no-stats",
-    "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
-    "--lang=smt2",
-    "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
+  fun cvc4_options ctxt =
+    ["--no-stats",
+     "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
+     "--lang=smt2"] @
+    (case SMT_Config.get_timeout ctxt of
+      NONE => []
+    | SOME t => ["--tlimit", string_of_int (Time.toMilliseconds t)])
 
   fun select_class ctxt =
     if Config.get ctxt cvc4_extensions then
@@ -125,6 +129,15 @@
       SMTLIB_Interface.hosmtlibC
     else
       SMTLIB_Interface.smtlibC
+
+  fun veriT_options ctxt =
+   ["--proof-with-sharing",
+    "--proof-define-skolems",
+    "--proof-prune",
+    "--proof-merge",
+    "--disable-print-success",
+    "--disable-banner"] @
+    Verit_Proof.veriT_current_strategy (Context.Proof ctxt)
 in
 
 val veriT: SMT_Solver.solver_config = {
@@ -132,14 +145,7 @@
   class = select_class,
   avail = is_some o check_tool "ISABELLE_VERIT",
   command = the o check_tool "ISABELLE_VERIT",
-  options = (fn ctxt => [
-    "--proof-with-sharing",
-    "--proof-define-skolems",
-    "--proof-prune",
-    "--proof-merge",
-    "--disable-print-success",
-    "--disable-banner"] @
-    Verit_Proof.veriT_current_strategy (Context.Proof ctxt)),
+  options = veriT_options,
   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 200 (* FUDGE *),
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "timeout"),
@@ -156,9 +162,11 @@
 local
   fun z3_options ctxt =
     ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
-     "smt.refine_inj_axioms=false",
-     "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)),
-     "-smt2"]
+     "smt.refine_inj_axioms=false"] @
+    (case SMT_Config.get_timeout ctxt of
+      NONE => []
+    | SOME t => ["-T:" ^ string_of_int (Real.ceil (Time.toReal t))]) @
+    ["-smt2"]
 
   fun select_class ctxt =
     if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC
diff -r 3b5196dac4c8 -r a40e69fde2b4 src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Fri Mar 05 17:29:49 2021 +0100
+++ b/src/Pure/Concurrent/timeout.ML	Fri Mar 05 20:38:55 2021 +0100
@@ -9,6 +9,7 @@
 signature TIMEOUT =
 sig
   exception TIMEOUT of Time.time
+  val ignored: Time.time -> bool
   val scale: unit -> real
   val scale_time: Time.time -> Time.time
   val end_time: Time.time -> Time.time
@@ -21,13 +22,15 @@
 
 exception TIMEOUT of Time.time;
 
+fun ignored timeout = timeout < Time.fromMilliseconds 1;
+
 fun scale () = Options.default_real "timeout_scale";
 fun scale_time t = Time.scale (scale ()) t;
 
 fun end_time timeout = Time.now () + scale_time timeout;
 
 fun apply timeout f x =
-  if timeout < Time.fromMilliseconds 1 then f x
+  if ignored timeout then f x
   else
     Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
       let