From: denes <??>
Date: Wed, 22 Jul 2009 13:14:16 +0000 (+0000)
Subject: Now using lazy strings for debug printings
X-Git-Tag: make_still_working~3634
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63741bdebe93f58cef3ea791ca634ef17237bd7f;p=helm.git

Now using lazy strings for debug printings
---

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 520d52396..45a4e0e09 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -185,7 +185,7 @@ module Paramod (B : Orderings.Blob) = struct
      * new'= demod A'' new    *
      * P' = P + new'          *)
     debug "Forward infer step...";
-    debug ("Number of actives : " ^ (string_of_int (List.length (fst actives))));
+    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
@@ -230,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 -> 
@@ -246,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;
@@ -271,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)
@@ -288,7 +288,7 @@ 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 
@@ -334,16 +334,16 @@ 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
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 603735479..994a141c9 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -730,8 +730,8 @@ module Superposition (B : Orderings.Blob) =
       in
         debug "Another superposition";
       let new_clauses = new_clauses @ additional_new_clauses in
-        debug (Printf.sprintf "Demodulating %d clauses"
-                 (List.length new_clauses));
+        debug (lazy (Printf.sprintf "Demodulating %d clauses"
+                 (List.length new_clauses)));
       let bag, new_clauses = 
         HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses
       in