From 57977d3ced75bb9d523280bcfd6e4bcfb07ba83e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 11 Oct 2006 09:49:27 +0000 Subject: [PATCH] My previous commit changed the regular timeout of paramodulation from infinity to 30s. Old behaviour restored. --- components/tactics/auto.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 305a42ab1..194f05dc9 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -555,10 +555,12 @@ let int params name default = raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) ;; -let flags_of_params params ?(use_only_paramod = bool params "paramodulation" false) () = +let flags_of_params params ?(for_applyS=false) () = let int = int params in let bool = bool params in let use_paramod = bool "use_paramod" true in + let use_only_paramod = + if for_applyS then true else bool "paramodulation" true in let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in let timeout = int "timeout" 0 in @@ -567,7 +569,7 @@ let flags_of_params params ?(use_only_paramod = bool params "paramodulation" fal AutoTypes.maxwidth = width; AutoTypes.timeout = if timeout = 0 then - if use_only_paramod then Unix.gettimeofday () +. 30.0 + if for_applyS then Unix.gettimeofday () +. 30.0 else 0.0 else @@ -583,7 +585,7 @@ let applyS_tac ~dbd ~term ~params = try let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] - (flags_of_params params ~use_only_paramod:true ()) status + (flags_of_params params ~for_applyS:true ()) status in proof, gl with -- 2.39.2