Fixed pretty printer and debug printings

[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 d65fce1b2fa4e1fb877b1c3f0b8475d81ee14788..48811239bf08a30caaca026a3c97929be3e4e590 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 (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,12 +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 
@@ -294,7 +294,7 @@ module Paramod (B : Orderings.Blob) = struct
               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
@@ -328,7 +328,6 @@ module Paramod (B : Orderings.Blob) = struct
       (*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 bag passives g_passives
     in