From b555e6b8c27c765a4611dda9528963ebff116412 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Jan 2006 15:14:26 +0000 Subject: [PATCH] some debug prints/stats --- helm/ocaml/cic/cicUniv.ml | 107 +++++++++++++++++++++---------------- helm/ocaml/cic/cicUniv.mli | 1 + 2 files changed, 61 insertions(+), 47 deletions(-) diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index 87839d8a3..8ae118c9b 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -135,21 +135,6 @@ let string_of_mal m = let string_of_bag b = string_of_mal b -(*****************************************************************************) -(** Helpers **) -(*****************************************************************************) - -(* find the repr *) -let repr u m = - try - MAL.find u m - with - Not_found -> empty_entry - -(* FIXME: May be faster if we make it by hand *) -let merge_closures f nodes m = - SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty - (*****************************************************************************) (** Benchmarking **) (*****************************************************************************) @@ -169,7 +154,23 @@ let end_spending () = partial := 0.0; time_spent := !time_spent +. interval ;; - + + +(*****************************************************************************) +(** Helpers **) +(*****************************************************************************) + +(* find the repr *) +let repr u m = + try + MAL.find u m + with + Not_found -> empty_entry + +(* FIXME: May be faster if we make it by hand *) +let merge_closures f nodes m = + SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty + (*****************************************************************************) (** _fats implementation **) @@ -536,62 +537,74 @@ let add_eq ?(fast=(!fast_implementation)) u v (b,already_contained) = (*prerr_endline "add_eq";*) begin_spending (); let rc = add_eq ~fast u v b in - end_spending(); + end_spending (); rc,already_contained let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained) = (* prerr_endline "add_ge"; *) begin_spending (); let rc = add_ge ~fast u v b in - end_spending(); + end_spending (); rc,already_contained let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) = (* prerr_endline "add_gt"; *) begin_spending (); let rc = add_gt ~fast u v b in - end_spending(); + end_spending (); rc,already_contained + +let profiler_eq = HExtlib.profile "CicUniv.add_eq" +let profiler_ge = HExtlib.profile "CicUniv.add_ge" +let profiler_gt = HExtlib.profile "CicUniv.add_gt" +let add_gt ?fast u v b = + profiler_gt.HExtlib.profile (fun _ -> add_gt ?fast u v b) () +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 **) (*****************************************************************************) let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) = - (* this sucks *) let merge_brutal (u,_) v = - if u = empty_bag then - ((*prerr_endline "HIT2";*)v) - else if fst v = empty_bag then - ((*prerr_endline "HIT3";*) u, snd v) - else - ((*prerr_endline "MISS";*) - let m1 = u in - let m2 = v in - MAL.fold ( - fun k v x -> - (SOF.fold ( - fun u x -> - let m = add_gt k u x in m) - (SOF.union v.one_s_gt v.gt_closure) - (SOF.fold ( - fun u x -> - let m = add_ge k u x in m) - (SOF.union v.one_s_ge v.ge_closure) - (SOF.fold ( - fun u x -> - let m = add_eq k u x in m) - (SOF.union v.one_s_eq v.eq_closure) x))) - ) m1 m2) + let m1 = u in + let m2 = v in + MAL.fold ( + fun k v x -> + (SOF.fold ( + fun u x -> + let m = add_gt k u x in m) + (SOF.union v.one_s_gt v.gt_closure) + (SOF.fold ( + fun u x -> + let m = add_ge k u x in m) + (SOF.union v.one_s_ge v.ge_closure) + (SOF.fold ( + fun u x -> + let m = add_eq k u x in m) + (SOF.union v.one_s_eq v.eq_closure) x))) + ) m1 m2 in - let _, already_contained = base_ugraph in - if UriManager.UriSet.mem uri_of_increment already_contained then - ((*prerr_endline "HIT1";*) - base_ugraph) + let base, already_contained = base_ugraph in + if MAL.is_empty base then + increment + else if + MAL.is_empty (fst increment) || + UriManager.UriSet.mem uri_of_increment already_contained + then + base_ugraph else fst (merge_brutal increment base_ugraph), UriManager.UriSet.add uri_of_increment already_contained +let profiler_merge = HExtlib.profile "CicUniv.merge_graphs" +let merge_ugraphs ~base_ugraph ~increment = + profiler_merge.HExtlib.profile + (fun _ -> merge_ugraphs ~base_ugraph ~increment) () + (*****************************************************************************) (** Xml sesialization and parsing **) (*****************************************************************************) diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli index cdeaa378e..eb3c50866 100644 --- a/helm/ocaml/cic/cicUniv.mli +++ b/helm/ocaml/cic/cicUniv.mli @@ -151,3 +151,4 @@ val eq: universe -> universe -> bool *) val get_spent_time: unit -> float val reset_spent_time: unit -> unit + -- 2.39.2