X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic%2FcicUniv.ml;h=0d75caf898cec408590e0f82a59aaf22bfa4b085;hb=ed5b072125435beb688d4da148fd3b09f849658a;hp=8ae118c9b1bb5ecf1d4c656ffcfb2bfb4ba15c86;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/cic/cicUniv.ml b/components/cic/cicUniv.ml index 8ae118c9b..0d75caf89 100644 --- a/components/cic/cicUniv.ml +++ b/components/cic/cicUniv.ml @@ -554,6 +554,7 @@ let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) = end_spending (); rc,already_contained +(* profiling code let profiler_eq = HExtlib.profile "CicUniv.add_eq" let profiler_ge = HExtlib.profile "CicUniv.add_ge" let profiler_gt = HExtlib.profile "CicUniv.add_gt" @@ -563,6 +564,7 @@ let add_ge ?fast u v b = profiler_ge.HExtlib.profile (fun _ -> add_ge ?fast u v b) () let add_eq ?fast u v b = profiler_eq.HExtlib.profile (fun _ -> add_eq ?fast u v b) () +*) (*****************************************************************************) (** END: Decomment this for performance comparisons **) @@ -600,10 +602,13 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) = fst (merge_brutal increment base_ugraph), UriManager.UriSet.add uri_of_increment already_contained -let profiler_merge = HExtlib.profile "CicUniv.merge_graphs" +(* profiling code; WARNING: the time spent during profiling can be + greater than the profiled time +let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs" let merge_ugraphs ~base_ugraph ~increment = profiler_merge.HExtlib.profile (fun _ -> merge_ugraphs ~base_ugraph ~increment) () +*) (*****************************************************************************) (** Xml sesialization and parsing **)