added timeout parameter to auto paramodulation.

[helm.git] / helm / software / components / tactics / autoTactic.ml

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index f063eeafb69ff99d7d49bf6b6810d6768f302e41..b4a3118199d517266147b7712a976a54ce841e08 100644 (file)
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -325,6 +325,7 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
   (* argument parsing *)
   let depth = int "depth" params in
   let width = int "width" params in
+  let timeout = string "timeout" params in
   let paramodulation = bool "paramodulation" params in
   let full = bool "full" params in
   let superposition = bool "superposition" params in
@@ -333,6 +334,9 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
   let subterms_only = bool "subterms_only" params in
   let caso_strano = bool "caso_strano" params in
   let demod_table = string "demod_table" params in
+  let timeout = 
+    try Some (float_of_string timeout) with Failure _ -> None
+  in
   (* the real tactic *)
   let auto_tac dbd (proof, goal) =
     let normal_auto () = 
@@ -364,7 +368,8 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
       try
-        let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full (proof, goal) in
+        let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full
+        ?timeout (proof, goal) in
         prerr_endline (Saturation.get_stats ());
         rc
       with exn ->