Removed dead code

[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 ac73df2d0b90fb1fd0fc9110536c13bee8885922..0dbd6260aede1286d79976ea364a17e40d1ca5b1 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,8 +11,8 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-let debug s = prerr_endline s ;;
-let debug _ = ();;
+let debug s = prerr_endline (Lazy.force s) ;; 
+let debug _ = ();; 
 
 let monster = 100;;
     
@@ -162,11 +162,11 @@ module Paramod (B : Orderings.Blob) = struct
   let backward_infer_step bag maxvar actives passives
                           g_actives g_passives g_current iterno =
     (* superposition left, simplifications on goals *)
-      debug "infer_left step...";
+      debug (lazy "infer_left step...");
       let bag, maxvar, new_goals = 
         Sup.infer_left bag maxvar g_current actives 
       in
-        debug "Performed infer_left step";
+        debug (lazy "Performed infer_left step");
        let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
         bag, maxvar, actives, passives, g_current::g_actives,
     (add_passive_goals g_passives new_goals)
@@ -184,11 +184,12 @@ module Paramod (B : Orderings.Blob) = struct
      * new = supright e'' A'' *
      * new'= demod A'' new    *
      * P' = P + new'          *)
-    debug "Forward infer step...";
+    debug (lazy "Forward infer step...");
+    debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
     let bag, maxvar, actives, new_clauses = 
       Sup.infer_right bag maxvar current actives 
     in
-      debug "Demodulating goals with actives...";
+      debug (lazy "Demodulating goals with actives...");
       (* keep goals demodulated w.r.t. actives and check if solved *)
       let bag, g_actives = 
         List.fold_left 
@@ -209,6 +210,7 @@ module Paramod (B : Orderings.Blob) = struct
           (bag,maxvar,[]) g_actives 
       in
       let bag = Terms.replace_in_bag (current,false,iterno) bag in
+       (* prerr_endline (Pp.pp_bag bag); *)
     bag, maxvar, actives,
     add_passive_clauses passives new_clauses, g_actives,
     add_passive_goals g_passives new_goals
@@ -228,8 +230,8 @@ module Paramod (B : Orderings.Blob) = struct
         if noinfer then
           begin
             debug 
-              ("Last chance: all is indexed " ^ string_of_float
-                (Unix.gettimeofday()));
+              (lazy("Last chance: all is indexed " ^ string_of_float
+                (Unix.gettimeofday())));
             let maxgoals = 100 in
             ignore(List.fold_left 
               (fun (acc,i) x -> 
@@ -244,7 +246,7 @@ module Paramod (B : Orderings.Blob) = struct
           end
         else if false then (* activates last chance strategy *)
           begin
-           debug("Last chance: "^string_of_float (Unix.gettimeofday()));
+           debug (lazy("Last chance: "^string_of_float (Unix.gettimeofday())));
            given_clause ~useage ~noinfer:true bag maxvar iterno weight_picks max_steps 
              (Some (Unix.gettimeofday () +. 20.))
              actives passives g_actives g_passives;
@@ -269,7 +271,7 @@ module Paramod (B : Orderings.Blob) = struct
        else
          let bag = Terms.replace_in_bag (current,false,iterno) bag in
         if backward then
-          let _ = debug ("Selected goal : " ^ Pp.pp_unit_clause current) in
+          let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in
          match 
            if noinfer then 
              if weight > monster then None else Some (bag,current)
@@ -286,14 +288,14 @@ module Paramod (B : Orderings.Blob) = struct
                  backward_infer_step bag maxvar actives passives
                    g_actives g_passives g_current iterno
         else
-          let _ = debug ("Selected fact : " ^ Pp.pp_unit_clause current) in
+          let _ = debug (lazy("Selected fact : " ^ Pp.pp_unit_clause current)) in
          (*let is_orphan = Sup.orphan_murder bag (fst actives) current in*)
           match 
             if noinfer then 
               if weight > monster then bag,None 
               else  bag, Some (current,actives)
             else if Sup.orphan_murder bag (fst actives) current then
-             let _ = debug "Orphan murdered" in
+             let _ = debug (lazy "Orphan murdered") in
               let bag = Terms.replace_in_bag (current,true,iterno) bag in
                 bag, None
             else Sup.keep_simplified current actives bag maxvar
@@ -332,23 +334,23 @@ module Paramod (B : Orderings.Blob) = struct
       aux_select bag passives g_passives
     in
       debug
-        (Printf.sprintf "Number of active goals : %d"
-           (List.length g_actives));
+        (lazy(Printf.sprintf "Number of active goals : %d"
+           (List.length g_actives)));
       debug
-        (Printf.sprintf "Number of passive goals : %d"
-           (passive_set_cardinal g_passives));
+        (lazy(Printf.sprintf "Number of passive goals : %d"
+           (passive_set_cardinal g_passives)));
       debug
-        (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
+        (lazy(Printf.sprintf "Number of actives : %d" (List.length (fst actives))));
       debug
-        (Printf.sprintf "Number of passives : %d"
-           (passive_set_cardinal passives));
+        (lazy(Printf.sprintf "Number of passives : %d"
+           (passive_set_cardinal passives)));
       given_clause ~useage ~noinfer
         bag maxvar iterno weight_picks max_steps timeout 
         actives passives g_actives g_passives
   ;;
 
   let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
-    let initial_timestamp = Unix.gettimeofday () in
+    let _initial_timestamp = Unix.gettimeofday () in
     let passives =
       add_passive_clauses ~no_weight:true passive_empty_set passives
     in
@@ -396,9 +398,6 @@ module Paramod (B : Orderings.Blob) = struct
                (Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
                   id it (Order.compute_unit_clause_weight cl) 
                   (Pp.pp_proof_step proof))) l;*)
-        prerr_endline 
-          (Printf.sprintf "Found proof, %fs" 
-            (Unix.gettimeofday() -. initial_timestamp));
         (* 
         prerr_endline "Proof:"; 
         List.iter (fun x ->