X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUniv.ml;h=8ae118c9b1bb5ecf1d4c656ffcfb2bfb4ba15c86;hb=5104e38ee747fd1052ce21f3f9f2ecc778d590ba;hp=87839d8a39d12ae18c4e7524dfae26ca7e7951e0;hpb=9262517c80e17d46b9bf9931dc879ac653a633e9;p=helm.git

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                                           **)
 (*****************************************************************************)