timeouts are passed as arguments, so that tptpprover can

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index d63d1449a2236d51f531b9c226e5d6818ebcf692..d85c5627a4e4b4e97d1a9e667253dac41cd7aecb 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,12 +11,9 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
- (*let debug s = prerr_endline s ;;*)
- let debug _ = ();;
+let debug s = prerr_endline s ;;
+let debug _ = ();;
     
-let max_nb_iter = max_int ;;
-let amount_of_time = 300.0 ;;
-
 module Paramod (B : Terms.Blob) = struct
   exception Failure of string * B.t Terms.bag * int * int
   type bag = B.t Terms.bag * int
@@ -159,18 +156,21 @@ module Paramod (B : Terms.Blob) = struct
     add_passive_clauses g_passives new_goals
   ;;
  
-  let rec given_clause bag maxvar nb_iter timeout actives passives g_actives g_passives =
-    (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
-      prerr_endline "Active table :"; 
-       (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
-         (fst actives)); *)
-    let nb_iter = nb_iter + 1 in
-    if nb_iter = max_nb_iter then       
-      raise (Failure ("No iterations left !",bag,maxvar,nb_iter));
-    if Unix.gettimeofday () > timeout then
-      raise (Failure ("Timeout !",bag,maxvar,nb_iter));
+  let rec given_clause 
+    bag maxvar iterno max_steps timeout 
+    actives passives g_actives g_passives 
+  =
+    let iterno = iterno + 1 in
+    if iterno = max_steps then       
+      raise (Failure ("No iterations left !",bag,maxvar,iterno));
+    (* timeout check: gettimeofday called only if timeout set *)
+    (match timeout with
+    | None -> ()
+    | Some timeout ->
+        if Unix.gettimeofday () > timeout then
+          raise (Failure ("Timeout !",bag,maxvar,iterno)));
 
-    let use_age = nb_iter mod 10 = 0 in
+    let use_age = iterno mod 10 = 0 in
 
     let rec aux_select passives g_passives =
       let backward,current,passives,g_passives =
@@ -191,6 +191,11 @@ module Paramod (B : Terms.Blob) = struct
                  forward_infer_step bag maxvar actives passives
                                     g_actives g_passives current
     in
+    
+    (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
+      prerr_endline "Active table :"; 
+       (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
+         (fst actives)); *)
 
     let bag,maxvar,actives,passives,g_actives,g_passives =      
       aux_select passives g_passives
@@ -207,18 +212,19 @@ module Paramod (B : Terms.Blob) = struct
        (Printf.sprintf "Number of passives : %d"
           (passive_set_cardinal passives));
       given_clause 
-        bag maxvar nb_iter timeout actives passives g_actives g_passives
+        bag maxvar iterno max_steps timeout 
+        actives passives g_actives g_passives
   ;;
 
-  let paramod (bag,maxvar) ~g_passives ~passives =
-    let timeout = Unix.gettimeofday () +. amount_of_time in 
+  let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+    let initial_timestamp = Unix.gettimeofday () in
     let passives = add_passive_clauses passive_empty_set passives in
     let g_passives = add_passive_clauses passive_empty_set g_passives in
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
     try 
      given_clause 
-      bag maxvar 0 timeout actives passives g_actives g_passives
+      bag maxvar 0 max_steps timeout actives passives g_actives g_passives
     with 
     | Sup.Success (bag, _, (i,_,_,_)) ->
         let l =
@@ -240,14 +246,16 @@ module Paramod (B : Terms.Blob) = struct
         in
         prerr_endline 
           (Printf.sprintf "Found proof, %fs" 
-            (Unix.gettimeofday() -. timeout +. amount_of_time));
-        (* prerr_endline "Proof:"; 
-        List.iter (fun x -> prerr_endline (string_of_int x);
-                prerr_endline (Pp.pp_unit_clause (fst (Terms.M.find x bag)))) l;*)
+            (Unix.gettimeofday() -. initial_timestamp));
+        (* 
+        prerr_endline "Proof:"; 
+        List.iter (fun x ->
+          prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l;
+        *)
         [ bag, i, l ]
-    | Failure (msg,_bag,_maxvar,nb_iter) -> 
+    | Failure (msg,_bag,_maxvar,iterno) -> 
         prerr_endline msg;
-        prerr_endline (Printf.sprintf "FAILURE in %d iterations" nb_iter); 
+        prerr_endline (Printf.sprintf "FAILURE in %d iterations" iterno); 
         []
   ;;