--- 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
--- 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
--- 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