From: Andrea Asperti Date: Mon, 11 Jan 2010 11:21:00 +0000 (+0000) Subject: Debugging info X-Git-Tag: make_still_working~3131 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e1c9f6efed4412893819965af30f6e44fa23f37b;p=helm.git Debugging info --- diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 6f1fb0f7f..6ec6048de 100644 --- 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 *)