attempt to run a last chance procedure after the timeout

[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 51bd67286f0dc498886df771a0ae18cd2f91a8a8..32eff6826f468e9d652f4e5797916deccaba9666 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,7 +11,7 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-(* let debug s = prerr_endline s ;;*)
+let debug s = prerr_endline s ;;
 let debug _ = ();;
     
 module Paramod (B : Terms.Blob) = struct
@@ -139,7 +139,9 @@ module Paramod (B : Terms.Blob) = struct
       let bag, g_actives = 
        List.fold_left 
           (fun (bag,acc) c -> 
-            match Sup.simplify_goal maxvar (snd actives) bag acc c with
+            match 
+              Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
+            with
               | None -> bag, acc
               | Some (bag,c) -> bag,c::acc)
           (bag,[]) g_actives 
@@ -158,7 +160,7 @@ module Paramod (B : Terms.Blob) = struct
     add_passive_clauses g_passives new_goals
   ;;
  
-  let rec given_clause 
+  let rec given_clause ~noinfer 
     bag maxvar iterno max_steps timeout 
     actives passives g_actives g_passives 
   =
@@ -166,32 +168,77 @@ module Paramod (B : Terms.Blob) = struct
     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)));
+    if timeout <> None &&
+      (match timeout with
+      | None -> assert false
+      | Some timeout -> Unix.gettimeofday () > timeout) then
+       begin
+         prerr_endline("Last chance: "^string_of_float (Unix.gettimeofday()));
+          given_clause ~noinfer:true bag maxvar iterno max_steps None
+           actives passives g_actives g_passives
+             (*raise (Failure ("Timeout !",bag,maxvar,iterno))*)
+       end
+    else
 
     let use_age = iterno mod 10 = 0 in
 
     let rec aux_select bag passives g_passives =
+      if noinfer && 
+       is_passive_set_empty passives && 
+       is_passive_set_empty g_passives then
+         begin
+           prerr_endline 
+             ("Last chance: all is indexed " ^ string_of_float
+               (Unix.gettimeofday()));
+           let maxgoals = 100 in
+            List.fold_left 
+             (fun (acc,i) x -> 
+                if i < maxgoals then
+                ignore(Sup.simplify_goal ~no_demod:true 
+                         maxvar (snd actives) bag acc x)
+                else
+                  ();
+                x::acc,i+1)
+             ([],0) g_actives;
+           raise (Failure (("Last chance: failed over " ^ 
+              string_of_int maxgoals^ " goal " ^ 
+              string_of_float (Unix.gettimeofday())),bag,maxvar,0));
+         end;
       let backward,current,passives,g_passives =
        select ~use_age:false passives g_passives
       in
        if backward then
-        match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
+        match 
+          if noinfer then Some (bag,current)
+          else 
+            Sup.simplify_goal 
+              ~no_demod:false maxvar (snd actives) bag g_actives current 
+        with
            | None -> aux_select bag passives g_passives
            | Some (bag,g_current) ->
-               backward_infer_step bag maxvar actives passives
-                 g_actives g_passives g_current
+               if noinfer then 
+                let g_actives = g_current :: g_actives in 
+                bag,maxvar,actives,passives,g_actives,g_passives
+              else
+                backward_infer_step bag maxvar actives passives
+                  g_actives g_passives g_current
        else
          (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *)
-          match Sup.keep_simplified current actives bag maxvar with
+          match 
+            if noinfer then bag, Some (current,actives)
+           else Sup.keep_simplified current actives bag maxvar with
        (*  match Sup.one_pass_simplification current actives bag maxvar with*)
              | bag,None -> aux_select bag passives g_passives
              | bag,Some (current,actives) ->
-                 forward_infer_step bag maxvar actives passives
-                                    g_actives g_passives current
+                 if noinfer then
+                   let actives = 
+                     current::fst actives,
+                     IDX.index_unit_clause (snd actives) current
+                   in
+                   bag,maxvar,actives,passives,g_actives,g_passives
+                 else
+                   forward_infer_step bag maxvar actives passives
+                     g_actives g_passives current
     in
     
     (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
@@ -213,7 +260,7 @@ module Paramod (B : Terms.Blob) = struct
       debug
        (Printf.sprintf "Number of passives : %d"
           (passive_set_cardinal passives));
-      given_clause 
+      given_clause ~noinfer
         bag maxvar iterno max_steps timeout 
         actives passives g_actives g_passives
   ;;
@@ -229,7 +276,7 @@ module Paramod (B : Terms.Blob) = struct
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
     try 
-     given_clause 
+     given_clause ~noinfer:false
       bag maxvar 0 max_steps timeout actives passives g_actives g_passives
     with 
     | Sup.Success (bag, _, (i,_,_,_)) ->