# HG changeset patch
# User boehmes
# Date 1419861433 -3600
# Node ID ef5e68575bc48e61d0ad31d68f598146a4b92316
# Parent  3a594fd13ca4ff44359d44812040b8707c72957e
limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps

diff -r 3a594fd13ca4 -r ef5e68575bc4 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Sun Dec 28 15:42:34 2014 +1100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Dec 29 14:57:13 2014 +0100
@@ -24,6 +24,7 @@
   (*options*)
   val oracle: bool Config.T
   val timeout: real Config.T
+  val reconstruction_step_timeout: real Config.T
   val random_seed: int Config.T
   val read_only_certificates: bool Config.T
   val verbose: bool Config.T
@@ -35,6 +36,7 @@
   val sat_solver: string Config.T
 
   (*tools*)
+  val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
 
   (*diagnostics*)
@@ -149,6 +151,7 @@
 
 val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true)
 val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
+val reconstruction_step_timeout = Attrib.setup_config_real @{binding smt_reconstruction_step_timeout} (K 10.0)
 val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
 val read_only_certificates = Attrib.setup_config_bool @{binding smt_read_only_certificates} (K false)
 val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
@@ -171,10 +174,12 @@
 
 (* tools *)
 
-fun with_timeout ctxt f x =
-  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
+fun with_time_limit ctxt timeout_config f x =
+  TimeLimit.timeLimit (seconds (Config.get ctxt timeout_config)) f x
   handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
 
+fun with_timeout ctxt = with_time_limit ctxt timeout
+
 
 (* certificates *)
 
diff -r 3a594fd13ca4 -r ef5e68575bc4 src/HOL/Tools/SMT/z3_replay.ML
--- a/src/HOL/Tools/SMT/z3_replay.ML	Sun Dec 28 15:42:34 2014 +1100
+++ b/src/HOL/Tools/SMT/z3_replay.ML	Mon Dec 29 14:57:13 2014 +0100
@@ -66,8 +66,12 @@
       (if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
 
 fun replay_step ctxt assumed (step as Z3_Proof.Z3_Step {id, prems, fixes, ...}) proofs =
-  let val nthms = map (the o Inttab.lookup proofs) prems
-  in Inttab.update (id, (fixes, replay_thm ctxt assumed nthms step)) proofs end
+  let
+    val nthms = map (the o Inttab.lookup proofs) prems
+    val replay = replay_thm ctxt assumed nthms
+    val thm = SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
+      handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+  in Inttab.update (id, (fixes, thm)) proofs end
 
 local
   val remove_trigger = mk_meta_eq @{thm trigger_def}