X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=67df0654ecf88bf3d0f73d5f7279700b9ec45a7d;hb=4693f3b9de6d867921b51f61e9a7dc36c3da1b77;hp=0dbac61c3be98ac41ab5f212727a5f8a3be946e2;hpb=bebc917ebff72c2e235cb3062a4c94f10a9aab27;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 0dbac61c3..67df0654e 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -22,7 +22,7 @@ module Superposition (B : Orderings.Blob) =
     
     exception Success of B.t Terms.bag * int * B.t Terms.clause
 
-    let debug s = prerr_endline s;;
+    let debug s = prerr_endline (Lazy.force s);;
     let debug _ = ();;
     let enable = true;;
 
@@ -410,7 +410,7 @@ module Superposition (B : Orderings.Blob) =
       let (id,_,_,_,_) = cl in
       let actives = List.map (fun (i,_,_,_,_) -> i) actives in
       let (res,_) = orphan_murder bag actives id in
-        if res then debug "Orphan murdered"; res
+        if res then debug (lazy "Orphan murdered"); res
     ;;
     let prof_orphan_murder = HExtlib.profile ~enable "orphan_murder";;
     let orphan_murder bag actives x =
@@ -588,6 +588,7 @@ module Superposition (B : Orderings.Blob) =
     (* this is OK for both the sup_left and sup_right inference steps *)
     let superposition table varlist subterm pos context =
       let cands = IDX.DT.retrieve_unifiables table subterm in
+      debug (lazy (string_of_int (IDX.ClauseSet.cardinal cands) ^ " candidates found"));
       HExtlib.filter_map
         (fun (dir, _, _, (id,nlit,plit,vl,_ (*as uc*))) ->
            match nlit,plit with
@@ -669,7 +670,7 @@ module Superposition (B : Orderings.Blob) =
         in
         bag, (alist, List.fold_left IDX.index_clause IDX.DT.empty alist)
       in*)
-        debug "Simplified active clauses with fact";
+        debug (lazy "Simplified active clauses with fact");
       (* We superpose active clauses with current *)
       let bag, maxvar, new_clauses =
         List.fold_left 
@@ -680,13 +681,13 @@ module Superposition (B : Orderings.Blob) =
              bag, maxvar, newc @ acc)
           (bag, maxvar, []) alist
       in
-        debug "First superpositions";
+        debug (lazy "First superpositions");
         (* We add current to active clauses so that it can be *
          * superposed with itself                             *)
       let alist, atable = 
         current :: alist, IDX.index_clause atable current
       in
-        debug "Indexed";
+        debug (lazy "Indexed");
       let fresh_current, maxvar = Utils.fresh_clause maxvar current in
         (* We need to put fresh_current into the bag so that all *
          * variables clauses refer to are known.                 *)
@@ -695,14 +696,14 @@ module Superposition (B : Orderings.Blob) =
       let bag, maxvar, additional_new_clauses =
         superposition_with_table bag maxvar fresh_current atable 
       in
-        debug "Another superposition";
+        debug (lazy "Another superposition");
       let new_clauses = new_clauses @ additional_new_clauses in
         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
-        debug "Demodulated new clauses";
+        debug (lazy "Demodulated new clauses");
       bag, maxvar, (alist, atable), new_clauses
     ;;
 
@@ -718,7 +719,7 @@ module Superposition (B : Orderings.Blob) =
       let bag, maxvar, new_goals =        
         superposition_with_table bag maxvar goal atable 
       in
-        debug "Superposed goal with active clauses";
+        debug (lazy "Superposed goal with active clauses");
         (* We simplify the new goals with active clauses *)
       let bag, new_goals = 
         List.fold_left
@@ -728,7 +729,7 @@ module Superposition (B : Orderings.Blob) =
               | Some (bag,g) -> bag,g::acc)
          (bag, []) new_goals
       in
-        debug "Simplified new goals with active clauses";
+        debug (lazy "Simplified new goals with active clauses");
       bag, maxvar, List.rev new_goals
     ;;