Debugging info

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 6f1fb0f7f91a3e1395bf3dc71fa6a65cb39a3136..6ec6048de9147191b13cfd96b14b5e763df8c255 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -247,10 +247,12 @@ module Superposition (B : Orderings.Blob) =
                      ((*prerr_endline ("Filtering: " ^ 
                         Pp.pp_foterm side ^ " =(< || =)" ^ 
                         Pp.pp_foterm newside ^ " coming from " ^ 
-                        Pp.pp_unit_clause uc );*)None)
+                        Pp.pp_unit_clause uc );*)
+                      debug (lazy "not applied");None)
                  else
                    Some (newside, subst, id, dir)
-               with FoUnif.UnificationFailure _ -> None)
+               with FoUnif.UnificationFailure _ -> 
+                 debug (lazy "not applied"); None)
         (IDX.ClauseSet.elements cands)
     ;;
 
@@ -268,7 +270,7 @@ module Superposition (B : Orderings.Blob) =
     ;;
       
     let rec demodulate bag (id, literal, vl, pr) table =
-      debug (lazy "demodulate...");
+      debug (lazy ("demodulate " ^ (string_of_int id)));
        match literal with
       | Terms.Predicate t -> assert false
       | Terms.Equation (l,r,ty,_) ->
@@ -750,6 +752,10 @@ module Superposition (B : Orderings.Blob) =
              bag, maxvar, newc @ acc)
           (bag, maxvar, []) alist
       in
+        debug
+       (lazy 
+        ("New clauses :" ^ (String.concat ";\n" 
+           (List.map Pp.pp_unit_clause new_clauses)))); 
         debug (lazy "First superpositions");
         (* We add current to active clauses so that it can be *
          * superposed with itself                             *)